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
feat(probability): define conditional probability and add basic related theorems #12279
Conversation
local notation μ `[` s `|` t `]` := cond μ t s | ||
local notation μ `[|` t`]` := cond μ t |
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.
Noticed that this conflicts with some existing notation for conditional expectation -- let me know what you think is best here, will be happy to change.
/-- The conditional probability measure of any finite measure on any set of positive measure | ||
is a probability measure. -/ | ||
instance cond_is_probability_measure [is_finite_measure μ] {s : set α} (hcs : μ s ≠ 0) : | ||
is_probability_measure $ μ[|s] := |
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.
I think it would be worthwhile to attempt to tweak the notation so that no $
is needed here.
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.
I agree, not sure what was going on here. Don't have much experience defining notation so suggestions are welcome. I'd also be OK with just doing without notation here for now.
Please push this branch to mathlib repo and PR to the master branch from there, as described in the contributor guidelines. |
Add the definition of conditional probability as a scaled restricted measure and prove Bayes' Theorem and other basic theorems.