## Stream: maths

### Topic: Constructing Polynomials

#### 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).

#### Reid Barton (Oct 25 2020 at 20:38):

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

#### Kevin Buzzard (Oct 25 2020 at 20:39):

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

#### 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⟩


#### Johan Commelin (Oct 25 2020 at 20:44):

L298 of data.finsupp.basic

#### 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?

#### 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?

#### Thomas Browning (Oct 25 2020 at 20:47):

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

#### 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

#### 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)

#### 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),

#### 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