English
If f is differentiable on a convex set D and its first derivative is differentiable on D, with a strictly positive second derivative on D, then f is strictly convex on D.
Русский
Если f дифференцируема на выпуклом D и производная ф продолжена дифференцируемо на D, и второй производной положителна строго на D, то f строго выпукла на D.
LaTeX
$$$\\forall D \\subseteq \\mathbb{R},\\; \\text{Convex}(D) \\Rightarrow \\forall f:\\mathbb{R}\\to\\mathbb{R},\\; \\text{DifferentiableOn}(f, D) \\Rightarrow \\text{DifferentiableOn}(\\mathrm{deriv}\,f, D) \\Rightarrow (\\forall x\\in D, 0 < (\\mathrm{deriv}^{[2]} f)(x)) \\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 `D`,
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 ∈ D, 0 < (deriv^[2] f) x) : StrictConvexOn ℝ D f :=
strictConvexOn_of_deriv2_pos hD hf fun x hx => hf'' x (interior_subset hx)
