unifIntegrable_subsingleton — Mathlib

English

If the index set is a singleton (Subsingleton ι), a single Lp-function family is uniformly integrable; this reduces to the constant-function case.

Русский

Если индексное множество синглетонно (одиночный элемент), то единственная функция в Lp-этоUniformIntegrable.

LaTeX

$$$[Subsingleton\ ι]\ →\ UnifIntegrable f p μ$$$

Lean4

/-- A single function is uniformly integrable. -/
theorem unifIntegrable_subsingleton [Subsingleton ι] (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) {f : ι → α → β}
    (hf : ∀ i, MemLp (f i) p μ) : UnifIntegrable f p μ :=
  by
  intro ε hε
  by_cases hι : Nonempty ι
  · obtain ⟨i⟩ := hι
    obtain ⟨δ, hδpos, hδ⟩ := (hf i).eLpNorm_indicator_le hp_one hp_top hε
    refine ⟨δ, hδpos, fun j s hs hμs => ?_⟩
    convert hδ s hs hμs
  · exact ⟨1, zero_lt_one, fun i => False.elim <| hι <| Nonempty.intro i⟩

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