TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Gronwall's integral inequality with variable and constant coefficients

Statement

Let $t_{0} \leq T$ , let $u, a, b : [t_{0}, T] \to R$ be continuous, with $u, b \geq 0$ , and suppose

$u (t) \leq a (t) + \int_{t_{0}}^{t} b (s) u (s) d s .$

Then

$u (t) \leq a (t) + \int_{t_{0}}^{t} a (s) b (s) \exp ⁣ (\int_{s}^{t} b (r) d r) d s .$

If $a$ is nondecreasing, this gives $u (t) \leq a (t) \exp (\int_{t_{0}}^{t} b)$ . The time-reflected form assumes $u (t) \leq a (t) + \int_{t}^{t_{0}} b (s) u (s) d s$ for $t \leq t_{0}$ . In particular, when $a = A \geq 0$ and $b = B \geq 0$ are constant, the two orientations give $u (t) \leq A e^{B ∣ t - t_{0} ∣}$ .

Facts & Assumptions

Given: The continuous functions and integral inequality in the Statement.

[L1]

The exponential is differentiable and $(\exp)^{'} = \exp$ (The exponential function is smooth and $(\exp)^{'} = \exp$ ).

[L2]

For every real $x$ , $\exp (x) > 0$ (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

[L3]

The chain rule gives $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ under its differentiability hypotheses (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)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[L4]

The product rule gives $(f g)^{'} = f^{'} g + f g^{'}$ (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L5]

An integrable derivative satisfies $\int_{a}^{b} G^{'} = G (b) - G (a)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[L6]

If integrable $p \leq q$ on an interval, then $\int p \leq \int q$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L7]

If $g$ is continuous on a nondegenerate compact interval, then its integral function is differentiable there with derivative $g$ , including domain-relative endpoint derivatives (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

Proof

technique · direct

1.1givenL1L3L4L7

If $T = t_{0}$ , every displayed integral is zero and the conclusion is immediate. Assume $t_{0} < T$ , and put $v (t) = \int_{t_{0}}^{t} b (s) u (s) d s$ and $B (t) = \int_{t_{0}}^{t} b (s) d s$ ; [L7] gives $v^{'} = b u$ and $B^{'} = b$ , after which [L3], [L4], and [L1] give $(e^{- B} v)^{'} = e^{- B} b (u - v) \leq e^{- B} b a$ .

2.1step 1.1L1L2L3L5L6algebra∎

Apply [L6] and [L5] to integrate the inequality, use $v (t_{0}) = 0$ , and divide by the positive factor from [L2]; this gives the displayed formula. If $a$ is nondecreasing, $a (s) \leq a (t)$ and direct integration of the exponential derivative gives the stated simplification. Replacing time by $- t$ proves the reflected form with $\int_{t}^{t_{0}}$ , and $b = 0$ gives $u \leq a$ .

Depends on

Used by

Dependency tree · two levels

49 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Gerald Teschl, Ordinary Differential Equations and Dynamical Systems, Ch. 2 (standard reference, not scraped)
Jiri Lebl, Basic Analysis I, Section 6.3 (standard reference, not scraped)