English
If f is continuous and f' is strictly monotone on ℝ, then f is strictly convex on the entire real line.
Русский
Если f непрерывна и f' строго монотонна на всей ℝ, то f строго выпукла на всей ℝ.
LaTeX
$$$$\\text{Continuous}(f) \\land \\text{StrictMonoOn}(\\text{deriv } f)(\\mathbb{R}) \\Rightarrow \\text{StrictConvexOn}_{\\mathbb{R}} \\mathbb{R} f.$$$$
Lean4
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ` and `f'` is strictly antitone on the
interior, then `f` is strictly concave on `D`.
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_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(h_anti : StrictAntiOn (deriv f) (interior D)) : StrictConcaveOn ℝ D f :=
have : StrictMonoOn (deriv (-f)) (interior D) := by simpa only [← deriv.neg] using h_anti.neg
neg_neg f ▸ (this.strictConvexOn_of_deriv hD hf.neg).neg
