Equal Symmetric Functions Imply Equal Coefficients

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.NewtonIdentities

Statement

Theorem Equal Symmetric Functions Imply Equal Coefficients

If $e_m(s) = e_m(t)$ for all $m < |s|$ and $|s| = |t|$, then for $0 < k \le |s|$, the coefficient of $x^k$ in $c \cdot \prod_{r \in s}(X - r)$ equals that in $c \cdot \prod_{r \in t}(X - r)$.

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

Proof ▼

By Vieta's formulas, the coefficient of $x^{|s|-k}$ is $(-1)^k e_k$. Since $e_k(s) = e_k(t)$ for $k < |s|$, the coefficients match for all degrees $\ge 1$.


  -- Use Vieta's formula: coefficient k is determined by esymm (card - k)
  rw [coeff_C_mul, coeff_C_mul]
  congr 1
  -- Apply Vieta's formula:
  -- (s.map (X - C ·)).prod.coeff k = (-1)^(s.card - k) * s.esymm (s.card - k)
  rw [Multiset.prod_X_sub_C_coeff s hk',
      Multiset.prod_X_sub_C_coeff t (by rw [← h_card]; exact hk')]
  -- Now show (-1)^(s.card - k) * s.esymm (s.card - k) = (-1)^(t.card - k) * t.esymm (t.card - k)
  congr 1
  · -- Show s.card - k = t.card - k
    rw [h_card]
  · -- Show s.esymm (s.card - k) = t.esymm (t.card - k)
    have h_diff_lt : s.card - k < s.card := by omega
    rw [h_esymm (s.card - k) h_diff_lt, h_card]

Dependencies (uses)

None

Dependents (used by)

Coefficient Matching at theta = 0

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