truncation of total degree of a multivariate power series

Stream: Is there code for X?

[Wenrong Zou]

I would like to use truncation of degree of multivariate power series. But the current truncation in mathlib is not about truncation of degree. I was wondering if anyone has done this. I was wondering whether this is a good way to do this. Here are my ideas. I am not sure which one is better. Thanks in advance!

import Mathlib

open MvPowerSeries Finset

/- `MvPowerSeries.trunc` in mathlib is defined to be truncation of some `n : σ →₀ ℕ`.
I would like to define a truncation of degree for multivariate power series (define it to be a
AddMonoidHom). -/

noncomputable section

variable {R : Type*} [CommRing R] {σ : Type*} [Fintype σ] [DecidableEq σ]

def MvPowerSeries.truncTotalDeg_aux (n : ℕ) (p : MvPowerSeries σ R) : MvPolynomial σ R :=
  ∑ m ∈ univ.finsuppAntidiag n, MvPolynomial.monomial m (coeff m p)

/- However, the homogeneous component is defined to be a multivariate power series in mathlib. -/
def MvPowerSeries.truncTotalDeg_aux' (n : ℕ) (p : MvPowerSeries σ R) : MvPowerSeries σ R :=
  ∑ m ∈ range n, homogeneousComponent m p

[Violeta Hernández]

docs#MvPowerSeries.trunc

[Violeta Hernández]

MvPowerSeries.trunc is quite a specific definition. Do we actually use it for anything?

As to the truncation you want, I think the specific definition does not matter as long as you can prove that its coefficients have the expected form.

[Wenrong Zou]

Make sense. Thanks!