Potential Vorticity Rescaled

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

noncomputable def CIV.zoomOmega (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

The rescaled potential vorticity Ω_n = λ³ δ Ω of eq:aniso:zoom:fields.

Equations

• CIV.zoomOmega lam h zc u p = lam ^ 3 * lam ^ (2 * h) * CIV.potentialVorticity u (CIV.zoomPoint lam h zc p)

theorem CIV.zoomOmega_eq (lam h zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) (hR : p.1.1 ≠ 0) : zoomOmega lam h zc u p = ((lam ^ (2 * h)) ^ 2 * dz (zoomV lam h zc u) p - dr (zoomW lam h zc u) p) / p.1.1