LemmaStatement: 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.

SDC iteration matrix for the scalar linear test equation

Statement

For the scalar test equation $y^{'} = λ y$ and $z = h λ$ , let $U^{*}$ be a collocation stage vector and $U^{k}$ the SDC iterates using the explicit-left-Euler stage block $Q_{Δ}$ from Finite explicit-left-Euler spectral deferred-correction sweep. Then $E^{k + 1} = B (z) E^{k}, B (z) : = (I - z Q_{Δ})^{- 1} z (Q - Q_{Δ}), E^{k} : = U^{k} - U^{*} .$ The inverse exists for every real $z$ because $Q_{Δ}$ is strictly lower triangular. In the induced infinity norm from Collocation tableau from distinct quadrature nodes, $∥ E^{k} ∥_{\infty, 2} \leq ∥ B (z) ∥_{\infty}^{k} ∥ E^{0} ∥_{\infty, 2}$ . This identity makes no convergence claim when the powers of $B (z)$ do not tend to zero; stability of the fully solved collocation step alone is not an SDC iteration guarantee.

Facts & Assumptions

Given: A fixed node set, its collocation matrices $Q, Q_{Δ}$ , a scalar $λ \in R$ , step $h > 0$ , and the scalar ODE $y^{'} = λ y$ .

[F1]

Finite explicit-left-Euler spectral deferred-correction sweep: the stage update is $U^{k + 1} = 1 u + h Q_{Δ} F (U^{k + 1}) + h (Q - Q_{Δ}) F (U^{k})$ .

[F2]

Fixed points of the SDC sweep are collocation stages: the SDC fixed point is the collocation stage vector.

[F3]

Finite explicit-left-Euler spectral deferred-correction sweep makes $Q_{Δ}$ strictly lower triangular; Collocation tableau from distinct quadrature nodes defines $∥ A ∥_{\infty} = \max_{i} \sum_{j} ∣ a_{i j} ∣$ .

Proof

1.1givenF1F2F3algebra

On this equation, $F (U) = λ U$ . Subtract the fixed-point instance of [F1] from its $k$ th sweep to obtain $(I - z Q_{Δ}) E^{k + 1} = z (Q - Q_{Δ}) E^{k} .$ The diagonal of $I - z Q_{Δ}$ consists of ones and it is lower triangular by [F3], so forward substitution uniquely solves this system for every $z \in R$ .

2.1step 1.1F3algebra∎

Solving step 1.1 gives $E^{k + 1} = B (z) E^{k}$ with the displayed $B (z)$ ; induction yields $E^{k} = B (z)^{k} E^{0}$ . For any vector $v$ , the row-wise triangle inequality gives $∥ B (z) v ∥_{\infty, 2} \leq ∥ B (z) ∥_{\infty} ∥ v ∥_{\infty, 2}$ , so applying this bound $k$ times gives the stated power estimate. No bound less than one is asserted for general $z$ or node sets.

Depends on

Used by

An explicit SDC sweep diverges on a stiff scalar mode Example

Dependency tree · two levels

9 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), §§1.1 and 3 (standard reference, not scraped)