Laurent Power Series

This file formalizes properties of Laurent polynomials and Laurent power series, following Section \ref{sec.details.gf.laure} of the source material.

Overview

Laurent polynomials are formal sums ∑_{i ∈ ℤ} aᵢ xⁱ where only finitely many coefficients are nonzero. Laurent power series are formal sums where the sequence of negative-indexed coefficients is essentially finite (i.e., only finitely many negative powers appear).

In Mathlib:

• Laurent polynomials are LaurentPolynomial R (notation R[T;T⁻¹]), implemented as AddMonoidAlgebra R ℤ
• Laurent series are LaurentSeries R (notation R⸨X⸩), implemented as HahnSeries ℤ R

Main Results

Laurent Polynomials (Theorem thm.fps.laure.laupol-ring)

• LaurentPolynomial forms a commutative K-algebra with x invertible
• Multiplication by x shifts coefficients: x · a = (aₙ₋₁)_{n∈ℤ} (Lemma lem.fps.laure.xa)
• For each k ∈ ℤ, we have xᵏ = (δᵢ,ₖ)_{i∈ℤ} (Proposition prop.fps.laure.xk)
• Every Laurent polynomial can be written as ∑ aᵢ xⁱ (eq_sum_T)

Laurent Series (Theorem thm.fps.laure.lauser-ring)

• LaurentSeries forms a commutative K-algebra with x invertible
• The product of two Laurent series is again a Laurent series (closure under multiplication)
• Every Laurent series can be written as ∑_{i∈ℤ} aᵢ xⁱ (Proposition prop.fps.laure.a=sumaixi)

References

• Source: AlgebraicCombinatorics/tex/Details/LaurentSeries.tex
• Labels: thm.fps.laure.laupol-ring, lem.fps.laure.xa, prop.fps.laure.xk, prop.fps.laure.a=sumaixi, thm.fps.laure.lauser-ring

Section: Laurent Polynomials

A Laurent polynomial over a commutative ring K is a formal sum ∑_{i ∈ ℤ} aᵢ xⁱ where only finitely many coefficients aᵢ are nonzero.

In Mathlib, LaurentPolynomial R is defined as AddMonoidAlgebra R ℤ, i.e., finitely supported functions ℤ →₀ R. The variable is denoted T to distinguish from polynomials.

Definition: Laurent Polynomials (def.fps.laure.laupol)

This section formalizes Definition \ref{def.fps.laure.laupol} from the source material.

A Laurent polynomial over K is an essentially finite family (aₙ)_{n∈ℤ}, i.e., a function ℤ → K with finite support. The set K[x^±] of all Laurent polynomials forms a K-submodule of the doubly infinite power series K[[x^±]].

Multiplication is defined by convolution: (a · b)n = ∑{i∈ℤ} aᵢ · b_{n-i}

The indeterminate x is defined as x = (δ_{i,1})_{i∈ℤ}, i.e., the sequence with 1 at position 1 and 0 elsewhere.

In Mathlib, Laurent polynomials are represented as LaurentPolynomial K = AddMonoidAlgebra K ℤ, which is exactly ℤ →₀ K (finitely supported functions from ℤ to K). This matches the definition of essentially finite families.

@[reducible, inline]

abbrev AlgebraicCombinatorics.FPS.Laurent.LaurentPoly (K : Type u_2) [CommRing K] : Type u_2

Definition of Laurent polynomials (Definition def.fps.laure.laupol)

A Laurent polynomial over K is an essentially finite family (aₙ)_{n∈ℤ}, represented in Mathlib as LaurentPolynomial K = AddMonoidAlgebra K ℤ = ℤ →₀ K.

This definition captures the key property: only finitely many coefficients are nonzero.

Equations

• AlgebraicCombinatorics.FPS.Laurent.LaurentPoly K = LaurentPolynomial K

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_finite_support {K : Type u_1} [CommRing K] (p : LaurentPoly K) : (↑p.support).Finite

Laurent polynomials are essentially finite families: they have finite support.

def AlgebraicCombinatorics.FPS.Laurent.laurentPoly_coeff {K : Type u_1} [CommRing K] (p : LaurentPoly K) (n : ℤ) : K

The coefficient function of a Laurent polynomial.

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentPoly_coeff p n = p n

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_mul_coeff {K : Type u_1} [CommRing K] (a b : LaurentPoly K) (n : ℤ) : (a * b) n = ∑ i ∈ a.support, a i * b (n - i)

Multiplication of Laurent polynomials is convolution. (Part of Definition def.fps.laure.laupol)

The product (a · b)n = ∑{i∈ℤ} aᵢ · b_{n-i}.

In Mathlib, this is the standard multiplication on AddMonoidAlgebra K ℤ.

def AlgebraicCombinatorics.FPS.Laurent.laurentPoly_X {K : Type u_1} [CommRing K] : LaurentPoly K

The indeterminate x in Laurent polynomials. (Part of Definition def.fps.laure.laupol)

The element x = (δ_{i,1})_{i∈ℤ} is the sequence with 1 at position 1 and 0 elsewhere. In Mathlib notation, this is T 1.

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentPoly_X = LaurentPolynomial.T 1

@[simp]

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_X_coeff {K : Type u_1} [CommRing K] (n : ℤ) : laurentPoly_X n = if n = 1 then 1 else 0

The indeterminate x has coefficient 1 at position 1 and 0 elsewhere.

@[simp]

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_one_coeff {K : Type u_1} [CommRing K] (n : ℤ) : 1 n = if n = 0 then 1 else 0

The unity element in Laurent polynomials. (Part of Theorem thm.fps.laure.laupol-ring)

The unity is 1 = (δ_{i,0})_{i∈ℤ}, i.e., the sequence with 1 at position 0 and 0 elsewhere.

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_one_eq_T_zero {K : Type u_1} [CommRing K] : 1 = LaurentPolynomial.T 0

The unity element equals T(0).

def AlgebraicCombinatorics.FPS.Laurent.laurentPoly_module {K : Type u_1} [CommRing K] : Module K (LaurentPoly K)

Laurent polynomials form a K-module. (Part of Definition def.fps.laure.laupol)

The set K[x^±] is a K-submodule of K[[x^±]]. In Mathlib, this is captured by the Module instance on LaurentPolynomial.

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentPoly_module = inferInstance

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_smul_coeff {K : Type u_1} [CommRing K] (c : K) (p : LaurentPoly K) (n : ℤ) : (c • p) n = c * p n

Scalar multiplication on Laurent polynomials acts coefficientwise. (Part of Definition def.fps.laure.laupol)

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_add_coeff {K : Type u_1} [CommRing K] (p q : LaurentPoly K) (n : ℤ) : (p + q) n = p n + q n

Addition on Laurent polynomials is coefficientwise. (Part of Definition def.fps.laure.laupol)

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_zero_coeff {K : Type u_1} [CommRing K] (n : ℤ) : 0 n = 0

The zero Laurent polynomial has all coefficients zero.

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_support_finite {K : Type u_1} [CommRing K] (p : LaurentPoly K) : {n : ℤ | p n ≠ 0}.Finite

The support of a Laurent polynomial is finite. (Key property from Definition def.fps.laure.laupol)

This is the essential finiteness condition: only finitely many coefficients are nonzero.

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_support_eq {K : Type u_1} [CommRing K] (p : LaurentPoly K) : {n : ℤ | p n ≠ 0} = ↑p.support

The support of a Laurent polynomial is exactly the Finsupp support.

def AlgebraicCombinatorics.FPS.Laurent.laurentPoly_ofFinsupp {K : Type u_1} [CommRing K] (f : ℤ →₀ K) : LaurentPoly K

Construction of Laurent polynomials from finite data.

Any finitely supported function ℤ → K gives a Laurent polynomial.

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentPoly_ofFinsupp f = f

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_ofFinsupp_coeff {K : Type u_1} [CommRing K] (f : ℤ →₀ K) (n : ℤ) : (laurentPoly_ofFinsupp f) n = f n

The coefficients of a Laurent polynomial constructed from a finsupp are the same.

def AlgebraicCombinatorics.FPS.Laurent.laurentPoly_single {K : Type u_1} [CommRing K] (k : ℤ) (a : K) : LaurentPoly K

Single term Laurent polynomial.

The Laurent polynomial with a single term a · x^k is represented as Finsupp.single k a.

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentPoly_single k a = fun₀ | k => a

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_single_coeff {K : Type u_1} [CommRing K] (k : ℤ) (a : K) (n : ℤ) : (laurentPoly_single k a) n = if n = k then a else 0

The coefficient of a single-term Laurent polynomial.

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_single_eq_C_mul_T {K : Type u_1} [CommRing K] (k : ℤ) (a : K) : laurentPoly_single k a = LaurentPolynomial.C a * LaurentPolynomial.T k

A single-term Laurent polynomial equals C(a) * T(k).

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPoly_iff_essentiallyFinite {K : Type u_1} [CommRing K] (f : ℤ → K) : (∃ (p : LaurentPoly K), ∀ (n : ℤ), p n = f n) ↔ {n : ℤ | f n ≠ 0}.Finite

Laurent polynomials are the essentially finite families.

This theorem explicitly states that Laurent polynomials (as ℤ →₀ K) are exactly the essentially finite families (aₙ)_{n∈ℤ}, formalizing Definition def.fps.laure.laupol.

def AlgebraicCombinatorics.FPS.Laurent.laurentPolynomial_commRing {K : Type u_1} [CommRing K] : CommRing (LaurentPolynomial K)

Laurent polynomials form a commutative K-algebra. (Theorem thm.fps.laure.laupol-ring, label: thm.fps.laure.laupol-ring)

This is the key structural result: K[T;T⁻¹] is a commutative ring with T invertible.

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentPolynomial_commRing = inferInstance

def AlgebraicCombinatorics.FPS.Laurent.laurentPolynomial_algebra {K : Type u_1} [CommRing K] : Algebra K (LaurentPolynomial K)

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentPolynomial_algebra = inferInstance

theorem AlgebraicCombinatorics.FPS.Laurent.T_isUnit {K : Type u_1} [CommRing K] : IsUnit (LaurentPolynomial.T 1)

The variable T in Laurent polynomials is a unit (invertible). (Part of Theorem thm.fps.laure.laupol-ring)

theorem AlgebraicCombinatorics.FPS.Laurent.T_inv {K : Type u_1} [CommRing K] : LaurentPolynomial.T 1 * LaurentPolynomial.T (-1) = 1

The inverse of T is T⁻¹ = T(-1). (Part of Theorem thm.fps.laure.laupol-ring)

theorem AlgebraicCombinatorics.FPS.Laurent.T_neg_one_mul_T {K : Type u_1} [CommRing K] : LaurentPolynomial.T (-1) * LaurentPolynomial.T 1 = 1

T(-1) * T = 1. (Part of Theorem thm.fps.laure.laupol-ring)

Section: Multiplication by T shifts coefficients

This section proves the analogue of Lemma lem.fps.xa for Laurent polynomials: multiplication by T shifts coefficients by 1.

theorem AlgebraicCombinatorics.FPS.Laurent.T_mul_coeff {K : Type u_1} [CommRing K] (a : LaurentPolynomial K) (n : ℤ) : (LaurentPolynomial.T 1 * a) n = a (n - 1)

Multiplication by T shifts coefficients down by 1. (Lemma lem.fps.laure.xa, label: lem.fps.laure.xa)

If a = (aₙ)_{n∈ℤ} is a Laurent polynomial, then T · a = (aₙ₋₁)_{n∈ℤ}. In other words, the coefficient at position n in T * a equals the coefficient at position n - 1 in a.

theorem AlgebraicCombinatorics.FPS.Laurent.T_neg_one_mul_coeff {K : Type u_1} [CommRing K] (a : LaurentPolynomial K) (n : ℤ) : (LaurentPolynomial.T (-1) * a) n = a (n + 1)

Multiplication by T⁻¹ shifts coefficients up by 1. (Lemma lem.fps.laure.xa, label: lem.fps.laure.xa)

If a = (aₙ)_{n∈ℤ} is a Laurent polynomial, then T⁻¹ · a = (aₙ₊₁)_{n∈ℤ}. In other words, the coefficient at position n in T(-1) * a equals the coefficient at position n + 1 in a.

theorem AlgebraicCombinatorics.FPS.Laurent.mul_T_coeff {K : Type u_1} [CommRing K] (a : LaurentPolynomial K) (n : ℤ) : (a * LaurentPolynomial.T 1) n = a (n - 1)

Multiplication on the right by T also shifts coefficients.

theorem AlgebraicCombinatorics.FPS.Laurent.mul_T_neg_one_coeff {K : Type u_1} [CommRing K] (a : LaurentPolynomial K) (n : ℤ) : (a * LaurentPolynomial.T (-1)) n = a (n + 1)

Multiplication on the right by T⁻¹ also shifts coefficients.

Section: Powers of T

This section proves that Tᵏ = (δᵢ,ₖ)_{i∈ℤ} for all k ∈ ℤ, the analogue of Proposition prop.fps.xk for Laurent polynomials.

theorem AlgebraicCombinatorics.FPS.Laurent.T_coeff_eq {K : Type u_1} [CommRing K] (k i : ℤ) : (LaurentPolynomial.T k) i = if i = k then 1 else 0

The k-th power of T is the unit sequence at k. (Proposition prop.fps.laure.xk, label: prop.fps.laure.xk)

For each k ∈ ℤ, the Laurent polynomial T(k) has coefficient 1 at position k and 0 everywhere else.

theorem AlgebraicCombinatorics.FPS.Laurent.T_eq_single {K : Type u_1} [CommRing K] (k : ℤ) : LaurentPolynomial.T k = fun₀ | k => 1

T(k) is the Kronecker delta at k, restated.

theorem AlgebraicCombinatorics.FPS.Laurent.T_mul_T {K : Type u_1} [CommRing K] (m n : ℤ) : LaurentPolynomial.T m * LaurentPolynomial.T n = LaurentPolynomial.T (m + n)

The product T(m) * T(n) = T(m + n) follows from the group structure.

theorem AlgebraicCombinatorics.FPS.Laurent.T_one_pow {K : Type u_1} [CommRing K] (n : ℕ) : LaurentPolynomial.T 1 ^ n = LaurentPolynomial.T ↑n

For natural number powers, (T 1)^n = T n. (Part of Proposition prop.fps.laure.xk)

theorem AlgebraicCombinatorics.FPS.Laurent.T_one_zpow {K : Type u_1} [CommRing K] (k : ℤ) : ↑(⋯.unit ^ k) = LaurentPolynomial.T k

The k-th power of x equals T(k) for all integers k. (Proposition prop.fps.laure.xk, label: prop.fps.laure.xk)

This is the key result showing that x^k = (δᵢ,ₖ)_{i∈ℤ} for all k ∈ ℤ. Since T 1 represents x and T k represents the Kronecker delta at k, this theorem shows that integer powers of x give the expected sequences.

For natural number powers, this follows from T_pow. For negative powers, we use the fact that T 1 is a unit with inverse T (-1).

theorem AlgebraicCombinatorics.FPS.Laurent.T_one_zpow_coeff {K : Type u_1} [CommRing K] (k i : ℤ) : ↑(⋯.unit ^ k) i = if i = k then 1 else 0

Corollary: The coefficient of x^k at position i is δᵢ,ₖ. (Proposition prop.fps.laure.xk, restated in terms of coefficients)

Section: Representation as sums

Every Laurent polynomial can be written as a finite sum ∑ aᵢ Tⁱ.

theorem AlgebraicCombinatorics.FPS.Laurent.eq_sum_T {K : Type u_1} [CommRing K] (a : LaurentPolynomial K) : a = ∑ i ∈ a.support, LaurentPolynomial.C (a i) * LaurentPolynomial.T i

Every Laurent polynomial is a sum of monomials.

Any Laurent polynomial a can be written as ∑_{i ∈ support(a)} aᵢ · Tⁱ.

theorem AlgebraicCombinatorics.FPS.Laurent.eq_sum_single {K : Type u_1} [CommRing K] (a : LaurentPolynomial K) : a = ∑ i ∈ a.support, fun₀ | i => a i

Alternative form: every Laurent polynomial is a sum over its support.

Section: Laurent Series

Laurent series are formal power series with finitely many negative exponents. In Mathlib, they are implemented as HahnSeries ℤ R, which are functions ℤ → R with well-founded support.

The key result (Theorem thm.fps.laure.lauser-ring) is that Laurent series form a commutative K-algebra, and in particular that the product of two Laurent series is again a Laurent series.

def AlgebraicCombinatorics.FPS.Laurent.laurentSeries_commRing {K : Type u_1} [CommRing K] : CommRing (LaurentSeries K)

Laurent series form a commutative K-algebra. (Theorem thm.fps.laure.lauser-ring, label: thm.fps.laure.lauser-ring)

This is the key structural result for Laurent series.

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentSeries_commRing = inferInstance

def AlgebraicCombinatorics.FPS.Laurent.laurentSeries_algebra {K : Type u_1} [CommRing K] : Algebra K (LaurentSeries K)

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentSeries_algebra = inferInstance

theorem AlgebraicCombinatorics.FPS.Laurent.LaurentSeries_X_isUnit {K : Type u_1} [CommRing K] : IsUnit ((HahnSeries.single 1) 1)

The variable X in Laurent series (as single 1 1) is a unit.

def AlgebraicCombinatorics.FPS.Laurent.singleFamily {K : Type u_1} [CommRing K] (x : LaurentSeries K) : HahnSeries.SummableFamily ℤ K ↑(HahnSeries.support x)

A summable family of single Hahn series indexed by the support of a given Laurent series. This is used to express a Laurent series as an infinite sum of monomials.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.FPS.Laurent.laurentSeries_eq_hsum_single {K : Type u_1} [CommRing K] (x : LaurentSeries K) : x = (singleFamily x).hsum

Every Laurent series is a sum of monomials. (Proposition prop.fps.laure.a=sumaixi, label: prop.fps.laure.a=sumaixi)

Any Laurent series a can be written as ∑_{i ∈ ℤ} aᵢ · xⁱ where the sum is taken over the support of a. This is the infinite sum version of eq_sum_T for Laurent polynomials.

In Mathlib notation, we express this using SummableFamily.hsum, which represents a formal infinite sum of Hahn series.

theorem AlgebraicCombinatorics.FPS.Laurent.laurentSeries_coeff_eq_finsum_single {K : Type u_1} [CommRing K] (x : LaurentSeries K) (n : ℤ) : x.coeff n = ∑ᶠ (i : ↑(HahnSeries.support x)), ((HahnSeries.single ↑i) (x.coeff ↑i)).coeff n

The coefficient version of laurentSeries_eq_hsum_single: the n-th coefficient of a Laurent series equals the finsum of the n-th coefficients of the single monomials.

Section: Closure of Laurent Series under Multiplication

The main technical content of Theorem thm.fps.laure.lauser-ring is showing that the product of two Laurent series is again a Laurent series. This requires showing that if (a_{-1}, a_{-2}, ...) and (b_{-1}, b_{-2}, ...) are essentially finite, then so is the corresponding sequence for the product.

def AlgebraicCombinatorics.FPS.Laurent.laurentOrder {K : Type u_1} [CommRing K] (f : LaurentSeries K) : ℤ

The order of a nonzero Laurent series is the smallest index with nonzero coefficient.

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentOrder f = HahnSeries.order f

theorem AlgebraicCombinatorics.FPS.Laurent.order_mul_ge {K : Type u_1} [CommRing K] (f g : LaurentSeries K) : HahnSeries.orderTop f + HahnSeries.orderTop g ≤ HahnSeries.orderTop (f * g)

If f and g are nonzero Laurent series with orders p and q respectively, then f * g has order at least p + q.

This is the key lemma showing closure under multiplication. (Part of proof of Theorem thm.fps.laure.lauser-ring)

theorem AlgebraicCombinatorics.FPS.Laurent.coeff_mul_eq_zero_of_lt_order {K : Type u_1} [CommRing K] (f g : LaurentSeries K) (n : ℤ) (hn : n < HahnSeries.order f + HahnSeries.order g) (hf : f ≠ 0) (hg : g ≠ 0) : (f * g).coeff n = 0

The product of two Laurent series has coefficients zero below the sum of their orders.

This formalizes the key step in the proof: if aᵢ = 0 for i < p and bⱼ = 0 for j < q, then cₙ = 0 for n < p + q. (Part of proof of Theorem thm.fps.laure.lauser-ring)

Section: Embedding of Power Series into Laurent Series

Power series embed into Laurent series via the natural map that sends ∑_{n≥0} aₙ xⁿ to the same series viewed as a Laurent series with zero coefficients for negative indices.

def AlgebraicCombinatorics.FPS.Laurent.powerSeriesToLaurent {K : Type u_1} [CommRing K] : PowerSeries K →+* LaurentSeries K

Power series embed into Laurent series. (Implicit in the source material)

Equations

• AlgebraicCombinatorics.FPS.Laurent.powerSeriesToLaurent = HahnSeries.ofPowerSeries ℤ K

theorem AlgebraicCombinatorics.FPS.Laurent.powerSeriesToLaurent_injective {K : Type u_1} [CommRing K] : Function.Injective ⇑powerSeriesToLaurent

The embedding preserves the ring structure.

theorem AlgebraicCombinatorics.FPS.Laurent.coeff_powerSeriesToLaurent {K : Type u_1} [CommRing K] (f : PowerSeries K) (n : ℕ) : (powerSeriesToLaurent f).coeff ↑n = (PowerSeries.coeff n) f

Coefficients are preserved for non-negative indices.

Section: Embedding of Laurent Polynomials into Laurent Series

Laurent polynomials embed into Laurent series.

def AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries {K : Type u_1} [CommRing K] (p : LaurentPolynomial K) : LaurentSeries K

A Laurent polynomial can be viewed as a Laurent series.

This is the inclusion K[T;T⁻¹] → K⸨X⸩.

Equations

• AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries p = { coeff := ⇑p, isPWO_support' := ⋯ }

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries_add {K : Type u_1} [CommRing K] (p q : LaurentPolynomial K) : laurentPolynomialToSeries (p + q) = laurentPolynomialToSeries p + laurentPolynomialToSeries q

The embedding is additive.

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries_zero {K : Type u_1} [CommRing K] : laurentPolynomialToSeries 0 = 0

The embedding sends 0 to 0.

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries_one {K : Type u_1} [CommRing K] : laurentPolynomialToSeries 1 = 1

The embedding sends 1 to 1.

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries_mul {K : Type u_1} [CommRing K] (p q : LaurentPolynomial K) : laurentPolynomialToSeries (p * q) = laurentPolynomialToSeries p * laurentPolynomialToSeries q

The embedding is multiplicative.

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries_coeff {K : Type u_1} [CommRing K] (p : LaurentPolynomial K) (n : ℤ) : (laurentPolynomialToSeries p).coeff n = p n

The embedding preserves coefficients.

Section: Binary Representation Uniqueness

This section proves that every natural number has a unique binary representation, which is Theorem thm.fps.laure.binary-rep-uniq in the source material.

A binary representation of n ∈ ℕ is an essentially finite sequence (bᵢ)_{i ∈ ℕ} with bᵢ ∈ {0, 1} such that n = ∑_{i ∈ ℕ} bᵢ · 2^i.

In Mathlib, this is captured by the equivalence Finset.equivBitIndices : ℕ ≃ Finset ℕ, where a finset s ⊆ ℕ represents the binary sequence with bᵢ = 1 iff i ∈ s.

def AlgebraicCombinatorics.FPS.Laurent.BinaryRepresentation (n : ℕ) (s : Finset ℕ) : Prop

Binary Representation Definition.

A binary representation of n is a finset s ⊆ ℕ such that n = ∑_{i ∈ s} 2^i. This is equivalent to specifying which bits are 1 in the binary expansion.

The essentially finite sequence (bᵢ)_{i ∈ ℕ} from the textbook corresponds to bᵢ = 1 if i ∈ s, and bᵢ = 0 otherwise.

Equations

• AlgebraicCombinatorics.FPS.Laurent.BinaryRepresentation n s = (n = ∑ i ∈ s, 2 ^ i)

theorem AlgebraicCombinatorics.FPS.Laurent.exists_binaryRepresentation (n : ℕ) : ∃ (s : Finset ℕ), BinaryRepresentation n s

Every natural number has a binary representation. (Existence part of Theorem thm.fps.laure.binary-rep-uniq)

theorem AlgebraicCombinatorics.FPS.Laurent.binaryRepresentation_unique {n : ℕ} {s t : Finset ℕ} (hs : BinaryRepresentation n s) (ht : BinaryRepresentation n t) : s = t

The binary representation is unique. (Uniqueness part of Theorem thm.fps.laure.binary-rep-uniq)

theorem AlgebraicCombinatorics.FPS.Laurent.binaryRepresentation_exists_unique (n : ℕ) : ∃! s : Finset ℕ, BinaryRepresentation n s

Unique Binary Representation Theorem. (Theorem thm.fps.laure.binary-rep-uniq, label: thm.fps.laure.binary-rep-uniq)

Each natural number n has a unique binary representation. More precisely, there exists a unique finset s ⊆ ℕ such that n = ∑_{i ∈ s} 2^i.

This is a fundamental result that motivates the study of Laurent series: when trying to prove the analogous result for balanced ternary representations (where coefficients can be -1, 0, or 1), we need to work with negative powers of the base, which leads naturally to Laurent series.

def AlgebraicCombinatorics.FPS.Laurent.canonicalBinaryRep (n : ℕ) : Finset ℕ

The canonical binary representation of n is n.bitIndices.toFinset.

Equations

• AlgebraicCombinatorics.FPS.Laurent.canonicalBinaryRep n = n.bitIndices.toFinset

theorem AlgebraicCombinatorics.FPS.Laurent.canonicalBinaryRep_spec (n : ℕ) : BinaryRepresentation n (canonicalBinaryRep n)

The canonical binary representation satisfies the defining property.

theorem AlgebraicCombinatorics.FPS.Laurent.canonicalBinaryRep_eq_of_binaryRepresentation {n : ℕ} {s : Finset ℕ} (hs : BinaryRepresentation n s) : s = canonicalBinaryRep n

The canonical binary representation is the unique one.

def AlgebraicCombinatorics.FPS.Laurent.binaryRepEquiv : ℕ ≃ Finset ℕ

Bijection between ℕ and Finset ℕ via binary representation.

This equivalence maps n to its binary representation (as a finset of indices where the binary digit is 1), and conversely maps a finset s to ∑_{i ∈ s} 2^i.

This is the formalization of the bijection implicit in Theorem thm.fps.laure.binary-rep-uniq.

Equations

• AlgebraicCombinatorics.FPS.Laurent.binaryRepEquiv = Finset.equivBitIndices

theorem AlgebraicCombinatorics.FPS.Laurent.binaryRepEquiv_apply (n : ℕ) : binaryRepEquiv n = canonicalBinaryRep n

The equivalence sends n to its canonical binary representation.

theorem AlgebraicCombinatorics.FPS.Laurent.binaryRepEquiv_symm_apply (s : Finset ℕ) : binaryRepEquiv.symm s = ∑ i ∈ s, 2 ^ i

The inverse of the equivalence computes the sum ∑_{i ∈ s} 2^i.

theorem AlgebraicCombinatorics.FPS.Laurent.binaryRepEquiv_left_inv (n : ℕ) : binaryRepEquiv.symm (binaryRepEquiv n) = n

Round-trip: converting to binary representation and back gives the original number.

theorem AlgebraicCombinatorics.FPS.Laurent.binaryRepEquiv_right_inv (s : Finset ℕ) : binaryRepEquiv (binaryRepEquiv.symm s) = s

Round-trip: converting from binary representation and back gives the original finset.

Section: Balanced Ternary Representation Uniqueness

This section proves Theorem thm.fps.laure.balanced-tern-rep-uniq: Every integer has a unique balanced ternary representation.

A balanced ternary representation of an integer n is an essentially finite sequence (b_i)_{i∈ℕ} with b_i ∈ {-1, 0, 1} such that n = ∑_{i∈ℕ} b_i · 3^i.

The proof uses Laurent polynomials and the key identity: ∏_{i=0}^{k} (1 + x^{3^i} + x^{-3^i}) = ∑_{|n| ≤ M_k} x^n where M_k = 3^0 + 3^1 + ... + 3^k = (3^{k+1} - 1) / 2.

Comparing coefficients shows that each integer in [-M_k, M_k] has exactly one k-bounded balanced ternary representation. Taking k → ∞ gives the full result.

def AlgebraicCombinatorics.FPS.Laurent.btDigits : Finset ℤ

The set of balanced ternary digits {-1, 0, 1}.

Equations

• AlgebraicCombinatorics.FPS.Laurent.btDigits = {-1, 0, 1}

theorem AlgebraicCombinatorics.FPS.Laurent.btDigits_card : btDigits.card = 3

theorem AlgebraicCombinatorics.FPS.Laurent.mem_btDigits_iff (b : ℤ) : b ∈ btDigits ↔ b = -1 ∨ b = 0 ∨ b = 1

structure AlgebraicCombinatorics.FPS.Laurent.BalancedTernaryRep (n : ℤ) : Type

Balanced Ternary Representation Definition. (Definition def.fps.laure.balanced-tern, label: def.fps.laure.balanced-tern)

A balanced ternary representation of an integer n is a finitely supported function f : ℕ → ℤ with values in {-1, 0, 1} such that n = ∑_i f(i) · 3^i.

Unlike binary representations (where digits are 0 or 1), balanced ternary allows digits to be -1, 0, or 1. This enables direct representation of negative integers without a separate sign.

• digits : ℕ →₀ ℤ

  The digit function

• digits_range (i : ℕ) : self.digits i ∈ btDigits

  All digits are in {-1, 0, 1}

• sum_eq : ∑ i ∈ self.digits.support, self.digits i * 3 ^ i = n

  The value equals n

def AlgebraicCombinatorics.FPS.Laurent.balancedTernaryValue (f : ℕ →₀ ℤ) : ℤ

The value of a finitely supported balanced ternary representation.

Equations

• AlgebraicCombinatorics.FPS.Laurent.balancedTernaryValue f = ∑ i ∈ f.support, f i * 3 ^ i

def AlgebraicCombinatorics.FPS.Laurent.kBoundedBTReps (k : ℕ) : Finset (Fin (k + 1) → ℤ)

A k-bounded balanced ternary representation is a function f : Fin (k+1) → {-1, 0, 1}.

These are representations where f(i) = 0 for all i > k.

Equations

• AlgebraicCombinatorics.FPS.Laurent.kBoundedBTReps k = Fintype.piFinset fun (x : Fin (k + 1)) => AlgebraicCombinatorics.FPS.Laurent.btDigits

def AlgebraicCombinatorics.FPS.Laurent.kBoundedBTValue (k : ℕ) (f : Fin (k + 1) → ℤ) : ℤ

The value of a k-bounded balanced ternary representation.

Equations

• AlgebraicCombinatorics.FPS.Laurent.kBoundedBTValue k f = ∑ i : Fin (k + 1), f i * 3 ^ ↑i

theorem AlgebraicCombinatorics.FPS.Laurent.card_kBoundedBTReps (k : ℕ) : (kBoundedBTReps k).card = 3 ^ (k + 1)

The number of k-bounded balanced ternary representations is 3^{k+1}.

def AlgebraicCombinatorics.FPS.Laurent.maxBT (k : ℕ) : ℕ

The maximum absolute value representable with k+1 balanced ternary digits: M_k = 3^0 + 3^1 + ... + 3^k = (3^{k+1} - 1) / 2

Equations

• AlgebraicCombinatorics.FPS.Laurent.maxBT k = ∑ i ∈ Finset.range (k + 1), 3 ^ i

theorem AlgebraicCombinatorics.FPS.Laurent.maxBT_eq (k : ℕ) : 2 * maxBT k + 1 = 3 ^ (k + 1)

Key identity: 2 * M_k + 1 = 3^{k+1}.

def AlgebraicCombinatorics.FPS.Laurent.Icc_symm (M : ℕ) : Finset ℤ

The set of integers from -M to M.

Equations

• AlgebraicCombinatorics.FPS.Laurent.Icc_symm M = Finset.Icc (-↑M) ↑M

theorem AlgebraicCombinatorics.FPS.Laurent.card_Icc_symm (M : ℕ) : (Icc_symm M).card = 2 * M + 1

The cardinality of Icc (-M) M is 2M + 1.

theorem AlgebraicCombinatorics.FPS.Laurent.card_Icc_symm_maxBT (k : ℕ) : (Icc_symm (maxBT k)).card = 3 ^ (k + 1)

Cardinality of Icc_symm (maxBT k) equals 3^{k+1}.

theorem AlgebraicCombinatorics.FPS.Laurent.sum_pow_three_Fin_eq_range (k : ℕ) : ∑ i : Fin (k + 1), 3 ^ ↑i = ∑ i ∈ Finset.range (k + 1), 3 ^ i

Helper for the bounds: sum of 3^i over Fin (k+1) equals sum over range (k+1).

theorem AlgebraicCombinatorics.FPS.Laurent.kBoundedBTValue_mem_Icc (k : ℕ) (f : Fin (k + 1) → ℤ) (hf : f ∈ kBoundedBTReps k) : kBoundedBTValue k f ∈ Icc_symm (maxBT k)

The value of any k-bounded representation is in [-M_k, M_k].

theorem AlgebraicCombinatorics.FPS.Laurent.kBoundedBTValue_injective_on (k : ℕ) : Set.InjOn (kBoundedBTValue k) ↑(kBoundedBTReps k)

kBoundedBTValue is injective on kBoundedBTReps.

theorem AlgebraicCombinatorics.FPS.Laurent.kBounded_unique (k : ℕ) (n : ℤ) (hn : n ∈ Icc_symm (maxBT k)) : ∃! f : Fin (k + 1) → ℤ, f ∈ kBoundedBTReps k ∧ kBoundedBTValue k f = n

Each integer in [-M_k, M_k] has a unique k-bounded balanced ternary representation.

This is the finite version of the balanced ternary uniqueness theorem.

The proof uses a cardinality argument:

• There are 3^{k+1} k-bounded representations (card_kBoundedBTReps)
• The target set Icc_symm (maxBT k) has cardinality 3^{k+1} (card_Icc_symm_maxBT)
• Each representation maps to a value in the target set (kBoundedBTValue_mem_Icc)
• By the pigeonhole principle, the map is a bijection

(Part of Theorem thm.fps.laure.balanced-tern-rep-uniq)

noncomputable def AlgebraicCombinatorics.FPS.Laurent.kBoundedToFinsupp (k : ℕ) (f : Fin (k + 1) → ℤ) : ℕ →₀ ℤ

Helper to convert a k-bounded representation to a Finsupp.

Equations

• 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) ⋯

theorem AlgebraicCombinatorics.FPS.Laurent.kBoundedToFinsupp_apply (k : ℕ) (f : Fin (k + 1) → ℤ) (i : ℕ) (hi : i < k + 1) : (kBoundedToFinsupp k f) i = f ⟨i, hi⟩

theorem AlgebraicCombinatorics.FPS.Laurent.kBoundedToFinsupp_apply_of_ge (k : ℕ) (f : Fin (k + 1) → ℤ) (i : ℕ) (hi : k + 1 ≤ i) : (kBoundedToFinsupp k f) i = 0

theorem AlgebraicCombinatorics.FPS.Laurent.kBoundedToFinsupp_sum (k : ℕ) (f : Fin (k + 1) → ℤ) : ∑ i ∈ (kBoundedToFinsupp k f).support, (kBoundedToFinsupp k f) i * 3 ^ i = kBoundedBTValue k f

The sum over kBoundedToFinsupp equals kBoundedBTValue.

theorem AlgebraicCombinatorics.FPS.Laurent.balancedTernary_exists (n : ℤ) : Nonempty (BalancedTernaryRep n)

Every integer has a balanced ternary representation. (Existence part of Theorem thm.fps.laure.balanced-tern-rep-uniq)

For any integer n, we can find k large enough that |n| ≤ M_k, then use the k-bounded existence result.

theorem AlgebraicCombinatorics.FPS.Laurent.two_sum_lt_pow_three (k : ℕ) : 2 * ∑ i ∈ Finset.range k, 3 ^ i < 3 ^ k

Key lemma: 2 * ∑_{i<k} 3^i < 3^k.

theorem AlgebraicCombinatorics.FPS.Laurent.sum_eq_sum_support' (f : ℕ →₀ ℤ) (s : Finset ℕ) (hs : f.support ⊆ s) : ∑ i ∈ s, f i * 3 ^ i = ∑ i ∈ f.support, f i * 3 ^ i

The sum over a superset equals the sum over the support (for finitely supported functions).

theorem AlgebraicCombinatorics.FPS.Laurent.btDigits_diff_abs_ge_one {a b : ℤ} (ha : a ∈ btDigits) (hb : b ∈ btDigits) (hab : a ≠ b) : |a - b| ≥ 1

If a, b ∈ {-1, 0, 1} and a ≠ b, then |a - b| ≥ 1.

theorem AlgebraicCombinatorics.FPS.Laurent.btDigits_diff_abs_le_two {a b : ℤ} (ha : a ∈ btDigits) (hb : b ∈ btDigits) : |a - b| ≤ 2

If a, b ∈ {-1, 0, 1}, then |a - b| ≤ 2.

theorem AlgebraicCombinatorics.FPS.Laurent.btDigits_sum_unique (f g : ℕ →₀ ℤ) (hf : ∀ (i : ℕ), f i ∈ btDigits) (hg : ∀ (i : ℕ), g i ∈ btDigits) (hsum : ∑ i ∈ f.support, f i * 3 ^ i = ∑ i ∈ g.support, g i * 3 ^ i) : f = g

Two finitely supported functions with values in btDigits and the same weighted sum are equal.

theorem AlgebraicCombinatorics.FPS.Laurent.balancedTernary_unique (n : ℤ) (r1 r2 : BalancedTernaryRep n) : r1.digits = r2.digits

The balanced ternary representation is unique. (Uniqueness part of Theorem thm.fps.laure.balanced-tern-rep-uniq)

If two balanced ternary representations have the same value, they must be equal.

theorem AlgebraicCombinatorics.FPS.Laurent.balancedTernary_exists_unique (n : ℤ) : ∃! f : ℕ →₀ ℤ, (∀ (i : ℕ), f i ∈ btDigits) ∧ balancedTernaryValue f = n

Unique Balanced Ternary Representation Theorem. (Theorem thm.fps.laure.balanced-tern-rep-uniq, label: thm.fps.laure.balanced-tern-rep-uniq)

Each integer n has a unique balanced ternary representation. More precisely, there exists a unique finitely supported function f : ℕ → ℤ with values in {-1, 0, 1} such that n = ∑_{i ∈ support(f)} f(i) · 3^i.

This theorem generalizes the binary representation uniqueness to allow negative digits, which enables representing negative integers directly (without a separate sign).

The proof uses Laurent polynomials and the key identity: ∏_{i=0}^{k} (1 + x^{3^i} + x^{-3^i}) = ∑_{|n| ≤ M_k} x^n where M_k = 3^0 + 3^1 + ... + 3^k = (3^{k+1} - 1) / 2.

Comparing coefficients shows that each integer in [-M_k, M_k] has exactly one k-bounded balanced ternary representation. Taking k → ∞ gives the full result.

Historical note: Balanced ternary representations were used in the Soviet Setun computer (1960s/70s). The uniqueness theorem goes back to Fibonacci.

Section: Equivalence with Alternative Balanced Ternary Representation

This section establishes the equivalence between the BalancedTernaryRep structure defined in this file (using ℕ →₀ ℤ with btDigits constraint) and the AlgebraicCombinatorics.BalancedTernaryRepresentation structure defined in LaurentSeries.lean (using an inductive BalancedTernaryDigit type).

Both representations capture the same mathematical concept: balanced ternary representations of integers. The equivalence theorems below show that:

1. Any BalancedTernaryRepresentation can be converted to a BalancedTernaryRep
2. Any BalancedTernaryRep can be converted to a BalancedTernaryRepresentation
3. These conversions are inverses of each other (up to the digit representation)

This provides a bridge between the two equivalent formulations.

@[reducible, inline]

abbrev AlgebraicCombinatorics.FPS.Laurent.BTRep (n : ℤ) : Type

Equations

• AlgebraicCombinatorics.FPS.Laurent.BTRep = AlgebraicCombinatorics.BalancedTernaryRepresentation

@[reducible, inline]

abbrev AlgebraicCombinatorics.FPS.Laurent.BTDigit : Type

Equations

• AlgebraicCombinatorics.FPS.Laurent.BTDigit = AlgebraicCombinatorics.BalancedTernaryDigit

theorem AlgebraicCombinatorics.FPS.Laurent.BTDigit.toInt_mem_btDigits (d : BTDigit) : BalancedTernaryDigit.toInt d ∈ btDigits

The existing BalancedTernaryDigit.toInt maps into btDigits.

def AlgebraicCombinatorics.FPS.Laurent.btDigitOfInt (z : ℤ) : BTDigit

Convert an integer in btDigits to a BalancedTernaryDigit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicCombinatorics.FPS.Laurent.btDigitOfInt_toInt (z : ℤ) (hz : z ∈ btDigits) : BalancedTernaryDigit.toInt (btDigitOfInt z) = z

@[simp]

theorem AlgebraicCombinatorics.FPS.Laurent.toInt_btDigitOfInt (d : BTDigit) : btDigitOfInt (BalancedTernaryDigit.toInt d) = d

@[simp]

theorem AlgebraicCombinatorics.FPS.Laurent.btDigitOfInt_zero : btDigitOfInt 0 = BalancedTernaryDigit.zero

btDigitOfInt 0 = zero

theorem AlgebraicCombinatorics.FPS.Laurent.btDigitOfInt_ne_zero_iff (z : ℤ) (hz : z ∈ btDigits) : btDigitOfInt z ≠ 0 ↔ z ≠ 0

btDigitOfInt z ≠ 0 iff z ≠ 0 (for z ∈ btDigits)

noncomputable def AlgebraicCombinatorics.FPS.Laurent.BTRep.toFinsupp {n : ℤ} (r : BTRep n) : BalancedTernaryRep n

Convert a BTRep (inductive style from LaurentSeries.lean) to a BalancedTernaryRep (Finsupp style).

Equations

• r.toFinsupp = { digits := { support := ⋯.toFinset, toFun := fun (i : ℕ) => (r.digits i).toInt, mem_support_toFun := ⋯ }, digits_range := ⋯, sum_eq := ⋯ }

noncomputable def AlgebraicCombinatorics.FPS.Laurent.BalancedTernaryRep.toInductive {n : ℤ} (r : BalancedTernaryRep n) : BTRep n

Convert a BalancedTernaryRep (Finsupp style) to a BTRep (inductive style from LaurentSeries.lean).

Equations

• r.toInductive = { digits := fun (i : ℕ) => AlgebraicCombinatorics.FPS.Laurent.btDigitOfInt (r.digits i), finite_support := ⋯, sum_eq := ⋯ }

theorem AlgebraicCombinatorics.FPS.Laurent.BTRep.toFinsupp_toInductive_digits {n : ℤ} (r : BTRep n) : r.toFinsupp.toInductive.digits = r.digits

Round-trip equivalence: Converting from the inductive representation to Finsupp and back gives the same digits (as BalancedTernaryDigit values).

theorem AlgebraicCombinatorics.FPS.Laurent.BalancedTernaryRep.toInductive_toFinsupp_digits {n : ℤ} (r : BalancedTernaryRep n) : r.toInductive.toFinsupp.digits = r.digits

Round-trip equivalence: Converting from Finsupp representation to inductive and back gives the same digits (as integer values in the Finsupp).

theorem AlgebraicCombinatorics.FPS.Laurent.balancedTernary_representations_equiv (n : ℤ) : (∃ (x : BalancedTernaryRep n), True) ↔ ∃ (x : BTRep n), True

The two balanced ternary representations are semantically equivalent: they both represent the same integer.

noncomputable def AlgebraicCombinatorics.FPS.Laurent.balancedTernary_equiv (n : ℤ) : BalancedTernaryRep n ≃ BTRep n

Type equivalence between the two balanced ternary representations. This shows the types BalancedTernaryRep n and AlgebraicCombinatorics.BalancedTernaryRepresentation n are equivalent (bijective correspondence).

Equations

• One or more equations did not get rendered due to their size.