lt_slope_of_hasDerivAt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable at `x ∈ S`, then the slope of any
secant line with left endpoint at `x` is strictly greater than the derivative of `f` at `x`. -/
theorem lt_slope_of_hasDerivAt (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hf' : HasDerivAt f f' x) : f' < slope f x y :=
  hfc.lt_slope_of_hasDerivWithinAt_Ioi hx hy hxy hf'.hasDerivWithinAt

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