English
If f is continuous and f' is strictly antitone on ℝ, then f is strictly concave on ℝ.
Русский
Если f непрерывна и f' строго антитоническая на ℝ, то f строго конкавна на ℝ.
LaTeX
$$$$\\text{Continuous}(f) \\land \\text{StrictAnti}(\\operatorname{deriv} f) \\Rightarrow \\operatorname{StrictConcaveOn}_{\\mathbb{R}} \\mathbb{R} f.$$$$
Lean4
/-- If a function `f` is continuous and `f'` is strictly antitone on `ℝ` then `f` is strictly
concave. Note that we don't require differentiability, since it is guaranteed at all but at most
one point by the strict antitonicity of `f'`. -/
theorem strictConcaveOn_univ_of_deriv {f : ℝ → ℝ} (hf : Continuous f) (hf'_anti : StrictAnti (deriv f)) :
StrictConcaveOn ℝ univ f :=
(hf'_anti.strictAntiOn _).strictConcaveOn_of_deriv convex_univ hf.continuousOn
