Smoothness of a spatial partial derivative

noncomputable def CIV.azimuthalVorticity (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The azimuthal vorticity ω_θ = ∂_z u_r - ∂_r u_z of eq:aniso:vorticity.

Equations

• CIV.azimuthalVorticity u z = CIV.curlComp u 1 z

noncomputable def CIV.potentialVorticity (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

Ω = ω_θ / r, extended continuously across the axis.

Equations

• CIV.potentialVorticity u z = if z.1 0 = 0 then CKN.spatialPartial (CIV.azimuthalVorticity u) 0 z else CIV.azimuthalVorticity u z / z.1 0

theorem CIV.potentialVorticity_eq_div (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hr : z.1 0 ≠ 0) : potentialVorticity u z = azimuthalVorticity u z / z.1 0

Off the axis, the potential vorticity is the quotient ω_θ / r.

theorem CIV.azimuthalVorticity_axis {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (h0 : z.1 0 = 0) (h1 : z.1 1 = 0) : azimuthalVorticity u z = 0

The azimuthal vorticity of a smooth axisymmetric field vanishes on the axis.

theorem CIV.contDiffOn_azimuthalVorticity {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => azimuthalVorticity u z) unitCylinder

The azimuthal vorticity of a smooth field is smooth on the open unit cylinder.

The meridional segment through the axis

Smoothness of the axial slice of the azimuthal vorticity

The integral representation of the potential vorticity

theorem CIV.abs_potentialVorticity_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {x₁ x₃ t M : ℝ} (hz : (meridional x₁ x₃, t) ∈ unitCylinder) (hM : ∀ s ∈ Set.Icc 0 1, |CKN.spatialPartial (azimuthalVorticity u) 0 (meridional (s * x₁) x₃, t)| ≤ M) : |potentialVorticity u (meridional x₁ x₃, t)| ≤ M

Explicit mean-value bound for the potential vorticity: if the radial derivative of the azimuthal vorticity is bounded by M along the segment from the axis to (x₁, x₃), so is the potential vorticity Ω itself at (x₁, x₃).

Continuity of the parametric integral, jointly on the meridional plane

theorem CIV.continuousOn_potentialVorticity_plane (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (ht : t ∈ Set.Ioo (-1) 0) : ContinuousOn (fun (y : ℝ × ℝ) => potentialVorticity u (meridional y.1 y.2, t)) {y : ℝ × ℝ | y.1 ^ 2 + y.2 ^ 2 < 1}

On a time slice of the unit cylinder, the potential vorticity Ω = ω_θ / r (the paragraph after eq:aniso:circulation:pde) is continuous on the whole open disk of the meridional plane {x₂ = 0}, including the axis point x₁ = x₃ = 0.