Lipschitz-in-space bound for the finite-axis rescaled radial field #
An input to the Arzelà–Ascoli extraction in Step 2 of the proof of prop:aniso:small
(eq:aniso:zoom:finite:compactness): on a rectangle
[Ra, Rb] × [Za, Zb] contained in the unit cylinder (via hmem), the finite-axis rescaled
radial field V_n of eq:aniso:zoom:finite:variables is Lipschitz in the spatial variables, with
a τ-independent constant 2C.
The proof follows CIV.Zoom.VRecLipschitz's two-edge mean-value-inequality route: on each
coordinate edge of the rectangle, Convex.norm_image_sub_le_of_norm_hasDerivWithin_le applied to
the per-point derivative bounds from abs_dr_zoomV_le_rpow_neg_half and
abs_dz_zoomV_le_rpow_neg_half gives a τ-uniform bound; the two edges are combined by the
triangle inequality.
theorem
CIV.lipschitzOnWith_zoomV
{C h lam 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, zoomPoint lam h zc (y, tau) ∈ unitCylinder)
: