Expected Shortfall is translation invariant

Proved

CoherentRisk.es_translationInvariant

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

operations-researchprobability

Expected Shortfall satisfies the translation axiom: adding a certain amount $c$ of the numeraire in every state reduces the required capital by exactly $c$ . The worst total shifts by $(m+1)c$ , and dividing by $m+1$ turns that into a shift of exactly $c$ -- which is why the averaging normalisation is the right one.

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_translationInvariant {n : ℕ} (m : Fin (n+1)) :
    TranslationInvariant (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