TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge 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.

IMEX Euler is first-order convergent on a common compact tube

Statement

Let $T > 0$ , $N \geq 1$ , $h = T / N$ , and let $y (t)$ solve the additive IVP of Additive autonomous ODE partitions on $[0, T]$ . Assume the exact path, all numerical states, and every selected implicit branch remain in a common compact convex tube with positive margin in the state domain. Suppose the uniform hypotheses of IMEX Euler has a first-order local defect and a one-step stability bound hold on this tube and use the exact-root IMEX Euler map with exact initial value $y_{0} = y (0)$ . For all sufficiently small $h = T / N$ satisfying these hypotheses, there is a constant $C_{T}$ , independent of $h$ and the step index, such that $\max_{0 \leq n \leq N} ∥ y_{n} - y (t_{n}) ∥_{2} \leq C_{T} h .$ This is a fixed-time first-order result for the selected local branch; it makes no assertion about other implicit roots.

Facts & Assumptions

Given: The finite grid, exact solution, exact-root IMEX Euler map, common tube, and branch hypotheses in the Statement.

[F1]

IMEX Euler has a first-order local defect and a one-step stability bound: on the common tube, the exact-start defect is bounded by $C h^{2}$ and the selected-root map is Lipschitz with constant $1 + L h$ .

[F2]

Global error from uniform one-step defect and stability: for a one-step map on a common compact tube, uniform local defect $C h^{p + 1}$ , one-step Lipschitz constant $1 + L h$ , and initial error at most $C_{0} h^{p}$ imply a fixed-time global error bound of order $h^{p}$ .

[A1]

The exact path, numerical states, and all implicit stages stay in the tube, so the uniform constants and map hypotheses of [F1] hold at every step.

Proof

1.1F1A1algebra

By [F1] and [A1], for each $n < N$ the exact-start local defect satisfies $∥ Ψ_{h} (y (t_{n})) - y (t_{n + 1}) ∥_{2} \leq C h^{2}$ , and for all compared states in the tube $∥ Ψ_{h} (u) - Ψ_{h} (v) ∥_{2} \leq (1 + L h) ∥ u - v ∥_{2}$ . The exact initial value gives zero initial error, which is at most $0 \cdot h$ .

2.1F2A1step 1.1∎

Apply [F2] with $p = 1$ , $C_{0} = 0$ , and the constants from step 1.1. All hypotheses are satisfied by [A1], so its fixed-time estimate gives $\max_{n \leq N} ∥ y_{n} - y (t_{n}) ∥_{2} \leq C_{T} h$ for a constant independent of $h$ and $n$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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