TheoremStatement: Literature-sourcedProof: 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.

Compatible-grid Euler has first-order solution and derivative error for a stable neutral delay

Statement

Let $T = K τ$ with integers $K, m \geq 1$ , set $h = τ / m$ and $N = K m$ , and let $∣ a ∣ < 1$ . Assume the compatible scalar neutral-delay problem of Scalar neutral delay equations and the derivative-segment shift has the unique solution $y$ supplied by Method of steps gives a unique compatible neutral-delay solution. Suppose $y$ is $C^{1}$ on $[0, T]$ , each grid-cell restriction is $C^{2}$ with one-sided endpoint derivatives, and $∣ y^{''} (t) ∣ \leq M$ on each cell interior for a constant $M \geq 0$ . Apply Explicit Euler for a scalar neutral delay on a compatible grid with exact history values and complete all $N$ updates (no budget or an integer budget $B \geq N$ ). Put $Λ = 2 L / (1 - ∣ a ∣)$ . If $Λ > 0$ , set $C_{T} = (M / 2) (e^{Λ T} - 1) / Λ$ ; if $Λ = 0$ , set $C_{T} = M T / 2$ . Then $\max_{0 \leq n \leq N} ∣ Y_{n} - y (t_{n}) ∣ \leq C_{T} h, \max_{0 \leq n < N} ∣ V_{n} - y^{'} (t_{n}) ∣ \leq Λ C_{T} h .$

Facts & Assumptions

Given: The scalar neutral-delay equation, compatible history, stable coefficient $∣ a ∣ < 1$ , a completed grid-aligned Euler run (no budget or $B \geq N$ ), and the piecewise $C^{2}$ exact solution in the Statement.

[F1]

At each time $t_{n}$ , $y^{'} (t_{n}) = a y^{'} (t_{n} - τ) + f (t_{n}, y (t_{n}), y (t_{n} - τ))$ , with negative-time values and derivatives given by $ϕ$ and $ϕ^{'}$ (Scalar neutral delay equations and the derivative-segment shift).

[F2]

Euler initializes the history exactly and uses $V_{n} = a ϕ^{'} (t_{n} - τ) + f (t_{n}, Y_{n}, Y_{n - m})$ for $n < m$ , and $V_{n} = a V_{n - m} + f (t_{n}, Y_{n}, Y_{n - m})$ for $n \geq m$ (Explicit Euler for a scalar neutral delay on a compatible grid).

[F3]

On any finite derivative-array prefix of length $M$ , the delayed mesh shift has inverse $(I - a S)^{- 1}$ with operator norm at most $(1 - ∣ a ∣)^{- 1}$ (The neutral derivative shift has a bounded Neumann inverse when $∣ a ∣ < 1$ ).

[F4]

A bounded derivative makes a differentiable vector path Lipschitz, and the vector-valued fundamental theorem gives increments as integrals (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).

[F5]

Under the canonical scalar/ $R^{1}$ coordinate identification, the norm of an integrable vector-valued integral is at most the integral of its 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, Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions).

[F6]

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

[L1]

If $e_{0} \leq C_{0} h^{p}$ and $e_{n + 1} \leq (1 + ℓ h) e_{n} + C h^{p + 1}$ on a uniform grid of length $T$ , then the finite recurrence has the explicit exponential bound, including the $ℓ = 0$ branch (Finite geometric error bound from a one-step recurrence).

Proof

1.1F1F2givenalgebra

Define $e_{j} = ∣ Y_{j} - y (t_{j}) ∣$ for $j \geq 0$ , $e_{j} = 0$ for $- m \leq j < 0$ , $E_{n} = \max_{- m \leq j \leq n} e_{j}$ , and $w_{j} = V_{j} - y^{'} (t_{j})$ . For $j < m$ , [F1]--[F2] give $w_{j} = f (t_{j}, Y_{j}, Y_{j - m}) - f (t_{j}, y (t_{j}), y (t_{j} - τ))$ ; for $j \geq m$ they give $w_{j} = a w_{j - m}$ plus this same $f$ difference. In both cases the residual vector $g_{0 : n} : = w_{0 : n} - a S_{m}^{(n + 1)} w_{0 : n}$ has supremum norm at most $2 L E_{n}$ .

1.2F4F5givenalgebra

By [F4], $y (t_{n + 1}) - y (t_{n}) = \int_{t_{n}}^{t_{n + 1}} y^{'} (s) d s$ . On this cell, [F4] applied to $y^{'}$ gives $∣ y^{'} (s) - y^{'} (t_{n}) ∣ \leq M (s - t_{n})$ ; [F5] then bounds the difference between this integral and $h y^{'} (t_{n})$ by $\int_{t_{n}}^{t_{n + 1}} M (s - t_{n}) d s = M h^{2} / 2$ .

2.1F3step 1.1algebra

The shift inverse [F3], applied to the prefix of length $n + 1$ , yields $\max_{0 \leq j \leq n} ∣ w_{j} ∣ \leq 2 L E_{n} / (1 - ∣ a ∣) = Λ E_{n}$ .

3.1F2F6step 2.1step 1.2L1algebra∎

Subtract the exact increment of step 1.2 from the Euler update in [F2] and use the triangle inequality [F6] and step 2.1 to obtain $e_{n + 1} \leq e_{n} + h Λ E_{n} + (M / 2) h^{2}$ . Hence $E_{n + 1} \leq (1 + Λ h) E_{n} + (M / 2) h^{2}$ , with $E_{0} = 0$ . Applying [L1] with $p = 1$ , $C_{0} = 0$ , $C = M / 2$ , and $ℓ = Λ$ gives $E_{N} \leq C_{T} h$ in both branches of the Statement. Step 2.1 then gives the stated derivative bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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