Worst-case risk is subadditive
ProvedCoherentRisk.worstCase_subadditiveprobability
Merging two positions never requires more capital under the worst-case measure than holding them separately: the worst outcome of a sum is at least the sum of the worst outcomes. This is the axiom Value-at-Risk fails, stated here for the measure that satisfies it.
Preamble
import Definitions.Def_CoherentRisk open CoherentRisk
Formal statement
namespace CoherentRisk
theorem worstCase_subadditive {n : ℕ} : Subadditive (worstCase (n := n)) := by
sorry
end CoherentRiskSource
Artzner et al. 1999, axiom S applied to the worst-case measure.
Human review
Confirmed by the mission captain (proposal self-audit).