Surjectivity of the power-sum specialization

Every finite sequence of prospective power sums is realized by an actual finite family of complex numbers: Newton-invert the prescribed values to elementary symmetric values, build the monic polynomial with those (sign-alternating) coefficients, split it over ℂ, and read the roots. The roots' elementary values match by Vieta, and their power sums then agree with the prescription by the triangular Newton recursion.

This is the globalization device: symmetric-function identities are proved for genuine variable families and transferred to arbitrary prospective power sums.

@[irreducible]

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

The elementary values prescribed by a sequence of power sums, via the Newton recursion.

Equations

• RS.eSeq t 0 = 1
• RS.eSeq t k.succ = (↑k + 1)⁻¹ * (-1) ^ (k + 2) * ∑ a ∈ {a ∈ Finset.antidiagonal (k + 1) | a.1 < k + 1}.attach, (-1) ^ (↑a).1 * RS.eSeq t (↑a).1 * t (↑a).2

theorem RS.eSeq_mul (t : ℕ → ℂ) (k : ℕ) : (↑k + 1) * eSeq t (k + 1) = (-1) ^ (k + 2) * ∑ a ∈ Finset.antidiagonal (k + 1) with a.1 < k + 1, (-1) ^ a.1 * eSeq t a.1 * t a.2

The defining relation of eSeq, unattached and cleared of the inverse.

theorem RS.t_eq_of_eSeq (t : ℕ → ℂ) (c : ℕ) (hc : 0 < c) : t c = (-1) ^ (c + 1) * ↑c * eSeq t c - ∑ a ∈ Finset.antidiagonal c with a.1 ∈ Set.Ioo 0 c, (-1) ^ a.1 * eSeq t a.1 * t a.2

The prescription satisfies the solved form of the Newton recursion.

The realizing polynomial and its roots

noncomputable def RS.ePoly (t : ℕ → ℂ) (n : ℕ) : Polynomial ℂ

The monic polynomial with the prescribed alternating elementary coefficients.

Equations

• RS.ePoly t n = ∑ k ∈ Finset.range (n + 1), (Polynomial.monomial (n - k)) ((-1) ^ k * RS.eSeq t k)

theorem RS.ePoly_coeff {t : ℕ → ℂ} {n k : ℕ} (hk : k ≤ n) : (ePoly t n).coeff (n - k) = (-1) ^ k * eSeq t k

The polynomial's coefficients are the prescribed elementary values, alternating in sign.

theorem RS.ePoly_coeff_self (t : ℕ → ℂ) (n : ℕ) : (ePoly t n).coeff n = 1

Its leading coefficient is 1.

theorem RS.ePoly_natDegree (t : ℕ → ℂ) (n : ℕ) : (ePoly t n).natDegree = n

Its degree is the number of prescribed values.

theorem RS.ePoly_monic (t : ℕ → ℂ) (n : ℕ) : (ePoly t n).Monic

It is monic.

theorem RS.ePoly_card_roots (t : ℕ → ℂ) (n : ℕ) : (ePoly t n).roots.card = n

Hence it has exactly that many roots over ℂ — the family the prescription is realized by.

theorem RS.ePoly_roots_esymm (t : ℕ → ℂ) {n k : ℕ} (hk : k ≤ n) : (ePoly t n).roots.esymm k = eSeq t k

Vieta: the roots of the realizing polynomial have the prescribed elementary values.

The surjectivity of the power-sum specialization

theorem RS.aeval_psum {N : ℕ} (x : Fin N → ℂ) (k : ℕ) : (MvPolynomial.aeval x) (MvPolynomial.psum (Fin N) ℂ k) = pVal x k

Evaluation of the power-sum polynomial is pVal.

theorem RS.exists_pVal_eq (n : ℕ) (t : ℕ → ℂ) : ∃ (N : ℕ) (x : Fin N → ℂ), ∀ (c : ℕ), 1 ≤ c → c ≤ n → pVal x c = t c

Every prospective power-sum sequence is realized by a finite family of complex numbers, up to any given degree.