NDIFF_2: Differentiable Functions on Normed Linear Spaces. {P}art {II}

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

definition

let X, Y, Z be RealNormSpace;
let f be Element of BoundedLinearOperators (X,Y);
let g be Element of BoundedLinearOperators (Y,Z);

func g * f -> Element of BoundedLinearOperators (X,Z) equals :: NDIFF_2:def 1
(modetrans (g,Y,Z)) * (modetrans (f,X,Y));

correctness

proof end;

end;

:: deftheorem defines * NDIFF_2:def 1 :

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

func g * f -> Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) equals :: NDIFF_2:def 2
(modetrans (g,Y,Z)) * (modetrans (f,X,Y));

correctness

proof end;

end;

:: deftheorem defines * NDIFF_2:def 2 :

theorem Th1: :: NDIFF_2:1

for S, T being 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))) ) ) )

proof end;

theorem :: NDIFF_2:2

for S, T being 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))) )

proof end;

theorem Th3: :: NDIFF_2:3

for S, T being 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 & ( for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) )

proof end;

definition

let S, T be RealNormSpace;
let f be PartFunc of S,T;
let x0, z be Point of S;

pred f is_Gateaux_differentiable_in x0,z means :: NDIFF_2:def 3
ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e ) ) );

end;

:: deftheorem defines is_Gateaux_differentiable_in NDIFF_2:def 3 :

theorem Th4: :: NDIFF_2:4

( ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( 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 ) & ( 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 ) )

proof end;

definition

let S, T be 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 & ( for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - it).|| < e ) ) ) );

existence by A1;
uniqueness

proof end;

end;

:: deftheorem Def4 defines Gateaux_diff NDIFF_2:def 4 :

theorem :: NDIFF_2:5

for S, T being 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 & 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} & 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))) ) ) )

proof end;

theorem :: NDIFF_2:6

for S, T being 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 & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( 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 & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) )

proof end;

theorem Th7: :: NDIFF_2:7

for S, T being 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 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )

proof end;

theorem :: NDIFF_2:8

for S, T, U being 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

proof end;

theorem Th9: :: NDIFF_2:9

for S, T, U being RealNormSpace
for R being RestFunc of S,T
for L being Lipschitzian LinearOperator of T,U holds L * R is RestFunc of S,U

proof end;

theorem :: NDIFF_2:10

for S, T, U being 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

proof end;

theorem Th11: :: NDIFF_2:11

for S, T, U being 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

proof end;

theorem Th12: :: NDIFF_2:12

for S, T, U being 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

proof end;

theorem :: NDIFF_2:13

for S, T being RealNormSpace
for x0 being Point of S
for U being 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 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) )

proof end;