English
Lebesgue differentiation theorem for averages: for locally integrable f, for almost every x the average of f over shrinking closed balls tends to f(x).
Русский
Теорема о среднем плотности Лебега: для локально интегрируемой функции f почти для почти всех x среднее значение f по сжимающимся шарикам стремится к f(x).
LaTeX
$$$\forall f: α→E\ (hf: LocallyIntegrable f μ)\ ∀ K>1,\ almostEvery x,\ Tendsto_{j} \big( y\mapsto f(y)\big)\text{ в средних шарах } (\overline{B}(w_j, δ_j)) \to f(x).$$$
Lean4
/-- A version of **Lebesgue differentiation theorem** for a sequence of closed balls whose
centers are not required to be fixed. -/
theorem ae_tendsto_average [NormedSpace ℝ E] [CompleteSpace E] {f : α → E} (hf : LocallyIntegrable f μ) (K : ℝ) :
∀ᵐ x ∂μ,
∀ {ι : Type*} {l : Filter ι} (w : ι → α) (δ : ι → ℝ) (_ : Tendsto δ l (𝓝[>] 0))
(_ : ∀ᶠ j in l, x ∈ closedBall (w j) (K * δ j)),
Tendsto (fun j => ⨍ y in closedBall (w j) (δ j), f y ∂μ) l (𝓝 (f x)) :=
by
filter_upwards [(vitaliFamily μ K).ae_tendsto_average hf] with x hx ι l w δ δlim xmem using
hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)
