The real dilogarithm

The dilogarithm Li₂ x = ∑_{n ≥ 1} xⁿ / n² on [-1, 1], its derivative -log(1 - x) / x, and the classical functional equations obtained by differentiating and evaluating at an endpoint. Mathlib has no polylogarithm.

Main definitions

• Dilog.Li₂: the real dilogarithm, as a power series.
• Dilog.rogersL: the Rogers dilogarithm L(x) = Li₂ x + ½ log x · log(1 - x).

Main results

• Dilog.Li₂_one: Li₂ 1 = π² / 6; Dilog.Li₂_neg_one: Li₂ (-1) = -π² / 12.
• Dilog.hasDerivAt_Li₂: Li₂′ x = -log(1 - x) / x for 0 < |x| < 1.
• Dilog.continuousOn_Li₂: continuity on [-1, 1].
• Dilog.Li₂_add_Li₂_one_sub: Euler's reflection Li₂ x + Li₂ (1 - x) = π²/6 - log x · log (1 - x).
• Dilog.Li₂_one_half: Li₂ (1/2) = π²/12 - (log 2)²/2.
• Dilog.Li₂_landen: Landen's identity Li₂ x + Li₂ (x / (x - 1)) = -(log (1 - x))² / 2.
• Dilog.Li₂_sq: the duplication formula Li₂ (x²) = 2 (Li₂ x + Li₂ (-x)).
• Dilog.Li₂_inv_goldenRatio_sq, Dilog.Li₂_inv_goldenRatio, Dilog.Li₂_neg_inv_goldenRatio: the values at φ⁻², φ⁻¹ and -φ⁻¹; Dilog.rogersL_inv_goldenRatio_sq: L(φ⁻²) = π²/15.
• Dilog.leeYang_effective_central_charge: L(φ⁻²) / L(1) = 2/5.

References

• L. Lewin, Polylogarithms and Associated Functions, North-Holland, 1981.
• D. Zagier, The dilogarithm function, in Frontiers in Number Theory, Physics, and Geometry II, Springer, 2007, 3–65.

noncomputable def Dilog.Li₂ (z : ℝ) : ℝ

The real dilogarithm Li₂ z = ∑_{n ≥ 1} zⁿ / n² = ∑_{n ≥ 0} z^{n+1} / (n+1)².

Equations

• Dilog.Li₂ z = ∑' (n : ℕ), z ^ (n + 1) / (↑n + 1) ^ 2

theorem Dilog.summable_one_div_add_one_sq : Summable fun (n : ℕ) => 1 / (↑n + 1) ^ 2

The dominating series ∑ 1/(n+1)² converges (shift of the p = 2 series).

theorem Dilog.summable_Li₂ {z : ℝ} (hz : |z| ≤ 1) : Summable fun (n : ℕ) => z ^ (n + 1) / (↑n + 1) ^ 2

The defining series of Li₂ is summable on the closed unit interval |z| ≤ 1 (majorised termwise by the convergent ∑ 1/(n+1)²).

@[simp]

theorem Dilog.Li₂_zero : Li₂ 0 = 0

theorem Dilog.Li₂_one : Li₂ 1 = Real.pi ^ 2 / 6

Li₂ 1 = π² / 6 — the Basel problem. Reindex ∑_{n≥0} 1/(n+1)² to hasSum_zeta_two (∑_{n : ℕ} 1/n² = π²/6, whose n = 0 term is 0).

theorem Dilog.hasDerivAt_Li₂ {x : ℝ} (habs : |x| < 1) (hx0 : x ≠ 0) : HasDerivAt Li₂ (-Real.log (1 - x) / x) x

Termwise differentiation of the dilogarithm series gives, on (-1,1) \ {0}, Li₂'(x) = -log(1 - x)/x (note ∑_{n≥1} xⁿ⁻¹ = 1/(1-x) and ∑ xⁿ/n = -log(1-x)). At x = 0 the derivative is 1, but the quotient form requires x ≠ 0.

theorem Dilog.continuousOn_Li₂ : ContinuousOn Li₂ (Set.Icc (-1) 1)

Li₂ is continuous on [-1, 1] (Weierstrass M-test: the series is dominated by ∑ 1/(n+1)² uniformly on the closed interval).

theorem Dilog.Li₂_add_Li₂_one_sub {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : Li₂ x + Li₂ (1 - x) = Real.pi ^ 2 / 6 - Real.log x * Real.log (1 - x)

Euler's reflection identity for the dilogarithm on (0,1): Li₂ x + Li₂ (1 - x) = π²/6 - log x · log (1 - x).

Proof: let F y := Li₂ y + Li₂ (1 - y) + log y · log (1 - y). Using hasDerivAt_Li₂ (and (Li₂ (1-·))' = log y/(1-y) by the chain rule), F' = 0 on (0,1), so F is constant there (constant_of_has_deriv_right_zero on subintervals). Its limit as y → 0⁺ is Li₂ 0 + Li₂ 1 + 0 = π²/6 by continuity of Li₂ on [-1,1] and log y · log(1-y) = (log(1-y)/y)·(y·log y) → (-1)·0 = 0.

theorem Dilog.Li₂_one_half : Li₂ (1 / 2) = Real.pi ^ 2 / 12 - Real.log 2 ^ 2 / 2

Euler's special value Li₂(1/2) = π²/12 - log²2/2 — the reflection identity at its fixed point x = 1/2.

theorem Dilog.Li₂_landen {x : ℝ} (hx : x ∈ Set.Ioo 0 (1 / 2)) : Li₂ x + Li₂ (x / (x - 1)) = -Real.log (1 - x) ^ 2 / 2

Landen's identity for the dilogarithm on (0, 1/2): Li₂ x + Li₂ (x/(x-1)) = -log²(1-x) / 2.

For x ∈ (0, 1/2) the second argument x/(x-1) ∈ (-1, 0) stays inside the disc of convergence of the defining power series; past x = 1/2 the identity requires analytic continuation, which the series definition does not provide.

Proof: same scheme as the reflection identity — the combination G y := Li₂ y + Li₂ (y/(y-1)) + log²(1-y)/2 has zero derivative on (0, 1/2) and tends to 0 as y → 0⁺.

theorem Dilog.Li₂_sq {x : ℝ} (hx : |x| ≤ 1) : Li₂ (x ^ 2) = 2 * (Li₂ x + Li₂ (-x))

Duplication (squaring) formula Li₂(x²) = 2(Li₂ x + Li₂(−x)) for |x| ≤ 1 — pure series rearrangement: odd powers cancel, even powers double. No calculus needed.

Golden-ratio evaluations

The classical special values Li₂(1/φ²) = π²/15 − log²φ, Li₂(1/φ) = π²/10 − log²φ and Li₂(−1/φ) = log²φ/2 − π²/15 (attributed to Landen; Lewin §1.4). The key golden facts are 1/φ + 1/φ² = 1 (so 1/φ² and 1/φ are a reflection pair) and (1/φ²)/((1/φ²)−1) = −1/φ (so Landen's identity maps 1/φ² to −1/φ); together with the duplication formula at 1/φ this gives a linear system — no five-term relation is needed.

theorem Dilog.Li₂_neg_one : Li₂ (-1) = -Real.pi ^ 2 / 12

Li₂(−1) = −π²/12 = −η(2): the duplication formula at x = 1.

theorem Dilog.Li₂_inv_goldenRatio_sq : Li₂ (Real.goldenRatio⁻¹ ^ 2) = Real.pi ^ 2 / 15 - Real.log Real.goldenRatio ^ 2

Li₂(1/φ²) = π²/15 − log²φ (classical; Landen, cf. Lewin §1.4).

theorem Dilog.Li₂_inv_goldenRatio : Li₂ Real.goldenRatio⁻¹ = Real.pi ^ 2 / 10 - Real.log Real.goldenRatio ^ 2

Li₂(1/φ) = π²/10 − log²φ (classical; Landen, cf. Lewin §1.4).

theorem Dilog.Li₂_neg_inv_goldenRatio : Li₂ (-Real.goldenRatio⁻¹) = Real.log Real.goldenRatio ^ 2 / 2 - Real.pi ^ 2 / 15

Li₂(−1/φ) = log²φ/2 − π²/15 (classical; Lewin §1.4).

noncomputable def Dilog.rogersL (x : ℝ) : ℝ

The Rogers dilogarithm L(x) = Li₂(x) + ½·log x · log(1−x) (the natural normalisation for 0 < x < 1; the log-product term removes the log² defects, so the golden-ratio values become pure rational multiples of π²).

Equations

• Dilog.rogersL x = Dilog.Li₂ x + Real.log x * Real.log (1 - x) / 2

theorem Dilog.rogersL_inv_goldenRatio_sq : rogersL (Real.goldenRatio⁻¹ ^ 2) = Real.pi ^ 2 / 15

L(1/φ²) = π²/15 — in physics terms: the effective central charge of the Lee-Yang thermodynamic-Bethe-ansatz system is c_eff = L(1/φ²)/L(1) = (π²/15)/(π²/6) = 2/5, the simplest TBA dilogarithm identity.

theorem Dilog.rogersL_inv_goldenRatio : rogersL Real.goldenRatio⁻¹ = Real.pi ^ 2 / 10

L(1/φ) = π²/10 (Landen).

theorem Dilog.rogersL_gold_sum : rogersL Real.goldenRatio⁻¹ + rogersL (Real.goldenRatio⁻¹ ^ 2) = Real.pi ^ 2 / 6

Rogers' two-term golden identity L(1/φ) + L(1/φ²) = L(1) = π²/6 — the weight-2 "sum rule" behind the golden-ratio ladder (Rogers 1907).

theorem Dilog.rogersL_one : rogersL 1 = Real.pi ^ 2 / 6

L(1) = Li₂(1) = π²/6: the log-product term vanishes at x = 1.

theorem Dilog.leeYang_effective_central_charge : rogersL (Real.goldenRatio⁻¹ ^ 2) / rogersL 1 = 2 / 5

The Lee–Yang effective central charge c_eff = L(1/φ²)/L(1) = 2/5, the simplest thermodynamic-Bethe-ansatz dilogarithm identity.