Scalar derivative sizes of the two-factor cutoff #
The gradient and heat sizes are bounded by a phase polynomial and inverse-radius shell terms.
theorem
ESS.buShortSpacePhaseGradientSize_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)
:
The sum of absolute spatial derivatives separates the spatial shell from the normal-phase growth.
theorem
ESS.buShortSpacePhaseHeatSize_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₂)
:
buShortSpacePhaseHeatSize scale R hR z ≤ 56 * (12 / buShortB scale) * (1 + z.1 2) ^ 2 + 3 * (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 absolute scalar heat derivative separates the spatial shell from quadratic normal-phase growth.