English
If the derivative of f is bounded in norm by C on [a,b], then the norm of f(x) − f(a) is bounded by C(x − a).
Русский
Если норма производной функции f ограничена сверху C на [a,b], то норма f(x)−f(a) ≤ C(x−a).
LaTeX
$$$\displaystyle \|f(x) - f(a)\| \le C\,(x - a) \quad \text{for all } x \in [a,b],$ given HasDerivWithinAt bounds.$$
Lean4
/-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that
* `‖f a‖ ≤ B a`;
* `f` and `B` have right derivatives `f'` and `B'` respectively at every point of `[a, b)`;
* we have `‖f' x‖ ≤ B x` everywhere on `[a, b)`.
Then `‖f x‖ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
to make this theorem work for piecewise differentiable functions.
-/
theorem image_norm_le_of_norm_deriv_right_le_deriv_boundary' {f' : ℝ → E} (hf : ContinuousOn f (Icc a b))
(hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x) {B B' : ℝ → ℝ} (ha : ‖f a‖ ≤ B a)
(hB : ContinuousOn B (Icc a b)) (hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x)
(bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ B' x) : ∀ ⦃x⦄, x ∈ Icc a b → ‖f x‖ ≤ B x :=
image_le_of_liminf_slope_right_le_deriv_boundary (continuous_norm.comp_continuousOn hf) ha hB hB' fun x hx _ hr =>
(hf' x hx).liminf_right_slope_norm_le ((bound x hx).trans_lt hr)
