English
Let μ be a locally finite measure on a metric space X, and let ρ be a locally finite measure absolutely continuous with respect to μ. Then for μ-almost every x, the ratio ρ(a)/μ(a) tends to the Radon–Nikodym derivative dρ/dμ at x as a shrinks to x along a Vitali family.
Русский
Пусть μ — локально конечная мера на метрическом пространстве X, а ρ — локально конечная мера, Absolutely Continuous по отношению к μ. Тогда для μ-почти каждого x предел отношения ρ(a)/μ(a) при сокращении a к x вдоль семейства Витали можно получить Radon–Nikodīm произвольной derivative dρ/dμ в точке x.
LaTeX
$$$\forall^{\mu}\ x\ \ Tendsto\bigl(\lambda a.\dfrac{\rho(a)}{\mu(a)}\bigr)\bigl(v.filterAt x\bigr)\bigl(\mathcal{N}(\rho. rnDeriv\, \mu\, x)\bigr).$$$
Lean4
/-- Weak version of the 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 `μ`.
This version assumes that `ρ` is absolutely continuous with respect to `μ`. The general version
without this superfluous assumption is `VitaliFamily.ae_tendsto_rnDeriv`.
-/
theorem ae_tendsto_rnDeriv_of_absolutelyContinuous :
∀ᵐ x ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x)) :=
by
have A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᵐ[μ] v.limRatioMeas hρ :=
rnDeriv_withDensity μ (v.limRatioMeas_measurable hρ)
rw [v.withDensity_limRatioMeas_eq hρ] at A
filter_upwards [v.ae_tendsto_limRatioMeas hρ, A] with _ _ h'x
rwa [h'x]
