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
- a representation of the integral of a nonnegative function f: ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) ≥ t} dt
- a representation of the integral of the p:th power of a nonnegative function f: ∫ f(ω)^p ∂μ(ω) = p * ∫ t^(p-1) * μ {ω | 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 #
lintegral_comp_eq_lintegral_meas_le_mulandlintegral_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.lintegral_eq_lintegral_meas_leandlintegral_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.lintegral_rpow_eq_lintegral_meas_le_mulandlintegral_rpow_eq_lintegral_meas_lt_mul: Other common special cases of the layer cake formulas, stating that for a nonnegative function f and p > 0, we have ∫ f(ω)^p ∂μ(ω) = p * ∫ μ {ω | f(ω) ≥ t} * t^(p-1) dt and ∫ f(ω)^p ∂μ(ω) = p * ∫ μ {ω | f(ω) > t} * t^(p-1) dt, respectively.
Tags #
layer cake representation, Cavalieri's principle, tail probability formula
Layercake formula #
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.
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.
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.
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.
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.
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.
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.