:: 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-2026 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, EUCLID, SQUARE_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions RLVECT_1, NORMSP_1, ALGSTR_0, NORMSP_0;
equalities RLVECT_1, FINSEQ_2, EUCLID, STRUCT_0, SQUARE_1, ALGSTR_0, NORMSP_0,
ORDINAL1;
expansions RLVECT_1, NORMSP_1;
theorems BINOP_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQOP,
SETWISEO, TARSKI, CARD_3, RLVECT_1, RELAT_1, RVSUM_1, ABSVALUE, FVSUM_1,
SEQ_2, PRVECT_1, NORMSP_1, SQUARE_1, EUCLID, XREAL_1, LOPBAN_1, RSSPACE3,
REAL_NS1, XXREAL_0, VALUED_1, XREAL_0, NORMSP_0, CARD_1, ORDINAL1;
schemes FUNCT_1, BINOP_1, FUNCT_2, FINSEQ_1, PRVECT_1, CLASSES1;
begin :: The Product Space of Real Linear Spaces
theorem
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
proof
let s,t be Real_Sequence, g be Real;
assume
A1: for n be Element of NAT holds t.n=|.s.n-g.|;
hereby
assume
A2: s is convergent & lim s = g;
A3: now
let r be Real;
assume 0 < r;
then consider n be Nat such that
A4: for m be Nat st n<=m holds |.s.m-g.| < r by A2,SEQ_2:def 7;
take n;
now
let m be Nat;
A5: m in NAT by ORDINAL1:def 12;
assume n<=m;
then |.|.s.m-g.|.| < r by A4;
hence |.t.m-0 .| < r by A1,A5;
end;
hence for m be Nat st n<=m holds |.t.m-0 .|< r;
end;
hence t is convergent by SEQ_2:def 6;
hence lim t = 0 by A3,SEQ_2:def 7;
end;
assume
A6: t is convergent & lim t = 0;
A7: now
let r be Real;
assume 0 < r;
then consider n be Nat such that
A8: for m be Nat st n<=m holds |.t.m-0 .| < r by A6,SEQ_2:def 7;
take n;
now
let m be Nat;
A9: m in NAT by ORDINAL1:def 12;
assume n<=m;
then |.t.m-0 .| < r by A8;
then |.|.s.m-g.|.| < r by A1,A9;
hence |.s.m-g.| < r;
end;
hence for m be Nat st n <= m holds |.s.m-g.| < r;
end;
hence s is convergent by SEQ_2:def 6;
hence thesis by A7,SEQ_2:def 7;
end;
theorem Th2:
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.|
proof
let x,y be FinSequence of REAL such that
A1: len x = len y and
A2: for i be Element of NAT st i in Seg len x holds 0 <= x.i & x.i <= y. i;
A3: for i be Nat st i in Seg len x holds (sqr x).i <= (sqr y).i
proof
let i be Nat;
assume i in Seg len x;
then
A4: 0 <= x.i & x.i <= y.i by A2;
(x.i)^2=(sqr x).i & (y.i)^2=(sqr y).i by VALUED_1:11;
hence thesis by A4,SQUARE_1:15;
end;
Seg len sqr y = dom sqr y & dom sqr y = dom y by FINSEQ_1:def 3,VALUED_1:11;
then
A5: len sqr y = len y by FINSEQ_1:def 3;
Seg len sqr x = dom sqr x & dom sqr x = dom x by FINSEQ_1:def 3,VALUED_1:11;
then
A6: len sqr x = len x by FINSEQ_1:def 3;
A7: 0 <= Sum sqr x by RVSUM_1:86;
sqr x is Element of (len sqr x)-tuples_on REAL & sqr y is Element of (
len sqr y)-tuples_on REAL by FINSEQ_2:92;
hence thesis by A1,A3,A6,A5,A7,RVSUM_1:82,SQUARE_1:26;
end;
theorem Th3:
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
proof
let F be FinSequence of REAL;
set i = len F;
set R1 = i|-> 0;
reconsider R2 = F as Element of i-tuples_on REAL by FINSEQ_2:92;
A1: Seg len F = dom F by FINSEQ_1:def 3;
assume
A2: for i be Element of NAT st i in dom F holds 0 = F.i;
A3: for j be Nat st j in Seg i holds R1.j = R2.j by A2,A1;
len R1 = i by CARD_1:def 7;
then dom R1 = dom R2 by FINSEQ_3:29;
then R1 = R2 by A1,A3,FINSEQ_1:13;
hence thesis by RVSUM_1:81;
end;
definition
let f be Function;
let X be set;
mode MultOps of X,f -> Function means
:Def1:
dom it = dom f &
for i being set st i in dom f holds it.i is Function of [:X,f.i:],f.i;
existence
proof
deffunc F(object) = pr2(X,f.$1);
consider g being Function such that
A1: dom g = dom f & for x be object st x in dom f holds g.x = F(x) from
FUNCT_1:sch 3;
take g;
thus dom g = dom f by A1;
let i be set;
assume i in dom f;
then g.i = pr2(X,f.i) by A1;
hence thesis;
end;
end;
registration
let F be Domain-Sequence;
let X be set;
cluster -> FinSequence-like for MultOps of X,F;
coherence
proof
let f be MultOps of X,F;
dom F = dom f & dom F = Seg len F by Def1,FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
end;
theorem Th4:
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)
proof
let X be set;
let F be Domain-Sequence;
let p be FinSequence;
dom p = dom F iff len p = len F by FINSEQ_3:29;
hence thesis by Def1;
end;
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; :: redefines . (FUNCT_1, definition)
coherence by Th4;
end;
theorem Th5:
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
proof
let X be non empty set;
let F be Domain-Sequence;
let f,g being Function of [:X,product F:],product F such that
A1: 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;
now
let x be Element of X,d being Element of product F;
A2: dom(f.(x,d)) = dom F & dom(g.(x,d)) = dom F by CARD_3:9;
for v be object st v in dom F holds (f.(x,d)).v = (g.(x,d)).v by A1;
hence f.(x,d) = g.(x,d) by A2,FUNCT_1:2;
end;
hence thesis by BINOP_1:2;
end;
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 :Def2:
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);
existence
proof
defpred Q[Element of X,Element of product F,Element of product F] means
for i being Element of dom F holds $3.i = (p.i).($1,$2.i);
A1: for x be Element of X,d being Element of product F ex z being Element
of product F st Q[x,d,z]
proof
let x be Element of X, d be Element of product F;
defpred P[object,object] means
ex i be Element of dom F st $1 =i & $2 = (p.i).
(x,d.i);
A2: for w be object st w in dom F ex z be object st P[w,z]
proof
let w be object;
assume w in dom F;
then reconsider i = w as Element of dom F;
take (p.i).(x,d.i);
thus thesis;
end;
consider z being Function such that
A3: dom z = dom F & for w being object st w in dom F holds P[w,z.w]
from CLASSES1:sch 1(A2);
now
let w be object;
assume w in dom F;
then ex i be Element of dom F st w = i & z.w = (p.i).(x,d.i) by A3;
hence z.w in F.w;
end;
then reconsider z9 = z as Element of product F by A3,CARD_3:9;
take z9;
let i be Element of dom F;
ex j being Element of dom F st j = i & z.i = (p.j).(x,d.j) by A3;
hence thesis;
end;
thus ex P being Function of [:X,product F:],product F st for x be Element
of X, d being Element of product F holds Q[x,d,P.(x,d)] from BINOP_1:sch 3(A1);
end;
uniqueness
proof
let P,Q be Function of [:X,product F:],product F such that
A4: for x be Element of X, f being Element of product F, i being
Element of dom F holds (P.(x,f)).i = (p.i).(x,f.i) and
A5: for x be Element of X, f being Element of product F, i being
Element of dom F holds (Q.(x,f)).i = (p.i).(x,f.i);
now
let x be Element of X, f being Element of product F;
let i be Element of dom F;
(P.(x,f)).i = (p.i).(x,f.i) by A4;
hence (P.(x,f)).i = (Q.(x,f)).i by A5;
end;
hence thesis by Th5;
end;
end;
definition
let R be Relation;
attr R is RealLinearSpace-yielding means :Def3:
for S be set st S in rng R holds S is RealLinearSpace;
end;
registration
cluster non empty RealLinearSpace-yielding for FinSequence;
existence
proof
set S = the RealLinearSpace;
take <*S*>;
thus <*S*> is non empty;
let x be set;
assume that
A1: x in rng <*S*> and
A2: not x is RealLinearSpace;
x in {S} by A1,FINSEQ_1:38;
hence contradiction by A2,TARSKI:def 1;
end;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
G.j in rng G by FUNCT_1:def 3;
hence thesis by Def3;
end;
end;
registration
cluster RealLinearSpace-yielding -> non-empty-addLoopStr-yielding
for Relation;
coherence
proof
let R be Relation;
assume R is RealLinearSpace-yielding; then
for x being set st x in rng R holds x is non empty addLoopStr;
hence thesis by PRVECT_1:def 9;
end;
end;
definition
let G be RealLinearSpace-Sequence, j be Element of dom carr G;
redefine func G.j -> RealLinearSpace; :: redefines . (FUNCT_1, definition)
coherence
proof
dom G = Seg len G & Seg len(carr G) = dom carr G by FINSEQ_1:def 3;
then reconsider j9 = j as Element of dom G by PRVECT_1:def 11;
G.j9 is RealLinearSpace;
hence thesis;
end;
end;
definition
::$CD 4
let G be RealLinearSpace-Sequence;
func multop G -> MultOps of REAL,carr G means
:Def8:
len it = len carr G &
for j be Element of dom carr G holds it.j = the Mult of G.j;
existence
proof
deffunc F(Element of dom carr G) = the Mult of G.$1;
consider p being non empty FinSequence such that
A20: len p = len carr G & for j be Element of dom carr G holds p.j = F
(j) from PRVECT_1:sch 1;
now
let ai be set;
assume ai in dom carr G;
then reconsider i=ai as Element of dom carr G;
len G = len(carr G) by PRVECT_1:def 11;
then reconsider j = i as Element of dom G by FINSEQ_3:29;
p.i = the Mult of G.i & the carrier of G.j = (carr G).j
by A20,PRVECT_1:def 11;
hence p.ai is Function of [:REAL,(carr G).ai:],(carr G).ai;
end;
then reconsider p9 = p as MultOps of REAL, carr G by A20,Th4;
take p9;
thus thesis by A20;
end;
uniqueness
proof
let f,h be MultOps of REAL, carr G;
assume that
A21: len f = len carr G and
A22: for j be Element of dom carr G holds f.j = the Mult of G.j and
A23: len h = len carr G and
A24: for j be Element of dom carr G holds h.j = the Mult of G.j;
reconsider f9 = f,h9 = h as FinSequence;
A25: now
let i be Nat;
assume i in dom f9;
then reconsider i9 = i as Element of dom carr G by A21,FINSEQ_3:29;
f9.i = the Mult of G.i9 by A22;
hence f9.i = h9.i by A24;
end;
dom f9 = Seg len f9 & dom h9 = Seg len h9 by FINSEQ_1:def 3;
hence thesis by A21,A23,A25,FINSEQ_1:13;
end;
end;
definition
let G be RealLinearSpace-Sequence;
func product G -> strict non empty RLSStruct equals
RLSStruct(# product carr G, zeros G, [:addop G:], [:multop G:] #);
coherence;
end;
Lm1: for LS be non empty addLoopStr st the addF of LS is commutative
associative holds LS is Abelian add-associative
by BINOP_1:def 2,BINOP_1:def 3;
Lm2: for LS be non empty addLoopStr st the ZeroF of LS is_a_unity_wrt the addF
of LS holds LS is right_zeroed by BINOP_1:3;
Lm3: for G be RealLinearSpace-Sequence holds for v1,w1 be Element of product
carr G, i be Element of dom carr G holds ([:addop G:].(v1,w1)).i = (the addF of
G.i).(v1.i,w1.i) & for vi,wi be VECTOR of G.i st vi=v1.i & wi=w1.i holds ([:
addop G:].(v1,w1)).i = vi+wi
proof
let G be RealLinearSpace-Sequence;
let v1,w1 be Element of product carr G;
let i be Element of dom carr G;
([:addop G:].(v1,w1)).i = ((addop G).i).(v1.i,w1.i) by PRVECT_1:def 8;
hence thesis by PRVECT_1:def 12;
end;
Lm4: for G be RealLinearSpace-Sequence, r be Element of REAL,
v be Element of product
carr G, i be Element of dom carr G holds ([:multop G:].(r,v)).i = (the Mult of
G.i).(r,v.i) & for vi be VECTOR of G.i st vi=v.i holds ([:multop G:].(r,v)).i =
r*vi
proof
let G be RealLinearSpace-Sequence;
let r be Element of REAL,v be Element of product carr G;
let i be Element of dom carr G;
([:multop G:].(r,v)).i = ((multop G).i).(r,v.i) by Def2;
hence thesis by Def8;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
Lm5: for G be RealLinearSpace-Sequence holds product G is vector-distributive
scalar-distributive scalar-associative scalar-unital
proof
deffunc ad(addLoopStr) = the addF of $1;
let G be RealLinearSpace-Sequence;
reconsider GS = RLSStruct(# product carr G,zeros G,[:addop G:],[:multop G:]
#) as non empty RLSStruct;
dom G = Seg len G by FINSEQ_1:def 3;
then dom G = Seg len carr G by PRVECT_1:def 11;
then
A1: dom G = dom carr G by FINSEQ_1:def 3;
now
let a1,b1 be Real;
reconsider a=a1,b=b1 as Element of REAL by XREAL_0:def 1;
let v,w be VECTOR of GS;
reconsider v1=v, w1=w as Element of product carr G;
A2: now
let x be object;
assume x in dom carr G;
then reconsider i = x as Element of dom carr G;
reconsider vi=v1.i as VECTOR of G.i by A1,PRVECT_1:def 11;
( [:multop G:].(jj,v1)).x = 1*vi by Lm4;
hence ([:multop G:].(jj,v1)).x =v1.x by RLVECT_1:def 8;
end;
A3: now
let x be object;
assume x in dom carr G;
then reconsider i = x as Element of dom carr G;
reconsider vi=v1.i as VECTOR of G.i by A1,PRVECT_1:def 11;
([:multop G:].(a+b,v1)).i = (a+b)*vi by Lm4
.= a*vi+b*vi by RLVECT_1:def 6
.= ad(G.i).(([:multop G:].(a,v1)).i,b*vi) by Lm4
.= ad(G.i).(([:multop G:].(a,v1)).i,([:multop G:].(b,v1)).i) by Lm4;
hence ([:multop G:].((a+b),v1)).x =([:addop G:].([:multop G:].(a,v1),[:
multop G:].(b,v1))).x by Lm3;
end;
A4: now
let x be object;
assume x in dom carr G;
then reconsider i = x as Element of dom carr G;
reconsider vi=v1.i, wi=w1.i as VECTOR of G.i by A1,PRVECT_1:def 11;
([:multop G:].(a,[:addop G:].(v1,w1))).i = (the Mult of G.i).(a,([:
addop G:].(v1,w1)).i) by Lm4
.= a*(vi+wi) by Lm3
.= a*vi+a*wi by RLVECT_1:def 5
.= ad(G.i).(([:multop G:].(a,v1)).i,a*wi) by Lm4
.= ad(G.i).(([:multop G:].(a,v1)).i,([:multop G:].(a,w1)).i) by Lm4;
hence ([:multop G:].(a,[:addop G:].(v1,w1))).x =([:addop G:].([:multop G
:].(a,v1),[:multop G:].(a,w1))).x by Lm3;
end;
dom([:multop G:].(a,[:addop G:].(v1,w1))) = dom carr G & dom([:addop G
:].([: multop G:].(a,v1),[:multop G:].(a,w1))) = dom carr G by CARD_3:9;
hence a1 * (v + w) = a1 * v + a1 * w by A4,FUNCT_1:2;
A5: now
let x be object;
assume x in dom carr G;
then reconsider i = x as Element of dom carr G;
reconsider vi=v1.i as VECTOR of G.i by A1,PRVECT_1:def 11;
([:multop G:].(a*b,v1)).i = (a*b)*vi by Lm4
.=a*(b*vi) by RLVECT_1:def 7
.=(the Mult of G.i).(a,([:multop G:].(b,v1)).i) by Lm4;
hence
([:multop G:].((a*b),v1)).x = ([:multop G:].(a,[:multop G:].(b,v1))
).x by Lm4;
end;
dom([:multop G:].(a+b,v1)) = dom carr G & dom([:addop G:].([:multop G
:].(a, v1),[:multop G:].(b,v1))) = dom carr G by CARD_3:9;
hence (a1 + b1) * v = a1 * v + b1 * v by A3,FUNCT_1:2;
dom([:multop G:].(a*b,v1)) = dom carr G & dom([:multop G:].(a,[:multop
G:].( b,v1))) = dom carr G by CARD_3:9;
hence a1 * b1 * v = a1 * (b1 * v) by A5,FUNCT_1:2;
dom([:multop G:].(jj,v1)) = dom carr G & dom v1 = dom carr G by CARD_3:9;
hence 1 * v = v by A2,FUNCT_1:2;
end;
hence thesis;
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;
coherence
proof
deffunc zr(addLoopStr) = the ZeroF of $1;
reconsider GS = RLSStruct(# product carr G,zeros G, [:addop G:],[:multop G
:] #) as non empty RLSStruct;
deffunc car(1-sorted) = the carrier of $1;
deffunc ad(addLoopStr) = the addF of $1;
A1: now
let i be Element of dom carr G;
dom G = Seg len G by FINSEQ_1:def 3
.= Seg len carr G by PRVECT_1:def 11
.= dom carr G by FINSEQ_1:def 3;
hence (carr G).i = car(G.i) by PRVECT_1:def 11;
end;
now
let i be Element of dom carr G;
(addop G).i = ad(G.i) & (carr G).i = car(G.i) by A1,PRVECT_1:def 12;
hence (addop G).i is associative by FVSUM_1:2;
end;
then
A2: [:addop G:] is associative by PRVECT_1:18;
now
let i be Element of dom carr G;
A3: (zeros G).i = 0.(G.i) by PRVECT_1:def 14;
(addop G).i = ad(G.i) & (carr G).i = car(G.i) by A1,PRVECT_1:def 12;
hence (zeros G).i is_a_unity_wrt (addop G).i by A3,PRVECT_1:1;
end; then
A4: zeros G is_a_unity_wrt [:addop G:] by PRVECT_1:19;
A5: GS is right_complementable
proof
let x be Element of GS;
reconsider y = (Frege complop G).x as Element of GS by FUNCT_2:5;
take y;
now
let i be Element of dom carr G;
0.(G.i) = zr(G.i); then
A6: zr(G.i) is_a_unity_wrt ad(G.i) by PRVECT_1:1;
A7: (complop G).i = comp G.i by PRVECT_1:def 13;
(carr G).i = car(G.i) & (addop G).i = ad(G.i) by A1,PRVECT_1:def 12;
hence (complop G).i is_an_inverseOp_wrt (addop G).i & (addop G).i is
having_a_unity by A6,A7,PRVECT_1:2,SETWISEO:def 2;
end;
then Frege complop G is_an_inverseOp_wrt [:addop G:] by PRVECT_1:20;
then [:addop G:].(x,y) = the_unity_wrt [:addop G:] by FINSEQOP:def 1;
hence thesis by A4,BINOP_1:def 8;
end;
now
let i be Element of dom carr G;
(addop G).i = ad(G.i) & (carr G).i = car(G.i) by A1,PRVECT_1:def 12;
hence (addop G).i is commutative by FVSUM_1:1;
end;
then [:addop G:] is commutative by PRVECT_1:17;
hence thesis by A2,A4,A5,Lm1,Lm2,Lm5;
end;
end;
begin :: The Product Space of Real Normed Spaces
definition
let R be Relation;
attr R is RealNormSpace-yielding means
:Def10:
for x be set st x in rng R holds x is RealNormSpace;
end;
registration
cluster non empty RealNormSpace-yielding for FinSequence;
existence
proof
set A = the RealNormSpace;
take <*A*>;
thus <*A*> is non empty;
let x be set;
assume that
A1: x in rng <*A*> and
A2: not x is RealNormSpace;
x in {A} by A1,FINSEQ_1:38;
hence contradiction by A2,TARSKI:def 1;
end;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
G.j in rng G by FUNCT_1:def 3;
hence thesis by Def10;
end;
end;
registration
cluster RealNormSpace-yielding -> RealLinearSpace-yielding for FinSequence;
coherence;
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
:Def11:
len it = len G
& for j be Element of dom G holds it.j=(the normF of G.j).(x.j);
existence
proof
deffunc F(Element of dom G) = In((the normF of G.$1).(x.$1),REAL);
consider f being Function of dom G,REAL such that
A1: for j being Element of dom G holds f.j = F(j) from FUNCT_2:sch 4;
A2: rng f c= REAL;
dom f = dom G by FUNCT_2:def 1;
then
A3: dom f = Seg len G by FINSEQ_1:def 3;
then f is FinSequence by FINSEQ_1:def 2;
then reconsider f as FinSequence of REAL by A2,FINSEQ_1:def 4;
A4: f in REAL* by FINSEQ_1:def 11;
len f = len G by A3,FINSEQ_1:def 3;
then f in (len G)-tuples_on REAL by A4;
then reconsider f as Element of REAL (len G);
take f;
thus len f = len G by CARD_1:def 7;
let j be Element of dom G;
f.j = F(j) by A1;
hence thesis;
end;
uniqueness
proof
let f,g be Element of REAL len G;
assume that
len f = len G and
A5: for j being Element of dom G holds f.j = (the normF of G.j).(x.j) and
len g = len G and
A6: for j being Element of dom G holds g.j = (the normF of G.j).(x.j);
now
let j be Nat;
assume j in Seg len G;
then reconsider j1=j as Element of dom G by FINSEQ_1:def 3;
f.j = (the normF of G.j1).(x.j1) by A5;
hence f.j = g.j by A6;
end;
hence thesis by FINSEQ_2:119;
end;
end;
definition
let G be RealNormSpace-Sequence;
func productnorm G -> Function of product carr (G qua
RealLinearSpace-Sequence),REAL means
:Def12:
for x being Element of product carr G holds it.x = |.normsequence(G,x).|;
existence
proof
deffunc F(Element of product carr G) = In(|.normsequence(G,$1).|,REAL);
consider f being Function of product carr G, REAL such that
A1: for x being Element of product carr G holds f.x = F(x) from FUNCT_2:sch 4;
take f;
let x be Element of product carr G;
f.x = F(x) by A1;
hence thesis;
end;
uniqueness
proof
let f,g be Function of product carr G,REAL;
assume that
A2: for x being Element of product carr G holds f.x = |.normsequence(G
,x).| and
A3: for x being Element of product carr G holds g.x = |.normsequence(G ,x).|;
now
let x be Element of product carr G;
f.x = |.normsequence(G,x).| by A2;
hence f.x = g.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let G be RealNormSpace-Sequence;
func product G -> strict non empty NORMSTR means
:Def13:
the RLSStruct of it
= product (G qua RealLinearSpace-Sequence) & the normF of it = productnorm G;
existence
proof
reconsider G0=NORMSTR(# product carr G,zeros G,[:addop G :],[:multop G:],
productnorm G #) as strict non empty NORMSTR;
take G0;
thus thesis;
end;
uniqueness;
end;
reserve G for RealNormSpace-Sequence;
theorem Th6:
product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop
G:], productnorm G #)
proof
the RLSStruct of product G = product(G qua RealLinearSpace-Sequence) by Def13
;
hence thesis by Def13;
end;
theorem Th7:
for x be VECTOR of product G, y be Element of product carr G st
x = y holds ||.x.|| = |.normsequence(G,y).|
proof
let x be VECTOR of product G;
let y be Element of product carr G;
assume
A1: x=y;
product G = NORMSTR(# product carr G,zeros G,[:addop G:], [:multop G:],
productnorm G #) by Th6;
hence thesis by A1,Def12;
end;
theorem Th8:
for x,y,z be Element of product carr G, i be Nat st
i in dom x & z = [:addop G :].(x,y) holds
normsequence(G,z).i <= (normsequence(G,x) + normsequence(G,y)).i
proof
let x,y,z be Element of product carr G, i be Nat such that
A1: i in dom x and
A2: z = [: addop G :].(x,y);
reconsider i0=i as Element of dom (carr G) by A1,CARD_3:9;
A3: z.i0 = ((addop G).i0).(x.i0,y.i0) by A2,PRVECT_1:def 8;
dom G = Seg len G by FINSEQ_1:def 3
.= Seg len carr G by PRVECT_1:def 11
.= dom carr G by FINSEQ_1:def 3;
then reconsider i0=i as Element of dom G by A1,CARD_3:9;
dom x = dom(carr G) & (carr G).i0 = the carrier of G.i0
by PRVECT_1:def 11,CARD_3:9;
then reconsider xi0=x.i0,yi0=y.i0,zi0=z.i0 as Element of G.i0 by A1,CARD_3:9;
||.zi0.|| = ||.xi0+yi0.|| by A3,PRVECT_1:def 12;
then
A4: ||.zi0.|| <= ||.xi0.|| + ||.yi0.|| by NORMSP_1:def 1;
A5: normsequence(G,x).i0 + normsequence(G,y).i0 = (normsequence(G,x) +
normsequence(G,y)).i0 by RVSUM_1:11;
(the normF of G.i0).yi0 = normsequence(G,y).i0 & (the normF of G.i0).zi0 =
normsequence(G,z).i0 by Def11;
hence thesis by A4,A5,Def11;
end;
theorem Th9:
for x be Element of product carr G, i be Nat st
i in dom x holds 0 <= normsequence(G,x).i
proof
let x be Element of product carr G, i be Nat such that
A1: i in dom x;
dom G = Seg len G by FINSEQ_1:def 3
.= Seg len carr G by PRVECT_1:def 11
.= dom carr G by FINSEQ_1:def 3;
then reconsider i0=i as Element of dom G by A1,CARD_3:9;
dom x = dom carr G & (carr G).i0 = the carrier of G.i0
by PRVECT_1:def 11,CARD_3:9;
then reconsider xi0=x.i0 as Element of G.i0 by A1,CARD_3:9;
0<= ||.xi0.|| by NORMSP_1:4;
hence thesis by Def11;
end;
Lm6: product G is reflexive discerning RealNormSpace-like
proof
A1: product G = NORMSTR(# product carr G,zeros G,[:addop G:], [:multop G:],
productnorm G #) by Th6;
A2: len G = len carr G by PRVECT_1:def 11;
reconsider n = len G as Element of NAT;
thus product G is reflexive
proof
reconsider z=0.(product G) as Element of product carr G by A1;
A3: for i be Element of dom carr G holds normsequence(G,z).i = 0
proof
let i be Element of dom carr G;
reconsider i0 = i as Element of dom G by A2,FINSEQ_3:29;
(carr G).i0 = the carrier of G.i0 by PRVECT_1:def 11;
then reconsider zi0=z.i0 as Element of G.i0 by CARD_3:9;
z.i = 0.(G.i) by A1,PRVECT_1:def 14;
then ||.zi0.|| = 0;
hence thesis by Def11;
end;
for i be Element of NAT st i in dom (sqr normsequence(G,z)) holds (
sqr normsequence(G,z)).i = 0
proof
let i be Element of NAT;
assume
A4: i in dom sqr normsequence(G,z);
len normsequence(G,z) = len G by Def11; then
A5: dom normsequence(G,z) = dom G by FINSEQ_3:29;
dom carr G = dom G by A2,FINSEQ_3:29;
then dom sqr normsequence(G,z) = dom carr G by A5,VALUED_1:11;
then (normsequence(G,z).i)^2 = 0^2 by A3,A4;
hence thesis by VALUED_1:11;
end;
then |.normsequence(G,z).| = 0 by Th3,SQUARE_1:17;
hence ||.0.product G.|| = 0 by Th7;
end;
thus product G is discerning proof let x being Point of product G;
reconsider z=x as Element of product carr G by A1;
assume
A6: ||.x.|| = 0;
now
let i be Element of dom carr G;
reconsider i0 = i as Element of dom G by A2,FINSEQ_3:29;
(carr G).i0 = the carrier of G.i0 by PRVECT_1:def 11;
then reconsider zzi0=z.i0 as Element of G.i0 by CARD_3:9;
||.x.|| = |.normsequence(G,z).| by Th7;
then normsequence(G,z) = 0*n by A6,EUCLID:8;
then normsequence(G,z).i = 0;
then ||.(zzi0).|| = 0 by Def11;
hence z.i = 0.(G.i) by NORMSP_0:def 5;
end;
hence thesis by A1,PRVECT_1:def 14;
end;
let x,y be Point of product G, a be Real;
reconsider z=x as Element of product carr G by A1;
reconsider xx = x, yy = y as Element of product carr G by A1;
reconsider ax=a * x as Element of product carr G by A1;
A7: ||.y.|| = |.normsequence(G,yy).| & |.normsequence(G,xx)+ normsequence(G
,yy) .| <= |.normsequence(G,xx).| + |.normsequence(G,yy).| by Th7,EUCLID:12;
A8: len normsequence(G,ax) = n by CARD_1:def 7; then
A9: dom normsequence(G,ax) = Seg n by FINSEQ_1:def 3;
A10: for i be Nat st i in dom normsequence(G,ax) holds normsequence(G,ax).i
= (|.a.| * normsequence(G,z)).i
proof
let i be Nat;
assume i in dom normsequence(G,ax);
then reconsider i0 = i as Element of dom G by A9,FINSEQ_1:def 3;
reconsider i1 = i0 as Element of dom carr G by A2,FINSEQ_3:29;
(carr G).i0 = the carrier of G.i0 & dom carr G = dom G
by A2,PRVECT_1:def 11,FINSEQ_3:29;
then reconsider axi0=ax.i0, zi0 = z.i0 as Element of G.i0 by CARD_3:9;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
( [:multop G:].(aa,z)).i1 = ((multop G).i1).(a,zi0) by Def2;
then axi0 = a * zi0 by A1,Def8;
then ||.axi0.|| = |.a.| * ||. zi0 .|| by NORMSP_1:def 1;
then ||.axi0.|| = |.a.| * normsequence(G,z).i0 by Def11;
then ||.axi0.|| = (|.a.| * normsequence(G,z)).i0 by RVSUM_1:44;
hence thesis by Def11;
end;
len (|.a.| * normsequence(G,z)) = n by CARD_1:def 7;
then |.normsequence(G,ax).| = |.|.a.|*normsequence(G,z).|
by A8,A10,FINSEQ_2:9; then
A11: |.normsequence(G,ax).| = |.|.a.|.| * |.normsequence(G,z).| by EUCLID:11;
reconsider z = x + y as Element of product carr G by A1;
A12: for i be Element of NAT st i in Seg n holds 0 <= normsequence(G,z).i &
normsequence(G,z).i <= (normsequence(G,xx)+ normsequence(G,yy)).i
proof
A13: dom xx = dom carr G by CARD_3:9;
A14: Seg n = dom G & dom carr G = dom G by A2,FINSEQ_1:def 3,FINSEQ_3:29;
let i be Element of NAT such that
A15: i in Seg n;
i in dom z by A15,A14,CARD_3:9;
hence thesis by A1,A15,A14,A13,Th8,Th9;
end;
A16: len normsequence(G,z) = n by Def11; then
len normsequence(G,z) = len (normsequence(G,xx)+ normsequence(G,yy))
by CARD_1:def 7; then
A17: |.normsequence(G,z).| <= |.normsequence(G,xx)+ normsequence(G,yy).|
by A16,A12,Th2;
||.x + y.|| = |.normsequence(G,z).| & ||.x.|| = |.normsequence(G,xx).|
by Th7;
hence thesis by A11,A17,A7,Th7,XXREAL_0:2;
end;
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;
coherence
proof
reconsider G1=G as RealLinearSpace-Sequence;
A1: the RLSStruct of product G = product (G qua RealLinearSpace-Sequence)
by Def13;
A2: now
let v be VECTOR of product G;
reconsider v1=v as VECTOR of product G1 by A1;
1 * v = 1 * v1 by A1;
hence 1 * v = v by RLVECT_1:def 8;
end;
A3: product G is right_complementable
proof
let v be VECTOR of product G;
reconsider v1=v as VECTOR of product G1 by A1;
reconsider w=-v1 as VECTOR of product G by A1;
take w;
v+w = v1-v1 by A1;
then v+w = 0.product G1 by RLVECT_1:15;
hence thesis by A1;
end;
A4: now
let a be Real;
let v,w be VECTOR of product G;
reconsider v1=v,w1=w as VECTOR of product G1 by A1;
a * (v + w) = a * (v1 + w1) by A1;
then a * (v + w) =a * v1 + a * w1 by RLVECT_1:def 5;
hence a * (v + w) = a*v +a*w by A1;
end;
A5: now
let a,b be Real, v be VECTOR of product G;
reconsider v1=v as VECTOR of product G1 by A1;
(a*b) * v = (a*b) * v1 by A1;
then (a*b) * v = a * (b * v1) by RLVECT_1:def 7;
hence (a*b) * v = a*(b*v) by A1;
end;
A6: now
let a,b be Real, v be VECTOR of product G;
reconsider v1=v as VECTOR of product G1 by A1;
(a+b) * v = (a+b) * v1 by A1;
then (a+b) * v = a * v1 + b * v1 by RLVECT_1:def 6;
hence (a+b) * v =a*v +b*v by A1;
end;
A7: product G is add-associative
proof
let v,w,x be VECTOR of product G;
reconsider v1=v,w1=w,x1=x as VECTOR of product G1 by A1;
(v+w)+x = (v1+w1)+x1 by A1;
then (v+w)+x =v1+(w1+x1) by RLVECT_1:def 3;
hence thesis by A1;
end;
A8: product G is Abelian
proof
let v,w be VECTOR of product G;
reconsider v1=v,w1=w as VECTOR of product G1 by A1;
v+w =v1+w1 by A1;
then v+w =w1+v1;
hence thesis by A1;
end;
product G is right_zeroed
proof
let v be VECTOR of product G;
reconsider v1=v as VECTOR of product G1 by A1;
v+0.product G = v1+0.product G1 by A1;
hence thesis;
end;
hence thesis by A8,A7,A3,A4,A6,A5,A2,Lm6;
end;
end;
theorem Th10:
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.||
proof
let 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;
reconsider n = len G as Element of NAT;
assume that
A1: y=x and
A2: xi=y.i;
A3: (normsequence(G,y).i)^2 = (sqr normsequence(G,y)).i by VALUED_1:11;
A4: for i be Nat st i in Seg n holds 0 <= (sqr normsequence(G,y)) .i
proof
let i be Nat such that
i in Seg n;
(normsequence(G,y).i)^2 >= 0 by XREAL_1:63;
hence thesis by VALUED_1:11;
end;
dom G = Seg n by FINSEQ_1:def 3; then
A5: 0 <= (normsequence(G,y).i)^2 & (sqr normsequence(G,y)).i <= Sum sqr
normsequence(G,y) by A4,REAL_NS1:7,XREAL_1:63;
||.xi.|| = normsequence(G,y).i by A2,Def11;
then sqrt ((sqr normsequence(G,y)).i) = normsequence(G,y).i
by A3,NORMSP_1:4,SQUARE_1:22; then
A6: ||.xi.|| = sqrt ((sqr normsequence(G,y)).i) by A2,Def11;
||.x.|| = |.normsequence(G,y).| by A1,Th7;
hence thesis by A3,A5,A6,SQUARE_1:26;
end;
Lm7: for RNS be RealNormSpace, S be sequence of RNS, g be Point of RNS holds S
is convergent & lim S = g iff ||.S - g.|| is convergent & lim ||.S - g.|| = 0
proof
let RNS be RealNormSpace, S be sequence of RNS, g be Point of RNS;
now
assume
A1: ||.S - g.|| is convergent & lim ||.S - g.|| = 0;
A2: now
let r be Real;
reconsider p=r as Real;
assume 0 < r;
then consider n be Nat such that
A3: for m be Nat st n<=m holds |.||.S - g.||.m-0 .| < p
by A1,SEQ_2:def 7;
reconsider n as Nat;
take n;
let m be Nat;
assume n<=m;
then |.||.S - g.||.m-0 .| < p by A3;
then |.||.(S - g).m.|| .| < p by NORMSP_0:def 4; then
|. ||.S.m - g.|| .| < p by NORMSP_1:def 4;
hence ||.S.m - g.|| < r by ABSVALUE:def 1,NORMSP_1:4;
end;
hence S is convergent;
hence lim S = g by A2,NORMSP_1:def 7;
end;
hence thesis by NORMSP_1:24;
end;
theorem Th11:
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.||
proof
let 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;
assume that
A1: xi=zx.i and
A2: zx=x and
A3: yi=zy.i and
A4: zy=y;
reconsider zyi = zy.i, zxi = zx.i as Element of G.i by A1,A3;
A5: product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:],
productnorm G #) by Th6;
then reconsider mzx =-x as Element of product carr G;
len G = len carr G by PRVECT_1:def 11; then
A6: dom G = dom carr G by FINSEQ_3:29;
-x = (-1) * x by RLVECT_1:16; then
A7: mzx.i = (-jj) * zxi by A2,A5,A6,Lm4;
then reconsider mzxi = mzx.i as Element of G.i;
reconsider zyMm = y-x as Element of product carr G by A5;
zyMm.i =zyi+mzxi by A4,A5,A6,Lm3;
then zyMm.i =zyi+-zxi by A7,RLVECT_1:16;
hence thesis by A1,A3,Th10;
end;
theorem
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
proof
let G be RealNormSpace-Sequence, seq be sequence of (product G),
x0 be Point of product G, y0 be Element of product carr G;
assume that
A1: x0 = y0 and
A2: seq is convergent & lim seq=x0;
let i be Element of dom G;
defpred P1[Nat,Element of G.i] means ex seqm be Element of
product carr G st seqm = seq.$1 & $2 = seqm.i;
len G = len carr G by PRVECT_1:def 11;
then
A3: dom G = dom carr G by FINSEQ_3:29;
then y0.i in (carr G).i by CARD_3:9;
then reconsider x0i=y0.i as Point of G.i by PRVECT_1:def 11;
A4: for x being Element of NAT ex y being Element of G.i st P1[x,y]
proof
let x be Element of NAT;
product G = NORMSTR(# product carr G,zeros G,[:addop G:], [:multop G:]
,productnorm G #) by Th6;
then consider seqm be Element of product carr G such that
A5: seqm =seq.x;
take seqm.i;
(carr G).i = the carrier of G.i by PRVECT_1:def 11;
hence thesis by A3,A5,CARD_3:9;
end;
consider f be sequence of the carrier of G.i such that
A6: for x being Element of NAT holds P1[x,f.x] from FUNCT_2:sch 3(A4);
for x being Nat holds P1[x,f.x]
proof let x be Nat;
x in NAT by ORDINAL1:def 12;
hence thesis by A6;
end;
then consider seqi be sequence of G.i such that
A7: for m be Nat ex seqm be Element of product carr G
st seqm= seq.m & seqi.m=seqm.i;
take seqi;
A8: for r be Real
st 0 < r ex m be Nat st
for n be Nat st m <= n holds ||.seqi.n - x0i.|| < r
proof
let r be Real;
assume r > 0;
then consider k be Nat such that
A9: for n be Nat st k <= n holds ||.seq.n - x0.|| < r by A2,NORMSP_1:def 7;
take k;
let n be Nat;
assume n >= k; then
A10: ||.(seq.n) - x0.|| < r by A9;
ex seqn be Element of product carr G st seqn = seq.n & seqi.n =
seqn.i by A7;
then ||. seqi.n - x0i.|| <= ||. seq.n - x0.|| by A1,Th11;
hence ||.(seqi.n) - x0i.|| < r by A10,XXREAL_0:2;
end;
then seqi is convergent;
hence thesis by A7,A8,NORMSP_1:def 7;
end;
theorem Th13:
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
proof
let G be RealNormSpace-Sequence, seq be sequence of (product G), x0 be Point
of product G, y0 be Element of product carr G;
assume that
A1: x0=y0 and
A2: 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;
defpred PP[Element of dom G, set] means ex rseqi be Real_Sequence, seqi be
sequence of G.$1 st rseqi=$2 & seqi is convergent & rseqi is convergent & lim
rseqi=0 & rseqi=||.seqi-lim seqi.|| & for m be Element of NAT holds ex seqm be
Element of product carr G st seqm= seq.m & seqi.m=seqm.$1;
A3: for i be Element of dom G ex yyseqi be Element of Funcs(NAT,REAL) st PP[
i,yyseqi]
proof
let i be Element of dom G;
consider seqi be sequence of G.i such that
A4: seqi is convergent and
y0.i = lim seqi and
A5: for m be Element of NAT holds ex Sm be Element of product carr G
st Sm= seq.m & seqi.m=Sm.i by A2;
set rseqi=||.seqi-lim seqi.||;
A6: rseqi is Element of Funcs(NAT,REAL) by FUNCT_2:8;
rseqi is convergent & lim rseqi=0 by A4,Lm7;
hence thesis by A4,A5,A6;
end;
consider yyseq be Function of (dom G),Funcs(NAT,REAL) such that
A7: for i be Element of dom G holds PP[i,yyseq.i] from FUNCT_2:sch 3(A3);
reconsider I = len G as Element of NAT;
defpred PQ[Element of NAT,Element of (REAL I)] means for i be Element of dom
G holds (yyseq.i).$1 = $2.i;
A8: for k be Element of NAT ex yseqk be Element of (REAL I) st PQ[k,yseqk]
proof
let k be Element of NAT;
defpred PPF[set,object] means
ex i be Element of dom G st i=$1 & $2 = (yyseq.i).k;
A9: for k be Nat st k in Seg I ex x be object st PPF[k,x]
proof
let j be Nat;
assume j in Seg I;
then reconsider i=j as Element of dom G by FINSEQ_1:def 3;
take (yyseq.i).k;
thus thesis;
end;
consider yseqk be FinSequence such that
A10: dom yseqk = Seg I & for j be Nat st j in Seg I holds PPF[j,yseqk.
j] from FINSEQ_1:sch 1(A9);
now
let j be Nat;
assume j in dom yseqk;
then consider i be Element of dom G such that
i=j and
A11: yseqk.j= (yyseq.i).k by A10;
yyseq.i is sequence of REAL by FUNCT_2:66;
hence yseqk.j in REAL by A11,FUNCT_2:5;
end;
then reconsider yyy=yseqk as FinSequence of REAL by FINSEQ_2:12;
yyy is Element of (len yyy)-tuples_on REAL by FINSEQ_2:92;
then reconsider yseqk as Element of (REAL I) by A10,FINSEQ_1:def 3;
now
let j be Element of dom G;
j in dom G;
then j in Seg I by FINSEQ_1:def 3;
then ex i be Element of dom G st i=j & yseqk.j= (yyseq.i).k by A10;
hence yseqk.j= (yyseq.j).k;
end;
hence thesis;
end;
consider yseq be sequence of REAL I such that
A12: for k be Element of NAT holds PQ[k,yseq.k] from FUNCT_2:sch 3(A8);
A13: now
let i0 be Element of NAT;
assume
i0 in Seg I;
then reconsider i=i0 as Element of dom G by FINSEQ_1:def 3;
take i;
consider rseqi be Real_Sequence, seqi be sequence of G.i such that
A14: rseqi=yyseq.i & seqi is convergent & rseqi is convergent & lim
rseqi= 0 &( rseqi=||.seqi-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) by A7;
take rseqi,seqi;
thus (for k be Element of NAT holds rseqi.k = (yseq.k).i0) & i=i0 & seqi
is convergent & rseqi is convergent & lim rseqi=(0*I).i & rseqi=||.seqi-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 by A12,A14;
end;
reconsider xseq=yseq as sequence of REAL-NS I by REAL_NS1:def 4;
xseq = yseq;
then consider
xseq be sequence of REAL-NS I, yseq be sequence of REAL I such that
A15: xseq=yseq and
A16: for i0 be Element of NAT st i0 in Seg I ex i be Element of dom G,
rseqi be Real_Sequence, seqi be sequence of G.i st (for k be Element of NAT
holds rseqi.k = (yseq.k).i0) & i=i0 & seqi is convergent & rseqi is convergent
& lim rseqi=(0*I).i & rseqi=||.seqi-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 by A13;
A17: for i be Nat st i in Seg I ex rseqi be Real_Sequence st (for
k be Nat holds rseqi.k = (yseq.k).i) & rseqi is convergent & (0*I).i
= lim rseqi
proof
let i0 be Nat;
assume i0 in Seg I;
then consider i be Element of dom G,
rseqi be Real_Sequence, seqi be sequence of G.i such that
A18: for k be Element of NAT holds rseqi.k = (yseq.k).i0 and
A19: i=i0 & seqi is convergent & rseqi is convergent &
lim rseqi=(0*I).i & rseqi=||.seqi-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 by A16;
take rseqi;
thus for k be Nat holds rseqi.k = (yseq.k).i0
proof let k be Nat;
k in NAT by ORDINAL1:def 12;
hence thesis by A18;
end;
thus thesis by A19;
end;
A20: product G = NORMSTR(# product carr G,zeros G, [:addop G:],[:multop G:],
productnorm G #) by Th6;
now
let x be object;
assume x in NAT;
then reconsider i=x as Element of NAT;
reconsider seqimx0 = seq.i-x0 as Element of product carr G by A20;
A21: now
reconsider mx0=-x0 as Element of product carr G by A20;
let k be Nat;
assume
A22: k in dom normsequence(G,seqimx0);
A23: len G= len normsequence(G,seqimx0) by Def11;
then reconsider k0=k as Element of dom G by A22,FINSEQ_3:29;
k in Seg I by A22,A23,FINSEQ_1:def 3;
then consider
k1 be Element of dom G, rseqk1i be Real_Sequence, seqk1i be
sequence of G.k1 such that
A24: for j be Element of NAT holds rseqk1i.j = (yseq.j).k and
A25: k1=k and
seqk1i is convergent and
rseqk1i is convergent and
lim rseqk1i=(0*I).k1 and
A26: rseqk1i=||.seqk1i-lim seqk1i.|| and
A27: for m be Element of NAT holds ex seqk1m be Element of product
carr G st seqk1m= seq.m & seqk1i.m=seqk1m.k1 by A16;
consider seqk0 be sequence of G.k0 such that
seqk0 is convergent and
A28: y0.k0 = lim seqk0 and
A29: for m be Element of NAT holds ex seqm0 be Element of product
carr G st seqm0= seq.m & seqk0.m=seqm0.k0 by A2;
A30: ex seqm0 be Element of product carr G st seqm0= seq.i & seqk0.i=
seqm0.k0 by A29;
now
let x be object;
assume x in NAT;
then reconsider m = x as Element of NAT;
( ex seqk1m be Element of product carr G st seqk1m= seq.m &
seqk1i.m=seqk1m.k1) & ex seqm0 be Element of product carr G st seqm0= seq.m &
seqk0.m = seqm0.k0 by A29,A27;
hence seqk1i.x = seqk0.x by A25;
end;
then
A31: seqk1i=seqk0 by A25,FUNCT_2:12;
len G = len carr G by PRVECT_1:def 11;
then
A32: dom G = dom carr G by FINSEQ_3:29;
-x0 = (-1) * x0 by RLVECT_1:16;
then mx0.k0 = (-jj)*(lim seqk0) by A1,A20,A28,A32,Lm4;
then -(lim seqk0) = mx0.k0 by RLVECT_1:16;
then
A33: seqimx0.k0 = seqk0.i - lim seqk0 by A20,A30,A32,Lm3;
thus (normsequence(G,seqimx0)).k = (the normF of G.k0).(seqimx0.k0) by
Def11
.= ||.(seqk0 -lim seqk0).i .|| by A33,NORMSP_1:def 4
.= (||.seqk1i - (lim seqk1i).||).i by A25,A31,NORMSP_0:def 4
.= (yseq.i).k by A24,A26;
end;
len (yseq.i)= I by CARD_1:def 7;
then len (yseq.i) = len normsequence(G,seqimx0) by Def11;
then dom (yseq.i) = dom normsequence(G,seqimx0) by FINSEQ_3:29;
then
A34: yseq.i = normsequence(G,seqimx0) by A21,FINSEQ_1:13;
thus ||.xseq-0.(REAL-NS I).||.x =||.(xseq-0.(REAL-NS I)).i .|| by
NORMSP_0:def 4
.=||.xseq.i-0.(REAL-NS I).|| by NORMSP_1:def 4
.=||.xseq.i.||
.=|.yseq.i.| by A15,REAL_NS1:1
.=||.seq.i -x0.|| by A34,Th7
.=||.(seq -x0).i.|| by NORMSP_1:def 4
.=||.seq-x0.||.x by NORMSP_0:def 4;
end;
then
A35: ||.xseq-0.(REAL-NS I).|| =||.seq-x0.|| by FUNCT_2:12;
(0*I) = 0.(REAL-NS I) by REAL_NS1:def 4;
then xseq is convergent & lim xseq = 0.(REAL-NS I) by A15,A17,REAL_NS1:11;
then ||.seq-x0.|| is convergent & lim ||.seq-x0.|| =0 by A35,Lm7;
hence thesis by Lm7;
end;
theorem
for G be RealNormSpace-Sequence st
for i be Element of dom G holds G.i is complete holds
product G is complete
proof
let G be RealNormSpace-Sequence such that
A1: for i be Element of dom G holds G.i is complete;
reconsider I = len G as Element of NAT;
A2: product G = NORMSTR(# product carr G,zeros G,[:addop G:], [:multop G:],
productnorm(G) #) by Th6;
for seq be sequence of (product G) holds seq is Cauchy_sequence_by_Norm
implies seq is convergent
proof
let seq be sequence of product G;
defpred PPG[Nat,object] means
ex i be Element of dom G st i=$1 & ex seqi be
sequence of G.i st seqi is convergent & $2 = 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;
assume
A3: seq is Cauchy_sequence_by_Norm;
A4: for k be Nat st k in Seg I ex x be object st PPG[k,x]
proof
let k be Nat;
assume k in Seg I;
then reconsider i=k as Element of dom G by FINSEQ_1:def 3;
defpred P1[Element of NAT,Element of G.i] means ex seqm be Element of
product carr G st seqm = seq.$1 & $2 = seqm.i;
A5: for x being Element of NAT ex y being Element of G.i st P1[x,y]
proof
let x be Element of NAT;
consider seqm be Element of product carr G such that
A6: seqm =seq.x by A2;
len G = len carr G by PRVECT_1:def 11;
then
A7: dom G = dom carr G by FINSEQ_3:29;
take seqm.i;
(carr G).i = the carrier of G.i by PRVECT_1:def 11;
hence thesis by A6,A7,CARD_3:9;
end;
ex f be sequence of the carrier of G.i st for x being Element
of NAT holds P1[x,f.x] from FUNCT_2:sch 3(A5);
then consider seqi be sequence of G.i such that
A8: for m be Element of NAT holds ex seqm be Element of product
carr G st seqm= seq.m & seqi.m=seqm.i;
A9: for m be Nat ex seqm be Element of product
carr G st seqm= seq.m & seqi.m=seqm.i
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A8;
end;
take lim seqi;
now
let r1 be Real such that
A10: r1 > 0;
reconsider r=r1 as Element of REAL by XREAL_0:def 1;
consider k be Nat such that
A11: for n,m be Nat st n >= k & m >= k holds ||. seq.n
- seq.m .|| < r by A3,A10,RSSPACE3:8;
take k;
let n,m be Nat;
assume n >= k & m >= k;
then
A12: ||. seq.n - seq.m .|| < r by A11;
( ex seqm be Element of product carr G st seqm = seq.m & seqi.m
= seqm.i)& ex seqn be Element of product carr G st seqn = seq.n & seqi.n = seqn
.i by A9;
then ||. seqi.n - seqi.m .||<= ||. seq.n - seq.m .|| by Th11;
hence ||. seqi.n - seqi.m .|| < r1 by A12,XXREAL_0:2;
end;
then
A13: seqi is Cauchy_sequence_by_Norm by RSSPACE3:8;
G.i is complete by A1;
hence thesis by A8,A13,LOPBAN_1:def 15;
end;
consider yy0 be FinSequence such that
A14: dom yy0 = Seg I & for j be Nat st j in Seg I holds PPG[j,yy0.j]
from FINSEQ_1:sch 1(A4);
A15: len yy0 = I by A14,FINSEQ_1:def 3;
then
A16: len yy0 = len carr G by PRVECT_1:def 11;
A17: now
let i be object;
assume i in dom carr G;
then reconsider x = i as Element of dom carr G;
reconsider x as Element of dom G by A15,A16,FINSEQ_3:29;
reconsider j =x as Element of NAT;
j in dom G;
then j in Seg I by FINSEQ_1:def 3;
then ex i0 be Element of dom G st i0=j & ex seqi be sequence of G.i0 st
seqi is convergent & yy0.j = lim seqi & for m be Element of NAT holds ex seqm
be Element of product carr G st seqm= seq.m & seqi.m=seqm.i0 by A14;
then yy0.x in the carrier of G.x;
hence yy0.i in (carr G).i by PRVECT_1:def 11;
end;
dom carr G = Seg len carr G & len G = len carr G
by PRVECT_1:def 11,FINSEQ_1:def 3;
then reconsider y0=yy0 as Element of product carr G by A14,A17,CARD_3:9;
A18: now
let i be Element of dom G;
reconsider j=i as Element of NAT;
i in dom G;
then i in Seg I by FINSEQ_1:def 3;
then consider i0 be Element of dom G such that
A19: i0=j and
A20: ex seqi be sequence of G.i0 st seqi is convergent & yy0.j = lim
seqi & for m be Element of NAT holds ex seqm be Element of product carr G st
seqm= seq.m & seqi.m=seqm.i0 by A14;
consider seqi be sequence of G.i0 such that
A21: seqi is convergent & yy0.j = lim seqi & for m be Element of NAT
holds ex seqm be Element of product carr G st seqm = seq.m & seqi.m=seqm.i0 by
A20;
reconsider seqi as sequence of G.i by A19;
take seqi;
thus 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
by A19,A21;
end;
reconsider x0 =y0 as Point of product G by A2;
x0 = y0;
hence thesis by A18,Th13;
end;
hence thesis by LOPBAN_1:def 15;
end;