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