Re: [isabelle] Pmf and measure



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:
> 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
> 

Attachment: signature.asc
Description: OpenPGP digital signature



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