derivWithin_le_slope — Mathlib

English

Under convexity on S, the derivative within S at x is bounded above by the slope between x and y.

Русский

При выпуклости на S производная внутри S в x не превосходит наклон между x и y.

LaTeX

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

Lean4

/-- Reformulation of `ConvexOn.le_slope_of_hasDerivWithinAt` using `derivWithin`. -/
theorem derivWithin_le_slope (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : DifferentiableWithinAt ℝ f S x) : derivWithin f S x ≤ slope f x y :=
  le_slope_of_hasDerivWithinAt hfc hx hy hxy hfd.hasDerivWithinAt

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