Chelsea Edmonds (Feb 23 2023 at 13:34): 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: Apr 19 2024 at 01:05 UTC