Zulip Chat Archive

Stream: maths

Topic: polynomial functions


view this post on Zulip 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 ?

view this post on Zulip Johan Commelin (Oct 16 2020 at 12:00):

I'm sure that there is very little api

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 16 2020 at 12:06):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 13:38):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 13:40):

Probably these were written before polynomial.

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 13:44):

@Mario Carneiro Am I right?

view this post on Zulip Mario Carneiro (Oct 16 2020 at 13:46):

yes, although those definitions are also somewhat purpose-built

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 16 2020 at 15:36):

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

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 15:43):

Can we evaluate mv_polynomial α int on α → nat?

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 15:43):

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

view this post on Zulip Mario Carneiro (Oct 16 2020 at 15:53):

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

view this post on Zulip Mario Carneiro (Oct 16 2020 at 15:53):

I think some are yet missing

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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