let X be RealUnitarySpace; :: thesis: ( 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 st not S is empty holds
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 ) & S is summable_set holds
(sum S) .|. (sum S) = sum_byfunc S,H )
assume A1:
( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity & X is Hilbert )
; :: thesis: for S being OrthonormalFamily of X st not S is empty holds
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 ) & S is summable_set holds
(sum S) .|. (sum S) = sum_byfunc S,H
let S be OrthonormalFamily of X; :: thesis: ( not S is empty implies 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 ) & S is summable_set holds
(sum S) .|. (sum S) = sum_byfunc S,H )
assume A2:
not S is empty
; :: thesis: 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 ) & S is summable_set holds
(sum S) .|. (sum S) = sum_byfunc S,H
let H be Functional of X; :: thesis: ( S c= dom H & ( for x being Point of X st x in S holds
H . x = x .|. x ) & S is summable_set implies (sum S) .|. (sum S) = sum_byfunc S,H )
assume A3:
( S c= dom H & ( for x being Point of X st x in S holds
H . x = x .|. x ) )
; :: thesis: ( not S is summable_set or (sum S) .|. (sum S) = sum_byfunc S,H )
assume A4:
S is summable_set
; :: thesis: (sum S) .|. (sum S) = sum_byfunc S,H
then A5:
S is_summable_set_by H
by A1, A3, Th6;
A6:
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S holds
(setsum Y1) .|. (setsum Y1) = setopfunc Y1,the carrier of X,REAL ,H,addreal
proof
let Y1 be
finite Subset of
X;
:: thesis: ( not Y1 is empty & Y1 c= S implies (setsum Y1) .|. (setsum Y1) = setopfunc Y1,the carrier of X,REAL ,H,addreal )
assume A7:
( not
Y1 is
empty &
Y1 c= S )
;
:: thesis: (setsum Y1) .|. (setsum Y1) = setopfunc Y1,the carrier of X,REAL ,H,addreal
Y1 is
finite OrthonormalFamily of
X
by A7, Th5;
then A9:
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, A7;
hence
(setsum Y1) .|. (setsum Y1) = setopfunc Y1,the
carrier of
X,
REAL ,
H,
addreal
by A1, A7, A9, Th3, A3, XBOOLE_1:1;
:: thesis: verum
end;
set p1 = (sum S) .|. (sum S);
set p2 = sum_byfunc S,H;
for e being Real st 0 < e holds
abs (((sum S) .|. (sum S)) - (sum_byfunc S,H)) < e
proof
let e be
Real;
:: thesis: ( 0 < e implies abs (((sum S) .|. (sum S)) - (sum_byfunc S,H)) < e )
assume A10:
0 < e
;
:: thesis: abs (((sum S) .|. (sum S)) - (sum_byfunc S,H)) < e
A11:
0 / 2
< e / 2
by A10, XREAL_1:76;
then consider Y01 being
finite Subset of
X such that A12:
( not
Y01 is
empty &
Y01 c= S & ( for
Y1 being
finite Subset of
X st
Y01 c= Y1 &
Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e / 2 ) )
by A2, A4, Th7;
consider Y02 being
finite Subset of
X such that A13:
( not
Y02 is
empty &
Y02 c= S & ( for
Y1 being
finite Subset of
X st
Y02 c= Y1 &
Y1 c= S holds
abs ((sum_byfunc S,H) - (setopfunc Y1,the carrier of X,REAL ,H,addreal )) < e / 2 ) )
by A5, A11, BHSP_6:def 7;
set Y1 =
Y01 \/ Y02;
set r =
setopfunc (Y01 \/ Y02),the
carrier of
X,
REAL ,
H,
addreal ;
reconsider Y011 =
Y01 as non
empty set by A12;
A14:
(
Y01 \/ Y02 is
finite Subset of
X &
Y01 c= Y01 \/ Y02 &
Y02 c= Y01 \/ Y02 &
Y01 \/ Y02 c= S )
by A12, A13, XBOOLE_1:7, XBOOLE_1:8;
Y01 \/ Y02 = Y011 \/ Y02
;
then
(setsum (Y01 \/ Y02)) .|. (setsum (Y01 \/ Y02)) = setopfunc (Y01 \/ Y02),the
carrier of
X,
REAL ,
H,
addreal
by A6, A14;
then A15:
abs (((sum S) .|. (sum S)) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal )) < e / 2
by A12, A14;
((sum S) .|. (sum S)) - (sum_byfunc S,H) = (((sum S) .|. (sum S)) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal )) + ((setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ) - (sum_byfunc S,H))
;
then A16:
abs (((sum S) .|. (sum S)) - (sum_byfunc S,H)) <= (abs (((sum S) .|. (sum S)) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ))) + (abs ((setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ) - (sum_byfunc S,H)))
by COMPLEX1:142;
(abs (((sum S) .|. (sum S)) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ))) + (abs ((sum_byfunc S,H) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ))) < (e / 2) + (e / 2)
by A13, A14, A15, XREAL_1:10;
then
(abs (((sum S) .|. (sum S)) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ))) + (abs ((setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ) - (sum_byfunc S,H))) < e
by UNIFORM1:13;
hence
abs (((sum S) .|. (sum S)) - (sum_byfunc S,H)) < e
by A16, XXREAL_0:2;
:: thesis: verum
end;
hence
(sum S) .|. (sum S) = sum_byfunc S,H
by Lm4; :: thesis: verum