TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

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 Dirichlet series with absolute convergence on a right half-plane is determined there by its coefficients

Statement

Let $f, g : Z_{> 0} \to C$ be arithmetic functions. Suppose the Dirichlet series

$\sum_{n \geq 1} f (n) n^{- s}, \sum_{n \geq 1} g (n) n^{- s}$

both converge absolutely on some half-plane $ℜ s > σ$ , and agree there as functions. Then $f (n) = g (n)$ for every $n$ .

Facts & Assumptions

Given: Absolute convergence and equality of the two Dirichlet series on $ℜ s > σ$ .

[L1]

A Dirichlet series is a sum $\sum a_{n} n^{- s}$ (Dirichlet series).

Proof

technique · direct

1.1L1givenassume-contra

Subtract the two series. It is enough to prove that if $\sum_{n \geq 1} h (n) n^{- s} = 0$ for all $ℜ s > σ$ and the series converges absolutely there, then $h = 0$ . Assume otherwise and let $m$ be the least index with $h (m) \neq 0$ .

2.1step 1.1givenalgebra

For real $t > σ$ , multiply the zero identity by $m^{t}$ : $0 = h (m) + \sum_{n > m} h (n) {(\frac{m}{n})}^{t} .$ Because the original series converges absolutely at one fixed real point $t_{0} > σ$ , the tail is dominated by $\sum_{n > m} ∣ h (n) ∣ {(\frac{m}{n})}^{t_{0}},$ and for each $n > m$ the factor $(m / n)^{t}$ tends to $0$ as $t \to + \infty$ . Hence the tail tends to $0$ , so letting $t \to + \infty$ yields $0 = h (m)$ , contradiction.

3.1step 1.1step 2.1discharge-contradiction∎

Therefore no such least $m$ exists and all coefficients agree.

Depends on

Dirichlet series

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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

Jan-Hendrik Evertse, Analytic Number Theory, Theorem 2.1.6 (standard reference, not scraped)