environ
vocabularies HIDDEN, FUNCT_1, COMPLEX1, RELAT_1, ZFMISC_1, XXREAL_0, PARTFUN1, ARYTM_1, XBOOLE_0, ORDINAL4, INT_1, SQUARE_1, ARYTM_3, RLVECT_1, SUPINF_2, RSSPACE, FUNCOP_1, FINSOP_1, NAT_1, FUNCT_4, BINOP_2, PROB_1, MEASURE6, MESFUNC1, TARSKI, MESFUNC5, IDEAL_1, SUBSET_1, RANDOM_1, RANDOM_2, C0SP1, FINSET_1, FINSEQ_1, ORDINAL2, RPR_1, CARD_1, SEQ_2, POWER, FUNCT_3, PROB_4, UPROOTS, FINSEQ_2, CARD_3, FUNCT_2, RFINSEQ, FUNCSDOM, POLYALG1, BHSP_5, NUMBERS, REAL_1, INTEGRA5, VALUED_1, EQREL_1, XCMPLX_0, SUPINF_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, FINSEQ_1, ORDINAL1, REAL_1, CARD_1, FINSET_1, NUMBERS, SUPINF_1, XXREAL_0, XCMPLX_0, COMPLEX1, XREAL_0, SUPINF_2, VALUED_0, VALUED_1, FINSEQ_2, NAT_D, RFINSEQ, FINSOP_1, STRUCT_0, IDEAL_1, BINOP_1, BINOP_2, RLVECT_1, FUNCSDOM, SEQ_2, SQUARE_1, GROUP_1, POWER, PROB_1, PROB_4, EXTREAL1, MESFUNC1, MEASURE6, MESFUNC5, MESFUNC6, MESFUNC2, RVSUM_1, UPROOTS, MESFUN6C, C0SP1, RANDOM_1, BHSP_5;
definitions TARSKI, RLVECT_1;
theorems FUNCT_1, FUNCT_2, PARTFUN1, COMPLEX1, XBOOLE_0, TARSKI, RELAT_1, VALUED_1, IDEAL_1, ZFMISC_1, RLVECT_1, FUNCOP_1, XBOOLE_1, MESFUNC2, EXTREAL1, MEASURE1, MESFUNC6, PROB_1, XXREAL_0, ABSVALUE, MESFUNC7, RELSET_1, XXREAL_3, XREAL_0, RANDOM_1, C0SP1, FINSEQ_4, POWER, BINOP_2, RFINSEQ, CARD_2, FINSEQ_1, FUNCT_4, FINSOP_1, NAT_1, NAT_2, NAT_D, XREAL_1, SQUARE_1, FINSEQ_2, INT_1, FUNCT_3, CARD_1, FINSEQ_3, FINSEQ_5, MESFUN6C, FUNCSDOM, BHSP_5, RVSUM_1, FIB_NUM3, SUBSET, XTUPLE_0, ORDINAL1, NUMBERS;
schemes FINSEQ_1, FUNCT_2, NAT_1, FUNCT_3;
registrations XBOOLE_0, ORDINAL1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, NAT_1, SUBSET_1, XCMPLX_0, XXREAL_0, MEASURE1, FINSEQ_1, RELAT_1, XXREAL_3, C0SP1, FUNCT_2, CARD_1, FINSET_1, BINOP_2, FUNCT_1, MESFUN6C, FUNCSDOM, RELSET_1, SQUARE_1, INT_1;
constructors HIDDEN, EXTREAL1, REAL_1, IDEAL_1, MEASURE6, MESFUNC2, MESFUNC5, MESFUNC6, SUPINF_1, REALSET1, RVSUM_1, MESFUNC1, RELSET_1, RANDOM_1, C0SP1, RFINSEQ, POWER, FINSOP_1, BINARITH, FINSEQOP, SETWISEO, PROB_4, WELLORD2, SQUARE_1, NAT_D, UPROOTS, MESFUN6C, BHSP_5, COMSEQ_2, BINOP_2, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, MESFUNC5, FINSEQ_2, FINSEQ_1, PROB_4, FUNCSDOM, VALUED_1, BHSP_5, RVSUM_1, SQUARE_1, CARD_1, ORDINAL1;
expansions TARSKI, FINSEQ_1;
definition
let Omega be non
empty set ;
let Sigma be
SigmaField of
Omega;
let P be
Probability of
Sigma;
let X be
Real-Valued-Random-Variable of
Sigma;
assume A1:
(
X is_integrable_on P &
(abs X) to_power 2
is_integrable_on P2M P )
;
correctness
existence
ex b1 being Real ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b1 = Integral ((P2M P),((abs Y) to_power 2)) );
uniqueness
for b1, b2 being Real st ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b1 = Integral ((P2M P),((abs Y) to_power 2)) ) & ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b2 = Integral ((P2M P),((abs Y) to_power 2)) ) holds
b1 = b2;
end;
Lm1:
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2 ex Q being Function of [:Omega1,Omega2:],REAL st
for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y})
Lm2:
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q1, Q2 being Function of [:Omega1,Omega2:],REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) holds
Q1 = Q2
Lm3:
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
Lm4:
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P1 = P2
Lm5:
for DK, DX being non empty set
for F being Function of DX,DK
for p, q being FinSequence of DX
for fp, fq being FinSequence of DK st fp = F * p & fq = F * q holds
F * (p ^ q) = fp ^ fq
Lm6:
for p being Function st dom p = Seg 1 holds
p = <*(p . 1)*>
theorem Th11:
for
DX1,
DX2 being non
empty set for
F1 being
Function of
DX1,
REAL for
F2 being
Function of
DX2,
REAL for
G being
Function of
[:DX1,DX2:],
REAL for
Y1 being non
empty finite Subset of
DX1 for
p1 being
FinSequence of
DX1 st
p1 is
one-to-one &
rng p1 = Y1 holds
for
p2 being
FinSequence of
DX2 for
p3 being
FinSequence of
[:DX1,DX2:] for
Y2 being non
empty finite Subset of
DX2 for
Y3 being
finite Subset of
[:DX1,DX2:] st
p2 is
one-to-one &
rng p2 = Y2 &
p3 is
one-to-one &
rng p3 = Y3 &
Y3 = [:Y1,Y2:] & ( for
x,
y being
set st
x in Y1 &
y in Y2 holds
G . (
x,
y)
= (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
theorem Th12:
for
DX1,
DX2 being non
empty set for
F1 being
Function of
DX1,
REAL for
F2 being
Function of
DX2,
REAL for
G being
Function of
[:DX1,DX2:],
REAL for
Y1 being non
empty finite Subset of
DX1 for
Y2 being non
empty finite Subset of
DX2 for
Y3 being
finite Subset of
[:DX1,DX2:] st
Y3 = [:Y1,Y2:] & ( for
x,
y being
set st
x in Y1 &
y in Y2 holds
G . (
x,
y)
= (F1 . x) * (F2 . y) ) holds
setopfunc (
Y3,
[:DX1,DX2:],
REAL,
G,
addreal)
= (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))
theorem Th14:
for
DX being non
empty set for
F being
Function of
DX,
REAL for
Y1,
Y2 being
finite Subset of
DX st
Y1 c= Y2 & ( for
x being
set st
x in Y2 holds
0 <= F . x ) holds
setopfunc (
Y1,
DX,
REAL,
F,
addreal)
<= setopfunc (
Y2,
DX,
REAL,
F,
addreal)
reconsider jj = 1 as R_eal by XXREAL_0:def 1;
Lm7:
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
Lm8:
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
Lm9:
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
definition
let Omega1,
Omega2 be non
empty finite set ;
let P1 be
Probability of
Trivial-SigmaField Omega1;
let P2 be
Probability of
Trivial-SigmaField Omega2;
func Product-Probability (
Omega1,
Omega2,
P1,
P2)
-> Probability of
Trivial-SigmaField [:Omega1,Omega2:] means :
Def2:
ex
Q being
Function of
[:Omega1,Omega2:],
REAL st
( ( for
x,
y being
set st
x in Omega1 &
y in Omega2 holds
Q . (
x,
y)
= (P1 . {x}) * (P2 . {y}) ) & ( for
z being
finite Subset of
[:Omega1,Omega2:] holds
it . z = setopfunc (
z,
[:Omega1,Omega2:],
REAL,
Q,
addreal) ) );
existence
ex b1 being Probability of Trivial-SigmaField [:Omega1,Omega2:] ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) )
uniqueness
for b1, b2 being Probability of Trivial-SigmaField [:Omega1,Omega2:] st ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) & ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) holds
b1 = b2
end;
::
deftheorem Def2 defines
Product-Probability RANDOM_2:def 2 :
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for b5 being Probability of Trivial-SigmaField [:Omega1,Omega2:] holds
( b5 = Product-Probability (Omega1,Omega2,P1,P2) iff ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b5 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) );
Lm10:
for Omega being non empty set
for Sigma being SigmaField of Omega holds
( Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed & Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed )
definition
let Omega be non
empty set ;
let Sigma be
SigmaField of
Omega;
func R_Algebra_of_Real-Valued-Random-Variables Sigma -> Algebra equals
AlgebraStr(#
(Real-Valued-Random-Variables-Set Sigma),
(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),
(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),
(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),
(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),
(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #);
coherence
AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #) is Algebra
by C0SP1:6;
end;
::
deftheorem defines
R_Algebra_of_Real-Valued-Random-Variables RANDOM_2:def 4 :
for Omega being non empty set
for Sigma being SigmaField of Omega holds R_Algebra_of_Real-Valued-Random-Variables Sigma = AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #);