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.
Sectional forward Euler separates temporal, quadrature, and cutoff errors
Statement
Assume all hypotheses of Sectional size discretization separates grid and cutoff errors, with continuous-model solution on , initial mass , grid spacing , and pivot endpoint . Let the finite grid have retained bins, take , an integer , and . Initialize both the exact finite sectional system and forward Euler by that theorem's same retained projection and tail-mass reservoir. Let be the successful forward-Euler states under the uniform positivity CFL, and let be the exact finite-sectional retained measure. There are constants and independent of such that The first term is temporal error for the fixed finite ODE; the terms in and are the separate grid and cutoff errors. The temporal constant may depend on the fixed grid and cutoff.
Facts & Assumptions
Given: A fixed finite-dimensional sectional ODE, its accepted forward-Euler steps, and the grid/cutoff estimate.
Sectional forward Euler converges globally with first-order error: for the fixed finite system.
Sectional size discretization separates grid and cutoff errors: the exact finite-sectional retained measure differs from by the displayed grid and cutoff terms.
Proof
Write the population-coordinate error vector as . Its total-variation norm as an atomic signed measure is at most by Cauchy-Schwarz. Thus [F1] and [F3] bound the temporal discrepancy by .
Insert the exact finite-sectional measure between the Euler retained measure and . The triangle inequality and [F2] add the temporal term from step 1.1 to the grid and cutoff terms in [F2], giving the asserted separated error budget.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
16 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
- Ernst Hairer, course notes, Chapter III: Équations Différentielles Ordinaires, §§III.2–III.3 (standard reference, not scraped)
- Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, §6.2 (standard reference, not scraped)