English
Similarly, with the strict inequality version, ∫ f^p dμ equals p ∫_0^∞ t^{p−1} μ{f > t} dt for p > 0.
Русский
Аналогично для строгой неравенности: ∫ f^p dμ = p ∫_0^∞ t^{p−1} μ{f > t} dt, при p>0.
LaTeX
$$$\\displaystyle \\int^{\\infty}_{0} f(\\omega)^p \, d\\mu = p \\int_{0}^{\\infty} t^{p-1} \\mu\\{\\omega : f(\\omega) > 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_le_mul` for a version with sets of the form
`{ω | f(ω) ≥ t}` instead. -/
theorem lintegral_rpow_eq_lintegral_meas_lt_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
rw [lintegral_rpow_eq_lintegral_meas_le_mul μ f_nn f_mble p_pos]
apply congr_arg fun z => ENNReal.ofReal p * z
apply lintegral_congr_ae
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f] with t ht
rw [ht]
