Theorems · Theorem · real analysis

convexOn_of_deriv2_nonneg

∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D →
        DifferentiableOn ℝ f (interior D) →
          DifferentiableOn ℝ (deriv f) (interior D) → (∀ x ∈ interior D, 0 ≤ deriv^[2] f x) → ConvexOn ℝ D f

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.

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

2 results in Mathlib

Foundations

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