Theorems · Theorem · measure theory

MeasureTheory.exists_pos_setLIntegral_lt_of_measure_lt

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  ∫⁻ (x : α), f x ∂μ ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε

If f has finite integral, then ∫⁻ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero. This lemma states this fact in terms of ε and δ.

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Cited by

1 results in Mathlib

Foundations

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