A represented measure is monotone

Proved

Repr.repr_monotone

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

operations-researchprobability

A position paying at least as much in every state is at most as risky under a represented measure. This is where nonnegativity of the weights is used: it is what makes each scenario's expectation order-preserving, and the ordering then survives the maximum.

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