monotoneOn_deriv — Mathlib

English

If f is convex on S and differentiable on S, then derivWithin f S is monotone on S.

Русский

Если f выпукла на S и дифференцируема на S, то derivWithin f S монотонна на S.

LaTeX

$$$$ \ MonotoneOn\ (\ derivWithin\ f\ S)\ S $$$$

Lean4

/-- If `f` is convex on `S` and differentiable at all points of `S`, then its derivative is monotone
on `S`. -/
theorem monotoneOn_deriv (hfc : ConvexOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) : MonotoneOn (deriv f) S :=
  by
  intro x hx y hy hxy
  rcases eq_or_lt_of_le hxy with rfl | hxy'
  · rfl
  exact (hfc.deriv_le_slope hx hy hxy' (hfd x hx)).trans (hfc.slope_le_deriv hx hy hxy' (hfd y hy))

Похожие утверждения