:: Differentiability of Polynomials over Reals
:: by Artur Korni{\l}owicz
::
:: Received February 23, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies LATTICES, VECTSP_1, POLYNOM1, FDIFF_1, PARTFUN1, NUMBERS, REAL_1,
RELAT_1, TARSKI, STRUCT_0, FUNCT_1, SUBSET_1, ALGSEQ_1, NAT_1, XXREAL_0,
SUPINF_2, POLYNOM2, POLYNOM3, POLYNOM5, FUNCSDOM, ARYTM_3, FUNCT_4,
NEWTON, CARD_1, FUNCT_7, MSAFREE2, MESFUNC1, FINSEQ_1, XBOOLE_0,
CALCUL_2, PREPOWER, FUNCOP_1, VALUED_0, HURWITZ, ARYTM_1, AFINSQ_1,
RCOMP_1, REALSET1, POLYNOM4, ORDINAL2, CARD_3, ORDINAL4, GROUP_1,
VALUED_1, XCMPLX_0, SQUARE_1, ALGSTR_0, RLVECT_1, POLYDIFF;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1,
NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NAT_1, NAT_D,
FUNCT_7, NEWTON, PREPOWER, TAYLOR_1, FINSEQ_1, VALUED_0, VALUED_1,
RCOMP_1, FCONT_1, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, GROUP_1,
FUNCSDOM, ALGSEQ_1, POLYNOM1, VFUNCT_1, NORMSP_1, POLYNOM3, POLYNOM4,
POLYNOM5, FDIFF_1, HURWITZ, RATFUNC1;
constructors RELSET_1, FDIFF_1, BINOP_2, POLYNOM4, POLYNOM5, ALGSEQ_1,
RATFUNC1, HURWITZ, FCONT_1, NAT_D, FUNCSDOM, RCOMP_1, PARTFUN2, FUNCT_7,
VFUNCT_1, TAYLOR_1, PREPOWER, NEWTON, ALGSTR_1;
registrations RELSET_1, FUNCT_2, VECTSP_1, STRUCT_0, XBOOLE_0, RELAT_1,
FUNCT_1, NAT_1, XREAL_0, NUMBERS, XCMPLX_0, ORDINAL1, POLYNOM3, MEMBERED,
FUNCOP_1, RATFUNC1, INT_1, POLYNOM5, FINSEQ_1, VALUED_1, VALUED_0,
FDIFF_1, RCOMP_1, FCONT_3, FUNCT_7, POLYNOM4, VFUNCT_1, RLVECT_1,
FINSET_1, MOEBIUS2, XXREAL_0, ALGSTR_1;
requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
definitions TARSKI, FUNCT_1, FUNCT_2, FDIFF_1, ALGSEQ_1, RATFUNC1;
equalities SUBSET_1, STRUCT_0, ALGSTR_0, VECTSP_1, POLYNOM3, HURWITZ,
POLYNOM5, FUNCSDOM, VALUED_1;
expansions FDIFF_1, ALGSEQ_1, FUNCT_1, POLYNOM1;
theorems FUNCT_2, FDIFF_1, POLYNOM5, FUNCOP_1, UPROOTS, FINSEQ_5, ORDINAL1,
XREAL_0, ALGSEQ_1, XXREAL_0, XREAL_1, NAT_1, RATFUNC1, HURWITZ, INT_1,
FINSEQ_1, FINSEQ_3, RLVECT_1, GROUP_1, NORMSP_1, VALUED_1, PARTFUN1,
NAT_D, FVSUM_1, POLYNOM4, VFUNCT_1, FUNCT_7, FUNCSDOM, TAYLOR_1,
PREPOWER, NEWTON, POLYNOM1, ZFMISC_1, HFDIFF_1, RFUNCT_1, POLYNOM2;
schemes FUNCT_2, NAT_1, FINSEQ_1;
begin :: Preliminaries
reserve c for Complex;
reserve r for Real;
reserve m,n for Nat;
reserve f for complex-valued Function;
theorem Th1:
0 + f = f
proof
thus dom(0+f) = dom f by VALUED_1:def 2;
let x be object;
assume x in dom (0+f);
hence (0+f).x = 0+f.x by VALUED_1:def 2
.= f.x;
end;
theorem
f - 0 = f
proof
thus dom(f-0) = dom f by VALUED_1:3;
let x be object;
assume
A1: x in dom (f-0);
dom(f-0) = dom f by VALUED_1:3;
hence (f-0).x = (f.x)-0 by A1,VALUED_1:3
.= f.x;
end;
registration
let f be complex-valued Function;
reduce 0 + f to f;
reducibility by Th1;
reduce f - 0 to f;
reducibility;
end;
theorem Th3:
c + f = ((dom f) --> c) + f
proof
set g = (dom f) --> c;
A2: dom(c+f) = dom f by VALUED_1:def 2;
thus
A3: dom(c+f) = dom g /\ dom f by VALUED_1:def 2
.= dom(g+f) by VALUED_1:def 1;
let x be object;
assume
A4: x in dom(c+f);
then
A5: g.x = c by A2,FUNCOP_1:7;
thus (c+f).x = c+f.x by A4,VALUED_1:def 2
.= (g+f).x by A3,A4,A5,VALUED_1:def 1;
end;
theorem Th4:
f - c = f - ((dom f) --> c)
proof
set g = (dom f) --> c;
A2: dom(f-c) = dom f by VALUED_1:3;
thus
A3: dom(f-c) = dom g /\ dom f by VALUED_1:3
.= dom(f-g) by VALUED_1:12;
let x be object;
assume
A4: x in dom(f-c);
then
A5: g.x = c by A2,FUNCOP_1:7;
thus (f-c).x = f.x-c by A3,A4,VALUED_1:3
.= (f-g).x by A3,A4,A5,VALUED_1:13;
end;
theorem Th5:
c (#) f = ((dom f) --> c) (#) f
proof
set g = (dom f) --> c;
A2: dom(c(#)f) = dom f by VALUED_1:def 5;
thus
A3: dom(c(#)f) = dom g /\ dom f by VALUED_1:def 5
.= dom(g(#)f) by VALUED_1:def 4;
let x be object;
assume
A4: x in dom(c(#)f);
then
A5: g.x = c by A2,FUNCOP_1:7;
thus (c(#)f).x = c*f.x by VALUED_1:6
.= (g(#)f).x by A3,A4,A5,VALUED_1:def 4;
end;
theorem Th6:
f + ((dom f) --> 0) = f
proof
thus f + ((dom f) --> 0) = f+0 by Th3
.= f;
end;
theorem Th7:
f - ((dom f) --> 0) = f
proof
thus f - ((dom f) --> 0) = f-0 by Th4
.= f;
end;
theorem
#Z 0 = REAL --> 1
proof
reconsider s = 1 as Element of REAL by XREAL_0:def 1;
#Z 0 = REAL --> s
proof
let r be Element of REAL;
thus ( #Z 0).r = r #Z 0 by TAYLOR_1:def 1
.= s by PREPOWER:34
.= (REAL --> s).r;
end;
hence thesis;
end;
begin :: Differentiability of real functions
registration
cluster differentiable -> continuous for Function of REAL,REAL;
coherence
proof
let f be Function of REAL,REAL;
assume f is differentiable;
then f is_differentiable_on REAL by FUNCT_2:def 1;
hence thesis by FDIFF_1:25;
end;
end;
definition
let f be differentiable Function of REAL,REAL;
func f`| -> Function of REAL,REAL equals
f `| REAL;
coherence
proof
dom f = REAL by FUNCT_2:def 1;
then f is_differentiable_on REAL by FDIFF_1:def 8;
then dom(f`|REAL) = REAL by FDIFF_1:def 7;
hence thesis by FUNCT_2:67;
end;
end;
theorem Th9:
for f being Function of REAL,REAL holds
f is differentiable iff for r holds f is_differentiable_in r
proof
let f be Function of REAL,REAL;
A1: f|REAL = f;
dom f = REAL by FUNCT_2:def 1;
hence f is differentiable implies
for r holds f is_differentiable_in r by A1,FDIFF_1:def 6,XREAL_0:def 1;
assume for r holds f is_differentiable_in r;
hence f is_differentiable_on dom f;
end;
theorem Th10:
for f being differentiable Function of REAL,REAL holds f`|.r = diff(f,r)
proof
let f be differentiable Function of REAL,REAL;
dom f = REAL by FUNCT_2:def 1;
then
A1: f is_differentiable_on REAL by FDIFF_1:def 8;
r in REAL by XREAL_0:def 1;
hence thesis by A1,FDIFF_1:def 7;
end;
definition
let f be Function of REAL,REAL;
redefine attr f is differentiable means :: redefines differentiable (FDIFF_1, definition)
for r holds f is_differentiable_in r;
compatibility by Th9;
end;
Lm1: [#]REAL is open Subset of REAL;
registration
cluster constant -> differentiable for Function of REAL,REAL;
coherence
proof
let f be Function of REAL,REAL such that
A1: f is constant;
A2: dom f = REAL by FUNCT_2:def 1;
ex r being Element of REAL st rng f = {r} by A1,FUNCT_2:111;
hence thesis by A2,Lm1,FDIFF_1:11;
end;
end;
theorem Th11:
for f being constant Function of REAL,REAL holds
f`| = REAL --> 0
proof
let f be constant Function of REAL,REAL;
reconsider z = 0 as Element of REAL by XREAL_0:def 1;
f`| = REAL --> z
proof
let r be Element of REAL;
A1: f|REAL = f;
dom f = REAL by FUNCT_2:def 1;
hence f`|.r = z by A1,Lm1,FDIFF_1:22
.= (REAL --> z).r;
end;
hence thesis;
end;
registration
cluster id REAL -> differentiable for Function of REAL,REAL;
coherence
proof
let f be Function of REAL,REAL;
assume f = id REAL;
then f is_differentiable_on REAL by Lm1,FDIFF_1:17;
hence thesis by FUNCT_2:def 1;
end;
end;
theorem
(id REAL)`| = REAL --> 1
proof
set f = id REAL;
reconsider z = 1 as Element of REAL by XREAL_0:def 1;
f`| = REAL --> z
proof
let r be Element of REAL;
f|REAL = f;
hence f`|.r = z by Lm1,FDIFF_1:17
.= (REAL --> z).r;
end;
hence thesis;
end;
registration
let n;
cluster #Z n -> differentiable;
coherence
proof
n in NAT by ORDINAL1:def 12;
then #Z n is_differentiable_on REAL by HFDIFF_1:8;
hence thesis by FUNCT_2:def 1;
end;
end;
theorem Th13:
( #Z n) `| = n (#) #Z (n-1)
proof
n in NAT by ORDINAL1:def 12;
hence ( #Z n) `| = (n(#) #Z (n-1)) | [#]REAL by HFDIFF_1:28
.= n(#) #Z (n-1);
end;
reserve f,g for differentiable Function of REAL,REAL;
registration
let f,g;
cluster f + g -> differentiable for Function of REAL,REAL;
coherence
proof
let h be Function of REAL,REAL such that
A1: h = f+g;
let r;
f is_differentiable_in r & g is_differentiable_in r by Th9;
hence thesis by A1,FDIFF_1:13;
end;
cluster f - g -> differentiable for Function of REAL,REAL;
coherence
proof
let h be Function of REAL,REAL such that
A2: h = f-g;
let r;
f is_differentiable_in r & g is_differentiable_in r by Th9;
hence thesis by A2,FDIFF_1:14;
end;
cluster f (#) g -> differentiable for Function of REAL,REAL;
coherence
proof
let h be Function of REAL,REAL such that
A3: h = f(#)g;
let r;
f is_differentiable_in r & g is_differentiable_in r by Th9;
hence thesis by A3,FDIFF_1:16;
end;
end;
registration
let f,r;
cluster r+f -> differentiable for Function of REAL,REAL;
coherence
proof
let h be Function of REAL,REAL;
reconsider r as Element of REAL by XREAL_0:def 1;
reconsider g = REAL --> r as differentiable Function of REAL,REAL;
dom f = REAL by FUNCT_2:def 1;
then g+f = r+f by Th3;
hence thesis;
end;
cluster r(#)f -> differentiable for Function of REAL,REAL;
coherence
proof
let h be Function of REAL,REAL;
reconsider r as Element of REAL by XREAL_0:def 1;
reconsider g = REAL --> r as differentiable Function of REAL,REAL;
dom f = REAL by FUNCT_2:def 1;
then g(#)f = r(#)f by Th5;
hence thesis;
end;
cluster f-r -> differentiable for Function of REAL,REAL;
coherence;
end;
registration
let f;
cluster -f -> differentiable for Function of REAL,REAL;
coherence;
cluster f^2 -> differentiable for Function of REAL,REAL;
coherence;
end;
theorem Th14:
(f+g)`| = f`| + g`|
proof
let s be Element of REAL;
A1: f is_differentiable_in s & g is_differentiable_in s by Th9;
A2: f`|.s = diff(f,s) & g`|.s = diff(g,s) by Th10;
thus (f+g)`|.s = diff(f+g,s) by Th10
.= diff(f,s) + diff(g,s) by A1,FDIFF_1:13
.= (f`| + g`|).s by A2,VALUED_1:1;
end;
theorem Th15:
(f-g)`| = f`| - g`|
proof
let s be Element of REAL;
A1: f is_differentiable_in s & g is_differentiable_in s by Th9;
A2: f`|.s = diff(f,s) & g`|.s = diff(g,s) by Th10;
thus (f-g)`|.s = diff(f-g,s) by Th10
.= diff(f,s) - diff(g,s) by A1,FDIFF_1:14
.= (f`| - g`|).s by A2,VALUED_1:15;
end;
theorem
(f(#)g)`| = g(#)(f`|) + f(#)(g`|)
proof
let s be Element of REAL;
A1: f is_differentiable_in s & g is_differentiable_in s by Th9;
A2: f`|.s = diff(f,s) & g`|.s = diff(g,s) by Th10;
A3: (g.s)*(f`|.s) = (g(#)(f`|)).s & (f.s)*(g`|.s) = (f(#)(g`|)).s
by VALUED_1:5;
thus (f(#)g)`|.s = diff(f(#)g,s) by Th10
.= (g.s)*diff(f,s) + (f.s)*diff(g,s) by A1,FDIFF_1:16
.= (g(#)(f`|) + f(#)(g`|)).s by A2,A3,VALUED_1:1;
end;
theorem
(r+f)`| = f`|
proof
reconsider s = r as Element of REAL by XREAL_0:def 1;
set g = REAL --> s;
A1: g`| = REAL --> 0 by Th11;
A2: dom(f`|) = REAL by FUNCT_2:def 1;
dom f = REAL by FUNCT_2:def 1;
then r+f = g+f by Th3;
hence (r+f)`| = g`|+f`| by Th14
.= f`| by A1,A2,Th6;
end;
theorem
(f-r)`| = f`|
proof
reconsider s = r as Element of REAL by XREAL_0:def 1;
set g = REAL --> s;
A1: g`| = REAL --> 0 by Th11;
A2: dom(f`|) = REAL by FUNCT_2:def 1;
dom f = REAL by FUNCT_2:def 1;
then f-r = f-g by Th4;
hence (f-r)`| = f`|-g`| by Th15
.= f`| by A1,A2,Th7;
end;
theorem Th19:
(r(#)f)`| = r(#)(f`|)
proof
let s be Element of REAL;
A1: f is_differentiable_in s by Th9;
A2: f`|.s = diff(f,s) by Th10;
thus (r(#)f)`|.s = diff(r(#)f,s) by Th10
.= r*diff(f,s) by A1,FDIFF_1:15
.= (r(#)(f`|)).s by A2,VALUED_1:6;
end;
theorem
(-f)`| = -(f`|) by Th19;
begin :: Polynomials
reserve L for non empty ZeroStr;
reserve x for Element of L;
theorem Th21:
for f being (the carrier of L)-valued Function
for a being object holds
Support(f+*(a,x)) c= Support f \/ {a}
proof
let f be (the carrier of L)-valued Function;
let a,z be object;
set g = f+*(a,x);
assume
A1: z in Support(g);
a = z or z in Support f
proof
assume a <> z;
then
A2: g.z = f.z by FUNCT_7:32;
dom g = dom f by FUNCT_7:30;
then z in dom f & g.z <> 0.L by A1,POLYNOM1:def 3;
hence thesis by A2,POLYNOM1:def 3;
end;
hence thesis by ZFMISC_1:136;
end;
registration
let L,x;
let f be finite-Support sequence of L;
let a be object;
cluster f+*(a,x) -> finite-Support for sequence of L;
coherence
proof
let g be sequence of L such that
A1: g = f+*(a,x);
A2: f is finite-Support;
Support g c= Support f \/ {a} by A1,Th21;
hence thesis by A2;
end;
end;
theorem Th22:
for p being Polynomial of L st p <> 0_.L holds len p-'1 = len p-1
proof
let p be Polynomial of L;
assume p <> 0_.L;
then 0 <> len p by POLYNOM4:5;
then 0+1 <= len p by NAT_1:13;
hence thesis by XREAL_1:233;
end;
registration
let L be non empty ZeroStr;
let x be Element of L;
cluster <%x%> -> constant;
coherence
proof
deg <%x%> <= 1-1 by XREAL_1:9,ALGSEQ_1:def 5;
hence deg <%x%> <= 0;
end;
cluster <%x,0.L%> -> constant;
coherence
proof
<%x,0.L%> = <%x%> by POLYNOM5:43;
hence thesis;
end;
end;
theorem Th23:
for L being non empty ZeroStr
for p being constant Polynomial of L holds
p = 0_.L or p = <%p.0%>
proof
let L be non empty ZeroStr;
let p be constant Polynomial of L;
deg p <= 0 by RATFUNC1:def 2;
then len p - 1 + 1 <= 0 + 1 by XREAL_1:6;
hence thesis by ALGSEQ_1:def 5;
end;
definition
let L,x,n;
func seq(n,x) -> sequence of L equals
0_.L+*(n,x);
coherence;
end;
registration
let L,x,n;
cluster seq(n,x) -> finite-Support;
coherence;
end;
theorem Th24:
seq(n,x).n = x
proof
dom(0_.L) = NAT;
hence thesis by ORDINAL1:def 12,FUNCT_7:31;
end;
theorem Th25:
m <> n implies seq(n,x).m = 0.L
proof
assume m <> n;
hence seq(n,x).m = (0_.L).m by FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
theorem Th26:
n+1 is_at_least_length_of seq(n,x)
proof
let i be Nat such that
A1: i >= n+1;
n+0 < n+1 by XREAL_1:8;
hence seq(n,x).i = (0_.L).i by A1,FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
theorem Th27:
x <> 0.L implies len seq(n,x) = n+1
proof
assume
A1: x <> 0.L;
set p = seq(n,x);
for m st m is_at_least_length_of p holds n+1 <= m
proof
let m such that
A2: m is_at_least_length_of p;
p.n = x by Th24;
hence n+1 <= m by A1,A2,NAT_1:13;
end;
hence thesis by Th26,ALGSEQ_1:def 3;
end;
theorem Th28:
seq(n,0.L) = 0_.L
proof
let m be Element of NAT;
per cases;
suppose m = n;
hence seq(n,0.L).m = 0.L by Th24
.= (0_.L).m;
end;
suppose m <> n;
hence seq(n,0.L).m = (0_.L).m by FUNCT_7:32;
end;
end;
theorem Th29:
for L being right_zeroed non empty addLoopStr, x,y being Element of L holds
seq(n,x) + seq(n,y) = seq(n,x+y)
proof
let L be right_zeroed non empty addLoopStr, x,y be Element of L;
let a be Element of NAT;
A1: (seq(n,x) + seq(n,y)).a = seq(n,x).a + seq(n,y).a by NORMSP_1:def 2;
per cases;
suppose a = n;
then seq(n,x).a = x & seq(n,y).a = y & seq(n,x+y).a = x+y by Th24;
hence thesis by NORMSP_1:def 2;
end;
suppose a <> n;
then seq(n,x).a = 0.L & seq(n,y).a = 0.L & seq(n,x+y).a = 0.L by Th25;
hence thesis by A1,RLVECT_1:def 4;
end;
end;
theorem Th30:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for x being Element of L holds
-seq(n,x) = seq(n,-x)
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let x be Element of L;
let a be Element of NAT;
dom(-seq(n,x)) = NAT by FUNCT_2:def 1;
then
A1: (-seq(n,x))/.a = -(seq(n,x))/.a by VFUNCT_1:def 5;
per cases;
suppose a = n;
then seq(n,x).a = x & seq(n,-x).a = -x by Th24;
hence thesis by A1;
end;
suppose a <> n;
then seq(n,x).a = 0.L & seq(n,-x).a = 0.L by Th25;
hence thesis by A1;
end;
end;
theorem
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for x,y being Element of L holds
seq(n,x) - seq(n,y) = seq(n,x-y)
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let x,y be Element of L;
thus seq(n,x) - seq(n,y) = seq(n,x) + seq(n,-y) by Th30
.= seq(n,x-y) by Th29;
end;
definition
let L be non empty ZeroStr;
let p be sequence of L;
let n;
func p||n -> sequence of L equals
p +* (n,0.L);
coherence;
end;
registration
let L be non empty ZeroStr;
let p be Polynomial of L;
let n;
cluster p||n -> finite-Support;
coherence;
end;
theorem Th32:
for L being non empty ZeroStr, p being sequence of L holds
(p||n).n = 0.L
proof
let L be non empty ZeroStr;
let p be sequence of L;
dom p = NAT by FUNCT_2:def 1;
hence thesis by FUNCT_7:31,ORDINAL1:def 12;
end;
theorem
for L being non empty ZeroStr, p being sequence of L holds
m <> n implies (p||n).m = p.m by FUNCT_7:32;
theorem Th34:
for L being non empty ZeroStr holds (0_.L) || n = 0_.L
proof
let L be non empty ZeroStr;
let m be Element of NAT;
m = n or m <> n;
hence thesis by Th32,FUNCT_7:32;
end;
registration
let L be non empty ZeroStr;
let n;
reduce (0_.L) || n to 0_.L;
reducibility by Th34;
end;
theorem
for L being non empty ZeroStr, p being Polynomial of L holds
n > len p-'1 implies p||n = p
proof
let L be non empty ZeroStr, p be Polynomial of L such that
A1: n > len p-'1;
let m be Element of NAT;
per cases;
suppose p = 0_.L;
hence thesis;
end;
suppose that
A2: m = n and
A3: p <> 0_.L;
0 <> len p by A3,POLYNOM4:5;
then 0-1 < len p-1 by XREAL_1:14;
then -1+1 <= len p-1 by INT_1:7;
then len p-'1+1 = len p by NAT_D:72;
then n >= len p by A1,NAT_1:13;
hence p.m = 0.L by A2,ALGSEQ_1:8
.= (p||n).m by A2,Th32;
end;
suppose m <> n;
hence (p||n).m = p.m by FUNCT_7:32;
end;
end;
theorem Th36:
for L being non empty ZeroStr, p being Polynomial of L holds
p <> 0_.L implies len(p||(len p-'1)) < len p
proof
let L be non empty ZeroStr, p be Polynomial of L;
assume
A1: p <> 0_.L;
set m = len p-'1;
A2: m = len p - 1 by A1,Th22;
A3: len p - 1 < len p - 0 by XREAL_1:15;
len p is_at_least_length_of p||m
proof
let i be Nat such that
A4: i >= len p;
thus (p||m).i = p.i by A2,A3,A4,FUNCT_7:32
.= 0.L by A4,ALGSEQ_1:8;
end;
then
A5: len(p||m) <= len p by ALGSEQ_1:def 3;
now
assume len(p||m) = len p;
then
A6: len(p||m) is_at_least_length_of p by ALGSEQ_1:def 3;
m is_at_least_length_of p||m
proof
let i be Nat;
assume
A7: i >= m;
per cases;
suppose
A8: i <> m;
then i > m by A7,XXREAL_0:1;
then i >= len p-1+1 by A2,NAT_1:13;
hence 0.L = p.i by ALGSEQ_1:8
.= (p||m).i by A8,FUNCT_7:32;
end;
suppose i = m;
hence (p||m).i = 0.L by Th32;
end;
end;
then m >= len(p||m) by ALGSEQ_1:def 3;
then
A9: p.m = 0.L by A6;
len p <> 0 by A1,POLYNOM4:5;
hence contradiction by A9,UPROOTS:18;
end;
hence thesis by A5,XXREAL_0:1;
end;
theorem Th37:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr
for p being Polynomial of L holds
p||(len p-'1) + Leading-Monomial p = p
proof
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let p be Polynomial of L;
set l = Leading-Monomial p;
set m = len p-'1;
let n be Element of NAT;
A1: (p||m + l).n = (p||m).n + l.n by NORMSP_1:def 2;
per cases;
suppose
A2: n = m;
(p||m).m = 0.L by Th32;
hence thesis by A1,A2,POLYNOM4:def 1;
end;
suppose
A3: n <> m;
then l.n = 0.L by POLYNOM4:def 1;
hence thesis by A1,A3,FUNCT_7:32;
end;
end;
registration
let L be non empty ZeroStr;
let p be constant Polynomial of L;
cluster Leading-Monomial(p) -> constant;
coherence
proof
deg Leading-Monomial(p) = deg p by POLYNOM4:15;
hence deg Leading-Monomial(p) <= 0 by RATFUNC1:def 2;
end;
end;
theorem Th38:
for L being add-associative right_zeroed right_complementable
distributive unital non empty doubleLoopStr
for x,y being Element of L holds
eval(seq(n,x),y) = seq(n,x).n * power(y,n)
proof
let L be add-associative right_zeroed right_complementable
distributive unital non empty doubleLoopStr;
let x,y be Element of L;
set p = seq(n,x);
consider F being FinSequence of L such that
A1: eval(p,y) = Sum F and
A2: len F = len p and
A3: for n being Element of NAT st n in dom F holds
F.n = p.(n-'1)*(power L).(y,n-'1) by POLYNOM4:def 2;
per cases;
suppose
A4: len p > 0;
then
A5: len p >= 0+1 by NAT_1:13;
then
A6: len p in dom F by A2,FINSEQ_3:25;
p <> 0_.L by A4,POLYNOM4:3;
then x <> 0.L by Th28;
then
A7: len p = n+1 by Th27;
A8: n+1-'1 = n by NAT_D:34;
now
let i be Element of NAT;
assume that
A9: i in dom F and
A10: i <> n+1;
i in Seg len F by A9,FINSEQ_1:def 3;
then i >= 0+1 by FINSEQ_1:1;
then i-'1 = i-1 by XREAL_1:19,XREAL_0:def 2;
then i-'1 <> n by A10;
then
A11: p.(i-'1) = 0.L by Th25;
thus F/.i = F.i by A9,PARTFUN1:def 6
.= 0.L*(power L).(y,i-'1) by A3,A9,A11
.= 0.L;
end;
hence eval(p,y) = F/.(n+1) by A1,A7,A5,A2,FINSEQ_3:25,POLYNOM2:3
.= F.(n+1) by A7,A6,PARTFUN1:def 6
.= p.n*power(y,n) by A3,A7,A5,A8,A2,FINSEQ_3:25;
end;
suppose len p = 0;
then
A12: p = 0_.L by POLYNOM4:5;
then p.n = 0.L by ORDINAL1:def 12,FUNCOP_1:7;
hence thesis by A12,POLYNOM4:17;
end;
end;
begin :: Differentiability of polynomials over reals
reserve p,q for Polynomial of F_Real;
set F = F_Real;
set z = 0_.F;
set j = 1_.F;
set r0 = In(0,REAL);
theorem Th39:
for r being Element of F_Real holds power(r,n) = r|^n
proof
let r be Element of F;
defpred P[Nat] means power(r,$1) = r|^$1;
power(r,0) = 1_F by GROUP_1:def 7;
then
A1: P[0] by NEWTON:4;
A2: now
let n be Nat;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
assume
A3: P[n];
power(r,n+1) = power(r,n1)*r by GROUP_1:def 7
.= r|^(n+1) by A3,NEWTON:6;
hence P[n+1];
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th40:
#Z n = FPower(1.F_Real,n)
proof
reconsider f = FPower(1.F,n) as Function of REAL,REAL;
#Z n = f
proof
let r be Element of REAL;
thus ( #Z n).r = r #Z n by TAYLOR_1:def 1
.= r |^ n by PREPOWER:36
.= 1.F * power(In(r,F),n) by Th39
.= f.r by POLYNOM5:def 12;
end;
hence thesis;
end;
theorem Th41:
for r being Element of F_Real holds
FPower(r,n+1) = FPower(r,n)(#)id(REAL)
proof
let r be Element of F;
reconsider f = FPower(r,n) as Function of REAL,REAL;
reconsider g = f(#)id(REAL) as Function of F,F;
now
let y be Element of F;
reconsider y1 = y as Element of REAL;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
thus g.y = f.y1*id(REAL).y1 by VALUED_1:5
.= r*power(y,n)*y by POLYNOM5:def 12
.= r*((power F).(y,n1)*y)
.= r*power(y,n+1) by GROUP_1:def 7;
end;
hence thesis by POLYNOM5:def 12;
end;
theorem Th42:
for r being Element of F_Real holds
FPower(r,n) is differentiable Function of REAL,REAL
proof
let r be Element of F;
defpred P[Nat] means
FPower(r,$1) is differentiable Function of REAL,REAL;
A1: P[0]
proof
FPower(r,0) = (the carrier of F) --> r by POLYNOM5:66;
hence thesis;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
FPower(r,n+1) = FPower(r,n)(#)id(REAL) by Th41;
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th43:
for r being Element of F_Real holds power(r,n) = ( #Z n).r
proof
let r be Element of F;
thus power(r,n) = 1.F * power(r,n)
.= FPower(1.F,n).r by POLYNOM5:def 12
.= ( #Z n).r by Th40;
end;
definition
let p;
func poly_diff(p) -> sequence of F_Real means :Def5:
for n being Nat holds it.n = p.(n+1) * (n+1);
existence
proof
defpred P[Element of NAT,object] means $2 = p.($1+1) * ($1+1);
A1: for x being Element of NAT ex y being Element of F st P[x,y]
proof
let x be Element of NAT;
p.(x+1) * (x+1) is Element of F by XREAL_0:def 1;
hence thesis;
end;
consider f being Function of NAT,F such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
uniqueness
proof
let f,g be sequence of F_Real such that
A3: for n being Nat holds f.n = p.(n+1) * (n+1) and
A4: for n being Nat holds g.n = p.(n+1) * (n+1);
let n be Element of NAT;
thus f.n = p.(n+1) * (n+1) by A3
.= g.n by A4;
end;
end;
registration
let p;
cluster poly_diff(p) -> finite-Support;
coherence
proof
consider n being Nat such that
A1: for i being Nat st i >= n holds p.i = 0.F by ALGSEQ_1:def 1;
take n;
let i be Nat such that
A2: i >= n;
i+1 >= i+0 by XREAL_1:6;
then p.(i+1) = 0.F by A1,A2,XXREAL_0:2;
hence 0.F = p.(i+1) * (i+1)
.= (poly_diff(p)).i by Def5;
end;
end;
theorem Th44:
p <> 0_.F_Real implies len poly_diff(p) = len p - 1
proof
set x = len p - 1;
set d = poly_diff(p);
assume p <> z;
then
A1: deg p <> -1 by HURWITZ:20;
0-1 <= x by XREAL_1:9;
then -1+1 < x+1 by A1;
then x >= 0 by INT_1:7;
then reconsider x as Element of NAT by INT_1:3;
A2: x is_at_least_length_of d
proof
let i be Nat;
assume i >= x;
then i+1 >= x+1 by XREAL_1:6;
then p.(i+1) = 0.F by ALGSEQ_1:8;
hence 0.F = p.(i+1) * (i+1)
.= d.i by Def5;
end;
for n st n is_at_least_length_of d holds x <= n
proof
let n such that
A3: n is_at_least_length_of d;
per cases;
suppose x = 0;
hence thesis;
end;
suppose x > 0;
then
A4: x >= 0+1 by INT_1:7;
len p = x+1;
then
A5: p.x <> 0.F by ALGSEQ_1:10;
reconsider x1 = x-1 as Element of NAT by A4,NAT_1:21;
A6: d.x1 = p.(x1+1) * (x1+1) by Def5;
assume x > n;
then x >= n+1 by INT_1:7;
then x1 >= n+1-1 by XREAL_1:9;
hence contradiction by A5,A3,A6;
end;
end;
hence thesis by A2,ALGSEQ_1:def 3;
end;
theorem Th45:
p <> 0_.F_Real implies len p = len poly_diff(p) + 1
proof
assume p <> z;
then len poly_diff(p) = len p - 1 by Th44;
hence thesis;
end;
theorem Th46:
for p being constant Polynomial of F_Real holds poly_diff(p) = 0_.F_Real
proof
let p be constant Polynomial of F_Real;
per cases;
suppose
p <> z;
then
A1: len p = len poly_diff(p) + 1 by Th45;
deg p <= 0 by RATFUNC1:def 2;
then len poly_diff(p) = 0 by A1;
then deg poly_diff(p) = -1;
hence thesis by HURWITZ:20;
end;
suppose
A2: p = z;
let n be Element of NAT;
thus z.n = z.(n+1) * (n+1)
.= (poly_diff(p)).n by A2,Def5;
end;
end;
theorem Th47:
poly_diff(p+q) = poly_diff(p) + poly_diff(q)
proof
let n be Element of NAT;
A1: (poly_diff(p)).n = p.(n+1) * (n+1) by Def5;
A2: (poly_diff(q)).n = q.(n+1) * (n+1) by Def5;
A3: (p+q).(n+1) = p.(n+1) + q.(n+1) by NORMSP_1:def 2;
thus (poly_diff(p+q)).n = (p+q).(n+1) * (n+1) by Def5
.= (poly_diff(p)).n + (poly_diff(q)).n by A1,A2,A3
.= (poly_diff(p) + poly_diff(q)).n by NORMSP_1:def 2;
end;
theorem Th48:
poly_diff(-p) = -poly_diff(p)
proof
let n be Element of NAT;
A1: (poly_diff(p)).n = p.(n+1) * (n+1) by Def5;
dom(-p) = NAT by FUNCT_2:def 1;
then
A2: (-p)/.(n+1) = -(p/.(n+1)) by VFUNCT_1:def 5;
A3: dom(-poly_diff(p)) = NAT by FUNCT_2:def 1;
thus (poly_diff(-p)).n = (-p).(n+1) * (n+1) by Def5
.= -((poly_diff(p))/.n) by A1,A2
.= (-poly_diff(p))/.n by A3,VFUNCT_1:def 5
.= (-poly_diff(p)).n;
end;
theorem
poly_diff(p-q) = poly_diff(p) - poly_diff(q)
proof
thus poly_diff(p-q) = poly_diff(p) + poly_diff(-q) by Th47
.= poly_diff(p) - poly_diff(q) by Th48;
end;
theorem Th50:
poly_diff(Leading-Monomial p) =
0_.F_Real +* (len p-'2,(p.(len p-'1))*(len p-'1))
proof
set l = Leading-Monomial(p);
set m = len p-'1;
set k = len p-'2;
reconsider a = (p.m)*m as Element of F by XREAL_0:def 1;
set f = z+*(k,a);
poly_diff(l) = f
proof
let n be Element of NAT;
A1: (poly_diff(l)).n = l.(n+1) * (n+1) by Def5;
A2: dom z = NAT;
per cases by NAT_1:53;
suppose
A3: len p = 0 or len p = 1;
1-1 >= 0;
then
A4: 1-'1 = 0 by XREAL_0:def 2;
1-2 < 0;
then
A5: k = 0 by A3,XREAL_0:def 2;
0-'1 = 0;
then
A6: l.(n+1) = 0.F by A3,A4,POLYNOM4:def 1;
now
per cases;
suppose n = 0;
hence f.n = 0.F by A2,A3,A4,A5,FUNCT_7:31;
end;
suppose n <> 0;
hence f.n = z.n by A5,FUNCT_7:32
.= 0.F;
end;
end;
hence thesis by A1,A6;
end;
suppose
A7: len p > 1;
then
A8: len p - 1 > 1-1 by XREAL_1:14;
per cases;
suppose
A9: m = n+1;
then
A10: l.(n+1) = p.m by POLYNOM4:def 1;
k = m-'1 by NAT_D:45;
then k+1 = n+1 by A9,NAT_D:34;
hence thesis by A1,A2,A9,A10,FUNCT_7:31;
end;
suppose
A11: m <> n+1;
then
A12: l.(n+1) = 0.F by POLYNOM4:def 1;
A13: len p-2 <> n by A8,A11,XREAL_0:def 2;
len p-2 > 1-2 by A7,XREAL_1:14;
then len p-2 >= -1+1 by INT_1:7;
then k = len p-2 by XREAL_0:def 2;
hence f.n = z.n by A13,FUNCT_7:32
.= (poly_diff(l)).n by A1,A12;
end;
end;
end;
hence thesis;
end;
theorem
for r,s being Element of F_Real holds poly_diff(<%r,s%>) = <%s%>
proof
let r,s be Element of F_Real;
let n be Element of NAT;
A1: (poly_diff(<%r,s%>)).n = <%r,s%>.(n+1) * (n+1) by Def5;
per cases;
suppose
A2: n = 0;
hence (poly_diff(<%r,s%>)).n = s by A1,POLYNOM5:38
.= <%s%>.n by A2,POLYNOM5:32;
end;
suppose n <> 0;
then
A3: 0+1 <= n by NAT_1:13;
1+1 <= n+1 by A3,XREAL_1:6;
then <%r,s%>.(n+1) = 0.F by POLYNOM5:38;
hence thesis by A1,A3,POLYNOM5:32;
end;
end;
definition
let p;
func Eval(p) -> Function of REAL,REAL equals
Polynomial-Function(F_Real,p);
coherence;
end;
registration
let p;
cluster Eval(p) -> differentiable;
coherence
proof
set f = Eval(p);
set L = RealVectSpace(REAL);
defpred P[Nat,object] means $2 = FPower(p.($1-'1),$1-'1);
A1: now
let n be Nat;
reconsider x = FPower(p.(n-'1),n-'1) as Element of L by FUNCT_2:9;
assume n in Seg len p;
take x;
thus P[n,x];
end;
consider G being FinSequence of L such that
A2: dom G = Seg len p and
A3: for n being Nat st n in Seg len p holds P[n,G.n] from FINSEQ_1:sch 5(A1);
A4: G|len G = G by FINSEQ_1:58;
reconsider SF = Sum G as Function of REAL,REAL by FUNCT_2:66;
A5: now
let x be Element of REAL;
reconsider x1 = x as Element of F;
consider H being FinSequence of F such that
A6: eval(p,x1) = Sum H and
A7: len H = len p and
A8: for n being Element of NAT st n in dom H holds
H.n = p.(n-'1)*(power F).(x1,n-'1) by POLYNOM4:def 2;
defpred P[Nat] means
for SFk being Function of REAL,REAL st
SFk = Sum (G|$1) holds Sum (H|$1) = SFk.x;
A9: len G = len p by A2,FINSEQ_1:def 3;
A10: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
assume
A11: for SFk being Function of REAL,REAL st SFk = Sum (G|k) holds
Sum (H|k) = SFk.x;
reconsider SFk1 = Sum (G|k) as Function of REAL,REAL by FUNCT_2:66;
let SFk be Function of REAL,REAL;
assume
A12: SFk = Sum (G|(k+1));
per cases;
suppose
A13: len G > k;
reconsider g2 = FPower(p.kk,k) as Function of REAL,REAL;
A14: k+1 >= 1 by NAT_1:11;
A15: k+1 <= len G by A13,NAT_1:13;
then
A16: k+1 in dom G by NAT_1:11,FINSEQ_3:25;
then
A17: G/.(k+1) = G.(k+1) by PARTFUN1:def 6
.= FPower(p.(k+1-'1),k+1-'1) by A2,A3,A14,A15,FINSEQ_3:25
.= FPower(p.kk,k+1-'1) by NAT_D:34
.= FPower(p.kk,k) by NAT_D:34;
G|(k+1) = G|k ^ <*G.(k+1)*> by A13,FINSEQ_5:83
.= G|k ^ <*G/.(k+1)*> by A16,PARTFUN1:def 6;
then
A18: SFk = Sum(G|k) + G/.(k+1) by A12,FVSUM_1:71
.= SFk1+g2 by A17,FUNCSDOM:28;
A19: Sum (H|k) = SFk1.x by A11;
A20: dom G = dom H by A2,A7,FINSEQ_1:def 3;
then
A21: H/.(k+1) = H.(k+1) by A16,PARTFUN1:def 6
.= p.(k+1-'1)*(power F).(x1,k+1-'1) by A8,A20,A16
.= p.kk*(power F).(x1,k+1-'1) by NAT_D:34
.= p.kk*power(x1,k) by NAT_D:34
.= FPower(p.kk,k).x by POLYNOM5:def 12;
H|(k+1) = H|k ^ <*H.(k+1)*> by A7,A9,A13,FINSEQ_5:83
.= H|k ^ <*H/.(k+1)*> by A20,A16,PARTFUN1:def 6;
hence Sum (H|(k+1)) = Sum(H|k) + H/.(k+1) by FVSUM_1:71
.= SFk.x by A21,A18,A19,VALUED_1:1;
end;
suppose
A22: len G <= k;
k <= k+1 by NAT_1:11;
then
A23: G|(k+1) = G & H|(k+1) = H by A7,A9,A22,FINSEQ_1:58,XXREAL_0:2;
G|k = G & H|k = H by A7,A9,A22,FINSEQ_1:58;
hence thesis by A11,A12,A23;
end;
end;
A24: P[0]
proof
let SFk be Function of REAL,REAL;
A25: G|0 = <*>the carrier of L;
assume SFk = Sum (G|0);
then
A26: SFk = 0.L by A25,RLVECT_1:43
.= REAL --> r0;
H|0 = <*>the carrier of F;
hence Sum (H|0) = 0.F by RLVECT_1:43
.= SFk.x by A26;
end;
A27: for k being Nat holds P[k] from NAT_1:sch 2(A24,A10);
A28: Sum(G|len G) = SF by FINSEQ_1:58;
thus f.x = Sum H by A6,POLYNOM5:def 13
.= Sum (H|len H) by FINSEQ_1:58
.= SF.x by A7,A9,A27,A28;
end;
defpred P[Nat] means
for g being PartFunc of REAL,REAL st g = Sum (G|$1) holds
g is differentiable;
A29: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
reconsider g1 = Sum (G|k) as Function of REAL,REAL by FUNCT_2:66;
assume
A30: for g being PartFunc of REAL,REAL st g = Sum (G|k) holds
g is differentiable;
then
A31: g1 is differentiable;
let g be PartFunc of REAL,REAL;
assume
A32: g = Sum (G|(k+1));
per cases;
suppose
A33: len G > k;
k+1 <= len G by A33,NAT_1:13;
then
A34: k+1 in dom G by NAT_1:11,FINSEQ_3:25;
then
A35: G/.(k+1) = G.(k+1) by PARTFUN1:def 6
.= FPower(p.(k+1-'1),k+1-'1) by A2,A3,A34
.= FPower(p.kk,k+1-'1) by NAT_D:34
.= FPower(p.kk,k) by NAT_D:34;
A36: FPower(p.kk,k) is differentiable Function of REAL,REAL by Th42;
G|(k+1) = G|k ^ <*G.(k+1)*> by A33,FINSEQ_5:83
.= G|k ^ <*G/.(k+1)*> by A34,PARTFUN1:def 6;
then g = Sum(G|k) + G/.(k+1) by A32,FVSUM_1:71
.= g1+FPower(p.kk,k) by A35,FUNCSDOM:28;
hence thesis by A31,A36;
end;
suppose
A37: len G <= k;
k <= k+1 by NAT_1:11;
then G|(k+1) = G by A37,FINSEQ_1:58,XXREAL_0:2
.= G|k by A37,FINSEQ_1:58;
hence thesis by A30,A32;
end;
end;
A38: P[0]
proof
let g be PartFunc of REAL,REAL;
A39: G|0 = <*>the carrier of L;
assume g = Sum(G|0);
then g = 0.L by A39,RLVECT_1:43
.= REAL --> r0;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A38,A29);
hence thesis by A4,A5,FUNCT_2:63;
end;
end;
theorem Th52:
Eval(0_.F_Real) = REAL --> 0
proof
Eval(z) = REAL --> r0
proof
let r be Element of REAL;
thus (Eval(z)).r = eval(z,In(r,F)) by POLYNOM5:def 13
.= r0 by POLYNOM4:17
.= (REAL --> r0).r;
end;
hence thesis;
end;
theorem Th53:
for r being Element of F_Real holds Eval(<%r%>) = REAL --> r
proof
let r be Element of F;
Eval(<%r%>) = REAL --> In(r,REAL)
proof
let a be Element of REAL;
thus (Eval(<%r%>)).a = eval(<%r%>,In(a,F)) by POLYNOM5:def 13
.= r by POLYNOM5:37
.= (REAL --> In(r,REAL)).a;
end;
hence thesis;
end;
Lm2: now
let r be Element of F;
Eval(<%r%>) = REAL --> In(r,REAL) by Th53;
hence Eval(<%r%>)`| = REAL --> 0 by Th11;
end;
theorem Th54:
p is constant implies Eval(p)`| = REAL --> 0
proof
assume p is constant;
then p = 0_.F or p = <%p.0%> by Th23;
hence thesis by Th52,Lm2,Th11;
end;
theorem Th55:
Eval(p+q) = Eval(p) + Eval(q)
proof
let r be Element of REAL;
set s = In(r,F);
(Eval(p)).r = eval(p,s) & (Eval(q)).r = eval(q,s) by POLYNOM5:def 13;
hence (Eval(p) + Eval(q)).r = eval(p,s) + eval(q,s) by VALUED_1:1
.= eval(p+q,s) by POLYNOM4:19
.= (Eval(p+q)).r by POLYNOM5:def 13;
end;
theorem Th56:
Eval(-p) = -Eval(p)
proof
let r be Element of REAL;
set s = In(r,F);
(Eval(p)).r = eval(p,s) by POLYNOM5:def 13;
hence (-Eval(p)).r = -eval(p,s) by VALUED_1:8
.= eval(-p,s) by POLYNOM4:20
.= (Eval(-p)).r by POLYNOM5:def 13;
end;
theorem
Eval(p-q) = Eval(p) - Eval(q)
proof
thus Eval(p-q) = Eval(p) + Eval(-q) by Th55
.= Eval(p) - Eval(q) by Th56;
end;
theorem
Eval(Leading-Monomial p) = FPower(p.(len p-'1),len p-'1)
proof
set l = Leading-Monomial p;
set m = len p-'1;
reconsider f = FPower(p.m,m) as Function of REAL,REAL;
Eval(l) = f
proof
let r be Element of REAL;
thus (Eval(l)).r = eval(l,In(r,F)) by POLYNOM5:def 13
.= p.m*power(In(r,F),m) by POLYNOM4:22
.= f.r by POLYNOM5:def 12;
end;
hence thesis;
end;
theorem Th59:
Eval(Leading-Monomial p) = p.(len p-'1) (#) #Z(len p-'1)
proof
set l = Leading-Monomial p;
set m = len p-'1;
set f = p.m (#) #Z(m);
Eval(l) = f
proof
let r be Element of REAL;
A1: power(In(r,F),m) = r |^ m by Th39
.= r #Z m by PREPOWER:36
.= ( #Z m).r by TAYLOR_1:def 1;
thus (Eval(l)).r = eval(l,In(r,F)) by POLYNOM5:def 13
.= p.m * power(In(r,F),m) by POLYNOM4:22
.= f.r by A1,VALUED_1:6;
end;
hence thesis;
end;
theorem Th60:
for r being Element of F_Real holds Eval(seq(n,r)) = r (#) #Z n
proof
let r be Element of F_Real;
let a be Element of REAL;
set p = seq(n,r);
set x = In(a,F);
A1: p.n = r by Th24;
A2: power(x,n) = ( #Z n).a by Th43;
thus (Eval(p)).a = eval(p,x) by POLYNOM5:def 13
.= p.n * power(x,n) by Th38
.= (r (#) #Z n).a by A1,A2,VALUED_1:6;
end;
Lm3:
Eval(Leading-Monomial p)`| = Eval(poly_diff(Leading-Monomial p))
proof
set l = Leading-Monomial(p);
set m = len p-'1;
set k = len p-'2;
reconsider f = FPower(p.m,m) as Function of REAL,REAL;
reconsider a = (p.m)*m as Element of F by XREAL_0:def 1;
A1: poly_diff(l) = seq(k,a) by Th50;
A2: ( #Z m)`| = m (#) #Z (m-1) by Th13;
len p <= 2-1 or len p >= 2 by INT_1:52;
then per cases by NAT_1:25;
suppose len p = 0 or len p = 1;
then
A3: p = z or p = <%p.0%> by ALGSEQ_1:def 5;
then poly_diff(l) = z by Th46;
hence thesis by A3,Th52,Th54;
end;
suppose
A4: 2 <= len p;
then
A5: len p-'2 = len p - 2 by XREAL_1:233;
len p-'1 = len p - 1 by A4,XXREAL_0:2,XREAL_1:233;
then
A6: a (#) #Z (m-1) = Eval(seq(k,a)) by A5,Th60;
Eval(l) = p.m (#) #Z m by Th59;
hence Eval(l)`| = p.m (#) (( #Z m)`|) by Th19
.= Eval(poly_diff(l)) by A1,A2,A6,RFUNCT_1:17;
end;
end;
theorem Th61:
(Eval(p))`| = Eval(poly_diff(p))
proof
set f = Eval(p)`|;
set g = Eval(poly_diff(p));
defpred P[Nat] means
for p st len p <= $1 holds Eval(p)`| = Eval(poly_diff(p));
A1: P[0]
proof
let p;
assume len p <= 0;
then len p = 0;
then
A2: p = z by POLYNOM4:5;
poly_diff(z) = z by Th46;
hence thesis by A2,Th52,Th54;
end;
A3: P[n] implies P[n+1]
proof
assume that
A4: P[n];
let p such that
A5: len p <= n+1;
set m = len p-'1;
set q = p||m;
now
per cases;
suppose p <> z;
hence len q < n+1 by A5,Th36,XXREAL_0:2;
end;
suppose p = z;
hence len q < n+1 by POLYNOM4:3;
end;
end;
then
A6: Eval(q)`| = Eval(poly_diff(q)) by A4,NAT_1:13;
set l = Leading-Monomial(p);
A7: q + l = p by Th37;
A8: poly_diff(q+l) = poly_diff(q)+poly_diff(l) by Th47;
A9: Eval(l)`| = Eval(poly_diff(l)) by Lm3;
A10: Eval(poly_diff(q)+poly_diff(l)) = Eval(poly_diff(q)) + Eval(poly_diff(l))
by Th55;
Eval(q+l) = Eval(q)+Eval(l) by Th55;
hence thesis by A6,A7,A8,A9,A10,Th14;
end;
A11: P[n] from NAT_1:sch 2(A1,A3);
len p = len p;
hence thesis by A11;
end;
registration
let p;
cluster (Eval p)`| -> differentiable;
coherence
proof
(Eval p)`| = Eval(poly_diff p) by Th61;
hence thesis;
end;
end;