The gradient of the smooth pressure against the transport term

For a smooth square-integrable pressure whose weak equation ∫ P Δψ = -∑ ∫ F_ij ∂_i∂_j ψ holds against every smooth compactly supported test function, the pressure equation ΔP = -∑ ∂_i c_i holds pointwise, where c_i = ∑_j ∂_j F_ji is the divergence of the tensor. Consequently ‖∇P‖² = -⟨c, ∇P⟩, the orthogonality behind the pressure gradient bound in the time derivative estimate of prop:lps-local-strong.

theorem ESS.LPS.lps_ibp_compactSupport {F g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (j : Fin 3) : ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv F j x * g x = -∫ (x : CKN.Foundation.Parabolic.Vec3), F x * CKN.spatialDeriv g j x

Integration by parts of a smooth function against a smooth compactly supported one.

theorem ESS.LPS.lps_pressure_laplacian_eq_neg_divergence {P : CKN.Foundation.Parabolic.Vec3 → ℝ} {F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hP : ContDiff ℝ (↑⊤) P) (hF : ∀ (i j : Fin 3), ContDiff ℝ (↑⊤) (F i j)) (hP0 : MeasureTheory.MemLp P 2 MeasureTheory.volume) (hP1 : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv P k) 2 MeasureTheory.volume) (hP2 : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (CKN.spatialDeriv P k) k) 2 MeasureTheory.volume) (hc0 : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, CKN.spatialDeriv (F j i) j x) 2 MeasureTheory.volume) (hc1 : ∀ (i : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, CKN.spatialDeriv (F j i) j x) i) 2 MeasureTheory.volume) (hweak : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : CKN.Foundation.Parabolic.Vec3), P x * CKN.spatialLaplacian ψ x = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), F i j x * CKN.mixedSecond ψ i j x) (x : CKN.Foundation.Parabolic.Vec3) : CKN.spatialLaplacian P x + ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, CKN.spatialDeriv (F j i) j y) i x = 0

The pressure equation holds pointwise for a smooth square-integrable pressure satisfying its weak form: ΔP = -∑ᵢ ∂ᵢ cᵢ with cᵢ = ∑ⱼ ∂ⱼ F_ji (prop:lps-local-strong).

theorem ESS.LPS.lps_pressure_gradient_sq_le {P : CKN.Foundation.Parabolic.Vec3 → ℝ} {F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hP : ContDiff ℝ (↑⊤) P) (hF : ∀ (i j : Fin 3), ContDiff ℝ (↑⊤) (F i j)) (hP0 : MeasureTheory.MemLp P 2 MeasureTheory.volume) (hP1 : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv P k) 2 MeasureTheory.volume) (hP2 : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (CKN.spatialDeriv P k) k) 2 MeasureTheory.volume) (hc0 : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, CKN.spatialDeriv (F j i) j x) 2 MeasureTheory.volume) (hc1 : ∀ (i : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, CKN.spatialDeriv (F j i) j x) i) 2 MeasureTheory.volume) (hweak : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : CKN.Foundation.Parabolic.Vec3), P x * CKN.spatialLaplacian ψ x = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), F i j x * CKN.mixedSecond ψ i j x) : ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv P i x ^ 2 ≤ ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), (∑ j : Fin 3, CKN.spatialDeriv (F j i) j x) ^ 2

The pressure gradient is bounded in L² by the divergence of the tensor: ∑ᵢ ‖∂ᵢ P‖² ≤ ∑ᵢ ‖cᵢ‖² (prop:lps-local-strong).