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


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 )
proof end;
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
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 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)
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 :
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 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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(b1 - (setsum Y1)).|| < e ) )
by A1;
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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(b1 - (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
||.(b2 - (setsum Y1)).|| < e ) ) ) holds
b1 = b2
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 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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(b3 - (setsum Y1)).|| < e ) ) );

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

:: deftheorem 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 & ( for x being Point of X holds |.(L . x).| <= K * ||.x.|| ) ) );

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 :
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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.(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 :: 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 :
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
|.(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
|.(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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.(b1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )
by A1;
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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.(b1 - (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
|.(b2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) ) holds
b1 = b2
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 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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.(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
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 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
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 Lipschitzian 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 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
proof end;

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;