:: by Kazuhisa Nakasho and Yasunari Shidama

::

:: Received February 27, 2019

:: Copyright (c) 2019 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 )

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

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

0 <= F . k ) holds

0 <= Product F

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)

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

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

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

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

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;

coherence

R_NormSpace_of_BoundedMultilinearOperators (X,Y) is complete by Th43;

end;
let Y be RealBanachSpace;

coherence

R_NormSpace_of_BoundedMultilinearOperators (X,Y) is complete by Th43;

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

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

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

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

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

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;