Adding a certain amount shifts the worst total by $(m+1)c$

Proved

CoherentRisk.worstTotal_translation

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

operations-researchprobability

Adding a certain amount $c$ in every state lowers the worst-total loss by exactly $(m+1)c$ . Every set competing for the maximum has exactly $m+1$ members, so each competitor's total is shifted by the same constant $(m+1)c$ ; a uniform shift of every competitor shifts their maximum by that amount and does not change which set attains it.

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_translation {n : ℕ} (m : Fin (n+1)) (X : Fin (n+1) → ℝ) (c : ℝ) :
    worstTotal (fun i => X i + c) m
      = worstTotal X m - (((m : ℕ) + 1 : ℕ) : ℝ) * c := 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

Adding a certain amount shifts the worst total by (m+1)c(m+1)c(m+1)c

Adding a certain amount shifts the worst total by $(m+1)c$