:: 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.|)

|.((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 ) )

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 H_{1}( set ) -> Element of COMPLEX = (f . $1) *' ;

ex b_{1} being complex-valued Function st

( dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f . c) *' ) )

for b_{1}, b_{2} being complex-valued Function st dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f . c) *' ) & dom b_{2} = dom f & ( for c being set st c in dom b_{2} holds

b_{2} . c = (f . c) *' ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being complex-valued Function st dom b_{1} = dom b_{2} & ( for c being set st c in dom b_{1} holds

b_{1} . c = (b_{2} . c) *' ) holds

( dom b_{2} = dom b_{1} & ( for c being set st c in dom b_{2} holds

b_{2} . c = (b_{1} . c) *' ) )

end;
deffunc H

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 ( dom it = dom f & ( for c being set st c in dom it holds

it . c = (f . c) *' ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

involutiveness for b

b

( dom b

b

proof end;

:: deftheorem Def1 defines *' COMSEQ_2:def 1 :

for f, b_{2} being complex-valued Function holds

( b_{2} = f *' iff ( dom b_{2} = dom f & ( for c being set st c in dom b_{2} holds

b_{2} . c = (f . c) *' ) ) );

for f, b

( b

b

definition

let C be non empty set ;

let f be Function of C,COMPLEX;

f *' is Function of C,COMPLEX

for b_{1} being Function of C,COMPLEX holds

( b_{1} = f *' iff ( dom b_{1} = C & ( for n being Element of C holds b_{1} . n = (f . n) *' ) ) )

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

f *' is Function of C,COMPLEX

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def2 defines *' COMSEQ_2:def 2 :

for C being non empty set

for f, b_{3} being Function of C,COMPLEX holds

( b_{3} = f *' iff ( dom b_{3} = C & ( for n being Element of C holds b_{3} . n = (f . n) *' ) ) );

for C being non empty set

for f, b

( b

registration

let C be non empty set ;

let s be complex-valued ManySortedSet of C;

coherence

s *' is C -defined

end;
let s be complex-valued ManySortedSet of C;

coherence

s *' is C -defined

proof end;

registration

let C be non empty set ;

let seq be complex-valued ManySortedSet of C;

coherence

for b_{1} being C -defined Function st b_{1} = seq *' holds

b_{1} is total

end;
let seq be complex-valued ManySortedSet of C;

coherence

for b

b

proof end;

begin

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

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;

( s is bounded iff ex r being Real st

for n being Element of NAT holds |.(s . n).| < r )

end;
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 ex r being Real st

for n being Element of NAT holds |.(s . n).| < r;

( s is bounded iff ex r being Real st

for n being Element of NAT holds |.(s . n).| < r )

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

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

ex b_{1} being Complex_Sequence st b_{1} is bounded
end;

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

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

( 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

:: The Limit of Complex Sequences

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

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 ;

ex b_{1} 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_{1}).| < p
by A1, Def5;

uniqueness

for b_{1}, b_{2} 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_{1}).| < 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_{2}).| < p ) holds

b_{1} = b_{2}

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

ex b

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

uniqueness

for b

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

|.((s . m) - b

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

|.((s . m) - b

b

proof end;

:: deftheorem Def6 defines lim COMSEQ_2:def 6 :

for s being Complex_Sequence st s is convergent holds

for b_{2} being Element of COMPLEX holds

( b_{2} = 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_{2}).| < p );

for s being Complex_Sequence st s is convergent holds

for b

( b

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

|.((s . m) - b

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

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

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

ex b_{1} being Complex_Sequence st b_{1} is convergent
by Lm1, Th9;

end;

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

registration

let s be convergent Complex_Sequence;

coherence

for b_{1} being Complex_Sequence st b_{1} = s *' holds

b_{1} is convergent

end;
coherence

for b

b

proof end;

begin

registration

let s1, s2 be convergent Complex_Sequence;

coherence

for b_{1} being Complex_Sequence st b_{1} = s1 + s2 holds

b_{1} is convergent

end;
coherence

for b

b

proof end;

registration

let s be convergent Complex_Sequence;

let c be complex number ;

coherence

for b_{1} being Complex_Sequence st b_{1} = c (#) s holds

b_{1} is convergent

end;
let c be complex number ;

coherence

for b

b

proof end;

theorem Th18: :: COMSEQ_2:18

for s being convergent Complex_Sequence

for r being complex number holds lim (r (#) s) = r * (lim s)

for r being complex number holds lim (r (#) s) = r * (lim s)

proof end;

theorem :: COMSEQ_2:20

for r being Element of COMPLEX

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

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

proof end;

registration

let s be convergent Complex_Sequence;

coherence

for b_{1} being Complex_Sequence st b_{1} = - s holds

b_{1} is convergent
;

end;
coherence

for b

b

registration

let s1, s2 be convergent Complex_Sequence;

coherence

for b_{1} being Complex_Sequence st b_{1} = s1 - s2 holds

b_{1} is convergent

end;
coherence

for b

b

proof end;

registration

for b_{1} being Complex_Sequence st b_{1} is convergent holds

b_{1} is bounded
end;

cluster Function-like V18( NAT , COMPLEX ) convergent -> bounded for Element of K19(K20(NAT,COMPLEX));

coherence for b

b

proof end;

registration

for b_{1} being Complex_Sequence st not b_{1} is bounded holds

not b_{1} is convergent
;

end;

cluster Function-like V18( NAT , COMPLEX ) non bounded -> non convergent for Element of K19(K20(NAT,COMPLEX));

coherence for b

not b

registration

let s1, s2 be convergent Complex_Sequence;

coherence

for b_{1} being Complex_Sequence st b_{1} = s1 (#) s2 holds

b_{1} is convergent

end;
coherence

for b

b

proof end;

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

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

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

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

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)

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

lim ((s9 /" s) *') = ((lim s9) *') / ((lim s) *')

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

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

lim (s (#) s1) = 0c

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

lim ((s (#) s1) *') = 0c

proof end;