The Navier–Stokes forcing of the local solution

For the forcing tensor G = -(U ⊗ U + p I) of prop:pv-local-solution, cut off to the slab ℝ³ × (0, σ) with the canonical Riesz pressure p, we show that almost every time slice is double-divergence free, ∑_{ij} ∫ G_ij ∂_i∂_j φ = 0, which is the equation -Δp = ∂_i∂_j(U_i U_j), and that the pressure lies in L^{5/3} of the slab when U ∈ L² ∩ L⁴ there.

theorem ESS.mixedSecond_continuous_hasCompactSupport {φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (i j : Fin 3) : Continuous (CKN.mixedSecond φ i j) ∧ HasCompactSupport (CKN.mixedSecond φ i j)

Second derivatives of a smooth compactly supported function are continuous with compact support.

theorem ESS.integrable_mul_of_memLp_two_of_hasCompactSupport {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : Continuous g) (hgc : HasCompactSupport g) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) MeasureTheory.volume

A square integrable function times a continuous compactly supported function is integrable.

theorem ESS.pvSlabForce_doubleDiv {σ : ℝ} {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hT2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ U U i j) (ENNReal.ofReal 2) MeasureTheory.volume) : ∀ᵐ (s : ℝ), ∀ (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∑ i : Fin 3, ∑ j : Fin 3, ∫ (y : CKN.Foundation.Parabolic.Vec3), pvSlabForce σ U i j (y, s) * CKN.mixedSecond φ i j y = 0

The Navier–Stokes forcing tensor with the canonical pressure is double divergence free on almost every time slice: -Δp = ∂_i∂_j(U_i U_j).

theorem ESS.pvSlab_holderTriple_tenThirds : (ENNReal.ofReal (10 / 3)).HolderTriple (ENNReal.ofReal (10 / 3)) (ENNReal.ofReal (5 / 3))

A Hölder triple for the quadratic tensor at exponent 5/3.

theorem ESS.pvSlabPressure_memLp_fiveThirds {σ : ℝ} {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hU2 : MeasureTheory.MemLp U 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))) (hU4 : MeasureTheory.MemLp U (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))) : MeasureTheory.MemLp (pvSlabPressure σ U) (ENNReal.ofReal (5 / 3)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))

The canonical pressure of a velocity in L² ∩ L⁴ of the slab lies in L^{5/3} of the slab.