slope_le_deriv — Mathlib

English

If f is convex on S and has a HasDerivWithinAt at x with respect to S, then slope ≤ f′(x) to y.

Русский

Если f выпукла на S и имеет HasDerivWithinAt в x относительно S, то наклон ≤ производная в x.

LaTeX

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

Lean4

/-- Reformulation of `ConvexOn.slope_le_of_hasDerivAt` using `deriv`. -/
theorem slope_le_deriv (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f y) :
    slope f x y ≤ deriv f y :=
  hfc.slope_le_of_hasDerivAt hx hy hxy hfd.hasDerivAt

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