unifIntegrable_const — Mathlib

English

A constant function g with any index i forms a uniformly integrable family; this is the special case of a constant sequence is uniformly integrable.

Русский

Постоянная функция образует униформно интегрируемое семейство; частный случай азимитированной константы.

LaTeX

$$$\text{UnifIntegrable }f p μ$ когда $f(i)\equiv g$ константа по i$$

Lean4

/-- A constant function is uniformly integrable. -/
theorem unifIntegrable_const {g : α → β} (hp : 1 ≤ p) (hp_ne_top : p ≠ ∞) (hg : MemLp g p μ) :
    UnifIntegrable (fun _ : ι => g) p μ := by
  intro ε hε
  obtain ⟨δ, hδ_pos, hgδ⟩ := hg.eLpNorm_indicator_le hp hp_ne_top hε
  exact ⟨δ, hδ_pos, fun _ => hgδ⟩

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