CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

The Grönwall estimate for two solutions of a Lipschitz ODE

Statement

Let $F : D \to R^{n}$ be continuous on an open ODE domain, let $I \subseteq R$ be an order-convex interval with at least two elements, and let $x, y : I \to R^{n}$ solve $z^{'} = F (t, z)$ with both graphs in $D$ . Fix $t_{0} \in I$ , and suppose that for every $t \in I$ ,

$∥ F (t, x (t)) - F (t, y (t)) ∥_{2} \leq L ∥ x (t) - y (t) ∥_{2} .$

Then

$∥ x (t) - y (t) ∥_{2} \leq e^{L ∣ t - t_{0} ∣} ∥ x (t_{0}) - y (t_{0}) ∥_{2} .$

Coincident initial values give uniqueness on every common interval.

Facts & Assumptions

Given: The two solutions and common state-Lipschitz constant in the Statement.

[L1]

For a continuous field on an open ODE domain and an order-convex interval with at least two elements, a curve solves the IVP if and only if it satisfies the associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).

[L2]

If a continuous nonnegative function $u$ satisfies $u (t) \leq A + \int_{t_{0}}^{t} L u (s) d s$ with constants $A, L \geq 0$ , then $u (t) \leq A e^{L (t - t_{0})}$ ; the reflected statement holds to the left of $t_{0}$ (Gronwall's integral inequality with variable and constant coefficients).

[L3]

For increasing limits the norm of a vector integral is at most the integral of the Euclidean norm, and for reversed limits the oriented form has the absolute value of that scalar integral (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable).

[L4]

If integrable real functions $p \leq q$ on a compact 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)$ ).

Proof

technique · direct

1.1

Subtracting the two equations from [L1], applying [L3], and integrating the stated pairwise Lipschitz inequality with [L4] on the compact interval between $t_{0}$ and $t$ gives $∥ x (t) - y (t) ∥_{2} \leq ∥ x (t_{0}) - y (t_{0}) ∥_{2} + L ∣ \int_{t_{0}}^{t} ∥ x (s) - y (s) ∥_{2} d s ∣$ .

givenL1L3L4

2.1

Applying [L2] in the relevant time orientation gives the displayed estimate; at $t = t_{0}$ it is equality, for $L = 0$ it is constant, and a zero initial difference forces equality of the solutions.

step 1.1L2algebra∎

Depends on

Used by

Locally unique ODE solutions agree on overlaps and glue across a common endpoint Lemma

Dependency tree · two levels

43 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)