Infinite Products of Formal Power Series - Part 2

This file formalizes the second part of the detailed proofs for infinite products of formal power series, following the Details section of Loehr's "Bijective Combinatorics".

The main content includes:

• Product rules (generalized distributive laws) for infinite products
• Composition rules for infinite products with substitution
• Supporting lemmas about coefficient extraction and summability

Main Definitions

• PowerSeries.EssentiallyFinite: A family (k_i)_{i ∈ I} is essentially finite if all but finitely many entries equal 0.
• PowerSeries.SfinI: The set of essentially finite families in ∏_{i ∈ I} S_i.

Main Results

Product Rules (Generalized Distributive Laws)

• PowerSeries.prodRule_claim3: For (i,k) ∈ S̄ \ T'_n, we have [x^m] p_{i,k} = 0 for all m ∈ {0,1,...,n}. (Claim 3, label: pf.prop.fps.prodrule-fin-inf.Tm-def)
• PowerSeries.prodRule_claim4: If (k_i)_{i ∈ I} ∈ S^I_fin, then (p_{i,k_i})_{i ∈ I} is multipliable. (Claim 4)
• PowerSeries.prodRule_claim5: Under certain conditions, [x^n](∏_{i ∈ I} p_{i,k_i}) = 0. (Claim 5)
• PowerSeries.prodRule_claim6: For (k_i) ∈ S^I_fin \ S^I_{I_n}, the product coefficient vanishes. (Claim 6)
• PowerSeries.prodRule_claim7: The family (∏_{i ∈ I} p_{i,k_i}) indexed by essentially finite families is summable. (Claim 7)
• PowerSeries.prodRule_claim8: Coefficient reduction to finite index sets. (Claim 8)
• PowerSeries.prodRule_claim9: Coefficient vanishing for non-contributing terms. (Claim 9)
• PowerSeries.prodRule_claim10: Product reduction to finite index sets. (Claim 10)
• PowerSeries.prodRule_claim11: Finite product-sum interchange. (Claim 11)
• PowerSeries.prodRule_infInf: Main Proposition (prop.fps.prodrule-inf-inf) - The generalized distributive law for infinite products and infinite sums: ∏_{i ∈ I} ∑_{k ∈ S_i} p_{i,k} = ∑_{(k_i) ∈ S^I_fin} ∏_{i ∈ I} p_{i,k_i}

Composition Rules

• PowerSeries.comp_prod_finite: For finite I, (∏_{i ∈ I} f_i) ∘ g = ∏_{i ∈ I} (f_i ∘ g). (Lemma lem.fps.subs.rule-infprod-fin)
• PowerSeries.comp_prod_multipliable: If (f_i)_{i ∈ I} is multipliable and [x^0]g = 0, then (f_i ∘ g)_{i ∈ I} is multipliable. (Proposition prop.fps.subs.rule-infprod, part 1)
• PowerSeries.comp_prod_infinite: For multipliable (f_i)_{i ∈ I} with [x^0]g = 0, (∏_{i ∈ I} f_i) ∘ g = ∏_{i ∈ I} (f_i ∘ g). (Proposition prop.fps.subs.rule-infprod, part 2)

References

• [Loehr, Bijective Combinatorics, Details: Infinite Products (Part 2)]

Essentially Finite Families

A family (k_i)_{i ∈ I} indexed by a set I with values in ℕ is essentially finite if all but finitely many entries equal 0. This is the key concept for indexing summable families of products.

@[reducible, inline]

abbrev PowerSeries.EssentiallyFinite {I : Type u_2} (f : I → ℕ) : Prop

A family f : I → ℕ is essentially finite if all but finitely many values are 0. This corresponds to S^I_fin in the source.

This is an alias for the canonical _root_.EssentiallyFinite defined in FPS/InfiniteProducts2.lean. Both definitions are definitionally equal: {i | f i ≠ 0}.Finite = (Function.support f).Finite by definition.

For the full API (including _root_.EssentiallyFinite.add, _root_.EssentiallyFinite.neg, _root_.EssentiallyFinite.toFinsupp, etc.), see FPS/InfiniteProducts2.lean.

This version is specialized to ℕ for use in product rule proofs.

Equations

• PowerSeries.EssentiallyFinite f = EssentiallyFinite f

theorem PowerSeries.essentiallyFinite_iff_support_finite {I : Type u_2} (f : I → ℕ) : EssentiallyFinite f ↔ (Function.support f).Finite

EssentiallyFinite is equivalent to having finite support.

theorem PowerSeries.EssentiallyFinite.support_finite {I : Type u_2} {f : I → ℕ} (hf : EssentiallyFinite f) : {i : I | f i ≠ 0}.Finite

The support of an essentially finite family is finite. (Delegates to _root_.EssentiallyFinite.finite_support)

theorem PowerSeries.essentiallyFinite_zero {I : Type u_2} : EssentiallyFinite fun (x : I) => 0

The zero family is essentially finite. (Delegates to _root_.EssentiallyFinite.zero)

theorem PowerSeries.essentiallyFinite_of_finite_support {I : Type u_2} {f : I → ℕ} {s : Finset I} (hs : ∀ (i : I), f i ≠ 0 → i ∈ s) : EssentiallyFinite f

A family with finite support is essentially finite.

Summability and Multipliability for Product Rules

The following definitions and lemmas support the product rule proofs.

def PowerSeries.CoeffSupportSet {K : Type u_1} [CommRing K] {I : Type u_2} (p : I → ℕ → PowerSeries K) (m : ℕ) : Set (I × ℕ)

For a summable family (p_{i,k}), the set T_m of pairs (i,k) with nonzero [x^m] p_{i,k} is finite. This corresponds to equation (pf.prop.fps.prodrule-fin-inf.Tm-def). (label: pf.prop.fps.prodrule-fin-inf.Tm-def)

Equations

• PowerSeries.CoeffSupportSet p m = {ik : I × ℕ | ik.2 ≠ 0 ∧ (PowerSeries.coeff m) (p ik.1 ik.2) ≠ 0}

def PowerSeries.CoeffSupportSetUnion {K : Type u_1} [CommRing K] {I : Type u_2} (p : I → ℕ → PowerSeries K) (n : ℕ) : Set (I × ℕ)

The union of coefficient support sets up to degree n. This corresponds to T'_n = T_0 ∪ T_1 ∪ ... ∪ T_n.

Equations

• PowerSeries.CoeffSupportSetUnion p n = ⋃ m ∈ Finset.range (n + 1), PowerSeries.CoeffSupportSet p m

def PowerSeries.IndexSetIn {K : Type u_1} [CommRing K] {I : Type u_2} (p : I → ℕ → PowerSeries K) (n : ℕ) : Set I

The index set I_n of first components appearing in T'_n.

Equations

• PowerSeries.IndexSetIn p n = {i : I | ∃ (k : ℕ), (i, k) ∈ PowerSeries.CoeffSupportSetUnion p n}

def PowerSeries.ValueSetKn {K : Type u_1} [CommRing K] {I : Type u_2} (p : I → ℕ → PowerSeries K) (n : ℕ) : Set ℕ

The value set K_n of second components appearing in T'_n.

Equations

• PowerSeries.ValueSetKn p n = {k : ℕ | ∃ (i : I), (i, k) ∈ PowerSeries.CoeffSupportSetUnion p n}

Claim 3: Coefficient Vanishing Outside T'_n

For (i,k) ∈ S̄ \ T'_n, we have [x^m] p_{i,k} = 0 for all m ∈ {0,1,...,n}. (label: pf.prop.fps.prodrule-fin-inf.Tm-def)

theorem PowerSeries.prodRule_claim3 {K : Type u_1} [CommRing K] {I : Type u_2} (p : I → ℕ → PowerSeries K) (n : ℕ) (i : I) (k : ℕ) (hk : k ≠ 0) (hnotin : (i, k) ∉ CoeffSupportSetUnion p n) (m : ℕ) : m ≤ n → (coeff m) (p i k) = 0

Claim 3: If (i,k) is not in the coefficient support union up to n, then all coefficients up to degree n vanish. (Claim 3, label: pf.prop.fps.prodrule-fin-inf.Tm-def)

Claim 4: Multipliability of Product Families

If (k_i)_{i ∈ I} is essentially finite, then (p_{i,k_i})_{i ∈ I} is multipliable.

theorem PowerSeries.prodRule_claim4 {K : Type u_1} [CommRing K] {I : Type u_2} (p : I → ℕ → PowerSeries K) (hp0 : ∀ (i : I), p i 0 = 1) (k : I → ℕ) (hk : EssentiallyFinite k) : {i : I | p i (k i) ≠ 1}.Finite

Claim 4: For an essentially finite family (k_i) with p_{i,0} = 1, the family (p_{i,k_i}) is multipliable (all but finitely many terms are 1). (Claim 4)

Claim 5: Product Coefficient Vanishing

Under certain conditions on the index family, the product coefficient vanishes.

theorem PowerSeries.prodRule_claim5 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : I → ℕ → PowerSeries K) (n : ℕ) (k : I → ℕ) (_hk : EssentiallyFinite k) (_hp0 : ∀ (i : I), p i 0 = 1) (j : I) (hkj : k j ≠ 0) (hnotin : (j, k j) ∉ CoeffSupportSetUnion p n) (s : Finset I) : j ∈ s → (coeff n) (∏ i ∈ s, p i (k i)) = 0

Claim 5: If some j ∈ I satisfies (j, k_j) ∉ T'_n, then [x^n](∏_{i ∈ I} p_{i,k_i}) = 0. (Claim 5)

Claim 6: Product Coefficient Vanishing for Non-Contributing Families

For families outside S^I_{I_n}, the product coefficient vanishes.

theorem PowerSeries.prodRule_claim6 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : I → ℕ → PowerSeries K) (n : ℕ) (k : I → ℕ) (hk : EssentiallyFinite k) (hp0 : ∀ (i : I), p i 0 = 1) (j : I) (hj_notin : j ∉ IndexSetIn p n) (hkj : k j ≠ 0) (s : Finset I) : j ∈ s → (coeff n) (∏ i ∈ s, p i (k i)) = 0

Claim 6: If (k_i) ∈ S^I_fin \ S^I_{I_n} (i.e., some k_j ≠ 0 for j ∉ I_n), then [x^n](∏_{i ∈ I} p_{i,k_i}) = 0. (Claim 6)

Claim 7: Summability of Product Family

The family (∏_{i ∈ I} p_{i,k_i}) indexed by essentially finite (k_i) is summable.

theorem PowerSeries.prodRule_claim7 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : I → ℕ → PowerSeries K) (_hp0 : ∀ (i : I), p i 0 = 1) (n : ℕ) (_hTn_finite : (CoeffSupportSetUnion p n).Finite) (hIn_finite : (IndexSetIn p n).Finite) (hKn_finite : (ValueSetKn p n).Finite) : {k : I → ℕ | EssentiallyFinite k ∧ (∀ i ∉ hIn_finite.toFinset, k i = 0) ∧ (coeff n) (∏ i ∈ hIn_finite.toFinset, p i (k i)) ≠ 0}.Finite

Claim 7: The family (∏_{i ∈ I} p_{i,k_i}) indexed by essentially finite families (k_i)_{i ∈ I} ∈ S^I_fin supported on I_n is summable. That is, for each n ∈ ℕ, only finitely many essentially finite families (k_i) supported on I_n satisfy [x^n](∏_{i ∈ I_n} p_{i,k_i}) ≠ 0.

The proof shows that any k with nonzero coefficient must satisfy:

• Property 1: All i ∉ I_n satisfy k i = 0 (support contained in I_n) - explicit in statement
• Property 2: All i ∈ I_n satisfy k i ∈ K_n ∪ {0} These two properties restrict k to finitely many possibilities.

Note: Property 1 is made explicit in the statement since the product is over the finite set I_n. For the infinite product interpretation (with p_{i,0} = 1), this constraint follows from the fact that factors with k_i ≠ 0 for i ∉ I_n would have vanishing coefficients up to degree n, making the product coefficient zero (by Claim 5/6). (Claim 7)

Claim 8: Coefficient Reduction to Finite Index Sets

The coefficient of the sum over essentially finite families equals the coefficient of the sum over a finite index set.

def PowerSeries.extendFromFinset {I : Type u_2} [DecidableEq I] (In : Finset I) (f : ↥In → ℕ) : I → ℕ

Extend a function from a finite subset to the full type by setting values to 0 outside.

Equations

• PowerSeries.extendFromFinset In f i = if h : i ∈ In then f ⟨i, h⟩ else 0

def PowerSeries.restrictToFinset {I : Type u_2} (In : Finset I) (k : I → ℕ) (i : ↥In) : ℕ

Restrict a function to a finite subset.

Equations

• PowerSeries.restrictToFinset In k i = k ↑i

theorem PowerSeries.prodRule_claim8 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : I → ℕ → PowerSeries K) (n : ℕ) (_hp0 : ∀ (i : I), p i 0 = 1) (In : Finset I) (_hIn : ∀ i ∉ In, i ∉ IndexSetIn p n) (S : I → Finset ℕ) (_hS0 : ∀ (i : I), 0 ∈ S i) (essFinFamilies : Finset (I → ℕ)) (_hEss : ∀ k ∈ essFinFamilies, EssentiallyFinite k) (hSIn : ∀ k ∈ essFinFamilies, ∀ i ∉ In, k i = 0) (hValInS : ∀ k ∈ essFinFamilies, ∀ i ∈ In, k i ∈ S i) (hComplete : ∀ (k : I → ℕ), (∀ i ∉ In, k i = 0) → (∀ i ∈ In, k i ∈ S i) → k ∈ essFinFamilies) : (coeff n) (∑ k ∈ essFinFamilies, ∏ i ∈ In, p i (k i)) = (coeff n) (∑ f ∈ Fintype.piFinset fun (i : ↥In) => S ↑i, ∏ i : ↥In, p (↑i) (f i))

Claim 8: The coefficient of the sum over essentially finite families equals the coefficient of the sum over the finite index set I_n. [x^n](∑_{(k_i) ∈ S^I_fin} ∏_{i ∈ I} p_{i,k_i}) = [x^n](∑_{(k_i) ∈ S^{I_n}} ∏_{i ∈ I_n} p_{i,k_i}).

The proof establishes a bijection between essFinFamilies (functions that are 0 outside In and have values in S i for i ∈ In) and Fintype.piFinset (fun i : In => S i.1).

Note: The hypotheses hValInS and hComplete ensure that essFinFamilies is exactly the set of extensions of functions in the piFinset. These are needed to establish the bijection between the two index sets.

(Claim 8)

Claim 9: Sum Coefficient Vanishing

For i ∉ I_n, the sum ∑_{k ∈ S_i \ {0}} p_{i,k} has vanishing coefficients up to degree n.

theorem PowerSeries.prodRule_claim9 {K : Type u_1} [CommRing K] {I : Type u_2} (p : I → ℕ → PowerSeries K) (n : ℕ) (i : I) (hi : i ∉ IndexSetIn p n) (Si : Finset ℕ) (_hSi : 0 ∈ Si) (m : ℕ) : m ≤ n → (coeff m) (∑ k ∈ Si \ {0}, p i k) = 0

Claim 9: For i ∉ I_n, we have [x^m](∑_{k ∈ S_i \ {0}} p_{i,k}) = 0 for each m ∈ {0,1,...,n}. (Claim 9)

Claim 10: Product Reduction to Finite Index Sets

The product over I reduces to the product over I_n for coefficient extraction.

theorem PowerSeries.prodRule_claim10 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : I → ℕ → PowerSeries K) (n : ℕ) (hp0 : ∀ (i : I), p i 0 = 1) (In : Finset I) (hIn : ∀ i ∉ In, i ∉ IndexSetIn p n) (S : I → Finset ℕ) (hS0 : ∀ (i : I), 0 ∈ S i) (J : Finset I) (hInJ : In ⊆ J) : (coeff n) (∏ i ∈ J, ∑ k ∈ S i, p i k) = (coeff n) (∏ i ∈ In, ∑ k ∈ S i, p i k)

Claim 10: For any finite set J ⊇ I_n, the coefficient of the product over J equals the coefficient of the product over I_n: [x^n](∏_{i ∈ J} ∑_{k ∈ S_i} p_{i,k}) = [x^n](∏_{i ∈ I_n} ∑_{k ∈ S_i} p_{i,k}).

This captures the key property that the infinite product's coefficient stabilizes at I_n. In the source, this is stated as reducing ∏_{i ∈ I} to ∏_{i ∈ I_n}, which makes sense when I is infinite but the coefficient only depends on finitely many terms.

The proof uses:

1. For i ∈ J \ I_n, we have ∑_{k ∈ S_i} p_{i,k} = 1 + ∑_{k ∈ S_i \ {0}} p_{i,k}
2. By Claim 9, [x^m](∑_{k ∈ S_i \ {0}} p_{i,k}) = 0 for all m ≤ n when i ∉ I_n
3. By Lemma lem.fps.prod.irlv.inf, these factors don't affect the coefficient

(Claim 10)

Claim 11: Finite Product-Sum Interchange

For a finite index set, the product of sums equals the sum of products.

theorem PowerSeries.prodRule_claim11 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : I → ℕ → PowerSeries K) (In : Finset I) (S : I → Finset ℕ) : ∏ i ∈ In, ∑ k ∈ S i, p i k = ∑ f ∈ Fintype.piFinset fun (i : ↥In) => S ↑i, ∏ i : ↥In, p (↑i) (f i)

Claim 11: For finite I_n, ∏_{i ∈ I_n} ∑_{k ∈ S_i} p_{i,k} = ∑_{(k_i) ∈ S^{I_n}} ∏_{i ∈ I_n} p_{i,k_i}. (Claim 11)

Main Proposition: Infinite-Infinite Product Rule (Generalized Distributive Law)

This is the culmination of Claims 3-11. It states that for a summable family (p_{i,k}) with p_{i,0} = 1, the infinite product of infinite sums equals the sum over essentially finite families of products.

Proposition prop.fps.prodrule-inf-inf: ∏_{i ∈ I} ∑_{k ∈ S_i} p_{i,k} = ∑_{(k_i)_{i ∈ I} ∈ S^I_fin} ∏_{i ∈ I} p_{i,k_i}

def PowerSeries.SfinI {I : Type u_2} (S : I → Set ℕ) : Set (I → ℕ)

The set S^I_fin of essentially finite families in ∏_{i ∈ I} S_i.

Equations

• PowerSeries.SfinI S = {k : I → ℕ | (∀ (i : I), k i ∈ S i) ∧ PowerSeries.EssentiallyFinite k}

theorem PowerSeries.prodRule_finite_interchange {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : I → ℕ → PowerSeries K) (M : Finset I) (S : I → Finset ℕ) : ∏ i ∈ M, ∑ k ∈ S i, p i k = ∑ f ∈ Fintype.piFinset fun (i : ↥M) => S ↑i, ∏ i : ↥M, p (↑i) (f i)

Auxiliary: For finite index sets, the product-sum interchange (Claim 11). This is a direct consequence of prodRule_claim11.

theorem PowerSeries.prodRule_infInf {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : I → ℕ → PowerSeries K) (S : I → Set ℕ) (_hS0 : ∀ (i : I), 0 ∈ S i) (_hp0 : ∀ (i : I), p i 0 = 1) (_hSummable : ∀ (m : ℕ), {ik : I × ℕ | ik.2 ∈ S ik.1 ∧ ik.2 ≠ 0 ∧ (coeff m) (p ik.1 ik.2) ≠ 0}.Finite) (hMultipliable : ∀ (n : ℕ), ∃ (M : Finset I), ∀ (J : Finset I), M ⊆ J → ∀ (Sfin : I → Finset ℕ), (∀ (i : I), ↑(Sfin i) ⊆ S i) → (∀ (i : I), 0 ∈ Sfin i) → (coeff n) (∏ i ∈ J, ∑ k ∈ Sfin i, p i k) = (coeff n) (∏ i ∈ M, ∑ k ∈ Sfin i, p i k)) (n : ℕ) : ∃ (M_n : Finset I), (∀ (J : Finset I), M_n ⊆ J → ∀ (Sfin : I → Finset ℕ), (∀ (i : I), ↑(Sfin i) ⊆ S i) → (∀ (i : I), 0 ∈ Sfin i) → (coeff n) (∏ i ∈ J, ∑ k ∈ Sfin i, p i k) = (coeff n) (∏ i ∈ M_n, ∑ k ∈ Sfin i, p i k)) ∧ ∀ (Sfin : I → Finset ℕ), (∀ (i : I), ↑(Sfin i) ⊆ S i) → (∀ (i : I), 0 ∈ Sfin i) → (coeff n) (∏ i ∈ M_n, ∑ k ∈ Sfin i, p i k) = (coeff n) (∑ f ∈ Fintype.piFinset fun (i : ↥M_n) => Sfin ↑i, ∏ i : ↥M_n, p (↑i) (f i))

Main Proposition (prop.fps.prodrule-inf-inf): The generalized distributive law for infinite products and infinite sums of formal power series.

Given:

• An index set I
• For each i ∈ I, a set S_i ⊆ ℕ with 0 ∈ S_i
• A family (p_{i,k})_{(i,k) ∈ I × ℕ} of FPS with p_{i,0} = 1 for all i
• The family (p_{i,k})_{(i,k) ∈ S̄} is summable (where S̄ = {(i,k) | k ∈ S_i, k ≠ 0})
• The family (∑_{k ∈ S_i} p_{i,k})_{i ∈ I} is multipliable

Then for each coefficient n:

• The LHS [x^n](∏_{i ∈ I} ∑_{k ∈ S_i} p_{i,k}) is computed via the multipliability approximator
• The RHS [x^n](∑_{(k_i) ∈ S^I_fin} ∏_{i ∈ I} p_{i,k_i}) is computed via the finite index set I_n
• These coefficients are equal

The proof chain (for each n):

1. Claim 10: [x^n](∏_{i ∈ I} ∑_{k ∈ S_i} p_{i,k}) = [x^n](∏_{i ∈ I_n} ∑_{k ∈ S_i} p_{i,k})
2. Claim 11: ∏_{i ∈ I_n} ∑_{k ∈ S_i} p_{i,k} = ∑_{(k_i) ∈ S^{I_n}} ∏_{i ∈ I_n} p_{i,k_i}
3. Claim 8: [x^n](∑_{(k_i) ∈ S^{I_n}} ∏_{i ∈ I_n} p_{i,k_i}) = [x^n](∑_{(k_i) ∈ S^I_fin} ∏_{i ∈ I} p_{i,k_i})

Note on hypotheses: The hypotheses hS0, hp0, and hSummable are needed for the full proof of the source proposition (to construct I_n and prove Claims 3-10). In this formulation, we use hMultipliable which already encapsulates the stabilization property. The full proof would derive hMultipliable from hSummable and hp0. These hypotheses are retained here to match the source statement and to support future completion of the intermediate claims.

(Proposition prop.fps.prodrule-inf-inf)

theorem PowerSeries.prodRule_infInf_coeff {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : I → ℕ → PowerSeries K) (n : ℕ) (M : Finset I) (Sfin : I → Finset ℕ) : (coeff n) (∏ i ∈ M, ∑ k ∈ Sfin i, p i k) = (coeff n) (∑ f ∈ Fintype.piFinset fun (i : ↥M) => Sfin ↑i, ∏ i : ↥M, p (↑i) (f i))

Corollary: The coefficient equality form of the generalized distributive law. For any finite approximation of the index sets and value sets, the coefficient of the product of sums equals the coefficient of the sum of products.

This is a direct consequence of Claim 11 (finite product-sum interchange). (Proposition prop.fps.prodrule-inf-inf, coefficient form)

Composition Rules for Infinite Products

The following results establish that composition distributes over infinite products.

theorem PowerSeries.comp_prod_finite {K : Type u_1} [CommRing K] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (f : ι → PowerSeries K) (g : PowerSeries K) (hg : constantCoeff g = 0) : subst g (∏ i ∈ s, f i) = ∏ i ∈ s, subst g (f i)

Finite product composition rule: For finite I, (∏_{i ∈ I} f_i) ∘ g = ∏_{i ∈ I} (f_i ∘ g). This is proved by induction on |I|. (Lemma lem.fps.subs.rule-infprod-fin)

theorem PowerSeries.xnEquiv_comp {K : Type u_1} [CommRing K] {n : ℕ} {f₁ f₂ g : PowerSeries K} (hf : ∀ k ≤ n, (coeff k) f₁ = (coeff k) f₂) (hg : constantCoeff g = 0) (k : ℕ) : k ≤ n → (coeff k) (subst g f₁) = (coeff k) (subst g f₂)

x^n-equivalence is preserved under composition when the inner series has zero constant term. This is a consequence of Proposition prop.fps.xneq.comp.

theorem PowerSeries.comp_prod_approx_determines {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (f : I → PowerSeries K) (g : PowerSeries K) (hg : constantCoeff g = 0) (n : ℕ) (M : Finset I) (hM_approx : ∀ k ≤ n, ∀ (J : Finset I), M ⊆ J → (coeff k) (∏ i ∈ J, f i) = (coeff k) (∏ i ∈ M, f i)) (J : Finset I) : M ⊆ J → (coeff n) (∏ i ∈ J, subst g (f i)) = (coeff n) (∏ i ∈ M, subst g (f i))

Claim 1 for infinite product composition: An x^n-approximator for (f_i) determines the x^n-coefficient in the product of (f_i ∘ g). (Claim 1 in proof of prop.fps.subs.rule-infprod)

Note: An x^n-approximator is a finite subset M that determines the first n+1 coefficients in the product, i.e., for all k ≤ n and all J ⊇ M, coeff k (∏ i ∈ J, f i) = coeff k (∏ i ∈ M, f i).

theorem PowerSeries.comp_prod_multipliable {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (f : I → PowerSeries K) (g : PowerSeries K) (hg : constantCoeff g = 0) (hf_mulable : ∀ (n : ℕ), ∃ (M : Finset I), ∀ (J : Finset I), M ⊆ J → (coeff n) (∏ i ∈ J, f i) = (coeff n) (∏ i ∈ M, f i)) (n : ℕ) : ∃ (M : Finset I), ∀ (J : Finset I), M ⊆ J → (coeff n) (∏ i ∈ J, subst g (f i)) = (coeff n) (∏ i ∈ M, subst g (f i))

If (f_i)_{i ∈ I} is multipliable and [x^0]g = 0, then (f_i ∘ g)_{i ∈ I} is multipliable. (Proposition prop.fps.subs.rule-infprod, first part)

theorem PowerSeries.comp_prod_infinite {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (f : I → PowerSeries K) (g : PowerSeries K) (hg : constantCoeff g = 0) (hf_mulable : ∀ (n : ℕ), ∃ (M : Finset I), ∀ (J : Finset I), M ⊆ J → (coeff n) (∏ i ∈ J, f i) = (coeff n) (∏ i ∈ M, f i)) (prod_f : PowerSeries K) (hprod : ∀ (n : ℕ) (M : Finset I), (∀ (J : Finset I), M ⊆ J → (coeff n) (∏ i ∈ J, f i) = (coeff n) (∏ i ∈ M, f i)) → (coeff n) prod_f = (coeff n) (∏ i ∈ M, f i)) (n : ℕ) : ∃ (M : Finset I), (coeff n) (subst g prod_f) = (coeff n) (∏ i ∈ M, subst g (f i))

For multipliable (f_i)_{i ∈ I} with [x^0]g = 0, (∏_{i ∈ I} f_i) ∘ g = ∏_{i ∈ I} (f_i ∘ g). (Proposition prop.fps.subs.rule-infprod, second part)

The hypothesis hprod says that prod_f is the infinite product: for any approximator M (a finite set such that all supersets give the same coefficient), the coefficient of prod_f equals the coefficient of the finite product over M. This is stronger than just saying prod_f's coefficients can be computed by some finite product, and is necessary to ensure prod_f actually represents the infinite product.

Additional Supporting Lemmas

theorem PowerSeries.coeff_zero_of_dvd {K : Type u_1} [CommRing K] {n : ℕ} {u v : PowerSeries K} (hdvd : u ∣ v) (hu : ∀ m ≤ n, (coeff m) u = 0) (m : ℕ) : m ≤ n → (coeff m) v = 0

If u divides v and the first n+1 coefficients of u are zero, then the first n+1 coefficients of v are also zero. (Lemma lem.fps.prod.irlv.mul)

theorem PowerSeries.coeff_mul_one_add_of_lt_order {K : Type u_1} [CommRing K] {φ ψ : PowerSeries K} (n : ℕ) (h : ↑n < ψ.order) : (coeff n) (φ * (1 + ψ)) = (coeff n) φ

Helper lemma: if order(ψ) > n, then coeff n (φ * (1 + ψ)) = coeff n φ.

theorem PowerSeries.coeff_prod_one_plus_summable {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (a : PowerSeries K) (f : I → PowerSeries K) (n : ℕ) (hf_zero : ∀ (i : I), ∀ m ≤ n, (coeff m) (f i) = 0) (s : Finset I) (m : ℕ) : m ≤ n → (coeff m) (a * ∏ i ∈ s, (1 + f i)) = (coeff m) a

For a summable family (f_i)_{i ∈ I} with [x^m] f_i = 0 for all m ≤ n and i ∈ I, we have [x^m](a · ∏_{i ∈ I}(1 + f_i)) = [x^m] a for all m ≤ n. (Lemma lem.fps.prod.irlv.inf)