(3.11) — a distortion risk functional is a mixture of Average Values-at-Risk

Proved

MultistageStochastic.distortion_avar_mixture

by naimengye · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-analysisoperations-researchprobabilityrisk-measures

Let $\sigma$ be a distortion function. Then there is a probability measure $\mu$ on $[0,1]$ , depending on $\sigma$ only, such that on every probability space $(\Omega,\mathcal F,P)$ and for every $Y\in L^\infty(P)$

\mathcal R_\sigma(Y)\;=\;\int_0^1\mathsf{AV@R}_\alpha(Y)\,\mu(d\alpha) . \tag{3.11}

The source exhibits the measure: $\mu_\sigma(A)=\sigma(0)\,\delta_0(A)+\int_A(1-u)\,d\sigma(u)$ , (3.12), an atom at $0$ of mass $\sigma(0)$ plus the Lebesgue–Stieltjes measure of $\sigma$ weighted by $1-u$ , and verifies by integration by parts that it is a probability measure and that the identity holds. This is the representation of "elementary importance" that identifies the distortion functionals with the mixtures in Kusuoka's theorem (mission II) whose supremum consists of a single measure.

Formalization Note The statement asserts the existence of the mixing measure rather than constructing (3.12), because the Lebesgue–Stieltjes measure of a nondecreasing density is not available in a form that makes the explicit formula shorter than the proof. The measure is quantified before the probability space, as the source's $\mu_\sigma$ is built from $\sigma$ alone: with the space bound first, $\mu$ could depend on $P$ , and on a one-point space every probability measure on $[0,1]$ would satisfy the identity. "Probability measure on $[0,1]$ " is mission II's IsKusuokaMeasure, and the Average Value-at-Risk at $\alpha=1$ is the essential supremum, as there.

Preamble

import Definitions.Def_MultistageStochastic_RiskFunctional
import Definitions.Def_MultistageStochastic_Distortion
open MeasureTheory
open scoped ENNReal

Formal statement

namespace MultistageStochastic
theorem distortion_avar_mixture (σ : ℝ → ℝ) (hσ : IsDistortionFunction σ) :
    ∃ μ : Measure ℝ, IsKusuokaMeasure μ ∧
      ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω), IsProbabilityMeasure P →
        ∀ Y, MemLinfty P Y →
          distortionFunctional P σ Y = ∫ α, averageValueAtRisk P Y α ∂μ := by sorry
end MultistageStochastic

Source

Georg Ch. Pflug and Alois Pichler, Multistage Stochastic Optimization, Springer 2014, https://doi.org/10.1007/978-3-319-08843-3 — Section 3.2, printed p. 100 (PDF p. 113), representation (3.11): "R_σ(Y) = ∫_0^1 V@R_α(Y) σ(α) dα = ∫_0^1 AV@R_α(Y) μ_σ(dα) for a probability measure μ_σ on the interval [0, 1]", with μ_σ given by (3.12) and the identity established on printed p. 101 (PDF p. 114).

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph