Uniform bounds of the rescaled potential vorticity at the moving axis points

Two of the three inputs of the compactness argument eq:aniso:zoom:finite:compactness in Step 2 of the proof of prop:aniso:small, at the moving axis points (0, z_n) of eq:aniso:zoom:finite:variables: on every compact subset K of the open half-plane and every compact set of times J ⊆ (-∞, -1], the rescaled potential vorticities Ω_n are eventually bounded by 2C (eq:aniso:zoom:finite:bound) and eventually Lipschitz in space with a constant independent of n (the first-derivative bounds obtained from eq:aniso:zoom:finite:identities and eq:aniso:zoom:derivatives).

theorem CIV.eventually_forall_zoomPoint_mem_unitCylinder_moving {h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) {zc : ℕ → ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) {lam : ℕ → ℝ} (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (K : Set ((ℝ × ℝ) × ℝ)) (hK : IsCompact K) (hKt : ∀ p ∈ K, p.2 < 0) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ p ∈ K, zoomPoint (lam n) h (zc n) p ∈ unitCylinder

A compact set of zoomed points with τ < 0 is eventually mapped into the unit cylinder by the finite-axis zoom about the moving axis points (0, zc n), |zc n| ≤ ρ < 1.

theorem CIV.eventually_lam_lt_one_and_zoomDelta_le_one {h : ℝ} (hh0 : 0 ≤ h) {lam : ℕ → ℝ} (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < lam n ∧ lam n < 1 ∧ lam n ^ (2 * h) ≤ 1

Eventually λ_n < 1, hence δ_n = λ_n^{2h} ≤ 1.

theorem CIV.zoomOmega_eventually_bdd {C h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hC : 0 ≤ C) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {zc : ℕ → ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) {lam : ℕ → ℝ} (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (K : Set (ℝ × ℝ)) (hK : IsCompact K) (J : Set ℝ) (hJ : IsCompact J) (hJt : ∀ τ ∈ J, τ ≤ -1) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ y ∈ K, ∀ τ ∈ J, |zoomOmega (lam n) h (zc n) u (y, τ)| ≤ 2 * C

hbdd for Ω_n at the moving axis points: eventually bounded by 2C on K × J, K compact in the open half-plane, J ⊆ (-∞, -1] compact.

theorem CIV.zoomOmega_eventually_lipschitzOnWith {C h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hC : 0 ≤ C) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {zc : ℕ → ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) {lam : ℕ → ℝ} (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (K : Set (ℝ × ℝ)) (hK : IsCompact K) (hKp : ∀ y ∈ K, 0 < y.1) (J : Set ℝ) (hJ : IsCompact J) (hJt : ∀ τ ∈ J, τ ≤ -1) : ∃ (L : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, LipschitzOnWith L.toNNReal (fun (y : ℝ × ℝ) => zoomOmega (lam n) h (zc n) u (y, τ)) K

hlip for Ω_n at the moving axis points: on a compact K in the open half-plane and a compact J ⊆ (-∞, -1], eventually Ω_n(·, τ) is Lipschitz on K with one constant.