LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01

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.

Prime-power expansion of Chebyshev's psi function

Statement

For every real $x \geq 1$ ,

ψ (x) = \sum_{p^{k} \leq x} \log p = \sum_{k \geq 1} θ (x^{1 / k}),

and both sums are finite.

Facts & Assumptions

Given: A real number $x \geq 1$ .

[L1]

The von Mangoldt function satisfies $Λ (n) = \log p$ when $n = p^{k}$ is a prime power and $Λ (n) = 0$ otherwise (The von Mangoldt function).

[L2]

By definition,

ψ (x) = \sum_{n \leq x} Λ (n)

(Chebyshev's psi function).

[L3]

By definition,

θ (y) = \sum_{p \leq y} \log p

for every real $y \geq 2$ (Chebyshev's theta function).

Proof

technique · direct

1.1

Only prime powers contribute to the sum in [L2], by [L1]. Therefore $ψ (x) = \sum_{p^{k} \leq x} \log p,$ where the sum ranges over all prime powers at most $x$ .

L1L2given

2.1

The displayed prime-power sum is finite: if $p^{k} \leq x$ , then already $2^{k} \leq p^{k} \leq x$ , so $k \leq \log_{2} x$ ; and for each fixed $k$ , only the primes $p \leq x^{1 / k}$ occur.

step 1.1givenalgebra

3.1

Fix $k \geq 1$ . The contribution of the $k$ th prime-power layer is $\sum_{p^{k} \leq x} \log p = \sum_{p \leq x^{1 / k}} \log p = θ (x^{1 / k}),$ by [L3]. Summing these finitely many layers from step 2.1 gives $\sum_{p^{k} \leq x} \log p = \sum_{k \geq 1} θ (x^{1 / k}) .$

L3step 2.1algebra

4.1

Combining steps 1.1 and 3.1 proves both displayed identities.

step 1.1step 3.1∎

Depends on

Used by

Dependency tree · two levels

7 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

Victor Shoup, A Computational Introduction to Number Theory and Algebra, Version 2 (standard reference, not scraped)