:: The Series on {B}anach Algebra
:: by Yasunari Shidama
::
:: Received February 3, 2004
:: Copyright (c) 2004-2026 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<p;
take 0;
let m be Nat such that
0<=m;
for n be Nat holds C.n = 0.X
by ORDINAL1:def 12,FUNCOP_1:7;
then ||.Partial_Sums C.m-0.X.|| = ||.0.X-0.X.|| by Th1
.=0 by NORMSP_1:6;
hence thesis by A1;
end;
end;
definition
let X be RealNormSpace;
let seq be sequence of X;
func Sum seq -> 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<s ex n be Nat st for m be
Nat st n<=m holds ||.seq.m -seq.n.||<s
proof
let X be RealNormSpace;
let seq be sequence of X;
assume seq is convergent;
then consider g1 be Element of X such that
A1: for s be Real st 0<s ex n be Nat st
for m be Nat st n<=m holds ||.seq.m -g1.||<s;
let s be Real;
assume 0<s;
then consider n be Nat such that
A2: for m be Nat st n<=m holds ||.seq.m -g1.||<s/2 by A1,XREAL_1:215;
now
let m be Nat;
assume n<=m;
then
A3: ||.seq.m -g1.||<s/2 by A2;
A4: ||.seq.m -g1+(g1-seq.n).||<=||.seq.m -g1.||+||.g1-seq.n.|| & ||.seq.m
-g1+( g1-seq.n).|| = ||.seq.m -seq.n.|| by Th3,NORMSP_1:def 1;
||.seq.n -g1.||<s/2 by A2;
then ||.g1-seq.n.||<s/2 by NORMSP_1:7;
then ||.seq.m -g1.||+||.g1-seq.n.||<s/2+s/2 by A3,XREAL_1:8;
hence ||.seq.m -seq.n.|| < s by A4,XXREAL_0:2;
end;
hence thesis;
end;
theorem Th5:
for X be RealNormSpace for seq be sequence of X holds seq is
Cauchy_sequence_by_Norm iff 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
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<s;
then consider k be Nat such that
A3: for m be Nat st k<=m holds ||.seq.m -seq.k.||<ss/2 by A2,
XREAL_1:215;
now
let m,n be Nat such that
A4: k<=m and
A5: k<=n;
||.seq.n -seq.k.||<s/2 by A3,A5;
then
A6: ||.seq.k-seq.n.||<s/2 by NORMSP_1:7;
||.seq.m -seq.k.||<s/2 by A3,A4;
then
A7: ||.seq.m -seq.k.||+||.seq.k-seq.n.||<s/2+s/2 by A6,XREAL_1:8;
||.seq.m -seq.k+(seq.k-seq.n).|| <=||.seq.m -seq.k.||+||.seq.k-
seq.n.|| & ||.seq.m -seq.k+(seq.k-seq.n).|| =||.seq.m -seq.n.|| by Th3,
NORMSP_1:def 1;
hence ||.seq.m -seq.n.|| < s by A7,XXREAL_0:2;
end;
hence ex k be Nat st for m,n be Nat st k <= m & k
<=n holds ||.seq.m-seq.n.||< s;
end;
hence seq is Cauchy_sequence_by_Norm by RSSPACE3:8;
end;
now
assume
A8: seq is Cauchy_sequence_by_Norm;
thus 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
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.||<p by A9;
hence thesis;
end;
end;
hence thesis by A1;
end;
theorem Th6:
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
proof
let X be RealNormSpace;
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)
.= ||.seq.k.|| + ||.seq.||.(k+1) by A1
.= (Partial_Sums ||.seq.||).k + ||.seq.||.(k+1) by A3,NORMSP_0:def 4
.= (Partial_Sums ||.seq.||).(k+1) by SERIES_1:def 1;
end;
A4: P[0] by SERIES_1:def 1;
for n be Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence (Partial_Sums ||.seq.||).m = ||.seq.||.m
.= ||.seq.m.|| by NORMSP_0:def 4
.= ||.0.X.|| by A1
.= 0;
end;
theorem Th7:
for X be RealNormSpace for seq,seq1 be sequence of X holds seq1
is subsequence of seq & seq is convergent implies seq1 is convergent
proof
let X be RealNormSpace;
let seq,seq1 be sequence of X;
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent;
consider g1 be Element of X such that
A3: for p be Real st 0<p ex n be Nat st
for m be Nat st n<=m holds ||.(seq.m)-g1.||< p by A2;
take g1;
let p be Real;
assume 0<p;
then consider n1 be Nat such that
A4: for m be Nat st n1<=m holds ||.(seq.m)-g1.||<p by A3;
take n=n1;
let m be Nat such that
A5: n<=m;
A6: m in NAT by ORDINAL1:def 12;
consider Nseq be increasing sequence of NAT such that
A7: seq1=seq*Nseq by A1,VALUED_0:def 17;
m<=Nseq.m by SEQM_3:14;
then
A8: n<=Nseq.m by A5,XXREAL_0:2;
seq1.m=seq.(Nseq.m) by A7,FUNCT_2:15,A6;
hence thesis by A4,A8;
end;
theorem Th8:
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
proof
let X be RealNormSpace;
let seq,seq1 be sequence of X;
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent;
consider Nseq be increasing sequence of NAT such that
A3: seq1=seq*Nseq by A1,VALUED_0:def 17;
A4: now
let p be Real;
assume 0<p;
then consider n1 be Nat such that
A5: for m be Nat st n1<=m holds ||.(seq.m)-(lim seq).||<p
by A2,NORMSP_1:def 7;
take n=n1;
let m be Nat such that
A6: n<=m;
A7: m in NAT by ORDINAL1:def 12;
m<=Nseq.m by SEQM_3:14;
then
A8: n<=Nseq.m by A6,XXREAL_0:2;
seq1.m=seq.(Nseq.m) by A3,FUNCT_2:15,A7;
hence ||.(seq1.m)-(lim seq).||<p by A5,A8;
end;
seq1 is convergent by A1,A2,Th7;
hence thesis by A4,NORMSP_1:def 7;
end;
:: Norm Space versions of SEQ_4_33 - SEQ_4_39
theorem
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 by Th7,Th8;
theorem Th10:
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
proof
let X be RealNormSpace;
let seq,seq1 be sequence of X;
assume that
A1: seq is convergent and
A2: ex k be Nat st seq=seq1 ^\k;
consider k be Nat such that
A3: seq=seq1 ^\k by A2;
consider g1 be Element of X such that
A4: for p be Real st 0<p ex n be Nat st
for m be Nat st n<=m holds ||.seq.m-g1.||<p by A1;
take g1;
let p be Real;
assume 0<p;
then consider n1 be Nat such that
A5: for m be Nat st n1<=m holds ||.seq.m-g1.||<p by A4;
take n=n1+k;
let m be Nat;
assume
A6: n<=m;
then consider l be Nat such that
A7: m=n1+k+l by NAT_1:10;
reconsider l as Nat;
m-k=n1+l+k+-k by A7;
then reconsider m1=m-k as Nat;
now
assume not n1<=m1;
then m1+k<n1+k by XREAL_1:6;
hence contradiction by A6;
end;
then m1+k=m & ||.seq.m1-g1.||<p by A5;
hence thesis by A3,NAT_1:def 3;
end;
theorem Th11:
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
proof
let X be RealNormSpace;
let seq,seq1 be sequence of X;
assume that
A1: seq is convergent and
A2: ex k be Nat st seq=seq1 ^\k;
consider k be Nat such that
A3: seq=seq1 ^\k by A2;
A4: now
let p be Real;
assume 0<p;
then consider n1 be Nat such that
A5: for m be Nat st n1<=m holds ||.seq.m-(lim seq).||<p by A1,
NORMSP_1:def 7;
take n=n1+k;
let m be Nat;
assume
A6: n<=m;
then consider l be Nat such that
A7: m=n1+k+l by NAT_1:10;
reconsider l as Nat;
m-k=n1+l+k+-k by A7;
then reconsider m1=m-k as Nat;
now
assume not n1<=m1;
then m1+k<n1+k by XREAL_1:6;
hence contradiction by A6;
end;
then m1+k=m & ||.seq.m1-(lim seq) .||<p by A5;
hence ||.seq1.m-(lim seq).||<p by A3,NAT_1:def 3;
end;
seq1 is convergent by A1,A2,Th10;
hence thesis by A4,NORMSP_1:def 7;
end;
theorem Th12:
for X be RealNormSpace for seq be sequence of X holds seq is
constant implies seq is convergent
proof
let X be RealNormSpace;
let seq be sequence of X;
assume seq is constant;
then consider r be Element of X such that
A1: for n be Nat holds seq.n=r by VALUED_0:def 18;
take g=r;
let p be Real such that
A2: 0<p;
take n=0;
let m be Nat such that
n<=m;
||.(seq.m)-g.||=||.r-g.|| by A1
.=||.0.X.|| by RLVECT_1:15
.=0;
hence thesis by A2;
end;
theorem Th13:
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
proof
let X be RealNormSpace;
let seq be sequence of X such that
A1: for n be Nat holds seq.n = 0.X;
take 0;
let p be Real such that
A2: 0<p;
take 0;
let m be Nat such that
0<=m;
|.(Partial_Sums ||.seq.||).m-0 .| = |.0-0 .| by A1,Th6
.= 0 by ABSVALUE:def 1;
hence thesis by A2;
end;
registration
let X be RealNormSpace;
cluster norm_summable for sequence of X;
existence
proof
reconsider C = NAT --> 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 <p holds ex n be Nat st for m be
Nat st n <= m holds ||.Partial_Sums(seq).m-Partial_Sums(seq).n.||<p
by Th5,LOPBAN_1:def 15,Th4;
theorem Th25:
for X be RealNormSpace for s be sequence of X
for n,m be Nat st n<=m
holds ||.Partial_Sums(s).m - Partial_Sums(s).n.|| <= |.
Partial_Sums(||.s.||).m - Partial_Sums(||.s.||).n.|
proof
let X be RealNormSpace;
let s be sequence of X;
set s1=Partial_Sums(s);
set s2=Partial_Sums(||.s.||);
let n,m be Nat;
assume n<=m;
then reconsider k=m-n as Element of NAT by INT_1:5;
defpred X[Nat] means
||.s1.(n+$1) - s1.n.|| <= |.s2.(n+$1) - s2
.n.|;
A1: n+k = m;
now
let k be Nat;
||.s.k.|| >=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<p;
then consider n be Nat such that
A2: for m be Nat st n <= m
holds |.Partial_Sums(||.seq.||).m-Partial_Sums(||.seq.||).n.|< p
by A1,SEQ_4:41;
reconsider n as Nat;
take n;
let m be Nat;
assume
A3: n <= m;
then
A4: ||.Partial_Sums(seq).m-Partial_Sums(seq).n.|| <= |.Partial_Sums(||.
seq.||).m-Partial_Sums(||.seq.||).n.| by Th25;
|.Partial_Sums(||.seq.||).m-Partial_Sums(||.seq.||).n.|< p by A2,A3;
hence ||.Partial_Sums(seq).m-Partial_Sums(seq).n.|| <p by A4,XXREAL_0:2;
end;
hence thesis by Th24;
end;
theorem
for X be RealNormSpace for rseq1 be Real_Sequence for seq2 be sequence
of X holds rseq1 is summable & (ex m be Nat st
for n be Nat st m<=n holds ||.seq2.n.|| <= rseq1.n )
implies seq2 is norm_summable
proof
let X be RealNormSpace;
let rseq1 be Real_Sequence;
let seq2 be sequence of X;
assume that
A1: rseq1 is summable and
A2: ex m be Nat st for n be Nat st m<=n holds ||.
seq2.n.|| <= rseq1.n;
consider m be Nat such that
A3: for n be Nat st m<=n holds ||.seq2.n.|| <= rseq1.n by A2;
A4: now
let n be Nat;
||.seq2.n.||=||.seq2.||.n by NORMSP_0:def 4;
hence 0 <= ||.seq2.||.n;
end;
now
let n be Nat;
assume m <= n;
then ||.seq2.n.|| <= rseq1.n by A3;
hence ||.seq2.||.n <= rseq1.n by NORMSP_0:def 4;
end;
hence ||.seq2.|| is summable by A1,A4,SERIES_1:19;
end;
theorem
for X be RealNormSpace for seq1,seq2 be sequence of X
st (for n be Nat holds 0 <= ||.seq1.||.n & ||.seq1.||.n <= ||.seq2.||.n) &
seq2 is norm_summable
holds seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.||
by SERIES_1:20;
theorem
for X be RealNormSpace for seq be sequence of X holds (for n be
Nat holds ||.seq.||.n>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 :: redefines invertible (ALGSTR_0, definition)
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 :: redefines " (LOPBAN_3, synonym) → / (ALGSTR_0, definition)
: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.|| <e
holds x=0.X
proof
let X be RealNormSpace;
let x be Point of X such that
A1: for e be Real st e > 0 holds ||.x.|| <e;
now
assume x<>0.X;
then 0<> ||.x.|| by NORMSP_0:def 5;
then 0< ||.x.||;
hence contradiction by A1;
end;
hence thesis;
end;
Lm2: for X be RealNormSpace for x,y be Point of X
st for e be Real st e>0 holds ||.x-y.|| <e
holds x=y
proof
let X be RealNormSpace;
let x,y be Point of X;
assume for e be Real st e > 0 holds ||.x-y.|| <e;
then x-y = 0.X by Lm1;
hence thesis by RLVECT_1:21;
end;
Lm3: for X be RealNormSpace for x,y be Point of X for seq be Real_Sequence st
( seq is convergent & lim seq=0 & for n be Nat holds ||.x-y.|| <=seq
.n ) holds x=y
proof
let X be RealNormSpace;
let x,y be Point of X;
let seq be Real_Sequence such that
A1: seq is convergent & lim seq=0 and
A2: for n be Nat holds ||.x-y.|| <=seq.n;
now
let e be Real;
assume 0 < e;
then consider n be Nat such that
A3: for m be Nat st n<=m holds |. seq.m - 0 .| < e by A1,
SEQ_2:def 7;
A4: seq.n <=|. seq.n .| by ABSVALUE:4;
A5: ||.x-y.|| <= seq.n by A2;
|. seq.n -0 .| < e by A3;
then seq.n < e by A4,XXREAL_0:2;
hence ||.x-y.|| < e by A5,XXREAL_0:2;
end;
hence thesis by Lm2;
end;
theorem
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 )
proof
let X be Banach_Algebra;
let x be Point of X such that
A1: ||.1.X - x .|| < 1;
set seq = (1.X - x)GeoSeq;
A2: seq is summable by A1,Th40;
then
A3: ||. seq^\1 .|| is convergent by LOPBAN_1:41;
reconsider y=Sum(seq) as Element of X;
A4: Partial_Sums(seq) is convergent by A2;
then lim ||. Partial_Sums(seq)-y.|| =0 by NORMSP_1:24;
then
A5: lim ( ||. x .|| (#) ||. Partial_Sums(seq)-y.|| ) = ||. x .|| *0 by A4,
NORMSP_1:24,SEQ_2:8
.=0;
lim (seq^\1)=0.X by A2,Th14;
then
A6: lim ( ||. seq^\1 .|| )= ||. 0.X.|| by A2,LOPBAN_1:41;
A7: ||. x .|| (#) ||. Partial_Sums(seq)-y.|| is convergent by A4,NORMSP_1:24
,SEQ_2:7;
then
A8: ||. seq^\1 .|| + ||. x .|| (#) ||. Partial_Sums(seq)-y.|| is convergent
by A3,SEQ_2:5;
A9: lim( ||. seq^\1 .|| + ||. x .|| (#) ||. Partial_Sums(seq)-y.||) = lim(
||. seq^\1 .||) + lim ( ||. x .|| (#) ||. Partial_Sums(seq)-y.||) by A7,A3,
SEQ_2:6
.=0 by A5,A6;
A10: for n be Nat holds (1.X -x)*seq.n=seq.(n+1)
proof
defpred P[Nat] means (1.X -x)*seq.$1=seq.($1+1);
A11: (1.X -x)*seq.0 =(1.X -x)*1.X by Def9
.=(1.X -x) by Th38;
A12: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A13: P[k];
thus (1.X -x)*seq.(k+1) = (1.X -x)*(seq.(k)*(1.X -x)) by Def9
.=(1.X -x)*seq.(k)*(1.X -x) by Th38
.=seq.((k+1)+1) by A13,Def9;
end;
seq.(0+1) =seq.0 * (1.X -x) by Def9
.=1.X * (1.X -x) by Def9
.=(1.X -x) by Th38;
then
A14: P[0] by A11;
for n be Nat holds P[n] from NAT_1:sch 2(A14,A12);
hence thesis;
end;
A15: for n be Nat holds (1.X -x)* (Partial_Sums(seq).n)=(
Partial_Sums(seq)^\1).n-seq.0
proof
defpred P[Nat] means (1.X -x)* (Partial_Sums(seq).$1)=(
Partial_Sums(seq)^\1).$1-seq.0;
A16: (1.X -x)*(Partial_Sums(seq).0) =(1.X -x)*(seq.0) by BHSP_4:def 1
.=(1.X -x)*1.X by Def9
.=1.X -x by Th38;
A17: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A18: P[k];
A19: (Partial_Sums(seq)^\1).(k+1)-seq.0 =(Partial_Sums(seq)).((k+1)+1)-
seq.0 by NAT_1:def 3
.=(Partial_Sums(seq)).(k+1)+seq.((k+1)+1)-seq.0 by BHSP_4:def 1
.=(Partial_Sums(seq)^\1).(k)+seq.((k+1)+1)+(-seq.0) by NAT_1:def 3
.=(Partial_Sums(seq)^\1).(k)-seq.0 +seq.((k+1)+1) by RLVECT_1:def 3;
(1.X -x)*(Partial_Sums(seq).(k+1)) = (1.X -x)*( Partial_Sums(seq).k
+seq.(k+1) ) by BHSP_4:def 1
.=(1.X -x)*(Partial_Sums(seq).k)+(1.X -x)*seq.(k+1) by Th38
.=(Partial_Sums(seq)^\1).k-seq.0+seq.((k+1)+1) by A10,A18;
hence thesis by A19;
end;
(Partial_Sums(seq)^\1).0-seq.0 =(Partial_Sums(seq)).(0+1)-seq.0 by
NAT_1:def 3
.=(Partial_Sums(seq)).(0)+seq.1-seq.0 by BHSP_4:def 1
.=seq.0 + seq.1-seq.0 by BHSP_4:def 1
.=seq.1 +(seq.0-seq.0) by Th38
.=seq.1 + 0.X by RLVECT_1:15
.=seq.(0+1) by RLVECT_1:4
.=seq.0*(1.X -x) by Def9
.=1.X * (1.X -x) by Def9
.=1.X -x by Th38;
then
A20: P[0] by A16;
for n be Nat holds P[n] from NAT_1:sch 2(A20,A17);
hence thesis;
end;
now
let n be Nat;
reconsider yn=Partial_Sums(seq).n as Element of X;
(Partial_Sums(seq)).(n+1) = (Partial_Sums(seq)).n + seq.(n+1) by
BHSP_4:def 1;
then
A21: (Partial_Sums(seq)).(n+1) = (Partial_Sums(seq)).n + (seq ^\1).n by
NAT_1:def 3;
(1.X - (1.X-x))*yn = 1.X*yn - (1.X -x)*yn by Th38
.= yn - (1.X -x)*yn by Th38
.=Partial_Sums(seq).n-((Partial_Sums(seq)^\1).n-seq.0) by A15
.=Partial_Sums(seq).n-(Partial_Sums(seq)^\1).n +seq.0 by Th38;
then (1.X - (1.X-x))*yn =Partial_Sums(seq).n -( (Partial_Sums(seq)).n + (
seq ^\1).n)+seq.0 by A21,NAT_1:def 3
.=Partial_Sums(seq).n-(Partial_Sums(seq)).n - (seq ^\1).n +seq.0 by Th38
.=0.X - (seq ^\1).n +seq.0 by RLVECT_1:15
.=0.X-((seq ^\1).n-seq.0) by RLVECT_1:29
.=-((seq ^\1).n-seq.0) by RLVECT_1:14
.= (seq.0- (seq ^\1).n) by RLVECT_1:33
.=seq.0-seq.(n+1) by NAT_1:def 3
.=1.X - seq.(n+1) by Def9;
then
A22: (1.X-x*yn) =1.X -(1.X - seq.(n+1) ) by Th38
.=seq.(n+1) by Th38
.=(seq^\1).n by NAT_1:def 3;
||. x*(yn-y) .|| <= ||. x .||*||. (yn-y).|| by Th38;
then
A23: ||. (seq^\1).||.n + ||. x*(yn-y) .|| <= ||. (seq^\1).||.n + ||. x .||
* ||. (yn-y).|| by XREAL_1:7;
||. (seq^\1).n+x*(yn-y) .|| <= ||. (seq^\1).n .|| + ||. x*(yn-y) .||
& ||. ( seq^\1).n .|| + ||. x*(yn-y) .|| = ||. (seq^\1).||.n + ||. x*(yn-y) .||
by NORMSP_0:def 4,NORMSP_1:def 1;
then
A24: ||. (seq^\1).n+x*(yn-y) .|| <= ||. (seq^\1).||.n + ||. x .|| * ||. (
yn-y).|| by A23,XXREAL_0:2;
1.X -x*y =1.X - 0.X -x*y by RLVECT_1:13
.=1.X - (x*yn-x*yn) -x*y by RLVECT_1:15
.=1.X-x*yn+x*yn-x*y by RLVECT_1:29
.=(1.X-x*yn)+(x*yn-x*y) by RLVECT_1:def 3
.=(1.X-x*yn)+x*(yn-y) by Th38;
then
||. 1.X -x*y.|| <= ||. (seq^\1).||.n + ||. x .|| * ||. (Partial_Sums(
seq)-y).n.|| by A22,A24,NORMSP_1:def 4;
then ||. 1.X -x*y.|| <= ||. (seq^\1).||.n + ||. x .|| * ||. Partial_Sums(
seq)-y.||.n by NORMSP_0:def 4;
then ||. 1.X -x*y.|| <= ||. (seq^\1).||.n + ( ||. x .|| (#) ||.
Partial_Sums(seq)-y.||).n by SEQ_1:9;
hence
||. 1.X -x*y.|| <=( ||. (seq^\1).|| + ||. x .|| (#) ||. Partial_Sums(
seq)-y.||).n by SEQ_1:7;
end;
then
A25: 1.X = x*y by A8,A9,Lm3;
A26: for n be Nat holds (Partial_Sums(seq).n)*(1.X -x)=(
Partial_Sums(seq)^\1).n-seq.0
proof
defpred P[Nat] means (Partial_Sums(seq).$1)*(1.X -x)=(
Partial_Sums(seq)^\1).$1-seq.0;
A27: (Partial_Sums(seq).0)*(1.X -x) =(seq.0)*(1.X -x) by BHSP_4:def 1
.=1.X *(1.X -x) by Def9
.=1.X -x by Th38;
A28: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A29: P[k];
A30: (Partial_Sums(seq)^\1).(k+1)-seq.0 =(Partial_Sums(seq)).((k+1)+1)-
seq.0 by NAT_1:def 3
.=(Partial_Sums(seq)).(k+1)+seq.((k+1)+1)-seq.0 by BHSP_4:def 1
.=(Partial_Sums(seq)^\1).(k)+seq.((k+1)+1)+(-seq.0) by NAT_1:def 3
.=(Partial_Sums(seq)^\1).(k)-seq.0 +seq.((k+1)+1) by RLVECT_1:def 3;
(Partial_Sums(seq).(k+1))*(1.X -x) = ( Partial_Sums(seq).k+seq.(k+1)
)*(1.X -x) by BHSP_4:def 1
.=(Partial_Sums(seq).k)*(1.X -x)+seq.(k+1)*(1.X -x) by Th38
.=(Partial_Sums(seq)^\1).k-seq.0+seq.((k+1)+1) by A29,Def9;
hence thesis by A30;
end;
(Partial_Sums(seq)^\1).0-seq.0 =(Partial_Sums(seq)).(0+1)-seq.0 by
NAT_1:def 3
.=(Partial_Sums(seq)).(0)+seq.1-seq.0 by BHSP_4:def 1
.=seq.0 + seq.1-seq.0 by BHSP_4:def 1
.=seq.1 +(seq.0-seq.0) by Th38
.=seq.1 + 0.X by RLVECT_1:15
.=seq.(0+1) by RLVECT_1:4
.=seq.0*(1.X -x) by Def9
.=1.X * (1.X -x) by Def9
.=1.X -x by Th38;
then
A31: P[0] by A27;
for n be Nat holds P[n] from NAT_1:sch 2(A31,A28);
hence thesis;
end;
now
let n be Nat;
reconsider yn=Partial_Sums(seq).n as Element of X;
(Partial_Sums(seq)).(n+1) = (Partial_Sums(seq)).n + seq.(n+1) by
BHSP_4:def 1;
then
A32: (Partial_Sums(seq)).(n+1) = (Partial_Sums(seq)).n + (seq ^\1).n by
NAT_1:def 3;
yn*(1.X - (1.X-x)) = yn*1.X - yn*(1.X -x) by Th38
.= yn - yn*(1.X -x) by Th38
.=Partial_Sums(seq).n-((Partial_Sums(seq)^\1).n-seq.0) by A26
.=Partial_Sums(seq).n-(Partial_Sums(seq)^\1).n +seq.0 by Th38;
then yn*(1.X - (1.X-x)) =Partial_Sums(seq).n -( (Partial_Sums(seq)).n + (
seq ^\1).n)+seq.0 by A32,NAT_1:def 3
.=Partial_Sums(seq).n-(Partial_Sums(seq)).n - (seq ^\1).n +seq.0 by Th38
.=0.X - (seq ^\1).n +seq.0 by RLVECT_1:15
.=0.X-((seq ^\1).n-seq.0) by RLVECT_1:29
.=-((seq ^\1).n-seq.0) by RLVECT_1:14
.= (seq.0- (seq ^\1).n) by RLVECT_1:33
.=seq.0-seq.(n+1) by NAT_1:def 3
.=1.X - seq.(n+1) by Def9;
then
A33: (1.X-yn*x) =1.X -(1.X - seq.(n+1) ) by Th38
.=seq.(n+1) by Th38
.=(seq^\1).n by NAT_1:def 3;
||. (yn-y)*x .|| <= ||. (yn-y).|| * ||. x .|| by Th38;
then
A34: ||. (seq^\1).||.n + ||. (yn-y)*x .|| <= ||. (seq^\1).||.n + ||. (yn-y
).|| * ||. x .|| by XREAL_1:7;
||. (seq^\1).n+(yn-y)*x .|| <= ||. (seq^\1).n .|| + ||. (yn-y)*x .||
& ||. ( seq^\1).n .|| + ||. (yn-y)*x .|| = ||. (seq^\1).||.n + ||. (yn-y)*x .||
by NORMSP_0:def 4,NORMSP_1:def 1;
then
A35: ||. (seq^\1).n+(yn-y)*x .|| <= ||. (seq^\1).||.n + ||. (yn-y).|| *
||. x .|| by A34,XXREAL_0:2;
1.X -y*x =1.X - 0.X -y*x by RLVECT_1:13
.=1.X - (yn*x-yn*x) -y*x by RLVECT_1:15
.=1.X-yn*x+yn*x-y*x by RLVECT_1:29
.=(1.X-yn*x)+(yn*x-y*x) by RLVECT_1:def 3
.=(1.X-yn*x)+(yn-y)*x by Th38;
then ||. 1.X -y*x.|| <= ||. (seq^\1).||.n + ||.(Partial_Sums(seq)-y).n.||
* ||.x.|| by A33,A35,NORMSP_1:def 4;
then
||. 1.X -y*x.|| <= ||. (seq^\1).||.n + ||. Partial_Sums(seq)-y.||.n *
||. x .|| by NORMSP_0:def 4;
then ||. 1.X -y*x.|| <= ||. (seq^\1).||.n + ( ||. x .|| (#) ||.
Partial_Sums(seq)-y.||).n by SEQ_1:9;
hence
||. 1.X -y*x.|| <=( ||. (seq^\1).|| + ||. x .|| (#) ||. Partial_Sums(
seq)-y.||).n by SEQ_1:7;
end;
then
A36: 1.X = y*x by A8,A9,Lm3;
hence x is invertible by A25;
hence thesis by A36,A25,Def8;
end;