:: The Series on {B}anach Algebra :: by Yasunari Shidama :: :: Received February 3, 2004 :: Copyright (c) 2004-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, NORMSP_1, NAT_1, SUBSET_1, FUNCT_1, SUPINF_2, SERIES_1, ARYTM_3, CARD_1, SEQ_2, FUNCOP_1, REAL_1, XXREAL_0, ARYTM_1, CARD_3, ORDINAL2, RSSPACE3, VALUED_0, RELAT_1, COMPLEX1, XXREAL_2, LOPBAN_1, SEQ_1, POWER, LOPBAN_2, MESFUNC1, REWRITE1, VECTSP_1, BINOP_1, PREPOWER, STRUCT_0, COMSEQ_3, PRE_TOPC, VALUED_1, LOPBAN_3; notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, DOMAIN_1, FUNCOP_1, XREAL_0, XXREAL_0, XCMPLX_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, NUMBERS, RLVECT_1, GROUP_1, VECTSP_1, NORMSP_0, NORMSP_1, RSSPACE3, VALUED_1, SEQ_1, SEQ_2, VALUED_0, SERIES_1, PREPOWER, POWER, BHSP_4, LOPBAN_1, LOPBAN_2, RECDEF_1; constructors DOMAIN_1, REAL_1, COMPLEX1, SEQ_2, BINOP_2, PREPOWER, SERIES_1, BHSP_4, RSSPACE3, LOPBAN_2, GCD_1, RECDEF_1, RELSET_1, COMSEQ_2; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, NORMSP_1, LOPBAN_2, ALGSTR_0, GCD_1, VALUED_1, FUNCT_2, VALUED_0, FUNCOP_1, NORMSP_0, NAT_1, INT_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin theorem :: LOPBAN_3:1 for X be add-associative right_zeroed right_complementable non empty NORMSTR for seq be sequence of X st ( for n be Nat holds seq. n = 0.X) for m be Nat holds (Partial_Sums seq).m = 0.X; definition let X be RealNormSpace; let seq be sequence of X; attr seq is summable means :: LOPBAN_3:def 1 Partial_Sums seq is convergent; end; registration let X be RealNormSpace; cluster summable for sequence of X; 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; end; definition let X be RealNormSpace; let seq be sequence of X; attr seq is norm_summable means :: LOPBAN_3:def 3 ||.seq.|| is summable; end; theorem :: LOPBAN_3:2 for X be RealNormSpace for seq be sequence of X for m be Nat holds 0 <= ||.seq.||.m; theorem :: LOPBAN_3:3 for X be RealNormSpace for x,y,z be Element of X holds ||.x-y.|| = ||.(x-z)+(z-y).||; theorem :: LOPBAN_3:4 for X be RealNormSpace for seq be sequence of X holds seq is convergent implies for s be Real st 0 0 holds ex n be Nat st for m be Nat st n <= m holds ||.seq.m-seq.n.||< p; theorem :: LOPBAN_3:6 for X be RealNormSpace for seq be sequence of X st (for n be Nat holds seq.n = 0.X) for m be Nat holds (Partial_Sums ||.seq.||).m = 0; theorem :: LOPBAN_3:7 for X be RealNormSpace for seq,seq1 be sequence of X holds seq1 is subsequence of seq & seq is convergent implies seq1 is convergent; theorem :: LOPBAN_3:8 for X be RealNormSpace for seq,seq1 be sequence of X holds seq1 is subsequence of seq & seq is convergent implies lim seq1=lim seq; :: Norm Space versions of SEQ_4_33 - SEQ_4_39 theorem :: LOPBAN_3:9 for X be RealNormSpace for seq,seq1 be sequence of X for k be Nat holds seq is convergent implies (seq ^\k) is convergent & lim (seq ^\k)= lim seq; theorem :: LOPBAN_3:10 for X be RealNormSpace for seq,seq1 be sequence of X holds seq is convergent & (ex k be Nat st seq=seq1 ^\k) implies seq1 is convergent; theorem :: LOPBAN_3:11 for X be RealNormSpace for seq,seq1 be sequence of X holds seq is convergent & (ex k be Nat st seq=seq1 ^\k) implies lim seq1 =lim seq; theorem :: LOPBAN_3:12 for X be RealNormSpace for seq be sequence of X holds seq is constant implies seq is convergent; theorem :: LOPBAN_3:13 for X be RealNormSpace for seq be sequence of X st (for n be Nat holds seq.n = 0.X) holds seq is norm_summable; registration let X be RealNormSpace; cluster norm_summable for sequence of X; end; :: Norm Space versions of SERIES_1_7 - SERIES_1_16 theorem :: LOPBAN_3:14 for X be RealNormSpace for s be sequence of X holds s is summable implies s is convergent & lim s = 0.X; theorem :: LOPBAN_3:15 for X be RealNormSpace for s1,s2 be sequence of X holds Partial_Sums(s1)+Partial_Sums(s2) = Partial_Sums(s1+s2); theorem :: LOPBAN_3:16 for X be RealNormSpace for s1,s2 be sequence of X holds Partial_Sums(s1)-Partial_Sums(s2) = Partial_Sums(s1-s2); registration let X be RealNormSpace; let seq be norm_summable sequence of X; cluster ||.seq.|| -> summable for Real_Sequence; end; registration let X be RealNormSpace; cluster summable -> convergent for sequence of X; end; theorem :: LOPBAN_3:17 for X be RealNormSpace for seq1,seq2 be sequence of X st seq1 is summable & seq2 is summable holds seq1+seq2 is summable & Sum(seq1+seq2) = Sum( seq1)+Sum(seq2); theorem :: LOPBAN_3:18 for X be RealNormSpace for seq1,seq2 be sequence of X st seq1 is summable & seq2 is summable holds seq1-seq2 is summable & Sum(seq1-seq2)= Sum( seq1)-Sum(seq2); registration let X be RealNormSpace; let seq1, seq2 be summable sequence of X; cluster seq1 + seq2 -> summable; cluster seq1 - seq2 -> summable; end; theorem :: LOPBAN_3:19 for X be RealNormSpace for seq be sequence of X for z be Real holds Partial_Sums(z * seq) = z * Partial_Sums(seq); theorem :: LOPBAN_3:20 for X be RealNormSpace for seq be summable sequence of X for z be Real holds z *seq is summable & Sum(z *seq)= z * Sum(seq); registration let X be RealNormSpace; let z be Real, seq be summable sequence of X; cluster z *seq -> summable; end; theorem :: LOPBAN_3:21 for X be RealNormSpace for s,s1 be sequence of X st for n be Nat holds s1.n=s.0 holds Partial_Sums(s^\1) = (Partial_Sums(s)^\1) - s1; theorem :: LOPBAN_3:22 for X be RealNormSpace for s be sequence of X holds s is summable implies for n be Nat holds s^\n is summable; registration let X be RealNormSpace; let seq be summable sequence of X, n be Nat; cluster seq^\n -> summable for sequence of X; end; theorem :: LOPBAN_3:23 for X be RealNormSpace for seq be sequence of X holds Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable; registration let X be RealNormSpace; let seq be norm_summable sequence of X; cluster Partial_Sums ||.seq.|| -> bounded_above for Real_Sequence; end; theorem :: LOPBAN_3:24 for X be RealBanachSpace for seq be sequence of X holds seq is summable iff for p be Real st 0

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