Commit 2023-05-10 10:25 ab8b90a8

View on Github →

feat: port Probability.ConditionalProbability (#3885)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/ConditionalProbability.lean

added def ProbabilityTheory.cond

added theorem ProbabilityTheory.cond_add_cond_compl_eq

added theorem ProbabilityTheory.cond_apply

added theorem ProbabilityTheory.cond_cond_eq_cond_inter'

added theorem ProbabilityTheory.cond_cond_eq_cond_inter

added theorem ProbabilityTheory.cond_empty

added theorem ProbabilityTheory.cond_eq_inv_mul_cond_mul

added theorem ProbabilityTheory.cond_inter_self

added theorem ProbabilityTheory.cond_mul_eq_inter'

added theorem ProbabilityTheory.cond_mul_eq_inter

added theorem ProbabilityTheory.cond_pos_of_inter_ne_zero

added theorem ProbabilityTheory.cond_probabilityMeasure

added theorem ProbabilityTheory.cond_univ

added theorem ProbabilityTheory.inter_pos_of_cond_ne_zero