:: 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; definitions SEQ_2, SERIES_1, NORMSP_1, ALGSTR_0, VECTSP_1; equalities BINOP_1, ALGSTR_0; expansions SERIES_1, NORMSP_1, ALGSTR_0; theorems ABSVALUE, RLVECT_1, VECTSP_1, FUNCSDOM, SEQ_1, SEQ_2, SEQM_3, SERIES_1, NAT_1, INT_1, FUNCT_2, NORMSP_1, SEQ_4, RSSPACE3, LOPBAN_1, PREPOWER, LOPBAN_2, GROUP_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, BHSP_4, VALUED_0, ALGSTR_0, NORMSP_0; schemes NAT_1, FUNCT_2; begin theorem Th1: 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 proof let X be add-associative right_zeroed right_complementable non empty NORMSTR; 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 RealNormSpace; let seq be sequence of X; attr seq is summable means :Def1: Partial_Sums seq is convergent; end; registration let X be RealNormSpace; cluster summable for sequence of X; existence proof reconsider C = NAT --> 0.X as sequence of X; take C, 0.X; let p be Real such that A1: 0
Element of X equals
lim Partial_Sums seq;
correctness;
end;
definition
let X be RealNormSpace;
let seq be sequence of X;
attr seq is norm_summable means
:Def3:
||.seq.|| is summable;
end;
theorem Th2:
for X be RealNormSpace for seq be sequence of X
for m be Nat holds 0 <= ||.seq.||.m
proof
let X be RealNormSpace;
let seq be sequence of X;
let m be Nat;
||.seq.||.m = ||.seq.m.|| by NORMSP_0:def 4;
hence thesis;
end;
theorem Th3:
for X be RealNormSpace for x,y,z be Element of X holds ||.x-y.||
= ||.(x-z)+(z-y).||
proof
let X be RealNormSpace;
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 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
proof
let X be RealNormSpace;
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;
reconsider ss=s as 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,RSSPACE3: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 RealNormSpace for s be sequence of X holds s is summable implies s is convergent & lim s = 0.X proof let X be RealNormSpace; 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,NORMSP_1:26 .= 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,NORMSP_1:20; hence thesis by A3,A4,Th10,Th11; end; theorem Th15: for X be RealNormSpace for s1,s2 be sequence of X holds Partial_Sums(s1)+Partial_Sums(s2) = Partial_Sums(s1+s2) proof let X be RealNormSpace; 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 RealNormSpace for s1,s2 be sequence of X holds Partial_Sums(s1)-Partial_Sums(s2) = Partial_Sums(s1-s2) proof let X be RealNormSpace; 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 RealNormSpace; let seq be norm_summable sequence of X; cluster ||.seq.|| -> summable for Real_Sequence; coherence by Def3; end; registration let X be RealNormSpace; cluster summable -> convergent for sequence of X; coherence by Th14; end; theorem Th17: 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) proof let X be RealNormSpace; 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 NORMSP_1:19; 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,NORMSP_1:25; hence thesis by A2,A3; end; theorem Th18: 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) proof let X be RealNormSpace; 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 NORMSP_1:20; 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,NORMSP_1:26; hence thesis by A2,A3; end; registration let X be RealNormSpace; 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 RealNormSpace for seq be sequence of X for z be Real holds Partial_Sums(z * seq) = z * Partial_Sums(seq) proof let X be RealNormSpace; let seq be sequence of X; let z be Real; 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,NORMSP_1:def 5 .=(z * Partial_Sums(seq).n )+ (z * seq.(n+1)) by NORMSP_1:def 5 .= z * ( Partial_Sums(seq).n + seq.(n+1)) by RLVECT_1:def 5 .= z * ( Partial_Sums(seq).(n+1)) by BHSP_4:def 1 .= (z * Partial_Sums(seq)).(n+1) by NORMSP_1:def 5; hence P[n+1]; end; Partial_Sums(z * seq).0 = (z * seq).0 by BHSP_4:def 1 .=z * seq.0 by NORMSP_1:def 5 .=z * Partial_Sums(seq).0 by BHSP_4:def 1 .=(z * Partial_Sums(seq)).0 by NORMSP_1:def 5; 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 RealNormSpace for seq be summable sequence of X for z be Real holds z *seq is summable & Sum(z *seq)= z * Sum(seq) proof let X be RealNormSpace; let seq be summable sequence of X; let z be Real; 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 NORMSP_1:22; Sum(z *seq)=lim((z *Partial_Sums(seq))) by Th19 .=z * Sum(seq) by A2,NORMSP_1:28; hence thesis by A3,A1; end; registration let X be RealNormSpace; let z be Real, seq be summable sequence of X; cluster z *seq -> summable; coherence by Th20; end; theorem Th21: 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 proof let X be RealNormSpace; 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 RealNormSpace for s be sequence of X holds s is summable implies for n be Nat holds s^\n is summable proof let X be RealNormSpace; 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, NAT_1:48,NORMSP_1:20; 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 RealNormSpace; 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 RealNormSpace for seq be sequence of X holds Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable proof let X be RealNormSpace; 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 RealNormSpace; 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 RealBanachSpace for seq be sequence of X holds seq is summable iff for p be Real st 0
=0; 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 NORMSP_1:def 1; 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 ||. s1.(n+(k+1))-s1.n .|| <= ||. s.(n+k+1).||+(s2.(n+k)-s2.n) by A6, ABSVALUE:def 1; hence thesis by A4,ABSVALUE:def 1; end; ||.s1.(n+0) - s1.n.|| = ||.0.X.|| by RLVECT_1:15 .= 0; then A7: X[0] by COMPLEX1:46; for k be Nat holds X[k] from NAT_1:sch 2(A7,A3); hence thesis by A1; end; theorem Th26: for X be RealBanachSpace for seq be sequence of X holds seq is norm_summable implies seq is summable proof let X be RealBanachSpace; 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 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
proof
let X be RealNormSpace;
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 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
proof
let X be RealNormSpace;
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 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
proof
let X be RealNormSpace;
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 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)
proof
let X be RealNormSpace;
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 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
by SERIES_1:32;
theorem
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 by SERIES_1:33;
theorem
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
proof
let X be RealNormSpace;
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 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
proof
let X be RealNormSpace;
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 RealBanachSpace;
cluster norm_summable -> summable for sequence of X;
coherence by Th26;
end;
begin :: Basic Properties of Sequence of Banach_Algebra
theorem Th38:
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
proof
let X be Banach_Algebra;
let x,y,z being Element of X;
let a,b be Real;
thus x+y = y+x;
thus (x+y)+z = x+(y+z) by RLVECT_1:def 3;
thus x+(0.X) = x by RLVECT_1:def 4;
thus ex t being Element of X st x+t=0.X by ALGSTR_0:def 11;
thus (x*y)*z = x*(y*z) by GROUP_1:def 3;
thus 1*x = x by RLVECT_1:def 8;
thus 0*x = 0.X by RLVECT_1:10;
thus a*0.X =0.X by RLVECT_1:10;
thus (-1)*x = -x by RLVECT_1:16;
thus 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) by FUNCSDOM:def 9,RLVECT_1:def 5,def 6,def 7,VECTSP_1:def 2,def 3,def 4
,def 8;
thus (a*b)*(x*y) =a*(b*(x*y)) by RLVECT_1:def 7
.=a*(x*(b*y) ) by LOPBAN_2:def 11
.=(a*x)*(b*y) by FUNCSDOM:def 9;
thus a*(x*y)=x*(a*y) by LOPBAN_2: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 LOPBAN_2:def 9
,NORMSP_0:def 5,NORMSP_1:def 1;
thus thesis by LOPBAN_2:def 10;
end;
registration
cluster -> well-unital for Banach_Algebra;
coherence
proof
let X be Banach_Algebra;
let x be Element of X;
thus thesis by Th38;
end;
end;
definition
let X be well-unital associative non empty multLoopStr;
let v be Element of X;
redefine attr v is invertible means
ex w be Element of X st v*w = 1.X & w*v=1.X;
compatibility
proof
thus v is invertible implies ex w be Element of X st v*w = 1.X & w*v=1.X
proof
assume
A1: v is invertible;
then consider y being Element of X such that
A2: v*y = 1.X by ALGSTR_0:def 28;
take y;
thus v * y = 1.X by A2;
consider x being Element of X such that
A3: x*v = 1.X by A1,ALGSTR_0:def 27;
x = x * 1.X by VECTSP_1:def 6
.= 1.X * y by A2,A3,GROUP_1:def 3
.= y by VECTSP_1:def 6;
hence thesis by A3;
end;
given w being Element of X such that
A4: v*w = 1.X & w*v=1.X;
thus v is right_invertible left_invertible by A4;
end;
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
for n being Nat holds it.n = a * S .n;
existence
proof
deffunc F(Nat) = a * S.$1;
consider S being sequence of X such that
A1: for n be Element of NAT holds S.n = F(n) from FUNCT_2:sch 4;
take S;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S1, S2 be sequence of X;
assume that
A2: for n be Nat holds S1.n = a * S.n and
A3: for n be Nat holds S2.n = a * S.n;
for n be Element of NAT holds S1.n = S2.n
proof
let n be Element of NAT;
S1.n = a * S.n by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
func S*a -> sequence of X means
for n being Nat holds it.n = S.n*a;
existence
proof
deffunc F(Nat) = S.$1 *a;
consider S being sequence of X such that
A4: for n be Element of NAT holds S.n = F(n) from FUNCT_2:sch 4;
take S;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A4;
end;
uniqueness
proof
let S1, S2 be sequence of X;
assume that
A5: for n be Nat holds S1.n = S.n *a and
A6: for n be Nat holds S2.n = S.n *a;
for n be Element of NAT holds S1.n = S2.n
proof
let n be Element of NAT;
S1.n = S.n *a by A5;
hence thesis by A6;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let X be non empty multMagma;
let seq1,seq2 be sequence of X;
func seq1 * seq2 -> sequence of X means
for n being Nat holds it.n = seq1.n * seq2.n;
existence
proof
deffunc F(Nat) = seq1.$1 * seq2.$1;
consider S being sequence of X such that
A1: for n be Element of NAT holds S.n = F(n) from FUNCT_2:sch 4;
take S;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S1, S2 be sequence of X;
assume that
A2: for n be Nat holds S1.n = seq1.n * seq2.n and
A3: for n be Nat holds S2.n = seq1.n * seq2.n;
for n be Element of NAT holds S1.n = S2.n
proof
let n be Element of NAT;
S1.n = seq1.n * seq2.n by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
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
A1: x is invertible;
redefine func x" means
:Def8:
x*it= 1.X & it*x= 1.X;
compatibility
proof
let y be Element of X;
consider x1 being Element of X such that
A2: x*x1 = 1.X by A1;
A3: x is right_mult-cancelable
proof
let y,z be Element of X;
assume
A4: y*x = z*x;
thus y = y*1.X by VECTSP_1:def 6
.= z*x*x1 by A2,A4,GROUP_1:def 3
.= z*1.X by A2,GROUP_1:def 3
.= z by VECTSP_1:def 6;
end;
thus y = x" implies x*y= 1.X & y*x= 1.X
by A1,A3,ALGSTR_0:def 30;
thus thesis by A1,A3,ALGSTR_0:def 30;
end;
end;
definition
let X be Banach_Algebra;
let z be Element of X;
func z GeoSeq -> sequence of X means
:Def9:
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 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 Banach_Algebra for z be Element of X holds z #N 0 = 1.X by Def9;
theorem Th40:
for X be Banach_Algebra for z be Element of X holds ||.z.|| < 1
implies z GeoSeq is summable norm_summable
proof
let X be Banach_Algebra;
let z be Element of X;
A1: 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;
A2: ||.(z GeoSeq).||.0 = ||.(z GeoSeq).0 .|| by NORMSP_0:def 4;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
||. (z GeoSeq.k)*z .|| <= ||. (z GeoSeq.k) .|| * ||.z.|| by
LOPBAN_2:def 9;
then
A4: ||. (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
XREAL_1:64;
then
A5: ||.
(z GeoSeq.k)*z .|| <= ( ||.z.|| GeoSeq ).k * ||.z.|| by A4,XXREAL_0:2;
||.z GeoSeq.||.(k+1) = ||. (z GeoSeq).(k+1) .|| by NORMSP_0:def 4
.= ||. (z GeoSeq).k * z .|| by Def9;
hence thesis by A5,PREPOWER:3;
end;
||.(z GeoSeq).0 .|| = ||.1.X.|| by Def9
.= 1 by LOPBAN_2:def 10
.= ( ||.z.|| GeoSeq ).0 by PREPOWER:3;
then
A6: P[0] by A2;
for n be Nat holds P[n] from NAT_1:sch 2(A6,A3);
hence thesis;
end;
assume ||.z.|| < 1;
then |. ||.z.||.| < 1 by ABSVALUE:def 1;
then ||.z.|| GeoSeq is summable by SERIES_1:24;
then ||.z GeoSeq.|| is summable by A1,SERIES_1:20;
then z GeoSeq is norm_summable;
hence thesis;
end;
theorem
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 by Th40;
Lm1: for X be RealNormSpace for x be Point of X
st for e be Real st e>0 holds ||.x.||