Theorems · Theorem · measure theory

MeasureTheory.exists_measurable_le_lintegral_eq

∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
  ∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

For any function f : α → ℝ≥0∞, there exists a measurable function g ≤ f with the same integral.

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Cited by

8 results in Mathlib

Foundations

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