:: Differentiability of Polynomials over Reals
:: by Artur Korni{\l}owicz
::
:: Received February 23, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

theorem Th1: :: POLYDIFF:1

for f being complex-valued Function holds 0 + f = f

proof end;

theorem :: POLYDIFF:2

for f being complex-valued Function holds f - 0 = f

proof end;

registration

let f be complex-valued Function;

reduce 0 + f to f;

reducibility
0 + f = f by Th1;

reduce f - 0 to f;

reducibility
f - 0 = f ;

end;

theorem Th3: :: POLYDIFF:3

for c being Complex
for f being complex-valued Function holds c + f = ((dom f) --> c) + f

proof end;

theorem Th4: :: POLYDIFF:4

for c being Complex
for f being complex-valued Function holds f - c = f - ((dom f) --> c)

proof end;

theorem Th5: :: POLYDIFF:5

for c being Complex
for f being complex-valued Function holds c (#) f = ((dom f) --> c) (#) f

proof end;

theorem Th6: :: POLYDIFF:6

for f being complex-valued Function holds f + ((dom f) --> 0) = f

proof end;

theorem Th7: :: POLYDIFF:7

for f being complex-valued Function holds f - ((dom f) --> 0) = f

proof end;

theorem :: POLYDIFF:8

#Z 0 = REAL --> 1

proof end;

registration

cluster Function-like V28( REAL , REAL ) differentiable -> continuous for Element of K10(K11(REAL,REAL));

coherence
for b₁ being Function of REAL,REAL st b₁ is differentiable holds
b₁ is continuous

proof end;

end;

definition

let f be differentiable Function of REAL,REAL;

func f `| -> Function of REAL,REAL equals :: POLYDIFF:def 1
f `| REAL;

coherence
f `| REAL is Function of REAL,REAL

proof end;

end;

:: deftheorem defines `| POLYDIFF:def 1 :
for f being differentiable Function of REAL,REAL holds f `| = f `| REAL;

theorem Th9: :: POLYDIFF:9

for f being Function of REAL,REAL holds
( f is differentiable iff for r being Real holds f is_differentiable_in r )

proof end;

theorem Th10: :: POLYDIFF:10

for r being Real
for f being differentiable Function of REAL,REAL holds (f `|) . r = diff (f,r)

proof end;

definition

let f be Function of REAL,REAL;

redefine attr f is differentiable means :: POLYDIFF:def 2
for r being Real holds f is_differentiable_in r;

compatibility
( f is differentiable iff for r being Real holds f is_differentiable_in r ) by Th9;

end;

:: deftheorem defines differentiable POLYDIFF:def 2 :
for f being Function of REAL,REAL holds
( f is differentiable iff for r being Real holds f is_differentiable_in r );

Lm1: [#] REAL is open Subset of REAL
;

registration

cluster Function-like constant V28( REAL , REAL ) -> differentiable for Element of K10(K11(REAL,REAL));

coherence
for b₁ being Function of REAL,REAL st b₁ is constant holds
b₁ is differentiable

proof end;

end;

theorem Th11: :: POLYDIFF:11

for f being constant Function of REAL,REAL holds f `| = REAL --> 0

proof end;

registration

cluster id REAL -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = id REAL holds
b₁ is differentiable

proof end;

end;

theorem :: POLYDIFF:12

(id REAL) `| = REAL --> 1

proof end;

registration

let n be Nat;

cluster #Z n -> differentiable ;

coherence
#Z n is differentiable

proof end;

end;

theorem Th13: :: POLYDIFF:13

for n being Nat holds (#Z n) `| = n (#) (#Z (n - 1))

proof end;

registration

let f, g be differentiable Function of REAL,REAL;

cluster f + g -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = f + g holds
b₁ is differentiable

proof end;

cluster f - g -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = f - g holds
b₁ is differentiable

proof end;

cluster f (#) g -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = f (#) g holds
b₁ is differentiable

proof end;

end;

registration

let f be differentiable Function of REAL,REAL;
let r be Real;

cluster r + f -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = r + f holds
b₁ is differentiable

proof end;

cluster r (#) f -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = r (#) f holds
b₁ is differentiable

proof end;

cluster f - r -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = f - r holds
b₁ is differentiable ;

end;

registration

let f be differentiable Function of REAL,REAL;

cluster - f -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = - f holds
b₁ is differentiable ;

cluster f ^2 -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = f ^2 holds
b₁ is differentiable ;

end;

theorem Th14: :: POLYDIFF:14

for f, g being differentiable Function of REAL,REAL holds (f + g) `| = (f `|) + (g `|)

proof end;

theorem Th15: :: POLYDIFF:15

for f, g being differentiable Function of REAL,REAL holds (f - g) `| = (f `|) - (g `|)

proof end;

theorem :: POLYDIFF:16

for f, g being differentiable Function of REAL,REAL holds (f (#) g) `| = (g (#) (f `|)) + (f (#) (g `|))

proof end;

theorem :: POLYDIFF:17

for r being Real
for f being differentiable Function of REAL,REAL holds (r + f) `| = f `|

proof end;

theorem :: POLYDIFF:18

for r being Real
for f being differentiable Function of REAL,REAL holds (f - r) `| = f `|

proof end;

theorem Th19: :: POLYDIFF:19

for r being Real
for f being differentiable Function of REAL,REAL holds (r (#) f) `| = r (#) (f `|)

proof end;

theorem :: POLYDIFF:20

for f being differentiable Function of REAL,REAL holds (- f) `| = - (f `|) by Th19;

theorem Th21: :: POLYDIFF:21

for L being non empty ZeroStr
for x being Element of L
for f being the carrier of b₁ -valued Function
for a being object holds Support (f +* (a,x)) c= (Support f) \/ {a}

proof end;

registration

let L be non empty ZeroStr ;
let x be Element of L;
let f be finite-Support sequence of L;
let a be object ;

cluster f +* (a,x) -> finite-Support for sequence of L;

coherence
for b₁ being sequence of L st b₁ = f +* (a,x) holds
b₁ is finite-Support

proof end;

end;

theorem Th22: :: POLYDIFF:22

for L being non empty ZeroStr
for p being Polynomial of L st p <> 0_. L holds
(len p) -' 1 = (len p) - 1

proof end;

registration

let L be non empty ZeroStr ;
let x be Element of L;

cluster <%x%> -> constant ;

coherence
<%x%> is constant

proof end;

cluster <%x,(0. L)%> -> constant ;

coherence
<%x,(0. L)%> is constant

proof end;

end;

theorem Th23: :: POLYDIFF:23

for L being non empty ZeroStr
for p being constant Polynomial of L holds
( p = 0_. L or p = <%(p . 0)%> )

proof end;

definition

let L be non empty ZeroStr ;
let x be Element of L;
let n be Nat;

func seq (n,x) -> sequence of L equals :: POLYDIFF:def 3
(0_. L) +* (n,x);

coherence
(0_. L) +* (n,x) is sequence of L ;

end;

:: deftheorem defines seq POLYDIFF:def 3 :
for L being non empty ZeroStr
for x being Element of L
for n being Nat holds seq (n,x) = (0_. L) +* (n,x);

registration

let L be non empty ZeroStr ;
let x be Element of L;
let n be Nat;

cluster seq (n,x) -> finite-Support ;

coherence
seq (n,x) is finite-Support ;

end;

theorem Th24: :: POLYDIFF:24

for n being Nat
for L being non empty ZeroStr
for x being Element of L holds (seq (n,x)) . n = x

proof end;

theorem Th25: :: POLYDIFF:25

for m, n being Nat
for L being non empty ZeroStr
for x being Element of L st m <> n holds
(seq (n,x)) . m = 0. L

proof end;

theorem Th26: :: POLYDIFF:26

for n being Nat
for L being non empty ZeroStr
for x being Element of L holds n + 1 is_at_least_length_of seq (n,x)

proof end;

theorem Th27: :: POLYDIFF:27

for n being Nat
for L being non empty ZeroStr
for x being Element of L st x <> 0. L holds
len (seq (n,x)) = n + 1

proof end;

theorem Th28: :: POLYDIFF:28

for n being Nat
for L being non empty ZeroStr holds seq (n,(0. L)) = 0_. L

proof end;

theorem Th29: :: POLYDIFF:29

for n being Nat
for L being non empty right_zeroed addLoopStr
for x, y being Element of L holds (seq (n,x)) + (seq (n,y)) = seq (n,(x + y))

proof end;

theorem Th30: :: POLYDIFF:30

for n being Nat
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for x being Element of L holds - (seq (n,x)) = seq (n,(- x))

proof end;

theorem :: POLYDIFF:31

for n being Nat
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for x, y being Element of L holds (seq (n,x)) - (seq (n,y)) = seq (n,(x - y))

proof end;

definition

let L be non empty ZeroStr ;
let p be sequence of L;
let n be Nat;

func p || n -> sequence of L equals :: POLYDIFF:def 4
p +* (n,(0. L));

coherence
p +* (n,(0. L)) is sequence of L ;

end;

:: deftheorem defines || POLYDIFF:def 4 :
for L being non empty ZeroStr
for p being sequence of L
for n being Nat holds p || n = p +* (n,(0. L));

registration

let L be non empty ZeroStr ;
let p be Polynomial of L;
let n be Nat;

cluster p || n -> finite-Support ;

coherence
p || n is finite-Support ;

end;

theorem Th32: :: POLYDIFF:32

for n being Nat
for L being non empty ZeroStr
for p being sequence of L holds (p || n) . n = 0. L

proof end;

theorem :: POLYDIFF:33

for m, n being Nat
for L being non empty ZeroStr
for p being sequence of L st m <> n holds
(p || n) . m = p . m by FUNCT_7:32;

theorem Th34: :: POLYDIFF:34

for n being Nat
for L being non empty ZeroStr holds (0_. L) || n = 0_. L

proof end;

registration

let L be non empty ZeroStr ;
let n be Nat;

reduce (0_. L) || n to 0_. L;

reducibility
(0_. L) || n = 0_. L by Th34;

end;

theorem :: POLYDIFF:35

for n being Nat
for L being non empty ZeroStr
for p being Polynomial of L st n > (len p) -' 1 holds
p || n = p

proof end;

theorem Th36: :: POLYDIFF:36

for L being non empty ZeroStr
for p being Polynomial of L st p <> 0_. L holds
len (p || ((len p) -' 1)) < len p

proof end;

theorem Th37: :: POLYDIFF:37

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds (p || ((len p) -' 1)) + (Leading-Monomial p) = p

proof end;

registration

let L be non empty ZeroStr ;
let p be constant Polynomial of L;

cluster Leading-Monomial p -> constant ;

coherence
Leading-Monomial p is constant

proof end;

end;

theorem Th38: :: POLYDIFF:38

for n being Nat
for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for x, y being Element of L holds eval ((seq (n,x)),y) = ((seq (n,x)) . n) * (power (y,n))

proof end;

set F = F_Real ;

set z = 0_. F_Real;

set j = 1_. F_Real;

set r0 = In (0,REAL);

theorem Th39: :: POLYDIFF:39

for n being Nat
for r being Element of F_Real holds power (r,n) = r |^ n

proof end;

theorem Th40: :: POLYDIFF:40

for n being Nat holds #Z n = FPower ((1. F_Real),n)

proof end;

theorem Th41: :: POLYDIFF:41

for n being Nat
for r being Element of F_Real holds FPower (r,(n + 1)) = (FPower (r,n)) (#) (id REAL)

proof end;

theorem Th42: :: POLYDIFF:42

for n being Nat
for r being Element of F_Real holds FPower (r,n) is differentiable Function of REAL,REAL

proof end;

theorem Th43: :: POLYDIFF:43

for n being Nat
for r being Element of F_Real holds power (r,n) = (#Z n) . r

proof end;

definition

let p be Polynomial of F_Real;

func poly_diff p -> sequence of F_Real means :Def5: :: POLYDIFF:def 5
for n being Nat holds it . n = (p . (n + 1)) * (n + 1);

existence
ex b₁ being sequence of F_Real st
for n being Nat holds b₁ . n = (p . (n + 1)) * (n + 1)

proof end;

uniqueness
for b₁, b₂ being sequence of F_Real st ( for n being Nat holds b₁ . n = (p . (n + 1)) * (n + 1) ) & ( for n being Nat holds b₂ . n = (p . (n + 1)) * (n + 1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines poly_diff POLYDIFF:def 5 :
for p being Polynomial of F_Real
for b₂ being sequence of F_Real holds
( b₂ = poly_diff p iff for n being Nat holds b₂ . n = (p . (n + 1)) * (n + 1) );

registration

let p be Polynomial of F_Real;

cluster poly_diff p -> finite-Support ;

coherence
poly_diff p is finite-Support

proof end;

end;

theorem Th44: :: POLYDIFF:44

for p being Polynomial of F_Real st p <> 0_. F_Real holds
len (poly_diff p) = (len p) - 1

proof end;

theorem Th45: :: POLYDIFF:45

for p being Polynomial of F_Real st p <> 0_. F_Real holds
len p = (len (poly_diff p)) + 1

proof end;

theorem Th46: :: POLYDIFF:46

for p being constant Polynomial of F_Real holds poly_diff p = 0_. F_Real

proof end;

theorem Th47: :: POLYDIFF:47

for p, q being Polynomial of F_Real holds poly_diff (p + q) = (poly_diff p) + (poly_diff q)

proof end;

theorem Th48: :: POLYDIFF:48

for p being Polynomial of F_Real holds poly_diff (- p) = - (poly_diff p)

proof end;

theorem :: POLYDIFF:49

for p, q being Polynomial of F_Real holds poly_diff (p - q) = (poly_diff p) - (poly_diff q)

proof end;

theorem Th50: :: POLYDIFF:50

for p being Polynomial of F_Real holds poly_diff (Leading-Monomial p) = (0_. F_Real) +* (((len p) -' 2),((p . ((len p) -' 1)) * ((len p) -' 1)))

proof end;

theorem :: POLYDIFF:51

for r, s being Element of F_Real holds poly_diff <%r,s%> = <%s%>

proof end;

definition

let p be Polynomial of F_Real;

func Eval p -> Function of REAL,REAL equals :: POLYDIFF:def 6
Polynomial-Function (F_Real,p);

coherence
Polynomial-Function (F_Real,p) is Function of REAL,REAL ;

end;

:: deftheorem defines Eval POLYDIFF:def 6 :
for p being Polynomial of F_Real holds Eval p = Polynomial-Function (F_Real,p);

registration

let p be Polynomial of F_Real;

cluster Eval p -> differentiable ;

coherence
Eval p is differentiable

proof end;

end;

theorem Th52: :: POLYDIFF:52

Eval (0_. F_Real) = REAL --> 0

proof end;

theorem Th53: :: POLYDIFF:53

for r being Element of F_Real holds Eval <%r%> = REAL --> r

proof end;

Lm2: now :: thesis: for r being Element of F_Real holds (Eval <%r%>) `| = REAL --> 0

let r be Element of F_Real; :: thesis: (Eval <%r%>) `| = REAL --> 0
Eval <%r%> = REAL --> (In (r,REAL)) by Th53;
hence (Eval <%r%>) `| = REAL --> 0 by Th11; :: thesis: verum

end;

theorem Th54: :: POLYDIFF:54

for p being Polynomial of F_Real st p is constant holds
(Eval p) `| = REAL --> 0

proof end;

theorem Th55: :: POLYDIFF:55

for p, q being Polynomial of F_Real holds Eval (p + q) = (Eval p) + (Eval q)

proof end;

theorem Th56: :: POLYDIFF:56

for p being Polynomial of F_Real holds Eval (- p) = - (Eval p)

proof end;

theorem :: POLYDIFF:57

for p, q being Polynomial of F_Real holds Eval (p - q) = (Eval p) - (Eval q)

proof end;

theorem :: POLYDIFF:58

for p being Polynomial of F_Real holds Eval (Leading-Monomial p) = FPower ((p . ((len p) -' 1)),((len p) -' 1))

proof end;

theorem Th59: :: POLYDIFF:59

for p being Polynomial of F_Real holds Eval (Leading-Monomial p) = (p . ((len p) -' 1)) (#) (#Z ((len p) -' 1))

proof end;

theorem Th60: :: POLYDIFF:60

for n being Nat
for r being Element of F_Real holds Eval (seq (n,r)) = r (#) (#Z n)

proof end;

Lm3: for p being Polynomial of F_Real holds (Eval (Leading-Monomial p)) `| = Eval (poly_diff (Leading-Monomial p))

proof end;

theorem Th61: :: POLYDIFF:61

for p being Polynomial of F_Real holds (Eval p) `| = Eval (poly_diff p)

proof end;

registration

let p be Polynomial of F_Real;

cluster (Eval p) `| -> differentiable ;

coherence
(Eval p) `| is differentiable

proof end;

end;