Vandermonde determinants in the falling-factorial basis

The falling factorials descPochhammer R j are monic of degree j, so Mathlib's Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde rewrites det (vandermonde y) as the determinant of the matrix (descPochhammer R j).eval (yᵢ). Unlike the powers, the falling factorials have a closed-form discrete antiderivative and a closed-form left shift, and this file proves the two identities for the Vandermonde determinant that those two facts supply.

The box-sum identity

Let x₀ ≤ x₁ ≤ ⋯ ≤ xₙ be integers and let y range over the box of integer vectors with xᵢ ≤ yᵢ ≤ xᵢ₊₁ - 1, one interval for each consecutive pair. Then

n ! · ∑ y, det (vandermonde y) = det (vandermonde x),

which is TauCeti.factorial_mul_sum_det_vandermonde. Unwinding the determinants, the product ∏_{i < j} (yⱼ - yᵢ) of the differences of an n-tuple, summed over the box, is 1 / n ! times the corresponding product for the (n + 1)-tuple that bounds it.

The identity drives the branching recursion for the Weyl dimension formula of GL n: the interlacing condition indexing the constituents of an irreducible restricted to GL (n - 1) is exactly such a box, and the two Vandermonde products are the two Weyl dimension numerators.

Three moves prove it; only the last uses the ordering hypothesis. The falling-factorial basis replaces the powers, because they have the closed-form discrete antiderivative TauCeti.sum_Ico_descPochhammer_eval. Multilinearity: a determinant is multilinear in its rows and the box constrains the rows independently, so the sum of the determinants over the box is the determinant of the matrix of row sums (MultilinearMap.map_sum_finset); evaluating those row sums, and clearing the denominators 1, 2, …, n by a column scaling, produces the matrix of differences (descPochhammer ℤ (j+1)).eval (xᵢ₊₁) - (descPochhammer ℤ (j+1)).eval (xᵢ), whose determinant is n ! times the sum. A row reduction: that matrix of differences is what remains of the (n+1) × (n+1) matrix (descPochhammer ℤ j).eval (xᵢ) after subtracting each row from its successor and deleting the column j = 0, which is constant equal to 1. Multiplying on the left by the bidiagonal matrix performing the subtraction contributes a factor (-1)^{n+1} to the determinant, and expanding the product along its first column — where only the last entry survives — contributes the same sign, so the two determinants agree.

The lowering identity

Over an arbitrary commutative ring, lower a single node yᵢ by one and weight the resulting Vandermonde determinant by yᵢ. Summing over the nodes gives back the original determinant, scaled by ∑ yᵢ - (0 + 1 + ⋯ + (m - 1)):

∑ i, yᵢ · det (vandermonde (update y i (yᵢ - 1))) = (∑ i, yᵢ - ∑ i, i) · det (vandermonde y),

which is TauCeti.sum_mul_det_vandermonde_update_sub_one, with TauCeti.sum_mul_prod_sub_update_sub_one its unwound form as a product of differences over the ordered pairs of an initial segment of ℕ. It is the Vandermonde identity behind the Frobenius determinant formula for the number of standard Young tableaux of a given shape, where the nodes are the beta-numbers of a Young diagram and lowering one of them is erasing a corner.

Two moves prove it. The left shift: x · (x - 1)^{underline j} = x^{underline (j+1)}, so multiplying the lowered row by yᵢ turns the falling-factorial matrix of the lowered node vector into the same matrix with its i-th row shifted up one degree, and x^{underline (j+1)} = x^{underline j} · (x - j) expands that row as yᵢ times the original minus j times the original, entry by entry. Jacobi's row formula Matrix.sum_det_updateRow_mul_row: summing over the rows the determinant of a matrix with one row scaled entry by entry multiplies the determinant by the total of the scaling factors, which turns the j-weighted correction into (0 + 1 + ⋯ + (m - 1)) · det.

Mathlib's monic_descPochhammer and descPochhammer_natDegree assume the coefficient ring is a nontrivial ring without zero divisors, which the lowering identity does not; it uses TauCeti.monic_descPochhammer, which holds over any ring, and TauCeti.descPochhammer_natDegree, which holds over any nontrivial ring. The trivial ring is handled separately, where the identity is vacuous.

Integrality of weighted Vandermonde products

Weight the rows of a Vandermonde determinant by wᵢ. If p j is monic of degree j, the column of u^j may be replaced by the column of the values of p j without changing the determinant, so if d j divides every weighted value wᵢ · (p j).eval (uᵢ) then ∏ⱼ d j divides ∏ᵢ wᵢ · det (vandermonde u) (TauCeti.prod_dvd_prod_mul_det_vandermonde). With p j the falling factorial and w = 1 this is the argument of Mathlib's Matrix.superFactorial_dvd_vandermonde_det. Three products arise as numerators of Weyl dimension formulas. The first two are divisible by 1! · 3! ⋯ (2n - 1)!:

• the odd Vandermonde product ∏ᵢ xᵢ · ∏_{i < j} (xᵢ² - xⱼ²), the numerator for the symplectic groups, with the monic odd polynomials x (x² - 1²) ⋯ (x² - k²), each of which is the falling factorial of degree 2k + 1 at x + k (TauCeti.mul_prod_sq_sub_sq_eq_descPochhammer_eval);
• the product ∏ᵢ (2xᵢ + 1) · ∏_{i < j} (xᵢ - xⱼ)(xᵢ + xⱼ + 1) of the differences of the values x (x + 1), the numerator for the odd orthogonal groups, with the polynomials ∏_{c < k} (x - c)(x + c + 1), whose weighted values are sums of two falling factorials of degree 2k + 1 (TauCeti.two_mul_add_one_mul_prod_sub_mul_add_add_one_eq).

The third, the unweighted product ∏_{i < j} (xᵢ² - xⱼ²), the numerator for the even orthogonal groups, is divisible by 2!/2 · 4!/2 ⋯ (2n - 2)!/2, with the monic even polynomials (x² - 0²) ⋯ (x² - k²), twice each of which is a sum of two falling factorials of degree 2k + 2 (TauCeti.two_mul_prod_sq_sub_sq_eq).

Main results

• TauCeti.factorial_mul_sum_det_vandermonde: the box-sum identity for Vandermonde determinants.
• TauCeti.sum_mul_det_vandermonde_update_sub_one and TauCeti.sum_mul_prod_sub_update_sub_one: the lowering identity for Vandermonde determinants.
• TauCeti.prod_dvd_prod_mul_det_vandermonde and TauCeti.prod_dvd_prod_mul_prod_sub: integrality for weighted Vandermonde products.
• TauCeti.prod_factorial_dvd_prod_mul_det_vandermonde_sq and TauCeti.prod_factorial_dvd_prod_mul_prod_sq_sub_sq: integrality for the odd Vandermonde product ∏ᵢ xᵢ · ∏_{i < j} (xⱼ² - xᵢ²), which is divisible by 1! · 3! ⋯ (2n - 1)!, a positive integer (TauCeti.prod_factorial_two_mul_add_one_pos).
• TauCeti.prod_factorial_dvd_prod_two_mul_add_one_mul_prod_sub_mul_add_add_one: integrality for the Vandermonde product of the values x (x + 1) weighted by 2x + 1, which is divisible by 1! · 3! ⋯ (2n - 1)! too.
• TauCeti.prod_add_one_mul_factorial_dvd_prod_prod_sq_sub_sq: integrality for the even Vandermonde product ∏_{i < j} (xᵢ² - xⱼ²), which is divisible by 2!/2 · 4!/2 ⋯ (2n - 2)!/2, a positive integer (TauCeti.prod_add_one_mul_factorial_two_mul_add_one_pos), the value of the product at the nodes n - 1, …, 1, 0 (TauCeti.prod_prod_sq_sub_sq_eq_prod_add_one_mul_factorial).

The box-sum identity

theorem TauCeti.factorial_mul_sum_det_vandermonde {n : ℕ} (x : Fin (n + 1) → ℤ) (hx : ∀ (i : Fin n), x i.castSucc ≤ x i.succ) : ↑n.factorial * ∑ y ∈ Finset.Icc (fun (i : Fin n) => x i.castSucc) fun (i : Fin n) => x i.succ - 1, (Matrix.vandermonde y).det = (Matrix.vandermonde x).det

Summing Vandermonde determinants over a box of nested intervals. For integers x₀ ≤ x₁ ≤ ⋯ ≤ xₙ, the Vandermonde determinant of y, summed over all integer vectors with xᵢ ≤ yᵢ ≤ xᵢ₊₁ - 1, is the Vandermonde determinant of x divided by n !; the statement clears that denominator, so it is an identity over ℤ.

The hypothesis is exactly what makes each interval a range of summation; the nodes are otherwise arbitrary integers, of either sign.

The lowering identity

theorem TauCeti.sum_mul_det_vandermonde_update_sub_one {R : Type u_1} [CommRing R] {m : ℕ} (y : Fin m → R) : ∑ i : Fin m, y i * (Matrix.vandermonde (Function.update y i (y i - 1))).det = (∑ i : Fin m, y i - ∑ i : Fin m, ↑↑i) * (Matrix.vandermonde y).det

The lowering identity for Vandermonde determinants. Lowering a single node by one and weighting by that node, then summing over the nodes, multiplies the Vandermonde determinant by the total of the nodes less 0 + 1 + ⋯ + (m - 1).

theorem TauCeti.sum_mul_prod_sub_update_sub_one {R : Type u_1} [CommRing R] (m : ℕ) (b : ℕ → R) : ∑ i ∈ Finset.range m, b i * ∏ k ∈ Finset.range m, ∏ l ∈ Finset.Ico (k + 1) m, (Function.update b i (b i - 1) k - Function.update b i (b i - 1) l) = (∑ i ∈ Finset.range m, b i - ∑ i ∈ Finset.range m, ↑i) * ∏ k ∈ Finset.range m, ∏ l ∈ Finset.Ico (k + 1) m, (b k - b l)

The lowering identity, unwound. For a sequence in a commutative ring, the product of the differences over the ordered pairs below a bound, with one term of the sequence lowered by one and the result weighted by that term, summed over the terms below the bound, is the total of the terms below the bound less 0 + 1 + ⋯ + (m - 1), times the product of the differences of the original sequence.

Integrality of weighted Vandermonde determinants

theorem TauCeti.prod_dvd_prod_mul_det_vandermonde {R : Type u_1} [CommRing R] {n : ℕ} (u w d : Fin n → R) (p : Fin n → Polynomial R) (hdeg : ∀ (j : Fin n), (p j).natDegree = ↑j) (hmonic : ∀ (j : Fin n), (p j).Monic) (hdvd : ∀ (i j : Fin n), d j ∣ w i * Polynomial.eval (u i) (p j)) : ∏ j : Fin n, d j ∣ (∏ i : Fin n, w i) * (Matrix.vandermonde u).det

Integrality for a weighted Vandermonde determinant. Let p j be monic of degree j and suppose that d j divides the weighted value w i * (p j).eval (u i) at every node. Then ∏ j, d j divides ∏ i, w i * det (vandermonde u): replacing the column of u^j by that of the values of p j does not change the determinant, after which column j of the weighted matrix is a multiple of d j. With p j the falling factorial and w = 1 this is the argument of Mathlib's Matrix.superFactorial_dvd_vandermonde_det.

theorem TauCeti.prod_dvd_prod_mul_prod_sub {R : Type u_1} [CommRing R] (m : ℕ) (u w d : ℕ → R) (p : ℕ → Polynomial R) (hdeg : ∀ j < m, (p j).natDegree = j) (hmonic : ∀ j < m, (p j).Monic) (hdvd : ∀ i < m, ∀ j < m, d j ∣ w i * Polynomial.eval (u i) (p j)) : ∏ k ∈ Finset.range m, d k ∣ ∏ k ∈ Finset.range m, w k * ∏ l ∈ Finset.Ico (k + 1) m, (u k - u l)

Integrality for a weighted Vandermonde product. For sequences of nodes uₖ and weights wₖ, if p j is monic of degree j for j < m and d j divides wᵢ * (p j).eval (uᵢ) for i, j < m, then ∏_{k < m} d k divides ∏_{k < m} wₖ · ∏_{k < l < m} (uₖ - uₗ). This is TauCeti.prod_dvd_prod_mul_det_vandermonde with the determinant expanded; the sign relating the two orders of the differences does not affect divisibility.

Products of squared differences, weighted by the nodes

theorem TauCeti.prod_factorial_two_mul_add_one_pos (n : ℕ) : 0 < ∏ k ∈ Finset.range n, ↑(2 * k + 1).factorial

The divisor 1! · 3! ⋯ (2n - 1)! of the odd Vandermonde product is positive, so it may be cancelled.

theorem TauCeti.prod_factorial_dvd_prod_mul_det_vandermonde_sq {n : ℕ} (x : Fin n → ℤ) : ∏ k ∈ Finset.range n, ↑(2 * k + 1).factorial ∣ (∏ i : Fin n, x i) * (Matrix.vandermonde fun (i : Fin n) => x i ^ 2).det

Integrality for the odd Vandermonde product. For integer nodes xᵢ, the product ∏ᵢ xᵢ · det (vandermonde (xᵢ²)) = ∏ᵢ xᵢ · ∏_{i < j} (xⱼ² - xᵢ²) is divisible by 1! · 3! ⋯ (2n - 1)!. This is the analogue, for the odd powers x, x³, …, x^{2n-1}, of Mathlib's Matrix.superFactorial_dvd_vandermonde_det for the powers 1, x, …, x^{n-1}.

theorem TauCeti.prod_factorial_dvd_prod_mul_prod_sq_sub_sq (m : ℕ) (b : ℕ → ℤ) : ∏ k ∈ Finset.range m, ↑(2 * k + 1).factorial ∣ ∏ k ∈ Finset.range m, b k * ∏ l ∈ Finset.Ico (k + 1) m, (b k ^ 2 - b l ^ 2)

Integrality for the odd Vandermonde product, unwound. For a sequence of integers, the product ∏_{k < m} bₖ · ∏_{k < l < m} (bₖ² - bₗ²) is divisible by 1! · 3! ⋯ (2m - 1)!. This is TauCeti.prod_factorial_dvd_prod_mul_det_vandermonde_sq with the determinant expanded.

theorem TauCeti.prod_add_one_mul_factorial_two_mul_add_one_pos (m : ℕ) : 0 < ∏ k ∈ Finset.range m, (↑k + 1) * ↑(2 * k + 1).factorial

The divisor 2!/2 · 4!/2 ⋯ (2m)!/2 of the even Vandermonde product is positive, so it may be cancelled.

theorem TauCeti.prod_prod_sq_sub_sq_eq_prod_add_one_mul_factorial {R : Type u_1} [CommRing R] (m : ℕ) : ∏ j ∈ Finset.range m, ∏ c ∈ Finset.range j, (↑j ^ 2 - ↑c ^ 2) = ∏ k ∈ Finset.range (m - 1), (↑k + 1) * ↑(2 * k + 1).factorial

The products ∏_{c < j} (j² - c²) for j < m, the rows of the even Vandermonde product at the nodes m - 1, …, 1, 0, multiply to 2!/2 · 4!/2 ⋯ (2m - 2)!/2: the row j = k + 1 is (k + 1) (2k + 1)! (TauCeti.prod_sq_sub_sq_eq_mul_factorial) and the row j = 0 is empty.

theorem TauCeti.prod_add_one_mul_factorial_dvd_prod_prod_sq_sub_sq (m : ℕ) (b : ℕ → ℤ) : ∏ k ∈ Finset.range (m - 1), (↑k + 1) * ↑(2 * k + 1).factorial ∣ ∏ k ∈ Finset.range m, ∏ l ∈ Finset.Ico (k + 1) m, (b k ^ 2 - b l ^ 2)

Integrality for the even Vandermonde product. For a sequence of integers, the product ∏_{k < l < m} (bₖ² - bₗ²) is divisible by ∏_{k < m - 1} (k + 1) (2k + 1)!, that is, by 2!/2 · 4!/2 ⋯ (2m - 2)!/2. In the Vandermonde determinant of the squares, the column of (x²)^j may be replaced by the column of ∏_{c < j} (x² - c²), whose values at the integers are multiples of its value ∏_{c < j} (j² - c²) at x = j (TauCeti.mul_factorial_dvd_prod_sq_sub_sq).

The Vandermonde product of x (x + 1), weighted by 2x + 1

theorem TauCeti.prod_factorial_dvd_prod_two_mul_add_one_mul_prod_sub_mul_add_add_one (m : ℕ) (b : ℕ → ℤ) : ∏ k ∈ Finset.range m, ↑(2 * k + 1).factorial ∣ ∏ k ∈ Finset.range m, (2 * b k + 1) * ∏ l ∈ Finset.Ico (k + 1) m, (b k - b l) * (b k + b l + 1)

Integrality for the Vandermonde product of the values x (x + 1). For a sequence of integers, the product ∏_{k < m} (2bₖ + 1) · ∏_{k < l < m} (bₖ - bₗ) (bₖ + bₗ + 1) is divisible by 1! · 3! ⋯ (2m - 1)!. The factors are the differences bₖ (bₖ + 1) - bₗ (bₗ + 1), so in the Vandermonde determinant of the nodes x (x + 1), weighted by 2x + 1, the column of (x (x + 1))^j may be replaced by the column of ∏_{c < j} (x - c) (x + c + 1), whose weighted values are multiples of (2j + 1)! (TauCeti.factorial_dvd_two_mul_add_one_mul_prod_sub_mul_add_add_one).