:: 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-2012 Association of Mizar Users


begin

definition
let X be RealUnitarySpace;
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ;
let Y be finite Subset of X;
func setsum Y ->  Element of X means :Def1: :: BHSP_6:def 1
 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
 ex b1 being Element of X ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b1 = the addF of X "**" p )
proofend;
uniqueness
 for b1, b2 being Element of X st ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b1 = the addF of X "**" p ) & ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b2 = the addF of X "**" p ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines setsum BHSP_6:def_1_:_
 for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for Y being finite Subset of X
for b3 being Element of X holds
( b3 = setsum Y iff ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b3 = the addF of X "**" p ) );

theorem Th1: :: BHSP_6:1
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for Y being finite Subset of X
for I being Function of the carrier of X, the carrier of X st Y c= dom I & ( for x being 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)
proofend;

theorem Th2: :: BHSP_6:2
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for Y1, Y2 being finite Subset of X st Y1 misses Y2 holds
for Z being finite Subset of X st Z = Y1 \/ Y2 holds
setsum Z = (setsum Y1) + (setsum Y2)
proofend;

begin

definition
let X be RealUnitarySpace;
let Y be Subset of X;
attrY is summable_set  means :Def2: :: BHSP_6:def 2
 ex x being Point of X st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) );
end;

:: deftheorem Def2 defines summable_set BHSP_6:def_2_:_
 for X being RealUnitarySpace
for Y being Subset of X holds
( Y is summable_set iff ex x being Point of X st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) ) );

definition
let X be RealUnitarySpace;
let Y be Subset of X;
assume A1: Y is summable_set ;
func sum Y ->  Point of X means :: BHSP_6:def 3
 for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
||.(it - (setsum Y1)).|| < e ) );
existence
 ex b1 being Point of X st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
||.(b1 - (setsum Y1)).|| < e ) ) by A1, Def2;
uniqueness
 for b1, b2 being Point of X st ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
||.(b1 - (setsum Y1)).|| < e ) ) ) &amp; ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
||.(b2 - (setsum Y1)).|| < e ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines sum BHSP_6:def_3_:_
 for X being RealUnitarySpace
for Y being Subset of X st Y is summable_set holds
for b3 being Point of X holds
( b3 = sum Y iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
||.(b3 - (setsum Y1)).|| < e ) ) );

definition
let X be RealUnitarySpace;
let L be linear-Functional of X;
attrL is Lipschitzian  means :Def4: :: BHSP_6:def 4
 ex K being Real st
( K > 0 &amp; ( for x being Point of X holds abs (L . x) <= K * ||.x.|| ) );
end;

:: deftheorem Def4 defines Lipschitzian BHSP_6:def_4_:_
 for X being RealUnitarySpace
for L being linear-Functional of X holds
( L is Lipschitzian iff ex K being Real st
( K > 0 &amp; ( for x being Point of X holds abs (L . x) <= K * ||.x.|| ) ) );

definition
let X be RealUnitarySpace;
let Y be Subset of X;
attrY is weakly_summable_set  means :Def5: :: BHSP_6:def 5
 ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e ) );
end;

:: deftheorem Def5 defines weakly_summable_set BHSP_6:def_5_:_
 for X being RealUnitarySpace
for Y being Subset of X holds
( Y is weakly_summable_set iff ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e ) ) );

definition
let X be RealUnitarySpace;
let Y be Subset of X;
let L be Functional of X;
predY is_summable_set_by L means :Def6: :: BHSP_6:def 6
 ex r being Real st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) );
end;

:: deftheorem Def6 defines is_summable_set_by BHSP_6:def_6_:_
 for X being RealUnitarySpace
for Y being Subset of X
for L being Functional of X holds
( Y is_summable_set_by L iff ex r being Real st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) );

definition
let X be RealUnitarySpace;
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 :: BHSP_6:def 7
 for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
abs (it - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) );
existence
 ex b1 being Real st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
abs (b1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) by A1, Def6;
uniqueness
 for b1, b2 being Real st ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
abs (b1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ) &amp; ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
abs (b2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines sum_byfunc BHSP_6:def_7_:_
 for X being RealUnitarySpace
for Y being Subset of X
for L being Functional of X st Y is_summable_set_by L holds
for b4 being Real holds
( b4 = sum_byfunc (Y,L) iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
abs (b4 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) );

theorem Th3: :: BHSP_6:3
for X being RealUnitarySpace
for Y being Subset of X st Y is summable_set holds
Y is weakly_summable_set
proofend;

theorem Th4: :: BHSP_6:4
for X being RealUnitarySpace
for L being linear-Functional of X
for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q &amp; ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
proofend;

theorem Th5: :: BHSP_6:5
for X being RealUnitarySpace st the addF of X is commutative &amp; the addF of X is associative &amp; the addF of X is having_a_unity holds
for S being finite Subset of X st not S is empty holds
for L being linear-Functional of X holds L . (setsum S) = setopfunc (S, the carrier of X,REAL,L,addreal)
proofend;

theorem Th6: :: BHSP_6:6
for X being RealUnitarySpace st the addF of X is commutative &amp; the addF of X is associative &amp; the addF of X is having_a_unity holds
for Y being Subset of X st Y is weakly_summable_set holds
ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
proofend;

theorem Th7: :: BHSP_6:7
for X being RealUnitarySpace st the addF of X is commutative &amp; the addF of X is associative &amp; the addF of X is having_a_unity holds
for Y being Subset of X st Y is weakly_summable_set holds
for L being linear-Functional of X st L is Lipschitzian holds
Y is_summable_set_by L
proofend;

theorem :: BHSP_6:8
for X being RealUnitarySpace st the addF of X is commutative &amp; the addF of X is associative &amp; the addF of X is having_a_unity holds
for Y being Subset of X st Y is summable_set holds
for L being linear-Functional of X st L is Lipschitzian holds
Y is_summable_set_by L by Th3, Th7;

theorem :: BHSP_6:9
for X being RealUnitarySpace
for Y being finite Subset of X st not Y is empty holds
Y is summable_set
proofend;

begin

theorem :: BHSP_6:10
for X being RealHilbertSpace st the addF of X is commutative &amp; the addF of X is associative &amp; the addF of X is having_a_unity holds
for Y being Subset of X holds
( Y is summable_set iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st not Y1 is empty &amp; Y1 c= Y &amp; Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )
proofend;