Valuation identity for the weighted product to The primorial as a product of primes

LemmaValuation identity for the weighted product#✓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)\) and, for real \(x \ge 0\), \(G(x) = \sum_{d \mid 210} \mu(d)\bigl(\lfloor 2100x/d \rfloor - \lfloor 1890x/d \rfloor - \lfloor 210x/d \rfloor\bigr)\). If \(p\) is a prime and \(n\), \(b\) are natural numbers with \(\lfloor \log_p (2100n) \rfloor < b\), where the floor of the logarithm is taken to be \(0\) when \(n = 0\), then \(\nu_p(n) = \sum_{j=1}^{b-1} G(n/p^j)\).

lemma nu9_eq_sum_G {p n b : ℕ} (hp : p.Prime)
    (hb : Nat.log p (10 * Q9 * n) < b) :
    nu9 p n = ∑ j ∈ Finset.Ico 1 b, G9r ((n : ℝ) / (((p ^ j : ℕ)) : ℝ))

Uses 17 · Used by 2

Statement usesContinuous Breusch function · The modulus \(Q_9 = 210\) · The \(p\)-adic valuation of the weighted product

Proof usesUpper bound for the scaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_{10}\) · Upper bound for the scaled factorial argument \(N_1\) · Scaled factorial argument \(N_1\) · Upper bound for the scaled factorial argument \(N_9\) · Scaled factorial argument N₉ · Legendre terms of \(N_1\) as real floors · Legendre terms of \(N_{10}\) as real floors · Legendre terms of \(N_9\) as real floors · Legendre's formula with integer summands · One divisor's contribution to the valuation · The Möbius divisor table for \(210\) · Entries of the divisor table for \(210\) divide \(210\) · Divisors in the table for \(210\) are positive

Used bySingle-term valuation identity for large primes · Bound for one small-square prime term

LemmaSingle-term valuation identity for large primes#✓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)\) and, for real \(x \ge 0\), \(G(x) = \sum_{d \mid 210} \mu(d)\bigl(\lfloor 2100x/d \rfloor - \lfloor 1890x/d \rfloor - \lfloor 210x/d \rfloor\bigr)\). If \(p\) is a prime and \(n \ge 1\) is a natural number with \(2100n < p^2\), then \(\nu_p(n) = G(n/p)\).

lemma nu9_eq_single {p n : ℕ} (hp : p.Prime) (hn : 1 ≤ n)
    (hbig : 10 * Q9 * n < p ^ 2) : nu9 p n = G9r ((n : ℝ) / (((p : ℕ)) : ℝ))

Uses 5 · Used by 1

Statement usesContinuous Breusch function · The modulus \(Q_9 = 210\) · The \(p\)-adic valuation of the weighted product

Proof usesThe continuous Breusch function vanishes at small ratios · Valuation identity for the weighted product

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

LemmaValue of \(10Qn\)#✓fully proved

Let \(Q = 210\) be the truncation modulus. For every natural number \(n\), \(10 \cdot Q \cdot n = 2100n\).

lemma U9_10Q9 (n : ℕ) : 10 * Q9 * n = 2100 * n

Uses 2 · Used by 2

Statement usesThe modulus \(Q_9 = 210\)

Proof usesValue of Q₉

Used byContribution of primes with \(p^2 > 2100n\) · Bound for one small-square prime term

LemmaLogarithm of a natural number from its factorization#✓fully proved

For every nonzero natural number \(K\), \(\log K = \sum_{p} v_p(K) \log p\), where \(p\) runs over the prime divisors of \(K\) and \(v_p(K)\) is the exponent of \(p\) in the prime factorization of \(K\).

lemma U9_log_fact (K : ℕ) (hK : K ≠ 0) :
    Real.log ((K : ℕ) : ℝ) =
      ∑ p ∈ K.factorization.support, ((K.factorization p : ℕ) : ℝ) * Real.log ((p : ℕ) : ℝ)

Used by 1

Used byA weighted log-factor as a sum over primes

LemmaBound on the prime factors of the ratio factors#✓fully proved

Let \((m, \mu)\) be an entry of the divisor table \(w_9\) (so \(m\) divides \(210\) and \(\mu\) is the Möbius value of \(m\)), let \(n\) be a natural number and put \(d = 210/m\). Then every prime factor of \((10nd)!/((9nd)!\,(nd)!)\) is at most \(2100n\).

lemma U9_supp_sub (q : ℕ × ℤ) (hq : q ∈ w9) (n : ℕ) :
    (ratio9 q.1 n).factorization.support ⊆ Nat.primesBelow (2100 * n + 1)

Uses 11 · Used by 1

Statement usesBinomial factor ratio₉ · The Möbius divisor table for \(210\)

Proof usesUpper bound for the scaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉ · The modulus \(Q_9 = 210\) · Value of Q₉ · Factorial divisibility behind ratio₉ · Entries of the divisor table for \(210\) divide \(210\) · Divisors in the table for \(210\) are positive

Used byA weighted log-factor as a sum over primes

LemmaValuation term of one binomial factor#✓fully proved

Let \(Q = 210\), let \(m \ge 1\) be a divisor of \(Q\), let \(w\) be an integer, and let \(p\) and \(n\) be natural numbers. Put \(N = n \cdot (Q/m)\) and \(R = (10N)!/((9N)!\,N!)\). For a natural number \(a\), write \(v_p(a)\) for the exponent of \(p\) in the prime factorization of \(a\) (zero when \(p\) is not prime). Then \(w \, (v_p((10N)!) - v_p((9N)!) - v_p(N!)) = w \, v_p(R)\).

lemma U9_nu9term_eq (q : ℕ × ℤ) (p n : ℕ) (hm1 : 1 ≤ q.1) (hd : q.1 ∣ Q9) :
    ((nu9term q p n : ℤ) : ℝ)
      = (q.2 : ℝ) * (((ratio9 q.1 n).factorization p : ℕ) : ℝ)

Uses 7 · Used by 1

Statement usesThe modulus \(Q_9 = 210\) · One divisor's contribution to the valuation · Binomial factor ratio₉

Proof usesScaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉ · Valuation of a factorial ratio as a difference of valuations

Used byA weighted log-factor as a sum over primes

LemmaValuation terms vanish off the prime support#✓fully proved

Let \(m \ge 1\) be a divisor of \(Q_9 = 210\), let \(\mu\) be an integer, let \(p\) and \(n\) be natural numbers, and put \(d = 210/m\). For a natural number \(k\) write \(v_p(k)\) for the exponent of \(p\) in the prime factorization of \(k\) (zero when \(p\) is not prime). If \(v_p\bigl((10nd)!/((9nd)!\,(nd)!)\bigr) = 0\), then the valuation term \(\mu\,\bigl(v_p((10nd)!) - v_p((9nd)!) - v_p((nd)!)\bigr)\) of the pair \((m, \mu)\) at \(p\) and \(n\) is \(0\).

lemma U9_nu9term_zero (q : ℕ × ℤ) (p n : ℕ) (hm1 : 1 ≤ q.1) (hd : q.1 ∣ Q9)
    (h0 : (ratio9 q.1 n).factorization p = 0) : nu9term q p n = 0

Uses 7 · Used by 1

Statement usesThe modulus \(Q_9 = 210\) · One divisor's contribution to the valuation · Binomial factor ratio₉

Proof usesScaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉ · Valuation of a factorial ratio as a difference of valuations

Used byA weighted log-factor as a sum over primes

LemmaA weighted log-factor as a sum over primes#✓fully proved

Let \((m, \mu)\) be an entry of the divisor table \(w_9\) (so \(m\) divides \(210\) and \(\mu\) is the Möbius value of \(m\)), let \(n \ge 1\) be a natural number, put \(d = 210/m\) and \(R = (10nd)!/((9nd)!\,(nd)!)\), and for a prime \(p\) write \(\nu_p = \mu\,\bigl(v_p((10nd)!) - v_p((9nd)!) - v_p((nd)!)\bigr)\), where \(v_p(k)\) is the exponent of \(p\) in the prime factorization of \(k\). Then \(\mu \log R\) equals the sum of \(\nu_p \log p\) over all primes \(p \le 2100n\).

lemma U9_q_expand (q : ℕ × ℤ) (hq : q ∈ w9) (n : ℕ) (hn : 1 ≤ n) :
    (q.2 : ℝ) * Real.log ((ratio9 q.1 n : ℕ) : ℝ)
      = ∑ p ∈ Nat.primesBelow (2100 * n + 1),
        ((nu9term q p n : ℤ) : ℝ) * Real.log ((p : ℕ) : ℝ)

Uses 11 · Used by 1

Statement usesOne divisor's contribution to the valuation · Binomial factor ratio₉ · The Möbius divisor table for \(210\)

Proof usesThe modulus \(Q_9 = 210\) · Logarithm of a natural number from its factorization · Valuation term of one binomial factor · Valuation terms vanish off the prime support · Bound on the prime factors of the ratio factors · Positivity of ratio₉ · Entries of the divisor table for \(210\) divide \(210\) · Divisors in the table for \(210\) are positive

Used byPrime factorization of \(\log F_9(n)\)

LemmaPrime factorization of \(\log F_9(n)\)#✓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 let \(F_9(n) = \prod_{m \mid 210} \binom{10N_m}{N_m}^{\mu(m)}\). For a prime \(p\) let \(v_p\) denote 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!))\), the \(p\)-adic valuation of \(F_9(n)\). Then \(\log F_9(n) = \sum_{p \le 2100n} \nu_9(p, n) \log p\), where \(p\) runs over the primes at most \(2100n\).

lemma U9_bridge (n : ℕ) (hn : 1 ≤ n) :
    logF9 n = ∑ p ∈ Nat.primesBelow (2100 * n + 1),
      ((nu9 p n : ℤ) : ℝ) * Real.log ((p : ℕ) : ℝ)

Uses 6 · Used by 1

Statement usesLogarithm of Breusch's product \(F_9(n)\) · The \(p\)-adic valuation of the weighted product

Proof usesA weighted log-factor as a sum over primes · One divisor's contribution to the valuation · Binomial factor ratio₉ · The Möbius divisor table for \(210\)

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

LemmaLogarithms of primes are nonnegative#✓fully proved

For every prime \(p\), \(\log p \ge 0\).

lemma U9_logp_nonneg {p : ℕ} (hp : p.Prime) : 0 ≤ Real.log ((p : ℕ) : ℝ)

Used by 3

Used byContribution of primes with \(p^2 > 2100n\) · Prime-logarithm bound for one level of \(G\) · Bound for one small-square prime term

Lemma\(G\) is at most its positive part#✓fully proved

For real \(y\) let \(G(y) = \sum_{m \mid 210} \mu(m) (\lfloor 2100y/m \rfloor_+ - \lfloor 1890y/m \rfloor_+ - \lfloor 210y/m \rfloor_+)\), where \(\mu\) is the Möbius function and \(\lfloor t \rfloor_+ = \max(\lfloor t \rfloor, 0)\). For every real number \(x\), \(G(x) \le \max(G(x), 0)\).

lemma U9_G_toNat (x : ℝ) : ((G9r x : ℤ) : ℝ) ≤ ((((G9r x).toNat : ℕ)) : ℝ)

Uses 1 · Used by 1

Statement usesContinuous Breusch function

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

LemmaThe truncated continuous Breusch function is at most 3#✓fully proved

For every real \(x \ge 0\), the continuous Breusch function \(G\) satisfies \(\max(G(x), 0) \le 3\).

lemma U9_toNat_le3 (x : ℝ) (hx : 0 ≤ x) : (G9r x).toNat ≤ 3

Uses 2 · Used by 1

Statement usesContinuous Breusch function

Proof usesThe continuous Breusch function is at most 3

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

LemmaPositive lower bounds on a truncation lift to the integer#✓fully proved

Let \(z\) be an integer and let \(i \ge 1\) be a natural number. If \(i \le \max(z, 0)\), then \(i \le z\).

lemma U9_of_toNat {z : ℤ} {i : ℕ} (hi : 1 ≤ i) (h : i ≤ z.toNat) :
    (i : ℤ) ≤ z

Used by 1

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

LemmaLayer-cake decomposition with three levels#✓fully proved

Let \(B\) be a finite set of natural numbers, let \(M : \mathbb{N} \to \mathbb{N}\) and \(c : \mathbb{N} \to \mathbb{R}\), and suppose \(M(p) \le 3\) for every \(p \in B\). Then \(\sum_{p \in B} M(p) c(p) = \sum_{i=1}^{3} \sum_{p \in B,\, M(p) \ge i} c(p)\).

lemma U9_layercake (B : Finset ℕ) (M : ℕ → ℕ) (c : ℕ → ℝ)
    (hM : ∀ p ∈ B, M p ≤ 3) :
    ∑ p ∈ B, ((M p : ℕ) : ℝ) * c p
      = ∑ i ∈ Finset.Icc 1 3, ∑ p ∈ B.filter (fun p => i ≤ M p), c p

Used by 1

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

LemmaA level bound turns into a bound on the prime#✓fully proved

Let \(n \ge 1\) be a natural number, \(p\) a prime and \(j \ge 1\) a real number. If \(j / 18900 \le n / p\), then \(p \le 18900\,n / j\).

lemma U9_ple_of_G (n p : ℕ) (_hn : 1 ≤ n) (hp : p.Prime)
    (jm : ℝ) (hjm : 1 ≤ jm)
    (hlvl : jm / 18900 ≤ (n : ℝ) / ((p : ℕ) : ℝ)) :
    ((p : ℕ) : ℝ) ≤ 18900 * (n : ℝ) / jm

Used by 3

Used byUpper 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

LemmaPrimes up to \(1890n\) have \(n/p \ge 1/1890\)#✓fully proved

Let \(Q = 210\) be the truncation modulus, let \(n \ge 1\) be a natural number and let \(p\) be a prime with \(p \le 1890 n\). Then \(1/(9Q) \le n/p\), where \(9Q = 1890\).

lemma U9_xlo (n p : ℕ) (_hn : 1 ≤ n) (hp : p.Prime) (hle : p ≤ 1890 * n) :
    1 / (((9 * Q9 : ℕ)) : ℝ) ≤ (n : ℝ) / ((p : ℕ) : ℝ)

Uses 1 · Used by 3

Statement usesThe modulus \(Q_9 = 210\)

Used byUpper 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

LemmaUpper bound for primes where a Möbius-weighted floor sum is at least 1#✓fully proved

For real \(x \ge 0\) let \(G(x) = \sum_{m \mid 210} \mu(m)\bigl(\lfloor 2100x/m \rfloor - \lfloor 1890x/m \rfloor - \lfloor 210x/m \rfloor\bigr)\), where \(\mu\) is the Möbius function. Let \(n \ge 1\) be a natural number and \(p \le 1890n\) a prime. If \(G(n/p) \ge 1\), then \(p \le 18900n/279\).

lemma U9_ple1 (n p : ℕ) (hn : 1 ≤ n) (hp : p.Prime)
    (hle : p ≤ 1890 * n) (hG : (1 : ℤ) ≤ G9r ((n : ℝ) / ((p : ℕ) : ℝ))) :
    ((p : ℕ) : ℝ) ≤ 18900 * (n : ℝ) / 279

Uses 4 · Used by 1

Statement usesContinuous Breusch function

Proof usesLevel-\(1\) threshold for the continuous Breusch function · A level bound turns into a bound on the prime · Primes up to \(1890n\) have \(n/p \ge 1/1890\)

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

LemmaUpper bound for primes where a Möbius-weighted floor sum is at least 2#✓fully proved

For real \(x \ge 0\) let \(G(x) = \sum_{m \mid 210} \mu(m)\bigl(\lfloor 2100x/m \rfloor - \lfloor 1890x/m \rfloor - \lfloor 210x/m \rfloor\bigr)\), where \(\mu\) is the Möbius function. Let \(n \ge 1\) be a natural number and \(p \le 1890n\) a prime. If \(G(n/p) \ge 2\), then \(p \le 18900n/657\).

lemma U9_ple2 (n p : ℕ) (hn : 1 ≤ n) (hp : p.Prime)
    (hle : p ≤ 1890 * n) (hG : (2 : ℤ) ≤ G9r ((n : ℝ) / ((p : ℕ) : ℝ))) :
    ((p : ℕ) : ℝ) ≤ 18900 * (n : ℝ) / 657

Uses 4 · Used by 1

Statement usesContinuous Breusch function

Proof usesLevel-\(2\) threshold for the continuous Breusch function · A level bound turns into a bound on the prime · Primes up to \(1890n\) have \(n/p \ge 1/1890\)

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

LemmaUpper bound for primes where a Möbius-weighted floor sum is at least 3#✓fully proved

For real \(x \ge 0\) let \(G(x) = \sum_{m \mid 210} \mu(m)\bigl(\lfloor 2100x/m \rfloor - \lfloor 1890x/m \rfloor - \lfloor 210x/m \rfloor\bigr)\), where \(\mu\) is the Möbius function. Let \(n \ge 1\) be a natural number and \(p \le 1890n\) a prime. If \(G(n/p) \ge 3\), then \(p \le 18900n/963\).

lemma U9_ple3 (n p : ℕ) (hn : 1 ≤ n) (hp : p.Prime)
    (hle : p ≤ 1890 * n) (hG : (3 : ℤ) ≤ G9r ((n : ℝ) / ((p : ℕ) : ℝ))) :
    ((p : ℕ) : ℝ) ≤ 18900 * (n : ℝ) / 963

Uses 4 · Used by 1

Statement usesContinuous Breusch function

Proof usesLevel-\(3\) threshold for the continuous Breusch function · A level bound turns into a bound on the prime · Primes up to \(1890n\) have \(n/p \ge 1/1890\)

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

LemmaThe primorial as a product of primes#✓fully proved

For every natural number \(k\), the primorial \(k\#\) equals the product of all primes \(p\) with \(p < k + 1\).

lemma U9_primorial_eq (k : ℕ) :
    primorial k = ∏ p ∈ Nat.primesBelow (k + 1), p

Used by 1

Used byChebyshev-type bound for the sum of prime logarithms

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.