English
If the norm of the log-derivative is bounded by B on [a,b], then the log-derivative remains controlled by B across the interval.
Русский
Если норма логарифмической производной ограничена сверху B на [a,b], то логарифмическая производная остается в рамках B по всём интервалу.
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` has right derivative `f'` at every point of `[a, b)`;
* `B` has derivative `B'` everywhere on `ℝ`;
* 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 : ∀ x, HasDerivAt B (B' x) x) (bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ B' x) : ∀ ⦃x⦄, x ∈ Icc a b → ‖f x‖ ≤ B x :=
image_norm_le_of_norm_deriv_right_le_deriv_boundary' hf hf' ha (fun x _ => (hB x).continuousAt.continuousWithinAt)
(fun x _ => (hB x).hasDerivWithinAt) bound
