The abstract of the Mizar article:

On Some Properties of Real Hilbert Space. Part I

by

Hiroshi Yamazaki,

Yasumasa Suzuki,

Takao Inoue, and

Yasunari Shidama

Received February 25, 2003

MML identifier: BHSP_6

[ Mizar article, MML identifier index ]

environ

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


begin :: Preliminaries

 reserve X for RealUnitarySpace;
 reserve x for Point of X;
 reserve i, n for Nat;

definition
  let X such that
   the add of X is commutative associative & the add of X has_a_unity;
  let Y be finite Subset of X;
  func setsum Y -> Element of X means
:: BHSP_6:def 1
  ex p being FinSequence of the carrier of X st
    p is one-to-one & rng p = Y & it = (the add of X) "**" p;
end;

theorem :: BHSP_6:1
  for X st the add of X is commutative associative & the add of X has_a_unity
  for Y be finite Subset of X
  for I be Function of the carrier of X,the carrier of X st
    Y c= dom I & for x be set st x in dom I holds I.x = x holds
  setsum(Y)
    = setopfunc(Y, the carrier of X, the carrier of X, I, the add of X);

theorem :: BHSP_6:2
  for X st the add of X is commutative associative & the add of X has_a_unity
  for Y1, Y2 be finite Subset of X st Y1 misses Y2
  for Z be finite Subset of X st Z = Y1 \/ Y2 holds
  setsum(Z) = setsum(Y1) + setsum(Y2);

begin :: Summability

definition let X;
  let Y be Subset of X;
  attr Y is summable_set means
:: BHSP_6:def 2
  ex x st
    for e be Real st e > 0 ex Y0 be finite Subset of X st
    Y0 is non empty & Y0 c= Y &
    for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y
      holds ||.x-setsum(Y1).|| < e;
end;

definition let X;
  let Y be Subset of X;
  assume Y is summable_set;
  func sum Y -> Point of X means
:: BHSP_6:def 3
    for e be Real st e > 0 ex Y0 be finite Subset of X st
  Y0 is non empty & Y0 c= Y &
  for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y
    holds ||.it-setsum(Y1).|| < e;
end;

definition let X;
           let L be linear-Functional of X;
  attr L is Bounded means
:: BHSP_6:def 4
  ex K be Real st K > 0 &
  for x holds abs(L.x) <= K * ||.x.||;
end;

definition let X;
           let Y be Subset of X;
  attr Y is weakly_summable_set means
:: BHSP_6:def 5
  ex x st
  for L be linear-Functional of X st L is Bounded
  for e be Real st e > 0
  ex Y0 be finite Subset of X st
  Y0 is non empty & Y0 c= Y &
  for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y
  holds abs(L.(x-setsum(Y1))) < e;
end;

definition let X;
           let Y be Subset of X;
           let L be Functional of X;
  pred Y is_summable_set_by L means
:: BHSP_6:def 6
  ex r be Real st
    for e be Real st e > 0
    ex Y0 be finite Subset of X st
    Y0 is non empty & Y0 c= Y &
    for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y
      holds
    abs(r-setopfunc(Y1,the carrier of X,REAL, L, addreal)) < e;
end;

definition let X;
           let Y be Subset of X;
           let L be Functional of X;
  assume Y is_summable_set_by L;
  func sum_byfunc(Y,L) -> Real means
:: BHSP_6:def 7
    for e be Real st e > 0
    ex Y0 be finite Subset of X st
    Y0 is non empty & Y0 c= Y &
    for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y
      holds
    abs(it-setopfunc(Y1,the carrier of X,REAL, L, addreal)) < e;
end;

theorem :: BHSP_6:3
  for Y be Subset of X st Y is summable_set holds
  Y is weakly_summable_set;

theorem :: BHSP_6:4
  for L be linear-Functional of X
  for p be FinSequence of the carrier of X st len p >=1
  for q be FinSequence of REAL st dom p = dom q &
      (for i st i in dom q holds q.i = L.(p.i) )
  holds L.((the add of X) "**" p) = addreal "**" q;

theorem :: BHSP_6:5
  for X st the add of X is commutative associative & the add of X has_a_unity
  for S be finite Subset of X st S is non empty
  for L be linear-Functional of X holds
  L.(setsum(S)) = setopfunc(S,the carrier of X,REAL, L, addreal);

theorem :: BHSP_6:6
  for X st the add of X is commutative associative & the add of X has_a_unity
  for Y be Subset of X holds
  Y is weakly_summable_set implies
  ex x st
    for L be linear-Functional of X st L is Bounded
    for e be Real st e > 0
    ex Y0 be finite Subset of X st
    Y0 is non empty & Y0 c= Y &
    for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y
    holds abs((L.x)-(setopfunc(Y1,the carrier of X,REAL, L, addreal))) < e;

theorem :: BHSP_6:7
  for X st the add of X is commutative associative & the add of X has_a_unity
  for Y be Subset of X st Y is weakly_summable_set
  for L be linear-Functional of X st L is Bounded holds
  Y is_summable_set_by L;

theorem :: BHSP_6:8
    for X st the add of X is commutative associative & the add of X has_a_unity
  for Y be Subset of X st Y is summable_set
  for L be linear-Functional of X st L is Bounded holds
  Y is_summable_set_by L;

theorem :: BHSP_6:9
    for Y be finite Subset of X st Y is non empty holds
  Y is summable_set;

begin :: Necessary and sufficient condition for summability

theorem :: BHSP_6:10
    for X st
    the add of X is commutative associative &
    the add of X has_a_unity & X is_Hilbert_space
  for Y be Subset of X holds Y is summable_set iff
  (for e be Real st e > 0 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 ||.setsum(Y1).|| < e));