The pressure-inclusive equation for the strong limit

The canonical double-Riesz pressure of a Leray--Hopf limit gives the unrestricted-test weak momentum identity.

theorem ESS.LPS.lps_limit_pressure_inclusive_weak_equation {T : ℝ} {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hLH : CKN.IsLerayHopfSolution T b u Du) : MeasureTheory.MemLp (CKN.Leray.associatedPressureForSolution hLH) (ENNReal.ofReal (5 / 3)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - CKN.Leray.associatedPressureForSolution hLH z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

The canonical associated pressure supplies the pressure-inclusive weak momentum equation for a Leray--Hopf limit.

theorem ESS.LPS.lps_associatedPressure_memLp_two_of_tensor_memLp_two {T : ℝ} {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hLH : CKN.IsLerayHopfSolution T b u Du) (hTensorTwo : ∀ (i j : Fin 3), MeasureTheory.MemLp (CKN.Leray.associatedPressureTensor T u i j) 2 MeasureTheory.volume) : MeasureTheory.MemLp (CKN.Leray.associatedPressureForSolution hLH) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

If the velocity tensor has space-time L² components, the associated double-Riesz pressure is also in space-time L².

theorem ESS.LPS.lps_limit_pressure_equation_with_l2_pressure {T : ℝ} {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hLH : CKN.IsLerayHopfSolution T b u Du) (hTensorTwo : ∀ (i j : Fin 3), MeasureTheory.MemLp (CKN.Leray.associatedPressureTensor T u i j) 2 MeasureTheory.volume) : MeasureTheory.MemLp (CKN.Leray.associatedPressureForSolution hLH) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - CKN.Leray.associatedPressureForSolution hLH z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

The limit equation and the L² pressure estimate are packaged together when the velocity tensor has square-integrable components.

theorem ESS.LPS.lps_velocity_memLp_four_of_uniform_h1_slices {T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (huMeas : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hGood : ∀ t ∈ Set.Ioo 0 T, IsLpsGoodTime u Du t) (B : ENNReal) (hB : B < ⊤) (huBound : ∀ t ∈ Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume ≤ B) (hDuBound : ∀ t ∈ Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, t)) 2 MeasureTheory.volume ≤ B) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (⇑CKN.Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

Uniform H¹ bounds on every positive-time slice give space-time L⁴ velocity on a finite slab by the interpolation estimate in lem:lps-H1-estimate.

theorem ESS.LPS.lps_associatedPressure_tensor_memLp_two_of_velocity_memLp_four {T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hU4 : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (⇑CKN.Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (i j : Fin 3) : MeasureTheory.MemLp (CKN.Leray.associatedPressureTensor T u i j) 2 MeasureTheory.volume

Space-time L⁴ velocity gives an L² velocity tensor on the finite slab, which is then extended by zero as in thm:assoc-pressure.

theorem ESS.LPS.lps_strong_limit_pressure_equation (ρ : CKN.Leray.RegMollifierProfile) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hb : (∀ (i : Fin 3), ∃ (h : CKN.H1Function Set.univ), (h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) => Db x i) ∧ CKN.IsInJ b) (T M : ℝ) (hT : 0 < T) (hM : 0 ≤ M) (hUniformBounds : ∀ (ε : ℝ) (hε : 0 < ε), have Uε := CKN.Leray.regR12Velocity ρ ε hε b ⋯; have Dε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Uε y i) j z; have D2ε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => Uε x i) j y) k z; (∀ t ∈ Set.Icc 0 T, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (Uε (x, t)) ^ 2 + CKN.spatialGradientSq Uε Dε (x, t) ≤ M) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, ∑ j : Fin 3, CKN.Foundation.Parabolic.vec3EuclideanNorm (D2ε z i j) ^ 2 ≤ M) (σ : ℕ → ℕ) (hσ : StrictMono σ) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hweakSlice : ∀ (t : ℝ), 0 < t → ∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), MeasureTheory.MemLp w 2 MeasureTheory.volume → Filter.Tendsto (fun (n : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.Leray.regR12Uε ρ b ⋯ (1 / (↑(σ n) + 1)) (x, t) i * w x i) Filter.atTop (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i))) (hrep : ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 < z.2 → u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) = CKN.Leray.compactnessMollifiedLimit (fun (n : ℕ) (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Leray.regR12Uε ρ b ⋯ (1 / (↑(σ n) + 1)) (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y)) σ z) (hLH : CKN.IsLerayHopfSolution T b u Du) : MeasureTheory.MemLp (CKN.Leray.associatedPressureForSolution hLH) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - CKN.Leray.associatedPressureForSolution hLH z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

The equation interface with the exact regularized uniform bounds and the space-time L⁴ velocity consequence supplied by compactness. The tensor bound follows from the limit's uniform H¹ slices.