English
If D is convex, f continuous on D, differentiable on interior(D), and deriv f is differentiable with second derivative nonpositive on interior(D), then f is concave on D.
Русский
Если D выпукло, f непрерывна на D, дифференцируема на interior(D), а вторая производная не положительна на interior(D), то f конкавна на D.
LaTeX
$$$$\\operatorname{ConcaveOn}_{\\mathbb{R}} D f \\leftarrow \\operatorname{ContinuousOn} f D \\land \\operatorname{DifferentiableOn} f (\\operatorname{interior} D) \\land \\operatorname{DifferentiableOn} (\\operatorname{deriv} f) (\\operatorname{interior} D) \\land (\\forall x \\in \\operatorname{interior} D, \\operatorname{deriv} f x'' \\le 0).$$$$
Lean4
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
interior, and `f''` is nonpositive on the interior, then `f` is concave on `D`. -/
theorem concaveOn_of_deriv2_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : DifferentiableOn ℝ f (interior D)) (hf'' : DifferentiableOn ℝ (deriv f) (interior D))
(hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0) : ConcaveOn ℝ D f :=
(antitoneOn_of_deriv_nonpos hD.interior hf''.continuousOn (by rwa [interior_interior]) <| by
rwa [interior_interior]).concaveOn_of_deriv
hD hf hf'
