Explicit prime counts in a window of ratio two

For every real x ≥ 4, the half-open window [x/2, x) contains at least c * x / log x primes for one universal positive constant c. The proof counts prime factors of a central binomial coefficient, so no prime-number-theorem hypothesis is assumed.

Main results

• Nat.exists_prime_half_le_and_lt: a prime exists in every such window.
• Nat.exists_forall_mul_div_log_le_card_primes: the uniform counting bound.
• Nat.exists_forall_mul_sqrt_div_log_le_card_primes: the bound at x = sqrt D, for all D ≥ 16.

References

Adapted from Anthropic's PrimesInWindow.lean. Its central-binomial and concavity estimates adapt Mathlib/NumberTheory/Bertrand.lean, originally by Patrick Stevens and Bolton Bailey; that source credit is retained.

1. Erdős's upper bound for the central binomial coefficient

2. The elementary estimate n^6 · (2n)^(6√(2n)) ≤ 2^n for n ≥ 16562

3. The count for n ≥ 16562

4. Half-open windows [x/2, x) with real endpoints

theorem Nat.exists_prime_half_le_and_lt (x : ℝ) (hx : 4 ≤ x) : ∃ (p : ℕ), Prime p ∧ x / 2 ≤ ↑p ∧ ↑p < x

For every real x ≥ 4 there is a prime p with x/2 ≤ p < x, by Bertrand's postulate.

theorem Nat.exists_forall_mul_div_log_le_card_primes : ∃ (c : ℝ), 0 < c ∧ ∀ (x : ℝ), 4 ≤ x → ∀ (S : Finset ℕ), (∀ (p : ℕ), Prime p → x / 2 ≤ ↑p → ↑p < x → p ∈ S) → c * (x / Real.log x) ≤ ↑S.card

There is a c > 0 such that, for every real x ≥ 4, every finite set of natural numbers that contains all primes p with x/2 ≤ p < x has at least c · x / log x elements. (This form applies to the set of those primes however it is written down.)

5. The window [√D/2, √D) used in the modular reduction

theorem Nat.exists_forall_mul_sqrt_div_log_le_card_primes : ∃ (c : ℝ), 0 < c ∧ ∀ (D : ℕ), 16 ≤ D → ∀ (S : Finset ℕ), (∀ (p : ℕ), Prime p → √↑D / 2 ≤ ↑p → ↑p < √↑D → p ∈ S) → c * (√↑D / Real.log ↑D) ≤ ↑S.card

There is a c > 0 such that, for every natural number D ≥ 16, every finite set of natural numbers that contains all primes p with √D/2 ≤ p < √D has at least c · √D / log D elements.