:: Conjugate Sequences, Bounded Complex Sequences and ConvergentComplex Sequences
:: by Adam Naumowicz
::
:: Received December 20, 1996
:: Copyright (c) 1996 Association of Mizar Users

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;

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-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, s' being Complex_Sequence holds (s (#) s') *' = (s *' ) (#) (s' *' )

proof end;

theorem :: COMSEQ_2:6

for s being Complex_Sequence holds (s *' ) " = (s " ) *'

proof end;

theorem :: COMSEQ_2:7

for s', s being Complex_Sequence holds (s' /" s) *' = (s' *' ) /" (s *' )

proof end;

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

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;

reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:57;

registration

cluster 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;

theorem Th13: :: COMSEQ_2:13

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
s + s' is convergent

proof end;

theorem Th14: :: COMSEQ_2:14

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim (s + s') = (lim s) + (lim s')

proof end;

theorem :: COMSEQ_2:15

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim |.(s + s').| = |.((lim s) + (lim s')).|

proof end;

theorem :: COMSEQ_2:16

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim ((s + s') *' ) = ((lim s) *' ) + ((lim s') *' )

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;

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, s' being Complex_Sequence st s is convergent & s' is convergent holds
s - s' is convergent

proof end;

theorem Th26: :: COMSEQ_2:26

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim (s - s') = (lim s) - (lim s')

proof end;

theorem :: COMSEQ_2:27

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim |.(s - s').| = |.((lim s) - (lim s')).|

proof end;

theorem :: COMSEQ_2:28

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim ((s - s') *' ) = ((lim s) *' ) - ((lim s') *' )

proof end;

registration

cluster 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 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, s' being Complex_Sequence st s is convergent Complex_Sequence & s' is convergent Complex_Sequence holds
s (#) s' is convergent

proof end;

theorem Th30: :: COMSEQ_2:30

for s, s' being Complex_Sequence st s is convergent Complex_Sequence & s' is convergent Complex_Sequence holds
lim (s (#) s') = (lim s) * (lim s')

proof end;

theorem :: COMSEQ_2:31

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim |.(s (#) s').| = |.(lim s).| * |.(lim s').|

proof end;

theorem :: COMSEQ_2:32

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim ((s (#) s') *' ) = ((lim s) *' ) * ((lim s') *' )

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-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

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: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 s', s being Complex_Sequence st s' is convergent & s is convergent & lim s <> 0c & s is non-zero holds
s' /" s is convergent

proof end;

theorem Th39: :: COMSEQ_2:39

for s', s being Complex_Sequence st s' is convergent & s is convergent & lim s <> 0c & s is non-zero holds
lim (s' /" s) = (lim s') / (lim s)

proof end;

theorem :: COMSEQ_2:40

for s', s being Complex_Sequence st s' is convergent & s is convergent & lim s <> 0c & s is non-zero holds
lim |.(s' /" s).| = |.(lim s').| / |.(lim s).|

proof end;

theorem :: COMSEQ_2:41

for s', s being Complex_Sequence st s' is convergent & s is convergent & lim s <> 0c & s is non-zero holds
lim ((s' /" s) *' ) = ((lim s') *' ) / ((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;