Evaluated symmetric values and the power–complete Newton identity

The specialization layer works with complex values rather than a formal symmetric-function ring: for a finite family x : Fin N → ℂ we define the power sums pVal x c and the complete homogeneous values hVal x k (a sum over size-k multisets), and prove the Newton identity

`(k+1) · h_{k+1} = ∑_{i ≤ k} p_{i+1} · h_{k−i}`

by double counting: adding i+1 copies of a marked variable to a size-(k−i) multiset produces each size-(k+1) multiset once per unit of multiplicity. Consequently hVal x satisfies the defining recursion of newtonH (pVal x).

noncomputable def RS.pVal {N : ℕ} (x : Fin N → ℂ) (c : ℕ) : ℂ

The power sum of exponent c of a finite family.

Equations

• RS.pVal x c = ∑ j : Fin N, x j ^ c

noncomputable def RS.hVal {N : ℕ} (x : Fin N → ℂ) (k : ℕ) : ℂ

The complete homogeneous value of degree k of a finite family: the sum of the products of all size-k multisets.

Equations

• RS.hVal x k = ∑ s : Sym (Fin N) k, (Multiset.map x ↑s).prod

@[simp]

theorem RS.hVal_zero {N : ℕ} (x : Fin N → ℂ) : hVal x 0 = 1

The degree-zero complete homogeneous value is 1.

theorem RS.sum_split_eq_count {N : ℕ} (x : Fin N → ℂ) (k : ℕ) (j : Fin N) : ∑ i ∈ Finset.range (k + 1), ∑ s : Sym (Fin N) (k - i), x j ^ (i + 1) * (Multiset.map x ↑s).prod = ∑ S : Sym (Fin N) (k + 1), ↑(Multiset.count j ↑S) * (Multiset.map x ↑S).prod

The per-variable splitting identity: marking i+1 copies of j inside a size-(k+1) multiset, every multiset arises once per unit of the multiplicity of j.

theorem RS.hVal_newton {N : ℕ} (x : Fin N → ℂ) (k : ℕ) : (↑k + 1) * hVal x (k + 1) = ∑ i ∈ Finset.range (k + 1), pVal x (i + 1) * hVal x (k - i)

The power–complete Newton identity, at the level of values.

theorem RS.newtonH_pVal {N : ℕ} (x : Fin N → ℂ) (k : ℕ) : newtonH (pVal x) k = hVal x k

hVal satisfies the newtonH recursion: the complete homogeneous values are the Newton lifts of the power sums.