English
If f is continuous on R and f'' is strictly negative on R, then f is strictly concave on R.
Русский
Если f непрерывна на ℝ и f'' на ℝ строго отрицательна, то f строго вогнута на ℝ.
LaTeX
$$$\\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{Continuous}(f) \\Rightarrow (\\forall x, (\\mathrm{deriv}^{[2]} f)(x) < 0) \\Rightarrow \\text{StrictConcaveOn}(\\mathbb{R}, \\mathbb{R}, f).$$
Lean4
/-- If a function `f` is continuous on `ℝ`, and `f''` is strictly negative on `ℝ`,
then `f` is strictly concave on `ℝ`.
Note that we don't require twice differentiability explicitly as it is already implied by the second
derivative being strictly negative, except at at most one point. -/
theorem strictConcaveOn_univ_of_deriv2_neg {f : ℝ → ℝ} (hf : Continuous f) (hf'' : ∀ x, deriv^[2] f x < 0) :
StrictConcaveOn ℝ univ f :=
strictConcaveOn_of_deriv2_neg' convex_univ hf.continuousOn fun x _ => hf'' x
