Divergence Identity

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

theorem CIV.zoomV_div_eq (lam h zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) (hR : p.1.1 ≠ 0) : zoomV lam h zc u p / p.1.1 = lam ^ 2 * (u (zoomPoint lam h zc p) 0 / (zoomPoint lam h zc p).1 0)

Off the axis, the rescaled radial velocity divided by r equals lam² times the meridional radial component at the zoomed point. This is the algebraic identity eq:aniso:zoom:fields for the V component.

theorem CIV.zoom_divergence_identity (lam h zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) (hR : p.1.1 ≠ 0) : dr (zoomV lam h zc u) p + zoomV lam h zc u p / p.1.1 + dz (zoomW lam h zc u) p = 0

The divergence of the rescaled velocity field vanishes pointwise on the meridional plane off the axis. This is eq:aniso:zoom:finite:identities — the zoom-in of the divergence-free condition.