English
For LocallyIntegrable f, the same a.e. convergence holds for the ENNReal-norm distance version of the integral.
Русский
Для LocallyIntegrable f сохраняется такое же почти равномерное сходство для нормы ENNReal расстояния в интеграле.
LaTeX
$$$\forall^{\mu}\ x,\ Tendsto(\lambda a.\dfrac{\int_{y∈a} ||f(y)-f(x)||_n \ dμ}{μ(a)}) (v.filterAt x) (𝓝 0).$$$
Lean4
theorem ae_tendsto_lintegral_enorm_sub_div {f : α → E} (hf : LocallyIntegrable f μ) :
∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0) :=
by
rcases hf.exists_nat_integrableOn with ⟨u, u_open, u_univ, hu⟩
have :
∀ n,
∀ᵐ x ∂μ,
Tendsto (fun a => (∫⁻ y in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0) :=
by
intro n
apply ae_tendsto_lintegral_enorm_sub_div_of_integrable
exact (integrable_indicator_iff (u_open n).measurableSet).2 (hu n)
filter_upwards [ae_all_iff.2 this] with x hx
obtain ⟨n, hn⟩ : ∃ n, x ∈ u n := by simpa only [← u_univ, mem_iUnion] using mem_univ x
apply Tendsto.congr' _ (hx n)
filter_upwards [v.eventually_filterAt_subset_of_nhds ((u_open n).mem_nhds hn),
v.eventually_filterAt_measurableSet x] with a ha h'a
congr 1
refine setLIntegral_congr_fun h'a (fun y hy ↦ ?_)
rw [indicator_of_mem (ha hy) f, indicator_of_mem hn f]
