:: Conjugate Sequences, Bounded Complex Sequences and Convergent :: Complex Sequences :: by Adam Naumowicz :: :: Received December 20, 1996 :: Copyright (c) 1996-2019 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, SUBSET_1, REAL_1, COMSEQ_1, COMPLEX1, RELAT_1, ARYTM_1, ARYTM_3, CARD_1, XXREAL_0, FUNCT_1, XBOOLE_0, PARTFUN1, VALUED_0, VALUED_1, XXREAL_2, FUNCOP_1, SEQ_2, ORDINAL2, XCMPLX_0, PBOOLE, TARSKI, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, RELAT_1, REAL_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, NAT_1, COMSEQ_1, XXREAL_0; constructors PARTFUN1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1, RELSET_1, PBOOLE, NUMBERS; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, VALUED_1, VALUED_0, XCMPLX_0, NAT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions RELAT_1, FUNCT_1, PARTFUN1; equalities VALUED_1; theorems COMSEQ_1, COMPLEX1, NAT_1, FUNCT_2, XREAL_0, XCMPLX_0, XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, PARTFUN1, VALUED_0, ORDINAL1, NUMBERS; schemes NAT_1, FUNCT_1; begin :: Preliminaries reserve n,n1,n2,m for Nat; reserve r,g1,g2,g,g9 for Complex; reserve R,R2 for Real; reserve s,s9,s1 for Complex_Sequence; theorem Th1: g<>0c & r<>0c implies |.g"-r".|=|.g-r.|/(|.g.|*|.r.|) proof assume A1: g<>0c & r<>0c; thus |.g"-r".|=|.1r/g-r".| by COMPLEX1:def 4,XCMPLX_1:215 .=|.1r/g-1r/r.| by COMPLEX1:def 4,XCMPLX_1:215 .=|.1r/g+-1r/r.| .=|.1r/g+-1r*r".| by XCMPLX_0:def 9 .=|.1r/g+(-1r)*r".| .=|.1r/g+(-1r)/r.| by XCMPLX_0:def 9 .=|.(1r*r+(-1r)*g)/(r*g).| by A1,XCMPLX_1:116 .=|.r-g.|/|.g*r.| by COMPLEX1:67,def 4 .=|.-(g-r).|/(|.g.|*|.r.|) by COMPLEX1:65 .=|.g-r.|/(|.g.|*|.r.|) by COMPLEX1:52; end; theorem Th2: for n ex r being Real st 00 by A2; let m such that A9: m <= n+1; A10: now assume m <= n; then A11: |.s.m.| < R1 by A3; R1+00 & for m st m<=n holds |.s.m.| complex-valued Function means :Def1: dom it = dom f & for c being set st c in dom it holds it.c = (f.c)*'; existence proof consider F being Function such that A1: dom F = dom f and A2: for x being object st x in dom f holds F.x = F(x) from FUNCT_1:sch 3; for x being object st x in dom F holds F.x is complex proof let x be object; assume x in dom F; then F.x = F(x) by A1,A2; hence thesis; end; then reconsider F as complex-valued Function by VALUED_0:def 7; take F; thus dom f = dom F by A1; thus thesis by A1,A2; end; uniqueness proof let h,g be complex-valued Function such that A3: dom h=dom f and A4: for c be set st c in dom h holds h.c = F(c) and A5: dom g=dom f and A6: for c be set st c in dom g holds g.c = F(c); thus dom h=dom g by A3,A5; let x be object; assume A7: x in dom h; hence h.x = F(x) by A4 .= g.x by A3,A5,A6,A7; end; involutiveness proof let g,f be complex-valued Function; assume that A8: dom g = dom f and A9: for c being set st c in dom g holds g.c = (f.c)*'; thus dom f = dom g by A8; let c be set; assume A10: c in dom f; thus f.c = (f.c)*'*' .= (g.c)*' by A8,A10,A9; end; end; definition let C be non empty set; let f be Function of C,COMPLEX; redefine func f*' -> Function of C,COMPLEX means :Def2: for n being Element of C holds it.n=(f.n)*'; coherence proof A1: dom(f*') = dom f by Def1 .= C by PARTFUN1:def 2; for x being object st x in C holds (f*').x in COMPLEX by XCMPLX_0:def 2; hence f*' is Function of C,COMPLEX by A1,FUNCT_2:3; end; compatibility proof let IT be Function of C,COMPLEX; A2: dom IT = C by FUNCT_2:def 1; hence IT = f*' implies for c being Element of C holds IT.c = (f.c)*' by Def1; assume A3: for c being Element of C holds IT.c = (f.c)*'; A4: dom IT = dom f by A2,FUNCT_2:def 1; for c being set st c in dom IT holds IT.c = (f.c)*' by A3; hence IT = f*' by A4,Def1; end; end; registration let C be non empty set; let s be complex-valued ManySortedSet of C; cluster s*' -> C-defined; coherence proof dom s c= C; hence dom(s*') c= C by Def1; end; end; registration let C be non empty set; let seq be complex-valued ManySortedSet of C; cluster seq*' -> total for C-defined Function; coherence proof let f be C-defined Function; assume f = seq*'; hence dom f = dom seq by Def1 .= C by PARTFUN1:def 2; end; end; theorem s is non-zero implies s*' is non-zero proof assume A1: s is non-zero; now let n be Element of NAT; s.n <> 0 by A1,COMSEQ_1:3; then (s.n)*' <>0c by COMPLEX1:29; hence s*'.n <>0c by Def2; end; hence thesis by COMSEQ_1:4; end; theorem (r(#)s)*' = (r*')(#)(s*') proof now let n be Element of NAT; thus (r(#)s)*'.n = ((r(#)s).n)*' by Def2 .= (r*s.n)*' by VALUED_1:6 .= (r*')*(s.n)*' by COMPLEX1:35 .= (r*')*(s*'.n) by Def2 .= ((r*')(#)(s*')).n by VALUED_1:6; end; hence thesis by FUNCT_2:63; end; theorem (s (#) s9)*' = (s*') (#) (s9*') proof now let n be Element of NAT; thus (s (#) s9)*'.n = ((s (#) s9).n)*' by Def2 .= (s.n * s9.n)*' by VALUED_1:5 .= (s.n)*' * (s9.n)*' by COMPLEX1:35 .= (s*'.n) * (s9.n)*' by Def2 .= (s*'.n) * (s9*'.n) by Def2 .= (s*' (#) s9*').n by VALUED_1:5; end; hence thesis by FUNCT_2:63; end; theorem (s*')" = (s")*' proof now let n be Element of NAT; thus (s*')".n = (s*'.n)" by VALUED_1:10 .= ((s.n)*')" by Def2 .= ((s.n)")*' by COMPLEX1:36 .= (s".n)*' by VALUED_1:10 .= (s")*'.n by Def2; end; hence thesis by FUNCT_2:63; end; theorem (s9/"s)*' = (s9*') /" (s*') proof now let n be Element of NAT; thus (s9/"s)*'.n = ((s9 (#) s").n)*' by Def2 .= ((s9.n) * (s".n))*' by VALUED_1:5 .= ((s9.n) * (s.n)")*' by VALUED_1:10 .= (s9.n)*' * ((s.n)")*' by COMPLEX1:35 .= (s9.n)*' * ((s.n)*')" by COMPLEX1:36 .= (s9*').n * ((s.n)*')" by Def2 .= (s9*').n * ((s*').n)" by Def2 .= (s9*').n * ((s*')").n by VALUED_1:10 .= ((s9*') /" (s*')).n by VALUED_1:5; end; hence thesis by FUNCT_2:63; end; begin :: BOUNDED COMPLEX SEQUENCES definition let f be complex-valued Function; attr f is bounded means :: SEQ_2:def 5 ex r being Real st for y being set st y in dom f holds |.f.y.| 0c; registration cluster bounded for Complex_Sequence; existence proof 1 in NAT; then reconsider j = 1 as Element of REAL by NUMBERS:19; take sc, j; let n; n in NAT by ORDINAL1:def 12; hence thesis by COMPLEX1:44,FUNCOP_1:7; end; end; theorem Th8: s is bounded iff ex r being Real st (0 Complex means :Def6: for p be Real st 0

g2; reconsider p = |.g1 - g2.|/2 as Real; A5: |.g1-g2.| > 0 by A4,COMPLEX1:62; then consider n1 such that A6: for m st n1<=m holds |.s.m-g1.|

convergent for Complex_Sequence; coherence proof let t be Complex_Sequence such that A1: t = s*'; consider g such that A2: for p being Real st 0

convergent for Complex_Sequence; coherence proof let s be Complex_Sequence such that A1: s = s1 + s2; consider g such that A2: for p be Real st 0

0; then consider n1 such that A5: for m st n1<=m holds |.s1.m - g.|

convergent for Complex_Sequence; coherence proof A1: now let c be Element of COMPLEX; per cases; suppose A2: c =0c; now let n; thus (c(#)s).n = 0c*s.n by A2,VALUED_1:6 .= 0c; end; hence c(#)s is convergent by Th9; end; suppose A3: c <> 0c; thus c(#)s is convergent proof consider g such that A4: for p be Real st 0

0 by A3,COMPLEX1:47; consider n such that A7: for m st n<=m holds |.s.m-g.|

0c; for p be Real st p>0 holds ex n st for m st n<=m holds |.(r(#)s) .m-r*(lim s).|

0; A3: |.r.|>0 by A1,COMPLEX1:47; p / |.r.| > 0 by A3,A2; then consider n such that A4: for m st n<=m holds |.s.m-(lim s).|< p/|.r.| by Def6; take n; let m; assume n<=m; then |.s.m-(lim s).|

convergent for Complex_Sequence; coherence; end; ::\$CT theorem Th16: for s being convergent Complex_Sequence holds lim(-s)=-(lim s) proof let s being convergent Complex_Sequence; lim(-s) = (-1)*(lim s) by Th14 .= - 1r*(lim s) by COMPLEX1:def 4; hence thesis by COMPLEX1:def 4; end; ::\$CT theorem for s being convergent Complex_Sequence holds lim (-s)*' = -(lim s)*' proof let s being convergent Complex_Sequence; thus lim (-s)*' = (lim (-s))*' by Th11 .= (-(lim s))*' by Th16 .= -(lim s)*' by COMPLEX1:33; end; registration let s1,s2 be convergent Complex_Sequence; cluster s1 - s2 -> convergent for Complex_Sequence; coherence proof - s2 is convergent; hence thesis; end; end; ::\$CT theorem Th18: for s,s9 being convergent Complex_Sequence holds lim(s - s9)=(lim s)-( lim s9) proof let s,s9 be convergent Complex_Sequence; lim(s - s9) = (lim s) + lim(-s9) by Th12 .= (lim s) + -(lim s9) by Th16; hence thesis; end; ::\$CT theorem for s,s9 being convergent Complex_Sequence holds lim (s - s9)*' = (lim s)*' - (lim s9)*' proof let s,s9 be convergent Complex_Sequence; thus lim (s - s9)*' = (lim (s - s9))*' by Th11 .= ((lim s) - (lim s9))*' by Th18 .= (lim s)*' - (lim s9)*' by COMPLEX1:34; end; registration cluster convergent -> bounded for Complex_Sequence; coherence proof let s; assume s is convergent; then consider g such that A1: for p be Real st 0

non convergent for Complex_Sequence; coherence; end; registration let s1,s2 be convergent Complex_Sequence; cluster s1 (#) s2 -> convergent for Complex_Sequence; coherence proof let s be Complex_Sequence such that A1: s = s1 (#) s2; consider g1 such that A2: for p being Real st 0

0c ex n st for m st n <=m holds |.(lim s).|/2<|.s.m.| proof let s be convergent Complex_Sequence such that A1: (lim s)<>0c; 0<|.(lim s).| by A1,COMPLEX1:47; then 0<|.(lim s).|/2; then consider n1 such that A2: for m st n1<=m holds |.s.m-(lim s).|<|.(lim s).|/2 by Def6; take n=n1; let m; assume n<=m; then A3: |.s.m-(lim s).|<|.(lim s).|/2 by A2; A4: |.(lim s)-s.m.|=|.-(s.m-(lim s)).| .=|.s.m-(lim s).| by COMPLEX1:52; A5: |.(lim s).|/2+(|.s.m.|- |.(lim s).|/2) =|.s.m.| & |.(lim s).|- |.s.m.|+ (|.s. m.|- |.(lim s).|/2) =|.(lim s).|/2; |.(lim s).|- |.s.m.|<=|.(lim s)-s.m.| by COMPLEX1:59; then |.(lim s).|- |.s.m.|<|.(lim s).|/2 by A3,A4,XXREAL_0:2; hence thesis by A5,XREAL_1:6; end; theorem Th23: for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero holds s" is convergent proof let s be convergent Complex_Sequence; assume that A1: (lim s)<>0c and A2: s is non-zero; consider n1 such that A3: for m st n1<=m holds |.(lim s).|/2<|.s.m.| by A1,Th22; take(lim s)"; let p be Real; assume A4: 0|.(lim s).|/2 by A1,COMPLEX1:47; A12: (p*(|.(lim s).|/2))/(|.(lim s).|/2 ) =(p*(|.(lim s).|/2))*(|.(lim s).|/ 2 )" by XCMPLX_0:def 9 .=p*((|.(lim s).|/2)*(|.(lim s).|/2 )") .=p*1 by A11,XCMPLX_0:def 7 .=p; A13: 0<>|.(lim s).| by A1,COMPLEX1:47; A14: (p*((|.(lim s).|*|.(lim s).|)/2))/(|.s.m.|*|.(lim s).|) =(p*(2"*(|.(lim s).|*|.(lim s).|)))* (|.s.m.|*|.(lim s).|)" by XCMPLX_0:def 9 .=p*2"*((|.(lim s).|*|.(lim s).|)*(|.(lim s).|*|.s.m.|)") .=p*2"*((|.(lim s).|*|.(lim s).|)* (|.(lim s).|"*|.s.m.|")) by XCMPLX_1:204 .=p*2"*(|.(lim s).|*(|.(lim s).|*|.(lim s).|")*|.s.m.|") .=p*2"*(|.(lim s).|*1*|.s.m.|") by A13,XCMPLX_0:def 7 .=p*(|.(lim s).|/2)*|.s.m.|" .=(p*(|.(lim s).|/2))/|.s.m.| by XCMPLX_0:def 9; m in NAT by ORDINAL1:def 12; then A15: s.m <> 0 by A2,COMSEQ_1:3; then s.m*(lim s)<>0c by A1; then 0<|.s.m*(lim s).| by COMPLEX1:47; then A16: 0<|.s.m.|*|.(lim s).| by COMPLEX1:65; n2<=n by NAT_1:12; then n2<=m by A7,XXREAL_0:2; then |.s.m-(lim s).|0c & s is non-zero implies lim s"=( lim s)" proof assume that A1: s is convergent and A2: (lim s)<>0c and A3: s is non-zero; consider n1 such that A4: for m st n1<=m holds |.(lim s).|/2<|.s.m.| by A1,A2,Th22; A5: 0<|.(lim s).| by A2,COMPLEX1:47; then 0*0<|.(lim s).|*|.(lim s).|; then A6: 0<(|.(lim s).|*|.(lim s).|)/2; A7: 0<>|.(lim s).| by A2,COMPLEX1:47; A8: now let p be Real; A9: 0<>|.(lim s).|/2 by A2,COMPLEX1:47; A10: (p*(|.(lim s).|/2))/(|.(lim s).|/2 ) =(p*(|.(lim s).|/2))*(|.(lim s) .|/2 )" by XCMPLX_0:def 9 .=p*((|.(lim s).|/2)*(|.(lim s).|/2 )") .=p*1 by A9,XCMPLX_0:def 7 .=p; assume A11: 0 0 by A3,COMSEQ_1:3; then s.m*(lim s)<>0c by A2; then 0<|.s.m*(lim s).| by COMPLEX1:47; then A19: 0<|.s.m.|*|.(lim s).| by COMPLEX1:65; n2<=n by NAT_1:12; then n2<=m by A13,XXREAL_0:2; then |.s.m-(lim s).|0c & s is non-zero implies lim (s")*' = (( lim s)*')" proof assume A1: s is convergent & (lim s)<>0c & s is non-zero; then s" is convergent by Th23; hence lim (s")*' = (lim s")*' by Th11 .= ((lim s)")*' by A1,Th24 .= ((lim s)*')" by COMPLEX1:36; end; theorem Th26: s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies s9/"s is convergent proof assume that A1: s9 is convergent and A2: s is convergent & (lim s)<>0c & s is non-zero; s" is convergent by A2,Th23; hence thesis by A1; end; theorem Th27: s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim(s9/"s)=(lim s9)/(lim s) proof assume that A1: s9 is convergent and A2: s is convergent & (lim s)<>0c & s is non-zero; s" is convergent by A2,Th23; then lim (s9(#)(s"))=(lim s9)*(lim s") by A1,Th20 .=(lim s9)*(lim s)" by A2,Th24 .=(lim s9)/(lim s) by XCMPLX_0:def 9; hence thesis; end; ::\$CT theorem s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim (s9/"s)*' = ((lim s9)*')/((lim s)*') proof assume A1: s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero; then s9/"s is convergent by Th26; hence lim (s9/"s)*' = (lim (s9/"s))*' by Th11 .= ((lim s9)/(lim s))*' by A1,Th27 .= ((lim s9)*')/((lim s)*') by COMPLEX1:37; end; theorem Th29: s is convergent & s1 is bounded & (lim s)=0c implies s(#)s1 is convergent proof assume that A1: s is convergent and A2: s1 is bounded and A3: (lim s) = 0c; take g=0c; consider R such that A4: 00; then |.((s(#)s1).m)-g.|<(p/R)*|.s1.m.| by A11,A10,A13,XREAL_1:68; hence thesis by A12,XXREAL_0:2; end; hence thesis by A6,A10; end; theorem Th30: s is convergent & s1 is bounded & (lim s)=0c implies lim(s(#)s1) =0c proof assume that A1: s is convergent and A2: s1 is bounded and A3: lim s=0c; A4: now consider R such that A5: 00; then |.((s(#)s1).m)-0c.|<(p/R)*|.s1.m.| by A11,A12,A13,XREAL_1:68; hence |.((s(#)s1).m)-0c.|