Prove2Me

AT02 subadditivity of ESαES_\alpha, as used in the proof of PROPOSITION 1(i)

Proved
MixFlex.RiskNeutral.expectedShortfall_subadditive

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

expected-shortfallp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1risk-measures

Let (Ω,F,P)(\Omega,\mathcal F,\mathbb P) be a probability space, Z1,…,ZNZ_1,\dots,Z_N integrable real random variables and α∈(0,1)\alpha\in(0,1). Then the Acerbi–Tasche α\alpha-expected shortfall is subadditive:

ESα(∑n=1NZn)≤∑n=1NESα(Zn).ES_\alpha\Big(\sum_{n=1}^N Z_n\Big)\le\sum_{n=1}^N ES_\alpha(Z_n).

This is the result of Acerbi and Tasche (2002) quoted in the proof of Proposition 1(i); combined with the expected-shortfall form of (A-1) it gives ΔRN≥0\Delta_{RN}\ge 0. It holds for arbitrary integrable random variables, not only demands.

Preamble
import Mathlib
import Definitions.Def_MixFlex_RiskNeutral_Model
Formal statement
namespace MixFlex.RiskNeutral

open MeasureTheory ProbabilityTheory

/-- Subadditivity of expected shortfall (Acerbi–Tasche 2002), as quoted in the proof of
Proposition 1(i), p. 52: `ES_α(Σ_n Z_n) ≤ Σ_n ES_α(Z_n)` for integrable random variables and
`α ∈ (0, 1)`. -/
theorem expectedShortfall_subadditive {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] {N : ℕ} (Z : Fin N → Ω → ℝ) (hmeas : ∀ n, Measurable (Z n))
    (hint : ∀ n, Integrable (Z n) μ) (α : ℝ) (hα0 : 0 < α) (hα1 : α < 1) :
    expectedShortfall μ (fun ω => ∑ n, Z n ω) α ≤ ∑ n, expectedShortfall μ (Z n) α := by sorry

end MixFlex.RiskNeutral
Source
Acerbi and Tasche (2002), as quoted in Tomlin and Wang, On the value of mix flexibility and dual sourcing in unreliable newsvendor networks, Manufacturing Service Oper. Management 7(1), 2005, p. 52, Appendix A, proof of PROPOSITION 1(i)
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