:: Real Function One-Side Differantiability
:: by Ewa Burakowska and Beata Madras
::
:: Received December 12, 1991
:: Copyright (c) 1991-2011 Association of Mizar Users

begin

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 convergent_to_0 Real_Sequence ex c being V8() Real_Sequence st
( rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of 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 convergent_to_0 Real_Sequence ex c being V8() Real_Sequence st
( rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of 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 convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f holds
for h1, h2 being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Element of NAT holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( for n being Element of 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 convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f holds
for h1, h2 being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h1 . n > 0 ) & ( for n being Element of 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 :Def1: :: FDIFF_3:def 1
( x0 in dom f & ( for a being Real_Sequence 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 :Def2: :: FDIFF_3:def 2
( x0 in dom f & ( for a being Real_Sequence 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 :Def3: :: FDIFF_3:def 3
( ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) );
pred f is_left_differentiable_in x0 means :Def4: :: FDIFF_3:def 4
( ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) );

end;

:: deftheorem Def1 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= (left_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds
( f /* a is convergent & f . x0 = lim (f /* a) ) ) ) );

:: deftheorem Def2 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= (right_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds
( f /* a is convergent & f . x0 = lim (f /* a) ) ) ) );

:: deftheorem Def3 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 convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) );

:: deftheorem Def4 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 convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of 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 convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
it = lim ((h ") (#) ((f /* (h + c)) - (f /* c)));
existence
ex b₁ being Real st
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
b₁ = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

proof end;

uniqueness
for b₁, b₂ being Real st ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
b₁ = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
b₂ = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) holds
b₁ = b₂

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 b₃ being Real holds
( b₃ = Ldiff (f,x0) iff for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
b₃ = 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 convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
it = lim ((h ") (#) ((f /* (h + c)) - (f /* c)));
existence
ex b₁ being Real st
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
b₁ = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

proof end;

uniqueness
for b₁, b₂ being Real st ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
b₁ = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
b₂ = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) holds
b₁ = b₂

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 b₃ being Real holds
( b₃ = Rdiff (f,x0) iff for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
b₃ = 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 convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of 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 convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of 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;