Re: [isabelle] (Super-)Martingale and conditional expectation

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,

On 28/10/2019 10:15, Kawin Worrasangasilpa wrote:

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?


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