Zagier numbers

DefinitionDomb-type sums#✓fully proved

For natural numbers \(n\), \(r\), \(s\) and \(t\), the Domb-type sum is the natural number

\[D(n, r, s, t) = \sum_{k=0}^{n} \binom{n}{k}^r \binom{2k}{k}^s \binom{2(n-k)}{n-k}^t.\]

The paper uses positive \(r\); the same finite formula is meaningful at \(r = 0\).

public def dombTypeSum (n r s t : ℕ) : ℕ :=
  ∑ k ∈ Finset.range (n + 1),
    n.choose k ^ r * (2 * k).choose k ^ s *
      (2 * (n - k)).choose (n - k) ^ t
Used by 4

DefinitionZagier numbers#✓fully proved

For a natural number \(n\), the Zagier number \(Z(n)\) is the Domb-type sum \(D(n, 1, 1, 1)\), that is,

\[Z(n) = \sum_{k=0}^{n} \binom{n}{k} \binom{2k}{k} \binom{2(n-k)}{n-k}.\]

These are the numbers of OEIS A081085.

public def zagierNumber (n : ℕ) : ℕ :=
  dombTypeSum n 1 1 1
Uses 1
Statement usesDomb-type sums
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.