slope_le_of_hasDerivAt — Mathlib

English

If f is concave on S and differentiable within (−∞, y) at y, then the left derivative at y is at least the slope from x to y.

Русский

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

LaTeX

$$$\text{If } x

Lean4

theorem slope_le_of_hasDerivAt (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hf' : HasDerivAt f f' x) : slope f x y ≤ f' :=
  hfc.slope_le_of_hasDerivWithinAt_Ioi hx hy hxy hf'.hasDerivWithinAt

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