Size and support of the lower-time derivative

The derivative of the initial-time transition is bounded by 8/ε and vanishes outside its transition strip.

theorem ESS.buShortTimeCutoff_deriv (ε s : ℝ) : deriv (buShortTimeCutoff ε) s = deriv (ucInitialTimeCutoff ε) (s - 1 / 2)

Differentiation commutes with shifting the time cutoff by one half.

theorem ESS.buShortTimeCutoff_abs_deriv_le {ε : ℝ} (hε : 0 < ε) (s : ℝ) : |deriv (buShortTimeCutoff ε) s| ≤ 8 / ε

The absolute derivative of the short-time cutoff is at most 8/ε.

theorem ESS.buShortTimeCutoff_deriv_eq_zero_early {ε s : ℝ} (hε : 0 < ε) (hs : s < 1 / 2 + ε) : deriv (buShortTimeCutoff ε) s = 0

The lower-time derivative vanishes before the transition strip.

theorem ESS.buShortTimeCutoff_deriv_eq_zero_late {ε s : ℝ} (hε : 0 < ε) (hs : 1 / 2 + 2 * ε < s) : deriv (buShortTimeCutoff ε) s = 0

The lower-time derivative vanishes after the transition strip.