:: by Hiroshi Yamazaki , Yasumasa Suzuki , Takao Inou\'e and Yasunari Shidama

::

:: Received February 25, 2003

:: Copyright (c) 2003-2019 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;

ex b_{1} being Element of X ex p being FinSequence of the carrier of X st

( p is one-to-one & rng p = Y & b_{1} = the addF of X "**" p )

for b_{1}, b_{2} being Element of X st ex p being FinSequence of the carrier of X st

( p is one-to-one & rng p = Y & b_{1} = the addF of X "**" p ) & ex p being FinSequence of the carrier of X st

( p is one-to-one & rng p = Y & b_{2} = the addF of X "**" p ) holds

b_{1} = b_{2}

end;
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 p being FinSequence of the carrier of X st

( p is one-to-one & rng p = Y & it = the addF of X "**" p );

ex b

( p is one-to-one & rng p = Y & b

proof end;

uniqueness for b

( p is one-to-one & rng p = Y & b

( p is one-to-one & rng p = Y & b

b

proof 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_{3} being Element of X holds

( b_{3} = setsum Y iff ex p being FinSequence of the carrier of X st

( p is one-to-one & rng p = Y & b_{3} = the addF of X "**" p ) );

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

( b

( p is one-to-one & rng p = Y & b

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)

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)

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;

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

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 ;

ex b_{1} 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_{1} - (setsum Y1)).|| < e ) )
by A1;

uniqueness

for b_{1}, b_{2} 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_{1} - (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_{2} - (setsum Y1)).|| < e ) ) ) holds

b_{1} = b_{2}

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

ex b

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

uniqueness

for b

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

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

b

proof 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_{3} being Point of X holds

( b_{3} = 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_{3} - (setsum Y1)).|| < e ) ) );

for X being RealUnitarySpace

for Y being Subset of X st Y is summable_set holds

for b

( b

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

:: 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.|| ) ) );

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;

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

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

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

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

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

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 ;

ex b_{1} 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

|.(b_{1} - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )
by A1;

uniqueness

for b_{1}, b_{2} 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

|.(b_{1} - (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

|.(b_{2} - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) ) holds

b_{1} = b_{2}

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

ex b

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

uniqueness

for b

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

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

b

proof 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_{4} being Real holds

( b_{4} = 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

|.(b_{4} - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) );

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

( b

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

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

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

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)

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

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

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;

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

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

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;