strictMonoOn_derivWithin — Mathlib

English

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

Русский

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

LaTeX

$$$\text{If } f \text{ is convex on } S \text{ and differentiable on } S, \text{ then } x \mapsto \ derivWithin f S(x) \text{ is strictly monotone on } S.$$$

Lean4

/-- If `f` is convex on `S` and differentiable on `S`, then its derivative within `S` is monotone
on `S`. -/
theorem strictMonoOn_derivWithin (hfc : StrictConvexOn ℝ S f) (hfd : DifferentiableOn ℝ f S) :
    StrictMonoOn (derivWithin f S) S := by
  intro x hx y hy hxy
  exact (hfc.derivWithin_lt_slope hx hy hxy (hfd x hx)).trans (hfc.slope_lt_derivWithin hx hy hxy (hfd y hy))

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