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

Chebyshev's theta function has linear lower and upper bounds

Statement

There exist positive constants c<C and a real number x0 such that

cx≤θ(x)≤Cx

for every real x≥x0.

Facts & Assumptions

Given: A real number x≥2.

[L1]

The central binomial coefficient satisfies 4n2n+1≤(2nn)≤4n for every natural number n (Central binomial coefficient bounds).

[L2]

For every prime p and natural n≥1, primes p with n<p≤2n divide (2nn), and in general vp(2nn)≤log⁡(2n)log⁡p (Prime valuations in the central binomial coefficient).

[L5]

The logarithm satisfies log⁡(ab)=log⁡a+log⁡b and log⁡(4n)=2nlog⁡2 (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L6]

Induction on N is valid (The principle of mathematical induction).

Proof

technique · direct
1.1L3L4L6constructalgebra

Put P(y):=∏p≤yp for real y≥2. We claim that P(y)≤4y−1(y≥2). Let q be the largest prime with q≤y. Then P(y)=P(q) and 4q−1≤4y−1, so it suffices to prove the claim when y=q is prime. For q=2 this is immediate. Let q=2m+1 be an odd prime, and assume inductively that P(r)≤4r−1 for every integer r with 2≤r≤2m. Then P(q)=P(m+1)∏m+1<p≤2m+1p. Every prime in the second product divides (2m+1m)=(2m+1)!m!(m+1)! by [L4], because it appears in the numerator and in neither denominator factorial. Also [L3] gives ∑k=02m+1(2m+1k)=22m+1, and the two equal middle terms (2m+1m)=(2m+1m+1) therefore satisfy (2m+1m)≤22m. Thus P(q)≤P(m+1)(2m+1m)≤4m⋅22m=42m=4q−1. So the claim holds for every real y≥2.

1.2L2givenalgebra

Again by [L2], the factorization of (2nn) can be written as log⁡(2nn)≤θ(2n)+Rn, where Rn:=∑k=2⌊log⁡2(2n)⌋θ((2n)1/k). Using the trivial estimate θ(y)≤ylog⁡y on each layer and (2n)1/k≤2n for k≥2, we get 0≤Rn≤2n log⁡(2n) ⌊log⁡2(2n)⌋=o(n).

2.1step 1.1L5algebra

By definition of θ and the logarithm law in [L5], θ(y)=log⁡P(y)≤log⁡(4y−1)=2(y−1)log⁡2<2ylog⁡2 for every real y≥2.

2.2L1L5step 1.2choosealgebra

The lower bound in [L1] and [L5] give log⁡(2nn)≥2nlog⁡2−log⁡(2n+1). Combining this with step 1.2 shows θ(2n)≥2nlog⁡2−log⁡(2n+1)−Rn. Since log⁡(2n+1)+Rn=o(n), choose n0 so large that log⁡(2n+1)+Rn≤nlog⁡2 for every n≥n0. Then θ(2n)≥nlog⁡2(n≥n0).

3.1step 2.2step 2.1givenalgebra∎

Let x≥4n0, and put n=⌊x/2⌋. Then n≥n0 and 2n≤x, so by monotonicity of θ and step 2.2, θ(x)≥θ(2n)≥nlog⁡2≥log⁡24 x. Step 2.1 also gives θ(x)≤2xlog⁡2 for every x≥2. Thus the theorem holds with c=log⁡24, C=2log⁡2, and x0=4n0.

Depends on

Used by

Dependency tree · two levels

47 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