Email Gateway (Aug 22 2022 at 20:50): Email Gateway (Aug 22 2022 at 20:50):From: Kawin Worrasangasilpa <kw448@cam.ac.uk>
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: 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: 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: 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
image.png
image.png
image.png
Forkable String are Rare.pdf
Email Gateway (Aug 22 2022 at 20:50):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Kawin,
First a few general hints:
There's the function cond_pmf that gives you the conditional distribution of a
probability mass function.
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
Email Gateway (Aug 22 2022 at 20:51):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
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
Last updated: Nov 21 2024 at 12:39 UTC