Power sums and the determinant Schur specialization

Given a sequence t : ℕ → ℂ of prospective power sums, this module defines the complete homogeneous sequence newtonH t by the Newton recursion (n+1) · h (n+1) = ∑_{i ≤ n} t (i+1) · h (n−i), its integer-indexed extension newtonHZ (zero in negative degrees), and the Schur specialization

`schurDet t rows = det (newtonHZ t (rows i + j − i))`,

the Jacobi–Trudi determinant read as a definition. All Schur values in this development are these determinants; the link to the symmetric-group characters is the frobenius field of SchurPackage in Interfaces/SchurPackage.lean.

@[irreducible]

noncomputable def RS.newtonH (t : ℕ → ℂ) : ℕ → ℂ

The complete homogeneous sequence attached to a sequence of power sums, via the Newton recursion (n+1) · h (n+1) = ∑_{i ≤ n} t (i+1) · h (n−i); h 0 = 1.

Equations

• RS.newtonH t 0 = 1
• RS.newtonH t n.succ = (↑n + 1)⁻¹ * ∑ i ∈ Finset.range (n + 1), t (i + 1) * RS.newtonH t (n - i)

noncomputable def RS.newtonHZ (t : ℕ → ℂ) (n : ℤ) : ℂ

Integer-indexed extension of newtonH, vanishing in negative degrees — the form entering the Jacobi–Trudi determinant.

Equations

• RS.newtonHZ t n = if 0 ≤ n then RS.newtonH t n.toNat else 0

noncomputable def RS.schurDet (t : ℕ → ℂ) (rows : List ℕ) : ℂ

The Schur specialization of a row-length list rows, defined as the Jacobi–Trudi determinant det (h_{rows i − i + j})_{i,j}.

Equations

• RS.schurDet t rows = (Matrix.of fun (i j : Fin rows.length) => RS.newtonHZ t (↑(rows.get i) + ↑↑j - ↑↑i)).det

noncomputable def RS.diagramSchur (μ : YoungDiagram) (t : ℕ → ℂ) : ℂ

The Schur specialization of a Young diagram: schurDet on its row-length list.

Equations

• RS.diagramSchur μ t = RS.schurDet t μ.rowLens

@[simp]

theorem RS.newtonH_zero (t : ℕ → ℂ) : newtonH t 0 = 1

The complete homogeneous sequence starts at 1.

@[simp]

theorem RS.newtonHZ_natCast (t : ℕ → ℂ) (n : ℕ) : newtonHZ t ↑n = newtonH t n

Its integer extension agrees in non-negative degrees.

@[simp]

theorem RS.newtonHZ_neg (t : ℕ → ℂ) (n : ℤ) (hn : n < 0) : newtonHZ t n = 0

And vanishes in negative ones.