:: 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 Association of Mizar Users environ vocabularies 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, ALGSTR_0; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, BINOP_2, STRUCT_0, ALGSTR_0, REAL_1, NAT_1, FUNCT_1, FUNCT_2, RELAT_1, COMPLEX1, PRE_TOPC, RLVECT_1, BHSP_1, BHSP_3, SQUARE_1, SEQ_2, BINOP_1, FINSET_1, SETWISEO, HAHNBAN, FINSEQ_1, FINSOP_1, BHSP_5, BHSP_6, PARTFUN1, XXREAL_0; constructors PARTFUN1, BINOP_1, DOMAIN_1, SETWISEO, REAL_1, SQUARE_1, NAT_1, BINOP_2, COMPLEX1, SEQ_2, FINSOP_1, BHSP_3, BHSP_5, BHSP_6, SEQ_1, SUPINF_1; registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, BINOP_2, MEMBERED, STRUCT_0, BHSP_5; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions TARSKI, SQUARE_1, RLVECT_1; theorems XBOOLE_0, XBOOLE_1, SQUARE_1, REAL_2, ZFMISC_1, REAL_1, XREAL_0, ABSVALUE, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, SEQ_2, SEQ_4, BHSP_1, BHSP_5, BHSP_6, UNIFORM1, CHAIN_1, XCMPLX_1, BINOP_2, XREAL_1, COMPLEX1, XXREAL_0; schemes NAT_1, FUNCT_2; begin :: Necessary and sufficient condition for summable set reserve X for RealUnitarySpace; reserve x, y, y1, y2 for Point of X; Lm1: for x, y, z, e be Real holds abs(x-y) < e/2 & abs(y-z) < e/2 implies abs(x-z) 0 ex k be Element of NAT st 1/(k+1) < p proof let p be real number; assume p > 0; then A1: 0 < p" by XREAL_1:124; consider k1 be Element of NAT such that A2: p" < k1 by SEQ_4:10; take k = k1; p"+0 < k1+1 by A2,XREAL_1:10; then 1/(k1+1) < 1/p" by A1,XREAL_1:78; hence 1/(k+1) < p by XCMPLX_1:218; end; Lm3: for p being real number, m being Element of NAT st p > 0 ex i be Element of NAT st 1/(i+1) < p & i >= m proof let p be real number, m be Element of NAT; assume p > 0; then A1: 0 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 by BHSP_6:def 6; 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)) j; n <= j by A30,XREAL_1:8; then A32: n < j by A31,REAL_1:def 5; A.(j+1) = (B.(j+1) \/ A.j) by A14; then A.j c= A.(j+1) by XBOOLE_1:7; hence A.(n+1) c= A.(j+1) by A29,A32,NAT_1:13,XBOOLE_1:1; end; end; hence A.(n+1) c= A.(j+1); end; thus thesis from NAT_1:sch 1(A27, A28); end; hence R[n+1] by A21,A22,A23,A25,XBOOLE_1:8; end; A33: for i be Element of NAT holds R[i] from NAT_1:sch 1(A19,A20); rng A c= bool Y proof let y be set such that A34: y in rng A; consider x be set such that A35: x in dom A & y = A.x by A34,FUNCT_1:def 5; reconsider i = x as Element of NAT by A14,A35; A.i c= Y by A33; hence y in bool Y by A35,ZFMISC_1:def 1; end; then A is Function of NAT, bool Y by A14,FUNCT_2:4; hence thesis by A33; end; then consider A be Function of NAT, bool Y such that A36: for i be Element of NAT holds A.i is finite Subset of X & A.i is non empty & A.i c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & A.i misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L, addreal))< 1/(i+1)) & for j be Element of NAT st i <= j holds A.i c= A.j; defpred P[set,set] means ex Y1 be finite Subset of X st Y1 is non empty & A.$1 = Y1 & $2 = setopfunc(Y1, the carrier of X, REAL, L, addreal); A37: for x be set st x in NAT ex y be set st y in REAL & P[x,y] proof let x be set such that A38: x in NAT; reconsider i=x as Element of NAT by A38; A39: A.i is finite Subset of X & A.i is non empty & A.i c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & A.x misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, L, addreal)) < 1/(i+1)) & for j be Element of NAT st i <= j holds A.i c= A.j by A36; then reconsider Y1 = A.x as finite Subset of X; reconsider y = setopfunc(Y1, the carrier of X, REAL, L, addreal) as set; ex Y1 be finite Subset of X st Y1 is non empty & A.x = Y1 & y = setopfunc(Y1, the carrier of X, REAL, L, addreal) by A39; hence thesis; end; ex F being Function of NAT, REAL st for x be set st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A37); then consider F being Function of NAT, REAL such that A40: for x be set st x in NAT holds ex Y1 be finite Subset of X st Y1 is non empty & A.x = Y1 & F.x = setopfunc(Y1, the carrier of X, REAL, L, addreal); set seq = F; A41: for e be real number st e > 0 ex k be Element of NAT st for n, m be Element of NAT st n >= k & m >= k holds abs((seq.n) - (seq.m)) < e proof let e be real number such that A42: e > 0; A43: e/2 > 0/2 by A42,REAL_1:73; then consider k be Element of NAT such that A44: 1/(k+1) < e/2 by Lm2; take k; let n, m be Element of NAT such that A45: n >= k & m >= k; consider Y0 be finite Subset of X such that A46: Y0 is non empty & A.k = Y0 & seq.k = setopfunc(Y0, the carrier of X, REAL, L, addreal) by A40; consider Y1 be finite Subset of X such that A47: Y1 is non empty & A.n = Y1 & seq.n = setopfunc(Y1, the carrier of X, REAL, L, addreal) by A40; consider Y2 be finite Subset of X such that A48: Y2 is non empty & A.m = Y2 & seq.m = setopfunc(Y2, the carrier of X, REAL, L, addreal) by A40; A49: Y0 c= Y1 by A36,A45,A46,A47; A50: Y0 c= Y2 by A36,A45,A46,A48; now per cases; case A51: Y0 = Y1; now per cases; case Y0 = Y2; hence abs((seq.n) - (seq.m)) < e by A42,A47,A48,A51,ABSVALUE:7; end; case A52: Y0 <> Y2; ex Y02 be finite Subset of X st Y02 is non empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 proof take Y02 = Y2 \ Y0; A53: Y2 \ Y0 c= Y2 by XBOOLE_1:36; Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39 .= Y2 by A50,XBOOLE_1:12; hence thesis by A48,A52,A53,XBOOLE_1:1,79; end; then consider Y02 be finite Subset of X such that A54: Y02 is non empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2; dom L = the carrier of X by FUNCT_2:def 1; then A55: setopfunc(Y2, the carrier of X, REAL, L, addreal) = addreal.( setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y02, the carrier of X, REAL, L, addreal)) by A54,BHSP_5:14 .= setopfunc(Y0, the carrier of X, REAL, L, addreal) + setopfunc(Y02, the carrier of X, REAL, L, addreal) by BINOP_2:def 9; abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) < 1/(k+1) by A36,A46,A54; then A56: abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) < e/2 by A44,XXREAL_0:2; A57: abs((seq.n) - (seq.m)) = abs(-setopfunc(Y02, the carrier of X, REAL, L, addreal)) by A47,A48,A51,A55 .= abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) by COMPLEX1:138; e/2 < e by A42,XREAL_1:218; hence abs((seq.n) - (seq.m)) < e by A56,A57,XXREAL_0:2; end; end; hence abs((seq.n) - (seq.m)) < e; end; case A58: Y0 <> Y1; now per cases; case A59: Y0 = Y2; ex Y01 be finite Subset of X st Y01 is non empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 proof take Y01 = Y1 \ Y0; A60: Y1 \ Y0 c= Y1 by XBOOLE_1:36; Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39 .= Y1 by A49,XBOOLE_1:12; hence thesis by A47,A58,A60,XBOOLE_1:1,79; end; then consider Y01 be finite Subset of X such that A61: Y01 is non empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1; dom L = the carrier of X by FUNCT_2:def 1; then A62: setopfunc(Y1, the carrier of X, REAL, L, addreal) = addreal.( setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y01, the carrier of X, REAL, L, addreal)) by A61,BHSP_5:14 .= setopfunc(Y0, the carrier of X, REAL, L, addreal) + setopfunc(Y01, the carrier of X, REAL, L, addreal) by BINOP_2:def 9; abs(setopfunc(Y01, the carrier of X, REAL, L, addreal)) < 1/(k+1) by A36,A46,A61; then abs((seq.n) - (seq.m)) < e/2 by A44,A47,A48,A59,A62, XXREAL_0:2; then abs((seq.n) - (seq.m))+ 0 < e/2 + e/2 by A43,XREAL_1:10; hence abs((seq.n) - (seq.m)) < e; end; case A63: Y0<>Y2; ex Y01 be finite Subset of X st Y01 is non empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 proof take Y01 = Y1 \ Y0; A64: Y1 \ Y0 c= Y1 by XBOOLE_1:36; Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39 .= Y1 by A49,XBOOLE_1:12; hence thesis by A47,A58,A64,XBOOLE_1:1,79; end; then consider Y01 be finite Subset of X such that A65: Y01 is non empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1; ex Y02 be finite Subset of X st Y02 is non empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 proof take Y02 = Y2 \ Y0; A66: Y2 \ Y0 c= Y2 by XBOOLE_1:36; Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39 .= Y2 by A50,XBOOLE_1:12; hence thesis by A48,A63,A66,XBOOLE_1:1,79; end; then consider Y02 be finite Subset of X such that A67: Y02 is non empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2; abs(setopfunc(Y01, the carrier of X, REAL, L, addreal)) < 1/(k+1) by A36,A46,A65; then A68: abs(setopfunc(Y01, the carrier of X, REAL, L, addreal)) < e/2 by A44,XXREAL_0:2; abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) < 1/(k+1) by A36,A46,A67; then abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) < e/2 by A44,XXREAL_0:2; then A69: abs(setopfunc(Y01, the carrier of X, REAL, L, addreal)) + abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) < e/2 + e/2 by A68,XREAL_1:10; dom L = the carrier of X by FUNCT_2:def 1; then A70: setopfunc(Y1, the carrier of X, REAL, L, addreal) = addreal.(setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y01, the carrier of X, REAL, L, addreal)) by A65,BHSP_5:14 .= setopfunc(Y0, the carrier of X, REAL, L, addreal) + setopfunc(Y01, the carrier of X, REAL, L, addreal) by BINOP_2:def 9; dom L = the carrier of X by FUNCT_2:def 1; then setopfunc(Y2, the carrier of X, REAL, L, addreal) = addreal.(setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y02, the carrier of X, REAL, L, addreal)) by A67,BHSP_5:14 .= setopfunc(Y0, the carrier of X, REAL, L, addreal) + setopfunc(Y02, the carrier of X, REAL, L, addreal) by BINOP_2:def 9; then seq.n - seq.m = setopfunc(Y01, the carrier of X, REAL, L, addreal) - setopfunc(Y02, the carrier of X, REAL, L, addreal) by A47,A48,A70; then abs((seq.n) - (seq.m)) <= abs(setopfunc(Y01, the carrier of X, REAL, L, addreal)) + abs(setopfunc(Y02, the carrier of X, REAL, L, addreal)) by COMPLEX1:143; hence abs((seq.n) - (seq.m)) < e by A69,XXREAL_0:2; end; end; hence abs((seq.n) - (seq.m)) < e; end; end; hence abs((seq.n) - (seq.m)) < e; end; for e be real number st 0 < e ex k be Element of NAT st for m be Element of NAT st k <= m holds abs(seq.m -seq.k)= k & m >= k holds abs((seq.n) - (seq.m)) < e by A41,A71; for m be Element of NAT st k <= m holds abs(seq.m - seq.k) 0 ex m be Element of NAT st for n be Element of NAT st n >= m holds abs(seq.n - x) < r by SEQ_2:def 6; reconsider r=x as Real by XREAL_0:def 1; A74: for e be Real st 0 < e 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 proof let e be Real such that A75: e > 0; A76: e/2 > 0/2 by A75,REAL_1:73; then consider m be Element of NAT such that A77: for n be Element of NAT st n >= m holds abs((seq.n)-r) < e/2 by A73; consider i be Element of NAT such that A78: 1/(i+1) < e/2 & i >= m by A76,Lm3; consider Y0 be finite Subset of X such that A79: Y0 is non empty & A.i = Y0 & seq.i = setopfunc(Y0, the carrier of X, REAL, L, addreal) by A40; A80: abs(setopfunc(Y0, the carrier of X, REAL, L, addreal) - r) < e/2 by A77,A78,A79; now let Y1 be finite Subset of X such that A81: Y0 c= Y1 & Y1 c= Y; now per cases; case Y0 = Y1; then abs(r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) < e/2 by A80,UNIFORM1:13; then abs(x - setopfunc(Y1, the carrier of X, REAL, L, addreal)) + 0 < e/2 + e/2 by A76,XREAL_1:10; hence abs(r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) < e; end; case A82: Y0 <> Y1; ex Y2 be finite Subset of X st Y2 is non empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 proof take Y2 = Y1 \ Y0; A83: Y1 \ Y0 c= Y1 by XBOOLE_1:36; Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39 .= Y1 by A81,XBOOLE_1:12; hence thesis by A81,A82,A83,XBOOLE_1:1,79; end; then consider Y2 be finite Subset of X such that A84: Y2 is non empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1; abs(setopfunc(Y2, the carrier of X, REAL, L, addreal)) < 1/(i+1) by A36,A79,A84; then A85: abs(setopfunc(Y2, the carrier of X, REAL, L, addreal)) < e/2 by A78,XXREAL_0:2; dom L = the carrier of X by FUNCT_2:def 1; then setopfunc(Y1, the carrier of X, REAL, L, addreal)-r = addreal.( setopfunc(Y0, the carrier of X, REAL, L, addreal), setopfunc(Y2, the carrier of X, REAL, L, addreal)) - r by A84,BHSP_5:14 .= setopfunc(Y0, the carrier of X, REAL, L, addreal) + setopfunc(Y2, the carrier of X, REAL, L, addreal) - r by BINOP_2:def 9 .= setopfunc(Y0, the carrier of X, REAL, L, addreal) - r + setopfunc(Y2, the carrier of X, REAL, L, addreal); then abs(setopfunc(Y1, the carrier of X, REAL, L, addreal)-r) <= abs(setopfunc(Y0, the carrier of X, REAL, L, addreal) - r) + abs(setopfunc(Y2, the carrier of X, REAL, L, addreal)) by ABSVALUE:21; then A86: abs(x - setopfunc(Y1, the carrier of X, REAL, L, addreal) ) <= abs(setopfunc(Y0, the carrier of X, REAL, L, addreal) - r) + abs(setopfunc(Y2, the carrier of X, REAL, L, addreal)) by UNIFORM1:13; abs(setopfunc(Y0, the carrier of X, REAL, L, addreal) - r) + abs(setopfunc(Y2, the carrier of X, REAL, L, addreal)) < e/2 + e/2 by A80,A85,XREAL_1:10; hence abs(r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) < e by A86,XXREAL_0:2; end; end; hence abs(r - setopfunc(Y1, the carrier of X, REAL, L, addreal)) < e; end; hence thesis by A79; end; take r; thus thesis by A74; end; hence thesis by BHSP_6:def 6; end; theorem Th2: for X st the addF of X is commutative associative & the addF 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 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) proof let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity; let S be finite OrthogonalFamily of X such that A2: S is non empty; let I be Function of the carrier of X, the carrier of X such that A3: S c= dom I & (for y st y in S holds I.y = y); let H be Function of the carrier of X, REAL such that A4: S c= dom H & (for y st y in S holds H.y= y.|.y); consider p be FinSequence of the carrier of X such that A5: p is one-to-one & rng p = S & setopfunc(S, (the carrier of X), (the carrier of X), I, (the addF of X)) = (the addF of X) "**" Func_Seq(I, p) by A1,A3,BHSP_5:def 5; A6: setopfunc(S, the carrier of X, REAL, H, addreal) = addreal "**" Func_Seq(H, p) by A4,A5,BHSP_5:def 5; A7: for y1, y2 st (y1 in S & y2 in S & y1 <> y2) holds (the scalar of X).[I.y1, I.y2] = 0 proof let y1, y2; assume A8: y1 in S & y2 in S & y1 <> y2; then A9: I.y1 = y1 & I.y2 = y2 by A3; y1.|.y2 = 0 by A8,BHSP_5:def 8; hence thesis by A9,BHSP_1:def 1; end; for y st y in S holds H.y = (the scalar of X).[I.y, I.y] proof let y; assume A10: y in S; then A11: I.y = y by A3; H.y = (y.|.y) by A4,A10 .= (the scalar of X).[I.y, I.y] by A11,BHSP_1:def 1; hence thesis; end; then (the scalar of X).[(the addF of X) "**" Func_Seq(I, p), (the addF of X) "**" Func_Seq(I, p)] = addreal "**" Func_Seq(H, p) by A2,A3,A4,A5,A7,BHSP_5:9; hence thesis by A5,A6,BHSP_1:def 1; end; theorem Th3: for X st the addF of X is commutative associative & the addF 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) proof let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity; let S be finite OrthogonalFamily of X such that A2: S is non empty; let H be Functional of X such that A3: S c= dom H & (for x st x in S holds H.x = (x.|.x)); reconsider I = id the carrier of X as Function of the carrier of X, the carrier of X; A4: for x be set st x in the carrier of X holds I.x = x by FUNCT_1:35; A5: dom I = the carrier of X by FUNCT_2:def 1; then A6: setsum(S) = setopfunc(S, the carrier of X, the carrier of X, I, the addF of X) by A1,A4,BHSP_6:1; S c= dom I & for x st x in S holds I.x = x by A5,FUNCT_1:35; hence thesis by A1,A2,A3,A6,Th2; end; theorem Th4: for Y be OrthogonalFamily of X for Z be Subset of X holds Z is Subset of Y implies Z is OrthogonalFamily of X proof let Y be OrthogonalFamily of X; let Z be Subset of X; assume Z is Subset of Y; then for x, y st x in Z & y in Z & x <> y holds x.|.y = 0 by BHSP_5:def 8; hence thesis by BHSP_5:def 8; end; theorem Th5: for Y be OrthonormalFamily of X for Z be Subset of X holds Z is Subset of Y implies Z is OrthonormalFamily of X proof let Y be OrthonormalFamily of X; let Z be Subset of X; assume A1: Z is Subset of Y; Y is OrthogonalFamily of X & for x st x in Y holds x.|.x = 1 by BHSP_5:def 9; then A2: Z is OrthogonalFamily of X by A1,Th4; for x st x in Z holds x.|.x = 1 by A1,BHSP_5:def 9; hence thesis by A2,BHSP_5:def 9; end; begin :: Equivalence of summability theorem Th6: for X st the addF of X is commutative associative & the addF 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 proof let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity & X is_Hilbert_space; let S be OrthonormalFamily of X; let H be Functional of X such that A2: S c= dom H & (for x st x in S holds H.x = (x.|.x)); A3: now assume A4: S is summable_set; now let e be Real such that A5: 0 < e; set e' = sqrt e; 0 < e' by A5,SQUARE_1:93; then consider e1 be Real such that A6: 0 < e1 & e1 < e' by CHAIN_1:1; e1^2 < e'^2 by A6,SQUARE_1:78; then A7: e1 > 0 & e1*e1 < e by A5,A6,SQUARE_1:def 4; consider Y0 be finite Subset of X such that A8: Y0 is non empty & Y0 c= S & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= S & Y0 misses Y1 holds ||.setsum(Y1).|| < e1) by A1,A4,A6,BHSP_6:10; take Y0; thus Y0 is non empty & Y0 c= S by A8; let Y1 be finite Subset of X such that A9: Y1 is non empty & Y1 c= S & Y0 misses Y1; 0 <= ||.setsum(Y1).|| by BHSP_1:34; then ||.setsum(Y1).||^2 < e1^2 by A8,A9,SQUARE_1:78; then A10: ||.setsum(Y1).||^2 < e by A7,XXREAL_0:2; Y1 is finite OrthonormalFamily of X by A9,Th5; then A11: Y1 is finite OrthogonalFamily of X by BHSP_5:def 9; for x st x in Y1 holds H.x = (x.|.x) by A2,A9; then A13: (setsum(Y1)).|.(setsum(Y1)) = setopfunc(Y1, the carrier of X, REAL, H, addreal) by A1,A9,A11,Th3,A2,XBOOLE_1:1; A14: ||.setsum(Y1).|| = sqrt ((setsum(Y1)).|.(setsum(Y1))) by BHSP_1:def 4; 0 <= (setsum(Y1)).|.(setsum(Y1)) by BHSP_1:def 2; then A15: ||.setsum(Y1).||^2 = setopfunc(Y1, the carrier of X, REAL, H, addreal) by A13,A14,SQUARE_1:def 4; 0 <= setopfunc(Y1, the carrier of X, REAL, H, addreal) by A13,BHSP_1:def 2; hence abs(setopfunc(Y1, the carrier of X, REAL, H, addreal)) < e by A10,A15,ABSVALUE:def 1; end; hence S is_summable_set_by H by Th1; end; now assume A16: S is_summable_set_by H; now let e be Real such that A17: 0 < e; set e1 = e * e; 0 < e1 & e1 = e*e by A17,XREAL_1:131; then consider Y0 be finite Subset of X such that A18: Y0 is non empty & Y0 c= S & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= S & Y0 misses Y1 holds abs(setopfunc(Y1, the carrier of X, REAL, H, addreal)) < e1) by A16,Th1; now let Y1 be finite Subset of X such that A19: Y1 is non empty & Y1 c= S & Y0 misses Y1; set F = setopfunc(Y1, the carrier of X, REAL, H, addreal); A20: abs F < e1 by A18,A19; F <= abs F by ABSVALUE:11; then F - e1 < abs F - abs F by A20,REAL_1:92; then A21: F < e1 by XREAL_1:50; Y1 is finite OrthonormalFamily of X by A19,Th5; then A22: Y1 is finite OrthogonalFamily of X by BHSP_5:def 9; (for x st x in Y1 holds H.x= (x.|.x)) by A2,A19; then A24: (setsum Y1).|.(setsum Y1) = F by A1,A19,A22,Th3,A2,XBOOLE_1:1; A25: 0 <= (setsum Y1).|.(setsum Y1) by BHSP_1:def 2; ||.setsum Y1.|| = sqrt ((setsum Y1).|.(setsum Y1)) by BHSP_1:def 4; then ||.setsum Y1.||^2 < e1 by A21,A24,A25,SQUARE_1:def 4; then sqrt(||.setsum(Y1).||^2) < sqrt(e^2) by SQUARE_1:95,XREAL_1:65; then sqrt(||.setsum(Y1).||^2) < e by A17,SQUARE_1:89; hence ||.setsum(Y1).|| < e by BHSP_1:34,SQUARE_1:89; end; hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= S & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= S & Y0 misses Y1 holds ||.setsum(Y1).|| < e) by A18; end; hence S is summable_set by A1,BHSP_6:10; end; hence thesis by A3; end; theorem Th7: 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) proof let S be Subset of X such that A1: S is non empty & S is summable_set; let e be Real such that A2: 0 < e; 0 <= ||.sum(S).|| by BHSP_1:34; then 0 <= 2*||.sum(S).|| by REAL_2:121; then A3: 0+0 < 2*||.sum(S).||+1 by XREAL_1:10; set e' = e/(2*||.sum(S).||+1); 0 < e' by A2,A3,REAL_2:127; then consider Y01 be finite Subset of X such that A4: Y01 is non empty & Y01 c= S & for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= S holds ||.sum(S) - setsum(Y1).|| < e' by A1,BHSP_6:def 3; consider Y02 be finite Subset of X such that A5: Y02 is non empty & Y02 c= S & for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= S holds ||.sum(S) - setsum(Y1).|| < 1 by A1,BHSP_6:def 3; set Y0 = Y01 \/ Y02; ex x being set st x in Y01 by A4,XBOOLE_0:def 1; then A6: Y0 is non empty; A7: Y0 c= S by A4,A5,XBOOLE_1:8; 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 proof let Y1 be finite Subset of X such that A8: Y0 c= Y1 & Y1 c= S; set F = (sum(S)).|.(sum(S)), G = (setsum(Y1)).|.(setsum(Y1)); set SS = sum(S)-setsum(Y1), SY = setsum(Y1); abs(F - G) = abs(F - ((sum(S)).|.SY) + (((sum(S)).|.SY) - G)) .= abs(((sum(S)).|.SS) + (((sum(S)).|.SY) - G)) by BHSP_1:17 .= abs(((sum(S)).|.SS) + (SS.|.SY)) by BHSP_1:16; then A9: abs(F - G) <= abs(((sum(S)).|.SS)) + abs(SS.|.SY) by COMPLEX1:142; abs(((sum(S)).|.SS)) <= ||.sum(S).||*||.SS.|| by BHSP_1:35; then abs(F - G) + abs(((sum(S)).|.SS)) <= abs(((sum(S)).|.SS)) + abs(SS.|.SY) + ||.sum(S).||*||.SS.|| by A9,XREAL_1:9; then abs(F - G) + abs(((sum(S)).|.SS)) <= (abs(SS.|.SY) + ||.sum(S).||*||.SS.||) + abs(((sum(S)).|.SS)); then A10: abs(F - G) <= abs(SS.|.SY) + ||.sum(S).||*||.SS.|| by XREAL_1:8; abs(SS.|.SY) <= ||.SS.||*||.SY.|| by BHSP_1:35; then abs(F - G) + abs(SS.|.SY) <= abs(SS.|.SY) + ||.sum(S).||*||.SS.|| + ||.SS.||*||.SY.|| by A10,XREAL_1:9; then abs(F - G) + abs(SS.|.SY) <= ||.sum(S).||*||.SS.|| + ||.SS.||*||.SY.|| + abs(SS.|.SY); then A11: abs(F - G) <= ||.SS.||*||.sum(S).|| + ||.SS.||*||.SY.|| by XREAL_1:8; ||.SY.|| = ||.-SY.|| by BHSP_1:37 .= ||.0.X - SY.|| by RLVECT_1:27 .= ||.-sum(S) + sum(S) - SY.|| by RLVECT_1:16 .= ||.-sum(S) + SS.|| by RLVECT_1:def 6; then ||.SY.|| <= ||.-sum(S).|| + ||.SS.|| by BHSP_1:36; then A12: ||.SY.|| <= ||.sum(S).|| + ||.SS.|| by BHSP_1:37; Y02 c= Y1 by A8,XBOOLE_1:11; then ||.SS.|| + ||.SY.|| < 1 + (||.sum(S).|| + ||.SS.||) by A5,A8,A12,XREAL_1:10; then ||.SY.|| + ||.SS.|| - ||.SS.|| < 1 + ||.sum(S).|| + ||.SS.|| - ||.SS.|| by REAL_1:92; then A13: ||.sum(S).|| + ||.SY.|| < 1 + ||.sum(S).|| + ||.sum(S).|| by XREAL_1:10; 0 <= ||.SS.|| by BHSP_1:34; then A14: ||.SS.||*(||.sum(S).|| + ||.SY.||) <= ||.SS.||*(2*||.sum(S).|| + 1) by A13,XREAL_1:66; Y01 c= Y1 by A8,XBOOLE_1:11; then ||.SS.||*(2*||.sum(S).|| + 1) < e'*(2*||.sum(S).|| + 1) by A3,A4,A8,XREAL_1:70; then ||.SS.||*(||.sum(S).|| + ||.SY.||) + ||.SS.||*(2*||.sum(S).|| + 1) < e'*(2*||.sum(S).|| + 1) + ||.SS.||*(2*||.sum(S).|| + 1) by A14,XREAL_1:10; then ||.SS.||*(||.sum(S).|| + ||.SY.||) + ||.SS.||*(2*||.sum(S).|| + 1) - ||.SS.||*(2*||.sum(S).|| + 1) < e'*(2*||.sum(S).|| + 1) + ||.SS.||*(2*||.sum(S).|| + 1) - ||.SS.||*(2*||.sum(S).|| + 1) by REAL_1:92; then ||.SS.||*(||.sum(S).|| + ||.SY.||) < e by A3,XCMPLX_1:88; then abs(F - G) + ||.SS.||*(||.sum(S).|| + ||.SY.||) < e + ||.SS.||*(||.sum(S).|| + ||.SY.||) by A11,XREAL_1:10; then abs(F - G) + ||.SS.||*(||.sum(S).|| + ||.SY.||) - ||.SS.||*(||.sum(S).|| + ||.SY.||) < e + ||.SS.||*(||.sum(S).|| + ||.SY.||) - ||.SS.||*(||.sum(S).|| + ||.SY.||) by REAL_1:92; hence thesis; end; hence thesis by A6,A7; end; Lm4: for p1, p2 being real number st for e be Real st 0 < e holds abs(p1 - p2) < e holds p1 = p2 proof let p1, p2 be real number; assume A1: for e be Real st 0 < e holds abs(p1 - p2) < e; assume p1 <> p2; then p1 - p2 <> 0; then 0 < abs(p1-p2) by COMPLEX1:133; hence contradiction by A1; end; theorem for X st the addF of X is commutative associative & the addF 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) proof let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity & X is_Hilbert_space; let S be OrthonormalFamily of X such that A2: S is non empty; let H be Functional of X such that A3: S c= dom H & (for x st x in S holds H.x= (x.|.x)); assume A4: S is summable_set; then A5: S is_summable_set_by H by A1,A3,Th6; A6: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= S holds (setsum(Y1)).|.(setsum(Y1)) = setopfunc(Y1, the carrier of X, REAL, H,addreal) proof let Y1 be finite Subset of X such that A7: Y1 is non empty & Y1 c= S; Y1 is finite OrthonormalFamily of X by A7,Th5; then A9: Y1 is finite OrthogonalFamily of X by BHSP_5:def 9; for x st x in Y1 holds H.x = (x.|.x) by A3,A7; hence thesis by A1,A7,A9,Th3,A3,XBOOLE_1:1; end; set p1 = (sum(S)).|.(sum(S)), p2 = sum_byfunc(S, H); for e be Real st 0 < e holds abs(p1 - p2) < e proof let e be Real such that A10: 0 < e; A11: 0/2 < e/2 by A10,REAL_1:73; then consider Y01 be finite Subset of X such that A12: Y01 is non empty & Y01 c= S & for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= S holds abs(p1 - ((setsum Y1).|.(setsum Y1))) < e/2 by A2,A4,Th7; consider Y02 be finite Subset of X such that A13: Y02 is non empty & Y02 c= S & for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= S holds abs(p2 - setopfunc(Y1, the carrier of X, REAL, H, addreal)) < e/2 by A5,A11,BHSP_6:def 7; set Y1 = Y01 \/ Y02; set r = setopfunc(Y1, the carrier of X, REAL, H, addreal); reconsider Y011 = Y01 as non empty set by A12; A14: Y1 is finite Subset of X & Y01 c= Y1 & Y02 c= Y1 & Y1 c= S by A12,A13,XBOOLE_1:7,8; Y1 = Y011 \/ Y02; then (setsum(Y1)).|.(setsum(Y1)) = r by A6,A14; then A15: abs(p1 - r) < e/2 by A12,A14; p1 - p2 = (p1 - r) + (r - p2); then A16: abs(p1-p2) <= abs(p1-r) + abs(r-p2) by COMPLEX1:142; abs(p1-r) + abs(p2-r) < e/2 + e/2 by A13,A14,A15,XREAL_1:10; then abs(p1-r) + abs(r-p2) < e by UNIFORM1:13; hence thesis by A16,XXREAL_0:2; end; hence thesis by Lm4; end;