The Radon–Nikodym derivative on a countable type

On a countable type with measurable singletons, a measure absolutely continuous with respect to a finite measure ν has density a ↦ μ {a} / ν {a}, so its Radon–Nikodym derivative is the ratio of atom masses ν-almost everywhere. [UPSTREAM] candidate for Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean.

theorem MeasureTheory.Measure.withDensity_div_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] {μ ν : Measure α} [IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) : (ν.withDensity fun (a : α) => μ {a} / ν {a}) = μ

theorem MeasureTheory.Measure.rnDeriv_eq_div_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] {μ ν : Measure α} [IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) : μ.rnDeriv ν =ᵐ[ν] fun (a : α) => μ {a} / ν {a}