A tile whose scores are all at most u has softmax mass at most n·eᵘ

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$, $\htmlData{mx=5}{s : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ and $\htmlData{mx=1}{u \in \htmlData{mx=0}{\mathbb{R}}}$, if $\htmlData{mx=5}{\forall j,\ \htmlData{mx=2}{\htmlData{mx=0}{s}(\htmlData{mx=1}{j})} \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{u}}$, then