English
If f is twice differentiable on an open convex set D and f'' is nonnegative on D, then f is 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{DifferentiableOn}(f, D) \\Rightarrow \\text{DifferentiableOn}(\\mathrm{deriv}\,f, D) \\Rightarrow (\\forall x\\in D, 0 \\le (\\mathrm{deriv}^{[2]} f)(x)) \\Rightarrow \\text{ConvexOn}(\\mathbb{R}, D, f).$$
Lean4
/-- If a function `f` is twice differentiable on `ℝ`, and `f''` is nonnegative on `ℝ`,
then `f` is convex on `ℝ`. -/
theorem convexOn_univ_of_deriv2_nonneg {f : ℝ → ℝ} (hf' : Differentiable ℝ f) (hf'' : Differentiable ℝ (deriv f))
(hf''_nonneg : ∀ x, 0 ≤ (deriv^[2] f) x) : ConvexOn ℝ univ f :=
convexOn_of_deriv2_nonneg' convex_univ hf'.differentiableOn hf''.differentiableOn fun x _ => hf''_nonneg x
