Coefficients against the staircase alternant

Multiplying by the zero-shape alternant det (powMat 0) = a_δ shifts coefficient extraction by the permuted staircase: the coefficient of w₀ in P · a_δ is the signed sum over permutations of the guarded shifted coefficients of P.

noncomputable def RS.stairShift {k : ℕ} (τ : Equiv.Perm (Fin k)) : Fin k →₀ ℕ

The permuted staircase exponent.

Equations

• RS.stairShift τ = ∑ i : Fin k, Finsupp.single i (k - 1 - ↑(τ i))

theorem RS.stairShift_apply {k : ℕ} (τ : Equiv.Perm (Fin k)) (j : Fin k) : (stairShift τ) j = k - 1 - ↑(τ j)

The staircase shift at a row, under a permutation.

theorem RS.coeff_mul_alternant {k : ℕ} (P : MvPolynomial (Fin k) ℂ) (w₀ : Fin k →₀ ℕ) : (P * (powMat fun (x : Fin k) => 0).det).coeff w₀ = ∑ τ : Equiv.Perm (Fin k), ↑↑(Equiv.Perm.sign τ) * if stairShift τ ≤ w₀ then P.coeff (w₀ - stairShift τ) else 0

Coefficient extraction against the staircase alternant.