The lower Lebesgue integral of a function vanishing on a set of full measure #
On a finite measure space, a function into ℝ≥0∞ that vanishes on a set having the measure of the
whole space has zero lower Lebesgue integral. The set need not be measurable, nor the function
(a.e.-)measurable: the lower integral is the supremum over measurable minorants, each of which
vanishes almost everywhere.
Main statements #
TauCeti.lintegral_eq_zero_of_measure_setOf_eq_zero_eq_measure_univ: the lower integral of a function vanishing on a set of full measure is zero.
theorem
TauCeti.lintegral_eq_zero_of_measure_setOf_eq_zero_eq_measure_univ
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{f : Ω → ENNReal}
(h : μ {ω : Ω | f ω = 0} = μ Set.univ)
:
For a finite measure, if a function into ℝ≥0∞ vanishes on a set (not necessarily measurable)
whose measure equals that of the whole space, then its lower Lebesgue integral is zero.