Stretching Identity

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

theorem CIV.stretching_meridional {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : ∑ i : Fin 3, ∑ j : Fin 3, curlComp u j z * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j z * curlComp u i z = CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 z * curlComp u 0 z ^ 2 + u z 0 / z.1 0 * curlComp u 1 z ^ 2 + CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 z * curlComp u 2 z ^ 2 + (CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 z + CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 z) * curlComp u 0 z * curlComp u 2 z - 2 * (u z 1 / z.1 0) * curlComp u 0 z * curlComp u 1 z

The vortex-stretching term eq:aniso:closure:stretch evaluated on the meridional plane. When an axisymmetric field is smooth and the point is off the axis, the sum ∑_i ∑_j ω_j ∂_j u_i ω_i collapses to the algebraic expression on the right-hand side. The proof expands both Fin 3 sums, replaces the three ∂_1 derivatives by their θ-relation values, and clears denominators.