A.4 Details: Limits of FPSs
A.4.1 Detailed proof of Lemma 1.462
We have \(\lim _{i\to \infty } f_i = f\). In other words, the sequence \((f_i)_{i\in \mathbb {N}}\) coefficientwise stabilizes to \(f\). In other words, for each \(n\in \mathbb {N}\),
(by the definition of “coefficientwise stabilizing”).
Now, let \(n\in \mathbb {N}\). Furthermore, let \(k\in \{ 0,1,\ldots ,n\} \). Then, the sequence \(\bigl([x^k] f_i\bigr)_{i\in \mathbb {N}}\) stabilizes to \([x^k] f\) (by 6, applied to \(k\) instead of \(n\)). In other words, there exists some \(N\in \mathbb {N}\) such that
(by the definition of “stabilizing”). Let us denote this \(N\) by \(N_k\). Thus,
Forget that we fixed \(k\). Thus, for each \(k\in \{ 0,1,\ldots ,n\} \), we have defined an integer \(N_k\in \mathbb {N}\) for which 7 holds. Altogether, we have thus defined \(n+1\) integers \(N_0, N_1, \ldots , N_n \in \mathbb {N}\).
Let us set \(P := \max \{ N_0, N_1, \ldots , N_n\} \). Then, of course, \(P\in \mathbb {N}\).
Now, let \(i\geq P\) be an integer. Then, for each \(k\in \{ 0,1,\ldots ,n\} \), we have \(i\geq P = \max \{ N_0, N_1, \ldots , N_n\} \geq N_k\) (since \(k\in \{ 0,1,\ldots ,n\} \)) and therefore \([x^k] f_i = [x^k] f\) (by 7). In other words, each \(k\in \{ 0,1,\ldots ,n\} \) satisfies \([x^k] f_i = [x^k] f\). Renaming the variable \(k\) as \(m\) in this result, we obtain the following:
In other words, \(f_i \overset {x^n}{\equiv } f\) (by the definition of \(x^n\)-equivalence).
Forget that we fixed \(i\). We thus have shown that all integers \(i\geq P\) satisfy \(f_i \overset {x^n}{\equiv } f\). Hence, there exists some integer \(N\in \mathbb {N}\) such that
(namely, \(N = P\)). This proves Lemma 1.462.
A.4.2 Detailed proof of Proposition 1.463
Let \((f_i)_{i\in \mathbb {N}}\) be a sequence of FPSs that coefficientwise stabilizes to an FPS \(f\), and let \(n\in \mathbb {N}\). Then there exists an integer \(K\in \mathbb {N}\) such that
This follows directly from Lemma 1.462 applied to the sequence \((f_i)\) and limit \(f\).
Let \((g_i)_{i\in \mathbb {N}}\) be a sequence of FPSs that coefficientwise stabilizes to an FPS \(g\), and let \(n\in \mathbb {N}\). Then there exists an integer \(L\in \mathbb {N}\) such that
Let \((f_i)_{i\in \mathbb {N}}\) and \((g_i)_{i\in \mathbb {N}}\) be sequences of FPSs that coefficientwise stabilize to \(f\) and \(g\) respectively, and let \(n\in \mathbb {N}\). Then there exists an integer \(P\in \mathbb {N}\) such that for all \(i\geq P\),
By Lemma A.85, there exists \(K\) such that \(f_i \overset {x^n}{\equiv } f\) for all \(i\geq K\). By Lemma A.86, there exists \(L\) such that \(g_i \overset {x^n}{\equiv } g\) for all \(i\geq L\). Set \(P := \max \{ K, L\} \). Then for all \(i\geq P\), both \(i\geq K\) and \(i\geq L\) hold, so both equivalences hold.
Recall that \(\lim _{i\to \infty } f_i = f\). Hence, Lemma 1.462 shows that there exists some integer \(N\in \mathbb {N}\) such that
Let us denote this \(N\) by \(K\). Hence, all integers \(i\geq K\) satisfy \(f_i \overset {x^n}{\equiv } f\).
Thus, we have found an integer \(K\in \mathbb {N}\) such that
Similarly, using \(\lim _{i\to \infty } g_i = g\), we can find an integer \(L\in \mathbb {N}\) such that
Consider these \(K\) and \(L\). Let us furthermore set \(P := \max \{ K, L\} \). Thus, \(P\in \mathbb {N}\).
We shall now show that each integer \(i\geq P\) satisfies \([x^n](f_i g_i) = [x^n](fg)\).
Indeed, let \(i\geq P\) be an integer. Then, \(f_i \overset {x^n}{\equiv } f\) (since \(i\geq P = \max \{ K, L\} \geq K\)), whereas \(g_i \overset {x^n}{\equiv } g\) (since \(i\geq P = \max \{ K, L\} \geq L\)). Hence, we obtain
(by the multiplicativity of \(x^n\)-equivalence, i.e., Theorem 1.328 (b)). In other words,
(by the definition of \(x^n\)-equivalence). Applying this to \(m = n\), we find
Forget that we fixed \(i\). We thus have shown that all integers \(i\geq P\) satisfy \([x^n](f_i g_i) = [x^n](fg)\). Hence, there exists some \(N\in \mathbb {N}\) such that
(namely, \(N = P\)). In other words,
(by the definition of “stabilizes”).
Forget that we fixed \(n\). We thus have shown that for each \(n\in \mathbb {N}\), the sequence \(\bigl([x^n](f_i g_i)\bigr)_{i\in \mathbb {N}}\) stabilizes to \([x^n](fg)\). In other words, the sequence \((f_i g_i)_{i\in \mathbb {N}}\) coefficientwise stabilizes to \(fg\) (by the definition of “coefficientwise stabilizing”). In other words, \(\lim _{i\to \infty }(f_i g_i) = fg\).
The same argument—but using the additivity of \(x^n\)-equivalence instead of the multiplicativity—shows that \(\lim _{i\to \infty }(f_i + g_i) = f + g\). Thus, the proof of Proposition 1.463 is complete.
If \((f_i)\) coefficientwise stabilizes to \(f\) and \((g_i)\) coefficientwise stabilizes to \(g\), then \((f_i + g_i)\) coefficientwise stabilizes to \(f + g\).
For each \(n\in \mathbb {N}\):
By Lemma 1.462, obtain \(K_f\) such that \(f_i \overset {x^n}{\equiv } f\) for \(i\geq K_f\), and \(K_g\) such that \(g_i \overset {x^n}{\equiv } g\) for \(i\geq K_g\).
Set \(P := \max \{ K_f, K_g\} \).
For \(i\geq P\), by the additivity of \(x^n\)-equivalence, \(f_i + g_i \overset {x^n}{\equiv } f + g\).
Extracting the \(n\)-th coefficient: \([x^n](f_i + g_i) = [x^n](f + g)\).
If \((f_i)\) coefficientwise stabilizes to \(f\) and \((g_i)\) coefficientwise stabilizes to \(g\), then \((f_i \cdot g_i)\) coefficientwise stabilizes to \(f \cdot g\).
For each \(n\in \mathbb {N}\):
By Lemma 1.462, obtain \(K_f\) such that \(f_i \overset {x^n}{\equiv } f\) for \(i\geq K_f\), and \(K_g\) such that \(g_i \overset {x^n}{\equiv } g\) for \(i\geq K_g\).
Set \(P := \max \{ K_f, K_g\} \).
For \(i\geq P\), by the multiplicativity of \(x^n\)-equivalence, \(f_i \cdot g_i \overset {x^n}{\equiv } f \cdot g\).
Extracting the \(n\)-th coefficient: \([x^n](f_i \cdot g_i) = [x^n](f \cdot g)\).
A.4.3 Helpers for Proposition 1.468
Let \(f, g \in K[[x]]\) with \(f \overset {x^n}{\equiv } g\), and let \(u, v\) be units in \(K\) with \(u = v\) as elements. Then the formal inverse of \(f\) with respect to \(u\) is \(x^n\)-equivalent to the formal inverse of \(g\) with respect to \(v\).
Let \(a \overset {x^n}{\equiv } b\) and \(c \overset {x^n}{\equiv } d\), where \(c\) and \(d\) are invertible with constant terms \(u\) and \(v\) respectively. Then \(a \cdot c^{-1} \overset {x^n}{\equiv } b \cdot d^{-1}\).
If \((g_i)\) coefficientwise stabilizes to \(g\) and each \(g_i\) has invertible constant term, then eventually the unit associated to the constant term of \(g_i\) equals the unit associated to the constant term of \(g\).
If \((g_i)\) coefficientwise stabilizes to \(g\) and each \(g_i\) has invertible constant term, then the sequence of formal inverses \((g_i^{-1})_{i \in \mathbb {N}}\) coefficientwise stabilizes to \(g^{-1}\). The proof proceeds by strong induction on the coefficient index, using the recursive formula for coefficients of the formal inverse.
A.4.4 Detailed proof of Proposition 1.468
First, let us show that \(g\) is invertible:
Claim 1: The FPS \(g\in K[[x]]\) is invertible.
We have assumed that \(\lim _{i\to \infty } g_i = g\). In other words, the sequence \((g_i)_{i\in \mathbb {N}}\) coefficientwise stabilizes to \(g\). In other words, for each \(n\in \mathbb {N}\), the sequence \(\bigl([x^n] g_i\bigr)_{i\in \mathbb {N}}\) stabilizes to \([x^n] g\) (by the definition of “coefficientwise stabilizing”). Applying this to \(n = 0\), we see that the sequence \(\bigl([x^0] g_i\bigr)_{i\in \mathbb {N}}\) stabilizes to \([x^0] g\). In other words, there exists some \(N\in \mathbb {N}\) such that
(by the definition of “stabilizes”). Consider this \(N\). Thus, all integers \(i\geq N\) satisfy \([x^0] g_i = [x^0] g\). Applying this to \(i = N\), we obtain \([x^0] g_N = [x^0] g\).
However, each FPS \(g_i\) is invertible (by assumption). Hence, in particular, the FPS \(g_N\) is invertible. By Proposition 1.111 (applied to \(a = g_N\)), this entails that its constant term \([x^0] g_N\) is invertible in \(K\). In other words, \([x^0] g\) is invertible in \(K\) (since \([x^0] g_N = [x^0] g\)).
But the FPS \(g\) is invertible if and only if its constant term \([x^0] g\) is invertible in \(K\) (by Proposition 1.111, applied to \(a = g\)). Hence, \(g\) is invertible (since its constant term \([x^0] g\) is invertible in \(K\)). This proves Claim 1.
It remains to prove that \(\lim _{i\to \infty } \frac{f_i}{g_i} = \frac{f}{g}\).
Recall that \(\lim _{i\to \infty } f_i = f\). Hence, Lemma 1.462 shows that there exists some integer \(N\in \mathbb {N}\) such that
Let us denote this \(N\) by \(K\). Hence, all integers \(i\geq K\) satisfy \(f_i \overset {x^n}{\equiv } f\).
Thus, we have found an integer \(K\in \mathbb {N}\) such that
Similarly, using \(\lim _{i\to \infty } g_i = g\), we can find an integer \(L\in \mathbb {N}\) such that
Consider these \(K\) and \(L\). Let us furthermore set \(P := \max \{ K, L\} \). Thus, \(P\in \mathbb {N}\).
We shall now show that each integer \(i\geq P\) satisfies \([x^n] \frac{f_i}{g_i} = [x^n] \frac{f}{g}\).
Indeed, let \(i\geq P\) be an integer. Then, \(f_i \overset {x^n}{\equiv } f\) (since \(i\geq P = \max \{ K, L\} \geq K\)), whereas \(g_i \overset {x^n}{\equiv } g\) (since \(i\geq P = \max \{ K, L\} \geq L\)). Since both FPSs \(g_i\) and \(g\) are invertible (by Claim 1), we thus obtain
(by Theorem 1.328 (e), applied to \(a = f_i\), \(b = f\), \(c = g_i\) and \(d = g\)). In other words,
(by the definition of \(x^n\)-equivalence). Applying this to \(m = n\), we find
Forget that we fixed \(i\). We thus have shown that all integers \(i\geq P\) satisfy \([x^n] \frac{f_i}{g_i} = [x^n] \frac{f}{g}\). Hence, there exists some \(N\in \mathbb {N}\) such that
(namely, \(N = P\)). In other words,
(by the definition of “stabilizes”).
Forget that we fixed \(n\). We thus have shown that for each \(n\in \mathbb {N}\), the sequence \(\left([x^n] \frac{f_i}{g_i}\right)_{i\in \mathbb {N}}\) stabilizes to \([x^n] \frac{f}{g}\). In other words, the sequence \(\left(\frac{f_i}{g_i}\right)_{i\in \mathbb {N}}\) coefficientwise stabilizes to \(\frac{f}{g}\) (by the definition of “coefficientwise stabilizing”). In other words, \(\lim _{i\to \infty } \frac{f_i}{g_i} = \frac{f}{g}\). This proves Proposition 1.468 (since we already have shown that \(g\) is invertible).
A.4.5 Detailed proof of Theorem 1.475
The family \((f_n)_{n\in \mathbb {N}}\) is summable. In other words, the family \((f_k)_{k\in \mathbb {N}}\) is summable (since this is the same family as \((f_n)_{n\in \mathbb {N}}\)). In other words, for each \(n\in \mathbb {N}\),
(by the definition of “summable”).
Let us define
Let us furthermore set
Now, fix \(n\in \mathbb {N}\). Then, all but finitely many \(k\in \mathbb {N}\) satisfy \([x^n] f_k = 0\) (by 8). In other words, there exists a finite subset \(J\) of \(\mathbb {N}\) such that
Consider this subset \(J\). The set \(J\) is a finite set of nonnegative integers, and thus has an upper bound. In other words, there exists some \(m\in \mathbb {N}\) such that
Consider this \(m\).
Let \(k\in \mathbb {N}\) be such that \(k\geq m+1\). If we had \(k\in J\), then we would have \(k\leq m\) (by 12), which would contradict \(k\geq m+1 {\gt} m\). Thus, we cannot have \(k\in J\). Hence, \(k\in \mathbb {N}\setminus J\) (since \(k\in \mathbb {N}\) but not \(k\in J\)). Therefore, 11 yields \([x^n] f_k = 0\).
Forget that we fixed \(k\). We thus have shown that
Now, let \(i\) be an integer such that \(i\geq m\). Then, \(i\in \mathbb {N}\) (since \(i\geq m\geq 0\)) and \(i+1\geq m+1\) (since \(i\geq m\)). From \(g = \sum _{k\in \mathbb {N}} f_k\), we obtain
On the other hand, from \(g_i = \sum _{k=0}^{i} f_k\), we obtain
Comparing this with 14, we obtain \([x^n] g_i = [x^n] g\).
Forget that we fixed \(i\). We thus have shown that
Hence, there exists some \(N\in \mathbb {N}\) such that
(namely, \(N = m\)). In other words, the sequence \(\bigl([x^n] g_i\bigr)_{i\in \mathbb {N}}\) stabilizes to \([x^n] g\) (by the definition of “stabilizes”).
Forget that we fixed \(n\). We thus have shown that for each \(n\in \mathbb {N}\),
In other words, the sequence \((g_i)_{i\in \mathbb {N}}\) coefficientwise stabilizes to \(g\). In other words, \(\lim _{i\to \infty } g_i = g\). In view of 9 and 10, we can rewrite this as
Renaming the summation index \(k\) as \(n\) everywhere in this equality, we can rewrite it as
This proves Theorem 1.475.
A.4.6 Helpers for Theorem 1.476
Let \(f \in K[[x]]\) satisfy \([x^k] f = \delta _{k,0}\) for all \(k \le n\) (i.e., \(f \equiv 1 \pmod{x^{n+1}}\)). Then for any \(g \in K[[x]]\) and any \(k \le n\),
The proof expands the product coefficient as a sum over the antidiagonal and observes that only the term with second component \(0\) survives, since \([x^j] f = 0\) for \(0 {\lt} j \le n\).
If \(f_m \equiv 1 \pmod{x^{n+1}}\), then for any \(k \le n\),
That is, extending a partial product by one more term that is \(1 + O(x^{n+1})\) does not change the first \(n+1\) coefficients.
For a multipliable family \((f_j)\), if \(f_j \equiv 1 \pmod{x^{n+1}}\) for all \(j \ge N\), then for all \(i \ge N\) and \(k \le n\),
The proof proceeds by induction on \(i\), repeatedly applying Lemma A.95.
For a multipliable family \((f_j)\), for each \(n \in \mathbb {N}\), there exists \(N\) such that for all \(i \ge N\),
This is the key stabilization lemma that directly implies Theorem 1.476.
A.4.7 Detailed proof of Theorem 1.476
The family \((f_n)_{n\in \mathbb {N}}\) is multipliable. In other words, each coefficient in the product of this family is finitely determined (by the definition of “multipliable”).
Let us define
Let us furthermore set
Now, fix \(n\in \mathbb {N}\). Then, the \(x^n\)-coefficient in the product of the family \((f_k)_{k\in \mathbb {N}}\) is finitely determined. In other words, there is a finite subset \(M\) of \(\mathbb {N}\) that determines the \(x^n\)-coefficient in the product of \((f_k)_{k\in \mathbb {N}}\). Consider this subset \(M\).
The set \(M\) is a finite set of nonnegative integers, and thus has an upper bound. In other words, there exists some \(m\in \mathbb {N}\) such that
Consider this \(m\).
Now, let \(i\) be an integer such that \(i\geq m\). Then, \(i\in \mathbb {N}\) (since \(i\geq m\geq 0\)) and \(m\leq i\). From 17, we see that all \(k\in M\) satisfy \(k\leq m\leq i\) and therefore \(k\in \{ 0,1,\ldots ,i\} \). In other words, \(M\subseteq \{ 0,1,\ldots ,i\} \).
However, the set \(M\) determines the \(x^n\)-coefficient in the product of \((f_k)_{k\in \mathbb {N}}\). In other words, every finite subset \(J\) of \(\mathbb {N}\) satisfying \(M\subseteq J\subseteq \mathbb {N}\) satisfies
(by the definition of “determines the \(x^n\)-coefficient in the product of \((f_k)_{k\in \mathbb {N}}\)”). Applying this to \(J = \{ 0,1,\ldots ,i\} \), we obtain
(since \(\{ 0,1,\ldots ,i\} \) is a finite subset of \(\mathbb {N}\) satisfying \(M\subseteq \{ 0,1,\ldots ,i\} \subseteq \mathbb {N}\)).
Moreover, the definition of the product of the multipliable family \((f_k)_{k\in \mathbb {N}}\) shows that
(since \(M\) is a finite subset of \(\mathbb {N}\) that determines the \(x^n\)-coefficient in the product of \((f_k)_{k\in \mathbb {N}}\)). Comparing this with 18, we find
In view of \(\prod _{k\in \{ 0,1,\ldots ,i\} } f_k = \prod _{k=0}^{i} f_k = g_i\) (by 15) and \(\prod _{k\in \mathbb {N}} f_k = g\) (by 16), we can rewrite this as
Forget that we fixed \(i\). We thus have shown that
Hence, the sequence \(\bigl([x^n] g_i\bigr)_{i\in \mathbb {N}}\) stabilizes to \([x^n] g\).
Forget that we fixed \(n\). We thus have shown that for each \(n\in \mathbb {N}\), the sequence \(\bigl([x^n] g_i\bigr)_{i\in \mathbb {N}}\) stabilizes to \([x^n] g\). In other words, the sequence \((g_i)_{i\in \mathbb {N}}\) coefficientwise stabilizes to \(g\). In other words, \(\lim _{i\to \infty } g_i = g\). In view of 15 and 16, we can rewrite this as
Renaming the product index \(k\) as \(n\) everywhere in this equality, we can rewrite it as
This proves Theorem 1.476.
A.4.8 Detailed proofs of Corollary 1.477
Let a FPS \(a\in K[[x]]\) be written in the form \(a = \sum _{n\in \mathbb {N}} a_n x^n\) with \(a_n\in K\). Then, the family \((a_n x^n)_{n\in \mathbb {N}}\) is summable. Hence, Theorem 1.475 (applied to \(f_n = a_n x^n\)) yields
In other words, \(a = \lim _{i\to \infty } \sum _{n=0}^{i} a_n x^n\). This proves Corollary 1.477.
A.4.9 Detailed proof of Theorem 1.478
Let us define
We have assumed that the limit \(\lim _{i\to \infty } \sum _{n=0}^{i} f_n\) exists. Let us denote this limit by \(g\). Thus,
In other words, the sequence \((g_i)_{i\in \mathbb {N}}\) coefficientwise stabilizes to \(g\). In other words, for each \(n\in \mathbb {N}\),
Let \(n\in \mathbb {N}\). Then, the sequence \(\bigl([x^n] g_i\bigr)_{i\in \mathbb {N}}\) stabilizes to \([x^n] g\) (by 21). In other words, there exists some \(N\in \mathbb {N}\) such that
Consider this \(N\). Let \(M\) be the set \(\{ 0,1,\ldots ,N\} \); this is a finite subset of \(\mathbb {N}\).
Let \(i\in \mathbb {N}\setminus M\). Thus,
In other words, \(i\) is a nonnegative integer with \(i\geq N+1\). Hence, \(i-1\geq N\). Therefore, 22 (applied to \(i-1\) instead of \(i\)) yields \([x^n] g_{i-1} = [x^n] g\). But 22 also yields \([x^n] g_i = [x^n] g\) (since \(i\geq N+1\geq N\)). Comparing these two equalities, we find
However, 19 yields
Moreover, 19 (applied to \(i-1\) instead of \(i\)) yields \(g_{i-1} = \sum _{k=0}^{i-1} f_k\). In view of this, we can rewrite 24 as
Hence, \([x^n] g_i = [x^n](f_i + g_{i-1}) = [x^n] f_i + \underbrace{[x^n] g_{i-1}}_{\substack{[=, , [, x, ^, n, ], , g, _, i, , \\ , , \text , {, (, b, y, ~, \eqref , {, p, f, ., t, h, m, ., f, p, s, ., l, i, m, ., s, u, m, -, l, i, m, -, c, o, n, v, ., 2, }, ), }]}} = [x^n] f_i + [x^n] g_i\). Subtracting \([x^n] g_i\) from both sides of this equality, we find \(0 = [x^n] f_i\). In other words, \([x^n] f_i = 0\).
Forget that we fixed \(i\). We thus have shown that all \(i\in \mathbb {N}\setminus M\) satisfy \([x^n] f_i = 0\). Hence, all but finitely many \(i\in \mathbb {N}\) satisfy \([x^n] f_i = 0\) (since all but finitely many \(i\in \mathbb {N}\) belong to \(\mathbb {N}\setminus M\) because the set \(M\) is finite). Renaming the index \(i\) as \(k\) in this statement, we obtain the following: All but finitely many \(k\in \mathbb {N}\) satisfy \([x^n] f_k = 0\).
Forget that we fixed \(n\). We thus have shown that for each \(n\in \mathbb {N}\),
In other words, the family \((f_n)_{n\in \mathbb {N}}\) is summable (by the definition of “summable”).
Hence, Theorem 1.475 yields \(\lim _{i\to \infty } \sum _{n=0}^{i} f_n = \sum _{n\in \mathbb {N}} f_n\). In other words, \(\sum _{n\in \mathbb {N}} f_n = \lim _{i\to \infty } \sum _{n=0}^{i} f_n\). This completes the proof of Theorem 1.478.
A.4.10 Helpers for Theorem 1.479
If \(f_i\) has constant term \(1\) for every \(i\) in a finite set \(S\), then \(\prod _{i \in S} f_i\) also has constant term \(1\).
A.4.11 Detailed proof of Theorem 1.479
Let us define
We have assumed that the limit \(\lim _{i\to \infty } \prod _{n=0}^{i} f_n\) exists. Let us denote this limit by \(g\). Thus,
Let \(n\in \mathbb {N}\) be arbitrary. Lemma 1.462 (applied to \(g_i\) and \(g\) instead of \(f_i\) and \(f\)) shows that there exists some integer \(N\in \mathbb {N}\) such that
(since \(g = \lim _{i\to \infty } g_i\)). Consider this \(N\).
Let \(M = \{ 0,1,\ldots ,N\} \). Thus, \(M\) is a finite subset of \(\mathbb {N}\). We shall show that this subset \(M\) determines the \(x^n\)-coefficient in the product of \((f_k)_{k\in \mathbb {N}}\).
For this purpose, we first observe that \(M = \{ 0,1,\ldots ,N\} \), so that
(since \(g_N\) was defined to be \(\prod _{k=0}^{N} f_k\)). Applying 27 to \(i = N\), we obtain \(g_N \overset {x^n}{\equiv } g\) (since \(N\geq N\)). Therefore, \(g \overset {x^n}{\equiv } g_N\) (since \(\overset {x^n}{\equiv }\) is an equivalence relation and thus symmetric).
Next, we shall show two claims:
Claim 1: For each integer \(j {\gt} N\), we have \(g \overset {x^n}{\equiv } g f_j\).
Let \(j {\gt} N\) be an integer. Thus, \(j\geq N+1\), so that \(j-1\geq N\). Hence, 27 (applied to \(i = j-1\)) yields \(g_{j-1} \overset {x^n}{\equiv } g\). However, 27 (applied to \(i = j\)) yields \(g_j \overset {x^n}{\equiv } g\) (since \(j\geq N+1\geq N\)). Thus, \(g \overset {x^n}{\equiv } g_j\) (by symmetry).
Also, we obviously have \(f_j \overset {x^n}{\equiv } f_j\) (by reflexivity).
However, the definition of \(g_{j-1}\) yields \(g_{j-1} = \prod _{k=0}^{j-1} f_k\). Furthermore, the definition of \(g_j\) yields
But recall that \(g_{j-1} \overset {x^n}{\equiv } g\) and \(f_j \overset {x^n}{\equiv } f_j\). Hence, \(g_{j-1} f_j \overset {x^n}{\equiv } g f_j\) (by the multiplicativity of \(x^n\)-equivalence). In view of \(g_j = g_{j-1} f_j\), we can rewrite this as \(g_j \overset {x^n}{\equiv } g f_j\).
Now, recall that \(g \overset {x^n}{\equiv } g_j\). Thus, \(g \overset {x^n}{\equiv } g_j \overset {x^n}{\equiv } g f_j\), so that \(g \overset {x^n}{\equiv } g f_j\) (by transitivity). This proves Claim 1.
Claim 2: If \(U\) is any finite subset of \(\mathbb {N}\) satisfying \(M\subseteq U\), then \(g \overset {x^n}{\equiv } \prod _{k\in U} f_k\).
We induct on the nonnegative integer \(|U\setminus M|\):
Base case: Let us check that Claim 2 holds when \(|U\setminus M| = 0\).
Indeed, let \(U\) be any finite subset of \(\mathbb {N}\) satisfying \(M\subseteq U\) and \(|U\setminus M| = 0\). Then, \(U\setminus M = \varnothing \) (since \(|U\setminus M| = 0\)), so that \(U\subseteq M\). Combined with \(M\subseteq U\), this yields \(U = M\). Thus, \(\prod _{k\in U} f_k = \prod _{k\in M} f_k = g_N\) (by 28). But we have already proved that \(g \overset {x^n}{\equiv } g_N\). In other words, \(g \overset {x^n}{\equiv } \prod _{k\in U} f_k\) (since \(\prod _{k\in U} f_k = g_N\)). This completes the base case.
Induction step: Let \(s\in \mathbb {N}\). Assume (as the induction hypothesis) that Claim 2 holds when \(|U\setminus M| = s\). We must now prove that Claim 2 holds when \(|U\setminus M| = s+1\).
Indeed, let \(U\) be any finite subset of \(\mathbb {N}\) satisfying \(M\subseteq U\) and \(|U\setminus M| = s+1\). Then, the set \(U\setminus M\) is nonempty (since \(|U\setminus M| = s+1 {\gt} 0\)). Hence, there exists some \(u\in U\setminus M\). Consider this \(u\). By the induction hypothesis (applied to \(U\setminus \{ u\} \) instead of \(U\)), we obtain \(g \overset {x^n}{\equiv } \prod _{k\in U\setminus \{ u\} } f_k\).
However, \(u\in U\setminus M\), so \(u\notin M = \{ 0,1,\ldots ,N\} \), which gives \(u {\gt} N\). Hence, Claim 1 (applied to \(j = u\)) yields \(g \overset {x^n}{\equiv } g f_u\).
We have \(g \overset {x^n}{\equiv } \prod _{k\in U\setminus \{ u\} } f_k\) and \(f_u \overset {x^n}{\equiv } f_u\). Hence, \(g f_u \overset {x^n}{\equiv } \left(\prod _{k\in U\setminus \{ u\} } f_k\right) f_u\) (by the multiplicativity of \(x^n\)-equivalence). In view of \(\prod _{k\in U} f_k = \left(\prod _{k\in U\setminus \{ u\} } f_k\right) f_u\), we can rewrite this as \(g f_u \overset {x^n}{\equiv } \prod _{k\in U} f_k\).
Now, recall that \(g \overset {x^n}{\equiv } g f_u\). Thus, \(g \overset {x^n}{\equiv } g f_u \overset {x^n}{\equiv } \prod _{k\in U} f_k\), so \(g \overset {x^n}{\equiv } \prod _{k\in U} f_k\) (by transitivity). This completes the induction step. Thus, Claim 2 is proved by induction.
Now, let \(J\) be a finite subset of \(\mathbb {N}\) satisfying \(M\subseteq J\subseteq \mathbb {N}\). Then, \(g \overset {x^n}{\equiv } \prod _{k\in J} f_k\) (by Claim 2, applied to \(U = J\)). In other words,
(by the definition of \(x^n\)-equivalence). Applying this to \(m = n\), we find
The same argument can be applied to \(M\) instead of \(J\) (since \(M\subseteq M\subseteq \mathbb {N}\)), and thus yields
Comparing these two equalities, we find
Forget that we fixed \(J\). We have now shown that every finite subset \(J\) of \(\mathbb {N}\) satisfying \(M\subseteq J\subseteq \mathbb {N}\) satisfies
In other words, the set \(M\) determines the \(x^n\)-coefficient in the product of \((f_k)_{k\in \mathbb {N}}\). Hence, the \(x^n\)-coefficient in the product of \((f_k)_{k\in \mathbb {N}}\) is finitely determined (since \(M\) is a finite subset of \(\mathbb {N}\)).
Forget that we fixed \(n\). We thus have shown that for each \(n\in \mathbb {N}\), the \(x^n\)-coefficient in the product of \((f_k)_{k\in \mathbb {N}}\) is finitely determined. In other words, each coefficient in the product of \((f_k)_{k\in \mathbb {N}}\) is finitely determined. In other words, the family \((f_k)_{k\in \mathbb {N}}\) is multipliable. In other words, the family \((f_n)_{n\in \mathbb {N}}\) is multipliable.
Hence, Theorem 1.476 yields \(\lim _{i\to \infty } \prod _{n=0}^{i} f_n = \prod _{n\in \mathbb {N}} f_n\). In other words, \(\prod _{n\in \mathbb {N}} f_n = \lim _{i\to \infty } \prod _{n=0}^{i} f_n\). This completes the proof of Theorem 1.479.
A.4.12 Helper lemmas from the Lean formalization
If a sequence \((a_i)_{i\in \mathbb {N}}\) in \(K\) stabilizes to both \(\ell _1\) and \(\ell _2\), then \(\ell _1 = \ell _2\).
Let \(N_1\) and \(N_2\) be the stabilization indices for \(\ell _1\) and \(\ell _2\) respectively. Set \(N := \max (N_1, N_2)\). Then \(a_N = \ell _1\) and \(a_N = \ell _2\), whence \(\ell _1 = \ell _2\).
If the family \((f_n)_{n\in \mathbb {N}}\) is summable, then the sequence of partial sums \(\left(\sum _{j=0}^{i} f_j\right)_{i\in \mathbb {N}}\) coefficientwise stabilizes to \(\sum _{n\in \mathbb {N}} f_n\).
This is a direct restatement of Theorem 1.475.
If the family \((f_n)_{n\in \mathbb {N}}\) is multipliable, then the sequence of partial products \(\left(\prod _{j=0}^{i} f_j\right)_{i\in \mathbb {N}}\) coefficientwise stabilizes to \(\prod _{n\in \mathbb {N}} f_n\).
This is a direct restatement of Theorem 1.476.
If the sequence of partial sums \(\left(\sum _{j=0}^{i} f_j\right)_{i\in \mathbb {N}}\) coefficientwise stabilizes to some limit, then the family \((f_n)_{n\in \mathbb {N}}\) is summable.
This is a direct restatement of the summability part of Theorem 1.478.
If the sequence of partial sums \(\left(\sum _{j=0}^{i} f_j\right)_{i\in \mathbb {N}}\) coefficientwise stabilizes to some limit and the family \((f_n)_{n\in \mathbb {N}}\) is summable, then the infinite sum equals the limit.
If the sequence of partial products \(\left(\prod _{j=0}^{i} f_j\right)_{i\in \mathbb {N}}\) coefficientwise stabilizes to some limit, then the family \((f_n)_{n\in \mathbb {N}}\) is multipliable.
This is a direct restatement of the multipliability part of Theorem 1.479.
If the sequence of partial products \(\left(\prod _{j=0}^{i} f_j\right)_{i\in \mathbb {N}}\) coefficientwise stabilizes to some limit and the family \((f_n)_{n\in \mathbb {N}}\) is multipliable, then the infinite product equals the limit.
If \(f \overset {x^n}{\equiv } g\), then \(f^d \overset {x^n}{\equiv } g^d\) for every \(d \in \mathbb {N}\). The proof proceeds by induction on \(d\), using the multiplicativity of \(x^n\)-equivalence at each step.