:: 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 ) )

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.|| )

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 )

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 ) )

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

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

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)

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)

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;

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

:: 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 ) ) );

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;

existence

ex b_{1} being Function of [: the carrier of E, the carrier of F:], the carrier of G st b_{1} is Bilinear ;

end;
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

proof 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)) ) ) )

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;

:: 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 ) );

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;

existence

ex b_{1} being Function of [:E,F:],G st b_{1} is Bilinear ;

end;
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

proof 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;

end;
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;

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;

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
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 ) );

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;

existence

ex b_{1} being Function of [:E,F:],G st b_{1} is Bilinear ;

end;
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

proof end;

definition
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;

end;
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;

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;

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:] ) )

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;