Grönwall Bound on the Nonnegative Half-Line

This is a one-dimensional Grönwall inequality on $[0,\infty)$.

Let $E,E':\mathbb R\to\mathbb R$ and $c\in\mathbb R$. Assume:

1. $E$ is continuous on $[0,\infty)$.
2. For every $s>0$, $E$ has derivative $E'(s)$ at $s$.
3. For every $s>0$, $E'(s)\le cE(s)$.

Then, for every $t\ge0$,

This result is a reusable differential-inequality lemma for exponential semigroup estimates.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Semigroup.Generated. Shown in its original module context. Proof omitted.

theorem le_exp_mul_of_hasDerivAt_le {E E' : ℝ → ℝ} {c : ℝ} (hc : ContinuousOn E (Ici 0))
    (hd : ∀ s, 0 < s → HasDerivAt E (E' s) s) (hle : ∀ s, 0 < s → E' s ≤ c * E s) {t : ℝ}
    (ht : 0 ≤ t) :
    E t ≤ Real.exp (c * t) * E 0

Module navigation

Module: Analysis/Semigroup/Generated/Curvature.

Previous: hasDerivAt_inner_apply · Next: norm_map_apply_sq_le_exp_of_mem_adjointComp.

Source excerpt, lines 167–170 · Frozen source 408915f.