TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

IMEX Euler preserves first-order convergence under per-step residuals of order h squared

Statement

Let $T > 0$ , $N \geq 1$ , $h = T / N$ , and let the exact solution and exact-root IMEX Euler map satisfy the common-tube hypotheses of IMEX Euler has a first-order local defect and a one-step stability bound. Set ${\tilde{y}}_{0} : = y_{0}$ . At step $n$ , suppose the solver returns ${\tilde{y}}_{n + 1}$ in the selected branch ball centered at $c_{n} = {\tilde{y}}_{n} + h a ({\tilde{y}}_{n})$ , with unscaled update residual $r_{n} : = {\tilde{y}}_{n + 1} - c_{n} - h b ({\tilde{y}}_{n + 1}), ∥ r_{n} ∥_{2} \leq C_{r} h^{2} .$ Assume $h L_{b} \leq 1 / 2$ in every branch ball, and that the exact path, numerical states, candidates, and exact branches remain in the common tube. For all sufficiently small $h = T / N$ satisfying these hypotheses, if $∥ y_{0} - y (0) ∥_{2} \leq C_{0} h$ , then $\max_{0 \leq n \leq N} ∥ {\tilde{y}}_{n} - y (t_{n}) ∥_{2} \leq C_{T} h,$ where $C_{T}$ is independent of $h$ and the step index. The residual is in update units; a derivative-scaled residual bound must be multiplied by $h$ before applying this statement.

Facts & Assumptions

Given: The grid, additive IVP, residual candidates, branch balls, common tube, and bounds in the Statement.

[F1]

IMEX Euler has a first-order local defect and a one-step stability bound: the exact-root map has local defect at most $C_{ℓ} h^{2}$ and is Lipschitz with constant $1 + L h$ on the tube.

[F2]

A local IMEX Euler branch from contraction: on a branch ball with $h L_{b} < 1$ , the unscaled update residual gives $∥ {\tilde{y}}_{n + 1} - y_{n + 1}^{*} ∥_{2} \leq ∥ r_{n} ∥_{2} / (1 - h L_{b})$ for its unique exact root $y_{n + 1}^{*}$ .

[F3]

Finite geometric error bound from a one-step recurrence: if $e_{n + 1} \leq (1 + L h) e_{n} + C h^{p + 1}$ for $h = T / N$ and $e_{0} \leq C_{0} h^{p}$ , then $\max_{n} e_{n} \leq C_{T} h^{p}$ with a constant independent of $h$ and $n$ .

[F4]

Implicit residuals and their update and derivative units: the update residual has the same units as the unknown; the derivative residual is the update residual divided by $h$ .

[A1]

In each step's closed branch ball $\overline{B} (c_{n}, R_{n}) \subset U$ , $R_{n} > 0$ , $∥ b ∥_{2} \leq M_{b}$ , $b$ is $L_{b}$ -Lipschitz, $h M_{b} \leq R_{n}$ , and $h L_{b} \leq 1 / 2$ ; both the unique exact root and returned candidate lie in that ball. The uniform tube constants in [F1] hold.

Proof

1.1givenF2A1algebra

Since $h L_{b} \leq 1 / 2$ , [F2] gives $∥ {\tilde{y}}_{n + 1} - Ψ_{h} ({\tilde{y}}_{n}) ∥_{2} \leq 2 C_{r} h^{2}$ , where $Ψ_{h} ({\tilde{y}}_{n}) = y_{n + 1}^{*}$ is the exact-root update from the current numerical state. The bound is valid at every step by [A1].

2.1F1step 1.1algebra

By the triangle inequality, [F1], and step 1.1, $e_{n + 1} : = ∥ {\tilde{y}}_{n + 1} - y (t_{n + 1}) ∥_{2} \leq (1 + L h) e_{n} + (C_{ℓ} + 2 C_{r}) h^{2} .$ Here the first term compares the exact-root map at ${\tilde{y}}_{n}$ with that map at $y (t_{n})$ ; the local-defect term compares the latter output with the exact next state.

3.1F3F4step 2.1given∎

Apply [F3] to this recurrence with $p = 1$ , $C = C_{ℓ} + 2 C_{r}$ , and the initial error from the Statement. This proves the displayed $O (h)$ global bound. By [F4], if a solver instead reports the derivative-scaled residual $r_{n} / h$ , the assumed update-residual budget is obtained by multiplying that bound by $h$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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

Uri M. Ascher, Steven J. Ruuth, and Raymond J. Spiteri, Implicit-explicit Runge-Kutta methods for time-dependent partial differential equations (standard reference, not scraped)
Tobias Embree, Lecture Notes on Numerical Analysis (standard reference, not scraped)