Commit 2024-02-22 17:42 3f4e4420

View on Github →

feat: Basic conditional probability lemmas (#10785) From PFR

Estimated changes

Modified Mathlib/Probability/ConditionalProbability.lean

added theorem ProbabilityTheory.comap_cond

modified theorem ProbabilityTheory.cond_absolutelyContinuous

modified theorem ProbabilityTheory.cond_add_cond_compl_eq

modified theorem ProbabilityTheory.cond_apply'

modified theorem ProbabilityTheory.cond_cond_eq_cond_inter'

modified theorem ProbabilityTheory.cond_cond_eq_cond_inter

added theorem ProbabilityTheory.cond_eq_zero

added theorem ProbabilityTheory.cond_eq_zero_of_meas_eq_zero

modified theorem ProbabilityTheory.cond_mul_eq_inter'

modified theorem ProbabilityTheory.cond_mul_eq_inter

added theorem ProbabilityTheory.sum_meas_smul_cond_fiber

Modified Mathlib/Probability/Distributions/Uniform.lean