BHSP_6: On Some Properties of Real {H}ilbert Space, {I}

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines setsum BHSP_6:def 1 :

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;

definition

let X be RealUnitarySpace;
let Y be Subset of X;

attr Y is summable_set means :: 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 defines summable_set BHSP_6:def 2 :

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 by A1;
uniqueness

proof end;

end;

:: deftheorem defines sum BHSP_6:def 3 :

definition

let X be RealUnitarySpace;
let Y be Subset of X;

attr Y is weakly_summable_set means :: 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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.(L . (x - (setsum Y1))).| < e ) );

end;

:: deftheorem defines weakly_summable_set BHSP_6:def 5 :

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 :: 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
|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) );

end;

:: deftheorem defines is_summable_set_by BHSP_6:def 6 :

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
|.(it - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) );

existence by A1;
uniqueness

proof end;

end;

:: deftheorem defines sum_byfunc BHSP_6:def 7 :

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

proof end;

theorem Th7: :: BHSP_6:7

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 Lipschitzian holds
Y is_summable_set_by L by Th3, Th7;

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;