Commit 2024-11-28 16:12 52e32981

View on Github →

feat(Probability): lemmas about composition-product of a measure and a kernel (#19562) From the TestingLowerBounds project.

Estimated changes

Modified Mathlib/Probability/Kernel/MeasureCompProd.lean

added theorem MeasureTheory.Measure.compProd_apply_univ

added theorem MeasureTheory.Measure.compProd_const

added theorem MeasureTheory.Measure.compProd_smul_left

added theorem MeasureTheory.Measure.fst_compProd