English
If D is convex, f is continuous on D, differentiable on interior(D), and deriv f is differentiable on interior(D) with nonnegative second derivative on interior(D), then f is convex on D.
Русский
Если D выпукло, f непрерывна на D, дифференцируема в interior(D), а производная f дифференцируема на interior(D) с неотрицательной второй производной на interior(D), тогда f выпукла на D.
LaTeX
$$$$\\operatorname{ConvexOn}_{\\mathbb{R}} D f \\leftarrow \\operatorname{ContinuousOn} f D \\land \\operatorname{DifferentiableOn} f (\\operatorname{interior} D) \\land \\operatorname{DifferentiableOn} (\\operatorname{deriv} f) (\\operatorname{interior} D) \\land (\\forall x \\in \\operatorname{interior} D, 0 \\le \\operatorname{deriv}^2 f x)$$$$
Lean4
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
interior, and `f''` is nonnegative on the interior, then `f` is convex on `D`. -/
theorem convexOn_of_deriv2_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : DifferentiableOn ℝ f (interior D)) (hf'' : DifferentiableOn ℝ (deriv f) (interior D))
(hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x) : ConvexOn ℝ D f :=
(monotoneOn_of_deriv_nonneg hD.interior hf''.continuousOn (by rwa [interior_interior]) <| by
rwa [interior_interior]).convexOn_of_deriv
hD hf hf'
