slope_le_deriv — Mathlib

English

For a concave function on S, the secant slope from x to y is bounded above by the derivative at x (or left/right derivatives) depending on the direction of approach.

Русский

Для вогнутой функции на S секантный наклон между x и y ограничен сверху производной в x (или левой/правой производной) в зависимости от направления подхода.

LaTeX

$$$\text{If } f \text{ is concave on } S,\; x

Lean4

theorem slope_le_deriv (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f x) :
    slope f x y ≤ deriv f x :=
  hfc.slope_le_of_hasDerivAt hx hy hxy hfd.hasDerivAt

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