## Stream: Is there code for X?

### Topic: Conditional Probability

#### Chelsea Edmonds (Feb 23 2023 at 13:34):

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!

#### Manuel Eberl (Feb 23 2023 at 14:12):

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.

#### Manuel Eberl (Feb 23 2023 at 14:17):

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.

#### Manuel Eberl (Feb 23 2023 at 14:19):

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"

#### Manuel Eberl (Feb 23 2023 at 14:20):

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.

#### Manuel Eberl (Feb 23 2023 at 14:20):

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

#### Manuel Eberl (Feb 23 2023 at 14:23):

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

#### Manuel Eberl (Feb 23 2023 at 14:24):

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.

#### Manuel Eberl (Feb 23 2023 at 14:25):

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

#### Manuel Eberl (Feb 23 2023 at 14:25):

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.

#### Chelsea Edmonds (Feb 24 2023 at 14:23):

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.

#### Yosuke Ito (Feb 25 2023 at 11:08):

@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.

#### Chelsea Edmonds (Feb 27 2023 at 21:34):

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.

#### Yosuke Ito (Feb 28 2023 at 11:09):

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: Jun 20 2024 at 08:21 UTC