:: Series on Complex {B}anach Algebra :: by Noboru Endou :: :: Received April 6, 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, CLVECT_1, NAT_1, SUBSET_1, FUNCT_1, SUPINF_2, SERIES_1, ARYTM_3, CARD_1, SEQ_2, FUNCOP_1, REAL_1, XXREAL_0, NORMSP_1, ARYTM_1, CARD_3, ORDINAL2, LOPBAN_3, RSSPACE3, VALUED_0, RELAT_1, COMPLEX1, XCMPLX_0, XXREAL_2, CLOPBAN1, SEQ_1, POWER, CLOPBAN2, MESFUNC1, VECTSP_1, PREPOWER, STRUCT_0, COMSEQ_3, PRE_TOPC, VALUED_1; notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, DOMAIN_1, FUNCOP_1, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, NUMBERS, RLVECT_1, VECTSP_1, NORMSP_1, VALUED_1, SEQ_1, VALUED_0, SEQ_2, SERIES_1, PREPOWER, POWER, NORMSP_0, CLVECT_1, CSSPACE3, BHSP_4, CLOPBAN1, CLOPBAN2, LOPBAN_3, RECDEF_1; constructors DOMAIN_1, REAL_1, COMPLEX1, SEQ_2, PREPOWER, SERIES_1, BHSP_4, CSSPACE3, CLOPBAN2, RECDEF_1, RELSET_1, BINOP_2, COMSEQ_2, BINOP_1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, CLOPBAN2, VALUED_1, FUNCT_2, VALUED_0, FUNCOP_1, NORMSP_0, XCMPLX_0, NAT_1, INT_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions SEQ_2, SERIES_1, CLVECT_1, VECTSP_1; equalities BINOP_1, ALGSTR_0; expansions SERIES_1, CLVECT_1; theorems ABSVALUE, RLVECT_1, VECTSP_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1, NAT_1, INT_1, FUNCT_2, SEQ_4, PREPOWER, CLVECT_1, CSSPACE3, LOPBAN_3, CLOPBAN1, CFUNCDOM, CLOPBAN2, GROUP_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, BHSP_4, NORMSP_1, VALUED_0, NORMSP_0; schemes NAT_1; begin :: Basic Properties of Sequences of Complex Normed Space theorem Th1: for X be add-associative right_zeroed right_complementable non empty CNORMSTR for seq be sequence of X st (for n be Nat holds seq. n = 0.X) holds for m be Nat holds (Partial_Sums seq).m = 0.X proof let X be add-associative right_zeroed right_complementable non empty CNORMSTR; let seq be sequence of X such that A1: for n be Nat holds seq.n = 0.X; let m be Nat; defpred P[Nat] means seq.$1 = (Partial_Sums seq).$1; A2: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A3: P[k]; thus seq.(k+1) = 0.X + seq.(k+1) by RLVECT_1:4 .= (Partial_Sums seq).k + seq.(k+1) by A1,A3 .= (Partial_Sums seq).(k+1) by BHSP_4:def 1; end; A4: P[0] by BHSP_4:def 1; for n be Nat holds P[n] from NAT_1:sch 2(A4,A2); then for n be Element of NAT holds P[n]; then seq = Partial_Sums seq by FUNCT_2:63; hence thesis by A1; end; definition let X be ComplexNormSpace; let seq be sequence of X; attr seq is summable means :Def1: Partial_Sums seq is convergent; end; registration let X be ComplexNormSpace; cluster summable for sequence of X; existence proof reconsider C = NAT --> 0.X as sequence of X; take C; take 0.X; let p be Real such that A1: 0
Element of X equals
lim Partial_Sums seq;
correctness;
end;
definition
let X be ComplexNormSpace;
let seq be sequence of X;
attr seq is norm_summable means
:Def3:
||.seq.|| is summable;
end;
theorem Th2:
for X be ComplexNormSpace, seq be sequence of X,
m be Nat holds 0 <= ||.seq.||.m
proof
let X be ComplexNormSpace;
let seq be sequence of X;
let m be Nat;
||.seq.||.m = ||.seq.m.|| by NORMSP_0:def 4;
hence thesis by CLVECT_1:105;
end;
theorem Th3:
for X be ComplexNormSpace, x,y,z be Element of X holds ||.x-y.||
= ||.(x-z)+(z-y).||
proof
let X be ComplexNormSpace;
let x,y,z be Element of X;
thus ||.x-y.|| = ||.x-0.X-y.|| by RLVECT_1:13
.= ||.x-(z-z)-y.|| by RLVECT_1:5
.= ||.(x-z)+z-y.|| by RLVECT_1:29
.= ||.(x-z)+(z-y).|| by RLVECT_1:def 3;
end;
theorem Th4:
for X be ComplexNormSpace, seq be sequence of X holds seq is
convergent implies
for s be Real st 0 < s ex n be Nat st for m be
Nat st n<=m holds ||.seq.m -seq.n.|| 0 holds ex n be Nat
st for m be Nat st n <= m holds ||.seq.m-seq.n.||< p
proof
let X be ComplexNormSpace;
let seq be sequence of X;
A1: now
assume
A2: for p be Real st p > 0 holds ex n be Nat st for m be
Nat st n <= m holds ||.seq.m-seq.n.||< p;
now
let s be Real;
assume 0 0 holds ex n be Nat st for m be
Nat st n <= m holds ||.seq.m-seq.n.||< p
proof
let p be Real;
assume p >0;
then consider n be Nat such that
A9: for m,k be Nat st n <= m & n <=k holds ||.seq.m-seq.k
.||< p by A8,CSSPACE3:8;
for m be Nat st n <= m holds ||.seq.m-seq.n.||
0.X as sequence of X; take C; for n be Nat holds C.n = 0.X by ORDINAL1:def 12,FUNCOP_1:7; hence thesis by Th13; end; end; :: Norm Space versions of SERIES_1_7 - SERIES_1_16 theorem Th14: for X be ComplexNormSpace, s be sequence of X holds s is summable implies s is convergent & lim s = 0.X proof let X be ComplexNormSpace; let s be sequence of X; assume s is summable; then A1: Partial_Sums(s) is convergent; then A2: Partial_Sums(s) ^\1 is convergent by Th7; lim(Partial_Sums(s) ^\1) = lim(Partial_Sums(s)) by A1,Th8; then A3: lim(Partial_Sums(s) ^\1 - Partial_Sums(s)) = lim(Partial_Sums(s)) - lim( Partial_Sums(s)) by A1,A2,CLVECT_1:120 .= 0.X by RLVECT_1:15; now let n be Nat; (Partial_Sums(s)).(n+1) = (Partial_Sums(s)).n + s.(n+1) by BHSP_4:def 1; then (Partial_Sums(s)).(n+1) = (Partial_Sums(s)).n + (s ^\1).n by NAT_1:def 3; then (Partial_Sums(s) ^\1).n = (s ^\1).n+ (Partial_Sums(s)).n by NAT_1:def 3; then (Partial_Sums(s) ^\1).n- (Partial_Sums(s)).n = (s ^\1).n+ ( ( Partial_Sums(s)).n- (Partial_Sums(s)).n ) by RLVECT_1:def 3; then (Partial_Sums(s) ^\1).n- (Partial_Sums(s)).n = (s ^\1).n+ ( 0.X) by RLVECT_1:15; hence (Partial_Sums(s) ^\1).n- (Partial_Sums(s)).n = (s ^\1).n by RLVECT_1:4; end; then A4: s ^\1 = Partial_Sums(s) ^\1 - Partial_Sums(s) by NORMSP_1:def 3; then s ^\1 is convergent by A1,A2,CLVECT_1:114; hence thesis by A3,A4,Th10,Th11; end; theorem Th15: for X be ComplexNormSpace, s1,s2 be sequence of X holds Partial_Sums(s1)+Partial_Sums(s2) = Partial_Sums(s1+s2) proof let X be ComplexNormSpace; let s1,s2 be sequence of X; A1: now let n be Nat; thus (Partial_Sums(s1) + Partial_Sums(s2)).(n+1) = Partial_Sums(s1).(n+1) + Partial_Sums(s2).(n+1) by NORMSP_1:def 2 .= Partial_Sums(s1).n + s1.(n+1) + Partial_Sums(s2).(n+1) by BHSP_4:def 1 .= Partial_Sums(s1).n+s1.(n+1)+(s2.(n+1) + Partial_Sums(s2).n) by BHSP_4:def 1 .= Partial_Sums(s1).n+s1.(n+1)+s2.(n+1)+Partial_Sums(s2).n by RLVECT_1:def 3 .= Partial_Sums(s1).n+(s1.(n+1)+s2.(n+1)) + Partial_Sums(s2).n by RLVECT_1:def 3 .= Partial_Sums(s1).n+(s1+s2).(n+1)+Partial_Sums(s2).n by NORMSP_1:def 2 .= Partial_Sums(s1).n+Partial_Sums(s2).n+(s1+s2).(n+1) by RLVECT_1:def 3 .= (Partial_Sums(s1)+Partial_Sums(s2)).n+(s1+s2).(n+1) by NORMSP_1:def 2; end; (Partial_Sums(s1) + Partial_Sums(s2)).0 = Partial_Sums(s1).0 + Partial_Sums(s2).0 by NORMSP_1:def 2 .= s1.0 + Partial_Sums(s2).0 by BHSP_4:def 1 .= s1.0 + s2.0 by BHSP_4:def 1 .= (s1+s2).0 by NORMSP_1:def 2; hence thesis by A1,BHSP_4:def 1; end; theorem Th16: for X be ComplexNormSpace, s1,s2 be sequence of X holds Partial_Sums(s1)-Partial_Sums(s2) = Partial_Sums(s1-s2) proof let X be ComplexNormSpace; let s1,s2 be sequence of X; A1: now let n be Nat; thus (Partial_Sums(s1) - Partial_Sums(s2)).(n+1) = Partial_Sums(s1).(n+1) - Partial_Sums(s2).(n+1) by NORMSP_1:def 3 .= (Partial_Sums(s1).n + s1.(n+1)) - Partial_Sums(s2).(n+1) by BHSP_4:def 1 .= (Partial_Sums(s1).n+s1.(n+1))-(s2.(n+1) + Partial_Sums(s2).n) by BHSP_4:def 1 .= (Partial_Sums(s1).n+s1.(n+1))-s2.(n+1)-Partial_Sums(s2).n by RLVECT_1:27 .= Partial_Sums(s1).n+(s1.(n+1)-s2.(n+1))-Partial_Sums(s2).n by RLVECT_1:def 3 .= (s1-s2).(n+1)+Partial_Sums(s1).n-Partial_Sums(s2).n by NORMSP_1:def 3 .= (s1-s2).(n+1)+(Partial_Sums(s1).n-Partial_Sums(s2).n) by RLVECT_1:def 3 .= (Partial_Sums(s1)-Partial_Sums(s2)).n+(s1-s2).(n+1) by NORMSP_1:def 3; end; (Partial_Sums(s1) - Partial_Sums(s2)).0 = Partial_Sums(s1).0 - Partial_Sums(s2).0 by NORMSP_1:def 3 .= s1.0 - Partial_Sums(s2).0 by BHSP_4:def 1 .= s1.0 - s2.0 by BHSP_4:def 1 .= (s1-s2).0 by NORMSP_1:def 3; hence thesis by A1,BHSP_4:def 1; end; registration let X be ComplexNormSpace; let seq be norm_summable sequence of X; cluster ||.seq.|| -> summable for Real_Sequence; coherence by Def3; end; registration let X be ComplexNormSpace; cluster summable -> convergent for sequence of X; coherence by Th14; end; theorem Th17: for X be ComplexNormSpace, 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) proof let X be ComplexNormSpace; let seq1,seq2 be sequence of X; assume seq1 is summable & seq2 is summable; then A1: Partial_Sums(seq1) is convergent & Partial_Sums(seq2) is convergent; then A2: Partial_Sums(seq1)+Partial_Sums(seq2) is convergent by CLVECT_1:113; A3: Partial_Sums(seq1)+Partial_Sums(seq2) =Partial_Sums(seq1+seq2) by Th15; Sum(seq1+seq2)=lim(Partial_Sums(seq1)+Partial_Sums(seq2)) by Th15 .=lim(Partial_Sums(seq1))+lim(Partial_Sums(seq2)) by A1,CLVECT_1:119; hence thesis by A2,A3; end; theorem Th18: for X be ComplexNormSpace, 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) proof let X be ComplexNormSpace; let seq1,seq2 be sequence of X; assume seq1 is summable & seq2 is summable; then A1: Partial_Sums(seq1) is convergent & Partial_Sums(seq2) is convergent; then A2: Partial_Sums(seq1)-Partial_Sums(seq2) is convergent by CLVECT_1:114; A3: Partial_Sums(seq1)-Partial_Sums(seq2) = Partial_Sums(seq1-seq2) by Th16; Sum(seq1-seq2)=lim(Partial_Sums(seq1)-Partial_Sums(seq2)) by Th16 .=lim(Partial_Sums(seq1))-lim(Partial_Sums(seq2)) by A1,CLVECT_1:120; hence thesis by A2,A3; end; registration let X be ComplexNormSpace; let seq1,seq2 be summable sequence of X; cluster seq1 + seq2 -> summable; coherence by Th17; cluster seq1 - seq2 -> summable; coherence by Th18; end; theorem Th19: for X be ComplexNormSpace, seq be sequence of X, z be Complex holds Partial_Sums(z * seq) = z * Partial_Sums(seq) proof let X be ComplexNormSpace; let seq be sequence of X; let z be Complex; defpred P[Nat] means Partial_Sums(z * seq).$1 = (z * Partial_Sums(seq)).$1; A1: now let n be Nat; assume A2: P[n]; Partial_Sums(z * seq).(n+1) =Partial_Sums(z * seq).n + (z * seq).(n+1) by BHSP_4:def 1 .=(z * Partial_Sums(seq).n )+ (z * seq).(n+1) by A2,CLVECT_1:def 14 .=(z * Partial_Sums(seq).n )+ (z * seq.(n+1)) by CLVECT_1:def 14 .= z * ( Partial_Sums(seq).n + seq.(n+1)) by CLVECT_1:def 2 .= z * ( Partial_Sums(seq).(n+1)) by BHSP_4:def 1 .= (z * Partial_Sums(seq)).(n+1) by CLVECT_1:def 14; hence P[n+1]; end; Partial_Sums(z * seq).0 = (z * seq).0 by BHSP_4:def 1 .=z * seq.0 by CLVECT_1:def 14 .=z * Partial_Sums(seq).0 by BHSP_4:def 1 .=(z * Partial_Sums(seq)).0 by CLVECT_1:def 14; then A3: P[0]; for n be Nat holds P[n] from NAT_1:sch 2(A3,A1); then for n be Element of NAT holds P[n]; hence thesis by FUNCT_2:63; end; theorem Th20: for X be ComplexNormSpace, seq be summable sequence of X, z be Complex holds z *seq is summable & Sum(z *seq)= z * Sum(seq) proof let X be ComplexNormSpace; let seq be summable sequence of X; let z be Complex; A1: Partial_Sums(z *seq)=(z *Partial_Sums(seq)) by Th19; A2: Partial_Sums(seq) is convergent by Def1; then A3: (z *Partial_Sums(seq)) is convergent by CLVECT_1:116; Sum(z *seq)=lim((z *Partial_Sums(seq))) by Th19 .=z * Sum(seq) by A2,CLVECT_1:122; hence thesis by A3,A1; end; registration let X be ComplexNormSpace; let z be Complex, seq be summable sequence of X; cluster z *seq -> summable; coherence by Th20; end; theorem Th21: for X be ComplexNormSpace, 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 proof let X be ComplexNormSpace; let s,s1 be sequence of X; assume A1: for n be Nat holds s1.n=s.0; A2: now let k be Nat; thus ((Partial_Sums(s)^\1) - s1).(k+1) = (Partial_Sums(s)^\1).(k+1) - s1.( k+1) by NORMSP_1:def 3 .= (Partial_Sums(s)^\1).(k+1) - s.0 by A1 .= Partial_Sums(s).(k+1+1) - s.0 by NAT_1:def 3 .= s.(k+1+1) + Partial_Sums(s).(k+1) - s.0 by BHSP_4:def 1 .= s.(k+1+1) + Partial_Sums(s).(k+1) - s1.k by A1 .= s.(k+1+1) + (Partial_Sums(s).(k+1) - s1.k) by RLVECT_1:def 3 .= s.(k+1+1) + ((Partial_Sums(s)^\1).k - s1.k) by NAT_1:def 3 .= s.(k+1+1) + ((Partial_Sums(s)^\1) - s1).k by NORMSP_1:def 3 .= ((Partial_Sums(s)^\1) - s1).k + (s^\1).(k+1) by NAT_1:def 3; end; ((Partial_Sums(s)^\1) - s1).0 = (Partial_Sums(s)^\1).0 - s1.0 by NORMSP_1:def 3 .= (Partial_Sums(s)^\1).0 - s.0 by A1 .= Partial_Sums(s).(0+1) - s.0 by NAT_1:def 3 .= Partial_Sums(s).0 + s.(0+1) - s.0 by BHSP_4:def 1 .= s.(0+1) + s.0 - s.0 by BHSP_4:def 1 .= s.(0+1) + (s.0 - s.0) by RLVECT_1:def 3 .= s.(0+1) + 0.X by RLVECT_1:15 .=s.(0+1) by RLVECT_1:4 .= (s^\1).0 by NAT_1:def 3; hence thesis by A2,BHSP_4:def 1; end; theorem Th22: for X be ComplexNormSpace, s be sequence of X holds s is summable implies for n be Nat holds s^\n is summable proof let X be ComplexNormSpace; let s be sequence of X; defpred X[Nat] means s^\$1 is summable; A1: for n be Nat st X[n] holds X[n+1] proof let n be Nat; reconsider s1 = NAT --> (s^\n).0 as sequence of X; for k be Nat holds s1.k = (s^\n).0 by ORDINAL1:def 12,FUNCOP_1:7; then A2: Partial_Sums(s^\n^\1) = (Partial_Sums(s^\n)^\1) - s1 by Th21; assume s^\n is summable; then Partial_Sums(s^\n) is convergent; then A3: Partial_Sums(s^\n)^\1 is convergent by Th7; s1 is convergent by Th12; then s^\(n+1)=(s^\n)^\1 & Partial_Sums(s^\n^\1) is convergent by A3,A2, CLVECT_1:114,NAT_1:48; hence thesis by Def1; end; assume s is summable; then A4: X[0] by NAT_1:47; thus for n be Nat holds X[n] from NAT_1:sch 2(A4,A1); end; registration let X be ComplexNormSpace; let seq be summable sequence of X, n be Nat; cluster seq^\n -> summable for sequence of X; coherence by Th22; end; theorem Th23: for X be ComplexNormSpace, seq be sequence of X holds Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable proof let X be ComplexNormSpace; let seq be sequence of X; for n be Nat holds 0 <=||.seq.||.n by Th2; then Partial_Sums(||.seq.||) is bounded_above iff ||.seq.|| is summable by SERIES_1:17; hence thesis; end; registration let X be ComplexNormSpace; let seq be norm_summable sequence of X; cluster Partial_Sums ||.seq.|| -> bounded_above for Real_Sequence; coherence by Th23; end; theorem Th24: for X be ComplexBanachSpace, seq be sequence of X holds seq is summable iff for p be Real st 0
=0 by CLVECT_1:105; hence ||.s.||.k >= 0 by NORMSP_0:def 4; end; then A2: s2 is non-decreasing by SERIES_1:16; A3: for k be Nat st X[k] holds X[k+1] proof let k be Nat; A4: |.s2.(n+(k+1)) - s2.n.| = |.s2.(n+k) + ( ||.s.||).(n+k+1) - s2.n.| by SERIES_1:def 1 .= |.s2.(n+k) + ||.s.(n+k+1).||-s2.n.| by NORMSP_0:def 4 .= |.||.s.(n+k+1).|| + (s2.(n+k) - s2.n).|; ||. s1.(n+(k+1)) - s1.n.|| = ||. s.(n+k+1) + s1.(n+k) - s1.n .|| by BHSP_4:def 1 .= ||. s.(n+k+1) + (s1.(n+k) - s1.n).|| by RLVECT_1:def 3; then A5: ||. s1.(n+(k+1))-s1.n .|| <= ||.s.(n+k+1).||+||.s1.(n+k) - s1.n.|| by CLVECT_1:def 13; s2.(n+k)>=s2.n by A2,SEQM_3:5; then A6: s2.(n+k) - s2.n >= 0 by XREAL_1:48; assume ||. s1.(n+k) - s1.n.|| <= |.s2.(n+k) - s2.n.|; then ||.s.(n+k+1).|| + ||. s1.(n+k) - s1.n.|| <= ||.s.(n+k+1).|| + |.s2. (n+k) - s2.n.| by XREAL_1:7; then ||. s1.(n+(k+1))-s1.n.|| <= ||. s.(n+k+1).||+ |.s2.(n+k)-s2.n.| by A5 ,XXREAL_0:2; then A7: ||. s1.(n+(k+1))-s1.n .|| <= ||. s.(n+k+1).||+(s2.(n+k)-s2.n) by A6, ABSVALUE:def 1; ||. s .(n+k+1) .|| >= 0 by CLVECT_1:105; hence thesis by A6,A7,A4,ABSVALUE:def 1; end; ||.s1.(n+0) - s1.n.|| = ||.0.X.|| by RLVECT_1:15 .= 0; then A8: X[0] by COMPLEX1:46; for k be Nat holds X[k] from NAT_1:sch 2(A8,A3); hence thesis by A1; end; theorem Th26: for X be ComplexBanachSpace, seq be sequence of X holds seq is norm_summable implies seq is summable proof let X be ComplexBanachSpace; let seq be sequence of X; assume seq is norm_summable; then A1: Partial_Sums(||.seq.||) is convergent by SERIES_1:def 2; now let p be Real; assume 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 by SERIES_1:27;
theorem
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
proof
let X be ComplexNormSpace;
let seq be sequence of X;
let rseq1 be Real_Sequence;
assume
A1: ( for n be Nat holds rseq1.n = n-root (||.seq.||.n))&
rseq1 is convergent & lim rseq1 < 1;
for n be Nat holds ||.seq.||.n >=0 by Th2;
hence ||.seq.|| is summable by A1,SERIES_1:28;
end;
theorem
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
proof
let X be ComplexNormSpace;
let seq be sequence of X;
let rseq1 be Real_Sequence;
assume
A1: ( 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;
for n be Nat holds ||.seq.||.n >=0 by Th2;
hence thesis by A1,SERIES_1:29;
end;
theorem
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
proof
let X be ComplexNormSpace;
let seq be sequence of X;
let rseq1 be Real_Sequence;
assume
A1: ( for n be Nat holds rseq1.n = n-root (||.seq.||.n))&
rseq1 is convergent & lim rseq1 > 1;
for n be Nat holds ||.seq.||.n >=0 by Th2;
hence ||.seq.|| is not summable by A1,SERIES_1:30;
end;
theorem
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)
proof
let X be ComplexNormSpace;
let seq be sequence of X;
let rseq1 be Real_Sequence;
assume ||.seq.|| is non-increasing & for n be Nat holds rseq1.n
= 2 to_power n *||.seq.||.(2 to_power n);
then
for n be Nat holds ||.seq.|| is non-increasing & ||.seq.||.n
>= 0 & rseq1.n = 2 to_power n *||.seq.||.(2 to_power n) by Th2;
then ||.seq.|| is summable iff rseq1 is summable by SERIES_1:31;
hence thesis;
end;
theorem
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
by SERIES_1:32;
theorem
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 by SERIES_1:33;
theorem
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
proof
let X be ComplexNormSpace;
let seq be sequence of X;
let rseq1 be Real_Sequence;
assume that
A1: for n be Nat holds seq.n<>0.X & rseq1.n=||.seq.||.(n+1)/
||. seq.||.n and
A2: rseq1 is convergent & lim rseq1 < 1;
now
let n be Nat;
A3: 0 <=||.seq.||.n by Th2;
A4: 0 <=||.seq.||.(n+1) by Th2;
A5: abs((||.seq.||)).(n+1) =|.(||.seq.||).(n+1).| by SEQ_1:12
.=||.seq.||.(n+1) by A4,ABSVALUE:def 1;
A6: seq.n<>0.X & ||.seq.||.n =||.seq.n.|| by A1,NORMSP_0:def 4;
abs((||.seq.||)).n =|.(||.seq.||).n.| by SEQ_1:12
.=||.seq.||.n by A3,ABSVALUE:def 1;
hence (||.seq.||).n <>0 & rseq1.n=abs((||.seq.||)).(n+1)/abs((||.seq.||)).
n by A1,A5,A6,NORMSP_0:def 5;
end;
then ||.seq.|| is absolutely_summable by A2,SERIES_1:37;
then
A7: abs(||.seq.||) is summable;
now
let n be Element of NAT;
A8: 0 <=||.seq.||.n by Th2;
thus abs((||.seq.||)).n =|.(||.seq.||).n.| by SEQ_1:12
.=||.seq.||.n by A8,ABSVALUE:def 1;
end;
then abs((||.seq.||)) =||.seq.|| by FUNCT_2:63;
hence thesis by A7;
end;
theorem
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
proof
let X be ComplexNormSpace;
let seq be sequence of X;
assume that
A1: for n be Nat holds seq.n <> 0.X and
A2: ex m be Nat st for n be Nat st n >=m holds ||.
seq.||.(n+1)/||.seq.||.n >= 1;
consider m be Nat such that
A3: for n be Nat st n >=m holds ||.seq.||.(n+1)/||.seq.||.n
>= 1 by A2;
A4: now
let n be Nat such that
A5: n>=m;
A6: 0 <=||.seq.||.n by Th2;
A7: 0 <=||.seq.||.(n+1) by Th2;
A8: abs((||.seq.||)).(n+1) =|.(||.seq.||).(n+1).| by SEQ_1:12
.=||.seq.||.(n+1) by A7,ABSVALUE:def 1;
abs((||.seq.||)).n =|.(||.seq.||).n.| by SEQ_1:12
.=||.seq.||.n by A6,ABSVALUE:def 1;
hence abs((||.seq.||)).(n+1)/abs((||.seq.||)).n >= 1 by A3,A5,A8;
end;
now
let n be Nat;
seq.n <> 0.X by A1;
then ||.seq.n.||<>0 by NORMSP_0:def 5;
hence ||.seq.||.n <>0 by NORMSP_0:def 4;
end;
hence ||.seq.|| is not summable by A4,SERIES_1:39;
end;
registration
let X be ComplexBanachSpace;
cluster norm_summable -> summable for sequence of X;
coherence by Th26;
end;
begin :: Basic Properties of Sequence of Complex_Banach_Algebra
theorem Th38:
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
proof
let X be Complex_Banach_Algebra;
let x,y,z being Element of X;
let a,b be Complex;
thus
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) by CFUNCDOM:def 9,CLVECT_1:def 2,def 3,def 4;
thus (a*b)*(x*y) =a*(b*(x*y)) by CLVECT_1:def 4
.=a*(x*(b*y) ) by CLOPBAN2:def 11
.=(a*x)*(b*y) by CFUNCDOM:def 9;
thus a*(x*y)=x*(a*y) by CLOPBAN2:def 11;
A1: x*(y-z)+x*z =x*((y-z)+z) by VECTSP_1:def 2
.=x*(y-(z-z)) by RLVECT_1:29
.=x*(y-0.X) by RLVECT_1:15
.=x*y by RLVECT_1:13;
x*0.X =x*(0.X+0.X) by RLVECT_1:def 4
.=x*0.X + x*0.X by VECTSP_1:def 2;
then 0.X = x*0.X + x*0.X-x* 0.X by RLVECT_1:15;
then 0.X = x*0.X + (x*0.X-x* 0.X) by RLVECT_1:def 3;
then
A2: 0.X = x*0.X + 0.X by RLVECT_1:15;
0.X*x =(0.X+0.X)*x by RLVECT_1:def 4
.=0.X*x + 0.X*x by VECTSP_1:def 3;
then 0.X = 0.X*x + 0.X*x-0.X * x by RLVECT_1:15;
then 0.X = 0.X*x + (0.X*x-0.X * x) by RLVECT_1:def 3;
then 0.X = 0.X*x + 0.X by RLVECT_1:15;
hence 0.X * x = 0.X & x*0.X =0.X by A2,RLVECT_1:def 4;
thus x*(y-z) =x*(y-z)+0.X by RLVECT_1:4
.=x*(y-z)+(x*z-x*z) by RLVECT_1:15
.=x*y-x*z by A1,RLVECT_1:def 3;
A3: (y-z)*x+z*x =((y-z)+z)*x by VECTSP_1:def 3
.=(y-(z-z))*x by RLVECT_1:29
.=(y-0.X)*x by RLVECT_1:15
.=y*x by RLVECT_1:13;
thus (y-z)*x =(y-z)*x+0.X by RLVECT_1:4
.=(y-z)*x+(z*x-z*x) by RLVECT_1:15
.=y*x-z*x by A3,RLVECT_1:def 3;
thus x+y-z = x+(y-z) by RLVECT_1:def 3;
thus x-y+z = x-(y-z) by RLVECT_1:29;
thus x-y-z = x-(y+z) by RLVECT_1:27;
thus (x-z)+(z+y)=(x-z)+z+y by RLVECT_1:def 3
.=x-(z-z)+y by RLVECT_1:29
.=x-0.X + y by RLVECT_1:15
.=x+y by RLVECT_1:13;
thus (x-z)+(z-y) =x-z+z-y by RLVECT_1:def 3
.=x-(z-z)-y by RLVECT_1:29
.=x-0.X -y by RLVECT_1:15
.=x-y by RLVECT_1:13;
thus (x-y)+y=x-(y-y) by RLVECT_1:29
.=x-0.X by RLVECT_1:15
.=x by RLVECT_1:13;
thus y-(y-x)=y-y + x by RLVECT_1:29
.=0.X + x by RLVECT_1:15
.=x by RLVECT_1:4;
thus ( ||.x.|| = 0 iff x = 0.X ) & ||.a * x.|| = |.a.| * ||.x.|| & ||.x + y
.|| <= ||.x.|| + ||.y.|| & ||. x*y .|| <= ||.x.|| * ||.y.|| by CLOPBAN2:def 9
,CLVECT_1:def 13,NORMSP_0:def 5;
thus ||. 1.X .|| = 1 by CLOPBAN2:def 10;
end;
registration
cluster -> well-unital for Complex_Banach_Algebra;
coherence
proof
let X be Complex_Banach_Algebra;
let x be Element of X;
thus thesis by VECTSP_1:def 4,def 8;
end;
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
:Def4:
it.0 = 1.X & for n be Nat holds it.(n+1) = it.n * z;
existence
proof
deffunc G(set,set)=(the multF of X).[$2,z];
consider g be Function such that
A1: dom g = NAT & g.0 = 1.X & for n being Nat holds g.(n+1) = G(n,g.n)
from NAT_1:sch 11;
defpred P[Nat] means g.$1 in the carrier of X;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then reconsider gk=g.k as Element of X;
g.(k+1)=(the multF of X).[gk,z] by A1;
hence thesis;
end;
A3: P[0] by A1;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A2);
then for n be object st n in NAT holds g.n in the carrier of X;
then reconsider g0=g as sequence of X by A1,FUNCT_2:3;
take g0;
thus thesis by A1;
end;
uniqueness
proof
let seq1,seq2 be sequence of X;
assume that
A4: seq1.0=1.X and
A5: for n be Nat holds seq1.(n+1)=seq1.n * z and
A6: seq2.0=1.X and
A7: for n be Nat holds seq2.(n+1)=seq2.n * z;
defpred P[Nat] means seq1.$1 = seq2.$1;
A8: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
hence seq1.(k+1) = seq2.k * z by A5
.= seq2.(k+1) by A7;
end;
A9: P[0] by A4,A6;
for n be Nat holds P[n] from NAT_1:sch 2(A9,A8);
then for n be Element of NAT holds P[n];
hence seq1 = seq2 by FUNCT_2:63;
end;
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
z GeoSeq.n;
correctness;
end;
theorem
for X be Complex_Banach_Algebra, z be Element of X holds z #N 0 = 1.X
by Def4;
theorem Th40:
for X be Complex_Banach_Algebra, z be Element of X holds
||.z.|| < 1 implies z GeoSeq is summable norm_summable
proof
let X be Complex_Banach_Algebra;
let z be Element of X;
A1: 0<= ||.z.|| by CLVECT_1:105;
A2: for n be Nat holds 0 <= ||.z GeoSeq.||.n & ||.z GeoSeq.||.n
<=(||.z.|| GeoSeq).n
proof
defpred P[Nat] means
0 <= ||.z GeoSeq.||.$1 & ||.z GeoSeq.||.$1
<= ( ||.z.|| GeoSeq ).$1;
A3: ||.(z GeoSeq).||.0 = ||.(z GeoSeq).0 .|| by NORMSP_0:def 4;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
A5: 0 <= ||.z.|| by CLVECT_1:105;
||.(z GeoSeq.k)*z.|| <= ||.(z GeoSeq.k).||*||.z.|| by CLOPBAN2:def 9;
then
A6: ||. (z GeoSeq.k)*z .|| <= ||. z GeoSeq .||.k * ||.z.|| by NORMSP_0:def 4;
assume P[k];
then ||. z GeoSeq.||.k * ||.z.|| <= (||.z.|| GeoSeq ).k * ||.z.|| by A5,
XREAL_1:64;
then
A7: ||.
(z GeoSeq.k)*z .|| <= ( ||.z.|| GeoSeq ).k * ||.z.|| by A6,XXREAL_0:2;
||.z GeoSeq.||.(k+1) = ||. (z GeoSeq).(k+1) .|| by NORMSP_0:def 4
.= ||. (z GeoSeq).k * z .|| by Def4;
hence thesis by A7,CLVECT_1:105,PREPOWER:3;
end;
||.(z GeoSeq).0 .|| = ||.1.X.|| by Def4
.= 1 by CLOPBAN2:def 10
.= ( ||.z.|| GeoSeq ).0 by PREPOWER:3;
then
A8: P[0] by A3,CLVECT_1:105;
for n be Nat holds P[n] from NAT_1:sch 2(A8,A4);
hence thesis;
end;
assume ||.z.|| < 1;
then |. ||.z.||.| < 1 by A1,ABSVALUE:def 1;
then ||.z.|| GeoSeq is summable by SERIES_1:24;
then ||.z GeoSeq.|| is summable by A2,SERIES_1:20;
then z GeoSeq is norm_summable;
hence thesis;
end;
theorem
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 by Th40;
Lm1: for X be ComplexNormSpace, x be Point of X
st for e be Real st e>0 holds||.x.||