:: 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-2011 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 b₁ being Element of X ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b₁ = the addF of X "**" p )

proof end;

uniqueness
for b₁, b₂ being Element of X st ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b₁ = the addF of X "**" p ) & ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b₂ = the addF of X "**" p ) holds
b₁ = b₂

proof end;

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 b₃ being Element of X holds
( b₃ = setsum Y iff ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b₃ = 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)

proof end;

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)

proof end;

begin

definition

let X be RealUnitarySpace;
let Y be Subset of X;
attr Y 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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & 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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(it - (setsum Y1)).|| < e ) );
existence
ex b₁ 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
||.(b₁ - (setsum Y1)).|| < e ) ) by A1, Def2;
uniqueness
for b₁, b₂ 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
||.(b₁ - (setsum Y1)).|| < e ) ) ) & ( 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
||.(b₂ - (setsum Y1)).|| < e ) ) ) holds
b₁ = b₂

proof end;

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 b₃ being Point of X holds
( b₃ = sum Y iff 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
||.(b₃ - (setsum Y1)).|| < e ) ) );

definition

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

end;

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

definition

let X be RealUnitarySpace;
let Y be Subset of X;
attr Y 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 Bounded holds
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
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 Bounded holds
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
abs (L . (x - (setsum Y1))) < e ) ) );

definition

let X be RealUnitarySpace;
let Y be Subset of X;
let L be Functional of X;
pred Y 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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & 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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & 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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (it - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) );
existence
ex b₁ being Real 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
abs (b₁ - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) by A1, Def6;
uniqueness
for b₁, b₂ being Real 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
abs (b₁ - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ) & ( 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
abs (b₂ - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ) holds
b₁ = b₂

proof end;

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 b₄ being Real holds
( b₄ = 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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (b₄ - (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

proof end;

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 & ( 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

proof end;

theorem Th5: :: BHSP_6:5

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 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)

proof end;

theorem Th6: :: BHSP_6:6

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 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 Bounded holds
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
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )

proof end;

theorem Th7: :: BHSP_6:7

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 Subset of X st Y is weakly_summable_set holds
for L being linear-Functional of X st L is Bounded holds
Y is_summable_set_by L

proof end;

theorem :: BHSP_6:8

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 Subset of X st Y is summable_set holds
for L being linear-Functional of X st L is Bounded 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

proof end;

begin

theorem :: BHSP_6:10

for X being RealHilbertSpace 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 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 & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )

proof end;