Commit 2022-03-02 09:30 35086a11

View on Github →

feat(probability): define conditional probability and add basic related theorems (#12344) Add the definition of conditional probability as a scaled restricted measure and prove Bayes' Theorem and other basic theorems.

Estimated changes

Modified src/measure_theory/measure/outer_measure.lean

added theorem measure_theory.outer_measure.pos_of_subset_ne_zero

Created src/probability/conditional.lean

added def probability_theory.cond

added theorem probability_theory.cond_apply

added theorem probability_theory.cond_cond_eq_cond_inter

added theorem probability_theory.cond_eq_inv_mul_cond_mul

added theorem probability_theory.cond_is_probability_measure

added theorem probability_theory.cond_mul_eq_inter

added theorem probability_theory.cond_pos_of_inter_ne_zero

added theorem probability_theory.cond_univ

added theorem probability_theory.inter_pos_of_cond_ne_zero