Radial Quotient

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

noncomputable def CIV.radialQuotient (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The quotient u_r / r read on the meridional plane: u₁ / x₁ off the axis and ∂₁ u₁ on it. For a field that is smooth and axisymmetric, u₁ vanishes on the axis, so the axis value is the limit of u₁ / x₁: this is the manuscript's "u_r/r extended continuously across the axis" (paragraph after eq:aniso:G; design note R7).

Equations

• CIV.radialQuotient u z = if z.1 0 = 0 then CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 z else u z 0 / z.1 0