monotoneOn_derivWithin — Mathlib

English

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

Русский

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

LaTeX

$$$$ \ MonotoneOn\ (\ deriv f)\ S $$$$

Lean4

/-- If `f` is convex on `S` and differentiable on `S`, then its derivative within `S` is monotone
on `S`. -/
theorem monotoneOn_derivWithin (hfc : ConvexOn ℝ S f) (hfd : DifferentiableOn ℝ f S) : MonotoneOn (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 x hx)).trans (hfc.slope_le_derivWithin hx hy hxy' (hfd y hy))

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