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 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 weighted_order of the sum of two formal power series is the minimum of their orders if their orders differ.

• MvPowerSeries.le_weightedOrder_mul: the weighted_order 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 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 non zero 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 R d) f ≠ 0 ∧ (Finsupp.weight w) d = n

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 R 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 R 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 R 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 R 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 R 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 R d) f ≠ 0 ∧ (Finsupp.weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (Finsupp.weight w) d < n → (coeff R 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 R d) a) = if a = 0 then ⊤ else ↑((Finsupp.weight w) d)

The weighted_order 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 R d) a) = ↑((Finsupp.weight w) d)

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

theorem MvPowerSeries.min_weightedOrder_le_add {σ : 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 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) = weightedOrder w f ⊓ weightedOrder w g

The weighted_order 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 weighted_order of the product of two formal power series is at least the sum of their orders.

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 weighted_order of the product of two formal power series is at least the sum of their orders.

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 R d) (f * (1 - g)) = (coeff R 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 R d) ((1 - g) * f) = (coeff R 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) : (∀ i ∈ s, ↑((Finsupp.weight w) d) < weightedOrder w (g i)) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f

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 R d) f = 0

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 R d) f ≠ 0 ∧ d.degree = n

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

The order of a mv_power_series

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 R d) f ≠ 0 ∧ ↑d.degree = 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 R d) f ≠ 0) : f.order ≤ ↑d.degree

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 : ↑d.degree < f.order) : (coeff R 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 : σ →₀ ℕ), d.degree < n → (coeff R 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 : σ →₀ ℕ), ↑d.degree < n → (coeff R 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 R d) f ≠ 0 ∧ d.degree = n) ∧ ∀ (d : σ →₀ ℕ), d.degree < n → (coeff R 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 R d) a).order = if a = 0 then ⊤ else ↑d.degree

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 R d) a).order = ↑d.degree

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} : 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 = 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.coeff_mul_left_one_sub_of_lt_order {σ : Type u_1} {R : Type u_3} [Ring R] {f g : MvPowerSeries σ R} (d : σ →₀ ℕ) (h : ↑d.degree < g.order) : (coeff R d) (f * (1 - g)) = (coeff R 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 : ↑d.degree < g.order) : (coeff R d) ((1 - g) * f) = (coeff R 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, ↑d.degree < (g i).order) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f

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 R d) ((weightedHomogeneousComponent w p) f) = if (Finsupp.weight w) d = p then (coeff R d) f else 0

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 R d) ((homogeneousComponent p) f) = if d.degree = p then (coeff R d) f else 0