Basic properties of polynomials

Stream: Is there code for X?

[Luke Mantle]

Are there lemmas for each of the following properties of polynomials?

• A sum of polynomials is a polynomial
• A product of polynomials is a polynomial
• The derivative of a polynomial is a polynomial

[Eric Wieser]

I suspect it's not the answer you want, but +, *, and docs#polynomial.derivative seem to match those requests

[Eric Wieser]

Your first two questions, in the context of docs#polynomial, is like asking "is there a lemma that says the sum of integers is an integer".

[Yakov Pechersky]

I think that maybe this can be interpreted as, are the polynomials a semiring?

[Yakov Pechersky]

Or, functions that when evaluated are pointwise equivalent to polynomial.eval, that is also true on sums of such functions

[Junyan Xu]

For this interpretation, we have docs#polynomial.eval_add, docs#polynomial.eval_mul, and docs#polynomial.deriv

[Kevin Buzzard]

Note that over finite rings there can be different polynomials giving rise to the same functions, so polynomials are no longer determined by the functions they induce

[Luke Mantle]

Junyan Xu said:

For this interpretation, we have docs#polynomial.eval_add, docs#polynomial.eval_mul, and docs#polynomial.deriv

Hmm ok this might be what I'm looking for.

Well, suppose I have (f : ℝ → ℝ) (h : ∀ x : ℝ, f x = x - 1). How can I show that f is a polynomial so that I can then use these properties on it?

[Eric Wieser]

You can show that f = (X - 1 : polynomial ℝ).eval

[Eric Wieser]

That likely follows from ext, simp [h]

[Ruben Van de Velde]

Yeah, "f is a polynomial" would be expressed in type theory as \exists p : \R[X], p.eval = f

[Kevin Buzzard]

Just to reiterate, there is a map from polynomials to functions, but to say that a function "is" a polynomial is not really meaningful in lean. And there are cases where two polynomials can give the same function.

[Luke Mantle]

Kevin Buzzard said:

Just to reiterate, there is a map from polynomials to functions, but to say that a function "is" a polynomial is not really meaningful in lean. And there are cases where two polynomials can give the same function.

Right, I'll keep this in mind

[Luke Mantle]

Ruben Van de Velde said:

Yeah, "f is a polynomial" would be expressed in type theory as \exists p : \R[X], p.eval = f

So I tried going this route, but I'm not sure quite what the proof would look like. This is my failed attempt:

example (f : ℝ → ℝ) (h : ∀ x : ℝ, f x = x - 1) : ∃ p : (polynomial ℝ), ∀ x : ℝ, f x = (p.eval x) :=
begin
  use ((λ x, x - 1) : (polynomial ℝ)),
end

[Eric Wieser]

The polynomial you want is X - 1, not (λ x, x - 1). docs#polynomial.X

[Luke Mantle]

Eric Wieser said:

The polynomial you want is X - 1, not (λ x, x - 1). docs#polynomial.X

Ah, ok, thanks!

[Johan Commelin]

Kevin Buzzard said:

Just to reiterate, there is a map from polynomials to functions, but to say that a function "is" a polynomial is not really meaningful in lean. And there are cases where two polynomials can give the same function.

@Luke Mantle I would argue that it isn't even mathematically correct outside of Lean to say that a function "is" a polynomial. It is important to distinguish the two!

[Junyan Xu]

To be fair, people definitely talk about polynomial functions.

[Johan Commelin]

Yes, but in my experience, it is always called that: a polynomial function.

[Adam Topaz]

The philosophical difference is that a polynomial over a ring $A$ can be evaluated at elements in any $A$-algebra, but a polynomial function on $A$ can only be evaluated at elements of $A$

[Adam Topaz]

At least that's how I distinguish the two

[Anne Baanen]

To me an important difference is there can be many more polynomials than polynomial functions: over a finite field, there are finitely many polynomial functions (since there are finitely many functions) but infinitely many polynomials.

[Jireh Loreaux]

While I understand the (important) distinction between polynomial and polynomial function, in my analysis circles we generally only ever use the term "polynomial". If necessary, context is used to disambiguate.

[Kevin Buzzard]

Yeah, if you're working over the reals (as the original poster was) then it's less of an issue. The only reason it comes up is because lean is working over a general base so the issue is there in lean whether or not you care about it