Uniform finite-axis rescaled field bounds on compact time intervals

The hbdd hypothesis shape (uniform boundedness on rectangles of bounded time) for the finite-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 that an eventual Arzelà–Ascoli extraction of (V_n, W_n) in C¹_loc (eq:aniso:zoom:finite:compactness) needs alongside the equicontinuity modulus.

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

For every compact set J ⊆ (-∞, -1] and every C ≥ 0, the rescaled radial field zoomV is uniformly bounded on {zoomPoint … ∈ unitCylinder} × J by a constant M depending only on C, J, and the exponent -(1/2).

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

For every compact set J ⊆ (-∞, -1] and every C ≥ 0, the sum |zoomW| + |zoomS| is uniformly bounded on {zoomPoint … ∈ unitCylinder} × J by a constant M depending only on C, J, h, and the exponent -(1/2) - h.

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

Combined uniform bound for |zoomV| + |zoomW| + |zoomS| on {zoomPoint … ∈ unitCylinder} × J. Follows from the two separate bounds above via additivity.