Derivatives of the normal transition cutoff

The fixed-width height transition has uniform first and second derivative bounds independent of the spatial cutoff radius.

theorem ESS.buShortNormalCutoff_affine (scale : ℝ) : buShortNormalCutoff scale = fun (y : ℝ) => CKN.smoothTransitionProfile (2 * (y - buShortYMinus scale))

The height cutoff is the canonical profile on an affine argument of slope two.

theorem ESS.buShortNormalCutoff_deriv (scale y : ℝ) : deriv (buShortNormalCutoff scale) y = 2 * deriv CKN.smoothTransitionProfile (2 * (y - buShortYMinus scale))

First derivative of the fixed-width height cutoff.

theorem ESS.buShortNormalCutoff_deriv_twice (scale y : ℝ) : deriv (deriv (buShortNormalCutoff scale)) y = 4 * deriv (deriv CKN.smoothTransitionProfile) (2 * (y - buShortYMinus scale))

Second derivative of the fixed-width height cutoff.

theorem ESS.buShortNormalCutoff_abs_deriv_le (scale y : ℝ) : |deriv (buShortNormalCutoff scale) y| ≤ 16

The first height derivative is bounded by sixteen.

theorem ESS.buShortNormalCutoff_abs_deriv_twice_le : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (scale y : ℝ), |deriv (deriv (buShortNormalCutoff scale)) y| ≤ C

The second height derivative has one global bound independent of scale.