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.
Every Picard–Lindelöf initial value problem has one maximal solution on an open interval
Statement
Every initial value problem satisfying the Picard-Lindelof hypotheses has a unique maximal solution. Its domain is an open interval containing the initial time, and every other solution through the same data is its restriction.
Facts & Assumptions
Given: An IVP satisfying the hypotheses of Picard-Lindelof.
A unique local solution exists on an interval around the initial time (Picard-Lindelöf local existence and uniqueness for first-order systems).
Locally unique solutions through the same data agree on every overlap (Locally unique ODE solutions agree on overlaps and glue across a common endpoint).
Proof
Take the union of the domains of all local solutions through the initial point; [L1] makes the family nonempty, the union of intervals containing is an interval, and local existence around every graph point makes open.
By [L2], all values assigned at a time in agree, so their pointwise union is a well-defined solution; every other solution is its restriction, which proves maximality, and the same property forces uniqueness of the maximal solution.
Depends on
Used by
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
- 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)