LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

The binomial double series for re-expanding a complex power series is absolutely convergent and may be regrouped

Statement

Let $\sum c_{n} (z - a)^{n}$ have radius $R$ . If $∣ b - a ∣ + ∣ h ∣ < R$ , then $\sum_{n \geq 0} \sum_{k = 0}^{n} (\binom{n}{k}) ∣ c_{n} ∣ ∣ b - a ∣^{n - k} ∣ h ∣^{k} < \infty,$ and the complex binomial double series may be regrouped by powers of $h$ .

Facts & Assumptions

Given: A complex power series and points $b, h$ satisfying $∣ b - a ∣ + ∣ h ∣ < R$ .

[L1]

The corresponding nonnegative real binomial double series converges and licenses regrouping (The binomial double series used to re-expand a power series at an interior point is absolutely convergent and may be regrouped).

[L2]

For complex $z, w$ and $n \in N$ , $(z + w)^{n} = \sum_{k \leq n} (\binom{n}{k}) z^{k} w^{n - k}$ (The binomial theorem over the complex field).

[L3]

Every absolutely convergent complex series converges, and every rearrangement has the same sum (Every absolutely convergent complex series converges, and rearrangements preserve its sum).

Proof

technique · direct

1.1

Apply [L1] to the real coefficient sequence $∣ c_{n} ∣$ and the nonnegative numbers $∣ b - a ∣, ∣ h ∣$ ; this gives the displayed finite total majorant.

2.1

By [L2], $c_{n} ((b - a) + h)^{n}$ is the finite sum over $k \leq n$ of the corresponding complex terms, each bounded by the majorant term in step 1.1.

step 1.1L2

3.1

Absolute convergence now permits regrouping by $k$ under [L3]. The cases $h = 0$ and $b = a$ merely make some terms vanish and are included.

step 1.1step 2.1L3∎

Depends on

Used by

A complex power-series sum re-expands about every interior point, at least to the distance from that point to the original boundary Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 85 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Power-series re-expansion notes, Colby College (standard reference, not scraped)