Landen connection formula and poly-Bernoulli numbers

29 fully proved8 ready to prove

Pole series and Landen data

DefinitionLinear fractional pole series#✓fully proved

For real numbers \(a\) and \(c\), this is the power series \(F_{a,c}(u)\) of \(\frac{cu}{a - cu}\): it is \(\sum_{n \ge 1} (c/a)^n u^n\) if \(a \neq 0\), the constant \(-1\) if \(a = 0\) and \(c \neq 0\), and \(0\) (a junk value) if \(a = c = 0\). It is \(u\) times the summand \(\frac{c}{a - cu}\) of \(G_g(u) = \frac{c}{a - cu} - \frac{d}{b - du}\) for the matrix \(g\) with rows \((a, b)\) and \((c, d)\).

public noncomputable def linearFractionalPoleSeries (a c : ℝ) : ℝ⟦X⟧ :=
  if a = 0 then (if c = 0 then 0 else -1)
  else mk fun n => if n = 0 then 0 else (c / a) ^ n

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, the function G_g(t) before Table 1.

Used by 3

Used byLanden form series · Landen form series of the identity matrix · The linear fractional pole series solves its defining equation

TheoremThe linear fractional pole series solves its defining equation#✓fully proved

For all real numbers \(a\) and \(c\), the linear fractional pole series \(F_{a,c}(u)\), the power series of \(\frac{cu}{a - cu}\), satisfies \((a - cu) \cdot F_{a,c}(u) = cu\) in \(\mathbb{R}[[u]]\).

public theorem linearFractionalPoleSeries_spec (a c : ℝ) :
    (C a - C c * X) * linearFractionalPoleSeries a c = C c * X

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, the function G_g(t) before Table 1.

Uses 1

Statement usesLinear fractional pole series

DefinitionLanden form series#✓fully proved

For real numbers \(a, b, c, d\), viewed as the matrix \(g\) with rows \((a, b)\) and \((c, d)\), this is the power series \(u \cdot G_g(u) = \frac{cu}{a - cu} - \frac{du}{b - du} \in \mathbb{R}[[u]]\), where \(G_g(t) = \frac{c}{a - ct} - \frac{d}{b - dt}\). Here the power series of \(\frac{cu}{a - cu}\) is \(\sum_{n \ge 1} (c/a)^n u^n\) if \(a \neq 0\), the constant \(-1\) if \(a = 0\) and \(c \neq 0\), and \(0\) if \(a = c = 0\); likewise for \(\frac{du}{b - du}\) with \(b, d\) in place of \(a, c\). For \(g \in GL_2(\mathbb{R})\) the last case does not occur.

public noncomputable def landenFormSeries (a b c d : ℝ) : ℝ⟦X⟧ :=
  linearFractionalPoleSeries a c - linearFractionalPoleSeries b d

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, the function G_g(t) before Table 1.

Uses 1 · Used by 6

Statement usesLinear fractional pole series

Used byWeighted form series · Initial value of the generalized multiple polylogarithm · Recurrence for appending the entry 1 · Recurrence for raising the last entry · Landen form series of the identity matrix · Reversed recursion for Kamano's generalized multiple polylogarithm

TheoremLanden form series of the identity matrix#✓fully proved

For the identity matrix \(g\), with rows \((1, 0)\) and \((0, 1)\), the Landen form series \(u \cdot G_g(u)\) is the constant power series \(1\) in \(\mathbb{R}[[u]]\); that is, \(G_g(t) = 1/t\).

public theorem landenFormSeries_identity : landenFormSeries 1 0 0 1 = 1

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Table 1.

Uses 2

Statement usesLanden form series

Proof usesLinear fractional pole series

DefinitionFormal integral against \(du/u\)#✓fully proved

For a real power series \(h\), this is the power series \(\int_0^z h(u)\,du/u\) computed coefficientwise: for \(n \ge 1\) its coefficient of \(z^n\) is the coefficient of \(u^n\) in \(h\) divided by \(n\), and its constant coefficient is \(0\). The constant coefficient of \(h\) is ignored, so this is the termwise integral only when \(h\) has zero constant term.

public noncomputable def integralDivX (h : ℝ⟦X⟧) : ℝ⟦X⟧ :=
  mk fun n => coeff n h / n

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, the integrals defining Li_k(g; (β, γ); z).

Used by 5

Used byInitial value of the generalized multiple polylogarithm · Recurrence for appending the entry 1 · Recurrence for raising the last entry · The formal integral against \(du/u\) is a right inverse of \(z \, d/dz\) · Reversed recursion for Kamano's generalized multiple polylogarithm

TheoremThe formal integral against \(du/u\) is a right inverse of \(z \, d/dz\)#✓fully proved

Let \(h \in \mathbb{R}[[z]]\) be a power series with zero constant term, and let \(I(h) = \sum_{n \ge 1} \frac{[z^n] h}{n} z^n\) be its formal integral \(\int_0^z h(u) \, du / u\), where \([z^n] h\) is the coefficient of \(z^n\) in \(h\). Then \(I(h)\) has zero constant term and \(z \, \frac{d}{dz} I(h) = h\).

public theorem integralDivX_spec (h : ℝ⟦X⟧) (h0 : constantCoeff h = 0) :
    constantCoeff (integralDivX h) = 0 ∧ X * derivative (integralDivX h) = h

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, the integrals defining Li_k(g; (β, γ); z).

Uses 1

Statement usesFormal integral against \(du/u\)

StructureLanden data#✓fully proved

Landen data \(g = (g_0, g_1, \dots, g_s)\) consist of a natural number \(s\), real numbers \(c_0, d_0\), and real numbers \(a_i, b_i, c_i, d_i\) for \(1 \le i \le s\). They encode the real \(2 \times 2\) matrix \(g_0\) with rows \((1, -1)\) and \((c_0, d_0)\) and, for \(1 \le i \le s\), the matrix \(g_i\) with rows \((a_i, b_i)\) and \((c_i, d_i)\). No invertibility is required.

MetaMathlibExt.LandenData · 15 lines

public structure LandenData where
  /-- The number `s` of matrices `g_1, …, g_s`. -/
  s : ℕ
  /-- The entry `c₀` of `g₀ = (1 -1; c₀ d₀)`. -/
  c₀ : ℝ
  /-- The entry `d₀` of `g₀ = (1 -1; c₀ d₀)`. -/
  d₀ : ℝ
  /-- The upper-left entries `a_i` of `g_i`. -/
  a : Fin s → ℝ
  /-- The upper-right entries `b_i` of `g_i`. -/
  b : Fin s → ℝ
  /-- The lower-left entries `c_i` of `g_i`. -/
  c : Fin s → ℝ
  /-- The lower-right entries `d_i` of `g_i`. -/
  d : Fin s → ℝ

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2.

Used by 19

Used byWeighted form series · Kamano's generalized multiple polylogarithm · Generalized Landen connection formula · Landen formula in the classical case · Initial value of the generalized multiple polylogarithm · Recurrence for appending the entry 1 · Sum formula · Recurrence for raising the last entry · Generalized poly-Bernoulli numbers of the second kind · Sum formula for generalized poly-Bernoulli numbers \(B_n\) · Generalized poly-Bernoulli numbers of the first kind · Generalized poly-Bernoulli numbers \(C_n\) as Taylor coefficients · Landen formula for generalized poly-Bernoulli numbers \(C_n\) · Sum formula for generalized poly-Bernoulli numbers \(C_n\) · Landen exponential variable · Defining relation of the Landen exponential variable · Reversed recursion for Kamano's generalized multiple polylogarithm · Transformed Landen data · The transformation of Landen data is an involution

Landen Data

DefinitionTransformed Landen data#✓fully proved

For Landen data \(g = (g_0, g_1, \dots, g_s)\) with \(g_0 = \begin{pmatrix} 1 & -1 \\ c_0 & d_0 \end{pmatrix}\) and \(g_i = \begin{pmatrix} a_i & b_i \\ c_i & d_i \end{pmatrix}\) for \(1 \le i \le s\), the transformed data \(\tilde g = (\tilde g_0, \tilde g_1, \dots, \tilde g_s)\) has the same \(s\), with \(\tilde g_0 = \begin{pmatrix} 1 & -1 \\ -d_0 & -c_0 \end{pmatrix}\) and, for \(1 \le i \le s\), the matrix \(\tilde g_i\) has first row \((a_i, b_i)\) and second row \(((c_0 - d_0) a_i - c_i, (c_0 - d_0) b_i - d_i)\). Equivalently, \(\tilde g_i = \begin{pmatrix} 1 & 0 \\ c_0 - d_0 & -1 \end{pmatrix} g_i\) for \(0 \le i \le s\).

public def tilde (D : LandenData) : LandenData where
  s := D.s
  c₀ := -D.d₀
  d₀ := -D.c₀
  a := D.a
  b := D.b
  c := fun i => (D.c₀ - D.d₀) * D.a i - D.c i
  d := fun i => (D.c₀ - D.d₀) * D.b i - D.d i

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, display before Theorem 2.

Uses 1 · Used by 3

Statement usesLanden data

Used byGeneralized Landen connection formula · Landen formula for generalized poly-Bernoulli numbers \(C_n\) · The transformation of Landen data is an involution

TheoremThe transformation of Landen data is an involution#✓fully proved

For Landen data \(g = (g_0, g_1, \dots, g_s)\) with \(g_0 = \begin{pmatrix} 1 & -1 \\ c_0 & d_0 \end{pmatrix}\), let \(\tilde g\) be the transformed data, given by \(\tilde g_i = \begin{pmatrix} 1 & 0 \\ c_0 - d_0 & -1 \end{pmatrix} g_i\) for \(0 \le i \le s\). Then the transformed data of \(\tilde g\) is \(g\) itself: \(\tilde{\tilde g} = g\).

public theorem tilde_tilde (D : LandenData) : D.tilde.tilde = D

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, remark before Theorem 2.

Uses 2

Statement usesLanden data · Transformed Landen data

DefinitionWeighted form series#✓fully proved

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data, where \(g_i\) has rows \((a_i, b_i)\) and \((c_i, d_i)\) for \(1 \le i \le s\), and let \(w_1, \dots, w_s\) be real numbers. The weighted form series of \(g\) with weights \(w\) is the formal power series \(u \sum_{i=1}^{s} w_i G_{g_i}(u) \in \mathbb{R}[[u]]\), where \(u\,G_{g_i}(u)\) is the Landen form series of \(g_i\): the expansion of \(\frac{c_i u}{a_i - c_i u} - \frac{d_i u}{b_i - d_i u}\), a fraction with zero numerator and zero denominator being read as \(0\).

public noncomputable def formSeries (D : LandenData) (w : Fin D.s → ℝ) : ℝ⟦X⟧ :=
  ∑ i, C (w i) * landenFormSeries (D.a i) (D.b i) (D.c i) (D.d i)

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, definition of Li_k(g; (β, γ); z).

Uses 2 · Used by 3

Statement usesLanden data · Landen form series

Used byRecurrence for appending the entry 1 · Recurrence for raising the last entry · Reversed recursion for Kamano's generalized multiple polylogarithm

DefinitionReversed recursion for Kamano's generalized multiple polylogarithm#✓fully proved

Fix Landen data \(g\), with \(g_0 = \begin{pmatrix} 1 & -1 \\ c_0 & d_0 \end{pmatrix}\) and \(g_i = \begin{pmatrix} a_i & b_i \\ c_i & d_i \end{pmatrix}\) for \(1 \le i \le s\), and weights \(\beta, \gamma \in \mathbb{R}^s\). For a real matrix \(h = \begin{pmatrix} a & b \\ c & d \end{pmatrix}\) let \(z\,G_h(z) \in \mathbb{R}[[z]]\) be the power series of \(\frac{cz}{a - cz} - \frac{dz}{b - dz}\), where a term whose numerator and denominator are both \(0\) is read as \(0\); for \(w \in \mathbb{R}^s\) let \(\Phi_w = \sum_{i=1}^s w_i \, z\,G_{g_i}(z) \in \mathbb{R}[[z]]\); and for \(f = \sum_n f_n z^n \in \mathbb{R}[[z]]\) let \(I(f) = \sum_{n \ge 1} (f_n / n) z^n\), which is the formal integral \(\int_0^z f(u) \, du / u\) when \(f_0 = 0\). For a finite list \(\ell\) of natural numbers, the series \(L(\ell) \in \mathbb{R}[[z]]\) is defined recursively: \(L(\ell) = 0\) if \(\ell\) is empty or its first entry is \(0\); \(L((1)) = I(z\,G_{g_0}(z))\); \(L((1, r, \ell')) = I(\Phi_\gamma \cdot L((r, \ell')))\) for every natural number \(r\) and list \(\ell'\); and \(L((n + 2, \ell')) = I(\Phi_\beta \cdot L((n + 1, \ell')))\) for every natural number \(n\) and list \(\ell'\).

Applied to the reversed list \((k_r, \dots, k_1)\) of an index \(k = (k_1, \dots, k_r)\), \(L\) gives Kamano's generalized multiple polylogarithm \(\mathrm{Li}_k(g; (\beta, \gamma); z)\). A list with a zero entry anywhere gives \(0\).

public noncomputable def polylogRev (D : LandenData) (β γ : Fin D.s → ℝ) :
    List ℕ → ℝ⟦X⟧
  | [] => 0
  | 0 :: _ => 0
  | [1] => integralDivX (landenFormSeries 1 (-1) D.c₀ D.d₀)
  | 1 :: r :: rs => integralDivX (D.formSeries γ * polylogRev D β γ (r :: rs))
  | (n + 2) :: rs => integralDivX (D.formSeries β * polylogRev D β γ ((n + 1) :: rs))
termination_by l => l.sum

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, display (6) and the two inductive integrals before it.

Uses 4 · Used by 4

Statement usesLanden data · Weighted form series · Formal integral against \(du/u\) · Landen form series

Used byKamano's generalized multiple polylogarithm · Initial value of the generalized multiple polylogarithm · Recurrence for appending the entry 1 · Recurrence for raising the last entry

Multiple polylogarithms

DefinitionKamano's generalized multiple polylogarithm#✓fully proved

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data, where \(g_0\) has rows \((1, -1)\) and \((c_0, d_0)\) and \(g_i\) has rows \((a_i, b_i)\) and \((c_i, d_i)\), and let \(\beta, \gamma \in \mathbb{R}^s\). For a matrix \(h\) with rows \((a, b)\) and \((c, d)\) put \(G_h(u) = \frac{c}{a - c u} - \frac{d}{b - d u}\), a fraction with zero numerator and zero denominator being read as \(0\). For an index \(\mathbf{k} = (k_1, \dots, k_r)\) of positive integers put \(\mathbf{k}{\uparrow} = (k_1, \dots, k_r + 1)\) and \(\mathbf{k}{\rightarrow} = (k_1, \dots, k_r, 1)\). The generalized multiple polylogarithm \(\mathrm{Li}_{\mathbf{k}} = \mathrm{Li}_{\mathbf{k}}(g; (\beta, \gamma); z) \in \mathbb{R}[[z]]\) is defined recursively by \(\mathrm{Li}_{(1)} = \int_0^z \left(\frac{c_0}{1 - c_0 u} + \frac{d_0}{1 + d_0 u}\right) du\), \(\mathrm{Li}_{\mathbf{k}{\uparrow}} = \int_0^z \sum_{i=1}^{s} \beta_i G_{g_i}(u) \, \mathrm{Li}_{\mathbf{k}}(u)\,du\) and \(\mathrm{Li}_{\mathbf{k}{\rightarrow}} = \int_0^z \sum_{i=1}^{s} \gamma_i G_{g_i}(u) \, \mathrm{Li}_{\mathbf{k}}(u)\,du\), where integrals of power series are taken term by term. A list of natural numbers that is empty or has a zero entry gives \(0\).

public noncomputable def generalizedMultiplePolylog (D : LandenData) (β γ : Fin D.s → ℝ)
    (k : List ℕ) : ℝ⟦X⟧ :=
  D.polylogRev β γ k.reverse

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, display (6).

Uses 2 · Used by 10

Statement usesLanden data · Reversed recursion for Kamano's generalized multiple polylogarithm

Used byGeneralized Landen connection formula · Landen formula in the classical case · Initial value of the generalized multiple polylogarithm · Recurrence for appending the entry 1 · Sum formula · Recurrence for raising the last entry · Generalized poly-Bernoulli numbers of the second kind · Generalized poly-Bernoulli numbers of the first kind · Generalized poly-Bernoulli numbers \(C_n\) as Taylor coefficients · Landen formula for generalized poly-Bernoulli numbers \(C_n\)

TheoremInitial value of the generalized multiple polylogarithm#✓fully proved

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data, where \(g_0\) has rows \((1, -1)\) and \((c_0, d_0)\), and let \(\beta, \gamma \in \mathbb{R}^s\). Then \(\mathrm{Li}_{(1)}(g; (\beta, \gamma); z) = \int_0^z G_{g_0}(u)\,du\), where \(u\,G_{g_0}(u) = \frac{c_0 u}{1 - c_0 u} + \frac{d_0 u}{1 + d_0 u}\) is the Landen form series of \(g_0\) and the integral of a power series is taken term by term.

public theorem generalizedMultiplePolylog_one (D : LandenData) (β γ : Fin D.s → ℝ) :
    generalizedMultiplePolylog D β γ [1] =
      integralDivX (landenFormSeries 1 (-1) D.c₀ D.d₀)

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, display (6).

Uses 5

Statement usesLanden data · Kamano's generalized multiple polylogarithm · Formal integral against \(du/u\) · Landen form series

Proof usesReversed recursion for Kamano's generalized multiple polylogarithm

TheoremRecurrence for raising the last entry#✓fully proved

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data and let \(\beta, \gamma \in \mathbb{R}^s\). For every list \((k_1, \dots, k_{r-1})\) of natural numbers (possibly empty) and every natural number \(m\), writing \(\mathbf{k} = (k_1, \dots, k_{r-1}, m + 1)\), \(\mathrm{Li}_{(k_1, \dots, k_{r-1}, m + 2)}(g; (\beta, \gamma); z) = \int_0^z \sum_{i=1}^{s} \beta_i G_{g_i}(u) \, \mathrm{Li}_{\mathbf{k}}(g; (\beta, \gamma); u)\,du\), where \(u \sum_{i} \beta_i G_{g_i}(u)\) is the weighted form series of \(g\) with weights \(\beta\) and the integral of a power series is taken term by term.

public theorem generalizedMultiplePolylog_up (D : LandenData) (β γ : Fin D.s → ℝ)
    (k : List ℕ) (m : ℕ) :
    generalizedMultiplePolylog D β γ (k ++ [m + 2]) =
      integralDivX (D.formSeries β * generalizedMultiplePolylog D β γ (k ++ [m + 1]))

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2.

Uses 6

Statement usesLanden data · Weighted form series · Kamano's generalized multiple polylogarithm · Formal integral against \(du/u\)

Proof usesReversed recursion for Kamano's generalized multiple polylogarithm · Landen form series

TheoremRecurrence for appending the entry 1#✓fully proved

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data and let \(\beta, \gamma \in \mathbb{R}^s\). For every nonempty list \(\mathbf{k} = (k_1, \dots, k_r)\) of natural numbers, \(\mathrm{Li}_{(k_1, \dots, k_r, 1)}(g; (\beta, \gamma); z) = \int_0^z \sum_{i=1}^{s} \gamma_i G_{g_i}(u) \, \mathrm{Li}_{\mathbf{k}}(g; (\beta, \gamma); u)\,du\), where \(u \sum_{i} \gamma_i G_{g_i}(u)\) is the weighted form series of \(g\) with weights \(\gamma\) and the integral of a power series is taken term by term.

public theorem generalizedMultiplePolylog_right (D : LandenData) (β γ : Fin D.s → ℝ)
    (k : List ℕ) (hk : k ≠ []) :
    generalizedMultiplePolylog D β γ (k ++ [1]) =
      integralDivX (D.formSeries γ * generalizedMultiplePolylog D β γ k)

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2.

Uses 6

Statement usesLanden data · Weighted form series · Kamano's generalized multiple polylogarithm · Formal integral against \(du/u\)

Proof usesReversed recursion for Kamano's generalized multiple polylogarithm · Landen form series

DefinitionCoefficient recursion for multiple polylogarithms#✓fully proved

For a finite list \(\ell\) of natural numbers and \(m \in \mathbb{N}\), the real number \(c_\ell(m)\) is defined by recursion on \(\ell\): for the empty list, \(c_{()}(m)\) is \(1\) if \(m = 0\) and \(0\) otherwise; for the list \((a, \ell')\) with first entry \(a\) followed by the list \(\ell'\), \(c_{(a, \ell')}(m) = \big(\sum_{m' < m} c_{\ell'}(m')\big) / m^a\).

The multiple polylogarithm \(\mathrm{Li}_{(k_1, \dots, k_r)}(z)\) is defined as the power series whose coefficient of \(z^m\) is \(c_{(k_r, \dots, k_1)}(m)\).

public noncomputable def multiplePolylogCoeffRev : List ℕ → ℕ → ℝ
  | [], m => if m = 0 then 1 else 0
  | a :: rs, m => (∑ m' ∈ Finset.range m, multiplePolylogCoeffRev rs m') / (m : ℝ) ^ a

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 1, definition of Li_k(z).

Used by 2

Used byDepth-one multiple polylogarithm · Multiple polylogarithm

DefinitionMultiple polylogarithm#✓fully proved

For a finite sequence \(k = (k_1, \dots, k_r)\) of natural numbers with \(r \ge 1\), the multiple polylogarithm is the formal power series

\[\mathrm{Li}_k(z) = \sum_{0 < m_1 < \cdots < m_r} \frac{z^{m_r}}{m_1^{k_1} \cdots m_r^{k_r}}\]

in \(\mathbb{R}[[z]]\); for the empty sequence it is the constant series \(1\).

public noncomputable def multiplePolylog (k : List ℕ) : ℝ⟦X⟧ :=
  mk (multiplePolylogCoeffRev k.reverse)

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 1.

Uses 1 · Used by 2

Statement usesCoefficient recursion for multiple polylogarithms

Used byDepth-one multiple polylogarithm · Landen connection formula

TheoremDepth-one multiple polylogarithm#✓fully proved

For every natural number \(a\) and every integer \(m \ge 1\), the coefficient of \(z^m\) in the multiple polylogarithm \(\mathrm{Li}_{(a)}(z)\) is \(1/m^a\).

public theorem coeff_multiplePolylog_singleton (a : ℕ) {m : ℕ} (hm : 0 < m) :
    coeff m (multiplePolylog [a]) = 1 / (m : ℝ) ^ a

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 1.

Uses 2

Statement usesMultiple polylogarithm

Proof usesCoefficient recursion for multiple polylogarithms

DefinitionCoefficient recursion for the non-strict multiple polylogarithm#✓fully proved

For a finite list \(\ell\) of natural numbers and \(m \in \mathbb{N}\), the real number \(c_\ell(m)\) is defined by recursion on \(\ell\): for the empty list, \(c_\ell(m) = 1\) if \(m = 0\) and \(c_\ell(m) = 0\) otherwise; for a list \(\ell = (a, \ell')\) with first entry \(a\) followed by the list \(\ell'\),

\[c_{(a, \ell')}(m) = \frac{1}{m^a} \sum_{m' = 0}^{m} c_{\ell'}(m'),\]

where \(0^0 = 1\) and \(1/0 = 0\).

Applied to the reversed list \((k_r, \dots, k_1)\) of positive integers \(k_1, \dots, k_r\) with \(r \ge 1\), it gives the coefficient of \(z^m\) in \(\sum_{0 < m_1 \le \cdots \le m_r} z^{m_r} / (m_1^{k_1} \cdots m_r^{k_r})\).

public noncomputable def multiplePolylogStarCoeffRev : List ℕ → ℕ → ℝ
  | [], m => if m = 0 then 1 else 0
  | a :: rs, m =>
      (∑ m' ∈ Finset.range (m + 1), multiplePolylogStarCoeffRev rs m') / (m : ℝ) ^ a

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 1, definition of Li⋆_k(z).

Used by 2

Used byDepth-one non-strict multiple polylogarithm · Non-strict multiple polylogarithm

DefinitionNon-strict multiple polylogarithm#✓fully proved

For an index \(k = (k_1, \dots, k_r)\) of positive integers with \(r \ge 1\), the non-strict multiple polylogarithm is the formal power series

\[\mathrm{Li}^\star_k(z) = \sum_{0\lt m_1\le\cdots\le m_r} \frac{z^{m_r}}{m_1^{k_1} \cdots m_r^{k_r}}\]

in \(\mathbb{R}[[z]]\).

The definition accepts every finite list \(k\) of natural numbers: for \(r \ge 1\) the coefficient of \(z^m\) is the sum of \(1/(m_1^{k_1} \cdots m_r^{k_r})\) over \(0 \le m_1 \le \cdots \le m_r = m\), where \(0^0 = 1\) and \(1/0 = 0\) (so for an index the terms with some \(m_i = 0\) vanish), and the empty list gives the constant series \(1\).

public noncomputable def multiplePolylogStar (k : List ℕ) : ℝ⟦X⟧ :=
  mk (multiplePolylogStarCoeffRev k.reverse)

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 1.

Uses 1 · Used by 2

Statement usesCoefficient recursion for the non-strict multiple polylogarithm

Used byDepth-one non-strict multiple polylogarithm · Duality of multi-poly-Bernoulli-star numbers

TheoremDepth-one non-strict multiple polylogarithm#✓fully proved

For all natural numbers \(a\) and \(m\), the coefficient of \(z^m\) in the non-strict multiple polylogarithm \(\mathrm{Li}^{\star}_{(a)}(z)\) is \(1/m^a\), with the conventions \(0^0 = 1\) and \(1/0 = 0\). In particular \(\mathrm{Li}^{\star}_{(a)}(z) = \sum_{m \ge 1} z^m / m^a\) for \(a \ge 1\).

public theorem coeff_multiplePolylogStar_singleton (a m : ℕ) :
    coeff m (multiplePolylogStar [a]) = 1 / (m : ℝ) ^ a

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 1.

Uses 2

Statement usesNon-strict multiple polylogarithm

Proof usesCoefficient recursion for the non-strict multiple polylogarithm

DefinitionHoffman dual on reversed lists#✓fully proved

The auxiliary map \(R\) on finite lists \(l = (l_1, \dots, l_m)\) of natural numbers is defined recursively by: \(R(()) = ()\); \(R(l) = ()\) if \(l_1 = 0\); \(R((1)) = (1)\); if \(l_1 = 1\) and \(m \ge 2\), then \(R(l)\) is \(R((l_2, \dots, l_m))\) with its first entry increased by \(1\) (unchanged if that list is empty); and if \(l_1 \ge 2\), then \(R(l) = (1, r_1, \dots, r_p)\) where \((r_1, \dots, r_p) = R((l_1 - 1, l_2, \dots, l_m))\).

Reading an index from its last entry, these are the rules \((1)^\vee = (1)\), \((k\rightarrow)^\vee = (k^\vee)\uparrow\) and \((k\uparrow)^\vee = (k^\vee)\rightarrow\) of Hoffman's dual index, where \(k\uparrow\) increases the last entry of \(k\) by \(1\) and \(k\rightarrow\) appends an entry \(1\): the Hoffman dual of an index \(k\) is the reverse of \(R\) applied to the reverse of \(k\).

public def hoffmanDualRev : List ℕ → List ℕ
  | [] => []
  | 0 :: _ => []
  | [1] => [1]
  | 1 :: r :: rs => (hoffmanDualRev (r :: rs)).modifyHead (· + 1)
  | (n + 2) :: rs => 1 :: hoffmanDualRev ((n + 1) :: rs)
termination_by l => l.sum

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2, definition of Hoffman's dual index.

Used by 2

Used byHoffman dual index · Small values of the Hoffman dual

DefinitionHoffman dual index#✓fully proved

For an index \(k = (k_1, \dots, k_r)\) of positive integers write \(k\uparrow = (k_1, \dots, k_r + 1)\) and \(k\rightarrow = (k_1, \dots, k_r, 1)\). The Hoffman dual index \(k^\vee\) is defined recursively by \((1)^\vee = (1)\), \((k\uparrow)^\vee = (k^\vee)\rightarrow\) and \((k\rightarrow)^\vee = (k^\vee)\uparrow\). On other finite lists of natural numbers, the empty list is sent to the empty list and a list with an entry \(0\) is sent to an unspecified junk value.

public def hoffmanDual (k : List ℕ) : List ℕ :=
  (hoffmanDualRev k.reverse).reverse

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2.

Uses 1 · Used by 2

Statement usesHoffman dual on reversed lists

Used bySmall values of the Hoffman dual · Duality of multi-poly-Bernoulli-star numbers

TheoremSmall values of the Hoffman dual#✓fully proved

The Hoffman dual index satisfies \((1)^\vee = (1)\), \((3)^\vee = (1, 1, 1)\) and \((1, 2)^\vee = (2, 1)\).

public theorem hoffmanDual_small_values :
    hoffmanDual [1] = [1] ∧ hoffmanDual [3] = [1, 1, 1] ∧ hoffmanDual [1, 2] = [2, 1]

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 2.

Uses 2

Statement usesHoffman dual index

Proof usesHoffman dual on reversed lists

DefinitionLanden exponential variable#✓fully proved

For Landen data \(g\) whose matrix \(g_0\) has rows \((1, -1)\) and \((c_0, d_0)\), this is the formal power series \(z(t) = (e^t - 1)(c_0 e^t + d_0)^{-1}\) in \(\mathbb{R}[[t]]\). The inverse is the power series inverse, which exists exactly when \(c_0 + d_0 \neq 0\); when \(c_0 + d_0 = 0\) the inverse is taken to be \(0\), so \(z(t) = 0\).

public noncomputable def landenExpVariable (D : LandenData) : ℝ⟦X⟧ :=
  (exp ℝ - 1) * (C D.c₀ * exp ℝ + C D.d₀)⁻¹

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 4, definition of C_n^{(k, g, (β, γ))}.

Uses 1 · Used by 5

Statement usesLanden data

Used byGeneralized poly-Bernoulli numbers of the second kind · Generalized poly-Bernoulli numbers of the first kind · Generalized poly-Bernoulli numbers \(C_n\) as Taylor coefficients · Landen formula for generalized poly-Bernoulli numbers \(C_n\) · Defining relation of the Landen exponential variable

TheoremDefining relation of the Landen exponential variable#✓fully proved

Let \(g\) be Landen data whose matrix \(g_0\) has rows \((1, -1)\) and \((c_0, d_0)\) with \(c_0 + d_0 \neq 0\), and let \(z(t) = (e^t - 1)(c_0 e^t + d_0)^{-1} \in \mathbb{R}[[t]]\) be its Landen exponential variable. Then \((c_0 e^t + d_0)\, z(t) = e^t - 1\) in \(\mathbb{R}[[t]]\).

public theorem landenExpVariable_spec (D : LandenData) (h : D.c₀ + D.d₀ ≠ 0) :
    (C D.c₀ * exp ℝ + C D.d₀) * landenExpVariable D = exp ℝ - 1

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 4.

Uses 2

Statement usesLanden data · Landen exponential variable

DefinitionGeneralized poly-Bernoulli numbers of the first kind#✓fully proved

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data, where \((c_0, d_0)\) is the bottom row of the matrix \(g_0\), let \(\beta, \gamma \in \mathbb{R}^s\), and let \(k = (k_1, \dots, k_r)\) be a list of natural numbers; write \(k\uparrow = (k_1, \dots, k_r + 1)\), with \(k\uparrow = ()\) when \(k\) is empty. Let \(z(t) \in \mathbb{R}[[t]]\) be the power series of \((e^t - 1)/(c_0 e^t + d_0)\) (the zero series when \(c_0 + d_0 = 0\)). The numbers \(C_n^{(k, g, (\beta, \gamma))} \in \mathbb{R}\), \(n \ge 0\), are defined by

\[\frac{d}{dt} \mathrm{Li}_{k\uparrow}(g; (\beta, \gamma); z(t)) = \sum_{n \ge 0} C_n^{(k, g, (\beta, \gamma))} \frac{t^n}{n!},\]

where \(\mathrm{Li}_{k\uparrow}(g; (\beta, \gamma); z)\) is Kamano's generalized multiple polylogarithm, into which the series \(z(t)\) is substituted.

public noncomputable def generalizedPolyBernoulliC (D : LandenData) (β γ : Fin D.s → ℝ)
    (k : List ℕ) (n : ℕ) : ℝ :=
  n.factorial * coeff n (derivative (subst (landenExpVariable D)
    (generalizedMultiplePolylog D β γ (k.modifyLast (· + 1)))))

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 4.

Uses 3 · Used by 4

Statement usesLanden data · Kamano's generalized multiple polylogarithm · Landen exponential variable

Used bySum formula for generalized poly-Bernoulli numbers \(B_n\) · Generalized poly-Bernoulli numbers \(C_n\) as Taylor coefficients · Landen formula for generalized poly-Bernoulli numbers \(C_n\) · Sum formula for generalized poly-Bernoulli numbers \(C_n\)

DefinitionGeneralized poly-Bernoulli numbers of the second kind#✓fully proved

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data, where \((c_0, d_0)\) is the bottom row of the matrix \(g_0\), let \(\beta, \gamma \in \mathbb{R}^s\), and let \(k = (k_1, \dots, k_r)\) be a list of natural numbers; write \(k\rightarrow = (k_1, \dots, k_r, 1)\), with \(k\rightarrow = (1)\) when \(k\) is empty. Let \(z(t) \in \mathbb{R}[[t]]\) be the power series of \((e^t - 1)/(c_0 e^t + d_0)\) (the zero series when \(c_0 + d_0 = 0\)). The numbers \(B_n^{(k, g, (\beta, \gamma))} \in \mathbb{R}\), \(n \ge 0\), are defined by

\[\frac{d}{dt} \mathrm{Li}_{k\rightarrow}(g; (\beta, \gamma); z(t)) = \sum_{n \ge 0} B_n^{(k, g, (\beta, \gamma))} \frac{t^n}{n!},\]

where \(\mathrm{Li}_{k\rightarrow}(g; (\beta, \gamma); z)\) is Kamano's generalized multiple polylogarithm, into which the series \(z(t)\) is substituted.

public noncomputable def generalizedPolyBernoulliB (D : LandenData) (β γ : Fin D.s → ℝ)
    (k : List ℕ) (n : ℕ) : ℝ :=
  n.factorial * coeff n (derivative (subst (landenExpVariable D)
    (generalizedMultiplePolylog D β γ (k ++ [1]))))

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 4.

Uses 3 · Used by 2

Statement usesLanden data · Kamano's generalized multiple polylogarithm · Landen exponential variable

Used bySum formula for generalized poly-Bernoulli numbers \(B_n\) · Sum formula for generalized poly-Bernoulli numbers \(C_n\)

TheoremGeneralized poly-Bernoulli numbers \(C_n\) as Taylor coefficients#✓fully proved

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data, where \((c_0, d_0)\) is the bottom row of the matrix \(g_0\), let \(\beta, \gamma \in \mathbb{R}^s\), let \(k = (k_1, \dots, k_r)\) be a list of natural numbers, and write \(k\uparrow = (k_1, \dots, k_r + 1)\), with \(k\uparrow = ()\) when \(k\) is empty. Let \(z(t) \in \mathbb{R}[[t]]\) be the power series of \((e^t - 1)/(c_0 e^t + d_0)\) (the zero series when \(c_0 + d_0 = 0\)). Then for every \(n \ge 0\) the generalized poly-Bernoulli number of the first kind satisfies

\[C_n^{(k, g, (\beta, \gamma))} = (n + 1)! \, [t^{n+1}] \, \mathrm{Li}_{k\uparrow}(g; (\beta, \gamma); z(t)),\]

where \([t^m] F\) is the coefficient of \(t^m\) in a power series \(F\) and \(\mathrm{Li}\) is Kamano's generalized multiple polylogarithm.

public theorem generalizedPolyBernoulliC_eq_coeff (D : LandenData) (β γ : Fin D.s → ℝ)
    (k : List ℕ) (n : ℕ) :
    generalizedPolyBernoulliC D β γ k n = (n + 1).factorial * coeff (n + 1)
      (subst (landenExpVariable D) (generalizedMultiplePolylog D β γ (k.modifyLast (· + 1))))

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Section 4.

Uses 4

Statement usesLanden data · Kamano's generalized multiple polylogarithm · Generalized poly-Bernoulli numbers of the first kind · Landen exponential variable

TheoremLanden connection formula#●ready to prove

Landen connection formula (Okuda–Ueno). Let \(n \ge 0\) and let \(k = (k_1, \dots, k_r)\) be an index of weight \(n\), that is, a finite sequence of positive integers with sum \(n\). Then the multiple polylogarithms satisfy the identity

\[\mathrm{Li}_k\left(\frac{z}{z - 1}\right) = (-1)^r \sum_{k'} \mathrm{Li}_{k'}(z)\]

in \(\mathbb{R}[[z]]\), where \(\mathrm{Li}_k(z) \in \mathbb{R}[[z]]\) is the multiple polylogarithm, \(\frac{z}{z - 1}\) stands for the series \(-\sum_{m \ge 1} z^m\) substituted into \(\mathrm{Li}_k\), and the sum runs over all indices \(k'\) of weight \(n\) from which \(k\) is obtained by adding up blocks of consecutive entries; equivalently, every partial sum \(k_1 + \cdots + k_j\) of \(k\) is also a partial sum of \(k'\).

public theorem_wanted multiplePolylog_landen_connection {n : ℕ} (k : Composition n) :
    subst (-(X * mk fun _ => (1 : ℝ))) (multiplePolylog k.blocks) =
      (-1 : ℝ) ^ k.length •
        ∑ k' : Composition n with k.boundaries ⊆ k'.boundaries, multiplePolylog k'.blocks

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Theorem 1 (quoting Okuda and Ueno, Prop. 9).

Uses 1

Statement usesMultiple polylogarithm

TheoremSum formula#●ready to prove

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data, let \(\beta, \gamma, \delta \in \mathbb{R}^s\), let \(\mu\) be a real number and let \(k \ge 1\) be an integer. Then \(\sum_{\mathbf{k}} \mu^{d(\mathbf{k}) - 1} \mathrm{Li}_{\mathbf{k}}(g; (\beta, \gamma); z) = \mathrm{Li}_{(k)}(g; (\beta + \mu \gamma, \delta); z)\), where the sum runs over all compositions \(\mathbf{k} = (k_1, \dots, k_r)\) of \(k\) (sequences of positive integers with \(k_1 + \dots + k_r = k\)) and \(d(\mathbf{k}) = r\) is the depth of \(\mathbf{k}\).

The paper takes \(\mu\) an indeterminate; both sides are polynomials in \(\mu\), so this is equivalent.

public theorem_wanted generalizedMultiplePolylog_sum_formula (D : LandenData)
    (β γ δ : Fin D.s → ℝ) (μ : ℝ) (k : ℕ) (hk : 0 < k) :
    ∑ c : Composition k, μ ^ (c.length - 1) • generalizedMultiplePolylog D β γ c.blocks =
      generalizedMultiplePolylog D (β + μ • γ) δ [k]

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Proposition 1, Identity (7).

Uses 2

Statement usesLanden data · Kamano's generalized multiple polylogarithm

TheoremGeneralized Landen connection formula#●ready to prove

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data, where \(g_0\) has rows \((1, -1)\) and \((c_0, d_0)\) and each \(g_i\) (\(1 \le i \le s\)) has rows \((a_i, b_i)\) and \((c_i, d_i)\) with \(a_i d_i - b_i c_i \ne 0\). Let \(\tilde g\) be the transformed data: \(\tilde g_0\) has rows \((1, -1)\) and \((-d_0, -c_0)\), and \(\tilde g_i = M g_i\), where \(M\) is the matrix with rows \((1, 0)\) and \((c_0 - d_0, -1)\). For all \(\beta, \gamma \in \mathbb{R}^s\) and every finite (possibly empty) sequence \(\mathbf{k}\) of positive integers, \(\mathrm{Li}_{\mathbf{k}}(g; (\beta, \gamma); \frac{z}{(c_0 - d_0) z - 1}) = \mathrm{Li}_{\mathbf{k}}(\tilde g; (\beta, \gamma); z)\) in \(\mathbb{R}[[z]]\), where \(\frac{z}{(c_0 - d_0) z - 1} = -\sum_{n \ge 0} (c_0 - d_0)^n z^{n+1}\) is substituted for \(z\).

The paper also assumes \(g_0 \in \mathrm{GL}_2(\mathbb{R})\), that is \(c_0 + d_0 \ne 0\); this is not needed. The invertibility of the \(g_i\) is needed: with \(a_i = c_i = 0\) the identity fails.

public theorem_wanted generalizedMultiplePolylog_landen_connection (D : LandenData)
    (hD : ∀ i, D.a i * D.d i - D.b i * D.c i ≠ 0) (β γ : Fin D.s → ℝ) {n : ℕ}
    (k : Composition n) :
    subst (-(X * mk fun m => (D.c₀ - D.d₀) ^ m)) (generalizedMultiplePolylog D β γ k.blocks) =
      generalizedMultiplePolylog D.tilde β γ k.blocks

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Theorem 2, Identity (8).

Uses 3

Statement usesLanden data · Transformed Landen data · Kamano's generalized multiple polylogarithm

TheoremLanden formula in the classical case#●ready to prove

Let \(g = (g_0, g_1, g_2)\) be the Landen data in which \(g_0 = g_2\) has rows \((1, -1)\) and \((1, 0)\) and \(g_1\) is the identity matrix, so that \(G_{g_1}(t) = 1/t\) and \(G_{g_2}(t) = 1/(1 - t)\). For all real numbers \(\beta_1\), \(\beta_2\), \(\gamma_1\), \(\gamma_2\) and every finite (possibly empty) sequence \(\mathbf{k}\) of positive integers, \(\mathrm{Li}_{\mathbf{k}}(g; ((\beta_1, \beta_2), (\gamma_1, \gamma_2)); \frac{z}{z - 1}) = -\mathrm{Li}_{\mathbf{k}}(g; ((\beta_1, \beta_1 - \beta_2), (\gamma_1, \gamma_1 - \gamma_2)); z)\) in \(\mathbb{R}[[z]]\), where \(\frac{z}{z - 1} = -\sum_{n \ge 1} z^n\) is substituted for \(z\).

public theorem_wanted generalizedMultiplePolylog_landen_connection_classical
    (β₁ β₂ γ₁ γ₂ : ℝ) {n : ℕ} (k : Composition n) :
    subst (-(X * mk fun _ => (1 : ℝ)))
        (generalizedMultiplePolylog ⟨2, 1, 0, ![1, 1], ![0, -1], ![0, 1], ![1, 0]⟩
          ![β₁, β₂] ![γ₁, γ₂] k.blocks) =
      -generalizedMultiplePolylog ⟨2, 1, 0, ![1, 1], ![0, -1], ![0, 1], ![1, 0]⟩
          ![β₁, β₁ - β₂] ![γ₁, γ₁ - γ₂] k.blocks

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Theorem 3, Identity (10).

Uses 2

Statement usesLanden data · Kamano's generalized multiple polylogarithm

TheoremDuality of multi-poly-Bernoulli-star numbers#●ready to prove

This duality is due to Imatomi. Let \(k\) be an index (a composition of a natural number \(m\)), let \(k^\vee\) be its Hoffman dual, and let \(\mathrm{Li}^\star_k\) be the non-strict multiple polylogarithm. Let \(F, G \in \mathbb{R}[[t]]\) satisfy \((e^t - 1) F = \mathrm{Li}^\star_k(1 - e^{-t})\) and \((1 - e^{-t}) G = \mathrm{Li}^\star_{k^\vee}(1 - e^{-t})\), and write \(F = \sum_{n \ge 0} C_{n,\star}^{(k)} t^n / n!\) and \(G = \sum_{n \ge 0} B_{n,\star}^{(k^\vee)} t^n / n!\). Then \(C_{n,\star}^{(k)} = (-1)^n B_{n,\star}^{(k^\vee)}\) for every \(n \ge 0\).

Since \(e^t - 1\) and \(1 - e^{-t}\) are non-zero-divisors in \(\mathbb{R}[[t]]\), these equations determine \(F\) and \(G\).

public theorem_wanted multiPolyBernoulliStar_duality {m : ℕ} (k : Composition m)
    (F G : ℝ⟦X⟧)
    (hF : (exp ℝ - 1) * F =
      subst (1 - rescale (-1 : ℝ) (exp ℝ)) (multiplePolylogStar k.blocks))
    (hG : (1 - rescale (-1 : ℝ) (exp ℝ)) * G =
      subst (1 - rescale (-1 : ℝ) (exp ℝ)) (multiplePolylogStar (hoffmanDual k.blocks)))
    (n : ℕ) :
    n.factorial * coeff n F = (-1 : ℝ) ^ n * (n.factorial * coeff n G)

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Theorem 4 (quoting Imatomi, Theorem 3.2), with generating functions (13) and (14).

Uses 2

Statement usesHoffman dual index · Non-strict multiple polylogarithm

TheoremSum formula for generalized poly-Bernoulli numbers \(C_n\)#●ready to prove

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data, let \(\beta, \gamma \in \mathbb{R}^s\), let \(\mu\) be a real number, and let \(k \ge 1\) and \(n \ge 0\) be integers. Write \(B_n\) and \(C_n\) for Kamano's generalized poly-Bernoulli numbers of the second and first kind, \(d(\mathbf{k})\) for the number of entries of an index \(\mathbf{k}\), and \(\{1\}^k = (1, \dots, 1)\) for the index of \(k\) ones. Then

\[\sum_{|\mathbf{k}| = k} \mu^{d(\mathbf{k}) - 1} C_n^{(\mathbf{k}, g, (\beta, \gamma))} = B_n^{((k), g, (\beta + \mu\gamma, \beta))} = C_n^{(\{1\}^k, g, (\beta, \beta + \mu\gamma))},\]

where the sum runs over all compositions \(\mathbf{k}\) of \(k\), that is, all tuples of positive integers with sum \(k\).

public theorem_wanted generalizedPolyBernoulliC_sum_formula (D : LandenData)
    (β γ : Fin D.s → ℝ) (μ : ℝ) (k n : ℕ) (hk : 0 < k) :
    ∑ c : Composition k, μ ^ (c.length - 1) * generalizedPolyBernoulliC D β γ c.blocks n =
        generalizedPolyBernoulliB D (β + μ • γ) β [k] n ∧
      generalizedPolyBernoulliB D (β + μ • γ) β [k] n =
        generalizedPolyBernoulliC D β (β + μ • γ) (List.replicate k 1) n

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Proposition 2, Identity (16).

Uses 3

Statement usesLanden data · Generalized poly-Bernoulli numbers of the second kind · Generalized poly-Bernoulli numbers of the first kind

TheoremSum formula for generalized poly-Bernoulli numbers \(B_n\)#●ready to prove

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data, let \(\beta, \gamma \in \mathbb{R}^s\), let \(\mu\) be a real number, and let \(k \ge 1\) and \(n \ge 0\) be integers. Write \(B_n\) and \(C_n\) for Kamano's generalized poly-Bernoulli numbers of the second and first kind, \(d(\mathbf{k})\) for the number of entries of an index \(\mathbf{k}\), and \(\{1\}^k = (1, \dots, 1)\) for the index of \(k\) ones. Then

\[\sum_{|\mathbf{k}| = k} \mu^{d(\mathbf{k}) - 1} B_n^{(\mathbf{k}, g, (\beta, \gamma))} = B_n^{((k), g, (\beta + \mu\gamma, \gamma))} = C_n^{(\{1\}^k, g, (\gamma, \beta + \mu\gamma))},\]

where the sum runs over all compositions \(\mathbf{k}\) of \(k\), that is, all tuples of positive integers with sum \(k\).

public theorem_wanted generalizedPolyBernoulliB_sum_formula (D : LandenData)
    (β γ : Fin D.s → ℝ) (μ : ℝ) (k n : ℕ) (hk : 0 < k) :
    ∑ c : Composition k, μ ^ (c.length - 1) * generalizedPolyBernoulliB D β γ c.blocks n =
        generalizedPolyBernoulliB D (β + μ • γ) γ [k] n ∧
      generalizedPolyBernoulliB D (β + μ • γ) γ [k] n =
        generalizedPolyBernoulliC D γ (β + μ • γ) (List.replicate k 1) n

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Proposition 2, Identity (17).

Uses 3

Statement usesLanden data · Generalized poly-Bernoulli numbers of the second kind · Generalized poly-Bernoulli numbers of the first kind

TheoremLanden formula for generalized poly-Bernoulli numbers \(C_n\)#●ready to prove

Let \(g = (g_0, g_1, \dots, g_s)\) be Landen data whose matrices \(g_1, \dots, g_s\) are invertible, where \((c_0, d_0)\) is the bottom row of \(g_0\). Let \(\tilde g\) be the transformed data: \(\tilde g_0\) has rows \((1, -1)\) and \((-d_0, -c_0)\), and \(\tilde g_i = h g_i\) for \(1 \le i \le s\), where \(h\) is the matrix with rows \((1, 0)\) and \((c_0 - d_0, -1)\). Let \(\beta, \gamma \in \mathbb{R}^s\), let \(k\) be a composition of a natural number \(m\) (the empty index when \(m = 0\)), and write \(k\uparrow\) for \(k\) with its last entry increased by \(1\) (\(k\uparrow\) is empty when \(k\) is). Let \(z(t) \in \mathbb{R}[[t]]\), the variable of \(g\), be the power series of \((e^t - 1)/(c_0 e^t + d_0)\) (the zero series when \(c_0 + d_0 = 0\)). Then for every \(n \ge 0\),

\[C_n^{(k, g, (\beta, \gamma))} = (-1)^{n+1} \, n! \, [t^n] \, \frac{d}{dt} \mathrm{Li}_{k\uparrow}(\tilde g; (\beta, \gamma); z(t)),\]

where \(C_n\) is the generalized poly-Bernoulli number of the first kind, \(\mathrm{Li}\) is Kamano's generalized multiple polylogarithm and \([t^n] F\) is the coefficient of \(t^n\) in \(F\). Here \(\tilde g\) is evaluated at the variable \(z(t)\) of \(g\), not at its own variable.

This is Theorem 5 in the reading its proof establishes: the proof differentiates \(\mathrm{Li}_{k\uparrow}(g; z(t)) = \mathrm{Li}_{k\uparrow}(\tilde g; z(-t))\). The paper's sign \((-1)^{n-1}\) equals \((-1)^{n+1}\) for all \(n \ge 0\).

As printed, with \(C_n^{(k, \tilde g, (\beta, \gamma))}\) formed from the variable \((e^t - 1)/(-d_0 e^t - c_0) = z(-t)\) of \(\tilde g\), the theorem is false: then \(C_n^{(k, \tilde g, (\beta, \gamma))} = C_n^{(k, g, (\beta, \gamma))}\) for all \(n\). For instance, \(s = 1\), \(g_0\) with rows \((1, -1)\) and \((1, 0)\), \(g_1\) the identity matrix, \(\beta = \gamma = (1)\), \(k = (1)\) and \(n = 0\) give \(C_0^{(k, g, (\beta, \gamma))} = C_0^{(k, \tilde g, (\beta, \gamma))} = 1\), while the printed identity asks for \(1 = -1\).

public theorem_wanted generalizedPolyBernoulliC_landen (D : LandenData)
    (hD : ∀ i, D.a i * D.d i - D.b i * D.c i ≠ 0) (β γ : Fin D.s → ℝ) {m : ℕ}
    (k : Composition m) (n : ℕ) :
    generalizedPolyBernoulliC D β γ k.blocks n =
      (-1 : ℝ) ^ (n + 1) * (n.factorial * coeff n (derivative (subst (landenExpVariable D)
        (generalizedMultiplePolylog D.tilde β γ (k.blocks.modifyLast (· + 1))))))

Sources

• Ken Kamano, A Generalization of the Landen Connection Formula and Generalized Poly-Bernoulli Numbers, INTEGERS 24 (2024), Article A77, Theorem 5.

Uses 5

Statement usesLanden data · Transformed Landen data · Kamano's generalized multiple polylogarithm · Generalized poly-Bernoulli numbers of the first kind · Landen exponential variable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.