Zulip Chat Archive

Stream: maths

Topic: Constructing Polynomials


view this post on Zulip Thomas Browning (Oct 25 2020 at 20:37):

If I have f : (↑(finset.range n) : set ℕ) → F, what's the best way to turn this into a polynomial (where f is giving the coefficients of the polynomial)? It seems like a polynomial is secretly a finsupp, but turning f into a finsupp seems a bit painful (since some of the coefficients could be zero).

view this post on Zulip Reid Barton (Oct 25 2020 at 20:38):

Probably something involving a suitable sum of f i * X^i

view this post on Zulip Kevin Buzzard (Oct 25 2020 at 20:39):

And your next question is how to prove that the coefficient of XiX^i is f(i)f(i), right?

view this post on Zulip Johan Commelin (Oct 25 2020 at 20:44):

/-- `on_finset s f hf` is the finsupp function representing `f` restricted to the finset `s`.
  The function needs to be `0` outside of `s`. Use this when the set needs to be filtered anyways,
  otherwise a better set representation is often available. -/
def on_finset (s : finset α) (f : α  M) (hf : a, f a  0  a  s) : α →₀ M :=
s.filter (λa, f a  0), f, by simpa

view this post on Zulip Johan Commelin (Oct 25 2020 at 20:44):

L298 of data.finsupp.basic

view this post on Zulip Reid Barton (Oct 25 2020 at 20:45):

and now your next question is how to show that when you evaluate it at x : F it agrees with the sum f i * x^i, right?

view this post on Zulip Thomas Browning (Oct 25 2020 at 20:46):

@Johan Commelin I saw that, but wouldn't I need to extend f to all of the natural numbers?

view this post on Zulip Thomas Browning (Oct 25 2020 at 20:47):

@Reid Barton Actually it's just Kevin's question that I need

view this post on Zulip Thomas Browning (Oct 25 2020 at 20:47):

At the end, I just need to know that it's a polynomial of degree less than n whose coefficients agree with f

view this post on Zulip Reid Barton (Oct 25 2020 at 20:48):

ah, lucky. But in general, using this on_finset directly would be breaking the abstraction that polynomial provides (or pretends to provide)

view this post on Zulip Thomas Browning (Oct 25 2020 at 23:49):

For reference, I ended up going with the finsupp.on_finset approach, by first extending f to by let g : ℕ → F := λ k, dite (k < n) (λ h, f ⟨k, finset.mem_coe.mpr (finset.mem_range.mpr h)⟩) (λ h, 0),

view this post on Zulip Thomas Browning (Oct 25 2020 at 23:50):

it ended up being fine, albeit rather longwinded


Last updated: May 11 2021 at 17:39 UTC