Theorems · Theorem · measure theory

MeasureTheory.exists_measurable_le_forall_setLIntegral_eq

∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (f : α → ENNReal),
  ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

If μ is an s-finite measure, then for any function f there exists a measurable function g ≤ f that has the same Lebesgue integral over every set. For the integral over the whole space, the statement is true without extra assumptions, see exists_measurable_le_lintegral_eq. See also MeasureTheory.Measure.restrict_toMeasurable_of_sFinite for a similar result.

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasureTheory.SFinite