補題(拡張されたGronwall の不等式の系１)
I = [a, b) を実数体における区間とする(-∞ ＜ a ＜ b ≦ +∞)。
α(t) と β(t) と f(t) を I で連続な実数値関数で
I の各点 t で β(t) ≧ 0 かつ
f(t) ≦ α(t) + ∫[a, t] β(s)f(s) ds とする。

さらに α(t) は I において単調増加とする。
即ち、t_1, t_2 ∈ I で t_1 ≦ t_2 のとき α(t_1) ≦ α(t_2) とする。

このとき、I の各点 t で
f(t) ≦ α(t)exp(∫[a, t] β(s) ds)

証明
>>588より、
f(t) ≦ α(t) + ∫[a, t]α(s)β(s)exp(∫[s, t] β(r) dr)ds

α(t) は I において単調増加であり、I の各点 s で β(s) ≧ 0 であるから
f(t) ≦ α(t) + α(t)∫[a, t]β(s)exp(∫[s, t] β(r) dr)ds

ψ(s) = -exp(-∫[t, s] β(r) dr) を s で微分すると
dψ/ds = β(s)exp(-∫[t, s] β(r) dr) = β(s)exp(∫[s, t] β(r) dr)

よって、
∫[a, t]β(s)exp(∫[s, t] β(r) dr)ds = ∫[a, t] dψ/ds ds
= ψ(t) - ψ(a) = -1 + exp(-∫[t, a] β(r) dr)

よって、
f(t) ≦ α(t) + α(t)(-1 + exp(-∫[t, a] β(r) dr)) = α(t)exp(∫[a, t] β(s) ds)
証明終