A represented measure is subadditive

Proved

Repr.repr_subadditive

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

operations-researchprobability

A risk measure given as a greatest expected loss over a family of scenarios is subadditive. The reason is structural: it is a maximum of linear functionals, and the scenario that is worst for the merged position is available to each part separately, but neither part need choose it.

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 repr_subadditive {n : ℕ} {ι : Type} [Fintype ι] [Nonempty ι]
    {rho : (Fin (n+1) → ℝ) → ℝ} {P : ι → (Fin (n+1) → ℝ)}
    (h : RepresentedBy rho P) : Subadditive rho := 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