Formal (multivariate) power series - Truncation

• MvPowerSeries.truncFinset s p restricts the support of a multivariate power series p to a finite set of monomials and obtains a multivariate polynomial.

• 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 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

def MvPowerSeries.truncFinset {σ : Type u_1} (R : Type u_4) [CommSemiring R] (s : Finset (σ →₀ ℕ)) : MvPowerSeries σ R →ₗ[R] MvPolynomial σ R

Restrict the support of a multivariate power series to a finite set of monomials and obtain a multivariate polynomial.

Equations

• MvPowerSeries.truncFinset R s = { toFun := fun (p : MvPowerSeries σ R) => ∑ x ∈ s, (MvPolynomial.monomial x) ((MvPowerSeries.coeff x) p), map_add' := ⋯, map_smul' := ⋯ }

theorem MvPowerSeries.truncFinset_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} (p : MvPowerSeries σ R) : (truncFinset R s) p = ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) p)

theorem MvPowerSeries.coeff_truncFinset_of_mem {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} {x : σ →₀ ℕ} (p : MvPowerSeries σ R) (h : x ∈ s) : MvPolynomial.coeff x ((truncFinset R s) p) = (coeff x) p

theorem MvPowerSeries.coeff_truncFinset_eq_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} {x : σ →₀ ℕ} (p : MvPowerSeries σ R) (h : x ∉ s) : MvPolynomial.coeff x ((truncFinset R s) p) = 0

theorem MvPowerSeries.coeff_truncFinset {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} [DecidableEq σ] {x : σ →₀ ℕ} (p : MvPowerSeries σ R) : MvPolynomial.coeff x ((truncFinset R s) p) = if x ∈ s then (coeff x) p else 0

theorem MvPowerSeries.truncFinset_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} {x : σ →₀ ℕ} (r : R) (h : x ∈ s) : (truncFinset R s) ((monomial x) r) = (MvPolynomial.monomial x) r

theorem MvPowerSeries.truncFinset_monomial_eq_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} {x : σ →₀ ℕ} (r : R) (h : x ∉ s) : (truncFinset R s) ((monomial x) r) = 0

theorem MvPowerSeries.truncFinset_C {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} (h : 0 ∈ s) (r : R) : (truncFinset R s) (C r) = MvPolynomial.C r

theorem MvPowerSeries.truncFinset_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} (h : 0 ∈ s) : (truncFinset R s) 1 = 1

theorem MvPowerSeries.truncFinset_truncFinset {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s t : Finset (σ →₀ ℕ)} (h : s ⊆ t) (p : MvPowerSeries σ R) : (truncFinset R s) ↑((truncFinset R t) p) = (truncFinset R s) p

theorem MvPowerSeries.truncFinset_map {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] {s : Finset (σ →₀ ℕ)} [CommSemiring S] (f : R →+* S) (p : MvPowerSeries σ R) : (truncFinset S s) ((map f) p) = (MvPolynomial.map f) ((truncFinset R s) p)

theorem MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} (hs : IsLowerSet ↑s) {x : σ →₀ ℕ} (f g : MvPowerSeries σ R) (hx : x ∈ s) : MvPolynomial.coeff x ((truncFinset R s) f * (truncFinset R s) g) = (coeff x) (f * g)

theorem MvPowerSeries.truncFinset_truncFinset_pow {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} (hs : IsLowerSet ↑s) {k : ℕ} (hk : 1 ≤ k) (p : MvPowerSeries σ R) : (truncFinset R s) (↑((truncFinset R s) p) ^ k) = (truncFinset R s) (p ^ k)

theorem MvPowerSeries.support_truncFinset_subset {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} (p : MvPowerSeries σ R) : ((truncFinset R s) p).support ⊆ s

theorem MvPowerSeries.totalDegree_truncFinset {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : Finset (σ →₀ ℕ)} (p : MvPowerSeries σ R) : ((truncFinset R s) p).totalDegree ≤ s.sup ⇑Finsupp.degree

def MvPowerSeries.trunc {σ : Type u_1} [DecidableEq σ] (R : Type u_4) [CommSemiring R] (n : σ →₀ ℕ) : MvPowerSeries σ R →ₗ[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 polynomial 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 i for some i.

Equations

• MvPowerSeries.trunc R n = MvPowerSeries.truncFinset R (Finset.Iio n)

theorem MvPowerSeries.coeff_trunc {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R) : MvPolynomial.coeff m ((trunc R n) φ) = if m < n then (coeff 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 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 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.trunc' {σ : Type u_1} [DecidableEq σ] (R : Type u_4) [CommSemiring R] (n : σ →₀ ℕ) : MvPowerSeries σ R →ₗ[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 polynomial 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 = MvPowerSeries.truncFinset R (Finset.Iic n)

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

Coefficients of the truncation of a multivariate power series.

theorem MvPowerSeries.trunc'_trunc' {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] {n m : σ →₀ ℕ} (h : n ≤ m) (φ : MvPowerSeries σ R) : (trunc' R n) ↑((trunc' R m) φ) = (trunc' R n) φ

@[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 a) = MvPolynomial.C a

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

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

@[deprecated MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul (since := "2026-02-20")]

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 m) (f * g) = MvPolynomial.coeff m ((trunc' R n) f * (trunc' R n) g)

theorem MvPowerSeries.trunc'_trunc'_pow {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] {n : σ →₀ ℕ} {k : ℕ} (hk : 1 ≤ k) (φ : MvPowerSeries σ R) : (trunc' R n) (↑((trunc' R n) φ) ^ k) = (trunc' R n) (φ ^ k)

@[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 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)

theorem MvPowerSeries.totalDegree_trunc' {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] {n : σ →₀ ℕ} (φ : MvPowerSeries σ R) : ((trunc' R n) φ).totalDegree ≤ Finsupp.degree n

theorem MvPowerSeries.ext_trunc' {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] {f g : MvPowerSeries σ R} : f = g ↔ ∀ (n : σ →₀ ℕ), (trunc' R n) f = (trunc' R n) g

theorem MvPowerSeries.eq_iff_frequently_trunc'_eq {σ : Type u_1} {R : Type u_2} [DecidableEq σ] [CommSemiring R] {f g : MvPowerSeries σ R} : f = g ↔ ∃ᶠ (m : σ →₀ ℕ) in Filter.atTop, (trunc' R m) f = (trunc' R m) g