begin
theorem Th1:
:: deftheorem defines ++ BHSP_5:def 1 :
:: deftheorem defines setop_SUM BHSP_5:def 2 :
:: deftheorem defines PO BHSP_5:def 3 :
:: deftheorem defines Func_Seq BHSP_5:def 4 :
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;
assume A3:
Y c= dom F
;
func setopfunc Y,
DX,
DK,
F,
f -> Element of
DK means :
Def5:
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) )
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
end;
:: deftheorem Def5 defines setopfunc BHSP_5:def 5 :
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
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
Element of
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 Element of NAT st i in dom q holds
q . i = PO i,p,x ) & b1 = addreal "**" q ) )
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 Element of 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 Element of NAT st i in dom q holds
q . i = PO i,p,x ) & b2 = addreal "**" q ) ) holds
b1 = b2
end;
:: deftheorem defines setop_xPre_PROD BHSP_5:def 6 :
:: deftheorem defines setop_xPROD BHSP_5:def 7 :
begin
:: deftheorem Def8 defines OrthogonalFamily BHSP_5:def 8 :
theorem Th2:
:: deftheorem Def9 defines OrthonormalFamily BHSP_5:def 9 :
theorem Th3:
theorem
begin
theorem
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
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
theorem Th12:
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
theorem
theorem
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)