English
If f is strictly convex on S and differentiable on S, then its derivative is strictly monotone on S.
Русский
Если f строго выпукла на S и дифференцируема на S, то её производная строго монотонна на S.
LaTeX
$$$\text{If } f \text{ is strictly convex on } S \text{ and differentiable on } S, \; \text{then } x \mapsto f'(x) \text{ is strictly monotone on } S.$$$
Lean4
/-- If `f` is convex on `S` and differentiable at all points of `S`, then its derivative is monotone
on `S`. -/
theorem strictMonoOn_deriv (hfc : StrictConvexOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) :
StrictMonoOn (deriv f) S := by
intro x hx y hy hxy
exact (hfc.deriv_lt_slope hx hy hxy (hfd x hx)).trans (hfc.slope_lt_deriv hx hy hxy (hfd y hy))
