Prove2Me

Proposition 3 — for subadditive risk measures, star-shaped ⇔ positively homogeneous ⇔ convex

Proved
StarShapedRisk.Representation.proposition3_subadditive_star_shaped_iff

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

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

Let ρ:X→R\rho:\mathcal X\to\mathbb R be a subadditive risk measure on a space X\mathcal X of bounded positions containing the constants: ρ(X+Y)≤ρ(X)+ρ(Y)\rho(X+Y)\le\rho(X)+\rho(Y) for all X,YX,Y. The following are equivalent:

  1. ρ\rho is star-shaped;
  2. ρ\rho is positively homogeneous (thus coherent);
  3. ρ\rho is convex.

Hence coherent risk measures are exactly the subadditive star-shaped ones, and positive homogeneity in the definition of coherence can be weakened to star-shapedness.

Preamble
import Mathlib
import Definitions.Def_StarShapedRisk_Representation_RiskMeasure
Formal statement
namespace StarShapedRisk.Representation
theorem proposition3_subadditive_star_shaped_iff {Ω : Type*} (𝒳 : PositionSpace Ω)
    (ρ : 𝒳.carrier → ℝ) (hρ : IsRiskMeasure 𝒳 ρ) (hsub : IsSubadditive 𝒳 ρ) :
    List.TFAE [IsStarShaped 𝒳 ρ, IsPositivelyHomogeneous 𝒳 ρ, IsConvex 𝒳 ρ] := by sorry
end StarShapedRisk.Representation
Source
Castagnoli, Cattelan, Maccheroni, Tebaldi, Wang, Star-Shaped Risk Measures, Operations Research 70(5) (2022), p. 2642, Proposition 3
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