UniformIntegrable — Mathlib

English

If f is Uniformly Integrable with respect to μ, then restricting μ to a subset E preserves Uniform Integrability of f.

Русский

Если f униформно интегрируема относительно μ, то ограничение меры μ на подмножество E сохраняет униформную интегрируемость f.

LaTeX

$$$\\operatorname{UnifIntegrable} f p μ \\Rightarrow \\operatorname{UnifIntegrable} f p (μ\\restriction E)$$$

Lean4

/-- In probability theory, a family of measurable functions is uniformly integrable if it is
uniformly integrable in the measure theory sense and is uniformly bounded. -/
def UniformIntegrable {_ : MeasurableSpace α} (f : ι → α → β) (p : ℝ≥0∞) (μ : Measure α) : Prop :=
  (∀ i, AEStronglyMeasurable (f i) μ) ∧ UnifIntegrable f p μ ∧ ∃ C : ℝ≥0, ∀ i, eLpNorm (f i) p μ ≤ C

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