Expected Shortfall is subadditive

Proved

CoherentRisk.es_subadditive

by viratkota · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

operations-researchprobability

Expected Shortfall satisfies the subadditivity axiom: merging two positions never requires more capital than holding them separately. This is precisely the axiom that Value-at-Risk violates, and it is the reason Expected Shortfall replaced it in the Basel market-risk framework. It follows from subadditivity of the worst total by dividing through by the positive constant $m+1$ .

As throughout CoherentRisk, the development counts states and refers to no probability measure, so no confidence level is attached to $m$ .

Preamble

import Definitions.Def_ExpectedShortfall

open CoherentRisk

Formal statement

namespace CoherentRisk

theorem es_subadditive {n : ℕ} (m : Fin (n+1)) :
    Subadditive (fun X : Fin (n+1) → ℝ => ES X m) := by
  sorry

end CoherentRisk

Source

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

View graph