MvPolynomial.mul_esymm_eq_sum
theorem MvPolynomial.mul_esymm_eq_sum :
∀ (σ : Type u_1) [inst : Fintype σ] (R : Type u_2) [inst_1 : CommRing R] (k : ℕ),
↑k * MvPolynomial.esymm σ R k =
(-1) ^ (k + 1) *
(Finset.filter (fun a => a.1 < k) (Finset.antidiagonal k)).sum fun a =>
(-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2
Newton's Identities provide a relationship between the kth elementary symmetric polynomial and lower degree elementary symmetric polynomials and power sums. Specifically, the kth elementary symmetric polynomial multiplied by k is equal to the sum, over all pairs (a, b) in the antidiagonal of k for which a is less than k, of (-1) raised to the power a+1 times the ath elementary symmetric polynomial times the bth power sum. Note that the antidiagonal of a number k is the set of pairs (a, b) such that a + b = k. This theorem is defined for any type σ (which has Fintype instance) and any commutative ring R.
More concisely: For any commutative ring R and type σ with Fintype instance, the kth elementary symmetric polynomial S\_k multiplied by k equals the sum, over all pairs (a, b) in the antidiagonal of k with a < k, of (-1) ^ (a+1) * S\_a * P\_b, where S\_i are elementary symmetric polynomials and P\_j are power sums.
|
MvPolynomial.psum_eq_mul_esymm_sub_sum
theorem MvPolynomial.psum_eq_mul_esymm_sub_sum :
∀ (σ : Type u_1) [inst : Fintype σ] (R : Type u_2) [inst_1 : CommRing R] (k : ℕ),
0 < k →
MvPolynomial.psum σ R k =
(-1) ^ (k + 1) * ↑k * MvPolynomial.esymm σ R k -
(Finset.filter (fun a => a.1 ∈ Set.Ioo 0 k) (Finset.antidiagonal k)).sum fun a =>
(-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2
This theorem provides a version of Newton's identities, which can be particularly useful when we know the values of the elementary symmetric polynomials and wish to calculate the values of the power sums. Specifically, for any given set `σ` of a `Fintype` and any given `CommRing` `R`, and for any natural number `k` greater than 0, the `k`th power sum polynomial is defined to be equal to (-1) to the power of `(k+1)` times `k` times the `k`th elementary symmetric polynomial minus the sum of the products of (-1) to the power of `a.1` times the `a.1`th elementary symmetric polynomial times the `a.2`th power sum polynomial over all pairs `(a.1, a.2)` in the antidiagonal of `k` such that `a.1` is in the open interval from 0 to `k`.
More concisely: For any CommRing R and Fintype σ, the k-th power sum polynomial equals (-1)^(k+1) * k * Ek(x) - ∑\_{a.1 < a.2 in pairs on the antidiagonal of k} (-1)^(a.1) * E(a.1)(x) * P(a.2)(x), where Ek and P are the k-th elementary symmetric polynomial and power sum polynomial, respectively.
|