English
Newton's identities give a recurrence for the k-th elementary symmetric polynomial esymm in terms of lower-degree polynomials esymm and power sums psum. Precisely, k esymm_k equals (-1)^{k+1} times a certain weighted sum of esymm and psum with combinatorial signs.
Русский
Ньютоновы тождества дают рекуррентную формулу для k-й элементарной симметрической полиномиальной функции esymm через более низкие степени esymm и psum с соответствующими знаками.
LaTeX
$$$k \cdot \mathrm{esymm}\, \sigma\, R\, k = (-1)^{k+1} \sum a \in \operatorname{antidiagonal}(k) (-1)^{a.1} \mathrm{esymm}\, \sigma\, R\, a.1 \cdot \mathrm{psum}\, \sigma\, R\, a.2$$$
Lean4
/-- **Newton's identities** give a recurrence relation for the kth elementary symmetric polynomial
in terms of lower degree elementary symmetric polynomials and power sums. -/
theorem mul_esymm_eq_sum (k : ℕ) :
k * esymm σ R k = (-1) ^ (k + 1) * ∑ a ∈ antidiagonal k with a.1 < k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 :=
by
classical
rw [NewtonIdentities.esymm_to_weight σ R k, NewtonIdentities.esymm_mul_psum_to_weight σ R k, eq_comm, ← sub_eq_zero,
sub_eq_add_neg, neg_mul_eq_neg_mul, neg_eq_neg_one_mul ((-1 : MvPolynomial σ R) ^ k)]
nth_rw 2 [← pow_one (-1 : MvPolynomial σ R)]
rw [← pow_add, add_comm 1 k, ← left_distrib, ←
sum_disjUnion (NewtonIdentities.disjoint_filter_pairs_lt_filter_pairs_eq σ k),
NewtonIdentities.disjUnion_filter_pairs_eq_pairs σ k, NewtonIdentities.weight_sum σ R k,
neg_one_pow_mul_eq_zero_iff.mpr rfl]
