The lifted finite-axis drift is Lipschitz across the axis

For the lifted drift B_n = (V_n X/R, W_n) of eq:drift:Bn:def and its divergence 2 V_n / R (continued to the axis by 2 ∂_R V_n), at a fixed time τ ≤ -1 and on a ball of the lifted space mapped into the unit cylinder, both are bounded and Lipschitz with constants depending only on the constant of eq:aniso:bounds: the footnote to eq:drift:Bn:def, |B_n| + |∇B_n| ≤ C |τ|^{-1/2}, read as a Lipschitz bound across the axis. The direction X/R is singular at the axis, but |V_n| ≤ C R there, and R₂ |X/R₁ - Y/R₂| ≤ |R₁ - R₂| + |X - Y|.

theorem CIV.abs_zoomLiftRadius_sub_le (x y : CKN.Vec 5) : |zoomLiftRadius x - zoomLiftRadius y| ≤ 2 * ‖x - y‖

The lifted radius is 2-Lipschitz for the sup norm of Vec 5.

theorem CIV.zoomLiftRadius_le_two_mul_norm (x : CKN.Vec 5) : zoomLiftRadius x ≤ 2 * ‖x‖

theorem CIV.abs_mul_div_sub_div_le {C a R1 R2 x1 y1 : ℝ} (hC : 0 ≤ C) (hR1 : 0 ≤ R1) (hR2 : 0 ≤ R2) (ha : |a| ≤ C * R2) (hx1 : |x1| ≤ R1) (hy1 : |y1| ≤ R2) : |a * (x1 / R1 - y1 / R2)| ≤ C * (|R1 - R2| + |x1 - y1|)

The singular direction X/R against a factor vanishing linearly on the axis.

theorem CIV.zoomLiftPoint_fst_mem {r τ : ℝ} {x : CKN.Vec 5} (hx : x ∈ Metric.closedBall 0 r) : (zoomLiftPoint (x, τ)).1 ∈ Set.Icc 0 (2 * r) ×ˢ Set.Icc (-r) r

A point of the ball of radius r of the lifted space lifts into [0, 2r] × [-r, r].

theorem CIV.abs_zoomV_le_mul {C h lam zc tau : ℝ} (hlam : 0 < lam) {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) (haxi : IsAxisymmetricOn u unitCylinder) (hC : 0 ≤ C) (htau : tau ≤ -1) {y : ℝ × ℝ} (hy0 : 0 ≤ y.1) (hp : zoomPoint lam h zc (y, tau) ∈ unitCylinder) : |zoomV lam h zc u (y, tau)| ≤ C * y.1

|V_n| ≤ C R on a rectangle through the axis mapped into the cylinder, at τ ≤ -1.

theorem CIV.norm_zoomDrift_sub_le {C h lam zc r tau : ℝ} (hlam : 0 < lam) {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) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc 0 (2 * r) ×ˢ Set.Icc (-r) r, zoomPoint lam h zc (y, tau) ∈ unitCylinder) {x y : CKN.Vec 5} (hx : x ∈ Metric.closedBall 0 r) (hy : y ∈ Metric.closedBall 0 r) : ‖zoomDrift lam h zc u (x, tau) - zoomDrift lam h zc u (y, tau)‖ ≤ 7 * C * ‖x - y‖

The lifted drift is Lipschitz with constant 7C on a ball of the lifted space mapped into the cylinder at a time τ ≤ -1.

theorem CIV.finDriftDiv_eq_two_mul_zoomVQuot (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Vec 5 × ℝ) : finDriftDiv lam h zc u z = 2 * zoomVQuot lam h zc u (zoomLiftPoint z)

The lifted divergence is 2 times the continued quotient V_n / R.

theorem CIV.abs_finDriftDiv_sub_le {C h lam zc r tau : ℝ} (hlam : 0 < lam) {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) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc 0 (2 * r) ×ˢ Set.Icc (-r) r, zoomPoint lam h zc (y, tau) ∈ unitCylinder) {x y : CKN.Vec 5} (hx : x ∈ Metric.closedBall 0 r) (hy : y ∈ Metric.closedBall 0 r) : |finDriftDiv lam h zc u (x, tau) - finDriftDiv lam h zc u (y, tau)| ≤ 12 * C * ‖x - y‖

The lifted divergence is Lipschitz with constant 12C on a ball mapped into the cylinder.

theorem CIV.zoomDrift_finDriftDiv_bound {C h lam zc tau : ℝ} (hlam : 0 < lam) {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) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (htau : tau ≤ -1) {x : CKN.Vec 5} (hp : zoomPoint lam h zc (zoomLiftPoint (x, tau)) ∈ unitCylinder) : ‖zoomDrift lam h zc u (x, tau)‖ ≤ C ∧ |finDriftDiv lam h zc u (x, tau)| ≤ 2 * C

The pointwise bounds ‖B_n‖ ≤ C and |div B_n| ≤ 2C on the lifted preimage at τ ≤ -1.