The binomial coefficients

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 Fin n there are of size k.

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) star = 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))