Pressure and divergence identities for the local energy inequality

For a weakly divergence-free square-integrable velocity slice u with weak gradient D, the trace ∑ₖ D_kk vanishes almost everywhere, and a locally integrable pressure p with square-integrable weak gradient G satisfies ∑ₖ ∫ u_k ψ Gₖ = -∑ₖ ∫ u_k p ∂ₖψ against a smooth compactly supported weight ψ. A pressure in L⁶ restricted by a bounded compactly supported factor is square integrable. These are the pressure identities of eq:reg-local-energy-forced.

theorem CKN.Leray.eLpNorm_mul_le_of_six {p h : Foundation.Parabolic.Vec3 → ℝ} (hp : MeasureTheory.AEStronglyMeasurable p MeasureTheory.volume) (hh : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) {K : Set Foundation.Parabolic.Vec3} (hK : MeasurableSet K) {M : ℝ} (hM : ∀ (x : Foundation.Parabolic.Vec3), |h x| ≤ M) (hhK : ∀ x ∉ K, h x = 0) : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => p x * h x) 2 MeasureTheory.volume ≤ ENNReal.ofReal M * (MeasureTheory.eLpNorm p (ENNReal.ofReal 6) MeasureTheory.volume * MeasureTheory.volume K ^ (1 / 3))

An L⁶ function times a bounded factor supported in a set of finite measure is square integrable.

theorem CKN.Leray.ae_sum_diag_eq_zero {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hdf : IsWeakDivFreeL2 u) {D : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3} (hD : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => D x k k) 2 MeasureTheory.volume) (hweak : ∀ (k : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => u x k) fun (x : Vec 3) => D x k) : ∀ᵐ (x : Foundation.Parabolic.Vec3), ∑ k : Fin 3, D x k k = 0

The trace of the weak gradient of a weakly divergence-free field vanishes.

theorem CKN.Leray.sum_integral_pressure_eq {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hdf : IsWeakDivFreeL2 u) {p : Foundation.Parabolic.Vec3 → ℝ} (hpl : MeasureTheory.LocallyIntegrable p MeasureTheory.volume) {G : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hG : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => G x k) 2 MeasureTheory.volume) (hpG : HasWeakGradientOn Set.univ p G) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hpψ : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => p x * (fderiv ℝ ψ x) (basisVec k)) 2 MeasureTheory.volume) : ∑ k : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), u x k * (ψ x * G x k) = -∑ k : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), u x k * (p x * (fderiv ℝ ψ x) (basisVec k))

The pressure identity ∑ₖ ∫ u_k ψ Gₖ = -∑ₖ ∫ u_k p ∂ₖψ.