:: Higher-Order Differentiation and Inverse Function Theorem in Real Normed Spaces
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received December 24, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users


theorem :: NDIFF13:1
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for x being Point of S st Z is open & x in Z & Z c= dom f holds
( f | Z is_differentiable_in x iff f is_differentiable_in x )
proof end;

theorem Th3: :: NDIFF13:2
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S holds
( f | Z is_differentiable_on Z iff f is_differentiable_on Z )
proof end;

theorem Th4: :: NDIFF13:3
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st f is_differentiable_on Z holds
(f | Z) `| Z = f `| Z
proof end;

theorem Th5: :: NDIFF13:4
for S, T being RealNormSpace
for f being PartFunc of S,T
for X, Z being Subset of S st Z is open & Z c= X & f is_differentiable_on X holds
f `| Z = (f `| X) | Z
proof end;

theorem :: NDIFF13:5
for S, T being RealNormSpace
for f being PartFunc of S,T
for X, Z being Subset of S st Z is open & Z c= X & f is_differentiable_on X & f `| X is_continuous_on X holds
f `| Z is_continuous_on Z
proof end;

theorem Th7: :: NDIFF13:6
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for k being Nat st f is_differentiable_on k,Z holds
( f | Z is_differentiable_on k,Z & diff ((f | Z),k,Z) = diff (f,k,Z) )
proof end;

theorem :: NDIFF13:7
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for k being Nat st f is_differentiable_on k,Z & diff (f,k,Z) is_continuous_on Z holds
( f | Z is_differentiable_on k,Z & diff ((f | Z),k,Z) is_continuous_on Z ) by Th7;

theorem Th9: :: NDIFF13:8
for S, T being RealNormSpace
for f being PartFunc of S,T
for X, Z being Subset of S st Z is open & Z c= X holds
for i being Nat st f is_differentiable_on i,X holds
( f is_differentiable_on i,Z & diff (f,i,Z) = (diff (f,i,X)) | Z )
proof end;

theorem Th10: :: NDIFF13:9
for S, T being RealNormSpace
for f being PartFunc of S,T
for X, Z being Subset of S st Z is open & Z c= X holds
for i being Nat st f is_differentiable_on i,X & diff (f,i,X) is_continuous_on X holds
( f is_differentiable_on i,Z & diff (f,i,Z) is_continuous_on Z )
proof end;

theorem Th11: :: NDIFF13:10
for X, Y being RealNormSpace
for a being Real
for v1, v2 being Lipschitzian LinearOperator of X,Y
for w1, w2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st v1 = w1 & v2 = w2 holds
( v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )
proof end;

theorem :: NDIFF13:11
for X, Y being RealNormSpace
for v1, v2, v3 being Lipschitzian LinearOperator of X,Y
for a, b being Real holds
( v1 + v2 = v2 + v1 & (v1 + v2) + v3 = v1 + (v2 + v3) & a (#) (v1 + v2) = (a (#) v1) + (a (#) v2) & (a + b) (#) v1 = (a (#) v1) + (b (#) v1) & (a * b) (#) v1 = a (#) (b (#) v1) )
proof end;

theorem Th13: :: NDIFF13:12
for X, Y, Z being RealNormSpace
for v being Lipschitzian LinearOperator of X,Y
for s being Lipschitzian LinearOperator of Y,Z
for pv being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for ps being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) st v = pv & s = ps holds
s * v = ps * pv
proof end;

theorem Th14: :: NDIFF13:13
for X, Y, Z being RealNormSpace
for v1, v2 being Lipschitzian LinearOperator of X,Y
for s1, s2 being Lipschitzian LinearOperator of Y,Z
for a being Real holds
( s1 * (v1 + v2) = (s1 * v1) + (s1 * v2) & (s1 + s2) * v1 = (s1 * v1) + (s2 * v1) & s1 * (a (#) v1) = a (#) (s1 * v1) )
proof end;

theorem :: NDIFF13:14
for S, T, U being RealNormSpace
for f1 being PartFunc of S,T
for f2 being PartFunc of T,U
for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
proof end;

theorem Th16: :: NDIFF13:15
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_continuous_on Z & v is_continuous_on T holds
v * u is_continuous_on Z
proof end;

theorem Th17: :: NDIFF13:16
for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:] st z = [x,y] holds
||.z.|| <= ||.x.|| + ||.y.||
proof end;

theorem :: NDIFF13:17
for E, F, G being RealNormSpace
for u being PartFunc of E,F
for L being Lipschitzian LinearOperator of F,G
for x being Point of E st u is_differentiable_in x holds
( L * u is_differentiable_in x & diff ((L * u),x) = L * (diff (u,x)) )
proof end;

theorem Th19: :: NDIFF13:18
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 Z & v is_differentiable_on T holds
( v * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ) )
proof end;

theorem Th20: :: NDIFF13:19
for F, G being RealNormSpace
for L being Lipschitzian LinearOperator of F,G holds
( L is_differentiable_on [#] F & L `| ([#] F) is_continuous_on [#] F & ( for x being Point of F holds (L `| ([#] F)) /. x = L ) )
proof end;

theorem Th21: :: NDIFF13:20
for E, F, G being RealNormSpace
for u being PartFunc of E,F
for Z being Subset of E
for L being Lipschitzian LinearOperator of F,G st u is_differentiable_on Z holds
( L * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((L * u) `| Z) /. x = L * ((u `| Z) /. x) ) )
proof end;

definition
let E, F, G be RealNormSpace;
let L be Lipschitzian LinearOperator of F,G;
func LTRN (L,E) -> Function means :Def1: :: NDIFF13:def 1
( 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 ) ) ) )
proof end;
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
proof end;
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))

proof end;

definition
let E, F, G be RealNormSpace;
let L be Lipschitzian LinearOperator of F,G;
let i be Nat;
func LTRN (i,L,E) -> Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) equals :: NDIFF13:def 2
(LTRN (L,E)) . i;
correctness
coherence
(LTRN (L,E)) . i is Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G))
;
by Lm1;
end;

:: deftheorem defines LTRN NDIFF13:def 2 :
for E, F, G being RealNormSpace
for L being Lipschitzian LinearOperator of F,G
for i being Nat holds LTRN (i,L,E) = (LTRN (L,E)) . i;

theorem Th22: :: NDIFF13:21
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 ) )
proof end;

theorem Th23: :: NDIFF13:22
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 Z & u `| Z is_continuous_on Z & v is_differentiable_on T & v `| T is_continuous_on T holds
( v * u is_differentiable_on Z & (v * u) `| Z is_continuous_on Z )
proof end;

theorem :: NDIFF13:23
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 st u is_differentiable_on Z & u `| Z is_continuous_on Z holds
( L * u is_differentiable_on Z & (L * u) `| Z is_continuous_on Z )
proof end;

theorem Th25: :: NDIFF13:24
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)) )
proof end;

theorem :: NDIFF13:25
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 )
proof end;

theorem Th27: :: NDIFF13:26
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)] ) )
proof end;

theorem Th28: :: NDIFF13:27
for S, T, U being RealNormSpace
for Z being Subset 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_on Z & v is_differentiable_on Z & w = <:u,v:> holds
( w is_differentiable_on Z & ( for x being Point of S st x in Z holds
(w `| Z) /. x = <:((u `| Z) /. x),((v `| Z) /. x):> ) & ( for x being Point of S st x in Z holds
for dx being Point of S holds ((w `| Z) /. x) . dx = [(((u `| Z) /. x) . dx),(((v `| Z) /. x) . dx)] ) )
proof end;

theorem Th29: :: NDIFF13:28
for S, T, U being RealNormSpace
for Z being Subset 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_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & w = <:u,v:> holds
( w is_differentiable_on Z & w `| Z is_continuous_on Z )
proof end;

theorem Th30: :: NDIFF13:29
for E, F being RealNormSpace
for i being Nat holds diff_SP ((i + 1),E,F) = diff_SP (i,E,(R_NormSpace_of_BoundedLinearOperators (E,F)))
proof end;

theorem Th31: :: NDIFF13:30
for E, F being RealNormSpace
for Z being Subset of E
for g being PartFunc of E,F
for f being PartFunc of E,(R_NormSpace_of_BoundedLinearOperators (E,F)) st (g | Z) `| Z = f | Z holds
for i being Nat holds diff (g,(i + 1),Z) = diff (f,i,Z)
proof end;

theorem Th32: :: NDIFF13:31
for E, F being RealNormSpace
for n being Nat
for Z being Subset of E
for g being PartFunc of E,F st g `| Z is_differentiable_on n,Z & g is_differentiable_on Z holds
g is_differentiable_on n + 1,Z
proof end;

theorem Th33: :: NDIFF13:32
for E, F being RealNormSpace
for n being Nat
for Z being Subset of E
for g being PartFunc of E,F st g `| Z is_differentiable_on n,Z & g is_differentiable_on Z & diff ((g `| Z),n,Z) is_continuous_on Z holds
( g is_differentiable_on n + 1,Z & diff (g,(n + 1),Z) is_continuous_on Z )
proof end;

theorem Th34: :: NDIFF13:33
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))) ) )
proof end;

theorem Th35: :: NDIFF13:34
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))) ) )
proof end;

theorem Th36: :: NDIFF13:35
for S, E being RealNormSpace
for Z being Subset of S
for u being PartFunc of S,E
for i being Nat st u is_differentiable_on i + 1,Z holds
u `| Z is_differentiable_on i,Z
proof end;

theorem Th37: :: NDIFF13:36
for S, E being RealNormSpace
for Z being Subset of S
for u being PartFunc of S,E
for i being Nat st u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z holds
( u `| Z is_differentiable_on i,Z & diff ((u `| Z),i,Z) is_continuous_on Z )
proof end;

theorem Th38: :: NDIFF13:37
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
proof end;

theorem Th39: :: NDIFF13:38
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
proof end;

theorem :: NDIFF13:39
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 )
proof end;

theorem Th41: :: NDIFF13:40
for S, E, F, G being RealNormSpace
for Z being Subset of S
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:] st w = <:u,v:> & u is_continuous_on Z & v is_continuous_on Z holds
w is_continuous_on Z
proof end;

theorem Th42: :: NDIFF13:41
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 )
proof end;

theorem Th43: :: NDIFF13:42
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 & v is_differentiable_on i,T holds
v * u is_differentiable_on i,Z
proof end;

theorem Th44: :: NDIFF13:43
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 )
proof end;

theorem Th45: :: NDIFF13:44
for E, F, G being RealNormSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G st f is_differentiable_on Z holds
( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & ( for z being Point of [:E,F:] st z in Z holds
( ( for dx being Point of E holds ((f `partial`1| Z) /. z) . dx = ((f `| Z) /. z) . (dx,(0. F)) ) & ( for dy being Point of F holds ((f `partial`2| Z) /. z) . dy = ((f `| Z) /. z) . ((0. E),dy) ) ) ) )
proof end;

theorem Th46: :: NDIFF13:45
for E, F being RealNormSpace ex L10 being Lipschitzian LinearOperator of E,[:E,F:] st
for dx being Point of E holds L10 . dx = [dx,(0. F)]
proof end;

theorem Th47: :: NDIFF13:46
for E, F being RealNormSpace ex L20 being Lipschitzian LinearOperator of F,[:E,F:] st
for dy being Point of F holds L20 . dy = [(0. E),dy]
proof end;

theorem Th48: :: NDIFF13:47
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
( L1 is_differentiable_on Z & L1 `| Z is_continuous_on Z & L1 `| Z = Z --> (0. (R_NormSpace_of_BoundedLinearOperators (E,F))) )
proof end;

theorem Th49: :: NDIFF13:48
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 )
proof end;

theorem Th50: :: NDIFF13:49
for i being Nat
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
( L1 is_differentiable_on i,Z & (diff (L1,i,Z)) `| Z is_continuous_on Z )
proof end;

theorem Th51: :: NDIFF13:50
for n being Nat
for S being RealNormSpace
for Z being Subset of S
for f being PartFunc of S,S st Z is open & f = id ([#] S) holds
( f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z )
proof end;

theorem :: NDIFF13:51
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 holds
( f `partial`1| Z is_differentiable_on i,Z & f `partial`2| Z is_differentiable_on i,Z )
proof end;

theorem Th53: :: NDIFF13:52
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 )
proof end;

theorem Th54: :: NDIFF13:53
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)):> )
proof end;

theorem Th55: :: NDIFF13:54
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 & ( for x being Point of S st x in Z holds
(w `| Z) /. x = <:((u `| Z) /. x),((v `| Z) /. x):> ) )
proof end;

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: :: NDIFF13:def 3
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:>
proof end;
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
proof end;
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: :: NDIFF13:55
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)):]))
proof end;

theorem Th57: :: NDIFF13:56
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):> )
proof end;

theorem Th58: :: NDIFF13:57
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)):> ) )
proof end;

theorem :: NDIFF13:58
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)):> ) )
proof end;

theorem Th60: :: NDIFF13:59
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)):> )
proof end;

theorem Th61: :: NDIFF13:60
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 )
proof end;

theorem :: NDIFF13:61
for X, Y being RealNormSpace
for V being Subset of [:X,Y:]
for D being Subset of X
for E being Subset of Y st D is open & E is open & V = [:D,E:] holds
V is open
proof end;

theorem Th63: :: NDIFF13:62
for E, F, G being RealNormSpace
for x being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for L being Point of (R_NormSpace_of_BoundedLinearOperators ((R_NormSpace_of_BoundedLinearOperators (F,E)),(R_NormSpace_of_BoundedLinearOperators (E,E)))) st x is invertible & ( for y being Point of (R_NormSpace_of_BoundedLinearOperators (F,E)) holds L . y = y * x ) holds
L is invertible
proof end;

theorem Th64: :: NDIFF13:63
for F being non trivial RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators (F,F) is non trivial RealBanachSpace
proof end;

theorem Th65: :: NDIFF13:64
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))) ) )
proof end;

theorem Th66: :: NDIFF13:65
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) ) ) )
proof end;

theorem :: NDIFF13:66
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 )
proof end;