let X be RealHilbertSpace; ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for S being OrthonormalFamily of X
for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds
H . x = x .|. x ) holds
( S is summable_set iff S is_summable_set_by H ) )
assume A1:
( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity )
; for S being OrthonormalFamily of X
for H being Functional of X st S c= dom H & ( for x being Point of X 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 X 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 X st x in S holds
H . x = x .|. x ) implies ( S is summable_set iff S is_summable_set_by H ) )
assume that
A2:
S c= dom H
and
A3:
for x being Point of X st x in S holds
H . x = x .|. x
; ( S is summable_set iff S is_summable_set_by H )
A4:
now assume A5:
S is
summable_set
;
S is_summable_set_by Hnow let e be
Real;
( 0 < e implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,H,addreal)) < e ) ) )assume A6:
0 < e
;
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,H,addreal)) < e ) )set e9 =
sqrt e;
0 < sqrt e
by A6, SQUARE_1:25;
then consider e1 being
Real such that A7:
0 < e1
and A8:
e1 < sqrt e
by CHAIN_1:1;
e1 ^2 < (sqrt e) ^2
by A7, A8, SQUARE_1:16;
then A9:
e1 * e1 < e
by A6, SQUARE_1:def 2;
consider Y0 being
finite Subset of
X such that A10:
( not
Y0 is
empty &
Y0 c= S )
and A11:
for
Y1 being
finite Subset of
X st not
Y1 is
empty &
Y1 c= S &
Y0 misses Y1 holds
||.(setsum Y1).|| < e1
by A1, A5, A7, BHSP_6:10;
take Y0 =
Y0;
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X 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 A10;
for Y1 being finite Subset of X 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
X;
( not Y1 is empty & Y1 c= S & Y0 misses Y1 implies abs (setopfunc (Y1, the carrier of X,REAL,H,addreal)) < e )assume that A12:
not
Y1 is
empty
and A13:
Y1 c= S
and A14:
Y0 misses Y1
;
abs (setopfunc (Y1, the carrier of X,REAL,H,addreal)) < e
Y1 is
finite OrthonormalFamily of
X
by A13, Th5;
then A15:
Y1 is
finite OrthogonalFamily of
X
by BHSP_5:def 9;
for
x being
Point of
X st
x in Y1 holds
H . x = x .|. x
by A3, A13;
then A16:
(setsum Y1) .|. (setsum Y1) = setopfunc (
Y1, the
carrier of
X,
REAL,
H,
addreal)
by A1, A2, A12, A13, A15, Th3, XBOOLE_1:1;
0 <= ||.(setsum Y1).||
by BHSP_1:28;
then
||.(setsum Y1).|| ^2 < e1 ^2
by A11, A12, A13, A14, SQUARE_1:16;
then A17:
||.(setsum Y1).|| ^2 < e
by A9, 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 A18:
||.(setsum Y1).|| ^2 = setopfunc (
Y1, the
carrier of
X,
REAL,
H,
addreal)
by A16, SQUARE_1:def 2;
0 <= setopfunc (
Y1, the
carrier of
X,
REAL,
H,
addreal)
by A16, BHSP_1:def 2;
hence
abs (setopfunc (Y1, the carrier of X,REAL,H,addreal)) < e
by A17, A18, ABSVALUE:def 1;
verum end; hence
S is_summable_set_by H
by Th1;
verum end;
now assume A19:
S is_summable_set_by H
;
S is summable_set now let e be
Real;
( 0 < e implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )assume A20:
0 < e
;
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) )set e1 =
e * e;
0 < e * e
by A20, XREAL_1:129;
then consider Y0 being
finite Subset of
X such that A21:
( not
Y0 is
empty &
Y0 c= S )
and A22:
for
Y1 being
finite Subset of
X 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 A19, Th1;
now let Y1 be
finite Subset of
X;
( not Y1 is empty & Y1 c= S & Y0 misses Y1 implies ||.(setsum Y1).|| < e )assume that A23:
not
Y1 is
empty
and A24:
Y1 c= S
and A25:
Y0 misses Y1
;
||.(setsum Y1).|| < eset F =
setopfunc (
Y1, the
carrier of
X,
REAL,
H,
addreal);
Y1 is
finite OrthonormalFamily of
X
by A24, Th5;
then A26:
Y1 is
finite OrthogonalFamily of
X
by BHSP_5:def 9;
abs (setopfunc (Y1, the carrier of X,REAL,H,addreal)) < e * e
by A22, A23, A24, A25;
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:4, XREAL_1:15;
then A27:
setopfunc (
Y1, the
carrier of
X,
REAL,
H,
addreal)
< e * e
by XREAL_1:48;
for
x being
Point of
X st
x in Y1 holds
H . x = x .|. x
by A3, A24;
then A28:
(setsum Y1) .|. (setsum Y1) = setopfunc (
Y1, the
carrier of
X,
REAL,
H,
addreal)
by A1, A2, A23, A24, A26, 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 A27, A28, SQUARE_1:def 2;
then
sqrt (||.(setsum Y1).|| ^2) < sqrt (e ^2)
by SQUARE_1:27, XREAL_1:63;
then
sqrt (||.(setsum Y1).|| ^2) < e
by A20, SQUARE_1:22;
hence
||.(setsum Y1).|| < e
by BHSP_1:28, SQUARE_1:22;
verum end; hence
ex
Y0 being
finite Subset of
X st
( not
Y0 is
empty &
Y0 c= S & ( for
Y1 being
finite Subset of
X st not
Y1 is
empty &
Y1 c= S &
Y0 misses Y1 holds
||.(setsum Y1).|| < e ) )
by A21;
verum end; hence
S is
summable_set
by A1, BHSP_6:10;
verum end;
hence
( S is summable_set iff S is_summable_set_by H )
by A4; verum