:: Real Function Differentiability
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-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 NUMBERS, REAL_1, SUBSET_1, RCOMP_1, SEQ_1, PARTFUN1, VALUED_0,
SEQ_2, ORDINAL2, CARD_1, ARYTM_3, FUNCT_1, RELAT_1, FUNCOP_1, VALUED_1,
FUNCT_2, NAT_1, TARSKI, ARYTM_1, XXREAL_1, XBOOLE_0, XXREAL_0, COMPLEX1,
FCONT_1, XXREAL_2, FDIFF_1, FUNCT_7, ASYMPT_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1,
SEQ_1, COMSEQ_2, SEQ_2, RELSET_1, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1,
XXREAL_0;
constructors PARTFUN1, REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, RCOMP_1,
PARTFUN2, RFUNCT_2, FCONT_1, VALUED_1, REALSET1, FINSET_1, SETFAM_1,
RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, NUMBERS;
registrations FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED,
RCOMP_1, VALUED_0, VALUED_1, FUNCT_2, FUNCOP_1, SEQ_4, RELAT_1, SEQ_1,
SEQ_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FCONT_1, XBOOLE_0, ORDINAL1;
equalities XBOOLE_0, VALUED_1, RCOMP_1, SUBSET_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, RCOMP_1;
theorems TARSKI, NAT_1, FUNCT_1, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SEQM_3,
SEQ_4, PARTFUN1, PARTFUN2, RFUNCT_1, RFUNCT_2, RCOMP_1, FCONT_1, FUNCT_2,
RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, FUNCOP_1,
XREAL_1, COMPLEX1, VALUED_1, VALUED_0, ORDINAL1;
schemes SEQ_1;
begin
reserve y for object, X for set;
reserve x,x0,x1,x2,g,g1,g2,r,r1,s,p,p1 for Real;
reserve n,m,k for Element of NAT;
reserve Y for Subset of REAL;
reserve Z for open Subset of REAL;
reserve s1,s3 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL,REAL;
theorem Th1:
(for r holds r in Y iff r in REAL) iff Y = REAL
proof
thus (for r holds r in Y iff r in REAL) implies Y=REAL
proof
assume for r holds r in Y iff r in REAL;
then for y being object holds y in Y iff y in REAL;
hence thesis by TARSKI:2;
end;
assume
A1: Y=REAL;
let r;
thus r in Y implies r in REAL;
thus thesis by A1;
end;
definition let x be Real;
let IT be Real_Sequence;
attr IT is x-convergent means :Def1:
IT is convergent & lim IT = x;
end;
registration
cluster 0-convergent non-zero for Real_Sequence;
existence
proof
deffunc F(Nat) = 1/($1+1);
consider s1 such that
A1: for n being Nat holds s1.n=F(n) from SEQ_1:sch 1;
take s1;
now
let n be Nat;
(n+1)" <> 0;
then 1/(n+1) <> 0 by XCMPLX_1:215;
hence s1.n <> 0 by A1;
end; then
A2: s1 is non-zero by SEQ_1:5;
lim s1 = 0 & s1 is convergent by A1,SEQ_4:31; then
s1 is 0-convergent;
hence thesis by A2;
end;
end;
registration let f be 0-convergent Real_Sequence;
cluster lim f -> zero;
coherence by Def1;
end;
registration
cluster 0-convergent -> convergent for Real_Sequence;
coherence;
end;
set cs = seq_const 0;
reserve h for non-zero 0-convergent Real_Sequence;
reserve c for constant Real_Sequence;
definition
let IT be PartFunc of REAL,REAL;
attr IT is RestFunc-like means :Def2:
IT is total & for h holds (h")(#)(IT/*h) is convergent &
lim ((h")(#)(IT/*h)) = 0;
end;
registration
cluster RestFunc-like for PartFunc of REAL,REAL;
existence
proof
reconsider cf = REAL --> In(0,REAL) as Function of REAL, REAL;
take f = cf;
thus f is total;
now
let h;
now
let n be Nat;
A2: rng h c= dom f;
A4: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(f/*h)).n = (h").n*((f/*h).n) by SEQ_1:8
.= (h").n*(f.(h.n)) by A4,A2,FUNCT_2:108
.= (h").n*0
.= In(0,REAL);
end;
then (h")(#)(f/*h) is constant & ((h")(#)(f/*h)).0 = 0
by VALUED_0:def 18;
hence (h")(#)(f/*h) is convergent & lim ((h")(#)(f/*h)) = 0 by SEQ_4:25;
end;
hence thesis;
end;
end;
definition
mode RestFunc is RestFunc-like PartFunc of REAL,REAL;
end;
definition
let IT be PartFunc of REAL,REAL;
attr IT is linear means :Def3:
IT is total & ex r st for p holds IT.p = r*p;
end;
registration
cluster linear for PartFunc of REAL,REAL;
existence
proof
deffunc F(Real) = In(1*$1,REAL);
defpred P[set] means $1 in REAL;
consider f such that
A1: (for r being Element of REAL holds r in dom f iff P[r]) &
for r being Element of REAL st r in dom f holds f.r= F(r)
from SEQ_1:sch 3;
take f;
for y being object holds y in REAL implies y in dom f by A1;
then REAL c= dom f;
then dom f = REAL;
hence f is total by PARTFUN1:def 2;
for p holds f.p = 1*p
proof let p;
In(1*p,REAL) = 1*p;
hence thesis by A1;
end;
hence thesis;
end;
end;
definition
mode LinearFunc is linear PartFunc of REAL,REAL;
end;
reserve R,R1,R2 for RestFunc;
reserve L,L1,L2 for LinearFunc;
theorem Th2:
L1+L2 is LinearFunc & L1-L2 is LinearFunc
proof
consider g1 such that
A1: for p holds L1.p = g1*p by Def3;
consider g2 such that
A2: for p holds L2.p = g2*p by Def3;
A3: L1 is total & L2 is total by Def3;
now
let p;
reconsider pp=p as Element of REAL by XREAL_0:def 1;
thus (L1+L2).p = L1.pp + L2.pp by A3,RFUNCT_1:56
.= g1*p + L2.p by A1
.= g1*p + g2*p by A2
.= (g1+g2)*p;
end;
hence L1+L2 is LinearFunc by A3,Def3;
now
let p;
reconsider pp=p as Element of REAL by XREAL_0:def 1;
thus (L1-L2).p = L1.pp - L2.pp by A3,RFUNCT_1:56
.= g1*p - L2.p by A1
.= g1*p - g2*p by A2
.= (g1-g2)*p;
end;
hence thesis by A3,Def3;
end;
theorem Th3:
r(#)L is LinearFunc
proof
consider g such that
A1: for p holds L.p = g*p by Def3;
A2: L is total by Def3;
now
let p;
reconsider pp = p as Element of REAL by XREAL_0:def 1;
thus (r(#)L).p = r*L.pp by A2,RFUNCT_1:57
.= r*(g*p) by A1
.= r*g*p;
end;
hence thesis by A2,Def3;
end;
theorem Th4:
R1+R2 is RestFunc & R1-R2 is RestFunc & R1(#)R2 is RestFunc
proof
A1: R1 is total & R2 is total by Def2;
now
let h;
A2: (h")(#)((R1+R2)/*h) = (h")(#)((R1/*h)+(R2/*h)) by A1,RFUNCT_2:13
.= ((h")(#)(R1/*h))+((h")(#)(R2/*h)) by SEQ_1:16;
A3: (h")(#)(R1/*h) is convergent & (h")(#)(R2/*h) is convergent by Def2;
hence (h")(#)((R1+R2)/*h) is convergent by A2;
lim ((h")(#)(R1/*h)) = 0 & lim ((h")(#)(R2/*h)) = 0 by Def2;
hence lim ((h")(#)((R1+R2)/*h)) = 0+0 by A3,A2,SEQ_2:6
.= 0;
end;
hence R1+R2 is RestFunc by A1,Def2;
now
let h;
A4: (h")(#)((R1-R2)/*h) = (h")(#)((R1/*h)-(R2/*h)) by A1,RFUNCT_2:13
.= ((h")(#)(R1/*h))-((h")(#)(R2/*h)) by SEQ_1:21;
A5: (h")(#)(R1/*h) is convergent & (h")(#)(R2/*h) is convergent by Def2;
hence (h")(#)((R1-R2)/*h) is convergent by A4;
lim ((h")(#)(R1/*h)) = 0 & lim ((h")(#)(R2/*h)) = 0 by Def2;
hence lim ((h")(#)((R1-R2)/*h)) = 0-0 by A5,A4,SEQ_2:12
.= 0;
end;
hence R1-R2 is RestFunc by A1,Def2;
now
let h;
A6: (h")(#)(R2/*h) is convergent by Def2;
A7: h" is non-zero by SEQ_1:33;
A8: (h")(#)(R1/*h) is convergent & h is convergent by Def2;
then
A9: h(#)((h")(#)(R1/*h)) is convergent;
lim ((h")(#)(R1/*h)) = 0 & lim h = 0 by Def2;
then
A10: lim (h(#)((h")(#)(R1/*h))) = 0*0 by A8,SEQ_2:15
.= 0;
A11: (h")(#)((R1(#)R2)/*h) = ((R1/*h)(#)(R2/*h))/"h by A1,RFUNCT_2:13
.= ((R1/*h)(#)(R2/*h)(#)(h"))/"(h(#)(h")) by A7,SEQ_1:43
.= ((R1/*h)(#)(R2/*h)(#)(h"))(#)((h"")(#)(h")) by SEQ_1:36
.= h(#)(h")(#)((R1/*h)(#)((h")(#)(R2/*h))) by SEQ_1:14
.= h(#)(h")(#)(R1/*h)(#)((h")(#)(R2/*h)) by SEQ_1:14
.= h(#)((h")(#)(R1/*h))(#)((h")(#)(R2/*h)) by SEQ_1:14;
hence (h")(#)((R1(#)R2)/*h) is convergent by A6,A9;
lim ((h")(#)(R2/*h)) = 0 by Def2;
hence lim ((h")(#)((R1(#)R2)/*h)) = 0*0 by A6,A9,A10,A11,SEQ_2:15
.= 0;
end;
hence thesis by A1,Def2;
end;
theorem Th5:
r(#)R is RestFunc
proof
A1: R is total by Def2;
now
let h;
A2: (h")(#)((r(#)R)/*h) = (h")(#)(r(#)(R/*h)) by A1,RFUNCT_2:14
.= r(#)((h")(#)(R/*h)) by SEQ_1:19;
A3: (h")(#)(R/*h) is convergent by Def2;
hence (h")(#)((r(#)R)/*h) is convergent by A2;
lim ((h")(#)(R/*h)) = 0 by Def2;
hence lim ((h")(#)((r(#)R)/*h)) = r*0 by A3,A2,SEQ_2:8
.= 0;
end;
hence thesis by A1,Def2;
end;
theorem Th6:
L1(#)L2 is RestFunc-like
proof
consider x1 such that
A1: for p holds L1.p=x1*p by Def3;
A2: L1 is total & L2 is total by Def3;
hence L1(#)L2 is total;
consider x2 such that
A3: for p holds L2.p=x2*p by Def3;
now
let h;
now
let n;
A4: h.n<>0 by SEQ_1:5;
thus ((h")(#)((L1(#)L2)/*h)).n=(h").n *((L1(#)L2)/*h).n by SEQ_1:8
.=(h").n*(L1(#)L2).(h.n) by A2,FUNCT_2:115
.=(h").n*(L1.(h.n)*L2.(h.n)) by A2,RFUNCT_1:56
.=(h").n*L1.(h.n)*L2.(h.n)
.=((h.n)")*L1.(h.n)*L2.(h.n) by VALUED_1:10
.=((h.n)")*((h.n)*x1)*L2.(h.n) by A1
.=((h.n)")*(h.n)*x1*L2.(h.n)
.=1*x1*L2.(h.n) by A4,XCMPLX_0:def 7
.=x1*(x2*(h.n)) by A3
.=x1*x2*(h.n)
.=((x1*x2)(#)h).n by SEQ_1:9;
end;
then
A5: (h")(#)((L1(#)L2)/*h)=(x1*x2)(#)h by FUNCT_2:63;
thus (h")(#)((L1(#)L2)/*h) is convergent by A5;
lim h=0;
hence lim ((h")(#)((L1(#)L2)/*h)) = (x1*x2)*0 by A5,SEQ_2:8
.=0;
end;
hence thesis;
end;
theorem Th7:
R(#)L is RestFunc & L(#)R is RestFunc
proof
A1: L is total by Def3;
consider x1 such that
A2: for p holds L.p=x1*p by Def3;
A3: R is total by Def2;
A4: now
let h;
A5: (h")(#)(R/*h) is convergent by Def2;
now
let n;
thus (L/*h).n=L.(h.n) by A1,FUNCT_2:115
.=x1*(h.n) by A2
.=(x1(#)h).n by SEQ_1:9;
end;
then
A6: (L/*h)=x1(#)h by FUNCT_2:63;
A7: L/*h is convergent by A6;
lim h=0;
then
A8: lim (L/*h)=x1*0 by A6,SEQ_2:8
.=0;
A9: (h")(#)((R(#)L)/*h)=(h")(#)((R/*h)(#)(L/*h)) by A3,A1,RFUNCT_2:13
.=((h")(#)(R/*h))(#)(L/*h) by SEQ_1:14;
hence (h")(#)((R(#)L)/*h) is convergent by A7,A5;
lim ((h")(#)(R/*h))=0 by Def2;
hence lim ((h")(#)((R(#)L)/*h))=0*0 by A9,A7,A8,A5,SEQ_2:15
.=0;
end;
hence R(#)L is RestFunc by A3,A1,Def2;
thus thesis by A3,A1,A4,Def2;
end;
definition
let 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;
let x0 be Real;
assume
A1: f is_differentiable_in x0;
func diff(f,x0) -> Real means
:Def5:
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 such that
A5: for p holds L.p = r*p by Def3;
take r;
L.1=r*1 by A5
.=r;
hence thesis by A2,A4;
end;
uniqueness
proof
let r,s be Real;
assume that
A6: ex N being Neighbourhood of x0 st N c= dom f & ex L,R st r=L.1 &
for x 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 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 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 st x in N holds f.x-f.x0 = L.(x-x0) + R.(x-x0) by A8;
consider r1 such that
A11: for p holds L.p = r1*p by Def3;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A12: ex L,R st s=L.1 & for x 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 st x in N1 holds f.x-f.x0 = L1.(x-x0) + R1.(x-x0) by A12;
consider p1 such that
A15: for p holds L1.p = p1*p by Def3;
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<g and
A18: N0 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A19: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now
let n be Nat;
0<>g/(n+2) by A17,XREAL_1:139;
hence 0<>s1.n by A19;
end;
then
A20: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A19,SEQ_4:31; then
s1 is 0-convergent;
then reconsider h = s1 as non-zero 0-convergent Real_Sequence
by A20;
A21: for n ex x st x in N & x in N1 & h.n=x-x0
proof
let n;
take x0+g/(n+2);
0+1<n+1+1 by XREAL_1:6;
then g/(n+2)<g/1 by A17,XREAL_1:76;
then
A22: x0 + g/(n+2)<x0 + g by XREAL_1:6;
0<g/(n+2) by A17,XREAL_1:139;
then x0+-g<x0+g/(n+2) by A17,XREAL_1:6;
then x0+g/(n+2) in ].x0-g,x0+g.[ by A22;
hence thesis by A16,A18,A19;
end;
A23: s=p1*1 by A13,A15;
A24: r=r1*1 by A9,A11;
A25: now
let x;
assume that
A26: x in N and
A27: x in N1;
f.x-f.x0 = L.(x-x0) + R.(x-x0) by A10,A26;
then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14,A27;
then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A11;
hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A24,A23;
end;
reconsider rs = r - s as Element of REAL by XREAL_0:def 1;
now
R1 is total by Def2;
then dom R1 = REAL by PARTFUN1:def 2;
then
A28: rng h c= dom R1;
let n be Nat;
R is total by Def2;
then dom R = REAL by PARTFUN1:def 2;
then
A29: rng h c= dom R;
A30: n in NAT by ORDINAL1:def 12;
then ex x st x in N & x in N1 & h.n=x-x0 by A21;
then r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A25;
then
A31: (r*(h.n))/(h.n)+(R.(h.n))/(h.n)=(s*(h.n)+R1.(h.n))/(h.n) by XCMPLX_1:62;
A32: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A30,A29,FUNCT_2:108
.= ((h")(#)(R/*h)).n by SEQ_1:8;
A33: h.n <> 0 by SEQ_1:5;
A34: (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A30,A28,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by SEQ_1:8;
A35: (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A33,XCMPLX_1:60
.= s;
(r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
then r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A31,A35,XCMPLX_1:62;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A32,A34;
hence rs = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
end;
then
((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant & (((h")(#)(R1/*h))-((h"
)(#)(R /*h))).1 = rs by VALUED_0:def 18;
then
A36: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by SEQ_4:25;
A37: (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by Def2;
(h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by Def2;
then r-s = 0-0 by A36,A37,SEQ_2:12;
hence thesis;
end;
end;
definition
let f,X;
pred f is_differentiable_on X means
X c= dom f & for x st x in X holds f|X is_differentiable_in x;
end;
theorem Th8:
f is_differentiable_on X implies X is Subset of REAL
by XBOOLE_1:1;
theorem Th9:
f is_differentiable_on Z iff Z c= dom f & for x st x in Z holds
f is_differentiable_in x
proof
thus f is_differentiable_on Z implies Z c=dom f & for x st x in Z holds f
is_differentiable_in x
proof
assume
A1: f is_differentiable_on Z;
hence Z c=dom f;
let x0;
assume
A2: x0 in Z;
then f|Z is_differentiable_in x0 by A1;
then consider N being Neighbourhood of x0 such that
A3: N c= dom(f|Z) and
A4: ex L,R st for x st x in N holds (f|Z).x-(f|Z).x0=L.(x-x0)+R.(x-x0);
take N;
dom(f|Z)=dom f/\Z by RELAT_1:61;
then dom(f|Z) c=dom f by XBOOLE_1:17;
hence N c= dom f by A3;
consider L,R such that
A5: for x st x in N holds (f|Z).x - (f|Z).x0 = L.(x-x0) + R.(x-x0) by A4;
take L,R;
let x;
assume
A6: x in N;
then (f|Z).x-(f|Z).x0=L.(x-x0)+R.(x-x0) by A5;
then f.x-(f|Z).x0=L.(x-x0)+R.(x-x0) by A3,A6,FUNCT_1:47;
hence thesis by A2,FUNCT_1:49;
end;
assume that
A7: Z c=dom f and
A8: for x st x in Z holds f is_differentiable_in x;
thus Z c=dom f by A7;
let x0;
assume
A9: x0 in Z;
then consider N1 being Neighbourhood of x0 such that
A10: N1 c= Z by RCOMP_1:18;
f is_differentiable_in x0 by A8,A9;
then consider N being Neighbourhood of x0 such that
A11: N c= dom f and
A12: ex L,R st for x st x in N holds f.x-f.x0=L.(x-x0)+R.(x-x0);
consider N2 being Neighbourhood of x0 such that
A13: N2 c= N1 and
A14: N2 c= N by RCOMP_1:17;
A15: N2 c= Z by A10,A13;
take N2;
N2 c= dom f by A11,A14;
then N2 c= dom f/\Z by A15,XBOOLE_1:19;
hence
A16: N2 c= dom(f|Z) by RELAT_1:61;
consider L,R such that
A17: for x st x in N holds f.x-f.x0=L.(x-x0)+R.(x-x0) by A12;
A18: x0 in N2 by RCOMP_1:16;
take L,R;
let x;
assume
A19: x in N2;
then f.x-f.x0=L.(x-x0)+R.(x-x0) by A14,A17;
then (f|Z).x-f.x0=L.(x-x0)+R.(x-x0) by A16,A19,FUNCT_1:47;
hence thesis by A16,A18,FUNCT_1:47;
end;
theorem
f is_differentiable_on Y implies Y is open
proof
assume
A1: f is_differentiable_on Y;
now
let x0 be Element of REAL;
assume x0 in Y;
then f|Y is_differentiable_in x0 by A1;
then consider N being Neighbourhood of x0 such that
A2: N c= dom(f|Y) and
ex L,R st for x st x in N holds (f|Y).x-(f|Y).x0=L.(x-x0)+R.(x-x0);
take N;
thus N c= Y by A2,XBOOLE_1:1;
end;
hence thesis by RCOMP_1:20;
end;
definition
let f,X;
assume
A1: f is_differentiable_on X;
func f`|X -> PartFunc of REAL,REAL means
:Def7:
dom it = X & for x st x in X holds it.x = diff(f,x);
existence
proof
deffunc F(Real) = In(diff(f,$1),REAL);
defpred P[set] means $1 in X;
consider F being PartFunc of REAL,REAL such that
A2: (for x being Element of REAL holds x in dom F iff P[x]) &
for x being Element of REAL st x in dom F holds F.x = F(x)
from SEQ_1:sch 3;
take F;
now
A3: X is Subset of REAL by A1,Th8;
let y be object;
assume y in X;
hence y in dom F by A2,A3;
end;
then
A4: X c= dom F;
for y being object st y in dom F holds y in X by A2;
then dom F c= X;
hence dom F = X by A4;
for x st x in X holds F.x = diff(f,x)
proof let x;
reconsider x as Element of REAL by XREAL_0:def 1;
x in X implies F.x = F(x) by A2;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let F,G be PartFunc of REAL,REAL;
assume that
A5: dom F = X and
A6: for x st x in X holds F.x = diff(f,x) and
A7: dom G = X and
A8: for x st x in X holds G.x = diff(f,x);
now
let x be Element of REAL;
assume
A9: x in dom F;
then F.x = diff(f,x) by A5,A6;
hence F.x=G.x by A5,A8,A9;
end;
hence thesis by A5,A7,PARTFUN1:5;
end;
end;
theorem
(Z c= dom f & ex r st rng f = {r}) implies f is_differentiable_on Z &
for x st x in Z holds (f`|Z).x = 0
proof
reconsider cf = REAL --> In(0,REAL) as Function of REAL, REAL;
set R=cf;
now
let h;
A2: now
let n be Nat;
A4: rng h c= dom R;
A5: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by SEQ_1:8
.= (h".n)*(R.(h.n)) by A5,A4,FUNCT_2:108
.= (h".n)*0
.= 0;
end;
then
A6: (h")(#)(R/*h) is constant by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent;
((h")(#)(R/*h)).0 = 0 by A2;
hence lim ((h")(#)(R/*h)) = 0 by A6,SEQ_4:25;
end;
then reconsider R as RestFunc by Def2;
set L = cf;
for p holds L.p = 0*p;
then reconsider L as LinearFunc by Def3;
assume
A7: Z c= dom f;
given r such that
A8: rng f = {r};
A9: now
let x0;
assume x0 in dom f;
then f.x0 in {r} by A8,FUNCT_1:def 3;
hence f.x0 = r by TARSKI:def 1;
end;
A10: now
let x0;
assume
A11: x0 in Z;
then consider N being Neighbourhood of x0 such that
A12: N c= Z by RCOMP_1:18;
A13: N c= dom f by A7,A12;
for x st x in N holds f.x - f.x0 = L.(x-x0) + R.(x-x0)
proof
let x;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x in N;
hence f.x - f.x0 = r - f.x0 by A9,A13
.= r - r by A7,A9,A11
.= L.(xx-xx0)+0
.= L.(x-x0)+R.(x-x0);
end;
hence f is_differentiable_in x0 by A13;
end;
hence
A14: f is_differentiable_on Z by A7,Th9;
let x0;
assume
A15: x0 in Z;
then
A16: f is_differentiable_in x0 by A10;
then 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);
then consider N being Neighbourhood of x0 such that
A17: N c= dom f;
A18: for x st x in N holds f.x - f.x0 = L.(x-x0) + R.(x-x0)
proof
let x;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x in N;
hence f.x - f.x0 = r - f.x0 by A9,A17
.=r - r by A7,A9,A15
.=L.(xx-xx0) + 0
.=L.(x-x0) + R.(x-x0);
end;
reconsider j =1 as Element of REAL by XREAL_0:def 1;
thus (f`|Z).x0 = diff(f,x0) by A14,A15,Def7
.= L.j by A16,A17,A18,Def5
.=0;
end;
registration
let h be non-zero Real_Sequence; let n be Nat;
cluster h^\n -> non-zero for Real_Sequence;
coherence
proof let hh be Real_Sequence such that
A1: hh = h^\n;
rng hh c= rng h by A1,NAT_1:55;
hence not 0 in rng hh;
end;
end;
registration
let h; let n be Nat;
cluster h^\n -> non-zero 0-convergent for Real_Sequence;
coherence
proof
lim h = 0;
then lim (h^\n) = 0 by SEQ_4:20; then
h^\n is 0-convergent;
hence thesis;
end;
end;
theorem Th12:
for x0 being Real for N being Neighbourhood of x0 st f
is_differentiable_in x0 & N c= dom f holds for h,c st rng c = {x0} & rng (h+c)
c= N holds h"(#)(f/*(h+c) - f/*c) is convergent & diff(f,x0) = lim (h"(#)(f/*(h
+c) - f/*c))
proof
let x0 be Real;
let N be Neighbourhood of x0;
assume that
A1: f is_differentiable_in x0 and
A2: N c= dom f;
consider N1 be Neighbourhood of x0 such that
N1 c= dom f and
A3: ex L,R st for x st x in N1 holds f.x - f.x0 = L.(x-x0) + R.(x-x0) by A1;
consider N2 be Neighbourhood of x0 such that
A4: N2 c= N and
A5: N2 c= N1 by RCOMP_1:17;
A6: N2 c= dom f by A2,A4;
let h,c such that
A7: rng c = {x0} and
A8: rng (h+c) c= N;
consider g be Real such that
A9: 0<g and
A10: N2 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
x0 + 0 < x0 + g & x0 - g < x0 - 0 by A9,XREAL_1:8,15;
then
A11: x0 in N2 by A10;
A12: rng c c= dom f
proof
let y be object;
assume y in rng c;
then y = x0 by A7,TARSKI:def 1;
then y in N by A4,A11;
hence thesis by A2;
end;
ex n st rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2
proof
x0 in rng c by A7,TARSKI:def 1;
then
A13: lim c = x0 by SEQ_4:25;
lim h = 0;
then lim (h + c) = 0 + x0 by A13,SEQ_2:6
.= x0;
then consider n being Nat such that
A14: for m being Nat st n<=m holds |.(h+c).m-x0.|<g by A9,
SEQ_2:def 7;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
A15: rng (c^\n) = {x0} by A7,VALUED_0:26;
thus rng (c^\n) c= N2
by A11,A15,TARSKI:def 1;
let y be object;
assume y in rng ((h+c)^\n);
then consider m such that
A16: y = ((h+c)^\n).m by FUNCT_2:113;
n + 0 <= n+m by XREAL_1:7;
then
A17: |.(h+c).(n+m)-x0.|<g by A14;
then (h+c).(m+n) - x0 < g by SEQ_2:1;
then ((h+c)^\n).m - x0 < g by NAT_1:def 3;
then
A18: ((h+c)^\n).m < x0 + g by XREAL_1:19;
-g < (h+c).(m+n) - x0 by A17,SEQ_2:1;
then -g < ((h+c)^\n).m - x0 by NAT_1:def 3;
then x0 +-g < ((h+c)^\n).m by XREAL_1:20;
hence thesis by A10,A16,A18;
end;
then consider n such that
rng (c^\n) c= N2 and
A19: rng ((h+c)^\n) c= N2;
consider L,R such that
A20: for x st x in N1 holds f.x - f.x0 = L.(x-x0) + R.(x-x0) by A3;
A21: rng (c^\n) c= dom f
proof
let y be object;
assume
A22: y in rng (c^\n);
rng (c^\n) = rng c by VALUED_0:26;
then y = x0 by A7,A22,TARSKI:def 1;
then y in N by A4,A11;
hence thesis by A2;
end;
A23: L is total by Def3;
A24: (L/*(h^\n) + R/*(h^\n))(#)(h^\n)" is convergent & lim ((L/*(h^\n) + R/*
(h^\n))(#)(h^\n)") = L.1
proof
deffunc F(Nat) = L.1 + ((R/*(h^\n))(#)(h^\n)").$1;
consider s1 such that
A25: for k being Nat holds s1.k = F(k) from SEQ_1:sch 1;
A26: now
A27: ((h^\n)")(#)(R/*(h^\n)) is convergent & lim (((h^\n)")(#) (R/*(h^\n
)))=0 by Def2;
let r be Real;
assume 0<r;
then consider m being Nat such that
A28: for k being Nat st m<=k holds |.(((h^\n)")(#) (R/*(h^\n))).k - 0 .|<r
by A27,
SEQ_2:def 7;
take n1=m;
let k being Nat such that
A29: n1<=k;
|.s1.k-L.1.| = |.L.1 + ((R/*(h^\n))(#)(h^\n)").k - L.1 .| by A25
.= |.(((h^\n)")(#)(R/*(h^\n))).k - 0 .|;
hence |.s1.k-L.1.|<r by A28,A29;
end;
consider s such that
A30: for p1 holds L.p1=s*p1 by Def3;
A31: L.1 = s*1 by A30
.= s;
now
let m;
A32: (h^\n).m <> 0 by SEQ_1:5;
thus ((L/*(h^\n) + R/*(h^\n))(#)(h^\n)").m = ((L/*(h^\n) + R/*(h^\n)).m)
*((h^\n)").m by SEQ_1:8
.= ((L/*(h^\n)).m + (R/*(h^\n)).m) *((h^\n)").m by SEQ_1:7
.= ((L/*(h^\n)).m)*((h^\n)").m+((R/*(h^\n)).m)*((h^\n)").m
.= ((L/*(h^\n)).m)*((h^\n)").m + ((R/*(h^\n))(#)(h^\n)").m by SEQ_1:8
.= ((L/*(h^\n)).m)*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by
VALUED_1:10
.= (L.((h^\n).m))*((h^\n).m)" + ((R/*(h^\n))(#) (h^\n)").m by A23,
FUNCT_2:115
.= (s*((h^\n).m))*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by A30
.= s*(((h^\n).m)*((h^\n).m)") + ((R/*(h^\n))(#)(h^\n)").m
.= s*1 + ((R/*(h^\n))(#)(h^\n)").m by A32,XCMPLX_0:def 7
.= s1.m by A25,A31;
end;
then
A33: (L/*(h^\n) + R/*(h^\n))(#)(h^\n)" = s1 by FUNCT_2:63;
hence (L/*(h^\n) + R/*(h^\n))(#)(h^\n)" is convergent by A26,SEQ_2:def 6;
hence thesis by A33,A26,SEQ_2:def 7;
end;
A34: rng ((h+c)^\n) c= dom f
by A19,A4,A2;
A35: rng (h+c) c= dom f
by A8,A2;
A36: for k holds f.(((h+c)^\n).k) - f.((c^\n).k) = L.((h^\n).k) + R.((h^\n). k)
proof
let k;
((h+c)^\n).k in rng ((h+c)^\n) by VALUED_0:28;
then
A37: ((h+c)^\n).k in N2 by A19;
(c^\n).k in rng (c^\n) & rng (c^\n) = rng c by VALUED_0:26,28;
then
A38: (c^\n).k = x0 by A7,TARSKI:def 1;
((h+c)^\n).k - (c^\n).k = (h^\n + c^\n).k - (c^\n).k by SEQM_3:15
.= (h^\n).k + (c^\n).k - (c^\n).k by SEQ_1:7
.= (h^\n).k;
hence thesis by A20,A5,A37,A38;
end;
A39: R is total by Def2;
now
let k;
thus (f/*((h+c)^\n)-f/*(c^\n)).k = (f/*((h+c)^\n)).k-(f/*(c^\n)).k by
RFUNCT_2:1
.= f.(((h+c)^\n).k) - (f/*(c^\n)).k by A34,FUNCT_2:108
.= f.(((h+c)^\n).k) - f.((c^\n).k) by A21,FUNCT_2:108
.= L.((h^\n).k) + R.((h^\n).k) by A36
.= (L/*(h^\n)).k + R.((h^\n).k) by A23,FUNCT_2:115
.= (L/*(h^\n)).k + (R/*(h^\n)).k by A39,FUNCT_2:115
.= (L/*(h^\n) + R/*(h^\n)).k by SEQ_1:7;
end;
then f/*((h+c)^\n) - f/*(c^\n) = L/*(h^\n) + R/*(h^\n) by FUNCT_2:63;
then
A40: ((L/*(h^\n) + R/*(h^\n))(#)(h^\n)") = ((((f/*(h+c))^\n)-f/*(c^\n))(#) (
h^\n)") by A35,VALUED_0:27
.=((((f/*(h+c))^\n)-((f/*c)^\n))(#)(h^\n)") by A12,VALUED_0:27
.=((((f/*(h+c))-(f/*c))^\n)(#)(h^\n)") by SEQM_3:17
.=((((f/*(h+c))-(f/*c))^\n)(#)((h")^\n)) by SEQM_3:18
.=((((f/*(h+c))-(f/*c))(#) h")^\n) by SEQM_3:19;
then
A41: L.1 = lim ((h")(#)((f/*(h+c)) - (f/*c))) by A24,SEQ_4:22;
thus h" (#) (f/*(h+c) - f/*c) is convergent by A24,A40,SEQ_4:21;
for x st x in N2 holds f.x - f.x0 = L.(x-x0) + R.(x-x0) by A20,A5;
hence thesis by A1,A6,A41,Def5;
end;
theorem Th13:
f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies
f1+f2 is_differentiable_in x0 & diff(f1+f2,x0)=diff(f1,x0)+diff(f2,x0)
proof
reconsider j =1 as Element of REAL by XREAL_0:def 1;
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0;
consider N1 be Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L,R st for x st x in N1 holds f1.x - f1.x0 = L.(x-x0) + R.(x-x0)
by A1;
consider L1,R1 such that
A5: for x st x in N1 holds f1.x - f1.x0 = L1.(x-x0) + R1.(x-x0) by A4;
consider N2 be Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L,R st for x st x in N2 holds f2.x - f2.x0 = L.(x-x0) + R.(x-x0)
by A2;
consider L2,R2 such that
A8: for x st x in N2 holds f2.x - f2.x0 = L2.(x-x0) + R2.(x-x0) by A7;
reconsider R=R1+R2 as RestFunc by Th4;
reconsider L=L1+L2 as LinearFunc by Th2;
A9: L1 is total & L2 is total by Def3;
consider N be Neighbourhood of x0 such that
A10: N c= N1 and
A11: N c= N2 by RCOMP_1:17;
A12: N c= dom f2 by A6,A11;
N c= dom f1 by A3,A10;
then N /\ N c= dom f1 /\ dom f2 by A12,XBOOLE_1:27;
then
A13: N c= dom (f1+f2) by VALUED_1:def 1;
A14: R1 is total & R2 is total by Def2;
A15: now
let x;
A16: x0 in N by RCOMP_1:16;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume
A17: x in N;
hence (f1+f2).x - (f1+f2).x0 = (f1.x+f2.x) - (f1+f2).x0 by A13,
VALUED_1:def 1
.=f1.x+f2.x - (f1.x0+f2.x0) by A13,A16,VALUED_1:def 1
.=(f1.x - f1.x0) + (f2.x - f2.x0)
.=L1.(x-x0)+R1.(x-x0) + (f2.x - f2.x0) by A5,A10,A17
.=L1.(x-x0)+R1.(x-x0) + (L2.(x-x0) + R2.(x-x0)) by A8,A11,A17
.=(L1.(x-x0)+L2.(x-x0)) + (R1.(x-x0) + R2.(x-x0))
.=L.(x-x0)+(R1.(xx-xx0) + R2.(xx-xx0)) by A9,RFUNCT_1:56
.=L.(x-x0)+R.(x-x0) by A14,RFUNCT_1:56;
end;
hence f1+f2 is_differentiable_in x0 by A13;
hence diff(f1+f2,x0)=L.1 by A13,A15,Def5
.=L1.j + L2.j by A9,RFUNCT_1:56
.=diff(f1,x0) + L2.1 by A1,A3,A5,Def5
.=diff(f1,x0) + diff(f2,x0) by A2,A6,A8,Def5;
end;
theorem Th14:
f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies
f1-f2 is_differentiable_in x0 & diff(f1-f2,x0)=diff(f1,x0)-diff(f2,x0)
proof
reconsider j =1 as Element of REAL by XREAL_0:def 1;
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0;
consider N1 be Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L,R st for x st x in N1 holds f1.x - f1.x0 = L.(x-x0) + R.(x-x0)
by A1;
consider L1,R1 such that
A5: for x st x in N1 holds f1.x - f1.x0 = L1.(x-x0) + R1.(x-x0) by A4;
consider N2 be Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L,R st for x st x in N2 holds f2.x - f2.x0 = L.(x-x0) + R.(x-x0)
by A2;
consider L2,R2 such that
A8: for x st x in N2 holds f2.x - f2.x0 = L2.(x-x0) + R2.(x-x0) by A7;
reconsider R=R1-R2 as RestFunc by Th4;
reconsider L=L1-L2 as LinearFunc by Th2;
A9: L1 is total & L2 is total by Def3;
consider N be Neighbourhood of x0 such that
A10: N c= N1 and
A11: N c= N2 by RCOMP_1:17;
A12: N c= dom f2 by A6,A11;
N c= dom f1 by A3,A10;
then N /\ N c= dom f1 /\ dom f2 by A12,XBOOLE_1:27;
then
A13: N c= dom (f1-f2) by VALUED_1:12;
A14: R1 is total & R2 is total by Def2;
A15: now
let x;
A16: x0 in N by RCOMP_1:16;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume
A17: x in N;
hence (f1-f2).x - (f1-f2).x0 = (f1.x-f2.x) - (f1-f2).x0 by A13,VALUED_1:13
.=f1.x - f2.x - (f1.x0-f2.x0) by A13,A16,VALUED_1:13
.=f1.x - f1.x0 - (f2.x - f2.x0)
.=L1.(x-x0) + R1.(x-x0) - (f2.x - f2.x0) by A5,A10,A17
.=L1.(x-x0) + R1.(x-x0) - (L2.(x-x0) + R2.(x-x0)) by A8,A11,A17
.=L1.(x-x0) - L2.(x-x0) + (R1.(x-x0) - R2.(x-x0))
.=L.(xx-xx0) + (R1.(xx-xx0) - R2.(xx-xx0)) by A9,RFUNCT_1:56
.=L.(x-x0) + R.(x-x0) by A14,RFUNCT_1:56;
end;
hence f1-f2 is_differentiable_in x0 by A13;
hence diff(f1-f2,x0)=L.1 by A13,A15,Def5
.=L1.j - L2.j by A9,RFUNCT_1:56
.=diff(f1,x0) - L2.1 by A1,A3,A5,Def5
.=diff(f1,x0) - diff(f2,x0) by A2,A6,A8,Def5;
end;
theorem Th15:
f is_differentiable_in x0 implies r(#)f is_differentiable_in x0
& diff((r(#)f),x0) = r*diff(f,x0)
proof
reconsider j =1 as Element of REAL by XREAL_0:def 1;
assume
A1: f is_differentiable_in x0;
then consider N1 be Neighbourhood of x0 such that
A2: N1 c= dom f and
A3: ex L,R st for x st x in N1 holds f.x - f.x0 = L.(x-x0) + R.(x-x0);
consider L1,R1 such that
A4: for x st x in N1 holds f.x - f.x0 = L1.(x-x0) + R1.(x-x0) by A3;
reconsider R = r(#)R1 as RestFunc by Th5;
reconsider L = r(#)L1 as LinearFunc by Th3;
A5: L1 is total by Def3;
A6: N1 c= dom(r(#)f) by A2,VALUED_1:def 5;
A7: R1 is total by Def2;
A8: now
let x;
A9: x0 in N1 by RCOMP_1:16;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume
A10: x in N1;
hence (r(#)f).x - (r(#)f).x0 = r*(f.x) - (r(#)f).x0 by A6,VALUED_1:def 5
.= r*f.x - r*f.x0 by A6,A9,VALUED_1:def 5
.= r*(f.x - f.x0)
.= r*(L1.(x-x0) + R1.(x-x0)) by A4,A10
.= r*L1.(x-x0) + r*R1.(x-x0)
.= L.(xx-xx0) + r*R1.(xx-xx0) by A5,RFUNCT_1:57
.= L.(x-x0) + R.(x-x0) by A7,RFUNCT_1:57;
end;
hence r(#)f is_differentiable_in x0 by A6;
hence diff((r(#)f),x0) = L.1 by A6,A8,Def5
.= r*L1.j by A5,RFUNCT_1:57
.= r*diff(f,x0) by A1,A2,A4,Def5;
end;
theorem Th16:
f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies
f1(#)f2 is_differentiable_in x0 & diff(f1(#)f2,x0)=(f2.x0)*diff(f1,x0)+(f1.x0)*
diff(f2,x0)
proof
reconsider j =1 as Element of REAL by XREAL_0:def 1;
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0;
consider N1 be Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L,R st for x st x in N1 holds f1.x - f1.x0 = L.(x-x0) + R.(x-x0)
by A1;
consider L1,R1 such that
A5: for x st x in N1 holds f1.x - f1.x0 = L1.(x-x0) + R1.(x-x0) by A4;
consider N2 be Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L,R st for x st x in N2 holds f2.x - f2.x0 = L.(x-x0) + R.(x-x0)
by A2;
consider L2,R2 such that
A8: for x st x in N2 holds f2.x - f2.x0 = L2.(x-x0) + R2.(x-x0) by A7;
reconsider R18=R2(#)L1 as RestFunc by Th7;
reconsider R17=R1(#)R2 as RestFunc by Th4;
A9: R18 is total by Def2;
reconsider R16=R1(#)L2 as RestFunc by Th7;
reconsider R14=L1(#)L2 as RestFunc by Th6;
reconsider R19=R16+R17 as RestFunc by Th4;
reconsider R20=R19+R18 as RestFunc by Th4;
A10: R14 is total by Def2;
reconsider R12=(f1.x0)(#)R2 as RestFunc by Th5;
A11: R2 is total by Def2;
reconsider L11=(f2.x0)(#)L1 as LinearFunc by Th3;
A12: L1 is total by Def3;
reconsider R11=(f2.x0)(#)R1 as RestFunc by Th5;
A13: R1 is total by Def2;
reconsider R13=R11+R12 as RestFunc by Th4;
reconsider R15=R13+R14 as RestFunc by Th4;
reconsider R=R15+R20 as RestFunc by Th4;
consider N be Neighbourhood of x0 such that
A14: N c= N1 and
A15: N c= N2 by RCOMP_1:17;
A16: N c= dom f2 by A6,A15;
N c= dom f1 by A3,A14;
then N /\ N c= dom f1 /\ dom f2 by A16,XBOOLE_1:27;
then
A17: N c= dom (f1(#)f2) by VALUED_1:def 4;
reconsider L12=(f1.x0)(#)L2 as LinearFunc by Th3;
A18: L2 is total by Def3;
reconsider L=L11+L12 as LinearFunc by Th2;
A19: R16 is total by Def2;
A20: L11 is total & L12 is total by Def3;
A21: now
let x;
reconsider xx = x, xx0 = x0, xxx0 = x - x0 as Element of REAL
by XREAL_0:def 1;
assume
A22: x in N;
then
A23: f1.x - f1.x0 + f1.x0 = L1.(x-x0) + R1.(x-x0) + f1.x0 by A5,A14;
thus (f1(#)f2).x - (f1(#)f2).x0 = (f1.x) * (f2.x) - (f1(#) f2).x0 by
VALUED_1:5
.=(f1.x)*(f2.x)+-(f1.x)*(f2.x0)+(f1.x)*(f2.x0)-(f1.x0)*(f2.x0) by
VALUED_1:5
.=(f1.x)*((f2.x)-(f2.x0))+((f1.x)-(f1.x0))*(f2.x0)
.=(f1.x)*((f2.x)-(f2.x0))+(L1.(x-x0)+R1.(x-x0))*(f2.x0) by A5,A14,A22
.=(f1.x)*((f2.x)-(f2.x0))+((f2.x0)*L1.(x-x0)+R1.(x-x0)*(f2.x0))
.=(f1.xx)*((f2.xx)-(f2.xx0))+(L11.(xx-xx0)+(f2.xx0)*R1.(xx-xx0))
by A12,RFUNCT_1:57
.=(L1.(x-x0) + R1.(x-x0) + f1.x0)*((f2.x)-(f2.x0))+(L11.(x-x0)+R11.(x-
x0)) by A13,A23,RFUNCT_1:57
.=(L1.(x-x0) + R1.(x-x0) + f1.x0)*(L2.(x-x0) + R2.(x-x0))+ (L11.(x-x0)
+R11.(x-x0)) by A8,A15,A22
.=(L1.(x-x0) + R1.(x-x0))*(L2.(x-x0) + R2.(x-x0))+ ((f1.x0)*L2.(x-x0)+
(f1.x0)*R2.(x-x0)) + (L11.(x-x0)+R11.(x-x0))
.=(L1.(xx-xx0) + R1.(xx-xx0))*(L2.(xx-xx0) + R2.(xx-xx0)
)+ (L12.(xx-x0)+(f1.x0)*R2.(xx-x0)) + (L11.(xx-x0)+R11.(xx-x0))
by A18,RFUNCT_1:57
.=(L1.(x-x0) + R1.(x-x0))*(L2.(x-x0) + R2.(x-x0))+ (L12.(x-x0)+R12.(x-
x0)) + (L11.(x-x0)+R11.(x-x0)) by A11,RFUNCT_1:57
.=(L1.(x-x0) + R1.(x-x0))*(L2.(x-x0) + R2.(x-x0))+ (L12.(x-x0)+(L11.(x
-x0)+(R11.(x-x0)+R12.(x-x0))))
.=(L1.(xx-x0) + R1.(xx-x0))*(L2.(xx-x0) + R2.(xx-x0))+
(L12.(xx-x0)+(L11.(xx-x0)+R13.(xx-xx0))) by A13,A11,RFUNCT_1:56
.=(L1.(xx-x0) + R1.(xx-x0))*(L2.(xx-x0) + R2.(xx-x0))+
(L11.(xx-x0)+L12.(xx-x0)+R13.(xx-xx0))
.=(L1.(x-x0)*L2.(x-x0)+L1.(x-x0)*R2.(x-x0))+R1.(x-x0)*(L2.(x-x0)+R2.(x
-x0))+ (L.(x-x0)+R13.(x-x0)) by A20,RFUNCT_1:56
.=R14.(xx-x0) + R2.(x-x0)*L1.(x-x0)+R1.(x-x0)*(L2.(x-x0)+R2.(x-x0))+
(L.(x-x0)+R13.(xxx0)) by A12,A18,RFUNCT_1:56
.=R14.(x-x0) + R18.(x-x0)+(R1.(x-x0)*L2.(x-x0)+R1.(x-x0)*R2.(x-x0))+ (
L.(x-x0)+R13.(xx-xx0)) by A12,A11,RFUNCT_1:56
.=R14.(xx-x0) + R18.(x-x0)+(R16.(x-x0)+R1.(x-x0)*R2.(x-x0))+ (L.(x-x0)+
R13.(xxx0)) by A18,A13,RFUNCT_1:56
.=R14.(x-x0) + R18.(x-x0)+(R16.(x-x0)+R17.(x-x0))+ (L.(x-x0)+R13.(x-x0
)) by A13,A11,RFUNCT_1:56
.=R14.(xx-xx0) + R18.(x-x0)+R19.(x-x0)+(L.(x-x0)+R13.(x-x0))
by A13,A11,A19,RFUNCT_1:56
.=R14.(x-x0) + (R19.(x-x0)+R18.(x-x0))+(L.(x-x0)+R13.(x-x0))
.=L.(xxx0)+R13.(x-xx0)+(R14.(x-x0) + R20.(x-x0)) by A13,A11,A19,A9,
RFUNCT_1:56
.=L.(x-x0)+(R13.(x-x0)+R14.(x-x0) + R20.(x-x0))
.=L.(xx-xx0)+(R15.(x-x0)+R20.(x-x0)) by A13,A11,A10,RFUNCT_1:56
.=L.(x-x0)+R.(x-x0) by A13,A11,A10,A19,A9,RFUNCT_1:56;
end;
hence f1(#)f2 is_differentiable_in x0 by A17;
hence diff(f1(#)f2,x0)=L.1 by A17,A21,Def5
.= L11.j + L12.j by A20,RFUNCT_1:56
.= f2.x0 * L1.j + L12.j by A12,RFUNCT_1:57
.= f2.x0 * L1.1 + f1.x0 *L2.1 by A18,RFUNCT_1:57
.= f2.x0 * diff(f1,x0) + f1.x0 * L2.1 by A1,A3,A5,Def5
.= f2.x0 * diff(f1,x0) + f1.x0 * diff(f2,x0) by A2,A6,A8,Def5;
end;
theorem Th17:
Z c= dom f & f|Z = id Z implies f is_differentiable_on Z & for x
st x in Z holds (f`|Z).x = 1
proof
reconsider j =1 as Element of REAL by XREAL_0:def 1;
reconsider cf = REAL --> In(0,REAL) as Function of REAL, REAL;
set R = cf;
now
let h;
A2: now
let n be Nat;
A3: rng h c= dom R;
A5: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by SEQ_1:8
.= (h".n)*(R.(h.n)) by A5,A3,FUNCT_2:108
.= (h".n)*0
.= 0;
end;
then
A6: (h")(#)(R/*h) is constant by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent;
((h")(#)(R/*h)).0 = 0 by A2;
hence lim ((h")(#)(R/*h)) = 0 by A6,SEQ_4:25;
end;
then reconsider R as RestFunc by Def2;
reconsider L = id REAL as PartFunc of REAL,REAL;
for p holds L.p = 1*p
by XREAL_0:def 1,FUNCT_1:18;
then reconsider L as LinearFunc by Def3;
assume that
A7: Z c= dom f and
A8: f|Z = id Z;
A9: now
let x;
assume
A10: x in Z;
then f|Z.x = x by A8,FUNCT_1:18;
hence f.x = x by A10,FUNCT_1:49;
end;
A11: now
let x0;
assume
A12: x0 in Z;
then consider N being Neighbourhood of x0 such that
A13: N c= Z by RCOMP_1:18;
A14: for x st x in N holds f.x - f.x0 = L.(x-x0) + R.(x-x0)
proof
let x;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x in N;
hence f.x - f.x0 = x - f.x0 by A9,A13
.= x - x0 by A9,A12
.= L.(xx-xx0)+0
.= L.(x-x0) + R.(x-x0);
end;
N c= dom f by A7,A13;
hence f is_differentiable_in x0 by A14;
end;
hence
A15: f is_differentiable_on Z by A7,Th9;
let x0;
assume
A16: x0 in Z;
then consider N1 being Neighbourhood of x0 such that
A17: N1 c= Z by RCOMP_1:18;
A18: f is_differentiable_in x0 by A11,A16;
then 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);
then consider N being Neighbourhood of x0 such that
A19: N c= dom f;
consider N2 being Neighbourhood of x0 such that
A20: N2 c= N1 and
A21: N2 c= N by RCOMP_1:17;
A22: N2 c= dom f by A19,A21;
A23: for x st x in N2 holds f.x - f.x0 = L.(x-x0) + R.(x-x0)
proof
let x;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x in N2;
then x in N1 by A20;
hence f.x - f.x0 = x - f.x0 by A9,A17
.= x - x0 by A9,A16
.= L.(xx-xx0)+0
.= L.(x-x0) + R.(x-x0);
end;
thus (f`|Z).x0 = diff(f,x0) by A15,A16,Def7
.= L.j by A18,A22,A23,Def5
.= 1;
end;
theorem
Z c= dom (f1+f2) & f1 is_differentiable_on Z & f2 is_differentiable_on
Z implies f1+f2 is_differentiable_on Z & for x st x in Z holds ((f1+f2)`|Z).x =
diff(f1,x) + diff(f2,x)
proof
assume that
A1: Z c= dom (f1+f2) and
A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;
now
let x0;
assume x0 in Z;
then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A2,Th9;
hence f1+f2 is_differentiable_in x0 by Th13;
end;
hence
A3: f1+f2 is_differentiable_on Z by A1,Th9;
now
let x;
assume
A4: x in Z;
then
A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2,Th9;
thus ((f1+f2)`|Z).x = diff((f1+f2),x) by A3,A4,Def7
.= diff(f1,x) + diff(f2,x) by A5,Th13;
end;
hence thesis;
end;
theorem
Z c= dom (f1-f2) & f1 is_differentiable_on Z & f2 is_differentiable_on
Z implies f1-f2 is_differentiable_on Z & for x st x in Z holds ((f1-f2)`|Z).x =
diff(f1,x) - diff(f2,x)
proof
assume that
A1: Z c= dom (f1-f2) and
A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;
now
let x0;
assume x0 in Z;
then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A2,Th9;
hence f1-f2 is_differentiable_in x0 by Th14;
end;
hence
A3: f1-f2 is_differentiable_on Z by A1,Th9;
now
let x;
assume
A4: x in Z;
then
A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2,Th9;
thus ((f1-f2)`|Z).x = diff((f1-f2),x) by A3,A4,Def7
.= diff(f1,x) - diff(f2,x) by A5,Th14;
end;
hence thesis;
end;
theorem
Z c= dom (r(#)f) & f is_differentiable_on Z implies r(#)f
is_differentiable_on Z & for x st x in Z holds ((r(#) f)`|Z).x =r*diff(f,x)
proof
assume that
A1: Z c= dom (r(#)f) and
A2: f is_differentiable_on Z;
now
let x0;
assume x0 in Z;
then f is_differentiable_in x0 by A2,Th9;
hence r(#)f is_differentiable_in x0 by Th15;
end;
hence
A3: r(#)f is_differentiable_on Z by A1,Th9;
now
let x;
assume
A4: x in Z;
then
A5: f is_differentiable_in x by A2,Th9;
thus ((r(#)f)`|Z).x = diff((r(#)f),x) by A3,A4,Def7
.= r*diff(f,x) by A5,Th15;
end;
hence thesis;
end;
theorem
Z c= dom (f1(#)f2) & f1 is_differentiable_on Z & f2
is_differentiable_on Z implies f1(#)f2 is_differentiable_on Z & for x st x in Z
holds ((f1(#)f2)`|Z).x = (f2.x)*diff(f1,x) + (f1.x)*diff(f2,x)
proof
assume that
A1: Z c= dom (f1(#)f2) and
A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;
now
let x0;
assume x0 in Z;
then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A2,Th9;
hence f1(#)f2 is_differentiable_in x0 by Th16;
end;
hence
A3: f1(#)f2 is_differentiable_on Z by A1,Th9;
now
let x;
assume
A4: x in Z;
then
A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2,Th9;
thus ((f1(#)f2)`|Z).x = diff((f1(#)f2),x) by A3,A4,Def7
.= f2.x*diff(f1,x) + f1.x*diff(f2,x) by A5,Th16;
end;
hence thesis;
end;
theorem
Z c= dom f & f|Z is constant implies f is_differentiable_on Z & for x
st x in Z holds (f`|Z).x = 0
proof
reconsider cf = REAL --> In(0,REAL) as Function of REAL, REAL;
set R = cf;
now
let h;
A2: now
let n be Nat;
A3: rng h c= dom R;
A5: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by SEQ_1:8
.=(h".n)*(R.(h.n)) by A5,A3,FUNCT_2:108
.=(h".n)*0
.=0;
end;
then
A6: (h")(#)(R/*h) is constant by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent;
((h")(#)(R/*h)).0 = 0 by A2;
hence lim ((h")(#)(R/*h)) = 0 by A6,SEQ_4:25;
end;
then reconsider R as RestFunc by Def2;
set L = cf;
for p holds L.p=0*p;
then reconsider L as LinearFunc by Def3;
assume that
A7: Z c= dom f and
A8: f|Z is constant;
consider r being Element of REAL such that
A9: for x being Element of REAL st x in Z/\dom f holds f.x=r by A8,PARTFUN2:57;
A10: now
let x0;
assume
A11: x0 in Z;
then consider N being Neighbourhood of x0 such that
A12: N c= Z by RCOMP_1:18;
A13: N c= dom f by A7,A12;
A14: x0 in Z/\dom f by A7,A11,XBOOLE_0:def 4;
for x st x in N holds f.x-f.x0=L.(x-x0)+R.(x-x0)
proof
let x;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x in N;
then x in Z/\dom f by A12,A13,XBOOLE_0:def 4;
hence f.x-f.x0=r-f.x0 by A9
.=r - r by A9,A14
.=L.(xx-xx0)+0
.=L.(x-x0)+R.(x-x0);
end;
hence f is_differentiable_in x0 by A13;
end;
hence
A15: f is_differentiable_on Z by A7,Th9;
let x0;
assume
A16: x0 in Z;
then consider N being Neighbourhood of x0 such that
A17: N c= Z by RCOMP_1:18;
A18: N c= dom f by A7,A17;
A19: x0 in Z/\dom f by A7,A16,XBOOLE_0:def 4;
A20: for x st x in N holds f.x-f.x0=L.(x-x0)+R.(x-x0)
proof
let x;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x in N;
then x in Z/\dom f by A17,A18,XBOOLE_0:def 4;
hence f.x - f.x0 = r - f.x0 by A9
.=r - r by A9,A19
.=L.(xx-xx0) + 0
.=L.(x-x0) + R.(x-x0);
end;
A21: f is_differentiable_in x0 by A10,A16;
reconsider j =1 as Element of REAL by XREAL_0:def 1;
thus (f`|Z).x0 = diff(f,x0) by A15,A16,Def7
.=L.j by A21,A18,A20,Def5
.=0;
end;
theorem
Z c= dom f & (for x st x in Z holds f.x = r*x + p) implies f
is_differentiable_on Z & for x st x in Z holds (f`|Z).x = r
proof
reconsider cf = REAL --> In(0,REAL) as Function of REAL, REAL;
set R = cf;
defpred P[set] means $1 in REAL;
now
let h;
A2: now
let n be Nat;
A3: rng h c= dom R;
A5: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by SEQ_1:8
.=(h".n)*(R.(h.n)) by A5,A3,FUNCT_2:108
.=(h".n)*0
.=0;
end;
then
A6: (h")(#)(R/*h) is constant by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent;
((h")(#)(R/*h)).0 = 0 by A2;
hence lim ((h")(#)(R/*h)) = 0 by A6,SEQ_4:25;
end;
then reconsider R as RestFunc by Def2;
assume that
A7: Z c= dom f and
A8: for x st x in Z holds f.x = r*x + p;
deffunc G(Real) = In(r*$1,REAL);
consider L being PartFunc of REAL,REAL such that
A9: (for x being Element of REAL holds x in dom L iff P[x]) &
for x being Element of REAL st x in dom L holds L.x=G(x)
from SEQ_1:sch 3;
for r holds r in dom L iff r in REAL
by A9;
then dom L = REAL by Th1;
then
A10: L is total by PARTFUN1:def 2;
A11: for x holds L.x=r*x
proof let x;
reconsider x as Element of REAL by XREAL_0:def 1;
L.x=G(x) by A9;
hence thesis;
end;
then reconsider L as LinearFunc by A10,Def3;
A12: now
let x0;
assume
A13: x0 in Z;
then consider N being Neighbourhood of x0 such that
A14: N c= Z by RCOMP_1:18;
A15: for x st x in N holds f.x-f.x0=L.(x-x0)+R.(x-x0)
proof
let x;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x in N;
hence f.x-f.x0=r*x+p-f.x0 by A8,A14
.=r*x+p - (r*x0+p) by A8,A13
.=r*(x-x0)+0
.=L.(xx-xx0)+0 by A11
.=L.(x-x0)+R.(x-x0);
end;
N c= dom f by A7,A14;
hence f is_differentiable_in x0 by A15;
end;
hence
A16: f is_differentiable_on Z by A7,Th9;
let x0;
assume
A17: x0 in Z;
then consider N being Neighbourhood of x0 such that
A18: N c= Z by RCOMP_1:18;
A19: for x st x in N holds f.x-f.x0=L.(x-x0)+R.(x-x0)
proof
let x;
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x in N;
hence f.x - f.x0 = r*x+p - f.x0 by A8,A18
.=r*x+p-(r*x0+p) by A8,A17
.=r*(x-x0)+0
.=L.(xx-xx0) + 0 by A11
.=L.(x-x0) + R.(x-x0);
end;
A20: N c= dom f by A7,A18;
A21: f is_differentiable_in x0 by A12,A17;
thus (f`|Z).x0 = diff(f,x0) by A16,A17,Def7
.=L.1 by A21,A20,A19,Def5
.=r*1 by A11
.=r;
end;
theorem Th24:
for x0 being Real holds f is_differentiable_in x0 implies
f is_continuous_in x0
proof
let x0 be Real;
assume
A1: f is_differentiable_in x0;
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
ex L,R st for x st x in N holds f.x - f.x0 = L.(x-x0) + R.(x-x0);
now
consider g be Real such that
A3: 0<g and
A4: N=].x0-g,x0+g.[ by RCOMP_1:def 6;
set s2 = seq_const x0;
let s1 such that
A5: rng s1 c= dom f and
A6: s1 is convergent and
A7: lim s1 = x0 and
A8: for n being Nat holds s1.n<>x0;
consider l be Nat such that
A9: for m being Nat st l<=m holds |.s1.m-x0.|<g by A6,A7,A3,SEQ_2:def 7;
reconsider c =s2^\l as constant Real_Sequence;
deffunc G(Nat) = s1.$1-s2.$1;
consider s3 such that
A10: for n being Nat holds s3.n=G(n) from SEQ_1:sch 1;
A11: s3=s1-s2 by A10,RFUNCT_2:1;
then
A12: s3 is convergent by A6;
A13: rng c = {x0}
proof
thus rng c c= {x0}
proof
let y be object;
assume y in rng c;
then consider n such that
A14: y=(s2^\l).n by FUNCT_2:113;
A15: s2.(n+l) = x0 by SEQ_1:57;
y=s2.(n+l) by A14,NAT_1:def 3;
then y=x0 by A15;
hence thesis by TARSKI:def 1;
end;
let y be object;
assume y in {x0};
then
A16: y=x0 by TARSKI:def 1;
c.0=s2.(0+l) by NAT_1:def 3
.= y by A16,SEQ_1:57;
hence thesis by VALUED_0:28;
end;
A17: now
let p be Real such that
A18: 0<p;
reconsider n=0 as Nat;
take n;
let m being Nat such that
n<=m;
A19: m in NAT by ORDINAL1:def 12;
x0 in N by RCOMP_1:16;
then rng c c= dom f by A2,A13,ZFMISC_1:31;
then |.(f/*c).m-f.x0.|=|.f.(c.m)-f.x0.| by FUNCT_2:108,A19
.=|.f.(s2.(m+l))-f.x0.| by NAT_1:def 3
.=|.f.x0-f.x0.| by SEQ_1:57
.=0 by ABSVALUE:2;
hence |.(f/*c).m-f.x0.|<p by A18;
end;
then
A20: f/*c is convergent by SEQ_2:def 6;
lim s2 = s2.0 by SEQ_4:26
.=x0 by SEQ_1:57;
then lim s3 =x0-x0 by A6,A7,A11,SEQ_2:12
.=0;
then
A21: lim(s3^\l)=0 by A12,SEQ_4:20;
A22: now
given n being Nat such that
A23: s3.n=0;
s1.n-s2.n=0 by A10,A23;
hence contradiction by A8,SEQ_1:57;
end;
A24: now
given n being Nat such that
A25: (s3^\l).n=0;
s3.(n+l)=0 by A25,NAT_1:def 3;
hence contradiction by A22;
end;
s3^\l is 0-convergent by A12,A21;
then reconsider h=s3^\l as 0-convergent non-zero Real_Sequence
by A24,SEQ_1:5;
now
let n;
thus (f/*(h+c)-f/*c+f/*c).n=(f/*(h+c)-f/*c).n+(f/*c).n by SEQ_1:7
.=(f/*(h+c)).n-(f/*c).n+(f/*c).n by RFUNCT_2:1
.=(f/*(h+c)).n;
end;
then
A26: f/*(h+c)-f/*c+(f/*c)=f/*(h+c) by FUNCT_2:63;
now
let n;
thus (h+c).n=((s1-s2+s2)^\l).n by A11,SEQM_3:15
.=(s1-s2+s2).(n+l) by NAT_1:def 3
.=(s1-s2).(n+l)+s2.(n+l) by SEQ_1:7
.=s1.(n+l)-s2.(n+l)+s2.(n+l) by RFUNCT_2:1
.=(s1^\l).n by NAT_1:def 3;
end;
then
A27: f/*(h+c)-f/*c+(f/*c)=f/*(s1^\l) by A26,FUNCT_2:63
.=(f/*s1)^\l by A5,VALUED_0:27;
rng (h+c) c= N
proof
let y be object;
assume y in rng(h+c);
then consider n such that
A28: y=(h+c).n by FUNCT_2:113;
(h+c).n=((s1-s2+s2)^\l).n by A11,SEQM_3:15
.=(s1-s2+s2).(n+l) by NAT_1:def 3
.=(s1-s2).(n+l)+s2.(n+l) by SEQ_1:7
.=s1.(n+l)-s2.(n+l)+s2.(n+l) by RFUNCT_2:1
.=s1.(l+n);
then |.(h+c).n-x0.|<g by A9,NAT_1:12;
hence thesis by A4,A28,RCOMP_1:1;
end; then
A29: h"(#)(f/*(h+c) - f/*c) is convergent by A1,A2,A13,Th12;
then
A30: lim (h(#)(h"(#)(f/*(h+c) - f/*c))) =0*lim(h"(#) (f/*(h+c) - f/*c)) by A21,
SEQ_2:15
.=0;
now
let n be Element of NAT;
A31: h.n<>0 by A24;
thus (h(#)(h"(#)(f/*(h+c) - f/*c))).n =h.n *(h"(#)(f/*(h+c) - f/*c)).n
by SEQ_1:8
.=h.n*((h").n*(f/*(h+c) - f/*c).n) by SEQ_1:8
.=h.n*(((h.n)")*(f/*(h+c) - f/*c).n) by VALUED_1:10
.=h.n*((h.n)")*(f/*(h+c) - f/*c).n
.=1*(f/*(h+c) - f/*c).n by A31,XCMPLX_0:def 7
.=(f/*(h+c) - f/*c).n;
end;
then
A32: h(#)(h"(#)(f/*(h+c) - f/*c))=f/*(h+c)-f/*c by FUNCT_2:63;
then
A33: f/*(h+c)-f/*c is convergent by A29;
then
A34: f/*(h+c)-f/*c+f/*c is convergent by A20;
hence f/*s1 is convergent by A27,SEQ_4:21;
lim(f/*c)=f.x0 by A17,A20,SEQ_2:def 7;
then lim(f/*(h+c)-f/*c+f/*c)=0+f.x0 by A30,A32,A33,A20,SEQ_2:6
.=f.x0;
hence f.x0=lim(f/*s1) by A34,A27,SEQ_4:22;
end;
hence thesis by FCONT_1:2;
end;
theorem
f is_differentiable_on X implies f|X is continuous
proof
assume
A1: f is_differentiable_on X;
let x be Real;
assume x in dom(f|X);
then x is Real & x in X;
then f|X is_differentiable_in x by A1;
hence thesis by Th24;
end;
theorem Th26:
f is_differentiable_on X & Z c= X implies f is_differentiable_on Z
proof
assume that
A1: f is_differentiable_on X and
A2: Z c= X;
X c= dom f by A1;
hence Z c= dom f by A2;
let x0;
assume
A3: x0 in Z;
then f|X is_differentiable_in x0 by A1,A2;
then consider N being Neighbourhood of x0 such that
A4: N c= dom(f|X) and
A5: ex L,R st for x st x in N holds (f|X).x-(f|X).x0=L.(x-x0)+R.(x-x0);
consider N1 being Neighbourhood of x0 such that
A6: N1 c= Z by A3,RCOMP_1:18;
consider N2 being Neighbourhood of x0 such that
A7: N2 c= N and
A8: N2 c= N1 by RCOMP_1:17;
A9: N2 c= Z by A6,A8;
take N2;
dom(f|X)=dom f/\X by RELAT_1:61;
then dom(f|X) c=dom f by XBOOLE_1:17;
then N c= dom f by A4;
then N2 c=dom f by A7;
then N2 c=dom f/\Z by A9,XBOOLE_1:19;
hence
A10: N2 c=dom(f|Z) by RELAT_1:61;
consider L,R such that
A11: for x st x in N holds (f|X).x-(f|X).x0=L.(x-x0)+R.(x-x0) by A5;
take L,R;
let x;
assume
A12: x in N2;
then (f|X).x-(f|X).x0=L.(x-x0)+R.(x-x0) by A7,A11;
then
A13: (f|X).x-f.x0=L.(x-x0)+R.(x-x0) by A2,A3,FUNCT_1:49;
x in N by A7,A12;
then f.x-f.x0=L.(x-x0)+R.(x-x0) by A4,A13,FUNCT_1:47;
then f.x-(f|Z).x0=L.(x-x0)+R.(x-x0) by A3,FUNCT_1:49;
hence thesis by A10,A12,FUNCT_1:47;
end;
theorem ::AN
:: f is_differentiable_in x0 implies
ex R st R.0=0 & R is_continuous_in 0
proof
A1: {} REAL is closed
by XBOOLE_1:3;
([#] REAL)` = {} REAL & REAL c= REAL & [#]REAL = REAL by XBOOLE_1:37;
then
reconsider Z = [#]REAL as open Subset of REAL by A1,RCOMP_1:def 5;
reconsider cf = REAL --> In(0,REAL) as Function of REAL, REAL;
set R = cf;
reconsider f=R as PartFunc of REAL,REAL;
now
let h;
A3: now
let n be Nat;
A4: rng h c= dom R;
A6: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by SEQ_1:8
.= (h".n)*(R.(h.n)) by A6,A4,FUNCT_2:108
.= (h".n)*0
.= 0;
end;
then
A7: (h")(#)(R/*h) is constant by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent;
((h")(#)(R/*h)).0 = 0 by A3;
hence lim ((h")(#)(R/*h)) = 0 by A7,SEQ_4:25;
end;
then reconsider R as RestFunc by Def2;
set L = cf;
for p holds L.p=0*p;
then reconsider L as LinearFunc by Def3;
f|Z is constant;
then consider r being Element of REAL such that
A8: for x being Element of REAL st x in Z/\dom f holds f.x=r by PARTFUN2:57;
A9:
now
let x0;
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x0 in Z;
set N = the Neighbourhood of x0;
A11: xx0 in Z/\dom f;
for x st x in N holds f.x-f.x0=L.(x-x0)+R.(x-x0)
proof
let x;
reconsider xx = x as Element of REAL by XREAL_0:def 1;
assume x in N;
then x in Z/\dom f;
hence f.x-f.x0=r-f.x0 by A8
.=r - r by A8,A11
.=L.(xx-xx0)+0
.=L.(x-x0)+R.(x-x0);
end;
hence f is_differentiable_in x0;
end;
set x0 = the Element of REAL;
f is_differentiable_in x0 by A9; then
consider N being Neighbourhood of x0 such that
N c= dom f and
A12: ex L,R st for x st x in N holds f.x - f.x0 = L.(x-x0) + R.(x-x0);
consider L,R such that
A13: for x st x in N holds f.x - f.x0 = L.(x-x0) + R.(x-x0) by A12;
take R;
consider p such that
A14: for r holds L.r = p*r by Def3;
f.x0 - f.x0 = L.(x0-x0) + R.(x0-x0) by A13,RCOMP_1:16;
then
A15: 0 = p*0 + R.0 by A14;
hence R.0=0;
A16: now
set s3 = cs;
let h;
A17: s3.1 = 0;
(h")(#)(R/*h) is convergent by Def2;
then (h")(#)(R/*h) is bounded;
then consider M being Real such that
M>0 and
A18: for n being Nat holds |.((h")(#)(R/*h)).n.|<M by SEQ_2:3;
A19: now
let n be Nat;
|.((h")(#)(R/*h)).n.|=|.((h").n)*(R/*h).n.| by SEQ_1:8
.=|.(h.n)"*(R/*h).n.| by VALUED_1:10;
then
A20: |.(h.n)"*(R/*h).n.|<=M by A18;
0<=|.(R/*h).n.| by COMPLEX1:46;
then 0<=abs((R/*h)).n by SEQ_1:12;
hence s3.n<=abs((R/*h)).n;
|.h.n.|>=0 by COMPLEX1:46;
then |.h.n.|*|.(h.n)"*(R/*h).n.|<=M*|.h.n.| by A20,XREAL_1:64;
then |.(h.n)*((h.n)"*(R/*h).n).|<=M*|.h.n.| by COMPLEX1:65;
then
A21: |.(h.n)*(h.n)"*(R/*h).n.|<=M*|.h.n.|;
h.n <>0 by SEQ_1:5;
then |.1*(R/*h).n.|<=M*|.h.n.| by A21,XCMPLX_0:def 7;
then |.(R/*h).n.|<=M*abs(h).n by SEQ_1:12;
then |.(R/*h).n.|<=(M(#)abs(h)).n by SEQ_1:9;
hence abs((R/*h)).n<=(M(#)abs (h)).n by SEQ_1:12;
end;
lim h=0;
then lim abs(h) = |.0 .| by SEQ_4:14
.=0 by ABSVALUE:2;
then
A22: lim (M(#)abs(h)) = M*0 by SEQ_2:8
.=lim s3 by A17,SEQ_4:25;
A23: abs(R/*h) is convergent by A22,A19,SEQ_2:19;
lim s3 = 0 by A17,SEQ_4:25;
then lim abs(R/*h)=0 by A22,A19,SEQ_2:20;
hence R/*h is convergent & lim (R/*h)=R.0 by A15,A23,SEQ_4:15;
end;
now
let s1;
assume that
rng s1 c= dom R and
A24: s1 is convergent & lim s1 = 0 and
A25: for n being Nat holds s1.n<>0;
s1 is 0-convergent by A24;
then s1 is 0-convergent non-zero Real_Sequence by A25,SEQ_1:5;
hence R/*s1 is convergent & lim (R/*s1)=R.0 by A16;
end;
hence thesis by FCONT_1:2;
end;
definition
let f be PartFunc of REAL, REAL;
attr f is differentiable means :Def8:
f is_differentiable_on dom f;
end;
Lm1: {} REAL is closed
by XBOOLE_1:3;
Lm2: [#] REAL is open
by XBOOLE_1:37,Lm1;
registration
cluster differentiable for Function of REAL, REAL;
existence
proof
reconsider Z = REAL as open Subset of REAL by Lm2;
reconsider f = id REAL as Function of REAL, REAL;
take f;
A1: Z = dom f;
f is_differentiable_on Z by A1,Th17;
hence thesis;
end;
end;
theorem
for f being differentiable PartFunc of REAL, REAL st Z c= dom f holds
f is_differentiable_on Z by Th26,Def8;