second derivative convexity

Stream: Is there code for X?

[Pietro Lavino]

is there theorem relating second derivatives and convexity of functions?

[Ruben Van de Velde]

Something like
strictConvexOn_univ_of_deriv2_pos Mathlib.Analysis.Convex.Deriv

∀ {f : ℝ → ℝ}, Continuous f → (∀ (x : ℝ), 0 < deriv^[2] f x) → StrictConvexOn ℝ Set.univ f

?

[Pietro Lavino]

yes thank you