Exact formula for the scaled factorial argument \(N_9\) to Power bound for the multinomial coefficient \(M(t)\), small \(t\)

LemmaExact formula for the scaled factorial argument \(N_9\)#✓fully proved

Let \(Q_9 = 210\) and, for natural numbers \(m\) and \(n\), let \(N_9(m, n) = 9 n \lfloor Q_9 / m \rfloor\). If \(m \ge 1\) and \(m\) divides \(Q_9\), then \(N_9(m, n) = \lfloor 9 Q_9 n / m \rfloor\).

lemma N9_eq {m n : ℕ} (hm1 : 1 ≤ m) (hd : m ∣ Q9) : N9m m n = 9*Q9*n/m

Uses 2 · Used by 2

Statement usesScaled factorial argument N₉ · The modulus \(Q_9 = 210\)

Used byLower bound for \(\log F_9(n)\) · Legendre terms of \(N_9\) as real floors

LemmaExact formula for the scaled factorial argument \(N_1\)#✓fully proved

Let \(Q_9 = 210\) and, for natural numbers \(m\) and \(n\), let \(N_1(m, n) = n \lfloor Q_9 / m \rfloor\). If \(m \ge 1\) and \(m\) divides \(Q_9\), then \(N_1(m, n) = \lfloor Q_9 n / m \rfloor\).

lemma N1_eq {m n : ℕ} (hm1 : 1 ≤ m) (hd : m ∣ Q9) : N1m m n = Q9*n/m

Uses 2 · Used by 2

Statement usesScaled factorial argument \(N_1\) · The modulus \(Q_9 = 210\)

Used byLower bound for \(\log F_9(n)\) · Legendre terms of \(N_1\) as real floors

LemmaCombined main term of the Möbius-weighted Stirling sums#✓fully proved

Let \(w_9\) be the table of pairs \((d, \mu(d))\) for the divisors \(d\) of \(210\), and let \(f(x) = x \log x - x\). For every natural number \(n \ge 1\), writing \(N = 210n\) (so that \(N/d\) is an integer for each \(d\) in \(w_9\)), we have \(\sum_{(d, \mu(d)) \in w_9} \mu(d) \bigl(f(10N/d) - f(9N/d) - f(N/d)\bigr) = 48 n (10 \log 10 - 9 \log 9)\).

lemma Z9_combined (n : ℕ) (hn : 1 ≤ n) :
    w9.toFinset.sum (fun q : ℕ×ℤ => (q.2:ℝ) * (fmain (((10*Q9*n/q.1:ℕ)):ℝ)
      - fmain (((9*Q9*n/q.1:ℕ)):ℝ) - fmain (((Q9*n/q.1:ℕ)):ℝ)))
    = 48 * (n:ℝ) * (10 * Real.log 10 - 9 * Real.log 9)

Uses 7 · Used by 1

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

Proof usesThe constant \(K_9\) · Value of Q₉ · Q₉ is positive · Closed form of the Möbius-weighted main-term sum

Used byLower bound for \(\log F_9(n)\)

LemmaLower bound for \(\log F_9(n)\)#✓fully proved

Let \(w_9\) be the table of divisors \(d\) of \(Q_9 = 210\) paired with their Möbius values \(\varepsilon\), and for a natural number \(n\) let

\[\log F_9(n) = \sum_{(d, \varepsilon) \in w_9} \varepsilon \log \frac{(10 n k_d)!}{(9 n k_d)!\,(n k_d)!}, \qquad k_d = 210/d.\]

Then for every natural number \(n \ge 1\),

\[48 n (10 \log 10 - 9 \log 9) - 16 - 48 \log(2100 n) \le \log F_9(n).\]

lemma logF9_lower (n : ℕ) (hn : 1 ≤ n) :
    48 * (n:ℝ) * (10 * Real.log 10 - 9 * Real.log 9) - 16
      - 48 * Real.log ((2100*n:ℕ):ℝ) ≤ logF9 n

Uses 25 · Used by 1

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

Proof usesExact formula for the scaled factorial argument \(N_{10}\) · Upper bound for the scaled factorial argument \(N_{10}\) · Positivity of the scaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_{10}\) · Exact formula for the scaled factorial argument \(N_1\) · Upper bound for the scaled factorial argument \(N_1\) · Positivity of the scaled factorial argument \(N_1\) · Scaled factorial argument \(N_1\) · Exact formula for the scaled factorial argument \(N_9\) · Upper bound for the scaled factorial argument \(N_9\) · Positivity of the scaled argument N₉ · Scaled factorial argument N₉ · The modulus \(Q_9 = 210\) · Value of Q₉ · Combined main term of the Möbius-weighted Stirling sums · Main Stirling term · Termwise Stirling lower bound in Breusch's argument · Logarithm of the binomial factor · Binomial factor ratio₉ · The Möbius divisor table for \(210\) · Entries of the divisor table for \(210\) divide \(210\) · The divisor table for \(210\) has 16 entries · The divisor table for \(210\) has no repeated entries · Divisors in the table for \(210\) are positive

Used byEndgame contradiction in Breusch's theorem

LemmaExtending the primorial bound leftward across an interval#✓fully proved

Let \(a \le m \le b\) be natural numbers, and write \(n\#\) for the primorial of \(n\) (the product of all primes \(p \le n\)). If \(10^a \cdot b\# \le 34^a\), then \(10^m \cdot m\# \le 34^m\).

lemma theta34_of_interval {lo hi m : ℕ} (hlo : lo ≤ m) (hhi : m ≤ hi)
    (hend : 10 ^ lo * primorial hi ≤ 34 ^ lo) :
    10 ^ m * primorial m ≤ 34 ^ m

Used by 1

Used byPrimorial bound \(3.4^m\) below \(133\)

DefinitionThe multinomial coefficient \(M(t)\) for the 3.4 primorial bound#✓fully proved

For a natural number \(t\), \(M(t) = \frac{(6t)!}{(3t)!\,(2t)!\,t!}\), defined as the quotient of \((6t)!\) by \((3t)!\,(2t)!\,t!\) in natural-number division.

def M34 (t : ℕ) : ℕ := (6*t)! / ((3*t)! * (2*t)! * t !)

Used by 10

Used byPower bound for the multinomial coefficient \(M(t)\), large \(t\) · Power bound for the multinomial coefficient \(M(t)\), small \(t\) · The multinomial coefficient \(M(t)\) as a product of binomial coefficients · Cleared-denominator identity for the multinomial coefficient \(M(t)\) · Key estimate for the multinomial coefficient \(M(t)\) · Positivity of the multinomial coefficient \(M(t)\) · Power bound for the multinomial coefficient \(M(t)\) · Splitting the primorial with a multinomial coefficient · Primorial bound by powers of 3.4, integer form · Primes in \((t, 6t)\) occur in \(M(t)\)

LemmaFactorial divisibility behind the multinomial coefficient#✓fully proved

For every natural number \(t\), the product \((3t)!\,(2t)!\,t!\) divides \((6t)!\).

lemma M34_dvd (t : ℕ) : (3*t)! * (2*t)! * t ! ∣ (6*t)!

Used by 2

Used byCleared-denominator identity for the multinomial coefficient \(M(t)\) · Positivity of the multinomial coefficient \(M(t)\)

LemmaPositivity of the multinomial coefficient \(M(t)\)#✓fully proved

Let \(M(t)\) be the natural-number quotient of \((6t)!\) by \((3t)!\,(2t)!\,t!\). For every natural number \(t\), \(M(t) > 0\).

lemma M34_pos (t : ℕ) : 0 < M34 t

Uses 2 · Used by 2

Statement usesThe multinomial coefficient \(M(t)\) for the 3.4 primorial bound

Proof usesFactorial divisibility behind the multinomial coefficient

Used bySplitting the primorial with a multinomial coefficient · Primes in \((t, 6t)\) occur in \(M(t)\)

LemmaCleared-denominator identity for the multinomial coefficient \(M(t)\)#✓fully proved

Let \(M(t)\) be the natural-number quotient of \((6t)!\) by \((3t)!\,(2t)!\,t!\). For every natural number \(t\), \(M(t) \cdot \big((3t)!\,(2t)!\,t!\big) = (6t)!\).

lemma M34_eq_mul (t : ℕ) : M34 t * ((3*t)! * (2*t)! * t !) = (6*t)!

Uses 2 · Used by 2

Statement usesThe multinomial coefficient \(M(t)\) for the 3.4 primorial bound

Proof usesFactorial divisibility behind the multinomial coefficient

Used byThe multinomial coefficient \(M(t)\) as a product of binomial coefficients · Primes in \((t, 6t)\) occur in \(M(t)\)

LemmaThe multinomial coefficient \(M(t)\) as a product of binomial coefficients#✓fully proved

Let \(M(t) = \frac{(6t)!}{(3t)!\,(2t)!\,t!}\). For every natural number \(t\), \(M(t) = \binom{6t}{3t} \binom{3t}{t}\).

lemma M34_eq_choose_mul (t : ℕ) : M34 t = Nat.choose (6*t) (3*t) * Nat.choose (3*t) t

Uses 2 · Used by 1

Statement usesThe multinomial coefficient \(M(t)\) for the 3.4 primorial bound

Proof usesCleared-denominator identity for the multinomial coefficient \(M(t)\)

Used byKey estimate for the multinomial coefficient \(M(t)\)

LemmaHalf-power bound for the central binomial coefficient#✓fully proved

For every natural number \(m \ge 1\), \(\binom{2m}{m} \le 2^{2m-1}\).

lemma choose_middle_half {m : ℕ} (hm : 1 ≤ m) : Nat.choose (2*m) m ≤ 2^(2*m-1)

Used by 1

Used byKey estimate for the multinomial coefficient \(M(t)\)

LemmaMultinomial bound for \((3t)!\)#✓fully proved

For every natural number \(t\), \((3t)! \le 3^{3t} (t!)^3\).

lemma multinomial3_le (t : ℕ) : (3*t)! ≤ 3^(3*t) * (t !)^3

Used by 1

Used byKey estimate for the multinomial coefficient \(M(t)\)

LemmaBinomial factorization of the factorial of a multiple of three#✓fully proved

For every natural number \(t\), \(\binom{3t}{t} \binom{2t}{t} (t!)^3 = (3t)!\).

lemma choose3_mul_choose2 (t : ℕ) :
    Nat.choose (3*t) t * Nat.choose (2*t) t * (t !)^3 = (3*t)!

Used by 1

Used byKey estimate for the multinomial coefficient \(M(t)\)

LemmaFour-power lower bound for the central binomial coefficient#✓fully proved

For every natural number \(t\), \(4^t \le (2t+1)\binom{2t}{t}\).

lemma four_pow_le (t : ℕ) : 4^t ≤ (2*t+1) * Nat.choose (2*t) t

Used by 1

Used byKey estimate for the multinomial coefficient \(M(t)\)

LemmaKey estimate for the multinomial coefficient \(M(t)\)#✓fully proved

Let \(M(t) = \frac{(6t)!}{(3t)!\,(2t)!\,t!}\). For every natural number \(t \ge 1\), \(2\,M(t) \le 432^t \, (2t + 1)\).

lemma M34_key (t : ℕ) (ht : 1 ≤ t) : 2 * M34 t ≤ 432^t * (2*t+1)

Uses 6 · Used by 1

Statement usesThe multinomial coefficient \(M(t)\) for the 3.4 primorial bound

Proof usesThe multinomial coefficient \(M(t)\) as a product of binomial coefficients · Binomial factorization of the factorial of a multiple of three · Half-power bound for the central binomial coefficient · Four-power lower bound for the central binomial coefficient · Multinomial bound for \((3t)!\)

Used byPower bound for the multinomial coefficient \(M(t)\), large \(t\)

LemmaBase case of the threshold inequality#✓fully proved

The inequality \(10^{1145} \cdot 432^{230} \cdot 461 \le 2 \cdot 34^{1145}\) holds; this is the inequality \(10^{5t-5} \cdot 432^{t} \cdot (2t+1) \le 2 \cdot 34^{5t-5}\) at \(t = 230\).

Checked by direct computation.

lemma P34_base : 10^(5*230-5) * 432^230 * (2*230+1) ≤ 2 * 34^(5*230-5)

Used by 1

Used byThreshold inequality for the multinomial bound

LemmaInduction step of the threshold inequality#✓fully proved

Let \(t \ge 230\) be a natural number. If \(10^{5t-5} \cdot 432^{t} \cdot (2t+1) \le 2 \cdot 34^{5t-5}\), then \(10^{5t} \cdot 432^{t+1} \cdot (2t+3) \le 2 \cdot 34^{5t}\), which is the same inequality with \(t+1\) in place of \(t\).

lemma P34_step (t : ℕ) (ht : 230 ≤ t)
    (ih : 10 ^ (5 * t - 5) * 432 ^ t * (2 * t + 1) ≤ 2 * 34 ^ (5 * t - 5)) :
    10 ^ (5 * (t + 1) - 5) * 432 ^ (t + 1) * (2 * (t + 1) + 1) ≤ 2 * 34 ^ (5 * (t + 1) - 5)

Used by 1

Used byThreshold inequality for the multinomial bound

LemmaThreshold inequality for the multinomial bound#✓fully proved

For every natural number \(t \ge 230\), \(10^{5t-5} \cdot 432^{t} \cdot (2t+1) \le 2 \cdot 34^{5t-5}\).

lemma P34 (t : ℕ) (ht : 230 ≤ t) :
    10^(5*t-5) * 432^t * (2*t+1) ≤ 2 * 34^(5*t-5)

Uses 2 · Used by 1

Proof usesBase case of the threshold inequality · Induction step of the threshold inequality

Used byPower bound for the multinomial coefficient \(M(t)\), large \(t\)

LemmaPower bound for the multinomial coefficient \(M(t)\), large \(t\)#✓fully proved

Let \(M(t) = \frac{(6t)!}{(3t)!\,(2t)!\,t!}\). For every natural number \(t \ge 230\), \(10^{5t-5} \cdot M(t) \le 34^{5t-5}\), that is, \(M(t) \le 3.4^{5t-5}\).

lemma M34_bound_large (t : ℕ) (ht : 230 ≤ t) : 10^(5*t-5) * M34 t ≤ 34^(5*t-5)

Uses 3 · Used by 1

Statement usesThe multinomial coefficient \(M(t)\) for the 3.4 primorial bound

Proof usesKey estimate for the multinomial coefficient \(M(t)\) · Threshold inequality for the multinomial bound

Used byPower bound for the multinomial coefficient \(M(t)\)

LemmaPower bound for the multinomial coefficient \(M(t)\), small \(t\)#✓fully proved

Let \(M(t) = \frac{(6t)!}{(3t)!\,(2t)!\,t!}\). For every natural number \(k < 207\), writing \(t = 23 + k\) (so \(23 \le t < 230\)), we have \(10^{5t-5} \cdot M(t) \le 34^{5t-5}\).

The finitely many cases are checked by direct computation.

lemma M34_bound_small : ∀ k < 207,
    10 ^ (5 * (23 + k) - 5) * M34 (23 + k) ≤ 34 ^ (5 * (23 + k) - 5)

Uses 1 · Used by 1

Statement usesThe multinomial coefficient \(M(t)\) for the 3.4 primorial bound

Used byPower bound for the multinomial coefficient \(M(t)\)

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.