:: Real Function One-Side Differantiability
:: by Ewa Burakowska and Beata Madras
::
:: Received December 12, 1991
:: Copyright (c) 1991-2017 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, FDIFF_1, SEQ_1, FUNCT_1, PARTFUN1, REAL_1, SUBSET_1,
XXREAL_0, CARD_1, XXREAL_1, ARYTM_1, TARSKI, RELAT_1, ARYTM_3, VALUED_0,
SEQ_2, ORDINAL2, VALUED_1, FUNCT_2, NAT_1, LIMFUNC1, XBOOLE_0, COMPLEX1,
SQUARE_1, ORDINAL4, RCOMP_1, FDIFF_3, ASYMPT_1;
notations TARSKI, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0,
COMPLEX1, REAL_1, SQUARE_1, NAT_1, RELSET_1, PARTFUN1, FUNCT_1, FUNCT_2,
FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, RFUNCT_1, RCOMP_1,
FDIFF_1, LIMFUNC1, RECDEF_1;
constructors FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3,
PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, LIMFUNC1, PARTFUN1, FDIFF_1,
VALUED_1, RECDEF_1, XXREAL_2, SETFAM_1, RELSET_1, BINOP_2, RVSUM_1,
COMSEQ_2, SEQ_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, FDIFF_1,
VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, SEQ_4, SQUARE_1, NAT_1, SEQ_1,
SEQ_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, SQUARE_1, PROB_1, LIMFUNC1, VALUED_1;
expansions TARSKI;
theorems NAT_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, ABSVALUE, RFUNCT_1, RFUNCT_2,
RCOMP_1, FDIFF_1, LIMFUNC2, FDIFF_2, TARSKI, SCHEME1, ZFMISC_1, FCONT_3,
FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1,
COMPLEX1, XXREAL_0, VALUED_1, XXREAL_1, XXREAL_2, VALUED_0, ORDINAL1,
XREAL_0;
schemes SEQ_1, SCHEME1, FUNCT_2, FDIFF_2;
begin
reserve h,h1,h2 for 0-convergent non-zero Real_Sequence,
c,c1 for constant Real_Sequence,
f,f1,f2 for PartFunc of REAL,REAL,
x0,r,r0,r1,r2,g,g1,g2 for Real,
n0,k,n,m for Element of NAT,
a,b,d for Real_Sequence,
x for set;
theorem Th1:
(ex r st r>0 & [.x0-r,x0.] c= dom f) implies ex h,c st rng c ={x0
} & rng (h+c) c= dom f & for n being Nat holds h.n < 0
proof
given r such that
A1: r>0 and
A2: [.x0-r,x0.] c= dom f;
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set a = seq_const x0;
reconsider a as constant Real_Sequence;
deffunc F(Nat) = (-r)/($1+2);
consider b such that
A3: for n being Nat holds b.n = F(n) from SEQ_1:sch 1;
A4: now
let n be Nat;
0 < r/(n+2) by A1,XREAL_1:139;
then -(r/(n+2)) < -0 by XREAL_1:24;
then (-r)/(n+2) < 0 by XCMPLX_1:187;
hence b.n < 0 by A3;
end;
then for n being Nat holds 0 <> b.n;
then
A5: b is non-zero by SEQ_1:5;
b is convergent & lim b = 0 by A3,SEQ_4:31;
then reconsider b as 0-convergent non-zero Real_Sequence
by A5,FDIFF_1:def 1;
take b;
take a;
thus rng a = {x0}
proof
thus rng a c= {x0}
proof
let x be object;
assume x in rng a;
then ex n st x = a.n by FUNCT_2:113;
then x = x0 by SEQ_1:57;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {x0};
then x = x0 by TARSKI:def 1
.= a.0 by SEQ_1:57;
hence thesis by VALUED_0:28;
end;
thus rng (b+a) c= dom f
proof
let x be object;
assume x in rng (b+a);
then consider n such that
A6: x = (b+a).n by FUNCT_2:113;
0+1 < n + 2 by XREAL_1:8;
then r*1 < r*(n+2) by A1,XREAL_1:97;
then r * (n+2)" < r*(n + 2)*((n + 2)") by XREAL_1:68;
then r * ((n+2)") < r*((n + 2)*(n + 2)");
then r * (n+2)" < r * 1 by XCMPLX_0:def 7;
then r/(n+2) < r by XCMPLX_0:def 9;
then x0 - r < x0 - r/(n+2) by XREAL_1:15;
then x0 - r < x0 + - r/(n+2);
then
A7: x0 - r <= x0 + (-r)/(n+2) by XCMPLX_1:187;
0 < r/(n+2) by A1,XREAL_1:139;
then x0 - r/(n+2) < x0 - 0 by XREAL_1:15;
then x0 + - r/(n+2) <= x0;
then x0 + (-r)/(n+2) <= x0 by XCMPLX_1:187;
then
A8: x0 + (-r)/(n+2) in {g1: x0 - r <= g1 & g1 <= x0 } by A7;
x = b.n +a.n by A6,SEQ_1:7
.= (-r)/(n+2) + a.n by A3
.= x0 + (-r)/(n+2) by SEQ_1:57;
then x in [.x0 - r, x0.] by A8,RCOMP_1:def 1;
hence thesis by A2;
end;
thus thesis by A4;
end;
theorem Th2:
(ex r st r>0 & [.x0,x0+r.] c= dom f) implies ex h,c st rng c ={x0
} & rng (h+c) c= dom f & for n being Nat holds h.n > 0
proof
given r such that
A1: r>0 and
A2: [.x0,x0+r.] c= dom f;
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set a = seq_const x0;
reconsider a as constant Real_Sequence;
deffunc F(Nat) = r/($1+2);
consider b such that
A3: for n being Nat holds b.n = F(n) from SEQ_1:sch 1;
A4: now
let n be Nat;
0 < r/(n+2) by A1,XREAL_1:139;
hence 0 < b.n by A3;
end;
then for n being Nat holds 0<>b.n;
then
A5: b is non-zero by SEQ_1:5;
b is convergent & lim b = 0 by A3,SEQ_4:31;
then reconsider b as 0-convergent non-zero Real_Sequence
by A5,FDIFF_1:def 1;
take b,a;
thus rng a = {x0}
proof
thus rng a c= {x0}
proof
let x be object;
assume x in rng a;
then ex n st x = a.n by FUNCT_2:113;
then x = x0 by SEQ_1:57;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {x0};
then x = x0 by TARSKI:def 1
.= a.0 by SEQ_1:57;
hence thesis by VALUED_0:28;
end;
thus rng (b+a) c= dom f
proof
let x be object;
assume x in rng (b+a);
then consider n such that
A6: x = (b+a).n by FUNCT_2:113;
0+1 < n + 2 by XREAL_1:8;
then r*1 < r*(n+2) by A1,XREAL_1:97;
then r * (n+2)" < r*(n + 2)*((n + 2)") by XREAL_1:68;
then r * (n+2)" < r*((n + 2)*(n + 2)");
then r * (n+2)" < r * 1 by XCMPLX_0:def 7;
then r/(n+2) < r by XCMPLX_0:def 9;
then
A7: x0 + r/(n+2) <= x0 + r by XREAL_1:6;
0 < r/(n+2) by A1,XREAL_1:139;
then x0 + 0 < x0 + r/(n+2) by XREAL_1:8;
then
A8: x0 + r/(n+2) in {g1: x0 <= g1 & g1 <= x0 + r} by A7;
x = b.n +a.n by A6,SEQ_1:7
.= r/(n+2) + a.n by A3
.= r/(n+2) + x0 by SEQ_1:57;
then x in [.x0,x0 + r.] by A8,RCOMP_1:def 1;
hence thesis by A2;
end;
thus thesis by A4;
end;
theorem Th3:
(for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n being Nat holds h.n <
0) holds h"(#)(f/*(h+c) - f/*c) is convergent) & {x0} c= dom f implies for h1,
h2,c st rng c ={x0} & rng (h1+c) c= dom f &
(for n being Nat holds h1.n < 0) & rng (h2+c)
c= dom f & (for n being Nat holds h2.n < 0)
holds lim (h1"(#)(f/*(h1+c) - f/*c)) = lim (
h2"(#)(f/*(h2+c) - f/*c))
proof
assume that
A1: for h,c st rng c ={x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n < 0)
holds h"(#)(f/*(h+c) - f/*c) is convergent and
A2: {x0} c= dom f;
let h1,h2,c such that
A3: rng c ={x0} and
A4: rng (h1+c) c= dom f and
A5: for n being Nat holds h1.n < 0 and
A6: rng (h2+c) c= dom f and
A7: for n being Nat holds h2.n < 0;
deffunc G(Element of NAT) = h2.$1;
deffunc F(Element of NAT) = h1.$1;
consider d such that
A8: for n holds d.(2*n) = F(n) & d.(2*n + 1) = G(n) from SCHEME1:sch 2;
now
let n be Nat;
consider m such that
A9: n = 2*m or n = 2*m + 1 by SCHEME1:1;
now
per cases by A9;
suppose
A10: n = 2*m;
d.(2*m) = h1.m by A8;
hence d.n <> 0 by A10,SEQ_1:5;
end;
suppose
A11: n = 2*m + 1;
d.(2*m + 1) = h2.m by A8;
hence d.n <> 0 by A11,SEQ_1:5;
end;
end;
hence d.n <> 0;
end;
then
A12: d is non-zero by SEQ_1:5;
A13: h2 is convergent & lim h2 = 0;
h1 is convergent & lim h1 = 0;
then d is convergent & lim d = 0 by A8,A13,FDIFF_2:1;
then reconsider d as 0-convergent non-zero Real_Sequence
by A12,FDIFF_1:def 1;
deffunc F(Nat) = 2*$1;
consider a such that
A14: for n being Nat holds a.n = F(n) from SEQ_1:sch 1;
deffunc G(Nat) = 2*$1+1;
consider b such that
A15: for n being Nat holds b.n = G(n) from SEQ_1:sch 1;
for n holds b.n = G(n) by A15;
then reconsider b as increasing sequence of NAT by FDIFF_2:3;
A16: rng (d + c) c= dom f
proof
let x be object;
assume x in rng (d + c);
then consider n such that
A17: x = (d + c).n by FUNCT_2:113;
consider m such that
A18: n = 2*m or n = 2*m + 1 by SCHEME1:1;
A19: x = d.n + c.n by A17,SEQ_1:7;
now
per cases by A18;
suppose
n = 2*m;
then x = h1.m + c.(2*m) by A8,A19
.= h1.m + c.m by VALUED_0:23
.= (h1 + c).m by SEQ_1:7;
then x in rng (h1 + c) by VALUED_0:28;
hence thesis by A4;
end;
suppose
n = 2*m + 1;
then x = h2.m + c.(2*m +1) by A8,A19
.= h2.m + c.m by VALUED_0:23
.= (h2 + c).m by SEQ_1:7;
then x in rng (h2 + c) by VALUED_0:28;
hence thesis by A6;
end;
end;
hence thesis;
end;
now
let n;
thus ((d"(#)(f/*(d+c) - f/*c))*b).n=(d"(#)(f/*(d+c) - f/*c)).(b.n) by
FUNCT_2:15
.= (d"(#)(f/*(d+c) - f/*c)).(2*n + 1) by A15
.= (d").(2*n + 1)*(f/*(d+c) - f/*c).(2*n + 1) by SEQ_1:8
.= (d").(2*n +1)*((f/*(d+c)).(2*n + 1) - (f/*c).(2*n + 1)) by RFUNCT_2:1
.= (d.( 2*n + 1))"*((f/*(d+c)).(2*n + 1) - (f/*c).(2*n + 1)) by
VALUED_1:10
.= (h2.n)"*((f/*(d+c)).(2*n + 1) - (f/*c).(2*n + 1)) by A8
.= (h2").n*((f/*(d+c)).(2*n + 1) - (f/*c).(2*n + 1)) by VALUED_1:10
.= (h2").n*(f.((d + c).(2*n + 1)) - (f/*c).(2*n + 1)) by A16,FUNCT_2:108
.= (h2").n*(f.(d.(2*n + 1) + c.(2*n + 1)) - (f/*c).(2*n + 1)) by SEQ_1:7
.= (h2").n*(f.(h2.n + c.(2*n + 1)) - (f/*c).(2*n + 1)) by A8
.= (h2").n*(f.(h2.n + c.n) - (f/*c).(2*n + 1)) by VALUED_0:23
.= (h2").n*(f.((h2 + c).n) - (f/*c).(2*n + 1)) by SEQ_1:7
.= (h2").n*((f/*(h2+c)).n - (f/*c).(2*n + 1)) by A6,FUNCT_2:108
.= (h2").n*((f/*(h2+c)).n - f.(c.(2*n + 1))) by A2,A3,FUNCT_2:108
.= (h2").n*((f/*(h2+c)).n - f.(c.n)) by VALUED_0:23
.= (h2").n*((f/*(h2+c)).n - (f/*c).n) by A2,A3,FUNCT_2:108
.= (h2").n*(f/*(h2+c) - f/*c).n by RFUNCT_2:1
.= (h2"(#)(f/*(h2+c) - f/*c)).n by SEQ_1:8;
end;
then
A20: h2"(#)(f/*(h2+c) - f/*c) is subsequence of d"(#)(f/*(d+c) - f/*c) by
FUNCT_2:63;
now
let n be Nat;
consider m such that
A21: n = 2*m or n = 2*m + 1 by SCHEME1:1;
now
per cases by A21;
suppose
A22: n = 2*m;
d.(2*m) = h1.m by A8;
hence d.n < 0 by A5,A22;
end;
suppose
A23: n = 2*m + 1;
d.(2*m + 1) = h2.m by A8;
hence d.n < 0 by A7,A23;
end;
end;
hence d.n < 0;
end;
then
A24: d"(#)(f/*(d+c) - f/*c) is convergent by A1,A3,A16;
for n holds a.n = F(n) by A14;
then reconsider a as increasing sequence of NAT by FDIFF_2:2;
now
let n;
thus ((d"(#)(f/*(d+c) - f/*c))*a).n = (d"(#)(f/*(d+c) - f/*c)).(a.n ) by
FUNCT_2:15
.= (d"(#)(f/*(d+c) - f/*c)).(2*n) by A14
.= (d").(2*n)*(f/*(d+c) - f/*c).(2*n) by SEQ_1:8
.= (d").(2*n)*((f/*(d+c)).(2*n) - (f/*c).(2*n)) by RFUNCT_2:1
.= (d.(2*n))"*((f/*(d+c)).(2*n) - (f/*c).(2*n)) by VALUED_1:10
.= (h1.n)"*((f/*(d+c)).(2*n) - (f/*c).(2*n)) by A8
.= (h1").n*((f/*(d+c)).(2*n) - (f/*c).(2*n)) by VALUED_1:10
.= (h1").n*(f.((d + c).(2*n)) - (f/*c).(2*n)) by A16,FUNCT_2:108
.= (h1").n*(f.(d.(2*n) + c.(2*n)) - (f/*c).(2*n)) by SEQ_1:7
.= (h1").n*(f.(h1.n + c.(2*n)) - (f/*c).(2*n)) by A8
.= (h1").n*(f.(h1.n + c.n) - (f/*c).(2*n)) by VALUED_0:23
.= (h1").n*(f.((h1 + c).n) - (f/*c).(2*n)) by SEQ_1:7
.= (h1").n*((f/*(h1+c)).n - (f/*c).(2*n)) by A4,FUNCT_2:108
.= (h1").n*((f/*(h1+c)).n - f.(c.(2*n))) by A2,A3,FUNCT_2:108
.= (h1").n*((f/*(h1+c)).n - f.(c.n)) by VALUED_0:23
.= (h1").n*((f/*(h1+c)).n - (f/*c).n) by A2,A3,FUNCT_2:108
.= (h1").n*(f/*(h1+c) - f/*c).n by RFUNCT_2:1
.= (h1"(#)(f/*(h1+c) - f/*c)).n by SEQ_1:8;
end;
then h1"(#)(f/*(h1+c) - f/*c) is subsequence of d"(#)(f/*(d+c) - f/*c) by
FUNCT_2:63;
then lim (h1"(#)(f/*(h1+c) - f/*c)) = lim (d"(#) (f/*(d+c) - f/*c)) by A24,
SEQ_4:17;
hence thesis by A24,A20,SEQ_4:17;
end;
theorem Th4:
(for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n being Nat holds h.n>0
) holds h"(#)(f/*(h+c) - f/*c) is convergent) & {x0} c= dom f implies for h1,h2
,c st rng c ={x0} & rng (h1 + c)c= dom f & rng (h2 + c) c= dom f &
(for n being Nat holds
h1.n >0) & (for n being Nat holds h2.n >0)
holds lim (h1"(#)(f/*(h1+c) - f/*c)) = lim (h2
"(#)(f/*(h2+c) - f/*c))
proof
assume that
A1: for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n being Nat holds h.n>0)
holds h"(#)(f/*(h+c) - f/*c) is convergent and
A2: {x0} c= dom f;
let h1,h2,c such that
A3: rng c ={x0} and
A4: rng (h1 + c) c= dom f and
A5: rng (h2 + c) c= dom f and
A6: for n being Nat holds h1.n >0 and
A7: for n being Nat holds h2.n >0;
deffunc G(Element of NAT) = h2.$1;
deffunc F(Element of NAT) = h1.$1;
consider d such that
A8: for n holds d.(2*n)=F(n) & d.(2*n+1)=G(n) from SCHEME1:sch 2;
now
let n be Nat;
consider m such that
A9: n = 2*m or n = 2*m+1 by SCHEME1:1;
now
per cases by A9;
suppose
n = 2*m;
then d.n = h1.m by A8;
hence d.n<>0 by SEQ_1:5;
end;
suppose
n = 2*m+1;
then d.n = h2.m by A8;
hence d.n<>0 by SEQ_1:5;
end;
end;
hence d.n<>0;
end;
then
A10: d is non-zero by SEQ_1:5;
A11: h2 is convergent & lim h2 =0;
h1 is convergent & lim h1 =0;
then d is convergent & lim d =0 by A8,A11,FDIFF_2:1;
then reconsider d as 0-convergent non-zero Real_Sequence
by A10,FDIFF_1:def 1;
deffunc F(Nat) = 2*$1;
consider a such that
A12: for n being Nat holds a.n = F(n) from SEQ_1:sch 1;
deffunc G(Nat) = 2*$1+1;
consider b such that
A13: for n being Nat holds b.n = G(n) from SEQ_1:sch 1;
for n holds b.n = G(n) by A13;
then reconsider b as increasing sequence of NAT by FDIFF_2:3;
A14: rng (d+c) c= dom f
proof
let x be object;
assume x in rng (d+c);
then consider n such that
A15: x = (d+c).n by FUNCT_2:113;
consider m such that
A16: n=2*m or n=2*m+1 by SCHEME1:1;
now
per cases by A16;
suppose
n = 2*m;
then x = d.(2*m) + c.(2*m) by A15,SEQ_1:7
.= h1.m + c.(2*m) by A8
.= h1.m + c.m by VALUED_0:23
.= (h1+c).m by SEQ_1:7;
then x in rng(h1+c) by VALUED_0:28;
hence thesis by A4;
end;
suppose
n = 2*m+1;
then x = d.(2*m+1) + c.(2*m+1) by A15,SEQ_1:7
.= h2.m + c.(2*m+1) by A8
.= h2.m + c.m by VALUED_0:23
.= (h2 + c).m by SEQ_1:7;
then x in rng(h2+c) by VALUED_0:28;
hence thesis by A5;
end;
end;
hence thesis;
end;
now
let n;
thus ((d"(#)(f/*(d+c) - f/*c))*b).n = (d"(#) (f/*(d+c) - f/*c)).(b.n) by
FUNCT_2:15
.= (d"(#)(f/*(d+c) - f/*c)).(2*n+1) by A13
.= (d").(2*n+1) * (f/*(d+c) - f/*c).(2*n+1) by SEQ_1:8
.= (d.(2*n+1))" * (f/*(d+c) - f/*c).(2*n+1) by VALUED_1:10
.= (h2.n)" * (f/*(d+c) - f/*c).(2*n+1) by A8
.= (h2").n * (f/*(d+c) - f/*c).(2*n+1) by VALUED_1:10
.= (h2").n *((f/*(d+c)).(2*n+1) - (f/*c).(2*n+1)) by RFUNCT_2:1
.= (h2").n *(f.((d+c).(2*n+1)) - (f/*c).(2*n+1)) by A14,FUNCT_2:108
.= (h2").n *(f.((d+c).(2*n+1)) - f.(c.(2*n+1))) by A2,A3,FUNCT_2:108
.= (h2").n *(f.(d.(2*n+1)+c.(2*n+1)) - f.(c.(2*n+1))) by SEQ_1:7
.= (h2").n *(f.(h2.n+c.(2*n+1)) - f.(c.(2*n+1))) by A8
.= (h2").n *(f.(h2.n+c.(2*n+1)) - f.(c.n)) by VALUED_0:23
.= (h2").n *(f.(h2.n+c.n) - f.(c.n)) by VALUED_0:23
.= (h2").n *(f.((h2+c).n) - f.(c.n)) by SEQ_1:7
.= (h2").n *((f/*(h2+c)).n - f.(c.n)) by A5,FUNCT_2:108
.= (h2").n *((f/*(h2+c)).n - (f/*c).n) by A2,A3,FUNCT_2:108
.= (h2").n *(f/*(h2+c) - f/*c).n by RFUNCT_2:1
.= (h2"(#)(f/*(h2+c) - f/*c)).n by SEQ_1:8;
end;
then
A17: h2"(#)(f/*(h2+c) - f/*c) is subsequence of d"(#)(f/*(d+c) - f/*c) by
FUNCT_2:63;
for n being Nat holds d.n > 0
proof
let n be Nat;
consider m such that
A18: n = 2*m or n = 2*m+1 by SCHEME1:1;
now
per cases by A18;
suppose
n = 2*m;
then d.n = h1.m by A8;
hence thesis by A6;
end;
suppose
n = 2*m+1;
then d.n = h2.m by A8;
hence thesis by A7;
end;
end;
hence thesis;
end;
then
A19: d"(#)(f/*(d+c) - f/*c) is convergent by A1,A3,A14;
for n holds a.n = F(n) by A12;
then reconsider a as increasing sequence of NAT by FDIFF_2:2;
now
let n;
thus ((d"(#)(f/*(d+c) - f/*c))*a).n = (d"(#) (f/*(d+c) - f/*c)).(a.n) by
FUNCT_2:15
.= (d"(#)(f/*(d+c) - f/*c)).(2*n) by A12
.= (d").(2*n) * (f/*(d+c) - f/*c).(2*n) by SEQ_1:8
.= (d.(2*n))" * (f/*(d+c) - f/*c).(2*n) by VALUED_1:10
.= (h1.n)" * (f/*(d+c) - f/*c).(2*n) by A8
.= (h1").n * (f/*(d+c) - f/*c).(2*n) by VALUED_1:10
.= (h1").n *((f/*(d+c)).(2*n) - (f/*c).(2*n)) by RFUNCT_2:1
.= (h1").n *(f.((d+c).(2*n)) - (f/*c).(2*n)) by A14,FUNCT_2:108
.= (h1").n *(f.((d+c).(2*n)) - f.(c.(2*n))) by A2,A3,FUNCT_2:108
.= (h1").n *(f.(d.(2*n)+c.(2*n)) - f.(c.(2*n))) by SEQ_1:7
.= (h1").n *(f.(h1.n+c.(2*n)) - f.(c.(2*n))) by A8
.= (h1").n *(f.(h1.n+c.(2*n)) - f.(c.n)) by VALUED_0:23
.= (h1").n *(f.(h1.n+c.n) - f.(c.n)) by VALUED_0:23
.= (h1").n *(f.((h1+c).n) - f.(c.n)) by SEQ_1:7
.= (h1").n *((f/*(h1+c)).n - f.(c.n)) by A4,FUNCT_2:108
.= (h1").n *((f/*(h1+c)).n - (f/*c).n) by A2,A3,FUNCT_2:108
.= (h1").n *(f/*(h1+c) - f/*c).n by RFUNCT_2:1
.= (h1"(#)(f/*(h1+c) - f/*c)).n by SEQ_1:8;
end;
then h1"(#)(f/*(h1+c) - f/*c) is subsequence of d"(#)(f/*(d+c) - f/*c) by
FUNCT_2:63;
then lim (h1"(#)(f/*(h1+c) - f/*c)) = lim (d"(#) (f/*(d+c) -f/*c)) by A19,
SEQ_4:17;
hence thesis by A19,A17,SEQ_4:17;
end;
definition
let f,x0;
pred f is_Lcontinuous_in x0 means
x0 in dom f & for a st rng a c=
left_open_halfline(x0) /\ dom f & a is convergent & lim a = x0 holds f/*a is
convergent & f.x0 = lim(f/*a);
pred f is_Rcontinuous_in x0 means
x0 in dom f & for a st rng a c=
right_open_halfline(x0) /\ dom f & a is convergent & lim a = x0 holds f/*a is
convergent & f.x0 = lim(f/*a);
pred f is_right_differentiable_in x0 means
(ex r st r>0 & [.x0, x0+r
.] c= dom f) & for h,c st rng c ={x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n >
0) holds h"(#)(f/*(h+c) - f/*c) is convergent;
pred f is_left_differentiable_in x0 means
(ex r st r>0 & [.x0-r,x0.]
c= dom f) & for h,c st rng c ={x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n<0)
holds h"(#)(f/*(h+c) - f/*c) is convergent;
end;
theorem Th5:
f is_left_differentiable_in x0 implies f is_Lcontinuous_in x0
proof
assume
A1: f is_left_differentiable_in x0;
A2: for a st rng a c= left_open_halfline(x0) /\ dom f & a is convergent &
lim a = x0 holds f/*a is convergent & f.x0 = lim(f/*a)
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set b = seq_const x0;
let a such that
A3: rng a c= left_open_halfline(x0) /\ dom f and
A4: a is convergent and
A5: lim a = x0;
consider r such that
A6: 0 < r and
A7: [.x0 - r, x0.] c= dom f by A1;
consider n0 being Nat such that
A8: for k being Nat st k>=n0 holds x0 - r 0
proof
let n;
A21: d.n = a.n - b.n by A9;
a.n in rng a by VALUED_0:28;
then a.n in left_open_halfline(x0) by A3,XBOOLE_0:def 4;
then a.n in { r1: r1 < x0 } by XXREAL_1:229;
then
A22: ex r1 st r1 = a.n & r1 < x0;
then a.n - x0 < x0 - x0 by XREAL_1:9;
hence d.n < 0 by A21,SEQ_1:57;
thus thesis by A21,A22,SEQ_1:57;
end;
A23: for n being Nat holds (d^\n0).n < 0
proof
let n be Nat;
A24: n+n0 in NAT by ORDINAL1:def 12;
(d^\n0).n = d.(n + n0) by NAT_1:def 3;
hence thesis by A20,A24;
end;
for n being Nat holds (d^\n0).n <>0
by A23;
then d ^\n0 is non-zero by SEQ_1:5;
then reconsider h = d^\n0 as 0-convergent non-zero Real_Sequence
by A11,A19,FDIFF_1:def 1;
A25: rng a c= dom f
by A3,XBOOLE_0:def 4;
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=((a-b+b)^\n0).n by A10,SEQM_3:15
.= (a-b+b).(n+n0) by NAT_1:def 3
.= (a-b).(n+n0)+b.(n+n0) by SEQ_1:7
.= a.(n+n0)-b.(n+n0)+b.(n+n0) by RFUNCT_2:1
.= (a^\n0).n by NAT_1:def 3;
end;
then
A27: f/*(h+c)-f/*c+(f/*c)=f/*(a^\n0) by A26,FUNCT_2:63
.= (f/*a)^\n0 by A25,VALUED_0:27;
A28: for n holds (a^\n0).n in [.x0 - r,x0.]
proof
let n;
a.(n + n0) in rng a by VALUED_0:28;
then (a^\n0).n in rng a by NAT_1:def 3;
then (a^\n0).n in left_open_halfline(x0) by A3,XBOOLE_0:def 4;
then (a^\n0).n in {g:g < x0} by XXREAL_1:229;
then
A29: ex g st g = (a^\n0).n & g < x0;
0 <= n & 0 + n0 = n0;
then n0 <= n0 + n by XREAL_1:6;
then x0 - r <= a.(n + n0) by A8;
then x0 - r <= (a^\n0).n by NAT_1:def 3;
then (a^\n0).n in {g: x0 - r <= g & g <= x0} by A29;
hence thesis by RCOMP_1:def 1;
end;
rng (h + c) c= [.x0 - r,x0.]
proof
let x be object;
assume x in rng(h + c);
then consider n such that
A30: x = (h+c).n by FUNCT_2:113;
(h+c).n=((a - b +b)^\n0).n by A10,SEQM_3:15
.= (a - b + b) .(n + n0) by NAT_1:def 3
.= (a - b).(n + n0) + b.(n + n0) by SEQ_1:7
.= a.(n + n0) - b.(n + n0) + b.(n + n0) by RFUNCT_2:1
.= (a^\n0).n by NAT_1:def 3;
hence thesis by A28,A30;
end;
then rng (h + c) c= dom f by A7;
then
A31: h"(#)(f/*(h+c) - f/*c) is convergent by A1,A23,A12;
then
A32: lim (h(#)(h"(#)(f/*(h+c) - f/*c)))=0*lim(h"(#) (f/*(h+c) - f/*c)) by A19,
SEQ_2:15
.=0;
now
let n;
A33: h.n<>0 by A23;
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 A33,XCMPLX_0:def 7
.= (f/*(h+c) - f/*c).n;
end;
then
A34: h(#)(h"(#)(f/*(h+c) - f/*c))=f/*(h+c)-f/*c by FUNCT_2:63;
then
A35: f/*(h+c)-f/*c is convergent by A31;
then
A36: f/*(h+c)-f/*c+f/*c is convergent by A18;
hence f/*a is convergent by A27,SEQ_4:21;
lim(f/*c)=f.x0 by A15,A18,SEQ_2:def 7;
then lim(f/*(h+c)-f/*c+f/*c) = 0+f.x0 by A32,A34,A35,A18,SEQ_2:6
.= f.x0;
hence thesis by A36,A27,SEQ_4:22;
end;
x0 in dom f
proof
consider r such that
A37: 0 < r and
A38: [.x0 - r,x0.] c= dom f by A1;
x0 - r <= x0 by A37,XREAL_1:44;
then x0 in [.x0 - r,x0.] by XXREAL_1:1;
hence thesis by A38;
end;
hence thesis by A2;
end;
theorem Th6:
f is_Lcontinuous_in x0 & f.x0<>g2 & (ex r st r>0 & [.x0-r,x0.] c=
dom f) implies ex r1 st r1 > 0 & [.x0-r1,x0.] c= dom f & for g st g in [.x0-r1,
x0.] holds f.g <> g2
proof
assume that
A1: f is_Lcontinuous_in x0 and
A2: f.x0 <> g2;
given r such that
A3: r>0 and
A4: [.x0-r,x0.] c= dom f;
defpred P[Element of NAT,set] means $2 in [.x0-r/($1+1),x0.] & $2 in dom f &
f.$2 = g2;
assume
A5: for r1 st r1>0 & [.x0-r1,x0.] c= dom f ex g st g in [.x0-r1,x0.] & f
.g = g2;
A6: for n ex g be Element of REAL st P[n,g]
proof
let n;
x0 - r <= x0 by A3,XREAL_1:44;
then
A7: x0 in [.x0 - r,x0.] by XXREAL_1:1;
0 + 1 <= n + 1 by XREAL_1:7;
then r/(n+1) <= r/1 by A3,XREAL_1:118;
then
A8: x0 - r <= x0 - r/(n+1) by XREAL_1:13;
x0 - r/(n+1) <= x0 by A3,XREAL_1:44,139;
then x0 - r/(n+1) in {g1: x0 - r <= g1 & g1 <= x0} by A8;
then x0 - r/(n+1) in [.x0 - r, x0.] by RCOMP_1:def 1;
then [.x0 - r/(n+1),x0.] c= [.x0 - r,x0.] by A7,XXREAL_2:def 12;
then
A9: [.x0 - r/(n+1),x0.] c= dom f by A4;
then consider g such that
A10: g in [.x0-r/(n+1),x0.] & f.g = g2 by A3,A5,XREAL_1:139;
take g;
thus thesis by A9,A10;
end;
consider a such that
A11: for n holds P[n,a.n] from FUNCT_2:sch 3(A6);
A12: rng a c= left_open_halfline(x0) /\ dom f
proof
let x be object;
assume x in rng a;
then consider n such that
A13: x=a.n by FUNCT_2:113;
a.n in [.x0-r/(n+1),x0.] by A11;
then a.n in {g1: x0 - r/(n+1) <= g1 & g1 <= x0} by RCOMP_1:def 1;
then
A14: ex g1 st g1 = a.n & x0 - r/(n+1) <= g1 & g1 <=x0;
a.n <> x0 by A2,A11;
then a.n < x0 by A14,XXREAL_0:1;
then a.n in {g1: g1 < x0};
then
A15: a.n in left_open_halfline(x0) by XXREAL_1:229;
a.n in dom f by A11;
hence thesis by A13,A15,XBOOLE_0:def 4;
end;
A16: left_open_halfline(x0) /\ dom f c= dom f by XBOOLE_1:17;
A17: for n holds (f/*a).n = g2
proof
let n;
thus (f/*a).n = f.(a.n) by A12,A16,FUNCT_2:108,XBOOLE_1:1
.= g2 by A11;
end;
now
let n be Nat;
n in NAT by ORDINAL1:def 12;
then (f/*a).n = g2 by A17;
hence (f/*a).n =(f/*a).(n+1) by A17;
end;
then
A18: lim (f/*a) = (f/*a).0 by SEQ_4:26,VALUED_0:25
.= g2 by A17;
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
deffunc F(Nat) = x0 - r/($1+1);
consider b such that
A19: for n being Nat holds b.n = F(n) from SEQ_1:sch 1;
A20: now
let n be Nat;
A21: n in NAT by ORDINAL1:def 12;
a.n in [.x0 - r/(n+1), x0.] by A11,A21;
then a.n in {g1: x0 - r/(n+1) <= g1 & g1 <= x0} by RCOMP_1:def 1;
then ex g1 st g1 = a.n & x0 - r/(n+1) <= g1 & g1 <=x0;
hence b.n <= a.n & a.n <= d.n by A19,SEQ_1:57;
end;
A22: lim d = d.0 by SEQ_4:26
.= x0 by SEQ_1:57;
b is convergent & lim b = x0 by A19,FCONT_3:5;
then a is convergent & lim a = x0 by A22,A20,SEQ_2:19,20;
hence contradiction by A1,A2,A12,A18;
end;
theorem Th7:
f is_right_differentiable_in x0 implies f is_Rcontinuous_in x0
proof
assume
A1: f is_right_differentiable_in x0;
then consider r such that
A2: r>0 and
A3: [.x0,x0 + r.] c= dom f;
A4: for a st rng a c= right_open_halfline(x0) /\ dom f & a is convergent &
lim a = x0 holds f/*a is convergent & f.x0 = lim(f/*a)
proof
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set b = seq_const x0;
let a such that
A5: rng a c= right_open_halfline(x0) /\ dom f and
A6: a is convergent and
A7: lim a = x0;
consider r such that
A8: r > 0 and
A9: [.x0, x0 + r.] c= dom f by A1;
x0 + 0 < x0 + r by A8,XREAL_1:6;
then consider n0 be Nat such that
A10: for k being Nat st k>=n0 holds a.k < x0 +r by A6,A7,LIMFUNC2:2;
deffunc F(Nat) = a.$1-b.$1;
consider d such that
A11: for n being Nat holds d.n = F(n) from SEQ_1:sch 1;
A12: d = a - b by A11,RFUNCT_2:1;
then
A13: d is convergent by A6;
reconsider c = b^\n0 as constant Real_Sequence;
A14: rng c = {x0}
proof
thus rng c c= {x0}
proof
let x be object;
assume x in rng c;
then consider n such that
A15: x = (b^\n0).n by FUNCT_2:113;
x = b.(n + n0) by A15,NAT_1:def 3;
then x = x0 by SEQ_1:57;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {x0};
then
A16: x = x0 by TARSKI:def 1;
c.0 = b.(0 + n0) by NAT_1:def 3
.= x by A16,SEQ_1:57;
hence thesis by VALUED_0:28;
end;
A17: now
let g be Real such that
A18: 0 0 & d.n <> 0
proof
let n;
A23: d.n = a.n - b.n by A11;
a.n in rng a by VALUED_0:28;
then a.n in right_open_halfline(x0) by A5,XBOOLE_0:def 4;
then a.n in { r1: x0 < r1 } by XXREAL_1:230;
then
A24: ex r1 st r1 = a.n & x0 < r1;
then a.n - x0 > x0 - x0 by XREAL_1:9;
hence d.n > 0 by A23,SEQ_1:57;
thus thesis by A23,A24,SEQ_1:57;
end;
A25: for n being Nat holds (d^\n0).n > 0
proof
let n be Nat;
A26: n+n0 in NAT by ORDINAL1:def 12;
(d^\n0).n = d.(n + n0) by NAT_1:def 3;
hence thesis by A22,A26;
end;
for n being Nat holds (d^\n0).n <>0
by A25;
then d ^\n0 is non-zero by SEQ_1:5;
then reconsider h = d^\n0 as 0-convergent non-zero Real_Sequence
by A13,A21,FDIFF_1:def 1;
A27: rng a c= dom f
by A5,XBOOLE_0:def 4;
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
A28: f/*(h+c)-f/*c+(f/*c)=f/*(h+c) by FUNCT_2:63;
now
let n;
thus (h+c).n=((a-b+b)^\n0).n by A12,SEQM_3:15
.= (a-b+b).(n+n0) by NAT_1:def 3
.= (a-b).(n+n0)+b.(n+n0) by SEQ_1:7
.= a.(n+n0)-b.(n+n0)+b.(n+n0) by RFUNCT_2:1
.= (a^\n0).n by NAT_1:def 3;
end;
then
A29: f/*(h+c)-f/*c+(f/*c)=f/*(a^\n0) by A28,FUNCT_2:63
.= (f/*a)^\n0 by A27,VALUED_0:27;
A30: for n holds (a^\n0).n in [.x0, x0 + r.]
proof
let n;
a.(n + n0) in rng a by VALUED_0:28;
then (a^\n0).n in rng a by NAT_1:def 3;
then (a^\n0).n in right_open_halfline(x0) by A5,XBOOLE_0:def 4;
then (a^\n0).n in {g:x0 < g} by XXREAL_1:230;
then
A31: ex g st g = (a^\n0).n & x0 < g;
0 <= n & 0 + n0 = n0;
then n0 <= n0 + n by XREAL_1:6;
then a.(n + n0) <= x0 +r by A10;
then (a^\n0).n <= x0 + r by NAT_1:def 3;
then (a^\n0).n in {g: x0 <= g & g <= x0 + r} by A31;
hence thesis by RCOMP_1:def 1;
end;
rng (h + c) c= [.x0,x0 + r.]
proof
let x be object;
assume x in rng(h + c);
then consider n such that
A32: x = (h+c).n by FUNCT_2:113;
(h+c).n=((a - b +b)^\n0).n by A12,SEQM_3:15
.= (a - b + b) .(n + n0) by NAT_1:def 3
.= (a - b).(n + n0) + b.(n + n0) by SEQ_1:7
.= a.(n + n0) - b.(n + n0) + b.(n + n0) by RFUNCT_2:1
.= (a^\n0).n by NAT_1:def 3;
hence thesis by A30,A32;
end;
then rng (h + c) c= dom f by A9;
then
A33: h"(#)(f/*(h+c) - f/*c) is convergent by A1,A25,A14;
then
A34: 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;
A35: h.n<>0 by A25;
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 A35,XCMPLX_0:def 7
.= (f/*(h+c) - f/*c).n;
end;
then
A36: h(#)(h"(#)(f/*(h+c) - f/*c))=f/*(h+c)-f/*c by FUNCT_2:63;
then
A37: f/*(h+c)-f/*c is convergent by A33;
then
A38: f/*(h+c)-f/*c+f/*c is convergent by A20;
hence f/*a is convergent by A29,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 A34,A36,A37,A20,SEQ_2:6
.= f.x0;
hence thesis by A38,A29,SEQ_4:22;
end;
x0 + 0 <= x0 +r by A2,XREAL_1:7;
then x0 in [.x0, x0 + r.] by XXREAL_1:1;
hence thesis by A3,A4;
end;
theorem Th8:
f is_Rcontinuous_in x0 & f.x0 <> g2 & (ex r st r>0 & [.x0, x0+r.]
c= dom f) implies ex r1 st r1>0 & [.x0, x0+r1.] c= dom f & for g st g in [.x0,
x0+r1.] holds f.g <> g2
proof
assume that
A1: f is_Rcontinuous_in x0 and
A2: f.x0 <> g2;
given r such that
A3: r>0 and
A4: [.x0, x0+r.] c= dom f;
defpred P[Element of NAT,set] means $2 in [.x0, x0+r/($1+1).] & $2 in dom f
& f.$2 = g2;
assume
A5: for r1 st r1>0 & [.x0, x0+r1.] c= dom f ex g st g in [.x0, x0+r1.] &
f.g = g2;
A6: for n ex g be Element of REAL st P[n,g]
proof
let n;
x0 + 0 <= x0 +r by A3,XREAL_1:7;
then
A7: x0 in [.x0, x0 + r.] by XXREAL_1:1;
0 + 1 <= n + 1 by XREAL_1:7;
then r/(n+1) <= r/1 by A3,XREAL_1:118;
then
A8: x0 + r/(n+1) <= x0 + r by XREAL_1:7;
x0 + 0 =x0;
then x0 <= x0 + r/(n+1) by A3,XREAL_1:7;
then x0 + r/(n+1) in {g1:x0 <= g1 & g1 <= x0+r} by A8;
then x0 +r/(n+1) in [.x0,x0+r.] by RCOMP_1:def 1;
then [.x0,x0+r/(n+1).] c= [.x0,x0+r.] by A7,XXREAL_2:def 12;
then
A9: [.x0,x0+r/(n+1).] c= dom f by A4;
then consider g such that
A10: g in [.x0,x0+r/(n+1).] & f.g = g2 by A3,A5,XREAL_1:139;
take g;
thus thesis by A9,A10;
end;
consider a such that
A11: for n holds P[n,a.n] from FUNCT_2:sch 3(A6);
A12: rng a c= right_open_halfline(x0) /\ dom f
proof
let x be object;
assume x in rng a;
then consider n such that
A13: x = a.n by FUNCT_2:113;
a.n in [.x0, x0 + r/(n+1).] by A11;
then a.n in{g1: x0<=g1 & g1<=x0+ r/(n+1)} by RCOMP_1:def 1;
then
A14: ex g1 st g1=a.n & x0<=g1 & g1<=x0+ r/(n+1);
x0 <> a.n by A2,A11;
then x0 < a.n by A14,XXREAL_0:1;
then a.n in {g1:x0 Real means
: Def5:
for h,c st rng c = {x0} & rng (h + c) c= dom f &
(for n being Nat holds h.n <0) holds it =lim (h"(#)(f/*(h+c) - f/*c));
existence
proof
A2: {x0} c= dom f
proof
let x be object;
assume x in {x0};
then
A3: x = x0 by TARSKI:def 1;
consider r such that
A4: r > 0 and
A5: [.x0 - r,x0.] c= dom f by A1;
x0 - r <= x0 by A4,XREAL_1:44;
then x0 in [.x0 - r,x0.] by XXREAL_1:1;
hence thesis by A3,A5;
end;
A6: for h,c st rng c = {x0} & rng (h + c) c= dom f &
(for n being Nat holds h.n <0)
holds h"(#)(f/*(h+c) - f/*c) is convergent by A1;
ex r st r > 0 & [.x0 - r, x0.] c= dom f by A1;
then consider h1,c1 such that
A7: rng c1 = {x0} and
A8: rng (h1 + c1) c= dom f & for n being Nat holds h1.n < 0 by Th1;
take lim (h1"(#)(f/*(h1+c1) - f/*c1));
let h,c such that
A9: rng c = {x0} and
A10: rng (h + c) c= dom f & for n being Nat holds h.n <0;
c1 = c by A7,A9,FDIFF_2:5;
hence thesis by A7,A8,A2,A10,A6,Th3;
end;
uniqueness
proof
ex r st r > 0 & [.x0 - r, x0.] c= dom f by A1;
then consider h,c such that
A11: rng c = {x0} & rng (h + c) c= dom f &
for n being Nat holds h.n < 0 by Th1;
let g1,g2 being Real such that
A12: for h,c st rng c = {x0} & rng (h + c) c= dom f &
(for n being Nat holds h.n
<0) holds g1=lim (h"(#)(f/*(h+c) - f/*c)) and
A13: for h,c st rng c = {x0} & rng (h + c) c= dom f &
(for n being Nat holds h.n
< 0) holds g2=lim (h"(#)(f/*(h+c) - f/*c));
g1 = lim (h"(#)(f/*(h+c) - f/*c)) by A12,A11;
hence thesis by A13,A11;
end;
end;
definition
let x0,f;
assume
A1: f is_right_differentiable_in x0;
func Rdiff(f,x0) -> Real means
:Def6:
for h,c st rng c = {x0} & rng (h+c) c=
dom f & (for n being Nat holds h.n > 0)
holds it=lim (h"(#)(f/*(h+c) - f/*c));
existence
proof
A2: {x0} c= dom f
proof
let x be object;
assume x in {x0};
then
A3: x = x0 by TARSKI:def 1;
consider r such that
A4: r>0 and
A5: [.x0,x0+r.] c= dom f by A1;
x0 + 0 <= x0 + r by A4,XREAL_1:7;
then x0 in [.x0,x0+r.] by XXREAL_1:1;
hence thesis by A3,A5;
end;
A6: for h,c st rng c = {x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n>0)
holds h"(#)(f/*(h+c) - f/*c) is convergent by A1;
ex r st r>0 & [.x0,x0+r.] c=dom f by A1;
then consider h,c such that
A7: rng c = {x0} and
A8: rng (h+c) c= dom f & for n being Nat holds h.n>0 by Th2;
take lim(h"(#)(f/*(h+c) - f/*c));
let h1,c1 such that
A9: rng c1 ={x0} and
A10: rng(h1 + c1) c=dom f & for n being Nat holds h1.n>0;
c1 = c by A7,A9,FDIFF_2:5;
hence thesis by A7,A8,A10,A6,A2,Th4;
end;
uniqueness
proof
ex r st r>0 & [.x0,x0 + r.] c=dom f by A1;
then consider h,c such that
A11: rng c ={x0} & rng (h+c) c= dom f &
for n being Nat holds h.n >0 by Th2;
let g1,g2 being Real such that
A12: for h,c st rng c ={x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n >
0) holds g1=lim (h"(#)(f/*(h+c) - f/*c)) and
A13: for h,c st rng c ={x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n >
0) holds g2=lim (h"(#)(f/*(h+c) - f/*c));
g1 = lim (h"(#)(f/*(h+c) - f/*c)) by A12,A11;
hence thesis by A13,A11;
end;
end;
theorem Th9:
for g being Real holds
f is_left_differentiable_in x0 & Ldiff(f,x0) = g iff (ex r st 0 <
r & [.x0 -r,x0.] c= dom f) & for h,c st rng c = {x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n < 0)
holds h"(#)(f/*(h+c) - f/*c) is convergent & lim(h"(#)(f/*(h+c) - f/*c)) = g
proof let g be Real;
thus f is_left_differentiable_in x0 & Ldiff(f,x0) = g implies (ex r st 0 < r
& [.x0 -r,x0.] c= dom f) & for h,c st rng c = {x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n < 0)
holds h"(#)(f/*(h+c) - f/*c) is convergent & lim(h"(#)(f/*(h+c
) - f/*c)) = g by Def5;
thus (ex r st 0 0 by A18;
thus (h(#)(h"(#)(f1/*(h+c) - f1/*c))).n = ((h(#)h")(#) (f1/*(h+c) - f1/*
c)).n by SEQ_1:14
.= (h(#)h").n *(f1/*(h+c) - f1/*c).n by SEQ_1:8
.= h.n * (h").n *(f1/*(h+c) - f1/*c).n by SEQ_1:8
.= h.n * (h.n)" *(f1/*(h+c) - f1/*c).n by VALUED_1:10
.= 1*(f1/*(h+c) - f1/*c).n by A46,XCMPLX_0:def 7
.= (f1/*(h+c) - f1/*c).n;
end;
then
A47: h(#)(h"(#)(f1/*(h+c) - f1/*c)) = (f1/*(h+c) - f1/*c) by FUNCT_2:63;
h(#)(h"(#)(f1/*(h+c) - f1/*c)) is convergent by A37;
then
A48: f1/*(h+c) is convergent by A28,A47,A20;
lim(f1/*c) = f1.x0 by A25,A28,SEQ_2:def 7;
then
A49: 0 = lim (f1/*(h+c)) - f1.x0 by A28,A47,A48,A38,SEQ_2:12;
A50: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A16,A18,A39;
then
A51: h"(#) (f2/*(h+c) - f2/*c)(#) (f1/*(h+c)) is convergent by A48;
lim (h"(#)((f1(#)f2)/*(h+c) - (f1(#)f2)/*c)) = lim (h"(#) (f2/*(h+c)
- f2/*c)(#)(f1/*(h+c)) + h"(#) (f1/*(h+c) - f1/*c)(#) (f2/*c)) by A44,
FUNCT_2:63
.= lim (h"(#) (f2/*(h+c) - f2/*c)(#)(f1/*(h+c))) + lim (h"(#) (f1/*(h+
c) - f1/*c)(#)(f2/*c)) by A51,A42,SEQ_2:6
.= lim (h"(#) (f2/*(h+c) - f2/*c))*lim(f1/*(h+c)) + lim (h"(#) (f1/*(h
+c) - f1/*c)(#)(f2/*c)) by A50,A48,SEQ_2:15
.= lim (h"(#) (f2/*(h+c) - f2/*c))* f1.x0 + lim (h"(#) (f1/*(h+c) - f1
/*c))*lim(f2/*c) by A41,A49,A34,SEQ_2:15
.= Ldiff(f1,x0) * f2.x0 + Ldiff(f2,x0) * f1.x0 by A36,A40,A31,A34,
SEQ_2:def 7;
hence thesis by A51,A42,A45;
end;
[.x0 - r,x0.] c= dom f1 /\ dom f2 by A14,A11,XBOOLE_1:19;
then [.x0 - r,x0.] c= dom (f1(#)f2) by VALUED_1:def 4;
hence thesis by A7,A15,Th9;
end;
Lm1: f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & (ex
r0 st r0 > 0 & for g st g in dom f2 & g in [.x0 - r0,x0.] holds f2.g <> 0)
implies f1/f2 is_left_differentiable_in x0 & Ldiff(f1/f2,x0) = (Ldiff(f1,x0)*f2
.x0 - Ldiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_left_differentiable_in x0;
consider r1 such that
A3: 0 < r1 and
A4: [.x0 -r1,x0.] c= dom f1 by A1;
given r0 such that
A5: r0 > 0 and
A6: for g st g in dom f2 & g in [.x0 - r0,x0.] holds f2.g <> 0;
consider r2 such that
A7: 0 < r2 and
A8: [.x0 -r2,x0.] c= dom f2 by A2;
set r3 = min(r0,r2);
A9: 0 < r3 by A5,A7,XXREAL_0:15;
then
A10: x0 - r3 <= x0 by XREAL_1:43;
r3 <= r2 by XXREAL_0:17;
then
A11: x0 - r2 <= x0 - r3 by XREAL_1:13;
then x0 - r2 <= x0 by A10,XXREAL_0:2;
then
A12: x0 in [.x0 - r2,x0.] by XXREAL_1:1;
x0 - r3 in { g: x0 - r2 <= g & g <= x0 } by A10,A11;
then x0 - r3 in [.x0 - r2,x0.] by RCOMP_1:def 1;
then [.x0 - r3,x0.] c= [.x0 - r2,x0.] by A12,XXREAL_2:def 12;
then
A13: [.x0 - r3,x0.] c= dom f2 by A8;
r3 <= r0 by XXREAL_0:17;
then
A14: x0 - r0 <= x0 - r3 by XREAL_1:13;
then x0 - r0 <= x0 by A10,XXREAL_0:2;
then
A15: x0 in [.x0 - r0,x0.] by XXREAL_1:1;
x0 - r3 in { g: x0 - r0 <= g & g <= x0 } by A10,A14;
then x0 - r3 in [.x0 - r0,x0.] by RCOMP_1:def 1;
then
A16: [.x0 - r3,x0.] c= [.x0 - r0,x0.] by A15,XXREAL_2:def 12;
set r = min(r1,r3);
A17: 0 < r by A3,A9,XXREAL_0:15;
then
A18: x0 - r <= x0 by XREAL_1:43;
r <= r3 by XXREAL_0:17;
then
A19: x0 - r3 <= x0 - r by XREAL_1:13;
then x0 - r3 <= x0 by A18,XXREAL_0:2;
then
A20: x0 in [.x0 - r3,x0.] by XXREAL_1:1;
x0 - r in { g: x0 - r3 <= g & g <= x0 } by A18,A19;
then x0 - r in [.x0 - r3,x0.] by RCOMP_1:def 1;
then
A21: [.x0 - r,x0.] c= [.x0 - r3,x0.] by A20,XXREAL_2:def 12;
[.x0 - r,x0.] c= dom(f2^)
proof
assume not thesis;
then consider x being object such that
A22: x in [.x0 - r,x0.] and
A23: not x in dom (f2^);
reconsider x as Real by A22;
A24: x in [.x0 - r3,x0.] by A21,A22;
A25: not x in dom f2 \ f2"{0} by A23,RFUNCT_1:def 2;
now
per cases by A25,XBOOLE_0:def 5;
suppose
not x in dom f2;
hence contradiction by A13,A24;
end;
suppose
A26: x in f2"{0};
then f2.x in {0} by FUNCT_1:def 7;
then
A27: f2.x = 0 by TARSKI:def 1;
x in dom f2 by A26,FUNCT_1:def 7;
hence contradiction by A6,A16,A24,A27;
end;
end;
hence contradiction;
end;
then
A28: [.x0 - r,x0.] c= dom f2\f2"{0} by RFUNCT_1:def 2;
r <= r1 by XXREAL_0:17;
then
A29: x0 - r1 <= x0 - r by XREAL_1:13;
then x0 - r1 <= x0 by A18,XXREAL_0:2;
then
A30: x0 in [.x0 - r1,x0.] by XXREAL_1:1;
x0 - r in { g: x0 - r1 <= g & g <= x0 } by A18,A29;
then x0 - r in [.x0 - r1,x0.] by RCOMP_1:def 1;
then [.x0 - r,x0.] c= [.x0 - r1,x0.] by A30,XXREAL_2:def 12;
then
A31: [.x0 - r,x0.] c= dom f1 by A4;
A32: for h,c st rng c = {x0} & rng (h+c) c= dom (f1/f2) &
(for n being Nat holds h.n <
0) holds h"(#)((f1/f2)/*(h+c) - (f1/f2)/*c) is convergent & lim(h"(#)((f1/f2)/*
(h+c) - (f1/f2)/*c)) = (Ldiff(f1,x0)*f2.x0 - Ldiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
let h,c;
assume that
A33: rng c = {x0} and
A34: rng (h+c) c= dom (f1/f2) and
A35: for n being Nat holds h.n < 0;
A36: rng (h + c) c= dom f1 /\ (dom f2\f2"{0}) by A34,RFUNCT_1:def 1;
0 <= r by A3,A9,XXREAL_0:15;
then x0 - r <= x0 by XREAL_1:43;
then
A37: x0 in [.x0 -r,x0.] by XXREAL_1:1;
then
A38: x0 in dom f1 by A31;
A39: rng c c= dom f1
by A33,A38,TARSKI:def 1;
dom f1 /\ (dom f2\f2"{0}) c= dom f1 by XBOOLE_1:17;
then
A40: rng (h + c) c= dom f1 by A36;
then
A41: lim(h"(#)(f1/*(h+c) - f1/*c)) = Ldiff(f1,x0) by A1,A33,A35,Th9;
A42: x0 in (dom f2\f2"{0}) by A28,A37;
rng c c= dom f2\f2"{0}
by A33,A42,TARSKI:def 1;
then
A43: rng c c= dom (f2^) by RFUNCT_1:def 2;
then
A44: rng c c= dom f1 /\ dom (f2^) by A39,XBOOLE_1:19;
A45: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A33,A35,A40;
A46: f2/*c is non-zero by A43,RFUNCT_2:11;
A47: now
let n;
thus (h"(#)((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c)))).n = (h").n *
((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c))).n by SEQ_1:8
.= (h").n * (((f1/*(h+c))(#)(f2/*c)).n - ((f1/*c)(#) (f2/*(h+c))).n)
by RFUNCT_2:1
.= (h").n * ((f1/*(h+c)).n * (f2/*c).n - ((f1/*c)(#)(f2/*(h+c))).n)
by SEQ_1:8
.= (h").n * (((f1/*(h+c)).n - (f1/*c).n) * (f2/*c).n + ((f1/*c).n*(
f2/*c).n) - ((f1/*c).n * (f2/*(h+c)).n)) by SEQ_1:8
.= (h").n * ((f1/*(h+c)).n - (f1/*c).n) * (f2/*c).n - (f1/*c).n * ((
h").n * ((f2/*(h+c)).n - (f2/*c).n))
.= (h").n * ((f1/*(h+c)) - (f1/*c)).n * (f2/*c).n - (f1/*c).n * ((h"
).n * ((f2/*(h+c)).n - (f2/*c).n)) by RFUNCT_2:1
.= (h").n * (f1/*(h+c) - (f1/*c)).n * (f2/*c).n - (f1/*c).n * ((h").
n * (f2/*(h+c) - (f2/*c)).n) by RFUNCT_2:1
.= (h" (#) (f1/*(h+c) - (f1/*c))).n * (f2/*c).n - (f1/*c).n * ((h").
n * (f2/*(h+c) - (f2/*c)).n) by SEQ_1:8
.= (h"(#)(f1/*(h+c) - (f1/*c))).n * (f2/*c).n - (f1/*c).n * (h"(#)(
f2/*(h+c) - (f2/*c))).n by SEQ_1:8
.= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c)).n - (f1/*c).n * (h"(#)(f2
/*(h+c) - (f2/*c))).n by SEQ_1:8
.= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c)).n - ((f1/*c)(#)(h"(#)(f2/*
(h+c)-(f2/*c)))).n by SEQ_1:8
.= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+
c)-(f2/*c)))).n by RFUNCT_2:1;
end;
now
let n;
thus (f2/*c + (f2/*(h+c) - f2/*c)).n = (f2/*c).n + (f2/*(h+c) - f2/*c).n
by SEQ_1:7
.= (f2/*c).n + ((f2/*(h+c)).n - (f2/*c).n) by RFUNCT_2:1
.= (f2/*(h+c)).n;
end;
then
A48: f2/*c + (f2/*(h+c) - f2/*c) = f2/*(h+c) by FUNCT_2:63;
dom f1 /\ (dom f2\f2"{0}) c=(dom f2\f2"{0}) by XBOOLE_1:17;
then
A49: rng (h + c) c= (dom f2\f2"{0}) by A36;
then
A50: rng (h + c) c= dom (f2^) by RFUNCT_1:def 2;
then
A51: rng (h + c) c= dom f1 /\ dom (f2^) by A40,XBOOLE_1:19;
A52: f2/*(h+c) is non-zero by A50,RFUNCT_2:11;
then
A53: (f2/*(h+c)) (#) (f2/*c) is non-zero by A46,SEQ_1:35;
h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c)=h"(#)((f1(#) (f2^))/*(h+c) - (f1
/f2)/*c) by RFUNCT_1:31
.=h"(#)((f1(#)(f2^))/*(h+c) - (f1(#)(f2^))/*c) by RFUNCT_1:31
.=h"(#)((f1/*(h+c))(#)((f2^)/*(h+c)) - (f1(#) (f2^))/*c) by A51,
RFUNCT_2:8
.=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1(#)(f2^))/*c) by A50,RFUNCT_2:12
.=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1/*c)(#) ((f2^)/*c)) by A44,
RFUNCT_2:8
.=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1/*c)/"(f2/*c)) by A43,RFUNCT_2:12
.=h"(#)(((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c)))/"((f2/*(h+c))
(#) (f2/*c))) by A52,A46,SEQ_1:50
.=(h"(#)((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c))))/"((f2/*(h+c))
(#) (f2/*c)) by SEQ_1:41;
then
A54: h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c) =((h"(#)(f1/*(h+c) - (f1/*c)) )
(#) (f2/*c) - (f1/*c)(#)(h"(#)(f2/*(h+c)-(f2/*c))))/"(f2/*(h+c)(#) (f2/*c)) by
A47,FUNCT_2:63;
dom f2 \ f2"{0} c= dom f2 by XBOOLE_1:36;
then
A55: rng (h + c) c= dom f2 by A49;
then
A56: lim(h"(#)(f2/*(h+c) - f2/*c)) = Ldiff(f2,x0) by A2,A33,A35,Th9;
A57: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A33,A35,A55;
now
let n;
A58: h.n <> 0 by A35;
thus (h(#)(h"(#)(f2/*(h+c) - f2/*c))).n = ((h(#)h")(#)(f2/*(h+c) - f2/*c
)). n by SEQ_1:14
.= (h(#)h").n *(f2/*(h+c) - f2/*c).n by SEQ_1:8
.= h.n * (h").n *(f2/*(h+c) - f2/*c).n by SEQ_1:8
.= h.n * (h.n)" *(f2/*(h+c) - f2/*c).n by VALUED_1:10
.= 1*(f2/*(h+c) - f2/*c).n by A58,XCMPLX_0:def 7
.= (f2/*(h+c) - f2/*c).n;
end;
then
A59: h(#)(h"(#)(f2/*(h+c) - f2/*c)) = (f2/*(h+c) - f2/*c) by FUNCT_2:63;
A60: for m holds c.m = x0
proof
let m;
c.m in rng c by VALUED_0:28;
hence thesis by A33,TARSKI:def 1;
end;
A61: for g be Real st 0 < g
ex n being Nat st for m being Nat st n <=m
holds |.(f1/*c).m - f1.x0.| < g
proof
let g be Real such that
A62: 0 < g;
take n = 0;
let m being Nat such that
n <= m;
A63: m in NAT by ORDINAL1:def 12;
|.(f1/*c).m - f1.x0.| = |.f1.(c.m) - f1.x0.| by A39,FUNCT_2:108,A63
.=|.f1.x0-f1.x0.| by A60,A63
.= 0 by ABSVALUE:def 1;
hence thesis by A62;
end;
then
A64: f1/*c is convergent by SEQ_2:def 6;
then
A65: lim(f1/*c) = f1.x0 by A61,SEQ_2:def 7;
dom (f2^) = dom f2 \ f2"{0} by RFUNCT_1:def 2;
then
A66: dom (f2^) c= dom f2 by XBOOLE_1:36;
A67: for g be Real st 0 < g
ex n being Nat st for m being Nat st n <=m holds |.(f2/*
c).m - f2.x0.| < g
proof
let g be Real such that
A68: 0 < g;
take n = 0;
let m being Nat such that
n <= m;
A69: m in NAT by ORDINAL1:def 12;
|.(f2/*c).m - f2.x0.| = |.f2.(c.m) - f2.x0.| by A43,A66,FUNCT_2:108
,XBOOLE_1:1,A69
.=|.f2.x0 - f2.x0.| by A60,A69
.= 0 by ABSVALUE:def 1;
hence thesis by A68;
end;
then
A70: f2/*c is convergent by SEQ_2:def 6;
then
A71: lim(f2/*c) = f2.x0 by A67,SEQ_2:def 7;
h(#)(h"(#)(f2/*(h+c) - f2/*c)) is convergent by A57;
then
A72: f2/*(h+c) is convergent by A70,A59,A48;
then
A73: f2/*(h+c) (#) (f2/*c) is convergent by A70;
h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A33,A35,A55;
then lim (h(#)(h"(#)(f2/*(h+c) - f2/*c))) = lim h *lim (h"(#)(f2/*(h+c) -
f2/* c ) ) by SEQ_2:15
.= 0;
then 0 = lim (f2/*(h+c)) - f2.x0 by A70,A71,A59,A72,SEQ_2:12;
then
A74: lim(f2/*(h+c) (#) (f2/*c)) = (f2.x0)^2 by A70,A71,A72,SEQ_2:15;
A75: lim(f2/*(h+c) (#) (f2/*c))<> 0
proof
assume not thesis;
then f2.x0 = 0 by A74,XCMPLX_1:6;
hence contradiction by A6,A8,A15,A12;
end;
h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A33,A35,A40;
then
A76: h"(#) (f1/*(h+c) - f1/*c)(#)(f2/*c) is convergent by A70;
A77: (f1/*c)(#)(h"(#) (f2/*(h+c) - f2/*c)) is convergent by A57,A64;
then
A78: ((h"(#)(f1/*(h+c) - (f1/*c)))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+c
)-(f2/*c)))) is convergent by A76;
then lim(h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c)) = lim((h"(#)(f1/*(h+c) - (
f1/*c)))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+c)-(f2/*c))))/ lim(f2/*(h+c)(#)(
f2/*c)) by A53,A73,A75,A54,SEQ_2:24
.=(lim((h"(#)(f1/*(h+c)-(f1/*c)))(#)(f2/*c))-lim((f1/*c)(#)(h"(#)(f2/*
(h+c)- (f2/*c)))))/lim(f2/*(h+c)(#)(f2/*c)) by A77,A76,SEQ_2:12
.=( lim(h"(#)(f1/*(h+c)-(f1/*c)))*lim(f2/*c) - lim((f1/*c) (#) (h"(#)(
f2/*(h+c)-(f2/*c)))) ) / lim(f2/*(h+c)(#)(f2/*c)) by A45,A70,SEQ_2:15
.=(Ldiff(f1,x0) * f2.x0 - Ldiff(f2,x0) * f1.x0)/(f2.x0)^2 by A41,A57,A56
,A64,A65,A71,A74,SEQ_2:15;
hence thesis by A53,A73,A75,A78,A54,SEQ_2:23;
end;
[.x0 - r,x0.] c= dom f1 /\ (dom f2\f2"{0}) by A31,A28,XBOOLE_1:19;
then [.x0 - r,x0.] c= dom (f1/f2) by RFUNCT_1:def 1;
hence thesis by A17,A32,Th9;
end;
theorem
f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & f2
.x0 <> 0 implies f1/f2 is_left_differentiable_in x0 & Ldiff(f1/f2,x0) = (Ldiff(
f1,x0)*f2.x0 - Ldiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_left_differentiable_in x0 and
A3: f2.x0 <> 0;
consider r1 such that
A4: r1 > 0 and
[.x0-r1,x0.] c= dom f2 and
A5: for g st g in [.x0-r1,x0.] holds f2.g <> 0 by A2,A3,Th5,Th6;
now
take r1;
thus r1 > 0 by A4;
let g;
assume that
g in dom f2 and
A6: g in [.x0 - r1,x0.];
thus f2.g <> 0 by A5,A6;
end;
hence thesis by A1,A2,Lm1;
end;
Lm2: f is_left_differentiable_in x0 & (ex r0 st r0 > 0 & for g st g in dom f &
g in [.x0 - r0,x0.] holds f.g <> 0) implies f^ is_left_differentiable_in x0 &
Ldiff(f^,x0) = - Ldiff(f,x0)/(f.x0)^2
proof
assume
A1: f is_left_differentiable_in x0;
then consider r2 such that
A2: 0 < r2 and
A3: [.x0 -r2,x0.] c= dom f;
given r0 such that
A4: r0 > 0 and
A5: for g st g in dom f & g in [.x0 - r0,x0.] holds f.g <> 0;
set r3 = min(r0,r2);
A6: 0 < r3 by A4,A2,XXREAL_0:15;
then
A7: x0 - r3 <= x0 by XREAL_1:43;
r3 <= r2 by XXREAL_0:17;
then
A8: x0 - r2 <= x0 - r3 by XREAL_1:13;
then x0 - r2 <= x0 by A7,XXREAL_0:2;
then
A9: x0 in [.x0 - r2,x0.] by XXREAL_1:1;
x0 - r3 in { g: x0 - r2 <= g & g <= x0 } by A7,A8;
then x0 - r3 in [.x0 - r2,x0.] by RCOMP_1:def 1;
then [.x0 - r3,x0.] c= [.x0 - r2,x0.] by A9,XXREAL_2:def 12;
then
A10: [.x0 - r3,x0.] c= dom f by A3;
r3 <= r0 by XXREAL_0:17;
then
A11: x0 - r0 <= x0 - r3 by XREAL_1:13;
then x0 - r0 <= x0 by A7,XXREAL_0:2;
then
A12: x0 in [.x0 - r0,x0.] by XXREAL_1:1;
x0 - r3 in { g: x0 - r0 <= g & g <= x0 } by A7,A11;
then x0 - r3 in [.x0 - r0,x0.] by RCOMP_1:def 1;
then
A13: [.x0 - r3,x0.] c= [.x0 - r0,x0.] by A12,XXREAL_2:def 12;
A14: [.x0 - r3,x0.] c= dom(f^)
proof
assume not thesis;
then consider x being object such that
A15: x in [.x0 - r3,x0.] and
A16: not x in dom (f^);
reconsider x as Real by A15;
A17: not x in dom f \ f"{0} by A16,RFUNCT_1:def 2;
now
per cases by A17,XBOOLE_0:def 5;
suppose
not x in dom f;
hence contradiction by A10,A15;
end;
suppose
A18: x in f"{0};
then f.x in {0} by FUNCT_1:def 7;
then
A19: f.x = 0 by TARSKI:def 1;
x in dom f by A18,FUNCT_1:def 7;
hence contradiction by A5,A13,A15,A19;
end;
end;
hence contradiction;
end;
A20: x0 in [.x0 - r3,x0.] by A7,XXREAL_1:1;
for h,c st rng c = {x0} & rng (h+c) c= dom (f^) &
(for n being Nat holds h.n < 0)
holds h"(#)((f^)/*(h+c) - (f^)/*c) is convergent & lim(h"(#)((f^)/*(h+c) - (f^)
/*c)) = - Ldiff(f,x0)/(f.x0)^2
proof
let h,c;
assume that
A21: rng c = {x0} and
A22: rng (h+c) c= dom (f^) and
A23: for n being Nat holds h.n < 0;
A24: for m holds c.m = x0
proof
let m;
c.m in rng c by VALUED_0:28;
hence thesis by A21,TARSKI:def 1;
end;
A25: dom f \ f"{0} c= dom f by XBOOLE_1:36;
rng (h + c) c= dom f\f"{0} by A22,RFUNCT_1:def 2;
then
A26: rng (h + c) c= dom f by A25;
then
A27: lim(h"(#)(f/*(h+c) - f/*c)) = Ldiff(f,x0) by A1,A21,A23,Th9;
A28: h"(#)(f/*(h+c) - f/*c) is convergent by A1,A21,A23,A26;
then
A29: -(h"(#)((f/*(h+c)) - (f/*c))) is convergent;
x0 in dom (f^) by A20,A14;
then
A30: x0 in (dom f\f"{0}) by RFUNCT_1:def 2;
rng c c= dom f\f"{0}
by A21,A30,TARSKI:def 1;
then
A31: rng c c= dom (f^) by RFUNCT_1:def 2;
then
A32: f/*c is non-zero by RFUNCT_2:11;
now
let n;
A33: h.n <> 0 by A23;
thus (h(#)(h"(#)(f/*(h+c) - f/*c))).n = ((h(#)h")(#) (f/*(h+c) - f/*c)).
n by SEQ_1:14
.= (h(#)h").n *(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
.= 1*(f/*(h+c) - f/*c).n by A33,XCMPLX_0:def 7
.= (f/*(h+c) - f/*c).n;
end;
then
A34: h(#)(h"(#)(f/*(h+c) - f/*c)) = (f/*(h+c) - f/*c) by FUNCT_2:63;
A35: f/*(h+c) is non-zero by A22,RFUNCT_2:11;
then
A36: (f/*(h+c)) (#) (f/*c) is non-zero by A32,SEQ_1:35;
now
let n;
thus (f/*c + (f/*(h+c) - f/*c)).n = (f/*c).n + (f/*(h+c) - f/*c).n by
SEQ_1:7
.= (f/*c).n + ((f/*(h+c)).n - (f/*c).n) by RFUNCT_2:1
.= (f/*(h+c)).n;
end;
then
A37: f/*c + (f/*(h+c) - f/*c) = f/*(h+c) by FUNCT_2:63;
dom (f^) = dom f \ f"{0} by RFUNCT_1:def 2;
then
A38: dom (f^) c= dom f by XBOOLE_1:36;
A39: for g be Real st 0 < g
ex n being Nat st for m being Nat st n <=m holds |.(f/*c)
.m - f.x0.| < g
proof
let g be Real such that
A40: 0 < g;
take n = 0;
let m being Nat such that
n <= m;
A41: m in NAT by ORDINAL1:def 12;
|.(f/*c).m - f.x0.| = |.f.(c.m) - f.x0.| by A31,A38,FUNCT_2:108
,XBOOLE_1:1,A41
.=|.f.x0 - f.x0.| by A24,A41
.= 0 by ABSVALUE:def 1;
hence thesis by A40;
end;
then
A42: f/*c is convergent by SEQ_2:def 6;
then
A43: lim(f/*c) = f.x0 by A39,SEQ_2:def 7;
h(#)(h"(#)(f/*(h+c) - f/*c)) is convergent by A28;
then
A44: f/*(h+c) is convergent by A42,A34,A37;
lim (h(#)(h"(#)(f/*(h+c) - f/*c))) = lim h *lim (h"(#)(f/*(h+c) - f/*
c ) ) by A28,SEQ_2:15
.= 0;
then 0 = lim (f/*(h+c)) - f.x0 by A42,A43,A34,A44,SEQ_2:12;
then
A45: lim(f/*(h+c) (#) (f/*c)) =(f.x0)^2 by A42,A43,A44,SEQ_2:15;
A46: lim(f/*(h+c) (#) (f/*c))<> 0
proof
assume not thesis;
then f.x0 = 0 by A45,XCMPLX_1:6;
hence contradiction by A5,A3,A12,A9;
end;
now
let n;
A47: (f/*(h+c)).n <>0 & (f/*c).n <>0 by A35,A32,SEQ_1:5;
thus (h"(#) ((f^)/*(h+c) - ((f^)/*c))).n = (h").n* ((f^)/*(h+c) - ((f^)
/*c)).n by SEQ_1:8
.= (h").n* (((f^)/*(h+c)).n - ((f^)/*c).n) by RFUNCT_2:1
.= (h").n* (((f/*(h+c))").n - ((f^)/*c).n) by A22,RFUNCT_2:12
.= (h").n* (((f/*(h+c))").n - ((f/*c)").n) by A31,RFUNCT_2:12
.= (h").n* (((f/*(h+c)).n)" - ((f/*c)").n) by VALUED_1:10
.= (h").n* (((f/*(h+c)).n)" - ((f/*c).n)") by VALUED_1:10
.= (h").n* (1/(f/*(h+c)).n - ((f/*c).n)") by XCMPLX_1:215
.= (h").n* (1/(f/*(h+c)).n - 1/(f/*c).n) by XCMPLX_1:215
.= (h").n* ((1*((f/*c).n) - 1*((f/*(h+c)).n))/((f/*(h+c)).n*(f/*c).n
)) by A47,XCMPLX_1:130
.= (h").n* ((-((f/*(h+c)).n - (f/*c).n))/((f/*(h+c))(#)(f/*c)).n) by
SEQ_1:8
.= (h").n* ((-((f/*(h+c) - (f/*c)).n))/((f/*(h+c))(#)(f/*c)).n) by
RFUNCT_2:1
.= (h").n*(-(((f/*(h+c) - (f/*c)).n)/((f/*(h+c))(#)(f/*c)).n)) by
XCMPLX_1:187
.= -((h").n*(((f/*(h+c) - (f/*c)).n)/(((f/*(h+c))(#)(f/*c)).n)))
.= -((h").n*((f/*(h+c) - (f/*c)).n))/((f/*(h+c))(#)(f/*c)).n by
XCMPLX_1:74
.= -( ((h" (#) ((f/*(h+c)) - (f/*c))).n) )/((f/*(h+c))(#)(f/*c)).n
by SEQ_1:8
.= -(((h"(#)((f/*(h+c)) - (f/*c))).n))*(((f/*(h+c))(#) (f/*c)).n)"
by XCMPLX_0:def 9
.= -((((h"(#)((f/*(h+c)) - (f/*c))).n))*(((f/*(h+c))(#) (f/*c))").n)
by VALUED_1:10
.= -(((h")(#)((f/*(h+c)) - (f/*c)))/"((f/*(h+c))(#)(f/*c))).n by
SEQ_1:8
.= (-((h"(#)((f/*(h+c)) - (f/*c)))/"((f/*(h+c))(#)(f/*c)))).n by
SEQ_1:10
.= ((-(h"(#)((f/*(h+c)) - (f/*c))))/"((f/*(h+c))(#)(f/*c))).n by
SEQ_1:48;
end;
then
A48: h"(#) ((f^)/*(h+c) - (f^)/*c) = (-(h"(#)((f/*(h+c)) - (f/*c))))/"((f
/*(h+c))(#) (f/*c)) by FUNCT_2:63;
A49: f/*(h+c) (#) (f/*c) is convergent by A42,A44;
then
lim(h"(#) ((f^)/*(h+c) - (f^)/*c)) = lim (-(h"(#) ((f/*(h+c)) - (f/*c
))))/(f.x0)^2 by A36,A45,A46,A29,A48,SEQ_2:24
.= (-Ldiff(f,x0))/(f.x0)^2 by A28,A27,SEQ_2:10
.= -Ldiff(f,x0)/(f.x0)^2 by XCMPLX_1:187;
hence thesis by A36,A49,A46,A29,A48,SEQ_2:23;
end;
hence thesis by A6,A14,Th9;
end;
theorem
f is_left_differentiable_in x0 & f.x0 <> 0 implies f^
is_left_differentiable_in x0 & Ldiff(f^,x0) = - Ldiff(f,x0)/(f.x0)^2
proof
assume that
A1: f is_left_differentiable_in x0 and
A2: f.x0 <> 0;
consider r1 such that
A3: r1 > 0 and
[.x0-r1,x0.] c= dom f and
A4: for g st g in [.x0-r1,x0.] holds f.g <> 0 by A1,A2,Th5,Th6;
now
take r1;
thus r1 > 0 by A3;
let g;
assume that
g in dom f and
A5: g in [.x0 - r1,x0.];
thus f.g <> 0 by A4,A5;
end;
hence thesis by A1,Lm2;
end;
theorem Th15:
for g1 being Real holds
f is_right_differentiable_in x0 & Rdiff(f,x0) = g1 iff (ex r st
r>0 & [.x0,x0+r.] c= dom f) & for h,c st rng c = {x0} & rng (h+c) c= dom f & (
for n being Nat holds h.n > 0)
holds h"(#)(f/*(h+c) - f/*c) is convergent & lim (h"(#)(f
/*(h+c) - f/*c)) = g1
proof let g1 be Real;
thus f is_right_differentiable_in x0 & Rdiff(f,x0) = g1 implies (ex r st r>0
& [.x0,x0+r.] c= dom f) & for h,c st rng c = {x0} & rng (h+c) c= dom f &
(for n being Nat
holds h.n > 0) holds h"(#)(f/*(h+c) - f/*c) is convergent & lim (h"(#)(f/*(h+c)
- f/*c)) = g1 by Def6;
assume that
A1: ex r st r>0 & [.x0,x0+r.] c= dom f and
A2: for h,c st rng c = {x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n > 0)
holds h"(#)(f/*(h+c) - f/*c) is convergent & lim (h"(#)(f/*(h+c) - f/*c)) = g1;
for h,c holds ( rng c = {x0} & rng (h+c) c= dom f &
for n being Nat holds h.n > 0
) implies h"(#)(f/*(h+c) - f/*c) is convergent by A2;
hence
A3: f is_right_differentiable_in x0 by A1;
for h,c holds ( rng c = {x0} & rng (h+c) c= dom f &
for n being Nat holds h.n > 0)
implies lim (h"(#)(f/*(h+c) - f/*c)) = g1 by A2;
hence thesis by A3,Def6;
end;
theorem
f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0
implies f1+f2 is_right_differentiable_in x0 & Rdiff(f1+f2,x0) = Rdiff(f1,x0)+
Rdiff(f2,x0)
proof
assume that
A1: f1 is_right_differentiable_in x0 and
A2: f2 is_right_differentiable_in x0;
consider r2 such that
A3: r2>0 and
A4: [.x0,x0+r2.] c=dom f2 by A2;
consider r1 such that
A5: r1>0 and
A6: [.x0,x0+r1.] c= dom f1 by A1;
A7: x0+0 = x0;
set r = min (r1,r2);
0 <= r by A5,A3,XXREAL_0:15;
then
A8: x0 <= x0 + r by A7,XREAL_1:7;
r<=r2 by XXREAL_0:17;
then
A9: x0 + r <= x0 + r2 by XREAL_1:7;
then x0 + r in {g: x0 <= g & g <= x0 +r2} by A8;
then
A10: x0 + r in [.x0,x0+r2.] by RCOMP_1:def 1;
x0 <= x0 + r2 by A8,A9,XXREAL_0:2;
then x0 in [.x0,x0+r2.] by XXREAL_1:1;
then [.x0,x0+r.] c= [.x0,x0+r2.] by A10,XXREAL_2:def 12;
then
A11: [.x0,x0+r.] c= dom f2 by A4;
r<=r1 by XXREAL_0:17;
then
A12: x0 + r <= x0 + r1 by XREAL_1:7;
then x0 + r in {g: x0 <= g & g <= x0 +r1} by A8;
then
A13: x0 + r in [.x0,x0+r1.] by RCOMP_1:def 1;
x0 <= x0 + r1 by A12,A8,XXREAL_0:2;
then x0 in [.x0,x0+r1.] by XXREAL_1:1;
then [.x0,x0+r.] c= [.x0,x0+r1.] by A13,XXREAL_2:def 12;
then [.x0,x0+r.] c= dom f1 by A6;
then
A14: [.x0,x0+r.] c= dom f1 /\ dom f2 by A11,XBOOLE_1:19;
then
A15: [.x0,x0+r.] c= dom(f1 + f2) by VALUED_1:def 1;
A16: for h,c st rng c = {x0} & rng (h+c) c= dom (f1+f2) &
(for n being Nat holds h.n >
0 ) holds h"(#)((f1+f2)/*(h+c) - (f1+f2)/*c) is convergent & lim (h"(#)((f1+f2)
/*(h+c) - (f1+f2)/*c)) = Rdiff(f1,x0) + Rdiff(f2,x0)
proof
let h,c;
assume that
A17: rng c = {x0} and
A18: rng (h+c) c= dom (f1+f2) and
A19: for n being Nat holds h.n > 0;
A20: rng (h+c) c= dom f1 /\ dom f2 by A18,VALUED_1:def 1;
A21: now
let n;
A22: rng c c= dom f1 /\ dom f2
proof
let x be object;
assume x in rng c;
then
A23: x = x0 by A17,TARSKI:def 1;
x0 in [.x0,x0 + r.] by A8,XXREAL_1:1;
hence thesis by A14,A23;
end;
thus (f1/*(h+c) - f1/*c + (f2/*(h+c) - f2/*c)).n = (f1/*(h+c) + (-(f1/*c
))).n + (f2/*(h+c) - f2/*c).n by SEQ_1:7
.= (f1/*(h+c)).n + (-(f1/*c)).n + (f2/*(h+c) + (-(f2/*c))).n by SEQ_1:7
.= (f1/*(h+c)).n + (-(f1/*c)).n + ((f2/*(h+c)).n + (-(f2/*c)).n) by
SEQ_1:7
.= (f1/*(h+c)).n + (f2/*(h+c)).n+ ((-(f1/*c)).n +(-(f2/*c)).n)
.= (f1/*(h+c)).n + (f2/*(h+c)).n + (-(f1/*c).n + (-(f2/*c)).n) by
SEQ_1:10
.= (f1/*(h+c)).n + (f2/*(h+c)).n + (-(f1/*c).n + -(f2/*c).n) by
SEQ_1:10
.= (f1/*(h+c)).n + (f2/*(h+c)).n - ((f1/*c).n + (f2/*c).n)
.= (f1/*(h+c) + f2/*(h+c)).n - ((f1/*c).n + (f2/*c).n) by SEQ_1:7
.= (f1/*(h+c) + f2/*(h+c)).n - ((f1/*c + f2/*c).n) by SEQ_1:7
.= (f1/*(h+c) + f2/*(h+c) - (f1/*c + f2/*c)).n by RFUNCT_2:1
.= ((f1+f2)/*(h+c) - (f1/*c + f2/*c)).n by A20,RFUNCT_2:8
.= ((f1+f2)/*(h+c) - (f1+f2)/*c).n by A22,RFUNCT_2:8;
end;
then
A24: f1/*(h+c)-f1/*c + (f2/*(h+c) - f2/*c)=(f1+f2)/*(h+c) - (f1+f2)/*c by
FUNCT_2:63;
dom f1 /\dom f2 c= dom f2 by XBOOLE_1:17;
then
A25: rng (h+c) c= dom f2 by A20;
then
A26: lim(h"(#)(f2/*(h+c) - f2/*c)) = Rdiff(f2,x0) by A2,A17,A19,Th15;
A27: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A17,A19,A25;
dom f1 /\ dom f2 c= dom f1 by XBOOLE_1:17;
then
A28: rng (h+c) c= dom f1 by A20;
A29: (h"(#)(f1/*(h+c) - f1/*c) +h"(#)(f2/*(h+c) - f2/*c)) = h"(#)(f1/*(h+c
) -f1/*c + (f2/*(h+c) - f2/*c)) by SEQ_1:16;
A30: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A17,A19,A28;
then (h"(#)(f1/*(h+c) - f1/*c) + h"(#)(f2/*(h+c) - f2/*c)) is convergent
by A27;
hence h"(#)((f1+f2)/*(h+c) - (f1+f2)/*c) is convergent by A29,A21,
FUNCT_2:63;
lim(h"(#)(f1/*(h+c) - f1/*c)) = Rdiff(f1,x0) by A1,A17,A19,A28,Th15;
hence thesis by A30,A27,A26,A29,A24,SEQ_2:6;
end;
00 and
A4: [.x0,x0+r2.] c=dom f2 by A2;
consider r1 such that
A5: r1>0 and
A6: [.x0,x0+r1.] c= dom f1 by A1;
set r = min (r1,r2);
A7: 0 0 ) holds h"(#)((f1-f2)/*(h+c) - (f1-f2)/*c) is convergent & lim(h"(#)((f1-f2
)/*(h+c) - (f1-f2)/*c)) = Rdiff(f1,x0) - Rdiff(f2,x0)
proof
let h,c;
assume that
A16: rng c ={x0} and
A17: rng (h+c) c= dom(f1-f2) and
A18: for n being Nat holds h.n > 0;
A19: rng (h+c) c= dom f1 /\ dom f2 by A17,VALUED_1:12;
A20: now
let n;
A21: rng c c= dom f1 /\ dom f2
proof
let x be object;
assume x in rng c;
then
A22: x = x0 by A16,TARSKI:def 1;
x0 in [.x0,x0+r.] by A8,XXREAL_1:1;
hence thesis by A14,A22;
end;
thus (f1/*(h+c) - f1/*c - (f2/*(h+c) - f2/*c)).n = (f1/*(h+c) - f1/*c).n
- (f2/*(h+c) - f2/*c).n by RFUNCT_2:1
.= (f1/*(h+c)).n - (f1/*c).n - (f2/*(h+c) - (f2/*c)).n by RFUNCT_2:1
.= (f1/*(h+c)).n - (f1/*c).n - ((f2/*(h+c)).n - (f2/*c).n) by
RFUNCT_2:1
.= (f1/*(h+c)).n - (f2/*(h+c)).n - ((f1/*c).n - (f2/*c).n)
.= (f1/*(h+c) - f2/*(h+c)).n - ((f1/*c).n - (f2/*c).n) by RFUNCT_2:1
.= (f1/*(h+c) - f2/*(h+c)).n - ((f1/*c - f2/*c).n) by RFUNCT_2:1
.= (f1/*(h+c) - f2/*(h+c) - (f1/*c - f2/*c)).n by RFUNCT_2:1
.= ((f1-f2)/*(h+c) - (f1/*c - f2/*c)).n by A19,RFUNCT_2:8
.= ((f1-f2)/*(h+c) - (f1-f2)/*c).n by A21,RFUNCT_2:8;
end;
then
A23: f1/*(h+c) - f1/*c - (f2/*(h+c) - f2/*c) = (f1-f2)/*(h+c) - (f1-f2)/*c
by FUNCT_2:63;
dom f1 /\ dom f2 c= dom f2 by XBOOLE_1:17;
then
A24: rng (h+c) c= dom f2 by A19;
then
A25: lim(h"(#)((f2/*(h+c) - f2/*c))) =Rdiff(f2,x0) by A2,A16,A18,Th15;
A26: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A16,A18,A24;
dom f1 /\ dom f2 c= dom f1 by XBOOLE_1:17;
then
A27: rng (h+c) c= dom f1 by A19;
A28: (h"(#)(f1/*(h+c) - f1/*c) - h"(#)(f2/*(h+c) - f2/*c)) = h"(#)(f1/*(h+
c) -f1/*c - (f2/*(h+c) - f2/*c)) by SEQ_1:21;
A29: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A16,A18,A27;
then (h"(#)(f1/*(h+c) - f1/*c) - h"(#)(f2/*(h+c) - f2/*c)) is convergent
by A26;
hence h"(#)((f1-f2)/*(h+c) - (f1-f2)/*c) is convergent by A28,A20,
FUNCT_2:63;
lim(h"(#)((f1/*(h+c) - f1/*c))) =Rdiff(f1,x0) by A1,A16,A18,A27,Th15;
hence thesis by A29,A26,A25,A28,A23,SEQ_2:12;
end;
[.x0,x0+r.] c= dom (f1 - f2) by A14,VALUED_1:12;
hence thesis by A7,A15,Th15;
end;
theorem
f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0
implies f1(#)f2 is_right_differentiable_in x0 & Rdiff(f1(#)f2,x0) = Rdiff(f1,x0
)*f2.x0 + Rdiff(f2,x0)*f1.x0
proof
assume that
A1: f1 is_right_differentiable_in x0 and
A2: f2 is_right_differentiable_in x0;
A3: x0 + 0 =x0;
consider r2 such that
A4: r2>0 and
A5: [.x0,x0+r2.] c=dom f2 by A2;
consider r1 such that
A6: r1>0 and
A7: [.x0,x0+r1.] c= dom f1 by A1;
set r = min (r1,r2);
0 <= r by A6,A4,XXREAL_0:15;
then
A8: x0 <= x0 + r by A3,XREAL_1:7;
r<=r2 by XXREAL_0:17;
then
A9: x0 + r <= x0 + r2 by XREAL_1:7;
then x0 + r in {g: x0 <= g & g <= x0 +r2} by A8;
then
A10: x0 + r in [.x0,x0+r2.] by RCOMP_1:def 1;
x0 <= x0 + r2 by A8,A9,XXREAL_0:2;
then x0 in [.x0,x0+r2.] by XXREAL_1:1;
then [.x0,x0+r.] c= [.x0,x0+r2.] by A10,XXREAL_2:def 12;
then
A11: [.x0,x0+r.] c= dom f2 by A5;
r<=r1 by XXREAL_0:17;
then
A12: x0 + r <= x0 + r1 by XREAL_1:7;
then x0 + r in {g: x0 <= g & g <= x0 +r1} by A8;
then
A13: x0 + r in [.x0,x0+r1.] by RCOMP_1:def 1;
x0 <= x0+r1 by A12,A8,XXREAL_0:2;
then x0 in [.x0,x0+r1.] by XXREAL_1:1;
then [.x0,x0+r.] c= [.x0,x0+r1.] by A13,XXREAL_2:def 12;
then
A14: [.x0,x0+r.] c= dom f1 by A7;
A15: 0 0 ) holds h"(#)((f1(#)f2)/*(h+c) - (f1(#)f2)/*c) is convergent & lim(h"(#)((
f1(#)f2)/*(h+c) - (f1(#) f2)/*c))=Rdiff(f1,x0)*f2.x0 + Rdiff(f2,x0)*f1.x0
proof
let h,c;
assume that
A17: rng c = {x0} and
A18: rng (h+c) c= dom (f1(#)f2) and
A19: for n being Nat holds h.n > 0;
A20: rng (h + c) c= dom f1 /\ dom f2 by A18,VALUED_1:def 4;
x0 + 0 <= x0 +r by A15,XREAL_1:7;
then
A21: x0 in [.x0,x0+ r.] by XXREAL_1:1;
then
A22: x0 in dom f2 by A11;
A23: rng c c=dom f2
by A17,A22,TARSKI:def 1;
A24: for m holds c.m = x0
proof
let m;
c.m in rng c by VALUED_0:28;
hence thesis by A17,TARSKI:def 1;
end;
A25: for g be Real st 0 0 by A19;
thus (h(#)(h"(#)(f1/*(h+c) - f1/*c))).n =((h(#)h")(#)(f1/*(h+c) - f1/*c)
). n by SEQ_1:14
.= (h(#)h").n*(f1/*(h+c) - f1/*c).n by SEQ_1:8
.= h.n*(h").n*(f1/*(h+c) - f1/*c).n by SEQ_1:8
.= h.n*(h.n)"*(f1/*(h+c) - f1/*c).n by VALUED_1:10
.= 1*(f1/*(h+c) - f1/*c).n by A31,XCMPLX_0:def 7
.= (f1/*(h+c) - f1/*c).n;
end;
then
A32: h(#)(h"(#)(f1/*(h+c) - f1/*c)) =(f1/*(h+c) - f1/*c) by FUNCT_2:63;
A33: x0 in dom f1 by A14,A21;
A34: rng c c=dom f1
by A17,A33,TARSKI:def 1;
A35: for g be Real st 0 0 & for g st g in dom f2 & g in [.x0, x0 + r0.] holds f2.g <> 0 )
implies f1/f2 is_right_differentiable_in x0 & Rdiff(f1/f2,x0) =(Rdiff(f1,x0)*f2
.x0 - Rdiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
assume that
A1: f1 is_right_differentiable_in x0 and
A2: f2 is_right_differentiable_in x0;
consider r2 such that
A3: 0 < r2 and
A4: [.x0,x0 + r2.] c= dom f2 by A2;
consider r1 such that
A5: 0 < r1 and
A6: [.x0,x0 + r1.] c= dom f1 by A1;
given r0 such that
A7: r0 > 0 and
A8: for g st g in dom f2 & g in [.x0,x0 + r0.] holds f2.g <> 0;
A9: 0 + x0 =x0;
set r3 = min(r0,r2);
0 <= r3 by A7,A3,XXREAL_0:15;
then
A10: x0 <= x0 +r3 by A9,XREAL_1:6;
r3 <= r2 by XXREAL_0:17;
then
A11: x0 + r3 <= x0 + r2 by XREAL_1:7;
then x0 <= x0 + r2 by A10,XXREAL_0:2;
then
A12: x0 in [.x0,x0 + r2.] by XXREAL_1:1;
x0 + r3 in { g:x0 <= g & g <= x0 + r2 } by A10,A11;
then x0 + r3 in [.x0,x0 +r2.] by RCOMP_1:def 1;
then [.x0,x0 + r3.] c= [.x0,x0 + r2.] by A12,XXREAL_2:def 12;
then
A13: [.x0,x0 + r3.] c= dom f2 by A4;
r3 <= r0 by XXREAL_0:17;
then
A14: x0 + r3 <= x0 + r0 by XREAL_1:7;
then x0 <= x0 +r0 by A10,XXREAL_0:2;
then
A15: x0 in [.x0,x0 + r0.] by XXREAL_1:1;
A16: x0 +0 = x0;
set r = min(r1,r3);
A17: 0 < r3 by A7,A3,XXREAL_0:15;
then 0 <= r by A5,XXREAL_0:15;
then
A18: x0 <= x0 + r by A16,XREAL_1:7;
r <= r3 by XXREAL_0:17;
then
A19: x0 + r <= x0 + r3 by XREAL_1:7;
then x0 <= x0 + r3 by A18,XXREAL_0:2;
then
A20: x0 in [.x0,x0 + r3.] by XXREAL_1:1;
x0 + r3 in { g: x0 <= g & g<= x0 + r0 } by A10,A14;
then x0 + r3 in [.x0,x0 + r0.] by RCOMP_1:def 1;
then
A21: [.x0,x0 +r3.] c= [.x0,x0 +r0.] by A15,XXREAL_2:def 12;
x0 + r in {g:x0 <= g & g <= x0 + r3} by A18,A19;
then x0 + r in [.x0,x0 +r3.] by RCOMP_1:def 1;
then
A22: [.x0,x0 + r.] c= [.x0,x0 +r3.] by A20,XXREAL_2:def 12;
[.x0,x0 + r.] c= dom(f2^)
proof
assume not thesis;
then consider x being object such that
A23: x in [.x0,x0 + r.] and
A24: not x in dom (f2^);
reconsider x as Real by A23;
A25: x in [.x0,x0 + r3.] by A22,A23;
A26: not x in dom f2 \ f2"{0} by A24,RFUNCT_1:def 2;
now
per cases by A26,XBOOLE_0:def 5;
suppose
not x in dom f2;
hence contradiction by A13,A25;
end;
suppose
A27: x in f2"{0};
then f2.x in {0} by FUNCT_1:def 7;
then
A28: f2.x = 0 by TARSKI:def 1;
x in dom f2 by A27,FUNCT_1:def 7;
hence contradiction by A8,A21,A25,A28;
end;
end;
hence contradiction;
end;
then
A29: [.x0,x0 + r.] c= dom f2\f2"{0} by RFUNCT_1:def 2;
r <= r1 by XXREAL_0:17;
then
A30: x0 + r <= x0 + r1 by XREAL_1:7;
then x0 <= x0 + r1 by A18,XXREAL_0:2;
then
A31: x0 in [.x0,x0 +r1.] by XXREAL_1:1;
x0 + r in { g:x0 <= g & g <= x0 + r1 } by A18,A30;
then x0 + r in [.x0,x0 + r1.] by RCOMP_1:def 1;
then [.x0,x0 +r.] c= [.x0,x0 + r1.] by A31,XXREAL_2:def 12;
then
A32: [.x0,x0 + r.] c= dom f1 by A6;
then [.x0,x0 + r.] c= dom f1 /\ (dom f2\f2"{0}) by A29,XBOOLE_1:19;
then
A33: [.x0,x0 + r.] c= dom (f1/f2) by RFUNCT_1:def 1;
A34: for h,c st rng c = {x0} & rng (h+c) c= dom (f1/f2) &
(for n being Nat holds h.n >
0) holds h"(#)((f1/f2)/*(h+c) - (f1/f2)/*c) is convergent & lim(h"(#)((f1/f2)/*
(h+c) - (f1/f2)/*c)) = (Rdiff(f1,x0)*f2.x0 - Rdiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
let h,c;
assume that
A35: rng c = {x0} and
A36: rng (h+c) c= dom (f1/f2) and
A37: for n being Nat holds h.n > 0;
A38: rng (h + c) c= dom f1 /\ (dom f2\f2"{0}) by A36,RFUNCT_1:def 1;
0 <= r & x0 + 0 = x0 by A5,A17,XXREAL_0:15;
then x0 <= x0 + r by XREAL_1:7;
then
A39: x0 in [.x0,x0 + r.] by XXREAL_1:1;
then
A40: x0 in dom f1 by A32;
A41: rng c c= dom f1
by A35,A40,TARSKI:def 1;
dom f1 /\ (dom f2\f2"{0}) c= dom f1 by XBOOLE_1:17;
then
A42: rng (h + c) c= dom f1 by A38;
then
A43: lim(h"(#)(f1/*(h+c) - f1/*c)) = Rdiff(f1,x0) by A1,A35,A37,Th15;
A44: x0 in (dom f2\f2"{0}) by A29,A39;
rng c c= (dom f2\f2"{0})
by A35,A44,TARSKI:def 1;
then
A45: rng c c= dom (f2^) by RFUNCT_1:def 2;
then
A46: rng c c= dom f1 /\ dom (f2^) by A41,XBOOLE_1:19;
A47: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A35,A37,A42;
A48: f2/*c is non-zero by A45,RFUNCT_2:11;
A49: now
let n;
thus (h"(#)((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c)))).n = (h").n *
((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c))).n by SEQ_1:8
.= (h").n * (((f1/*(h+c))(#)(f2/*c)).n - ((f1/*c)(#) (f2/*(h+c))).n)
by RFUNCT_2:1
.= (h").n * ((f1/*(h+c)).n * (f2/*c).n - ((f1/*c)(#)(f2/*(h+c))).n)
by SEQ_1:8
.= (h").n * (((f1/*(h+c)).n - (f1/*c).n) * (f2/*c).n + ((f1/*c).n*(
f2/*c).n) - ((f1/*c).n * (f2/*(h+c)).n)) by SEQ_1:8
.= (h").n * ((f1/*(h+c)).n - (f1/*c).n) * (f2/*c).n - (f1/*c).n * ((
h").n * ((f2/*(h+c)).n - (f2/*c).n))
.= (h").n * ((f1/*(h+c)) - (f1/*c)).n * (f2/*c).n - (f1/*c).n * ((h"
).n * ((f2/*(h+c)).n - (f2/*c).n)) by RFUNCT_2:1
.= (h").n * (f1/*(h+c) - (f1/*c)).n * (f2/*c).n - (f1/*c).n * ((h").
n * (f2/*(h+c) - (f2/*c)).n) by RFUNCT_2:1
.= (h" (#) (f1/*(h+c) - (f1/*c))).n * (f2/*c).n - (f1/*c).n * ((h").
n * (f2/*(h+c) - (f2/*c)).n) by SEQ_1:8
.= (h"(#)(f1/*(h+c) - (f1/*c))).n * (f2/*c).n - (f1/*c).n * (h"(#)(
f2/*(h+c) - (f2/*c))).n by SEQ_1:8
.= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c)).n - (f1/*c).n * (h"(#)(f2
/*(h+c) - (f2/*c))).n by SEQ_1:8
.= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c)).n - ((f1/*c)(#)(h"(#)(f2/*
(h+c)-(f2/*c)))).n by SEQ_1:8
.= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+
c)-(f2/*c)))).n by RFUNCT_2:1;
end;
now
let n;
thus (f2/*c + (f2/*(h+c) - f2/*c)).n = (f2/*c).n + (f2/*(h+c) - f2/*c).n
by SEQ_1:7
.= (f2/*c).n + ((f2/*(h+c)).n - (f2/*c).n) by RFUNCT_2:1
.= (f2/*(h+c)).n;
end;
then
A50: f2/*c + (f2/*(h+c) - f2/*c) = f2/*(h+c) by FUNCT_2:63;
dom f1 /\ (dom f2\f2"{0}) c=(dom f2\f2"{0}) by XBOOLE_1:17;
then
A51: rng (h + c) c= (dom f2\f2"{0}) by A38;
then
A52: rng (h + c) c= dom (f2^) by RFUNCT_1:def 2;
then
A53: rng (h + c) c= dom f1 /\ dom (f2^) by A42,XBOOLE_1:19;
A54: f2/*(h+c) is non-zero by A52,RFUNCT_2:11;
then
A55: (f2/*(h+c)) (#) (f2/*c) is non-zero by A48,SEQ_1:35;
h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c)=h"(#)((f1(#) (f2^))/*(h+c) - (f1
/f2)/*c) by RFUNCT_1:31
.=h"(#)((f1(#)(f2^))/*(h+c) - (f1(#)(f2^))/*c) by RFUNCT_1:31
.=h"(#)((f1/*(h+c))(#)((f2^)/*(h+c)) - (f1(#) (f2^))/*c) by A53,
RFUNCT_2:8
.=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1(#)(f2^))/*c) by A52,RFUNCT_2:12
.=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1/*c)(#) ((f2^)/*c)) by A46,
RFUNCT_2:8
.=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1/*c)/"(f2/*c)) by A45,RFUNCT_2:12
.=h"(#)(((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c)))/"((f2/*(h+c))
(#) (f2/*c))) by A54,A48,SEQ_1:50
.=(h"(#)((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c))))/"((f2/*(h+c))
(#) (f2/*c)) by SEQ_1:41;
then
A56: h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c) =((h"(#)(f1/*(h+c) - (f1/*c)) )
(#) (f2/*c) - (f1/*c)(#)(h"(#)(f2/*(h+c)-(f2/*c))))/"(f2/*(h+c)(#) (f2/*c)) by
A49,FUNCT_2:63;
dom f2 \ f2"{0} c= dom f2 by XBOOLE_1:36;
then
A57: rng (h + c) c= dom f2 by A51;
then
A58: lim(h"(#)(f2/*(h+c) - f2/*c)) = Rdiff(f2,x0) by A2,A35,A37,Th15;
A59: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A35,A37,A57;
now
let n;
A60: h.n <> 0 by A37;
thus (h(#)(h"(#)(f2/*(h+c) - f2/*c))).n = ((h(#)h")(#)(f2/*(h+c) - f2/*c
)). n by SEQ_1:14
.= (h(#)h").n *(f2/*(h+c) - f2/*c).n by SEQ_1:8
.= h.n * (h").n *(f2/*(h+c) - f2/*c).n by SEQ_1:8
.= h.n * (h.n)" *(f2/*(h+c) - f2/*c).n by VALUED_1:10
.= 1*(f2/*(h+c) - f2/*c).n by A60,XCMPLX_0:def 7
.= (f2/*(h+c) - f2/*c).n;
end;
then
A61: h(#)(h"(#)(f2/*(h+c) - f2/*c)) = (f2/*(h+c) - f2/*c) by FUNCT_2:63;
A62: for m holds c.m = x0
proof
let m;
c.m in rng c by VALUED_0:28;
hence thesis by A35,TARSKI:def 1;
end;
A63: for g be Real st 0 < g
ex n being Nat st for m being Nat st n <=m holds |.(f1/*c
).m - f1.x0.| < g
proof
let g be Real such that
A64: 0 < g;
take n = 0;
let m being Nat such that
n <= m;
A65: m in NAT by ORDINAL1: def 12;
|.(f1/*c).m - f1.x0.| = |.f1.(c.m) - f1.x0.| by A41,FUNCT_2:108,A65
.=|.f1.x0-f1.x0.| by A62,A65
.= 0 by ABSVALUE:def 1;
hence thesis by A64;
end;
then
A66: f1/*c is convergent by SEQ_2:def 6;
then
A67: lim(f1/*c) = f1.x0 by A63,SEQ_2:def 7;
dom (f2^) = dom f2 \ f2"{0} by RFUNCT_1:def 2;
then
A68: dom (f2^) c= dom f2 by XBOOLE_1:36;
A69: for g be Real st 0 < g
ex n being Nat st for m being Nat st n <=m holds |.(f2/*
c).m - f2.x0.| < g
proof
let g be Real such that
A70: 0 < g;
take n = 0;
let m being Nat such that
n <= m;
A71: m in NAT by ORDINAL1: def 12;
|.(f2/*c).m - f2.x0.| = |.f2.(c.m) - f2.x0.| by A45,A68,FUNCT_2:108
,XBOOLE_1:1,A71
.=|.f2.x0 - f2.x0.| by A62,A71
.= 0 by ABSVALUE:def 1;
hence thesis by A70;
end;
then
A72: f2/*c is convergent by SEQ_2:def 6;
then
A73: lim(f2/*c) = f2.x0 by A69,SEQ_2:def 7;
h(#)(h"(#)(f2/*(h+c) - f2/*c)) is convergent by A59;
then
A74: f2/*(h+c) is convergent by A72,A61,A50;
then
A75: f2/*(h+c) (#) (f2/*c) is convergent by A72;
h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A35,A37,A57;
then lim (h(#)(h"(#)(f2/*(h+c) - f2/*c))) = lim h *lim (h"(#)(f2/*(h+c) -
f2/* c ) ) by SEQ_2:15
.= 0;
then 0 = lim (f2/*(h+c)) - f2.x0 by A72,A73,A61,A74,SEQ_2:12;
then
A76: lim(f2/*(h+c) (#) (f2/*c)) = (f2.x0)^2 by A72,A73,A74,SEQ_2:15;
A77: lim(f2/*(h+c) (#) (f2/*c))<> 0
proof
assume not thesis;
then f2.x0 = 0 by A76,XCMPLX_1:6;
hence contradiction by A8,A4,A15,A12;
end;
h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A35,A37,A42;
then
A78: h"(#) (f1/*(h+c) - f1/*c)(#)(f2/*c) is convergent by A72;
A79: (f1/*c)(#)(h"(#) (f2/*(h+c) - f2/*c)) is convergent by A59,A66;
then
A80: ((h"(#)(f1/*(h+c) - (f1/*c)))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+c
)-(f2/*c)))) is convergent by A78;
then lim(h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c)) = lim((h"(#)(f1/*(h+c) - (
f1/*c)))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+c)-(f2/*c))))/ lim(f2/*(h+c)(#)(
f2/*c)) by A55,A75,A77,A56,SEQ_2:24
.=(lim((h"(#)(f1/*(h+c)-(f1/*c)))(#)(f2/*c))-lim((f1/*c)(#)(h"(#)(f2/*
(h+c)- (f2/*c)))))/lim(f2/*(h+c)(#)(f2/*c)) by A79,A78,SEQ_2:12
.=( lim(h"(#)(f1/*(h+c)-(f1/*c)))*lim(f2/*c) - lim((f1/*c) (#) (h"(#)(
f2/*(h+c)-(f2/*c)))) ) / lim(f2/*(h+c)(#)(f2/*c)) by A47,A72,SEQ_2:15
.=(Rdiff(f1,x0) * f2.x0 - Rdiff(f2,x0) * f1.x0)/(f2.x0)^2 by A43,A59,A58
,A66,A67,A73,A76,SEQ_2:15;
hence thesis by A55,A75,A77,A80,A56,SEQ_2:23;
end;
0 < r by A5,A17,XXREAL_0:15;
hence thesis by A33,A34,Th15;
end;
theorem
f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 &
f2.x0 <> 0 implies f1/f2 is_right_differentiable_in x0 & Rdiff(f1/f2,x0) = (
Rdiff(f1,x0)*f2.x0 - Rdiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
assume that
A1: f1 is_right_differentiable_in x0 and
A2: f2 is_right_differentiable_in x0 and
A3: f2.x0 <> 0;
consider r1 such that
A4: r1 > 0 and
[.x0,x0 + r1.] c= dom f2 and
A5: for g st g in [.x0,x0 + r1.] holds f2.g <> 0 by A2,A3,Th7,Th8;
now
take r1;
thus r1 > 0 by A4;
let g;
assume that
g in dom f2 and
A6: g in [.x0,x0+r1.];
thus f2.g <> 0 by A5,A6;
end;
hence thesis by A1,A2,Lm3;
end;
Lm4: f is_right_differentiable_in x0 & (ex r0 st r0 > 0 & for g st g in dom f
& g in [.x0, x0 + r0.] holds f.g <> 0) implies f^ is_right_differentiable_in x0
& Rdiff(f^,x0) = - Rdiff(f,x0)/(f.x0)^2
proof
A1: 0 + x0 =x0;
assume
A2: f is_right_differentiable_in x0;
then consider r2 such that
A3: 0 < r2 and
A4: [.x0,x0 + r2.] c= dom f;
given r0 such that
A5: r0 > 0 and
A6: for g st g in dom f & g in [.x0,x0 + r0.] holds f.g <> 0;
set r3 = min(r0,r2);
0 <= r3 by A5,A3,XXREAL_0:15;
then
A7: x0 <= x0 +r3 by A1,XREAL_1:6;
r3 <= r2 by XXREAL_0:17;
then
A8: x0 + r3 <= x0 + r2 by XREAL_1:7;
then x0 <= x0 + r2 by A7,XXREAL_0:2;
then
A9: x0 in [.x0,x0 + r2.] by XXREAL_1:1;
x0 + r3 in { g:x0 <= g & g <= x0 + r2 } by A7,A8;
then x0 + r3 in [.x0,x0 +r2.] by RCOMP_1:def 1;
then [.x0,x0 + r3.] c= [.x0,x0 + r2.] by A9,XXREAL_2:def 12;
then
A10: [.x0,x0 + r3.] c= dom f by A4;
r3 <= r0 by XXREAL_0:17;
then
A11: x0 + r3 <= x0 + r0 by XREAL_1:7;
then x0 <= x0 +r0 by A7,XXREAL_0:2;
then
A12: x0 in [.x0,x0 + r0.] by XXREAL_1:1;
x0 + r3 in { g: x0 <= g & g<= x0 + r0 } by A7,A11;
then x0 + r3 in [.x0,x0 + r0.] by RCOMP_1:def 1;
then
A13: [.x0,x0 +r3.] c= [.x0,x0 +r0.] by A12,XXREAL_2:def 12;
A14: [.x0,x0 + r3.] c= dom(f^)
proof
assume not thesis;
then consider x being object such that
A15: x in [.x0,x0 + r3.] and
A16: not x in dom (f^);
reconsider x as Real by A15;
A17: not x in dom f \ f"{0} by A16,RFUNCT_1:def 2;
now
per cases by A17,XBOOLE_0:def 5;
suppose
not x in dom f;
hence contradiction by A10,A15;
end;
suppose
A18: x in f"{0};
then f.x in {0} by FUNCT_1:def 7;
then
A19: f.x = 0 by TARSKI:def 1;
x in dom f by A18,FUNCT_1:def 7;
hence contradiction by A6,A13,A15,A19;
end;
end;
hence contradiction;
end;
A20: x0 in [. x0, x0 + r3 .] by A7,XXREAL_1:1;
A21: for h,c st rng c = {x0} & rng (h+c) c= dom (f^) &
(for n being Nat holds h.n > 0)
holds h"(#)((f^)/*(h+c) - (f^)/*c) is convergent & lim(h"(#)((f^)/*(h+c) - (f^)
/*c)) = - Rdiff(f,x0)/(f.x0)^2
proof
let h,c;
assume that
A22: rng c = {x0} and
A23: rng (h+c) c= dom (f^) and
A24: for n being Nat holds h.n > 0;
A25: for m holds c.m = x0
proof
let m;
c.m in rng c by VALUED_0:28;
hence thesis by A22,TARSKI:def 1;
end;
A26: dom f \ f"{0} c= dom f by XBOOLE_1:36;
rng (h + c) c= dom f\f"{0} by A23,RFUNCT_1:def 2;
then
A27: rng (h + c) c= dom f by A26;
then
A28: lim(h"(#)(f/*(h+c) - f/*c)) = Rdiff(f,x0) by A2,A22,A24,Th15;
A29: h"(#)(f/*(h+c) - f/*c) is convergent by A2,A22,A24,A27;
then
A30: -(h"(#)((f/*(h+c)) - (f/*c))) is convergent;
x0 in dom (f^) by A20,A14;
then
A31: x0 in (dom f\f"{0}) by RFUNCT_1:def 2;
rng c c= (dom f\f"{0})
by A22,A31,TARSKI:def 1;
then
A32: rng c c= dom (f^) by RFUNCT_1:def 2;
then
A33: f/*c is non-zero by RFUNCT_2:11;
now
let n;
A34: h.n <> 0 by A24;
thus (h(#)(h"(#)(f/*(h+c) - f/*c))).n = ((h(#)h")(#)(f/*(h+c) - f/*c)).n
by SEQ_1:14
.= (h(#)h").n *(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
.= 1*(f/*(h+c) - f/*c).n by A34,XCMPLX_0:def 7
.= (f/*(h+c) - f/*c).n;
end;
then
A35: h(#)(h"(#)(f/*(h+c) - f/*c)) = (f/*(h+c) - f/*c) by FUNCT_2:63;
A36: f/*(h+c) is non-zero by A23,RFUNCT_2:11;
then
A37: (f/*(h+c)) (#) (f/*c) is non-zero by A33,SEQ_1:35;
now
let n;
thus (f/*c + (f/*(h+c) - f/*c)).n = (f/*c).n + (f/*(h+c) - f/*c).n by
SEQ_1:7
.= (f/*c).n + ((f/*(h+c)).n - (f/*c).n) by RFUNCT_2:1
.= (f/*(h+c)).n;
end;
then
A38: f/*c + (f/*(h+c) - f/*c) = f/*(h+c) by FUNCT_2:63;
dom (f^) = dom f \ f"{0} by RFUNCT_1:def 2;
then
A39: dom (f^) c= dom f by XBOOLE_1:36;
A40: for g be Real st 0 < g
ex n being Nat st for m being Nat st n <=m holds |.(f/*c)
.m - f.x0.| < g
proof
let g be Real such that
A41: 0 < g;
take n = 0;
let m being Nat such that
n <= m;
A42: m in NAT by ORDINAL1:def 12;
|.(f/*c).m - f.x0.| = |.f.(c.m) - f.x0.| by A32,A39,FUNCT_2:108
,XBOOLE_1:1,A42
.=|.f.x0 - f.x0.| by A25,A42
.= 0 by ABSVALUE:def 1;
hence thesis by A41;
end;
then
A43: f/*c is convergent by SEQ_2:def 6;
then
A44: lim(f/*c) = f.x0 by A40,SEQ_2:def 7;
h(#)(h"(#)(f/*(h+c) - f/*c)) is convergent by A29;
then
A45: f/*(h+c) is convergent by A43,A35,A38;
lim (h(#)(h"(#)(f/*(h+c) - f/*c))) = lim h *lim (h"(#)(f/*(h+c) - f/*
c)) by A29,SEQ_2:15
.= 0;
then 0 = lim (f/*(h+c)) - f.x0 by A43,A44,A35,A45,SEQ_2:12;
then
A46: lim(f/*(h+c) (#) (f/*c)) = (f.x0)^2 by A43,A44,A45,SEQ_2:15;
A47: lim(f/*(h+c) (#) (f/*c))<> 0
proof
assume not thesis;
then f.x0 = 0 by A46,XCMPLX_1:6;
hence contradiction by A6,A4,A12,A9;
end;
now
let n;
A48: (f/*(h+c)).n <>0 & (f/*c).n <>0 by A36,A33,SEQ_1:5;
thus (h"(#) ((f^)/*(h+c) - (f^)/*c)).n = (h").n* ((f^)/*(h+c) - (f^)/*c)
.n by SEQ_1:8
.= (h").n* (((f^)/*(h+c)).n - ((f^)/*c).n) by RFUNCT_2:1
.= (h").n* (((f/*(h+c))").n - ((f^)/*c).n) by A23,RFUNCT_2:12
.= (h").n* (((f/*(h+c))").n - ((f/*c)").n) by A32,RFUNCT_2:12
.= (h").n* (((f/*(h+c)).n)" - ((f/*c)").n) by VALUED_1:10
.= (h").n* (((f/*(h+c)).n)" - ((f/*c).n)") by VALUED_1:10
.= (h").n* (1/(f/*(h+c)).n - ((f/*c).n)") by XCMPLX_1:215
.= (h").n* (1/(f/*(h+c)).n - 1/(f/*c).n) by XCMPLX_1:215
.= (h").n* ((1*((f/*c).n) - 1*((f/*(h+c)).n))/((f/*(h+c)).n*(f/*c).n
)) by A48,XCMPLX_1:130
.= (h").n* ((-((f/*(h+c)).n - (f/*c).n))/((f/*(h+c))(#)(f/*c)).n) by
SEQ_1:8
.= (h").n* ((-((f/*(h+c) - (f/*c)).n))/((f/*(h+c))(#)(f/*c)).n) by
RFUNCT_2:1
.= (h").n*(-(((f/*(h+c) - (f/*c)).n)/((f/*(h+c))(#)(f/*c)).n)) by
XCMPLX_1:187
.= -((h").n*(((f/*(h+c) - (f/*c)).n)/(((f/*(h+c))(#)(f/*c)).n)))
.= -((h").n*((f/*(h+c) - (f/*c)).n))/((f/*(h+c))(#)(f/*c)).n by
XCMPLX_1:74
.= -( ((h" (#) ((f/*(h+c)) - (f/*c))).n) )/((f/*(h+c))(#)(f/*c)).n
by SEQ_1:8
.= -(((h"(#)((f/*(h+c)) - (f/*c))).n))*(((f/*(h+c))(#) (f/*c)).n)"
by XCMPLX_0:def 9
.= -((((h"(#)((f/*(h+c)) - (f/*c))).n))*(((f/*(h+c))(#) (f/*c))").n)
by VALUED_1:10
.= -(((h")(#)((f/*(h+c)) - (f/*c)))/"((f/*(h+c))(#)(f/*c))).n by
SEQ_1:8
.= (-((h"(#)((f/*(h+c)) - (f/*c)))/"((f/*(h+c))(#)(f/*c)))).n by
SEQ_1:10
.= ((-(h"(#)((f/*(h+c)) - (f/*c))))/"((f/*(h+c))(#)(f/*c))).n by
SEQ_1:48;
end;
then
A49: h"(#) ((f^)/*(h+c) - (f^)/*c) = (-(h"(#)((f/*(h+c)) - (f/*c))))/"((f
/*(h+c ))(#) (f/*c)) by FUNCT_2:63;
A50: f/*(h+c) (#) (f/*c) is convergent by A43,A45;
then
lim(h"(#) ((f^)/*(h+c) - (f^)/*c)) = lim(-(h"(#) ((f/*(h+c))- (f/*c))
))/(f.x0)^2 by A37,A46,A47,A30,A49,SEQ_2:24
.=(- Rdiff(f,x0)) /(f.x0)^2 by A29,A28,SEQ_2:10
.=- Rdiff(f,x0) /(f.x0)^2 by XCMPLX_1:187;
hence thesis by A37,A50,A47,A30,A49,SEQ_2:23;
end;
0 < r3 by A5,A3,XXREAL_0:15;
hence thesis by A14,A21,Th15;
end;
theorem
f is_right_differentiable_in x0 & f.x0 <> 0 implies f^
is_right_differentiable_in x0 & Rdiff(f^,x0) = - Rdiff(f,x0)/(f.x0)^2
proof
assume that
A1: f is_right_differentiable_in x0 and
A2: f.x0 <> 0;
consider r1 such that
A3: r1 > 0 and
[.x0,x0 + r1.] c= dom f and
A4: for g st g in [.x0,x0 + r1.] holds f.g <> 0 by A1,A2,Th7,Th8;
now
take r1;
thus r1 > 0 by A3;
let g;
assume that
g in dom f and
A5: g in [.x0,x0+r1.];
thus f.g <> 0 by A4,A5;
end;
hence thesis by A1,Lm4;
end;
theorem
f is_right_differentiable_in x0 & f is_left_differentiable_in x0 &
Rdiff(f,x0) = Ldiff(f,x0) implies f is_differentiable_in x0 & diff(f,x0)=Rdiff(
f,x0) & diff(f,x0)=Ldiff(f,x0)
proof
assume that
A1: f is_right_differentiable_in x0 and
A2: f is_left_differentiable_in x0 and
A3: Rdiff(f,x0) = Ldiff(f,x0);
A4: ex N being Neighbourhood of x0 st N c= dom f
proof
consider r2 such that
A5: r2>0 and
A6: [.x0,x0+r2.] c= dom f by A1;
consider r1 such that
A7: r1>0 and
A8: [.x0-r1,x0.] c= dom f by A2;
set r = min(r1,r2);
r > 0 by A7,A5,XXREAL_0:15;
then reconsider N = ].x0 -r,x0+r.[ as Neighbourhood of x0 by RCOMP_1:def 6;
take N;
let x be object;
assume x in N;
then x in { g: x0 - r < g & g < x0 + r} by RCOMP_1:def 2;
then consider g such that
A9: g = x and
A10: x0 - r < g and
A11: g < x0 + r;
now
per cases;
suppose
A12: g <= x0;
r <= r1 by XXREAL_0:17;
then x0 - r1 <= x0 - r by XREAL_1:13;
then x0 - r1 <= g by A10,XXREAL_0:2;
then g in {g1: x0 - r1 <= g1 & g1 <= x0} by A12;
then g in [.x0-r1,x0.] by RCOMP_1:def 1;
hence thesis by A8,A9;
end;
suppose
A13: g > x0;
r <= r2 by XXREAL_0:17;
then x0 + r <= x0 + r2 by XREAL_1:7;
then g <= x0 + r2 by A11,XXREAL_0:2;
then g in {g1: x0 <= g1 & g1 <= x0+r2} by A13;
then g in [.x0,x0+r2.] by RCOMP_1:def 1;
hence thesis by A6,A9;
end;
end;
hence thesis;
end;
for h,c st rng c = {x0} & rng (h + c) c= dom f holds h"(#)(f/*(h+c) - f
/*c) is convergent & lim (h"(#) (f/*(h+c) - f/*c)) = Ldiff(f,x0)
proof
let h,c;
assume that
A14: rng c = {x0} and
A15: rng (h + c) c= dom f;
A16: rng c c= dom f
proof
consider S being Neighbourhood of x0 such that
A17: S c= dom f by A4;
x0 in S by RCOMP_1:16;
hence thesis by A14,A17,ZFMISC_1:31;
end;
now
per cases;
suppose
ex N be Element of NAT st for n st n >= N holds h.n > 0;
then consider N be Element of NAT such that
A18: for n st n >= N holds h.n > 0;
set h1 = h ^\N;
A19: for n being Nat holds h1.n > 0
proof
let n be Nat;
h1.n = h.(n+N) & N + 0 <= n + N by NAT_1:def 3,XREAL_1:7;
hence thesis by A18;
end;
set c1 = c ^\N;
A20: rng c1 = {x0}
proof
thus rng c1 c= {x0} by A14,VALUED_0:21;
let x be object;
A21: c.N in rng c by VALUED_0:28;
assume x in {x0};
then
A22: x = x0 by TARSKI:def 1;
c1.0 = c.(0+N) by NAT_1:def 3
.= c.N;
then c1.0 = x by A14,A22,A21,TARSKI:def 1;
hence thesis by VALUED_0:28;
end;
A23: h1 + c1 = (h + c)^\N by SEQM_3:15;
then
A24: h1"(#)(f/*(h1+c1) - f/*c1) = h1"(#)((f/*(h+c))^\N - f/*c1) by A15,
VALUED_0:27
.= h1"(#)((f/*(h+c))^\N - (f/*c)^\N) by A16,VALUED_0:27
.= h1"(#)((f/*(h+c) - f/*c)^\N) by SEQM_3:17
.= ((h")^\N) (#)((f/*(h+c) - f/*c)^\N) by SEQM_3:18
.= (h"(#)(f/*(h+c) - f/*c))^\N by SEQM_3:19;
rng (h1 + c1) c= rng (h + c) by A23,VALUED_0:21;
then
A25: rng (h1 + c1) c= dom f by A15;
then
A26: h1"(#)(f/*(h1+c1) - f/*c1) is convergent by A1,A20,A19;
hence h"(#)(f/*(h+c) - f/*c) is convergent by A24,SEQ_4:21;
lim (h1"(#)(f/*(h1+c1) - f/*c1)) = Rdiff(f,x0) by A1,A20,A25,A19,Th15;
hence lim (h"(#)(f/*(h+c) - f/*c)) =Ldiff(f,x0) by A3,A26,A24,SEQ_4:22;
end;
suppose
A27: for N be Element of NAT ex n st n >= N & h.n <= 0;
now
per cases;
suppose
ex M be Element of NAT st for m st m >= M holds h.m < 0;
then consider M be Element of NAT such that
A28: for n st n >= M holds h.n < 0;
set h1 = h ^\M;
A29: for n being Nat holds h1.n < 0
proof
let n be Nat;
h1.n = h.(n+M) & M + 0 <= n + M by NAT_1:def 3,XREAL_1:7;
hence thesis by A28;
end;
set c1 = c ^\M;
A30: rng c1 = {x0}
proof
thus rng c1 c= {x0} by A14,VALUED_0:21;
let x be object;
A31: c.M in rng c by VALUED_0:28;
assume x in {x0};
then
A32: x = x0 by TARSKI:def 1;
c1.0 = c.(0+M) by NAT_1:def 3
.= c.M;
then c1.0 = x by A14,A32,A31,TARSKI:def 1;
hence thesis by VALUED_0:28;
end;
A33: h1 + c1 = (h + c)^\M by SEQM_3:15;
then
A34: h1"(#)(f/*(h1+c1) - f/*c1) = h1"(#)((f/*(h+c))^\M - f/*c1) by A15,
VALUED_0:27
.= h1"(#)((f/*(h+c))^\M - (f/*c)^\M) by A16,VALUED_0:27
.= h1"(#)((f/*(h+c) - f/*c)^\M) by SEQM_3:17
.= ((h")^\M) (#)((f/*(h+c) - f/*c)^\M) by SEQM_3:18
.= (h"(#)(f/*(h+c) - f/*c))^\M by SEQM_3:19;
rng (h1 + c1) c= rng (h + c) by A33,VALUED_0:21;
then
A35: rng (h1 + c1) c= dom f by A15;
then
A36: h1"(#)(f/*(h1+c1) - f/*c1) is convergent by A2,A30,A29;
hence h"(#)(f/*(h+c) - f/*c) is convergent by A34,SEQ_4:21;
lim (h1"(#)(f/*(h1+c1) - f/*c1)) = Ldiff(f,x0) by A2,A30,A35,A29
,Th9;
hence lim (h"(#)(f/*(h+c) - f/*c)) =Ldiff(f,x0) by A36,A34,SEQ_4:22
;
end;
suppose
A37: for M be Element of NAT ex m st m >= M & h.m >= 0;
set s = (h")(#)(f/*(h+c)-f/*c);
defpred R[Real] means $1 > 0;
defpred P[Real] means $1 < 0;
A38: for N be Element of NAT ex n st n >= N & P[h.n]
proof
let m;
consider n such that
A39: n >= m and
A40: h.n <= 0 by A27;
take n;
thus n >= m by A39;
h.n <> 0 by SEQ_1:5;
hence thesis by A40;
end;
consider q1 being increasing sequence of NAT such that
A41: (for n being Nat holds P[(h*q1).n]) &
for n st (for r st r = h.n
holds P[r]) ex m st n = q1.m from FDIFF_2:sch 1(A38);
A42: for N be Element of NAT ex n st n >= N & R[h.n]
proof
let m;
consider n such that
A43: n >= m and
A44: h.n >= 0 by A37;
take n;
thus n >= m by A43;
h.n <> 0 by SEQ_1:5;
hence thesis by A44;
end;
consider q2 being increasing sequence of NAT such that
A45: (for n being Nat holds R[(h*q2).n]) &
for n st (for r st r = h.n
holds R[r]) ex m st n = q2.m from FDIFF_2:sch 1(A42);
set h1 = h*q1;
reconsider h1 as subsequence of h;
A46: h1 is convergent by SEQ_4:16;
A47: lim h = 0;
then
A48: lim h1 = 0 by SEQ_4:17;
set h2 = h*q2;
A49: h2 is convergent by SEQ_4:16;
lim h2 = 0 by A47,SEQ_4:17;
then reconsider h2 as 0-convergent non-zero Real_Sequence
by A49,FDIFF_1:def 1;
set c2 = c*q2;
A50: rng c2 = {x0} by A14,VALUED_0:26;
reconsider c2 as constant Real_Sequence;
rng ((h+c)*q2) c= rng (h+c) by VALUED_0:21;
then rng ((h+c)*q2) c= dom f by A15;
then rng (h2+c2) c= dom f by RFUNCT_2:2;
then
A51: h2"(#)(f/*(h2+c2)-f/*c2) is convergent & lim(h2"(#)(f/*(h2+
c2)-f/*c2))=Ldiff (f,x0) by A1,A3,A45,A50,Th15;
A52: h2"(#)(f/*(h2+c2)-f/*c2) = h2"(#)(f/*((h+c)*q2)-f/*c2) by
RFUNCT_2:2
.= h2"(#)(f/*(h+c)*q2-f/*c2) by A15,FUNCT_2:110
.= ((h")*q2)(#)(f/*(h+c)*q2-f/*c2) by RFUNCT_2:5
.= ((h")*q2)(#)(f/*(h+c)*q2-f/*c*q2) by A16,FUNCT_2:110
.= ((h")*q2)(#)((f/*(h+c)-f/*c)*q2) by RFUNCT_2:2
.= ((h")(#)(f/*(h+c)-f/*c))*q2 by RFUNCT_2:2;
reconsider h1 as 0-convergent non-zero Real_Sequence
by A46,A48,FDIFF_1:def 1;
set c1 = c*q1;
A53: rng c1 = {x0} by A14,VALUED_0:26;
reconsider c1 as constant Real_Sequence;
rng ((h+c)*q1) c= rng (h+c) by VALUED_0:21;
then rng ((h+c)*q1) c= dom f by A15;
then rng (h1+c1) c= dom f by RFUNCT_2:2;
then
A54: h1"(#)(f/*(h1+c1)-f/*c1) is convergent & lim(h1"(#)(f/*(h1+
c1)-f/*c1))=Ldiff (f,x0) by A2,A41,A53,Th9;
A55: h1"(#)(f/*(h1+c1)-f/*c1) = h1"(#)(f/*((h+c)*q1)-f/*c1) by
RFUNCT_2:2
.= h1"(#)(f/*(h+c)*q1-f/*c1) by A15,FUNCT_2:110
.= ((h")*q1)(#)(f/*(h+c)*q1-f/*c1) by RFUNCT_2:5
.= ((h")*q1)(#)(f/*(h+c)*q1-f/*c*q1) by A16,FUNCT_2:110
.= ((h")*q1)(#)((f/*(h+c)-f/*c)*q1) by RFUNCT_2:2
.= ((h")(#)(f/*(h+c)-f/*c))*q1 by RFUNCT_2:2;
A56: for g1 be Real st 0= q2.n2 by XXREAL_0:25;
A63: n >= q1.n1 by XXREAL_0:25;
per cases;
suppose
h.m > 0;
then for r st r = h.m holds r > 0;
then consider k such that
A64: m = q2.k by A45,A61;
A65: n2 in NAT by ORDINAL1:def 12;
dom q2 = NAT & q2.k >= q2.n2 by A60,A62,A64,FUNCT_2:def 1
,XXREAL_0:2;
then not k < n2 by VALUED_0:def 13,A65;
then |.(s*q2).k - Ldiff(f,x0).| 0 by SEQ_1:5;
then for r st r = h.m holds r < 0 by A66;
then consider k such that
A67: m = q1.k by A41,A61;
A68: n1 in NAT by ORDINAL1:def 12;
dom q1 = NAT & q1.k >= q1.n1 by A60,A63,A67,FUNCT_2:def 1
,XXREAL_0:2;
then not k < n1 by VALUED_0:def 13,A68;
then |.(s*q1).k - Ldiff(f,x0).| 0 and
A4: N = ].x0 - g1,x0 + g1.[ by RCOMP_1:def 6;
A5: g1 > g1/2 by A3,XREAL_1:216;
A6: ex r st r>0 & [.x0,x0+r.] c= dom f
proof
take r = g1/2;
thus r > 0 by A3,XREAL_1:215;
|.(x0 + g1/2) -x0 .| = g1/2 by A3,ABSVALUE:def 1;
then
A7: x0 + r in ].x0 -g1,x0 +g1.[ by A5,RCOMP_1:1;
x0 in ].x0 - g1, x0 + g1 .[ by A4,RCOMP_1:16;
then [.x0,x0 +r.] c= ].x0 -g1,x0 +g1.[ by A7,XXREAL_2:def 12;
hence thesis by A2,A4;
end;
A8: ex r st 0 < r & [.x0 -r,x0.] c= dom f
proof
take r = g1/2;
thus r > 0 by A3,XREAL_1:215;
|.(x0 - g1/2) -x0 .| =|.-g1/2 + 0 .| .=|.g1/2 .|by COMPLEX1:52
.=g1/2 by A3,ABSVALUE:def 1;
then
A9: x0 - r in ].x0 -g1,x0 +g1.[ by A5,RCOMP_1:1;
x0 in ].x0 - g1, x0 + g1 .[ by A4,RCOMP_1:16;
then [.x0 -r,x0 .] c= ].x0 -g1,x0 +g1.[ by A9,XXREAL_2:def 12;
hence thesis by A2,A4;
end;
diff(f,x0) = diff(f,x0);
then ( for h,c st rng c = {x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n>0)
holds h" (#)(f/*(h+c) - f/*c) is convergent & lim (h"(#) (f/*(h+c) - f/*c)) =
diff(f,x0) )& for h,c st rng c = {x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n <
0) holds h"(#)(f/*(h+c) - f/*c) is convergent & lim(h"(#)(f/*(h+c) - f/*c)) =
diff(f,x0) by A1,FDIFF_2:12;
hence thesis by A6,A8,Th9,Th15;
end;