The Vandermonde coefficient formula

Lemma 3.1 of Alon-Nathanson-Ruzsa: a closed form for the coefficient of ∏ i, X i ^ c i in (X 0 + ⋯ + X k) ^ m * ∏_{i > j} (X i - X j), culminating in Vandermonde_coefficient_formula.

def fallingFactorial (s r : ℕ) : ℕ

Falling factorial (s)_r = s(s-1)...(s-r + 1)

Equations

• fallingFactorial s r = if r = 0 then 1 else ∏ i ∈ Finset.range r, (s - i)

def vandermondeMatrix {k : ℕ} (c : Fin (k + 1) → ℕ) : Matrix (Fin (k + 1)) (Fin (k + 1)) ℚ

Vandermonde matrix (c^j)

Equations

• vandermondeMatrix c = Matrix.of fun (i j : Fin (k + 1)) => ↑(c i) ^ ↑j

def fallingFactorialMatrix {k : ℕ} (c : Fin (k + 1) → ℕ) : Matrix (Fin (k + 1)) (Fin (k + 1)) ℚ

Falling factorial matrix ((c)_j)

Equations

• fallingFactorialMatrix c = Matrix.of fun (i j : Fin (k + 1)) => ↑(fallingFactorial (c i) ↑j)

def expectedValue {k : ℕ} (c : Fin (k + 1) → ℕ) (m : ℕ) : ℚ

Expected value: m! / (∏ c!) * ∏_{i>j} (c - c)

Equations

• expectedValue c m = (↑m.factorial * ∏ i : Fin (k + 1), ∏ j : Fin (k + 1), if ↑j < ↑i then ↑(c i) - ↑(c j) else 1) / ∏ i : Fin (k + 1), ↑(c i).factorial

def toFinsupp {k : ℕ} (c : Fin (k + 1) → ℕ) : Fin (k + 1) →₀ ℕ

Convert a function c : Fin (k + 1) → ℕ to Finsupp

Equations

• toFinsupp c = { support := {i : Fin (k + 1) | c i ≠ 0}, toFun := c, mem_support_toFun := ⋯ }

theorem det_fallingFactorial_eq_det_vandermonde {k : ℕ} (c : Fin (k + 1) → ℕ) : (fallingFactorialMatrix c).det = (vandermondeMatrix c).det

theorem fallingFactorial_eq_factorial_div (n k : ℕ) : fallingFactorial n k = if k ≤ n then n.factorial / (n - k).factorial else 0

def symmetricSumFixed {k : ℕ} (c : Fin (k + 1) → ℕ) (m : ℕ) : ℚ

Symmetric group sum expression C = ∑{σ∈S{k + 1}} (-1)^{sign(σ)} * m! / ∏ᵢ (cᵢ - σ(i))! Corrected to use proper sign and handle 0 case.

Equations

• One or more equations did not get rendered due to their size.

theorem symmetricSumFixed_eq_expectedValue {k : ℕ} (c : Fin (k + 1) → ℕ) (m : ℕ) : symmetricSumFixed c m = expectedValue c m

theorem coeff_term {k : ℕ} (c : Fin (k + 1) → ℕ) (m : ℕ) (σ : Equiv.Perm (Fin (k + 1))) (h_sum : ∑ i : Fin (k + 1), c i = m + (k + 1).choose 2) : MvPolynomial.coeff (toFinsupp c) ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * ∏ i : Fin (k + 1), MvPolynomial.X i ^ ↑(σ i)) = if ∀ (i : Fin (k + 1)), ↑(σ i) ≤ c i then ↑m.factorial / ∏ i : Fin (k + 1), ↑(c i - ↑(σ i)).factorial else 0

theorem Vandermonde_coefficient_formula {k : ℕ} (c : Fin (k + 1) → ℕ) (m : ℕ) (h_sum : ∑ i : Fin (k + 1), c i = m + (k + 1).choose 2) : MvPolynomial.coeff (toFinsupp c) ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * ∏ i : Fin (k + 1), ∏ j : Fin (k + 1), if j < i then MvPolynomial.X i - MvPolynomial.X j else 1) = expectedValue c m