The finite-axis bounds of the zoom-in variables

Step 1 of the finite-h zoom-in argument. Two families of bounds are proved here.

• The potential vorticity of the rescaled fields obeys eq:aniso:zoom:finite:bound: away from the axis Ω_n = (δ² ∂_z V_n - ∂_r W_n)/R, and both quotients are controlled by the second derivatives along the radial segment from the axis, because ∂_z u_r and ∂_r u_z vanish there. On the axis the same bound holds for the continuous extension, which is δ² ∂_r ∂_z V_n - ∂_r ∂_r W_n there. Uniformly in the rescaled time τ ≤ -1 this gives |Ω_n| ≤ 2C.
• The six drift bounds of eq:aniso:zoom:derivatives that the Step 2 comparison argument consumes: V_n, W_n and their first derivatives are all bounded by C (-τ)^{-1/2} once τ ≤ -1, since each of their anisotropic exponents is at most -1/2.

The same segment argument bounds the quotient V_n/R by the supremum of ∂_R V_n, because V_n vanishes on the axis, and with these bounds the lifted drift eq:drift:Bn:def of Step 2, B_n = (V_n X/R, W_n) on ℝ⁴ × ℝ, is bounded by C (-τ)^{-1/2} as well. Its divergence in the five lifted coordinates is computed here too: the trace of ∇_X(V_n X/R) is ∂_R V_n + 3 V_n/R, and the divergence identity of eq:aniso:zoom:finite:identities turns the sum into 2 V_n/R.

An elementary bound for a scaled difference

Differentiability of the two numerators along the radial segment

The two numerators vanish on the axis

The two quotients that build the rescaled potential vorticity

theorem CIV.abs_dz_zoomV_div_le {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hR : p.1.1 ≠ 0) : |dz (zoomV lam h zc u) p / p.1.1| ≤ C * (-p.2) ^ (-(3 / 2) + h)

|∂_z V_n / R| ≤ C (-τ)^{-3/2 + h}, from the segment representation of the quotient and the bound on ∂_r ∂_z V_n of eq:aniso:zoom:derivatives.

theorem CIV.abs_dr_zoomW_div_le {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hR : p.1.1 ≠ 0) : |dr (zoomW lam h zc u) p / p.1.1| ≤ C * (-p.2) ^ (-(3 / 2) - h)

|∂_r W_n / R| ≤ C (-τ)^{-3/2 - h}, from the segment representation of the quotient and the bound on ∂_r ∂_r W_n of eq:aniso:zoom:derivatives.

The finite-axis bound off the axis

theorem CIV.abs_zoomOmega_le {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hR : p.1.1 ≠ 0) : |zoomOmega lam h zc u p| ≤ C * ((lam ^ (2 * h)) ^ 2 * (-p.2) ^ (-(3 / 2) + h) + (-p.2) ^ (-(3 / 2) - h))

The finite-axis bound eq:aniso:zoom:finite:bound on the rescaled potential vorticity, away from the axis: there Ω_n is the quotient (δ² ∂_z V_n - ∂_r W_n)/R of eq:aniso:zoom:finite:identities, and each of the two quotients is controlled along the radial segment from the axis.

The finite-axis bound on the axis

theorem CIV.abs_zoomOmega_axis_le {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hR : p.1.1 = 0) : |zoomOmega lam h zc u p| ≤ C * ((lam ^ (2 * h)) ^ 2 * (-p.2) ^ (-(3 / 2) + h) + (-p.2) ^ (-(3 / 2) - h))

The finite-axis bound eq:aniso:zoom:finite:bound on the axis itself, where the continuous extension of Ω_n is δ² ∂_r ∂_z V_n - ∂_r ∂_r W_n.

theorem CIV.abs_zoomOmega_le_of_mem {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) : |zoomOmega lam h zc u p| ≤ C * ((lam ^ (2 * h)) ^ 2 * (-p.2) ^ (-(3 / 2) + h) + (-p.2) ^ (-(3 / 2) - h))

The finite-axis bound eq:aniso:zoom:finite:bound at every point of the rescaled cylinder, on and off the axis.

theorem CIV.abs_zoomOmega_le_two_mul_const {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hC : 0 ≤ C) (hδ : lam ^ (2 * h) ≤ 1) (hh0 : 0 < h) (hh1 : h < 1 / 2) (hτ : p.2 ≤ -1) : |zoomOmega lam h zc u p| ≤ 2 * C

The uniform-in-n form of eq:aniso:zoom:finite:bound used by the comparison argument: once the rescaled time satisfies τ ≤ -1 and the anisotropic ratio δ = λ^{2h} is at most 1, both powers of -τ are at most 1 and the finite-axis bound collapses to 2C.

The Step 2 drift bounds

theorem CIV.abs_zoomV_le_rpow_neg_half {C h lam zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hC : 0 ≤ C) (hτ : p.2 ≤ -1) : |zoomV lam h zc u p| ≤ C * (-p.2) ^ (-(1 / 2))

Drift bound for V_n (eq:aniso:zoom:derivatives, exponent -1/2).

theorem CIV.abs_dr_zoomV_le_rpow_neg_half {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hC : 0 ≤ C) (hτ : p.2 ≤ -1) : |dr (zoomV lam h zc u) p| ≤ C * (-p.2) ^ (-(1 / 2))

Drift bound for ∂_r V_n (eq:aniso:zoom:derivatives, exponent -1).

theorem CIV.abs_dz_zoomV_le_rpow_neg_half {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (hτ : p.2 ≤ -1) : |dz (zoomV lam h zc u) p| ≤ C * (-p.2) ^ (-(1 / 2))

Drift bound for ∂_z V_n (eq:aniso:zoom:derivatives, exponent -1 + h).

theorem CIV.abs_zoomW_le_rpow_neg_half {C h lam zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hτ : p.2 ≤ -1) : |zoomW lam h zc u p| ≤ C * (-p.2) ^ (-(1 / 2))

Drift bound for W_n (eq:aniso:zoom:derivatives, exponent -1/2 - h).

theorem CIV.abs_dr_zoomW_le_rpow_neg_half {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hτ : p.2 ≤ -1) : |dr (zoomW lam h zc u) p| ≤ C * (-p.2) ^ (-(1 / 2))

Drift bound for ∂_r W_n (eq:aniso:zoom:derivatives, exponent -1 - h).

theorem CIV.abs_dz_zoomW_le_rpow_neg_half {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hC : 0 ≤ C) (hτ : p.2 ≤ -1) : |dz (zoomW lam h zc u) p| ≤ C * (-p.2) ^ (-(1 / 2))

Drift bound for ∂_z W_n (eq:aniso:zoom:derivatives, exponent -1).

The quotient of the radial velocity by the radius

theorem CIV.zoomV_axis (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (haxi : IsAxisymmetricOn u unitCylinder) {Z τ : ℝ} (hp : zoomPoint lam h zc ((0, Z), τ) ∈ unitCylinder) : zoomV lam h zc u ((0, Z), τ) = 0

The radial velocity of an axisymmetric field vanishes on the axis of the zoom-in map (the standing assumptions of Section sec:aniso:equations). At p.1.1 = 0 the zoom point lies on the rotation axis, so apply_axis_zero forces u_r = 0 and hence zoomV = 0.

theorem CIV.abs_zoomV_div_le {C h lam zc : ℝ} (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) {p : (ℝ × ℝ) × ℝ} (hp : zoomPoint lam h zc p ∈ unitCylinder) (hR : p.1.1 ≠ 0) (hC : 0 ≤ C) (hτ : p.2 ≤ -1) : |zoomV lam h zc u p / p.1.1| ≤ C * (-p.2) ^ (-(1 / 2))

|V_n/R| ≤ sup |∂_R V_n| along the radial segment to the axis, the estimate recorded before eq:drift:Bn:def: V_n vanishes at R = 0, the segment stays in the preimage of the unit cylinder, and eq:aniso:zoom:derivatives bounds ∂_R V_n there by C (-τ)^{-1/2} once τ ≤ -1.

The lifted drift of Step 2

noncomputable def CIV.zoomLiftRadius (X : CKN.Vec 5) : ℝ

The radius R = |X| of the four-dimensional part of the lifted spatial variable (X, Z) ∈ ℝ⁴ × ℝ, in which the radial operator ∂_RR + 3R⁻¹∂_R of eq:aniso:zoom:finite:equation is the Laplacian of ℝ⁴ acting on radial functions.

Equations

• CIV.zoomLiftRadius X = √(X 0 ^ 2 + X 1 ^ 2 + X 2 ^ 2 + X 3 ^ 2)

noncomputable def CIV.zoomLiftPoint (q : CKN.Vec 5 × ℝ) : (ℝ × ℝ) × ℝ

The meridional point (R, Z, τ) = (|X|, Z, τ) underlying the lifted point (X, Z, τ).

Equations

• CIV.zoomLiftPoint q = ((CIV.zoomLiftRadius q.1, q.1 4), q.2)

theorem CIV.zoomLiftRadius_nonneg (X : CKN.Vec 5) : 0 ≤ zoomLiftRadius X

The lifted radius is nonnegative.

theorem CIV.abs_le_zoomLiftRadius (X : CKN.Vec 5) {i : Fin 5} (hi : i ≠ 4) : |X i| ≤ zoomLiftRadius X

Each of the four radial coordinates is bounded by the lifted radius.

theorem CIV.abs_div_zoomLiftRadius_le_one (X : CKN.Vec 5) {i : Fin 5} (hi : i ≠ 4) : |X i / zoomLiftRadius X| ≤ 1

The direction field X/|X| is bounded by one, including at the axis, where the junk value of the division is 0.

noncomputable def CIV.zoomDrift (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (q : CKN.Vec 5 × ℝ) : CKN.Vec 5

The Step 2 drift eq:drift:Bn:def, B_n(X, Z, τ) = (V_n(|X|, Z, τ) X/|X|, W_n(|X|, Z, τ)) on ℝ⁴ × ℝ. The four radial components take the value 0 on the axis X = 0, which is both the junk value of the division and, since V_n vanishes there by zoomV_axis, the continuous extension.

Equations

• CIV.zoomDrift lam h zc u q i = if i = 4 then CIV.zoomW lam h zc u (CIV.zoomLiftPoint q) else CIV.zoomV lam h zc u (CIV.zoomLiftPoint q) * (q.1 i / CIV.zoomLiftRadius q.1)

theorem CIV.zoomDrift_apply_axis (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) {q : CKN.Vec 5 × ℝ} (hR : zoomLiftRadius q.1 = 0) {i : Fin 5} (hi : i ≠ 4) : zoomDrift lam h zc u q i = 0

The four radial components of the lifted drift vanish on the axis.

theorem CIV.norm_zoomDrift_le {C h lam zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hτ : q.2 ≤ -1) : ‖zoomDrift lam h zc u q‖ ≤ C * (-q.2) ^ (-(1 / 2))

The uniform bound |B_n| ≤ C |τ|^{-1/2} for τ ≤ -1 on the lifted drift of eq:drift:Bn:def: the four radial components are V_n times a direction vector of length at most one, and the vertical component is W_n, so the two drift bounds of eq:aniso:zoom:derivatives bound every component.

The divergence of the lifted drift

theorem CIV.exists_zoomLiftRadius_update (X : CKN.Vec 5) {i : Fin 5} (hi : i ≠ 4) : ∃ (rest : ℝ), 0 ≤ rest ∧ ∀ (s : ℝ), zoomLiftRadius (Function.update X i s) = √(s ^ 2 + rest)

Freezing all but one of the four radial coordinates leaves the lifted radius a function s ↦ √(s² + rest) of the remaining one, with rest the sum of the other three squares.

theorem CIV.zoomLiftRadius_update_four (X : CKN.Vec 5) (s : ℝ) : zoomLiftRadius (Function.update X 4 s) = zoomLiftRadius X

The lifted radius does not depend on the vertical coordinate.

theorem CIV.hasDerivAt_sqrt_sq_add {rest a : ℝ} (hpos : 0 < a ^ 2 + rest) : HasDerivAt (fun (s : ℝ) => √(s ^ 2 + rest)) (a / √(a ^ 2 + rest)) a

∂_s √(s² + rest) = s/√(s² + rest) away from the origin.

theorem CIV.hasDerivAt_zoomV_radial (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : HasDerivAt (fun (r : ℝ) => zoomV lam h zc u ((r, p.1.2), p.2)) (dr (zoomV lam h zc u) p) p.1.1

V_n restricted to a radial slice has derivative ∂_R V_n.

theorem CIV.hasDerivAt_zoomW_radial (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : HasDerivAt (fun (r : ℝ) => zoomW lam h zc u ((r, p.1.2), p.2)) (dr (zoomW lam h zc u) p) p.1.1

W_n restricted to a radial slice has derivative ∂_R W_n.

theorem CIV.hasDerivAt_zoomV_vertical (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : HasDerivAt (fun (s : ℝ) => zoomV lam h zc u ((p.1.1, s), p.2)) (dz (zoomV lam h zc u) p) p.1.2

V_n restricted to a vertical slice has derivative ∂_Z V_n.

theorem CIV.hasDerivAt_zoomW_vertical (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) : HasDerivAt (fun (s : ℝ) => zoomW lam h zc u ((p.1.1, s), p.2)) (dz (zoomW lam h zc u) p) p.1.2

W_n restricted to a vertical slice has derivative ∂_Z W_n.

theorem CIV.deriv_zoomDrift_coord (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hR : 0 < zoomLiftRadius q.1) {i : Fin 5} (hi : i ≠ 4) : deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 i s, q.2) i) (q.1 i) = dr (zoomV lam h zc u) (zoomLiftPoint q) * (q.1 i ^ 2 / zoomLiftRadius q.1 ^ 2) + zoomV lam h zc u (zoomLiftPoint q) * ((zoomLiftRadius q.1 ^ 2 - q.1 i ^ 2) / zoomLiftRadius q.1 ^ 3)

The i-th diagonal entry of ∇_X(V_n X/R) for one of the four radial coordinates: ∂_{X_i}(V_n X_i/R) = ∂_R V_n · X_i²/R² + V_n (R² - X_i²)/R³, away from the axis.

theorem CIV.deriv_zoomDrift_vertical (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) : deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 4 s, q.2) 4) (q.1 4) = dz (zoomW lam h zc u) (zoomLiftPoint q)

The vertical entry of ∇B_n: the fifth component of the lifted drift depends on the fifth coordinate through W_n alone, so its derivative is ∂_Z W_n.

theorem CIV.deriv_zoomDrift_coord_dz (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) {j : Fin 5} (hj : j ≠ 4) : deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 4 s, q.2) j) (q.1 4) = dz (zoomV lam h zc u) (zoomLiftPoint q) * (q.1 j / zoomLiftRadius q.1)

The vertical entry of a radial row of ∇B_n: a radial component j of the lifted drift, differentiated in the vertical direction, depends on the fifth coordinate through V_n alone, scaled by the fixed direction cosine X_j/R. No positivity of the radius is needed, since the factor X_j/R is unchanged by the differentiation.

theorem CIV.deriv_zoomDrift_vertical_dr (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hR : 0 < zoomLiftRadius q.1) {i : Fin 5} (hi : i ≠ 4) : deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 i s, q.2) 4) (q.1 i) = dr (zoomW lam h zc u) (zoomLiftPoint q) * (q.1 i / zoomLiftRadius q.1)

The radial entry of the vertical row of ∇B_n: the vertical component of the lifted drift, differentiated in a radial direction i, is ∂_R W_n at the underlying meridional point, scaled by the direction cosine X_i/R, exactly as in hasDerivAt_zoomV_radial's composition with the lifted radius but for W_n in place of V_n.

theorem CIV.deriv_zoomDrift_offdiag (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hR : 0 < zoomLiftRadius q.1) {i j : Fin 5} (hi : i ≠ 4) (hj : j ≠ 4) (hij : i ≠ j) : deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 i s, q.2) j) (q.1 i) = dr (zoomV lam h zc u) (zoomLiftPoint q) * (q.1 i * q.1 j / zoomLiftRadius q.1 ^ 2) - zoomV lam h zc u (zoomLiftPoint q) * (q.1 i * q.1 j / zoomLiftRadius q.1 ^ 3)

Away from the axis, the j-th radial component of the lifted drift, differentiated in a different radial coordinate i, depends on i only through the common factor V_n/R: X_j is held fixed by the update, so the product rule leaves only the derivative of the quotient V_n(R(s), Z)/R(s), computed exactly as in deriv_zoomDrift_coord but without the extra s/R(s) factor that appears there when i = j.

Bounds on the entries of ∇B_n

theorem CIV.abs_deriv_zoomDrift_vertical_le {C h lam zc : ℝ} (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) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hC : 0 ≤ C) (hτ : q.2 ≤ -1) : |deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 4 s, q.2) 4) (q.1 4)| ≤ C * (-q.2) ^ (-(1 / 2))

The vertical entry of the vertical row of ∇B_n is bounded by the ∂_Z W_n drift bound of eq:aniso:zoom:derivatives.

theorem CIV.abs_deriv_zoomDrift_coord_dz_le {C h lam zc : ℝ} (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) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (hτ : q.2 ≤ -1) {j : Fin 5} (hj : j ≠ 4) : |deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 4 s, q.2) j) (q.1 4)| ≤ C * (-q.2) ^ (-(1 / 2))

The vertical entry of a radial row of ∇B_n is bounded by the ∂_Z V_n drift bound times a direction cosine of absolute value at most one.

theorem CIV.abs_deriv_zoomDrift_vertical_dr_le {C h lam zc : ℝ} (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) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hR : 0 < zoomLiftRadius q.1) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hτ : q.2 ≤ -1) {i : Fin 5} (hi : i ≠ 4) : |deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 i s, q.2) 4) (q.1 i)| ≤ C * (-q.2) ^ (-(1 / 2))

The radial entry of the vertical row of ∇B_n is bounded by the ∂_R W_n drift bound times a direction cosine of absolute value at most one.

theorem CIV.abs_deriv_zoomDrift_coord_le {C h lam zc : ℝ} (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) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hR : 0 < zoomLiftRadius q.1) (hC : 0 ≤ C) (hτ : q.2 ≤ -1) {i : Fin 5} (hi : i ≠ 4) : |deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 i s, q.2) i) (q.1 i)| ≤ 2 * C * (-q.2) ^ (-(1 / 2))

The diagonal entry of a radial row of ∇B_n is bounded by twice the V_n/∂_R V_n drift bounds of eq:aniso:zoom:derivatives, using that V_n vanishes on the axis.

theorem CIV.abs_deriv_zoomDrift_offdiag_le {C h lam zc : ℝ} (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) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hR : 0 < zoomLiftRadius q.1) (hC : 0 ≤ C) (hτ : q.2 ≤ -1) {i j : Fin 5} (hi : i ≠ 4) (hj : j ≠ 4) (hij : i ≠ j) : |deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 i s, q.2) j) (q.1 i)| ≤ 2 * C * (-q.2) ^ (-(1 / 2))

The off-diagonal entry of a radial row of ∇B_n is bounded by twice the V_n/∂_R V_n drift bounds, exactly as the diagonal entry: X_i X_j/R² and X_i X_j/R³ are each bounded by one direction cosine times another, and the second is absorbed into V_n/R.

theorem CIV.abs_deriv_zoomDrift_le {C h lam zc : ℝ} (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) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hR : 0 < zoomLiftRadius q.1) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) (hτ : q.2 ≤ -1) {i j : Fin 5} : |deriv (fun (s : ℝ) => zoomDrift lam h zc u (Function.update q.1 i s, q.2) j) (q.1 i)| ≤ 2 * C * (-q.2) ^ (-(1 / 2))

The uniform bound |∇B_n| ≤ 2 C |τ|^{-1/2} on every entry of the Jacobian of the lifted drift eq:drift:Bn:def away from the axis, for τ ≤ -1: differentiating any one of the five lifted components B_n in any one of the five lifted directions gives a value bounded by 2 C (-τ)^{-1/2}, from the drift bounds of eq:aniso:zoom:derivatives together with the direction cosines |X_i/R| ≤ 1. Combined with norm_zoomDrift_le, this is the footnote's |B_n| + |∇B_n| ≤ C|τ|^{-1/2}.

noncomputable def CIV.zoomDriftJacobian (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (q : CKN.Vec 5 × ℝ) : Fin 5 → Fin 5 → ℝ

The Jacobian ∇B_n of the lifted drift eq:drift:Bn:def in the five lifted spatial coordinates: entry (i, j) is the j-th component of B_n differentiated in the i-th direction.

Equations

• CIV.zoomDriftJacobian lam h zc u q i j = deriv (fun (s : ℝ) => CIV.zoomDrift lam h zc u (Function.update q.1 i s, q.2) j) (q.1 i)

theorem CIV.norm_zoomDriftJacobian_le {C h lam zc : ℝ} (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) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hR : 0 < zoomLiftRadius q.1) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) (hτ : q.2 ≤ -1) : ‖zoomDriftJacobian lam h zc u q‖ ≤ 2 * C * (-q.2) ^ (-(1 / 2))

The footnote's |∇B_n| ≤ C |τ|^{-1/2} for τ ≤ -1, away from the axis, as a genuine norm bound on zoomDriftJacobian: combined with norm_zoomDrift_le, this is the pair of bounds |B_n| + |∇B_n| ≤ C|τ|^{-1/2} (up to the harmless factor of two carried by every entry of ∇B_n) recorded before eq:drift:Bn:def.

noncomputable def CIV.zoomDriftDivergence (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (q : CKN.Vec 5 × ℝ) : ℝ

The pointwise divergence of the lifted drift in the five lifted spatial coordinates.

Equations

• CIV.zoomDriftDivergence lam h zc u q = ∑ i : Fin 5, deriv (fun (s : ℝ) => CIV.zoomDrift lam h zc u (Function.update q.1 i s, q.2) i) (q.1 i)

theorem CIV.zoomDriftDivergence_eq (lam h zc : ℝ) (hlam : 0 < lam) (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 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hR : 0 < zoomLiftRadius q.1) : zoomDriftDivergence lam h zc u q = 2 * (zoomV lam h zc u (zoomLiftPoint q) / zoomLiftRadius q.1)

div_{X,Z} B_n = 2 V_n/R away from the axis. The four radial entries sum to the trace ∂_R V_n + 3 V_n/R of ∇_X(V_n X/R), because Σ X_i² = R²; adding ∂_Z W_n and using the divergence identity ∂_R V_n + V_n/R + ∂_Z W_n = 0 of eq:aniso:zoom:finite:identities leaves 2 V_n/R.