English
If a function f on [a,b] is continuous, its derivative bounds with a comparative function B and a slope condition, then f ≤ B throughout [a,b].
Русский
Если функция f непрерывна на [a,b], её производная ограничена по отношению к сопоставимой функции B и соблюдены условия касательных, тогда f ≤ B на всём [a,b].
LaTeX
$$$\displaystyle \forall x\in[a,b],\; f(x) \le B(x)$ under the prescribed differentiability and slope conditions.$$
Lean4
/-- General fencing theorem for continuous functions with an estimate on the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that
* `‖f a‖ ≤ B a`;
* `B` has right derivative at every point of `[a, b)`;
* for each `x ∈ [a, b)` the right-side limit inferior of `(‖f z‖ - ‖f x‖) / (z - x)`
is bounded above by a function `f'`;
* we have `f' x < B' x` whenever `‖f x‖ = B x`.
Then `‖f x‖ ≤ B x` everywhere on `[a, b]`. -/
theorem image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary {E : Type*} [NormedAddCommGroup E] {f : ℝ → E}
{f' : ℝ → ℝ}
(hf : ContinuousOn f (Icc a b))
-- `hf'` actually says `liminf (‖f z‖ - ‖f x‖) / (z - x) ≤ f' x`
(hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r → ∃ᶠ z in 𝓝[>] x, slope (norm ∘ f) x z < r) {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_le_of_liminf_slope_right_lt_deriv_boundary' (continuous_norm.comp_continuousOn hf) hf' ha hB hB' bound
