Power bound for the multinomial coefficient \(M(t)\) to Upper bound for log 3

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

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

lemma M34_bound (t : ℕ) (ht : 23 ≤ 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 usesPower bound for the multinomial coefficient \(M(t)\), large \(t\) · Power bound for the multinomial coefficient \(M(t)\), small \(t\)

Used byPrimorial bound by powers of 3.4, integer form

LemmaSuperadditivity of floor division for three terms#✓fully proved

For natural numbers \(a, b, c\) and \(q > 0\), \(\lfloor a/q \rfloor + \lfloor b/q \rfloor + \lfloor c/q \rfloor \le \lfloor (a+b+c)/q \rfloor\).

lemma div_add_div_add_div_le (a b c q : ℕ) (hq : 0 < q) :
    a / q + b / q + c / q ≤ (a + b + c) / q

Used by 1

Used byPrimes in \((t, 6t)\) occur in \(M(t)\)

LemmaFloor-difference bound on the range 3t < p ≤ 6t#✓fully proved

Let \(t \ge 1\) and \(p\) be natural numbers with \(3t < p \le 6t\). Then \(\lfloor 6t/p \rfloor - \lfloor 3t/p \rfloor - \lfloor 2t/p \rfloor \ge 1\).

lemma vp_term_case1 (t p : ℕ) (_ht : 1 ≤ t) (hlo : 3 * t < p) (hhi : p ≤ 6 * t) :
    1 ≤ 6 * t / p - 3 * t / p - 2 * t / p

Used by 1

Used byFloor-difference bound on the range t < p ≤ 6t

LemmaFloor-difference bound on the range 2t < p ≤ 3t#✓fully proved

Let \(t \ge 1\) and \(p\) be natural numbers with \(2t < p \le 3t\). Then \(\lfloor 6t/p \rfloor - \lfloor 3t/p \rfloor - \lfloor 2t/p \rfloor \ge 1\).

lemma vp_term_case2 (t p : ℕ) (_ht : 1 ≤ t) (hlo : 2 * t < p) (hhi : p ≤ 3 * t) :
    1 ≤ 6 * t / p - 3 * t / p - 2 * t / p

Used by 1

Used byFloor-difference bound on the range t < p ≤ 6t

LemmaFloor-difference bound on the range 3t/2 < p ≤ 2t#✓fully proved

Let \(t \ge 1\) and \(p\) be natural numbers with \(3t < 2p\) and \(p \le 2t\). Then \(\lfloor 6t/p \rfloor - \lfloor 3t/p \rfloor - \lfloor 2t/p \rfloor \ge 1\).

lemma vp_term_case3 (t p : ℕ) (_ht : 1 ≤ t) (hlo : 3 * t < 2 * p) (hhi : p ≤ 2 * t) :
    1 ≤ 6 * t / p - 3 * t / p - 2 * t / p

Used by 1

Used byFloor-difference bound on the range t < p ≤ 6t

LemmaFloor-difference bound on the range 6t/5 < p ≤ 3t/2#✓fully proved

Let \(t \ge 1\) and \(p\) be natural numbers with \(6t < 5p\) and \(2p \le 3t\). Then \(\lfloor 6t/p \rfloor - \lfloor 3t/p \rfloor - \lfloor 2t/p \rfloor \ge 1\).

lemma vp_term_case4 (t p : ℕ) (ht : 1 ≤ t) (hlo : 6 * t < 5 * p) (hhi : 2 * p ≤ 3 * t) :
    1 ≤ 6 * t / p - 3 * t / p - 2 * t / p

Used by 1

Used byFloor-difference bound on the range t < p ≤ 6t

LemmaFloor-difference bound on the range t < p ≤ 6t/5#✓fully proved

Let \(t \ge 1\) and \(p\) be natural numbers with \(t < p\) and \(5p \le 6t\). Then \(\lfloor 6t/p \rfloor - \lfloor 3t/p \rfloor - \lfloor 2t/p \rfloor \ge 1\).

lemma vp_term_case5 (t p : ℕ) (_ht : 1 ≤ t) (hlo : t < p) (hhi : 5 * p ≤ 6 * t) :
    1 ≤ 6 * t / p - 3 * t / p - 2 * t / p

Used by 1

Used byFloor-difference bound on the range t < p ≤ 6t

LemmaFloor-difference bound on the range t < p ≤ 6t#✓fully proved

Let \(t \ge 1\) and \(p\) be natural numbers with \(t < p \le 6t\). Then \(\lfloor 6t/p \rfloor - \lfloor 3t/p \rfloor - \lfloor 2t/p \rfloor \ge 1\).

This is the \(j = 1\) term of Legendre's formula for the exponent of \(p\) in \((6t)!/((3t)!\,(2t)!\,t!)\); on this range \(\lfloor t/p \rfloor = 0\).

lemma vp_term1 (t p : ℕ) (ht : 1 ≤ t) (hlo : t < p) (hhi : p ≤ 6 * t) :
    1 ≤ 6 * t / p - 3 * t / p - 2 * t / p

Uses 5 · Used by 1

Proof usesFloor-difference bound on the range 3t < p ≤ 6t · Floor-difference bound on the range 2t < p ≤ 3t · Floor-difference bound on the range 3t/2 < p ≤ 2t · Floor-difference bound on the range 6t/5 < p ≤ 3t/2 · Floor-difference bound on the range t < p ≤ 6t/5

Used byPrimes in \((t, 6t)\) occur in \(M(t)\)

LemmaPrimes in \((t, 6t)\) occur in \(M(t)\)#✓fully proved

For every natural number \(t \ge 1\) and every prime \(p\) with \(t < p \le 6t\), the exponent of \(p\) in the prime factorization of the multinomial coefficient \(M(t) = (6t)!/((3t)!\,(2t)!\,t!)\) is at least \(1\).

lemma vp_M34 (t : ℕ) (ht : 1 ≤ t) (p : ℕ) (hp : p.Prime)
    (hlo : t < p) (hhi : p ≤ 6 * t) : 1 ≤ (M34 t).factorization p

Uses 5 · 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)\) · Positivity of the multinomial coefficient \(M(t)\) · Superadditivity of floor division for three terms · Floor-difference bound on the range t < p ≤ 6t

Used bySplitting the primorial with a multinomial coefficient

LemmaSplitting the primorial with a multinomial coefficient#✓fully proved

For a natural number \(n\) let \(n\#\) be the primorial, the product of the primes \(p \le n\), and let \(M(t) = \frac{(6t)!}{(3t)!\,(2t)!\,t!}\). For every natural number \(m \ge 1\), with \(t = \lfloor (m+5)/6 \rfloor\), we have \(m\# \le t\# \cdot M(t)\).

lemma theta_le_M34 (m : ℕ) (hm : 1 ≤ m) :
    primorial m ≤ primorial ((m+5)/6) * M34 ((m+5)/6)

Uses 3 · Used by 1

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

Proof usesPositivity of the multinomial coefficient \(M(t)\) · Primes in \((t, 6t)\) occur in \(M(t)\)

Used byPrimorial bound by powers of 3.4, integer form

LemmaPrimorial bound \(3.4^m\) below \(133\)#✓fully proved

For a natural number \(n\) let \(n\#\) be the primorial, the product of the primes \(p \le n\). For every natural number \(m < 133\), \(10^m \cdot m\# \le 34^m\).

Proved by covering \(0 \le m \le 132\) with finitely many intervals \([a, b]\) and checking \(10^a \cdot b\# \le 34^a\) for each; this gives the bound on \([a, b]\) because \(n\#\) is nondecreasing in \(n\) and \(10 \le 34\).

lemma theta34_base : ∀ m : ℕ, m < 133 → 10^m * primorial m ≤ 34^m

Uses 1 · Used by 1

Proof usesExtending the primorial bound leftward across an interval

Used byPrimorial bound by powers of 3.4, integer form

LemmaPrimorial bound by powers of 3.4, integer form#✓fully proved

For every natural number \(m\), the primorial \(m\#\) (the product of all primes \(p \le m\)) satisfies \(10^m \cdot m\# \le 34^m\).

lemma theta34_nat (m : ℕ) : 10^m * primorial m ≤ 34^m

Uses 4 · Used by 1

Proof usesThe multinomial coefficient \(M(t)\) for the 3.4 primorial bound · Power bound for the multinomial coefficient \(M(t)\) · Primorial bound \(3.4^m\) below \(133\) · Splitting the primorial with a multinomial coefficient

Used byPrimorial bound by powers of 3.4, real form

LemmaPrimorial bound by powers of 3.4, real form#✓fully proved

For every real number \(x \ge 0\), the primorial of \(\lfloor x \rfloor\) (the product of all primes \(p \le \lfloor x \rfloor\)) is at most \(3.4^x\), where \(3.4^x\) is the real power.

lemma theta34_real {x : ℝ} (hx : 0 ≤ x) :
    (primorial ⌊x⌋₊ : ℝ) ≤ (3.4 : ℝ)^x

Uses 1 · Used by 1

Proof usesPrimorial bound by powers of 3.4, integer form

Used byChebyshev-type bound for the sum of prime logarithms

LemmaBounding a logarithm above by the exponential#✓fully proved

Let \(a\) and \(r\) be real numbers with \(a > 0\). If \(a < e^r\), then \(\log a < r\), where \(\log\) is the natural logarithm.

lemma log_lt_of_exp_gt {a r : ℝ} (ha : 0 < a) (h : a < Real.exp r) :
    Real.log a < r

Used by 3

Used byUpper bound for log 3 · Upper bound for log 10 · Upper bound for log 17

LemmaLogarithm lower bound from an exponential bound#✓fully proved

For real numbers \(a > 0\) and \(r\), if \(e^r < a\) then \(r < \log a\), where \(\log\) is the natural logarithm.

lemma log_gt_of_exp_lt {a r : ℝ} (ha : 0 < a) (h : Real.exp r < a) :
    r < Real.log a

Used by 2

Used byLower bound for log 2 · Lower bound for log 5

LemmaExponential lower bound from a power comparison#✓fully proved

Let \(a\) and \(c\) be nonnegative real numbers and let \(n\) and \(m\) be positive integers. If \(c < e\) and \(a^n < c^m\), then \(a < e^{m/n}\), where \(m/n\) is real division.

lemma lt_exp_of_pow_lt {a c : ℝ} {n m : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) (hm : m ≠ 0)
    (hc : c < Real.exp 1) (hc0 : 0 ≤ c) (h : a ^ n < c ^ m) :
    a < Real.exp ((m : ℝ) / n)

Used by 3

Used byUpper bound for log 3 · Upper bound for log 10 · Upper bound for log 17

LemmaPower comparison above e bounds an exponential#✓fully proved

Let \(e\) be Euler's number, let \(a\) and \(c\) be real numbers and let \(m, n\) be nonzero natural numbers, with \(a \ge 0\), \(e^{m/n} \ge 0\) and \(c > e\). If \(c^m < a^n\), then \(e^{m/n} < a\).

lemma exp_lt_of_pow_lt {a c : ℝ} {n m : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) (hm : m ≠ 0)
    (hc : Real.exp 1 < c) (ha0 : 0 ≤ Real.exp ((m : ℝ) / n)) (h : c ^ m < a ^ n) :
    Real.exp ((m : ℝ) / n) < a

Used by 2

Used byLower bound for log 2 · Lower bound for log 5

LemmaLower bound for log 2#✓fully proved

The natural logarithm of \(2\) satisfies \(0.6931 < \log 2\).

lemma log2_gt : (0.6931 : ℝ) < Real.log 2

Uses 2 · Used by 2

Proof usesPower comparison above e bounds an exponential · Logarithm lower bound from an exponential bound

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

LemmaLower bound for log 5#✓fully proved

The natural logarithm of \(5\) satisfies \(1.6094 < \log 5\).

lemma log5_gt : (1.6094 : ℝ) < Real.log 5

Uses 2 · Used by 2

Proof usesPower comparison above e bounds an exponential · Logarithm lower bound from an exponential bound

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

LemmaUpper bound for log 3#✓fully proved

The natural logarithm of \(3\) satisfies \(\log 3 < 1.0987\).

lemma log3_lt : Real.log 3 < (1.0987 : ℝ)

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

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.