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 :: LOPBAN_3:30 for X be RealNormSpace for seq be sequence of X for 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 :: LOPBAN_3:31 for X be RealNormSpace for seq be sequence of X for 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 :: LOPBAN_3:32 for X be RealNormSpace for seq be sequence of X for 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 :: LOPBAN_3:33 for X be RealNormSpace for seq be sequence of X for 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 :: LOPBAN_3:34 for X be RealNormSpace for seq be sequence of X for 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 :: LOPBAN_3:35 for X be RealNormSpace for seq be sequence of X for 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 :: LOPBAN_3:36 for X be RealNormSpace for seq be sequence of X for 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 :: LOPBAN_3:37 for X be RealNormSpace for 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 RealBanachSpace; cluster norm_summable -> summable for sequence of X; end; begin :: Basic Properties of Sequence of Banach_Algebra theorem :: LOPBAN_3:38 for X be Banach_Algebra holds for x,y,z being Element of X for a,b be Real 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) & 1*x=x & 0*x=0.X & a*0.X =0.X& (-1)*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 iff x = 0.X ) & ||.a * x.|| = |.a.| * ||.x.|| & ||.x + y.|| <= ||. x.|| + ||.y.|| & ||. x*y .|| <= ||.x.|| * ||.y.|| & ||. 1.X .|| = 1 & X is complete; registration cluster -> well-unital for Banach_Algebra; end; definition let X be well-unital associative non empty multLoopStr; let v be Element of X; redefine attr v is invertible means :: LOPBAN_3:def 4 ex w be Element of X st v*w = 1.X & w*v=1.X; end; definition let X be non empty multMagma; let S be sequence of X; let a be Element of X; func a * S -> sequence of X means :: LOPBAN_3:def 5 for n being Nat holds it.n = a * S .n; func S*a -> sequence of X means :: LOPBAN_3:def 6 for n being Nat holds it.n = S.n*a; end; definition let X be non empty multMagma; let seq1,seq2 be sequence of X; func seq1 * seq2 -> sequence of X means :: LOPBAN_3:def 7 for n being Nat holds it.n = seq1.n * seq2.n; end; notation let X be associative well-unital non empty multLoopStr; let x be Element of X; synonym x" for /x; end; definition let X be associative well-unital non empty multLoopStr; let x be Element of X such that x is invertible; redefine func x" means :: LOPBAN_3:def 8 x*it= 1.X & it*x= 1.X; end; definition let X be Banach_Algebra; let z be Element of X; func z GeoSeq -> sequence of X means :: LOPBAN_3:def 9 it.0 = 1.X & for n be Nat holds it.(n+1) = it.n * z; end; definition let X be Banach_Algebra; let z be Element of X, n be Nat; func z #N n -> Element of X equals :: LOPBAN_3:def 10 z GeoSeq.n; end; theorem :: LOPBAN_3:39 for X be Banach_Algebra for z be Element of X holds z #N 0 = 1.X; theorem :: LOPBAN_3:40 for X be Banach_Algebra for z be Element of X holds ||.z.|| < 1 implies z GeoSeq is summable norm_summable; theorem :: LOPBAN_3:41 for X be Banach_Algebra for 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 :: LOPBAN_3:42 for X be Banach_Algebra for x be Point of X st ||.1.X - x .|| < 1 holds x is invertible & x" = Sum ((1.X - x) GeoSeq );