Lipschitz-in-space bound for the receding-axis rescaled azimuthal vorticity

The Lipschitz-in-space bound for the receding-axis rescaled azimuthal vorticity Θ_n of eq:aniso:zoom:receding:vorticity, the derivative-bound analogue of eq:aniso:zoom:receding:bound, the input the receding-axis Arzelà–Ascoli extraction of Step 3 needs alongside its finite-axis counterparts CIV.Zoom.VRecLipschitz / CIV.Zoom.WRecLipschitz.

Private helper: mixed-partial symmetry for spatial partials 0 and 2

Private helper: vertical derivative of spatialPartial (u· i) 0 along zoomPointRec

Radial and vertical derivative facts for zoomTheta

theorem CIV.hasDerivAt_dr_zoomTheta (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) : HasDerivAt (fun (r : ℝ) => zoomTheta lam h rc zc u ((r, p.1.2), p.2)) (dr (zoomTheta lam h rc zc u) p) p.1.1

theorem CIV.hasDerivAt_dz_zoomTheta (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) : HasDerivAt (fun (s : ℝ) => zoomTheta lam h rc zc u ((p.1.1, s), p.2)) (dz (zoomTheta lam h rc zc u) p) p.1.2

Pointwise derivative bounds

theorem CIV.abs_dr_zoomTheta_le_const {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| ≤ 4 * C

theorem CIV.abs_dz_zoomTheta_le_const {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) : |dz (zoomTheta lam h rc zc u) p| ≤ 4 * C

Lipschitz-in-space bound

theorem CIV.lipschitzOnWith_zoomTheta {C h lam rc zc Ra Rb Za Zb tau : ℝ} (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) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb, zoomPointRec lam h rc zc (y, tau) ∈ unitCylinder) : LipschitzOnWith (8 * C).toNNReal (fun (y : ℝ × ℝ) => zoomTheta lam h rc zc u (y, tau)) (Set.Icc Ra Rb ×ˢ Set.Icc Za Zb)