The layer cake formula / Cavalieri's principle / tail probability formula

In this file we prove the following layer cake formula.

Consider a non-negative measurable function f on a measure space. Apply pointwise to it an increasing absolutely continuous function G : ℝ≥0 → ℝ≥0 vanishing at the origin, with derivative G' = g on the positive real line (in other words, G a primitive of a non-negative locally integrable function g on the positive real line). Then the integral of the result, ∫ G ∘ f, can be written as the integral over the positive real line of the "tail measures" of f (i.e., a function giving the measures of the sets on which f exceeds different positive real values) weighted by g. In probability theory contexts, the "tail measures" could be referred to as "tail probabilities" of the random variable f, or as values of the "complementary cumulative distribution function" of the random variable f. The terminology "tail probability formula" is therefore occasionally used for the layer cake formula (or a standard application of it).

The essence of the (mathematical) proof is Fubini's theorem.

We also give the most common application of the layer cake formula - a representation of the integral of a nonnegative function f: ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) ≥ t} dt

Variants of the formulas with measures of sets of the form {ω | f(ω) > t} instead of {ω | f(ω) ≥ t} are also included.

Main results

• MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul and MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul: The general layer cake formulas with Lebesgue integrals, written in terms of measures of sets of the forms {ω | t ≤ f(ω)} and {ω | t < f(ω)}, respectively.
• MeasureTheory.lintegral_eq_lintegral_meas_le and MeasureTheory.lintegral_eq_lintegral_meas_lt: The most common special cases of the layer cake formulas, stating that for a nonnegative function f we have ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) ≥ t} dt and ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) > t} dt, respectively.
• Integrable.integral_eq_integral_meas_lt: A Bochner integral version of the most common special case of the layer cake formulas, stating that for an integrable and a.e.-nonnegative function f we have ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) > t} dt.

See also

Another common application, a representation of the integral of a real power of a nonnegative function, is given in Mathlib/Analysis/SpecialFunctions/Pow/Integral.lean.

Tags

layer cake representation, Cavalieri's principle, tail probability formula

theorem MeasureTheory.countable_meas_le_ne_meas_lt {α : Type u_1} {R : Type u_2} [MeasurableSpace α] (μ : Measure α) [LinearOrder R] (g : α → R) : {t : R | μ {a : α | t ≤ g a} ≠ μ {a : α | t < g a}}.Countable

theorem MeasureTheory.meas_le_ae_eq_meas_lt {α : Type u_1} [MeasurableSpace α] (μ : Measure α) {R : Type u_3} [LinearOrder R] [MeasurableSpace R] (ν : Measure R) [NoAtoms ν] (g : α → R) : (fun (t : R) => μ {a : α | t ≤ g a}) =ᶠ[ae ν] fun (t : R) => μ {a : α | t < g a}

Layercake formula

theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : Measure α) [SFinite μ] (f_nn : 0 ≤ f) (f_mble : Measurable f) (g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t) (g_mble : Measurable g) (g_nn : ∀ 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.

theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : Measure α) (f_nn : 0 ≤ f) (f_mble : Measurable f) (g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t) (g_mble : Measurable g) (g_nn : ∀ 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. Compared to lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite, we remove the sigma-finite 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.

theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : Measure α) (f_nn : 0 ≤ᶠ[ae μ] f) (f_mble : AEMeasurable f μ) (g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t) (g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Set.Ioi 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)

The layer cake formula / Cavalieri's principle / tail probability formula:

Let f be a non-negative measurable function on a measure space. Let G be an increasing absolutely continuous function on the positive real line, vanishing at the origin, with derivative G' = g. Then the integral of the composition G ∘ f can be written as the integral over the positive real line of the "tail measures" μ {ω | f(ω) ≥ t} of f weighted by g.

Roughly speaking, the statement is: ∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0..∞, g(t) * μ {ω | f(ω) ≥ t}.

See MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul for a version with sets of the form {ω | f(ω) > t} instead.

theorem MeasureTheory.lintegral_eq_lintegral_meas_le {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (μ : Measure α) (f_nn : 0 ≤ᶠ[ae μ] f) (f_mble : AEMeasurable f μ) : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a : α | t ≤ f a}

The standard case of the layer cake formula / Cavalieri's principle / tail probability formula:

For a nonnegative function f on a measure space, the Lebesgue integral of f can be written (roughly speaking) as: ∫⁻ f ∂μ = ∫⁻ t in 0..∞, μ {ω | f(ω) ≥ t}.

See MeasureTheory.lintegral_eq_lintegral_meas_lt for a version with sets of the form {ω | f(ω) > t} instead.

theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : Measure α) (f_nn : 0 ≤ᶠ[ae μ] f) (f_mble : AEMeasurable f μ) (g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t) (g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Set.Ioi 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)

The layer cake formula / Cavalieri's principle / tail probability formula:

Let f be a non-negative measurable function on a measure space. Let G be an increasing absolutely continuous function on the positive real line, vanishing at the origin, with derivative G' = g. Then the integral of the composition G ∘ f can be written as the integral over the positive real line of the "tail measures" μ {ω | f(ω) > t} of f weighted by g.

Roughly speaking, the statement is: ∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0..∞, g(t) * μ {ω | f(ω) > t}.

See lintegral_comp_eq_lintegral_meas_le_mul for a version with sets of the form {ω | f(ω) ≥ t} instead.

theorem MeasureTheory.lintegral_eq_lintegral_meas_lt {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (μ : Measure α) (f_nn : 0 ≤ᶠ[ae μ] f) (f_mble : AEMeasurable f μ) : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a : α | t < f a}

The standard case of the layer cake formula / Cavalieri's principle / tail probability formula:

For a nonnegative function f on a measure space, the Lebesgue integral of f can be written (roughly speaking) as: ∫⁻ f ∂μ = ∫⁻ t in 0..∞, μ {ω | f(ω) > t}.

See lintegral_eq_lintegral_meas_le for a version with sets of the form {ω | f(ω) ≥ t} instead.

theorem MeasureTheory.Integrable.integral_eq_integral_meas_lt {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → ℝ} (f_intble : Integrable f μ) (f_nn : 0 ≤ᶠ[ae μ] f) : ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioi 0, μ.real {a : α | t < f a}

The standard case of the layer cake formula / Cavalieri's principle / tail probability formula:

For an integrable a.e.-nonnegative real-valued function f, the Bochner integral of f can be written (roughly speaking) as: ∫ f ∂μ = ∫ t in 0..∞, μ {ω | f(ω) > t}.

See MeasureTheory.lintegral_eq_lintegral_meas_lt for a version with Lebesgue integral ∫⁻ instead.

theorem MeasureTheory.Integrable.integral_eq_integral_meas_le {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → ℝ} (f_intble : Integrable f μ) (f_nn : 0 ≤ᶠ[ae μ] f) : ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioi 0, μ.real {a : α | t ≤ f a}

theorem MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → ℝ} {M : ℝ} (f_intble : Integrable f μ) (f_nn : 0 ≤ᶠ[ae μ] f) (f_bdd : f ≤ᶠ[ae μ] fun (x : α) => M) : ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 M, μ.real {a : α | t ≤ f a}