In 1999 Artzner, Delbaen, Eber and Heath asked what a risk measure ought to satisfy, wrote down four axioms, and observed that the industry standard of the day -- Value-at-Risk -- fails one of them. The failing axiom is subadditivity: merging two positions should never require more capital than holding them apart. VaR can violate it, so under VaR a diversified book can appear riskier than its parts.
That observation did not stay academic. It is the reason the Basel framework moved its market-risk capital standard from Value-at-Risk to Expected Shortfall. Few results in mathematical finance have had a more direct regulatory consequence, and the mathematics is elementary enough to state completely.
A position is a payoff X : Fin (n+1) -> R across finitely many equally-weighted states, and a
risk measure rho sends it to the capital that must be added to make it acceptable. Following
Definition 2.4 of the paper, rho is coherent when it is translation-invariant, subadditive,
positively homogeneous and monotone. Nonemptiness of the state space is carried in the index type
so the worst case is always attained; no probability measure is needed for these four axioms,
which is faithful to the paper -- Artzner et al. state T, S, PH and M without reference to one.
Value-at-Risk is defined here at an integer tolerance k rather than a probability level, which
keeps the quantile unambiguous on a finite space: VaR X k is the least capital leaving at most
k states in loss, corresponding to level k/(n+1).
The mission's goal theorem is the negative result: Value-at-Risk is not subadditive. A witness
is 25 equiprobable states with X losing 100 in state 0 alone and Y losing 100 in state 1
alone. Each has one losing state in twenty-five, so at tolerance k = 1 both have VaR = 0;
their sum loses in two states, exceeding the tolerance, so VaR (X+Y) 1 = 100 > 0 + 0. The
witness was checked numerically before this mission was drafted; what is open is the Lean proof.
The milestones establish the positive contrast on the same footing: worst-case risk, the most conservative measure, satisfies all four axioms, so the failure is specific to VaR rather than inherent to risk measurement.
P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent Measures of Risk, Mathematical Finance 9 (1999) 203-228. Axioms T, S, PH and M are Definition 2.4; the failure of subadditivity for VaR and the diversification consequence are discussed in Section 3.
namespace CoherentRisk
theorem var_not_subadditive :
¬ (∀ (m : ℕ) (k : ℕ), Subadditive (fun X : Fin (m+1) → ℝ => VaR X k)) := by
sorry
end CoherentRiskValue-at-Risk violates subadditivity: there are positions whose combined VaR exceeds the sum of their individual VaRs, so under VaR the pooling of positions can appear to increase risk. A witness on 25 states: X loses 100 in state 0 alone and Y loses 100 in state 1 alone, each a single losing state in twenty-five, so at tolerance k=1 both have VaR 0; their sum loses in two states, exceeding the tolerance, giving VaR 100. Note that VaR here counts STATES and refers to no probability measure, per its own definition -- the state count 25 is not load-bearing (two states suffice) and reading k=1 as a 4% tail is an interpretation the formal statement does not make. This is the failure that moved the Basel market-risk standard from Value-at-Risk to Expected Shortfall.
No open leaves. Every sub-goal is proved or awaiting decomposition.