Lipschitz-in-space bound for the finite-axis rescaled vertical field #
The input to the Arzelà–Ascoli extraction of the finite-axis rescaled variables,
companion to CIV.Zoom.VLipschitz's radial bound: on a rectangle [Ra, Rb] × [Za, Zb]
contained in the unit cylinder (via hmem), the finite-axis rescaled vertical field
W_n is Lipschitz in the spatial variables, with a τ-independent constant 2C.
The proof follows the same two-edge mean-value-inequality route as
CIV.Zoom.VRecLipschitz: on each coordinate edge of the rectangle, the
per-point derivative bounds from abs_dr_zoomW_le_rpow_neg_half and
abs_dz_zoomW_le_rpow_neg_half give a τ-uniform bound; the two edges are
combined by the triangle inequality.
theorem
CIV.lipschitzOnWith_zoomW
{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)
(hh0 : 0 ≤ h)
(htau : tau ≤ -1)
(hmem : ∀ y ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb, zoomPoint lam h zc (y, tau) ∈ unitCylinder)
: