Direct verification: the product is computed coefficient-wise and shown to equal \(1\).

By computing the derivative of \(\overline{\log } = \sum _{n \ge 1} \frac{(-1)^{n-1}}{n} x^n\) term-by-term: \(\overline{\log }' = \sum _{n \ge 1} (-1)^{n-1} x^{n-1} = \sum _{n \ge 0} (-1)^n x^n = \iota \).

Since \(\overline{\exp } = \exp - 1\), we have \(\overline{\exp }' = \exp ' - 0 = \exp ' = \exp \), where the last equality is the standard fact \(\exp ' = \exp \).

We have \((\iota \circ g) \cdot (1 + g) = (\iota \cdot (1+x)) \circ g = 1 \circ g = 1\). Since \([x^0](1+g) \ne 0\), this gives \(\iota \circ g = (1+g)^{-1}\).

(a) Let us first show that \(\overline{\exp }^{\prime }=\exp ^{\prime }=\exp \). Indeed, \(\overline{\exp }=\exp -1\), so that \(\exp =\overline{\exp }+1\) and therefore

Next, we recall that \(\exp =\sum _{n\in \mathbb {N}}\frac{1}{n!}x^{n}\). Hence, the definition of a derivative yields

Comparing this with (26), we find

Now, we can apply the chain rule to \(f=\overline{\exp }\) (since \(\left[x^{0}\right]g=0\)), and thus obtain

The same computation (but with \(\overline{\exp }\) replaced by \(\exp \)) yields \(\left(\exp \circ g\right)^{\prime }=\left(\exp \circ g\right)\cdot g^{\prime }\). Combining these two formulas, we obtain \(\left(\overline{\exp }\circ g\right)^{\prime }=\left(\exp \circ g\right)^{\prime }=\left( \exp \circ g\right)\cdot g^{\prime }\). This proves part (a).

(b) We have \(\overline{\log }=\sum _{n\geq 1}\frac{\left(-1\right) ^{n-1}}{n}x^{n}\). Thus,

(here, we have substituted \(n\) for \(n-1\) in the sum). On the other hand, \(\left(1+x\right)^{-1} =\sum _{n\in \mathbb {N}}\left(-1\right)^{n}x^{n}\). Comparing these two equalities, we find

Now, we can apply the chain rule to \(f=\overline{\log }\) (since \(\left[x^{0}\right]g=0\)), and thus obtain

However, we claim that \(\left(1+x\right)^{-1}\circ g=\left(1+g\right) ^{-1}\). Indeed, \(\frac{1}{1+x}\circ g=\frac{1\circ g}{\left(1+x\right)\circ g}\) (since the FPS \(1+x\) is invertible), and \(1\circ \, g=\underline{1}\) and \(\left(1+x\right)\circ g=1+g\), so \(\left(1+x\right)^{-1}\circ g=\left(1+g\right)^{-1}\). Hence, (30) becomes

This proves part (b).

By strong induction on the coefficient index. The base case uses the matching constant terms. For the inductive step, the ODE relates \([x^{n+1}] h \cdot (n+1)\) to a convolution involving only lower coefficients; by the induction hypothesis, these coincide for \(h_1\) and \(h_2\), and one cancels \(n+1\) using the \(\mathbb {Q}\)-algebra structure.

As in Lemma 1.217, by strong induction on the coefficient index, cancelling \(n+1\) at each step.

We substitute \(\overline{\exp }\) into the identity \(\iota \cdot (1 + x) = 1\), noting that \((1 + x) \circ \overline{\exp } = 1 + \overline{\exp } = \exp \).

Write \(f\) in the form \(f=\sum _{n\in \mathbb {N}}f_{n}x^{n}\) with \(f_{0},f_{1},f_{2},\ldots \in K\). Thus, \(f_{0}=\left[x^{0}\right]f\). Now, \(f\left[g\right]=\sum _{n\in \mathbb {N}}f_{n}g^{n}\). However, \(\left[x^{0}\right] \left(\sum _{n\in \mathbb {N}}f_{n}g^{n}\right)=f_{0}=\left[x^{0}\right] f\). In view of \(f\circ g=f\left[g\right]=\sum _{n\in \mathbb {N}}f_{n}g^{n}\), we can rewrite this as \(\left[x^{0}\right]\left(f\circ g\right) =\left[x^{0}\right]f\).

Let us first prove that \(\overline{\log }\circ \overline{\exp }=x\).

The idea of this proof is to show that \(\overline{\log }\circ \overline{\exp }\) and \(x\) are two FPSs with the same constant term (namely, \(0\)) and with the same derivative. Once this is proved, they must be equal (since a FPS is determined by its constant term and its derivative over a \(\mathbb {Q}\)-algebra).

We have \(\left[x^{0}\right]\overline{\exp }=0\) (since \(\overline{\exp }=\sum _{n\geq 1}\frac{1}{n!}x^{n}\)). Hence, Lemma 1.220 (applied to \(f=\overline{\log }\) and \(g=\overline{\exp }\)) yields \(\left[x^{0}\right]\left(\overline{\log }\circ \overline{\exp }\right)=\left[x^{0}\right]\overline{\log }=0\) (since \(\overline{\log }=\sum _{n\geq 1}\frac{\left(-1\right)^{n-1}}{n}x^{n}\)). Now,

However, \(\overline{\exp }=\exp -1\) and thus \(1+\overline{\exp }=\exp \). Now, Proposition 1.216 (b) (applied to \(g=\overline{\exp }\)) yields

(where the underbrace uses (28), and \(x^{\prime }=1\)). Hence, \(\overline{\log }\circ \overline{\exp }-x\) is constant (since its derivative is \(0\)). In view of (31), this constant must be \(0\). Thus, \(\overline{\log }\circ \overline{\exp }=x\).

Now it remains to prove that \(\overline{\exp }\circ \overline{\log }=x\).

We shall first show that \(\exp \circ \overline{\log }=1+x\).

To wit: The FPS \(1+x\) is invertible. Applying the quotient rule to \(f=\exp \circ \, \overline{\log }\) and \(g=1+x\), we obtain

In view of

(where we used (29)) and \(\left(1+x\right)^{\prime }=1\), we can rewrite this as

Thus, \(\frac{\exp \circ \, \overline{\log }}{1+x}\) is constant, say equal to \(\underline{a}\) for some \(a\in K\). Then \(\exp \circ \, \overline{\log }=a\left(1+x\right)\), so \(\left[x^{0}\right]\left(\exp \circ \, \overline{\log }\right)=a\). However, it is easy to see that \(\left[x^{0}\right]\left(\exp \circ \, \overline{\log }\right)=1\) (using Lemma 1.220). Comparing, we find \(a=1\). Thus, \(\exp \circ \, \overline{\log }=1+x\).

Now, \(\overline{\exp }=\exp -1=\exp +\, \underline{-1}\). Hence,

This completes the proof.

(a) Let \(f,g\in K\left[\left[x\right]\right]_{0}\). Then \(\left[ x^{0}\right]f=0\) and \(\left[x^{0}\right]g=0\). Hence, Lemma 1.220 yields \(\left[x^{0}\right]\left(f\circ g\right)=\left[x^{0}\right]f=0\). In other words, \(f\circ g\in K\left[ \left[x\right]\right]_{0}\).

(b) This is analogous to the proof of part (a).

(c) Let \(g\in K\left[\left[x\right]\right]_{0}\). From \(\exp =\sum _{n\in \mathbb {N}}\frac{1}{n!}x^{n}\), we obtain \(\left[ x^{0}\right]\exp =1\), so that \(\exp \in K\left[\left[ x\right]\right]_{1}\). Hence, part (b) (applied to \(f=\exp \)) yields \(\exp \circ g\in K\left[\left[ x\right]\right]_{1}\).

(d) Let \(f\in K\left[\left[x\right]\right]_{1}\). Thus, \(\left[x^{0}\right]f=1\). Now, \(\left[x^{0}\right]\left(f-1\right)=\left[x^{0}\right] f-\left[x^{0}\right]1=1-1=0\), so that \(f-1\in K\left[\left[x\right]\right]_{0}\). Furthermore, \(\left[x^{0}\right] \overline{\log }=0\) and thus \(\overline{\log }\in K\left[\left[ x\right]\right]_{0}\). Hence, part (a) (applied to \(\overline{\log }\) and \(f-1\) instead of \(f\) and \(g\)) yields \(\overline{\log }\circ \left(f-1\right)\in K\left[\left[x\right] \right]_{0}\).

First, we make a simple auxiliary observation: Each \(g\in K\left[\left[x\right]\right]_{0}\) satisfies

[Proof of (32): Recall that \(\overline{\exp }=\exp -1\), so that \(\exp =\overline{\exp }+\underline{1}\). Hence, \(\exp \circ g=\left(\overline{\exp }+\underline{1}\right)\circ g=\overline{\exp }\circ g+\underline{1}\circ g\). But \(\underline{1}\circ g=\underline{1}=1\). Hence, \(\exp \circ g=\overline{\exp }\circ g+1\).]

Now, let us show that \(\operatorname {Exp}\circ \operatorname {Log} =\operatorname {id}\). Indeed, we fix some \(f\in K\left[\left[x\right] \right]_{1}\). Then, \(f-1\in K\left[\left[x\right]\right]_{0}\) (by Lemma 1.223 (d)). By associativity of composition and Theorem 1.221, we get

Hence

(by (32)), so

Using a similar argument (with \(\overline{\log }\circ \overline{\exp }=x\) from Theorem 1.221), we can show that \(\operatorname {Log}\circ \operatorname {Exp}=\operatorname {id}\). Combining, \(\operatorname {Exp}\) and \(\operatorname {Log}\) are mutually inverse bijections.

\([x^0](f - 1) = [x^0]f - 1 = 1 - 1 = 0\).

By strong induction on the coefficient index. The ODE gives \([x^{n+1}] h \cdot (n+1) = [x^n](h \cdot g)\); the right side is a convolution involving only coefficients of \(h\) of index \(\le n\), which agree by induction hypothesis. Cancelling \(n+1\) uses the \(\mathbb {Q}\)-algebra structure.

\(\operatorname {Exp}(0) = \exp \circ 0 = 1\) (since \([x^0]\exp = 1\) and substituting \(0\) picks out the constant term). \(\operatorname {Log}(1) = \overline{\log } \circ (1 - 1) = \overline{\log } \circ 0 = 0\) (since \([x^0]\overline{\log } = 0\)).

(a) Let \(f,g\in K\left[\left[x\right]\right]_{0}\). Thus, \(\left[ x^{0}\right]f=0\) and \(\left[x^{0}\right]g=0\). By the definition of \(\operatorname {Exp}\), we have

Similarly, \(\operatorname {Exp}g=\sum _{n\in \mathbb {N}}\frac{1}{n!}g^{n}\) and \(\operatorname {Exp}\left(f+g\right)=\sum _{n\in \mathbb {N}}\frac{1}{n!}\left(f+g\right)^{n}\).

Now, the latter equality becomes

Comparing this with \(\operatorname {Exp}f\cdot \operatorname {Exp}g =\sum _{k\in \mathbb {N}}\ \ \sum _{\ell \in \mathbb {N}}\frac{1}{k!\ell !}f^{k}g^{\ell }\), we obtain \(\operatorname {Exp}\left(f+g\right)=\operatorname {Exp} f\cdot \operatorname {Exp}g\).

(In the Lean formalization, this is proved via ODE uniqueness: both sides satisfy the ODE \(h^{\prime } = h \cdot (f^{\prime } + g^{\prime })\) with the same initial condition.)

(b) This follows from part (a), since we know that \(\operatorname {Log}\) is inverse to \(\operatorname {Exp}\). Setting \(u=\operatorname {Log}f\) and \(v=\operatorname {Log}g\), part (a) gives \(\operatorname {Exp}\left(u+v\right)=\operatorname {Exp}u\cdot \operatorname {Exp}v\), and applying \(\operatorname {Log}\) (using Lemma 1.224) yields \(\operatorname {Log}\left(fg\right)=\operatorname {Log}f+\operatorname {Log}g\).

(a) It is clear that the set \(K\left[\left[x\right]\right]_{0}\) contains the FPS \(0\) (since \(\left[x^{0}\right]0=0\)). If \(f,g\in K\left[\left[x\right]\right]_{0}\), then \(\left[x^{0}\right]f=0\) and \(\left[x^{0}\right]g=0\), and therefore \(f+g\in K\left[\left[x\right]\right]_{0}\) (since \(\left[x^{0}\right]\left( f+g\right)=0+0=0\)) and \(f-g\in K\left[\left[x\right]\right] _{0}\) (by a similar argument).

(b) Any \(a\in K\left[\left[ x\right]\right]_{1}\) is invertible in \(K\left[\left[x\right]\right]\) (since \(\left[x^{0}\right]a=1\) is invertible in \(K\)). Next, \(K\left[\left[x\right]\right]_{1}\) is closed under multiplication: if \(f,g\in K\left[\left[x\right]\right]_{1}\), then \(\left[x^{0}\right]f=1\) and \(\left[x^{0}\right]g=1\), and therefore \(\left[x^{0}\right]\left( fg\right)=1\cdot 1=1\). Similarly, \(K\left[\left[x\right]\right]_{1}\) is closed under division.

Lemma 1.228 yields that these two maps are group homomorphisms. Lemma 1.224 shows that they are mutually inverse. Combining these results, we conclude that these two maps are mutually inverse group isomorphisms.

Both sides multiply with \((1+x)\) to give \(1\); since the constant coefficient of \(1+x\) is nonzero, the inverse is unique.

Substitution is a ring homomorphism, so \((a \circ g) \cdot (b \circ g) = (a \cdot b) \circ g = 1 \circ g = 1\). Since \([x^0](a \circ g) \ne 0\), the inverse is unique.

Since \([x^0]f\) is a unit, the invertibility criterion for power series gives the result (a power series is invertible if and only if its constant coefficient is invertible). The constant coefficient of \(f^{-1}\) is the inverse of \([x^0]f = 1\).

\(1' = 0\), so \(\operatorname {loder}(1) = 0 \cdot 1^{-1} = 0\).

The definition of \(\operatorname {Log}\) yields \(\operatorname {Log}f=\overline{\log }\circ \left( f-1\right)\).

From \(f\in K\left[\left[x\right]\right]_{1}\), we obtain \(\left[ x^{0}\right]f=1\). Now, \(\left[x^{0}\right] \left(f-1\right)=\left[x^{0}\right]f-\left[x^{0}\right]1=0\). Hence, Proposition 1.216 (b) (applied to \(g=f-1\)) yields

In view of \(\operatorname {Log}f=\overline{\log }\circ \left(f-1\right)\), we can rewrite this as \(\left(\operatorname {Log}f\right)^{\prime }=\frac{\left(f-1\right) ^{\prime }}{f}\).

Since \(\left(f-1\right)^{\prime }=f^{\prime }\), we can rewrite this further as \(\left(\operatorname {Log}f\right)^{\prime }=\frac{f^{\prime }}{f}=\operatorname {loder}f\).

The definition of a logarithmic derivative yields \(\operatorname {loder}f=\frac{f^{\prime }}{f}\) and \(\operatorname {loder}g=\frac{g^{\prime }}{g}\), but it also yields

Induct on \(k\). The base case (\(k=0\)) requires showing that \(\operatorname {loder}1=0\), which is easy to see from the definition of a logarithmic derivative (since \(1^{\prime }=0\)). The induction step follows easily from Proposition 1.237.

First of all, \(f\) is invertible. This shows that \(f^{-1}\) is well-defined.

Proposition 1.237 (applied to \(g=f^{-1}\)) yields \(\operatorname {loder}\left(ff^{-1}\right)=\operatorname {loder} f+\operatorname {loder}\left(f^{-1}\right)\). However, we also have \(\operatorname {loder}\left(\underbrace{ff^{-1}}_{=1}\right) =\operatorname {loder}1=0\) (since \(1^{\prime }=0\)). Comparing these two equalities, we obtain \(\operatorname {loder}f+\operatorname {loder}\left( f^{-1}\right)=0\). In other words, \(\operatorname {loder}\left( f^{-1}\right)=-\operatorname {loder}f\).

For the sum: the constant coefficient of each \(f_i\) is \(0\), so the sum of constant coefficients is \(0\). For the product: the constant coefficient of \(\prod f_i\) is \(\prod [x^0](f_i) = \prod 1 = 1\).

For each \(n\), let \(M\) be an \(x^n\)-approximator for the product family. If \(i \notin M\), then \([x^k](f_i) = 0\) for \(1 \le k \le n\) (by the approximator property). This forces \([(f_i - 1)]_k = 0\) for \(0 \le k \le n\), and a substitution argument shows \([\operatorname {Log} f_i]_n = 0\). Hence the set of \(i\) with nonzero \(n\)-th coefficient is contained in \(M\).

For each \(n\), choose an \(x^n\)-approximator \(M\). By the finite version (\(\operatorname {Log}\) of a finite product equals the sum of \(\operatorname {Log}\)s, which follows from Lemma 1.228(b) by induction), we have \(\operatorname {Log}(\prod _{i \in M} f_i) = \sum _{i \in M} \operatorname {Log}(f_i)\). The \(n\)-th coefficient of the infinite product agrees with that of the finite product over \(M\), and the \(n\)-th coefficient of the sum is the finite sum over \(M\) (since \([\operatorname {Log} f_i]_n = 0\) for \(i \notin M\)). A coefficient comparison argument completes the proof.

Since \(\operatorname {Exp}(g_i) = 1 + \overline{\exp } \circ g_i\), the family is of the form \((1 + h_i)\) where \(h_i = \overline{\exp } \circ g_i\). The key observation is that if \([x^k](g_i) = 0\) for all \(k \le n\), then \([x^n](\overline{\exp } \circ g_i) = 0\) as well (since \(\overline{\exp }\) has constant term \(0\), so the substitution preserves vanishing of low-order terms). The summability of \((g_i)\) then implies the multipliability of \((1 + h_i)\).

Let \(f_i = \operatorname {Exp}(g_i)\). By Proposition 1.242, \(\operatorname {Log}(\prod f_i) = \sum \operatorname {Log}(f_i) = \sum g_i\) (using \(\operatorname {Log} \circ \operatorname {Exp} = \mathrm{id}\)). Applying \(\operatorname {Exp}\) to both sides and using \(\operatorname {Exp} \circ \operatorname {Log} = \mathrm{id}\) yields the result.