Theorems · Theorem · measure theory

MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le

∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
  [MeasureTheory.SigmaFinite (μ.trim hm)] (C : ENNReal) {f : α → ENNReal},
  (∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C) → ∫⁻ (x : α), f x ∂μ ≤ C

If the Lebesgue integral of a function is bounded by some constant on all sets with finite measure in a sub-σ-algebra and the measure is σ-finite on that sub-σ-algebra, then the integral over the whole space is bounded by that same constant.

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFinite