Commit 2024-12-11 17:41 eaab7c8d

View on Github →

feat(Probability): absolute continuity of Measure.compProd (#19629) Also rename some lemmas to use dot notation. From the TestingLowerBounds project.

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

added theorem MeasureTheory.Measure.AbsolutelyContinuous.withDensity_rnDeriv

added theorem MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv_swap

Modified Mathlib/MeasureTheory/Measure/MutuallySingular.lean

added theorem MeasureTheory.Measure.MutuallySingular.congr_ac

added theorem MeasureTheory.Measure.absolutelyContinuous_of_add_of_mutuallySingular

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

added theorem MeasureTheory.Measure.AbsolutelyContinuous.compProd

added theorem MeasureTheory.Measure.AbsolutelyContinuous.compProd_left

added theorem MeasureTheory.Measure.AbsolutelyContinuous.compProd_of_compProd

added theorem MeasureTheory.Measure.AbsolutelyContinuous.compProd_right

added theorem MeasureTheory.Measure.AbsolutelyContinuous.mutuallySingular_compProd_iff

added theorem MeasureTheory.Measure.MutuallySingular.compProd_of_left

deleted theorem MeasureTheory.Measure.absolutelyContinuous_compProd

added theorem MeasureTheory.Measure.absolutelyContinuous_compProd_iff

deleted theorem MeasureTheory.Measure.absolutelyContinuous_compProd_left

added theorem MeasureTheory.Measure.absolutelyContinuous_compProd_left_iff

added theorem MeasureTheory.Measure.absolutelyContinuous_compProd_of_compProd

deleted theorem MeasureTheory.Measure.absolutelyContinuous_compProd_right

added theorem MeasureTheory.Measure.mutuallySingular_compProd_iff

added theorem MeasureTheory.Measure.mutuallySingular_compProd_left_iff

added theorem MeasureTheory.Measure.mutuallySingular_of_mutuallySingular_compProd