TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-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.

Pringsheim's theorem for power series with nonnegative coefficients

Statement

Let

$f (z) = \sum_{n \geq 0} a_{n} z^{n}$

have radius of convergence $R$ with $0 < R < \infty$ , and assume that every $a_{n} \geq 0$ is real. Then the boundary point $R$ is singular for the function element defined by $f$ on $D (0, R)$ .

Facts & Assumptions

Given: A power series $\sum_{n \geq 0} a_{n} z^{n}$ with radius $R \in (0, \infty)$ and nonnegative coefficients.

[L1]

Singular boundary points are those across which no holomorphic extension on a neighbourhood exists (Singular boundary points and natural boundaries of function elements).

[L2]

A holomorphic function equals its Taylor series throughout the largest centred disc contained in its domain (A holomorphic function equals its Taylor series throughout the largest centred disc in its domain).

[L3]

The radius of convergence is the one given by Cauchy-Hadamard (Cauchy-Hadamard for complex power series, including zero and infinite radius).

[L4]

A complex power-series sum has derivatives of every order, obtained by repeated termwise differentiation (A complex power-series sum has complex derivatives of every order, obtained by repeated termwise differentiation).

Proof

technique · direct

1.1

Replacing $z$ by $R z$ reduces the theorem to the case $R = 1$ : the rescaled series $\sum_{n \geq 0} a_{n} R^{n} z^{n}$ still has nonnegative coefficients, has radius $1$ by [L3], and $1$ is regular for it exactly when $R$ is regular for the original series.

L1L3algebra

1.2

Assume from now on that $R = 1$ , and suppose toward a contradiction that $1$ is regular. Then there is $ρ > 0$ and a holomorphic extension $F$ on $D (1, ρ)$ agreeing with the original series on $D (0, 1) \cap D (1, ρ)$ . By [L2], $F$ has a Taylor expansion $F (1 + h) = \sum_{m \geq 0} b_{m} h^{m} (∣ h ∣ < ρ) .$

L1L2assume-contra

2.1

Fix $m, N \in N$ and choose real $x$ with $\max {0, 1 - ρ} < x < 1$ , so $x$ lies in the overlap where both series represent $F$ . Applying [L4] to the original series about $0$ gives $\frac{F^{(m)} (x)}{m!} = \sum_{n \geq m} (\binom{n}{m}) a_{n} x^{n - m} \geq \sum_{n = m}^{N} (\binom{n}{m}) a_{n} x^{n - m},$ because every $a_{n} \geq 0$ . Applying [L4] to the Taylor series about $1$ shows that $F^{(m)} (x) \to m! b_{m}$ as $x \to 1^{-}$ . Letting $x \to 1^{-}$ therefore yields $b_{m} \geq \sum_{n = m}^{N} (\binom{n}{m}) a_{n} .$

L4step 1.2algebra

3.1

Choose $t$ with $0 < t < ρ$ and put $y : = 1 + t / 2 > 1$ . By step 1.2, $F (y) = \sum_{m \geq 0} b_{m} (t / 2)^{m} < \infty .$ For every $N$ , $\sum_{n = 0}^{N} a_{n} y^{n} = \sum_{n = 0}^{N} a_{n} \sum_{m = 0}^{n} (\binom{n}{m}) (t / 2)^{m} = \sum_{m = 0}^{N} (\sum_{n = m}^{N} (\binom{n}{m}) a_{n}) (t / 2)^{m} \leq \sum_{m = 0}^{N} b_{m} (t / 2)^{m} \leq F (y),$ where the inequality is step 2.1. Since the left-hand partial sums are nondecreasing, letting $N \to \infty$ gives $\sum_{n \geq 0} a_{n} y^{n} \leq F (y) < \infty$ .

step 1.2step 2.1algebra

4.1

Step 3.1 says that the original power series converges at the real point $y > 1$ , contradicting [L3] because the radius in the reduced case is $1$ . Therefore $1$ is singular, and undoing the rescaling proves that the point $R$ is singular for the original series.

L3step 1.1step 3.1discharge-contradiction∎

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

Philippe Flajolet, Symbolic Enumerative Combinatorics and Complex Asymptotic Analysis, Theorem 4 (standard reference, not scraped)
Henry Wilton, Riemann Surfaces lecture notes, §2.1 (standard reference, not scraped)