:: Random Variables and Product of Probability Spaces
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 1, 2012
:: Copyright (c) 2012-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, PROB_1, MEASURE1, PARTFUN1, SUBSET_1, TARSKI,
RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0, XXREAL_1, LOPBAN_1, FUNCT_2, DIST_1,
MSSUBFAM, VALUED_0, MESFUNC1, SUPINF_2, FINSEQ_1, NAT_1, CARD_3, CARD_1,
ZFMISC_1, RPR_1, FINSET_1, PROB_4, EQREL_1, RANDOM_1, RANDOM_2, RANDOM_3,
FUNCOP_1, FINANCE1, PBOOLE, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, PBOOLE, ENUMSET1,
FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_1, NAT_1, XREAL_0,
VALUED_0, FINSEQ_1, RPR_1, SUPINF_2, PROB_1, PROB_2, MEASURE1, MEASURE6,
MESFUNC1, PROB_4, MESFUNC6, RANDOM_1, DIST_1, RANDOM_2, FINANCE1;
constructors REAL_1, RPR_1, MESFUNC6, MESFUNC3, DIST_1, MEASURE6, INTEGRA2,
PROB_4, MESFUNC1, RELSET_1, COMSEQ_2, RANDOM_2, FINANCE1, ENUMSET1;
registrations XBOOLE_0, SUBSET_1, NAT_1, XREAL_0, XXREAL_0, ORDINAL1,
MEASURE1, FUNCOP_1, FINANCE1, VALUED_0, FINSEQ_1, FUNCT_2, RELAT_1,
PROB_2, FINSET_1, NUMBERS, PROB_1, PARTFUN1, RELSET_1, CARD_1, PBOOLE,
PRE_CIRC;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Random Variables
reserve Omega, Omega1, Omega2 for non empty set;
reserve Sigma for SigmaField of Omega;
reserve S1 for SigmaField of Omega1;
reserve S2 for SigmaField of Omega2;
theorem :: RANDOM_3:1
for B being non empty set, f being Function holds
f " (union B)
= union the set of all f "Y where Y is Element of B;
theorem :: RANDOM_3:2
for f be Function of Omega1,Omega2,
B be SetSequence of Omega2,
D be SetSequence of Omega1
st for n be Element of NAT holds D.n = f "(B.n) holds
f"(Union B) = Union D;
theorem :: RANDOM_3:3
for f be Function of Omega1,Omega2,
B be SetSequence of Omega2,
D be SetSequence of Omega1
st for n be Element of NAT holds D.n = f "(B.n) holds
f"(Intersection B) = Intersection D;
theorem :: RANDOM_3:4
for F being Function of Omega,REAL,
r being Real
st F is Real-Valued-Random-Variable of Sigma
holds F"(].-infty,r.[) in Sigma;
theorem :: RANDOM_3:5
for F being Function of Omega,REAL st
F is Real-Valued-Random-Variable of Sigma holds
{ x where x is Element of Borel_Sets : F"x is Element of Sigma }
is SigmaField of REAL;
theorem :: RANDOM_3:6
for f being Function of Omega,REAL
st f is Real-Valued-Random-Variable of Sigma holds
{ x where x is Element of Borel_Sets : f"x is Element of Sigma }
= Borel_Sets;
theorem :: RANDOM_3:7
for f being Function of Omega,REAL holds
f is_random_variable_on Sigma, Borel_Sets iff
f is Real-Valued-Random-Variable of Sigma;
theorem :: RANDOM_3:8
for f being Function of Omega,REAL holds
set_of_random_variables_on (Sigma,Borel_Sets) =
Real-Valued-Random-Variables-Set Sigma;
definition
let Omega1, Omega2, S1, S2;
let F be Function of Omega1,Omega2;
attr F is (S1,S2)-random_variable-like means
:: RANDOM_3:def 1
F is_random_variable_on S1,S2;
end;
registration
let Omega1, Omega2, S1, S2;
cluster (S1,S2)-random_variable-like for Function of Omega1, Omega2;
end;
definition
let Omega1, Omega2, S1, S2;
mode random_variable of S1,S2 is
(S1,S2)-random_variable-like Function of Omega1, Omega2;
end;
theorem :: RANDOM_3:9
for f being Function of Omega,REAL holds
f is random_variable of Sigma, Borel_Sets iff
f is Real-Valued-Random-Variable of Sigma;
definition
let F be Function;
attr F is random_variable_family-like means
:: RANDOM_3:def 2
for x be set st x in dom F
ex Omega1, Omega2 be non empty set,
S1 be SigmaField of Omega1, S2 be SigmaField of Omega2,
f be random_variable of S1,S2 st F.x = f;
end;
registration
cluster random_variable_family-like for Function;
end;
definition
mode random_variable_family is random_variable_family-like Function;
end;
reserve F for random_variable of S1,S2;
definition
let Y be non empty set;
let S be SigmaField of Y;
let F be Function;
attr F is S-Measure_valued means
:: RANDOM_3:def 3
for x be set st x in dom F ex M being sigma_Measure of S st F.x = M;
end;
registration
let Y be non empty set;
let S be SigmaField of Y;
cluster S-Measure_valued for Function;
end;
definition
let Y be non empty set;
let S be SigmaField of Y;
let F be Function;
attr F is S-Probability_valued means
:: RANDOM_3:def 4
for x be set st x in dom F ex P be Probability of S st F.x = P;
end;
registration
let Y be non empty set;
let S be SigmaField of Y;
cluster S-Probability_valued for Function;
end;
registration
let X,Y be non empty set;
let S be SigmaField of Y;
cluster X-defined for S-Probability_valued Function;
end;
registration
let X, Y be non empty set;
let S be SigmaField of Y;
cluster total for X-defined S-Probability_valued Function;
end;
registration
let Y be non empty set, S be SigmaField of Y;
cluster S-Probability_valued -> S-Measure_valued for Function;
end;
definition
let Y be non empty set;
let S be SigmaField of Y;
let F be Function;
attr F is S-Random-Variable-Family means
:: RANDOM_3:def 5
for x be set st x in dom F
ex Z be Real-Valued-Random-Variable of S st F.x = Z;
end;
registration
let Y be non empty set;
let S be SigmaField of Y;
cluster S-Random-Variable-Family for Function;
end;
theorem :: RANDOM_3:10
for y being Element of S2 st y <> {} holds
{z where z is Element of Omega1: F.z is Element of y} = F"y;
theorem :: RANDOM_3:11
for F be random_variable of S1,S2 holds
{x where x is Subset of Omega1 : ex y be Element of S2 st x =F"y } c= S1 &
{x where x is Subset of Omega1 : ex y be Element of S2 st x =F"y }
is SigmaField of Omega1;
definition
let Omega1,Omega2,S1,S2;
let M be Measure of S1,
F be random_variable of S1,S2;
func image_measure(F,M) -> Measure of S2 means
:: RANDOM_3:def 6
for y be Element of S2 holds it.y = M.(F"y);
end;
registration
let Omega1,Omega2,S1,S2;
let M be sigma_Measure of S1,
F be random_variable of S1,S2;
cluster image_measure(F,M) -> sigma-additive;
end;
theorem :: RANDOM_3:12
for P being Probability of S1,
F being random_variable of S1,S2 holds
(image_measure(F,P2M(P))).Omega2 = 1;
definition
let Omega1,Omega2,S1,S2;
let P be Probability of S1,
F be random_variable of S1,S2;
func probability(F,P) -> Probability of S2 equals
:: RANDOM_3:def 7
M2P(image_measure(F,P2M(P)));
end;
theorem :: RANDOM_3:13
for P being Probability of S1,
F being random_variable of S1,S2 holds
probability(F,P) = image_measure(F,P2M(P));
theorem :: RANDOM_3:14
for P being Probability of S1,
F be random_variable of S1,S2 holds
for y be set st y in S2 holds (probability(F,P)).y = P.(F"y);
theorem :: RANDOM_3:15
for F be Function of Omega1, Omega2
holds F is random_variable of
Trivial-SigmaField Omega1, Trivial-SigmaField Omega2;
theorem :: RANDOM_3:16
for S be non empty set,
F be non empty FinSequence of S holds
F is random_variable of
Trivial-SigmaField (Seg len F),Trivial-SigmaField (S);
theorem :: RANDOM_3:17
for V,S be finite non empty set,
G be random_variable of Trivial-SigmaField (V),Trivial-SigmaField (S)
holds
for y be set st y in Trivial-SigmaField (S) holds
(probability(G,Trivial-Probability V)).y = card(G"y)/card(V);
theorem :: RANDOM_3:18
for S be finite non empty set,
s be non empty FinSequence of S
holds
ex G be random_variable of
Trivial-SigmaField (Seg len s),Trivial-SigmaField (S)
st G = s &
for x be set st x in S
holds
(probability(G,Trivial-Probability (Seg len s))).{x}
= FDprobability (x,s);
begin :: Product of Probability Spaces
registration
let D be non-empty ManySortedSet of NAT;
let n be Nat;
cluster D.n -> non empty;
end;
definition
let S, F be ManySortedSet of NAT;
attr F is S -SigmaField_sequence-like means
:: RANDOM_3:def 8
for n be Nat holds F.n is SigmaField of S.n;
end;
registration
let S be ManySortedSet of NAT;
cluster S-SigmaField_sequence-like for ManySortedSet of NAT;
end;
definition
let D be ManySortedSet of NAT;
mode SigmaField_sequence of D is
D-SigmaField_sequence-like ManySortedSet of NAT;
end;
definition
let D be ManySortedSet of NAT;
let S be SigmaField_sequence of D;
let n be Nat;
redefine func S.n -> SigmaField of D.n;
end;
definition
let D be non-empty ManySortedSet of NAT;
let S be SigmaField_sequence of D;
let M be ManySortedSet of NAT;
attr M is S-Probability_sequence-like means
:: RANDOM_3:def 9
for n be Nat holds M.n is Probability of S.n;
end;
registration
let D be non-empty ManySortedSet of NAT;
let S be SigmaField_sequence of D;
cluster S-Probability_sequence-like for ManySortedSet of NAT;
end;
definition
let D be non-empty ManySortedSet of NAT;
let S be SigmaField_sequence of D;
mode Probability_sequence of S is
S-Probability_sequence-like ManySortedSet of NAT;
end;
definition
let D be non-empty ManySortedSet of NAT;
let S be SigmaField_sequence of D;
let P be Probability_sequence of S;
let n be Nat;
redefine func P.n -> Probability of (S.n);
end;
definition
let D be ManySortedSet of NAT;
func Product_dom(D) -> ManySortedSet of NAT means
:: RANDOM_3:def 10
it.0 = D.0 & for i be Nat holds it.(i+1) = [:it.i, D.(i+1) :];
end;
theorem :: RANDOM_3:19
for D be ManySortedSet of NAT holds
(Product_dom(D)).0 = D.0 &
(Product_dom(D)).1 = [:D.0,D.1:] &
(Product_dom(D)).2 = [:D.0,D.1,D.2:] &
(Product_dom(D)).3 = [:D.0,D.1,D.2,D.3:];
registration
let D be non-empty ManySortedSet of NAT;
cluster Product_dom(D) -> non-empty;
end;
registration
let D be finite-yielding ManySortedSet of NAT;
cluster Product_dom(D) -> finite-yielding;
end;
definition
let Omega,Sigma;
let P be set;
assume P is Probability of Sigma;
func modetrans(P,Sigma) -> Probability of Sigma equals
:: RANDOM_3:def 11
P;
end;
definition
let D be finite-yielding non-empty ManySortedSet of NAT;
func Trivial-SigmaField_sequence(D) -> SigmaField_sequence of D means
:: RANDOM_3:def 12
for n be Nat holds it.n = Trivial-SigmaField (D.n);
end;
definition
let D be finite-yielding non-empty ManySortedSet of NAT;
let P be Probability_sequence of Trivial-SigmaField_sequence(D);
let n be Nat;
redefine func P.n -> Probability of Trivial-SigmaField(D.n);
end;
definition
let D be finite-yielding non-empty ManySortedSet of NAT;
let P be Probability_sequence of Trivial-SigmaField_sequence(D);
func Product-Probability(P,D) -> ManySortedSet of NAT means
:: RANDOM_3:def 13
it.0 = P.0 & for i be Nat holds
it.(i+1) = Product-Probability
( (Product_dom(D)).i,D.(i+1),
modetrans(it.i,Trivial-SigmaField ((Product_dom(D)).i)), P.(i+1));
end;
theorem :: RANDOM_3:20
for D be finite-yielding non-empty ManySortedSet of NAT,
P be Probability_sequence of Trivial-SigmaField_sequence(D),
n be Nat holds
Product-Probability(P,D).n is
Probability of Trivial-SigmaField ((Product_dom(D)).n);
theorem :: RANDOM_3:21
for D be finite-yielding non-empty ManySortedSet of NAT,
P be Probability_sequence of Trivial-SigmaField_sequence(D),
n be Nat holds
ex Pn be Probability of Trivial-SigmaField ((Product_dom(D)).n)
st Pn = Product-Probability(P,D).n
& Product-Probability(P,D).(n+1)
= Product-Probability ( (Product_dom(D)).n,D.(n+1),Pn,P.(n+1));
theorem :: RANDOM_3:22
for D be finite-yielding non-empty ManySortedSet of NAT,
P be Probability_sequence of Trivial-SigmaField_sequence(D) holds
Product-Probability(P,D).0 = P.0 &
Product-Probability(P,D).1 =
Product-Probability(D.0,D.1,P.0,P.1) &
(ex P1 be Probability of Trivial-SigmaField ([:D.0,D.1:]) st
P1 = Product-Probability(P,D).1 &
Product-Probability(P,D).2 =
Product-Probability([:D.0,D.1:],D.2,P1,P.2) ) &
(ex P2 be Probability of Trivial-SigmaField ([:D.0,D.1,D.2:]) st
P2 = Product-Probability(P,D).2 &
Product-Probability(P,D).3 =
Product-Probability([:D.0,D.1,D.2:],D.3,P2,P.3)) &
(ex P3 be Probability of Trivial-SigmaField ([:D.0,D.1,D.2,D.3:]) st
P3 = Product-Probability(P,D).3 &
Product-Probability(P,D).4 =
Product-Probability([:D.0,D.1,D.2,D.3:],D.4,P3,P.4));