English
If f is differentiable on a convex domain D and its second derivative is strictly negative on D, then f is strictly concave on D.
Русский
Если f дифференцируема на D и f''(strictly negative) на D, то f строго вогнута на D.
LaTeX
$$$\\forall D \\subseteq \\mathbb{R},\\; \\text{Convex}(D) \\Rightarrow \\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{DifferentiableOn}(f, D) \\Rightarrow (\\forall x\\in D, (\\mathrm{deriv}^{[2]} f)(x) < 0) \\Rightarrow \\text{StrictConcaveOn}(\\mathbb{R}, D, f).$$
Lean4
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ` and `f''` is strictly negative on `D`,
then `f` is strictly concave on `D`.
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_of_deriv2_neg' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf'' : ∀ x ∈ D, deriv^[2] f x < 0) : StrictConcaveOn ℝ D f :=
strictConcaveOn_of_deriv2_neg hD hf fun x hx => hf'' x (interior_subset hx)
