Assoc Pressure Helmholtz Identity

Supporting estimates for the Navier–Stokes development.

noncomputable def CKN.Leray.associatedPressureTestGradient (h : Foundation.Parabolic.Vec3 × ℝ → ℝ) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

The product-space gradient of a scalar test field.

Equations

• CKN.Leray.associatedPressureTestGradient h z i = CKN.spatialPartialProd h i z

noncomputable def CKN.Leray.associatedPressureTestLaplacianComponent (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (i : Fin 3) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The componentwise spatial Laplacian of a vector-valued pressure test field.

Equations

• CKN.Leray.associatedPressureTestLaplacianComponent φ i z = ∑ k : Fin 3, CKN.spatialPartialProd (CKN.spatialPartialProd (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ w i) k) k z

theorem CKN.Leray.associatedPressureHelmholtz_identity {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (z : Foundation.Parabolic.Vec3 × ℝ) : φ z = associatedPressureTestCurl (associatedPressureHelmholtzVectorPotential φ) z + associatedPressureTestGradient (associatedPressureHelmholtzScalarPotential φ) z

The smooth spatial Helmholtz decomposition of a compactly supported test field, as in lem:helmholtz-test.