First-derivative and Lipschitz bounds for the rescaled potential vorticity

Step 2 of the finite-h zoom-in argument, away from the axis. On a rectangle contained in {R ≥ ε} the rescaled potential vorticity Ω_n of eq:aniso:zoom:fields has first spatial derivatives bounded uniformly in the zoom scale.

Off the axis Ω_n = (δ² ∂_Z V_n − ∂_R W_n)/R (eq:aniso:zoom:finite:identities), so the quotient rule expresses ∂_R Ω_n and ∂_Z Ω_n through the first and second derivatives of V_n and W_n, each of which obeys one of the twelve rescaled bounds of eq:aniso:zoom:derivatives. Every exponent appearing there is at most -1/2 when 0 ≤ h ≤ 1/2, so for τ ≤ -1 all six inputs are bounded by C (-τ)^{-1/2}, and R ≥ ε turns the two denominators into the constants ε^{-1} and ε^{-2}:

|∂_R Ω_n| ≤ 2C(ε⁻¹ + ε⁻²)(-τ)^{-1/2},   |∂_Z Ω_n| ≤ 2Cε⁻¹(-τ)^{-1/2}.

The vertical derivative needs the mixed second derivative ∂_Z ∂_R W_n, which the second-order chain rules produce in the opposite order ∂_R ∂_Z W_n; the two agree by the symmetry of the Cartesian mixed spatial partials of the velocity, which is why the smoothness hypothesis here is C^∞ rather than C² (a classical solution supplies exactly this).

Integrating these two bounds along the two coordinate edges of a rectangle gives the Lipschitz-in-space bound with the τ-independent constant 2C(2ε⁻¹ + ε⁻²), which is the input of the equicontinuity argument.

Elementary inequalities

The two pieces of the numerator, differentiated along a coordinate slice

The rescaled potential vorticity differentiated along a coordinate slice

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

Off the axis, Ω_n restricted to a radial slice is differentiable, with the derivative the quotient rule applied to eq:aniso:zoom:finite:identities.

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

Off the axis, Ω_n restricted to a vertical slice is differentiable.

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

The quotient rule for ∂_R Ω_n off the axis.

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

The quotient rule for ∂_Z Ω_n off the axis.

The uniform first-derivative bounds

theorem CIV.abs_dr_zoomOmega_le {C h lam zc eps : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) (hdelta : lam ^ (2 * h) ≤ 1) (heps : 0 < eps) {p : (ℝ × ℝ) × ℝ} (hR : eps ≤ p.1.1) (hp : zoomPoint lam h zc p ∈ unitCylinder) (htau : p.2 ≤ -1) : |dr (zoomOmega lam h zc u) p| ≤ 2 * C * (1 / eps + 1 / eps ^ 2) * (-p.2) ^ (-(1 / 2))

The radial derivative of Ω_n on {R ≥ ε}, uniformly in the zoom scale, with the exponent -1/2 of eq:aniso:zoom:derivatives.

theorem CIV.abs_dz_zoomOmega_le {C h lam zc eps : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (hdelta : lam ^ (2 * h) ≤ 1) (heps : 0 < eps) {p : (ℝ × ℝ) × ℝ} (hR : eps ≤ p.1.1) (hp : zoomPoint lam h zc p ∈ unitCylinder) (htau : p.2 ≤ -1) : |dz (zoomOmega lam h zc u) p| ≤ 2 * C * (1 / eps) * (-p.2) ^ (-(1 / 2))

The vertical derivative of Ω_n on {R ≥ ε}, uniformly in the zoom scale, with the exponent -1/2 of eq:aniso:zoom:derivatives.

theorem CIV.abs_dr_zoomOmega_add_abs_dz_zoomOmega_le {C h lam zc eps : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) (hdelta : lam ^ (2 * h) ≤ 1) (heps : 0 < eps) {p : (ℝ × ℝ) × ℝ} (hR : eps ≤ p.1.1) (hp : zoomPoint lam h zc p ∈ unitCylinder) (htau : p.2 ≤ -1) : |dr (zoomOmega lam h zc u) p| + |dz (zoomOmega lam h zc u) p| ≤ 2 * C * (2 / eps + 1 / eps ^ 2) * (-p.2) ^ (-(1 / 2))

The first-derivative bound of Ω_n on {R ≥ ε}: the sum of the two spatial derivatives is bounded by 2C(2ε⁻¹ + ε⁻²)(-τ)^{-1/2}, uniformly in the zoom scale.

The Lipschitz bound on a rectangle

theorem CIV.abs_zoomOmega_sub_zoomOmega_le {C h lam zc eps Ra Rb Za Zb tau : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) (hdelta : lam ^ (2 * h) ≤ 1) (heps : 0 < eps) (hepsRa : eps ≤ Ra) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb, zoomPoint lam h zc (y, tau) ∈ unitCylinder) {y1 y2 : ℝ × ℝ} (hy1 : y1 ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb) (hy2 : y2 ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb) : |zoomOmega lam h zc u (y1, tau) - zoomOmega lam h zc u (y2, tau)| ≤ 2 * C * (2 / eps + 1 / eps ^ 2) * dist y1 y2

The two-point bound on a rectangle [Ra, Rb] × [Za, Zb] ⊆ {R ≥ ε} at a fixed rescaled time τ ≤ -1: joining the two points by the two coordinate edges through (y₂₁, y₁₂) and applying the mean value inequality on each edge.

theorem CIV.lipschitzOnWith_zoomOmega {C h lam zc eps Ra Rb Za Zb tau : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) (hdelta : lam ^ (2 * h) ≤ 1) (heps : 0 < eps) (hepsRa : eps ≤ Ra) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb, zoomPoint lam h zc (y, tau) ∈ unitCylinder) : LipschitzOnWith (2 * C * (2 / eps + 1 / eps ^ 2)).toNNReal (fun (y : ℝ × ℝ) => zoomOmega lam h zc u (y, tau)) (Set.Icc Ra Rb ×ˢ Set.Icc Za Zb)

The Lipschitz-in-space bound on a rectangle [Ra, Rb] × [Za, Zb] ⊆ {R ≥ ε}, at every rescaled time τ ≤ -1, with a constant independent of the zoom scale and of τ.