First-derivative identities and bound for the rescaled receding azimuthal vorticity

The derivative identities and first-derivative bound of the rescaled receding azimuthal vorticity Θ_n of eq:aniso:zoom:receding:vorticity, off eq:aniso:zoom:receding:equation's manuscript display — the ingredient of eq:aniso:zoom:receding:bound's derivative analogue needed before the Arzelà–Ascoli extraction of Step 3.

A C² mixed-partial symmetry fact for the two Cartesian spatial directions 0 and 2

The four pieces of zoomTheta, differentiated along a coordinate slice

The derivative identities and bound for the rescaled receding azimuthal vorticity

theorem CIV.dr_zoomTheta_eq (lam h rc 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 : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (zoomTheta lam h rc zc u) p = (lam ^ (2 * h)) ^ 2 * dr (dz (zoomVRec lam h rc zc u)) p - dr (dr (zoomWRec lam h rc zc u)) p

The radial derivative of the rescaled receding azimuthal vorticity Θ_n, differentiating eq:aniso:zoom:receding:vorticity's difference termwise.

theorem CIV.dz_zoomTheta_eq (lam h rc 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 : zoomPointRec lam h rc zc p ∈ unitCylinder) : dz (zoomTheta lam h rc zc u) p = (lam ^ (2 * h)) ^ 2 * dz (dz (zoomVRec lam h rc zc u)) p - dr (dz (zoomWRec lam h rc zc u)) p

The vertical derivative of the rescaled receding azimuthal vorticity Θ_n, differentiating eq:aniso:zoom:receding:vorticity's difference termwise.

The first-derivative bound

theorem CIV.abs_dr_zoomTheta_add_abs_dz_zoomTheta_le {C h lam rc zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) (hdelta : lam ^ (2 * h) ≤ 1) {p : (ℝ × ℝ) × ℝ} (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (htau : p.2 ≤ -1) : |dr (zoomTheta lam h rc zc u) p| + |dz (zoomTheta lam h rc zc u) p| ≤ 4 * C * (-p.2) ^ (-(1 / 2))

The sum of the radial and vertical derivatives of the rescaled receding azimuthal vorticity Θ_n is bounded uniformly in the zoom scale by 4C(-τ)^{-1/2}, the derivative analogue of eq:aniso:zoom:receding:bound.