The abstract of the Mizar article:

Real Function One-Side Differentiability

by

Ewa Burakowska, and

Beata Madras

Received December 12, 1991

MML identifier: FDIFF_3

[ Mizar article, MML identifier index ]

environ

 vocabulary FDIFF_1, SEQ_1, SEQM_3, PARTFUN1, RCOMP_1, ARYTM_1, RELAT_1,
      FUNCT_1, ARYTM_3, SEQ_2, ORDINAL2, LIMFUNC1, BOOLE, ABSVALUE, SQUARE_1,
      FINSEQ_1, FDIFF_3, ARYTM;
 notation TARSKI, XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
      NAT_1, RELSET_1, PARTFUN1, SEQ_1, SEQ_2, SEQM_3, ABSVALUE, SQUARE_1,
      RFUNCT_1, RFUNCT_2, RCOMP_1, FDIFF_1, LIMFUNC1;
 constructors REAL_1, NAT_1, SEQ_2, SEQM_3, ABSVALUE, RFUNCT_1, RFUNCT_2,
      RCOMP_1, FDIFF_1, LIMFUNC1, PROB_1, PARTFUN1, MEMBERED, XBOOLE_0;
 clusters FDIFF_1, RELSET_1, XREAL_0, SEQ_1, SEQM_3, ARYTM_3, MEMBERED,
      ZFMISC_1, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve h,h1,h2 for convergent_to_0 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 Nat,
         a,b,d for Real_Sequence,
         x for set;

theorem :: FDIFF_3:1
(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 holds h.n < 0;

theorem :: FDIFF_3:2
(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 holds h.n > 0;

theorem :: FDIFF_3:3
(for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n 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 holds h1.n < 0) &
rng (h2+c) c= dom f & (for n holds h2.n < 0) holds
lim (h1"(#)(f*(h1 + c) - f*c)) = lim (h2"(#)(f*(h2 + c) - f*c));

theorem :: FDIFF_3:4
(for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n 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 holds h1.n >0) & (for n holds h2.n >0) holds
lim (h1"(#)(f*(h1+c) - f*c)) = lim (h2"(#)(f*(h2+c) - f*c));

definition let f,x0;
pred f is_Lcontinuous_in x0 means
:: FDIFF_3:def 1
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
:: FDIFF_3:def 2
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
:: FDIFF_3:def 3
(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 holds h.n > 0) holds
  h"(#)(f*(h + c) - f*c) is convergent;
pred f is_left_differentiable_in x0 means
:: FDIFF_3:def 4
(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 holds h.n<0) holds
  h"(#)(f*(h + c) - f*c) is convergent;
end;

theorem :: FDIFF_3:5
f is_left_differentiable_in x0 implies f is_Lcontinuous_in x0;

theorem :: FDIFF_3:6
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;

theorem :: FDIFF_3:7
f is_right_differentiable_in x0 implies f is_Rcontinuous_in x0;

theorem :: FDIFF_3:8
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;

definition let x0,f;
assume f is_left_differentiable_in x0;
func Ldiff (f,x0) -> Real means
:: FDIFF_3:def 5
for h,c st rng c = {x0} & rng (h + c) c= dom f & (for n holds h.n <0) holds
 it =lim (h"(#)(f*(h + c) - f*c));
end;

definition let x0 ,f;
assume  f is_right_differentiable_in x0;
func Rdiff(f,x0) -> Real means
:: FDIFF_3:def 6
for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n > 0) holds
it=lim (h"(#)(f*(h + c) - f*c));
end;

theorem :: FDIFF_3:9
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 holds h.n < 0)
holds h"(#)(f*(h + c) - f*c) is convergent & lim(h"(#)(f*(h + c) - f*c)) = g;

theorem :: FDIFF_3:10
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies
f1 + f2 is_left_differentiable_in x0 &
Ldiff(f1+f2,x0) = Ldiff(f1,x0) + Ldiff(f2,x0);

theorem :: FDIFF_3:11
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies
f1 - f2 is_left_differentiable_in x0 &
Ldiff(f1-f2,x0) = Ldiff(f1,x0) - Ldiff(f2,x0);

theorem :: FDIFF_3:12
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies
f1(#)f2 is_left_differentiable_in x0 &
Ldiff(f1(#)f2,x0) = Ldiff(f1,x0)*f2.x0 + Ldiff(f2,x0)*f1.x0;

theorem :: FDIFF_3:13
  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;

theorem :: FDIFF_3:14
  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;

theorem :: FDIFF_3:15
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 holds h.n > 0) holds
h"(#)(f*(h+c) - f*c) is convergent & lim (h"(#)(f*(h+c) - f*c)) = g1;

theorem :: FDIFF_3:16
  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);

theorem :: FDIFF_3:17
  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);

theorem :: FDIFF_3:18
  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;

theorem :: FDIFF_3:19
  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;

theorem :: FDIFF_3:20
  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;

theorem :: FDIFF_3:21
  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);

theorem :: FDIFF_3:22
  f is_differentiable_in x0 implies f is_right_differentiable_in x0 &
f is_left_differentiable_in x0 & diff(f,x0) = Rdiff(f,x0)
& diff(f,x0) = Ldiff(f,x0);