English
A finite sequence of Lp functions is uniformly integrable; the property holds uniformly over the finite index set.
Русский
Конечная последовательность функций в Lp является uniformly integrable; свойство сохраняется на конечном индексе.
LaTeX
$$$[Finite\ ι]\ ∀ i, MemLp (f i) p μ \Rightarrow UnifIntegrable f p μ$$$
Lean4
/-- This lemma is less general than `MeasureTheory.unifIntegrable_finite` which applies to
all sequences indexed by a finite type. -/
theorem unifIntegrable_fin (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) {n : ℕ} {f : Fin n → α → β} (hf : ∀ i, MemLp (f i) p μ) :
UnifIntegrable f p μ := by
revert f
induction n with
| zero => exact fun {f} hf ↦ unifIntegrable_subsingleton hp_one hp_top hf
| succ n h =>
intro f hfLp ε hε
let g : Fin n → α → β := fun k => f k.castSucc
have hgLp : ∀ i, MemLp (g i) p μ := fun i => hfLp i.castSucc
obtain ⟨δ₁, hδ₁pos, hδ₁⟩ := h hgLp hε
obtain ⟨δ₂, hδ₂pos, hδ₂⟩ := (hfLp (Fin.last n)).eLpNorm_indicator_le hp_one hp_top hε
refine ⟨min δ₁ δ₂, lt_min hδ₁pos hδ₂pos, fun i s hs hμs => ?_⟩
by_cases hi : i.val < n
· rw [(_ : f i = g ⟨i.val, hi⟩)]
· exact hδ₁ _ s hs (le_trans hμs <| ENNReal.ofReal_le_ofReal <| min_le_left _ _)
· simp [g]
· obtain rfl : i = Fin.last n := Fin.ext (le_antisymm (Fin.is_le i) (not_lt.mp hi))
exact hδ₂ _ hs (le_trans hμs <| ENNReal.ofReal_le_ofReal <| min_le_right _ _)
