Calculus of vorticity test fields

The curl of a smooth compact test field commutes with time differentiation.

theorem ESS.vorticityTestPartial_timePartial_commute {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => vorticityTestPartial f i w) z = vorticityTestPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial f w) i z

noncomputable def ESS.vorticityTestTimePartial (f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : CKN.Foundation.Parabolic.ParabolicPoint → ℝ

The CKN time derivative of a scalar test in product coordinates.

Equations

• ESS.vorticityTestTimePartial f z = CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f (have this := w; this)) z

theorem ESS.vorticityTestCurl_timePartial {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : vorticityTestTimePartial (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => vorticityTestCurl ψ w i) z = vorticityTestCurl (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) (k : Fin 3) => vorticityTestTimePartial (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ y k) w) z i

The time derivative of the test curl is the curl of the time derivative, using CKN's factor-wise derivatives (manuscript lem:vorticity-weak-eq).