Stirling-type bounds used in Section 6 of the paper

• log_factorial_le : log m! ≤ m log m - m + (log m)/2 + 1 for m ≥ 1;
• log_factorial_ge : m log m - m ≤ log m!;
• sum_log_factorial_two_mul_ge : ∑_{i=1}^{h-1} log (2i)! ≥ h² log 2h - (3/2) h² - 2h log 2h, the bound displayed before (6.15) in the paper.

theorem Zeta5Irrational.log_factorial_le {m : ℕ} (hm : 1 ≤ m) : Real.log ↑m.factorial ≤ ↑m * Real.log ↑m - ↑m + Real.log ↑m / 2 + 1

theorem Zeta5Irrational.log_factorial_ge (m : ℕ) : ↑m * Real.log ↑m - ↑m ≤ Real.log ↑m.factorial

noncomputable def Zeta5Irrational.Gaux (x : ℝ) : ℝ

An antiderivative of x log (2x).

Equations

• Zeta5Irrational.Gaux x = x ^ 2 / 2 * Real.log (2 * x) - x ^ 2 / 4

theorem Zeta5Irrational.hasDerivAt_Gaux {x : ℝ} (hx : 0 < x) : HasDerivAt Gaux (x * Real.log (2 * x)) x

theorem Zeta5Irrational.integral_x_log {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : ∫ (x : ℝ) in a..b, x * Real.log (2 * x) = Gaux b - Gaux a

theorem Zeta5Irrational.monotoneOn_x_log : MonotoneOn (fun (x : ℝ) => x * Real.log (2 * x)) (Set.Ici 1)

theorem Zeta5Irrational.sum_range_cast (m : ℕ) : ∑ k ∈ Finset.range m, ↑k = ↑m * (↑m - 1) / 2

theorem Zeta5Irrational.sum_log_factorial_two_mul_ge {h : ℕ} (hh : 2 ≤ h) : ↑h ^ 2 * Real.log (2 * ↑h) - 3 / 2 * ↑h ^ 2 - 2 * ↑h * Real.log (2 * ↑h) ≤ ∑ i ∈ Finset.Icc 1 (h - 1), Real.log ↑(2 * i).factorial

∑_{i=1}^{h-1} log (2i)! ≥ h² log (2h) - (3/2) h² - 2 h log (2h).