Representation of a risk measure over generalized scenarios
DefinitionCoherentRiskRepresentationThe representation apparatus of Artzner, Delbaen, Eber and Heath, on a finite state space.
A scenario is a probability weight vector on the states: nonnegative entries summing to one. Given a family of scenarios indexed by a nonempty finite type, the worst-scenario value of a payoff is
the greatest expected loss over the family. A risk measure is represented by that family when its value is exactly this maximum.
This is the shape of the central theorem of Artzner et al.: a coherent measure is a worst case over a family of generalized scenarios. Writing it as a maximum of linear functionals is what makes the four axioms transparent — subadditivity and positive homogeneity come from the maximum-of-linear form, translation invariance from the weights summing to one, and monotonicity from their nonnegativity.
What this does and does not assert. The weights are supplied explicitly as data; nothing here constructs them from a measure-theoretic probability space, and no -algebra is involved. As elsewhere in CoherentRisk, the state space is finite and carries no measure of its own — a scenario is a weighting the reader provides, not one the development derives. The maximum is over a nonempty finite family, so it is genuinely attained rather than a junk value.
import Definitions.Def_CoherentRisk
open CoherentRisk
namespace Repr
variable {n : ℕ} {ι : Type} [Fintype ι] [Nonempty ι]
/-- The greatest expected loss over a family of probability weight vectors. -/
noncomputable def worstScenario (P : ι → (Fin (n+1) → ℝ)) (X : Fin (n+1) → ℝ) : ℝ :=
Finset.univ.sup' Finset.univ_nonempty (fun k => ∑ i, P k i * (-X i))
lemma le_worstScenario (P : ι → (Fin (n+1) → ℝ)) (X : Fin (n+1) → ℝ) (k : ι) :
(∑ i, P k i * (-X i)) ≤ worstScenario P X := by
unfold worstScenario
exact Finset.le_sup' (fun k => ∑ i, P k i * (-X i)) (Finset.mem_univ k)
lemma worstScenario_le {P : ι → (Fin (n+1) → ℝ)} {X : Fin (n+1) → ℝ} {b : ℝ}
(hb : ∀ k, (∑ i, P k i * (-X i)) ≤ b) : worstScenario P X ≤ b :=
Finset.sup'_le _ _ (fun k _ => hb k)
lemma exists_worstScenario (P : ι → (Fin (n+1) → ℝ)) (X : Fin (n+1) → ℝ) :
∃ k, worstScenario P X = ∑ i, P k i * (-X i) := by
obtain ⟨k, _, hk⟩ := Finset.exists_mem_eq_sup' (Finset.univ_nonempty (α := ι))
(fun k => ∑ i, P k i * (-X i))
exact ⟨k, hk⟩
/-- `rho` is **represented** by a family of probability weight vectors: its value is the greatest
expected loss over the family. This is the shape of the Artzner representation — a coherent
measure as a worst case over generalized scenarios. -/
def RepresentedBy (rho : (Fin (n+1) → ℝ) → ℝ) (P : ι → (Fin (n+1) → ℝ)) : Prop :=
(∀ k i, 0 ≤ P k i) ∧ (∀ k, ∑ i, P k i = 1) ∧ ∀ X, rho X = worstScenario P X
end Repr