Theorem 1 (average) — the $\mu$-average of star-shaped risk measures is a star-shaped risk measure

Let $\{\rho_i\}_{i\in I}$ be a collection of star-shaped risk measures on a space $\mathcal X$ of bounded positions containing the constants, and let $\mu$ be a probability measure on the set of all subsets of $I$. Then the average

is a star-shaped risk measure. In particular, every convex combination $\sum_i c_i\rho_i$ of finitely many star-shaped risk measures is one.

Averaging risk assessments across models or experts therefore preserves star-shapedness.

Formalization Note The σ-algebra on $I$ is the power set (hypothesis ‹MeasurableSpace I› = ⊤) and $\mu$ is a countably additive probability measure; the integral is Lean's Bochner integral. Every map $i\mapsto\rho_i(X)$ is then measurable and bounded (by $\sup_\omega|X(\omega)|$), hence integrable, so the integral is never the junk value of a non-integrable function.