A short-interval estimate for actual differentiable trajectories. The proof uses the supremum norm and the mean value inequality, so the constant is two under the stated smallness condition.
theorem
EulerShortTimeLinearGrowth.norm_le_two
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(T L : ℝ)
(hL : 0 ≤ L)
(f f' : ℝ → E)
(hd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt f (f' t) (Set.Icc 0 T) t)
(hb : ∀ t ∈ Set.Icc 0 T, ‖f' t‖ ≤ L * ‖f t‖)
(hshort : L * T ≤ 1 / 2)
(s t : ↑(Set.Icc 0 T))
(hst : s ≤ t)
: