:: 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.|)
proof end;

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 ) )
proof end;

begin

definition
let f be complex-valued Function;
deffunc H1( set ) -> Element of COMPLEX = (f . $1) *' ;
func f *' -> 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) *' ) )
proof end;
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
proof end;
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) *' ) )
proof end;
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 func f *' -> 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
proof end;
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) *' ) ) )
proof end;
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;
cluster s *' -> C -defined complex-valued ;
coherence
s *' is C -defined
proof end;
end;

registration
let C be non empty set ;
let seq be complex-valued ManySortedSet of C;
cluster seq *' -> C -defined total for C -defined Function;
coherence
for b1 being C -defined Function st b1 = seq *' holds
b1 is total
proof end;
end;

theorem :: COMSEQ_2:3
for s being Complex_Sequence st s is non-zero holds
s *' is non-zero
proof end;

theorem :: COMSEQ_2:4
for r being Element of COMPLEX
for s being Complex_Sequence holds (r (#) s) *' = (r *') (#) (s *')
proof end;

theorem :: COMSEQ_2:5
for s, s9 being Complex_Sequence holds (s (#) s9) *' = (s *') (#) (s9 *')
proof end;

theorem :: COMSEQ_2:6
for s being Complex_Sequence holds (s *') " = (s ") *'
proof end;

theorem :: COMSEQ_2:7
for s9, s being Complex_Sequence holds (s9 /" s) *' = (s9 *') /" (s *')
proof end;

begin

definition
let f be complex-valued Function;
:: SEQ_2:def 5
attr f 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 )
proof end;
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
proof end;
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 ) ) )
proof end;

begin

:: Convergent Complex Sequences
:: The Limit of Complex Sequences
definition
let s be complex-valued ManySortedSet of NAT ;
attr s 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
proof end;
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
proof end;

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
proof end;

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;
cluster s *' -> convergent for Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = s *' holds
b1 is convergent
proof end;
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) *'
proof end;

begin

registration
let s1, s2 be convergent Complex_Sequence;
cluster s1 + s2 -> convergent for Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = s1 + s2 holds
b1 is convergent
proof end;
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)
proof end;

theorem :: COMSEQ_2:15
canceled;

theorem :: COMSEQ_2:16
for s, s9 being convergent Complex_Sequence holds lim ((s + s9) *') = ((lim s) *') + ((lim s9) *')
proof end;

registration
let s be convergent Complex_Sequence;
let c be complex number ;
cluster c (#) s -> convergent for Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = c (#) s holds
b1 is convergent
proof end;
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)
proof end;

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) *')
proof end;

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)
proof end;

theorem :: COMSEQ_2:23
canceled;

theorem :: COMSEQ_2:24
for s being convergent Complex_Sequence holds lim ((- s) *') = - ((lim s) *')
proof end;

registration
let s1, s2 be convergent Complex_Sequence;
cluster s1 - s2 -> convergent for Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = s1 - s2 holds
b1 is convergent
proof end;
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)
proof end;

theorem :: COMSEQ_2:27
canceled;

theorem :: COMSEQ_2:28
for s, s9 being convergent Complex_Sequence holds lim ((s - s9) *') = ((lim s) *') - ((lim s9) *')
proof end;

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
proof end;
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;
cluster s1 (#) s2 -> convergent for Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = s1 (#) s2 holds
b1 is convergent
proof end;
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)
proof end;

theorem :: COMSEQ_2:31
canceled;

theorem :: COMSEQ_2:32
for s, s9 being convergent Complex_Sequence holds lim ((s (#) s9) *') = ((lim s) *') * ((lim s9) *')
proof end;

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).|
proof end;

theorem Th34: :: COMSEQ_2:34
for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero holds
s " is convergent
proof end;

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) "
proof end;

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) *') "
proof end;

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
proof end;

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)
proof end;

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) *')
proof end;

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
proof end;

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
proof end;

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
proof end;