An integral bound by superlevel-set norms

Integral Minkowski applied to the layer-cake representation bounds the Lᵖ seminorm of a function by the integral of the Lᵖ seminorms of its superlevel indicators. This form is useful when geometric inequalities control the measures of superlevel sets. Both sides are extended nonnegative numbers, so no integrability or finite-norm hypothesis is needed. The integral comparison is TauCeti.lintegral_Lp_lintegral_le.

theorem TauCeti.eLpNorm_le_lintegral_measure_norm_gt {α : Type u_1} {F : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [NormedAddCommGroup F] {f : α → F} (hf : MeasureTheory.AEStronglyMeasurable f μ) {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) : MeasureTheory.eLpNorm f p μ ≤ ∫⁻ (t : ℝ) in Set.Ioi 0, μ {x : α | t < ‖f x‖} ^ (1 / p.toReal)

The Lᵖ seminorm is bounded by the integral of the pth roots of the measures of norm-superlevel sets. This is integral Minkowski for the layer-cake representation, valid also when either side is infinite.