Operations Research

Motivation

Chapter 3 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks which of the assumptions behind the index theorem can be dropped and which cannot, using the simplest bandit processes there are: jobs, which pay a single reward when they complete. Along the way it settles three questions that matter on their own. When identical machines run in parallel, which schedule of deterministic jobs minimizes the total completion time (Baker's theorem), and what does the equal-ratio case look like (Theorem 3.3)? When an object is hidden in one of several boxes and each search costs money and may fail, in what order should the boxes be searched (Blackwell's search-index theorem, Theorem 3.6)? And when two bandit processes discount at different rates, is there still an index policy (Nash's Theorem 3.4)? The search theorem is the chapter's example of what the index machinery yields once undiscounted criteria are admitted through the limit $\gamma \downarrow 0$; the scheduling results are the source of the counterexamples that show a second machine breaks the index structure.

Setting

Jobs on parallel machines. There are $n$ jobs with service times $s_i > 0$ and weights $c_i$, and $m$ identical machines. A schedule assigns each job a machine and a position in that machine's processing order; each machine processes its jobs consecutively. The completion time $C_i$ of a job is the total service time of the jobs on its machine up to and including it; the flow time is $\sum_i C_i$ and the weighted flow time $\sum_i c_i C_i$. The load of a machine is the total service time assigned to it, and $\delta_j$ is its excess over the average $S/m$. The SPT list schedule sorts the jobs by increasing service time and deals them out cyclically to the machines. The level of a job is its position counted from the end of its machine's schedule.

The search problem (Problem 3). A stationary object is hidden in one of $n$ boxes, in box $i$ with probability $p_i$. A search of box $i$ costs $c_i$ and finds the object with probability $q_i$ if it is there. A search policy is a sequence of boxes; after $N_i$ unsuccessful searches of box $i$ the posterior probability that the object is there is proportional to $p_i(1-q_i)^{N_i}$, and the search index of the box is $p'_i q_i/c_i$, the current probability of finding the object per unit cost. The expected cost of a policy is $\sum_k c_{\sigma_k}\Pr[\text{not found by the first } k \text{ searches}]$.

Two discount factors. Bandit process $A$ (state space $S_A$, kernel $P_A$, reward $r_A$) discounts at rate $a$ and $B$ at rate $b$; a reward obtained at time $t$ is worth $a^t$ or $b^t$ times its face value according to which process produced it. The cross indices are $\nu_{AB}(x) = \sup_{\tau>0} \mathbb{E}\sum_{t<\tau} a^t r_A(x(t)) \big/ \mathbb{E}[1 - b^\tau]$ and $\nu_{BA}(y)$ with the roles exchanged: each is computed from one process's stopping times but with the other's discount factor in the denominator. The book prints the denominator as $\mathbb{E}\int_0^\tau b^t\,dt$ and compares $\nu_{AB}(x)$ with $\nu_{BA}(y)$ at every time; both are corrected here (see the Theorem 3.4 item), since the printed rule is not optimal. The family is the two-armed Markov bandit of the Bandit Algorithms model on the disjoint union $S_A \oplus S_B$.

Formalization targets

Goal: Theorem 3.6

For prior probabilities $p_i \ge 0$ summing to one, detection probabilities $0 < q_i \le 1$ and costs $c_i > 0$, a search policy is optimal if and only if at every step it searches a box of maximal current index $p'_i q_i / c_i$:

Milestones

Theorem 3.3, as the identity $\sum_i c_i C_i = \frac{\kappa}{2}\big(\sum_i s_i^2 + S^2/m + \sum_j \delta_j^2\big)$ when $c_i = \kappa s_i$; Theorem 3.4 in discrete time and corrected, that a policy selecting, at time $t$, $A$ when $a^t \nu_{AB}(x) > b^t \nu_{BA}(y)$ and $B$ when $a^t \nu_{AB}(x) < b^t \nu_{BA}(y)$ attains the supremum of the bandit-dependently discounted payoff; Theorem 3.7, that SPT minimizes the flow time on $m$ machines and that the optimal schedules are exactly those placing the $r$-th block of $m$ longest jobs at level $r$ from the end, for some order of the equal jobs.

Significance

Theorem 3.6 is the classical solution of the discrete search problem (Blackwell, reported by Matula 1964; Kadane 1969): the greedy rule in probability-per-cost is optimal, and every optimal policy is of that form. The book derives it from the index theorem through an auxiliary family of bandit processes (Problem 3A) and the undiscounted limit (Corollary 3.5), which is why it sits in this chapter; as a statement it is elementary and self-contained, and it is the template for the tax problems and Klimov's model of Chapter 4. Theorem 3.7 and Theorem 3.3 are the positive results about parallel machines that survive the loss of the index structure; Theorem 3.4 shows the index theorem's shape persisting under bandit-dependent discounting, with two twists: each index depends on the other process's discount factor, which is exactly why it does not extend to three processes, and the comparison at time $t$ weighs the indices by $a^t$ and $b^t$, so the rule is not stationary in the states. The printed statement misses the second twist and misnormalizes the first; two one-state bandits paying $0.18$ ($a = 0.9$) and $1$ ($b = 0.5$) are best played $B, B, B$ and then $A$ forever, which no stationary rule does.

None of these is machine-checked. Formalizing them gives the platform an optimality theorem for an infinite-horizon search process with an explicit index characterization in both directions, the standard parallel-machine flow-time results with a precise uniqueness clause, and a first statement on the Bandit Algorithms two-armed model with unequal discounting.

Difficulty

For Theorem 3.6 the obvious route, comparing two adjacent searches, gives only that interchanging a pair in the wrong index order lowers the cost; turning that into optimality over all infinite sequences needs that an optimal policy exists (costs are bounded below by zero and the index policy has finite cost), that a policy neglecting a box of positive prior has infinite cost, and that any first deviation from the index rule can be improved by moving a later search forward, which requires tracking how the not-found probability changes along the whole tail. The converse direction is the same interchange run backwards, and the tie case must be handled so that the equivalence is exact. Theorem 3.7's first part follows from writing the flow time as $\sum_i \ell_i s_i$ with $\ell_i$ the level and applying a rearrangement inequality over the multiset of levels, but the multiset of levels itself depends on how many jobs each machine gets, so balancing the machine counts is part of the argument; the uniqueness clause needs both that the multiset is forced and that the pairing of levels with service times is forced by strict monotonicity. Theorem 3.4 is the hardest: the book's proof changes the time scale of each process so that the two share a discount factor, which produces a semi-Markov family, and applies the index theorem there; in discrete time on the Markov model one needs either a discrete analogue of that argument or a direct prevailing-charge proof with two charge scales.

Formalization scope

Schedules are assignments of machines and positions with distinct positions on a machine, without idling; the flow-time quantities are finite sums over Fin n. The SPT schedule is defined by the ascending rank of a job (ties broken by index) and carries its own injectivity proof. The search cost is a series in $[0, \infty]$ of nonnegative terms, so no summability hypothesis is needed and "infinite cost" is literal; the index is stated unnormalized, $p_i(1-q_i)^{N_i} q_i/c_i$, which orders the boxes exactly as the posterior index does. The two-discount family uses the platform's MarkovBanditPolicy 2 (S_A ⊕ S_B) and markovBanditMeasure with the kernel that moves an $A$-state by $P_A$ and a $B$-state by $P_B$; the payoff is the round-by-round series $\sum_t (a^t \mathbb{E}[r\mathbf 1\{A_t = A\}] + b^t \mathbb{E}[r\mathbf 1\{A_t = B\}])$, absolutely summable for bounded rewards, and the policy condition is imposed at histories whose current states have the right types (all reachable histories do). Hypotheses: $m \ge 1$, service times positive; $p_i \ge 0$, $\sum p_i = 1$, $0 < q_i \le 1$, $c_i > 0$; countable state spaces, bounded rewards, $a, b \in (0,1)$.

Trivializing readings are excluded: the search "iff" is over all sequences, not a finite horizon; the uniqueness clause is stated in full, with ties resolved by any ranking of the equal jobs; the cross indices are suprema over positive stopping times (denominators at least one), and the two-discount rule weighs the indices by $a^t$, $b^t$. Welcome contributions: the rearrangement and level-count lemmas for schedules, the interchange lemma for the search cost, and a discrete prevailing-charge argument for Theorem 3.4.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 3. doi:10.1002/9780470980033
• D. W. Matula, A periodic optimal search, American Mathematical Monthly 71(1), 1964. doi:10.2307/2311300
• J. B. Kadane, Quiz show problems, Journal of Mathematical Analysis and Applications 27(3), 1969. doi:10.1016/0022-247X(69)90140-2
• K. R. Baker, Introduction to Sequencing and Scheduling, Wiley, 1974.
• P. Nash, A generalized bandit problem, Journal of the Royal Statistical Society B 42(2), 1980. doi:10.1111/j.2517-6161.1980.tb01119.x

Motivation

Every data-driven decision problem faces the same trap. A decision-maker estimates a risk functional $R(P,\ell) = \mathbb{E}_P[\ell(\xi)]$ from a nominal distribution $\hat P_N$ built from $N$ training samples, then optimizes a loss function $\ell$ against $\hat P_N$ instead of the unknown true distribution $P$. Because the optimizer adapts to the noise in $\hat P_N$, the in-sample risk of the optimizer systematically understates its true, out-of-sample risk — a phenomenon Smith and Winkler named the optimizer's curse (Smith & Winkler, Management Science, 2006). The remedy explored here is to hedge against a whole neighborhood of plausible distributions around $\hat P_N$, rather than trusting the point estimate. Kuhn, Mohajerin Esfahani, Nguyen and Shafieezadeh-Abadeh's INFORMS TutORials chapter (2019) develops this neighborhood using the Wasserstein distance, and the present mission formalizes its foundational duality theory: the machinery every later result in the chapter (finite-sample guarantees, elliptical tractability, regularization) builds on.

Setting

Fix a norm $\|\cdot\|$ on a finite-dimensional real vector space $E$ (representing $\mathbb{R}^m$). For $p \in [1,\infty)$, the type-$p$ Wasserstein distance between two Borel probability measures $Q, Q'$ on $E$ is

where $\Pi(Q,Q')$ is the set of couplings of $Q$ and $Q'$ — joint probability measures on $E \times E$ whose marginals are $Q$ and $Q'$. The optimal $\pi$ can be read as a transportation plan moving one pile of dirt ($Q$) into another ($Q'$) at minimum cost, which is why $W_p$ is also called the earth mover's distance; the underlying linear program was formalized by Kantorovich (1942) after Monge's 1781 original.

Given $N$ training samples $\hat\xi_1,\dots,\hat\xi_N$, the empirical distribution is $\hat P_N = \frac1N\sum_{i=1}^N \delta_{\hat\xi_i}$. Centered at $\hat P_N$, the Wasserstein ambiguity set of radius $\varepsilon \ge 0$ is

where $\Xi \subseteq E$ is a closed set known to contain the support of the true distribution. The worst-case risk of a loss function $\ell$ is

and minimizing it over a class of admissible loss functions $\mathcal{L}$ is a distributionally robust optimization problem. $\varepsilon$ measures the estimation error one insures against; a larger ambiguity set gives a more conservative (and more expensive) guarantee.

Formalization targets

Goal — Theorem 7, strong duality

This is the Lagrangian dual of the worst-case risk evaluation problem, with $\gamma$ the multiplier of the Wasserstein constraint $W_p(Q,\hat P_N)\le\varepsilon$: it converts a supremum over an infinite-dimensional space of measures into a one-dimensional minimization of the Moreau-Yosida regularization $\ell_\gamma$. Every tractability result later in the chapter (finite convex reformulations, SDP relaxations) specializes this duality by choosing a loss class for which $\ell_\gamma$ is computable.

Supporting dual representations of $W_p$ — Theorems 1 and 2

These identify $W_p$ as a linear program's strong dual (Theorem 1) and, for $p=1$, specialize it to the Kantorovich-Rubinstein form (Theorem 2), which is what lets the worst-case-risk analysis reason about Lipschitz loss functions directly.

Upper and lower bounds — Theorems 5 and 6

These are the tractable, easily-computed bracket that Theorems 7 and 10 later show is tight in important special cases.

Exact case — Theorem 10

Theorem 5's inequality becomes exact under convexity — the cleanest closing corollary of the duality theory, obtained from Theorem 7 by evaluating the Moreau-Yosida regularization of a convex function explicitly.

Significance

Theorem 7 is the hinge on which the entire computational program of Wasserstein distributionally robust optimization turns: every tractable reformulation in the source chapter (piecewise-concave losses via conic duality, quadratic losses via semidefinite programming, the shrinkage-estimator connection) is obtained by substituting a specific loss class into the right-hand side of Theorem 7 and showing the resulting Moreau-Yosida regularization is computable. Kuhn et al. themselves derive it as a corollary of Blanchet & Murthy (2019) and Gao & Kleywegt (2016) for the empirical case, generalized to Polish spaces by Blanchet & Murthy and Gao & Kleywegt independently — the paper cites [12] and [37] for the general statement. Formalizing it is what makes every later, more computational result in the chapter — the ones a solver is more likely to reach for next — rest on a mechanically verified foundation rather than a citation chain.

Status. The mathematical result is well established (multiple independent published proofs cited above); nothing here is open research. What this mission contributes is the first machine-checked formal statement of the duality theorem and its supporting dual representations (Theorems 1, 2, 5, 6, 10) on the Prove2Me platform — none of Wp's dual representation, the Wasserstein ambiguity set, or the worst-case risk functional exist there prior to this mission (see Formalization scope).

Difficulty

The obvious proof strategy — write down the Lagrangian of the semi-infinite program (6), swap the order of the outer supremum over $Q$ and the inner minimization over the multiplier $\gamma$, and invoke ordinary Lagrangian strong duality — fails because (6) is an infinite- dimensional linear program over measures, not a finite convex program: there is no compact feasible set or Slater point in a form that ordinary finite-dimensional duality applies to directly. The actual proof goes through the dual representation of the Wasserstein distance itself (Theorem 1, which is why it is a prerequisite milestone), reformulating the constraint $W_p(Q,\hat P_N)\le\varepsilon$ via its own dual variables and swapping the resulting sup-inf using minimax theorems for semi-infinite programs, not ordinary Lagrangian duality for finite programs.

Formalization scope

$E$ is a generic finite-dimensional real normed space (NormedAddCommGroup, NormedSpace ℝ, Borel-measurable), representing $\mathbb{R}^m$ with the paper's arbitrary fixed norm as a parameter rather than fixing the Euclidean norm. A coupling is formalized directly via MeasureTheory.Measure.map: π.map Prod.fst = Q ∧ π.map Prod.snd = Q'. Constrained infima/suprema (over couplings, over the ambiguity set, over Lipschitz test functions, over perturbation matrices) use Mathlib's guarded-binder idiom ⨅ x (_ : P x), f x, which correctly returns $\top$ (resp. $\bot$) outside the feasible set rather than a finite junk value.

Two deliberate, disclosed conventions keep the extremal-value definitions faithful without extended-real integration machinery, both recorded in MODERATION_NOTES.md:

1. worstCaseRisk and the dual representations (Theorems 1, 2) are valued in EReal, not ℝ, so an unbounded supremum is recorded as $+\infty$ rather than collapsed to Mathlib's real-valued junk value 0 on an unbounded family.
2. The goal theorem (7) and its Moreau-Yosida regularization restrict the loss function to bounded continuous $\ell$ (BoundedContinuousFunction E ℝ), narrower than the paper's general upper-semicontinuous, $\hat P_N$-integrable loss class $\mathcal{L}$ (Assumption 1). This keeps $\ell_\gamma(\xi) = \sup_{z\in\Xi}\ell(z)-\gamma\|z-\xi\|^p$ a finite real number for every nonempty $\Xi$, so the right-hand side's Bochner integral is well-posed; the milestones (Theorems 5, 6, 10) keep the more general real-valued (not necessarily bounded) loss class, since their statements do not require evaluating a pointwise supremum over $\Xi$.
3. Ξ is required closed in Theorems 5, 6 and 7, matching the paper's own standing assumption (p. 6: "we let $\Xi\subseteq\mathbb{R}^m$ be a closed set that is known to contain the support of $P$") for the whole worst-case-risk framework, which is used silently in the paper wherever a theorem takes $\Xi$ as an argument but was not carried into these theorems' own hypothesis lists in an earlier draft.
4. The goal theorem (7) additionally requires $\hat P_N$ itself supported on $\Xi$ ($\hat P_N(\Xi^c)=0$, the same "supported on $\Xi$" convention ambiguitySet uses for $Q\in\mathcal P(\Xi)$), which the paper's framework presupposes for the nominal distribution throughout §2. Combined with $\ell$ bounded, this makes $\ell_\gamma$ bounded on the full-measure set $\Xi$ (above by $\sup\ell$ unconditionally, below by $\ell(\xi)$ itself via $z=\xi$ for $\xi\in\Xi$), which is what makes the right-hand side's integral genuinely well-posed rather than liable to Mathlib's non-integrable junk value $0$.

There is no trivializing formalization risk from a vacuous hypothesis: Ξ.Nonempty and 0 < N are both required exactly where the paper's own indexing and support assumptions require them, and every extremal value uses the extended-real convention above rather than a convention that would make an inequality vacuously true.

No definition in this mission exists on the platform prior to this series (GET /theorems?q=Wasserstein, q=Kantorovich, q=optimal transport, q=coupling return only unrelated discrete/finite-type constructions); all seven definitions and six theorems are drafted fresh. WassersteinDRO.Duality.wassersteinDistance, .ambiguitySet and .worstCaseRisk are the substrate every later mission in this five-part series (Gelbrich tractability, finite-sample guarantees, regularization, shrinkage estimation) either imports directly or redefines locally per the series' reuse rule.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research, 130–166. https://doi.org/10.1287/educ.2019.0198
• Villani, C. (2009). Optimal Transport: Old and New. Springer. (Cited as [108] for Theorems 1 and 2.)
• Smith, J. E., & Winkler, R. L. (2006). The optimizer's curse: Skepticism and postdecision surprise in decision analysis. Management Science, 52(3), 311–322. https://doi.org/10.1287/mnsc.1050.0451
• Gao, R., & Kleywegt, A. J. (2016). Distributionally Robust Stochastic Optimization with Wasserstein Distance. arXiv:1604.02199.
• Blanchet, J., & Murthy, K. (2019). Quantifying Distributional Model Risk via Optimal Transport. Mathematics of Operations Research, 44(2), 565–600. https://doi.org/10.1287/moor.2018.0936

Motivation

A Markov decision process (MDP) chooses a decision in every period of a dynamic system whose state evolves stochastically in response to the decision, so as to maximize expected discounted return. Firms use this model for inventory, pricing, and advertising decisions that respond to a randomly evolving demand state; engineers use it for maintaining or replacing equipment that degrades stochastically. A recurring practical question is qualitative rather than numerical: does the optimal decision increase with the state — should a firm price higher after a period of strong sales, or replace a machine sooner the worse its observed condition — without having to solve the dynamic program numerically for every instance of the model? Topkis's Chapter 3, Section 3.9 (Topkis, Supermodularity and Complementarity, 2011, building on Topkis [1968]) answers this by isolating the lattice-theoretic structure — supermodularity of the return function and of the transition law — under which monotone optimal policies are guaranteed on structural grounds alone. A closely related but logically independent question was studied earlier by Lehmann [1955], who characterized when a family of distributions is stochastically increasing in a parameter; Topkis generalizes Lehmann's characterization to any property of the parameter dependence whose defining set of functions forms a closed convex cone, of which stochastic monotonicity, supermodularity, and convexity are three instances (Theorem 3.9.1, Corollary 3.9.1). Serfozo [1976] independently develops related conditions for partially observed Markov decision processes, and Amir [1996] and Amir, Mirman, and Perkins [1991] give analogous monotonicity results for other classes of dynamic programming models.

Setting

Fix a finite planning horizon of $k$ periods, $i = 1, \dots, k$. In period $i$ the state $t$ ranges over a set $T_i \subseteq \mathbb{R}^m$; given state $t$, the decision $x$ is restricted to a finite, nonempty set $X_{t,i} \subseteq \mathbb{R}^n$ (finiteness guarantees that an optimal decision always exists — no continuity or compactness argument is used). Write $S_i = \{(x,t) : t \in T_i,\, x \in X_{t,i}\}$ for the set of admissible (decision, state) pairs in period $i$. The (bounded) expected net return of choosing decision $x$ in state $t$, period $i$, is $r_i(x,t)$. A discount rate $\beta \in [0,1]$ gives $\gamma = 1/(1+\beta)$, the value in period $i$ of one unit of return in period $i+1$. Given decision $x$, state $t$, and period $i$, the state $w$ of period $i+1$ is drawn from a distribution $F(x,t,i,\cdot)$ on $\mathbb{R}^m$.

The optimal-value function $f_i(t)$ (present value of acting optimally from state $t$, period $i$, onward) and the decision-value function $g_i(x,t)$ (present value of choosing $x$ in state $t$, period $i$, then acting optimally thereafter) are defined by backward induction from period $k$:

A subset $S$ of a Euclidean space is increasing if it is upward closed under the coordinatewise order. A family of distributions $\{F(a,\cdot) : a \in D\}$ indexed by a parameter $a$ is stochastically increasing on $D$ if the probability $\int_S dF(a,w)$ of every increasing set $S$ is a monotone (non-decreasing) function of $a$ on $D$; when $D$ is a sublattice, the family is stochastically supermodular on $D$ if that same probability is a supermodular function of $a$ on $D$. A real-valued function $\varphi$ on a lattice is supermodular on a set $D$ if $\varphi(a_1) + \varphi(a_2) \le \varphi(a_1 \vee a_2) + \varphi(a_1 \wedge a_2)$ for all $a_1, a_2 \in D$ — the mission series' shared notion, defined once in chunk 02-monotonicity and reused here as Supermodularity.Monotonicity.SupermodularOn.

Formalization targets

Goal — Theorem 3.9.2 (monotone optimal policies)

together with the existence of a greatest and a least optimal decision at every state, each increasing in the state, in every period $i$ — under the hypotheses that $S_i$ is a sublattice of $\mathbb{R}^{n+m}$, $X_{t,i}$ is expanding in $t$, $r_i$ is increasing in $t$ (on sections) and jointly supermodular in $(x,t)$, and $F(x,t,i,\cdot)$ is stochastically increasing in $t$ (on sections) and stochastically jointly supermodular in $(x,t)$, for every period $i$.

This is the weakest of the targets that is still worth stating on its own: it packages four related conclusions (parts (a)–(d) of Theorem 3.9.2) that share one hypothesis set, rather than isolating just the headline monotone-decision claim, because the book's own proof derives all four together and a solver attacking part (c) or (d) needs part (a) and (b) established first.

Supporting milestones

• Lemma 3.9.4: under the monotonicity half of the goal's hypotheses alone (no supermodularity), $f_i(t)$ is increasing in $t$ for every period $i$. This is the induction Theorem 3.9.2 reuses and strengthens.
• Corollary 3.9.1(b): on a sublattice $T$, a family of distributions is stochastically supermodular in $t$ iff $\int h(w)\,dF(t,w)$ is supermodular in $t$ for every increasing $h$. This is what lets the goal's hypothesis "$F(x,t,i,\cdot)$ stochastically supermodular in $(x,t)$" be converted into "$\int f_{i+1}(w)\,dF(x,t,i,w)$ supermodular in $(x,t)$", the step that feeds $g_i$'s supermodularity.
• Theorem 3.9.1: the general closed-convex-cone characterization of which Corollary 3.9.1(b) is the supermodularity instance (monotonicity and convexity are the other two instances, not formalized here since the goal's proof only needs the supermodularity case).

Significance

The result gives a purely structural sufficient condition — no smoothness, convexity of the decision set, or specific functional form — for monotone comparative statics in dynamic optimization: whenever the one-period return and the state transition are individually monotone and jointly supermodular in (decision, state), so is the whole multi-period value function, and so are the optimal decisions. Textbook applications include optimal advertising that decreases with prior-period sales, optimal pricing that increases with prior-period sales, and optimal maintenance of a deteriorating system, none of which need to be re-derived from scratch once the structural hypotheses are checked for the specific return and transition functions at hand.

Formalizing it contributes a genuinely new layer to the mission series and, per the paper's own triage (substrate.md), to the platform's application of Mathlib's probability-kernel infrastructure: a finite-horizon MDP with a Lebesgue–Stieltjes-style transition law and its associated stochastic-dominance vocabulary (stochastically increasing / stochastically supermodular families of distributions) did not previously exist on the platform or in this mission series, and both are reusable beyond this mission by any future formalization of dynamic programming under uncertainty. The proof itself is not open — Topkis [2011] (unchanged from the 1968/1998 original) gives a complete, elementary backward-induction argument — so what this mission produces is the formalization of a known, structurally distinctive proof technique, not a new mathematical result.

Difficulty

The naive argument — "supermodularity of $r_i$ plus supermodularity of the transition kernel obviously gives supermodularity of $g_i$" — breaks exactly at the integral: supermodularity of $(x,t) \mapsto F(x,t,i,\cdot)$ is a statement about the whole family of distributions, not about a single number, so "the transition is jointly supermodular" has to be unpacked into "the probability of every increasing set is jointly supermodular in $(x,t)$" before it says anything about $\int f_{i+1}(w)\,dF(x,t,i,w)$ for a specific function $f_{i+1}$. Corollary 3.9.1(b) is exactly the step that licenses this unpacking, and it is not free: it needs Theorem 3.9.1's closed-convex-cone argument (approximating $f_{i+1}$ from below by increasing step functions and invoking monotone convergence), not a pointwise argument on $r_i$ and $F$ separately. A second place the naive argument fails is at the constraint sets: because $X_{t,i}$ only grows with $t$ rather than being fixed, monotonicity of $f_i$ (Lemma 3.9.4) needs its own induction combining that growth with monotonicity of $g_i$ — supermodularity of $g_i$ alone does not hand you monotonicity of the arg max without it.

Formalization scope

States and decisions are represented as Fin m → ℝ and Fin n → ℝ (finite-dimensional Euclidean coordinate spaces with the coordinatewise/product order, matching the book's own restriction to $\mathbb{R}^m$ and $\mathbb{R}^n$ — no abstract lattice is used where the book itself specializes). Distributions are represented as MeasureTheory.Measure on the relevant coordinate space, with IsProbabilityMeasure supplied explicitly wherever a stochastic-dominance hypothesis is used (the probability of a set is read off as (μ S).toReal, which is only faithful to $\int_S dF$ when μ is a probability measure — an unconstrained arbitrary measure would let .toReal collapse an infinite value to $0$ and make the hypothesis trivially satisfiable, a formalization this mission rules out). Integrands h are required integrable against every measure in the family wherever an integral is asserted to lie in a set V, since the Bochner integral of a non-integrable function is definitionally 0 in Lean/Mathlib and would otherwise make Theorem 3.9.1 and Corollary 3.9.1(b) trivially true. Decision sets $X_{t,i}$ are finite (Finset, not merely a bounded or compact Set) and required nonempty exactly where the book assumes it: this finiteness, not any compactness or semicontinuity argument, is what guarantees an optimal decision exists, and dropping it would silently substitute Chapter 2's compactness-based existence machinery for the different argument this section actually uses. The optimal-value and decision-value functions $f_i, g_i$ are represented as any functions satisfying the two backward-recursion equations that define them, rather than being constructed by explicit backward recursion in Lean; since the equations determine $f_i, g_i$ uniquely from $r_i$ and $F$, this is a faithful reading of "define $f_i, g_i$ by (3.9.1) and (3.9.2)," not a weakening of the theorem. The goal's part (c) is stated using the mission series' InducedSetOrder (the Veinott/strong set order, chunk 01-lattices) and part (d) as the existence of two selection functions (greatest, least optimal decision), each monotone in the state — matching the book's "there is a greatest (least) optimal decision ... and this greatest (least) optimal decision is increasing in $t$." The infinite-horizon stationary extension that the book gives immediately after Theorem 3.9.2 (relying on an unproved citation to Blackwell [1965]) is out of scope for this mission.

Reusable infrastructure: the StochasticallyIncreasingOn/StochasticallySupermodularOn definitions are parametric in the ambient preorder/lattice and in the measure's target dimension, so a future mission on stochastic convexity (Corollary 3.9.1(c), not formalized here) or on Topkis's §3.10 stochastic inventory model (which explicitly depends on §3.9, per the book's own reading-order note) can reuse them without modification. Contributions extending this mission to the infinite-horizon case, or completing Corollary 3.9.1's monotonicity and convexity halves, are welcome.

Selected references

• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 2011 (unchanged from the 1998 original), Chapter 3, Section 3.9. DOI: 10.1515/9781400822539.
• D. M. Topkis, "Ordered Optimal Solutions," PhD dissertation / working paper, Stanford University, 1968 (the original source for this section's results).
• E. L. Lehmann, "Ordered Families of Distributions," Annals of Mathematical Statistics 26(3), 1955, pp. 399–419. https://doi.org/10.1214/aoms/1177728487
• R. Serfozo, "Monotone Optimal Policies for Markov Decision Processes," Mathematical Programming Study 6, 1976, pp. 202–215.
• R. Amir, "Sensitivity Analysis of Multisector Optimal Economic Dynamics," Journal of Mathematical Economics 25(1), 1996, pp. 123–141.
• R. Amir, L. J. Mirman, and W. R. Perkins, "One-Sector Nonclassical Optimal Growth: Optimality Conditions and Comparative Dynamics," International Economic Review 32(3), 1991, pp. 625–644.
• D. Blackwell, "Discounted Dynamic Programming," Annals of Mathematical Statistics 36(1), 1965, pp. 226–235. https://doi.org/10.1214/aoms/1177700285

Motivation

Every method in Chapters 2-4 of this series solves a projection or proximal subproblem at every step — a Euclidean projection, or a Bregman-divergence prox-mapping — which can itself be as hard as the original problem when $X$ is a complicated feasible set (a spectrahedron, a flow polytope, a matroid base polytope). The conditional gradient method (Frank & Wolfe, 1956) sidesteps this entirely: instead of a projection, each step calls a linear optimization (LO) oracle — minimize a linear function over $X$ — which is frequently far cheaper (over a spectrahedron, this reduces to a single eigenvector computation; over many combinatorial polytopes, to a greedy algorithm). This is the origin of the modern "projection-free" family of optimization methods widely used at the scale where projections are the bottleneck.

Setting

Fix a nonempty compact convex set $X$ in a real normed space $E$ and a convex $f:X\to \mathbb R$ with $L$-Lipschitz gradient (Eq. (7.1.4)): $\|f'(x)-f'(y)\|_*\le L\|x-y\|$. The classic conditional gradient (CndG) method, Algorithm 7.1, sets $x_0\in X$, $y_0=x_0$, and for $k=1,2,\dots$: calls the LO oracle $x_k\in\arg\min_{z\in X}\langle f'(y_{k-1}),z\rangle$, then sets $y_k=(1-\alpha_k)y_{k-1}+\alpha_kx_k$ for a stepsize $\alpha_k\in[0,1]$, either the fixed schedule $\alpha_k=2/(k+1)$ (Eq. (7.1.9)) or exact line search (Eq. (7.1.10)).

Section 7.1.1.2 extends this to bilinear saddle-point problems, where $f$ itself is the (generally nonsmooth) function $f(x)=\max_{y\in Y}\{\langle Ax,y\rangle-\hat f(y)\}$ (Eq. (7.1.5)) for a compact convex $Y$ and linear operator $A$. Since $f$ is nonsmooth, the method is applied instead to a family of smooth approximations $f_\eta$ built from a strongly convex $\omega$ on $Y$ (Eq. (7.1.21)-(7.1.23)), with the smoothing parameter $\eta_k$ allowed to vary across iterations rather than being fixed in advance.

Formalization targets

Goal — Theorem 7.1

Supporting milestones, in attack order

• Lemma 7.1: the smoothed objective family $f_\eta$ is monotone nondecreasing in $\eta\ge0$ — the one-line fact ($V(y)-D_Y^2\le0$ pointwise) that licenses a variable, decreasing smoothing schedule $\eta_k$ rather than a schedule fixed in advance from knowledge of the target accuracy.
• Theorem 7.2: the saddle-point counterpart of the goal theorem, running the same CndG algorithm on the smoothed gradients $f_{\eta_k}'$ instead of $f'$ directly, with the explicit rate $f(y_k)-f^*\le\frac{2}{k(k+1)}\sum_{i=1}^k[i\eta_iD_Y^2+\frac{\|A\|^2}{\sigma_v\eta_i} \|x_i-y_{i-1}\|^2]$.

Every constant here is exactly the book's; the goal theorem's bound is left in terms of the actual step distances $\sum\|x_i-y_{i-1}\|^2$, not a diameter-based simplification (see Difficulty).

Significance

This mission formalizes the founding convergence result of the entire projection-free family (Frank-Wolfe methods), which has become central to large-scale machine learning precisely because its per-iteration cost can be orders of magnitude below that of a projection-based method on structured feasible sets. Theorem 7.1's specific form — a rate depending on the realized step distances rather than a fixed diameter — is also the more informative, tighter statement (the book's own remarks show it recovers the classical diameter-based $O(LD_X^2/\varepsilon)$ complexity as a corollary, but also explains why the rate can be much better in practice when the iterates settle near an extreme point).

No result matching conditional gradient / Frank-Wolfe methods exists on the platform as of 2026-09-18 (q=Frank-Wolfe and q=conditional gradient both return zero hits — see Prior art in MODERATION_NOTES.md).

Difficulty

The chief formalization difficulty is representing "with the stepsize policy in (7.1.9) or (7.1.10)" faithfully without either restricting to one policy (weaker than the book's stated theorem) or introducing an awkward disjunction of two separate algorithm definitions. The book's own proof resolves this by a single observation used for both policies at once: $f(y_k)\le f(\tilde y_k)$ for $\tilde y_k$ the point the fixed schedule $\gamma_k=2/(k+1)$ would have produced — trivially by equality under (7.1.9), or because $y_k$ is chosen to minimize $f$ over the entire line segment under (7.1.10), of which $\tilde y_k$ is one point. This mission's hyk_le hypothesis states exactly this shared consequence, which is genuinely what the proof uses and genuinely covers both policies, rather than picking one arbitrarily.

A second difficulty is not collapsing $\sum_{i=1}^k\|x_i-y_{i-1}\|^2$ into a diameter bound $kD_X^2$ inside the milestone itself — the book's own remarks perform that substitution as a separate, weaker corollary (Eq. (7.1.19)) after stating Theorem 7.1 in its sharper form; folding the substitution into the goal statement itself would silently prove a different, weaker theorem.

Formalization scope

conditional_gradient_rate and saddle_point_cndg_rate state the LO oracle's exactness (x k ∈ Argmin_{z∈X}⟨fGrad(y(k-1)),z⟩) as a pointwise hypothesis rather than deriving it from IsCompact X via an existence lemma — matching the pointwise-hypothesis convention this series uses throughout for argmin-defined algorithmic steps (chunk 03-deterministic's mirror-descent updates, chunk 04-stochastic's stochastic mirror-descent update). X compact convex is still included as a hypothesis, matching the book's own standing assumption on the problem class, even though it is not itself needed to derive the stated conclusion from the other hypotheses.

smoothed_objective_monotone and saddle_point_cndg_rate realize $f_\eta$/$f$ via sSup of the image of $Y$ under the pointwise saddle-point objective, matching the book's own max_{y∈Y}{...} definition (Eq. (7.1.5), (7.1.23)) directly rather than introducing a separate Def_ file for a "bilinear saddle-point objective" structure — no other item in this mission reuses that definition verbatim, so per this series' convention (no shared substrate bundled into a structure unless reused), it is inlined at each use.

A trivializing formalization this mission rules out: stating the LO oracle via an $\varepsilon$-approximate minimizer ((fGrad (y(k-1))) (x k) ≤ (fGrad (y(k-1))) z + ε for some ε) rather than an exact one — this is explicitly a different, weaker algorithm the book does not analyze in Theorem 7.1/7.2 (the book studies approximate LO oracles separately, later in the chapter, not selected here).

Left out of scope, for time: Theorem 7.7 (the matching lower complexity bound for LO-oracle methods, Eq. (7.1.60)) — formalizing it faithfully requires first modeling the abstract class of "LCP methods" (any algorithm restricted to LO-oracle calls) as a universally-quantified object, a substantially different and more involved formalization task than the two upper-bound convergence theorems selected here; named per Hard Rule 7 rather than approximated. The d(x)=\sum x_i\log x_i entropy-smoothing remark and the primal/primal-dual averaging CndG variants (§7.1.2, not covered by this mission's page range) are likewise not attempted.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 7, §7.1.1. https://doi.org/10.1007/978-3-030-39568-1
• M. Frank, P. Wolfe, "An algorithm for quadratic programming," Naval Research Logistics Quarterly, 3(1-2), 1956, pp. 95-110.
• M. Jaggi, "Revisiting Frank-Wolfe: projection-free sparse convex optimization," ICML, 2013 (the modern machine-learning revival of the method).

Motivation

Two-stage stochastic linear programming with recourse models a decision made before uncertainty resolves (the first-stage variables $x$) followed by a corrective decision made after (the second-stage, or recourse, variables $y$). Solving such a program means minimizing $c^{\mathsf T}x + Q(x)$, where $Q(x)$ is the expected cost of the best recourse action given $x$ -- an object defined only implicitly, as the value of an embedded linear program that must be solved (or bounded) for every realization of the uncertain data. Before any algorithm for this problem can be justified -- the L-shaped method, stochastic decomposition, scenario decomposition, all developed in later chapters of Birge & Louveaux, Introduction to Stochastic Programming (Springer, 2011) -- one needs to know that $Q$ is well-behaved enough to optimize over at all: that the feasible region is closed and convex, that $Q$ itself is a finite, Lipschitz, convex function on it, that an optimal solution is actually attained rather than only approached in the limit, and finally what an optimality condition for the resulting nonsmooth convex program even looks like. This mission formalizes exactly that foundational layer, Chapter 3, Section 3.1 of the book.

Setting

Fix natural numbers $n_1, n_2, m_1, m_2$ and a finite scenario count $K$. A two-stage recourse instance consists of first-stage data $A \in \mathbb{R}^{m_1 \times n_1}$, $b \in \mathbb{R}^{m_1}$, $c \in \mathbb{R}^{n_1}$, a fixed recourse matrix $W \in \mathbb{R}^{m_2 \times n_2}$, and, for each scenario $k = 1,\dots,K$, a cost vector $q_k \in \mathbb{R}^{n_2}$, a right-hand side $h_k \in \mathbb{R}^{m_2}$, a technology matrix $T_k \in \mathbb{R}^{m_2 \times n_1}$, and a probability $p_k \ge 0$ with $\sum_k p_k = 1$ (Eq. (1.1)). The first-stage feasible region is $K_1 = \{x \mid Ax = b,\ x \ge 0\}$.

For a fixed $x$ and scenario $k$, the second-stage value is

(Eq. (1.6)), taken as an extended real: $+\infty$ if no feasible $y$ exists, $-\infty$ if the inner program is unbounded below. The expected recourse value is $Q(x) = \sum_k p_k\, Q(x,\xi_k)$ (Eq. (1.3)), combined so that $+\infty + (-\infty) = +\infty$ -- the book's own convention (p. 109): infeasibility in one scenario is treated as fatal even if another scenario is unboundedly favorable. The second-stage feasibility set is $K_2 = \{x \mid Q(x) < \infty\}$, and the deterministic-equivalent objective is $z(x) = c^{\mathsf T}x + Q(x)$ (Eq. (1.2)). For $x$ with $Q(x)$ finite, the subdifferential $\partial Q(x)$ is the set of $\eta$ satisfying $Q(x) + \eta^{\mathsf T}(y-x) \le Q(y)$ for every $y$ (p. 115).

A simple-recourse instance is the special case $W = [I,-I]$: the recourse cost splits as $q = (q^+,q^-)$, and $Q(x)$ decomposes componentwise via the closed form of Eq. (1.9)-(1.10) using the (left- and right-limit) distribution functions $F_i^-, F_i^+$ of each $h_i$.

Formalization targets

Goal -- Chapter 3, Theorem 9 (p. 116)

given that (1.2) has a finite optimal value. This is the KKT-style necessary and sufficient optimality condition for the two-stage recourse LP, and the weakest of the mission's targets in the sense that everything else supports it: convexity and finiteness of $Q$ (Theorem 6) are what make the left-to-right implication meaningful, closedness/convexity of $K_2$ (Theorem 5) makes the feasible region well-posed, and attainment (Theorem 8) is what makes "$x^*$ is optimal" a statement about a point that exists rather than an infimum that may not be reached.

Supporting milestones

• Theorem 5(a) (p. 111): $K_2$ is closed and convex.
• Theorem 6(a) (p. 112): $Q$ is finite on $K_2$, and Lipschitzian and convex there.
• Theorem 8 (p. 115): under boundedness of $K_1 \cap K_2$ or eventual linearity of $Q$ along recession directions, a finite optimal value is attained.
• Corollary 10 (p. 116): Theorem 9 specialized to simple recourse, with $\partial Q(x^*)$ replaced by its explicit componentwise description.

Significance

Theorem 9 is the hinge on which the rest of the book's algorithmic chapters turn. The L-shaped method (Chapter 5) is a cutting-plane scheme whose cuts are literally elements of $\partial Q(x)$; stochastic decomposition and sampling-based methods use the same subdifferential structure with estimated cuts; the differentiable specialization (Eq. (1.14), $c + \nabla Q(x^*) = A^{\mathsf T}\lambda^* + \mu^*$) underlies nonlinear-programming approaches to the smooth case. None of this is meaningful without first knowing $Q$ is convex, finite where it needs to be, and that a minimizer exists to characterize. Formalizing this mission's four milestones from the actual definition of $Q$ as an embedded linear program's value -- rather than assuming these properties -- is exactly the content the book itself proves (or, for Theorem 6, explicitly cites to Wets [1972] and Kall [1976] rather than proving); this mission asks for genuine Lean proofs of Theorems 5, 8, 9 and Corollary 10 from the LP structure of $Q$, and records Theorem 6 as a stated (not re-derived) input, matching the book's own presentation.

Difficulty

The obvious shortcut is to treat $Q$ as an opaque convex function and apply a textbook convex-KKT theorem off the shelf. This fails to capture what Theorem 9 actually is: a statement about the specific function $Q(x) = \sum_k p_k \min_y\{q_k^{\mathsf T}y \mid Wy = h_k - T_k x,\ y \ge 0\}$, built from finitely many parametric linear programs, each of which can be infeasible ($Q(x,\xi_k) = +\infty$) or unbounded ($Q(x,\xi_k) = -\infty$) depending on $x$. Convexity of $Q$ must come from convexity of the value function of a parametric LP in its right-hand side (the book's Theorem 2 argument: a convex combination of optimal solutions at two right-hand sides is feasible, hence suboptimal, at the combined right-hand side) -- not from an assumed hypothesis. Handling $\pm\infty$ correctly is a second, easy-to-miss source of error: the book fixes an explicit, non-default convention ($+\infty$ dominates $-\infty$) for combining per-scenario values, the opposite of the convention Mathlib's own extended-real arithmetic uses, so any formalization that reaches for EReal's built-in addition to aggregate $Q$ silently states a different theorem. Theorem 8's attainment condition is a genuine existence result, not an automatic consequence of convexity: continuity alone does not give attainment on an unbounded feasible region, and the book's own counterexample (Eq. (1.11), a negative-exponential tail with infimum $0$ attained by no finite $x$) shows the boundedness/recession hypotheses are load-bearing.

Formalization scope

The scenario set is modeled as Fin K, a finite discrete random variable, matching Section 3.1b's development; under this model "$\xi$ has finite second moments" (the standing hypothesis of Theorems 4-11 in the general, possibly-continuous case) holds automatically and so does not appear as a separate hypothesis anywhere in this mission. Q(x,\xi_k) is defined as an EReal via sInf of the second-stage LP's feasible objective values -- sInf of the empty set is ⊤, and of a set unbounded below is ⊥ -- and is genuinely derived from that inner minimization rather than assumed convex; this rules out the chapter's trivializing formalization, which the paper-level triage explicitly warns against: taking Q(x) as an opaque convex-function hypothesis instead of deriving its properties from the inner LP's structure. Aggregating the $K$ per-scenario values into $Q(x)$ uses a bespoke bookAdd operation implementing the book's stated convention $+\infty+(-\infty)=+\infty$, since Mathlib's EReal addition is defined with the opposite convention ($\bot+\top=\top+\bot=\bot$). $\partial Q(x)$ is the ordinary subgradient-inequality set for this extended-real-valued function.

Theorem 8's condition (b) is stated with the book's own quantifier structure: the threshold $\bar\lambda$ and the recession value depend on the point $x$ and direction $v$ exactly as written, with no strengthening. Theorem 6(a)'s Lipschitz bound is stated, not derived -- the book itself cites it to Wets [1972] and Kall [1976] without proof -- so a faithful Lean proof of that milestone is expected to remain out of scope for this mission. Corollary 10 similarly takes the closed form of $\partial Q_i(x)$ from Eq. (1.10) as a hypothesis on an abstract $Q$, matching how the book itself uses (1.10) as an already-established fact rather than re-deriving it from the second-stage LP in the corollary's own proof. Theorem 11's subdifferential-decomposition result ($\partial Q(x) = E_\omega[\partial Q(x,\xi(\omega))] + N(K_2,x)$) is deliberately left out of this mission's scope: it is not needed by Theorem 9's own proof, and its normal-cone term would require relatively-complete-recourse machinery this mission does not otherwise need. No prior-art match was found on the platform: VectorSpaceOpt.fenchel_duality and the Luenberger-derived VectorSpaceOpt.generalized_kuhn_tucker / kkt_complementary_slackness family use a differentiable (Gateaux-derivative) or conjugate-function KKT model over general normed spaces, not this chapter's finite-dimensional, possibly-nondifferentiable subgradient formulation over the specific polyhedral set $K_1$, so none is a faithful match and all items here are original drafts.

Selected references

• J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• R.J-B. Wets, "Programming Under Uncertainty: The Equivalent Convex Program," SIAM Journal on Applied Mathematics 14 (1966), 89-105 (Lipschitz continuity of the recourse function, cited by the book as Wets [1972] for the closely related result used in Theorem 6). https://doi.org/10.1137/0114008
• D.P. Walkup and R.J-B. Wets, "Stochastic Programs with Recourse," SIAM Journal on Applied Mathematics 15 (1967), 1299-1314 (finiteness of the recourse function and coincidence of the possibility and expectation feasibility sets, underlying Proposition 3 and Theorem 4). https://doi.org/10.1137/0115113

Motivation

The discrete-time Riccati equation is the central object of linear-quadratic optimal control — the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005, §4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of §4.2 develops K-convexity, the analytical engine behind Scarf's optimality of $(s,S)$ inventory policies — a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.

Setting

Matrices $A \in \mathbb{R}^{n\times n}$, $B \in \mathbb{R}^{n\times m}$, $Q = C^\top C \succeq 0$, $R \succ 0$. The Riccati operator (BertsekasRiccatiMap)

$(A,B)$ is controllable if $[B, AB, \dots, A^{n-1}B]$ has rank $n$ (BertsekasControllablePair); $(A,C)$ is observable if $(A^\top, C^\top)$ is controllable (BertsekasObservablePair). Separately, $g : \mathbb{R} \to \mathbb{R}$ is $K$-convex (BertsekasKConvex, Def. 4.2.1) if $K + g(z+y) \ge g(y) + \tfrac{z}{b}(g(y) - g(y-b))$ for all $z \ge 0$, $b > 0$, $y$.

Target

with $L = -(B^\top P B + R)^{-1} B^\top P A$ — BertsekasDP.riccati_convergence_stability (goal). Milestones: Lemma 4.2.1(a)–(d) (kconvex_of_convex, kconvex_combination, kconvex_expectation, kconvex_sS_structure), culminating in the $(s,S)$ structure theorem for continuous coercive $K$-convex functions.

Significance

The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of $(s,S)$-policy optimality. All results are classical and proved in the book; the formal work is new.

Difficulty

The Riccati proof interleaves monotonicity of $F$ on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument — several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing $A$ fails: nothing is symmetric about $A + BL$. For Lemma 4.2.1(d), the difficulty is that $g$ is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.

Formalization scope

Real matrices over Fin n; Matrix.PosSemidef/PosDef; matrix inverse is Mathlib's total inverse (zero on singular input — harmless here since $B^\top P B + R \succ 0$ along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via spectrum ℂ of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real $K$; note $K \ge 0$ is forced whenever it is satisfiable ($z = 0$), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 4.4.1, Def. 4.1.1, §4.2, Lemma 4.2.1.) http://www.athenasc.com/dpbook.html
• R. E. Kalman, Contributions to the theory of optimal control, Bol. Soc. Mat. Mexicana 5 (1960), 102–119.
• H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in Mathematical Methods in the Social Sciences, Stanford Univ. Press, 1960.

Two quadratic functions can be compared losslessly. The S-procedure says that, when the constraint is strictly feasible, the implication

holds if and only if a single nonnegative multiplier certifies it as a matrix inequality, $\lambda \begin{bmatrix} F_1 & g_1 \\ g_1^{T} & h_1\end{bmatrix} \succeq \begin{bmatrix} F_2 & g_2 \\ g_2^{T} & h_2\end{bmatrix}$ for some $\lambda \ge 0$. It is a cornerstone of control theory, trust-region methods and robust optimization, and a rare case in which a nonconvex problem has zero duality gap. The route runs through the theory this mission builds from Boyd & Vandenberghe §5.8–5.9 and Appendix B: strong alternatives for convex inequality systems, cone-program strong duality under a generalized Slater condition, semidefinite programming duality, the LMI theorems of alternatives, and the hidden convexity of the joint range of two quadratic forms.

Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's Convex Optimization (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.

Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not entangled — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.

How much flow can be sent from a source $s$ to a sink $t$ through a network with arc capacities $u_{ij}\in(0,\infty]$ — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination $\mathbf{f}=\sum_i a_i\mathbf{f}^i$ of simple circulations with only forward arcs, with integer $a_i$ when $\mathbf{f}$ is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ($\max b_s$ s.t. $\mathbf{A}\mathbf{f}=\mathbf{b}$, $b_t=-b_s$, $b_i=0$ for $i\ne s,t$, $0\le\mathbf{f}\le\mathbf{u}$), defines augmenting paths (Definition 7.2: $f_{ij}<u_{ij}$ on forward arcs, $f_{ij}>0$ on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:

(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;

(b) the value of the maximum flow equals the minimum cut capacity

— the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).

Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time $\tau$ and a recommendation must be sound (wrong with probability at most $\delta$) while minimizing $\mathbb{E}[\tau]$. The information-theoretic complexity is $c^*(\nu)^{-1} = \sup_{\alpha\in\mathcal{P}_{k-1}} \inf_{\nu'\in\mathcal{E}_{alt}(\nu)} \sum_i \alpha_i D(\nu_i, \nu_i')$: every sound strategy needs $\mathbb{E}[\tau] \ge c^*(\nu)\log\frac{1}{4\delta}$, and the Track-and-Stop algorithm — the goal theorem — achieves $\lim_{\delta\to 0} \mathbb{E}[\tau]/\log(1/\delta) = c^*(\nu)$ exactly. The mission also covers the fixed-budget counterpart, sequential halving.

When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of $[0,1]$, and the correct exponential rate is governed by the binary relative entropy $d(p,q) = p\log\frac{p}{q} + (1-p)\log\frac{1-p}{1-q}$ rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of $d$. The goal theorem shows KL-UCB attains

— asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.

Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy $D(P,Q)$, and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event $A$, $P(A) + Q(A^c) \ge \frac{1}{2}\exp(-D(P,Q))$ — no test can distinguish $P$ from $Q$ with total error probability below $\frac{1}{2}e^{-D(P,Q)}$. This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality $\int p \wedge q \ge \frac{1}{2}(\int\sqrt{pq})^2$), Pinsker's inequality $\delta(P,Q) \le \sqrt{D(P,Q)/2}$, and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.

Why the two-item periodic JRP is hard

The joint replenishment problem (JRP) is the multi-item extension of the economic order quantity (EOQ) model. Each item is reordered periodically and pays its own ordering and holding costs, and a joint ordering cost is shared by items ordered at the same time. Before this work no hardness result was known for the periodic JRP (p. 10), even though no exact polynomial-time algorithm was known either (Schulz and Telha, arXiv:2007.09045; Operations Research, 2024, as Integer Factorization: Why Two-Item Joint Replenishment Is Hard).

The paper explains this through number theory. In the periodic JRP the joint cost is incurred every $\gcd(q_1, q_2)$ periods, so the objective contains a greatest common divisor of the decision variables. The paper's Theorem 2 states that, assuming the Riemann hypothesis, the two-item periodic JRP is NP-hard under randomized reductions. The proof composes two reductions:

• Shor's reduction from Partition to RangeDivisor ("does $M$ have a divisor in $[L, U]$?"), given in the paper's appendix and based on Shor (2011); this is where the Riemann hypothesis enters;
• a reduction from RangeDivisor to the two-item periodic JRP, whose correctness is Lemma 3 (pp. 13–14).

This mission formalizes Lemma 3. Mission 4 of this series formalizes the Partition half; missions 1 and 2 formalize the integer-factorization reductions behind Theorem 1.

Setting

A period is a positive integer $q$. An item with ordering cost $K$ and holding cost $H$ costs

per unit time. The two-item periodic JRP (objective (3), p. 10) minimizes, over $q_1, q_2 \in \mathbb{Z}_+$,

As a decision problem (p. 13), it asks whether some $(q_1, q_2)$ has cost at most a threshold $z$.

An instance of RangeDivisor (p. 12) is a triple of integers $M \ge U \ge L > 0$ satisfying

it is a yes-instance when $M$ has a divisor $q$ with $L \le q \le U$.

Given such a triple, the instance $\mathrm{JRP}_{M,U,L}$ sets

and the threshold is $z_{M,L,U} = L + U + 2M^2(M+1)$, where $2M^2(M+1) = \mathrm{EOQ}_{K_2,H_2}(M)$. Once item 2 is fixed at $q_2 = M$, item 1 solves problem (5):

In Lean these objects are JRPHard.Aperiodic.eoq, JRPHard.Periodic.periodicCost, JRPHard.Periodic.coefK2, JRPHard.Periodic.coefH2 (shared with missions 1 and 2), and IsRangeDivisorInstance, HasDivisorIn, coefK0, rangeCost, threshold, obj5 and fConv in the namespace JRPHard.RangeDiv.

Formalization targets

Goal: Lemma 3

For every RangeDivisor instance $(M, L, U)$,

Milestones (the steps of the proof, pp. 14–15)

1. Item 2 is pinned: every plan with $q_2 \ne M$ costs more than $z_{M,L,U}$.
2. $f(q) = LU/q + q$ is a lower bound on problem (5)'s objective, $f(L) = f(U) = L + U$, and $f$ is minimized at $\sqrt{LU}$.
3. $\gcd(q, M) \ne q \Rightarrow \gcd(q, M) \le q/2$.
4. If $\gcd(q, M) \ne q$, the objective of (5) at $q$ is at least $2\sqrt{2LU} > L + U$.
5. A divisor $q \in [L, U]$ of $M$ has objective at most $L + U$.
6. A period with objective at most $L + U$ divides $M$ and lies in $[L, U]$.

Significance

Lemma 3 is the step that carries hardness from number theory to inventory theory. With Shor's result it shows that, under the Riemann hypothesis, no polynomial-time exact algorithm for the two-item periodic JRP exists unless NP problems can be solved in randomized polynomial time. The paper concludes (p. 15) that no algorithm for the two-item problem may be simultaneously exact and polynomial on all inputs, so some concession, such as heuristics, must be made.

The result is proved in the paper; it has not been machine-checked. The mission produces a checked statement of the reduction's correctness with every coefficient explicit, and it corrects two imprecisions in the printed lemma (the threshold and the unspecified "sufficiently large" coefficients of item 2; see below). The objects (eoq, periodicCost) are the same ones used in mission 2 of this series.

Difficulty

Each step is elementary, but the statement mixes integer and real reasoning. The objective of (5) is not monotone or convex in $q$: its value jumps between $LU/q + q$ at divisors of $M$ and at least $2LU/q + q$ elsewhere. The argument must show that the gap between these two curves exceeds the window around $L + U$, and this is exactly what RangeDivisor's condition $L + U < 2\sqrt{2LU}$ provides. Without that condition a non-divisor can be cheaper than $L + U$ (for $L = 1$, $U = 100$, $M = 7$, the period $q = 14$ has objective $100/7 + 14 < 101$). The pinning of $q_2 = M$ also has to beat the slack $M + 2\sqrt{LU}$ against $L + U$, which is where $M \ge U$ is used.