A004: ∫₀¹ log(1+x²)/x dx = π²/24

On (0, 1) we have log(1+x²)/x = ∑_{n ≥ 0} (-1)ⁿ x^(2n+1)/(n+1). The integrals of the absolute values of the terms are 1/(2(n+1)²), which are summable, so the series may be integrated term by term (MeasureTheory.hasSum_integral_of_summable_integral_norm). The result is ∑_{n ≥ 0} (-1)ⁿ/(2(n+1)²) = η(2)/2 = π²/24.

In Lean the integrand at x = 0 is log 1 / 0 = 0; a single point does not affect the integral.

theorem LeanPolyLog.Proofs.A004 : ∫ (x : ℝ) in 0..1, Real.log (1 + x ^ 2) / x = Real.pi ^ 2 / 24

A004 (corrected): ∫₀¹ log(1+x²)/x dx = π²/24.