ThmDex – An index of mathematical definitions, results, and conjectures.
P3336
Using results
(i) R4872: Homomorphism property of the standard natural real exponential function in the binary case
(ii) R3711: Homomorphism property of the standard natural logarithm for binary multiplication

we have \begin{equation} \begin{split} \log \sum_{n = 1}^N \exp(x_n) & = \log \left( \exp(\tau) \sum_{n = 1}^N \exp(x_n) \exp(- \tau) \right) \\ & = \log \exp(\tau) + \log \sum_{n = 1}^N \exp(x_n) \exp(- \tau) \\ & = \tau + \log \sum_{n = 1}^N \exp(x_n - \tau) \end{split} \end{equation} $\square$