:: BHSP_6 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let X be RealUnitarySpace;
assume A1: ( the add of X is commutative & the add of X is associative & the add of X has_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 add 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 add 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 add of X "**" p ) & ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b2 = the add of X "**" p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines setsum BHSP_6:def 1 :
for X being RealUnitarySpace st the add of X is commutative & the add of X is associative & the add of X has_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 add of X "**" p ) );

theorem Th1: :: BHSP_6:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealUnitarySpace st the add of X is commutative & the add of X is associative & the add of X has_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 add of X
proof end;

theorem Th2: :: BHSP_6:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealUnitarySpace st the add of X is commutative & the add of X is associative & the add of X has_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 :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 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, 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 & 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 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 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
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 & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (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
abs (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
abs (b4 - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) );

theorem Th3: :: BHSP_6:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 add of X "**" p) = addreal "**" q
proof end;

theorem Th5: :: BHSP_6:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealUnitarySpace st the add of X is commutative & the add of X is associative & the add of X has_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealUnitarySpace st the add of X is commutative & the add of X is associative & the add of X has_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealUnitarySpace st the add of X is commutative & the add of X is associative & the add of X has_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealUnitarySpace st the add of X is commutative & the add of X is associative & the add of X has_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
proof end;

theorem :: BHSP_6:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealUnitarySpace st the add of X is commutative & the add of X is associative & the add of X has_a_unity & X is_Hilbert_space 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;