Prime gaps and primes in short intervals

Bertrand-type and Breusch theorems, Ramanujan primes, prime gaps, bounded gaps, Sylvester–Schur on prime factors of consecutive products.

TheoremDusart's short-interval prime gap bound#●ready to prove

Let \(\log\) be the natural logarithm. For every real number \(x \ge 468991632\) there is a prime \(p\) with \(x < p \le x + \frac{x}{5000 (\log x)^2}\).

theorem_wanted dusart_prime_gap (x : ℝ) (hx : 468991632 ≤ x) :
    ∃ p : ℕ, p.Prime ∧ x < (p : ℝ)
      ∧ (p : ℝ) ≤ x + x / (5000 * (Real.log x) ^ 2)

Sources

Pierre Dusart, Explicit estimates of some functions over primes, Ramanujan J. 45(1) (2018), 227–251, https://doi.org/10.1007/s11139-016-9839-4, Corollary 5.5.

TheoremRamanujan's two-primes refinement of Bertrand's postulate#✓fully proved

For every natural number \(n \ge 6\) there are primes \(p\) and \(q\) with \(n < p < q < 2n\); that is, the open interval \((n, 2n)\) contains two distinct primes.

For \(n \ge 48\) this follows from Breusch's theorem applied at \(n\) and at \(9n/8\); the remaining finitely many cases are checked by direct computation.

theorem ramanujan_two_primes_between (n : ℕ) (hn : 6 ≤ n) :
    ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ n < p ∧ p < q ∧ q < 2 * n

Sources

Nathaniel Benjamin, Grant Fickes, Eugene Fiorini, Edgar Jaramillo Rodriguez, Eric Jovinelly, and Tony W. H. Wong, "Primes and Perfect Powers in the Catalan Triangle", Journal of Integer Sequences 22 (2019), Article 19.7.6, proof sentence at line 153 (inside the proof of the theorem labeled c_nn not power), attributed there to Ramanujan, https://cs.uwaterloo.ca/journals/JIS/VOL22/Fiorini/fiorini3.tex.

Uses 1

Proof usesBreusch's theorem on primes between \(x\) and \(9x/8\)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.