Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

Bessel's Inequality

by
Hiroshi Yamazaki,
Yasunari Shidama, and
Yatsuka Nakamura

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)

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])

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)]

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) ]

theorem :: BHSP_5:11
for X st the add of X is commutative associative &
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 &
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));
```