The e–h convolution and the single-variable resolvent

Over any variable subset A, the alternating e–h convolution vanishes in positive degree, and the mixed convolution with one extra variable j telescopes to X j ^ m — the entrywise content of the bialternant matrix factorization. The hSub add-one-variable recurrence enters as the hypothesis HSubRec, discharged in HInsert.lean.

@[reducible, inline]

abbrev RS.HSubRec (k : ℕ) : Prop

The hSub add-one-variable recurrence, as a hypothesis.

Equations

• RS.HSubRec k = ∀ {A : Finset (Fin k)} {j : Fin k}, j ∉ A → ∀ (m : ℕ), RS.hSub (insert j A) (m + 1) = RS.hSub A (m + 1) + MvPolynomial.X j * RS.hSub (insert j A) m

theorem RS.hSub_empty {k : ℕ} (m : ℕ) : hSub ∅ (m + 1) = 0

Positive-degree hSub of the empty subset vanishes.

noncomputable def RS.fmix {k : ℕ} (A : Finset (Fin k)) (j : Fin k) (M : ℕ) : MvPolynomial (Fin k) ℂ

The mixed e–h convolution with one extra variable.

Equations

• RS.fmix A j M = ∑ r ∈ Finset.range (M + 1), (-1) ^ r * (RS.eSub A r * RS.hSub (insert j A) (M - r))

theorem RS.conv_eq_zero {k : ℕ} (hrec : HSubRec k) (A : Finset (Fin k)) (m : ℕ) : ∑ r ∈ Finset.range (m + 2), (-1) ^ r * (eSub A r * hSub A (m + 1 - r)) = 0

The e–h convolution vanishes in positive degree.

theorem RS.fmix_eq_pow {k : ℕ} (hrec : HSubRec k) {A : Finset (Fin k)} {j : Fin k} (hj : j ∉ A) (m : ℕ) : fmix A j m = MvPolynomial.X j ^ m

The single-variable resolvent: the mixed convolution telescopes to a power of the extra variable.