LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

A finite scalar remainder bound for the diagonal Padé exponential

Statement

For $m \geq 0$ and $ρ \geq 0$ , put $d_{m} (ρ) : = 1 - \sum_{j = 1}^{m} a_{m, j} ρ^{j},$ with the empty sum equal to zero and $a_{m, j}$ as in Diagonal Padé approximant to the exponential. If $d_{m} (ρ) > 0$ , then $q_{m}$ has no zero in $∣ z ∣ \leq ρ$ and, for every such $z$ , $∣ e^{z} - r_{m} (z) ∣ \leq \frac{ρ^{2 m + 1} e^{ρ} (m!)^{2}}{(2 m)! (2 m + 1)! d_{m} (ρ)} .$ This is a finite-order bound; it makes no adaptive choice of $m$ or scaling.

Facts & Assumptions

Given: An integer $m \geq 0$ , a radius $ρ \geq 0$ with $d_{m} (ρ) > 0$ , and a complex number $z$ with $∣ z ∣ \leq ρ$ .

[F1]

The Padé numerator and denominator coefficients are $a_{m, j} = (2 m - j)! m! / ((2 m)! j! (m - j)!)$ and $q_{m} (z) = p_{m} (- z)$ (Diagonal Padé approximant to the exponential).

[F2]

The scalar exponential is its everywhere absolutely convergent series (The complex exponential by its power series); the bounded-operator exponential lemma includes absolute convergence of the same series when the operator is multiplication by a scalar (The exponential series of a bounded operator).

Proof

1.1F1F2algebra

Set $g_{m} (t) = t^{m} (1 - t)^{m}$ . For real $h \neq 0$ and fixed $t, z$ , the power series in [F2] gives $\frac{e^{(t + h) z} - e^{t z}}{h} = \sum_{n \geq 1} \frac{z^{n}}{n!} \sum_{ℓ = 0}^{n - 1} (t + h)^{n - 1 - ℓ} t^{ℓ}$ . For $∣ h ∣ \leq 1$ , the inner sum is bounded by $n (∣ t ∣ + 1)^{n - 1}$ , so the summable majorant $\sum_{n \geq 1} n ∣ z ∣^{n} (∣ t ∣ + 1)^{n - 1} / n!$ makes the tails uniform in $h$ ; termwise limits of finite partial sums then give $\frac{d}{d t} e^{t z} = z e^{t z}$ . For $z \neq 0$ , integration by parts $2 m + 1$ times, using $g_{m}^{(2 m + 1)} = 0$ , gives $\int_{0}^{1} e^{t z} g_{m} (t) d t = {[e^{t z} \sum_{k = 0}^{2 m} \frac{(- 1)^{k} g_{m}^{(k)} (t)}{z^{k + 1}}]}_{t = 0}^{t = 1} .$ For $k < m$ , both endpoint derivatives vanish. For $k = m + ℓ$ with $0 \leq ℓ \leq m$ , expansion of $t^{m} (1 - t)^{m}$ at the endpoints gives $g_{m}^{(k)} (1) = (- 1)^{m} (\binom{m}{ℓ}) (m + ℓ)!$ and $g_{m}^{(k)} (0) = (- 1)^{ℓ} (\binom{m}{ℓ}) (m + ℓ)!$ . After multiplication by $(- 1)^{m} z^{2 m + 1} / (2 m)!$ , the coefficient of $e^{z} z^{m - ℓ}$ is $(- 1)^{m - ℓ} (\binom{m}{ℓ}) (m + ℓ)! / (2 m)! = (- 1)^{m - ℓ} a_{m, m - ℓ}$ , and the coefficient of $z^{m - ℓ}$ without $e^{z}$ is $- (\binom{m}{ℓ}) (m + ℓ)! / (2 m)! = - a_{m, m - ℓ}$ . These are exactly the coefficients of $q_{m} (z) e^{z} - p_{m} (z)$ , so collecting the powers gives $q_{m} (z) e^{z} - p_{m} (z) = \frac{(- 1)^{m} z^{2 m + 1}}{(2 m)!} \int_{0}^{1} e^{t z} t^{m} (1 - t)^{m} d t .$ Both sides are continuous at $z = 0$ , so the identity holds there as well.

2.1givenstep 1.1algebra

By the triangle inequality, $∣ q_{m} (z) ∣ = ∣ p_{m} (- z) ∣ \geq 1 - \sum_{j = 1}^{m} a_{m, j} ∣ z ∣^{j} \geq d_{m} (ρ) > 0$ . Thus $q_{m}$ has no zero in the disk. Also $\int_{0}^{1} t^{m} (1 - t)^{m} d t = \frac{(m!)^{2}}{(2 m + 1)!},$ as follows by integrating by parts $m$ times and then integrating $(1 - t)^{2 m}$ . Hence $∣ \int_{0}^{1} e^{t z} t^{m} (1 - t)^{m} d t ∣ \leq e^{ρ} (m!)^{2} / (2 m + 1)!$ .

3.1step 1.1step 2.1algebra∎

Divide the identity in step 1.1 by the nonzero $q_{m} (z)$ from step 2.1 and use $∣ z ∣^{2 m + 1} \leq ρ^{2 m + 1}$ . This gives the stated remainder bound.

Depends on

Used by

Dependency tree · two levels

21 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)