Alphabeta Math
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.

Psi and theta differ by at most a square-root term

Statement

There are positive constants K1,K2 such that for every real x2,

0ψ(x)θ(x)K1xlogx

and, for all sufficiently large x,

ψ(x)θ(x)K2x.

Facts & Assumptions

Given: A real number x2.

[L1]

The prime-power expansion is ψ(x)=k1θ(x1/k) (Prime-power expansion of Chebyshev's psi function).

[L2]

Chebyshev's theta function has linear upper bounds for large arguments (Chebyshev's theta function has linear lower and upper bounds).

[L3]

By definition, θ(y)=pylogp and ψ(y)=nyΛ(n) (Chebyshev's theta function, Chebyshev's psi function).

Proof

technique · direct
1.1

Subtracting the k=1 term from [L1] gives ψ(x)θ(x)=k2θ(x1/k). Every summand is nonnegative, so 0ψ(x)θ(x).

L1L3givenalgebra
2.1

The k=2 term is θ(x)xlogx, because there are at most x primes at most x, and each contributes at most logxlogx. The terms with k>log2x vanish because x1/k<2. For 3klog2x, one has x1/kx1/3, so k=3log2xθ(x1/k)x1/3logxlog2xK1xlogx for a fixed constant K1, because (logx)x1/6 is bounded for x2. Together with step 1.1, this proves ψ(x)θ(x)K1xlogx for a suitable constant K1.

step 1.1givenalgebra
3.1

By [L2], choose C>0 and y02 such that θ(y)Cy for every yy0. Put C:=max{C,θ(y0)}. If 1yy0, monotonicity gives θ(y)θ(y0)CCy, while for yy0 one has θ(y)CyCy. Thus θ(y)Cy for every real y1. Then for all sufficiently large x, the term k=2 satisfies θ(x)Cx. Also, using the finite range from step 2.1, k=3log2xθ(x1/k)Cx1/3log2xCx for large x, because (logx)x1/60. Therefore ψ(x)θ(x)K2x for a suitable constant K2.

L2step 1.1step 2.1choosealgebra

Depends on

Used by

Dependency tree · two levels

13 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