*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] (Super-)Martingale and conditional expectation*From*: Kawin Worrasangasilpa <kw448 at cam.ac.uk>*Date*: Mon, 28 Oct 2019 09:15:40 +0000

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}*,

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

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

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 * ε"

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

"Φ_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

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

**Attachment:
Forkable String are Rare.pdf**

**Follow-Ups**:**Re: [isabelle] (Super-)Martingale and conditional expectation***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Quoted parameters to interpretation in LaTeX output
- Next by Date: Re: [isabelle] Unfortunate duplicate name
- Previous by Thread: Re: [isabelle] Quoted parameters to interpretation in LaTeX output
- 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