lopban_9.miz
begin
LMELM1: for X,Y be
RealLinearSpace, x be
Point of X, y be
Point of Y holds
[x, y] is
Point of
[:X, Y:]
proof
let X,Y be
RealLinearSpace, x be
Point of X, y be
Point of Y;
[x, y] is
set by
TARSKI: 1;
hence
[x, y] is
Point of
[:X, Y:] by
PRVECT_3: 9;
end;
definition
let X,Y,Z be
RealLinearSpace;
::
LOPBAN_9:def1
func
BilinearOperators (X,Y,Z) ->
Subset of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) means
:
Def6: for x be
set holds x
in it iff x is
BilinearOperator of X, Y, Z;
existence
proof
defpred
P[
object] means $1 is
BilinearOperator of X, Y, Z;
consider IT be
set such that
A1: for x be
object holds x
in IT iff x
in (
Funcs (the
carrier of
[:X, Y:],the
carrier of Z)) &
P[x] from
XBOOLE_0:sch 1;
take IT;
for x be
object st x
in IT holds x
in (
Funcs (the
carrier of
[:X, Y:],the
carrier of Z)) by
A1;
hence IT is
Subset of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) by
TARSKI:def 3;
let x be
set;
thus x
in IT implies x is
BilinearOperator of X, Y, Z by
A1;
assume
A2: x is
BilinearOperator of X, Y, Z;
then x
in (
Funcs (the
carrier of
[:X, Y:],the
carrier of Z)) by
FUNCT_2: 8;
hence thesis by
A1,
A2;
end;
uniqueness
proof
let X1,X2 be
Subset of (
RealVectSpace (the
carrier of
[:X, Y:],Z));
assume that
A3: for x be
set holds x
in X1 iff x is
BilinearOperator of X, Y, Z and
A4: for x be
set holds x
in X2 iff x is
BilinearOperator of X, Y, Z;
A5: X2
c= X1
proof
let x be
object;
assume x
in X2;
then x is
BilinearOperator of X, Y, Z by
A4;
hence thesis by
A3;
end;
X1
c= X2
proof
let x be
object;
assume x
in X1;
then x is
BilinearOperator of X, Y, Z by
A3;
hence thesis by
A4;
end;
hence thesis by
A5,
XBOOLE_0:def 10;
end;
end
registration
let X,Y,Z be
RealLinearSpace;
cluster (
BilinearOperators (X,Y,Z)) -> non
empty
functional;
coherence
proof
set f = the
BilinearOperator of X, Y, Z;
f
in (
BilinearOperators (X,Y,Z)) by
Def6;
hence (
BilinearOperators (X,Y,Z)) is non
empty;
let x be
object;
assume x
in (
BilinearOperators (X,Y,Z));
hence thesis;
end;
end
LM14: for X be
RealLinearSpace, x1,x2,x3,x4 be
Point of X holds ((x1
+ x2)
+ (x3
+ x4))
= ((x1
+ x3)
+ (x2
+ x4))
proof
let X be
RealLinearSpace, x1,x2,x3,x4 be
Point of X;
thus ((x1
+ x2)
+ (x3
+ x4))
= (((x1
+ x2)
+ x3)
+ x4) by
RLVECT_1:def 3
.= (((x1
+ x3)
+ x2)
+ x4) by
RLVECT_1:def 3
.= ((x1
+ x3)
+ (x2
+ x4)) by
RLVECT_1:def 3;
end;
Th14: for X,Y,Z be
RealLinearSpace holds (
BilinearOperators (X,Y,Z)) is
linearly-closed
proof
let X,Y,Z be
RealLinearSpace;
set W = (
BilinearOperators (X,Y,Z));
A1: for v,u be
VECTOR of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) st v
in (
BilinearOperators (X,Y,Z)) & u
in (
BilinearOperators (X,Y,Z)) holds (v
+ u)
in (
BilinearOperators (X,Y,Z))
proof
let v,u be
VECTOR of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) such that
A2: v
in W and
A3: u
in W;
reconsider u1 = u as
BilinearOperator of X, Y, Z by
A3,
Def6;
reconsider v1 = v as
BilinearOperator of X, Y, Z by
A2,
Def6;
(v
+ u) is
BilinearOperator of X, Y, Z
proof
reconsider L = (v
+ u) as
Function of
[:X, Y:], Z by
FUNCT_2: 66;
A4: for x1,x2 be
Point of X, y be
Point of Y holds (L
. ((x1
+ x2),y))
= ((L
. (x1,y))
+ (L
. (x2,y)))
proof
let x1,x2 be
Point of X, y be
Point of Y;
A5:
[x1, y] is
Element of
[:X, Y:] &
[x2, y] is
Element of
[:X, Y:] &
[(x1
+ x2), y] is
Element of
[:X, Y:] by
LMELM1;
hence (L
. ((x1
+ x2),y))
= ((v1
. ((x1
+ x2),y))
+ (u1
. ((x1
+ x2),y))) by
LOPBAN_1: 1
.= (((v1
. (x1,y))
+ (v1
. (x2,y)))
+ (u1
. ((x1
+ x2),y))) by
LOPBAN_8: 11
.= (((v1
. (x1,y))
+ (v1
. (x2,y)))
+ ((u1
. (x1,y))
+ (u1
. (x2,y)))) by
LOPBAN_8: 11
.= (((v1
. (x1,y))
+ (u1
. (x1,y)))
+ ((v1
. (x2,y))
+ (u1
. (x2,y)))) by
LM14
.= ((L
. (x1,y))
+ ((v1
. (x2,y))
+ (u1
. (x2,y)))) by
A5,
LOPBAN_1: 1
.= ((L
. (x1,y))
+ (L
. (x2,y))) by
A5,
LOPBAN_1: 1;
end;
A6: for x be
Point of X, y be
Point of Y, a be
Real holds (L
. ((a
* x),y))
= (a
* (L
. (x,y)))
proof
let x be
Point of X, y be
Point of Y, a be
Real;
A7:
[x, y] is
Element of
[:X, Y:] &
[(a
* x), y] is
Element of
[:X, Y:] by
LMELM1;
hence (L
. ((a
* x),y))
= ((v1
. ((a
* x),y))
+ (u1
. ((a
* x),y))) by
LOPBAN_1: 1
.= ((a
* (v1
. (x,y)))
+ (u1
. ((a
* x),y))) by
LOPBAN_8: 11
.= ((a
* (v1
. (x,y)))
+ (a
* (u1
. (x,y)))) by
LOPBAN_8: 11
.= (a
* ((v1
. (x,y))
+ (u1
. (x,y)))) by
RLVECT_1:def 5
.= (a
* (L
. (x,y))) by
A7,
LOPBAN_1: 1;
end;
A8: for x be
Point of X, y1,y2 be
Point of Y holds (L
. (x,(y1
+ y2)))
= ((L
. (x,y1))
+ (L
. (x,y2)))
proof
let x be
Point of X, y1,y2 be
Point of Y;
A9:
[x, y1] is
Element of
[:X, Y:] &
[x, y2] is
Element of
[:X, Y:] &
[x, (y1
+ y2)] is
Element of
[:X, Y:] by
LMELM1;
hence (L
. (x,(y1
+ y2)))
= ((v1
. (x,(y1
+ y2)))
+ (u1
. (x,(y1
+ y2)))) by
LOPBAN_1: 1
.= (((v1
. (x,y1))
+ (v1
. (x,y2)))
+ (u1
. (x,(y1
+ y2)))) by
LOPBAN_8: 11
.= (((v1
. (x,y1))
+ (v1
. (x,y2)))
+ ((u1
. (x,y1))
+ (u1
. (x,y2)))) by
LOPBAN_8: 11
.= (((v1
. (x,y1))
+ (u1
. (x,y1)))
+ ((v1
. (x,y2))
+ (u1
. (x,y2)))) by
LM14
.= ((L
. (x,y1))
+ ((v1
. (x,y2))
+ (u1
. (x,y2)))) by
A9,
LOPBAN_1: 1
.= ((L
. (x,y1))
+ (L
. (x,y2))) by
A9,
LOPBAN_1: 1;
end;
for x be
Point of X, y be
Point of Y, a be
Real holds (L
. (x,(a
* y)))
= (a
* (L
. (x,y)))
proof
let x be
Point of X, y be
Point of Y, a be
Real;
A10:
[x, y] is
Element of
[:X, Y:] &
[x, (a
* y)] is
Element of
[:X, Y:] by
LMELM1;
hence (L
. (x,(a
* y)))
= ((v1
. (x,(a
* y)))
+ (u1
. (x,(a
* y)))) by
LOPBAN_1: 1
.= ((a
* (v1
. (x,y)))
+ (u1
. (x,(a
* y)))) by
LOPBAN_8: 11
.= ((a
* (v1
. (x,y)))
+ (a
* (u1
. (x,y)))) by
LOPBAN_8: 11
.= (a
* ((v1
. (x,y))
+ (u1
. (x,y)))) by
RLVECT_1:def 5
.= (a
* (L
. (x,y))) by
A10,
LOPBAN_1: 1;
end;
hence thesis by
A4,
A6,
A8,
LOPBAN_8: 11;
end;
hence thesis by
Def6;
end;
for b be
Real holds for v be
VECTOR of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) st v
in W holds (b
* v)
in W
proof
let b be
Real;
let v be
VECTOR of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) such that
A11: v
in W;
reconsider v1 = v as
BilinearOperator of X, Y, Z by
A11,
Def6;
(b
* v) is
BilinearOperator of X, Y, Z
proof
reconsider L = (b
* v) as
Function of
[:X, Y:], Z by
FUNCT_2: 66;
A12: for x1,x2 be
Point of X, y be
Point of Y holds (L
. ((x1
+ x2),y))
= ((L
. (x1,y))
+ (L
. (x2,y)))
proof
let x1,x2 be
Point of X, y be
Point of Y;
A13:
[x1, y] is
Element of
[:X, Y:] &
[x2, y] is
Element of
[:X, Y:] &
[(x1
+ x2), y] is
Element of
[:X, Y:] by
LMELM1;
hence (L
. ((x1
+ x2),y))
= (b
* (v1
. ((x1
+ x2),y))) by
LOPBAN_1: 2
.= (b
* ((v1
. (x1,y))
+ (v1
. (x2,y)))) by
LOPBAN_8: 11
.= ((b
* (v1
. (x1,y)))
+ (b
* (v1
. (x2,y)))) by
RLVECT_1:def 5
.= ((L
. (x1,y))
+ (b
* (v1
. (x2,y)))) by
A13,
LOPBAN_1: 2
.= ((L
. (x1,y))
+ (L
. (x2,y))) by
A13,
LOPBAN_1: 2;
end;
A14: for x be
Point of X, y be
Point of Y, a be
Real holds (L
. ((a
* x),y))
= (a
* (L
. (x,y)))
proof
let x be
Point of X, y be
Point of Y, a be
Real;
A15:
[x, y] is
Element of
[:X, Y:] &
[(a
* x), y] is
Element of
[:X, Y:] by
LMELM1;
hence (L
. ((a
* x),y))
= (b
* (v1
. ((a
* x),y))) by
LOPBAN_1: 2
.= (b
* (a
* (v1
. (x,y)))) by
LOPBAN_8: 11
.= ((b
* a)
* (v1
. (x,y))) by
RLVECT_1:def 7
.= (a
* (b
* (v1
. (x,y)))) by
RLVECT_1:def 7
.= (a
* (L
. (x,y))) by
A15,
LOPBAN_1: 2;
end;
A16: for x be
Point of X, y1,y2 be
Point of Y holds (L
. (x,(y1
+ y2)))
= ((L
. (x,y1))
+ (L
. (x,y2)))
proof
let x be
Point of X, y1,y2 be
Point of Y;
A17:
[x, y1] is
Element of
[:X, Y:] &
[x, y2] is
Element of
[:X, Y:] &
[x, (y1
+ y2)] is
Element of
[:X, Y:] by
LMELM1;
hence (L
. (x,(y1
+ y2)))
= (b
* (v1
. (x,(y1
+ y2)))) by
LOPBAN_1: 2
.= (b
* ((v1
. (x,y1))
+ (v1
. (x,y2)))) by
LOPBAN_8: 11
.= ((b
* (v1
. (x,y1)))
+ (b
* (v1
. (x,y2)))) by
RLVECT_1:def 5
.= ((L
. (x,y1))
+ (b
* (v1
. (x,y2)))) by
A17,
LOPBAN_1: 2
.= ((L
. (x,y1))
+ (L
. (x,y2))) by
A17,
LOPBAN_1: 2;
end;
for x be
Point of X, y be
Point of Y, a be
Real holds (L
. (x,(a
* y)))
= (a
* (L
. (x,y)))
proof
let x be
Point of X, y be
Point of Y, a be
Real;
A18:
[x, y] is
Element of
[:X, Y:] &
[x, (a
* y)] is
Element of
[:X, Y:] by
LMELM1;
hence (L
. (x,(a
* y)))
= (b
* (v1
. (x,(a
* y)))) by
LOPBAN_1: 2
.= (b
* (a
* (v1
. (x,y)))) by
LOPBAN_8: 11
.= ((b
* a)
* (v1
. (x,y))) by
RLVECT_1:def 7
.= (a
* (b
* (v1
. (x,y)))) by
RLVECT_1:def 7
.= (a
* (L
. (x,y))) by
A18,
LOPBAN_1: 2;
end;
hence thesis by
A12,
A14,
A16,
LOPBAN_8: 11;
end;
hence thesis by
Def6;
end;
hence thesis by
A1,
RLSUB_1:def 1;
end;
registration
let X,Y,Z be
RealLinearSpace;
cluster (
BilinearOperators (X,Y,Z)) ->
linearly-closed;
coherence by
Th14;
end
definition
let X,Y,Z be
RealLinearSpace;
::
LOPBAN_9:def2
func
R_VectorSpace_of_BilinearOperators (X,Y,Z) ->
strict
RLSStruct equals
RLSStruct (# (
BilinearOperators (X,Y,Z)), (
Zero_ ((
BilinearOperators (X,Y,Z)),(
RealVectSpace (the
carrier of
[:X, Y:],Z)))), (
Add_ ((
BilinearOperators (X,Y,Z)),(
RealVectSpace (the
carrier of
[:X, Y:],Z)))), (
Mult_ ((
BilinearOperators (X,Y,Z)),(
RealVectSpace (the
carrier of
[:X, Y:],Z)))) #);
coherence ;
end
registration
let X,Y,Z be
RealLinearSpace;
cluster (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) -> non
empty;
coherence ;
end
registration
let X,Y,Z be
RealLinearSpace;
cluster (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) ->
Abelian
add-associative
right_zeroed
right_complementable
vector-distributive
scalar-distributive
scalar-associative
scalar-unital;
coherence by
RSSPACE: 11;
end
registration
let X,Y,Z be
RealLinearSpace;
cluster (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) ->
constituted-Functions;
coherence by
MONOID_0: 80;
end
theorem ::
LOPBAN_9:1
for X,Y,Z be
RealLinearSpace holds (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) is
Subspace of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) by
RSSPACE: 11;
definition
let X,Y,Z be
RealLinearSpace;
let f be
Element of (
R_VectorSpace_of_BilinearOperators (X,Y,Z));
let v be
VECTOR of X, w be
VECTOR of Y;
:: original:
.
redefine
func f
. (v,w) ->
VECTOR of Z ;
coherence
proof
reconsider f as
BilinearOperator of X, Y, Z by
Def6;
(f
. (v,w)) is
VECTOR of Z;
hence thesis;
end;
end
theorem ::
LOPBAN_9:2
Th16: for X,Y,Z be
RealLinearSpace holds for f,g,h be
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds h
= (f
+ g) iff for x be
VECTOR of X, y be
VECTOR of Y holds (h
. (x,y))
= ((f
. (x,y))
+ (g
. (x,y)))
proof
let X,Y,Z be
RealLinearSpace;
let f,g,h be
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z));
reconsider f9 = f, g9 = g, h9 = h as
BilinearOperator of X, Y, Z by
Def6;
A1: (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) is
Subspace of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) by
RSSPACE: 11;
then
reconsider f1 = f as
VECTOR of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) by
RLSUB_1: 10;
reconsider h1 = h as
VECTOR of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) by
A1,
RLSUB_1: 10;
reconsider g1 = g as
VECTOR of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) by
A1,
RLSUB_1: 10;
A2:
now
assume
A3: h
= (f
+ g);
let x be
Element of X, y be
Element of Y;
A4: h1
= (f1
+ g1) by
A1,
A3,
RLSUB_1: 13;
[x, y] is
Element of
[:X, Y:] by
LMELM1;
hence (h9
. (x,y))
= ((f9
. (x,y))
+ (g9
. (x,y))) by
A4,
LOPBAN_1: 1;
end;
now
assume
A5: for x be
Element of X, y be
Element of Y holds (h9
. (x,y))
= ((f9
. (x,y))
+ (g9
. (x,y)));
for z be
Element of
[:X, Y:] holds (h9
. z)
= ((f9
. z)
+ (g9
. z))
proof
let z be
Element of
[:X, Y:];
consider x be
Point of X, y be
Point of Y such that
A6: z
=
[x, y] by
PRVECT_3: 9;
thus (h9
. z)
= (h9
. (x,y)) by
A6
.= ((f9
. (x,y))
+ (g9
. (x,y))) by
A5
.= ((f9
. z)
+ (g9
. z)) by
A6;
end;
then h1
= (f1
+ g1) by
LOPBAN_1: 1;
hence h
= (f
+ g) by
A1,
RLSUB_1: 13;
end;
hence thesis by
A2;
end;
theorem ::
LOPBAN_9:3
Th17: for X,Y,Z be
RealLinearSpace holds for f,h be
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds for a be
Real holds h
= (a
* f) iff for x be
VECTOR of X, y be
VECTOR of Y holds (h
. (x,y))
= (a
* (f
. (x,y)))
proof
let X,Y,Z be
RealLinearSpace;
let f,h be
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z));
reconsider f9 = f, h9 = h as
BilinearOperator of X, Y, Z by
Def6;
let a be
Real;
A1: (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) is
Subspace of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) by
RSSPACE: 11;
then
reconsider f1 = f as
VECTOR of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) by
RLSUB_1: 10;
reconsider h1 = h as
VECTOR of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) by
A1,
RLSUB_1: 10;
A2:
now
assume
A3: h
= (a
* f);
let x be
Element of X, y be
Element of Y;
A4: h1
= (a
* f1) by
A1,
A3,
RLSUB_1: 14;
[x, y] is
Element of
[:X, Y:] by
LMELM1;
hence (h9
. (x,y))
= (a
* (f9
. (x,y))) by
A4,
LOPBAN_1: 2;
end;
now
assume
A5: for x be
Element of X, y be
Element of Y holds (h9
. (x,y))
= (a
* (f9
. (x,y)));
for z be
Element of
[:X, Y:] holds (h9
. z)
= (a
* (f9
. z))
proof
let z be
Element of
[:X, Y:];
consider x be
Point of X, y be
Point of Y such that
A6: z
=
[x, y] by
PRVECT_3: 9;
thus (h9
. z)
= (h9
. (x,y)) by
A6
.= (a
* (f9
. (x,y))) by
A5
.= (a
* (f9
. z)) by
A6;
end;
then h1
= (a
* f1) by
LOPBAN_1: 2;
hence h
= (a
* f) by
A1,
RLSUB_1: 14;
end;
hence thesis by
A2;
end;
theorem ::
LOPBAN_9:4
Th18: for X,Y,Z be
RealLinearSpace holds (
0. (
R_VectorSpace_of_BilinearOperators (X,Y,Z)))
= (the
carrier of
[:X, Y:]
--> (
0. Z))
proof
let X,Y,Z be
RealLinearSpace;
A1: (
0. (
RealVectSpace (the
carrier of
[:X, Y:],Z)))
= (the
carrier of
[:X, Y:]
--> (
0. Z));
(
R_VectorSpace_of_BilinearOperators (X,Y,Z)) is
Subspace of (
RealVectSpace (the
carrier of
[:X, Y:],Z)) by
RSSPACE: 11;
hence thesis by
A1,
RLSUB_1: 11;
end;
theorem ::
LOPBAN_9:5
for X,Y,Z be
RealLinearSpace holds (the
carrier of
[:X, Y:]
--> (
0. Z)) is
BilinearOperator of X, Y, Z by
LOPBAN_8: 9,
LOPBAN_8:def 2;
begin
LMELM2: for X,Y be
RealNormSpace, x be
Point of X, y be
Point of Y holds
[x, y] is
Point of
[:X, Y:]
proof
let X,Y be
RealNormSpace, x be
Point of X, y be
Point of Y;
[x, y] is
set by
TARSKI: 1;
hence
[x, y] is
Point of
[:X, Y:] by
PRVECT_3: 18;
end;
definition
let X,Y,Z be
RealNormSpace;
let IT be
BilinearOperator of X, Y, Z;
::
LOPBAN_9:def3
attr IT is
Lipschitzian means
:
Def8: ex K be
Real st
0
<= K & for x be
VECTOR of X, y be
VECTOR of Y holds
||.(IT
. (x,y)).||
<= ((K
*
||.x.||)
*
||.y.||);
end
theorem ::
LOPBAN_9:6
Th21: for X,Y,Z be
RealNormSpace holds for f be
BilinearOperator of X, Y, Z st (for x be
VECTOR of X, y be
VECTOR of Y holds (f
. (x,y))
= (
0. Z)) holds f is
Lipschitzian
proof
let X,Y,Z be
RealNormSpace;
let f be
BilinearOperator of X, Y, Z such that
A1: for x be
VECTOR of X, y be
VECTOR of Y holds (f
. (x,y))
= (
0. Z);
A2:
now
let x be
VECTOR of X, y be
VECTOR of Y;
thus
||.(f
. (x,y)).||
=
||.(
0. Z).|| by
A1
.= ((
0
*
||.x.||)
*
||.y.||);
end;
take
0 ;
thus thesis by
A2;
end;
theorem ::
LOPBAN_9:7
for X,Y,Z be
RealNormSpace holds (the
carrier of
[:X, Y:]
--> (
0. Z)) is
BilinearOperator of X, Y, Z by
LOPBAN_8: 9,
LOPBAN_8:def 3;
registration
let X,Y,Z be
RealNormSpace;
cluster
Lipschitzian for
BilinearOperator of X, Y, Z;
existence
proof
set f = (the
carrier of
[:X, Y:]
--> (
0. Z));
reconsider f as
BilinearOperator of X, Y, Z by
LOPBAN_8: 9,
LOPBAN_8:def 3;
take f;
for x be
VECTOR of X, y be
VECTOR of Y holds (f
. (x,y))
= (
0. Z)
proof
let x be
VECTOR of X, y be
VECTOR of Y;
[x, y] is
Point of
[:X, Y:] by
LMELM2;
hence thesis by
FUNCOP_1: 7;
end;
hence thesis by
Th21;
end;
end
theorem ::
LOPBAN_9:8
EQSET: for X,Y,Z be
RealNormSpace, z be
object holds (z
in (
BilinearOperators (X,Y,Z)) iff z is
BilinearOperator of X, Y, Z)
proof
let X,Y,Z be
RealNormSpace, z be
object;
reconsider X0 = X, Y0 = Y, Z0 = Z as
RealLinearSpace;
hereby
assume z
in (
BilinearOperators (X,Y,Z));
then z is
BilinearOperator of X0, Y0, Z0 by
Def6;
then
consider g be
Function of
[:the
carrier of X0, the
carrier of Y0:], the
carrier of Z0 such that
A1: z
= g & g is
Bilinear by
LOPBAN_8:def 2;
thus z is
BilinearOperator of X, Y, Z by
A1,
LOPBAN_8:def 3;
end;
assume z is
BilinearOperator of X, Y, Z;
then
consider g be
Function of
[:the
carrier of X, the
carrier of Y:], the
carrier of Z such that
A1: z
= g & g is
Bilinear by
LOPBAN_8:def 3;
reconsider w = g as
BilinearOperator of X0, Y0, Z0 by
LOPBAN_8:def 2,
A1;
w
in (
BilinearOperators (X,Y,Z)) by
Def6;
hence z
in (
BilinearOperators (X,Y,Z)) by
A1;
end;
definition
let X,Y,Z be
RealNormSpace;
::
LOPBAN_9:def4
func
BoundedBilinearOperators (X,Y,Z) ->
Subset of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) means
:
Def9: for x be
set holds x
in it iff x is
Lipschitzian
BilinearOperator of X, Y, Z;
existence
proof
defpred
P[
object] means $1 is
Lipschitzian
BilinearOperator of X, Y, Z;
consider IT be
set such that
A1: for x be
object holds x
in IT iff x
in (
BilinearOperators (X,Y,Z)) &
P[x] from
XBOOLE_0:sch 1;
take IT;
for x be
object st x
in IT holds x
in (
BilinearOperators (X,Y,Z)) by
A1;
hence IT is
Subset of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
TARSKI:def 3;
let x be
set;
thus x
in IT implies x is
Lipschitzian
BilinearOperator of X, Y, Z by
A1;
assume x is
Lipschitzian
BilinearOperator of X, Y, Z;
hence thesis by
A1,
EQSET;
end;
uniqueness
proof
let X1,X2 be
Subset of (
R_VectorSpace_of_BilinearOperators (X,Y,Z));
assume that
A3: for x be
set holds x
in X1 iff x is
Lipschitzian
BilinearOperator of X, Y, Z and
A4: for x be
set holds x
in X2 iff x is
Lipschitzian
BilinearOperator of X, Y, Z;
A5: X2
c= X1
proof
let x be
object;
assume x
in X2;
then x is
Lipschitzian
BilinearOperator of X, Y, Z by
A4;
hence thesis by
A3;
end;
X1
c= X2
proof
let x be
object;
assume x
in X1;
then x is
Lipschitzian
BilinearOperator of X, Y, Z by
A3;
hence thesis by
A4;
end;
hence thesis by
A5,
XBOOLE_0:def 10;
end;
end
registration
let X,Y,Z be
RealNormSpace;
cluster (
BoundedBilinearOperators (X,Y,Z)) -> non
empty;
coherence
proof
set f = (the
carrier of
[:X, Y:]
--> (
0. Z));
reconsider f as
BilinearOperator of X, Y, Z by
LOPBAN_8: 9,
LOPBAN_8:def 3;
for x be
VECTOR of X, y be
VECTOR of Y holds (f
. (x,y))
= (
0. Z)
proof
let x be
VECTOR of X, y be
VECTOR of Y;
[x, y] is
Point of
[:X, Y:] by
LMELM2;
hence thesis by
FUNCOP_1: 7;
end;
then f is
Lipschitzian by
Th21;
hence thesis by
Def9;
end;
end
registration
let X,Y,Z be
RealNormSpace;
cluster (
BoundedBilinearOperators (X,Y,Z)) ->
linearly-closed;
coherence
proof
set W = (
BoundedBilinearOperators (X,Y,Z));
A1: for v,u be
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) st v
in W & u
in W holds (v
+ u)
in W
proof
let v,u be
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) such that
A2: v
in W and
A3: u
in W;
reconsider f = (v
+ u) as
BilinearOperator of X, Y, Z by
EQSET;
f is
Lipschitzian
proof
reconsider v1 = v as
Lipschitzian
BilinearOperator of X, Y, Z by
A2,
Def9;
consider K2 be
Real such that
A4:
0
<= K2 and
A5: for x be
VECTOR of X, y be
VECTOR of Y holds
||.(v1
. (x,y)).||
<= ((K2
*
||.x.||)
*
||.y.||) by
Def8;
reconsider u1 = u as
Lipschitzian
BilinearOperator of X, Y, Z by
A3,
Def9;
consider K1 be
Real such that
A6:
0
<= K1 and
A7: for x be
VECTOR of X, y be
VECTOR of Y holds
||.(u1
. (x,y)).||
<= ((K1
*
||.x.||)
*
||.y.||) by
Def8;
take K3 = (K1
+ K2);
now
let x be
VECTOR of X, y be
VECTOR of Y;
A8:
||.((u1
. (x,y))
+ (v1
. (x,y))).||
<= (
||.(u1
. (x,y)).||
+
||.(v1
. (x,y)).||) by
NORMSP_1:def 1;
A9:
||.(v1
. (x,y)).||
<= ((K2
*
||.x.||)
*
||.y.||) by
A5;
||.(u1
. (x,y)).||
<= ((K1
*
||.x.||)
*
||.y.||) by
A7;
then
A10: (
||.(u1
. (x,y)).||
+
||.(v1
. (x,y)).||)
<= (((K1
*
||.x.||)
*
||.y.||)
+ ((K2
*
||.x.||)
*
||.y.||)) by
A9,
XREAL_1: 7;
||.(f
. (x,y)).||
=
||.((u1
. (x,y))
+ (v1
. (x,y))).|| by
Th16;
hence
||.(f
. (x,y)).||
<= ((K3
*
||.x.||)
*
||.y.||) by
A8,
A10,
XXREAL_0: 2;
end;
hence thesis by
A4,
A6;
end;
hence thesis by
Def9;
end;
for a be
Real holds for v be
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) st v
in W holds (a
* v)
in W
proof
let a be
Real;
let v be
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) such that
A11: v
in W;
reconsider f = (a
* v) as
BilinearOperator of X, Y, Z by
EQSET;
f is
Lipschitzian
proof
reconsider v1 = v as
Lipschitzian
BilinearOperator of X, Y, Z by
A11,
Def9;
consider K be
Real such that
A12:
0
<= K and
A13: for x be
VECTOR of X, y be
VECTOR of Y holds
||.(v1
. (x,y)).||
<= ((K
*
||.x.||)
*
||.y.||) by
Def8;
take (
|.a.|
* K);
A14:
now
let x be
VECTOR of X, y be
VECTOR of Y;
0
<=
|.a.| by
COMPLEX1: 46;
then
A15: (
|.a.|
*
||.(v1
. (x,y)).||)
<= (
|.a.|
* ((K
*
||.x.||)
*
||.y.||)) by
A13,
XREAL_1: 64;
||.(a
* (v1
. (x,y))).||
= (
|.a.|
*
||.(v1
. (x,y)).||) by
NORMSP_1:def 1;
hence
||.(f
. (x,y)).||
<= (((
|.a.|
* K)
*
||.x.||)
*
||.y.||) by
A15,
Th17;
end;
0
<=
|.a.| by
COMPLEX1: 46;
hence thesis by
A12,
A14;
end;
hence thesis by
Def9;
end;
hence thesis by
A1,
RLSUB_1:def 1;
end;
end
definition
let X,Y,Z be
RealNormSpace;
::
LOPBAN_9:def5
func
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) ->
strict
RLSStruct equals
RLSStruct (# (
BoundedBilinearOperators (X,Y,Z)), (
Zero_ ((
BoundedBilinearOperators (X,Y,Z)),(
R_VectorSpace_of_BilinearOperators (X,Y,Z)))), (
Add_ ((
BoundedBilinearOperators (X,Y,Z)),(
R_VectorSpace_of_BilinearOperators (X,Y,Z)))), (
Mult_ ((
BoundedBilinearOperators (X,Y,Z)),(
R_VectorSpace_of_BilinearOperators (X,Y,Z)))) #);
coherence ;
end
theorem ::
LOPBAN_9:9
for X,Y,Z be
RealNormSpace holds (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) is
Subspace of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
RSSPACE: 11;
registration
let X,Y,Z be
RealNormSpace;
cluster (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) -> non
empty;
coherence ;
end
registration
let X,Y,Z be
RealNormSpace;
cluster (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) ->
Abelian
add-associative
right_zeroed
right_complementable
vector-distributive
scalar-distributive
scalar-associative
scalar-unital;
coherence by
RSSPACE: 11;
end
registration
let X,Y,Z be
RealNormSpace;
cluster (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) ->
constituted-Functions;
coherence by
MONOID_0: 80;
end
definition
let X,Y,Z be
RealNormSpace;
let f be
Element of (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z));
let v be
VECTOR of X, w be
VECTOR of Y;
:: original:
.
redefine
func f
. (v,w) ->
VECTOR of Z ;
coherence
proof
reconsider f as
BilinearOperator of X, Y, Z by
Def9;
(f
. (v,w)) is
VECTOR of Z;
hence thesis;
end;
end
theorem ::
LOPBAN_9:10
Th24: for X,Y,Z be
RealNormSpace holds for f,g,h be
VECTOR of (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) holds h
= (f
+ g) iff for x be
VECTOR of X, y be
VECTOR of Y holds (h
. (x,y))
= ((f
. (x,y))
+ (g
. (x,y)))
proof
let X,Y,Z be
RealNormSpace;
let f,g,h be
VECTOR of (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z));
A1: (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) is
Subspace of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
RSSPACE: 11;
then
reconsider f1 = f as
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
RLSUB_1: 10;
reconsider h1 = h as
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
A1,
RLSUB_1: 10;
reconsider g1 = g as
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
A1,
RLSUB_1: 10;
hereby
assume
A2: h
= (f
+ g);
let x be
Element of X, y be
Element of Y;
h1
= (f1
+ g1) by
A1,
A2,
RLSUB_1: 13;
hence (h
. (x,y))
= ((f
. (x,y))
+ (g
. (x,y))) by
Th16;
end;
assume for x be
Element of X, y be
Element of Y holds (h
. (x,y))
= ((f
. (x,y))
+ (g
. (x,y)));
then h1
= (f1
+ g1) by
Th16;
hence thesis by
A1,
RLSUB_1: 13;
end;
theorem ::
LOPBAN_9:11
Th25: for X,Y,Z be
RealNormSpace holds for f,h be
VECTOR of (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) holds for a be
Real holds h
= (a
* f) iff for x be
VECTOR of X, y be
VECTOR of Y holds (h
. (x,y))
= (a
* (f
. (x,y)))
proof
let X,Y,Z be
RealNormSpace;
let f,h be
VECTOR of (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z));
let a be
Real;
A1: (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) is
Subspace of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
RSSPACE: 11;
then
reconsider f1 = f as
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
RLSUB_1: 10;
reconsider h1 = h as
VECTOR of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
A1,
RLSUB_1: 10;
hereby
assume
A2: h
= (a
* f);
let x be
Element of X, y be
Element of Y;
h1
= (a
* f1) by
A1,
A2,
RLSUB_1: 14;
hence (h
. (x,y))
= (a
* (f
. (x,y))) by
Th17;
end;
assume for x be
Element of X, y be
Element of Y holds (h
. (x,y))
= (a
* (f
. (x,y)));
then h1
= (a
* f1) by
Th17;
hence thesis by
A1,
RLSUB_1: 14;
end;
theorem ::
LOPBAN_9:12
Th26: for X,Y,Z be
RealNormSpace holds (
0. (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)))
= (the
carrier of
[:X, Y:]
--> (
0. Z))
proof
let X,Y,Z be
RealNormSpace;
A1: (
0. (
R_VectorSpace_of_BilinearOperators (X,Y,Z)))
= (the
carrier of
[:X, Y:]
--> (
0. Z)) by
Th18;
(
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) is
Subspace of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
RSSPACE: 11;
hence thesis by
A1,
RLSUB_1: 11;
end;
definition
let X,Y,Z be
RealNormSpace;
let f be
object;
::
LOPBAN_9:def6
func
modetrans (f,X,Y,Z) ->
Lipschitzian
BilinearOperator of X, Y, Z equals
:
Def11: f;
coherence by
A1,
Def9;
end
definition
let X,Y,Z be
RealNormSpace;
let u be
BilinearOperator of X, Y, Z;
::
LOPBAN_9:def7
func
PreNorms (u) -> non
empty
Subset of
REAL equals {
||.(u
. (t,s)).|| where t be
VECTOR of X, s be
VECTOR of Y :
||.t.||
<= 1 &
||.s.||
<= 1 };
coherence
proof
A1:
now
let x be
object;
now
assume x
in {
||.(u
. (t,s)).|| where t be
VECTOR of X, s be
VECTOR of Y :
||.t.||
<= 1 &
||.s.||
<= 1 };
then ex t be
VECTOR of X, s be
VECTOR of Y st x
=
||.(u
. (t,s)).|| &
||.t.||
<= 1 &
||.s.||
<= 1;
hence x
in
REAL ;
end;
hence x
in {
||.(u
. (t,s)).|| where t be
VECTOR of X, s be
VECTOR of Y :
||.t.||
<= 1 &
||.s.||
<= 1 } implies x
in
REAL ;
end;
||.(
0. X).||
=
0 &
||.(
0. Y).||
=
0 ;
then
||.(u
. ((
0. X),(
0. Y))).||
in {
||.(u
. (t,s)).|| where t be
VECTOR of X, s be
VECTOR of Y :
||.t.||
<= 1 &
||.s.||
<= 1 };
hence thesis by
A1,
TARSKI:def 3;
end;
end
registration
let X,Y,Z be
RealNormSpace;
let g be
Lipschitzian
BilinearOperator of X, Y, Z;
cluster (
PreNorms g) ->
bounded_above;
coherence
proof
consider K be
Real such that
A1:
0
<= K and
A2: for x be
VECTOR of X, y be
VECTOR of Y holds
||.(g
. (x,y)).||
<= ((K
*
||.x.||)
*
||.y.||) by
Def8;
take K;
let r be
ExtReal;
assume r
in (
PreNorms g);
then
consider t be
VECTOR of X, s be
VECTOR of Y such that
A3: r
=
||.(g
. (t,s)).|| and
A4:
||.t.||
<= 1 &
||.s.||
<= 1;
A5:
||.(g
. (t,s)).||
<= ((K
*
||.t.||)
*
||.s.||) by
A2;
(
||.t.||
*
||.s.||)
<= (1
* 1) by
XREAL_1: 66,
A4;
then (K
* (
||.t.||
*
||.s.||))
<= (K
* 1) by
A1,
XREAL_1: 64;
hence r
<= K by
A3,
A5,
XXREAL_0: 2;
end;
end
theorem ::
LOPBAN_9:13
for X,Y,Z be
RealNormSpace holds for g be
BilinearOperator of X, Y, Z holds g is
Lipschitzian iff (
PreNorms g) is
bounded_above
proof
let X,Y,Z be
RealNormSpace;
let g be
BilinearOperator of X, Y, Z;
now
reconsider K = (
upper_bound (
PreNorms g)) as
Real;
assume
A1: (
PreNorms g) is
bounded_above;
A2:
now
let t be
VECTOR of X, s be
VECTOR of Y;
now
per cases ;
case
A3: t
= (
0. X) or s
= (
0. Y);
then
A4:
||.t.||
=
0 or
||.s.||
=
0 ;
t
= (
0
* t) or s
= (
0
* s) by
A3;
then (g
. (t,s))
= (
0
* (g
. (t,s))) by
LOPBAN_8: 12
.= (
0. Z) by
RLVECT_1: 10;
hence
||.(g
. (t,s)).||
<= ((K
*
||.t.||)
*
||.s.||) by
A4;
end;
case
A5: t
<> (
0. X) & s
<> (
0. Y);
reconsider t1 = ((
||.t.||
" )
* t) as
VECTOR of X;
reconsider s1 = ((
||.s.||
" )
* s) as
VECTOR of Y;
A6:
||.t.||
<>
0 &
||.s.||
<>
0 by
A5,
NORMSP_0:def 5;
then
A7: (
||.t.||
*
||.s.||)
<>
0 by
XCMPLX_1: 6;
A8: ((
||.(g
. (t,s)).||
/ (
||.t.||
*
||.s.||))
* (
||.t.||
*
||.s.||))
= ((
||.(g
. (t,s)).||
* ((
||.t.||
*
||.s.||)
" ))
* (
||.t.||
*
||.s.||)) by
XCMPLX_0:def 9
.= (
||.(g
. (t,s)).||
* (((
||.t.||
*
||.s.||)
" )
* (
||.t.||
*
||.s.||)))
.= (
||.(g
. (t,s)).||
* 1) by
A7,
XCMPLX_0:def 7
.=
||.(g
. (t,s)).||;
A9:
|.(
||.t.||
" ).|
=
|.(1
* (
||.t.||
" )).|
.=
|.(1
/
||.t.||).| by
XCMPLX_0:def 9
.= (1
/
||.t.||) by
ABSVALUE:def 1
.= (1
* (
||.t.||
" )) by
XCMPLX_0:def 9
.= (
||.t.||
" );
A10:
|.(
||.s.||
" ).|
=
|.(1
* (
||.s.||
" )).|
.=
|.(1
/
||.s.||).| by
XCMPLX_0:def 9
.= (1
/
||.s.||) by
ABSVALUE:def 1
.= (1
* (
||.s.||
" )) by
XCMPLX_0:def 9
.= (
||.s.||
" );
A11:
|.((
||.t.||
*
||.s.||)
" ).|
=
|.((
||.t.||
" )
* (
||.s.||
" )).| by
XCMPLX_1: 204
.= ((
||.t.||
" )
* (
||.s.||
" )) by
A9,
A10,
COMPLEX1: 65
.= ((
||.t.||
*
||.s.||)
" ) by
XCMPLX_1: 204;
A12:
||.t1.||
= (
|.(
||.t.||
" ).|
*
||.t.||) by
NORMSP_1:def 1
.= 1 by
A6,
A9,
XCMPLX_0:def 7;
||.s1.||
= (
|.(
||.s.||
" ).|
*
||.s.||) by
NORMSP_1:def 1
.= 1 by
A6,
A10,
XCMPLX_0:def 7;
then
A13:
||.(g
. (t1,s1)).||
in {
||.(g
. (t,s)).|| where t be
VECTOR of X, s be
VECTOR of Y :
||.t.||
<= 1 &
||.s.||
<= 1 } by
A12;
(
||.(g
. (t,s)).||
/ (
||.t.||
*
||.s.||))
= (
||.(g
. (t,s)).||
* ((
||.t.||
*
||.s.||)
" )) by
XCMPLX_0:def 9
.=
||.(((
||.t.||
*
||.s.||)
" )
* (g
. (t,s))).|| by
A11,
NORMSP_1:def 1
.=
||.(((
||.t.||
" )
* (
||.s.||
" ))
* (g
. (t,s))).|| by
XCMPLX_1: 204
.=
||.((
||.t.||
" )
* ((
||.s.||
" )
* (g
. (t,s)))).|| by
RLVECT_1:def 7
.=
||.((
||.t.||
" )
* (g
. (t,s1))).|| by
LOPBAN_8: 12
.=
||.(g
. (t1,s1)).|| by
LOPBAN_8: 12;
then (
||.(g
. (t,s)).||
/ (
||.t.||
*
||.s.||))
<= K by
A1,
A13,
SEQ_4:def 1;
hence
||.(g
. (t,s)).||
<= (K
* (
||.t.||
*
||.s.||)) by
A8,
XREAL_1: 64;
end;
end;
hence
||.(g
. (t,s)).||
<= ((K
*
||.t.||)
*
||.s.||);
end;
take K;
0
<= K
proof
consider r0 be
object such that
A14: r0
in (
PreNorms g) by
XBOOLE_0:def 1;
reconsider r0 as
Real by
A14;
now
let r be
Real;
assume r
in (
PreNorms g);
then ex t be
VECTOR of X, s be
VECTOR of Y st r
=
||.(g
. (t,s)).|| &
||.t.||
<= 1 &
||.s.||
<= 1;
hence
0
<= r;
end;
then
0
<= r0 by
A14;
hence thesis by
A1,
A14,
SEQ_4:def 1;
end;
hence g is
Lipschitzian by
A2;
end;
hence thesis;
end;
definition
let X,Y,Z be
RealNormSpace;
::
LOPBAN_9:def8
func
BoundedBilinearOperatorsNorm (X,Y,Z) ->
Function of (
BoundedBilinearOperators (X,Y,Z)),
REAL means
:
Def13: for x be
object st x
in (
BoundedBilinearOperators (X,Y,Z)) holds (it
. x)
= (
upper_bound (
PreNorms (
modetrans (x,X,Y,Z))));
existence
proof
deffunc
F(
object) = (
upper_bound (
PreNorms (
modetrans ($1,X,Y,Z))));
A1: for z be
object st z
in (
BoundedBilinearOperators (X,Y,Z)) holds
F(z)
in
REAL by
XREAL_0:def 1;
thus ex f be
Function of (
BoundedBilinearOperators (X,Y,Z)),
REAL st for x be
object st x
in (
BoundedBilinearOperators (X,Y,Z)) holds (f
. x)
=
F(x) from
FUNCT_2:sch 2(
A1);
end;
uniqueness
proof
let NORM1,NORM2 be
Function of (
BoundedBilinearOperators (X,Y,Z)),
REAL such that
A2: for x be
object st x
in (
BoundedBilinearOperators (X,Y,Z)) holds (NORM1
. x)
= (
upper_bound (
PreNorms (
modetrans (x,X,Y,Z)))) and
A3: for x be
object st x
in (
BoundedBilinearOperators (X,Y,Z)) holds (NORM2
. x)
= (
upper_bound (
PreNorms (
modetrans (x,X,Y,Z))));
A4: for z be
object st z
in (
BoundedBilinearOperators (X,Y,Z)) holds (NORM1
. z)
= (NORM2
. z)
proof
let z be
object such that
A5: z
in (
BoundedBilinearOperators (X,Y,Z));
(NORM1
. z)
= (
upper_bound (
PreNorms (
modetrans (z,X,Y,Z)))) by
A2,
A5;
hence thesis by
A3,
A5;
end;
(
dom NORM1)
= (
BoundedBilinearOperators (X,Y,Z)) by
FUNCT_2:def 1;
hence thesis by
A4,
FUNCT_2:def 1;
end;
end
Th29: for X,Y,Z be
RealNormSpace holds for f be
Lipschitzian
BilinearOperator of X, Y, Z holds (
modetrans (f,X,Y,Z))
= f
proof
let X,Y,Z be
RealNormSpace;
let f be
Lipschitzian
BilinearOperator of X, Y, Z;
f
in (
BoundedBilinearOperators (X,Y,Z)) by
Def9;
hence thesis by
Def11;
end;
registration
let X,Y,Z be
RealNormSpace;
let f be
Lipschitzian
BilinearOperator of X, Y, Z;
reduce (
modetrans (f,X,Y,Z)) to f;
reducibility by
Th29;
end
theorem ::
LOPBAN_9:14
Th30: for X,Y,Z be
RealNormSpace holds for f be
Lipschitzian
BilinearOperator of X, Y, Z holds ((
BoundedBilinearOperatorsNorm (X,Y,Z))
. f)
= (
upper_bound (
PreNorms f))
proof
let X,Y,Z be
RealNormSpace;
let f be
Lipschitzian
BilinearOperator of X, Y, Z;
reconsider f9 = f as
set;
f
in (
BoundedBilinearOperators (X,Y,Z)) by
Def9;
hence ((
BoundedBilinearOperatorsNorm (X,Y,Z))
. f)
= (
upper_bound (
PreNorms (
modetrans (f9,X,Y,Z)))) by
Def13
.= (
upper_bound (
PreNorms f));
end;
definition
let X,Y,Z be
RealNormSpace;
::
LOPBAN_9:def9
func
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) -> non
empty
NORMSTR equals
NORMSTR (# (
BoundedBilinearOperators (X,Y,Z)), (
Zero_ ((
BoundedBilinearOperators (X,Y,Z)),(
R_VectorSpace_of_BilinearOperators (X,Y,Z)))), (
Add_ ((
BoundedBilinearOperators (X,Y,Z)),(
R_VectorSpace_of_BilinearOperators (X,Y,Z)))), (
Mult_ ((
BoundedBilinearOperators (X,Y,Z)),(
R_VectorSpace_of_BilinearOperators (X,Y,Z)))), (
BoundedBilinearOperatorsNorm (X,Y,Z)) #);
coherence ;
end
theorem ::
LOPBAN_9:15
Th31: for X,Y,Z be
RealNormSpace holds (the
carrier of
[:X, Y:]
--> (
0. Z))
= (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)))
proof
let X,Y,Z be
RealNormSpace;
(the
carrier of
[:X, Y:]
--> (
0. Z))
= (
0. (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z))) by
Th26
.= (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)));
hence thesis;
end;
theorem ::
LOPBAN_9:16
Th32: for X,Y,Z be
RealNormSpace holds for f be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds for g be
Lipschitzian
BilinearOperator of X, Y, Z st g
= f holds for t be
VECTOR of X, s be
VECTOR of Y holds
||.(g
. (t,s)).||
<= ((
||.f.||
*
||.t.||)
*
||.s.||)
proof
let X,Y,Z be
RealNormSpace;
let f be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
let g be
Lipschitzian
BilinearOperator of X, Y, Z such that
A1: g
= f;
now
let t be
VECTOR of X, s be
VECTOR of Y;
now
per cases ;
case
A3: t
= (
0. X) or s
= (
0. Y);
then
A4:
||.t.||
=
0 or
||.s.||
=
0 ;
t
= (
0
* t) or s
= (
0
* s) by
A3;
then (g
. (t,s))
= (
0
* (g
. (t,s))) by
LOPBAN_8: 12
.= (
0. Z) by
RLVECT_1: 10;
hence
||.(g
. (t,s)).||
<= ((
||.f.||
*
||.t.||)
*
||.s.||) by
A4;
end;
case
A5: t
<> (
0. X) & s
<> (
0. Y);
reconsider t1 = ((
||.t.||
" )
* t) as
VECTOR of X;
reconsider s1 = ((
||.s.||
" )
* s) as
VECTOR of Y;
A6:
||.t.||
<>
0 &
||.s.||
<>
0 by
A5,
NORMSP_0:def 5;
then
A7: (
||.t.||
*
||.s.||)
<>
0 by
XCMPLX_1: 6;
A8:
|.(
||.t.||
" ).|
=
|.(1
* (
||.t.||
" )).|
.=
|.(1
/
||.t.||).| by
XCMPLX_0:def 9
.= (1
/
||.t.||) by
ABSVALUE:def 1
.= (1
* (
||.t.||
" )) by
XCMPLX_0:def 9
.= (
||.t.||
" );
A9:
|.(
||.s.||
" ).|
=
|.(1
* (
||.s.||
" )).|
.=
|.(1
/
||.s.||).| by
XCMPLX_0:def 9
.= (1
/
||.s.||) by
ABSVALUE:def 1
.= (1
* (
||.s.||
" )) by
XCMPLX_0:def 9
.= (
||.s.||
" );
A10:
|.((
||.t.||
*
||.s.||)
" ).|
=
|.((
||.t.||
" )
* (
||.s.||
" )).| by
XCMPLX_1: 204
.= ((
||.t.||
" )
* (
||.s.||
" )) by
A8,
A9,
COMPLEX1: 65
.= ((
||.t.||
*
||.s.||)
" ) by
XCMPLX_1: 204;
A11:
||.t1.||
= (
|.(
||.t.||
" ).|
*
||.t.||) by
NORMSP_1:def 1
.= 1 by
A6,
A8,
XCMPLX_0:def 7;
A12:
||.s1.||
= (
|.(
||.s.||
" ).|
*
||.s.||) by
NORMSP_1:def 1
.= 1 by
A6,
A9,
XCMPLX_0:def 7;
(
||.(g
. (t,s)).||
/ (
||.t.||
*
||.s.||))
= (
||.(g
. (t,s)).||
* ((
||.t.||
*
||.s.||)
" )) by
XCMPLX_0:def 9
.=
||.(((
||.t.||
*
||.s.||)
" )
* (g
. (t,s))).|| by
A10,
NORMSP_1:def 1
.=
||.(((
||.t.||
" )
* (
||.s.||
" ))
* (g
. (t,s))).|| by
XCMPLX_1: 204
.=
||.((
||.t.||
" )
* ((
||.s.||
" )
* (g
. (t,s)))).|| by
RLVECT_1:def 7
.=
||.((
||.t.||
" )
* (g
. (t,s1))).|| by
LOPBAN_8: 12
.=
||.(g
. (t1,s1)).|| by
LOPBAN_8: 12;
then (
||.(g
. (t,s)).||
/ (
||.t.||
*
||.s.||))
in {
||.(g
. (t,s)).|| where t be
VECTOR of X, s be
VECTOR of Y :
||.t.||
<= 1 &
||.s.||
<= 1 } by
A11,
A12;
then (
||.(g
. (t,s)).||
/ (
||.t.||
*
||.s.||))
<= (
upper_bound (
PreNorms g)) by
SEQ_4:def 1;
then
A13: (
||.(g
. (t,s)).||
/ (
||.t.||
*
||.s.||))
<=
||.f.|| by
A1,
Th30;
((
||.(g
. (t,s)).||
/ (
||.t.||
*
||.s.||))
* (
||.t.||
*
||.s.||))
= ((
||.(g
. (t,s)).||
* ((
||.t.||
*
||.s.||)
" ))
* (
||.t.||
*
||.s.||)) by
XCMPLX_0:def 9
.= (
||.(g
. (t,s)).||
* (((
||.t.||
*
||.s.||)
" )
* (
||.t.||
*
||.s.||)))
.= (
||.(g
. (t,s)).||
* 1) by
A7,
XCMPLX_0:def 7
.=
||.(g
. (t,s)).||;
hence
||.(g
. (t,s)).||
<= (
||.f.||
* (
||.t.||
*
||.s.||)) by
A13,
XREAL_1: 64;
end;
end;
hence
||.(g
. (t,s)).||
<= ((
||.f.||
*
||.t.||)
*
||.s.||);
end;
hence thesis;
end;
theorem ::
LOPBAN_9:17
Th33: for X,Y,Z be
RealNormSpace holds for f be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds
0
<=
||.f.||
proof
let X,Y,Z be
RealNormSpace;
let f be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
reconsider g = f as
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
consider r0 be
object such that
A1: r0
in (
PreNorms g) by
XBOOLE_0:def 1;
reconsider r0 as
Real by
A1;
A3: ((
BoundedBilinearOperatorsNorm (X,Y,Z))
. f)
= (
upper_bound (
PreNorms g)) by
Th30;
now
let r be
Real;
assume r
in (
PreNorms g);
then ex t be
VECTOR of X, s be
VECTOR of Y st r
=
||.(g
. (t,s)).|| &
||.t.||
<= 1 &
||.s.||
<= 1;
hence
0
<= r;
end;
then
0
<= r0 by
A1;
hence thesis by
A1,
A3,
SEQ_4:def 1;
end;
theorem ::
LOPBAN_9:18
Th34: for X,Y,Z be
RealNormSpace holds for f be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st f
= (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))) holds
0
=
||.f.||
proof
let X,Y,Z be
RealNormSpace;
let f be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) such that
A1: f
= (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)));
reconsider g = f as
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
set z = (the
carrier of
[:X, Y:]
--> (
0. Z));
reconsider z as
Function of the
carrier of
[:X, Y:], the
carrier of Z;
consider r0 be
object such that
A2: r0
in (
PreNorms g) by
XBOOLE_0:def 1;
reconsider r0 as
Real by
A2;
A3: (for s be
Real st s
in (
PreNorms g) holds s
<=
0 ) implies (
upper_bound (
PreNorms g))
<=
0 by
SEQ_4: 45;
A5: z
= g by
A1,
Th31;
A6:
now
let r be
Real;
assume r
in (
PreNorms g);
then
consider t be
VECTOR of X, s be
VECTOR of Y such that
A7: r
=
||.(g
. (t,s)).|| and
||.t.||
<= 1 &
||.s.||
<= 1;
[t, s] is
Point of
[:X, Y:] by
LMELM2;
then (g
. (t,s))
= (
0. Z) by
FUNCOP_1: 7,
A5;
hence
0
<= r & r
<=
0 by
A7;
end;
then
0
<= r0 by
A2;
then (
upper_bound (
PreNorms g))
=
0 by
A6,
A2,
A3,
SEQ_4:def 1;
hence thesis by
Th30;
end;
registration
let X,Y,Z be
RealNormSpace;
cluster ->
Function-like
Relation-like for
Element of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
coherence ;
end
definition
let X,Y,Z be
RealNormSpace;
let f be
Element of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
let v be
VECTOR of X, w be
VECTOR of Y;
:: original:
.
redefine
func f
. (v,w) ->
VECTOR of Z ;
coherence
proof
reconsider f as
BilinearOperator of X, Y, Z by
Def9;
(f
. (v,w)) is
VECTOR of Z;
hence thesis;
end;
end
theorem ::
LOPBAN_9:19
Th35: for X,Y,Z be
RealNormSpace holds for f,g,h be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds h
= (f
+ g) iff for x be
VECTOR of X, y be
VECTOR of Y holds (h
. (x,y))
= ((f
. (x,y))
+ (g
. (x,y)))
proof
let X,Y,Z be
RealNormSpace;
let f,g,h be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
reconsider f1 = f, g1 = g, h1 = h as
VECTOR of (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z));
h
= (f
+ g) iff h1
= (f1
+ g1);
hence thesis by
Th24;
end;
theorem ::
LOPBAN_9:20
Th36: for X,Y,Z be
RealNormSpace holds for f,h be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds for a be
Real holds h
= (a
* f) iff for x be
VECTOR of X, y be
VECTOR of Y holds (h
. (x,y))
= (a
* (f
. (x,y)))
proof
let X,Y,Z be
RealNormSpace;
let f,h be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
let a be
Real;
reconsider f1 = f as
VECTOR of (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z));
reconsider h1 = h as
VECTOR of (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z));
h
= (a
* f) iff h1
= (a
* f1);
hence thesis by
Th25;
end;
theorem ::
LOPBAN_9:21
Th37: for X,Y,Z be
RealNormSpace holds for f,g be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds for a be
Real holds (
||.f.||
=
0 iff f
= (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)))) &
||.(a
* f).||
= (
|.a.|
*
||.f.||) &
||.(f
+ g).||
<= (
||.f.||
+
||.g.||)
proof
let X,Y,Z be
RealNormSpace;
let f,g be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
let a be
Real;
A1:
now
assume
A2: f
= (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)));
thus
||.f.||
=
0
proof
reconsider g = f as
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
set z = (the
carrier of
[:X, Y:]
--> (
0. Z));
reconsider z as
Function of the
carrier of
[:X, Y:], the
carrier of Z;
consider r0 be
object such that
A3: r0
in (
PreNorms g) by
XBOOLE_0:def 1;
reconsider r0 as
Real by
A3;
A4: (for s be
Real st s
in (
PreNorms g) holds s
<=
0 ) implies (
upper_bound (
PreNorms g))
<=
0 by
SEQ_4: 45;
A6: z
= g by
A2,
Th31;
A7:
now
let r be
Real;
assume r
in (
PreNorms g);
then
consider t be
VECTOR of X, s be
VECTOR of Y such that
A8: r
=
||.(g
. (t,s)).|| and
||.t.||
<= 1 &
||.s.||
<= 1;
[t, s] is
Point of
[:X, Y:] by
LMELM2;
then (g
. (t,s))
= (
0. Z) by
A6,
FUNCOP_1: 7;
hence
0
<= r & r
<=
0 by
A8;
end;
then
0
<= r0 by
A3;
then (
upper_bound (
PreNorms g))
=
0 by
A3,
A4,
A7,
SEQ_4:def 1;
hence thesis by
Th30;
end;
end;
A9:
||.(f
+ g).||
<= (
||.f.||
+
||.g.||)
proof
reconsider f1 = f, g1 = g, h1 = (f
+ g) as
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
A10: (for s be
Real st s
in (
PreNorms h1) holds s
<= (
||.f.||
+
||.g.||)) implies (
upper_bound (
PreNorms h1))
<= (
||.f.||
+
||.g.||) by
SEQ_4: 45;
A11:
now
let t be
VECTOR of X, s be
VECTOR of Y such that
A12:
||.t.||
<= 1 &
||.s.||
<= 1;
A13: (
||.t.||
*
||.s.||)
<= (1
* 1) by
A12,
XREAL_1: 66;
0
<=
||.g.|| by
Th33;
then
A14: (
||.g.||
* (
||.t.||
*
||.s.||))
<= (
||.g.||
* 1) by
A13,
XREAL_1: 64;
0
<=
||.f.|| by
Th33;
then (
||.f.||
* (
||.t.||
*
||.s.||))
<= (
||.f.||
* 1) by
A13,
XREAL_1: 64;
then
A15: (((
||.f.||
*
||.t.||)
*
||.s.||)
+ ((
||.g.||
*
||.t.||)
*
||.s.||))
<= ((
||.f.||
* 1)
+ (
||.g.||
* 1)) by
A14,
XREAL_1: 7;
A16:
||.((f1
. (t,s))
+ (g1
. (t,s))).||
<= (
||.(f1
. (t,s)).||
+
||.(g1
. (t,s)).||) by
NORMSP_1:def 1;
A17:
||.(g1
. (t,s)).||
<= ((
||.g.||
*
||.t.||)
*
||.s.||) by
Th32;
||.(f1
. (t,s)).||
<= ((
||.f.||
*
||.t.||)
*
||.s.||) by
Th32;
then (
||.(f1
. (t,s)).||
+
||.(g1
. (t,s)).||)
<= (((
||.f.||
*
||.t.||)
*
||.s.||)
+ ((
||.g.||
*
||.t.||)
*
||.s.||)) by
A17,
XREAL_1: 7;
then
A18: (
||.(f1
. (t,s)).||
+
||.(g1
. (t,s)).||)
<= (
||.f.||
+
||.g.||) by
A15,
XXREAL_0: 2;
||.(h1
. (t,s)).||
=
||.((f1
. (t,s))
+ (g1
. (t,s))).|| by
Th35;
hence
||.(h1
. (t,s)).||
<= (
||.f.||
+
||.g.||) by
A16,
A18,
XXREAL_0: 2;
end;
now
let r be
Real;
assume r
in (
PreNorms h1);
then ex t be
VECTOR of X, s be
VECTOR of Y st r
=
||.(h1
. (t,s)).|| &
||.t.||
<= 1 &
||.s.||
<= 1;
hence r
<= (
||.f.||
+
||.g.||) by
A11;
end;
hence thesis by
A10,
Th30;
end;
A20:
||.(a
* f).||
= (
|.a.|
*
||.f.||)
proof
reconsider f1 = f, h1 = (a
* f) as
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
A21: (for s be
Real st s
in (
PreNorms h1) holds s
<= (
|.a.|
*
||.f.||)) implies (
upper_bound (
PreNorms h1))
<= (
|.a.|
*
||.f.||) by
SEQ_4: 45;
A22:
now
A23:
0
<=
||.f.|| by
Th33;
let t be
VECTOR of X, s be
VECTOR of Y;
assume
||.t.||
<= 1 &
||.s.||
<= 1;
then (
||.t.||
*
||.s.||)
<= (1
* 1) by
XREAL_1: 66;
then
A24: (
||.f.||
* (
||.t.||
*
||.s.||))
<= (
||.f.||
* 1) by
A23,
XREAL_1: 64;
||.(f1
. (t,s)).||
<= ((
||.f.||
*
||.t.||)
*
||.s.||) by
Th32;
then
A25:
||.(f1
. (t,s)).||
<=
||.f.|| by
A24,
XXREAL_0: 2;
A26:
||.(a
* (f1
. (t,s))).||
= (
|.a.|
*
||.(f1
. (t,s)).||) by
NORMSP_1:def 1;
A27:
0
<=
|.a.| by
COMPLEX1: 46;
||.(h1
. (t,s)).||
=
||.(a
* (f1
. (t,s))).|| by
Th36;
hence
||.(h1
. (t,s)).||
<= (
|.a.|
*
||.f.||) by
A25,
A26,
A27,
XREAL_1: 64;
end;
A28:
now
let r be
Real;
assume r
in (
PreNorms h1);
then ex t be
VECTOR of X, s be
VECTOR of Y st r
=
||.(h1
. (t,s)).|| &
||.t.||
<= 1 &
||.s.||
<= 1;
hence r
<= (
|.a.|
*
||.f.||) by
A22;
end;
A29:
now
per cases ;
case
A30: a
<>
0 ;
A31:
now
A32:
0
<=
||.(a
* f).|| by
Th33;
let t be
VECTOR of X, s be
VECTOR of Y;
assume
||.t.||
<= 1 &
||.s.||
<= 1;
then (
||.t.||
*
||.s.||)
<= (1
* 1) by
XREAL_1: 66;
then
A33: (
||.(a
* f).||
* (
||.t.||
*
||.s.||))
<= (
||.(a
* f).||
* 1) by
A32,
XREAL_1: 64;
||.(h1
. (t,s)).||
<= ((
||.(a
* f).||
*
||.t.||)
*
||.s.||) by
Th32;
then
A34:
||.(h1
. (t,s)).||
<=
||.(a
* f).|| by
A33,
XXREAL_0: 2;
(h1
. (t,s))
= (a
* (f1
. (t,s))) by
Th36;
then
A35: ((a
" )
* (h1
. (t,s)))
= (((a
" )
* a)
* (f1
. (t,s))) by
RLVECT_1:def 7
.= (1
* (f1
. (t,s))) by
A30,
XCMPLX_0:def 7
.= (f1
. (t,s)) by
RLVECT_1:def 8;
A36:
|.(a
" ).|
=
|.(1
* (a
" )).|
.=
|.(1
/ a).| by
XCMPLX_0:def 9
.= (1
/
|.a.|) by
ABSVALUE: 7
.= (1
* (
|.a.|
" )) by
XCMPLX_0:def 9
.= (
|.a.|
" );
A37:
0
<=
|.(a
" ).| by
COMPLEX1: 46;
||.((a
" )
* (h1
. (t,s))).||
= (
|.(a
" ).|
*
||.(h1
. (t,s)).||) by
NORMSP_1:def 1;
hence
||.(f1
. (t,s)).||
<= ((
|.a.|
" )
*
||.(a
* f).||) by
A34,
A35,
A36,
A37,
XREAL_1: 64;
end;
A38:
now
let r be
Real;
assume r
in (
PreNorms f1);
then ex t be
VECTOR of X, s be
VECTOR of Y st r
=
||.(f1
. (t,s)).|| &
||.t.||
<= 1 &
||.s.||
<= 1;
hence r
<= ((
|.a.|
" )
*
||.(a
* f).||) by
A31;
end;
A39: (for s be
Real st s
in (
PreNorms f1) holds s
<= ((
|.a.|
" )
*
||.(a
* f).||)) implies (
upper_bound (
PreNorms f1))
<= ((
|.a.|
" )
*
||.(a
* f).||) by
SEQ_4: 45;
A40:
0
<=
|.a.| by
COMPLEX1: 46;
||.f.||
<= ((
|.a.|
" )
*
||.(a
* f).||) by
A38,
A39,
Th30;
then (
|.a.|
*
||.f.||)
<= (
|.a.|
* ((
|.a.|
" )
*
||.(a
* f).||)) by
A40,
XREAL_1: 64;
then
A41: (
|.a.|
*
||.f.||)
<= ((
|.a.|
* (
|.a.|
" ))
*
||.(a
* f).||);
|.a.|
<>
0 by
A30,
COMPLEX1: 47;
then (
|.a.|
*
||.f.||)
<= (1
*
||.(a
* f).||) by
A41,
XCMPLX_0:def 7;
hence (
|.a.|
*
||.f.||)
<=
||.(a
* f).||;
end;
case
A42: a
=
0 ;
reconsider fz = f as
VECTOR of (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z));
A43: (a
* f)
= (a
* fz)
.= (
0. (
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z))) by
A42,
RLVECT_1: 10
.= (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)));
thus (
|.a.|
*
||.f.||)
= (
0
*
||.f.||) by
A42,
ABSVALUE: 2
.=
||.(a
* f).|| by
A43,
Th34;
end;
end;
||.(a
* f).||
<= (
|.a.|
*
||.f.||) by
A21,
A28,
Th30;
hence thesis by
A29,
XXREAL_0: 1;
end;
now
reconsider g = f as
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
set z = (the
carrier of
[:X, Y:]
--> (
0. Z));
reconsider z as
Function of the
carrier of
[:X, Y:], the
carrier of Z;
assume
A44:
||.f.||
=
0 ;
now
let t be
VECTOR of X, s be
VECTOR of Y;
A45:
[t, s] is
Point of
[:X, Y:] by
LMELM2;
||.(g
. (t,s)).||
<= ((
||.f.||
*
||.t.||)
*
||.s.||) by
Th32;
then
||.(g
. (t,s)).||
=
0 by
A44;
hence (g
. (t,s))
= (
0. Z) by
NORMSP_0:def 5
.= (z
. (t,s)) by
A45,
FUNCOP_1: 7;
end;
then g
= z by
BINOP_1: 2;
hence f
= (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))) by
Th31;
end;
hence thesis by
A1,
A9,
A20;
end;
Th38: for X,Y,Z be
RealNormSpace holds (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) is
reflexive
discerning
RealNormSpace-like
proof
let X,Y,Z be
RealNormSpace;
thus
||.(
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))).||
=
0 by
Th37;
for x,y be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds for a be
Real holds (
||.x.||
=
0 iff x
= (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)))) &
||.(a
* x).||
= (
|.a.|
*
||.x.||) &
||.(x
+ y).||
<= (
||.x.||
+
||.y.||) by
Th37;
hence thesis by
NORMSP_1:def 1,
NORMSP_0:def 5;
end;
registration
let X,Y,Z be
RealNormSpace;
cluster (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) -> non
empty;
coherence ;
end
registration
let X,Y,Z be
RealNormSpace;
cluster (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ->
reflexive
discerning
RealNormSpace-like;
coherence by
Th38;
end
theorem ::
LOPBAN_9:22
Th39: for X,Y,Z be
RealNormSpace holds (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) is
RealNormSpace
proof
let X,Y,Z be
RealNormSpace;
(
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) is
RealLinearSpace;
hence thesis by
RSSPACE3: 2;
end;
registration
let X,Y,Z be
RealNormSpace;
cluster (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ->
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
Abelian
add-associative
right_zeroed
right_complementable;
coherence by
Th39;
end
theorem ::
LOPBAN_9:23
Th40: for X,Y,Z be
RealNormSpace holds for f,g,h be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds h
= (f
- g) iff for x be
VECTOR of X, y be
VECTOR of Y holds (h
. (x,y))
= ((f
. (x,y))
- (g
. (x,y)))
proof
let X,Y,Z be
RealNormSpace;
let f,g,h be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
reconsider f9 = f, g9 = g, h9 = h as
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
hereby
assume h
= (f
- g);
then (h
+ g)
= (f
- (g
- g)) by
RLVECT_1: 29;
then
A1: (h
+ g)
= (f
- (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)))) by
RLVECT_1: 15;
now
let x be
VECTOR of X, y be
VECTOR of Y;
(f9
. (x,y))
= ((h9
. (x,y))
+ (g9
. (x,y))) by
A1,
Th35;
then ((f9
. (x,y))
- (g9
. (x,y)))
= ((h9
. (x,y))
+ ((g9
. (x,y))
- (g9
. (x,y)))) by
RLVECT_1:def 3;
then ((f9
. (x,y))
- (g9
. (x,y)))
= ((h9
. (x,y))
+ (
0. Z)) by
RLVECT_1: 15;
hence ((f9
. (x,y))
- (g9
. (x,y)))
= (h9
. (x,y));
end;
hence for x be
VECTOR of X, y be
VECTOR of Y holds (h
. (x,y))
= ((f
. (x,y))
- (g
. (x,y)));
end;
assume
A2: for x be
VECTOR of X, y be
VECTOR of Y holds (h
. (x,y))
= ((f
. (x,y))
- (g
. (x,y)));
now
let x be
VECTOR of X, y be
VECTOR of Y;
(h9
. (x,y))
= ((f9
. (x,y))
- (g9
. (x,y))) by
A2;
then ((h9
. (x,y))
+ (g9
. (x,y)))
= ((f9
. (x,y))
- ((g9
. (x,y))
- (g9
. (x,y)))) by
RLVECT_1: 29;
then ((h9
. (x,y))
+ (g9
. (x,y)))
= ((f9
. (x,y))
- (
0. Z)) by
RLVECT_1: 15;
hence ((h9
. (x,y))
+ (g9
. (x,y)))
= (f9
. (x,y));
end;
then f
= (h
+ g) by
Th35;
then (f
- g)
= (h
+ (g
- g)) by
RLVECT_1:def 3;
then (f
- g)
= (h
+ (
0. (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)))) by
RLVECT_1: 15;
hence thesis;
end;
begin
Lm3: for e be
Real, seq be
Real_Sequence st (seq is
convergent & ex k be
Nat st for i be
Nat st k
<= i holds (seq
. i)
<= e) holds (
lim seq)
<= e
proof
let e be
Real;
let seq be
Real_Sequence such that
A1: seq is
convergent and
A2: ex k be
Nat st for i be
Nat st k
<= i holds (seq
. i)
<= e;
consider k be
Nat such that
A3: for i be
Nat st k
<= i holds (seq
. i)
<= e by
A2;
reconsider ee = e as
Element of
REAL by
XREAL_0:def 1;
set cseq = (
seq_const e);
A4: (
lim cseq)
= (cseq
. 1) by
SEQ_4: 26
.= e by
SEQ_1: 57;
A5:
now
let i be
Nat;
A6: ((seq
^\ k)
. i)
= (seq
. (k
+ i)) by
NAT_1:def 3;
(seq
. (k
+ i))
<= e by
A3,
NAT_1: 11;
hence ((seq
^\ k)
. i)
<= (cseq
. i) by
A6,
SEQ_1: 57;
end;
(
lim (seq
^\ k))
= (
lim seq) by
A1,
SEQ_4: 20;
hence thesis by
A1,
A5,
A4,
SEQ_2: 18;
end;
theorem ::
LOPBAN_9:24
Th42: for X,Y,Z be
RealNormSpace st Z is
complete holds for seq be
sequence of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st seq is
Cauchy_sequence_by_Norm holds seq is
convergent
proof
let X,Y,Z be
RealNormSpace such that
A1: Z is
complete;
let vseq be
sequence of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) such that
A2: vseq is
Cauchy_sequence_by_Norm;
defpred
P[
set,
set] means ex xseq be
sequence of Z st (for n be
Nat holds (xseq
. n)
= ((vseq
. n)
. $1)) & xseq is
convergent & $2
= (
lim xseq);
A3: for xy be
Element of
[:X, Y:] holds ex z be
Element of Z st
P[xy, z]
proof
let xy be
Element of
[:X, Y:];
deffunc
F(
Nat) = ((
modetrans ((vseq
. $1),X,Y,Z))
. xy);
consider xseq be
sequence of Z such that
A4: for n be
Element of
NAT holds (xseq
. n)
=
F(n) from
FUNCT_2:sch 4;
A5: for n be
Nat holds (xseq
. n)
= ((vseq
. n)
. xy)
proof
let n be
Nat;
n
in
NAT by
ORDINAL1:def 12;
then
A6: (xseq
. n)
= ((
modetrans ((vseq
. n),X,Y,Z))
. xy) by
A4;
(vseq
. n) is
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
hence thesis by
A6;
end;
take (
lim xseq);
consider x be
Point of X, y be
Point of Y such that
A7: xy
=
[x, y] by
PRVECT_3: 18;
A8: for m,k be
Nat holds
||.((xseq
. m)
- (xseq
. k)).||
<= (
||.((vseq
. m)
- (vseq
. k)).||
* (
||.x.||
*
||.y.||))
proof
let m,k be
Nat;
reconsider h1 = ((vseq
. m)
- (vseq
. k)) as
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
A9: (xseq
. m)
= ((vseq
. m)
. (x,y)) by
A5,
A7;
A10: (xseq
. k)
= ((vseq
. k)
. (x,y)) by
A5,
A7;
((xseq
. m)
- (xseq
. k))
= (h1
. (x,y)) by
A9,
A10,
Th40;
then
||.((xseq
. m)
- (xseq
. k)).||
<= ((
||.((vseq
. m)
- (vseq
. k)).||
*
||.x.||)
*
||.y.||) by
Th32;
hence thesis;
end;
now
let e be
Real such that
A11: e
>
0 ;
now
per cases ;
case
A12: x
= (
0. X) or y
= (
0. Y);
reconsider k =
0 as
Nat;
take k;
thus for n,m be
Nat st n
>= k & m
>= k holds
||.((xseq
. n)
- (xseq
. m)).||
< e
proof
let n,m be
Nat such that n
>= k and m
>= k;
A13: (xseq
. m)
= ((vseq
. m)
. (x,y)) by
A5,
A7;
A14: (vseq
. m) is
Lipschitzian
BilinearOperator of X, Y, Z & (vseq
. n) is
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
A15: x
= (
0
* x) or y
= (
0
* y) by
A12;
then
A16: ((vseq
. m)
. (x,y))
= (
0
* ((vseq
. m)
. (x,y))) by
A14,
LOPBAN_8: 12
.= (
0. Z) by
RLVECT_1: 10;
A17: (xseq
. n)
= ((vseq
. n)
. (x,y)) by
A5,
A7;
((vseq
. n)
. (x,y))
= (
0
* ((vseq
. n)
. (x,y))) by
A14,
A15,
LOPBAN_8: 12
.= (
0. Z) by
RLVECT_1: 10;
hence thesis by
A11,
A13,
A16,
A17;
end;
end;
case x
<> (
0. X) & y
<> (
0. Y);
then
||.x.||
<>
0 &
||.y.||
<>
0 by
NORMSP_0:def 5;
then
||.x.||
>
0 &
||.y.||
>
0 ;
then
A18:
0
< (
||.x.||
*
||.y.||) by
XREAL_1: 129;
then
consider k be
Nat such that
A19: for n,m be
Nat st n
>= k & m
>= k holds
||.((vseq
. n)
- (vseq
. m)).||
< (e
/ (
||.x.||
*
||.y.||)) by
A2,
A11,
XREAL_1: 139,
RSSPACE3: 8;
take k;
thus for n,m be
Nat st n
>= k & m
>= k holds
||.((xseq
. n)
- (xseq
. m)).||
< e
proof
let n,m be
Nat such that
A20: n
>= k and
A21: m
>= k;
||.((vseq
. n)
- (vseq
. m)).||
< (e
/ (
||.x.||
*
||.y.||)) by
A19,
A20,
A21;
then
A22: (
||.((vseq
. n)
- (vseq
. m)).||
* (
||.x.||
*
||.y.||))
< ((e
/ (
||.x.||
*
||.y.||))
* (
||.x.||
*
||.y.||)) by
A18,
XREAL_1: 68;
A23: ((e
/ (
||.x.||
*
||.y.||))
* (
||.x.||
*
||.y.||))
= ((e
* ((
||.x.||
*
||.y.||)
" ))
* (
||.x.||
*
||.y.||)) by
XCMPLX_0:def 9
.= (e
* (((
||.x.||
*
||.y.||)
" )
* (
||.x.||
*
||.y.||)))
.= (e
* 1) by
A18,
XCMPLX_0:def 7
.= e;
||.((xseq
. n)
- (xseq
. m)).||
<= (
||.((vseq
. n)
- (vseq
. m)).||
* (
||.x.||
*
||.y.||)) by
A8;
hence thesis by
A22,
A23,
XXREAL_0: 2;
end;
end;
end;
hence ex k be
Nat st for n,m be
Nat st n
>= k & m
>= k holds
||.((xseq
. n)
- (xseq
. m)).||
< e;
end;
then xseq is
convergent by
A1,
RSSPACE3: 8;
hence thesis by
A5;
end;
consider f be
Function of the
carrier of
[:X, Y:], the
carrier of Z such that
A24: for z be
Element of
[:X, Y:] holds
P[z, (f
. z)] from
FUNCT_2:sch 3(
A3);
reconsider tseq = f as
Function of
[:X, Y:], Z;
A25: for x1,x2 be
Point of X, y be
Point of Y holds (tseq
. ((x1
+ x2),y))
= ((tseq
. (x1,y))
+ (tseq
. (x2,y)))
proof
let x1,x2 be
Point of X, y be
Point of Y;
reconsider x1y =
[x1, y] as
Point of
[:X, Y:] by
LMELM2;
reconsider x2y =
[x2, y] as
Point of
[:X, Y:] by
LMELM2;
reconsider x1x2y =
[(x1
+ x2), y] as
Point of
[:X, Y:] by
LMELM2;
consider sqx1y be
sequence of Z such that
A26: for n be
Nat holds (sqx1y
. n)
= ((vseq
. n)
. x1y) & sqx1y is
convergent & (tseq
. x1y)
= (
lim sqx1y) by
A24;
consider sqx2y be
sequence of Z such that
A27: for n be
Nat holds (sqx2y
. n)
= ((vseq
. n)
. x2y) & sqx2y is
convergent & (tseq
. x2y)
= (
lim sqx2y) by
A24;
consider sqx1x2y be
sequence of Z such that
A28: for n be
Nat holds (sqx1x2y
. n)
= ((vseq
. n)
. x1x2y) & sqx1x2y is
convergent & (tseq
. x1x2y)
= (
lim sqx1x2y) by
A24;
for n be
Nat holds (sqx1x2y
. n)
= ((sqx1y
. n)
+ (sqx2y
. n))
proof
let n be
Nat;
A29: (vseq
. n) is
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
A30: (sqx1y
. n)
= ((vseq
. n)
. (x1,y)) by
A26;
A31: (sqx2y
. n)
= ((vseq
. n)
. (x2,y)) by
A27;
thus (sqx1x2y
. n)
= ((vseq
. n)
. ((x1
+ x2),y)) by
A28
.= ((sqx1y
. n)
+ (sqx2y
. n)) by
A29,
A30,
A31,
LOPBAN_8: 12;
end;
then
A32: sqx1x2y
= (sqx1y
+ sqx2y) by
NORMSP_1:def 2;
thus (tseq
. ((x1
+ x2),y))
= ((tseq
. (x1,y))
+ (tseq
. (x2,y))) by
A26,
A27,
A28,
A32,
NORMSP_1: 25;
end;
A33: for x be
Point of X, y be
Point of Y, a be
Real holds (tseq
. ((a
* x),y))
= (a
* (tseq
. (x,y)))
proof
let x be
Point of X, y be
Point of Y, a be
Real;
reconsider xy =
[x, y] as
Point of
[:X, Y:] by
LMELM2;
reconsider axy =
[(a
* x), y] as
Point of
[:X, Y:] by
LMELM2;
consider sqxy be
sequence of Z such that
A34: for n be
Nat holds (sqxy
. n)
= ((vseq
. n)
. xy) & sqxy is
convergent & (tseq
. xy)
= (
lim sqxy) by
A24;
consider sqaxy be
sequence of Z such that
A35: for n be
Nat holds (sqaxy
. n)
= ((vseq
. n)
. axy) & sqaxy is
convergent & (tseq
. axy)
= (
lim sqaxy) by
A24;
for n be
Nat holds (sqaxy
. n)
= (a
* (sqxy
. n))
proof
let n be
Nat;
A36: (vseq
. n) is
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
(sqaxy
. n)
= ((vseq
. n)
. ((a
* x),y)) by
A35
.= (a
* ((vseq
. n)
. (x,y))) by
A36,
LOPBAN_8: 12;
hence (sqaxy
. n)
= (a
* (sqxy
. n)) by
A34;
end;
then sqaxy
= (a
* sqxy) by
NORMSP_1:def 5;
hence (tseq
. ((a
* x),y))
= (a
* (tseq
. (x,y))) by
A34,
A35,
NORMSP_1: 28;
end;
A40: for x be
Point of X, y1,y2 be
Point of Y holds (tseq
. (x,(y1
+ y2)))
= ((tseq
. (x,y1))
+ (tseq
. (x,y2)))
proof
let x be
Point of X, y1,y2 be
Point of Y;
reconsider x1y =
[x, y1] as
Point of
[:X, Y:] by
LMELM2;
reconsider x2y =
[x, y2] as
Point of
[:X, Y:] by
LMELM2;
reconsider x1x2y =
[x, (y1
+ y2)] as
Point of
[:X, Y:] by
LMELM2;
consider sqx1y be
sequence of Z such that
A41: for n be
Nat holds (sqx1y
. n)
= ((vseq
. n)
. x1y) & sqx1y is
convergent & (tseq
. x1y)
= (
lim sqx1y) by
A24;
consider sqx2y be
sequence of Z such that
A42: for n be
Nat holds (sqx2y
. n)
= ((vseq
. n)
. x2y) & sqx2y is
convergent & (tseq
. x2y)
= (
lim sqx2y) by
A24;
consider sqx1x2y be
sequence of Z such that
A43: for n be
Nat holds (sqx1x2y
. n)
= ((vseq
. n)
. x1x2y) & sqx1x2y is
convergent & (tseq
. x1x2y)
= (
lim sqx1x2y) by
A24;
for n be
Nat holds (sqx1x2y
. n)
= ((sqx1y
. n)
+ (sqx2y
. n))
proof
let n be
Nat;
A44: (vseq
. n) is
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
A45: (sqx1y
. n)
= ((vseq
. n)
. (x,y1)) by
A41;
A46: (sqx2y
. n)
= ((vseq
. n)
. (x,y2)) by
A42;
thus (sqx1x2y
. n)
= ((vseq
. n)
. (x,(y1
+ y2))) by
A43
.= ((sqx1y
. n)
+ (sqx2y
. n)) by
A44,
A45,
A46,
LOPBAN_8: 12;
end;
then sqx1x2y
= (sqx1y
+ sqx2y) by
NORMSP_1:def 2;
hence (tseq
. (x,(y1
+ y2)))
= ((tseq
. (x,y1))
+ (tseq
. (x,y2))) by
A41,
A42,
A43,
NORMSP_1: 25;
end;
for x be
Point of X, y be
Point of Y, a be
Real holds (tseq
. (x,(a
* y)))
= (a
* (tseq
. (x,y)))
proof
let x be
Point of X, y be
Point of Y, a be
Real;
reconsider xy =
[x, y] as
Point of
[:X, Y:] by
LMELM2;
reconsider axy =
[x, (a
* y)] as
Point of
[:X, Y:] by
LMELM2;
consider sqxy be
sequence of Z such that
A48: for n be
Nat holds (sqxy
. n)
= ((vseq
. n)
. xy) & sqxy is
convergent & (tseq
. xy)
= (
lim sqxy) by
A24;
consider sqaxy be
sequence of Z such that
A49: for n be
Nat holds (sqaxy
. n)
= ((vseq
. n)
. axy) & sqaxy is
convergent & (tseq
. axy)
= (
lim sqaxy) by
A24;
for n be
Nat holds (sqaxy
. n)
= (a
* (sqxy
. n))
proof
let n be
Nat;
A50: (vseq
. n) is
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
(sqaxy
. n)
= ((vseq
. n)
. (x,(a
* y))) by
A49
.= (a
* ((vseq
. n)
. (x,y))) by
A50,
LOPBAN_8: 12;
hence (sqaxy
. n)
= (a
* (sqxy
. n)) by
A48;
end;
then sqaxy
= (a
* sqxy) by
NORMSP_1:def 5;
hence (tseq
. (x,(a
* y)))
= (a
* (tseq
. (x,y))) by
A48,
A49,
NORMSP_1: 28;
end;
then
reconsider tseq as
BilinearOperator of X, Y, Z by
A25,
A33,
A40,
LOPBAN_8: 12;
B53:
now
let e1 be
Real such that
A54: e1
>
0 ;
reconsider e = e1 as
Real;
consider k be
Nat such that
A55: for n,m be
Nat st n
>= k & m
>= k holds
||.((vseq
. n)
- (vseq
. m)).||
< e by
A2,
A54,
RSSPACE3: 8;
reconsider k as
Nat;
take k;
now
let m be
Nat;
assume m
>= k;
then
A56:
||.((vseq
. m)
- (vseq
. k)).||
< e by
A55;
A57:
||.(vseq
. m).||
= (
||.vseq.||
. m) by
NORMSP_0:def 4;
A58:
||.(vseq
. k).||
= (
||.vseq.||
. k) by
NORMSP_0:def 4;
|.(
||.(vseq
. m).||
-
||.(vseq
. k).||).|
<=
||.((vseq
. m)
- (vseq
. k)).|| by
NORMSP_1: 9;
hence
|.((
||.vseq.||
. m)
- (
||.vseq.||
. k)).|
< e1 by
A56,
A57,
A58,
XXREAL_0: 2;
end;
hence for m be
Nat st m
>= k holds
|.((
||.vseq.||
. m)
- (
||.vseq.||
. k)).|
< e1;
end;
then
A59:
||.vseq.|| is
convergent by
SEQ_4: 41;
A60: tseq is
Lipschitzian
proof
take (
lim
||.vseq.||);
A61:
now
let x be
Point of X, y be
Point of Y;
[x, y] is
set by
TARSKI: 1;
then
reconsider xy =
[x, y] as
Point of
[:X, Y:] by
PRVECT_3: 18;
consider xyseq be
sequence of Z such that
A62: for n be
Nat holds (xyseq
. n)
= ((vseq
. n)
. xy) and
A63: xyseq is
convergent and
A64: (tseq
. xy)
= (
lim xyseq) by
A24;
A65:
||.(tseq
. xy).||
= (
lim
||.xyseq.||) by
A63,
A64,
LOPBAN_1: 20;
A66: for m be
Nat holds
||.(xyseq
. m).||
<= (
||.(vseq
. m).||
* (
||.x.||
*
||.y.||))
proof
let m be
Nat;
(vseq
. m) is
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
then
||.((vseq
. m)
. (x,y)).||
<= ((
||.(vseq
. m).||
*
||.x.||)
*
||.y.||) by
Th32;
hence
||.(xyseq
. m).||
<= (
||.(vseq
. m).||
* (
||.x.||
*
||.y.||)) by
A62;
end;
A68: for n be
Nat holds (
||.xyseq.||
. n)
<= (((
||.x.||
*
||.y.||)
(#)
||.vseq.||)
. n)
proof
let n be
Nat;
A69: (
||.xyseq.||
. n)
=
||.(xyseq
. n).|| by
NORMSP_0:def 4;
A70:
||.(vseq
. n).||
= (
||.vseq.||
. n) by
NORMSP_0:def 4;
||.(xyseq
. n).||
<= (
||.(vseq
. n).||
* (
||.x.||
*
||.y.||)) by
A66;
hence thesis by
A69,
A70,
SEQ_1: 9;
end;
A72: (
lim ((
||.x.||
*
||.y.||)
(#)
||.vseq.||))
= ((
lim
||.vseq.||)
* (
||.x.||
*
||.y.||)) by
B53,
SEQ_2: 8,
SEQ_4: 41;
||.xyseq.|| is
convergent by
A63,
A64,
LOPBAN_1: 20;
hence
||.(tseq
. (x,y)).||
<= (((
lim
||.vseq.||)
*
||.x.||)
*
||.y.||) by
A59,
A65,
A68,
A72,
SEQ_2: 18;
end;
now
let n be
Nat;
||.(vseq
. n).||
>=
0 ;
hence (
||.vseq.||
. n)
>=
0 by
NORMSP_0:def 4;
end;
hence thesis by
B53,
A61,
SEQ_2: 17,
SEQ_4: 41;
end;
A73: for e be
Real st e
>
0 holds ex k be
Nat st for n be
Nat st n
>= k holds for x be
Point of X, y be
Point of Y holds
||.(((vseq
. n)
. (x,y))
- (tseq
. (x,y))).||
<= ((e
*
||.x.||)
*
||.y.||)
proof
let e be
Real;
assume e
>
0 ;
then
consider k be
Nat such that
A74: for n,m be
Nat st n
>= k & m
>= k holds
||.((vseq
. n)
- (vseq
. m)).||
< e by
A2,
RSSPACE3: 8;
take k;
now
let n be
Nat such that
A75: n
>= k;
now
let x be
Point of X, y be
Point of Y;
[x, y] is
set by
TARSKI: 1;
then
reconsider xy =
[x, y] as
Point of
[:X, Y:] by
PRVECT_3: 18;
consider xyseq be
sequence of Z such that
A76: for n be
Nat holds (xyseq
. n)
= ((vseq
. n)
. xy) and
A77: xyseq is
convergent and
A78: (tseq
. xy)
= (
lim xyseq) by
A24;
A79: for m,k be
Nat holds
||.((xyseq
. m)
- (xyseq
. k)).||
<= (
||.((vseq
. m)
- (vseq
. k)).||
* (
||.x.||
*
||.y.||))
proof
let m,k be
Nat;
reconsider h1 = ((vseq
. m)
- (vseq
. k)) as
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
(xyseq
. k)
= ((vseq
. k)
. xy) by
A76;
then ((xyseq
. m)
- (xyseq
. k))
= (((vseq
. m)
. (x,y))
- ((vseq
. k)
. (x,y))) by
A76
.= (h1
. (x,y)) by
Th40;
then
||.((xyseq
. m)
- (xyseq
. k)).||
<= ((
||.((vseq
. m)
- (vseq
. k)).||
*
||.x.||)
*
||.y.||) by
Th32;
hence thesis;
end;
A81: for m be
Nat st m
>= k holds
||.((xyseq
. n)
- (xyseq
. m)).||
<= ((e
*
||.x.||)
*
||.y.||)
proof
let m be
Nat;
assume m
>= k;
then
A82:
||.((vseq
. n)
- (vseq
. m)).||
< e by
A74,
A75;
A83:
||.((xyseq
. n)
- (xyseq
. m)).||
<= (
||.((vseq
. n)
- (vseq
. m)).||
* (
||.x.||
*
||.y.||)) by
A79;
(
||.((vseq
. n)
- (vseq
. m)).||
* (
||.x.||
*
||.y.||))
<= (e
* (
||.x.||
*
||.y.||)) by
A82,
XREAL_1: 64;
hence thesis by
A83,
XXREAL_0: 2;
end;
||.((xyseq
. n)
- (tseq
. (x,y))).||
<= ((e
*
||.x.||)
*
||.y.||)
proof
deffunc
F(
Nat) =
||.((xyseq
. $1)
- (xyseq
. n)).||;
consider rseq be
Real_Sequence such that
A84: for m be
Nat holds (rseq
. m)
=
F(m) from
SEQ_1:sch 1;
now
let i be
object;
assume i
in
NAT ;
then
reconsider k = i as
Nat;
thus (rseq
. i)
=
||.((xyseq
. k)
- (xyseq
. n)).|| by
A84
.=
||.((xyseq
- (xyseq
. n))
. k).|| by
NORMSP_1:def 4
.= (
||.(xyseq
- (xyseq
. n)).||
. i) by
NORMSP_0:def 4;
end;
then
A85: rseq
=
||.(xyseq
- (xyseq
. n)).|| by
FUNCT_2: 12;
A86: (xyseq
- (xyseq
. n)) is
convergent by
A77,
NORMSP_1: 21;
(
lim (xyseq
- (xyseq
. n)))
= ((tseq
. (x,y))
- (xyseq
. n)) by
A77,
A78,
NORMSP_1: 27;
then
A87: (
lim rseq)
=
||.((tseq
. (x,y))
- (xyseq
. n)).|| by
A85,
A86,
LOPBAN_1: 41;
for m be
Nat st m
>= k holds (rseq
. m)
<= ((e
*
||.x.||)
*
||.y.||)
proof
let m be
Nat such that
A88: m
>= k;
(rseq
. m)
=
||.((xyseq
. m)
- (xyseq
. n)).|| by
A84
.=
||.((xyseq
. n)
- (xyseq
. m)).|| by
NORMSP_1: 7;
hence thesis by
A81,
A88;
end;
then (
lim rseq)
<= ((e
*
||.x.||)
*
||.y.||) by
A85,
A86,
LOPBAN_1: 41,
Lm3;
hence thesis by
A87,
NORMSP_1: 7;
end;
hence
||.(((vseq
. n)
. (x,y))
- (tseq
. (x,y))).||
<= ((e
*
||.x.||)
*
||.y.||) by
A76;
end;
hence for x be
Point of X, y be
Point of Y holds
||.(((vseq
. n)
. (x,y))
- (tseq
. (x,y))).||
<= ((e
*
||.x.||)
*
||.y.||);
end;
hence thesis;
end;
reconsider tseq as
Lipschitzian
BilinearOperator of X, Y, Z by
A60;
reconsider tv = tseq as
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by
Def9;
A89: for e be
Real st e
>
0 holds ex k be
Nat st for n be
Nat st n
>= k holds
||.((vseq
. n)
- tv).||
<= e
proof
let e be
Real such that
A90: e
>
0 ;
consider k be
Nat such that
A91: for n be
Nat st n
>= k holds for x be
Point of X, y be
Point of Y holds
||.(((vseq
. n)
. (x,y))
- (tseq
. (x,y))).||
<= ((e
*
||.x.||)
*
||.y.||) by
A73,
A90;
now
set g1 = tseq;
let n be
Nat such that
A92: n
>= k;
reconsider h1 = ((vseq
. n)
- tv) as
Lipschitzian
BilinearOperator of X, Y, Z by
Def9;
set f1 = (vseq
. n);
A93:
now
let t be
Point of X, s be
Point of Y;
assume
||.t.||
<= 1 &
||.s.||
<= 1;
then (
||.t.||
*
||.s.||)
<= (1
* 1) by
XREAL_1: 66;
then
A94: (e
* (
||.t.||
*
||.s.||))
<= (e
* 1) by
A90,
XREAL_1: 64;
A95:
||.((f1
. (t,s))
- (g1
. (t,s))).||
<= ((e
*
||.t.||)
*
||.s.||) by
A91,
A92;
||.(h1
. (t,s)).||
=
||.((f1
. (t,s))
- (g1
. (t,s))).|| by
Th40;
hence
||.(h1
. (t,s)).||
<= e by
A94,
A95,
XXREAL_0: 2;
end;
A96:
now
let r be
Real;
assume r
in (
PreNorms h1);
then ex t be
VECTOR of X, s be
VECTOR of Y st r
=
||.(h1
. (t,s)).|| &
||.t.||
<= 1 &
||.s.||
<= 1;
hence r
<= e by
A93;
end;
(for s be
Real st s
in (
PreNorms h1) holds s
<= e) implies (
upper_bound (
PreNorms h1))
<= e by
SEQ_4: 45;
hence
||.((vseq
. n)
- tv).||
<= e by
A96,
Th30;
end;
hence thesis;
end;
for e be
Real st e
>
0 holds ex m be
Nat st for n be
Nat st n
>= m holds
||.((vseq
. n)
- tv).||
< e
proof
let e be
Real such that
A98: e
>
0 ;
consider m be
Nat such that
A99: for n be
Nat st n
>= m holds
||.((vseq
. n)
- tv).||
<= (e
/ 2) by
A89,
A98,
XREAL_1: 215;
A100: (e
/ 2)
< e by
A98,
XREAL_1: 216;
now
let n be
Nat;
assume n
>= m;
then
||.((vseq
. n)
- tv).||
<= (e
/ 2) by
A99;
hence
||.((vseq
. n)
- tv).||
< e by
A100,
XXREAL_0: 2;
end;
hence thesis;
end;
hence thesis by
NORMSP_1:def 6;
end;
theorem ::
LOPBAN_9:25
Th43: for X,Y be
RealNormSpace, Z be
RealBanachSpace holds (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) is
RealBanachSpace
proof
let X,Y be
RealNormSpace;
let Z be
RealBanachSpace;
for seq be
sequence of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st seq is
Cauchy_sequence_by_Norm holds seq is
convergent by
Th42;
hence thesis by
LOPBAN_1:def 15;
end;
registration
let X,Y be
RealNormSpace;
let Z be
RealBanachSpace;
cluster (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ->
complete;
coherence by
Th43;
end
begin
reserve X,Y,Z for
RealLinearSpace;
theorem ::
LOPBAN_9:26
ex I be
LinearOperator of (
R_VectorSpace_of_LinearOperators (X,(
R_VectorSpace_of_LinearOperators (Y,Z)))), (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) st I is
bijective & for u be
Point of (
R_VectorSpace_of_LinearOperators (X,(
R_VectorSpace_of_LinearOperators (Y,Z)))) holds for x be
Point of X, y be
Point of Y holds ((I
. u)
. (x,y))
= ((u
. x)
. y)
proof
set XC = the
carrier of X;
set YC = the
carrier of Y;
set ZC = the
carrier of Z;
consider I0 be
Function of (
Funcs (XC,(
Funcs (YC,ZC)))), (
Funcs (
[:XC, YC:],ZC)) such that
A1: I0 is
bijective & for f be
Function of XC, (
Funcs (YC,ZC)) holds for d,e be
object st d
in XC & e
in YC holds ((I0
. f)
. (d,e))
= ((f
. d)
. e) by
NDIFF_6: 1;
set LXYZ = the
carrier of (
R_VectorSpace_of_LinearOperators (X,(
R_VectorSpace_of_LinearOperators (Y,Z))));
set BXYZ = the
carrier of (
R_VectorSpace_of_BilinearOperators (X,Y,Z));
set LYZ = the
carrier of (
R_VectorSpace_of_LinearOperators (Y,Z));
now
let x be
object;
assume x
in (
Funcs (XC,LYZ));
then
consider f be
Function such that
A5: x
= f & (
dom f)
= XC & (
rng f)
c= LYZ by
FUNCT_2:def 2;
(
rng f)
c= (
Funcs (YC,ZC)) by
A5,
XBOOLE_1: 1;
hence x
in (
Funcs (XC,(
Funcs (YC,ZC)))) by
A5,
FUNCT_2:def 2;
end;
then
A6: (
Funcs (XC,LYZ))
c= (
Funcs (XC,(
Funcs (YC,ZC)))) by
TARSKI:def 3;
then LXYZ
c= (
Funcs (XC,(
Funcs (YC,ZC)))) by
XBOOLE_1: 1;
then
reconsider I = (I0
| LXYZ) as
Function of LXYZ, (
Funcs (
[:XC, YC:],ZC)) by
FUNCT_2: 32;
A7: for x be
Element of LXYZ holds (for p be
Point of X, q be
Point of Y holds ex G be
LinearOperator of Y, Z st G
= (x
. p) & ((I
. x)
. (p,q))
= (G
. q)) & (I
. x)
in BXYZ
proof
let f be
Element of LXYZ;
A8: (I
. f)
= (I0
. f) by
FUNCT_1: 49;
A9: f
in (
Funcs (XC,(
Funcs (YC,ZC)))) by
A6,
TARSKI:def 3,
XBOOLE_1: 1;
then
A10: f is
Function of XC, (
Funcs (YC,ZC)) by
FUNCT_2: 66;
reconsider g = f as
Function of XC, (
Funcs (YC,ZC)) by
A9,
FUNCT_2: 66;
reconsider F = f as
LinearOperator of X, (
R_VectorSpace_of_LinearOperators (Y,Z)) by
LOPBAN_1:def 6;
thus for x be
Point of X, y be
Point of Y holds ex G be
LinearOperator of Y, Z st G
= (f
. x) & ((I
. f)
. (x,y))
= (G
. y)
proof
let x be
Point of X, y be
Point of Y;
(g
. x)
= (F
. x);
then
reconsider G = (g
. x) as
LinearOperator of Y, Z by
LOPBAN_1:def 6;
take G;
thus thesis by
A1,
A8;
end;
reconsider BL = (I0
. f) as
Function of
[:X, Y:], Z by
A9,
FUNCT_2: 5,
FUNCT_2: 66;
A14: for x1,x2 be
Point of X, y be
Point of Y holds (BL
. ((x1
+ x2),y))
= ((BL
. (x1,y))
+ (BL
. (x2,y)))
proof
let x1,x2 be
Point of X, y be
Point of Y;
A15: (BL
. (x1,y))
= ((F
. x1)
. y) by
A1,
A10;
A16: (BL
. (x2,y))
= ((F
. x2)
. y) by
A1,
A10;
A17: (BL
. ((x1
+ x2),y))
= ((F
. (x1
+ x2))
. y) by
A1,
A10;
(F
. (x1
+ x2))
= ((F
. x1)
+ (F
. x2)) by
VECTSP_1:def 20;
hence thesis by
A15,
A16,
A17,
LOPBAN_1: 16;
end;
A18: for x be
Point of X, y be
Point of Y, a be
Real holds (BL
. ((a
* x),y))
= (a
* (BL
. (x,y)))
proof
let x be
Point of X, y be
Point of Y, a be
Real;
A19: (BL
. ((a
* x),y))
= ((F
. (a
* x))
. y) by
A1,
A10;
A20: (BL
. (x,y))
= ((F
. x)
. y) by
A1,
A10;
(F
. (a
* x))
= (a
* (F
. x)) by
LOPBAN_1:def 5;
hence thesis by
A19,
A20,
LOPBAN_1: 17;
end;
A21: for x be
Point of X, y1,y2 be
Point of Y holds (BL
. (x,(y1
+ y2)))
= ((BL
. (x,y1))
+ (BL
. (x,y2)))
proof
let x be
Point of X, y1,y2 be
Point of Y;
reconsider Fx = (F
. x) as
LinearOperator of Y, Z by
LOPBAN_1:def 6;
A22: (BL
. (x,y1))
= (Fx
. y1) by
A1,
A10;
A23: (BL
. (x,y2))
= (Fx
. y2) by
A1,
A10;
(BL
. (x,(y1
+ y2)))
= (Fx
. (y1
+ y2)) by
A1,
A10;
hence thesis by
A22,
A23,
VECTSP_1:def 20;
end;
A25: for x be
Point of X, y be
Point of Y, a be
Real holds (BL
. (x,(a
* y)))
= (a
* (BL
. (x,y)))
proof
let x be
Point of X, y be
Point of Y, a be
Real;
reconsider Fx = (F
. x) as
LinearOperator of Y, Z by
LOPBAN_1:def 6;
A26: (BL
. (x,y))
= (Fx
. y) by
A1,
A10;
(BL
. (x,(a
* y)))
= (Fx
. (a
* y)) by
A1,
A10;
hence thesis by
A26,
LOPBAN_1:def 5;
end;
reconsider BL as
BilinearOperator of X, Y, Z by
A14,
A18,
A21,
A25,
LOPBAN_8: 11;
BL
in BXYZ by
Def6;
hence (I
. f)
in BXYZ by
FUNCT_1: 49;
end;
then (
rng I)
c= BXYZ by
FUNCT_2: 114;
then
reconsider I as
Function of LXYZ, BXYZ by
FUNCT_2: 6;
A28: for x1,x2 be
Element of LXYZ holds (I
. (x1
+ x2))
= ((I
. x1)
+ (I
. x2))
proof
let x1,x2 be
Element of LXYZ;
for p be
Point of X, q be
Point of Y holds ((I
. (x1
+ x2))
. (p,q))
= (((I
. x1)
. (p,q))
+ ((I
. x2)
. (p,q)))
proof
let p be
Point of X, q be
Point of Y;
consider Gx1p be
LinearOperator of Y, Z such that
A29: Gx1p
= (x1
. p) & ((I
. x1)
. (p,q))
= (Gx1p
. q) by
A7;
consider Gx2p be
LinearOperator of Y, Z such that
A30: Gx2p
= (x2
. p) & ((I
. x2)
. (p,q))
= (Gx2p
. q) by
A7;
consider Gx1x2p be
LinearOperator of Y, Z such that
A31: Gx1x2p
= ((x1
+ x2)
. p) & ((I
. (x1
+ x2))
. (p,q))
= (Gx1x2p
. q) by
A7;
((x1
+ x2)
. p)
= ((x1
. p)
+ (x2
. p)) by
LOPBAN_1: 16;
hence thesis by
A29,
A30,
A31,
LOPBAN_1: 16;
end;
hence thesis by
Th16;
end;
for x be
Element of LXYZ, a be
Real holds (I
. (a
* x))
= (a
* (I
. x))
proof
let x be
Element of LXYZ, a be
Real;
for p be
Point of X, q be
Point of Y holds ((I
. (a
* x))
. (p,q))
= (a
* ((I
. x)
. (p,q)))
proof
let p be
Point of X, q be
Point of Y;
consider Gxp be
LinearOperator of Y, Z such that
A33: Gxp
= (x
. p) & ((I
. x)
. (p,q))
= (Gxp
. q) by
A7;
consider Gxap be
LinearOperator of Y, Z such that
A34: Gxap
= ((a
* x)
. p) & ((I
. (a
* x))
. (p,q))
= (Gxap
. q) by
A7;
((a
* x)
. p)
= (a
* (x
. p)) by
LOPBAN_1: 17;
hence thesis by
A33,
A34,
LOPBAN_1: 17;
end;
hence thesis by
Th17;
end;
then
reconsider I as
LinearOperator of (
R_VectorSpace_of_LinearOperators (X,(
R_VectorSpace_of_LinearOperators (Y,Z)))), (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
A28,
LOPBAN_1:def 5,
VECTSP_1:def 20;
A36: for u be
Point of (
R_VectorSpace_of_LinearOperators (X,(
R_VectorSpace_of_LinearOperators (Y,Z)))) holds for x be
Point of X, y be
Point of Y holds ((I
. u)
. (x,y))
= ((u
. x)
. y)
proof
let u be
Point of (
R_VectorSpace_of_LinearOperators (X,(
R_VectorSpace_of_LinearOperators (Y,Z))));
let p be
Point of X, q be
Point of Y;
consider G be
LinearOperator of Y, Z such that
A37: G
= (u
. p) & ((I
. u)
. (p,q))
= (G
. q) by
A7;
thus ((I
. u)
. (p,q))
= ((u
. p)
. q) by
A37;
end;
for y be
object st y
in BXYZ holds ex x be
object st x
in LXYZ & y
= (I
. x)
proof
let y be
object;
assume
A39: y
in BXYZ;
then y
in (
Funcs (
[:XC, YC:],ZC));
then y
in (
rng I0) by
A1,
FUNCT_2:def 3;
then
consider f be
object such that
A40: f
in (
Funcs (XC,(
Funcs (YC,ZC)))) & (I0
. f)
= y by
FUNCT_2: 11;
reconsider f as
Function of XC, (
Funcs (YC,ZC)) by
A40,
FUNCT_2: 66;
reconsider BL = y as
BilinearOperator of X, Y, Z by
A39,
Def6;
reconsider BLp = BL as
Point of (
R_VectorSpace_of_BilinearOperators (X,Y,Z)) by
Def6;
A42: (
dom f)
= XC by
FUNCT_2:def 1;
for x be
object st x
in XC holds (f
. x)
in LYZ
proof
let x be
object;
assume
A43: x
in XC;
then
reconsider fx = (f
. x) as
Function of YC, ZC by
FUNCT_2: 5,
FUNCT_2: 66;
reconsider xp = x as
Point of X by
A43;
A44: for p be
Point of Y, q be
Point of Y holds (fx
. (p
+ q))
= ((fx
. p)
+ (fx
. q))
proof
let p be
Point of Y, q be
Point of Y;
A45: (BL
. (xp,p))
= (fx
. p) by
A1,
A40;
A46: (BL
. (xp,q))
= (fx
. q) by
A1,
A40;
(BL
. (xp,(p
+ q)))
= (fx
. (p
+ q)) by
A1,
A40;
hence (fx
. (p
+ q))
= ((fx
. p)
+ (fx
. q)) by
A45,
A46,
LOPBAN_8: 11;
end;
for p be
Point of Y, a be
Real holds (fx
. (a
* p))
= (a
* (fx
. p))
proof
let p be
Point of Y, a be
Real;
A48: (BL
. (xp,p))
= (fx
. p) by
A1,
A40;
(BL
. (xp,(a
* p)))
= (fx
. (a
* p)) by
A1,
A40;
hence (fx
. (a
* p))
= (a
* (fx
. p)) by
A48,
LOPBAN_8: 11;
end;
then
reconsider fx as
LinearOperator of Y, Z by
A44,
LOPBAN_1:def 5,
VECTSP_1:def 20;
fx
in LYZ by
LOPBAN_1:def 6;
hence (f
. x)
in LYZ;
end;
then
reconsider f as
Function of XC, LYZ by
A42,
FUNCT_2: 3;
A50: for x1,x2 be
Point of X holds (f
. (x1
+ x2))
= ((f
. x1)
+ (f
. x2))
proof
let x1,x2 be
Point of X;
reconsider fx1x2 = (f
. (x1
+ x2)) as
LinearOperator of Y, Z by
LOPBAN_1:def 6;
reconsider fx1 = (f
. x1) as
LinearOperator of Y, Z by
LOPBAN_1:def 6;
reconsider fx2 = (f
. x2) as
LinearOperator of Y, Z by
LOPBAN_1:def 6;
for y be
Point of Y holds (fx1x2
. y)
= ((fx1
. y)
+ (fx2
. y))
proof
let y be
Point of Y;
A51: (BL
. (x1,y))
= (fx1
. y) by
A1,
A40;
A52: (BL
. (x2,y))
= (fx2
. y) by
A1,
A40;
(BL
. ((x1
+ x2),y))
= (fx1x2
. y) by
A1,
A40;
hence (fx1x2
. y)
= ((fx1
. y)
+ (fx2
. y)) by
A51,
A52,
LOPBAN_8: 11;
end;
hence (f
. (x1
+ x2))
= ((f
. x1)
+ (f
. x2)) by
LOPBAN_1: 16;
end;
for x be
Point of X, a be
Real holds (f
. (a
* x))
= (a
* (f
. x))
proof
let x be
Point of X, a be
Real;
reconsider fx = (f
. x) as
LinearOperator of Y, Z by
LOPBAN_1:def 6;
reconsider fax = (f
. (a
* x)) as
LinearOperator of Y, Z by
LOPBAN_1:def 6;
for y be
Point of Y holds (fax
. y)
= (a
* (fx
. y))
proof
let y be
Point of Y;
A54: (BL
. (x,y))
= (fx
. y) by
A1,
A40;
(BL
. ((a
* x),y))
= (fax
. y) by
A1,
A40;
hence (fax
. y)
= (a
* (fx
. y)) by
A54,
LOPBAN_8: 11;
end;
hence (f
. (a
* x))
= (a
* (f
. x)) by
LOPBAN_1: 17;
end;
then
reconsider f as
LinearOperator of X, (
R_VectorSpace_of_LinearOperators (Y,Z)) by
A50,
LOPBAN_1:def 5,
VECTSP_1:def 20;
A56: f
in LXYZ by
LOPBAN_1:def 6;
take f;
thus thesis by
A40,
A56,
FUNCT_1: 49;
end;
then
A58: (
rng I)
= BXYZ by
FUNCT_2: 10;
reconsider I as
LinearOperator of (
R_VectorSpace_of_LinearOperators (X,(
R_VectorSpace_of_LinearOperators (Y,Z)))), (
R_VectorSpace_of_BilinearOperators (X,Y,Z));
take I;
I is
one-to-one
onto by
A1,
A58,
FUNCT_1: 52,
FUNCT_2:def 3;
hence thesis by
A36;
end;
reserve X,Y,Z for
RealNormSpace;
theorem ::
LOPBAN_9:27
ex I be
LinearOperator of (
R_NormSpace_of_BoundedLinearOperators (X,(
R_NormSpace_of_BoundedLinearOperators (Y,Z)))), (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st I is
bijective & for u be
Point of (
R_NormSpace_of_BoundedLinearOperators (X,(
R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
||.u.||
=
||.(I
. u).|| & for x be
Point of X, y be
Point of Y holds ((I
. u)
. (x,y))
= ((u
. x)
. y)
proof
set XC = the
carrier of X;
set YC = the
carrier of Y;
set ZC = the
carrier of Z;
consider I0 be
Function of (
Funcs (XC,(
Funcs (YC,ZC)))), (
Funcs (
[:XC, YC:],ZC)) such that
A1: I0 is
bijective & for f be
Function of XC, (
Funcs (YC,ZC)) holds for d,e be
object st d
in XC & e
in YC holds ((I0
. f)
. (d,e))
= ((f
. d)
. e) by
NDIFF_6: 1;
set LXYZ = the
carrier of (
R_NormSpace_of_BoundedLinearOperators (X,(
R_NormSpace_of_BoundedLinearOperators (Y,Z))));
set BXYZ = the
carrier of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
set LYZ = the
carrier of (
R_NormSpace_of_BoundedLinearOperators (Y,Z));
A3: LYZ
c= (
Funcs (YC,ZC)) by
XBOOLE_1: 1;
A4: LXYZ
c= (
Funcs (XC,LYZ)) by
XBOOLE_1: 1;
(
Funcs (XC,LYZ))
c= (
Funcs (XC,(
Funcs (YC,ZC))))
proof
let x be
object;
assume x
in (
Funcs (XC,LYZ));
then
consider f be
Function such that
A6: x
= f & (
dom f)
= XC & (
rng f)
c= LYZ by
FUNCT_2:def 2;
(
rng f)
c= (
Funcs (YC,ZC)) by
A3,
A6,
XBOOLE_1: 1;
hence x
in (
Funcs (XC,(
Funcs (YC,ZC)))) by
A6,
FUNCT_2:def 2;
end;
then
A7: LXYZ
c= (
Funcs (XC,(
Funcs (YC,ZC)))) by
A4,
XBOOLE_1: 1;
then
reconsider I = (I0
| LXYZ) as
Function of LXYZ, (
Funcs (
[:XC, YC:],ZC)) by
FUNCT_2: 32;
A8: for x be
Element of LXYZ holds (for p be
Point of X, q be
Point of Y holds ex G be
Lipschitzian
LinearOperator of Y, Z st G
= (x
. p) & ((I
. x)
. (p,q))
= (G
. q)) & (I
. x) is
Lipschitzian
BilinearOperator of X, Y, Z & (I
. x)
in BXYZ & ex Ix be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st Ix
= (I
. x) &
||.x.||
=
||.Ix.||
proof
let f be
Element of LXYZ;
A9: (I
. f)
= (I0
. f) by
FUNCT_1: 49;
A10: f
in (
Funcs (XC,(
Funcs (YC,ZC)))) by
A7,
TARSKI:def 3;
A11: f is
Function of XC, (
Funcs (YC,ZC)) by
A7,
TARSKI:def 3,
FUNCT_2: 66;
reconsider g = f as
Function of XC, (
Funcs (YC,ZC)) by
A7,
TARSKI:def 3,
FUNCT_2: 66;
reconsider F = f as
Lipschitzian
LinearOperator of X, (
R_NormSpace_of_BoundedLinearOperators (Y,Z)) by
LOPBAN_1:def 9;
thus for x be
Point of X, y be
Point of Y holds ex G be
Lipschitzian
LinearOperator of Y, Z st G
= (f
. x) & ((I
. f)
. (x,y))
= (G
. y)
proof
let x be
Point of X, y be
Point of Y;
(g
. x)
= (F
. x);
then
reconsider G = (g
. x) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
take G;
thus thesis by
A1,
A9;
end;
reconsider BL = (I0
. f) as
Function of
[:X, Y:], Z by
A10,
FUNCT_2: 5,
FUNCT_2: 66;
A15: for x1,x2 be
Point of X, y be
Point of Y holds (BL
. ((x1
+ x2),y))
= ((BL
. (x1,y))
+ (BL
. (x2,y)))
proof
let x1,x2 be
Point of X, y be
Point of Y;
A16: (BL
. (x1,y))
= ((F
. x1)
. y) by
A1,
A11;
A17: (BL
. (x2,y))
= ((F
. x2)
. y) by
A1,
A11;
A18: (BL
. ((x1
+ x2),y))
= ((F
. (x1
+ x2))
. y) by
A1,
A11;
(F
. (x1
+ x2))
= ((F
. x1)
+ (F
. x2)) by
VECTSP_1:def 20;
hence thesis by
A16,
A17,
A18,
LOPBAN_1: 35;
end;
A19: for x be
Point of X, y be
Point of Y, a be
Real holds (BL
. ((a
* x),y))
= (a
* (BL
. (x,y)))
proof
let x be
Point of X, y be
Point of Y, a be
Real;
A20: (BL
. ((a
* x),y))
= ((F
. (a
* x))
. y) by
A1,
A11;
A21: (BL
. (x,y))
= ((F
. x)
. y) by
A1,
A11;
(F
. (a
* x))
= (a
* (F
. x)) by
LOPBAN_1:def 5;
hence thesis by
A20,
A21,
LOPBAN_1: 36;
end;
A22: for x be
Point of X, y1,y2 be
Point of Y holds (BL
. (x,(y1
+ y2)))
= ((BL
. (x,y1))
+ (BL
. (x,y2)))
proof
let x be
Point of X, y1,y2 be
Point of Y;
reconsider Fx = (F
. x) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
A23: (BL
. (x,y1))
= (Fx
. y1) by
A1,
A11;
A24: (BL
. (x,y2))
= (Fx
. y2) by
A1,
A11;
(BL
. (x,(y1
+ y2)))
= (Fx
. (y1
+ y2)) by
A1,
A11;
hence thesis by
A23,
A24,
VECTSP_1:def 20;
end;
A26: for x be
Point of X, y be
Point of Y, a be
Real holds (BL
. (x,(a
* y)))
= (a
* (BL
. (x,y)))
proof
let x be
Point of X, y be
Point of Y, a be
Real;
reconsider Fx = (F
. x) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
A27: (BL
. (x,y))
= (Fx
. y) by
A1,
A11;
(BL
. (x,(a
* y)))
= (Fx
. (a
* y)) by
A1,
A11;
hence thesis by
A27,
LOPBAN_1:def 5;
end;
reconsider BL as
BilinearOperator of X, Y, Z by
A15,
A19,
A22,
A26,
LOPBAN_8: 12;
A29: for x be
Point of X, y be
Point of Y holds
||.(BL
. (x,y)).||
<= ((
||.f.||
*
||.x.||)
*
||.y.||)
proof
let x be
Point of X, y be
Point of Y;
reconsider Fx = (F
. x) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
A30: (BL
. (x,y))
= (Fx
. y) by
A1,
A11;
A31:
||.(Fx
. y).||
<= (
||.(F
. x).||
*
||.y.||) by
LOPBAN_1: 32;
(
||.(F
. x).||
*
||.y.||)
<= ((
||.f.||
*
||.x.||)
*
||.y.||) by
LOPBAN_1: 32,
XREAL_1: 64;
hence
||.(BL
. (x,y)).||
<= ((
||.f.||
*
||.x.||)
*
||.y.||) by
A30,
A31,
XXREAL_0: 2;
end;
then
reconsider BL as
Lipschitzian
BilinearOperator of X, Y, Z by
Def8;
reconsider BLp = BL as
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by
Def9;
(I
. f)
= BL by
FUNCT_1: 49;
hence (I
. f) is
Lipschitzian
BilinearOperator of X, Y, Z;
BLp
in BXYZ;
hence (I
. f)
in BXYZ by
FUNCT_1: 49;
A33:
||.BLp.||
= (
upper_bound (
PreNorms (
modetrans (BL,X,Y,Z)))) by
Def13
.= (
upper_bound (
PreNorms BL));
now
let r be
Real;
assume r
in (
PreNorms BL);
then
consider t be
VECTOR of X, s be
VECTOR of Y such that
A34: r
=
||.(BL
. (t,s)).|| and
A35:
||.t.||
<= 1 &
||.s.||
<= 1;
A36:
||.(BL
. (t,s)).||
<= ((
||.f.||
*
||.t.||)
*
||.s.||) by
A29;
(
||.t.||
*
||.s.||)
<= (1
* 1) by
A35,
XREAL_1: 66;
then (
||.f.||
* (
||.t.||
*
||.s.||))
<= (
||.f.||
* 1) by
XREAL_1: 64;
hence r
<=
||.f.|| by
A34,
A36,
XXREAL_0: 2;
end;
then
A37:
||.BLp.||
<=
||.f.|| by
A33,
SEQ_4: 45;
A39:
||.f.||
= (
upper_bound (
PreNorms (
modetrans (F,X,(
R_NormSpace_of_BoundedLinearOperators (Y,Z)))))) by
LOPBAN_1:def 13
.= (
upper_bound (
PreNorms F)) by
LOPBAN_1: 29;
now
let r be
Real;
assume r
in (
PreNorms F);
then
consider x be
VECTOR of X such that
A40: r
=
||.(F
. x).|| and
A41:
||.x.||
<= 1;
reconsider Fx = (F
. x) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
A42:
||.(F
. x).||
= (
upper_bound (
PreNorms Fx)) by
LOPBAN_1: 30;
now
let s be
Real;
assume s
in (
PreNorms Fx);
then
consider y be
Point of Y such that
B42: s
=
||.(Fx
. y).|| and
A43:
||.y.||
<= 1;
A44:
||.(Fx
. y).||
=
||.(BL
. (x,y)).|| by
A1,
A11;
A45:
||.(BL
. (x,y)).||
<= ((
||.BLp.||
*
||.x.||)
*
||.y.||) by
Th32;
(
||.x.||
*
||.y.||)
<= (1
* 1) by
A41,
A43,
XREAL_1: 66;
then (
||.BLp.||
* (
||.x.||
*
||.y.||))
<= (
||.BLp.||
* 1) by
XREAL_1: 64;
hence s
<=
||.BLp.|| by
B42,
A44,
A45,
XXREAL_0: 2;
end;
hence r
<=
||.BLp.|| by
A40,
A42,
SEQ_4: 45;
end;
then
A46:
||.f.||
<=
||.BLp.|| by
A39,
SEQ_4: 45;
take BLp;
thus BLp
= (I
. f) &
||.f.||
=
||.BLp.|| by
A37,
A46,
FUNCT_1: 49,
XXREAL_0: 1;
end;
then (
rng I)
c= BXYZ by
FUNCT_2: 114;
then
reconsider I as
Function of LXYZ, BXYZ by
FUNCT_2: 6;
A47: for x1,x2 be
Element of LXYZ holds (I
. (x1
+ x2))
= ((I
. x1)
+ (I
. x2))
proof
let x1,x2 be
Element of LXYZ;
for p be
Point of X, q be
Point of Y holds ((I
. (x1
+ x2))
. (p,q))
= (((I
. x1)
. (p,q))
+ ((I
. x2)
. (p,q)))
proof
let p be
Point of X, q be
Point of Y;
consider Gx1p be
Lipschitzian
LinearOperator of Y, Z such that
A48: Gx1p
= (x1
. p) & ((I
. x1)
. (p,q))
= (Gx1p
. q) by
A8;
consider Gx2p be
Lipschitzian
LinearOperator of Y, Z such that
A49: Gx2p
= (x2
. p) & ((I
. x2)
. (p,q))
= (Gx2p
. q) by
A8;
consider Gx1x2p be
Lipschitzian
LinearOperator of Y, Z such that
A50: Gx1x2p
= ((x1
+ x2)
. p) & ((I
. (x1
+ x2))
. (p,q))
= (Gx1x2p
. q) by
A8;
((x1
+ x2)
. p)
= ((x1
. p)
+ (x2
. p)) by
LOPBAN_1: 35;
hence thesis by
A48,
A49,
A50,
LOPBAN_1: 35;
end;
hence thesis by
Th35;
end;
for x be
Element of LXYZ, a be
Real holds (I
. (a
* x))
= (a
* (I
. x))
proof
let x be
Element of LXYZ, a be
Real;
for p be
Point of X, q be
Point of Y holds ((I
. (a
* x))
. (p,q))
= (a
* ((I
. x)
. (p,q)))
proof
let p be
Point of X, q be
Point of Y;
consider Gxp be
Lipschitzian
LinearOperator of Y, Z such that
A52: Gxp
= (x
. p) & ((I
. x)
. (p,q))
= (Gxp
. q) by
A8;
consider Gxap be
Lipschitzian
LinearOperator of Y, Z such that
A53: Gxap
= ((a
* x)
. p) & ((I
. (a
* x))
. (p,q))
= (Gxap
. q) by
A8;
((a
* x)
. p)
= (a
* (x
. p)) by
LOPBAN_1: 36;
hence thesis by
A52,
A53,
LOPBAN_1: 36;
end;
hence thesis by
Th36;
end;
then
reconsider I as
LinearOperator of (
R_NormSpace_of_BoundedLinearOperators (X,(
R_NormSpace_of_BoundedLinearOperators (Y,Z)))), (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by
A47,
LOPBAN_1:def 5,
VECTSP_1:def 20;
A55: for u be
Point of (
R_NormSpace_of_BoundedLinearOperators (X,(
R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
||.u.||
=
||.(I
. u).|| & for x be
Point of X, y be
Point of Y holds ((I
. u)
. (x,y))
= ((u
. x)
. y)
proof
let u be
Point of (
R_NormSpace_of_BoundedLinearOperators (X,(
R_NormSpace_of_BoundedLinearOperators (Y,Z))));
consider Iu be
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) such that
A56: Iu
= (I
. u) &
||.u.||
=
||.Iu.|| by
A8;
thus
||.u.||
=
||.(I
. u).|| by
A56;
let p be
Point of X, q be
Point of Y;
consider G be
Lipschitzian
LinearOperator of Y, Z such that
A57: G
= (u
. p) & ((I
. u)
. (p,q))
= (G
. q) by
A8;
thus ((I
. u)
. (p,q))
= ((u
. p)
. q) by
A57;
end;
for y be
object st y
in BXYZ holds ex x be
object st x
in LXYZ & y
= (I
. x)
proof
let y be
object;
assume
A59: y
in BXYZ;
then y
in (
Funcs (
[:XC, YC:],ZC)) by
TARSKI:def 3;
then y
in (
rng I0) by
A1,
FUNCT_2:def 3;
then
consider f be
object such that
A60: f
in (
Funcs (XC,(
Funcs (YC,ZC)))) & (I0
. f)
= y by
FUNCT_2: 11;
reconsider f as
Function of XC, (
Funcs (YC,ZC)) by
A60,
FUNCT_2: 66;
reconsider BL = y as
Lipschitzian
BilinearOperator of X, Y, Z by
A59,
Def9;
reconsider BLp = BL as
Point of (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by
Def9;
A62: (
dom f)
= XC by
FUNCT_2:def 1;
for x be
object st x
in XC holds (f
. x)
in LYZ
proof
let x be
object;
assume
A63: x
in XC;
then
reconsider fx = (f
. x) as
Function of YC, ZC by
FUNCT_2: 5,
FUNCT_2: 66;
reconsider xp = x as
Point of X by
A63;
A64: for p be
Point of Y, q be
Point of Y holds (fx
. (p
+ q))
= ((fx
. p)
+ (fx
. q))
proof
let p be
Point of Y, q be
Point of Y;
A65: (BL
. (xp,p))
= (fx
. p) by
A60,
A1;
A66: (BL
. (xp,q))
= (fx
. q) by
A60,
A1;
(BL
. (xp,(p
+ q)))
= (fx
. (p
+ q)) by
A60,
A1;
hence (fx
. (p
+ q))
= ((fx
. p)
+ (fx
. q)) by
A65,
A66,
LOPBAN_8: 12;
end;
for p be
Point of Y, a be
Real holds (fx
. (a
* p))
= (a
* (fx
. p))
proof
let p be
Point of Y, a be
Real;
A68: (BL
. (xp,p))
= (fx
. p) by
A60,
A1;
(BL
. (xp,(a
* p)))
= (fx
. (a
* p)) by
A60,
A1;
hence (fx
. (a
* p))
= (a
* (fx
. p)) by
A68,
LOPBAN_8: 12;
end;
then
reconsider fx as
LinearOperator of Y, Z by
A64,
LOPBAN_1:def 5,
VECTSP_1:def 20;
for p be
Point of Y holds
||.(fx
. p).||
<= ((
||.BLp.||
*
||.xp.||)
*
||.p.||)
proof
let p be
Point of Y;
(BL
. (xp,p))
= (fx
. p) by
A60,
A1;
hence thesis by
Th32;
end;
then
reconsider fx as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 8;
fx
in LYZ by
LOPBAN_1:def 9;
hence (f
. x)
in LYZ;
end;
then
reconsider f as
Function of XC, LYZ by
A62,
FUNCT_2: 3;
A71: for x1,x2 be
Point of X holds (f
. (x1
+ x2))
= ((f
. x1)
+ (f
. x2))
proof
let x1,x2 be
Point of X;
reconsider fx1x2 = (f
. (x1
+ x2)) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
reconsider fx1 = (f
. x1) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
reconsider fx2 = (f
. x2) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
for y be
Point of Y holds (fx1x2
. y)
= ((fx1
. y)
+ (fx2
. y))
proof
let y be
Point of Y;
A72: (BL
. (x1,y))
= (fx1
. y) by
A60,
A1;
A73: (BL
. (x2,y))
= (fx2
. y) by
A60,
A1;
(BL
. ((x1
+ x2),y))
= (fx1x2
. y) by
A60,
A1;
hence (fx1x2
. y)
= ((fx1
. y)
+ (fx2
. y)) by
A72,
A73,
LOPBAN_8: 12;
end;
hence (f
. (x1
+ x2))
= ((f
. x1)
+ (f
. x2)) by
LOPBAN_1: 35;
end;
for x be
Point of X, a be
Real holds (f
. (a
* x))
= (a
* (f
. x))
proof
let x be
Point of X, a be
Real;
reconsider fx = (f
. x) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
reconsider fax = (f
. (a
* x)) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
for y be
Point of Y holds (fax
. y)
= (a
* (fx
. y))
proof
let y be
Point of Y;
A75: (BL
. (x,y))
= (fx
. y) by
A60,
A1;
(BL
. ((a
* x),y))
= (fax
. y) by
A60,
A1;
hence (fax
. y)
= (a
* (fx
. y)) by
A75,
LOPBAN_8: 12;
end;
hence (f
. (a
* x))
= (a
* (f
. x)) by
LOPBAN_1: 36;
end;
then
reconsider f as
LinearOperator of X, (
R_NormSpace_of_BoundedLinearOperators (Y,Z)) by
A71,
LOPBAN_1:def 5,
VECTSP_1:def 20;
for x be
Point of X holds
||.(f
. x).||
<= (
||.BLp.||
*
||.x.||)
proof
let x be
Point of X;
reconsider fx = (f
. x) as
Lipschitzian
LinearOperator of Y, Z by
LOPBAN_1:def 9;
A78: for y be
Point of Y holds
||.(fx
. y).||
<= ((
||.BLp.||
*
||.x.||)
*
||.y.||)
proof
let y be
Point of Y;
(BL
. (x,y))
= (fx
. y) by
A60,
A1;
hence
||.(fx
. y).||
<= ((
||.BLp.||
*
||.x.||)
*
||.y.||) by
Th32;
end;
A79:
||.(f
. x).||
= (
upper_bound (
PreNorms fx)) by
LOPBAN_1: 30;
now
let s be
Real;
assume s
in (
PreNorms fx);
then
consider y be
Point of Y such that
A80: s
=
||.(fx
. y).|| and
A81:
||.y.||
<= 1;
A82:
||.(fx
. y).||
<= ((
||.BLp.||
*
||.x.||)
*
||.y.||) by
A78;
((
||.BLp.||
*
||.x.||)
*
||.y.||)
<= ((
||.BLp.||
*
||.x.||)
* 1) by
A81,
XREAL_1: 66;
hence s
<= (
||.BLp.||
*
||.x.||) by
A80,
A82,
XXREAL_0: 2;
end;
hence
||.(f
. x).||
<= (
||.BLp.||
*
||.x.||) by
A79,
SEQ_4: 45;
end;
then
reconsider f as
Lipschitzian
LinearOperator of X, (
R_NormSpace_of_BoundedLinearOperators (Y,Z)) by
LOPBAN_1:def 8;
A83: f
in LXYZ by
LOPBAN_1:def 9;
take f;
thus thesis by
A60,
A83,
FUNCT_1: 49;
end;
then
A85: (
rng I)
= BXYZ by
FUNCT_2: 10;
for u be
Point of (
R_NormSpace_of_BoundedLinearOperators (X,(
R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
||.(I
. u).||
<= (1
*
||.u.||) by
A55;
then
reconsider I as
Lipschitzian
LinearOperator of (
R_NormSpace_of_BoundedLinearOperators (X,(
R_NormSpace_of_BoundedLinearOperators (Y,Z)))), (
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by
LOPBAN_1:def 8;
take I;
I is
one-to-one
onto by
A1,
A85,
FUNCT_1: 52,
FUNCT_2:def 3;
hence thesis by
A55;
end;