Laurent Power Series

This file formalizes the content from Section sec.gf.laure of the textbook, covering Laurent power series and related concepts.

Main Definitions

• BinaryRepresentation - A binary representation of a nonnegative integer
• BalancedTernaryRepresentation - A balanced ternary representation of an integer
• DoublyInfinitePowerSeries - The K-module K[[x^±]] of all families indexed by ℤ
• DoublyInfinitePowerSeries.IsLaurentSeries - Predicate for when a doubly infinite power series is a Laurent series (Definition def.fps.laure.lauser)
• We also use Mathlib's LaurentPolynomial for K[x^±] and LaurentSeries for K((x))

Main Results

• binaryRepresentation_unique - Each n ∈ ℕ has a unique binary representation
• balancedTernaryRepresentation_unique - Each integer has a unique balanced ternary representation
• isLaurentSeries_ofLaurentSeries - Mathlib's LaurentSeries satisfies our IsLaurentSeries predicate
• toLaurentSeries_ofLaurentSeries / ofLaurentSeries_toLaurentSeries - Round-trip equivalence showing our definition matches Mathlib's
• Int.isPWO_of_bddBelow - Bounded below subsets of ℤ are partially well-ordered
• Properties of Laurent polynomials and Laurent series from Mathlib

References

• [Grinberg, Algebraic Combinatorics], Section on Laurent power series

Binary Representation

A binary representation encodes a nonnegative integer as an essentially finite sequence of bits (0 or 1).

structure AlgebraicCombinatorics.BinaryRepresentation (n : ℕ) : Type

A binary representation of a nonnegative integer n is an essentially finite sequence (b_i)_{i ∈ ℕ} of elements in {0, 1} such that n = ∑ b_i * 2^i.

This corresponds to Definition in sec.gf.laure of the source.

• bits : ℕ → Fin 2

  The sequence of bits

• finite_support : {i : ℕ | self.bits i ≠ 0}.Finite

  Only finitely many bits are nonzero

• sum_eq : ∑ᶠ (i : ℕ), ↑(self.bits i) * 2 ^ i = n

  The sum equals n

theorem AlgebraicCombinatorics.binaryRepresentation_exists (n : ℕ) : Nonempty (BinaryRepresentation n)

Every natural number has a binary representation. This is part of Theorem thm.fps.laure.binary-rep-uniq.

theorem AlgebraicCombinatorics.binaryRepresentation_unique (n : ℕ) (r₁ r₂ : BinaryRepresentation n) : r₁.bits = r₂.bits

The binary representation of a natural number is unique. This is Theorem thm.fps.laure.binary-rep-uniq.

Balanced Ternary Representation

A balanced ternary representation uses digits from {-1, 0, 1} with base 3. Unlike binary representations, this can represent negative integers.

inductive AlgebraicCombinatorics.BalancedTernaryDigit : Type

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

• negOne : BalancedTernaryDigit
• zero : BalancedTernaryDigit
• one : BalancedTernaryDigit

instance AlgebraicCombinatorics.instDecidableEqBalancedTernaryDigit : DecidableEq BalancedTernaryDigit

Equations

• AlgebraicCombinatorics.instDecidableEqBalancedTernaryDigit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance AlgebraicCombinatorics.instReprBalancedTernaryDigit : Repr BalancedTernaryDigit

Equations

• AlgebraicCombinatorics.instReprBalancedTernaryDigit = { reprPrec := AlgebraicCombinatorics.instReprBalancedTernaryDigit.repr }

def AlgebraicCombinatorics.instReprBalancedTernaryDigit.repr : BalancedTernaryDigit → ℕ → Std.Format

Equations

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

def AlgebraicCombinatorics.BalancedTernaryDigit.toInt : BalancedTernaryDigit → ℤ

Convert a balanced ternary digit to an integer

Equations

• AlgebraicCombinatorics.BalancedTernaryDigit.negOne.toInt = -1
• AlgebraicCombinatorics.BalancedTernaryDigit.zero.toInt = 0
• AlgebraicCombinatorics.BalancedTernaryDigit.one.toInt = 1

instance AlgebraicCombinatorics.BalancedTernaryDigit.instZero : Zero BalancedTernaryDigit

Equations

• AlgebraicCombinatorics.BalancedTernaryDigit.instZero = { zero := AlgebraicCombinatorics.BalancedTernaryDigit.zero }

@[simp]

theorem AlgebraicCombinatorics.BalancedTernaryDigit.toInt_zero : toInt 0 = 0

theorem AlgebraicCombinatorics.BalancedTernaryDigit.toInt_injective : Function.Injective toInt

Different digits have different integer values

theorem AlgebraicCombinatorics.BalancedTernaryDigit.toInt_range (d : BalancedTernaryDigit) : -1 ≤ d.toInt ∧ d.toInt ≤ 1

The range of toInt is {-1, 0, 1}

theorem AlgebraicCombinatorics.BalancedTernaryDigit.toInt_mod_three_injective : Function.Injective fun (d : BalancedTernaryDigit) => d.toInt % 3

Different digits have different residues mod 3

theorem AlgebraicCombinatorics.BalancedTernaryDigit.eq_of_toInt_mod_three_eq (a b : BalancedTernaryDigit) (h : a.toInt % 3 = b.toInt % 3) : a = b

structure AlgebraicCombinatorics.BalancedTernaryRepresentation (n : ℤ) : Type

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

This corresponds to the Definition of balanced ternary representation in sec.gf.laure.

• digits : ℕ → BalancedTernaryDigit

  The sequence of digits

• finite_support : {i : ℕ | self.digits i ≠ 0}.Finite

  Only finitely many digits are nonzero

• sum_eq : ∑ᶠ (i : ℕ), (self.digits i).toInt * 3 ^ i = n

  The sum equals n

Helper definitions and lemmas for balanced ternary existence proof

theorem AlgebraicCombinatorics.BalancedTernaryDigit.ne_zero_iff_toInt_ne_zero (d : BalancedTernaryDigit) : d ≠ 0 ↔ d.toInt ≠ 0

A digit is nonzero iff its toInt is nonzero

theorem AlgebraicCombinatorics.balancedTernaryRepresentation_exists (n : ℤ) : Nonempty (BalancedTernaryRepresentation n)

Every integer has a balanced ternary representation. This is part of Theorem thm.fps.laure.balanced-tern-rep-uniq.

theorem AlgebraicCombinatorics.balancedTernaryRepresentation_unique (n : ℤ) (r₁ r₂ : BalancedTernaryRepresentation n) : r₁.digits = r₂.digits

The balanced ternary representation of an integer is unique. This is Theorem thm.fps.laure.balanced-tern-rep-uniq.

Doubly Infinite Power Series

The K-module K[[x^±]] of all families (a_n)_{n ∈ ℤ} of elements of K. This is the largest space allowing negative powers of x, but it does not have a well-defined multiplication in general.

This corresponds to Definition def.fps.laure.double.

def AlgebraicCombinatorics.DoublyInfinitePowerSeries (K : Type u_1) [Semiring K] : Type u_1

The K-module of doubly infinite power series K[[x^±]].

An element is a family (a_n)_{n ∈ ℤ} of elements of K. Addition and scalar multiplication are defined entrywise.

Note: This is NOT a ring because multiplication is not always well-defined (the convolution sum may be infinite).

This corresponds to Definition def.fps.laure.double.

Equations

• AlgebraicCombinatorics.DoublyInfinitePowerSeries K = (ℤ → K)

instance AlgebraicCombinatorics.DoublyInfinitePowerSeries.instAddCommMonoid {K : Type u_1} [Semiring K] : AddCommMonoid (DoublyInfinitePowerSeries K)

Equations

• AlgebraicCombinatorics.DoublyInfinitePowerSeries.instAddCommMonoid = Pi.addCommMonoid

instance AlgebraicCombinatorics.DoublyInfinitePowerSeries.instModule {K : Type u_1} [Semiring K] : Module K (DoublyInfinitePowerSeries K)

Equations

• AlgebraicCombinatorics.DoublyInfinitePowerSeries.instModule = Pi.module ℤ (fun (a : ℤ) => K) K

def AlgebraicCombinatorics.DoublyInfinitePowerSeries.coeff {K : Type u_1} [Semiring K] (f : DoublyInfinitePowerSeries K) (n : ℤ) : K

The coefficient of x^n in a doubly infinite power series

Equations

• f.coeff n = f n

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.ext {K : Type u_1} [Semiring K] {f g : DoublyInfinitePowerSeries K} (h : ∀ (n : ℤ), f.coeff n = g.coeff n) : f = g

Two doubly infinite power series are equal iff all their coefficients are equal

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.ext_iff {K : Type u_1} [Semiring K] {f g : DoublyInfinitePowerSeries K} : f = g ↔ ∀ (n : ℤ), f.coeff n = g.coeff n

@[simp]

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.coeff_add {K : Type u_1} [Semiring K] (f g : DoublyInfinitePowerSeries K) (n : ℤ) : (f + g).coeff n = f.coeff n + g.coeff n

@[simp]

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.coeff_smul {K : Type u_1} [Semiring K] (r : K) (f : DoublyInfinitePowerSeries K) (n : ℤ) : (r • f).coeff n = r * f.coeff n

def AlgebraicCombinatorics.DoublyInfinitePowerSeries.single {K : Type u_1} [Semiring K] (n : ℤ) : DoublyInfinitePowerSeries K

The element x^n in K[[x^±]], represented as a family

Equations

• AlgebraicCombinatorics.DoublyInfinitePowerSeries.single n m = if m = n then 1 else 0

@[simp]

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.coeff_single {K : Type u_1} [Semiring K] (n m : ℤ) : (single n).coeff m = if m = n then 1 else 0

@[simp]

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.coeff_zero {K : Type u_1} [Semiring K] (n : ℤ) : coeff 0 n = 0

The zero element of K[[x^±]] has all coefficients zero. This is part of Definition def.fps.laure.double.

@[simp]

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.single_zero_eq_one {K : Type u_1} [Semiring K] : single 0 = fun (n : ℤ) => if n = 0 then 1 else 0

The single at 0 with coefficient 1 represents 1 (as a constant series).

@[simp]

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.coeff_single_self {K : Type u_1} [Semiring K] (n : ℤ) : (single n).coeff n = 1

Coefficient of single n at n is 1.

@[simp]

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.coeff_single_ne {K : Type u_1} [Semiring K] {n m : ℤ} (h : m ≠ n) : (single n).coeff m = 0

Coefficient of single n at m ≠ n is 0.

@[simp]

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.smul_single {K : Type u_1} [Semiring K] (r : K) (n : ℤ) : r • single n = fun (m : ℤ) => if m = n then r else 0

Scalar multiplication of single.

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.eq_coeff_at_position {K : Type u_1} [Semiring K] (f : DoublyInfinitePowerSeries K) (m : ℤ) : f m = f.coeff m

Any doubly infinite power series f equals (coeff f n) at position n. This is the pointwise characterization of the notation ∑_{n∈ℤ} a_n x^n: at each position m, the coefficient is a_m.

This formalizes the representation mentioned at the end of Definition def.fps.laure.double: "we will later use the notation ∑{n∈ℤ} a_n x^n for a family (a_n){n∈ℤ}".

Note: This is a formal identity of families. The "sum" is well-defined because at each coefficient position m, only the term n = m contributes.

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.coeff_eq_single_contrib {K : Type u_1} [Semiring K] (f : DoublyInfinitePowerSeries K) (m : ℤ) : f.coeff m = f.coeff m * (single m).coeff m

The representation f = ∑{n∈ℤ} (coeff f n) · x^n holds pointwise: at position m, f m = (coeff f m) · 1 + ∑{n≠m} (coeff f n) · 0 = coeff f m.

def AlgebraicCombinatorics.DoublyInfinitePowerSeries.IsLaurentSeries {K : Type u_1} [Semiring K] (f : DoublyInfinitePowerSeries K) : Prop

A doubly infinite power series is a Laurent series if the sequence of negative coefficients (a_{-1}, a_{-2}, a_{-3}, ...) is essentially finite, i.e., all sufficiently negative indices have zero coefficient.

This is Definition def.fps.laure.lauser from the textbook: We let K((x)) be the subset of K[[x^±]] consisting of all families (a_i){i∈ℤ} such that the sequence (a{-1}, a_{-2}, a_{-3}, ...) is essentially finite -- i.e., such that all sufficiently low i ∈ ℤ satisfy a_i = 0.

The elements of K((x)) are called Laurent series in one indeterminate x over K.

Equations

• f.IsLaurentSeries = ∃ (N : ℤ), ∀ n < N, f.coeff n = 0

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.IsLaurentSeries.support_bddBelow {K : Type u_1} [Semiring K] {f : DoublyInfinitePowerSeries K} (hf : f.IsLaurentSeries) : BddBelow {n : ℤ | f.coeff n ≠ 0}

The support of a Laurent series is bounded below.

def AlgebraicCombinatorics.DoublyInfinitePowerSeries.ofLaurentSeries {K : Type u_1} [Semiring K] (f : LaurentSeries K) : DoublyInfinitePowerSeries K

Convert a Mathlib LaurentSeries to a DoublyInfinitePowerSeries

Equations

• AlgebraicCombinatorics.DoublyInfinitePowerSeries.ofLaurentSeries f n = f.coeff n

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.isLaurentSeries_ofLaurentSeries {K : Type u_1} [Semiring K] (f : LaurentSeries K) : (ofLaurentSeries f).IsLaurentSeries

A Mathlib LaurentSeries satisfies our IsLaurentSeries predicate.

This shows that Mathlib's definition of LaurentSeries (as HahnSeries ℤ K) matches the textbook Definition def.fps.laure.lauser.

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.Int.isPWO_of_bddBelow {s : Set ℤ} (hs : BddBelow s) : s.IsPWO

For ℤ, a set bounded below is partially well-ordered.

This follows from the fact that any sequence in ℤ bounded below has a monotone subsequence (by Ramsey's theorem / infinite pigeonhole).

def AlgebraicCombinatorics.DoublyInfinitePowerSeries.toLaurentSeries {K : Type u_1} [Semiring K] (f : DoublyInfinitePowerSeries K) (hf : f.IsLaurentSeries) : LaurentSeries K

Convert a DoublyInfinitePowerSeries satisfying IsLaurentSeries to a Mathlib LaurentSeries

Equations

• f.toLaurentSeries hf = { coeff := fun (n : ℤ) => f.coeff n, isPWO_support' := ⋯ }

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.toLaurentSeries_ofLaurentSeries {K : Type u_1} [Semiring K] (f : LaurentSeries K) : (ofLaurentSeries f).toLaurentSeries ⋯ = f

The round-trip from LaurentSeries to DoublyInfinitePowerSeries and back gives the same series

theorem AlgebraicCombinatorics.DoublyInfinitePowerSeries.ofLaurentSeries_toLaurentSeries {K : Type u_1} [Semiring K] (f : DoublyInfinitePowerSeries K) (hf : f.IsLaurentSeries) : ofLaurentSeries (f.toLaurentSeries hf) = f

The round-trip from DoublyInfinitePowerSeries to LaurentSeries and back gives the same function

Laurent Polynomials

The K-algebra K[x^±] of Laurent polynomials consists of essentially finite families (a_n)_{n ∈ ℤ}. Unlike K[[x^±]], this IS a ring.

We use Mathlib's LaurentPolynomial which is defined as AddMonoidAlgebra R ℤ.

This corresponds to Definition def.fps.laure.laupol.

Theorem thm.fps.laure.laupol-ring

The K-module K[x^±], equipped with the convolution multiplication, is a commutative K-algebra. Its unity is (δ_{i,0})_{i∈ℤ}. The element x (represented as T 1) is invertible in this K-algebra.

This is fully formalized below using Mathlib's LaurentPolynomial type.

Part 1: K[x^±] is a commutative K-algebra

The Laurent polynomial ring K[x^±] is a commutative semiring (and a commutative ring when K is a ring). It is also a K-algebra.

In Mathlib, this is established via AddMonoidAlgebra.instCommSemiring and related instances.

instance AlgebraicCombinatorics.laurentPolynomial_commSemiring (K : Type u_1) [CommSemiring K] : CommSemiring (LaurentPolynomial K)

Laurent polynomials form a commutative semiring. This is part of Theorem thm.fps.laure.laupol-ring.

Equations

• AlgebraicCombinatorics.laurentPolynomial_commSemiring K = inferInstance

instance AlgebraicCombinatorics.laurentPolynomial_algebra (K : Type u_1) [CommSemiring K] : Algebra K (LaurentPolynomial K)

Laurent polynomials form a K-algebra. This is part of Theorem thm.fps.laure.laupol-ring.

Equations

• AlgebraicCombinatorics.laurentPolynomial_algebra K = inferInstance

Part 2: The unity is (δ_{i,0})_{i∈ℤ}

The multiplicative identity in K[x^±] is the family that is 1 at index 0 and 0 elsewhere. In Mathlib, this is LaurentPolynomial.T 0 = 1.

theorem AlgebraicCombinatorics.laurentPolynomial_one_eq_T_zero (K : Type u_1) [CommSemiring K] : 1 = LaurentPolynomial.T 0

The unity of K[x^±] is T 0 = (δ_{i,0})_{i∈ℤ}. This is part of Theorem thm.fps.laure.laupol-ring.

@[simp]

theorem AlgebraicCombinatorics.laurentPolynomial_one_apply (K : Type u_1) [CommSemiring K] (n : ℤ) : 1 n = if n = 0 then 1 else 0

The unity of K[x^±] evaluated at index n is 1 if n = 0, else 0. This is the explicit characterization from Theorem thm.fps.laure.laupol-ring.

Part 3: The element x is invertible

The element x (represented as T 1 in Mathlib) is a unit in K[x^±], with inverse x⁻¹ = T (-1).

theorem AlgebraicCombinatorics.laurentPolynomial_T_isUnit (K : Type u_1) [CommSemiring K] : IsUnit (LaurentPolynomial.T 1)

The element T 1 (corresponding to x) is invertible in K[T;T⁻¹]. This is part of Theorem thm.fps.laure.laupol-ring.

theorem AlgebraicCombinatorics.laurentPolynomial_T_isUnit' (K : Type u_1) [CommSemiring K] (n : ℤ) : IsUnit (LaurentPolynomial.T n)

More generally, T n is invertible for any n ∈ ℤ. This generalizes the invertibility statement in Theorem thm.fps.laure.laupol-ring.

@[simp]

theorem AlgebraicCombinatorics.laurentPolynomial_T_mul_T_neg (K : Type u_1) [CommSemiring K] (n : ℤ) : LaurentPolynomial.T n * LaurentPolynomial.T (-n) = 1

The inverse of T n is T (-n). This is the explicit inverse formula from Theorem thm.fps.laure.laupol-ring.

@[simp]

theorem AlgebraicCombinatorics.laurentPolynomial_T_neg_mul_T (K : Type u_1) [CommSemiring K] (n : ℤ) : LaurentPolynomial.T (-n) * LaurentPolynomial.T n = 1

The inverse of T n is T (-n) (multiplication in the other order). This is the explicit inverse formula from Theorem thm.fps.laure.laupol-ring.

def AlgebraicCombinatorics.laurentPolynomial_T_unit (K : Type u_1) [CommSemiring K] (n : ℤ) : (LaurentPolynomial K)ˣ

The unit associated to T n, with explicit inverse T (-n).

Equations

• AlgebraicCombinatorics.laurentPolynomial_T_unit K n = { val := LaurentPolynomial.T n, inv := LaurentPolynomial.T (-n), val_inv := ⋯, inv_val := ⋯ }

Representation as sum

Any Laurent polynomial f = (a_i){i ∈ ℤ} satisfies f = ∑{i ∈ support f} a_i T^i.

theorem AlgebraicCombinatorics.laurentPolynomial_eq_sum (K : Type u_1) [CommSemiring K] (f : LaurentPolynomial K) : f = Finsupp.sum f fun (n : ℤ) (a : K) => LaurentPolynomial.C a * LaurentPolynomial.T n

Any Laurent polynomial f = (a_i){i ∈ ℤ} satisfies f = ∑{i ∈ support f} a_i T^i. This is Proposition prop.fps.laure.a=sumaixi.

Here we state this for Laurent polynomials, where the sum is finite.

Alternative characterizations

The Laurent polynomial ring K[x^±] can equivalently be described as:

• The group algebra of ℤ over K
• The localization of K[x] at the powers of x

These are mentioned in the textbook after Theorem thm.fps.laure.laupol-ring.

theorem AlgebraicCombinatorics.laurentPolynomial_eq_groupAlgebra (K : Type u_1) [CommSemiring K] : LaurentPolynomial K = AddMonoidAlgebra K ℤ

K[x^±] is isomorphic to the group algebra K[ℤ]. This is one of the alternative characterizations mentioned after Theorem thm.fps.laure.laupol-ring.

instance AlgebraicCombinatorics.laurentPolynomial_commRing (K : Type u_1) [CommRing K] : CommRing (LaurentPolynomial K)

When K is a CommRing, Laurent polynomials form a CommRing. This is part of Theorem thm.fps.laure.laupol-ring.

Equations

• AlgebraicCombinatorics.laurentPolynomial_commRing K = inferInstance

Laurent Series

The K-algebra K((x)) of Laurent series consists of families (a_n)_{n ∈ ℤ} such that a_n = 0 for all sufficiently negative n.

We use Mathlib's LaurentSeries which is defined as HahnSeries ℤ R.

This corresponds to Definition def.fps.laure.lauser.

def AlgebraicCombinatorics.laurentPolyToSeries (K : Type u_1) [CommRing K] : LaurentPolynomial K →+* LaurentSeries K

The ring homomorphism from Laurent polynomials to Laurent series. This embeds K[x^±] into K((x)) by mapping each Laurent polynomial to the corresponding Laurent series with the same coefficients.

This is mentioned after Theorem thm.fps.laure.lauser-ring.

Equations

• AlgebraicCombinatorics.laurentPolyToSeries K = AddMonoidAlgebra.liftNCRingHom HahnSeries.C (AlgebraicCombinatorics.singleMonoidHom✝ K) ⋯

theorem AlgebraicCombinatorics.laurentPolyToSeries_single (K : Type u_1) [CommRing K] (n : ℤ) (r : K) : ((laurentPolyToSeries K) fun₀ | n => r) = (HahnSeries.single n) r

The Laurent polynomial to series map sends single n r to single n r.

theorem AlgebraicCombinatorics.laurentPolyToSeries_coeff (K : Type u_1) [CommRing K] (f : LaurentPolynomial K) (n : ℤ) : ((laurentPolyToSeries K) f).coeff n = f n

The Laurent polynomial to series map preserves coefficients.

theorem AlgebraicCombinatorics.laurentPolyToSeries_injective (K : Type u_1) [CommRing K] : Function.Injective ⇑(laurentPolyToSeries K)

The Laurent polynomial to series map is injective.

theorem AlgebraicCombinatorics.laurentPolynomial_embeds_in_laurentSeries (K : Type u_1) [CommRing K] : ∃ (f : LaurentPolynomial K →+* LaurentSeries K), Function.Injective ⇑f

The Laurent polynomial ring K[x^±] can be embedded into the Laurent series ring K((x)). This is mentioned after Theorem thm.fps.laure.lauser-ring.

theorem AlgebraicCombinatorics.one_sub_X_pow_isUnit (K : Type u_1) [CommRing K] (i : ℕ) (hi : 0 < i) : IsUnit (1 - PowerSeries.X ^ i)

For any positive integer i, the power series 1 - x^i is invertible in K[[x]] and hence also in K((x)). This allows the computation in the proof of Theorem thm.fps.laure.balanced-tern-rep-uniq.

Module Structure on K[[x^±]]

While K[[x^±]] is not a ring, it has a K[x^±]-module structure. A Laurent polynomial can be multiplied with any doubly infinite power series.

This corresponds to the discussion in "A K[x^±]-module structure on K[[x^±]]".

def AlgebraicCombinatorics.laurentPolynomialSmul {K : Type u_1} [CommRing K] (p : LaurentPolynomial K) (f : DoublyInfinitePowerSeries K) : DoublyInfinitePowerSeries K

The action of a Laurent polynomial on a doubly infinite power series.

The product (∑ b_n x^n) · (∑ a_n x^n) = (∑ c_n x^n) where c_n = ∑{i ∈ ℤ} a_i b{n-i}. This sum is finite because the Laurent polynomial has finite support.

This makes K[[x^±]] into a K[x^±]-module.

Equations

• AlgebraicCombinatorics.laurentPolynomialSmul p f n = Finsupp.sum p fun (i : ℤ) (b : K) => b * f (n - i)

theorem AlgebraicCombinatorics.torsion_example {K : Type u_1} [CommRing K] [Nontrivial K] : ∃ (p : LaurentPolynomial K) (f : DoublyInfinitePowerSeries K), p ≠ 0 ∧ f ≠ 0 ∧ laurentPolynomialSmul p f = 0

The multiplication (1-x) · (∑_{n ∈ ℤ} x^n) = 0 shows that K[[x^±]] has torsion as a K[x^±]-module. This is the calculation showing why we cannot divide by (1-x) in K[[x^±]].

This corresponds to the discussion at the end of the section.

k-bounded Balanced Ternary Representations

A balanced ternary representation is k-bounded if all digits beyond position k are zero. This is used in the rigorous proof of Theorem thm.fps.laure.balanced-tern-rep-uniq.

def AlgebraicCombinatorics.BalancedTernaryRepresentation.isBounded {n : ℤ} (r : BalancedTernaryRepresentation n) (k : ℕ) : Prop

A balanced ternary representation is k-bounded if b_{k+1} = b_{k+2} = ... = 0.

Equations

• r.isBounded k = ∀ i > k, r.digits i = 0

theorem AlgebraicCombinatorics.bounded_sum_eq {n : ℤ} (r : BalancedTernaryRepresentation n) (k : ℕ) (hk : r.isBounded k) : n = ∑ i ∈ Finset.range (k + 1), (r.digits i).toInt * 3 ^ i

For k-bounded representations, the finsum equals a finite sum over range(k+1).

theorem AlgebraicCombinatorics.sum_powers_of_three_eq_zero (k : ℕ) (c : ℕ → ℤ) (hc : ∀ i ≤ k, -2 ≤ c i ∧ c i ≤ 2) (hzero : ∀ i > k, c i = 0) (hsum : ∑ i ∈ Finset.range (k + 1), c i * 3 ^ i = 0) (i : ℕ) : c i = 0

Key lemma: if sum of c_i * 3^i = 0 where c_i ∈ {-2,...,2}, then all c_i = 0.

This is the core uniqueness argument: the difference of two balanced ternary representations has coefficients in {-2,...,2}, and if the sum is 0, all coefficients must be 0.

theorem AlgebraicCombinatorics.balancedTernaryRepresentation_bounded_unique (k : ℕ) (n : ℤ) (_hn : |n| ≤ ∑ i ∈ Finset.range (k + 1), 3 ^ i) (r₁ r₂ : BalancedTernaryRepresentation n) (h₁ : r₁.isBounded k) (h₂ : r₂.isBounded k) : r₁.digits = r₂.digits

Each integer n with |n| ≤ 3^0 + 3^1 + ... + 3^k has a unique k-bounded balanced ternary representation.

This is the key lemma used in the rigorous proof of Theorem thm.fps.laure.balanced-tern-rep-uniq.

Field Structure

When K is a field, K((x)) is also a field. This is mentioned at the end of the section.

Partial Product Formula

The key computation used to prove Theorem thm.fps.laure.balanced-tern-rep-uniq involves the partial products ∏_{i=0}^{k} (1 + x^{3^i} + x^{-3^i}).

def AlgebraicCombinatorics.balancedTernaryPartialProduct (K : Type u_1) [CommSemiring K] (k : ℕ) : LaurentPolynomial K

The partial product ∏_{i=0}^{k} (1 + T^{3^i} + T^{-3^i}) in the Laurent polynomial ring. This is used in the proof of Theorem thm.fps.laure.balanced-tern-rep-uniq.

Equations

• AlgebraicCombinatorics.balancedTernaryPartialProduct K k = ∏ i ∈ Finset.range (k + 1), (1 + LaurentPolynomial.T (3 ^ i) + LaurentPolynomial.T (-3 ^ i))

theorem AlgebraicCombinatorics.one_plus_T_plus_Tinv_eq (K : Type u_1) [CommRing K] : (1 + LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) * (LaurentPolynomial.T 1 * (1 - LaurentPolynomial.T 1)) = 1 - LaurentPolynomial.T 3

The identity 1 + x + x^{-1} = (1 - x^3) / (x(1-x)) as Laurent polynomials. This is used in simplifying the partial products.

theorem AlgebraicCombinatorics.geom_sum_three (k : ℕ) : 2 * ∑ i ∈ Finset.range (k + 1), 3 ^ i = 3 ^ (k + 1) - 1

The sum 3^0 + 3^1 + ... + 3^k = (3^{k+1} - 1) / 2. This is used in bounding the range of balanced ternary representations.