:: Hilbert Space of Real Sequences :: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama :: :: Received April 3, 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, STRUCT_0, RSSPACE, RLVECT_1, SEQ_1, VALUED_1, SERIES_1, SUPINF_2, ARYTM_3, REAL_1, RELAT_1, ARYTM_1, PROB_2, CARD_3, COMPLEX1, SUBSET_1, CARD_1, XXREAL_0, FUNCT_1, SQUARE_1, BHSP_1, ALGSTR_0, ZFMISC_1, REALSET1, PRE_TOPC, VALUED_0, XXREAL_2, ORDINAL2, SEQ_2, NAT_1, BHSP_3, NORMSP_1, REWRITE1, RSSPACE2, ASYMPT_1; notations TARSKI, SUBSET_1, ZFMISC_1, ORDINAL1, BINOP_1, REALSET1, RELAT_1, PARTFUN1, FUNCT_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, REAL_1, NAT_1, VALUED_1, SQUARE_1, SEQ_1, SERIES_1, COMSEQ_2, SEQ_2, STRUCT_0, ALGSTR_0, XREAL_0, PRE_TOPC, RLVECT_1, BHSP_1, BHSP_2, BHSP_3, FUNCSDOM, RSSPACE; constructors PARTFUN1, BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, NAT_D, SEQ_2, SERIES_1, REALSET1, RLSUB_1, BHSP_2, BHSP_3, RSSPACE, VALUED_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, FUNCSDOM; registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, RSSPACE, VALUED_1, FUNCT_2, VALUED_0, NAT_1, SEQ_4, SERIES_1, SQUARE_1, SEQ_1, SEQ_2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Hilbert Space of Real Sequences theorem :: RSSPACE2:1 the carrier of l2_Space = the_set_of_l2RealSequences & (for x be set holds x is VECTOR of l2_Space iff x is Real_Sequence & seq_id(x)(#)seq_id(x)is summable) & 0.l2_Space = Zeroseq & (for u be VECTOR of l2_Space holds u = seq_id(u)) & (for u,v be VECTOR of l2_Space holds u+v =seq_id(u)+seq_id(v)) & (for r be Real for u be VECTOR of l2_Space holds r*u =r(#)seq_id(u)) & (for u be VECTOR of l2_Space holds -u =-seq_id(u) & seq_id(-u)=-seq_id(u)) & (for u,v be VECTOR of l2_Space holds u-v =seq_id(u)-seq_id(v)) & (for v,w be VECTOR of l2_Space holds seq_id(v)(#)seq_id(w) is summable) & for v,w be VECTOR of l2_Space holds v.|.w = Sum(seq_id(v)(#)seq_id(w)); theorem :: RSSPACE2:2 for x, y, z being Point of l2_Space for a be Real holds ( x .|. x = 0 iff x = 0.l2_Space ) & 0 <= x .|. x & x .|. y = y .|. x & (x+y) .|. z = x .|. z + y .|. z & (a*x) .|. y = a * ( x .|. y ); registration cluster l2_Space -> RealUnitarySpace-like; end; registration cluster l2_Space -> complete; end; registration cluster complete for RealUnitarySpace; end; definition mode RealHilbertSpace is complete RealUnitarySpace; end; begin :: Miscellaneous theorem :: RSSPACE2:3 for r be Real_Sequence st (for n be Nat holds 0 <= r.n) holds ( for n be Nat holds 0 <= (Partial_Sums r).n ) & ( for n be Nat holds r.n <= (Partial_Sums r).n ) & ( r is summable implies ( for n be Nat holds (Partial_Sums r).n <= Sum r) & for n be Nat holds r.n <= Sum r ); theorem :: RSSPACE2:4 (for x,y be Real holds (x+y)*(x+y) <= 2*x*x + 2*y*y) & for x,y be Real holds x*x <= 2*(x-y)*(x-y) + 2*y*y; theorem :: RSSPACE2:5 for e being Real, s being Real_Sequence st (s is convergent & ex k being Nat st for i being Nat st k <= i holds s.i <= e ) holds lim s <=e; theorem :: RSSPACE2:6 for c being Real, s being Real_Sequence st s is convergent for r be Real_Sequence st (for i be Nat holds r.i = (s.i-c)*(s.i-c)) holds r is convergent & lim r = (lim s-c)*(lim s-c); theorem :: RSSPACE2:7 for c being Real, s,s1 being Real_Sequence st s is convergent & s1 is convergent for r be Real_Sequence st (for i be Nat holds r.i = (s.i- c)*(s.i-c)+s1.i) holds r is convergent & lim r = (lim s-c)*(lim s-c)+lim s1;