slope_le_of_hasDerivAt — Mathlib

English

Under differentiability on Iio y, slope ≤ leftDeriv at y.

Русский

При дифференцируемости на Iio y наклон ≤ левая производная в y.

LaTeX

$$$$ \ slope f x y \le \ derivWithin f(Iio y) y $$$$

Lean4

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

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