A007: ∫₀^{π/4} x log cos x dx = πG/8 - (π²/32) log 2 - (21/128) ζ(3)

LeanPool.PolylogIntegrals.Lemmas.Fourier computes `∫₀^{π/4} x log (2 + 2 cos 2x) dx = (π/4) G

• (21/64) ζ(3)by integrating the Fourier series oflog (1 + 2r cos 2x + r²)term by term and lettingr → 1⁻. On [0, π/4]we have2 + 2 cos 2x = 4 cos² x, so log (2 + 2 cos 2x) = 2 log 2 + 2 log cos x, and ∫₀^{π/4} x dx = π²/32`.

theorem LeanPolyLog.Proofs.A007 : ∫ (x : ℝ) in 0..Real.pi / 4, x * Real.log (Real.cos x) = Real.pi * G / 8 - Real.pi ^ 2 / 32 * Real.log 2 - 21 / 128 * zeta3

A007: ∫₀^{π/4} x log cos x dx = πG/8 - (π²/32) log 2 - (21/128) ζ(3).