definition
let E,
F,
G be
RealNormSpace;
let L be
Lipschitzian LinearOperator of
F,
G;
func LTRN (
L,
E)
-> Function means :
Def1:
(
dom it = NAT &
it . 0 = L & ( for
i being
Nat ex
K being
Lipschitzian LinearOperator of
(diff_SP ((i + 1),E,F)),
(diff_SP ((i + 1),E,G)) ex
M being
Lipschitzian LinearOperator of
(diff_SP (i,E,F)),
(diff_SP (i,E,G)) st
(
it . (i + 1) = K &
In (
(it . i),
(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G)))))
= M & ( for
V being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) holds
K . V = M * V ) ) ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = L & ( for i being Nat ex K being Lipschitzian LinearOperator of (diff_SP ((i + 1),E,F)),(diff_SP ((i + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) st
( b1 . (i + 1) = K & In ((b1 . i),(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds K . V = M * V ) ) ) )
uniqueness
for b1, b2 being Function st dom b1 = NAT & b1 . 0 = L & ( for i being Nat ex K being Lipschitzian LinearOperator of (diff_SP ((i + 1),E,F)),(diff_SP ((i + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) st
( b1 . (i + 1) = K & In ((b1 . i),(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds K . V = M * V ) ) ) & dom b2 = NAT & b2 . 0 = L & ( for i being Nat ex K being Lipschitzian LinearOperator of (diff_SP ((i + 1),E,F)),(diff_SP ((i + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) st
( b2 . (i + 1) = K & In ((b2 . i),(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds K . V = M * V ) ) ) holds
b1 = b2
end;
::
deftheorem Def1 defines
LTRN NDIFF13:def 1 :
for E, F, G being RealNormSpace
for L being Lipschitzian LinearOperator of F,G
for b5 being Function holds
( b5 = LTRN (L,E) iff ( dom b5 = NAT & b5 . 0 = L & ( for i being Nat ex K being Lipschitzian LinearOperator of (diff_SP ((i + 1),E,F)),(diff_SP ((i + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) st
( b5 . (i + 1) = K & In ((b5 . i),(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds K . V = M * V ) ) ) ) );
Lm1:
for E, F, G being RealNormSpace
for L being Lipschitzian LinearOperator of F,G
for i being Nat holds (LTRN (L,E)) . i is Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G))
theorem Th22:
for
E,
F,
G being
RealNormSpace for
L being
Lipschitzian LinearOperator of
F,
G holds
(
LTRN (
0,
L,
E)
= L & ( for
i being
Nat for
V being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) holds
(LTRN ((i + 1),L,E)) . V = (LTRN (i,L,E)) * V ) )
theorem Th25:
for
E,
F,
G being
RealNormSpace for
Z being
Subset of
E for
u being
PartFunc of
E,
F for
L being
Lipschitzian LinearOperator of
F,
G for
i being
Nat st
u is_differentiable_on i,
Z holds
(
L * u is_differentiable_on i,
Z &
diff (
(L * u),
i,
Z)
= (LTRN (i,L,E)) * (diff (u,i,Z)) )
theorem
for
E,
F,
G being
RealNormSpace for
Z being
Subset of
E for
u being
PartFunc of
E,
F for
L being
Lipschitzian LinearOperator of
F,
G for
i being
Nat st
u is_differentiable_on i,
Z &
diff (
u,
i,
Z)
is_continuous_on Z holds
(
L * u is_differentiable_on i,
Z &
diff (
(L * u),
i,
Z)
is_continuous_on Z )
theorem Th27:
for
S,
T,
U being
RealNormSpace for
x being
Point of
S for
u being
PartFunc of
S,
T for
v being
PartFunc of
S,
U for
w being
PartFunc of
S,
[:T,U:] st
u is_differentiable_in x &
v is_differentiable_in x &
w = <:u,v:> holds
(
w is_differentiable_in x &
diff (
w,
x)
= <:(diff (u,x)),(diff (v,x)):> & ( for
dx being
Point of
S holds
(diff (w,x)) . dx = [((diff (u,x)) . dx),((diff (v,x)) . dx)] ) )
theorem Th34:
for
S,
E,
F,
G being
RealNormSpace for
B being
Lipschitzian BilinearOperator of
E,
F,
G for
W being
PartFunc of
S,
G for
w being
PartFunc of
S,
[:E,F:] for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F for
x being
Point of
S st
u is_differentiable_in x &
v is_differentiable_in x &
x in dom w &
W = B * w &
w = <:u,v:> holds
(
W is_differentiable_in x &
w is_differentiable_in x &
diff (
W,
x)
= (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) &
diff (
w,
x)
= <:(diff (u,x)),(diff (v,x)):> & ( for
ds being
Point of
S holds
(diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) )
theorem Th35:
for
S,
E,
F,
G being
RealNormSpace for
Z being
Subset of
S for
B being
Lipschitzian BilinearOperator of
E,
F,
G for
W being
PartFunc of
S,
G for
w being
PartFunc of
S,
[:E,F:] for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F st
u is_differentiable_on Z &
v is_differentiable_on Z &
W = B * w &
w = <:u,v:> holds
(
W is_differentiable_on Z & ( for
x being
Point of
S st
x in Z holds
for
ds being
Point of
S holds
((W `| Z) /. x) . ds = (B . ((((u `| Z) /. x) . ds),(v /. x))) + (B . ((u /. x),(((v `| Z) /. x) . ds))) ) )
theorem Th38:
for
E,
F,
G being
RealNormSpace ex
B being
Lipschitzian BilinearOperator of
(R_NormSpace_of_BoundedLinearOperators (E,F)),
(R_NormSpace_of_BoundedLinearOperators (F,G)),
(R_NormSpace_of_BoundedLinearOperators (E,G)) st
for
u being
Point of
(R_NormSpace_of_BoundedLinearOperators (E,F)) for
v being
Point of
(R_NormSpace_of_BoundedLinearOperators (F,G)) holds
B . (
u,
v)
= v * u
theorem Th39:
for
i being
Nat for
S,
E,
F,
G being
RealNormSpace for
Z being
Subset of
S for
B being
Lipschitzian BilinearOperator of
E,
F,
G for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F for
w being
PartFunc of
S,
[:E,F:] for
W being
PartFunc of
S,
G st
W = B * w &
w = <:u,v:> &
u is_differentiable_on i,
Z &
v is_differentiable_on i,
Z holds
W is_differentiable_on i,
Z
theorem
for
S,
E,
F,
G being
RealNormSpace for
Z being
Subset of
S for
B being
Lipschitzian BilinearOperator of
E,
F,
G for
W being
PartFunc of
S,
G for
w being
PartFunc of
S,
[:E,F:] for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F st
u is_differentiable_on Z &
u `| Z is_continuous_on Z &
v is_differentiable_on Z &
v `| Z is_continuous_on Z &
W = B * w &
w = <:u,v:> holds
(
W is_differentiable_on Z &
W `| Z is_continuous_on Z )
theorem Th42:
for
i being
Nat for
S,
E,
F,
G being
RealNormSpace for
Z being
Subset of
S for
B being
Lipschitzian BilinearOperator of
E,
F,
G for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F for
w being
PartFunc of
S,
[:E,F:] for
W being
PartFunc of
S,
G st
W = B * w &
w = <:u,v:> &
u is_differentiable_on i,
Z &
diff (
u,
i,
Z)
is_continuous_on Z &
v is_differentiable_on i,
Z &
diff (
v,
i,
Z)
is_continuous_on Z holds
(
W is_differentiable_on i,
Z &
diff (
W,
i,
Z)
is_continuous_on Z )
theorem Th44:
for
i being
Nat for
E,
F,
G being
RealNormSpace for
Z being
Subset of
E for
T being
Subset of
F for
u being
PartFunc of
E,
F for
v being
PartFunc of
F,
G st
u .: Z c= T &
u is_differentiable_on i,
Z &
diff (
u,
i,
Z)
is_continuous_on Z &
v is_differentiable_on i,
T &
diff (
v,
i,
T)
is_continuous_on T holds
(
v * u is_differentiable_on i,
Z &
diff (
(v * u),
i,
Z)
is_continuous_on Z )
theorem Th49:
for
E,
F being
RealNormSpace for
Z being non
empty Subset of
E for
L1 being
PartFunc of
E,
F for
L0 being
Point of
F st
Z is
open &
L1 = Z --> L0 holds
for
i being
Nat holds
( ex
P being
Point of
(diff_SP (i,E,F)) st
diff (
L1,
i,
Z)
= Z --> P &
diff (
L1,
i,
Z)
is_differentiable_on Z &
(diff (L1,i,Z)) `| Z is_continuous_on Z )
theorem Th53:
for
i being
Nat for
E,
F,
G being
RealNormSpace for
Z being non
empty Subset of
[:E,F:] for
f being
PartFunc of
[:E,F:],
G st
f is_differentiable_on i + 1,
Z &
diff (
f,
(i + 1),
Z)
is_continuous_on Z holds
(
f `partial`1| Z is_differentiable_on i,
Z &
diff (
(f `partial`1| Z),
i,
Z)
is_continuous_on Z &
f `partial`2| Z is_differentiable_on i,
Z &
diff (
(f `partial`2| Z),
i,
Z)
is_continuous_on Z )
theorem Th54:
for
S,
E,
F being
RealNormSpace for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F for
w being
PartFunc of
S,
[:E,F:] for
x being
Point of
S st
w = <:u,v:> &
u is_differentiable_in x &
v is_differentiable_in x holds
(
w is_differentiable_in x &
diff (
w,
x)
= <:(diff (u,x)),(diff (v,x)):> )
definition
let S,
E,
F be
RealNormSpace;
func CTP (
S,
E,
F)
-> Lipschitzian LinearOperator of
[:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):],
(R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) means :
Def3:
for
f being
Lipschitzian LinearOperator of
S,
E for
g being
Lipschitzian LinearOperator of
S,
F holds
it . (
f,
g)
= <:f,g:>;
existence
ex b1 being Lipschitzian LinearOperator of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) st
for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds b1 . (f,g) = <:f,g:>
uniqueness
for b1, b2 being Lipschitzian LinearOperator of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) st ( for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds b1 . (f,g) = <:f,g:> ) & ( for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds b2 . (f,g) = <:f,g:> ) holds
b1 = b2
end;
::
deftheorem Def3 defines
CTP NDIFF13:def 3 :
for S, E, F being RealNormSpace
for b4 being Lipschitzian LinearOperator of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) holds
( b4 = CTP (S,E,F) iff for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds b4 . (f,g) = <:f,g:> );
theorem Th56:
for
S,
E,
F being
RealNormSpace for
i being
Nat holds
CTP (
S,
(diff_SP (i,S,E)),
(diff_SP (i,S,F))) is
Lipschitzian LinearOperator of
[:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],
(R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (i,S,E)),(diff_SP (i,S,F)):]))
theorem Th57:
for
S,
E,
F being
RealNormSpace for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F for
w being
PartFunc of
S,
[:E,F:] for
Z being
Subset of
S st
w = <:u,v:> &
u is_differentiable_on Z &
v is_differentiable_on Z holds
(
w is_differentiable_on Z &
w `| Z = (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):> )
theorem Th58:
for
S,
E,
F being
RealNormSpace for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F for
w being
PartFunc of
S,
[:E,F:] for
Z being
Subset of
S st
w = <:u,v:> &
u is_differentiable_on Z &
v is_differentiable_on Z holds
(
diff (
w,
0,
Z)
is_differentiable_on Z & ex
T being
Lipschitzian LinearOperator of
[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],
(diff_SP (1,S,[:E,F:])) st
(
T = CTP (
S,
(diff_SP (0,S,E)),
(diff_SP (0,S,F))) &
diff (
w,1,
Z)
= T * <:(diff (u,1,Z)),(diff (v,1,Z)):> ) )
theorem
for
S,
E,
F being
RealNormSpace for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F for
w being
PartFunc of
S,
[:E,F:] for
Z being
Subset of
S st
w = <:u,v:> &
u is_differentiable_on 2,
Z &
v is_differentiable_on 2,
Z holds
(
w is_differentiable_on 2,
Z & ex
L1 being
Lipschitzian LinearOperator of
[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],
(diff_SP (1,S,[:E,F:])) ex
L2 being
Lipschitzian LinearOperator of
[:(diff_SP (2,S,E)),(diff_SP (2,S,F)):],
(diff_SP (1,S,[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):])) ex
T being
Lipschitzian LinearOperator of
[:(diff_SP (2,S,E)),(diff_SP (2,S,F)):],
(diff_SP (2,S,[:E,F:])) st
(
L1 = CTP (
S,
(diff_SP (0,S,E)),
(diff_SP (0,S,F))) &
L2 = CTP (
S,
(diff_SP (1,S,E)),
(diff_SP (1,S,F))) &
T = (LTRN (1,L1,S)) * L2 &
diff (
w,2,
Z)
= T * <:(diff (u,2,Z)),(diff (v,2,Z)):> ) )
theorem Th60:
for
i being
Nat for
S,
E,
F being
RealNormSpace for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F for
w being
PartFunc of
S,
[:E,F:] for
Z being
Subset of
S st
w = <:u,v:> &
u is_differentiable_on i + 1,
Z &
v is_differentiable_on i + 1,
Z holds
(
w is_differentiable_on i + 1,
Z & ex
T being
Lipschitzian LinearOperator of
[:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],
(diff_SP ((i + 1),S,[:E,F:])) st
diff (
w,
(i + 1),
Z)
= T * <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> )
theorem Th61:
for
S,
E,
F being
RealNormSpace for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F for
w being
PartFunc of
S,
[:E,F:] for
Z being
Subset of
S for
i being
Nat st
w = <:u,v:> &
u is_differentiable_on i + 1,
Z &
diff (
u,
(i + 1),
Z)
is_continuous_on Z &
v is_differentiable_on i + 1,
Z &
diff (
v,
(i + 1),
Z)
is_continuous_on Z holds
(
w is_differentiable_on i + 1,
Z &
diff (
w,
(i + 1),
Z)
is_continuous_on Z )
theorem Th65:
for
E being
RealBanachSpace for
F,
G being non
trivial RealBanachSpace for
Z being non
empty Subset of
[:E,F:] for
c being
Point of
G for
A being
Subset of
E for
B being
Subset of
F st
Z is
open &
A is
open &
B is
open &
[:A,B:] c= Z holds
for
i being
Nat for
f being
PartFunc of
[:E,F:],
G for
g being
PartFunc of
E,
F st
dom f = Z &
f is_differentiable_on i + 1,
Z &
diff (
f,
(i + 1),
Z)
is_continuous_on Z &
dom g = A &
rng g c= B &
g is_continuous_on A & ( for
x being
Point of
E st
x in A holds
f . (
x,
(g . x))
= c ) & ( for
x being
Point of
E for
z being
Point of
[:E,F:] st
x in A &
z = [x,(g . x)] holds
partdiff`2 (
f,
z) is
invertible ) holds
(
g is_differentiable_on i + 1,
A &
diff (
g,
(i + 1),
A)
is_continuous_on A & ( for
x being
Point of
E for
z being
Point of
[:E,F:] st
x in A &
z = [x,(g . x)] holds
diff (
g,
x)
= - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
theorem Th66:
for
F,
G being non
trivial RealBanachSpace ex
I being
PartFunc of
(R_NormSpace_of_BoundedLinearOperators (F,G)),
(R_NormSpace_of_BoundedLinearOperators (G,F)) st
(
dom I = InvertibleOperators (
F,
G) &
rng I = InvertibleOperators (
G,
F) &
I is
one-to-one &
I is_continuous_on InvertibleOperators (
F,
G) & ex
J being
PartFunc of
(R_NormSpace_of_BoundedLinearOperators (G,F)),
(R_NormSpace_of_BoundedLinearOperators (F,G)) st
(
J = I " &
J is
one-to-one &
dom J = InvertibleOperators (
G,
F) &
rng J = InvertibleOperators (
F,
G) &
J is_continuous_on InvertibleOperators (
G,
F) ) & ( for
u being
Point of
(R_NormSpace_of_BoundedLinearOperators (F,G)) st
u in InvertibleOperators (
F,
G) holds
I . u = Inv u ) & ( for
n being
Nat holds
(
I is_differentiable_on n + 1,
InvertibleOperators (
F,
G) &
diff (
I,
(n + 1),
(InvertibleOperators (F,G)))
is_continuous_on InvertibleOperators (
F,
G) ) ) )
theorem
for
E,
F being non
trivial RealBanachSpace for
Z being
Subset of
E for
f being
PartFunc of
E,
F for
a being
Point of
E for
b being
Point of
F for
n being
Nat st
Z is
open &
dom f = Z &
f is_differentiable_on n + 1,
Z &
diff (
f,
(n + 1),
Z)
is_continuous_on Z &
a in Z &
f . a = b &
diff (
f,
a) is
invertible holds
ex
A being
Subset of
E ex
B being
Subset of
F ex
g being
PartFunc of
F,
E st
(
A is
open &
B is
open &
A c= dom f &
a in A &
b in B &
f .: A = B &
dom g = B &
rng g = A &
dom (f | A) = A &
rng (f | A) = B &
f | A is
one-to-one &
g is
one-to-one &
g = (f | A) " &
f | A = g " &
g . b = a & ( for
y being
Point of
F st
y in B holds
diff (
f,
(g /. y)) is
invertible ) & ( for
y being
Point of
F st
y in B holds
diff (
g,
y)
= Inv (diff (f,(g /. y))) ) &
f is_differentiable_on n + 1,
A &
diff (
f,
(n + 1),
A)
is_continuous_on A &
g is_differentiable_on n + 1,
B &
diff (
g,
(n + 1),
B)
is_continuous_on B )