lt_slope_of_hasDerivWithinAt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable within `S` at `x ∈ S`, then the
slope of any secant line with left endpoint at `x` is strictly greater than the derivative of `f`
within `S` at `x`.

This is fractionally weaker than `StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi` but simpler to
apply under a `DifferentiableOn S` hypothesis. -/
theorem lt_slope_of_hasDerivWithinAt (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hf' : HasDerivWithinAt f f' S x) : f' < slope f x y :=
  hfc.lt_slope_of_hasDerivWithinAt_Ioi hx hy hxy <|
    hf'.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsGT hx hy hxy

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