Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck 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.

The binomial double series used to re-expand a power series at an interior point is absolutely convergent and may be regrouped

Statement

Let ∑n≥0an(x−c)n have radius R, let d satisfy ∣d−c∣<R, and let h satisfy ∣d−c∣+∣h∣<R. Then

∑n=0∞∑k=0nι ⁣(nk)∣an∣ ∣d−c∣n−k∣h∣k<∞.

Consequently the binomial double series is absolutely convergent and may be regrouped by powers of h:

∑n=0∞an(d+h−c)n=∑k=0∞(∑n=k∞ι ⁣(nk)an(d−c)n−k)hk.

Facts & Assumptions

Given: The power series and points c,d,d+h from the statement.

[L2]

The binomial theorem gives ∑k=0nι ⁣(nk)un−kvk=(u+v)n for all real u,v (The binomial theorem in R: (x+y)n=∑k<n+1ι ⁣(nk) xky n−k).

Proof

technique · direct
1.1

Put ρ:=∣d−c∣+∣h∣<R. By [L2], the sum of the absolute values in row n is ∣an∣ρn.

givenL2algebra
2.1

The series ∑n∣an∣ρn converges by [L1], so the triangular double series is absolutely convergent.

step 1.1L1
3.1

Apply the binomial theorem before summing and [L3] to regroup the absolutely convergent double series by k. This yields the displayed identity.

step 2.1L2L3∎

Depends on

Used by

Dependency tree · two levels

36 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