:: by Artur Korni{\l}owicz

::

:: Received February 23, 2017

:: Copyright (c) 2017 Association of Mizar Users

registration
end;

registration

for b_{1} being Function of REAL,REAL st b_{1} is differentiable holds

b_{1} is continuous
end;

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

coherence for b

b

proof end;

definition

let f be differentiable Function of REAL,REAL;

coherence

f `| REAL is Function of REAL,REAL

end;
coherence

f `| REAL is Function of REAL,REAL

proof end;

:: deftheorem defines `| POLYDIFF:def 1 :

for f being differentiable Function of REAL,REAL holds f `| = f `| REAL;

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 )

( f is differentiable iff for r being Real holds f is_differentiable_in r )

proof end;

definition

let f be Function of REAL,REAL;

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

end;
redefine attr f is differentiable means :: POLYDIFF:def 2

for r being Real holds f is_differentiable_in r;

compatibility for r being Real holds f is_differentiable_in r;

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

:: 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 );

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

for b_{1} being Function of REAL,REAL st b_{1} is constant holds

b_{1} is differentiable
end;

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

coherence for b

b

proof end;

registration

coherence

for b_{1} being Function of REAL,REAL st b_{1} = id REAL holds

b_{1} is differentiable

end;
for b

b

proof end;

registration
end;

registration

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

coherence

for b_{1} being Function of REAL,REAL st b_{1} = f + g holds

b_{1} is differentiable

for b_{1} being Function of REAL,REAL st b_{1} = f - g holds

b_{1} is differentiable

for b_{1} being Function of REAL,REAL st b_{1} = f (#) g holds

b_{1} is differentiable

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

registration

let f be differentiable Function of REAL,REAL;

let r be Real;

coherence

for b_{1} being Function of REAL,REAL st b_{1} = r + f holds

b_{1} is differentiable

for b_{1} being Function of REAL,REAL st b_{1} = r (#) f holds

b_{1} is differentiable

for b_{1} being Function of REAL,REAL st b_{1} = f - r holds

b_{1} is differentiable
;

end;
let r be Real;

coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

registration

let f be differentiable Function of REAL,REAL;

coherence

for b_{1} being Function of REAL,REAL st b_{1} = - f holds

b_{1} is differentiable
;

coherence

for b_{1} being Function of REAL,REAL st b_{1} = f ^2 holds

b_{1} is differentiable
;

end;
coherence

for b

b

coherence

for b

b

theorem :: POLYDIFF:16

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

proof end;

theorem :: POLYDIFF:20

theorem Th21: :: POLYDIFF:21

for L being non empty ZeroStr

for x being Element of L

for f being the carrier of b_{1} -valued Function

for a being object holds Support (f +* (a,x)) c= (Support f) \/ {a}

for x being Element of L

for f being the carrier of b

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 ;

coherence

for b_{1} being sequence of L st b_{1} = f +* (a,x) holds

b_{1} is finite-Support

end;
let x be Element of L;

let f be finite-Support sequence of L;

let a be object ;

coherence

for b

b

proof 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

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;

coherence

<%x%> is constant

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

end;
let x be Element of L;

coherence

<%x%> is constant

proof end;

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

proof 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)%> )

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;

coherence

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

end;
let x be Element of L;

let n be Nat;

coherence

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

:: 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);

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;

coherence

seq (n,x) is finite-Support ;

end;
let x be Element of L;

let n be Nat;

coherence

seq (n,x) is finite-Support ;

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

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)

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

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 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))

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))

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))

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;

coherence

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

end;
let p be sequence of L;

let n be Nat;

coherence

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

:: 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));

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;

coherence

p || n is finite-Support ;

end;
let p be Polynomial of L;

let n be Nat;

coherence

p || n is finite-Support ;

theorem :: POLYDIFF:33

registration
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

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

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

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;

coherence

Leading-Monomial p is constant

end;
let p be constant Polynomial of L;

coherence

Leading-Monomial p is constant

proof 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))

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 Th41: :: POLYDIFF:41

for n being Nat

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

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

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

proof end;

definition

let p be Polynomial of F_Real;

ex b_{1} being sequence of F_Real st

for n being Nat holds b_{1} . n = (p . (n + 1)) * (n + 1)

for b_{1}, b_{2} being sequence of F_Real st ( for n being Nat holds b_{1} . n = (p . (n + 1)) * (n + 1) ) & ( for n being Nat holds b_{2} . n = (p . (n + 1)) * (n + 1) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = (p . (n + 1)) * (n + 1);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines poly_diff POLYDIFF:def 5 :

for p being Polynomial of F_Real

for b_{2} being sequence of F_Real holds

( b_{2} = poly_diff p iff for n being Nat holds b_{2} . n = (p . (n + 1)) * (n + 1) );

for p being Polynomial of F_Real

for b

( b

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;

definition
end;

:: deftheorem defines Eval POLYDIFF:def 6 :

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

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

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;
Eval <%r%> = REAL --> (In (r,REAL)) by Th53;

hence (Eval <%r%>) `| = REAL --> 0 by Th11; :: thesis: verum

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;

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

proof end;