:: Double Sequences and Limits :: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama :: :: Received August 31, 2013 :: Copyright (c) 2013-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_3, ARYTM_1, XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, VALUED_0, ORDINAL2, SEQ_2, XREAL_0, COMPLEX1, XCMPLX_0, XXREAL_2, FINSET_1, MEMBERED, MESFUNC9, BHSP_3, SEQ_1, VALUED_1, DBLSEQ_1, FUNCOP_1, BINOP_1, BINOP_2, REAL_1; notations ZFMISC_1, SUBSET_1, ORDINAL1, XXREAL_2, RELAT_1, PARTFUN1, RELSET_1, FUNCT_1, FUNCT_2, NUMBERS, BINOP_1, XCMPLX_0, TARSKI, XBOOLE_0, FUNCOP_1, FUNCT_3, FINSEQOP, MEMBERED, COMPLEX1, XXREAL_0, XREAL_0, SEQ_1, NAT_1, MESFUNC9, VALUED_1, SEQ_2, FINSET_1, BINOP_2; constructors TOPMETR, NAT_D, MESFUNC9, SEQ_2, COMSEQ_2, SEQ_4, REAL_1, FINSEQOP, FUNCT_3, BINOP_2; registrations ORDINAL1, XXREAL_0, XREAL_0, XBOOLE_0, NUMBERS, XCMPLX_0, FINSET_1, SUBSET_1, MEMBERED, VALUED_0, XXREAL_2, RELSET_1, MEASURE6, SEQ_4, FUNCT_1, FUNCT_2, VALUED_1, BINOP_2, NAT_1, SEQ_2, SEQ_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin reserve Rseq, Rseq1, Rseq2 for Function of [:NAT,NAT:],REAL; reserve rseq1,rseq2 for convergent Real_Sequence; reserve n,m,N,M for Nat; reserve e,r for Real; :: Convergence in the Pringsheim sense definition let Rseq; attr Rseq is P-convergent means :: DBLSEQ_1:def 1 ex p be Real st for e be Real st 0=N & m>=N holds |.Rseq.(n,m) - p.| < e; end; definition let Rseq; assume Rseq is P-convergent; func P-lim Rseq -> Real means :: DBLSEQ_1:def 2 for e be Real st 0=N & m>=N holds |. Rseq.(n,m) - it .| < e; end; definition let Rseq; attr Rseq is convergent_in_cod1 means :: DBLSEQ_1:def 3 for m be Element of NAT holds ProjMap2(Rseq,m) is convergent; attr Rseq is convergent_in_cod2 means :: DBLSEQ_1:def 4 for n be Element of NAT holds ProjMap1(Rseq,n) is convergent; end; definition let Rseq; func lim_in_cod1 Rseq -> Function of NAT,REAL means :: DBLSEQ_1:def 5 for m be Element of NAT holds it.m = lim ProjMap2(Rseq,m); end; definition let Rseq; func lim_in_cod2 Rseq -> Function of NAT,REAL means :: DBLSEQ_1:def 6 for n be Element of NAT holds it.n = lim ProjMap1(Rseq,n); end; definition let Rseq; assume lim_in_cod1 Rseq is convergent; func cod1_major_iterated_lim Rseq -> Real means :: DBLSEQ_1:def 7 for e be Real st 0=M holds |.(lim_in_cod1 Rseq).m - it.| < e; end; definition let Rseq; assume lim_in_cod2 Rseq is convergent; func cod2_major_iterated_lim Rseq -> Real means :: DBLSEQ_1:def 8 for e be Real st 0=N holds |.(lim_in_cod2 Rseq).n - it.| < e; end; definition let Rseq be Function of [:NAT,NAT:],REAL; attr Rseq is uniformly_convergent_in_cod1 means :: DBLSEQ_1:def 9 Rseq is convergent_in_cod1 & for e be Real st e>0 ex M be Nat st for m be Nat st m>=M holds for n be Nat holds |. Rseq.(n,m) - (lim_in_cod1 Rseq).n .| < e; end; definition let Rseq be Function of [:NAT,NAT:],REAL; attr Rseq is uniformly_convergent_in_cod2 means :: DBLSEQ_1:def 10 Rseq is convergent_in_cod2 & for e be Real st e>0 ex N be Nat st for n be Nat st n>=N holds for m be Nat holds |. Rseq.(n,m) - (lim_in_cod2 Rseq).m .| < e; end; definition let Rseq; attr Rseq is non-decreasing means :: DBLSEQ_1:def 11 for n1,m1,n2,m2 be Nat st n1>=n2 & m1>=m2 holds Rseq.(n1,m1) >= Rseq.(n2,m2); attr Rseq is non-increasing means :: DBLSEQ_1:def 12 for n1,m1,n2,m2 be Nat st n1>=n2 & m1>=m2 holds Rseq.(n1,m1) <= Rseq.(n2,m2); end; theorem :: DBLSEQ_1:1 for a,b,c be Real st a <= b & b <= c holds |.b.| <= |.a.| or |.b.| <= |.c.|; registration cluster non-decreasing P-convergent -> bounded_below bounded_above for Function of [:NAT,NAT:],REAL; end; registration cluster non-increasing P-convergent -> bounded_below bounded_above for Function of [:NAT,NAT:],REAL; end; registration let r be Element of REAL; cluster [:NAT,NAT:] --> r -> P-convergent convergent_in_cod1 convergent_in_cod2 for Function of [:NAT,NAT:],REAL; end; theorem :: DBLSEQ_1:2 for r be Element of REAL holds P-lim ([:NAT,NAT:] --> r) = r; registration cluster P-convergent convergent_in_cod1 convergent_in_cod2 for Function of [:NAT,NAT:],REAL; end; reserve Pseq for P-convergent Function of [:NAT,NAT:],REAL; registration let Pseq2 be P-convergent convergent_in_cod2 Function of [:NAT,NAT:],REAL; cluster lim_in_cod2 Pseq2 -> convergent; end; theorem :: DBLSEQ_1:3 Rseq is P-convergent convergent_in_cod2 implies P-lim Rseq = cod2_major_iterated_lim Rseq; registration let Pseq1 be P-convergent convergent_in_cod1 Function of [:NAT,NAT:],REAL; cluster lim_in_cod1 Pseq1 -> convergent; end; theorem :: DBLSEQ_1:4 Rseq is P-convergent convergent_in_cod1 implies P-lim Rseq = cod1_major_iterated_lim Rseq; registration cluster non-decreasing bounded_above -> P-convergent convergent_in_cod1 convergent_in_cod2 for Function of [:NAT,NAT:],REAL; end; registration cluster non-increasing bounded_below -> P-convergent convergent_in_cod1 convergent_in_cod2 for Function of [:NAT,NAT:],REAL; end; theorem :: DBLSEQ_1:5 Rseq is uniformly_convergent_in_cod1 & lim_in_cod1 Rseq is convergent implies Rseq is P-convergent & P-lim Rseq = cod1_major_iterated_lim Rseq; theorem :: DBLSEQ_1:6 Rseq is uniformly_convergent_in_cod2 & lim_in_cod2 Rseq is convergent implies Rseq is P-convergent & P-lim Rseq = cod2_major_iterated_lim Rseq; definition let Rseq; attr Rseq is Cauchy means :: DBLSEQ_1:def 13 for e be Real st e>0 ex N be Nat st for n1,n2,m1,m2 be Nat st N<=n1 & n1<=n2 & N<=m1 & m1<=m2 holds |.Rseq.(n2,m2) - Rseq.(n1,m1).| < e; end; theorem :: DBLSEQ_1:7 Rseq is P-convergent iff Rseq is Cauchy; theorem :: DBLSEQ_1:8 for Rseq be Function of [:NAT,NAT:],REAL st Rseq is non-decreasing or Rseq is non-increasing holds Rseq is P-convergent iff Rseq is bounded_below bounded_above; definition let X,Y be non empty set; let H be BinOp of Y; let f,g be Function of X,Y; redefine func H*(f,g) -> Function of [:X,X:],Y; end; theorem :: DBLSEQ_1:9 multreal*(rseq1,rseq2) is convergent_in_cod1 convergent_in_cod2 & lim_in_cod1 (multreal*(rseq1,rseq2)) is convergent & cod1_major_iterated_lim (multreal*(rseq1,rseq2)) = lim rseq1 * lim rseq2 & lim_in_cod2 (multreal*(rseq1,rseq2)) is convergent & cod2_major_iterated_lim (multreal*(rseq1,rseq2)) = lim rseq1 * lim rseq2 & multreal*(rseq1,rseq2) is P-convergent & P-lim (multreal*(rseq1,rseq2)) = lim rseq1 * lim rseq2; theorem :: DBLSEQ_1:10 addreal*(rseq1,rseq2) is convergent_in_cod1 convergent_in_cod2 & lim_in_cod1 (addreal*(rseq1,rseq2)) is convergent & cod1_major_iterated_lim (addreal*(rseq1,rseq2)) = lim rseq1 + lim rseq2 & lim_in_cod2 (addreal*(rseq1,rseq2)) is convergent & cod2_major_iterated_lim (addreal*(rseq1,rseq2)) = lim rseq1 + lim rseq2 & addreal*(rseq1,rseq2) is P-convergent & P-lim (addreal*(rseq1,rseq2)) = lim rseq1 + lim rseq2; theorem :: DBLSEQ_1:11 Rseq1 is P-convergent & Rseq2 is P-convergent implies Rseq1+Rseq2 is P-convergent & P-lim(Rseq1+Rseq2) = P-lim Rseq1 + P-lim Rseq2; theorem :: DBLSEQ_1:12 Rseq1 is P-convergent & Rseq2 is P-convergent implies Rseq1-Rseq2 is P-convergent & P-lim(Rseq1-Rseq2) = P-lim Rseq1 - P-lim Rseq2; theorem :: DBLSEQ_1:13 for Rseq be Function of [:NAT,NAT:],REAL, r be Real st Rseq is P-convergent holds r(#)Rseq is P-convergent & P-lim (r(#)Rseq) = r * P-lim Rseq; theorem :: DBLSEQ_1:14 Rseq is P-convergent &(for n,m be Nat holds Rseq.(n,m) >= r) implies P-lim Rseq >= r; theorem :: DBLSEQ_1:15 Rseq1 is P-convergent & Rseq2 is P-convergent & (for n,m be Nat holds Rseq1.(n,m) <= Rseq2.(n,m)) implies P-lim Rseq1 <= P-lim Rseq2; theorem :: DBLSEQ_1:16 Rseq1 is P-convergent & Rseq2 is P-convergent & P-lim Rseq1 = P-lim Rseq2 & (for n,m be Nat holds Rseq1.(n,m) <= Rseq.(n,m) & Rseq.(n,m) <= Rseq2.(n,m) ) implies Rseq is P-convergent & P-lim Rseq = P-lim Rseq1; definition let X be non empty set, seq be Function of [:NAT,NAT:],X; mode subsequence of seq -> Function of [:NAT,NAT:],X means :: DBLSEQ_1:def 14 ex N,M be increasing sequence of NAT st for n,m be Nat holds it.(n,m) = seq.(N.n,M.m); end; registration let Pseq; cluster -> P-convergent for subsequence of Pseq; end; theorem :: DBLSEQ_1:17 for Psubseq be subsequence of Pseq holds P-lim Psubseq = P-lim Pseq; registration let Rseq be convergent_in_cod1 Function of [:NAT,NAT:],REAL; cluster -> convergent_in_cod1 for subsequence of Rseq; end; theorem :: DBLSEQ_1:18 for Rseq1 be subsequence of Rseq st Rseq is convergent_in_cod1 & lim_in_cod1 Rseq is convergent holds lim_in_cod1 Rseq1 is convergent & cod1_major_iterated_lim Rseq1 = cod1_major_iterated_lim Rseq; registration let Rseq be convergent_in_cod2 Function of [:NAT,NAT:],REAL; cluster -> convergent_in_cod2 for subsequence of Rseq; end; theorem :: DBLSEQ_1:19 for Rseq1 be subsequence of Rseq st Rseq is convergent_in_cod2 & lim_in_cod2 Rseq is convergent holds lim_in_cod2 Rseq1 is convergent & cod2_major_iterated_lim Rseq1 = cod2_major_iterated_lim Rseq;