:: Convergent Sequences in Complex Unitary Space :: by Noboru Endou :: :: Received February 10, 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, XCMPLX_0, REAL_1, NAT_1, SUBSET_1, ORDINAL2, SUPINF_2, SEQ_2, XXREAL_0, CARD_1, METRIC_1, FUNCT_1, ARYTM_3, ARYTM_1, RELAT_1, COMPLEX1, NORMSP_1, SEQ_1, TARSKI, STRUCT_0, XBOOLE_0, BHSP_3, XXREAL_2, VALUED_0, REWRITE1; notations TARSKI, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, NAT_1, SEQ_1, VALUED_0, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_1, BHSP_1, SEQ_2, CLVECT_1, CSSPACE, RECDEF_1; constructors REAL_1, COMPLEX1, SEQ_2, BHSP_3, CSSPACE, VALUED_1, RECDEF_1, RELSET_1, VFUNCT_1, COMSEQ_2; registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, MEMBERED, STRUCT_0, VALUED_0, VFUNCT_1, FUNCT_2; requirements SUBSET, REAL, NUMERALS, ARITHM; begin :: Convergence in complex unitary space reserve X for ComplexUnitarySpace; reserve x, y, w, g, g1, g2 for Point of X; reserve z for Complex; reserve p, q, r, M, M1, M2 for Real; reserve seq, seq1, seq2, seq3 for sequence of X; reserve k,n,m for Nat; reserve Nseq for increasing sequence of NAT; definition let X, seq; attr seq is convergent means :: CLVECT_2:def 1 ex g st for r st r > 0 ex m st for n st n >= m holds dist(seq.n, g) < r; end; theorem :: CLVECT_2:1 seq is constant implies seq is convergent; theorem :: CLVECT_2:2 seq1 is convergent & (ex k st for n st k <= n holds seq2.n = seq1 .n) implies seq2 is convergent; theorem :: CLVECT_2:3 seq1 is convergent & seq2 is convergent implies seq1 + seq2 is convergent; theorem :: CLVECT_2:4 seq1 is convergent & seq2 is convergent implies seq1 - seq2 is convergent; theorem :: CLVECT_2:5 seq is convergent implies z * seq is convergent; theorem :: CLVECT_2:6 seq is convergent implies - seq is convergent; theorem :: CLVECT_2:7 seq is convergent implies seq + x is convergent; theorem :: CLVECT_2:8 seq is convergent implies seq - x is convergent; theorem :: CLVECT_2:9 seq is convergent iff ex g st for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r; definition let X, seq; assume seq is convergent; func lim seq -> Point of X means :: CLVECT_2:def 2 for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , it) < r; end; theorem :: CLVECT_2:10 seq is constant & x in rng seq implies lim seq = x; theorem :: CLVECT_2:11 seq is constant & (ex n st seq.n = x) implies lim seq = x; theorem :: CLVECT_2:12 seq1 is convergent & (ex k st for n st n >= k holds seq2.n = seq1.n) implies lim seq1 = lim seq2; theorem :: CLVECT_2:13 seq1 is convergent & seq2 is convergent implies lim (seq1 + seq2 ) = (lim seq1) + (lim seq2); theorem :: CLVECT_2:14 seq1 is convergent & seq2 is convergent implies lim (seq1 - seq2 ) = (lim seq1) - (lim seq2); theorem :: CLVECT_2:15 seq is convergent implies lim (z * seq) = z * (lim seq); theorem :: CLVECT_2:16 seq is convergent implies lim (- seq) = - (lim seq); theorem :: CLVECT_2:17 seq is convergent implies lim (seq + x) = (lim seq) + x; theorem :: CLVECT_2:18 seq is convergent implies lim (seq - x) = (lim seq) - x; theorem :: CLVECT_2:19 seq is convergent implies (lim seq = g iff for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r); definition let X, seq; func ||.seq.|| -> Real_Sequence means :: CLVECT_2:def 3 for n holds it.n =||.(seq.n).||; end; theorem :: CLVECT_2:20 seq is convergent implies ||.seq.|| is convergent; theorem :: CLVECT_2:21 seq is convergent & lim seq = g implies ||.seq.|| is convergent & lim ||.seq.|| = ||.g.||; theorem :: CLVECT_2:22 seq is convergent & lim seq = g implies ||.seq - g.|| is convergent & lim ||.seq - g.|| = 0; definition let X, seq, x; func dist(seq, x) -> Real_Sequence means :: CLVECT_2:def 4 for n holds it.n =dist((seq. n) , x); end; theorem :: CLVECT_2:23 seq is convergent & lim seq = g implies dist(seq,g) is convergent; theorem :: CLVECT_2:24 seq is convergent & lim seq = g implies dist(seq,g) is convergent & lim dist(seq,g) = 0; theorem :: CLVECT_2:25 seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ||.seq1 + seq2.|| is convergent & lim ||.seq1 + seq2.|| = ||.g1 + g2 .||; theorem :: CLVECT_2:26 seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ||.(seq1 + seq2) - (g1 + g2).|| is convergent & lim ||.(seq1 + seq2) - (g1 + g2).|| = 0; theorem :: CLVECT_2:27 seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ||.seq1 - seq2.|| is convergent & lim ||.seq1 - seq2.|| = ||.g1 - g2 .||; theorem :: CLVECT_2:28 seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ||.(seq1 - seq2) - (g1 - g2).|| is convergent & lim ||.(seq1 - seq2) - (g1 - g2).|| = 0; theorem :: CLVECT_2:29 seq is convergent & lim seq = g implies ||.z * seq.|| is convergent & lim ||.z * seq.|| = ||.z * g.||; theorem :: CLVECT_2:30 seq is convergent & lim seq = g implies ||.(z * seq) - (z * g).|| is convergent & lim ||.(z * seq) - (z * g).|| = 0; theorem :: CLVECT_2:31 seq is convergent & lim seq = g implies ||.- seq.|| is convergent & lim ||.- seq.|| = ||.- g.||; theorem :: CLVECT_2:32 seq is convergent & lim seq = g implies ||.(- seq) - (- g).|| is convergent & lim ||.(- seq) - (- g).|| = 0; theorem :: CLVECT_2:33 seq is convergent & lim seq = g implies ||.(seq + x) - (g + x) .|| is convergent & lim ||.(seq + x) - (g + x).|| = 0; theorem :: CLVECT_2:34 seq is convergent & lim seq = g implies ||.seq - x.|| is convergent & lim ||.seq - x.|| = ||.g - x.||; theorem :: CLVECT_2:35 seq is convergent & lim seq = g implies ||.(seq - x) - (g - x).|| is convergent & lim ||.(seq - x) - (g - x).|| = 0; theorem :: CLVECT_2:36 seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies dist((seq1 + seq2) , (g1 + g2)) is convergent & lim dist((seq1 + seq2) , (g1 + g2)) = 0; theorem :: CLVECT_2:37 seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies dist((seq1 - seq2) , (g1 - g2)) is convergent & lim dist((seq1 - seq2) , (g1 - g2)) = 0; theorem :: CLVECT_2:38 seq is convergent & lim seq = g implies dist((z * seq) , (z * g)) is convergent & lim dist((z * seq) , (z * g)) = 0; theorem :: CLVECT_2:39 seq is convergent & lim seq = g implies dist((seq + x) , (g + x)) is convergent & lim dist((seq + x) , (g + x)) = 0; definition let X, x, r; func Ball(x,r) -> Subset of X equals :: CLVECT_2:def 5 {y where y is Point of X : ||.x - y.|| < r}; func cl_Ball(x,r) -> Subset of X equals :: CLVECT_2:def 6 {y where y is Point of X : ||.x - y .|| <= r}; func Sphere(x,r) -> Subset of X equals :: CLVECT_2:def 7 {y where y is Point of X : ||.x - y .|| = r}; end; theorem :: CLVECT_2:40 w in Ball(x,r) iff ||.x - w.|| < r; theorem :: CLVECT_2:41 w in Ball(x,r) iff dist(x,w) < r; theorem :: CLVECT_2:42 r > 0 implies x in Ball(x,r); theorem :: CLVECT_2:43 y in Ball(x,r) & w in Ball(x,r) implies dist(y,w) < 2 * r; theorem :: CLVECT_2:44 y in Ball(x,r) implies y - w in Ball(x - w,r); theorem :: CLVECT_2:45 y in Ball(x,r) implies (y - x) in Ball (0.(X),r); theorem :: CLVECT_2:46 y in Ball(x,r) & r <= q implies y in Ball(x,q); theorem :: CLVECT_2:47 w in cl_Ball(x,r) iff ||.x - w.|| <= r; theorem :: CLVECT_2:48 w in cl_Ball(x,r) iff dist(x,w) <= r; theorem :: CLVECT_2:49 r >= 0 implies x in cl_Ball(x,r); theorem :: CLVECT_2:50 y in Ball(x,r) implies y in cl_Ball(x,r); theorem :: CLVECT_2:51 w in Sphere(x,r) iff ||.x - w.|| = r; theorem :: CLVECT_2:52 w in Sphere(x,r) iff dist(x,w) = r; theorem :: CLVECT_2:53 y in Sphere(x,r) implies y in cl_Ball(x,r); theorem :: CLVECT_2:54 Ball(x,r) c= cl_Ball(x,r); theorem :: CLVECT_2:55 Sphere(x,r) c= cl_Ball(x,r); theorem :: CLVECT_2:56 Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r); begin definition let X; let seq; attr seq is Cauchy means :: CLVECT_2:def 8 for r st r > 0 ex k st for n, m st n >= k & m >= k holds dist((seq.n), (seq.m)) < r; end; theorem :: CLVECT_2:57 seq is constant implies seq is Cauchy; theorem :: CLVECT_2:58 seq is Cauchy iff for r st r > 0 ex k st for n, m st n >= k & m >= k holds ||.(seq.n) - (seq.m).|| < r; theorem :: CLVECT_2:59 seq1 is Cauchy & seq2 is Cauchy implies seq1 + seq2 is Cauchy; theorem :: CLVECT_2:60 seq1 is Cauchy & seq2 is Cauchy implies seq1 - seq2 is Cauchy; theorem :: CLVECT_2:61 seq is Cauchy implies z * seq is Cauchy; theorem :: CLVECT_2:62 seq is Cauchy implies - seq is Cauchy; theorem :: CLVECT_2:63 seq is Cauchy implies seq + x is Cauchy; theorem :: CLVECT_2:64 seq is Cauchy implies seq - x is Cauchy; theorem :: CLVECT_2:65 seq is convergent implies seq is Cauchy; definition let X; let seq1, seq2; pred seq1 is_compared_to seq2 means :: CLVECT_2:def 9 for r st r > 0 ex m st for n st n >= m holds dist(seq1.n, seq2.n) < r; end; theorem :: CLVECT_2:66 seq is_compared_to seq; theorem :: CLVECT_2:67 seq1 is_compared_to seq2 implies seq2 is_compared_to seq1; definition let X; let seq1, seq2; redefine pred seq1 is_compared_to seq2; reflexivity; symmetry; end; theorem :: CLVECT_2:68 seq1 is_compared_to seq2 & seq2 is_compared_to seq3 implies seq1 is_compared_to seq3; theorem :: CLVECT_2:69 seq1 is_compared_to seq2 iff for r st r > 0 ex m st for n st n >= m holds ||.(seq1.n) - (seq2.n).|| < r; theorem :: CLVECT_2:70 ( ex k st for n st n >= k holds seq1.n = seq2.n ) implies seq1 is_compared_to seq2; theorem :: CLVECT_2:71 seq1 is Cauchy & seq1 is_compared_to seq2 implies seq2 is Cauchy; theorem :: CLVECT_2:72 seq1 is convergent & seq1 is_compared_to seq2 implies seq2 is convergent; theorem :: CLVECT_2:73 seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 implies seq2 is convergent & lim seq2 = g; definition let X; let seq; attr seq is bounded means :: CLVECT_2:def 10 ex M st M > 0 & for n holds ||.seq.n.|| <= M; end; theorem :: CLVECT_2:74 seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded; theorem :: CLVECT_2:75 seq is bounded implies -seq is bounded; theorem :: CLVECT_2:76 seq1 is bounded & seq2 is bounded implies seq1 - seq2 is bounded; theorem :: CLVECT_2:77 seq is bounded implies z * seq is bounded; theorem :: CLVECT_2:78 seq is constant implies seq is bounded; theorem :: CLVECT_2:79 for m ex M st ( M > 0 & for n st n <= m holds ||.seq.n.|| < M ); theorem :: CLVECT_2:80 seq is convergent implies seq is bounded; theorem :: CLVECT_2:81 seq1 is bounded & seq1 is_compared_to seq2 implies seq2 is bounded; theorem :: CLVECT_2:82 seq is bounded & seq1 is subsequence of seq implies seq1 is bounded; theorem :: CLVECT_2:83 seq is convergent & seq1 is subsequence of seq implies seq1 is convergent; theorem :: CLVECT_2:84 seq1 is subsequence of seq & seq is convergent implies lim seq1= lim seq; theorem :: CLVECT_2:85 seq is Cauchy & seq1 is subsequence of seq implies seq1 is Cauchy; theorem :: CLVECT_2:86 (seq1 + seq2) ^\k = (seq1 ^\k) + (seq2 ^\k); theorem :: CLVECT_2:87 (-seq) ^\k = -(seq ^\k); theorem :: CLVECT_2:88 (seq1 - seq2) ^\k = (seq1 ^\k) - (seq2 ^\k); theorem :: CLVECT_2:89 (z * seq) ^\k = z * (seq ^\k); theorem :: CLVECT_2:90 seq is convergent implies (seq ^\k) is convergent & lim (seq ^\k)=lim seq; theorem :: CLVECT_2:91 seq is convergent & (ex k st seq = seq1 ^\k) implies seq1 is convergent; theorem :: CLVECT_2:92 seq is Cauchy & (ex k st seq = seq1 ^\k) implies seq1 is Cauchy; theorem :: CLVECT_2:93 seq is Cauchy implies (seq ^\k) is Cauchy; theorem :: CLVECT_2:94 seq1 is_compared_to seq2 implies (seq1 ^\k) is_compared_to (seq2 ^\k); theorem :: CLVECT_2:95 seq is bounded implies (seq ^\k) is bounded; theorem :: CLVECT_2:96 seq is constant implies (seq ^\k) is constant; definition let X; attr X is complete means :: CLVECT_2:def 11 for seq holds seq is Cauchy implies seq is convergent; end; theorem :: CLVECT_2:97 X is complete & seq is Cauchy implies seq is bounded;