Chebyshev-type bound for the sum of prime logarithms to Primes in \((X, 9X/8)\) for large \(X\), assuming the upper bound

LemmaChebyshev-type bound for the sum of prime logarithms#✓fully proved

For every real number \(Y \ge 0\), the sum of \(\log p\) over all primes \(p \le \lfloor Y \rfloor\) is at most \(Y \log 3.4\).

lemma U9_theta_le (Y : ℝ) (hY : 0 ≤ Y) :
    ∑ p ∈ Nat.primesBelow (⌊Y⌋₊ + 1), Real.log ((p : ℕ) : ℝ)
      ≤ Y * Real.log 3.4

Uses 2 · Used by 1

Proof usesThe primorial as a product of primes · Primorial bound by powers of 3.4, real form

Used byPrime-logarithm bound for one level of \(G\)

LemmaPrime-logarithm bound for one level of \(G\)#✓fully proved

For real \(x \ge 0\) let \(G(x) = \sum_{m \mid 210} \mu(m) (\lfloor 2100x/m \rfloor - \lfloor 1890x/m \rfloor - \lfloor 210x/m \rfloor)\), where \(\mu\) is the Möbius function. Let \(n \ge 1\) be a natural number, let \(B\) be a finite set of primes \(p\) with \(p \le 1890n\), let \(i \ge 1\) be a natural number, and let \(j \ge 1\) be a real number with \(18900n/j \ge 0\). Suppose that every prime \(p \le 1890n\) with \(G(n/p) \ge i\) satisfies \(p \le 18900n/j\). Then the sum of \(\log p\) over the \(p \in B\) with \(\max(G(n/p), 0) \ge i\) is at most \((18900n/j) \log 3.4\).

lemma U9_Bi_le (n : ℕ) (_hn : 1 ≤ n) (B : Finset ℕ)
    (hBmem : ∀ p ∈ B, p.Prime ∧ p ≤ 1890 * n)
    (i : ℕ) (hi : 1 ≤ i) (jm : ℝ) (_hjm : 1 ≤ jm)
    (hle_i : ∀ p : ℕ, p.Prime → p ≤ 1890 * n → (i : ℤ) ≤ G9r ((n : ℝ) / ((p : ℕ) : ℝ)) →
      ((p : ℕ) : ℝ) ≤ 18900 * (n : ℝ) / jm)
    (hYnn : 0 ≤ 18900 * (n : ℝ) / jm) :
    ∑ p ∈ B.filter (fun p => i ≤ (G9r ((n : ℝ) / ((p : ℕ) : ℝ))).toNat),
        Real.log ((p : ℕ) : ℝ)
      ≤ 18900 * (n : ℝ) / jm * Real.log 3.4

Uses 4 · Used by 1

Statement usesContinuous Breusch function

Proof usesLogarithms of primes are nonnegative · Positive lower bounds on a truncation lift to the integer · Chebyshev-type bound for the sum of prime logarithms

Used byContribution of primes with \(p^2 > 2100n\)

LemmaContribution of primes with \(p^2 > 2100n\)#✓fully proved

Write \(v_p(m)\) for the exponent of \(p\) in \(m\) and \(\mu\) for the Möbius function, and set \(\nu_p(n) = \sum_{d \mid 210} \mu(d)\bigl(v_p((2100n/d)!) - v_p((1890n/d)!) - v_p((210n/d)!)\bigr)\). For every natural number \(n \ge 1\), the sum of \(\nu_p(n) \log p\) over the primes \(p \le 1890n\) with \(p^2 > 2100n\) satisfies

\[ \sum_{\substack{p \le 1890n \text{ prime} \\ p^2 > 2100n}} \nu_p(n) \log p \le \left(\frac{18900}{279} + \frac{18900}{657} + \frac{18900}{963}\right) n \log 3.4. \]

lemma U9_B_le (n : ℕ) (hn : 1 ≤ n) :
    ∑ p ∈ ((Nat.primesBelow (2100 * n + 1)).filter (fun p => p ≤ 1890 * n)).filter
      (fun p => 2100 * n < p ^ 2),
      ((nu9 p n : ℤ) : ℝ) * Real.log ((p : ℕ) : ℝ)
    ≤ (18900 / 279 + 18900 / 657 + 18900 / 963 : ℝ) * (n : ℝ) * Real.log 3.4

Uses 13 · Used by 1

Statement usesThe \(p\)-adic valuation of the weighted product

Proof usesContinuous Breusch function · The modulus \(Q_9 = 210\) · Value of \(10Qn\) · Prime-logarithm bound for one level of \(G\) · \(G\) is at most its positive part · Layer-cake decomposition with three levels · Logarithms of primes are nonnegative · Upper bound for primes where a Möbius-weighted floor sum is at least 1 · Upper bound for primes where a Möbius-weighted floor sum is at least 2 · Upper bound for primes where a Möbius-weighted floor sum is at least 3 · The truncated continuous Breusch function is at most 3 · Single-term valuation identity for large primes

Used byUpper bound for \(\log F_9(n)\) when \((1890n, 2100n)\) has no prime

LemmaBound for one small-square prime term#✓fully proved

Let \(n \ge 1\) be a natural number and let \(p\) be a prime with \(p^2 \le 2100n\). For each divisor \(m\) of \(210\) put \(N_m = 210n/m\), let \(\mu\) be the Möbius function and \(v_p\) the \(p\)-adic valuation, and put \(\nu_9(p, n) = \sum_{m \mid 210} \mu(m) (v_p((10N_m)!) - v_p((9N_m)!) - v_p(N_m!))\). Then \(\nu_9(p, n) \log p \le 3 \log(2100n)\).

lemma U9_Cterm_le (n p : ℕ) (hn : 1 ≤ n) (hp : p.Prime)
    (_hleX : p ^ 2 ≤ 2100 * n) :
    ((nu9 p n : ℤ) : ℝ) * Real.log ((p : ℕ) : ℝ)
      ≤ 3 * Real.log (((2100 * n : ℕ)) : ℝ)

Uses 8 · Used by 1

Statement usesThe \(p\)-adic valuation of the weighted product

Proof usesContinuous Breusch function · The continuous Breusch function is at most 3 · The continuous Breusch function vanishes at small ratios · The modulus \(Q_9 = 210\) · Value of \(10Qn\) · Logarithms of primes are nonnegative · Valuation identity for the weighted product

Used byContribution of the small-square primes

LemmaCounting small-square primes#✓fully proved

Let \(n \ge 1\) be a natural number and let \(C\) be a finite set of primes \(p\) with \(p^2 \le 2100n\). Then \(C\) has at most \(\sqrt{2100n}/3\) elements.

lemma U9_Ccard_le (n : ℕ) (hn : 1 ≤ n) (C : Finset ℕ)
    (hC : ∀ p ∈ C, p.Prime ∧ p ^ 2 ≤ 2100 * n) :
    (C.card : ℝ) ≤ Real.sqrt (((2100 * n : ℕ)) : ℝ) / 3

Uses 1 · Used by 1

Proof usesPrime-counting bound \(\pi(x) \le x/3\) for real \(x \ge 36\)

Used byContribution of the small-square primes

LemmaContribution of the small-square primes#✓fully proved

Let \(n \ge 1\) be a natural number. For each divisor \(m\) of \(210\) put \(N_m = 210n/m\), let \(\mu\) be the Möbius function, and for a prime \(p\) with \(p\)-adic valuation \(v_p\) put \(\nu_9(p, n) = \sum_{m \mid 210} \mu(m) (v_p((10N_m)!) - v_p((9N_m)!) - v_p(N_m!))\). Then the sum of \(\nu_9(p, n) \log p\) over the primes \(p \le 1890n\) with \(p^2 \le 2100n\) is at most \(\sqrt{2100n} \log(2100n)\).

lemma U9_C_le (n : ℕ) (hn : 1 ≤ n) :
    ∑ p ∈ ((Nat.primesBelow (2100 * n + 1)).filter (fun p => p ≤ 1890 * n)).filter
      (fun p => ¬ 2100 * n < p ^ 2),
      ((nu9 p n : ℤ) : ℝ) * Real.log ((p : ℕ) : ℝ)
    ≤ Real.sqrt (2100 * (n : ℝ)) * Real.log (2100 * (n : ℝ))

Uses 3 · Used by 1

Statement usesThe \(p\)-adic valuation of the weighted product

Proof usesCounting small-square primes · Bound for one small-square prime term

Used byUpper bound for \(\log F_9(n)\) when \((1890n, 2100n)\) has no prime

TheoremUpper bound for \(\log F_9(n)\) when \((1890n, 2100n)\) has no prime#✓fully proved

Let \(n \ge 1\) be a natural number such that no prime \(p\) satisfies \(1890n < p \le 2100n\), and let \(\log F_9(n) = \sum_{d \mid 210} \mu(d) \log \frac{(2100n/d)!}{(1890n/d)!\,(210n/d)!}\), where \(\mu\) is the Möbius function. Then

\[ \log F_9(n) \le \left(\frac{18900}{279} + \frac{18900}{657} + \frac{18900}{963}\right) n \log 3.4 \;+\; \sqrt{2100n}\,\log(2100n). \]

theorem logF9_upper (n : ℕ) (hn : 1 ≤ n)
    (hA : ∀ p : ℕ, p.Prime → 1890 * n < p → p ≤ 2100 * n → False) :
    logF9 n ≤ (18900 / 279 + 18900 / 657 + 18900 / 963 : ℝ) * n * Real.log 3.4
      + Real.sqrt (2100 * n) * Real.log (2100 * n)

Uses 5 · Used by 1

Statement usesLogarithm of Breusch's product \(F_9(n)\)

Proof usesContribution of primes with \(p^2 > 2100n\) · Contribution of the small-square primes · Prime factorization of \(\log F_9(n)\) · The \(p\)-adic valuation of the weighted product

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

DefinitionBreusch's endgame upper-bound inequality#✓fully proved

For a natural number \(n\) write \(L(n) = \sum_{d \mid 210} \mu(d) \log \binom{2100n/d}{210n/d}\), where \(\mu\) is the Möbius function; this is the logarithm of Breusch's product \(F_9(n)\). The endgame upper-bound inequality at \(n\) is the statement

\[L(n) \le \left(\frac{18900}{279} + \frac{18900}{657} + \frac{18900}{963}\right) n \log 3.4 + \sqrt{2100n}\,\log(2100n).\]

def UpperIneq (n : ℕ) : Prop :=
  logF9 n ≤ (18900/279 + 18900/657 + 18900/963 : ℝ) * n
    * Real.log 3.4 + Real.sqrt ((2100:ℝ)*n) * Real.log ((2100:ℝ)*n)

Uses 1 · Used by 3

Statement usesLogarithm of Breusch's product \(F_9(n)\)

Used byPrimes in \((X, 9X/8)\) for large \(X\), assuming the upper bound · Endgame contradiction in Breusch's theorem · Breusch's theorem from the upper bound

DefinitionBreusch's prime chain#✓fully proved

The chain is the list of the following 111 natural numbers, in order:

53, 59, 61, 67, 73, 79, 83, 89, 97, 109, 113, 127, 139, 151, 167, 181, 199, 223, 241, 271, 293, 317, 353, 397, 443, 491, 547, 613, 683, 761, 853, 953, 1069, 1201, 1327, 1489, 1669, 1877, 2111, 2371, 2663, 2971, 3331, 3739, 4201, 4723, 5309, 5953, 6691, 7523, 8461, 9511, 10691, 12011, 13499, 15173, 17053, 19183, 21577, 24251, 27281, 30689, 34519, 38833, 43669, 49123, 55259, 62143, 69899, 78623, 88427, 99469, 111893, 125863, 141587, 159233, 179119, 201499, 226669, 254993, 286859, 322709, 363047, 408427, 459479, 516911, 581521, 654209, 735983, 827969, 931421, 1047841, 1178809, 1326151, 1491913, 1678399, 1888193, 2124197, 2389721, 2688421, 3024457, 3402473, 3827767, 4306231, 4844501, 5450041, 6131239, 6897643, 7759831, 8729801, 9820997.

Every entry is prime, and each entry after the first is less than \(\frac{9}{8}\) times the entry before it.

MathlibExt.NumberTheory.BreuschWanted.Internal.chain · 20 lines

def chain : List ℕ :=
  [53, 59, 61, 67, 73, 79,
  83, 89, 97, 109, 113, 127,
  139, 151, 167, 181, 199, 223,
  241, 271, 293, 317, 353, 397,
  443, 491, 547, 613, 683, 761,
  853, 953, 1069, 1201, 1327, 1489,
  1669, 1877, 2111, 2371, 2663, 2971,
  3331, 3739, 4201, 4723, 5309, 5953,
  6691, 7523, 8461, 9511, 10691, 12011,
  13499, 15173, 17053, 19183, 21577, 24251,
  27281, 30689, 34519, 38833, 43669, 49123,
  55259, 62143, 69899, 78623, 88427, 99469,
  111893, 125863, 141587, 159233, 179119, 201499,
  226669, 254993, 286859, 322709, 363047, 408427,
  459479, 516911, 581521, 654209, 735983, 827969,
  931421, 1047841, 1178809, 1326151, 1491913, 1678399,
  1888193, 2124197, 2389721, 2688421, 3024457, 3402473,
  3827767, 4306231, 4844501, 5450041, 6131239, 6897643,
  7759831, 8729801, 9820997]

Used by 5

Used byPrimes in \((X, 9X/8)\) for \(53 \le X < 9820997\) · Last entry of Breusch's prime chain · Entries of Breusch's prime chain are prime · Consecutive entries of Breusch's prime chain are within a factor \(9/8\) · Breusch's prime chain is strictly increasing

TheoremEntries of Breusch's prime chain are prime#✓fully proved

Every entry of the chain is a prime number.

theorem chain_prime : ∀ p ∈ chain, p.Prime

Uses 1 · Used by 1

Statement usesBreusch's prime chain

Used byPrimes in \((X, 9X/8)\) for \(53 \le X < 9820997\)

TheoremBreusch's prime chain is strictly increasing#✓fully proved

Each entry of the chain is less than every later entry.

theorem chain_sorted : chain.Pairwise (· < ·)

Uses 1 · Used by 1

Statement usesBreusch's prime chain

Used byPrimes in \((X, 9X/8)\) for \(53 \le X < 9820997\)

TheoremConsecutive entries of Breusch's prime chain are within a factor \(9/8\)#✓fully proved

If \(b\) immediately follows \(a\) in the chain, then \(8b < 9a\).

theorem chain_ratio : ∀ pr ∈ chain.zip chain.tail, 8 * pr.2 < 9 * pr.1

Uses 1 · Used by 1

Statement usesBreusch's prime chain

Used byPrimes in \((X, 9X/8)\) for \(53 \le X < 9820997\)

TheoremLast entry of Breusch's prime chain#✓fully proved

The last entry of the chain is \(9820997\).

theorem chain_getLast : chain.getLast (by decide : chain ≠ []) = 9820997

Uses 1

Statement usesBreusch's prime chain

LemmaBracketing a real number in an increasing list#✓fully proved

Let \(X\) be a real number and let \(c_0 < c_1 < \dots < c_k\) be natural numbers with \(c_0 \le X < c_k\). Then there is an index \(i < k\) with \(c_i \le X < c_{i+1}\).

lemma bracket (X : ℝ) : ∀ (l : List ℕ) (prev : ℕ),
    List.Pairwise (· < ·) (prev :: l) → (prev:ℝ) ≤ X →
    ∀ (hne : prev :: l ≠ []), (X:ℝ) < ((((prev :: l).getLast hne : ℕ)):ℝ) →
    ∃ (l1 : List ℕ) (a b : ℕ) (l2 : List ℕ),
      prev :: l = l1 ++ [a, b] ++ l2 ∧ (a:ℝ) ≤ X ∧ (X:ℝ) < (b:ℝ)

Used by 1

Used byPrimes in \((X, 9X/8)\) for \(53 \le X < 9820997\)

LemmaConsecutive pairs survive prepending#✓fully proved

Let \(R\) be a list of natural numbers and let \(a, b, d\) be natural numbers. If \((a, b)\) is a pair of consecutive entries of \(R\) (an element of the list obtained by zipping \(R\) with its tail), then \((a, b)\) is also a pair of consecutive entries of the list obtained by prepending \(d\) to \(R\).

lemma zip_cons_mem {R : List ℕ} {d a b : ℕ}
    (h : (a, b) ∈ R.zip R.tail) : (a, b) ∈ (d :: R).zip (d :: R).tail

Used by 1

Used byAdjacent entries form a consecutive pair

LemmaAdjacent entries form a consecutive pair#✓fully proved

Let \(l\), \(l_1\), \(l_2\) be lists of natural numbers and let \(a, b\) be natural numbers. If \(l\) is the concatenation of \(l_1\), the two-entry list \(a, b\), and \(l_2\), then \((a, b)\) is a pair of consecutive entries of \(l\) (an element of the list obtained by zipping \(l\) with its tail).

lemma zip_mem_of_consec {l : List ℕ} {a b : ℕ} {l1 l2 : List ℕ}
    (h : l = l1 ++ [a, b] ++ l2) : (a, b) ∈ l.zip l.tail

Uses 1 · Used by 1

Proof usesConsecutive pairs survive prepending

Used byPrimes in \((X, 9X/8)\) for \(53 \le X < 9820997\)

TheoremPrimes in \((X, 9X/8)\) for \(53 \le X < 9820997\)#✓fully proved

For every real number \(X\) with \(53 \le X < 9820997\) there is a prime \(p\) with \(X < p < \frac{9}{8}X\).

theorem chain_cover (X : ℝ) (hlo : (53 : ℝ) ≤ X) (hhi : X < (9820997 : ℝ)) :
    ∃ p : ℕ, p.Prime ∧ (X : ℝ) < (p : ℝ) ∧ (p : ℝ) < (9 / 8 : ℝ) * X

Uses 6 · Used by 1

Proof usesBracketing a real number in an increasing list · Breusch's prime chain · Entries of Breusch's prime chain are prime · Consecutive entries of Breusch's prime chain are within a factor \(9/8\) · Breusch's prime chain is strictly increasing · Adjacent entries form a consecutive pair

Used byBreusch's theorem from the upper bound

LemmaEvery large real lies in a window \((5600n/3, 1890n)\)#✓fully proved

For every real number \(X \ge 5600 \cdot 4762 / 3\) there is a natural number \(n \ge 4762\) with \(5600n/3 \le X \le 1890n\).

lemma overlap (X : ℝ) (hX : (5600 * 4762 / 3 : ℝ) ≤ X) :
    ∃ n : ℕ, 4762 ≤ n ∧ (5600 : ℝ) * n / 3 ≤ X ∧ X ≤ (1890 : ℝ) * n

Used by 1

Used byPrimes in \((X, 9X/8)\) for large \(X\), assuming the upper bound

LemmaEndgame contradiction in Breusch's theorem#✓fully proved

Let \(n \ge 4762\) be a natural number. If there is no prime \(p\) with \(1890n < p \le 2100n\) and \(n\) satisfies the endgame upper-bound inequality, then we have a contradiction.

lemma main_contra (n : ℕ) (hn : 4762 ≤ n)
    (_hA : ∀ p : ℕ, p.Prime → 1890 * n < p → p ≤ 2100 * n → False)
    (hupper : UpperIneq n) : False

Uses 5 · Used by 1

Statement usesBreusch's endgame upper-bound inequality

Proof usesNumerical margin of the main term · Positivity of the gap in Breusch's prime interval argument · Logarithm of Breusch's product \(F_9(n)\) · Lower bound for \(\log F_9(n)\)

Used byPrimes in \((X, 9X/8)\) for large \(X\), assuming the upper bound

TheoremPrimes in \((X, 9X/8)\) for large \(X\), assuming 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 5600 \cdot 4762 / 3\) 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 analytic_at_X (X : ℝ) (hX : (5600 * 4762 / 3 : ℝ) ≤ 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 usesEndgame contradiction in Breusch's theorem · Every large real lies in a window \((5600n/3, 1890n)\)

Used byBreusch's theorem from the upper bound

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.