English
In the vector-valued setting, if f and f' are as in Grönwall with ‖f(a)‖ ≤ δ and ‖f'(x)‖ ≤ K‖f(x)‖ + ε, then ‖f(x)‖ ≤ gronwallBound(δ,K,ε,x−a).
Русский
Векторная версия: если ‖f(a)‖ ≤ δ и ‖f'(x)‖ ≤ K‖f(x)‖ + ε, тогда ‖f(x)‖ ≤ gronwallBound(δ,K,ε,x−a).
LaTeX
$$$\|f(x)\| \le \operatorname{gronwallBound}(\delta,K,\varepsilon,(x-a))$ for all x ∈ [a,b].$$
Lean4
/-- A Grönwall-like inequality: if `f : ℝ → E` is continuous on `[a, b]`, has right derivative
`f' x` at every point `x ∈ [a, b)`, and satisfies the inequalities `‖f a‖ ≤ δ`,
`∀ x ∈ [a, b), ‖f' x‖ ≤ K * ‖f x‖ + ε`, then `‖f x‖` is bounded by `gronwallBound δ K ε (x - a)`
on `[a, b]`. -/
theorem norm_le_gronwallBound_of_norm_deriv_right_le {f f' : ℝ → E} {δ K ε : ℝ} {a b : ℝ}
(hf : ContinuousOn f (Icc a b)) (hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x) (ha : ‖f a‖ ≤ δ)
(bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖ + ε) : ∀ x ∈ Icc a b, ‖f x‖ ≤ gronwallBound δ K ε (x - a) :=
le_gronwallBound_of_liminf_deriv_right_le (continuous_norm.comp_continuousOn hf)
(fun x hx _r hr => (hf' x hx).liminf_right_slope_norm_le hr) ha bound
