English
If f is concave on S and differentiable on S, then the derivative within f on S is antitone on S; i.e., for any x,y ∈ S with x ≤ y, we have derivWithin f S x ≥ derivWithin f S y.
Русский
Пусть f выпукло-вогнута на S и дифференцируема на S. Тогда производная derivWithin f S на S антимонотонна; то есть для любых x,y ∈ S с x ≤ y верно derivWithin f S x ≥ derivWithin f S y.
LaTeX
$$$\text{Concave on } S \land \text{Differentiable on } S \Rightarrow \operatorname{AntitoneOn}(\operatorname{derivWithin} f\, S)\, S.$$$
Lean4
theorem antitoneOn_derivWithin (hfc : ConcaveOn ℝ S f) (hfd : DifferentiableOn ℝ f S) :
AntitoneOn (derivWithin f S) S := by
intro x hx y hy hxy
rcases eq_or_lt_of_le hxy with rfl | hxy'
· rfl
exact (hfc.derivWithin_le_slope hx hy hxy' (hfd y hy)).trans (hfc.slope_le_derivWithin hx hy hxy' (hfd x hx))
