:: BHSP_6 semantic presentation

definition

let c₁ be RealUnitarySpace;
assume E1: ( the add of c₁ is commutative & the add of c₁ is associative & the add of c₁ has_a_unity ) ;
let c₂ be finite Subset of c₁;
func setsum c₂ -> Element of a₁ means :Def1: :: BHSP_6:def 1
ex b₁ being FinSequence of the carrier of a₁ st
( b₁ is one-to-one & rng b₁ = a₂ & a₃ = the add of a₁ "**" b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines setsum BHSP_6:def 1 :

theorem Th1: :: BHSP_6:1

for b₁ being RealUnitarySpace st the add of b₁ is commutative & the add of b₁ is associative & the add of b₁ has_a_unity holds
for b₂ being finite Subset of b₁
for b₃ being Function of the carrier of b₁,the carrier of b₁ st b₂ c= dom b₃ & ( for b₄ being set st b₄ in dom b₃ holds
b₃ . b₄ = b₄ ) holds
setsum b₂ = setopfunc b₂,the carrier of b₁,the carrier of b₁,b₃,the add of b₁

proof end;

theorem Th2: :: BHSP_6:2

for b₁ being RealUnitarySpace st the add of b₁ is commutative & the add of b₁ is associative & the add of b₁ has_a_unity holds
for b₂, b₃ being finite Subset of b₁ st b₂ misses b₃ holds
for b₄ being finite Subset of b₁ st b₄ = b₂ \/ b₃ holds
setsum b₄ = (setsum b₂) + (setsum b₃)

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be Subset of c₁;
attr a₂ is summable_set means :Def2: :: BHSP_6:def 2
ex b₁ being Point of a₁ st
for b₂ being Real st b₂ > 0 holds
ex b₃ being finite Subset of a₁ st
( not b₃ is empty & b₃ c= a₂ & ( for b₄ being finite Subset of a₁ st b₃ c= b₄ & b₄ c= a₂ holds
||.(b₁ - (setsum b₄)).|| < b₂ ) );

end;

:: deftheorem Def2 defines summable_set BHSP_6:def 2 :

definition

let c₁ be RealUnitarySpace;
let c₂ be Subset of c₁;
assume E5: c₂ is summable_set ;
func sum c₂ -> Point of a₁ means :: BHSP_6:def 3
for b₁ being Real st b₁ > 0 holds
ex b₂ being finite Subset of a₁ st
( not b₂ is empty & b₂ c= a₂ & ( for b₃ being finite Subset of a₁ st b₂ c= b₃ & b₃ c= a₂ holds
||.(a₃ - (setsum b₃)).|| < b₁ ) );
existence by E5, Def2;
uniqueness

proof end;

end;

:: deftheorem Def3 defines sum BHSP_6:def 3 :

definition

let c₁ be RealUnitarySpace;
let c₂ be linear-Functional of c₁;
attr a₂ is Bounded means :Def4: :: BHSP_6:def 4
ex b₁ being Real st
( b₁ > 0 & ( for b₂ being Point of a₁ holds abs (a₂ . b₂) <= b₁ * ||.b₂.|| ) );

end;

:: deftheorem Def4 defines Bounded BHSP_6:def 4 :

definition

let c₁ be RealUnitarySpace;
let c₂ be Subset of c₁;
attr a₂ is weakly_summable_set means :Def5: :: BHSP_6:def 5
ex b₁ being Point of a₁ st
for b₂ being linear-Functional of a₁ st b₂ is Bounded holds
for b₃ being Real st b₃ > 0 holds
ex b₄ being finite Subset of a₁ st
( not b₄ is empty & b₄ c= a₂ & ( for b₅ being finite Subset of a₁ st b₄ c= b₅ & b₅ c= a₂ holds
abs (b₂ . (b₁ - (setsum b₅))) < b₃ ) );

end;

:: deftheorem Def5 defines weakly_summable_set BHSP_6:def 5 :

definition

let c₁ be RealUnitarySpace;
let c₂ be Subset of c₁;
let c₃ be Functional of c₁;
pred c₂ is_summable_set_by c₃ means :Def6: :: BHSP_6:def 6
ex b₁ being Real st
for b₂ being Real st b₂ > 0 holds
ex b₃ being finite Subset of a₁ st
( not b₃ is empty & b₃ c= a₂ & ( for b₄ being finite Subset of a₁ st b₃ c= b₄ & b₄ c= a₂ holds
abs (b₁ - (setopfunc b₄,the carrier of a₁,REAL ,a₃,addreal )) < b₂ ) );

end;

:: deftheorem Def6 defines is_summable_set_by BHSP_6:def 6 :

definition

let c₁ be RealUnitarySpace;
let c₂ be Subset of c₁;
let c₃ be Functional of c₁;
assume E8: c₂ is_summable_set_by c₃ ;
func sum_byfunc c₂,c₃ -> Real means :: BHSP_6:def 7
for b₁ being Real st b₁ > 0 holds
ex b₂ being finite Subset of a₁ st
( not b₂ is empty & b₂ c= a₂ & ( for b₃ being finite Subset of a₁ st b₂ c= b₃ & b₃ c= a₂ holds
abs (a₄ - (setopfunc b₃,the carrier of a₁,REAL ,a₃,addreal )) < b₁ ) );
existence by E8, Def6;
uniqueness

proof end;

end;

:: deftheorem Def7 defines sum_byfunc BHSP_6:def 7 :

theorem Th3: :: BHSP_6:3

for b₁ being RealUnitarySpace
for b₂ being Subset of b₁ st b₂ is summable_set holds
b₂ is weakly_summable_set

proof end;

theorem Th4: :: BHSP_6:4

for b₁ being RealUnitarySpace
for b₂ being linear-Functional of b₁
for b₃ being FinSequence of the carrier of b₁ st len b₃ >= 1 holds
for b₄ being FinSequence of REAL st dom b₃ = dom b₄ & ( for b₅ being Nat st b₅ in dom b₄ holds
b₄ . b₅ = b₂ . (b₃ . b₅) ) holds
b₂ . (the add of b₁ "**" b₃) = addreal "**" b₄

proof end;

theorem Th5: :: BHSP_6:5

for b₁ being RealUnitarySpace st the add of b₁ is commutative & the add of b₁ is associative & the add of b₁ has_a_unity holds
for b₂ being finite Subset of b₁ st not b₂ is empty holds
for b₃ being linear-Functional of b₁ holds b₃ . (setsum b₂) = setopfunc b₂,the carrier of b₁,REAL ,b₃,addreal

proof end;

theorem Th6: :: BHSP_6:6

for b₁ being RealUnitarySpace st the add of b₁ is commutative & the add of b₁ is associative & the add of b₁ has_a_unity holds
for b₂ being Subset of b₁ st b₂ is weakly_summable_set holds
ex b₃ being Point of b₁ st
for b₄ being linear-Functional of b₁ st b₄ is Bounded holds
for b₅ being Real st b₅ > 0 holds
ex b₆ being finite Subset of b₁ st
( not b₆ is empty & b₆ c= b₂ & ( for b₇ being finite Subset of b₁ st b₆ c= b₇ & b₇ c= b₂ holds
abs ((b₄ . b₃) - (setopfunc b₇,the carrier of b₁,REAL ,b₄,addreal )) < b₅ ) )

proof end;

theorem Th7: :: BHSP_6:7

proof end;

theorem Th8: :: BHSP_6:8

for b₁ being RealUnitarySpace st the add of b₁ is commutative & the add of b₁ is associative & the add of b₁ has_a_unity holds
for b₂ being Subset of b₁ st b₂ is summable_set holds
for b₃ being linear-Functional of b₁ st b₃ is Bounded holds
b₂ is_summable_set_by b₃

proof end;

theorem Th9: :: BHSP_6:9

for b₁ being RealUnitarySpace
for b₂ being finite Subset of b₁ st not b₂ is empty holds
b₂ is summable_set

proof end;

theorem Th10: :: BHSP_6:10

for b₁ being RealUnitarySpace st the add of b₁ is commutative & the add of b₁ is associative & the add of b₁ has_a_unity & b₁ is_Hilbert_space holds
for b₂ being Subset of b₁ holds
( b₂ is summable_set iff for b₃ being Real st b₃ > 0 holds
ex b₄ being finite Subset of b₁ st
( not b₄ is empty & b₄ c= b₂ & ( for b₅ being finite Subset of b₁ st not b₅ is empty & b₅ c= b₂ & b₄ misses b₅ holds
||.(setsum b₅).|| < b₃ ) ) )

proof end;