Whole-space Gagliardo–Nirenberg interpolation

The L^{10/3} inequality follows by interpolating between L² and the whole-space L⁶ Sobolev estimate for representative-level H¹ functions.

noncomputable def CKN.gagliardoNirenbergSobolevConstant : ENNReal

The chosen CKN whole-space Sobolev constant used in eq:gn-ten-thirds.

Equations

• CKN.gagliardoNirenbergSobolevConstant = Classical.choose CKN.sobolev_L6_global

theorem CKN.enorm_sq_le_vec3Euclidean_sq (v : Foundation.Parabolic.Vec3) : ‖v‖ₑ ^ 2 ≤ ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm v) ^ 2

The default Pi norm squared is bounded by the Euclidean velocity norm squared. This comparison is used when reading the Leray–Hopf slice bound.

theorem CKN.vec3Euclidean_sq_le_three_enorm_sq (v : Foundation.Parabolic.Vec3) : ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm v) ^ 2 ≤ 3 * ‖v‖ₑ ^ 2

The Euclidean velocity norm squared is bounded by three times the default Pi norm squared.

theorem CKN.h1_gagliardoNirenberg_tenThirds (v : H1Function Set.univ) : MeasureTheory.eLpNorm v.toFun (ENNReal.ofReal (10 / 3)) MeasureTheory.volume ≤ gagliardoNirenbergSobolevConstant ^ (3 / 5) * MeasureTheory.eLpNorm v.toFun 2 MeasureTheory.volume ^ (2 / 5) * MeasureTheory.eLpNorm (fun (x : Vec 3) => Foundation.Parabolic.vec3EuclideanNorm (v.grad x)) 2 MeasureTheory.volume ^ (3 / 5)

The whole-space L^{10/3} Gagliardo–Nirenberg inequality in eq:gn-ten-thirds. The L⁶ step is the CKN whole-space Sobolev theorem.