The abstract of the Mizar article:

On Some Properties of Real Hilbert Space. Part II

by

Hiroshi Yamazaki,

Yasumasa Suzuki,

Takao Inoue, and

Yasunari Shidama

Received April 17, 2003

MML identifier: BHSP_7

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, PRE_TOPC, NORMSP_1, RLVECT_1, FUNCT_1, ARYTM, ARYTM_1,
      ARYTM_3, RELAT_1, ABSVALUE, BINOP_1, SQUARE_1, SEQ_2, PROB_2, BHSP_1,
      BHSP_3, FINSET_1, VECTSP_1, HAHNBAN, FINSEQ_1, SETWISEO, FINSOP_1,
      BHSP_5, BHSP_6, SEMI_AF1;
 notation TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, STRUCT_0, REAL_1, NAT_1, FUNCT_1, FUNCT_2, RELAT_1, PRE_TOPC,
      RLVECT_1, ABSVALUE, BHSP_1, BHSP_3, SQUARE_1, SEQ_2, BINOP_1, FINSET_1,
      VECTSP_1, SETWISEO, HAHNBAN, FINSEQ_1, FINSOP_1, BHSP_5, BHSP_6;
 constructors REAL_1, NAT_1, DOMAIN_1, SQUARE_1, SEQ_2, PREPOWER, BINOP_1,
      BHSP_3, SETWISEO, HAHNBAN1, FINSOP_1, BHSP_5, BHSP_6, MEMBERED;
 clusters RELSET_1, STRUCT_0, XREAL_0, XBOOLE_0, FINSET_1, BHSP_5, MEMBERED,
      NUMBERS, ORDINAL2;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Necessary and sufficient condition for summable set

  reserve X for RealUnitarySpace;

  reserve x, y, y1, y2 for Point of X;

theorem :: BHSP_7:1
  for Y be Subset of X
  for L be Functional of X
  holds Y is_summable_set_by L
  iff
  (for e be Real st 0 < e holds
  ex Y0 be finite Subset of X st
    Y0 is non empty & Y0 c= Y &
    (for Y1 be finite Subset of X st
      Y1 is non empty & Y1 c= Y & Y0 misses Y1
     holds
     abs(setopfunc(Y1, the carrier of X, REAL, L, addreal)) <e ));

theorem :: BHSP_7:2
  for X st the add of X is commutative associative &
  the add of X has_a_unity
  for S be finite OrthogonalFamily of X st S is non empty
  for I be Function of the carrier of X, the carrier of X st
  S c= dom I & (for y st y in S holds I.y = y)
  for H be Function of the carrier of X, REAL st
  S c= dom H & (for y st y in S holds H.y= (y.|.y))
  holds
  setopfunc(S, the carrier of X, the carrier of X, I, the add of X)
  .|. setopfunc(S, the carrier of X, the carrier of X, I, the add of X)
  = setopfunc(S, the carrier of X, REAL, H, addreal);

theorem :: BHSP_7:3
  for X st the add of X is commutative associative &
  the add of X has_a_unity
  for S be finite OrthogonalFamily of X st S is non empty
  for H be Functional of X st
  S c= dom H & (for x st x in S holds H.x = (x.|.x))
  holds
  (setsum(S)).|.(setsum(S))
  = setopfunc(S, the carrier of X, REAL, H, addreal);

theorem :: BHSP_7:4
  for Y be OrthogonalFamily of X
  for Z be Subset of X
  holds
  Z is Subset of Y implies Z is OrthogonalFamily of X;

theorem :: BHSP_7:5
  for Y be OrthonormalFamily of X
  for Z be Subset of X
  holds
  Z is Subset of Y implies Z is OrthonormalFamily of X;

begin :: Equivalence of summability

theorem :: BHSP_7:6
  for X st the add of X is commutative associative &
  the add of X has_a_unity & X is_Hilbert_space
  for S be OrthonormalFamily of X
  for H be Functional of X st
  S c= dom H & (for x st x in S holds H.x = (x.|.x))
  holds
  S is summable_set iff S is_summable_set_by H;

theorem :: BHSP_7:7
  for S be Subset of X st
  S is non empty & S is summable_set
  holds
  (for e be Real st 0 < e ex Y0 be finite Subset of X st
  Y0 is non empty & Y0 c= S &
  for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= S
  holds abs(((sum(S)).|.(sum(S))) - ((setsum(Y1)).|.(setsum(Y1)))) < e);

theorem :: BHSP_7:8
    for X st the add of X is commutative associative &
  the add of X has_a_unity & X is_Hilbert_space
  for S be OrthonormalFamily of X st S is non empty
  for H be Functional of X st
  S c= dom H & (for x st x in S holds H.x = (x.|.x))
  holds
  S is summable_set implies (sum(S)).|.(sum(S)) = sum_byfunc(S, H);