Prove2Me

Theorem 1 (supremum) — the supremum of star-shaped risk measures is a star-shaped risk measure

Proved
StarShapedRisk.Representation.theorem1_supremum

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

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

Let {ρi}i∈I\{\rho_i\}_{i\in I} be a nonempty collection of star-shaped risk measures on a space X\mathcal X of bounded positions containing the constants. Then the supremum

ρ∨(X)=sup⁡i∈Iρi(X),X∈X,\rho_\vee(X)=\sup_{i\in I}\rho_i(X),\qquad X\in\mathcal X,

is a star-shaped risk measure.

Together with the infimum part, this shows that star-shaped risk measures form a complete lattice under pointwise operations, and it covers robustifications such as the worst case over a set of scenarios.

Formalization Note The index set is assumed nonempty. The supremum is Lean's ⨆ in R\mathbb R, which is the true supremum because the family {ρi(X)}\{\rho_i(X)\} is bounded by sup⁡ω∣X(ω)∣\sup_\omega|X(\omega)|.

Preamble
import Mathlib
import Definitions.Def_StarShapedRisk_Representation_RiskMeasure
import Definitions.Def_StarShapedRisk_Representation_Aggregation
Formal statement
namespace StarShapedRisk.Representation
theorem theorem1_supremum {Ω : Type*} (𝒳 : PositionSpace Ω) {I : Type*} [Nonempty I]
    (ρ : I → 𝒳.carrier → ℝ) (hρ : ∀ i, IsStarShapedRiskMeasure 𝒳 (ρ i)) :
    IsStarShapedRiskMeasure 𝒳 (riskSup 𝒳 ρ) := by sorry
end StarShapedRisk.Representation
Source
Castagnoli, Cattelan, Maccheroni, Tebaldi, Wang, Star-Shaped Risk Measures, Operations Research 70(5) (2022), p. 2643, Theorem 1 (supremum)
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