Bounds on the partial sums of the logarithm

The partial sum ∑ n ∈ Finset.Ioc 0 N, Real.log n equals Real.log N !. Comparing the sum with the integral ∫ t in 1..x, Real.log t = x * log x - x + 1 yields crude upper and lower bounds of the form ∑ n ∈ Ioc 0 ⌊x⌋₊, log n = x * log x - x + O(log x), which are convenient in analytic number theory (for instance in the proof of Mertens' theorems).

Main statements

• sum_log_eq_log_factorial: ∑ n ∈ Ioc 0 N, log n = log N !, and its Finset.range restatement sum_log_add_one_eq_log_factorial: ∑ n ∈ range N, log (n + 1) = log N !.
• sum_log_le / le_sum_log: two-sided bounds on ∑ n ∈ Ioc 0 ⌊x⌋₊, log n.
• le_sum_log_nat: a sharper lower bound N * log N - N ≤ ∑ n ∈ Ioc 0 N, log n via Stirling.

theorem Real.sum_log_eq_log_factorial (N : ℕ) : ∑ n ∈ Finset.Ioc 0 N, log ↑n = log ↑N.factorial

The partial sum of the logarithm is equal to the log of the factorial.

theorem Real.sum_log_add_one_eq_log_factorial (N : ℕ) : ∑ n ∈ Finset.range N, log (↑n + 1) = log ↑N.factorial

The partial sum of the logarithm, in Finset.range form: ∑ n ∈ range N, log (n + 1).

theorem Real.sum_log_le {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, log ↑n ≤ x * log x - x + log x + 1

A crude upper bound on the partial sum of the logarithm.

theorem Real.sum_log_le' {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, log ↑n ≤ x * log x

An even cruder upper bound on the partial sum of the logarithm.

theorem Real.le_sum_log {x : ℝ} (hx : 1 ≤ x) : x * log x - x - log x + 1 ≤ ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, log ↑n

A crude lower bound on the partial sum of the logarithm.

theorem Real.le_sum_log' {x : ℝ} (hx : 1 ≤ x) : x * log x - 2 * x ≤ ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, log ↑n

An even cruder lower bound on the partial sum of the logarithm.

theorem Real.le_sum_log_nat (N : ℕ) : ↑N * log ↑N - ↑N ≤ ∑ n ∈ Finset.Ioc 0 N, log ↑n

A sharper bound on the partial sum of the logarithm in the natural number case.