English
If f is continuous on a convex set D and its second derivative is strictly negative on the interior, then f is strictly concave on D.
Русский
Пусть f непрерывна на выпуклом D и f'' на внутренности D строго отрицательна; тогда f строго вогнута на D.
LaTeX
$$$\\forall D \\subseteq \\mathbb{R},\\; \\text{Convex}(D) \\Rightarrow \\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{ContinuousOn}(f,D) \\Rightarrow \\big(\\forall x\\in \\mathrm{intr}(D), \\; (\\mathrm{deriv}^{[2]} f)(x) < 0\\big) \\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 the
interior, then `f` is strictly concave on `D`.
Note that we don't require twice differentiability explicitly as it 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 ∈ interior D, deriv^[2] f x < 0) : StrictConcaveOn ℝ D f :=
((strictAntiOn_of_deriv_neg hD.interior fun z hz =>
(differentiableAt_of_deriv_ne_zero (hf'' z hz).ne).differentiableWithinAt.continuousWithinAt) <|
by rwa [interior_interior]).strictConcaveOn_of_deriv
hD hf
