Theorems · Theorem · measure theory

MeasureTheory.setLIntegral_mono_ae

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal},
  AEMeasurable g (μ.restrict s) → (∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x) → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Lebesgue integral over a set is monotone in function. This version assumes that the upper estimate is an a.e. measurable function and the estimate holds a.e. on the set. See also setLIntegral_mono_ae' for a version that assumes measurability of the set but assumes no regularity of either function.

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Cited by

5 results in Mathlib

Foundations

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