:: FDIFF_3 semantic presentation

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 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 convergent_to_0 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 convergent_to_0 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 convergent_to_0 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 convergent_to_0 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 convergent_to_0 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 :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 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 :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 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 Def1 defines is_Lcontinuous_in FDIFF_3:def 1 :

:: deftheorem Def2 defines is_Rcontinuous_in FDIFF_3:def 2 :

:: deftheorem Def3 defines is_right_differentiable_in FDIFF_3:def 3 :

:: deftheorem Def4 defines is_left_differentiable_in FDIFF_3:def 4 :

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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Ldiff FDIFF_3:def 5 :

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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Rdiff FDIFF_3:def 6 :

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 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 convergent_to_0 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;