A power-mean estimate for time majorants

An extended-real estimate used when a slice majorant is integrated in time over the backward window of a parabolic cell: a power-mean bound that trades a sub-unit power for the total mass.

theorem CKN.Core.Step4.lintegral_rpow_le_rpow_lintegral_mul_measure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {J : α → ENNReal} (hJ : AEMeasurable J μ) {θ : ℝ} (hθ0 : 0 < θ) (hθ1 : θ < 1) : ∫⁻ (s : α), J s ^ θ ∂μ ≤ (∫⁻ (s : α), J s ∂μ) ^ θ * μ Set.univ ^ (1 - θ)

Jensen/Hoelder on a finite measure space: a sub-unit power of an integral dominates the integral of the power, at the cost of the total mass.