discriminants of low degree polynomials

Stream: mathlib4

[Christian Merten]

Since recently, we have docs#Polynomial.disc (added by @David Loeffler). We also have manually defined discriminants for polynomials of degree 2 and 3 in terms of docs#discrim and docs#Cubic.disc.
For degree 2, we already have that they agree (docs#Polynomial.disc_of_degree_eq_two).

I think these should be unified, i.e., I suggest to deprecate docs#discrim and docs#Cubic.disc. The only issue is that docs#Polynomial.disc requires CommRing while the manually defined ones only require Ring. However, almost all results for the old definitions assume commutativity anyways.
What do you think?

(The context is that I am looking at #25905 right now, which adds more things on discriminants of quadratic polynomials. I think we should stop having statements about terms like C a * X ^ 2 + C b * X + C c, but instead about p : R[X] with hp : p.natDegree = 2, because it is much easier to use. Deprecating docs#discrim would stop leading users to using the former.)

[Weiyi Wang]

For a non-commutative ring, is the definition of discrim mathematically correct/useful? I doubt it is, and if it is not, that would be a good reason to deprecate it

[Oliver Nash]

If people are interested in developing more about discriminants (and resultants) I think it would be good to upgrade our existing definitions to be polynomials rather than scalars.

[David Loeffler]

Tangentially related: I wrote a proof that the general definition of discriminant recovers the standard formula for cubics, mostly to check I had the signs right; but I didn’t include it in the PR, because evaluating the det of a 5 x 5 matrix takes more than the default heartbeat limit! Is provably correct evaluation of determinants really that hard, or was I just doing it wrong?

[Oliver Nash]

I also thought it was a shame that your cubic discriminant proof didn't make it to master because of the required heartbeat bump.

I only looked at the proof for a few minutes but I don't remember it being the evaluation of the determinant that took the time. IIRC there was a 25-way case split with a non-trivial goal discharged by simp in each case which was the real culprit. And when I looked at that I thought one thing that might have helped was further upstream API (to avoid unfolding some definitions in those simp calls).

[Oliver Nash]

It was a nice proof though, and because it's elementary you might get lucky if you post it in general and challenge people to speed it up / provide a fast proof!

[Violeta Hernández]

Tangential note, but I think the hypothesis should be p.degree = 2 instead of p.natDegree = 2. It's generally a bit easier to go from degree to natDegree than the other way around.

[Mr Proof]

Fun fact of nonlinear algebra: :smiley:

All systems of polynomial inequalities in the reals can be put in the following form by introducing additional variables:

$\exists x \in \mathbb{R}^N / \{0\} : A^{ijkl}x_i x_j x_k x_l = 0$

The condition to when such an equation has solutions can be written in terms of symmetrical invariants in terms of $A$.
For $N=2$ these include generalisations of hyper-determinants. For $N>2$ they are wildly complicated. (It would be fun to document this somewhere).

There is an algorithm to solve all such equations but it runs higher than exponential time.

They can also be written as a system of quadratics but that is less symmetric IMO:

$\exists y \in \mathbb{R}^N / \{0\} : \bigwedge\limits_{k=0}^M B_k^{ij}y_i y_j= 0$

but it has a nicer geometric meaning of when do M, N-dimensional ellipsoids intersect.

[David Loeffler]

Oliver Nash said:

I also thought it was a shame that your cubic discriminant proof didn't make it to master because of the required heartbeat bump.

I only looked at the proof for a few minutes but I don't remember it being the evaluation of the determinant that took the time. IIRC there was a 25-way case split with a non-trivial goal discharged by simp in each case which was the real culprit. And when I looked at that I thought one thing that might have helped was further upstream API (to avoid unfolding some definitions in those simp calls).

FWIW, I have now PR'd the cubic discriminant formula at #29431. I managed to speed it up a fair bit by doing as much simp'ing as possible before the case-split (prompted by your remark making me realise that I had mis-diagnosed where the real slowness was – thanks!).

[Christopher Hoskin]

To this end I've opened https://github.com/leanprover-community/mathlib4/pull/29921

[Snir Broshi]

Violeta Hernández said:

Tangential note, but I think the hypothesis should be p.degree = 2 instead of p.natDegree = 2. It's generally a bit easier to go from degree to natDegree than the other way around.

I think the opposite is true, callers can use docs#Polynomial.natDegree_eq_of_degree_eq_some which doesn't require anything, unlike the other way around (docs#Polynomial.degree_eq_natDegree) which requires showing p ≠ 0.
Therefore I think hypotheses should use natDegree and conclusions should use degree

[Antoine Chambert-Loir]

Has somebody tried to formalize the formulas for degrees 4 and 5 ?
image.png
image.png
(from the book by Gelfand, Kapranov and Zelevinski, pages 405 and 406)

[Weiyi Wang]

This looks like also going to be a stress test for doc renderer :laughing:

[Christopher Hoskin]

And also #29980