slope_le_of_hasDerivWithinAt — Mathlib

English

If f is concave on S and differentiable on an interval to the right of x, then the secant slope is bounded above by the right derivative at x.

Русский

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

LaTeX

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

Lean4

theorem slope_le_of_hasDerivWithinAt (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : HasDerivWithinAt f f' S x) : slope f x y ≤ f' :=
  hfc.slope_le_of_hasDerivWithinAt_Ioi hx hy hxy <|
    hfd.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsGT hx hy hxy

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