Grönwall inequality with an integrable coefficient

Given: The interval, nonnegative number $A$, continuous nonnegative function $u$, measurable nonnegative integrable coefficient $\mathrm{\ell }$, and one of the integral inequalities in the Statement.

Assume Countable Choice and Dependent Choice for the library fundamental theorem of calculus for absolutely continuous functions. The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$), The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain

A measurable function with finite integral of its absolute value represents an $L^1$ function; here $\mathrm{\ell }\in L^1[a,b]$. The class $L^1(\mu )$ of integrable functions

The indefinite integral of an $L^1$ function is absolutely continuous. The indefinite integral of an $L^1$ function is absolutely continuous

Under [A1], every absolutely continuous function is the integral of its almost-everywhere derivative, and that derivative is integrable. Fundamental theorem of calculus for absolutely continuous functions

If an absolutely continuous function is followed by a Lipschitz function on its image, the composition is absolutely continuous. A Lipschitz function after an absolutely continuous function is absolutely continuous

The product of absolutely continuous functions is absolutely continuous. The product of two absolutely continuous functions is absolutely continuous

The exponential has derivative $e^r$; the mean-value theorem therefore makes $r\mapsto e^{-r}$ Lipschitz on every compact interval. The exponential function is smooth and $(\exp {)}^{\mathrm{\prime }}=\exp$, Mean value theorem on a closed real interval

At a point where the inner and outer derivatives exist, the ordinary chain rule gives the derivative of their composition; the product rule gives the derivative of a product. The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f\circ g$ is differentiable at $c$ with $(f\circ g{)}^{\mathrm{\prime }}(c)=f^{\mathrm{\prime }}(g(c))g^{\mathrm{\prime }}(c)$, Sum, product, quotient, and chain rules from difference quotients

When $a<b$, reflection on $(a,b)$ is a $C^1$ diffeomorphism, so substitution preserves Lebesgue integrals of $L^1$ functions; the endpoints have measure zero. A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions

For $g\in L^1[a,b]$, its indefinite integral $x\mapsto {\int }_a^{x}g(s)ds$ is differentiable almost everywhere with derivative $g$. The indefinite integral of an $L^1$ function is differentiable almost everywhere