Boundedness of the receding-axis zoom fields on compact time rectangles

For the receding-axis rescaled radial and vertical fields V_n, W_n (and the swirl source S_n) of eq:aniso:zoom:fields, the companion boundedness input — distinct from the first-derivative/Lipschitz bound — that an eventual Arzelà–Ascoli extraction of (V_n, W_n) in C¹_loc needs alongside the equicontinuity modulus.

theorem CIV.exists_forall_abs_zoomVRec_le_of_isCompact {C h : ℝ} (hC : 0 ≤ C) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (rc zc : ℝ) {J : Set ℝ} (hJ : IsCompact J) (hJsub : ∀ τ ∈ J, τ ≤ -1) : ∃ (M : ℝ), ∀ (lam : ℝ), 0 < lam → ∀ (p : (ℝ × ℝ) × ℝ), zoomPointRec lam h rc zc p ∈ unitCylinder → p.2 ∈ J → |zoomVRec lam h rc zc u p| ≤ M

theorem CIV.exists_forall_abs_zoomWRec_add_abs_zoomSRec_le_of_isCompact {C h : ℝ} (hC : 0 ≤ C) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (rc zc : ℝ) {J : Set ℝ} (hJ : IsCompact J) (hJsub : ∀ τ ∈ J, τ ≤ -1) : ∃ (M : ℝ), ∀ (lam : ℝ), 0 < lam → ∀ (p : (ℝ × ℝ) × ℝ), zoomPointRec lam h rc zc p ∈ unitCylinder → p.2 ∈ J → |zoomWRec lam h rc zc u p| + |zoomSRec lam h rc zc u p| ≤ M

theorem CIV.exists_forall_abs_zoomVRec_add_abs_zoomWRec_add_abs_zoomSRec_le_of_isCompact {C h : ℝ} (hC : 0 ≤ C) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (rc zc : ℝ) {J : Set ℝ} (hJ : IsCompact J) (hJsub : ∀ τ ∈ J, τ ≤ -1) : ∃ (M : ℝ), ∀ (lam : ℝ), 0 < lam → ∀ (p : (ℝ × ℝ) × ℝ), zoomPointRec lam h rc zc p ∈ unitCylinder → p.2 ∈ J → |zoomVRec lam h rc zc u p| + |zoomWRec lam h rc zc u p| + |zoomSRec lam h rc zc u p| ≤ M