mul_sub_le_image_sub_of_le_deriv — Mathlib

English

If f is differentiable and f′(x) ≤ C for all x, then f grows at most as fast as C x, i.e., f(y)−f(x) ≤ C(y−x) for x≤y.

Русский

Если f дифференцируема и f′(x) ≤ C для всех x, тогда f растет не быстрее, чем Cx: f(y)−f(x) ≤ C(y−x) для x≤y.

LaTeX

$$$\\forall x\\le y:\\; f(y)-f(x) \\le C(y-x)$$$

Lean4

/-- Let `f : ℝ → ℝ` be a differentiable function. If `C ≤ f'`, then `f` grows at least as fast
as `C * x`, i.e., `C * (y - x) ≤ f y - f x` whenever `x ≤ y`. -/
theorem mul_sub_le_image_sub_of_le_deriv {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C} (hf'_ge : ∀ x, C ≤ deriv f x) ⦃x y⦄
    (hxy : x ≤ y) : C * (y - x) ≤ f y - f x :=
  convex_univ.mul_sub_le_image_sub_of_le_deriv hf.continuous.continuousOn hf.differentiableOn (fun x _ => hf'_ge x) x
    trivial y trivial hxy

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