English
A constant sequence of a function g is uniformly tight if g ∈ Lp(μ) and p ≠ ∞.
Русский
Постоянная последовательность одной функции g является униформно ограниченной, если g лежит в Lp(μ) и p не равен бесконечности.
LaTeX
$$$\\text{UnifTight}\\\\; (\\\\lambda i. g)\\\\; p\\\\; μ \\\\Leftrightarrow \\\\ g \\in L^p(μ) \\, (p≠∞)$$$
Lean4
/-- A constant sequence is tight. -/
theorem unifTight_const {g : α → β} (hp_ne_top : p ≠ ∞) (hg : MemLp g p μ) : UnifTight (fun _ : ι => g) p μ :=
by
intro ε hε
by_cases hε_top : ε = ∞
· exact ⟨∅, (by simp), fun _ => hε_top.symm ▸ le_top⟩
obtain ⟨s, _, hμs, hgε⟩ := hg.exists_eLpNorm_indicator_compl_lt hp_ne_top (coe_ne_zero.mpr hε.ne')
exact ⟨s, ne_of_lt hμs, fun _ => hgε.le⟩