Theorems · Theorem · real analysis

concaveOn_of_deriv2_nonpos

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

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

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

2 results in Mathlib

Foundations

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