Signed counts of the permutations carrying one antitone sequence above another

Let β and η be antitone sequences indexed by Fin n with values in a preorder. Say that a permutation τ of Fin n dominates β by η when β j ≤ η (τ j) for every j. The signed count of the dominating permutations is 1 when the comparisons β j ≤ η i cut out exactly the initial segments i ≤ j, and 0 otherwise.

The signed count is the determinant of the 0/1 matrix of the comparisons β j ≤ η i. Because η decreases, each row of that matrix is the indicator of an initial segment of Fin n; because β decreases, those initial segments grow with the row. A chain of n nested initial segments of Fin n either repeats a term — and two rows coincide — or starts empty — and a row vanishes — or is the complete flag, in which case the matrix is lower triangular with unit diagonal.

The three cases are the cancellation behind the Pieri rule for Schur polynomials: adding a monomial to the beta-numbers of a shape and sorting the result back into decreasing order leaves exactly the shapes obtained by adding a horizontal strip, every other arrangement of the same values cancelling against the opposite one.

Main results

• TauCeti.sum_sign_filter_forall_le_of_antitone: the signed count of the permutations dominating one antitone sequence by another.

theorem TauCeti.sum_sign_filter_forall_le_of_antitone {n : ℕ} {α : Type u_1} [Preorder α] [DecidableLE α] {β η : Fin n → α} (hβ : Antitone β) (hη : Antitone η) : ∑ τ : Equiv.Perm (Fin n) with ∀ (j : Fin n), β j ≤ η (τ j), ↑(Equiv.Perm.sign τ) = if ∀ (i j : Fin n), β j ≤ η i ↔ i ≤ j then 1 else 0

The signed count of the permutations carrying β above η. For antitone β and η indexed by Fin n, the sum of the signs of the permutations τ with β j ≤ η (τ j) for every j is 1 when the comparisons β j ≤ η i hold exactly for i ≤ j, and 0 otherwise.