Domb numbers
DefinitionDomb numbers#✓fully proved
MetaMathlibExt.dombNumber
For a natural number \(n\), the Domb number \(\mathrm{Domb}(n)\) is the Domb-type sum \(D(n,2,1,1)\), that is, \(\mathrm{Domb}(n) = \sum_{k=0}^{n} \binom{n}{k}^2 \binom{2k}{k} \binom{2(n-k)}{n-k}\) (OEIS A002895).
public def dombNumber (n : ℕ) : ℕ :=
dombTypeSum n 2 1 1public 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) ^ tMathlibExt/Combinatorics/Enumerative/ZagierNumber.lean:30
Uses 1 · Used by 1
Statement usesDomb-type sums
TheoremExplicit formula for the Domb numbers#✓fully proved
MetaMathlibExt.dombNumber_unfold
For every natural number \(n\), the Domb number \(\mathrm{Domb}(n)\) equals \(\sum_{k=0}^{n} \binom{n}{k}^2 \binom{2k}{k} \binom{2(n-k)}{n-k}\).
public theorem dombNumber_unfold (n : ℕ) :
dombNumber n =
∑ k ∈ Finset.range (n + 1),
n.choose k ^ 2 * (2 * k).choose k * (2 * (n - k)).choose (n - k)public def dombNumber (n : ℕ) : ℕ :=
dombTypeSum n 2 1 1MathlibExt/Combinatorics/Enumerative/DombNumber.lean:33
Uses 2
Statement usesDomb numbers
Proof usesDomb-type sums
2 fully proved
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.