Assoc Pressure Provider Limit

Supporting estimates for the Navier–Stokes development.

noncomputable def CKN.Leray.associatedPressureProviderMeasure (T : ℝ) : MeasureTheory.Measure (Foundation.Parabolic.Vec3 × ℝ)

Product volume on space and the open positive time interval ending at T.

Equations

• CKN.Leray.associatedPressureProviderMeasure T = MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T))

theorem CKN.Leray.associatedPressureForSolution_momentum_identity {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) (φ : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : φ ∈ 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 - associatedPressureForSolution hLH z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

The selected Riesz pressure gives the unrestricted-test momentum identity for every finite-time Leray--Hopf solution, as in thm:assoc-pressure.