Theorems · Theorem · real analysis

ConvexOn.le_slope_of_hasDerivAt

∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ}, ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivAt f f' x → f' ≤ slope f x y

If f : ℝ → ℝ is convex on S and differentiable at x ∈ S, then the slope of any secant line with left endpoint at x is bounded below by the derivative of f at x.

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

1 results in Mathlib

Foundations

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