Prove2Me

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

Proved
StarShapedRisk.Representation.theorem1_infimum

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 infimum

ρ∧(X)=inf⁡i∈Iρi(X),X∈X,\rho_\wedge(X)=\inf_{i\in I}\rho_i(X),\qquad X\in\mathcal X,

is a star-shaped risk measure.

This is the part of Theorem 1 that shows a minimum of convex risk measures is star-shaped, one direction of the representation theorem.

Formalization Note The index set is assumed nonempty (an empty collection has no real infimum). The infimum is Lean's ⨅ in R\mathbb R; since inf⁡ωX(ω)≤ρi(X)≤sup⁡ωX(ω)\inf_\omega X(\omega)\le\rho_i(X)\le\sup_\omega X(\omega) for every risk measure, the family is bounded and the value is the true infimum.

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