Energy interpolation for Leray--Hopf fields

The spatial and space-time interpolation estimates are the energy interpolation used in lem:u-ten-thirds and eq:gn-ten-thirds.

noncomputable def CKN.energyInterpolationSobolevConstant : ℝ

The Sobolev constant chosen from the ball-time interpolation estimate.

Equations

• CKN.energyInterpolationSobolevConstant = Classical.choose CKN.ball_time_sobolev

noncomputable def CKN.ballTimeSobolevConstant : ℝ

The constant in the ball-time Sobolev interpolation estimate.

Equations

• CKN.ballTimeSobolevConstant = CKN.energyInterpolationSobolevConstant

noncomputable def CKN.energyTenThirdsConstant : ENNReal

The global energy interpolation constant for the L^{10/3} bound.

Equations

• CKN.energyTenThirdsConstant = ENNReal.ofReal (3 ^ (2 / 3)) * 3 * ENNReal.ofReal CKN.energyInterpolationSobolevConstant

theorem CKN.lerayHopf_memLp_tenThirds {T : ℝ} {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hLH : IsLerayHopfSolution T a u Du) : MeasureTheory.MemLp u (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ (10 / 3) ≤ energyTenThirdsConstant * (essSup (fun (s : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, s))) ^ 2) (MeasureTheory.volume.restrict (Set.Ioo 0 T)) ^ (2 / 3) * ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), ENNReal.ofReal (spatialGradientSq u Du z))

lem:u-ten-thirds, with its first quantitative bound and the resulting space-time L^{10/3} membership. The vector constant includes the finite dimensional aggregation from its three scalar components.