Newton's Identities

This module implements Newton's identities relating power sums to elementary symmetric polynomials, enabling the translation from power sum equality to coefficient equality.

Key Results

• MvPolynomial.mul_esymm_eq_sum: Newton's identities formula
• multiset_newton_identity: Application to multisets of polynomial roots

References

• Blueprint §6 - Newton's identities framework
• Research Paper - Theorem 2.3 (page 5)
• Source Code

Main results

• multiset_newton_identity: Newton's identity for multisets
• esymm_eq_of_psum_eq: Equal power sums imply equal elementary symmetric functions
• esymm_rotated_roots_invariant: Elementary symmetric polynomials are θ-invariant

Tags

Newton's identities, elementary symmetric functions, power sums

theorem fin_univ_map_get (l : List ℝ) : Multiset.map (fun (i : Fin l.length) => l.get i) Finset.univ.val = ↑l

Conversion between Finset.univ mapped through list indexing and the list itself. Establishes that mapping List.get over all indices in Fin l.length recovers the original list as a multiset. This is used to convert between indexed sums (over Fin n) and multiset operations.

theorem fin_sum_eq_multiset_sum (l : List ℝ) (g : ℝ → ℝ) : ∑ i : Fin l.length, g (l.get i) = (Multiset.map g ↑l).sum

Equality between indexed sums and multiset sums. Shows that summing a function over indexed list elements (via Fin l.length) equals the multiset sum obtained by mapping the function and summing. This bridges the gap between finset-indexed sums and multiset operations.

theorem multiset_newton_identity (s : Multiset ℝ) (m : ℕ) : 0 < m → ↑m * s.esymm m = (-1) ^ (m + 1) * ∑ a ∈ Finset.antidiagonal m, if a.1 < m then (-1) ^ a.1 * s.esymm a.1 * (Multiset.map (fun (x : ℝ) => x ^ a.2) s).sum else 0

Newton's identity for multisets: relates elementary symmetric functions to power sums. For a multiset s and m > 0, we have: m * esymm_m = (-1)^(m+1) * ∑{i < m} (-1)^i * esymm_i * psum{m-i} where psum_j = ∑_{x ∈ s} x^j

theorem flatMap_singleton_cast (l : List ℕ) : (List.flatMap (fun (a : ℝ) => [a]) do let a ← l pure ↑a) = List.map Nat.cast l

Simplification of flatMap with singleton lists and type coercion. Establishes that flatMapping a list of naturals to singleton lists of reals is equivalent to directly mapping the coercion function. This simplifies list transformations involving type conversions.

theorem esymm_eq_of_psum_eq (s t : Multiset ℝ) (h_card : s.card = t.card) (h_psum : ∀ (j : ℕ), 0 < j → j < s.card → (Multiset.map (fun (x : ℝ) => x ^ j) s).sum = (Multiset.map (fun (x : ℝ) => x ^ j) t).sum) (m : ℕ) : m < s.card → s.esymm m = t.esymm m

Equal power sums imply equal elementary symmetric functions. If two multisets have the same cardinality and the same power sums, then they have the same elementary symmetric functions.

theorem polynomial_coeff_eq_of_esymm_eq (s t : Multiset ℝ) (c : ℝ) (_hc : c ≠ 0) (h_esymm : ∀ m < s.card, s.esymm m = t.esymm m) (h_card : s.card = t.card) (k : ℕ) (hk : 0 < k) (hk' : k ≤ s.card) : (Polynomial.C c * (Multiset.map (fun (r : ℝ) => Polynomial.X - Polynomial.C r) s).prod).coeff k = (Polynomial.C c * (Multiset.map (fun (r : ℝ) => Polynomial.X - Polynomial.C r) t).prod).coeff k

Equal elementary symmetric functions imply equal polynomial coefficients. If two multisets have the same esymm values, then the polynomials constructed from their roots have the same coefficients.

theorem multiset_esymm_one_eq_sum {R : Type u_1} [CommSemiring R] (s : Multiset R) : s.esymm 1 = s.sum

The first elementary symmetric function equals the sum. For any multiset s, esymm 1 computes the sum of all elements. This follows from the definition: selecting 1-element subsets gives singleton products, which are just the elements themselves.

theorem multiset_coe_realProjectionsList_sum (N : ℕ) (θ : ℝ) : (↑(realProjectionsList N θ)).sum = ∑ k ∈ Finset.range N, Real.cos (θ + 2 * Real.pi * ↑k / ↑N)

Multiset sum of real projections equals the Finset sum. Conversion lemma establishing that the multiset sum of realProjectionsList N θ (cosines of N equally-spaced angles starting at θ) equals the corresponding Finset sum over Finset.range N. Bridges list, multiset, and finset representations of the same sum.

theorem multiset_powersum_realProjectionsList (N : ℕ) (θ : ℝ) (j : ℕ) : (Multiset.map (fun (x : ℝ) => x ^ j) ↑(realProjectionsList N θ)).sum = ∑ k ∈ Finset.range N, Real.cos (θ + 2 * Real.pi * ↑k / ↑N) ^ j

Power sum of real projections as multiset equals Finset power sum. Establishes that the j-th power sum computed via multiset operations (map then sum) equals the same power sum computed as a Finset sum. This conversion is essential for applying Newton's identities to relate elementary symmetric functions to power sums of rotated roots.

theorem esymm_rotated_roots_invariant (N m : ℕ) (θ₁ θ₂ : ℝ) (hN : 0 < N) (hm : 0 < m) (hm' : m < N) : have l1 := ↑(realProjectionsList N θ₁); have l2 := ↑(realProjectionsList N θ₂); l1.esymm m = l2.esymm m

Elementary symmetric polynomials in rotated roots are θ-invariant for 0 < m < N.