Positivity of the scaled factorial argument \(N_{10}\) to Exact formula for the scaled factorial argument \(N_{10}\)

LemmaPositivity of the scaled factorial argument \(N_{10}\)#✓fully proved

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

lemma N10_pos {m n : ℕ} (hn : 1 ≤ n) (hm1 : 1 ≤ m) (hd : m ∣ Q9) :
    1 ≤ N10m m n

Uses 3 · Used by 2

Statement usesScaled factorial argument \(N_{10}\) · The modulus \(Q_9 = 210\)

Proof usesQuotients of Q₉ by its divisors are positive

Used byTermwise Stirling lower bound in Breusch's argument · Lower bound for \(\log F_9(n)\)

LemmaPositivity of the scaled argument N₉#✓fully proved

For natural numbers \(m\) and \(n\) with \(n \ge 1\), \(m \ge 1\) and \(m\) dividing \(Q_9 = 210\), the scaled factorial argument \(N_9(m, n) = 9n \lfloor Q_9 / m \rfloor\) satisfies \(N_9(m, n) \ge 1\).

lemma N9_pos {m n : ℕ} (hn : 1 ≤ n) (hm1 : 1 ≤ m) (hd : m ∣ Q9) :
    1 ≤ N9m m n

Uses 3 · Used by 2

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

Proof usesQuotients of Q₉ by its divisors are positive

Used byTermwise Stirling lower bound in Breusch's argument · Lower bound for \(\log F_9(n)\)

LemmaPositivity of 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 \(n \ge 1\), \(m \ge 1\) and \(m\) divides \(Q_9\), then \(N_1(m, n) \ge 1\).

lemma N1_pos {m n : ℕ} (hn : 1 ≤ n) (hm1 : 1 ≤ m) (hd : m ∣ Q9) :
    1 ≤ N1m m n

Uses 3 · Used by 2

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

Proof usesQuotients of Q₉ by its divisors are positive

Used byTermwise Stirling lower bound in Breusch's argument · Lower bound for \(\log F_9(n)\)

LemmaUpper bound for the scaled factorial argument \(N_{10}\)#✓fully proved

Let \(Q_9 = 210\) and, for natural numbers \(m\) and \(n\), let \(N_{10}(m, n) = 10 n \lfloor Q_9 / m \rfloor\), where \(\lfloor Q_9 / 0 \rfloor\) is taken to be \(0\). Then \(N_{10}(m, n) \le 10 Q_9 n\) for all natural numbers \(m\) and \(n\).

lemma N10_le {m n : ℕ} : N10m m n ≤ 10 * Q9 * n

Uses 2 · Used by 3

Statement usesScaled factorial argument \(N_{10}\) · The modulus \(Q_9 = 210\)

Used byLower bound for \(\log F_9(n)\) · Valuation identity for the weighted product · Bound on the prime factors of the ratio factors

LemmaUpper bound 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\), where \(\lfloor Q_9 / 0 \rfloor\) is taken to be \(0\). Then \(N_9(m, n) \le 10 Q_9 n\) for all natural numbers \(m\) and \(n\).

lemma N9_le {m n : ℕ} : N9m m n ≤ 10 * Q9 * n

Uses 2 · Used by 2

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

Used byLower bound for \(\log F_9(n)\) · Valuation identity for the weighted product

LemmaUpper bound 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\), where \(\lfloor Q_9 / 0 \rfloor\) is taken to be \(0\). Then \(N_1(m, n) \le 10 Q_9 n\) for all natural numbers \(m\) and \(n\).

lemma N1_le {m n : ℕ} : N1m m n ≤ 10 * Q9 * n

Uses 2 · Used by 2

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

Used byLower bound for \(\log F_9(n)\) · Valuation identity for the weighted product

LemmaN₁₀ splits as N₉ + N₁#✓fully proved

For natural numbers \(m\) and \(n\) with \(m \ge 1\) and \(m\) dividing \(Q_9 = 210\), write \(N_k(m, n) = kn \lfloor Q_9 / m \rfloor\) for \(k = 1, 9, 10\). Then \(N_{10}(m, n) = N_9(m, n) + N_1(m, n)\).

lemma Nadd9 {m n : ℕ} (hm1 : 1 ≤ m) (hd : m ∣ Q9) :
    N10m m n = N9m m n + N1m m n

Uses 4 · Used by 1

Statement usesScaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉ · The modulus \(Q_9 = 210\)

Used byFactorial divisibility behind ratio₉

LemmaFactorial divisibility behind ratio₉#✓fully proved

For natural numbers \(m\) and \(n\) with \(m \ge 1\) and \(m\) dividing \(Q_9 = 210\), write \(N_k(m, n) = kn \lfloor Q_9 / m \rfloor\) for \(k = 1, 9, 10\). Then \(N_9(m, n)! \cdot N_1(m, n)!\) divides \(N_{10}(m, n)!\).

lemma ratio9_dvd (m n : ℕ) (hm1 : 1 ≤ m) (hd : m ∣ Q9) :
    (N9m m n)! * (N1m m n)! ∣ (N10m m n)!

Uses 5 · Used by 4

Statement usesScaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉ · The modulus \(Q_9 = 210\)

Proof usesN₁₀ splits as N₉ + N₁

Used byLogarithm of the binomial factor · Positivity of ratio₉ · Valuation of a factorial ratio as a difference of valuations · Bound on the prime factors of the ratio factors

LemmaPositivity of ratio₉#✓fully proved

For natural numbers \(m\) and \(n\) with \(n \ge 1\), \(m \ge 1\) and \(m\) dividing \(Q_9 = 210\), the binomial factor \(\mathrm{ratio}_9(m, n) = N_{10}(m, n)! / (N_9(m, n)! \cdot N_1(m, n)!)\) is positive, where \(N_k(m, n) = kn \lfloor Q_9 / m \rfloor\) for \(k = 1, 9, 10\).

lemma ratio9_pos (m n : ℕ) (_hn : 1 ≤ n) (hm1 : 1 ≤ m) (hd : m ∣ Q9) :
    0 < ratio9 m n

Uses 6 · Used by 1

Statement usesThe modulus \(Q_9 = 210\) · Binomial factor ratio₉

Proof usesScaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉ · Factorial divisibility behind ratio₉

Used byA weighted log-factor as a sum over primes

LemmaLogarithm of the binomial factor#✓fully proved

Let \(m\) and \(n\) be natural numbers with \(n \ge 1\), \(m \ge 1\) and \(m \mid 210\), and put \(k = 210/m\). Then

\[\log \frac{(10nk)!}{(9nk)!\,(nk)!} = \log (10nk)! - \log (9nk)! - \log (nk)!.\]

lemma log_ratio9 (m n : ℕ) (_hn : 1 ≤ n) (hm1 : 1 ≤ m) (hd : m ∣ Q9) :
    Real.log ((ratio9 m n : ℕ) : ℝ)
      = Real.log (((N10m m n)!) : ℝ) - Real.log (((N9m m n)!) : ℝ)
        - Real.log (((N1m m n)!) : ℝ)

Uses 6 · Used by 1

Statement usesScaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉ · The modulus \(Q_9 = 210\) · Binomial factor ratio₉

Proof usesFactorial divisibility behind ratio₉

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

LemmaMöbius reciprocal sum over the divisors of 210, in the rationals#✓fully proved

Let \(w_9\) be the table of pairs \((d, \mu(d))\), where \(d\) runs over the divisors of \(210\) and \(\mu\) is the Möbius function. Then the sum of \(\mu(d)/d\) over the pairs of \(w_9\), computed in \(\mathbb{Q}\), is \(8/35\); that is, \(\sum_{d \mid 210} \mu(d)/d = 8/35\).

lemma w9_mu_sum_Q : w9.toFinset.sum (fun q : ℕ × ℤ => (q.2 : ℚ) / (q.1 : ℚ)) = 8/35

Uses 3 · Used by 1

Statement usesThe Möbius divisor table for \(210\)

Proof usesSum over a duplicate-free list · The divisor table for \(210\) has no repeated entries

Used byMöbius reciprocal sum over the divisors of 210, in the reals

LemmaMöbius reciprocal sum over the divisors of 210, in the reals#✓fully proved

Let \(w_9\) be the table of pairs \((d, \mu(d))\), where \(d\) runs over the divisors of \(210\) and \(\mu\) is the Möbius function. Then the sum of \(\mu(d)/d\) over the pairs of \(w_9\), computed in \(\mathbb{R}\), is \(8/35\); that is, \(\sum_{d \mid 210} \mu(d)/d = 8/35\).

lemma w9_mu_sum_R : w9.toFinset.sum (fun q : ℕ × ℤ => (q.2 : ℝ) / (q.1 : ℝ)) = 8/35

Uses 2 · Used by 1

Statement usesThe Möbius divisor table for \(210\)

Proof usesMöbius reciprocal sum over the divisors of 210, in the rationals

Used byClosed form of the Möbius-weighted main-term sum

LemmaLower bound for \(\log N!\)#✓fully proved

For every natural number \(N \ge 1\), \(N \log N - N + 1 \le \log N!\).

lemma log_fact_lower {N : ℕ} (hN : 1 ≤ N) :
    (N : ℝ) * Real.log (N : ℝ) - (N : ℝ) + 1 ≤ Real.log ((N ! : ℕ) : ℝ)

Uses 1 · Used by 1

Proof usesWeak Stirling lower bound for factorials

Used byTermwise Stirling lower bound in Breusch's argument

LemmaUpper bound for \(\log N!\)#✓fully proved

For every natural number \(N \ge 1\), \(\log N! \le (N + 1) \log N - N + 1\).

lemma log_fact_upper {N : ℕ} (hN : 1 ≤ N) :
    Real.log ((N ! : ℕ) : ℝ) ≤ ((N : ℝ)+1) * Real.log (N : ℝ) - (N : ℝ) + 1

Uses 1 · Used by 1

Proof usesWeak Stirling upper bound for factorials

Used byTermwise Stirling lower bound in Breusch's argument

DefinitionMain Stirling term#✓fully proved

For a real number \(x\), \(f_{\mathrm{main}}(x) = x \log x - x\).

This is the main term of Stirling's approximation to \(\log x!\).

noncomputable def fmain (x : ℝ) : ℝ := x * Real.log x - x

Used by 4

Used byTermwise Stirling lower bound in Breusch's argument · Closed form of the Möbius-weighted main-term sum · Lower bound for \(\log F_9(n)\) · Combined main term of the Möbius-weighted Stirling sums

LemmaTermwise Stirling lower bound in Breusch's argument#✓fully proved

Let \((d, \varepsilon)\) be a pair in the Möbius divisor table \(W_9\) for \(Q_9 = 210\) and let \(n \ge 1\) be a natural number. Write \(q = \lfloor Q_9 / d \rfloor\) for the natural-number quotient, and let \(A = N_{10}(d, n) = 10nq\), \(B = N_9(d, n) = 9nq\) and \(C = N_1(d, n) = nq\) be the scaled factorial arguments and \(f_{\mathrm{main}}(x) = x \log x - x\) the main Stirling term. Then \(\varepsilon (\log A! - \log B! - \log C!) \ge \varepsilon (f_{\mathrm{main}}(A) - f_{\mathrm{main}}(B) - f_{\mathrm{main}}(C)) - (1 + \log A + \log B + \log C)\).

lemma logF9_term_lower (q : ℕ × ℤ) (hq : q ∈ w9) (n : ℕ) (hn : 1 ≤ n) :
    (q.2 : ℝ) * (Real.log (((N10m q.1 n)!) : ℝ) - Real.log (((N9m q.1 n)!) : ℝ)
      - Real.log (((N1m q.1 n)!) : ℝ))
    ≥ (q.2 : ℝ) * (fmain ((N10m q.1 n : ℕ) : ℝ) - fmain ((N9m q.1 n : ℕ) : ℝ)
      - fmain ((N1m q.1 n : ℕ) : ℝ))
      - (1 + Real.log ((N10m q.1 n : ℕ) : ℝ) + Real.log ((N9m q.1 n : ℕ) : ℝ)
        + Real.log ((N1m q.1 n : ℕ) : ℝ))

Uses 14 · Used by 1

Statement usesScaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉ · Main Stirling term · The Möbius divisor table for \(210\)

Proof usesPositivity of the scaled factorial argument \(N_{10}\) · Positivity of the scaled factorial argument \(N_1\) · Positivity of the scaled argument N₉ · The modulus \(Q_9 = 210\) · Lower bound for \(\log N!\) · Upper bound for \(\log N!\) · Entries of the divisor table for \(210\) divide \(210\) · Signs in the divisor table for \(210\) · Divisors in the table for \(210\) are positive

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

LemmaDivisors of 210 divide multiples of 210#✓fully proved

Let \(w_9\) be the table of divisors \(d\) of \(Q_9 = 210\) paired with their Möbius values. If \(C\) is a natural number with \(Q_9 \mid C\), then for every pair \((d, \varepsilon)\) in \(w_9\) and every natural number \(n\), \(d \mid C n\).

lemma CNdvd9 (C : ℕ) (hC : Q9 ∣ C) (q : ℕ × ℤ) (hq : q ∈ w9) (n : ℕ) :
    q.1 ∣ C * n

Uses 3 · Used by 1

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

Proof usesEntries of the divisor table for \(210\) divide \(210\)

Used byClosed form of the Möbius-weighted main-term sum

DefinitionThe constant \(K_9\)#✓fully proved

Let \(w_9\) be the table of divisors \(d\) of \(Q_9 = 210\) paired with their Möbius values \(\varepsilon\). Then

\[K_9 = \sum_{(d, \varepsilon) \in w_9} \frac{\varepsilon \log d}{d}.\]

It comes from the \(\log d\) terms in the closed form of \(\sum_{(d, \varepsilon) \in w_9} \varepsilon f(N/d)\) with \(f(x) = x \log x - x\), for \(N\) a multiple of \(210\).

noncomputable def K9 : ℝ :=
  w9.toFinset.sum (fun q : ℕ × ℤ => (q.2 : ℝ) * Real.log (q.1 : ℝ) / (q.1 : ℝ))

Uses 1 · Used by 2

Statement usesThe Möbius divisor table for \(210\)

Used byClosed form of the Möbius-weighted main-term sum · Combined main term of the Möbius-weighted Stirling sums

LemmaClosed form of the Möbius-weighted main-term sum#✓fully proved

Let \(w_9\) be the table of pairs \((d, \mu(d))\) for the divisors \(d\) of \(210\), let \(f(x) = x \log x - x\), and let \(K_9 = \sum_{(d, \mu(d)) \in w_9} \mu(d) \log d / d\). For natural numbers \(C > 0\) and \(n \ge 1\) with \(210 \mid C\), writing \(N = Cn\) (so that \(N/d\) is an integer for each \(d\) in \(w_9\)), we have \(\sum_{(d, \mu(d)) \in w_9} \mu(d) f(N/d) = \frac{8}{35} N (\log N - 1) - K_9 N\).

lemma Z9_value (C n : ℕ) (hC0 : 0 < C) (hn : 1 ≤ n) (hC : Q9 ∣ C) :
    w9.toFinset.sum (fun q : ℕ × ℤ => (q.2 : ℝ) * fmain (((C*n/q.1 : ℕ)) : ℝ))
    = (8/35) * ((C*n : ℕ):ℝ) * (Real.log ((C*n : ℕ):ℝ) - 1)
      - K9 * ((C*n : ℕ):ℝ)

Uses 7 · Used by 1

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

Proof usesDivisors of 210 divide multiples of 210 · Möbius reciprocal sum over the divisors of 210, in the reals · Divisors in the table for \(210\) are positive

Used byCombined main term of the Möbius-weighted Stirling sums

LemmaExact formula for the scaled factorial argument \(N_{10}\)#✓fully proved

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

lemma N10_eq {m n : ℕ} (hm1 : 1 ≤ m) (hd : m ∣ Q9) : N10m m n = 10*Q9*n/m

Uses 2 · Used by 2

Statement usesScaled factorial argument \(N_{10}\) · The modulus \(Q_9 = 210\)

Used byLower bound for \(\log F_9(n)\) · Legendre terms of \(N_{10}\) as real floors

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.