Infinite Products of Formal Power Series

This file formalizes the theory of infinite products of formal power series (FPS), following the treatment in the source material (Section sec.gf.prod).

Relationship with InfiniteProducts1.lean

This file (InfiniteProducts.lean) provides the primary API in the PowerSeries namespace. The file InfiniteProducts1.lean provides an alternative formalization in the AlgebraicCombinatorics.FPS namespace with definitionally equivalent definitions:

• PowerSeries.Multipliable a = AlgebraicCombinatorics.FPS.Multipliable a
• PowerSeries.tprod a h = AlgebraicCombinatorics.FPS.infprod a h
• PowerSeries.DeterminesCoeffInProd a M n = AlgebraicCombinatorics.FPS.DeterminesCoeff a n M (argument order)
• PowerSeries.IsXnApproximator a M n = AlgebraicCombinatorics.FPS.IsXnApproximator a n M (argument order)

The PowerSeries namespace versions are canonical and recommended for new code.

Main Definitions

• PowerSeries.DeterminesCoeffInProd: A finite subset M determines the x^n-coefficient in the product of a family if adding more factors doesn't change that coefficient.
• PowerSeries.CoeffFinitelyDeterminedInProd: The x^n-coefficient is finitely determined if some finite subset determines it.
• PowerSeries.Multipliable: A family of FPS is multipliable if all coefficients in its product are finitely determined.
• PowerSeries.tprod: The infinite product of a multipliable family.
• PowerSeries.IsXnApproximator: A finite subset that determines the first n+1 coefficients.

Main Results

• PowerSeries.multipliable_coeff_eq_of_determines: The infinite product is well-defined.
• PowerSeries.tprod_coeff: The coefficient of the infinite product equals the coefficient of any determining finite partial product.
• PowerSeries.multipliable_one_add_of_summable: If (f_i) is summable, then (1 + f_i) is multipliable.
• PowerSeries.multipliable_of_finite_ne_one: If all but finitely many entries equal 1, the family is multipliable.
• PowerSeries.multipliable_of_union: Products can be split into subproducts.
• PowerSeries.multipliable_mul: Products of multipliable families are multipliable.
• PowerSeries.multipliable_div: Quotients of multipliable families (with invertible denominators).
• PowerSeries.multipliable_subfamily: Subfamilies of multipliable families of invertible FPS.
• PowerSeries.multipliable_reindex: Reindexing preserves multipliability.
• PowerSeries.tprod_fubini: Fubini rule for infinite products (I × J → I then J).
• PowerSeries.tprod_fubini_J: Fubini rule for infinite products (I × J → J then I).
• PowerSeries.fubini_prod_invertible: Fubini rule showing both row/column families are multipliable.

References

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

Motivating Example: Binary Representation

The product ∏_{i ∈ ℕ} (1 + x^{2^i}) equals 1/(1-x) in R[[x]]. This relates to the unique binary representation of natural numbers. (Label: eq.fps.prod.binary.2)

theorem PowerSeries.prod_one_add_pow_two_eq {R : Type u_1} [CommRing R] (m : ℕ) : ∏ i ∈ Finset.range (m + 1), (1 + X ^ 2 ^ i) = (1 - X ^ 2 ^ (m + 1)) * (1 - X).invOfUnit 1

The product of (1 + x^{2^i}) for i from 0 to m equals (1 - x^{2^{m+1}}) / (1 - x). This is the finite version of the binary product identity. (Label: eq.fps.prod.binary.1)

Definition of Coefficient Determination

Definition \ref{def.fps.determines-xn-coeff}

def PowerSeries.DeterminesCoeffInProd {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (M : Finset I) (n : ℕ) : Prop

A finite subset M of I determines the x^n-coefficient in the product of a family (a_i)_{i ∈ I} if for every finite superset J of M, the x^n-coefficient of ∏_{i ∈ J} a_i equals that of ∏_{i ∈ M} a_i. (Label: def.fps.determines-xn-coeff part (b))

Equations

• PowerSeries.DeterminesCoeffInProd a M n = ∀ (J : Finset I), M ⊆ J → (PowerSeries.coeff n) (∏ i ∈ J, a i) = (PowerSeries.coeff n) (∏ i ∈ M, a i)

theorem PowerSeries.determinesCoeffInProd_mono {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {M₁ M₂ : Finset I} {n : ℕ} (h : DeterminesCoeffInProd a M₁ n) (hsub : M₁ ⊆ M₂) : DeterminesCoeffInProd a M₂ n

If M₁ determines the x^n coefficient and M₁ ⊆ M₂, then M₂ also determines it.

def PowerSeries.DeterminesCoeffInSum {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (M : Finset I) (n : ℕ) : Prop

A finite subset M of I determines the x^n-coefficient in the sum of a family (a_i)_{i ∈ I} if for every finite superset J of M, the x^n-coefficient of ∑_{i ∈ J} a_i equals that of ∑_{i ∈ M} a_i. (Label: def.fps.determines-xn-coeff part (a))

Equations

• PowerSeries.DeterminesCoeffInSum a M n = ∀ (J : Finset I), M ⊆ J → (PowerSeries.coeff n) (∑ i ∈ J, a i) = (PowerSeries.coeff n) (∑ i ∈ M, a i)

Definition of Finitely Determined Coefficients

Definition \ref{def.fps.xn-coeff-fin-determined}

def PowerSeries.CoeffFinitelyDeterminedInProd {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (n : ℕ) : Prop

The x^n-coefficient in the product of (a_i)_{i ∈ I} is finitely determined if there exists a finite subset M that determines it. (Label: def.fps.xn-coeff-fin-determined part (b))

Equations

• PowerSeries.CoeffFinitelyDeterminedInProd a n = ∃ (M : Finset I), PowerSeries.DeterminesCoeffInProd a M n

def PowerSeries.CoeffFinitelyDeterminedInSum {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (n : ℕ) : Prop

The x^n-coefficient in the sum of (a_i)_{i ∈ I} is finitely determined if there exists a finite subset M that determines it. (Label: def.fps.xn-coeff-fin-determined part (a))

Equations

• PowerSeries.CoeffFinitelyDeterminedInSum a n = ∃ (M : Finset I), PowerSeries.DeterminesCoeffInSum a M n

API for Finitely Determined Coefficients

Basic lemmas for CoeffFinitelyDeterminedInProd and CoeffFinitelyDeterminedInSum. (Label: def.fps.xn-coeff-fin-determined)

theorem PowerSeries.determinesCoeffInSum_mono {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {M₁ M₂ : Finset I} {n : ℕ} (h : DeterminesCoeffInSum a M₁ n) (hsub : M₁ ⊆ M₂) : DeterminesCoeffInSum a M₂ n

If M₁ determines the x^n coefficient in a sum and M₁ ⊆ M₂, then M₂ also determines it.

theorem PowerSeries.coeffFinitelyDeterminedInProd_of_finite {R : Type u_1} [CommRing R] {I : Type u_2} [Fintype I] (a : I → PowerSeries R) (n : ℕ) : CoeffFinitelyDeterminedInProd a n

For a finite index set, every coefficient in a product is finitely determined. (Label: def.fps.xn-coeff-fin-determined)

theorem PowerSeries.coeffFinitelyDeterminedInSum_of_finite {R : Type u_1} [CommRing R] {I : Type u_2} [Fintype I] (a : I → PowerSeries R) (n : ℕ) : CoeffFinitelyDeterminedInSum a n

For a finite index set, every coefficient in a sum is finitely determined. (Label: def.fps.xn-coeff-fin-determined)

theorem PowerSeries.determinesCoeffInSum_empty_iff {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (n : ℕ) : DeterminesCoeffInSum a ∅ n ↔ ∀ (i : I), (coeff n) (a i) = 0

The empty set determines the x^n-coefficient in a sum if and only if all terms have zero x^n-coefficient. (Label: def.fps.xn-coeff-fin-determined)

theorem PowerSeries.determinesCoeffInProd_empty_iff {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (n : ℕ) : DeterminesCoeffInProd a ∅ n ↔ ∀ (J : Finset I), (coeff n) (∏ i ∈ J, a i) = (coeff n) 1

The empty set determines the x^n-coefficient in a product if and only if the product of any finite subset has the same x^n-coefficient as 1. (Label: def.fps.xn-coeff-fin-determined)

theorem PowerSeries.coeffFinitelyDeterminedInSum_value_unique {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {n : ℕ} {M₁ M₂ : Finset I} (hM₁ : DeterminesCoeffInSum a M₁ n) (hM₂ : DeterminesCoeffInSum a M₂ n) : (coeff n) (∑ i ∈ M₁, a i) = (coeff n) (∑ i ∈ M₂, a i)

The value of the finitely determined coefficient in a sum is unique: for any two determining sets, the coefficient values agree. (Label: def.fps.xn-coeff-fin-determined)

theorem PowerSeries.coeffFinitelyDeterminedInProd_value_unique {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {n : ℕ} {M₁ M₂ : Finset I} (hM₁ : DeterminesCoeffInProd a M₁ n) (hM₂ : DeterminesCoeffInProd a M₂ n) : (coeff n) (∏ i ∈ M₁, a i) = (coeff n) (∏ i ∈ M₂, a i)

The value of the finitely determined coefficient in a product is unique: for any two determining sets, the coefficient values agree. (Label: def.fps.xn-coeff-fin-determined)

theorem PowerSeries.coeffFinitelyDeterminedInSum_of_finite_support {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (n : ℕ) (h : {i : I | (coeff n) (a i) ≠ 0}.Finite) : CoeffFinitelyDeterminedInSum a n

If all but finitely many terms have zero x^n-coefficient, then the x^n-coefficient in the sum is finitely determined. (Label: def.fps.xn-coeff-fin-determined)

Summability and Finite Determination

Proposition \ref{prop.fps.summable=fin-det}

theorem PowerSeries.summable_iff_coeff_finitely_determined {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) : (∀ (n : ℕ), {i : I | (coeff n) (a i) ≠ 0}.Finite) ↔ ∀ (n : ℕ), CoeffFinitelyDeterminedInSum a n

A family of FPS is summable if and only if each coefficient in its sum is finitely determined. (Label: prop.fps.summable=fin-det part (a))

Multipliability

Definition \ref{def.fps.multipliable}

def PowerSeries.Multipliable {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) : Prop

A family (a_i)_{i ∈ I} of FPS is multipliable if for each n ∈ ℕ, the x^n-coefficient in its product is finitely determined. (Label: def.fps.multipliable part (a))

Equations

• PowerSeries.Multipliable a = ∀ (n : ℕ), PowerSeries.CoeffFinitelyDeterminedInProd a n

theorem PowerSeries.multipliable_coeff_eq_of_determines {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {M₁ M₂ : Finset I} {n : ℕ} (h₁ : DeterminesCoeffInProd a M₁ n) (h₂ : DeterminesCoeffInProd a M₂ n) : (coeff n) (∏ i ∈ M₁, a i) = (coeff n) (∏ i ∈ M₂, a i)

For a multipliable family, the x^n-coefficient of the infinite product is well-defined: it equals the x^n-coefficient of any finite partial product that determines it. (Label: prop.fps.multipliable.prod-wd)

The Infinite Product

Definition \ref{def.fps.multipliable} part (b)

noncomputable def PowerSeries.tprodCoeff {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (ha : Multipliable a) (n : ℕ) : R

For a multipliable family, the n-th coefficient of the infinite product. This is the common value of (∏ i ∈ M, a i).coeff n for any finite M that determines the x^n-coefficient. (Label: def.fps.multipliable part (b))

Equations

• PowerSeries.tprodCoeff a ha n = (PowerSeries.coeff n) (∏ i ∈ Exists.choose ⋯, a i)

noncomputable def PowerSeries.tprod {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (ha : Multipliable a) : PowerSeries R

The infinite product of a multipliable family of formal power series. For a multipliable family (a_i)_{i ∈ I}, this is the FPS whose x^n-coefficient equals the x^n-coefficient of any finite partial product that determines it. (Label: def.fps.multipliable part (b))

Equations

• PowerSeries.tprod a ha = PowerSeries.mk fun (n : ℕ) => PowerSeries.tprodCoeff a ha n

theorem PowerSeries.tprod_coeff {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} (ha : Multipliable a) {M : Finset I} {n : ℕ} (hM : DeterminesCoeffInProd a M n) : (coeff n) (tprod a ha) = (coeff n) (∏ i ∈ M, a i)

The n-th coefficient of the infinite product equals the n-th coefficient of any finite partial product that determines it. (Label: def.fps.multipliable part (b))

theorem PowerSeries.tprod_eq_finprod {R : Type u_1} [CommRing R] {I : Type u_2} [Fintype I] (a : I → PowerSeries R) (ha : Multipliable a) : tprod a ha = ∏ i : I, a i

For a finite family, the infinite product definition agrees with the finite product. (Label: prop.fps.multipliable.prod-wd2)

x^n-Approximators

Definition \ref{def.fps.infprod-approx}

def PowerSeries.IsXnApproximator {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (M : Finset I) (n : ℕ) : Prop

A finite subset M is an x^n-approximator for a family (a_i)_{i ∈ I} if it determines the first n+1 coefficients (i.e., x^0, x^1, ..., x^n) in the product. (Label: def.fps.infprod-approx)

Equations

• PowerSeries.IsXnApproximator a M n = ∀ m ≤ n, PowerSeries.DeterminesCoeffInProd a M m

theorem PowerSeries.isXnApproximator_mono {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {M : Finset I} {n m : ℕ} (hM : IsXnApproximator a M n) (hmn : m ≤ n) : IsXnApproximator a M m

An x^n-approximator is also an x^m-approximator for any m ≤ n. (Label: def.fps.infprod-approx)

theorem PowerSeries.isXnApproximator_superset {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {M N : Finset I} {n : ℕ} (hM : IsXnApproximator a M n) (hMN : M ⊆ N) : IsXnApproximator a N n

If M is an x^n-approximator and M ⊆ N, then N is also an x^n-approximator. (Label: def.fps.infprod-approx)

theorem PowerSeries.isXnApproximator_empty_of_forall_eq_one {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} (ha : ∀ (i : I), a i = 1) (n : ℕ) : IsXnApproximator a ∅ n

The empty set is an x^n-approximator if and only if all a_i = 1. More precisely, if the family has all entries equal to 1, then ∅ is an approximator. (Label: def.fps.infprod-approx)

theorem PowerSeries.isXnApproximator_determines_coeff {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {M : Finset I} {n : ℕ} (hM : IsXnApproximator a M n) : DeterminesCoeffInProd a M n

An x^n-approximator always determines the x^n-coefficient. (Label: def.fps.infprod-approx)

theorem PowerSeries.exists_xn_approximator {R : Type u_1} [CommRing R] {I : Type u_2} [DecidableEq I] (a : I → PowerSeries R) (ha : Multipliable a) (n : ℕ) : ∃ (M : Finset I), IsXnApproximator a M n

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

Lemmas on Irrelevant Factors

Lemma \ref{lem.fps.prod.irlv.1}

theorem PowerSeries.coeff_mul_one_add_eq_of_coeff_zero {R : Type u_1} [CommRing R] {a f : PowerSeries R} {n : ℕ} (hf : ∀ m ≤ n, (coeff m) f = 0) (m : ℕ) (hm : m ≤ n) : (coeff m) (a * (1 + f)) = (coeff m) a

If f has zero coefficients for x^0, ..., x^n, then multiplying by (1 + f) doesn't change the first n+1 coefficients. (Label: lem.fps.prod.irlv.1)

theorem PowerSeries.coeff_mul_prod_one_add_eq {R : Type u_1} [CommRing R] {I : Type u_2} {a : PowerSeries R} {J : Finset I} {f : I → PowerSeries R} {n : ℕ} (hf : ∀ i ∈ J, ∀ m ≤ n, (coeff m) (f i) = 0) (m : ℕ) (hm : m ≤ n) : (coeff m) (a * ∏ i ∈ J, (1 + f i)) = (coeff m) a

Extension of the irrelevant factor lemma to finite products. (Label: lem.fps.prod.irlv.fin)

Criterion for Multipliability

Theorem \ref{thm.fps.1+f-mulable}

theorem PowerSeries.multipliable_one_add_of_summable {R : Type u_1} [CommRing R] {I : Type u_2} {f : I → PowerSeries R} (hf : ∀ (n : ℕ), {i : I | (coeff n) (f i) ≠ 0}.Finite) : Multipliable fun (i : I) => 1 + f i

If (f_i)_{i ∈ I} is a summable family of FPS, then (1 + f_i)_{i ∈ I} is multipliable. This is the main criterion for multipliability. (Label: thm.fps.1+f-mulable)

Simple Criteria for Multipliability

Proposition \ref{prop.fps.1-mulable} and Remark \ref{rmk.fps.0-mulable}

theorem PowerSeries.multipliable_of_finite_ne_one {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) (h : {i : I | a i ≠ 1}.Finite) : Multipliable a

If all but finitely many entries of a family equal 1, the family is multipliable. (Label: prop.fps.1-mulable)

@[simp]

theorem PowerSeries.multipliable_const_one {R : Type u_1} [CommRing R] {I : Type u_2} : Multipliable fun (x : I) => 1

The constant 1 family is always multipliable. The empty set determines all coefficients since ∏_{i ∈ ∅} 1 = 1. (Label: def.fps.multipliable)

@[simp]

theorem PowerSeries.tprod_const_one {R : Type u_1} [CommRing R] {I : Type u_2} (h : Multipliable fun (x : I) => 1 := ⋯) : tprod (fun (x : I) => 1) h = 1

The product of all 1s is 1. (Label: def.fps.multipliable)

@[simp]

theorem PowerSeries.multipliable_empty {R : Type u_1} [CommRing R] (a : Empty → PowerSeries R) : Multipliable a

For the empty index type, any family is trivially multipliable. The empty set determines all coefficients since the product is 1. (Label: def.fps.multipliable)

@[simp]

theorem PowerSeries.tprod_empty {R : Type u_1} [CommRing R] (a : Empty → PowerSeries R) (h : Multipliable a := ⋯) : tprod a h = 1

For the empty index type, the infinite product is 1. (Label: def.fps.multipliable)

@[simp]

theorem PowerSeries.multipliable_singleton {R : Type u_1} [CommRing R] {I : Type u_2} [Unique I] (a : I → PowerSeries R) : Multipliable a

For a singleton index type, any family is multipliable. (Label: def.fps.multipliable)

@[simp]

theorem PowerSeries.tprod_singleton {R : Type u_1} [CommRing R] {I : Type u_2} [Unique I] (a : I → PowerSeries R) (h : Multipliable a := ⋯) : tprod a h = a default

For a singleton index type, the infinite product equals the single element. (Label: def.fps.multipliable)

theorem PowerSeries.multipliable_of_zero_mem {R : Type u_1} [CommRing R] {I : Type u_2} (a : I → PowerSeries R) {j : I} (hj : a j = 0) : Multipliable a

If a family contains 0 as an entry, it is multipliable (and the product is 0). (Label: rmk.fps.0-mulable)

The Binary Product Identity (Infinite Version)

This is the infinite version of the binary product identity, stating that ∏_{i ∈ ℕ} (1 + x^{2^i}) = 1/(1-x). (Label: eq.fps.prod.binary.2)

theorem PowerSeries.multipliable_one_add_pow_two {R : Type u_1} [CommRing R] : Multipliable fun (i : ℕ) => 1 + X ^ 2 ^ i

The family (1 + x^{2^i})_{i ∈ ℕ} is multipliable.

theorem PowerSeries.tprod_one_add_pow_two_eq {R : Type u_1} [CommRing R] : tprod (fun (i : ℕ) => 1 + X ^ 2 ^ i) ⋯ = (1 - X).invOfUnit 1

The infinite product ∏_{i ∈ ℕ} (1 + x^{2^i}) equals 1/(1-x). This relates to the unique binary representation of natural numbers: each natural number can be written uniquely as a sum of distinct powers of 2. (Label: eq.fps.prod.binary.2)

Properties of Infinite Products

Proposition \ref{prop.fps.union-mulable}

theorem PowerSeries.multipliable_of_union {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {J : Set I} (hJ : Multipliable fun (i : ↑J) => a ↑i) (hIJ : Multipliable fun (i : ↑(Set.univ \ J)) => a ↑i) : Multipliable a

If the subfamilies over J and I \ J are multipliable, then the entire family is multipliable. (Label: prop.fps.union-mulable part (a))

theorem PowerSeries.tprod_eq_tprod_mul_tprod {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {J : Set I} (ha : Multipliable a) (hJ : Multipliable fun (i : ↑J) => a ↑i) (hIJ : Multipliable fun (i : ↑(Set.univ \ J)) => a ↑i) : tprod a ha = tprod (fun (i : ↑J) => a ↑i) hJ * tprod (fun (i : ↑(Set.univ \ J)) => a ↑i) hIJ

The product over I equals the product of subproducts over J and I \ J. (Label: prop.fps.union-mulable part (b))

Product Rule for Multipliable Families

Proposition \ref{prop.fps.prod-mulable}

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

If (a_i) and (b_i) are multipliable, then so is (a_i * b_i). (Label: prop.fps.prod-mulable part (a))

The proof follows the detailed proof in Section sec.details.gf.prod:

1. Get x^n-approximators U and V for families a and b respectively
2. Let M = U ∪ V
3. Show M determines the x^n coefficient for (a_i * b_i)
4. Use the fact that if two pairs of FPS agree up to degree n, their products also agree up to degree n

theorem PowerSeries.tprod_mul_eq_mul_tprod {R : Type u_1} [CommRing R] {I : Type u_2} {a b : I → PowerSeries R} (ha : Multipliable a) (hb : Multipliable b) (hab : Multipliable fun (i : I) => a i * b i := ⋯) : tprod (fun (i : I) => a i * b i) hab = tprod a ha * tprod b hb

The product of (a_i * b_i) equals the product of products. (Label: prop.fps.prod-mulable part (b))

Division Rule for Multipliable Families

Proposition \ref{prop.fps.div-mulable}

theorem PowerSeries.multipliable_div {R : Type u_1} [CommRing R] {I : Type u_2} {a b : I → PowerSeries R} (ha : Multipliable a) (hb : Multipliable b) (hb_inv : ∀ (i : I), IsUnit ((coeff 0) (b i))) : Multipliable fun (i : I) => a i * Ring.inverse (b i)

If (a_i) and (b_i) are multipliable and each b_i is invertible, then (a_i / b_i) is multipliable. (Label: prop.fps.div-mulable part (a))

The proof is similar to multipliable_mul, using the additional fact that if two FPS agree up to degree n and both have invertible constant terms, then their Ring.inverses also agree up to degree n.

theorem PowerSeries.tprod_div_eq_div_tprod {R : Type u_1} [CommRing R] {I : Type u_2} {a b : I → PowerSeries R} (ha : Multipliable a) (hb : Multipliable b) (hb_inv : ∀ (i : I), IsUnit ((coeff 0) (b i))) (hab : Multipliable fun (i : I) => a i * Ring.inverse (b i) := ⋯) : tprod (fun (i : I) => a i * Ring.inverse (b i)) hab = tprod a ha * Ring.inverse (tprod b hb)

The product of (a_i / b_i) equals the quotient of products. (Label: prop.fps.div-mulable part (b))

Subfamilies of Multipliable Families

Remark \ref{rmk.fps.subfamily-not-mulable} shows that not every subfamily of a multipliable family is multipliable. However, for invertible FPS, this holds.

Proposition \ref{prop.fps.prods-mulable-subfams}

theorem PowerSeries.isXnApproximator_inter_subfamily {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {U : Finset I} {n : ℕ} (hU : IsXnApproximator a U n) (ha_inv : ∀ (i : I), IsUnit ((coeff 0) (a i))) (J : Set I) : IsXnApproximator (fun (i : ↑J) => a ↑i) (U.preimage Subtype.val ⋯) n

Key lemma: If U is an x^n-approximator for the full family, and all FPS are invertible, then U ∩ J is an x^n-approximator for the subfamily J. This is Lemma lem.fps.prods-mulable-subfams-appr from the tex source. The invertibility assumption is essential for this lemma.

theorem PowerSeries.multipliable_subfamily {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} (ha : Multipliable a) (ha_inv : ∀ (i : I), IsUnit ((coeff 0) (a i))) (J : Set I) : Multipliable fun (i : ↑J) => a ↑i

If (a_i)_{i ∈ I} is a multipliable family of invertible FPS, then any subfamily is also multipliable. (Label: prop.fps.prods-mulable-subfams)

Reindexing

Proposition \ref{prop.fps.prods-mulable-rules.reindex}

theorem PowerSeries.multipliable_reindex {R : Type u_1} [CommRing R] {S : Type u_3} {T : Type u_4} {f : S → T} (hf : Function.Bijective f) {a : T → PowerSeries R} (ha : Multipliable a) : Multipliable (a ∘ f)

Reindexing a multipliable family via a bijection preserves multipliability. (Label: prop.fps.prods-mulable-rules.reindex)

theorem PowerSeries.tprod_reindex {R : Type u_1} [CommRing R] {S : Type u_3} {T : Type u_4} {f : S → T} (hf : Function.Bijective f) {a : T → PowerSeries R} (ha : Multipliable a) (haf : Multipliable (a ∘ f) := ⋯) : tprod (a ∘ f) haf = tprod a ha

Reindexing a multipliable family via a bijection preserves the product. (Label: prop.fps.prods-mulable-rules.reindex)

Breaking Products into Subproducts

Proposition \ref{prop.fps.prods-mulable-rules.SW1}

theorem PowerSeries.multipliable_prod_fibers {R : Type u_1} [CommRing R] {S : Type u_3} {W : Type u_4} {f : S → W} {a : S → PowerSeries R} (ha : Multipliable a) (ha_fibers : ∀ (w : W), Multipliable fun (s : { s : S // f s = w }) => a ↑s) : Multipliable fun (w : W) => tprod (fun (s : { s : S // f s = w }) => a ↑s) ⋯

The family of subproducts indexed by fibers is multipliable. (Label: prop.fps.prods-mulable-rules.SW1)

This theorem proves that if a family (a_s)_{s ∈ S} of power series is multipliable, and each fiber {s : f s = w} gives a multipliable subfamily, then the family of fiber products (tprod_{s : f s = w} a_s)_{w ∈ W} is also multipliable.

Note: The TeX source proof uses Lemma lem.fps.prods-mulable-subfams-appr which requires invertibility. This Lean proof uses a different approach that avoids the invertibility assumption: instead of showing each fiber's tprod is x^n-equivalent to 1 (which requires invertibility to "cancel" other fibers), we directly relate the outer product to the full product via unions of fiber approximators.

theorem PowerSeries.multipliable_prod_fibers_inv {R : Type u_1} [CommRing R] {S : Type u_3} {W : Type u_4} {f : S → W} {a : S → PowerSeries R} (ha : Multipliable a) (ha_inv : ∀ (s : S), IsUnit ((coeff 0) (a s))) (ha_fibers : ∀ (w : W), Multipliable fun (s : { s : S // f s = w }) => a ↑s := ⋯) : Multipliable fun (w : W) => tprod (fun (s : { s : S // f s = w }) => a ↑s) ⋯

The family of subproducts indexed by fibers is multipliable (invertible case). (Label: prop.fps.prods-mulable-rules.SW1)

This is a version of multipliable_prod_fibers with an invertibility assumption that enables a complete proof. The tex source proof implicitly uses invertibility through Lemma lem.fps.prods-mulable-subfams-appr.

When all FPS in the family have unit constant term, we can use coeff_eq_of_mul_eq_unit to cancel common factors and relate fiber products.

theorem PowerSeries.tprod_eq_tprod_fibers {R : Type u_1} [CommRing R] {S : Type u_3} {W : Type u_4} {f : S → W} {a : S → PowerSeries R} (ha : Multipliable a) (ha_fibers : ∀ (w : W), Multipliable fun (s : { s : S // f s = w }) => a ↑s) (ha_outer : Multipliable fun (w : W) => tprod (fun (s : { s : S // f s = w }) => a ↑s) ⋯ := ⋯) : tprod a ha = tprod (fun (w : W) => tprod (fun (s : { s : S // f s = w }) => a ↑s) ⋯) ha_outer

A multipliable product can be broken into subproducts indexed by a map. (Label: prop.fps.prods-mulable-rules.SW1)

This theorem states that if (a_s)_{s ∈ S} is a multipliable family of FPS, then the infinite product can be computed by first grouping elements by their image under f : S → W, computing the infinite product within each fiber, and then taking the infinite product of those results.

Proof approach: Rather than trying to show that U ∩ fiber(w) determines the coefficient in the fiber product (which requires invertibility to "cancel" other fibers), we use proper approximators M_w for each fiber from ha_fibers, and relate everything through the full product approximator. This approach follows multipliable_prod_fibers.

theorem PowerSeries.tprod_eq_tprod_fibers_inv {R : Type u_1} [CommRing R] {S : Type u_3} {W : Type u_4} {f : S → W} {a : S → PowerSeries R} (ha : Multipliable a) (ha_inv : ∀ (s : S), IsUnit ((coeff 0) (a s))) (ha_fibers : ∀ (w : W), Multipliable fun (s : { s : S // f s = w }) => a ↑s := ⋯) (ha_outer : Multipliable fun (w : W) => tprod (fun (s : { s : S // f s = w }) => a ↑s) ⋯ := ⋯) : tprod a ha = tprod (fun (w : W) => tprod (fun (s : { s : S // f s = w }) => a ↑s) ⋯) ha_outer

A multipliable product can be broken into subproducts indexed by a map (invertible case). (Label: prop.fps.prods-mulable-rules.SW1)

This is a version of tprod_eq_tprod_fibers with an invertibility assumption that enables a complete proof. The tex source proof implicitly uses invertibility through Lemma lem.fps.prods-mulable-subfams-appr.

When all FPS in the family have unit constant term, we can use coeff_eq_of_mul_eq_unit to cancel common factors and relate fiber products.

Fubini Rule for Infinite Products

Proposition \ref{prop.fps.prods-mulable-rules.fubini1}

theorem PowerSeries.multipliable_tprod_fubini {R : Type u_1} [CommRing R] {I : Type u_3} {J : Type u_4} {a : I × J → PowerSeries R} (ha : Multipliable a) (ha_I : ∀ (i : I), Multipliable fun (j : J) => a (i, j)) : Multipliable fun (i : I) => tprod (fun (j : J) => a (i, j)) ⋯

Fubini rule: the iterated product over I then J is multipliable. (Label: prop.fps.prods-mulable-rules.fubini1)

theorem PowerSeries.tprod_fubini {R : Type u_1} [CommRing R] {I : Type u_3} {J : Type u_4} {a : I × J → PowerSeries R} (ha : Multipliable a) (ha_I : ∀ (i : I), Multipliable fun (j : J) => a (i, j)) (_ha_J : ∀ (j : J), Multipliable fun (i : I) => a (i, j)) (ha_outer_I : Multipliable fun (i : I) => tprod (fun (j : J) => a (i, j)) ⋯ := ⋯) : tprod a ha = tprod (fun (i : I) => tprod (fun (j : J) => a (i, j)) ⋯) ha_outer_I

Fubini rule: products over I × J can be computed as iterated products. (Label: prop.fps.prods-mulable-rules.fubini1)

theorem PowerSeries.multipliable_tprod_fubini_J {R : Type u_1} [CommRing R] {I : Type u_3} {J : Type u_4} {a : I × J → PowerSeries R} (ha : Multipliable a) (ha_J : ∀ (j : J), Multipliable fun (i : I) => a (i, j)) : Multipliable fun (j : J) => tprod (fun (i : I) => a (i, j)) ⋯

Fubini rule (J-first version): the iterated product over J then I is multipliable. (Label: prop.fps.prods-mulable-rules.fubini1)

theorem PowerSeries.tprod_fubini_J {R : Type u_1} [CommRing R] {I : Type u_3} {J : Type u_4} {a : I × J → PowerSeries R} (ha : Multipliable a) (ha_J : ∀ (j : J), Multipliable fun (i : I) => a (i, j)) (ha_outer_J : Multipliable fun (j : J) => tprod (fun (i : I) => a (i, j)) ⋯ := ⋯) : tprod a ha = tprod (fun (j : J) => tprod (fun (i : I) => a (i, j)) ⋯) ha_outer_J

Fubini rule (J-first version): products over I × J can be computed as iterated products over J then I. (Label: prop.fps.prods-mulable-rules.fubini1)

theorem PowerSeries.tprod_fubini_full {R : Type u_1} [CommRing R] {I : Type u_3} {J : Type u_4} {a : I × J → PowerSeries R} (ha : Multipliable a) (ha_I : ∀ (i : I), Multipliable fun (j : J) => a (i, j)) (ha_J : ∀ (j : J), Multipliable fun (i : I) => a (i, j)) (ha_outer_I : Multipliable fun (i : I) => tprod (fun (j : J) => a (i, j)) ⋯ := ⋯) (ha_outer_J : Multipliable fun (j : J) => tprod (fun (i : I) => a (i, j)) ⋯ := ⋯) : tprod (fun (i : I) => tprod (fun (j : J) => a (i, j)) ⋯) ha_outer_I = tprod a ha ∧ tprod a ha = tprod (fun (j : J) => tprod (fun (i : I) => a (i, j)) ⋯) ha_outer_J

Full Fubini rule: products over I × J can be computed as iterated products in either order.

This combines both directions of the Fubini rule:

• ∏_{(i,j) ∈ I × J} a_{(i,j)} = ∏_{i ∈ I} ∏_{j ∈ J} a_{(i,j)}
• ∏_{(i,j) ∈ I × J} a_{(i,j)} = ∏_{j ∈ J} ∏_{i ∈ I} a_{(i,j)}

(Label: prop.fps.prods-mulable-rules.fubini1)

theorem PowerSeries.fubini_prod_invertible {R : Type u_1} [CommRing R] {I : Type u_3} {J : Type u_4} {a : I × J → PowerSeries R} (ha : Multipliable a) (ha_inv : ∀ (p : I × J), IsUnit ((coeff 0) (a p))) : (∀ (i : I), Multipliable fun (j : J) => a (i, j)) ∧ ∀ (j : J), Multipliable fun (i : I) => a (i, j)

Fubini rule for invertible FPS: no additional multipliability assumptions needed. (Label: prop.fps.prods-mulable-rules.fubini)

Approximator Properties

Proposition \ref{prop.fps.infprod-approx-xneq}

theorem PowerSeries.xn_approximator_superset {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {M : Finset I} {n : ℕ} (hM : IsXnApproximator a M n) {J : Finset I} (hMJ : M ⊆ J) (m : ℕ) (hm : m ≤ n) : (coeff m) (∏ i ∈ J, a i) = (coeff m) (∏ i ∈ M, a i)

If M is an x^n-approximator, then any finite superset J gives the same first n+1 coefficients. (Label: prop.fps.infprod-approx-xneq part (a))

theorem PowerSeries.tprod_coeff_eq_approximator {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} (ha : Multipliable a) {M : Finset I} {n : ℕ} (hM : IsXnApproximator a M n) (m : ℕ) (hm : m ≤ n) : (coeff m) (tprod a ha) = (coeff m) (∏ i ∈ M, a i)

For a multipliable family, the infinite product's coefficients match those of any approximator. (Label: prop.fps.infprod-approx-xneq part (b))

Approximator Properties in terms of x^n-equivalence

Proposition \ref{prop.fps.infprod-approx-xneq}

These are the same results as above, but stated using the xnEquiv relation (which says two FPS agree on coefficients 0 through n).

Note: The xnEquiv definition and basic lemmas (xnEquiv_refl, xnEquiv_symm, xnEquiv_trans) are imported from AlgebraicCombinatorics.FPS.Limits.

theorem PowerSeries.xn_approximator_superset_xnEquiv {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} {M : Finset I} {n : ℕ} (hM : IsXnApproximator a M n) {J : Finset I} (hMJ : M ⊆ J) : ∏ i ∈ J, a i ≡[x^n] ∏ i ∈ M, a i

If M is an x^n-approximator, then any finite superset J gives an x^n-equivalent finite product. (Label: prop.fps.infprod-approx-xneq part (a))

This is the x^n-equivalence form of the approximator property: for any finite J ⊇ M, we have ∏_{i∈J} a_i ≡[x^n] ∏_{i∈M} a_i.

theorem PowerSeries.tprod_xnEquiv_approximator {R : Type u_1} [CommRing R] {I : Type u_2} {a : I → PowerSeries R} (ha : Multipliable a) {M : Finset I} {n : ℕ} (hM : IsXnApproximator a M n) : tprod a ha ≡[x^n] ∏ i ∈ M, a i

For a multipliable family, the infinite product is x^n-equivalent to the product over any x^n-approximator. (Label: prop.fps.infprod-approx-xneq part (b))

This is the x^n-equivalence form: if M is an x^n-approximator for a multipliable family (a_i)_{i∈I}, then ∏_{i∈I} a_i ≡[x^n] ∏_{i∈M} a_i.