Theorems · Theorem · real analysis

MonotoneOn.convexOn_of_deriv

∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D → DifferentiableOn ℝ f (interior D) → MonotoneOn (deriv f) (interior D) → ConvexOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ, is differentiable on its interior, and f' is monotone on the interior, then f is convex on D.

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

4 results in Mathlib

Foundations

Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound