unifTight_of_subsingleton — Mathlib

English

A finite family of Lp functions is uniformly tight.

Русский

Для конечного набора функций из Lp согласована униформная ограниченность.

LaTeX

$$$[Finite\\\\ ι]\\\\rightarrow \\\\operatorname{UnifTight} f p μ$ если ∀ i, f_i ∈ L^p(μ)$$

Lean4

/-- A single function is tight. -/
theorem unifTight_of_subsingleton [Subsingleton ι] (hp_top : p ≠ ∞) {f : ι → α → β} (hf : ∀ i, MemLp (f i) p μ) :
    UnifTight f p μ := fun ε hε ↦ by
  by_cases hε_top : ε = ∞
  · exact ⟨∅, by simp, fun _ => hε_top.symm ▸ le_top⟩
  by_cases hι : Nonempty ι
  case neg => exact ⟨∅, (by simp), fun i => False.elim <| hι <| Nonempty.intro i⟩
  obtain ⟨i⟩ := hι
  obtain ⟨s, _, hμs, hfε⟩ := (hf i).exists_eLpNorm_indicator_compl_lt hp_top (coe_ne_zero.2 hε.ne')
  refine ⟨s, ne_of_lt hμs, fun j => ?_⟩
  convert hfε.le

Похожие утверждения