:: 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 b1 being Function of REAL,REAL st b1 is differentiable holds
b1 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 b1 being Function of REAL,REAL st b1 is constant holds
b1 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 b1 being Function of REAL,REAL st b1 = id REAL holds
b1 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 b1 being Function of REAL,REAL st b1 = f + g holds
b1 is differentiable
proof end;
cluster f - g -> differentiable for Function of REAL,REAL;
coherence
for b1 being Function of REAL,REAL st b1 = f - g holds
b1 is differentiable
proof end;
cluster f (#) g -> differentiable for Function of REAL,REAL;
coherence
for b1 being Function of REAL,REAL st b1 = f (#) g holds
b1 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 b1 being Function of REAL,REAL st b1 = r + f holds
b1 is differentiable
proof end;
cluster r (#) f -> differentiable for Function of REAL,REAL;
coherence
for b1 being Function of REAL,REAL st b1 = r (#) f holds
b1 is differentiable
proof end;
cluster f - r -> differentiable for Function of REAL,REAL;
coherence
for b1 being Function of REAL,REAL st b1 = f - r holds
b1 is differentiable
;
end;

registration
let f be differentiable Function of REAL,REAL;
cluster - f -> differentiable for Function of REAL,REAL;
coherence
for b1 being Function of REAL,REAL st b1 = - f holds
b1 is differentiable
;
cluster f ^2 -> differentiable for Function of REAL,REAL;
coherence
for b1 being Function of REAL,REAL st b1 = f ^2 holds
b1 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 b1 -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 b1 being sequence of L st b1 = f +* (a,x) holds
b1 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 b1 being sequence of F_Real st
for n being Nat holds b1 . n = (p . (n + 1)) * (n + 1)
proof end;
uniqueness
for b1, b2 being sequence of F_Real st ( for n being Nat holds b1 . n = (p . (n + 1)) * (n + 1) ) & ( for n being Nat holds b2 . n = (p . (n + 1)) * (n + 1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines poly_diff POLYDIFF:def 5 :
for p being Polynomial of F_Real
for b2 being sequence of F_Real holds
( b2 = poly_diff p iff for n being Nat holds b2 . 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;