Zulip Chat Archive

Stream: general

Topic: Best way to reason on distribution of solutions?

Shi Zhengyu (Feb 05 2022 at 12:06):

Hi all,

What is the best way to reason about the distribution of real roots of a polynomial? I was trying to prove two polynomials' solutions are interlaced. Below is a definition of interlace I wrote for two lists.

mutual def Interlace, Interlace' {num_t: Type} [linear_order num_t]
with Interlace: list num_t -> list num_t -> Prop
| (x :: xs) (y :: ys) := (x <= y)  Interlace' xs (y :: ys)
| (x :: xs) nil := true
| _ _ := false
with Interlace': list num_t -> list num_t -> Prop
| (x :: xs) (y :: ys) := (y <= x)  Interlace (x :: xs) ys
| _ _ := false

Then I need to define

def solution (A: polynomial ): list  := sorry

Is it good practice to use above definition, and treat solutions as elements of a list? If so, how should I fill in the sorry above?


Kevin Buzzard (Feb 05 2022 at 12:34):

I don't know much about inductive types but if I were thinking about formalising this I would have just written the predicate directly; one doesn't need inductive types to do it: just write that the n'th term of one list is in between the n'th and the n+1st term of the other one. As for solution this is going to be there already -- at least as a finset -- let's try docs#polynomial.roots ? And then take the reals ones and sort them.

Last updated: Aug 03 2023 at 10:10 UTC