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.

Scaled Taylor action has a finite normwise truncation and roundoff certificate

Statement

Let $A \in M_{n} (C)$ , $n \geq 1$ , $v \in C^{n}$ , $t \in R$ , and choose $s \geq 1$ , $p \geq 0$ , and rational $R \in [0, 1]$ with $∣ t ∣ ∥ A ∥_{2} / s \leq R$ . Put $δ = t / s$ , $P : = \sum_{j = 0}^{p} (δ A)^{j} / j!$ , and

$Q_{p} (R) : = \frac{R^{p + 1}}{(p + 1)! (1 - R / (p + 2))} .$

Suppose each computed substep ${\hat{w}}_{ℓ}$ has local term and summation certificates $α_{ℓ j}, ζ_{ℓ j} \geq 0$ as in Finite scaled Taylor action for the matrix exponential, and define $d_{ℓ 0} : = 0$ , $d_{ℓ j} : = (R / j) d_{ℓ, j - 1} + α_{ℓ j}$ , and $ϵ_{ℓ} : = \sum_{j = 1}^{p} (d_{ℓ j} + ζ_{ℓ j})$ (empty sums are zero). Then

$∥ e^{t A} v - {\hat{w}}_{s} ∥_{2} \leq s 3^{s - 1} Q_{p} (R) ∥ v ∥_{2} + \sum_{ℓ = 1}^{s} 3^{s - ℓ} ϵ_{ℓ} .$

If the algorithm has rational upper bound $ρ_{v} \geq ∥ v ∥_{2}$ and returns success, its reported certificate is valid and at most the requested tolerance. A completed recurrence uses exactly $s p$ calls to $A$ . A return before the recurrence makes zero such calls; an early stop during it makes at most $s p$ calls.

Facts & Assumptions

Given: A finite complex matrix $A$ , vector $v$ , real time $t$ , integers $s \geq 1, p \geq 0$ , a rational upper bound $R \in [0, 1]$ for $∣ t ∣ ∥ A ∥_{2} / s$ , and successful local arithmetic certificates as specified by Finite scaled Taylor action for the matrix exponential.

[F1]

The phi-function family by everywhere-convergent series and The scalar and matrix phi series converge absolutely: $e^{t A} = φ_{0} (t A) = \sum_{j \geq 0} (t A)^{j} / j!$ .

[F2]

The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2: the operator $2$ -norm is submultiplicative and homogeneous.

[F3]

The exponential series of a bounded operator: the matrix exponential satisfies $e^{t A} e^{s A} = e^{(t + s) A}$ .

[F4]

Finite scaled Taylor action for the matrix exponential: each computed Taylor term and partial sum has the supplied local normwise error certificate, and the loop performs one $A$ call for each pair $(ℓ, j)$ .

Proof

technique · direct

1.1givenF1F2algebra

Let $R_{*} : = ∣ δ ∣ ∥ A ∥_{2} \leq R$ . For $j \geq p + 1$ , consecutive scalar tail terms have ratio $R_{*} / (j + 1) \leq R / (p + 2) < 1$ . The tail is therefore bounded by the geometric series beginning at $R^{p + 1} / (p + 1)!$ , giving $∥ e^{δ A} - P ∥_{2} \leq \sum_{j \geq p + 1} R^{j} / j! \leq Q_{p} (R)$ .

1.2F1F2algebra

For $0 \leq R \leq 1$ , $e^{R} = \sum_{j \geq 0} R^{j} / j! \leq \sum_{j \geq 0} 1 / j! \leq 3$ : for $j \geq 1$ , the $j - 1$ factors $2, \dots, j$ in $j!$ are each at least $2$ , so $j! \geq 2^{j - 1}$ and $\sum_{j \geq 1} 2^{- (j - 1)} = 2$ . Thus $∥ e^{δ A} ∥_{2} \leq 3$ and $∥ P ∥_{2} \leq \sum_{j = 0}^{p} R^{j} / j! \leq 3$ .

1.3givenF2F4algebrainduction

Fix substep $ℓ$ and let $z_{ℓ 0}^{*} : = {\hat{w}}_{ℓ - 1}$ and $z_{ℓ j}^{*} : = (δ / j) A z_{ℓ, j - 1}^{*}$ . The local provider certificate gives $∥ z_{ℓ j} - z_{ℓ j}^{*} ∥_{2} \leq (R / j) ∥ z_{ℓ, j - 1} - z_{ℓ, j - 1}^{*} ∥_{2} + α_{ℓ j}$ ; induction on $j$ yields the bound $d_{ℓ j}$ . The partial-sum certificate adds at most $ζ_{ℓ j}$ at stage $j$ , so $∥ {\hat{w}}_{ℓ} - P {\hat{w}}_{ℓ - 1} ∥_{2} \leq ϵ_{ℓ}$ .

2.1step 1.1step 1.2F2F3algebra

Write $X : = e^{δ A}$ . The algebraic telescoping identity $X^{s} - P^{s} = \sum_{j = 0}^{s - 1} X^{s - 1 - j} (X - P) P^{j}$ holds by cancellation of adjacent terms. By step 1.2 every summand has norm at most $3^{s - 1} Q_{p} (R)$ , so $∥ X^{s} v - P^{s} v ∥_{2} \leq s 3^{s - 1} Q_{p} (R) ∥ v ∥_{2}$ . By [F3], $X^{s} = e^{t A}$ .

2.2step 1.2step 1.3algebra

Set $e_{ℓ} : = {\hat{w}}_{ℓ} - P {\hat{w}}_{ℓ - 1}$ . Repeated substitution gives ${\hat{w}}_{s} - P^{s} v = \sum_{ℓ = 1}^{s} P^{s - ℓ} e_{ℓ}$ . By step 1.2, $∥ P^{s - ℓ} ∥_{2} \leq 3^{s - ℓ}$ , hence $∥ {\hat{w}}_{s} - P^{s} v ∥_{2} \leq \sum_{ℓ = 1}^{s} 3^{s - ℓ} ϵ_{ℓ}$ .

3.1step 2.1step 2.2F4algebra

The triangle inequality applied to steps 2.1 and 2.2 gives the stated total error certificate. The algorithm declares success only when its outward rational bound is at most the tolerance.

4.1givenF4∎

If the recurrence completes, its nested loops make one call to $A$ for each $1 \leq ℓ \leq s$ and $1 \leq j \leq p$ , giving exactly $s p$ calls, including zero when $p = 0$ . No other step calls $A$ , so a return before the recurrence makes zero calls and an early stop during it makes at most $s p$ calls.

Remarks

The certificate is for the specified finite matrix, time, budgets, norm bounds, and local arithmetic certificates. It asserts no mesh-uniform estimate from finite-dimensional exactness and returns an inconclusive status if any bound cannot be certified.

Depends on

Used by

Dependency tree · two levels

26 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

Awad H. Al-Mohy and Nicholas J. Higham, Computing the action of the matrix exponential, with an application to exponential integrators (standard reference, not scraped)
Nicholas J. Higham and Lijing Lin, Functions of Matrices: A Short Course (standard reference, not scraped)