Worst-case risk is represented by the point masses

Proved

Repr.worstCase_representedBy

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

operations-researchprobability

The worst-case measure is exactly the representation whose scenarios are the point masses — each individual state taken as certain. Maximising the expected loss over that family picks out the single largest loss, which is what worstCase reports.

This grounds the abstract representation in the most familiar coherent measure, and combined with the constructive half it re-derives the coherence of worstCase from the representation rather than axiom by axiom.

As throughout CoherentRisk, the state space is finite and carries no measure of its own; a scenario is a weighting supplied as data, not derived from a probability space.

Preamble

import Definitions.Def_CoherentRiskRepresentation

open CoherentRisk Repr

Formal statement

namespace Repr

theorem worstCase_representedBy {n : ℕ} :
    ∃ P : Fin (n+1) → (Fin (n+1) → ℝ), RepresentedBy (worstCase (n := n)) P := by
  sorry

end Repr

Source

P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent Measures of Risk, Mathematical Finance 9 (1999) 203-228, Section 3

View graph