Carleson/ToMathlib/MeasureTheory/Integral/Layercake.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

5 declarations, 0 contain sorry, 0 declared as axioms

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

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

Imports (4)
Imported by 2 files
  1. theorem MeasureTheory.lintegral_comp_eq_lintegral_distribution_mul The layer cake formula / Cavalieri's principle / tail probability formula: Let f be a non-negative measurable function on a measure space line 376 source

    Source documentation

    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_le_mul for a version with sets of the form {ω | f(ω) ≥ t} instead.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, Measurable, AEMeasurable, MeasureTheory.MeasureSpace.volume, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.Iio, HMul.hMul, MeasureTheory.distribution

    Proof uses: MeasureTheory.Measurable.ennreal_induction', MeasureTheory.SimpleFunc.induction, MeasureTheory.SimpleFunc, Set, MeasurableSet, Eq.mpr, MeasureTheory.SimpleFunc.piecewise, MeasureTheory.SimpleFunc.const, OfNat.ofNat, Set.indicator, Function.const, id, congr, congrArg, funext, congrFun', congrFun, Set.piecewise, Classical.propDecidable, Membership.mem and 101 more

    135 instances, coercions and auxiliary constants left out.

    Tactic trace: 110 steps

    Open to load the checked before-and-after goal states.

    theorem lintegral_comp_eq_lintegral_distribution_mul (μ : Measure α)
    (f_mble : Measurable f) (g_mble : AEMeasurable g) :
    ∫⁻ ω, (∫⁻ t in (Iio (f ω)), g t) ∂μ =
      ∫⁻ t, distribution f t μ * g t := by
…

    Mentions: g, MeasureTheory.distribution

  2. theorem MeasureTheory.lintegral_comp_eq_lintegral_distribution_mul' line 479 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, AEMeasurable, MeasureTheory.MeasureSpace.volume, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.Iio, HMul.hMul, MeasureTheory.distribution

    Proof uses: And, Measurable, Filter.EventuallyEq, MeasureTheory.ae, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, MeasureTheory.lintegral_congr_ae, Filter.mp_mem, Set.ofPred, Filter.univ_mem', Membership.mem, Set, id, Eq.rec, Preorder, funext and 3 more

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

    Open to load the checked before-and-after goal states.

  3. theorem MeasureTheory.lintegral_eq_lintegral_distribution Documented declaration: lintegral_eq_lintegral_distribution line 499 source

    Source documentation

    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.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, AEMeasurable, Eq, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, MeasureTheory.distribution

    Proof uses: MeasureTheory.Measure.restrict, Set.Iio, OfNat.ofNat, HMul.hMul, MeasureTheory.lintegral_comp_eq_lintegral_distribution_mul', aemeasurable_const, Eq.mpr, id, congrArg, Eq.symm, Eq.mp, funext, mul_one, Eq.rec, Eq.refl, Set, MeasureTheory.setLIntegral_const, ENNReal.volume_Iio, one_mul

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

    theorem lintegral_eq_lintegral_distribution (μ : Measure α)
    (f_mble : AEMeasurable f μ) :
    ∫⁻ ω, f ω ∂μ = ∫⁻ t, distribution f t μ := by
…

    Mentions: MeasureTheory.distribution

  4. theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul' The layer cake formula / Cavalieri's principle / tail probability formula: Let f be a non-negative measurable function on a measure space line 529 source

    Source documentation

    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_distribution_mul for a version with sets of the form {ω | f(ω) > t} instead.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, AEMeasurable, MeasureTheory.MeasureSpace.volume, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.Iio, HMul.hMul, Set, Set.ofPred, LE.le

    Proof uses: Eq.mpr, MeasureTheory.distribution, id, congrArg, MeasureTheory.lintegral_comp_eq_lintegral_distribution_mul', LT.lt, ENorm.enorm, MeasureTheory.lintegral_congr_ae, Filter.mp_mem, MeasureTheory.ae, MeasureTheory.meas_le_ae_eq_meas_lt, Filter.univ_mem', Membership.mem, Eq.refl

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

    theorem lintegral_comp_eq_lintegral_meas_le_mul' (μ : Measure α)
    (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g) :
    ∫⁻ ω, (∫⁻ t in Set.Iio (f ω), g t) ∂μ =
      ∫⁻ t, μ {a : α | t ≤ f a} * g t := by
…

    Mentions: g

  5. theorem MeasureTheory.lintegral_eq_lintegral_meas_le' Documented declaration: lintegral_eq_lintegral_meas_le' line 548 source

    Source documentation

    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.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, AEMeasurable, Eq, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, Set, Set.ofPred, LE.le

    Proof uses: Eq.mpr, MeasureTheory.distribution, id, congrArg, MeasureTheory.lintegral_eq_lintegral_distribution, LT.lt, ENorm.enorm, MeasureTheory.lintegral_congr_ae, Filter.mp_mem, MeasureTheory.ae, MeasureTheory.meas_le_ae_eq_meas_lt, Filter.univ_mem', Membership.mem, Eq.refl

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

    theorem lintegral_eq_lintegral_meas_le' (μ : Measure α)
    (f_mble : AEMeasurable f μ) :
    ∫⁻ ω, f ω ∂μ = ∫⁻ t, μ {a : α | t ≤ f a} := by
…