The Mizar abstract of BHSP

Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users
The abstract of the Mizar article:: Series in Banach and Hilbert Spaces
by
Elzbieta Kraszewska, and
Jan Popiolek
Received April 1, 1992
MML identifier: BHSP_4
[ Mizar article, MML identifier index ]
environ

 vocabulary BHSP_1, PRE_TOPC, NORMSP_1, SEQ_1, RLVECT_1, FUNCT_1, SERIES_1,
      ARYTM_1, SUPINF_2, SEQ_2, ORDINAL2, SEQM_3, BHSP_3, LATTICES, ABSVALUE,
      ARYTM_3, POWER, PROB_1, INT_1, METRIC_1, ARYTM, GROUP_1;
 notation SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, STRUCT_0, REAL_1,
      NAT_1, FUNCT_2, SEQ_1, SEQ_2, SEQM_3, SERIES_1, ABSVALUE, PRE_TOPC,
      RLVECT_1, NORMSP_1, BHSP_1, BHSP_2, BHSP_3, PREPOWER, POWER, INT_1;
 constructors REAL_1, NAT_1, SEQ_2, SERIES_1, BHSP_2, BHSP_3, PREPOWER,
      PARTFUN1, MEMBERED, XBOOLE_0;
 clusters INT_1, STRUCT_0, XREAL_0, SEQ_1, RELSET_1, MEMBERED, ZFMISC_1,
      XBOOLE_0, ORDINAL2;
 requirements NUMERALS, REAL, SUBSET, ARITHM;


begin

 reserve X for RealUnitarySpace;
 reserve g for Point of X;
 reserve a, b, r, M2 for Real;
 reserve seq, seq1, seq2 for sequence of X;
 reserve Rseq,Rseq1,Rseq2 for Real_Sequence;
 reserve k, n, m, m1, m2 for Nat;

scheme Rec_Func_Ex_RUS{ X() -> RealUnitarySpace,
                     z() -> Point of X(),
                     G(Nat, Point of X()) -> Point of X()}:
ex f being Function of NAT, the carrier of X() st
f.0 = z() & for n being Element of NAT,
x being Point of X() st x = f.n holds f.(n + 1) = G(n,x);

definition
          let X;
          let seq;
          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
    Partial_Sums(seq1) + Partial_Sums(seq2) =
    Partial_Sums(seq1 + seq2);

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

theorem :: BHSP_4:3
    Partial_Sums(a * seq) = a * Partial_Sums(seq);

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;
           let 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
     X is_Hilbert_space implies
     ( 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;

canceled;

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

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

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

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

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

theorem :: BHSP_4:21
        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;

canceled;

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

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

theorem :: BHSP_4:25
     X is_Hilbert_space implies
     ( 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:26
       X is_Hilbert_space implies
     ( 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 Rseq, n;
          func Sum(Rseq, n) -> Real equals
:: BHSP_4:def 6
    Partial_Sums(Rseq).n;
end;

definition
          let Rseq, n,m;
          func Sum(Rseq, n, m) -> Real equals
:: BHSP_4:def 7
    Sum(Rseq, n) - Sum(Rseq, m);
end;

definition
          let X, seq;
          attr seq is absolutely_summable means
:: BHSP_4:def 8
 ||.seq.|| is summable;
end;

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: BHSP_4:44
       X is_Hilbert_space implies
     ( seq is absolutely_summable implies seq is summable );

definition
          let X, seq, Rseq;
          func Rseq * seq -> sequence of X means
:: BHSP_4:def 9
    for n holds it.n = Rseq.n * seq.n;
end;

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

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

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

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

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

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

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

theorem :: BHSP_4:52
       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 10
   for r st r > 0 ex k st for n, m st ( n >= k & m >= k )
          holds abs((Rseq.n - Rseq.m)) < r;
  synonym Rseq is_Cauchy_sequence;
end;

theorem :: BHSP_4:53
        X is_Hilbert_space implies
      ( seq is_Cauchy_sequence & Rseq is_Cauchy_sequence implies
      Rseq * seq is_Cauchy_sequence );

theorem :: BHSP_4:54
     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:55
     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:56
       for n holds
     Sum(Rseq * seq, n+1) =
     (Rseq * Partial_Sums(seq)).(n+1) -
     Sum((Rseq^\1 - Rseq) * Partial_Sums(seq), n);
The abstract of the Mizar article:

Series in Banach and Hilbert Spaces
