*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] (Super-)Martingale and conditional expectation*From*: Andreas Lochbihler <mail at andreas-lochbihler.de>*Date*: Tue, 29 Oct 2019 20:11:23 +0100*In-reply-to*: <1e7e6466-afb6-64a4-7244-94c1905d91c2@andreas-lochbihler.de>*References*: <1e7e6466-afb6-64a4-7244-94c1905d91c2@andreas-lochbihler.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.9.0

Dear Kawin,

definition cond_exp_pmf :: "'a pmf ⇒ ('a ⇒ real) ⇒ ('a ⇒ 'b) ⇒ real pmf" where "cond_exp_pmf p X Y = map_pmf (λy. measure_pmf.expectation (cond_pmf p (Y -` {y})) X) (map_pmf Y p)"

So E[Phi_t+1 | Phi_1, ..., Phi_t] in your notation would be something like cond_exp_pmf (w_pmf (t + 1)) (Phi_n' (t + 1)) (%w. (Phi_n' 0 w, Phi_n' 1 w, ..., Phi_n' t w))

Best, Andreas On 29/10/2019 07:11, Kawin Worrasangasilpa wrote:

Dear Andreas,Thank you very greatly for your email, I think I might have given you too little toprecisely state what I have done so far and what it is left of me to formalise.I did almost everything you suggested already; there are some differences in style which Istrongly appreciate your suggestions and will try anyone of them out in case it may makemy proof cleaner.However, what I am stuck with is the last bits of the paper about conditional expectation.(For reference: this is the theory file I have formalised the paper up until now (more orless) https://bitbucket.org/wkawin/ouroboros/src/master/Forkable_Strings_Are_Rare.thy)So my biggest issue now is this line of equations/inequalities in the paper that I need toformalise:image.pngI will dig in cond_pmf in no time to try to address this results, but as I don'tunderstand much in details in concept of conditional expectations with many variablesconditioned on, it would be very grateful of you if you could guide me or give me a bit ofa hint on how to handle this with cond_pmf.Best regards, KawinOn Mon, Oct 28, 2019 at 6:24 PM Andreas Lochbihler <mail at andreas-lochbihler.de<mailto:mail at andreas-lochbihler.de>> wrote:Dear Kawin, First a few general hints: 1. There's the function cond_pmf that gives you the conditional distribution of a probability mass function. 2. measure_pmf converts a pmf into a measure space where everything is measurable and events have the right probability. So you can use measure_pmf.expectation to talk about the expectation of a pmf. I've had a quick look at the attached paper and I noticed that most definitions and proofs are somewhat recursive over the length of the bitstring, in particular the margins. So IMO it would make sense to mimick this recursion in the definitions, say like this: fun wn :: "nat => bool list pmf" where "wn 0 = return_pmf []" | "wn (Suc n) = map_pmf (#) (pair_pmf (bernoulli_pmf ((1-ε)/2)) (wn n))" You can then define the generalized margin functions also by recursion: fun l :: "bool list => int" and m :: "bool list => int" where "l [] = 0" | "m [] = 0" | "l (True # w) = l w + 1" | "m (True # w) = m w + 1" | "l (False # w) = (if l w > m w & m w = 0 then l w - 1 else if l w = 0 then 0 else l w - 1)" | "m (False # w) = (if l w > m w & m w = 0 then 0 else m w - 1)" Note that I am looking always at the character at the front rather than the back. So what I've formalized is actually the margin of the reversed word. But for the purpose of the analysis, this should not matter. So you get the random variable definition Phi :: "bool list => real" where "Phi w = real_of_int (l w) + alpha * real_of_int (min 0 (m w))" I would not even define this as a probability distribution and instead always reason about "map_pmf Phi (wn ...)" explicitly. Then, you can express something like Delta_{t+1} as "map_pmf (%w. Phi w - Phi (tl w)) (wn (t+1))" I hope this helps a bit, Andreas On 28/10/2019 10:15, Kawin Worrasangasilpa wrote: > Hi, > > I need to formalise some big results (see bound 1 in the attachment) regarding probability > proofs and the hardest part is to formlise some conditional expectation and probability > equations and inequalities (to finally define (super)martingales). I have used > Probability_Mass_Function.thy to formalise random variables I need in 'a pmf function form > which is to define a measure space then use them with functions to build random variables. > However, I now get stuck and do not know how to proceed next to get conditional > expectation on those random variables. So I would like to know if there is a simple or an > efficient way to get conditional expectation formalised from what I have? > > In more detail, from this two paragraphs (in full in attachement), and \lamda and \mu are > just function directly define recursively on any member of {0,1}*, > image.png > I define n cion-tossings in two ways: > (*first way*) > definition w_n_pmf :: "nat pmf" where > "w_n_pmf = map_pmf (λb. (if b then 1 else 0)) (bernoulli_pmf ((1-ε)/2))" > > (*second way*) > definition Pi_pmf :: "'a set ⇒ 'b ⇒ ('a ⇒ 'b pmf) ⇒ ('a ⇒ 'b) pmf" where > "Pi_pmf A dflt p = > embed_pmf (λf. if (∀x. x ∉ A ⟶ f x = dflt) then ∏x∈A. pmf (p x) (f x) else 0)" > (*this is not my definition it is from Manuel Eberl's unpuplished work Pi_pmf.thy*) > > definition w_i_pmf :: "nat ⇒ (nat ⇒ bool) pmf" where "w_i_pmf n = Pi_pmf {..<n} False (λ_. > bernoulli_pmf ((1-ε)/2))" > > definition w_pmf where "w_pmf n = map_pmf (λf. map f [0..<n]) (w_i_pmf n)" > > then define > image.png > so I have it formalised as Φ_n_pmf' as follows, (I drop details of rev_m as not necessary > here) > > definition Φ_n' :: "nat ⇒ bool list ⇒ real" where > "Φ_n' n l= (λp. real_of_int (fst p) + α * (real_of_int (min 0 (snd p)))) (rev_m (drop > (size l - n) l)) + n * ε" > > definition Φ_n_pmf' where > "Φ_n_pmf' n = map_pmf (λx. Φ_n' n x) (w_pmf n)" > > So as you can see here I picked my second version of n coin-tossings to formalise Φ_n_pmf'. > > Final result I need to formalise is > image.png > I tried to dig in Conditional_Expectation.thy, but could not see how to fomalise this yet > while it took some time already, so I wonder if anyone has ever used it to formalise > similar results? > > Regards, > Kawin

- Previous by Date: [isabelle] Isabelle under NetBSD Linux emulation
- Next by Date: [isabelle] Cannot update finished theory
- Previous by Thread: Re: [isabelle] (Super-)Martingale and conditional expectation
- Next by Thread: [isabelle] Isabelle under NetBSD Linux emulation
- Cl-isabelle-users October 2019 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