English
For a nonnegative function f on a measure space and p > 0, the p-th power integral equals p times the integral over t>0 of t^{p−1} times the measure of {ω : f(ω) ≥ t}. More precisely, ∫ f^p dμ = p ∫_0^∞ t^{p−1} μ{f ≥ t} dt.
Русский
Для неотрицательной функции f на мере μ верна формула слоя: ∫ f^p dμ = p ∫_0^∞ t^{p−1} μ{ω : f(ω) ≥ t} dt.
LaTeX
$$$\\displaystyle \\int^{\\infty}_{0} f(\\omega)^p \, d\\mu = p \\int_{0}^{\\infty} t^{p-1} \\mu\\{\\omega : f(\\omega) \\ge t\\} \, dt$$$
Lean4
/-- 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 lintegral_rpow_eq_lintegral_meas_le_mul {f : α → ℝ} (f_nn : 0 ≤ᵐ[μ] f) (f_mble : AEMeasurable f μ) {p : ℝ}
(p_pos : 0 < p) :
∫⁻ ω, ENNReal.ofReal (f ω ^ p) ∂μ =
ENNReal.ofReal p * ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) :=
by
have one_lt_p : -1 < p - 1 := by linarith
have obs : ∀ x : ℝ, ∫ t : ℝ in 0..x, t ^ (p - 1) = x ^ p / p :=
by
intro x
rw [integral_rpow (Or.inl one_lt_p)]
simp [Real.zero_rpow p_pos.ne.symm]
set g := fun t : ℝ => t ^ (p - 1)
have g_nn : ∀ᵐ t ∂volume.restrict (Ioi (0 : ℝ)), 0 ≤ g t :=
by
filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]
intro t t_pos
exact Real.rpow_nonneg (mem_Ioi.mp t_pos).le (p - 1)
have g_intble (t) (ht : 0 < t) : IntervalIntegrable g volume 0 t := intervalIntegral.intervalIntegrable_rpow' one_lt_p
have key := lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn
rw [← key, ← lintegral_const_mul'' (ENNReal.ofReal p)] <;> simp_rw [obs]
· congr with ω
rw [← ENNReal.ofReal_mul p_pos.le, mul_div_cancel₀ (f ω ^ p) p_pos.ne.symm]
· have aux := (measurable_const (a := p)).aemeasurable (μ := μ)
exact measurable_id.ennreal_ofReal.comp_aemeasurable <| (f_mble.pow aux).div_const p
