uniformIntegrable_const — Mathlib

English

A constant sequence of functions g is uniformly integrable for any index set, provided p is finite and g ∈ L^p(μ).

Русский

Пусть константная последовательность функций g является элементом L^p(μ) и p конечен; тогда она равномерно интегрируема.

LaTeX

$$$(1 \le p) \land (p \neq \infty) \land (\mathrm{MemLp}\,g\;p\;\mu) \Rightarrow \mathrm{UniformIntegrable}( (\lambda\_, g),p,\mu)$$$

Lean4

/-- A constant sequence of functions is uniformly integrable in the probability sense. -/
theorem uniformIntegrable_const {g : α → β} (hp : 1 ≤ p) (hp_ne_top : p ≠ ∞) (hg : MemLp g p μ) :
    UniformIntegrable (fun _ : ι => g) p μ :=
  ⟨fun _ => hg.1, unifIntegrable_const hp hp_ne_top hg,
    ⟨(eLpNorm g p μ).toNNReal, fun _ => le_of_eq (ENNReal.coe_toNNReal hg.2.ne).symm⟩⟩

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