:: Extended Real Valued Double Sequence and Its Convergence :: by Noboru Endou :: :: Received July 1, 2015 :: Copyright (c) 2015-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, NAT_1, ZFMISC_1, VALUED_0, ORDINAL2, SEQ_2, ORDINAL1, COMPLEX1, XCMPLX_0, XXREAL_2, MESFUNC9, DBLSEQ_1, FUNCOP_1, REAL_1, DBLSEQ_2, DBLSEQ_3, SUPINF_1, SUPINF_2, MESFUNC5, SERIES_1, PARTFUN1, CARD_3, RINFSUP1, QC_LANG1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, BINOP_1, XREAL_0, XXREAL_3, XCMPLX_0, COMPLEX1, PARTFUN1, FUNCT_1, XXREAL_0, RELSET_1, FUNCT_2, FUNCOP_1, NAT_1, XXREAL_2, SUPINF_1, VALUED_0, FUNCT_4, SUPINF_2, SEQ_2, EXTREAL1, MESFUNC1, MESFUNC5, RINFSUP2, MESFUNC9, DBLSEQ_1, DBLSEQ_2; constructors TOPMETR, NAT_D, MESFUNC9, SEQ_2, COMSEQ_2, DBLSEQ_1, MESFUNC5, SUPINF_1, EXTREAL1, MESFUNC1, RINFSUP2, DBLSEQ_2, FUNCT_4; registrations ORDINAL1, XXREAL_0, XREAL_0, XBOOLE_0, NUMBERS, XCMPLX_0, SUBSET_1, MEMBERED, VALUED_0, RELSET_1, FUNCT_2, NAT_1, RELAT_1, XXREAL_3, COMPLEX1, RINFSUP2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin registration let X be non empty set; cluster nonnegative nonpositive for Function of X,REAL; end; registration let X be non empty set; cluster without-infty without+infty nonnegative nonpositive for Function of X,ExtREAL; end; registration let X be non empty set; cluster nonnegative -> without-infty for Function of X,ExtREAL; cluster nonpositive -> without+infty for Function of X,ExtREAL; cluster without-infty for without+infty Function of X,ExtREAL; end; definition let X be non empty set, f be Function of X,ExtREAL; redefine func -f -> Function of X,ExtREAL; end; registration let X be non empty set, f be without-infty Function of X,ExtREAL; cluster -f -> without+infty; end; registration let X be non empty set, f be without+infty Function of X,ExtREAL; cluster -f -> without-infty; end; registration let X be non empty set, f be nonnegative Function of X,ExtREAL; cluster -f -> nonpositive; end; registration let X be non empty set, f be nonpositive Function of X,ExtREAL; cluster -f -> nonnegative; end; registration let A,B be non empty set; let f be without-infty Function of [:A,B:],ExtREAL; cluster ~f -> without-infty; end; registration let A,B be non empty set; let f be without+infty Function of [:A,B:],ExtREAL; cluster ~f -> without+infty; end; registration let A,B be non empty set; let f be nonnegative Function of [:A,B:],ExtREAL; cluster ~f -> nonnegative; end; registration let A,B be non empty set; let f be nonpositive Function of [:A,B:],ExtREAL; cluster ~f -> nonpositive; end; theorem :: DBLSEQ_3:1 for seq be ExtREAL_sequence holds Partial_Sums(-seq) = -(Partial_Sums seq); theorem :: DBLSEQ_3:2 for X be non empty set, f be PartFunc of X,ExtREAL holds -(-f) = f; theorem :: DBLSEQ_3:3 for X,Y be non empty set, f be Function of [:X,Y:], ExtREAL holds ~(-f) = -(~f); registration let seq be nonnegative ExtREAL_sequence; cluster Partial_Sums seq -> nonnegative; end; registration let seq be nonpositive ExtREAL_sequence; cluster Partial_Sums seq -> nonpositive; end; theorem :: DBLSEQ_3:4 for seq be nonnegative ExtREAL_sequence, m be Nat holds seq.m <= (Partial_Sums seq).m; theorem :: DBLSEQ_3:5 for seq be nonpositive ExtREAL_sequence, m be Nat holds seq.m >= (Partial_Sums seq).m; theorem :: DBLSEQ_3:6 for X be non empty set, f be without-infty without+infty Function of X,ExtREAL holds f is Function of X,REAL; definition let X be non empty set; let f1,f2 be without-infty Function of X,ExtREAL; redefine func f1+f2 -> without-infty Function of X,ExtREAL; end; definition let X be non empty set; let f1,f2 be without+infty Function of X,ExtREAL; redefine func f1+f2 -> without+infty Function of X,ExtREAL; end; definition let X be non empty set; let f1 be without-infty Function of X,ExtREAL; let f2 be without+infty Function of X,ExtREAL; redefine func f1-f2 -> without-infty Function of X,ExtREAL; end; definition let X be non empty set; let f1 be without+infty Function of X,ExtREAL; let f2 be without-infty Function of X,ExtREAL; redefine func f1-f2 -> without+infty Function of X,ExtREAL; end; theorem :: DBLSEQ_3:7 for X be non empty set, x be Element of X, f1,f2 be Function of X,ExtREAL holds ( f1 is without-infty & f2 is without-infty implies (f1+f2).x = f1.x + f2.x ) & ( f1 is without+infty & f2 is without+infty implies (f1+f2).x = f1.x + f2.x ) & ( f1 is without-infty & f2 is without+infty implies (f1-f2).x = f1.x - f2.x ) & ( f1 is without+infty & f2 is without-infty implies (f1-f2).x = f1.x - f2.x ) ; theorem :: DBLSEQ_3:8 for X be non empty set, f1,f2 be without-infty Function of X,ExtREAL holds f1 + f2 = f1 - (-f2) & -(f1 + f2) = -f1 - f2; theorem :: DBLSEQ_3:9 for X be non empty set, f1,f2 be without+infty Function of X,ExtREAL holds f1 + f2 = f1 - (-f2) & -(f1 + f2) = -f1 - f2; theorem :: DBLSEQ_3:10 for X be non empty set, f1 be without-infty Function of X,ExtREAL, f2 be without+infty Function of X,ExtREAL holds f1 - f2 = f1 + (-f2) & f2 - f1 = f2 + (-f1) & -(f1 - f2) = -f1 + f2 & -(f2 - f1) = -f2 + f1; definition let f be Function of [:NAT,NAT:],ExtREAL, n,m be Nat; redefine func f.(n,m) -> Element of ExtREAL; end; theorem :: DBLSEQ_3:11 for f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (f1+f2).(n,m) = f1.(n,m) + f2.(n,m); theorem :: DBLSEQ_3:12 for f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (f1+f2).(n,m) = f1.(n,m) + f2.(n,m); theorem :: DBLSEQ_3:13 for f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be without+infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (f1-f2).(n,m) = f1.(n,m) - f2.(n,m) & (f2-f1).(n,m) = f2.(n,m) - f1.(n,m); theorem :: DBLSEQ_3:14 for X,Y be non empty set, f1,f2 be without-infty Function of [:X,Y:],ExtREAL holds ~(f1+f2) = ~f1 + ~f2; theorem :: DBLSEQ_3:15 for X,Y be non empty set, f1,f2 be without+infty Function of [:X,Y:],ExtREAL holds ~(f1+f2) = ~f1 + ~f2; theorem :: DBLSEQ_3:16 for X,Y be non empty set, f1 be without-infty Function of [:X,Y:],ExtREAL, f2 be without+infty Function of [:X,Y:],ExtREAL holds ~(f1-f2) = ~f1 - ~f2 & ~(f2-f1) = ~f2 - ~f1; registration cluster convergent_to_+infty -> convergent for ExtREAL_sequence; cluster convergent_to_-infty -> convergent for ExtREAL_sequence; cluster convergent_to_finite_number -> convergent for ExtREAL_sequence; end; registration cluster convergent for ExtREAL_sequence; cluster convergent for without-infty ExtREAL_sequence; cluster convergent for without+infty ExtREAL_sequence; end; theorem :: DBLSEQ_3:17 for seq be convergent ExtREAL_sequence holds (seq is convergent_to_finite_number iff -seq is convergent_to_finite_number) & (seq is convergent_to_+infty iff -seq is convergent_to_-infty) & (seq is convergent_to_-infty iff -seq is convergent_to_+infty) & -seq is convergent & lim (-seq) = - lim seq; theorem :: DBLSEQ_3:18 for seq1,seq2 be without-infty ExtREAL_sequence st seq1 is convergent_to_+infty & seq2 is convergent_to_+infty holds seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim(seq1+seq2) = +infty; theorem :: DBLSEQ_3:19 for seq1,seq2 be without-infty ExtREAL_sequence st seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number holds seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim(seq1+seq2)=+infty; theorem :: DBLSEQ_3:20 for seq1,seq2 be without+infty ExtREAL_sequence st seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number holds seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim(seq1+seq2)=+infty; theorem :: DBLSEQ_3:21 for seq1,seq2 be without-infty ExtREAL_sequence st seq1 is convergent_to_-infty & seq2 is convergent_to_-infty holds seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim(seq1+seq2) = -infty; theorem :: DBLSEQ_3:22 for seq1,seq2 be without-infty ExtREAL_sequence st seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number holds seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim(seq1+seq2) = -infty; theorem :: DBLSEQ_3:23 for seq1,seq2 be without-infty ExtREAL_sequence st seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number holds seq1 + seq2 is convergent_to_finite_number & seq1 + seq2 is convergent & lim(seq1+seq2) = lim seq1 + lim seq2; theorem :: DBLSEQ_3:24 for seq1,seq2 be without+infty ExtREAL_sequence holds (seq1 is convergent_to_+infty & seq2 is convergent_to_+infty implies seq1+seq2 is convergent_to_+infty & seq1+seq2 is convergent & lim(seq1+seq2) = +infty) & (seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number implies seq1+seq2 is convergent_to_+infty & seq1+seq2 is convergent & lim(seq1+seq2) = +infty) & (seq1 is convergent_to_-infty & seq2 is convergent_to_-infty implies seq1+seq2 is convergent_to_-infty & seq1+seq2 is convergent & lim(seq1+seq2) = -infty) & (seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies seq1+seq2 is convergent_to_-infty & seq1+seq2 is convergent & lim(seq1+seq2) = -infty) & (seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies seq1+seq2 is convergent_to_finite_number & seq1+seq2 is convergent & lim(seq1+seq2) = lim seq1 + lim seq2); theorem :: DBLSEQ_3:25 for seq1 be without-infty ExtREAL_sequence, seq2 be without+infty ExtREAL_sequence holds (seq1 is convergent_to_+infty & seq2 is convergent_to_-infty implies seq1-seq2 is convergent_to_+infty & seq1-seq2 is convergent & seq2-seq1 is convergent_to_-infty & seq2-seq1 is convergent & lim(seq1-seq2) = +infty & lim(seq2-seq1) = -infty) & (seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number implies seq1-seq2 is convergent_to_+infty & seq1-seq2 is convergent & seq2-seq1 is convergent_to_-infty & seq2-seq1 is convergent & lim(seq1-seq2) = +infty & lim(seq2-seq1) = -infty) & (seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies seq1-seq2 is convergent_to_-infty & seq1-seq2 is convergent & seq2-seq1 is convergent_to_+infty & seq2-seq1 is convergent & lim(seq1-seq2) = -infty & lim(seq2-seq1) = +infty) & (seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies seq1-seq2 is convergent_to_finite_number & seq1-seq2 is convergent & seq2-seq1 is convergent_to_finite_number & seq2-seq1 is convergent & lim(seq1-seq2) = lim seq1 - lim seq2 & lim(seq2-seq1) = lim seq2 - lim seq1); begin :: Subsequences of convergent extended real valued sequences theorem :: DBLSEQ_3:26 for seq1,seq2 be ExtREAL_sequence st seq2 is subsequence of seq1 & seq1 is convergent_to_finite_number holds seq2 is convergent_to_finite_number & lim seq1 = lim seq2; theorem :: DBLSEQ_3:27 for seq1,seq2 be ExtREAL_sequence st seq2 is subsequence of seq1 & seq1 is convergent_to_+infty holds seq2 is convergent_to_+infty & lim seq2=+infty; theorem :: DBLSEQ_3:28 for seq1,seq2 be ExtREAL_sequence st seq2 is subsequence of seq1 & seq1 is convergent_to_-infty holds seq2 is convergent_to_-infty & lim seq2=-infty; begin :: Convergency for extended real valued double sequences theorem :: DBLSEQ_3:29 for Rseq be Function of [:NAT,NAT:],REAL st lim_in_cod1 Rseq is convergent holds cod1_major_iterated_lim Rseq = lim (lim_in_cod1 Rseq); theorem :: DBLSEQ_3:30 for Rseq be Function of [:NAT,NAT:],REAL st lim_in_cod2 Rseq is convergent holds cod2_major_iterated_lim Rseq = lim (lim_in_cod2 Rseq); definition let Eseq be Function of [:NAT,NAT:],ExtREAL; attr Eseq is P-convergent_to_finite_number means :: DBLSEQ_3:def 1 ex p be Real st for e be Real st 0=N & m>=N holds |. Eseq.(n,m) - (p qua ExtReal) .| < e; attr Eseq is P-convergent_to_+infty means :: DBLSEQ_3:def 2 for g be Real st 0 < g ex N be Nat st for n,m be Nat st n>=N & m>=N holds g <= Eseq.(n,m); attr Eseq is P-convergent_to_-infty means :: DBLSEQ_3:def 3 for g be Real st g < 0 ex N be Nat st for n,m be Nat st n>=N & m>=N holds Eseq.(n,m) <= g; end; definition let f be Function of [:NAT,NAT:],ExtREAL; attr f is convergent_in_cod1_to_+infty means :: DBLSEQ_3:def 4 for m be Element of NAT holds ProjMap2(f,m) is convergent_to_+infty; attr f is convergent_in_cod1_to_-infty means :: DBLSEQ_3:def 5 for m be Element of NAT holds ProjMap2(f,m) is convergent_to_-infty; attr f is convergent_in_cod1_to_finite means :: DBLSEQ_3:def 6 for m be Element of NAT holds ProjMap2(f,m) is convergent_to_finite_number; attr f is convergent_in_cod1 means :: DBLSEQ_3:def 7 for m be Element of NAT holds ProjMap2(f,m) is convergent; attr f is convergent_in_cod2_to_+infty means :: DBLSEQ_3:def 8 for m be Element of NAT holds ProjMap1(f,m) is convergent_to_+infty; attr f is convergent_in_cod2_to_-infty means :: DBLSEQ_3:def 9 for m be Element of NAT holds ProjMap1(f,m) is convergent_to_-infty; attr f is convergent_in_cod2_to_finite means :: DBLSEQ_3:def 10 for m be Element of NAT holds ProjMap1(f,m) is convergent_to_finite_number; attr f is convergent_in_cod2 means :: DBLSEQ_3:def 11 for m be Element of NAT holds ProjMap1(f,m) is convergent; end; theorem :: DBLSEQ_3:31 for f be Function of [:NAT,NAT:],ExtREAL holds ( f is convergent_in_cod1_to_+infty or f is convergent_in_cod1_to_-infty or f is convergent_in_cod1_to_finite implies f is convergent_in_cod1 ) & ( f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty or f is convergent_in_cod2_to_finite implies f is convergent_in_cod2 ); theorem :: DBLSEQ_3:32 for X,Y,Z be non empty set, F be Function of [:X,Y:],Z, x be Element of X holds ProjMap1(F,x) = ProjMap2(~F,x); theorem :: DBLSEQ_3:33 for X,Y,Z be non empty set, F be Function of [:X,Y:],Z, y be Element of Y holds ProjMap2(F,y) = ProjMap1(~F,y); theorem :: DBLSEQ_3:34 for X,Y be non empty set, F be Function of [:X,Y:],ExtREAL, x be Element of X holds ProjMap1(-F,x) = -ProjMap1(F,x); theorem :: DBLSEQ_3:35 for X,Y be non empty set, F be Function of [:X,Y:],ExtREAL, y be Element of Y holds ProjMap2(-F,y) = -ProjMap2(F,y); theorem :: DBLSEQ_3:36 for f be Function of [:NAT,NAT:],ExtREAL holds (f is convergent_in_cod1_to_+infty iff ~f is convergent_in_cod2_to_+infty) & (f is convergent_in_cod2_to_+infty iff ~f is convergent_in_cod1_to_+infty) & (f is convergent_in_cod1_to_-infty iff ~f is convergent_in_cod2_to_-infty) & (f is convergent_in_cod2_to_-infty iff ~f is convergent_in_cod1_to_-infty) & (f is convergent_in_cod1_to_finite iff ~f is convergent_in_cod2_to_finite) & (f is convergent_in_cod2_to_finite iff ~f is convergent_in_cod1_to_finite); theorem :: DBLSEQ_3:37 for f be Function of [:NAT,NAT:],ExtREAL holds (f is convergent_in_cod1_to_+infty iff -f is convergent_in_cod1_to_-infty) & (f is convergent_in_cod1_to_-infty iff -f is convergent_in_cod1_to_+infty) & (f is convergent_in_cod1_to_finite iff -f is convergent_in_cod1_to_finite) & (f is convergent_in_cod2_to_+infty iff -f is convergent_in_cod2_to_-infty) & (f is convergent_in_cod2_to_-infty iff -f is convergent_in_cod2_to_+infty) & (f is convergent_in_cod2_to_finite iff -f is convergent_in_cod2_to_finite); definition let f be Function of [:NAT,NAT:],ExtREAL; func lim_in_cod1 f -> ExtREAL_sequence means :: DBLSEQ_3:def 12 for m be Element of NAT holds it.m = lim ProjMap2(f,m); func lim_in_cod2 f -> ExtREAL_sequence means :: DBLSEQ_3:def 13 for n be Element of NAT holds it.n = lim ProjMap1(f,n); end; theorem :: DBLSEQ_3:38 for f be Function of [:NAT,NAT:],ExtREAL holds lim_in_cod1 f = lim_in_cod2 (~f) & lim_in_cod2 f = lim_in_cod1 (~f); registration let X,Y be non empty set, F be without+infty Function of [:X,Y:],ExtREAL, x be Element of X; cluster ProjMap1(F,x) -> without+infty; end; registration let X,Y be non empty set, F be without+infty Function of [:X,Y:],ExtREAL, y be Element of Y; cluster ProjMap2(F,y) -> without+infty; end; registration let X,Y be non empty set, F be without-infty Function of [:X,Y:],ExtREAL, x be Element of X; cluster ProjMap1(F,x) -> without-infty; end; registration let X,Y be non empty set, F be without-infty Function of [:X,Y:],ExtREAL, y be Element of Y; cluster ProjMap2(F,y) -> without-infty; end; definition let f be Function of [:NAT,NAT:],ExtREAL; func Partial_Sums_in_cod2 f -> Function of [:NAT,NAT:],ExtREAL means :: DBLSEQ_3:def 14 for n,m be Nat holds it.(n,0) = f.(n,0) & it.(n,m+1) = it.(n,m) + f.(n,m+1); end; definition let f be Function of [:NAT,NAT:],ExtREAL; func Partial_Sums_in_cod1 f -> Function of [:NAT,NAT:],ExtREAL means :: DBLSEQ_3:def 15 for n,m be Nat holds it.(0,m) = f.(0,m) & it.(n+1,m) = it.(n,m) + f.(n+1,m); end; registration let f be without-infty Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod2 f -> without-infty; end; registration let f be without+infty Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod2 f -> without+infty; end; registration let f be nonnegative Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod2 f -> nonnegative for Function of [:NAT,NAT:],ExtREAL; end; registration let f be nonpositive Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod2 f -> nonpositive for Function of [:NAT,NAT:],ExtREAL; end; registration let f be without-infty Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod1 f -> without-infty; end; registration let f be without+infty Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod1 f -> without+infty; end; registration let f be nonnegative Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod1 f -> nonnegative for Function of [:NAT,NAT:],ExtREAL; end; registration let f be nonpositive Function of [:NAT,NAT:],ExtREAL; cluster Partial_Sums_in_cod1 f -> nonpositive for Function of [:NAT,NAT:],ExtREAL; end; definition let f be Function of [:NAT,NAT:],ExtREAL; func Partial_Sums f -> Function of [:NAT,NAT:],ExtREAL equals :: DBLSEQ_3:def 16 Partial_Sums_in_cod2( Partial_Sums_in_cod1 f ); end; theorem :: DBLSEQ_3:39 for f be Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (Partial_Sums_in_cod1 f).(n,m) = (Partial_Sums_in_cod2 ~f).(m,n) & (Partial_Sums_in_cod2 f).(n,m) = (Partial_Sums_in_cod1 ~f).(m,n); theorem :: DBLSEQ_3:40 for f be Function of [:NAT,NAT:],ExtREAL holds ~Partial_Sums_in_cod1 f = Partial_Sums_in_cod2 ~f & ~Partial_Sums_in_cod2 f = Partial_Sums_in_cod1 ~f; theorem :: DBLSEQ_3:41 for f be Function of [:NAT,NAT:],ExtREAL, g be ext-real-valued Function, n be Nat st (for k be Nat holds (Partial_Sums_in_cod1 f).(n,k) = g.k) holds (for k be Nat holds (Partial_Sums f).(n,k) = (Partial_Sums g).k) & (lim_in_cod2(Partial_Sums f)).n = Sum g; theorem :: DBLSEQ_3:42 for f be Function of [:NAT,NAT:],ExtREAL holds Partial_Sums_in_cod2(-f) = -(Partial_Sums_in_cod2 f) & Partial_Sums_in_cod1(-f) = -(Partial_Sums_in_cod1 f); theorem :: DBLSEQ_3:43 for f be Function of [:NAT,NAT:],ExtREAL, m,n be Element of NAT holds (Partial_Sums_in_cod1 f).(m,n) = Partial_Sums(ProjMap2(f,n)).m & (Partial_Sums_in_cod2 f).(m,n) = Partial_Sums(ProjMap1(f,m)).n; theorem :: DBLSEQ_3:44 for f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums_in_cod2(f1+f2) = Partial_Sums_in_cod2 f1 + Partial_Sums_in_cod2 f2 & Partial_Sums_in_cod1(f1+f2) = Partial_Sums_in_cod1 f1 + Partial_Sums_in_cod1 f2; theorem :: DBLSEQ_3:45 for f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums_in_cod2(f1+f2) = Partial_Sums_in_cod2 f1 + Partial_Sums_in_cod2 f2 & Partial_Sums_in_cod1(f1+f2) = Partial_Sums_in_cod1 f1 + Partial_Sums_in_cod1 f2; theorem :: DBLSEQ_3:46 for f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums_in_cod2(f1-f2) = Partial_Sums_in_cod2 f1 - Partial_Sums_in_cod2 f2 & Partial_Sums_in_cod1(f1-f2) = Partial_Sums_in_cod1 f1 - Partial_Sums_in_cod1 f2 & Partial_Sums_in_cod2(f2-f1) = Partial_Sums_in_cod2 f2 - Partial_Sums_in_cod2 f1 & Partial_Sums_in_cod1(f2-f1) = Partial_Sums_in_cod1 f2 - Partial_Sums_in_cod1 f1; theorem :: DBLSEQ_3:47 for f be without-infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (Partial_Sums f).(n+1,m) = (Partial_Sums_in_cod2 f).(n+1,m) + (Partial_Sums f).(n,m) & (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m+1) = (Partial_Sums_in_cod1 f).(n,m+1) + (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m); theorem :: DBLSEQ_3:48 for f be without+infty Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (Partial_Sums f).(n+1,m) = (Partial_Sums_in_cod2 f).(n+1,m) + (Partial_Sums f).(n,m) & (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m+1) = (Partial_Sums_in_cod1 f).(n,m+1) + (Partial_Sums_in_cod1(Partial_Sums_in_cod2 f)).(n,m); theorem :: DBLSEQ_3:49 for f be Function of [:NAT,NAT:],ExtREAL st f is without-infty or f is without+infty holds Partial_Sums f = Partial_Sums_in_cod1(Partial_Sums_in_cod2 f); theorem :: DBLSEQ_3:50 for f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums(f1 + f2) = Partial_Sums f1 + Partial_Sums f2; theorem :: DBLSEQ_3:51 for f1,f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums(f1 + f2) = Partial_Sums f1 + Partial_Sums f2; theorem :: DBLSEQ_3:52 for f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be without+infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums(f1 - f2) = Partial_Sums f1 - Partial_Sums f2 & Partial_Sums(f2 - f1) = Partial_Sums f2 - Partial_Sums f1; theorem :: DBLSEQ_3:53 for f be Function of [:NAT,NAT:],ExtREAL, k be Element of NAT holds ProjMap2(Partial_Sums_in_cod1 f,k) = Partial_Sums(ProjMap2(f,k)) & ProjMap1(Partial_Sums_in_cod2 f,k) = Partial_Sums(ProjMap1(f,k)); theorem :: DBLSEQ_3:54 for f be Function of [:NAT,NAT:],ExtREAL st f is without-infty or f is without+infty holds ProjMap1(Partial_Sums f,0) = ProjMap1(Partial_Sums_in_cod2 f,0) & ProjMap2(Partial_Sums f,0) = ProjMap2(Partial_Sums_in_cod1 f,0); theorem :: DBLSEQ_3:55 for C,D be non empty set, F1,F2 be without-infty Function of [:C,D:],ExtREAL, c be Element of C holds ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c); theorem :: DBLSEQ_3:56 for C,D be non empty set, F1,F2 be without-infty Function of [:C,D:],ExtREAL, d be Element of D holds ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d); theorem :: DBLSEQ_3:57 for C,D be non empty set, F1,F2 be without+infty Function of [:C,D:],ExtREAL, c be Element of C holds ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c); theorem :: DBLSEQ_3:58 for C,D be non empty set, F1,F2 be without+infty Function of [:C,D:],ExtREAL, d be Element of D holds ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d); theorem :: DBLSEQ_3:59 for C,D be non empty set, F1 be without-infty Function of [:C,D:],ExtREAL, F2 be without+infty Function of [:C,D:],ExtREAL, c be Element of C holds ProjMap1(F1-F2,c) = ProjMap1(F1,c) - ProjMap1(F2,c) & ProjMap1(F2-F1,c) = ProjMap1(F2,c) - ProjMap1(F1,c); theorem :: DBLSEQ_3:60 for C,D be non empty set, F1 be without-infty Function of [:C,D:],ExtREAL, F2 be without+infty Function of [:C,D:],ExtREAL, d be Element of D holds ProjMap2(F1-F2,d) = ProjMap2(F1,d) - ProjMap2(F2,d) & ProjMap2(F2-F1,d) = ProjMap2(F2,d) - ProjMap2(F1,d); begin :: Nonnegative extended real valued double sequences theorem :: DBLSEQ_3:61 for seq be nonnegative ExtREAL_sequence st not Partial_Sums seq is convergent_to_+infty holds for n be Nat holds seq.n is Real; theorem :: DBLSEQ_3:62 for seq be nonnegative ExtREAL_sequence st seq is non-decreasing holds seq is convergent_to_+infty or seq is convergent_to_finite_number; registration let f be nonnegative Function of [:NAT,NAT:],ExtREAL, n be Element of NAT; cluster ProjMap1(f,n) -> nonnegative; cluster ProjMap2(f,n) -> nonnegative; end; theorem :: DBLSEQ_3:63 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT holds ProjMap1(Partial_Sums_in_cod2 f,m) is non-decreasing; theorem :: DBLSEQ_3:64 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n be Element of NAT holds ProjMap2(Partial_Sums_in_cod1 f,n) is non-decreasing; registration let f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT; cluster ProjMap1(Partial_Sums_in_cod2 f,m) -> non-decreasing; cluster ProjMap2(Partial_Sums_in_cod1 f,m) -> non-decreasing; end; theorem :: DBLSEQ_3:65 for f be nonnegative Function of [:NAT,NAT:],ExtREAL holds ( f is convergent_in_cod1 implies lim_in_cod1 f is nonnegative ) & ( f is convergent_in_cod2 implies lim_in_cod2 f is nonnegative ); theorem :: DBLSEQ_3:66 for f be nonnegative Function of [:NAT,NAT:],ExtREAL holds Partial_Sums_in_cod1 f is convergent_in_cod1 & Partial_Sums_in_cod2 f is convergent_in_cod2; theorem :: DBLSEQ_3:67 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT st not ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_+infty holds for n be Nat holds f.(n,m) is Real; theorem :: DBLSEQ_3:68 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT st not ProjMap1(Partial_Sums_in_cod2 f,m) is convergent_to_+infty holds for n be Nat holds f.(m,n) is Real; theorem :: DBLSEQ_3:69 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat st (for i be Nat st i <= n holds f.(i,m) is Real) holds (Partial_Sums_in_cod1 f).(n,m) < +infty; theorem :: DBLSEQ_3:70 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat st (for i be Nat st i <= m holds f.(n,i) is Real) holds (Partial_Sums_in_cod2 f).(n,m) < +infty; theorem :: DBLSEQ_3:71 for f be without-infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f is convergent_in_cod1_to_-infty implies ex m be Element of NAT st ProjMap2(Partial_Sums_in_cod1 f,m) is convergent_to_-infty; theorem :: DBLSEQ_3:72 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat holds (for k be Element of NAT st k<=m holds not ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty) iff (for k be Element of NAT st k<=m holds lim ProjMap1(Partial_Sums_in_cod2 f,k) < +infty); theorem :: DBLSEQ_3:73 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat holds (for k be Element of NAT st k<=m holds not ProjMap2(Partial_Sums_in_cod1 f,k) is convergent_to_+infty) iff (for k be Element of NAT st k<=m holds lim ProjMap2(Partial_Sums_in_cod1 f,k) < +infty); theorem :: DBLSEQ_3:74 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat holds (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m = +infty iff ex k be Element of NAT st k <= m & ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty; theorem :: DBLSEQ_3:75 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Nat holds (Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 f))).m = +infty iff ex k be Element of NAT st k <= m & ProjMap2(Partial_Sums_in_cod1 f,k) is convergent_to_+infty; theorem :: DBLSEQ_3:76 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, n,m be Nat holds (Partial_Sums_in_cod1 f).(n,m) >= f.(n,m) & (Partial_Sums_in_cod2 f).(n,m) >= f.(n,m); theorem :: DBLSEQ_3:77 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT st (ex k be Element of NAT st k <= m & ProjMap1(Partial_Sums_in_cod2 f,k) is convergent_to_+infty) holds ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m) is convergent_to_+infty & lim(ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m)) = +infty; theorem :: DBLSEQ_3:78 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, m be Element of NAT st (ex k be Element of NAT st k <= m & ProjMap2(Partial_Sums_in_cod1 f,k) is convergent_to_+infty) holds ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f),m) is convergent_to_+infty & lim(ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f),m)) = +infty; theorem :: DBLSEQ_3:79 for f be without-infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f is convergent_in_cod1_to_finite iff Partial_Sums_in_cod1 f is convergent_in_cod1_to_finite; theorem :: DBLSEQ_3:80 for f be nonnegative Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod1_to_finite holds for m be Element of NAT holds (Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 f))).m = lim(ProjMap2(Partial_Sums_in_cod1(Partial_Sums_in_cod2 f),m)); theorem :: DBLSEQ_3:81 for f be without-infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f is convergent_in_cod2_to_finite iff Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite; theorem :: DBLSEQ_3:82 for f be nonnegative Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod2_to_finite holds for m be Element of NAT holds (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 f))).m = lim(ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1 f),m)); :: Fatou's Lemma for Double Sequence theorem :: DBLSEQ_3:83 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, seq be ExtREAL_sequence st (for m be Element of NAT holds seq.m = lim_inf ProjMap2(f,m)) holds Sum seq <= lim_inf lim_in_cod2(Partial_Sums_in_cod2 f); theorem :: DBLSEQ_3:84 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, seq be ExtREAL_sequence st (for m be Element of NAT holds seq.m = lim_inf ProjMap1(f,m)) holds Sum seq <= lim_inf lim_in_cod1(Partial_Sums_in_cod1 f); theorem :: DBLSEQ_3:85 for f be Function of [:NAT,NAT:],ExtREAL, seq be ExtREAL_sequence, n,m be Nat holds ( (for i,j be Nat holds f.(i,j) <= seq.i) implies (Partial_Sums_in_cod1 f).(n,m) <= (Partial_Sums seq).n ) & ( (for i,j be Nat holds f.(i,j) <= seq.j) implies (Partial_Sums_in_cod2 f).(n,m) <= (Partial_Sums seq).m ); theorem :: DBLSEQ_3:86 for seq be ExtREAL_sequence, r be R_eal st (for n be Nat holds seq.n <= r) holds lim_sup seq <= r; theorem :: DBLSEQ_3:87 for seq be ExtREAL_sequence, r be R_eal st (for n be Nat holds r <= seq.n) holds r <= lim_inf seq; theorem :: DBLSEQ_3:88 for f be nonnegative Function of [:NAT,NAT:],ExtREAL holds ( for i1,i2,j be Nat st i1 <= i2 holds (Partial_Sums_in_cod1 f).(i1,j) <= (Partial_Sums_in_cod1 f).(i2,j) ) & ( for i,j1,j2 be Nat st j1 <= j2 holds (Partial_Sums_in_cod2 f).(i,j1) <= (Partial_Sums_in_cod2 f).(i,j2) ); theorem :: DBLSEQ_3:89 for f be Function of [:NAT,NAT:],ExtREAL, i,j,k be Nat st (for m be Element of NAT holds ProjMap2(f,m) is non-decreasing) & i<=j holds (Partial_Sums_in_cod2 f).(i,k) <= (Partial_Sums_in_cod2 f).(j,k); theorem :: DBLSEQ_3:90 for f be Function of [:NAT,NAT:],ExtREAL, i,j,k be Nat st (for n be Element of NAT holds ProjMap1(f,n) is non-decreasing) & i<=j holds (Partial_Sums_in_cod1 f).(k,i) <= (Partial_Sums_in_cod1 f).(k,j); :: Moonotone Convergence Theorem for Double Sequence theorem :: DBLSEQ_3:91 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, seq be ExtREAL_sequence st (for m be Element of NAT holds ProjMap2(f,m) is non-decreasing & seq.m = lim ProjMap2(f,m)) holds lim_in_cod2(Partial_Sums_in_cod2 f) is non-decreasing & Sum seq = lim lim_in_cod2(Partial_Sums_in_cod2 f); theorem :: DBLSEQ_3:92 for f be nonnegative Function of [:NAT,NAT:],ExtREAL, seq be ExtREAL_sequence st (for m be Element of NAT holds ProjMap1(f,m) is non-decreasing & seq.m = lim ProjMap1(f,m)) holds lim_in_cod1(Partial_Sums_in_cod1 f) is non-decreasing & Sum seq = lim lim_in_cod1(Partial_Sums_in_cod1 f); begin :: Pringsheim sense convergence for extended real valued double sequences theorem :: DBLSEQ_3:93 for f be Function of [:NAT,NAT:],ExtREAL st f is P-convergent_to_+infty holds not f is P-convergent_to_-infty & not f is P-convergent_to_finite_number; theorem :: DBLSEQ_3:94 for f be Function of [:NAT,NAT:],ExtREAL st f is P-convergent_to_-infty holds not f is P-convergent_to_+infty & not f is P-convergent_to_finite_number; definition let f be Function of [:NAT,NAT:],ExtREAL; attr f is P-convergent means :: DBLSEQ_3:def 17 f is P-convergent_to_finite_number or f is P-convergent_to_+infty or f is P-convergent_to_-infty; end; definition let f be Function of [:NAT,NAT:],ExtREAL; assume f is P-convergent; func P-lim f -> ExtReal means :: DBLSEQ_3:def 18 (ex p be Real st it = p & (for e be Real st 0=N & m>=N holds |.f.(n,m) - it.| < e) & f is P-convergent_to_finite_number) or (it = +infty & f is P-convergent_to_+infty) or (it = -infty & f is P-convergent_to_-infty); end; theorem :: DBLSEQ_3:95 for f be Function of [:NAT,NAT:],ExtREAL, r be Real st (for n,m be Nat holds f.(n,m) = r) holds f is P-convergent_to_finite_number & P-lim f = r; theorem :: DBLSEQ_3:96 for f be Function of [:NAT,NAT:],ExtREAL st (for n1,m1,n2,m2 be Nat st n1<=n2 & m1<=m2 holds f.(n1,m1)<=f.(n2,m2)) holds f is P-convergent & P-lim f = sup rng f; theorem :: DBLSEQ_3:97 for f1,f2 be Function of [:NAT,NAT:],ExtREAL st (for n,m be Nat holds f1.(n,m) <= f2.(n,m)) holds sup rng f1 <= sup rng f2; theorem :: DBLSEQ_3:98 for f be Function of [:NAT,NAT:],ExtREAL holds for n,m be Nat holds f.(n,m) <= sup rng f; theorem :: DBLSEQ_3:99 for f be Function of [:NAT,NAT:],ExtREAL, K be R_eal st (for n,m be Nat holds f.(n,m) <= K) holds sup rng f <= K; theorem :: DBLSEQ_3:100 for f be Function of [:NAT,NAT:],ExtREAL, K be R_eal st K <> +infty & (for n,m be Nat holds f.(n,m) <= K) holds sup rng f < +infty; theorem :: DBLSEQ_3:101 for f be without-infty Function of [:NAT,NAT:],ExtREAL holds sup rng f <> +infty iff ex K be Real st 0 < K & for n,m be Nat holds f.(n,m) <= K; theorem :: DBLSEQ_3:102 for f be Function of [:NAT,NAT:],ExtREAL, c be ExtReal st (for n,m be Nat holds f.(n,m) = c) holds f is P-convergent & P-lim f = c & P-lim f = sup rng f; theorem :: DBLSEQ_3:103 for f be Function of [:NAT,NAT:],ExtREAL, f1,f2 be without-infty Function of [:NAT,NAT:],ExtREAL st (for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f1.(n1,m1) <= f1.(n2,m2) ) & (for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f2.(n1,m1) <= f2.(n2,m2) ) & (for n,m be Nat holds f1.(n,m) + f2.(n,m) = f.(n,m) ) holds f is P-convergent & P-lim f = sup rng f & P-lim f = P-lim f1 + P-lim f2 & sup rng f = sup rng f1 + sup rng f2; theorem :: DBLSEQ_3:104 for f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be Function of [:NAT,NAT:],ExtREAL, c be Real st 0 <= c & (for n,m be Nat holds f2.(n,m) = c * f1.(n,m)) holds sup rng f2 = c * sup rng f1 & f2 is without-infty; theorem :: DBLSEQ_3:105 for f1 be without-infty Function of [:NAT,NAT:],ExtREAL, f2 be Function of [:NAT,NAT:],ExtREAL, c be Real st 0 <= c & ( for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f1.(n1,m1) <= f1.(n2,m2) ) & ( for n,m be Nat holds f2.(n,m) = c * f1.(n,m) ) holds (for n1,m1,n2,m2 be Nat st n1 <= n2 & m1 <= m2 holds f2.(n1,m1) <= f2.(n2,m2) ) & f2 is without-infty & f2 is P-convergent & P-lim f2 = sup rng f2 & P-lim f2 = c * P-lim f1;