Email Gateway (Aug 22 2022 at 20:44): Email Gateway (Aug 22 2022 at 20:44):From: Kawin Worrasangasilpa <kw448@cam.ac.uk>
Hi,
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?
Regards,
Kawin
Email Gateway (Aug 22 2022 at 20:44):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
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
Email Gateway (Aug 22 2022 at 20:45):From: Manuel Eberl <eberlm@in.tum.de>
Andreas already answered most things, but for an n-ary independent
product of PMFs, the best way (in most cases) is to use the Pi_pmf that
(I think) I sent you last year. I really should put this into the
distribution at some point; I'm not sure why I haven't done that
already. I probably forgot.
Manuel
Pi_pmf.thy
Email Gateway (Aug 22 2022 at 20:45):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Hi Kawin,
for your question (3), the sigma-algebra generated by random variable(s) are not regularly used, but you can easily define it by yourself.
A random variable is nothing but a measurable function f mapping an arbitrary sigma-algebra (sp,sts) to Borel sigma_algebra. So you already have two sigma-algebras. The sigma-algebra generated by that random variable is a set of all PREIMAGEs of points in Borel sets. In HOL4, I defined it in this way:
[sigma_function_def] Definition (in HOL4's martingaleTheory)
⊢ ∀sp A f.
sigma sp A f = (sp,IMAGE (λs. PREIMAGE f s ∩ sp) (subsets A))
If I take f as the random variable, A as (subsets Borel), then I get the sigma-algebra generated by that random variable. This is because PREIMAGE naturally forms a sigma-algebra:
[PREIMAGE_SIGMA_ALGEBRA] Theorem (in HOL4's sigma_algebraTheory)
⊢ ∀sp A f.
sigma_algebra A ∧ f ∈ (sp → space A) ⇒
sigma_algebra (sp,IMAGE (λs. PREIMAGE f s ∩ sp) (subsets A))
Furthermore, there's the concept of "sigma-algebra generated from multiple random variables" (from an index set). (see, e.g., [1, p.52])
[sigma_functions_def] Definition (in HOL's martingaleTheory)
⊢ ∀sp A f J.
sigma sp A f J =
sigma sp
(BIGUNION
(IMAGE
(λi. IMAGE (λs. PREIMAGE (f i) s ∩ sp) (subsets (A i)))
J))
The trick here is, I quote, "although PREIMAGE (f i) s ∩ sp is a sigma-algebra, this is (in general) no longer true for their BIGUNIONs; this explains why we have to use the sigma-hull outside of BIGUNION". [1]
Then I can prove that, the generated sigma-algebra indeed makes all those random variables (i.e. measurable functions) simultaneously measurable in it:
[SIGMA_SIMULTANEOUSLY_MEASURABLE] Theorem (in HOL's martingaleTheory)
⊢ ∀sp A f J.
(∀i. i ∈ J ⇒ sigma_algebra (A i)) ∧
(∀i. f i ∈ (sp → space (A i))) ⇒
∀i. i ∈ J ⇒ f i ∈ measurable (sigma_functions sp A f J) (A i)
These definitions are not commonly needed in the core Probability Theory. I only found some applications in Kolmogorov's 0-1 Law and Martingales.
Hope this helps,
--Chun
[1] Schilling, R.L.: Measures, Integrals and Martingales. Cambridge University Press (2005).
Il 15/10/19 05:40, Kawin Worrasangasilpa ha scritto:
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC