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

theorem Th1: :: COMSEQ_2:1

for r, g being 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 Nat ex r being Real st
( 0 < r & ( for m being Nat st m <= n holds
|.(s . m).| < r ) )

proof end;

definition

let f be complex-valued Function;
deffunc H₁( object ) -> object = (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 b₁ being complex-valued Function st
( dom b₁ = dom f & ( for c being set st c in dom b₁ holds
b₁ . c = (f . c) *' ) )

proof end;

uniqueness
for b₁, b₂ being complex-valued Function st dom b₁ = dom f & ( for c being set st c in dom b₁ holds
b₁ . c = (f . c) *' ) & dom b₂ = dom f & ( for c being set st c in dom b₂ holds
b₂ . c = (f . c) *' ) holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being complex-valued Function st dom b₁ = dom b₂ & ( for c being set st c in dom b₁ holds
b₁ . c = (b₂ . c) *' ) holds
( dom b₂ = dom b₁ & ( for c being set st c in dom b₂ holds
b₂ . c = (b₁ . c) *' ) )

proof end;

end;

:: deftheorem Def1 defines *' COMSEQ_2:def 1 :
for f, b₂ being complex-valued Function holds
( b₂ = f *' iff ( dom b₂ = dom f & ( for c being set st c in dom b₂ holds
b₂ . 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
for n being Element of C holds it . n = (f . n) *' ;

coherence
f *' is Function of C,COMPLEX

proof end;

compatibility
for b₁ being Function of C,COMPLEX holds
( b₁ = f *' iff 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, b₃ being Function of C,COMPLEX holds
( b₃ = f *' iff for n being Element of C holds b₃ . 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 b₁ being C -defined Function st b₁ = seq *' holds
b₁ 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 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 s, s9 being Complex_Sequence holds (s9 /" s) *' = (s9 *') /" (s *')

proof end;

definition

let f be complex-valued Function;

:: SEQ_2:def 5

attr f is bounded means :: COMSEQ_2:def 3
ex r being Real st
for y being set st y in dom f holds
|.(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 st
for y being set st y in dom f holds
|.(f . y).| < r );

definition

let s be Complex_Sequence;

redefine attr s is bounded means :: COMSEQ_2:def 4
ex r being Real st
for n being Nat holds |.(s . n).| < r;

compatibility
( s is bounded iff ex r being Real st
for n being Nat holds |.(s . n).| < r )

proof end;

end;

:: deftheorem defines bounded COMSEQ_2:def 4 :
for s being Complex_Sequence holds
( s is bounded iff ex r being Real st
for n being Nat holds |.(s . n).| < r );

set sc = NAT --> 0c;

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 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 Nat holds |.(s . n).| < r ) ) )

proof end;

:: 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 Complex st
for p being Real st 0 < p holds
ex n being Nat st
for m being 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 Complex st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < p );

definition

let s be Complex_Sequence;
assume A1: s is convergent ;

func lim s -> Complex means :Def6: :: COMSEQ_2:def 6
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - it).| < p;

existence
ex b₁ being Complex st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - b₁).| < p by A1;
uniqueness
for b₁, b₂ being Complex st ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - b₁).| < p ) & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - b₂).| < p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines lim COMSEQ_2:def 6 :
for s being Complex_Sequence st s is convergent holds
for b₂ being Complex holds
( b₂ = lim s iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - b₂).| < p );

theorem Th9: :: COMSEQ_2:9

for s being Complex_Sequence st ex g being Complex st
for n being Nat holds s . n = g holds
s is convergent

proof end;

theorem Th10: :: COMSEQ_2:10

for s being Complex_Sequence
for g being Complex st ( for n being Nat holds s . n = g ) holds
lim s = g

proof end;

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 b₁ being Complex_Sequence st b₁ is convergent

proof end;

end;

registration

let s be convergent Complex_Sequence;

cluster s *' -> convergent for Complex_Sequence;

coherence
for b₁ being Complex_Sequence st b₁ = s *' holds
b₁ is convergent

proof end;

end;

theorem :: COMSEQ_2:11

canceled;

::$CT

theorem Th11: :: COMSEQ_2:12

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

proof end;

registration

let s1, s2 be convergent Complex_Sequence;

cluster s1 + s2 -> convergent for Complex_Sequence;

coherence
for b₁ being Complex_Sequence st b₁ = s1 + s2 holds
b₁ is convergent

proof end;

end;

theorem :: COMSEQ_2:13

canceled;

::$CT

theorem Th12: :: 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;

::$CT

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;

cluster c (#) s -> convergent for Complex_Sequence;

coherence
for b₁ being Complex_Sequence st b₁ = c (#) s holds
b₁ is convergent

proof end;

end;

theorem :: COMSEQ_2:17

canceled;

::$CT

theorem Th14: :: COMSEQ_2:18

for s being convergent Complex_Sequence
for r being Complex holds lim (r (#) s) = r * (lim s)

proof end;

theorem :: COMSEQ_2:19

canceled;

::$CT

theorem :: COMSEQ_2:20

for r being 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 b₁ being Complex_Sequence st b₁ = - s holds
b₁ is convergent ;

end;

theorem :: COMSEQ_2:21

canceled;

::$CT

theorem Th16: :: COMSEQ_2:22

for s being convergent Complex_Sequence holds lim (- s) = - (lim s)

proof end;

theorem :: COMSEQ_2:23

canceled;

::$CT

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 b₁ being Complex_Sequence st b₁ = s1 - s2 holds
b₁ is convergent

proof end;

end;

theorem :: COMSEQ_2:25

canceled;

::$CT

theorem Th18: :: 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;

::$CT

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 b₁ being Complex_Sequence st b₁ is convergent holds
b₁ 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 b₁ being Complex_Sequence st not b₁ is bounded holds
not b₁ is convergent ;

end;

registration

let s1, s2 be convergent Complex_Sequence;

cluster s1 (#) s2 -> convergent for Complex_Sequence;

coherence
for b₁ being Complex_Sequence st b₁ = s1 (#) s2 holds
b₁ is convergent

proof end;

end;

theorem :: COMSEQ_2:29

canceled;

::$CT

theorem Th20: :: 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;

::$CT

theorem :: COMSEQ_2:32

for s, s9 being convergent Complex_Sequence holds lim ((s (#) s9) *') = ((lim s) *') * ((lim s9) *')

proof end;

theorem Th22: :: COMSEQ_2:33

for s being convergent Complex_Sequence st lim s <> 0c holds
ex n being Nat st
for m being Nat st n <= m holds
|.(lim s).| / 2 < |.(s . m).|

proof end;

theorem Th23: :: COMSEQ_2:34

for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero holds
s " is convergent

proof end;

theorem Th24: :: 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;

::$CT

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 Th26: :: COMSEQ_2:38

for s, s9 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 Th27: :: COMSEQ_2:39

for s, s9 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;

::$CT

theorem :: COMSEQ_2:41

for s, s9 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 Th29: :: 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 Th30: :: 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;

::$CT

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;