TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21

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.

Picard-Lindelöf local existence and uniqueness for first-order systems

Statement

Let $D \subseteq R \times R^{n}$ be open, let $F : D \to R^{n}$ be continuous and locally Lipschitz in the state variable, and let $(t_{0}, x_{0}) \in D$ . Then a unique local solution of the IVP exists on some interval around the initial time. More quantitatively, if $h, r > 0$ make

$[t_{0} - h, t_{0} + h] \times \overline{B} (x_{0}, r) \subseteq D,$

if $∥ F ∥_{2} \leq M$ and $F$ has state-Lipschitz constant $L$ on this cylinder, and if $h M \leq r$ and $L h < 1$ , then there is exactly one solution on $[t_{0} - h, t_{0} + h]$ through $(t_{0}, x_{0})$ whose graph lies in the cylinder. Any two solutions through the same initial data agree on every common subinterval containing $t_{0}$ .

In particular, a unique local solution exists on an interval around the initial time.

Facts & Assumptions

Given: The IVP in the Statement and a compact cylinder about $(t_{0}, x_{0})$ on which $F$ is bounded by $M$ and state-Lipschitz with constant $L$ .

[L1]

A contraction of a nonempty complete metric space has exactly one fixed point (A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point).

[L2]

A curve solves the IVP if and only if it satisfies the associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).

[L3]

Continuous $R^{n}$ -valued curves on a nonempty compact interval are complete in the supremum metric (Continuous $R^{n}$ -valued curves on a nonempty compact interval form a complete supremum-metric space).

[L4]

Under $h M \leq r$ , the Picard operator preserves the closed curve ball (A bounded vector field makes the Picard operator preserve a sufficiently short closed curve ball).

[L5]

Under $L h < 1$ , the Picard operator is a contraction (A state-Lipschitz vector field makes the Picard operator a contraction when $L h < 1$ ).

[L6]

Every interval in the real line is connected (The connected subspaces of $R$ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in $R$ ").

Proof

technique · direct

1.1givenL1L3L4L5

Choose $r > 0$ and then $h > 0$ so the cylinder lies in $D$ , $h M \leq r$ , and $L h < 1$ ; the closed curve ball is nonempty and complete by [L3], is invariant by [L4], and its Picard operator is a contraction by [L5], so [L1] gives exactly one fixed point.

2.1step 1.1L2L4L6∎

By [L2] the fixed point is a solution. Any other solution cannot leave the state ball before time $h$ , by the same first-exit estimate as [L4], so it is the same fixed point there. For two solutions on a larger common interval, their agreement set is nonempty and closed, and local repetition of this argument makes it open; the common interval is connected by [L6], so they agree throughout it.

Picard-Lindelöf local existence and uniqueness for first-order systems

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources