:: NDIFF_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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
coherence
(modetrans g,Y,Z) * (modetrans f,X,Y) is Element of BoundedLinearOperators X,Z
;
proof end;
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);
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
coherence
(modetrans g,Y,Z) * (modetrans f,X,Y) is Point of (R_NormSpace_of_BoundedLinearOperators X,Z)
;
proof end;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 V48 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 V48 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 V48 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 :
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 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 ) ) ) );

theorem Th4: :: NDIFF_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( ( 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
ex b1 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 abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - b1).|| < e ) ) ) )
proof end;
uniqueness
for b1, b2 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 abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - b1).|| < 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 abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - b2).|| < e ) ) ) ) holds
b1 = b2
proof end;
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 & ( 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))) - b6).|| < e ) ) ) ) );

theorem :: NDIFF_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 V48 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 V48 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;