Normalizer for the second-derivative exponent

The uniform second-derivative half of eq:aniso:zoom:derivatives for W_n

theorem CIV.abs_drdr_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 (dr (zoomW lam h zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2))

Uniform bound for ∂_R∂_R W_n (eq:aniso:zoom:derivatives, exponent -3/2 - h). The raw combined bound abs_drdr_zoomW_add_abs_drdr_zoomS_le contains a swirl summand |dr(dr(zoomS))|; dropping it by nonnegativity and normalizing the remaining W_n bound to the standard τ ≤ -1 form gives the uniform estimate.

theorem CIV.abs_drdz_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) : |dr (dz (zoomW lam h zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2))

Uniform bound for ∂_R∂_Z W_n (eq:aniso:zoom:derivatives, exponent -3/2). The raw combined bound abs_drdz_zoomW_add_abs_drdz_zoomS_le contains a swirl summand |dr(dz(zoomS))|; dropping it by nonnegativity and normalizing the remaining W_n bound to the standard τ ≤ -1 form gives the uniform estimate.

theorem CIV.abs_dzdz_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) (hh1 : h ≤ 1 / 2) (hτ : p.2 ≤ -1) : |dz (dz (zoomW lam h zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2))

Uniform bound for ∂_Z∂_Z W_n (eq:aniso:zoom:derivatives, exponent -3/2 + h). The raw combined bound abs_dzdz_zoomW_add_abs_dzdz_zoomS_le contains a swirl summand |dz(dz(zoomS))|; dropping it by nonnegativity and normalizing the remaining W_n bound to the standard τ ≤ -1 form gives the uniform estimate.