Order of multivariate power series

We work with MvPowerSeries σ R, for Semiring R, and w : σ → ℕ.

Weighted Order

• MvPowerSeries.weightedOrder: the weighted order of a multivariate power series, with respect to w, as an element of ℕ∞.

• MvPowerSeries.weightedOrder_zero: the weighted order of 0 is 0.

• MvPowerSeries.ne_zero_iff_weightedOrder_finite: a multivariate power series is nonzero if and only if its weighted order is finite.

• MvPowerSeries.exists_coeff_ne_zero_of_weightedOrder: if the weighted order is finite, then there exists a nonzero coefficient of weight the weighted order.

• MvPowerSeries.weightedOrder_le : if a coefficient is nonzero, then the weighted order is at most the weight of that exponent.

• MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder: all coefficients of weights strictly less than the weighted order vanish.

• MvPowerSeries.weightedOrder_eq_top_iff: the weighted order of f is ⊤ if and only if f = 0.

• MvPowerSeries.nat_le_weightedOrder: if all coefficients of weight < n vanish, then the weighted order is at least n.

• MvPowerSeries.weightedOrder_eq_nat_iff: the weighted order is some integer n iff there exists a nonzero coefficient of weight n, and all coefficients of strictly smaller weight vanish.

• MvPowerSeries.weightedOrder_monomial, MvPowerSeries.weightedOrder_monomial_of_ne_zero: the weighted order of a monomial, of a monomial with nonzero coefficient.

• MvPowerSeries.min_weightedOrder_le_add: the order of the sum of two multivariate power series is at least the minimum of their orders.

• MvPowerSeries.weightedOrder_add_of_weightedOrder_ne: the weightedOrder of the sum of two formal power series is the minimum of their orders if their orders differ.

• MvPowerSeries.le_weightedOrder_mul: the weightedOrder of the product of two formal power series is at least the sum of their orders.

• MvPowerSeries.coeff_mul_left_one_sub_of_lt_weightedOrder, MvPowerSeries.coeff_mul_right_one_sub_of_lt_weightedOrder: the coefficients of f * (1 - g) and (1 - g) * f in weights strictly less than the weighted order of g.

• MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder: the coefficients of f * Π i in s, (1 - g i), in weights strictly less than the weighted orders of g i, for i ∈ s.

Order

• MvPowerSeries.order: the weighted order, for w = (1 : σ → ℕ).

• MvPowerSeries.ne_zero_iff_order_finite: f is nonzero iff its order is finite.

• MvPowerSeries.order_eq_top_iff: the order of f is infinite iff f = 0.

• MvPowerSeries.exists_coeff_ne_zero_of_order: if the order is finite, then there exists a nonzero coefficient of degree equal to the order.

• MvPowerSeries.order_le : if a coefficient of some degree is nonzero, then the order is at least that degree.

• MvPowerSeries.nat_le_order: if all coefficients of degree strictly smaller than some integer vanish, then the order is at least that integer.

• MvPowerSeries.order_eq_nat_iff: the order of a power series is an integer n iff there exists a nonzero coefficient in that degree, and all coefficients below that degree vanish.

• MvPowerSeries.order_monomial, MvPowerSeries.order_monomial_of_ne_zero: the order of a monomial, with a nonzero coefficient

• MvPowerSeries.min_order_le_add: the order of a sum of two power series is at least the minimum of their orders.

• MvPowerSeries.order_add_of_order_ne: the order of a sum of two power series of distinct orders is the minimum of their orders.

• MvPowerSeries.order_mul_ge: the order of a product of two power series is at least the sum of their orders.

• MvPowerSeries.coeff_mul_left_one_sub_of_lt_order, MvPowerSeries.coeff_mul_right_one_sub_of_lt_order: the coefficients of f * (1 - g) and (1 - g) * f below the order of g coincide with that of f.

• MvPowerSeries.coeff_mul_prod_one_sub_of_lt_order: the coefficients of f * Π i in s, (1 - g i) coincide with that of f below the minimum of the orders of the g i, for i ∈ s.

Homogeneous components

• MvPowerSeries.weightedHomogeneousComponent, MvPowerSeries.homogeneousComponent: the power series which is the sum of all monomials of given weighted degree, resp. degree.

NOTE: Under Finite σ, one can use Finsupp.finite_of_degree_le and Finsupp.finite_of_weight_le to show that they have finite support, hence correspond to MvPolynomial.

However, when σ is finite, this is not necessarily an MvPolynomial. (For example: the homogeneous components of degree 1 of the multivariate power series, all of which coefficients are 1, is the sum of all indeterminates.)

TODO: Define a coercion to MvPolynomial.

theorem MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} : f ≠ 0 ↔ ∃ (n : ℕ) (d : σ →₀ ℕ), (coeff d) f ≠ 0 ∧ (Finsupp.weight w) d = n

noncomputable def MvPowerSeries.weightedOrder {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) (f : MvPowerSeries σ R) : ℕ∞

The weighted order of a mv_power_series

Equations

• MvPowerSeries.weightedOrder w f = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)

@[simp]

theorem MvPowerSeries.weightedOrder_zero {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) : weightedOrder w 0 = ⊤

theorem MvPowerSeries.ne_zero_iff_weightedOrder_finite {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} : f ≠ 0 ↔ ↑(weightedOrder w f).toNat = weightedOrder w f

@[simp]

theorem MvPowerSeries.weightedOrder_eq_top_iff {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} : weightedOrder w f = ⊤ ↔ f = 0

The 0 power series is the unique power series with infinite order.

theorem MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} (h : ↑(weightedOrder w f).toNat = weightedOrder w f) : ∃ (d : σ →₀ ℕ), (coeff d) f ≠ 0 ∧ ↑((Finsupp.weight w) d) = weightedOrder w f

If the order of a formal power series f is finite, then some coefficient of weight equal to the order of f is nonzero.

theorem MvPowerSeries.weightedOrder_le {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : (coeff d) f ≠ 0) : weightedOrder w f ≤ ↑((Finsupp.weight w) d)

If the dth coefficient of a formal power series is nonzero, then the weighted order of the power series is less than or equal to weight d w.

theorem MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : ↑((Finsupp.weight w) d) < weightedOrder w f) : (coeff d) f = 0

The nth coefficient of a formal power series is 0 if n is strictly smaller than the order of the power series.

theorem MvPowerSeries.nat_le_weightedOrder {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {n : ℕ} (h : ∀ (d : σ →₀ ℕ), (Finsupp.weight w) d < n → (coeff d) f = 0) : ↑n ≤ weightedOrder w f

The order of a formal power series is at least n if the dth coefficient is 0 for all d such that weight w d < n.

theorem MvPowerSeries.le_weightedOrder {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {n : ℕ∞} (h : ∀ (d : σ →₀ ℕ), ↑((Finsupp.weight w) d) < n → (coeff d) f = 0) : n ≤ weightedOrder w f

The order of a formal power series is at least n if the dth coefficient is 0 for all d such that weight w d < n.

theorem MvPowerSeries.weightedOrder_eq_nat {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {n : ℕ} : weightedOrder w f = ↑n ↔ (∃ (d : σ →₀ ℕ), (coeff d) f ≠ 0 ∧ (Finsupp.weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (Finsupp.weight w) d < n → (coeff d) f = 0

The order of a formal power series is exactly n if and only if some coefficient of weight n is nonzero, and the dth coefficient is 0 for all d such that weight w d < n.

theorem MvPowerSeries.weightedOrder_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {d : σ →₀ ℕ} {a : R} [Decidable (a = 0)] : weightedOrder w ((monomial d) a) = if a = 0 then ⊤ else ↑((Finsupp.weight w) d)

The weightedOrder of the monomial a*X^d is infinite if a = 0 and weight w d otherwise.

theorem MvPowerSeries.weightedOrder_monomial_of_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {d : σ →₀ ℕ} {a : R} (h : a ≠ 0) : weightedOrder w ((monomial d) a) = ↑((Finsupp.weight w) d)

The order of the monomial a*X^n is n if a ≠ 0.

@[simp]

theorem MvPowerSeries.weightedOrder_one {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) [Nontrivial R] : weightedOrder w 1 = 0

theorem MvPowerSeries.min_weightedOrder_le_add {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R} : min (weightedOrder w f) (weightedOrder w g) ≤ weightedOrder w (f + g)

The order of the sum of two formal power series is at least the minimum of their orders.

theorem MvPowerSeries.weightedOrder_add_of_weightedOrder_ne {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R} (h : weightedOrder w f ≠ weightedOrder w g) : weightedOrder w (f + g) = min (weightedOrder w f) (weightedOrder w g)

The weightedOrder of the sum of two formal power series is the minimum of their orders if their orders differ.

theorem MvPowerSeries.le_weightedOrder_mul {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R} : weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)

The weightedOrder of the product of two formal power series is at least the sum of their orders.

theorem MvPowerSeries.le_weightedOrder_pow {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} (n : ℕ) : n • weightedOrder w f ≤ weightedOrder w (f ^ n)

theorem MvPowerSeries.le_weightedOrder_prod {σ : Type u_1} {R : Type u_3} [CommSemiring R] {ι : Type u_4} (w : σ → ℕ) (f : ι → MvPowerSeries σ R) (s : Finset ι) : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder w (∏ i ∈ s, f i)

theorem MvPowerSeries.weightedOrder_mul_ge {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R} : weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)

Alias of MvPowerSeries.le_weightedOrder_mul.

---

The weightedOrder of the product of two formal power series is at least the sum of their orders.

theorem MvPowerSeries.le_weightedOrder_smul {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {a : R} : weightedOrder w f ≤ weightedOrder w (a • f)

theorem MvPowerSeries.le_weightedOrder_map {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {S : Type u_3} [Semiring S] (φ : R →+* S) : weightedOrder w f ≤ weightedOrder w ((map φ) f)

theorem MvPowerSeries.coeff_mul_left_one_sub_of_lt_weightedOrder {σ : Type u_1} (w : σ → ℕ) {R : Type u_3} [Ring R] {f g : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : ↑((Finsupp.weight w) d) < weightedOrder w g) : (coeff d) (f * (1 - g)) = (coeff d) f

theorem MvPowerSeries.coeff_mul_right_one_sub_of_lt_weightedOrder {σ : Type u_1} (w : σ → ℕ) {R : Type u_3} [Ring R] {f g : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : ↑((Finsupp.weight w) d) < weightedOrder w g) : (coeff d) ((1 - g) * f) = (coeff d) f

theorem MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder {σ : Type u_1} (w : σ → ℕ) {R : Type u_4} {ι : Type u_5} [CommRing R] (d : σ →₀ ℕ) (s : Finset ι) (f : MvPowerSeries σ R) (g : ι → MvPowerSeries σ R) (h : ∀ i ∈ s, ↑((Finsupp.weight w) d) < weightedOrder w (g i)) : (coeff d) (f * ∏ i ∈ s, (1 - g i)) = (coeff d) f

@[simp]

theorem MvPowerSeries.weightedOrder_neg {σ : Type u_1} (w : σ → ℕ) {R : Type u_3} [Ring R] (f : MvPowerSeries σ R) : weightedOrder w (-f) = weightedOrder w f

@[simp]

theorem MvPowerSeries.weightedOrder_toSubring {σ : Type u_1} (w : σ → ℕ) {R : Type u_3} [Ring R] (p : MvPowerSeries σ R) (T : Subring R) (hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T) : weightedOrder w (p.toSubring T hp) = weightedOrder w p

@[deprecated MvPowerSeries.eq_zero_iff_forall_coeff_zero (since := "2026-01-06")]

theorem MvPowerSeries.eq_zero_iff_forall_coeff_eq_zero_and {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} : f = 0 ↔ ∀ (d : σ →₀ ℕ), (coeff d) f = 0

Alias of MvPowerSeries.eq_zero_iff_forall_coeff_zero.

theorem MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_degree {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} : f ≠ 0 ↔ ∃ (n : ℕ) (d : σ →₀ ℕ), (coeff d) f ≠ 0 ∧ Finsupp.degree d = n

noncomputable def MvPowerSeries.order {σ : Type u_1} {R : Type u_2} [Semiring R] (f : MvPowerSeries σ R) : ℕ∞

The order of an MvPowerSeries.

Equations

• f.order = MvPowerSeries.weightedOrder (fun (x : σ) => 1) f

@[simp]

theorem MvPowerSeries.order_zero {σ : Type u_1} {R : Type u_2} [Semiring R] : order 0 = ⊤

theorem MvPowerSeries.ne_zero_iff_order_finite {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} : f ≠ 0 ↔ ↑f.order.toNat = f.order

@[simp]

theorem MvPowerSeries.order_eq_top_iff {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} : f.order = ⊤ ↔ f = 0

The 0 power series is the unique power series with infinite order.

theorem MvPowerSeries.exists_coeff_ne_zero_and_order {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} (h : ↑f.order.toNat = f.order) : ∃ (d : σ →₀ ℕ), (coeff d) f ≠ 0 ∧ ↑(Finsupp.degree d) = f.order

If the order of a formal power series f is finite, then some coefficient of degree the order of f is nonzero.

theorem MvPowerSeries.order_le {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : (coeff d) f ≠ 0) : f.order ≤ ↑(Finsupp.degree d)

If the dth coefficient of a formal power series is nonzero, then the order of the power series is less than or equal to degree d.

theorem MvPowerSeries.coeff_of_lt_order {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : ↑(Finsupp.degree d) < f.order) : (coeff d) f = 0

The nth coefficient of a formal power series is 0 if n is strictly smaller than the order of the power series.

theorem MvPowerSeries.nat_le_order {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {n : ℕ} (h : ∀ (d : σ →₀ ℕ), Finsupp.degree d < n → (coeff d) f = 0) : ↑n ≤ f.order

The order of a formal power series is at least n if the dth coefficient is 0 for all d such that degree d < n.

theorem MvPowerSeries.le_order {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {n : ℕ∞} (h : ∀ (d : σ →₀ ℕ), ↑(Finsupp.degree d) < n → (coeff d) f = 0) : n ≤ f.order

The order of a formal power series is at least n if the dth coefficient is 0 for all d such that degree d < n.

theorem MvPowerSeries.order_eq_nat {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {n : ℕ} : f.order = ↑n ↔ (∃ (d : σ →₀ ℕ), (coeff d) f ≠ 0 ∧ Finsupp.degree d = n) ∧ ∀ (d : σ →₀ ℕ), Finsupp.degree d < n → (coeff d) f = 0

The order of a formal power series is exactly n some coefficient of degree n is nonzero, and the dth coefficient is 0 for all d such that degree d < n.

theorem MvPowerSeries.order_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] {d : σ →₀ ℕ} {a : R} [Decidable (a = 0)] : ((monomial d) a).order = if a = 0 then ⊤ else ↑(Finsupp.degree d)

The order of the monomial a*X^d is infinite if a = 0 and degree d otherwise.

theorem MvPowerSeries.order_monomial_of_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {d : σ →₀ ℕ} {a : R} (h : a ≠ 0) : ((monomial d) a).order = ↑(Finsupp.degree d)

The order of the monomial a*X^n is n if a ≠ 0.

theorem MvPowerSeries.min_order_le_add {σ : Type u_1} {R : Type u_2} [Semiring R] {f g : MvPowerSeries σ R} : min f.order g.order ≤ (f + g).order

The order of the sum of two formal power series is at least the minimum of their orders.

theorem MvPowerSeries.order_add_of_order_ne {σ : Type u_1} {R : Type u_2} [Semiring R] {f g : MvPowerSeries σ R} (h : f.order ≠ g.order) : (f + g).order = min f.order g.order

The order of the sum of two formal power series is the minimum of their orders if their orders differ.

theorem MvPowerSeries.le_order_mul {σ : Type u_1} {R : Type u_2} [Semiring R] {f g : MvPowerSeries σ R} : f.order + g.order ≤ (f * g).order

The order of the product of two formal power series is at least the sum of their orders.

theorem MvPowerSeries.order_mul_ge {σ : Type u_1} {R : Type u_2} [Semiring R] {f g : MvPowerSeries σ R} : f.order + g.order ≤ (f * g).order

Alias of MvPowerSeries.le_order_mul.

---

The order of the product of two formal power series is at least the sum of their orders.

theorem MvPowerSeries.le_order_pow {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} (n : ℕ) : n • f.order ≤ (f ^ n).order

theorem MvPowerSeries.le_order_prod {σ : Type u_1} {R : Type u_3} [CommSemiring R] {ι : Type u_4} (f : ι → MvPowerSeries σ R) (s : Finset ι) : ∑ i ∈ s, (f i).order ≤ (∏ i ∈ s, f i).order

theorem MvPowerSeries.one_le_order_iff_constCoeff_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} : 1 ≤ f.order ↔ constantCoeff f = 0

theorem MvPowerSeries.order_ne_zero_iff_constCoeff_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} : f.order ≠ 0 ↔ constantCoeff f = 0

theorem MvPowerSeries.le_order_pow_of_constantCoeff_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} (n : ℕ) (hf : constantCoeff f = 0) : ↑n ≤ (f ^ n).order

theorem MvPowerSeries.le_order_smul {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {a : R} : f.order ≤ (a • f).order

theorem MvPowerSeries.le_order_map {σ : Type u_1} {R : Type u_2} [Semiring R] {S : Type u_3} [Semiring S] (f : R →+* S) {φ : MvPowerSeries σ R} : φ.order ≤ ((map f) φ).order

theorem MvPowerSeries.coeff_mul_left_one_sub_of_lt_order {σ : Type u_1} {R : Type u_3} [Ring R] {f g : MvPowerSeries σ R} (d : σ →₀ ℕ) (h : ↑(Finsupp.degree d) < g.order) : (coeff d) (f * (1 - g)) = (coeff d) f

theorem MvPowerSeries.coeff_mul_right_one_sub_of_lt_order {σ : Type u_1} {R : Type u_3} [Ring R] {f g : MvPowerSeries σ R} (d : σ →₀ ℕ) (h : ↑(Finsupp.degree d) < g.order) : (coeff d) ((1 - g) * f) = (coeff d) f

theorem MvPowerSeries.coeff_mul_prod_one_sub_of_lt_order {σ : Type u_1} {R : Type u_4} {ι : Type u_5} [CommRing R] (d : σ →₀ ℕ) (s : Finset ι) (f : MvPowerSeries σ R) (g : ι → MvPowerSeries σ R) : (∀ i ∈ s, ↑(Finsupp.degree d) < (g i).order) → (coeff d) (f * ∏ i ∈ s, (1 - g i)) = (coeff d) f

@[simp]

theorem MvPowerSeries.order_neg {σ : Type u_1} {R : Type u_3} [Ring R] (f : MvPowerSeries σ R) : (-f).order = f.order

@[simp]

theorem MvPowerSeries.order_toSubring {σ : Type u_1} {R : Type u_3} [Ring R] (p : MvPowerSeries σ R) (T : Subring R) (hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T) : (p.toSubring T hp).order = p.order

def MvPowerSeries.IsWeightedHomogeneous {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) (f : MvPowerSeries σ R) (p : ℕ) : Prop

Weighted homogeneous power series

Equations

• MvPowerSeries.IsWeightedHomogeneous w f p = ∀ {d : σ →₀ ℕ}, (MvPowerSeries.coeff d) f ≠ 0 → (Finsupp.weight w) d = p

theorem MvPowerSeries.IsWeightedHomogeneous.coeff_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {w : σ → ℕ} {f : MvPowerSeries σ R} {p : ℕ} (hf : IsWeightedHomogeneous w f p) {d : σ →₀ ℕ} (hd : (Finsupp.weight w) d ≠ p) : (coeff d) f = 0

theorem MvPowerSeries.IsWeightedHomogeneous.add {σ : Type u_1} {R : Type u_2} [Semiring R] {w : σ → ℕ} {f g : MvPowerSeries σ R} {p : ℕ} (hf : IsWeightedHomogeneous w f p) (hg : IsWeightedHomogeneous w g p) : IsWeightedHomogeneous w (f + g) p

theorem MvPowerSeries.IsWeightedHomogeneous.mul {σ : Type u_1} {R : Type u_2} [Semiring R] {w : σ → ℕ} {f g : MvPowerSeries σ R} {p q : ℕ} (hf : IsWeightedHomogeneous w f p) (hg : IsWeightedHomogeneous w g q) : IsWeightedHomogeneous w (f * g) (p + q)

noncomputable def MvPowerSeries.weightedHomogeneousComponent {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) (p : ℕ) : MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R

The weighted homogeneous components of an MvPowerSeries f.

Equations

• One or more equations did not get rendered due to their size.

theorem MvPowerSeries.coeff_weightedHomogeneousComponent {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) (p : ℕ) (d : σ →₀ ℕ) (f : MvPowerSeries σ R) : (coeff d) ((weightedHomogeneousComponent w p) f) = if (Finsupp.weight w) d = p then (coeff d) f else 0

theorem MvPowerSeries.weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {w : σ → ℕ} {f : MvPowerSeries σ R} {p : ℕ} (hf : ↑p < weightedOrder w f) : (weightedHomogeneousComponent w p) f = 0

theorem MvPowerSeries.weightedHomogeneousComponent_of_weightedOrder {σ : Type u_1} {R : Type u_2} [Semiring R] {w : σ → ℕ} {f : MvPowerSeries σ R} {p : ℕ} (hf : ↑p = weightedOrder w f) : (weightedHomogeneousComponent w p) f ≠ 0

theorem MvPowerSeries.isWeightedHomogeneous_weightedHomogeneousComponent {σ : Type u_1} {R : Type u_2} [Semiring R] (w : σ → ℕ) (f : MvPowerSeries σ R) (p : ℕ) : IsWeightedHomogeneous w ((weightedHomogeneousComponent w p) f) p

theorem MvPowerSeries.isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent {σ : Type u_1} {R : Type u_2} [Semiring R] {w : σ → ℕ} {f : MvPowerSeries σ R} {p : ℕ} : IsWeightedHomogeneous w f p ↔ f = (weightedHomogeneousComponent w p) f

theorem MvPowerSeries.weightedHomogeneousComponent_mul_of_le_weightedOrder {σ : Type u_1} {R : Type u_2} [Semiring R] {w : σ → ℕ} {f g : MvPowerSeries σ R} {p q : ℕ} (hf : ↑p ≤ weightedOrder w f) (hg : ↑q ≤ weightedOrder w g) : (weightedHomogeneousComponent w (p + q)) (f * g) = (weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g

def MvPowerSeries.IsHomogeneous {σ : Type u_1} {R : Type u_2} [Semiring R] (f : MvPowerSeries σ R) (p : ℕ) : Prop

Homogeneous power series

Equations

• f.IsHomogeneous p = MvPowerSeries.IsWeightedHomogeneous 1 f p

theorem MvPowerSeries.IsHomogeneous.coeff_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {p : ℕ} (hf : f.IsHomogeneous p) {d : σ →₀ ℕ} (hd : Finsupp.degree d ≠ p) : (coeff d) f = 0

theorem MvPowerSeries.IsHomogeneous.add {σ : Type u_1} {R : Type u_2} [Semiring R] {f g : MvPowerSeries σ R} {p : ℕ} (hf : f.IsHomogeneous p) (hg : g.IsHomogeneous p) : (f + g).IsHomogeneous p

theorem MvPowerSeries.IsHomogeneous.mul {σ : Type u_1} {R : Type u_2} [Semiring R] {f g : MvPowerSeries σ R} {p q : ℕ} (hf : f.IsHomogeneous p) (hg : g.IsHomogeneous q) : (f * g).IsHomogeneous (p + q)

noncomputable def MvPowerSeries.homogeneousComponent {σ : Type u_1} {R : Type u_2} [Semiring R] (p : ℕ) : MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R

The homogeneous components of an MvPowerSeries

Equations

• MvPowerSeries.homogeneousComponent p = MvPowerSeries.weightedHomogeneousComponent 1 p

theorem MvPowerSeries.coeff_homogeneousComponent {σ : Type u_1} {R : Type u_2} [Semiring R] (p : ℕ) (d : σ →₀ ℕ) (f : MvPowerSeries σ R) : (coeff d) ((homogeneousComponent p) f) = if Finsupp.degree d = p then (coeff d) f else 0

theorem MvPowerSeries.homogeneousComponent_of_lt_order_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {p : ℕ} (hf : ↑p < f.order) : (homogeneousComponent p) f = 0

theorem MvPowerSeries.homogeneousComponent_of_order {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {p : ℕ} (hf : ↑p = f.order) : (homogeneousComponent p) f ≠ 0

theorem MvPowerSeries.isHomogeneous_homogeneousComponent {σ : Type u_1} {R : Type u_2} [Semiring R] (f : MvPowerSeries σ R) (p : ℕ) : ((homogeneousComponent p) f).IsHomogeneous p

theorem MvPowerSeries.isHomogeneous_iff_eq_homogeneousComponent {σ : Type u_1} {R : Type u_2} [Semiring R] {f : MvPowerSeries σ R} {p : ℕ} : f.IsHomogeneous p ↔ f = (homogeneousComponent p) f

theorem MvPowerSeries.homogeneousComponent_mul_of_le_order {σ : Type u_1} {R : Type u_2} [Semiring R] {f g : MvPowerSeries σ R} {p q : ℕ} (hf : ↑p ≤ f.order) (hg : ↑q ≤ g.order) : (homogeneousComponent (p + q)) (f * g) = (homogeneousComponent p) f * (homogeneousComponent q) g