Spatial interpolation for regularized velocities

The whole-space Gagliardo–Nirenberg estimate applies to almost every positive-time slice of a regularized velocity.

theorem CKN.Leray.regUniform_spatial_slice_tenThirds (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (hSlices : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ∃ (h : Fin 3 → H1Function Set.univ), (∀ (i : Fin 3) (x : Vec 3), (h i).toFun x = u (x, t) i) ∧ ∀ (i : Fin 3) (x : Vec 3) (j : Fin 3), (h i).grad x j = Du (x, t) i j) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ∀ (i : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u (x, t) i) (ENNReal.ofReal (10 / 3)) MeasureTheory.volume ≤ gagliardoNirenbergSobolevConstant ^ (3 / 5) * MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume ^ (2 / 5) * MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (Du (x, t) i)) 2 MeasureTheory.volume ^ (3 / 5)

The spatial L^{10/3} Gagliardo–Nirenberg estimate holds on almost every positive-time slice, component by component.

theorem CKN.Leray.regUniform_component_memLp_tenThirds (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (A D : ENNReal) (hSlices : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ∃ (h : Fin 3 → H1Function Set.univ), (∀ (i : Fin 3) (x : Vec 3), (h i).toFun x = u (x, t) i) ∧ ∀ (i : Fin 3) (x : Vec 3) (j : Fin 3), (h i).grad x j = Du (x, t) i j) (hSliceBound : ∀ (t : ℝ), 0 < t → ∀ (i : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume ≤ A) (hUmeasurable : Measurable u) (hDumeasurable : Measurable Du) (hGradientEnergyBound : ∫⁻ (t : ℝ) in Set.Ioi 0, ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (spatialGradientSq u Du (x, t)) ≤ D) (hAfinite : A < ⊤) (hDfinite : D < ⊤) (i : Fin 3) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioi 0))) ^ (10 / 3) ≤ (gagliardoNirenbergSobolevConstant ^ (3 / 5)) ^ (10 / 3) * A ^ (4 / 3) * D

Energy and dissipation bounds integrate the slice interpolation estimate to space-time L^{10/3}, component by component.