:: Series in Banach and Hilbert Spaces
::  by El\.zbieta Kraszewska and Jan Popio{\l}ek
::
:: Received April 1, 1992
:: Copyright (c) 1992-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, REAL_1, SEQ_1, SUBSET_1, BHSP_1, SUPINF_2, XBOOLE_0,
      ALGSTR_0, NAT_1, SERIES_1, FUNCT_1, CARD_1, ARYTM_3, PRE_TOPC, STRUCT_0,
      RLVECT_1, ARYTM_1, RELAT_1, SEQ_2, CARD_3, ORDINAL2, BHSP_3, XXREAL_0,
      NORMSP_1, XXREAL_2, FUNCOP_1, COMPLEX1, VALUED_1, POWER, NEWTON,
      VALUED_0, INT_1, METRIC_1, RSSPACE2;
 notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, ALGSTR_0,
      REAL_1, INT_1, NAT_1, FUNCT_2, FUNCOP_1, VALUED_1, SEQ_1, SEQ_2,
      SERIES_1, VALUED_0, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_1,
      BHSP_1, BHSP_2, BHSP_3, RSSPACE2, NEWTON, POWER, XXREAL_0;
 constructors REAL_1, SEQ_2, NEWTON, SERIES_1, BHSP_2, BHSP_3, RELSET_1, ABIAN,
      BINOP_2, VFUNCT_1, COMSEQ_2;
 registrations ORDINAL1, RELSET_1, XREAL_0, INT_1, MEMBERED, STRUCT_0,
      RLVECT_1, VALUED_0, VALUED_1, FUNCT_2, NUMBERS, FUNCOP_1, VFUNCT_1,
      BHSP_2, BHSP_3, NEWTON, NAT_1;
 requirements NUMERALS, REAL, SUBSET, ARITHM;


begin

reserve a, b, r, M2 for Real;
reserve Rseq,Rseq1,Rseq2 for Real_Sequence;
reserve k, n, m, m1, m2 for Nat;

definition
  let X be non empty addLoopStr;
  let seq be sequence of X;
  func Partial_Sums(seq) -> sequence of X means
:: BHSP_4:def 1

  it.0 = seq.0 & for n holds it.(n + 1) = it.n + seq.(n + 1);
end;

theorem :: BHSP_4:1
  for X being Abelian add-associative non empty addLoopStr, seq1,
  seq2 being sequence of X holds Partial_Sums(seq1) + Partial_Sums(seq2) =
  Partial_Sums(seq1 + seq2);

theorem :: BHSP_4:2
  for X being Abelian add-associative right_zeroed
  right_complementable non empty addLoopStr, seq1, seq2 being sequence of X
  holds Partial_Sums(seq1) - Partial_Sums(seq2) = Partial_Sums(seq1 - seq2);

theorem :: BHSP_4:3
  for X being vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty RLSStruct, seq being
  sequence of X holds Partial_Sums(a * seq) = a * Partial_Sums(seq);

reserve X for RealUnitarySpace;
reserve g for Point of X;
reserve seq, seq1, seq2 for sequence of X;

theorem :: BHSP_4:4
  Partial_Sums(- seq) = - Partial_Sums(seq);

theorem :: BHSP_4:5
  a * Partial_Sums(seq1) + b * Partial_Sums(seq2) = Partial_Sums(a *
  seq1 + b * seq2);

definition
  let X, seq;
  attr seq is summable means
:: BHSP_4:def 2

  Partial_Sums(seq) is convergent;
  func Sum(seq) -> Point of X equals
:: BHSP_4:def 3
  lim Partial_Sums(seq);
end;

theorem :: BHSP_4:6
  seq1 is summable & seq2 is summable implies seq1 + seq2 is summable &
  Sum(seq1 + seq2) = Sum(seq1) + Sum(seq2);

theorem :: BHSP_4:7
  seq1 is summable & seq2 is summable implies seq1 - seq2 is summable &
  Sum(seq1 - seq2) = Sum(seq1) - Sum(seq2);

theorem :: BHSP_4:8
  seq is summable implies a * seq is summable & Sum(a * seq) = a * Sum( seq);

theorem :: BHSP_4:9
  seq is summable implies seq is convergent & lim seq = 0.X;

theorem :: BHSP_4:10
  for X being RealHilbertSpace, seq being sequence of X
   holds seq is summable iff for r st r > 0 ex k
st for n, m st n >= k & m >= k holds ||.(Partial_Sums(seq)).n - (Partial_Sums(
  seq)).m.|| < r;

theorem :: BHSP_4:11
  seq is summable implies Partial_Sums(seq) is bounded;

theorem :: BHSP_4:12
  for seq, seq1 st for n holds seq1.n = seq.0 holds Partial_Sums(
  seq^\1) = (Partial_Sums(seq)^\1) - seq1;

theorem :: BHSP_4:13
  seq is summable implies for k holds seq^\k is summable;

theorem :: BHSP_4:14
  (ex k st seq^\k is summable) implies seq is summable;

definition
  let X, seq, n;
  func Sum(seq,n) -> Point of X equals
:: BHSP_4:def 4
  Partial_Sums(seq).n;
end;

theorem :: BHSP_4:15
  Sum(seq, 0) = seq.0;

theorem :: BHSP_4:16
  Sum(seq, 1) = Sum(seq, 0) + seq.1;

theorem :: BHSP_4:17
  Sum(seq, 1) = seq.0 + seq.1;

theorem :: BHSP_4:18
  Sum(seq, n + 1) = Sum(seq, n) + seq.(n + 1);

theorem :: BHSP_4:19
  seq.(n + 1) = Sum(seq, n + 1) - Sum(seq, n);

theorem :: BHSP_4:20
  seq.1 = Sum(seq, 1) - Sum(seq, 0);

definition
  let X, seq, n, m;
  func Sum(seq, n, m) -> Point of X equals
:: BHSP_4:def 5
  Sum(seq, n) - Sum(seq, m);
end;

theorem :: BHSP_4:21
  Sum(seq, 1, 0) = seq.1;

theorem :: BHSP_4:22
  Sum(seq, n+1, n) = seq.(n+1);

theorem :: BHSP_4:23
  for X being RealHilbertSpace, seq being sequence of X
   holds seq is summable iff for r st r > 0 ex k
  st for n, m st n >= k & m >= k holds ||.Sum(seq, n) - Sum(seq, m).|| < r;

theorem :: BHSP_4:24
  for X being RealHilbertSpace, seq being sequence of X
   holds seq is summable iff for r st r > 0 ex k st for
  n, m st n >= k & m >= k holds ||.Sum(seq, n, m).|| < r;

definition
  let X, seq;

  attr seq is absolutely_summable means
:: BHSP_4:def 6

  ||.seq.|| is summable;
end;

theorem :: BHSP_4:25
  seq1 is absolutely_summable & seq2 is absolutely_summable implies seq1
  + seq2 is absolutely_summable;

theorem :: BHSP_4:26
  seq is absolutely_summable implies a * seq is absolutely_summable;

theorem :: BHSP_4:27
  ( for n being Nat holds ||.seq.||.n <= Rseq.n ) &
    Rseq is summable implies seq
  is absolutely_summable;

theorem :: BHSP_4:28
  ( for n being Nat holds seq.n <> 0.X &
   Rseq.n = ||.seq.(n+1).||/||.seq.n.|| ) &
  Rseq is convergent & lim Rseq < 1 implies seq is absolutely_summable;

theorem :: BHSP_4:29
  r > 0 & ( ex m st for n st n >= m holds ||.seq.n.|| >= r)
  implies not seq is convergent or lim seq <> 0.X;

theorem :: BHSP_4:30
  ( for n holds seq.n <> 0.X ) & ( ex m st for n st n >= m holds
  ||.seq.(n+1).||/||.seq.n.|| >= 1 ) implies not seq is summable;

theorem :: BHSP_4:31
  (for n holds seq.n <> 0.X) & (for n holds Rseq.n = ||.seq.(n+1).||/||.
  seq.n.||) & Rseq is convergent & lim Rseq > 1 implies not seq is summable;

theorem :: BHSP_4:32
  ( for n holds Rseq.n = n-root (||.seq.n.||) ) & Rseq is convergent &
  lim Rseq < 1 implies seq is absolutely_summable;

theorem :: BHSP_4:33
  (for n holds Rseq.n = n-root (||.seq.||.n)) & (ex m st for n st n >= m
  holds Rseq.n >= 1) implies not seq is summable;

theorem :: BHSP_4:34
  (for n holds Rseq.n = n-root (||.seq.||.n)) & Rseq is convergent & lim
  Rseq > 1 implies not seq is summable;

theorem :: BHSP_4:35
  Partial_Sums(||.seq.||) is non-decreasing;

theorem :: BHSP_4:36
  for n holds Partial_Sums(||.seq.||).n >= 0;

theorem :: BHSP_4:37
  for n holds ||.Partial_Sums(seq).n.|| <= Partial_Sums(||.seq.||) .n;

theorem :: BHSP_4:38
  for n holds ||.Sum(seq, n).|| <= Sum(||.seq.||, n);

theorem :: BHSP_4:39
  for n, m holds ||.Partial_Sums(seq).m - Partial_Sums(seq).n.||
  <= |.Partial_Sums(||.seq.||).m - Partial_Sums(||.seq.||).n.|;

theorem :: BHSP_4:40
  for n, m holds ||.Sum(seq, m) - Sum(seq, n).|| <= |.Sum(||.seq.||, m
  ) - Sum(||.seq.||, n).|;

theorem :: BHSP_4:41
  for n, m holds ||.Sum(seq, m, n).|| <= |.Sum(||.seq.||, m, n).|;

theorem :: BHSP_4:42
  for X being RealHilbertSpace, seq being sequence of X
   holds seq is absolutely_summable implies seq is
  summable;

definition
  let X, seq, Rseq;
  func Rseq * seq -> sequence of X means
:: BHSP_4:def 7

  for n holds it.n = Rseq.n * seq.n;
end;

theorem :: BHSP_4:43
  Rseq * (seq1 + seq2) = Rseq * seq1 + Rseq * seq2;

theorem :: BHSP_4:44
  (Rseq1 + Rseq2) * seq = Rseq1 * seq + Rseq2 * seq;

theorem :: BHSP_4:45
  (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq);

theorem :: BHSP_4:46
  (a (#) Rseq) * seq = a * (Rseq * seq);

theorem :: BHSP_4:47
  Rseq * (- seq) = (- Rseq) * seq;

theorem :: BHSP_4:48
  Rseq is convergent & seq is convergent implies Rseq * seq is convergent;

theorem :: BHSP_4:49
  Rseq is bounded & seq is bounded implies Rseq * seq is bounded;

theorem :: BHSP_4:50
  Rseq is convergent & seq is convergent implies Rseq * seq is
  convergent & lim (Rseq * seq) = lim Rseq * lim seq;

definition
  let Rseq;
  attr Rseq is Cauchy means
:: BHSP_4:def 8

  for r st r > 0 ex k st for n, m st n >= k
  & m >= k holds |.(Rseq.n - Rseq.m).| < r;
end;

theorem :: BHSP_4:51
  for X being RealHilbertSpace, seq being sequence of X
   holds seq is Cauchy & Rseq is Cauchy implies Rseq *
  seq is Cauchy;

theorem :: BHSP_4:52
  for n holds Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n
  = Partial_Sums(Rseq * seq).(n+1) - (Rseq * Partial_Sums(seq)).(n+1);

theorem :: BHSP_4:53
  for n holds Partial_Sums(Rseq * seq).(n+1) = (Rseq *
Partial_Sums(seq)).(n+1) - Partial_Sums((Rseq^\1 - Rseq) * Partial_Sums(seq)).n
;

theorem :: BHSP_4:54
  for n holds Sum(Rseq * seq, n+1) = (Rseq * Partial_Sums(seq)).(n+1) -
  Sum((Rseq^\1 - Rseq) * Partial_Sums(seq), n);