English
For a set S and a doubling locally finite measure μ, for μ-almost every x there exist moving centers w_j and radii δ_j tending to 0 such that the ratio μ(S ∩ closedBall(w_j, δ_j)) / μ(closedBall(w_j, δ_j)) tends to 1 along the Vitali family around x.
Русский
Для множества S и локально конечно меры μ, почти для почти всех x существует последовательность центров w_j и радиусов δ_j, стремящихся к 0, так что отношение μ(S ∩ закрытого шара) к μ(закрытому шару) стремится к 1 вдоль семейства Vitali около x.
LaTeX
$$$\forall S, K: \ μ\text{-almost every } x,\ Tendsto\Big( j \mapsto \frac{μ(S\cap \overline{B}(w_j, δ_j))}{μ(\overline{B}(w_j, δ_j))}\Big)_{l} \to 1.$$$
Lean4
/-- A version of **Lebesgue's density theorem** for a sequence of closed balls whose centers are
not required to be fixed.
See also `Besicovitch.ae_tendsto_measure_inter_div`. -/
theorem ae_tendsto_measure_inter_div (S : Set α) (K : ℝ) :
∀ᵐ x ∂μ.restrict S,
∀ {ι : Type*} {l : Filter ι} (w : ι → α) (δ : ι → ℝ) (_ : Tendsto δ l (𝓝[>] 0))
(_ : ∀ᶠ j in l, x ∈ closedBall (w j) (K * δ j)),
Tendsto (fun j => μ (S ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1) :=
by
filter_upwards [(vitaliFamily μ K).ae_tendsto_measure_inter_div S] with x hx ι l w δ δlim xmem using
hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)
