English
A sequence of functions f is uniformly integrable if and only if there exists a bound C such that the tail Lp-norms are controlled by ε for all index sets; this is a restatement in a general inequality form.
Русский
Последовательность функций в равной равенстве: существует ограничение C такое, что хвостовые Lp-нормы управляются ε.
LaTeX
$$$\text{UniformIntegrable } f p μ \iff \exists C>0, \forall i, eLpNorm(...) ≤ ε$$$
Lean4
theorem unifIntegrable_of_tendsto_Lp_zero (hp : 1 ≤ p) (hp' : p ≠ ∞) (hf : ∀ n, MemLp (f n) p μ)
(hf_tendsto : Tendsto (fun n => eLpNorm (f n) p μ) atTop (𝓝 0)) : UnifIntegrable f p μ :=
by
intro ε hε
rw [ENNReal.tendsto_atTop_zero] at hf_tendsto
obtain ⟨N, hN⟩ := hf_tendsto (ENNReal.ofReal ε) (by simpa)
let F : Fin N → α → β := fun n => f n
have hF : ∀ n, MemLp (F n) p μ := fun n => hf n
obtain ⟨δ₁, hδpos₁, hδ₁⟩ := unifIntegrable_fin hp hp' hF hε
refine ⟨δ₁, hδpos₁, fun n s hs hμs => ?_⟩
by_cases hn : n < N
· exact hδ₁ ⟨n, hn⟩ s hs hμs
· exact (eLpNorm_indicator_le _).trans (hN n (not_lt.1 hn))
