:: 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-2019 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;