Commit 2023-09-29 13:54 042888f5

View on Github →

feat(Probability/Kernel/Disintegration): Uniqueness of the disintegration kernel (#6110)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

added theorem MeasurableSpace.ae_induction_on_inter

added theorem MeasureTheory.all_ae_of

Modified Mathlib/Probability/Kernel/CondDistrib.lean

added theorem ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd

Modified Mathlib/Probability/Kernel/Disintegration.lean

added theorem ProbabilityTheory.eq_condKernel_of_measure_eq_compProd'

added theorem ProbabilityTheory.eq_condKernel_of_measure_eq_compProd

added theorem ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real