# Re: [isabelle] Pmf and measure

Dear Kawin,
> 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?

`There's the function pair_pmf that takes two pmfs and combines them into one. The type is
``as you'd expect:
`
pair_pmf :: 'a pmf => 'b pmf => ('a * 'b) pmf

`So if you write "pair_pmf (bernoulli_pmf p) (bernoulli_pmf q)", the resulting type is
``indeed "(bool * bool) pmf".
`
> 2) Following (1), are there any n-ary to combine n independent pmf's?

`This is getting into applicative functors. The pmf type is a monad (with operations
``return_pmf and bind_pmf) and this is the main workhorse for building more complex
``distribution from basic building blocks. Every monad is also an applicative functor and
``the above pair_pmf is just the product operation of an applicative functor. So you can use
``the standard operations of applicative functors to iterate the construction. The AFP entry
`
https://www.isa-afp.org/entries/Applicative_Lifting.html

`defines some notation and some proof machinery for applicative functors, which also work
``for pmfs. For example, if you have pmfs p1 to p3 and you want to combine their independent
``samples with the function f, then you can write this as
`
return_pmf f ⋄ p1 ⋄ p2 ⋄ p3
where (⋄) denotes the applicative operation ap_pmf on pmfs defined in that AFP entry.
> 3) This one does not directly relate to two questions above. Do we have
> formalisation of sigma-algebra generated by random variable in Isabelle?

`PMFs are discrete distributions, so everything is measurable and their Sigma algebra is
``therefore the powerset. In Isabelle, this is formalized as "count_space". Note that there
``is no formalization of an abstract event space Omega that we (partially) observe through
``the random variables, as is often done in probability theory. A pmf models only the
``projection of Omega to the random variable's output space, but the connection to Omega is
``lost. If you really need to formalize this, you'll probably want to look at the
``formalization of measure theory in HOL-Probability.
`
Hope this helps
Andreas

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