BHSP_7: On Some Properties of Real {H}ilbert Space, {II}

:: On Some Properties of Real {H}ilbert Space, {II}
:: by Hiroshi Yamazaki , Yasumasa Suzuki , Takao Inou\'e and Yasunari Shidama
::
:: Received April 17, 2003
:: Copyright (c) 2003-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, BHSP_1, PRE_TOPC, REAL_1, COMPLEX1, ARYTM_1, ARYTM_3, XXREAL_0, CARD_1, SUBSET_1, RELAT_1, HAHNBAN, BHSP_6, FINSET_1, XBOOLE_0, TARSKI, BHSP_5, STRUCT_0, BINOP_2, FUNCT_1, ZFMISC_1, NAT_1, SEQ_2, ALGSTR_0, BINOP_1, SETWISEO, PROB_2, FINSEQ_1, FINSOP_1, SQUARE_1, NORMSP_1, SEMI_AF1, SUPINF_2, RSSPACE2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, BINOP_2, STRUCT_0, ALGSTR_0, NORMSP_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCT_2, RELAT_1, PRE_TOPC, BHSP_1, SQUARE_1, SEQ_2, BINOP_1, FINSET_1, SETWISEO, HAHNBAN, FINSEQ_1, FINSOP_1, BHSP_5, BHSP_6, RSSPACE2, PARTFUN1, XXREAL_0;
definitions TARSKI;
theorems XBOOLE_1, SQUARE_1, ZFMISC_1, ABSVALUE, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, SEQ_2, SEQ_4, BHSP_1, BHSP_5, BHSP_6, UNIFORM1, CHAIN_1, XCMPLX_1, BINOP_2, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1;
schemes NAT_1, FUNCT_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, BINOP_2, STRUCT_0, BHSP_5, SQUARE_1, NAT_1, VALUED_0;
constructors HIDDEN, BINOP_1, DOMAIN_1, SETWISEO, REAL_1, SQUARE_1, BINOP_2, COMPLEX1, FINSOP_1, BHSP_3, BHSP_5, BHSP_6, RELSET_1, COMSEQ_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities SQUARE_1, RLVECT_1;
expansions TARSKI;

Lm1: for x, y, z, e being Real st |.(x - y).| < e / 2 & |.(y - z).| < e / 2 holds
|.(x - z).| < e

proof end;

Lm2: for p being Real st p > 0 holds
ex k being Nat st 1 / (k + 1) < p

proof end;

Lm3: for p being Real
for m being Nat st p > 0 holds
ex i being Nat st
( 1 / (i + 1) < p & i >= m )

proof end;

theorem Th1: :: BHSP_7:1

for X being RealUnitarySpace
for Y being Subset of X
for L being Functional of X holds
( Y is_summable_set_by L iff for e being Real st 0 < e 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
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) )

proof end;

theorem Th2: :: BHSP_7: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 S being finite OrthogonalFamily of X st not S is empty holds
for I being Function of the carrier of X, the carrier of X st S c= dom I & ( for y being Point of X st y in S holds
I . y = y ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = y .|. y ) holds
(setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)

proof end;

theorem Th3: :: BHSP_7:3

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 OrthogonalFamily 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 ) holds
(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)

proof end;

theorem Th4: :: BHSP_7:4

for X being RealUnitarySpace
for Y being OrthogonalFamily of X
for Z being Subset of X st Z is Subset of Y holds
Z is OrthogonalFamily of X

proof end;

theorem Th5: :: BHSP_7:5

for X being RealUnitarySpace
for Y being OrthonormalFamily of X
for Z being Subset of X st Z is Subset of Y holds
Z is OrthonormalFamily of X

proof end;

theorem Th6: :: BHSP_7:6

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

proof end;

theorem Th7: :: BHSP_7:7

for X being RealUnitarySpace
for S being Subset of X st S is summable_set holds
for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
|.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e ) )

proof end;

Lm4: for p1, p2 being Real st ( for e being Real st 0 < e holds
|.(p1 - p2).| < e ) holds
p1 = p2

proof end;

theorem :: BHSP_7:8

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 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 ) & S is summable_set holds
(sum S) .|. (sum S) = sum_byfunc (S,H)

proof end;