A represented measure is positively homogeneous

Proved

Repr.repr_positivelyHomogeneous

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

operations-researchprobability

Scaling a position by a nonnegative factor scales a represented measure by the same factor: the factor passes through each scenario's expectation and then through the maximum, since a nonnegative factor does not reorder the competitors.

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