Re: [isabelle] Pmf and measure
> 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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and