Scalar System R

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

theorem CIV.scalar_nse_r (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.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) z + u z 0 * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 z + u z 2 * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 z - u z 1 ^ 2 / z.1 0 = CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 0 z + CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 z / z.1 0 + CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 2 z - u z 0 / z.1 0 ^ 2 - CKN.spatialPartial p 0 z + f z 0

The radial component of eq:aniso:scalar:nse. Take the momentum equation at i = 0 from hsol.2.2.2.1 z hz 0, rewrite its convective sum with sum_convective_zero_meridional and its Laplacian sum with sum_spatialSecondPartial_zero_meridional, and rearrange. The centrifugal term -u_θ²/r comes from the convective rewrite and the -u_r/r² from the Laplacian rewrite.