:: 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);