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 : σ.

def MvPowerSeries.truncFun {σ : Type u_1} {R : Type u_2} [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} [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) [CommSemiring R] (n : σ →₀ ℕ) : MvPowerSeries σ R →+ MvPolynomial σ R

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

Equations

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

theorem MvPowerSeries.coeff_trunc {σ : Type u_1} {R : Type u_2} [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} [CommSemiring R] (n : σ →₀ ℕ) (hnn : n ≠ 0) : (trunc R n) 1 = 1

@[simp]

theorem MvPowerSeries.trunc_c {σ : Type u_1} {R : Type u_2} [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} [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} [CommSemiring R] [CommSemiring S] (n : σ →₀ ℕ) (f : R →+* S) (p : MvPowerSeries σ R) : (trunc S n) ((map σ f) p) = (MvPolynomial.map f) ((trunc R n) p)