:: 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-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies 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 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;
 constructors BINOP_1, DOMAIN_1, SETWISEO, REAL_1, SQUARE_1, BINOP_2, COMPLEX1,
      FINSOP_1, BHSP_3, BHSP_5, BHSP_6, RELSET_1, COMSEQ_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;
 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 |.setopfunc(Y1, the carrier of X, REAL,
  L, addreal).| <e;

theorem :: BHSP_7:2
  for X st the addF of X is commutative associative & the addF of X
is having_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 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);

theorem :: BHSP_7:3
  for X st the addF of X is commutative associative & the addF of X
is having_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 being RealHilbertSpace
   st the addF of X is commutative associative & the addF of X
  is having_a_unity for S be OrthonormalFamily of X for H be
  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;

theorem :: BHSP_7:7
  for S be Subset of X st S is summable_set
  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 |.((sum(S)).|.(sum(S))) - ((
  setsum(Y1)).|.(setsum(Y1))).| < e;

theorem :: BHSP_7:8
  for X being RealHilbertSpace
   st the addF of X is commutative associative & the addF of X is
  having_a_unity for S be OrthonormalFamily of X for H be
  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 implies (sum(S)).|.(sum(S)) = sum_byfunc(S, H);