:: On Some Properties of Real {H}ilbert Space, {I}
:: by Hiroshi Yamazaki , Yasumasa Suzuki , Takao Inou\'e and Yasunari Shidama
::
:: Received February 25, 2003
:: Copyright (c) 2003-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, BHSP_1, PRE_TOPC, SUBSET_1, ALGSTR_0, BINOP_1, SETWISEO,
FINSET_1, FINSEQ_1, STRUCT_0, FUNCT_1, RELAT_1, FINSOP_1, FUNCT_2,
TARSKI, BHSP_5, XBOOLE_0, ARYTM_3, REAL_1, XXREAL_0, CARD_1, NORMSP_1,
ARYTM_1, SEMI_AF1, SUPINF_2, HAHNBAN, COMPLEX1, BINOP_2, RLVECT_1,
BHSP_3, ZFMISC_1, NAT_1, SEQ_2, BHSP_6, RSSPACE2, FCONT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, FUNCT_2,
NAT_1, RELSET_1, FINSET_1, BINOP_2, PARTFUN1, STRUCT_0, ALGSTR_0,
NORMSP_0, PRE_TOPC, RLVECT_1, BHSP_1, BHSP_2, BHSP_3, BINOP_1, SETWISEO,
HAHNBAN, FINSEQ_1, RSSPACE2, FINSOP_1, BHSP_5;
constructors BINOP_1, SETWISEO, REAL_1, NAT_1, NAT_D, BINOP_2, FINSOP_1,
BHSP_2, BHSP_3, HAHNBAN, BHSP_5, SUPINF_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2,
FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, BINOP_2, MEMBERED, STRUCT_0,
CARD_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities ALGSTR_0;
theorems XBOOLE_0, XBOOLE_1, TARSKI, ABSVALUE, FINSEQ_1, INT_1, FINSEQ_4,
FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, VECTSP_1, SEQ_4, BHSP_1, BHSP_2,
BHSP_3, BHSP_5, HAHNBAN, FINSOP_1, FINSEQ_3, XCMPLX_0, XCMPLX_1, BINOP_2,
XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1;
schemes NAT_1, FUNCT_2;
begin :: Preliminaries
reserve X for RealUnitarySpace;
reserve x for Point of X;
reserve i, n for Nat;
definition
let X such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
let Y be finite Subset of X;
func setsum Y -> Element of X means
:Def1:
ex p being FinSequence of the
carrier of X st p is one-to-one & rng p = Y & it = (the addF of X) "**" p;
existence
proof
consider p being FinSequence such that
A2: rng p = Y and
A3: p is one-to-one by FINSEQ_4:58;
reconsider q = p as FinSequence of the carrier of X by A2,FINSEQ_1:def 4;
ex p being FinSequence of the carrier of X st p is one-to-one & rng p
= Y & (the addF of X) "**" q = (the addF of X) "**" p by A2,A3;
hence thesis;
end;
uniqueness
proof
let X1, X2 be Element of X such that
A4: ex p1 being FinSequence of the carrier of X st p1 is one-to-one &
rng p1 = Y & X1 = (the addF of X) "**" p1 and
A5: ex p2 being FinSequence of the carrier of X st p2 is one-to-one &
rng p2 = Y & X2 = (the addF of X) "**" p2;
consider p2 being FinSequence of the carrier of X such that
A6: p2 is one-to-one & rng p2 = Y and
A7: X2 = (the addF of X) "**" p2 by A5;
consider p1 being FinSequence of the carrier of X such that
A8: p1 is one-to-one & rng p1 = Y and
A9: X1 = (the addF of X) "**" p1 by A4;
ex P being Permutation of dom p1 st p2 = p1*P & dom P = dom p1 & rng
P = dom p1 by A8,A6,BHSP_5:1;
hence thesis by A1,A9,A7,FINSOP_1:7;
end;
end;
theorem Th1:
for X st the addF of X is commutative associative & the addF of X
is having_a_unity for Y be finite Subset of X for I be Function of the carrier
of X,the carrier of X st Y c= dom I & for x be set st x in dom I holds I.x = x
holds setsum(Y) = setopfunc(Y, the carrier of X, the carrier of X, I, the addF
of X)
proof
let X such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
let Y be finite Subset of X;
consider p being FinSequence of the carrier of X such that
A2: p is one-to-one and
A3: rng p = Y and
A4: setsum(Y) = (the addF of X) "**" p by A1,Def1;
let I be Function of the carrier of X,the carrier of X such that
A5: Y c= dom I and
A6: for x be set st x in dom I holds I.x = x;
now
let xd be object;
A7: xd in dom p implies p.xd in rng(p) by FUNCT_1:3;
xd in dom(Func_Seq(I,p)) iff xd in dom(I*p) by BHSP_5:def 4;
hence xd in dom(Func_Seq(I,p)) iff xd in dom p by A5,A3,A7,FUNCT_1:11;
end;
then
A8: dom Func_Seq(I,p)=dom p by TARSKI:2;
now
let s be object;
assume
A9: s in dom Func_Seq(I,p);
then reconsider i = s as Nat;
A10: p.i in rng(p) by A8,A9,FUNCT_1:3;
Func_Seq(I,p).s = (I*p).i by BHSP_5:def 4
.= I.(p.i) by A8,A9,FUNCT_1:13
.= p.i by A5,A6,A3,A10;
hence Func_Seq(I,p).s = p.s;
end;
then Func_Seq(I,p) =p by A8,FUNCT_1:2;
hence thesis by A1,A2,A3,A4,BHSP_5:def 5;
end;
theorem Th2:
for X st the addF of X is commutative associative & the addF of X
is having_a_unity for Y1, Y2 be finite Subset of X st Y1 misses Y2 for Z be
finite Subset of X st Z = Y1 \/ Y2 holds setsum(Z) = setsum(Y1) + setsum(Y2)
proof
let X such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
reconsider I = id the carrier of X as Function of the carrier of X, the
carrier of X;
let Y1, Y2 be finite Subset of X such that
A2: Y1 misses Y2;
A3: dom I = the carrier of X by FUNCT_2:def 1;
let Z be finite Subset of X;
assume Z = Y1 \/ Y2;
then
A4: setopfunc(Z,the carrier of X,the carrier of X,I,the addF of X) =
setopfunc(Y1,the carrier of X,the carrier of X,I,the addF of X) + setopfunc(Y2,
the carrier of X,the carrier of X,I,the addF of X) by A1,A2,A3,BHSP_5:14;
A5: for x be set st x in the carrier of X holds I.x = x by FUNCT_1:18;
then setsum(Y1) = setopfunc(Y1,the carrier of X,the carrier of X,I,the addF
of X) & setsum(Y2) = setopfunc(Y2,the carrier of X,the carrier of X,I,the addF
of X) by A1,A3,Th1;
hence thesis by A1,A5,A3,A4,Th1;
end;
begin :: Summability
definition
let X;
let Y be Subset of X;
attr Y is summable_set means
ex x st for e be Real st e > 0 ex Y0 be
finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X
st Y0 c= Y1 & Y1 c= Y holds ||.x-setsum(Y1).|| < e;
end;
definition
let X;
let Y be Subset of X;
assume
A1: Y is summable_set;
func sum Y -> Point of X means
for e be Real st e > 0 ex Y0 be finite Subset
of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 &
Y1 c= Y holds ||.it-setsum(Y1).|| < e;
existence by A1;
uniqueness
proof
let y1, y2 be Point of X such that
A2: for e1 be Real st e1 > 0 ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.
y1-setsum(Y1).|| < e1 and
A3: for e2 be Real st e2 > 0 ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.
y2-setsum(Y1).|| < e2;
A4: now
let e3 be Real such that
A5: e3 >0;
set e4 = e3/2;
consider Y01 be finite Subset of X such that
Y01 is non empty and
A6: Y01 c= Y and
A7: for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= Y holds ||.y1-
setsum(Y1).|| < e4 by A2,A5,XREAL_1:139;
consider Y02 be finite Subset of X such that
Y02 is non empty and
A8: Y02 c= Y and
A9: for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= Y holds ||.y2-
setsum(Y1).|| < e4 by A3,A5,XREAL_1:139;
set Y00 = Y01 \/ Y02;
A10: e3/2 + e3/2 = e3 & Y01 c= Y00 by XBOOLE_1:7;
A11: Y00 c= Y by A6,A8,XBOOLE_1:8;
then ||.y2-setsum(Y00).|| < e4 by A9,XBOOLE_1:7;
then ||.-(y2-setsum(Y00)).|| < e4 by BHSP_1:31;
then ||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).|| < e3 by A7,A11,A10,
XREAL_1:8;
then (||.y1-setsum(Y00) + -(y2-setsum(Y00)).||) + (||.y1-setsum(Y00).||
+ ||.-(y2-setsum(Y00)).||) < (||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).||) +
e3 by BHSP_1:30,XREAL_1:8;
then
A12: ||.y1-setsum(Y00) + -(y2-setsum(Y00)).|| + (||.y1-setsum(Y00).|| +
||.-(y2-setsum(Y00)).||) + - (||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).||) <
e3 + (||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).||) + - (||.y1-setsum(Y00).||
+ ||.-(y2-setsum(Y00)).||) by XREAL_1:8;
||.y1 - y2.|| = ||.(y1 - y2) + 0.X.|| by RLVECT_1:def 4
.= ||.(y1 - y2) + (setsum(Y00) - setsum(Y00)).|| by RLVECT_1:5
.= ||.((y1 - y2) + setsum(Y00)) - setsum(Y00).|| by RLVECT_1:def 3
.= ||.(y1 - (y2 - setsum(Y00))) - setsum(Y00).|| by RLVECT_1:29
.= ||.y1 - (setsum(Y00) + (y2 - setsum(Y00))).|| by RLVECT_1:27
.= ||.(y1 - setsum(Y00)) - (y2 - setsum(Y00)).|| by RLVECT_1:27
.= ||.(y1 - setsum(Y00)) + - (y2 - setsum(Y00)).||;
hence ||.y1 - y2.|| < e3 by A12;
end;
y1 = y2
proof
assume y1 <> y2;
then y1 - y2 <> 0.X by VECTSP_1:19;
then
A13: ||.y1 - y2.|| <> 0 by BHSP_1:26;
0 <= ||.y1 - y2.|| by BHSP_1:28;
hence contradiction by A4,A13;
end;
hence thesis;
end;
end;
definition
let X;
let L be linear-Functional of X;
attr L is Lipschitzian means
ex K be Real st K > 0 & for x holds |.L.x.| <= K * ||.x.||;
end;
definition
let X;
let Y be Subset of X;
attr Y is weakly_summable_set means
ex x st for L be
linear-Functional of X st L is Lipschitzian for e be Real st e > 0
ex Y0 be finite
Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0
c= Y1 & Y1 c= Y holds |.L.(x-setsum(Y1)).| < e;
end;
definition
let X;
let Y be Subset of X;
let L be Functional of X;
pred Y is_summable_set_by L means
ex r be Real st for e be Real st e
> 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite
Subset of X st Y0 c= Y1 & Y1 c= Y holds |.r-setopfunc(Y1,the carrier of X,
REAL, L, addreal).| < e;
end;
definition
let X;
let Y be Subset of X;
let L be Functional of X;
assume
A1: Y is_summable_set_by L;
func sum_byfunc(Y,L) -> Real means
for e be Real st e > 0 ex Y0 be finite
Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0
c= Y1 & Y1 c= Y holds |.it-setopfunc(Y1,the carrier of X,REAL, L, addreal).| <
e;
existence by A1;
uniqueness
proof
let r1, r2 be Real such that
A2: for e1 be Real st e1 > 0 ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |.
r1-setopfunc(Y1,the carrier of X,REAL, L, addreal).| < e1 and
A3: for e2 be Real st e2 > 0 ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |.
r2-setopfunc(Y1,the carrier of X,REAL, L, addreal).| < e2;
A4: now
let e3 be Real such that
A5: e3 >0;
set e4 = e3/2;
consider Y01 be finite Subset of X such that
Y01 is non empty and
A6: Y01 c= Y and
A7: for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= Y holds |.r1
- setopfunc(Y1,the carrier of X,REAL, L, addreal).| < e4 by A2,A5,XREAL_1:139;
consider Y02 be finite Subset of X such that
Y02 is non empty and
A8: Y02 c= Y and
A9: for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= Y holds |.r2
- setopfunc(Y1,the carrier of X,REAL, L, addreal).| < e4 by A3,A5,XREAL_1:139;
set Y00 = Y01 \/ Y02;
A10: e3/2 + e3/2 = e3 & Y01 c= Y00 by XBOOLE_1:7;
A11: Y00 c= Y by A6,A8,XBOOLE_1:8;
then
|.r2-setopfunc(Y00,the carrier of X,REAL, L, addreal).| < e4 by A9,
XBOOLE_1:7;
then |.(r1-setopfunc(Y00,the carrier of X,REAL, L, addreal)) - (r2-
setopfunc(Y00,the carrier of X,REAL, L, addreal)).| <= |.r1-setopfunc(Y00,the
carrier of X, REAL, L, addreal).| + |.r2-setopfunc(Y00,the carrier of X,REAL,
L, addreal).| & |.r1-setopfunc(Y00,the carrier of X,REAL, L, addreal).| + |.
r2-setopfunc( Y00,the carrier of X,REAL, L, addreal).| < e3
by A7,A11,A10,
COMPLEX1:57,XREAL_1:8;
hence |.r1-r2.| < e3 by XXREAL_0:2;
end;
r1 = r2
proof
assume
A12: r1 <> r2;
A13: |.r1-r2.| <> 0
proof
assume |.r1-r2.| = 0;
then r1-r2 = 0 by ABSVALUE:2;
hence contradiction by A12;
end;
0 <= |.r1-r2.| by COMPLEX1:46;
hence contradiction by A4,A13;
end;
hence thesis;
end;
end;
theorem Th3:
for Y be Subset of X st Y is summable_set holds Y is weakly_summable_set
proof
let Y be Subset of X;
assume Y is summable_set;
then consider x such that
A1: for e be Real st 0 < e ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x
- setsum(Y1).|| < e;
now
let L be linear-Functional of X;
assume L is Lipschitzian;
then consider K be Real such that
A2: 0 < K and
A3: for x holds |.L.x.| <= K * ||.x.||;
now
let e1 be Real such that
A4: 0 < e1;
set e = e1/K;
consider Y0 be finite Subset of X such that
A5: Y0 is non empty & Y0 c= Y and
A6: for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c=Y holds ||.x -
setsum(Y1).|| < e by A1,A2,A4,XREAL_1:139;
A7: e * K = e1 by A2,XCMPLX_1:87;
now
let Y1 be finite Subset of X;
assume Y0 c= Y1 & Y1 c=Y;
then K * ||.x - setsum(Y1).|| < e1 by A2,A7,A6,XREAL_1:68;
then
|.L.(x-setsum(Y1)).| + K*||.(x-setsum(Y1)).|| < K*||.(x-setsum(
Y1)).|| + e1 by A3,XREAL_1:8;
then
|.L.(x-setsum(Y1)).| + K*||.(x-setsum(Y1)).|| - K*||.(x-setsum(
Y1)).|| < K*||.(x-setsum(Y1)).|| + e1 - K*||.(x-setsum(Y1)).|| by XREAL_1:14;
hence |.L.(x-setsum(Y1)).| < e1;
end;
hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1
be finite Subset of X st Y0 c= Y1 & Y1 c=Y holds |.L.(x-setsum(Y1)).| < e1
by A5;
end;
hence for e1 be Real st 0 < e1
ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c=Y holds |.
L.(x-setsum(Y1)).| < e1;
end;
hence thesis;
end;
theorem Th4:
for L be linear-Functional of X for p be FinSequence of the
carrier of X st len p >=1 for q be FinSequence of REAL st dom p = dom q & (for
i st i in dom q holds q.i = L.(p.i) ) holds L.((the addF of X) "**" p) =
addreal "**" q
proof
let L be linear-Functional of X;
let p be FinSequence of the carrier of X such that
A1: len p >= 1;
consider f be sequence of the carrier of X such that
A2: f.1 = p.1 and
A3: for n be Nat st 0 <> n & n < len p holds f.(n + 1) = (the
addF of X).(f.n,p.(n + 1)) and
A4: (the addF of X) "**" p = f.(len p) by A1,FINSOP_1:1;
let q be FinSequence of REAL such that
A5: dom p = dom q and
A6: for i st i in dom q holds q.i = L.(p.i);
Seg (len q) = dom p by A5,FINSEQ_1:def 3
.= Seg (len p) by FINSEQ_1:def 3;
then
A7: len q = len p by FINSEQ_1:6;
then consider g be sequence of REAL such that
A8: g.1 = q.1 and
A9: for n be Nat st 0 <> n & n < len q holds g.(n + 1) =
addreal.(g.n,q.(n + 1)) and
A10: addreal "**" q = g.(len q) by A1,FINSOP_1:1;
defpred P[Nat] means 1 <= $1 & $1 <= len q implies g.$1 = L.(f.$1);
A11: now
let n;
A12: n in NAT by ORDINAL1:def 12;
assume
A13: P[n];
now
A14: n <= n+1 by NAT_1:11;
assume that
A15: 1 <=n+1 and
A16: n+1 <= len q;
per cases;
suppose
A17: n=0;
1 in dom p by A1,FINSEQ_3:25;
hence g.(n+1) = L.(f.(n+1)) by A5,A6,A2,A8,A17;
end;
suppose
A18: n<>0;
then
A19: 0+1 <= n by INT_1:7,A12;
reconsider z=f.n as Element of X;
reconsider z1=z as VECTOR of X;
A20: n+1 in dom q by A15,A16,FINSEQ_3:25;
then p.(n+1) in rng p by A5,FUNCT_1:3;
then reconsider y=p.(n+1) as Element of X;
reconsider y1=y as VECTOR of X;
set Lz=L.z1, Ly=L.y1;
A21: n+1-1 < len q-0 by A16,XREAL_1:15;
hence g.(n+1) = addreal.(g.n,q.(n + 1)) by A9,A18
.= addreal.(L.(f.n), L.y) by A6,A13,A16,A14,A19,A20,XXREAL_0:2
.= Lz + Ly by BINOP_2:def 9
.= L .(z1+y1) by HAHNBAN:def 2
.= L.(f.(n + 1)) by A3,A7,A18,A21;
end;
end;
hence P[n+1];
end;
A22: P[0];
for n holds P[n] from NAT_1:sch 2(A22,A11);
hence thesis by A1,A4,A7,A10;
end;
theorem Th5:
for X st the addF of X is commutative associative & the addF of X
is having_a_unity for S be finite Subset of X st S is non empty for L be
linear-Functional of X holds L.(setsum(S)) = setopfunc(S,the carrier of X,REAL,
L, addreal)
proof
let X such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
let S be finite Subset of X;
assume S is non empty;
then
A2: 0+1 <= card S by INT_1:7;
let L be linear-Functional of X;
consider p be FinSequence of the carrier of X such that
A3: p is one-to-one & rng p = S and
A4: setsum(S) = (the addF of X) "**" p by A1,Def1;
reconsider q1 = Func_Seq(L,p) as FinSequence of REAL;
A5: for i st i in dom p holds q1.i = L.(p.i)
proof
let i such that
A6: i in dom p;
q1.i = (L*p).i by BHSP_5:def 4
.= L.(p.i) by A6,FUNCT_1:13;
hence thesis;
end;
A7: dom L = the carrier of X by FUNCT_2:def 1;
now
let xd be object;
A8: xd in dom p implies p.xd in rng(p) by FUNCT_1:3;
xd in dom(Func_Seq(L,p)) iff xd in dom(L*p) by BHSP_5:def 4;
hence xd in dom(Func_Seq(L,p)) iff xd in dom p by A7,A8,FUNCT_1:11;
end;
then
A9: dom Func_Seq(L,p)=dom p by TARSKI:2;
len p >=1 by A3,A2,FINSEQ_4:62;
then L.((the addF of X) "**" p) = addreal "**" q1 by A9,A5,Th4;
hence thesis by A3,A4,BHSP_5:def 5;
end;
theorem Th6:
for X st the addF of X is commutative associative & the addF of X
is having_a_unity for Y be Subset of X holds Y is weakly_summable_set implies
ex x st for L be linear-Functional of X st L is Lipschitzian
for e be Real st
e > 0
ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite
Subset of X st Y0 c= Y1 & Y1 c= Y holds |.(L.x)-(setopfunc(Y1,the carrier of
X,REAL, L, addreal)).| < e
proof
let X such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
let Y be Subset of X;
assume Y is weakly_summable_set;
then consider x such that
A2: for L be linear-Functional of X st L is Lipschitzian
for e be Real st e >
0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite
Subset of X st Y0 c= Y1 & Y1 c= Y holds |.L.(x-setsum(Y1)).| < e;
take x;
now
let L be linear-Functional of X such that
A3: L is Lipschitzian;
now
let e be Real;
assume e > 0;
then consider Y0 be finite Subset of X such that
A4: Y0 is non empty and
A5: Y0 c= Y and
A6: for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |.L.
(x- setsum(Y1)).| < e by A2,A3;
take Y0;
now
set x1 = x;
let Y1 be finite Subset of X such that
A7: Y0 c= Y1 and
A8: Y1 c= Y;
set y1 = setsum(Y1);
set r = L.(x-setsum(Y1));
Y1 <> {} by A4,A7;
then r = L.x1 - L.y1 & L.y1=setopfunc(Y1,the carrier of X,REAL, L,
addreal) by A1,Th5,HAHNBAN:19;
hence |.(L.x)-(setopfunc(Y1,the carrier of X,REAL, L, addreal)).| < e
by A6,A7,A8;
end;
hence Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c=
Y1 & Y1 c= Y holds |.(L.x)-(setopfunc(Y1,the carrier of X,REAL, L, addreal)).|
< e by A4,A5;
end;
hence
for e be Real st e > 0
ex Y0 be finite Subset of X st Y0 is non empty
& Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |.(L.x)-
(setopfunc(Y1,the carrier of X,REAL, L, addreal)).| < e;
end;
hence thesis;
end;
theorem Th7:
for X st the addF of X is commutative associative & the addF of X
is having_a_unity for Y be Subset of X st Y is weakly_summable_set for L be
linear-Functional of X st L is Lipschitzian holds Y is_summable_set_by L
proof
let X such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
let Y be Subset of X;
assume Y is weakly_summable_set;
then consider x such that
A2: for L be linear-Functional of X st L is Lipschitzian
for e be Real st e >
0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite
Subset of X st Y0 c= Y1 & Y1 c= Y holds |.(L.x)-(setopfunc(Y1,the carrier of
X,REAL, L, addreal)).| < e by A1,Th6;
let L be linear-Functional of X;
assume L is Lipschitzian;
then
for e be Real st e > 0
ex Y0 be finite Subset of X st Y0 is non empty &
Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |.(L.x)-(
setopfunc(Y1,the carrier of X,REAL, L, addreal)).| < e by A2;
hence thesis;
end;
theorem
for X st the addF of X is commutative associative & the addF of X is
having_a_unity for Y be Subset of X st Y is summable_set for L be
linear-Functional of X st L is Lipschitzian holds Y is_summable_set_by L
by Th3,Th7;
theorem
for Y be finite Subset of X st Y is non empty holds Y is summable_set
proof
let Y be finite Subset of X such that
A1: Y is non empty;
set x = setsum Y;
now
let e be Real such that
A2: e >0;
ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be
finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x-setsum(Y1).|| < e
proof
take Y;
now
let Y1 be finite Subset of X;
assume Y c= Y1 & Y1 c= Y;
then Y1 = Y by XBOOLE_0:def 10;
then x - setsum(Y1) = 0.X by RLVECT_1:15;
hence ||.x-setsum(Y1).|| < e by A2,BHSP_1:26;
end;
hence thesis by A1;
end;
hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be
finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x-setsum(Y1).|| < e;
end;
hence thesis;
end;
begin :: Necessary and sufficient condition for summability
theorem
for X being RealHilbertSpace
st the addF of X is commutative associative & the addF of X is
having_a_unity for Y be Subset of X holds Y is summable_set iff
for e be Real st e > 0 holds ex Y0 be finite Subset of X st Y0 is non empty &
Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses
Y1 holds ||.setsum(Y1).|| < e
proof
let X be RealHilbertSpace such that
A1: the addF of X is commutative associative & the addF of X is having_a_unity;
let Y be Subset of X;
A2: now
defpred P[object,object] means
ex D2 being set st D2 = $2 &
( $2 is finite Subset of X & D2 is non empty & D2 c= Y &
for z be Real st z=$1 for Y1 be finite Subset of X st Y1 is non empty &
Y1 c= Y & D2 misses Y1 holds ||.setsum(Y1).|| < 1/(z+1));
assume
A3: for e be Real st e > 0 holds ex Y0 be finite Subset of X st Y0 is
non empty & Y0 c= Y &
for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y
& Y0 misses Y1 holds ||.setsum(Y1).|| < e;
A4: for x being object st x in NAT
ex y being object st y in bool Y & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider xx= x as Nat;
reconsider e = 1/(xx+1) as Real;
0/(xx + 1) < 1/(xx + 1) by XREAL_1:74;
then consider Y0 be finite Subset of X such that
A5: Y0 is non empty & Y0 c= Y and
A6: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0
misses Y1 holds ||.setsum(Y1).|| < e by A3;
reconsider Y0 as object;
take Y0;
thus Y0 in bool Y by A5;
take Y0;
thus thesis by A5,A6;
end;
consider B being sequence of bool Y such that
A7: for x be object st x in NAT holds P[x,B .x] from FUNCT_2:sch 1(A4);
ex A be sequence of bool Y st for i be Nat holds A.i
is finite Subset of X & A.i is non empty & A.i c= Y & (for Y1 be finite Subset
of X st Y1 is non empty & Y1 c= Y & A.i misses Y1 holds ||.setsum(Y1).|| < 1/(i
+1)) & for j be Nat st i <= j holds A.i c= A.j
proof
A8: for x be object st x in NAT holds B.x is finite Subset of X & B.x
is non empty & B.x c= Y & for z be Real st z=x for Y1 be finite Subset of X st
Y1 is non empty & Y1 c= Y & B.x misses Y1 holds ||.setsum(Y1).|| < 1/(z+1)
proof let x be object;
assume x in NAT;
then P[x,B.x] by A7;
hence thesis;
end;
deffunc G(Nat,set) = B.($1+1) \/ $2;
ex A being Function st dom A = NAT & A.0 = B.0 & for n being Nat
holds A.(n+1) = G(n,A.n) from NAT_1:sch 11;
then consider A being Function such that
A9: dom A = NAT and
A10: A.0 = B.0 and
A11: for n being Nat holds A.(n+1) = B.(n+1) \/ A.n;
defpred R[Nat] means A.$1 is finite Subset of X & A.$1 is non
empty & A.$1 c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y
& A.$1 misses Y1 holds ||.setsum(Y1).|| < 1/($1+1)) & for j be Nat
st $1 <= j holds A.$1 c= A.j;
A12: now
let n be Nat such that
A13: R[n];
A14: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & A.(n+
1) misses Y1 holds ||.setsum(Y1).|| < 1/((n+1)+1)
proof
let Y1 be finite Subset of X such that
A15: Y1 is non empty & Y1 c= Y and
A16: A.(n+1) misses Y1;
A.(n+1) = B.(n+1) \/ A.n by A11;
then B.(n+1) misses Y1 by A16,XBOOLE_1:7,63;
hence thesis by A8,A15;
end;
defpred P[Nat] means (n+1) <= $1 implies A.(n+1) c= A.$1;
A17: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat such that
A18: n+1 <= j implies A.(n+1) c= A.j and
A19: n+1 <= j+1;
per cases;
suppose
n = j;
hence thesis;
end;
suppose
A20: n <> j;
A.(j+1) = (B.(j+1) \/ A.j) by A11;
then
A21: A.j c= A.(j+1) by XBOOLE_1:7;
n <= j by A19,XREAL_1:6;
then n < j by A20,XXREAL_0:1;
hence thesis by A18,A21,NAT_1:13,XBOOLE_1:1;
end;
end;
A22: P[0];
A23: for j be Nat holds P[j] from NAT_1:sch 2(A22, A17);
A24: A.(n+1) = B.(n+1) \/ A.n & B.(n+1) is finite Subset of X by A8,A11;
thus R[n+1] by A13,A14,A23,XBOOLE_1:8,A24;
end;
for j0 be Nat st j0=0 holds for j be Nat st
j0 <= j holds A.j0 c= A.j
proof
let j0 be Nat such that
A25: j0 = 0;
defpred P[Nat] means (j0 <= $1 implies A.j0 c= A.$1);
A26: now
let j be Nat such that
A27: P[j];
A.(j+1) = (B.(j+1) \/ A.j) by A11;
then A.j c= A.(j+1) by XBOOLE_1:7;
hence P[j+1] by A25,A27,XBOOLE_1:1;
end;
A28: P[0];
thus for j be Nat holds P[j] from NAT_1:sch 2(A28, A26);
end;
then
A29: R[0] by A8,A10;
A30: for i be Nat holds R[i] from NAT_1:sch 2(A29,A12);
now
let y be object;
assume y in rng A;
then consider x be object such that
A31: x in dom A and
A32: y = A.x by FUNCT_1:def 3;
reconsider i = x as Nat by A9,A31;
A.i c= Y by A30;
hence y in bool Y by A32;
end;
then rng A c= bool Y by TARSKI:def 3;
then A is sequence of bool Y by A9,FUNCT_2:2;
hence thesis by A30;
end;
then consider A be sequence of bool Y such that
A33: for i be Nat holds A.i is finite Subset of X & A.i is
non empty & A.i c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c=
Y & A.i misses Y1 holds ||.setsum(Y1).|| < 1/(i+1)) & for j be Nat
st i <= j holds A.i c= A.j;
defpred P[object,object] means
ex Y1 be finite Subset of X st Y1 is non empty &
A.$1 = Y1 & $2=setsum(Y1);
A34: for x be object st x in NAT
ex y be object st y in the carrier of X & P[x,y ]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
A.i is finite Subset of X by A33;
then reconsider Y1 = A.x as finite Subset of X;
reconsider y = setsum(Y1) as set;
A.i is non empty by A33;
then
ex Y1 be finite Subset of X st Y1 is non empty set & A.x = Y1 & y =
setsum(Y1);
hence thesis;
end;
ex F being sequence of the carrier of X st for x be object st x in
NAT holds P[x,F.x] from FUNCT_2:sch 1(A34);
then consider F being sequence of the carrier of X such that
A35: for x be object st x in NAT holds ex Y1 be finite Subset of X st Y1
is non empty & A.x = Y1 & F.x = setsum(Y1);
reconsider seq = F as sequence of X;
now
let e be Real such that
A36: e > 0;
A37: e/2 > 0/2 by A36,XREAL_1:74;
ex k be Nat st 1/(k+1) < e/2
proof
set p = e/2;
consider k1 be Nat such that
A38: p"<k1 by SEQ_4:3;
take k = k1;
p"+0 < k1+1 by A38,XREAL_1:8;
then 1/(k1+1) < 1/p" by A37,XREAL_1:76;
then 1/(k+1) < 1 * p"" by XCMPLX_0:def 9;
hence thesis;
end;
then consider k be Nat such that
A39: 1/(k+1) < e/2;
now
let nn, mm be Nat such that
A40: nn >= k and
A41: mm >= k;
nn in NAT & mm in NAT & k in NAT by ORDINAL1:def 12;
then reconsider k,m=mm,n=nn as Element of NAT;
consider Y2 be finite Subset of X such that
Y2 is non empty and
A42: A.m = Y2 and
A43: seq.m = setsum(Y2) by A35;
consider Y0 be finite Subset of X such that
Y0 is non empty and
A44: A.k = Y0 and
A45: seq.k = setsum(Y0) by A35;
A46: Y0 c= Y2 by A33,A41,A44,A42;
consider Y1 be finite Subset of X such that
Y1 is non empty and
A47: A.n = Y1 and
A48: seq.n = setsum(Y1) by A35;
A49: Y0 c= Y1 by A33,A40,A44,A47;
now
per cases;
case
A50: Y0 = Y1;
now
per cases;
case
Y0 = Y2;
then (seq.n) - (seq.m) = 0.X by A48,A43,A50,RLVECT_1:5;
hence ||.(seq.n) - (seq.m).|| < e by A36,BHSP_1:26;
end;
case
A51: Y0 <> Y2;
ex Y02 be finite Subset of X st Y02 is non empty & Y02
c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2
proof
take Y02 = Y2 \ Y0;
A52: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
A53: Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A46,XBOOLE_1:12;
hence Y02 is non empty by A51;
thus Y02 c= Y by A42,A52,XBOOLE_1:1;
thus thesis by XBOOLE_1:79,A53;
end;
then consider Y02 be finite Subset of X such that
A54: Y02 is non empty & Y02 c= Y and
A55: Y02 misses Y0 and
A56: Y0 \/ Y02 = Y2;
||.setsum(Y02).|| < 1/(k+1) by A33,A44,A54,A55;
then
A57: ||.setsum(Y02).|| < e/2 by A39,XXREAL_0:2;
setsum(Y2) = setsum(Y0) + setsum(Y02) by A1,A55,A56,Th2;
then
A58: ||.(seq.n) - (seq.m).|| = ||.(setsum(Y0) - setsum(Y0)) -
setsum(Y02).|| by A48,A43,A50,RLVECT_1:27
.= ||.0.X - setsum(Y02).|| by RLVECT_1:15
.= ||. - setsum(Y02).|| by RLVECT_1:14
.= ||.setsum(Y02).|| by BHSP_1:31;
e*(1/2) < e*1 by A36,XREAL_1:68;
hence ||.(seq.n) - (seq.m).|| < e by A57,A58,XXREAL_0:2;
end;
end;
hence ||.(seq.n) - (seq.m).|| < e;
end;
case
A59: Y0 <> Y1;
now
per cases;
case
Y0 = Y2;
then
A60: seq.k - seq.m = 0.X by A45,A43,RLVECT_1:5;
ex Y01 be finite Subset of X st Y01 is non empty & Y01
c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1
proof
take Y01 = Y1 \ Y0;
A61: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A49,XBOOLE_1:12;
hence thesis by A47,A59,A61,XBOOLE_1:1,79;
end;
then consider Y01 be finite Subset of X such that
A62: Y01 is non empty & Y01 c= Y and
A63: Y01 misses Y0 and
A64: Y0 \/ Y01 = Y1;
seq.n = seq.k + setsum(Y01) by A1,A45,A48,A63,A64,Th2;
then
A65: seq.n - seq.k = seq.k + (setsum(Y01) +- seq.k) by
RLVECT_1:def 3
.= seq.k - (seq.k - setsum(Y01)) by RLVECT_1:33
.= (setsum(Y0) - setsum(Y0)) + setsum(Y01) by A45,RLVECT_1:29
.= 0.X + setsum(Y01) by RLVECT_1:5
.= setsum(Y01) by RLVECT_1:4;
seq.n - seq.m = seq.n - seq.m + 0.X by RLVECT_1:4
.= seq.n - seq.m + (seq.k - seq.k) by RLVECT_1:5
.= seq.n - (seq.m - (seq.k - seq.k)) by RLVECT_1:29
.= seq.n - ((seq.m - seq.k) + seq.k) by RLVECT_1:29
.= seq.n - (seq.k - (seq.k - seq.m)) by RLVECT_1:33
.= setsum(Y01) + 0.X by A65,A60,RLVECT_1:29;
then ||.(seq.n) - (seq.m).|| <= ||.setsum(Y01).|| + ||.0.X.||
by BHSP_1:30;
then
A66: ||.(seq.n) - (seq.m).|| <= ||.setsum( Y01).|| + 0 by BHSP_1:26;
||. setsum(Y01).|| < 1/(k+1) by A33,A44,A62,A63;
then ||. setsum(Y01).|| < e/2 by A39,XXREAL_0:2;
then ||.(seq.n) - (seq.m).|| < e/2 by A66,XXREAL_0:2;
then ||.(seq.n) - (seq.m).|| + 0 < e/2 + e/2 by A36,XREAL_1:8;
hence ||.(seq.n) - (seq.m).|| < e;
end;
case
A67: Y0<>Y2;
ex Y02 be finite Subset of X st Y02 is non empty & Y02
c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2
proof
take Y02 = Y2 \ Y0;
A68: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A46,XBOOLE_1:12;
hence thesis by A42,A67,A68,XBOOLE_1:1,79;
end;
then consider Y02 be finite Subset of X such that
A69: Y02 is non empty & Y02 c= Y and
A70: Y02 misses Y0 and
A71: Y0 \/ Y02 = Y2;
||.setsum(Y02).|| < 1/(k+1) by A33,A44,A69,A70;
then
A72: ||.setsum(Y02).|| < e/2 by A39,XXREAL_0:2;
ex Y01 be finite Subset of X st Y01 is non empty & Y01
c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1
proof
take Y01 = Y1 \ Y0;
A73: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A49,XBOOLE_1:12;
hence thesis by A47,A59,A73,XBOOLE_1:1,79;
end;
then consider Y01 be finite Subset of X such that
A74: Y01 is non empty & Y01 c= Y and
A75: Y01 misses Y0 and
A76: Y0 \/ Y01 = Y1;
setsum(Y1) = setsum(Y0) + setsum(Y01) by A1,A75,A76,Th2;
then
A77: seq.n - seq.k = setsum(Y01) + (seq.k +- seq.k) by A45,A48,
RLVECT_1:def 3
.= setsum(Y01) + 0.X by RLVECT_1:5
.= setsum(Y01) by RLVECT_1:4;
setsum(Y2) = setsum(Y0) + setsum(Y02) by A1,A70,A71,Th2;
then
A78: seq.m - seq.k = setsum(Y02) + (seq.k +- seq.k) by A45,A43,
RLVECT_1:def 3
.= setsum(Y02) + 0.X by RLVECT_1:5
.= setsum(Y02) by RLVECT_1:4;
seq.n - seq.m = seq.n - seq.m + 0.X by RLVECT_1:4
.= seq.n - seq.m + (seq.k - seq.k) by RLVECT_1:5
.= seq.n - (seq.m - (seq.k - seq.k)) by RLVECT_1:29
.= seq.n - ((seq.m - seq.k) + seq.k) by RLVECT_1:29
.= seq.n - (seq.k - (seq.k - seq.m)) by RLVECT_1:33
.= (seq.n - seq.k) + (seq.k +- seq.m) by RLVECT_1:29
.= setsum(Y01) +- setsum(Y02) by A77,A78,RLVECT_1:33;
then ||.(seq.n) - (seq.m).|| <= ||. setsum(Y01).|| + ||. -
setsum(Y02).|| by BHSP_1:30;
then
A79: ||.(seq.n) - (seq.m).|| <= ||. setsum(Y01).|| + ||.
setsum(Y02).|| by BHSP_1:31;
||. setsum(Y01).|| < 1/(k+1) by A33,A44,A74,A75;
then ||. setsum(Y01).|| < e/2 by A39,XXREAL_0:2;
then ||.setsum(Y01).|| + ||. setsum(Y02).|| < e/2 + e/2 by A72,
XREAL_1:8;
hence ||.(seq.n) - (seq.m).|| < e by A79,XXREAL_0:2;
end;
end;
hence ||.(seq.n) - (seq.m).|| < e;
end;
end;
hence ||.(seq.nn) - (seq.mm).|| < e;
end;
hence ex k be Nat st for n, m be Nat st n >= k & m
>= k holds ||.(seq.n) - (seq.m).|| < e;
end;
then
seq is Cauchy by BHSP_3:2;
then seq is convergent by BHSP_3:def 4;
then consider x being Point of X such that
A80: for r be Real st r > 0 ex m be Nat st for n be
Nat st n >= m holds ||.seq.n - x.|| < r by BHSP_2:9;
now
let e be Real such that
A81: e >0;
A82: e/2 > 0/2 by A81,XREAL_1:74;
then consider m be Nat such that
A83: for n be Nat st n >= m holds ||. (seq.n)-x .|| < e/ 2 by A80;
ex i be Nat st 1/(i+1) < e/2 & i >= m
proof
set p = e/2;
consider k1 be Nat such that
A84: p"<k1 by SEQ_4:3;
take i = k1+m;
k1 <= k1 + m by NAT_1:11;
then p" < i by A84,XXREAL_0:2;
then p"+0<i+1 by XREAL_1:8;
then 1/(i+1)<1/p" by A82,XREAL_1:76;
then 1/(i+1)<1 * p"" by XCMPLX_0:def 9;
hence thesis by NAT_1:11;
end;
then consider i be Nat such that
A85: 1/(i+1) < e/2 and
A86: i >= m;
reconsider i as Element of NAT by ORDINAL1:def 12;
consider Y0 be finite Subset of X such that
A87: Y0 is non empty and
A88: A.i = Y0 and
A89: seq.i=setsum(Y0) by A35;
A90: ||.setsum(Y0) - x.|| < e/2 by A83,A86,A89;
now
let Y1 be finite Subset of X such that
A91: Y0 c= Y1 and
A92: Y1 c= Y;
now
per cases;
case
Y0 = Y1;
then ||.x - setsum(Y1).|| = ||.-(x - setsum(Y0)).|| by BHSP_1:31
.= ||.setsum(Y0) - x.|| by RLVECT_1:33;
then ||.x - setsum(Y1).|| < e/2 by A83,A86,A89;
then ||.x-setsum(Y1).|| + 0 < e/2 + e/2 by A81,XREAL_1:8;
hence ||.x-setsum(Y1).|| < e;
end;
case
A93: Y0 <> Y1;
ex Y2 be finite Subset of X st Y2 is non empty & Y2 c= Y &
Y0 misses Y2 & Y0 \/ Y2 = Y1
proof
take Y2 = Y1 \ Y0;
A94: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A91,XBOOLE_1:12;
hence thesis by A92,A93,A94,XBOOLE_1:1,79;
end;
then consider Y2 be finite Subset of X such that
A95: Y2 is non empty & Y2 c= Y and
A96: Y0 misses Y2 and
A97: Y0 \/ Y2 = Y1;
setsum(Y1) - x = setsum(Y0) + setsum(Y2) - x by A1,A96,A97,Th2
.= setsum(Y0) - x + setsum(Y2) by RLVECT_1:def 3;
then ||.setsum(Y1) - x.|| <= ||.setsum(Y0) - x.|| + ||.setsum(Y2)
.|| by BHSP_1:30;
then ||.-(setsum(Y1) - x).|| <= ||.setsum(Y0) - x.|| + ||.setsum(
Y2).|| by BHSP_1:31;
then
A98: ||.x +- setsum(Y1).|| <= ||.setsum(Y0) - x.|| + ||.setsum(Y2
).|| by RLVECT_1:33;
||.setsum(Y2).|| < 1/(i+1) by A33,A88,A95,A96;
then ||.setsum(Y2).|| < e/2 by A85,XXREAL_0:2;
then ||.setsum(Y0)-x.|| + ||.setsum(Y2).|| < e/2 + e/2 by A90,
XREAL_1:8;
hence ||.x - setsum(Y1).|| < e by A98,XXREAL_0:2;
end;
end;
hence ||.x-setsum(Y1).|| < e;
end;
hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1
be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x-setsum(Y1).|| < e by A87
,A88;
end;
hence Y is summable_set;
end;
now
assume Y is summable_set;
then consider x being Point of X such that
A99: for e be Real st e > 0 holds ex Y0 be finite Subset of X st Y0 is
non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.x-setsum(Y1).|| < e;
now
let e be Real;
assume e > 0;
then consider Y0 be finite Subset of X such that
A100: Y0 is non empty and
A101: Y0 c= Y and
A102: for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x-
setsum (Y1).|| < e/2 by A99,XREAL_1:139;
reconsider Y0 as finite non empty Subset of X by A100;
now
let Y1 be finite Subset of X such that
Y1 is non empty and
A103: Y1 c= Y and
A104: Y0 misses Y1;
set Z = Y0 \/ Y1;
Y0 c= Z by XBOOLE_1:7;
then ||.x - setsum(Z).|| < e/2 by A101,A102,A103,XBOOLE_1:8;
then
A105: ||.(x - setsum(Z)).|| + ||.(x - setsum(Y0)).|| < e/2 + e/2 by A101,A102
,
XREAL_1:8;
||.(x-setsum(Z))-(x-setsum(Y0)).|| <= ||.(x-setsum(Z)).|| + ||.-(
x-setsum(Y0)).|| by BHSP_1:30;
then
A106: ||.(x-setsum(Z))-(x-setsum(Y0)).|| <= ||.(x-setsum(Z)).|| + ||.(x
-setsum(Y0)).|| by BHSP_1:31;
setsum(Z) - setsum(Y0) = setsum(Y1) + setsum(Y0) - setsum(Y0) by A1
,A104,Th2
.= setsum(Y1) + (setsum(Y0) +- setsum(Y0)) by RLVECT_1:def 3
.= setsum(Y1) + 0.X by RLVECT_1:5
.= setsum(Y1) by RLVECT_1:4;
then ||.setsum(Y1).|| = ||.-(setsum(Z) - setsum(Y0)).|| by BHSP_1:31
.= ||.setsum(Y0) - setsum(Z).|| by RLVECT_1:33
.= ||.0.X + (setsum(Y0) - setsum(Z)).|| by RLVECT_1:4
.= ||.(x - x) + (setsum(Y0) - setsum(Z)).|| by RLVECT_1:5
.= ||.x - (x - (setsum(Y0) - setsum(Z))).|| by RLVECT_1:29
.= ||.x - ((x - setsum(Y0)) + setsum(Z)).|| by RLVECT_1:29
.= ||.(x - setsum(Z)) - (x - setsum(Y0)).|| by RLVECT_1:27;
hence ||.setsum(Y1).|| < e by A106,A105,XXREAL_0:2;
end;
hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1
be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds ||.
setsum(Y1).|| < e by A101;
end;
hence
for e be Real st e > 0 holds ex Y0 be finite Subset of X st Y0 is non
empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y &
Y0 misses Y1 holds ||.setsum(Y1).|| < e;
end;
hence thesis by A2;
end;