Associated Pressure

Supporting estimates for the Navier–Stokes development.

theorem CKN.associatedPressure (T : ℝ) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) : IsLerayHopfSolution T a u Du → ∃ (p : Foundation.Parabolic.ParabolicPoint → ℝ), MeasureTheory.MemLp p (ENNReal.ofReal (5 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ (∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ i : Fin 3, u z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, 0 z i * φ z i = 0) ∧ (essSup (fun (t : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3) (MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤ → essSup (fun (t : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3), ‖p (x, t)‖ₑ ^ (3 / 2)) (MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤)

Every finite-time Leray–Hopf solution has an associated CKN pressure, as in thm:assoc-pressure.