Constructing Polynomials

Stream: maths

[Thomas Browning]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

/-- `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]

L298 of data.finsupp.basic

[Reid Barton]

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]

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

[Thomas Browning]

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

[Thomas Browning]

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]

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

[Thomas Browning]

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]

it ended up being fine, albeit rather longwinded