polynomial functions

Stream: maths

[Anatole Dedecker]

I was wondering : what is the preferred way to talk about polynomial functions in mathlib, for e.g. analysis purposes ? I was thinking of using polynomial.eval but it seems there are only a few analysis facts about it. Is it a lack of API, or am I just looking for the wrong thing ?

[Johan Commelin]

I'm sure that there is very little api

[Johan Commelin]

For the Witt project we needed a very special kind of polynomial function, but we defined an is_poly predicate on functions. It can work quite well.

[Reid Barton]

I suspect we have precisely enough to prove that the complex numbers are algebraically closed.

[Johan Commelin]

But I guess it's still ad hoc. That proof doesn't set up a small is_poly API either, afaik.

[Yury G. Kudryashov]

What's the difference between is_poly and ∃ p, p.eval = f?

[Yury G. Kudryashov]

We also have custom polynomials in docs#poly and docs#is_poly in number_theory/dioph

[Yury G. Kudryashov]

Probably these were written before polynomial.

[Yury G. Kudryashov]

@Mario Carneiro Am I right?

[Mario Carneiro]

yes, although those definitions are also somewhat purpose-built

[Yury G. Kudryashov]

BTW, the docstring of docs#is_poly doesn't mention the implications of using nat.sub in the definition.

[Yury G. Kudryashov]

And I think that it should be moved to a namespace (or migrated to mv_polynomial and ℤ-valued functions)

[Johan Commelin]

Yury G. Kudryashov said:

What's the difference between is_poly and ∃ p, p.eval = f?

In the case of witt vectors you need a nat-indexed family of polynomials. But for the general purpose notion, that would indeed be exactly the definition I would use.

[Mario Carneiro]

Yury G. Kudryashov said:

BTW, the docstring of docs#is_poly doesn't mention the implications of using nat.sub in the definition.

That's because it has no implications. It defines the correct subset even though nat.sub is used

[Mario Carneiro]

Actually I take it back, is_poly doesn't use nat.sub

[Johan Commelin]

Does it make sense to think that this code should be refactored to use mv_polynomial \a int?

[Yury G. Kudryashov]

Can we evaluate mv_polynomial α int on α → nat?

[Yury G. Kudryashov]

(I guess, the answer is "turn it into α → int first")

[Mario Carneiro]

I would suggest trying to locate all the analogous theorems before refactoring the file

[Mario Carneiro]

I think some are yet missing

[Mario Carneiro]

I suspect that even if this predicate was defined using mv_polynomial it is sufficiently different as to still require definition

[Mario Carneiro]

so perhaps it would be better to not change the definition and instead just relate it to mv_polynomial

[Mario Carneiro]

I rather like the fact that this file has few dependencies though. It seems like we would lose that

[Yury G. Kudryashov]

IMHO being related to general concepts defined in mathlib is more important than having few dependencies.