Documentation

LeanPool.CIVAxisymmetric.Zoom.RecedingSecondDerivativeBoundsV

Exponent normalization for the receding-axis radial field #

source
theorem CIV.abs_drdr_zoomVRec_le_rpow_neg_half {C h lam rc 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 : zoomPointRec lam h rc zc p ∈ unitCylinder) (hC : 0 ≤ C) (hτ : p.2 ≤ -1) :
|dr (dr (zoomVRec lam h rc zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2))

Second-derivative bound eq:aniso:zoom:derivatives for ∂_R∂_R V_n in the receding-axis recentred rescaled radial field, normalizing the raw combined-exponent bound abs_drdr_zoomVRec_le to the single exponent -1/2 for τ ≤ -1.

source
theorem CIV.abs_drdz_zoomVRec_le_rpow_neg_half {C h lam rc 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 : zoomPointRec lam h rc zc p ∈ unitCylinder) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (hτ : p.2 ≤ -1) :
|dr (dz (zoomVRec lam h rc zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2))

Second-derivative bound eq:aniso:zoom:derivatives for ∂_R∂_Z V_n in the receding-axis recentred rescaled radial field, normalizing the raw combined-exponent bound abs_drdz_zoomVRec_le to the single exponent -1/2 for τ ≤ -1 and h ≤ 1/2.

source
theorem CIV.abs_dzdz_zoomVRec_le_rpow_neg_half {C h lam rc 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 : zoomPointRec lam h rc zc p ∈ unitCylinder) (hC : 0 ≤ C) (hh1 : h ≤ 1 / 2) (hτ : p.2 ≤ -1) :
|dz (dz (zoomVRec lam h rc zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2))

Second-derivative bound eq:aniso:zoom:derivatives for ∂_Z∂_Z V_n in the receding-axis recentred rescaled radial field, normalizing the raw combined-exponent bound abs_dzdz_zoomVRec_le to the single exponent -1/2 for τ ≤ -1 and h ≤ 1/2.