:: Double Series and Sums
::  by Noboru Endou
:: 
:: Received March 31, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_3, ARYTM_1,
      XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, VALUED_0, ORDINAL2, SEQ_2,
      ORDINAL1, XREAL_0, COMPLEX1, XXREAL_2, FINSET_1, MEMBERED, MESFUNC9,
      SEQ_1, VALUED_1, DBLSEQ_1, QC_LANG1, FUNCT_2, SERIES_1, DBLSEQ_2,
      FINSEQ_1, FUNCOP_1, SUPINF_2, CLASSES1, CARD_3, ORDINAL4, REAL_1,
      PARTFUN1, MATRIX_1, MCART_1, MATRIXC1, INCSP_1, TREES_1, PARTFUN3;
 notations VALUED_1, TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1,
      FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1, XXREAL_2, NUMBERS, BINOP_1,
      XCMPLX_0, FUNCOP_1, MEMBERED, COMPLEX1, XXREAL_0, XREAL_0, SEQ_1, NAT_1,
      FUNCT_4, MESFUNC9, FUNCT_2, SEQ_2, FINSET_1, DBLSEQ_1, SERIES_1,
      PARTFUN3, RINFSUP1, CLASSES1, FINSEQ_1, GLIB_003, RVSUM_1, MATRIX_0,
      MATRPROB;
 constructors TOPMETR, NAT_D, MESFUNC9, SEQ_2, COMSEQ_2, SEQ_4, DBLSEQ_1,
      SERIES_1, CLASSES1, PARTFUN3, GLIB_003, RVSUM_1, FUNCT_4, MATRPROB;
 registrations ORDINAL1, XXREAL_0, XREAL_0, XBOOLE_0, NUMBERS, XCMPLX_0,
      FINSET_1, MEMBERED, VALUED_0, XXREAL_2, RELSET_1, SEQ_4, FUNCT_1,
      FUNCT_2, VALUED_1, BINOP_2, NAT_1, CARD_1, RELAT_1, DBLSEQ_1, XTUPLE_0;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Double series and its convergence

 reserve Rseq, Rseq1, Rseq2 for Function of [:NAT,NAT:],REAL;

definition let f be Function of [:NAT,NAT:],REAL;
  redefine attr f is nonnegative-yielding means
:: DBLSEQ_2:def 1
    for i, j being Nat holds f.(i,j) >= 0;
end;

theorem :: DBLSEQ_2:1
  Rseq is non-decreasing implies
    (for m being Element of NAT holds ProjMap1(Rseq,m) is non-decreasing) &
    (for n being Element of NAT holds ProjMap2(Rseq,n) is non-decreasing);

theorem :: DBLSEQ_2:2
  Rseq is non-decreasing & Rseq is convergent_in_cod1 implies
   lim_in_cod1 Rseq is non-decreasing;

theorem :: DBLSEQ_2:3
  Rseq is non-decreasing & Rseq is convergent_in_cod2 implies
   lim_in_cod2 Rseq is non-decreasing;

theorem :: DBLSEQ_2:4
Rseq is non-decreasing & Rseq is P-convergent implies
  (for n,m being Nat holds Rseq.(n,m) <= P-lim Rseq);

theorem :: DBLSEQ_2:5
  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));

theorem :: DBLSEQ_2:6
for C,D,E being non empty set, f being Function of [:C,D:],E holds
 ex g being Function of [:D,C:],E st
  for d being Element of D, c being Element of C holds g.(d,c) = f.(c,d);

theorem :: DBLSEQ_2:7
  for C,D,E being set, f being Function of [:C,D:],E holds f = ~~f;

scheme :: DBLSEQ_2:sch 1
  RecEx2D1{C() -> non empty set, D() -> non empty set,
   H() -> Function of C(),D(), F(set,set,Nat) -> Element of D()}:
  ex g being Function of [:C(),NAT:],D() st
   for a being Element of C() holds
    g.(a,0) = H().a & for n being Nat holds g.(a,n+1) = F(g.(a,n), a, n);

scheme :: DBLSEQ_2:sch 2
  RecEx2D1R{C() -> non empty set,
   H() -> Function of C(),REAL, F(set,set,Nat) -> real number}:
  ex g being Function of [:C(),NAT:],REAL st
   for a being Element of C() holds
    g.(a,0) = H().a & for n being natural number holds
      g.(a,n+1) = F(g.(a,n), a, n);

scheme :: DBLSEQ_2:sch 3
  RecEx2D2{C() -> non empty set, D() -> non empty set,
   H() -> Function of C(),D(), F(set,set,Nat) -> Element of D()}:
  ex g being Function of [:NAT,C():],D() st
   for a being Element of C() holds
    g.(0,a) = H().a & for n being Nat holds
      g.(n+1,a) = F(g.(n,a), a, n);

scheme :: DBLSEQ_2:sch 4
  RecEx2D2R{C() -> non empty set,
   H() -> Function of C(),REAL, F(set,set,Nat) -> real number}:
  ex g being Function of [:NAT,C():],REAL st
   for a being Element of C() holds
    g.(0,a) = H().a & for n being Nat holds
      g.(n+1,a) = F(g.(n,a), a, n);

definition
  let Rseq be Function of [:NAT,NAT:],REAL;
  func Partial_Sums_in_cod2(Rseq) -> Function of [:NAT,NAT:],REAL means
:: 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);
end;

definition
 let Rseq be Function of [:NAT,NAT:],REAL;
 func Partial_Sums_in_cod1(Rseq) -> Function of [:NAT,NAT:],REAL means
:: 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);
end;

theorem :: DBLSEQ_2:8
  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);

theorem :: DBLSEQ_2:9
  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);

theorem :: DBLSEQ_2:10
   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;

definition
  let Rseq be Function of [:NAT,NAT:],REAL;
  func Partial_Sums(Rseq) -> Function of [:NAT,NAT:],REAL equals
:: DBLSEQ_2:def 4
    Partial_Sums_in_cod2( Partial_Sums_in_cod1 Rseq );
end;

theorem :: DBLSEQ_2:11
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);

theorem :: DBLSEQ_2:12
  Partial_Sums Rseq = Partial_Sums_in_cod1(Partial_Sums_in_cod2 Rseq);

theorem :: DBLSEQ_2:13
  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);

theorem :: DBLSEQ_2:14
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);

theorem :: DBLSEQ_2:15
  Partial_Sums Rseq is P-convergent implies
    Rseq is P-convergent & P-lim Rseq = 0;

theorem :: DBLSEQ_2:16
  Partial_Sums(Rseq1 + Rseq2) = Partial_Sums(Rseq1) + Partial_Sums(Rseq2);

theorem :: DBLSEQ_2:17
  Partial_Sums Rseq1 is P-convergent & Partial_Sums Rseq2 is P-convergent
    implies Partial_Sums(Rseq1+Rseq2) is P-convergent;

theorem :: DBLSEQ_2:18
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;

theorem :: DBLSEQ_2:19
   ProjMap1(Partial_Sums Rseq,0) = ProjMap1(Partial_Sums_in_cod2 Rseq,0)
 & ProjMap2(Partial_Sums Rseq,0) = ProjMap2(Partial_Sums_in_cod1 Rseq,0);

theorem :: DBLSEQ_2:20
  for C,D being non empty set, F1,F2 being Function of [:C,D:],REAL,
      c being Element of C holds
  ProjMap1(F1+F2,c) = ProjMap1(F1,c) + ProjMap1(F2,c);

theorem :: DBLSEQ_2:21
  for C,D being non empty set, F1,F2 being Function of [:C,D:],REAL,
      d being Element of D holds
    ProjMap2(F1+F2,d) = ProjMap2(F1,d) + ProjMap2(F2,d);

theorem :: DBLSEQ_2:22
  Partial_Sums Rseq is convergent_in_cod1 iff
    Partial_Sums_in_cod1 Rseq is convergent_in_cod1;

theorem :: DBLSEQ_2:23
  Partial_Sums Rseq is convergent_in_cod2 iff
    Partial_Sums_in_cod2 Rseq is convergent_in_cod2;

theorem :: DBLSEQ_2:24
  Partial_Sums Rseq is convergent_in_cod1 implies
  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);

theorem :: DBLSEQ_2:25
  Partial_Sums Rseq is convergent_in_cod2 implies
    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);

theorem :: DBLSEQ_2:26
  Partial_Sums Rseq is convergent_in_cod1 implies
    lim_in_cod1(Partial_Sums Rseq)
      = Partial_Sums(lim_in_cod1(Partial_Sums_in_cod1 Rseq));

theorem :: DBLSEQ_2:27
  Partial_Sums Rseq is convergent_in_cod2 implies
    lim_in_cod2(Partial_Sums Rseq)
      = Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2 Rseq));

begin :: Double series of non-negative double sequence

theorem :: DBLSEQ_2:28
  Rseq is nonnegative-yielding implies
    Partial_Sums_in_cod2 Rseq is nonnegative-yielding &
    Partial_Sums_in_cod1 Rseq is nonnegative-yielding;

theorem :: DBLSEQ_2:29
  Rseq is nonnegative-yielding implies
    Partial_Sums Rseq is non-decreasing;

theorem :: DBLSEQ_2:30
  Rseq is nonnegative-yielding implies
   (Partial_Sums Rseq is P-convergent
  iff Partial_Sums Rseq is bounded_below bounded_above);

theorem :: DBLSEQ_2:31
(for n,m being Nat holds Rseq1.(n,m) <= Rseq2.(n,m)) implies
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);

theorem :: DBLSEQ_2:32
  Rseq1 is nonnegative-yielding &
  (for n,m being Nat holds Rseq1.(n,m) <= Rseq2.(n,m)) implies
   for i,j being Nat holds
    (Partial_Sums Rseq1).(i,j) <= (Partial_Sums Rseq2).(i,j);

theorem :: DBLSEQ_2:33
  Rseq1 is nonnegative-yielding &
  (for n,m being Nat holds Rseq1.(n,m) <= Rseq2.(n,m))
& Partial_Sums Rseq2 is P-convergent
 implies Partial_Sums Rseq1 is P-convergent;

theorem :: DBLSEQ_2:34
  for rseq being Real_Sequence, m being Nat st
    rseq is nonnegative holds
      rseq.m <= (Partial_Sums rseq).m;

theorem :: DBLSEQ_2:35
  Rseq is nonnegative-yielding implies
   (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));

theorem :: DBLSEQ_2:36
  Rseq is nonnegative-yielding implies
  ( 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) )
;

theorem :: DBLSEQ_2:37
  Rseq is nonnegative-yielding implies
   ( for i1,i2,j be Nat st i1 <= i2 holds
      (Partial_Sums Rseq).(i1,j) <= (Partial_Sums Rseq).(i2,j) )
 & ( for i,j1,j2 be Nat st j1 <= j2 holds
      (Partial_Sums Rseq).(i,j1) <= (Partial_Sums Rseq).(i,j2) );

theorem :: DBLSEQ_2:38
  Rseq is nonnegative-yielding implies
  (for i1,i2,j1,j2 being Nat st i1 <= i2 & j1 <= j2 holds
      (Partial_Sums Rseq).(i1,j1) <= (Partial_Sums Rseq).(i2,j2));

theorem :: DBLSEQ_2:39
  Rseq is nonnegative-yielding implies
    for k being Element of NAT holds
   ProjMap2(Partial_Sums_in_cod1 Rseq,k) is non-decreasing
 & ProjMap1(Partial_Sums_in_cod2 Rseq,k) is non-decreasing
 & 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;

theorem :: DBLSEQ_2:40
  Rseq is nonnegative-yielding &
  Partial_Sums Rseq is P-convergent implies
   Partial_Sums_in_cod1 Rseq is convergent_in_cod1
 & Partial_Sums_in_cod2 Rseq is convergent_in_cod2;

theorem :: DBLSEQ_2:41
  Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent implies
    Partial_Sums Rseq is convergent_in_cod1
  & Partial_Sums Rseq is convergent_in_cod2;

theorem :: DBLSEQ_2:42
  Rseq is nonnegative-yielding &
  Partial_Sums Rseq is P-convergent implies
   lim_in_cod1(Partial_Sums_in_cod1 Rseq) is summable
 & lim_in_cod2(Partial_Sums_in_cod2 Rseq) is summable;

theorem :: DBLSEQ_2:43
  Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent implies
    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));

begin :: Summability for rearrangements of non-negative real sequence

theorem :: DBLSEQ_2:44
  for s1,s2 be Real_Sequence
    st s1 is nonnegative & s1,s2 are_fiberwise_equipotent
  holds s2 is nonnegative;

theorem :: DBLSEQ_2:45
  for X being non empty set, s being sequence of X, n being Nat
    holds dom(Shift(s|(Segm n),1)) = Seg n;

registration
  let X be non empty set;
  let s be sequence of X;
  let n be Nat;
  cluster Shift(s|(Segm n),1) -> FinSequence-like;
end;

theorem :: DBLSEQ_2:46
  for X being non empty set, s being sequence of X, n being Nat
    holds Shift(s|(Segm n),1) is FinSequence of X;

theorem :: DBLSEQ_2:47
for X being non empty set, s being sequence of X, n,m being Nat
  st m+1 in dom Shift(s|Segm n, 1) holds Shift(s|Segm n,1).(m+1) = s.m;

theorem :: DBLSEQ_2:48
  for X being non empty set, 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*>;

theorem :: DBLSEQ_2:49
  for s being Real_Sequence, n being Nat holds
    (Partial_Sums s).n = Sum(Shift(s|Segm(n+1),1));

theorem :: DBLSEQ_2:50
for X being non empty set, s1,s2 being sequence of X, n being Nat
 st s1,s2 are_fiberwise_equipotent holds
  ex m being Nat, fs2 being Subset of Shift(s2|Segm m,1) st
   Shift(s1|Segm(n+1),1),fs2 are_fiberwise_equipotent;

theorem :: DBLSEQ_2:51
  for X being non empty set, fs being FinSequence of X,
      fss being Subset of fs
  holds Seq fss,fss are_fiberwise_equipotent;

theorem :: DBLSEQ_2:52
  for s1,s2 being Real_Sequence, n being Nat
    st s1,s2 are_fiberwise_equipotent & s1 is nonnegative
   ex m being Nat st (Partial_Sums s1).n <= (Partial_Sums s2).m;

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;

begin :: Basic relations between double sequence and matrix

theorem :: DBLSEQ_2:54
for D being non empty set, Rseq being Function of [:NAT,NAT:],D,
    n,m being Nat holds
 ex M be 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);

theorem :: DBLSEQ_2:55
  for n,m being Nat, Rseq being Function of [:NAT,NAT:],REAL,
      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;