Eq. (7) — a risk measure is the minimal capital making a position acceptable

Proved

StarShapedRisk.LawInvariant.eq7_rho_isLeast_acceptance

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

acceptance-setsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1risk-measures

Let $\mathcal X$ be the space of bounded measurable losses on $(\Omega,\mathcal F)$ and let $\rho:\mathcal X\to\mathbb R$ be a risk measure with acceptance set $\mathcal A_\rho=\{X\in\mathcal X\mid\rho(X)\le 0\}$ . Then for every $X\in\mathcal X$ the minimum below exists and

\rho(X)=\min\{m\in\mathbb R\mid X-m\in\mathcal A_\rho\}.

The risk of a position is thus the smallest amount by which the loss must be uniformly reduced to make the position acceptable, so $\mathcal A_\rho$ determines $\rho$ . The proof of Theorem 5 starts from this identity.

Formalization Note "min" is stated as an attained minimum (IsLeast): $\rho(X)$ belongs to the set and is a lower bound of it.

Preamble

import Mathlib
import Definitions.Def_StarShapedRisk_LawInvariant_Model

Formal statement

namespace StarShapedRisk.LawInvariant

/-- Castagnoli et al. (2022), Eq. (7) (p. 2642), on the space of bounded measurable positions:
a risk measure is recovered from its acceptance set as an attained minimum,
`ρ X = min {m ∈ ℝ | X - m ∈ A_ρ}`. -/
theorem eq7_rho_isLeast_acceptance {Ω : Type*} [MeasurableSpace Ω]
    (ρ : Positions Ω → ℝ) (hρ : IsRiskMeasure ρ) (X : Positions Ω) :
    IsLeast {m : ℝ | X - const m ∈ acceptanceSetOf ρ} (ρ X) := by sorry

end StarShapedRisk.LawInvariant

Source

Castagnoli, Cattelan, Maccheroni, Tebaldi, Wang, Star-Shaped Risk Measures, Operations Research 70(5) (2022), p. 2642, Eq. (7)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph