Lipschitz-in-space bound for the receding-axis rescaled radial field #
The input to the Arzelà–Ascoli extraction of Step 3: on a rectangle [Ra, Rb] × [Za, Zb]
contained in the unit cylinder (via hmem), the receding-axis rescaled radial field
V_n of eq:aniso:zoom:receding:variables is Lipschitz in the spatial variables, with a
τ-independent constant 2C.
The proof follows CIV.Zoom.OmegaLipschitz's abs_zoomOmega_sub_zoomOmega_le /
lipschitzOnWith_zoomOmega: on each coordinate edge of the rectangle, the
mean-value inequality (Convex.norm_image_sub_le_of_norm_hasDerivWithin_le) applied to the
per-point derivative bounds from abs_dr_zoomVRec_le and abs_dz_zoomVRec_le gives a
τ-uniform bound; the two edges are combined by the triangle inequality.
theorem
CIV.lipschitzOnWith_zoomVRec
{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)
(hh1 : h ≤ 1 / 2)
(htau : tau ≤ -1)
(hmem : ∀ y ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb, zoomPointRec lam h rc zc (y, tau) ∈ unitCylinder)
: