Theorems · Theorem · real analysis

ConvexOn.slope_le_of_hasDerivWithinAt_Iio

∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' (Set.Iio y) y → slope f x y ≤ f'

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

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

5 results in Mathlib

Foundations

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