:: Real Function Differentiability
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: FDIFF_1:1
for Y being Subset of REAL holds
( ( for r being Real holds
( r in Y iff r in REAL ) ) iff Y = REAL )
proofend;

definition
let x be real number ;
let IT be Real_Sequence;
attrIT is x -convergent  means :Def1: :: FDIFF_1:def 1
( IT is convergent & lim IT = x );
end;

:: deftheorem Def1 defines -convergent FDIFF_1:def_1_:_
 for x being real number
for IT being Real_Sequence holds
( IT is x -convergent iff ( IT is convergent & lim IT = x ) );

registration
clusterV1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent for Element of K19(K20(NAT,REAL));
existence
 ex b1 being Real_Sequence st
( b1 is 0 -convergent & b1 is non-zero )
proofend;
end;

registration
let f be 0 -convergent Real_Sequence;
cluster lim f ->  empty ;
coherence
 lim f is empty
proofend;
end;

registration
clusterV6() quasi_total 0 -convergent  ->  convergent for Element of K19(K20(NAT,REAL));
coherence
 for b1 being Real_Sequence st b1 is 0 -convergent holds
b1 is convergent
proofend;
end;

reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:45;

definition
let IT be PartFunc of REAL,REAL;
attrIT is RestFunc-like  means :Def2: :: FDIFF_1:def 2
( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) ) );
end;

:: deftheorem Def2 defines RestFunc-like FDIFF_1:def_2_:_
 for IT being PartFunc of REAL,REAL holds
( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) ) ) );

reconsider cf = REAL --> 0 as Function of REAL,REAL by FUNCOP_1:45;

registration
clusterV1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued RestFunc-like for Element of K19(K20(REAL,REAL));
existence
 ex b1 being PartFunc of REAL,REAL st b1 is RestFunc-like
proofend;
end;

definition
mode RestFunc is RestFunc-like PartFunc of REAL,REAL;
end;

definition
let IT be PartFunc of REAL,REAL;
attrIT is linear  means :Def3: :: FDIFF_1:def 3
( IT is total & ex r being Real st
for p being Real holds IT . p = r * p );
end;

:: deftheorem Def3 defines linear FDIFF_1:def_3_:_
 for IT being PartFunc of REAL,REAL holds
( IT is linear iff ( IT is total & ex r being Real st
for p being Real holds IT . p = r * p ) );

registration
clusterV1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued linear for Element of K19(K20(REAL,REAL));
existence
 ex b1 being PartFunc of REAL,REAL st b1 is linear
proofend;
end;

definition
mode LinearFunc is linear PartFunc of REAL,REAL;
end;

theorem Th2: :: FDIFF_1:2
for L1, L2 being LinearFunc holds
( L1 + L2 is LinearFunc & L1 - L2 is LinearFunc )
proofend;

theorem Th3: :: FDIFF_1:3
for r being Real
for L being LinearFunc holds r (#) L is LinearFunc
proofend;

theorem Th4: :: FDIFF_1:4
for R1, R2 being RestFunc holds
( R1 + R2 is RestFunc & R1 - R2 is RestFunc & R1 (#) R2 is RestFunc )
proofend;

theorem Th5: :: FDIFF_1:5
for r being Real
for R being RestFunc holds r (#) R is RestFunc
proofend;

theorem Th6: :: FDIFF_1:6
for L1, L2 being LinearFunc holds L1 (#) L2 is RestFunc-like
proofend;

theorem Th7: :: FDIFF_1:7
for R being RestFunc
for L being LinearFunc holds
( R (#) L is RestFunc & L (#) R is RestFunc )
proofend;

definition
let f be PartFunc of REAL,REAL;
let x0 be real number ;
predf is_differentiable_in x0 means :Def4: :: FDIFF_1:def 4
 ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) );
end;

:: deftheorem Def4 defines is_differentiable_in FDIFF_1:def_4_:_
 for f being PartFunc of REAL,REAL
for x0 being real number holds
( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) );

definition
let f be PartFunc of REAL,REAL;
let x0 be real number ;
assume A1: f is_differentiable_in x0 ;
func diff (f,x0) ->  Real means :Def5: :: FDIFF_1:def 5
 ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
( it = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );
existence
 ex b1 being Real ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
proofend;
uniqueness
 for b1, b2 being Real st ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
( b2 = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines diff FDIFF_1:def_5_:_
 for f being PartFunc of REAL,REAL
for x0 being real number st f is_differentiable_in x0 holds
for b3 being Real holds
( b3 = diff (f,x0) iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
( b3 = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let X be set ;
predf is_differentiable_on X means :Def6: :: FDIFF_1:def 6
( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) );
end;

:: deftheorem Def6 defines is_differentiable_on FDIFF_1:def_6_:_
 for f being PartFunc of REAL,REAL
for X being set holds
( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) ) );

theorem Th8: :: FDIFF_1:8
for X being set
for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
X is Subset of REAL
proofend;

theorem Th9: :: FDIFF_1:9
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )
proofend;

theorem :: FDIFF_1:10
for Y being Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on Y holds
Y is open
proofend;

definition
let f be PartFunc of REAL,REAL;
let X be set ;
assume A1: f is_differentiable_on X ;
funcf `| X ->  PartFunc of REAL,REAL means :Def7: :: FDIFF_1:def 7
( dom it = X & ( for x being Real st x in X holds
it . x = diff (f,x) ) );
existence
 ex b1 being PartFunc of REAL,REAL st
( dom b1 = X & ( for x being Real st x in X holds
b1 . x = diff (f,x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of REAL,REAL st dom b1 = X & ( for x being Real st x in X holds
b1 . x = diff (f,x) ) & dom b2 = X & ( for x being Real st x in X holds
b2 . x = diff (f,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines `| FDIFF_1:def_7_:_
 for f being PartFunc of REAL,REAL
for X being set st f is_differentiable_on X holds
for b3 being PartFunc of REAL,REAL holds
( b3 = f `| X iff ( dom b3 = X & ( for x being Real st x in X holds
b3 . x = diff (f,x) ) ) );

theorem :: FDIFF_1:11
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & ex r being Real st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
proofend;

registration
let h be non-zero 0 -convergent Real_Sequence;
let n be Element of NAT ;
clusterh ^\ n ->  non-zero 0 -convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = h ^\ n holds
( b1 is non-zero & b1 is 0 -convergent )
proofend;
end;

theorem Th12: :: FDIFF_1:12
for f being PartFunc of REAL,REAL
for x0 being real number
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
proofend;

theorem Th13: :: FDIFF_1:13
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
proofend;

theorem Th14: :: FDIFF_1:14
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
proofend;

theorem Th15: :: FDIFF_1:15
for x0, r being Real
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
proofend;

theorem Th16: :: FDIFF_1:16
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0))) )
proofend;

theorem Th17: :: FDIFF_1:17
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) )
proofend;

theorem :: FDIFF_1:18
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) )
proofend;

theorem :: FDIFF_1:19
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )
proofend;

theorem :: FDIFF_1:20
for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) )
proofend;

theorem :: FDIFF_1:21
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 (#) f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 (#) f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 (#) f2) `| Z) . x = ((f2 . x) * (diff (f1,x))) + ((f1 . x) * (diff (f2,x))) ) )
proofend;

theorem :: FDIFF_1:22
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & f | Z is V8() holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
proofend;

theorem :: FDIFF_1:23
for r, p being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds
f . x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
proofend;

theorem Th24: :: FDIFF_1:24
for f being PartFunc of REAL,REAL
for x0 being real number st f is_differentiable_in x0 holds
f is_continuous_in x0
proofend;

theorem :: FDIFF_1:25
for X being set
for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
f | X is continuous
proofend;

theorem Th26: :: FDIFF_1:26
for X being set
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
proofend;

theorem :: FDIFF_1:27
ex R being RestFunc st
( R . 0 = 0 & R is_continuous_in 0 )
proofend;

definition
let f be PartFunc of REAL,REAL;
attrf is differentiable  means :Def8: :: FDIFF_1:def 8
f is_differentiable_on dom f;
end;

:: deftheorem Def8 defines differentiable FDIFF_1:def_8_:_
 for f being PartFunc of REAL,REAL holds
( f is differentiable iff f is_differentiable_on dom f );

Lm1:  {} REAL is closed
proofend;

Lm2:  [#] REAL is open
proofend;

registration
clusterV1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued differentiable for Element of K19(K20(REAL,REAL));
existence
 ex b1 being Function of REAL,REAL st b1 is differentiable
proofend;
end;

theorem :: FDIFF_1:28
for Z being open Subset of REAL
for f being differentiable PartFunc of REAL,REAL st Z c= dom f holds
f is_differentiable_on Z
proofend;