AT02 Prop. 3.1(iii)–(iv): $ES_\alpha(aX+b)=aES_\alpha(X)-b$ , as used in the proof of PROPOSITION 1(iii)

Proved

MixFlex.RiskNeutral.expectedShortfall_affine

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

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

Let $Z$ be an integrable random variable on a probability space, $a>0$ , $b\in\mathbb R$ and $\alpha\in(0,1)$ . Then the Acerbi–Tasche $\alpha$ -expected shortfall satisfies

ES_\alpha(aZ+b)=a\,ES_\alpha(Z)-b.

This combines positive homogeneity and translation invariance of expected shortfall (Acerbi and Tasche 2002, Proposition 3.1(iii) and (iv)); the proof of Proposition 1(iii) uses it to show that expected shortfall is additive on perfectly positively correlated demands.

Preamble

import Mathlib
import Definitions.Def_MixFlex_RiskNeutral_Model

Formal statement

namespace MixFlex.RiskNeutral

open MeasureTheory ProbabilityTheory

/-- Positive homogeneity and translation invariance of expected shortfall (Acerbi–Tasche 2002,
Proposition 3.1(iii)–(iv)), as quoted in the proof of Proposition 1(iii), p. 52:
`ES_α(aZ + b) = a ES_α(Z) − b` for `a > 0`. -/
theorem expectedShortfall_affine {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] (Z : Ω → ℝ) (hmeas : Measurable Z) (hint : Integrable Z μ)
    (a b : ℝ) (ha : 0 < a) (α : ℝ) (hα0 : 0 < α) (hα1 : α < 1) :
    expectedShortfall μ (fun ω => a * Z ω + b) α = a * expectedShortfall μ Z α - b := by sorry

end MixFlex.RiskNeutral

Source

Acerbi and Tasche (2002), Proposition 3.1(iii)–(iv), 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(iii)

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

AT02 Prop. 3.1(iii)–(iv): ESα(aX+b)=aESα(X)−bES_\alpha(aX+b)=aES_\alpha(X)-bESα​(aX+b)=aESα​(X)−b, as used in the proof of PROPOSITION 1(iii)

AT02 Prop. 3.1(iii)–(iv): $ES_\alpha(aX+b)=aES_\alpha(X)-b$ , as used in the proof of PROPOSITION 1(iii)