Newton's Identities for Multisets

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.NewtonIdentities

Statement

Newton's identities recursively determine the elementary symmetric polynomials $e_k$ from the power sums $p_j = \sum \alpha_i^j$.

Theorem Newton's Identities for Multisets

[blueprint]

For a multiset $s$ and $m > 0$, $m \cdot e_m(s) = (-1)^{m+1} \sum_{\substack{(a,b) \\ a+b = m,\; a < m}} (-1)^a\, e_a(s)\, p_b(s).$

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

Proof ▼

Evaluate the multivariable polynomial Newton identity (`MvPolynomial.mul_esymm_eq_sum`) at the list elements via `aeval`, then convert between finset-indexed and multiset representations.


  -- Get a list representation of the multiset
  obtain ⟨l, rfl⟩ := Quot.exists_rep s
  -- Apply MvPolynomial.mul_esymm_eq_sum with σ = Fin l.length
  have mvpoly_newton := MvPolynomial.mul_esymm_eq_sum (Fin l.length) ℝ m
  -- Evaluate both sides using aeval with f i = l.get i
  have key := congr_arg (MvPolynomial.aeval (fun i : Fin l.length => l.get i)) mvpoly_newton
  simp only [map_mul, map_natCast] at key
  -- Convert LHS using aeval_esymm_eq_multiset_esymm
  rw [MvPolynomial.aeval_esymm_eq_multiset_esymm] at key
  have list_eq : (Finset.univ.val.map (fun i : Fin l.length => l.get i) : Multiset ℝ) = ↑l :=
    fin_univ_map_get l
  rw [list_eq] at key
  -- Convert RHS
  simp only [map_mul, map_pow, map_neg, map_one, map_sum] at key
  -- Rewrite the filtered sum as an if-sum
  rw [Finset.sum_filter] at key
  -- Now key has the right structure, convert to match the goal
  -- Note: ↑l and Quot.mk (List.isSetoid ℝ) l are definitionally equal
  convert key using 2
  apply Finset.sum_congr rfl
  intro x _
  split_ifs with hx
  · -- When x.1 < m, we need to show the terms are equal
    congr 1
    · congr 1  -- Handle esymm part
      change (↑l : Multiset ℝ).esymm x.1 = _
      rw [← list_eq, MvPolynomial.aeval_esymm_eq_multiset_esymm, list_eq]
    · -- Handle psum part: (↑l).map (· ^ x.2) |>.sum = aeval ... (psum ...)
      change ((↑l : Multiset ℝ).map (fun x_1 => x_1 ^ x.2)).sum = _
      rw [MvPolynomial.psum, map_sum]
      simp only [map_pow, MvPolynomial.aeval_X]
      rw [fin_sum_eq_multiset_sum l (· ^ x.2), ← list_eq]
  · rfl

Dependencies (uses)

Dependents (used by)

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms