A.1 Details: Infinite products (part 1)
Fix a commutative ring \(K\).
A.1.1 Essentially finite families
A family \((k_i)_{i \in I}\) of natural numbers is essentially finite if all but finitely many entries equal \(0\), i.e., the set \(\{ i \in I : k_i \neq 0\} \) is finite. This corresponds to \(S^I_{\mathrm{fin}}\) in the source.
For a family \((p_{i,k})\) of FPSs, the coefficient support set \(T_m\) at degree \(m\) is the set \(\{ (i,k) : k \neq 0 \text{ and } [x^m] p_{i,k} \neq 0\} \).
The coefficient support union \(T'_n = T_0 \cup T_1 \cup \cdots \cup T_n\) is the union of coefficient support sets up to degree \(n\).
- PowerSeries.CoeffSupportSetUnion p n = ⋃ m ∈ Finset.range (n + 1), PowerSeries.CoeffSupportSet p m
The index set \(I_n\) is the set of first components appearing in \(T'_n\): \(I_n = \{ i \in I : \exists k,\; (i,k) \in T'_n\} \).
The value set \(K_n\) is the set of second components appearing in \(T'_n\): \(K_n = \{ k \in \mathbb {N} : \exists i,\; (i,k) \in T'_n\} \).
The set \(S^I_{\mathrm{fin}}\) of essentially finite families in \(\prod _{i \in I} S_i\) is the set of all families \((k_i)_{i \in I}\) such that \(k_i \in S_i\) for all \(i\) and the family \((k_i)\) is essentially finite.
Given a finite subset \(I_n \subseteq I\) and a function \(f : I_n \to \mathbb {N}\), extend from finset produces a function \(I \to \mathbb {N}\) by setting \(f(i)\) for \(i \in I_n\) and \(0\) otherwise. This is used in the bijection between essentially finite families supported on \(I_n\) and functions \(I_n \to S\).
- PowerSeries.extendFromFinset In f i = if h : i ∈ In then f ⟨i, h⟩ else 0
Given a finite subset \(I_n \subseteq I\) and a function \(k : I \to \mathbb {N}\), restrict to finset produces the restriction \(k|_{I_n} : I_n \to \mathbb {N}\). This is the inverse direction of the bijection used in Claim 8.
- PowerSeries.restrictToFinset In k i = k ↑i
A.1.2 Existence of approximators
For a multipliable family \((\mathbf{a}_i)_{i \in I}\) and any \(n \in \mathbb {N}\), there exists an \(x^n\)-approximator \(M\) for \((\mathbf{a}_i)_{i \in I}\). The proof takes the union of finite sets \(M_0, M_1, \ldots , M_n\) where each \(M_k\) determines the \(x^k\)-coefficient.
A.1.3 Multipliability criteria
If \((f_i)_{i \in I}\) is a family of FPSs such that for each \(n\), the set \(\{ i \in I : [x^n] f_i \neq 0\} \) is finite (i.e., the family is coefficient-wise summable), then the family \((1 + f_i)_{i \in I}\) is multipliable.
The proof constructs an approximator \(M\) as the union of the finite sets \(\{ i : [x^m] f_i \neq 0\} \) for \(m = 0, 1, \ldots , n\), and shows that multiplying by \((1 + f_i)\) for \(i \notin M\) does not change coefficients up to degree \(n\).
If \((a_i)_{i \in I}\) is a family of FPSs such that \(\{ i \in I : a_i \neq 1\} \) is finite, then the family is multipliable. The finite support set itself serves as a determining set for every coefficient.
If \(J \subseteq I\) and both the subfamily \((a_i)_{i \in J}\) and the subfamily \((a_i)_{i \in I \setminus J}\) are multipliable, then the full family \((a_i)_{i \in I}\) is multipliable. The proof combines \(x^n\)-approximators for the two subfamilies.
A.1.4 Multipliable product and division rules (Lean formalization)
If \((\mathbf{a}_i)_{i \in I}\) and \((\mathbf{b}_i)_{i \in I}\) are both multipliable, then the pointwise product family \((\mathbf{a}_i \cdot \mathbf{b}_i)_{i \in I}\) is multipliable. The proof takes \(M = U \cup V\) where \(U\) and \(V\) are \(x^n\)-approximators for the two families.
Under the hypotheses of Theorem A.13, the infinite product of the pointwise product equals the product of the two infinite products:
If \((\mathbf{a}_i)_{i \in I}\) and \((\mathbf{b}_i)_{i \in I}\) are multipliable and each \(\mathbf{b}_i\) has invertible constant term, then the family \((\mathbf{a}_i \cdot \mathbf{b}_i^{-1})_{i \in I}\) is multipliable.
Under the hypotheses of Theorem A.15,
A.1.5 Subfamily and reindexing lemmas
If \(U\) is an \(x^n\)-approximator for a family \((\mathbf{a}_i)_{i \in I}\) of invertible FPSs and \(J \subseteq I\), then \(U \cap J\) (as a preimage under the subtype embedding) is an \(x^n\)-approximator for the subfamily \((\mathbf{a}_i)_{i \in J}\). This is the Lean formalization of Lemma 1.368, using the invertibility hypothesis to cancel factors outside \(J\).
If \((\mathbf{a}_i)_{i \in I}\) is multipliable and each \(\mathbf{a}_i\) has invertible constant term, then for any \(J \subseteq I\), the subfamily \((\mathbf{a}_i)_{i \in J}\) is multipliable.
If \(f : S \to T\) is a bijection and \((\mathbf{a}_t)_{t \in T}\) is multipliable, then \((\mathbf{a}_{f(s)})_{s \in S}\) is multipliable.
Under the hypotheses of Theorem A.19, the reindexed infinite product equals the original: \(\prod _{s \in S} \mathbf{a}_{f(s)} = \prod _{t \in T} \mathbf{a}_t\).
A.1.6 Fiber product decomposition
Let \(f : S \to W\) be a map, and \((\mathbf{a}_s)_{s \in S}\) a multipliable family. Suppose that for each \(w \in W\), the fiber subfamily \((\mathbf{a}_s)_{s \in f^{-1}(w)}\) is multipliable. Then the family of fiber products \(\bigl(\prod _{s \in f^{-1}(w)} \mathbf{a}_s\bigr)_{w \in W}\) is multipliable. The proof uses \(f(U)\) (the image of an \(x^n\)-approximator \(U\)) as the approximator for the outer product.
A.1.7 Fubini rules for infinite products
Let \((\mathbf{a}_{(i,j)})_{(i,j) \in I \times J}\) be a multipliable family. Suppose that for each \(i \in I\), the row family \((\mathbf{a}_{(i,j)})_{j \in J}\) is multipliable. Then the family of row products \(\bigl(\prod _{j \in J} \mathbf{a}_{(i,j)}\bigr)_{i \in I}\) is multipliable.
Under the hypotheses of Theorem A.23,
This is the Fubini rule for infinite products of FPSs.
If \((\mathbf{a}_{(i,j)})_{(i,j) \in I \times J}\) is a multipliable family of invertible FPSs (each has unit constant term), then both the row families \((\mathbf{a}_{(i,j)})_{j \in J}\) for each \(i\) and the column families \((\mathbf{a}_{(i,j)})_{i \in I}\) for each \(j\) are multipliable. No additional multipliability hypotheses are needed in the invertible case, because subfamilies of invertible multipliable families are automatically multipliable.
A.1.8 Coefficient form of the generalized distributive law
For any finite set \(M \subseteq I\) and finite value sets \((S_i)_{i \in M}\),
This is a direct corollary of Claim 11 (finite product-sum interchange).
A.1.9 Congruence lemma for division
Let \(a, b, c, d \in K\left[\left[x\right]\right]\) be four FPSs such that \(c\) and \(d\) are invertible. Let \(n \in \mathbb {N}\). Assume that
Assume further that
Then,
We have assumed that
In other words, \(a \overset {x^n}{\equiv } b\) (by the definition of the relation \(\overset {x^n}{\equiv }\)). Similarly, \(c \overset {x^n}{\equiv } d\). Hence, by the compatibility of \(\overset {x^n}{\equiv }\) with division (Theorem 1.328 (e)), we obtain \(\frac{a}{c} \overset {x^n}{\equiv } \frac{b}{d}\). In other words,
(by the definition of the relation \(\overset {x^n}{\equiv }\)). This proves Lemma A.27.
A.1.10 Detailed proof of Proposition 1.367
A.1.11 Approximator intersection lemma
Let \(\left(\mathbf{a}_{i}\right)_{i \in I} \in K\left[\left[x\right]\right]^{I}\) be a family of invertible FPSs. Let \(J\) be a subset of \(I\). Let \(n \in \mathbb {N}\). Let \(U\) be an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in I}\). Then, \(U \cap J\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in J}\).
The set \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in I}\). In other words, \(U\) is a finite subset of \(I\) that determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in I}\) (by the definition of an \(x^n\)-approximator). Hence, in particular, \(U\) is finite. Moreover, \(U \subseteq I\) (since \(U\) is a subset of \(I\)).
Let \(M = U \cap J\). Thus, \(M = U \cap J \subseteq U\), so that the set \(M\) is finite (since \(U\) is finite). Moreover, \(M\) is a subset of \(J\) (since \(M = U \cap J \subseteq J\)).
Now, let \(N\) be a finite subset of \(J\) satisfying \(M \subseteq N \subseteq J\). We shall show that
Indeed, the set \(N \cup U\) is finite (since \(N\) and \(U\) are finite) and is a subset of \(I\) (since \(N \subseteq J \subseteq I\) and \(U \subseteq I\)); it also satisfies \(U \subseteq N \cup U \subseteq I\). Now, we recall that \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in I}\). Hence, Proposition 1.364 (a) (applied to \(U\) and \(N \cup U\) instead of \(M\) and \(J\)) yields
(since \(N \cup U\) is a finite subset of \(I\) satisfying \(U \subseteq N \cup U \subseteq I\)).
On the other hand, we have assumed that \(\left(\mathbf{a}_{i}\right)_{i \in I}\) is a family of invertible FPSs. Thus, for each \(i \in I\), the FPS \(\mathbf{a}_{i}\) is invertible, so that its inverse \(\mathbf{a}_{i}^{-1}\) is well-defined. We obviously have
(since the relation \(\overset {x^n}{\equiv }\) is reflexive).
Hence, by the compatibility of \(\overset {x^n}{\equiv }\) with multiplication (Theorem 1.328 (b)), applied to \(a = \prod _{i \in N \cup U} \mathbf{a}_{i}\) and \(b = \prod _{i \in U} \mathbf{a}_{i}\) and \(c = \prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\) and \(d = \prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\), we obtain
On the other hand, the sets \(N\) and \(U \setminus J\) are disjoint (since \(N \subseteq J\) and \(U \setminus J \subseteq J^c\)), and their union is \(N \cup (U \setminus J) = N \cup U\) (since \(U = (U \cap J) \cup (U \setminus J)\) and \(U \cap J = M \subseteq N\)). Hence, the set \(N \cup U\) is the union of its two disjoint subsets \(N\) and \(U \setminus J\). Thus, we can split the product \(\prod _{i \in N \cup U} \mathbf{a}_{i}\) as follows:
Multiplying both sides of this equality by \(\prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\), we obtain
However, the set \(U\) is the union of its two disjoint subsets \(U \cap J\) and \(U \setminus J\). Thus, we can split the product \(\prod _{i \in U} \mathbf{a}_{i}\) as follows:
Multiplying both sides by \(\prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\), we obtain
Substituting these two simplifications into the \(x^n\)-equivalence above, we obtain
In other words, each \(m \in \left\{ 0, 1, \ldots , n\right\} \) satisfies
(by the definition of \(\overset {x^n}{\equiv }\)).
Forget that we fixed \(N\). We have thus shown that every finite subset \(N\) of \(J\) satisfying \(M \subseteq N \subseteq J\) satisfies the above equality for each \(m \in \left\{ 0, 1, \ldots , n\right\} \).
Now, let \(m \in \left\{ 0, 1, \ldots , n\right\} \). Then, every finite subset \(N\) of \(J\) satisfying \(M \subseteq N \subseteq J\) satisfies
In other words, the set \(M\) determines the \(x^m\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) (by the definition of “determining the \(x^m\)-coefficient in a product”).
Forget that we fixed \(m\). We thus have shown that \(M\) determines the \(x^m\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) for each \(m \in \left\{ 0, 1, \ldots , n\right\} \). In other words, \(M\) determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\). In other words, \(M\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in J}\) (by the definition of an “\(x^n\)-approximator”, since \(M\) is a finite subset of \(J\)). In other words, \(U \cap J\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in J}\) (since \(M = U \cap J\)). This proves Lemma A.28.
A.1.12 Detailed proof of Proposition 1.369
Let \(J\) be a subset of \(I\). We shall show that the family \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is multipliable.
Fix \(n \in \mathbb {N}\). We know that the family \(\left(\mathbf{a}_{i}\right)_{i \in I}\) is multipliable. Hence, there exists an \(x^n\)-approximator \(U\) for \(\left(\mathbf{a}_{i}\right)_{i \in I}\) (by Lemma 1.363). Consider this \(U\).
Set \(M = U \cap J\). Lemma A.28 yields that \(U \cap J\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in J}\). In other words, \(M\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in J}\) (since \(M = U \cap J\)). In other words, \(M\) is a finite subset of \(J\) that determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) (by the definition of an \(x^n\)-approximator). Thus, the set \(M\) determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\). Hence, in particular, this set \(M\) determines the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\). Therefore, the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is finitely determined (by the definition of “finitely determined”, since \(M\) is a finite subset of \(J\)).
Forget that we fixed \(n\). We thus have proved that for each \(n \in \mathbb {N}\), the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is finitely determined. In other words, each coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is finitely determined. In other words, the family \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is multipliable (by the definition of “multipliable”).
Forget that we fixed \(J\). We thus have shown that the family \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is multipliable whenever \(J\) is a subset of \(I\). In other words, any subfamily of \(\left(\mathbf{a}_{i}\right)_{i \in I}\) is multipliable. This proves Proposition 1.369.
A.1.13 Finite products and \(x^n\)-equivalence
Let \(n \in \mathbb {N}\). Let \(V\) be a finite set. Let \(\left(c_{w}\right)_{w \in V} \in K\left[\left[x\right]\right]^{V}\) and \(\left(d_{w}\right)_{w \in V} \in K\left[\left[x\right]\right]^{V}\) be two families of FPSs such that
Then, we have
This is just Theorem 1.328 (f) (the part about products), with the letters \(S\), \(s\), \(a_s\), and \(b_s\) renamed as \(V\), \(w\), \(c_w\), and \(d_w\).
A.1.14 Detailed proof of Proposition 1.372
We shall subdivide our proof into several claims.
Claim 1: Let \(w \in W\). Then, the family \(\left(\mathbf{a}_{s}\right)_{s \in S,\; f(s) = w}\) is multipliable.
[Proof of Claim 1: This was an assumption of Proposition 1.372.]
Let us set
This is well-defined, because for each \(w \in W\), the product \(\prod _{\substack{[s, , \in , S, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s}\) is well-defined (since Claim 1 shows that the family \(\left(\mathbf{a}_{s}\right)_{s \in S,\; f(s) = w}\) is multipliable).
Now, let \(n \in \mathbb {N}\). By Lemma 1.363 (applied to \(S\) and \(\left(\mathbf{a}_{s}\right)_{s \in S}\) instead of \(I\) and \(\left(\mathbf{a}_{i}\right)_{i \in I}\)), there exists an \(x^n\)-approximator for \(\left(\mathbf{a}_{s}\right)_{s \in S}\). Pick such an \(x^n\)-approximator, and call it \(U\). Then, \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{s}\right)_{s \in S}\); in other words, \(U\) is a finite subset of \(S\) that determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{s}\right)_{s \in S}\) (by the definition of an \(x^n\)-approximator).
The set \(U\) is finite. Thus, its image \(f(U) = \left\{ f(u) \mid u \in U\right\} \) is finite as well. Now, we claim the following:
Claim 2: For each \(w \in W\), we have
[Proof of Claim 2: Let \(w \in W\). Let \(J\) be the subset \(\left\{ s \in S \mid f(s) = w\right\} \) of \(S\). Then, the family \(\left(\mathbf{a}_{s}\right)_{s \in J}\) is just the family \(\left(\mathbf{a}_{s}\right)_{s \in S,\; f(s) = w}\), and thus is multipliable (by Claim 1). Furthermore, Lemma A.28 (applied to \(S\) and \(\left(\mathbf{a}_{s}\right)_{s \in S}\) instead of \(I\) and \(\left(\mathbf{a}_{i}\right)_{i \in I}\)) yields that \(U \cap J\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{s}\right)_{s \in J}\) (since \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{s}\right)_{s \in S}\)). Hence, Proposition 1.364 (b) (applied to \(J\), \(\left(\mathbf{a}_{s}\right)_{s \in J}\) and \(U \cap J\) instead of \(I\), \(\left(\mathbf{a}_{i}\right)_{i \in I}\) and \(M\)) yields
However, we have \(J = \left\{ s \in S \mid f(s) = w\right\} \). Thus, \(\prod _{s \in J} \mathbf{a}_{s} = \prod _{\substack{[s, , \in , S, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s} = \mathbf{b}_w\) and \(U \cap J = \left\{ s \in U \mid f(s) = w\right\} \). So the product sign “\(\prod _{s \in U \cap J}\)” is equivalent to “\(\prod _{\substack{[s, , \in , U, ;, \\ , , f, (, s, ), , =, , w]}}\)”. Thus,
This proves Claim 2.]
Claim 3: The set \(f(U)\) determines the \(x^n\)-coefficient in the product of \(\left(\mathbf{b}_{w}\right)_{w \in W}\).
[Proof of Claim 3: Let \(T\) be a finite subset of \(W\) satisfying \(f(U) \subseteq T\). We must show that \(\left[x^n\right] \left(\prod _{w \in T} \mathbf{b}_w\right) = \left[x^n\right] \left(\prod _{w \in f(U)} \mathbf{b}_w\right)\).
By Claim 2, for each \(w \in W\) we have \(\mathbf{b}_{w} \overset {x^n}{\equiv } \prod _{\substack{[s, , \in , U, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s}\). Hence, by Lemma A.29, we get
and similarly
Now, for \(w \notin f(U)\), there are no \(s \in U\) with \(f(s) = w\), so the inner product is \(1\) (the empty product). Hence, for any finite set \(V \supseteq f(U)\),
(by the standard fiberwise reindexing of finite products). Applying this to both \(V = T\) and \(V = f(U)\), we conclude that both products equal \(\prod _{s \in U} \mathbf{a}_{s}\). Therefore,
This proves Claim 3.]
From Claim 3, the \(x^n\)-coefficient in the product of \(\left(\mathbf{b}_w\right)_{w \in W}\) is finitely determined (since \(f(U)\) is a finite subset of \(W\)). Since this holds for each \(n \in \mathbb {N}\), the family \(\left(\mathbf{b}_w\right)_{w \in W}\) is multipliable. This proves part (a) of Proposition 1.372.
For part (b), we observe that by Proposition 1.364 (b), the infinite product \(\prod _{s \in S} \mathbf{a}_s\) is \(x^n\)-equivalent to \(\prod _{s \in U} \mathbf{a}_s\). By the computation above, the infinite product \(\prod _{w \in W} \mathbf{b}_w\) is also \(x^n\)-equivalent to \(\prod _{s \in U} \mathbf{a}_s\). Since this holds for all \(n\), the two infinite products are equal.
A.1.15 Detailed proof of Proposition 1.366
(a) Fix \(n \in \mathbb {N}\). We know that the family \(\left(\mathbf{a}_{i}\right)_{i \in I}\) is multipliable. Hence, there exists an \(x^n\)-approximator \(U\) for \(\left(\mathbf{a}_{i}\right)_{i \in I}\) (by Lemma 1.363). Consider this \(U\).
We also know that the family \(\left(\mathbf{b}_{i}\right)_{i \in I}\) is multipliable. Hence, there exists an \(x^n\)-approximator \(V\) for \(\left(\mathbf{b}_{i}\right)_{i \in I}\) (by Lemma 1.363, applied to \(\mathbf{b}_{i}\) instead of \(\mathbf{a}_{i}\)). Consider this \(V\).
We know that \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in I}\). In other words, \(U\) is a finite subset of \(I\) that determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in I}\) (by the definition of an \(x^n\)-approximator). Hence, in particular, \(U\) is finite. Similarly, \(V\) is finite. Moreover, \(U \subseteq I\); similarly, \(V \subseteq I\).
Let \(M = U \cup V\). This set \(M\) is finite (since \(U\) and \(V\) are finite). Moreover, \(M = U \cup V \subseteq I \cup I = I\). Hence, \(M\) is a finite subset of \(I\).
Now, let \(N\) be a finite subset of \(I\) satisfying \(M \subseteq N \subseteq I\). We shall show that
Indeed, let \(m \in \left\{ 0, 1, \ldots , n\right\} \). We have \(U \subseteq U \cup V = M \subseteq N\). The set \(N\) is a finite subset of \(I\) and satisfies \(U \subseteq N\). Now, recall that \(U\) determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in I}\). Hence, \(U\) determines the \(x^m\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in I}\) (since \(m \in \left\{ 0, 1, \ldots , n\right\} \)). In other words, every finite subset \(T\) of \(I\) satisfying \(U \subseteq T \subseteq I\) satisfies
We can apply this to \(T = N\) (since \(N\) is a finite subset of \(I\) satisfying \(U \subseteq N \subseteq I\)), and thus obtain
However, we can also apply it to \(T = M\) (since \(M\) is a finite subset of \(I\) satisfying \(U \subseteq M \subseteq I\)), and thus obtain
Comparing these two equalities, we obtain
The same argument (applied to \(\mathbf{b}_{i}\) and \(V\) instead of \(\mathbf{a}_{i}\) and \(U\)) yields
Forget that we fixed \(m\). We thus have proved these equalities for each \(m \in \left\{ 0, 1, \ldots , n\right\} \). Hence, Lemma 1.346 (applied to \(a = \prod _{i \in N} \mathbf{a}_{i}\) and \(b = \prod _{i \in M} \mathbf{a}_{i}\) and \(c = \prod _{i \in N} \mathbf{b}_{i}\) and \(d = \prod _{i \in M} \mathbf{b}_{i}\)) yields that
for each \(m \in \left\{ 0, 1, \ldots , n\right\} \). Applying this to \(m = n\), we obtain
In view of
this rewrites as
Forget that we fixed \(N\). We thus have shown that every finite subset \(N\) of \(I\) satisfying \(M \subseteq N \subseteq I\) satisfies the above equality. In other words, \(M\) determines the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\) (by the definition of “determining the \(x^n\)-coefficient”). Hence, the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\) is finitely determined (since \(M\) is a finite subset of \(I\)).
Forget that we fixed \(n\). We thus have proved that for each \(n \in \mathbb {N}\), the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\) is finitely determined. In other words, the family \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\) is multipliable. This proves Proposition 1.366 (a).
(b) Proposition 1.366 (a) shows that the family \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\) is multipliable.
Let \(n \in \mathbb {N}\). In our above proof of Proposition 1.366 (a), we have seen the following:
There exists an \(x^n\)-approximator \(U\) for \(\left(\mathbf{a}_{i}\right)_{i \in I}\).
There exists an \(x^n\)-approximator \(V\) for \(\left(\mathbf{b}_{i}\right)_{i \in I}\).
Consider these \(U\) and \(V\). Let \(M = U \cup V\). Thus, \(M = U \cup V \supseteq U\) and \(M = U \cup V \supseteq V\). In our above proof, we have seen that \(M\) is a finite subset of \(I\) and \(M\) determines the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\).
We recall that the relation \(\overset {x^n}{\equiv }\) is an equivalence relation (by Theorem 1.328 (a)).
Now, the definition of the infinite product \(\prod _{i \in I} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\) (namely, Definition 1.343 (b)) yields that
(since \(M\) is a finite subset of \(I\) that determines the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\)). On the other hand, the set \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in I}\). Thus, Proposition 1.364 (b) (applied to \(U\) instead of \(M\)) yields
Since the relation \(\overset {x^n}{\equiv }\) is symmetric, we thus obtain \(\prod _{i \in U} \mathbf{a}_{i} \overset {x^n}{\equiv } \prod _{i \in I} \mathbf{a}_{i}\). Moreover, \(M\) is a finite subset of \(I\) satisfying \(U \subseteq M\); hence, Proposition 1.364 (a) yields
Hence, \(\prod _{i \in M} \mathbf{a}_{i} \overset {x^n}{\equiv } \prod _{i \in I} \mathbf{a}_{i}\) (since the relation \(\overset {x^n}{\equiv }\) is transitive). The same argument (applied to \(\left(\mathbf{b}_{i}\right)_{i \in I}\) and \(V\) instead of \(\left(\mathbf{a}_{i}\right)_{i \in I}\) and \(U\)) yields \(\prod _{i \in M} \mathbf{b}_{i} \overset {x^n}{\equiv } \prod _{i \in I} \mathbf{b}_{i}\). From these two \(x^n\)-equivalences, we obtain
(by Theorem 1.328 (b)). In view of
this rewrites as
In other words,
Applying this to \(m = n\), we obtain
In view of \(\left[x^{n}\right] \left(\prod _{i \in I} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right) = \left[x^{n}\right] \left(\prod _{i \in M} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right)\), this rewrites as
Now, forget that we fixed \(n\). We thus have proved that each \(n \in \mathbb {N}\) satisfies the above equality. In other words, each coefficient of the FPS \(\prod _{i \in I} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\) equals the corresponding coefficient of \(\left(\prod _{i \in I} \mathbf{a}_{i}\right) \left(\prod _{i \in I} \mathbf{b}_{i}\right)\). Hence, we have
This proves Proposition 1.366 (b).
A.1.16 Product rule claims
(Claim 3.) If \((i,k) \notin T'_n\) (the coefficient support union up to \(n\)) and \(k \neq 0\), then \([x^m] p_{i,k} = 0\) for all \(m \in \{ 0,1,\ldots ,n\} \).
If \([x^m] p_{i,k} \neq 0\) for some \(m \leq n\), then \((i,k) \in T_m \subseteq T'_n\), contradicting the hypothesis.
(Claim 4.) If \((k_i)_{i \in I}\) is essentially finite and \(p_{i,0} = 1\) for all \(i\), then the family \((p_{i,k_i})_{i \in I}\) is multipliable.
All but finitely many \(i \in I\) satisfy \(k_i = 0\) (since \((k_i)_{i \in I}\) is essentially finite) and thus \(p_{i,k_i} = p_{i,0} = 1\). Hence, all but finitely many entries of the family \((p_{i,k_i})_{i \in I}\) equal \(1\). Thus, this family is multipliable (by Proposition 1.351).
(Claim 5.) If some \(j \in I\) satisfies \(k_j \neq 0\) and \((j, k_j) \notin T'_n\), then \([x^n](\prod _{i \in s} p_{i,k_i}) = 0\) for any finite \(s \ni j\).
The product \(\prod _{i \in s} p_{i,k_i}\) is a multiple of \(p_{j,k_j}\) (since \(p_{j,k_j}\) is one of the factors of this product). Moreover, by Claim 3, we have \([x^m] p_{j,k_j} = 0\) for each \(m \in \{ 0,1,\ldots ,n\} \). Hence, Lemma A.42 (applied to \(u = p_{j,k_j}\) and \(v = \prod _{i \in s} p_{i,k_i}\)) shows that \([x^m](\prod _{i \in s} p_{i,k_i}) = 0\) for each \(m \in \{ 0,1,\ldots ,n\} \). Applying this to \(m = n\) yields the claim.
(Claim 6.) If \(j \notin I_n\) and \(k_j \neq 0\), then \([x^n](\prod _{i \in s} p_{i,k_i}) = 0\) for any finite \(s \ni j\).
We have \(k_j \in S_j\) and \(k_j \neq 0\), so \((j, k_j) \in \overline{S}\). Moreover, \((j, k_j) \notin T'_n\) (because if we had \((j, k_j) \in T'_n\), then we would have \(j \in I_n\) by the definition of \(I_n\); but this would contradict \(j \notin I_n\)). Hence, \((j, k_j) \in \overline{S} \setminus T'_n\). Therefore, Claim 5 yields \([x^n](\prod _{i \in s} p_{i,k_i}) = 0\).
(Claim 7.) The family \((\prod _{i \in I_n} p_{i,k_i})\) indexed by essentially finite families \((k_i)\) supported on \(I_n\) is summable: for each \(n\), only finitely many such families yield \([x^n](\prod _{i \in I_n} p_{i,k_i}) \neq 0\).
Let \((k_i)_{i \in I} \in S^I_{\mathrm{fin}}\) satisfy \([x^n](\prod _{i \in I} p_{i,k_i}) \neq 0\). Then it must satisfy two properties: (1) all \(i \in I \setminus I_n\) satisfy \(k_i = 0\) (otherwise Claim 6 would give a contradiction); (2) all \(i \in I_n\) satisfy \(k_i \in K_n \cup \{ 0\} \) (otherwise \((j, k_j) \in \overline{S} \setminus T'_n\) for some \(j \in I_n\), and Claim 5 would give a contradiction). These two properties together restrict \((k_i)\) to finitely many possibilities (since the sets \(I_n\) and \(K_n \cup \{ 0\} \) are finite). Hence, all but finitely many families yield \([x^n](\prod _{i \in I} p_{i,k_i}) = 0\), proving summability.
(Claim 9.) For \(i \notin I_n\), we have \([x^m](\sum _{k \in S_i \setminus \{ 0\} } p_{i,k}) = 0\) for each \(m \in \{ 0,1,\ldots ,n\} \).
Each term \(p_{i,k}\) with \(k \neq 0\) has \([x^m] p_{i,k} = 0\) by Claim 3 (since \((i,k) \notin T'_n\) because \(i \notin I_n\)).
(Claim 10.) For any finite set \(J \supseteq I_n\), \([x^n](\prod _{i \in J} \sum _{k \in S_i} p_{i,k}) = [x^n](\prod _{i \in I_n} \sum _{k \in S_i} p_{i,k})\). The product stabilizes at \(I_n\).
For \(i \in J \setminus I_n\), we have \(\sum _{k \in S_i} p_{i,k} = 1 + \sum _{k \in S_i \setminus \{ 0\} } p_{i,k}\). By Claim 9, the remainder has zero coefficients up to degree \(n\), so multiplying by it does not change the coefficient at degree \(n\).
(Claim 11.) For a finite index set \(I_n\),
This is the standard finite distributive law (product of sums equals sum of products).
This is the standard finite distributive law (product of sums equals sum of products over all choice functions). See Proposition 1.383.
(Claim 8.) The coefficient of the sum over essentially finite families equals the coefficient of the sum restricted to the finite index set \(I_n\):
The proof establishes a bijection between essentially finite families supported on \(I_n\) and functions \(I_n \to S\), via restriction and extension by \(0\).
A.1.17 Composition rules for infinite products
If \(f_1 \overset {x^n}{\equiv } f_2\) and \([x^0]g = 0\), then \(f_1 \circ g \overset {x^n}{\equiv } f_2 \circ g\). That is, \(x^n\)-equivalence is preserved under composition with a fixed inner series.
The coefficient \([x^k](f \circ g)\) involves a sum over \(d\) of \([x^d]f \cdot [x^k](g^d)\). For \(d {\gt} k\), \([x^k](g^d) = 0\) since \(\operatorname {ord}(g^d) \geq d {\gt} k\). For \(d \leq k \leq n\), \([x^d]f_1 = [x^d]f_2\) by \(x^n\)-equivalence.
If \(M\) is an \(x^n\)-approximator for \((f_i)_{i \in I}\) (i.e., for all \(k \leq n\) and \(J \supseteq M\), \([x^k](\prod _{i \in J} f_i) = [x^k](\prod _{i \in M} f_i)\)), and \([x^0]g = 0\), then for all \(J \supseteq M\), \([x^n](\prod _{i \in J} (f_i \circ g)) = [x^n](\prod _{i \in M} (f_i \circ g))\).
If \((f_i)_{i \in I}\) is multipliable and \([x^0]g = 0\), then \((f_i \circ g)_{i \in I}\) is multipliable.
For each \(n\), combine the approximators for degrees \(0, 1, \ldots , n\) into a single approximator \(M\) (their union), then apply Lemma A.40.
A.1.18 Additional supporting lemmas
If \(u \mid v\) and \([x^m] u = 0\) for all \(m \leq n\), then \([x^m] v = 0\) for all \(m \leq n\).
Write \(v = u \cdot w\). Then \([x^m] v = \sum _{(i,j) \in \mathrm{antidiag}(m)} [x^i] u \cdot [x^j] w\). Since \(i \leq m \leq n\), we have \([x^i] u = 0\), so each term vanishes.