:: Differentiable Functions into Real Normed Spaces
:: by Hiroyuki Okazaki , Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received October 13, 2010
:: Copyright (c) 2010-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, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1, NAT_1,
FDIFF_1, SUBSET_1, RELAT_1, RCOMP_1, TARSKI, SEQ_1, ARYTM_3, VALUED_1,
FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, COMPLEX1, STRUCT_0,
CARD_1, VALUED_0, XXREAL_0, FUNCOP_1, XXREAL_2, XBOOLE_0, XXREAL_1,
FUNCT_7, ASYMPT_1;
notations TARSKI, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2,
FUNCOP_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, VALUED_0,
COMPLEX1, VALUED_1, SEQ_1, SEQ_2, RCOMP_1, FDIFF_1, STRUCT_0, PRE_TOPC,
RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, NDIFF_1, NFCONT_3;
constructors REAL_1, FDIFF_1, VFUNCT_1, NDIFF_1, RELSET_1, RVSUM_1, BINOP_2,
INTEGR15, NAT_D, MEASURE6, NFCONT_3, COMSEQ_2, SEQ_1, NUMBERS;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, MEMBERED, FUNCT_2,
NUMBERS, VALUED_0, NORMSP_0, NORMSP_1, RELAT_1, SUBSET_1, FUNCOP_1,
NAT_1, RCOMP_1, VALUED_1, SEQ_4, FDIFF_1, SEQ_1, SEQ_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions XBOOLE_0, TARSKI;
equalities RCOMP_1, SUBSET_1, XBOOLE_0;
expansions RCOMP_1, XBOOLE_0, TARSKI;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1,
ZFMISC_1, SEQ_1, SEQ_2, NAT_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2,
ORDINAL1, SEQ_4, NORMSP_1, LOPBAN_1, LOPBAN_3, PARTFUN1, PARTFUN2,
FDIFF_1, NDIFF_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1,
VALUED_0, NORMSP_0, XREAL_0, RCOMP_1, SEQM_3, RFUNCT_2, NFCONT_3;
schemes FUNCT_2, SEQ_1;
begin :: Differentiable of Functions into a Real Normed Space
reserve F for RealNormSpace;
reserve G for RealNormSpace;
reserve X for set;
reserve x,x0,g,r,s,p 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 seq for sequence of G;
reserve f,f1,f2 for PartFunc of REAL,the carrier of F;
reserve h for 0-convergent non-zero Real_Sequence;
reserve c for constant Real_Sequence;
set cs = seq_const 0;
theorem Th1:
(for n holds ||. seq.n .|| <= s1.n) & s1 is convergent & lim s1=0 implies
seq is convergent & lim(seq)=0.G
proof
assume that
A1: for n holds ||. seq.n .|| <= s1.n and
A2: s1 is convergent and
A3: lim(s1)=0;
now
let p be Real;
assume 0<p;
then consider n being Nat such that
A4: for m being Nat st n<=m holds |.s1.m-0 .|<p by A2,A3,SEQ_2:def 7;
reconsider n as Element of NAT by ORDINAL1:def 12;
now
let m be Nat;
A5: m in NAT by ORDINAL1:def 12;
assume n<=m; then
A6: |.s1.m-0 .|<p by A4;
A7: ||. seq.m-0.G .|| = ||. seq.m .|| by RLVECT_1:13;
A8: s1.m <= |.s1.m.| by ABSVALUE:4;
||. seq.m .|| <= s1.m by A1,A5;
then ||. seq.m - 0.G .|| <= |.s1.m.| by A7,A8,XXREAL_0:2;
hence ||. seq.m - 0.G .|| < p by A6,XXREAL_0:2;
end;
hence ex n being Nat st
for m being Nat st n<=m holds ||. seq.m - (0.G) .|| < p;
end; then
A9: for p be Real st 0<p
ex n being Nat st for m being Nat st n<=m
holds ||. seq.m - 0.G .|| < p;
hence seq is convergent by NORMSP_1:def 6;
hence thesis by A9,NORMSP_1:def 7;
end;
theorem Th2:
(s1^\k)(#)(seq^\k)= (s1(#)seq) ^\k
proof
now let n;
thus ((s1(#)seq) ^\k).n=(s1(#)seq).(n+k) by NAT_1:def 3
.=s1.(n+k)*seq.(n+k) by NDIFF_1:def 2
.=(s1 ^\k).n*seq.(n+k) by NAT_1:def 3
.=(s1 ^\k).n*(seq ^\k).n by NAT_1:def 3
.=((s1 ^\k)(#)(seq ^\k)).n by NDIFF_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
definition let F;
let IT be PartFunc of REAL,the carrier of F;
attr IT is RestFunc-like means :Def1:
IT is total & for h holds (h")(#)(IT/*h) is convergent &
lim ((h")(#)(IT/*h)) = 0.F;
end;
registration let F;
cluster RestFunc-like for PartFunc of REAL,the carrier of F;
existence
proof
take f = REAL --> 0.F;
thus f is total;
now
let h;
now let n be Nat;
A2: rng h c= dom f;
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 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<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 reconsider h = s1 as 0-convergent non-zero Real_Sequence
by A20,FDIFF_1:def 1;
A21: for n ex x be Real st x in N & x in N1 & h.n=x-x0
proof
let n;
take x=x0+g/(n+2);
reconsider z0=0 as Element of NAT;
z0 + 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=1*p1 by A13,A15;
A24: r=1*r1 by A9,A11;
A25: now
let x be Real;
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 (x-x0)*r1 + R/.(x-x0) = L1/.(x-x0) + R1/.(x-x0) by A11;
then ((x-x0)*1) *r1 + R/.(x-x0) = ((x-x0)*1)*p1 + R1/.(x-x0) by A15;
then ((x-x0)*1) *r + R/.(x-x0) = ((x-x0)*1)*p1 + R1/.(x-x0)
by A24,RLVECT_1:def 7;
hence (x-x0)*r + R/.(x-x0) = (x-x0)*s + R1/.(x-x0) by A23,RLVECT_1:def 7;
end;
now
R1 is total by Def1;
then dom R1 = REAL by PARTFUN1:def 2; then
A28: rng h c= dom R1;
let n be Nat;
R is total by Def1;
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 be Real st x in N & x in N1 & h.n=x-x0 by A21;
then (h.n)*r + R/.(h.n) = (h.n)*s + R1/.(h.n) by A25; then
(1/(h.n))*((h.n)*r)+(1/(h.n))*(R/.(h.n))
=(1/(h.n))*((h.n)*s+R1/.(h.n)) by RLVECT_1:def 5; then
((1/(h.n))*(h.n))*r +(1/(h.n))*(R/.(h.n))
=(1/(h.n))*((h.n)*s+R1/.(h.n)) by RLVECT_1:def 7;
then A31:
((1/(h.n))*(h.n))*r +(1/(h.n))*(R/.(h.n))
=(1/(h.n))*((h.n)*s)+ (1/(h.n))*(R1/.(h.n)) by RLVECT_1:def 5;
A32: (1/(h.n))*(R/.(h.n)) = (h.n)"*(R/.(h.n)) by XCMPLX_1:215
.= (h".n)*(R/.(h.n)) by VALUED_1:10
.= (h".n)*((R/*h).n) by A30,A29,FUNCT_2:109
.= ((h")(#)(R/*h)).n by NDIFF_1:def 2;
A33: h.n <> 0 by SEQ_1:5;
A34: (1/(h.n))*(R1/.(h.n)) = (h.n)"*(R1/.(h.n)) by XCMPLX_1:215
.= (h".n)*(R1/.(h.n)) by VALUED_1:10
.= (h".n)*((R1/*h).n) by A30,A28,FUNCT_2:109
.= ((h")(#)(R1/*h)).n by NDIFF_1:def 2;
A35: ((1/(h.n))*(h.n))*s = 1*s by A33,XCMPLX_1:106
.= s by RLVECT_1:def 8;
((1/(h.n))*(h.n))*r = 1*r by A33,XCMPLX_1:106
.= r by RLVECT_1:def 8;
then r + ((h")(#)(R/*h)).n
= s + ((h")(#)(R1/*h)).n by A31,A35,A32,A34,RLVECT_1:def 7; then
r +( ((h")(#)(R/*h)).n - ((h")(#)(R/*h)).n )
= s + ((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n by RLVECT_1:28; then
r +( ((h")(#)(R/*h)).n - ((h")(#)(R/*h)).n )
= s +( ((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n ) by RLVECT_1:28; then
r + 0.F = s +( ((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n ) by RLVECT_1:15;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by RLVECT_1:4;
then
r -s = (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) +(s-s) by RLVECT_1:28;
then
r -s = (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) +0.F by RLVECT_1:15;
then
A36: r -s = ((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n by RLVECT_1:4;
thus r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by A36,NORMSP_1:def 3;
end; then
((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant & (((h")(#)(R1/*h))-((h"
)(#)(R /*h))).0 = r-s by VALUED_0:def 18; then
A37: lim ( (h")(#)(R1/*h)-(h")(#)(R/*h) ) = r-s by NDIFF_1:18;
A38: (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0.F by Def1;
(h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0.F by Def1;
then r-s = 0.F-0.F by A37,A38,NORMSP_1:26;
hence thesis by RLVECT_1:13,21;
end;
end;
definition let F,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 Th9:
f is_differentiable_on X implies X is Subset of REAL
by XBOOLE_1:1;
theorem Th10:
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 A2: Z c=dom f;
let x0;
assume
A3: x0 in Z;
then f|Z is_differentiable_in x0 by A1;
then consider N being Neighbourhood of x0 such that
A4: N c= dom(f|Z) and
A5: 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 A4;
consider L,R such that
A6: for x st x in N holds (f|Z)/.x - (f|Z)/.x0
= L/.(x-x0) + R/.(x-x0) by A5;
now let x;
assume
A7: x in N;
then A8: (f|Z)/.x-(f|Z)/.x0=L/.(x-x0)+R/.(x-x0) by A6;
f/.x-(f|Z)/.x0=L/.(x-x0)+R/.(x-x0) by A8,A4,A7,PARTFUN2:15;
hence f/.x-f/.x0=L/.(x-x0)+R/.(x-x0) by A2,A3,PARTFUN2:17;
end;
hence thesis;
end;
assume that
A9: Z c=dom f and
A10: for x st x in Z holds f is_differentiable_in x;
thus Z c=dom f by A9;
let x0;
assume
A11: x0 in Z;
then consider N1 being Neighbourhood of x0 such that
A12: N1 c= Z by RCOMP_1:18;
f is_differentiable_in x0 by A10,A11;
then consider N being Neighbourhood of x0 such that
A13: N c= dom f and
A14: 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
A15: N2 c= N1 and
A16: N2 c= N by RCOMP_1:17;
A17: N2 c= Z by A12,A15;
take N2;
N2 c= dom f by A13,A16;
then N2 c= dom f/\Z by A17,XBOOLE_1:19;
hence
A18: N2 c= dom(f|Z) by RELAT_1:61;
consider L,R such that
A19: for x st x in N holds f/.x-f/.x0=L/.(x-x0)+R/.(x-x0) by A14;
A20: x0 in N2 by RCOMP_1:16;
take L,R;
now let x;
assume
A21: x in N2;
then f/.x-f/.x0=L/.(x-x0)+R/.(x-x0) by A16,A19;
then (f|Z)/.x-f/.x0=L/.(x-x0)+R/.(x-x0) by A21,A18,PARTFUN2:15;
hence (f|Z)/.x-(f|Z)/.x0=L/.(x-x0)+R/.(x-x0) by A20,A18,PARTFUN2:15;
end;
hence thesis;
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,f,X;
assume
A1: f is_differentiable_on X;
func f`|X -> PartFunc of REAL,the carrier of F means :Def6:
dom it = X & for x st x in X holds it.x = diff(f,x);
existence
proof
deffunc FG(Real) = diff(f,$1);
defpred P[set] means $1 in X;
consider F0 being PartFunc of REAL,the carrier of F such that
A2: (for x being Element of REAL holds x in dom F0 iff P[x]) &
for x being Element of REAL st x in dom F0
holds F0.x = FG(x) from SEQ_1:sch 3;
take F0;
now
A3: X is Subset of REAL by A1,Th9;
let y be object;
assume y in X;
hence y in dom F0 by A2,A3;
end; then
A4: X c= dom F0;
for y be object st y in dom F0 holds y in X by A2;
then dom F0 c= X;
hence dom F0 = X by A4;
now
let x;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
assume x in X;
then xx in dom F0 by A2;
hence F0.x = diff(f,x) by A2;
end;
hence thesis;
end;
uniqueness
proof
let F0,G0 be PartFunc of REAL,the carrier of F;
assume that
A5: dom F0 = X and
A6: for x st x in X holds F0.x = diff(f,x) and
A7: dom G0 = X and
A8: for x st x in X holds G0.x = diff(f,x);
now
let x be Element of REAL;
assume
A9: x in dom F0;
then F0.x = diff(f,x) by A5,A6;
hence F0.x=G0.x by A5,A8,A9;
end;
hence thesis by A5,A7,PARTFUN1:5;
end;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem
(Z c= dom f & ex r be Point of F st rng f = {r})
implies f is_differentiable_on Z &
for x st x in Z holds (f`|Z)/.x = 0.F
proof
set R = REAL --> 0.F;
A1: dom R = REAL;
now let h;
now let n be Nat;
A2: rng h c= dom R;
A3: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by NDIFF_1:def 2
.= (h".n)*(R/.(h.n)) by A3,A2,FUNCT_2:108
.= 0.F by RLVECT_1:10;
end; then
(h")(#)(R/*h) is constant
& ((h")(#)(R/*h)).0 = 0.F by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent &
lim ((h")(#)(R/*h)) = 0.F by NDIFF_1:18;
end;
then reconsider R as RestFunc of F by Def1;
reconsider L = (REAL --> 0.F) as Function of REAL,F;
now let p be Real;
reconsider pp=p as Element of REAL by XREAL_0:def 1;
thus L/.p = L/.pp
.= (0.F)
.= p*(0.F) by RLVECT_1:10;
end;
then reconsider L as LinearFunc of F by Def2;
assume
A4: Z c= dom f;
given r be Point of F such that
A5: rng f = {r};
A6: now let x0;
assume A7: x0 in dom f;
then f/.x0 = f.x0 by PARTFUN1:def 6;
then f/.x0 in {r} by A5,A7,FUNCT_1:def 3;
hence f/.x0 = r by TARSKI:def 1;
end;
A8: now
let x0;
assume
A9: x0 in Z;
then consider N being Neighbourhood of x0 such that
A10: N c= Z by RCOMP_1:18;
A11: N c= dom f by A4,A10;
for x st x in N holds f/.x - f/.x0 = L/.(x-x0) + R/.(x-x0)
proof
let x;
A12: x-x0 in REAL by XREAL_0:def 1;
then
A13: R/.(x-x0)=R.(x-x0) by A1,PARTFUN1:def 6
.= 0.F by FUNCOP_1:7,A12;
assume x in N;
hence f/.x - f/.x0 = r - f/.x0 by A6,A11
.= r - r by A4,A6,A9
.=0.F by RLVECT_1:15
.=L.(x-x0) by FUNCOP_1:7,A12
.=L/.(x-x0) by A1,PARTFUN1:def 6,A12
.=L/.(x-x0) + R/.(x-x0) by A13,RLVECT_1:4;
end;
hence f is_differentiable_in x0 by A11;
end;
hence
A14: f is_differentiable_on Z by A4,Th10;
let x0;
assume
A15: x0 in Z; then
A16: f is_differentiable_in x0 by A8;
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;
A19: x-x0 in REAL by XREAL_0:def 1;
then
A20: R/.(x-x0)=R.(x-x0) by A1,PARTFUN1:def 6
.= 0.F by FUNCOP_1:7,A19;
assume x in N;
hence f/.x - f/.x0 = r - f/.x0 by A6,A17
.=r - r by A4,A6,A15
.=0.F by RLVECT_1:15
.=L.(x-x0) by FUNCOP_1:7,A19
.=L/.(x-x0) by A1,PARTFUN1:def 6,A19
.=L/.(x-x0) + R/.(x-x0) by A20,RLVECT_1:4;
end;
dom ((f`|Z)) = Z by A14,Def6;
hence (f`|Z)/.x0 =(f`|Z).x0 by A15,PARTFUN1:def 6
.= diff(f,x0) by A14,A15,Def6
.= L/.jj by A16,A17,A18,Def4
.=0.F;
end;
theorem Th13:
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;
reconsider z0=0 as Nat;
x0 + z0 < x0 + g & x0 - g < x0 - 0 by A9,XREAL_1:8,15; then
A11: x0 in N2 by A10;
now 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 y in dom f by A2;
end; then
A12: rng c c= dom f;
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;
reconsider z0=0 as Real;
lim h = z0;
then lim (h + c) = z0 + 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;
for y be object st y in rng (c^\n) holds
y in N2 by A11,A15,TARSKI:def 1;
hence rng(c^\n) c= N2;
now 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;
reconsider z0=0 as Nat;
n + z0 <= 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 y in N2 by A10,A16,A18;
end;
hence rng ((h+c)^\n) c= N2;
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;
now let y be object;
assume
A21: y in rng (c^\n);
rng (c^\n) = rng c by VALUED_0:26;
then y = x0 by A7,A21,TARSKI:def 1;
then y in N by A4,A11;
hence y in dom f by A2;
end;
then
A22: rng (c^\n) c= dom f;
A23: (h^\n)"(#)(L/*(h^\n) + R/*(h^\n)) is convergent &
lim ((h^\n)"(#)(L/*(h^\n) + R/*(h^\n))) = L/.1
proof
deffunc F0(Element of NAT) = L.jj + ((h^\n)"(#)(R/*(h^\n))).$1;
consider s1 be sequence of the carrier of F such that
A24: for k holds s1.k = F0(k) from FUNCT_2:sch 4;
A25: now
A26: ((h^\n)")(#)(R/*(h^\n)) is convergent & lim (((h^\n)")(#) (R/*(h^\n
)))=0.F by Def1;
let r be Real;
assume 0<r;
then consider m be Nat such that
A27: for k be Nat
st m<=k holds ||.(((h^\n)")(#) (R/*(h^\n))).k
- 0.F .|| <r by A26,NORMSP_1:def 7;
take n1=m;
let k be Nat such that
A28: n1<=k;
A29: k in NAT by ORDINAL1:def 12;
A30: ||. s1.k -L/.jj .||
= ||. L.jj + ((h^\n)"(#)(R/*(h^\n))).k - L/.jj .|| by A24,A29
.= ||. (((h^\n)")(#)(R/*(h^\n))).k + (L/.jj - L/.jj) .|| by RLVECT_1:28
.= ||. (((h^\n)")(#)(R/*(h^\n))).k + 0.F .|| by RLVECT_1:15
.= ||. (((h^\n)")(#)(R/*(h^\n))).k .|| by RLVECT_1:4;
||. (((h^\n)")(#)(R/*(h^\n))).k -0.F .|| < r by A27,A28;
hence ||. s1.k -L/.jj .|| <r by A30,RLVECT_1:13;
end;
consider s be Point of F such that
A31: for p1 be Real holds L/.p1=p1*s by Def2;
A32: L/.jj = 1*s by A31
.= s by RLVECT_1:def 8;
now
let m;
A33: (h^\n).m <> 0 by SEQ_1:5;
thus ((h^\n)"(#)(L/*(h^\n) + R/*(h^\n))).m
= ((h^\n)"(#)(L/*(h^\n)) + (h^\n)"(#)(R/*(h^\n))).m by NDIFF_1:9
.= ((h^\n)"(#)(L/*(h^\n))).m + ((h^\n)"(#)(R/*(h^\n))).m
by NORMSP_1:def 2
.= ((h^\n)").m*(L/*(h^\n)).m + ((h^\n)"(#)(R/*(h^\n))).m
by NDIFF_1:def 2
.= ((h^\n)").m*(L/.((h^\n).m)) + ((h^\n)"(#)(R/*(h^\n))).m
by FUNCT_2:115
.= ((h^\n)").m*(((h^\n).m)*s) + ((h^\n)"(#)(R/*(h^\n))).m by A31
.= ((h^\n).m)"*(((h^\n).m) *s) + ((h^\n)"(#)(R/*(h^\n))).m
by VALUED_1:10
.= ((h^\n).m)"*(((h^\n).m)) *s + ((h^\n)"(#)(R/*(h^\n))).m
by RLVECT_1:def 7
.= 1*s + ((h^\n)"(#)(R/*(h^\n))).m by A33,XCMPLX_0:def 7
.= s + ((h^\n)"(#)(R/*(h^\n))).m by RLVECT_1:def 8
.= s1.m by A24,A32;
end; then
A34: (h^\n)"(#)(L/*(h^\n) + R/*(h^\n)) = s1 by FUNCT_2:63;
hence (h^\n)"(#)(L/*(h^\n) + R/*(h^\n)) is convergent
by A25,NORMSP_1:def 6;
hence thesis by A34,A25,NORMSP_1:def 7;
end;
for y being object st y in rng ((h+c)^\n) holds y in dom f by A2,A4,A19;
then
A35: rng ((h+c)^\n) c= dom f;
for y being object st y in rng (h+c) holds y in dom f by A2,A8;
then
A36: rng (h+c) c= dom f;
A37: 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
A38: ((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
A39: (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,A38,A39;
end;
A40: R is total by Def1;
now
let k;
dom R = REAL by A40,FUNCT_2:def 1; then
A41:rng (h^\n) c= dom R;
thus (f/*((h+c)^\n)-f/*(c^\n)).k
= (f/*((h+c)^\n)).k-(f/*(c^\n)).k by NORMSP_1:def 3
.= f/.(((h+c)^\n).k) - (f/*(c^\n)).k by A35,FUNCT_2:109
.= f/.(((h+c)^\n).k) - f/.((c^\n).k) by A22,FUNCT_2:109
.= L/.((h^\n).k) + R/.((h^\n).k) by A37
.= (L/*(h^\n)).k + R/.((h^\n).k) by FUNCT_2:115
.= (L/*(h^\n)).k + (R/*(h^\n)).k by A41,FUNCT_2:109
.= (L/*(h^\n) + R/*(h^\n)).k by NORMSP_1:def 2;
end;
then f/*((h+c)^\n) - f/*(c^\n) = L/*(h^\n) + R/*(h^\n) by FUNCT_2:63; then
A42: ((h^\n)"(#)(L/*(h^\n) + R/*(h^\n)))
= ( ( h^\n)"(#)(((f/*(h+c))^\n)-f/*(c^\n))) by A36,VALUED_0:27
.=((h^\n)"(#)(((f/*(h+c))^\n)-((f/*c)^\n))) by A12,VALUED_0:27
.=((h^\n)"(#)(((f/*(h+c))-(f/*c))^\n)) by NDIFF_1:16
.=(((h")^\n)(#)(((f/*(h+c))-(f/*c))^\n)) by SEQM_3:18
.=(( h"(#)((f/*(h+c))-(f/*c)))^\n) by Th2; then
A43: L/.1 = lim ((h")(#)((f/*(h+c)) - (f/*c))) by A23,LOPBAN_3:11;
thus h" (#) (f/*(h+c) - f/*c) is convergent by A23,A42,LOPBAN_3:10;
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,A43,Def4;
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
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 of F by Th7;
reconsider L=L1+L2 as LinearFunc of F by Th3;
consider N be Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by RCOMP_1:17;
A11: N c= dom f2 by A6,A10;
N c= dom f1 by A3,A9;
then N /\ N c= dom f1 /\ dom f2 by A11,XBOOLE_1:27; then
A12: N c= dom (f1+f2) by VFUNCT_1:def 1;
R1 is total & R2 is total by Def1; then
R1+R2 is total by VFUNCT_1:32; then
A13: dom (R1+R2) = REAL by FUNCT_2:def 1;
L1+L2 is total by VFUNCT_1:32; then
A14: dom (L1+L2) = REAL by FUNCT_2:def 1;
A15: now let x;
A16: x0 in N by RCOMP_1:16;
A17: x - x0 in REAL by XREAL_0:def 1;
assume
A18: x in N;
hence (f1+f2)/.x - (f1+f2)/.x0 = (f1/.x+f2/.x) - (f1+f2)/.x0 by A12,
VFUNCT_1:def 1
.=f1/.x+f2/.x - (f1/.x0+f2/.x0) by A12,A16,VFUNCT_1:def 1
.=f1/.x+(f2/.x - (f1/.x0+f2/.x0)) by RLVECT_1:28
.=f1/.x+((f2/.x - f2/.x0) - f1/.x0 ) by RLVECT_1:27
.=f1/.x+(f2/.x - f2/.x0) - f1/.x0 by RLVECT_1:28
.= (f2/.x - f2/.x0) + (f1/.x - f1/.x0) by RLVECT_1:28
.=L1/.(x-x0)+R1/.(x-x0) + (f2/.x - f2/.x0) by A5,A9,A18
.=L1/.(x-x0)+R1/.(x-x0) + (L2/.(x-x0) + R2/.(x-x0)) by A8,A10,A18
.=L1/.(x-x0)+R1/.(x-x0) + L2/.(x-x0) + R2/.(x-x0) by RLVECT_1:def 3
.=(L1/.(x-x0)+L2/.(x-x0)) + R1/.(x-x0) + R2/.(x-x0) by RLVECT_1:def 3
.=(L1/.(x-x0)+L2/.(x-x0)) + (R1/.(x-x0) + R2/.(x-x0)) by RLVECT_1:def 3
.=L/.(x-x0)+(R1/.(x-x0) + R2/.(x-x0)) by A14,VFUNCT_1:def 1,A17
.=L/.(x-x0)+R/.(x-x0) by A13,VFUNCT_1:def 1,A17;
end;
hence f1+f2 is_differentiable_in x0 by A12;
hence diff(f1+f2,x0)=L/.jj by A12,A15,Def4
.=L/.jj
.=L1/.jj + L2/.jj by A14,VFUNCT_1:def 1
.=L1/.jj + L2/.jj
.=L1/.jj + L2/.jj
.=diff(f1,x0) + L2/.jj by A1,A3,A5,Def4
.=diff(f1,x0) + diff(f2,x0) by A2,A6,A8,Def4;
end;
theorem Th15:
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
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 of F by Th7;
reconsider L=L1-L2 as LinearFunc of F by Th3;
consider N be Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by RCOMP_1:17;
A11: N c= dom f2 by A6,A10;
N c= dom f1 by A3,A9;
then N /\ N c= dom f1 /\ dom f2 by A11,XBOOLE_1:27; then
A12: N c= dom (f1-f2) by VFUNCT_1:def 2;
R1 is total & R2 is total by Def1; then
R1-R2 is total by VFUNCT_1:32; then
A13: dom (R1-R2) = REAL by FUNCT_2:def 1;
L1-L2 is total by VFUNCT_1:32; then
A14: dom (L1-L2) = REAL by FUNCT_2:def 1;
A15: now
let x;
A16: x0 in N by RCOMP_1:16;
A17: x - x0 in REAL by XREAL_0:def 1;
assume
A18: x in N;
hence (f1-f2)/.x - (f1-f2)/.x0
= (f1/.x-f2/.x) - (f1-f2)/.x0 by A12,VFUNCT_1:def 2
.=f1/.x-f2/.x - (f1/.x0-f2/.x0) by A12,A16,VFUNCT_1:def 2
.=f1/.x-(f2/.x + (f1/.x0-f2/.x0)) by RLVECT_1:27
.=f1/.x-(f2/.x + f1/.x0-f2/.x0) by RLVECT_1:28
.=f1/.x-(f1/.x0+ (f2/.x -f2/.x0)) by RLVECT_1:28
.=(f1/.x-f1/.x0) - (f2/.x -f2/.x0) by RLVECT_1:27
.=L1/.(x-x0)+R1/.(x-x0) - (f2/.x - f2/.x0) by A5,A9,A18
.=L1/.(x-x0)+R1/.(x-x0) - (L2/.(x-x0) + R2/.(x-x0)) by A8,A10,A18
.=L1/.(x-x0)+(R1/.(x-x0) - (L2/.(x-x0) + R2/.(x-x0))) by RLVECT_1:28
.=L1/.(x-x0)+( (R1/.(x-x0) - R2/.(x-x0)) - L2/.(x-x0)) by RLVECT_1:27
.=L1/.(x-x0)+((R1/.(x-x0) - R2/.(x-x0))) - L2/.(x-x0) by RLVECT_1:28
.=(L1/.(x-x0)-L2/.(x-x0)) + (R1/.(x-x0) - R2/.(x-x0)) by RLVECT_1:28
.=L/.(x-x0)+(R1/.(x-x0) - R2/.(x-x0)) by A14,VFUNCT_1:def 2,A17
.=L/.(x-x0)+R/.(x-x0) by A13,VFUNCT_1:def 2,A17;
end;
hence f1-f2 is_differentiable_in x0 by A12;
hence diff(f1-f2,x0)=L/.jj by A12,A15,Def4
.=L/.jj
.=L1/.jj - L2/.jj by A14,VFUNCT_1:def 2
.=L1/.jj - L2/.jj
.=L1/.jj - L2/.jj
.=diff(f1,x0) - L2/.jj by A1,A3,A5,Def4
.=diff(f1,x0) - diff(f2,x0) by A2,A6,A8,Def4;
end;
theorem Th16:
for r be Real st
f is_differentiable_in x0 holds r(#)f is_differentiable_in x0
& diff((r(#)f),x0) = r*diff(f,x0)
proof
let r be Real;
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 of F by Th8;
reconsider L = r(#)L1 as LinearFunc of F by Th4;
A5: N1 c= dom(r(#)f) by A2,VFUNCT_1:def 4;
R1 is total by Def1; then
r(#)R1 is total by VFUNCT_1:34; then
A6: dom (r(#)R1) = REAL by FUNCT_2:def 1;
r(#)L1 is total by VFUNCT_1:34; then
A7: dom (r(#)L1) = REAL by FUNCT_2:def 1;
A8: now
let x;
A9: x0 in N1 by RCOMP_1:16;
A10: x - x0 in REAL by XREAL_0:def 1;
assume
A11: x in N1;
hence (r(#)f)/.x - (r(#)f)/.x0
= r*(f/.x) - (r(#)f)/.x0 by A5,VFUNCT_1:def 4
.= r*f/.x - r*f/.x0 by A5,A9,VFUNCT_1:def 4
.= r*(f/.x - f/.x0) by RLVECT_1:34
.= r*(L1/.(x-x0) + R1/.(x-x0)) by A4,A11
.= r*L1/.(x-x0) + r*R1/.(x-x0) by RLVECT_1:def 5
.= L/.(x-x0) + r*R1/.(x-x0) by A7,VFUNCT_1:def 4,A10
.= L/.(x-x0) + R/.(x-x0) by A6,VFUNCT_1:def 4,A10;
end;
hence r(#)f is_differentiable_in x0 by A5;
hence diff((r(#)f),x0) = L/.jj by A5,A8,Def4
.=L/.jj
.=r*L1/.jj by A7,VFUNCT_1:def 4
.= r*L1/.jj
.= r*diff(f,x0) by A1,A2,A4,Def4;
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,Th10;
hence f1+f2 is_differentiable_in x0 by Th14;
end;
hence
A3: f1+f2 is_differentiable_on Z by A1,Th10;
let x;
assume
A4: x in Z; then
A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2,Th10;
thus ((f1+f2)`|Z).x = diff((f1+f2),x) by A3,A4,Def6
.= diff(f1,x) + diff(f2,x) by A5,Th14;
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,Th10;
hence f1-f2 is_differentiable_in x0 by Th15;
end;
hence
A3: f1-f2 is_differentiable_on Z by A1,Th10;
let x;
assume
A4: x in Z; then
A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2,Th10;
thus ((f1-f2)`|Z).x = diff((f1-f2),x) by A3,A4,Def6
.= diff(f1,x) - diff(f2,x) by A5,Th15;
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,Th10;
hence r(#)f is_differentiable_in x0 by Th16;
end;
hence
A3: r(#)f is_differentiable_on Z by A1,Th10;
let x;
assume
A4: x in Z; then
A5: f is_differentiable_in x by A2,Th10;
thus ((r(#)f)`|Z).x = diff((r(#)f),x) by A3,A4,Def6
.= r*diff(f,x) by A5,Th16;
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.F
proof
set R = REAL --> 0.F;
A1: dom R = REAL;
now let h;
now let n be Nat;
A2: rng h c= dom R;
A3: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by NDIFF_1:def 2
.=(h".n)*(R/.(h.n)) by A3,A2,FUNCT_2:108
.=0.F by RLVECT_1:10;
end; then
(h")(#)(R/*h) is constant
& ((h")(#)(R/*h)).0 = 0.F by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent &
lim ((h")(#)(R/*h)) = 0.F by NDIFF_1:18;
end;
then reconsider R as RestFunc of F by Def1;
set L = REAL --> 0.F;
now let p be Real;
reconsider pp=p as Element of REAL by XREAL_0:def 1;
thus L/.p = L/.pp
.= (0.F)
.= p*(0.F) by RLVECT_1:10;
end;
then reconsider L as LinearFunc of F by Def2;
assume that
A4: Z c= dom f and
A5: f|Z is constant;
consider r be Point of F such that
A6: for x being Element of REAL st x in Z/\dom f holds f.x=r
by A5,PARTFUN2:57;
A7: now let x;
assume A8: x in Z/\dom f;
then x in dom f by XBOOLE_0:def 4;
hence f/.x= f.x by PARTFUN1:def 6
.= r by A8,A6;
end;
A9: now
let x0;
assume
A10: x0 in Z;
then consider N being Neighbourhood of x0 such that
A11: N c= Z by RCOMP_1:18;
A12: N c= dom f by A4,A11;
A13: x0 in Z/\dom f by A4,A10,XBOOLE_0:def 4;
for x st x in N holds f/.x-f/.x0=L/.(x-x0)+R/.(x-x0)
proof
let x;
A14: x-x0 in REAL by XREAL_0:def 1;
then
A15: R/.(x-x0)=R.(x-x0) by A1,PARTFUN1:def 6
.= 0.F by FUNCOP_1:7,A14;
assume x in N;
then x in Z/\dom f by A11,A12,XBOOLE_0:def 4;
hence f/.x-f/.x0=r-f/.x0 by A7
.=r - r by A7,A13
.=0.F by RLVECT_1:15
.=L.(x-x0) by FUNCOP_1:7,A14
.=L/.(x-x0) by A1,PARTFUN1:def 6,A14
.=L/.(x-x0) + R/.(x-x0) by A15,RLVECT_1:4;
end;
hence f is_differentiable_in x0 by A12;
end;
hence
A16: f is_differentiable_on Z by A4,Th10;
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: N c= dom f by A4,A18;
A20: x0 in Z/\dom f by A4,A17,XBOOLE_0:def 4;
A21: for x st x in N holds f/.x-f/.x0=L/.(x-x0)+R/.(x-x0)
proof
let x;
A22: x-x0 in REAL by XREAL_0:def 1;
then
A23: R/.(x-x0)=R.(x-x0) by A1,PARTFUN1:def 6
.= 0.F by FUNCOP_1:7,A22;
assume x in N;
then x in Z/\dom f by A18,A19,XBOOLE_0:def 4;
hence f/.x - f/.x0 = r - f/.x0 by A7
.=r - r by A7,A20
.=0.F by RLVECT_1:15
.=L.(x-x0) by FUNCOP_1:7,A22
.=L/.(x-x0) by A1,PARTFUN1:def 6,A22
.=L/.(x-x0) + R/.(x-x0) by A23,RLVECT_1:4;
end;
A24: f is_differentiable_in x0 by A9,A17;
thus (f`|Z).x0 = diff(f,x0) by A16,A17,Def6
.=L/.jj by A24,A19,A21,Def4
.=0.F;
end;
theorem Th21:
for r,p be Point of F,Z,f
st Z c= dom f & (for x st x in Z holds f/.x = x*r + p)
holds f is_differentiable_on Z
& for x st x in Z holds (f`|Z).x = r
proof
let r,p be Point of F;
let Z,f;
set R = (REAL --> 0.F);
defpred P[object] means $1 in REAL;
A1: dom R = REAL;
now let h;
now let n be Nat;
A2: rng h c= dom R;
A3: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by NDIFF_1:def 2
.=(h".n)*(R/.(h.n)) by A3,A2,FUNCT_2:108
.=0.F by RLVECT_1:10;
end; then
(h")(#)(R/*h) is constant
& ((h")(#)(R/*h)).0 = 0.F by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent &
lim ((h")(#)(R/*h)) = 0.F by NDIFF_1:18;
end;
then reconsider R as RestFunc of F by Def1;
assume that
A4: Z c= dom f and
A5: for x st x in Z holds f/.x = x*r + p;
deffunc G(Real) = $1*r;
consider L being PartFunc of REAL,the carrier of F such that
A6: (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 x being Real holds x in dom L iff P[x]
by A6;
then
A7: dom L = REAL by FDIFF_1:1;
A8: for x being Element of REAL holds L/.x=G(x)
proof let x be Element of REAL;
A9: x in dom L by A7;
L.x=G(x) by A6;
hence thesis by PARTFUN1:def 6,A9;
end;
A10: L is total by PARTFUN1:def 2,A7;
A11: now
let x;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
thus L/.x = L/.xx
.=x*r by A8;
end;
then reconsider L as LinearFunc of F by A10,Def2;
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 be Real;
A16: x-x0 in REAL by XREAL_0:def 1;
then
A17: R/.(x-x0)=R.(x-x0) by A1,PARTFUN1:def 6
.= 0.F by FUNCOP_1:7,A16;
assume x in N;
hence f/.x-f/.x0=x*r+p-f/.x0 by A5,A14
.=x*r+p - (x0*r+p) by A5,A13
.=x*r+p - x0*r-p by RLVECT_1:27
.=p+(x*r- x0*r)-p by RLVECT_1:28
.=(x*r- x0*r)+(p-p) by RLVECT_1:28
.=(x*r- x0*r)+0.F by RLVECT_1:15
.=(x-x0)*r + 0.F by RLVECT_1:35
.=L/.(x-x0) + R/.(x-x0) by A17,A11;
end;
N c= dom f by A4,A14;
hence f is_differentiable_in x0 by A15;
end;
hence
A18: f is_differentiable_on Z by A4,Th10;
let x0;
assume
A19: x0 in Z;
then consider N being Neighbourhood of x0 such that
A20: N c= Z by RCOMP_1:18;
A21: for x st x in N holds f/.x-f/.x0=L/.(x-x0)+R/.(x-x0)
proof
let x;
A22: x-x0 in REAL by XREAL_0:def 1;
then
A23: R/.(x-x0)=R.(x-x0) by A1,PARTFUN1:def 6
.= 0.F by FUNCOP_1:7,A22;
assume x in N;
hence f/.x - f/.x0 = x*r+p - f/.x0 by A5,A20
.=x*r+p - (x0*r+p) by A5,A19
.=x*r+p - x0*r-p by RLVECT_1:27
.=p+(x*r- x0*r)-p by RLVECT_1:28
.=(x*r- x0*r)+(p-p) by RLVECT_1:28
.=(x*r- x0*r)+0.F by RLVECT_1:15
.=(x-x0)*r + 0.F by RLVECT_1:35
.=L/.(x-x0) + R/.(x-x0) by A23,A11;
end;
A24: N c= dom f by A4,A20;
A25: f is_differentiable_in x0 by A12,A19;
thus (f`|Z).x0 = diff(f,x0) by A18,A19,Def6
.=L/.jj by A25,A24,A21,Def4
.=1*r by A11
.=r by RLVECT_1:def 8;
end;
theorem Th22:
for x0 being Real st f is_differentiable_in x0 holds
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);
A3:x0 in N by RCOMP_1:16;
now
consider g be Real such that
A4: 0<g and
A5: N=].x0-g,x0+g.[ by RCOMP_1:def 6;
reconsider xx=x0 as Element of REAL by XREAL_0:def 1;
set s2 = seq_const x0;
let s1 such that
A6: rng s1 c= dom f and
A7: s1 is convergent and
A8: lim s1 = x0 and
A9: for n being Nat holds s1.n<>x0;
consider l be Nat such that
A10: for m being Nat st l<=m holds |.s1.m-x0.|<g by A7,A8,A4,SEQ_2:def 7;
reconsider c =s2^\l as constant Real_Sequence;
deffunc G(Real) = s1.$1-s2.$1;
consider s3 such that
A11: for n being Nat holds s3.n=G(n) from SEQ_1:sch 1;
A12: s3=s1-s2 by A11,RFUNCT_2:1;
then
A13: s3 is convergent by A7;
A14: rng c = {x0}
proof
thus rng c c= {x0}
proof let y be object;
assume y in rng c;
then consider n such that
A15: y=(s2^\l).n by FUNCT_2:113;
y=s2.(n+l) by A15,NAT_1:def 3;
then y=x0 by SEQ_1:57;
hence y in {x0} by TARSKI:def 1;
end;
let y be object;
assume y in {x0}; then
A16: y=x0 by TARSKI:def 1;
reconsider z0 = 0 as Element of NAT;
c.z0 = s2.(z0 + l) by NAT_1:def 3
.= y by A16,SEQ_1:57;
hence y in rng c 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 be 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,A14,ZFMISC_1:31;
then ||.(f/*c).m-f/.x0 .||=||.f/.(c.m)-f/.x0 .|| by FUNCT_2:109,A19
.=||.f/.(s2.(m+l))-f/.x0 .|| by NAT_1:def 3
.=||.f/.x0-f/.x0 .|| by SEQ_1:57
.=||. 0.F .|| by RLVECT_1:15
.=0;
hence ||.(f/*c).m-f/.x0 .||<p by A18;
end; then
A20: f/*c is convergent by NORMSP_1:def 6;
lim s2 = s2.0 by SEQ_4:26
.=x0 by SEQ_1:57;
then lim s3 =x0-x0 by A7,A8,A12,SEQ_2:12
.=0; then
A21: lim(s3^\l)=0 by A13,SEQ_4:20;
A22:
now
given n such that
A23: s3.n=0;
s1.n-s2.n=0 by A11,A23;
hence contradiction by A9,SEQ_1:57;
end;
A24:
now
given n being Nat such that
A25: (s3^\l).n=0;
A26: n+l in NAT by ORDINAL1:def 12;
s3.(n+l)=0 by A25,NAT_1:def 3;
hence contradiction by A22,A26;
end;
then s3^\l is non-zero by SEQ_1:5;
then reconsider h=s3^\l as 0-convergent non-zero Real_Sequence
by A13,A21,FDIFF_1:def 1;
now
let n;
thus (f/*(h+c)-f/*c+f/*c).n
=(f/*(h+c)-f/*c).n+(f/*c).n by NORMSP_1:def 2
.=(f/*(h+c)).n-(f/*c).n+(f/*c).n by NORMSP_1:def 3
.=(f/*(h+c)).n-((f/*c).n-(f/*c).n) by RLVECT_1:29
.=(f/*(h+c)).n-0.F by RLVECT_1:15
.=(f/*(h+c)).n by RLVECT_1:13;
end; then
A27: 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 A12,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
A28: f/*(h+c)-f/*c+(f/*c)=f/*(s1^\l) by A27,FUNCT_2:63
.=(f/*s1)^\l by A6,VALUED_0:27;
now let y be object;
assume y in rng(h+c);
then consider n such that
A29: y=(h+c).n by FUNCT_2:113;
(h+c).n=((s1-s2+s2)^\l).n by A12,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 A10,NAT_1:12;
hence y in N by A5,A29,RCOMP_1:1;
end; then
A30:rng(h+c) c= N;
A31: lim (h(#)(h"(#)(f/*(h+c) - f/*c)))
= 0 * lim(h"(#) (f/*(h+c) - f/*c)) by A21,A1,A2,A14,Th13,A30,NDIFF_1:14
.=0.F by RLVECT_1:10;
now
let n;
A32: h.n<>0 by A24;
thus (h(#)(h"(#)(f/*(h+c) - f/*c))).n = h.n *(h"(#)(f/*(h+c) - f/*c)).n
by NDIFF_1:def 2
.=h.n*((h").n*(f/*(h+c) - f/*c).n) by NDIFF_1:def 2
.=h.n*(((h.n)")*(f/*(h+c) - f/*c).n) by VALUED_1:10
.=h.n*((h.n)")*(f/*(h+c) - f/*c).n by RLVECT_1:def 7
.=1*(f/*(h+c) - f/*c).n by A32,XCMPLX_0:def 7
.=(f/*(h+c) - f/*c).n by RLVECT_1:def 8;
end; then
A33: h(#)(h"(#)(f/*(h+c) - f/*c))=f/*(h+c)-f/*c by FUNCT_2:63; then
A34: f/*(h+c)-f/*c is convergent by A30,A1,A2,A14,Th13,NDIFF_1:13; then
f/*(h+c)-f/*c+f/*c is convergent by A20,NORMSP_1:19;
hence f/*s1 is convergent by A28,LOPBAN_3:10;
lim(f/*c)=f/.x0 by A17,A20,NORMSP_1:def 7;
then lim(f/*(h+c)-f/*c+f/*c)=0.F+f/.x0 by A31,A33,A34,A20,NORMSP_1:25
.=f/.x0 by RLVECT_1:4;
hence f/.x0=lim(f/*s1) by A34,A28,A20,LOPBAN_3:11,NORMSP_1:19;
end;
hence thesis by A3,A2,NFCONT_3:7;
end;
theorem
f is_differentiable_on X implies (f|X) is continuous
proof
assume
A1: f is_differentiable_on X;
for x being Real st x in dom(f|X) holds f|X is_continuous_in x
by A1,Th22;
hence thesis by NFCONT_3:def 2;
end;
theorem Th24:
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; then
A3:Z c= dom f by A2;
now let x0;
assume
A4: x0 in Z;
then f|X is_differentiable_in x0 by A1,A2;
then consider N being Neighbourhood of x0 such that
A5: N c= dom(f|X) and
A6: 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
A7: N1 c= Z by A4,RCOMP_1:18;
consider N2 being Neighbourhood of x0 such that
A8: N2 c= N and
A9: N2 c= N1 by RCOMP_1:17;
A10: N2 c= Z by A7,A9;
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 A5;
then N2 c=dom f by A8;
then N2 c=dom f/\Z by A10,XBOOLE_1:19; then
A11: N2 c=dom(f|Z) by RELAT_1:61;
A12: N2 c= dom(f|X) by A8,A5;
consider L,R such that
A13: for x st x in N holds
(f|X)/.x-(f|X)/.x0=L/.(x-x0)+R/.(x-x0) by A6;
for x st x in N2 holds
(f|Z)/.x-(f|Z)/.x0=L/.(x-x0)+R/.(x-x0)
proof
let x;
assume
A14: x in N2;
then A15:(f|X)/.x-(f|X)/.x0=L/.(x-x0)+R/.(x-x0) by A8,A13;
A16: x0 in N2 by RCOMP_1:16;
(f|X)/.x-f/.x0=L/.(x-x0)+R/.(x-x0) by A15,A16,A12,PARTFUN2:15;
then f/.x-f/.x0=L/.(x-x0)+R/.(x-x0) by A14,A12,PARTFUN2:15;
then f/.x-(f|Z)/.x0=L/.(x-x0)+R/.(x-x0) by A16,A11,PARTFUN2:15;
hence thesis by A14,A11,PARTFUN2:15;
end;
hence (f|Z) is_differentiable_in x0 by A11;
end;
hence thesis by A3;
end;
Lm1: {} REAL is closed;
theorem
ex R be RestFunc of F st R/.0=0.F & R is_continuous_in 0
proof
([#] REAL)` = {} REAL & REAL c= REAL & [#]REAL = REAL by XBOOLE_1:37;
then
reconsider Z = [#]REAL as open Subset of REAL by Lm1,RCOMP_1:def 5;
set R = (REAL --> 0.F);
reconsider f=R as PartFunc of REAL,the carrier of F;
A1: dom R = REAL;
now
let h;
now
let n be Nat;
A2: rng h c= dom R;
A3: n in NAT by ORDINAL1:def 12;
thus ((h")(#)(R/*h)).n = (h".n)*((R/*h).n) by NDIFF_1:def 2
.= (h".n)*(R/.(h.n)) by A3,A2,FUNCT_2:108
.= 0.F by RLVECT_1:10;
end;
then (h")(#)(R/*h) is constant
& ((h")(#)(R/*h)).0 = 0.F by VALUED_0:def 18;
hence (h")(#)(R/*h) is convergent &
lim ((h")(#)(R/*h)) = 0.F by NDIFF_1:18;
end;
then reconsider R as RestFunc of F by Def1;
set L = (REAL --> 0.F);
now let p be Real;
reconsider pp=p as Element of REAL by XREAL_0:def 1;
thus L/.p = L/.pp
.= 0.F
.= p*(0.F) by RLVECT_1:10;
end;
then reconsider L as LinearFunc of F by Def2;
A5: f|Z is constant;
consider r be Point of F such that
A6: for x being Element of REAL st x in Z/\dom f holds f.x=r
by A5,PARTFUN2:57;
A7: now let x;
assume A8: x in Z/\dom f;
then x in dom f;
hence f/.x= f.x by PARTFUN1:def 6
.= r by A8,A6;
end;
A9: now
let x0;
assume
A10: x0 in Z;
set N = the Neighbourhood of x0;
for x st x in N holds f/.x-f/.x0=L/.(x-x0)+R/.(x-x0)
proof
A12: x0 in Z/\dom f by A10;
let x;
A13: x-x0 in REAL by XREAL_0:def 1;
then
A14: R/.(x-x0)=R.(x-x0) by A1,PARTFUN1:def 6
.= 0.F by FUNCOP_1:7,A13;
assume x in N;
then x in Z/\dom f;
hence f/.x-f/.x0=r-f/.x0 by A7
.=r - r by A7,A12
.=0.F by RLVECT_1:15
.=L.(x-x0) by FUNCOP_1:7,A13
.=L/.(x-x0) by A1,PARTFUN1:def 6,A13
.=L/.(x-x0) + R/.(x-x0) by A14,RLVECT_1:4;
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
A15: 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
A16: for x st x in N holds f/.x - f/.x0 = L/.(x-x0) + R/.(x-x0) by A15;
take R;
consider p be Point of F such that
A17: for r holds L/.r = r*p by Def2;
f/.x0 - f/.x0 = L/.(x0-x0) + R/.(x0-x0) by A16,RCOMP_1:16; then
0.F = L/.(x0-x0) + R/.(x0-x0) by RLVECT_1:15; then
0.F = 0 * p+ R/.0 by A17; then
0.F = 0.F + R/.0 by RLVECT_1:10;
hence
A18: R/.0=0.F by RLVECT_1:4;
A19: now
set s3 = cs;
let h;
A20: s3.1 = 0;
(h")(#)(R/*h) is convergent &
lim ((h")(#)(R/*h)) = 0.F by Def1;
then ||.(h")(#)(R/*h).|| is bounded by LOPBAN_1:20,SEQ_2:13;
then consider M being Real such that M>0 and
A21: for n being Nat holds |.(||.((h")(#)(R/*h)) .||).n .| <M by SEQ_2:3;
A22: now let n;
|.(||.((h")(#)(R/*h)) .||).n .| <M by A21; then
|. ||.((h")(#)(R/*h)).n .|| .| <M by NORMSP_0:def 4;
hence ||.((h")(#)(R/*h)).n .|| < M by ABSVALUE:def 1;
end;
reconsider z0=0 as Real;
A23: now
let n be Element of NAT;
||.((h")(#)(R/*h)).n .||=||.((h").n)*(R/*h).n .|| by NDIFF_1:def 2
.=||.(h.n)"*(R/*h).n .|| by VALUED_1:10; then
A24: ||.(h.n)"*(R/*h).n .||<=M by A22;
|.(h.n).|>=0 by COMPLEX1:46;
then |.(h.n).|*||.(h.n)"*(R/*h).n .|| <=M*|.(h.n).| by A24,XREAL_1:64;
then ||.(h.n)*((h.n)"*(R/*h).n) .|| <=M*|.(h.n).| by NORMSP_1:def 1; then
A25: ||.(h.n)*(h.n)"*(R/*h).n .||<=M*|.(h.n).| by RLVECT_1:def 7;
h.n <>0 by SEQ_1:5;
then ||.1*(R/*h).n.|| <=M*|.(h.n).| by A25,XCMPLX_0:def 7;
then ||.(R/*h).n.|| <=M*|.(h.n).| by RLVECT_1:def 8;
then ||.(R/*h).n .|| <=M*abs(h).n by SEQ_1:12;
hence ||.(R/*h).n .|| <=(M(#)abs(h)).n by SEQ_1:9;
end;
lim h=z0;
then lim abs(h) = |.z0.| by SEQ_4:14
.=z0 by ABSVALUE:2; then
A26: lim (M(#)abs(h)) = M*z0 by SEQ_2:8
.=lim s3 by A20,SEQ_4:25;
reconsider z0=0 as Real;
lim (M(#)abs(h)) = 0 by A26,A20,SEQ_4:25;
hence R/*h is convergent & lim (R/*h)=R/.0 by A18,A23,Th1;
end;
R is total by Def1; then
A27:dom R=REAL by FUNCT_2:def 1;
now
let s1;
assume that rng s1 c= dom R and
A28: s1 is convergent & lim s1 = 0 and
A29: for n being Nat holds s1.n <> 0;
for n being Nat holds s1.n <> 0
by A29;
then s1 is non-zero by SEQ_1:5;
then s1 is 0-convergent non-zero Real_Sequence by A28,FDIFF_1:def 1;
hence R/*s1 is convergent & R/.In(0,REAL)=lim (R/*s1) by A19;
end;
hence thesis by A27,NFCONT_3:7;
end;
definition let F;
let f be PartFunc of REAL, the carrier of F;
attr f is differentiable means :Def7:
f is_differentiable_on dom f;
end;
Lm2: [#] REAL is open
by XBOOLE_1:37,Lm1;
registration let F;
cluster differentiable for Function of REAL, the carrier of F;
existence
proof
reconsider Z = REAL as open Subset of REAL by Lm2;
reconsider f = (REAL --> 0.F) as Function of REAL, the carrier of F;
take f;
A1: Z = dom f;
now let x;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
assume x in Z;
thus f/.x = f/.xx
.= 0.F
.= x*(0.F) by RLVECT_1:10
.= x*(0.F) + 0.F by RLVECT_1:4;
end;
then f is_differentiable_on Z by A1,Th21;
hence thesis;
end;
end;
theorem
for f being differentiable PartFunc of REAL, the carrier of F
st Z c= dom f holds f is_differentiable_on Z
by Def7,Th24;