:: The Product Space of Real Normed Spaces and Its Properties
:: by Noboru Endou , Yasunari Shidama and Keiichi Miyajima
::
:: Received July 9, 2007
:: Copyright (c) 2007-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SEQ_1, SUBSET_1, NUMBERS, FUNCT_1, COMPLEX1, ARYTM_1, SEQ_2,
ORDINAL2, CARD_1, ARYTM_3, XXREAL_0, FINSEQ_1, NAT_1, RVSUM_1, SQUARE_1,
RELAT_1, CARD_3, FINSEQ_2, ZFMISC_1, MCART_1, PRVECT_1, XBOOLE_0,
RLVECT_1, GROUP_2, STRUCT_0, ALGSTR_0, BINOP_1, VECTSP_1, REAL_1,
SUPINF_2, FUNCT_6, FINSEQOP, SETWISEO, NORMSP_1, TARSKI, PRE_TOPC,
EUCLID, FUNCT_2, REAL_NS1, REWRITE1, RSSPACE3, PRVECT_2, NORMSP_0,
METRIC_1, RELAT_2, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_3, XCMPLX_0,
XXREAL_0, NUMBERS, XREAL_0, COMPLEX1, NAT_1, RELAT_1, FUNCT_1, RVSUM_1,
STRUCT_0, ALGSTR_0, FUNCT_2, FUNCT_3, BINOP_1, REAL_1, SEQ_1, COMSEQ_2,
SEQ_2, RLVECT_1, VECTSP_1, SETWISEO, FINSEQ_1, FINSEQ_2, FINSEQOP,
SQUARE_1, PRE_TOPC, EUCLID, PRVECT_1, NORMSP_0, NORMSP_1, RSSPACE3,
LOPBAN_1, REAL_NS1;
constructors FUNCT_3, FINSEQOP, REAL_1, SEQ_2, COMPLEX1, SQUARE_1, BINOP_2,
SETWISEO, PRVECT_1, RSSPACE3, LOPBAN_1, REAL_NS1, RVSUM_1, NORMSP_1,
RELSET_1, COMSEQ_2, NUMBERS;
registrations STRUCT_0, FINSEQ_2, FINSEQ_1, CARD_3, RLVECT_1, PRVECT_1,
XREAL_0, MEMBERED, NORMSP_1, REAL_NS1, ORDINAL1, FUNCT_1, FUNCT_2,
RELAT_1, XBOOLE_0, NUMBERS, VALUED_0, NORMSP_0, CARD_1, EUCLID, SQUARE_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: The Product Space of Real Linear Spaces
theorem :: PRVECT_2:1
for s,t be Real_Sequence, g be Real st for n be Element of NAT
holds t.n = |.s.n-g.| holds s is convergent & lim s = g iff t is convergent &
lim t = 0;
theorem :: PRVECT_2:2
for x,y be FinSequence of REAL st len x = len y & for i be
Element of NAT st i in Seg len x holds 0 <= x.i & x.i <= y.i holds |.x.| <= |.y
.|;
theorem :: PRVECT_2:3
for F be FinSequence of REAL st for i be Element of NAT st i in
dom F holds F.i = 0 holds Sum F = 0;
definition
let f be Function;
let X be set;
mode MultOps of X,f -> Function means
:: PRVECT_2:def 1
dom it = dom f & for i being
set st i in dom f holds it.i is Function of [:X,f.i:],f.i;
end;
registration
let F be Domain-Sequence;
let X be set;
cluster -> FinSequence-like for MultOps of X,F;
end;
theorem :: PRVECT_2:4
for X be set, F be Domain-Sequence, p be FinSequence holds (p is
MultOps of X,F iff len p = len F & for i be set st i in dom F holds p.i is
Function of [:X,F.i:],F.i);
definition
let F be Domain-Sequence;
let X be set;
let p be MultOps of X,F;
let i be Element of dom F;
redefine func p.i -> Function of [:X,F.i:],F.i;
end;
theorem :: PRVECT_2:5
for X be non empty set, F be Domain-Sequence, f,g being Function
of [:X,product F:],product F st for x be Element of X, d being Element of
product F, i being Element of dom F holds (f.(x,d)).i = (g.(x,d)).i holds f = g
;
definition
let F be Domain-Sequence;
let X be non empty set;
let p be MultOps of X,F;
func [:p:] -> Function of [:X,product F:],product F means
:: PRVECT_2:def 2
for x be
Element of X, d being Element of product F, i being Element of dom F holds (it.
(x,d)).i = (p.i).(x,d.i);
end;
definition
let R be Relation;
attr R is RealLinearSpace-yielding means
:: PRVECT_2:def 3
for S be set st S in rng R holds S is RealLinearSpace;
end;
registration
cluster non empty RealLinearSpace-yielding for FinSequence;
end;
definition
mode RealLinearSpace-Sequence is non empty RealLinearSpace-yielding
FinSequence;
end;
definition
let G be RealLinearSpace-Sequence;
let j be Element of dom G;
redefine func G.j -> RealLinearSpace;
end;
definition
let G be RealLinearSpace-Sequence;
func carr G -> Domain-Sequence means
:: PRVECT_2:def 4
len it = len G & for j be Element of dom G holds it.j = the carrier of G.j;
end;
definition
let G be RealLinearSpace-Sequence, j be Element of dom carr G;
redefine func G.j -> RealLinearSpace;
end;
definition
let G be RealLinearSpace-Sequence;
func addop G -> BinOps of carr G means
:: PRVECT_2:def 5
len it = len carr G & for j be
Element of dom carr G holds it.j = the addF of G.j;
func complop G -> UnOps of carr G means
:: PRVECT_2:def 6
len it = len carr G & for j be Element of dom carr G holds it.j = comp G.j;
func zeros G -> Element of product carr G means
:: PRVECT_2:def 7
for j be Element of dom carr G holds it.j = the ZeroF of G.j;
func multop G -> MultOps of REAL,carr G means
:: PRVECT_2:def 8
len it = len carr G &
for j be Element of dom carr G holds it.j = the Mult of G.j;
end;
definition
let G be RealLinearSpace-Sequence;
func product G -> strict non empty RLSStruct equals
:: PRVECT_2:def 9
RLSStruct(# product carr
G,zeros G,[:addop G :],[:multop G:] #);
end;
registration
let G be RealLinearSpace-Sequence;
cluster product G -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
end;
begin :: The Product Space of Real Normed Spaces
definition
let R be Relation;
attr R is RealNormSpace-yielding means
:: PRVECT_2:def 10
for x be set st x in rng R holds x is RealNormSpace;
end;
registration
cluster non empty RealNormSpace-yielding for FinSequence;
end;
definition
mode RealNormSpace-Sequence is non empty RealNormSpace-yielding FinSequence;
end;
definition
let G be RealNormSpace-Sequence;
let j be Element of dom G;
redefine func G.j -> RealNormSpace;
end;
registration
cluster RealNormSpace-yielding -> RealLinearSpace-yielding for FinSequence;
end;
definition
let G be RealNormSpace-Sequence;
let x be Element of product carr G;
func normsequence(G,x) -> Element of REAL len G means
:: PRVECT_2:def 11
len it = len G
& for j be Element of dom G holds it.j=(the normF of G.j).(x.j);
end;
definition
let G be RealNormSpace-Sequence;
func productnorm G -> Function of product carr (G qua
RealLinearSpace-Sequence),REAL means
:: PRVECT_2:def 12
for x being Element of product carr G holds it.x = |.normsequence(G,x).|;
end;
definition
let G be RealNormSpace-Sequence;
func product G -> strict non empty NORMSTR means
:: PRVECT_2:def 13
the RLSStruct of it
= product (G qua RealLinearSpace-Sequence) & the normF of it = productnorm G;
end;
reserve G for RealNormSpace-Sequence;
theorem :: PRVECT_2:6
product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop
G:], productnorm G #);
theorem :: PRVECT_2:7
for x be VECTOR of product G, y be Element of product carr G st x
= y holds ||.x.|| = |.normsequence(G,y).|;
theorem :: PRVECT_2:8
for x,y,z be Element of product carr G, i be Element of NAT st i
in dom x & z = [:addop G :].(x,y) holds normsequence(G,z).i <= (normsequence(G,
x) + normsequence(G,y)).i;
theorem :: PRVECT_2:9
for x be Element of product carr G, i be Element of NAT st i in
dom x holds 0 <= normsequence(G,x).i;
registration
let G be RealNormSpace-Sequence;
cluster product G -> reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
end;
theorem :: PRVECT_2:10
for G be RealNormSpace-Sequence, i be Element of dom G, x be
Point of product G, y be Element of product carr G, xi be Point of G.i st y = x
& xi = y.i holds ||.xi.|| <= ||.x.||;
theorem :: PRVECT_2:11
for G be RealNormSpace-Sequence, i be Element of dom G, x,y be
Point of product G, xi,yi be Point of G.i, zx,zy be Element of product carr G
st xi=zx.i & zx=x & yi=zy.i & zy=y holds ||.yi - xi.|| <= ||.y - x.||;
theorem :: PRVECT_2:12
for G be RealNormSpace-Sequence, seq be sequence of product G, x0 be
Point of product G, y0 be Element of product carr G st x0 = y0 & seq is
convergent & lim seq=x0 holds for i be Element of dom G ex seqi be sequence of
G.i st seqi is convergent & y0.i = lim seqi & for m be Element of NAT holds ex
seqm be Element of product carr G st seqm= seq.m & seqi.m=seqm.i;
theorem :: PRVECT_2:13
for G be RealNormSpace-Sequence, seq be sequence of (product G),
x0 be Point of product G, y0 be Element of product carr G st x0=y0 & for i be
Element of dom G ex seqi be sequence of G.i st seqi is convergent & y0.i = lim
seqi & for m be Element of NAT holds ex seqm be Element of product carr G st
seqm= seq.m & seqi.m=seqm.i holds seq is convergent & lim seq=x0;
theorem :: PRVECT_2:14
for G be RealNormSpace-Sequence st for i be Element of dom G holds G.i
is complete holds product G is complete;