Chapter 3, Theorem 9 -- KKT optimality condition for the two-stage recourse LP

Proved

StochasticProg.Recourse.thm9_kkt_optimality

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

convex-optimizationkktrecoursestochastic-programming

Chapter 3, Theorem 9 (goal theorem). Suppose the deterministic-equivalent program (1.2) -- minimize $z(x) = c^{\mathsf T}x + Q(x)$ over $K_1 = \{x \mid Ax=b,\ x\ge 0\}$ -- has a finite optimal value. A point $x^* \in K_1$ is optimal if and only if there exist $\lambda^* \in \mathbb{R}^{m_1}$ and $\mu^* \in \mathbb{R}^{n_1}_{\ge 0}$ with $(\mu^*)^{\mathsf T}x^* = 0$ such that

-c + A^{\mathsf T}\lambda^* + \mu^* \in \partial Q(x^*).

This is the KKT-style optimality condition for the two-stage stochastic linear program with fixed recourse: it combines the subdifferential of the convex, possibly nondifferentiable recourse function $Q$ (Theorem 6) with the ordinary linear-programming complementarity condition for the polyhedral constraint set $K_1$ .

Formalization Note. "Optimal in (1.2)" is formalized as attaining the infimum of $z$ over $K_1$ , i.e. $z(x^*) = \inf_{x \in K_1} z(x)$ , using the extended-real-valued sInf; "finite optimal value" is the hypothesis that this infimum equals some real $z_0$ , exactly as the theorem statement presupposes. $\partial Q(x^*)$ is StochasticProg.Recourse.subdiffQ.

Moderator's note. The book's standing assumption for §3.1c–e (p. 112: "assuming it is not −∞") is stated explicitly: no second-stage problem is unbounded below (Q(x, ξ_k) ≠ −∞ for every x and scenario k; for the abstract Q of Corollary 10, Q x ≠ −∞). Without it "finite on K₂" and the KKT characterisation can fail.

Preamble

import Mathlib
import Definitions.Def_StochasticProg_Recourse_Instance
import Definitions.Def_StochasticProg_Recourse_Subdiff

Formal statement

namespace StochasticProg.Recourse

variable {n1 n2 m1 m2 K : ℕ}

/-- Chapter 3, Theorem 9 (p. 116), the goal theorem: suppose the deterministic
equivalent problem (1.2) has a finite optimal value. A solution `x* ∈ K1` is
optimal if and only if there exist `λ* ∈ ℝ^{m1}` and `μ* ∈ ℝ^{n1}_+` with
`(μ*)ᵀx* = 0` such that `-c + Aᵀλ* + μ* ∈ ∂Q(x*)` (Eq. (1.12)). -/
theorem thm9_kkt_optimality (inst : Instance n1 n2 m1 m2 K)
    (hQ : ∀ x k, QVal inst x k ≠ ⊥)
    (hfin : ∃ z0 : ℝ, sInf (obj inst '' K1 inst) = (z0 : EReal))
    (xstar : Fin n1 → ℝ) (hx : xstar ∈ K1 inst) :
    (obj inst xstar = sInf (obj inst '' K1 inst)) ↔
      ∃ (lam : Fin m1 → ℝ) (mu : Fin n1 → ℝ),
        (∀ i, 0 ≤ mu i) ∧ dotProduct mu xstar = 0 ∧
        (fun j => -inst.c j + Matrix.mulVec (Matrix.transpose inst.A) lam j + mu j) ∈
          subdiffQ inst xstar := by sorry

end StochasticProg.Recourse

Source

Birge & Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer 2011, p. 116, Chapter 3, Theorem 9

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Fix natural numbers $n_1, n_2, m_1, m_2, K$ (all implicit; any values, including $0$ , are allowed) and an object $\mathrm{inst}$ of a bundle-defined type $\mathrm{Instance}\, n_1\, n_2\, m_1\, m_2\, K$ . The statement itself only exposes two components of $\mathrm{inst}$ : a vector $c \in \mathbb{R}^{n_1}$ (written $\mathrm{inst}.c$ ) and a real matrix $A$ with $m_1$ rows and $n_1$ columns (written $\mathrm{inst}.A$ ); whatever else $\mathrm{Instance}$ contains is not visible here. The statement also uses four bundle-defined objects whose definitions are not part of this declaration and are therefore opaque to this read-back; only their types can be seen:

$\mathrm{QVal}(\mathrm{inst}, x, k)$ : for $x \in \mathbb{R}^{n_1}$ and an index $k$ of some unspecified type, a value in the extended reals $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$ ;
$\mathrm{obj}(\mathrm{inst})$ : a function $\mathbb{R}^{n_1} \to \overline{\mathbb{R}}$ , written $f$ below;
$K_1(\mathrm{inst})$ : a subset of $\mathbb{R}^{n_1}$ , written $K_1$ below;
$\mathrm{subdiffQ}(\mathrm{inst}, x)$ : for $x \in \mathbb{R}^{n_1}$ , a subset of $\mathbb{R}^{n_1}$ , written $\partial Q(x)$ below (the name is the bundle's; nothing here asserts it is a subdifferential of anything).

Let $z^\star \in \overline{\mathbb{R}}$ denote the infimum $\inf\{\, f(x) : x \in K_1 \,\}$ , taken in the extended reals (so it always exists; in particular it is $+\infty$ if $K_1$ is empty).

Hypotheses.

For every $x \in \mathbb{R}^{n_1}$ and every index $k$ , $\mathrm{QVal}(\mathrm{inst}, x, k) \neq -\infty$ . (The value $+\infty$ is not excluded.)
There exists a real number $z_0$ with $z^\star = z_0$ , i.e. the infimum is a finite real number — neither $+\infty$ nor $-\infty$ . This in particular forces $K_1 \neq \emptyset$ . It does not assert that the infimum is attained.
A point $x^\star \in \mathbb{R}^{n_1}$ with $x^\star \in K_1$ .

Conclusion. The following two statements are equivalent (a biconditional, both directions):

(a) $f(x^\star) = z^\star$ , as an equality in $\overline{\mathbb{R}}$ (so, given hypothesis 2, $f(x^\star)$ is the finite real number $z_0$ );
(b) there exist vectors $\lambda \in \mathbb{R}^{m_1}$ and $\mu \in \mathbb{R}^{n_1}$ such that

\mu_i \ge 0 \text{ for every } i \in \{1,\dots,n_1\}, \qquad \sum_{i=1}^{n_1} \mu_i\, x^\star_i = 0,

and the vector $v \in \mathbb{R}^{n_1}$ with components

v_j = -c_j + (A^{\mathsf T}\lambda)_j + \mu_j, \qquad j \in \{1,\dots,n_1\},

satisfies $v \in \partial Q(x^\star)$ . Here $(A^{\mathsf T}\lambda)_j = \sum_{i=1}^{m_1} A_{ij}\,\lambda_i$ .

Nothing is asserted about uniqueness of $\lambda$ , $\mu$ , or $x^\star$ ; the existential in (b) is plain existence.

Edge cases the quantifiers include. If $n_1 = 0$ , then $x^\star$ , $c$ , $\mu$ and $v$ are all the empty vector, the sign and orthogonality conditions on $\mu$ hold trivially, and (b) reduces to "the empty vector lies in $\partial Q(x^\star)$ ". If $m_1 = 0$ , then $\lambda$ is the empty vector and $A^{\mathsf T}\lambda = 0$ , so $v = -c + \mu$ . If hypothesis 1 fails for any $x, k$ , or if the infimum $z^\star$ is $\pm\infty$ (including the case $K_1 = \emptyset$ ), the theorem asserts nothing. Because $f$ takes values in $\overline{\mathbb{R}}$ , $f(x^\star)$ may a priori be $+\infty$ or $-\infty$ ; in that case (a) is false (the infimum is finite), and the theorem then claims that no $\lambda, \mu$ as in (b) exist. The parameters $n_2$ , $m_2$ , $K$ and the index type of $k$ play no visible role in the statement beyond being carried by $\mathrm{inst}$ and hypothesis 1.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph