The endpoint vanishing of the rescaled vorticities along the zoom sequence

The endpoint vanishing in Steps 2 and 3 of the proof of prop:aniso:small: once the rescaled scalar (the potential vorticity Ω_n in the finite-axis case, the azimuthal vorticity Θ_n in the receding-axis case) converges locally uniformly up to τ = -1, and its limit solves the limit equation (eq:aniso:zoom:finite:limit, respectively eq:aniso:zoom:receding:limit:a) with an admissible drift, the limit inherits the decay bound of eq:aniso:zoom:finite:bound (respectively eq:aniso:zoom:receding:bound) because δ_n → 0, the comparison principle lem:aniso:comparison makes it vanish, and hence the rescaled scalars tend to zero at every point of {τ = -1} (off the axis in the finite-axis case). The zoom centres move with n, as in eq:aniso:zoom:finite:variables and eq:aniso:zoom:receding:variables.

theorem CIV.eventually_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))) (p : (ℝ × ℝ) × ℝ) (hp : p.2 < 0) : ∀ᶠ (n : ℕ) in Filter.atTop, zoomPoint (lam n) h (zc n) p ∈ unitCylinder

A fixed point of the zoomed variables 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.tendsto_zoomDeltaSq_seq {h : ℝ} (hh : 0 < h) {lam : ℕ → ℝ} (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) : Filter.Tendsto (fun (n : ℕ) => (lam n ^ (2 * h)) ^ 2) Filter.atTop (nhds 0)

δ_n² = (λ_n^{2h})² → 0 along a zoom sequence λ_n → 0⁺.

theorem CIV.abs_le_of_tendsto_zoomOmega {C h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) {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_pos : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) {p : (ℝ × ℝ) × ℝ} (hp : p.2 < 0) {L : ℝ} (hL : Filter.Tendsto (fun (n : ℕ) => zoomOmega (lam n) h (zc n) u p) Filter.atTop (nhds L)) : |L| ≤ C * (-p.2) ^ (-(3 / 2) - h)

The decay bound of the finite-axis limit, inherited from eq:aniso:zoom:finite:bound since δ_n → 0: at a point with τ < 0, a limit of Ω_n along the zoom sequence is bounded by C |τ|^{-3/2-h}.

theorem CIV.abs_le_of_tendsto_zoomTheta {C h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) {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) {rc zc : ℕ → ℝ} (hcz : ∀ (n : ℕ), rc n ^ 2 + zc n ^ 2 ≤ ρ ^ 2) {lam : ℕ → ℝ} (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) {p : (ℝ × ℝ) × ℝ} (hp : p.2 < 0) {L : ℝ} (hL : Filter.Tendsto (fun (n : ℕ) => zoomTheta (lam n) h (rc n) (zc n) u p) Filter.atTop (nhds L)) : |L| ≤ C * (-p.2) ^ (-1 - h)

The decay bound of the receding-axis limit, inherited from eq:aniso:zoom:receding:bound since δ_n → 0.

theorem CIV.tendsto_zoomOmega_endpoint_of_limit {C h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) {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_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 × ℝ → ℝ) (hB : IsAdmissibleDrift 5 (Set.Iio (-1)) B divB) (heq : IsDistributionalDriftDiffusion 5 4 (Set.Iio (-1)) B divB fun (z : CKN.Vec 5 × ℝ) => Ω (zoomLiftPoint z)) (q : ℝ × ℝ) : 0 < q.1 → Filter.Tendsto (fun (n : ℕ) => zoomOmega (lam n) h (zc n) u (q, -1)) Filter.atTop (nhds 0)

The finite-axis endpoint vanishing along the zoom sequence: if the rescaled potential vorticities at the moving axis points converge locally uniformly on {R > 0, τ ≤ -1} to a limit Ω whose lift solves eq:aniso:zoom:finite:limit with an admissible drift, then Ω_n(·, -1) tends to zero at every point off the axis.

theorem CIV.tendsto_zoomTheta_endpoint_of_limit {C h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) {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) {rc zc : ℕ → ℝ} (hcz : ∀ (n : ℕ), rc n ^ 2 + zc n ^ 2 ≤ ρ ^ 2) {lam : ℕ → ℝ} (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (Θ : (ℝ × ℝ) × ℝ → ℝ) (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 × ℝ → ℝ) (hB : IsAdmissibleDrift 2 (Set.Iio (-1)) B divB) (heq : IsDistributionalDriftDiffusion 2 1 (Set.Iio (-1)) B divB fun (z : CKN.Vec 2 × ℝ) => Θ (planeLiftPoint z)) (q : ℝ × ℝ) : Filter.Tendsto (fun (n : ℕ) => zoomTheta (lam n) h (rc n) (zc n) u (q, -1)) Filter.atTop (nhds 0)

The receding-axis endpoint vanishing along the zoom sequence: if the rescaled azimuthal vorticities at the moving centres converge locally uniformly on ℝ² × (-∞, -1] to a limit Θ solving eq:aniso:zoom:receding:limit:a with an admissible drift, then Θ_n(·, -1) tends to zero at every point.

theorem CIV.isLocallyBoundedOn_zoomOmegaLimit {C h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) {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_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) : IsLocallyBoundedOn 5 (Set.Iio (-1)) fun (z : CKN.Vec 5 × ℝ) => Ω (zoomLiftPoint z)

F2-Q: the lifted limit of the rescaled potential vorticities is locally bounded on ℝ⁵ × (-∞, -1), with the decay of eq:aniso:zoom:finite:bound inherited from δ_n → 0.

theorem CIV.tendsto_setLIntegral_enorm_sub_of_tendstoUniformlyOn {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {K : Set X} (hKm : MeasurableSet K) (hKf : μ K ≠ ⊤) {F : ℕ → X → ℝ} {g : X → ℝ} (hF : TendstoUniformlyOn F g Filter.atTop K) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : X) in K, ‖F n x - g x‖ₑ ∂μ) Filter.atTop (nhds 0)

Uniform convergence on a set of finite measure gives convergence of the integral of the distance, in ℝ≥0∞.

theorem CIV.tendsto_lintegral_of_tendstoUniformlyOn {m : ℕ} {T : ℝ} (qn : ℕ → CKN.Vec m × ℝ → ℝ) (q : CKN.Vec m × ℝ → ℝ) (hconv : ∀ (K : Set (CKN.Vec m × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic T → TendstoUniformlyOn qn q Filter.atTop K) (K : Set (CKN.Vec m × ℝ)) : IsCompact K → K ⊆ Set.univ ×ˢ Set.Iio T → Filter.Tendsto (fun (n : ℕ) => ∫⁻ (z : CKN.Vec m × ℝ) in K, ‖qn n z - q z‖ₑ) Filter.atTop (nhds 0)

R2-L1: locally uniform convergence on Vec m × (-∞, T] gives L¹ convergence on every compact subset of Vec m × (-∞, T).