English
Under differentiability at y, the left derivative at x is bounded above by the right derivative at x.
Русский
При дифференцируемости в y левая производная не превосходит правую производную в x.
LaTeX
$$$$ \ derivWithin\ f(Iio x) x \le \ derivWithin\ f(Ioi x) x $$$$
Lean4
/-- If `f : ℝ → ℝ` is convex on `S` and differentiable within `S` at `y`, then the slope of any
secant line with right endpoint at `y` is bounded above by the derivative of `f` within `S` at `y`.
This is fractionally weaker than `ConvexOn.slope_le_of_hasDerivWithinAt_Iio` but simpler to apply
under a `DifferentiableOn S` hypothesis. -/
theorem slope_le_of_hasDerivWithinAt (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hf' : HasDerivWithinAt f f' S y) : slope f x y ≤ f' :=
hfc.slope_le_of_hasDerivWithinAt_Iio hx hy hxy <|
hf'.mono_of_mem_nhdsWithin <| hfc.1.ordConnected.mem_nhdsLT hx hy hxy
