Spatial multi-indices of order at most two

A spatial multi-index derivative of order at most two is the function itself, a single spatial partial, or an iterated partial; and the antisymmetric part of a velocity gradient is a signed vorticity component. Both are used in the interior estimates of the proof of lem:aniso:annulus.

theorem CIV.multiPartial_cases_of_order_le_two (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (α : Fin 3 → ℕ) (hα : α 0 + α 1 + α 2 ≤ 2) : multiPartial g α = g ∨ (∃ (j : Fin 3), multiPartial g α = CKN.spatialPartial g j) ∨ ∃ (j : Fin 3) (l : Fin 3), multiPartial g α = fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial g j w) l z

A spatial multi-index derivative of order at most two is the function itself, one partial, or an iterated partial.

theorem CIV.spatialPartial_antisymm_eq_smul_curlComp (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i j : Fin 3) : ∃ (m : Fin 3) (σ : ℝ), |σ| ≤ 1 ∧ ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j z - CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) i z = σ * curlComp u m z

The antisymmetric part of the velocity gradient is a signed vorticity component.