:: Double Series and Sums
:: by Noboru Endou
::
:: Received March 31, 2014
:: Copyright (c) 2014-2016 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;
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,
FUNCT_4;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
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
:: DBLSEQ_2:def 1
for i, j being Nat holds f.(i,j) >= 0;
end;
theorem :: DBLSEQ_2:1
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);
theorem :: DBLSEQ_2:2
Rseq is non-decreasing & Rseq is convergent_in_cod1 implies
lim_in_cod1 Rseq is non-decreasing;
theorem :: DBLSEQ_2:3
Rseq is non-decreasing & Rseq is convergent_in_cod2 implies
lim_in_cod2 Rseq is non-decreasing;
theorem :: DBLSEQ_2:4
Rseq is non-decreasing & Rseq is P-convergent implies
(for n,m being Nat holds Rseq.(n,m) <= P-lim Rseq);
theorem :: DBLSEQ_2:5
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));
theorem :: DBLSEQ_2:6
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);
theorem :: DBLSEQ_2:7
for C,D,E being set, f being Function of [:C,D:],E holds f = ~~f;
scheme :: DBLSEQ_2:sch 1
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);
scheme :: DBLSEQ_2:sch 2
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);
scheme :: DBLSEQ_2:sch 3
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);
scheme :: DBLSEQ_2:sch 4
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);
definition
let Rseq be Function of [:NAT,NAT:],REAL;
func Partial_Sums_in_cod2(Rseq) -> Function of [:NAT,NAT:],REAL means
:: DBLSEQ_2:def 2
for n,m being Nat holds
it.(n,0) = Rseq.(n,0) & it.(n,m+1) = it.(n,m) + Rseq.(n,m+1);
end;
definition
let Rseq be Function of [:NAT,NAT:],REAL;
func Partial_Sums_in_cod1(Rseq) -> Function of [:NAT,NAT:],REAL means
:: DBLSEQ_2:def 3
for n,m being Nat holds
it.(0,m) = Rseq.(0,m) & it.(n+1,m) = it.(n,m) + Rseq.(n+1,m);
end;
theorem :: DBLSEQ_2:8
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);
theorem :: DBLSEQ_2:9
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);
theorem :: DBLSEQ_2:10
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;
definition
let Rseq be Function of [:NAT,NAT:],REAL;
func Partial_Sums(Rseq) -> Function of [:NAT,NAT:],REAL equals
:: DBLSEQ_2:def 4
Partial_Sums_in_cod2( Partial_Sums_in_cod1 Rseq );
end;
theorem :: DBLSEQ_2:11
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);
theorem :: DBLSEQ_2:12
Partial_Sums Rseq = Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq);
theorem :: DBLSEQ_2:13
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);
theorem :: DBLSEQ_2:14
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);
theorem :: DBLSEQ_2:15
Partial_Sums Rseq is P-convergent implies
Rseq is P-convergent & P-lim Rseq = 0;
theorem :: DBLSEQ_2:16
Partial_Sums(Rseq1 + Rseq2) = Partial_Sums(Rseq1) + Partial_Sums(Rseq2);
theorem :: DBLSEQ_2:17
Partial_Sums Rseq1 is P-convergent & Partial_Sums Rseq2 is P-convergent
implies Partial_Sums(Rseq1+Rseq2) is P-convergent;
theorem :: DBLSEQ_2:18
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;
theorem :: DBLSEQ_2:19
ProjMap1(Partial_Sums Rseq,0) = ProjMap1(Partial_Sums_in_cod2 Rseq,0)
& ProjMap2(Partial_Sums Rseq,0) = ProjMap2(Partial_Sums_in_cod1 Rseq,0);
theorem :: DBLSEQ_2:20
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);
theorem :: DBLSEQ_2:21
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);
theorem :: DBLSEQ_2:22
Partial_Sums Rseq is convergent_in_cod1 iff
Partial_Sums_in_cod1 Rseq is convergent_in_cod1;
theorem :: DBLSEQ_2:23
Partial_Sums Rseq is convergent_in_cod2 iff
Partial_Sums_in_cod2 Rseq is convergent_in_cod2;
theorem :: DBLSEQ_2:24
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);
theorem :: DBLSEQ_2:25
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);
theorem :: DBLSEQ_2:26
Partial_Sums Rseq is convergent_in_cod1 implies
lim_in_cod1(Partial_Sums Rseq)
= Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 Rseq));
theorem :: DBLSEQ_2:27
Partial_Sums Rseq is convergent_in_cod2 implies
lim_in_cod2(Partial_Sums Rseq)
= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 Rseq));
begin :: Double series of non-negative double sequence
theorem :: DBLSEQ_2:28
Rseq is nonnegative-yielding implies
Partial_Sums_in_cod2 Rseq is nonnegative-yielding &
Partial_Sums_in_cod1 Rseq is nonnegative-yielding;
theorem :: DBLSEQ_2:29
Rseq is nonnegative-yielding implies
Partial_Sums Rseq is non-decreasing;
theorem :: DBLSEQ_2:30
Rseq is nonnegative-yielding implies
(Partial_Sums Rseq is P-convergent
iff Partial_Sums Rseq is bounded_below bounded_above);
theorem :: DBLSEQ_2:31
(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);
theorem :: DBLSEQ_2:32
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);
theorem :: DBLSEQ_2:33
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;
theorem :: DBLSEQ_2:34
for rseq being Real_Sequence, m being Nat st
rseq is nonnegative holds
rseq.m <= (Partial_Sums rseq).m;
theorem :: DBLSEQ_2:35
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));
theorem :: DBLSEQ_2:36
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) )
;
theorem :: DBLSEQ_2:37
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) );
theorem :: DBLSEQ_2:38
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));
theorem :: DBLSEQ_2:39
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;
theorem :: DBLSEQ_2:40
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;
theorem :: DBLSEQ_2:41
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;
theorem :: DBLSEQ_2:42
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;
theorem :: DBLSEQ_2:43
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));
begin :: Summability for rearrangements of non-negative real sequence
theorem :: DBLSEQ_2:44
for s1,s2 be Real_Sequence
st s1 is nonnegative & s1,s2 are_fiberwise_equipotent
holds s2 is nonnegative;
theorem :: DBLSEQ_2:45
for X being non empty set, s being sequence of X, n being Nat
holds dom(Shift(s|(Segm n),1)) = Seg n;
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;
end;
theorem :: DBLSEQ_2:46
for X being non empty set, s being sequence of X, n being Nat
holds Shift(s|(Segm n),1) is FinSequence of X;
theorem :: DBLSEQ_2:47
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;
theorem :: DBLSEQ_2:48
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*>;
theorem :: DBLSEQ_2:49
for s being Real_Sequence, n being Nat holds
(Partial_Sums s).n = Sum(Shift(s|Segm(n+1),1));
theorem :: DBLSEQ_2:50
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;
theorem :: DBLSEQ_2:51
for X being non empty set, fs being FinSequence of X,
fss being Subset of fs
holds Seq fss,fss are_fiberwise_equipotent;
theorem :: DBLSEQ_2:52
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;
theorem :: DBLSEQ_2:53
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;
begin :: Basic relations between double sequence and matrix
theorem :: DBLSEQ_2:54
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);
theorem :: DBLSEQ_2:55
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;