Difficulty of formalizing a polynomial in Lean4

Stream: maths

[Brisal]

Hello! I want to formalize the following Polynomial:
(x^(-3) + x^(-2) + ... + x^2 + x^3) ^ 4

This is my #mwe

import Mathlib
def I := Finset.Icc (-3 : ℤ) 3

noncomputable def tset : Polynomial ℝ :=
  ∑ i ∈ I, if (0 : ℤ) ≤ i then Polynomial.X ^ (i.toNat)
  else (1 / Polynomial.X) ^ ((-i).toNat)

Is it right? Or maybe it has another way to formalize this.

[Brisal]

Maybe it should ues PowerSeries? :thinking:

[Yaël Dillies]

Indeed! This is not a polynomial

[Brisal]

Yaël Dillies said:

Indeed! This is not a polynomial

I'm really sorry, but I'm not quite sure how to formalize this. Could you please write an example for this one?

[Kevin Buzzard]

It's impossible to formlize "the polynomial (x^(-3) + x^(-2) + ... + x^2 + x^3) ^ 4" because that's not a polynomial (the $x^{-3}$ term is not allowed in a polynomial, by definition of polynomial). So you have to formalize something else. There are power series, Hahn series, rational functions, meromorphic functions and even occasionally-junk-valued functions all called (x^(-3) + x^(-2) + ... + x^2 + x^3) ^ 4 but until you say what the question is very precisely, it's difficult to answer it.

[Kevin Buzzard]

A theorem prover is an extremely pedantic thing. Even if you were to come here asking how to formalize 37, there would be the same question: do you mean the natural number 37, the integer 37, the real number 37, the p-adic number 37, the quaternion 37 etc etc.

In fact one of the subquestions here is: when you say $x^2$ you really mean $1\times x^2$. Which 1 is that?

[Brisal]

Kevin Buzzard said:

It's impossible to formlize "the polynomial (x^(-3) + x^(-2) + ... + x^2 + x^3) ^ 4" because that's not a polynomial (the $x^{-3}$ term is not allowed in a polynomial, by definition of polynomial). So you have to formalize something else. There are power series, Hahn series, rational functions, meromorphic functions and even occasionally-junk-valued functions all called (x^(-3) + x^(-2) + ... + x^2 + x^3) ^ 4 but until you say what the question is very precisely, it's difficult to answer it.

I indeed didn't state the requirements clearly. Actually, I'm formalizing an exercise problem:

"Build a generating function for $a_{r}$, the number of integer solutions to e_1 + e_2 + e_3 + e_4 = r, -3 \leq e_j \leq 3."

The answer is $x^{-3} + x^{-2} + \cdots + x^2 + x^3)^4.

[Kevin Buzzard]

Can I ask you another question? Can you build a generating function for $b_{r}$, where $b_{r}$ is always 37? What would your answer to that be?

[Brisal]

Kevin Buzzard said:

Can I ask you another question? Can you build a generating function for $b_{r}$, where $b_{r}$ is always 37? What would your answer to that be?

Like

PowerSeries.mk (fun _ => (37 : ℝ))

? Not for sure.

[Philippe Duchon]

If you want to take formal finite sums of integer powers of an indeterminate (which looks like this is what you want to do), Mathlib has LaurentPolynomial (of course power series by themselves won't do the trick). It also has LaurentSeries (finite support in the negative integers).

I don't think Mathlib has very good support for generating functions (in the enumerative combinatorics sense) at the moment, even when the solutions are "just" power series; going with negative exponents is only making it more complex.

[Brisal]

Philippe Duchon said:

If you want to take formal finite sums of integer powers of an indeterminate (which looks like this is what you want to do), Mathlib has LaurentPolynomial (of course power series by themselves won't do the trick). It also has LaurentSeries (finite support in the negative integers).

I don't think Mathlib has very good support for generating functions (in the enumerative combinatorics sense) at the moment, even when the solutions are "just" power series; going with negative exponents is only making it more complex.

I got that. I fact I've tried to use LaurentPolynomial and LaurentSeries to solve this problem., but finally I found that is difficult.

[Kenny Lau]

Risal said:

Like

PowerSeries.mk (fun _ => (37 : ℝ))

? Not for sure.

why R?

[Brisal]

Kenny Lau said:

Risal said:

Like

PowerSeries.mk (fun _ => (37 : ℝ))

? Not for sure.

why R?

I'm more accustomed to adding R, so this works: PowerSeries.mk (fun _ => 37)

[Kenny Lau]

the point of Kevin's question is to ask you what type 37 should be, and in your new answer you've left out its type

[Aaron Liu]

well the default is Nat

[Riccardo Brasca]

@Risal what we are trying to say is that the problem here is mathematical before being about Lean. You say you are interested in $x^{-3} + x^{-2} + \cdots$: but what kind of object is this for you? We don't want a super precise answer (Lean will want this, but we can help), but you cannot say "it's a polynomial", as polynomials don't have monomial of negative degree. You may want:

• Laurent polynomials
• Laurent series
• Puiseux series
• Meromorphic functions if you are more analytical than algebraic
• more exotic things

[Eric Wieser]

docs#LaurentPolynomial indeed seems like a good fit here

[Kevin Buzzard]

Another point is this (which I was going to get to later). I wanted to let $r$ be an integer, because that seems to be what's happening in the original question. So the answer to my question must be something like $\sum_{n\in\Z}37x^n$. But the original question has a ^4 in which means that the target type must have exponentiation by a positive natural. But what the heck does $(\sum_{n\in\Z}37x^n)^4$ mean? This involves non-convergent sums 37+37+37+37+... .

[Weiyi Wang]

Philippe Duchon said:

I don't think Mathlib has very good support for generating functions (in the enumerative combinatorics sense) at the moment, even when the solutions are "just" power series; going with negative exponents is only making it more complex.

On a related note, I started working on some of these in #30567

[Brisal]

Thank for everyone's advice. I'm going to learn how to formalize it in Laurent ploynomials,

[Brisal]

Riccardo Brasca said:

Risal what we are trying to say is that the problem here is mathematical before being about Lean. You say you are interested in $x^{-3} + x^{-2} + \cdots$: but what kind of object is this for you? We don't want a super precise answer (Lean will want this, but we can help), but you cannot say "it's a polynomial", as polynomials don't have monomial of negative degree. You may want:

• Laurent polynomials
• Laurent series
• Puiseux series
• Meromorphic functions if you are more analytical than algebraic
• more exotic things

Thank you for your help. In fact, I am indeed unfamiliar with the mathematics in this field. I will look into it.

[Timothy Chow]

In enumerative combinatorics, one is usually interested in a formal power series ring such as

$$\mathbb{Q}[[x]]$$

or maybe a formal Laurent series ring when (as here) one wants negative exponents. But one complication is that when the coefficients don't grow too fast, one often wants to treat the series as a holomorphic function, and apply complex-analytic techniques to estimate the growth rate of the coefficients. Of course all this is overkill for the original question which involves only a Laurent polynomial, but maybe one should be prepared for the possibility that the next few exercises will involve power series.