Chelsea Edmonds (Mar 14 2023 at 17:03): Chelsea Edmonds (Mar 14 2023 at 17:03):I have a concern regarding our current main probability formalisation in the library, and want to check I'm not missing something obvious. Say we have a set of events and event $A$. And we want to show a certain level of independence (which we should be able to based on other assumptions):
prob (A ∩ (⋂ T)) = prob A * prob (⋂T)"
But this doesn't work for the base case where T = {} as (⋂{}) = UNIV and in our formalisation prob UNIV = 0 unless you can prove that UNIV is a subset or equal to the space which is often not the case (as the "space" definition is not necessarily the same as UNIV with how we go about setting up probability spaces up typically in Isabelle currently). On paper, however, UNIV is typically considered the space so this fact does clearly hold (as P(U) = 1). This seems to pose a rather notable problem that I'm currently getting around by adding in what should be unnecessary assumptions and using base cases of sets of size 1. As far I can see it does not appear to be a problem in other probability formalisations I've seen in other proof assistants. I'd be curious if anyone has any thoughts as to why the formalisation works this way currently/how best to work with it/if something needs to be changed?
Manuel Eberl (Mar 29 2023 at 09:57):That does look like an issue. I haven't worked with this library in a while – is T = {} an important case? It does seem that me that this is kind of a boring case that one can simply work around.
But yes, it would probably have been better to add an additional ∩ space M. Perhaps we still should.
Last updated: Feb 28 2025 at 08:24 UTC