English
Lebesgue differentiation for norm-valued functions: if f is locally integrable, then for almost every x the average of ||f(y)-f(x)|| over shrinking closed balls tends to 0 as the center and radius vary along a Vitali family.
Русский
Лебеговская теорема плотности для значений в нормированном пространстве: если f локально интегрируема, то почти для почти всякого x среднее по шарикам стремится к 0.
LaTeX
$$$\forall f: α→E\ (hf: LocallyIntegrable f μ)\ ∀ K>1,\ almostEvery x,\ Tendsto_{j\to} \big( y\mapsto \|f(y)-f(x)\|\big)\text{ over } (\overline{B}(w_j, δ_j)) → 0.$$$
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_norm_sub {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 - f x‖ ∂μ) l (𝓝 0) :=
by
filter_upwards [(vitaliFamily μ K).ae_tendsto_average_norm_sub hf] with x hx ι l w δ δlim xmem using
hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)
