English
If f is twice differentiable on an open convex set D and f'' is strictly negative on D, then f is strictly concave on D.
Русский
Если f дважды дифференцируема на открытом выпуклом D и f'' строго отрицательно на D, то f строго вогнута на D.
LaTeX
$$$\\forall D \\subseteq \\mathbb{R},\\; \\text{Convex}(D) \\text{ открыто} \\Rightarrow \\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{DifferentiableOn}(f, D) \\Rightarrow \\text{DifferentiableOn}(\\mathrm{deriv}\,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 twice differentiable on an open convex set `D ⊆ ℝ` and
`f''` is nonpositive on `D`, then `f` is concave on `D`. -/
theorem concaveOn_of_deriv2_nonpos' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf' : DifferentiableOn ℝ f D)
(hf'' : DifferentiableOn ℝ (deriv f) D) (hf''_nonpos : ∀ x ∈ D, deriv^[2] f x ≤ 0) : ConcaveOn ℝ D f :=
concaveOn_of_deriv2_nonpos hD hf'.continuousOn (hf'.mono interior_subset) (hf''.mono interior_subset) fun x hx =>
hf''_nonpos x (interior_subset hx)
