:: 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 H₁( 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 b₁ being PartFunc of C,COMPLEX st
( dom b₁ = dom f & ( for c being Element of C st c in dom b₁ holds
b₁ . c = (f /. c) *' ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of C,COMPLEX st dom b₁ = dom f & ( for c being Element of C st c in dom b₁ holds
b₁ . c = (f /. c) *' ) & dom b₂ = dom f & ( for c being Element of C st c in dom b₂ holds
b₂ . c = (f /. c) *' ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines *' COMSEQ_2:def 1 :
for C being non empty set
for f, b₃ being PartFunc of C,COMPLEX holds
( b₃ = f *' iff ( dom b₃ = dom f & ( for c being Element of C st c in dom b₃ holds
b₃ . 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 b₁ being PartFunc of C,COMPLEX holds
( b₁ = f *' iff ( dom b₁ = C & ( for n being Element of C holds b₁ . 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 b₃ being PartFunc of C,COMPLEX holds
( b₃ = f *' iff ( dom b₃ = C & ( for n being Element of C holds b₃ . 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 b₁ being Complex_Sequence st b₁ 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 b₁ 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) - b₁).| < p by A1, Def4;
uniqueness
for b₁, b₂ 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) - b₁).| < 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) - b₂).| < p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines lim COMSEQ_2:def 5 :
for s being Complex_Sequence st s is convergent holds
for b₂ being Element of COMPLEX holds
( b₂ = 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) - b₂).| < 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 b₁ being Complex_Sequence st b₁ is convergent by Lm1, Th9;

end;

registration

let s be convergent Complex_Sequence;
cluster |.s.| -> convergent Real_Sequence;
coherence
for b₁ being Real_Sequence st b₁ = |.s.| holds
b₁ 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 b₁ being Complex_Sequence st b₁ = s1 + s2 holds
b₁ 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 b₁ being Complex_Sequence st b₁ = c (#) s holds
b₁ 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 b₁ being Complex_Sequence st b₁ = - s holds
b₁ 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 b₁ being Complex_Sequence st b₁ = s1 - s2 holds
b₁ 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 b₁ being Complex_Sequence st b₁ is convergent holds
b₁ is bounded

proof end;

end;

registration

cluster Function-like V15( NAT , COMPLEX ) non bounded -> non convergent Element of K21(K22(NAT,COMPLEX));
coherence
for b₁ being Complex_Sequence st not b₁ is bounded holds
not b₁ 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 b₁ being Complex_Sequence st b₁ = s1 (#) s2 holds
b₁ 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;