English
If f is continuous on R and f'' is strictly positive on R, then f is strictly convex on R.
Русский
Если f непрерывна на ℝ и f'' строго положительная на ℝ, то f строго выпукла на ℝ.
LaTeX
$$$\\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{Continuous}(f) \\Rightarrow (\\forall x, (\\mathrm{deriv}^{[2]} f)(x) > 0) \\Rightarrow \\text{StrictConvexOn}(\\mathbb{R}, \\mathbb{R}, f).$$
Lean4
/-- If a function `f` is continuous on `ℝ`, and `f''` is strictly positive on `ℝ`,
then `f` is strictly convex on `ℝ`.
Note that we don't require twice differentiability explicitly as it is already implied by the second
derivative being strictly positive, except at at most one point. -/
theorem strictConvexOn_univ_of_deriv2_pos {f : ℝ → ℝ} (hf : Continuous f) (hf'' : ∀ x, 0 < (deriv^[2] f) x) :
StrictConvexOn ℝ univ f :=
strictConvexOn_of_deriv2_pos' convex_univ hf.continuousOn fun x _ => hf'' x
