:: The Differentiable Functions on Normed Linear Spaces
:: by Hiroshi Imura , Morishige Kimura and Yasunari Shidama
::
:: Received May 24, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

:: Normed Linear Spaces varsions of RCOMP_1:37 -
:: RCOMP_1:37 --> NFCONT_1:4
theorem Th1: :: NDIFF_1:1
for S being RealNormSpace
for x0 being Point of S
for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st
( N c= N1 & N c= N2 )
proofend;

theorem Th2: :: NDIFF_1:2
for S being RealNormSpace
for X being Subset of S st X is open holds
for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X
proofend;

theorem :: NDIFF_1:3
for S being RealNormSpace
for X being Subset of S st X is open holds
for r being Point of S st r in X holds
ex g being Real st
( 0 < g &amp;  {  y where y is Point of S : ||.(y - r).|| < g  }  c= X )
proofend;

theorem Th4: :: NDIFF_1:4
for S being RealNormSpace
for X being Subset of S st ( for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X ) holds
X is open
proofend;

theorem :: NDIFF_1:5
for S being RealNormSpace
for X being Subset of S holds
( ( for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X ) iff X is open ) by Th2, Th4;

:: Normed Linear Spaces versions of SEQ_1: -
definition
let X be set ;
let S be ZeroStr ;
let f be Function of X,S;
redefine attr f is non-zero  means :Def1: :: NDIFF_1:def 1
 rng f c= NonZero S;
compatibility
 ( f is non-zero iff rng f c= NonZero S )
proofend;
end;

:: deftheorem Def1 defines non-zero NDIFF_1:def_1_:_
 for X being set
for S being ZeroStr
for f being Function of X,S holds
( f is non-zero iff rng f c= NonZero S );

theorem Th6: :: NDIFF_1:6
for S being RealNormSpace
for seq being sequence of S holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0. S )
proofend;

theorem Th7: :: NDIFF_1:7
for S being RealNormSpace
for seq being sequence of S holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. S )
proofend;

definition
let RNS be RealLinearSpace;
let S be sequence of RNS;
let a be Real_Sequence;
funca (#) S ->  sequence of RNS means :Def2: :: NDIFF_1:def 2
 for n being Element of NAT holds it . n = (a . n) * (S . n);
existence
 ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = (a . n) * (S . n)
proofend;
uniqueness
 for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (a . n) * (S . n) ) &amp; ( for n being Element of NAT holds b2 . n = (a . n) * (S . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines (#) NDIFF_1:def_2_:_
 for RNS being RealLinearSpace
for S being sequence of RNS
for a being Real_Sequence
for b4 being sequence of RNS holds
( b4 = a (#) S iff for n being Element of NAT holds b4 . n = (a . n) * (S . n) );

definition
let RNS be RealLinearSpace;
let z be Point of RNS;
let a be Real_Sequence;
funca * z ->  sequence of RNS means :Def3: :: NDIFF_1:def 3
 for n being Element of NAT holds it . n = (a . n) * z;
existence
 ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = (a . n) * z
proofend;
uniqueness
 for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (a . n) * z ) &amp; ( for n being Element of NAT holds b2 . n = (a . n) * z ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines * NDIFF_1:def_3_:_
 for RNS being RealLinearSpace
for z being Point of RNS
for a being Real_Sequence
for b4 being sequence of RNS holds
( b4 = a * z iff for n being Element of NAT holds b4 . n = (a . n) * z );

theorem :: NDIFF_1:8
for S being RealNormSpace
for seq being sequence of S
for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq)
proofend;

theorem Th9: :: NDIFF_1:9
for S being RealNormSpace
for rseq being Real_Sequence
for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)
proofend;

theorem Th10: :: NDIFF_1:10
for r being Real
for S being RealNormSpace
for seq being sequence of S
for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq)
proofend;

theorem :: NDIFF_1:11
for S being RealNormSpace
for seq being sequence of S
for rseq1, rseq2 being Real_Sequence holds (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq)
proofend;

theorem Th12: :: NDIFF_1:12
for S being RealNormSpace
for rseq being Real_Sequence
for seq1, seq2 being sequence of S holds rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2)
proofend;

theorem Th13: :: NDIFF_1:13
for S being RealNormSpace
for rseq being Real_Sequence
for seq being sequence of S st rseq is convergent &amp; seq is convergent holds
rseq (#) seq is convergent
proofend;

theorem Th14: :: NDIFF_1:14
for S being RealNormSpace
for rseq being Real_Sequence
for seq being sequence of S st rseq is convergent &amp; seq is convergent holds
lim (rseq (#) seq) = (lim rseq) * (lim seq)
proofend;

theorem Th15: :: NDIFF_1:15
for k being Element of NAT
for S being RealNormSpace
for seq, seq1 being sequence of S holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
proofend;

theorem Th16: :: NDIFF_1:16
for k being Element of NAT
for S being RealNormSpace
for seq, seq1 being sequence of S holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
proofend;

theorem Th17: :: NDIFF_1:17
for k being Element of NAT
for S being RealNormSpace
for seq being sequence of S st seq is non-zero holds
seq ^\ k is non-zero
proofend;

definition
let S be RealNormSpace;
let x be Point of S;
let IT be sequence of S;
attrIT is x -convergent  means :Def4: :: NDIFF_1:def 4
( IT is convergent &amp; lim IT = x );
end;

:: deftheorem Def4 defines -convergent NDIFF_1:def_4_:_
 for S being RealNormSpace
for x being Point of S
for IT being sequence of S holds
( IT is x -convergent iff ( IT is convergent &amp; lim IT = x ) );

theorem Th18: :: NDIFF_1:18
for X being RealNormSpace
for seq being sequence of X st seq is constant holds
( seq is convergent &amp; ( for k being Element of NAT holds lim seq = seq . k ) )
proofend;

theorem Th19: :: NDIFF_1:19
for S being RealNormSpace
for seq being sequence of S
for x0 being Point of S
for r being Real st 0 < r &amp; ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
seq is convergent
proofend;

theorem Th20: :: NDIFF_1:20
for S being RealNormSpace
for seq being sequence of S
for x0 being Point of S
for r being Real st 0 < r &amp; ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
lim seq = 0. S
proofend;

registration
let S be non trivial RealNormSpace;
clusterV1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total non-zero 0. S -convergent for Element of K6(K7(NAT, the carrier of S));
existence
 ex b1 being sequence of S st
( b1 is non-zero &amp; b1 is 0. S -convergent )
proofend;
end;

theorem :: NDIFF_1:21
for S being RealNormSpace
for a being non-zero 0 -convergent Real_Sequence
for z being Point of S st z <> 0. S holds
( a * z is non-zero &amp; a * z is 0. S -convergent )
proofend;

theorem :: NDIFF_1:22
for S being RealNormSpace
for Y being Subset of S holds
( ( for r being Point of S holds
( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S )
proofend;

registration
let S be non trivial RealNormSpace;
clusterV1() V16() V19( NAT ) V20( the carrier of S) Function-like constant total quasi_total for Element of K6(K7(NAT, the carrier of S));
existence
 ex b1 being sequence of S st b1 is constant
proofend;
end;

definition
let S, T be non trivial RealNormSpace;
let IT be PartFunc of S,T;
attrIT is RestFunc-like  means :Def5: :: NDIFF_1:def 5
( IT is total &amp; ( for h being non-zero 0. S -convergent sequence of S holds
( (||.h.|| ") (#) (IT /* h) is convergent &amp; lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) );
end;

:: deftheorem Def5 defines RestFunc-like NDIFF_1:def_5_:_
 for S, T being non trivial RealNormSpace
for IT being PartFunc of S,T holds
( IT is RestFunc-like iff ( IT is total &amp; ( for h being non-zero 0. b1 -convergent sequence of S holds
( (||.h.|| ") (#) (IT /* h) is convergent &amp; lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ) );

registration
let S, T be non trivial RealNormSpace;
clusterV16() V19( the carrier of S) V20( the carrier of T) Function-like RestFunc-like for Element of K6(K7( the carrier of S, the carrier of T));
existence
 ex b1 being PartFunc of S,T st b1 is RestFunc-like
proofend;
end;

definition
let S, T be non trivial RealNormSpace;
mode RestFunc of S,T is RestFunc-like PartFunc of S,T;
end;

theorem :: NDIFF_1:23
for S, T being non trivial RealNormSpace
for R being PartFunc of S,T st R is total holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 &amp; ( for z being Point of S st z <> 0. S &amp; ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) )
proofend;

theorem Th24: :: NDIFF_1:24
for S, T being non trivial RealNormSpace
for R being RestFunc of S,T
for s being non-zero 0. b1 -convergent sequence of S holds
( R /* s is convergent &amp; lim (R /* s) = 0. T )
proofend;

theorem Th25: :: NDIFF_1:25
for S, T being non trivial RealNormSpace
for h1, h2 being PartFunc of S,T
for seq being sequence of S 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 Th26: :: NDIFF_1:26
for S, T being non trivial RealNormSpace
for h being PartFunc of S,T
for seq being sequence of S
for r being Real st h is total holds
(r (#) h) /* seq = r * (h /* seq)
proofend;

theorem Th27: :: NDIFF_1:27
for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for s1 being sequence of S st rng s1 c= dom f &amp; s1 is convergent &amp; lim s1 = x0 &amp; ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent &amp; f /. x0 = lim (f /* s1) ) ) ) )
proofend;

theorem Th28: :: NDIFF_1:28
for T, S being non trivial RealNormSpace
for R1, R2 being RestFunc of S,T holds
( R1 + R2 is RestFunc of S,T &amp; R1 - R2 is RestFunc of S,T )
proofend;

theorem Th29: :: NDIFF_1:29
for T, S being non trivial RealNormSpace
for r being Real
for R being RestFunc of S,T holds r (#) R is RestFunc of S,T
proofend;

definition
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let x0 be Point of S;
predf is_differentiable_in x0 means :Def6: :: NDIFF_1:def 6
 ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) );
end;

:: deftheorem Def6 defines is_differentiable_in NDIFF_1:def_6_:_
 for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S holds
( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) );

definition
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let x0 be Point of S;
assume A1: f is_differentiable_in x0 ;
func diff (f,x0) ->  Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) means :Def7: :: NDIFF_1:def 7
 ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (it . (x - x0)) + (R /. (x - x0)) );
existence
 ex b1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (b1 . (x - x0)) + (R /. (x - x0)) )
proofend;
uniqueness
 for b1, b2 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (b1 . (x - x0)) + (R /. (x - x0)) ) &amp; ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (b2 . (x - x0)) + (R /. (x - x0)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines diff NDIFF_1:def_7_:_
 for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
for b5 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) holds
( b5 = diff (f,x0) iff ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (b5 . (x - x0)) + (R /. (x - x0)) ) );

definition
let X be set ;
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
predf is_differentiable_on X means :Def8: :: NDIFF_1:def 8
( X c= dom f &amp; ( for x being Point of S st x in X holds
f | X is_differentiable_in x ) );
end;

:: deftheorem Def8 defines is_differentiable_on NDIFF_1:def_8_:_
 for X being set
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T holds
( f is_differentiable_on X iff ( X c= dom f &amp; ( for x being Point of S st x in X holds
f | X is_differentiable_in x ) ) );

theorem Th30: :: NDIFF_1:30
for X being set
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T st f is_differentiable_on X holds
X is Subset of S
proofend;

theorem Th31: :: NDIFF_1:31
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open holds
( f is_differentiable_on Z iff ( Z c= dom f &amp; ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) )
proofend;

theorem :: NDIFF_1:32
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for Y being Subset of S st f is_differentiable_on Y holds
Y is open
proofend;

definition
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let X be set ;
assume A1: f is_differentiable_on X ;
funcf `| X ->  PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) means :Def9: :: NDIFF_1:def 9
( dom it = X &amp; ( for x being Point of S st x in X holds
it /. x = diff (f,x) ) );
existence
 ex b1 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) st
( dom b1 = X &amp; ( for x being Point of S st x in X holds
b1 /. x = diff (f,x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) st dom b1 = X &amp; ( for x being Point of S st x in X holds
b1 /. x = diff (f,x) ) &amp; dom b2 = X &amp; ( for x being Point of S st x in X holds
b2 /. x = diff (f,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines `| NDIFF_1:def_9_:_
 for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for X being set st f is_differentiable_on X holds
for b5 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) holds
( b5 = f `| X iff ( dom b5 = X &amp; ( for x being Point of S st x in X holds
b5 /. x = diff (f,x) ) ) );

theorem :: NDIFF_1:33
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open &amp; Z c= dom f &amp; ex r being Point of T st rng f = {r} holds
( f is_differentiable_on Z &amp; ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
proofend;

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

theorem Th34: :: NDIFF_1:34
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S
for N being Neighbourhood of x0 st f is_differentiable_in x0 &amp; N c= dom f holds
for h being non-zero 0. b1 -convergent sequence of S
for c being constant sequence of S st rng c = {x0} &amp; rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent &amp; lim ((f /* (h + c)) - (f /* c)) = 0. T )
proofend;

theorem Th35: :: NDIFF_1:35
for T, S being non trivial RealNormSpace
for f1, f2 being PartFunc of S,T
for x0 being Point of S 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 Th36: :: NDIFF_1:36
for T, S being non trivial RealNormSpace
for f1, f2 being PartFunc of S,T
for x0 being Point of S 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 Th37: :: NDIFF_1:37
for T, S being non trivial RealNormSpace
for r being Real
for f being PartFunc of S,T
for x0 being Point of S 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_1:38
for S being non trivial RealNormSpace
for f being PartFunc of S,S
for Z being Subset of S st Z is open &amp; Z c= dom f &amp; f | Z = id Z holds
( f is_differentiable_on Z &amp; ( for x being Point of S st x in Z holds
(f `| Z) /. x = id the carrier of S ) )
proofend;

theorem :: NDIFF_1:39
for S, T being non trivial RealNormSpace
for Z being Subset of S st Z is open holds
for f1, f2 being PartFunc of S,T 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 Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )
proofend;

theorem :: NDIFF_1:40
for S, T being non trivial RealNormSpace
for Z being Subset of S st Z is open holds
for f1, f2 being PartFunc of S,T 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 Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
proofend;

theorem :: NDIFF_1:41
for S, T being non trivial RealNormSpace
for Z being Subset of S st Z is open holds
for r being Real
for f being PartFunc of S,T st Z c= dom (r (#) f) &amp; f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z &amp; ( for x being Point of S st x in Z holds
((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )
proofend;

theorem :: NDIFF_1:42
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open &amp; Z c= dom f &amp; f | Z is constant holds
( f is_differentiable_on Z &amp; ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
proofend;

theorem :: NDIFF_1:43
for S being non trivial RealNormSpace
for f being PartFunc of S,S
for r being Real
for p being Point of S
for Z being Subset of S st Z is open &amp; Z c= dom f &amp; ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) holds
( f is_differentiable_on Z &amp; ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
proofend;

theorem Th44: :: NDIFF_1:44
for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
f is_continuous_in x0
proofend;

theorem :: NDIFF_1:45
for X being set
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T st f is_differentiable_on X holds
f is_continuous_on X
proofend;

theorem :: NDIFF_1:46
for X being set
for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open &amp; f is_differentiable_on X &amp; Z c= X holds
f is_differentiable_on Z
proofend;

theorem :: NDIFF_1:47
for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex R being RestFunc of S,T st
( R /. (0. S) = 0. T &amp; R is_continuous_in 0. S &amp; ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) )
proofend;