0.F;
thus f is total;
A1: dom f = REAL by FUNCOP_1:13;
now
let h;
now let n be Nat;
A2: rng h c= dom f by A1;
A3: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(f/*h)).n = (h").n*((f/*h).n) by NDIFF_1:def 2
.= (h").n*(f.(h.n)) by A3,A2,FUNCT_2:108
.= 0.F by FUNCOP_1:7,RLVECT_1:10;
end;
then (h")(#)(f/*h) is constant & ((h")(#)(f/*h)).0 = 0.F by
VALUED_0:def 18;
hence (h")(#)(f/*h) is convergent & lim ((h")(#)(f/*h))
= 0.F by NDIFF_1:18;
end;
hence thesis;
end;
end;
definition let F;
mode RestFunc of F is RestFunc-like PartFunc of REAL,the carrier of F;
end;
definition let F;
let IT be Function of REAL,the carrier of F;
attr IT is linear means :Def2:
ex r be Point of F st for p be Real holds IT/.p = p*r;
end;
registration let F;
cluster linear for Function of REAL,the carrier of F;
existence
proof
deffunc FG(Real) = $1*(0.F);
consider f be Function of REAL, the carrier of F such that
A1: for x being Element of REAL holds f.x = FG(x) from FUNCT_2:sch 4;
A2: for x being Real holds f/.x = FG(x)
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
f/.x = FG(x) by A1;
hence thesis;
end;
take f;
thus thesis by A2;
end;
end;
definition let F;
mode LinearFunc of F is linear Function of REAL,the carrier of F;
end;
reserve R,R1,R2 for RestFunc of F;
reserve L,L1,L2 for LinearFunc of F;
theorem Th3:
L1+L2 is LinearFunc of F & L1-L2 is LinearFunc of F
proof
consider g1 be Point of F such that
A1: for p be Real holds L1/.p = p*g1 by Def2;
consider g2 be Point of F such that
A2: for p be Real holds L2/.p = p*g2 by Def2;
A3: L1+L2 is total by VFUNCT_1:32;
now
let p be Real;
reconsider pp=p as Element of REAL by XREAL_0:def 1;
thus (L1+L2)/.p = L1/.pp + L2/.pp by VFUNCT_1:37
.= p*g1 + L2/.pp by A1
.= p*g1 + p*g2 by A2
.= p*(g1+g2) by RLVECT_1:def 5;
end;
hence L1+L2 is LinearFunc of F by A3,Def2;
A4: L1-L2 is total by VFUNCT_1:32;
now
let p be Real;
reconsider pp=p as Element of REAL by XREAL_0:def 1;
thus (L1-L2)/.p = L1/.pp - L2/.pp by VFUNCT_1:37
.= p*g1 - L2/.pp by A1
.= p*g1 - p*g2 by A2
.= p*(g1-g2) by RLVECT_1:34;
end;
hence thesis by A4,Def2;
end;
theorem Th4:
r(#)L is LinearFunc of F
proof
consider g be Point of F such that
A1: for p be Real holds L/.p = p*g by Def2;
A2: r(#)L is total by VFUNCT_1:34;
now
let p be Real;
reconsider pp=p as Element of REAL by XREAL_0:def 1;
thus (r(#)L)/.p = r*L/.pp by VFUNCT_1:39
.= r*(p*g) by A1
.= (r*p)*g by RLVECT_1:def 7
.= p*(r*g) by RLVECT_1:def 7;
end;
hence thesis by A2,Def2;
end;
theorem Th5:
for h1,h2 be PartFunc of REAL, the carrier of F
for seq be Real_Sequence st rng seq c= dom h1 /\ dom h2 holds
(h1+h2)/*seq = h1/*seq+h2/*seq & (h1-h2)/*seq=h1/*seq - h2/*seq
proof
let h1,h2 be PartFunc of REAL,the carrier of F;
let seq be Real_Sequence;
A1: dom h1 /\ dom h2 c= dom h1 by XBOOLE_1:17;
A2: dom h1 /\ dom h2 c= dom h2 by XBOOLE_1:17;
assume
A3: rng seq c= dom h1 /\ dom h2; then
A4: rng seq c= dom (h1 + h2) by VFUNCT_1:def 1;
now let n be Nat;
A5: n in NAT by ORDINAL1:def 12;
A6:seq.n in rng seq by FUNCT_2:4,A5;
thus ((h1+h2)/*seq).n = (h1+h2)/.(seq.n) by A4,FUNCT_2:109,A5
.= h1/.(seq.n) + h2/.(seq.n) by A4,A6,VFUNCT_1:def 1
.= (h1/*seq).n + h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A5
.= (h1/*seq).n + (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A5;
end;
hence (h1+h2)/*seq=h1/*seq+h2/*seq by NORMSP_1:def 2;
A7: rng seq c= dom (h1 - h2) by A3,VFUNCT_1:def 2;
now
let n be Nat;
A8: n in NAT by ORDINAL1:def 12;
A9:seq.n in rng seq by FUNCT_2:4,A8;
thus ((h1-h2)/*seq).n = (h1-h2)/.(seq.n) by A7,FUNCT_2:109,A8
.= h1/.(seq.n) - h2/.(seq.n) by A7,A9,VFUNCT_1:def 2
.= (h1/*seq).n - h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A8
.= (h1/*seq).n - (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A8;
end;
hence thesis by NORMSP_1:def 3;
end;
theorem Th6:
for h1,h2 be PartFunc of REAL,the carrier of F
for seq be Real_Sequence st h1 is total & h2 is total holds
(h1+h2)/*seq = h1/*seq + h2/*seq & (h1-h2)/*seq = h1/*seq - h2/*seq
proof
let h1,h2 be PartFunc of REAL,the carrier of F;
let seq be Real_Sequence;
assume h1 is total & h2 is total;
then h1+h2 is total by VFUNCT_1:32;
then dom (h1+h2) = REAL by PARTFUN1:def 2;
then dom h1 /\ dom h2 = REAL by VFUNCT_1:def 1;then
A1: rng seq c= dom h1 /\ dom h2;
hence (h1+h2)/*seq = h1/*seq + h2/*seq by Th5;
thus thesis by A1,Th5;
end;
theorem Th7:
R1+R2 is RestFunc of F & R1-R2 is RestFunc of F
proof
A1: R1 is total & R2 is total by Def1;
A2: now
let h;
A3: (h")(#)((R1+R2)/*h) = (h")(#)((R1/*h)+(R2/*h)) by A1,Th6
.= ((h")(#)(R1/*h))+((h")(#)(R2/*h)) by NDIFF_1:9;
A4: (h")(#)(R1/*h) is convergent & (h")(#)(R2/*h) is convergent by Def1;
hence (h")(#)((R1+R2)/*h) is convergent by A3,NORMSP_1:19;
lim ((h")(#)(R1/*h)) = 0.F & lim ((h")(#)(R2/*h)) = 0.F by Def1;
hence lim ((h")(#)((R1+R2)/*h)) = 0.F+0.F by A4,A3,NORMSP_1:25
.= 0.F by RLVECT_1:def 4;
end;
R1+R2 is total by A1,VFUNCT_1:32;
hence R1+R2 is RestFunc of F by A2,Def1;
A5: now let h;
A6: (h")(#)((R1-R2)/*h) = (h")(#)((R1/*h)-(R2/*h)) by A1,Th6
.= ((h")(#)(R1/*h))-((h")(#)(R2/*h)) by NDIFF_1:12;
A7: (h")(#)(R1/*h) is convergent & (h")(#)(R2/*h) is convergent by Def1;
hence (h")(#)((R1-R2)/*h) is convergent by A6,NORMSP_1:20;
lim ((h")(#)(R1/*h)) = 0.F & lim ((h")(#)(R2/*h)) = 0.F by Def1;
hence lim ((h")(#)((R1-R2)/*h)) = 0.F-0.F by A7,A6,NORMSP_1:26
.= 0.F by RLVECT_1:13;
end;
R1-R2 is total by A1,VFUNCT_1:32;
hence R1-R2 is RestFunc of F by A5,Def1;
end;
theorem Th8:
r(#)R is RestFunc of F
proof
A1: R is total by Def1; then
A2:r(#)R is total by VFUNCT_1:34;
now let h;
dom R = REAL by A1,FUNCT_2:def 1; then
rng h c= dom R; then
A3: (h")(#)((r(#)R)/*h) = (h")(#)(r*(R/*h)) by NFCONT_3:4
.= r*((h")(#)(R/*h)) by NDIFF_1:10;
A4: (h")(#)(R/*h) is convergent by Def1;
hence (h")(#)((r(#)R)/*h) is convergent by A3,NORMSP_1:22;
lim ((h")(#)(R/*h)) = 0.F by Def1;
hence lim ((h")(#)((r(#)R)/*h)) = r*0.F by A4,A3,NORMSP_1:28
.= 0.F by RLVECT_1:10;
end;
hence thesis by A2,Def1;
end;
definition let F,f;
let x0 be Real;
pred f is_differentiable_in x0 means
ex N being Neighbourhood of x0
st N c= dom f & ex L,R st for x st x in N
holds f/.x - f/.x0 = L/.(x-x0) + R/.(x-x0);
end;
definition
let F,f;
let x0 be Real;
assume
A1: f is_differentiable_in x0;
func diff(f,x0) -> Point of F means
:Def4:
ex N being Neighbourhood of x0 st N c= dom f & ex L,R st it=L/.1
& for x st x in N holds f/.x-f/.x0 = L/.(x-x0) + R/.(x-x0);
existence
proof
consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: ex L,R st for x st x in N
holds f/.x - f/.x0 = L/.(x-x0) + R/.(x-x0) by A1;
consider L,R such that
A4: for x st x in N holds f/.x - f/.x0 = L/.(x-x0) + R/.(x-x0) by A3;
consider r be Point of F such that
A5: for p be Real holds L/.p = p*r by Def2;
take r;
L/.1=1*r by A5
.=r by RLVECT_1:def 8;
hence thesis by A2,A4;
end;
uniqueness
proof
let r,s be Point of F;
assume that
A6: ex N being Neighbourhood of x0 st N c= dom f & ex L,R st r=L/.1 &
for x be Real st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) and
A7: ex N being Neighbourhood of x0 st N c= dom f & ex L,R st s=L/.1 &
for x be Real st x in N holds f/.x-f/.x0 = L/.(x-x0) + R/.(x-x0);
consider N being Neighbourhood of x0 such that
N c= dom f and
A8: ex L,R st r=L/.1 & for x be Real
st x in N holds f/.x-f/.x0 = L/.(x-x0)+R/.(x-x0) by A6;
consider L,R such that
A9: r=L/.1 and
A10: for x be Real
st x in N holds f/.x-f/.x0 = L/.(x-x0) + R/.(x-x0) by A8;
consider r1 be Point of F such that
A11: for p be Real holds L/.p = p*r1 by Def2;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A12: ex L,R st s=L/.1 & for x be Real st x in N1
holds f/.x-f/.x0=L/.(x-x0)+R/.(x-x0) by A7;
consider L1,R1 such that
A13: s =L1/.1 and
A14: for x be Real st x in N1
holds f/.x-f/.x0 = L1/.(x-x0) + R1/.(x-x0) by A12;
consider p1 be Point of F such that
A15: for p be Real holds L1/.p = p*p1 by Def2;
consider N0 be Neighbourhood of x0 such that
A16: N0 c= N & N0 c= N1 by RCOMP_1:17;
consider g be Real such that
A17: 0