-
Notifications
You must be signed in to change notification settings - Fork 315
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: Basic conditional probability lemmas #10785
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
lemma law_of_total_probability {Y : Ω → α} (hY : Measurable Y) (μ : Measure Ω) [IsFiniteMeasure μ] : | ||
μ = ∑ y, μ (Y ⁻¹' {y}) • (μ[|Y ← y]) := by |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you revert this equality, and give a more descriptive name to the theorem, mentioning sum and cond?
I also don't like that name because this is not the only statement that could be called "law of total probability". For example, when I think of that law, I imagine the first of the two equalities on the wikipedia page: https://en.wikipedia.org/wiki/Law_of_total_probability . There is also the continuous case...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What about now?
LGTM! |
Pull request successfully merged into master. Build succeeded: |
From PFR