English
If f is twice differentiable on a convex set D and f'' is nonnegative on D, then f is convex on D.
Русский
Пусть на выпуклом D функция f дважды дифференцируема, и 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 an open convex set `D ⊆ ℝ` and
`f''` is nonnegative on `D`, then `f` is convex on `D`. -/
theorem convexOn_of_deriv2_nonneg' {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf' : DifferentiableOn ℝ f D)
(hf'' : DifferentiableOn ℝ (deriv f) D) (hf''_nonneg : ∀ x ∈ D, 0 ≤ (deriv^[2] f) x) : ConvexOn ℝ D f :=
convexOn_of_deriv2_nonneg hD hf'.continuousOn (hf'.mono interior_subset) (hf''.mono interior_subset) fun x hx =>
hf''_nonneg x (interior_subset hx)
