Commit 2025-01-28 16:40 22d2235f

View on Github →

feat(Probability): notation and lemmas for the composition of a measure and a kernel (Measure.bind) (#19639) From the TestingLowerBounds project.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/Prod.lean

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

added theorem MeasureTheory.Measure.comp_apply_univ

added theorem MeasureTheory.Measure.const_comp

added theorem MeasureTheory.Measure.deterministic_comp_eq_map

added theorem MeasureTheory.Measure.id_comp

added theorem MeasureTheory.Measure.swap_comp

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

added theorem MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp

added theorem MeasureTheory.Measure.parallelComp_comp_compProd

added theorem MeasureTheory.Measure.prod_comp_left

added theorem MeasureTheory.Measure.prod_comp_right

added theorem ProbabilityTheory.Kernel.parallelComp_comm

added theorem ProbabilityTheory.Kernel.parallelComp_comp_parallelComp

added theorem ProbabilityTheory.Kernel.parallelComp_comp_prod

added theorem ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp

added theorem ProbabilityTheory.Kernel.parallelComp_id_right_comp_parallelComp

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

added theorem MeasureTheory.Measure.AbsolutelyContinuous.comp

added theorem MeasureTheory.Measure.AbsolutelyContinuous.comp_left

added theorem MeasureTheory.Measure.AbsolutelyContinuous.comp_right

added theorem MeasureTheory.Measure.add_comp'

added theorem MeasureTheory.Measure.add_comp

added theorem MeasureTheory.Measure.compProd_eq_comp_prod

added theorem MeasureTheory.Measure.compProd_id_eq_copy_comp

added theorem MeasureTheory.Measure.comp_add

added theorem MeasureTheory.Measure.comp_assoc

added theorem MeasureTheory.Measure.comp_smul

added theorem MeasureTheory.Measure.map_comp

added theorem MeasureTheory.Measure.snd_compProd

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

added theorem MeasureTheory.Measure.compProd_id

Modified Mathlib/Probability/Kernel/Proper.lean

deleted theorem ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_bind

added theorem ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_comp

Modified scripts/noshake.json