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