Can anyone point me towards some good examples for conditional probability lemmas? I've found some very minimal stuff in the main library, and a little in AFP entries on Markov and CryptHOL, but not much else. I couldn't even find Bayes theorem after searching (though that was very easy to formalise myself!). Would be great to know if my searches missed anything!

Judging from the hits grepping for `cond_prob`

turns up it seems likely that you found all that there is. It does not seem to be used much and there isn't really a big library of facts for it. The conditional expectation, `cond_exp`

is used much more.

Conditional expectation is defined in a very general way though. My paltry knowledge of probability theory is not enough to really understand all that is going on there.

In principle it should also be possible to condition a probability space, i.e. not just define "in the probability space M, what is the probability of event X under the precondition that event Y occurs" but "derive from M a new probability space M' with the additional precondition that the event X holds"

If X is an even with non-zero probability that gives us a new probability space M' with measure M' Y = measure M Y / measure M X.

Not sure if something like this exists already and whether it's useful (probably?).

I am a bit puzzled that the Markov Chain development in the AFP doesn't seem to mention conditional probability at all (even though it is a crucial ingredient in the standard definition of a Markov Chain).

My suspicion is that this is because the Markov Chain library doesn't talk about a sequence of random variables of results (which is the usual way to present it) but rather a single distribution over streams of results. And the σ-algebra (i.e. the measurable sets) are probably defined in such a way that memorylessness is already encoded in the measurable sets.

This is the sort of thing that Johannes Hölzl would probably be able to explain, but I fear he will probably not respond to emails if you ask him (he was among those poor souls swallowed up by the black hole that is Apple Munich).

Sébastien Gouëzel is an expert on this advanced probability theory stuff (he did all the ergodic theory/conditional expectation stuff) and he always replies to emails in a very helpful and quick manner, so it might be useful to contact him if you're planning to do something ambitious in the realm of probability in Isabelle.

Thanks for checking! My knowledge of probability theory is generally just enough to scrape by when using it, so I wasn't sure if I was missing something. I was similarly surprised by the lack of use of the definition, particularly in things such as markov chains, your suspicions there seem accurate though. I found a few extra things searching for cond_pmf, and there is also this useful lemma "measure_uniform_measure_eq_cond_prob" which I think roughly does something along the lines of conditioning a probability space already. I'm mostly looking at the probabilistic method in the space of combinatorics which I've done a bit of now over the last 6 months. This last proof is the first time I feel like I'm testing our existing formalisations a little - but hopefully it's not too ambitious! Thanks for the recommendations re people to talk to - will keep that in mind.

@Chelsea Edmonds

I also searched lemmas on conditional probability, but I could not find much either. Therefore, I formalized a bit on conditional probability theory myself.

I will send you the library if you wish, although it is not complete.

Yosuke Ito said:

Chelsea Edmonds

I also searched lemmas on conditional probability, but I could not find much either. Therefore, I formalized a bit on conditional probability theory myself.

I will send you the library if you wish, although it is not complete.

That'd be fantastic if you're will to share! I'd obviously give you full credit if I ended up using any of it in my work.

All right. I attach my theory file on this message. Could you download it?

The lemmas on conditional probability can be found in the section 'Additional Lemmas for the "Probability" Library'.

I apologize if they are not what you need, since I proved them especially for formalizing actuarial mathematics.

(When the formalization reach a good stopping point, I will upload this file to AFP after refining the proofs.)

Preliminaries.thy

Last updated: Dec 07 2023 at 12:30 UTC