:: Bessel's Inequality
:: by Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura
::
:: 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 b1 being Element of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" p )
proof end;
uniqueness
for b1, b2 being Element of DX st ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" p ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b2 = f "**" p ) holds
b1 = b2
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 b4 being Element of DX holds
( b4 = f ++ Y iff ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b4 = 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 b1 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 b1 being Element of DK ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" (Func_Seq (F,p)) )
proof end;
uniqueness
for b1, b2 being Element of DK st ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" (Func_Seq (F,p)) ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b2 = f "**" (Func_Seq (F,p)) ) holds
b1 = b2
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 b6 being Element of DK holds
( b6 = setopfunc (Y,DX,DK,F,f) iff ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b6 = 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 b1 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) ) & b1 = addreal "**" q ) )
proof end;
uniqueness
for b1, b2 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) ) & b1 = 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) ) & b2 = addreal "**" q ) ) holds
b1 = b2
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 b4 being Real holds
( b4 = 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) ) & b4 = 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 b1 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 b1 being Subset of X st
for x, y being Point of X st x in b1 & y in b1 & x <> y holds
x .|. y = 0
proof end;
end;

:: deftheorem Def8 defines OrthogonalFamily BHSP_5:def 8 :
for X being RealUnitarySpace
for b2 being Subset of X holds
( b2 is OrthogonalFamily of X iff for x, y being Point of X st x in b2 & y in b2 & 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;
existence
ex b1 being OrthogonalFamily of X st b1 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 b1 being Subset of X st
( b1 is OrthogonalFamily of X & ( for x being Point of X st x in b1 holds
x .|. x = 1 ) )
proof end;
end;

:: deftheorem Def9 defines OrthonormalFamily BHSP_5:def 9 :
for X being RealUnitarySpace
for b2 being Subset of X holds
( b2 is OrthonormalFamily of X iff ( b2 is OrthogonalFamily of X & ( for x being Point of X st x in b2 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;
existence
ex b1 being OrthonormalFamily of X st b1 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 * ()) + (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 = () + ()
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) <= ^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;