## Stream: maths

### Topic: polynomial functions

#### Anatole Dedecker (Oct 16 2020 at 10:19):

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 (Oct 16 2020 at 12:00):

I'm sure that there is very little api

#### Johan Commelin (Oct 16 2020 at 12:00):

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 (Oct 16 2020 at 12:06):

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

#### Johan Commelin (Oct 16 2020 at 12:12):

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

#### Yury G. Kudryashov (Oct 16 2020 at 13:38):

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

#### Yury G. Kudryashov (Oct 16 2020 at 13:39):

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

#### Yury G. Kudryashov (Oct 16 2020 at 13:40):

Probably these were written before polynomial.

#### Yury G. Kudryashov (Oct 16 2020 at 13:44):

@Mario Carneiro Am I right?

#### Mario Carneiro (Oct 16 2020 at 13:46):

yes, although those definitions are also somewhat purpose-built

#### Yury G. Kudryashov (Oct 16 2020 at 14:07):

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

#### Yury G. Kudryashov (Oct 16 2020 at 14:09):

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

#### Johan Commelin (Oct 16 2020 at 15:29):

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 (Oct 16 2020 at 15:34):

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 (Oct 16 2020 at 15:36):

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

#### Johan Commelin (Oct 16 2020 at 15:40):

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

#### Yury G. Kudryashov (Oct 16 2020 at 15:43):

Can we evaluate mv_polynomial α int on α → nat?

#### Yury G. Kudryashov (Oct 16 2020 at 15:43):

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

#### Mario Carneiro (Oct 16 2020 at 15:53):

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

#### Mario Carneiro (Oct 16 2020 at 15:53):

I think some are yet missing

#### Mario Carneiro (Oct 16 2020 at 15:56):

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

#### Mario Carneiro (Oct 16 2020 at 15:57):

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

#### Mario Carneiro (Oct 16 2020 at 15:58):

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

#### Yury G. Kudryashov (Oct 16 2020 at 16:08):

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

Last updated: May 18 2021 at 08:14 UTC