English
Under the same hypotheses as ConvexFromDeriv, the result holds; if f is continuous on D, differentiable on interior(D), and deriv is monotone on interior(D), then f is convex on D.
Русский
При тех же условиях, что и в предыдущем утверждении, вывод остаётся: непрерывность на D, дифференцируемость на interior(D) и монотонность deriv на interior(D) → выпуклость на D.
LaTeX
$$$$\\operatorname{ConvexOn}_{\\mathbb{R}} D f \\Leftarrow \\operatorname{ContinuousOn} f D \\;\\&\\; \\operatorname{DifferentiableOn} f (\\operatorname{interior} D) \\;\\&\\; \\operatorname{MonotoneOn}(\\operatorname{deriv} f)(\\operatorname{interior} D).$$$$
Lean4
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
and `f'` is antitone on the interior, then `f` is concave on `D`. -/
theorem concaveOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : DifferentiableOn ℝ f (interior D)) (h_anti : AntitoneOn (deriv f) (interior D)) : ConcaveOn ℝ D f :=
haveI : MonotoneOn (deriv (-f)) (interior D) := by simpa only [← deriv.neg] using h_anti.neg
neg_convexOn_iff.mp (this.convexOn_of_deriv hD hf.neg hf'.neg)
