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.

Dirichlet's hyperbola method for summatory convolutions

Statement

Let $f, g$ be arithmetic functions with summatory functions $F (y) = \sum_{n \leq y} f (n)$ and $G (y) = \sum_{n \leq y} g (n)$ (Summatory functions and average orders). If $x \geq 1$ and $U, V \geq 1$ satisfy $U V = x$ , then

\sum_{n \leq x} (f * g) (n) = \sum_{a \leq U} f (a) G (x / a) + \sum_{b \leq V} g (b) F (x / b) - F (U) G (V) .

Facts & Assumptions

Given: Arithmetic functions $f, g$ , a real $x \geq 1$ , and reals $U, V \geq 1$ with $U V = x$ .

Proof

technique · direct

1.1

By Dirichlet convolution of arithmetic functions, $\sum_{n \leq x} (f * g) (n) = \sum_{n \leq x} \sum_{d ∣ n} f (d) g (n / d) = \sum_{a b \leq x} f (a) g (b),$ where the last equality is the finite reindexing of Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule.

givenalgebra

2.1

Every lattice point $(a, b)$ with $a b \leq x = U V$ lies in at least one of the regions $a \leq U$ or $b \leq V$ , for otherwise $a > U$ and $b > V$ would give $a b > U V = x$ . Therefore $\sum_{a b \leq x} f (a) g (b) = \sum_{\begin{array}{c} a b \leq x \\ a \leq U \end{array}} f (a) g (b) + \sum_{\begin{array}{c} a b \leq x \\ b \leq V \end{array}} f (a) g (b) - \sum_{\begin{array}{c} a \leq U \\ b \leq V \end{array}} f (a) g (b) .$

step 1.1givenalgebra

3.1

For fixed $a \leq U$ , the inner sum over $b$ is exactly $G (x / a)$ , and for fixed $b \leq V$ the inner sum over $a$ is exactly $F (x / b)$ . The overlap sum factors as $(\sum_{a \leq U} f (a)) (\sum_{b \leq V} g (b)) = F (U) G (V) .$ Substituting these identities into step 2.1 gives the claimed formula.

step 2.1givenalgebra∎

Depends on

Used by

Dependency tree · two levels

11 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

Tom Sanders, Topics in Analytic Number Theory, Chapter 1 (standard reference, not scraped)
Karl-Dieter Crisman, Number Theory: In Context and Interactive (standard reference, not scraped)