ae_tendsto_lintegral_enorm_sub_div_of_integrable

English

If f is integrable, then almost everywhere the Lintegral of the ENNReal-norm distance goes to 0 along shrinking sets.

Русский

Если f интегрируема, то почти всюду норма ENNReal расстояния ∥f(y)-f(x)∥ даёт предел 0 при сжатии областей.

LaTeX

$$$\forall^{\mu}\ x,\ Tendsto(\lambda a.\dfrac{\int_{y∈a} ||f(y)-f(x)||_E \,dμ}{μ(a)}) (v.filterAt x) (𝓝 0).$$$

Lean4

theorem ae_tendsto_lintegral_enorm_sub_div_of_integrable {f : α → E} (hf : Integrable f μ) :
    ∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0) :=
  by
  have I : Integrable (hf.1.mk f) μ := hf.congr hf.1.ae_eq_mk
  filter_upwards [v.ae_tendsto_lintegral_enorm_sub_div'_of_integrable I hf.1.stronglyMeasurable_mk, hf.1.ae_eq_mk] with
    x hx h'x
  apply hx.congr _
  intro a
  congr 1
  apply lintegral_congr_ae
  apply ae_restrict_of_ae
  filter_upwards [hf.1.ae_eq_mk] with y hy
  rw [hy, h'x]

Похожие утверждения