Theorems · Theorem · real analysis

StrictAntiOn.strictConcaveOn_of_deriv

∀ {D : Set ℝ},
  Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → StrictAntiOn (deriv f) (interior D) → StrictConcaveOn ℝ D f

If a function f is continuous on a convex set D ⊆ ℝ and f' is strictly antitone on the interior, then f is strictly concave on D. Note that we don't require differentiability, since it is guaranteed at all but at most one point by the strict antitonicity of f'.

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

2 results in Mathlib

Foundations

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