English
Analogous to the previous lemma, but phrased for the finite index case; the uniform integrability is proven by reduction to the finite subcollection.
Русский
Аналогично предыдущему для конечного индекса, где униформ-интегрируемость получена сведением к конечной подпуке.
LaTeX
$$См. предыдущее: UnifIntegrable_finite$$
Lean4
/-- A finite sequence of Lp functions is uniformly integrable. -/
theorem unifIntegrable_finite [Finite ι] (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) {f : ι → α → β} (hf : ∀ i, MemLp (f i) p μ) :
UnifIntegrable f p μ := by
obtain ⟨n, hn⟩ := Finite.exists_equiv_fin ι
intro ε hε
let g : Fin n → α → β := f ∘ hn.some.symm
have hg : ∀ i, MemLp (g i) p μ := fun _ => hf _
obtain ⟨δ, hδpos, hδ⟩ := unifIntegrable_fin hp_one hp_top hg hε
refine ⟨δ, hδpos, fun i s hs hμs => ?_⟩
simpa [g] using hδ (hn.some i) s hs hμs
