A one-dimensional second derivative test used by the parabolic maximum principle.

theorem deriv_deriv_nonpos_of_isLocalMax {f : ℝ → ℝ} {x : ℝ} (hf : ContDiff ℝ 2 f) (hmax : IsLocalMax f x) : deriv (deriv f) x ≤ 0