A002: Li₂(1/(1+i)) = 5π²/96 - log²2/8 + i(π log 2 / 8 - G)

Landen's identity Li₂(z) + Li₂(z/(z-1)) = -½ log²(1 - z) at z = i, where i/(i-1) = 1/(1+i), gives Li₂(1/(1+i)) = -½ log²(1 - i) - Li₂(i). Then:

• log(1 - i) = ½ log 2 - (π/4) i, so -½ log²(1 - i) = π²/32 - log²2/8 + i π log 2 / 8;
• Li₂(i) = -π²/48 + iG (A001).

The real parts add up to π²/32 + π²/48 - log²2/8 = 5π²/96 - log²2/8.

theorem LeanPolyLog.Proofs.A002 : Li 2 (1 / (1 + Complex.I)) = ↑(5 * Real.pi ^ 2 / 96 - Real.log 2 ^ 2 / 8) + ↑(Real.pi / 8 * Real.log 2 - G) * Complex.I

A002: Li₂(1/(1+i)) = 5π²/96 - log²2/8 + i(π log 2 / 8 - G).