Local Energy L4

Supporting estimates for the Navier–Stokes development.

theorem CKN.scalarH1L4_bound {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (v : H1Function (euclideanBall x₀ r)) (h3 : MeasureTheory.MemLp v.toFun 3 (MeasureTheory.volume.restrict (euclideanBall x₀ r))) : MeasureTheory.MemLp v.toFun 4 (MeasureTheory.volume.restrict (euclideanBall x₀ r)) ∧ MeasureTheory.eLpNorm v.toFun 4 (MeasureTheory.volume.restrict (euclideanBall x₀ r)) ^ 4 ≤ MeasureTheory.eLpNorm v.toFun 3 (MeasureTheory.volume.restrict (euclideanBall x₀ r)) ^ 2 * (ENNReal.ofReal sobolevPoincareFaithfulC5 * (MeasureTheory.eLpNorm v.grad 2 (MeasureTheory.volume.restrict (euclideanBall x₀ r)) + (ENNReal.ofReal r)⁻¹ * MeasureTheory.eLpNorm v.toFun 2 (MeasureTheory.volume.restrict (euclideanBall x₀ r)))) ^ 2

The spatial interpolation step used for manuscript label lem:lei-L4 of the Escauriaza–Seregin–Šverák manuscript: an H¹ slice in L³ belongs to L⁴, with a bound that retains the L³ factor and the Sobolev L⁶ factor for later time integration.