Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31
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 power-series sum may be re-expanded about every interior point, with coefficients given by its derivatives there

Statement

Suppose f(x)=∑n≥0an(x−c)n has radius R, and let d satisfy ∣d−c∣<R. Then for every real x with

∣d−c∣+∣x−d∣<R

one has

f(x)=∑k=0∞f(k)(d)ι(k!)(x−d)k.

Thus the sum may be re-expanded about every interior point.

Facts & Assumptions

Given: The series for f and the interior point d.

[L1]

The binomial double series is absolutely convergent when ∣d−c∣+∣x−d∣<R and may be regrouped by powers of x−d (The binomial double series used to re-expand a power series at an interior point is absolutely convergent and may be regrouped).

[L2]

Repeated termwise differentiation gives f(k)(d)=∑n≥kι(nk‾)an(d−c)n−k (A power-series sum is infinitely differentiable inside its radius and satisfies an=f(n)(c)/ι(n!) at its centre).

Proof

technique · direct
1.1

Fix x satisfying the stated inequality and set h:=x−d. By [L1], f(x)=∑k≥0bkhk, where bk:=∑n≥kι ⁣(nk)an(d−c)n−k.

givenL1
2.1

By [L2] and [L3], ι(k!)bk=f(k)(d) for every k.

step 1.1L2L3algebra
3.1

Substituting the coefficient identity from step 2.1 into the series in step 1.1 proves the formula.

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · two levels

28 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