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

ex b_{1} being Function of (X . i),(product X) st

for r being object st r in X . i holds

b_{1} . r = x +* (i,r)

for b_{1}, b_{2} being Function of (X . i),(product X) st ( for r being object st r in X . i holds

b_{1} . r = x +* (i,r) ) & ( for r being object st r in X . i holds

b_{2} . r = x +* (i,r) ) holds

b_{1} = b_{2}

end;
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 for r being object st r in X . i holds

it . r = x +* (i,r);

ex b

for r being object st r in X . i holds

b

proof end;

uniqueness for b

b

b

b

proof 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_{4} being Function of (X . i),(product X) holds

( b_{4} = reproj (i,x) iff for r being object st r in X . i holds

b_{4} . r = x +* (i,r) );

for X being non-empty non empty FinSequence

for i being object

for x being Element of product X

for b

( b

b

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

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

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

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

ex b_{1} being Function of (X . i),(product X) ex x0 being Element of product (carr X) st

( x0 = x & b_{1} = reproj (i,x0) )

for b_{1}, b_{2} being Function of (X . i),(product X) st ex x0 being Element of product (carr X) st

( x0 = x & b_{1} = reproj (i,x0) ) & ex x0 being Element of product (carr X) st

( x0 = x & b_{2} = reproj (i,x0) ) holds

b_{1} = b_{2}
;

end;
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 x0 being Element of product (carr X) st

( x0 = x & it = reproj (i,x0) );

ex b

( x0 = x & b

proof end;

uniqueness for b

( x0 = x & b

( x0 = x & b

b

:: 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_{4} being Function of (X . i),(product X) holds

( b_{4} = reproj (i,x) iff ex x0 being Element of product (carr X) st

( x0 = x & b_{4} = reproj (i,x0) ) );

for X being RealLinearSpace-Sequence

for i being Element of dom X

for x being Element of (product X)

for b

( b

( x0 = x & b

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

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

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

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;

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

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;

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

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;

existence

ex b_{1} being Function of (product X),Y st b_{1} is Multilinear ;

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

proof end;

definition

let X be RealLinearSpace-Sequence;

let Y be RealLinearSpace;

mode MultilinearOperator of X,Y is Multilinear Function of (product X),Y;

end;
let Y be RealLinearSpace;

mode MultilinearOperator of X,Y is Multilinear Function of (product X),Y;

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

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)

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;

ex b_{1} being Subset of (RealVectSpace ( the carrier of (product X),Y)) st

for x being set holds

( x in b_{1} iff x is MultilinearOperator of X,Y )

for b_{1}, b_{2} being Subset of (RealVectSpace ( the carrier of (product X),Y)) st ( for x being set holds

( x in b_{1} iff x is MultilinearOperator of X,Y ) ) & ( for x being set holds

( x in b_{2} iff x is MultilinearOperator of X,Y ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is MultilinearOperator of X,Y );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def6 defines MultilinearOperators LOPBAN10:def 4 :

for X being RealLinearSpace-Sequence

for Y being RealLinearSpace

for b_{3} being Subset of (RealVectSpace ( the carrier of (product X),Y)) holds

( b_{3} = MultilinearOperators (X,Y) iff for x being set holds

( x in b_{3} iff x is MultilinearOperator of X,Y ) );

for X being RealLinearSpace-Sequence

for Y being RealLinearSpace

for b

( b

( x in b

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;

coherence

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

MultilinearOperators (X,Y) is linearly-closed

end;
let Y be RealLinearSpace;

coherence

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

proof end;

coherence MultilinearOperators (X,Y) is linearly-closed

proof end;

definition

let X be RealLinearSpace-Sequence;

let Y be RealLinearSpace;

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

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 ;

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

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;

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;

coherence

not R_VectorSpace_of_MultilinearOperators (X,Y) is empty ;

end;
let Y be RealLinearSpace;

coherence

not R_VectorSpace_of_MultilinearOperators (X,Y) is empty ;

registration

let X be RealLinearSpace-Sequence;

let Y be RealLinearSpace;

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

registration

let X be RealLinearSpace-Sequence;

let Y be RealLinearSpace;

coherence

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

end;
let Y be RealLinearSpace;

coherence

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

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

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

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

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

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)

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

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

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

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

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;

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

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;

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

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;

existence

ex b_{1} being Function of (product X),Y st b_{1} is Multilinear ;

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

proof end;

definition

let X be RealNormSpace-Sequence;

let Y be RealNormSpace;

mode MultilinearOperator of X,Y is Multilinear Function of (product X),Y;

end;
let Y be RealNormSpace;

mode MultilinearOperator of X,Y is Multilinear Function of (product X),Y;

definition

let X be RealNormSpace-Sequence;

let Y be RealNormSpace;

ex b_{1} being Subset of (RealVectSpace ( the carrier of (product X),Y)) st

for x being set holds

( x in b_{1} iff x is MultilinearOperator of X,Y )

for b_{1}, b_{2} being Subset of (RealVectSpace ( the carrier of (product X),Y)) st ( for x being set holds

( x in b_{1} iff x is MultilinearOperator of X,Y ) ) & ( for x being set holds

( x in b_{2} iff x is MultilinearOperator of X,Y ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is MultilinearOperator of X,Y );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def6 defines MultilinearOperators LOPBAN10:def 7 :

for X being RealNormSpace-Sequence

for Y being RealNormSpace

for b_{3} being Subset of (RealVectSpace ( the carrier of (product X),Y)) holds

( b_{3} = MultilinearOperators (X,Y) iff for x being set holds

( x in b_{3} iff x is MultilinearOperator of X,Y ) );

for X being RealNormSpace-Sequence

for Y being RealNormSpace

for b

( b

( x in b

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;

coherence

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

MultilinearOperators (X,Y) is linearly-closed

end;
let Y be RealNormSpace;

coherence

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

proof end;

coherence MultilinearOperators (X,Y) is linearly-closed

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

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;

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

definition

let X be RealNormSpace-Sequence;

let Y be RealNormSpace;

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

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 ;

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

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;

coherence

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

end;
let Y be RealNormSpace;

coherence

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

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

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

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

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

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)

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

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;

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

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

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

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

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

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

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

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

ex b_{1} 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_{1} = Product Nx )

for b_{1}, b_{2} 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_{1} = 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_{2} = Product Nx ) holds

b_{1} = b_{2}

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

ex b

( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & b

proof end;

uniqueness for b

( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & b

( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & b

b

proof end;

:: deftheorem DefNrPro defines NrProduct LOPBAN10:def 9 :

for X being RealNormSpace-Sequence

for x being Point of (product X)

for b_{3} being non negative Real holds

( b_{3} = 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_{3} = Product Nx ) );

for X being RealNormSpace-Sequence

for x being Point of (product X)

for b

( b

( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & b

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

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

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

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;

ex b_{1} being MultilinearOperator of X,Y st b_{1} is Lipschitzian

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

proof end;

definition

let X be RealNormSpace-Sequence;

let Y be RealNormSpace;

ex b_{1} being Subset of (R_VectorSpace_of_MultilinearOperators (X,Y)) st

for x being set holds

( x in b_{1} iff x is Lipschitzian MultilinearOperator of X,Y )

for b_{1}, b_{2} being Subset of (R_VectorSpace_of_MultilinearOperators (X,Y)) st ( for x being set holds

( x in b_{1} iff x is Lipschitzian MultilinearOperator of X,Y ) ) & ( for x being set holds

( x in b_{2} iff x is Lipschitzian MultilinearOperator of X,Y ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is Lipschitzian MultilinearOperator of X,Y );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def9 defines BoundedMultilinearOperators LOPBAN10:def 11 :

for X being RealNormSpace-Sequence

for Y being RealNormSpace

for b_{3} being Subset of (R_VectorSpace_of_MultilinearOperators (X,Y)) holds

( b_{3} = BoundedMultilinearOperators (X,Y) iff for x being set holds

( x in b_{3} iff x is Lipschitzian MultilinearOperator of X,Y ) );

for X being RealNormSpace-Sequence

for Y being RealNormSpace

for b

( b

( x in b

registration

let X be RealNormSpace-Sequence;

let Y be RealNormSpace;

coherence

not BoundedMultilinearOperators (X,Y) is empty

BoundedMultilinearOperators (X,Y) is linearly-closed

end;
let Y be RealNormSpace;

coherence

not BoundedMultilinearOperators (X,Y) is empty

proof end;

coherence BoundedMultilinearOperators (X,Y) is linearly-closed

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

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;

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

definition

let X be RealNormSpace-Sequence;

let Y be RealNormSpace;

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

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 ;

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

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;

for b_{1} being Element of (R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) holds

( b_{1} is Function-like & b_{1} is Relation-like )
;

end;
let Y be RealNormSpace;

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

coherence for b

( b

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

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

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

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

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)

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

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

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

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

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

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;

{ ||.(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

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

{ ||.(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;

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

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

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 )

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

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

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

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)

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)

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

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

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 )

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;

ex b_{1} being Function of (BoundedMultilinearOperators (X,Y)),REAL st

for x being object st x in BoundedMultilinearOperators (X,Y) holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X,Y)))

for b_{1}, b_{2} being Function of (BoundedMultilinearOperators (X,Y)),REAL st ( for x being object st x in BoundedMultilinearOperators (X,Y) holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in BoundedMultilinearOperators (X,Y) holds

b_{2} . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds

b_{1} = b_{2}

end;
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 for x being object st x in BoundedMultilinearOperators (X,Y) holds

it . x = upper_bound (PreNorms (modetrans (x,X,Y)));

ex b

for x being object st x in BoundedMultilinearOperators (X,Y) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines BoundedMultilinearOperatorsNorm LOPBAN10:def 15 :

for X being RealNormSpace-Sequence

for Y being RealNormSpace

for b_{3} being Function of (BoundedMultilinearOperators (X,Y)),REAL holds

( b_{3} = BoundedMultilinearOperatorsNorm (X,Y) iff for x being object st x in BoundedMultilinearOperators (X,Y) holds

b_{3} . x = upper_bound (PreNorms (modetrans (x,X,Y))) );

for X being RealNormSpace-Sequence

for Y being RealNormSpace

for b

( b

b

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;

reducibility

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

end;
let Y be RealNormSpace;

let f be Lipschitzian MultilinearOperator of X,Y;

reducibility

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

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)

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;

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

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 ;

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

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

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)

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

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

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;

for b_{1} being Element of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds

( b_{1} is Function-like & b_{1} is Relation-like )
;

end;
let Y be RealNormSpace;

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

coherence for b

( b

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

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

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

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

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

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

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;

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

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

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;