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-2011 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);
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 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 convergent_to_0 Real_Sequence
for c being V8() 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 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 convergent_to_0 Real_Sequence
for c being V8() 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 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 convergent_to_0 Real_Sequence
for c being V8() 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 abs 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 non trivial RealNormSpace;
let f be PartFunc of S,T;
let x0, z be Point of S;
pred f is_Gateaux_differentiable_in x0,z means :Def3: :: 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 abs h < d & h <> 0 & (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 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Gateaux_diff NDIFF_2:def 4 :

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 & ex dv being Point of T st
for h being convergent_to_0 Real_Sequence
for c being V8() 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 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 & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() 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 non trivial RealNormSpace
for R being REST 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 T, S, U being non trivial RealNormSpace
for R being REST of T,U st R /. (0. T) = 0. U holds
for L being bounded LinearOperator of S,T holds R * L is REST of S,U

proof end;

theorem Th9: :: NDIFF_2:9

for S, T, U being non trivial RealNormSpace
for R being REST of S,T
for L being bounded LinearOperator of T,U holds L * R is REST of S,U

proof end;

theorem :: NDIFF_2:10

for S, T, U being non trivial RealNormSpace
for R1 being REST of S,T st R1 /. (0. S) = 0. T holds
for R2 being REST of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is REST of S,U

proof end;

theorem Th11: :: NDIFF_2:11

for S, T, U being non trivial RealNormSpace
for R1 being REST of S,T st R1 /. (0. S) = 0. T holds
for R2 being REST of T,U st R2 /. (0. T) = 0. U holds
for L being bounded LinearOperator of S,T holds R2 * (L + R1) is REST of S,U

proof end;

theorem Th12: :: NDIFF_2:12

for S, T, U being non trivial RealNormSpace
for R1 being REST of S,T st R1 /. (0. S) = 0. T holds
for R2 being REST of T,U st R2 /. (0. T) = 0. U holds
for L1 being bounded LinearOperator of S,T
for L2 being bounded LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is REST of S,U

proof end;

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 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) )

proof end;