slope_lt_of_hasDerivAt — Mathlib

English

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

Русский

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

LaTeX

$$$\text{If } x

Lean4

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

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