Root isolations for real or complex roots

Stream: Is there code for X?

[metakuntyyy]

Given a polynomial in R[X] or C[X] do we have root isolating theorems.

For example in this interval/bounding box there exists exactly one root in a given interval. Like Sturm sequences or Descartes.

[Aaron Liu]

probably something like docs#MeromorphicOn.codiscrete_setOf_order_eq_zero_or_top I think?

[metakuntyyy]

Hmm, I fail to see how I could prove that given f and a box B there exists n roots in the interior of B. Maybe it would make sense to prove Sturm's theorem first if it's not proven yet.

[metakuntyyy]

I did some literature search and checked some computer algebra systems and they implement complex root isolation based on bounding boxes. Such as sage

[Aaron Liu]

oh I thought you wanted to show the roots were isolated

[Aaron Liu]

maybe should've read more carefully

[metakuntyyy]

It seems to be formalised in Isabelle this year: https://www.isa-afp.org/browser_info/current/AFP/Sturm_Sequences/outline.pdf

[Aaron Liu]

new idea: you can apply banach fixed point theorem to show a small enough box contains exactly one root

[metakuntyyy]

Hmmmm, very interesting. Do you know the theorem statement I need to prove?

[Aaron Liu]

you would need to provide a map which is a contraction on a small closed box around your root, and you would need to show any fixed point of that map within the box is a root

[Aaron Liu]

I recommend newton's method

[metakuntyyy]

Thanks :+1: , I'll try it with a toy example of a polynomial of degree 5 and see how it works.

[Artie Khovanov]

@Tomaz Mascarenhas is working on Sturm's theorem

[Bhavik Mehta]

@Alain Chavarri Villarello has useful stuff about this too, if I remember correctly

[Alain Chavarri Villarello]

I formalized a version of Sturm’s theorem over real closed fields (still needs polishing) which might be useful. The total root count result in $(-\infty, \infty)$ is sturm_theorem_total. The interval version is sturm_theorem, and, for now, it uses a technical assumption that is not strictly necessary.

[Artie Khovanov]

Oh nice! @Alain Chavarri Villarello would I be able to incorporate this material into my real closed field project? https://github.com/artie2000/real_closed_field
Or even better, would you be willing to collaborate? :slight_smile:

[Alain Chavarri Villarello]

@Artie Khovanov Of course, you can incorporate whatever you need! I’m not sure how much time I have to collaborate on this at the moment, but I’d be happy to chat about it :slight_smile:

[Artie Khovanov]

OK thanks, I will incorporate your work and DM you if I have any questions.