let X be RealUnitarySpace; ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity & X is Hilbert implies for S being OrthonormalFamily of X
for H being Functional of X st S c= dom H & ( for x being Point of st x in S holds
H . x = x .|. x ) holds
( S is summable_set iff S is_summable_set_by H ) )
assume that
A1:
( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity )
and
A2:
X is Hilbert
; for S being OrthonormalFamily of X
for H being Functional of X st S c= dom H & ( for x being Point of st x in S holds
H . x = x .|. x ) holds
( S is summable_set iff S is_summable_set_by H )
let S be OrthonormalFamily of X; for H being Functional of X st S c= dom H & ( for x being Point of st x in S holds
H . x = x .|. x ) holds
( S is summable_set iff S is_summable_set_by H )
let H be Functional of X; ( S c= dom H & ( for x being Point of st x in S holds
H . x = x .|. x ) implies ( S is summable_set iff S is_summable_set_by H ) )
assume that
A3:
S c= dom H
and
A4:
for x being Point of st x in S holds
H . x = x .|. x
; ( S is summable_set iff S is_summable_set_by H )
A5:
now assume A6:
S is
summable_set
;
S is_summable_set_by Hnow let e be
Real;
( 0 < e implies ex Y0 being finite Subset of st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e ) ) )assume A7:
0 < e
;
ex Y0 being finite Subset of st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e ) )set e' =
sqrt e;
0 < sqrt e
by A7, SQUARE_1:93;
then consider e1 being
Real such that A8:
0 < e1
and A9:
e1 < sqrt e
by CHAIN_1:1;
e1 ^2 < (sqrt e) ^2
by A8, A9, SQUARE_1:78;
then A10:
e1 * e1 < e
by A7, SQUARE_1:def 4;
consider Y0 being
finite Subset of
such that A11:
( not
Y0 is
empty &
Y0 c= S )
and A12:
for
Y1 being
finite Subset of st not
Y1 is
empty &
Y1 c= S &
Y0 misses Y1 holds
||.(setsum Y1).|| < e1
by A1, A2, A6, A8, BHSP_6:10;
take Y0 =
Y0;
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e ) )thus
( not
Y0 is
empty &
Y0 c= S )
by A11;
for Y1 being finite Subset of st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < elet Y1 be
finite Subset of ;
( not Y1 is empty & Y1 c= S & Y0 misses Y1 implies abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e )assume that A13:
not
Y1 is
empty
and A14:
Y1 c= S
and A15:
Y0 misses Y1
;
abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e
Y1 is
finite OrthonormalFamily of
X
by A14, Th5;
then A16:
Y1 is
finite OrthogonalFamily of
X
by BHSP_5:def 9;
for
x being
Point of st
x in Y1 holds
H . x = x .|. x
by A4, A14;
then A17:
(setsum Y1) .|. (setsum Y1) = setopfunc Y1,the
carrier of
X,
REAL ,
H,
addreal
by A1, A3, A13, A14, A16, Th3, XBOOLE_1:1;
0 <= ||.(setsum Y1).||
by BHSP_1:34;
then
||.(setsum Y1).|| ^2 < e1 ^2
by A12, A13, A14, A15, SQUARE_1:78;
then A18:
||.(setsum Y1).|| ^2 < e
by A10, XXREAL_0:2;
(
||.(setsum Y1).|| = sqrt ((setsum Y1) .|. (setsum Y1)) &
0 <= (setsum Y1) .|. (setsum Y1) )
by BHSP_1:def 2, BHSP_1:def 4;
then A19:
||.(setsum Y1).|| ^2 = setopfunc Y1,the
carrier of
X,
REAL ,
H,
addreal
by A17, SQUARE_1:def 4;
0 <= setopfunc Y1,the
carrier of
X,
REAL ,
H,
addreal
by A17, BHSP_1:def 2;
hence
abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e
by A18, A19, ABSVALUE:def 1;
verum end; hence
S is_summable_set_by H
by Th1;
verum end;
now assume A20:
S is_summable_set_by H
;
S is summable_set now let e be
Real;
( 0 < e implies ex Y0 being finite Subset of st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )assume A21:
0 < e
;
ex Y0 being finite Subset of st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) )set e1 =
e * e;
0 < e * e
by A21, XREAL_1:131;
then consider Y0 being
finite Subset of
such that A22:
( not
Y0 is
empty &
Y0 c= S )
and A23:
for
Y1 being
finite Subset of st not
Y1 is
empty &
Y1 c= S &
Y0 misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e * e
by A20, Th1;
now let Y1 be
finite Subset of ;
( not Y1 is empty & Y1 c= S & Y0 misses Y1 implies ||.(setsum Y1).|| < e )assume that A24:
not
Y1 is
empty
and A25:
Y1 c= S
and A26:
Y0 misses Y1
;
||.(setsum Y1).|| < eset F =
setopfunc Y1,the
carrier of
X,
REAL ,
H,
addreal ;
Y1 is
finite OrthonormalFamily of
X
by A25, Th5;
then A27:
Y1 is
finite OrthogonalFamily of
X
by BHSP_5:def 9;
abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e * e
by A23, A24, A25, A26;
then
(setopfunc Y1,the carrier of X,REAL ,H,addreal ) - (e * e) < (abs (setopfunc Y1,the carrier of X,REAL ,H,addreal )) - (abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ))
by ABSVALUE:11, XREAL_1:17;
then A28:
setopfunc Y1,the
carrier of
X,
REAL ,
H,
addreal < e * e
by XREAL_1:50;
for
x being
Point of st
x in Y1 holds
H . x = x .|. x
by A4, A25;
then A29:
(setsum Y1) .|. (setsum Y1) = setopfunc Y1,the
carrier of
X,
REAL ,
H,
addreal
by A1, A3, A24, A25, A27, Th3, XBOOLE_1:1;
(
0 <= (setsum Y1) .|. (setsum Y1) &
||.(setsum Y1).|| = sqrt ((setsum Y1) .|. (setsum Y1)) )
by BHSP_1:def 2, BHSP_1:def 4;
then
||.(setsum Y1).|| ^2 < e * e
by A28, A29, SQUARE_1:def 4;
then
sqrt (||.(setsum Y1).|| ^2 ) < sqrt (e ^2 )
by SQUARE_1:95, XREAL_1:65;
then
sqrt (||.(setsum Y1).|| ^2 ) < e
by A21, SQUARE_1:89;
hence
||.(setsum Y1).|| < e
by BHSP_1:34, SQUARE_1:89;
verum end; hence
ex
Y0 being
finite Subset of st
( not
Y0 is
empty &
Y0 c= S & ( for
Y1 being
finite Subset of st not
Y1 is
empty &
Y1 c= S &
Y0 misses Y1 holds
||.(setsum Y1).|| < e ) )
by A22;
verum end; hence
S is
summable_set
by A1, A2, BHSP_6:10;
verum end;
hence
( S is summable_set iff S is_summable_set_by H )
by A5; verum