English
If the norm of the derivative of f is controlled by a boundary function B', then the norm of logDeriv f is controlled by that boundary via the mean value principle.
Русский
Если норма производной функция f ограничена границей B', тогда норма logDeriv f ограничена этой границей через принцип среднего значения.
LaTeX
$$$\displaystyle \|\logDeriv f(x)\| \le B'(x) \quad\text{for all } x\in[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` and `B` have right derivatives `f'` and `B'` respectively at every point of `[a, b)`;
* 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 : 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 → ‖f' x‖ < B' x) : ∀ ⦃x⦄, x ∈ Icc a b → ‖f x‖ ≤ B x :=
image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary hf
(fun x hx _ hr => (hf' x hx).liminf_right_slope_norm_le hr) ha hB hB' bound
