English
If the index set ι is a singleton, a single Lp function is uniformly tight.
Русский
Если множество индексов ι одноэлементное, то одна функция Lp образует униформно ограниченный набор.
LaTeX
$$$[Subsingleton\\\\ ι]\\\\Rightarrow\\\\UnifTight f p μ$ для единственного i с MemLp (f i) p μ$$
Lean4
/-- A finite sequence of Lp functions is uniformly tight. -/
theorem unifTight_finite [Finite ι] (hp_top : p ≠ ∞) {f : ι → α → β} (hf : ∀ i, MemLp (f i) p μ) : UnifTight f p μ :=
fun ε hε ↦ by
obtain ⟨n, hn⟩ := Finite.exists_equiv_fin ι
set g : Fin n → α → β := f ∘ hn.some.symm
have hg : ∀ i, MemLp (g i) p μ := fun _ => hf _
obtain ⟨s, hμs, hfε⟩ := unifTight_fin hp_top hg hε
refine ⟨s, hμs, fun i => ?_⟩
simpa only [g, Function.comp_apply, Equiv.symm_apply_apply] using hfε (hn.some i)
