Power Sum Polynomials


Title: Power Sum Polynomials
Author: Manuel Eberl
Submission date: 2020-04-24

This article provides a formalisation of the symmetric multivariate polynomials known as power sum polynomials. These are of the form pn(X1,…, Xk) = X1n + … + Xkn. A formal proof of the Girard–Newton Theorem is also given. This theorem relates the power sum polynomials to the elementary symmetric polynomials sk in the form of a recurrence relation (-1)k k sk = ∑i∈[0,k) (-1)i si pk-i .

As an application, this is then used to solve a generalised form of a puzzle given as an exercise in Dummit and Foote's Abstract Algebra: For k complex unknowns x1, …, xk, define pj := x1j + … + xkj. Then for each vector a ∈ ℂk, show that there is exactly one solution to the system p1 = a1, …, pk = ak up to permutation of the xi and determine the value of pi for i>k.

  author  = {Manuel Eberl},
  title   = {Power Sum Polynomials},
  journal = {Archive of Formal Proofs},
  month   = apr,
  year    = 2020,
  note    = {\url{http://isa-afp.org/entries/Power_Sum_Polynomials.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Polynomial_Factorization, Symmetric_Polynomials
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.