:: Differentiable Functions on Normed Linear Spaces. {P}art {II}
:: by Hiroshi Imura , Yuji Sakai and Yasunari Shidama
::
:: Received June 4, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

definition
let X, Y, Z be RealNormSpace;
let f be Element of BoundedLinearOperators (X,Y);
let g be Element of BoundedLinearOperators (Y,Z);
funcg * f ->  Element of BoundedLinearOperators (X,Z) equals :: NDIFF_2:def 1
(modetrans (g,Y,Z)) * (modetrans (f,X,Y));
correctness
coherence
(modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Element of BoundedLinearOperators (X,Z);
proofend;
end;

:: deftheorem  defines * NDIFF_2:def_1_:_
 for X, Y, Z being RealNormSpace
for f being Element of BoundedLinearOperators (X,Y)
for g being Element of BoundedLinearOperators (Y,Z) holds g * f = (modetrans (g,Y,Z)) * (modetrans (f,X,Y));

definition
let X, Y, Z be RealNormSpace;
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y));
let g be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z));
funcg * f ->  Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) equals :: NDIFF_2:def 2
(modetrans (g,Y,Z)) * (modetrans (f,X,Y));
correctness
coherence
(modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Point of (R_NormSpace_of_BoundedLinearOperators (X,Z));
proofend;
end;

:: deftheorem  defines * NDIFF_2:def_2_:_
 for X, Y, Z being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for g being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds g * f = (modetrans (g,Y,Z)) * (modetrans (f,X,Y));

theorem Th1: :: NDIFF_2:1
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 & ( for z being Point of S
for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )
proofend;

theorem :: NDIFF_2:2
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
for z being Point of S
for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= dom f holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) )
proofend;

theorem Th3: :: NDIFF_2:3
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 N c= dom f holds
for z being Point of S
for dv being Point of T holds
( ( for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) iff for e being Real st e > 0 holds
ex d being Real st
( d > 0 &amp; ( for h being Real st abs h < d &amp; h <> 0 &amp; (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) )
proofend;

definition
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let x0, z be Point of S;
predf is_Gateaux_differentiable_in x0,z means :Def3: :: NDIFF_2:def 3
 ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex dv being Point of T st
for e being Real st e > 0 holds
ex d being Real st
( d > 0 &amp; ( for h being Real st abs h < d &amp; h <> 0 &amp; (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) );
end;

:: deftheorem Def3 defines is_Gateaux_differentiable_in NDIFF_2:def_3_:_
 for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0, z being Point of S holds
( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex dv being Point of T st
for e being Real st e > 0 holds
ex d being Real st
( d > 0 &amp; ( for h being Real st abs h < d &amp; h <> 0 &amp; (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) ) );

theorem Th4: :: NDIFF_2:4
( ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y ) ) &amp; ( for X being RealNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ) &amp; ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) &amp; ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) &amp; ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 &amp; ||.(x - z).|| < e / 2 &amp; ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) &amp; ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 &amp; ||.(x - z).|| < e / 2 &amp; ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) &amp; ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) &amp; ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) )
proofend;

definition
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let x0, z be Point of S;
assume A1: f is_Gateaux_differentiable_in x0,z ;
func Gateaux_diff (f,x0,z) ->  Point of T means :Def4: :: NDIFF_2:def 4
 ex N being Neighbourhood of x0 st
( N c= dom f &amp; ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 &amp; ( for h being Real st abs h < d &amp; h <> 0 &amp; (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - it).|| < e ) ) ) );
existence
 ex b1 being Point of T ex N being Neighbourhood of x0 st
( N c= dom f &amp; ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 &amp; ( for h being Real st abs h < d &amp; h <> 0 &amp; (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - b1).|| < e ) ) ) )
proofend;
uniqueness
 for b1, b2 being Point of T st ex N being Neighbourhood of x0 st
( N c= dom f &amp; ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 &amp; ( for h being Real st abs h < d &amp; h <> 0 &amp; (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - b1).|| < e ) ) ) ) &amp; ex N being Neighbourhood of x0 st
( N c= dom f &amp; ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 &amp; ( for h being Real st abs h < d &amp; h <> 0 &amp; (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - b2).|| < e ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines Gateaux_diff NDIFF_2:def_4_:_
 for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0, z being Point of S st f is_Gateaux_differentiable_in x0,z holds
for b6 being Point of T holds
( b6 = Gateaux_diff (f,x0,z) iff ex N being Neighbourhood of x0 st
( N c= dom f &amp; ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 &amp; ( for h being Real st abs h < d &amp; h <> 0 &amp; (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - b6).|| < e ) ) ) ) );

theorem :: NDIFF_2:5
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0, z being Point of S holds
( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f &amp; ex dv being Point of T st
for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} &amp; rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent &amp; dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )
proofend;

theorem :: NDIFF_2:6
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
for z being Point of S holds
( f is_Gateaux_differentiable_in x0,z &amp; Gateaux_diff (f,x0,z) = (diff (f,x0)) . z &amp; ex N being Neighbourhood of x0 st
( N c= dom f &amp; ( for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} &amp; rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent &amp; Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) )
proofend;

theorem Th7: :: NDIFF_2:7
for S, T being non trivial RealNormSpace
for R being RestFunc of S,T st R /. (0. S) = 0. T holds
for e being Real st e > 0 holds
ex d being Real st
( d > 0 &amp; ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )
proofend;

theorem :: NDIFF_2:8
for T, S, U being non trivial RealNormSpace
for R being RestFunc of T,U st R /. (0. T) = 0. U holds
for L being Lipschitzian LinearOperator of S,T holds R * L is RestFunc of S,U
proofend;

theorem Th9: :: NDIFF_2:9
for S, T, U being non trivial RealNormSpace
for R being RestFunc of S,T
for L being Lipschitzian LinearOperator of T,U holds L * R is RestFunc of S,U
proofend;

theorem :: NDIFF_2:10
for S, T, U being non trivial RealNormSpace
for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U
proofend;

theorem Th11: :: NDIFF_2:11
for S, T, U being non trivial RealNormSpace
for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U
proofend;

theorem Th12: :: NDIFF_2:12
for S, T, U being non trivial RealNormSpace
for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L1 being Lipschitzian LinearOperator of S,T
for L2 being Lipschitzian LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U
proofend;

theorem :: NDIFF_2:13
for S, T being non trivial RealNormSpace
for x0 being Point of S
for U being non trivial RealNormSpace
for f1 being PartFunc of S,T st f1 is_differentiable_in x0 holds
for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 &amp; diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) )
proofend;