The binomial coefficients

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-02-16.
Last modified on 2024-10-16.

module elementary-number-theory.binomial-coefficients where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers

open import foundation.identity-types

open import univalent-combinatorics.standard-finite-types

Idea

The binomial coefficient (n choose k) measures how many decidable subsets of size k there are of a finite type of size n.

Definition

Binomial coefficients of natural numbers

binomial-coefficient-ℕ : ℕ → ℕ → ℕ
binomial-coefficient-ℕ zero-ℕ zero-ℕ = 1
binomial-coefficient-ℕ zero-ℕ (succ-ℕ k) = 0
binomial-coefficient-ℕ (succ-ℕ n) zero-ℕ = 1
binomial-coefficient-ℕ (succ-ℕ n) (succ-ℕ k) =
  (binomial-coefficient-ℕ n k) +ℕ (binomial-coefficient-ℕ n (succ-ℕ k))

Binomial coefficients indexed by elements of standard finite types

binomial-coefficient-Fin : (n : ℕ) → Fin (succ-ℕ n) → ℕ
binomial-coefficient-Fin n x = binomial-coefficient-ℕ n (nat-Fin (succ-ℕ n) x)

Properties

If k > n then binomial-coefficient-ℕ n k ＝ 0

is-zero-binomial-coefficient-ℕ :
  (n k : ℕ) → le-ℕ n k → is-zero-ℕ (binomial-coefficient-ℕ n k)
is-zero-binomial-coefficient-ℕ zero-ℕ (succ-ℕ k) _ = refl
is-zero-binomial-coefficient-ℕ (succ-ℕ n) (succ-ℕ k) H =
  ap-add-ℕ
    ( is-zero-binomial-coefficient-ℕ n k H)
    ( is-zero-binomial-coefficient-ℕ n (succ-ℕ k) (preserves-le-succ-ℕ n k H))

binomial-coefficient-ℕ n n ＝ 1

is-one-on-diagonal-binomial-coefficient-ℕ :
  (n : ℕ) → is-one-ℕ (binomial-coefficient-ℕ n n)
is-one-on-diagonal-binomial-coefficient-ℕ zero-ℕ = refl
is-one-on-diagonal-binomial-coefficient-ℕ (succ-ℕ n) =
  ap-add-ℕ
    ( is-one-on-diagonal-binomial-coefficient-ℕ n)
    ( is-zero-binomial-coefficient-ℕ n (succ-ℕ n) (succ-le-ℕ n))

See also

Recent changes