[isabelle] Pmf and measure


I have recently had to deal with probability in Isabelle but mostly I have
been doing it through Probability_Mass_Function.thy. So I would like to ask
about some facilities we have on “ 'a pmf".
I know how to use some pre-constructed pmf such as
bernoulli_pmf p :: bool pmf
as a coin tossing in a way that pmf (bernoulli_pmf p) True = p and  pmf
(bernoulli_pmf p) False = 1 - p,  when p is incusively between 0 and 1.
1) How can we define two independent, for example, coins tossing, as one
function of type " 'a pmf"? Is there any function built in Isabelle already
that can make this kind of product just from bernoulli_pmf? What would the
type of this product be, should it be (bool x bool) pmf for 2 bernoulli_pmf
for example?

2) Following (1), are there any n-ary to combine n independent pmf's?

3) This one does not directly relate to two questions above. Do we have
formalisation of sigma-algebra generated by random variable in Isabelle?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.