Subset-indexed elementary and complete homogeneous polynomials

For a subset A of the variables of MvPolynomial (Fin k) ℂ, the elementary symmetric polynomial eSub A r in the variables of A and the complete homogeneous polynomial hSub A m supported in A, with the add-one-variable recurrence for eSub — the engine of the e–h convolution and the bialternant Jacobi–Trudi identity. The hSub recurrence is proven in HInsert.lean.

noncomputable def RS.eSub {k : ℕ} (A : Finset (Fin k)) (r : ℕ) : MvPolynomial (Fin k) ℂ

The elementary symmetric polynomial in a subset of the variables.

Equations

• RS.eSub A r = (Multiset.map MvPolynomial.X A.val).esymm r

noncomputable def RS.hSub {k : ℕ} (A : Finset (Fin k)) (m : ℕ) : MvPolynomial (Fin k) ℂ

The complete homogeneous polynomial supported in a subset of the variables.

Equations

• RS.hSub A m = ∑ w : Sym (Fin k) m with ∀ i ∈ ↑w, i ∈ A, (Multiset.map MvPolynomial.X ↑w).prod

theorem RS.eSub_zero {k : ℕ} (A : Finset (Fin k)) : eSub A 0 = 1

The empty elementary symmetric polynomial is 1.

theorem RS.hSub_zero {k : ℕ} (A : Finset (Fin k)) : hSub A 0 = 1

And so is the degree-zero complete homogeneous one.

theorem RS.eSub_eq_zero_of_lt {k : ℕ} (A : Finset (Fin k)) (r : ℕ) (hr : A.card < r) : eSub A r = 0

Vanishing of eSub beyond the subset size.

theorem RS.eSub_insert {k : ℕ} {A : Finset (Fin k)} {j : Fin k} (hj : j ∉ A) (r : ℕ) : eSub (insert j A) (r + 1) = eSub A (r + 1) + MvPolynomial.X j * eSub A r

The add-one-variable recurrence for eSub.