:: Series in Banach and Hilbert Spaces
:: by El\.zbieta Kraszewska and Jan Popio{\l}ek
::
:: Received April 1, 1992
:: Copyright (c) 1992-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, REAL_1, SEQ_1, SUBSET_1, BHSP_1, SUPINF_2, XBOOLE_0,
ALGSTR_0, NAT_1, SERIES_1, FUNCT_1, CARD_1, ARYTM_3, PRE_TOPC, STRUCT_0,
RLVECT_1, ARYTM_1, RELAT_1, SEQ_2, CARD_3, ORDINAL2, BHSP_3, XXREAL_0,
NORMSP_1, XXREAL_2, FUNCOP_1, COMPLEX1, VALUED_1, POWER, NEWTON,
VALUED_0, INT_1, METRIC_1, RSSPACE2;
notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, ALGSTR_0,
REAL_1, INT_1, NAT_1, FUNCT_2, FUNCOP_1, VALUED_1, SEQ_1, SEQ_2,
SERIES_1, VALUED_0, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_1,
BHSP_1, BHSP_2, BHSP_3, RSSPACE2, NEWTON, POWER, XXREAL_0;
constructors REAL_1, SEQ_2, NEWTON, SERIES_1, BHSP_2, BHSP_3, RELSET_1, ABIAN,
BINOP_2, VFUNCT_1, COMSEQ_2;
registrations ORDINAL1, RELSET_1, XREAL_0, INT_1, MEMBERED, STRUCT_0,
RLVECT_1, VALUED_0, VALUED_1, FUNCT_2, NUMBERS, FUNCOP_1, VFUNCT_1,
BHSP_2, BHSP_3, NEWTON, NAT_1;
requirements NUMERALS, REAL, SUBSET, ARITHM;
definitions FUNCT_2;
equalities RLVECT_1, SERIES_1, VALUED_1;
expansions FUNCT_2, VALUED_1;
theorems NAT_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, SERIES_1, ABSVALUE, RLVECT_1,
BHSP_1, BHSP_2, BHSP_3, PREPOWER, POWER, INT_1, NORMSP_1, XCMPLX_1,
FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1;
schemes NAT_1, FUNCT_2;
begin
reserve a, b, r, M2 for Real;
reserve Rseq,Rseq1,Rseq2 for Real_Sequence;
reserve k, n, m, m1, m2 for Nat;
deffunc 09(RealUnitarySpace) = 0.$1;
definition
let X be non empty addLoopStr;
let seq be sequence of X;
func Partial_Sums(seq) -> sequence of X means
:Def1:
it.0 = seq.0 & for n holds it.(n + 1) = it.n + seq.(n + 1);
existence
proof
deffunc G(Nat,Point of X) = $2 + seq.($1 + 1);
consider f being sequence of the carrier of X such that
A1: f.0 = seq.0 & for n being Nat holds f.(n + 1) = G(n,f.n) from
NAT_1:sch 12;
take f;
thus thesis by A1;
end;
uniqueness
proof
let seq1,seq2 be sequence of X;
assume that
A2: seq1.0 = seq.0 and
A3: for n holds seq1.(n + 1) = seq1.n + seq.(n + 1) and
A4: seq2.0 = seq.0 and
A5: for n holds seq2.(n + 1) = seq2.n + seq.(n + 1);
defpred P[Nat] means seq1.$1 = seq2.$1;
A6: for k st P[k] holds P[k+1]
proof
let k;
assume seq1.k =seq2.k;
hence seq1.(k + 1) = seq2.k + seq.(k+1) by A3
.= seq2.(k + 1) by A5;
end;
A7: P[0] by A2,A4;
for n holds P[n] from NAT_1:sch 2(A7,A6);
then for n being Element of NAT holds P[n];
hence seq1 = seq2;
end;
end;
theorem Th1:
for X being Abelian add-associative non empty addLoopStr, seq1,
seq2 being sequence of X holds Partial_Sums(seq1) + Partial_Sums(seq2) =
Partial_Sums(seq1 + seq2)
proof
let X be Abelian add-associative non empty addLoopStr, seq1, seq2 be
sequence of X;
set PSseq1 = Partial_Sums(seq1);
set PSseq2 = Partial_Sums(seq2);
A1: now
let n;
thus (PSseq1 + PSseq2).(n + 1) = PSseq1.(n + 1) + PSseq2.(n + 1) by
NORMSP_1:def 2
.= PSseq1.n + seq1.(n + 1) + PSseq2.(n + 1) by Def1
.= PSseq1.n + seq1.(n + 1) + (seq2.(n + 1) + PSseq2.n) by Def1
.= PSseq1.n + seq1.(n + 1) + seq2.(n + 1) + PSseq2.n by RLVECT_1:def 3
.= PSseq1.n + (seq1.(n + 1) + seq2.(n + 1)) + PSseq2.n by RLVECT_1:def 3
.= PSseq1.n + (seq1 + seq2).(n + 1) + PSseq2.n by NORMSP_1:def 2
.= PSseq1.n + PSseq2.n + (seq1 + seq2).(n + 1) by RLVECT_1:def 3
.= (PSseq1 + PSseq2).n + (seq1 + seq2).(n + 1) by NORMSP_1:def 2;
end;
(PSseq1 + PSseq2).0 = PSseq1.0 + PSseq2.0 by NORMSP_1:def 2
.= seq1.0 + PSseq2.0 by Def1
.= seq1.0 + seq2.0 by Def1
.= (seq1 + seq2).0 by NORMSP_1:def 2;
hence thesis by A1,Def1;
end;
theorem Th2:
for X being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, seq1, seq2 being sequence of X
holds Partial_Sums(seq1) - Partial_Sums(seq2) = Partial_Sums(seq1 - seq2)
proof
let X be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, seq1, seq2 be sequence of X;
set PSseq1 = Partial_Sums(seq1);
set PSseq2 = Partial_Sums(seq2);
A1: now
let n;
thus (PSseq1 - PSseq2).(n + 1) = PSseq1.(n + 1) - PSseq2.(n + 1) by
NORMSP_1:def 3
.= (PSseq1.n + seq1.(n + 1)) - PSseq2.(n + 1) by Def1
.= (PSseq1.n + seq1.(n + 1)) - (seq2.(n + 1) + PSseq2.n) by Def1
.= ((PSseq1.n + seq1.(n + 1)) - seq2.(n + 1)) - PSseq2.n by RLVECT_1:27
.= (PSseq1.n + (seq1.(n + 1) - seq2.(n + 1))) - PSseq2.n by
RLVECT_1:def 3
.= (PSseq1.n - PSseq2.n) + (seq1.(n + 1) - seq2.(n + 1)) by
RLVECT_1:def 3
.= (PSseq1 - PSseq2).n + (seq1.(n + 1) - seq2.(n + 1)) by NORMSP_1:def 3
.= (PSseq1 - PSseq2).n + (seq1 - seq2).(n + 1) by NORMSP_1:def 3;
end;
(PSseq1 - PSseq2).0 = (PSseq1).0 - (PSseq2).0 by NORMSP_1:def 3
.= seq1.0 - (PSseq2).0 by Def1
.= seq1.0 - seq2.0 by Def1
.= (seq1 - seq2).0 by NORMSP_1:def 3;
hence thesis by A1,Def1;
end;
theorem Th3:
for X being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, seq being
sequence of X holds Partial_Sums(a * seq) = a * Partial_Sums(seq)
proof
let X be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, seq be sequence of X;
set PSseq = Partial_Sums(seq);
A1: now
let n;
thus (a * PSseq).(n + 1) = a * PSseq.(n + 1) by NORMSP_1:def 5
.= a * (PSseq.n + seq.(n + 1)) by Def1
.= a * PSseq.n + a * seq.(n + 1) by RLVECT_1:def 5
.= (a * PSseq).n + a * seq.(n + 1) by NORMSP_1:def 5
.= (a * PSseq).n + (a * seq).(n + 1) by NORMSP_1:def 5;
end;
(a * PSseq).0 = a * PSseq.0 by NORMSP_1:def 5
.= a * seq.0 by Def1
.= (a * seq).0 by NORMSP_1:def 5;
hence thesis by A1,Def1;
end;
reserve X for RealUnitarySpace;
reserve g for Point of X;
reserve seq, seq1, seq2 for sequence of X;
theorem
Partial_Sums(- seq) = - Partial_Sums(seq)
proof
Partial_Sums((-1) * seq) = (-1) * Partial_Sums(seq) by Th3;
then Partial_Sums(- seq) = (-1) * Partial_Sums(seq) by BHSP_1:55;
hence thesis by BHSP_1:55;
end;
theorem
a * Partial_Sums(seq1) + b * Partial_Sums(seq2) = Partial_Sums(a *
seq1 + b * seq2)
proof
thus a * Partial_Sums(seq1) + b * Partial_Sums(seq2) = Partial_Sums(a * seq1
) + b * Partial_Sums(seq2) by Th3
.= Partial_Sums(a * seq1) + Partial_Sums(b * seq2) by Th3
.= Partial_Sums(a * seq1 + b * seq2) by Th1;
end;
definition
let X, seq;
attr seq is summable means
:Def2:
Partial_Sums(seq) is convergent;
func Sum(seq) -> Point of X equals
lim Partial_Sums(seq);
coherence;
end;
theorem
seq1 is summable & seq2 is summable implies seq1 + seq2 is summable &
Sum(seq1 + seq2) = Sum(seq1) + Sum(seq2)
proof
assume seq1 is summable & seq2 is summable;
then
A1: Partial_Sums(seq1) is convergent & Partial_Sums(seq2) is convergent;
then Partial_Sums(seq1) + Partial_Sums(seq2) is convergent by BHSP_2:3;
then Partial_Sums(seq1 + seq2) is convergent by Th1;
hence seq1 + seq2 is summable;
thus Sum(seq1 + seq2) = lim (Partial_Sums(seq1) + Partial_Sums(seq2)) by Th1
.= Sum(seq1) + Sum(seq2) by A1,BHSP_2:13;
end;
theorem
seq1 is summable & seq2 is summable implies seq1 - seq2 is summable &
Sum(seq1 - seq2) = Sum(seq1) - Sum(seq2)
proof
assume seq1 is summable & seq2 is summable;
then
A1: Partial_Sums(seq1) is convergent & Partial_Sums(seq2) is convergent;
then Partial_Sums(seq1) - Partial_Sums(seq2) is convergent by BHSP_2:4;
then Partial_Sums(seq1 - seq2) is convergent by Th2;
hence seq1 - seq2 is summable;
thus Sum(seq1 - seq2) = lim (Partial_Sums(seq1) - Partial_Sums(seq2)) by Th2
.= Sum(seq1) - Sum(seq2) by A1,BHSP_2:14;
end;
theorem
seq is summable implies a * seq is summable & Sum(a * seq) = a * Sum( seq)
proof
assume seq is summable;
then
A1: Partial_Sums(seq) is convergent;
then a * Partial_Sums(seq) is convergent by BHSP_2:5;
then Partial_Sums(a * seq) is convergent by Th3;
hence a * seq is summable;
thus Sum(a * seq) = lim (a * Partial_Sums(seq)) by Th3
.= a * Sum(seq) by A1,BHSP_2:15;
end;
theorem Th9:
seq is summable implies seq is convergent & lim seq = 0.X
proof
set PSseq = Partial_Sums(seq);
now
let n;
(PSseq).(n + 1) = (PSseq).n + seq.(n + 1) by Def1
.= (PSseq).n + (seq ^\1).n by NAT_1:def 3;
hence (PSseq ^\1).n = (PSseq).n + (seq ^\1).n by NAT_1:def 3;
end;
then
A1: (PSseq ^\1) = PSseq + seq ^\1 by NORMSP_1:def 2;
seq ^\1 + (PSseq - PSseq) = seq ^\1
proof
let n be Element of NAT;
thus (seq ^\1 + (PSseq - PSseq)).n = (seq ^\1).n + (PSseq - PSseq).n
by NORMSP_1:def 2
.= (seq ^\1).n + (PSseq.n - PSseq.n) by NORMSP_1:def 3
.= (seq ^\1).n + 09(X) by RLVECT_1:15
.= (seq ^\1).n;
end;
then
A2: seq ^\1 = PSseq ^\1 - PSseq by A1,BHSP_1:61;
assume seq is summable;
then
A3: PSseq is convergent;
A4: seq ^\1 is convergent by A3,A2,BHSP_2:4;
hence seq is convergent by BHSP_3:37;
lim(PSseq ^\1) = lim(PSseq) by A3,BHSP_3:36;
then lim(PSseq ^\1 - PSseq) = lim(PSseq) - lim(PSseq) by A3,BHSP_2:14
.= 09(X) by RLVECT_1:15;
hence thesis by A2,A4,BHSP_3:28,37;
end;
theorem Th10:
for X being RealHilbertSpace, seq being sequence of X
holds seq is summable iff for r st r > 0 ex k
st for n, m st n >= k & m >= k holds ||.(Partial_Sums(seq)).n - (Partial_Sums(
seq)).m.|| < r
by BHSP_3:2,BHSP_3:def 4;
theorem
seq is summable implies Partial_Sums(seq) is bounded;
theorem Th12:
for seq, seq1 st for n holds seq1.n = seq.0 holds Partial_Sums(
seq^\1) = (Partial_Sums(seq)^\1) - seq1
proof
let seq, seq1;
assume
A1: for n holds seq1.n = seq.0;
A2: now
let n;
thus ((Partial_Sums(seq)^\1) - seq1).(n + 1) = (Partial_Sums(seq)^\1).(n +
1) - seq1.(n + 1) by NORMSP_1:def 3
.= (Partial_Sums(seq)^\1).(n + 1) - seq.0 by A1
.= Partial_Sums(seq).(n + 1 + 1) - seq.0 by NAT_1:def 3
.= seq.(n + 1 + 1) + Partial_Sums(seq).(n + 1) - seq.0 by Def1
.= seq.(n + 1 + 1) + Partial_Sums(seq).(n + 1) - seq1.n by A1
.= seq.(n + 1 + 1) + (Partial_Sums(seq).(n + 1) - seq1.n) by
RLVECT_1:def 3
.= seq.(n + 1 + 1) + ((Partial_Sums(seq)^\1).n - seq1.n) by NAT_1:def 3
.= seq.(n + 1 + 1) + ((Partial_Sums(seq)^\1) - seq1).n by NORMSP_1:def 3
.= ((Partial_Sums(seq)^\1) - seq1).n + (seq^\1).(n + 1) by NAT_1:def 3;
end;
((Partial_Sums(seq)^\1) - seq1).0 = (Partial_Sums(seq)^\1).0 - seq1.0 by
NORMSP_1:def 3
.= (Partial_Sums(seq)^\1).0 - seq.0 by A1
.= Partial_Sums(seq).(0 + 1) - seq.0 by NAT_1:def 3
.= Partial_Sums(seq).0 + seq.(0 + 1) - seq.0 by Def1
.= seq.(0 + 1) + seq.0 - seq.0 by Def1
.= seq.(0 + 1) + (seq.0 - seq.0) by RLVECT_1:def 3
.= seq.(0 + 1) + 09(X) by RLVECT_1:15
.= seq.(0 + 1)
.= (seq^\1).0 by NAT_1:def 3;
hence thesis by A2,Def1;
end;
theorem Th13:
seq is summable implies for k holds seq^\k is summable
proof
defpred P[Nat] means seq^\($1) is summable;
A1: for k st P[k] holds P[k+1]
proof
let k;
reconsider seq1 = NAT --> (seq^\k).0 as sequence of X;
assume seq^\k is summable;
then
A2: Partial_Sums(seq^\k) is convergent;
for m holds seq1.m = (seq^\k).0
by ORDINAL1:def 12,FUNCOP_1:7;
then
seq1 is convergent & Partial_Sums(seq^\k^\1) = (Partial_Sums(seq^\k)^\
1) - seq1 by Th12;
then
seq^\(k+1)=(seq^\k)^\1 & Partial_Sums(seq^\k^\1) is convergent
by A2,BHSP_2:4,BHSP_3:31;
hence thesis by Def2;
end;
assume seq is summable;
then
A3: P[0] by NAT_1:47;
thus for k holds P[k] from NAT_1:sch 2(A3,A1);
end;
theorem
(ex k st seq^\k is summable) implies seq is summable
proof
given k such that
A1: seq^\k is summable;
seq^\k^\1 is summable by A1,Th13;
then
A2: Partial_Sums(seq^\k^\1) is convergent;
reconsider seq1 = NAT --> Partial_Sums(seq).k as sequence of X;
defpred P[Nat] means
(Partial_Sums(seq)^\(k+1)).$1 = Partial_Sums
(seq^\(k+1)).$1 + seq1.$1;
A3: Partial_Sums(seq^\(k+1)).0 = (seq^\(k+1)).0 by Def1
.= seq.(0+(k+1)) by NAT_1:def 3
.= seq.(k+1);
A4: now
let m;
A5: m in NAT by ORDINAL1:def 12;
assume
A6: P[m];
Partial_Sums(seq^\(k+1)).(m+1) + seq1.(m+1) = seq1.(m+1) + (
Partial_Sums(seq^\(k+1)).m + (seq^\(k+1)).(m+1)) by Def1
.= seq1.(m+1) + Partial_Sums(seq^\(k+1)).m + (seq^\(k+1)).(m+1) by
RLVECT_1:def 3
.= Partial_Sums(seq).k + Partial_Sums(seq^\(k+1)).m + (seq^\(k+1)).(m+
1)
.= (Partial_Sums(seq)^\(k+1)).m + (seq^\(k+1)).(m+1) by A6,FUNCOP_1:7,A5
.= Partial_Sums(seq).(m+(k+1)) + (seq^\(k+1)).(m+1) by NAT_1:def 3
.= Partial_Sums(seq).(m+(k+1)) + seq.(m+1+(k+1)) by NAT_1:def 3
.= Partial_Sums(seq).(m+(k+1)+1) by Def1
.= Partial_Sums(seq).(m+1+(k+1))
.= (Partial_Sums(seq)^\(k+1)).(m+1) by NAT_1:def 3;
hence P[m+1];
end;
(Partial_Sums(seq)^\(k+1)).0 = Partial_Sums(seq).(0+(k+1)) by NAT_1:def 3
.= Partial_Sums(seq).k + seq.(k+1) by Def1
.= Partial_Sums(seq^\(k+1)).0 + seq1.0 by A3;
then
A7: P[0];
for m holds P[m] from NAT_1:sch 2(A7,A4);
then
A8: Partial_Sums(seq)^\(k+1) = Partial_Sums(seq^\(k+1)) + seq1 by
NORMSP_1:def 2
.= Partial_Sums((seq^\k)^\1) + seq1 by BHSP_3:31;
Partial_Sums(seq)^\(k+1) is convergent by A2,A8,BHSP_2:3;
hence thesis by BHSP_3:37;
end;
definition
let X, seq, n;
func Sum(seq,n) -> Point of X equals
Partial_Sums(seq).n;
coherence;
end;
theorem
Sum(seq, 0) = seq.0 by Def1;
theorem Th16:
Sum(seq, 1) = Sum(seq, 0) + seq.1
proof
Partial_Sums(seq).1 = Partial_Sums(seq).0 + seq.(0 + 1) by Def1
.= Partial_Sums(seq).0 + seq.1;
hence thesis;
end;
theorem Th17:
Sum(seq, 1) = seq.0 + seq.1
proof
thus Sum(seq, 1) = Sum(seq, 0) + seq.1 by Th16
.= seq.0 + seq.1 by Def1;
end;
theorem
Sum(seq, n + 1) = Sum(seq, n) + seq.(n + 1) by Def1;
theorem Th19:
seq.(n + 1) = Sum(seq, n + 1) - Sum(seq, n)
proof
thus Sum(seq, n + 1) - Sum(seq, n) = ( seq.(n + 1) + Sum(seq, n) ) - Sum(seq
, n) by Def1
.= seq.(n + 1) + ( Sum(seq, n) - Sum(seq, n) ) by RLVECT_1:def 3
.= seq.(n + 1) + 0.X by RLVECT_1:15
.= seq.(n + 1);
end;
theorem
seq.1 = Sum(seq, 1) - Sum(seq, 0)
proof
seq.(0 + 1) = Sum(seq, 0 + 1) - Sum(seq, 0) by Th19;
hence thesis;
end;
definition
let X, seq, n, m;
func Sum(seq, n, m) -> Point of X equals
Sum(seq, n) - Sum(seq, m);
coherence;
end;
theorem
Sum(seq, 1, 0) = seq.1
proof
Sum(seq, 1, 0) = (seq.0 + seq.1) - Sum(seq, 0) by Th17
.= (seq.1 + seq.0) - seq.0 by Def1
.= seq.1 + (seq.0 - seq.0) by RLVECT_1:def 3
.= seq.1 + 09(X) by RLVECT_1:15;
hence thesis;
end;
theorem
Sum(seq, n+1, n) = seq.(n+1) by Th19;
theorem Th23:
for X being RealHilbertSpace, seq being sequence of X
holds seq is summable iff for r st r > 0 ex k
st for n, m st n >= k & m >= k holds ||.Sum(seq, n) - Sum(seq, m).|| < r
proof
let X be RealHilbertSpace, seq be sequence of X;
thus seq is summable implies for r st r > 0 ex k st for n, m st n >= k & m
>= k holds ||.Sum(seq, n) - Sum(seq, m).|| < r
proof
assume
A1: seq is summable;
now
let r;
assume r > 0;
then consider k such that
A2: for n, m st n >= k & m >= k holds ||.(Partial_Sums(seq)).n - (
Partial_Sums(seq)).m.|| < r by A1,Th10;
take k;
let n, m;
assume n >= k & m >= k;
hence ||.Sum(seq, n) - Sum(seq, m).|| < r by A2;
end;
hence thesis;
end;
thus ( for r st r > 0 ex k st for n, m st n >= k & m >= k holds ||.Sum(seq,
n) - Sum(seq, m).|| < r ) implies seq is summable
proof
assume
A3: for r st r > 0 ex k st for n, m st n >= k & m >= k holds ||.Sum(
seq, n) - Sum(seq, m).|| < r;
now
let r;
assume r > 0;
then consider k such that
A4: for n, m st n >= k & m >= k holds ||.Sum(seq, n) - Sum(seq, m)
.|| < r by A3;
take k;
let n, m;
assume n >= k & m >= k;
then ||.Sum(seq, n) - Sum(seq, m).|| < r by A4;
hence ||.( Partial_Sums(seq)).n - (Partial_Sums(seq)).m.|| < r;
end;
hence thesis by Th10;
end;
end;
theorem
for X being RealHilbertSpace, seq being sequence of X
holds seq is summable iff for r st r > 0 ex k st for
n, m st n >= k & m >= k holds ||.Sum(seq, n, m).|| < r
proof
let X be RealHilbertSpace, seq be sequence of X;
thus seq is summable implies for r st r > 0 ex k st for n, m st n >= k & m
>= k holds ||.Sum(seq, n, m).|| < r
proof
assume
A1: seq is summable;
now
let r;
assume r > 0;
then consider k such that
A2: for n, m st n >= k & m >= k holds ||.Sum(seq, n) - Sum(seq, m)
.|| < r by A1,Th23;
take k;
let n, m;
assume n >= k & m >= k;
hence ||.Sum(seq, n, m).|| < r by A2;
end;
hence thesis;
end;
thus ( for r st r > 0 ex k st for n, m st n >= k & m >= k holds ||.Sum(seq,
n, m).|| < r ) implies seq is summable
proof
assume
A3: for r st r > 0 ex k st for n, m st n >= k & m >= k holds ||.Sum(
seq, n, m).|| < r;
now
let r;
assume r > 0;
then consider k such that
A4: for n, m st n >= k & m >= k holds ||.Sum(seq, n, m).|| < r by A3;
take k;
let n, m;
assume n >= k & m >= k;
then ||.Sum(seq, n, m).|| < r by A4;
hence ||.Sum(seq, n) - Sum(seq, m).|| < r;
end;
hence thesis by Th23;
end;
end;
definition
let X, seq;
attr seq is absolutely_summable means
||.seq.|| is summable;
end;
theorem
seq1 is absolutely_summable & seq2 is absolutely_summable implies seq1
+ seq2 is absolutely_summable
proof
A1: for n being Nat
holds ||.seq1 + seq2.||.n >= 0 & ||.seq1 + seq2.||.n <= (||.seq1
.|| + ||.seq2.||).n
proof
let n be Nat;
||.seq1 + seq2.||.n = ||.(seq1 + seq2).n.|| by BHSP_2:def 3;
hence ||.seq1 + seq2.||.n >= 0 by BHSP_1:28;
||.seq1 + seq2.||.n = ||.(seq1 + seq2).n.|| by BHSP_2:def 3
.= ||.(seq1).n + (seq2).n.|| by NORMSP_1:def 2;
then ||.seq1 + seq2.||.n <= ||.(seq1).n.|| + ||.(seq2).n.|| by BHSP_1:30;
then ||.seq1 + seq2.||.n <= ||.seq1.||.n + ||.(seq2).n.|| by BHSP_2:def 3;
then ||.seq1 + seq2.||.n <= ||.seq1.||.n + ||.seq2.||.n by BHSP_2:def 3;
hence ||.seq1 + seq2.||.n <= (||.seq1.|| + ||.seq2.||).n by SEQ_1:7;
end;
assume seq1 is absolutely_summable & seq2 is absolutely_summable;
then ||.seq1.|| is summable & ||.seq2.|| is summable;
then ||.seq1.|| + ||.seq2.|| is summable by SERIES_1:7;
then ||.seq1 + seq2.|| is summable by A1,SERIES_1:20;
hence thesis;
end;
theorem
seq is absolutely_summable implies a * seq is absolutely_summable
proof
A1: for n being Nat
holds ||.a * seq.||.n >= 0 & ||.a * seq.||.n <= (|.a.| (#) ||.seq
.||).n
proof
let n be Nat;
||.a * seq.||.n = ||.(a * seq).n.|| by BHSP_2:def 3;
hence ||.a * seq.||.n >= 0 by BHSP_1:28;
||.a * seq.||.n = ||.(a * seq).n.|| by BHSP_2:def 3
.= ||.a * seq.n.|| by NORMSP_1:def 5
.= |.a.| * ||.seq.n.|| by BHSP_1:27
.= |.a.| * ||.seq.||.n by BHSP_2:def 3
.= (|.a.| (#) ||.seq.||).n by SEQ_1:9;
hence ||.a * seq.||.n <= (|.a.| (#) ||.seq.||).n;
end;
assume seq is absolutely_summable;
then ||.seq.|| is summable;
then |.a.| (#) ||.seq.|| is summable by SERIES_1:10;
then ||.a * seq.|| is summable by A1,SERIES_1:20;
hence thesis;
end;
theorem
( for n being Nat holds ||.seq.||.n <= Rseq.n ) &
Rseq is summable implies seq
is absolutely_summable
proof
A1: for n being Nat holds ||.seq.||.n >= 0
proof
let n be Nat;
||.seq.||.n = ||.seq.n.|| by BHSP_2:def 3;
hence thesis by BHSP_1:28;
end;
assume ( for n being Nat holds ||.seq.||.n <= Rseq.n)& Rseq is summable;
then ||.seq.|| is summable by A1,SERIES_1:20;
hence thesis;
end;
theorem
( for n being Nat holds seq.n <> 0.X &
Rseq.n = ||.seq.(n+1).||/||.seq.n.|| ) &
Rseq is convergent & lim Rseq < 1 implies seq is absolutely_summable
proof
assume that
A1: for n being Nat
holds seq.n <> 09(X) & Rseq.n = ||.seq.(n+1).||/||.seq.n.|| and
A2: Rseq is convergent & lim Rseq < 1;
for n being Nat
holds ||.seq.||.n > 0 & Rseq.n = ||.seq.||.(n+1)/||.seq.||.n
proof
let n be Nat;
A3: ||.seq.n.|| <> 0 by A1,BHSP_1:26;
||.seq.n.|| >= 0 by BHSP_1:28;
hence ||.seq.||.n > 0 by A3,BHSP_2:def 3;
Rseq.n = ||.seq.(n+1).||/||.seq.n.|| by A1
.= ||.seq.||.(n+1)/||.seq.n.|| by BHSP_2:def 3;
hence Rseq.n = ||.seq.||.(n+1)/||.seq.||.n by BHSP_2:def 3;
end;
hence thesis by A2,SERIES_1:26;
end;
theorem Th29:
r > 0 & ( ex m st for n st n >= m holds ||.seq.n.|| >= r)
implies not seq is convergent or lim seq <> 0.X
proof
assume
A1: r > 0;
given m such that
A2: for n st n >= m holds ||.seq.n.|| >= r;
per cases;
suppose
not seq is convergent;
hence thesis;
end;
suppose
A3: seq is convergent;
now
assume lim seq = 09(X);
then consider k being Nat such that
A4: for n being Nat
st n >= k holds ||.seq.n - 09(X).|| < r by A1,A3,BHSP_2:19;
set n = m+k;
m+k >= k by NAT_1:11;
then n >= k;
then ||.seq.n - 09(X).|| < r by A4;
then
A5: ||.seq.n.|| < r;
m+k >= m by NAT_1:11;
then n >= m;
hence contradiction by A2,A5;
end;
hence thesis;
end;
end;
theorem Th30:
( for n holds seq.n <> 0.X ) & ( ex m st for n st n >= m holds
||.seq.(n+1).||/||.seq.n.|| >= 1 ) implies not seq is summable
proof
assume
A1: for n holds seq.n <> 09(X);
given m such that
A2: for n st n >= m holds ||.seq.(n+1).||/||.seq.n.|| >= 1;
A3: now
defpred P[Nat] means ||.seq.(m+$1).|| >= ||.seq.m.||;
let n;
A4: for k st P[k] holds P[k+1]
proof
let k;
assume
A5: ||.seq.(m+k).|| >= ||.seq.m.||;
A6: ||.seq.(m+k).|| <> 0 by A1,BHSP_1:26;
||.seq.(m+k+1).||/||.seq.(m+k).|| >= 1 & ||.seq.(m+k).|| >= 0 by A2,
BHSP_1:28,NAT_1:11;
then ||.seq.(m+k+1).|| >= ||.seq.(m+k).|| by A6,XREAL_1:191;
hence thesis by A5,XXREAL_0:2;
end;
A7: P[0];
A8: for k holds P[k] from NAT_1:sch 2(A7,A4);
assume n >= m;
then consider k be Nat such that
A9: n = m + k by NAT_1:10;
thus ||.seq.n.|| >= ||.seq.m.|| by A8,A9;
end;
A10: ||.seq.m.|| <> 0 by A1,BHSP_1:26;
||.seq.m.|| >= 0 by BHSP_1:28;
then not seq is convergent or lim seq <> 09(X) by A10,A3,Th29;
hence thesis by Th9;
end;
theorem
(for n holds seq.n <> 0.X) & (for n holds Rseq.n = ||.seq.(n+1).||/||.
seq.n.||) & Rseq is convergent & lim Rseq > 1 implies not seq is summable
proof
assume that
A1: for n holds seq.n <> 09(X) and
A2: for n holds Rseq.n = ||.seq.(n+1).||/||.seq.n.|| and
A3: Rseq is convergent and
A4: lim Rseq > 1;
lim Rseq - 1 > 0 by A4,XREAL_1:50;
then consider m being Nat such that
A5: for n being Nat st n >= m
holds |.Rseq.n - lim Rseq.| < lim Rseq - 1 by A3,
SEQ_2:def 7;
now
let n;
A6: m + 1 >= m by NAT_1:11;
A7: Rseq.n = ||.seq.(n+1).||/||.seq.n.|| by A2;
assume n >= m + 1;
then n >= m by A6,XXREAL_0:2;
then
|.||.seq.(n+1).||/||.seq.n.|| - lim Rseq.| < lim Rseq - 1 by A5,A7;
then - (lim Rseq - 1) < ||.seq.(n+1).||/||.seq.n.|| - lim Rseq by SEQ_2:1;
then 1 - lim Rseq + lim Rseq < ||.seq.(n+1).||/||.seq.n.|| - lim Rseq +
lim Rseq by XREAL_1:6;
hence ||.seq.(n+1).||/||.seq.n.|| >= 1;
end;
hence thesis by A1,Th30;
end;
theorem
( for n holds Rseq.n = n-root (||.seq.n.||) ) & Rseq is convergent &
lim Rseq < 1 implies seq is absolutely_summable
proof
assume that
A1: for n holds Rseq.n = n-root (||.seq.n.||) and
A2: Rseq is convergent & lim Rseq < 1;
for n being Nat holds ||.seq.||.n >= 0 & Rseq.n = n-root (||.seq.||.n)
proof
let n be Nat;
||.seq.||.n = ||.seq.n.|| by BHSP_2:def 3;
hence ||.seq.||.n >= 0 by BHSP_1:28;
Rseq.n = n-root (||.seq.n.||) by A1;
hence Rseq.n = n-root (||.seq.||.n) by BHSP_2:def 3;
end;
hence thesis by A2,SERIES_1:28;
end;
theorem
(for n holds Rseq.n = n-root (||.seq.||.n)) & (ex m st for n st n >= m
holds Rseq.n >= 1) implies not seq is summable
proof
assume
A1: for n holds Rseq.n = n-root (||.seq.||.n);
given m such that
A2: for n st n >= m holds Rseq.n >= 1;
now
let n;
assume
A3: n >= m+1;
m + 1 >= 1 by NAT_1:11;
then
A4: n >= 1 by A3,XXREAL_0:2;
m+1 >= m by NAT_1:11;
then
A5: n>=m by A3,XXREAL_0:2;
Rseq.n = n-root (||.seq.||.n) by A1
.= n-root ||.seq.n.|| by BHSP_2:def 3;
then ||.seq.n.|| >= 0 & n-root ||.seq.n.|| |^ n >= 1 by A2,A5,BHSP_1:28
,PREPOWER:11;
hence ||.seq.n.|| >= 1 by A4,POWER:4;
end;
then not seq is convergent or lim seq <> 09(X) by Th29;
hence thesis by Th9;
end;
theorem
(for n holds Rseq.n = n-root (||.seq.||.n)) & Rseq is convergent & lim
Rseq > 1 implies not seq is summable
proof
assume that
A1: for n holds Rseq.n = n-root (||.seq.||.n) and
A2: Rseq is convergent and
A3: lim Rseq > 1;
lim Rseq - 1 > 0 by A3,XREAL_1:50;
then consider m being Nat such that
A4: for n being Nat st n >= m
holds |.Rseq.n - lim Rseq.| < lim Rseq - 1 by A2,
SEQ_2:def 7;
now
let n;
assume
A5: n >= m + 1;
A6: Rseq.n = n-root (||.seq.||.n) by A1
.= n-root ||.seq.n.|| by BHSP_2:def 3;
m + 1 >= m by NAT_1:11;
then n >= m by A5,XXREAL_0:2;
then |.n-root ||.seq.n.|| - lim Rseq.| < lim Rseq - 1 by A4,A6;
then - (lim Rseq - 1) < n-root ||.seq.n.|| - lim Rseq by SEQ_2:1;
then
1 - lim Rseq + lim Rseq < n-root ||.seq.n.|| - lim Rseq + lim Rseq by
XREAL_1:6;
then
A7: ||.seq.n.|| >= 0 & n-root ||.seq.n.|| |^ n >= 1 by BHSP_1:28,PREPOWER:11;
m + 1 >= 1 by NAT_1:11;
then n >= 1 by A5,XXREAL_0:2;
hence ||.seq.n.|| >= 1 by A7,POWER:4;
end;
then not seq is convergent or lim seq <> 09(X) by Th29;
hence thesis by Th9;
end;
theorem Th35:
Partial_Sums(||.seq.||) is non-decreasing
proof
now
let n be Nat;
||.seq.(n+1).|| >= 0 by BHSP_1:28;
then ||.seq.||.(n+1) >= 0 by BHSP_2:def 3;
then
0 + Partial_Sums(||.seq.||).n <= ||.seq.||.(n+1) + Partial_Sums(||.seq
.||).n by XREAL_1:6;
hence Partial_Sums(||.seq.||).n <= Partial_Sums(||.seq.||).(n+1) by
SERIES_1:def 1;
end;
hence thesis;
end;
theorem
for n holds Partial_Sums(||.seq.||).n >= 0
proof
let n;
||.(seq.0).|| >= 0 by BHSP_1:28;
then
A1: ||.seq.||.0 >= 0 by BHSP_2:def 3;
Partial_Sums(||.seq.||).0 <= Partial_Sums(||.seq.||).n by Th35,SEQM_3:11;
hence thesis by A1,SERIES_1:def 1;
end;
theorem Th37:
for n holds ||.Partial_Sums(seq).n.|| <= Partial_Sums(||.seq.||) .n
proof
defpred P[Nat] means
||.Partial_Sums(seq).$1.|| <= Partial_Sums(
||.seq.||).$1;
A1: now
let n;
assume P[n];
then
A2: ||.Partial_Sums(seq).n.|| + ||.seq.(n+1).|| <= Partial_Sums(||.seq.||)
.n + ||.seq.(n+1).|| by XREAL_1:6;
Partial_Sums(seq).(n+1) = Partial_Sums(seq).n + seq.(n+1) by Def1;
then
||.Partial_Sums(seq).(n+1).|| <= ||.Partial_Sums(seq).n.|| + ||.seq.(n
+1).|| by BHSP_1:30;
then
||.Partial_Sums(seq).(n+1).|| <= Partial_Sums(||.seq.||).n + ||.seq.(n
+1).|| by A2,XXREAL_0:2;
then
||.Partial_Sums(seq).(n+1).|| <= Partial_Sums(||.seq.||).n + ||.seq.||
.(n+1) by BHSP_2:def 3;
hence P[n+1] by SERIES_1:def 1;
end;
Partial_Sums(||.seq.||).0 = ||.seq.||.0 by SERIES_1:def 1
.= ||.(seq.0).|| by BHSP_2:def 3;
then
A3: P[0] by Def1;
thus for n holds P[n] from NAT_1:sch 2(A3,A1);
end;
theorem
for n holds ||.Sum(seq, n).|| <= Sum(||.seq.||, n) by Th37;
theorem Th39:
for n, m holds ||.Partial_Sums(seq).m - Partial_Sums(seq).n.||
<= |.Partial_Sums(||.seq.||).m - Partial_Sums(||.seq.||).n.|
proof
let n, m;
A1: now
reconsider d = n, t = m as Integer;
set PSseq9 = Partial_Sums(||.seq.||);
set PSseq = Partial_Sums(seq);
defpred P[Nat] means
||.PSseq.m - PSseq.(m+$1).|| <= |.PSseq9
.m - PSseq9.(m+$1).|;
A2: PSseq9 is non-decreasing by Th35;
A3: now
let k;
A4: ||.seq.(m+k+1).|| >= 0 by BHSP_1:28;
A5: |.PSseq9.m - PSseq9.(m+(k+1)).| = |.-(PSseq9.(m+(k+1)) - PSseq9. m).|
.= |.PSseq9.(m+k+1) - PSseq9.m.| by COMPLEX1:52
.= |.PSseq9.(m+k) + (||.seq.||).(m+k+1) - PSseq9.m.| by SERIES_1:def 1
.= |.||.seq.(m+k+1).|| + PSseq9.(m+k) - PSseq9.m.| by BHSP_2:def 3
.= |.(PSseq9.(m+k) - PSseq9.m) + ||.seq.(m+k+1).||.|;
||.PSseq.m - PSseq.(m+(k+1)).|| = ||.PSseq.m - (PSseq.(m+k) + seq.(
m + k +1)).|| by Def1
.= ||.(PSseq.m - PSseq.(m+k)) - seq.(m+k+1).|| by RLVECT_1:27
.= ||.(PSseq.m - PSseq.(m+k)) + -seq.(m+k+1).||;
then ||.PSseq.m - PSseq.(m+(k+1)).|| <= ||.PSseq.m - PSseq.(m+k).|| +
||.-seq.(m+k+1).|| by BHSP_1:30;
then
A6: ||.PSseq.m - PSseq.(m+(k+1)).|| <= ||.PSseq.m - PSseq.(m+k).|| +
||.seq.(m+k+1).|| by BHSP_1:31;
A7: PSseq9.(m+k) - PSseq9.m >= 0 by A2,SEQM_3:5,XREAL_1:48;
assume P[k];
then ||.PSseq.m - PSseq.(m+k).|| + ||.seq.(m+k+1).|| <= |.PSseq9.m -
PSseq9.(m+k).| + ||.seq.(m+k+1).|| by XREAL_1:6;
then ||.PSseq.m - PSseq.(m+(k+1)).|| <= |.-(PSseq9.(m+k) - PSseq9.m).|
+ ||.seq.(m+k+1).|| by A6,XXREAL_0:2;
then ||.PSseq.m - PSseq.(m+(k+1)).|| <= |.PSseq9.(m+k) - PSseq9.m.| +
||.seq.(m+k+1).|| by COMPLEX1:52;
then ||.PSseq.m - PSseq.(m+(k+1)).|| <= (PSseq9.(m+k) - PSseq9.m) + ||.
seq.(m+k+1).|| by A7,ABSVALUE:def 1;
hence P[k+1] by A7,A4,A5,ABSVALUE:def 1;
end;
assume n >= m;
then reconsider k = d - t as Element of NAT by INT_1:5;
A8: m + k = n;
||.PSseq.m - PSseq.(m+0).|| = ||.09(X).|| by RLVECT_1:15
.= 0 by BHSP_1:26;
then
A9: P[0] by COMPLEX1:46;
for k holds P[k] from NAT_1:sch 2(A9,A3);
hence thesis by A8;
end;
now
reconsider d = n, t = m as Integer;
set PSseq9 = Partial_Sums(||.seq.||);
set PSseq = Partial_Sums(seq);
defpred P[Nat] means
||.PSseq.(n+$1) - PSseq.n.|| <= |.PSseq9
.(n+$1) - PSseq9.n.|;
A10: PSseq9 is non-decreasing by Th35;
A11: now
let k;
A12: ||.seq.(n+k+1).|| >= 0 by BHSP_1:28;
A13: |.PSseq9.(n+(k+1)) - PSseq9.n.| = |.PSseq9.(n+k) + (||.seq.||).(
n+k +1) - PSseq9.n.| by SERIES_1:def 1
.= |.||.seq.(n+k+1).|| + PSseq9.(n+k) - PSseq9.n.| by BHSP_2:def 3
.= |.||.seq.(n+k+1).|| + (PSseq9.(n+k) - PSseq9.n).|;
assume P[k];
then
A14: ||.seq.(n+k+1).|| + ||.PSseq.(n+k) - PSseq.n.|| <= ||.seq.(n+k+1)
.|| + |.PSseq9.(n+k) - PSseq9.n.| by XREAL_1:7;
A15: PSseq9.(n+k) - PSseq9.n >= 0 by A10,SEQM_3:5,XREAL_1:48;
||.PSseq.(n+(k+1)) - PSseq.n.|| = ||.seq.(n+k+1) + PSseq.(n+k) -
PSseq .n.|| by Def1
.= ||.seq.(n+k+1) + (PSseq.(n+k) - PSseq.n).|| by RLVECT_1:def 3;
then
||.PSseq.(n+(k+1)) - PSseq.n.|| <= ||.seq.(n+k+1).|| + ||.PSseq.(n+k
) - PSseq.n.|| by BHSP_1:30;
then
||.PSseq.(n+(k+1)) - PSseq.n.|| <= ||.seq.(n+k+1).|| + |.PSseq9.(
n+k)-PSseq9.n.| by A14,XXREAL_0:2;
then
||.PSseq.(n+(k+1)) - PSseq.n.|| <= ||.seq.(n+k+1).|| + (PSseq9.(n+k
)-PSseq9.n) by A15,ABSVALUE:def 1;
hence P[k+1] by A15,A12,A13,ABSVALUE:def 1;
end;
assume n <= m;
then reconsider k = t - d as Element of NAT by INT_1:5;
A16: n + k = m;
||.PSseq.(n+0) - PSseq.n.|| = ||.09(X).|| by RLVECT_1:15
.= 0 by BHSP_1:26;
then
A17: P[0] by COMPLEX1:46;
for k holds P[k] from NAT_1:sch 2(A17,A11);
hence thesis by A16;
end;
hence thesis by A1;
end;
theorem
for n, m holds ||.Sum(seq, m) - Sum(seq, n).|| <= |.Sum(||.seq.||, m
) - Sum(||.seq.||, n).| by Th39;
theorem
for n, m holds ||.Sum(seq, m, n).|| <= |.Sum(||.seq.||, m, n).| by Th39;
theorem
for X being RealHilbertSpace, seq being sequence of X
holds seq is absolutely_summable implies seq is
summable
proof
let X be RealHilbertSpace, seq be sequence of X;
assume that
A1: seq is absolutely_summable;
A2: ||.seq.|| is summable by A1;
now
let r;
assume r > 0;
then consider k being Nat such that
A3: for m being Nat
st m >= k holds |.Partial_Sums(||.seq.||).m - Partial_Sums
(||.seq.||).k.| < r/2 by A2,SERIES_1:21,XREAL_1:215;
reconsider k as Nat;
take k;
now
let m, n;
A4: ||.Partial_Sums(seq).n - Partial_Sums(seq).m.|| <= |.Partial_Sums
(||.seq.||).n - Partial_Sums(||.seq.||).m.| by Th39;
assume m >= k & n >= k;
then
|.Partial_Sums(||.seq.||).m - Partial_Sums(||.seq.||).k.| < r /2 &
|. Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.|| ).k.| < r/2 by A3;
then
A5: |.Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).k.| + |.
Partial_Sums(||.seq.||).m - Partial_Sums(||.seq.||).k.| < r/2 + r/2 by
XREAL_1:8;
|.Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).m.| = |.(
Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).k) - (Partial_Sums(||.seq
.||).m - Partial_Sums(||.seq.|| ).k).|;
then |.Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).m.| <= |.
Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).k.| + |.Partial_Sums(||.
seq.||).m - Partial_Sums(||.seq.||).k.| by COMPLEX1:57;
then |.Partial_Sums(||.seq.||).n - Partial_Sums(||.seq.||).m.| < r by A5
,XXREAL_0:2;
hence ||.Partial_Sums(seq).n - Partial_Sums(seq).m.|| < r by A4,
XXREAL_0:2;
end;
hence for n, m st n >= k & m >= k holds ||.Partial_Sums(seq).n -
Partial_Sums(seq).m.|| < r;
end;
hence thesis by Th10;
end;
definition
let X, seq, Rseq;
func Rseq * seq -> sequence of X means
:Def7:
for n holds it.n = Rseq.n * seq.n;
existence
proof
deffunc F(Nat) = Rseq.$1 * seq.$1;
consider M being sequence of X such that
A1: for n being Element of NAT holds M.n = F(n) from FUNCT_2:sch 4;
take M;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let seq1, seq2;
assume that
A2: for n holds seq1.n = Rseq.n * seq.n and
A3: for n holds seq2.n = Rseq.n * seq.n;
let n be Element of NAT;
seq1.n = Rseq.n * seq.n by A2;
hence seq1.n = seq2.n by A3;
end;
end;
theorem
Rseq * (seq1 + seq2) = Rseq * seq1 + Rseq * seq2
proof
let n be Element of NAT;
thus (Rseq * (seq1 + seq2)).n = Rseq.n * (seq1 + seq2).n by Def7
.= Rseq.n * (seq1.n + seq2.n) by NORMSP_1:def 2
.= Rseq.n * seq1.n + Rseq.n * seq2.n by RLVECT_1:def 5
.= (Rseq * seq1).n + Rseq.n * seq2.n by Def7
.= (Rseq * seq1).n + (Rseq * seq2).n by Def7
.= (Rseq * seq1 + Rseq * seq2).n by NORMSP_1:def 2;
end;
theorem
(Rseq1 + Rseq2) * seq = Rseq1 * seq + Rseq2 * seq
proof
let n be Element of NAT;
thus ((Rseq1 + Rseq2) * seq).n = (Rseq1 + Rseq2).n * seq.n by Def7
.= (Rseq1.n + Rseq2.n) * seq.n by SEQ_1:7
.= Rseq1.n * seq.n + Rseq2.n * seq.n by RLVECT_1:def 6
.= (Rseq1 * seq).n + Rseq2.n * seq.n by Def7
.= (Rseq1 * seq).n + (Rseq2 * seq).n by Def7
.= (Rseq1 * seq + Rseq2 * seq).n by NORMSP_1:def 2;
end;
theorem
(Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)
proof
let n be Element of NAT;
thus ((Rseq1 (#) Rseq2) * seq).n = (Rseq1 (#) Rseq2).n * seq.n by Def7
.= (Rseq1.n * Rseq2.n) * seq.n by SEQ_1:8
.= Rseq1.n * (Rseq2.n * seq.n) by RLVECT_1:def 7
.= Rseq1.n * (Rseq2 * seq).n by Def7
.= (Rseq1 * (Rseq2 * seq)).n by Def7;
end;
theorem Th46:
(a (#) Rseq) * seq = a * (Rseq * seq)
proof
let n be Element of NAT;
thus ((a (#) Rseq) * seq).n = (a (#) Rseq).n * seq.n by Def7
.= (a * Rseq.n) * seq.n by SEQ_1:9
.= a * (Rseq.n * seq.n) by RLVECT_1:def 7
.= a * (Rseq * seq).n by Def7
.= (a * (Rseq * seq)).n by NORMSP_1:def 5;
end;
theorem
Rseq * (- seq) = (- Rseq) * seq
proof
let n be Element of NAT;
thus (Rseq * (- seq)).n = Rseq.n * (-seq).n by Def7
.= Rseq.n * (-(seq.n)) by BHSP_1:44
.= (-(Rseq.n)) * seq.n by RLVECT_1:24
.= (- Rseq).n * seq.n by SEQ_1:10
.= ((- Rseq) * seq).n by Def7;
end;
theorem Th48:
Rseq is convergent & seq is convergent implies Rseq * seq is convergent
proof
assume that
A1: Rseq is convergent and
A2: seq is convergent;
consider p being Real such that
A3: for r being Real st r > 0
ex m being Nat st for n being Nat st n >= m holds |.
Rseq.n - p.| < r by A1,SEQ_2:def 6;
consider g such that
A4: for r st r > 0
ex m being Nat st
for n being Nat st n >= m holds ||.seq.n - g.|| < r by A2,
BHSP_2:9;
reconsider p as Real;
now
take h = p * g;
let r;
consider b being Real such that
A5: b > 0 and
A6: for n being Nat holds |.Rseq.n.| < b by A1,SEQ_2:3,13;
reconsider b as Real;
A7: b + ||.g.|| > 0 + 0 by A5,BHSP_1:28,XREAL_1:8;
assume
A8: r > 0;
then consider m1 being Nat such that
A9: for n being Nat st n >= m1
holds |.Rseq.n - p.| < r/(b + ||.g.||) by A3,A7,
XREAL_1:139;
consider m2 being Nat such that
A10: for n being Nat
st n >= m2 holds ||.seq.n - g.|| < r/(b + ||.g.||) by A4,A7,A8,
XREAL_1:139;
reconsider m = m1 + m2 as Nat;
take m;
let n be Nat such that
A11: n >= m;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A11,XXREAL_0:2;
then ||.g.|| >= 0 & |.Rseq.n - p.| <= r/(b + ||.g.||) by A9,BHSP_1:28;
then
A12: ||.g.|| * |.Rseq.n - p.| <= ||.g.|| * (r/(b + ||.g.||)) by XREAL_1:64;
A13: |.Rseq.n.| >= 0 & ||.seq.n - g.|| >= 0 by BHSP_1:28,COMPLEX1:46;
m >= m2 by NAT_1:12;
then n >= m2 by A11,XXREAL_0:2;
then
A14: ||.seq.n - g.|| < r/(b + ||.g.||) by A10;
|.Rseq.n.| < b by A6;
then |.Rseq.n.| * ||.seq.n - g.|| < b * (r/(b + ||.g.||)) by A14,A13,
XREAL_1:96;
then
|.Rseq.n.| * ||.seq.n - g.|| + ||.g.|| * |.Rseq.n - p.| < b * (r/(b
+ ||.g.||)) + ||.g.|| * (r/(b + ||.g.||)) by A12,XREAL_1:8;
then
|.Rseq.n.| * ||.seq.n - g.|| + ||.g.|| * |.Rseq.n - p.| < (b * r)/(
b + ||.g.||) + ||.g.|| * (r/(b + ||.g.||)) by XCMPLX_1:74;
then
|.Rseq.n.| * ||.seq.n - g.|| + ||.g.|| * |.Rseq.n - p.| < (b * r)/(
b + ||.g.||) + (||.g.|| * r)/(b + ||.g.||) by XCMPLX_1:74;
then |.Rseq.n.| * ||.seq.n - g.|| + ||.g.|| * |.Rseq.n - p.| < (b * r +
||.g.|| * r)/(b + ||.g.||) by XCMPLX_1:62;
then
|.Rseq.n.| * ||.seq.n - g.|| + ||.g.|| * |.Rseq.n - p.| < ((b + ||.
g.||) * r)/(b + ||.g.||);
then
A15: |.Rseq.n.| * ||.seq.n - g.|| + ||.g.|| * |.Rseq.n - p.| < r by A7,
XCMPLX_1:89;
||.(Rseq * seq).n - p * g.|| = ||.Rseq.n * seq.n - p * g.|| by Def7
.= ||.(Rseq.n * seq.n - p * g) + 09(X).||
.= ||.(Rseq.n * seq.n - p * g) + (Rseq.n * g - Rseq.n * g).|| by
RLVECT_1:15
.= ||.Rseq.n * seq.n - (p * g - (Rseq.n * g - Rseq.n * g)).|| by
RLVECT_1:29
.= ||.Rseq.n * seq.n - (Rseq.n * g + (p * g - Rseq.n * g)).|| by
RLVECT_1:29
.= ||.(Rseq.n * seq.n - Rseq.n * g) - (p * g - Rseq.n * g).|| by
RLVECT_1:27
.= ||.(Rseq.n * seq.n - Rseq.n * g) + (Rseq.n * g - p * g).|| by
RLVECT_1:33;
then ||.(Rseq * seq).n - p * g.|| <= ||.Rseq.n * seq.n - Rseq.n * g.|| +
||.Rseq.n * g - p * g.|| by BHSP_1:30;
then
||.(Rseq * seq).n - p * g.|| <= ||.Rseq.n * (seq.n - g).|| + ||.Rseq.
n * g - p * g.|| by RLVECT_1:34;
then
||.(Rseq * seq).n - p * g.|| <= ||.Rseq.n * (seq.n - g).|| + ||.(Rseq
.n - p) * g.|| by RLVECT_1:35;
then ||.(Rseq * seq).n - p * g.|| <= |.Rseq.n.| * ||.seq.n - g.|| + ||.(
Rseq.n - p) * g.|| by BHSP_1:27;
then ||.(Rseq * seq).n - p * g.|| <= |.Rseq.n.| * ||.seq.n - g.|| + ||.g
.|| * |.Rseq.n - p.| by BHSP_1:27;
hence ||.(Rseq * seq).n - h.|| < r by A15,XXREAL_0:2;
end;
hence thesis by BHSP_2:9;
end;
theorem
Rseq is bounded & seq is bounded implies Rseq * seq is bounded
proof
assume that
A1: Rseq is bounded and
A2: seq is bounded;
consider M1 being Real such that
A3: M1 > 0 and
A4: for n being Nat holds |.Rseq.n.| < M1 by A1,SEQ_2:3;
consider M2 such that
A5: M2 > 0 and
A6: for n holds ||.seq.n.|| <= M2 by A2,BHSP_3:def 3;
now
reconsider M = M1 * M2 as Real;
take M;
now
let n;
|.Rseq.n.| >= 0 by COMPLEX1:46;
then
A7: |.Rseq.n.| * ||.seq.n.|| <= |.Rseq.n.| * M2 by A6,XREAL_1:64;
|.Rseq.n.| <= M1 by A4;
then
A8: |.Rseq.n.| * M2 <= M1 * M2 by A5,XREAL_1:64;
||.(Rseq * seq).n.|| = ||.Rseq.n * seq.n.|| by Def7
.= |.Rseq.n.| * ||.seq.n.|| by BHSP_1:27;
hence ||.(Rseq * seq).n.|| <= M by A7,A8,XXREAL_0:2;
end;
hence M > 0 & for n holds ||.(Rseq * seq).n.|| <= M by A3,A5,XREAL_1:129;
end;
hence thesis by BHSP_3:def 3;
end;
theorem
Rseq is convergent & seq is convergent implies Rseq * seq is
convergent & lim (Rseq * seq) = lim Rseq * lim seq
proof
assume that
A1: Rseq is convergent and
A2: seq is convergent;
consider b being Real such that
A3: b > 0 and
A4: for n being Nat holds |.Rseq.n.| < b by A1,SEQ_2:3,13;
reconsider b as Real;
A5: b + ||.lim seq.|| > 0 + 0 by A3,BHSP_1:28,XREAL_1:8;
A6: ||.lim seq.|| >= 0 by BHSP_1:28;
A7: now
let r;
assume r > 0;
then
A8: r/(b + ||.lim seq.||) > 0 by A5,XREAL_1:139;
then consider m1 being Nat such that
A9: for n being Nat st n >= m1
holds |.Rseq.n - lim Rseq.| < r/(b + ||.lim seq
.||) by A1,SEQ_2:def 7;
consider m2 being Nat such that
A10: for n being Nat
st n >= m2 holds dist(seq.n, lim seq) < r/(b + ||.lim seq
.||) by A2,A8,BHSP_2:def 2;
take m = m1 + m2;
let n be Nat such that
A11: n >= m;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A11,XXREAL_0:2;
then |.Rseq.n - lim Rseq.| <= r/(b + ||.lim seq.||) by A9;
then
A12: ||.lim seq.|| * |.Rseq.n - lim Rseq.| <= ||.lim seq.|| * (r/(b + ||.
lim seq.||)) by A6,XREAL_1:64;
A13: ||.seq.n - lim seq.|| >= 0 by BHSP_1:28;
m >= m2 by NAT_1:12;
then n >= m2 by A11,XXREAL_0:2;
then dist(seq.n, lim seq) < r/(b + ||.lim seq.||) by A10;
then
A14: ||.seq.n - lim seq.|| < r/(b + ||.lim seq.||) by BHSP_1:def 5;
|.Rseq.n.| < b & |.Rseq.n.| >= 0 by A4,COMPLEX1:46;
then |.Rseq.n.| * ||.seq.n - lim seq.|| < b * (r/(b + ||.lim seq.||)) by
A14,A13,XREAL_1:96;
then |.Rseq.n.| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.Rseq.n -
lim Rseq.| <
b * (r/(b + ||.lim seq.||)) + ||.lim seq.|| * (r/(b + ||.lim seq.||
)) by A12,XREAL_1:8;
then |.Rseq.n.| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.Rseq.n -
lim Rseq.| <
(b * r)/(b + ||.lim seq.||) + ||.lim seq.|| * (r/(b + ||.lim seq.||
)) by XCMPLX_1:74;
then |.Rseq.n.| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.Rseq.n -
lim Rseq.| < (b * r)/(b + ||.lim seq.||) + (||.lim seq.|| * r)/(b + ||.lim seq
.||) by XCMPLX_1:74;
then |.Rseq.n.| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.Rseq.n -
lim Rseq.| <
(b * r + ||.lim seq.|| * r)/(b + ||.lim seq.||) by XCMPLX_1:62;
then |.Rseq.n.| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.Rseq.n -
lim Rseq.| < ((b + ||.lim seq.||) * r)/(b + ||.lim seq.||);
then
A15: |.Rseq.n.| * ||.seq.n - lim seq.|| + ||.lim seq.|| * |.Rseq.n -
lim Rseq.| < r by A5,XCMPLX_1:89;
||.(Rseq * seq).n - lim Rseq * lim seq.|| = ||.Rseq.n * seq.n - lim
Rseq * lim seq.|| by Def7
.= ||.(Rseq.n * seq.n - lim Rseq * lim seq) + 09(X).||
.= ||.(Rseq.n * seq.n - lim Rseq * lim seq) + (Rseq.n * lim seq - Rseq
.n * lim seq).|| by RLVECT_1:15
.= ||.Rseq.n * seq.n - (lim Rseq * lim seq - (Rseq.n * lim seq - Rseq.
n * lim seq)).|| by RLVECT_1:29
.= ||.Rseq.n * seq.n - (Rseq.n * lim seq + (lim Rseq * lim seq - Rseq.
n * lim seq)).|| by RLVECT_1:29
.= ||.(Rseq.n * seq.n - Rseq.n * lim seq) - (lim Rseq * lim seq - Rseq
.n * lim seq).|| by RLVECT_1:27
.= ||.(Rseq.n * seq.n - Rseq.n * lim seq) + (Rseq.n * lim seq - lim
Rseq * lim seq).|| by RLVECT_1:33;
then
||.(Rseq * seq).n - lim Rseq * lim seq.|| <= ||.Rseq.n * seq.n - Rseq
.n * lim seq.|| + ||.Rseq.n * lim seq - lim Rseq * lim seq.|| by BHSP_1:30;
then
||.(Rseq * seq).n - lim Rseq * lim seq.|| <= ||.Rseq.n * (seq.n - lim
seq).|| + ||.Rseq.n * lim seq - lim Rseq * lim seq.|| by RLVECT_1:34;
then
||.(Rseq * seq).n - lim Rseq * lim seq.|| <= ||.Rseq.n * (seq.n - lim
seq).|| + ||.(Rseq.n - lim Rseq) * lim seq.|| by RLVECT_1:35;
then
||.(Rseq * seq).n - lim Rseq * lim seq.|| <= |.Rseq.n.| * ||.seq.n -
lim seq.|| + ||.(Rseq.n - lim Rseq) * lim seq.|| by BHSP_1:27;
then
||.(Rseq * seq).n - lim Rseq * lim seq.|| <= |.Rseq.n.| * ||.seq.n -
lim seq.|| + ||.lim seq.|| * |.Rseq.n - lim Rseq.| by BHSP_1:27;
then ||.(Rseq * seq).n - lim Rseq * lim seq.|| < r by A15,XXREAL_0:2;
hence dist((Rseq * seq).n, (lim Rseq * lim seq)) < r by BHSP_1:def 5;
end;
Rseq * seq is convergent by A1,A2,Th48;
hence thesis by A7,BHSP_2:def 2;
end;
definition
let Rseq;
attr Rseq is Cauchy means
for r st r > 0 ex k st for n, m st n >= k
& m >= k holds |.(Rseq.n - Rseq.m).| < r;
end;
theorem
for X being RealHilbertSpace, seq being sequence of X
holds seq is Cauchy & Rseq is Cauchy implies Rseq *
seq is Cauchy
proof
let X be RealHilbertSpace, seq be sequence of X;
assume that
A1: seq is Cauchy and
A2: Rseq is Cauchy;
now
let r be Real;
assume
A3: r > 0;
consider k such that
A4: for n, m st n >= k & m >= k holds |.(Rseq.n - Rseq.m).| < r by A2,A3;
reconsider k as Nat;
take k;
let n be Nat;
thus n >= k implies |.(Rseq.n - Rseq.k).| < r by A4;
end;
then
A5: Rseq is convergent by SEQ_4:41;
Rseq * seq is convergent by A5,Th48,A1,BHSP_3:def 4;
hence thesis;
end;
theorem Th52:
for n holds Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n
= Partial_Sums(Rseq * seq).(n+1) - (Rseq * Partial_Sums(seq)).(n+1)
proof
defpred P[Nat] means
Partial_Sums((Rseq - Rseq^\1) * Partial_Sums
(seq)).$1 = Partial_Sums(Rseq * seq).($1+1) - (Rseq * Partial_Sums(seq)).($1+1)
;
A1: Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).0 = ((Rseq - Rseq^\1)
* Partial_Sums(seq)).0 by Def1
.= (Rseq - Rseq^\1).0 * Partial_Sums(seq).0 by Def7
.= (Rseq + -Rseq^\1).0 * seq.0 by Def1
.= (Rseq.0 + (-Rseq^\1).0) * seq.0 by SEQ_1:7
.= (Rseq.0 + -(Rseq^\1).0) * seq.0 by SEQ_1:10
.= (Rseq.0 - (Rseq^\1).0) * seq.0
.= (Rseq.0 - Rseq.(0+1)) * seq.0 by NAT_1:def 3
.= Rseq.0 * seq.0 - Rseq.1 * seq.0 by RLVECT_1:35;
A2: (Rseq * Partial_Sums(seq)).(0+1) = Rseq.(0+1) * Partial_Sums(seq).(0+1)
by Def7
.= Rseq.(0+1) * (Partial_Sums(seq).0 + seq.(0+1)) by Def1
.= Rseq.1 * (seq.0 + seq.1) by Def1
.= Rseq.1 * seq.0 + Rseq.1 * seq.1 by RLVECT_1:def 5;
A3: now
let n;
assume P[n];
then Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (Rseq *
Partial_Sums(seq)).(n+1) = Partial_Sums(Rseq * seq).(n+1) - ((Rseq *
Partial_Sums(seq)).(n+1) - (Rseq * Partial_Sums(seq)).(n+1)) by RLVECT_1:29;
then
A4: Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (Rseq *
Partial_Sums(seq)).(n+1) = Partial_Sums(Rseq * seq).(n+1) - 09(X) by
RLVECT_1:15;
Partial_Sums(Rseq * seq).((n+1)+1) = Partial_Sums(Rseq * seq).(n+1) +
(Rseq * seq).((n+1)+1) by Def1
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (Rseq *
Partial_Sums(seq)).(n+1) + (Rseq * seq).((n+1)+1) by A4
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + ((Rseq *
Partial_Sums(seq)).(n+1) + (Rseq * seq).((n+1)+1)) by RLVECT_1:def 3
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (Rseq.(n+1)
* Partial_Sums(seq).(n+1) + (Rseq * seq).((n+1)+1)) by Def7
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (((Rseq.(n+1
) - Rseq.((n+1)+1)) + Rseq.((n+1)+1)) * Partial_Sums(seq).(n+1) + Rseq.((n+1)+1
) * seq.((n+1)+1)) by Def7
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (((Rseq.(n+1
) - Rseq.((n+1)+1)) * Partial_Sums(seq).(n+1) + Rseq.((n+1)+1) * Partial_Sums(
seq).(n+1)) + Rseq.((n+1)+1) * seq.((n+1)+1)) by RLVECT_1:def 6
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (((Rseq.(n+1
) - (Rseq^\1).(n+1)) * Partial_Sums(seq).(n+1) + Rseq.((n+1)+1) * Partial_Sums(
seq).(n+1)) + Rseq.((n+1)+1) * seq.((n+1)+1)) by NAT_1:def 3
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (((Rseq.(n+1
) + -(Rseq^\1).(n+1)) * Partial_Sums(seq).(n+1) + Rseq.((n+1)+1) * Partial_Sums
(seq).(n+1)) + Rseq.((n+1)+1) * seq.((n+1)+1))
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (((Rseq.(n+1
) + (-Rseq^\1).(n+1)) * Partial_Sums(seq).(n+1) + Rseq.((n+1)+1) * Partial_Sums
(seq).(n+1)) + Rseq.((n+1)+1) * seq.((n+1)+1)) by SEQ_1:10
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (((Rseq - (
Rseq^\1)).(n+1) * Partial_Sums(seq).(n+1) + Rseq.((n+1)+1) * Partial_Sums(seq).
(n+1)) + Rseq.((n+1)+1) * seq.((n+1)+1)) by SEQ_1:7
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + ((Rseq - (
Rseq^\1)).(n+1) * Partial_Sums(seq).(n+1) + (Rseq.((n+1)+1) * Partial_Sums(seq)
.(n+1) + Rseq.((n+1)+1) * seq.((n+1)+1))) by RLVECT_1:def 3
.= (Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (Rseq - (
Rseq^\1)).(n+1) * Partial_Sums(seq).(n+1)) + (Rseq.((n+1)+1) * Partial_Sums(seq
).(n+1) + Rseq.((n+1)+1) * seq.((n+1)+1)) by RLVECT_1:def 3
.= (Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + ((Rseq -
Rseq^\1) * Partial_Sums(seq)).(n+1)) + (Rseq.((n+1)+1) * Partial_Sums(seq).(n+1
) + Rseq.((n+1)+1) * seq.((n+1)+1)) by Def7
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).(n+1) + (Rseq.((
n+1)+1) * Partial_Sums(seq).(n+1) + Rseq.((n+1)+1) * seq.((n+1)+1)) by Def1
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).(n+1) + (Rseq.((
n+1)+1) * (Partial_Sums(seq).(n+1) + seq.((n+1)+1))) by RLVECT_1:def 5
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).(n+1) + (Rseq.((
n+1)+1) * Partial_Sums(seq).((n+1)+1)) by Def1
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).(n+1) + (Rseq *
Partial_Sums(seq)).((n+1)+1) by Def7;
then
Partial_Sums(Rseq * seq).((n+1)+1) - (Rseq * Partial_Sums(seq)).((n+1
) +1) = Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).(n+1) + ((Rseq *
Partial_Sums(seq)).((n+1)+1) - (Rseq * Partial_Sums(seq)).((n+1)+1)) by
RLVECT_1:def 3;
then
Partial_Sums(Rseq * seq).((n+1)+1) - (Rseq * Partial_Sums(seq)).((n+1
) +1) = Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).(n+1) + 09(X)
by RLVECT_1:15;
hence P[n+1];
end;
Partial_Sums(Rseq * seq).(0+1) = Partial_Sums(Rseq * seq).0 + (Rseq *
seq).(0+1) by Def1
.= (Rseq * seq).0 + (Rseq * seq).1 by Def1
.= Rseq.0 * seq.0 + (Rseq * seq).1 by Def7
.= Rseq.0 * seq.0 + Rseq.1 * seq.1 by Def7;
then
Partial_Sums(Rseq * seq).(0+1) = (Rseq.0 * seq.0 + 09(X)) + Rseq.1 * seq
.1
.= (Rseq.0 * seq.0 + (Rseq.1 * seq.0 - Rseq.1 * seq.0)) + Rseq.1 * seq.1
by RLVECT_1:15
.= ((Rseq.0 * seq.0 + -(Rseq.1 * seq.0)) + Rseq.1 * seq.0) + Rseq.1 *
seq.1 by RLVECT_1:def 3
.= Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).0 + (Rseq *
Partial_Sums(seq)).(0+1) by A1,A2,RLVECT_1:def 3;
then Partial_Sums(Rseq * seq).(0+1) - (Rseq * Partial_Sums(seq)).(0+1) =
Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).0 + ((Rseq * Partial_Sums(
seq)).(0+1) - (Rseq * Partial_Sums(seq)).(0+1)) by RLVECT_1:def 3;
then Partial_Sums(Rseq * seq).(0+1) - (Rseq * Partial_Sums(seq)).(0+1) =
Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).0 + 09(X) by RLVECT_1:15;
then
A5: P[0];
thus for n holds P[n] from NAT_1:sch 2(A5,A3);
end;
theorem Th53:
for n holds Partial_Sums(Rseq * seq).(n+1) = (Rseq *
Partial_Sums(seq)).(n+1) - Partial_Sums((Rseq^\1 - Rseq) * Partial_Sums(seq)).n
proof
let n;
Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (Rseq *
Partial_Sums(seq)).(n+1) = (Partial_Sums(Rseq * seq).(n+1) - (Rseq *
Partial_Sums(seq)).(n+1)) + (Rseq * Partial_Sums(seq)).(n+1) by Th52;
then Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (Rseq *
Partial_Sums(seq)).(n+1) = Partial_Sums(Rseq * seq).(n+1) - ((Rseq *
Partial_Sums(seq)).(n+1) - (Rseq * Partial_Sums(seq)).(n+1)) by RLVECT_1:29;
then Partial_Sums((Rseq - Rseq^\1) * Partial_Sums(seq)).n + (Rseq *
Partial_Sums(seq)).(n+1) = Partial_Sums(Rseq * seq).(n+1) - 09(X) by
RLVECT_1:15;
then Partial_Sums(Rseq * seq).(n+1) = (Rseq * Partial_Sums(seq)).(n+1) +
Partial_Sums(((-1) (#) (Rseq^\1) - -Rseq) * Partial_Sums(seq)).n;
then Partial_Sums(Rseq * seq).(n+1) = (Rseq * Partial_Sums(seq)).(n+1) +
Partial_Sums(((-1) (#) (Rseq^\1 - Rseq)) * Partial_Sums(seq)).n by SEQ_1:24;
then Partial_Sums(Rseq * seq).(n+1) = (Rseq * Partial_Sums(seq)).(n+1) +
Partial_Sums((-1) * ((Rseq^\1 - Rseq) * Partial_Sums(seq))).n by Th46;
then
Partial_Sums(Rseq * seq).(n+1) = (Rseq * Partial_Sums(seq)).(n+1) + ((-1
) * Partial_Sums((Rseq^\1 - Rseq) * Partial_Sums(seq))).n by Th3;
then
Partial_Sums(Rseq * seq).(n+1) = (Rseq * Partial_Sums(seq)).(n+1) + (-1)
* Partial_Sums((Rseq^\1 - Rseq) * Partial_Sums(seq)).n by NORMSP_1:def 5;
hence thesis by RLVECT_1:16;
end;
theorem
for n holds Sum(Rseq * seq, n+1) = (Rseq * Partial_Sums(seq)).(n+1) -
Sum((Rseq^\1 - Rseq) * Partial_Sums(seq), n) by Th53;