Newton's Identities

This file defines MvPolynomial power sums as a means of implementing Newton's identities. The combinatorial proof, due to Zeilberger, defines for k : ℕ a subset pairs of (range k).powerset × range k and a map pairMap such that pairMap is an involution on pairs, and a map weight which identifies elements of pairs with the terms of the summation in Newton's identities and which satisfies weight ∘ pairMap = -weight. The result therefore follows neatly from an identity implemented in mathlib as Finset.sum_involution. Namely, we use Finset.sum_involution to show that ∑ t ∈ pairs σ k, weight σ R k t = 0. We then identify (-1) ^ k * k * esymm σ R k with the terms of the weight sum for which t.fst has cardinality k, and (-1) ^ i * esymm σ R i * psum σ R (k - i) with the terms of the weight sum for which t.fst has cardinality i for i < k , and we thereby derive the main result (-1) ^ k * k * esymm σ R k + ∑ i ∈ range k, (-1) ^ i * esymm σ R i * psum σ R (k - i) = 0 (or rather, two equivalent forms which provide direct definitions for esymm and psum in lower-degree terms).

Main declarations

• MvPolynomial.mul_esymm_eq_sum: a recurrence relation for the kth elementary symmetric polynomial in terms of lower-degree elementary symmetric polynomials and power sums.

• MvPolynomial.psum_eq_mul_esymm_sub_sum: a recurrence relation for the degree-k power sum in terms of lower-degree elementary symmetric polynomials and power sums.

References

See [Zei84] for the combinatorial proof of Newton's identities.

theorem MvPolynomial.mul_esymm_eq_sum (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] (k : ℕ) : ↑k * MvPolynomial.esymm σ R k = (-1) ^ (k + 1) * ∑ a ∈ Finset.filter (fun (a : ℕ × ℕ) => a.1 < k) (Finset.antidiagonal k), (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2

Newton's identities give a recurrence relation for the kth elementary symmetric polynomial in terms of lower degree elementary symmetric polynomials and power sums.

theorem MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] : ∑ a ∈ Finset.antidiagonal (Fintype.card σ), (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2 = 0

theorem MvPolynomial.psum_eq_mul_esymm_sub_sum (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] (k : ℕ) (h : 0 < k) : MvPolynomial.psum σ R k = (-1) ^ (k + 1) * ↑k * MvPolynomial.esymm σ R k - ∑ a ∈ Finset.filter (fun (a : ℕ × ℕ) => a.1 ∈ Set.Ioo 0 k) (Finset.antidiagonal k), (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2

A version of Newton's identities which may be more useful in the case that we know the values of the elementary symmetric polynomials and would like to calculate the values of the power sums.