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.
Forward Euler on the scalar linear equation
Example
For the IVP , , the exact solution is . The forward Euler map is . Its local defect from the exact value is
For every fixed finite interval with , this defect is uniformly in as , so the local order is exactly one. The one-step stability factor is .
Verification
Given: , , and the Euler map . Verify the defect and its order.
[F1] One-step ODE methods, local defect, uniform order, and step stability: the local defect is , and order one requires a uniform bound.
[F2] Forward Euler has uniform local order one and a one-step Lipschitz bound: under its continuous-partial-derivative and uniform-bound hypotheses, Euler has a componentwise local defect and one-step bound .
[F3] Multivariable Taylor formula with a Lagrange remainder along a line segment: for a scalar function, Taylor's formula through degree one has a second-derivative Lagrange remainder at an interior point of the segment.
Fix , let , and take and . These are an open domain with convex state fibers and a compact subset . For , the bounds in [F2] hold throughout with , , , and . The function solves the IVP, its graph on lies in , and for every the Euler output state lies between and , so its input and output pairs lie in . Starting from , Euler returns and the exact endpoint is . Therefore [F1] gives .
Apply [F3] to at with increment : there is with . Thus .
Since , for we have . The lower and upper bounds establish uniform error, hence order exactly one under [F1].
For any scalar inputs , . This verifies the stated stability factor; it also agrees with [F2] for and .
Remarks
The exact calculation is local: it does not turn a local defect estimate into a global trajectory bound. The Taylor formula here is used only for this smooth scalar example.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
17 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, Section III.2 (standard reference, not scraped)
- Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Julia Edition, Section 6.2.1 (standard reference, not scraped)