The weighted swirl component of the scalar Navier–Stokes equation

For ψ = (−t)^η u_θ on the meridional plane {x₂ = 0} off the axis, the weighted swirl equation of lem:aniso:closure is: ∂_t ψ + u_r ∂_r ψ + u_z ∂_z ψ − (∂_r² ψ + r⁻¹ ∂_r ψ + ∂_z² ψ) + (r⁻² + u_r/r + η/(−t)) ψ = (−t)^η f_θ.

The weight depends only on time, so spatial derivatives factor through it. The time derivative picks up the extra term η/(−t) ψ from differentiating the weight. As in scalar_nse_swirl, the rotation invariance of the pressure is not assumed: it follows from the axisymmetry of the velocity and of the force (pressure_rotZ_invariant).

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