Integer-indexed complete homogeneous polynomials

The ℤ-indexed extension of hSub, vanishing in negative degrees, and the guarded range-k form of the resolvent — the entry form of the bialternant matrices.

noncomputable def RS.hSubZ {k : ℕ} (A : Finset (Fin k)) (d : ℤ) : MvPolynomial (Fin k) ℂ

The ℤ-indexed extension of hSub, vanishing in negative degrees.

Equations

• RS.hSubZ A d = if 0 ≤ d then RS.hSub A d.toNat else 0

@[simp]

theorem RS.hSubZ_natCast {k : ℕ} (A : Finset (Fin k)) (m : ℕ) : hSubZ A ↑m = hSub A m

The integer extension agrees in non-negative degrees.

@[simp]

theorem RS.hSubZ_neg {k : ℕ} (A : Finset (Fin k)) (d : ℤ) (hd : d < 0) : hSubZ A d = 0

And vanishes in negative ones.

theorem RS.sum_fin_resolvent {k : ℕ} (hrec : HSubRec k) {A : Finset (Fin k)} {j : Fin k} (hj : j ∉ A) (hcard : A.card + 1 = k) (m : ℕ) : ∑ r : Fin k, (-1) ^ ↑r * (eSub A ↑r * hSubZ (insert j A) (↑m - ↑↑r)) = MvPolynomial.X j ^ m

The resolvent in guarded range-k form: for j ∉ A with insert j A filling all k variables, the r-sum over Fin k computes X j ^ m for every m.