Vorticity Equation

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

theorem CIV.spatialPartial_eq_jointFDeriv {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hg : DifferentiableAt ℝ (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => g w) z) (i : Fin 3) : CKN.spatialPartial g i z = (fderiv ℝ (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => g w) z) (CKN.basisVec i, 0)

The classical spatial partial derivative is the joint Fréchet derivative applied to the embedded spatial direction.

theorem CIV.timePartial_eq_jointFDeriv {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hg : DifferentiableAt ℝ (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => g w) z) : CKN.timePartial g z = (fderiv ℝ (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => g w) z) (0, 1)

The classical time partial derivative is the joint Fréchet derivative applied to the embedded time direction.

theorem CIV.contDiffOn_spatialPartial {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial g i z) unitCylinder

If a scalar field is jointly smooth on the unit cylinder, so is each of its classical spatial partial derivatives.

theorem CIV.contDiffOn_timePartial {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.timePartial g z) unitCylinder

If a scalar field is jointly smooth on the unit cylinder, so is its classical time partial derivative.

theorem CIV.spatialSecondPartial_eq_jointFDeriv2 {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ unitCylinder) (i j : Fin 3) : CKN.spatialSecondPartial g i j z = ((fderiv ℝ (fderiv ℝ fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => g w) z) (CKN.basisVec j, 0)) (CKN.basisVec i, 0)

theorem CIV.spatialSecondPartial_comm {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ unitCylinder) (i j : Fin 3) : CKN.spatialSecondPartial g i j z = CKN.spatialSecondPartial g j i z

Cartesian mixed spatial partials of a jointly smooth scalar field commute.

theorem CIV.spatialPartial_timePartial_eq_jointFDeriv2 {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ unitCylinder) (i : Fin 3) : CKN.spatialPartial (CKN.timePartial g) i z = ((fderiv ℝ (fderiv ℝ fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => g w) z) (CKN.basisVec i, 0)) (0, 1)

theorem CIV.timePartial_spatialPartial_eq_jointFDeriv2 {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ unitCylinder) (i : Fin 3) : CKN.timePartial (CKN.spatialPartial g i) z = ((fderiv ℝ (fderiv ℝ fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => g w) z) (0, 1)) (CKN.basisVec i, 0)

theorem CIV.spatialPartial_timePartial_comm {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ unitCylinder) (i : Fin 3) : CKN.spatialPartial (CKN.timePartial g) i z = CKN.timePartial (CKN.spatialPartial g i) z

The classical spatial and time partial derivatives of a jointly smooth scalar field commute.

theorem CIV.hasDerivAt_meridional_zero {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {a b t : ℝ} (hz : (meridional a b, t) ∈ unitCylinder) : HasDerivAt (fun (s : ℝ) => g (meridional s b, t)) (CKN.spatialPartial g 0 (meridional a b, t)) a

Differentiating along the meridional plane in the radial direction, at fixed axial coordinate and time, gives the classical radial spatial partial derivative (the critical subtlety: eq:aniso:scalar:nse:r holds only on the meridional plane, so this one-dimensional chain rule, not a naive Cartesian derivative, is what lets us differentiate it).

theorem CIV.hasDerivAt_meridional_two {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {a b t : ℝ} (hz : (meridional a b, t) ∈ unitCylinder) : HasDerivAt (fun (s : ℝ) => g (meridional a s, t)) (CKN.spatialPartial g 2 (meridional a b, t)) b

Differentiating along the meridional plane in the axial direction, at fixed radial coordinate and time, gives the classical axial spatial partial derivative (the same critical subtlety as hasDerivAt_meridional_zero).

theorem CIV.hasDerivAt_meridional_zero_at {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) : HasDerivAt (fun (s : ℝ) => g (meridional s (z.1 2), z.2)) (CKN.spatialPartial g 0 z) (z.1 0)

hasDerivAt_meridional_zero, restated so the basepoint and derivative value are read off directly at the point itself.

theorem CIV.hasDerivAt_meridional_two_at {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) : HasDerivAt (fun (s : ℝ) => g (meridional (z.1 0) s, z.2)) (CKN.spatialPartial g 2 z) (z.1 2)

hasDerivAt_meridional_two, restated so the basepoint and derivative value are read off directly at the point itself.

theorem CIV.azimuthal_vorticity_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) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : CKN.timePartial (azimuthalVorticity u) z + u z 0 * CKN.spatialPartial (azimuthalVorticity u) 0 z + u z 2 * CKN.spatialPartial (azimuthalVorticity u) 2 z = u z 0 / z.1 0 * azimuthalVorticity u z + 1 / z.1 0 * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1 ^ 2) 2 z + (CKN.spatialSecondPartial (azimuthalVorticity u) 0 0 z + CKN.spatialPartial (azimuthalVorticity u) 0 z / z.1 0 + CKN.spatialSecondPartial (azimuthalVorticity u) 2 2 z - azimuthalVorticity u z / z.1 0 ^ 2) + (CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w 0) 2 z - CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w 2) 0 z)

The azimuthal vorticity equation eq:aniso:theta: away from the axis, the material derivative of the azimuthal vorticity of a classical, forced, axisymmetric solution equals its stretching by the radial velocity, the source ∂_z(u_θ²)/r, its cylindrical Laplacian, and the azimuthal component of the curl of the force.