Formal (multivariate) power series - Truncation

• MvPowerSeries.trunc n φ truncates a formal multivariate power series to the multivariate polynomial that has the same coefficients as φ, for all m < n, and 0 otherwise.

  Note that here, m and n have types σ →₀ ℕ, so that m < n means that m ≠ n and m s ≤ n s for all s : σ.

• MvPowerSeries.trunc_one : truncation of the unit power series

• MvPowerSeries.trunc_C : truncation of a constant

• MvPowerSeries.trunc_C_mul : truncation of constant multiple.

• MvPowerSeries.trunc' n φ truncates a formal multivariate power series to the multivariate polynomial that has the same coefficients as φ, for all m ≤ n, and 0 otherwise.

  Here, m and n have types σ →₀ ℕ so that m ≤ n means that m s ≤ n s for all s : σ.

• MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc' : compares the coefficients of a product with those of the product of truncations.

• MvPowerSeries.trunc'_one : truncation of a the unit power series.

• MvPowerSeries.trunc'_C : truncation of a constant.

• MvPowerSeries.trunc'_C_mul : truncation of a constant multiple.

• MvPowerSeries.trunc'_map : image of a truncation under a change of rings

TODO

• Unify both versions using a general purpose API

def MvPowerSeries.truncFun {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) : MvPolynomial σ R

Auxiliary definition for the truncation function.

Equations

• MvPowerSeries.truncFun n φ = ∑ m ∈ Finset.Iio n, (MvPolynomial.monomial m) ((MvPowerSeries.coeff R m) φ)

theorem MvPowerSeries.coeff_truncFun {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : MvPolynomial.coeff m (truncFun n φ) = if m < n then (coeff R m) φ else 0

def MvPowerSeries.trunc {σ : Type u_1} (R : Type u_2) [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) : MvPowerSeries σ R →+ MvPolynomial σ R

The nth truncation of a multivariate formal power series to a multivariate polynomial

If f : MvPowerSeries σ R and n : σ →₀ ℕ is a (finitely-supported) function from σ to the naturals, then trunc' R n f is the multivariable power series obtained from f by keeping only the monomials $c\prod_i X_i^{a_i}$ where a i ≤ n i for all i and $a i < n ifor somei`.

Equations

• MvPowerSeries.trunc R n = { toFun := MvPowerSeries.truncFun n, map_zero' := ⋯, map_add' := ⋯ }

theorem MvPowerSeries.coeff_trunc {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : MvPolynomial.coeff m ((trunc R n) φ) = if m < n then (coeff R m) φ else 0

@[simp]

theorem MvPowerSeries.trunc_one {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) (hnn : n ≠ 0) : (trunc R n) 1 = 1

@[simp]

theorem MvPowerSeries.trunc_C {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) (hnn : n ≠ 0) (a : R) : (trunc R n) ((C σ R) a) = MvPolynomial.C a

@[simp]

theorem MvPowerSeries.trunc_C_mul {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) (a : R) (p : MvPowerSeries σ R) : (trunc R n) ((C σ R) a * p) = MvPolynomial.C a * (trunc R n) p

@[simp]

theorem MvPowerSeries.trunc_map {σ : Type u_1} {R : Type u_2} {S : Type u_3} [DecidableEq σ] [CommSemiring R] [CommSemiring S] (n : σ →₀ ℕ) (f : R →+* S) (p : MvPowerSeries σ R) : (trunc S n) ((map σ f) p) = (MvPolynomial.map f) ((trunc R n) p)

def MvPowerSeries.truncFun' {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) : MvPolynomial σ R

Auxiliary definition for the truncation function.

Equations

• MvPowerSeries.truncFun' n φ = ∑ m ∈ Finset.Iic n, (MvPolynomial.monomial m) ((MvPowerSeries.coeff R m) φ)

theorem MvPowerSeries.coeff_truncFun' {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : MvPolynomial.coeff m (truncFun' n φ) = if m ≤ n then (coeff R m) φ else 0

Coefficients of the truncated function.

def MvPowerSeries.trunc' {σ : Type u_1} (R : Type u_2) [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) : MvPowerSeries σ R →+ MvPolynomial σ R

The nth truncation of a multivariate formal power series to a multivariate polynomial.

If f : MvPowerSeries σ R and n : σ →₀ ℕ is a (finitely-supported) function from σ to the naturals, then trunc' R n f is the multivariable power series obtained from f by keeping only the monomials $c\prod_i X_i^{a_i}$ where a i ≤ n i for all i.

Equations

• MvPowerSeries.trunc' R n = { toFun := MvPowerSeries.truncFun' n, map_zero' := ⋯, map_add' := ⋯ }

theorem MvPowerSeries.coeff_trunc' {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : MvPolynomial.coeff m ((trunc' R n) φ) = if m ≤ n then (coeff R m) φ else 0

Coefficients of the truncation of a multivariate power series.

@[simp]

theorem MvPowerSeries.trunc'_one {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) : (trunc' R n) 1 = 1

Truncation of the multivariate power series 1

@[simp]

theorem MvPowerSeries.trunc'_C {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) (a : R) : (trunc' R n) ((C σ R) a) = MvPolynomial.C a

theorem MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc' {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) (f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h : m ≤ n) : (coeff R m) (f * g) = MvPolynomial.coeff m ((trunc' R n) f * (trunc' R n) g)

Coefficients of the truncation of a product of two multivariate power series

@[simp]

theorem MvPowerSeries.trunc'_C_mul {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (n : σ →₀ ℕ) (a : R) (p : MvPowerSeries σ R) : (trunc' R n) ((C σ R) a * p) = MvPolynomial.C a * (trunc' R n) p

@[simp]

theorem MvPowerSeries.trunc'_map {σ : Type u_1} {R : Type u_2} {S : Type u_3} [DecidableEq σ] [CommSemiring R] [CommSemiring S] (n : σ →₀ ℕ) (f : R →+* S) (p : MvPowerSeries σ R) : (trunc' S n) ((map σ f) p) = (MvPolynomial.map f) ((trunc' R n) p)