Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Theorem 8.11 — with K2K_2K2​ polyhedral and finite value, the deterministic equivalent convex program (8.2) is stable

Proved
Wets1974.Stability.stable_of_K2_polyhedral

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

dualitylagrange-multipliersp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1stochastic-programming

Consider a stochastic program with fixed recourse whose random element ξ\xiξ, with law a probability measure μ\muμ, satisfies the weak covariance condition (Definition 2.2), and whose recourse matrix WWW has full row rank (standing assumption, p. 312). Let Z(x)=cˉx+Q(x)Z(x)=\bar cx+\mathcal Q(x)Z(x)=cˉx+Q(x) be the objective (3.1) and K2K_2K2​ the induced constraint set (Corollary 4.5). Consider the deterministic equivalent convex program (8.2),

minimize Z(x)subject to Ax=b, x∈K2, x≥0.\text{minimize } Z(x)\quad\text{subject to } Ax=b,\ x\in K_2,\ x\ge0 .minimize Z(x)subject to Ax=b, x∈K2​, x≥0.

Suppose that

  1. K2K_2K2​ is a convex polyhedron, and
  2. the program is finite: v=inf⁡{Z(x):x∈K1∩K2}v=\inf\{Z(x): x\in K_1\cap K_2\}v=inf{Z(x):x∈K1​∩K2​} is a real number.

Then (8.2) is stable: there is a multiplier π∈Rm\pi\in\mathbb R^mπ∈Rm for the fixed constraints Ax=bAx=bAx=b with

v≤Z(x)+π (b−Ax)for every x∈K2 with x≥0.v\le Z(x)+\pi\,(b-Ax)\qquad\text{for every }x\in K_2\text{ with }x\ge0 .v≤Z(x)+π(b−Ax)for every x∈K2​ with x≥0.

Equivalently, the dual program (8.3), sup⁡{u∣u≤Q(x)+(cˉ−πA)x+πb  ∀x∈K2∩{x≥0}}\sup\{u \mid u\le\mathcal Q(x)+(\bar c-\pi A)x+\pi b\ \ \forall x\in K_2\cap\{x\ge0\}\}sup{u∣u≤Q(x)+(cˉ−πA)x+πb  ∀x∈K2​∩{x≥0}}, is solvable and there is no duality gap.

Stability means that the optimal value reacts at a bounded rate to perturbations b↦b−ub\mapsto b-ub↦b−u of the first-stage constraints. The paper's Example 8.5 shows that the weak covariance condition cannot be dropped.

Formalization Note The paper states the hypothesis as "KKK is polyhedral" with K=K1∩K2K=K_1\cap K_2K=K1​∩K2​. Read literally, that is false: with K2K_2K2​ the closed unit disk in R2\mathbb R^2R2 (produced by T(ξ)T(\xi)T(ξ) uniform on the unit circle, p≡1p\equiv1p≡1, W=(1)W=(1)W=(1), q≡0q\equiv0q≡0), c≡(−1,0)c\equiv(-1,0)c≡(−1,0), and K1={x2=1, x≥0}K_1=\{x_2=1,\ x\ge0\}K1​={x2​=1, x≥0}, the set K={(0,1)}K=\{(0,1)\}K={(0,1)} is polyhedral and the value 000 is finite, but −x1+π(1−x2)<0-x_1+\pi(1-x_2)<0−x1​+π(1−x2​)<0 at x=(2h−h2,1−h)x=(\sqrt{2h-h^2},1-h)x=(2h−h2​,1−h) for small h>0h>0h>0, so no multiplier exists. The paper's own sentence before Lemma 8.9 ties "polyhedral region" to K2K_2K2​ (Theorems 4.7, 4.10 concern K2K_2K2​), and the proof applies Lemma 8.9 with the objective's domain K2K_2K2​; the statement here uses K2K_2K2​. In (8.3) the page writes ccc where (3.1) and (8.2) require cˉ\bar ccˉ. The middle constraint of (8.2), written with the polar matrix W∗W^*W∗, is the constraint x∈K2x\in K_2x∈K2​ by Corollary 4.5.

Preamble
import Mathlib
import Definitions.Def_Wets1974_Stability_Model
Formal statement
namespace Wets1974.Stability

open MeasureTheory Matrix

/-- Theorem 8.11, p. 337 (with "K₂ polyhedral", see the natural-language statement): for a
stochastic program with fixed recourse satisfying the weak covariance condition, with `W` of
full row rank (p. 312), if the induced constraint set `K₂` is a polyhedron and the program is
finite, then the deterministic equivalent convex program (8.2),
`inf {Z(x) | A x = b, x ∈ K₂, x ≥ 0}`, is stable. -/
theorem stable_of_K2_polyhedral {n nb mb m : ℕ} (μ : Measure (DataSpace n nb mb))
    [IsProbabilityMeasure μ] (hcov : WeakCovariance μ)
    (W : Matrix (Fin mb) (Fin nb) ℝ) (hW : FullRowRank W)
    (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ)
    (hK2 : IsPolyhedron (K2 μ W))
    (hfin : IsFiniteProgram (Z μ W) (K2 μ W) A b) :
    IsStable (Z μ W) (K2 μ W) A b := by sorry

end Wets1974.Stability
Source
Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3), 1974, p. 337, Theorem 8.11; program (8.2) and dual (8.3), p. 334; Definition 8.1(iv), p. 334
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