English
If f is continuous on ℝ and f' is strictly monotone on ℝ, then f is strictly convex on ℝ.
Русский
Если f непрерывна на ℝ и f' строго монотонна на ℝ, то f строго выпукла на ℝ.
LaTeX
$$$$\\text{Continuous}(f) \\land \\text{StrictMono}(\\operatorname{deriv} f) \\Rightarrow \\operatorname{StrictConvexOn}_{\\mathbb{R}} \\mathbb{R} f.$$$$
Lean4
/-- If a function `f` is continuous and `f'` is strictly monotone on `ℝ` then `f` is strictly
convex. Note that we don't require differentiability, since it is guaranteed at all but at most
one point by the strict monotonicity of `f'`. -/
theorem strictConvexOn_univ_of_deriv {f : ℝ → ℝ} (hf : Continuous f) (hf'_mono : StrictMono (deriv f)) :
StrictConvexOn ℝ univ f :=
(hf'_mono.strictMonoOn _).strictConvexOn_of_deriv convex_univ hf.continuousOn
