Abel's five-term relation

For x, y ∈ (0, 1) the Rogers dilogarithm satisfies

L(x) + L(y) = L(xy) + L(x(1 - y)/(1 - xy)) + L(y(1 - x)/(1 - xy)).

For fixed y the difference of the two sides has vanishing derivative in x on (0, 1), so it is constant, and its limit at x → 0⁺ is 0.

Main results

• Dilog.hasDerivAt_rogersL: L′(x) = -½ (log(1 - x)/x + log x/(1 - x)) on (0, 1).
• Dilog.tendsto_rogersL_nhdsGT_zero, Dilog.continuousAt_rogersL.
• Dilog.rogersL_fiveterm: the five-term relation.

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.

theorem Dilog.hasDerivAt_rogersL {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : HasDerivAt rogersL (-(Real.log (1 - x) / x + Real.log x / (1 - x)) / 2) x

The derivative of the Rogers L-function on (0,1): L'(x) = −(log(1−x)/x + log x/(1−x))/2.

theorem Dilog.fiveterm_hasDerivAt_zero {x y : ℝ} (hx : x ∈ Set.Ioo 0 1) (hy : y ∈ Set.Ioo 0 1) : HasDerivAt (fun (t : ℝ) => rogersL t - rogersL (t * y) - rogersL (t * (1 - y) / (1 - t * y)) - rogersL (y * (1 - t) / (1 - t * y))) 0 x

The five-term difference, as a function of x with y fixed, has zero derivative on (0,1): the log-terms of L' cancel after rewriting every argument's logarithm in the basis {log x, log y, log(1−x), log(1−y), log(1−xy)}.

theorem Dilog.tendsto_rogersL_nhdsGT_zero : Filter.Tendsto rogersL (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

L(t) → 0 as t → 0⁺: the Li₂ part is continuous, and log t · log(1−t) → 0 is squeezed by 2·(−t log t) → 0 (using −log(1−t) ≤ 2t on (0,½]).

theorem Dilog.continuousAt_rogersL {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : ContinuousAt rogersL x

The Rogers L-function is continuous at every interior point of (0,1).

theorem Dilog.rogersL_fiveterm {x y : ℝ} (hx : x ∈ Set.Ioo 0 1) (hy : y ∈ Set.Ioo 0 1) : rogersL x + rogersL y = rogersL (x * y) + rogersL (x * (1 - y) / (1 - x * y)) + rogersL (y * (1 - x) / (1 - x * y))

Abel's five-term relation in Rogers L form: for x, y ∈ (0,1), L(x) + L(y) = L(xy) + L(x(1−y)/(1−xy)) + L(y(1−x)/(1−xy)). The main theorem of weight-2 dilogarithm theory.