:: Continuity of Bounded Linear Operators on Normed Linear Spaces
:: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama
::
:: Received September 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users

theorem Th020: :: LOPBAN_8:1

for E, F being RealNormSpace
for E1 being Subset of E
for f being PartFunc of E,F st E1 is dense & F is complete & dom f = E1 & f is_uniformly_continuous_on E1 holds
( ex g being Function of E,F st
( g | E1 = f & g is_uniformly_continuous_on the carrier of E & ( for x being Point of E ex seq being sequence of E st
( rng seq c= E1 & seq is convergent & lim seq = x & f /* seq is convergent & g . x = lim (f /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds
( f /* seq is convergent & g . x = lim (f /* seq) ) ) ) & ( for g1, g2 being Function of E,F st g1 | E1 = f & g1 is_continuous_on the carrier of E & g2 | E1 = f & g2 is_continuous_on the carrier of E holds
g1 = g2 ) )

proof end;

theorem :: LOPBAN_8:2

for E, F, G being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for g being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) ex h being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) st
( h = g * f & ||.h.|| <= ||.g.|| * ||.f.|| )

proof end;

theorem LMCONT1: :: LOPBAN_8:3

for E, F being RealNormSpace
for L being Lipschitzian LinearOperator of E,F holds
( L is_Lipschitzian_on the carrier of E & L is_uniformly_continuous_on the carrier of E )

proof end;

theorem :: LOPBAN_8:4

for E, F being RealNormSpace
for E1 being SubRealNormSpace of E
for f being Point of (R_NormSpace_of_BoundedLinearOperators (E1,F)) st F is complete & ex E0 being Subset of E st
( E0 = the carrier of E1 & E0 is dense ) holds
( ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) & ( for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) )

proof end;

theorem :: LOPBAN_8:5

for E, F, G being non empty set
for f being Function of [:E,F:],G
for x being object st x in E holds
(curry f) . x is Function of F,G

proof end;

theorem :: LOPBAN_8:6

for E, F, G being non empty set
for f being Function of [:E,F:],G
for y being object st y in F holds
(curry' f) . y is Function of E,G

proof end;

theorem LM4: :: LOPBAN_8:7

for E, F, G being non empty set
for f being Function of [:E,F:],G
for x, y being object st x in E & y in F holds
((curry f) . x) . y = f . (x,y)

proof end;

theorem LM5: :: LOPBAN_8:8

for E, F, G being non empty set
for f being Function of [:E,F:],G
for x, y being object st x in E & y in F holds
((curry' f) . y) . x = f . (x,y)

proof end;

definition

let E, F, G be RealLinearSpace;
let f be Function of [: the carrier of E, the carrier of F:], the carrier of G;

attr f is Bilinear means :: LOPBAN_8:def 1
( ( for v being Point of E st v in dom (curry f) holds
(curry f) . v is additive homogeneous Function of F,G ) & ( for v being Point of F st v in dom (curry' f) holds
(curry' f) . v is additive homogeneous Function of E,G ) );

end;

:: deftheorem defines Bilinear LOPBAN_8:def 1 :
for E, F, G being RealLinearSpace
for f being Function of [: the carrier of E, the carrier of F:], the carrier of G holds
( f is Bilinear iff ( ( for v being Point of E st v in dom (curry f) holds
(curry f) . v is additive homogeneous Function of F,G ) & ( for v being Point of F st v in dom (curry' f) holds
(curry' f) . v is additive homogeneous Function of E,G ) ) );

:: Bilinear Operators

theorem EX1: :: LOPBAN_8:9

for E, F, G being RealLinearSpace holds [: the carrier of E, the carrier of F:] --> (0. G) is Bilinear

proof end;

registration

let E, F, G be RealLinearSpace;

cluster Relation-like [: the carrier of E, the carrier of F:] -defined the carrier of G -valued Function-like total quasi_total Bilinear for Element of bool [:[: the carrier of E, the carrier of F:], the carrier of G:];

correctness
existence
ex b₁ being Function of [: the carrier of E, the carrier of F:], the carrier of G st b₁ is Bilinear ;

proof end;

end;

theorem LM6: :: LOPBAN_8:10

for E, F, G being RealLinearSpace
for L being Function of [: the carrier of E, the carrier of F:], the carrier of G holds
( L is Bilinear iff ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ) ) )

proof end;

definition

let E, F, G be RealLinearSpace;
let f be Function of [:E,F:],G;

attr f is Bilinear means :: LOPBAN_8:def 2
ex g being Function of [: the carrier of E, the carrier of F:], the carrier of G st
( f = g & g is Bilinear );

end;

:: deftheorem defines Bilinear LOPBAN_8:def 2 :
for E, F, G being RealLinearSpace
for f being Function of [:E,F:],G holds
( f is Bilinear iff ex g being Function of [: the carrier of E, the carrier of F:], the carrier of G st
( f = g & g is Bilinear ) );

registration

let E, F, G be RealLinearSpace;

cluster Relation-like the carrier of [:E,F:] -defined the carrier of G -valued non empty Function-like total quasi_total Bilinear for Element of bool [: the carrier of [:E,F:], the carrier of G:];

correctness
existence
ex b₁ being Function of [:E,F:],G st b₁ is Bilinear ;

proof end;

end;

definition

let E, F, G be RealLinearSpace;
let f be Function of [:E,F:],G;
let x be Point of E;
let y be Point of F;
:: original: .
redefine func f . (x,y) -> Point of G;
correctness
coherence
f . (x,y) is Point of G;

proof end;

end;

theorem :: LOPBAN_8:11

for E, F, G being RealLinearSpace
for L being Function of [:E,F:],G holds
( L is Bilinear iff ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ) ) ) by LM6;

definition

let E, F, G be RealLinearSpace;
mode BilinearOperator of E,F,G is Bilinear Function of [:E,F:],G;

end;

definition

let E, F, G be RealNormSpace;
let f be Function of [:E,F:],G;

attr f is Bilinear means :: LOPBAN_8:def 3
ex g being Function of [: the carrier of E, the carrier of F:], the carrier of G st
( f = g & g is Bilinear );

end;

:: deftheorem defines Bilinear LOPBAN_8:def 3 :
for E, F, G being RealNormSpace
for f being Function of [:E,F:],G holds
( f is Bilinear iff ex g being Function of [: the carrier of E, the carrier of F:], the carrier of G st
( f = g & g is Bilinear ) );

registration

let E, F, G be RealNormSpace;

cluster Relation-like the carrier of [:E,F:] -defined the carrier of G -valued non empty Function-like total quasi_total Bilinear for Element of bool [: the carrier of [:E,F:], the carrier of G:];

correctness
existence
ex b₁ being Function of [:E,F:],G st b₁ is Bilinear ;

proof end;

end;

definition

let E, F, G be RealNormSpace;
mode BilinearOperator of E,F,G is Bilinear Function of [:E,F:],G;

end;

definition

let E, F, G be RealNormSpace;
let f be Function of [:E,F:],G;
let x be Point of E;
let y be Point of F;
:: original: .
redefine func f . (x,y) -> Point of G;
correctness
coherence
f . (x,y) is Point of G;

proof end;

end;

theorem LM8: :: LOPBAN_8:12

for E, F, G being RealNormSpace
for L being Function of [:E,F:],G holds
( L is Bilinear iff ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ) ) ) by LM6;

theorem :: LOPBAN_8:13

for E, F, G being RealNormSpace
for f being BilinearOperator of E,F,G holds
( ( f is_continuous_on the carrier of [:E,F:] implies f is_continuous_in 0. [:E,F:] ) & ( f is_continuous_in 0. [:E,F:] implies f is_continuous_on the carrier of [:E,F:] ) & ( f is_continuous_on the carrier of [:E,F:] implies ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) ) & ( ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) implies f is_continuous_on the carrier of [:E,F:] ) )

proof end;