Commit 2025-02-19 18:19 46c8a2ff

View on Github →

feat: absolute continuity results for composition of measures and kernels (#21902) A new file with results about the absolute continuity of the composition of measures and kernels which use an assumption CountableOrCountablyGenerated α β on the measurable spaces. From the TestingLowerBounds project.

Estimated changes

Modified Mathlib.lean

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

added theorem MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd

added theorem MeasureTheory.Measure.MutuallySingular.compProd_of_right'

added theorem MeasureTheory.Measure.MutuallySingular.compProd_of_right

added theorem MeasureTheory.Measure.absolutelyContinuous_compProd_iff'

added theorem MeasureTheory.Measure.absolutelyContinuous_compProd_right_iff

added theorem MeasureTheory.Measure.mutuallySingular_compProd_right_iff

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

added theorem ProbabilityTheory.Kernel.compProd_apply_prod

added theorem ProbabilityTheory.Kernel.compProd_apply_univ

added theorem ProbabilityTheory.Kernel.compProd_congr

added theorem ProbabilityTheory.Kernel.compProd_eq_zero_iff

modified theorem ProbabilityTheory.Kernel.fst_map_id_prod

modified theorem ProbabilityTheory.Kernel.snd_map_prod_id

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

modified theorem MeasureTheory.Measure.compProd_congr

added theorem MeasureTheory.Measure.compProd_eq_zero_iff