:: Conjugate Sequences, Bounded Complex Sequences and Convergent Complex Sequences
:: by Adam Naumowicz
::
:: Received December 20, 1996
:: Copyright (c) 1996-2011 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 C be non empty set ;
let f be PartFunc of C,COMPLEX;
deffunc H1( set ) -> Element of COMPLEX = (f /. $1) *' ;
func f *' -> PartFunc of C,COMPLEX means :Def1: :: COMSEQ_2:def 1
( dom it = dom f & ( for c being Element of C st c in dom it holds
it . c = (f /. c) *' ) );
existence
ex b1 being PartFunc of C,COMPLEX st
( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = (f /. c) *' ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,COMPLEX st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = (f /. c) *' ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds
b2 . c = (f /. c) *' ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines *' COMSEQ_2:def 1 :
for C being non empty set
for f, b3 being PartFunc of C,COMPLEX holds
( b3 = f *' iff ( dom b3 = dom f & ( for c being Element of C st c in dom b3 holds
b3 . c = (f /. c) *' ) ) );

definition
let C be non empty set ;
let f be Function of C,COMPLEX;
redefine func f *' means :Def2: :: COMSEQ_2:def 2
( dom it = C & ( for n being Element of C holds it . n = (f . n) *' ) );
compatibility
for b1 being PartFunc 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 being Function of C,COMPLEX
for b3 being PartFunc 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 seq be Function of C,COMPLEX;
cluster seq *' -> total ;
coherence
seq *' is total
proof end;
end;

theorem :: COMSEQ_2:3
for s being Complex_Sequence st s is non-empty holds
s *' is non-empty
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 s be Complex_Sequence;
redefine attr s is bounded means :Def3: :: COMSEQ_2:def 3
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 Def3 defines bounded COMSEQ_2:def 3 :
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 ;

Lm1: for n being Element of NAT holds sc . n = 0c
by FUNCOP_1:13;

registration
cluster V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total V15( NAT , COMPLEX ) V31() bounded Element of K21(K22(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

definition
let s be Complex_Sequence;
attr s is convergent means :Def4: :: COMSEQ_2:def 4
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 Def4 defines convergent COMSEQ_2:def 4 :
for s being Complex_Sequence 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 :Def5: :: COMSEQ_2:def 5
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, Def4;
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 Def5 defines lim COMSEQ_2:def 5 :
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;

registration
cluster V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total V15( NAT , COMPLEX ) V31() convergent Element of K21(K22(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 Real_Sequence;
coherence
for b1 being Real_Sequence st b1 = |.s.| holds
b1 is convergent
proof end;
end;

theorem Th11: :: COMSEQ_2:11
for s being Complex_Sequence st s is convergent holds
lim |.s.| = |.(lim s).|
proof end;

registration
let s be convergent Complex_Sequence;
cluster s *' -> convergent ;
coherence
s *' is convergent
proof end;
end;

theorem Th12: :: COMSEQ_2:12
for s being Complex_Sequence st s is convergent holds
lim (s *') = (lim s) *'
proof end;

begin

theorem Th13: :: COMSEQ_2:13
for s, s9 being Complex_Sequence st s is convergent & s9 is convergent holds
s + s9 is convergent
proof end;

registration
let s1, s2 be convergent Complex_Sequence;
cluster s1 + s2 -> convergent Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = s1 + s2 holds
b1 is convergent
by Th13;
end;

theorem Th14: :: COMSEQ_2:14
for s, s9 being Complex_Sequence st s is convergent & s9 is convergent holds
lim (s + s9) = (lim s) + (lim s9)
proof end;

theorem :: COMSEQ_2:15
for s, s9 being Complex_Sequence st s is convergent & s9 is convergent holds
lim |.(s + s9).| = |.((lim s) + (lim s9)).|
proof end;

theorem :: COMSEQ_2:16
for s, s9 being Complex_Sequence st s is convergent & s9 is convergent 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 Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = c (#) s holds
b1 is convergent
proof end;
end;

theorem :: COMSEQ_2:17
for r being Element of COMPLEX
for s being Complex_Sequence st s is convergent holds
r (#) s is convergent ;

theorem Th18: :: COMSEQ_2:18
for s being Complex_Sequence
for r being complex number st s is convergent holds
lim (r (#) s) = r * (lim s)
proof end;

theorem :: COMSEQ_2:19
for r being Element of COMPLEX
for s being Complex_Sequence st s is convergent holds
lim |.(r (#) s).| = |.r.| * |.(lim s).|
proof end;

theorem :: COMSEQ_2:20
for r being Element of COMPLEX
for s being Complex_Sequence st s is convergent holds
lim ((r (#) s) *') = (r *') * ((lim s) *')
proof end;

registration
let s be convergent Complex_Sequence;
cluster - s -> convergent Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = - s holds
b1 is convergent
;
end;

theorem :: COMSEQ_2:21
for s being Complex_Sequence st s is convergent holds
- s is convergent ;

theorem Th22: :: COMSEQ_2:22
for s being Complex_Sequence st s is convergent holds
lim (- s) = - (lim s)
proof end;

theorem :: COMSEQ_2:23
for s being Complex_Sequence st s is convergent holds
lim |.(- s).| = |.(lim s).|
proof end;

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

theorem Th25: :: COMSEQ_2:25
for s, s9 being Complex_Sequence st s is convergent & s9 is convergent holds
s - s9 is convergent
proof end;

registration
let s1, s2 be convergent Complex_Sequence;
cluster s1 - s2 -> convergent Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = s1 - s2 holds
b1 is convergent
by Th25;
end;

theorem Th26: :: COMSEQ_2:26
for s, s9 being Complex_Sequence st s is convergent & s9 is convergent holds
lim (s - s9) = (lim s) - (lim s9)
proof end;

theorem :: COMSEQ_2:27
for s, s9 being Complex_Sequence st s is convergent & s9 is convergent holds
lim |.(s - s9).| = |.((lim s) - (lim s9)).|
proof end;

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

registration
cluster Function-like V15( NAT , COMPLEX ) convergent -> bounded Element of K21(K22(NAT,COMPLEX));
coherence
for b1 being Complex_Sequence st b1 is convergent holds
b1 is bounded
proof end;
end;

registration
cluster Function-like V15( NAT , COMPLEX ) non bounded -> non convergent Element of K21(K22(NAT,COMPLEX));
coherence
for b1 being Complex_Sequence st not b1 is bounded holds
not b1 is convergent
;
end;

theorem Th29: :: COMSEQ_2:29
for s, s9 being Complex_Sequence st s is convergent Complex_Sequence & s9 is convergent Complex_Sequence holds
s (#) s9 is convergent
proof end;

registration
let s1, s2 be convergent Complex_Sequence;
cluster s1 (#) s2 -> convergent Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = s1 (#) s2 holds
b1 is convergent
by Th29;
end;

theorem Th30: :: COMSEQ_2:30
for s, s9 being Complex_Sequence st s is convergent Complex_Sequence & s9 is convergent Complex_Sequence holds
lim (s (#) s9) = (lim s) * (lim s9)
proof end;

theorem :: COMSEQ_2:31
for s, s9 being Complex_Sequence st s is convergent & s9 is convergent holds
lim |.(s (#) s9).| = |.(lim s).| * |.(lim s9).|
proof end;

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

theorem Th33: :: COMSEQ_2:33
for s being Complex_Sequence st s is convergent & 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 Complex_Sequence st s is convergent & lim s <> 0c & s is non-empty 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-empty holds
lim (s ") = (lim s) "
proof end;

theorem :: COMSEQ_2:36
for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-empty holds
lim |.(s ").| = |.(lim s).| "
proof end;

theorem :: COMSEQ_2:37
for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-empty 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-empty 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-empty holds
lim (s9 /" s) = (lim s9) / (lim s)
proof end;

theorem :: COMSEQ_2:40
for s9, s being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-empty holds
lim |.(s9 /" s).| = |.(lim s9).| / |.(lim s).|
proof end;

theorem :: COMSEQ_2:41
for s9, s being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-empty 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
for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
lim |.(s (#) s1).| = 0
proof end;

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;