Alphabeta MathHow 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.
First-order systems, initial value problems, and solutions on intervals
Definition
Let be open, let , and let . The equation
is a first-order system. An initial value problem consists of this equation and data , written .
A solution on an interval is a function such that , for every , is differentiable on in the domain-relative sense of The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, and
Endpoints of use the corresponding one-sided, domain-relative derivative. A local solution is one whose interval contains a nondegenerate neighborhood of relative to the time projection of .
Depends on
Used by
- The Dirichlet right-hand side gives a first-order equation with no solution Counterexample
- Extensions, maximal solutions, maximal intervals, and global solutions Definition
- Local Lipschitz continuity in the state variable, locally uniform in time and parameters Definition
- Euler polygonal approximations for a continuous ODE are uniformly bounded and equicontinuous Lemma
- Locally unique ODE solutions agree on overlaps and glue across a common endpoint Lemma
- A first-order initial value problem is equivalent to its Volterra integral equation Proposition
- A scalar first-order linear ODE has a unique solution given by the integrating-factor formula Theorem
- Osgood's criterion gives uniqueness without a Lipschitz bound Theorem
- Picard-Lindelöf local existence and uniqueness for first-order systems Theorem
Dependency tree · two levels
25 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
- Gerald Teschl, Ordinary Differential Equations and Dynamical Systems, Ch. 2 (standard reference, not scraped)
- Jiri Lebl, Basic Analysis I, Section 6.3 (standard reference, not scraped)