Commit 2024-01-18 15:15 1bf390a0

View on Github →

feat(Probability): condKernel and condDistrib applied to singletons of non-zero measure (#9351) From the PFR project.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

added theorem MeasurableEmbedding.prod_mk_left

added theorem MeasurableEmbedding.prod_mk_right

added theorem measurableEmbedding_prod_mk_left

added theorem measurableEmbedding_prod_mk_right

Modified Mathlib/Probability/Kernel/CondDistrib.lean

added theorem ProbabilityTheory.condDistrib_apply_of_ne_zero

Modified Mathlib/Probability/Kernel/Disintegration.lean

added theorem ProbabilityTheory.condKernel_apply_of_ne_zero

added theorem ProbabilityTheory.condKernel_apply_of_ne_zero_of_measurableSet