:: Double Series and Sums
:: by Noboru Endou
::
:: Received March 31, 2014
:: Copyright (c) 2014-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,
ORDINAL1, XREAL_0, COMPLEX1, XXREAL_2, FINSET_1, MEMBERED, MESFUNC9,
SEQ_1, VALUED_1, DBLSEQ_1, QC_LANG1, FUNCT_2, SERIES_1, DBLSEQ_2,
FINSEQ_1, FUNCOP_1, SUPINF_2, CLASSES1, CARD_3, ORDINAL4, REAL_1,
PARTFUN1, MATRIX_1, MCART_1, MATRIXC1, INCSP_1, TREES_1, PARTFUN3,
NUMBER09;
notations VALUED_1, TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1, XXREAL_2, NUMBERS, BINOP_1,
XCMPLX_0, FUNCOP_1, MEMBERED, COMPLEX1, XXREAL_0, XREAL_0, SEQ_1, NAT_1,
FUNCT_4, MESFUNC9, FUNCT_2, SEQ_2, FINSET_1, DBLSEQ_1, SERIES_1,
PARTFUN3, RINFSUP1, CLASSES1, FINSEQ_1, GLIB_003, RVSUM_1, MATRIX_0,
MATRPROB;
constructors TOPMETR, NAT_D, MESFUNC9, SEQ_2, COMSEQ_2, SEQ_4, DBLSEQ_1,
SERIES_1, CLASSES1, PARTFUN3, GLIB_003, RVSUM_1, FUNCT_4, MATRPROB;
registrations ORDINAL1, XXREAL_0, XREAL_0, XBOOLE_0, NUMBERS, XCMPLX_0,
FINSET_1, MEMBERED, VALUED_0, XXREAL_2, RELSET_1, SEQ_4, FUNCT_1,
FUNCT_2, VALUED_1, BINOP_2, NAT_1, CARD_1, RELAT_1, DBLSEQ_1, XTUPLE_0;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions PARTFUN3;
equalities BINOP_1;
expansions MEASURE6, DBLSEQ_1, FUNCT_2, TARSKI, PARTFUN3, RINFSUP1;
theorems TARSKI, XREAL_0, NAT_1, FUNCT_1, XXREAL_0, ZFMISC_1, XREAL_1,
FUNCT_2, RELAT_1, MESFUNC9, ORDINAL1, VALUED_1, COMPLEX1, MEMBERED,
XXREAL_2, RINFSUP1, SEQM_3, SEQ_2, SEQ_4, DBLSEQ_1, BINOP_1, XTUPLE_0,
XBOOLE_0, FUNCT_3, SERIES_1, SERIES_3, CARD_1, XBOOLE_1, FUNCOP_1,
CLASSES1, RFINSEQ, FINSEQ_1, FINSEQ_3, RVSUM_1, GLIB_003, PREPOWER,
MCART_1, MATRIX_0, FINSEQ_5, PARTFUN1, MATRPROB, ABSVALUE, FUNCT_4,
SUBSET_1;
schemes FUNCT_2, STACKS_1, RECDEF_1, NAT_1, BINOP_1, FINSEQ_1, FUNCT_1,
MATRIX_0;
begin :: Double series and its convergence
reserve Rseq, Rseq1, Rseq2 for Function of [:NAT,NAT:],REAL;
definition let f be Function of [:NAT,NAT:],REAL;
redefine attr f is nonnegative-yielding means :: redefines nonnegative-yielding (PARTFUN3, definition)
for i, j being Nat holds f.(i,j) >= 0;
compatibility
proof
thus f is nonnegative-yielding implies
for i,j being Nat holds f.(i,j) >= 0
proof
assume
A0: f is nonnegative-yielding;
let i,j be Nat;
i in NAT & j in NAT by ORDINAL1:def 12; then
[i,j] in [:NAT,NAT:] by ZFMISC_1:def 2;
hence thesis by A0,FUNCT_2:4;
end;
assume
A1: for i,j being Nat holds f.(i,j) >= 0;
let r be Real;
assume r in rng f;
then consider x being Element of [:NAT,NAT:] such that
A2: r = f.x by FUNCT_2:113;
consider x1,x2 being object such that
A3: x1 in NAT & x2 in NAT & x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1,x2 as Nat by A3;
r = f.(x1,x2) by A3,A2;
hence thesis by A1;
end;
end;
theorem
Rseq is non-decreasing implies
(for m being Element of NAT holds ProjMap1(Rseq,m) is non-decreasing) &
(for n being Element of NAT holds ProjMap2(Rseq,n) is non-decreasing)
proof
assume a1: Rseq is non-decreasing;
hereby let m be Element of NAT;
now let n1,n2 be Nat;
a0: n1 in NAT & n2 in NAT by ORDINAL1:def 12;
assume n1<=n2; then
Rseq.(m,n1) <= Rseq.(m,n2) by a1; then
ProjMap1(Rseq,m).n1 <= Rseq.(m,n2) by a0,MESFUNC9:def 6;
hence ProjMap1(Rseq,m).n1 <= ProjMap1(Rseq,m).n2 by a0,MESFUNC9:def 6;
end;
hence ProjMap1(Rseq,m) is non-decreasing by SEQM_3:6;
end;
hereby let m be Element of NAT;
now let n1,n2 be Nat;
a2: n1 in NAT & n2 in NAT by ORDINAL1:def 12;
assume n1<=n2; then
Rseq.(n1,m) <= Rseq.(n2,m) by a1; then
ProjMap2(Rseq,m).n1 <= Rseq.(n2,m) by a2,MESFUNC9:def 7;
hence ProjMap2(Rseq,m).n1 <= ProjMap2(Rseq,m).n2 by a2,MESFUNC9:def 7;
end;
hence ProjMap2(Rseq,m) is non-decreasing by SEQM_3:6;
end;
end;
theorem
Rseq is non-decreasing & Rseq is convergent_in_cod1 implies
lim_in_cod1 Rseq is non-decreasing
proof
assume that
a1: Rseq is non-decreasing and
a2: Rseq is convergent_in_cod1;
now let i,j be Nat;
assume a4: i <= j;
reconsider n1=i, n2=j as Element of NAT by ORDINAL1:def 12;
a5: ProjMap2(Rseq,n1) is convergent & ProjMap2(Rseq,n2) is convergent by a2;
now let m be Nat;
m in NAT by ORDINAL1:def 12; then
ProjMap2(Rseq,n1).m = Rseq.(m,n1) &
ProjMap2(Rseq,n2).m = Rseq.(m,n2) by MESFUNC9:def 7;
hence ProjMap2(Rseq,n1).m <= ProjMap2(Rseq,n2).m by a1,a4;
end; then
lim ProjMap2(Rseq,n1) <= lim ProjMap2(Rseq,n2) by a5,SEQ_2:18; then
(lim_in_cod1 Rseq).n1 <= lim ProjMap2(Rseq,n2) by DBLSEQ_1:def 5;
hence (lim_in_cod1 Rseq).i <= (lim_in_cod1 Rseq).j by DBLSEQ_1:def 5;
end;
hence lim_in_cod1 Rseq is non-decreasing by SEQM_3:6;
end;
theorem
Rseq is non-decreasing & Rseq is convergent_in_cod2 implies
lim_in_cod2 Rseq is non-decreasing
proof
assume that
a1: Rseq is non-decreasing and
a2: Rseq is convergent_in_cod2;
now let i,j be Nat;
assume a4: i<=j;
reconsider m1=i, m2=j as Element of NAT by ORDINAL1:def 12;
p1: ProjMap1(Rseq,m1) is convergent & ProjMap1(Rseq,m2) is convergent by a2;
now let n be Nat;
n in NAT by ORDINAL1:def 12; then
ProjMap1(Rseq,m1).n = Rseq.(m1,n) &
ProjMap1(Rseq,m2).n = Rseq.(m2,n) by MESFUNC9:def 6;
hence ProjMap1(Rseq,m1).n <= ProjMap1(Rseq,m2).n by a1,a4;
end; then
lim ProjMap1(Rseq,m1) <= lim ProjMap1(Rseq,m2) by p1,SEQ_2:18; then
(lim_in_cod2 Rseq).m1 <= lim ProjMap1(Rseq,m2) by DBLSEQ_1:def 6;
hence (lim_in_cod2 Rseq).i <= (lim_in_cod2 Rseq).j by DBLSEQ_1:def 6;
end;
hence lim_in_cod2 Rseq is non-decreasing by SEQM_3:6;
end;
theorem
Rseq is non-decreasing & Rseq is P-convergent implies
(for n,m being Nat holds Rseq.(n,m) <= P-lim Rseq)
proof
assume a1: Rseq is non-decreasing & Rseq is P-convergent;
hereby let n,m be Nat;
reconsider n1=n, m1=m as Element of NAT by ORDINAL1:def 12;
Rseq.(n,m) is Element of REAL by XREAL_0:def 1; then
reconsider Rseq1 = [:NAT,NAT:] --> Rseq.(n,m)
as Function of [:NAT,NAT:],REAL by FUNCOP_1:46;
deffunc F2(Element of NAT,Element of NAT) = Rseq.(n+$1,m+$2);
consider Rseq2 be Function of [:NAT,NAT:],REAL such that
a4: for i be Element of NAT for j be Element of NAT holds
Rseq2.(i,j) = F2(i,j) from BINOP_1:sch 4;
a5: now let i,j be Nat;
a6: n+i>=n & m+j>=m by NAT_1:11;
i in NAT & j in NAT by ORDINAL1:def 12; then
Rseq1.(i,j) = Rseq.(n,m) & Rseq2.(i,j) = Rseq.(n+i,m+j)
by a4,FUNCOP_1:70;
hence Rseq1.(i,j) <= Rseq2.(i,j) by a1,a6;
end;
reconsider r = Rseq.(n,m) as Element of REAL by XREAL_0:def 1;
Rseq1 = [:NAT,NAT:] --> r; then
a7: Rseq1 is P-convergent & P-lim Rseq1 = Rseq.(n,m) by DBLSEQ_1:2;
deffunc N(Element of NAT) = n+$1;
consider N be Function of NAT,NAT such that
b1: for i be Element of NAT holds N.i = N(i) from FUNCT_2:sch 4;
now let k be Nat;
k is Element of NAT by ORDINAL1:def 12; then
b2: N.k = n+k & N.(k+1) = n+(k+1) by b1;
k < k+1 by NAT_1:13;
hence N.k < N.(k+1) by b2,XREAL_1:6;
end; then
reconsider N as increasing sequence of NAT by VALUED_1:def 13;
deffunc M(Element of NAT) = m+$1;
consider M be Function of NAT,NAT such that
c1: for j be Element of NAT holds M.j = M(j) from FUNCT_2:sch 4;
now let k be Nat;
k is Element of NAT by ORDINAL1:def 12; then
c2: M.k = m+k & M.(k+1) = m+(k+1) by c1;
k < k+1 by NAT_1:13;
hence M.k < M.(k+1) by c2,XREAL_1:6;
end; then
reconsider M as increasing sequence of NAT by VALUED_1:def 13;
for i,j be Nat holds Rseq2.(i,j) = Rseq.(N.i,M.j)
proof
let i,j be Nat;
c5: i in NAT & j in NAT by ORDINAL1:def 12; then
N.i = n+i & M.j = m+j by b1,c1;
hence Rseq2.(i,j) = Rseq.(N.i,M.j) by c5,a4;
end; then
Rseq2 is subsequence of Rseq by DBLSEQ_1:def 14; then
Rseq2 is P-convergent & P-lim Rseq2 = P-lim Rseq by a1,DBLSEQ_1:17;
hence Rseq.(n,m) <= P-lim Rseq by a5,a7,DBLSEQ_1:15;
end;
end;
theorem lmADD:
dom (Rseq1+Rseq2) = [:NAT,NAT:] & dom (Rseq1-Rseq2) = [:NAT,NAT:] &
(for n,m being Nat holds
(Rseq1+Rseq2).(n,m) = Rseq1.(n,m) + Rseq2.(n,m)) &
(for n,m being Nat holds
(Rseq1-Rseq2).(n,m) = Rseq1.(n,m) - Rseq2.(n,m))
proof
thus A1: dom(Rseq1+Rseq2) = [:NAT,NAT:]
& dom(Rseq1-Rseq2) = [:NAT,NAT:] by FUNCT_2:def 1;
hereby let n,m be Nat;
n in NAT & m in NAT by ORDINAL1:def 12;
hence (Rseq1+Rseq2).(n,m) = Rseq1.(n,m) + Rseq2.(n,m)
by A1,VALUED_1:def 1,ZFMISC_1:87;
end;
hereby let n,m be Nat;
n in NAT & m in NAT by ORDINAL1:def 12;
hence (Rseq1-Rseq2).(n,m) = Rseq1.(n,m) - Rseq2.(n,m)
by A1,VALUED_1:13,ZFMISC_1:87;
end;
end;
theorem
for C,D,E being non empty set, f being Function of [:C,D:],E holds
ex g being Function of [:D,C:],E st
for d being Element of D, c being Element of C holds g.(d,c) = f.(c,d)
proof
let C,D,E be non empty set;
let f be Function of [:C,D:],E;
deffunc F(Element of D,Element of C) = f.($2,$1);
consider IT be Function of [:D,C:],E such that
A1: for d being Element of D, c being Element of C holds IT.(d,c) = F(d,c)
from STACKS_1:sch 2;
take IT;
thus thesis by A1;
end;
theorem
for C,D,E being set, f being Function of [:C,D:],E holds f = ~~f
by FUNCT_4:53;
scheme
RecEx2D1{C() -> non empty set, D() -> non empty set,
H() -> Function of C(),D(), F(set,set,Nat) -> Element of D()}:
ex g being Function of [:C(),NAT:],D() st
for a being Element of C() holds
g.(a,0) = H().a & for n being Nat holds g.(a,n+1) = F(g.(a,n), a, n)
proof
a1:for a be Element of C() holds
ex f be Function of NAT,D() st
f.0 = H().a & for n being Nat holds f.(n+1) = F(f.n,a,n)
proof
let a be Element of C();
defpred P1[Nat,Element of D(),Element of D()] means $3 = F($2,a,$1);
a2: for n being Nat, x be Element of D() ex y be Element of D() st P1[n,x,y];
thus ex f be Function of NAT,D() st
f.0 = H().a & for n being Nat holds P1[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(a2);
end;
ex g be Function of C(),Funcs(NAT,D()) st
for a be Element of C() holds
ex f be Function of NAT,D() st
g.a = f & f.0 = H().a & for n being Nat holds f.(n+1) = F(f.n,a,n)
proof
set h1 = {[a,l] where a is Element of C(), l is Element of Funcs(NAT,D()) :
ex f be Function of NAT,D() st
f = l & f.0 = H().a & for n being Nat holds f.(n+1) = F(f.n,a,n) };
a3: now let x,y1,y2 be object;
assume a4: [x,y1] in h1 & [x,y2] in h1; then
consider a1 be Element of C(), l1 be Element of Funcs(NAT,D()) such that
a5: [x,y1] = [a1,l1] &
ex f be Function of NAT,D() st
f = l1 & f.0 = H().a1 & for n being Nat holds f.(n+1) = F(f.n,a1,n);
consider a2 be Element of C(), l2 be Element of Funcs(NAT,D()) such that
a6: [x,y2] = [a2,l2] &
ex f be Function of NAT,D() st
f = l2 & f.0 = H().a2 & for n being Nat holds f.(n+1) = F(f.n,a2,n)
by a4;
consider f1 be Function of NAT,D() such that
a7: f1 = l1 & f1.0 = H().a1 &
for n being Nat holds f1.(n+1) = F(f1.n,a1,n) by a5;
consider f2 be Function of NAT,D() such that
a8: f2 = l2 & f2.0 = H().a2 &
for n being Nat holds f2.(n+1) = F(f2.n,a2,n) by a6;
a9: a1 = x & y1 = l1 & a2 = x & y2 = l2 by a5,a6,XTUPLE_0:1;
now let x be Element of NAT;
defpred P2[Nat] means f1.$1 = f2.$1;
a11: P2[0] by a7,a8,a9;
a12: now let n be Nat;
assume P2[n]; then
F(f1.n,a2,n) = f2.(n+1) by a8;
hence P2[n+1] by a7,a9;
end;
for n be Nat holds P2[n] from NAT_1:sch 2(a11,a12);
hence f1.x = f2.x;
end;
hence y1 = y2 by a7,a8,a9,FUNCT_2:63;
end;
now let x be object;
assume x in h1; then
ex a be Element of C(), l be Element of Funcs(NAT,D()) st
x = [a,l] &
ex f be Function of NAT,D() st
f = l & f.0 = H().a & for n being Nat holds f.(n+1) = F(f.n,a,n);
hence x in [:C(),Funcs(NAT,D()):] by ZFMISC_1:def 2;
end; then
reconsider h1 as Relation of C(),Funcs(NAT,D()) by TARSKI:def 3;
for x be object holds x in C() implies x in dom h1
proof
let x be object;
assume x in C(); then
reconsider x1=x as Element of C();
consider f be Function of NAT,D() such that
a15: f.0 = H().x & for n being Nat holds f.(n+1) = F(f.n,x1,n) by a1;
reconsider f as Element of Funcs(NAT,D()) by FUNCT_2:8;
[x,f] in h1 by a15;
hence thesis by XTUPLE_0:def 12;
end; then
C() c= dom h1; then
dom h1 = C() by XBOOLE_0:def 10; then
reconsider h1 as Function of C(),Funcs(NAT,D())
by a3,FUNCT_1:def 1,FUNCT_2:def 1;
take h1;
thus for a be Element of C() holds
ex f be Function of NAT,D() st
h1.a = f & f.0 = H().a & for n being Nat holds f.(n+1) = F(f.n,a,n)
proof
let a be Element of C();
dom h1 = C() by FUNCT_2:def 1; then
[a,h1.a] in h1 by FUNCT_1:1; then
consider x be Element of C(), l be Element of Funcs(NAT,D()) such that
a16: [a,h1.a] = [x,l]
& ex h be Function of NAT,D() st
h = l & h.0 = H().x & for n being Nat holds h.(n+1) = F(h.n,x,n);
a = x & h1.a = l by a16,XTUPLE_0:1;
hence thesis by a16;
end;
end; then
consider g be Function of C(),Funcs(NAT,D()) such that
a17:for a be Element of C() holds
ex f be Function of NAT,D() st
g.a = f & f.0 = H().a &
for n being Nat holds f.(n+1) = F(f.n,a,n);
set h1 = { [[a,n],z] where n is Element of NAT,
a is Element of C(), z is Element of D() :
ex f be Function of NAT,D() st f = g.a & z = f.n };
a18: now let x,y1,y2 be object;
assume a19: [x,y1] in h1 & [x,y2] in h1; then
consider n1 be Element of NAT, a1 be Element of C(),
z1 be Element of D() such that
a20: [x,y1] = [[a1,n1],z1]
& ex f1 be Function of NAT,D() st f1 = g.a1 & z1 = f1.n1;
consider n2 be Element of NAT, a2 be Element of C(),
z2 be Element of D() such that
a21: [x,y2] = [[a2,n2],z2]
& ex f2 be Function of NAT,D() st f2 = g.a2 & z2 = f2.n2 by a19;
x = [a1,n1] & x = [a2,n2] by a20,a21,XTUPLE_0:1; then
a1 = a2 & n1 = n2 by XTUPLE_0:1;
hence y1 = y2 by a20,a21,XTUPLE_0:1;
end;
now let x be object;
assume x in h1; then
consider n1 be Element of NAT, a1 be Element of C(),
z1 be Element of D() such that
a22: x = [[a1,n1],z1] and
ex f1 be Function of NAT,D() st f1 = g.a1 & z1 = f1.n1;
[a1,n1] in [:C(),NAT:] by ZFMISC_1:def 2;
hence x in [:[:C(),NAT:],D():] by a22,ZFMISC_1:def 2;
end; then
reconsider h1 as Relation of [:C(),NAT:],D() by TARSKI:def 3;
for x be object holds x in [:C(),NAT:] implies x in dom h1
proof
let x be object;
assume x in [:C(),NAT:]; then
consider d,n be object such that
a24: d in C() & n in NAT & x = [d,n] by ZFMISC_1:def 2;
reconsider d as Element of C() by a24;
reconsider n as Element of NAT by a24;
consider h be Function of NAT,D() such that
a25: g.d = h and
h.0 = H().d & for n being Nat holds h.(n+1) = F(h.n,d,n) by a17;
h.n is Element of D(); then
consider z be Element of D() such that
a26: ex f be Function of NAT,D() st f = g.d & z = f.n by a25;
[x,z] in h1 by a24,a26;
hence thesis by XTUPLE_0:def 12;
end; then
d2: [:C(),NAT:] c= dom h1; then
dom h1 = [:C(),NAT:] by XBOOLE_0:def 10; then
reconsider h1 as Function of [:C(),NAT:],D()
by a18,FUNCT_1:def 1,FUNCT_2:def 1;
take h1;
thus for a be Element of C() holds
h1.(a,0) = H().a &
for n being Nat holds h1.(a,n+1) = F(h1.(a,n),a,n)
proof
let a be Element of C();
consider h be Function of NAT,D() such that
a27: g.a = h & h.0 = H().a &
for n be Nat holds h.(n+1) = F(h.n,a,n) by a17;
a28:now
let k be Nat;
[a,k+1] in [:C(),NAT:] by ZFMISC_1:def 2; then
[a,k+1] in dom h1 by FUNCT_2:def 1; then
consider u be object such that
a29: [[a,k+1],u] in h1 by XTUPLE_0:def 12;
k in NAT by ORDINAL1:def 12; then
[a,k] in [:C(),NAT:] by ZFMISC_1:def 2; then
[a,k] in dom h1 by FUNCT_2:def 1; then
consider v be object such that
a30: [[a,k],v] in h1 by XTUPLE_0:def 12;
consider n1 be Element of NAT, d1 be Element of C(),
z1 be Element of D() such that
a31: [[a,k],v] = [[d1,n1],z1] &
ex f2 be Function of NAT,D() st f2= g.d1 & z1 = f2.n1 by a30;
consider f2 be Function of NAT,D() such that
a32: f2 = g.d1 & z1 = f2.n1 by a31;
consider n be Element of NAT, d be Element of C(),
z be Element of D() such that
a33: [[a,k+1],u] = [[d,n],z] &
ex f1 be Function of NAT,D() st f1 = g.d & z = f1.n by a29;
[a,k] = [d1,n1] & [a,k+1] = [d,n] by a31,a33,XTUPLE_0:1; then
a34: a = d1 & k = n1 & a = d & k+1 = n by XTUPLE_0:1;
hence h1.(a,k+1) = h.n by a27,a29,a33,FUNCT_1:1
.= F(f2.n1,a,n1) by a27,a32,a34
.= F(h1.(a,k),a,k) by a30,a32,a31,a34,FUNCT_1:1;
end;
[a,0] in [:C(),NAT:] by ZFMISC_1:def 2; then
consider u be object such that
a36: [[a,0],u] in h1 by d2,XTUPLE_0:def 12;
consider n be Element of NAT, d be Element of C(),
z be Element of D() such that
a37: [[a,0],u] = [[d,n],z] &
ex f1 be Function of NAT,D() st f1 = g.d & z = f1.n by a36;
[a,0] = [d,n] & u = z by a37,XTUPLE_0:1; then
a = d & 0 = n by XTUPLE_0:1;
hence thesis by a27,a28,a36,a37,FUNCT_1:1;
end;
end;
scheme
RecEx2D1R{C() -> non empty set,
H() -> Function of C(),REAL, F(set,set,Nat) -> real number}:
ex g being Function of [:C(),NAT:],REAL st
for a being Element of C() holds
g.(a,0) = H().a & for n being natural number holds
g.(a,n+1) = F(g.(a,n), a, n)
proof
defpred P[set,set] means
ex f being Function of NAT,REAL st
$2 = f & f.0 = H().$1 &
for n being Nat holds f.(n+1) = F(f.n,$1,n);
c1:for a be Element of C() ex f be Element of Funcs(NAT,REAL) st P[a,f]
proof
let a be Element of C();
defpred P1[Nat, set, set] means $3 = F($2,a,$1);
c2: for n be Nat for x be Element of REAL
ex y be Element of REAL st P1[n,x,y]
proof
let n be Nat;
let x be Element of REAL;
reconsider y = F(x,a,n) as Element of REAL by XREAL_0:def 1;
take y;
thus thesis;
end;
reconsider A = H().a as Element of REAL;
consider f be Function of NAT,REAL such that
c3: f.0 = A & for n be Nat holds P1[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(c2);
reconsider f as Element of Funcs(NAT,REAL) by FUNCT_2:8;
take f;
thus thesis by c3;
end;
consider g be Function of C(),Funcs(NAT,REAL) such that
a17:for a be Element of C() holds P[a,g.a] from FUNCT_2:sch 3(c1);
set h1 = { [[a,n],z] where n is Element of NAT,
a is Element of C(), z is Element of REAL :
ex f be Function of NAT,REAL st f = g.a & z = f.n };
a18:
now let x,y1,y2 be object;
assume a19: [x,y1] in h1 & [x,y2] in h1; then
consider n1 be Element of NAT, a1 be Element of C(),
z1 be Element of REAL such that
a20: [x,y1] = [[a1,n1],z1] &
ex f1 be Function of NAT,REAL st f1 = g.a1 & z1 = f1.n1;
consider n2 be Element of NAT, a2 be Element of C(),
z2 be Element of REAL such that
a21: [x,y2] = [[a2,n2],z2] &
ex f2 be Function of NAT,REAL st f2 = g.a2 & z2 = f2.n2 by a19;
x = [a1,n1] & x = [a2,n2] by a20,a21,XTUPLE_0:1; then
a1 = a2 & n1 = n2 by XTUPLE_0:1;
hence y1 = y2 by a20,a21,XTUPLE_0:1;
end;
now let x be object;
assume x in h1; then
consider n1 be Element of NAT, a1 be Element of C(),
z1 be Element of REAL such that
a22: x = [[a1,n1],z1] and
ex f1 be Function of NAT,REAL st f1 = g.a1 & z1 = f1.n1;
[a1,n1] in [:C(),NAT:] by ZFMISC_1:def 2;
hence x in [:[:C(),NAT:],REAL:] by a22,ZFMISC_1:def 2;
end; then
reconsider h1 as Relation of [:C(),NAT:],REAL by TARSKI:def 3;
for x be object holds x in [:C(),NAT:] implies x in dom h1
proof
let x be object;
assume x in [:C(),NAT:]; then
consider d,n be object such that
a24: d in C() & n in NAT & x = [d,n] by ZFMISC_1:def 2;
reconsider d as Element of C() by a24;
reconsider n as Element of NAT by a24;
consider h be Function of NAT,REAL such that
a25: g.d = h and
h.0 = H().d and
for n be Nat holds h.(n+1) = F(h.n,d,n) by a17;
h.n is Element of REAL; then
consider z be Element of REAL such that
a26: ex f be Function of NAT,REAL st f = g.d & z = f.n by a25;
[x,z] in h1 by a24,a26;
hence thesis by XTUPLE_0:def 12;
end; then
d2: [:C(),NAT:] c= dom h1; then
dom h1 = [:C(),NAT:] by XBOOLE_0:def 10; then
reconsider h1 as Function of [:C(),NAT:],REAL
by a18,FUNCT_1:def 1,FUNCT_2:def 1;
take h1;
thus for a be Element of C() holds
h1.(a,0) = H().a &
for n being Nat holds h1.(a,n+1) = F(h1.(a,n),a,n)
proof
let a be Element of C();
consider h be Function of NAT,REAL such that
a27: g.a = h & h.0 = H().a &
for n be Nat holds h.(n+1) = F(h.n,a,n) by a17;
a28:now
let k be Nat;
[a,k+1] in [:C(),NAT:] by ZFMISC_1:def 2; then
[a,k+1] in dom h1 by FUNCT_2:def 1; then
consider u be object such that
a29: [[a,k+1],u] in h1 by XTUPLE_0:def 12;
k in NAT by ORDINAL1:def 12; then
[a,k] in [:C(),NAT:] by ZFMISC_1:def 2; then
[a,k] in dom h1 by FUNCT_2:def 1; then
consider v be object such that
a30: [[a,k],v] in h1 by XTUPLE_0:def 12;
consider n1 be Element of NAT, d1 be Element of C(),
z1 be Element of REAL such that
a31: [[a,k],v] = [[d1,n1],z1] &
ex f2 be Function of NAT,REAL st f2= g.d1 & z1 = f2.n1 by a30;
consider f2 be Function of NAT,REAL such that
a32: f2 = g.d1 & z1 = f2.n1 by a31;
consider n be Element of NAT, d be Element of C(),
z be Element of REAL such that
a33: [[a,k+1],u] = [[d,n],z] &
ex f1 be Function of NAT,REAL st f1 = g.d & z = f1.n by a29;
[a,k] = [d1,n1] & [a,k+1] = [d,n] by a31,a33,XTUPLE_0:1; then
a34: a = d1 & k = n1 & a = d & k+1 = n by XTUPLE_0:1;
hence h1.(a,k+1) = h.n by a27,a29,a33,FUNCT_1:1
.= F(f2.n1,a,n1) by a27,a32,a34
.= F(h1.(a,k),a,k) by a30,a32,a31,a34,FUNCT_1:1;
end;
[a,0] in [:C(),NAT:] by ZFMISC_1:def 2; then
consider u be object such that
a36: [[a,0],u] in h1 by d2,XTUPLE_0:def 12;
consider n be Element of NAT, d be Element of C(),
z be Element of REAL such that
a37: [[a,0],u] = [[d,n],z] &
ex f1 be Function of NAT,REAL st f1 = g.d & z = f1.n by a36;
[a,0] = [d,n] & u = z by a37,XTUPLE_0:1; then
a = d & 0 = n by XTUPLE_0:1;
hence thesis by a27,a28,a36,a37,FUNCT_1:1;
end;
end;
scheme
RecEx2D2{C() -> non empty set, D() -> non empty set,
H() -> Function of C(),D(), F(set,set,Nat) -> Element of D()}:
ex g being Function of [:NAT,C():],D() st
for a being Element of C() holds
g.(0,a) = H().a & for n being Nat holds
g.(n+1,a) = F(g.(n,a), a, n)
proof
consider h be Function of [:C(),NAT:],D() such that
a1: for a be Element of C() holds
h.(a,0) = H().a
& for n being Nat holds h.(a,n+1) = F(h.(a,n),a,n) from RecEx2D1;
take g = ~h;
hereby let a be Element of C();
thus g.(0,a) = h.(a,0) by FUNCT_4:def 8 .= H().a by a1;
thus for n being Nat holds g.(n+1,a) = F(g.(n,a),a,n)
proof
let n be Nat;
a2: n in NAT by ORDINAL1:def 12;
g.(n+1,a) = h.(a,n+1) by FUNCT_4:def 8; then
g.(n+1,a) = F(h.(a,n),a,n) by a1;
hence g.(n+1,a) = F(g.(n,a),a,n) by a2,FUNCT_4:def 8;
end;
end;
end;
scheme
RecEx2D2R{C() -> non empty set,
H() -> Function of C(),REAL, F(set,set,Nat) -> real number}:
ex g being Function of [:NAT,C():],REAL st
for a being Element of C() holds
g.(0,a) = H().a & for n being Nat holds
g.(n+1,a) = F(g.(n,a), a, n)
proof
consider h be Function of [:C(),NAT:],REAL such that
a1: for a be Element of C() holds
h.(a,0) = H().a
& for n being Nat holds h.(a,n+1) = F(h.(a,n),a,n) from RecEx2D1R;
take g = ~h;
hereby let a be Element of C();
thus g.(0,a) = h.(a,0) by FUNCT_4:def 8 .= H().a by a1;
thus for n being Nat holds g.(n+1,a) = F(g.(n,a),a,n)
proof
let n be Nat;
a2: n in NAT by ORDINAL1:def 12;
g.(n+1,a) = h.(a,n+1) by FUNCT_4:def 8; then
g.(n+1,a) = F(h.(a,n),a,n) by a1;
hence g.(n+1,a) = F(g.(n,a),a,n) by a2,FUNCT_4:def 8;
end;
end;
end;
definition
let Rseq be Function of [:NAT,NAT:],REAL;
func Partial_Sums_in_cod2(Rseq) -> Function of [:NAT,NAT:],REAL means :DefCS:
for n,m being Nat holds
it.(n,0) = Rseq.(n,0) & it.(n,m+1) = it.(n,m) + Rseq.(n,m+1);
existence
proof
deffunc F0(Element of NAT) = Rseq.($1,0);
consider f0 be Function of NAT,REAL such that
a0: for n be Element of NAT holds f0.n = F0(n) from FUNCT_2:sch 4;
deffunc F(real number,Nat,Nat) = $1 + Rseq.($2,$3+1);
consider IT be Function of [:NAT,NAT:],REAL such that
a1: for a being Element of NAT holds
IT.(a,0) = f0.a &
for n being natural number holds IT.(a,n+1) = F(IT.(a,n),a,n)
from RecEx2D1R;
take IT;
hereby let n,m be Nat;
a2: n in NAT & m in NAT by ORDINAL1:def 12; then
IT.(n,0) = f0.n by a1;
hence IT.(n,0) = Rseq.(n,0) & IT.(n,m+1) = IT.(n,m) + Rseq.(n,m+1)
by a0,a1,a2;
end;
end;
uniqueness
proof
let f1,f2 be Function of [:NAT,NAT:],REAL;
assume that
a1: for n,m being natural number holds
f1.(n,0) = Rseq.(n,0) & f1.(n,m+1) = f1.(n,m) + Rseq.(n,m+1) and
a2: for n,m being natural number holds
f2.(n,0) = Rseq.(n,0) & f2.(n,m+1) = f2.(n,m) + Rseq.(n,m+1);
a3:dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] by FUNCT_2:def 1;
for n,m be object st n in NAT & m in NAT holds f1.(n,m) = f2.(n,m)
proof
let n,m be object;
assume n in NAT & m in NAT; then
reconsider n1 = n, m1 = m as Element of NAT;
defpred P[Nat] means f1.(n1,$1) = f2.(n1,$1);
f1.(n1,0) = Rseq.(n1,0) by a1; then
a4: P[0] by a2;
a5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume a6: P[k];
f1.(n1,k+1) = f1.(n1,k) + Rseq.(n1,k+1) by a1;
hence f1.(n1,k+1) = f2.(n1,k+1) by a2,a6;
end;
for k be Nat holds P[k] from NAT_1:sch 2(a4,a5); then
P[m1];
hence f1.(n,m) = f2.(n,m);
end;
hence thesis by a3,FUNCT_3:6;
end;
end;
definition
let Rseq be Function of [:NAT,NAT:],REAL;
func Partial_Sums_in_cod1(Rseq) -> Function of [:NAT,NAT:],REAL means :DefRS:
for n,m being Nat holds
it.(0,m) = Rseq.(0,m) & it.(n+1,m) = it.(n,m) + Rseq.(n+1,m);
existence
proof
deffunc F0(Element of NAT) = Rseq.(0,$1);
consider f0 be Function of NAT,REAL such that
a0: for n be Element of NAT holds f0.n = F0(n) from FUNCT_2:sch 4;
deffunc F(Real, Nat, Nat) = $1 + Rseq.($3+1,$2);
consider IT be Function of [:NAT,NAT:],REAL such that
a1: for a be Element of NAT holds
IT.(0,a) = f0.a &
for n being natural number holds IT.(n+1,a) = F(IT.(n,a),a,n)
from RecEx2D2R;
take IT;
hereby let n,m be natural number;
a2: n in NAT & m in NAT by ORDINAL1:def 12; then
IT.(0,m) = f0.m by a1;
hence IT.(0,m) = Rseq.(0,m) & IT.(n+1,m) = IT.(n,m) + Rseq.(n+1,m)
by a0,a1,a2;
end;
end;
uniqueness
proof
let f1,f2 be Function of [:NAT,NAT:],REAL;
assume that
a1: for n,m being natural number holds
f1.(0,m) = Rseq.(0,m) & f1.(n+1,m) = f1.(n,m) + Rseq.(n+1,m) and
a2: for n,m being natural number holds
f2.(0,m) = Rseq.(0,m) & f2.(n+1,m) = f2.(n,m) + Rseq.(n+1,m);
a3:dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] by FUNCT_2:def 1;
for n,m be object st n in NAT & m in NAT holds f1.(n,m) = f2.(n,m)
proof
let n,m be object;
assume n in NAT & m in NAT; then
reconsider n1 = n, m1 = m as Element of NAT;
defpred P[Nat] means f1.($1,m1) = f2.($1,m1);
f1.(0,m1) = Rseq.(0,m1) by a1; then
a4: P[0] by a2;
a5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume a6: P[k];
f1.(k+1,m1) = f1.(k,m1) + Rseq.(k+1,m1) by a1;
hence f1.(k+1,m1) = f2.(k+1,m1) by a2,a6;
end;
for k be Nat holds P[k] from NAT_1:sch 2(a4,a5); then
P[n1];
hence f1.(n,m) = f2.(n,m);
end;
hence thesis by a3,FUNCT_3:6;
end;
end;
theorem thADD:
Partial_Sums_in_cod2(Rseq1+Rseq2)
= Partial_Sums_in_cod2(Rseq1) + Partial_Sums_in_cod2(Rseq2) &
Partial_Sums_in_cod1(Rseq1+Rseq2)
= Partial_Sums_in_cod1(Rseq1) + Partial_Sums_in_cod1(Rseq2)
proof
set CS1 = Partial_Sums_in_cod2(Rseq1);
set CS2 = Partial_Sums_in_cod2(Rseq2);
set CS12 = Partial_Sums_in_cod2(Rseq1+Rseq2);
set RS1 = Partial_Sums_in_cod1(Rseq1);
set RS2 = Partial_Sums_in_cod1(Rseq2);
set RS12 = Partial_Sums_in_cod1(Rseq1+Rseq2);
now let n be Element of NAT, m be Element of NAT;
defpred C[Nat] means CS12.(n,$1) = CS1.(n,$1) + CS2.(n,$1);
CS12.(n,0) = (Rseq1+Rseq2).(n,0) by DefCS
.= Rseq1.(n,0) + Rseq2.(n,0) by lmADD
.= CS1.(n,0) + Rseq2.(n,0) by DefCS; then
a1: C[0] by DefCS;
a2: for k be Nat st C[k] holds C[k+1]
proof
let k be Nat;
assume a3: C[k];
CS12.(n,k+1) = CS12.(n,k) + (Rseq1+Rseq2).(n,k+1) by DefCS
.= CS1.(n,k) + CS2.(n,k) + ( Rseq1.(n,k+1) + Rseq2.(n,k+1) ) by a3,lmADD
.= CS1.(n,k) + Rseq1.(n,k+1) + CS2.(n,k) + Rseq2.(n,k+1)
.= CS1.(n,k+1) + CS2.(n,k) + Rseq2.(n,k+1) by DefCS
.= CS1.(n,k+1) + ( CS2.(n,k) + Rseq2.(n,k+1) );
hence C[k+1] by DefCS;
end;
for k be Nat holds C[k] from NAT_1:sch 2(a1,a2); then
C[m];
hence CS12.(n,m) = (CS1+CS2).(n,m) by lmADD;
end;
hence CS12 = CS1 + CS2 by BINOP_1:2;
now let n,m be Element of NAT;
defpred R[Nat] means RS12.($1,m) = RS1.($1,m) + RS2.($1,m);
RS12.(0,m) = (Rseq1+Rseq2).(0,m) by DefRS
.= Rseq1.(0,m) + Rseq2.(0,m) by lmADD
.= RS1.(0,m) + Rseq2.(0,m) by DefRS; then
a4: R[0] by DefRS;
a5: for k be Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume a6: R[k];
RS12.(k+1,m) = RS12.(k,m) + (Rseq1+Rseq2).(k+1,m) by DefRS
.= RS1.(k,m) + RS2.(k,m) + (Rseq1.(k+1,m) + Rseq2.(k+1,m)) by a6,lmADD
.= RS1.(k,m) + Rseq1.(k+1,m) + RS2.(k,m) + Rseq2.(k+1,m)
.= RS1.(k+1,m) + RS2.(k,m) + Rseq2.(k+1,m) by DefRS
.= RS1.(k+1,m) + (RS2.(k,m) + Rseq2.(k+1,m));
hence R[k+1] by DefRS;
end;
for k be Nat holds R[k] from NAT_1:sch 2(a4,a5); then
R[n];
hence RS12.(n,m) = (RS1+RS2).(n,m) by lmADD;
end;
hence RS12 = RS1 + RS2 by BINOP_1:2;
end;
theorem Tr2:
for n,m being Nat holds
(Partial_Sums_in_cod2 Rseq).(n,m) = (Partial_Sums_in_cod1 ~Rseq).(m,n)
& (Partial_Sums_in_cod1 Rseq).(n,m) = (Partial_Sums_in_cod2 ~Rseq).(m,n)
proof
hereby let n,m be Nat;
defpred P[Nat] means
(Partial_Sums_in_cod2(Rseq)).(n,$1)=(Partial_Sums_in_cod1(~Rseq)).($1,n);
Z: n in NAT & m in NAT by ORDINAL1:def 12;
(Partial_Sums_in_cod2(Rseq)).(n,0) = Rseq.(n,0) by DefCS; then
(Partial_Sums_in_cod2(Rseq)).(n,0) = ~Rseq.(0,n) by Z,FUNCT_4:def 8; then
a1: P[0] by DefRS;
a2: now let k be Nat;
assume P[k]; then
(Partial_Sums_in_cod2(Rseq)).(n,k+1)
= (Partial_Sums_in_cod1(~Rseq)).(k,n) + Rseq.(n,k+1) by DefCS
.= (Partial_Sums_in_cod1(~Rseq)).(k,n) + ~Rseq.(k+1,n)
by FUNCT_4:def 8,Z;
hence P[k+1] by DefRS;
end;
for k be Nat holds P[k] from NAT_1:sch 2(a1,a2);
hence (Partial_Sums_in_cod2 Rseq).(n,m)=(Partial_Sums_in_cod1 ~Rseq).(m,n);
Z: n in NAT & m in NAT by ORDINAL1:def 12;
defpred Q[Nat] means
(Partial_Sums_in_cod1(Rseq)).($1,m)=(Partial_Sums_in_cod2(~Rseq)).(m,$1);
(Partial_Sums_in_cod1(Rseq)).(0,m) = Rseq.(0,m) by DefRS; then
(Partial_Sums_in_cod1(Rseq)).(0,m) = ~Rseq.(m,0) by Z,FUNCT_4:def 8; then
a4: Q[0] by DefCS;
a5: now let k be Nat;
assume Q[k]; then
(Partial_Sums_in_cod1(Rseq)).(k+1,m)
= (Partial_Sums_in_cod2(~Rseq)).(m,k) + Rseq.(k+1,m) by DefRS
.= (Partial_Sums_in_cod2(~Rseq)).(m,k) + ~Rseq.(m,k+1)
by Z,FUNCT_4:def 8;
hence Q[k+1] by DefCS;
end;
for k be Nat holds Q[k] from NAT_1:sch 2(a4,a5);
hence (Partial_Sums_in_cod1 Rseq).(n,m)=(Partial_Sums_in_cod2 ~Rseq).(m,n);
end;
end;
theorem
Partial_Sums_in_cod2 Rseq = ~(Partial_Sums_in_cod1 ~Rseq)
& Partial_Sums_in_cod2 ~Rseq = ~(Partial_Sums_in_cod1 Rseq)
& ~(Partial_Sums_in_cod2 Rseq) = Partial_Sums_in_cod1 ~Rseq
& ~(Partial_Sums_in_cod2 ~Rseq) = Partial_Sums_in_cod1 Rseq
proof
now let n,m be Element of NAT;
(Partial_Sums_in_cod2 Rseq).(n,m)
= (Partial_Sums_in_cod1 ~Rseq).(m,n) by Tr2;
hence (Partial_Sums_in_cod2 Rseq).(n,m)
= ~(Partial_Sums_in_cod1 ~Rseq).(n,m) by FUNCT_4:def 8;
end;
hence Partial_Sums_in_cod2 Rseq = ~(Partial_Sums_in_cod1 ~Rseq)
by BINOP_1:2;
now let n,m be Element of NAT;
(Partial_Sums_in_cod2 ~Rseq).(n,m)
= (Partial_Sums_in_cod1 Rseq).(m,n) by Tr2;
hence (Partial_Sums_in_cod2(~Rseq)).(n,m)
= (~Partial_Sums_in_cod1(Rseq)).(n,m) by FUNCT_4:def 8;
end;
hence
a1: Partial_Sums_in_cod2(~Rseq) = ~Partial_Sums_in_cod1(Rseq) by BINOP_1:2;
now let n,m be Element of NAT;
(~Partial_Sums_in_cod2(Rseq)).(n,m)
= (Partial_Sums_in_cod2(Rseq)).(m,n) by FUNCT_4:def 8;
hence (~Partial_Sums_in_cod2(Rseq)).(n,m)
= (Partial_Sums_in_cod1(~Rseq)).(n,m) by Tr2;
end;
hence ~Partial_Sums_in_cod2(Rseq)
= Partial_Sums_in_cod1(~Rseq) by BINOP_1:2;
now let n,m be Element of NAT;
(~Partial_Sums_in_cod2(~Rseq)).(n,m)
= (~Partial_Sums_in_cod1(Rseq)).(m,n) by a1,FUNCT_4:def 8;
hence (~Partial_Sums_in_cod2(~Rseq)).(n,m)
= (Partial_Sums_in_cod1(Rseq)).(n,m) by FUNCT_4:def 8;
end;
hence ~Partial_Sums_in_cod2 ~Rseq =Partial_Sums_in_cod1 Rseq by BINOP_1:2;
end;
definition
let Rseq be Function of [:NAT,NAT:],REAL;
func Partial_Sums(Rseq) -> Function of [:NAT,NAT:],REAL equals
Partial_Sums_in_cod2( Partial_Sums_in_cod1 Rseq );
correctness;
end;
theorem ThRS:
for n,m being Nat holds
(Partial_Sums Rseq).(n+1,m)
= (Partial_Sums_in_cod2 Rseq).(n+1,m) + (Partial_Sums Rseq).(n,m) &
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n,m+1)
= (Partial_Sums_in_cod1 Rseq).(n,m+1)
+ (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n,m)
proof
let n,m be Nat;
set RPS = Partial_Sums Rseq;
set CPS = Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq);
set ROW = Partial_Sums_in_cod1 Rseq;
set COL = Partial_Sums_in_cod2 Rseq;
defpred P[Nat] means RPS.(n+1,$1) = COL.(n+1,$1) + RPS.(n,$1);
a1:RPS.(n,0) = ROW.(n,0) by DefCS;
RPS.(n+1,0) = ROW.(n+1,0) by DefCS
.= ROW.(n,0) + Rseq.(n+1,0) by DefRS; then
a3:P[0] by a1,DefCS;
a4:for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
a6: COL.(n+1,k+1) = COL.(n+1,k) + Rseq.(n+1,k+1) by DefCS;
RPS.(n,k+1) = RPS.(n,k) + ROW.(n,k+1) by DefCS; then
COL.(n+1,k+1) + RPS.(n,k+1)
= RPS.(n+1,k) + ( Rseq.(n+1,k+1) + ROW.(n,k+1) ) by A5,a6
.= RPS.(n+1,k) + ROW.(n+1,k+1) by DefRS;
hence P[k+1] by DefCS;
end;
for k be Nat holds P[k] from NAT_1:sch 2(a3,a4);
hence RPS.(n+1,m) = COL.(n+1,m) + RPS.(n,m);
defpred Q[Nat] means CPS.($1,m+1) = ROW.($1,m+1) + CPS.($1,m);
b1:CPS.(0,m) = COL.(0,m) by DefRS;
CPS.(0,m+1) = COL.(0,m+1) by DefRS
.= COL.(0,m) + Rseq.(0,m+1) by DefCS; then
b3:Q[0] by b1,DefRS;
b4:for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume B5: Q[k];
b6: ROW.(k+1,m+1) = ROW.(k,m+1) + Rseq.(k+1,m+1) by DefRS;
CPS.(k+1,m) = CPS.(k,m) + COL.(k+1,m) by DefRS; then
ROW.(k+1,m+1) + CPS.(k+1,m)
= CPS.(k,m+1) + ( Rseq.(k+1,m+1) + COL.(k+1,m) ) by B5,b6
.= CPS.(k,m+1) + COL.(k+1,m+1) by DefCS;
hence Q[k+1] by DefRS;
end;
for k being Nat holds Q[k] from NAT_1:sch 2(b3,b4);
hence thesis;
end;
th103:
for m,n being Nat holds
(Partial_Sums Rseq).(m,n)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(m,n)
proof
defpred P1[Nat] means
for m be Nat holds
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(m,$1)
= (Partial_Sums Rseq).(m,$1);
defpred P2[Nat] means
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).($1,0)
= (Partial_Sums Rseq).($1,0);
Y3:(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(0,0)
= (Partial_Sums_in_cod2 Rseq).(0,0) by DefRS
.= Rseq.(0,0) by DefCS;
(Partial_Sums Rseq).(0,0)
= (Partial_Sums_in_cod1(Rseq)).(0,0) by DefCS
.= Rseq.(0,0) by DefRS; then
Y1:P2[0] by Y3;
Y2:for i be Nat st P2[i] holds P2[i+1]
proof
let i be Nat;
assume Y3: P2[i];
Y4: (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(i+1,0)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2(Rseq))).(i,0)
+ (Partial_Sums_in_cod2(Rseq)).(i+1,0) by DefRS
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(i,0)
+ Rseq.(i+1,0) by DefCS;
(Partial_Sums Rseq).(i+1,0)
= (Partial_Sums_in_cod1 Rseq).(i+1,0) by DefCS
.= (Partial_Sums_in_cod1 Rseq).(i,0) + Rseq.(i+1,0) by DefRS
.= (Partial_Sums Rseq).(i,0) + Rseq.(i+1,0) by DefCS;
hence P2[i+1] by Y3,Y4;
end;
for n be Nat holds P2[n] from NAT_1:sch 2(Y1,Y2); then
X1:P1[0];
X2:for j be Nat st P1[j] holds P1[j+1]
proof
let j be Nat;
assume Z3: P1[j];
for m be Nat holds
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(m,j+1)
= (Partial_Sums Rseq).(m,j+1)
proof
let n be Nat;
defpred P3[Nat] means
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).($1,j+1)
= (Partial_Sums Rseq).($1,j+1);
Z4: (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(0,j+1)
= (Partial_Sums_in_cod2 Rseq).(0,j+1) by DefRS
.= (Partial_Sums_in_cod2 Rseq).(0,j) + Rseq.(0,j+1) by DefCS
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(0,j)
+ Rseq.(0,j+1) by DefRS;
(Partial_Sums Rseq).(0,j+1)
= (Partial_Sums Rseq).(0,j)
+ (Partial_Sums_in_cod1 Rseq).(0,j+1) by DefCS
.= (Partial_Sums Rseq).(0,j) + Rseq.(0,j+1) by DefRS
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(0,j)
+ Rseq.(0,j+1) by Z3; then
Z1: P3[0] by Z4;
Z2: for i be Nat st P3[i] holds P3[i+1]
proof
let i be Nat;
assume P3[i];
Z6: (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(i,j)
= (Partial_Sums Rseq).(i,j) by Z3;
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(i+1,j+1)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(i,j+1)
+ (Partial_Sums_in_cod2 Rseq).(i+1,j+1) by DefRS
.= (Partial_Sums Rseq).(i,j)
+ (Partial_Sums_in_cod1 Rseq).(i,j+1)
+ (Partial_Sums_in_cod2 Rseq).(i+1,j+1) by Z6,ThRS
.= (Partial_Sums Rseq).(i,j)
+ (Partial_Sums_in_cod1 Rseq).(i,j+1)
+ ( (Partial_Sums_in_cod2 Rseq).(i+1,j)
+Rseq.(i+1,j+1) ) by DefCS
.= (Partial_Sums Rseq).(i,j)
+ ( (Partial_Sums_in_cod1(Rseq)).(i,j+1)
+Rseq.(i+1,j+1) )
+ (Partial_Sums_in_cod2(Rseq)).(i+1,j)
.= (Partial_Sums Rseq).(i,j)
+ (Partial_Sums_in_cod1(Rseq)).(i+1,j+1)
+ (Partial_Sums_in_cod2(Rseq)).(i+1,j) by DefRS
.= (Partial_Sums Rseq).(i,j)
+ (Partial_Sums_in_cod2 Rseq).(i+1,j)
+ (Partial_Sums_in_cod1 Rseq).(i+1,j+1)
.= (Partial_Sums Rseq).(i+1,j)
+ (Partial_Sums_in_cod1 Rseq).(i+1,j+1) by ThRS;
hence thesis by DefCS;
end;
for n be Nat holds P3[n] from NAT_1:sch 2(Z1,Z2);
hence thesis;
end;
hence P1[j+1];
end;
for m be Nat holds P1[m] from NAT_1:sch 2(X1,X2);
hence thesis;
end;
theorem th103a:
Partial_Sums Rseq = Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)
proof
now let x be Element of [:NAT,NAT:];
consider n,m be object such that
A1: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2;
reconsider n1=n,m1=m as Nat by A1;
(Partial_Sums Rseq).(n1,m1)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n1,m1) by th103;
hence (Partial_Sums Rseq).x
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).x by A1;
end;
hence thesis;
end;
theorem thRS2:
for n,m being Nat holds
Rseq.(n+1,m+1) = (Partial_Sums Rseq).(n+1,m+1)
- (Partial_Sums Rseq).(n,m+1)
- (Partial_Sums Rseq).(n+1,m)
+ (Partial_Sums Rseq).(n,m)
proof
let n,m be Nat;
set RPS = Partial_Sums_in_cod2(Partial_Sums_in_cod1 Rseq);
A1:RPS.(n+1,m+1)
= (Partial_Sums_in_cod1(Rseq)).(n+1,m+1) + RPS.(n+1,m) by DefCS
.= Rseq.(n+1,m+1) + (Partial_Sums_in_cod1(Rseq)).(n,m+1)
+ RPS.(n+1,m) by DefRS;
RPS.(n,m+1) = (Partial_Sums_in_cod1(Rseq)).(n,m+1) + RPS.(n,m) by DefCS;
hence thesis by A1;
end;
theorem
for n,m being Nat holds
Rseq.(n+1,m+1) = (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n+1,m+1)
- (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n+1,m)
- (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n,m+1)
+ (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n,m)
proof
let n,m be Nat;
set CPS = Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq);
set CS = Partial_Sums_in_cod2 Rseq;
A1:CPS.(n+1,m+1) = CS.(n+1,m+1) + CPS.(n,m+1) by DefRS
.= Rseq.(n+1,m+1) + CS.(n+1,m) + CPS.(n,m+1) by DefCS;
CPS.(n+1,m) = CS.(n+1,m) + CPS.(n,m) by DefRS;
hence thesis by A1;
end;
theorem
Partial_Sums Rseq is P-convergent implies
Rseq is P-convergent & P-lim Rseq = 0
proof
set CPS = Partial_Sums Rseq;
assume A1: CPS is P-convergent;
set Plim = P-lim CPS;
a2: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) - 0 .| < e
proof
let e be Real;
assume A3: 0 < e;
set e1 = e/4;
consider N be Nat such that
a4: for n,m be Nat st n>=N & m>=N holds
|. CPS.(n,m) - Plim .| < e1 by A1,A3,DBLSEQ_1:def 2;
take N1 = N+1;
hereby let n1,m1 be Nat;
assume A5: n1>=N1 & m1>=N1; then
a5: n1 > N & m1 > N by NAT_1:13; then
reconsider n = n1-1, m=m1-1 as Element of NAT by NAT_1:20;
a6: n1 = n+1 & m1=m+1;
n+1 > N & m+1 > N by A5,NAT_1:13; then
a7: n >= N & m >= N by NAT_1:13;
Rseq.(n1,m1)
= CPS.(n1,m1) - CPS.(n,m1) - CPS.(n1,m) + CPS.(n,m) by a6,thRS2
.= ( (CPS.(n1,m1)- Plim) - (CPS.(n1,m)-Plim) )
- ( (CPS.(n,m1)-Plim) - (CPS.(n,m)-Plim) ); then
a8: |. Rseq.(n1,m1)-0 .|
<= |. (CPS.(n1,m1)- Plim) - (CPS.(n1,m)-Plim) .|
+ |. (CPS.(n,m1)-Plim) - (CPS.(n,m)-Plim) .| by COMPLEX1:57;
a9: |. (CPS.(n1,m1)- Plim) - (CPS.(n1,m)-Plim) .|
<= |. CPS.(n1,m1)- Plim .| + |. CPS.(n1,m)-Plim .| by COMPLEX1:57;
a10: |. (CPS.(n,m1)-Plim) - (CPS.(n,m)-Plim) .|
<= |. CPS.(n,m1)-Plim .| + |. CPS.(n,m)-Plim .| by COMPLEX1:57;
|. CPS.(n1,m1) - Plim.| < e1 & |. CPS.(n,m1) - Plim.| < e1 &
|. CPS.(n1,m) - Plim.| < e1 & |. CPS.(n,m)-Plim.| < e1 by a4,a5,a7; then
|. CPS.(n1,m1) - Plim.| + |. CPS.(n1,m) - Plim.| < e1+e1 &
|. CPS.(n,m1) - Plim.| + |. CPS.(n,m)-Plim.| < e1+e1 by XREAL_1:8; then
|. (CPS.(n1,m1) - Plim) - (CPS.(n1,m) - Plim) .| < e1+e1 &
|. (CPS.(n,m1) - Plim) - (CPS.(n,m) - Plim) .| < e1+e1
by a9,a10,XXREAL_0:2; then
|. (CPS.(n1,m1) - Plim) - (CPS.(n1,m) - Plim) .|
+ |. (CPS.(n,m1) - Plim) - (CPS.(n,m)-Plim) .| < (e1+e1)+(e1+e1)
by XREAL_1:8;
hence |. Rseq.(n1,m1) - 0 .| < e by a8,XXREAL_0:2;
end;
end;
hence Rseq is P-convergent;
hence P-lim Rseq = 0 by a2,DBLSEQ_1:def 2;
end;
theorem lm74:
Partial_Sums(Rseq1 + Rseq2) = Partial_Sums(Rseq1) + Partial_Sums(Rseq2)
proof
Partial_Sums(Rseq1+Rseq2)
= Partial_Sums_in_cod2(Partial_Sums_in_cod1(Rseq1)
+Partial_Sums_in_cod1(Rseq2)) by thADD;
hence thesis by thADD;
end;
theorem
Partial_Sums Rseq1 is P-convergent & Partial_Sums Rseq2 is P-convergent
implies Partial_Sums(Rseq1+Rseq2) is P-convergent
proof
assume Partial_Sums(Rseq1) is P-convergent &
Partial_Sums(Rseq2) is P-convergent; then
Partial_Sums(Rseq1) + Partial_Sums(Rseq2) is P-convergent by DBLSEQ_1:11;
hence thesis by lm74;
end;
theorem th100:
for m,n being Element of NAT holds
(Partial_Sums_in_cod1(Rseq)).(m,n) = Partial_Sums(ProjMap2(Rseq,n)).m &
(Partial_Sums_in_cod2(Rseq)).(m,n) = Partial_Sums(ProjMap1(Rseq,m)).n
proof
let m,n be Element of NAT;
defpred P[Nat] means
(Partial_Sums_in_cod1(Rseq)).($1,n) = Partial_Sums(ProjMap2(Rseq,n)).$1;
Partial_Sums(ProjMap2(Rseq,n)).0 = (ProjMap2(Rseq,n)).0 by SERIES_1:def 1
.= Rseq.(0,n) by MESFUNC9:def 7; then
a1:P[0] by DefRS;
a2:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k]; then
(Partial_Sums_in_cod1(Rseq)).(k+1,n)
= Partial_Sums(ProjMap2(Rseq,n)).k + Rseq.(k+1,n) by DefRS
.= Partial_Sums(ProjMap2(Rseq,n)).k + (ProjMap2(Rseq,n)).(k+1)
by MESFUNC9:def 7;
hence P[k+1] by SERIES_1:def 1;
end;
for k be Nat holds P[k] from NAT_1:sch 2(a1,a2);
hence (Partial_Sums_in_cod1(Rseq)).(m,n) = Partial_Sums(ProjMap2(Rseq,n)).m;
defpred Q[Nat] means
(Partial_Sums_in_cod2(Rseq)).(m,$1) = Partial_Sums(ProjMap1(Rseq,m)).$1;
Partial_Sums(ProjMap1(Rseq,m)).0 = (ProjMap1(Rseq,m)).0 by SERIES_1:def 1
.= Rseq.(m,0) by MESFUNC9:def 6; then
a3:Q[0] by DefCS;
a4:for k be Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume Q[k]; then
(Partial_Sums_in_cod2(Rseq)).(m,k+1)
= Partial_Sums(ProjMap1(Rseq,m)).k + Rseq.(m,k+1) by DefCS
.= Partial_Sums(ProjMap1(Rseq,m)).k + (ProjMap1(Rseq,m)).(k+1)
by MESFUNC9:def 6;
hence Q[k+1] by SERIES_1:def 1;
end;
for k be Nat holds Q[k] from NAT_1:sch 2(a3,a4);
hence thesis;
end;
theorem th00:
ProjMap1(Partial_Sums Rseq,0) = ProjMap1(Partial_Sums_in_cod2 Rseq,0)
& ProjMap2(Partial_Sums Rseq,0) = ProjMap2(Partial_Sums_in_cod1 Rseq,0)
proof
A1:now let m be Element of NAT;
ProjMap1(Partial_Sums Rseq,0).m
= (Partial_Sums Rseq).(0,m) by MESFUNC9:def 6
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(0,m) by th103a
.= (Partial_Sums_in_cod2 Rseq).(0,m) by DefRS;
hence ProjMap1(Partial_Sums Rseq,0).m
= ProjMap1(Partial_Sums_in_cod2 Rseq,0).m by MESFUNC9:def 6;
end;
now let n be Element of NAT;
ProjMap2(Partial_Sums Rseq,0).n
= (Partial_Sums Rseq).(n,0) by MESFUNC9:def 7
.= (Partial_Sums_in_cod1 Rseq).(n,0) by DefCS;
hence ProjMap2(Partial_Sums Rseq,0).n
= ProjMap2(Partial_Sums_in_cod1 Rseq,0).n by MESFUNC9:def 7;
end;
hence thesis by A1;
end;
theorem
for C,D being non empty set, F1,F2 being Function of [:C,D:],REAL,
c being Element of C holds
ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c)
proof
let C,D be non empty set;
let F1,F2 be Function of [:C,D:],REAL;
let c be Element of C;
dom ProjMap1(F1+F2,c) = D
& dom ProjMap1(F1,c) = D & dom ProjMap1(F2,c) = D by FUNCT_2:def 1; then
A2:dom ProjMap1(F1+F2,c) = dom ProjMap1(F1,c) /\ dom ProjMap1(F2,c);
for d being object st d in dom ProjMap1(F1+F2,c) holds
ProjMap1(F1+F2,c).d = ProjMap1(F1,c).d + ProjMap1(F2,c).d
proof
let d be object;
assume A3: d in dom ProjMap1(F1+F2,c); then
A4: ProjMap1(F1+F2,c).d = (F1+F2).(c,d) & ProjMap1(F1,c).d = F1.(c,d)
& ProjMap1(F2,c).d = F2.(c,d) by MESFUNC9:def 6;
reconsider d1=d as Element of D by A3;
[c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then
[c,d] in dom(F1+F2) by FUNCT_2:def 1;
hence thesis by A4,VALUED_1:def 1;
end;
hence thesis by A2,VALUED_1:def 1;
end;
theorem
for C,D being non empty set, F1,F2 being Function of [:C,D:],REAL,
d being Element of D holds
ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d)
proof
let C,D be non empty set;
let F1,F2 be Function of [:C,D:],REAL;
let d be Element of D;
dom ProjMap2(F1+F2,d) = C
& dom ProjMap2(F1,d) = C & dom ProjMap2(F2,d) = C by FUNCT_2:def 1; then
A2:dom ProjMap2(F1+F2,d) = dom ProjMap2(F1,d) /\ dom ProjMap2(F2,d);
for c being object st c in dom ProjMap2(F1+F2,d) holds
ProjMap2(F1+F2,d).c = ProjMap2(F1,d).c + ProjMap2(F2,d).c
proof
let c be object;
assume A3: c in dom ProjMap2(F1+F2,d); then
A4: ProjMap2(F1+F2,d).c = (F1+F2).(c,d) & ProjMap2(F1,d).c = F1.(c,d)
& ProjMap2(F2,d).c = F2.(c,d) by MESFUNC9:def 7;
reconsider c1=c as Element of C by A3;
[c,d] in [:C,D:] by A3,ZFMISC_1:def 2; then
[c,d] in dom(F1+F2) by FUNCT_2:def 1;
hence thesis by A4,VALUED_1:def 1;
end;
hence thesis by A2,VALUED_1:def 1;
end;
theorem th01a:
Partial_Sums Rseq is convergent_in_cod1 iff
Partial_Sums_in_cod1 Rseq is convergent_in_cod1
proof
hereby assume A1: Partial_Sums Rseq is convergent_in_cod1;
now let m be Element of NAT;
defpred P[Nat] means
for k be Element of NAT st k = $1 holds
ProjMap2(Partial_Sums_in_cod1 Rseq,k) is convergent;
now let k be Element of NAT;
assume k = 0; then
ProjMap2(Partial_Sums Rseq,k) = ProjMap2(Partial_Sums_in_cod1 Rseq,k)
by th00;
hence ProjMap2(Partial_Sums_in_cod1 Rseq,k) is convergent by A1;
end; then
A3: P[0];
A4: for m1 being Nat st P[m1] holds P[m1+1]
proof
let m1 be Nat;
reconsider m=m1 as Element of NAT by ORDINAL1:def 12;
assume P[m1];
hereby let k be Element of NAT;
assume B2: k = m1+1; then
reconsider k1 = k-1 as Element of NAT by NAT_1:11,21;
B4: ProjMap2(Partial_Sums Rseq,m) is convergent
& ProjMap2(Partial_Sums Rseq,k) is convergent by A1;
now let e be Real;
assume B6: 0<e; then
consider N1 be Nat such that
B7: for n being Nat st n>=N1 holds
|.ProjMap2(Partial_Sums Rseq,m).n
- lim(ProjMap2(Partial_Sums Rseq,m)).| < e/2 by B4,SEQ_2:def 7;
consider N2 be Nat such that
B8: for n being Nat st n>=N2 holds
|.ProjMap2(Partial_Sums Rseq,k).n
- lim(ProjMap2(Partial_Sums Rseq,k)).| < e/2
by B4,B6,SEQ_2:def 7;
reconsider N=max(N1,N2) as Nat by TARSKI:1;
take N;
hereby let n be Nat;
assume B9: n>=N;
N >= N1 & N >= N2 by XXREAL_0:25; then
n >= N1 & n >= N2 by B9,XXREAL_0:2; then
|.ProjMap2(Partial_Sums Rseq,m).n
- lim(ProjMap2(Partial_Sums Rseq,m)).| < e/2
& |.ProjMap2(Partial_Sums Rseq,k).n
- lim(ProjMap2(Partial_Sums Rseq,k)).| < e/2 by B7,B8; then
B12: |.ProjMap2(Partial_Sums Rseq,m).n
- lim(ProjMap2(Partial_Sums Rseq,m)).|
+ |.ProjMap2(Partial_Sums Rseq,k).n
- lim(ProjMap2(Partial_Sums Rseq,k)).| < e/2 + e/2
by XREAL_1:8;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
ProjMap2(Partial_Sums Rseq,k).n
= (Partial_Sums Rseq).(n1,k) by MESFUNC9:def 7
.= (Partial_Sums Rseq).(n1,m)
+ (Partial_Sums_in_cod1 Rseq).(n1,k) by B2,DefCS
.= ProjMap2(Partial_Sums Rseq,m).n
+ (Partial_Sums_in_cod1 Rseq).(n1,k) by MESFUNC9:def 7
.= ProjMap2(Partial_Sums Rseq,m).n
+ ProjMap2(Partial_Sums_in_cod1 Rseq,k).n by MESFUNC9:def 7; then
|.ProjMap2(Partial_Sums_in_cod1 Rseq,k).n
- ( lim(ProjMap2(Partial_Sums Rseq,k))
- lim(ProjMap2(Partial_Sums Rseq,m)) ).|
= |.( ProjMap2(Partial_Sums Rseq,k).n
- lim(ProjMap2(Partial_Sums Rseq,k)) )
-( ProjMap2(Partial_Sums Rseq,m).n
- lim(ProjMap2(Partial_Sums Rseq,m)) ).|; then
|.ProjMap2(Partial_Sums_in_cod1 Rseq,k).n
- ( lim(ProjMap2(Partial_Sums Rseq,k))
- lim(ProjMap2(Partial_Sums Rseq,m)) ).|
<= |.ProjMap2(Partial_Sums Rseq,k).n
- lim(ProjMap2(Partial_Sums Rseq,k)).|
+ |.ProjMap2(Partial_Sums Rseq,m).n
- lim(ProjMap2(Partial_Sums Rseq,m)).| by COMPLEX1:57;
hence |.ProjMap2(Partial_Sums_in_cod1 Rseq,k).n
- ( lim(ProjMap2(Partial_Sums Rseq,k))
- lim(ProjMap2(Partial_Sums Rseq,m)) ).| < e by B12,XXREAL_0:2;
end;
end;
hence ProjMap2(Partial_Sums_in_cod1 Rseq,k) is convergent
by SEQ_2:def 6;
end;
end;
for m1 being Nat holds P[m1] from NAT_1:sch 2(A3,A4);
hence ProjMap2(Partial_Sums_in_cod1 Rseq,m) is convergent;
end;
hence Partial_Sums_in_cod1 Rseq is convergent_in_cod1;
end;
assume C0: Partial_Sums_in_cod1 Rseq is convergent_in_cod1;
now let m be Element of NAT;
defpred P[Nat] means
for k being Element of NAT st k = $1 holds
ProjMap2(Partial_Sums Rseq,k) is convergent;
ProjMap2(Partial_Sums Rseq,0) = ProjMap2(Partial_Sums_in_cod1 Rseq,0)
by th00; then
C1: P[0] by C0;
C2: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume C3: P[m];
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
hereby let k be Element of NAT;
assume C4: k=m+1; then
reconsider k1=k-1 as Element of NAT by NAT_1:11,21;
for n being Element of NAT holds
ProjMap2(Partial_Sums Rseq,k).n
= (ProjMap2(Partial_Sums Rseq,m1)
+ ProjMap2(Partial_Sums_in_cod1 Rseq,m1+1)).n
proof
let n be Element of NAT;
ProjMap2(Partial_Sums Rseq,k).n
= (Partial_Sums Rseq).(n,m1+1) by C4,MESFUNC9:def 7
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n,m1+1) by th103a
.= (Partial_Sums_in_cod1 Rseq).(n,m1+1)
+ (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n,m1) by ThRS
.= (Partial_Sums_in_cod1 Rseq).(n,m1+1)
+ (Partial_Sums Rseq).(n,m1) by th103a
.= ProjMap2(Partial_Sums_in_cod1 Rseq,m1+1).n
+ (Partial_Sums Rseq).(n,m1) by MESFUNC9:def 7
.= ProjMap2(Partial_Sums_in_cod1 Rseq,m1+1).n
+ ProjMap2(Partial_Sums Rseq,m1).n by MESFUNC9:def 7;
hence thesis by VALUED_1:1;
end; then
C5: ProjMap2(Partial_Sums Rseq,k)
= ProjMap2(Partial_Sums Rseq,m1)
+ ProjMap2(Partial_Sums_in_cod1 Rseq,m1+1);
ProjMap2(Partial_Sums Rseq,m1) is convergent
& ProjMap2(Partial_Sums_in_cod1 Rseq,m1+1) is convergent by C3,C0;
hence ProjMap2(Partial_Sums Rseq,k) is convergent by C5,SEQ_2:5;
end;
end;
for m being Nat holds P[m] from NAT_1:sch 2(C1,C2);
hence ProjMap2(Partial_Sums Rseq,m) is convergent;
end;
hence Partial_Sums Rseq is convergent_in_cod1;
end;
theorem th01b:
Partial_Sums Rseq is convergent_in_cod2 iff
Partial_Sums_in_cod2 Rseq is convergent_in_cod2
proof
hereby assume A1: Partial_Sums Rseq is convergent_in_cod2;
now let m be Element of NAT;
defpred P[Nat] means
for k be Element of NAT st k = $1 holds
ProjMap1(Partial_Sums_in_cod2 Rseq,k) is convergent;
now let k be Element of NAT;
assume k = 0; then
ProjMap1(Partial_Sums Rseq,k) = ProjMap1(Partial_Sums_in_cod2 Rseq,k)
by th00;
hence ProjMap1(Partial_Sums_in_cod2 Rseq,k) is convergent by A1;
end; then
A3: P[0];
A4: for m1 being Nat st P[m1] holds P[m1+1]
proof
let m1 be Nat;
reconsider m=m1 as Element of NAT by ORDINAL1:def 12;
assume P[m1];
hereby let k be Element of NAT;
assume B2: k = m1+1; then
reconsider k1 = k-1 as Element of NAT by NAT_1:11,21;
B4: ProjMap1(Partial_Sums Rseq,m) is convergent
& ProjMap1(Partial_Sums Rseq,k) is convergent by A1;
now let e be Real;
assume B6: 0<e; then
consider N1 be Nat such that
B7: for n being Nat st n>=N1 holds
|.ProjMap1(Partial_Sums Rseq,m).n
- lim(ProjMap1(Partial_Sums Rseq,m)).| < e/2 by B4,SEQ_2:def 7;
consider N2 be Nat such that
B8: for n being Nat st n>=N2 holds
|.ProjMap1(Partial_Sums Rseq,k).n
- lim(ProjMap1(Partial_Sums Rseq,k)).| < e/2
by B4,B6,SEQ_2:def 7;
reconsider N=max(N1,N2) as Nat by TARSKI:1;
take N;
hereby let n be Nat;
assume B9: n>=N;
N >= N1 & N >= N2 by XXREAL_0:25; then
n >= N1 & n >= N2 by B9,XXREAL_0:2; then
|.ProjMap1(Partial_Sums Rseq,m).n
- lim(ProjMap1(Partial_Sums Rseq,m)).| < e/2
& |.ProjMap1(Partial_Sums Rseq,k).n
- lim(ProjMap1(Partial_Sums Rseq,k)).| < e/2 by B7,B8; then
B12: |.ProjMap1(Partial_Sums Rseq,m).n
- lim(ProjMap1(Partial_Sums Rseq,m)).|
+ |.ProjMap1(Partial_Sums Rseq,k).n
- lim(ProjMap1(Partial_Sums Rseq,k)).| < e/2 + e/2
by XREAL_1:8;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
ProjMap1(Partial_Sums Rseq,k).n
= (Partial_Sums Rseq).(k,n1) by MESFUNC9:def 6
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(m+1,n1)
by B2,th103a
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(m,n1)
+ (Partial_Sums_in_cod2 Rseq).(m+1,n1) by DefRS
.= (Partial_Sums Rseq).(m,n1)
+ (Partial_Sums_in_cod2 Rseq).(k,n1) by B2,th103a
.= ProjMap1(Partial_Sums Rseq,m).n
+ (Partial_Sums_in_cod2 Rseq).(k,n1) by MESFUNC9:def 6
.= ProjMap1(Partial_Sums Rseq,m).n
+ ProjMap1(Partial_Sums_in_cod2 Rseq,k).n by MESFUNC9:def 6; then
|.ProjMap1(Partial_Sums_in_cod2 Rseq,k).n
- ( lim(ProjMap1(Partial_Sums Rseq,k))
- lim(ProjMap1(Partial_Sums Rseq,m)) ).|
= |.( ProjMap1(Partial_Sums Rseq,k).n
- lim(ProjMap1(Partial_Sums Rseq,k)) )
-( ProjMap1(Partial_Sums Rseq,m).n
- lim(ProjMap1(Partial_Sums Rseq,m)) ).|; then
|.ProjMap1(Partial_Sums_in_cod2 Rseq,k).n
- ( lim(ProjMap1(Partial_Sums Rseq,k))
- lim(ProjMap1(Partial_Sums Rseq,m)) ).|
<= |.ProjMap1(Partial_Sums Rseq,k).n
- lim(ProjMap1(Partial_Sums Rseq,k)).|
+ |.ProjMap1(Partial_Sums Rseq,m).n
- lim(ProjMap1(Partial_Sums Rseq,m)).| by COMPLEX1:57;
hence |.ProjMap1(Partial_Sums_in_cod2 Rseq,k).n
- ( lim(ProjMap1(Partial_Sums Rseq,k))
- lim(ProjMap1(Partial_Sums Rseq,m)) ).| < e by B12,XXREAL_0:2;
end;
end;
hence ProjMap1(Partial_Sums_in_cod2 Rseq,k) is convergent
by SEQ_2:def 6;
end;
end;
for m1 being Nat holds P[m1] from NAT_1:sch 2(A3,A4);
hence ProjMap1(Partial_Sums_in_cod2 Rseq,m) is convergent;
end;
hence Partial_Sums_in_cod2 Rseq is convergent_in_cod2;
end;
assume C0: Partial_Sums_in_cod2 Rseq is convergent_in_cod2;
now let m be Element of NAT;
defpred P[Nat] means
for k being Element of NAT st k = $1 holds
ProjMap1(Partial_Sums Rseq,k) is convergent;
ProjMap1(Partial_Sums Rseq,0) = ProjMap1(Partial_Sums_in_cod2 Rseq,0)
by th00; then
C1: P[0] by C0;
C2: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume C3: P[m];
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
hereby let k be Element of NAT;
assume C4: k=m+1; then
reconsider k1=k-1 as Element of NAT by NAT_1:11,21;
for n being Element of NAT holds
ProjMap1(Partial_Sums Rseq,k).n
= (ProjMap1(Partial_Sums Rseq,m1)
+ ProjMap1(Partial_Sums_in_cod2 Rseq,m1+1)).n
proof
let n be Element of NAT;
ProjMap1(Partial_Sums Rseq,k).n
= (Partial_Sums Rseq).(m1+1,n) by C4,MESFUNC9:def 6
.= (Partial_Sums_in_cod2 Rseq).(m1+1,n)
+ (Partial_Sums_in_cod2(Partial_Sums_in_cod1 Rseq)).(m1,n) by ThRS
.= ProjMap1(Partial_Sums_in_cod2 Rseq,m1+1).n
+ (Partial_Sums Rseq).(m1,n) by MESFUNC9:def 6
.= ProjMap1(Partial_Sums_in_cod2 Rseq,m1+1).n
+ ProjMap1(Partial_Sums Rseq,m1).n by MESFUNC9:def 6;
hence thesis by VALUED_1:1;
end; then
C5: ProjMap1(Partial_Sums Rseq,k)
= ProjMap1(Partial_Sums Rseq,m1)
+ ProjMap1(Partial_Sums_in_cod2 Rseq,m1+1);
ProjMap1(Partial_Sums Rseq,m1) is convergent
& ProjMap1(Partial_Sums_in_cod2 Rseq,m1+1) is convergent by C3,C0;
hence ProjMap1(Partial_Sums Rseq,k) is convergent by C5,SEQ_2:5;
end;
end;
for m being Nat holds P[m] from NAT_1:sch 2(C1,C2);
hence ProjMap1(Partial_Sums Rseq,m) is convergent;
end;
hence Partial_Sums Rseq is convergent_in_cod2;
end;
theorem th02a:
Partial_Sums Rseq is convergent_in_cod1 implies
for k being Nat holds
(lim_in_cod1(Partial_Sums Rseq)).(k+1)
= (lim_in_cod1(Partial_Sums Rseq)).k
+ (lim_in_cod1(Partial_Sums_in_cod1 Rseq)).(k+1)
proof
assume A1: Partial_Sums Rseq is convergent_in_cod1;
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
Partial_Sums_in_cod1 Rseq is convergent_in_cod1 by A1,th01a; then
A2:ProjMap2(Partial_Sums Rseq,k1) is convergent
& ProjMap2(Partial_Sums_in_cod1 Rseq,k1+1) is convergent by A1;
A3:(lim_in_cod1(Partial_Sums Rseq)).(k+1)
= lim ProjMap2(Partial_Sums Rseq,k1+1) by DBLSEQ_1:def 5;
A4:(lim_in_cod1(Partial_Sums Rseq)).k
= lim ProjMap2(Partial_Sums Rseq,k1)
& (lim_in_cod1(Partial_Sums_in_cod1 Rseq)).(k+1)
= lim ProjMap2(Partial_Sums_in_cod1 Rseq,k1+1) by DBLSEQ_1:def 5;
now let j be Element of NAT;
B1: ProjMap2(Partial_Sums Rseq,k1).j
= (Partial_Sums_in_cod2(Partial_Sums_in_cod1 Rseq)).(j,k1)
by MESFUNC9:def 7;
ProjMap2(Partial_Sums_in_cod1 Rseq,k1+1).j
= (Partial_Sums_in_cod1 Rseq).(j,k1+1) by MESFUNC9:def 7; then
ProjMap2(Partial_Sums Rseq,k1).j
+ ProjMap2(Partial_Sums_in_cod1 Rseq,k1+1).j
= (Partial_Sums_in_cod2(Partial_Sums_in_cod1 Rseq)).(j,k1+1)
by B1,DefCS
.= ProjMap2(Partial_Sums Rseq,k1+1).j by MESFUNC9:def 7;
hence
ProjMap2(Partial_Sums Rseq,k1+1).j
= (ProjMap2(Partial_Sums Rseq,k1)
+ ProjMap2(Partial_Sums_in_cod1 Rseq,k1+1)).j by VALUED_1:1;
end; then
ProjMap2(Partial_Sums Rseq,k1+1)
= ProjMap2(Partial_Sums Rseq,k1)
+ ProjMap2(Partial_Sums_in_cod1 Rseq,k1+1);
hence thesis by A3,A4,A2,SEQ_2:6;
end;
theorem th02b:
Partial_Sums Rseq is convergent_in_cod2 implies
for k being Nat holds
(lim_in_cod2(Partial_Sums Rseq)).(k+1)
= (lim_in_cod2(Partial_Sums Rseq)).k
+ (lim_in_cod2(Partial_Sums_in_cod2 Rseq)).(k+1)
proof
assume A1: Partial_Sums Rseq is convergent_in_cod2;
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
Partial_Sums_in_cod2 Rseq is convergent_in_cod2 by A1,th01b; then
A2:ProjMap1(Partial_Sums Rseq,k1) is convergent
& ProjMap1(Partial_Sums_in_cod2 Rseq,k1+1) is convergent by A1;
A3:(lim_in_cod2(Partial_Sums Rseq)).(k+1)
= lim ProjMap1(Partial_Sums Rseq,k1+1) by DBLSEQ_1:def 6;
A4:(lim_in_cod2(Partial_Sums Rseq)).k
= lim ProjMap1(Partial_Sums Rseq,k1)
& (lim_in_cod2(Partial_Sums_in_cod2 Rseq)).(k+1)
= lim ProjMap1(Partial_Sums_in_cod2 Rseq,k1+1) by DBLSEQ_1:def 6;
now let j be Element of NAT;
B1: ProjMap1(Partial_Sums Rseq,k1).j
= (Partial_Sums Rseq).(k1,j) by MESFUNC9:def 6
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(k1,j) by th103a;
ProjMap1(Partial_Sums_in_cod2 Rseq,k1+1).j
= (Partial_Sums_in_cod2 Rseq).(k1+1,j) by MESFUNC9:def 6; then
ProjMap1(Partial_Sums Rseq,k1).j
+ ProjMap1(Partial_Sums_in_cod2 Rseq,k1+1).j
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(k1+1,j)
by B1,DefRS
.= (Partial_Sums Rseq).(k1+1,j) by th103a
.= ProjMap1(Partial_Sums Rseq,k1+1).j by MESFUNC9:def 6;
hence ProjMap1(Partial_Sums Rseq,k1+1).j
= (ProjMap1(Partial_Sums Rseq,k1)
+ ProjMap1(Partial_Sums_in_cod2 Rseq,k1+1)).j by VALUED_1:1;
end; then
ProjMap1(Partial_Sums Rseq,k1+1)
= ProjMap1(Partial_Sums Rseq,k1)
+ ProjMap1(Partial_Sums_in_cod2 Rseq,k1+1);
hence thesis by A3,A4,A2,SEQ_2:6;
end;
theorem th03a:
Partial_Sums Rseq is convergent_in_cod1 implies
lim_in_cod1(Partial_Sums Rseq)
= Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 Rseq))
proof
assume AS: Partial_Sums Rseq is convergent_in_cod1;
now let m be Nat;
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
defpred P[Nat] means
Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 Rseq)).$1
= (lim_in_cod1(Partial_Sums Rseq)).$1;
Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 Rseq)).0
= (lim_in_cod1(Partial_Sums_in_cod1 Rseq)).0 by SERIES_1:def 1
.= lim ProjMap2(Partial_Sums_in_cod1 Rseq,0) by DBLSEQ_1:def 5
.= lim ProjMap2(Partial_Sums Rseq,0) by th00
.= (lim_in_cod1(Partial_Sums Rseq)).0 by DBLSEQ_1:def 5; then
A1: P[0];
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A3: P[k];
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 Rseq)).(k+1)
= (lim_in_cod1(Partial_Sums Rseq)).k
+ (lim_in_cod1(Partial_Sums_in_cod1 Rseq)).(k+1) by A3,SERIES_1:def 1;
hence thesis by AS,th02a;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence (lim_in_cod1(Partial_Sums Rseq)).m
= Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 Rseq)).m;
end;
hence thesis;
end;
theorem th03b:
Partial_Sums Rseq is convergent_in_cod2 implies
lim_in_cod2(Partial_Sums Rseq)
= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 Rseq))
proof
assume AS: Partial_Sums Rseq is convergent_in_cod2;
now let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
defpred P[Nat] means
Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 Rseq)).$1
= (lim_in_cod2(Partial_Sums Rseq)).$1;
Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 Rseq)).0
= (lim_in_cod2(Partial_Sums_in_cod2 Rseq)).0 by SERIES_1:def 1
.= lim ProjMap1(Partial_Sums_in_cod2 Rseq,0) by DBLSEQ_1:def 6
.= lim ProjMap1(Partial_Sums Rseq,0) by th00
.= (lim_in_cod2(Partial_Sums Rseq)).0 by DBLSEQ_1:def 6; then
A1: P[0];
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A3: P[k];
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 Rseq)).(k+1)
= (lim_in_cod2(Partial_Sums Rseq)).k
+ (lim_in_cod2(Partial_Sums_in_cod2 Rseq)).(k+1) by A3,SERIES_1:def 1;
hence thesis by AS,th02b;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence
(lim_in_cod2(Partial_Sums Rseq)).n
= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 Rseq)).n;
end;
hence thesis;
end;
begin :: Double series of non-negative double sequence
theorem lm80:
Rseq is nonnegative-yielding implies
Partial_Sums_in_cod2 Rseq is nonnegative-yielding &
Partial_Sums_in_cod1 Rseq is nonnegative-yielding
proof
assume a1: Rseq is nonnegative-yielding;
now
let i,j be Nat;
defpred C[Nat] means (Partial_Sums_in_cod2(Rseq)).(i,$1) >= 0;
(Partial_Sums_in_cod2(Rseq)).(i,0) = Rseq.(i,0) by DefCS; then
a2:C[0] by a1;
a3:for k be Nat st C[k] holds C[k+1]
proof
let k be Nat;
assume C[k]; then
a4: (Partial_Sums_in_cod2(Rseq)).(i,k) >= 0 & Rseq.(i,k+1) >= 0 by a1;
(Partial_Sums_in_cod2(Rseq)).(i,k+1)
= (Partial_Sums_in_cod2(Rseq)).(i,k) + Rseq.(i,k+1)
by DefCS;
hence C[k+1] by a4;
end;
for k be Nat holds C[k] from NAT_1:sch 2(a2,a3);
hence (Partial_Sums_in_cod2(Rseq)).(i,j) >= 0;
defpred R[Nat] means (Partial_Sums_in_cod1(Rseq)).($1,j) >= 0;
(Partial_Sums_in_cod1(Rseq)).(0,j) = Rseq.(0,j) by DefRS; then
a5:R[0] by a1;
a6:for k be Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume R[k]; then
a7: (Partial_Sums_in_cod1(Rseq)).(k,j) >= 0 & Rseq.(k+1,j) >= 0 by a1;
(Partial_Sums_in_cod1(Rseq)).(k+1,j)
= (Partial_Sums_in_cod1(Rseq)).(k,j) + Rseq.(k+1,j)
by DefRS;
hence R[k+1] by a7;
end;
for k be Nat holds R[k] from NAT_1:sch 2(a5,a6);
hence (Partial_Sums_in_cod1(Rseq)).(i,j) >= 0;
end;
hence thesis;
end;
theorem th80a:
Rseq is nonnegative-yielding implies
Partial_Sums Rseq is non-decreasing
proof
set CPS = Partial_Sums Rseq;
assume a1: Rseq is nonnegative-yielding;
now let n1,m1,n2,m2 be Nat;
assume b2: n1>=n2 & m1>=m2; then
consider dn be Nat such that
b3: n1 = n2+dn by NAT_1:10;
consider dm be Nat such that
b4: m1 = m2+dm by b2,NAT_1:10;
reconsider dn,dm as Element of NAT by ORDINAL1:def 12;
defpred P1[Nat] means CPS.(n2+$1,m2) >= CPS.(n2,m2);
b5: P1[0];
b6: for k be Nat st P1[k] holds P1[k+1]
proof
let k be Nat;
assume a7: P1[k];
b8: CPS.(n2+k+1,m2)
= (Partial_Sums_in_cod2(Rseq)).(n2+k+1,m2) + CPS.(n2+k,m2) by ThRS;
Partial_Sums_in_cod2 Rseq is nonnegative-yielding by a1,lm80; then
CPS.(n2+k+1,m2) >= CPS.(n2+k,m2) by b8,XREAL_1:31;
hence P1[k+1] by a7,XXREAL_0:2;
end;
for k be Nat holds P1[k] from NAT_1:sch 2(b5,b6); then
b9: CPS.(n1,m2) >= CPS.(n2,m2) by b3;
defpred P2[Nat] means CPS.(n1,m2+$1) >= CPS.(n1,m2);
b10:P2[0];
b11:for k be Nat st P2[k] holds P2[k+1]
proof
let k be Nat;
assume b12: P2[k];
b13: CPS.(n1,m2+k+1)
= (Partial_Sums_in_cod1 Rseq).(n1,m2+k+1) + CPS.(n1,m2+k) by DefCS;
Partial_Sums_in_cod1 Rseq is nonnegative-yielding by a1,lm80; then
CPS.(n1,m2+k+1) >= CPS.(n1,m2+k) by b13,XREAL_1:31;
hence P2[k+1] by b12,XXREAL_0:2;
end;
for k be Nat holds P2[k] from NAT_1:sch 2(b10,b11); then
CPS.(n1,m1) >= CPS.(n1,m2) by b4;
hence CPS.(n1,m1) >= CPS.(n2,m2) by b9,XXREAL_0:2;
end;
hence Partial_Sums Rseq is non-decreasing;
end;
theorem
Rseq is nonnegative-yielding implies
(Partial_Sums Rseq is P-convergent
iff Partial_Sums Rseq is bounded_below bounded_above)
proof
assume Rseq is nonnegative-yielding; then
a2:Partial_Sums Rseq is non-decreasing by th80a;
hence Partial_Sums Rseq is P-convergent
implies Partial_Sums Rseq is bounded_below bounded_above;
assume Partial_Sums Rseq is bounded_below bounded_above;
hence Partial_Sums Rseq is P-convergent by a2;
end;
theorem lm84a:
(for n,m being Nat holds Rseq1.(n,m) <= Rseq2.(n,m)) implies
for i,j being Nat holds
(Partial_Sums_in_cod1 Rseq1).(i,j) <= (Partial_Sums_in_cod1 Rseq2).(i,j)
& (Partial_Sums_in_cod2 Rseq1).(i,j) <= (Partial_Sums_in_cod2 Rseq2).(i,j)
proof
set RS1 = Partial_Sums_in_cod1 Rseq1, RS2 = Partial_Sums_in_cod1 Rseq2;
set CS1 = Partial_Sums_in_cod2 Rseq1, CS2 = Partial_Sums_in_cod2 Rseq2;
assume a1: for n,m be Nat holds Rseq1.(n,m) <= Rseq2.(n,m);
let i,j be Nat;
defpred R[Nat] means RS1.($1,j) <=RS2.($1,j);
RS1.(0,j) = Rseq1.(0,j) & RS2.(0,j) = Rseq2.(0,j) by DefRS; then
a2:R[0] by a1;
a3:for k be Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume R[k]; then
a4: RS1.(k,j) <= RS2.(k,j) & Rseq1.(k+1,j) <= Rseq2.(k+1,j) by a1;
RS1.(k+1,j) = RS1.(k,j) + Rseq1.(k+1,j) &
RS2.(k+1,j) = RS2.(k,j) + Rseq2.(k+1,j) by DefRS;
hence R[k+1] by a4,XREAL_1:7;
end;
for k be Nat holds R[k] from NAT_1:sch 2(a2,a3);
hence RS1.(i,j) <= RS2.(i,j);
defpred C[Nat] means CS1.(i,$1) <= CS2.(i,$1);
CS1.(i,0) = Rseq1.(i,0) & CS2.(i,0) = Rseq2.(i,0) by DefCS; then
a5:C[0] by a1;
a6:for k be Nat st C[k] holds C[k+1]
proof
let k be Nat;
assume C[k]; then
a7: CS1.(i,k) <= CS2.(i,k) & Rseq1.(i,k+1) <= Rseq2.(i,k+1) by a1;
CS1.(i,k+1) = CS1.(i,k) + Rseq1.(i,k+1) &
CS2.(i,k+1) = CS2.(i,k) + Rseq2.(i,k+1) by DefCS;
hence C[k+1] by a7,XREAL_1:7;
end;
for k be Nat holds C[k] from NAT_1:sch 2(a5,a6);
hence CS1.(i,j) <= CS2.(i,j);
end;
theorem lm84:
Rseq1 is nonnegative-yielding &
(for n,m being Nat holds Rseq1.(n,m) <= Rseq2.(n,m)) implies
for i,j being Nat holds
(Partial_Sums Rseq1).(i,j) <= (Partial_Sums Rseq2).(i,j)
proof
set RPS1 = Partial_Sums(Rseq1);
set RPS2 = Partial_Sums(Rseq2);
assume
a1: Rseq1 is nonnegative-yielding &
for n,m be Nat holds Rseq1.(n,m) <= Rseq2.(n,m);
let i,j be Nat;
defpred P[Nat] means RPS1.(i,$1) <= RPS2.(i,$1);
a2:P[0]
proof
defpred Q0[Nat] means RPS1.($1,0) <= RPS2.($1,0);
a3: RPS1.(0,0) = (Partial_Sums_in_cod1(Rseq1)).(0,0) by DefCS
.= Rseq1.(0,0) by DefRS;
RPS2.(0,0) = (Partial_Sums_in_cod1(Rseq2)).(0,0) by DefCS
.= Rseq2.(0,0) by DefRS; then
a4: Q0[0] by a1,a3;
a5: for l be Nat st Q0[l] holds Q0[l+1]
proof
let l be Nat;
assume Q0[l];
RPS1.(l+1,0) = (Partial_Sums_in_cod1 Rseq1).(l+1,0)
& RPS2.(l+1,0) = (Partial_Sums_in_cod1 Rseq2).(l+1,0) by DefCS;
hence Q0[l+1] by a1,lm84a;
end;
for l be Nat holds Q0[l] from NAT_1:sch 2(a4,a5);
hence P[0];
end;
a8:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A9: P[k];
a10:(Partial_Sums_in_cod1(Rseq1)).(i,k+1)
<= (Partial_Sums_in_cod1(Rseq2)).(i,k+1) by a1,lm84a;
RPS1.(i,k+1)
= (Partial_Sums_in_cod1(Rseq1)).(i,k+1) + RPS1.(i,k) by DefCS; then
RPS1.(i,k+1) <= (Partial_Sums_in_cod1(Rseq2)).(i,k+1) + RPS2.(i,k)
by A9,a10,XREAL_1:7;
hence P[k+1] by DefCS;
end;
for k be Nat holds P[k] from NAT_1:sch 2(a2,a8);
hence RPS1.(i,j) <= RPS2.(i,j);
end;
theorem
Rseq1 is nonnegative-yielding &
(for n,m being Nat holds Rseq1.(n,m) <= Rseq2.(n,m))
& Partial_Sums Rseq2 is P-convergent
implies Partial_Sums Rseq1 is P-convergent
proof
set RPS1 = Partial_Sums Rseq1;
set RPS2 = Partial_Sums Rseq2;
assume that
a2: Rseq1 is nonnegative-yielding &
for n,m be Nat holds Rseq1.(n,m) <= Rseq2.(n,m) and
a1: RPS2 is P-convergent;
for n,m be Nat holds 0 <= Rseq2.(n,m)
proof
let n,m be Nat;
0 <= Rseq1.(n,m) & Rseq1.(n,m) <= Rseq2.(n,m) by a2;
hence 0 <= Rseq2.(n,m);
end; then
Rseq2 is nonnegative-yielding; then
RPS2 is non-decreasing by th80a; then
RPS2 is bounded_above by a1; then
consider M be Real such that
a3: M is UpperBound of RPS2.: [:NAT,NAT:] by XXREAL_2:def 10;
now let a be ExtReal;
assume a in RPS1.: [:NAT,NAT:]; then
consider x be Element of [:NAT,NAT:] such that
a5: x in [:NAT,NAT:] & a = RPS1.x by FUNCT_2:65;
consider n,m be object such that
a6: n in NAT & m in NAT & x = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Element of NAT by a6;
a7: RPS1.(n,m) <= RPS2.(n,m) by a2,lm84;
RPS2.(n,m) <= M by a3,XXREAL_2:def 1,a6,FUNCT_2:35;
hence a <= M by a5,a6,a7,XXREAL_0:2;
end; then
M is UpperBound of RPS1.: [:NAT,NAT:] by XXREAL_2:def 1; then
a8:RPS1 is bounded_above by XXREAL_2:def 10;
RPS1 is non-decreasing by a2,th80a;
hence RPS1 is P-convergent by a8;
end;
theorem th101:
for rseq being Real_Sequence, m being Nat st
rseq is nonnegative holds
rseq.m <= (Partial_Sums rseq).m
proof
let rseq be Real_Sequence, m be Nat;
assume A1: rseq is nonnegative;
defpred P[Nat] means rseq.$1 <= (Partial_Sums rseq).$1;
a3:P[0] by SERIES_1:def 1;
a4:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
(Partial_Sums rseq).(k+1) = (Partial_Sums rseq).k + rseq.(k+1)
by SERIES_1:def 1;
hence P[k+1] by XREAL_1:31,SERIES_3:34,A1;
end;
for k be Nat holds P[k] from NAT_1:sch 2(a3,a4);
hence rseq.m <= Partial_Sums(rseq).m;
end;
theorem
Rseq is nonnegative-yielding implies
(for m,n being Nat holds
Rseq.(m,n) <= (Partial_Sums_in_cod1 Rseq).(m,n) &
Rseq.(m,n) <= (Partial_Sums_in_cod2 Rseq).(m,n))
proof
assume a1: Rseq is nonnegative-yielding;
hereby let m1,n1 be Nat;
reconsider m=m1, n=n1 as Element of NAT by ORDINAL1:def 12;
now let j be Nat;
j in NAT by ORDINAL1:def 12; then
(ProjMap2(Rseq,n)).j = Rseq.(j,n) by MESFUNC9:def 7;
hence (ProjMap2(Rseq,n)).j >= 0 by a1;
end; then
(ProjMap2(Rseq,n)).m <= Partial_Sums(ProjMap2(Rseq,n)).m
by th101,RINFSUP1:def 3; then
(ProjMap2(Rseq,n)).m <= (Partial_Sums_in_cod1 Rseq).(m,n) by th100;
hence Rseq.(m1,n1) <= (Partial_Sums_in_cod1 Rseq).(m1,n1)
by MESFUNC9:def 7;
now let j be Nat;
j in NAT by ORDINAL1:def 12; then
(ProjMap1(Rseq,m)).j = Rseq.(m,j) by MESFUNC9:def 6;
hence (ProjMap1(Rseq,m)).j >= 0 by a1;
end; then
ProjMap1(Rseq,m) is nonnegative-yielding; then
(ProjMap1(Rseq,m)).n <= Partial_Sums(ProjMap1(Rseq,m)).n by th101; then
(ProjMap1(Rseq,m)).n <= (Partial_Sums_in_cod2 Rseq).(m,n) by th100;
hence Rseq.(m1,n1) <= (Partial_Sums_in_cod2 Rseq).(m1,n1)
by MESFUNC9:def 6;
end;
end;
theorem th1003:
Rseq is nonnegative-yielding implies
( for i1,i2,j being Nat st i1 <= i2 holds
(Partial_Sums_in_cod1 Rseq).(i1,j) <= (Partial_Sums_in_cod1 Rseq).(i2,j) )
& ( for i,j1,j2 being Nat st j1 <= j2 holds
(Partial_Sums_in_cod2 Rseq).(i,j1) <= (Partial_Sums_in_cod2 Rseq).(i,j2) )
proof
assume A1: Rseq is nonnegative-yielding;
A2:now let i1,i2,j be natural number;
assume i1 <= i2; then
consider k be Nat such that
A3: i2 = i1 + k by NAT_1:10;
defpred P[Nat] means
$1 <= k implies (Partial_Sums_in_cod1 Rseq).(i1,j)
<= (Partial_Sums_in_cod1 Rseq).(i1+$1,j);
A4: P[0];
A5: for l be Nat st P[l] holds P[l+1]
proof
let l be Nat;
assume A6: P[l];
now assume A7: l+1 <= k;
(Partial_Sums_in_cod1 Rseq).(i1+l+1,j)
= (Partial_Sums_in_cod1 Rseq).(i1+l,j) + Rseq.(i1+l+1,j) by DefRS; then
(Partial_Sums_in_cod1 Rseq).(i1+l,j)
<= (Partial_Sums_in_cod1 Rseq).(i1+l+1,j) by A1,XREAL_1:31;
hence (Partial_Sums_in_cod1 Rseq).(i1,j)
<= (Partial_Sums_in_cod1 Rseq).(i1+(l+1),j)
by A6,A7,NAT_1:13,XXREAL_0:2;
end;
hence P[l+1];
end;
for l be Nat holds P[l] from NAT_1:sch 2(A4,A5);
hence (Partial_Sums_in_cod1 Rseq).(i1,j)
<= (Partial_Sums_in_cod1 Rseq).(i2,j) by A3;
end;
now let i,j1,j2 be natural number;
assume j1 <= j2; then
consider k be Nat such that
B3: j2 = j1 + k by NAT_1:10;
defpred P[Nat] means
$1 <= k implies (Partial_Sums_in_cod2 Rseq).(i,j1)
<= (Partial_Sums_in_cod2 Rseq).(i,j1+$1);
B4: P[0];
B5: for l be Nat st P[l] holds P[l+1]
proof
let l be Nat;
assume B6: P[l];
now assume B7: l+1 <= k;
(Partial_Sums_in_cod2 Rseq).(i,j1+l+1)
= (Partial_Sums_in_cod2 Rseq).(i,j1+l) + Rseq.(i,j1+l+1) by DefCS; then
(Partial_Sums_in_cod2 Rseq).(i,j1+l)
<= (Partial_Sums_in_cod2 Rseq).(i,j1+l+1) by A1,XREAL_1:31;
hence (Partial_Sums_in_cod2 Rseq).(i,j1)
<= (Partial_Sums_in_cod2 Rseq).(i,j1+(l+1))
by B6,B7,NAT_1:13,XXREAL_0:2;
end;
hence P[l+1];
end;
for l be Nat holds P[l] from NAT_1:sch 2(B4,B5);
hence (Partial_Sums_in_cod2 Rseq).(i,j1)
<= (Partial_Sums_in_cod2 Rseq).(i,j2) by B3;
end;
hence thesis by A2;
end;
theorem th105:
Rseq is nonnegative-yielding implies
( for i1,i2,j be Nat st i1 <= i2 holds
(Partial_Sums Rseq).(i1,j) <= (Partial_Sums Rseq).(i2,j) )
& ( for i,j1,j2 be Nat st j1 <= j2 holds
(Partial_Sums Rseq).(i,j1) <= (Partial_Sums Rseq).(i,j2) )
proof
assume
A1: Rseq is nonnegative-yielding;
hereby let i1,i2,j be Nat;
assume A3: i1 <= i2;
defpred P[Nat] means
(Partial_Sums Rseq).(i1,$1) <= (Partial_Sums Rseq).(i2,$1);
(Partial_Sums Rseq).(i1,0) = (Partial_Sums_in_cod1 Rseq).(i1,0)
& (Partial_Sums Rseq).(i2,0) = (Partial_Sums_in_cod1 Rseq).(i2,0)
by DefCS; then
A4: P[0] by A3,A1,th1003;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
A7: (Partial_Sums_in_cod1 Rseq).(i1,k+1)
<= (Partial_Sums_in_cod1 Rseq).(i2,k+1) by A3,A1,th1003;
(Partial_Sums Rseq).(i1,k+1)
= (Partial_Sums Rseq).(i1,k) + (Partial_Sums_in_cod1 Rseq).(i1,k+1)
& (Partial_Sums Rseq).(i2,k+1)
= (Partial_Sums Rseq).(i2,k) + (Partial_Sums_in_cod1 Rseq).(i2,k+1)
by DefCS;
hence thesis by A6,A7,XREAL_1:7;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A5);
hence (Partial_Sums Rseq).(i1,j) <= (Partial_Sums Rseq).(i2,j);
end;
hereby let i,j1,j2 be Nat;
assume B3: j1 <= j2;
defpred Q[Nat] means
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).($1,j1)
<= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).($1,j2);
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(0,j1)
= (Partial_Sums_in_cod2 Rseq).(0,j1)
& (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(0,j2)
= (Partial_Sums_in_cod2 Rseq).(0,j2) by DefRS; then
B4: Q[0] by B3,A1,th1003;
B5: for k be Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume C6: Q[k];
C7: (Partial_Sums_in_cod2 Rseq).(k+1,j1)
<= (Partial_Sums_in_cod2 Rseq).(k+1,j2) by B3,A1,th1003;
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(k+1,j1)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(k,j1)
+ (Partial_Sums_in_cod2 Rseq).(k+1,j1)
& (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(k+1,j2)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(k,j2)
+ (Partial_Sums_in_cod2 Rseq).(k+1,j2) by DefRS;
hence thesis by C6,C7,XREAL_1:7;
end;
B6: for k be Nat holds Q[k] from NAT_1:sch 2(B4,B5);
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(i,j1)
= (Partial_Sums Rseq).(i,j1)
& (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(i,j2)
= (Partial_Sums Rseq).(i,j2) by th103;
hence (Partial_Sums Rseq).(i,j1) <= (Partial_Sums Rseq).(i,j2) by B6;
end;
end;
theorem
Rseq is nonnegative-yielding implies
(for i1,i2,j1,j2 being Nat st i1 <= i2 & j1 <= j2 holds
(Partial_Sums Rseq).(i1,j1) <= (Partial_Sums Rseq).(i2,j2))
proof
assume A1: Rseq is nonnegative-yielding;
hereby let i1,i2,j1,j2 be Nat;
assume i1<=i2 & j1<=j2; then
(Partial_Sums Rseq).(i1,j1) <= (Partial_Sums Rseq).(i1,j2)
& (Partial_Sums Rseq).(i1,j2) <= (Partial_Sums Rseq).(i2,j2)
by A1,th105;
hence (Partial_Sums Rseq).(i1,j1) <= (Partial_Sums Rseq).(i2,j2)
by XXREAL_0:2;
end;
end;
theorem th1005:
Rseq is nonnegative-yielding implies
for k being Element of NAT holds
ProjMap2(Partial_Sums_in_cod1 Rseq,k) is non-decreasing
& ProjMap1(Partial_Sums_in_cod2 Rseq,k) is non-decreasing
& ProjMap2(Partial_Sums_in_cod1 Rseq,k) is nonnegative
& ProjMap1(Partial_Sums_in_cod2 Rseq,k) is nonnegative
& ProjMap2(Partial_Sums_in_cod2 Rseq,k) is nonnegative
& ProjMap1(Partial_Sums_in_cod1 Rseq,k) is nonnegative
proof
assume
A1: Rseq is nonnegative-yielding;
hereby let k be Element of NAT;
X1: now let i be Nat;
i is Element of NAT by ORDINAL1:def 12; then
A3: ProjMap2(Partial_Sums_in_cod1 Rseq,k).i
= (Partial_Sums_in_cod1 Rseq).(i,k) by MESFUNC9:def 7;
ProjMap2(Partial_Sums_in_cod1 Rseq,k).(i+1)
= (Partial_Sums_in_cod1 Rseq).(i+1,k) by MESFUNC9:def 7
.= (Partial_Sums_in_cod1 Rseq).(i,k) + Rseq.(i+1,k) by DefRS;
hence ProjMap2(Partial_Sums_in_cod1 Rseq,k).i
<= ProjMap2(Partial_Sums_in_cod1 Rseq,k).(i+1) by A1,A3,XREAL_1:31;
end;
hence ProjMap2(Partial_Sums_in_cod1 Rseq,k) is non-decreasing
by VALUED_1:def 15;
X2: now let j be Nat;
j is Element of NAT by ORDINAL1:def 12; then
A5: ProjMap1(Partial_Sums_in_cod2 Rseq,k).j
= (Partial_Sums_in_cod2 Rseq).(k,j) by MESFUNC9:def 6;
ProjMap1(Partial_Sums_in_cod2 Rseq,k).(j+1)
= (Partial_Sums_in_cod2 Rseq).(k,j+1) by MESFUNC9:def 6
.= (Partial_Sums_in_cod2 Rseq).(k,j) + Rseq.(k,j+1) by DefCS;
hence ProjMap1(Partial_Sums_in_cod2 Rseq,k).j
<= ProjMap1(Partial_Sums_in_cod2 Rseq,k).(j+1) by A1,A5,XREAL_1:31;
end;
hence ProjMap1(Partial_Sums_in_cod2 Rseq,k) is non-decreasing
by VALUED_1:def 15;
B1: ProjMap2(Partial_Sums_in_cod1 Rseq,k).0
= (Partial_Sums_in_cod1 Rseq).(0,k) by MESFUNC9:def 7
.= Rseq.(0,k) by DefRS;
now let i be Nat;
ProjMap2(Partial_Sums_in_cod1 Rseq,k).(i+0)
>= ProjMap2(Partial_Sums_in_cod1 Rseq,k).0
by X1,SEQM_3:5,VALUED_1:def 15;
hence ProjMap2(Partial_Sums_in_cod1 Rseq,k).i >= 0 by B1,A1;
end;
hence ProjMap2(Partial_Sums_in_cod1 Rseq,k) is nonnegative;
B2: ProjMap1(Partial_Sums_in_cod2 Rseq,k).0
= (Partial_Sums_in_cod2 Rseq).(k,0) by MESFUNC9:def 6
.= Rseq.(k,0) by DefCS;
now let i be Nat;
ProjMap1(Partial_Sums_in_cod2 Rseq,k).(i+0)
>= ProjMap1(Partial_Sums_in_cod2 Rseq,k).0
by X2,SEQM_3:5,VALUED_1:def 15;
hence ProjMap1(Partial_Sums_in_cod2 Rseq,k).i >= 0 by B2,A1;
end;
hence ProjMap1(Partial_Sums_in_cod2 Rseq,k) is nonnegative;
now let i be Nat;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
B3: ProjMap2(Partial_Sums_in_cod2 Rseq,k).i
= (Partial_Sums_in_cod2 Rseq).(i1,k) by MESFUNC9:def 7
.= (Partial_Sums(ProjMap1(Rseq,i1))).k by th100;
(ProjMap1(Rseq,i1)).k = Rseq.(i1,k) by MESFUNC9:def 6; then
B4: (ProjMap1(Rseq,i1)).k >= 0 by A1;
now let p be Nat;
p is Element of NAT by ORDINAL1:def 12; then
(ProjMap1(Rseq,i1)).p = Rseq.(i1,p) by MESFUNC9:def 6;
hence (ProjMap1(Rseq,i1)).p >= 0 by A1;
end; then
ProjMap1(Rseq,i1) is nonnegative-yielding;
hence ProjMap2(Partial_Sums_in_cod2 Rseq,k).i >= 0 by B3,B4,th101;
end;
hence ProjMap2(Partial_Sums_in_cod2 Rseq,k) is nonnegative;
now let i be Nat;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
B5: ProjMap1(Partial_Sums_in_cod1 Rseq,k).i
= (Partial_Sums_in_cod1 Rseq).(k,i1) by MESFUNC9:def 6
.= (Partial_Sums(ProjMap2(Rseq,i1))).k by th100;
(ProjMap2(Rseq,i1)).k = Rseq.(k,i1) by MESFUNC9:def 7; then
B6: (ProjMap2(Rseq,i1)).k >= 0 by A1;
now let p be Nat;
p is Element of NAT by ORDINAL1:def 12; then
(ProjMap2(Rseq,i1)).p = Rseq.(p,i1) by MESFUNC9:def 7;
hence (ProjMap2(Rseq,i1)).p >= 0 by A1;
end; then
ProjMap2(Rseq,i1) is nonnegative-yielding;
hence ProjMap1(Partial_Sums_in_cod1 Rseq,k).i >= 0 by B5,B6,th101;
end;
hence ProjMap1(Partial_Sums_in_cod1 Rseq,k) is nonnegative;
end;
end;
theorem th1006:
Rseq is nonnegative-yielding &
Partial_Sums Rseq is P-convergent implies
Partial_Sums_in_cod1 Rseq is convergent_in_cod1
& Partial_Sums_in_cod2 Rseq is convergent_in_cod2
proof
assume that
A1: Rseq is nonnegative-yielding and
A2: Partial_Sums Rseq is P-convergent;
now let k be Element of NAT;
B1: ProjMap2(Partial_Sums_in_cod1 Rseq,k) is non-decreasing by A1,th1005;
now let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
B2: (Partial_Sums Rseq).(n,k)
= (Partial_Sums(ProjMap1(Partial_Sums_in_cod1 Rseq,n1))).k by th100;
B3: (ProjMap2(Partial_Sums_in_cod1 Rseq,k)).n1
= (Partial_Sums_in_cod1 Rseq).(n1,k) by MESFUNC9:def 7
.= (ProjMap1(Partial_Sums_in_cod1 Rseq,n1)).k by MESFUNC9:def 6;
now let d be Nat;
ProjMap1(Partial_Sums_in_cod1 Rseq,n1) is nonnegative by A1,th1005;
hence (ProjMap1(Partial_Sums_in_cod1 Rseq,n1)).d >= 0;
end; then
ProjMap1(Partial_Sums_in_cod1 Rseq,n1) is nonnegative-yielding; then
B4: (ProjMap2(Partial_Sums_in_cod1 Rseq,k)).n1
<= (Partial_Sums Rseq).(n,k) by B2,B3,th101;
consider N be Nat such that
B6: for n,m being Nat st n>=N & m>=N holds
|. (Partial_Sums Rseq).(n,m) - P-lim(Partial_Sums Rseq) .| < 1
by A2,DBLSEQ_1:def 2;
reconsider N1 = max(N,max(k,n)) as Nat by TARSKI:1;
B7: N1>=N & N1>=max(k,n) & max(k,n)>=k & max(k,n)>=n by XXREAL_0:25; then
|.(Partial_Sums Rseq).(N1,N1)- P-lim(Partial_Sums Rseq).| < 1 by B6; then
(Partial_Sums Rseq).(N1,N1) - P-lim(Partial_Sums Rseq) <= 1
by ABSVALUE:5; then
(Partial_Sums Rseq).(N1,N1) - P-lim(Partial_Sums Rseq) < 2
by XXREAL_0:2; then
B8: (Partial_Sums Rseq).(N1,N1) < P-lim(Partial_Sums Rseq) + 2 by XREAL_1:19;
B9: N1>=k & N1>=n by B7,XXREAL_0:2;
Partial_Sums Rseq is non-decreasing by A1,th80a; then
(Partial_Sums Rseq).(n,k) <= (Partial_Sums Rseq).(N1,N1) by B9; then
(ProjMap2(Partial_Sums_in_cod1 Rseq,k)).n
<= (Partial_Sums Rseq).(N1,N1) by B4,XXREAL_0:2;
hence (ProjMap2(Partial_Sums_in_cod1 Rseq,k)).n
< P-lim(Partial_Sums Rseq) + 2 by B8,XXREAL_0:2;
end; then
ProjMap2(Partial_Sums_in_cod1 Rseq,k) is bounded_above by SEQ_2:def 3;
hence ProjMap2(Partial_Sums_in_cod1 Rseq,k) is convergent by B1;
end;
hence Partial_Sums_in_cod1 Rseq is convergent_in_cod1;
now let k be Element of NAT;
C1: ProjMap1(Partial_Sums_in_cod2 Rseq,k) is non-decreasing by A1,th1005;
now let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
B2: (Partial_Sums Rseq).(k,n)
= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(k,n) by th103
.= (Partial_Sums(ProjMap2(Partial_Sums_in_cod2 Rseq,n1))).k by th100;
B3: (ProjMap1(Partial_Sums_in_cod2 Rseq,k)).n1
= (Partial_Sums_in_cod2 Rseq).(k,n1) by MESFUNC9:def 6
.= (ProjMap2(Partial_Sums_in_cod2 Rseq,n1)).k by MESFUNC9:def 7;
now let d be Nat;
ProjMap2(Partial_Sums_in_cod2 Rseq,n1) is nonnegative by A1,th1005;
hence (ProjMap2(Partial_Sums_in_cod2 Rseq,n1)).d >= 0;
end; then
ProjMap2(Partial_Sums_in_cod2 Rseq,n1) is nonnegative-yielding; then
B4: (ProjMap1(Partial_Sums_in_cod2 Rseq,k)).n1
<= (Partial_Sums Rseq).(k,n) by B2,B3,th101;
consider N be Nat such that
B6: for n,m being Nat st n>=N & m>=N holds
|. (Partial_Sums Rseq).(n,m) - P-lim(Partial_Sums Rseq) .| < 1
by A2,DBLSEQ_1:def 2;
reconsider N1 = max(N,max(k,n)) as Nat by TARSKI:1;
B7: N1>=N & N1>=max(k,n) & max(k,n)>=k & max(k,n)>=n by XXREAL_0:25; then
|.(Partial_Sums Rseq).(N1,N1)- P-lim(Partial_Sums Rseq).| < 1 by B6; then
(Partial_Sums Rseq).(N1,N1) - P-lim(Partial_Sums Rseq) <= 1
by ABSVALUE:5; then
(Partial_Sums Rseq).(N1,N1) - P-lim(Partial_Sums Rseq) < 2
by XXREAL_0:2; then
B8: (Partial_Sums Rseq).(N1,N1) < P-lim(Partial_Sums Rseq) + 2 by XREAL_1:19;
B9: N1>=k & N1>=n by B7,XXREAL_0:2;
Partial_Sums Rseq is non-decreasing by A1,th80a; then
(Partial_Sums Rseq).(k,n) <= (Partial_Sums Rseq).(N1,N1) by B9; then
(ProjMap1(Partial_Sums_in_cod2 Rseq,k)).n
<= (Partial_Sums Rseq).(N1,N1) by B4,XXREAL_0:2;
hence (ProjMap1(Partial_Sums_in_cod2 Rseq,k)).n
< P-lim(Partial_Sums Rseq) + 2 by B8,XXREAL_0:2;
end; then
ProjMap1(Partial_Sums_in_cod2 Rseq,k) is bounded_above by SEQ_2:def 3;
hence ProjMap1(Partial_Sums_in_cod2 Rseq,k) is convergent by C1;
end;
hence Partial_Sums_in_cod2 Rseq is convergent_in_cod2;
end;
theorem th1006a:
Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent implies
Partial_Sums Rseq is convergent_in_cod1
& Partial_Sums Rseq is convergent_in_cod2
proof
assume that
A1: Rseq is nonnegative-yielding and
A2: Partial_Sums Rseq is P-convergent;
Partial_Sums_in_cod1 Rseq is convergent_in_cod1
& Partial_Sums_in_cod2 Rseq is convergent_in_cod2 by A1,A2,th1006;
hence thesis by th01a,th01b;
end;
theorem
Rseq is nonnegative-yielding &
Partial_Sums Rseq is P-convergent implies
lim_in_cod1(Partial_Sums_in_cod1 Rseq) is summable
& lim_in_cod2(Partial_Sums_in_cod2 Rseq) is summable
proof
assume that
A1: Rseq is nonnegative-yielding and
A2: Partial_Sums Rseq is P-convergent;
Partial_Sums Rseq is convergent_in_cod1
& Partial_Sums Rseq is convergent_in_cod2 by A1,A2,th1006a; then
A3:lim_in_cod1(Partial_Sums Rseq) is convergent
& lim_in_cod2(Partial_Sums Rseq) is convergent by A2; then
Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 Rseq)) is convergent
by A1,A2,th1006a,th03a;
hence lim_in_cod1(Partial_Sums_in_cod1 Rseq) is summable by SERIES_1:def 2;
Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 Rseq)) is convergent
by A3,A1,A2,th1006a,th03b;
hence lim_in_cod2(Partial_Sums_in_cod2 Rseq) is summable by SERIES_1:def 2;
end;
theorem
Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent implies
P-lim(Partial_Sums Rseq) = Sum(lim_in_cod1(Partial_Sums_in_cod1 Rseq))
& P-lim(Partial_Sums Rseq) = Sum(lim_in_cod2(Partial_Sums_in_cod2 Rseq))
proof
assume that
A1: Rseq is nonnegative-yielding and
A2: Partial_Sums Rseq is P-convergent;
A4:Partial_Sums Rseq is convergent_in_cod1
& Partial_Sums Rseq is convergent_in_cod2 by A1,A2,th1006a;
A5:Sum(lim_in_cod1(Partial_Sums_in_cod1 Rseq))
= lim Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 Rseq))
by SERIES_1:def 3;
for e be Real st 0<e ex M be Nat st
for m be Nat st m>=M holds
|.(lim_in_cod1(Partial_Sums Rseq)).m
- cod1_major_iterated_lim(Partial_Sums Rseq).| < e
by A2,A4,DBLSEQ_1:def 7; then
cod1_major_iterated_lim(Partial_Sums Rseq)
= lim(lim_in_cod1(Partial_Sums Rseq)) by A2,A4,SEQ_2:def 7
.= Sum(lim_in_cod1(Partial_Sums_in_cod1 Rseq)) by A5,A1,A2,th1006a,th03a;
hence P-lim(Partial_Sums Rseq)
= Sum(lim_in_cod1(Partial_Sums_in_cod1 Rseq))
by A1,A2,th1006a,DBLSEQ_1:4;
A6:Sum(lim_in_cod2(Partial_Sums_in_cod2 Rseq))
= lim Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 Rseq))
by SERIES_1:def 3;
for e be Real st 0<e ex M be Nat st
for m be Nat st m>=M holds
|.(lim_in_cod2(Partial_Sums Rseq)).m
- cod2_major_iterated_lim(Partial_Sums Rseq).| < e
by A2,A4,DBLSEQ_1:def 8; then
cod2_major_iterated_lim(Partial_Sums Rseq)
= lim(lim_in_cod2(Partial_Sums Rseq)) by A2,A4,SEQ_2:def 7
.= Sum(lim_in_cod2(Partial_Sums_in_cod2 Rseq)) by A6,A1,A2,th1006a,th03b;
hence P-lim(Partial_Sums Rseq)
= Sum(lim_in_cod2(Partial_Sums_in_cod2 Rseq))
by A1,A2,th1006a,DBLSEQ_1:3;
end;
begin :: Summability for rearrangements of non-negative real sequence
theorem TMP6:
for s1,s2 be Real_Sequence
st s1 is nonnegative & s1,s2 are_fiberwise_equipotent
holds s2 is nonnegative
proof
let s1,s2 be Real_Sequence;
assume that
A1: s1 is nonnegative and
A2: s1,s2 are_fiberwise_equipotent;
consider H be Function such that
A3: dom H = dom s2 & rng H = dom s1 & H is one-to-one & s2=s1*H
by A2,CLASSES1:77;
A4:dom H = NAT & rng H = NAT by A3,FUNCT_2:def 1;
now let m be Nat;
A6: H.m in dom s1 by A3,A4,ORDINAL1:def 12,FUNCT_1:3;
s2.m = s1.(H.m) by A3,A4,ORDINAL1:def 12,FUNCT_1:13;
hence 0 <= s2.m by A1,A6;
end;
hence s2 is nonnegative;
end;
theorem SH1:
for X being non empty set, s being sequence of X, n being Nat
holds dom(Shift(s|(Segm n),1)) = Seg n
proof
let X be non empty set;
let s be sequence of X;
let n be Nat;
Segm n c= NAT; then
NAT /\ Segm n = Segm n by XBOOLE_1:28; then
dom s /\ Segm n = Segm n by FUNCT_2:def 1; then
A2:dom(s|Segm n) = Segm n by RELAT_1:61;
A3:dom Shift(s|(Segm n),1)
= {m+1 where m is Nat : m in dom(s|(Segm n))} by VALUED_1:def 12;
now let k be object;
assume k in dom Shift(s|(Segm n),1); then
consider m be Nat such that
A4: k = m+1 & m in dom(s|(Segm n)) by A3;
per cases;
suppose n = 0;
hence k in Seg n by A4;
end;
suppose n <> 0; then
reconsider n1 = n-1 as Element of NAT by NAT_1:20;
reconsider n1 as Nat;
B3: n = n1 + 1;
m in Segm(n1+1) by A4,RELAT_1:57; then
m in succ Segm n1 by NAT_1:38; then
m in {l where l is Nat : l <= n1} by NAT_1:54; then
consider l be Nat such that
A5: m = l & l <= n1;
1 <= m+1 & m+1 <= n by A5,B3,NAT_1:11,XREAL_1:6;
hence k in Seg n by A4,FINSEQ_1:1;
end;
end; then
A6:dom Shift(s|(Segm n),1) c= Seg n;
now let k be object;
assume k in Seg n; then
k in {l where l is Nat : 1 <= l & l <= n} by FINSEQ_1:def 1; then
consider l be Nat such that
A7: k = l & 1 <= l & l <= n;
0 < l by A7; then
reconsider l1 = l-1 as Element of NAT by NAT_1:20;
0 < n by A7; then
reconsider i = n-1 as Element of NAT by NAT_1:20;
B5: n = i+1;
B9: k = l1 + 1 by A7;
l1 <= i by A7,XREAL_1:9; then
l1 in {m where m is Nat : m <= i}; then
l1 in succ Segm i by NAT_1:54; then
l1 in Segm n by B5,NAT_1:38;
hence k in dom Shift(s|(Segm n),1) by A2,A3,B9;
end; then
Seg n c= dom Shift(s|(Segm n),1);
hence dom Shift(s|(Segm n),1) = Seg n by A6,XBOOLE_0:def 10;
end;
registration
let X be non empty set;
let s be sequence of X;
let n be Nat;
cluster Shift(s|(Segm n),1) -> FinSequence-like;
coherence
proof
dom(Shift(s|(Segm n),1)) = Seg n by SH1;
hence thesis by FINSEQ_1:def 2;
end;
end;
theorem SH2:
for X being non empty set, s being sequence of X, n being Nat
holds Shift(s|(Segm n),1) is FinSequence of X
proof
let X be non empty set, s be sequence of X, n be Nat;
rng Shift(s|(Segm n),1) c= X;
hence thesis by FINSEQ_1:def 4;
end;
theorem SH3:
for X being non empty set, s being sequence of X, n,m being Nat
st m+1 in dom Shift(s|Segm n, 1) holds Shift(s|Segm n,1).(m+1) = s.m
proof
let X be non empty set;
let s be sequence of X;
let n,m be Nat;
assume m+1 in dom Shift(s|Segm n,1); then
consider k be Nat such that
A1: k in dom(s|Segm n) & m+1 = k+1 by VALUED_1:39;
Shift(s|Segm n,1).(m+1) = (s|Segm n).m by A1,VALUED_1:def 12;
hence Shift(s|Segm n,1).(m+1) = s.m by A1,FUNCT_1:47;
end;
theorem SH4:
for X being non empty set, s being sequence of X holds
Shift(s|(Segm 0),1) = {} & Shift(s|(Segm 1),1) = <*s.0*>
& Shift(s|(Segm 2),1) = <*s.0,s.1*>
& for n being Nat holds Shift(s|(Segm(n+1)),1) =
Shift(s|(Segm n),1)^<*s.n*>
proof
let X be non empty set, s be sequence of X;
thus Shift(s|(Segm 0),1) = {};
A1:dom(Shift(s|(Segm 1),1)) = Seg 1 by SH1; then
1 in dom(Shift(s|(Segm 1),1)) by FINSEQ_1:2,TARSKI:def 1; then
ex n being Nat st n in dom(s|(Segm 1)) & 1 = n+1 by VALUED_1:39; then
A3:Shift(s|(Segm 1),1).1 = (s|(Segm 1)).0 by VALUED_1:def 12;
0 in {0} by TARSKI:def 1; then
0 in Segm 1 by CARD_1:49,ORDINAL1:def 17;
hence Shift(s|(Segm 1),1) = <*s.0*> by A1,A3,FUNCT_1:49,FINSEQ_1:def 8;
A6:dom(Shift(s|(Segm 2),1)) = Seg 2 by SH1; then
A4:len(Shift(s|(Segm 2),1)) = 2 by FINSEQ_1:def 3;
A5:Segm 2 = {0,1} by CARD_1:50,ORDINAL1:def 17;
A7:1 in dom(Shift(s|(Segm 2),1)) & 2 in dom(Shift(s|(Segm 2),1))
by A6,FINSEQ_1:2,TARSKI:def 2; then
ex n being Nat st n in dom(s|(Segm 2)) & 1 = n+1 by VALUED_1:39; then
A9:Shift(s|(Segm 2),1).1 = (s|(Segm 2)).0 by VALUED_1:def 12;
0 in Segm 2 by A5,TARSKI:def 2; then
A10:Shift(s|(Segm 2),1).1 = s.0 by A9,FUNCT_1:49;
ex m be Nat st m in dom(s|(Segm 2)) & 2 = m+1 by A7,VALUED_1:39; then
A12:Shift(s|(Segm 2),1).2 = (s|(Segm 2)).1 by VALUED_1:def 12;
1 in Segm 2 by A5,TARSKI:def 2;
hence Shift(s|(Segm 2),1) = <*s.0,s.1*>
by A4,A10,A12,FUNCT_1:49,FINSEQ_1:44;
hereby let n be Nat;
X3: n is Element of NAT by ORDINAL1:def 12;
dom(Shift(s|(Segm(n+1)),1)) = Seg(n+1) & dom(Shift(s|(Segm n),1)) = Seg n
by SH1; then
A13:len(Shift(s|(Segm(n+1)),1)) = n+1 & len(Shift(s|(Segm n),1)) = n
by X3,FINSEQ_1:def 3;
A14:len <*s.n*> = 1 by FINSEQ_1:40;
A15:for k be Nat st k in dom(Shift(s|(Segm n),1)) holds
Shift(s|(Segm(n+1)),1).k = Shift(s|(Segm n),1).k
proof
let k be Nat;
assume A17: k in dom(Shift(s|(Segm n),1)); then
A18: k in Seg n by SH1; then
1 <= k by FINSEQ_1:1; then
reconsider k1 = k-1 as Element of NAT by NAT_1:21;
Seg n c= Seg(n+1) by FINSEQ_3:18; then
k in Seg(n+1) by A18; then
A19: k in dom(Shift(s|Segm(n+1),1)) by SH1;
k = k1 + 1; then
Shift(s|Segm n,1).k = s.k1 & Shift(s|Segm(n+1),1).k = s.k1 by A17,A19,SH3;
hence thesis;
end;
for k be Nat st k in dom <*s.n*>
holds Shift(s|(Segm(n+1)),1).(len Shift(s|(Segm n),1) + k) = <*s.n*>.k
proof
let k be Nat;
assume k in dom <*s.n*>; then
k in Seg 1 by FINSEQ_1:def 8; then
A20: k = 1 by FINSEQ_1:2,TARSKI:def 1; then
A23: <*s.n*>.k = s.n by FINSEQ_1:def 8;
A21: n is Element of NAT by ORDINAL1:def 12;
dom Shift(s|Segm n,1) = Seg n by SH1; then
A22: len Shift(s|Segm n,1) = n by A21,FINSEQ_1:def 3;
n+1 in Seg(n+1) by FINSEQ_1:4; then
n+1 in dom Shift(s|Segm(n+1),1) by SH1;
hence thesis by A23,A22,A20,SH3;
end;
hence Shift(s|(Segm(n+1)),1) = Shift(s|(Segm n),1)^ <*s.n*>
by A13,A14,A15,FINSEQ_3:38;
end;
end;
theorem SH5:
for s being Real_Sequence, n being Nat holds
(Partial_Sums s).n = Sum(Shift(s|Segm(n+1),1))
proof
let s be Real_Sequence, n be Nat;
defpred P[Nat] means (Partial_Sums s).$1 = Sum(Shift(s|Segm($1+1),1));
A1:(Partial_Sums s).0 = s.0 by SERIES_1:def 1;
Shift(s|Segm(0+1),1) = <*s.0*> by SH4; then
A2:P[0] by A1,RVSUM_1:73;
A3:for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
A5: (Partial_Sums s).(k+1) = (Partial_Sums s).k + s.(k+1) by SERIES_1:def 1;
Shift(s|Segm(k+1+1),1) = Shift(s|Segm(k+1),1)^<*s.(k+1)*> by SH4;
hence P[k+1] by A4,A5,RVSUM_1:74;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem SH6:
for X being non empty set, s1,s2 being sequence of X, n being Nat
st s1,s2 are_fiberwise_equipotent holds
ex m being Nat, fs2 being Subset of Shift(s2|Segm m,1) st
Shift(s1|Segm(n+1),1),fs2 are_fiberwise_equipotent
proof
let X be non empty set;
let s1,s2 be sequence of X;
let n be Nat;
assume A1: s1,s2 are_fiberwise_equipotent;
A4:dom s1 = NAT & dom s2 = NAT by FUNCT_2:def 1; then
consider P being Permutation of dom s1 such that
A2: s1 = s2*P by A1,CLASSES1:80;
deffunc F(set) = P.$1 + 1;
defpred P2[set] means $1 is Nat;
{F(i) where i is Nat: i <= n & P2[i]} is finite from FINSEQ_1:sch 6; then
reconsider D = {F(i) where i is Nat: i<=n & P2[i]} as finite set;
now let x be object;
assume x in D; then
consider i be Nat such that
A3: x = F(i) & i<=n & P2[i];
thus x is natural by A3;
end; then
reconsider D as finite natural-membered set by MEMBERED:def 6;
P.0+1 in {F(i) where i is Nat: i<=n & P2[i]}; then
reconsider D as non empty finite natural-membered set;
reconsider m = max D as Nat by TARSKI:1;
take m;
set fs2 = {[j+1,s2.j] where j is Nat: j+1 in D};
now let z be object;
assume z in fs2; then
consider j be Nat such that
A4: z = [j+1,s2.j] & j+1 in D;
1 <= j+1 & j+1 <= m by A4,NAT_1:11,XXREAL_2:def 8; then
j+1 in Seg m by FINSEQ_1:1; then
A6: j+1 in dom(Shift(s2|Segm m,1)) by SH1; then
Shift(s2|Segm m,1).(j+1) = s2.j by SH3;
hence z in Shift(s2|Segm m,1) by A4,A6,FUNCT_1:def 2;
end; then
fs2 c= Shift(s2|Segm m,1); then
reconsider fs2 as Subset of Shift(s2|Segm m,1);
take fs2;
defpred P2[object,object] means ex i be Nat st $1=i+1 & $2 = P.i + 1;
P1:for x,y1,y2 be object st x in Seg(n+1) & P2[x,y1] & P2[x,y2] holds y1=y2;
P2:for x being object st x in Seg(n+1) holds ex y being object st P2[x,y]
proof
let x be object;
assume A7: x in Seg(n+1); then
reconsider x as Nat;
1 <= x & x <= n+1 by A7,FINSEQ_1:1; then
reconsider i = x-1 as Element of NAT by NAT_1:21;
A8: x = i+1;
ex y being object st P2[x,y]
proof
take y = P.i+1;
thus thesis by A8;
end;
hence thesis;
end;
now let x be object;
assume x in dom fs2; then
[x,fs2.x] in fs2 by FUNCT_1:def 2; then
consider j be Nat such that
X2: [x,fs2.x] = [j+1,s2.j] & j+1 in D;
x = j+1 & fs2.x = s2.j by X2,XTUPLE_0:1;
hence x in {i+1 where i is Nat: i+1 in D} by X2;
end; then
X3:dom fs2 c= {i+1 where i is Nat: i+1 in D};
now let x be object;
assume x in {i+1 where i is Nat: i+1 in D}; then
consider i be Nat such that
X4: x = i+1 & i+1 in D;
[x,s2.i] in fs2 by X4;
hence x in dom fs2 by XTUPLE_0:def 12;
end; then
{i+1 where i is Nat: i+1 in D} c= dom fs2; then
X5:dom fs2 = {i+1 where i is Nat: i+1 in D} by X3,XBOOLE_0:def 10;
consider P2 be Function such that
A9: dom P2 = Seg(n+1)
& for x be object st x in Seg(n+1) holds P2[x,P2.x]
from FUNCT_1:sch 2(P1,P2);
A10:dom P2 = dom(Shift(s1|Segm(n+1),1)) by A9,SH1;
now let y be object;
assume y in rng P2; then
consider x be object such that
B1: x in dom P2 & y = P2.x by FUNCT_1:def 3;
consider i be Nat such that
B2: x = i+1 & P2.x = P.i+1 by B1,A9;
B5: i <= n by B2,B1,A9,FINSEQ_1:1,XREAL_1:6;
y in D by B5,B1,B2;
hence y in dom fs2 by X5,B1,B2;
end; then
B6:rng P2 c= dom fs2;
now let y be object;
assume y in dom fs2; then
consider i be Nat such that
C1: y = i+1 & i+1 in D by X5;
consider j be Nat such that
C2: i+1 = P.j+1 & j <= n & j is Nat by C1;
C3: 1 <= j+1 & j+1 <= n+1 by C2,NAT_1:11,XREAL_1:6; then
ex k being Nat st j+1 = k+1 & P2.(j+1) = P.k + 1 by A9,FINSEQ_1:1;
hence y in rng P2 by C1,C2,C3,A9,FUNCT_1:3,FINSEQ_1:1;
end; then
dom fs2 c= rng P2; then
A11:rng P2 = dom fs2 by B6,XBOOLE_0:def 10;
now let x1,x2 be object;
assume D1: x1 in dom P2 & x2 in dom P2 & P2.x1 = P2.x2; then
consider i1 be Nat such that
D3: x1 = i1+1 & P2.x1 = P.i1+1 by A9;
consider i2 be Nat such that
D4: x2 = i2+1 & P2.x2 = P.i2+1 by D1,A9;
dom P = NAT by A4,FUNCT_2:def 1; then
i1 in dom P & i2 in dom P by ORDINAL1:def 12;
hence x1 = x2 by D1,D3,D4,FUNCT_1:def 4;
end; then
A12:P2 is one-to-one by FUNCT_1:def 4;
E0:dom(fs2*P2) = dom P2 by B6,RELAT_1:27; then
E1:dom(fs2*P2) = dom Shift(s1|Segm(n+1),1) by A9,SH1;
for x be object st x in dom Shift(s1|Segm(n+1),1)
holds Shift(s1|Segm(n+1),1).x = (fs2*P2).x
proof
let x be object;
assume E4: x in dom Shift(s1|Segm(n+1),1); then
E2: x in Seg(n+1) by SH1;
reconsider i=x as Nat by E4;
1 <= i & i <= n+1 by E2,FINSEQ_1:1; then
reconsider j=i-1 as Element of NAT by NAT_1:21;
i = j+1; then
E11:Shift(s1|Segm(n+1),1).x = (s2*P).j by A2,E4,SH3;
j in NAT; then
j in dom P by A4,FUNCT_2:def 1; then
E12:(s2*P).j = s2.(P.j) by FUNCT_1:13;
consider k be Nat such that
E6: i = k+1 & P2.i = P.k+1 by E2,A9;
P2.x in dom fs2 by A11,E4,E1,E0,FUNCT_1:3; then
[P2.x,fs2.(P2.x)] in fs2 by FUNCT_1:def 2; then
consider l be Nat such that
E7: [P2.x,fs2.(P2.x)] = [l+1,s2.l] & l+1 in D;
P2.i = l+1 & fs2.(P2.i) = s2.l by E7,XTUPLE_0:1;
hence Shift(s1|Segm(n+1),1).x = (fs2*P2).x by E11,E12,E6,E4,E1,FUNCT_1:12;
end;
hence Shift(s1|Segm(n+1),1),fs2 are_fiberwise_equipotent
by A10,A11,A12,E0,FUNCT_1:def 11,CLASSES1:77;
end;
theorem SH7:
for X being non empty set, fs being FinSequence of X,
fss being Subset of fs
holds Seq fss,fss are_fiberwise_equipotent
proof
let X be non empty set, fs be FinSequence of X, fss be Subset of fs;
dom fss c= dom fs by RELAT_1:11; then
A0:dom fss c= Seg len fs by FINSEQ_1:def 3; then
A1:fss is FinSubsequence by FINSEQ_1:def 12; then
A2:Seq fss = fss*Sgm(dom fss) by FINSEQ_1:def 15;
A3:rng Sgm(dom fss) = dom fss by A1,FINSEQ_1:50; then
A4:dom Sgm(dom fss) = dom Seq fss by A2,RELAT_1:27;
a0: dom fss is included_in_Seg by A0,FINSEQ_1:def 13;
now let x1,x2 be object;
assume A5: x1 in dom Sgm(dom fss) & x2 in dom Sgm(dom fss)
& Sgm(dom fss).x1 = Sgm(dom fss).x2;
reconsider i1 = x1, i2 = x2 as Nat by A5;
reconsider k1 = Sgm(dom fss).i1, k2 = Sgm(dom fss).i2 as Nat;
A6: 1 <= i1 & 1<= i2 & i1 <= len Sgm(dom fss) & i2 <=len Sgm(dom fss)
by A5,FINSEQ_3:25;
now assume i1 <> i2; then
i1 < i2 or i1 > i2 by XXREAL_0:1;
hence contradiction by A5,A6,a0,FINSEQ_1:def 14;
end;
hence x1 = x2;
end;
hence thesis by A2,A3,A4,CLASSES1:77,FUNCT_1:def 4;
end;
theorem SH8:
for s1,s2 being Real_Sequence, n being Nat
st s1,s2 are_fiberwise_equipotent & s1 is nonnegative
ex m being Nat st (Partial_Sums s1).n <= (Partial_Sums s2).m
proof
let s1,s2 be Real_Sequence;
let n be Nat;
assume that
A1: s1,s2 are_fiberwise_equipotent and
A2: s1 is nonnegative;
B1:s2 is nonnegative by A1,A2,TMP6;
consider m being Nat, F2 be Subset of Shift(s2|Segm m,1) such that
A3: Shift(s1|Segm(n+1),1),F2 are_fiberwise_equipotent by A1,SH6;
take m;
reconsider FS1 = Shift(s1|Segm(n+1),1),
FS2 = Shift(s2|Segm m,1) as FinSequence of REAL by SH2;
reconsider F2 as Subset of FS2;
Seq F2,F2 are_fiberwise_equipotent by SH7; then
A4:Sum FS1 = Sum(Seq F2) by A3,CLASSES1:76,RFINSEQ:9;
now let i be Element of NAT;
assume A6: i in dom FS2; then
reconsider i1 = i-1 as Element of NAT by NAT_1:21,FINSEQ_3:25;
i1+1 = i; then
FS2.i = s2.i1 by A6,SH3;
hence 0 <= FS2.i by A1,A2,TMP6,RINFSUP1:def 3;
end; then
Sum(Seq F2) <= Sum FS2 by GLIB_003:2; then
A7:(Partial_Sums s1).n <= Sum FS2 by A4,SH5;
Shift(s2|Segm(m+1),1) = Shift(s2|Segm m,1) ^ <*s2.m*> by SH4; then
Sum(Shift(s2|Segm(m+1),1)) = Sum FS2 + s2.m by RVSUM_1:74; then
A8:(Partial_Sums s2).m = Sum FS2 + s2.m by SH5;
(Partial_Sums s2).m >= Sum FS2 by A8,XREAL_1:31,B1;
hence (Partial_Sums s1).n <= (Partial_Sums s2).m by A7,XXREAL_0:2;
end;
theorem
for s1,s2 being Real_Sequence st
s1,s2 are_fiberwise_equipotent & s1 is nonnegative & s1 is summable
holds s2 is summable & Sum s1 = Sum s2
proof
let s1,s2 be Real_Sequence;
assume that
A1: s1,s2 are_fiberwise_equipotent & s1 is nonnegative and
A2: s1 is summable;
Partial_Sums s1 is bounded_above by A2,A1,SERIES_1:17; then
consider r be Real such that
A5: for n being Nat holds (Partial_Sums s1).n < r by SEQ_2:def 3;
A3:for n being Nat holds 0<=s2.n by A1,TMP6,RINFSUP1:def 3;
B3:now let n be Nat;
consider m be Nat such that
A6: (Partial_Sums s2).n <= (Partial_Sums s1).m by A1,TMP6,SH8;
thus (Partial_Sums s2).n < r by A5,A6,XXREAL_0:2;
end; then
B2:Partial_Sums s2 is bounded_above by SEQ_2:def 3;
hence A7: s2 is summable by A3,SERIES_1:17;
A8:Partial_Sums s1 is bounded_above
& Partial_Sums s2 is bounded_above by A2,B3,SEQ_2:def 3,A1,SERIES_1:17;
now let n be Nat;
consider m be Nat such that
A11: (Partial_Sums s1).n <= (Partial_Sums s2).m by A1,SH8;
(Partial_Sums s2).m <= lim Partial_Sums s2
by A3,B2,SERIES_1:16,SEQ_4:37;
hence (Partial_Sums s1).n <= lim Partial_Sums s2 by A11,XXREAL_0:2;
end; then
lim Partial_Sums s1 <= lim Partial_Sums s2
by A2,SERIES_1:def 2,PREPOWER:2; then
Sum s1 <= lim Partial_Sums s2 by SERIES_1:def 3; then
A12:Sum s1 <= Sum s2 by SERIES_1:def 3;
now let m be Nat;
consider n be Nat such that
A13: (Partial_Sums s2).m <= (Partial_Sums s1).n by A1,TMP6,SH8;
(Partial_Sums s1).n <= lim Partial_Sums s1
by A8,A1,SERIES_1:16,SEQ_4:37;
hence (Partial_Sums s2).m <= lim Partial_Sums s1 by A13,XXREAL_0:2;
end; then
lim Partial_Sums s2 <= lim Partial_Sums s1
by A7,SERIES_1:def 2,PREPOWER:2; then
Sum s2 <= lim Partial_Sums s1 by SERIES_1:def 3; then
Sum s2 <= Sum s1 by SERIES_1:def 3;
hence Sum s1 = Sum s2 by A12,XXREAL_0:1;
end;
begin :: Basic relations between double sequence and matrix
theorem
for D being non empty set, Rseq being Function of [:NAT,NAT:],D,
n,m being Nat holds
ex M be Matrix of n+1,m+1,D st
for i,j being Nat st i <= n & j <= m holds Rseq.(i,j) = M*(i+1,j+1)
proof
let D be non empty set, Rseq be Function of [:NAT,NAT:],D;
let n,m be Nat;
defpred P[Nat,Nat,object] means
ex i1,j1 being Nat st i1=$1-1 & j1=$2-1 & $3=Rseq.(i1,j1);
A1:now let i,j be Nat;
assume [i,j] in [:Seg(n+1),Seg(m+1):]; then
[i,j]`1 in Seg(n+1) & [i,j]`2 in Seg(m+1) by MCART_1:10; then
1 <= i & 1 <= j by FINSEQ_1:1; then
reconsider i1 = i-1, j1 = j-1 as Element of NAT by NAT_1:21;
reconsider i1, j1 as Nat;
dom Rseq = [:NAT,NAT:] by FUNCT_2:def 1; then
[i1,j1] in dom Rseq by ZFMISC_1:def 2; then
reconsider x = Rseq.(i1,j1) as Element of D by FUNCT_2:5;
take x;
thus P[i,j,x];
end;
consider M be Matrix of n+1,m+1,D such that
A2: for i,j being Nat st [i,j] in Indices M holds P[i,j,M*(i,j)]
from MATRIX_0:sch 2(A1);
take M;
hereby let i,j be Nat;
assume i <= n & j <= m; then
i < n+1 & j < m+1 by NAT_1:13; then
i+1 in Seg(n+1) & j+1 in Seg(m+1) by FINSEQ_3:11; then
[i+1,j+1] in [:Seg(n+1),Seg(m+1):] by ZFMISC_1:def 2; then
[i+1,j+1] in Indices M by MATRIX_0:23; then
consider i1,j1 be Nat such that
A4: i1=i+1-1 & j1=j+1-1 & M*(i+1,j+1) = Rseq.(i1,j1) by A2;
thus Rseq.(i,j) = M*(i+1,j+1) by A4;
end;
end;
theorem
for n,m being Nat, Rseq being Function of [:NAT,NAT:],REAL,
M being Matrix of n+1,m+1,REAL st
( for i,j being Nat st i<=n & j<=m holds Rseq.(i,j) = M*(i+1,j+1) )
holds (Partial_Sums Rseq).(n,m) = SumAll M
proof
let n,m be Nat;
let Rseq be Function of [:NAT,NAT:],REAL;
let M be Matrix of n+1,m+1,REAL;
assume
A1: for i,j being Nat st i<=n & j<=m holds Rseq.(i,j) = M*(i+1,j+1);
A2:len M = n+1 by MATRIX_0:25; then
A3:width M = m+1 by MATRIX_0:20;
X1:for i being Nat st i<=n holds
(Partial_Sums_in_cod2 Rseq).(i,m) = (LineSum M).(i+1)
proof
let i be Nat;
assume B0: i<=n; then
1 <= i+1 & i+1 <= n+1 by NAT_1:11,XREAL_1:6; then
B01:i+1 in Seg(n+1) by FINSEQ_1:1;
defpred P1[Nat] means
$1+1 <= width M implies
(Partial_Sums_in_cod2 Rseq).(i,$1) = Sum (Line(M,i+1)|($1+1));
now assume 0+1 <= width M;
B2: (Partial_Sums_in_cod2 Rseq).(i,0) = Rseq.(i,0) by DefCS;
len Line(M,i+1) = m+1 by A3,MATRIX_0:def 7; then
B5: len (Line(M,i+1)|1) = 1 by NAT_1:11,FINSEQ_1:59;
1 <= width M by A3,NAT_1:11; then
B4: 1 in Seg width M by FINSEQ_1:1;
(Line(M,i+1)|1).1 = Line(M,i+1).1 by FINSEQ_3:112; then
Line(M,i+1)|(0+1) = <* M*(i+1,1) *>
by B5,B4,MATRIX_0:def 7,FINSEQ_1:40; then
B6: Sum(Line(M,i+1)|(0+1)) = M*(i+1,1) by RVSUM_1:73;
thus (Partial_Sums_in_cod2 Rseq).(i,0) = Sum(Line(M,i+1)|(0+1))
by A1,B0,B2,B6;
end; then
P0: P1[0];
P1: for k being Nat st P1[k] holds P1[k+1]
proof
let k be Nat;
assume C1: P1[k];
now assume C2: k+1+1 <= width M; then
C3: k+1 <= k+1+1 & k+1+1 <= len Line(M,i+1) by MATRIX_0:def 7,NAT_1:11; then
C5: len (Line(M,i+1)|(k+1+1)) = k+1+1 by FINSEQ_1:59; then
Line(M,i+1)|(k+1+1)
= (Line(M,i+1)|(k+1+1))|(k+1)
^ <* Line(M,i+1)|(k+1+1)/.(len (Line(M,i+1)|(k+1+1))) *>
by FINSEQ_5:21; then
C6: Line(M,i+1)|(k+1+1)
= Line(M,i+1)|(k+1) ^ <* Line(M,i+1)|(k+2)/.(k+2) *>
by C5,FINSEQ_1:82,NAT_1:11;
1 <= k+1+1 by NAT_1:11; then
C7: k+2 in Seg width M by C2,FINSEQ_1:1;
C8: k+1 <= m by A3,C2,XREAL_1:6;
k+2 in Seg len(Line(M,i+1)|(k+2)) by C5,FINSEQ_1:4; then
k+2 in dom (Line(M,i+1)|(k+2)) by FINSEQ_1:def 3; then
Line(M,i+1)|(k+2)/.(k+2) = (Line(M,i+1)|(k+2)).(k+2)
by PARTFUN1:def 6; then
Line(M,i+1)|(k+2)/.(k+2) = Line(M,i+1).(k+2) by FINSEQ_3:112; then
Line(M,i+1)|(k+2)/.(k+2) = M*(i+1,k+2) by C7,MATRIX_0:def 7; then
Sum(Line(M,i+1)|(k+1+1)) = Sum(Line(M,i+1)|(k+1)) + M*(i+1,k+2)
by C6,RVSUM_1:74; then
Sum(Line(M,i+1)|(k+1+1))
= (Partial_Sums_in_cod2 Rseq).(i,k) + Rseq.(i,k+1)
by C3,B0,A1,C8,C1,C2,XXREAL_0:2;
hence (Partial_Sums_in_cod2 Rseq).(i,k+1) = Sum(Line(M,i+1)|(k+1+1))
by DefCS;
end;
hence P1[k+1];
end;
C9: m+1 = len Line(M,i+1) by A3,MATRIX_0:def 7;
for k be Nat holds P1[k] from NAT_1:sch 2(P0,P1); then
(Partial_Sums_in_cod2 Rseq).(i,m) = Sum(Line(M,i+1)|(m+1)) by A3; then
(Partial_Sums_in_cod2 Rseq).(i,m) = Sum Line(M,i+1) by C9,FINSEQ_1:58;
hence (Partial_Sums_in_cod2 Rseq).(i,m) = (LineSum M).(i+1)
by B01,A2,MATRPROB:20;
end;
defpred P2[Nat] means
$1 <= n implies
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).($1,m)
= Sum((LineSum M)|($1+1));
now assume 0 <= n;
0+1 <= n+1 by XREAL_1:6; then
0+1 <= len (LineSum M) by A2,MATRPROB:20; then
len((LineSum M)|(0+1)) = 1 by FINSEQ_1:59; then
D2: ((LineSum M)|(0+1)) = <* ((LineSum M)|(0+1)).1 *> by FINSEQ_1:40;
(Partial_Sums_in_cod2 Rseq).(0,m) = (LineSum M).(0+1) by X1; then
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(0,m)
= (LineSum M).(0+1) by DefRS
.= Sum <* (LineSum M).(0+1) *> by RVSUM_1:73;
hence (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)).(0,m)
= Sum ((LineSum M)|(0+1)) by D2,FINSEQ_3:112;
end; then
P2:P2[0];
P3:for k being Nat st P2[k] holds P2[k+1]
proof
let k be Nat;
assume E1: P2[k];
now assume E2: k+1 <= n; then
k+1<=k+1+1 & k+1+1 <= n+1 by NAT_1:11,XREAL_1:6; then
k+1+1 <= len(LineSum M) by A2,MATRPROB:20; then
E3: len((LineSum M)|(k+1+1)) = k+1+1 by FINSEQ_1:59; then
E5: (LineSum M)|(k+1+1)
= ((LineSum M)|(k+1+1))|(k+1)
^ <* ((LineSum M)|(k+1+1))/.(len ((LineSum M)|(k+1+1))) *>
by FINSEQ_5:21
.= (LineSum M)|(k+1) ^ <* ((LineSum M)|(k+1+1))/.(k+1+1) *>
by E3,NAT_1:11,FINSEQ_1:82;
E7: k<=k+1 by NAT_1:11;
k+2 in Seg len((LineSum M)|(k+2)) by E3,FINSEQ_1:4; then
k+2 in dom ((LineSum M)|(k+2)) by FINSEQ_1:def 3; then
((LineSum M)|(k+2))/.(k+2) = ((LineSum M)|(k+2)).(k+2) by PARTFUN1:def 6
.= (LineSum M).(k+2) by FINSEQ_3:112; then
Sum((LineSum M)|(k+1+1))
= Sum((LineSum M)|(k+1)) + (LineSum M).(k+1+1) by E5,RVSUM_1:74
.= (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(k,m)
+ (Partial_Sums_in_cod2 Rseq).(k+1,m) by E1,E7,E2,X1,XXREAL_0:2;
hence (Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(k+1,m)
= Sum((LineSum M)|(k+1+1)) by DefRS;
end;
hence P2[k+1];
end;
for k being Nat holds P2[k] from NAT_1:sch 2(P2,P3); then
X2:(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n,m)
= Sum((LineSum M)|(n+1));
len (LineSum M) = n+1 by A2,MATRPROB:20; then
(LineSum M)|(n+1) = LineSum M by FINSEQ_1:58; then
(Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq)).(n,m)
= SumAll M by X2,MATRPROB:def 3;
hence (Partial_Sums Rseq).(n,m) = SumAll M by th103;
end;