Radial Quotient Branches

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

theorem CIV.radialQuotient_off_axis (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z.1 0 ≠ 0) : radialQuotient u z = u z 0 / z.1 0

When z is off the axis (z.1 0 ≠ 0), the radial quotient reduces to u z 0 / z.1 0.

theorem CIV.radialQuotient_on_axis (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z.1 0 = 0) : radialQuotient u z = CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 z

When z lies on the axis (z.1 0 = 0), the radial quotient is the spatial partial of u(·, 0) at 0 in direction z.1, i.e. ∂₁(u(·, 0))(0).