*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] On random variables, dependencies and their expectations*From*: Kawin Worrasangasilpa <kw448 at cam.ac.uk>*Date*: Thu, 21 Jun 2018 00:53:31 +0100

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

**Follow-Ups**:**Re: [isabelle] On random variables, dependencies and their expectations***From:*Andreas Lochbihler

- Previous by Date: [isabelle] 1/0=0
- Next by Date: Re: [isabelle] make_string
- Previous by Thread: Re: [isabelle] 1/0=0
- Next by Thread: Re: [isabelle] On random variables, dependencies and their expectations
- 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