Basic definitions

Mathlib does not (yet) have polylogarithms or Catalan's constant, so we define them here by their series.

• LeanPolyLog.Li s z: the polylogarithm Li_s(z) = ∑_{n ≥ 1} z^n / n^s on ℂ.
• LeanPolyLog.Lir s x: the same series on ℝ.
• LeanPolyLog.G: Catalan's constant ∑_{n ≥ 0} (-1)^n / (2n+1)^2.
• LeanPolyLog.zeta3: Apéry's constant ∑_{n ≥ 1} 1/n^3.

For s ≥ 2 the polylog series converges absolutely on the closed unit disk. Outside the disk tsum returns the junk value 0. Every statement in this project therefore evaluates Li only for ‖z‖ ≤ 1; for instance A014 is stated in a form that avoids Li₃(1+i).

noncomputable def LeanPolyLog.Li (s : ℕ) (z : ℂ) : ℂ

The polylogarithm Li_s(z) = ∑_{n=1}^∞ z^n / n^s, as a series. Meaningful for ‖z‖ ≤ 1 and s ≥ 2.

Equations

• LeanPolyLog.Li s z = ∑' (n : ℕ), z ^ (n + 1) / (↑n + 1) ^ s

noncomputable def LeanPolyLog.Lir (s : ℕ) (x : ℝ) : ℝ

The real polylogarithm Li_s(x) = ∑_{n=1}^∞ x^n / n^s, meaningful for |x| ≤ 1 and s ≥ 2.

Equations

• LeanPolyLog.Lir s x = ∑' (n : ℕ), x ^ (n + 1) / (↑n + 1) ^ s

noncomputable def LeanPolyLog.G : ℝ

Catalan's constant G = ∑_{n=0}^∞ (-1)^n / (2n+1)^2 ≈ 0.9159655941772190.

Equations

• LeanPolyLog.G = ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) ^ 2

noncomputable def LeanPolyLog.zeta3 : ℝ

Apéry's constant ζ(3) = ∑_{n=1}^∞ 1/n^3 ≈ 1.2020569031595943.

Equations

• LeanPolyLog.zeta3 = ∑' (n : ℕ), 1 / (↑n + 1) ^ 3