Layer Cake

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Measure.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ENNReal} (hf : Measurable f) {p : ℝ} (hp : 0 < p) (hfinite : ∀ᵐ (z : α) ∂μ, f z < ⊤) : ∫⁻ (z : α), f z ^ p ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, μ {z : α | ENNReal.ofReal t < f z} * ENNReal.ofReal (t ^ (p - 1))

The layer-cake formula for the p-th power integral of an a.e.-finite measurable ℝ≥0∞-valued function: ∫⁻ f^p ∂μ = p * ∫⁻_{t>0} μ {f > t} * t^(p-1) dt.