Commit 2024-05-06 12:00 f5fbe095

View on Github →

feat: generalize kernel Radon-Nikodym derivative to CountableOrCountablyGenerated (#12571) Radon-Nikodym derivatives of finite kernels kernel α γ are currently defined under the assumption that γ is countably generated. We extend the construction to the case that either α is countable or γ is countably generated.

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

added theorem MeasureTheory.Measure.rnDeriv_le_one_of_le

modified theorem MeasureTheory.Measure.rnDeriv_mul_rnDeriv

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

added theorem ProbabilityTheory.kernel.mem_mutuallySingularSetSlice

modified def ProbabilityTheory.kernel.mutuallySingularSet

added theorem ProbabilityTheory.kernel.not_mem_mutuallySingularSetSlice

modified theorem ProbabilityTheory.kernel.rnDerivAux_le_one

modified theorem ProbabilityTheory.kernel.rnDerivAux_nonneg