Theorems · Theorem · measure theory

MeasureTheory.unifIntegrable_const

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

A constant function is uniformly integrable.

Defined in

Mathlib.MeasureTheory.Function.UniformIntegrable

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup