Receding-axis curvature terms vanish in the limit

As the recentring offset A = rc / lam → ∞, the two correction terms − Vₙ/(Aₙ+R)·Θₙ and − Θₙ/(Aₙ+R)² of zoomTheta_pde tend to zero at a fixed point ((R, Z), τ).

The two play different roles in eq:aniso:zoom:receding:equation. Only − Θₙ/(Aₙ+R)² is one of the three terms the manuscript drops on passing to the limit; the other two dropped terms are ∂_R Θₙ/(Aₙ+R) and ∂_Z(Sₙ²)/(Aₙ+R). The stretching term − Vₙ Θₙ/(Aₙ+R) is not dropped: zoomTheta_transport_divergenceForm absorbs it into the perfect divergence ∂_R(Vₙ Θₙ) + ∂_Z(Wₙ Θₙ) that the limiting equation retains. The limit proved for it here is an auxiliary estimate on the transport part, not the removal of an axis term.

The limits are taken along the germ 𝓝[>] 0 of the zoom scale, and every hypothesis about the zoom point is an eventual one: at a fixed ((R, Z), τ) the recentred zoom point lies in the unit cylinder only for small scales, never for all of them (lam = 1 forces τ < 0 while lam = √(1/(-τ)) forces lam² τ = -1, so the all-scales form is satisfied by no real τ). eventually_zoomPointRec_mem_unitCylinder_at produces the eventual form from the standing hypotheses of prop:aniso:small.

Producing the eventual hypotheses

theorem CIV.eventually_zoomPointRec_mem_unitCylinder_at {h rc zc : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hm : rc ^ 2 + zc ^ 2 < 1) (p : (ℝ × ℝ) × ℝ) (hp : p.2 < 0) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), zoomPointRec lam h rc zc p ∈ unitCylinder

The one-point form of eventually_zoomPointRec_mem_unitCylinder: at a fixed negative-time point p, and for a recentring (rc, zc) strictly inside the unit disc of the meridional plane, the recentred zoom point lies in the unit cylinder for all sufficiently small scales. This is the witness that makes the eventual membership hypotheses of this file and of CIV.Zoom.RecedingDrTermVanish satisfiable.

theorem CIV.eventually_abs_zoomVRec_le {C h rc zc : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hm : rc ^ 2 + zc ^ 2 < 1) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (p : (ℝ × ℝ) × ℝ) (hp : p.2 < 0) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), |zoomVRec lam h rc zc u p| ≤ C * (-p.2) ^ (-(1 / 2))

The (0, 0) entry of eq:aniso:zoom:derivatives in eventual form: the recentred radial velocity is bounded by the scale-independent constant C (-τ)^{-1/2} for all sufficiently small scales. This produces the hV hypothesis of tendsto_zoomTheta_pde_curvature_terms_nhdsWithin_zero.

theorem CIV.eventually_abs_zoomTheta_le {C h rc zc : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hC : 0 ≤ C) (hm : rc ^ 2 + zc ^ 2 < 1) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : p.2 < 0) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), |zoomTheta lam h rc zc u p| ≤ C * ((-p.2) ^ (-1 + h) + (-p.2) ^ (-1 - h))

eq:aniso:zoom:receding:bound in eventual form: since δ = lam ^ (2 * h) ≤ 1 for small scales, the two terms of abs_zoomTheta_le collapse to the scale-independent constant C ((-τ)^{-1+h} + (-τ)^{-1-h}). This produces the hTheta hypothesis of tendsto_zoomTheta_pde_curvature_terms_nhdsWithin_zero.

The two offset decay lemmas

theorem CIV.tendsto_offset_sq_term_nhdsWithin_zero {rc M : ℝ} (hrc : 0 < rc) {R : ℝ} (hR : 0 ≤ R) (D : ℝ → ℝ) (hD : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), |D lam| ≤ M) : Filter.Tendsto (fun (lam : ℝ) => D lam / (rc / lam + R) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

eq:aniso:zoom:receding:limit: a numerator bounded for small scales, divided by (A + R)² with A = rc / lam → ∞, tends to 0 as lam → 0⁺.

theorem CIV.tendsto_offset_term_nhdsWithin_zero {rc M : ℝ} (hrc : 0 < rc) {R : ℝ} (hR : 0 ≤ R) (D : ℝ → ℝ) (hD : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), |D lam| ≤ M) : Filter.Tendsto (fun (lam : ℝ) => D lam / (rc / lam + R)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

eq:aniso:zoom:receding:limit: the same with the offset to the first power, the form consumed by the ∂_R Θₙ/(Aₙ+R) limit of CIV.Zoom.RecedingDrTermVanish and by the divergence limit of the receding drift.

The two curvature terms

theorem CIV.tendsto_zoomTheta_pde_curvature_terms_nhdsWithin_zero {rc h zc : ℝ} (hrc : 0 < rc) {R Z tau : ℝ} (hR : 0 ≤ R) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) {MV MTheta : ℝ} (hV : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), |zoomVRec lam h rc zc u ((R, Z), tau)| ≤ MV) (hTheta : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), |zoomTheta lam h rc zc u ((R, Z), tau)| ≤ MTheta) : Filter.Tendsto (fun (lam : ℝ) => zoomVRec lam h rc zc u ((R, Z), tau) / (rc / lam + R) * zoomTheta lam h rc zc u ((R, Z), tau) + zoomTheta lam h rc zc u ((R, Z), tau) / (rc / lam + R) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

eq:aniso:zoom:receding:limit (the curvature pair): the two terms − Vₙ/(Aₙ+R)·Θₙ − Θₙ/(Aₙ+R)² of zoomTheta_pde vanish as lam → 0⁺. The bounds on Vₙ and Θₙ are required only for small scales, which is what eventually_abs_zoomVRec_le and eventually_abs_zoomTheta_le supply.