ThmDex – An index of mathematical definitions, results, and conjectures.
F11360
Formulation 0
Let $\exp$ be the D1932: Standard natural real exponential function.
Let $\log$ be the D865: Standard natural real logarithm function.
Let $\tau, x_1, \ldots, x_N \in \mathbb{R}$ each be a D993: Real number.
Then \begin{equation} \log \sum_{n = 1}^N \exp(x_n) = \tau + \log \sum_{n = 1}^N \exp(x_n - \tau) \end{equation}