LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 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.

The summatory logarithm is x log x minus x plus O(log x)

Statement

For every real $x \geq 1$ ,

\sum_{n \leq x} \log n = x \log x - x + O (\log x) .

Facts & Assumptions

Given: A real $x \geq 1$ and $N : = ⌊ x ⌋$ .

Proof

technique · direct

1.1

The function $\log$ of The natural logarithm as the inverse of the exponential function is increasing on $(0, \infty)$ by The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, so monotonicity of the integral gives $\int_{1}^{N} \log t d t \leq \sum_{n = 1}^{N} \log n \leq \int_{1}^{N + 1} \log t d t .$

givenalgebra

2.1

By Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ and The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, the function $G (t) : = t \log t - t$ satisfies $G^{'} (t) = \log t + t \cdot \frac{1}{t} - 1 = \log t$ for every $t > 0$ . Therefore The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ yields $\int_{1}^{Y} \log t d t = Y \log Y - Y + 1$ for every $Y \geq 1$ . Applying this with $Y = N$ and $Y = N + 1$ in step 1.1 gives $\sum_{n = 1}^{N} \log n = N \log N - N + O (\log N) .$

step 1.1givenalgebra

3.1

Since $N \leq x < N + 1$ , one has $N = x + O (1)$ and therefore $N \log N = x \log x + O (\log x)$ . Substituting this into step 2.1 and using $\sum_{n \leq x} \log n = \sum_{n = 1}^{N} \log n$ proves $\sum_{n \leq x} \log n = x \log x - x + O (\log x) .$

step 2.1givenalgebra∎

Depends on

Used by

The average order of tau is log n Corollary

Dependency tree · two levels

37 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)