The maximising group really consists of worst states
ProvedCoherentRisk.worstTotal_extremalThe worst total is attained at some group of exactly states with the property that every state inside the group pays at most what every state outside it pays. In other words the maximising group really is a group of worst states.
This supplies the bridge between the definition and its intended reading. worstTotal is defined as a maximum over all groups of states, and the coherence proofs never need to know which group attains that maximum — which is precisely why they are short. But the interpretation of Expected Shortfall as an average over the worst states does need it, and without this theorem that reading is an assertion rather than a consequence.
The argument is an exchange: if some state inside the maximising group paid strictly more than some state left outside, then swapping the two would lower the group's total payoff and hence raise its total loss, contradicting maximality. Note the statement is an existence claim: ties are possible, so it does not assert that every maximising group has this property, only that one does.
As throughout CoherentRisk, the development counts states and refers to no probability measure, so is an integer depth rather than a confidence level.
import Definitions.Def_ExpectedShortfall open CoherentRisk
namespace CoherentRisk
theorem worstTotal_extremal {n : ℕ} (m : Fin (n+1)) (X : Fin (n+1) → ℝ) :
∃ S : Finset (Fin (n+1)), S.card = (m : ℕ) + 1 ∧
worstTotal X m = -(∑ i ∈ S, X i) ∧
∀ i ∈ S, ∀ j, j ∉ S → X i ≤ X j := by
sorry
end CoherentRisk