:: The Series on {B}anach Algebra
:: by Yasunari Shidama
::
:: Received February 3, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: LOPBAN_3:1
for X being non empty right_complementable add-associative right_zeroed NORMSTR
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
proofend;

definition
let X be RealNormSpace;
let seq be sequence of X;
attrseq is summable  means :Def1: :: LOPBAN_3:def 1
 Partial_Sums seq is convergent ;
end;

:: deftheorem Def1 defines summable LOPBAN_3:def_1_:_
 for X being RealNormSpace
for seq being sequence of X holds
( seq is summable iff Partial_Sums seq is convergent );

registration
let X be RealNormSpace;
clusterV4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) summable for Element of K32(K33(NAT, the carrier of X));
existence
 ex b1 being sequence of X st b1 is summable
proofend;
end;

definition
let X be RealNormSpace;
let seq be sequence of X;
func Sum seq ->  Element of X equals :: LOPBAN_3:def 2
 lim (Partial_Sums seq);
correctness
coherence
lim (Partial_Sums seq) is Element of X;
;
end;

:: deftheorem  defines Sum LOPBAN_3:def_2_:_
 for X being RealNormSpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);

definition
let X be RealNormSpace;
let seq be sequence of X;
attrseq is norm_summable  means :Def3: :: LOPBAN_3:def 3
||.seq.|| is summable ;
end;

:: deftheorem Def3 defines norm_summable LOPBAN_3:def_3_:_
 for X being RealNormSpace
for seq being sequence of X holds
( seq is norm_summable iff ||.seq.|| is summable );

theorem Th2: :: LOPBAN_3:2
for X being RealNormSpace
for seq being sequence of X
for m being Element of NAT holds 0 <= ||.seq.|| . m
proofend;

theorem Th3: :: LOPBAN_3:3
for X being RealNormSpace
for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).||
proofend;

theorem Th4: :: LOPBAN_3:4
for X being RealNormSpace
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
proofend;

theorem Th5: :: LOPBAN_3:5
for X being RealNormSpace
for seq being sequence of X holds
( seq is Cauchy_sequence_by_Norm 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 )
proofend;

theorem Th6: :: LOPBAN_3:6
for X being RealNormSpace
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
proofend;

theorem Th7: :: LOPBAN_3:7
for X being RealNormSpace
for seq, seq1 being sequence of X st seq1 is subsequence of seq &amp; seq is convergent holds
seq1 is convergent
proofend;

theorem Th8: :: LOPBAN_3:8
for X being RealNormSpace
for seq, seq1 being sequence of X st seq1 is subsequence of seq &amp; seq is convergent holds
lim seq1 = lim seq
proofend;

:: Norm Space versions of SEQ_4_33 - SEQ_4_39
theorem :: LOPBAN_3:9
for X being RealNormSpace
for seq, seq1 being sequence of X
for k being Element of NAT st seq is convergent holds
( seq ^\ k is convergent &amp; lim (seq ^\ k) = lim seq ) by Th7, Th8;

theorem Th10: :: LOPBAN_3:10
for X being RealNormSpace
for seq, seq1 being sequence of X st seq is convergent &amp; ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is convergent
proofend;

theorem Th11: :: LOPBAN_3:11
for X being RealNormSpace
for seq, seq1 being sequence of X st seq is convergent &amp; ex k being Element of NAT st seq = seq1 ^\ k holds
lim seq1 = lim seq
proofend;

theorem Th12: :: LOPBAN_3:12
for X being RealNormSpace
for seq being sequence of X st seq is constant holds
seq is convergent
proofend;

theorem Th13: :: LOPBAN_3:13
for X being RealNormSpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
seq is norm_summable
proofend;

registration
let X be RealNormSpace;
clusterV4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) norm_summable for Element of K32(K33(NAT, the carrier of X));
existence
 ex b1 being sequence of X st b1 is norm_summable
proofend;
end;

:: Norm Space versions of SERIES_1_7 - SERIES_1_16
theorem Th14: :: LOPBAN_3:14
for X being RealNormSpace
for s being sequence of X st s is summable holds
( s is convergent &amp; lim s = 0. X )
proofend;

theorem Th15: :: LOPBAN_3:15
for X being RealNormSpace
for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)
proofend;

theorem Th16: :: LOPBAN_3:16
for X being RealNormSpace
for s1, s2 being sequence of X holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
proofend;

registration
let X be RealNormSpace;
let seq be norm_summable sequence of X;
cluster||.seq.|| ->  summable for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = ||.seq.|| holds
b1 is summable by Def3;
end;

registration
let X be RealNormSpace;
cluster Function-like V30( NAT , the carrier of X) summable  ->  convergent for Element of K32(K33(NAT, the carrier of X));
coherence
 for b1 being sequence of X st b1 is summable holds
b1 is convergent by Th14;
end;

theorem Th17: :: LOPBAN_3:17
for X being RealNormSpace
for seq1, seq2 being sequence of X st seq1 is summable &amp; seq2 is summable holds
( seq1 + seq2 is summable &amp; Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
proofend;

theorem Th18: :: LOPBAN_3:18
for X being RealNormSpace
for seq1, seq2 being sequence of X st seq1 is summable &amp; seq2 is summable holds
( seq1 - seq2 is summable &amp; Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
proofend;

registration
let X be RealNormSpace;
let seq1, seq2 be summable sequence of X;
clusterseq1 + seq2 ->  summable ;
coherence
 seq1 + seq2 is summable by Th17;
clusterseq1 - seq2 ->  summable ;
coherence
 seq1 - seq2 is summable by Th18;
end;

theorem Th19: :: LOPBAN_3:19
for X being RealNormSpace
for seq being sequence of X
for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
proofend;

theorem Th20: :: LOPBAN_3:20
for X being RealNormSpace
for seq being summable sequence of X
for z being Real holds
( z * seq is summable &amp; Sum (z * seq) = z * (Sum seq) )
proofend;

registration
let X be RealNormSpace;
let z be Real;
let seq be summable sequence of X;
clusterz * seq ->  summable ;
coherence
 z * seq is summable by Th20;
end;

theorem Th21: :: LOPBAN_3:21
for X being RealNormSpace
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
proofend;

theorem Th22: :: LOPBAN_3:22
for X being RealNormSpace
for s being sequence of X st s is summable holds
for n being Element of NAT holds s ^\ n is summable
proofend;

registration
let X be RealNormSpace;
let seq be summable sequence of X;
let n be Element of NAT ;
clusterseq ^\ n ->  summable for sequence of X;
coherence
 for b1 being sequence of X st b1 = seq ^\ n holds
b1 is summable by Th22;
end;

theorem Th23: :: LOPBAN_3:23
for X being RealNormSpace
for seq being sequence of X holds
( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable )
proofend;

registration
let X be RealNormSpace;
let seq be norm_summable sequence of X;
cluster Partial_Sums ||.seq.|| ->  bounded_above for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = Partial_Sums ||.seq.|| holds
b1 is bounded_above by Th23;
end;

theorem Th24: :: LOPBAN_3:24
for X being RealBanachSpace
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 )
proofend;

theorem Th25: :: LOPBAN_3:25
for X being RealNormSpace
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))
proofend;

theorem Th26: :: LOPBAN_3:26
for X being RealBanachSpace
for seq being sequence of X st seq is norm_summable holds
seq is summable
proofend;

theorem :: LOPBAN_3:27
for X being RealNormSpace
for rseq1 being Real_Sequence
for seq2 being sequence of X st rseq1 is summable &amp; 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
proofend;

theorem :: LOPBAN_3:28
for X being RealNormSpace
for seq1, seq2 being sequence of X st ( for n being Element of NAT holds
( 0 <= ||.seq1.|| . n &amp; ||.seq1.|| . n <= ||.seq2.|| . n ) ) &amp; seq2 is norm_summable holds
( seq1 is norm_summable &amp; Sum ||.seq1.|| <= Sum ||.seq2.|| )
proofend;

theorem :: LOPBAN_3:29
for X being RealNormSpace
for seq being sequence of X st ( for n being Element of NAT holds ||.seq.|| . n > 0 ) &amp; 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:27;

theorem :: LOPBAN_3:30
for X being RealNormSpace
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) ) &amp; rseq1 is convergent &amp; lim rseq1 < 1 holds
seq is norm_summable
proofend;

theorem :: LOPBAN_3:31
for X being RealNormSpace
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) ) &amp; 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
proofend;

theorem :: LOPBAN_3:32
for X being RealNormSpace
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) ) &amp; rseq1 is convergent &amp; lim rseq1 > 1 holds
not seq is norm_summable
proofend;

theorem :: LOPBAN_3:33
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ||.seq.|| is non-increasing &amp; ( 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 )
proofend;

theorem :: LOPBAN_3:34
for X being RealNormSpace
for seq being sequence of X
for p being Real st p > 1 &amp; ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
seq is norm_summable
proofend;

theorem :: LOPBAN_3:35
for X being RealNormSpace
for seq being sequence of X
for p being Real st p <= 1 &amp; ( 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:33;

theorem :: LOPBAN_3:36
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds
( seq . n <> 0. X &amp; rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) &amp; rseq1 is convergent &amp; lim rseq1 < 1 holds
seq is norm_summable
proofend;

theorem :: LOPBAN_3:37
for X being RealNormSpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) &amp; 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
proofend;

registration
let X be RealBanachSpace;
cluster Function-like V30( NAT , the carrier of X) norm_summable  ->  summable for Element of K32(K33(NAT, the carrier of X));
coherence
 for b1 being sequence of X st b1 is norm_summable holds
b1 is summable by Th26;
end;

begin

theorem Th38: :: LOPBAN_3:38
for X being Banach_Algebra
for x, y, z being Element of X
for a, b being Real holds
( x + y = y + x &amp; (x + y) + z = x + (y + z) &amp; x + (0. X) = x &amp; ex t being Element of X st x + t = 0. X &amp; (x * y) * z = x * (y * z) &amp; 1 * x = x &amp; 0 * x = 0. X &amp; a * (0. X) = 0. X &amp; (- 1) * x = - x &amp; x * (1. X) = x &amp; (1. X) * x = x &amp; x * (y + z) = (x * y) + (x * z) &amp; (y + z) * x = (y * x) + (z * x) &amp; a * (x * y) = (a * x) * y &amp; a * (x + y) = (a * x) + (a * y) &amp; (a + b) * x = (a * x) + (b * x) &amp; (a * b) * x = a * (b * x) &amp; (a * b) * (x * y) = (a * x) * (b * y) &amp; a * (x * y) = x * (a * y) &amp; (0. X) * x = 0. X &amp; x * (0. X) = 0. X &amp; x * (y - z) = (x * y) - (x * z) &amp; (y - z) * x = (y * x) - (z * x) &amp; (x + y) - z = x + (y - z) &amp; (x - y) + z = x - (y - z) &amp; (x - y) - z = x - (y + z) &amp; x + y = (x - z) + (z + y) &amp; x - y = (x - z) + (z - y) &amp; x = (x - y) + y &amp; x = y - (y - x) &amp; ( ||.x.|| = 0 implies x = 0. X ) &amp; ( x = 0. X implies ||.x.|| = 0 ) &amp; ||.(a * x).|| = (abs a) * ||.x.|| &amp; ||.(x + y).|| <= ||.x.|| + ||.y.|| &amp; ||.(x * y).|| <= ||.x.|| * ||.y.|| &amp; ||.(1. X).|| = 1 &amp; X is complete )
proofend;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like V150() associative right-distributive right_unital Banach_Algebra-like  ->  well-unital for Normed_AlgebraStr ;
coherence
 for b1 being Banach_Algebra holds b1 is well-unital
proofend;
end;

definition
let X be non empty associative well-unital multLoopStr ;
let v be Element of X;
redefine attr v is invertible  means :Def4: :: LOPBAN_3:def 4
 ex w being Element of X st
( v * w = 1. X &amp; w * v = 1. X );
compatibility
 ( v is invertible iff ex w being Element of X st
( v * w = 1. X &amp; w * v = 1. X ) )
proofend;
end;

:: deftheorem Def4 defines invertible LOPBAN_3:def_4_:_
 for X being non empty associative well-unital multLoopStr
for v being Element of X holds
( v is invertible iff ex w being Element of X st
( v * w = 1. X &amp; w * v = 1. X ) );

definition
let X be non empty Normed_AlgebraStr ;
let S be sequence of X;
let a be Element of X;
funca * S ->  sequence of X means :: LOPBAN_3:def 5
 for n being Element of NAT holds it . n = a * (S . n);
existence
 ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = a * (S . n)
proofend;
uniqueness
 for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = a * (S . n) ) &amp; ( for n being Element of NAT holds b2 . n = a * (S . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines * LOPBAN_3:def_5_:_
 for X being non empty Normed_AlgebraStr
for S being sequence of X
for a being Element of X
for b4 being sequence of X holds
( b4 = a * S iff for n being Element of NAT holds b4 . n = a * (S . n) );

definition
let X be non empty Normed_AlgebraStr ;
let S be sequence of X;
let a be Element of X;
funcS * a ->  sequence of X means :: LOPBAN_3:def 6
 for n being Element of NAT holds it . n = (S . n) * a;
existence
 ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (S . n) * a
proofend;
uniqueness
 for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (S . n) * a ) &amp; ( for n being Element of NAT holds b2 . n = (S . n) * a ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines * LOPBAN_3:def_6_:_
 for X being non empty Normed_AlgebraStr
for S being sequence of X
for a being Element of X
for b4 being sequence of X holds
( b4 = S * a iff for n being Element of NAT holds b4 . n = (S . n) * a );

definition
let X be non empty Normed_AlgebraStr ;
let seq1, seq2 be sequence of X;
funcseq1 * seq2 ->  sequence of X means :: LOPBAN_3:def 7
 for n being Element of NAT holds it . n = (seq1 . n) * (seq2 . n);
existence
 ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (seq1 . n) * (seq2 . n)
proofend;
uniqueness
 for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (seq1 . n) * (seq2 . n) ) &amp; ( for n being Element of NAT holds b2 . n = (seq1 . n) * (seq2 . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines * LOPBAN_3:def_7_:_
 for X being non empty Normed_AlgebraStr
for seq1, seq2, b4 being sequence of X holds
( b4 = seq1 * seq2 iff for n being Element of NAT holds b4 . n = (seq1 . n) * (seq2 . n) );

notation
let X be non empty associative well-unital multLoopStr ;
let x be Element of X;
synonym x " for  / x;
end;

definition
let X be non empty associative well-unital multLoopStr ;
let x be Element of X;
assume B1: x is invertible ;
redefine func / x means :Def8: :: LOPBAN_3:def 8
( x * it = 1. X &amp; it * x = 1. X );
compatibility
 for b1 being Element of the carrier of X holds
( b1 = x " iff ( x * b1 = 1. X &amp; b1 * x = 1. X ) )
proofend;
end;

:: deftheorem Def8 defines " LOPBAN_3:def_8_:_
 for X being non empty associative well-unital multLoopStr
for x being Element of X st x is invertible holds
for b3 being Element of the carrier of X holds
( b3 = x " iff ( x * b3 = 1. X &amp; b3 * x = 1. X ) );

definition
let X be Banach_Algebra;
let z be Element of X;
funcz GeoSeq  ->  sequence of X means :Def9: :: LOPBAN_3:def 9
( it . 0 = 1. X &amp; ( for n being Element of NAT holds it . (n + 1) = (it . n) * z ) );
existence
 ex b1 being sequence of X st
( b1 . 0 = 1. X &amp; ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) )
proofend;
uniqueness
 for b1, b2 being sequence of X st b1 . 0 = 1. X &amp; ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) &amp; b2 . 0 = 1. X &amp; ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * z ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines GeoSeq LOPBAN_3:def_9_:_
 for X being Banach_Algebra
for z being Element of X
for b3 being sequence of X holds
( b3 = z GeoSeq iff ( b3 . 0 = 1. X &amp; ( for n being Element of NAT holds b3 . (n + 1) = (b3 . n) * z ) ) );

definition
let X be Banach_Algebra;
let z be Element of X;
let n be Element of NAT ;
funcz #N n ->  Element of X equals :: LOPBAN_3:def 10
(z GeoSeq) . n;
correctness
coherence
(z GeoSeq) . n is Element of X;
;
end;

:: deftheorem  defines #N LOPBAN_3:def_10_:_
 for X being Banach_Algebra
for z being Element of X
for n being Element of NAT holds z #N n = (z GeoSeq) . n;

theorem :: LOPBAN_3:39
for X being Banach_Algebra
for z being Element of X holds z #N 0 = 1. X by Def9;

theorem Th40: :: LOPBAN_3:40
for X being Banach_Algebra
for z being Element of X st ||.z.|| < 1 holds
( z GeoSeq is summable &amp; z GeoSeq is norm_summable )
proofend;

theorem :: LOPBAN_3:41
for X being Banach_Algebra
for x being Point of X st ||.((1. X) - x).|| < 1 holds
( ((1. X) - x) GeoSeq is summable &amp; ((1. X) - x) GeoSeq is norm_summable ) by Th40;

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

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

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

theorem :: LOPBAN_3:42
for X being Banach_Algebra
for x being Point of X st ||.((1. X) - x).|| < 1 holds
( x is invertible &amp; x " = Sum (((1. X) - x) GeoSeq) )
proofend;