Expected Shortfall is coherent
ProvedCoherentRisk.es_coherentoperations-researchprobability
Expected Shortfall is a coherent measure of risk: it satisfies all four axioms of Artzner, Delbaen, Eber and Heath -- translation invariance, subadditivity, positive homogeneity and monotonicity. This is the positive counterpart to the failure of Value-at-Risk, which satisfies the other three but violates subadditivity. Together the two results are the formal content of the regulatory shift from Value-at-Risk to Expected Shortfall: one can average over a tail of bad states and retain coherence, but one cannot merely count them.
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 es_coherent {n : ℕ} (m : Fin (n+1)) :
Coherent (fun X : Fin (n+1) → ℝ => ES X 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