English
For μ-a.e. x, the limit as r ↓ 0 of ρ(closedBall x r) / μ(closedBall x r) exists and equals ρ.rnDeriv μ x.
Русский
Для практически почти всех x по μ предел при r→0+ от отношения ρ закрытого шара к μ закрытого шара существует и совпадает с ρ.rnDeriv μ x.
LaTeX
$$$$\\forall^{\\ae} x \\; \\partial_\\mu,\\; \\ Tendsto\\left(\\lambda r,\\; \\frac{\\rho(\\overline{B}(x,r))}{\\mu(\\overline{B}(x,r))}\\right)\\left(\\mathcal{N}_{[>0]}(0)\\right)\\left(\\mathcal{N}(\\rho.rnDeriv\\;\\mu\\;x)\\right).$$$$
Lean4
/-- In a space with the Besicovitch covering property, the ratio of the measure of balls converges
almost surely to the Radon-Nikodym derivative. -/
theorem ae_tendsto_rnDeriv (ρ μ : Measure β) [IsLocallyFiniteMeasure μ] [IsLocallyFiniteMeasure ρ] :
∀ᵐ x ∂μ, Tendsto (fun r => ρ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (ρ.rnDeriv μ x)) :=
by
filter_upwards [VitaliFamily.ae_tendsto_rnDeriv (Besicovitch.vitaliFamily μ) ρ] with x hx
exact hx.comp (tendsto_filterAt μ x)
