Prove2Me

Expected Shortfall is monotone

Proved
CoherentRisk.es_monotone

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

operations-researchprobability

Expected Shortfall satisfies the monotonicity axiom: a position that pays at least as much in every state is at most as risky.

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

Preamble
import Definitions.Def_ExpectedShortfall

open CoherentRisk
Formal statement
namespace CoherentRisk

theorem es_monotone {n : ℕ} (m : Fin (n+1)) :
    Monotone' (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