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



Dear Kawin,

Thanks for providing the additional context. So here are my comments on the conditional expectations:

E[X | Y = _] normally denotes a function that takes an outcome y in the range of the random variable Y and then returns the expectation of the random variable conditioned on Y = y. Now, we can also see consider this function as a measurable function itself, where y contributes its probability P[Y = y] to the expectation E[X | Y = y]. The theory Conditional_Expectation in HOL-Probability formalizes this idea, but the main proof effort is to show that the result is again measurable. As you're working with pmf's, you shouldn't have to worry about measurability. So unless you find some really important lemmas in there, I'd recommend to directly define this as follows:

Let p :: 'a pmf denote the underlying distribution of the joint random experiment. In your case, the distribution over strings (bool list). Further, assume that X and Y are random variables, i.e., X :: 'a => real and Y :: 'a => 'b for some 'b. Then, the conditional expectation is also a random variable given by

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

Note that this is well-defined: cond_pmf requires the set (Y -` {y}) to have positive probability. This holds because y is drawn from "map_pmf Y p". Also note that you could fold the two map_pmf's into one using the equality pmf.map_comp.

In your case, you want to condition on many random variables Z_1, ..., Z_n. Since random variables have the form Z_i = map_pmf Y_i p for some underlying distribution p :: 'a pmf and some function Y_i :: 'a => 'b_i, you can easily combine them into one joint random variable given by Y :: 'a => 'b_1 * 'b_2 * ... * b_n by Y a = (Y_1 a, Y_2 a, ..., Y_n a).

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

Of course, you can't write ... in Isabelle. This would have to be a proper recursive definition, but I hope that it conveys the main idea.

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 to precisely 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 I strongly appreciate your suggestions and will try anyone of them out in case it may make my 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 or less) 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 to formalise:
image.png
I will dig in cond_pmf in no time to try to address this results, but as I don't understand much in details in concept of conditional expectations with many variables conditioned on, it would be very grateful of you if you could guide me or give me a bit of a hint on how to handle this with cond_pmf.

Best regards,
Kawin




On 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





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