Pieri chain: positivity of alternant coefficients along diagram chains

The staircase exponent vector eVec, and the positivity of the coefficient of the target monomial in p₁ʳ · a_{eVec λ} when μ extends λ by r cells.

noncomputable def RS.eVec (nu : YoungDiagram) (k : ℕ) : Fin k → ℕ

The staircase exponent vector of a diagram in k variables.

Equations

• RS.eVec nu k i = nu.rowLen ↑i + (k - 1 - ↑i)

theorem RS.eVec_strict (nu : YoungDiagram) (k : ℕ) (i j : Fin k) : i < j → eVec nu k j < eVec nu k i

The staircase exponent vector is strictly decreasing.

theorem RS.coeff_pow_p1_altDet_natCast {k : ℕ} (r : ℕ) (w : Fin k → ℕ) (hw : ∀ (i j : Fin k), i < j → w j < w i) (e : Fin k → ℕ) : (∀ (i j : Fin k), i < j → e j < e i) → ∃ (N : ℕ), ((∑ l : Fin k, MvPolynomial.X l) ^ r * altDet e).coeff (∑ i : Fin k, Finsupp.single i (w i)) = ↑N

Coefficients of a power of the first power sum against an alternant are natural numbers: no cancellation into negatives.

theorem RS.coeff_chain_pos {k : ℕ} (lam mu : YoungDiagram) (hle : lam ≤ mu) (r : ℕ) (hcard : mu.card = lam.card + r) (hk : mu.colLen 0 ≤ k) : ∃ (N : ℕ), 0 < N ∧ ((∑ l : Fin k, MvPolynomial.X l) ^ r * altDet (eVec lam k)).coeff (∑ i : Fin k, Finsupp.single i (eVec mu k i)) = ↑N

Positivity along a chain: when one diagram extends another by r cells, the target monomial's coefficient is a positive natural number.