L6 From Gradient

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

theorem CIV.lintegral_pow_six_le_of_eq_on_ball {C : ℝ} (hC : 0 < C) (hsob : ∀ (g : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ 1 g → HasCompactSupport g → MeasureTheory.eLpNorm g 6 MeasureTheory.volume ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm (fderiv ℝ g) 2 MeasureTheory.volume) {u g : CKN.Foundation.Parabolic.Vec3 → ℝ} {ρ : ℝ} (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (heq : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ, g x = u x) : (∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 ρ, ENNReal.ofReal |u x| ^ 6) ^ (1 / 6) ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm (fderiv ℝ g) 2 MeasureTheory.volume

If u agrees with a C¹ compactly supported function g on a ball of radius ρ, then the L⁶ norm of u on that ball is controlled by the L² norm of the gradient of g.

This is the key estimate used in the closure argument of lem:aniso:closure to bound local L⁶ averages by global energy quantities.