Chapter 3, Theorem 5(a) -- K2 is closed and convex

Proved

StochasticProg.Recourse.thm5a_K2_closed_convex

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

convex-optimizationrecoursestochastic-programming

Chapter 3, Theorem 5(a). For a two-stage recourse instance with fixed recourse matrix $W$ and a finite scenario set, the second-stage feasibility set

K_2 = \{x \mid Q(x) < \infty\}

is closed and convex.

This is the book's structural fact underlying every later optimality result of the chapter: the constraint set of the deterministic-equivalent program (1.2) is well-behaved (closed, convex) before anything is said about the recourse value $Q$ itself.

Formalization Note. The book states Theorem 5 for a general random vector $\xi$ with finite second moments; under the finite-scenario model Fin K used throughout this mission, "finite second moments" holds automatically, so the hypothesis does not appear as a separate argument.

Preamble

import Mathlib
import Definitions.Def_StochasticProg_Recourse_Instance

Formal statement

namespace StochasticProg.Recourse

variable {n1 n2 m1 m2 K : ℕ}

/-- Chapter 3, Theorem 5(a) (p. 111): for a fixed recourse matrix `W` and a finite
scenario set (finite second moments are automatic), the second-stage feasibility
set `K2` is closed and convex. -/
theorem thm5a_K2_closed_convex (inst : Instance n1 n2 m1 m2 K) :
    IsClosed (K2 inst) ∧ Convex ℝ (K2 inst) := by sorry

end StochasticProg.Recourse

Source

Birge & Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer 2011, p. 111, Chapter 3, Theorem 5(a)

Read-back

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

Let $n_1, n_2, m_1, m_2, K$ be natural numbers (any values are allowed, including $0$ ), and let $\mathrm{inst}$ be an arbitrary element of the type $\mathrm{Instance}\; n_1\; n_2\; m_1\; m_2\; K$ . This type, and the map $K_2$ applied to it below, are custom definitions from the imported file Definitions.Def_StochasticProg_Recourse_Instance, whose contents are not part of the code given here; nothing in this declaration constrains what an instance contains (no hypothesis is placed on $\mathrm{inst}$ , and in particular no assumption about a recourse matrix, scenario set, moments, or fixedness of anything appears as a binder or hypothesis of the theorem).

The statement asserts, for every such $\mathrm{inst}$ , the conjunction of two claims about the set $K_2(\mathrm{inst})$ , where $K_2(\mathrm{inst})$ is whatever set the imported definition K2 produces from $\mathrm{inst}$ — a subset of some ambient type that the code does not display:

K_2(\mathrm{inst}) \text{ is closed} \quad\text{and}\quad K_2(\mathrm{inst}) \text{ is convex over } \mathbb{R}.

Here "closed" means closed with respect to whatever topology the ambient type of $K_2(\mathrm{inst})$ carries (as inferred from its typeclass instances, not stated in this declaration), and "convex over $\mathbb{R}$ " means: for all $x, y \in K_2(\mathrm{inst})$ and all real $a, b \ge 0$ with $a + b = 1$ , the point $a\,x + b\,y$ lies in $K_2(\mathrm{inst})$ , using the real scalar multiplication and addition of that ambient type. Both properties hold trivially if $K_2(\mathrm{inst})$ is empty or is the whole space, and the statement does not exclude either case. The proof body is sorry, i.e. the claim is stated but not proved.

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