Compactness of the rescaled potential vorticities at the moving axis points

The compactness step eq:aniso:zoom:finite:compactness of Step 2 of the proof of prop:aniso:small, at the moving axis points (0, z_n) of eq:aniso:zoom:finite:variables.

Off the axis the rescaled potential vorticity is Ω_n = Θ_n / R, where Θ_n = λ_n² δ_n ω_θ is the rescaled azimuthal vorticity of eq:aniso:zoom:receding:vorticity taken about the axis point itself (no radial offset). On a compact subset of the open half-plane R is bounded below, so the time-pairing estimate of Θ_n, obtained from eq:aniso:zoom:receding:equation with A = 0 exactly as in the receding-axis case, holds with constants depending on that lower bound. The half-plane compactness theorem then gives locally uniform convergence of Θ_n on {R > 0, τ ≤ -1}, and dividing by R gives that of Ω_n.

theorem CIV.hpair_zoomTheta_axis_eventual {C h CΓ ρ Rstar tstar : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρR : ρ < Rstar) (hR1 : Rstar ≤ 1) (htstar : tstar < 0) {zc : ℕ → ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) (hCnn : 0 ≤ C) (hCΓnn : 0 ≤ CΓ) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haniso : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hΓ : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∀ t ∈ Set.Ioo tstar 0, |circulation u (x, t)| ≤ CΓ) (hforce : ForceC2Bounded f) (lam : ℕ → ℝ) (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (K : Set (ℝ × ℝ)) : IsCompact K → (∀ y ∈ K, 0 < y.1) → ∀ (J : Set ℝ), IsCompact J → (∀ τ ∈ J, τ ≤ -1) → ∃ (Cₒ : ℝ), 0 ≤ Cₒ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (ψ : ℝ × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ interior K → ∀ (B : ℝ), 0 ≤ B → (∀ (y : ℝ × ℝ), |ψ y| ≤ B ∧ ‖fderiv ℝ ψ y‖ ≤ B ∧ ‖fderiv ℝ (fderiv ℝ ψ) y‖ ≤ B) → ∀ τ ∈ J, ∀ τ' ∈ J, |∫ (y : ℝ × ℝ), (zoomTheta (lam n) h 0 (zc n) u (y, τ) - zoomTheta (lam n) h 0 (zc n) u (y, τ')) * ψ y| ≤ Cₒ * B * |τ - τ'|

The time-pairing estimate for the rescaled azimuthal vorticity about the moving axis points (0, zc n), on compact subsets of the open half-plane.

theorem CIV.zoomOmega_eq_zoomTheta_div (lam h zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) (hR : p.1.1 ≠ 0) : zoomOmega lam h zc u p = zoomTheta lam h 0 zc u p / p.1.1

Off the axis the rescaled potential vorticity is the rescaled azimuthal vorticity about the axis point divided by R.

theorem CIV.exists_subseq_tendstoUniformlyOn_zoomOmega_moving {C h CΓ ρ Rstar tstar : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρR : ρ < Rstar) (hR1 : Rstar ≤ 1) (htstar : tstar < 0) {zc : ℕ → ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) (hCnn : 0 ≤ C) (hCΓnn : 0 ≤ CΓ) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haniso : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hΓ : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∀ t ∈ Set.Ioo tstar 0, |circulation u (x, t)| ≤ CΓ) (hforce : ForceC2Bounded f) (lam : ℕ → ℝ) (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (Ω : (ℝ × ℝ) × ℝ → ℝ), ContinuousOn Ω {p : (ℝ × ℝ) × ℝ | 0 < p.1.1 ∧ p.2 ≤ -1} ∧ ∀ (K : Set ((ℝ × ℝ) × ℝ)), IsCompact K → K ⊆ {p : (ℝ × ℝ) × ℝ | 0 < p.1.1 ∧ p.2 ≤ -1} → TendstoUniformlyOn (fun (n : ℕ) => zoomOmega (lam (φ n)) h (zc (φ n)) u) Ω Filter.atTop K

eq:aniso:zoom:finite:compactness at the moving axis points: along a subsequence the rescaled potential vorticities converge uniformly on every compact subset of {R > 0, τ ≤ -1}, to a limit continuous there.