The delta power-sum sequence

At the sequence t₀ = (1, 0, 0, …) the completed cycle weight is the identity indicator and the complete homogeneous values are inverse factorials; the Frobenius formula then evaluates the Jacobi–Trudi character degree as n! times the Jacobi–Trudi determinant at t₀.

noncomputable def RS.deltaSeq : ℕ → ℂ

The delta power-sum sequence.

Equations

• RS.deltaSeq c = if c = 1 then 1 else 0

@[simp]

theorem RS.deltaSeq_one : deltaSeq 1 = 1

The delta sequence's first value is 1.

theorem RS.newtonH_deltaSeq (d : ℕ) : newtonH deltaSeq d = (↑d.factorial)⁻¹

Complete homogeneous values of the delta sequence are inverse factorials.

theorem RS.cycleProd_deltaSeq {n : ℕ} (π : Equiv.Perm (Fin n)) : cycleProd deltaSeq π = if π = 1 then 1 else 0

The completed cycle weight of the delta sequence is the identity indicator.

theorem RS.jtChar_one_eq (μ : YoungDiagram) : jtChar μ 1 = ↑μ.card.factorial * diagramSchur μ deltaSeq

The degree evaluation: the Jacobi–Trudi character degree is n! times the Jacobi–Trudi determinant at the delta sequence.