LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

A Gronwall bound for retarded-delay inequalities

Statement

Let $τ, T > 0$ , $L, H \geq 0$ , let $q : [0, T] \to [0, \infty)$ be continuous, and let $u : [- τ, T] \to [0, \infty)$ be continuous with $u (s) \leq H$ for $s \in [- τ, 0]$ . Suppose that $u (t) \leq H + \int_{0}^{t} (q (s) + L (u (s) + u (s - τ))) d s (0 \leq t \leq T) .$ Then, writing $U (t) = \max {H, \sup_{0 \leq r \leq t} u (r)}$ , one has $U (t) \leq (H + \int_{0}^{t} q (s) d s) e^{2 L t} (0 \leq t \leq T) .$

Facts & Assumptions

Given: The nonnegative continuous functions, constants, history bound, and integral inequality in the Statement.

[F1]

A continuous real function on a compact subset of $R$ is uniformly continuous (Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous).

[F2]

If continuous nonnegative $v, a, b$ satisfy $v (t) \leq a (t) + \int_{0}^{t} b (s) v (s) d s$ and $a$ is nondecreasing, then $v (t) \leq a (t) e^{\int_{0}^{t} b (s) d s}$ (Gronwall's integral inequality with variable and constant coefficients).

[F3]

A continuous real-valued function on a nonempty compact metric space is bounded (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

Proof

1.1givenF1F3

The running maximum $U$ is finite because [F3] bounds $u$ on the compact interval $[0, T]$ . It is continuous because [F1] gives a modulus of continuity: when $t$ increases by at most $δ$ , any newly included value of $u$ can exceed the old maximum by at most that modulus at $δ$ . Also $u (s) \leq U (s)$ and $u (s - τ) \leq U (s)$ for $s \geq 0$ : the latter is bounded by $H$ when $s - τ \leq 0$ , and otherwise its argument lies in $[0, s]$ .

2.1givenstep 1.1algebra

Put $A (t) = H + \int_{0}^{t} q (s) d s$ , which is continuous and nondecreasing. For each $r \in [0, t]$ , the assumed inequality and step 1.1 give $u (r) \leq A (r) + 2 L \int_{0}^{r} U (s) d s \leq A (t) + 2 L \int_{0}^{t} U (s) d s$ . Since the same upper bound is at least $H$ , taking the maximum over $r \in [0, t]$ yields $U (t) \leq A (t) + 2 L \int_{0}^{t} U (s) d s$ .

3.1F2step 2.1∎

Apply [F2] to step 2.1 with $v = U$ , $a = A$ , and the constant coefficient $b = 2 L$ . It gives $U (t) \leq A (t) e^{2 L t}$ , the required bound.

Depends on

Used by

Dependency tree · two levels

37 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

M. Zennaro, The Numerical Solution of Delay Differential Equations, Dobbiaco 2006 summer-school lecture notes (standard reference, not scraped)
Nicola Guglielmi and Ernst Hairer, Solving Delay Differential Equations, Chapter 1 (standard reference, not scraped)