:: Extended Real Valued Double Sequence and Its Convergence
:: by Noboru Endou
::
:: Received July 1, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

Lm1: for X being set
for x being object holds (X --> 0.) . x = 0

proof end;

registration

let X be non empty set ;

cluster non empty V7() V10(X) V11( REAL ) Function-like total V32(X, REAL ) complex-valued ext-real-valued real-valued nonnegative nonpositive for Element of bool [:X,REAL:];

existence
ex b₁ being Function of X,REAL st
( b₁ is nonnegative & b₁ is nonpositive )

proof end;

end;

registration

let X be non empty set ;

cluster non empty V7() V10(X) V11( ExtREAL ) Function-like total V32(X, ExtREAL ) ext-real-valued nonnegative nonpositive V183() V184() for Element of bool [:X,ExtREAL:];

existence
ex b₁ being Function of X,ExtREAL st
( b₁ is V183() & b₁ is V184() & b₁ is nonnegative & b₁ is nonpositive )

proof end;

end;

Lm2: for X being non empty set holds
( X --> 0. is V183() Function of X,ExtREAL & X --> 0. is V184() Function of X,ExtREAL )

proof end;

registration

let X be non empty set ;

cluster Function-like V32(X, ExtREAL ) nonnegative -> V183() for Element of bool [:X,ExtREAL:];

correctness
coherence
for b₁ being Function of X,ExtREAL st b₁ is nonnegative holds
b₁ is V183();

proof end;

cluster Function-like V32(X, ExtREAL ) nonpositive -> V184() for Element of bool [:X,ExtREAL:];

correctness
coherence
for b₁ being Function of X,ExtREAL st b₁ is nonpositive holds
b₁ is V184();

proof end;

cluster non empty V7() V10(X) V11( ExtREAL ) Function-like total V32(X, ExtREAL ) ext-real-valued V183() V184() for Element of bool [:X,ExtREAL:];

existence
not for b₁ being V184() Function of X,ExtREAL holds b₁ is V183()

proof end;

end;

definition

let X be non empty set ;
let f be Function of X,ExtREAL;
:: original: -
redefine func - f -> Function of X,ExtREAL;
correctness
coherence
- f is Function of X,ExtREAL;

proof end;

end;

registration

let X be non empty set ;
let f be V183() Function of X,ExtREAL;

cluster - f -> V184() ;

correctness
coherence
- f is without+infty ;

proof end;

end;

registration

let X be non empty set ;
let f be V184() Function of X,ExtREAL;

cluster - f -> V183() ;

correctness
coherence
- f is without-infty ;

proof end;

end;

registration

let X be non empty set ;
let f be nonnegative Function of X,ExtREAL;

cluster - f -> nonpositive ;

correctness
coherence
- f is nonpositive ;

proof end;

end;

registration

let X be non empty set ;
let f be nonpositive Function of X,ExtREAL;

cluster - f -> nonnegative ;

correctness
coherence
- f is nonnegative ;

proof end;

end;

registration

let A, B be non empty set ;
let f be V183() Function of [:A,B:],ExtREAL;

cluster ~ f -> without-infty ;

correctness
coherence
~ f is without-infty ;

proof end;

end;

registration

let A, B be non empty set ;
let f be V184() Function of [:A,B:],ExtREAL;

cluster ~ f -> without+infty ;

correctness
coherence
~ f is without+infty ;

proof end;

end;

registration

let A, B be non empty set ;
let f be nonnegative Function of [:A,B:],ExtREAL;

cluster ~ f -> nonnegative ;

correctness
coherence
~ f is nonnegative ;

proof end;

end;

registration

let A, B be non empty set ;
let f be nonpositive Function of [:A,B:],ExtREAL;

cluster ~ f -> nonpositive ;

correctness
coherence
~ f is nonpositive ;

proof end;

end;

theorem Th1: :: DBLSEQ_3:1

for seq being ExtREAL_sequence holds Partial_Sums (- seq) = - (Partial_Sums seq)

proof end;

theorem Th2: :: DBLSEQ_3:2

for X being non empty set
for f being PartFunc of X,ExtREAL holds - (- f) = f

proof end;

theorem :: DBLSEQ_3:3

for X, Y being non empty set
for f being Function of [:X,Y:],ExtREAL holds ~ (- f) = - (~ f)

proof end;

registration

let seq be nonnegative ExtREAL_sequence;

cluster Partial_Sums seq -> nonnegative ;

correctness
coherence
Partial_Sums seq is nonnegative ;
by MESFUNC9:16;

end;

registration

let seq be nonpositive ExtREAL_sequence;

cluster Partial_Sums seq -> nonpositive ;

correctness
coherence
Partial_Sums seq is nonpositive ;

proof end;

end;

theorem Th4: :: DBLSEQ_3:4

for seq being nonnegative ExtREAL_sequence
for m being Nat holds seq . m <= (Partial_Sums seq) . m

proof end;

theorem :: DBLSEQ_3:5

for seq being nonpositive ExtREAL_sequence
for m being Nat holds seq . m >= (Partial_Sums seq) . m

proof end;

theorem :: DBLSEQ_3:6

for X being non empty set
for f being V183() V184() Function of X,ExtREAL holds f is Function of X,REAL

proof end;

definition

let X be non empty set ;
let f1, f2 be V183() Function of X,ExtREAL;
:: original: +
redefine func f1 + f2 -> V183() Function of X,ExtREAL;
correctness
coherence
f1 + f2 is V183() Function of X,ExtREAL;

proof end;

end;

definition

let X be non empty set ;
let f1, f2 be V184() Function of X,ExtREAL;
:: original: +
redefine func f1 + f2 -> V184() Function of X,ExtREAL;
correctness
coherence
f1 + f2 is V184() Function of X,ExtREAL;

proof end;

end;

definition

let X be non empty set ;
let f1 be V183() Function of X,ExtREAL;
let f2 be V184() Function of X,ExtREAL;
:: original: -
redefine func f1 - f2 -> V183() Function of X,ExtREAL;
correctness
coherence
f1 - f2 is V183() Function of X,ExtREAL;

proof end;

end;

definition

let X be non empty set ;
let f1 be V184() Function of X,ExtREAL;
let f2 be V183() Function of X,ExtREAL;
:: original: -
redefine func f1 - f2 -> V184() Function of X,ExtREAL;
correctness
coherence
f1 - f2 is V184() Function of X,ExtREAL;

proof end;

end;

theorem Th7: :: DBLSEQ_3:7

for X being non empty set
for x being Element of X
for f1, f2 being Function of X,ExtREAL holds
( ( f1 is V183() & f2 is V183() implies (f1 + f2) . x = (f1 . x) + (f2 . x) ) & ( f1 is V184() & f2 is V184() implies (f1 + f2) . x = (f1 . x) + (f2 . x) ) & ( f1 is V183() & f2 is V184() implies (f1 - f2) . x = (f1 . x) - (f2 . x) ) & ( f1 is V184() & f2 is V183() implies (f1 - f2) . x = (f1 . x) - (f2 . x) ) )

proof end;

Lm3: for X being non empty set
for f1, f2 being V183() Function of X,ExtREAL holds f1 + f2 = f1 - (- f2)

proof end;

Lm4: for X being non empty set
for f1, f2 being V184() Function of X,ExtREAL holds f1 + f2 = f1 - (- f2)

proof end;

Lm5: for X being non empty set
for f1 being V183() Function of X,ExtREAL
for f2 being V184() Function of X,ExtREAL holds
( f1 - f2 = f1 + (- f2) & f2 - f1 = f2 + (- f1) )

proof end;

theorem Th8: :: DBLSEQ_3:8

for X being non empty set
for f1, f2 being V183() Function of X,ExtREAL holds
( f1 + f2 = f1 - (- f2) & - (f1 + f2) = (- f1) - f2 )

proof end;

theorem Th9: :: DBLSEQ_3:9

for X being non empty set
for f1, f2 being V184() Function of X,ExtREAL holds
( f1 + f2 = f1 - (- f2) & - (f1 + f2) = (- f1) - f2 )

proof end;

theorem Th10: :: DBLSEQ_3:10

for X being non empty set
for f1 being V183() Function of X,ExtREAL
for f2 being V184() Function of X,ExtREAL holds
( f1 - f2 = f1 + (- f2) & f2 - f1 = f2 + (- f1) & - (f1 - f2) = (- f1) + f2 & - (f2 - f1) = (- f2) + f1 )

proof end;

definition

let f be Function of [:NAT,NAT:],ExtREAL;
let n, m be Nat;
:: original: .
redefine func f . (n,m) -> Element of ExtREAL ;
coherence
f . (n,m) is Element of ExtREAL

proof end;

end;

theorem Th11: :: DBLSEQ_3:11

for f1, f2 being V183() Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds (f1 + f2) . (n,m) = (f1 . (n,m)) + (f2 . (n,m))

proof end;

theorem :: DBLSEQ_3:12

for f1, f2 being V184() Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds (f1 + f2) . (n,m) = (f1 . (n,m)) + (f2 . (n,m))

proof end;

theorem :: DBLSEQ_3:13

for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being V184() Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds
( (f1 - f2) . (n,m) = (f1 . (n,m)) - (f2 . (n,m)) & (f2 - f1) . (n,m) = (f2 . (n,m)) - (f1 . (n,m)) )

proof end;

theorem :: DBLSEQ_3:14

for X, Y being non empty set
for f1, f2 being V183() Function of [:X,Y:],ExtREAL holds ~ (f1 + f2) = (~ f1) + (~ f2)

proof end;

theorem :: DBLSEQ_3:15

for X, Y being non empty set
for f1, f2 being V184() Function of [:X,Y:],ExtREAL holds ~ (f1 + f2) = (~ f1) + (~ f2)

proof end;

theorem :: DBLSEQ_3:16

for X, Y being non empty set
for f1 being V183() Function of [:X,Y:],ExtREAL
for f2 being V184() Function of [:X,Y:],ExtREAL holds
( ~ (f1 - f2) = (~ f1) - (~ f2) & ~ (f2 - f1) = (~ f2) - (~ f1) )

proof end;

registration

cluster Function-like V32( omega , ExtREAL ) convergent_to_+infty -> convergent for Element of bool [:omega,ExtREAL:];

correctness
coherence
for b₁ being ExtREAL_sequence st b₁ is convergent_to_+infty holds
b₁ is convergent ;
by MESFUNC5:def 11;

cluster Function-like V32( omega , ExtREAL ) convergent_to_-infty -> convergent for Element of bool [:omega,ExtREAL:];

correctness
coherence
for b₁ being ExtREAL_sequence st b₁ is convergent_to_-infty holds
b₁ is convergent ;
by MESFUNC5:def 11;

cluster Function-like V32( omega , ExtREAL ) convergent_to_finite_number -> convergent for Element of bool [:omega,ExtREAL:];

correctness
coherence
for b₁ being ExtREAL_sequence st b₁ is convergent_to_finite_number holds
b₁ is convergent ;
by MESFUNC5:def 11;

end;

registration

cluster non empty V7() V10( omega ) V11( ExtREAL ) Function-like total V32( omega , ExtREAL ) ext-real-valued convergent for Element of bool [:omega,ExtREAL:];

existence
ex b₁ being ExtREAL_sequence st b₁ is convergent

proof end;

cluster non empty V7() V10( omega ) V11( ExtREAL ) Function-like total V32( omega , ExtREAL ) ext-real-valued V183() convergent for Element of bool [:omega,ExtREAL:];

existence
ex b₁ being V183() ExtREAL_sequence st b₁ is convergent

proof end;

cluster non empty V7() V10( omega ) V11( ExtREAL ) Function-like total V32( omega , ExtREAL ) ext-real-valued V184() convergent for Element of bool [:omega,ExtREAL:];

existence
ex b₁ being V184() ExtREAL_sequence st b₁ is convergent

proof end;

end;

Lm6: for seq being convergent ExtREAL_sequence holds
( ( seq is convergent_to_finite_number implies - seq is convergent_to_finite_number ) & ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) & ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & - seq is convergent & lim (- seq) = - (lim seq) )

proof end;

theorem Th17: :: DBLSEQ_3:17

for seq being convergent ExtREAL_sequence holds
( ( seq is convergent_to_finite_number implies - seq is convergent_to_finite_number ) & ( - seq is convergent_to_finite_number implies seq is convergent_to_finite_number ) & ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) & ( - seq is convergent_to_-infty implies seq is convergent_to_+infty ) & ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & ( - seq is convergent_to_+infty implies seq is convergent_to_-infty ) & - seq is convergent & lim (- seq) = - (lim seq) )

proof end;

theorem Th18: :: DBLSEQ_3:18

for seq1, seq2 being V183() 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 )

proof end;

theorem Th19: :: DBLSEQ_3:19

for seq1, seq2 being V183() 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 )

proof end;

theorem :: DBLSEQ_3:20

for seq1, seq2 being V184() 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 )

proof end;

theorem Th21: :: DBLSEQ_3:21

for seq1, seq2 being V183() 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 )

proof end;

theorem Th22: :: DBLSEQ_3:22

for seq1, seq2 being V183() 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 )

proof end;

theorem Th23: :: DBLSEQ_3:23

for seq1, seq2 being V183() 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) )

proof end;

theorem Th24: :: DBLSEQ_3:24

for seq1, seq2 being V184() 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) ) ) )

proof end;

theorem :: DBLSEQ_3:25

for seq1 being V183() ExtREAL_sequence
for seq2 being V184() 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) ) ) )

proof end;

theorem :: DBLSEQ_3:26

for seq1, seq2 being 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 )

proof end;

theorem :: DBLSEQ_3:27

for seq1, seq2 being ExtREAL_sequence st seq2 is subsequence of seq1 & seq1 is convergent_to_+infty holds
( seq2 is convergent_to_+infty & lim seq2 = +infty )

proof end;

theorem :: DBLSEQ_3:28

for seq1, seq2 being ExtREAL_sequence st seq2 is subsequence of seq1 & seq1 is convergent_to_-infty holds
( seq2 is convergent_to_-infty & lim seq2 = -infty )

proof end;

theorem :: DBLSEQ_3:29

for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod1 Rseq is convergent holds
cod1_major_iterated_lim Rseq = lim (lim_in_cod1 Rseq)

proof end;

theorem :: DBLSEQ_3:30

for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod2 Rseq is convergent holds
cod2_major_iterated_lim Rseq = lim (lim_in_cod2 Rseq)

proof end;

definition

let Eseq be Function of [:NAT,NAT:],ExtREAL;

attr Eseq is P-convergent_to_finite_number means :: DBLSEQ_3:def 1
ex p being Real st
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Eseq . (n,m)) - p).| < e;

attr Eseq is P-convergent_to_+infty means :: DBLSEQ_3:def 2
for g being Real st 0 < g holds
ex N being Nat st
for n, m being 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 being Real st g < 0 holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
Eseq . (n,m) <= g;

end;

:: deftheorem defines P-convergent_to_finite_number DBLSEQ_3:def 1 :
for Eseq being Function of [:NAT,NAT:],ExtREAL holds
( Eseq is P-convergent_to_finite_number iff ex p being Real st
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Eseq . (n,m)) - p).| < e );

:: deftheorem defines P-convergent_to_+infty DBLSEQ_3:def 2 :
for Eseq being Function of [:NAT,NAT:],ExtREAL holds
( Eseq is P-convergent_to_+infty iff for g being Real st 0 < g holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
g <= Eseq . (n,m) );

:: deftheorem defines P-convergent_to_-infty DBLSEQ_3:def 3 :
for Eseq being Function of [:NAT,NAT:],ExtREAL holds
( Eseq is P-convergent_to_-infty iff for g being Real st g < 0 holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
Eseq . (n,m) <= g );

definition

let f be Function of [:NAT,NAT:],ExtREAL;

attr f is convergent_in_cod1_to_+infty means :: DBLSEQ_3:def 4
for m being 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 being 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 being 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 being Element of NAT holds ProjMap2 (f,m) is convergent ;

attr f is convergent_in_cod2_to_+infty means :: DBLSEQ_3:def 8
for m being 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 being 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 being 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 being Element of NAT holds ProjMap1 (f,m) is convergent ;

end;

:: deftheorem defines convergent_in_cod1_to_+infty DBLSEQ_3:def 4 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1_to_+infty iff for m being Element of NAT holds ProjMap2 (f,m) is convergent_to_+infty );

:: deftheorem defines convergent_in_cod1_to_-infty DBLSEQ_3:def 5 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1_to_-infty iff for m being Element of NAT holds ProjMap2 (f,m) is convergent_to_-infty );

:: deftheorem defines convergent_in_cod1_to_finite DBLSEQ_3:def 6 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1_to_finite iff for m being Element of NAT holds ProjMap2 (f,m) is convergent_to_finite_number );

:: deftheorem defines convergent_in_cod1 DBLSEQ_3:def 7 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1 iff for m being Element of NAT holds ProjMap2 (f,m) is convergent );

:: deftheorem defines convergent_in_cod2_to_+infty DBLSEQ_3:def 8 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod2_to_+infty iff for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_+infty );

:: deftheorem defines convergent_in_cod2_to_-infty DBLSEQ_3:def 9 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod2_to_-infty iff for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_-infty );

:: deftheorem defines convergent_in_cod2_to_finite DBLSEQ_3:def 10 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod2_to_finite iff for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_finite_number );

:: deftheorem defines convergent_in_cod2 DBLSEQ_3:def 11 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod2 iff for m being Element of NAT holds ProjMap1 (f,m) is convergent );

theorem :: DBLSEQ_3:31

for f being 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 ) )

proof end;

theorem Th32: :: DBLSEQ_3:32

for X, Y, Z being non empty set
for F being Function of [:X,Y:],Z
for x being Element of X holds ProjMap1 (F,x) = ProjMap2 ((~ F),x)

proof end;

theorem Th33: :: DBLSEQ_3:33

for X, Y, Z being non empty set
for F being Function of [:X,Y:],Z
for y being Element of Y holds ProjMap2 (F,y) = ProjMap1 ((~ F),y)

proof end;

theorem Th34: :: DBLSEQ_3:34

for X, Y being non empty set
for F being Function of [:X,Y:],ExtREAL
for x being Element of X holds ProjMap1 ((- F),x) = - (ProjMap1 (F,x))

proof end;

theorem Th35: :: DBLSEQ_3:35

for X, Y being non empty set
for F being Function of [:X,Y:],ExtREAL
for y being Element of Y holds ProjMap2 ((- F),y) = - (ProjMap2 (F,y))

proof end;

theorem Th36: :: DBLSEQ_3:36

for f being Function of [:NAT,NAT:],ExtREAL holds
( ( f is convergent_in_cod1_to_+infty implies ~ f is convergent_in_cod2_to_+infty ) & ( ~ f is convergent_in_cod2_to_+infty implies f is convergent_in_cod1_to_+infty ) & ( f is convergent_in_cod2_to_+infty implies ~ f is convergent_in_cod1_to_+infty ) & ( ~ f is convergent_in_cod1_to_+infty implies f is convergent_in_cod2_to_+infty ) & ( f is convergent_in_cod1_to_-infty implies ~ f is convergent_in_cod2_to_-infty ) & ( ~ f is convergent_in_cod2_to_-infty implies f is convergent_in_cod1_to_-infty ) & ( f is convergent_in_cod2_to_-infty implies ~ f is convergent_in_cod1_to_-infty ) & ( ~ f is convergent_in_cod1_to_-infty implies f is convergent_in_cod2_to_-infty ) & ( f is convergent_in_cod1_to_finite implies ~ f is convergent_in_cod2_to_finite ) & ( ~ f is convergent_in_cod2_to_finite implies f is convergent_in_cod1_to_finite ) & ( f is convergent_in_cod2_to_finite implies ~ f is convergent_in_cod1_to_finite ) & ( ~ f is convergent_in_cod1_to_finite implies f is convergent_in_cod2_to_finite ) )

proof end;

theorem :: DBLSEQ_3:37

for f being Function of [:NAT,NAT:],ExtREAL holds
( ( f is convergent_in_cod1_to_+infty implies - f is convergent_in_cod1_to_-infty ) & ( - f is convergent_in_cod1_to_-infty implies f is convergent_in_cod1_to_+infty ) & ( f is convergent_in_cod1_to_-infty implies - f is convergent_in_cod1_to_+infty ) & ( - f is convergent_in_cod1_to_+infty implies f is convergent_in_cod1_to_-infty ) & ( f is convergent_in_cod1_to_finite implies - f is convergent_in_cod1_to_finite ) & ( - f is convergent_in_cod1_to_finite implies f is convergent_in_cod1_to_finite ) & ( f is convergent_in_cod2_to_+infty implies - f is convergent_in_cod2_to_-infty ) & ( - f is convergent_in_cod2_to_-infty implies f is convergent_in_cod2_to_+infty ) & ( f is convergent_in_cod2_to_-infty implies - f is convergent_in_cod2_to_+infty ) & ( - f is convergent_in_cod2_to_+infty implies f is convergent_in_cod2_to_-infty ) & ( f is convergent_in_cod2_to_finite implies - f is convergent_in_cod2_to_finite ) & ( - f is convergent_in_cod2_to_finite implies f is convergent_in_cod2_to_finite ) )

proof end;

definition

let f be Function of [:NAT,NAT:],ExtREAL;

func lim_in_cod1 f -> ExtREAL_sequence means :D1DEF5: :: DBLSEQ_3:def 12
for m being Element of NAT holds it . m = lim (ProjMap2 (f,m));

existence
ex b₁ being ExtREAL_sequence st
for m being Element of NAT holds b₁ . m = lim (ProjMap2 (f,m))

proof end;

uniqueness
for b₁, b₂ being ExtREAL_sequence st ( for m being Element of NAT holds b₁ . m = lim (ProjMap2 (f,m)) ) & ( for m being Element of NAT holds b₂ . m = lim (ProjMap2 (f,m)) ) holds
b₁ = b₂

proof end;

func lim_in_cod2 f -> ExtREAL_sequence means :D1DEF6: :: DBLSEQ_3:def 13
for n being Element of NAT holds it . n = lim (ProjMap1 (f,n));

existence
ex b₁ being ExtREAL_sequence st
for n being Element of NAT holds b₁ . n = lim (ProjMap1 (f,n))

proof end;

uniqueness
for b₁, b₂ being ExtREAL_sequence st ( for n being Element of NAT holds b₁ . n = lim (ProjMap1 (f,n)) ) & ( for n being Element of NAT holds b₂ . n = lim (ProjMap1 (f,n)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem D1DEF5 defines lim_in_cod1 DBLSEQ_3:def 12 :
for f being Function of [:NAT,NAT:],ExtREAL
for b₂ being ExtREAL_sequence holds
( b₂ = lim_in_cod1 f iff for m being Element of NAT holds b₂ . m = lim (ProjMap2 (f,m)) );

:: deftheorem D1DEF6 defines lim_in_cod2 DBLSEQ_3:def 13 :
for f being Function of [:NAT,NAT:],ExtREAL
for b₂ being ExtREAL_sequence holds
( b₂ = lim_in_cod2 f iff for n being Element of NAT holds b₂ . n = lim (ProjMap1 (f,n)) );

theorem Th38: :: DBLSEQ_3:38

for f being Function of [:NAT,NAT:],ExtREAL holds
( lim_in_cod1 f = lim_in_cod2 (~ f) & lim_in_cod2 f = lim_in_cod1 (~ f) )

proof end;

registration

let X, Y be non empty set ;
let F be V184() Function of [:X,Y:],ExtREAL;
let x be Element of X;

cluster ProjMap1 (F,x) -> V184() ;

correctness
coherence
ProjMap1 (F,x) is without+infty ;

proof end;

end;

registration

let X, Y be non empty set ;
let F be V184() Function of [:X,Y:],ExtREAL;
let y be Element of Y;

cluster ProjMap2 (F,y) -> V184() ;

correctness
coherence
ProjMap2 (F,y) is without+infty ;

proof end;

end;

registration

let X, Y be non empty set ;
let F be V183() Function of [:X,Y:],ExtREAL;
let x be Element of X;

cluster ProjMap1 (F,x) -> V183() ;

correctness
coherence
ProjMap1 (F,x) is without-infty ;

proof end;

end;

registration

let X, Y be non empty set ;
let F be V183() Function of [:X,Y:],ExtREAL;
let y be Element of Y;

cluster ProjMap2 (F,y) -> V183() ;

correctness
coherence
ProjMap2 (F,y) is without-infty ;

proof end;

end;

definition

let f be Function of [:NAT,NAT:],ExtREAL;

func Partial_Sums_in_cod2 f -> Function of [:NAT,NAT:],ExtREAL means :DefCSM: :: DBLSEQ_3:def 14
for n, m being Nat holds
( it . (n,0) = f . (n,0) & it . (n,(m + 1)) = (it . (n,m)) + (f . (n,(m + 1))) );

existence
ex b₁ being Function of [:NAT,NAT:],ExtREAL st
for n, m being Nat holds
( b₁ . (n,0) = f . (n,0) & b₁ . (n,(m + 1)) = (b₁ . (n,m)) + (f . (n,(m + 1))) )

proof end;

uniqueness
for b₁, b₂ being Function of [:NAT,NAT:],ExtREAL st ( for n, m being Nat holds
( b₁ . (n,0) = f . (n,0) & b₁ . (n,(m + 1)) = (b₁ . (n,m)) + (f . (n,(m + 1))) ) ) & ( for n, m being Nat holds
( b₂ . (n,0) = f . (n,0) & b₂ . (n,(m + 1)) = (b₂ . (n,m)) + (f . (n,(m + 1))) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefCSM defines Partial_Sums_in_cod2 DBLSEQ_3:def 14 :
for f, b₂ being Function of [:NAT,NAT:],ExtREAL holds
( b₂ = Partial_Sums_in_cod2 f iff for n, m being Nat holds
( b₂ . (n,0) = f . (n,0) & b₂ . (n,(m + 1)) = (b₂ . (n,m)) + (f . (n,(m + 1))) ) );

definition

let f be Function of [:NAT,NAT:],ExtREAL;

func Partial_Sums_in_cod1 f -> Function of [:NAT,NAT:],ExtREAL means :DefRSM: :: DBLSEQ_3:def 15
for n, m being Nat holds
( it . (0,m) = f . (0,m) & it . ((n + 1),m) = (it . (n,m)) + (f . ((n + 1),m)) );

existence
ex b₁ being Function of [:NAT,NAT:],ExtREAL st
for n, m being Nat holds
( b₁ . (0,m) = f . (0,m) & b₁ . ((n + 1),m) = (b₁ . (n,m)) + (f . ((n + 1),m)) )

proof end;

uniqueness
for b₁, b₂ being Function of [:NAT,NAT:],ExtREAL st ( for n, m being Nat holds
( b₁ . (0,m) = f . (0,m) & b₁ . ((n + 1),m) = (b₁ . (n,m)) + (f . ((n + 1),m)) ) ) & ( for n, m being Nat holds
( b₂ . (0,m) = f . (0,m) & b₂ . ((n + 1),m) = (b₂ . (n,m)) + (f . ((n + 1),m)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefRSM defines Partial_Sums_in_cod1 DBLSEQ_3:def 15 :
for f, b₂ being Function of [:NAT,NAT:],ExtREAL holds
( b₂ = Partial_Sums_in_cod1 f iff for n, m being Nat holds
( b₂ . (0,m) = f . (0,m) & b₂ . ((n + 1),m) = (b₂ . (n,m)) + (f . ((n + 1),m)) ) );

registration

let f be V183() Function of [:NAT,NAT:],ExtREAL;

cluster Partial_Sums_in_cod2 f -> V183() ;

correctness
coherence
Partial_Sums_in_cod2 f is without-infty ;

proof end;

end;

registration

let f be V184() Function of [:NAT,NAT:],ExtREAL;

cluster Partial_Sums_in_cod2 f -> V184() ;

correctness
coherence
Partial_Sums_in_cod2 f is without+infty ;

proof end;

end;

registration

let f be nonnegative Function of [:NAT,NAT:],ExtREAL;

cluster Partial_Sums_in_cod2 f -> nonnegative for Function of [:NAT,NAT:],ExtREAL;

correctness
coherence
for b₁ being Function of [:NAT,NAT:],ExtREAL st b₁ = Partial_Sums_in_cod2 f holds
b₁ is nonnegative ;

proof end;

end;

registration

let f be nonpositive Function of [:NAT,NAT:],ExtREAL;

cluster Partial_Sums_in_cod2 f -> nonpositive for Function of [:NAT,NAT:],ExtREAL;

correctness
coherence
for b₁ being Function of [:NAT,NAT:],ExtREAL st b₁ = Partial_Sums_in_cod2 f holds
b₁ is nonpositive ;

proof end;

end;

registration

let f be V183() Function of [:NAT,NAT:],ExtREAL;

cluster Partial_Sums_in_cod1 f -> V183() ;

correctness
coherence
Partial_Sums_in_cod1 f is without-infty ;

proof end;

end;

registration

let f be V184() Function of [:NAT,NAT:],ExtREAL;

cluster Partial_Sums_in_cod1 f -> V184() ;

correctness
coherence
Partial_Sums_in_cod1 f is without+infty ;

proof end;

end;

registration

let f be nonnegative Function of [:NAT,NAT:],ExtREAL;

cluster Partial_Sums_in_cod1 f -> nonnegative for Function of [:NAT,NAT:],ExtREAL;

correctness
coherence
for b₁ being Function of [:NAT,NAT:],ExtREAL st b₁ = Partial_Sums_in_cod1 f holds
b₁ is nonnegative ;

proof end;

end;

registration

let f be nonpositive Function of [:NAT,NAT:],ExtREAL;

cluster Partial_Sums_in_cod1 f -> nonpositive for Function of [:NAT,NAT:],ExtREAL;

correctness
coherence
for b₁ being Function of [:NAT,NAT:],ExtREAL st b₁ = Partial_Sums_in_cod1 f holds
b₁ is nonpositive ;

proof end;

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);

correctness
coherence
Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f) is Function of [:NAT,NAT:],ExtREAL;
;

end;

:: deftheorem defines Partial_Sums DBLSEQ_3:def 16 :
for f being Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f = Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f);

theorem Th39: :: DBLSEQ_3:39

for f being Function of [:NAT,NAT:],ExtREAL
for n, m being 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) )

proof end;

theorem Th40: :: DBLSEQ_3:40

for f being 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) )

proof end;

theorem :: DBLSEQ_3:41

for f being Function of [:NAT,NAT:],ExtREAL
for g being ext-real-valued Function
for n being Nat st ( for k being Nat holds (Partial_Sums_in_cod1 f) . (n,k) = g . k ) holds
( ( for k being Nat holds (Partial_Sums f) . (n,k) = (Partial_Sums g) . k ) & (lim_in_cod2 (Partial_Sums f)) . n = Sum g )

proof end;

theorem Th42: :: DBLSEQ_3:42

for f being 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) )

proof end;

theorem Th43: :: DBLSEQ_3:43

for f being Function of [:NAT,NAT:],ExtREAL
for m, n being 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 )

proof end;

theorem Th44: :: DBLSEQ_3:44

for f1, f2 being V183() 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) )

proof end;

theorem Th45: :: DBLSEQ_3:45

for f1, f2 being V184() 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) )

proof end;

theorem Th46: :: DBLSEQ_3:46

for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being V184() 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) )

proof end;

theorem Th47: :: DBLSEQ_3:47

for f being V183() Function of [:NAT,NAT:],ExtREAL
for n, m being 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)) )

proof end;

theorem :: DBLSEQ_3:48

for f being V184() Function of [:NAT,NAT:],ExtREAL
for n, m being 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)) )

proof end;

Lm7: for f being V183() Function of [:NAT,NAT:],ExtREAL
for m, n being Nat holds (Partial_Sums f) . (m,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (m,n)

proof end;

Lm8: for f being V183() Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)

proof end;

Lm9: for f being V184() Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)

proof end;

theorem :: DBLSEQ_3:49

for f being Function of [:NAT,NAT:],ExtREAL st ( not f is V183() or not f is V184() ) holds
Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f) by Lm8, Lm9;

theorem :: DBLSEQ_3:50

for f1, f2 being V183() Function of [:NAT,NAT:],ExtREAL holds Partial_Sums (f1 + f2) = (Partial_Sums f1) + (Partial_Sums f2)

proof end;

theorem :: DBLSEQ_3:51

for f1, f2 being V184() Function of [:NAT,NAT:],ExtREAL holds Partial_Sums (f1 + f2) = (Partial_Sums f1) + (Partial_Sums f2)

proof end;

theorem :: DBLSEQ_3:52

for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being V184() 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) )

proof end;

theorem :: DBLSEQ_3:53

for f being Function of [:NAT,NAT:],ExtREAL
for k being 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)) )

proof end;

theorem Th54: :: DBLSEQ_3:54

for f being Function of [:NAT,NAT:],ExtREAL st ( not f is V183() or not f is V184() ) 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) )

proof end;

theorem :: DBLSEQ_3:55

for C, D being non empty set
for F1, F2 being V183() Function of [:C,D:],ExtREAL
for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))

proof end;

theorem :: DBLSEQ_3:56

for C, D being non empty set
for F1, F2 being V183() Function of [:C,D:],ExtREAL
for d being Element of D holds ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))

proof end;

theorem :: DBLSEQ_3:57

for C, D being non empty set
for F1, F2 being V184() Function of [:C,D:],ExtREAL
for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))

proof end;

theorem :: DBLSEQ_3:58

for C, D being non empty set
for F1, F2 being V184() Function of [:C,D:],ExtREAL
for d being Element of D holds ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))

proof end;

theorem :: DBLSEQ_3:59

for C, D being non empty set
for F1 being V183() Function of [:C,D:],ExtREAL
for F2 being V184() Function of [:C,D:],ExtREAL
for c being Element of C holds
( ProjMap1 ((F1 - F2),c) = (ProjMap1 (F1,c)) - (ProjMap1 (F2,c)) & ProjMap1 ((F2 - F1),c) = (ProjMap1 (F2,c)) - (ProjMap1 (F1,c)) )

proof end;

theorem :: DBLSEQ_3:60

for C, D being non empty set
for F1 being V183() Function of [:C,D:],ExtREAL
for F2 being V184() Function of [:C,D:],ExtREAL
for d being Element of D holds
( ProjMap2 ((F1 - F2),d) = (ProjMap2 (F1,d)) - (ProjMap2 (F2,d)) & ProjMap2 ((F2 - F1),d) = (ProjMap2 (F2,d)) - (ProjMap2 (F1,d)) )

proof end;

theorem :: DBLSEQ_3:61

for seq being nonnegative ExtREAL_sequence st not Partial_Sums seq is convergent_to_+infty holds
for n being Nat holds seq . n is Real

proof end;

theorem Th62: :: DBLSEQ_3:62

for seq being nonnegative ExtREAL_sequence holds
( not seq is non-decreasing or seq is convergent_to_+infty or seq is convergent_to_finite_number )

proof end;

Lm10: for f being Function of [:NAT,NAT:],ExtREAL
for n being Element of NAT st f is nonnegative holds
( ProjMap1 (f,n) is nonnegative & ProjMap2 (f,n) is nonnegative )

proof end;

registration

let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
let n be Element of NAT ;

cluster ProjMap1 (f,n) -> nonnegative ;

correctness
coherence
ProjMap1 (f,n) is nonnegative ;
by Lm10;

cluster ProjMap2 (f,n) -> nonnegative ;

correctness
coherence
ProjMap2 (f,n) is nonnegative ;
by Lm10;

end;

theorem Th63: :: DBLSEQ_3:63

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT holds ProjMap1 ((Partial_Sums_in_cod2 f),m) is non-decreasing

proof end;

theorem Th64: :: DBLSEQ_3:64

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for n being Element of NAT holds ProjMap2 ((Partial_Sums_in_cod1 f),n) is non-decreasing

proof end;

registration

let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
let m be Element of NAT ;

cluster ProjMap1 ((Partial_Sums_in_cod2 f),m) -> non-decreasing ;

correctness
coherence
ProjMap1 ((Partial_Sums_in_cod2 f),m) is non-decreasing ;
by Th63;

cluster ProjMap2 ((Partial_Sums_in_cod1 f),m) -> non-decreasing ;

correctness
coherence
ProjMap2 ((Partial_Sums_in_cod1 f),m) is non-decreasing ;
by Th64;

end;

theorem Th65: :: DBLSEQ_3:65

for f being 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 ) )

proof end;

theorem :: DBLSEQ_3:66

for f being 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 ) by RINFSUP2:37;

theorem :: DBLSEQ_3:67

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT st not ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_+infty holds
for n being Nat holds f . (n,m) is Real

proof end;

theorem :: DBLSEQ_3:68

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT st not ProjMap1 ((Partial_Sums_in_cod2 f),m) is convergent_to_+infty holds
for n being Nat holds f . (m,n) is Real

proof end;

theorem :: DBLSEQ_3:69

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for n, m being Nat st ( for i being Nat st i <= n holds
f . (i,m) is Real ) holds
(Partial_Sums_in_cod1 f) . (n,m) < +infty

proof end;

theorem :: DBLSEQ_3:70

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for n, m being Nat st ( for i being Nat st i <= m holds
f . (n,i) is Real ) holds
(Partial_Sums_in_cod2 f) . (n,m) < +infty

proof end;

theorem :: DBLSEQ_3:71

for f being V183() Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod1_to_-infty holds
ex m being Element of NAT st ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_-infty

proof end;

theorem Th72: :: DBLSEQ_3:72

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Nat holds
( ( for k being Element of NAT st k <= m holds
not ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) iff for k being Element of NAT st k <= m holds
lim (ProjMap1 ((Partial_Sums_in_cod2 f),k)) < +infty )

proof end;

theorem :: DBLSEQ_3:73

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Nat holds
( ( for k being Element of NAT st k <= m holds
not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) iff for k being Element of NAT st k <= m holds
lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty )

proof end;

theorem Th74: :: DBLSEQ_3:74

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Nat holds
( (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = +infty iff ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) )

proof end;

theorem :: DBLSEQ_3:75

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Nat holds
( (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = +infty iff ex k being Element of NAT st
( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) )

proof end;

theorem Th76: :: DBLSEQ_3:76

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds
( (Partial_Sums_in_cod1 f) . (n,m) >= f . (n,m) & (Partial_Sums_in_cod2 f) . (n,m) >= f . (n,m) )

proof end;

theorem Th77: :: DBLSEQ_3:77

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT st ex k being 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 )

proof end;

theorem :: DBLSEQ_3:78

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT st ex k being 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 )

proof end;

theorem Th79: :: DBLSEQ_3:79

for f being V183() 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 )

proof end;

theorem Th80: :: DBLSEQ_3:80

for f being nonnegative Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod1_to_finite holds
for m being 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))

proof end;

theorem :: DBLSEQ_3:81

for f being V183() 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 )

proof end;

theorem :: DBLSEQ_3:82

for f being nonnegative Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod2_to_finite holds
for m being 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))

proof end;

:: Fatou's Lemma for Double Sequence

theorem Th83: :: DBLSEQ_3:83

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence st ( for m being Element of NAT holds seq . m = lim_inf (ProjMap2 (f,m)) ) holds
Sum seq <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f))

proof end;

theorem :: DBLSEQ_3:84

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence st ( for m being Element of NAT holds seq . m = lim_inf (ProjMap1 (f,m)) ) holds
Sum seq <= lim_inf (lim_in_cod1 (Partial_Sums_in_cod1 f))

proof end;

theorem Th85: :: DBLSEQ_3:85

for f being Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence
for n, m being Nat holds
( ( ( for i, j being Nat holds f . (i,j) <= seq . i ) implies (Partial_Sums_in_cod1 f) . (n,m) <= (Partial_Sums seq) . n ) & ( ( for i, j being Nat holds f . (i,j) <= seq . j ) implies (Partial_Sums_in_cod2 f) . (n,m) <= (Partial_Sums seq) . m ) )

proof end;

theorem Th86: :: DBLSEQ_3:86

for seq being ExtREAL_sequence
for r being R_eal st ( for n being Nat holds seq . n <= r ) holds
lim_sup seq <= r

proof end;

theorem Th87: :: DBLSEQ_3:87

for seq being ExtREAL_sequence
for r being R_eal st ( for n being Nat holds r <= seq . n ) holds
r <= lim_inf seq

proof end;

theorem :: DBLSEQ_3:88

for f being nonnegative Function of [:NAT,NAT:],ExtREAL holds
( ( for i1, i2, j being Nat st i1 <= i2 holds
(Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,j2) ) )

proof end;

theorem Th89: :: DBLSEQ_3:89

for f being Function of [:NAT,NAT:],ExtREAL
for i, j, k being Nat st ( for m being 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)

proof end;

theorem :: DBLSEQ_3:90

for f being Function of [:NAT,NAT:],ExtREAL
for i, j, k being Nat st ( for n being 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)

proof end;

:: Moonotone Convergence Theorem for Double Sequence

theorem Th91: :: DBLSEQ_3:91

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence st ( for m being 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)) )

proof end;

theorem :: DBLSEQ_3:92

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence st ( for m being 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)) )

proof end;

theorem Th93: :: DBLSEQ_3:93

for f being 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 )

proof end;

theorem Th94: :: DBLSEQ_3:94

for f being 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 )

proof end;

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;

:: deftheorem defines P-convergent DBLSEQ_3:def 17 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is P-convergent iff ( f is P-convergent_to_finite_number or f is P-convergent_to_+infty or f is P-convergent_to_-infty ) );

definition

let f be Function of [:NAT,NAT:],ExtREAL;
assume A1: f is P-convergent ;

func P-lim f -> ExtReal means :Def5: :: DBLSEQ_3:def 18
( ex p being Real st
( it = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= 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 ) );

existence
ex b₁ being ExtReal st
( ex p being Real st
( b₁ = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b₁).| < e ) & f is P-convergent_to_finite_number ) or ( b₁ = +infty & f is P-convergent_to_+infty ) or ( b₁ = -infty & f is P-convergent_to_-infty ) )

proof end;

uniqueness
for b₁, b₂ being ExtReal st ( ex p being Real st
( b₁ = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b₁).| < e ) & f is P-convergent_to_finite_number ) or ( b₁ = +infty & f is P-convergent_to_+infty ) or ( b₁ = -infty & f is P-convergent_to_-infty ) ) & ( ex p being Real st
( b₂ = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b₂).| < e ) & f is P-convergent_to_finite_number ) or ( b₂ = +infty & f is P-convergent_to_+infty ) or ( b₂ = -infty & f is P-convergent_to_-infty ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines P-lim DBLSEQ_3:def 18 :
for f being Function of [:NAT,NAT:],ExtREAL st f is P-convergent holds
for b₂ being ExtReal holds
( b₂ = P-lim f iff ( ex p being Real st
( b₂ = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b₂).| < e ) & f is P-convergent_to_finite_number ) or ( b₂ = +infty & f is P-convergent_to_+infty ) or ( b₂ = -infty & f is P-convergent_to_-infty ) ) );

theorem :: DBLSEQ_3:95

for f being Function of [:NAT,NAT:],ExtREAL
for r being Real st ( for n, m being Nat holds f . (n,m) = r ) holds
( f is P-convergent_to_finite_number & P-lim f = r )

proof end;

theorem Th96: :: DBLSEQ_3:96

for f being Function of [:NAT,NAT:],ExtREAL st ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f . (n1,m1) <= f . (n2,m2) ) holds
( f is P-convergent & P-lim f = sup (rng f) )

proof end;

theorem :: DBLSEQ_3:97

for f1, f2 being Function of [:NAT,NAT:],ExtREAL st ( for n, m being Nat holds f1 . (n,m) <= f2 . (n,m) ) holds
sup (rng f1) <= sup (rng f2)

proof end;

theorem :: DBLSEQ_3:98

for f being Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds f . (n,m) <= sup (rng f)

proof end;

theorem :: DBLSEQ_3:99

for f being Function of [:NAT,NAT:],ExtREAL
for K being R_eal st ( for n, m being Nat holds f . (n,m) <= K ) holds
sup (rng f) <= K

proof end;

theorem :: DBLSEQ_3:100

for f being Function of [:NAT,NAT:],ExtREAL
for K being R_eal st K <> +infty & ( for n, m being Nat holds f . (n,m) <= K ) holds
sup (rng f) < +infty

proof end;

theorem Th101: :: DBLSEQ_3:101

for f being V183() Function of [:NAT,NAT:],ExtREAL holds
( sup (rng f) <> +infty iff ex K being Real st
( 0 < K & ( for n, m being Nat holds f . (n,m) <= K ) ) )

proof end;

theorem Th102: :: DBLSEQ_3:102

for f being Function of [:NAT,NAT:],ExtREAL
for c being ExtReal st ( for n, m being Nat holds f . (n,m) = c ) holds
( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )

proof end;

Lm8: for f being V183() Function of [:NAT,NAT:],ExtREAL holds
( sup (rng f) in REAL or sup (rng f) = +infty )

proof end;

theorem :: DBLSEQ_3:103

for f being Function of [:NAT,NAT:],ExtREAL
for f1, f2 being V183() Function of [:NAT,NAT:],ExtREAL st ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & ( for n, m being 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)) )

proof end;

theorem Th104: :: DBLSEQ_3:104

for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being Function of [:NAT,NAT:],ExtREAL
for c being Real st 0 <= c & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) holds
( sup (rng f2) = c * (sup (rng f1)) & f2 is V183() )

proof end;

theorem :: DBLSEQ_3:105

for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being Function of [:NAT,NAT:],ExtREAL
for c being Real st 0 <= c & ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) holds
( ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & f2 is V183() & f2 is P-convergent & P-lim f2 = sup (rng f2) & P-lim f2 = c * (P-lim f1) )

proof end;