This file defines (multivariate) formal power series and develops the basic properties of these objects.
A formal power series is to a polynomial like an infinite sum is to a finite sum.
We provide the natural inclusion from polynomials to formal power series.
The file starts with setting up the (semi)ring structure on multivariate power series.
trunc n φ truncates a formal power series to the polynomial that has the same coefficients as φ, for all m ≤ n, and 0 otherwise.
If the constant coefficient of a formal power series is invertible, then this formal power series is invertible.
Formal power series over a local ring form a local ring.
We prove that if the ring of coefficients is an integral domain, then formal power series in one variable form an integral domain.
The order of a formal power series φ is the multiplicity of the variable X in φ.
If the coefficients form an integral domain, then order is a valuation (order_mul, order_add_ge).
In this file we define multivariate formal power series with variables indexed by σ and coefficients in α as mv_power_series σ α := (σ →₀ ℕ) → α. Unfortunately there is not yet enough API to show that they are the completion of the ring of multivariate polynomials. However, we provide most of the infrastructure that is needed to do this. Once I-adic completion (topological or algebraic) is available it should not be hard to fill in the details.
Formal power series in one variable are defined as power_series α := mv_power_series unit α.
This allows us to port a lot of proofs and properties from the multivariate case to the single variable case. However, it means that formal power series are indexed by (unit →₀ ℕ), which is of course canonically isomorphic to ℕ. We then build some glue to treat formal power series as if they are indexed by ℕ. Occasionally this leads to proofs that are uglier than expected.
Multivariate formal power series, where σ is the index set of the variables and α is the coefficient ring.
The nth monomial with coefficient a as multivariate formal power series.
The nth coefficient of a multivariate formal power series.
Two multivariate formal power series are equal if all their coefficients are equal.
Two multivariate formal power series are equal if and only if all their coefficients are equal.
The constant multivariate formal power series.
The variables of the multivariate formal power series ring.
The constant coefficient of a formal power series.
If a multivariate formal power series is invertible, then so is its constant coefficient.
The map between multivariate formal power series induced by a map on the coefficients.
The nth truncation of a multivariate formal power series to a multivariate polynomial
Auxiliary definition that unifies the totalised inverse formal power series (_)⁻¹ and the inverse formal power series that depends on an inverse of the constant coefficient inv_of_unit.
A multivariate formal power series is invertible if the constant coefficient is invertible.
Multivariate formal power series over a local ring form a local ring.
The natural inclusion from multivariate polynomials into multivariate formal power series.
Formal power series over the coefficient ring α.
The nth coefficient of a formal power series.
The nth monomial with coefficient a as formal power series.
Two formal power series are equal if all their coefficients are equal.
Two formal power series are equal if all their coefficients are equal.
Constructor for formal power series.
The constant coefficient of a formal power series.
The constant formal power series.
The variable of the formal power series ring.
If a formal power series is invertible, then so is its constant coefficient.
The map between formal power series induced by a map on the coefficients.
The nth truncation of a formal power series to a polynomial
A formal power series is invertible if the constant coefficient is invertible.
The ideal spanned by the variable in the power series ring over an integral domain is a prime ideal.
The variable of the power series ring over an integral domain is prime.
The order of a formal power series φ is the smallest n : enat such that X^n divides φ. The order is ⊤ if and only if φ = 0.
If the order of a formal power series is finite, then the coefficient indexed by the order is nonzero.
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.
The nth coefficient of a formal power series is 0 if n is strictly smaller than the order of the power series.
The 0 power series is the unique power series with infinite order.
The order of the 0 power series is infinite.
The order of a formal power series is at least n if the ith coefficient is 0 for all i < n.
The order of a formal power series is at least n if the ith coefficient is 0 for all i < n.
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.
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.
The order of the sum of two formal power series is at least the minimum of their orders.
The order of the sum of two formal power series is the minimum of their orders if their orders differ.
The order of the product of two formal power series is at least the sum of their orders.
The order of the monomial a*X^n is infinite if a = 0 and n otherwise.
The order of the monomial a*X^n is n if a ≠ 0.
The order of the formal power series 1 is 0.
The order of the formal power series X is 1.
The order of the formal power series X^n is n.
The order of the product of two formal power series over an integral domain is the sum of their orders.
The natural inclusion from polynomials into formal power series.