English
If f is convex on S and differentiable at x in S, then the derivative from the left bounds the slope to the right.
Русский
Если f выпукла на S и дифференцируема в x ∈ S, то производная слева ограничивает наклон к правой точке.
LaTeX
$$$$ f' \le \operatorname{slope}(f,x,y) $$$$
Lean4
/-- If `f : ℝ → ℝ` is convex on `S` and differentiable within `S` at `x`, then the slope of any
secant line with left endpoint at `x` is bounded below by the derivative of `f` within `S` at `x`.
This is fractionally weaker than `ConvexOn.le_slope_of_hasDerivWithinAt_Ioi` but simpler to apply
under a `DifferentiableOn S` hypothesis. -/
theorem le_slope_of_hasDerivWithinAt (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hf' : HasDerivWithinAt f f' S x) : f' ≤ slope f x y :=
hfc.le_slope_of_hasDerivWithinAt_Ioi hx hy hxy <|
hf'.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsGT hx hy hxy
