CoherentRisk
Definitionoperations-researchprobability
The four Artzner-Delbaen-Eber-Heath axioms for a risk measure on a finite state space -- translation invariance, subadditivity, positive homogeneity, monotonicity -- with coherence as their conjunction; the worst-case measure (minus the worst outcome); and Value-at-Risk at an integer tolerance k, the least capital leaving at most k states in strict loss. Note that VaR here counts STATES, not probability: no measure or weighting is asserted, so reading k as a probability level requires an equiprobability assumption the code does not make. VaR degenerates to the constant 0 for every payoff when k >= n+1, and coincides exactly with the worst-case measure at k = 0.
Definition code
import Mathlib
/-!
Coherent risk measures on a finite outcome space.
Source: P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, *Coherent Measures of Risk*,
Mathematical Finance **9** (1999) 203-228, Definition 2.4 (axioms T, S, PH, M).
A risk measure assigns to a position -- a payoff `X` across finitely many states of the world --
a real number read as the capital that must be added to make the position acceptable. Artzner
et al. single out four axioms, and a measure satisfying all four is called COHERENT. Their
paper's practical consequence is that Value-at-Risk fails the fourth (subadditivity), so
diversification can appear to increase VaR, while worst-case and expected-shortfall measures
do not fail it.
We work on `Fin (n+1) -> R`, i.e. a nonempty finite state space with payoffs in the reals.
Nonemptiness is built into the index type so that 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 a probability.
-/
namespace CoherentRisk
variable {n : ℕ}
/-- **Translation invariance** (Artzner et al., axiom T): adding a certain amount `c` of the
numeraire to every state reduces the required capital by exactly `c`. -/
def TranslationInvariant (rho : (Fin (n+1) → ℝ) → ℝ) : Prop :=
∀ (X : Fin (n+1) → ℝ) (c : ℝ), rho (fun i => X i + c) = rho X - c
/-- **Subadditivity** (axiom S): merging two positions cannot require more capital than
holding them separately. This is the axiom Value-at-Risk violates. -/
def Subadditive (rho : (Fin (n+1) → ℝ) → ℝ) : Prop :=
∀ X Y : Fin (n+1) → ℝ, rho (fun i => X i + Y i) ≤ rho X + rho Y
/-- **Positive homogeneity** (axiom PH): scaling a position scales its risk. -/
def PositivelyHomogeneous (rho : (Fin (n+1) → ℝ) → ℝ) : Prop :=
∀ (lam : ℝ), 0 ≤ lam → ∀ X : Fin (n+1) → ℝ, rho (fun i => lam * X i) = lam * rho X
/-- **Monotonicity** (axiom M): a position that pays at least as much in every state is at
most as risky. -/
def Monotone' (rho : (Fin (n+1) → ℝ) → ℝ) : Prop :=
∀ X Y : Fin (n+1) → ℝ, (∀ i, X i ≤ Y i) → rho Y ≤ rho X
/-- A risk measure is **coherent** when it satisfies all four axioms. -/
def Coherent (rho : (Fin (n+1) → ℝ) → ℝ) : Prop :=
TranslationInvariant rho ∧ Subadditive rho ∧ PositivelyHomogeneous rho ∧ Monotone' rho
/-- **Worst-case risk**: minus the worst outcome across the states. The canonical coherent
measure, and the most conservative one. -/
noncomputable def worstCase (X : Fin (n+1) → ℝ) : ℝ :=
-(Finset.univ.inf' Finset.univ_nonempty X)
/-- **Value-at-Risk** at integer tolerance `k`: the least capital `v` such that at most `k`
states remain in strict loss after adding it.
WHAT THIS DOES AND DOES NOT ASSERT. The definition counts STATES, not probability. It refers to
no measure and no weighting, so reading `k` as the level `k/(n+1)` is an interpretation the code
does not make -- it is only correct if the reader supplies the assumption that the states are
equally likely. That assumption is not needed for the axioms, and is not stated here.
DEGENERATE REGIME. `sInf` on the reals returns `0` for a set that is empty or unbounded below.
The set here is never empty, since large enough `v` always clears every state. But it is the
whole line exactly when `k >= n+1`: the in-loss count can never exceed the `n+1` states, so the
constraint holds for every `v` and `VaR X k = 0` IDENTICALLY, for every payoff. That regime
carries no information about `X` and any statement about `VaR` must exclude it or be read as
vacuous there. For `k <= n` the infimum is attained and genuinely depends on `X`.
At `k = 0` this coincides exactly with `worstCase`. -/
noncomputable def VaR (X : Fin (n+1) → ℝ) (k : ℕ) : ℝ :=
sInf {v : ℝ | (Finset.univ.filter (fun i => X i + v < 0)).card ≤ k}
end CoherentRisk
Source
Artzner, Delbaen, Eber & Heath, Coherent Measures of Risk, Mathematical Finance 9 (1999) 203-228, Definition 2.4.
Human review
Confirmed by the mission captain (proposal self-audit).