:: Multilinear Operator and Its Basic Properties
:: by Kazuhisa Nakasho
::
:: Received February 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

definition

let X be non-empty non empty FinSequence;
let i be object ;
let x be Element of product X;

func reproj (i,x) -> Function of (X . i),(product X) means :Def1: :: LOPBAN10:def 1
for r being object st r in X . i holds
it . r = x +* (i,r);

existence
ex b₁ being Function of (X . i),(product X) st
for r being object st r in X . i holds
b₁ . r = x +* (i,r)

proof end;

uniqueness
for b₁, b₂ being Function of (X . i),(product X) st ( for r being object st r in X . i holds
b₁ . r = x +* (i,r) ) & ( for r being object st r in X . i holds
b₂ . r = x +* (i,r) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines reproj LOPBAN10:def 1 :
for X being non-empty non empty FinSequence
for i being object
for x being Element of product X
for b₄ being Function of (X . i),(product X) holds
( b₄ = reproj (i,x) iff for r being object st r in X . i holds
b₄ . r = x +* (i,r) );

theorem Th1: :: LOPBAN10:1

for X being non-empty non empty FinSequence
for x being Element of product X
for i being Element of dom X
for r being object st r in X . i holds
((reproj (i,x)) . r) . i = r

proof end;

theorem Th2: :: LOPBAN10:2

for X being non-empty non empty FinSequence
for x being Element of product X
for i, j being Element of dom X
for r being object st r in X . i & i <> j holds
((reproj (i,x)) . r) . j = x . j

proof end;

theorem Th2X: :: LOPBAN10:3

for X being non-empty non empty FinSequence
for x being Element of product X
for i being Element of dom X holds (reproj (i,x)) . (x . i) = x

proof end;

definition

let X be RealLinearSpace-Sequence;
let i be Element of dom X;
let x be Element of (product X);

func reproj (i,x) -> Function of (X . i),(product X) means :Def20: :: LOPBAN10:def 2
ex x0 being Element of product (carr X) st
( x0 = x & it = reproj (i,x0) );

existence
ex b₁ being Function of (X . i),(product X) ex x0 being Element of product (carr X) st
( x0 = x & b₁ = reproj (i,x0) )

proof end;

uniqueness
for b₁, b₂ being Function of (X . i),(product X) st ex x0 being Element of product (carr X) st
( x0 = x & b₁ = reproj (i,x0) ) & ex x0 being Element of product (carr X) st
( x0 = x & b₂ = reproj (i,x0) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def20 defines reproj LOPBAN10:def 2 :
for X being RealLinearSpace-Sequence
for i being Element of dom X
for x being Element of (product X)
for b₄ being Function of (X . i),(product X) holds
( b₄ = reproj (i,x) iff ex x0 being Element of product (carr X) st
( x0 = x & b₄ = reproj (i,x0) ) );

LemmaX: for X being RealLinearSpace-Sequence holds dom (carr X) = dom X

proof end;

theorem Th3: :: LOPBAN10:4

for X being RealLinearSpace-Sequence
for i being Element of dom X
for x being Element of (product X)
for r being Element of (X . i)
for F being Function st F = (reproj (i,x)) . r holds
F . i = r

proof end;

theorem Th4: :: LOPBAN10:5

for X being RealLinearSpace-Sequence
for i, j being Element of dom X
for x being Element of (product X)
for r being Element of (X . i)
for F, s being Function st F = (reproj (i,x)) . r & x = s & i <> j holds
F . j = s . j

proof end;

theorem Th4X: :: LOPBAN10:6

for X being RealLinearSpace-Sequence
for i being Element of dom X
for x being Element of (product X)
for s being Function st x = s holds
(reproj (i,x)) . (s . i) = x

proof end;

definition

let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;
let f be Function of (product X),Y;

attr f is Multilinear means :Def3: :: LOPBAN10:def 3
for i being Element of dom X
for x being Element of (product X) holds f * (reproj (i,x)) is LinearOperator of (X . i),Y;

end;

:: deftheorem Def3 defines Multilinear LOPBAN10:def 3 :
for X being RealLinearSpace-Sequence
for Y being RealLinearSpace
for f being Function of (product X),Y holds
( f is Multilinear iff for i being Element of dom X
for x being Element of (product X) holds f * (reproj (i,x)) is LinearOperator of (X . i),Y );

registration

let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;

cluster Relation-like the carrier of (product X) -defined the carrier of Y -valued Function-like non empty total quasi_total Multilinear for Element of K19(K20( the carrier of (product X), the carrier of Y));

correctness
existence
ex b₁ being Function of (product X),Y st b₁ is Multilinear ;

proof end;

end;

definition

let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;
mode MultilinearOperator of X,Y is Multilinear Function of (product X),Y;

end;

theorem LOPBAN73: :: LOPBAN10:7

for X, Y being RealLinearSpace
for f being LinearOperator of X,Y holds 0. Y = f . (0. X)

proof end;

theorem :: LOPBAN10:8

for X being RealLinearSpace-Sequence
for Y being RealLinearSpace
for g being MultilinearOperator of X,Y
for t being Point of (product X)
for s being Element of product (carr X) st s = t & ex i being Element of dom X st s . i = 0. (X . i) holds
g . t = 0. Y

proof end;

theorem :: LOPBAN10:9

for X being RealLinearSpace-Sequence
for Y being RealLinearSpace
for g being MultilinearOperator of X,Y
for a being FinSequence of REAL st dom a = dom X holds
for t, t1 being Point of (product X)
for s, s1 being Element of product (carr X) st t = s & t1 = s1 & ( for i being Element of dom X holds s1 . i = (a /. i) * (s . i) ) holds
g . t1 = (Product a) * (g . t)

proof end;

definition

let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;

func MultilinearOperators (X,Y) -> Subset of (RealVectSpace ( the carrier of (product X),Y)) means :Def6: :: LOPBAN10:def 4
for x being set holds
( x in it iff x is MultilinearOperator of X,Y );

existence
ex b₁ being Subset of (RealVectSpace ( the carrier of (product X),Y)) st
for x being set holds
( x in b₁ iff x is MultilinearOperator of X,Y )

proof end;

uniqueness
for b₁, b₂ being Subset of (RealVectSpace ( the carrier of (product X),Y)) st ( for x being set holds
( x in b₁ iff x is MultilinearOperator of X,Y ) ) & ( for x being set holds
( x in b₂ iff x is MultilinearOperator of X,Y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines MultilinearOperators LOPBAN10:def 4 :
for X being RealLinearSpace-Sequence
for Y being RealLinearSpace
for b₃ being Subset of (RealVectSpace ( the carrier of (product X),Y)) holds
( b₃ = MultilinearOperators (X,Y) iff for x being set holds
( x in b₃ iff x is MultilinearOperator of X,Y ) );

LM14: for X being RealLinearSpace
for x1, x2, x3, x4 being Point of X holds (x1 + x2) + (x3 + x4) = (x1 + x3) + (x2 + x4)

proof end;

registration

let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;

cluster MultilinearOperators (X,Y) -> functional non empty ;

coherence
( not MultilinearOperators (X,Y) is empty & MultilinearOperators (X,Y) is functional )

proof end;

cluster MultilinearOperators (X,Y) -> linearly-closed ;

coherence
MultilinearOperators (X,Y) is linearly-closed

proof end;

end;

definition

let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;

func R_VectorSpace_of_MultilinearOperators (X,Y) -> strict RLSStruct equals :: LOPBAN10:def 5
RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #);

coherence
RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is strict RLSStruct ;

end;

:: deftheorem defines R_VectorSpace_of_MultilinearOperators LOPBAN10:def 5 :
for X being RealLinearSpace-Sequence
for Y being RealLinearSpace holds R_VectorSpace_of_MultilinearOperators (X,Y) = RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #);

theorem :: LOPBAN10:10

for X being RealLinearSpace-Sequence
for Y being RealLinearSpace holds RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is Subspace of RealVectSpace ( the carrier of (product X),Y) by RSSPACE:11;

registration

let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;

cluster R_VectorSpace_of_MultilinearOperators (X,Y) -> non empty strict ;

coherence
not R_VectorSpace_of_MultilinearOperators (X,Y) is empty ;

end;

registration

let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;

cluster R_VectorSpace_of_MultilinearOperators (X,Y) -> right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( R_VectorSpace_of_MultilinearOperators (X,Y) is Abelian & R_VectorSpace_of_MultilinearOperators (X,Y) is add-associative & R_VectorSpace_of_MultilinearOperators (X,Y) is right_zeroed & R_VectorSpace_of_MultilinearOperators (X,Y) is right_complementable & R_VectorSpace_of_MultilinearOperators (X,Y) is vector-distributive & R_VectorSpace_of_MultilinearOperators (X,Y) is scalar-distributive & R_VectorSpace_of_MultilinearOperators (X,Y) is scalar-associative & R_VectorSpace_of_MultilinearOperators (X,Y) is scalar-unital ) by RSSPACE:11;

end;

registration

let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;

cluster R_VectorSpace_of_MultilinearOperators (X,Y) -> strict constituted-Functions ;

coherence
R_VectorSpace_of_MultilinearOperators (X,Y) is constituted-Functions by MONOID_0:80;

end;

definition

let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;
let f be Element of (R_VectorSpace_of_MultilinearOperators (X,Y));
let v be VECTOR of (product X);
:: original: .
redefine func f . v -> VECTOR of Y;
coherence
f . v is VECTOR of Y

proof end;

end;

theorem :: LOPBAN10:11

for X being RealLinearSpace-Sequence
for Y being RealLinearSpace
for f, g, h being VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of (product X) holds h . x = (f . x) + (g . x) )

proof end;

theorem :: LOPBAN10:12

for X being RealLinearSpace-Sequence
for Y being RealLinearSpace
for f, h being VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of (product X) holds h . x = a * (f . x) )

proof end;

theorem :: LOPBAN10:13

for X being RealLinearSpace-Sequence
for Y being RealLinearSpace holds 0. (R_VectorSpace_of_MultilinearOperators (X,Y)) = the carrier of (product X) --> (0. Y)

proof end;

theorem :: LOPBAN10:14

for X being RealLinearSpace-Sequence
for Y being RealLinearSpace holds the carrier of (product X) --> (0. Y) is MultilinearOperator of X,Y

proof end;

Def2: for X being RealNormSpace-Sequence
for i being Element of dom X
for x being Element of (product X) ex x0 being Element of product (carr X) st
( x0 = x & reproj (i,x) = reproj (i,x0) )

proof end;

theorem Th3: :: LOPBAN10:15

for X being RealNormSpace-Sequence
for i being Element of dom X
for x being Element of (product X)
for r being Element of (X . i)
for F being Function st F = (reproj (i,x)) . r holds
F . i = r

proof end;

theorem Th4: :: LOPBAN10:16

for X being RealNormSpace-Sequence
for i, j being Element of dom X
for x being Element of (product X)
for r being Element of (X . i)
for F, s being Function st F = (reproj (i,x)) . r & x = s & i <> j holds
F . j = s . j

proof end;

theorem Th4X: :: LOPBAN10:17

for X being RealNormSpace-Sequence
for i being Element of dom X
for x being Element of (product X)
for s being Function st x = s holds
(reproj (i,x)) . (s . i) = x

proof end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let f be Function of (product X),Y;

attr f is Multilinear means :Def3: :: LOPBAN10:def 6
for i being Element of dom X
for x being Element of (product X) holds f * (reproj (i,x)) is LinearOperator of (X . i),Y;

end;

:: deftheorem Def3 defines Multilinear LOPBAN10:def 6 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Function of (product X),Y holds
( f is Multilinear iff for i being Element of dom X
for x being Element of (product X) holds f * (reproj (i,x)) is LinearOperator of (X . i),Y );

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

cluster Relation-like the carrier of (product X) -defined the carrier of Y -valued Function-like non empty total quasi_total Multilinear for Element of K19(K20( the carrier of (product X), the carrier of Y));

correctness
existence
ex b₁ being Function of (product X),Y st b₁ is Multilinear ;

proof end;

end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
mode MultilinearOperator of X,Y is Multilinear Function of (product X),Y;

end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

func MultilinearOperators (X,Y) -> Subset of (RealVectSpace ( the carrier of (product X),Y)) means :Def6: :: LOPBAN10:def 7
for x being set holds
( x in it iff x is MultilinearOperator of X,Y );

existence
ex b₁ being Subset of (RealVectSpace ( the carrier of (product X),Y)) st
for x being set holds
( x in b₁ iff x is MultilinearOperator of X,Y )

proof end;

uniqueness
for b₁, b₂ being Subset of (RealVectSpace ( the carrier of (product X),Y)) st ( for x being set holds
( x in b₁ iff x is MultilinearOperator of X,Y ) ) & ( for x being set holds
( x in b₂ iff x is MultilinearOperator of X,Y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines MultilinearOperators LOPBAN10:def 7 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for b₃ being Subset of (RealVectSpace ( the carrier of (product X),Y)) holds
( b₃ = MultilinearOperators (X,Y) iff for x being set holds
( x in b₃ iff x is MultilinearOperator of X,Y ) );

LM14: for X being RealNormSpace
for x1, x2, x3, x4 being Point of X holds (x1 + x2) + (x3 + x4) = (x1 + x3) + (x2 + x4)

proof end;

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

cluster MultilinearOperators (X,Y) -> functional non empty ;

coherence
( not MultilinearOperators (X,Y) is empty & MultilinearOperators (X,Y) is functional )

proof end;

cluster MultilinearOperators (X,Y) -> linearly-closed ;

coherence
MultilinearOperators (X,Y) is linearly-closed

proof end;

end;

theorem :: LOPBAN10:18

for X being RealNormSpace-Sequence
for Y being RealNormSpace holds RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is Subspace of RealVectSpace ( the carrier of (product X),Y) by RSSPACE:11;

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

cluster RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is Abelian & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is add-associative & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is right_zeroed & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is right_complementable & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is vector-distributive & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is scalar-distributive & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is scalar-associative & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is scalar-unital ) by RSSPACE:11;

end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

func R_VectorSpace_of_MultilinearOperators (X,Y) -> strict RealLinearSpace equals :: LOPBAN10:def 8
RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #);

coherence
RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #) is strict RealLinearSpace ;

end;

:: deftheorem defines R_VectorSpace_of_MultilinearOperators LOPBAN10:def 8 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace holds R_VectorSpace_of_MultilinearOperators (X,Y) = RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (product X),Y)))) #);

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

cluster R_VectorSpace_of_MultilinearOperators (X,Y) -> strict constituted-Functions ;

coherence
R_VectorSpace_of_MultilinearOperators (X,Y) is constituted-Functions by MONOID_0:80;

end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let f be Element of (R_VectorSpace_of_MultilinearOperators (X,Y));
let v be VECTOR of (product X);
:: original: .
redefine func f . v -> VECTOR of Y;
coherence
f . v is VECTOR of Y

proof end;

end;

theorem Th16: :: LOPBAN10:19

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of (product X) holds h . x = (f . x) + (g . x) )

proof end;

theorem Th17: :: LOPBAN10:20

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f, h being VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of (product X) holds h . x = a * (f . x) )

proof end;

theorem Th18: :: LOPBAN10:21

for X being RealNormSpace-Sequence
for Y being RealNormSpace holds 0. (R_VectorSpace_of_MultilinearOperators (X,Y)) = the carrier of (product X) --> (0. Y)

proof end;

theorem Th19: :: LOPBAN10:22

for X being RealNormSpace-Sequence
for Y being RealNormSpace holds the carrier of (product X) --> (0. Y) is MultilinearOperator of X,Y

proof end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let IT be MultilinearOperator of X,Y;
let x be VECTOR of (product X);
:: original: .
redefine func IT . x -> Point of Y;
correctness
coherence
IT . x is Point of Y;

proof end;

end;

registration

let X be RealNormSpace-Sequence;

cluster product X -> constituted-Functions ;

coherence
product X is constituted-Functions ;

end;

definition

let X be RealNormSpace-Sequence;
let x be Point of (product X);
let i be Element of dom X;
:: original: .
redefine func x . i -> Point of (X . i);
correctness
coherence
x . i is Point of (X . i);

proof end;

end;

EXTh10: for G being RealNormSpace-Sequence holds the carrier of (product G) = product (carr G)

proof end;

theorem EXTh12: :: LOPBAN10:23

for G being RealNormSpace-Sequence
for p, q, r being Point of (product G) holds
( p + q = r iff for i being Element of dom G holds r . i = (p . i) + (q . i) )

proof end;

theorem EXTh13: :: LOPBAN10:24

for G being RealNormSpace-Sequence
for p, r being Point of (product G)
for a being Real holds
( a * p = r iff for i being Element of dom G holds r . i = a * (p . i) )

proof end;

theorem :: LOPBAN10:25

for G being RealNormSpace-Sequence
for p being Point of (product G) holds
( 0. (product G) = p iff for i being Element of dom G holds p . i = 0. (G . i) )

proof end;

theorem :: LOPBAN10:26

for G being RealNormSpace-Sequence
for p, q, r being Point of (product G) holds
( p - q = r iff for i being Element of dom G holds r . i = (p . i) - (q . i) )

proof end;

definition

let X be RealNormSpace-Sequence;
let x be Point of (product X);

func NrProduct x -> non negative Real means :DefNrPro: :: LOPBAN10:def 9
ex Nx being FinSequence of REAL st
( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & it = Product Nx );

existence
ex b₁ being non negative Real ex Nx being FinSequence of REAL st
( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & b₁ = Product Nx )

proof end;

uniqueness
for b₁, b₂ being non negative Real st ex Nx being FinSequence of REAL st
( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & b₁ = Product Nx ) & ex Nx being FinSequence of REAL st
( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & b₂ = Product Nx ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefNrPro defines NrProduct LOPBAN10:def 9 :
for X being RealNormSpace-Sequence
for x being Point of (product X)
for b₃ being non negative Real holds
( b₃ = NrProduct x iff ex Nx being FinSequence of REAL st
( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & b₃ = Product Nx ) );

theorem :: LOPBAN10:27

for X being RealNormSpace-Sequence
for x being Point of (product X) holds
( ( ex i being Element of dom X st x . i = 0. (X . i) implies NrProduct x = 0 ) & ( NrProduct x = 0 implies ex i being Element of dom X st x . i = 0. (X . i) ) & ( ( for i being Element of dom X holds not x . i = 0. (X . i) ) implies 0 < NrProduct x ) )

proof end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let IT be MultilinearOperator of X,Y;

attr IT is Lipschitzian means :Def8: :: LOPBAN10:def 10
ex K being Real st
( 0 <= K & ( for x being Point of (product X) holds ||.(IT . x).|| <= K * (NrProduct x) ) );

end;

:: deftheorem Def8 defines Lipschitzian LOPBAN10:def 10 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for IT being MultilinearOperator of X,Y holds
( IT is Lipschitzian iff ex K being Real st
( 0 <= K & ( for x being Point of (product X) holds ||.(IT . x).|| <= K * (NrProduct x) ) ) );

theorem Th21: :: LOPBAN10:28

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being MultilinearOperator of X,Y st ( for x being VECTOR of (product X) holds f . x = 0. Y ) holds
f is Lipschitzian

proof end;

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

cluster Relation-like the carrier of (product X) -defined the carrier of Y -valued Function-like non empty total quasi_total Multilinear Lipschitzian for Element of K19(K20( the carrier of (product X), the carrier of Y));

existence
ex b₁ being MultilinearOperator of X,Y st b₁ is Lipschitzian

proof end;

end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

func BoundedMultilinearOperators (X,Y) -> Subset of (R_VectorSpace_of_MultilinearOperators (X,Y)) means :Def9: :: LOPBAN10:def 11
for x being set holds
( x in it iff x is Lipschitzian MultilinearOperator of X,Y );

existence
ex b₁ being Subset of (R_VectorSpace_of_MultilinearOperators (X,Y)) st
for x being set holds
( x in b₁ iff x is Lipschitzian MultilinearOperator of X,Y )

proof end;

uniqueness
for b₁, b₂ being Subset of (R_VectorSpace_of_MultilinearOperators (X,Y)) st ( for x being set holds
( x in b₁ iff x is Lipschitzian MultilinearOperator of X,Y ) ) & ( for x being set holds
( x in b₂ iff x is Lipschitzian MultilinearOperator of X,Y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines BoundedMultilinearOperators LOPBAN10:def 11 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for b₃ being Subset of (R_VectorSpace_of_MultilinearOperators (X,Y)) holds
( b₃ = BoundedMultilinearOperators (X,Y) iff for x being set holds
( x in b₃ iff x is Lipschitzian MultilinearOperator of X,Y ) );

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

cluster BoundedMultilinearOperators (X,Y) -> non empty ;

coherence
not BoundedMultilinearOperators (X,Y) is empty

proof end;

cluster BoundedMultilinearOperators (X,Y) -> linearly-closed ;

coherence
BoundedMultilinearOperators (X,Y) is linearly-closed

proof end;

end;

theorem :: LOPBAN10:29

for X being RealNormSpace-Sequence
for Y being RealNormSpace holds RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is Subspace of R_VectorSpace_of_MultilinearOperators (X,Y) by RSSPACE:11;

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

cluster RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is Abelian & RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is add-associative & RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is right_zeroed & RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is right_complementable & RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is vector-distributive & RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is scalar-distributive & RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is scalar-associative & RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is scalar-unital ) by RSSPACE:11;

end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

func R_VectorSpace_of_BoundedMultilinearOperators (X,Y) -> strict RealLinearSpace equals :: LOPBAN10:def 12
RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #);

coherence
RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is strict RealLinearSpace ;

end;

:: deftheorem defines R_VectorSpace_of_BoundedMultilinearOperators LOPBAN10:def 12 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace holds R_VectorSpace_of_BoundedMultilinearOperators (X,Y) = RLSStruct(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))) #);

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

cluster -> Relation-like Function-like for Element of the carrier of (R_VectorSpace_of_BoundedMultilinearOperators (X,Y));

coherence
for b₁ being Element of (R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) holds
( b₁ is Function-like & b₁ is Relation-like ) ;

end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let f be Element of (R_VectorSpace_of_BoundedMultilinearOperators (X,Y));
let v be VECTOR of (product X);
:: original: .
redefine func f . v -> VECTOR of Y;
coherence
f . v is VECTOR of Y

proof end;

end;

theorem Th24: :: LOPBAN10:30

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of (product X) holds h . x = (f . x) + (g . x) )

proof end;

theorem Th25: :: LOPBAN10:31

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f, h being VECTOR of (R_VectorSpace_of_BoundedMultilinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of (product X) holds h . x = a * (f . x) )

proof end;

theorem Th26: :: LOPBAN10:32

for X being RealNormSpace-Sequence
for Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) = the carrier of (product X) --> (0. Y)

proof end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let f be object ;
assume A1: f in BoundedMultilinearOperators (X,Y) ;

func modetrans (f,X,Y) -> Lipschitzian MultilinearOperator of X,Y equals :Def11: :: LOPBAN10:def 13
f;

coherence
f is Lipschitzian MultilinearOperator of X,Y by A1, Def9;

end;

:: deftheorem Def11 defines modetrans LOPBAN10:def 13 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being object st f in BoundedMultilinearOperators (X,Y) holds
modetrans (f,X,Y) = f;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let u be MultilinearOperator of X,Y;

func PreNorms u -> non empty Subset of REAL equals :: LOPBAN10:def 14
{ ||.(u . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } ;

coherence
{ ||.(u . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } is non empty Subset of REAL

proof end;

end;

:: deftheorem defines PreNorms LOPBAN10:def 14 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for u being MultilinearOperator of X,Y holds PreNorms u = { ||.(u . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } ;

theorem :: LOPBAN10:33

for X being RealNormSpace-Sequence
for s being Element of (product X) ex F being FinSequence of REAL st
( dom F = dom X & ( for i being Element of dom X holds F . i = ||.(s . i).|| ) )

proof end;

theorem LM281: :: LOPBAN10:34

for F being FinSequence of REAL st ( for i being Element of dom F holds
( 0 <= F . i & F . i <= 1 ) ) holds
( 0 <= Product F & Product F <= 1 )

proof end;

theorem LM28: :: LOPBAN10:35

for X being RealNormSpace-Sequence
for x being Point of (product X) st ( for i being Element of dom X holds ||.(x . i).|| <= 1 ) holds
( 0 <= NrProduct x & NrProduct x <= 1 )

proof end;

LM31: for F being FinSequence of REAL st ( for i being Element of dom F holds F . i > 0 ) holds
Product F > 0

proof end;

theorem LM32: :: LOPBAN10:36

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for g being MultilinearOperator of X,Y
for t being Point of (product X) st ex i being Element of dom X st t . i = 0. (X . i) holds
g . t = 0. Y

proof end;

theorem LM34: :: LOPBAN10:37

for X being RealNormSpace-Sequence
for x being Point of (product X) ex d being FinSequence of REAL st
( dom d = dom X & ( for i being Element of dom X holds d . i = ||.(x . i).|| " ) )

proof end;

theorem LM33: :: LOPBAN10:38

for X being RealNormSpace-Sequence
for s being Point of (product X)
for a being FinSequence of REAL ex s1 being Point of (product X) st
for i being Element of dom X holds s1 . i = (a /. i) * (s . i)

proof end;

theorem LM35: :: LOPBAN10:39

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for g being MultilinearOperator of X,Y
for a being FinSequence of REAL st dom a = dom X holds
for t, t1 being Point of (product X) st ( for i being Element of dom X holds t1 . i = (a /. i) * (t . i) ) holds
g . t1 = (Product a) * (g . t)

proof end;

LM36A: for F, G being FinSequence of REAL st len F = len G & ( for i being Element of NAT st i in dom F holds
G . i = (F . i) " ) holds
Product G = (Product F) "

proof end;

theorem LM36: :: LOPBAN10:40

for F, G being FinSequence of REAL st dom F = dom G & ( for i being Element of dom F holds G . i = (F . i) " ) holds
Product G = (Product F) "

proof end;

theorem Th27: :: LOPBAN10:41

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for g being Lipschitzian MultilinearOperator of X,Y holds PreNorms g is bounded_above

proof end;

theorem :: LOPBAN10:42

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for g being MultilinearOperator of X,Y holds
( g is Lipschitzian iff PreNorms g is bounded_above )

proof end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

func BoundedMultilinearOperatorsNorm (X,Y) -> Function of (BoundedMultilinearOperators (X,Y)),REAL means :Def13: :: LOPBAN10:def 15
for x being object st x in BoundedMultilinearOperators (X,Y) holds
it . x = upper_bound (PreNorms (modetrans (x,X,Y)));

existence
ex b₁ being Function of (BoundedMultilinearOperators (X,Y)),REAL st
for x being object st x in BoundedMultilinearOperators (X,Y) holds
b₁ . x = upper_bound (PreNorms (modetrans (x,X,Y)))

proof end;

uniqueness
for b₁, b₂ being Function of (BoundedMultilinearOperators (X,Y)),REAL st ( for x being object st x in BoundedMultilinearOperators (X,Y) holds
b₁ . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in BoundedMultilinearOperators (X,Y) holds
b₂ . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines BoundedMultilinearOperatorsNorm LOPBAN10:def 15 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for b₃ being Function of (BoundedMultilinearOperators (X,Y)),REAL holds
( b₃ = BoundedMultilinearOperatorsNorm (X,Y) iff for x being object st x in BoundedMultilinearOperators (X,Y) holds
b₃ . x = upper_bound (PreNorms (modetrans (x,X,Y))) );

Th29: for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Lipschitzian MultilinearOperator of X,Y holds modetrans (f,X,Y) = f

proof end;

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let f be Lipschitzian MultilinearOperator of X,Y;

reduce modetrans (f,X,Y) to f;

reducibility
modetrans (f,X,Y) = f by Th29;

end;

theorem Th30: :: LOPBAN10:43

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Lipschitzian MultilinearOperator of X,Y holds (BoundedMultilinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)

proof end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

func R_NormSpace_of_BoundedMultilinearOperators (X,Y) -> non empty strict NORMSTR equals :: LOPBAN10:def 16
NORMSTR(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(BoundedMultilinearOperatorsNorm (X,Y)) #);

coherence
NORMSTR(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(BoundedMultilinearOperatorsNorm (X,Y)) #) is non empty strict NORMSTR ;

end;

:: deftheorem defines R_NormSpace_of_BoundedMultilinearOperators LOPBAN10:def 16 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace holds R_NormSpace_of_BoundedMultilinearOperators (X,Y) = NORMSTR(# (BoundedMultilinearOperators (X,Y)),(Zero_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Add_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(Mult_ ((BoundedMultilinearOperators (X,Y)),(R_VectorSpace_of_MultilinearOperators (X,Y)))),(BoundedMultilinearOperatorsNorm (X,Y)) #);

theorem Th31: :: LOPBAN10:44

for X being RealNormSpace-Sequence
for Y being RealNormSpace holds the carrier of (product X) --> (0. Y) = 0. (R_NormSpace_of_BoundedMultilinearOperators (X,Y))

proof end;

theorem Th32: :: LOPBAN10:45

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y))
for g being Lipschitzian MultilinearOperator of X,Y st g = f holds
for t being VECTOR of (product X) holds ||.(g . t).|| <= ||.f.|| * (NrProduct t)

proof end;

theorem Th33: :: LOPBAN10:46

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds 0 <= ||.f.||

proof end;

theorem Th34: :: LOPBAN10:47

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st f = 0. (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds
0 = ||.f.||

proof end;

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

cluster -> Relation-like Function-like for Element of the carrier of (R_NormSpace_of_BoundedMultilinearOperators (X,Y));

coherence
for b₁ being Element of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds
( b₁ is Function-like & b₁ is Relation-like ) ;

end;

definition

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let f be Element of (R_NormSpace_of_BoundedMultilinearOperators (X,Y));
let v be VECTOR of (product X);
:: original: .
redefine func f . v -> VECTOR of Y;
coherence
f . v is VECTOR of Y

proof end;

end;

theorem Th35: :: LOPBAN10:48

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of (product X) holds h . x = (f . x) + (g . x) )

proof end;

theorem Th36: :: LOPBAN10:49

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f, h being Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of (product X) holds h . x = a * (f . x) )

proof end;

theorem Th37: :: LOPBAN10:50

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y))
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

proof end;

Th38: for X being RealNormSpace-Sequence
for Y being RealNormSpace holds
( R_NormSpace_of_BoundedMultilinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is RealNormSpace-like )

proof end;

theorem Th39: :: LOPBAN10:51

for X being RealNormSpace-Sequence
for Y being RealNormSpace holds R_NormSpace_of_BoundedMultilinearOperators (X,Y) is RealNormSpace

proof end;

registration

let X be RealNormSpace-Sequence;
let Y be RealNormSpace;

cluster R_NormSpace_of_BoundedMultilinearOperators (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like ;

coherence
( R_NormSpace_of_BoundedMultilinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is RealNormSpace-like & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is vector-distributive & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is scalar-distributive & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is scalar-associative & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is scalar-unital & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is Abelian & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is add-associative & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is right_zeroed & R_NormSpace_of_BoundedMultilinearOperators (X,Y) is right_complementable ) by Th39;

end;

theorem :: LOPBAN10:52

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds
( h = f - g iff for x being VECTOR of (product X) holds h . x = (f . x) - (g . x) )

proof end;