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

Proved

StarShapedRisk.Representation.eq7_min_acceptance

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

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

Let $\rho:\mathcal X\to\mathbb R$ be a risk measure on a space $\mathcal X$ of bounded positions containing the constants, and $\mathcal A_\rho=\{X\mid\rho(X)\le0\}$ its acceptance set. Then for every $X\in\mathcal X$ the minimum below is attained and

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

In words, the risk of $X$ is the least amount by which the loss must be uniformly reduced to make the position acceptable; in particular $\mathcal A_\rho$ determines $\rho$ .

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

Preamble

import Mathlib
import Definitions.Def_StarShapedRisk_Representation_RiskMeasure
import Definitions.Def_StarShapedRisk_Representation_AcceptanceSet

Formal statement

namespace StarShapedRisk.Representation
theorem eq7_min_acceptance {Ω : Type*} (𝒳 : PositionSpace Ω) (ρ : 𝒳.carrier → ℝ)
    (hρ : IsRiskMeasure 𝒳 ρ) (X : 𝒳.carrier) :
    IsLeast {m : ℝ | X - 𝒳.const m ∈ acceptanceSet 𝒳 ρ} (ρ X) := by sorry
end StarShapedRisk.Representation

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