Theorems · Theorem · measure theory

MeasureTheory.unifIntegrable_finite

∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} [Finite ι],
  1 ≤ p → p ≠ ⊤ → ∀ {f : ι → α → β}, (∀ (i : ι), MeasureTheory.MemLp (f i) p μ) → MeasureTheory.UnifIntegrable f p μ

A finite sequence of Lp functions is uniformly integrable.

Defined in

Mathlib.MeasureTheory.Function.UniformIntegrable

Cited by

1 results in Mathlib

Foundations

Depth 224 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupFinite