Differential operators on vorticity tests

Time derivatives, Laplacians, and curls of compact smooth tests retain the expected support and commute in the combinations used in lem:vorticity-weak-eq.

noncomputable def ESS.vorticityTestTimeDerivative (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3

The time derivative of a compact vector test, in ordinary product coordinates.

Equations

• ESS.vorticityTestTimeDerivative ψ z i = ESS.vorticityTestTimePartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ w i) (have this := z; this)

noncomputable def ESS.vorticityTestLaplacian (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3

The spatial Laplacian of a compact vector test, in ordinary product coordinates.

Equations

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

noncomputable def ESS.vorticityScalarLaplacian (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The spatial Laplacian of a scalar test function via the test-coordinate derivatives.

Equations

• ESS.vorticityScalarLaplacian φ z = ∑ j : Fin 3, ESS.vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => ESS.vorticityTestPartial φ j w) j z

theorem ESS.vorticityTestCurl_laplacian_commute {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : vorticityTestCurl (vorticityTestLaplacian ψ) z i = vorticityTestLaplacian (vorticityTestCurl ψ) z i

Curl and the spatial Laplacian commute on smooth vector tests.

theorem ESS.vorticityTestTimeDerivative_tsupport {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} : tsupport (vorticityTestTimeDerivative ψ) ⊆ tsupport ψ

The time derivative of a vector test is supported in the original test support.

theorem ESS.vorticityTestLaplacian_tsupport {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} : tsupport (vorticityTestLaplacian ψ) ⊆ tsupport ψ

The Laplacian of a vector test is supported in the original test support.

theorem ESS.vorticityTestTimeDerivative_mem_spaceTimeTestFunction {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hψ : ψ ∈ CKN.spaceTimeTestFunction Ω I) : vorticityTestTimeDerivative ψ ∈ CKN.spaceTimeTestFunction Ω I

Time differentiation preserves the compact CKN test class and its support.

theorem ESS.vorticityTestLaplacian_mem_spaceTimeTestFunction {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hψ : ψ ∈ CKN.spaceTimeTestFunction Ω I) : vorticityTestLaplacian ψ ∈ CKN.spaceTimeTestFunction Ω I

The spatial Laplacian preserves the compact CKN test class and its support.

theorem ESS.vorticityTestCurl_tsupport_subset {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} : tsupport (vorticityTestCurl ψ) ⊆ tsupport ψ

The curl of a smooth vector test is supported in the original test support.