English
If two continuous functions on an interval have the same right-hand derivative and share the same value at the left endpoint, then they are identical on the entire interval.
Русский
Если две непрерывные функции на интервале имеют одинаковую правую производную и равны в левой границе, то они совпадают на всём интервале.
LaTeX
$$$\displaystyle \text{If }f,g\text{ have the same right-derivative and } f(a)=g(a),\; f\equiv g\text{ on }[a,b].$$$
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` has right derivative `f'` at every point of `[a, b)`;
* `B` has derivative `B'` everywhere on `ℝ`;
* the norm of `f'` is strictly less than `B'` whenever `‖f x‖ = B x`.
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_lt_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 : ∀ x, HasDerivAt B (B' x) x) (bound : ∀ x ∈ Ico a b, ‖f x‖ = B x → ‖f' x‖ < B' x) :
∀ ⦃x⦄, x ∈ Icc a b → ‖f x‖ ≤ B x :=
image_norm_le_of_norm_deriv_right_lt_deriv_boundary' hf hf' ha (fun x _ => (hB x).continuousAt.continuousWithinAt)
(fun x _ => (hB x).hasDerivWithinAt) bound
