Dilogarithm identities

TheoremEntry 24 of Chapter 9 of Ramanujan's notebooks#✓fully proved

Let \(x, y \in [0, 1]\) and \(\theta, \varphi \in (-\pi, \pi]\) satisfy \(x e^{i\theta} + y e^{i\varphi} = 1\). Write \(\ell(t) = \log t\) for \(0 < t \le 1\) and \(\ell(0) = 0\). Then the four series \(\sum_{k \ge 1} \frac{x^k \cos k\theta}{k^2}\), \(\sum_{k \ge 1} \frac{y^k \cos k\varphi}{k^2}\), \(\sum_{k \ge 1} \frac{x^k \sin k\theta}{k^2}\) and \(\sum_{k \ge 1} \frac{y^k \sin k\varphi}{k^2}\) converge absolutely, and

\[ \sum_{k \ge 1} \frac{x^k \cos k\theta}{k^2} + \sum_{k \ge 1} \frac{y^k \cos k\varphi}{k^2} = \frac{\pi^2}{6} - \ell(x) \ell(y) + \theta \varphi, \]

\[ \sum_{k \ge 1} \frac{x^k \sin k\theta}{k^2} + \sum_{k \ge 1} \frac{y^k \sin k\varphi}{k^2} = -\varphi \, \ell(x) - \theta \, \ell(y). \]

MathlibExt.Analysis.Ramanujan.Part1Ch9.Entry24Dougall.ramanujan_part1_ch9_entry24_dougall · 17 lines

theorem ramanujan_part1_ch9_entry24_dougall (x y theta phi : ℝ)
    (hx : 0 ≤ x ∧ x ≤ 1) (hy : 0 ≤ y ∧ y ≤ 1)
    (htheta : -Real.pi < theta ∧ theta ≤ Real.pi)
    (hphi : -Real.pi < phi ∧ phi ≤ Real.pi)
    (hxy : (x : ℂ) * Complex.exp (Complex.I * theta) +
      (y : ℂ) * Complex.exp (Complex.I * phi) = 1) :
    Summable (chapter9DilogCosTerm x theta) ∧
      Summable (chapter9DilogCosTerm y phi) ∧
      Summable (chapter9DilogSinTerm x theta) ∧
      Summable (chapter9DilogSinTerm y phi) ∧
      (∑' j : ℕ, chapter9DilogCosTerm x theta j) +
          ∑' j : ℕ, chapter9DilogCosTerm y phi j =
        Real.pi ^ 2 / 6 - chapter9BoundaryLog x * chapter9BoundaryLog y +
          theta * phi ∧
      (∑' j : ℕ, chapter9DilogSinTerm x theta j) +
          ∑' j : ℕ, chapter9DilogSinTerm y phi j =
        -phi * chapter9BoundaryLog x - theta * chapter9BoundaryLog y

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 9.

TheoremEntry 25 of Chapter 9 of Ramanujan's notebooks#✓fully proved

Let \(x, y \in [0, 1]\) and let \(\theta\) and \(\varphi\) be real numbers with \(x e^{i\theta} + y e^{i\varphi} = xy \, e^{i(\theta + \varphi)}\). Then \(1 - x \cos\theta \ne 0\) and \(1 - y \cos\varphi \ne 0\). Put \(A_x = 1 - 2x \cos\theta + x^2\), \(A_y = 1 - 2y \cos\varphi + y^2\), \(u_x = \arctan \frac{x \sin\theta}{1 - x \cos\theta}\) and \(u_y = \arctan \frac{y \sin\varphi}{1 - y \cos\varphi}\). Then \(A_x > 0\), \(A_y > 0\), the four series \(\sum_{k \ge 1} \frac{x^k \cos k\theta}{k^2}\), \(\sum_{k \ge 1} \frac{y^k \cos k\varphi}{k^2}\), \(\sum_{k \ge 1} \frac{x^k \sin k\theta}{k^2}\) and \(\sum_{k \ge 1} \frac{y^k \sin k\varphi}{k^2}\) converge absolutely, and

\[ \sum_{k \ge 1} \frac{x^k \cos k\theta}{k^2} + \sum_{k \ge 1} \frac{y^k \cos k\varphi}{k^2} = \frac{\log A_x \log A_y}{8} - \frac{u_x u_y}{2}, \]

\[ \sum_{k \ge 1} \frac{x^k \sin k\theta}{k^2} + \sum_{k \ge 1} \frac{y^k \sin k\varphi}{k^2} = -\frac{u_y \log A_x}{4} - \frac{u_x \log A_y}{4}. \]

MathlibExt.Analysis.Ramanujan.Part1Ch9.Entry25Dixon.ramanujan_part1_ch9_entry25_dixon · 22 lines

theorem ramanujan_part1_ch9_entry25_dixon (x y theta phi : ℝ)
    (hx : 0 ≤ x ∧ x ≤ 1) (hy : 0 ≤ y ∧ y ≤ 1)
    (hxy : (x : ℂ) * Complex.exp (Complex.I * theta) +
      (y : ℂ) * Complex.exp (Complex.I * phi) =
        (x * y : ℝ) * Complex.exp (Complex.I * (theta + phi))) :
    let Ax := 1 - 2 * x * Real.cos theta + x ^ 2
    let Ay := 1 - 2 * y * Real.cos phi + y ^ 2
    let ux := Real.arctan (x * Real.sin theta / (1 - x * Real.cos theta))
    let uy := Real.arctan (y * Real.sin phi / (1 - y * Real.cos phi))
    1 - x * Real.cos theta ≠ 0 ∧
      1 - y * Real.cos phi ≠ 0 ∧
      0 < Ax ∧ 0 < Ay ∧
      Summable (chapter9DilogCosTerm x theta) ∧
      Summable (chapter9DilogCosTerm y phi) ∧
      Summable (chapter9DilogSinTerm x theta) ∧
      Summable (chapter9DilogSinTerm y phi) ∧
      (∑' j : ℕ, chapter9DilogCosTerm x theta j) +
          ∑' j : ℕ, chapter9DilogCosTerm y phi j =
        Real.log Ax * Real.log Ay / 8 - ux * uy / 2 ∧
      (∑' j : ℕ, chapter9DilogSinTerm x theta j) +
          ∑' j : ℕ, chapter9DilogSinTerm y phi j =
        -Real.log Ax * uy / 4 - Real.log Ay * ux / 4

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 9.

TheoremThe Entry 26 boundary logarithm is the real logarithm#✓fully proved

Let \(\log\) be the real logarithm, extended to all of \(\mathbb{R}\) by \(\log 0 = 0\) and \(\log x = \log|x|\) for \(x < 0\). For every real \(x\), the boundary logarithm of \(x\), defined as \(0\) if \(x = 0\) and as \(\log x\) otherwise, equals \(\log x\).

theorem chapter9BoundaryLog_eq_log (x : ℝ) : chapter9BoundaryLog x = Real.log x

Used by 2

Used byRamanujan's Landen-type identity in terms of the Entry 24 series · Ramanujan's Landen-type dilogarithm identity (Entry 26)

TheoremThe Entry 26 and Entry 24 dilogarithm cosine terms agree#✓fully proved

For all real \(\rho\) and \(\alpha\) and every natural number \(j\), the \(j\)-th term \(\rho^{j+1} \cos((j+1)\alpha) / (j+1)^2\) of the dilogarithm cosine series defined for Entry 26 equals the \(j\)-th term of the cosine series defined for Entry 24, which is given by the same formula.

theorem chapter9DilogCosTerm_eq_entry24 (rho angle : ℝ) (j : ℕ) :
    chapter9DilogCosTerm rho angle j =
      Entry24Dougall.chapter9DilogCosTerm rho angle j

TheoremThe Entry 26 and Entry 24 dilogarithm sine terms agree#✓fully proved

For all real \(\rho\) and \(\alpha\) and every natural number \(j\), the \(j\)-th term \(\rho^{j+1} \sin((j+1)\alpha) / (j+1)^2\) of the dilogarithm sine series defined for Entry 26 equals the \(j\)-th term of the sine series defined for Entry 24, which is given by the same formula.

theorem chapter9DilogSinTerm_eq_entry24 (rho angle : ℝ) (j : ℕ) :
    chapter9DilogSinTerm rho angle j =
      Entry24Dougall.chapter9DilogSinTerm rho angle j

TheoremRamanujan's Landen-type identity in terms of the Entry 24 series#✓fully proved

For real \(\rho\) and \(\alpha\) and \(k \ge 1\) let \(c_k(\rho, \alpha) = \rho^k \cos(k\alpha) / k^2\) and \(s_k(\rho, \alpha) = \rho^k \sin(k\alpha) / k^2\) be the terms of the dilogarithm series of Entry 24, and write \(C(\rho, \alpha) = \sum_{j \ge 0} c_{2j+1}(\rho, \alpha)\) and \(S(\rho, \alpha) = \sum_{j \ge 0} s_{2j+1}(\rho, \alpha)\). Let \(x, y \in [0, 1]\) and \(\theta, \varphi \in (-\pi, \pi]\) satisfy \(x e^{i\theta} + y e^{i\varphi} + xy\, e^{i(\theta + \varphi)} = 1\). Then the four series defining \(C(x, \theta)\), \(C(y, \varphi)\), \(S(x, \theta)\) and \(S(y, \varphi)\) converge absolutely, and, where \(\log\) is the real logarithm with \(\log 0 = 0\), \(C(x, \theta) + C(y, \varphi) = \pi^2/8 - \tfrac12 \log x \log y + \tfrac12 \theta\varphi\) and \(S(x, \theta) + S(y, \varphi) = -\tfrac12 \varphi \log x - \tfrac12 \theta \log y\).

MathlibExt.Analysis.Ramanujan.Part1Ch9.Entry26Ramanujanpi.ramanujan_part1_ch9_entry26_ramanujanpi_entry24_terms · 21 lines

theorem ramanujan_part1_ch9_entry26_ramanujanpi_entry24_terms
    (x y theta phi : ℝ)
    (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hy0 : 0 ≤ y) (hy1 : y ≤ 1)
    (htheta0 : -Real.pi < theta) (htheta1 : theta ≤ Real.pi)
    (hphi0 : -Real.pi < phi) (hphi1 : phi ≤ Real.pi)
    (hrelation :
      (x : ℂ) * Complex.exp (Complex.I * (theta : ℂ)) +
          (y : ℂ) * Complex.exp (Complex.I * (phi : ℂ)) +
          ((x * y : ℝ) : ℂ) *
            Complex.exp (Complex.I * ((theta + phi : ℝ) : ℂ)) = 1) :
    Summable (fun j : ℕ => Entry24Dougall.chapter9DilogCosTerm x theta (2 * j)) ∧
      Summable (fun j : ℕ => Entry24Dougall.chapter9DilogCosTerm y phi (2 * j)) ∧
      Summable (fun j : ℕ => Entry24Dougall.chapter9DilogSinTerm x theta (2 * j)) ∧
      Summable (fun j : ℕ => Entry24Dougall.chapter9DilogSinTerm y phi (2 * j)) ∧
      (∑' j : ℕ, Entry24Dougall.chapter9DilogCosTerm x theta (2 * j)) +
          (∑' j : ℕ, Entry24Dougall.chapter9DilogCosTerm y phi (2 * j)) =
        Real.pi ^ 2 / 8 - (1 / 2 : ℝ) * Real.log x * Real.log y +
          (1 / 2 : ℝ) * theta * phi ∧
      (∑' j : ℕ, Entry24Dougall.chapter9DilogSinTerm x theta (2 * j)) +
          (∑' j : ℕ, Entry24Dougall.chapter9DilogSinTerm y phi (2 * j)) =
        -(1 / 2 : ℝ) * phi * Real.log x - (1 / 2 : ℝ) * theta * Real.log y

Uses 1 · Used by 1

Proof usesThe Entry 26 boundary logarithm is the real logarithm

Used byRamanujan's Landen-type dilogarithm identity (Entry 26)

TheoremRamanujan's Landen-type dilogarithm identity (Entry 26)#✓fully proved

For real \(\rho\) and \(\alpha\) write \(C(\rho, \alpha) = \sum_{j \ge 0} \rho^{2j+1} \cos((2j+1)\alpha) / (2j+1)^2\) and \(S(\rho, \alpha) = \sum_{j \ge 0} \rho^{2j+1} \sin((2j+1)\alpha) / (2j+1)^2\). Let \(x, y \in [0, 1]\) and \(\theta, \varphi \in (-\pi, \pi]\) satisfy \(x e^{i\theta} + y e^{i\varphi} + xy\, e^{i(\theta + \varphi)} = 1\). Then the four series defining \(C(x, \theta)\), \(C(y, \varphi)\), \(S(x, \theta)\) and \(S(y, \varphi)\) converge absolutely, and, with the convention \(\log 0 = 0\), \(C(x, \theta) + C(y, \varphi) = \pi^2/8 - \tfrac12 \log x \log y + \tfrac12 \theta\varphi\) and \(S(x, \theta) + S(y, \varphi) = -\tfrac12 \varphi \log x - \tfrac12 \theta \log y\).

Proof: Identify the odd series with Legendre's chi function, prove Landen's identity by differentiation, and extend it to the closed right half-disk by continuity. This follows the route in Berndt, Part I, Chapter 9, Entry 26, and Lewin, Polylogarithms and Associated Functions, Chapter 1.

MathlibExt.Analysis.Ramanujan.Part1Ch9.Entry26Ramanujanpi.ramanujan_part1_ch9_entry26_ramanujanpi · 23 lines

theorem ramanujan_part1_ch9_entry26_ramanujanpi
    (x y theta phi : ℝ)
    (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hy0 : 0 ≤ y) (hy1 : y ≤ 1)
    (htheta0 : -Real.pi < theta) (htheta1 : theta ≤ Real.pi)
    (hphi0 : -Real.pi < phi) (hphi1 : phi ≤ Real.pi)
    (hrelation :
      (x : ℂ) * Complex.exp (Complex.I * (theta : ℂ)) +
          (y : ℂ) * Complex.exp (Complex.I * (phi : ℂ)) +
          ((x * y : ℝ) : ℂ) *
            Complex.exp (Complex.I * ((theta + phi : ℝ) : ℂ)) = 1) :
    Summable (fun j : ℕ => chapter9DilogCosTerm x theta (2 * j)) ∧
      Summable (fun j : ℕ => chapter9DilogCosTerm y phi (2 * j)) ∧
      Summable (fun j : ℕ => chapter9DilogSinTerm x theta (2 * j)) ∧
      Summable (fun j : ℕ => chapter9DilogSinTerm y phi (2 * j)) ∧
      (∑' j : ℕ, chapter9DilogCosTerm x theta (2 * j)) +
          (∑' j : ℕ, chapter9DilogCosTerm y phi (2 * j)) =
        Real.pi ^ 2 / 8 -
          (1 / 2 : ℝ) * chapter9BoundaryLog x * chapter9BoundaryLog y +
          (1 / 2 : ℝ) * theta * phi ∧
      (∑' j : ℕ, chapter9DilogSinTerm x theta (2 * j)) +
          (∑' j : ℕ, chapter9DilogSinTerm y phi (2 * j)) =
        -(1 / 2 : ℝ) * phi * chapter9BoundaryLog x -
          (1 / 2 : ℝ) * theta * chapter9BoundaryLog y

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 9, Entry 26, p. 273.

Uses 2

Proof usesThe Entry 26 boundary logarithm is the real logarithm · Ramanujan's Landen-type identity in terms of the Entry 24 series

TheoremHoorfar–Qi dilogarithm series#●ready to prove

Write \(L(x) = \sum_{m \ge 1} x^m/m^2 + \frac{1}{2} \log x \log(1 - x)\) for the Rogers dilogarithm on \([0, 1]\) (with \(\log 0 = 0\)). For positive integers \(p, q\) and real numbers \(\theta, \beta\) with \(0 < \theta < 1\) and \(0 < \beta < 1\),

\[ \sum_{n \ge 0} L\left(\frac{\beta(1 - \theta^p)(1 - \theta^q)\theta^n} {(1 - \beta\theta^{n+p})(1 - \beta\theta^{n+q})}\right) = \sum_{n=0}^{q-1} L\left(\frac{\beta(1 - \theta^p)\theta^n}{1 - \beta\theta^{n+p}}\right) + \sum_{n=0}^{p-1} L\left(\frac{1 - \theta^q}{1 - \beta\theta^{n+q}}\right) - p\,L(1 - \theta^q). \]

public theorem_wanted rogersDilog_hoorfarQi_series {p q : ℕ} (hp : 0 < p) (hq : 0 < q)
    {θ β : ℝ} (hθ₀ : 0 < θ) (hθ₁ : θ < 1) (hβ₀ : 0 < β) (hβ₁ : β < 1) :
    let L : ℝ → ℝ := fun x => (∑' n : ℕ, x ^ (n + 1) / ((n : ℝ) + 1) ^ 2) + log x * log (1 - x) / 2
    ∑' n : ℕ, L (β * (1 - θ ^ p) * (1 - θ ^ q) * θ ^ n /
        ((1 - β * θ ^ (n + p)) * (1 - β * θ ^ (n + q)))) =
      ∑ n ∈ Finset.range q, L (β * (1 - θ ^ p) * θ ^ n / (1 - β * θ ^ (n + p))) +
        ∑ n ∈ Finset.range p, L ((1 - θ ^ q) / (1 - β * θ ^ (n + q))) - p * L (1 - θ ^ q)

Sources

• Chance Sanford, A Dilogarithm Series and a Generalization of a Theorem of Bridgeman, INTEGERS 25 (2025), Article A52, Theorem 1, quoting Hoorfar and Qi.

TheoremBridgeman's dilogarithm series for a positive Pell solution#●ready to prove

Write \(L(x) = \sum_{m \ge 1} x^m/m^2 + \frac{1}{2} \log x \log(1 - x)\) for the Rogers dilogarithm on \([0, 1]\) (with \(\log 0 = 0\)). Let \(n\) be a natural number that is not a perfect square, let \(a, b\) be positive rationals with \(a^2 - n b^2 = 1\), and put \(u = a + b\sqrt{n}\). Define rationals \(a_k, b_k\) by \(a_0 = 1\), \(b_0 = 0\), \(a_{k+1} = a a_k + n b b_k\) and \(b_{k+1} = b a_k + a b_k\), so that \(u^k = a_k + b_k\sqrt{n}\). Then

\[ L(1/u^2) = \sum_{k \ge 2} L(b^2/b_k^2), \]

and if \(a\) and \(b\) are integers, then for every \(k \ge 0\) there is an integer \(m\) with \(b_k = bm\).

public theorem_wanted rogersDilog_pell_positive_series {n : ℕ} (hn : ¬ IsSquare n) {a b : ℚ}
    (ha : 0 < a) (hb : 0 < b) (hpell : a ^ 2 - n * b ^ 2 = 1) {A B : ℕ → ℚ}
    (hA₀ : A 0 = 1) (hB₀ : B 0 = 0) (hA : ∀ k, A (k + 1) = a * A k + n * b * B k)
    (hB : ∀ k, B (k + 1) = b * A k + a * B k) :
    let L : ℝ → ℝ := fun x => (∑' n : ℕ, x ^ (n + 1) / ((n : ℝ) + 1) ^ 2) + log x * log (1 - x) / 2
    L (1 / ((a : ℝ) + b * √n) ^ 2) = ∑' k : ℕ, L ((b : ℝ) ^ 2 / (B (k + 2) : ℝ) ^ 2) ∧
      ((∃ a' b' : ℤ, a = a' ∧ b = b') → ∀ k, ∃ m : ℤ, B k = b * m)

Sources

• Chance Sanford, A Dilogarithm Series and a Generalization of a Theorem of Bridgeman, INTEGERS 25 (2025), Article A52, Theorem 3 (3), quoting Bridgeman.

TheoremBridgeman's dilogarithm series for a negative Pell solution#●ready to prove

Write \(L(x) = \sum_{m \ge 1} x^m/m^2 + \frac{1}{2} \log x \log(1 - x)\) for the Rogers dilogarithm on \([0, 1]\) (with \(\log 0 = 0\)). Let \(n\) be a natural number that is not a perfect square, let \(a, b\) be positive rationals with \(a^2 - n b^2 = -1\), and put \(u = a + b\sqrt{n}\). Define rationals \(a_k, b_k\) by \(a_0 = 1\), \(b_0 = 0\), \(a_{k+1} = a a_k + n b b_k\) and \(b_{k+1} = b a_k + a b_k\), so that \(u^k = a_k + b_k\sqrt{n}\). Then

\[ L(1/u^2) = \sum_{k \ge 1} L\left(\frac{a^2}{n b_{2k}^2}\right) + \sum_{k \ge 1} L\left(\frac{a^2}{a_{2k+1}^2}\right), \]

and if \(a\) and \(b\) are integers, then for every \(k \ge 0\) both \(b_{2k}/a\) and \(a_{2k+1}/a\) are integers.

public theorem_wanted rogersDilog_pell_negative_series {n : ℕ} (hn : ¬ IsSquare n) {a b : ℚ}
    (ha : 0 < a) (hb : 0 < b) (hpell : a ^ 2 - n * b ^ 2 = -1) {A B : ℕ → ℚ}
    (hA₀ : A 0 = 1) (hB₀ : B 0 = 0) (hA : ∀ k, A (k + 1) = a * A k + n * b * B k)
    (hB : ∀ k, B (k + 1) = b * A k + a * B k) :
    let L : ℝ → ℝ := fun x => (∑' n : ℕ, x ^ (n + 1) / ((n : ℝ) + 1) ^ 2) + log x * log (1 - x) / 2
    L (1 / ((a : ℝ) + b * √n) ^ 2) =
        ∑' k : ℕ, L ((a : ℝ) ^ 2 / (n * (B (2 * (k + 1)) : ℝ) ^ 2)) +
          ∑' k : ℕ, L ((a : ℝ) ^ 2 / (A (2 * (k + 1) + 1) : ℝ) ^ 2) ∧
      ((∃ a' b' : ℤ, a = a' ∧ b = b') →
        ∀ k, (∃ m : ℤ, B (2 * k) = a * m) ∧ ∃ m : ℤ, A (2 * k + 1) = a * m)

Sources

• Chance Sanford, A Dilogarithm Series and a Generalization of a Theorem of Bridgeman, INTEGERS 25 (2025), Article A52, Theorem 3 (4), quoting Bridgeman.

TheoremSanford's coupled recurrence#●ready to prove

Let \(a, b\) be real numbers in \((0, 1)\) with \(a \ne b\), and for every natural number \(m\) put

\[ x_m = \frac{a(a - b)(1 - b)^m}{a(1 - b)^{m+1} - b(1 - a)^{m+1}}, \qquad y_m = \frac{b(a - b)(1 - a)^m}{a(1 - b)^{m+1} - b(1 - a)^{m+1}}. \]

Then for every natural number \(n\),

\[ x_{n+1} = \frac{x_n(1 - y_n)}{1 - x_n y_n} \quad\text{and}\quad y_{n+1} = \frac{y_n(1 - x_n)}{1 - x_n y_n}. \]

public theorem_wanted sanford_coupled_recurrence {a b : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1)
    (hb₀ : 0 < b) (hb₁ : b < 1) (hab : a ≠ b) (n : ℕ) :
    let x : ℕ → ℝ := fun m =>
      a * (a - b) * (1 - b) ^ m / (a * (1 - b) ^ (m + 1) - b * (1 - a) ^ (m + 1))
    let y : ℕ → ℝ := fun m =>
      b * (a - b) * (1 - a) ^ m / (a * (1 - b) ^ (m + 1) - b * (1 - a) ^ (m + 1))
    x (n + 1) = x n * (1 - y n) / (1 - x n * y n) ∧ y (n + 1) = y n * (1 - x n) / (1 - x n * y n)

Sources

• Chance Sanford, A Dilogarithm Series and a Generalization of a Theorem of Bridgeman, INTEGERS 25 (2025), Article A52, Lemma 1.

TheoremSanford's dilogarithm series identity#●ready to prove

Write \(L(x) = \sum_{m \ge 1} x^m/m^2 + \frac{1}{2} \log x \log(1 - x)\) for the Rogers dilogarithm on \([0, 1]\) (with \(\log 0 = 0\)). For real numbers \(a, b \in (0, 1)\) with \(a \ne b\),

\[ \sum_{n \ge 0} L\left(\frac{ab(a - b)^2(1 - a)^n(1 - b)^n} {\left(a(1 - b)^{n+1} - b(1 - a)^{n+1}\right)^2}\right) = L(a) + L(b) - L\left(\frac{|a - b|}{1 - \min(a, b)}\right). \]

public theorem_wanted rogersDilog_sanford_principal_series {a b : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1)
    (hb₀ : 0 < b) (hb₁ : b < 1) (hab : a ≠ b) :
    let L : ℝ → ℝ := fun x => (∑' n : ℕ, x ^ (n + 1) / ((n : ℝ) + 1) ^ 2) + log x * log (1 - x) / 2
    ∑' n : ℕ, L (a * b * (a - b) ^ 2 * (1 - a) ^ n * (1 - b) ^ n /
        (a * (1 - b) ^ (n + 1) - b * (1 - a) ^ (n + 1)) ^ 2) =
      L a + L b - L (|a - b| / (1 - min a b))

Sources

• Chance Sanford, A Dilogarithm Series and a Generalization of a Theorem of Bridgeman, INTEGERS 25 (2025), Article A52, Theorem 4.

TheoremSanford's symmetric dilogarithm series#●ready to prove

Write \(L(x) = \sum_{m \ge 1} x^m/m^2 + \frac{1}{2} \log x \log(1 - x)\) for the Rogers dilogarithm on \([0, 1]\) (with \(\log 0 = 0\)). For every real number \(a \in (0, 1)\),

\[ \sum_{n \ge 1} L\left(\frac{a^2 \left(\frac{1 - a}{2}\right)^n \left(\frac{1 + a}{2}\right)^n} {\left(\left(\frac{1 + a}{2}\right)^{n+1} - \left(\frac{1 - a}{2}\right)^{n+1}\right)^2}\right) = L\left(\frac{1 - a}{1 + a}\right). \]

public theorem_wanted rogersDilog_sanford_symmetric_series {a : ℝ} (ha₀ : 0 < a) (ha₁ : a < 1) :
    let L : ℝ → ℝ := fun x => (∑' n : ℕ, x ^ (n + 1) / ((n : ℝ) + 1) ^ 2) + log x * log (1 - x) / 2
    ∑' n : ℕ, L (a ^ 2 * (1 / 2 - a / 2) ^ (n + 1) * (1 / 2 + a / 2) ^ (n + 1) /
        ((1 / 2 + a / 2) ^ (n + 2) - (1 / 2 - a / 2) ^ (n + 2)) ^ 2) =
      L ((1 - a) / (1 + a))

Sources

• Chance Sanford, A Dilogarithm Series and a Generalization of a Theorem of Bridgeman, INTEGERS 25 (2025), Article A52, Corollary 1.

TheoremSanford's Lucas-sequence dilogarithm series for \(Q > 0\)#●ready to prove

Write \(L(x) = \sum_{m \ge 1} x^m/m^2 + \frac{1}{2} \log x \log(1 - x)\) for the Rogers dilogarithm on \([0, 1]\) (with \(\log 0 = 0\)). Let \((P, Q)\) be Lucas sequence parameters with \(P > 0\), \(Q > 0\) and \(D = P^2 - 4Q > 0\), let \(U = U(P, Q)\) be the Lucas sequence, and put \(\alpha = (P + \sqrt{D})/2\). Then for every integer \(k \ge 1\),

\[ \sum_{n \ge 1} L\left(\frac{U_k^2 Q^{kn}}{U_{k(n+1)}^2}\right) = L\left(\frac{Q^k}{\alpha^{2k}}\right). \]

public theorem_wanted rogersDilog_lucasU_series (params : LucasSequenceParams)
    (hP : 0 < params.p) (hQ : 0 < params.q) (hD : 0 < params.p ^ 2 - 4 * params.q)
    {k : ℕ} (hk : 0 < k) :
    let L : ℝ → ℝ := fun x => (∑' n : ℕ, x ^ (n + 1) / ((n : ℝ) + 1) ^ 2) + log x * log (1 - x) / 2
    let α : ℝ := (params.p + √((params.p ^ 2 - 4 * params.q : ℤ) : ℝ)) / 2
    ∑' n : ℕ, L ((lucasU params k : ℝ) ^ 2 * (params.q : ℝ) ^ (k * (n + 1)) /
        (lucasU params (k * (n + 2)) : ℝ) ^ 2) = L ((params.q : ℝ) ^ k / α ^ (2 * k))

Sources

• Chance Sanford, A Dilogarithm Series and a Generalization of a Theorem of Bridgeman, INTEGERS 25 (2025), Article A52, Theorem 5 (8).

Uses 2

Statement usesParameters of a Lucas sequence · Lucas sequence \(U(P, Q)\)

TheoremSanford's Lucas-sequence dilogarithm series for \(Q < 0\)#●ready to prove

Write \(L(x) = \sum_{m \ge 1} x^m/m^2 + \frac{1}{2} \log x \log(1 - x)\) for the Rogers dilogarithm on \([0, 1]\) (with \(\log 0 = 0\)). Let \((P, Q)\) be Lucas sequence parameters with \(P > 0\) and \(Q < 0\), let \(U = U(P, Q)\) be the Lucas sequence and \(V = V(P, Q)\) its companion, and put \(D = P^2 - 4Q\) and \(\alpha = (P + \sqrt{D})/2\). Then for every odd natural number \(k\),

\[ \sum_{n \ge 1} L\left(-\frac{V_k^2 Q^{k(2n-1)}}{D\,U_{2kn}^2}\right) + \sum_{n \ge 1} L\left(\frac{V_k^2 Q^{2kn}}{V_{k(2n+1)}^2}\right) = L\left(-\frac{Q^k}{\alpha^{2k}}\right). \]

public theorem_wanted rogersDilog_lucasUV_series_of_neg (params : LucasSequenceParams)
    (hP : 0 < params.p) (hQ : params.q < 0) {k : ℕ} (hk : Odd k) :
    let L : ℝ → ℝ := fun x => (∑' n : ℕ, x ^ (n + 1) / ((n : ℝ) + 1) ^ 2) + log x * log (1 - x) / 2
    let D : ℤ := params.p ^ 2 - 4 * params.q
    let α : ℝ := (params.p + √(D : ℝ)) / 2
    ∑' n : ℕ, L (-(lucasV params k : ℝ) ^ 2 * (params.q : ℝ) ^ (k * (2 * n + 1)) /
        ((D : ℝ) * (lucasU params (2 * k * (n + 1)) : ℝ) ^ 2)) +
      ∑' n : ℕ, L ((lucasV params k : ℝ) ^ 2 * (params.q : ℝ) ^ (2 * k * (n + 1)) /
        (lucasV params (k * (2 * n + 3)) : ℝ) ^ 2) =
      L (-(params.q : ℝ) ^ k / α ^ (2 * k))

Sources

• Chance Sanford, A Dilogarithm Series and a Generalization of a Theorem of Bridgeman, INTEGERS 25 (2025), Article A52, Theorem 5 (9).

Uses 3

Statement usesParameters of a Lucas sequence · Lucas sequence \(U(P, Q)\) · Companion Lucas sequence \(V(P, Q)\)

7 fully proved8 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.