:: Real Function One-Side Differantiability
:: by Ewa Burakowska and Beata Madras
::
:: Copyright (c) 1991-2018 Association of Mizar Users

theorem Th1: :: FDIFF_3:1
for f being PartFunc of REAL,REAL
for x0 being Real st ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f ) holds
ex h being non-zero 0 -convergent Real_Sequence ex c being constant Real_Sequence st
( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) )
proof end;

theorem Th2: :: FDIFF_3:2
for f being PartFunc of REAL,REAL
for x0 being Real st ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) holds
ex h being non-zero 0 -convergent Real_Sequence ex c being constant Real_Sequence st
( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) )
proof end;

theorem Th3: :: FDIFF_3:3
for f being PartFunc of REAL,REAL
for x0 being Real st ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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 holds
for h1, h2 being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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 end;

theorem Th4: :: FDIFF_3:4
for f being PartFunc of REAL,REAL
for x0 being Real st ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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 holds
for h1, h2 being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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 end;

definition
let f be PartFunc of REAL,REAL;
let x0 be Real;
pred f is_Lcontinuous_in x0 means :: FDIFF_3:def 1
( x0 in dom f & ( for a being Real_Sequence st rng a c= () /\ (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 being Real_Sequence st rng a c= () /\ (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 being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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 :: FDIFF_3:def 4
( ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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;

:: deftheorem defines is_Lcontinuous_in FDIFF_3:def 1 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_Lcontinuous_in x0 iff ( x0 in dom f & ( for a being Real_Sequence st rng a c= () /\ (dom f) & a is convergent & lim a = x0 holds
( f /* a is convergent & f . x0 = lim (f /* a) ) ) ) );

:: deftheorem defines is_Rcontinuous_in FDIFF_3:def 2 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_Rcontinuous_in x0 iff ( x0 in dom f & ( for a being Real_Sequence st rng a c= () /\ (dom f) & a is convergent & lim a = x0 holds
( f /* a is convergent & f . x0 = lim (f /* a) ) ) ) );

:: deftheorem defines is_right_differentiable_in FDIFF_3:def 3 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_right_differentiable_in x0 iff ( ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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 ) ) );

:: deftheorem defines is_left_differentiable_in FDIFF_3:def 4 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_left_differentiable_in x0 iff ( ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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 ) ) );

theorem Th5: :: FDIFF_3:5
for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_differentiable_in x0 holds
f is_Lcontinuous_in x0
proof end;

theorem Th6: :: FDIFF_3:6
for f being PartFunc of REAL,REAL
for x0, g2 being Real st f is_Lcontinuous_in x0 & f . x0 <> g2 & ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f ) holds
ex r1 being Real st
( r1 > 0 & [.(x0 - r1),x0.] c= dom f & ( for g being Real st g in [.(x0 - r1),x0.] holds
f . g <> g2 ) )
proof end;

theorem Th7: :: FDIFF_3:7
for f being PartFunc of REAL,REAL
for x0 being Real st f is_right_differentiable_in x0 holds
f is_Rcontinuous_in x0
proof end;

theorem Th8: :: FDIFF_3:8
for f being PartFunc of REAL,REAL
for x0, g2 being Real st f is_Rcontinuous_in x0 & f . x0 <> g2 & ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) holds
ex r1 being Real st
( r1 > 0 & [.x0,(x0 + r1).] c= dom f & ( for g being Real st g in [.x0,(x0 + r1).] holds
f . g <> g2 ) )
proof end;

definition
let x0 be Real;
let f be PartFunc of REAL,REAL;
assume A1: f is_left_differentiable_in x0 ;
func Ldiff (f,x0) -> Real means :Def5: :: FDIFF_3:def 5
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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
ex b1 being Real st
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
b1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))
proof end;
uniqueness
for b1, b2 being Real st ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
b1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
b2 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Ldiff FDIFF_3:def 5 :
for x0 being Real
for f being PartFunc of REAL,REAL st f is_left_differentiable_in x0 holds
for b3 being Real holds
( b3 = Ldiff (f,x0) iff for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
b3 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) );

definition
let x0 be Real;
let f be PartFunc of REAL,REAL;
assume A1: f is_right_differentiable_in x0 ;
func Rdiff (f,x0) -> Real means :Def6: :: FDIFF_3:def 6
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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
ex b1 being Real st
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
b1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))
proof end;
uniqueness
for b1, b2 being Real st ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
b1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
b2 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Rdiff FDIFF_3:def 6 :
for x0 being Real
for f being PartFunc of REAL,REAL st f is_right_differentiable_in x0 holds
for b3 being Real holds
( b3 = Rdiff (f,x0) iff for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
b3 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) );

theorem Th9: :: FDIFF_3:9
for f being PartFunc of REAL,REAL
for x0, g being Real holds
( f is_left_differentiable_in x0 & Ldiff (f,x0) = g iff ( ex r being Real st
( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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 end;

theorem :: FDIFF_3:10
for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds
( f1 + f2 is_left_differentiable_in x0 & Ldiff ((f1 + f2),x0) = (Ldiff (f1,x0)) + (Ldiff (f2,x0)) )
proof end;

theorem :: FDIFF_3:11
for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds
( f1 - f2 is_left_differentiable_in x0 & Ldiff ((f1 - f2),x0) = (Ldiff (f1,x0)) - (Ldiff (f2,x0)) )
proof end;

theorem :: FDIFF_3:12
for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds
( f1 (#) f2 is_left_differentiable_in x0 & Ldiff ((f1 (#) f2),x0) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) )
proof end;

Lm1: for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f2 & g in [.(x0 - r0),x0.] holds
f2 . g <> 0 ) ) holds
( 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 end;

theorem :: FDIFF_3:13
for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & f2 . x0 <> 0 holds
( 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 end;

Lm2: for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f & g in [.(x0 - r0),x0.] holds
f . g <> 0 ) ) holds
( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )

proof end;

theorem :: FDIFF_3:14
for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_differentiable_in x0 & f . x0 <> 0 holds
( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )
proof end;

theorem Th15: :: FDIFF_3:15
for f being PartFunc of REAL,REAL
for x0, g1 being Real holds
( f is_right_differentiable_in x0 & Rdiff (f,x0) = g1 iff ( ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence 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 end;

theorem :: FDIFF_3:16
for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 holds
( f1 + f2 is_right_differentiable_in x0 & Rdiff ((f1 + f2),x0) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) )
proof end;

theorem :: FDIFF_3:17
for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 holds
( f1 - f2 is_right_differentiable_in x0 & Rdiff ((f1 - f2),x0) = (Rdiff (f1,x0)) - (Rdiff (f2,x0)) )
proof end;

theorem :: FDIFF_3:18
for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 holds
( f1 (#) f2 is_right_differentiable_in x0 & Rdiff ((f1 (#) f2),x0) = ((Rdiff (f1,x0)) * (f2 . x0)) + ((Rdiff (f2,x0)) * (f1 . x0)) )
proof end;

Lm3: for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f2 & g in [.x0,(x0 + r0).] holds
f2 . g <> 0 ) ) holds
( 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 end;

theorem :: FDIFF_3:19
for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 & f2 . x0 <> 0 holds
( 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 end;

Lm4: for f being PartFunc of REAL,REAL
for x0 being Real st f is_right_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f & g in [.x0,(x0 + r0).] holds
f . g <> 0 ) ) holds
( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )

proof end;

theorem :: FDIFF_3:20
for f being PartFunc of REAL,REAL
for x0 being Real st f is_right_differentiable_in x0 & f . x0 <> 0 holds
( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )
proof end;

theorem :: FDIFF_3:21
for f being PartFunc of REAL,REAL
for x0 being Real st f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & Rdiff (f,x0) = Ldiff (f,x0) holds
( f is_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )
proof end;

theorem :: FDIFF_3:22
for f being PartFunc of REAL,REAL
for x0 being Real st f is_differentiable_in x0 holds
( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )
proof end;