English
If f is differentiable and deriv f(x) ≤ C for all x in D, then the image difference is bounded by C times distance: f(y)−f(x) ≤ C(y−x) for x≤y.
Русский
Если производная f не превосходит C на D, то разность значений не более C умножить на расстояние: f(y)−f(x) ≤ C(y−x) для x≤y.
LaTeX
$$$\\forall x\\le y\\in D:\\; f(y)-f(x) \\le C(y-x)$$$
Lean4
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f' ≤ C`, then
`f` grows at most as fast as `C * x` on `D`, i.e., `f y - f x ≤ C * (y - x)` whenever `x, y ∈ D`,
`x ≤ y`. -/
theorem image_sub_le_mul_sub_of_deriv_le {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : DifferentiableOn ℝ f (interior D)) {C} (le_hf' : ∀ x ∈ interior D, deriv f x ≤ C) (x : ℝ) (hx : x ∈ D)
(y : ℝ) (hy : y ∈ D) (hxy : x ≤ y) : f y - f x ≤ C * (y - x) :=
have hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (fun y => -f y) x := fun x hx =>
by
rw [deriv.fun_neg, neg_le_neg_iff]
exact le_hf' x hx
by linarith [hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x hx y hy hxy]
