Passing the finite-axis zoom sequence to its limit

Elementary limit lemmas for eq:aniso:zoom:finite:limit, the equation obeyed by the locally uniform limit Ω_∞ of the rescaled potential vorticities Ω_n of eq:aniso:zoom:fields, along a sequence of zoom scales λ_n → 0⁺:

• λ_n → 0⁺ forces δ_n = λ_n^{2h} → 0 and, for any sequence uniformly bounded by M, δ_n² · (\text{that sequence}) → 0 — the mechanism removing δ_n² ∂_{ZZ} Ω_n from the equation (tendsto_zoomDeltaSq_nhdsWithin_zero, tendsto_zoomDeltaSq_mul_of_bounded).
• the force term G_n of eq:interior:force:scaled tends to zero uniformly in the point along every scale sequence (eventually_forall_abs_zoomForce_lt), transporting the scale limit tendsto_zoomForce_bound_nhdsWithin_zero of CIV.Zoom.FiniteLift along an arbitrary λ_n → 0⁺.
• the algebraic divergence identity div_{X,Z} B_n = 2 V_n / R of CIV.Zoom.FiniteAxisBounds (zoomDriftDivergence_eq) holds for every finite n, so it passes to the limit once V_n / R does (tendsto_zoomDriftDivergence_of_tendsto_zoomV_div): this is the "With div_{X,Z} B = 2 V / R" clause of eq:aniso:zoom:finite:limit.
• the products B_n Ω_n and (V_n/R) Ω_n pass to the limit under an integral against a fixed test function by dominated convergence, given almost-everywhere convergence of the pointwise product and a uniform domination (tendsto_integral_mul_of_ae_tendsto).

The limit equation itself, CIV.IsDistributionalDriftDiffusion 5 4 (Set.Iio (-1)) B divB Ω_∞ with an admissible drift, is CIV.exists_admissibleDrift_zoomOmegaLimit.

δ_n → 0 removes the δ_n² ∂_{ZZ} Ω_n term

theorem CIV.tendsto_zoomDelta_nhdsWithin_zero {h : ℝ} (hh : 0 < h) : Filter.Tendsto (fun (lam : ℝ) => lam ^ (2 * h)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

δ = λ^{2h} → 0 as the zoom scale λ → 0⁺, for any positive anisotropy exponent h.

theorem CIV.tendsto_zoomDeltaSq_nhdsWithin_zero {h : ℝ} (hh : 0 < h) : Filter.Tendsto (fun (lam : ℝ) => (lam ^ (2 * h)) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

δ² = (λ^{2h})² → 0 as λ → 0⁺.

theorem CIV.tendsto_zoomDeltaSq_mul_of_bounded {h M : ℝ} (hh : 0 < h) {D : ℝ → ℝ} (hD : ∀ (lam : ℝ), |D lam| ≤ M) : Filter.Tendsto (fun (lam : ℝ) => (lam ^ (2 * h)) ^ 2 * D lam) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

δ_n² · D_n → 0 whenever D_n is uniformly bounded and λ_n → 0⁺: the mechanism that removes δ_n² ∂_{ZZ} Ω_n from eq:aniso:zoom:finite:equation in the limit, given the uniform bound on ∂_{ZZ} Ω_n as an explicit hypothesis.

The force term G_n → 0 uniformly along a scale sequence

theorem CIV.eventually_forall_abs_zoomForce_lt (h : ℝ) (hh0 : 0 ≤ h) {lamSeq zcSeq : ℕ → ℝ} (hlam : Filter.Tendsto lamSeq Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (hMf : ForceC2Bounded f) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : (ℝ × ℝ) × ℝ), zoomPoint (lamSeq n) h (zcSeq n) p ∈ unitCylinder → |zoomForce (lamSeq n) h (zcSeq n) f p| < ε

The force term G_n = zoomForce of eq:interior:force:scaled tends to zero uniformly in the point along every scale sequence λ_n → 0⁺: composing the scale limit tendsto_zoomForce_bound_nhdsWithin_zero of CIV.Zoom.FiniteLift along λ_n with the uniform-in-the-point bound abs_zoomForce_le (reproved directly from abs_potentialVorticity_force_le so the same bounding constant is used at every n). This is the "G_n → 0 uniformly" clause of eq:aniso:zoom:finite:limit.

div_{X,Z} B = 2 V / R passes to the limit

theorem CIV.tendsto_zoomDriftDivergence_of_tendsto_zoomV_div (h : ℝ) {lamSeq zcSeq : ℕ → ℝ} (hlam : ∀ (n : ℕ), 0 < lamSeq n) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (fo : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pr fo unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {q : CKN.Vec 5 × ℝ} (hR : 0 < zoomLiftRadius q.1) (hp : ∀ (n : ℕ), zoomPoint (lamSeq n) h (zcSeq n) (zoomLiftPoint q) ∈ unitCylinder) {L : ℝ} (hL : Filter.Tendsto (fun (n : ℕ) => zoomV (lamSeq n) h (zcSeq n) u (zoomLiftPoint q) / zoomLiftRadius q.1) Filter.atTop (nhds L)) : Filter.Tendsto (fun (n : ℕ) => zoomDriftDivergence (lamSeq n) h (zcSeq n) u q) Filter.atTop (nhds (2 * L))

The exact algebraic identity zoomDriftDivergence_eq of CIV.Zoom.FiniteAxisBounds, div_{X,Z} B_n = 2 V_n / R, holds at every finite n, so it passes to the limit outright as soon as V_n / R converges: the "With div_{X,Z} B = 2 V / R" clause of eq:aniso:zoom:finite:limit, conditioned only on the convergence of V_n / R.

Passing a product of two convergent sequences to the limit under an integral

theorem CIV.tendsto_mul_mul_of_tendsto {Ω B : ℕ → CKN.Vec 5 × ℝ → ℝ} {Ωlim Blim φ : CKN.Vec 5 × ℝ → ℝ} {z : CKN.Vec 5 × ℝ} (hΩ : Filter.Tendsto (fun (n : ℕ) => Ω n z) Filter.atTop (nhds (Ωlim z))) (hB : Filter.Tendsto (fun (n : ℕ) => B n z) Filter.atTop (nhds (Blim z))) : Filter.Tendsto (fun (n : ℕ) => Ω n z * B n z * φ z) Filter.atTop (nhds (Ωlim z * Blim z * φ z))

The pointwise mechanism of "passing the products B_n Ω_n and (V_n/R) Ω_n to the limit": if two sequences converge at a point, so does their product against a fixed third factor.

theorem CIV.tendsto_integral_mul_of_ae_tendsto {Ω B : ℕ → CKN.Vec 5 × ℝ → ℝ} {Ωlim Blim φ : CKN.Vec 5 × ℝ → ℝ} (hmeas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Vec 5 × ℝ) => Ω n z * B n z * φ z) MeasureTheory.volume) {M : ℝ} (hφ : MeasureTheory.Integrable φ MeasureTheory.volume) (hbound : ∀ (n : ℕ), ∀ᵐ (z : CKN.Vec 5 × ℝ), |Ω n z * B n z * φ z| ≤ M * |φ z|) (hlim : ∀ᵐ (z : CKN.Vec 5 × ℝ), Filter.Tendsto (fun (n : ℕ) => Ω n z * B n z * φ z) Filter.atTop (nhds (Ωlim z * Blim z * φ z))) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec 5 × ℝ), Ω n z * B n z * φ z) Filter.atTop (nhds (∫ (z : CKN.Vec 5 × ℝ), Ωlim z * Blim z * φ z))

Passing the product Ω_n B_n to the limit inside a fixed integral against φ, by the Lebesgue dominated convergence theorem: given almost-everywhere convergence of the pointwise product and a uniform domination by M |φ|, the paired integrals converge. This is the integral-level mechanism of "the weak-* convergence of B_n against the strong convergence of Ω_n … passes the products B_n Ω_n and (V_n/R) Ω_n to the limit" of eq:aniso:zoom:finite:limit.