\documentclass[numbers=enddot,12pt,final,onecolumn,notitlepage]{scrartcl}%
\usepackage{amsfonts}
\usepackage[headsepline,footsepline,manualmark]{scrlayer-scrpage}
\usepackage[all,cmtip]{xy}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{framed}
\usepackage{comment}
\usepackage{color}
\usepackage{hyperref}
\usepackage{ifthen}
\usepackage[sc]{mathpazo}
\usepackage[T1]{fontenc}
\usepackage{needspace}
\usepackage{tabls}
\usepackage{graphicx}%
\setcounter{MaxMatrixCols}{30}
%TCIDATA{OutputFilter=latex2.dll}
%TCIDATA{Version=5.50.0.2960}
%TCIDATA{LastRevised=Friday, December 15, 2017 23:12:09}
%TCIDATA{<META NAME="GraphicsSave" CONTENT="32">}
%TCIDATA{<META NAME="SaveForMode" CONTENT="1">}
%TCIDATA{BibliographyScheme=Manual}
%BeginMSIPreambleData
\providecommand{\U}[1]{\protect\rule{.1in}{.1in}}
%EndMSIPreambleData
\newcounter{exer}
\theoremstyle{definition}
\newtheorem{theo}{Theorem}[section]
\newenvironment{theorem}[1][]
{\begin{theo}[#1]\begin{leftbar}}
{\end{leftbar}\end{theo}}
\newtheorem{lem}[theo]{Lemma}
\newenvironment{lemma}[1][]
{\begin{lem}[#1]\begin{leftbar}}
{\end{leftbar}\end{lem}}
\newtheorem{prop}[theo]{Proposition}
\newenvironment{proposition}[1][]
{\begin{prop}[#1]\begin{leftbar}}
{\end{leftbar}\end{prop}}
\newtheorem{defi}[theo]{Definition}
\newenvironment{definition}[1][]
{\begin{defi}[#1]\begin{leftbar}}
{\end{leftbar}\end{defi}}
\newtheorem{remk}[theo]{Remark}
\newenvironment{remark}[1][]
{\begin{remk}[#1]\begin{leftbar}}
{\end{leftbar}\end{remk}}
\newtheorem{coro}[theo]{Corollary}
\newenvironment{corollary}[1][]
{\begin{coro}[#1]\begin{leftbar}}
{\end{leftbar}\end{coro}}
\newtheorem{conv}[theo]{Convention}
\newenvironment{condition}[1][]
{\begin{conv}[#1]\begin{leftbar}}
{\end{leftbar}\end{conv}}
\newtheorem{quest}[theo]{Question}
\newenvironment{algorithm}[1][]
{\begin{quest}[#1]\begin{leftbar}}
{\end{leftbar}\end{quest}}
\newtheorem{warn}[theo]{Warning}
\newenvironment{conclusion}[1][]
{\begin{warn}[#1]\begin{leftbar}}
{\end{leftbar}\end{warn}}
\newtheorem{conj}[theo]{Conjecture}
\newenvironment{conjecture}[1][]
{\begin{conj}[#1]\begin{leftbar}}
{\end{leftbar}\end{conj}}
\newtheorem{exam}[theo]{Example}
\newenvironment{example}[1][]
{\begin{exam}[#1]\begin{leftbar}}
{\end{leftbar}\end{exam}}
\newtheorem{exmp}[exer]{Exercise}
\newenvironment{exercise}[1][]
{\begin{exmp}[#1]\begin{leftbar}}
{\end{leftbar}\end{exmp}}
\newenvironment{statement}{\begin{quote}}{\end{quote}}
\iffalse
\newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} }{\ \rule{0.5em}{0.5em}}
\fi
\let\sumnonlimits\sum
\let\prodnonlimits\prod
\let\cupnonlimits\bigcup
\let\capnonlimits\bigcap
\renewcommand{\sum}{\sumnonlimits\limits}
\renewcommand{\prod}{\prodnonlimits\limits}
\renewcommand{\bigcup}{\cupnonlimits\limits}
\renewcommand{\bigcap}{\capnonlimits\limits}
\setlength\tablinesep{3pt}
\setlength\arraylinesep{3pt}
\setlength\extrarulesep{3pt}
\voffset=0cm
\hoffset=-0.7cm
\setlength\textheight{22.5cm}
\setlength\textwidth{15.5cm}
\newenvironment{verlong}{}{}
\newenvironment{vershort}{}{}
\newenvironment{noncompile}{}{}
\excludecomment{verlong}
\includecomment{vershort}
\excludecomment{noncompile}
\newcommand{\id}{\operatorname{id}}
\newcommand{\rev}{\operatorname{rev}}
\newcommand{\conncomp}{\operatorname{conncomp}}
\newcommand{\conn}{\operatorname{conn}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\powset}[2][]{\ifthenelse{\equal{#2}{}}{\mathcal{P}\left(#1\right)}{\mathcal{P}_{#1}\left(#2\right)}}
\newcommand{\set}[1]{\left\{ #1 \right\}}
\newcommand{\abs}[1]{\left| #1 \right|}
\newcommand{\tup}[1]{\left( #1 \right)}
\newcommand{\ive}[1]{\left[ #1 \right]}
\newcommand{\verts}[1]{\operatorname{V}\left( #1 \right)}
\newcommand{\edges}[1]{\operatorname{E}\left( #1 \right)}
\newcommand{\arcs}[1]{\operatorname{A}\left( #1 \right)}
\newcommand{\underbrack}[2]{\underbrace{#1}_{\substack{#2}}}
\newcommand{\are}{\ar@{-}}
\newcommand{\arebi}[1][]{\ar@{<-}@/_/[#1] \ar@/^/[#1]}
\newcommand\arxiv[1]{\href{http://www.arxiv.org/abs/#1}{\texttt{arXiv:#1}}}
\ihead{Why log and exp are inverse}
\ohead{page \thepage}
\cfoot{}
\begin{document}

\begin{center}
\textbf{Why the log and exp series are mutually inverse}

\textit{Darij Grinberg,
%TCIMACRO{\TeXButton{today}{\today}}%
%BeginExpansion
\today
%EndExpansion
}
\end{center}

The purpose of this note is to detail an argument that I have only briefly
mentioned in class: namely, the (algebraic) proof of the fact that the power
series $\exp$ and $\log$ (or, more precisely, $\exp x-1$ and $\log\left(
1+x\right)  $) are mutually inverse. Along the way, I will prove a few basic
properties of the derivative of formal power series. A significant part of
this note is copy-pasted from \cite[solution to Exercise 1.7.20]{GriRei16}.

First, let us recall the setting in which we are working.

We let $\mathbf{k}$ be a commutative $\mathbb{Q}$-algebra. For example,
$\mathbf{k}$ can be one of the fields $\mathbb{Q}$, $\mathbb{R}$ and
$\mathbb{C}$. (If you are curious: A $\mathbb{Q}$\textit{-algebra} is a ring
whose elements can be divided by $1,2,3,\ldots$. Thus, $\mathbb{Z}$ is not a
$\mathbb{Q}$-algebra, since $2$ cannot be divided by $3$ \textbf{inside}
$\mathbb{Z}$.)

(In class, I used the notation $K$ for $\mathbf{k}$.)

We consider the ring $\mathbf{k}\left[  \left[  x\right]  \right]  $ of formal
power series in one indeterminate $x$ over $\mathbf{k}$. We shall abbreviate
the notion \textquotedblleft formal power series\textquotedblright\ by
\textquotedblleft\textit{FPS}\textquotedblright.

If $f\in\mathbf{k}\left[  \left[  x\right]  \right]  $ and $g\in
\mathbf{k}\left[  \left[  x\right]  \right]  $ are two FPSs such that the
constant term of $g$ is $0$, then we can define a new FPS $f\left[  g\right]
\in\mathbf{k}\left[  \left[  x\right]  \right]  $ by%
\[
f\left[  g\right]  =\sum_{n\geq0}f_{n}g^{n},
\]
where $f_{0},f_{1},f_{2},\ldots$ are the coefficients of $f$ (so that
$f=\sum_{n\geq0}f_{n}x^{n}$). The sum $\sum_{n\geq0}f_{n}g^{n}$ is
well-defined, because the family $\left(  f_{n}g^{n}\right)  _{n\in\mathbb{N}%
}$ is summable (i.e., for each $i\in\mathbb{N}$, only finitely many entries of
this family have a nonzero $x^{i}$-coefficient); this is thanks to our
assumption that the constant term of $g$ is $0$. The FPS $f\left[  g\right]  $
is called the \textit{composition} of $f$ with $g$ (or the result of
\textit{substituting} $g$ into $f$). An alternative notation for $f\left[
g\right]  $ is $f\circ g$. (Some authors also write $f\left(  g\right)  $
instead of $f\left[  g\right]  $, but this is dangerous notation, since
$f\left(  g\right)  $ may just as well mean the product of $f$ with $g$; thus,
we shall stick to the notation $f\left[  g\right]  $.)

We define two FPSs $\exp\in\mathbf{k}\left[  \left[  x\right]  \right]  $ and
$\overline{\log}\in\mathbf{k}\left[  \left[  x\right]  \right]  $ by
\[
\exp=\sum_{n\geq0}\dfrac{1}{n!}x^{n}\ \ \ \ \ \ \ \ \ \ \text{and}%
\ \ \ \ \ \ \ \ \ \ \overline{\log}=\sum_{n\geq1}\dfrac{\left(  -1\right)
^{n-1}}{n}x^{n}.
\]
Here, we are using that $\mathbf{k}$ is a $\mathbb{Q}$-algebra. (If we only
knew that $\mathbf{k}$ is a ring, then we wouldn't be able to divide by $n!$
and by $n$ in these formulas.)

The FPS $\overline{\log}$ defined above is commonly called $\log\left(
1+x\right)  $ (because it is precisely the Taylor series of the $\log\left(
1+z\right)  $ function from complex analysis). However, I will avoid the
\textquotedblleft$\log\left(  1+x\right)  $\textquotedblright\ notation,
because it looks like it is a combination of something called
\textquotedblleft$\log$\textquotedblright\ with something called
\textquotedblleft$1+x$\textquotedblright, but I have not introduced anything
called \textquotedblleft$\log$\textquotedblright. (In fact, there is no FPS
called \textquotedblleft$\log$\textquotedblright.)

The FPS $\overline{\log}$ has constant term $0$ (because the sum in its
definition starts at $n=1$). The FPS $\exp$ has constant term $\dfrac{1}%
{0!}=1$; thus, the FPS $\exp-1$ has constant term $1-1=0$. Let us denote the
FPS $\exp-1$ by $\overline{\exp}$. Then, both FPSs $\overline{\exp}$ and
$\overline{\log}$ have constant term $0$; hence, they can be substituted into
one another. We now claim the following:

\begin{theorem}
\label{thm.exp-log-inv}We have $\overline{\exp}\left[  \overline{\log}\right]
=x$ and $\overline{\log}\left[  \overline{\exp}\right]  =x$.
\end{theorem}

Theorem \ref{thm.exp-log-inv} is an \textquotedblleft algebraic
analogue\textquotedblright\ of the well-known fact from calculus that the
exponential function and the natural logarithm function are each other's
inverse. It is often used in enumerative combinatorics (for computing
generating functions). We shall give a purely algebraic proof (somewhat
similar to the one given in \cite[Example 7.67]{Loehr-bij}). Other proofs
(some combinatorial, some analytic) can be found in the literature.

The proof of Theorem \ref{thm.exp-log-inv} uses the concept of the
\textit{derivative} of an FPS. This concept is very simple (a lot simpler than
the concept of derivative in analysis, where it requires dealing with the
intricacies of convergence and differentiability): The \textit{derivative} of
an FPS $f\in\mathbf{k}\left[  \left[  x\right]  \right]  $ is defined to be
the FPS $\sum_{n\geq1}nf_{n}x^{n-1}$, where $f_{0},f_{1},f_{2},\ldots$ are the
coefficients of $f$ (so that $f=\sum_{n\geq0}f_{n}x^{n}$). This derivative is
denoted by $f^{\prime}$ or by $\dfrac{d}{dx}f$.

The following properties of derivatives are easy to check:

\begin{proposition}
\label{prop.derivatives.leibniz}\textbf{(a)} We have $\dfrac{d}{dx}\left(
f+g\right)  =\dfrac{d}{dx}f+\dfrac{d}{dx}g$ for any $f\in\mathbf{k}\left[
\left[  x\right]  \right]  $ and $g\in\mathbf{k}\left[  \left[  x\right]
\right]  $.

\textbf{(b)} We have $\dfrac{d}{dx}\left(  \lambda f\right)  =\lambda\dfrac
{d}{dx}f$ for any $f\in\mathbf{k}\left[  \left[  x\right]  \right]  $ and
$\lambda\in\mathbf{k}$.

\textbf{(c)} We have $\dfrac{d}{dx}\left(  fg\right)  =\left(  \dfrac{d}%
{dx}f\right)  g+f\left(  \dfrac{d}{dx}g\right)  $ for any $f\in\mathbf{k}%
\left[  \left[  x\right]  \right]  $ and $g\in\mathbf{k}\left[  \left[
x\right]  \right]  $. (Keep in mind that $f\left(  \dfrac{d}{dx}g\right)  $
means the \textbf{product} of $f$ with $\dfrac{d}{dx}g$, not the composition
of $f$ with $\dfrac{d}{dx}g$. The latter would be denoted by $f\left[
\dfrac{d}{dx}g\right]  $.)

\textbf{(d)} We have $\dfrac{d}{dx}\left(  w^{n}\right)  =n\left(  \dfrac
{d}{dx}w\right)  w^{n-1}$ for any $w\in\mathbf{k}\left[  \left[  x\right]
\right]  $ and any positive integer $n$.

\textbf{(e)} If $v\in\mathbf{k}\left[  \left[  x\right]  \right]  $ is an FPS
that has a multiplicative inverse $v^{-1}$, then $\dfrac{d}{dx}\left(
v^{-1}\right)  =-v^{-2}\left(  \dfrac{d}{dx}v\right)  $.
\end{proposition}

Proposition \ref{prop.derivatives.leibniz} \textbf{(c)} is known as the
\textit{Leibniz rule}.

\begin{proof}
[Proof of Proposition \ref{prop.derivatives.leibniz}.]We leave the easy proofs
of parts \textbf{(a)} and \textbf{(b)} to the reader.

\textbf{(c)} Let $f\in\mathbf{k}\left[  \left[  x\right]  \right]  $ and
$g\in\mathbf{k}\left[  \left[  x\right]  \right]  $.

Let $f_{0},f_{1},f_{2},\ldots$ be the coefficients of $f$; thus,
\begin{equation}
f=\sum_{n\geq0}f_{n}x^{n}. \label{pf.prop.derivatives.leibniz.c.f=}%
\end{equation}
Hence, the definition of $\dfrac{d}{dx}f$ yields
\begin{equation}
\dfrac{d}{dx}f=\sum_{n\geq1}nf_{n}x^{n-1}=\sum_{n\geq0}\left(  n+1\right)
f_{n+1}x^{n} \label{pf.prop.derivatives.leibniz.c.df=}%
\end{equation}
(here, we have substituted $n+1$ for $n$ in the sum).

Let $g_{0},g_{1},g_{2},\ldots$ be the coefficients of $g$; thus,
\begin{equation}
g=\sum_{n\geq0}g_{n}x^{n}. \label{pf.prop.derivatives.leibniz.c.g=}%
\end{equation}
Hence, the definition of $\dfrac{d}{dx}g$ yields
\begin{equation}
\dfrac{d}{dx}g=\sum_{n\geq1}ng_{n}x^{n-1}=\sum_{n\geq0}\left(  n+1\right)
g_{n+1}x^{n} \label{pf.prop.derivatives.leibniz.c.dg=}%
\end{equation}
(here, we have substituted $n+1$ for $n$ in the sum).

Multiplying the equalities (\ref{pf.prop.derivatives.leibniz.c.df=}) and
(\ref{pf.prop.derivatives.leibniz.c.g=}), we obtain%
\begin{align}
\left(  \dfrac{d}{dx}f\right)  g  &  =\left(  \sum_{n\geq0}\left(  n+1\right)
f_{n+1}x^{n}\right)  \left(  \sum_{n\geq0}g_{n}x^{n}\right) \nonumber\\
&  =\sum_{n\geq0}\left(  \sum_{k=0}^{n}\left(  k+1\right)  f_{k+1}%
g_{n-k}\right)  x^{n} \label{pf.prop.derivatives.leibniz.c.2}%
\end{align}
(by the definition of the product of two FPSs).

Multiplying the equalities (\ref{pf.prop.derivatives.leibniz.c.f=}) and
(\ref{pf.prop.derivatives.leibniz.c.dg=}), we obtain%
\begin{align}
f\left(  \dfrac{d}{dx}g\right)   &  =\left(  \sum_{n\geq0}f_{n}x^{n}\right)
\left(  \sum_{n\geq0}\left(  n+1\right)  g_{n+1}x^{n}\right) \nonumber\\
&  =\sum_{n\geq0}\left(  \sum_{k=0}^{n}f_{k}\left(  n-k+1\right)
g_{n-k+1}\right)  x^{n} \label{pf.prop.derivatives.leibniz.c.3}%
\end{align}
(by the definition of the product of two FPSs).

Adding the equalities (\ref{pf.prop.derivatives.leibniz.c.2}) and
(\ref{pf.prop.derivatives.leibniz.c.3}) together, we find%
\begin{align}
&  \left(  \dfrac{d}{dx}f\right)  g+f\left(  \dfrac{d}{dx}g\right)
\nonumber\\
&  =\sum_{n\geq0}\left(  \sum_{k=0}^{n}\left(  k+1\right)  f_{k+1}%
g_{n-k}\right)  x^{n}+\sum_{n\geq0}\left(  \sum_{k=0}^{n}f_{k}\left(
n-k+1\right)  g_{n-k+1}\right)  x^{n}\nonumber\\
&  =\sum_{n\geq0}\left(  \sum_{k=0}^{n}\left(  k+1\right)  f_{k+1}g_{n-k}%
+\sum_{k=0}^{n}f_{k}\left(  n-k+1\right)  g_{n-k+1}\right)  x^{n}%
\label{pf.prop.derivatives.leibniz.c.4}%
\end{align}
(by the definition of the sum of two FPSs).

Multiplying the equalities (\ref{pf.prop.derivatives.leibniz.c.f=}) and
(\ref{pf.prop.derivatives.leibniz.c.g=}), we obtain%
\[
fg=\left(  \sum_{n\geq0}f_{n}x^{n}\right)  \left(  \sum_{n\geq0}g_{n}%
x^{n}\right)  =\sum_{n\geq0}\left(  \sum_{k=0}^{n}f_{k}g_{n-k}\right)  x^{n}%
\]
(by the definition of the product of two FPSs). Thus, $\sum_{k=0}^{0}%
f_{k}g_{0-k},\sum_{k=0}^{1}f_{k}g_{1-k},\sum_{k=0}^{2}f_{k}g_{2-k},\ldots$ are
the coefficients of the FPS $fg$. Hence, the definition of a derivative yields%
\begin{equation}
\dfrac{d}{dx}\left(  fg\right)  =\sum_{n\geq1}n\left(  \sum_{k=0}^{n}%
f_{k}g_{n-k}\right)  x^{n-1}.\label{pf.prop.derivatives.leibniz.c.5}%
\end{equation}


But each $n\in\mathbb{N}$ satisfies%
\begin{align*}
&  n\left(  \sum_{k=0}^{n}f_{k}g_{n-k}\right)  \\
&  =\sum_{k=0}^{n}\underbrace{n}_{=k+\left(  n-k\right)  }f_{k}g_{n-k}%
=\sum_{k=0}^{n}\underbrace{\left(  k+\left(  n-k\right)  \right)  f_{k}%
g_{n-k}}_{=kf_{k}g_{n-k}+f_{k}\left(  n-k\right)  g_{n-k}}\\
&  =\sum_{k=0}^{n}\left(  kf_{k}g_{n-k}+f_{k}\left(  n-k\right)
g_{n-k}\right)  \\
&  =\underbrace{\sum_{k=0}^{n}kf_{k}g_{n-k}}_{=0f_{0}g_{n-0}+\sum_{k=1}%
^{n}kf_{k}g_{n-k}}+\underbrace{\sum_{k=0}^{n}f_{k}\left(  n-k\right)  g_{n-k}%
}_{=\sum_{k=0}^{n-1}f_{k}\left(  n-k\right)  g_{n-k}+f_{n}\left(  n-n\right)
g_{n-n}}\\
&  =\underbrace{0f_{0}g_{n-0}}_{=0}+\sum_{k=1}^{n}kf_{k}g_{n-k}+\sum
_{k=0}^{n-1}f_{k}\left(  n-k\right)  g_{n-k}+\underbrace{f_{n}\left(
n-n\right)  g_{n-n}}_{\substack{=0\\\text{(since }n-n=0\text{)}}}\\
&  =\sum_{k=1}^{n}kf_{k}g_{n-k}+\sum_{k=0}^{n-1}f_{k}\left(  n-k\right)
g_{n-k}\\
&  =\sum_{k=0}^{n-1}\left(  k+1\right)  f_{k+1}g_{n-\left(  k+1\right)  }%
+\sum_{k=0}^{n-1}f_{k}\left(  n-k\right)  g_{n-k}\\
&  \ \ \ \ \ \ \ \ \ \ \left(  \text{here, we have substituted }k+1\text{ for
}k\text{ in the first sum}\right)  .
\end{align*}
Thus, (\ref{pf.prop.derivatives.leibniz.c.5}) becomes%
\begin{align*}
&  \dfrac{d}{dx}\left(  fg\right)  \\
&  =\sum_{n\geq1}\underbrace{n\left(  \sum_{k=0}^{n}f_{k}g_{n-k}\right)
}_{=\sum_{k=0}^{n-1}\left(  k+1\right)  f_{k+1}g_{n-\left(  k+1\right)  }%
+\sum_{k=0}^{n-1}f_{k}\left(  n-k\right)  g_{n-k}}x^{n-1}\\
&  =\sum_{n\geq1}\left(  \sum_{k=0}^{n-1}\left(  k+1\right)  f_{k+1}%
g_{n-\left(  k+1\right)  }+\sum_{k=0}^{n-1}f_{k}\left(  n-k\right)
g_{n-k}\right)  x^{n-1}\\
&  =\sum_{n\geq0}\left(  \underbrace{\sum_{k=0}^{\left(  n+1\right)  -1}%
}_{=\sum_{k=0}^{n}}\left(  k+1\right)  f_{k+1}\underbrace{g_{\left(
n+1\right)  -\left(  k+1\right)  }}_{=g_{n-k}}+\underbrace{\sum_{k=0}^{\left(
n+1\right)  -1}}_{=\sum_{k=0}^{n}}f_{k}\underbrace{\left(  \left(  n+1\right)
-k\right)  }_{=n-k+1}\underbrace{g_{\left(  n+1\right)  -k}}_{=g_{n-k+1}%
}\right)  x^{n}\\
&  \ \ \ \ \ \ \ \ \ \ \left(  \text{here, we have substituted }n+1\text{ for
}n\text{ in the sum}\right)  \\
&  =\sum_{n\geq0}\left(  \sum_{k=0}^{n}\left(  k+1\right)  f_{k+1}g_{n-k}%
+\sum_{k=0}^{n}f_{k}\left(  n-k+1\right)  g_{n-k+1}\right)  x^{n}\\
&  =\left(  \dfrac{d}{dx}f\right)  g+f\left(  \dfrac{d}{dx}g\right)
\end{align*}
(by (\ref{pf.prop.derivatives.leibniz.c.4})). This proves Proposition
\ref{prop.derivatives.leibniz} \textbf{(c)}.

\textbf{(d)} Proposition \ref{prop.derivatives.leibniz} \textbf{(d)} follows
easily by induction over $n$ using Proposition \ref{prop.derivatives.leibniz}
\textbf{(c)}.

\textbf{(e)} Let $v\in\mathbf{k}\left[  \left[  x\right]  \right]  $ be an FPS
that has a multiplicative inverse $v^{-1}$. The Leibniz rule (applied to $v$
and $v^{-1}$) yields%
\[
\dfrac{d}{dx}\left(  v\cdot v^{-1}\right)  =\left(  \dfrac{d}{dx}v\right)
v^{-1}+v\dfrac{d}{dx}\left(  v^{-1}\right)  .
\]
Comparing this with $\dfrac{d}{dx}\underbrace{\left(  v\cdot v^{-1}\right)
}_{=1}=\dfrac{d}{dx}1=0$, we obtain $\left(  \dfrac{d}{dx}v\right)
v^{-1}+v\dfrac{d}{dx}\left(  v^{-1}\right)  =0$. Solving this equality for
$\dfrac{d}{dx}\left(  v^{-1}\right)  $, we find%
\[
\dfrac{d}{dx}\left(  v^{-1}\right)  =-\dfrac{1}{v}\left(  \dfrac{d}%
{dx}v\right)  v^{-1}=-v^{-2}\left(  \dfrac{d}{dx}v\right)  .
\]
This proves Proposition \ref{prop.derivatives.leibniz} \textbf{(e)}.
\end{proof}

Next, we notice that%
\begin{align}
\overline{\exp}  &  =\underbrace{\exp}_{=\sum_{n\geq0}\dfrac{1}{n!}x^{n}%
}-1=\sum_{n\geq0}\dfrac{1}{n!}x^{n}-1=\underbrace{\dfrac{1}{0!}}_{=\dfrac
{1}{1}=1}\underbrace{x^{0}}_{=1}+\sum_{n\geq1}\dfrac{1}{n!}x^{n}-1\nonumber\\
&  \ \ \ \ \ \ \ \ \ \ \left(  \text{here, we have split off the addend for
}n=0\text{ from the sum}\right) \nonumber\\
&  =1+\sum_{n\geq1}\dfrac{1}{n!}x^{n}-1=\sum_{n\geq1}\dfrac{1}{n!}x^{n}.
\label{sol.convolution-series.i.expbar=}%
\end{align}
Hence, the FPS $\overline{\exp}$ has constant term $0$. Hence, the FPS
$\overline{\log}\left[  \overline{\exp}\right]  $ is well-defined.

Also,%
\begin{equation}
\overline{\log}=\sum_{n\geq1}\dfrac{\left(  -1\right)  ^{n-1}}{n}x^{n}.
\label{sol.convolution-series.i.logbar=}%
\end{equation}
Hence, the FPS $\overline{\log}$ has constant term $0$. Hence, the FPS
$\overline{\exp}\left[  \overline{\log}\right]  $ is well-defined.

For each $n\geq1$, we have%
\begin{equation}
\left(  \text{the constant term of }\overline{\log}^{n}\right)  =0
\label{sol.convolution-series.i.cstlog0}%
\end{equation}
\footnote{\textit{Proof of (\ref{sol.convolution-series.i.cstlog0}):} Let
$n\geq1$. The FPS $\overline{\log}$ is divisible by $x$ (since it has constant
term $0$). Hence, the FPS $\overline{\log}^{n}$ is divisible by $x^{n}$. Thus,
the FPS $\overline{\log}^{n}$ is also divisible by $x$ (since $x^{n}$ is
divisible by $x$ (since $n\geq1$)), and therefore has constant term $0$. In
other words, we have $\left(  \text{the constant term of }\overline{\log}%
^{n}\right)  =0$. This proves (\ref{sol.convolution-series.i.cstlog0}).}.

Substituting $\overline{\log}$ for $x$ on both sides of the equality
(\ref{sol.convolution-series.i.expbar=}), we obtain%
\[
\overline{\exp}\left[  \overline{\log}\right]  =\sum_{n\geq1}\dfrac{1}%
{n!}\overline{\log}^{n}.
\]
Hence,%
\begin{align*}
&  \left(  \text{the constant term of }\overline{\exp}\left[  \overline{\log
}\right]  \right) \\
&  =\left(  \text{the constant term of }\sum_{n\geq1}\dfrac{1}{n!}%
\overline{\log}^{n}\right) \\
&  =\sum_{n\geq1}\dfrac{1}{n!}\underbrace{\left(  \text{the constant term of
}\overline{\log}^{n}\right)  }_{\substack{=0\\\text{(by
(\ref{sol.convolution-series.i.cstlog0}))}}}=\sum_{n\geq1}\dfrac{1}{n!}0=0.
\end{align*}
In other words, the FPS $\overline{\exp}\left[  \overline{\log}\right]  $ has
constant term $0$. A similar argument (with the roles of $\overline{\exp}$ and
$\overline{\log}$ switched) shows that the FPS $\overline{\log}\left[
\overline{\exp}\right]  $ has constant term $0$.

Next, we prove some simple lemmas:

\begin{lemma}
\label{lem.I1}Let $u\in\mathbf{k}\left[  \left[  x\right]  \right]  $ and
$v\in\mathbf{k}\left[  \left[  x\right]  \right]  $ be two FPSs having the
same constant term. Assume that $\dfrac{d}{dx}u=\dfrac{d}{dx}v$. Then, $u=v$.
\end{lemma}

\begin{proof}
[Proof of Lemma \ref{lem.I1}.]Let $u_{0},u_{1},u_{2},\ldots$ be the
coefficients of the FPS $u$ (so that $u=\sum_{n\geq0}u_{n}x^{n}$). Thus,
$\dfrac{d}{dx}u=\sum_{n\geq1}nu_{n}x^{n-1}$ (by the definition of the derivative).

Let $v_{0},v_{1},v_{2},\ldots$ be the coefficients of the FPS $v$ (so that
$v=\sum_{n\geq0}v_{n}x^{n}$). Thus, $\dfrac{d}{dx}v=\sum_{n\geq1}nv_{n}%
x^{n-1}$ (by the definition of the derivative).

Now,%
\[
\sum_{n\geq1}nu_{n}x^{n-1}=\dfrac{d}{dx}u=\dfrac{d}{dx}v=\sum_{n\geq1}%
nv_{n}x^{n-1}.
\]
Comparing coefficients in front of $x^{n-1}$ on both sides of this equality,
we obtain%
\begin{equation}
nu_{n}=nv_{n}\ \ \ \ \ \ \ \ \ \ \text{for each integer }n\geq1.
\label{sol.convolution-series.i.1.pf.1}%
\end{equation}


On the other hand, the FPS $u$ has constant term $u_{0}$ (since $u=\sum
_{n\geq0}u_{n}x^{n}$), and the FPS $v$ has constant term $v_{0}$ (similarly).
Thus, the constant terms of $u$ and $v$ are $u_{0}$ and $v_{0}$, respectively.
Therefore, $u_{0}=v_{0}$ (since the FPSs $u$ and $v$ have the same constant term).

Now, each $n\in\mathbb{N}$ satisfies $u_{n}=v_{n}$%
\ \ \ \ \footnote{\textit{Proof.} Let $n\in\mathbb{N}$. We must prove that
$u_{n}=v_{n}$.
\par
If $n=0$, then this follows immediately from $u_{0}=v_{0}$. Hence, we WLOG
assume that we don't have $n=0$. Thus, $n\geq1$ (since $n\in\mathbb{N}$).
Therefore, (\ref{sol.convolution-series.i.1.pf.1}) yields $nu_{n}=nv_{n}$. We
can multiply both sides of this equality by $\dfrac{1}{n}$ (since $\mathbf{k}$
is a $\mathbb{Q}$-algebra), and thus obtain $u_{n}=v_{n}$, qed.}. Hence,
$\sum_{n\geq0}\underbrace{u_{n}}_{=v_{n}}x^{n}=\sum_{n\geq0}v_{n}x^{n}$. Thus,
$u=\sum_{n\geq0}u_{n}x^{n}=\sum_{n\geq0}v_{n}x^{n}=v$. This proves Lemma
\ref{lem.I1}.
\end{proof}

\begin{lemma}
\label{lem.I2}Let $w\in\mathbf{k}\left[  \left[  x\right]  \right]  $ be an
FPS having constant term $0$. Then,
\begin{equation}
\dfrac{d}{dx}\left(  \overline{\exp}\left[  w\right]  \right)  =\left(
\dfrac{d}{dx}w\right)  \cdot\exp\left[  w\right]
\label{sol.convolution-series.i.2.exp}%
\end{equation}
and%
\begin{equation}
\dfrac{d}{dx}\left(  \overline{\log}\left[  w\right]  \right)  =\left(
\dfrac{d}{dx}w\right)  \cdot\dfrac{1}{1+w}.
\label{sol.convolution-series.i.2.log}%
\end{equation}

\end{lemma}

\begin{proof}
[Proof of Lemma \ref{lem.I2}.]Substituting $w$ for $x$ on both sides of the
equality (\ref{sol.convolution-series.i.expbar=}), we obtain%
\[
\overline{\exp}\left[  w\right]  =\sum_{n\geq1}\dfrac{1}{n!}w^{n}.
\]
Applying the operator $\dfrac{d}{dx}$ to this equality, we find%
\begin{align*}
\dfrac{d}{dx}\overline{\exp}\left[  w\right]   &  =\dfrac{d}{dx}\sum_{n\geq
1}\dfrac{1}{n!}w^{n}=\sum_{n\geq1}\dfrac{1}{n!}\cdot\underbrace{\dfrac{d}%
{dx}\left(  w^{n}\right)  }_{\substack{=n\left(  \dfrac{d}{dx}w\right)
w^{n-1}\\\text{(by Proposition \ref{prop.derivatives.leibniz} \textbf{(d)})}%
}}=\sum_{n\geq1}\underbrace{\dfrac{1}{n!}\cdot n}_{=\dfrac{1}{\left(
n-1\right)  !}}\left(  \dfrac{d}{dx}w\right)  w^{n-1}\\
&  =\sum_{n\geq1}\dfrac{1}{\left(  n-1\right)  !}\left(  \dfrac{d}%
{dx}w\right)  w^{n-1}=\sum_{n\geq0}\dfrac{1}{n!}\left(  \dfrac{d}{dx}w\right)
w^{n}\\
&  \ \ \ \ \ \ \ \ \ \ \left(  \text{here, we have substituted }n\text{ for
}n-1\text{ in the sum}\right)  .
\end{align*}
Comparing this with%
\[
\left(  \dfrac{d}{dx}w\right)  \cdot\underbrace{\exp\left[  w\right]
}_{\substack{=\sum_{n\geq0}\dfrac{1}{n!}w^{n}\\\text{(since }\exp=\sum
_{n\geq0}\dfrac{1}{n!}x^{n}\text{)}}}=\left(  \dfrac{d}{dx}w\right)  \cdot
\sum_{n\geq0}\dfrac{1}{n!}w^{n}=\sum_{n\geq0}\dfrac{1}{n!}\left(  \dfrac
{d}{dx}w\right)  w^{n},
\]
we obtain $\dfrac{d}{dx}\left(  \overline{\exp}\left[  w\right]  \right)
=\left(  \dfrac{d}{dx}w\right)  \cdot\exp\left[  w\right]  $. This proves
(\ref{sol.convolution-series.i.2.exp}).

Substituting $w$ for $x$ on both sides of the equality
(\ref{sol.convolution-series.i.logbar=}), we obtain%
\[
\overline{\log}\left[  w\right]  =\sum_{n\geq1}\dfrac{\left(  -1\right)
^{n-1}}{n}w^{n}.
\]
Applying the operator $\dfrac{d}{dx}$ to this equality, we find%
\begin{align*}
\dfrac{d}{dx}\overline{\log}\left[  w\right]   &  =\dfrac{d}{dx}\sum_{n\geq
1}\dfrac{\left(  -1\right)  ^{n-1}}{n}w^{n}=\sum_{n\geq1}\dfrac{\left(
-1\right)  ^{n-1}}{n}\cdot\underbrace{\dfrac{d}{dx}\left(  w^{n}\right)
}_{\substack{=n\left(  \dfrac{d}{dx}w\right)  w^{n-1}\\\text{(by Proposition
\ref{prop.derivatives.leibniz} \textbf{(d)})}}}\\
&  =\sum_{n\geq1}\dfrac{\left(  -1\right)  ^{n-1}}{n}\cdot n\left(  \dfrac
{d}{dx}w\right)  w^{n-1}\\
&  =\sum_{n\geq1}\left(  -1\right)  ^{n-1}\left(  \dfrac{d}{dx}w\right)
w^{n-1}=\sum_{n\geq0}\left(  -1\right)  ^{n}\left(  \dfrac{d}{dx}w\right)
w^{n}\\
&  \ \ \ \ \ \ \ \ \ \ \left(  \text{here, we have substituted }n\text{ for
}n-1\text{ in the sum}\right)  .
\end{align*}
Comparing this with%
\[
\left(  \dfrac{d}{dx}w\right)  \cdot\underbrace{\dfrac{1}{1+w}}_{=\sum
_{n\geq0}\left(  -1\right)  ^{n}w^{n}}=\left(  \dfrac{d}{dx}w\right)
\cdot\sum_{n\geq0}\left(  -1\right)  ^{n}w^{n}=\sum_{n\geq0}\left(  -1\right)
^{n}\left(  \dfrac{d}{dx}w\right)  w^{n},
\]
we obtain $\dfrac{d}{dx}\left(  \overline{\log}\left[  w\right]  \right)
=\left(  \dfrac{d}{dx}w\right)  \cdot\dfrac{1}{1+w}$. This proves
(\ref{sol.convolution-series.i.2.log}). Thus, Lemma \ref{lem.I2} is proven.
\end{proof}

\begin{lemma}
\label{lem.I3}Let $u\in\mathbf{k}\left[  \left[  x\right]  \right]  $ and
$v\in\mathbf{k}\left[  \left[  x\right]  \right]  $ be two FPSs having
constant term $1$. Assume that $\left(  \dfrac{d}{dx}u\right)  \cdot v=\left(
\dfrac{d}{dx}v\right)  \cdot u$. Then, $u=v$.
\end{lemma}

\begin{proof}
[Proof of Lemma \ref{lem.I3}.]The FPS $v$ has constant term $1$, and thus has
a multiplicative inverse $v^{-1}$. The Leibniz rule (applied to $u$ and
$v^{-1}$) yields%
\begin{align*}
\dfrac{d}{dx}\left(  uv^{-1}\right)   &  =\left(  \dfrac{d}{dx}u\right)
v^{-1}+u\underbrace{\dfrac{d}{dx}\left(  v^{-1}\right)  }_{\substack{=-v^{-2}%
\left(  \dfrac{d}{dx}v\right)  \\\text{(by Proposition
\ref{prop.derivatives.leibniz} \textbf{(e)})}}}=\left(  \dfrac{d}{dx}u\right)
v^{-1}+u\left(  -v^{-2}\left(  \dfrac{d}{dx}v\right)  \right) \\
&  =v^{-2}\underbrace{\left(  \left(  \dfrac{d}{dx}u\right)  \cdot v-\left(
\dfrac{d}{dx}v\right)  \cdot u\right)  }_{\substack{=0\\\text{(since }\left(
\dfrac{d}{dx}u\right)  \cdot v=\left(  \dfrac{d}{dx}v\right)  \cdot u\text{)}%
}}=v^{-2}0=0=\dfrac{d}{dx}1.
\end{align*}
Moreover, the FPSs $uv^{-1}$ and $1$ have the same constant
term\footnote{\textit{Proof.} The FPS $v$ has constant term $1$. Hence, its
inverse $v^{-1}$ has constant term $1^{-1}=1$. Now, both FPSs $u$ and $v^{-1}$
have constant term $1$. Hence, their product $uv^{-1}$ has constant term
$1\cdot1=1$. Since the FPS $1$ also has constant term $1$, this shows that the
FPSs $uv^{-1}$ and $1$ have the same constant term (namely, $1$).}. Hence,
Lemma \ref{lem.I1} (applied to $uv^{-1}$ and $1$ instead of $u$ and $v$) shows
that $uv^{-1}=1$. Thus, $u=v$. This proves Lemma \ref{lem.I3}.
\end{proof}

\begin{proof}
[Proof of Theorem \ref{thm.exp-log-inv}.]The equality
(\ref{sol.convolution-series.i.2.log}) (applied to $w=x$) yields $\dfrac
{d}{dx}\left(  \overline{\log}\left[  x\right]  \right)  =\underbrace{\left(
\dfrac{d}{dx}x\right)  }_{=1}\cdot\dfrac{1}{1+x}=\dfrac{1}{1+x}$. In other
words, $\dfrac{d}{dx}\overline{\log}=\dfrac{1}{1+x}$ (since $\overline{\log
}=\overline{\log}\left[  x\right]  $).

Now, (\ref{sol.convolution-series.i.2.exp}) (applied to $w=\overline{\log}$)
shows that%
\[
\dfrac{d}{dx}\left(  \overline{\exp}\left[  \overline{\log}\right]  \right)
=\underbrace{\left(  \dfrac{d}{dx}\overline{\log}\right)  }_{=\dfrac{1}{1+x}%
}\cdot\exp\left[  \overline{\log}\right]  =\dfrac{1}{1+x}\cdot\exp\left[
\overline{\log}\right]  .
\]


But $\overline{\exp}=\exp-1$ and thus $\exp=\overline{\exp}+1$. Substituting
$\overline{\log}$ for $x$ in this equality, we find $\exp\left[
\overline{\log}\right]  =\overline{\exp}\left[  \overline{\log}\right]  +1$.
Hence,%
\begin{align*}
\dfrac{d}{dx}\left(  \exp\left[  \overline{\log}\right]  \right)   &
=\dfrac{d}{dx}\left(  \overline{\exp}\left[  \overline{\log}\right]
+1\right)  =\dfrac{d}{dx}\overline{\exp}\left[  \overline{\log}\right]
+\underbrace{\dfrac{d}{dx}1}_{=0}\\
&  =\dfrac{d}{dx}\overline{\exp}\left[  \overline{\log}\right]  =\dfrac
{1}{1+x}\cdot\exp\left[  \overline{\log}\right]  .
\end{align*}
Multiplying this equality by $1+x$, we find%
\[
\left(  \dfrac{d}{dx}\left(  \exp\left[  \overline{\log}\right]  \right)
\right)  \cdot\left(  1+x\right)  =\exp\left[  \overline{\log}\right]  .
\]
Comparing this with $\underbrace{\left(  \dfrac{d}{dx}\left(  1+x\right)
\right)  }_{=1}\cdot\exp\left[  \overline{\log}\right]  =\exp\left[
\overline{\log}\right]  $, we find
\[
\left(  \dfrac{d}{dx}\left(  \exp\left[  \overline{\log}\right]  \right)
\right)  \cdot\left(  1+x\right)  =\left(  \dfrac{d}{dx}\left(  1+x\right)
\right)  \cdot\exp\left[  \overline{\log}\right]  .
\]
Since both FPSs $\exp\left[  \overline{\log}\right]  $ and $1+x$ have constant
term $1$\ \ \ \ \footnote{\textit{Proof.} It is clear that the FPS $1+x$ has
constant term $1$. Thus, it remains to prove that the FPS $\exp\left[
\overline{\log}\right]  $ has constant term $1$.
\par
Recall that the FPS $\overline{\exp}\left[  \overline{\log}\right]  $ has
constant term $0$. Hence, the FPS $\overline{\exp}\left[  \overline{\log
}\right]  +1$ has constant term $0+1=1$. In other words, the FPS $\exp\left[
\overline{\log}\right]  $ has constant term $1$ (since $\exp\left[
\overline{\log}\right]  =\overline{\exp}\left[  \overline{\log}\right]  +1$).
Qed.}, we can thus apply Lemma \ref{lem.I3} to $u=\exp\left[  \overline{\log
}\right]  $ and $v=1+x$. We thus conclude that $\exp\left[  \overline{\log
}\right]  =1+x$. Comparing this with $\exp\left[  \overline{\log}\right]
=\overline{\exp}\left[  \overline{\log}\right]  +1$, we obtain $\overline
{\exp}\left[  \overline{\log}\right]  +1=1+x$. Subtracting $1$ from this
equality, we find $\overline{\exp}\left[  \overline{\log}\right]  =x$.

The equality (\ref{sol.convolution-series.i.2.exp}) (applied to $w=x$) yields
$\dfrac{d}{dx}\left(  \overline{\exp}\left[  x\right]  \right)
=\underbrace{\left(  \dfrac{d}{dx}x\right)  }_{=1}\cdot\underbrace{\exp\left[
x\right]  }_{=\exp}=\exp$. In other words, $\dfrac{d}{dx}\overline{\exp}=\exp$
(since $\overline{\exp}=\overline{\exp}\left[  x\right]  $).

On the other hand, (\ref{sol.convolution-series.i.2.log}) (applied to
$w=\overline{\exp}$) shows that%
\[
\dfrac{d}{dx}\left(  \overline{\log}\left[  \overline{\exp}\right]  \right)
=\underbrace{\left(  \dfrac{d}{dx}\overline{\exp}\right)  }_{=\exp
=\overline{\exp}+1=1+\overline{\exp}}\cdot\dfrac{1}{1+\overline{\exp}}=\left(
1+\overline{\exp}\right)  \cdot\dfrac{1}{1+\overline{\exp}}=1=\dfrac{d}{dx}x.
\]
Since the two FPSs $\overline{\log}\left[  \overline{\exp}\right]  $ and $x$
have the same constant term\footnote{This is because the FPS $\overline{\log
}\left[  \overline{\exp}\right]  $ has constant term $0$, and the FPS $x$ also
has constant term $0$.}, we can thus apply Lemma \ref{lem.I1} to
$u=\overline{\log}\left[  \overline{\exp}\right]  $ and $v=x$. We thus
conclude that $\overline{\log}\left[  \overline{\exp}\right]  =x$. The proof
of Theorem \ref{thm.exp-log-inv} is thus complete.
\end{proof}

\begin{thebibliography}{99999999}                                                                                         %


\bibitem[Loehr11]{Loehr-bij}%
\href{http://www.math.vt.edu/people/nloehr/bijbook.html}{Nicholas A. Loehr,
\textit{Bijective Combinatorics}, Chapman \& Hall/CRC 2011.}

\bibitem[GriRei18]{GriRei16}Darij Grinberg, Victor Reiner, \textit{Hopf
algebras in Combinatorics}, version of 11 May 2018,
\arxiv{1409.8356v5}. \newline%
See also \url{http://www.cip.ifi.lmu.de/~grinberg/algebra/HopfComb-sols.pdf} for a version that gets updated.
\end{thebibliography}


\end{document}