English
Let f: R → R be differentiable and assume that its derivative is bounded above by a constant C, i.e. f'(x) ≤ C for every x ∈ R. Then for all real x ≤ y, the increment of f is bounded by C times the increment of the argument: f(y) − f(x) ≤ C (y − x). In particular, f is globally Lipschitz with Lipschitz constant C on R.
Русский
Пусть f: R → R дифференцируема и производная удовлетворяет ограничению сверху f'(x) ≤ C для всех x ∈ R. Тогда для любых x ≤ y имеем f(y) − f(x) ≤ C (y − x). Тогда f является глобально Л Lipschitz с константой Lipschitz C на R.
LaTeX
$$$\exists C \in \mathbb{R}, \; \forall x,y \in \mathbb{R}, \; x \le y \Rightarrow f(y) - f(x) \le C\,(y - x) \\ \text{where } \forall x \in \mathbb{R}, \; \ deriv f x \le C$$$
Lean4
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f' ≤ C`, then `f` grows at most as fast
as `C * x`, i.e., `f y - f x ≤ C * (y - x)` whenever `x ≤ y`. -/
theorem image_sub_le_mul_sub_of_deriv_le {f : ℝ → ℝ} (hf : Differentiable ℝ f) {C} (le_hf' : ∀ x, deriv f x ≤ C) ⦃x y⦄
(hxy : x ≤ y) : f y - f x ≤ C * (y - x) :=
convex_univ.image_sub_le_mul_sub_of_deriv_le hf.continuous.continuousOn hf.differentiableOn (fun x _ => le_hf' x) x
trivial y trivial hxy
