:: NDIFF_2 semantic presentation

definition

let c₁, c₂, c₃ be RealNormSpace;
let c₄ be Element of BoundedLinearOperators c₁,c₂;
let c₅ be Element of BoundedLinearOperators c₂,c₃;
func c₅ * c₄ -> Element of BoundedLinearOperators a₁,a₃ equals :: NDIFF_2:def 1
(modetrans a₅,a₂,a₃) * (modetrans a₄,a₁,a₂);
correctness

proof end;

end;

:: deftheorem Def1 defines * NDIFF_2:def 1 :

definition

let c₁, c₂, c₃ be RealNormSpace;
let c₄ be Point of (R_NormSpace_of_BoundedLinearOperators c₁,c₂);
let c₅ be Point of (R_NormSpace_of_BoundedLinearOperators c₂,c₃);
func c₅ * c₄ -> Point of (R_NormSpace_of_BoundedLinearOperators a₁,a₃) equals :: NDIFF_2:def 2
(modetrans a₅,a₂,a₃) * (modetrans a₄,a₁,a₂);
correctness

proof end;

end;

:: deftheorem Def2 defines * NDIFF_2:def 2 :

theorem Th1: :: NDIFF_2:1

for b₁, b₂ being non trivial RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ st b₃ is_differentiable_in b₄ holds
ex b₅ being Neighbourhood of b₄ st
( b₅ c= dom b₃ & ( for b₆ being Point of b₂
for b₇ being convergent_to_0 Real_Sequence
for b₈ being V48 sequence of b₂ st rng b₈ = {b₄} & rng ((b₇ * b₆) + b₈) c= b₅ holds
( (b₇ " ) (#) ((b₃ * ((b₇ * b₆) + b₈)) - (b₃ * b₈)) is convergent & (diff b₃,b₄) . b₆ = lim ((b₇ " ) (#) ((b₃ * ((b₇ * b₆) + b₈)) - (b₃ * b₈))) ) ) )

proof end;

theorem Th2: :: NDIFF_2:2

for b₁, b₂ being non trivial RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ st b₃ is_differentiable_in b₄ holds
for b₅ being Point of b₂
for b₆ being convergent_to_0 Real_Sequence
for b₇ being V48 sequence of b₂ st rng b₇ = {b₄} & rng ((b₆ * b₅) + b₇) c= dom b₃ holds
( (b₆ " ) (#) ((b₃ * ((b₆ * b₅) + b₇)) - (b₃ * b₇)) is convergent & (diff b₃,b₄) . b₅ = lim ((b₆ " ) (#) ((b₃ * ((b₆ * b₅) + b₇)) - (b₃ * b₇))) )

proof end;

theorem Th3: :: NDIFF_2:3

for b₁, b₂ being non trivial RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁
for b₅ being Neighbourhood of b₄ st b₅ c= dom b₃ holds
for b₆ being Point of b₁
for b₇ being Point of b₂ holds
( ( for b₈ being convergent_to_0 Real_Sequence
for b₉ being V48 sequence of b₁ st rng b₉ = {b₄} & rng ((b₈ * b₆) + b₉) c= b₅ holds
( (b₈ " ) (#) ((b₃ * ((b₈ * b₆) + b₉)) - (b₃ * b₉)) is convergent & b₇ = lim ((b₈ " ) (#) ((b₃ * ((b₈ * b₆) + b₉)) - (b₃ * b₉))) ) ) iff for b₈ being Real st b₈ > 0 holds
ex b₉ being Real st
( b₉ > 0 & ( for b₁₀ being Real st abs b₁₀ < b₉ & b₁₀ <> 0 & (b₁₀ * b₆) + b₄ in b₅ holds
||.(((b₁₀ " ) * ((b₃ /. ((b₁₀ * b₆) + b₄)) - (b₃ /. b₄))) - b₇).|| < b₈ ) ) )

proof end;

definition

let c₁, c₂ be non trivial RealNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄, c₅ be Point of c₁;
pred c₃ is_Gateaux_differentiable_in c₄,c₅ means :Def3: :: NDIFF_2:def 3
ex b₁ being Neighbourhood of a₄ st
( b₁ c= dom a₃ & ex b₂ being Point of a₂ st
for b₃ being Real st b₃ > 0 holds
ex b₄ being Real st
( b₄ > 0 & ( for b₅ being Real st abs b₅ < b₄ & b₅ <> 0 & (b₅ * a₅) + a₄ in b₁ holds
||.(((b₅ " ) * ((a₃ /. ((b₅ * a₅) + a₄)) - (a₃ /. a₄))) - b₂).|| < b₃ ) ) );

end;

:: deftheorem Def3 defines is_Gateaux_differentiable_in NDIFF_2:def 3 :

theorem Th4: :: NDIFF_2:4

( ( for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds
( ||.(b₂ - b₃).|| > 0 iff b₂ <> b₃ ) ) & ( for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds ||.(b₂ - b₃).|| = ||.(b₃ - b₂).|| ) & ( for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds
( ||.(b₂ - b₃).|| = 0 iff b₂ = b₃ ) ) & ( for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds
( ||.(b₂ - b₃).|| <> 0 iff b₂ <> b₃ ) ) & ( for b₁ being RealNormSpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Real st b₅ > 0 & ||.(b₂ - b₄).|| < b₅ / 2 & ||.(b₄ - b₃).|| < b₅ / 2 holds
||.(b₂ - b₃).|| < b₅ ) & ( for b₁ being RealNormSpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Real st b₅ > 0 & ||.(b₂ - b₄).|| < b₅ / 2 & ||.(b₃ - b₄).|| < b₅ / 2 holds
||.(b₂ - b₃).|| < b₅ ) & ( for b₁ being RealNormSpace
for b₂ being Point of b₁ st ( for b₃ being Real st b₃ > 0 holds
||.b₂.|| < b₃ ) holds
b₂ = 0. b₁ ) & ( for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ st ( for b₄ being Real st b₄ > 0 holds
||.(b₂ - b₃).|| < b₄ ) holds
b₂ = b₃ ) )

proof end;

definition

let c₁, c₂ be non trivial RealNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄, c₅ be Point of c₁;
assume E5: c₃ is_Gateaux_differentiable_in c₄,c₅ ;
func Gateaux_diff c₃,c₄,c₅ -> Point of a₂ means :Def4: :: NDIFF_2:def 4
ex b₁ being Neighbourhood of a₄ st
( b₁ c= dom a₃ & ( for b₂ being Real st b₂ > 0 holds
ex b₃ being Real st
( b₃ > 0 & ( for b₄ being Real st abs b₄ < b₃ & b₄ <> 0 & (b₄ * a₅) + a₄ in b₁ holds
||.(((b₄ " ) * ((a₃ /. ((b₄ * a₅) + a₄)) - (a₃ /. a₄))) - a₆).|| < b₂ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Gateaux_diff NDIFF_2:def 4 :

theorem Th5: :: NDIFF_2:5

for b₁, b₂ being non trivial RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄, b₅ being Point of b₁ holds
( b₃ is_Gateaux_differentiable_in b₄,b₅ iff ex b₆ being Neighbourhood of b₄ st
( b₆ c= dom b₃ & ex b₇ being Point of b₂ st
for b₈ being convergent_to_0 Real_Sequence
for b₉ being V48 sequence of b₁ st rng b₉ = {b₄} & rng ((b₈ * b₅) + b₉) c= b₆ holds
( (b₈ " ) (#) ((b₃ * ((b₈ * b₅) + b₉)) - (b₃ * b₉)) is convergent & b₇ = lim ((b₈ " ) (#) ((b₃ * ((b₈ * b₅) + b₉)) - (b₃ * b₉))) ) ) )

proof end;

theorem Th6: :: NDIFF_2:6

for b₁, b₂ being non trivial RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ st b₃ is_differentiable_in b₄ holds
for b₅ being Point of b₂ holds
( b₃ is_Gateaux_differentiable_in b₄,b₅ & Gateaux_diff b₃,b₄,b₅ = (diff b₃,b₄) . b₅ & ex b₆ being Neighbourhood of b₄ st
( b₆ c= dom b₃ & ( for b₇ being convergent_to_0 Real_Sequence
for b₈ being V48 sequence of b₂ st rng b₈ = {b₄} & rng ((b₇ * b₅) + b₈) c= b₆ holds
( (b₇ " ) (#) ((b₃ * ((b₇ * b₅) + b₈)) - (b₃ * b₈)) is convergent & Gateaux_diff b₃,b₄,b₅ = lim ((b₇ " ) (#) ((b₃ * ((b₇ * b₅) + b₈)) - (b₃ * b₈))) ) ) ) )

proof end;

theorem Th7: :: NDIFF_2:7

for b₁, b₂ being non trivial RealNormSpace
for b₃ being REST of b₁,b₂ st b₃ /. (0. b₁) = 0. b₂ holds
for b₄ being Real st b₄ > 0 holds
ex b₅ being Real st
( b₅ > 0 & ( for b₆ being Point of b₁ st ||.b₆.|| < b₅ holds
||.(b₃ /. b₆).|| <= b₄ * ||.b₆.|| ) )

proof end;

theorem Th8: :: NDIFF_2:8

for b₁, b₂, b₃ being non trivial RealNormSpace
for b₄ being REST of b₁,b₃ st b₄ /. (0. b₁) = 0. b₃ holds
for b₅ being bounded LinearOperator of b₂,b₁ holds b₄ * b₅ is REST of b₂,b₃

proof end;

theorem Th9: :: NDIFF_2:9

for b₁, b₂, b₃ being non trivial RealNormSpace
for b₄ being REST of b₁,b₂
for b₅ being bounded LinearOperator of b₂,b₃ holds b₅ * b₄ is REST of b₁,b₃

proof end;

theorem Th10: :: NDIFF_2:10

for b₁, b₂, b₃ being non trivial RealNormSpace
for b₄ being REST of b₁,b₂ st b₄ /. (0. b₁) = 0. b₂ holds
for b₅ being REST of b₂,b₃ st b₅ /. (0. b₂) = 0. b₃ holds
b₅ * b₄ is REST of b₁,b₃

proof end;

theorem Th11: :: NDIFF_2:11

for b₁, b₂, b₃ being non trivial RealNormSpace
for b₄ being REST of b₁,b₂ st b₄ /. (0. b₁) = 0. b₂ holds
for b₅ being REST of b₂,b₃ st b₅ /. (0. b₂) = 0. b₃ holds
for b₆ being bounded LinearOperator of b₁,b₂ holds b₅ * (b₆ + b₄) is REST of b₁,b₃

proof end;

theorem Th12: :: NDIFF_2:12

proof end;

theorem Th13: :: NDIFF_2:13

for b₁, b₂ being non trivial RealNormSpace
for b₃ being Point of b₁
for b₄ being non trivial RealNormSpace
for b₅ being PartFunc of b₁,b₂ st b₅ is_differentiable_in b₃ holds
for b₆ being PartFunc of b₂,b₄ st b₆ is_differentiable_in b₅ /. b₃ holds
( b₆ * b₅ is_differentiable_in b₃ & diff (b₆ * b₅),b₃ = (diff b₆,(b₅ /. b₃)) * (diff b₅,b₃) )

proof end;