[isabelle] (Super-)Martingale and conditional expectation


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

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

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 
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?


Attachment: Forkable String are Rare.pdf
Description: Adobe PDF document

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.