le_slope_of_hasDerivAt — Mathlib

English

Reformulation of a slope inequality using derivWithin.

Русский

Переформулировка неравенства наклона с помощью derivWithin.

LaTeX

$$$$ \ derivWithin\ f\ S x \le \ slope\ f x y $$$$

Lean4

/-- If `f : ℝ → ℝ` is convex on `S` and differentiable at `x ∈ S`, then the slope of any secant
line with left endpoint at `x` is bounded below by the derivative of `f` at `x`. -/
theorem le_slope_of_hasDerivAt (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (ha : HasDerivAt f f' x) :
    f' ≤ slope f x y :=
  hfc.le_slope_of_hasDerivWithinAt_Ioi hx hy hxy ha.hasDerivWithinAt

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