Growth bounds for the phase transition factor

The derivatives of the normal phase transition have polynomial growth on the active half-space strip.

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

The phase transition has first height derivative growing at most linearly in height on the active strip.

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

The phase transition has time derivative with quadratic height growth on the active strip.

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

The second height derivative of the phase transition grows at most quadratically in height on the active strip.