leftDeriv_le_slope — Mathlib

English

Let hfc be concave on S and f differentiable within Iio y. Then the left derivative at y bounds the slope from x to y.

Русский

Пусть hfc конкавна на S и f дифференцируема внутри Iio y. Тогда левая производная в y ограничивает наклон между x и y.

LaTeX

$$$\text{If } x

Lean4

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

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