A uniformly better position has a smaller worst total

Proved

CoherentRisk.worstTotal_antitone

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

operations-researchprobability

If $Y$ pays at least as much as $X$ in every state, then the worst-total loss of $Y$ is at most that of $X$ . Each competing set of states has a larger total payoff under $Y$ , hence a smaller total loss, and the inequality survives taking the maximum.

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 worstTotal_antitone {n : ℕ} (m : Fin (n+1)) (X Y : Fin (n+1) → ℝ)
    (h : ∀ i, X i ≤ Y i) : worstTotal Y m ≤ worstTotal 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