Receding Second Derivative Bounds W

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.abs_drdr_zoomWRec_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) (hh0 : 0 ≤ h) (hτ : p.2 ≤ -1) : |dr (dr (zoomWRec lam h rc zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2))

Uniform second-derivative bound eq:aniso:zoom:derivatives for ∂_R∂_R W_n in the receding-axis recentred rescaled variables, the receding-axis analogue of CIV.abs_dr_zoomW_le_rpow_neg_half one derivative order further: the raw combined bound abs_drdr_zoomWRec_add_abs_drdr_zoomSRec_le supplies |∂_R∂_R W_n| + |∂_R∂_R S_n| ≤ C (-τ)^{-3/2 - h}, and dropping the S_n summand and normalizing the exponent to -1/2 for τ ≤ -1 gives the uniform estimate needed by the corresponding statement.

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

Uniform second-derivative bound eq:aniso:zoom:derivatives for ∂_R∂_Z W_n in the receding-axis recentred rescaled variables, the receding-axis analogue of CIV.abs_dz_zoomW_le_rpow_neg_half one derivative order further: the raw combined bound abs_drdz_zoomWRec_add_abs_drdz_zoomSRec_le supplies |∂_R∂_Z W_n| + |∂_R∂_Z S_n| ≤ C (-τ)^{-3/2}, the h terms cancelling, and dropping the S_n summand and normalizing the exponent to -1/2 for τ ≤ -1 gives the uniform estimate.

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

Uniform second-derivative bound eq:aniso:zoom:derivatives for ∂_Z∂_Z W_n in the receding-axis recentred rescaled variables, the receding-axis analogue of CIV.abs_dz_zoomW_le_rpow_neg_half one derivative order further: the raw combined bound abs_dzdz_zoomWRec_add_abs_dzdz_zoomSRec_le supplies |∂_Z∂_Z W_n| + |∂_Z∂_Z S_n| ≤ C (-τ)^{-3/2 + h}, and dropping the S_n summand and normalizing the exponent to -1/2 for τ ≤ -1 with h ≤ 1/2 gives the uniform estimate.