The worst-total loss is subadditive
ProvedCoherentRisk.worstTotal_subadditiveoperations-researchprobability
The worst-total loss over any states is subadditive: the worst total of a merged position never exceeds the sum of the worst totals of its parts. The reason is structural rather than computational. The functional is a maximum of linear functionals, one for each admissible set of states, and a maximum of linear functionals is always subadditive: the single set of states that realises the worst total for is available to and to separately, but neither is obliged to choose it, so each may only do better.
As throughout CoherentRisk, the development counts states and refers to no probability measure, so no confidence level is attached to .
Preamble
import Definitions.Def_ExpectedShortfall open CoherentRisk
Formal statement
namespace CoherentRisk
theorem worstTotal_subadditive {n : ℕ} (m : Fin (n+1)) (X Y : Fin (n+1) → ℝ) :
worstTotal (fun i => X i + Y i) m ≤ worstTotal X m + worstTotal Y m := by
sorry
end CoherentRiskSource
C. Acerbi and D. Tasche, On the coherence of expected shortfall, Journal of Banking and Finance 26 (2002) 1487-1503, Section 3; P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent Measures of Risk, Mathematical Finance 9 (1999) 203-228, Definition 2.4