:: by Hiroshi Imura , Yuji Sakai and Yasunari Shidama

::

:: Received June 4, 2004

:: Copyright (c) 2004-2019 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);

coherence

(modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Element of BoundedLinearOperators (X,Z);

end;
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 (modetrans (g,Y,Z)) * (modetrans (f,X,Y));

coherence

(modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Element of BoundedLinearOperators (X,Z);

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

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

coherence

(modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Point of (R_NormSpace_of_BoundedLinearOperators (X,Z));

end;
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 (modetrans (g,Y,Z)) * (modetrans (f,X,Y));

coherence

(modetrans (g,Y,Z)) * (modetrans (f,X,Y)) is Point of (R_NormSpace_of_BoundedLinearOperators (X,Z));

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

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

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

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

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;

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

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

:: deftheorem defines is_Gateaux_differentiable_in NDIFF_2:def 3 :

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

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

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

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 ;

ex b_{1} being Point of T 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))) - b_{1}).|| < e ) ) ) )
by A1;

uniqueness

for b_{1}, b_{2} being Point of T st 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))) - b_{1}).|| < e ) ) ) ) & 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))) - b_{2}).|| < e ) ) ) ) holds

b_{1} = b_{2}

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

ex b

( 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))) - b

uniqueness

for b

( 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))) - b

( 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))) - b

b

proof end;

:: deftheorem Def4 defines Gateaux_diff NDIFF_2:def 4 :

for S, T being 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 b_{6} being Point of T holds

( b_{6} = Gateaux_diff (f,x0,z) iff 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))) - b_{6}).|| < e ) ) ) ) );

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

( b

( 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))) - b

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

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

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

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

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

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

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

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

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

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;