English
For a finite index set, UniformIntegrable holds for any family of Lp functions; the finite version mirrors the finite-n lemma.
Русский
Для конечного множества индексов UniformIntegrable выполняется для любой семьи функций Lp; конечная версия повторяет конечную лемму.
LaTeX
$$$[Finite ι]\ (hp\, one\, hp\, top)\ (hf : ∀ i, MemLp (f i) p μ) \Rightarrow UniformIntegrable f p μ$$$
Lean4
/-- A finite sequence of Lp functions is uniformly integrable in the probability sense. -/
theorem uniformIntegrable_finite [Finite ι] (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) (hf : ∀ i, MemLp (f i) p μ) :
UniformIntegrable f p μ := by
cases nonempty_fintype ι
refine ⟨fun n => (hf n).1, unifIntegrable_finite hp_one hp_top hf, ?_⟩
by_cases hι : Nonempty ι
· choose _ hf using hf
set C :=
(Finset.univ.image fun i : ι => eLpNorm (f i) p μ).max'
⟨eLpNorm (f hι.some) p μ, Finset.mem_image.2 ⟨hι.some, Finset.mem_univ _, rfl⟩⟩
refine ⟨C.toNNReal, fun i => ?_⟩
rw [ENNReal.coe_toNNReal]
· exact Finset.le_max' (α := ℝ≥0∞) _ _ (Finset.mem_image.2 ⟨i, Finset.mem_univ _, rfl⟩)
· refine ne_of_lt ((Finset.max'_lt_iff _ _).2 fun y hy => ?_)
rw [Finset.mem_image] at hy
obtain ⟨i, -, rfl⟩ := hy
exact hf i
· exact ⟨0, fun i => False.elim <| hι <| Nonempty.intro i⟩
