English
If f is continuous on a convex set D and its second derivative is strictly positive on the interior, then f is strictly convex on D.
Русский
Пусть f непрерывна на выпуклом D и f'' строго положительна внутри D; тогда f строго выпукла на D.
LaTeX
$$$\\forall D \\subseteq \\mathbb{R},\\; \\text{Convex}(D) \\Rightarrow \\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{ContinuousOn}(f,D) \\Rightarrow \\big(\\forall x\\in \\mathrm{intr}(D), 0 < (\\text{deriv}^{[2]} f)(x)\\big) \\Rightarrow \\text{StrictConvexOn}(\\mathbb{R}, D, f).$$
Lean4
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ` and `f''` is strictly positive on the
interior, then `f` is strictly convex on `D`.
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_of_deriv2_pos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf'' : ∀ x ∈ interior D, 0 < (deriv^[2] f) x) : StrictConvexOn ℝ D f :=
((strictMonoOn_of_deriv_pos hD.interior fun z hz =>
(differentiableAt_of_deriv_ne_zero (hf'' z hz).ne').differentiableWithinAt.continuousWithinAt) <|
by rwa [interior_interior]).strictConvexOn_of_deriv
hD hf
