Growth bounds for the normal cutoff derivatives

The fixed normal transition and the phase transition give a single quadratic height bound for all derivatives used by the heat product rule.

theorem ESS.buShortEtaScalar_deriv_height_bound {scale y s : ℝ} (hscale : 0 < scale) (hy : 2 < y) (hs : 1 / 2 ≤ s) (hs1 : s ≤ 1) : |deriv (fun (r : ℝ) => buShortEtaScalar scale r s) y| ≤ (16 + 48 * (12 / buShortB scale)) * (1 + y)

The height derivative of the normal cutoff has linear growth on the active strip.

theorem ESS.buShortEtaScalar_deriv_time_bound {scale y s : ℝ} (hscale : 0 < scale) (hy : 2 < y) (hs : 1 / 2 < s) (hs1 : s ≤ 1) : |deriv (fun (t : ℝ) => buShortEtaScalar scale y t) s| ≤ 56 * (12 / buShortB scale) * (1 + y) ^ 2

The time derivative of the normal cutoff has quadratic height growth on the active strip.

theorem ESS.buShortEtaScalar_deriv_height_twice_bound {scale y s C₁ C₂ : ℝ} (hscale : 0 < scale) (hy : 2 < y) (hs : 1 / 2 ≤ s) (hs1 : s ≤ 1) (hC₁ : 0 ≤ C₁) (hN : ∀ (scale y : ℝ), |deriv (deriv (buShortNormalCutoff scale)) y| ≤ C₁) (hC₂ : 0 ≤ C₂) (hP : ∀ (x : ℝ), |deriv (deriv CKN.smoothTransitionProfile) x| ≤ C₂) : |deriv (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortEtaScalar scale q s) r) y| ≤ (C₁ + 1536 * (12 / buShortB scale) + 36 * C₂ * (12 / buShortB scale) ^ 2 + 24 * (12 / buShortB scale)) * (1 + y) ^ 2

The second height derivative of the normal cutoff has quadratic height growth on the active strip.