:: Differentiability Properties of Lipschitzian Bilinear Operators in Real Normed Spaces
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received December 9, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

theorem Th1: :: NDIFF12:1

for E, F, G being RealNormSpace
for f being BilinearOperator of E,F,G
for z being Point of [:E,F:] holds
( f * (reproj1 z) is LinearOperator of E,G & f * (reproj2 z) is LinearOperator of F,G )

proof end;

theorem Th2: :: NDIFF12:2

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G
for z being Point of [:E,F:] holds
( f * (reproj1 z) is Lipschitzian LinearOperator of E,G & f * (reproj2 z) is Lipschitzian LinearOperator of F,G & ex g being Point of (R_NormSpace_of_BoundedBilinearOperators (E,F,G)) st
( f = g & ( for x being VECTOR of E holds ||.((f * (reproj1 z)) . x).|| <= (||.g.|| * ||.(z `2).||) * ||.x.|| ) & ( for y being VECTOR of F holds ||.((f * (reproj2 z)) . y).|| <= (||.g.|| * ||.(z `1).||) * ||.y.|| ) ) )

proof end;

theorem Th3: :: NDIFF12:3

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G ex K being Real st
( 0 <= K & ( for z being Point of [:E,F:] holds
( ( for x being Point of E holds ||.((f * (reproj1 z)) . x).|| <= (K * ||.(z `2).||) * ||.x.|| ) & ( for y being Point of F holds ||.((f * (reproj2 z)) . y).|| <= (K * ||.(z `1).||) * ||.y.|| ) ) ) )

proof end;

theorem Th4: :: NDIFF12:4

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G
for z being Point of [:E,F:] holds
( f is_partial_differentiable_in`1 z & partdiff`1 (f,z) = f * (reproj1 z) & f is_partial_differentiable_in`2 z & partdiff`2 (f,z) = f * (reproj2 z) )

proof end;

theorem Th5: :: NDIFF12:5

for E, F being RealNormSpace
for s, t being Point of [:E,F:]
for a being Real holds
( s = [(s `1),(s `2)] & (s + t) `1 = (s `1) + (t `1) & (s + t) `2 = (s `2) + (t `2) & (s - t) `1 = (s `1) - (t `1) & (s - t) `2 = (s `2) - (t `2) & (a * s) `1 = a * (s `1) & (a * s) `2 = a * (s `2) )

proof end;

theorem Th6: :: NDIFF12:6

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G ex K being Real st
( 0 <= K & ( for z being Point of [:E,F:] holds
( ||.(partdiff`1 (f,z)).|| <= K * ||.z.|| & ||.(partdiff`2 (f,z)).|| <= K * ||.z.|| ) ) )

proof end;

theorem Th7: :: NDIFF12:7

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G holds
( ( for z1, z2 being Point of [:E,F:] holds partdiff`1 (f,(z1 + z2)) = (partdiff`1 (f,z1)) + (partdiff`1 (f,z2)) ) & ( for z being Point of [:E,F:]
for a being Real holds partdiff`1 (f,(a * z)) = a * (partdiff`1 (f,z)) ) & ( for z1, z2 being Point of [:E,F:] holds partdiff`1 (f,(z1 - z2)) = (partdiff`1 (f,z1)) - (partdiff`1 (f,z2)) ) )

proof end;

theorem Th8: :: NDIFF12:8

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G holds
( ( for z1, z2 being Point of [:E,F:] holds partdiff`2 (f,(z1 + z2)) = (partdiff`2 (f,z1)) + (partdiff`2 (f,z2)) ) & ( for z being Point of [:E,F:]
for a being Real holds partdiff`2 (f,(a * z)) = a * (partdiff`2 (f,z)) ) & ( for z1, z2 being Point of [:E,F:] holds partdiff`2 (f,(z1 - z2)) = (partdiff`2 (f,z1)) - (partdiff`2 (f,z2)) ) )

proof end;

theorem :: NDIFF12:9

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G
for Z being Subset of [:E,F:] st Z is open holds
( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z )

proof end;

theorem Th10: :: NDIFF12:10

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G ex K being Real st
( 0 <= K & ( for z being Point of [:E,F:] ex L being Lipschitzian LinearOperator of [:E,F:],G st
( ( for dx being Point of E
for dy being Point of F holds L . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ( for s being Point of [:E,F:] holds ||.(L . s).|| <= (K * ||.z.||) * ||.s.|| ) ) ) )

proof end;

theorem Th11: :: NDIFF12:11

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G ex K being Real st
( 0 <= K & ( for z being Point of [:E,F:] holds
( f is_differentiable_in z & ( for dx being Point of E
for dy being Point of F holds (diff (f,z)) . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ||.(diff (f,z)).|| <= K * ||.z.|| ) ) )

proof end;

theorem Th12: :: NDIFF12:12

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G
for z being Point of [:E,F:]
for dx being Point of E
for dy being Point of F holds (diff (f,z)) . (dx,dy) = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy)

proof end;

theorem Th13: :: NDIFF12:13

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G holds
( ( for z1, z2 being Point of [:E,F:] holds diff (f,(z1 + z2)) = (diff (f,z1)) + (diff (f,z2)) ) & ( for z being Point of [:E,F:]
for a being Real holds diff (f,(a * z)) = a * (diff (f,z)) ) & ( for z1, z2 being Point of [:E,F:] holds diff (f,(z1 - z2)) = (diff (f,z1)) - (diff (f,z2)) ) )

proof end;

theorem Th14: :: NDIFF12:14

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G
for Z being Subset of [:E,F:] st Z is open holds
( f is_differentiable_on Z & f `| Z is_continuous_on Z )

proof end;

theorem Th15: :: NDIFF12:15

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G holds
( f `| ([#] [:E,F:]) is Lipschitzian LinearOperator of [:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) & f `| ([#] [:E,F:]) is_differentiable_on [#] [:E,F:] & f `| ([#] [:E,F:]) is_continuous_on the carrier of [:E,F:] & ( for z being Point of [:E,F:] holds diff ((f `| ([#] [:E,F:])),z) = f `| ([#] [:E,F:]) ) )

proof end;

theorem Th16: :: NDIFF12:16

for E, F being RealNormSpace
for L being Lipschitzian LinearOperator of E,F holds
( (diff (L,([#] E))) . 0 = L & (diff (L,([#] E))) . 1 = ([#] E) --> L & (diff (L,([#] E))) . 2 = ([#] E) --> (([#] E) --> (([#] E) --> (0. F))) & (diff (L,([#] E))) . 3 = ([#] E) --> (([#] E) --> (([#] E) --> (([#] E) --> (0. F)))) )

proof end;

theorem :: NDIFF12:17

for E, F being RealNormSpace
for i being Nat holds 0. (diff_SP ((i + 1),E,F)) = ([#] E) --> (0. (diff_SP (i,E,F)))

proof end;

theorem Th18: :: NDIFF12:18

for E, F being RealNormSpace
for L being Lipschitzian LinearOperator of E,F
for i being Nat holds diff (L,(i + 2),([#] E)) = ([#] E) --> (0. (diff_SP ((i + 2),E,F)))

proof end;

theorem Th19: :: NDIFF12:19

for E, F being RealNormSpace
for L being Lipschitzian LinearOperator of E,F
for i being Nat holds
( diff (L,(i + 1),([#] E)) is_differentiable_on [#] E & (diff (L,(i + 1),([#] E))) `| ([#] E) = ([#] E) --> (0. (diff_SP ((i + 2),E,F))) & (diff (L,(i + 1),([#] E))) `| ([#] E) is_continuous_on [#] E )

proof end;

theorem Th20: :: NDIFF12:20

for E, F being RealNormSpace
for L being Lipschitzian LinearOperator of E,F
for i being Nat holds
( diff (L,i,([#] E)) is_differentiable_on [#] E & (diff (L,i,([#] E))) `| ([#] E) is_continuous_on [#] E )

proof end;

theorem :: NDIFF12:21

for E, F, G being RealNormSpace
for B being Lipschitzian BilinearOperator of E,F,G
for i being Nat holds
( diff (B,i,([#] [:E,F:])) is_differentiable_on [#] [:E,F:] & (diff (B,i,([#] [:E,F:]))) `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] )

proof end;