:: by Noboru Endou

::

:: Received March 31, 2014

:: Copyright (c) 2014-2016 Association of Mizar Users

definition

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

( f is nonnegative-yielding iff for i, j being Nat holds f . (i,j) >= 0 )

end;
redefine attr f is nonnegative-yielding means :: DBLSEQ_2:def 1

for i, j being Nat holds f . (i,j) >= 0 ;

compatibility for i, j being Nat holds f . (i,j) >= 0 ;

( f is nonnegative-yielding iff for i, j being Nat holds f . (i,j) >= 0 )

proof end;

:: deftheorem defines nonnegative-yielding DBLSEQ_2:def 1 :

for f being Function of [:NAT,NAT:],REAL holds

( f is nonnegative-yielding iff for i, j being Nat holds f . (i,j) >= 0 );

for f being Function of [:NAT,NAT:],REAL holds

( f is nonnegative-yielding iff for i, j being Nat holds f . (i,j) >= 0 );

theorem :: DBLSEQ_2:1

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing holds

( ( for m being Element of NAT holds ProjMap1 (Rseq,m) is V115() ) & ( for n being Element of NAT holds ProjMap2 (Rseq,n) is V115() ) )

( ( for m being Element of NAT holds ProjMap1 (Rseq,m) is V115() ) & ( for n being Element of NAT holds ProjMap2 (Rseq,n) is V115() ) )

proof end;

theorem :: DBLSEQ_2:2

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing & Rseq is convergent_in_cod1 holds

lim_in_cod1 Rseq is V115()

lim_in_cod1 Rseq is V115()

proof end;

theorem :: DBLSEQ_2:3

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing & Rseq is convergent_in_cod2 holds

lim_in_cod2 Rseq is V115()

lim_in_cod2 Rseq is V115()

proof end;

theorem :: DBLSEQ_2:4

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing & Rseq is P-convergent holds

for n, m being Nat holds Rseq . (n,m) <= P-lim Rseq

for n, m being Nat holds Rseq . (n,m) <= P-lim Rseq

proof end;

theorem lmADD: :: DBLSEQ_2:5

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL holds

( dom (Rseq1 + Rseq2) = [:NAT,NAT:] & dom (Rseq1 - Rseq2) = [:NAT,NAT:] & ( for n, m being Nat holds (Rseq1 + Rseq2) . (n,m) = (Rseq1 . (n,m)) + (Rseq2 . (n,m)) ) & ( for n, m being Nat holds (Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m)) ) )

( dom (Rseq1 + Rseq2) = [:NAT,NAT:] & dom (Rseq1 - Rseq2) = [:NAT,NAT:] & ( for n, m being Nat holds (Rseq1 + Rseq2) . (n,m) = (Rseq1 . (n,m)) + (Rseq2 . (n,m)) ) & ( for n, m being Nat holds (Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m)) ) )

proof end;

theorem :: DBLSEQ_2:6

for C, D, E being non empty set

for f being Function of [:C,D:],E ex g being Function of [:D,C:],E st

for d being Element of D

for c being Element of C holds g . (d,c) = f . (c,d)

for f being Function of [:C,D:],E ex g being Function of [:D,C:],E st

for d being Element of D

for c being Element of C holds g . (d,c) = f . (c,d)

proof end;

theorem :: DBLSEQ_2:7

scheme :: DBLSEQ_2:sch 1

RecEx2D1{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> Function of F_{1}(),F_{2}(), F_{4}( set , set , Nat) -> Element of F_{2}() } :

RecEx2D1{ F

ex g being Function of [:F_{1}(),NAT:],F_{2}() st

for a being Element of F_{1}() holds

( g . (a,0) = F_{3}() . a & ( for n being Nat holds g . (a,(n + 1)) = F_{4}((g . (a,n)),a,n) ) )

for a being Element of F

( g . (a,0) = F

proof end;

scheme :: DBLSEQ_2:sch 2

RecEx2D1R{ F_{1}() -> non empty set , F_{2}() -> Function of F_{1}(),REAL, F_{3}( set , set , Nat) -> real number } :

RecEx2D1R{ F

ex g being Function of [:F_{1}(),NAT:],REAL st

for a being Element of F_{1}() holds

( g . (a,0) = F_{2}() . a & ( for n being natural number holds g . (a,(n + 1)) = F_{3}((g . (a,n)),a,n) ) )

for a being Element of F

( g . (a,0) = F

proof end;

scheme :: DBLSEQ_2:sch 3

RecEx2D2{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> Function of F_{1}(),F_{2}(), F_{4}( set , set , Nat) -> Element of F_{2}() } :

RecEx2D2{ F

ex g being Function of [:NAT,F_{1}():],F_{2}() st

for a being Element of F_{1}() holds

( g . (0,a) = F_{3}() . a & ( for n being Nat holds g . ((n + 1),a) = F_{4}((g . (n,a)),a,n) ) )

for a being Element of F

( g . (0,a) = F

proof end;

scheme :: DBLSEQ_2:sch 4

RecEx2D2R{ F_{1}() -> non empty set , F_{2}() -> Function of F_{1}(),REAL, F_{3}( set , set , Nat) -> real number } :

RecEx2D2R{ F

ex g being Function of [:NAT,F_{1}():],REAL st

for a being Element of F_{1}() holds

( g . (0,a) = F_{2}() . a & ( for n being Nat holds g . ((n + 1),a) = F_{3}((g . (n,a)),a,n) ) )

for a being Element of F

( g . (0,a) = F

proof end;

definition

let Rseq be Function of [:NAT,NAT:],REAL;

ex b_{1} being Function of [:NAT,NAT:],REAL st

for n, m being Nat holds

( b_{1} . (n,0) = Rseq . (n,0) & b_{1} . (n,(m + 1)) = (b_{1} . (n,m)) + (Rseq . (n,(m + 1))) )

for b_{1}, b_{2} being Function of [:NAT,NAT:],REAL st ( for n, m being Nat holds

( b_{1} . (n,0) = Rseq . (n,0) & b_{1} . (n,(m + 1)) = (b_{1} . (n,m)) + (Rseq . (n,(m + 1))) ) ) & ( for n, m being Nat holds

( b_{2} . (n,0) = Rseq . (n,0) & b_{2} . (n,(m + 1)) = (b_{2} . (n,m)) + (Rseq . (n,(m + 1))) ) ) holds

b_{1} = b_{2}

end;
func Partial_Sums_in_cod2 Rseq -> Function of [:NAT,NAT:],REAL means :DefCS: :: DBLSEQ_2:def 2

for n, m being Nat holds

( it . (n,0) = Rseq . (n,0) & it . (n,(m + 1)) = (it . (n,m)) + (Rseq . (n,(m + 1))) );

existence for n, m being Nat holds

( it . (n,0) = Rseq . (n,0) & it . (n,(m + 1)) = (it . (n,m)) + (Rseq . (n,(m + 1))) );

ex b

for n, m being Nat holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem DefCS defines Partial_Sums_in_cod2 DBLSEQ_2:def 2 :

for Rseq, b_{2} being Function of [:NAT,NAT:],REAL holds

( b_{2} = Partial_Sums_in_cod2 Rseq iff for n, m being Nat holds

( b_{2} . (n,0) = Rseq . (n,0) & b_{2} . (n,(m + 1)) = (b_{2} . (n,m)) + (Rseq . (n,(m + 1))) ) );

for Rseq, b

( b

( b

definition

let Rseq be Function of [:NAT,NAT:],REAL;

ex b_{1} being Function of [:NAT,NAT:],REAL st

for n, m being Nat holds

( b_{1} . (0,m) = Rseq . (0,m) & b_{1} . ((n + 1),m) = (b_{1} . (n,m)) + (Rseq . ((n + 1),m)) )

for b_{1}, b_{2} being Function of [:NAT,NAT:],REAL st ( for n, m being Nat holds

( b_{1} . (0,m) = Rseq . (0,m) & b_{1} . ((n + 1),m) = (b_{1} . (n,m)) + (Rseq . ((n + 1),m)) ) ) & ( for n, m being Nat holds

( b_{2} . (0,m) = Rseq . (0,m) & b_{2} . ((n + 1),m) = (b_{2} . (n,m)) + (Rseq . ((n + 1),m)) ) ) holds

b_{1} = b_{2}

end;
func Partial_Sums_in_cod1 Rseq -> Function of [:NAT,NAT:],REAL means :DefRS: :: DBLSEQ_2:def 3

for n, m being Nat holds

( it . (0,m) = Rseq . (0,m) & it . ((n + 1),m) = (it . (n,m)) + (Rseq . ((n + 1),m)) );

existence for n, m being Nat holds

( it . (0,m) = Rseq . (0,m) & it . ((n + 1),m) = (it . (n,m)) + (Rseq . ((n + 1),m)) );

ex b

for n, m being Nat holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem DefRS defines Partial_Sums_in_cod1 DBLSEQ_2:def 3 :

for Rseq, b_{2} being Function of [:NAT,NAT:],REAL holds

( b_{2} = Partial_Sums_in_cod1 Rseq iff for n, m being Nat holds

( b_{2} . (0,m) = Rseq . (0,m) & b_{2} . ((n + 1),m) = (b_{2} . (n,m)) + (Rseq . ((n + 1),m)) ) );

for Rseq, b

( b

( b

theorem thADD: :: DBLSEQ_2:8

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL holds

( Partial_Sums_in_cod2 (Rseq1 + Rseq2) = (Partial_Sums_in_cod2 Rseq1) + (Partial_Sums_in_cod2 Rseq2) & Partial_Sums_in_cod1 (Rseq1 + Rseq2) = (Partial_Sums_in_cod1 Rseq1) + (Partial_Sums_in_cod1 Rseq2) )

( Partial_Sums_in_cod2 (Rseq1 + Rseq2) = (Partial_Sums_in_cod2 Rseq1) + (Partial_Sums_in_cod2 Rseq2) & Partial_Sums_in_cod1 (Rseq1 + Rseq2) = (Partial_Sums_in_cod1 Rseq1) + (Partial_Sums_in_cod1 Rseq2) )

proof end;

theorem Tr2: :: DBLSEQ_2:9

for Rseq being Function of [:NAT,NAT:],REAL

for n, m being Nat holds

( (Partial_Sums_in_cod2 Rseq) . (n,m) = (Partial_Sums_in_cod1 (~ Rseq)) . (m,n) & (Partial_Sums_in_cod1 Rseq) . (n,m) = (Partial_Sums_in_cod2 (~ Rseq)) . (m,n) )

for n, m being Nat holds

( (Partial_Sums_in_cod2 Rseq) . (n,m) = (Partial_Sums_in_cod1 (~ Rseq)) . (m,n) & (Partial_Sums_in_cod1 Rseq) . (n,m) = (Partial_Sums_in_cod2 (~ Rseq)) . (m,n) )

proof end;

theorem :: DBLSEQ_2:10

for Rseq being Function of [:NAT,NAT:],REAL holds

( Partial_Sums_in_cod2 Rseq = ~ (Partial_Sums_in_cod1 (~ Rseq)) & Partial_Sums_in_cod2 (~ Rseq) = ~ (Partial_Sums_in_cod1 Rseq) & ~ (Partial_Sums_in_cod2 Rseq) = Partial_Sums_in_cod1 (~ Rseq) & ~ (Partial_Sums_in_cod2 (~ Rseq)) = Partial_Sums_in_cod1 Rseq )

( Partial_Sums_in_cod2 Rseq = ~ (Partial_Sums_in_cod1 (~ Rseq)) & Partial_Sums_in_cod2 (~ Rseq) = ~ (Partial_Sums_in_cod1 Rseq) & ~ (Partial_Sums_in_cod2 Rseq) = Partial_Sums_in_cod1 (~ Rseq) & ~ (Partial_Sums_in_cod2 (~ Rseq)) = Partial_Sums_in_cod1 Rseq )

proof end;

definition

let Rseq be Function of [:NAT,NAT:],REAL;

coherence

Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq) is Function of [:NAT,NAT:],REAL;

;

end;
func Partial_Sums Rseq -> Function of [:NAT,NAT:],REAL equals :: DBLSEQ_2:def 4

Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq);

correctness Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq);

coherence

Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq) is Function of [:NAT,NAT:],REAL;

;

:: deftheorem defines Partial_Sums DBLSEQ_2:def 4 :

for Rseq being Function of [:NAT,NAT:],REAL holds Partial_Sums Rseq = Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq);

for Rseq being Function of [:NAT,NAT:],REAL holds Partial_Sums Rseq = Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq);

theorem ThRS: :: DBLSEQ_2:11

for Rseq being Function of [:NAT,NAT:],REAL

for n, m being Nat holds

( (Partial_Sums Rseq) . ((n + 1),m) = ((Partial_Sums_in_cod2 Rseq) . ((n + 1),m)) + ((Partial_Sums Rseq) . (n,m)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 Rseq) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m)) )

for n, m being Nat holds

( (Partial_Sums Rseq) . ((n + 1),m) = ((Partial_Sums_in_cod2 Rseq) . ((n + 1),m)) + ((Partial_Sums Rseq) . (n,m)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 Rseq) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m)) )

proof end;

th103: for Rseq being Function of [:NAT,NAT:],REAL

for m, n being Nat holds (Partial_Sums Rseq) . (m,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (m,n)

proof end;

theorem th103a: :: DBLSEQ_2:12

for Rseq being Function of [:NAT,NAT:],REAL holds Partial_Sums Rseq = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)

proof end;

theorem thRS2: :: DBLSEQ_2:13

for Rseq being Function of [:NAT,NAT:],REAL

for n, m being Nat holds Rseq . ((n + 1),(m + 1)) = ((((Partial_Sums Rseq) . ((n + 1),(m + 1))) - ((Partial_Sums Rseq) . (n,(m + 1)))) - ((Partial_Sums Rseq) . ((n + 1),m))) + ((Partial_Sums Rseq) . (n,m))

for n, m being Nat holds Rseq . ((n + 1),(m + 1)) = ((((Partial_Sums Rseq) . ((n + 1),(m + 1))) - ((Partial_Sums Rseq) . (n,(m + 1)))) - ((Partial_Sums Rseq) . ((n + 1),m))) + ((Partial_Sums Rseq) . (n,m))

proof end;

theorem :: DBLSEQ_2:14

for Rseq being Function of [:NAT,NAT:],REAL

for n, m being Nat holds Rseq . ((n + 1),(m + 1)) = ((((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),(m + 1))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),m))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1)))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m))

for n, m being Nat holds Rseq . ((n + 1),(m + 1)) = ((((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),(m + 1))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),m))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1)))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m))

proof end;

theorem :: DBLSEQ_2:15

for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is P-convergent holds

( Rseq is P-convergent & P-lim Rseq = 0 )

( Rseq is P-convergent & P-lim Rseq = 0 )

proof end;

theorem lm74: :: DBLSEQ_2:16

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL holds Partial_Sums (Rseq1 + Rseq2) = (Partial_Sums Rseq1) + (Partial_Sums Rseq2)

proof end;

theorem :: DBLSEQ_2:17

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq1 is P-convergent & Partial_Sums Rseq2 is P-convergent holds

Partial_Sums (Rseq1 + Rseq2) is P-convergent

Partial_Sums (Rseq1 + Rseq2) is P-convergent

proof end;

theorem th100: :: DBLSEQ_2:18

for Rseq being Function of [:NAT,NAT:],REAL

for m, n being Element of NAT holds

( (Partial_Sums_in_cod1 Rseq) . (m,n) = (Partial_Sums (ProjMap2 (Rseq,n))) . m & (Partial_Sums_in_cod2 Rseq) . (m,n) = (Partial_Sums (ProjMap1 (Rseq,m))) . n )

for m, n being Element of NAT holds

( (Partial_Sums_in_cod1 Rseq) . (m,n) = (Partial_Sums (ProjMap2 (Rseq,n))) . m & (Partial_Sums_in_cod2 Rseq) . (m,n) = (Partial_Sums (ProjMap1 (Rseq,m))) . n )

proof end;

theorem th00: :: DBLSEQ_2:19

for Rseq being Function of [:NAT,NAT:],REAL holds

( ProjMap1 ((Partial_Sums Rseq),0) = ProjMap1 ((Partial_Sums_in_cod2 Rseq),0) & ProjMap2 ((Partial_Sums Rseq),0) = ProjMap2 ((Partial_Sums_in_cod1 Rseq),0) )

( ProjMap1 ((Partial_Sums Rseq),0) = ProjMap1 ((Partial_Sums_in_cod2 Rseq),0) & ProjMap2 ((Partial_Sums Rseq),0) = ProjMap2 ((Partial_Sums_in_cod1 Rseq),0) )

proof end;

theorem :: DBLSEQ_2:20

for C, D being non empty set

for F1, F2 being Function of [:C,D:],REAL

for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))

for F1, F2 being Function of [:C,D:],REAL

for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))

proof end;

theorem :: DBLSEQ_2:21

for C, D being non empty set

for F1, F2 being Function of [:C,D:],REAL

for d being Element of D holds ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))

for F1, F2 being Function of [:C,D:],REAL

for d being Element of D holds ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))

proof end;

theorem th01a: :: DBLSEQ_2:22

for Rseq being Function of [:NAT,NAT:],REAL holds

( Partial_Sums Rseq is convergent_in_cod1 iff Partial_Sums_in_cod1 Rseq is convergent_in_cod1 )

( Partial_Sums Rseq is convergent_in_cod1 iff Partial_Sums_in_cod1 Rseq is convergent_in_cod1 )

proof end;

theorem th01b: :: DBLSEQ_2:23

for Rseq being Function of [:NAT,NAT:],REAL holds

( Partial_Sums Rseq is convergent_in_cod2 iff Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )

( Partial_Sums Rseq is convergent_in_cod2 iff Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )

proof end;

theorem th02a: :: DBLSEQ_2:24

for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is convergent_in_cod1 holds

for k being Nat holds (lim_in_cod1 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod1 (Partial_Sums Rseq)) . k) + ((lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) . (k + 1))

for k being Nat holds (lim_in_cod1 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod1 (Partial_Sums Rseq)) . k) + ((lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) . (k + 1))

proof end;

theorem th02b: :: DBLSEQ_2:25

for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is convergent_in_cod2 holds

for k being Nat holds (lim_in_cod2 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod2 (Partial_Sums Rseq)) . k) + ((lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) . (k + 1))

for k being Nat holds (lim_in_cod2 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod2 (Partial_Sums Rseq)) . k) + ((lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) . (k + 1))

proof end;

theorem th03a: :: DBLSEQ_2:26

for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is convergent_in_cod1 holds

lim_in_cod1 (Partial_Sums Rseq) = Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 Rseq))

lim_in_cod1 (Partial_Sums Rseq) = Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 Rseq))

proof end;

theorem th03b: :: DBLSEQ_2:27

for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is convergent_in_cod2 holds

lim_in_cod2 (Partial_Sums Rseq) = Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 Rseq))

lim_in_cod2 (Partial_Sums Rseq) = Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 Rseq))

proof end;

theorem lm80: :: DBLSEQ_2:28

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds

( Partial_Sums_in_cod2 Rseq is nonnegative-yielding & Partial_Sums_in_cod1 Rseq is nonnegative-yielding )

( Partial_Sums_in_cod2 Rseq is nonnegative-yielding & Partial_Sums_in_cod1 Rseq is nonnegative-yielding )

proof end;

theorem th80a: :: DBLSEQ_2:29

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds

Partial_Sums Rseq is non-decreasing

Partial_Sums Rseq is non-decreasing

proof end;

theorem :: DBLSEQ_2:30

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds

( Partial_Sums Rseq is P-convergent iff ( Partial_Sums Rseq is bounded_below & Partial_Sums Rseq is bounded_above ) )

( Partial_Sums Rseq is P-convergent iff ( Partial_Sums Rseq is bounded_below & Partial_Sums Rseq is bounded_above ) )

proof end;

theorem lm84a: :: DBLSEQ_2:31

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) holds

for i, j being Nat holds

( (Partial_Sums_in_cod1 Rseq1) . (i,j) <= (Partial_Sums_in_cod1 Rseq2) . (i,j) & (Partial_Sums_in_cod2 Rseq1) . (i,j) <= (Partial_Sums_in_cod2 Rseq2) . (i,j) )

for i, j being Nat holds

( (Partial_Sums_in_cod1 Rseq1) . (i,j) <= (Partial_Sums_in_cod1 Rseq2) . (i,j) & (Partial_Sums_in_cod2 Rseq1) . (i,j) <= (Partial_Sums_in_cod2 Rseq2) . (i,j) )

proof end;

theorem lm84: :: DBLSEQ_2:32

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) holds

for i, j being Nat holds (Partial_Sums Rseq1) . (i,j) <= (Partial_Sums Rseq2) . (i,j)

for i, j being Nat holds (Partial_Sums Rseq1) . (i,j) <= (Partial_Sums Rseq2) . (i,j)

proof end;

theorem :: DBLSEQ_2:33

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) & Partial_Sums Rseq2 is P-convergent holds

Partial_Sums Rseq1 is P-convergent

Partial_Sums Rseq1 is P-convergent

proof end;

theorem th101: :: DBLSEQ_2:34

for rseq being Real_Sequence

for m being Nat st rseq is nonnegative holds

rseq . m <= (Partial_Sums rseq) . m

for m being Nat st rseq is nonnegative holds

rseq . m <= (Partial_Sums rseq) . m

proof end;

theorem :: DBLSEQ_2:35

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds

for m, n being Nat holds

( Rseq . (m,n) <= (Partial_Sums_in_cod1 Rseq) . (m,n) & Rseq . (m,n) <= (Partial_Sums_in_cod2 Rseq) . (m,n) )

for m, n being Nat holds

( Rseq . (m,n) <= (Partial_Sums_in_cod1 Rseq) . (m,n) & Rseq . (m,n) <= (Partial_Sums_in_cod2 Rseq) . (m,n) )

proof end;

theorem th1003: :: DBLSEQ_2:36

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds

( ( for i1, i2, j being Nat st i1 <= i2 holds

(Partial_Sums_in_cod1 Rseq) . (i1,j) <= (Partial_Sums_in_cod1 Rseq) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds

(Partial_Sums_in_cod2 Rseq) . (i,j1) <= (Partial_Sums_in_cod2 Rseq) . (i,j2) ) )

( ( for i1, i2, j being Nat st i1 <= i2 holds

(Partial_Sums_in_cod1 Rseq) . (i1,j) <= (Partial_Sums_in_cod1 Rseq) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds

(Partial_Sums_in_cod2 Rseq) . (i,j1) <= (Partial_Sums_in_cod2 Rseq) . (i,j2) ) )

proof end;

theorem th105: :: DBLSEQ_2:37

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds

( ( for i1, i2, j being Nat st i1 <= i2 holds

(Partial_Sums Rseq) . (i1,j) <= (Partial_Sums Rseq) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds

(Partial_Sums Rseq) . (i,j1) <= (Partial_Sums Rseq) . (i,j2) ) )

( ( for i1, i2, j being Nat st i1 <= i2 holds

(Partial_Sums Rseq) . (i1,j) <= (Partial_Sums Rseq) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds

(Partial_Sums Rseq) . (i,j1) <= (Partial_Sums Rseq) . (i,j2) ) )

proof end;

theorem :: DBLSEQ_2:38

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds

for i1, i2, j1, j2 being Nat st i1 <= i2 & j1 <= j2 holds

(Partial_Sums Rseq) . (i1,j1) <= (Partial_Sums Rseq) . (i2,j2)

for i1, i2, j1, j2 being Nat st i1 <= i2 & j1 <= j2 holds

(Partial_Sums Rseq) . (i1,j1) <= (Partial_Sums Rseq) . (i2,j2)

proof end;

theorem th1005: :: DBLSEQ_2:39

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds

for k being Element of NAT holds

( ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is V115() & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is V115() & ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative )

for k being Element of NAT holds

( ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is V115() & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is V115() & ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative )

proof end;

theorem th1006: :: DBLSEQ_2:40

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent holds

( Partial_Sums_in_cod1 Rseq is convergent_in_cod1 & Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )

( Partial_Sums_in_cod1 Rseq is convergent_in_cod1 & Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )

proof end;

theorem th1006a: :: DBLSEQ_2:41

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent holds

( Partial_Sums Rseq is convergent_in_cod1 & Partial_Sums Rseq is convergent_in_cod2 )

( Partial_Sums Rseq is convergent_in_cod1 & Partial_Sums Rseq is convergent_in_cod2 )

proof end;

theorem :: DBLSEQ_2:42

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent holds

( lim_in_cod1 (Partial_Sums_in_cod1 Rseq) is summable & lim_in_cod2 (Partial_Sums_in_cod2 Rseq) is summable )

( lim_in_cod1 (Partial_Sums_in_cod1 Rseq) is summable & lim_in_cod2 (Partial_Sums_in_cod2 Rseq) is summable )

proof end;

theorem :: DBLSEQ_2:43

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent holds

( P-lim (Partial_Sums Rseq) = Sum (lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) & P-lim (Partial_Sums Rseq) = Sum (lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) )

( P-lim (Partial_Sums Rseq) = Sum (lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) & P-lim (Partial_Sums Rseq) = Sum (lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) )

proof end;

theorem TMP6: :: DBLSEQ_2:44

for s1, s2 being Real_Sequence st s1 is nonnegative & s1,s2 are_fiberwise_equipotent holds

s2 is nonnegative

s2 is nonnegative

proof end;

theorem SH1: :: DBLSEQ_2:45

for X being non empty set

for s being sequence of X

for n being Nat holds dom (Shift ((s | (Segm n)),1)) = Seg n

for s being sequence of X

for n being Nat holds dom (Shift ((s | (Segm n)),1)) = Seg n

proof end;

registration

let X be non empty set ;

let s be sequence of X;

let n be Nat;

coherence

Shift ((s | (Segm n)),1) is FinSequence-like

end;
let s be sequence of X;

let n be Nat;

coherence

Shift ((s | (Segm n)),1) is FinSequence-like

proof end;

theorem SH2: :: DBLSEQ_2:46

for X being non empty set

for s being sequence of X

for n being Nat holds Shift ((s | (Segm n)),1) is FinSequence of X

for s being sequence of X

for n being Nat holds Shift ((s | (Segm n)),1) is FinSequence of X

proof end;

theorem SH3: :: DBLSEQ_2:47

for X being non empty set

for s being sequence of X

for n, m being Nat st m + 1 in dom (Shift ((s | (Segm n)),1)) holds

(Shift ((s | (Segm n)),1)) . (m + 1) = s . m

for s being sequence of X

for n, m being Nat st m + 1 in dom (Shift ((s | (Segm n)),1)) holds

(Shift ((s | (Segm n)),1)) . (m + 1) = s . m

proof end;

theorem SH4: :: DBLSEQ_2:48

for X being non empty set

for s being sequence of X holds

( Shift ((s | (Segm 0)),1) = {} & Shift ((s | (Segm 1)),1) = <*(s . 0)*> & Shift ((s | (Segm 2)),1) = <*(s . 0),(s . 1)*> & ( for n being Nat holds Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*> ) )

for s being sequence of X holds

( Shift ((s | (Segm 0)),1) = {} & Shift ((s | (Segm 1)),1) = <*(s . 0)*> & Shift ((s | (Segm 2)),1) = <*(s . 0),(s . 1)*> & ( for n being Nat holds Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*> ) )

proof end;

theorem SH5: :: DBLSEQ_2:49

for s being Real_Sequence

for n being Nat holds (Partial_Sums s) . n = Sum (Shift ((s | (Segm (n + 1))),1))

for n being Nat holds (Partial_Sums s) . n = Sum (Shift ((s | (Segm (n + 1))),1))

proof end;

theorem SH6: :: DBLSEQ_2:50

for X being non empty set

for s1, s2 being sequence of X

for n being Nat st s1,s2 are_fiberwise_equipotent holds

ex m being Nat ex fs2 being Subset of (Shift ((s2 | (Segm m)),1)) st Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent

for s1, s2 being sequence of X

for n being Nat st s1,s2 are_fiberwise_equipotent holds

ex m being Nat ex fs2 being Subset of (Shift ((s2 | (Segm m)),1)) st Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent

proof end;

theorem SH7: :: DBLSEQ_2:51

for X being non empty set

for fs being FinSequence of X

for fss being Subset of fs holds Seq fss,fss are_fiberwise_equipotent

for fs being FinSequence of X

for fss being Subset of fs holds Seq fss,fss are_fiberwise_equipotent

proof end;

theorem SH8: :: DBLSEQ_2:52

for s1, s2 being Real_Sequence

for n being Nat st s1,s2 are_fiberwise_equipotent & s1 is nonnegative holds

ex m being Nat st (Partial_Sums s1) . n <= (Partial_Sums s2) . m

for n being Nat st s1,s2 are_fiberwise_equipotent & s1 is nonnegative holds

ex m being Nat st (Partial_Sums s1) . n <= (Partial_Sums s2) . m

proof end;

theorem :: DBLSEQ_2:53

for s1, s2 being Real_Sequence st s1,s2 are_fiberwise_equipotent & s1 is nonnegative & s1 is summable holds

( s2 is summable & Sum s1 = Sum s2 )

( s2 is summable & Sum s1 = Sum s2 )

proof end;

theorem :: DBLSEQ_2:54

for D being non empty set

for Rseq being Function of [:NAT,NAT:],D

for n, m being Nat ex M being Matrix of n + 1,m + 1,D st

for i, j being Nat st i <= n & j <= m holds

Rseq . (i,j) = M * ((i + 1),(j + 1))

for Rseq being Function of [:NAT,NAT:],D

for n, m being Nat ex M being Matrix of n + 1,m + 1,D st

for i, j being Nat st i <= n & j <= m holds

Rseq . (i,j) = M * ((i + 1),(j + 1))

proof end;

theorem :: DBLSEQ_2:55

for n, m being Nat

for Rseq being Function of [:NAT,NAT:],REAL

for M being Matrix of n + 1,m + 1,REAL st ( for i, j being Nat st i <= n & j <= m holds

Rseq . (i,j) = M * ((i + 1),(j + 1)) ) holds

(Partial_Sums Rseq) . (n,m) = SumAll M

for Rseq being Function of [:NAT,NAT:],REAL

for M being Matrix of n + 1,m + 1,REAL st ( for i, j being Nat st i <= n & j <= m holds

Rseq . (i,j) = M * ((i + 1),(j + 1)) ) holds

(Partial_Sums Rseq) . (n,m) = SumAll M

proof end;