Working with Multivariate Polynomials

Stream: mathlib4

[Paul Wintz]

I am trying to work with multivariable polynomials, such as
a₁x₁²x₂² + a₂x₁² x₂ + a₃x₁x₂ + a₄x₁x₂² + ⋯ + c
using coefficients and variables in \mathbb{R}.

Ultimately, I want to do things like take derivatives, have vectors of polynomials, and show that given polynomials are positive definite, but currently, I'm having trouble simply specifying a polynomial using Mathlib.Data.MvPolynomial.Basic. Could somebody help me with an example of how to do this?

I imagine the process would be something like:

1. Specify a basis of monomials, such as {1, x_1, x_2, x_1^2, x_1x_2, x_2^2}.
2. Specify the coefficients to specify a linear combination.
   For the first step, I suspect we'd use MvPolynomial.monomial, but even defining one monomial is tripping me up (I'm still getting my sea/lean legs)

[David Ang]

If you have two variables x and y and want to write down a*x^2*y^2, perhaps you could do something like example : MvPolynomial (Fin 2) R := C a * X 0^2 * X 1^2, where C and X are under the MvPolynomial namespace? Here X is a function that takes in an index from an indexing set and outputs the variable with that index in the ordering of your choice. It’s really just a wrapper for monomial, and I think it’s a lot easier to write C and X instead.

[Alex J. Best]

docs4#MvPolynomial.pderiv is the partial derivative function by the way, and if you have explicit examples simp should be able to work out the derivative for you

[Paul Wintz]

Thank you for your responses.

@David Ang , I have tried to implement a polynomial using your suggestion, but I haven't been able to get it to work. Here is my code:

open MvPolynomial
def R := ℝ      -- Ring
def σ := Fin 2  -- Index Set
def a₁ := (2:ℝ) -- Cofficient

example : MvPolynomial σ R := C a₁ * X 0^2 * X 1^2

This produces an error:

failed to synthesize instance
  CommSemiring R

It seems like R is not the a valid type, so I tried replacing def R := ℝ with variable {R : Type _} [CommSemiring R]. This change fixes the first error but produces a different one:

typeclass instance problem is stuck, it is often due to metavariables
  HMul ((fun x => MvPolynomial ℕ ℝ) a₁) (MvPolynomial ℕ ?m.22340) (MvPolynomial σ R)Lean 4

Ultimately, I want R to be the set of reals, but I don't know how to specify that.
Any suggestions?

[David Ang]

I think you can simply replace your R with \R. Currently it says you don't have CommSemiring R and HMul because when you define R to be \R, Lean doesn't carry over all the instances from \R to R (unless e.g. you marked the definition as reducible).

[Eric Wieser]

Using abbrev R := ℝ instead of def R := ℝ would fix it

[Paul Wintz]

Thanks, that fixed my problems. I have another question, though. I expected that using σ := Fin 2, as shown below, would mean that my polynomial can only have two indeterminates, but in the following code, I define pol using four variables: X 0, X 1, X 3, and X 4. Why does this work?

open MvPolynomial

variable {R : Type _} [CommSemiring R]

abbrev σ := Fin 2  -- Index Set
def a₁ := (2:ℝ)
def a₂ := (5:ℝ)

noncomputable def pol : MvPolynomial σ ℝ := C a₁ * X 0^2 * X 1^2 + C a₂ * X 3^2 * X 4^2

[Kevin Buzzard]

That's because of the (highly dubious in my opinion) design decision to have 4 : Fin 2 make sense and I think right now it is equal to 0, although there have been other times when it's been equal to 1.

[Eric Wieser]

I don't remember it ever being equal to 1 except in Zulip messages falsely-claiming/wishing it was; but perhaps it was before I started using mathlib.

[Kevin Buzzard]

Wasn't addition once defined as "if it's bigger than n-1 then the answer is n-1"?

[Kevin Buzzard]

And then it changed to "although we have ZMod already let's just copy that"

[Eric Wieser]

Not 6 years ago in Lean 3.42 at least, or when the operations were first added

[Kevin Buzzard]

Oh apologies -- it was subtraction which was borked! Addition on Fin n and ZMod n agreed for n > 0 but not subtraction (which at some point, and possibly still, was "lift to naturals, apply borked natural subtraction, and then descend again")