:: Extended Real Valued Double Sequence and Its Convergence
:: by Noboru Endou
::
:: Received July 1, 2015
:: Copyright (c) 2015-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, 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;