*To*: Kawin Worrasangasilpa <kw448 at cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] (Super-)Martingale and conditional expectation*From*: Andreas Lochbihler <mail at andreas-lochbihler.de>*Date*: Mon, 28 Oct 2019 19:24:40 +0100*In-reply-to*: <CAGn19Sx-eLdeek3Y0Pz8v0BuFa7W9anvfyDgWkEBjtSksCsxPA@mail.gmail.com>*References*: <CAGn19Sx-eLdeek3Y0Pz8v0BuFa7W9anvfyDgWkEBjtSksCsxPA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.9.0

Dear Kawin, First a few general hints:

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)"

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 probabilityproofs and the hardest part is to formlise some conditional expectation and probabilityequations and inequalities (to finally define (super)martingales). I have usedProbability_Mass_Function.thy to formalise random variables I need in 'a pmf function formwhich 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 conditionalexpectation on those random variables. So I would like to know if there is a simple or anefficient 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 arejust 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.pngso I have it formalised as Φ_n_pmf' as follows, (I drop details of rev_m as not necessaryhere)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.pngI tried to dig in Conditional_Expectation.thy, but could not see how to fomalise this yetwhile it took some time already, so I wonder if anyone has ever used it to formalisesimilar results?Regards, Kawin

**References**:**[isabelle] (Super-)Martingale and conditional expectation***From:*Kawin Worrasangasilpa

- Previous by Date: Re: [isabelle] Unfortunate duplicate name
- Next by Date: Re: [isabelle] A small proof checker (String => Bool)
- Previous by Thread: [isabelle] (Super-)Martingale and conditional expectation
- Next by Thread: Re: [isabelle] (Super-)Martingale and conditional expectation
- 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