Theorems · Theorem · measure theory

MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite

∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α)
  [MeasureTheory.SFinite μ],
  0 ≤ f →
    Measurable f →
      (∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
        Measurable g →
          (∀ t > 0, 0 ≤ g t) →
            ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
              ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

An auxiliary version of the layer cake formula (Cavalieri's principle, tail probability formula), with a measurability assumption that would also essentially follow from the integrability assumptions, and a sigma-finiteness assumption. See MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul and MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul for the main formulations of the layer cake formula.

Defined in

Mathlib.MeasureTheory.Integral.Layercake

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasureTheory.SFinite