Theorems · Theorem · real analysis

AntitoneOn.concaveOn_of_deriv

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

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

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

2 results in Mathlib

Foundations

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