0) & (ex m be Nat st for n be Nat st n >=m holds ||.seq.||.(n+1)/||.seq.||.n >= 1) implies not seq is norm_summable; theorem :: CLOPBAN3:30 for X be ComplexNormSpace, seq be sequence of X, rseq1 be Real_Sequence holds (for n be Nat holds rseq1.n = n-root (||.seq.||. n)) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable; theorem :: CLOPBAN3:31 for X be ComplexNormSpace, seq be sequence of X, rseq1 be Real_Sequence holds (for n be Nat holds rseq1.n = n-root (||.seq.||. n)) & (ex m be Nat st for n be Nat st m<=n holds rseq1.n >= 1) implies ||.seq.|| is not summable; theorem :: CLOPBAN3:32 for X be ComplexNormSpace, seq be sequence of X, rseq1 be Real_Sequence holds (for n be Nat holds rseq1.n = n-root (||.seq.||. n)) & rseq1 is convergent & lim rseq1 > 1 implies seq is not norm_summable; theorem :: CLOPBAN3:33 for X be ComplexNormSpace, seq be sequence of X, rseq1 be Real_Sequence st ||.seq.|| is non-increasing & (for n be Nat holds rseq1.n = 2 to_power n *||.seq.||.(2 to_power n)) holds (seq is norm_summable iff rseq1 is summable); theorem :: CLOPBAN3:34 for X be ComplexNormSpace, seq be sequence of X, p be Real st p>1 & ( for n be Nat st n >=1 holds ||.seq.||.n = 1/ (n to_power p) ) holds seq is norm_summable; theorem :: CLOPBAN3:35 for X be ComplexNormSpace, seq be sequence of X, p be Real holds p<=1 & (for n be Nat st n >=1 holds ||.seq.||.n=1/n to_power p) implies not seq is norm_summable; theorem :: CLOPBAN3:36 for X be ComplexNormSpace, seq be sequence of X, rseq1 be Real_Sequence holds (for n be Nat holds seq.n<>0.X & rseq1.n=||.seq .||.(n+1)/||.seq.||.n) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable; theorem :: CLOPBAN3:37 for X be ComplexNormSpace, seq be sequence of X holds (for n be Nat holds seq.n<>0.X) & (ex m be Nat st for n be Nat st n >=m holds ||.seq.||.(n+1)/||.seq.||.n >= 1) implies seq is not norm_summable; registration let X be ComplexBanachSpace; cluster norm_summable -> summable for sequence of X; end; begin :: Basic Properties of Sequence of Complex_Banach_Algebra theorem :: CLOPBAN3:38 for X be Complex_Banach_Algebra holds for x,y,z being Element of X, a,b be Complex holds 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 iff x = 0.X ) & ||.a * x.|| = |.a.| * ||.x.|| & ||.x + y .|| <= ||.x.|| + ||.y.|| & ||. x*y .|| <= ||.x.|| * ||.y.|| & ||. 1.X .|| = 1; registration cluster -> well-unital for Complex_Banach_Algebra; end; definition ::$CD 3 end; definition let X be Complex_Banach_Algebra; let z be Element of X; func z GeoSeq -> sequence of X means :: CLOPBAN3:def 7 it.0 = 1.X & for n be Nat holds it.(n+1) = it.n * z; end; definition let X be Complex_Banach_Algebra; let z be Element of X, n be Nat; func z #N n -> Element of X equals :: CLOPBAN3:def 8 z GeoSeq.n; end; theorem :: CLOPBAN3:39 for X be Complex_Banach_Algebra, z be Element of X holds z #N 0 = 1.X; theorem :: CLOPBAN3:40 for X be Complex_Banach_Algebra, z be Element of X holds ||.z.|| < 1 implies z GeoSeq is summable norm_summable; theorem :: CLOPBAN3:41 for X be Complex_Banach_Algebra, x be Point of X st ||.1.X - x .|| < 1 holds (1.X - x) GeoSeq is summable & (1.X - x) GeoSeq is norm_summable; theorem :: CLOPBAN3:42 for X be Complex_Banach_Algebra, x be Point of X st ||.1.X - x .|| < 1 holds x is invertible & x" = Sum ((1.X - x) GeoSeq );