Vorticity Divergence Form

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

def CIV.serrinForceFlux (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i m : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

Antisymmetric force flux, with ∑ₘ ∂ₘ F_{im} = (curl f)_i.

Equations

• CIV.serrinForceFlux f i m z = if m = i + 1 then f z (i + 2) else if m = i + 2 then -f z (i + 1) else 0

noncomputable def CIV.serrinVortFlux (u f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i m : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

Divergence-form flux of the vorticity equation, ω_m u_i - u_m ω_i + F_{im}.

Equations

• CIV.serrinVortFlux u f i m z = CIV.curlComp u m z * u z i - u z m * CIV.curlComp u i z + CIV.serrinForceFlux f i m z

theorem CIV.sum_spatialPartial_curlComp_eq_zero {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ unitCylinder → ∑ m : Fin 3, CKN.spatialPartial (curlComp u m) m z = 0

The sum of spatial partial derivatives of the vorticity components vanishes on the unit cylinder. This is the key cancellation ∑_m ∂_m ω_m = 0 that follows from the antisymmetry of the curl.

theorem CIV.spatialPartial_mul_of_contDiffOn {a b : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (ha : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => a z) unitCylinder) (hb : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => b z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (j : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => a w * b w) j z = CKN.spatialPartial a j z * b z + a z * CKN.spatialPartial b j z

Product rule for the classical spatial partial derivative on the unit cylinder: when both factors are smooth, the derivative of the product is the sum of the standard Leibniz terms.

theorem CIV.sum_spatialPartial_serrinForceFlux {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ unitCylinder → ∀ (i : Fin 3), ∑ m : Fin 3, CKN.spatialPartial (serrinForceFlux f i m) m z = curlComp f i z

The divergence of the antisymmetric force flux equals the curl of the forcing: ∑_m ∂_m F_{im} = (curl f)_i.

theorem CIV.vorticity_divergence_form {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hcl : IsClassicalSolutionOn u p f unitCylinder) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ unitCylinder → ∀ (i : Fin 3), CKN.timePartial (curlComp u i) z - ∑ m : Fin 3, CKN.spatialSecondPartial (curlComp u i) m m z = ∑ m : Fin 3, CKN.spatialPartial (serrinVortFlux u f i m) m z

The vorticity equation in divergence form on the unit cylinder: ∂_t ω − Δω = div(ω ⊗ u − u ⊗ ω) + curl f, i.e. the form in which the interior estimates of the proof of lem:aniso:annulus use it.