Real_Function_Convex_iff_Derivative_Increasing
Provedanalysisconvex-functionsderivativesproofwiki
A differentiable function on (a,b) is convex iff its derivative is increasing.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue theorem Real_Function_Convex_iff_Derivative_Increasing (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) : ConvexOn ℝ (Set.Ioo a b) f ↔ MonotoneOn (deriv f) (Set.Ioo a b) := by sorry
Source