Theorems · Theorem · real analysis

strictConcaveOn_of_deriv2_neg

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

If a function f is continuous on a convex set D ⊆ ℝ and f'' is strictly negative on the interior, then f is strictly concave on D. Note that we don't require twice differentiability explicitly as it already implied by the second derivative being strictly negative, except at at most one point.

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

4 results in Mathlib

Foundations

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