TheoremStatement: 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 solvable Padé moment system gives the stated Taylor order

Statement

Let $m, n \geq 0$ , $R > 0$ , and $f (z) = \sum_{k = 0}^{\infty} c_{k} z^{k}$ for $∣ z ∣ < R$ , with the series convergent there. Suppose $q_{0} = 1, q_{1}, \dots, q_{n}$ solve the full normalized Padé moment equations of Exact Padé coefficient matching with defect statuses. Define $p_{k} = \sum_{j = 0}^{\min (k, n)} q_{j} c_{k - j}$ for $0 \leq k \leq m$ , and $p (z) = \sum_{k = 0}^{m} p_{k} z^{k}$ , $q (z) = \sum_{j = 0}^{n} q_{j} z^{j}$ . Then

f (z) - \frac{p (z)}{q (z)} = O (z^{m + n + 1}) as z \to 0.

This is a local Taylor-matching statement only; it gives no pole-location claim and no guarantee about analytic continuation beyond the neighborhood where $f$ is given.

Here $h (z) = O (z^{M})$ as $z \to 0$ means there are constants $C, δ > 0$ such that $∣ h (z) ∣ \leq C ∣ z ∣^{M}$ whenever $0 < ∣ z ∣ < δ$ .

Facts & Assumptions

Given: Integers $m, n \geq 0$ , a radius $R > 0$ , a convergent power series $f (z) = \sum_{k = 0}^{\infty} c_{k} z^{k}$ for $∣ z ∣ < R$ , and a normalized denominator solution $q_{0} = 1, q_{1}, \dots, q_{n}$ .

[F1]

Exact Padé coefficient matching with defect statuses: the moment equations make coefficients of $q f$ vanish in degrees $m + 1, \dots, m + n$ , while $p_{k}$ equals the coefficient of $q f$ for $0 \leq k \leq m$ .

[A1]

Since $q (0) = q_{0} = 1$ , continuity gives a neighborhood of $0$ on which $∣ q (z) ∣ \geq 1 / 2$ , so $1 / q$ is bounded there.

Proof

1.1givenF1algebra

Multiplication of the Taylor series of $f$ by $q$ gives coefficient $\sum_{j = 0}^{\min (k, n)} q_{j} c_{k - j}$ at degree $k$ . By [F1], for each $0 \leq k \leq m$ this coefficient is $p_{k}$ , so the coefficients of $q f - p$ through degree $m$ vanish.

2.1givenF1step 1.1algebra

For each $m < k \leq m + n$ , write $k = m + ℓ$ with $1 \leq ℓ \leq n$ . The moment equation in [F1] says $\sum_{j = 1}^{n} q_{j} c_{k - j} = - c_{k}$ , exactly the assertion that the degree- $k$ coefficient of $q f$ is zero, because $q_{0} = 1$ . Therefore every coefficient of $q f - p$ through degree $m + n$ vanishes.

3.1givenA1step 2.1algebra∎

Analyticity implies $q f - p$ has a Taylor expansion whose first possibly nonzero term has degree at least $m + n + 1$ , so $q f - p = O (z^{m + n + 1})$ . By [A1], divide by the nonvanishing $q$ near zero to obtain the asserted local order for $f - p / q$ . This proof uses only the solvable coefficient equations; it makes no claim about zeros of $q$ away from $0$ .

Depends on

Exact Padé coefficient matching with defect statuses

Used by

Padé matching can be singular or create a Froissart doublet Example

Dependency tree · one level

1 result within one dependency step 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

Pedro Gonnet, Stefan Güttel, and Lloyd N. Trefethen, Robust Padé Approximation via SVD, Section 2 (standard reference, not scraped)