TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Padé error and squaring defects give a conditional exponential error bound

Statement

Suppose Finite-order Padé scaling-and-squaring exponential returns status conditional-error-bound for a stored finite matrix $A$ , Padé order $m$ , and scaling count $s$ , with computed candidate ${\hat{X}}_{s}$ and exact nonnegative upper bound $E_{s}$ (rational in the fully encoded rational adapter). Also suppose the caller-supplied certification hypotheses hold: with $B = 2^{- s} A$ , the cycle $Γ$ is polygonal with trace in $∣ z ∣ \leq ρ$ for exact dyadic $ρ > 0$ , $σ (B) \subset {∣ z ∣ < ρ}$ , $Γ$ is disjoint from $σ (B)$ and null-homologous in the disk, and its index is one at every point of $σ (B)$ . Then $∥ {\hat{X}}_{s} - \exp (A) ∥_{\infty, C} \leq E_{s} .$ The assertion is conditional on the exact denominator residual, scalar disk remainder, caller-supplied contour topology, validated contour resolvent bound, and every recorded squaring-defect bound. The validator does not establish the contour hypotheses or count enclosed eigenvalues. A finite budget need not produce a bound.

Facts & Assumptions

Given: A conditional-error-bound return with exact stored matrix $A$ , Padé order $m$ , scale $s$ , disk radius $ρ$ , $d_{m} (ρ) > 0$ , coefficient-weighted contour length upper $ℓ$ , validator bound $M$ , scalar exponential upper bounds $U (ρ)$ and $U (α)$ , local squaring bounds $δ_{j}$ , and recurrence values $E_{j}$ .

[F1]

The algorithm forms $B = 2^{- s} A$ , computes the rational-coefficient polynomial matrices $P_{m} (B)$ and $Q_{m} (B)$ exactly, and accepts its initial candidate only after an exact solve check (Finite-order Padé scaling-and-squaring exponential).

[F2]

A verified denominator solve satisfies $Q_{m} (B) {\hat{X}}_{0} = P_{m} (B)$ exactly (An exact residual check certifies the Padé denominator solve).

[F3]

The scalar exponential is the everywhere-defined power series (The complex exponential by its power series). If $d_{m} (ρ) > 0$ , then $q_{m}$ has no zero in the disk and $∣ e^{z} - r_{m} (z) ∣ \leq ρ^{2 m + 1} e^{ρ} (m!)^{2} / ((2 m)! (2 m + 1)! d_{m} (ρ))$ for $∣ z ∣ \leq ρ$ (A finite scalar remainder bound for the diagonal Padé exponential).

[F4]

A scalar rational error and uniform contour resolvent bound imply $∥ e^{B} - r_{m} (B) ∥_{\infty, C} \leq L_{Γ} ε M / (2 π)$ (A resolvent contour bound transfers scalar rational error to matrices).

[F5]

The validator's successful return supplies the stated uniform resolvent bound on every supplied contour segment (The finite disk cover validator returns a uniform resolvent bound on success).

[F6]

If ${\hat{X}}_{j + 1} = {\hat{X}}_{j}^{2} + D_{j}$ and $X_{j + 1} = X_{j}^{2}$ , then $∥ {\hat{X}}_{j + 1} - X_{j + 1} ∥ \leq (2 ∥ X_{j} ∥ + ∥ {\hat{X}}_{j} - X_{j} ∥) ∥ {\hat{X}}_{j} - X_{j} ∥ + ∥ D_{j} ∥$ (Error propagation through exact and perturbed squaring steps).

[F7]

The complex infinity norm is the maximum absolute row sum (The complex induced infinity matrix norm) and is submultiplicative (The complex infinity matrix norm is compatible and submultiplicative).

[F8]

The bounded-operator exponential series is absolutely convergent and satisfies $∥ \exp (t T) ∥ \leq e^{∣ t ∣ ∥ T ∥}$ (Every finite-dimensional normed space is Banach, The exponential series of a bounded operator).

[F9]

Analytic primary matrix functions respect products (Jordan, contour, similarity, and normal-functional-calculus formulas agree).

[F10]

The Padé functions are $p_{m} (z)$ , $q_{m} (z) = p_{m} (- z)$ , and $r_{m} (z) = p_{m} (z) / q_{m} (z)$ where the denominator is nonzero (Diagonal Padé approximant to the exponential).

[F11]

The algorithm defines $U (0) = 1$ and, for $0 < x < K + 2$ , $U (x) = \sum_{k = 0}^{K} x^{k} / k! + [x^{K + 1} / (K + 1)!] / (1 - x / (K + 2))$ (Finite-order Padé scaling-and-squaring exponential). Its upper-bound property is proved in step 1.1 below.

[L1]

$π / 4 = \int_{0}^{1} (1 + x^{2})^{- 1} d x$ , and on $[0, 1]$ the finite identity $\frac{1}{1 + x^{2}} = \sum_{k = 0}^{7} (- x^{2})^{k} + \frac{x^{16}}{1 + x^{2}}$ holds.

Proof

1.1F3F11giveninductionalgebra

For $x = 0$ the series gives $e^{0} = 1 = U (0)$ . For $0 < x < K + 2$ , put $a_{j} = x^{j} / j!$ and $r = x / (K + 2) < 1$ . For every $j \geq K + 1$ , $a_{j + 1} / a_{j} = x / (j + 1) \leq r$ . Induction yields $a_{K + 1 + q} \leq a_{K + 1} r^{q}$ . Finite geometric sums and passage to the convergent series give $\sum_{j = K + 1}^{\infty} a_{j} \leq a_{K + 1} / (1 - r)$ . Adding the first $K + 1$ terms proves $e^{x} \leq U (x)$ for both actual scalar inputs. This uses the explicit exponential series in [F3], not an unproved algorithm property.

1.2L1algebra

Integrating [L1] gives a positive remainder and the partial sum $1 - \frac{1}{3} + \frac{1}{5} - \frac{1}{7} + \frac{1}{9} - \frac{1}{11} + \frac{1}{13} - \frac{1}{15} = (45045 - 15015 + 9009 - 6435 + 5005 - 4095 + 3465 - 3003) / 45045 = 33976 / 45045$ . Since $4 \cdot 33976 = 135904 > 135135 = 3 \cdot 45045$ , we have $π / 4 > 3 / 4$ , hence $π > 3$ and $1 / (2 π) < 1 / 6$ . Therefore $L_{Γ} ε M / (2 π) \leq ℓ ε M / 6$ whenever $L_{Γ} \leq ℓ$ .

1.3F1F2F3F9F10algebra

Let $B = 2^{- s} A$ . Since $d_{m} (ρ) > 0$ , [F3] makes $q_{m}$ nonzero throughout $∣ z ∣ \leq ρ$ , which contains $σ (B)$ by the caller's topological hypothesis. In a Jordan basis of $B$ , polynomial evaluation makes each block of $Q_{m} (B)$ upper triangular with diagonal $q_{m} (λ)$ , so $Q_{m} (B)$ is invertible. The polynomial $q_{m}$ has finitely many zeros and none in the closed disk by [F3]; hence some $η > 0$ makes $q_{m}$ nonzero on the open disk $D (0, ρ + η)$ , which contains both $Γ$ and $σ (B)$ . Thus $1 / q_{m}$ is holomorphic there. By the product rule [F9] applied to $q_{m} (1 / q_{m}) = 1$ , $Q_{m} (B) (1 / q_{m}) (B) = I$ , hence $(1 / q_{m}) (B) = Q_{m} (B)^{- 1}$ . Applying [F9] again to $r_{m} = p_{m} (1 / q_{m})$ from [F10] gives $r_{m} (B) = P_{m} (B) Q_{m} (B)^{- 1}$ . The polynomial matrices $P_{m} (B)$ and $Q_{m} (B)$ commute, so this is also $Q_{m} (B)^{- 1} P_{m} (B)$ . The exact solve from [F2] therefore makes the initial candidate ${\hat{X}}_{0} = r_{m} (B)$ .

2.1F7F8F11step 1.1givenalgebra

Put $X_{j} = \exp (2^{j} B)$ for $0 \leq j \leq s$ . The exponential semigroup law in [F8] gives $X_{j + 1} = X_{j}^{2}$ and $X_{s} = \exp (A)$ . The row-sum matrix norm is the operator norm induced by the vector infinity norm: the row triangle inequality gives the upper bound, and for a maximizing row choose each nonzero coordinate of $x$ to cancel the phase of that matrix entry, with arbitrary unit phases for zero entries; then $∥ x ∥_{\infty} = 1$ and that row attains its row sum. By [F7] and [F8], $∥ X_{j} ∥_{\infty, C} \leq e^{2^{j} ∥ B ∥_{\infty, C}} \leq e^{α} \leq U (α)$ by [F11], where $α \geq ∥ A ∥_{\infty, C}$ is the exact row bound used by the algorithm.

2.2F3F4F5F11step 1.1step 1.2step 1.3algebra

The scalar bound [F3] applies at every point of $Γ$ because its trace lies in $∣ z ∣ \leq ρ$ . Since $e^{ρ} \leq U (ρ)$ by [F11], it gives $\sup_{Γ} ∣ e^{z} - r_{m} (z) ∣ \leq ε$ with the $ε$ computed by the algorithm. The validator gives the resolvent bound $M$ by [F5]; applying [F4] and then step 1.2 gives $∥ {\hat{X}}_{0} - e^{B} ∥_{\infty, C} \leq \frac{L_{Γ}}{2 π} ε M \leq \frac{ℓ ε M}{6} = E_{0} .$

3.1F6F7step 2.2step 2.1algebra

For each returned square, the exact controller audit defines $D_{j} = {\hat{X}}_{j + 1} - {\hat{X}}_{j}^{2}$ . Since $∣ x + i y ∣ \leq ∣ x ∣ + ∣ y ∣$ , its row sums give $∥ D_{j} ∥_{\infty, C} \leq δ_{j}$ . If $∥ {\hat{X}}_{j} - X_{j} ∥_{\infty, C} \leq E_{j}$ , [F6] and step 2.1 imply $∥ {\hat{X}}_{j + 1} - X_{j + 1} ∥_{\infty, C} \leq (2 U (α) + E_{j}) E_{j} + δ_{j} = E_{j + 1} .$ Starting from step 2.2, induction proves this bound for every $j \leq s$ .

4.1step 2.1step 3.1∎

At $j = s$ , $X_{s} = \exp (A)$ by step 2.1, so step 3.1 gives $∥ {\hat{X}}_{s} - \exp (A) ∥_{\infty, C} \leq E_{s}$ , as claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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

Jan Zur, Matrix Functions, TU Berlin full lecture notes (standard reference, not scraped)
Awad H. Al-Mohy and Nicholas J. Higham, A New Scaling and Squaring Algorithm for the Matrix Exponential (standard reference, not scraped)