Alphabeta Math
PropositionStatement: AI-adaptedProof: 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 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)=x0, the iterates converge uniformly to the unique fixed point. If q=Lh<1, the Banach a priori and a posteriori bounds hold. Without Lh<1,

d∞(Tmx,Tmy)≤(Lh)mm!d∞(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∗,xn)≤qnd(x1,x0)/(1−q), with the corresponding a posteriori estimate (The a priori bound d(x∗,xn)≤qnd(x1,x0)/(1−q) and the a posteriori bound d(x∗,xn+1)≤q d(xn+1,xn)/(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≤b, ∥∫abf∥2≤∫ab∥f∥2 (For a≤b and f:[a,b]→Rm integrable when a<b, ∥∫abf∥2≤∫ab∥f∥2; for a<b, ∥f∥2 is integrable).

[L5]

If q=Lh<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 Lh<1).

[L6]

Continuous Rn-valued curves on a nonempty compact interval form a complete space in the supremum metric (Continuous Rn-valued curves on a nonempty compact interval form a complete supremum-metric space).

[L7]

A closed subspace of a complete metric space is complete (Closed subspaces of complete metric spaces are complete; the converse under countable choice).

Proof

technique · direct
1.1givenL1L5algebra

When q=Lh<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.

1.2givenL4algebra

For m=1, [L4] gives the pointwise bound ∥Tx(t)−Ty(t)∥2≤L∣t−t0∣d∞(x,y). If the corresponding bound holds with m−1, another application of [L4] integrates Lm∣s−t0∣m−1/(m−1)! from t0 to t and gives Lm∣t−t0∣m/m!; induction and ∣t−t0∣≤h yield the displayed supremum estimate.

2.1step 1.2L2L3L6L7algebra∎

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 ∑m≥1(Lh)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.

Depends on

Used by

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