mathlib3 documentation

measure_theory.integral.layercake

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Main results #

Tags #

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

Layercake formula #

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 > 0 interval_integrable g measure_theory.measure_space.volume 0 t) (g_mble : measurable g) (g_nn : (t : ), t > 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)

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.

See measure_theory.lintegral_comp_eq_lintegral_meas_le_mul and measure_theory.lintegral_comp_eq_lintegral_meas_lt_mul for the main formulations of the layer cake formula.

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 > 0 interval_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 formula / 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}.

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

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}.

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

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}.

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

theorem measure.meas_le_ne_meas_lt_subset_meas_pos {α : Type u_1} [measurable_space α] (μ : measure_theory.measure α) {R : Type u_2} [linear_order R] [measurable_space R] [measurable_singleton_class R] {g : α R} (g_mble : measurable g) {t : R} (ht : μ {a : α | t g a} μ {a : α | t < g a}) :
0 < μ {a : α | g a = t}
theorem measure.countable_meas_le_ne_meas_lt {α : Type u_1} [measurable_space α] (μ : measure_theory.measure α) [measure_theory.sigma_finite μ] {R : Type u_2} [linear_order R] [measurable_space R] [measurable_singleton_class R] {g : α R} (g_mble : measurable g) :
{t : R | μ {a : α | t g a} μ {a : α | t < g a}}.countable
theorem measure.meas_le_ae_eq_meas_lt {α : Type u_1} [measurable_space α] (μ : measure_theory.measure α) [measure_theory.sigma_finite μ] {R : Type u_2} [linear_order R] [measurable_space R] [measurable_singleton_class R] (ν : measure_theory.measure R) [measure_theory.has_no_atoms ν] {g : α R} (g_mble : measurable g) :
(λ (t : R), μ {a : α | t g a}) =ᵐ[ν] λ (t : R), μ {a : α | t < g a}
theorem lintegral_comp_eq_lintegral_meas_lt_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 > 0 interval_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 formula / 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}.

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

theorem lintegral_eq_lintegral_meas_lt {α : 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}.

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

theorem lintegral_rpow_eq_lintegral_meas_lt_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}.

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