:: Series on Complex {B}anach Algebra
:: by Noboru Endou
::
:: Received April 6, 2004
:: Copyright (c) 2004-2011 Association of Mizar Users

begin

theorem Th1: :: CLOPBAN3:1

for X being non empty right_complementable add-associative right_zeroed CNORMSTR
for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
for m being Element of NAT holds (Partial_Sums seq) . m = 0. X

proof end;

definition

let X be ComplexNormSpace;
canceled;
let seq be sequence of X;
attr seq is summable means :Def2: :: CLOPBAN3:def 2
Partial_Sums seq is convergent ;

end;

:: deftheorem CLOPBAN3:def 1 :
canceled;

:: deftheorem Def2 defines summable CLOPBAN3:def 2 :
for X being ComplexNormSpace
for seq being sequence of X holds
( seq is summable iff Partial_Sums seq is convergent );

registration

let X be ComplexNormSpace;
cluster V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V27( NAT , the carrier of X) summable Element of K18(K19(NAT, the carrier of X));
existence
ex b₁ being sequence of X st b₁ is summable

proof end;

end;

definition

let X be ComplexNormSpace;
let seq be sequence of X;
func Sum seq -> Element of X equals :: CLOPBAN3:def 3
lim (Partial_Sums seq);
correctness
coherence
lim (Partial_Sums seq) is Element of X;
;

end;

:: deftheorem defines Sum CLOPBAN3:def 3 :
for X being ComplexNormSpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);

definition

let X be ComplexNormSpace;
let seq be sequence of X;
attr seq is norm_summable means :Def4: :: CLOPBAN3:def 4
||.seq.|| is summable ;

end;

:: deftheorem Def4 defines norm_summable CLOPBAN3:def 4 :
for X being ComplexNormSpace
for seq being sequence of X holds
( seq is norm_summable iff ||.seq.|| is summable );

theorem Th2: :: CLOPBAN3:2

for X being ComplexNormSpace
for seq being sequence of X
for m being Element of NAT holds 0 <= ||.seq.|| . m

proof end;

theorem Th3: :: CLOPBAN3:3

for X being ComplexNormSpace
for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).||

proof end;

theorem Th4: :: CLOPBAN3:4

for X being ComplexNormSpace
for seq being sequence of X st seq is convergent holds
for s being Real st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < s

proof end;

theorem Th5: :: CLOPBAN3:5

for X being ComplexNormSpace
for seq being sequence of X holds
( seq is CCauchy iff for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p )

proof end;

theorem Th6: :: CLOPBAN3:6

for X being ComplexNormSpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
for m being Element of NAT holds (Partial_Sums ||.seq.||) . m = 0

proof end;

theorem :: CLOPBAN3:7

canceled;

theorem :: CLOPBAN3:8

canceled;

theorem :: CLOPBAN3:9

canceled;

theorem Th10: :: CLOPBAN3:10

for X being ComplexNormSpace
for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent

proof end;

theorem Th11: :: CLOPBAN3:11

for X being ComplexNormSpace
for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq

proof end;

theorem :: CLOPBAN3:12

canceled;

theorem :: CLOPBAN3:13

for X being ComplexNormSpace
for seq, seq1 being sequence of X
for k being Element of NAT st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th10, Th11;

theorem Th14: :: CLOPBAN3:14

for X being ComplexNormSpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is convergent

proof end;

theorem Th15: :: CLOPBAN3:15

for X being ComplexNormSpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds
lim seq1 = lim seq

proof end;

theorem Th16: :: CLOPBAN3:16

for X being ComplexNormSpace
for seq being sequence of X st seq is constant holds
seq is convergent

proof end;

theorem Th17: :: CLOPBAN3:17

for X being ComplexNormSpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
seq is norm_summable

proof end;

registration

let X be ComplexNormSpace;
cluster V1() Relation-like NAT -defined the carrier of X -valued Function-like V26( NAT ) V27( NAT , the carrier of X) norm_summable Element of K18(K19(NAT, the carrier of X));
existence
ex b₁ being sequence of X st b₁ is norm_summable

proof end;

end;

theorem Th18: :: CLOPBAN3:18

for X being ComplexNormSpace
for s being sequence of X st s is summable holds
( s is convergent & lim s = 0. X )

proof end;

theorem Th19: :: CLOPBAN3:19

for X being ComplexNormSpace
for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)

proof end;

theorem Th20: :: CLOPBAN3:20

for X being ComplexNormSpace
for s1, s2 being sequence of X holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)

proof end;

registration

let X be ComplexNormSpace;
let seq be norm_summable sequence of X;
cluster ||.seq.|| -> summable Real_Sequence;
coherence
for b₁ being Real_Sequence st b₁ = ||.seq.|| holds
b₁ is summable by Def4;

end;

registration

let X be ComplexNormSpace;
cluster Function-like V27( NAT , the carrier of X) summable -> convergent Element of K18(K19(NAT, the carrier of X));
coherence
for b₁ being sequence of X st b₁ is summable holds
b₁ is convergent by Th18;

end;

theorem Th21: :: CLOPBAN3:21

for X being ComplexNormSpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )

proof end;

theorem Th22: :: CLOPBAN3:22

for X being ComplexNormSpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )

proof end;

registration

let X be ComplexNormSpace;
let seq1, seq2 be summable sequence of X;
cluster seq1 + seq2 -> summable ;
coherence
seq1 + seq2 is summable by Th21;
cluster seq1 - seq2 -> summable ;
coherence
seq1 - seq2 is summable by Th22;

end;

theorem Th23: :: CLOPBAN3:23

for X being ComplexNormSpace
for seq being sequence of X
for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq)

proof end;

theorem Th24: :: CLOPBAN3:24

for X being ComplexNormSpace
for seq being summable sequence of X
for z being Complex holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )

proof end;

registration

let X be ComplexNormSpace;
let z be Complex;
let seq be summable sequence of X;
cluster z * seq -> summable ;
coherence
z * seq is summable by Th24;

end;

theorem Th25: :: CLOPBAN3:25

for X being ComplexNormSpace
for s, s1 being sequence of X st ( for n being Element of NAT holds s1 . n = s . 0 ) holds
Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1

proof end;

theorem Th26: :: CLOPBAN3:26

for X being ComplexNormSpace
for s being sequence of X st s is summable holds
for n being Element of NAT holds s ^\ n is summable

proof end;

registration

let X be ComplexNormSpace;
let seq be summable sequence of X;
let n be Element of NAT ;
cluster seq ^\ n -> summable ;
coherence
seq ^\ n is summable by Th26;

end;

theorem Th27: :: CLOPBAN3:27

for X being ComplexNormSpace
for seq being sequence of X holds
( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable )

proof end;

registration

let X be ComplexNormSpace;
let seq be norm_summable sequence of X;
cluster Partial_Sums ||.seq.|| -> bounded_above ;
coherence
Partial_Sums ||.seq.|| is bounded_above by Th27;

end;

theorem Th28: :: CLOPBAN3:28

for X being ComplexBanachSpace
for seq being sequence of X holds
( seq is summable 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
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p )

proof end;

theorem Th29: :: CLOPBAN3:29

for X being ComplexNormSpace
for s being sequence of X
for n, m being Element of NAT st n <= m holds
||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n))

proof end;

theorem Th30: :: CLOPBAN3:30

for X being ComplexBanachSpace
for seq being sequence of X st seq is norm_summable holds
seq is summable

proof end;

theorem :: CLOPBAN3:31

for X being ComplexNormSpace
for rseq1 being Real_Sequence
for seq2 being sequence of X st rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n holds
seq2 is norm_summable

proof end;

theorem :: CLOPBAN3:32

for X being ComplexNormSpace
for seq1, seq2 being sequence of X st ( for n being Element of NAT holds
( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable holds
( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| )

proof end;

theorem :: CLOPBAN3:33

for X being ComplexNormSpace
for seq being sequence of X st ( for n being Element of NAT holds ||.seq.|| . n > 0 ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 holds
not seq is norm_summable by SERIES_1:31;

theorem :: CLOPBAN3:34

for X being ComplexNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable

proof end;

theorem :: CLOPBAN3:35

for X being ComplexNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 holds
not ||.seq.|| is summable

proof end;

theorem :: CLOPBAN3:36

for X being ComplexNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds
not seq is norm_summable

proof end;

theorem :: CLOPBAN3:37

for X being ComplexNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds
( seq is norm_summable iff rseq1 is summable )

proof end;

theorem :: CLOPBAN3:38

for X being ComplexNormSpace
for seq being sequence of X
for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
seq is norm_summable

proof end;

theorem :: CLOPBAN3:39

for X being ComplexNormSpace
for seq being sequence of X
for p being Real st p <= 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
not seq is norm_summable by SERIES_1:37;

theorem :: CLOPBAN3:40

for X being ComplexNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable

proof end;

theorem :: CLOPBAN3:41

for X being ComplexNormSpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 holds
not seq is norm_summable

proof end;

registration

let X be ComplexBanachSpace;
cluster Function-like V27( NAT , the carrier of X) norm_summable -> summable Element of K18(K19(NAT, the carrier of X));
coherence
for b₁ being sequence of X st b₁ is norm_summable holds
b₁ is summable by Th30;

end;

begin

theorem Th42: :: CLOPBAN3:42

for X being Complex_Banach_Algebra
for x, y, z being Element of X
for a, b being Complex holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1r * x = x & 0c * x = 0. X & a * (0. X) = 0. X & (- 1r) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )

proof end;

registration

cluster non empty right_complementable Abelian add-associative right_zeroed V130() V131() V182() right-distributive right_unital vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like V221() V226() -> well-unital Normed_Complex_AlgebraStr ;
coherence
for b₁ being Complex_Banach_Algebra holds b₁ is well-unital

proof end;

end;

definition

let X be non empty Normed_Complex_AlgebraStr ;
let S be sequence of X;
let a be Element of X;
canceled;
canceled;
canceled;
func a * S -> sequence of X means :: CLOPBAN3:def 8
for n being Element of NAT holds it . n = a * (S . n);
existence
ex b₁ being sequence of X st
for n being Element of NAT holds b₁ . n = a * (S . n)

proof end;

uniqueness
for b₁, b₂ being sequence of X st ( for n being Element of NAT holds b₁ . n = a * (S . n) ) & ( for n being Element of NAT holds b₂ . n = a * (S . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem CLOPBAN3:def 5 :
canceled;

:: deftheorem CLOPBAN3:def 6 :
canceled;

:: deftheorem CLOPBAN3:def 7 :
canceled;

:: deftheorem defines * CLOPBAN3:def 8 :
for X being non empty Normed_Complex_AlgebraStr
for S being sequence of X
for a being Element of X
for b₄ being sequence of X holds
( b₄ = a * S iff for n being Element of NAT holds b₄ . n = a * (S . n) );

definition

let X be non empty Normed_Complex_AlgebraStr ;
let S be sequence of X;
let a be Element of X;
func S * a -> sequence of X means :: CLOPBAN3:def 9
for n being Element of NAT holds it . n = (S . n) * a;
existence
ex b₁ being sequence of X st
for n being Element of NAT holds b₁ . n = (S . n) * a

proof end;

uniqueness
for b₁, b₂ being sequence of X st ( for n being Element of NAT holds b₁ . n = (S . n) * a ) & ( for n being Element of NAT holds b₂ . n = (S . n) * a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines * CLOPBAN3:def 9 :
for X being non empty Normed_Complex_AlgebraStr
for S being sequence of X
for a being Element of X
for b₄ being sequence of X holds
( b₄ = S * a iff for n being Element of NAT holds b₄ . n = (S . n) * a );

definition

let X be non empty Normed_Complex_AlgebraStr ;
let seq1, seq2 be sequence of X;
func seq1 * seq2 -> sequence of X means :: CLOPBAN3:def 10
for n being Element of NAT holds it . n = (seq1 . n) * (seq2 . n);
existence
ex b₁ being sequence of X st
for n being Element of NAT holds b₁ . n = (seq1 . n) * (seq2 . n)

proof end;

uniqueness
for b₁, b₂ being sequence of X st ( for n being Element of NAT holds b₁ . n = (seq1 . n) * (seq2 . n) ) & ( for n being Element of NAT holds b₂ . n = (seq1 . n) * (seq2 . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines * CLOPBAN3:def 10 :
for X being non empty Normed_Complex_AlgebraStr
for seq1, seq2, b₄ being sequence of X holds
( b₄ = seq1 * seq2 iff for n being Element of NAT holds b₄ . n = (seq1 . n) * (seq2 . n) );

definition

let X be Complex_Banach_Algebra;
let z be Element of X;
canceled;
func z GeoSeq -> sequence of X means :Def12: :: CLOPBAN3:def 12
( it . 0 = 1. X & ( for n being Element of NAT holds it . (n + 1) = (it . n) * z ) );
existence
ex b₁ being sequence of X st
( b₁ . 0 = 1. X & ( for n being Element of NAT holds b₁ . (n + 1) = (b₁ . n) * z ) )

proof end;

uniqueness
for b₁, b₂ being sequence of X st b₁ . 0 = 1. X & ( for n being Element of NAT holds b₁ . (n + 1) = (b₁ . n) * z ) & b₂ . 0 = 1. X & ( for n being Element of NAT holds b₂ . (n + 1) = (b₂ . n) * z ) holds
b₁ = b₂

proof end;

end;

:: deftheorem CLOPBAN3:def 11 :
canceled;

:: deftheorem Def12 defines GeoSeq CLOPBAN3:def 12 :
for X being Complex_Banach_Algebra
for z being Element of X
for b₃ being sequence of X holds
( b₃ = z GeoSeq iff ( b₃ . 0 = 1. X & ( for n being Element of NAT holds b₃ . (n + 1) = (b₃ . n) * z ) ) );

definition

let X be Complex_Banach_Algebra;
let z be Element of X;
let n be Element of NAT ;
func z #N n -> Element of X equals :: CLOPBAN3:def 13
(z GeoSeq) . n;
correctness
coherence
(z GeoSeq) . n is Element of X;
;

end;

:: deftheorem defines #N CLOPBAN3:def 13 :
for X being Complex_Banach_Algebra
for z being Element of X
for n being Element of NAT holds z #N n = (z GeoSeq) . n;

theorem :: CLOPBAN3:43

for X being Complex_Banach_Algebra
for z being Element of X holds z #N 0 = 1. X by Def12;

theorem Th44: :: CLOPBAN3:44

for X being Complex_Banach_Algebra
for z being Element of X st ||.z.|| < 1 holds
( z GeoSeq is summable & z GeoSeq is norm_summable )

proof end;

theorem :: CLOPBAN3:45

for X being Complex_Banach_Algebra
for x being Point of X st ||.((1. X) - x).|| < 1 holds
( ((1. X) - x) GeoSeq is summable & ((1. X) - x) GeoSeq is norm_summable ) by Th44;

Lm1: for X being ComplexNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X

proof end;

Lm2: for X being ComplexNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y

proof end;

Lm3: for X being ComplexNormSpace
for x, y being Point of X
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) holds
x = y

proof end;

theorem :: CLOPBAN3:46

for X being Complex_Banach_Algebra
for x being Point of X st ||.((1. X) - x).|| < 1 holds
( x is invertible & x " = Sum (((1. X) - x) GeoSeq) )

proof end;