The idea is to reduce it to the case \(n=2\) by induction, then to use the discrete Fubini rule.

Same method as for Proposition 1.375, but now using the discrete Fubini rule for infinite sums. The proof is by induction on \(n\):

• Base case (\(n=0\)): Both sides equal \(1\).

• Inductive step: Split the product into the first \(n\) factors and the last factor, apply the induction hypothesis on the first \(n\), then apply the Cauchy product formula for infinite sums.

Summability of the product family is established by showing that for each coefficient \(d\), only finitely many functions \(f\) give a nonzero contribution (using finite support of each summable family in the discrete topology).

The product \(\prod _i p_{i,f(i)}\) is divisible by \(p_{j,f(j)}\), which has order \({\gt} d\). Since the order of a product is at least the sum of the orders of the factors, the product also has order \({\gt} d\).

For each coefficient \(d\), define \(T_i = \bigcup _{m\le d} \mathrm{supp}([x^m]\circ p_i)\). Each \(T_i\) is finite (by discrete summability). If \(f(i)\notin T_i\) for some \(i\), then \([x^d](\prod _j p_{j,f(j)}) = 0\) by Lemma 1.377. The set \(\{ f \mid \forall i,\, f(i)\in T_i\} \) is finite (product of finite sets), so the support at coefficient \(d\) is finite.

For each coefficient \(d\), the support of \((\alpha ,\beta )\mapsto [x^d](f_\alpha g_\beta )\) is contained in the finite product of coefficient supports, using the Cauchy product formula and the finiteness of supports.

This is the particular case of Proposition 1.382 for \(I=\left\{ 1,2,3,\ldots \right\} \).

The proof is a long-winded reduction to the finite case. It proceeds by showing both sides have the same \(n\)-th coefficient for each \(n\).

Setup. For each \(m\in \mathbb {N}\), define \(T'_n = \{ (i,k)\in \overline{S} \mid \exists m\le n,\, [x^m](p_{i,k})\ne 0\} \). This set is finite by coefficient-wise summability. Let \(I_n = \{ i \in I \mid \exists k: (i,k)\in T'_n\} \). Then \(I_n\) is finite.

RHS reduction (Claim 8). For the RHS, only essentially finite functions \(f\) with “graph” contained in \(T'_n\) can contribute to the \(n\)-th coefficient. If some \((j, f(j))\notin T'_n\) with \(f(j)\ne 0\), then \([x^m](p_{j,f(j)}) = 0\) for all \(m\le n\), so \([x^n](\prod _i p_{i,f(i)}) = 0\) (by the finite product coefficient lemma). The set of such functions is finite (since their graphs inject into the finite powerset of \(T'_n\)).

LHS reduction (Claim 10). For the LHS, write \(\sum _k p_{i,k} = 1 + \sum _{k\ne 0} p_{i,k}\). For \(i\notin I_n\), the sum \(\sum _{k\ne 0} p_{i,k}\) has all coefficients up to \(n\) equal to \(0\). By the irrelevance lemma (Lemma 1.384), the factors for \(i\notin I_n\) do not affect the \(n\)-th coefficient. Thus \([x^n](\prod _i \sum _k p_{i,k}) = [x^n](\prod _{i\in I_n} \sum _k p_{i,k})\).

Finite product rule (Claim 11). Since \(I_n\) is finite, we can apply Proposition 1.383: \(\prod _{i\in I_n} \sum _k p_{i,k} = \sum _{(k_i)_{i\in I_n}\in \prod _{i\in I_n} S_i} \prod _{i\in I_n} p_{i,k_i}\).

Combining Claims 8, 10, and 11 shows both sides have equal \(n\)-th coefficients.

This is just Proposition 1.376, with the indexing set \(\left\{ 1,2,\ldots ,n\right\} \) replaced by \(N\). It can be proved by reindexing the products (using a bijection between \(N\) and \(\{ 1,2,\ldots ,|N|\} \)) or directly by induction on \(\left\vert N\right\vert \).

The idea is to argue that the first \(n+1\) coefficients of \(a\prod _{i\in J}\left( 1+f_{i}\right) \) agree with those of \(a\).

First, one shows that for any finite subset \(s\) of \(J\), if each \(f_i\) has \([x^m](f_i) = 0\) for all \(m\le n\), then \([x^m](\prod _{i\in s}(1+f_i)) = [x^m](1)\) for all \(m\le n\). This uses the expansion \(\prod _{i\in s}(1+f_i) = \sum _{t\subseteq s}\prod _{i\in t}f_i\); for \(t\ne \emptyset \), each \(\prod _{i\in t}f_i\) has order \({\gt}n\), so its \(m\)-th coefficient is zero.

Then, for the infinite product, the result follows by taking limits: \(\prod _{i\in J}(1+f_i)\) is the limit of the partial products \(\prod _{i\in s}(1+f_i)\), and since \([x^m]\) is continuous, each partial product gives \([x^m](\prod _{i\in s}(1+f_i)) = [x^m](1)\).

Finally, the coefficient of \(a\cdot \prod _{i\in J}(1+f_i)\) uses the Cauchy product formula, which only involves coefficients of \(\prod _{i\in J}(1+f_i)\) up to degree \(m\le n\), all of which equal the corresponding coefficients of \(1\). Hence \([x^m](a\cdot \prod _{i\in J}(1+f_i)) = [x^m](a\cdot 1) = [x^m](a)\).

If the family \((1+f_i)_{i\in J}\) is not multipliable, the infinite product defaults to \(1\) by convention, and the result holds trivially.

We have \(T'_n = \bigcup _{m\le n} \mathrm{supp}\! \left((i,k)\mapsto [x^m](p_{i,k})\right)\). Each support set is finite by coefficient-wise summability (summable families over a discrete topological space have finite support). A finite union of finite sets is finite.

Write \(\prod _{i\in S} f_i = f_j \cdot \prod _{i\in S\setminus \{ j\} } f_i\). For each \(m\le n\), use the Cauchy product formula: each term involves \([x^a](f_j)\) with \(a\le m\le n\), which is \(0\) by hypothesis.

Each such function is determined by its graph, which is a subset of \(T\). The map sending \(f\) to its graph is injective (since the graph determines \(f\) on nonzero values, and the rest are \(0\)). Since the powerset of \(T\) is finite, the image is finite, so the set of such functions is finite.

Write \(\prod _{i\in t}(1+g_i) = \prod _{i\in s}(1+g_i) \cdot \prod _{i\in t\setminus s}(1+g_i)\). For the second factor, each \(g_i\) (\(i\in t\setminus s\)) has order \({\gt}n\), so by expanding \(\prod _{i\in t\setminus s}(1+g_i)\) via the powerset formula, all terms except the empty product have order \({\gt}n\). Hence \([x^m]\! \left(\prod _{i\in t\setminus s}(1+g_i)\right) = [x^m](1)\) for all \(m\le n\), and the Cauchy product formula gives the result.

The infinite product \(\prod _{i\in I}(1+g_i)\) is the limit of partial products \(\prod _{i\in s}(1+g_i)\) over finite sets \(s\). By Lemma 1.388, for any \(s\supseteq I_n\), the \(n\)-th coefficient of \(\prod _{i\in s}(1+g_i)\) equals that of \(\prod _{i\in I_n}(1+g_i)\). By continuity of \([x^n]\) and the eventual constancy, the limit also has this \(n\)-th coefficient.

The subfamily \((p_{i,k})_{k\in S_i, k\ne 0}\) is summable because it injects into the summable family \((p_{i,k})_{(i,k)\in \overline{S}}\) via \((i,\cdot )\). Adding the single term \(p_{i,0}\) preserves summability. Formally, we reduce to coefficient-wise summability and split each coefficient sum at \(k=0\).

Write \(\sum _k p_{i,k} = 1 + \sum _{k\ne 0} p_{i,k}\). We need to show \((1 + g_i)_{i\in I}\) is multipliable, where \(g_i = \sum _{k\ne 0} p_{i,k}\). By the multipliability criterion (Theorem 1.350), it suffices to show that \(\sum _{s \in \mathcal{F}(I)} \prod _{i\in s} g_i\) is summable, where \(\mathcal{F}(I)\) denotes the set of all finite subsets of \(I\). This is proved coefficient-wise: for each \(n\), the support of \(s\mapsto [x^n](\prod _{i\in s}g_i)\) is contained in the set of finite subsets \(s\) with \(s\subseteq I_n\) (the finite set of indices contributing to coefficients up to \(n\)), which is finite.

For each coefficient \(n\), define \(T'_n = \{ (i,k)\in \overline{S} \mid \exists m\le n,\, [x^m](p_{i,k})\ne 0\} \). This is finite by Lemma 1.385. The support of \(f\mapsto [x^n](\prod _{i\in I} p_{i,f(i)})\) is contained in the set of essentially finite functions whose “graph” \(\{ (i,f(i)) : f(i)\ne 0\} \) is a subset of \(T'_n\) (if \((j,f(j))\notin T'_n\) for some \(j\) with \(f(j)\ne 0\), then \([x^n](\prod _{i\in I} p_{i,f(i)}) = 0\) by Lemma 1.386). This set of functions is finite by Lemma 1.387.

The identity \(\prod _{i\in \mathbb {N}}(1+f_i) = \sum _{s\subseteq \mathbb {N},\, s\text{ finite}} \prod _{i\in s} f_i\) holds provided the right-hand side is summable. For the summability: for each coefficient \(d\), define \(T = \bigcup _{m\le d}\mathrm{supp}([x^m]\circ a)\), which is finite by discrete summability. Any finset \(s\) not contained in \(T\) contributes \(0\) to coefficient \(d\) (since some factor \(a_i\) with \(i\notin T\) has all low coefficients zero). The set of finsets contained in \(T\) is finite.

This follows from Proposition 1.393 by observing that both formulations sum over the same collection of finite subsets of \(\mathbb {N}\).

For each \(k{\gt}0\), we have \(1+x^{k}=\frac{1-x^{2k}}{1-x^{k}}\) (since \(1-x^{2k}=\left( 1-x^{k}\right) \left( 1+x^{k}\right) \)). Thus,

where the even factors cancel. The cancellation is justified by the fact that the family \(\left( 1-x^{k}\right) _{k{\gt}0}\) factors as a product over even and odd indices, by the partition of positive integers into evens and odds (by Proposition 1.365).

Lean proof strategy. The Lean proof proceeds differently: both sides are shown to equal the same partition-theoretic generating function. The RHS equals \(\sum _n d_n \cdot x^n\) (generating function for partitions into distinct parts, i.e., parts of multiplicity \({\lt}2\)). The LHS equals \(\sum _n o_n \cdot x^n\) (generating function for partitions into odd parts). These are equal by Glaisher’s theorem.

Proposition 1.395 shows that the generating functions for \(d_n\) and \(o_n\) are equal, hence \(d_n = o_n\) for all \(n\).

This follows from Proposition 1.395 by reindexing the product using the bijection \(i\mapsto 2i-1\) between \(\mathbb {N}^{+}\) and the odd positive integers.

The \(n\)-th coefficient of \(\mathrm{rescale}(a)(f)\) is \(a^n\cdot [x^n]f\). This is continuous because \([x^n]\) is continuous (it is a projection) and scalar multiplication by \(a^n\) is continuous.

The Lean formalization proves the special case of rescaling \(g = ax\) (i.e., substituting \(ax\) for \(x\)). The proof uses Lemma 1.398 (the rescale map is continuous) together with the fact that it is a ring homomorphism, so it commutes with infinite products.

The \(\operatorname {Exp}\) map converts infinite sums in \(K[[x]]_0\) to infinite products in \(K[[x]]_1\). This is because \(\operatorname {Exp}\) is a continuous ring homomorphism from \(K[[x]]_0\) (with addition) to \(K[[x]]_1\) (with multiplication), and therefore commutes with infinite sums and products.

The \(\operatorname {Log}\) map converts infinite products in \(K[[x]]_1\) to infinite sums in \(K[[x]]_0\). This follows from the fact that \(\operatorname {Log}\) is a continuous ring homomorphism from \(K[[x]]_1\) (with multiplication) to \(K[[x]]_0\) (with addition), and therefore commutes with infinite products and sums.