A013: ∫₀¹ arctan x / (x+1) · log² x dx = -(π²/24) G - (π³/32) log 2 + (21π/64) ζ(3) #
Integrate by parts with u = arctan x and
H(x) = -2 Li₃(-x) + 2 log x · Li₂(-x) + log(1+x) log² x, an antiderivative of log² x/(1+x)
that is continuous on [0, 1] with H(0) = 0. The boundary term is
(π/4) H(1) = (π/4) (-2 Li₃(-1)) = (3π/8) ζ(3), and the remaining integral splits as
∫₀¹ H(x)/(1+x²) dx = -2 𝒥 + 2 𝒦 + ℳ, where
𝒥 = ∫₀¹ Li₃(-x)/(1+x²) dx,𝒦 = ∫₀¹ log x · Li₂(-x)/(1+x²) dx = π² G/48(LeanPolyLog.Arctan.integral_log_mul_Lir_two_neg_div_one_add_sq),ℳ = ∫₀¹ log(1+x) log² x/(1+x²) dx.
Writing Li₃(-x) = -½ ∫₀¹ x log² y/(1+xy) dy and swapping the order of integration turns 𝒥
into -½ ∫₀¹ log² y · K(y) dy, with the same kernel K(y) = (log 2/2 + πy/4 - log(1+y))/(1+y²)
as in A012. Hence -2 𝒥 = (log 2/2)(π³/16) + (π/4)(3/16) ζ(3) - ℳ, and ℳ cancels.