Documentation

Mathlib.RingTheory.PowerSeries.Order

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

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

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
Instances For
    source
    @[simp]
    theorem PowerSeries.order_zero {R : Type u_1} [Semiring R] :
    PowerSeries.order 0 = ⊤

    The order of the 0 power series is infinite.

    source
    theorem PowerSeries.order_finite_iff_ne_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} :
    (PowerSeries.order φ).Dom ↔ φ ≠ 0
    source
    theorem PowerSeries.coeff_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (h : (PowerSeries.order φ).Dom) :
    (PowerSeries.coeff R ((PowerSeries.order φ).get h)) φ ≠ 0

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

    source
    theorem PowerSeries.order_le {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (h : (PowerSeries.coeff R n) φ ≠ 0) :
    PowerSeries.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.

    source
    theorem PowerSeries.coeff_of_lt_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (h : ↑n < PowerSeries.order φ) :
    (PowerSeries.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.

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

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

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

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

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

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

    source
    theorem PowerSeries.order_eq_nat {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : ℕ} :
    PowerSeries.order φ = ↑n ↔ (PowerSeries.coeff R n) φ ≠ 0 ∧ ∀ i < n, (PowerSeries.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.

    source
    theorem PowerSeries.order_eq {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : PartENat} :
    PowerSeries.order φ = n ↔ (∀ (i : ℕ), ↑i = n → (PowerSeries.coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → (PowerSeries.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.

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

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

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

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

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

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

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

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

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

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

    source
    theorem PowerSeries.coeff_mul_of_lt_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} {ψ : PowerSeries R} {n : ℕ} (h : ↑n < PowerSeries.order ψ) :
    (PowerSeries.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.

    source
    theorem PowerSeries.coeff_mul_one_sub_of_lt_order {R : Type u_2} [CommRing R] {φ : PowerSeries R} {ψ : PowerSeries R} (n : ℕ) (h : ↑n < PowerSeries.order ψ) :
    (PowerSeries.coeff R n) (φ * (1 - ψ)) = (PowerSeries.coeff R n) φ
    source
    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 < PowerSeries.order (f i)) → (PowerSeries.coeff R k) (φ * Finset.prod s fun (i : ι) => 1 - f i) = (PowerSeries.coeff R k) φ
    source
    theorem PowerSeries.X_pow_order_dvd {R : Type u_1} [Semiring R] {φ : PowerSeries R} (h : (PowerSeries.order φ).Dom) :
    PowerSeries.X ^ (PowerSeries.order φ).get h ∣ φ
    source
    theorem PowerSeries.order_eq_multiplicity_X {R : Type u_2} [Semiring R] [DecidableRel fun (x x_1 : PowerSeries R) => x ∣ x_1] (φ : PowerSeries R) :
    PowerSeries.order φ = multiplicity PowerSeries.X φ
    source
    @[simp]
    theorem PowerSeries.order_one {R : Type u_1} [Semiring R] [Nontrivial R] :
    PowerSeries.order 1 = 0

    The order of the formal power series 1 is 0.

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

    The order of the formal power series X is 1.

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

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

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

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