slope_lt_of_hasDerivWithinAt — Mathlib

English

If f is strictly convex on S and differentiable within S at y, then the slope from x to y is strictly less than the derivative of f within S at y.

Русский

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

LaTeX

$$$\text{If } x

Lean4

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

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

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