Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Theorem 2 — the demand estimator dPd_{\mathcal P}dP​ of a moment ambiguity set is subadditive

Proved
DRCVRP.Moment.demandEstimator_subadditive

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

distributionally-robust-optimizationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1subadditivityvehicle-routing

Let P\mathcal PP be a moment ambiguity set of the form (4),

P={P∈P0(Rn): P(q~∈Q)=1, EP[q~]=μ, EP[φ(q~)]≤σ},\mathcal P=\Big\{\mathbb P\in\mathcal P_0(\mathbb R^n):\ \mathbb P(\tilde{\boldsymbol q}\in\mathcal Q)=1,\ \mathbb E_{\mathbb P}[\tilde{\boldsymbol q}]=\boldsymbol\mu,\ \mathbb E_{\mathbb P}[\boldsymbol\varphi(\tilde{\boldsymbol q})]\le\boldsymbol\sigma\Big\},P={P∈P0​(Rn): P(q~​∈Q)=1, EP​[q~​]=μ, EP​[φ(q~​)]≤σ},

with support box Q=[q‾,q‾]\mathcal Q=[\underline{\boldsymbol q},\overline{\boldsymbol q}]Q=[q​,q​], q‾≥0\underline{\boldsymbol q}\ge\mathbf 0q​≥0, satisfying the standing assumptions μ∈int⁡Q\boldsymbol\mu\in\operatorname{int}\mathcal Qμ∈intQ, each component φl\varphi_lφl​ of φ:Rn→Rp\boldsymbol\varphi:\mathbb R^n\to\mathbb R^pφ:Rn→Rp convex, and φ(μ)<σ\boldsymbol\varphi(\boldsymbol\mu)<\boldsymbol\sigmaφ(μ)<σ. Let ϵ∈(0,1)\epsilon\in(0,1)ϵ∈(0,1) be the risk level and Q>0Q>0Q>0 the vehicle capacity, and let

dP(S)=max⁡{⌈1Qsup⁡P∈PP-VaR1−ϵ[∑i∈Sq~i]⌉,1} (S≠∅),dP(∅)=0,d_{\mathcal P}(S)=\max\left\{\left\lceil\frac1Q\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\right\rceil,1\right\}\ (S\neq\emptyset),\qquad d_{\mathcal P}(\emptyset)=0,dP​(S)=max{⌈Q1​P∈Psup​P-VaR1−ϵ​[i∈S∑​q~​i​]⌉,1} (S=∅),dP​(∅)=0,

be the demand estimator (2). Then dPd_{\mathcal P}dP​ satisfies the paper's subadditivity condition "(S) Subadditivity. For all customer subsets S,T⊆VCS, T\subseteq V_CS,T⊆VC​, we have dP(S∪T)≤dP(S)+dP(T)d_{\mathcal P}(S\cup T)\le d_{\mathcal P}(S)+d_{\mathcal P}(T)dP​(S∪T)≤dP​(S)+dP​(T)":

dP(S∪T) ≤ dP(S)+dP(T)for all S,T⊆VC.d_{\mathcal P}(S\cup T)\ \le\ d_{\mathcal P}(S)+d_{\mathcal P}(T)\qquad\text{for all } S,T\subseteq V_C .dP​(S∪T) ≤ dP​(S)+dP​(T)for all S,T⊆VC​.

By Theorem 1 of the paper, subadditivity of dPd_{\mathcal P}dP​ (together with nonnegative demands) makes the two-index vehicle flow formulation 2VF(P\mathcal PP) equivalent to the route-based distributionally robust CVRP, so this theorem shows that for every moment ambiguity set the compact formulation can be solved by branch-and-cut in place of the route-based one. For marginal-histogram ambiguity sets the estimator can fail to be subadditive (Example 1 of the paper).

Formalization Note Customer subsets are Finset (Fin n) (overlapping and empty subsets included). The estimator is integer valued. The statement is about the rounded estimator with its ceiling and its max⁡{⋅,1}\max\{\cdot,1\}max{⋅,1}, not about subadditivity of the worst-case VaR itself. See the definition item for the encoding of the ambiguity set and of the worst-case VaR.

Preamble
import Mathlib
import Definitions.Def_MultistageStochastic_RiskFunctional
import Definitions.Def_DRCVRP_Moment_AmbiguitySet

open MeasureTheory
Formal statement
namespace DRCVRP.Moment

theorem demandEstimator_subadditive {n p : ℕ} (qlo qhi μ : Fin n → ℝ)
    (φ : Fin p → (Fin n → ℝ) → ℝ) (σ : Fin p → ℝ) (ε Q : ℝ)
    (hqlo : ∀ i, 0 ≤ qlo i)
    (hμ : ∀ i, qlo i < μ i ∧ μ i < qhi i)
    (hφ : ∀ l, ConvexOn ℝ Set.univ (φ l))
    (hσ : ∀ l, φ l μ < σ l)
    (hε0 : 0 < ε) (hε1 : ε < 1) (hQ : 0 < Q)
    (S T : Finset (Fin n)) :
    demandEstimator (momentAmbiguitySet qlo qhi μ φ σ) ε Q (S ∪ T) ≤
      demandEstimator (momentAmbiguitySet qlo qhi μ φ σ) ε Q S +
        demandEstimator (momentAmbiguitySet qlo qhi μ φ σ) ε Q T := by sorry

end DRCVRP.Moment
Source
Ghosal and Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Oper. Res. 68(3) (2020) 716–732, §3, p. 723, Theorem 2; condition (S) p. 722; estimator p. 721, Eq. (2); ambiguity set p. 722, Eq. (4) and standing assumptions
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me