ELp Norm Bridge

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.comparison_eLpNorm_top_of_ae_dominance {m : ℕ} {I : Set ℝ} {q : CKN.Vec m × ℝ → ℝ} (hq : IsLocallyBoundedOn m I q) (hstep : ∀ᵐ (τ₀ : ℝ) (τ : ℝ) ∂MeasureTheory.volume.restrict I, τ₀ < τ → ∀ (M : ℝ), (∀ᵐ (x : CKN.Vec m), |q (x, τ₀)| ≤ M) → ∀ᵐ (x : CKN.Vec m), |q (x, τ)| ≤ M) : ∀ᵐ (τ₀ : ℝ) (τ : ℝ) ∂MeasureTheory.volume.restrict I, τ₀ < τ → MeasureTheory.eLpNorm (fun (x : CKN.Vec m) => q (x, τ)) ⊤ MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : CKN.Vec m) => q (x, τ₀)) ⊤ MeasureTheory.volume

The L^∞ bridge in the comparison monotonicity argument: if, for almost every reference time τ₀ and almost every later time τ, every real number dominating the earlier slice x ↦ q (x, τ₀) almost everywhere also dominates the later slice x ↦ q (x, τ) almost everywhere, then the essential supremum of the later slice is bounded by the essential supremum of the earlier one. The earlier slice's essential supremum may itself be infinite, in which case the bound holds trivially; when it is finite, its own value serves as the dominating real number, so the hypothesis transfers it directly to the later slice.