slope_le_rightDeriv — Mathlib

English

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

Русский

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

LaTeX

$$$\text{If } x

Lean4

theorem slope_le_rightDeriv (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : DifferentiableWithinAt ℝ f (Ioi x) x) : slope f x y ≤ derivWithin f (Ioi x) x :=
  hfc.slope_le_of_hasDerivWithinAt_Ioi hx hy hxy hfd.hasDerivWithinAt

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