Theorems · Theorem · measure theory

MeasureTheory.uniformIntegrable_finite

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

A finite sequence of Lp functions is uniformly integrable in the probability sense.

Defined in

Mathlib.MeasureTheory.Function.UniformIntegrable

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupFinite