Expected Shortfall is decreasing in the depth

Expected Shortfall is antitone in the depth: widening the tail reports less risk. Formally, if $a \le b$ then $\mathrm{ES}(X,b) \le \mathrm{ES}(X,a)$.

This is the monotonicity that the ExpectedShortfall definition asserts informally in its docstring. It is proved here by induction on the gap between the two depths, each single step being the un-normalised one-step inequality: dividing that inequality by the product of the two group sizes, both positive, turns it into the comparison of averages.

Combined with the fact that Expected Shortfall at depth $0$ is the worst-case measure, it identifies depth $0$ as the maximum of the entire family and recovers the earlier bound $\mathrm{ES}(X,m) \le \mathrm{worstCase}(X)$ as the special case $a = 0$.

As throughout CoherentRisk, the development counts states and refers to no probability measure, so the depth is an integer count rather than a confidence level.