Upper bound for log 17 to One-period shift of \(G_9\)

LemmaUpper bound for log 17#✓fully proved

The natural logarithm of \(17\) satisfies \(\log 17 < 2.8333\).

lemma log17_lt : Real.log 17 < (2.8333 : ℝ)

Uses 2 · Used by 1

Proof usesBounding a logarithm above by the exponential · Exponential lower bound from a power comparison

Used byNumerical margin of the main term

LemmaLogarithm of 10#✓fully proved

The natural logarithm satisfies \(\log 10 = \log 2 + \log 5\).

lemma log10_eq : Real.log (10 : ℝ) = Real.log 2 + Real.log 5

Used by 2

Used byLogarithm bounded by a multiple of the square root · Numerical margin of the main term

LemmaLogarithm of 9#✓fully proved

The natural logarithm satisfies \(\log 9 = 2 \log 3\).

lemma log9_eq : Real.log (9 : ℝ) = 2 * Real.log 3

Used by 1

Used byNumerical margin of the main term

LemmaLogarithm of 3.4#✓fully proved

The natural logarithm satisfies \(\log(34/10) = \log 17 - \log 5\).

lemma log34div10_eq : Real.log (34 / 10 : ℝ) = Real.log 17 - Real.log 5

Used by 1

Used byNumerical margin of the main term

LemmaEvaluation of a three-term rational sum#✓fully proved

In the real numbers, \(\frac{18900}{279} + \frac{18900}{657} + \frac{18900}{963} = \frac{28121100}{242141}\).

The right-hand side is the sum written in lowest terms.

lemma c9_eq : (18900 / 279 + 18900 / 657 + 18900 / 963 : ℝ) = 28121100 / 242141

Used by 1

Used byNumerical margin of the main term

TheoremNumerical margin of the main term#✓fully proved

With \(\log\) the natural logarithm, \(48\,(10 \log 10 - 9 \log 9) - \left(\frac{18900}{279} + \frac{18900}{657} + \frac{18900}{963}\right) \log \frac{34}{10} > 13\).

theorem T03c_eqmain_margin : 48 * (10 * Real.log 10 - 9 * Real.log 9) -
    (18900 / 279 + 18900 / 657 + 18900 / 963 : ℝ) * Real.log (34 / 10) > 13

Uses 8 · Used by 1

Proof usesEvaluation of a three-term rational sum · Logarithm of 10 · Upper bound for log 17 · Lower bound for log 2 · Logarithm of 3.4 · Upper bound for log 3 · Lower bound for log 5 · Logarithm of 9

Used byEndgame contradiction in Breusch's theorem

LemmaPrime-counting bound \(\pi(m) \le m/3\) for \(36 \le m < 156\)#✓fully proved

Let \(\pi(m)\) denote the number of primes \(p \le m\). For every natural number \(m\) with \(36 \le m < 156\), \(3\pi(m) \le m\).

Checked by computation.

lemma pi_third_small : ∀ m : ℕ, 36 ≤ m → m < 156 → 3 * Nat.primeCounting m ≤ m

Used by 1

Used byPrime-counting bound \(\pi(m) \le m/3\) for natural \(m \ge 36\)

LemmaPrime-counting bound \(\pi(m) \le m/3\) from \(156\) on#✓fully proved

Let \(\pi(m)\) denote the number of primes \(p \le m\). For every natural number \(m \ge 156\), \(3\pi(m) \le m\).

lemma pi_third_large (m : ℕ) (hm : 156 ≤ m) : 3 * Nat.primeCounting m ≤ m

Used by 1

Used byPrime-counting bound \(\pi(m) \le m/3\) for natural \(m \ge 36\)

LemmaPrime-counting bound \(\pi(m) \le m/3\) for natural \(m \ge 36\)#✓fully proved

Let \(\pi(m)\) denote the number of primes \(p \le m\). For every natural number \(m \ge 36\), \(3\pi(m) \le m\).

lemma pi_third_nat (m : ℕ) (hm36 : 36 ≤ m) : 3 * Nat.primeCounting m ≤ m

Uses 2 · Used by 1

Proof usesPrime-counting bound \(\pi(m) \le m/3\) from \(156\) on · Prime-counting bound \(\pi(m) \le m/3\) for \(36 \le m < 156\)

Used byPrime-counting bound \(\pi(x) \le x/3\) for real \(x \ge 36\)

TheoremPrime-counting bound \(\pi(x) \le x/3\) for real \(x \ge 36\)#✓fully proved

Let \(\pi(n)\) denote the number of primes \(p \le n\). For every real number \(x \ge 36\), \(\pi(\lfloor x \rfloor) \le x/3\).

theorem pi_third {x : ℝ} (hx : 36 ≤ x) : (Nat.primeCounting ⌊x⌋₊ : ℝ) ≤ x / 3

Uses 1 · Used by 1

Proof usesPrime-counting bound \(\pi(m) \le m/3\) for natural \(m \ge 36\)

Used byCounting small-square primes

LemmaUpper bound for log 10#✓fully proved

The natural logarithm of \(10\) satisfies \(\log 10 < 2.4\).

lemma log10_lt : Real.log 10 < (2.4 : ℝ)

Uses 2 · Used by 1

Proof usesBounding a logarithm above by the exponential · Exponential lower bound from a power comparison

Used byLogarithm bounded by a multiple of the square root

LemmaStrict decay of log over square root beyond e squared#✓fully proved

Let \(a\) and \(t\) be real numbers with \(a > 0\), \(t > 1\) and \(\log a > 2\), where \(\log\) is the natural logarithm. Then \(\frac{\log(at)}{\sqrt{at}} < \frac{\log a}{\sqrt{a}}\).

lemma log_div_sqrt_decay {a t : ℝ} (ha : 0 < a) (ht : 1 < t)
    (hla : 2 < Real.log a) :
    Real.log (a*t) / Real.sqrt (a*t) < Real.log a / Real.sqrt a

Used by 1

Used byLogarithm bounded by a multiple of the square root

LemmaLogarithm bounded by a multiple of the square root#✓fully proved

For every real number \(x \ge 10^7\), \(\log x \le 0.006\sqrt{x}\), where \(\log\) is the natural logarithm.

lemma log_le_sqrt06 (x : ℝ) (hx : (10 ^ 7 : ℝ) ≤ x) :
    Real.log x ≤ 0.006 * Real.sqrt x

Uses 5 · Used by 1

Proof usesLogarithm of 10 · Upper bound for log 10 · Lower bound for log 2 · Lower bound for log 5 · Strict decay of log over square root beyond e squared

Used byPositivity of the gap in Breusch's prime interval argument

LemmaPositivity of the gap in Breusch's prime interval argument#✓fully proved

For every natural number \(n \ge 4762\), \(13n - 16 - 48\log(2100n) - \sqrt{2100n}\,\log(2100n) > 0\), where \(\log\) is the natural logarithm.

lemma gap_pos (n : ℕ) (hn : 4762 ≤ n) :
    (13:ℝ)*n - 16 - 48*Real.log ((2100:ℝ)*n)
      - Real.sqrt ((2100:ℝ)*n)*Real.log ((2100:ℝ)*n) > 0

Uses 1 · Used by 1

Proof usesLogarithm bounded by a multiple of the square root

Used byEndgame contradiction in Breusch's theorem

DefinitionContinuous Breusch function#✓fully proved

For real \(x\), the continuous Breusch function is the integer

\[G(x) = \sum_{d \mid 210} \mu(d) \left( \lfloor 2100x/d \rfloor - \lfloor 1890x/d \rfloor - \lfloor 210x/d \rfloor \right),\]

where \(d\) ranges over the positive divisors of \(210\), \(\mu\) is the Möbius function, and each floor is the natural-number floor, which is \(0\) for negative arguments.

noncomputable def G9r (x : ℝ) : ℤ := w9.toFinset.sum (fun q : ℕ × ℤ =>
  q.2 * ((Int.ofNat ⌊((10*Q9:ℕ):ℝ)*x/(q.1:ℝ)⌋₊)
    - (Int.ofNat ⌊((9*Q9:ℕ):ℝ)*x/(q.1:ℝ)⌋₊) - (Int.ofNat ⌊((Q9:ℕ):ℝ)*x/(q.1:ℝ)⌋₊)))

Uses 2 · Used by 17

Statement usesThe modulus \(Q_9 = 210\) · The Möbius divisor table for \(210\)

Used byThe continuous Breusch function agrees with the grid function · The continuous Breusch function is at most 3 · Level-\(1\) threshold for the continuous Breusch function · Level-\(2\) threshold for the continuous Breusch function · Level-\(3\) threshold for the continuous Breusch function · The continuous Breusch function vanishes near zero · The continuous Breusch function vanishes at small ratios · Single-term valuation identity for large primes · Valuation identity for the weighted product · \(G\) is at most its positive part · 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 · Contribution of primes with \(p^2 > 2100n\) · Prime-logarithm bound for one level of \(G\) · Bound for one small-square prime term

LemmaFloor of a quotient of natural numbers#✓fully proved

For all natural numbers \(a\) and \(b\), the floor of the real number \(a / b\) equals the quotient of \(a\) by \(b\) in integer division. When \(b = 0\) both sides are \(0\), since division by zero gives \(0\) in both the reals and the natural numbers.

lemma nat_floor_nat_div (a b : ℕ) : ⌊((a:ℝ))/((b:ℝ))⌋₊ = a / b

Used by 1

Used byInteger cast of the floor of a quotient of natural numbers

LemmaRemainder bound for common multiples#✓fully proved

Let \(a\), \(b\), \(d\) be natural numbers with \(b > 0\), \(d > 0\), \(d \mid b\) and \(d \mid a\). Then the remainder of \(a\) modulo \(b\) is at most \(b - d\).

lemma nat_mod_le_of_dvd (a b d : ℕ) (hb : 0 < b) (_hd0 : 0 < d)
    (hdb : d ∣ b) (hda : d ∣ a) : a % b ≤ b - d

Used by 1

Used byReal floors at divisors of 210 agree with grid floors

LemmaReal floors at divisors of 210 agree with grid floors#✓fully proved

Let \(C\) and \(L\) be positive natural numbers, let \(m\) be a divisor of \(210\) with \(C \mid mL\), and let \(x \ge 0\) be a real number. Then \(\lfloor Cx/m \rfloor = \lfloor C \lfloor Lx \rfloor / (mL) \rfloor\).

lemma floor_grid_match (C L : ℕ) (hC : 0 < C) (hL : 0 < L) (m : ℕ) (hm : m ∣ 210)
    (hCmL : C ∣ m * L) (x : ℝ) (hx : 0 ≤ x) :
    ⌊((C:ℕ):ℝ)*x/(m:ℝ)⌋₊ = C*⌊((L:ℕ):ℝ)*x⌋₊/(m*L)

Uses 1 · Used by 1

Proof usesRemainder bound for common multiples

Used byThe continuous Breusch function agrees with the grid function

LemmaShifting a floor quotient by one period#✓fully proved

Let \(C\) and \(m\) be natural numbers with \(m > 0\) and \(m \mid C\). Then for every natural number \(j\), \(\lfloor C(j + 18900)/(18900m) \rfloor = \lfloor Cj/(18900m) \rfloor + C/m\).

lemma div_shift189 (C m : ℕ) (hmC : m ∣ C) (hm0 : 0 < m) (j : ℕ) :
    (C*(j+18900))/(m*18900) = C*j/(m*18900) + C/m

Used by 1

Used byOne-period shift of \(G_9\)

LemmaOne-period shift of \(G_9\)#✓fully proved

For every natural number \(j\), the grid \(G\)-function for \(k = 9\) satisfies \(G_9(j + 18900) = G_9(j)\).

lemma G9_shift (j : ℕ) : G9 (j + 18900) = G9 j

Uses 10 · Used by 1

Statement usesBreusch grid function for \(k = 9\)

Proof usesSummand of the Breusch grid function · The modulus \(Q_9 = 210\) · Value of Q₉ · Shifting a floor quotient by one period · Sum over a duplicate-free list · The Möbius divisor table for \(210\) · Entries of the divisor table for \(210\) divide \(210\) · The divisor table for \(210\) has no repeated entries · Divisors in the table for \(210\) are positive

Used byPeriodicity of \(G_9\) in multiples of \(18900\)

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.