LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generated

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.

Error bound for piecewise-linear stored delay histories

Statement

Let $h = τ / m$ with integer $m \geq 1$ , and let the mesh nodes cover a finite interval containing $[- τ, T]$ , with every delay breakpoint $k τ$ a mesh node. Suppose $y$ is continuous and each restriction to a mesh cell is $C^{2}$ (with one-sided derivatives at its endpoints), with $M \geq 0$ and $∥ y^{''} (t) ∥_{2} \leq M$ on every cell interior. Let the stored nodal values $Y_{j}$ satisfy $∥ Y_{j} - y (t_{j}) ∥_{2} \leq E$ and let ${\hat{y}}_{h}$ be their piecewise-linear interpolant as in Explicit Euler with a stored piecewise-linear delay history. Then $\sup_{t} ∥ {\hat{y}}_{h} (t) - y (t) ∥_{2} \leq E + \frac{M h^{2}}{8} .$

Facts & Assumptions

Given: A grid-aligned piecewise $C^{2}$ vector path, its nodal approximations, and the piecewise-linear interpolant.

[F1]

The stored history is the linear interpolant of consecutive nodal values on every history and solution cell (Explicit Euler with a stored piecewise-linear delay history).

[F2]

If a vector function has integrable derivative, its increment is the integral of that derivative (If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz).

[F3]

The Euclidean norm of an integral is at most the integral of the Euclidean norm (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).

[F4]

The grid uses $h = τ / m$ , so every breakpoint $k τ$ is a mesh node (Explicit Euler with a stored piecewise-linear delay history).

[F5]

The Euclidean norm satisfies the triangle inequality (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

Proof

1.1givenF1F5algebra

Fix a cell $[a, b]$ of length $h$ and $t \in [a, b]$ . Set $λ = (t - a) / h$ and let $I_{h} y (t) = (1 - λ) y (a) + λ y (b)$ interpolate the exact endpoints. By [F1], ${\hat{y}}_{h} (t) = (1 - λ) Y_{a} + λ Y_{b}$ , so the nodal error bound and [F5] give $∥ {\hat{y}}_{h} (t) - I_{h} y (t) ∥_{2} \leq (1 - λ) E + λ E = E$ .

1.2F2F3F4given

Applying [F2] twice and using [F3] with $∥ y^{''} ∥_{2} \leq M$ gives Taylor remainders $R_{a}, R_{b}$ about $t$ satisfying $y (a) = y (t) + (a - t) y^{'} (t) + R_{a}$ , $y (b) = y (t) + (b - t) y^{'} (t) + R_{b}$ , $∥ R_{a} ∥_{2} \leq M (t - a)^{2} / 2$ , and $∥ R_{b} ∥_{2} \leq M (b - t)^{2} / 2$ .

2.1step 1.2F5algebra

In $(1 - λ) y (a) + λ y (b)$ the terms involving $y^{'} (t)$ cancel because $(1 - λ) (a - t) + λ (b - t) = 0$ . Hence [F5] gives $∥ I_{h} y (t) - y (t) ∥_{2} \leq \frac{M}{2} ((1 - λ) λ^{2} + λ (1 - λ)^{2}) h^{2} = \frac{M}{2} λ (1 - λ) h^{2} \leq M h^{2} / 8$ .

3.1F4F5step 1.1step 2.1algebra∎

By [F4], every delay breakpoint is a mesh node, so no cellwise estimate straddles a breakpoint. The triangle inequality [F5] combines steps 1.1 and 2.1 to give $∥ {\hat{y}}_{h} (t) - y (t) ∥_{2} \leq E + M h^{2} / 8$ on each cell, and taking the supremum proves the claim.

Depends on

Used by

Dependency tree · two levels

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