Documentation

TauCeti.LinearAlgebra.Vandermonde

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_Icc_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 predecessor 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; the two facts hold in general because descPochhammer R j is the image of descPochhammer ℤ j under the unique ring homomorphism, and a monic polynomial stays monic of the same degree under any ring homomorphism to a nontrivial ring. The trivial ring is handled separately, where the identity is vacuous.

Main results #

The discrete antiderivative of a falling factorial #

source
theorem TauCeti.sum_Icc_descPochhammer_eval (m : ℕ) {p q : ℤ} (h : p ≤ q) :
(↑m + 1) * ∑ t ∈ Finset.Icc p (q - 1), Polynomial.eval t (descPochhammer ℤ m) = Polynomial.eval q (descPochhammer ℤ (m + 1)) - Polynomial.eval p (descPochhammer ℤ (m + 1))

The discrete antiderivative of a falling factorial. Summing the degree m falling factorial over the integer range p ≤ t < q gives the difference of the degree m + 1 falling factorial at the endpoints, divided by m + 1; the statement clears that denominator.

The hypothesis p ≤ q is what makes the range a range: for q < p the sum is empty while the right-hand side need not vanish.

The box-sum identity #

source
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 #

source
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).

source
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.