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.

Picard iteration converges with geometric short-time and factorial cylinder error bounds

Statement

Let $T$ be a Picard operator on an invariant curve ball over a time interval of half-length $h$ , and let $L$ be a state-Lipschitz constant. Starting at $x^{(0)} (t) = x_{0}$ , the iterates converge uniformly to the unique fixed point. If $q = L h < 1$ , the Banach a priori and a posteriori bounds hold. Without $L h < 1$ ,

$d_{\infty} (T^{m} x, T^{m} y) \leq \frac{(L h)^{m}}{m!} d_{\infty} (x, y),$

and the corresponding factorial-series tail bounds the error.

Facts & Assumptions

Given: The invariant Picard ball, the constant $L$ , and the index-zero iterate.

[L1]

For a contraction of constant $q < 1$ , $d (x^{*}, x_{n}) \leq q^{n} d (x_{1}, x_{0}) / (1 - q)$ , with the corresponding a posteriori estimate (The a priori bound $d (x^{*}, x_{n}) \leq q^{n} d (x_{1}, x_{0}) / (1 - q)$ and the a posteriori bound $d (x^{*}, x_{n + 1}) \leq q d (x_{n + 1}, x_{n}) / (1 - q)$ ).

[L2]

Summably contracting iterates have a unique fixed point and the iteration tail bounds its error (Weissinger's fixed-point criterion for summably contracting iterates).

[L3]

The exponential-series partial sums converge to $\exp$ uniformly on every bounded interval (Picard iteration from $1$ produces the exponential partial sums).

[L4]

For an integrable vector-valued function on $[a, b]$ with $a \leq b$ , ${∥ \int_{a}^{b} f ∥}_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable).

[L5]

If $q = L h < 1$ , the Picard operator on the invariant curve ball is a contraction with constant $q$ (A state-Lipschitz vector field makes the Picard operator a contraction when $L h < 1$ ).

[L6]

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

[L7]

A closed subspace of a complete metric space is complete (A subspace of a complete metric space is complete iff it is closed, and a complete subspace of any metric space is closed).

Proof

technique · direct

1.1

When $q = L h < 1$ , [L5] makes the Picard operator a contraction with constant $q$ , so substitution into [L1] gives the geometric estimates; if $L = 0$ , all differences vanish after one Picard step.

givenL1L5algebra

1.2

For $m = 1$ , [L4] gives the pointwise bound $∥ T x (t) - T y (t) ∥_{2} \leq L ∣ t - t_{0} ∣ d_{\infty} (x, y)$ . If the corresponding bound holds with $m - 1$ , another application of [L4] integrates $L^{m} ∣ s - t_{0} ∣^{m - 1} / (m - 1)!$ from $t_{0}$ to $t$ and gives $L^{m} ∣ t - t_{0} ∣^{m} / m!$ ; induction and $∣ t - t_{0} ∣ \leq h$ yield the displayed supremum estimate.

givenL4algebra

2.1

The invariant curve ball is a closed ball in the supremum metric, hence is nonempty and complete by [L6] and [L7]. By [L3], the series $\sum_{m \geq 1} (L h)^{m} / m!$ converges, so [L2] applied to step 1.2 gives uniform convergence to the unique fixed point and the stated factorial tail estimate, including $h = 0$ .

step 1.2L2L3L6L7algebra∎

Depends on

Used by

Picard iteration for y'=y, y(0)=1, recovers the exponential series Example

Dependency tree · two levels

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