The Step 2 second-derivative bounds

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

Second-derivative bound for ∂_R∂_R V_n (eq:aniso:zoom:derivatives, exponent -1/2).

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

Second-derivative bound for ∂_R∂_Z V_n (eq:aniso:zoom:derivatives, exponent -1).

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

Second-derivative bound for ∂_Z∂_Z V_n (eq:aniso:zoom:derivatives, exponent -1 + 2h).