le_slope_of_hasDerivWithinAt_Iio — Mathlib

English

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

Русский

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

LaTeX

$$$\text{If } x

Lean4

theorem le_slope_of_hasDerivWithinAt_Iio (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hf' : HasDerivWithinAt f f' (Iio y) y) : f' ≤ slope f x y := by
  simpa only [neg_neg, Pi.neg_def, slope_neg] using
    neg_le_neg (hfc.neg.slope_le_of_hasDerivWithinAt_Iio hx hy hxy hf'.neg)

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