:: Differentiable Functions into Real Normed Spaces
:: by Hiroyuki Okazaki , Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received October 13, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

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

theorem Th1: :: NDIFF_3:1
for G being RealNormSpace
for s1 being Real_Sequence
for seq being sequence of G st ( for n being Element of NAT holds ||.(seq . n).|| <= s1 . n ) &amp; s1 is convergent &amp; lim s1 = 0 holds
( seq is convergent &amp; lim seq = 0. G )
proofend;

theorem Th2: :: NDIFF_3:2
for G being RealNormSpace
for k being Element of NAT
for s1 being Real_Sequence
for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k
proofend;

definition
let F be non trivial RealNormSpace;
let IT be PartFunc of REAL, the carrier of F;
attrIT is RestFunc-like  means :Def1: :: NDIFF_3:def 1
( IT is total &amp; ( for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (IT /* h) is convergent &amp; lim ((h ") (#) (IT /* h)) = 0. F ) ) );
end;

:: deftheorem Def1 defines RestFunc-like NDIFF_3:def_1_:_
 for F being non trivial RealNormSpace
for IT being PartFunc of REAL, the carrier of F holds
( IT is RestFunc-like iff ( IT is total &amp; ( for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (IT /* h) is convergent &amp; lim ((h ") (#) (IT /* h)) = 0. F ) ) ) );

registration
let F be non trivial RealNormSpace;
clusterV13() V16( REAL ) V17( the carrier of F) Function-like RestFunc-like for Element of K6(K7(REAL, the carrier of F));
existence
 ex b1 being PartFunc of REAL, the carrier of F st b1 is RestFunc-like
proofend;
end;

definition
let F be non trivial RealNormSpace;
mode RestFunc of F is RestFunc-like PartFunc of REAL, the carrier of F;
end;

definition
let F be non trivial RealNormSpace;
let IT be Function of REAL, the carrier of F;
attrIT is linear  means :Def2: :: NDIFF_3:def 2
 ex r being Point of F st
for p being Real holds IT . p = p * r;
end;

:: deftheorem Def2 defines linear NDIFF_3:def_2_:_
 for F being non trivial RealNormSpace
for IT being Function of REAL, the carrier of F holds
( IT is linear iff ex r being Point of F st
for p being Real holds IT . p = p * r );

registration
let F be non trivial RealNormSpace;
clusterV1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total linear for Element of K6(K7(REAL, the carrier of F));
existence
 ex b1 being Function of REAL, the carrier of F st b1 is linear
proofend;
end;

definition
let F be non trivial RealNormSpace;
mode LinearFunc of F is linear Function of REAL, the carrier of F;
end;

theorem Th3: :: NDIFF_3:3
for F being non trivial RealNormSpace
for L1, L2 being LinearFunc of F holds
( L1 + L2 is LinearFunc of F &amp; L1 - L2 is LinearFunc of F )
proofend;

theorem Th4: :: NDIFF_3:4
for F being non trivial RealNormSpace
for r being Real
for L being LinearFunc of F holds r (#) L is LinearFunc of F
proofend;

theorem Th5: :: NDIFF_3:5
for F being non trivial RealNormSpace
for h1, h2 being PartFunc of REAL, the carrier of F
for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) &amp; (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
proofend;

theorem Th6: :: NDIFF_3:6
for F being non trivial RealNormSpace
for h1, h2 being PartFunc of REAL, the carrier of F
for seq being Real_Sequence st h1 is total &amp; h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) &amp; (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
proofend;

theorem Th7: :: NDIFF_3:7
for F being non trivial RealNormSpace
for R1, R2 being RestFunc of F holds
( R1 + R2 is RestFunc of F &amp; R1 - R2 is RestFunc of F )
proofend;

theorem Th8: :: NDIFF_3:8
for F being non trivial RealNormSpace
for r being Real
for R being RestFunc of F holds r (#) R is RestFunc of F
proofend;

definition
let F be non trivial RealNormSpace;
let f be PartFunc of REAL, the carrier of F;
let x0 be real number ;
predf is_differentiable_in x0 means :Def3: :: NDIFF_3:def 3
 ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) );
end;

:: deftheorem Def3 defines is_differentiable_in NDIFF_3:def_3_:_
 for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for x0 being real number holds
( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) );

definition
let F be non trivial RealNormSpace;
let f be PartFunc of REAL, the carrier of F;
let x0 be real number ;
assume A1: f is_differentiable_in x0 ;
func diff (f,x0) ->  Point of F means :Def4: :: NDIFF_3:def 4
 ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex L being LinearFunc of F ex R being RestFunc of F st
( it = L . 1 &amp; ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) );
existence
 ex b1 being Point of F ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex L being LinearFunc of F ex R being RestFunc of F st
( b1 = L . 1 &amp; ( 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 Point of F st ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex L being LinearFunc of F ex R being RestFunc of F st
( b1 = L . 1 &amp; ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) &amp; ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex L being LinearFunc of F ex R being RestFunc of F st
( b2 = L . 1 &amp; ( 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 Def4 defines diff NDIFF_3:def_4_:_
 for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for x0 being real number st f is_differentiable_in x0 holds
for b4 being Point of F holds
( b4 = diff (f,x0) iff ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex L being LinearFunc of F ex R being RestFunc of F st
( b4 = L . 1 &amp; ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ) ) );

definition
let F be non trivial RealNormSpace;
let f be PartFunc of REAL, the carrier of F;
let X be set ;
predf is_differentiable_on X means :Def5: :: NDIFF_3:def 5
( X c= dom f &amp; ( for x being Real st x in X holds
f | X is_differentiable_in x ) );
end;

:: deftheorem Def5 defines is_differentiable_on NDIFF_3:def_5_:_
 for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for X being set holds
( f is_differentiable_on X iff ( X c= dom f &amp; ( for x being Real st x in X holds
f | X is_differentiable_in x ) ) );

theorem Th9: :: NDIFF_3:9
for F being non trivial RealNormSpace
for X being set
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
X is Subset of REAL
proofend;

theorem Th10: :: NDIFF_3:10
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F holds
( f is_differentiable_on Z iff ( Z c= dom f &amp; ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )
proofend;

theorem :: NDIFF_3:11
for F being non trivial RealNormSpace
for Y being Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds
Y is open
proofend;

definition
let F be non trivial RealNormSpace;
let f be PartFunc of REAL, the carrier of F;
let X be set ;
assume A1: f is_differentiable_on X ;
funcf `| X ->  PartFunc of REAL, the carrier of F means :Def6: :: NDIFF_3:def 6
( dom it = X &amp; ( for x being Real st x in X holds
it . x = diff (f,x) ) );
existence
 ex b1 being PartFunc of REAL, the carrier of F st
( dom b1 = X &amp; ( for x being Real st x in X holds
b1 . x = diff (f,x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of REAL, the carrier of F st dom b1 = X &amp; ( for x being Real st x in X holds
b1 . x = diff (f,x) ) &amp; dom b2 = X &amp; ( for x being Real st x in X holds
b2 . x = diff (f,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines `| NDIFF_3:def_6_:_
 for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for X being set st f is_differentiable_on X holds
for b4 being PartFunc of REAL, the carrier of F holds
( b4 = f `| X iff ( dom b4 = X &amp; ( for x being Real st x in X holds
b4 . x = diff (f,x) ) ) );

theorem :: NDIFF_3:12
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom f &amp; ex r being Point of F st rng f = {r} holds
( f is_differentiable_on Z &amp; ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) )
proofend;

theorem Th13: :: NDIFF_3:13
for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for x0 being real number
for N being Neighbourhood of x0 st f is_differentiable_in x0 &amp; N c= dom f holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} &amp; rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent &amp; diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
proofend;

theorem Th14: :: NDIFF_3:14
for F being non trivial RealNormSpace
for x0 being Real
for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 &amp; f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 &amp; diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
proofend;

theorem Th15: :: NDIFF_3:15
for F being non trivial RealNormSpace
for x0 being Real
for f1, f2 being PartFunc of REAL, the carrier of F st f1 is_differentiable_in x0 &amp; f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 &amp; diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
proofend;

theorem Th16: :: NDIFF_3:16
for F being non trivial RealNormSpace
for x0 being Real
for f being PartFunc of REAL, the carrier of F
for r being Real st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 &amp; diff ((r (#) f),x0) = r * (diff (f,x0)) )
proofend;

theorem :: NDIFF_3:17
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 + f2) &amp; f1 is_differentiable_on Z &amp; f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) )
proofend;

theorem :: NDIFF_3:18
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 - f2) &amp; f1 is_differentiable_on Z &amp; f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )
proofend;

theorem :: NDIFF_3:19
for F being non trivial RealNormSpace
for r being Real
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom (r (#) f) &amp; f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z &amp; ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) )
proofend;

theorem :: NDIFF_3:20
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom f &amp; f | Z is constant holds
( f is_differentiable_on Z &amp; ( for x being Real st x in Z holds
(f `| Z) . x = 0. F ) )
proofend;

theorem Th21: :: NDIFF_3:21
for F being non trivial RealNormSpace
for r, p being Point of F
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom f &amp; ( for x being Real st x in Z holds
f /. x = (x * r) + p ) holds
( f is_differentiable_on Z &amp; ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
proofend;

theorem Th22: :: NDIFF_3:22
for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F
for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
proofend;

theorem :: NDIFF_3:23
for F being non trivial RealNormSpace
for X being set
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
f | X is continuous
proofend;

theorem Th24: :: NDIFF_3:24
for F being non trivial RealNormSpace
for X being set
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X &amp; Z c= X holds
f is_differentiable_on Z
proofend;

Lm1:  {} REAL is closed
proofend;

theorem :: NDIFF_3:25
for F being non trivial RealNormSpace ex R being RestFunc of F st
( R /. 0 = 0. F &amp; R is_continuous_in 0 )
proofend;

definition
let F be non trivial RealNormSpace;
let f be PartFunc of REAL, the carrier of F;
attrf is differentiable  means :Def7: :: NDIFF_3:def 7
f is_differentiable_on dom f;
end;

:: deftheorem Def7 defines differentiable NDIFF_3:def_7_:_
 for F being non trivial RealNormSpace
for f being PartFunc of REAL, the carrier of F holds
( f is differentiable iff f is_differentiable_on dom f );

Lm2:  [#] REAL is open
proofend;

registration
let F be non trivial RealNormSpace;
clusterV1() V13() V16( REAL ) V17( the carrier of F) Function-like total quasi_total differentiable for Element of K6(K7(REAL, the carrier of F));
existence
 ex b1 being Function of REAL, the carrier of F st b1 is differentiable
proofend;
end;

theorem :: NDIFF_3:26
for F being non trivial RealNormSpace
for Z being open Subset of REAL
for f being differentiable PartFunc of REAL, the carrier of F st Z c= dom f holds
f is_differentiable_on Z
proofend;