English
In full generality, for a locally finite measure ρ and μ with ρ ≪ μ, the ratio ρ(a)/μ(a) tends μ-almost everywhere to the Radon–Nikodym derivative ρ.rnDeriv μ at x as a shrinks to x along a Vitali family.
Русский
В полной общности, для locally finite measures ρ и μ с ρ ≪ μ, отношение ρ(a)/μ(a) стремится к радону-никодимовой производной ρ.rnDeriv μ в x почти наверно по μ, когда a схлопывается к x вдоль семейства Витали.
LaTeX
$$$\forall^{\mu}\ x,\ Tendsto\bigl(\lambda a.\dfrac{ρ(a)}{μ(a)}\bigr)(v.filterAt x)\bigl(\mathcal{N}(ρ.rnDeriv μ x)\bigr).$$$
Lean4
/-- Main theorem on differentiation of measures: given a Vitali family `v` for a locally finite
measure `μ`, and another locally finite measure `ρ`, then for `μ`-almost every `x` the
ratio `ρ a / μ a` converges, when `a` shrinks to `x` along the Vitali family, towards the
Radon-Nikodym derivative of `ρ` with respect to `μ`. -/
theorem ae_tendsto_rnDeriv : ∀ᵐ x ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x)) :=
by
let t := μ.withDensity (ρ.rnDeriv μ)
have eq_add : ρ = ρ.singularPart μ + t := haveLebesgueDecomposition_add _ _
have A : ∀ᵐ x ∂μ, Tendsto (fun a => ρ.singularPart μ a / μ a) (v.filterAt x) (𝓝 0) :=
v.ae_eventually_measure_zero_of_singular (mutuallySingular_singularPart ρ μ)
have B : ∀ᵐ x ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x := rnDeriv_withDensity μ (measurable_rnDeriv ρ μ)
have C : ∀ᵐ x ∂μ, Tendsto (fun a => t a / μ a) (v.filterAt x) (𝓝 (t.rnDeriv μ x)) :=
v.ae_tendsto_rnDeriv_of_absolutelyContinuous (withDensity_absolutelyContinuous _ _)
filter_upwards [A, B, C] with _ Ax Bx Cx
convert Ax.add Cx using 1
· ext1 a
conv_lhs => rw [eq_add]
simp only [Pi.add_apply, coe_add, ENNReal.add_div]
· simp only [Bx, zero_add]
