1.16 Laurent power series
1.16.1 Motivation
Fix a commutative ring \(K\).
A binary representation of an integer \(n\) means an essentially finite sequence \(\left( b_{i}\right) _{i\in \mathbb {N}}=\left( b_{0},b_{1},b_{2},\ldots \right) \in \left\{ 0,1\right\} ^{\mathbb {N}}\) such that
(Recall that “essentially finite” means “all but finitely many \(i\in \mathbb {N}\) satisfy \(b_{i}=0\)”.)
Each \(n\in \mathbb {N}\) has a unique binary representation.
In the first formalization, the proof uses the canonical bit-index representation from Mathlib. In the second formalization, the proof proceeds by strong induction on \(n\): the least significant bit is determined by \(n \bmod 2\), and uniqueness of the remaining bits follows from the induction hypothesis applied to \(n / 2\).
A balanced ternary representation of an integer \(n\) means an essentially finite sequence \(\left( b_{i}\right) _{i\in \mathbb {N}}=\left( b_{0},b_{1},b_{2},\ldots \right) \in \left\{ 0,1,-1\right\} ^{\mathbb {N}}\) such that
- digits : ℕ → BalancedTernaryDigit
The sequence of digits
Only finitely many digits are nonzero
The sum equals n
Each integer \(n\) has a unique balanced ternary representation.
Existence. In the first formalization, existence is proved by finding \(k\) large enough that \(|n| \le M_k = 3^0 + 3^1 + \cdots + 3^k\), then using a cardinality/pigeonhole argument: the map from \(k\)-bounded representations (of which there are \(3^{k+1}\)) to the interval \(\{ m \in \mathbb {Z} : |m| \le M_k\} \) (which also has size \(3^{k+1}\)) is injective, hence surjective. In the second formalization, existence is proved by strong induction on \(|n|\): the least significant digit is determined by \(n \bmod 3\) (choosing from \(\{ -1,0,1\} \)), and the remaining digits represent \((n - d) / 3\).
Uniqueness. Both formalizations prove uniqueness by showing that if the difference \(c_i = b_i - b_i'\) of two representations satisfies \(\sum c_i \cdot 3^i = 0\) with \(c_i \in \{ -2,\ldots ,2\} \) and all but finitely many \(c_i = 0\), then all \(c_i = 0\). This is proved by induction on the highest nonzero index: \(c_0 \equiv 0 \pmod{3}\) forces \(c_0 = 0\), then dividing by \(3\) reduces to the induction hypothesis.
Let \(c : \mathbb {N} \to \mathbb {Z}\) be an essentially finite sequence with \(c_i \in \{ -2, \ldots , 2\} \) for all \(i\). If \(\sum _{i} c_i \cdot 3^i = 0\), then \(c_i = 0\) for all \(i\).
By induction on the highest nonzero index \(k\). Since \(c_0 \equiv 0 \pmod{3}\) and \(|c_0| \le 2\), we get \(c_0 = 0\). Dividing the remaining sum by \(3\) gives a shifted sequence satisfying the same hypotheses with a smaller bound, and the induction hypothesis applies.
Each integer \(n\) with \(|n| \le 3^0 + 3^1 + \cdots + 3^k\) has a unique \(k\)-bounded balanced ternary representation.
In the first formalization, this uses a cardinality argument: the number of \(k\)-bounded representations is \(3^{k+1}\), the target interval \(\{ m : |m| \le M_k\} \) also has size \(3^{k+1}\), and the evaluation map is injective (by Lemma 1.484), hence bijective. In the second formalization, uniqueness follows directly from Lemma 1.484 applied to the difference of two representations.
A balanced ternary digit is one of \(-1\), \(0\), or \(1\). There is an injection from the set of balanced ternary digits to \(\mathbb {Z}\) sending each digit to its integer value. This injection is injective, and two digits are equal if and only if their integer values are congruent modulo \(3\).
Exhaustive case analysis on the three values of a balanced ternary digit.
Every integer \(n\) has a balanced ternary representation. The proof proceeds by strong induction on \(|n|\): the least significant digit \(d\) is chosen by \(n \bmod 3\) (from \(\{ -1, 0, 1\} \)), and the remaining digits represent \((n - d)/3\), which satisfies \(|(n-d)/3| {\lt} |n|\) for \(n \ne 0\).
Base case: \(n = 0\) uses the zero representation (all digits zero). Inductive step: pick the digit \(d\) such that \(n \equiv d \pmod{3}\) with \(d \in \{ -1, 0, 1\} \), form \(m = (n - d)/3\), and prepend \(d\) to the representation of \(m\) (obtained by the induction hypothesis since \(|m| {\lt} |n|\)).
Define the partial product \(P_k = \prod _{i=0}^{k} (1 + T(3^i) + T(-3^i))\) in \(K[x^{\pm }]\). The geometric sum identity \(2 \sum _{i=0}^{k} 3^i = 3^{k+1} - 1\) is used to establish that \(P_k\) enumerates all integers in \([-M_k, M_k]\) where \(M_k = (3^{k+1}-1)/2\).
- AlgebraicCombinatorics.balancedTernaryPartialProduct K k = ∏ i ∈ Finset.range (k + 1), (1 + LaurentPolynomial.T (3 ^ i) + LaurentPolynomial.T (-3 ^ i))
The geometric sum identity is proved by induction on \(k\).
For \(M_k = \sum _{i=0}^{k} 3^i\), we have \(2 M_k + 1 = 3^{k+1}\).
By induction on \(k\).
For all \(k \ge 0\), we have \(2 \sum _{i=0}^{k-1} 3^i {\lt} 3^k\).
By induction on \(k\).
The value \(\sum _{i=0}^{k} f(i) \cdot 3^i\) of any \(k\)-bounded balanced ternary representation \(f\) (with \(f(i) \in \{ -1, 0, 1\} \)) lies in the interval \([-M_k, M_k]\).
Each term \(f(i) \cdot 3^i\) satisfies \(-3^i \le f(i) \cdot 3^i \le 3^i\), so the total sum is bounded by \(\pm \sum _{i=0}^{k} 3^i = \pm M_k\).
If two \(k\)-bounded balanced ternary representations have the same value, they must be equal. The proof uses a mod-\(3\) argument: the lowest digit is determined by the value modulo \(3\), and dividing by \(3\) reduces to the induction hypothesis.
By strong induction on \(k\). Base case (\(k = 0\)): the value equals \(f(0)\), so equality of values gives equality of digits. Inductive step: the value modulo \(3\) determines \(f(0)\) (since \(f(0) \in \{ -1, 0, 1\} \)), then dividing by \(3\) gives a \((k-1)\)-bounded problem.
A \(k\)-bounded representation \(f : \{ 0, 1, \ldots , k\} \to \mathbb {Z}\) can be converted to a finitely supported function \(\mathbb {N} \to \mathbb {Z}\) by extending with zeros. The weighted sum of the resulting function equals the \(k\)-bounded value.
- AlgebraicCombinatorics.FPS.Laurent.kBoundedToFinsupp k f = Finsupp.onFinset (Finset.range (k + 1)) (fun (i : ℕ) => if h : i < k + 1 then f ⟨i, h⟩ else 0) ⋯
The finitely supported function is constructed by extending with zeros. The sum identity follows by reindexing.
1.16.2 The space \(K\left[\left[x^{\pm }\right]\right]\)
Let \(K\left[ \left[ x^{\pm }\right] \right] \) be the \(K\)-module \(K^{\mathbb {Z}}\) of all families \(\left( a_{n}\right) _{n\in \mathbb {Z}}=\left( \ldots ,a_{-2},a_{-1},a_{0},a_{1},a_{2},\ldots \right) \) of elements of \(K\). Its addition and its scaling are defined entrywise:
An element of \(K\left[ \left[ x^{\pm }\right] \right] \) will be called a doubly infinite power series. We use the notation \(\sum _{n\in \mathbb {Z}}a_{n}x^{n}\) for a family \(\left( a_{n}\right) _{n\in \mathbb {Z}}\in K\left[ \left[ x^{\pm }\right] \right] \).
For \(n \in \mathbb {Z}\), the monomial \(x^n \in K[\! [x^{\pm }]\! ]\) is the family \((\delta _{m,n})_{m \in \mathbb {Z}}\). Its coefficient at \(m\) is \(\delta _{m,n}\). Scalar multiplication satisfies \(\lambda \cdot x^n = (\lambda \delta _{m,n})_{m \in \mathbb {Z}}\).
Immediate from the definitions.
For any \(f = (a_n) \in K[\! [x^{\pm }]\! ]\) and \(m \in \mathbb {Z}\), \(f\) evaluated at position \(m\) gives \(a_m\). Equivalently, the coefficient of \(f\) at \(m\) equals the scalar by which \(f\) scales the \(m\)-th basis vector \((\delta _{n,m})_{n \in \mathbb {Z}}\).
Immediate from the definitions.
1.16.3 Laurent polynomials
Let \(K\left[ x^{\pm }\right] \) be the \(K\)-submodule of \(K\left[ \left[ x^{\pm }\right] \right] \) consisting of all essentially finite families \(\left( a_{n}\right) _{n\in \mathbb {Z}}\). The elements of \(K\left[ x^{\pm }\right] \) are called Laurent polynomials in the indeterminate \(x\) over \(K\).
We define a multiplication on \(K\left[ x^{\pm }\right] \) by setting
The sum \(\sum _{i\in \mathbb {Z}}a_{i}b_{n-i}\) is well-defined because it is essentially finite.
We define an element \(x\in K\left[ x^{\pm }\right] \) by
In Mathlib, Laurent polynomials are represented as finitely supported functions \(\mathbb {Z} \to K\) (the group algebra of \(\mathbb {Z}\) over \(K\)).
The \(K\)-module \(K\left[ x^{\pm }\right] \), equipped with the multiplication defined above, is a commutative \(K\)-algebra. Its unity is \(\left( \delta _{i,0}\right) _{i\in \mathbb {Z}}\). The element \(x\) is invertible in this \(K\)-algebra.
The commutative ring and algebra structures are provided by Mathlib’s group algebra structure. Invertibility of \(x = T(1)\) is witnessed by \(T(-1)\): we have \(T(1) \cdot T(-1) = T(1 + (-1)) = T(0) = 1\) and similarly \(T(-1) \cdot T(1) = 1\).
For every \(n \in \mathbb {Z}\), \(T(n)\) is a unit in \(K[x^{\pm }]\) with inverse \(T(-n)\): we have \(T(n) \cdot T(-n) = 1\) and \(T(-n) \cdot T(n) = 1\).
- AlgebraicCombinatorics.laurentPolynomial_T_unit K n = { val := LaurentPolynomial.T n, inv := LaurentPolynomial.T (-n), val_inv := ⋯, inv_val := ⋯ }
By \(T(a) \cdot T(b) = T(a+b)\) and \(T(0) = 1\).
Every Laurent polynomial \(f \in K[x^{\pm }]\) can be written as \(f = \sum _{n \in \mathrm{supp}(f)} f(n) \cdot T(n)\). Moreover, \(K[x^{\pm }]\) is isomorphic to the group algebra \(K[\mathbb {Z}]\).
The decomposition follows from the fact that any finitely supported function equals the sum of its single-term components. The group algebra isomorphism is the identity on the underlying finitely supported functions \(\mathbb {Z} \to K\).
If \(a = (a_n)_{n \in \mathbb {Z}}\) is a Laurent polynomial, then \(T(1) \cdot a = (a_{n-1})_{n \in \mathbb {Z}}\) and \(T(-1) \cdot a = (a_{n+1})_{n \in \mathbb {Z}}\).
Follows from the definition of multiplication: the convolution of a single-term function with \(a\) shifts the coefficients.
For each \(k \in \mathbb {Z}\), the Laurent polynomial \(T(k)\) has coefficient \(1\) at position \(k\) and \(0\) elsewhere: \(T(k)_i = \delta _{i,k}\). Moreover, \(T(1)^k = T(k)\) for all \(k \in \mathbb {Z}\) (using integer powers via the unit structure).
The coefficient characterization follows from the fact that \(T(k)\) is the family with \(1\) at position \(k\) and \(0\) elsewhere. The power identity \(T(1)^k = T(k)\) is proved by induction on \(k\) (for \(k \geq 0\), using \(T(a) \cdot T(b) = T(a+b)\); for \(k {\lt} 0\), using the inverse \(T(-1)\)).
For any \(k \in \mathbb {Z}\) and \(n \in \mathbb {Z}\), the coefficient \([x^n] T(k)\) equals \(\delta _{n,k}\), i.e., \(1\) if \(n = k\) and \(0\) otherwise. For power series embedded into Laurent series, the coefficient at non-negative index \(n \in \mathbb {N}\) is preserved.
Follows from the fact that \(T(k)\) is the family \((\delta _{n,k})_{n \in \mathbb {Z}}\) and the definition of coefficients.
A Laurent series \(f \in K((x))\) equals the summable-family sum of the monomials \(f_n \cdot x^n\) (each being the family \((\delta _{m,n} \cdot f_n)_{m \in \mathbb {Z}}\)). This constructs an explicit summable family whose sum recovers \(f\).
Construct the summable family by sending \(n \in \mathbb {Z}\) to the monomial \(f_n \cdot x^n\). The support at any given position is a singleton (or empty), hence finite. Checking coefficients: at position \(m\), only the \(m\)-th monomial contributes.
Any doubly infinite power series \(a=\left( a_{i}\right) _{i\in \mathbb {Z}}\in K\left[ \left[ x^{\pm }\right] \right] \) satisfies
Here, the powers \(x^{i}\) are taken in the Laurent polynomial ring \(K\left[ x^{\pm }\right] \), but the infinite sum \(\sum _{i\in \mathbb {Z}}a_{i}x^{i}\) is taken in the \(K\)-module \(K\left[ \left[ x^{\pm }\right] \right] \).
For Laurent polynomials, the sum is finite and the identity holds in \(K[x^{\pm }]\) itself. For Laurent series, the identity is formalized using a summable family construction.
For Laurent polynomials, this follows from the decomposition of a finitely supported function as a sum of its single-term components. For Laurent series, the proof constructs a summable family of monomials and shows that its sum equals the original series by checking coefficients: at each position \(n\), only the \(n\)-th monomial contributes (using the coefficient characterization of \(x^k\) from Lemma 1.502 and Lemma 1.503).
1.16.4 Laurent series
We let \(K\left( \left( x\right) \right) \) be the subset of \(K\left[ \left[ x^{\pm }\right] \right] \) consisting of all families \(\left( a_{i}\right) _{i\in \mathbb {Z}}\in K\left[ \left[ x^{\pm }\right] \right] \) such that the sequence \(\left( a_{-1},a_{-2},a_{-3},\ldots \right) \) is essentially finite – i.e., such that all sufficiently low \(i\in \mathbb {Z}\) satisfy \(a_{i}=0\).
The elements of \(K\left( \left( x\right) \right) \) are called Laurent series in one indeterminate \(x\) over \(K\).
In Mathlib, Laurent series are implemented as Hahn series over \(\mathbb {Z}\) with coefficients in \(K\), which are functions \(\mathbb {Z} \to K\) whose support is well-founded (equivalently, bounded below). The formalization also provides a predicate on doubly infinite power series that captures this textbook definition.
- f.IsLaurentSeries = ∃ (N : ℤ), ∀ n < N, f.coeff n = 0
Mathlib’s Laurent series satisfy the textbook definition (the sequence of negative-indexed coefficients is essentially finite). Moreover, the conversions between doubly infinite power series satisfying this condition and Mathlib’s Laurent series are inverse to each other.
The forward direction uses the well-foundedness of the support: a Hahn series has a minimum support element (if nonempty), and all indices below it have zero coefficient. The round-trip identities hold by direct computation on coefficients.
If \(s \subseteq \mathbb {Z}\) is bounded below, then \(s\) is partially well-ordered.
Given a sequence in \(s\), shift it to \(\mathbb {N}\) by subtracting the lower bound. By Ramsey’s theorem (monotone subsequence in \(\mathbb {N}\)), extract a monotone subsequence. A strictly decreasing sequence in \(\mathbb {N}\) is impossible, so the monotone case gives the result.
The subset \(K\left( \left( x\right) \right) \) is a \(K\)-submodule of \(K\left[ \left[ x^{\pm }\right] \right] \). It has a multiplication given by the same convolution rule as \(K\left[ x^{\pm }\right] \): namely,
The sum \(\sum _{i\in \mathbb {Z}}a_{i}b_{n-i}\) is well-defined because for sufficiently low \(i\) we have \(a_i = 0\), and for sufficiently high \(i\) we have \(b_{n-i} = 0\).
Equipped with this multiplication, \(K\left( \left( x\right) \right) \) is a commutative \(K\)-algebra with unity \(\left( \delta _{i,0}\right) _{i\in \mathbb {Z}}\). The element \(x\) is invertible in this algebra.
The commutative ring and algebra structures follow from Mathlib’s Laurent series ring structure, using the agreement between our definition and Mathlib’s (Lemma 1.507). Well-definedness of the product follows from the partial well-orderedness of the support and the order multiplicativity (Lemma 1.510).
The algebra structure extends the FPS algebra via the power series embedding (Lemma 1.511) and includes Laurent polynomials via the Laurent polynomial embedding (Lemma 1.512).
Invertibility of \(x\): the element \(x = x^1\) has inverse \(x^{-1}\), since \(x^1 \cdot x^{-1} = x^{1+(-1)} = x^0 = 1\).
If \(f\) and \(g\) are Laurent series, then \(\operatorname {ord}(f) + \operatorname {ord}(g) \le \operatorname {ord}(f \cdot g)\). In particular, the coefficients of \(f \cdot g\) vanish below \(\operatorname {ord}(f) + \operatorname {ord}(g)\).
This is a standard property of Hahn series from Mathlib.
1.16.5 Embeddings
There is an injective ring homomorphism \(K\left[\left[x\right]\right] \hookrightarrow K\left(\left(x\right)\right)\) that preserves coefficients.
This is provided by Mathlib’s embedding of power series into Hahn series, which is injective.
There is an injective ring homomorphism \(K\left[x^{\pm }\right] \hookrightarrow K\left(\left(x\right)\right)\) that preserves coefficients.
- AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries p = { coeff := ⇑p, isPWO_support' := ⋯ }
In the first formalization, the map sends a finitely supported function \(p : \mathbb {Z} \to K\) to the Laurent series with the same coefficient function (whose support, being finite, is automatically bounded below). Additivity and multiplicativity are checked by comparing coefficients.
In the second formalization, the map is constructed as a ring homomorphism using the universal property of the group algebra, sending \(n \in \mathbb {Z}\) to the monomial \(x^n\) in \(K((x))\).
The embedding \(K[x^{\pm }] \hookrightarrow K((x))\) preserves addition: for Laurent polynomials \(p, q\), the image of \(p + q\) equals the sum of their images.
By checking coefficients: both sides agree at every position \(n \in \mathbb {Z}\).
The embedding sends \(0 \in K[x^{\pm }]\) to \(0 \in K((x))\) and \(1 \in K[x^{\pm }]\) to \(1 \in K((x))\).
By checking coefficients at each position.
The embedding preserves coefficients: for any Laurent polynomial \(p\) and \(n \in \mathbb {Z}\), the \(n\)-th coefficient of the image equals \(p(n)\). Moreover, \(T(n)\) maps to the monomial \(x^n\) in \(K((x))\).
Immediate from the definition of the embedding.
1.16.6 The partial product formula
In the Laurent polynomial ring,
By direct algebraic computation using \(T(a) \cdot T(b) = T(a+b)\) and the ring axioms.
For any positive integer \(i\), the power series \(1 - x^i\) is invertible in \(K\left[\left[x\right]\right]\) and hence also in \(K\left(\left(x\right)\right)\).
The constant coefficient of \(1 - x^i\) is \(1\), which is a unit. By the invertibility criterion for power series (a power series is invertible if and only if its constant coefficient is a unit), \(1 - x^i\) is invertible.
1.16.7 Laurent polynomial action and torsion
A Laurent polynomial \(p \in K[x^{\pm }]\) acts on a doubly infinite power series \(f \in K[\! [x^{\pm }]\! ]\) by the convolution formula:
- AlgebraicCombinatorics.laurentPolynomialSmul p f n = Finsupp.sum p fun (i : ℤ) (b : K) => b * f (n - i)
Well-definedness follows from the finite support of \(p\), which makes the sum finite.
The constant series \(\mathbf{1} = (1, 1, 1, \ldots ) \in K[\! [x^{\pm }]\! ]\) satisfies \((1 - x) \cdot \mathbf{1} = 0\). This shows that the \(K[x^{\pm }]\)-module \(K[\! [x^{\pm }]\! ]\) has torsion: a nonzero module element is annihilated by a nonzero ring element.
The coefficient at position \(n\) of \((1 - x) \cdot \mathbf{1}\) is \(1 \cdot 1 + (-1) \cdot 1 = 0\) (the contribution from position \(n\) minus the contribution from position \(n - 1\), both equal to \(1\)).
1.16.8 Equivalence of balanced ternary formulations
The two formulations of balanced ternary representations (the finitely-supported-function formulation and the digit-sequence formulation) are equivalent: for each \(n \in \mathbb {Z}\), the two types of balanced ternary representations of \(n\) are in bijection. The conversions are mutual inverses (up to the digit representation).
- One or more equations did not get rendered due to their size.
- r.toInductive = { digits := fun (i : ℕ) => AlgebraicCombinatorics.FPS.Laurent.btDigitOfInt (r.digits i), finite_support := ⋯, sum_eq := ⋯ }
The forward direction converts a finitely supported function with values in \(\{ -1, 0, 1\} \) to a digit sequence \(\mathbb {N} \to \{ -1, 0, 1\} \) via the natural identification. The backward direction converts a digit sequence to a finitely supported function via the integer embedding. Round-trip identities follow from the fact that the conversions between digits and integers are mutually inverse.
A balanced ternary representation is \(k\)-bounded if all digits at positions \({\gt} k\) are zero. For a \(k\)-bounded representation of \(n\), the value equals the finite sum \(\sum _{i=0}^{k} d_i \cdot 3^i\).
The predicate is \(\forall i {\gt} k,\; d_i = 0\). The sum identity follows from rewriting the infinite sum as a finite sum over \(\{ 0, \ldots , k\} \) using the vanishing of higher digits.