Worst-case risk is coherent
ProvedCoherentRisk.worstCase_coherentoperations-researchprobability
The worst-case measure, which charges minus the worst outcome across the states, satisfies all four axioms: it is translation-invariant, subadditive, positively homogeneous and monotone. It is the canonical coherent measure and the most conservative one, and it establishes that the axioms are jointly satisfiable.
Preamble
import Definitions.Def_CoherentRisk open CoherentRisk
Formal statement
namespace CoherentRisk
theorem worstCase_coherent {n : ℕ} : Coherent (worstCase (n := n)) := by
sorry
end CoherentRiskSource
Artzner et al. 1999, Definition 2.4 and the discussion of the worst-case (SPAN-style) measure.
Human review
Confirmed by the mission captain (proposal self-audit).