Let $\exp$ be the D1932: Standard natural real exponential function.
Let $\log$ be the D865: Standard natural real logarithm function.
Let $x_1, \ldots, x_N \in \mathbb{R}$ each be a D993: Real number such that
Let $\log$ be the D865: Standard natural real logarithm function.
Let $x_1, \ldots, x_N \in \mathbb{R}$ each be a D993: Real number such that
| (i) | \begin{equation} \tau : = \max(x_1, \ldots, x_N) \end{equation} |
Then
\begin{equation}
\log \sum_{n = 1}^N \exp(x_n)
= \tau + \log \sum_{n = 1}^N \exp(x_n - \tau)
\end{equation}