slope_le_derivWithin — Mathlib

English

Under concavity, the slope from x to y is bounded above by the derivative at x from the right.

Русский

При вогнутости наклон секанты ограничен сверху производной справа в x.

LaTeX

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

Lean4

theorem slope_le_derivWithin (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : DifferentiableWithinAt ℝ f S x) : slope f x y ≤ derivWithin f S x :=
  hfc.slope_le_of_hasDerivWithinAt hx hy hxy hfd.hasDerivWithinAt

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