Breusch's theorem from the upper bound to Breusch's theorem on primes between \(x\) and \(9x/8\)

TheoremBreusch's theorem from the upper bound#✓fully proved

For a natural number \(n\) write \(L(n) = \sum_{m \mid 210} \mu(m) \log \binom{2100n/m}{210n/m}\), where \(\mu\) is the Möbius function. Let \(x \ge 48\) be a real number, and suppose that every natural number \(n \ge 1\) such that no prime \(p\) satisfies \(1890n < p \le 2100n\) also satisfies \(L(n) \le \left(\frac{18900}{279} + \frac{18900}{657} + \frac{18900}{963}\right) n \log 3.4 + \sqrt{2100n}\,\log(2100n)\). Then there is a prime \(p\) with \(x < p < \frac{9}{8}x\).

theorem breusch_prime_interval_of_upper (x : ℝ) (hx : 48 ≤ x)
    (hU : ∀ n : ℕ, 1 ≤ n →
      (∀ p : ℕ, p.Prime → 1890 * n < p → p ≤ 2100 * n → False) → UpperIneq n) :
    ∃ p : ℕ, p.Prime ∧ (x : ℝ) < (p : ℝ) ∧ (p : ℝ) < (9 / 8 : ℝ) * x

Uses 3 · Used by 1

Statement usesBreusch's endgame upper-bound inequality

Proof usesPrimes in \((X, 9X/8)\) for large \(X\), assuming the upper bound · Primes in \((X, 9X/8)\) for \(53 \le X < 9820997\)

Used byBreusch's theorem on primes between \(x\) and \(9x/8\)

TheoremBreusch's theorem on primes between \(x\) and \(9x/8\)#✓fully proved

For every real number \(x \ge 48\) there is a prime \(p\) with \(x < p < \frac{9}{8}x\).

theorem breusch_prime_interval : ∀ x : ℝ, 48 ≤ x →
    ∃ p : ℕ, p.Prime ∧ x < (p : ℝ) ∧ (p : ℝ) < (9 / 8 : ℝ) * x

Sources

• R. Breusch, Zur Verallgemeinerung des Bertrandschen Postulates, Math. Z. 34 (1932), 505–526, conclusion on p. 515.

Uses 2 · Used by 1

Proof usesBreusch's theorem from the upper bound · Upper bound for \(\log F_9(n)\) when \((1890n, 2100n)\) has no prime

Used byRamanujan's two-primes refinement of Bertrand's postulate

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.