A014: ∫₀¹ log x · log(1+x)/(1+x²) dx = 11π³/128 + (3π/32) log²2 - 2G log 2 - 3 Im Li₃((1+i)/2)

As in the tutorial, log x · log(1+x) = ½ (log² x + log²(1+x) - log²(x/(1+x))) splits the integral as ½ (𝒦 + ℳ - 𝒥), where

• 𝒦 = ∫₀¹ log² x/(1+x²) dx = π³/16 (LeanPolyLog.Arctan.integral_log_sq_div_one_add_sq),
• ℳ = ∫₀¹ log²(1+x)/(1+x²) dx = 7π³/64 + (3π/16) log²2 - 2G log 2 - 4 Im Li₃((1+i)/2) (LeanPolyLog.Trilog.integral_log_one_add_sq_div_one_add_sq),
• 𝒥 = ∫₀¹ log²(x/(1+x))/(1+x²) dx = 2G log 2 + 2 Im Li₃((1+i)/2) (LeanPolyLog.Trilog.integral_log_sub_log_sq_div_one_add_sq).

The tutorial evaluates ℳ through Li₃(1+i), outside the unit disk, where the series Li is not defined. Here ℳ and 𝒥 come from explicit complex primitives whose polylogarithms are only evaluated at points of norm at most 1: ψ(x) = ((1-x) + (1+x)i)/2 and φ(x) = (x-i)/(x+1) for ℳ, and χ(x) = x(1-i)/(1+x) for 𝒥.

theorem LeanPolyLog.Proofs.A014 : ∫ (x : ℝ) in 0..1, Real.log x * Real.log (x + 1) / (x ^ 2 + 1) = 11 * Real.pi ^ 3 / 128 + 3 * Real.pi / 32 * Real.log 2 ^ 2 - 2 * G * Real.log 2 - 3 * (Li 3 ((1 + Complex.I) / 2)).im

A014 (simplified form): ∫₀¹ log x · log(1+x) / (1+x²) dx = 11π³/128 + (3π/32) log²2 - 2G log 2 - 3 Im Li₃((1+i)/2).