Expected Shortfall on a finite state space
DefinitionExpectedShortfallExpected Shortfall built on the coherence axioms of CoherentRisk.
For a payoff across states and a depth (itself an index of those states, so that never exceeds ), the worst-total loss is
the greatest total loss borne by any set of exactly states, and Expected Shortfall is its average,
Writing the functional as a maximum over subsets is the Acerbi-Tasche representation, and it is what makes coherence transparent: it exhibits Expected Shortfall as a maximum of linear functionals, and such a maximum is automatically subadditive. At the definition reduces to the worst single state.
What this does and does not assert. As in CoherentRisk, the development COUNTS STATES and refers to no probability measure and no weighting. Classical Expected Shortfall is a conditional expectation over a tail of a distribution; the functional here is the average loss over the worst of the states. The two agree exactly when the states carry the uniform measure, and that identification is an assumption the reader supplies rather than one this file makes. Accordingly no confidence level is attached to : it is an integer depth, not a tail probability. The nonemptiness lemma is included because it is what makes the maximum genuinely attained rather than a junk value.
import Definitions.Def_CoherentRisk
/-!
Expected Shortfall on a finite state space, built on the axioms of `Def_CoherentRisk`.
Source: C. Acerbi and D. Tasche, *On the coherence of expected shortfall*, Journal of Banking
and Finance **26** (2002) 1487-1503; and P. Artzner, F. Delbaen, J.-M. Eber and D. Heath,
*Coherent Measures of Risk*, Mathematical Finance **9** (1999) 203-228.
WHAT THIS DOES AND DOES NOT ASSERT. As in `Def_CoherentRisk`, the development COUNTS STATES.
It refers to no probability measure and no weighting. The classical Expected Shortfall is a
conditional expectation over a tail of a distribution; the functional here is the average loss
over the worst `m+1` of the `n+1` states, and the two agree exactly when the states are given
the uniform measure. That identification is an assumption the reader supplies, not one this
file makes, so no confidence level is attached to `m` anywhere below.
-/
namespace CoherentRisk
variable {n : ℕ}
/-- There is always at least one set of `m+1` states to choose, because `m` indexes the `n+1`
states and so `m+1` never exceeds `n+1`. This is what makes the supremum below attained
rather than a junk value. -/
lemma powersetCard_univ_nonempty (m : Fin (n+1)) :
(Finset.powersetCard ((m : ℕ) + 1) (Finset.univ : Finset (Fin (n+1)))).Nonempty := by
rw [Finset.powersetCard_nonempty]
simpa using Nat.succ_le_of_lt m.isLt
/-- **Worst-total loss** over any `m+1` states: the greatest total loss borne by a set of
exactly `m+1` states. Written as a maximum over subsets, which is the Acerbi-Tasche
representation and is what makes coherence transparent -- it exhibits the functional as a
maximum of linear functionals. -/
noncomputable def worstTotal (X : Fin (n+1) → ℝ) (m : Fin (n+1)) : ℝ :=
(Finset.powersetCard ((m : ℕ) + 1) Finset.univ).sup' (powersetCard_univ_nonempty m)
(fun S => -(∑ i ∈ S, X i))
/-- **Expected Shortfall** at integer depth `m`: the average loss across the worst `m+1`
states. At `m = 0` it is the worst single state, i.e. `worstCase`; as `m` grows it averages
over a wider tail and so reports less risk. -/
noncomputable def ES (X : Fin (n+1) → ℝ) (m : Fin (n+1)) : ℝ :=
worstTotal X m / (((m : ℕ) + 1 : ℕ) : ℝ)
end CoherentRisk