TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

Contraction and residual error bound for the SDC sweep

Statement

Let $C$ be a nonempty closed product ball of admissible stage vectors in $(R^{d})^{M}$ , with metric $∥ U - V ∥_{\infty, 2} = \max_{i} ∥ U_{i} - V_{i} ∥_{2}$ . For each $V \in C$ , assume the inner stage map $Z ⟼ 1 u + h Q_{Δ} F (Z) + h (Q - Q_{Δ}) F (V)$ maps $C$ into itself, and assume the stage field $F (U) = (f (t + c_{i} h, U_{i}))_{i = 1}^{M}$ is $L$ -Lipschitz there for some $L \geq 0$ . Put $a = h L ∥ Q_{Δ} ∥_{\infty}, q = \frac{h L ∥ Q - Q_{Δ} ∥_{\infty}}{1 - a} .$ If $a < 1$ and $q < 1$ , then every sweep is uniquely defined in $C$ , the sweep map $S : U^{k} \mapsto U^{k + 1}$ is a contraction with constant $q$ , and its unique fixed point $U^{*}$ is the unique collocation stage vector in $C$ . For every $V \in C$ , $∥ V - U^{*} ∥_{\infty, 2} \leq \frac{∥ S (V) - V ∥_{\infty, 2}}{1 - q} .$ If the initial iterate satisfies $U^{0} \in C$ , then the iterates $U^{k + 1} = S (U^{k})$ obey $∥ U^{k} - U^{*} ∥_{\infty, 2} \leq q^{k} ∥ U^{0} - U^{*} ∥_{\infty, 2}$ . In particular, a residual-certified predictor used with Finite explicit-left-Euler spectral deferred-correction sweep must lie in $C$ . These are local stage-iteration claims; they assert no convergence when either contraction inequality fails.

Facts & Assumptions

Given: The SDC sweep, its lower-triangular stage preconditioner $Q_{Δ}$ , a nonempty closed product ball $C$ , and the self-map and Lipschitz hypotheses in the Statement. The geometric iterate estimate additionally has the stated premise $U^{0} \in C$ .

[F1]

$R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ : every Cauchy sequence in a finite-dimensional Euclidean space converges in that space.

[F2]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation and The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the Euclidean norm has the triangle inequality.

[F3]

A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point: a contraction of a nonempty complete metric space into itself has a unique fixed point and its iterates converge to that point.

[F4]

Fixed points of the SDC sweep are collocation stages: a fixed point of the SDC sweep is exactly a solution of the collocation stage equations.

[F5]

Collocation tableau from distinct quadrature nodes: $∥ Q ∥_{\infty} = \max_{i} \sum_{j} ∣ Q_{i j} ∣$ , and the row-sum norm satisfies $∥ A V ∥_{\infty, 2} \leq ∥ A ∥_{\infty} ∥ V ∥_{\infty, 2}$ for block vectors.

[F6]

Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric: a metric is symmetric, separates distinct points, and satisfies the triangle inequality.

[F7]

Cauchy sequence in a metric space: a sequence is Cauchy when its pairwise distances tend to zero uniformly beyond a sufficiently large index.

[F8]

Complete metric space: every Cauchy sequence converges in the space: a metric space is complete when every Cauchy sequence converges to a point in it.

[A1]

For each $V \in C$ , the inner stage map $Z \mapsto 1 u + h Q_{Δ} F (Z) + h (Q - Q_{Δ}) F (V)$ maps $C$ into itself; $F$ is $L$ -Lipschitz in $∥ \cdot ∥_{\infty, 2}$ on $C$ ; and $a < 1$ , $q < 1$ . For the geometric iterate estimate, $U^{0} \in C$ .

Proof

1.1givenA1F1F2F6F7F8construct

The block distance $d (U, V) = \max_{i} ∥ U_{i} - V_{i} ∥_{2}$ has the metric properties [F6]: symmetry and separation hold coordinatewise, and [F2] gives $d (U, W) \leq d (U, V) + d (V, W)$ . If $(U^{n})$ is $d$ -Cauchy in the sense of [F7], then each of its finitely many Euclidean coordinates is Cauchy; [F1] gives coordinate limits. Since $C$ is a closed product ball, the coordinatewise limit belongs to $C$ , so [F8] makes $(C, d)$ complete.

2.1A1F3F5step 1.1algebra

For a fixed previous iterate $V \in C$ , the new-stage equation is $Z = 1 u + h Q_{Δ} F (Z) + h (Q - Q_{Δ}) F (V)$ . Its right-hand side maps $C$ into itself by [A1]; the norm inequality in [F5] and the Lipschitz bound in [A1] show that its difference at $Z, W \in C$ is at most $a ∥ Z - W ∥_{\infty, 2}$ . Since $a < 1$ , [F3] gives a unique $Z = S (V)$ in $C$ .

3.1A1F5step 2.1algebra

Let $V, W \in C$ , and write $Z = S (V)$ , $Z^{'} = S (W)$ . Subtracting their stage equations cancels the fixed initial derivative and yields $∥ Z - Z^{'} ∥_{\infty, 2} \leq h L ∥ Q_{Δ} ∥_{\infty} ∥ Z - Z^{'} ∥_{\infty, 2} + h L ∥ Q - Q_{Δ} ∥_{\infty} ∥ V - W ∥_{\infty, 2} .$ Rearranging by $1 - a > 0$ gives $∥ S (V) - S (W) ∥_{\infty, 2} \leq q ∥ V - W ∥_{\infty, 2}$ , so $S$ is a contraction of $C$ .

4.1A1F3F4step 1.1step 3.1induction

By [F3] and step 1.1, $S$ has a unique fixed point $U^{*} \in C$ . Fact [F4] identifies it with the unique collocation stage vector in this ball. Under the iterate premise $U^{0} \in C$ in [A1], repeated application of the contraction inequality in step 3.1 gives $∥ U^{k} - U^{*} ∥_{\infty, 2} \leq q^{k} ∥ U^{0} - U^{*} ∥_{\infty, 2}$ .

5.1A1step 3.1step 4.1F2algebra∎

For any $V \in C$ , $S (U^{*}) = U^{*}$ and the triangle inequality give $∥ V - U^{*} ∥_{\infty, 2} \leq ∥ V - S (V) ∥_{\infty, 2} + ∥ S (V) - S (U^{*}) ∥_{\infty, 2} \leq ∥ V - S (V) ∥_{\infty, 2} + q ∥ V - U^{*} ∥_{\infty, 2}$ . Since $1 - q > 0$ , rearranging proves the residual estimate.

Depends on

Used by

Dependency tree · two levels

61 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

Mathew F. Causley and David C. Seal, On the convergence of spectral deferred correction methods, Communications in Applied Mathematics and Computational Science 14 (2019), §3 (standard reference, not scraped)
Ernst Hairer, Syvert P. Nørsett, and Gerhard Wanner, Solving Ordinary Differential Equations I, 2nd ed., Chapter II §II.7 (standard reference, not scraped)