mathlib documentation

measure_theory.integral.layercake

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 sigma-finite 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 two most common applications of the layer cake formula

Main results #

Tags #

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

Layercake theorem #

theorem measure_theory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable {α : Type u_1} [measurable_space α] {f : α → } {g : } (μ : measure_theory.measure α) [measure_theory.sigma_finite μ] (f_nn : 0 f) (f_mble : measurable f) (g_intble : ∀ (t : ), t > 0interval_integrable g measure_theory.measure_space.volume 0 t) (g_mble : measurable g) (g_nn : ∀ (t : ), t > 00 g t) :
∫⁻ (ω : α), ennreal.of_real (∫ (t : ) in 0..f ω, g t) μ = ∫⁻ (t : ) in set.Ioi 0, μ {a : α | t f a} * ennreal.of_real (g t)

An auxiliary version of the layer cake theorem (Cavalieri's principle, tail probability formula), with a measurability assumption that would also essentially follow from the integrability assumptions.

See measure_theory.layercake for the main formulation of the layer cake theorem.

theorem measure_theory.lintegral_comp_eq_lintegral_meas_le_mul {α : Type u_1} [measurable_space α] {f : α → } {g : } (μ : measure_theory.measure α) [measure_theory.sigma_finite μ] (f_nn : 0 f) (f_mble : measurable f) (g_intble : ∀ (t : ), t > 0interval_integrable g measure_theory.measure_space.volume 0 t) (g_nn : ∀ᵐ (t : ) ∂measure_theory.measure_space.volume.restrict (set.Ioi 0), 0 g t) :
∫⁻ (ω : α), ennreal.of_real (∫ (t : ) in 0..f ω, g t) μ = ∫⁻ (t : ) in set.Ioi 0, μ {a : α | t f a} * ennreal.of_real (g t)

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

Let f be a non-negative measurable function on a sigma-finite 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}.

theorem measure_theory.lintegral_eq_lintegral_meas_le {α : Type u_1} [measurable_space α] {f : α → } (μ : measure_theory.measure α) [measure_theory.sigma_finite μ] (f_nn : 0 f) (f_mble : measurable f) :
∫⁻ (ω : α), ennreal.of_real (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 sigma-finite measure space, the Lebesgue integral of f can be written (roughly speaking) as: ∫⁻ f ∂μ = ∫⁻ t in 0 .. ∞, μ {ω | f(ω) ≥ t}.

theorem measure_theory.lintegral_rpow_eq_lintegral_meas_le_mul {α : Type u_1} [measurable_space α] {f : α → } (μ : measure_theory.measure α) [measure_theory.sigma_finite μ] (f_nn : 0 f) (f_mble : measurable f) {p : } (p_pos : 0 < p) :
∫⁻ (ω : α), ennreal.of_real (f ω ^ p) μ = ennreal.of_real p * ∫⁻ (t : ) in set.Ioi 0, μ {a : α | t f a} * ennreal.of_real (t ^ (p - 1))

An application of the layer cake formula / Cavalieri's principle / tail probability formula:

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