The Cartesian vorticity equation

The display in the proof of lem:aniso:closure: taking the curl of the momentum equation of a classical solution gives ∂_t ω + (u·∇)ω − Δω = (ω·∇)u + curl f, a Cartesian identity holding on the whole open cylinder (not restricted to the meridional plane). The pressure drops out because mixed second partials commute, the time derivative commutes with the spatial partials, the Laplacian commutes with the curl by the same commutation, and the identity curl((u·∇)u) = (u·∇)ω − (ω·∇)u is the one place the divergence-free condition is used.

theorem CIV.cartesian_vorticity_pde (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u p f unitCylinder) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ unitCylinder) (i : Fin 3) : CKN.timePartial (curlComp u i) z + ∑ j : Fin 3, u z j * CKN.spatialPartial (curlComp u i) j z - ∑ j : Fin 3, CKN.spatialSecondPartial (curlComp u i) j j z = ∑ j : Fin 3, curlComp u j z * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j z + curlComp f i z

The Cartesian vorticity equation of lem:aniso:closure: taking the curl of the momentum equation of a classical solution gives ∂_t ω + (u·∇)ω − Δω = (ω·∇)u + curl f, holding at every point of the whole open cylinder (a Cartesian identity, not restricted to the meridional plane). The pressure cancels by spatialSecondPartial_comm, the time derivative commutes with the curl by spatialPartial_timePartial_comm (through spatialPartial_momentum), the Laplacian commutes with the curl by the same mixed-partial symmetry, and curl_convective_identity supplies the one step, curl((u·∇)u) = (u·∇)ω − (ω·∇)u, that uses the divergence-free condition.