A represented measure is translation invariant

Proved

Repr.repr_translationInvariant

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

operations-researchprobability

Adding a certain amount $c$ in every state lowers a represented measure by exactly $c$ . This is where the requirement that each scenario's weights sum to one does its work: the constant contributes $c$ times that sum to every scenario, shifting all of them equally, and a uniform shift of every competitor shifts their maximum by the same amount.

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