:: On Some Properties of Real {H}ilbert Space, {I} :: by Hiroshi Yamazaki , Yasumasa Suzuki , Takao Inou\'e and Yasunari Shidama :: :: Received February 25, 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, SUBSET_1, ALGSTR_0, BINOP_1, SETWISEO, FINSET_1, FINSEQ_1, STRUCT_0, FUNCT_1, RELAT_1, FINSOP_1, FUNCT_2, TARSKI, BHSP_5, XBOOLE_0, ARYTM_3, REAL_1, XXREAL_0, CARD_1, NORMSP_1, ARYTM_1, SEMI_AF1, SUPINF_2, HAHNBAN, COMPLEX1, BINOP_2, RLVECT_1, BHSP_3, ZFMISC_1, NAT_1, SEQ_2, BHSP_6, RSSPACE2, FCONT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, FUNCT_2, NAT_1, RELSET_1, FINSET_1, BINOP_2, PARTFUN1, STRUCT_0, ALGSTR_0, NORMSP_0, PRE_TOPC, RLVECT_1, BHSP_1, BHSP_2, BHSP_3, BINOP_1, SETWISEO, HAHNBAN, FINSEQ_1, RSSPACE2, FINSOP_1, BHSP_5; constructors BINOP_1, SETWISEO, REAL_1, NAT_1, NAT_D, BINOP_2, FINSOP_1, BHSP_2, BHSP_3, HAHNBAN, BHSP_5, SUPINF_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, BINOP_2, MEMBERED, STRUCT_0, CARD_1; 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 addF of X is commutative associative & the addF of X is having_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 addF of X) "**" p; end; theorem :: BHSP_6:1 for X st the addF of X is commutative associative & the addF of X is having_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 addF of X); theorem :: BHSP_6:2 for X st the addF of X is commutative associative & the addF of X is having_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 Lipschitzian means :: BHSP_6:def 4 ex K be Real st K > 0 & for x holds |.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 Lipschitzian 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 |.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 |.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 |.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 addF of X) "**" p) = addreal "**" q; theorem :: BHSP_6:5 for X st the addF of X is commutative associative & the addF of X is having_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 addF of X is commutative associative & the addF of X is having_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 Lipschitzian 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 |.(L.x)-(setopfunc(Y1,the carrier of X,REAL, L, addreal)).| < e; theorem :: BHSP_6:7 for X st the addF of X is commutative associative & the addF of X is having_a_unity for Y be Subset of X st Y is weakly_summable_set for L be linear-Functional of X st L is Lipschitzian holds Y is_summable_set_by L; theorem :: BHSP_6:8 for X st the addF of X is commutative associative & the addF of X is having_a_unity for Y be Subset of X st Y is summable_set for L be linear-Functional of X st L is Lipschitzian 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 being RealHilbertSpace st the addF of X is commutative associative & the addF of X is having_a_unity 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;