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 (MvPowerSeries.truncFun n φ) = if m < n then (MvPowerSeries.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 ((MvPowerSeries.trunc R n) φ) = if m < n then (MvPowerSeries.coeff R m) φ else 0

@[simp]

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