Exponential concentration of a weighted mean (source code)

= Exponential concentration of a weighted mean
{title2=$\displaystyle\lim_{\tau\downarrow0}\frac{\sum_j a_je^{a_j/\tau}}{\sum_je^{a_j/\tau}}=\max_j a_j$}

For finitely many real numbers $a_1,\ldots,a_m$, let $M=\max_ja_j$. Divide numerator and denominator of their exponentially weighted mean by $e^{M/\tau}$. Every term with $a_j<M$ vanishes as $\tau\downarrow0$, while each maximizer contributes $M$ to the numerator and one to the denominator. Their quotient therefore tends to $M$, even when the maximum is negative or attained more than once. The finiteness of the list is used to pass the <limit> through each sum.