:: Double Sequences and Limits
:: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 31, 2013
:: Copyright (c) 2013-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 NUMBERS, SUBSET_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_3, ARYTM_1,
XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, VALUED_0, ORDINAL2, SEQ_2,
XREAL_0, COMPLEX1, XCMPLX_0, XXREAL_2, FINSET_1, MEMBERED, MESFUNC9,
BHSP_3, SEQ_1, VALUED_1, DBLSEQ_1, FUNCOP_1, BINOP_1, BINOP_2, REAL_1;
notations ZFMISC_1, SUBSET_1, ORDINAL1, XXREAL_2, RELAT_1, PARTFUN1, RELSET_1,
FUNCT_1, FUNCT_2, NUMBERS, BINOP_1, XCMPLX_0, TARSKI, XBOOLE_0, FUNCOP_1,
FUNCT_3, FINSEQOP, MEMBERED, COMPLEX1, XXREAL_0, XREAL_0, SEQ_1, NAT_1,
MESFUNC9, VALUED_1, SEQ_2, FINSET_1, BINOP_2;
constructors TOPMETR, NAT_D, MESFUNC9, SEQ_2, COMSEQ_2, SEQ_4, REAL_1,
FINSEQOP, FUNCT_3, BINOP_2;
registrations ORDINAL1, XXREAL_0, XREAL_0, XBOOLE_0, NUMBERS, XCMPLX_0,
FINSET_1, SUBSET_1, MEMBERED, VALUED_0, XXREAL_2, RELSET_1, MEASURE6,
SEQ_4, FUNCT_1, FUNCT_2, VALUED_1, BINOP_2, NAT_1, SEQ_2, SEQ_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities BINOP_1;
expansions MEASURE6;
theorems TARSKI, XREAL_0, NAT_1, FUNCT_1, XXREAL_0, ZFMISC_1, XREAL_1,
FUNCT_2, RELAT_1, MESFUNC9, ORDINAL1, HEINE, NUMBERS, XCMPLX_1, VALUED_1,
ABSVALUE, COMPLEX1, MEMBERED, XXREAL_2, RINFSUP1, SEQM_3, SEQ_2, SEQ_4,
FUNCOP_1, FINSEQOP, XBOOLE_1, BINOP_2;
schemes FUNCT_2, FUNCT_3, FRAENKEL, ASYMPT_0;
begin
reserve Rseq, Rseq1, Rseq2 for Function of [:NAT,NAT:],REAL;
reserve rseq1,rseq2 for convergent Real_Sequence;
reserve n,m,N,M for Nat;
reserve e,r for Real;
:: Convergence in the Pringsheim sense
definition let Rseq;
attr Rseq is P-convergent means
ex p be Real st
for e be Real st 0<e
ex N be Nat st
for n,m be Nat st n>=N & m>=N holds
|.Rseq.(n,m) - p.| < e;
end;
definition let Rseq;
assume A1: Rseq is P-convergent;
func P-lim Rseq -> Real means :def6:
for e be Real st 0<e
ex N be Nat st
for n,m be Nat st n>=N & m>=N holds
|. Rseq.(n,m) - it .| < e;
existence by A1;
uniqueness
proof
given g1,g2 be Real such that
A2: for e st 0<e
ex N st for n,m st n>=N & m>=N holds |. Rseq.(n,m)-g1 .| < e and
A3: for e st 0<e
ex N st for n,m st n>=N & m>=N holds |. Rseq.(n,m)-g2 .| < e and
A4: g1<>g2;
A5: now assume |.g1-g2.|=0; then
g1-g2 = 0 by ABSVALUE:2;
hence contradiction by A4;
end;
A6: 0<=|.g1-g2.| by COMPLEX1:46; then
consider N1 be Nat such that
A7: for n,m st N1<=n & N1<=m holds |. Rseq.(n,m)-g1 .| < |.g1-g2.|/4 by A2,A5;
consider N2 be Nat such that
A8: for n,m st N2<=n & N2<=m holds |.Rseq.(n,m)-g2.| < |.g1-g2.|/4 by A3,A5,A6;
N1+N2 >= N1 & N1+N2 >= N2 by NAT_1:11; then
|.Rseq.(N1+N2,N1+N2)-g1.| < |.g1-g2.|/4 &
|.Rseq.(N1+N2,N1+N2)-g2.| < |.g1-g2.|/4 by A7,A8; then
A10: |.Rseq.(N1+N2,N1+N2)-g2.| + |.Rseq.(N1+N2,N1+N2)-g1.|
< |.g1-g2.|/4 + |.g1-g2.|/4 by XREAL_1:8;
|.g1-g2.| = |. (-(Rseq.(N1+N2,N1+N2)-g1)) + (Rseq.(N1+N2,N1+N2)-g2).|; then
|.g1-g2.| <= |.-(Rseq.(N1+N2,N1+N2)-g1).| + |.Rseq.(N1+N2,N1+N2)-g2.|
by COMPLEX1:56; then
A11: |.g1-g2.| <= |.Rseq.(N1+N2,N1+N2)-g1.| + |.Rseq.(N1+N2,N1+N2)-g2.|
by COMPLEX1:52;
|.g1-g2.|/2 < |.g1-g2.| by A5,A6,XREAL_1:216;
hence contradiction by A10,A11,XXREAL_0:2;
end;
end;
definition let Rseq;
attr Rseq is convergent_in_cod1 means
for m be Element of NAT holds ProjMap2(Rseq,m) is convergent;
attr Rseq is convergent_in_cod2 means
for n be Element of NAT holds ProjMap1(Rseq,n) is convergent;
end;
definition let Rseq;
func lim_in_cod1 Rseq -> Function of NAT,REAL means :def32:
for m be Element of NAT holds it.m = lim ProjMap2(Rseq,m);
existence
proof
defpred P[Element of NAT,set] means $2 = lim ProjMap2(Rseq,$1);
a1:now let m be Element of NAT;
reconsider n = lim ProjMap2(Rseq,m) as Element of REAL by XREAL_0:def 1;
take n;
thus P[m,n];
end;
consider IT be Function of NAT,REAL such that
a2: for m be Element of NAT holds P[m,IT.m] from FUNCT_2:sch 3(a1);
take IT;
thus thesis by a2;
end;
uniqueness
proof
let f1,f2 be Function of NAT,REAL;
assume that
a3: for m be Element of NAT holds f1.m = lim ProjMap2(Rseq,m) and
a4: for m be Element of NAT holds f2.m = lim ProjMap2(Rseq,m);
now let m be Element of NAT;
thus f1.m = lim ProjMap2(Rseq,m) by a3 .= f2.m by a4;
end;
hence f1 = f2 by FUNCT_2:63;
end;
end;
definition let Rseq;
func lim_in_cod2 Rseq -> Function of NAT,REAL means :def33:
for n be Element of NAT holds it.n = lim ProjMap1(Rseq,n);
existence
proof
defpred P[Element of NAT,set] means $2 = lim ProjMap1(Rseq,$1);
a1:now let m be Element of NAT;
reconsider n = lim ProjMap1(Rseq,m) as Element of REAL by XREAL_0:def 1;
take n;
thus P[m,n];
end;
consider IT be Function of NAT,REAL such that
a2: for m be Element of NAT holds P[m,IT.m] from FUNCT_2:sch 3(a1);
take IT;
thus thesis by a2;
end;
uniqueness
proof
let f1,f2 be Function of NAT,REAL;
assume that
a3: for n be Element of NAT holds f1.n = lim ProjMap1(Rseq,n) and
a4: for n be Element of NAT holds f2.n = lim ProjMap1(Rseq,n);
now let n be Element of NAT;
thus f1.n = lim ProjMap1(Rseq,n) by a3 .= f2.n by a4;
end;
hence f1 = f2 by FUNCT_2:63;
end;
end;
definition let Rseq;
assume a2: lim_in_cod1 Rseq is convergent;
func cod1_major_iterated_lim Rseq -> Real means :def34:
for e be Real st 0<e
ex M be Nat st
for m be Nat st m>=M holds
|.(lim_in_cod1 Rseq).m - it.| < e;
existence by a2,SEQ_2:def 6;
uniqueness
proof
let z1,z2 be Real;
assume that
a4: for e st 0<e
ex M st for m st m>=M holds |.(lim_in_cod1 Rseq).m - z1.| < e
and
a5: for e st 0<e
ex M st for m st m>=M holds |.(lim_in_cod1 Rseq).m - z2.| < e;
assume a6: z1 <> z2;
set p = |.z1 - z2.|/2;
a7: |.z1-z2.| > 0 by a6,COMPLEX1:62; then
consider M1 be Nat such that
a8: for m st M1<=m holds |.(lim_in_cod1 Rseq).m-z1.| < p by a4;
consider M2 be Nat such that
a9: for m st M2<=m holds |.(lim_in_cod1 Rseq).m-z2.| < p by a5,a7;
set M = max(M1,M2);
a0: M is Nat by TARSKI:1;
for m st M <= m holds 2*p<2*p
proof
let m;
set s = lim_in_cod1 Rseq;
assume a10: M <= m;
M2<=M by XXREAL_0:25; then
M + M2 <= M + m by a10,XREAL_1:7; then
M2<=m by XREAL_1:6; then
a11: |. s.m - z2.|< p by a9;
|.z1 - z2.| = |.z1 - s.m - (z2 - s.m).|; then
|.z1 - z2.| <= |.z1-s.m.| + |.z2-s.m.| by COMPLEX1:57; then
a12: |.z1 - z2.| <= |.s.m - z1.| + |.z2-s.m.| by COMPLEX1:60;
M1<=M by XXREAL_0:25; then
M + M1 <= M + m by a10,XREAL_1:7; then
M1<=m by XREAL_1:6; then
|.s.m - z1.|< p by a8; then
|.s.m - z1.| + |.s.m - z2.| <p + p by a11,XREAL_1:8;
hence thesis by a12,COMPLEX1:60;
end;
hence contradiction by a0;
end;
end;
definition let Rseq;
assume a2: lim_in_cod2 Rseq is convergent;
func cod2_major_iterated_lim Rseq -> Real means :def35:
for e be Real st 0<e
ex N be Nat st
for n be Nat st n>=N holds
|.(lim_in_cod2 Rseq).n - it.| < e;
existence by a2,SEQ_2:def 6;
uniqueness
proof
let z1,z2 be Real;
assume that
a4: for e st 0<e
ex M st for m st m>=M holds |.(lim_in_cod2 Rseq).m - z1.| < e
and
a5: for e st 0<e
ex M st for m st m>=M holds |.(lim_in_cod2 Rseq).m - z2.| < e;
assume a6: z1 <> z2;
set p = |.z1 - z2.|/2;
a7: |.z1-z2.| > 0 by a6,COMPLEX1:62; then
consider M1 be Nat such that
a8: for m st M1<=m holds |.(lim_in_cod2 Rseq).m-z1.| < p by a4;
consider M2 be Nat such that
a9: for m st M2<=m holds |.(lim_in_cod2 Rseq).m-z2.| < p by a5,a7;
set M = max(M1,M2);
a0: M is Nat by TARSKI:1;
for m st M <= m holds 2*p<2*p
proof
let m;
set s = lim_in_cod2 Rseq;
assume a10: M <= m;
M2<=M by XXREAL_0:25; then
M + M2 <= M + m by a10,XREAL_1:7; then
M2<=m by XREAL_1:6; then
a11: |. s.m - z2.|< p by a9;
|.z1 - z2.| = |.z1 - s.m - (z2 - s.m).|; then
|.z1 - z2.| <= |.z1-s.m.| + |.z2-s.m.| by COMPLEX1:57; then
a12: |.z1 - z2.| <= |.s.m - z1.| + |.z2-s.m.| by COMPLEX1:60;
M1<=M by XXREAL_0:25; then
M + M1 <= M + m by a10,XREAL_1:7; then
M1<=m by XREAL_1:6; then
|.s.m - z1.|< p by a8; then
|.s.m - z1.| + |.s.m - z2.| <p + p by a11,XREAL_1:8;
hence thesis by a12,COMPLEX1:60;
end;
hence contradiction by a0;
end;
end;
definition
let Rseq be Function of [:NAT,NAT:],REAL;
attr Rseq is uniformly_convergent_in_cod1 means
Rseq is convergent_in_cod1 &
for e be Real st e>0
ex M be Nat st
for m be Nat st m>=M holds
for n be Nat holds
|. Rseq.(n,m) - (lim_in_cod1 Rseq).n .| < e;
end;
definition
let Rseq be Function of [:NAT,NAT:],REAL;
attr Rseq is uniformly_convergent_in_cod2 means
Rseq is convergent_in_cod2 &
for e be Real st e>0
ex N be Nat st
for n be Nat st n>=N holds
for m be Nat holds
|. Rseq.(n,m) - (lim_in_cod2 Rseq).m .| < e;
end;
definition let Rseq;
attr Rseq is non-decreasing means
for n1,m1,n2,m2 be Nat st
n1>=n2 & m1>=m2 holds Rseq.(n1,m1) >= Rseq.(n2,m2);
attr Rseq is non-increasing means
for n1,m1,n2,m2 be Nat st
n1>=n2 & m1>=m2 holds Rseq.(n1,m1) <= Rseq.(n2,m2);
end;
theorem th28:
for a,b,c be Real st a <= b & b <= c holds
|.b.| <= |.a.| or |.b.| <= |.c.|
proof
let a,b,c be Real;
assume a1: a<=b & b<=c;
per cases;
suppose b >= 0; then
|.b.| = b & |.c.| = c by a1,ABSVALUE:def 1;
hence thesis by a1;
end;
suppose b < 0; then
|.a.| = -a & |.b.| = -b by a1,ABSVALUE:def 1;
hence thesis by a1,XREAL_1:24;
end;
end;
registration
cluster non-decreasing P-convergent -> bounded_below bounded_above
for Function of [:NAT,NAT:],REAL;
coherence
proof let Rseq be Function of [:NAT,NAT:],REAL;
assume a1: Rseq is non-decreasing P-convergent; then
consider p be Real such that
a3: for e st 0<e
ex N st for n,m st n>=N & m>=N holds |.Rseq.(n,m)-p.| < e;
consider N such that
a4: for n,m st n>=N & m>=N holds |.Rseq.(n,m)-p.| < 1 by a3;
a5:for n,m st n>=N & m>=N holds |.Rseq.(n,m).| < 1 + |.p.|
proof
let n,m;
assume n>=N & m>=N; then
a6: |.Rseq.(n,m)-p.| < 1 by a4;
|.Rseq.(n,m)-p.| >= |.Rseq.(n,m).| - |.p.| by COMPLEX1:59; then
|.Rseq.(n,m).| - |.p.| < 1 by a6,XXREAL_0:2;
hence |.Rseq.(n,m).| < 1 + |.p.| by XREAL_1:19;
end;
deffunc F(Element of NAT) = $1;
deffunc F1(Nat) = |.Rseq.(1,$1).|;
reconsider E2 = {F(m) where m is Element of NAT: m <= N} as
finite non empty Subset of NAT from ASYMPT_0:sch 2;
reconsider EE = [:E2,E2:] as finite set;
c1:E2 is finite;
deffunc F(Element of NAT,Element of NAT) = |.Rseq.($1,$2).|;
a9:{F(m,n) where m is Element of NAT, n is Element of NAT :
m in E2 & n in E2} is finite from FRAENKEL:sch 22(c1,c1);
set F = {F(m,n) where m is Element of NAT, n is Element of NAT :
m in E2 & n in E2};
N is Element of NAT by ORDINAL1:def 12; then
N in E2; then
b1: |.Rseq.(N,N).| in F;
now let x be object;
assume x in F; then
consider p be Element of NAT, q be Element of NAT such that
a10: x = F(p,q) & p in E2 & q in E2;
thus x is real by a10;
end; then
reconsider F as non empty real-membered set by b1,MEMBERED:def 3;
reconsider M1 = sup F as Element of REAL by a9,XXREAL_2:16;
set M = max(M1,1 + |.p.|);
a14:M >= 1+ |.p.| & 1+ |.p.| >= 1 & M >= M1 & M >= M1
by XXREAL_0:25,XREAL_1:31,COMPLEX1:46;
c1:for n,m holds |.Rseq.(n,m).| <= M
proof
let n,m;
c0: n is Element of NAT & m is Element of NAT & N is Element of NAT
by ORDINAL1:def 12;
per cases;
suppose n >= N & m >= N; then
|.Rseq.(n,m).| < 1 + |.p.| by a5;
hence |.Rseq.(n,m).| <= M by a14,XXREAL_0:2;
end;
suppose n < N & m < N; then
n in E2 & m in E2 by c0; then
|.Rseq.(n,m).| in F; then
a15: |.Rseq.(n,m).| <= M1 by XXREAL_2:4;
M >= M1 by XXREAL_0:25;
hence |.Rseq.(n,m).| <= M by a15,XXREAL_0:2;
end;
suppose a18: n < N & m >= N; then
a19: Rseq.(n,N) <= Rseq.(n,m) & Rseq.(n,m) <= Rseq.(N,m) by a1;
n in E2 & N in E2 by a18,c0; then
|.Rseq.(n,N).| in F; then
a20: |.Rseq.(n,N).| <= M1 by XXREAL_2:4;
a21: |.Rseq.(N,m).| < 1+ |.p.| by a5,a18;
per cases by a19,th28;
suppose |.Rseq.(n,m).| <= |.Rseq.(n,N).|; then
|.Rseq.(n,m).| <= M1 by a20,XXREAL_0:2;
hence |.Rseq.(n,m).| <= M by a14,XXREAL_0:2;
end;
suppose |.Rseq.(n,m).| <= |.Rseq.(N,m).|; then
|.Rseq.(n,m).| <= 1+ |.p.| by a21,XXREAL_0:2;
hence |.Rseq.(n,m).| <= M by a14,XXREAL_0:2;
end;
end;
suppose a22: n >= N & m < N; then
a23: Rseq.(N,m) <= Rseq.(n,m) & Rseq.(n,m) <= Rseq.(n,N) by a1;
N in E2 & m in E2 by a22,c0; then
|.Rseq.(N,m).| in F; then
a24: |.Rseq.(N,m).| <= M1 by XXREAL_2:4;
a25: |.Rseq.(n,N).| < 1+ |.p.| by a5,a22;
per cases by a23,th28;
suppose |.Rseq.(n,m).| <= |.Rseq.(N,m).|; then
|.Rseq.(n,m).| <= M1 by a24,XXREAL_0:2;
hence |.Rseq.(n,m).| <= M by a14,XXREAL_0:2;
end;
suppose |.Rseq.(n,m).| <= |.Rseq.(n,N).|; then
|.Rseq.(n,m).| <= 1+ |.p.| by a25,XXREAL_0:2;
hence |.Rseq.(n,m).| <= M by a14,XXREAL_0:2;
end;
end;
end;
now let a be ExtReal;
assume a in Rseq.: [:NAT,NAT:]; then
consider x be Element of [:NAT,NAT qua non empty set:] such that
b2: x in [:NAT,NAT:] & a = Rseq.x by FUNCT_2:65;
consider n,m be object such that
b3: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by b3;
|.Rseq.(n,m).| <= M by c1;
hence -M <= a & a <= M by b2,b3,ABSVALUE:5;
end; then
(for a be ExtReal st a in Rseq.: [:NAT,NAT:] holds -M <= a) &
(for a be ExtReal st a in Rseq.: [:NAT,NAT:] holds a <= M); then
-M is LowerBound of Rseq.: [:NAT,NAT:] &
M is UpperBound of Rseq.: [:NAT,NAT:] by XXREAL_2:def 1,def 2;
hence thesis by XXREAL_2:def 9,def 10;
end;
end;
registration
cluster non-increasing P-convergent -> bounded_below bounded_above
for Function of [:NAT,NAT:],REAL;
coherence
proof
let Rseq be Function of [:NAT,NAT:],REAL;
assume a1: Rseq is non-increasing P-convergent; then
consider p be Real such that
a3: for e st 0<e
ex N st for n,m st n>=N & m>=N holds |.Rseq.(n,m)-p.| < e;
consider N such that
a4: for n,m st n>=N & m>=N holds |.Rseq.(n,m)-p.| < 1 by a3;
a5:for n,m st n>=N & m>=N holds |.Rseq.(n,m).| < 1 + |.p.|
proof
let n,m;
assume n>=N & m>=N; then
a6: |.Rseq.(n,m)-p.| < 1 by a4;
|.Rseq.(n,m)-p.| >= |.Rseq.(n,m).| - |.p.| by COMPLEX1:59; then
|.Rseq.(n,m).| - |.p.| < 1 by a6,XXREAL_0:2;
hence |.Rseq.(n,m).| < 1 + |.p.| by XREAL_1:19;
end;
deffunc F1(Element of NAT) = |.Rseq.(1,$1).|;
deffunc F(Element of NAT) = $1;
reconsider E2 = {F(m) where m is Element of NAT: m <= N} as
finite non empty Subset of NAT from ASYMPT_0:sch 2;
reconsider EE = [:E2,E2:] as finite set;
c1:E2 is finite;
deffunc F(Element of NAT,Element of NAT) = |.Rseq.($1,$2).|;
a9:{F(m,n) where m is Element of NAT, n is Element of NAT :
m in E2 & n in E2} is finite from FRAENKEL:sch 22(c1,c1);
set F = {F(m,n) where m is Element of NAT, n is Element of NAT :
m in E2 & n in E2};
N is Element of NAT by ORDINAL1:def 12; then
N in E2; then
b1: |.Rseq.(N,N).| in F;
now let x be object;
assume x in F; then
consider p be Element of NAT, q be Element of NAT such that
a10: x = F(p,q) & p in E2 & q in E2;
thus x is real by a10;
end; then
reconsider F as non empty real-membered set by b1,MEMBERED:def 3;
reconsider M1 = sup F as Element of REAL by a9,XXREAL_2:16;
set M = max(M1,1+ |.p.|);
a14:M >= 1+ |.p.| & 1+ |.p.| >= 1 & M >= M1 & M >= M1
by XXREAL_0:25,XREAL_1:31,COMPLEX1:46;
c1:for n,m holds |.Rseq.(n,m).| <= M
proof
let n,m;
c0: n is Element of NAT & m is Element of NAT & N is Element of NAT
by ORDINAL1:def 12;
per cases;
suppose n >= N & m >= N; then
|.Rseq.(n,m).| < 1 + |.p.| by a5;
hence |.Rseq.(n,m).| <= M by a14,XXREAL_0:2;
end;
suppose n < N & m < N; then
n in E2 & m in E2 by c0; then
|.Rseq.(n,m).| in F; then
a15: |.Rseq.(n,m).| <= M1 by XXREAL_2:4;
M >= M1 by XXREAL_0:25;
hence |.Rseq.(n,m).| <= M by a15,XXREAL_0:2;
end;
suppose a18: n < N & m >= N; then
a19: Rseq.(n,N) >= Rseq.(n,m) & Rseq.(n,m) >= Rseq.(N,m) by a1;
n in E2 & N in E2 by a18,c0; then
|.Rseq.(n,N).| in F; then
a20: |.Rseq.(n,N).| <= M1 by XXREAL_2:4;
a21: |.Rseq.(N,m).| < 1+ |.p.| by a5,a18;
per cases by a19,th28;
suppose |.Rseq.(n,m).| <= |.Rseq.(n,N).|; then
|.Rseq.(n,m).| <= M1 by a20,XXREAL_0:2;
hence |.Rseq.(n,m).| <= M by a14,XXREAL_0:2;
end;
suppose |.Rseq.(n,m).| <= |.Rseq.(N,m).|; then
|.Rseq.(n,m).| <= 1+ |.p.| by a21,XXREAL_0:2;
hence |.Rseq.(n,m).| <= M by a14,XXREAL_0:2;
end;
end;
suppose a22: n >= N & m < N; then
a23: Rseq.(N,m) >= Rseq.(n,m) & Rseq.(n,m) >= Rseq.(n,N) by a1;
N in E2 & m in E2 by a22,c0; then
|.Rseq.(N,m).| in F; then
a24: |.Rseq.(N,m).| <= M1 by XXREAL_2:4;
a25: |.Rseq.(n,N).| < 1+ |.p.| by a5,a22;
per cases by a23,th28;
suppose |.Rseq.(n,m).| <= |.Rseq.(N,m).|; then
|.Rseq.(n,m).| <= M1 by a24,XXREAL_0:2;
hence |.Rseq.(n,m).| <= M by a14,XXREAL_0:2;
end;
suppose |.Rseq.(n,m).| <= |.Rseq.(n,N).|; then
|.Rseq.(n,m).| <= 1+ |.p.| by a25,XXREAL_0:2;
hence |.Rseq.(n,m).| <= M by a14,XXREAL_0:2;
end;
end;
end;
now let a be ExtReal;
assume a in Rseq.: [:NAT,NAT:]; then
consider x be Element of [:NAT,NAT:] such that
b2: x in [:NAT,NAT:] & a = Rseq.x by FUNCT_2:65;
consider n,m be object such that
b3: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by b3;
|.Rseq.(n,m).| <= M by c1;
hence -M <= a & a <= M by b3,b2,ABSVALUE:5;
end; then
(for a be ExtReal st a in Rseq.: [:NAT,NAT:] holds -M <= a) &
(for a be ExtReal st a in Rseq.: [:NAT,NAT:] holds a <= M); then
-M is LowerBound of Rseq.: [:NAT,NAT:] &
M is UpperBound of Rseq.: [:NAT,NAT:] by XXREAL_2:def 1,def 2;
hence thesis by XXREAL_2:def 9,def 10;
end;
end;
LM111:
for r be Element of REAL holds
[:NAT,NAT:]-->r is P-convergent & [:NAT,NAT:]-->r is convergent_in_cod1
& [:NAT,NAT:]-->r is convergent_in_cod2
proof
let r be Element of REAL;
set Rseq = [:NAT,NAT:] --> r;
a1:for n,m be Nat holds Rseq.(n,m) = r
proof
let n,m be Nat;
n is Element of NAT & m is Element of NAT by ORDINAL1:def 12;
hence Rseq.(n,m) = r by FUNCOP_1:70;
end;
a3:now let e be Real;
assume a2: 0<e;
a4: now let n,m such that n>=0 & m>=0;
Rseq.(n,m) = r by a1;
hence |. Rseq.(n,m) - r.| < e by a2,COMPLEX1:44;
end;
reconsider N = 0 as Nat;
take N;
thus for n,m st n>=N & m>=N holds |. Rseq.(n,m) - r.| < e by a4;
end;
b1:now let m be Element of NAT;
now let e be Real;
assume b3: 0<e;
now let n be Nat;
assume 0<=n;
b4: n is Element of NAT by ORDINAL1:def 12; then
ProjMap2(Rseq,m).n = Rseq.(n,m) by MESFUNC9:def 7; then
ProjMap2(Rseq,m).n = r by b4,FUNCOP_1:70;
hence |.ProjMap2(Rseq,m).n - r.| < e by b3,ABSVALUE:2;
end;
hence ex N be Nat st for n be Nat st N<=n
holds |.ProjMap2(Rseq,m).n-r.| < e;
end;
hence ProjMap2(Rseq,m) is convergent by SEQ_2:def 6;
end;
now let n be Element of NAT;
now let e be Real;
assume c3: 0<e;
now let m be Nat;
assume 0<=m;
c4: m is Element of NAT by ORDINAL1:def 12; then
ProjMap1(Rseq,n).m = Rseq.(n,m) by MESFUNC9:def 6; then
ProjMap1(Rseq,n).m = r by c4,FUNCOP_1:70;
hence |.ProjMap1(Rseq,n).m - r.| < e by c3,ABSVALUE:2;
end;
hence ex M be Nat st for m be Nat st M<=m
holds |.ProjMap1(Rseq,n).m-r.| < e;
end;
hence ProjMap1(Rseq,n) is convergent by SEQ_2:def 6;
end;
hence thesis by a3,b1;
end;
registration
let r be Element of REAL;
cluster [:NAT,NAT:] --> r -> P-convergent convergent_in_cod1
convergent_in_cod2 for Function of [:NAT,NAT:],REAL;
coherence by LM111;
end;
theorem
for r be Element of REAL holds P-lim ([:NAT,NAT:] --> r) = r
proof
let r be Element of REAL;
set Rseq = [:NAT,NAT:] --> r;
a1:for n,m be Nat holds Rseq.(n,m) = r
proof
let n,m be Nat;
n is Element of NAT & m is Element of NAT by ORDINAL1:def 12;
hence Rseq.(n,m) = r by FUNCOP_1:70;
end;
now let e be Real;
assume a2: 0<e;
a4: now let n,m such that n>=0 & m>=0;
Rseq.(n,m) = r by a1;
hence |. Rseq.(n,m) - r.| < e by a2,COMPLEX1:44;
end;
reconsider N = 0 as Nat;
take N;
thus for n,m st n>=N & m>=N holds |. Rseq.(n,m) - r.| < e by a4;
end;
hence P-lim ([:NAT,NAT:] --> r) = r by def6;
end;
registration
cluster P-convergent convergent_in_cod1 convergent_in_cod2
for Function of [:NAT,NAT:],REAL;
existence
proof
a1: 1 is Element of REAL by XREAL_0:def 1; then
reconsider f = [:NAT,NAT:] --> 1 as Function of [:NAT,NAT:],REAL
by FUNCOP_1:46;
f is P-convergent convergent_in_cod1 convergent_in_cod2
by a1;
hence thesis;
end;
end;
reserve Pseq for P-convergent Function of [:NAT,NAT:],REAL;
registration
let Pseq2 be P-convergent convergent_in_cod2 Function of [:NAT,NAT:],REAL;
cluster lim_in_cod2 Pseq2 -> convergent;
coherence
proof
Pseq2 is P-convergent; then
consider z be Real such that
a3: for e st 0<e
ex N1 be Nat st
for n,m st n>=N1 & m>=N1 holds |.Pseq2.(n,m)-z.| < e;
for e st 0<e
ex N st for n st n>=N holds |.(lim_in_cod2 Pseq2).n - z.| < e
proof
let e;
assume a8: 0 < e; then
consider N1 be Nat such that
a15: for n,m st n>=N1 & m>=N1 holds |.Pseq2.(n,m)-z.| < e/2 by a3;
a12:for n be Element of NAT st n >= N1 holds
ex N2 be Nat st
for m st m>=N2 holds
|.ProjMap1(Pseq2,n).m - (lim_in_cod2 Pseq2).n.| < e/2
proof
let n be Element of NAT;
assume n >= N1;
Pseq2 is convergent_in_cod2; then
ProjMap1(Pseq2,n) is convergent; then
consider N2 be Nat such that
a9: for m be Nat st m>=N2 holds
|.ProjMap1(Pseq2,n).m - lim ProjMap1(Pseq2,n).| < e/2
by a8,SEQ_2:def 7;
take N2;
thus for m st m >= N2 holds
|.ProjMap1(Pseq2,n).m - (lim_in_cod2 Pseq2).n .| < e/2
proof
let m;
assume m >=N2; then
|.ProjMap1(Pseq2,n).m - lim ProjMap1(Pseq2,n).| < e/2 by a9;
hence thesis by def33;
end;
end;
take N1;
thus for n st n>=N1 holds |.(lim_in_cod2 Pseq2).n - z.| < e
proof
let n;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
assume a14: n>=N1; then
consider N2 be Nat such that
a13: for m st m>=N2 holds
|.ProjMap1(Pseq2,n1).m - (lim_in_cod2 Pseq2).n1 .| < e/2
by a12;
reconsider M=max(N2,N1) as Element of NAT by ORDINAL1:def 12;
a17: ProjMap1(Pseq2,n1).M = Pseq2.(n,M) by MESFUNC9:def 6;
a16: M>=N2 & M>=N1 by XXREAL_0:25;
a18: |.(lim_in_cod2 Pseq2).n - z.|
<= |.(lim_in_cod2 Pseq2).n - ProjMap1(Pseq2,n1).M .|
+ |.Pseq2.(n,M) - z.| by a17,COMPLEX1:63;
|.(lim_in_cod2 Pseq2).n - ProjMap1(Pseq2,n1).M .|
= |.ProjMap1(Pseq2,n1).M - (lim_in_cod2 Pseq2).n .| by COMPLEX1:60; then
a20: |.(lim_in_cod2 Pseq2).n - ProjMap1(Pseq2,n1).M .| < e/2
by a13,XXREAL_0:25;
|.Pseq2.(n1,M) - z.| < e/2 by a15,a16,a14; then
|.(lim_in_cod2 Pseq2).n - ProjMap1(Pseq2,n1).M .|
+ |.Pseq2.(n,M) - z.| < e/2 + e/2 by a20,XREAL_1:8;
hence |.(lim_in_cod2 Pseq2).n - z.| < e by a18,XXREAL_0:2;
end;
end;
hence lim_in_cod2 Pseq2 is convergent by SEQ_2:def 6;
end;
end;
theorem
Rseq is P-convergent convergent_in_cod2 implies
P-lim Rseq = cod2_major_iterated_lim Rseq
proof
assume a1: Rseq is P-convergent convergent_in_cod2; then
consider z be Real such that
a3: for e st 0<e
ex N1 be Nat st
for n,m st n>=N1 & m>=N1 holds |.Rseq.(n,m)-z.| < e;
for e st 0<e
ex N st for n st n>=N holds |.(lim_in_cod2 Rseq).n - z.| < e
proof
let e;
assume a8: 0 < e; then
consider N1 be Nat such that
a15: for n,m st n>=N1 & m>=N1 holds |.Rseq.(n,m)-z.| < e/2 by a3;
a12:for n be Element of NAT st n >= N1 holds
ex N2 be Nat st
for m st m>=N2 holds |.ProjMap1(Rseq,n).m - (lim_in_cod2 Rseq).n.| < e/2
proof
let n be Element of NAT;
assume n >= N1;
ProjMap1(Rseq,n) is convergent by a1; then
consider N2 be Nat such that
a9: for m be Nat st m>=N2 holds
|.ProjMap1(Rseq,n).m - lim ProjMap1(Rseq,n).| < e/2
by a8,SEQ_2:def 7;
take N2;
thus for m st m >= N2 holds
|.ProjMap1(Rseq,n).m - (lim_in_cod2 Rseq).n .| < e/2
proof
let m;
assume m >=N2; then
|.ProjMap1(Rseq,n).m - lim ProjMap1(Rseq,n).| < e/2 by a9;
hence thesis by def33;
end;
end;
take N1;
thus for n st n>=N1 holds |.(lim_in_cod2 Rseq).n - z.| < e
proof
let n;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
assume a14: n>=N1; then
consider N2 be Nat such that
a13: for m st m>=N2 holds
|.ProjMap1(Rseq,n1).m - (lim_in_cod2 Rseq).n1 .| < e/2
by a12;
reconsider M=max(N2,N1) as Element of NAT by ORDINAL1:def 12;
a17: ProjMap1(Rseq,n1).M = Rseq.(n,M) by MESFUNC9:def 6;
a16: M>=N2 & M>=N1 by XXREAL_0:25;
a18: |.(lim_in_cod2 Rseq).n - z.|
<= |.(lim_in_cod2 Rseq).n - ProjMap1(Rseq,n1).M .|
+ |.Rseq.(n,M) - z.| by a17,COMPLEX1:63;
|.(lim_in_cod2 Rseq).n - ProjMap1(Rseq,n1).M .|
= |.ProjMap1(Rseq,n1).M - (lim_in_cod2 Rseq).n .| by COMPLEX1:60; then
a20: |.(lim_in_cod2 Rseq).n - ProjMap1(Rseq,n1).M .| < e/2 by a13,XXREAL_0:25;
|.Rseq.(n1,M) - z.| < e/2 by a15,a16,a14; then
|.(lim_in_cod2 Rseq).n - ProjMap1(Rseq,n1).M .|
+ |.Rseq.(n,M) - z.| < e/2 + e/2 by a20,XREAL_1:8;
hence |.(lim_in_cod2 Rseq).n - z.| < e by a18,XXREAL_0:2;
end;
end; then
a21:lim_in_cod2 Rseq is convergent by SEQ_2:def 6;
for e st 0<e
ex N st for n st n>=N holds |.(lim_in_cod2 Rseq).n - P-lim Rseq.| < e
proof
let e;
assume a22: 0<e; then
consider N1 be Nat such that
a23: for n,m st n>=N1 & m>=N1 holds |.Rseq.(n,m)-P-lim Rseq.| < e/2 by a1,def6;
take N = N1;
hereby let n;
assume n>=N; then
a27: for m st m >= N1 holds |.Rseq.(n,m) - P-lim Rseq.| < e/2 by a23;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
ProjMap1(Rseq,n1) is convergent by a1; then
consider N3 be Nat such that
a29: for m st m>=N3 holds
|.ProjMap1(Rseq,n1).m - lim ProjMap1(Rseq,n1).| < e/2
by a22,SEQ_2:def 7;
reconsider M = max(N1,N3) as Element of NAT by ORDINAL1:def 12;
a31: |.Rseq.(n,M) - P-lim Rseq.| < e/2 by a27,XXREAL_0:25;
ProjMap1(Rseq,n1).M = Rseq.(n,M) by MESFUNC9:def 6; then
|.Rseq.(n,M) - lim ProjMap1(Rseq,n1).| < e/2 by a29,XXREAL_0:25; then
|.Rseq.(n,M) - (lim_in_cod2 Rseq).n .| < e/2 by def33; then
|.(lim_in_cod2 Rseq).n - Rseq.(n,M).| < e/2 by COMPLEX1:60; then
a32: |.(lim_in_cod2 Rseq).n - Rseq.(n,M).| + |.Rseq.(n,M) - P-lim Rseq.|
< e/2 + e/2 by a31,XREAL_1:8;
|.(lim_in_cod2 Rseq).n - P-lim Rseq.|
<= |.(lim_in_cod2 Rseq).n - Rseq.(n,M).|
+ |. Rseq.(n,M) - P-lim Rseq.| by COMPLEX1:63;
hence |.(lim_in_cod2 Rseq).n - P-lim Rseq.| < e by a32,XXREAL_0:2;
end;
end;
hence thesis by a21,def35;
end;
registration
let Pseq1 be P-convergent convergent_in_cod1 Function of [:NAT,NAT:],REAL;
cluster lim_in_cod1 Pseq1 -> convergent;
coherence
proof
Pseq1 is P-convergent; then
consider z be Real such that
a3: for e st 0<e
ex N1 be Nat st
for n,m st n>=N1 & m>=N1 holds |.Pseq1.(n,m)-z.| < e;
for e st 0<e
ex N st for n st n>=N holds |.(lim_in_cod1 Pseq1).n - z.| < e
proof
let e;
assume a8: 0 < e; then
consider N1 be Nat such that
a15: for n,m st n>=N1 & m>=N1 holds |.Pseq1.(n,m)-z.| < e/2 by a3;
a12:for n be Element of NAT st n >= N1 holds
ex N2 be Nat st
for m st m>=N2 holds
|.ProjMap2(Pseq1,n).m - (lim_in_cod1 Pseq1).n .| < e/2
proof
let n be Element of NAT;
assume n >= N1;
Pseq1 is convergent_in_cod1; then
ProjMap2(Pseq1,n) is convergent; then
consider N2 be Nat such that
a9: for m st m>=N2 holds
|.ProjMap2(Pseq1,n).m - lim ProjMap2(Pseq1,n).| < e/2
by a8,SEQ_2:def 7;
take N2;
thus for m st m >= N2 holds
|.ProjMap2(Pseq1,n).m - (lim_in_cod1 Pseq1).n .| < e/2
proof
let m;
assume m >=N2; then
|.ProjMap2(Pseq1,n).m - lim ProjMap2(Pseq1,n).| < e/2 by a9;
hence thesis by def32;
end;
end;
take N1;
thus for n st n>=N1 holds |.(lim_in_cod1 Pseq1).n - z.| < e
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
assume a14: n>=N1; then
consider N2 be Nat such that
a13: for m st m>=N2 holds
|.ProjMap2(Pseq1,n1).m - (lim_in_cod1 Pseq1).n .| < e/2 by a12;
reconsider M=max(N2,N1) as Element of NAT by ORDINAL1:def 12;
a17: ProjMap2(Pseq1,n1).M = Pseq1.(M,n) by MESFUNC9:def 7;
a16: M>=N2 & M>=N1 by XXREAL_0:25;
a18: |.(lim_in_cod1 Pseq1).n - z.|
<= |.(lim_in_cod1 Pseq1).n - ProjMap2(Pseq1,n1).M .|
+ |.Pseq1.(M,n) - z.| by a17,COMPLEX1:63;
|.(lim_in_cod1 Pseq1).n - ProjMap2(Pseq1,n1).M .|
= |.ProjMap2(Pseq1,n1).M - (lim_in_cod1 Pseq1).n .| by COMPLEX1:60; then
a20: |.(lim_in_cod1 Pseq1).n - ProjMap2(Pseq1,n1).M .| < e/2
by a13,XXREAL_0:25;
|.Pseq1.(M,n1) - z.| < e/2 by a15,a16,a14; then
|.(lim_in_cod1 Pseq1).n - ProjMap2(Pseq1,n1).M .|
+ |.Pseq1.(M,n) - z.| < e/2 + e/2 by a20,XREAL_1:8;
hence |.(lim_in_cod1 Pseq1).n - z.| < e by a18,XXREAL_0:2;
end;
end;
hence lim_in_cod1 Pseq1 is convergent by SEQ_2:def 6;
end;
end;
theorem
Rseq is P-convergent convergent_in_cod1 implies
P-lim Rseq = cod1_major_iterated_lim Rseq
proof
assume a1: Rseq is P-convergent convergent_in_cod1; then
consider z be Real such that
a3: for e st 0<e
ex N1 be Nat st
for n,m st n>=N1 & m>=N1 holds |.Rseq.(n,m)-z.| < e;
for e st 0<e
ex N st for n st n>=N holds |.(lim_in_cod1 Rseq).n - z.| < e
proof
let e;
assume a8: 0 < e; then
consider N1 be Nat such that
a15: for n,m st n>=N1 & m>=N1 holds |.Rseq.(n,m)-z.| < e/2 by a3;
a12:for n be Element of NAT st n >= N1 holds
ex N2 be Nat st
for m st m>=N2 holds |.ProjMap2(Rseq,n).m - (lim_in_cod1 Rseq).n .| < e/2
proof
let n be Element of NAT;
assume n >= N1;
ProjMap2(Rseq,n) is convergent by a1; then
consider N2 be Nat such that
a9: for m st m>=N2 holds |.ProjMap2(Rseq,n).m - lim ProjMap2(Rseq,n).| < e/2
by a8,SEQ_2:def 7;
take N2;
thus for m st m >= N2 holds
|.ProjMap2(Rseq,n).m - (lim_in_cod1 Rseq).n .| < e/2
proof
let m;
assume m >=N2; then
|.ProjMap2(Rseq,n).m - lim ProjMap2(Rseq,n).| < e/2 by a9;
hence thesis by def32;
end;
end;
take N1;
thus for n st n>=N1 holds |.(lim_in_cod1 Rseq).n - z.| < e
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
assume a14: n>=N1; then
consider N2 be Nat such that
a13: for m st m>=N2 holds
|.ProjMap2(Rseq,n1).m - (lim_in_cod1 Rseq).n .| < e/2 by a12;
reconsider M=max(N2,N1) as Element of NAT by ORDINAL1:def 12;
a17: ProjMap2(Rseq,n1).M = Rseq.(M,n) by MESFUNC9:def 7;
a16: M>=N2 & M>=N1 by XXREAL_0:25;
a18: |.(lim_in_cod1 Rseq).n - z.|
<= |.(lim_in_cod1 Rseq).n - ProjMap2(Rseq,n1).M .|
+ |.Rseq.(M,n) - z.| by a17,COMPLEX1:63;
|.(lim_in_cod1 Rseq).n - ProjMap2(Rseq,n1).M .|
= |.ProjMap2(Rseq,n1).M - (lim_in_cod1 Rseq).n .| by COMPLEX1:60; then
a20: |.(lim_in_cod1 Rseq).n - ProjMap2(Rseq,n1).M .| < e/2 by a13,XXREAL_0:25;
|.Rseq.(M,n1) - z.| < e/2 by a15,a16,a14; then
|.(lim_in_cod1 Rseq).n - ProjMap2(Rseq,n1).M .|
+ |.Rseq.(M,n) - z.| < e/2 + e/2 by a20,XREAL_1:8;
hence |.(lim_in_cod1 Rseq).n - z.| < e by a18,XXREAL_0:2;
end;
end; then
a21:lim_in_cod1 Rseq is convergent by SEQ_2:def 6;
for e st 0<e
ex N st for n st n>=N holds |.(lim_in_cod1 Rseq).n - P-lim Rseq.| < e
proof
let e;
assume a22: 0<e; then
consider N1 be Nat such that
a23: for n,m st n>=N1 & m>=N1 holds
|.Rseq.(n,m)-P-lim Rseq.| < e/2 by a1,def6;
take N = N1;
hereby let n;
assume n>=N; then
a27: for m st m >= N1 holds |.Rseq.(m,n) - P-lim Rseq.| < e/2 by a23;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
ProjMap2(Rseq,n1) is convergent by a1; then
consider N3 be Nat such that
a29: for m st m>=N3 holds
|.ProjMap2(Rseq,n1).m - lim ProjMap2(Rseq,n1).| < e/2
by a22,SEQ_2:def 7;
reconsider M = max(N1,N3) as Element of NAT by ORDINAL1:def 12;
a31: |.Rseq.(M,n) - P-lim Rseq.| < e/2 by a27,XXREAL_0:25;
ProjMap2(Rseq,n1).M = Rseq.(M,n) by MESFUNC9:def 7; then
|.Rseq.(M,n) - lim ProjMap2(Rseq,n1).| < e/2 by a29,XXREAL_0:25; then
|.Rseq.(M,n) - (lim_in_cod1 Rseq).n .| < e/2 by def32; then
|.(lim_in_cod1 Rseq).n - Rseq.(M,n).| < e/2 by COMPLEX1:60; then
a32: |.(lim_in_cod1 Rseq).n - Rseq.(M,n).| + |.Rseq.(M,n) - P-lim Rseq.|
< e/2 + e/2 by a31,XREAL_1:8;
|.(lim_in_cod1 Rseq).n - P-lim Rseq.|
<= |.(lim_in_cod1 Rseq).n - Rseq.(M,n).|
+ |.Rseq.(M,n) - P-lim Rseq.| by COMPLEX1:63;
hence |.(lim_in_cod1 Rseq).n - P-lim Rseq.| < e by a32,XXREAL_0:2;
end;
end;
hence thesis by a21,def34;
end;
LM112:
Rseq is non-decreasing bounded_above implies
Rseq is P-convergent convergent_in_cod1 convergent_in_cod2
proof
assume that
a1: Rseq is non-decreasing and
a2: Rseq is bounded_above;
reconsider M = sup(Rseq.: [:NAT,NAT:]) as Element of REAL by a2,XXREAL_2:16;
b2:[:NAT,NAT:] = dom Rseq by FUNCT_2:def 1; then
b3:rng Rseq = Rseq.: [:NAT,NAT:] by RELAT_1:113;
a3:for e st 0<e ex N st Rseq.(N,N) > M-e
proof
let e;
assume a4: 0<e;
assume a7: for n holds Rseq.(n,n) <= M-e;
now let a be ExtReal;
assume a in Rseq.: [:NAT,NAT:]; then
consider x be object such that
a5: x in dom Rseq & a = Rseq.x by b3,FUNCT_1:def 3;
consider i,j be object such that
a6: i in NAT & j in NAT & x = [i,j] by a5,ZFMISC_1:def 2;
reconsider i,j as Nat by a6;
a0: max(i,j) is Nat by TARSKI:1;
max(i,j) >= i & max(i,j) >= j by XXREAL_0:25; then
a8: Rseq.(max(i,j),max(i,j)) >= Rseq.(i,j) by a1,a0;
Rseq.(max(i,j),max(i,j)) <= M-e by a7,a0;
hence a <= M-e by a5,a6,a8,XXREAL_0:2;
end; then
M-e is UpperBound of Rseq.: [:NAT,NAT:] by XXREAL_2:def 1;
hence contradiction by a4,XREAL_1:44,XXREAL_2:def 3;
end;
for e st 0<e
ex N st for n,m st n>=N & m>=N holds |.Rseq.(n,m) - M.| < e
proof
let e;
assume a5: 0<e; then
consider N such that
a10: Rseq.(N,N) > M - e by a3;
take N;
hereby let n,m;
assume n>=N & m>=N; then
a11: Rseq.(N,N) <= Rseq.(n,m) by a1;
n in NAT & m in NAT by ORDINAL1:def 12; then
[n,m] in [:NAT,NAT:] by ZFMISC_1:def 2; then
a12: Rseq.(n,m) <= M by b2,b3,FUNCT_1:3,XXREAL_2:4;
M < M+e by a5,XREAL_1:29; then
M - e < Rseq.(n,m) & Rseq.(n,m) < M + e by a10,a11,a12,XXREAL_0:2;
hence |.Rseq.(n,m) - M.| < e by RINFSUP1:1;
end;
end;
hence Rseq is P-convergent;
for m be Element of NAT holds ProjMap2(Rseq,m) is convergent
proof
let m be Element of NAT;
NAT = dom ProjMap2(Rseq,m) by FUNCT_2:def 1; then
c3: rng ProjMap2(Rseq,m) = ProjMap2(Rseq,m).:NAT by RELAT_1:113;
now let a be object;
assume a in ProjMap2(Rseq,m).:NAT; then
consider i be object such that
c4: i in dom ProjMap2(Rseq,m) & a = ProjMap2(Rseq,m).i by c3,FUNCT_1:def 3;
reconsider i as Element of NAT by c4;
[i,m] in [:NAT,NAT:] by ZFMISC_1:def 2; then
Rseq.(i,m) in Rseq.: [:NAT,NAT:] by b2,b3,FUNCT_1:3;
hence a in Rseq.: [:NAT,NAT:] by c4,MESFUNC9:def 7;
end;
then
c5: ProjMap2(Rseq,m) is bounded_above by a2,XXREAL_2:43,TARSKI:def 3;
now let n;
n is Element of NAT by ORDINAL1:def 12; then
c6: ProjMap2(Rseq,m).n = Rseq.(n,m) & ProjMap2(Rseq,m).(n+1) = Rseq.(n+1,m)
by MESFUNC9:def 7;
n<=n+1 by NAT_1:11;
hence ProjMap2(Rseq,m).n <= ProjMap2(Rseq,m).(n+1) by a1,c6;
end; then
ProjMap2(Rseq,m) is non-decreasing by SEQM_3:def 8;
hence ProjMap2(Rseq,m) is convergent by c5;
end;
hence Rseq is convergent_in_cod1;
for m be Element of NAT holds ProjMap1(Rseq,m) is convergent
proof
let m be Element of NAT;
NAT = dom ProjMap1(Rseq,m) by FUNCT_2:def 1; then
c3: rng ProjMap1(Rseq,m) = ProjMap1(Rseq,m).:NAT by RELAT_1:113;
now let a be object;
assume a in ProjMap1(Rseq,m).:NAT; then
consider i be object such that
c4: i in dom ProjMap1(Rseq,m) & a = ProjMap1(Rseq,m).i by c3,FUNCT_1:def 3;
reconsider i as Element of NAT by c4;
[m,i] in [:NAT,NAT:] by ZFMISC_1:def 2; then
Rseq.(m,i) in Rseq.: [:NAT,NAT:] by b2,b3,FUNCT_1:3;
hence a in Rseq.: [:NAT,NAT:] by c4,MESFUNC9:def 6;
end; then
c5: ProjMap1(Rseq,m) is bounded_above by a2,XXREAL_2:43,TARSKI:def 3;
now let n;
n is Element of NAT by ORDINAL1:def 12; then
c6: ProjMap1(Rseq,m).n = Rseq.(m,n) & ProjMap1(Rseq,m).(n+1) = Rseq.(m,n+1)
by MESFUNC9:def 6;
n<=n+1 by NAT_1:11;
hence ProjMap1(Rseq,m).n <= ProjMap1(Rseq,m).(n+1) by a1,c6;
end; then
ProjMap1(Rseq,m) is non-decreasing by SEQM_3:def 8;
hence ProjMap1(Rseq,m) is convergent by c5;
end;
hence Rseq is convergent_in_cod2;
end;
registration
cluster non-decreasing bounded_above ->
P-convergent convergent_in_cod1 convergent_in_cod2
for Function of [:NAT,NAT:],REAL;
coherence by LM112;
end;
LM113:
Rseq is non-increasing bounded_below implies
Rseq is P-convergent convergent_in_cod1 convergent_in_cod2
proof
assume that
a1: Rseq is non-increasing and
a2: Rseq is bounded_below;
reconsider M = inf(Rseq.: [:NAT,NAT:]) as Element of REAL by a2,XXREAL_2:15;
b2:[:NAT,NAT:] = dom Rseq by FUNCT_2:def 1; then
b3:rng Rseq = Rseq.: [:NAT,NAT:] by RELAT_1:113;
a3:for e st 0<e ex N st Rseq.(N,N) < M+e
proof
let e;
assume a4: 0<e;
assume a7: for n holds Rseq.(n,n) >= M+e;
now let a be ExtReal;
assume a in Rseq.: [:NAT,NAT:]; then
consider x be object such that
a5: x in dom Rseq & a = Rseq.x by b3,FUNCT_1:def 3;
consider i,j be object such that
a6: i in NAT & j in NAT & x = [i,j] by a5,ZFMISC_1:def 2;
reconsider i,j as Nat by a6;
a0: max(i,j) is Nat by TARSKI:1;
max(i,j) >= i & max(i,j) >= j by XXREAL_0:25; then
a8: Rseq.(max(i,j),max(i,j)) <= Rseq.(i,j) by a1,a0;
Rseq.(max(i,j),max(i,j)) >= M+e by a7,a0;
hence a >= M+e by a5,a6,a8,XXREAL_0:2;
end; then
M+e is LowerBound of Rseq.: [:NAT,NAT:] by XXREAL_2:def 2;
hence contradiction by a4,XREAL_1:29,XXREAL_2:def 4;
end;
for e st 0<e
ex N st for n,m st n>=N & m>=N holds |.Rseq.(n,m) - M.| < e
proof
let e;
assume a5: 0<e; then
consider N such that
a10: Rseq.(N,N) < M+e by a3;
take N;
hereby let n,m;
assume n>=N & m>=N; then
a11: Rseq.(N,N) >= Rseq.(n,m) by a1;
n in NAT & m in NAT by ORDINAL1:def 12; then
[n,m] in [:NAT,NAT:] by ZFMISC_1:def 2; then
a12: Rseq.(n,m) >= M by b2,b3,FUNCT_1:3,XXREAL_2:3;
M > M-e by a5,XREAL_1:44; then
M - e < Rseq.(n,m) & Rseq.(n,m) < M + e by a10,a11,a12,XXREAL_0:2;
hence |.Rseq.(n,m) - M.| < e by RINFSUP1:1;
end;
end;
hence Rseq is P-convergent;
for m be Element of NAT holds ProjMap2(Rseq,m) is convergent
proof
let m be Element of NAT;
NAT = dom ProjMap2(Rseq,m) by FUNCT_2:def 1; then
c3: rng ProjMap2(Rseq,m) = ProjMap2(Rseq,m).:NAT by RELAT_1:113;
now let a be object;
assume a in ProjMap2(Rseq,m).:NAT; then
consider i be object such that
c4: i in dom ProjMap2(Rseq,m) & a = ProjMap2(Rseq,m).i by c3,FUNCT_1:def 3;
reconsider i as Element of NAT by c4;
[i,m] in [:NAT,NAT:] by ZFMISC_1:def 2; then
Rseq.(i,m) in Rseq.: [:NAT,NAT:] by b2,b3,FUNCT_1:3;
hence a in Rseq.: [:NAT,NAT:] by c4,MESFUNC9:def 7;
end; then
c5: ProjMap2(Rseq,m) is bounded_below by a2,XXREAL_2:44,TARSKI:def 3;
now let n;
n is Element of NAT by ORDINAL1:def 12; then
c6: ProjMap2(Rseq,m).n = Rseq.(n,m) & ProjMap2(Rseq,m).(n+1) = Rseq.(n+1,m)
by MESFUNC9:def 7;
n<=n+1 by NAT_1:11;
hence ProjMap2(Rseq,m).n >= ProjMap2(Rseq,m).(n+1) by a1,c6;
end; then
ProjMap2(Rseq,m) is non-increasing by SEQM_3:def 9;
hence ProjMap2(Rseq,m) is convergent by c5;
end;
hence Rseq is convergent_in_cod1;
for m be Element of NAT holds ProjMap1(Rseq,m) is convergent
proof
let m be Element of NAT;
NAT = dom ProjMap1(Rseq,m) by FUNCT_2:def 1; then
c3: rng ProjMap1(Rseq,m) = ProjMap1(Rseq,m).:NAT by RELAT_1:113;
now let a be object;
assume a in ProjMap1(Rseq,m).:NAT; then
consider i be object such that
c4: i in dom ProjMap1(Rseq,m) & a = ProjMap1(Rseq,m).i by c3,FUNCT_1:def 3;
reconsider i as Element of NAT by c4;
[m,i] in [:NAT,NAT:] by ZFMISC_1:def 2; then
Rseq.(m,i) in Rseq.: [:NAT,NAT:] by b2,b3,FUNCT_1:3;
hence a in Rseq.: [:NAT,NAT:] by c4,MESFUNC9:def 6;
end; then
c5: ProjMap1(Rseq,m) is bounded_below by a2,XXREAL_2:44,TARSKI:def 3;
now let n;
n is Element of NAT by ORDINAL1:def 12; then
c6: ProjMap1(Rseq,m).n = Rseq.(m,n) & ProjMap1(Rseq,m).(n+1) = Rseq.(m,n+1)
by MESFUNC9:def 6;
n<=n+1 by NAT_1:11;
hence ProjMap1(Rseq,m).n >= ProjMap1(Rseq,m).(n+1) by a1,c6;
end; then
ProjMap1(Rseq,m) is non-increasing by SEQM_3:def 9;
hence ProjMap1(Rseq,m) is convergent by c5;
end;
hence Rseq is convergent_in_cod2;
end;
registration
cluster non-increasing bounded_below ->
P-convergent convergent_in_cod1 convergent_in_cod2
for Function of [:NAT,NAT:],REAL;
coherence by LM113;
end;
theorem
Rseq is uniformly_convergent_in_cod1 & lim_in_cod1 Rseq is convergent implies
Rseq is P-convergent & P-lim Rseq = cod1_major_iterated_lim Rseq
proof
assume that
a3: Rseq is uniformly_convergent_in_cod1 and
a2: lim_in_cod1 Rseq is convergent;
a4:now let e be Real;
assume a5: 0<e; then
consider N1 be Nat such that
a6: for m st m >= N1 holds
for n holds |.Rseq.(n,m) - (lim_in_cod1 Rseq).n .| < e/2 by a3;
consider z be Real such that
a7: for e st e>0
ex N2 be Nat st
for m st m>=N2 holds |.(lim_in_cod1 Rseq).m - z.| < e by a2,SEQ_2:def 6;
a8: z = cod1_major_iterated_lim Rseq by a2,a7,def34;
consider N2 be Nat such that
a9: for n st n>=N2 holds |.(lim_in_cod1 Rseq).n - z.| < e/2 by a5,a7;
set N = max(N1,N2);
a0: N is Nat by TARSKI:1;
for n,m st n>=N & m>=N holds
|.Rseq.(n,m) - cod1_major_iterated_lim Rseq.| < e
proof
let n,m;
assume a10: n>=N & m>=N;
N >= N1 & N >= N2 by XXREAL_0:25; then
n >= N2 & m >= N1 by a10,XXREAL_0:2; then
|.Rseq.(n,m) - (lim_in_cod1 Rseq).n .| <e/2
& |.(lim_in_cod1 Rseq).n - z.| < e/2 by a6,a9; then
a12: |.Rseq.(n,m) - (lim_in_cod1 Rseq).n .|
+ |.(lim_in_cod1 Rseq).n - z.| < e/2 + e/2 by XREAL_1:8;
|.Rseq.(n,m) - cod1_major_iterated_lim Rseq.|
<= |.Rseq.(n,m) - (lim_in_cod1 Rseq).n .|
+ |.(lim_in_cod1 Rseq).n - cod1_major_iterated_lim Rseq.|
by COMPLEX1:63;
hence |.Rseq.(n,m) - cod1_major_iterated_lim Rseq.| < e
by a8,a12,XXREAL_0:2;
end;
hence ex N st for n,m st n>=N & m>=N holds
|.Rseq.(n,m) - cod1_major_iterated_lim Rseq.| < e by a0;
end;
hence Rseq is P-convergent;
hence thesis by a4,def6;
end;
theorem
Rseq is uniformly_convergent_in_cod2 & lim_in_cod2 Rseq is convergent implies
Rseq is P-convergent & P-lim Rseq = cod2_major_iterated_lim Rseq
proof
assume that
a3: Rseq is uniformly_convergent_in_cod2 and
a2: lim_in_cod2 Rseq is convergent;
a4:now let e;
assume a5: 0<e; then
consider N1 be Nat such that
a6: for n st n >= N1 holds
for m holds |.Rseq.(n,m) - (lim_in_cod2 Rseq).m .| < e/2 by a3;
consider z be Real such that
a7: for e st e>0
ex N2 be Nat st
for n st n>=N2 holds
|.(lim_in_cod2 Rseq).n - z.| < e by a2,SEQ_2:def 6;
a8: z = cod2_major_iterated_lim Rseq by a2,a7,def35;
consider N2 be Nat such that
a9: for n st n>=N2 holds |.(lim_in_cod2 Rseq).n - z.| < e/2 by a5,a7;
set N = max(N1,N2);
a0: N is Nat by TARSKI:1;
for n,m st n>=N & m>=N holds
|.Rseq.(n,m) - cod2_major_iterated_lim Rseq.| < e
proof
let n,m;
assume a10: n>=N & m>=N;
N >= N1 & N >= N2 by XXREAL_0:25; then
n >= N1 & m >= N2 by a10,XXREAL_0:2; then
|.Rseq.(n,m) - (lim_in_cod2 Rseq).m .| <e/2
& |.(lim_in_cod2 Rseq).m - z.| < e/2 by a6,a9; then
a12: |.Rseq.(n,m) - (lim_in_cod2 Rseq).m .|
+ |.(lim_in_cod2 Rseq).m - z.| < e/2 + e/2 by XREAL_1:8;
|.Rseq.(n,m) - cod2_major_iterated_lim Rseq.|
<= |.Rseq.(n,m) - (lim_in_cod2 Rseq).m .|
+ |.(lim_in_cod2 Rseq).m - cod2_major_iterated_lim Rseq.|
by COMPLEX1:63;
hence |.Rseq.(n,m) - cod2_major_iterated_lim Rseq.| < e
by a8,a12,XXREAL_0:2;
end;
hence ex N st
for n,m st n>=N & m>=N holds
|.Rseq.(n,m) - cod2_major_iterated_lim Rseq.| < e by a0;
end;
hence Rseq is P-convergent;
hence thesis by a4,def6;
end;
definition
let Rseq;
attr Rseq is Cauchy means
for e be Real st e>0
ex N be Nat st
for n1,n2,m1,m2 be Nat st N<=n1 & n1<=n2 & N<=m1 & m1<=m2
holds |.Rseq.(n2,m2) - Rseq.(n1,m1).| < e;
end;
theorem
Rseq is P-convergent iff Rseq is Cauchy
proof
hereby assume a1: Rseq is P-convergent;
now let e;
assume a2: e > 0;
consider z be Real such that
a3: for e st 0<e
ex N st
for n,m st n>=N & m>=N holds |.Rseq.(n,m) - z.| < e by a1;
consider N such that
a4: for n,m st n>=N & m>=N holds |.Rseq.(n,m) - z.| < e/2 by a2,a3;
now let n1,n2,m1,m2 be Nat;
assume b1: N<=n1 & n1<=n2 & N<=m1 & m1<=m2; then
N<=n2 & N<=m2 by XXREAL_0:2; then
|.Rseq.(n1,m1) - z.| < e/2 & |.Rseq.(n2,m2) - z.| < e/2 by a4,b1; then
|.Rseq.(n2,m2) - z.| + |.Rseq.(n1,m1) - z.| < e/2 + e/2
by XREAL_1:8; then
a5: |.Rseq.(n2,m2) - z.| + |.z - Rseq.(n1,m1).| < e by COMPLEX1:60;
|.Rseq.(n2,m2) - Rseq.(n1,m1).|
<= |.Rseq.(n2,m2) - z.| + |.z - Rseq.(n1,m1).| by COMPLEX1:63;
hence |.Rseq.(n2,m2) - Rseq.(n1,m1).| < e by a5,XXREAL_0:2;
end;
hence ex N st
for n1,n2,m1,m2 be Nat st N<=n1 & n1<=n2 & N<=m1 & m1<=m2
holds |.Rseq.(n2,m2) - Rseq.(n1,m1).| < e;
end;
hence Rseq is Cauchy;
end;
assume a6: Rseq is Cauchy;
deffunc F(Element of NAT) = Rseq.($1,$1);
consider seq be Function of NAT,REAL such that
a7: for n be Element of NAT holds seq.n = F(n) from FUNCT_2:sch 4;
reconsider seq as Real_Sequence;
now let e;
assume e > 0; then
consider N such that
a8: for n1,n2,m1,m2 be Nat st N<=n1 & n1<=n2 & N<=m1 & m1<=m2
holds |. Rseq.(n2,m2) - Rseq.(n1,m1).| < e by a6;
take N;
hereby let n;
c1: n is Element of NAT & N is Element of NAT by ORDINAL1:def 12;
assume n>=N; then
|. Rseq.(n,n) - Rseq.(N,N).| < e by a8; then
|. seq.n - Rseq.(N,N).| < e by a7,c1;
hence |. seq.n - seq.N .| < e by a7,c1;
end;
end; then
a11: seq is convergent by SEQ_4:41;
reconsider z = lim seq as Complex;
for e st 0<e
ex N st for n,m st n>=N & m>=N holds |.Rseq.(n,m) - z.| < e
proof
let e;
assume a12: 0<e; then
consider N1 be Nat such that
a13: for n st n>=N1 holds |. seq.n - lim seq.| < e/2 by a11,SEQ_2:def 7;
consider N2 be Nat such that
a14: for n1,n2,m1,m2 be Nat st N2<=n1 & n1<=n2 & N2<=m1 & m1<=m2
holds |. Rseq.(n2,m2) - Rseq.(n1,m1).| < e/2 by a6,a12;
reconsider N = max(N1,N2) as Nat by TARSKI:1;
take N;
hereby let n,m;
c2: N is Element of NAT by ORDINAL1:def 12;
assume a15: n>=N & m>=N;
a18: Rseq.(N,N) = seq.N by a7,c2;
N>=N1 & N>=N2 by XXREAL_0:25; then
|. Rseq.(N,N) - z.| < e/2 & |. Rseq.(n,m) - Rseq.(N,N).| < e/2
by a13,a14,a18,a15; then
b1: |. Rseq.(n,m) - Rseq.(N,N).| + |. Rseq.(N,N) - z.| < e/2+e/2
by XREAL_1:8;
|. Rseq.(n,m) - z.| <= |. Rseq.(n,m) - Rseq.(N,N).| + |. Rseq.(N,N) - z.|
by COMPLEX1:63;
hence |. Rseq.(n,m) - z.| < e by b1,XXREAL_0:2;
end;
end;
hence Rseq is P-convergent;
end;
theorem
for Rseq be Function of [:NAT,NAT:],REAL st
Rseq is non-decreasing or Rseq is non-increasing holds
Rseq is P-convergent iff Rseq is bounded_below bounded_above;
definition
let X,Y be non empty set;
let H be BinOp of Y;
let f,g be Function of X,Y;
redefine func H*(f,g) -> Function of [:X,X:],Y; :: redefines * (FINSEQOP, definition)
coherence
proof
a1:dom H = [:Y,Y:] & dom f = X & dom g = X by FUNCT_2:def 1;
a2:rng [:f,g:] c= [:Y,Y:];
dom(H*(f,g)) = dom(H*[:f,g:]) by FINSEQOP:def 4; then
dom(H*(f,g)) = dom [:f,g:] by a1,a2,RELAT_1:27; then
a3:dom(H*(f,g)) = [:X,X:] by FUNCT_2:def 1;
rng(H*(f,g)) = rng(H*[:f,g:]) by FINSEQOP:def 4; then
rng (H*(f,g)) c= rng H & rng H c= Y by RELAT_1:26,def 19;
hence H*(f,g) is Function of [:X,X:],Y by a3,FUNCT_2:2,XBOOLE_1:1;
end;
end;
theorem
multreal*(rseq1,rseq2) is convergent_in_cod1 convergent_in_cod2
& lim_in_cod1 (multreal*(rseq1,rseq2)) is convergent
& cod1_major_iterated_lim (multreal*(rseq1,rseq2)) = lim rseq1 * lim rseq2
& lim_in_cod2 (multreal*(rseq1,rseq2)) is convergent
& cod2_major_iterated_lim (multreal*(rseq1,rseq2)) = lim rseq1 * lim rseq2
& multreal*(rseq1,rseq2) is P-convergent
& P-lim (multreal*(rseq1,rseq2)) = lim rseq1 * lim rseq2
proof
set Rseq = multreal*(rseq1,rseq2);
a2:for n,m holds Rseq.(n,m) = rseq1.n * rseq2.m
proof
let n,m;
a1: n in NAT & m in NAT by ORDINAL1:def 12;
dom Rseq = [:NAT,NAT:] by FUNCT_2:def 1; then
[n,m] in dom Rseq by a1,ZFMISC_1:def 2; then
Rseq.(n,m) = multreal.(rseq1.n,rseq2.m) by FINSEQOP:77;
hence Rseq.(n,m) = rseq1.n * rseq2.m by BINOP_2:def 11;
end;
x1:for m be Element of NAT, e be Real st 0<e
ex N st
for n st n>=N holds |. ProjMap2(Rseq,m).n - (lim rseq1)*rseq2.m .| < e
proof
let m be Element of NAT, e be Real;
assume a3: 0<e;
per cases;
suppose rseq2.m <> 0; then
a4: |.rseq2.m .| > 0 by COMPLEX1:47; then
consider N such that
a5: for n st n>=N holds |. rseq1.n - lim rseq1.| < e/ |. rseq2.m .|
by a3,SEQ_2:def 7;
take N;
hereby let n;
assume n>=N; then
a6: |. rseq1.n - lim rseq1.| < e/ |. rseq2.m .| by a5;
n is Element of NAT by ORDINAL1:def 12; then
|.ProjMap2(Rseq,m).n - (lim rseq1)*rseq2.m .|
= |. Rseq.(n,m) - (lim rseq1)*rseq2.m .| by MESFUNC9:def 7
.= |. rseq1.n * rseq2.m - (lim rseq1)*rseq2.m .| by a2
.= |.(rseq1.n - lim rseq1)*rseq2.m .|
.= |. rseq1.n - lim rseq1.| * |. rseq2.m .| by COMPLEX1:65; then
|.ProjMap2(Rseq,m).n - (lim rseq1)*rseq2.m .|
< e/ |. rseq2.m .| * |. rseq2.m .| by a4,a6,XREAL_1:68;
hence |.ProjMap2(Rseq,m).n - (lim rseq1)*rseq2.m .| < e
by a4,XCMPLX_1:87;
end;
end;
suppose a7: rseq2.m = 0;
take 0;
hereby let n;
assume n >= 0;
n is Element of NAT by ORDINAL1:def 12; then
|.ProjMap2(Rseq,m).n - (lim rseq1)*rseq2.m .|
= |. Rseq.(n,m) - (lim rseq1)*rseq2.m .| by MESFUNC9:def 7
.= |. rseq1.n * rseq2.m - (lim rseq1)*rseq2.m .| by a2
.= 0 by a7,COMPLEX1:44;
hence |.ProjMap2(Rseq,m).n - (lim rseq1)*rseq2.m .| < e by a3;
end;
end;
end;
p1:for m be Element of NAT holds ProjMap2(Rseq,m) is convergent
proof
let m be Element of NAT;
for e st 0<e
ex N st for n st n>=N holds
|.ProjMap2(Rseq,m).n - (lim rseq1)*rseq2.m .| < e by x1;
hence ProjMap2(Rseq,m) is convergent by SEQ_2:def 6;
end;
hence Rseq is convergent_in_cod1;
x2:for m be Element of NAT, e be Real st 0<e
ex N st for n st n>=N holds
|. ProjMap1(Rseq,m).n - (rseq1.m)*(lim rseq2).| < e
proof
let m be Element of NAT, e be Real;
assume a3: 0<e;
per cases;
suppose rseq1.m <> 0; then
a4: |. rseq1.m .| > 0 by COMPLEX1:47; then
consider N be Nat such that
a5: for n be Nat st n>=N holds
|. rseq2.n - lim rseq2.| < e/ |. rseq1.m .| by a3,SEQ_2:def 7;
take N;
hereby let n;
assume n>=N; then
a6: |. rseq2.n - lim rseq2.| < e/ |. rseq1.m .| by a5;
n is Element of NAT by ORDINAL1:def 12; then
|. ProjMap1(Rseq,m).n - (lim rseq2)*rseq1.m .|
= |. Rseq.(m,n) - (lim rseq2)*rseq1.m .| by MESFUNC9:def 6
.= |. rseq2.n * rseq1.m - (lim rseq2)*rseq1.m .| by a2
.= |. (rseq2.n - lim rseq2)*rseq1.m .|
.= |. rseq2.n - lim rseq2.| * |. rseq1.m .| by COMPLEX1:65; then
|. ProjMap1(Rseq,m).n - (lim rseq2)*rseq1.m .|
< e/ |. rseq1.m .| * |. rseq1.m .| by a4,a6,XREAL_1:68;
hence |. ProjMap1(Rseq,m).n - (rseq1.m)*(lim rseq2).| < e
by a4,XCMPLX_1:87;
end;
end;
suppose a7: rseq1.m = 0;
take 0;
hereby let n;
assume n >= 0;
n is Element of NAT by ORDINAL1:def 12; then
|. ProjMap1(Rseq,m).n - (lim rseq2)*rseq1.m .|
= |. Rseq.(m,n) - (lim rseq2)*rseq1.m .| by MESFUNC9:def 6
.= |. rseq2.n * rseq1.m - (lim rseq2)*rseq1.m .| by a2
.= 0 by a7,COMPLEX1:44;
hence |. ProjMap1(Rseq,m).n - (rseq1.m)*(lim rseq2).| < e by a3;
end;
end;
end;
p2:for m be Element of NAT holds ProjMap1(Rseq,m) is convergent
proof
let m be Element of NAT;
for e st 0<e ex N st for n st n>=N holds
|.ProjMap1(Rseq,m).n - (rseq1.m)*(lim rseq2).| < e by x2;
hence ProjMap1(Rseq,m) is convergent by SEQ_2:def 6;
end;
hence Rseq is convergent_in_cod2;
x3:for e st 0<e ex N st for n st n>=N holds
|.(lim_in_cod1 Rseq).n - (lim rseq1)*(lim rseq2).| < e
proof
let e;
assume a3: 0<e;
a6: for n holds (lim_in_cod1 Rseq).n = (lim rseq1)*(rseq2.n)
proof
let n;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
a4: ProjMap2(Rseq,n1) is convergent by p1;
a5: (lim_in_cod1 Rseq).n = lim ProjMap2(Rseq,n1) by def32;
for e st 0<e ex N st for m st m>=N holds
|.ProjMap2(Rseq,n1).m - (lim rseq1)*rseq2.n .| < e by x1;
hence (lim_in_cod1 Rseq).n = (lim rseq1)*(rseq2.n) by a5,a4,SEQ_2:def 7;
end;
per cases by COMPLEX1:46;
suppose b1: |.lim rseq1.| > 0; then
consider N such that
a7: for n st n>=N holds |. rseq2.n - lim rseq2.| < e / |.lim rseq1.|
by a3,SEQ_2:def 7;
take N;
hereby let n;
assume n>=N; then
a8: |. rseq2.n - lim rseq2.| < e / |.lim rseq1.| by a7;
|.(lim_in_cod1 Rseq).n - (lim rseq1)*(lim rseq2).|
= |.(lim rseq1)*(rseq2.n) - (lim rseq1)*(lim rseq2).| by a6
.= |.(lim rseq1)*(rseq2.n - lim rseq2).|
.= |.lim rseq1.| * |. rseq2.n - lim rseq2.| by COMPLEX1:65;
hence |.(lim_in_cod1 Rseq).n - (lim rseq1)*(lim rseq2).| < e
by a8,b1,XREAL_1:79;
end;
end;
suppose a9: |.lim rseq1.| = 0;
take 0;
hereby let n;
assume n >= 0;
|.(lim_in_cod1 Rseq).n - (lim rseq1)*(lim rseq2).|
= |.(lim rseq1)*(rseq2.n) - (lim rseq1)*(lim rseq2).| by a6
.= |.(lim rseq1)*(rseq2.n - lim rseq2).|
.= |.lim rseq1.| * |. rseq2.n - lim rseq2.| by COMPLEX1:65
.= 0 by a9;
hence |.(lim_in_cod1 Rseq).n - (lim rseq1)*(lim rseq2).| < e by a3;
end;
end;
end;
hence lim_in_cod1 Rseq is convergent by SEQ_2:def 6;
hence cod1_major_iterated_lim Rseq = lim rseq1 * lim rseq2 by x3,def34;
x4:for e st 0<e ex N st for n st n>=N holds
|.(lim_in_cod2 Rseq).n - (lim rseq1)*(lim rseq2).| < e
proof
let e;
assume a3: 0<e;
a6: for n holds (lim_in_cod2 Rseq).n = (rseq1.n)*(lim rseq2)
proof
let n;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
a4: ProjMap1(Rseq,n1) is convergent by p2;
a5: (lim_in_cod2 Rseq).n = lim ProjMap1(Rseq,n1) by def33;
for e st 0<e ex N st for m st m>=N holds
|.ProjMap1(Rseq,n1).m - (rseq1.n)*(lim rseq2).| < e by x2;
hence (lim_in_cod2 Rseq).n = (rseq1.n)*(lim rseq2) by a5,a4,SEQ_2:def 7;
end;
per cases by COMPLEX1:46;
suppose b1: |.lim rseq2.| > 0; then
consider N such that
a7: for n st n>=N holds |. rseq1.n - lim rseq1.| < e / |.lim rseq2.|
by a3,SEQ_2:def 7;
take N;
hereby let n;
assume n>=N; then
a8: |. rseq1.n - lim rseq1.| < e / |.lim rseq2.| by a7;
|.(lim_in_cod2 Rseq).n - (lim rseq1)*(lim rseq2).|
= |.(rseq1.n)*(lim rseq2) - (lim rseq1)*(lim rseq2).| by a6
.= |.(rseq1.n - lim rseq1)*(lim rseq2).|
.= |.lim rseq2.| * |. rseq1.n - lim rseq1.| by COMPLEX1:65;
hence |.(lim_in_cod2 Rseq).n - (lim rseq1)*(lim rseq2).| < e
by a8,b1,XREAL_1:79;
end;
end;
suppose a9: |.lim rseq2.| = 0;
take 0;
hereby let n;
assume n >= 0;
|.(lim_in_cod2 Rseq).n - (lim rseq1)*(lim rseq2).|
= |.(rseq1.n)*(lim rseq2) - (lim rseq1)*(lim rseq2).| by a6
.= |.(lim rseq2)*(rseq1.n - lim rseq1).|
.= |.lim rseq2.| * |. rseq1.n - lim rseq1.| by COMPLEX1:65
.= 0 by a9;
hence |.(lim_in_cod2 Rseq).n - (lim rseq1)*(lim rseq2).| < e by a3;
end;
end;
end;
hence lim_in_cod2 Rseq is convergent by SEQ_2:def 6;
hence cod2_major_iterated_lim Rseq = lim rseq1 * lim rseq2
by x4,def35;
x5:for e st 0<e ex N st for n,m st n>=N & m>=N holds
|. Rseq.(n,m) - (lim rseq1)*(lim rseq2).| < e
proof
let e;
assume c1: 0<e;
consider K be Real such that
c2: 0 < K & for n holds |. rseq1.n .| < K by SEQ_2:3;
set b = max(K,|.lim rseq2.|);
c10:b >= K & b >= |.lim rseq2.| by XXREAL_0:25; then
consider N1 be Nat such that
c4: for n st n>=N1 holds |. rseq1.n - lim rseq1.| < e/(2*b)
by c1,c2,SEQ_2:def 7;
consider N2 be Nat such that
c5: for n st n>=N2 holds |. rseq2.n - lim rseq2.| < e/(2*b)
by c1,c2,c10,SEQ_2:def 7;
reconsider N = max(N1,N2) as Nat by TARSKI:1;
take N;
thus for n,m st n>=N & m>=N holds
|. Rseq.(n,m) - (lim rseq1)*(lim rseq2).| < e
proof
let n,m;
assume c13: n >= N & m >= N;
max(N1,N2) >= N1 & max(N1,N2) >= N2 by XXREAL_0:25; then
c6: n >= N1 & m >= N2 by c13,XXREAL_0:2;
c7: |. Rseq.(n,m) - (lim rseq1)*(lim rseq2).|
<= |. Rseq.(n,m) - (rseq1.n)*(lim rseq2).|
+ |. (rseq1.n)*(lim rseq2) - (lim rseq1)*(lim rseq2).| by COMPLEX1:63;
c11: |. rseq1.n - lim rseq1.| >= 0 & |. rseq2.m - lim rseq2.| >= 0
by COMPLEX1:46;
c12: |. rseq1.n .| < b & |.lim rseq2.| <= b by c2,c10,XXREAL_0:2;
|. Rseq.(n,m) - (rseq1.n)*(lim rseq2).|
= |.(rseq1.n)*(rseq2.m) - (rseq1.n)*(lim rseq2).| by a2
.= |.(rseq1.n)*(rseq2.m - lim rseq2).|
.= |. rseq1.n .| * |. rseq2.m - lim rseq2.| by COMPLEX1:65; then
c8: |. Rseq.(n,m) - (rseq1.n)*(lim rseq2).|
<= b * |. rseq2.m - lim rseq2.| by c11,c12,XREAL_1:64;
|. rseq2.m - lim rseq2.| < e/(2*b) by c5,c6; then
b * |. rseq2.m - lim rseq2.| < b * (e/(2*b)) by c2,c10,XREAL_1:68; then
|. Rseq.(n,m) - (rseq1.n)*(lim rseq2).| < b * (e/(2*b))
by c8,XXREAL_0:2; then
|. Rseq.(n,m) - (rseq1.n)*(lim rseq2).| < e/(2*b/b) by XCMPLX_1:81; then
c15: |. Rseq.(n,m) - (rseq1.n)*(lim rseq2).| < e/2 by c2,c10,XCMPLX_1:89;
|. (rseq1.n)*(lim rseq2) - (lim rseq1)*(lim rseq2).|
= |.(lim rseq2)*(rseq1.n - lim rseq1).|
.= |.lim rseq2.| * |. rseq1.n - lim rseq1.| by COMPLEX1:65; then
c9: |.(rseq1.n)*(lim rseq2) - (lim rseq1)*(lim rseq2).|
<= b * |. rseq1.n - lim rseq1.| by c11,XXREAL_0:25,XREAL_1:64;
|. rseq1.n - lim rseq1.| < e/(2*b) by c4,c6; then
b * |. rseq1.n - lim rseq1.| < b * (e/(2*b)) by c2,c10,XREAL_1:68; then
|.(rseq1.n)*(lim rseq2) - (lim rseq1)*(lim rseq2).| < b * (e/(2*b))
by c9,XXREAL_0:2; then
|.(rseq1.n)*(lim rseq2) - (lim rseq1)*(lim rseq2).| < e/(2*b/b)
by XCMPLX_1:81; then
|.(rseq1.n)*(lim rseq2) - (lim rseq1)*(lim rseq2).| < e/2
by c2,c10,XCMPLX_1:89; then
|. Rseq.(n,m) - (rseq1.n)*(lim rseq2).|
+ |.(rseq1.n)*(lim rseq2) - (lim rseq1)*(lim rseq2).| < e/2 + e/2
by c15,XREAL_1:8;
hence |. Rseq.(n,m) - (lim rseq1)*(lim rseq2).| < e by c7,XXREAL_0:2;
end;
end;
hence Rseq is P-convergent;
hence P-lim Rseq = lim rseq1 * lim rseq2 by x5,def6;
end;
theorem
addreal*(rseq1,rseq2) is convergent_in_cod1 convergent_in_cod2
& lim_in_cod1 (addreal*(rseq1,rseq2)) is convergent
& cod1_major_iterated_lim (addreal*(rseq1,rseq2)) = lim rseq1 + lim rseq2
& lim_in_cod2 (addreal*(rseq1,rseq2)) is convergent
& cod2_major_iterated_lim (addreal*(rseq1,rseq2)) = lim rseq1 + lim rseq2
& addreal*(rseq1,rseq2) is P-convergent
& P-lim (addreal*(rseq1,rseq2)) = lim rseq1 + lim rseq2
proof
set Rseq = addreal*(rseq1,rseq2);
a2:for n,m holds Rseq.(n,m) = rseq1.n + rseq2.m
proof
let n,m;
a1: n in NAT & m in NAT by ORDINAL1:def 12;
dom Rseq = [:NAT,NAT:] by FUNCT_2:def 1; then
[n,m] in dom Rseq by a1,ZFMISC_1:def 2; then
Rseq.(n,m) = addreal.(rseq1.n,rseq2.m) by FINSEQOP:77;
hence Rseq.(n,m) = rseq1.n + rseq2.m by BINOP_2:def 9;
end;
x1:for m be Element of NAT, e be Real st 0<e
ex N be Nat st
for n be Nat st n>=N holds
|.ProjMap2(Rseq,m).n - (lim rseq1 + rseq2.m).| < e
proof
let m be Element of NAT, e be Real;
assume 0<e; then
consider N be Nat such that
a3: for n be Nat st n>=N holds
|.rseq1.n - lim rseq1.| < e by SEQ_2:def 7;
take N;
hereby let n be Nat;
assume a4: n>=N;
n is Element of NAT by ORDINAL1:def 12; then
|.ProjMap2(Rseq,m).n - (lim rseq1 + rseq2.m).|
= |. Rseq.(n,m) - (lim rseq1 + rseq2.m).| by MESFUNC9:def 7
.= |.(rseq1.n + rseq2.m) - (lim rseq1 + rseq2.m).| by a2
.= |. rseq1.n - lim rseq1.|;
hence |. ProjMap2(Rseq,m).n - (lim rseq1 + rseq2.m).|< e
by a3,a4;
end;
end;
p1:for m be Element of NAT holds ProjMap2(Rseq,m) is convergent
proof
let m be Element of NAT;
for e st 0<e ex N st for n st n>=N holds
|. ProjMap2(Rseq,m).n - (lim rseq1 + rseq2.m).| < e by x1;
hence ProjMap2(Rseq,m) is convergent by SEQ_2:def 6;
end;
hence Rseq is convergent_in_cod1;
x2:for m be Element of NAT, e be Real st 0<e
ex N st for n st n>=N holds
|. ProjMap1(Rseq,m).n - (rseq1.m + lim rseq2).| < e
proof
let m be Element of NAT, e be Real;
assume 0<e; then
consider N such that
a3: for n st n>=N holds |. rseq2.n - lim rseq2.| < e by SEQ_2:def 7;
take N;
hereby let n;
assume a4: n>=N;
n is Element of NAT by ORDINAL1:def 12; then
|. ProjMap1(Rseq,m).n - (lim rseq2 + rseq1.m).|
= |. Rseq.(m,n) - (lim rseq2 + rseq1.m).| by MESFUNC9:def 6
.= |. rseq2.n + rseq1.m - (lim rseq2 + rseq1.m).| by a2
.= |. rseq2.n - lim rseq2.|;
hence |. ProjMap1(Rseq,m).n - (rseq1.m + lim rseq2).| < e
by a3,a4;
end;
end;
p2:for m be Element of NAT holds ProjMap1(Rseq,m) is convergent
proof
let m be Element of NAT;
for e st 0<e ex N st for n st n>=N holds
|.ProjMap1(Rseq,m).n - (rseq1.m + lim rseq2).| < e by x2;
hence ProjMap1(Rseq,m) is convergent by SEQ_2:def 6;
end;
hence Rseq is convergent_in_cod2;
x3:for e st 0<e ex N st for n st n>=N holds
|.(lim_in_cod1 Rseq).n - (lim rseq1 + lim rseq2).| < e
proof
let e;
assume 0<e; then
consider N such that
a3: for n st n>=N holds |. rseq2.n - lim rseq2.| < e by SEQ_2:def 7;
take N;
hereby let n;
assume n>=N; then
a4: |. rseq2.n - lim rseq2.| < e by a3;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
a5: ProjMap2(Rseq,n1) is convergent by p1;
a6: (lim_in_cod1 Rseq).n = lim ProjMap2(Rseq,n1) by def32;
for e st 0<e ex N st for m st m>=N holds
|. ProjMap2(Rseq,n1).m - (lim rseq1 + rseq2.n).| < e by x1; then
|.(lim_in_cod1 Rseq).n - (lim rseq1 + lim rseq2).|
= |.(lim rseq1 + rseq2.n) - (lim rseq1 + lim rseq2).|
by a5,a6,SEQ_2:def 7;
hence |. (lim_in_cod1 Rseq).n - (lim rseq1 + lim rseq2).| < e by a4;
end;
end;
hence lim_in_cod1 Rseq is convergent by SEQ_2:def 6;
hence cod1_major_iterated_lim Rseq = lim rseq1 + lim rseq2 by x3,def34;
x4:for e st 0<e ex N st for n st n>=N holds
|. (lim_in_cod2 Rseq).n - (lim rseq1 + lim rseq2).| < e
proof
let e;
assume 0<e; then
consider N such that
a3: for n st n>=N holds |. rseq1.n - lim rseq1.| < e by SEQ_2:def 7;
take N;
hereby let n;
assume n>=N; then
a4: |. rseq1.n - lim rseq1.| < e by a3;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
a5: ProjMap1(Rseq,n1) is convergent by p2;
a6: (lim_in_cod2 Rseq).n = lim ProjMap1(Rseq,n1) by def33;
for e st 0<e ex N st for m st m>=N holds
|.ProjMap1(Rseq,n1).m - (rseq1.n + lim rseq2).| < e by x2; then
|.(lim_in_cod2 Rseq).n - (lim rseq1 + lim rseq2).|
= |.(rseq1.n + lim rseq2) - (lim rseq1 + lim rseq2).|
by a5,a6,SEQ_2:def 7;
hence |.(lim_in_cod2 Rseq).n - (lim rseq1 + lim rseq2).| < e by a4;
end;
end;
hence lim_in_cod2 Rseq is convergent by SEQ_2:def 6;
hence cod2_major_iterated_lim Rseq = lim rseq1 + lim rseq2
by x4,def35;
x5:for e st 0<e ex N st for n,m st n>=N & m>=N holds
|. Rseq.(n,m) - (lim rseq1 + lim rseq2).| < e
proof
let e;
assume c1: 0<e; then
consider N1 be Nat such that
c4: for n st n>=N1 holds |. rseq1.n - lim rseq1.| < e/2 by SEQ_2:def 7;
consider N2 be Nat such that
c5: for n st n>=N2 holds |. rseq2.n - lim rseq2.| < e/2 by c1,SEQ_2:def 7;
reconsider N = max(N1,N2) as Nat by TARSKI:1;
take N;
thus for n,m st n>=N & m>=N holds
|. Rseq.(n,m) - (lim rseq1 + lim rseq2).| < e
proof
let n,m;
assume c13: n>=N & m>=N;
max(N1,N2) >= N1 & max(N1,N2) >= N2 by XXREAL_0:25; then
c6: n >= N1 & m >= N2 by c13,XXREAL_0:2;
|. Rseq.(n,m) - (lim rseq1 + lim rseq2).|
= |. rseq1.n + rseq2.m - (lim rseq1 + lim rseq2).| by a2
.= |.(rseq1.n - lim rseq1) + (rseq2.m - lim rseq2).|; then
a8: |. Rseq.(n,m) - (lim rseq1 + lim rseq2).|
<= |. rseq1.n - lim rseq1.| + |. rseq2.m - lim rseq2.| by COMPLEX1:56;
|. rseq1.n - lim rseq1.| < e/2 & |. rseq2.m - lim rseq2.| < e/2
by c4,c5,c6; then
|. rseq1.n - lim rseq1.| + |. rseq2.m - lim rseq2.| < e/2 + e/2
by XREAL_1:8;
hence |. Rseq.(n,m) - (lim rseq1 + lim rseq2).| < e by a8,XXREAL_0:2;
end;
end;
hence Rseq is P-convergent;
hence P-lim Rseq = lim rseq1 + lim rseq2 by x5,def6;
end;
lmADD:
for Rseq1,Rseq2 be Function of [:NAT,NAT:],REAL holds
dom(Rseq1+Rseq2) = [:NAT,NAT:] & dom(Rseq1-Rseq2) = [:NAT,NAT:] &
(for n,m be Nat holds
(Rseq1+Rseq2).(n,m) = Rseq1.(n,m) + Rseq2.(n,m)) &
(for n,m be Nat holds
(Rseq1-Rseq2).(n,m) = Rseq1.(n,m) - Rseq2.(n,m))
proof
let Rseq1,Rseq2 be Function of [:NAT,NAT:],REAL;
thus
a1: dom(Rseq1+Rseq2) = [:NAT,NAT:] & dom(Rseq1-Rseq2) = [:NAT,NAT:]
by FUNCT_2:def 1;
hereby let n,m;
n in NAT & m in NAT by ORDINAL1:def 12;
hence (Rseq1+Rseq2).(n,m) = Rseq1.(n,m) + Rseq2.(n,m)
by VALUED_1:def 1,a1,ZFMISC_1:87;
end;
hereby let n,m;
n in NAT & m in NAT by ORDINAL1:def 12;
hence (Rseq1-Rseq2).(n,m) = Rseq1.(n,m) - Rseq2.(n,m)
by VALUED_1:13,a1,ZFMISC_1:87;
end;
end;
theorem
Rseq1 is P-convergent & Rseq2 is P-convergent implies
Rseq1+Rseq2 is P-convergent & P-lim(Rseq1+Rseq2) = P-lim Rseq1 + P-lim Rseq2
proof
assume a1: Rseq1 is P-convergent & Rseq2 is P-convergent;
a2:now let e;
assume a4: 0 < e; then
consider N1 be Nat such that
a5: for n,m st n>=N1 & m>=N1 holds
|. Rseq1.(n,m) - P-lim Rseq1.| < e/2 by a1,def6;
consider N2 be Nat such that
a6: for n,m st n>=N2 & m>=N2 holds
|. Rseq2.(n,m) - P-lim Rseq2.| < e/2 by a1,a4,def6;
reconsider N=max(N1,N2) as Nat by TARSKI:1;
take N;
now let n,m;
assume a8: n>=N & m>=N;
N>=N1 & N>=N2 by XXREAL_0:25; then
n>=N1 & n>=N2 & m>=N1 & m>=N2 by a8,XXREAL_0:2; then
|. Rseq1.(n,m) - P-lim Rseq1.| < e/2 &
|. Rseq2.(n,m) - P-lim Rseq2.| < e/2 by a5,a6; then
a9: |. Rseq1.(n,m) - P-lim Rseq1.| + |. Rseq2.(n,m) - P-lim Rseq2.| < e/2+e/2
by XREAL_1:8;
(Rseq1+Rseq2).(n,m) = Rseq1.(n,m) + Rseq2.(n,m) by lmADD; then
(Rseq1+Rseq2).(n,m) - (P-lim Rseq1 + P-lim Rseq2)
= (Rseq1.(n,m) - P-lim Rseq1) + (Rseq2.(n,m) - P-lim Rseq2); then
|.(Rseq1+Rseq2).(n,m) - (P-lim Rseq1 + P-lim Rseq2).|
<= |. Rseq1.(n,m) - P-lim Rseq1.|
+ |. Rseq2.(n,m) - P-lim Rseq2.| by COMPLEX1:56;
hence |.(Rseq1+Rseq2).(n,m) - (P-lim Rseq1 + P-lim Rseq2).| < e
by a9,XXREAL_0:2;
end;
hence for n,m be Nat st n>=N & m>=N holds
|.(Rseq1+Rseq2).(n,m) - (P-lim Rseq1 + P-lim Rseq2).| < e;
end;
hence Rseq1+Rseq2 is P-convergent;
hence thesis by a2,def6;
end;
theorem th54b:
Rseq1 is P-convergent & Rseq2 is P-convergent implies
Rseq1-Rseq2 is P-convergent & P-lim(Rseq1-Rseq2) = P-lim Rseq1 - P-lim Rseq2
proof
assume a1: Rseq1 is P-convergent & Rseq2 is P-convergent;
a2:now let e;
assume a4: 0 < e; then
consider N1 be Nat such that
a5: for n,m st n>=N1 & m>=N1 holds
|. Rseq1.(n,m) - P-lim Rseq1.| < e/2 by a1,def6;
consider N2 be Nat such that
a6: for n,m st n>=N2 & m>=N2 holds
|. Rseq2.(n,m) - P-lim Rseq2.| < e/2 by a1,a4,def6;
reconsider N=max(N1,N2) as Nat by TARSKI:1;
take N;
now let n,m;
assume a8: n>=N & m>=N;
N>=N1 & N>=N2 by XXREAL_0:25; then
n>=N1 & n>=N2 & m>=N1 & m>=N2 by a8,XXREAL_0:2; then
a10: |. Rseq1.(n,m) - P-lim Rseq1.| < e/2 &
|. Rseq2.(n,m) - P-lim Rseq2.| < e/2 by a5,a6; then
|. P-lim Rseq2 - Rseq2.(n,m).| < e/2 by COMPLEX1:60; then
a9: |. Rseq1.(n,m) - P-lim Rseq1.| + |.P-lim Rseq2 - Rseq2.(n,m) .| < e/2+e/2
by a10,XREAL_1:8;
(Rseq1-Rseq2).(n,m) = Rseq1.(n,m) - Rseq2.(n,m) by lmADD; then
(Rseq1-Rseq2).(n,m) - (P-lim Rseq1 - P-lim Rseq2)
= (Rseq1.(n,m) - P-lim Rseq1) + (P-lim Rseq2 - Rseq2.(n,m)); then
|.(Rseq1-Rseq2).(n,m) - (P-lim Rseq1 - P-lim Rseq2).|
<= |. Rseq1.(n,m) - P-lim Rseq1.|
+ |.P-lim Rseq2 - Rseq2.(n,m).| by COMPLEX1:56;
hence |. (Rseq1-Rseq2).(n,m) - (P-lim Rseq1 - P-lim Rseq2).| < e
by a9,XXREAL_0:2;
end;
hence for n,m be Nat st n>=N & m>=N holds
|.(Rseq1-Rseq2).(n,m) - (P-lim Rseq1 - P-lim Rseq2).| < e;
end;
hence Rseq1-Rseq2 is P-convergent;
hence thesis by a2,def6;
end;
lm55a:
for a be Real st
(for n,m be Nat holds Rseq.(n,m) = a) holds
Rseq is P-convergent & P-lim Rseq = a
proof
let a be Real;
assume a1: for n,m be Nat holds Rseq.(n,m) = a;
a3:now let e be Real;
assume a2: 0<e;
a4: now let n,m such that n>=0 & m>=0;
Rseq.(n,m) = a by a1;
hence |. Rseq.(n,m) - a.| < e by a2,COMPLEX1:44;
end;
reconsider N = 0 as Nat;
take N;
thus for n,m st n>=N & m>=N holds |. Rseq.(n,m) - a.| < e by a4;
end;
hence Rseq is P-convergent;
hence P-lim Rseq = a by a3,def6;
end;
theorem
for Rseq be Function of [:NAT,NAT:],REAL, r be Real st
Rseq is P-convergent holds
r(#)Rseq is P-convergent & P-lim (r(#)Rseq) = r * P-lim Rseq
proof
let Rseq be Function of [:NAT,NAT:],REAL;
let r be Real;
assume a1: Rseq is P-convergent;
a4:now assume a2: r=0;
a3: now let n,m;
(r(#)Rseq).(n,m) = r * Rseq.(n,m) by VALUED_1:6;
hence (r(#)Rseq).(n,m) = 0 by a2;
end;
hence r(#)Rseq is P-convergent by lm55a;
thus P-lim (r(#)Rseq) = 0 by a3,lm55a;
end;
now assume r <> 0; then
a5: |.r.| > 0 by COMPLEX1:47;
a7: now let e be Real;
assume 0 < e; then
consider N such that
a6: for n,m st n>=N & m>=N holds |. Rseq.(n,m) - P-lim Rseq.| < e/ |.r.|
by a1,a5,def6;
take N;
hereby let n,m;
assume n>=N & m>=N; then
|. Rseq.(n,m) - P-lim Rseq.| < e/ |.r.| by a6; then
|.r.| * |.Rseq.(n,m) - P-lim Rseq.| < e/ |.r.| * |.r.|
by a5,XREAL_1:68; then
|.r.| * |. Rseq.(n,m) - P-lim Rseq.| < |.r.| / (|.r.| / e)
by XCMPLX_1:79; then
|.r.| * |. Rseq.(n,m) - P-lim Rseq.| < e by a5,XCMPLX_1:52; then
|.r*(Rseq.(n,m) - P-lim Rseq).| < e by COMPLEX1:65; then
|.r*Rseq.(n,m) - r * P-lim Rseq.| < e;
hence |.(r(#)Rseq).(n,m) - r * P-lim Rseq.| < e by VALUED_1:6;
end;
end;
hence r(#)Rseq is P-convergent;
hence P-lim (r(#)Rseq) = r * P-lim Rseq by a7,def6;
end;
hence thesis by a4;
end;
theorem th55b:
Rseq is P-convergent &(for n,m be Nat holds Rseq.(n,m) >= r)
implies P-lim Rseq >= r
proof
assume a1: Rseq is P-convergent;
assume a2: for n,m be Nat holds Rseq.(n,m) >= r;
assume not P-lim Rseq >= r; then
r - P-lim Rseq > 0 by XREAL_1:50; then
consider N such that
a3: for n,m st n>=N & m>=N holds
|. Rseq.(n,m) - P-lim Rseq.| < r - P-lim Rseq by a1,def6;
|. Rseq.(N,N) - P-lim Rseq.| < r - P-lim Rseq by a3; then
P-lim Rseq + (r - P-lim Rseq) > Rseq.(N,N) by RINFSUP1:1;
hence contradiction by a2;
end;
theorem
Rseq1 is P-convergent & Rseq2 is P-convergent &
(for n,m be Nat holds Rseq1.(n,m) <= Rseq2.(n,m)) implies
P-lim Rseq1 <= P-lim Rseq2
proof
assume a1: Rseq1 is P-convergent & Rseq2 is P-convergent;
assume a2: for n,m be Nat holds Rseq1.(n,m) <= Rseq2.(n,m);
a3:Rseq2 - Rseq1 is P-convergent &
P-lim(Rseq2-Rseq1) = P-lim Rseq2 - P-lim Rseq1 by a1,th54b;
now let n,m;
(Rseq2-Rseq1).(n,m) = Rseq2.(n,m) - Rseq1.(n,m) by lmADD;
hence (Rseq2-Rseq1).(n,m) >= 0 by a2,XREAL_1:48;
end;
hence P-lim Rseq1 <= P-lim Rseq2 by a3,th55b,XREAL_1:49;
end;
theorem
Rseq1 is P-convergent & Rseq2 is P-convergent & P-lim Rseq1 = P-lim Rseq2 &
(for n,m be Nat holds
Rseq1.(n,m) <= Rseq.(n,m) & Rseq.(n,m) <= Rseq2.(n,m) )
implies Rseq is P-convergent & P-lim Rseq = P-lim Rseq1
proof
assume that
a1: Rseq1 is P-convergent & Rseq2 is P-convergent and
a2: P-lim Rseq1 = P-lim Rseq2 and
a3: for n,m be Nat holds
Rseq1.(n,m) <= Rseq.(n,m) & Rseq.(n,m) <= Rseq2.(n,m);
a4:for e st 0<e
ex N st for n,m st n>=N & m>=N holds |. Rseq.(n,m) - P-lim Rseq1.| < e
proof
let e;
assume a5: 0<e; then
consider N1 be Nat such that
a6: for n,m st n>=N1 & m>=N1 holds |. Rseq1.(n,m) - P-lim Rseq1.| < e
by a1,def6;
consider N2 be Nat such that
a7: for n,m st n>=N2 & m>=N2 holds |. Rseq2.(n,m) - P-lim Rseq1.| < e
by a1,a2,a5,def6;
reconsider N = max(N1,N2) as Nat by TARSKI:1;
take N;
a8: max(N1,N2) >= N1 & max(N1,N2) >= N2 by XXREAL_0:25;
hereby let n,m;
assume n>=N & m>=N; then
n>=N1 & m>=N1 & n>=N2 & m>=N2 by a8,XXREAL_0:2; then
a9: |. Rseq1.(n,m) - P-lim Rseq1.| < e & |. Rseq2.(n,m) - P-lim Rseq1.| < e
by a6,a7; then
a10: -e < - |. Rseq1.(n,m) - P-lim Rseq1.| by XREAL_1:24;
- |. Rseq1.(n,m) - P-lim Rseq1.| <= Rseq1.(n,m) - P-lim Rseq1
by ABSVALUE:4; then
a11: -e < Rseq1.(n,m) - P-lim Rseq1 by a10,XXREAL_0:2;
Rseq2.(n,m) - P-lim Rseq1 <= |. Rseq2.(n,m) - P-lim Rseq1.|
by ABSVALUE:4; then
a12: Rseq2.(n,m) - P-lim Rseq1 < e by a9,XXREAL_0:2;
a13: Rseq1.(n,m) - P-lim Rseq1 <= Rseq.(n,m) - P-lim Rseq1 &
Rseq.(n,m) - P-lim Rseq1 <= Rseq2.(n,m) - P-lim Rseq1
by a3,XREAL_1:9; then
-e < Rseq.(n,m) - P-lim Rseq1 & Rseq.(n,m) - P-lim Rseq1 < e
by a11,a12,XXREAL_0:2; then
a14: |. Rseq.(n,m) - P-lim Rseq1.| <= e by ABSVALUE:5;
-(Rseq.(n,m) - P-lim Rseq1) <> e by a3,a11,XREAL_1:9; then
|. Rseq.(n,m) - P-lim Rseq1.| <> e by a13,a12,ABSVALUE:1;
hence |. Rseq.(n,m) - P-lim Rseq1.| < e by a14,XXREAL_0:1;
end;
end;
hence Rseq is P-convergent;
hence P-lim Rseq = P-lim Rseq1 by a4,def6;
end;
definition
let X be non empty set, seq be Function of [:NAT,NAT:],X;
mode subsequence of seq -> Function of [:NAT,NAT:],X means :def9:
ex N,M be increasing sequence of NAT st
for n,m be Nat holds it.(n,m) = seq.(N.n,M.m);
existence
proof
deffunc F(object,object) = seq.((id NAT).$1,(id NAT).$2);
consider s be Function such that
a1: dom s = [:NAT,NAT:] & for n,m be object st n in NAT & m in NAT holds
s.(n,m) = F(n,m) from FUNCT_3:sch 2;
for z be object st z in [:NAT,NAT:] holds s.z in X
proof
let z be object;
assume z in [:NAT,NAT:]; then
consider n,m be object such that
a2: n in NAT & m in NAT & z = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Nat by a2;
s.z = s.(n,m) by a2; then
s.z = seq.((id NAT).n,(id NAT).m) by a1,a2;
hence s.z in X;
end; then
reconsider s as Function of [:NAT,NAT:],X by a1,FUNCT_2:3;
take s,(id NAT),(id NAT);
hereby let n,m be Nat;
n is Element of NAT & m is Element of NAT by ORDINAL1:def 12;
hence s.(n,m) = seq.((id NAT).n,(id NAT).m) by a1;
end;
end;
end;
lem01:
for seq be increasing sequence of NAT, n be Nat holds
n <= seq.n
proof
let seq be increasing sequence of NAT;
let n be Nat;
a1:seq is Real_Sequence by FUNCT_2:7,NUMBERS:19;
rng seq c= NAT by RELAT_1:def 19;
hence n <= seq.n by a1,HEINE:2;
end;
LM114:
for Rseq1 be subsequence of Rseq st Rseq is P-convergent holds
Rseq1 is P-convergent & P-lim Rseq1 = P-lim Rseq
proof
let Rseq1 be subsequence of Rseq;
assume a1: Rseq is P-convergent;
a2:for e st 0<e
ex N st for n,m st n>=N & m>=N holds |. Rseq1.(n,m) - P-lim Rseq.| < e
proof
let e;
assume 0<e; then
consider N such that
a3: for n,m st n>=N & m>=N holds |. Rseq.(n,m) - P-lim Rseq.| < e by a1,def6;
take N;
hereby let n,m;
assume a4: n>=N & m>=N;
consider I1,I2 be increasing sequence of NAT such that
a5: for n,m holds Rseq1.(n,m) = Rseq.(I1.n,I2.m) by def9;
I1.n >= n & I2.m >= m by lem01; then
I1.n >= N & I2.m >= N by a4,XXREAL_0:2; then
|. Rseq.(I1.n,I2.m) - P-lim Rseq.| < e by a3;
hence |. Rseq1.(n,m) - P-lim Rseq.| < e by a5;
end;
end;
hence Rseq1 is P-convergent;
hence P-lim Rseq1 = P-lim Rseq by a2,def6;
end;
th63d:
Rseq is convergent_in_cod1 implies
for Rseq1 be subsequence of Rseq holds Rseq1 is convergent_in_cod1
proof
assume a1: Rseq is convergent_in_cod1;
hereby let Rseq1 be subsequence of Rseq;
consider I1,I2 be increasing sequence of NAT such that
a7: for n,m holds Rseq1.(n,m) = Rseq.(I1.n,I2.m) by def9;
for m be Element of NAT holds ProjMap2(Rseq1,m) is convergent
proof
let m be Element of NAT;
reconsider m2=I2.m as Element of NAT;
a4: ProjMap2(Rseq,m2) is convergent by a1;
now let e be Real;
assume 0<e; then
consider N such that
a5: for n st n>=N holds
|.ProjMap2(Rseq,m2).n - lim ProjMap2(Rseq,m2).| < e
by a4,SEQ_2:def 7;
take N;
hereby let n;
assume a6: n >= N;
x1: I1.n is Element of NAT & n is Element of NAT by ORDINAL1:def 12;
I1.n >= n by lem01; then
I1.n >= N by a6,XXREAL_0:2; then
|.ProjMap2(Rseq,m2).(I1.n) - lim ProjMap2(Rseq,m2).| < e by a5; then
|. Rseq.(I1.n,I2.m)-lim ProjMap2(Rseq,m2).| < e
by MESFUNC9:def 7; then
|. Rseq1.(n,m) - lim ProjMap2(Rseq,m2).| < e by a7;
hence |. ProjMap2(Rseq1,m).n - lim ProjMap2(Rseq,m2).| < e
by x1,MESFUNC9:def 7;
end;
end;
hence ProjMap2(Rseq1,m) is convergent by SEQ_2:def 6;
end;
hence Rseq1 is convergent_in_cod1;
end;
end;
registration
let Pseq;
cluster -> P-convergent for subsequence of Pseq;
coherence by LM114;
end;
theorem
for Psubseq be subsequence of Pseq holds
P-lim Psubseq = P-lim Pseq by LM114;
registration
let Rseq be convergent_in_cod1 Function of [:NAT,NAT:],REAL;
cluster -> convergent_in_cod1 for subsequence of Rseq;
coherence by th63d;
end;
theorem
for Rseq1 be subsequence of Rseq st
Rseq is convergent_in_cod1 & lim_in_cod1 Rseq is convergent holds
lim_in_cod1 Rseq1 is convergent &
cod1_major_iterated_lim Rseq1 = cod1_major_iterated_lim Rseq
proof
let Rseq1 be subsequence of Rseq;
assume that
a1: Rseq is convergent_in_cod1 & lim_in_cod1 Rseq is convergent;
consider I1,I2 be increasing sequence of NAT such that
a7: for n,m be Nat holds Rseq1.(n,m) = Rseq.(I1.n,I2.m) by def9;
a8:Rseq1 is convergent_in_cod1 by a1;
a10:for e st 0<e
ex N st for m st m >= N holds
|.(lim_in_cod1 Rseq1).m - cod1_major_iterated_lim Rseq.| < e
proof
let e;
assume 0<e; then
consider N such that
a11: for m st m >= N holds
|.(lim_in_cod1 Rseq).m - cod1_major_iterated_lim Rseq.| < e by a1,def34;
take N;
hereby let m;
assume a12: m >= N;
reconsider m2 = I2.m as Element of NAT;
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
x2: ProjMap2(Rseq1,m1) is convergent by a8;
for p be Real st 0<p
ex K be Nat st
for n be Nat st n>=K holds
|.ProjMap2(Rseq1,m1).n - lim ProjMap2(Rseq,m2).| < p
proof
let p be Real;
assume b1: 0<p;
ProjMap2(Rseq,m2) is convergent by a1; then
consider K be Nat such that
b2: for n st n>=K holds |.ProjMap2(Rseq,m2).n - lim ProjMap2(Rseq,m2).| < p
by b1,SEQ_2:def 7;
take K;
hereby let n;
assume b3: n >= K;
x2: n is Element of NAT &
I1.n is Element of NAT & I2.m is Element of NAT by ORDINAL1:def 12;
I1.n >= n by lem01; then
I1.n >= K by b3,XXREAL_0:2; then
|.ProjMap2(Rseq,m2).(I1.n)-lim ProjMap2(Rseq,m2).| < p by b2; then
|. Rseq.(I1.n,I2.m)-lim ProjMap2(Rseq,m2).| <p
by MESFUNC9:def 7; then
|. Rseq1.(n,m) - lim ProjMap2(Rseq,m2).| < p by a7;
hence |. ProjMap2(Rseq1,m1).n - lim ProjMap2(Rseq,m2).| <p
by x2,MESFUNC9:def 7;
end;
end; then
c1: lim ProjMap2(Rseq1,m1) = lim ProjMap2(Rseq,m2) by x2,SEQ_2:def 7;
I2.m >= m by lem01; then
I2.m >= N by a12,XXREAL_0:2; then
a13: |.(lim_in_cod1 Rseq).(I2.m) - cod1_major_iterated_lim Rseq.| < e by a11;
(lim_in_cod1 Rseq).(I2.m) = lim ProjMap2(Rseq,m2) by def32;
hence |.(lim_in_cod1 Rseq1).m - cod1_major_iterated_lim Rseq.| < e
by def32,a13,c1;
end;
end;
hence lim_in_cod1 Rseq1 is convergent by SEQ_2:def 6;
hence thesis by a10,def34;
end;
th63c:
Rseq is convergent_in_cod2 implies
for Rseq1 be subsequence of Rseq holds Rseq1 is convergent_in_cod2
proof
assume a1: Rseq is convergent_in_cod2;
hereby let Rseq1 be subsequence of Rseq;
consider I1,I2 be increasing sequence of NAT such that
a7: for n,m holds Rseq1.(n,m) = Rseq.(I1.n,I2.m) by def9;
for m be Element of NAT holds ProjMap1(Rseq1,m) is convergent
proof
let m be Element of NAT;
reconsider m1 = I1.m as Element of NAT;
a4: ProjMap1(Rseq,m1) is convergent by a1;
now let e;
assume 0<e; then
consider N such that
a5: for n st n>=N holds
|. ProjMap1(Rseq,m1).n - lim ProjMap1(Rseq,m1).| < e
by a4,SEQ_2:def 7;
take N;
hereby let n;
assume a6: n >= N;
x2: n is Element of NAT &
I1.m is Element of NAT & I2.n is Element of NAT by ORDINAL1:def 12;
I2.n >= n by lem01; then
I2.n >= N by a6,XXREAL_0:2; then
|. ProjMap1(Rseq,m1).(I2.n) - lim ProjMap1(Rseq,m1).| < e by a5; then
|. Rseq.(I1.m,I2.n)-lim ProjMap1(Rseq,m1).| < e
by MESFUNC9:def 6; then
|. Rseq1.(m,n) - lim ProjMap1(Rseq,m1).| < e by a7;
hence |.ProjMap1(Rseq1,m).n - lim ProjMap1(Rseq,m1).| < e
by x2,MESFUNC9:def 6;
end;
end;
hence ProjMap1(Rseq1,m) is convergent by SEQ_2:def 6;
end;
hence Rseq1 is convergent_in_cod2;
end;
end;
registration
let Rseq be convergent_in_cod2 Function of [:NAT,NAT:],REAL;
cluster -> convergent_in_cod2 for subsequence of Rseq;
coherence by th63c;
end;
theorem
for Rseq1 be subsequence of Rseq st
Rseq is convergent_in_cod2 & lim_in_cod2 Rseq is convergent holds
lim_in_cod2 Rseq1 is convergent &
cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq
proof
let Rseq1 be subsequence of Rseq;
assume that
a1: Rseq is convergent_in_cod2 & lim_in_cod2 Rseq is convergent;
consider I1,I2 be increasing sequence of NAT such that
a7: for n,m holds Rseq1.(n,m) = Rseq.(I1.n,I2.m) by def9;
a8:Rseq1 is convergent_in_cod2 by a1;
a10:for e st 0<e ex N st for m st m >= N holds
|.(lim_in_cod2 Rseq1).m - cod2_major_iterated_lim Rseq.| < e
proof
let e;
assume 0<e; then
consider N such that
a11: for m st m >= N holds
|.(lim_in_cod2 Rseq).m - cod2_major_iterated_lim Rseq.| < e
by a1,def35;
take N;
hereby let m;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
assume a12: m >= N;
reconsider m1 = I1.m as Element of NAT;
x2: ProjMap1(Rseq1,mm) is convergent by a8;
for p be Real st 0<p
ex K be Nat st
for n be Nat st n>=K holds
|.ProjMap1(Rseq1,mm).n - lim ProjMap1(Rseq,m1).| < p
proof
let p be Real;
assume b1: 0<p;
ProjMap1(Rseq,m1) is convergent by a1; then
consider K be Nat such that
b2: for n st n>=K holds
|. ProjMap1(Rseq,m1).n - lim ProjMap1(Rseq,m1).| < p
by b1,SEQ_2:def 7;
take K;
hereby let n;
assume b3: n >= K;
x3: n is Element of NAT &
I1.m is Element of NAT & I2.n is Element of NAT by ORDINAL1:def 12;
I2.n >= n by lem01; then
I2.n >= K by b3,XXREAL_0:2; then
|. ProjMap1(Rseq,m1).(I2.n)-lim ProjMap1(Rseq,m1).| < p by b2; then
|. Rseq.(I1.m,I2.n)-lim ProjMap1(Rseq,m1).| <p
by MESFUNC9:def 6; then
|. Rseq1.(m,n) - lim ProjMap1(Rseq,m1).| < p by a7;
hence |.ProjMap1(Rseq1,mm).n - lim ProjMap1(Rseq,m1).| <p
by x3,MESFUNC9:def 6;
end;
end; then
c1: lim ProjMap1(Rseq1,mm) = lim ProjMap1(Rseq,m1) by x2,SEQ_2:def 7;
I1.m >= m by lem01; then
I1.m >= N by a12,XXREAL_0:2; then
a13: |.(lim_in_cod2 Rseq).(I1.m) - cod2_major_iterated_lim Rseq.| < e by a11;
(lim_in_cod2 Rseq).(I1.m) = lim ProjMap1(Rseq,m1) by def33;
hence |.(lim_in_cod2 Rseq1).m - cod2_major_iterated_lim Rseq.| < e
by def33,a13,c1;
end;
end;
hence lim_in_cod2 Rseq1 is convergent by SEQ_2:def 6;
hence thesis by a10,def35;
end;