Formalization Blueprint for “An Introduction to Algebraic Combinatorics” by Darij Grinberg

A.4 Details: Limits of FPSs

A.4.1 Detailed proof of Lemma 1.462

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}\),

\begin{equation} \text{the sequence } \bigl([x^n] f_i\bigr)_{i\in \mathbb {N}} \text{ stabilizes to } [x^n] f \label{pf.lem.fps.lim.xn-equiv.stab} \end{equation}
6

(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

\[ \text{all integers } i\geq N \text{ satisfy } [x^k] f_i = [x^k] f \]

(by the definition of “stabilizing”). Let us denote this \(N\) by \(N_k\). Thus,

\begin{equation} \text{all integers } i\geq N_k \text{ satisfy } [x^k] f_i = [x^k] f. \label{pf.lem.fps.lim.xn-equiv.Nk} \end{equation}
7

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:

\[ \text{Each } m\in \{ 0,1,\ldots ,n\} \text{ satisfies } [x^m] f_i = [x^m] f. \]

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

\[ \text{all integers } i\geq N \text{ satisfy } f_i \overset {x^n}{\equiv } f \]

(namely, \(N = P\)). This proves Lemma 1.462.

A.4.2 Detailed proof of Proposition 1.463

Lemma A.85

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

\[ \text{all integers } i\geq K \text{ satisfy } f_i \overset {x^n}{\equiv } f. \]
theorem PowerSeries.exists_xnEquiv_K {K : Type u_1} [CommRing K] {f : PowerSeries K} {lf : PowerSeries K} (hf : CoeffStabilizesTo f lf) (n : ) :
∃ (K_1 : ), iK_1, f i ≡[x^n] lf
Proof

This follows directly from Lemma 1.462 applied to the sequence \((f_i)\) and limit \(f\).

Lemma A.86

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

\[ \text{all integers } i\geq L \text{ satisfy } g_i \overset {x^n}{\equiv } g. \]
theorem PowerSeries.exists_xnEquiv_L {K : Type u_1} [CommRing K] {g : PowerSeries K} {lg : PowerSeries K} (hg : CoeffStabilizesTo g lg) (n : ) :
∃ (L : ), iL, g i ≡[x^n] lg
Proof

This is the exact same statement as Lemma A.85, but applied to the sequence \((g_i)\) and limit \(g\). It follows directly from Lemma 1.462.

Lemma A.87

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\),

\[ f_i \overset {x^n}{\equiv } f \qquad \text{and}\qquad g_i \overset {x^n}{\equiv } g. \]
theorem PowerSeries.exists_xnEquiv_both {K : Type u_1} [CommRing K] {f g : PowerSeries K} {lf lg : PowerSeries K} (hf : CoeffStabilizesTo f lf) (hg : CoeffStabilizesTo g lg) (n : ) :
∃ (P : ), iP, (f i ≡[x^n] lf) g i ≡[x^n] lg
Proof

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.

Detailed proof of Proposition 1.463

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

\[ \text{all integers } i\geq N \text{ satisfy } f_i \overset {x^n}{\equiv } f. \]

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

\[ \text{all integers } i\geq K \text{ satisfy } f_i \overset {x^n}{\equiv } f. \]

Similarly, using \(\lim _{i\to \infty } g_i = g\), we can find an integer \(L\in \mathbb {N}\) such that

\[ \text{all integers } i\geq L \text{ satisfy } g_i \overset {x^n}{\equiv } g. \]

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

\[ f_i g_i \overset {x^n}{\equiv } fg \]

(by the multiplicativity of \(x^n\)-equivalence, i.e., Theorem 1.328 (b)). In other words,

\[ \text{each } m\in \{ 0,1,\ldots ,n\} \text{ satisfies } [x^m](f_i g_i) = [x^m](fg) \]

(by the definition of \(x^n\)-equivalence). Applying this to \(m = n\), we find

\[ [x^n](f_i g_i) = [x^n](fg). \]

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

\[ \text{all integers } i\geq N \text{ satisfy } [x^n](f_i g_i) = [x^n](fg) \]

(namely, \(N = P\)). In other words,

\[ \text{the sequence } \bigl([x^n](f_i g_i)\bigr)_{i\in \mathbb {N}} \text{ stabilizes to } [x^n](fg) \]

(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.

Lemma A.88

If \((f_i)\) coefficientwise stabilizes to \(f\) and \((g_i)\) coefficientwise stabilizes to \(g\), then \((f_i + g_i)\) coefficientwise stabilizes to \(f + g\).

theorem PowerSeries.coeffStabilizesTo_add' {K : Type u_1} [CommRing K] {f g : PowerSeries K} {lf lg : PowerSeries K} (hf : CoeffStabilizesTo f lf) (hg : CoeffStabilizesTo g lg) :
CoeffStabilizesTo (fun (i : ) => f i + g i) (lf + lg)
Proof

For each \(n\in \mathbb {N}\):

  1. 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\).

  2. Set \(P := \max \{ K_f, K_g\} \).

  3. For \(i\geq P\), by the additivity of \(x^n\)-equivalence, \(f_i + g_i \overset {x^n}{\equiv } f + g\).

  4. Extracting the \(n\)-th coefficient: \([x^n](f_i + g_i) = [x^n](f + g)\).

Lemma A.89

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\).

theorem PowerSeries.coeffStabilizesTo_mul' {K : Type u_1} [CommRing K] {f g : PowerSeries K} {lf lg : PowerSeries K} (hf : CoeffStabilizesTo f lf) (hg : CoeffStabilizesTo g lg) :
CoeffStabilizesTo (fun (i : ) => f i * g i) (lf * lg)
Proof

For each \(n\in \mathbb {N}\):

  1. 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\).

  2. Set \(P := \max \{ K_f, K_g\} \).

  3. For \(i\geq P\), by the multiplicativity of \(x^n\)-equivalence, \(f_i \cdot g_i \overset {x^n}{\equiv } f \cdot g\).

  4. 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

Lemma A.90
#

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\).

theorem PowerSeries.xnEquiv_invOfUnit' {K : Type u_1} [CommRing K] {n : } {f g : PowerSeries K} (u v : Kˣ) (huv : u = v) (h : f ≡[x^n] g) :
Lemma A.91
#

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}\).

theorem PowerSeries.xnEquiv_div {K : Type u_1} [CommRing K] {n : } {a b c d : PowerSeries K} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) (u : Kˣ) (hu : constantCoeff c = u) (v : Kˣ) (hv : constantCoeff d = v) :
Lemma A.92
#

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\).

theorem PowerSeries.unit_eq_of_coeffStabilizesTo {K : Type u_1} [CommRing K] {g : PowerSeries K} {lg : PowerSeries K} (hg : CoeffStabilizesTo g lg) (hunit : ∀ (i : ), IsUnit (constantCoeff (g i))) :
∃ (N : ), iN, .unit = .unit
Lemma A.93
#

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.

theorem PowerSeries.coeffStabilizesTo_invOfUnit {K : Type u_1} [CommRing K] {g : PowerSeries K} {lg : PowerSeries K} (hg : CoeffStabilizesTo g lg) (hunit : ∀ (i : ), IsUnit (constantCoeff (g i))) :
CoeffStabilizesTo (fun (i : ) => (g i).invOfUnit .unit) (lg.invOfUnit .unit)

A.4.4 Detailed proof of Proposition 1.468

Detailed proof of Proposition 1.468

First, let us show that \(g\) is invertible:

Claim 1: The FPS \(g\in K[[x]]\) is invertible.

Proof of Claim 1

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

\[ \text{all integers } i\geq N \text{ satisfy } [x^0] g_i = [x^0] g \]

(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

\[ \text{all integers } i\geq N \text{ satisfy } f_i \overset {x^n}{\equiv } f. \]

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

\[ \text{all integers } i\geq K \text{ satisfy } f_i \overset {x^n}{\equiv } f. \]

Similarly, using \(\lim _{i\to \infty } g_i = g\), we can find an integer \(L\in \mathbb {N}\) such that

\[ \text{all integers } i\geq L \text{ satisfy } g_i \overset {x^n}{\equiv } g. \]

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

\[ \frac{f_i}{g_i} \overset {x^n}{\equiv } \frac{f}{g} \]

(by Theorem 1.328 (e), applied to \(a = f_i\), \(b = f\), \(c = g_i\) and \(d = g\)). In other words,

\[ \text{each } m\in \{ 0,1,\ldots ,n\} \text{ satisfies } [x^m] \frac{f_i}{g_i} = [x^m] \frac{f}{g} \]

(by the definition of \(x^n\)-equivalence). Applying this to \(m = n\), we find

\[ [x^n] \frac{f_i}{g_i} = [x^n] \frac{f}{g}. \]

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

\[ \text{all integers } i\geq N \text{ satisfy } [x^n] \frac{f_i}{g_i} = [x^n] \frac{f}{g} \]

(namely, \(N = P\)). In other words,

\[ \text{the sequence } \left([x^n] \frac{f_i}{g_i}\right)_{i\in \mathbb {N}} \text{ stabilizes to } [x^n] \frac{f}{g} \]

(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

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}\),

\begin{equation} \text{all but finitely many } k\in \mathbb {N} \text{ satisfy } [x^n] f_k = 0 \label{pf.thm.fps.lim.sum-lim.1} \end{equation}
8

(by the definition of “summable”).

Let us define

\begin{equation} g_i := \sum _{k=0}^{i} f_k \qquad \text{for each } i\in \mathbb {N}. \label{pf.thm.fps.lim.sum-lim.gi} \end{equation}
9

Let us furthermore set

\begin{equation} g := \sum _{k\in \mathbb {N}} f_k. \label{pf.thm.fps.lim.sum-lim.g} \end{equation}
10

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

\begin{equation} \text{all } k\in \mathbb {N}\setminus J \text{ satisfy } [x^n] f_k = 0. \label{pf.thm.fps.lim.sum-lim.2} \end{equation}
11

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

\begin{equation} \text{all } k\in J \text{ satisfy } k\leq m. \label{pf.thm.fps.lim.sum-lim.3} \end{equation}
12

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

\begin{equation} [x^n] f_k = 0 \qquad \text{for each } k\in \mathbb {N} \text{ satisfying } k\geq m+1. \label{pf.thm.fps.lim.sum-lim.4} \end{equation}
13

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

\begin{align} [x^n] g & = [x^n]\left(\sum _{k\in \mathbb {N}} f_k\right) = \sum _{k\in \mathbb {N}} [x^n] f_k \nonumber \\ & = \sum _{k=0}^{i} [x^n] f_k + \sum _{k=i+1}^{\infty } \underbrace{[x^n] f_k}_{\substack{[=, , 0, , \\ , , \text , {, (, b, y, ~, \eqref , {, p, f, ., t, h, m, ., f, p, s, ., l, i, m, ., s, u, m, -, l, i, m, ., 4, }, }, , \\ , , \text , {, s, i, n, c, e, , }, , k, \geq , i, +, 1, \geq , m, +, 1, \text , {, ), }]}} = \sum _{k=0}^{i} [x^n] f_k + \underbrace{\sum _{k=i+1}^{\infty } 0}_{=0} \nonumber \\ & = \sum _{k=0}^{i} [x^n] f_k. \label{pf.thm.fps.lim.sum-lim.5} \end{align}

On the other hand, from \(g_i = \sum _{k=0}^{i} f_k\), we obtain

\[ [x^n] g_i = [x^n]\left(\sum _{k=0}^{i} f_k\right) = \sum _{k=0}^{i} [x^n] f_k. \]

Comparing this with 14, we obtain \([x^n] g_i = [x^n] g\).

Forget that we fixed \(i\). We thus have shown that

\[ \text{all integers } i\geq m \text{ satisfy } [x^n] g_i = [x^n] g. \]

Hence, there exists some \(N\in \mathbb {N}\) such that

\[ \text{all integers } i\geq N \text{ satisfy } [x^n] g_i = [x^n] g \]

(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}\),

\[ \text{the sequence } \bigl([x^n] g_i\bigr)_{i\in \mathbb {N}} \text{ 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 9 and 10, we can rewrite this as

\[ \lim _{i\to \infty } \sum _{k=0}^{i} f_k = \sum _{k\in \mathbb {N}} f_k. \]

Renaming the summation index \(k\) as \(n\) everywhere in this equality, we can rewrite it as

\[ \lim _{i\to \infty } \sum _{n=0}^{i} f_n = \sum _{n\in \mathbb {N}} f_n. \]

This proves Theorem 1.475.

A.4.6 Helpers for Theorem 1.476

Lemma A.94
#

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\),

\[ [x^k](g \cdot f) = [x^k] g. \]

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\).

theorem PowerSeries.coeff_mul_one_plus_higher {K : Type u_1} [CommRing K] {g f : PowerSeries K} {n : } (hf : kn, (coeff k) f = if k = 0 then 1 else 0) (k : ) :
k n(coeff k) (g * f) = (coeff k) g
Lemma A.95
#

If \(f_m \equiv 1 \pmod{x^{n+1}}\), then for any \(k \le n\),

\[ [x^k] \prod _{j=0}^{m} f_j = [x^k] \prod _{j=0}^{m-1} f_j. \]

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.

theorem PowerSeries.coeff_prod_extend {K : Type u_1} [CommRing K] {f : PowerSeries K} {n m : } (hf : kn, (coeff k) (f m) = if k = 0 then 1 else 0) (k : ) (hk : k n) :
(coeff k) (∏ jFinset.range (m + 1), f j) = (coeff k) (∏ jFinset.range m, f j)
Lemma A.96
#

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\),

\[ [x^k] \prod _{j=0}^{i} f_j = [x^k] \prod _{j=0}^{N} f_j. \]

The proof proceeds by induction on \(i\), repeatedly applying Lemma A.95.

theorem PowerSeries.coeff_prod_range_eq_of_ge {K : Type u_1} [CommRing K] {f : PowerSeries K} {n N : } (hN : jN, kn, (coeff k) (f j) = if k = 0 then 1 else 0) {i : } (hi : i N) {k : } (hk : k n) :
(coeff k) (∏ jFinset.range (i + 1), f j) = (coeff k) (∏ jFinset.range (N + 1), f j)
Lemma A.97
#

For a multipliable family \((f_j)\), for each \(n \in \mathbb {N}\), there exists \(N\) such that for all \(i \ge N\),

\[ [x^n] \prod _{j=0}^{i} f_j = [x^n] \prod _{j\in \mathbb {N}} f_j. \]

This is the key stabilization lemma that directly implies Theorem 1.476.

theorem PowerSeries.coeff_partial_prod_stabilizes {K : Type u_1} [CommRing K] {f : PowerSeries K} (hf : IsMultipliable f) (n : ) :
∃ (N : ), iN, (coeff n) (∏ jFinset.range (i + 1), f j) = (coeff n) (tprod' f hf)

A.4.7 Detailed proof of Theorem 1.476

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

\begin{equation} g_i := \prod _{k=0}^{i} f_k \qquad \text{for each } i\in \mathbb {N}. \label{pf.thm.fps.lim.prod-lim.gi} \end{equation}
15

Let us furthermore set

\begin{equation} g := \prod _{k\in \mathbb {N}} f_k. \label{pf.thm.fps.lim.prod-lim.g} \end{equation}
16

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

\begin{equation} \text{all } k\in M \text{ satisfy } k\leq m. \label{pf.thm.fps.lim.prod-lim.3} \end{equation}
17

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

\[ [x^n]\left(\prod _{k\in J} f_k\right) = [x^n]\left(\prod _{k\in M} f_k\right) \]

(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

\begin{equation} [x^n]\left(\prod _{k\in \{ 0,1,\ldots ,i\} } f_k\right) = [x^n]\left(\prod _{k\in M} f_k\right) \label{pf.thm.fps.lim.prod-lim.4} \end{equation}
18

(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

\[ [x^n]\left(\prod _{k\in \mathbb {N}} f_k\right) = [x^n]\left(\prod _{k\in M} f_k\right) \]

(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

\[ [x^n]\left(\prod _{k\in \{ 0,1,\ldots ,i\} } f_k\right) = [x^n]\left(\prod _{k\in \mathbb {N}} f_k\right). \]

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

\[ [x^n] g_i = [x^n] g. \]

Forget that we fixed \(i\). We thus have shown that

\[ \text{all integers } i\geq m \text{ satisfy } [x^n] g_i = [x^n] g. \]

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

\[ \lim _{i\to \infty } \prod _{k=0}^{i} f_k = \prod _{k\in \mathbb {N}} f_k. \]

Renaming the product index \(k\) as \(n\) everywhere in this equality, we can rewrite it as

\[ \lim _{i\to \infty } \prod _{n=0}^{i} f_n = \prod _{n\in \mathbb {N}} f_n. \]

This proves Theorem 1.476.

A.4.8 Detailed proofs of Corollary 1.477

Proof 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

\[ \lim _{i\to \infty } \sum _{n=0}^{i} a_n x^n = \sum _{n\in \mathbb {N}} a_n x^n = a. \]

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

Proof of Theorem 1.478

Let us define

\begin{equation} g_i := \sum _{k=0}^{i} f_k \qquad \text{for each } i\in \mathbb {N}. \label{pf.thm.fps.lim.sum-lim-conv.gi} \end{equation}
19

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,

\begin{equation} g = \lim _{i\to \infty } \sum _{n=0}^{i} f_n = \lim _{i\to \infty } g_i. \label{pf.thm.fps.lim.sum-lim-conv.g=lim} \end{equation}
20

In other words, the sequence \((g_i)_{i\in \mathbb {N}}\) coefficientwise stabilizes to \(g\). In other words, for each \(n\in \mathbb {N}\),

\begin{equation} \text{the sequence } \bigl([x^n] g_i\bigr)_{i\in \mathbb {N}} \text{ stabilizes to } [x^n] g. \label{pf.thm.fps.lim.sum-lim-conv.gstab} \end{equation}
21

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

\begin{equation} \text{all integers } i\geq N \text{ satisfy } [x^n] g_i = [x^n] g. \label{pf.thm.fps.lim.sum-lim-conv.1} \end{equation}
22

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,

\[ i\in \mathbb {N}\setminus M = \mathbb {N}\setminus \{ 0,1,\ldots ,N\} = \{ N+1, N+2, N+3, \ldots \} . \]

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

\begin{equation} [x^n] g_{i-1} = [x^n] g_i. \label{pf.thm.fps.lim.sum-lim-conv.2} \end{equation}
23

However, 19 yields

\begin{equation} g_i = \sum _{k=0}^{i} f_k = f_i + \sum _{k=0}^{i-1} f_k. \label{pf.thm.fps.lim.sum-lim-conv.3} \end{equation}
24

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

\[ g_i = f_i + g_{i-1}. \]

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}\),

\[ \text{all but finitely many } k\in \mathbb {N} \text{ satisfy } [x^n] f_k = 0. \]

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

Lemma A.98
#

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\).

theorem PowerSeries.constantCoeff_prod_eq_one {K : Type u_1} [CommRing K] {f : PowerSeries K} {s : Finset } (hf : is, constantCoeff (f i) = 1) :
constantCoeff (∏ js, f j) = 1

A.4.11 Detailed proof of Theorem 1.479

Proof of Theorem 1.479

Let us define

\begin{equation} g_i := \prod _{k=0}^{i} f_k \qquad \text{for each } i\in \mathbb {N}. \label{pf.thm.fps.lim.prod-lim-conv.gi} \end{equation}
25

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,

\begin{equation} g = \lim _{i\to \infty } \prod _{n=0}^{i} f_n = \lim _{i\to \infty } g_i. \label{pf.thm.fps.lim.prod-lim-conv.g=lim} \end{equation}
26

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

\begin{equation} \text{all integers } i\geq N \text{ satisfy } g_i \overset {x^n}{\equiv } g \label{pf.thm.fps.lim.prod-lim-conv.gi-equiv-g} \end{equation}
27

(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

\begin{equation} \prod _{k\in M} f_k = \prod _{k\in \{ 0,1,\ldots ,N\} } f_k = \prod _{k=0}^{N} f_k = g_N \label{pf.thm.fps.lim.prod-lim-conv.=gN} \end{equation}
28

(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\).

Proof of Claim 1

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

\[ g_j = \prod _{k=0}^{j} f_k = \left(\prod _{k=0}^{j-1} f_k\right) f_j = g_{j-1} f_j. \]

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\).

Proof of Claim 2

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,

\[ \text{each } m\in \{ 0,1,\ldots ,n\} \text{ satisfies } [x^m] g = [x^m]\left(\prod _{k\in J} f_k\right) \]

(by the definition of \(x^n\)-equivalence). Applying this to \(m = n\), we find

\[ [x^n] g = [x^n]\left(\prod _{k\in J} f_k\right). \]

The same argument can be applied to \(M\) instead of \(J\) (since \(M\subseteq M\subseteq \mathbb {N}\)), and thus yields

\[ [x^n] g = [x^n]\left(\prod _{k\in M} f_k\right). \]

Comparing these two equalities, we find

\[ [x^n]\left(\prod _{k\in J} f_k\right) = [x^n]\left(\prod _{k\in M} f_k\right). \]

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

\[ [x^n]\left(\prod _{k\in J} f_k\right) = [x^n]\left(\prod _{k\in M} f_k\right). \]

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

Lemma A.99

If a sequence \((a_i)_{i\in \mathbb {N}}\) in \(K\) stabilizes to both \(\ell _1\) and \(\ell _2\), then \(\ell _1 = \ell _2\).

theorem Seq.stabilizesTo_unique' {K : Type u_1} {a : K} {lim₁ lim₂ : K} (h₁ : StabilizesTo a lim₁) (h₂ : StabilizesTo a lim₂) :
lim₁ = lim₂
Proof

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\).

Lemma A.100

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\).

theorem PowerSeries.coeffStabilizesTo_partial_sum' {K : Type u_1} [CommRing K] {f : PowerSeries K} (hf : IsSummable f) :
CoeffStabilizesTo (fun (i : ) => jFinset.range (i + 1), f j) (tsum' f hf)
Proof

This is a direct restatement of Theorem 1.475.

Lemma A.101

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\).

theorem PowerSeries.coeffStabilizesTo_partial_prod' {K : Type u_1} [CommRing K] {f : PowerSeries K} (hf : IsMultipliable f) :
CoeffStabilizesTo (fun (i : ) => jFinset.range (i + 1), f j) (tprod' f hf)
Proof

This is a direct restatement of Theorem 1.476.

Lemma A.102

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.

theorem PowerSeries.isSummable_of_coeffStabilizesTo_partial_sum' {K : Type u_1} [CommRing K] {f : PowerSeries K} {lim : PowerSeries K} (h : CoeffStabilizesTo (fun (i : ) => jFinset.range (i + 1), f j) lim) :
Proof

This is a direct restatement of the summability part of Theorem 1.478.

Lemma A.103

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.

theorem PowerSeries.tsum'_eq_of_coeffStabilizesTo_partial_sum' {K : Type u_1} [CommRing K] {f : PowerSeries K} {lim : PowerSeries K} (h : CoeffStabilizesTo (fun (i : ) => jFinset.range (i + 1), f j) lim) (hsum : IsSummable f) :
tsum' f hsum = lim
Proof

By Theorem 1.475, the partial sums converge to the infinite sum. By uniqueness of limits (Lemma 1.454), the limit equals the infinite sum.

Lemma A.104

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.

theorem PowerSeries.isMultipliable_of_coeffStabilizesTo_partial_prod' {K : Type u_1} [CommRing K] {f : PowerSeries K} {lim : PowerSeries K} (h : CoeffStabilizesTo (fun (i : ) => jFinset.range (i + 1), f j) lim) (hconst : ∀ (i : ), constantCoeff (f i) = 1) :
Proof

This is a direct restatement of the multipliability part of Theorem 1.479.

Lemma A.105

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.

theorem PowerSeries.tprod'_eq_of_coeffStabilizesTo_partial_prod' {K : Type u_1} [CommRing K] {f : PowerSeries K} {lim : PowerSeries K} (h : CoeffStabilizesTo (fun (i : ) => jFinset.range (i + 1), f j) lim) (hmult : IsMultipliable f) :
tprod' f hmult = lim
Proof

By Theorem 1.476, the partial products converge to the infinite product. By uniqueness of limits (Lemma 1.454), the limit equals the infinite product.

Lemma A.106
#

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.

theorem PowerSeries.xnEquiv_pow {K : Type u_1} [CommRing K] {n : } {f g : PowerSeries K} (h : f ≡[x^n] g) (d : ) :
f ^ d ≡[x^n] g ^ d