Documentation

LeanPool.CIVAxisymmetric.Zoom.FiniteSelectionIdentity

The chain-rule bridge between the meridional-plane quantities ∂_r u_r, u_r/r, ∂_z u_z of eq:aniso:zoom:selected at a time t < 0 and the finite-axis rescaled fields V_n, W_n of eq:aniso:zoom:fields, evaluated at the corresponding rescaled point (R, 0, -1) with lam² = -t: the identity that lets Step 2's contradiction (paragraph after eq:aniso:zoom:finite:limit) read the selected sequence's scaled quantity off the zoom variables at τ = -1.

theorem CIV.neg_t_mul_meridionalQuantity_selection_eq {h : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {t : ℝ} (ht : t < 0) {lam R zc : ℝ} (hlam : 0 < lam) (hR : R ≠ 0) (hlamsq : lam ^ 2 = -t) (hp : zoomPoint lam h zc ((R, 0), -1) ∈ unitCylinder) :
-t * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (meridional (lam * R) zc, t)| + |radialQuotient u (meridional (lam * R) zc, t)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 (meridional (lam * R) zc, t)|) = |dr (zoomV lam h zc u) ((R, 0), -1)| + |zoomV lam h zc u ((R, 0), -1) / R| + |dz (zoomW lam h zc u) ((R, 0), -1)|