*To*: Kawin Worrasangasilpa <kw448 at cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] On random variables, dependencies and their expectations*From*: Andreas Lochbihler <mail at andreas-lochbihler.de>*Date*: Thu, 21 Jun 2018 20:38:52 +0200*In-reply-to*: <CAGn19SyRQG4hak1rSdSk=Kay3q60ZQ6KJnizZv7wfEyiMK90vg@mail.gmail.com>*References*: <CAGn19SyRQG4hak1rSdSk=Kay3q60ZQ6KJnizZv7wfEyiMK90vg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Dear Kawin,

fun w_list_pmf :: "nat => bool list pmf" where "w_list_pmf 0 = return_pmf []" | "w_list_pmf n = bind_pmf (w_list_pmf (n - 1)) (%xs. bind_pmf (bernoulli_pmf *(1 - e) / 2)) (%x. return_pmf (x # xs)))" You can also define the function Δ_n using monadic programming: definition Δ_n where "Δ_n n = bind_pmf (w_list_pmf (n + 1)) (%xs. return_pmf (f xs - f (tl xs)))"

Hope this helps, Andreas Am 21.06.2018 um 01:53 schrieb Kawin Worrasangasilpa:

Hi, I have been trying to deal with random variables in Isabelle/HOL for some time and I still can't find out how to deal with them exactly. I found in "HOL/Probability/Probability_Mass_Function.thy" on how to define an " 'a pmf " value briefly. For example, I could use map_pmf to change to different space: context fixes ε :: real begin definition w_n :: "nat pmf" where "w_n = map_pmf (λb. (if b then 1 else 0)) (bernoulli_pmf ((1-ε)/2))" (*this is to change from {True, False} to {1, 0}*) definition W_n :: "int pmf" where "W_n = map_pmf (λb. (-1) ^ (if b then 0 else 1)) (bernoulli_pmf ((1-ε)/2))" (*this is to change from {True, False} to {1, -1}*) or use lift_definition: lift_definition w_list_pmf :: "nat ⇒ bool list pmf" is "λn (l::bool list). if size l = n then (((1-ε)/2)^(count (mset l) True))*((1+ε/2)^(count (mset l) False)) else 0" (*this is to have a bool list random variable of fixed length and all members are independent Bernoulli random variables with p = (1-ε)/2*) But when it becomes more complicated and the random variables are dependent I have no idea how to phrase it. For example, Let us say I have a sequence of random variables Φ_i = f (w_1w_2...w_i) (all w_i are independent Bernoulli random variables), and then construct Δ_i = Φ_i - Φ_(i-1). The complication, in this case, is Φ_i = f (w_1w_2...w_i) and Φ_(i-1) f (w_1w_2...w_(i-1)) use the same w_t sequence which are w_1,w_2,...,w_(i-1), but the first Φ also uses w_i for the last element in the list. So, I tried, lift_definition w_list_pmf :: "nat ⇒ bool list pmf" is "λn (l::bool list). if size l = n then (((1-ε)/2)^(count (mset l) True))*((1+ε/2)^(count (mset l) False)) else 0" sorry definition Φ_n :: "nat ⇒ real pmf" where "Φ_n n = map_pmf (λl. f l) (w_list_pmf n)" (*with f being any function in "bool list => real" and "n" is the lenth of the input list*) definition Δ_n :: "nat ⇒ real pmf" where "Δ_n n = map_pmf (λp. fst p - snd p) (pair_pmf (Φ_n n) (Φ_n (n -1)))", But I guess this makes (Φ_n n) and (Φ_n(n-1)) completely independent which is not what I want since they use common random variables in their generating process: w_1,w_2,...,w_(i-1). So I realised that these constants of " 'a pmf" type are not supposed to be used as random variables but distribution (please correct me on this). Also, I would like to calculate these random variables' expectation, for which I tried lemma "n > 0 ⟶ prob_space.expectation (Δ_n n) (id) < -ε" sorry ,and felt really doubtful of the existence of the function "id" since if "Δ_n n" could be used as a random variable, it wouldn't need any function to be involved in calculating the expectation. Could I ask whether there are any better ways or repositories I should check to sort out this random variables issue and their expectations? Thanks, Kawin

**References**:**[isabelle] On random variables, dependencies and their expectations***From:*Kawin Worrasangasilpa

- Previous by Date: Re: [isabelle] datatype_compat in Isabelle2018-RC0
- Next by Date: Re: [isabelle] datatype_compat in Isabelle2018-RC0
- Previous by Thread: [isabelle] On random variables, dependencies and their expectations
- Next by Thread: [isabelle] 1/0 = 0
- Cl-isabelle-users June 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list