:: Multilinear Operator and Its Basic Properties
:: by Kazuhisa Nakasho
::
:: Copyright (c) 2019 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),() means :Def1: :: LOPBAN10:def 1
for r being object st r in X . i holds
it . r = x +* (i,r);
existence
ex b1 being Function of (X . i),() st
for r being object st r in X . i holds
b1 . r = x +* (i,r)
proof end;
uniqueness
for b1, b2 being Function of (X . i),() st ( for r being object st r in X . i holds
b1 . r = x +* (i,r) ) & ( for r being object st r in X . i holds
b2 . r = x +* (i,r) ) holds
b1 = b2
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 b4 being Function of (X . i),() holds
( b4 = reproj (i,x) iff for r being object st r in X . i holds
b4 . 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 ();
func reproj (i,x) -> Function of (X . i),() means :Def20: :: LOPBAN10:def 2
ex x0 being Element of product (carr X) st
( x0 = x & it = reproj (i,x0) );
existence
ex b1 being Function of (X . i),() ex x0 being Element of product (carr X) st
( x0 = x & b1 = reproj (i,x0) )
proof end;
uniqueness
for b1, b2 being Function of (X . i),() st ex x0 being Element of product (carr X) st
( x0 = x & b1 = reproj (i,x0) ) & ex x0 being Element of product (carr X) st
( x0 = x & b2 = reproj (i,x0) ) holds
b1 = b2
;
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 ()
for b4 being Function of (X . i),() holds
( b4 = reproj (i,x) iff ex x0 being Element of product (carr X) st
( x0 = x & b4 = 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 ()
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 ()
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 ()
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 (),Y;
attr f is Multilinear means :Def3: :: LOPBAN10:def 3
for i being Element of dom X
for x being Element of () 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 (),Y holds
( f is Multilinear iff for i being Element of dom X
for x being Element of () 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 () -defined the carrier of Y -valued Function-like non empty total quasi_total Multilinear for Element of K19(K20( the carrier of (), the carrier of Y));
correctness
existence
ex b1 being Function of (),Y st b1 is Multilinear
;
proof end;
end;

definition 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 ()
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 ()
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 = () * (g . t)
proof end;

definition
let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;
func MultilinearOperators (X,Y) -> Subset of (RealVectSpace ( the carrier of (),Y)) means :Def6: :: LOPBAN10:def 4
for x being set holds
( x in it iff x is MultilinearOperator of X,Y );
existence
ex b1 being Subset of (RealVectSpace ( the carrier of (),Y)) st
for x being set holds
( x in b1 iff x is MultilinearOperator of X,Y )
proof end;
uniqueness
for b1, b2 being Subset of (RealVectSpace ( the carrier of (),Y)) st ( for x being set holds
( x in b1 iff x is MultilinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is MultilinearOperator of X,Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines MultilinearOperators LOPBAN10:def 4 :
for X being RealLinearSpace-Sequence
for Y being RealLinearSpace
for b3 being Subset of (RealVectSpace ( the carrier of (),Y)) holds
( b3 = MultilinearOperators (X,Y) iff for x being set holds
( x in b3 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;
coherence
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 (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #);
coherence
RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),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 (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),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 (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #) is Subspace of RealVectSpace ( the carrier of (),Y) by RSSPACE:11;

registration
let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;
coherence
not R_VectorSpace_of_MultilinearOperators (X,Y) is empty
;
end;

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

registration
let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;
coherence by MONOID_0:80;
end;

definition
let X be RealLinearSpace-Sequence;
let Y be RealLinearSpace;
let f be Element of ;
let v be VECTOR of ();
:: 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 holds
( h = f + g iff for x being VECTOR of () 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
for a being Real holds
( h = a * f iff for x being VECTOR of () holds h . x = a * (f . x) )
proof end;

theorem :: LOPBAN10:13
for X being RealLinearSpace-Sequence
for Y being RealLinearSpace holds 0. = the carrier of () --> (0. Y)
proof end;

theorem :: LOPBAN10:14
for X being RealLinearSpace-Sequence
for Y being RealLinearSpace holds the carrier of () --> (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 () 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 ()
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 ()
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 ()
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 (),Y;
attr f is Multilinear means :Def3: :: LOPBAN10:def 6
for i being Element of dom X
for x being Element of () 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 (),Y holds
( f is Multilinear iff for i being Element of dom X
for x being Element of () 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 () -defined the carrier of Y -valued Function-like non empty total quasi_total Multilinear for Element of K19(K20( the carrier of (), the carrier of Y));
correctness
existence
ex b1 being Function of (),Y st b1 is Multilinear
;
proof end;
end;

definition end;

definition
let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
func MultilinearOperators (X,Y) -> Subset of (RealVectSpace ( the carrier of (),Y)) means :Def6: :: LOPBAN10:def 7
for x being set holds
( x in it iff x is MultilinearOperator of X,Y );
existence
ex b1 being Subset of (RealVectSpace ( the carrier of (),Y)) st
for x being set holds
( x in b1 iff x is MultilinearOperator of X,Y )
proof end;
uniqueness
for b1, b2 being Subset of (RealVectSpace ( the carrier of (),Y)) st ( for x being set holds
( x in b1 iff x is MultilinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is MultilinearOperator of X,Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines MultilinearOperators LOPBAN10:def 7 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for b3 being Subset of (RealVectSpace ( the carrier of (),Y)) holds
( b3 = MultilinearOperators (X,Y) iff for x being set holds
( x in b3 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;
coherence
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 (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #) is Subspace of RealVectSpace ( the carrier of (),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 (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),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 (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #) is Abelian & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #) is add-associative & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #) is right_zeroed & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #) is right_complementable & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #) is vector-distributive & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #) is scalar-distributive & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #) is scalar-associative & RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #) is scalar-unital )
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 (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #);
coherence
RLSStruct(# (MultilinearOperators (X,Y)),(Zero_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),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 (),Y)))),(Add_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))),(Mult_ ((MultilinearOperators (X,Y)),(RealVectSpace ( the carrier of (),Y)))) #);

registration
let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
coherence by MONOID_0:80;
end;

definition
let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let f be Element of ;
let v be VECTOR of ();
:: 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 holds
( h = f + g iff for x being VECTOR of () 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
for a being Real holds
( h = a * f iff for x being VECTOR of () holds h . x = a * (f . x) )
proof end;

theorem Th18: :: LOPBAN10:21
for X being RealNormSpace-Sequence
for Y being RealNormSpace holds 0. = the carrier of () --> (0. Y)
proof end;

theorem Th19: :: LOPBAN10:22
for X being RealNormSpace-Sequence
for Y being RealNormSpace holds the carrier of () --> (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 ();
:: 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;
coherence ;
end;

definition
let X be RealNormSpace-Sequence;
let x be Point of ();
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 (carr G)
proof end;

theorem EXTh12: :: LOPBAN10:23
for G being RealNormSpace-Sequence
for p, q, r being Point of () 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 ()
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 () holds
( 0. () = 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 () 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 ();
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 b1 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).|| ) & b1 = Product Nx )
proof end;
uniqueness
for b1, b2 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).|| ) & b1 = 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).|| ) & b2 = Product Nx ) holds
b1 = b2
proof end;
end;

:: deftheorem DefNrPro defines NrProduct LOPBAN10:def 9 :
for X being RealNormSpace-Sequence
for x being Point of ()
for b3 being non negative Real holds
( b3 = 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).|| ) & b3 = Product Nx ) );

theorem :: LOPBAN10:27
for X being RealNormSpace-Sequence
for x being Point of () 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 () holds ||.(IT . x).|| <= K * () ) );
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 () holds ||.(IT . x).|| <= K * () ) ) );

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 () 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 () -defined the carrier of Y -valued Function-like non empty total quasi_total Multilinear Lipschitzian for Element of K19(K20( the carrier of (), the carrier of Y));
existence
ex b1 being MultilinearOperator of X,Y st b1 is Lipschitzian
proof end;
end;

definition
let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
func BoundedMultilinearOperators (X,Y) -> Subset of means :Def9: :: LOPBAN10:def 11
for x being set holds
( x in it iff x is Lipschitzian MultilinearOperator of X,Y );
existence
ex b1 being Subset of st
for x being set holds
( x in b1 iff x is Lipschitzian MultilinearOperator of X,Y )
proof end;
uniqueness
for b1, b2 being Subset of st ( for x being set holds
( x in b1 iff x is Lipschitzian MultilinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is Lipschitzian MultilinearOperator of X,Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines BoundedMultilinearOperators LOPBAN10:def 11 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for b3 being Subset of holds
( b3 = BoundedMultilinearOperators (X,Y) iff for x being set holds
( x in b3 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;
coherence
proof end;
end;

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

registration
let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
coherence
( RLSStruct(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #) is Abelian & RLSStruct(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #) is add-associative & RLSStruct(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #) is right_zeroed & RLSStruct(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #) is right_complementable & RLSStruct(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #) is vector-distributive & RLSStruct(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #) is scalar-distributive & RLSStruct(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #) is scalar-associative & RLSStruct(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #) is scalar-unital )
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(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #);
coherence
RLSStruct(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #) 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(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)) #);

registration
let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
cluster -> Relation-like Function-like for Element of the carrier of ;
coherence
for b1 being Element of holds
( b1 is Function-like & b1 is Relation-like )
;
end;

definition
let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let f be Element of ;
let v be VECTOR of ();
:: 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 holds
( h = f + g iff for x being VECTOR of () 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
for a being Real holds
( h = a * f iff for x being VECTOR of () holds h . x = a * (f . x) )
proof end;

theorem Th26: :: LOPBAN10:32
for X being RealNormSpace-Sequence
for Y being RealNormSpace holds 0. = the carrier of () --> (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 ;
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 () : for i being Element of dom X holds ||.(t . i).|| <= 1 } ;
coherence
{ ||.(u . t).|| where t is VECTOR of () : 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 () : for i being Element of dom X holds ||.(t . i).|| <= 1 } ;

theorem :: LOPBAN10:33
for X being RealNormSpace-Sequence
for s being Element of () 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 () 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 () 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 () 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 ()
for a being FinSequence of REAL ex s1 being Point of () 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 () st ( for i being Element of dom X holds t1 . i = (a /. i) * (t . i) ) holds
g . t1 = () * (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 = () "

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 = () "
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 (),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 b1 being Function of (),REAL st
for x being object st x in BoundedMultilinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
proof end;
uniqueness
for b1, b2 being Function of (),REAL st ( for x being object st x in BoundedMultilinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in BoundedMultilinearOperators (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines BoundedMultilinearOperatorsNorm LOPBAN10:def 15 :
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for b3 being Function of (),REAL holds
( b3 = BoundedMultilinearOperatorsNorm (X,Y) iff for x being object st x in BoundedMultilinearOperators (X,Y) holds
b3 . 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 () . f = upper_bound ()
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(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)),() #);
coherence
NORMSTR(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)),() #) 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(# (),(Zero_ ((),)),(Add_ ((),)),(Mult_ ((),)),() #);

theorem Th31: :: LOPBAN10:44
for X being RealNormSpace-Sequence
for Y being RealNormSpace holds the carrier of () --> (0. Y) = 0.
proof end;

theorem Th32: :: LOPBAN10:45
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Point of
for g being Lipschitzian MultilinearOperator of X,Y st g = f holds
for t being VECTOR of () holds ||.(g . t).|| <= * ()
proof end;

theorem Th33: :: LOPBAN10:46
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Point of holds 0 <=
proof end;

theorem Th34: :: LOPBAN10:47
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being Point of st f = 0. holds
0 =
proof end;

registration
let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
cluster -> Relation-like Function-like for Element of the carrier of ;
coherence
for b1 being Element of holds
( b1 is Function-like & b1 is Relation-like )
;
end;

definition
let X be RealNormSpace-Sequence;
let Y be RealNormSpace;
let f be Element of ;
let v be VECTOR of ();
:: 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 holds
( h = f + g iff for x being VECTOR of () 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
for a being Real holds
( h = a * f iff for x being VECTOR of () 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
for a being Real holds
( ( = 0 implies f = 0. ) & ( f = 0. implies = 0 ) & ||.(a * f).|| = |.a.| * & ||.(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;
coherence by Th39;
end;

theorem :: LOPBAN10:52
for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f, g, h being Point of holds
( h = f - g iff for x being VECTOR of () holds h . x = (f . x) - (g . x) )
proof end;