:: Continuity of Bounded Linear Operators on Normed Linear Spaces
:: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama
::
:: 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
for g being Point of ex h being Point of st
( 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 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 st
( dom g = the carrier of E & g | the carrier of E1 = 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 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
() . 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
() . 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
(() . 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
(() . 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 () holds
() . v is additive homogeneous Function of F,G ) & ( for v being Point of F st v in dom () holds
() . 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 () holds
() . v is additive homogeneous Function of F,G ) & ( for v being Point of F st v in dom () holds
() . 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 b1 being Function of [: the carrier of E, the carrier of F:], the carrier of G st b1 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 b1 being Function of [:E,F:],G st b1 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 b1 being Function of [:E,F:],G st b1 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 * ) * ) ) ) & ( ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ) * ) ) implies f is_continuous_on the carrier of [:E,F:] ) )
proof end;