A011: ∫₀¹ Li₂(x) / (x √(1-x²)) dx = (3/8) π² log 2 - (7/16) ζ(3)

The weight w(y) = -log y has the moments ∫₀¹ yⁿ (-log y) 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 + φ) dφ = (π/2)·(π/2) log 2 - J, where J = ∫₀^{π/2} φ log sin φ dφ = -(π²/8) log 2 + (7/16) ζ(3) is LeanPolyLog.Proofs.integral_mul_log_sin, proved on the way to A009.

theorem LeanPolyLog.Proofs.A011 : ∫ (x : ℝ) in 0..1, Lir 2 x / (x * √(1 - x ^ 2)) = 3 / 8 * Real.pi ^ 2 * Real.log 2 - 7 / 16 * zeta3

A011: ∫₀¹ Li₂(x) / (x √(1-x²)) dx = (3/8) π² log 2 - (7/16) ζ(3).