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

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

証明
s ∈ I に対して、
g(s) = exp(-∫[a, s] β(r) dr)∫[a, s] β(r)f(r) dr とおく。

dg/ds = -β(s)exp(-∫[a, s] β(r) dr)∫[a, s] β(r)f(r) dr
+ β(s)f(s)exp(-∫[a, s] β(r) dr)
= (f(s) - ∫[a, s] β(r)f(r) dr)β(s)exp(-∫[a, s] β(r) dr)

ここで、f(s) - ∫[a, s] β(r)f(r) dr ≦ α(s) で β(s) ≧ 0 だから
dg/ds ≦ α(s)β(s)exp(-∫[a, s] β(r) dr)

g(a) = 0 であるから両辺を [a, t] において積分すると
g(t) = ∫[a, t] dg/ds ds ≦ ∫[a, t] α(s)β(s)exp(-∫[a, s] β(r) dr) ds
g(t) = exp(-∫[a, t] β(r) dr)∫[a, t] β(r)f(r) dr であったから

∫[a, t] β(s)f(s) ds = exp(∫[a, t] β(r) dr)g(t)
≦ exp(∫[a, t] β(r) dr)∫[a, t] α(s)β(s)exp(-∫[a, s] β(r) dr) ds
= ∫[a, t] α(s)β(s)exp(∫[a, t] β(r) -∫[a, s] β(r) dr) ds
= ∫[a, t] α(s)β(s)exp(∫[s, t] β(r) dr) ds

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