Proposition 1 — star-shapedness via deleveraging and increasing risk-to-exposure ratios

Proved

StarShapedRisk.Representation.proposition1_star_shaped_iff

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

p2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1risk-measuresstar-shaped-risk-measures

Let $\rho:\mathcal X\to\mathbb R$ be a risk measure (monotone, translation invariant, normalized) on a space $\mathcal X$ of bounded positions containing the constants. The following are equivalent:

$\rho$ is star-shaped: $\rho(\lambda X)\ge\lambda\rho(X)$ for all $X\in\mathcal X$ and $\lambda>1$ ;
$\rho(\alpha X)\le\alpha\rho(X)$ for all $X\in\mathcal X$ and all $\alpha\in(0,1)$ ;
for each $X\in\mathcal X$ , the risk-to-exposure ratio

r_X:\beta\mapsto\frac{\rho(\beta X)}{\beta}

is an increasing (non-decreasing) function of $\beta$ on $(0,\infty)$ .

The equivalence explains the names "increasing along rays" and "radiant" and is the elementary tool behind the later characterizations.

Formalization Note "Increasing" is weak monotonicity (MonotoneOn on $(0,\infty)$ ).

Preamble

import Mathlib
import Definitions.Def_StarShapedRisk_Representation_RiskMeasure

Formal statement

namespace StarShapedRisk.Representation
theorem proposition1_star_shaped_iff {Ω : Type*} (𝒳 : PositionSpace Ω) (ρ : 𝒳.carrier → ℝ)
    (hρ : IsRiskMeasure 𝒳 ρ) :
    List.TFAE
      [IsStarShaped 𝒳 ρ,
       ∀ (X : 𝒳.carrier) (α : ℝ), 0 < α → α < 1 → ρ (α • X) ≤ α * ρ X,
       ∀ X : 𝒳.carrier, MonotoneOn (fun β : ℝ => ρ (β • X) / β) (Set.Ioi 0)] := by sorry
end StarShapedRisk.Representation

Source

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

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