Infinite Products of Formal Power Series (Part 1)

This file formalizes detailed proofs about infinite products of formal power series, following the "Details: Infinite products (part 1)" section of the source.

Relationship with InfiniteProducts.lean

This file (InfiniteProducts1.lean) re-exports the canonical definitions from InfiniteProducts.lean (in the PowerSeries namespace) into the AlgebraicCombinatorics.FPS namespace. The definitions are definitionally equal:

• AlgebraicCombinatorics.FPS.Multipliable := PowerSeries.Multipliable
• AlgebraicCombinatorics.FPS.infprod := PowerSeries.tprod
• AlgebraicCombinatorics.FPS.DeterminesCoeff a n U := PowerSeries.DeterminesCoeffInProd a U n
• AlgebraicCombinatorics.FPS.CoeffFinitelyDetermined := PowerSeries.CoeffFinitelyDeterminedInProd
• AlgebraicCombinatorics.FPS.IsXnApproximator a n U := PowerSeries.IsXnApproximator a U n

The PowerSeries namespace versions are canonical and recommended for new code. The AlgebraicCombinatorics.FPS aliases are provided for consistency with other "Details" files.

Key difference: This file contains a fully proved version of SW1 (multipliable_fiber_prods, infprod_eq_infprod_fiber) with the invertibility hypothesis (hinv : ∀ s, IsUnit (constantCoeff (a s))). The InfiniteProducts.lean file has both:

• Fully proved multipliable_prod_fibers_inv / tprod_eq_tprod_fibers_inv (with invertibility)
• Sorry'd multipliable_prod_fibers / tprod_eq_tprod_fibers (without invertibility)

This file is kept separate to:

1. Follow the structure of the TeX source (Details: Infinite products part 1)
2. Provide detailed proofs of specific propositions from the source
3. Use the AlgebraicCombinatorics.FPS namespace for consistency with other "Details" files

Main Definitions

• AlgebraicCombinatorics.FPS.IsXnApproximator: Alias for PowerSeries.IsXnApproximator with swapped argument order. A finite subset U ⊆ I is an x^n-approximator for a family (aᵢ)_{i∈I} if it determines the first n+1 coefficients of the infinite product. (Definition def.fps.xnappr)

• AlgebraicCombinatorics.FPS.Multipliable: Alias for PowerSeries.Multipliable. A family of FPSs is multipliable if each coefficient in the product is finitely determined. (Definition def.fps.multipliable)

• AlgebraicCombinatorics.FPS.infprod: Alias for PowerSeries.tprod. The infinite product of a multipliable family of FPSs. (Definition def.fps.multipliable (b))

Main Results

Proposition prop.fps.union-mulable

• multipliable_of_subset: If (aᵢ)_{i∈I} is multipliable and J ⊆ I, then both (aᵢ)_{i∈J} and (aᵢ)_{i∈I\J} are multipliable.
• infprod_union_eq: The infinite product over I equals the product of infinite products over J and I \ J.

Proposition prop.fps.prod-mulable

• multipliable_mul: If (aᵢ) and (bᵢ) are multipliable, so is (aᵢ · bᵢ).
• infprod_mul_eq: The infinite product of (aᵢ · bᵢ) equals the product of the infinite products.

Lemma lem.fps.prod.irlv.cong-div

• xnEquiv_div: If a ≡ b and c ≡ d (mod x^{n+1}) with c, d invertible, then a/c ≡ b/d (mod x^{n+1}).

Proposition prop.fps.div-mulable

• multipliable_div: If (aᵢ) and (bᵢ) are multipliable with each bᵢ invertible, then (aᵢ/bᵢ) is multipliable.
• infprod_div_eq: The infinite product of (aᵢ/bᵢ) equals the quotient of the infinite products.

Lemma lem.fps.prods-mulable-subfams-appr

• xnApproximator_inter: If U is an x^n-approximator for (aᵢ)_{i∈I}, then U ∩ J is an x^n-approximator for (aᵢ)_{i∈J}.

Lemma lem.fps.prods-mulable-rules.SW1.lem1

• xnEquiv_finprod: If each cᵥ ≡ dᵥ (mod x^{n+1}), then ∏_{v∈V} cᵥ ≡ ∏_{v∈V} dᵥ.

Proposition prop.fps.prods-mulable-rules.SW1

• multipliable_fiber_prods: Infinite products can be reindexed along a surjection, grouping terms by fibers.
• infprod_eq_infprod_fiber: The infinite product over the source equals the infinite product over the target of fiber products.

References

• Source: AlgebraicCombinatorics/tex/Details/InfiniteProducts1.tex

Implementation Notes

This file re-exports the canonical definitions from PowerSeries namespace into AlgebraicCombinatorics.FPS namespace using abbrev. The definitions are definitionally equal, so all theorems work seamlessly with either namespace.

The key insight is that a family is multipliable if for each coefficient index n, there exists a finite "approximating" set that determines that coefficient.

x^n-Equivalence (Local Notation)

We use PowerSeries.XnEquiv from XnEquivalence.lean for the underlying definition. The notation f ≡[x^n] g is imported from Limits.lean (via InfiniteProducts.lean).

Lemma lem.fps.prod.irlv.cong-mul

If a ≡ b and c ≡ d (mod x^{n+1}), then a·c ≡ b·d (mod x^{n+1}). This is used in the proof of Proposition prop.fps.prod-mulable.

theorem AlgebraicCombinatorics.FPS.xnEquiv_mul_of_coeff_eq {K : Type u_1} [CommRing K] {n : ℕ} {a b c d : PowerSeries K} (hab : ∀ m ≤ n, (PowerSeries.coeff m) a = (PowerSeries.coeff m) b) (hcd : ∀ m ≤ n, (PowerSeries.coeff m) c = (PowerSeries.coeff m) d) (m : ℕ) : m ≤ n → (PowerSeries.coeff m) (a * c) = (PowerSeries.coeff m) (b * d)

If coefficients agree up to n, products agree up to n. (Lemma lem.fps.prod.irlv.cong-mul) Label: lem.fps.prod.irlv.cong-mul

Lemma lem.fps.prod.irlv.cong-div

If a ≡ b and c ≡ d (mod x^{n+1}) with c, d invertible, then a/c ≡ b/d (mod x^{n+1}).

This is the division analogue of lem.fps.prod.irlv.cong-mul.

theorem AlgebraicCombinatorics.FPS.xnEquiv_div {K : Type u_1} [CommRing K] {n : ℕ} {a b c d : PowerSeries K} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) (hc : IsUnit (PowerSeries.constantCoeff c)) (hd : IsUnit (PowerSeries.constantCoeff d)) : a * c.invOfUnit hc.unit ≡[x^n] b * d.invOfUnit hd.unit

If coefficients agree up to n for numerators and invertible denominators, quotients agree up to n. (Lemma lem.fps.prod.irlv.cong-div) Label: lem.fps.prod.irlv.cong-div

x^n-Approximators and Multipliable Families

The definitions below are aliases for the canonical PowerSeries versions. They are provided for consistency with other "Details" files and to maintain the argument order used in this file.

@[reducible, inline]

abbrev AlgebraicCombinatorics.FPS.DeterminesCoeff {K : Type u_1} [CommRing K] {ι : Type u_2} (a : ι → PowerSeries K) (n : ℕ) (U : Finset ι) : Prop

Alias for PowerSeries.DeterminesCoeffInProd with swapped argument order. A finite subset U ⊆ I determines the x^n-coefficient in the product of (aᵢ)_{i∈I} if for every finite subset T with U ⊆ T ⊆ I, the x^n-coefficient of ∏_{i∈T} aᵢ equals that of ∏_{i∈U} aᵢ. (Definition def.fps.infprod.coeff-det)

Equations

• AlgebraicCombinatorics.FPS.DeterminesCoeff a n U = PowerSeries.DeterminesCoeffInProd a U n

@[reducible, inline]

abbrev AlgebraicCombinatorics.FPS.IsXnApproximator {K : Type u_1} [CommRing K] {ι : Type u_2} (a : ι → PowerSeries K) (n : ℕ) (U : Finset ι) : Prop

Alias for PowerSeries.IsXnApproximator with swapped argument order. A finite subset U ⊆ I is an x^n-approximator for (aᵢ)_{i∈I} if it determines the first n+1 coefficients in the product. (Definition def.fps.xnappr) Label: def.fps.xnappr

Equations

• AlgebraicCombinatorics.FPS.IsXnApproximator a n U = PowerSeries.IsXnApproximator a U n

@[reducible, inline]

abbrev AlgebraicCombinatorics.FPS.CoeffFinitelyDetermined {K : Type u_1} [CommRing K] {ι : Type u_2} (a : ι → PowerSeries K) (n : ℕ) : Prop

Alias for PowerSeries.CoeffFinitelyDeterminedInProd. The x^n-coefficient in the product of (aᵢ)_{i∈I} is finitely determined if there exists a finite subset that determines it. (Definition def.fps.infprod.coeff-det)

Equations

• AlgebraicCombinatorics.FPS.CoeffFinitelyDetermined a n = PowerSeries.CoeffFinitelyDeterminedInProd a n

@[reducible, inline]

abbrev AlgebraicCombinatorics.FPS.Multipliable {K : Type u_1} [CommRing K] {ι : Type u_2} (a : ι → PowerSeries K) : Prop

Alias for PowerSeries.Multipliable. A family (aᵢ)_{i∈I} of FPSs is multipliable if each coefficient in the product is finitely determined. (Definition def.fps.multipliable) Label: def.fps.multipliable

Equations

• AlgebraicCombinatorics.FPS.Multipliable a = PowerSeries.Multipliable a

theorem AlgebraicCombinatorics.FPS.multipliable_exists_approximator {K : Type u_1} [CommRing K] {ι : Type u_2} {a : ι → PowerSeries K} (h : Multipliable a) (n : ℕ) : ∃ (U : Finset ι), IsXnApproximator a n U

If a family is multipliable, there exists an x^n-approximator for each n. (Lemma lem.fps.mulable.approx) Label: lem.fps.mulable.approx

The Infinite Product

The infinite product definitions are aliases for the canonical PowerSeries versions.

@[reducible, inline]

noncomputable abbrev AlgebraicCombinatorics.FPS.infprodCoeff {K : Type u_1} [CommRing K] {ι : Type u_2} (a : ι → PowerSeries K) (h : Multipliable a) (n : ℕ) : K

Alias for PowerSeries.tprodCoeff. The n-th coefficient of the infinite product of a multipliable family. This is well-defined because the coefficient is finitely determined.

Equations

• AlgebraicCombinatorics.FPS.infprodCoeff a h n = PowerSeries.tprodCoeff a h n

@[reducible, inline]

noncomputable abbrev AlgebraicCombinatorics.FPS.infprod {K : Type u_1} [CommRing K] {ι : Type u_2} (a : ι → PowerSeries K) (h : Multipliable a) : PowerSeries K

Alias for PowerSeries.tprod. The infinite product of a multipliable family of FPSs. (Definition def.fps.multipliable (b)) Label: def.fps.multipliable

Equations

• ∏∞ a h = PowerSeries.tprod a h

def AlgebraicCombinatorics.FPS.«term∏∞» : Lean.ParserDescr

Equations

• AlgebraicCombinatorics.FPS.«term∏∞» = Lean.ParserDescr.node `AlgebraicCombinatorics.FPS.«term∏∞» 1024 (Lean.ParserDescr.symbol "∏∞ ")

theorem AlgebraicCombinatorics.FPS.coeff_infprod_eq_coeff_finprod {K : Type u_1} [CommRing K] {ι : Type u_2} {a : ι → PowerSeries K} {n : ℕ} (h : Multipliable a) {U : Finset ι} (hU : DeterminesCoeff a n U) : (PowerSeries.coeff n) (∏∞ a h) = (PowerSeries.coeff n) (∏ i ∈ U, a i)

The n-th coefficient of the infinite product equals that of any approximating finite product. (Proposition prop.fps.infprod-approx-xneq (a)) Label: prop.fps.infprod-approx-xneq

theorem AlgebraicCombinatorics.FPS.infprod_xnEquiv_finprod {K : Type u_1} [CommRing K] {ι : Type u_2} {a : ι → PowerSeries K} {n : ℕ} (h : Multipliable a) {U : Finset ι} (hU : IsXnApproximator a n U) : ∏∞ a h ≡[x^n] ∏ i ∈ U, a i

If U is an x^n-approximator, the infinite product is x^n-equivalent to the finite product over U. (Proposition prop.fps.infprod-approx-xneq (b)) Label: prop.fps.infprod-approx-xneq

Lemma lem.fps.prods-mulable-subfams-appr

If U is an x^n-approximator for (aᵢ)_{i∈I} (a family of invertible FPSs), then U ∩ J is an x^n-approximator for (aᵢ)_{i∈J}.

This lemma is used in the proof of multipliable_of_subset.

theorem AlgebraicCombinatorics.FPS.xnApproximator_inter {K : Type u_1} [CommRing K] {ι : Type u_2} [DecidableEq ι] {a : ι → PowerSeries K} {n : ℕ} {U J : Finset ι} (hU : IsXnApproximator a n U) (hinv : ∀ (i : ι), IsUnit (PowerSeries.constantCoeff (a i))) : ∃ (M : Finset ↥J), IsXnApproximator (fun (i : ↥J) => a ↑i) n M

The intersection of an approximator with a subset gives an approximator for the subfamily. (Lemma lem.fps.prods-mulable-subfams-appr) Label: lem.fps.prods-mulable-subfams-appr

Given U an x^n-approximator for (aᵢ)_{i∈I} and J ⊆ I (as a Finset), there exists an x^n-approximator for (aᵢ)_{i∈J} derived from U ∩ J.

Proposition prop.fps.union-mulable (prop.fps.prods-mulable-subfams)

If (aᵢ)_{i∈I} is a multipliable family of invertible FPSs and J ⊆ I, then both (aᵢ)_{i∈J} and (aᵢ)_{i∈I\J} are multipliable, and ∏_{i∈I} aᵢ = (∏_{i∈J} aᵢ) · (∏_{i∈I\J} aᵢ).

theorem AlgebraicCombinatorics.FPS.multipliable_of_subset {K : Type u_1} [CommRing K] {ι : Type u_2} {a : ι → PowerSeries K} {J : Set ι} (h : Multipliable a) (hinv : ∀ (i : ι), IsUnit (PowerSeries.constantCoeff (a i))) : Multipliable fun (i : ↑J) => a ↑i

Subfamilies of a multipliable family of invertible FPSs are multipliable. (Proposition prop.fps.union-mulable (a) / prop.fps.prods-mulable-subfams) Label: prop.fps.union-mulable

Note: This is also known as multipliable_subfamily in the source. The proof uses xnApproximator_inter (lem.fps.prods-mulable-subfams-appr).

theorem AlgebraicCombinatorics.FPS.infprod_union_eq {K : Type u_1} [CommRing K] {ι : Type u_2} {a : ι → PowerSeries K} {J : Set ι} (h : Multipliable a) (_hinv : ∀ (i : ι), IsUnit (PowerSeries.constantCoeff (a i))) (hJ : Multipliable fun (i : ↑J) => a ↑i) (hJc : Multipliable fun (i : ↑Jᶜ) => a ↑i) : ∏∞ a h = ∏∞ (fun (i : ↑J) => a ↑i) hJ * ∏∞ (fun (i : ↑Jᶜ) => a ↑i) hJc

The infinite product splits over a disjoint union. (Proposition prop.fps.union-mulable (b)) Label: prop.fps.union-mulable

Proposition prop.fps.prod-mulable

If (aᵢ)_{i∈I} and (bᵢ)_{i∈I} are multipliable families, then so is (aᵢ · bᵢ)_{i∈I}, and ∏_{i∈I} (aᵢ · bᵢ) = (∏_{i∈I} aᵢ) · (∏_{i∈I} bᵢ).

theorem AlgebraicCombinatorics.FPS.multipliable_mul {K : Type u_1} [CommRing K] {ι : Type u_2} {a b : ι → PowerSeries K} (ha : Multipliable a) (hb : Multipliable b) : Multipliable fun (i : ι) => a i * b i

Part (a): The pointwise product of multipliable families is multipliable. (Proposition prop.fps.prod-mulable (a)) Label: prop.fps.prod-mulable

theorem AlgebraicCombinatorics.FPS.infprod_mul_eq {K : Type u_1} [CommRing K] {ι : Type u_2} {a b : ι → PowerSeries K} (ha : Multipliable a) (hb : Multipliable b) (hab : Multipliable fun (i : ι) => a i * b i) : ∏∞ (fun (i : ι) => a i * b i) hab = ∏∞ a ha * ∏∞ b hb

Part (b): The infinite product of pointwise products equals the product of infinite products. (Proposition prop.fps.prod-mulable (b)) Label: prop.fps.prod-mulable

Proposition prop.fps.div-mulable

If (aᵢ)_{i∈I} and (bᵢ)_{i∈I} are multipliable families with each bᵢ invertible, then (aᵢ/bᵢ)_{i∈I} is multipliable and ∏_{i∈I} (aᵢ/bᵢ) = (∏_{i∈I} aᵢ) / (∏_{i∈I} bᵢ).

theorem AlgebraicCombinatorics.FPS.multipliable_div {K : Type u_1} [CommRing K] {ι : Type u_2} {a b : ι → PowerSeries K} (ha : Multipliable a) (hb : Multipliable b) (hinv : ∀ (i : ι), IsUnit (PowerSeries.constantCoeff (b i))) : Multipliable fun (i : ι) => a i * (b i).invOfUnit ⋯.unit

The pointwise quotient of multipliable families (with invertible denominators) is multipliable. (Proposition prop.fps.div-mulable (a)) Label: prop.fps.div-mulable

theorem AlgebraicCombinatorics.FPS.infprod_div_eq {K : Type u_1} [CommRing K] {ι : Type u_2} {a b : ι → PowerSeries K} (ha : Multipliable a) (hb : Multipliable b) (hinv : ∀ (i : ι), IsUnit (PowerSeries.constantCoeff (b i))) (hab : Multipliable fun (i : ι) => a i * (b i).invOfUnit ⋯.unit) (hprod_inv : IsUnit (PowerSeries.constantCoeff (∏∞ b hb))) : ∏∞ (fun (i : ι) => a i * (b i).invOfUnit ⋯.unit) hab = ∏∞ a ha * (∏∞ b hb).invOfUnit hprod_inv.unit

The infinite product of pointwise quotients equals the quotient of infinite products. (Proposition prop.fps.div-mulable (b)) Label: prop.fps.div-mulable

Requires that the product of denominators has invertible constant coefficient.

Lemma lem.fps.prods-mulable-rules.SW1.lem1

If each cᵥ ≡ dᵥ (mod x^{n+1}) for v ∈ V (finite), then ∏_{v∈V} cᵥ ≡ ∏_{v∈V} dᵥ.

This is a restatement of part of Theorem thm.fps.xneq.props (f).

theorem AlgebraicCombinatorics.FPS.xnEquiv_finprod {K : Type u_1} [CommRing K] {ι : Type u_2} {n : ℕ} {V : Finset ι} {c d : ι → PowerSeries K} (h : ∀ v ∈ V, c v ≡[x^n] d v) : ∏ v ∈ V, c v ≡[x^n] ∏ v ∈ V, d v

Finite products preserve x^n-equivalence. (Lemma lem.fps.prods-mulable-rules.SW1.lem1) Label: lem.fps.prods-mulable-rules.SW1.lem1

Proposition prop.fps.prods-mulable-rules.SW1

Let f : S → W be a surjection. If (aₛ)_{s∈S} is a multipliable family such that for each w ∈ W, the subfamily (aₛ)_{s∈S, f(s)=w} is multipliable, then:

(a) The family (bᵥ)_{w∈W} where bᵥ = ∏_{s∈S, f(s)=w} aₛ is multipliable. (b) ∏_{s∈S} aₛ = ∏_{w∈W} bᵥ.

This allows reindexing/grouping of infinite products.

theorem AlgebraicCombinatorics.FPS.multipliable_fiber_prods {K : Type u_1} [CommRing K] {S : Type u_2} {W : Type u_3} {a : S → PowerSeries K} {f : S → W} (hS : Multipliable a) (hinv : ∀ (s : S), IsUnit (PowerSeries.constantCoeff (a s))) (hfiber : ∀ (w : W), Multipliable fun (s : { s : S // f s = w }) => a ↑s) : Multipliable fun (w : W) => ∏∞ (fun (s : { s : S // f s = w }) => a ↑s) ⋯

For a surjection f : S → W, if the original family and all fiber families are multipliable, then the family of fiber products is multipliable. (Proposition prop.fps.prods-mulable-rules.SW1, Claim 1 setup) Label: prop.fps.prods-mulable-rules.SW1

Note: The proof requires invertibility of each a s (i.e., IsUnit (constantCoeff (a s))). This is used in Claim 2 of the tex proof, which applies lem.fps.prods-mulable-subfams-appr to show that U ∩ fiber_w is an x^n-approximator for the fiber subfamily.

theorem AlgebraicCombinatorics.FPS.infprod_eq_infprod_fiber {K : Type u_1} [CommRing K] {S : Type u_2} {W : Type u_3} {a : S → PowerSeries K} {f : S → W} (hS : Multipliable a) (hinv : ∀ (s : S), IsUnit (PowerSeries.constantCoeff (a s))) (hfiber : ∀ (w : W), Multipliable fun (s : { s : S // f s = w }) => a ↑s) (hW : Multipliable fun (w : W) => ∏∞ (fun (s : { s : S // f s = w }) => a ↑s) ⋯) : ∏∞ a hS = ∏∞ (fun (w : W) => ∏∞ (fun (s : { s : S // f s = w }) => a ↑s) ⋯) hW

For a surjection f : S → W, the infinite product over S equals the infinite product over W of fiber products. (Proposition prop.fps.prods-mulable-rules.SW1 (b)) Label: prop.fps.prods-mulable-rules.SW1

Finite Families are Multipliable

A finite family of FPSs is always multipliable.

theorem AlgebraicCombinatorics.FPS.multipliable_of_finite {K : Type u_1} [CommRing K] {ι : Type u_2} [Finite ι] (a : ι → PowerSeries K) : Multipliable a

A finite family of FPSs is multipliable.

theorem AlgebraicCombinatorics.FPS.infprod_of_finite {K : Type u_1} [CommRing K] {ι : Type u_2} [Fintype ι] (a : ι → PowerSeries K) : ∏∞ a ⋯ = ∏ i : ι, a i

The infinite product of a finite family equals the finite product.

Constant Family

A constant family (c)_{i∈I} where c has constant term 1 is multipliable if and only if I is finite or c = 1.

theorem AlgebraicCombinatorics.FPS.multipliable_one {K : Type u_1} [CommRing K] {ι : Type u_2} : Multipliable fun (x : ι) => 1

If all FPSs in a family are 1, the family is multipliable.

theorem AlgebraicCombinatorics.FPS.infprod_one {K : Type u_1} [CommRing K] {ι : Type u_2} : ∏∞ (fun (x : ι) => 1) ⋯ = 1

The infinite product of the constant 1 family is 1.