Gronwall不等式是目前常用不等式之一。它与Holder不等式一样，分别具备离散形式与连续形式。
在数学中，格朗沃尔 引理 或格朗沃尔不等式说明了对于满足一定的 微分方程 或积分方程的函数，有相应的关于此微分方程或积分方程的不等式。格朗沃尔不等式有两种形式，分别是积分形式和 微分形式 。积分形式下的不等式可以有几种不同的写法。
释义
格朗沃尔不等式常常被用来估计 常微分方程 的解的取值范围。比如，它可以用来证明初值问题的解的唯一性（见柯西-利普希茨定理）。
格朗沃尔不等式的名称来自多玛·哈肯·格朗沃尔。格朗沃尔是一位 瑞典 的数学家，后来移居 美国 。
格朗沃尔不等式的微分形式首先由格朗沃尔在1919年证明。而积分形式则是由 理查德·贝尔曼 （Richard Bellman）在1943年证明。
离散形式
设 是非负 实数 列， 。如果对每一个 ，
,
那么
连续形式
设 是定义在 上的连续实函数， 。如果对一切 ，都有
那么
微分形式
设 I 是一个 实数 区间，记为： 或 或 ，其中 。又设 β 和 u 为定义在 I 上的 实数 值的 连续函数 。假设 u 是一个在 I 的内部（也就是不包括端点）可微的函数，并且满足如下的 导数 不等式：
那么对于所有的 ，函数 u 都小于等于以下 微分方程 的解：
注意：不等式对函数 β 和 u 的符号没有任何要求。
证明
如果设
是以下微分方程
其中 的解，那么对所有的 t 都有 ，因此根据复合函数求导法则中的除法定则：
对所有的 成立，因此
于是格朗沃尔不等式得证。
积分形式
设 I 是一个 实数 区间，记为： 或 或 ，其中 。又设 α 、 β 和 u 为定义在 I 上的实数值的函数。假设 β 和 u 是连续的，则有：
(a) 如果 β 是非负函数并且 u 满足如下的积分不等式：
，
那么
。
(b) 如果在之前的条件下， α 还是一个 常数 ，那么
注意：
不等式的成立条件里并没有限制 α 和 u 的符号；
相比于 微分形式 ，积分形式中对函数 u 的可微性没有做要求。
证明
(a) 定义
则运用复合函数求导法则中的乘积法则、链式法则、 指数函数 的求导法则以及微积分基本定理，可以得到：
由于注意到括号中的部分小于 α ，可以得到相应的不等式，并进行积分。由于函数 β 以及其指数都是非负函数，积分后不等号保持不变。然而 ，因此积分式等价于：
再运用第一步里 v ( t ) 的定义，就得到：
最后将原来条件里的不等式带入上式左边，就可以得到格朗沃尔不等式了。
(b) 如果函数 α 为常数函数，那么命题 (a) 中不等式的右边可以进行积分。由微积分基本定理可以获得：