Theorems · Theorem · real analysis

StrictConvexOn.lt_slope_of_hasDerivWithinAt

∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' S x → f' < slope f x y

If f : ℝ → ℝ is strictly convex on S and differentiable within S at x ∈ S, then the slope of any secant line with left endpoint at x is strictly greater than the derivative of f within S at x. This is fractionally weaker than StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi but simpler to apply under a DifferentiableOn S hypothesis.

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

2 results in Mathlib

Foundations

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