image_sub_lt_mul_sub_of_deriv_lt — Mathlib

English

If f is differentiable and f′(x) < C for all x in D°, then f(y)−f(x) < C(y−x) for x<y in D.

Русский

Если f дифференцируема и f′(x) < C на D°, то f(y)−f(x) < C(y−x) при x<y в D.

LaTeX

$$$\\forall x

Lean4

/-- Let `f : ℝ → ℝ` be a differentiable function. If `f' < C`, then `f` grows slower than
`C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x < y`. -/
theorem image_sub_lt_mul_sub_of_deriv_lt {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C} (lt_hf' : ∀ x, deriv f x < C) ⦃x y⦄
    (hxy : x < y) : f y - f x < C * (y - x) :=
  convex_univ.image_sub_lt_mul_sub_of_deriv_lt hf.continuous.continuousOn hf.differentiableOn (fun x _ => lt_hf' x) x
    trivial y trivial hxy

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