:: Cauchy Sequence of Complex Unitary Space
::  by Yasumasa Suzuki and Noboru Endou
::
:: Received March 18, 2004
:: Copyright (c) 2004-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, CSSPACE, PRE_TOPC, NAT_1, SEQ_1, COMSEQ_1, XCMPLX_0,
      REAL_1, SUBSET_1, SUPINF_2, SERIES_1, ARYTM_3, FUNCT_1, CARD_1, ARYTM_1,
      RELAT_1, COMPLEX1, SEQ_2, CARD_3, ORDINAL2, BHSP_3, XXREAL_0, NORMSP_1,
      XXREAL_2, FUNCOP_1, VALUED_1, POWER, NEWTON, VALUED_0, INT_1, METRIC_1,
      CSSPACE2;
 notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, XREAL_0,
      REAL_1, FUNCOP_1, VALUED_1, SEQ_1, SEQ_2, INT_1, NAT_1, NEWTON, SERIES_1,
      VALUED_0, PRE_TOPC, COMSEQ_1, STRUCT_0, RLVECT_1, VFUNCT_1, NORMSP_1,
      BHSP_4, POWER, COMSEQ_2, COMSEQ_3, NORMSP_0, CLVECT_1, CSSPACE, CLVECT_2,
      CSSPACE2;
 constructors REAL_1, COMSEQ_2, COMSEQ_3, BHSP_4, CLVECT_2, SEQ_2, RELSET_1,
      ABIAN, VFUNCT_1;
 registrations ORDINAL1, FUNCT_2, XXREAL_0, XREAL_0, INT_1, MEMBERED, STRUCT_0,
      VALUED_1, NUMBERS, VALUED_0, RELSET_1, FUNCOP_1, VFUNCT_1, XCMPLX_0,
      COMSEQ_2, NEWTON, NAT_1;
 requirements REAL, NUMERALS, SUBSET, ARITHM;


begin :: Cauchy sequence of complex unitary space

reserve X for ComplexUnitarySpace;
reserve g for Point of X;
reserve seq, seq1, seq2 for sequence of X;
reserve Rseq for Real_Sequence;
reserve Cseq,Cseq1,Cseq2 for Complex_Sequence;
reserve z,z1,z2 for Complex;
reserve r for Real;
reserve k,n,m for Nat;

theorem :: CLVECT_3:1
  Partial_Sums(seq1) + Partial_Sums(seq2) = Partial_Sums(seq1 + seq2);

theorem :: CLVECT_3:2
  Partial_Sums(seq1) - Partial_Sums(seq2) = Partial_Sums(seq1 - seq2);

theorem :: CLVECT_3:3
  Partial_Sums(z * seq) = z * Partial_Sums(seq);

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

theorem :: CLVECT_3:5
  z1 * Partial_Sums(seq1) + z2 * Partial_Sums(seq2) = Partial_Sums(z1*
  seq1 + z2*seq2);

definition
  let X, seq;
  attr seq is summable means
:: CLVECT_3:def 1

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

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

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

theorem :: CLVECT_3:8
  seq is summable implies z * seq is summable & Sum(z*seq) = z * Sum(seq );

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

theorem :: CLVECT_3:10
  for X being ComplexHilbertSpace, 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 :: CLVECT_3:11
  seq is summable implies Partial_Sums(seq) is bounded;

theorem :: CLVECT_3:12
  (for n holds seq1.n = seq.0) implies Partial_Sums(seq^\1) = (
  Partial_Sums(seq)^\1) - seq1;

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

theorem :: CLVECT_3: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
:: CLVECT_3:def 3
  Partial_Sums(seq).n;
end;

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

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

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

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

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

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

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

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

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

theorem :: CLVECT_3:23
  for X being ComplexHilbertSpace, 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 :: CLVECT_3:24
  for X being ComplexHilbertSpace, 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 Cseq, n;
  func Sum(Cseq,n) -> Complex equals
:: CLVECT_3:def 5
  Partial_Sums(Cseq).n;
end;

definition
  let Cseq, n,m;
  func Sum(Cseq,n,m) -> Complex equals
:: CLVECT_3:def 6
  Sum(Cseq,n) - Sum(Cseq,m);
end;

definition
  let X, seq;
  attr seq is absolutely_summable means
:: CLVECT_3:def 7

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

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

theorem :: CLVECT_3:26
  seq is absolutely_summable implies z * seq is absolutely_summable;

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

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

theorem :: CLVECT_3: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 :: CLVECT_3: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 :: CLVECT_3: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 :: CLVECT_3:32
  ( for n holds Rseq.n = n-root (||.seq.n.||) ) & Rseq is convergent &
  lim Rseq < 1 implies seq is absolutely_summable;

theorem :: CLVECT_3: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 :: CLVECT_3:34
  (for n holds Rseq.n = n-root (||.seq.||.n)) & Rseq is convergent & lim
  Rseq > 1 implies not seq is summable;

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

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

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

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

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

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

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

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

definition
  let X, seq, Cseq;
  func Cseq * seq -> sequence of X means
:: CLVECT_3:def 8

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

theorem :: CLVECT_3:43
  Cseq * (seq1 + seq2) = Cseq * seq1 + Cseq * seq2;

theorem :: CLVECT_3:44
  (Cseq1 + Cseq2) * seq = Cseq1 * seq + Cseq2 * seq;

theorem :: CLVECT_3:45
  (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq);

theorem :: CLVECT_3:46
  (z (#) Cseq) * seq = z * (Cseq * seq);

theorem :: CLVECT_3:47
  Cseq * (- seq) = (- Cseq) * seq;

theorem :: CLVECT_3:48
  Cseq is convergent & seq is convergent implies Cseq * seq is convergent;

theorem :: CLVECT_3:49
  Cseq is bounded & seq is bounded implies Cseq * seq is bounded;

theorem :: CLVECT_3:50
  Cseq is convergent & seq is convergent implies Cseq * seq is
  convergent & lim (Cseq * seq) = lim Cseq * lim seq;

definition
  let Cseq;
  attr Cseq is Cauchy means
:: CLVECT_3:def 9

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

theorem :: CLVECT_3:51
  for X being ComplexHilbertSpace, seq being sequence of X
  holds seq is Cauchy & Cseq is Cauchy implies Cseq *
  seq is Cauchy;

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

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

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