Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Conjugate Sequences, Bounded Complex Sequences and Convergent Complex Sequences

**by****Adam Naumowicz**- Received December 20, 1996
- MML identifier: COMSEQ_2

- [ Mizar article, MML identifier index ]

environ vocabulary COMPLEX1, COMSEQ_1, RELAT_1, ARYTM_1, ARYTM_3, FUNCT_1, ARYTM, PARTFUN1, FINSEQ_4, ANPROJ_1, SEQ_1, LATTICES, SEQ_2, ORDINAL2, SQUARE_1, ABSVALUE; notation XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SEQ_2, ABSVALUE, NAT_1, SQUARE_1, FINSEQ_4, COMPLEX1, COMSEQ_1; constructors REAL_1, ABSVALUE, NAT_1, SQUARE_1, COMSEQ_1, SEQ_2, FINSEQ_4, PARTFUN1, COMPLEX1, MEMBERED; clusters XREAL_0, COMSEQ_1, RELSET_1, FUNCT_2, ARYTM_3, COMPLEX1, MEMBERED, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve n,n1,n2,m for Nat; reserve r,g1,g2,g,g' for Element of COMPLEX; reserve R,R2 for Real; reserve s,s',s1 for Complex_Sequence; ::::::::::::::::::::: :: PRELIMINARIES :: ::::::::::::::::::::: theorem :: COMSEQ_2:1 g<>0c & r<>0c implies |.g"-r".|=|.g-r.|/(|.g.|*|.r.|); theorem :: COMSEQ_2:2 for n ex r being Real st 0<r & for m st m<=n holds |.s.m.|<r; ::::::::::::::::::::::::::: :: CONJUGATE SEQUENCES :: ::::::::::::::::::::::::::: begin definition let C be non empty set; let f be PartFunc of C,COMPLEX; func f*' ->PartFunc of C,COMPLEX means :: COMSEQ_2:def 1 dom it = dom f & for c being Element of C st c in dom it holds it.c = (f/.c)*'; end; definition let C be non empty set; let f be Function of C,COMPLEX; redefine func f*' means :: COMSEQ_2:def 2 dom it = C & for n being Element of C holds it.n=(f.n)*'; end; definition let C be non empty set; let seq be Function of C,COMPLEX; cluster seq*' -> total; end; theorem :: COMSEQ_2:3 s is non-zero implies s*' is non-zero; theorem :: COMSEQ_2:4 (r(#)s)*' = (r*')(#)(s*'); theorem :: COMSEQ_2:5 (s (#) s')*' = (s*') (#) (s'*'); theorem :: COMSEQ_2:6 (s*')" = (s")*'; theorem :: COMSEQ_2:7 (s'/"s)*' = (s'*') /" (s*'); begin :: BOUNDED COMPLEX SEQUENCES definition let s; attr s is bounded means :: COMSEQ_2:def 3 ex r being Real st for n holds |.s.n.|<r; end; definition cluster bounded Complex_Sequence; end; theorem :: COMSEQ_2:8 s is bounded iff ex r being Real st (0<r & for n holds |.s.n.|<r); :::::::::::::::::::::::::::::::::::::: :: CONVERGENT COMPLEX SEQUENCES :: :: THE LIMIT OF COMPLEX SEQUENCES :: :::::::::::::::::::::::::::::::::::::: begin definition let s; attr s is convergent means :: COMSEQ_2:def 4 ex g st for p be Real st 0<p ex n st for m st n<=m holds |.s.m-g.|<p; end; definition let s; assume s is convergent; func lim s -> Element of COMPLEX means :: COMSEQ_2:def 5 for p be Real st 0<p ex n st for m st n<=m holds |.s.m-it.|<p; end; theorem :: COMSEQ_2:9 (ex g st for n being Nat holds s.n = g) implies s is convergent; theorem :: COMSEQ_2:10 for g st for n being Nat holds s.n = g holds lim s = g; definition cluster convergent Complex_Sequence; end; definition let s be convergent Complex_Sequence; cluster |.s.| -> convergent; end; theorem :: COMSEQ_2:11 s is convergent implies lim |.s.| = |.lim s.|; definition let s be convergent Complex_Sequence; cluster s*' -> convergent; end; theorem :: COMSEQ_2:12 s is convergent implies lim(s*') = (lim s)*'; ::::::::::::::::::::: :: MAIN THEOREMS :: ::::::::::::::::::::: begin theorem :: COMSEQ_2:13 s is convergent & s' is convergent implies (s + s') is convergent; theorem :: COMSEQ_2:14 s is convergent & s' is convergent implies lim (s + s')=(lim s)+(lim s'); theorem :: COMSEQ_2:15 s is convergent & s' is convergent implies lim |.(s + s').| = |.(lim s)+(lim s').|; theorem :: COMSEQ_2:16 s is convergent & s' is convergent implies lim (s + s')*' = (lim s)*' + (lim s')*'; theorem :: COMSEQ_2:17 s is convergent implies r(#)s is convergent; theorem :: COMSEQ_2:18 s is convergent implies lim(r(#)s)=r*(lim s); theorem :: COMSEQ_2:19 s is convergent implies lim |.(r(#)s).| = |.r.|*|.(lim s).|; theorem :: COMSEQ_2:20 s is convergent implies lim (r(#)s)*' = (r*')*(lim s)*'; theorem :: COMSEQ_2:21 s is convergent implies - s is convergent; theorem :: COMSEQ_2:22 s is convergent implies lim(-s)=-(lim s); theorem :: COMSEQ_2:23 s is convergent implies lim |.-s.| = |.lim s.|; theorem :: COMSEQ_2:24 s is convergent implies lim (-s)*' = -(lim s)*'; theorem :: COMSEQ_2:25 s is convergent & s' is convergent implies s - s' is convergent; theorem :: COMSEQ_2:26 s is convergent & s' is convergent implies lim(s - s')=(lim s)-(lim s'); theorem :: COMSEQ_2:27 s is convergent & s' is convergent implies lim |.s - s'.| = |.(lim s) - (lim s').|; theorem :: COMSEQ_2:28 s is convergent & s' is convergent implies lim (s - s')*' = (lim s)*' - (lim s')*'; definition cluster convergent -> bounded Complex_Sequence; end; definition cluster non bounded -> non convergent Complex_Sequence; end; theorem :: COMSEQ_2:29 s is convergent Complex_Sequence & s' is convergent Complex_Sequence implies s (#) s' is convergent; theorem :: COMSEQ_2:30 s is convergent Complex_Sequence & s' is convergent Complex_Sequence implies lim(s(#)s')=(lim s)*(lim s'); theorem :: COMSEQ_2:31 s is convergent & s' is convergent implies lim |.s(#)s'.| = |.lim s.|*|.lim s'.|; theorem :: COMSEQ_2:32 s is convergent & s' is convergent implies lim (s(#)s')*' = (lim s)*' * (lim s')*'; theorem :: COMSEQ_2:33 s is convergent implies ((lim s)<>0c implies ex n st for m st n<=m holds |.(lim s).|/2<|.s.m.|); theorem :: COMSEQ_2:34 s is convergent & (lim s)<>0c & s is non-zero implies s" is convergent; theorem :: COMSEQ_2:35 s is convergent & (lim s)<>0c & s is non-zero implies lim s"=(lim s)"; theorem :: COMSEQ_2:36 s is convergent & (lim s)<>0c & s is non-zero implies lim |.s".| = (|.lim s.|)"; theorem :: COMSEQ_2:37 s is convergent & (lim s)<>0c & s is non-zero implies lim (s")*' = ((lim s)*')"; theorem :: COMSEQ_2:38 s' is convergent & s is convergent & (lim s)<>0c & s is non-zero implies s'/"s is convergent; theorem :: COMSEQ_2:39 s' is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim(s'/"s)=(lim s')/(lim s); theorem :: COMSEQ_2:40 s' is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim |.(s'/"s).|=|.(lim s').|/|.(lim s).|; theorem :: COMSEQ_2:41 s' is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim (s'/"s)*' = ((lim s')*')/((lim s)*'); theorem :: COMSEQ_2:42 s is convergent & s1 is bounded & (lim s)=0c implies s(#)s1 is convergent; theorem :: COMSEQ_2:43 s is convergent & s1 is bounded & (lim s)=0c implies lim(s(#)s1)=0c; theorem :: COMSEQ_2:44 s is convergent & s1 is bounded & (lim s)=0c implies lim |.s(#)s1.| = 0; theorem :: COMSEQ_2:45 s is convergent & s1 is bounded & (lim s)=0c implies lim (s(#)s1)*' = 0c;

Back to top