Bounds for the spatial and normal cutoff product

The spatial shell terms carry inverse powers of the radius, while the normal-phase terms have fixed polynomial height growth.

theorem ESS.buShortSpacePhase_spatialPartial_bound {scale R : ℝ} (hscale : 0 < scale) (hR : 0 < R) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hy : 2 < z.1 2) (hs : 1 / 2 ≤ z.2) (hs1 : z.2 ≤ 1) (j : Fin 3) : |CKN.spatialPartial (buCutScalar (buShortSpacePhaseCutoff scale R hR)) j z| ≤ CKN.cutoffGradientConstant / (2 * R) + (16 + 48 * (12 / buShortB scale)) * (1 + z.1 2)

The first spatial derivative of the two-factor cutoff separates the shell and normal-phase contributions.

theorem ESS.buShortSpacePhase_spatialSecondPartial_diag_bound {scale R C₁ C₂ : ℝ} (hscale : 0 < scale) (hR : 0 < R) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hy : 2 < z.1 2) (hs : 1 / 2 ≤ z.2) (hs1 : z.2 ≤ 1) (hC₁ : 0 ≤ C₁) (hN : ∀ (scale y : ℝ), |deriv (deriv (buShortNormalCutoff scale)) y| ≤ C₁) (hC₂ : 0 ≤ C₂) (hP : ∀ (x : ℝ), |deriv (deriv CKN.smoothTransitionProfile) x| ≤ C₂) (j : Fin 3) : |CKN.spatialSecondPartial (buCutScalar (buShortSpacePhaseCutoff scale R hR)) j j z| ≤ CKN.cutoffSecondDerivativeConstant / (2 * R) ^ 2 + 2 * (CKN.cutoffGradientConstant / (2 * R)) * ((16 + 48 * (12 / buShortB scale)) * (1 + z.1 2)) + (C₁ + 1536 * (12 / buShortB scale) + 36 * C₂ * (12 / buShortB scale) ^ 2 + 24 * (12 / buShortB scale)) * (1 + z.1 2) ^ 2

The diagonal spatial second derivative separates its shell, mixed, and normal-phase contributions.

theorem ESS.buShortSpacePhase_timePartial_bound {scale R : ℝ} (hscale : 0 < scale) (hR : 0 < R) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hy : 2 < z.1 2) (hs : 1 / 2 < z.2) (hs1 : z.2 ≤ 1) : |CKN.timePartial (buCutScalar (buShortSpacePhaseCutoff scale R hR)) z| ≤ 56 * (12 / buShortB scale) * (1 + z.1 2) ^ 2

The time derivative of the two-factor cutoff has only the normal-phase contribution.