English
If f is differentiable on [a,b], and the derivative within the segment is bounded by C, then the norm of the increment is at most C over the segment.
Русский
Если f дифференцируема на [a,b] и производная в сегменте ограничена C, тогда приращение нормы не превышает C на отрезке.
LaTeX
$$$\displaystyle \|f(x) - f(a)\| \le C\,(x-a)\quad\text{for all } x\in[a,b].$$$
Lean4
/-- A function on `[a, b]` with the norm of the derivative within `[a, b]`
bounded by `C` satisfies `‖f x - f a‖ ≤ C * (x - a)`, `derivWithin`
version. -/
theorem norm_image_sub_le_of_norm_deriv_le_segment {C : ℝ} (hf : DifferentiableOn ℝ f (Icc a b))
(bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C) : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a) :=
by
refine norm_image_sub_le_of_norm_deriv_le_segment' ?_ bound
exact fun x hx => (hf x hx).hasDerivWithinAt
