English
Let f be concave on a set S ⊆ R. If x and y are in S with x < y and f is differentiable at y, then the derivative of f at y is bounded above by the slope of the secant line through (x, f(x)) and (y, f(y)); that is, f'(y) ≤ (f(y) − f(x)) / (y − x).
Русский
Пусть f выпукло-вогнута на множестве S ⊆ R. Пусть x, y ∈ S и x < y, и f дифференцируема в точке y. Тогда производная f в y не превосходит наклона секущей через (x, f(x)) и (y, f(y)); то есть f'(y) ≤ (f(y) − f(x)) / (y − x).
LaTeX
$$$\text{Concave on } S:\ \text{If } x \in S, y \in S, x < y, \ f \text{ differentiable at } y, \text{ then } f'(y) \le \frac{f(y) - f(x)}{y - x}.$$$
Lean4
theorem deriv_le_slope (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f y) :
deriv f y ≤ slope f x y :=
hfc.le_slope_of_hasDerivAt hx hy hxy hfd.hasDerivAt
