ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4871 on D5754: Standard real log-sum-exp function
Translation property of the standard real log-sum-exp function
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}
Subresults
▶ R5141: Real log-sum-exp method
Proofs
Proof 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.
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$