:: Bessel's Inequality
:: by Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura
::
:: Received January 30, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

theorem Th1: :: BHSP_5:1

for D being set
for p1, p2 being FinSequence of D st p1 is one-to-one & p2 is one-to-one & rng p1 = rng p2 holds
( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) )

proof end;

definition

let DX be non empty set ;
let f be BinOp of DX;
assume that
A1: ( f is commutative & f is associative ) and
A2: f is having_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 );

existence
ex b₁ being Element of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₁ = f "**" p )

proof end;

uniqueness
for b₁, b₂ being Element of DX st ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₁ = f "**" p ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₂ = f "**" p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines ++ BHSP_5:def 1 :
for DX being non empty set
for f being BinOp of DX st f is commutative & f is associative & f is having_a_unity holds
for Y being finite Subset of DX
for b₄ being Element of DX holds
( b₄ = f ++ Y iff ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₄ = f "**" p ) );

definition

let X be RealUnitarySpace;
let Y be finite Subset of X;

func setop_SUM (Y,X) -> set equals :: BHSP_5:def 2
the addF of X ++ Y if Y <> {}
otherwise 0. X;

correctness
coherence
( ( Y <> {} implies the addF of X ++ Y is set ) & ( not Y <> {} implies 0. X is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: deftheorem defines setop_SUM BHSP_5:def 2 :
for X being RealUnitarySpace
for Y being finite Subset of X holds
( ( Y <> {} implies setop_SUM (Y,X) = the addF of X ++ Y ) & ( not Y <> {} implies setop_SUM (Y,X) = 0. X ) );

definition

let X be RealUnitarySpace;
let x be Point of X;
let p be FinSequence;
let i be Nat;

func PO (i,p,x) -> set equals :: BHSP_5:def 3
the scalar of X . [x,(p . i)];

correctness
coherence
the scalar of X . [x,(p . i)] is set ;
;

end;

:: deftheorem defines PO BHSP_5:def 3 :
for X being RealUnitarySpace
for x being Point of X
for p being FinSequence
for i being Nat holds PO (i,p,x) = the scalar of X . [x,(p . i)];

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;

correctness
coherence
F * p is FinSequence of DK;
by FINSEQ_2:32;

end;

:: deftheorem defines Func_Seq BHSP_5:def 4 :
for DK, DX being non empty set
for F being Function of DX,DK
for p being FinSequence of DX holds Func_Seq (F,p) = F * p;

definition

let DK, DX be non empty set ;
let f be BinOp of DK;
assume that
A1: ( f is commutative & f is associative ) and
A2: f is having_a_unity ;
let Y be finite Subset of DX;
let F be Function of DX,DK;
A3: dom F = DX by FUNCT_2:def 1;

func setopfunc (Y,DX,DK,F,f) -> Element of DK means :Def5: :: 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)) );

existence
ex b₁ being Element of DK ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₁ = f "**" (Func_Seq (F,p)) )

proof end;

uniqueness
for b₁, b₂ being Element of DK st ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₁ = f "**" (Func_Seq (F,p)) ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₂ = f "**" (Func_Seq (F,p)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines setopfunc BHSP_5:def 5 :
for DK, DX being non empty set
for f being BinOp of DK st f is commutative & f is associative & f is having_a_unity holds
for Y being finite Subset of DX
for F being Function of DX,DK
for b₆ being Element of DK holds
( b₆ = setopfunc (Y,DX,DK,F,f) iff ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₆ = f "**" (Func_Seq (F,p)) ) );

definition

let X be RealUnitarySpace;
let x be Point of 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 being Nat st i in dom q holds
q . i = PO (i,p,x) ) & it = addreal "**" q ) );

existence
ex b₁ being Real 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 being Nat st i in dom q holds
q . i = PO (i,p,x) ) & b₁ = addreal "**" q ) )

proof end;

uniqueness
for b₁, b₂ being Real st 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 being Nat st i in dom q holds
q . i = PO (i,p,x) ) & b₁ = addreal "**" q ) ) & 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 being Nat st i in dom q holds
q . i = PO (i,p,x) ) & b₂ = addreal "**" q ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines setop_xPre_PROD BHSP_5:def 6 :
for X being RealUnitarySpace
for x being Point of X
for Y being finite Subset of X
for b₄ being Real holds
( b₄ = setop_xPre_PROD (x,Y,X) iff 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 being Nat st i in dom q holds
q . i = PO (i,p,x) ) & b₄ = addreal "**" q ) ) );

definition

let X be RealUnitarySpace;
let x be Point of 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 ;

correctness
coherence
( ( Y <> {} implies setop_xPre_PROD (x,Y,X) is Real ) & ( not Y <> {} implies 0 is Real ) );
consistency
for b₁ being Real holds verum;
;

end;

:: deftheorem defines setop_xPROD BHSP_5:def 7 :
for X being RealUnitarySpace
for x being Point of X
for Y being finite Subset of X holds
( ( Y <> {} implies setop_xPROD (x,Y,X) = setop_xPre_PROD (x,Y,X) ) & ( not Y <> {} implies setop_xPROD (x,Y,X) = 0 ) );

definition

let X be RealUnitarySpace;

mode OrthogonalFamily of X -> Subset of X means :Def8: :: BHSP_5:def 8
for x, y being Point of X st x in it & y in it & x <> y holds
x .|. y = 0 ;

existence
ex b₁ being Subset of X st
for x, y being Point of X st x in b₁ & y in b₁ & x <> y holds
x .|. y = 0

proof end;

end;

:: deftheorem Def8 defines OrthogonalFamily BHSP_5:def 8 :
for X being RealUnitarySpace
for b₂ being Subset of X holds
( b₂ is OrthogonalFamily of X iff for x, y being Point of X st x in b₂ & y in b₂ & x <> y holds
x .|. y = 0 );

theorem Th2: :: BHSP_5:2

for X being RealUnitarySpace holds {} is OrthogonalFamily of X

proof end;

registration

let X be RealUnitarySpace;

cluster finite for OrthogonalFamily of X;

existence
ex b₁ being OrthogonalFamily of X st b₁ is finite

proof end;

end;

definition

let X be RealUnitarySpace;

mode OrthonormalFamily of X -> Subset of X means :Def9: :: BHSP_5:def 9
( it is OrthogonalFamily of X & ( for x being Point of X st x in it holds
x .|. x = 1 ) );

existence
ex b₁ being Subset of X st
( b₁ is OrthogonalFamily of X & ( for x being Point of X st x in b₁ holds
x .|. x = 1 ) )

proof end;

end;

:: deftheorem Def9 defines OrthonormalFamily BHSP_5:def 9 :
for X being RealUnitarySpace
for b₂ being Subset of X holds
( b₂ is OrthonormalFamily of X iff ( b₂ is OrthogonalFamily of X & ( for x being Point of X st x in b₂ holds
x .|. x = 1 ) ) );

theorem Th3: :: BHSP_5:3

for X being RealUnitarySpace holds {} is OrthonormalFamily of X

proof end;

registration

let X be RealUnitarySpace;

cluster finite for OrthonormalFamily of X;

existence
ex b₁ being OrthonormalFamily of X st b₁ is finite

proof end;

end;

theorem :: BHSP_5:4

for X being RealUnitarySpace
for x being Point of X holds
( x = 0. X iff for y being Point of X holds x .|. y = 0 )

proof end;

:: parallelogram law

theorem :: BHSP_5:5

for X being RealUnitarySpace
for x, y being Point of X holds (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))

proof end;

:: The Pythagorean theorem

theorem :: BHSP_5:6

for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)

proof end;

theorem Th7: :: BHSP_5:7

for X being RealUnitarySpace
for p being FinSequence of the carrier of X st len p >= 1 & ( for i, j being Nat st i in dom p & j in dom p & i <> j holds
the scalar of X . [(p . i),(p . j)] = 0 ) holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Nat st i in dom q holds
q . i = the scalar of X . [(p . i),(p . i)] ) holds
( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q

proof end;

theorem Th8: :: BHSP_5:8

for X being RealUnitarySpace
for x being Point of X
for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Nat st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( the addF of X "**" p) = addreal "**" q

proof end;

theorem Th9: :: BHSP_5:9

for X being RealUnitarySpace
for S being non empty finite Subset of X
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(F . y1),(F . y2)] = 0 ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))

proof end;

theorem Th10: :: BHSP_5:10

for X being RealUnitarySpace
for x being Point of X
for S being non empty finite Subset of X
for F being Function of the carrier of X, the carrier of X st S c= dom F holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [x,( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))

proof end;

theorem Th11: :: BHSP_5:11

for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)

proof end;

theorem Th12: :: BHSP_5:12

for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)

proof end;

theorem :: BHSP_5:13

for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2

proof end;

theorem :: BHSP_5:14

for DK, DX being non empty set
for f being BinOp of DK st f is commutative & f is associative & f is having_a_unity holds
for Y1, Y2 being finite Subset of DX st Y1 misses Y2 holds
for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being 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)))

proof end;