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 ∂μ(ω) = 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

theorem MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (μ : MeasureTheory.Measure α) (f_nn : 0 ≤ᵐ[μ] 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 α] {f : α → ℝ} (μ : MeasureTheory.Measure α) (f_nn : 0 ≤ᵐ[μ] 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.