Scalar System Div

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

theorem CIV.scalar_nse_div (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u p f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 z + u z 0 / z.1 0 + CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 z = 0

On the meridional plane, off the axis, the divergence equation eq:aniso:scalar:nse:div holds for a classical solution: ∂_r u_r + u_r/r + ∂_z u_z = 0.