:: Conjugate Sequences, Bounded Complex Sequences and Convergent Complex Sequences :: by Adam Naumowicz :: :: Received December 20, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin theorem Th1: :: COMSEQ_2:1 for g, r being Element of COMPLEX st g <> 0c & r <> 0c holds |.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|) proofend; theorem Th2: :: COMSEQ_2:2 for s being Complex_Sequence for n being Element of NAT ex r being Real st ( 0 < r & ( for m being Element of NAT st m <= n holds |.(s . m).| < r ) ) proofend; begin definition let f be complex-valued Function; deffunc H1( set ) -> Element of COMPLEX = (f . $1) *' ; funcf *' -> complex-valued Function means :Def1: :: COMSEQ_2:def 1 ( dom it = dom f & ( for c being set st c in dom it holds it . c = (f . c) *' ) ); existence ex b1 being complex-valued Function st ( dom b1 = dom f & ( for c being set st c in dom b1 holds b1 . c = (f . c) *' ) ) proofend; uniqueness for b1, b2 being complex-valued Function st dom b1 = dom f & ( for c being set st c in dom b1 holds b1 . c = (f . c) *' ) & dom b2 = dom f & ( for c being set st c in dom b2 holds b2 . c = (f . c) *' ) holds b1 = b2 proofend; involutiveness for b1, b2 being complex-valued Function st dom b1 = dom b2 & ( for c being set st c in dom b1 holds b1 . c = (b2 . c) *' ) holds ( dom b2 = dom b1 & ( for c being set st c in dom b2 holds b2 . c = (b1 . c) *' ) ) proofend; end; :: deftheorem Def1 defines *' COMSEQ_2:def_1_:_ for f, b2 being complex-valued Function holds ( b2 = f *' iff ( dom b2 = dom f & ( for c being set st c in dom b2 holds b2 . c = (f . c) *' ) ) ); definition let C be non empty set ; let f be Function of C,COMPLEX; :: original:*' redefine funcf *' -> Function of C,COMPLEX means :Def2: :: COMSEQ_2:def 2 ( dom it = C & ( for n being Element of C holds it . n = (f . n) *' ) ); coherence f *' is Function of C,COMPLEX proofend; compatibility for b1 being Function of C,COMPLEX holds ( b1 = f *' iff ( dom b1 = C & ( for n being Element of C holds b1 . n = (f . n) *' ) ) ) proofend; end; :: deftheorem Def2 defines *' COMSEQ_2:def_2_:_ for C being non empty set for f, b3 being Function of C,COMPLEX holds ( b3 = f *' iff ( dom b3 = C & ( for n being Element of C holds b3 . n = (f . n) *' ) ) ); registration let C be non empty set ; let s be complex-valued ManySortedSet of C; clusters *' -> C -defined complex-valued ; coherence s *' is C -defined proofend; end; registration let C be non empty set ; let seq be complex-valued ManySortedSet of C; clusterseq *' -> C -defined total for C -defined Function; coherence for b1 being C -defined Function st b1 = seq *' holds b1 is total proofend; end; theorem :: COMSEQ_2:3 for s being Complex_Sequence st s is non-zero holds s *' is non-zero proofend; theorem :: COMSEQ_2:4 for r being Element of COMPLEX for s being Complex_Sequence holds (r (#) s) *' = (r *') (#) (s *') proofend; theorem :: COMSEQ_2:5 for s, s9 being Complex_Sequence holds (s (#) s9) *' = (s *') (#) (s9 *') proofend; theorem :: COMSEQ_2:6 for s being Complex_Sequence holds (s *') " = (s ") *' proofend; theorem :: COMSEQ_2:7 for s9, s being Complex_Sequence holds (s9 /" s) *' = (s9 *') /" (s *') proofend; begin definition let f be complex-valued Function; :: SEQ_2:def 5 attrf is bounded means :: COMSEQ_2:def 3 ex r being real number st for y being set st y in dom f holds abs (f . y) < r; end; :: deftheorem defines bounded COMSEQ_2:def_3_:_ for f being complex-valued Function holds ( f is bounded iff ex r being real number st for y being set st y in dom f holds abs (f . y) < r ); definition let s be Complex_Sequence; redefine attr s is bounded means :Def4: :: COMSEQ_2:def 4 ex r being Real st for n being Element of NAT holds |.(s . n).| < r; compatibility ( s is bounded iff ex r being Real st for n being Element of NAT holds |.(s . n).| < r ) proofend; end; :: deftheorem Def4 defines bounded COMSEQ_2:def_4_:_ for s being Complex_Sequence holds ( s is bounded iff ex r being Real st for n being Element of NAT holds |.(s . n).| < r ); reconsider sc = NAT --> 0c as Complex_Sequence ; registration cluster Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued bounded for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st b1 is bounded proofend; end; theorem Th8: :: COMSEQ_2:8 for s being Complex_Sequence holds ( s is bounded iff ex r being Real st ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) ) proofend; begin :: Convergent Complex Sequences :: The Limit of Complex Sequences definition let s be complex-valued ManySortedSet of NAT ; attrs is convergent means :Def5: :: COMSEQ_2:def 5 ex g being Element of COMPLEX st for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s . m) - g).| < p; end; :: deftheorem Def5 defines convergent COMSEQ_2:def_5_:_ for s being complex-valued ManySortedSet of NAT holds ( s is convergent iff ex g being Element of COMPLEX st for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s . m) - g).| < p ); definition let s be Complex_Sequence; assume A1: s is convergent ; func lim s -> Element of COMPLEX means :Def6: :: COMSEQ_2:def 6 for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s . m) - it).| < p; existence ex b1 being Element of COMPLEX st for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s . m) - b1).| < p by A1, Def5; uniqueness for b1, b2 being Element of COMPLEX st ( for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s . m) - b1).| < p ) & ( for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s . m) - b2).| < p ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines lim COMSEQ_2:def_6_:_ for s being Complex_Sequence st s is convergent holds for b2 being Element of COMPLEX holds ( b2 = lim s iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s . m) - b2).| < p ); theorem Th9: :: COMSEQ_2:9 for s being Complex_Sequence st ex g being Element of COMPLEX st for n being Element of NAT holds s . n = g holds s is convergent proofend; theorem Th10: :: COMSEQ_2:10 for s being Complex_Sequence for g being Element of COMPLEX st ( for n being Element of NAT holds s . n = g ) holds lim s = g proofend; Lm1: for n being Element of NAT holds sc . n = 0c by FUNCOP_1:7; registration cluster Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued convergent for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st b1 is convergent by Lm1, Th9; end; registration let s be convergent Complex_Sequence; clusters *' -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = s *' holds b1 is convergent proofend; end; theorem :: COMSEQ_2:11 canceled; theorem Th12: :: COMSEQ_2:12 for s being Complex_Sequence st s is convergent holds lim (s *') = (lim s) *' proofend; begin registration let s1, s2 be convergent Complex_Sequence; clusters1 + s2 -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = s1 + s2 holds b1 is convergent proofend; end; theorem :: COMSEQ_2:13 canceled; theorem Th14: :: COMSEQ_2:14 for s, s9 being convergent Complex_Sequence holds lim (s + s9) = (lim s) + (lim s9) proofend; theorem :: COMSEQ_2:15 canceled; theorem :: COMSEQ_2:16 for s, s9 being convergent Complex_Sequence holds lim ((s + s9) *') = ((lim s) *') + ((lim s9) *') proofend; registration let s be convergent Complex_Sequence; let c be complex number ; clusterc (#) s -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = c (#) s holds b1 is convergent proofend; end; theorem :: COMSEQ_2:17 canceled; theorem Th18: :: COMSEQ_2:18 for s being convergent Complex_Sequence for r being complex number holds lim (r (#) s) = r * (lim s) proofend; theorem :: COMSEQ_2:19 canceled; theorem :: COMSEQ_2:20 for r being Element of COMPLEX for s being convergent Complex_Sequence holds lim ((r (#) s) *') = (r *') * ((lim s) *') proofend; registration let s be convergent Complex_Sequence; cluster - s -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = - s holds b1 is convergent ; end; theorem :: COMSEQ_2:21 canceled; theorem Th22: :: COMSEQ_2:22 for s being convergent Complex_Sequence holds lim (- s) = - (lim s) proofend; theorem :: COMSEQ_2:23 canceled; theorem :: COMSEQ_2:24 for s being convergent Complex_Sequence holds lim ((- s) *') = - ((lim s) *') proofend; registration let s1, s2 be convergent Complex_Sequence; clusters1 - s2 -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = s1 - s2 holds b1 is convergent proofend; end; theorem :: COMSEQ_2:25 canceled; theorem Th26: :: COMSEQ_2:26 for s, s9 being convergent Complex_Sequence holds lim (s - s9) = (lim s) - (lim s9) proofend; theorem :: COMSEQ_2:27 canceled; theorem :: COMSEQ_2:28 for s, s9 being convergent Complex_Sequence holds lim ((s - s9) *') = ((lim s) *') - ((lim s9) *') proofend; registration cluster Function-like V18( NAT , COMPLEX ) convergent -> bounded for Element of K19(K20(NAT,COMPLEX)); coherence for b1 being Complex_Sequence st b1 is convergent holds b1 is bounded proofend; end; registration cluster Function-like V18( NAT , COMPLEX ) non bounded -> non convergent for Element of K19(K20(NAT,COMPLEX)); coherence for b1 being Complex_Sequence st not b1 is bounded holds not b1 is convergent ; end; registration let s1, s2 be convergent Complex_Sequence; clusters1 (#) s2 -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = s1 (#) s2 holds b1 is convergent proofend; end; theorem :: COMSEQ_2:29 canceled; theorem Th30: :: COMSEQ_2:30 for s, s9 being convergent Complex_Sequence holds lim (s (#) s9) = (lim s) * (lim s9) proofend; theorem :: COMSEQ_2:31 canceled; theorem :: COMSEQ_2:32 for s, s9 being convergent Complex_Sequence holds lim ((s (#) s9) *') = ((lim s) *') * ((lim s9) *') proofend; theorem Th33: :: COMSEQ_2:33 for s being convergent Complex_Sequence st lim s <> 0c holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(lim s).| / 2 < |.(s . m).| proofend; theorem Th34: :: COMSEQ_2:34 for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero holds s " is convergent proofend; theorem Th35: :: COMSEQ_2:35 for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-zero holds lim (s ") = (lim s) " proofend; theorem :: COMSEQ_2:36 canceled; theorem :: COMSEQ_2:37 for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-zero holds lim ((s ") *') = ((lim s) *') " proofend; theorem Th38: :: COMSEQ_2:38 for s9, s being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds s9 /" s is convergent proofend; theorem Th39: :: COMSEQ_2:39 for s9, s being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds lim (s9 /" s) = (lim s9) / (lim s) proofend; theorem :: COMSEQ_2:40 canceled; theorem :: COMSEQ_2:41 for s9, s being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds lim ((s9 /" s) *') = ((lim s9) *') / ((lim s) *') proofend; theorem Th42: :: COMSEQ_2:42 for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds s (#) s1 is convergent proofend; theorem Th43: :: COMSEQ_2:43 for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds lim (s (#) s1) = 0c proofend; theorem :: COMSEQ_2:44 canceled; theorem :: COMSEQ_2:45 for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds lim ((s (#) s1) *') = 0c proofend;