The dilogarithm

Mathlib has no polylogarithms, so this file collects the facts about Li_s that the proofs use, with the dilogarithm Li_2 as the main case. Lir s and Li s both unfold to the series ∑_{n ≥ 0} z^(n+1)/(n+1)^s, so its basic properties are proved once, over 𝕜 = ℝ or ℂ (RCLike). The complex counterparts are in LeanPool.PolylogIntegrals.Lemmas.DilogComplex.

Main results

The series over 𝕜 = ℝ or ℂ:

• LeanPolyLog.Dilog.summable_pow_div_pow, LeanPolyLog.Dilog.continuousOn_tsum_pow_div_pow: for s ≥ 2 it converges absolutely, and is continuous, on the closed unit disk (M-test).
• LeanPolyLog.Dilog.hasDerivAt_tsum_pow_div_pow: termwise differentiation on the open disk.
• LeanPolyLog.Dilog.tsum_pow_div_pow_sq: the duplication formula.

The real polylogarithm Lir:

• LeanPolyLog.Dilog.Lir_one: Li_1(x) = -log(1 - x) for |x| < 1.
• LeanPolyLog.Dilog.Lir_two_one, LeanPolyLog.Dilog.Lir_two_neg_one, LeanPolyLog.Dilog.Lir_two_one_half: Li_2(1) = π²/6, Li_2(-1) = -π²/12 and Li_2(1/2) = π²/12 - log²2/2.
• LeanPolyLog.Dilog.continuousOn_Lir: for s ≥ 2, Li_s is continuous on [-1, 1].
• LeanPolyLog.Dilog.hasDerivAt_Lir_succ, LeanPolyLog.Dilog.hasDerivAt_Lir_two: for 0 < |x| < 1, Li_(s+1)'(x) = Li_s(x)/x; in particular Li_2'(x) = -log(1 - x)/x.
• LeanPolyLog.Dilog.Lir_sq, LeanPolyLog.Dilog.Lir_two_sq: the duplication formula Li_s(x²) = 2^(s-1) (Li_s(x) + Li_s(-x)) for |x| ≤ 1.
• LeanPolyLog.Dilog.Lir_two_add_Lir_two_one_sub: Euler's reflection formula Li_2(x) + Li_2(1 - x) = π²/6 - log x · log(1 - x) for 0 < x < 1.
• LeanPolyLog.Dilog.Lir_two_neg_add_Lir_two_div: Landen's identity Li_2(-y) + Li_2(y/(1+y)) = -½ log²(1+y) for 0 ≤ y ≤ 1.

Proof sketch

The derivative comes from termwise differentiation on a ball of radius r < 1, where the derivatives of the terms are bounded by rⁿ; the derivative series ∑ xⁿ/(n+1)^s equals Li_s(x)/x, and Li_1(x) = -log(1 - x) is Mathlib's Real.hasSum_pow_div_log_of_abs_lt_one. The duplication formula splits the series into even and odd terms. Reflection and Landen are proved by showing that the difference of the two sides is continuous on a closed interval with derivative 0 inside (LeanPolyLog.Dilog.eq_of_hasDerivAt_eq_zero, from the mean value theorem), and evaluating it at 0. For reflection this needs the continuity of log t · log(1 - t) at 0 (LeanPolyLog.Dilog.continuous_log_mul_log_one_sub).

The polylog series over ℝ or ℂ

theorem LeanPolyLog.Dilog.norm_pow_div_pow {𝕜 : Type u_1} [RCLike 𝕜] (s n : ℕ) (z : 𝕜) : ‖z ^ (n + 1) / (↑n + 1) ^ s‖ = ‖z‖ ^ (n + 1) / (↑n + 1) ^ s

The norm of the n-th term of the polylog series.

theorem LeanPolyLog.Dilog.summable_one_div_succ_pow {s : ℕ} (hs : 2 ≤ s) : Summable fun (n : ℕ) => 1 / (↑n + 1) ^ s

∑_{n ≥ 0} 1/(n+1)^s converges for s ≥ 2.

theorem LeanPolyLog.Dilog.norm_pow_div_pow_le {𝕜 : Type u_1} [RCLike 𝕜] {s : ℕ} {z : 𝕜} (hz : ‖z‖ ≤ 1) (n : ℕ) : ‖z ^ (n + 1) / (↑n + 1) ^ s‖ ≤ 1 / (↑n + 1) ^ s

On the closed unit disk, the n-th term of the polylog series is bounded by 1/(n+1)^s.

theorem LeanPolyLog.Dilog.summable_pow_div_pow {𝕜 : Type u_1} [RCLike 𝕜] {s : ℕ} (hs : 2 ≤ s) {z : 𝕜} (hz : ‖z‖ ≤ 1) : Summable fun (n : ℕ) => z ^ (n + 1) / (↑n + 1) ^ s

For s ≥ 2 the polylog series converges (absolutely) on the closed unit disk.

theorem LeanPolyLog.Dilog.continuousOn_tsum_pow_div_pow {𝕜 : Type u_1} [RCLike 𝕜] {s : ℕ} (hs : 2 ≤ s) : ContinuousOn (fun (z : 𝕜) => ∑' (n : ℕ), z ^ (n + 1) / (↑n + 1) ^ s) (Metric.closedBall 0 1)

For s ≥ 2 the polylog series is continuous on the closed unit disk (Weierstrass M-test).

theorem LeanPolyLog.Dilog.hasDerivAt_tsum_pow_div_pow {𝕜 : Type u_1} [RCLike 𝕜] (s : ℕ) {z : 𝕜} (hz : ‖z‖ < 1) : HasDerivAt (fun (w : 𝕜) => ∑' (n : ℕ), w ^ (n + 1) / (↑n + 1) ^ (s + 1)) (∑' (n : ℕ), z ^ n / (↑n + 1) ^ s) z

Termwise differentiation of the polylog series on the open unit disk: d/dz ∑ z^(n+1)/(n+1)^(s+1) = ∑ z^n/(n+1)^s.

theorem LeanPolyLog.Dilog.tsum_pow_div_pow_eq_div {𝕜 : Type u_1} [RCLike 𝕜] (s : ℕ) {z : 𝕜} (hz : z ≠ 0) : ∑' (n : ℕ), z ^ n / (↑n + 1) ^ s = (∑' (n : ℕ), z ^ (n + 1) / (↑n + 1) ^ s) / z

Away from 0, ∑ z^n/(n+1)^s = (∑ z^(n+1)/(n+1)^s) / z.

theorem LeanPolyLog.Dilog.tsum_pow_div_pow_sq {𝕜 : Type u_1} [RCLike 𝕜] {s : ℕ} (hs : 2 ≤ s) {z : 𝕜} (hz : ‖z‖ ≤ 1) : ∑' (n : ℕ), (z ^ 2) ^ (n + 1) / (↑n + 1) ^ s = 2 ^ (s - 1) * (∑' (n : ℕ), z ^ (n + 1) / (↑n + 1) ^ s + ∑' (n : ℕ), (-z) ^ (n + 1) / (↑n + 1) ^ s)

The duplication formula for the polylog series: ∑ (z²)^(n+1)/(n+1)^s = 2^(s-1) (∑ z^(n+1)/(n+1)^s + ∑ (-z)^(n+1)/(n+1)^s). Only even powers survive in the sum on the right.

Constancy from a vanishing derivative

theorem LeanPolyLog.Dilog.eq_of_hasDerivAt_eq_zero {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hc : ContinuousOn f (Set.Icc a b)) (hd : ∀ x ∈ Set.Ioo a b, HasDerivAt f 0 x) : f a = f b

A real function that is continuous on [a, b] and has derivative 0 on (a, b) takes the same value at a and b.

The real polylogarithm Lir

@[simp]

theorem LeanPolyLog.Dilog.Lir_zero (s : ℕ) : Lir s 0 = 0

Li_s(0) = 0.

theorem LeanPolyLog.Dilog.hasSum_Lir {s : ℕ} (hs : 2 ≤ s) {x : ℝ} (hx : |x| ≤ 1) : HasSum (fun (n : ℕ) => x ^ (n + 1) / (↑n + 1) ^ s) (Lir s x)

For s ≥ 2 the series of Li_s(x) converges for |x| ≤ 1.

theorem LeanPolyLog.Dilog.continuousOn_Lir {s : ℕ} (hs : 2 ≤ s) : ContinuousOn (Lir s) (Set.Icc (-1) 1)

For s ≥ 2, Li_s is continuous on [-1, 1].

theorem LeanPolyLog.Dilog.Lir_one {x : ℝ} (hx : |x| < 1) : Lir 1 x = -Real.log (1 - x)

Li_1(x) = -log(1 - x) for |x| < 1.

theorem LeanPolyLog.Dilog.Lir_two_one : Lir 2 1 = Real.pi ^ 2 / 6

Li_2(1) = ζ(2) = π²/6.

theorem LeanPolyLog.Dilog.hasDerivAt_Lir_succ (s : ℕ) {x : ℝ} (hx : |x| < 1) (hx0 : x ≠ 0) : HasDerivAt (Lir (s + 1)) (Lir s x / x) x

d/dx Li_(s+1)(x) = Li_s(x)/x for 0 < |x| < 1.

theorem LeanPolyLog.Dilog.hasDerivAt_Lir_two {x : ℝ} (hx : |x| < 1) (hx0 : x ≠ 0) : HasDerivAt (Lir 2) (-Real.log (1 - x) / x) x

d/dx Li_2(x) = -log(1 - x)/x for 0 < |x| < 1.

theorem LeanPolyLog.Dilog.Lir_sq {s : ℕ} (hs : 2 ≤ s) {x : ℝ} (hx : |x| ≤ 1) : Lir s (x ^ 2) = 2 ^ (s - 1) * (Lir s x + Lir s (-x))

The duplication formula Li_s(x²) = 2^(s-1) (Li_s(x) + Li_s(-x)) for |x| ≤ 1, s ≥ 2.

theorem LeanPolyLog.Dilog.Lir_two_sq {x : ℝ} (hx : |x| ≤ 1) : Lir 2 (x ^ 2) = 2 * (Lir 2 x + Lir 2 (-x))

The duplication formula Li_2(x²) = 2 (Li_2(x) + Li_2(-x)) for |x| ≤ 1.

theorem LeanPolyLog.Dilog.Lir_two_neg_one : Lir 2 (-1) = -(Real.pi ^ 2 / 12)

Li_2(-1) = -η(2) = -π²/12, from the duplication formula at x = 1.

Euler's reflection formula

theorem LeanPolyLog.Dilog.continuousAt_log_mul_log_one_sub_zero : ContinuousAt (fun (t : ℝ) => Real.log t * Real.log (1 - t)) 0

log t · log(1 - t) is continuous at 0 (Lean's log 0 = 0): near 0 it is bounded by 2 |t log t|, since |log(1 - t)| ≤ |t|/(1 - |t|).

theorem LeanPolyLog.Dilog.continuous_log_mul_log_one_sub : Continuous fun (t : ℝ) => Real.log t * Real.log (1 - t)

t ↦ log t · log(1 - t) is continuous on ℝ (with Lean's log 0 = 0).

theorem LeanPolyLog.Dilog.Lir_two_add_Lir_two_one_sub {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : Lir 2 x + Lir 2 (1 - x) = Real.pi ^ 2 / 6 - Real.log x * Real.log (1 - x)

Euler's reflection formula: Li_2(x) + Li_2(1 - x) = π²/6 - log x · log(1 - x) for 0 < x < 1.

theorem LeanPolyLog.Dilog.Lir_two_one_half : Lir 2 (1 / 2) = Real.pi ^ 2 / 12 - Real.log 2 ^ 2 / 2

Li_2(1/2) = π²/12 - log²2/2, from the reflection formula at x = 1/2.

Landen's identity

theorem LeanPolyLog.Dilog.Lir_two_neg_add_Lir_two_div {y : ℝ} (hy0 : 0 ≤ y) (hy1 : y ≤ 1) : Lir 2 (-y) + Lir 2 (y / (1 + y)) = -(Real.log (1 + y) ^ 2 / 2)

Landen's identity on [0, 1]: Li_2(-y) + Li_2(y/(1+y)) = -½ log²(1+y).