English
Under the same hypothesis as above, if f is differentiable from the right at x (i.e., has a right-hand derivative at x), then the right-hand derivative is strictly less than the secant slope from x to y.
Русский
При тех же предпосылках, если f имеет правая производная в точке x, то правая производнаяStrict меньше наклона секантной прямой между x и y.
LaTeX
$$$\text{If } f \text{ is strictly convex on } S \text{ and differentiable from the right at } x, \text{ then } f' < \frac{f(y)-f(x)}{y-x}. $$$
Lean4
theorem rightDeriv_lt_slope (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hfd : DifferentiableWithinAt ℝ f (Ioi x) x) : derivWithin f (Ioi x) x < slope f x y :=
hfc.lt_slope_of_hasDerivWithinAt_Ioi hx hy hxy hfd.hasDerivWithinAt
