Singmaster's bound on binomial multiplicities

For a ≥ 2, the set of positions (n, k) with k ≤ n and C(n, k) = a is finite with at most 2 + 2 ⌊log₂ a⌋ elements (Singmaster, 1971). Positions with 2k ≤ n satisfy 2^k ≤ C(2k, k) ≤ C(n, k) = a, so 1 ≤ k ≤ log₂ a, and for fixed k ≥ 1 the map n ↦ C(n, k) is strictly increasing, so each such k gives at most one position; the positions with 2k > n inject into these by (n, k) ↦ (n, n - k). The proof gives 2 ⌊log₂ a⌋.

Main results

• Singmaster.ncard_choose_eq_le_two_mul_log: positions of a >= 2 in Pascal triangle: finite, at most 2 log2 a (sharpened)
• Singmaster.ncard_choose_eq_le: positions of a >= 2 in Pascal triangle: finite, at most 2 + 2 log2 a

References

• D. Singmaster, How often does an integer occur as a binomial coefficient?, Amer. Math. Monthly 78 (1971), 385–386.

theorem Singmaster.ncard_choose_eq_le_two_mul_log (a : ℕ) (ha : 2 ≤ a) : {p : ℕ × ℕ | p.2 ≤ p.1 ∧ p.1.choose p.2 = a}.Finite ∧ {p : ℕ × ℕ | p.2 ≤ p.1 ∧ p.1.choose p.2 = a}.ncard ≤ 2 * Nat.log 2 a

Singmaster's bound, sharpened. An integer a ≥ 2 occurs at most 2 ⌊log₂ a⌋ times in Pascal's triangle (Singmaster 1971 states 2 + 2 log₂ a): the positions (n, k) with k ≤ n and C(n, k) = a form a finite set with at most that many elements.

theorem Singmaster.ncard_choose_eq_le (a : ℕ) (ha : 2 ≤ a) : {p : ℕ × ℕ | p.2 ≤ p.1 ∧ p.1.choose p.2 = a}.Finite ∧ {p : ℕ × ℕ | p.2 ≤ p.1 ∧ p.1.choose p.2 = a}.ncard ≤ 2 + 2 * Nat.log 2 a

Singmaster's bound (1971). An integer a ≥ 2 occurs at most 2 + 2 ⌊log₂ a⌋ times in Pascal's triangle (the form stated by Singmaster; see ncard_choose_eq_le_two_mul_log).