PropositionStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

A first-order initial value problem is equivalent to its Volterra integral equation

Statement

Let $n \geq 1$ , let $D \subseteq R \times R^{n}$ be open, let $F : D \to R^{n}$ be continuous, let $(t_{0}, x_{0}) \in D$ , let $I \subseteq R$ be order-convex with at least two elements, and let $x : I \to R^{n}$ be continuous with $t_{0} \in I$ and $(t, x (t)) \in D$ . A curve solves the IVP if and only if it satisfies the associated Volterra integral equation. Explicitly, the equation is

$x (t) = x_{0} + \int_{t_{0}}^{t} F (s, x (s)) d s (t \in I) .$

The integral is oriented, so the assertion applies on either side of $t_{0}$ .

Facts & Assumptions

Given: The data in the Statement and componentwise vector integration as in The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral.

[L1]

If a differentiable $f : [a, b] \to R^{m}$ has integrable derivative, then $\int_{a}^{b} f^{'} = f (b) - f (a)$ (If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz).

[L2]

If $I$ is order-convex with at least two elements, $g : I \to R$ is continuous, and $t_{0} \in I$ , then $t \mapsto \int_{t_{0}}^{t} g$ is a primitive of $g$ on $I$ (Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ ).

[L3]

Every continuous real function on a compact interval is Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

Proof

technique · direct

1.1

For the forward direction, the identity is immediate at $t = t_{0}$ ; for $t \neq t_{0}$ , each component of $x^{'} = F (\cdot, x)$ is continuous and hence integrable by [L3], so [L1] on the closed interval between $t_{0}$ and $t$ , followed by orientation when $t < t_{0}$ , gives $x (t) - x_{0} = \int_{t_{0}}^{t} F (s, x (s)) d s$ .

givenL1L3

2.1

For the reverse direction, [L2] applied componentwise differentiates the displayed integral equation and gives $x^{'} (t) = F (t, x (t))$ ; at $t = t_{0}$ the oriented integral is $0$ , so $x (t_{0}) = x_{0}$ .

givenL2algebra∎

Depends on

Used by

Dependency tree · two levels

69 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)