English
A form of Newton's identities expressing psum k in terms of esymm k and a signed sum over the antidiagonal; this provides a usable relation between power sums and elementary symmetric polynomials.
Русский
Формула Ньютона выражает psum k через esymm k и знаковую сумму по антидиагонали, обеспечивая связь между степенями и элементарными симметрическими полиномами.
LaTeX
$$$\operatorname{psum} \sigma\, R\, k = (-1)^{k+1} k \mathrm{esymm}\, \sigma\, R\, k - \sum a \in \operatorname{antidiagonal}(k) (-1)^{a.1} \mathrm{esymm}\, \sigma\, R a.1 \cdot \mathrm{psum}\, \sigma\, R a.2$$$
Lean4
/-- A version of Newton's identities which may be more useful in the case that we know the values of
the elementary symmetric polynomials and would like to calculate the values of the power sums. -/
theorem psum_eq_mul_esymm_sub_sum (k : ℕ) (h : 0 < k) :
psum σ R k =
(-1) ^ (k + 1) * k * esymm σ R k -
∑ a ∈ antidiagonal k with a.1 ∈ Set.Ioo 0 k, (-1) ^ a.fst * esymm σ R a.1 * psum σ R a.2 :=
by
simp only [Set.Ioo, Set.mem_setOf_eq, and_comm]
have hesymm := mul_esymm_eq_sum σ R k
rw [←
(sum_filter_add_sum_filter_not ({a ∈ antidiagonal k | a.fst < k}) (fun a ↦ 0 < a.fst)
(fun a ↦ (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd))] at hesymm
have sub_both_sides :=
congrArg
(· -
(-1 : MvPolynomial σ R) ^ (k + 1) *
∑ a ∈ {a ∈ antidiagonal k | a.fst < k} with 0 < a.fst, (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd)
hesymm
simp only [left_distrib, add_sub_cancel_left] at sub_both_sides
have sub_both_sides := congrArg ((-1 : MvPolynomial σ R) ^ (k + 1) * ·) sub_both_sides
simp only [mul_sub_left_distrib, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k + 1, rfl⟩, one_mul,
filter_filter (fun a : ℕ × ℕ ↦ a.fst < k) (fun a ↦ ¬0 < a.fst)] at sub_both_sides
have : {a ∈ antidiagonal k | a.fst < k ∧ ¬0 < a.fst} = {(0, k)} :=
by
ext a
rw [mem_filter, mem_antidiagonal, mem_singleton]
refine ⟨?_, by rintro rfl; cutsat⟩
rintro ⟨ha, ⟨_, ha0⟩⟩
rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]
rw [this, sum_singleton] at sub_both_sides
simp only [_root_.pow_zero, esymm_zero, mul_one, one_mul, filter_filter] at sub_both_sides
exact sub_both_sides.symm
