Theorem 8.11 — with polyhedral and finite value, the deterministic equivalent convex program (8.2) is stable
ProvedWets1974.Stability.stable_of_K2_polyhedralConsider a stochastic program with fixed recourse whose random element , with law a probability measure , satisfies the weak covariance condition (Definition 2.2), and whose recourse matrix has full row rank (standing assumption, p. 312). Let be the objective (3.1) and the induced constraint set (Corollary 4.5). Consider the deterministic equivalent convex program (8.2),
Suppose that
- is a convex polyhedron, and
- the program is finite: is a real number.
Then (8.2) is stable: there is a multiplier for the fixed constraints with
Equivalently, the dual program (8.3), , is solvable and there is no duality gap.
Stability means that the optimal value reacts at a bounded rate to perturbations 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 " is polyhedral" with . Read literally, that is false: with the closed unit disk in (produced by uniform on the unit circle, , , ), , and , the set is polyhedral and the value is finite, but at for small , so no multiplier exists. The paper's own sentence before Lemma 8.9 ties "polyhedral region" to (Theorems 4.7, 4.10 concern ), and the proof applies Lemma 8.9 with the objective's domain ; the statement here uses . In (8.3) the page writes where (3.1) and (8.2) require . The middle constraint of (8.2), written with the polar matrix , is the constraint by Corollary 4.5.
import Mathlib import Definitions.Def_Wets1974_Stability_Model
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.