Lipschitz-in-space bound for the rescaled vertical field W_n

On a rectangle contained in {R ≥ 0} the rescaled vertical field W_n of eq:aniso:zoom:receding:variables has first spatial derivatives bounded uniformly in the zoom scale and in the rescaled time τ ≤ -1. The proof drops the nonnegative S_n summand from the combined anisotropic bounds (abs_dr_zoomWRec_add_abs_dr_zoomSRec_le, abs_dz_zoomWRec_add_abs_dz_zoomSRec_le) to obtain τ-uniform pointwise bounds |∂_R W_n| ≤ C and |∂_Z W_n| ≤ C, then integrates along the two coordinate edges of a rectangle via Convex.norm_image_sub_le_of_norm_hasDerivWithin_le. This is the input to the Arzelà–Ascoli extraction of Step 3.

The τ-uniform derivative bounds

The two-point bound on a rectangle

theorem CIV.abs_zoomWRec_sub_zoomWRec_le {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) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb, zoomPointRec lam h rc zc (y, tau) ∈ unitCylinder) {y1 y2 : ℝ × ℝ} (hy1 : y1 ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb) (hy2 : y2 ∈ Set.Icc Ra Rb ×ˢ Set.Icc Za Zb) : |zoomWRec lam h rc zc u (y1, tau) - zoomWRec lam h rc zc u (y2, tau)| ≤ 2 * C * dist y1 y2

The two-point bound on a rectangle [Ra, Rb] × [Za, Zb] at a fixed rescaled time τ ≤ -1: joining the two points by the two coordinate edges through (y₂₁, y₁₂) and applying the mean value inequality on each edge.

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

The Lipschitz-in-space bound for the rescaled vertical field W_n on a rectangle, at every rescaled time τ ≤ -1, with a constant independent of the zoom scale and of τ.