Assoc Pressure Helmholtz

Supporting estimates for the Navier–Stokes development.

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

The time-dependent Newtonian potential of a smooth compactly supported space-time density, used in lem:helmholtz-test.

Equations

• CKN.Leray.associatedPressureNewtonianPotential h z = CKN.pressureNewtonianPotential (fun (y : CKN.Foundation.Parabolic.Vec3) => h (y, z.2)) z.1

theorem CKN.Leray.associatedPressureNewtonianPotential_contDiff {h : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : ContDiff ℝ (↑⊤) h) (hc : HasCompactSupport h) : ContDiff ℝ (↑⊤) (associatedPressureNewtonianPotential h)

This potential is jointly smooth, as required for the test-field Helmholtz decomposition in lem:helmholtz-test.

theorem CKN.Leray.associatedPressureNewtonianPotential_laplacian {h : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : ContDiff ℝ (↑⊤) h) (hc : HasCompactSupport h) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => associatedPressureNewtonianPotential h (x, z.2)) z.1 = h z

Each spatial slice of this potential solves its Poisson equation, as used in lem:helmholtz-test.

theorem CKN.Leray.associatedPressureNewtonianPotential_spatialPartial {h : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : ContDiff ℝ (↑⊤) h) (hc : HasCompactSupport h) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialPartialProd (associatedPressureNewtonianPotential h) i z = associatedPressureNewtonianPotential (spatialPartialProd h i) z

Spatial differentiation commutes with this Newtonian potential on smooth compactly supported data.

noncomputable def CKN.Leray.associatedPressureTestDivergence (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The divergence of a compactly supported smooth vector test, used in lem:helmholtz-test.

Equations

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

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

The three-dimensional curl of a compactly supported smooth vector test on each time slice, used in lem:helmholtz-test.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Leray.associatedPressureHelmholtzScalarPotential (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 × ℝ → ℝ

The scalar Newtonian potential in the test-field Helmholtz decomposition.

Equations

• CKN.Leray.associatedPressureHelmholtzScalarPotential φ = CKN.Leray.associatedPressureNewtonianPotential (CKN.Leray.associatedPressureTestDivergence φ)

noncomputable def CKN.Leray.associatedPressureHelmholtzVectorPotential (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

The vector Newtonian potential in the test-field Helmholtz decomposition.

Equations

• CKN.Leray.associatedPressureHelmholtzVectorPotential φ z j = -CKN.Leray.associatedPressureNewtonianPotential (CKN.Leray.associatedPressureTestCurlComponent φ j) z

theorem CKN.Leray.associatedPressureTestDivergence_contDiff {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) : ContDiff ℝ (↑⊤) (associatedPressureTestDivergence φ)

The divergence of a smooth test is smooth, as used in lem:helmholtz-test.

theorem CKN.Leray.associatedPressureTestDivergence_hasCompactSupport {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) : HasCompactSupport (associatedPressureTestDivergence φ)

The divergence of a compactly supported test has compact support, as used in lem:helmholtz-test.

theorem CKN.Leray.associatedPressureTestCurlComponent_contDiff {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (j : Fin 3) : ContDiff ℝ (↑⊤) (associatedPressureTestCurlComponent φ j)

Each component of the curl of a smooth test is smooth, as used in lem:helmholtz-test.

theorem CKN.Leray.associatedPressureTestCurlComponent_hasCompactSupport {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (j : Fin 3) : HasCompactSupport (associatedPressureTestCurlComponent φ j)

Each component of the curl of a compactly supported test has compact support, as used in lem:helmholtz-test.

theorem CKN.Leray.associatedPressureHelmholtzScalarPotential_contDiff {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) : ContDiff ℝ (↑⊤) (associatedPressureHelmholtzScalarPotential φ)

The scalar Helmholtz potential is jointly smooth, as required in lem:helmholtz-test.

theorem CKN.Leray.associatedPressureHelmholtzVectorPotential_contDiff {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) : ContDiff ℝ (↑⊤) (associatedPressureHelmholtzVectorPotential φ)

The vector Helmholtz potential is jointly smooth, as required in lem:helmholtz-test.