English
If f is concave on S and differentiable at every point of S, then the derivative f' is antitone on S; i.e., f'(x) ≥ f'(y) for x < y in S.
Русский
Если f вогнута на S и дифференцируема на каждой точке S, то производная f' на S антимонотна; то есть f'(x) ≥ f'(y) для x < y в S.
LaTeX
$$$\text{ConcaveOn}(\mathbb{R}, S, f)\ \land\ (\forall x\in S,\ DifferentiableAt\ \mathbb{R}\ f\ x)\Rightarrow \operatorname{AntitoneOn}(\operatorname{deriv} f)\, S.$$$
Lean4
/-- If `f` is concave on `S` and differentiable at all points of `S`, then its derivative is
antitone (monotone decreasing) on `S`. -/
theorem antitoneOn_deriv (hfc : ConcaveOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) : AntitoneOn (deriv f) S := by
simpa using (hfc.neg.monotoneOn_deriv (fun x hx ↦ (hfd x hx).neg)).neg
