deriv_lt_slope — Mathlib

English

If f is strictly convex on S and differentiable at x, then the derivative f' at x is strictly less than the secant slope from x to y for x<y in S.

Русский

Если f строго выпукла на S и дифференцируема в x, то производная в x строго меньше наклона секантной прямой между x и y, когда x<y и x,y ∈ S.

LaTeX

$$$\text{If } f \text{ is strictly convex on } S \text{ and } \text{ differentiable at } x,\; x

Lean4

theorem deriv_lt_slope (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : DifferentiableAt ℝ f x) : deriv f x < slope f x y :=
  hfc.lt_slope_of_hasDerivAt hx hy hxy hfd.hasDerivAt

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