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.