unifIntegrable_of_tendsto_Lp — Mathlib

English

If f is a single function in MemLp, it is uniformly integrable; i.e., the constant function valued in f is uniformly integrable.

Русский

Единичная функция в MemLp="UniformIntegrable".

LaTeX

$$$\text{UnifIntegrable } f p μ$ for a singleton index set$$

Lean4

/-- Convergence in Lp implies uniform integrability. -/
theorem unifIntegrable_of_tendsto_Lp (hp : 1 ≤ p) (hp' : p ≠ ∞) (hf : ∀ n, MemLp (f n) p μ) (hg : MemLp g p μ)
    (hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)) : UnifIntegrable f p μ :=
  by
  have : f = (fun _ => g) + fun n => f n - g := by ext1 n; simp
  rw [this]
  refine UnifIntegrable.add ?_ ?_ hp (fun _ => hg.aestronglyMeasurable) fun n => (hf n).1.sub hg.aestronglyMeasurable
  · exact unifIntegrable_const hp hp' hg
  · exact unifIntegrable_of_tendsto_Lp_zero hp hp' (fun n => (hf n).sub hg) hfg

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