Commit 2025-04-08 13:38 4f399dab

View on Github →

feat(GiryMonad): use AEMeasurable (#23754) Also deduce lintegral_prod from lintegral_bind.

Estimated changes

Modified Mathlib/MeasureTheory/Category/MeasCat.lean

Modified Mathlib/MeasureTheory/Integral/Prod.lean

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

Modified Mathlib/MeasureTheory/Measure/GiryMonad.lean

added theorem AEMeasurable.ae_of_bind

added theorem AEMeasurable.ae_of_join

added theorem MeasureTheory.Measure.ae_ae_of_ae_bind

added theorem MeasureTheory.Measure.ae_ae_of_ae_join

added theorem MeasureTheory.Measure.aemeasurable_bind

added theorem MeasureTheory.Measure.aemeasurable_lintegral

added theorem MeasureTheory.Measure.bind_congr_right

modified theorem MeasureTheory.Measure.bind_zero_right'

modified theorem MeasureTheory.Measure.bind_zero_right

modified theorem MeasureTheory.Measure.join_dirac

added theorem MeasureTheory.Measure.join_smul

added theorem MeasureTheory.Measure.le_ae_join

modified theorem MeasureTheory.Measure.lintegral_bind

modified theorem MeasureTheory.Measure.lintegral_join

Modified Mathlib/MeasureTheory/Measure/Prod.lean

modified theorem MeasureTheory.lintegral_prod_of_measurable

Modified Mathlib/Probability/Kernel/Composition/Comp.lean

Modified Mathlib/Probability/Kernel/Composition/CompNotation.lean

Modified Mathlib/Probability/Kernel/Composition/Lemmas.lean

Modified Mathlib/Probability/Kernel/Composition/MeasureComp.lean

Modified Mathlib/Probability/Kernel/Defs.lean

added theorem ProbabilityTheory.Kernel.aemeasurable

Modified Mathlib/Probability/Kernel/Invariance.lean

Modified Mathlib/Probability/Kernel/Proper.lean