Formal power series (in one variable) - Order

The PowerSeries.order of a formal power series φ is the multiplicity of the variable X in φ.

If the coefficients form an integral domain, then PowerSeries.order is an additive valuation (PowerSeries.order_mul, PowerSeries.min_order_le_order_add).

We prove that if the commutative ring R of coefficients is an integral domain, then the ring R⟦X⟧ of formal power series in one variable over R is an integral domain.

Given a non-zero power series f, divided_by_X_pow_order f is the power series obtained by dividing out the largest power of X that divides f, that is its order. This is useful when proving that R⟦X⟧ is a normalization monoid, which is done in PowerSeries.Inverse.

theorem PowerSeries.exists_coeff_ne_zero_iff_ne_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} : (∃ (n : ℕ), (coeff R n) φ ≠ 0) ↔ φ ≠ 0

def PowerSeries.order {R : Type u_1} [Semiring R] (φ : PowerSeries R) : ℕ∞

The order of a formal power series φ is the greatest n : PartENat such that X^n divides φ. The order is ⊤ if and only if φ = 0.

Equations

• φ.order = if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)

@[simp]

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

The order of the 0 power series is infinite.

theorem PowerSeries.order_finite_iff_ne_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} : φ.order < ⊤ ↔ φ ≠ 0

@[simp]

theorem PowerSeries.order_eq_top {R : Type u_1} [Semiring R] {φ : PowerSeries R} : φ.order = ⊤ ↔ φ = 0

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

theorem PowerSeries.coe_toNat_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (hf : φ ≠ 0) : ↑φ.order.toNat = φ.order

theorem PowerSeries.coeff_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (h : φ ≠ 0) : (coeff R φ.order.toNat) φ ≠ 0

If the order of a formal power series is finite, then the coefficient indexed by the order is nonzero.

theorem PowerSeries.order_le {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (h : (coeff R n) φ ≠ 0) : φ.order ≤ ↑n

If the nth coefficient of a formal power series is nonzero, then the order of the power series is less than or equal to n.

theorem PowerSeries.coeff_of_lt_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (h : ↑n < φ.order) : (coeff R n) φ = 0

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

theorem PowerSeries.coeff_of_lt_order_toNat {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (h : n < φ.order.toNat) : (coeff R n) φ = 0

theorem PowerSeries.nat_le_order {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : ℕ) (h : ∀ i < n, (coeff R i) φ = 0) : ↑n ≤ φ.order

The order of a formal power series is at least n if the ith coefficient is 0 for all i < n.

theorem PowerSeries.le_order {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : ℕ∞) (h : ∀ (i : ℕ), ↑i < n → (coeff R i) φ = 0) : n ≤ φ.order

The order of a formal power series is at least n if the ith coefficient is 0 for all i < n.

theorem PowerSeries.order_eq_nat {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : ℕ} : φ.order = ↑n ↔ (coeff R n) φ ≠ 0 ∧ ∀ i < n, (coeff R i) φ = 0

The order of a formal power series is exactly n if the nth coefficient is nonzero, and the ith coefficient is 0 for all i < n.

theorem PowerSeries.order_eq {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : ℕ∞} : φ.order = n ↔ (∀ (i : ℕ), ↑i = n → (coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → (coeff R i) φ = 0

The order of a formal power series is exactly n if the nth coefficient is nonzero, and the ith coefficient is 0 for all i < n.

theorem PowerSeries.min_order_le_order_add {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) : min φ.order ψ.order ≤ (φ + ψ).order

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

@[deprecated PowerSeries.min_order_le_order_add (since := "2024-11-12")]

theorem PowerSeries.le_order_add {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) : min φ.order ψ.order ≤ (φ + ψ).order

Alias of PowerSeries.min_order_le_order_add.

---

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

theorem PowerSeries.order_add_of_order_eq {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) (h : φ.order ≠ ψ.order) : (φ + ψ).order = min φ.order ψ.order

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

theorem PowerSeries.le_order_mul {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) : φ.order + ψ.order ≤ (φ * ψ).order

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

theorem PowerSeries.le_order_pow {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : ℕ) : n • φ.order ≤ (φ ^ n).order

theorem PowerSeries.order_mul_ge {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) : φ.order + ψ.order ≤ (φ * ψ).order

Alias of PowerSeries.le_order_mul.

---

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

theorem PowerSeries.order_monomial {R : Type u_1} [Semiring R] (n : ℕ) (a : R) [Decidable (a = 0)] : ((monomial R n) a).order = if a = 0 then ⊤ else ↑n

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

theorem PowerSeries.order_monomial_of_ne_zero {R : Type u_1} [Semiring R] (n : ℕ) (a : R) (h : a ≠ 0) : ((monomial R n) a).order = ↑n

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

theorem PowerSeries.coeff_mul_of_lt_order {R : Type u_1} [Semiring R] {φ ψ : PowerSeries R} {n : ℕ} (h : ↑n < ψ.order) : (coeff R n) (φ * ψ) = 0

If n is strictly smaller than the order of ψ, then the nth coefficient of its product with any other power series is 0.

theorem PowerSeries.coeff_mul_one_sub_of_lt_order {R : Type u_2} [Ring R] {φ ψ : PowerSeries R} (n : ℕ) (h : ↑n < ψ.order) : (coeff R n) (φ * (1 - ψ)) = (coeff R n) φ

theorem PowerSeries.coeff_mul_prod_one_sub_of_lt_order {R : Type u_2} {ι : Type u_3} [CommRing R] (k : ℕ) (s : Finset ι) (φ : PowerSeries R) (f : ι → PowerSeries R) : (∀ i ∈ s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff R k) φ

def PowerSeries.divXPowOrder {R : Type u_1} [Semiring R] (f : PowerSeries R) : PowerSeries R

Given a non-zero power series f, divXPowOrder f is the power series obtained by dividing out the largest power of X that divides f, that is its order

Equations

• f.divXPowOrder = PowerSeries.mk fun (n : ℕ) => (PowerSeries.coeff R (n + f.order.toNat)) f

@[deprecated PowerSeries.divXPowOrder (since := "2025-04-15")]

def PowerSeries.divided_by_X_pow_order {R : Type u_1} [Semiring R] (f : PowerSeries R) : PowerSeries R

Alias of PowerSeries.divXPowOrder.

---

Given a non-zero power series f, divXPowOrder f is the power series obtained by dividing out the largest power of X that divides f, that is its order

Equations

• @PowerSeries.divided_by_X_pow_order = @PowerSeries.divXPowOrder

@[simp]

theorem PowerSeries.coeff_divXPowOrder {R : Type u_1} [Semiring R] {f : PowerSeries R} {n : ℕ} : (coeff R n) f.divXPowOrder = (coeff R (n + f.order.toNat)) f

@[simp]

theorem PowerSeries.divXPowOrder_zero {R : Type u_1} [Semiring R] : divXPowOrder 0 = 0

theorem PowerSeries.constantCoeff_divXPowOrder {R : Type u_1} [Semiring R] {f : PowerSeries R} : (constantCoeff R) f.divXPowOrder = (coeff R f.order.toNat) f

theorem PowerSeries.constantCoeff_divXPowOrder_eq_zero_iff {R : Type u_1} [Semiring R] {f : PowerSeries R} : (constantCoeff R) f.divXPowOrder = 0 ↔ f = 0

theorem PowerSeries.X_pow_order_mul_divXPowOrder {R : Type u_1} [Semiring R] {f : PowerSeries R} : X ^ f.order.toNat * f.divXPowOrder = f

@[deprecated PowerSeries.X_pow_order_mul_divXPowOrder (since := "2025-04-15")]

theorem PowerSeries.self_eq_X_pow_order_mul_divided_by_X_pow_order {R : Type u_1} [Semiring R] {f : PowerSeries R} : X ^ f.order.toNat * f.divXPowOrder = f

Alias of PowerSeries.X_pow_order_mul_divXPowOrder.

theorem PowerSeries.X_pow_order_dvd {R : Type u_1} [Semiring R] {φ : PowerSeries R} : X ^ φ.order.toNat ∣ φ

theorem PowerSeries.order_eq_emultiplicity_X {R : Type u_2} [Semiring R] (φ : PowerSeries R) : φ.order = emultiplicity X φ

@[simp]

theorem PowerSeries.order_one {R : Type u_1} [Semiring R] [Nontrivial R] : order 1 = 0

The order of the formal power series 1 is 0.

theorem PowerSeries.order_zero_of_unit {R : Type u_1} [Semiring R] [Nontrivial R] {f : PowerSeries R} : IsUnit f → f.order = 0

The order of an invertible power series is 0.

@[simp]

theorem PowerSeries.order_X {R : Type u_1} [Semiring R] [Nontrivial R] : X.order = 1

The order of the formal power series X is 1.

@[simp]

theorem PowerSeries.order_X_pow {R : Type u_1} [Semiring R] [Nontrivial R] (n : ℕ) : (X ^ n).order = ↑n

The order of the formal power series X^n is n.

@[simp]

theorem PowerSeries.divXPowOrder_X {R : Type u_1} [Semiring R] [Nontrivial R] : X.divXPowOrder = 1

Dividing X by the maximal power of X dividing it leaves 1.

@[deprecated PowerSeries.divXPowOrder_X (since := "2025-04-15")]

theorem PowerSeries.divided_by_X_pow_order_of_X_eq_one {R : Type u_1} [Semiring R] [Nontrivial R] : X.divXPowOrder = 1

Alias of PowerSeries.divXPowOrder_X.

---

Dividing X by the maximal power of X dividing it leaves 1.

theorem PowerSeries.order_mul {R : Type u_1} [Semiring R] [NoZeroDivisors R] (φ ψ : PowerSeries R) : (φ * ψ).order = φ.order + ψ.order

The order of the product of two formal power series over an integral domain is the sum of their orders.

theorem PowerSeries.order_pow {R : Type u_1} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (φ : PowerSeries R) (n : ℕ) : (φ ^ n).order = n • φ.order

theorem PowerSeries.divXPowOrder_mul_divXPowOrder {R : Type u_1} [Semiring R] [NoZeroDivisors R] {f g : PowerSeries R} : f.divXPowOrder * g.divXPowOrder = (f * g).divXPowOrder

The operation of dividing a power series by the largest possible power of X preserves multiplication.

@[deprecated PowerSeries.divXPowOrder_mul_divXPowOrder (since := "2025-04-15")]

theorem PowerSeries.divided_by_X_pow_orderMul {R : Type u_1} [Semiring R] [NoZeroDivisors R] {f g : PowerSeries R} : f.divXPowOrder * g.divXPowOrder = (f * g).divXPowOrder

Alias of PowerSeries.divXPowOrder_mul_divXPowOrder.

---

The operation of dividing a power series by the largest possible power of X preserves multiplication.