The integral of the real power of a nonnegative function

In this file, we give a common application of the layer cake formula --- a representation of the integral of the p:th power of a nonnegative function f: ∫ f(ω)^p ∂μ(ω) = p * ∫ t^(p-1) * μ {ω | f(ω) ≥ t} dt.

A variant of the formula with measures of sets of the form {ω | f(ω) > t} instead of {ω | f(ω) ≥ t} is also included.

Main results

• MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul and MeasureTheory.lintegral_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 * ∫ μ {ω | f(ω) ≥ t} * tᵖ⁻¹ dt and `∫ f(ω)ᵖ ∂μ(ω) = p * ∫ μ {ω | f(ω) > t} * tᵖ⁻¹ dt, respectively.

Tags

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

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

An application 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^p ∂μ = p * ∫⁻ t in 0..∞, t^(p-1) * μ {ω | f(ω) ≥ t}.

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

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

An application 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^p ∂μ = p * ∫⁻ t in 0..∞, t^(p-1) * μ {ω | f(ω) > t}.

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