le_slope_of_hasDerivWithinAt — Mathlib

English

If f is concave on S and differentiable on S, then the slope from x to y is bounded above by the derivative at x.

Русский

Если f вогнута на S и дифференцируема на S, наклон между x и y не превосходит производную в x.

LaTeX

$$$\text{If } f \text{ concave on } S \text{ and differentiable on } S,\; \text{slope}(f,x,y) \le f'(x).$$$

Lean4

theorem le_slope_of_hasDerivWithinAt (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hf' : HasDerivWithinAt f f' S y) : f' ≤ slope f x y :=
  hfc.le_slope_of_hasDerivWithinAt_Iio hx hy hxy <|
    hf'.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsLT hx hy hxy

Похожие утверждения