Newton's identities

Stream: maths

[Kevin Buzzard]

I had it in mind that "Newton's identities" on the UG todo list should mean the theorem which says that the $S_n$-invariants of $R[X_1,X_2,...,X_n]$ equals $R[e_1,e_2,...,e_n]$. But on the todo list page the Wikipedia link is to a page called Newton's identities which are explicit formulae for $\sum_i X_i^k$ in terms of the $e_j$ and $\sum_i X_i^{k'}$ for $k'<k$. I have an undergraduate interested in doing these and I've suggested they work on the latter, as they feel more like identities than the result I was quoting above. Is this what is required?

[Johan Commelin]

Yes, I think so

[Johan Commelin]

https://github.com/leanprover-community/mathlib/pull/3169/files#diff-35f33e1426e44b39c25727d721f3ad04cdf09c7fc57a5ccb04d166c1eb2f31fa is a rough start on symmetric polynomials

[Johan Commelin]

Not claiming it is any good.

[Patrick Massot]

It meant the identities but of course in the long run we want both.

[Kevin Buzzard]

But doing the identities will remove the item from the UG todo list, so we'll start there!

[Jake Levinson]

There are some nice generating function proofs of Newton's identities that prove them "all at once" rather than e.g. by induction or by counting. I don't know if these would be easy to carry out in Lean but they were certainly easier for me to understand when I first learned them.

Wikipedia sketches the argument here: https://en.wikipedia.org/wiki/Newton%27s_identities#Comparing_coefficients_in_series.

I wrote a version as cleanly as I could here (see "The Power Symmetric Polynomials"), avoiding term-by-term comparisons until the very end: https://levjake.wordpress.com/2013/11/26/everything-you-wanted-to-know-about-symmetric-polynomials-part-ii/.

[Kevin Buzzard]

Thanks a lot for this Jake! Right now the UG in question is trying to find the nicest proof to formalise.

[Jake Levinson]

As a warmup, I would instead suggest proving the e-to-h identities, which are algebraically quite similar but the proof is easier, the proof is:

$\displaystyle{\big(\sum_{k=0}^\infty (-1)^k e_k t^k \big) \big(\sum_{k=0}^\infty h_k t^k \big) = \prod_{i=1}^\infty (1 - x_i t) \prod_{i=1}^\infty \frac{1}{(1-x_i t)} = 1,}$

then expand term by term. Mathematically this will require a subset of the same tools as Newton's identities (geometric series and generating function magic, but no exp or log).

[Kevin Buzzard]

Do we have docs#mv_power_series ? Edit: oh cool, we do!