The two limit equations of the proof of prop:aniso:small

The locally uniform limits of the rescaled vorticities solve, in the sense of distributions and with an admissible drift, the limit equations of Steps 2 and 3: eq:aniso:zoom:finite:limit on ℝ⁴ × ℝ × (-∞, -1) (the lifted potential vorticity, (m, d) = (5, 4)) and eq:aniso:zoom:receding:limit:a on ℝ² × (-∞, -1) (the azimuthal vorticity, (m, d) = (2, 1)). The drift is extracted from the rescaled drifts and the finite-n equations are passed to the limit.

theorem CIV.tendstoUniformlyOn_planeLift {Θn : ℕ → (ℝ × ℝ) × ℝ → ℝ} {Θ : (ℝ × ℝ) × ℝ → ℝ} (hconv : ∀ (K : Set ((ℝ × ℝ) × ℝ)), IsCompact K → K ⊆ {p : (ℝ × ℝ) × ℝ | p.2 ≤ -1} → TendstoUniformlyOn Θn Θ Filter.atTop K) (K : Set (CKN.Vec 2 × ℝ)) : IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic (-1) → TendstoUniformlyOn (fun (n : ℕ) (z : CKN.Vec 2 × ℝ) => Θn n (planeLiftPoint z)) (fun (z : CKN.Vec 2 × ℝ) => Θ (planeLiftPoint z)) Filter.atTop K

Locally uniform convergence on (ℝ × ℝ) × (-∞, -1] pulled back to Vec 2 × ℝ.

theorem CIV.exists_admissibleDrift_zoomThetaLimit {C h CΓ ρ Rstar tstar : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {lam rc zc : ℕ → ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρR : ρ < Rstar) (hR1 : Rstar ≤ 1) (htstar : tstar < 0) (hcz : ∀ (n : ℕ), rc n ^ 2 + zc n ^ 2 ≤ ρ ^ 2) (hC : 0 ≤ C) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (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) (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (hA : Filter.Tendsto (fun (n : ℕ) => rc n / lam n) Filter.atTop Filter.atTop) (Θ : (ℝ × ℝ) × ℝ → ℝ) (hΘc : ContinuousOn Θ {p : (ℝ × ℝ) × ℝ | p.2 ≤ -1}) (hconv : ∀ (K : Set ((ℝ × ℝ) × ℝ)), IsCompact K → K ⊆ {p : (ℝ × ℝ) × ℝ | p.2 ≤ -1} → TendstoUniformlyOn (fun (n : ℕ) => zoomTheta (lam n) h (rc n) (zc n) u) Θ Filter.atTop K) : ∃ (B : CKN.Vec 2 × ℝ → CKN.Vec 2) (divB : CKN.Vec 2 × ℝ → ℝ), IsAdmissibleDrift 2 (Set.Iio (-1)) B divB ∧ IsDistributionalDriftDiffusion 2 1 (Set.Iio (-1)) B divB fun (z : CKN.Vec 2 × ℝ) => Θ (planeLiftPoint z)

eq:aniso:zoom:receding:limit:a: the locally uniform limit of the rescaled azimuthal vorticities at the moving centres solves the limit equation on ℝ² × (-∞, -1) in the sense of distributions, with an admissible drift.

theorem CIV.exists_admissibleDrift_zoomOmegaLimit {C h CΓ ρ Rstar tstar : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {lam zc : ℕ → ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρR : ρ < Rstar) (hR1 : Rstar ≤ 1) (htstar : tstar < 0) (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) (hC : 0 ≤ C) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (hΓ : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∀ t ∈ Set.Ioo tstar 0, |circulation u (x, t)| ≤ CΓ) (hforce : ForceC2Bounded f) (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (Ω : (ℝ × ℝ) × ℝ → ℝ) (hΩc : ContinuousOn Ω {p : (ℝ × ℝ) × ℝ | 0 < p.1.1 ∧ p.2 ≤ -1}) (hconv : ∀ (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) : ∃ (B : CKN.Vec 5 × ℝ → CKN.Vec 5) (divB : CKN.Vec 5 × ℝ → ℝ), IsAdmissibleDrift 5 (Set.Iio (-1)) B divB ∧ IsDistributionalDriftDiffusion 5 4 (Set.Iio (-1)) B divB fun (z : CKN.Vec 5 × ℝ) => Ω (zoomLiftPoint z)

eq:aniso:zoom:finite:limit: the locally uniform limit of the rescaled potential vorticities at the moving axis points, lifted to ℝ⁴ × ℝ, solves the limit equation on ℝ⁵ × (-∞, -1) in the sense of distributions, with an admissible drift.