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.

A power series, its formal derivative, and its zero-constant-term formal antiderivative have the same radius of convergence

Statement

For a power series $\sum_{n \geq 0} a_{n} (x - c)^{n}$ , define its formal derivative and its zero-constant-term formal antiderivative by

$\sum_{n \geq 0} ι (n + 1) a_{n + 1} (x - c)^{n}, \sum_{n \geq 0} \frac{a_{n}}{ι (n + 1)} (x - c)^{n + 1},$

where $ι (n + 1) > 0$ is the canonical natural in $R$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing). All three power series have the same radius of convergence.

Facts & Assumptions

Given: The three formal power series in the statement, centred at the same real $c$ .

[L1]

For $0 \leq q < 1$ , the geometric series $\sum q^{n}$ converges. Its terms are nonnegative, so $∣ q^{n} ∣ = q^{n}$ and the convergence is absolute (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges, Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Basic properties of the absolute value).

[L2]

The Cauchy product of two absolutely convergent series converges absolutely; applying this to two copies of $\sum q^{n}$ shows that $\sum_{n \geq 0} ι (n + 1) q^{n}$ converges (If $\sum a_{k}$ and $\sum b_{k}$ both converge absolutely then their Cauchy product converges absolutely, with sum $A B$ ).

[L3]

The terms of a convergent series tend to $0$ (If a series converges then its terms tend to $0$ ), a convergent sequence is bounded (Every convergent sequence is bounded), and direct comparison preserves convergence of nonnegative series (If $0 \leq a_{k} \leq b_{k}$ eventually, convergence of $\sum b_{k}$ gives convergence of $\sum a_{k}$ , and divergence of $\sum a_{k}$ gives divergence of $\sum b_{k}$ ).

[L4]

The canonical naturals $ι (n + 1)$ are positive and at least $1$ (Canonical naturals are positive and strictly increasing).

Proof

technique · direct

1.1L1L2L3choose

Fix distances $0 \leq r < s$ and put $q = r / s$ when $s > 0$ . By [L2], the series with nonnegative terms $ι (n + 1) q^{n}$ converges. Its terms tend to $0$ and hence form a bounded sequence by [L3], say with bound $M$ .

1.2L3L4algebra

Conversely, if the derivative series converges absolutely at a distance $s > 0$ , then $∣ a_{n + 1} ∣ s^{n + 1} \leq s ι (n + 1) ∣ a_{n + 1} ∣ s^{n}$ because $ι (n + 1) \geq 1$ . Comparison gives absolute convergence of the original series there, after adjoining its first term.

1.3L3L4algebra

If the original series converges absolutely at distance $s > 0$ , then the antiderivative terms satisfy $∣ a_{n} ∣ s^{n + 1} / ι (n + 1) \leq s ∣ a_{n} ∣ s^{n}$ , so the antiderivative converges absolutely at $s$ .

2.1step 1.1L3

Suppose the original series converges absolutely at distance $s > 0$ . Its shifted absolute terms $u_{n} : = ∣ a_{n + 1} ∣ s^{n + 1}$ form a convergent series. At distance $r < s$ , the derivative's absolute terms satisfy $ι (n + 1) ∣ a_{n + 1} ∣ r^{n} = s^{- 1} ι (n + 1) q^{n} u_{n} \leq (M / s) u_{n}$ , so the derivative series converges absolutely there by [L3].

2.2step 1.1L3

Conversely, if the antiderivative converges absolutely at distance $s > 0$ , put $v_{n} : = ∣ a_{n} ∣ s^{n + 1} / ι (n + 1)$ . At every $r < s$ , $∣ a_{n} ∣ r^{n} = s^{- 1} ι (n + 1) q^{n} v_{n} \leq (M / s) v_{n}$ , so the original series converges absolutely at $r$ by [L3].

3.1givenstep 2.1step 1.2step 1.3step 2.2L3∎

Write $R_{0}, R_{D}, R_{I}$ for the three radii. If $0 \leq r < R_{0}$ , the supremum definition supplies an admissible distance $s > r$ for the original series; choosing $u$ with $r < u < s$ , the original series is absolutely convergent at $u$ , and step 2.1 makes the derivative absolutely convergent at every distance below $r$ . Thus $r$ is admissible for the derivative and $R_{0} \leq R_{D}$ . Conversely, if $0 \leq r < R_{D}$ , choose an admissible derivative distance $s > r$ and then $u$ with $r < u < s$ . The derivative converges absolutely at $u$ , so step 1.2 and direct comparison make the original series absolutely convergent at every distance below $r$ ; hence $R_{D} \leq R_{0}$ . The same argument with steps 1.3 and 2.2 gives $R_{0} = R_{I}$ . Therefore all three extended radii are equal, including $0$ and $+ \infty$ .

A power series, its formal derivative, and its zero-constant-term formal antiderivative have the same radius of convergence

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources