Force Quotient

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

theorem CIV.abs_azimuthalVorticity_le_of_forceC2Bounded {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {M : ℝ} (hM : ∀ z ∈ unitCylinder, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ M) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) : |azimuthalVorticity f z| ≤ 2 * M

If the force is C²-bounded by M, then the azimuthal vorticity is bounded by 2M.

theorem CIV.abs_spatialPartial_azimuthalVorticity_le_of_forceC2Bounded {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {M : ℝ} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hM : ∀ z ∈ unitCylinder, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ M) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) : |CKN.spatialPartial (azimuthalVorticity f) 0 z| ≤ 2 * M

If the force is C²-bounded by M and C^∞, then the radial derivative of the azimuthal vorticity is bounded by 2M.

theorem CIV.abs_potentialVorticity_force_le {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (hMf : ForceC2Bounded f) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x₁ x₃ t : ℝ), (meridional x₁ x₃, t) ∈ unitCylinder → |potentialVorticity f (meridional x₁ x₃, t)| ≤ C

If the force is C²-bounded and C^∞, then the potential vorticity of f is bounded on the unit cylinder.