uniformIntegrable_subsingleton — Mathlib

English

If ι is a subsingleton and p is a finite exponent with 1 ≤ p and p ≠ ∞, and every f_i belongs to L^p(μ), then the family f: i ↦ f_i is uniformly integrable.

Русский

Пусть индексный набор ι состоит из одного элемента; пусть 1 ≤ p и p ≠ ∞; если для каждого i выполнено f_i ∈ L^p(μ), то семейство f: i ↦ f_i является uniformly integrable.

LaTeX

$$$(Subsingleton\;\iota) \land (1 \le p) \land (p \neq \infty) \land (\forall i, \text{MemLp}(f_i)\;p\;\mu) \Rightarrow \mathrm{UniformIntegrable}(f,p,\mu)$$$

Lean4

/-- A single function is uniformly integrable in the probability sense. -/
theorem uniformIntegrable_subsingleton [Subsingleton ι] (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) (hf : ∀ i, MemLp (f i) p μ) :
    UniformIntegrable f p μ :=
  uniformIntegrable_finite hp_one hp_top hf

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