Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Bessel's Inequality

**by****Hiroshi Yamazaki,****Yasunari Shidama, and****Yatsuka Nakamura**- Received January 30, 2003
- MML identifier: BHSP_5

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, BHSP_1, PRE_TOPC, NORMSP_1, RLVECT_1, FUNCT_1, ARYTM_1, FINSET_1, RELAT_1, BHSP_5, BINOP_1, VECTSP_1, PROB_2, FUZZY_2, SQUARE_1, FUNCT_2, FINSEQ_1, SETWISEO, CARD_1, FINSOP_1, DECOMP_1; notation TARSKI, SUBSET_1, XBOOLE_0, NUMBERS, XREAL_0, STRUCT_0, REAL_1, NAT_1, FUNCT_2, FINSET_1, RELAT_1, PRE_TOPC, RLVECT_1, BHSP_1, SQUARE_1, BINOP_1, VECTSP_1, CARD_1, SETWISEO, FUNCT_1, FINSEQ_1, FINSOP_1; constructors REAL_1, NAT_1, BHSP_1, PREPOWER, DOMAIN_1, SQUARE_1, SETWISEO, BINOP_1, VECTSP_1, FINSOP_1, MEMBERED, PARTFUN1; clusters RELSET_1, FINSEQ_1, FUNCT_1, FUNCT_2, FINSET_1, STRUCT_0, MEMBERED, NUMBERS, ORDINAL2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Sum of the result of operation with each element of a set reserve X for RealUnitarySpace; reserve x, y, y1, y2 for Point of X; reserve xd for set; reserve i, j, n for Nat; reserve DX for non empty set; reserve p1, p2 for FinSequence of DX; theorem :: BHSP_5:1 p1 is one-to-one & p2 is one-to-one & rng p1 = rng p2 implies dom p1 = dom p2 & ex P being Permutation of dom p1 st p2 = p1*P & dom P = dom p1 & rng P = dom p1; definition let DX be non empty set; let f be BinOp of DX such that f is commutative associative & f has_a_unity; let Y be finite Subset of DX; func f ++ Y -> Element of DX means :: BHSP_5:def 1 ex p being FinSequence of DX st p is one-to-one & rng p = Y & it = f "**" p; end; definition let X; let Y be finite Subset of X; func setop_SUM(Y,X) equals :: BHSP_5:def 2 (the add of X) ++ Y if Y <> {} otherwise 0.X; end; definition let X, x; let p be FinSequence; let i; func PO(i,p,x) equals :: BHSP_5:def 3 (the scalar of X).[x,p.i]; end; definition let DK, DX be non empty set; let F be Function of DX, DK; let p be FinSequence of DX; func Func_Seq(F,p) -> FinSequence of DK equals :: BHSP_5:def 4 F*p; end; definition let DK, DX be non empty set; let f be BinOp of DK such that f is commutative associative & f has_a_unity; let Y be finite Subset of DX; let F be Function of DX,DK such that Y c= dom F; func setopfunc(Y,DX,DK,F,f) -> Element of DK means :: BHSP_5:def 5 ex p being FinSequence of DX st p is one-to-one & rng p = Y & it = f "**" Func_Seq(F,p); end; definition let X, x; let Y be finite Subset of X; func setop_xPre_PROD(x,Y,X) -> Real means :: BHSP_5:def 6 ex p being FinSequence of the carrier of X st p is one-to-one & rng p = Y & ex q being FinSequence of REAL st dom(q) = dom(p) & (for i st i in dom q holds q.i = PO(i,p,x)) & it = addreal "**" q; end; definition let X, x; let Y be finite Subset of X; func setop_xPROD(x,Y,X) -> Real equals :: BHSP_5:def 7 setop_xPre_PROD(x,Y,X) if Y <> {} otherwise 0; end; begin :: Orthogonal Family & Orthonormal Family definition let X; mode OrthogonalFamily of X -> Subset of X means :: BHSP_5:def 8 for x, y st x in it & y in it & x <> y holds x.|.y = 0; end; theorem :: BHSP_5:2 {} is OrthogonalFamily of X; definition let X; cluster finite OrthogonalFamily of X; end; definition let X; mode OrthonormalFamily of X -> Subset of X means :: BHSP_5:def 9 it is OrthogonalFamily of X & for x st x in it holds x.|.x = 1; end; theorem :: BHSP_5:3 {} is OrthonormalFamily of X; definition let X; cluster finite OrthonormalFamily of X; end; theorem :: BHSP_5:4 x = 0.X iff (for y holds x.|.y = 0); begin :: Bessel's inequality :: parallelogram law theorem :: BHSP_5:5 ||.x+y.||^2 + ||.x-y.||^2 = 2*||.x.||^2 + 2*||.y.||^2; :: The Pythagorean theorem theorem :: BHSP_5:6 x, y are_orthogonal implies ||.x+y.||^2 = ||.x.||^2 + ||.y.||^2; theorem :: BHSP_5:7 for p be FinSequence of the carrier of X st (len p >=1 & for i,j st (i in dom p & j in dom p & i <> j) holds (the scalar of X).[p.i,p.j]=0) for q be FinSequence of REAL st dom p = dom q & (for i st i in dom q holds q.i = (the scalar of X).[(p.i),(p.i)]) holds ((the add of X) "**" p).|. ((the add of X) "**" p) = addreal "**" q; theorem :: BHSP_5:8 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 = (the scalar of X).[x,p.i]) holds x.|.((the add of X) "**" p) = addreal "**" q; theorem :: BHSP_5:9 for S be finite non empty Subset of X for F be Function of the carrier of X, the carrier of X st (S c= dom F & (for y1,y2 st y1 in S & y2 in S & y1 <> y2 holds (the scalar of X).[F.y1,F.y2] = 0)) for H be Function of the carrier of X, REAL st S c= dom H & (for y st y in S holds H.y= (the scalar of X).[F.y,F.y]) for p be FinSequence of the carrier of X st p is one-to-one & rng p = S holds (the scalar of X).[(the add of X) "**" Func_Seq(F,p), (the add of X) "**" Func_Seq(F,p)] = addreal "**" Func_Seq(H,p); theorem :: BHSP_5:10 for S be finite non empty Subset of X for F be Function of the carrier of X, the carrier of X st S c= dom F for H be Function of the carrier of X, REAL st S c= dom H & (for y st y in S holds H.y = (the scalar of X).[x,F.y]) for p be FinSequence of the carrier of X st p is one-to-one & rng p = S holds (the scalar of X).[x,(the add of X) "**" Func_Seq(F,p) ] = addreal "**" Func_Seq(H,p); theorem :: BHSP_5:11 for X st the add of X is commutative associative & the add of X has_a_unity for x for S be finite OrthonormalFamily of X st S is non empty for H be Function of the carrier of X, REAL st S c= dom H & (for y st y in S holds H.y= (x.|.y)^2) for F be Function of the carrier of X, the carrier of X st S c= dom F & (for y st y in S holds F.y = (x.|.y)*y) holds x.|.setopfunc(S, the carrier of X, the carrier of X, F, the add of X) = setopfunc(S, the carrier of X, REAL, H, addreal); theorem :: BHSP_5:12 for X st the add of X is commutative associative & the add of X has_a_unity for x for S be finite OrthonormalFamily of X st S is non empty for F be Function of the carrier of X, the carrier of X st S c= dom F & (for y st y in S holds F.y = (x.|.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= (x.|.y)^2) holds setopfunc(S, the carrier of X, the carrier of X, F, the add of X) .|. setopfunc(S, the carrier of X, the carrier of X, F, the add of X) = setopfunc(S, the carrier of X, REAL, H, addreal); theorem :: BHSP_5:13 for X st the add of X is commutative associative & the add of X has_a_unity for x for S be finite OrthonormalFamily of X st S is non empty for H be Function of the carrier of X, REAL st S c= dom H & (for y st y in S holds H.y = (x.|.y)^2) holds setopfunc(S, the carrier of X, REAL, H, addreal) <= ||.x.||^2; theorem :: BHSP_5:14 for DK, DX be non empty set for f be BinOp of DK st f is commutative associative & f has_a_unity for Y1, Y2 be finite Subset of DX st Y1 misses Y2 for F be Function of DX, DK st Y1 c= dom F & Y2 c= dom F for Z be finite Subset of DX st Z = Y1 \/ Y2 holds setopfunc(Z,DX,DK,F,f) = f.(setopfunc(Y1,DX,DK,F,f), setopfunc(Y2,DX,DK,F,f));

Back to top