A016: ∫₀¹ Li₃(x) / (x √(1-x²)) dx = Li₄(1/2)/2 + 41π⁴/5760 + log⁴2/48 + π² log²2/6

The weight w(y) = log² y / 2 has the moments ∫₀¹ yⁿ log² y / 2 dy = 1/(n+1)³, so LeanPolyLog.Arcsin.integral_Lir_div_mul_sqrt (Fubini, then y = sin φ) gives ∫₀¹ Li₃(x) / (x √(1-x²)) dx = ∫₀^{π/2} (log² sin φ / 2) (π/2 + φ) dφ = (π/4) L + A015/2, where L = ∫₀^{π/2} log² sin φ dφ = π³/24 + (π/2) log² 2 is LeanPolyLog.LogSinSq.integral_log_sin_sq and A015 is ∫₀^{π/2} φ log² sin φ dφ.

theorem LeanPolyLog.Proofs.A016 : ∫ (x : ℝ) in 0..1, Lir 3 x / (x * √(1 - x ^ 2)) = Lir 4 (1 / 2) / 2 + 41 * Real.pi ^ 4 / 5760 + Real.log 2 ^ 4 / 48 + Real.pi ^ 2 * Real.log 2 ^ 2 / 6

A016: ∫₀¹ Li₃(x) / (x √(1-x²)) dx = Li₄(1/2)/2 + 41π⁴/5760 + log⁴2/48 + π² log²2/6.