Corollary 7.3 — the LP value function is finite convex polyhedral on pos A, or identically −∞

Proved

Wets1974.Stability.LPValue_polyhedral_or_bot

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

convex-analysislinear-programmingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1parametric-lp

Let $A$ be a real $m\times n$ matrix and $c\in\mathbb R^n$ a row vector. For $t\in\mathbb R^m$ let

Q(t)=\min\{cx \mid Ax=t,\ x\ge 0\}\in[-\infty,+\infty]

(with $+\infty$ for an infeasible and $-\infty$ for an unbounded program), and let $\operatorname{pos}A=\{Ax: x\ge 0\}$ . Then exactly the following dichotomy holds:

either $Q$ is a finite convex polyhedral function on $\operatorname{pos}A$ : there are finitely many affine functions $a_0,\dots,a_k$ on $\mathbb R^m$ with

Q(t)=\max_{0\le i\le k}a_i(t)\in\mathbb R\qquad\text{for every }t\in\operatorname{pos}A;

or $Q(t)=-\infty$ for every $t\in\operatorname{pos}A$ .

In the paper's words, $Q$ is finite convex polyhedral on $\operatorname{pos}A$ unless $Q(t)=-\infty$ for some $t\in\operatorname{pos}A$ , in which case it is identically $-\infty$ there. This is the parametric-LP fact that makes the recourse function $Q(x,\xi)$ piecewise linear in its right-hand side, and it drives Proposition 7.5 and Theorem 7.6.

Formalization Note $Q$ is the platform definition KallMayer.Recourse.LPValue A c t. The paper's Theorem 7.2 assumes $A$ has rank $m$ ; Corollary 7.3 holds without it, and this statement omits it, which makes it stronger. "Convex polyhedral" is read as the maximum of finitely many affine functions (see the definition file); the paper never defines it.

Preamble

import Mathlib
import Definitions.Def_KallMayer_Recourse_LPValue
import Definitions.Def_Wets1974_Stability_ConvexAnalysis

Formal statement

namespace Wets1974.Stability

/-- Corollary 7.3, p. 328: the value function `Q(t) = min {c x | A x = t, x ≥ 0}` is a finite
convex polyhedral function on `pos A`, unless `Q(t) = −∞` for some `t ∈ pos A`, in which case
it is identically `−∞` on `pos A`. -/
theorem LPValue_polyhedral_or_bot {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (c : Fin n → ℝ) :
    IsFiniteConvexPolyhedralOn (fun t => KallMayer.Recourse.LPValue A c t) (posCone A) ∨
      ∀ t ∈ posCone A, KallMayer.Recourse.LPValue A c t = ⊥ := by sorry

end Wets1974.Stability

Source

Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3), 1974, p. 328, Corollary 7.3

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