Prove2Me

Expected Shortfall is positively homogeneous

Proved
CoherentRisk.es_positivelyHomogeneous

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

operations-researchprobability

Expected Shortfall satisfies the positive-homogeneity axiom: scaling a position by a nonnegative factor scales its risk by the same factor. Doubling a position doubles the capital it requires.

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