Prove2Me

Distributionally robust chance constraint   ⟺  \iff worst-case VaR bound, Eq. (1)

Proved
DRCVRP.RCI.chance_constraint_iff_worstCaseVaR_le

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

chance-constraintsdistributionally-robust-optimizationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1value-at-risk

Let P\mathcal P be a nonempty set of probability distributions of the demand vector q~∈Rn\tilde{\boldsymbol q}\in\mathbb R^n, let ϵ∈(0,1)\epsilon\in(0,1), Q∈RQ\in\mathbb R, and let Rk\mathbf R_k be a route, a list of distinct customers. Assume the values P-VaR1−ϵ[∑i∈Rkq~i]\mathbb P\text{-VaR}_{1-\epsilon}[\sum_{i\in\mathbf R_k}\tilde q_i], P∈P\mathbb P\in\mathcal P, are bounded above. Then

P[Rk∈R(q~)]≥1−ϵ  ∀P∈P  ⟺  P-VaR1−ϵ[∑i∈Rkq~i]≤Q  ∀P∈P  ⟺  sup⁡P∈PP-VaR1−ϵ[∑i∈Rkq~i]≤Q,\mathbb P\big[\mathbf R_k\in\mathcal R(\tilde{\boldsymbol q})\big]\ge1-\epsilon\ \ \forall\mathbb P\in\mathcal P \iff \mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in\mathbf R_k}\tilde q_i\Big]\le Q\ \ \forall\mathbb P\in\mathcal P \iff \sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in\mathbf R_k}\tilde q_i\Big]\le Q ,

where Rk∈R(q)\mathbf R_k\in\mathcal R(\boldsymbol q) means ∑i∈Rkqi≤Q\sum_{i\in\mathbf R_k}q_i\le Q.

A route satisfies its distributionally robust chance constraint exactly when the worst-case value-at-risk of its cumulative demand fits into one vehicle; this is what motivates the demand estimator (2).

Formalization Note The statement is the conjunction of the first-and-second and the first-and-third equivalences. The supremum is a real sSup; nonemptiness and boundedness above of the VaR values make it the paper's finite supremum (for an empty P\mathcal P the paper's supremum is −∞-\infty, which a real sSup cannot represent). The route is a List (Fin n) without duplicates, and the sum over the route is the sum over its underlying finite set.

Preamble
import Mathlib
import Definitions.Def_MultistageStochastic_RiskFunctional
import Definitions.Def_DRCVRP_RCI_DemandEstimator
import Definitions.Def_DRCVRP_RCI_Formulations

open MeasureTheory
Formal statement
namespace DRCVRP.RCI

/-- Eq. (1), §3, p. 721: for a route `R_k` (a list of distinct customers) and an ambiguity set
`𝒫` (`Amb`) of probability distributions of the demand vector,
`ℙ[R_k ∈ ℛ(q̃)] ≥ 1 - ε ∀ ℙ ∈ 𝒫 ⟺ ℙ-VaR_{1-ε}[∑_{i ∈ R_k} q̃_i] ≤ Q ∀ ℙ ∈ 𝒫
⟺ sup_{ℙ ∈ 𝒫} ℙ-VaR_{1-ε}[∑_{i ∈ R_k} q̃_i] ≤ Q`.
The supremum is a real `sSup`; `Amb` nonempty and the VaR values bounded above make it the
paper's (finite) supremum. -/
theorem chance_constraint_iff_worstCaseVaR_le {n : ℕ} (Amb : Set (Measure (Fin n → ℝ)))
    (hAmb : ∀ P ∈ Amb, IsProbabilityMeasure P) (hne : Amb.Nonempty)
    (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε < 1) (Q : ℝ) (r : List (Fin n)) (hr : r.Nodup)
    (hbdd : BddAbove ((fun P => MultistageStochastic.valueAtRisk P
      (fun q => ∑ i ∈ r.toFinset, q i) (1 - ε)) '' Amb)) :
    (RouteChanceFeasible Amb ε Q r ↔
      ∀ P ∈ Amb, MultistageStochastic.valueAtRisk P (fun q => ∑ i ∈ r.toFinset, q i) (1 - ε) ≤ Q) ∧
    (RouteChanceFeasible Amb ε Q r ↔ worstCaseVaR Amb ε r.toFinset ≤ Q) := by sorry

end DRCVRP.RCI
Source
Ghosal and Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Oper. Res. 68(3) (2020) 716–732, §3, p. 721, Eq. (1)
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