LOPBAN11: Continuity of Multilinear Operator on Normed Linear Spaces

:: Continuity of Multilinear Operator on Normed Linear Spaces
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received February 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

theorem NDIFF825: :: LOPBAN11:1

for n being Nat
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r )

proof end;

theorem LM03: :: LOPBAN11:2

for R1, R2 being FinSequence of REAL
for n, i being Nat
for r being Real st i in dom R1 & R1 = n |-> 1 & R2 = R1 +* (i,r) holds
Product R2 = r

proof end;

theorem :: LOPBAN11:3

for F being FinSequence of REAL st ( for k being Element of NAT st k in dom F holds
0 <= F . k ) holds
0 <= Product F

proof end;

theorem DCARXX: :: LOPBAN11:4

for X being RealNormSpace-Sequence holds dom (carr X) = dom X

proof end;

theorem ZERXI: :: LOPBAN11:5

for X being RealNormSpace-Sequence
for z being Element of (product X) st z = 0. (product X) holds
for i being Element of dom X holds z . i = 0. (X . i)

proof end;

theorem FXZER: :: LOPBAN11:6

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being MultilinearOperator of X,Y holds f . (0. (product X)) = 0. Y

proof end;

theorem PSPROD: :: LOPBAN11:7

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 Th42: :: LOPBAN11:8

for X being RealNormSpace-Sequence
for Y being RealNormSpace st Y is complete holds
for seq being sequence of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent

proof end;

theorem Th43: :: LOPBAN11:9

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

proof end;

registration

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

cluster R_NormSpace_of_BoundedMultilinearOperators (X,Y) -> complete ;

coherence by Th43;

end;

theorem NDIFF823: :: LOPBAN11:10

for n being Nat
for F being Element of REAL n
for s being Real st ( for i being Nat st i in dom F holds
( 0 <= F . i & F . i <= s ) ) holds
|.F.| <= sqrt ((s * s) * (len F))

proof end;

theorem LM02: :: LOPBAN11:11

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being MultilinearOperator of X,Y
for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds
for v0, v1 being Point of (product X)
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) holds
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

proof end;

theorem LM01: :: LOPBAN11:12

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being MultilinearOperator of X,Y
for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds
for v0 being Point of (product X) ex M being Real st
( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds
ex F being FinSequence of REAL st
( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

proof end;

theorem NDIFF824: :: LOPBAN11:13

for X being RealNormSpace-Sequence
for x being Point of (product X)
for r being Real st 0 < r holds
ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st
( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )

proof end;

theorem :: LOPBAN11:14

for X being RealNormSpace-Sequence
for Y being RealNormSpace
for f being MultilinearOperator of X,Y holds
( ( f is_continuous_on the carrier of (product X) implies f is_continuous_in 0. (product X) ) & ( f is_continuous_in 0. (product X) implies f is_continuous_on the carrier of (product X) ) & ( f is_continuous_on the carrier of (product X) implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of (product X) ) )

proof end;