Operations Research

Motivation

Every wireless network control algorithm — routing, scheduling, power control, admission control — is ultimately judged against one question: which traffic loads can it keep stable? Answering that question requires a precise, algorithm-independent notion of queueing stability under random arrivals and a randomly time-varying, possibly non-ergodic-looking channel. Tassiulas & Ephremides (1992) and Neely, Modiano & Rohrs (2005) developed the framework used throughout Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006): "strong stability" of a queue backlog process, defined purely through the time-averaged expected backlog, with no assumption that the arrival or service process is stationary, Markov, or even has a well-defined long-run average. The present mission formalizes the chapter's foundational single-queue results — the two structural facts every later network-wide capacity and control result in the book is built from.

Setting

A queue is described by three processes on slots $t=0,1,2,\dots$: an arrival process $A(t)$ (new bits admitted at the end of slot $t$), a service process $\mathrm{svc}(t)$ (the transmission rate offered during slot $t$), and the backlog $U(t)$, evolving by the queueing law

$$U(t+1)=\max[U(t)-\mathrm{svc}(t),0]+A(t).$$

The queue is strongly stable if its expected backlog has a bounded time average, $\limsup_{t\to\infty}\frac1t\sum_{\tau=0}^{t-1}\mathbb E\{U(\tau)\}<\infty$. An arrival process is admissible with rate $\lambda$ if (i) its time-average expected rate is $\lambda$, (ii) its second moment conditioned on the history is uniformly bounded, and (iii) for every $\delta>0$ there is an averaging window over which the conditional average rate exceeds $\lambda$ by at most $\delta$, uniformly in the starting time — a robust substitute for "the rate is exactly $\lambda$" that holds for i.i.d., Markov-modulated, and burstiness-constrained arrivals alike. A service process is admissible with rate $\mu$ analogously, with a deterministic pointwise upper bound in place of the second-moment condition. Both notions are formalized here on a filtered probability space $(\Omega,P,\mathcal F)$, with $\mathcal F(t)$ the history of slots $0,\dots,t-1$ exactly as the book's own $\mathcal H(t)$.

Formalization targets

Goal — Lemma 3.6 (Stability Conditions under Admissibility)

$$\text{(a) } \lambda\le\mu \text{ is necessary for strong stability;}\qquad \text{(b) } \lambda<\mu \text{ is sufficient for it.}$$

This is the chapter's central single-queue result: it converts the purely structural notion of strong stability into the one comparison — arrival rate versus service rate — that every later capacity-region and control-algorithm argument in the book reduces to.

Milestone — Lemma 3.3 (Necessary Condition for Strong Stability)

$$\text{if } U \text{ is strongly stable and } \mathbb E\{A(t)\}\le A_{\max}\ \forall t \text{ (or } \mathbb E\{\mathrm{svc}(t)-A(t)\}\le D_{\max}\ \forall t\text{), then } \lim_{t\to\infty}\mathbb E\{U(t)\}/t=0.$$

This is the elementary real-analysis fact — no admissibility, no probability beyond an already-given expectation sequence — that underlies the necessity half of Lemma 3.6's proof.

Significance

Strong stability and the admissibility framework are the load-bearing definitions of the entire book: every later chapter's algorithm-performance theorem (Chapter 4's backpressure throughput optimality, Chapter 5's utility-optimal Lyapunov drift bound, Chapter 6's energy-constrained control) is a theorem about when its induced queues are strongly stable, and every one of those proofs cites Lemma 3.6 (or its network generalization, Theorem 3.8's capacity region) as the final step converting a drift bound into a stability conclusion. Formalizing it fixes, once for the whole series, the precise real-analysis and conditional-expectation content of "arrival rate below service rate implies stability" that a Prove2Me solver would otherwise have to reconstruct from scratch for each downstream chapter.

Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for strong stability, admissible arrival process, Lyapunov drift, network capacity region — the one hit, a Foster–Lyapunov hitting-time bound for a finite-state MDP, is a scalar drift-to-a-target-state object, not a queue-backlog vector with no absorbing state, and is not reused). This mission is the first formalization of either result.

Difficulty

The obvious first idea for the sufficiency half (b) is to try to bound $\mathbb E\{U(t)\}$ directly by unrolling the queueing recursion and taking expectations termwise. This fails immediately: expectation does not commute with $\max(\cdot,0)$, so $\mathbb E\{U(t+1)\}\ne\max[\mathbb E\{U(t)\}-\mathbb E\{\mathrm{svc}(t)\},0]+\mathbb E\{A(t)\}$ in general — the whole reason admissibility's second-moment and $T$-slot averaging clauses exist is to control exactly this gap between the pathwise recursion and its expectation, via a genuine (non-elementary) drift argument. The necessity half (a) has the opposite trap: it is tempting to prove $\lambda\le\mu$ from a single-slot expectation inequality, but a queue can be strongly stable while $\mathbb E\{U(t)\}$ oscillates on any finite window, so the argument has to go through the time-averaged (Lemma 3.3) quantity, not a slot-by-slot one.

Formalization scope

Admissibility's conditional-expectation clauses are stated with Mathlib's Filtration ℕ and condExp (P[f | 𝓕 t]), following this platform's established idiom for martingale-difference hypotheses. Every conditional or plain expectation in a defining clause carries an explicit Integrable guard, because Mathlib's Bochner integral and condExp both silently default to 0 on a non-integrable function — without the guard, a process with an undefined or infinite second moment would satisfy admissibility vacuously, which is not the book's assumption (the book assumes these moments are finite; it never derives it). Lemma 3.3 is formalized directly on the real sequences representing $\mathbb E\{U(t)\}$, $\mathbb E\{A(t)\}$, $\mathbb E\{\mathrm{svc}(t)\}$ — exactly the content the book's own statement and proof use, with no further probabilistic structure, since the lemma's hypotheses and conclusion never mention anything but these expectations. Out of scope for this mission: the network-wide capacity region (Definition 3.7, Theorem 3.8, Corollaries 3.9-3.10) and the graph-family construction $\Gamma$/$\mathrm{Cl}\{\Gamma\}$ of §3.2-3.3. Faithfully formalizing "$\lambda$ is stably supportable by the network" requires embedding admissible-process realizations into a full multi-queue routing model, which is substantially heavier than either result formalized here and was left out entirely — per this series' faithfulness-over-coverage rule — rather than approximated by, e.g., dropping the second-moment or $T$-slot clauses of admissibility, which would silently change what "admissible" means. A trivializing formalization to rule out: defining AdmissibleArrival/AdmissibleService without the Integrable guards above would make Lemma 3.6 provable by choosing a non-integrable process, which is not the book's theorem.

Selected references

• Georgiadis, Neely & Tassiulas, Resource Allocation and Cross-Layer Control in Wireless Networks, Foundations and Trends in Networking, Vol. 1, No. 1 (2006), pp. 1-144. https://doi.org/10.1561/1300000001
• Tassiulas & Ephremides, "Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks", IEEE Transactions on Automatic Control, 37(12), 1992. https://doi.org/10.1109/9.182479
• Neely, Modiano & Rohrs, "Dynamic power allocation and routing for time-varying wireless networks", IEEE Journal on Selected Areas in Communications, 23(1), 2005. https://doi.org/10.1109/JSAC.2004.837349

Motivation

The group Steiner tree problem generalizes the ordinary Steiner tree problem: given a rooted tree and several groups of vertices, find a minimum-cost subtree that connects at least one vertex of each group to the root. It is a canonical instance of the generalized-connectivity family this survey studies in Chapter 11 — a family that also contains the online set-cover problem (Chapter 5 of this series) as a special case. Buchbinder and Naor's chapter shows how to convert the celebrated offline randomized-rounding algorithm of Garg, Konjevod and Ravi [56] into an online one, by imitating its per-edge coupling structure one iteration at a time as the online fractional solution (obtained from this survey's own Chapter 4 framework) evolves. This mission formalizes that online rounding scheme's three defining probabilistic guarantees and the resulting competitive-ratio theorem.

Setting

Fix a rooted tree T = (V, E, r) with non-negative edge costs c : E → ℝ, and k groups g₁, …, g_k ⊆ V, each request (r, gᵢ) arriving online. An online covering algorithm (from Chapter 4's framework, applied to the LP relaxation of this connectivity problem) maintains a monotonically increasing fractional weight w : E → ℝ on the edges, reinterpreted so that wₑ is the maximum flow that can be routed through e to any vertex of its subtree — a technical substitution needed so weights are monotone non-increasing along any root-to-leaf path, the property the rounding algorithm requires. At the end of each iteration in which some weights are augmented from w to w' = w + δ, the rounding algorithm processes every edge e with δₑ > 0, in topological order starting from the root, and randomly decides whether to add it to a growing random edge-cover C ⊆ E: deterministically, if w'ₑ > 1; via a single coin flip, if e is incident to the root or its parent edge's inclusion in C is already certain; via a coin flip conditional on the parent edge already being in C, otherwise. Because a coin is only ever flipped for a child once its parent is (or is already known to be) in C, C always induces a connected subtree containing the root.

Formalization targets

Theorem 11.4 (the goal, p. 231): there is a randomized online algorithm for the group Steiner problem in trees with competitive ratio O(log²n log k), where n is the number of leaves. It is built by running T independent trials of the rounding scheme in parallel and taking the union of the resulting covers, for T chosen (this mission's own explicit derivation — the book gives only the narrative "we run O(log k log N) independent trials... using simple probabilistic analysis") so that every group fails to be covered with probability at most 1/(2k), while the union's expected cost stays at T · log(n) · OPT.

Three milestones, in attack order, each stated exactly as the book states it (p. 230-231), with the book's own caveat "we state the main lemmas and omit the proofs" preserved — no in-source proof exists for any of the three beyond the algorithm's own description, so each is left sorry with no invented proof strategy:

• Lemma 11.1: at the end of an iteration, ℙ[e ∈ C] = w'ₑ for every edge, and ℙ[e ∈ C] = 1 whenever wₑ > 1 already.
• Lemma 11.2: the expected cost of C is at most ∑_{e∈T} cₑ w'ₑ (linearity of expectation applied to Lemma 11.1).
• Lemma 11.3: for a group g of size at most N with total routable flow wg ≥ 1, the probability some vertex of g is covered is Ω(1/log N).

Significance

This is the survey's most involved application of the primal-dual framework: unlike Chapters 5, 9, 10 and 13, which round a single scalar decision per online step, the group Steiner algorithm must couple an entire iteration's worth of edge decisions so that the resulting random set stays a connected subtree — the coin-flip probabilities in the Algorithm box are exactly the minimal adjustment needed to keep marginal probabilities matching the fractional solution while preserving this connectivity invariant online. No formal development of the group Steiner problem (online or offline) was found on the platform as of 2026-09-20; this mission is the first.

Difficulty

Two distinct obstacles. First, faithfully representing "the probability that e ∈ C" for an online, coupled random process without assuming its proof: the mission represents the algorithm's random cover as an abstract finite probability distribution RandomCover E and states each lemma as an implication from the Algorithm box's three coupling rules (transcribed as hypotheses on marginal and conditional probabilities) to the claimed marginal or expected-value conclusion — capturing exactly what the book asserts without proof, rather than either assuming the conclusion trivially or constructing a full multi-iteration coupled process (which the source's own "we omit the proofs" indicates is genuinely nontrivial, citing [56]). Second, Theorem 11.4's own competitive ratio is stated in the book only asymptotically, with a purely narrative derivation ("we run O(log k log N) independent trials... we get a competitive ratio of O(log n log k log N)... probability at least 1 − 1/k") and no displayed formula anywhere in the chapter. Per this series' explicit-constants rule, this mission supplies its own explicit closed form for the number of trials T and the resulting bounds via a standard Chernoff/union-bound argument applied to Lemma 11.3's constant α; this derivation is the mission's own (documented below), not a transcription, since none exists in the source to transcribe.

Formalization scope

RandomCover E is a finite pmf p : Finset E → ℝ (Finset E itself finite since E is Fintype), with marg, condProb and expectedCost/probHits derived from it by ordinary Finset sums — no measure theory, since the sample space is always finite. RoundedTree E bundles parent : E → Option E (e(p)) and a non-negative cost. Lemma 11.3's wg (the flow routable to a group's vertices simultaneously) is left as hypothesis-supplied data rather than defined via an explicit max-flow formalization, which this mission's scope does not require (welcome contribution). Theorem 11.4's number of trials is the explicit closed form T = ⌈(log N · log(2k)) / α⌉, α the (existentially quantified, uniform) constant from Lemma 11.3; its coverage guarantee is 1 − 1/(2k) per group (this mission's own union-bound derivation), not the book's stated 1 − 1/k — the book reaches the stronger bound via an additional shortest-path fallback mechanism for any group the trials miss, which is out of scope here (welcome contribution, along with completing any of the four sorrys and formalizing Theorem 11.5's extension to general graphs via HST embedding, out of scope since it depends on an external embedding result not proved in this book).

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024
• N. Garg, G. Konjevod, R. Ravi. A polylogarithmic approximation algorithm for the group Steiner tree problem. Journal of Algorithms, 37(1):66-84, 2000 (cited as [56] in the survey).
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor. A general approach to online network optimization problems. ACM Transactions on Algorithms, 2(4):640-660, 2006 (cited as [4], the source of this chapter's results per the Notes, p. 231).

Motivation

Section 4 of this survey derives a simple randomized $O(\log m \log n)$-competitive algorithm for the online set-cover problem, by rounding the fractional solution the online packing-covering framework produces. An intriguing question the survey poses next: can the same guarantee be achieved deterministically? The standard tool for removing randomness, the method of conditional expectations, requires finding a pessimistic estimator — a potential function whose value the algorithm can track and whose behavior certifies the randomized algorithm's guarantee step by step. Chapter 5 constructs exactly this potential function for the weighted online set-cover problem, and shows that greedily minimizing it online reproduces the randomized algorithm's competitive ratio with no randomness at all. This mission formalizes that construction: the potential function itself (Lemma 5.1) and the correctness guarantee it buys (Theorem 5.2).

Setting

Fix a finite universe of elements $E$ and a finite family of sets $T$ with positive costs $c_s$, both known to the algorithm in advance (only which elements will actually need covering, and in what order, is unknown). A monotonically increasing assignment $w : T \to \mathbb{R}$ of fractional weights to sets is produced online by a fractional subroutine (any $O(\log m)$- competitive online fractional algorithm — the survey's own Section 4.2 supplies one). An element's weight is $w_e := \sum_{s \mid e \in s} w_s$. Given a target $\alpha \ge c(C_{OPT})$ (a guessed upper bound on the optimal integral cover's cost — the survey handles an unknown optimum by doubling this guess across phases, outside this chapter's own scope), the algorithm maintains a chosen cover $C \subseteq T$ and the potential

$$\Phi \;=\; \sum_{e \notin \bar C} n^{2w_e} \;+\; n \cdot \exp\!\Big(\tfrac{1}{2\alpha} \sum_{s} \big(c_s \chi_C(s) - 3 w_s c_s \log n\big)\Big),$$

where $n = |E|$ and $\chi_C$ is $C$'s characteristic function. Whenever a set $s$'s weight increases, the algorithm computes $\Phi$ both with and without adding $s$ to $C$ and chooses whichever keeps $\Phi$ from exceeding its value before the step (failing only if neither does, which Lemma 5.1 shows cannot happen when $\alpha \ge c(C_{OPT})$).

Formalization targets

Theorem 5.2 (goal, p. 139): given the invariant $\Phi < n^2$ that Lemma 5.1 maintains throughout a run, (i) every element of weight $\ge 1$ is covered, and (ii) the chosen cover costs at most $\alpha \cdot O(\log m \log n)$.

Lemma 5.1 (milestone, p. 137): the potential function never increases in expectation across a weight-augmenting step, under the algorithm's own randomized choice of whether to add the augmented set to the cover (the internal argument — via the method of conditional expectations — that certifies the deterministic algorithm's choice rule never fails).

Significance

This chapter answers, for the online set-cover problem specifically, a question that recurs throughout online algorithm design: when can a randomized guarantee be derandomized online? The potential-function technique here is the survey's own template for the answer (it recurs, per the chapter's Notes section, in the routing algorithm of Chapter 9 and the ad-auctions algorithm of Chapter 10, both formalized as separate missions in this series) — a self-contained, reusable instance of "derandomization via an explicit pessimistic estimator" in the online setting, distinct from the offline set-cover primal-dual and dual-fitting algorithms of this book's own Chapter 2, already on the platform (PrimalDualOnline.SetCover.*, checked below: a static instance with no arrival order and no potential function, a genuinely different model).

Difficulty

The central formalization challenge is that Lemma 5.1's own statement, "$\Phi_{end} \le \Phi_{start}$", denotes the potential's value in expectation under the algorithm's randomized choice — not a single deterministic before/after pair — since the lemma is proved via a probabilistic argument (adding $s$ to the cover with probability $1 - n^{-2\delta_s}$) whose role is purely internal to justifying the deterministic algorithm's rule (choose whichever of the two options controls $\Phi$). Stating the lemma as a bare inequality between two potential values, without the mixture, would either be false (the "add $s$" branch alone can increase $\Phi$) or would silently smuggle in the derandomized choice as a hypothesis rather than proving it is always available. This mission states the expectation explicitly as a probability-weighted average of the two branch potentials, matching the actual analytic content of the book's proof (equations 5.1-5.6) rather than its final one-line restatement.

Formalization scope

SetCoverInstance E T bundles elemSets : E → Finset T (the sets containing an element) and positive costs c. elementWeight and coveredBy are literal transcriptions of $w_e$ and "$e \in \bar C$". potential transcribes $\Phi$'s displayed formula verbatim, with n cast from Fintype.card E. potential_nonincreasing (Lemma 5.1) is the expectation inequality described above. algorithm_correctness (Theorem 5.2) takes the potential invariant Φ < n² as a hypothesis (the state Lemma 5.1, applied repeatedly from the initial value $\Phi < n^2$, is what the book's own proof shows every reachable state satisfies) together with an explicit ratio β standing for "the fractional solution is O(log m)-competitive" (∑ wₛcₛ ≤ βα) — the book imports this fact from Section 4 as a black-box subroutine rather than re-deriving a specific numeric constant in this chapter, and this mission does the same rather than re-deriving Chapter 4's own constant under the (different) $d \to m$ substitution the book's prose glosses over. The conclusion is then the fully explicit α · log n · (3β + 2), matching the book's own derivation (displayed inequality, p. 139-140) with O(log m) replaced by the parameter β. This correctly rules out the trivializing formalization in which the O(log m log n) bound is left as an unquantified existential constant, or in which Φ's invariant is assumed directly as an unmotivated free hypothesis rather than the fact Lemma 5.1 is what actually establishes. Reals throughout; Real.log, Real.exp, Real.rpow (via the ^ notation on reals) for the book's own log, exp and n^{2w_e}. Nothing here is reused from 04-framework (concurrent draft; per this series' own rule, drafts do not import drafts) even though this chapter's fractional subroutine is conceptually the same online covering framework — restated here only as the abstract ratio β, not as a Lean dependency. Welcome contributions: completing the two sorrys, and formalizing the doubling-across-phases wrapper (Section 5.1's "Obtaining a Deterministic Algorithm" discussion) that removes the need to know α ≥ c(C_OPT) in advance.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor. The online set cover problem. STOC 2003 / SIAM J. Comput. 39(2), 2009 (cited by this book's Chapter 5 Notes as [3]).

Motivation

Reinforcement learning formalizes a scenario supervised learning cannot: an agent that actively interacts with an environment, choosing actions that change both the state it observes next and the reward it receives, rather than passively receiving an i.i.d. labeled sample. Every practical treatment of this scenario — from classical dynamic programming to modern deep reinforcement learning — is built on the Markov decision process (MDP), a model in which the effect of an action depends only on the current state, not on the full history that led to it. Two questions define the theory this mission covers: given a fixed way of acting (a policy), what value does it obtain, and how is that value actually computed rather than merely characterized as the solution of a fixed-point equation? Mohri, Rostamizadeh and Talwalkar's chapter 17 answers both for the stationary, infinite-horizon discounted case, and this mission targets its two central results: that a fixed policy's value is not just characterized but uniquely determined by a linear system with an explicit closed-form solution (Theorem 17.10), and that the optimal value function — obtained instead by choosing the best action at every state — can be computed by an iterative algorithm guaranteed to converge regardless of where it starts (Theorem 17.11).

Setting

A (finite) Markov decision process consists of a finite set of states $S$, a finite set of actions $A$, a transition kernel $P[s'\mid s,a]$ giving the distribution over the next state $s'$ after taking action $a$ at state $s$, and an expected reward $\mathbb E[r(s,a)]$ for that transition. A (stationary) policy $\pi:S\to\Delta(A)$ assigns each state a distribution over actions — possibly, but not necessarily, a point mass on a single action. Fixing $\pi$ turns the MDP into an ordinary Markov chain on $S$: at each step the agent is at some state $s$, draws $a\sim\pi(s)$, receives (expected) reward $\mathbb E[r(s,a)]$, and moves to a state drawn from $P[\cdot\mid s,a]$. For a discount factor $\gamma\in[0,1)$, the value of $\pi$ at $s$ is the expected discounted sum of future rewards starting from $s$,

$$V_\pi(s) = \mathbb E_{a_t\sim\pi(s_t)}\Big[\sum_{t=0}^{+\infty}\gamma^t r(s_t,a_t) \;\Big|\; s_0=s\Big],$$

and the state-action value function $Q_\pi(s,a)$ is the analogous quantity for taking $a$ at $s$ and then following $\pi$. Marginalizing the raw kernel and reward over the mixed action $\pi(s)$ gives the induced transition matrix $P_{s,s'}=P[s'\mid s,\pi(s)]=\sum_a \pi(s)(a) P[s'\mid s,a]$ and induced reward vector $R_s=\mathbb E[r(s,\pi(s))]=\sum_a\pi(s)(a)\,\mathbb E[r(s,a)]$ — the objects that turn $\pi$'s value into a genuinely linear-algebraic quantity. A policy $\pi^*$ is optimal if $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and every state $s$; write $V^*$ for its value function.

Formalization targets

Theorem 17.10 (goal). For a finite MDP and a fixed policy $\pi$, the matrix $I-\gamma P$ (with $P$ the policy-induced transition matrix) is invertible, and $\pi$'s value function is the unique solution of the Bellman equations, given in closed form by

$$V_\pi = (I-\gamma P)^{-1} R.$$

Proposition 17.9 (milestone). The value function itself satisfies the linear system that Theorem 17.10 solves:

$$\forall s\in S,\quad V_\pi(s) = \mathbb E_{a\sim\pi(s)}[r(s,a)] + \gamma\sum_{s'} P[s'\mid s,\pi(s)]\,V_\pi(s').$$

Theorem 17.7 (milestone). A policy $\pi$ is optimal if and only if it places probability only on $Q_\pi$-maximizing actions: for every $(s,a)$ with $\pi(s)(a)>0$, $a\in \operatorname{argmax}_{a'} Q_\pi(s,a')$.

Theorem 17.11 (milestone). The Bellman optimality operator $\Phi$, $[\Phi(V)](s)=\max_{a} \{\mathbb E[r(s,a)]+\gamma\sum_{s'}P[s'\mid s,a]V(s')\}$, is a $\gamma$-contraction for $\lVert\cdot\rVert_\infty$; consequently, for any starting vector $V_0$, the value-iteration sequence $V_{n+1}=\Phi(V_n)$ converges to a fixed point of $\Phi$.

Significance

Theorem 17.10 is what makes policy evaluation on a finite MDP an exact, finite computation rather than an infinite limit: instead of summing an infinite discounted series or solving an implicit fixed-point equation numerically, a single $|S|\times|S|$ matrix inversion gives the policy's value at every state simultaneously. It is also the base case every planning algorithm in the chapter builds on: policy iteration alternates optimizing a policy with exactly this evaluation step. Theorem 17.11 gives the complementary guarantee for the harder problem of finding the optimal value function directly, without fixing a policy first: value iteration converges from any starting point, with a convergence rate ($O(\log(1/\epsilon))$ iterations for $\epsilon$-accuracy) that follows from the same contraction argument. Together, the two results are the mathematical content behind why dynamic-programming planning for finite MDPs is tractable at all — the discount factor $\gamma<1$, not any structural assumption on rewards or transitions, is what buys both the uniqueness in Theorem 17.10 and the convergence in Theorem 17.11. Formalizing them requires reproducing this linear-algebraic and metric content precisely, not just asserting the conclusions: an invertibility claim asserted without the operator-norm argument, or a convergence claim without the contraction property, would state something true by fiat rather than the book's actual result. No faithful prior art exists on the platform for this exact model (see Formalization scope).

Difficulty

The obvious shortcut for Theorem 17.10 is to assert $I-\gamma P$ is invertible without proof — true, but not what the book does, and not informative about why it holds. The genuine content is that $P$, being row-stochastic (every row of $P$ sums to exactly $1$, since $\pi(s)$ and $P[\cdot\mid s,a]$ are both proper distributions), has operator norm $\lVert P\rVert_\infty=1$ exactly, so $\lVert\gamma P\rVert_\infty=\gamma<1$ strictly; this rules out $1$ as an eigenvalue of $\gamma P$, which is exactly what invertibility of $I-\gamma P$ requires. The same $\gamma<1$ fact, applied differently, drives Theorem 17.11: showing $\Phi$ is $\gamma$-Lipschitz requires bounding $\Phi(V)(s)-\Phi(U)(s)$ by comparing the maximizing action for $V$ against the same action's value under $U$ (not $U$'s own maximizer), since the two suprema need not be attained at the same action — a step easy to state incorrectly as a direct comparison of two maxima. Both theorems fail if $\gamma=1$ is allowed: the discounted setting's central asset, a strict contraction, disappears exactly at that boundary.

Formalization scope

States and actions are modeled as finite types (Fintype S, Fintype A); the raw kernel and reward P : S → A → S → ℝ, Er : S → A → ℝ are unconstrained functions, with IsTransitionKernel asserting the required distribution property explicitly rather than assuming it silently. A policy is π : S → A → ℝ with IsPolicy π asserting π s is a distribution over A for every s — deliberately not π : S → A or a PMF-valued function, since Theorem 17.7's own quantifier ("for any pair (s,a) with π(s)(a) > 0") requires treating π(s) as a genuine mixture. PolicyValue is defined as the actual infinite discounted expectation (via an explicit state-occupation-distribution recursion), not as the Bellman fixed point — so that Proposition 17.9 (the value function satisfies the linear system) and Theorem 17.10 (that system has a unique, invertible-matrix solution) are both non-vacuous claims about the same object, rather than one being definitionally true of the other. The trivializing formalization this rules out is asserting IsUnit (1 - γ • P) as a bare hypothesis, or defining V_π as (1-γP)⁻¹R and calling the resulting identity a theorem; both would erase the mission's actual content. Two platform modules model related MDPs (BertsekasSSPModel, a stochastic-shortest-path model with a termination-probability deficit rather than exact row-stochasticity, and FoundationsRL.RLBasics, a finite-horizon episodic model indexed by layer) — neither specializes exactly to this chapter's stationary, always-continuing, infinite-horizon discounted convention, so every definition here is drafted fresh rather than imported. This chunk covers §17.2–17.4.2 (the MDP model, policy value, Bellman's equations, value and policy iteration); §17.4.3 (the linear-programming formulation) and §17.5 (stochastic-approximation learning algorithms — TD(0), Q-learning, SARSA) are out of scope, since they require a stochastic-approximation convergence substrate this mission does not build.

Selected references

• Mohri, M., Rostamizadeh, A., and Talwalkar, A. Foundations of Machine Learning, 2nd ed., chapter 17. MIT Press, 2018.
• Bellman, R. Dynamic Programming. Princeton University Press, 1957.
• Puterman, M. L. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1994.

Comparing random outcomes without comparing numbers

Operations research and applied probability are full of questions of the shape "is X riskier, larger, or later than Y?" when X and Y are random: two queueing disciplines' waiting times, two inventory policies' shortfall, two insurance portfolios' claim size. Comparing their means answers a weaker question than the modeler usually wants, since two distributions can share a mean while one is uniformly the "worse" one to face. Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) is the standard reference for the family of orders built to make "X is stochastically no larger than Y" precise, and this mission formalizes the foundational member of that family: the usual stochastic order, together with its central structural theorem.

The usual stochastic order

Let $X$ be a real-valued random variable on a probability space $(\Omega,\mu)$, and let $Y$ be a real-valued random variable on a (possibly different) probability space $(\Omega',\nu)$. $X$ is smaller than $Y$ in the usual stochastic order, written $X \le_{st} Y$, if

$$P\{X > x\} \le P\{Y > x\} \quad \text{for every } x \in (-\infty,\infty).$$

Equivalently, $P\{X \le x\} \ge P\{Y \le x\}$ for every $x$: $Y$'s cumulative distribution function never exceeds $X$'s. Two features of the definition matter for everything that follows. First, it is a comparison of distributions, not of jointly defined variables — $X$ and $Y$ need not live on the same probability space, and the order depends only on their laws. Second, the inequality must hold for every threshold $x$ simultaneously; it is not a comparison of two summary statistics such as means or medians, and a distribution can fail $X \le_{st} Y$ even while $E[X] \le E[Y]$.

A closely related order compares residual lifetimes rather than raw tail probabilities. $X$ is smaller than $Y$ in the hazard rate order, written $X \le_{hr} Y$, if the survival functions $\bar F(x) = P\{X>x\}$, $\bar G(x) = P\{Y>x\}$ satisfy $\bar F(x)\bar G(y) \ge \bar F(y)\bar G(x)$ for all $x \le y$ — the general, density-free form of the condition that for absolutely continuous distributions reduces to a pointwise comparison of hazard rates $r(t) = f(t)/\bar F(t)$. It is one of several stronger orders (alongside the likelihood ratio order) that the book shows all imply $\le_{st}$, and it is the mission's second definition.

Formalization targets

Goal: the coupling characterization (Theorem 1.A.1)

$$X \le_{st} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y : \Omega'' \to \mathbb{R} \text{ with } \hat X =_{st} X,\ \hat Y =_{st} Y,\ \text{and } P\{\hat X \le \hat Y\} = 1.$$

This is the order's Strassen-type coupling theorem: $X \le_{st} Y$ holds exactly when copies of $X$ and $Y$ can be realized on one common probability space so that, almost surely, the copy of $X$ never exceeds the copy of $Y$. It is the weakest possible statement with this shape (existence of some coupling on some space, not a canonical one), and it is the archetype every later chapter's own coupling theorem — for the hazard rate order, the convex order (via a martingale coupling), the multivariate orders — restates for its own comparison.

Supporting milestones

• Theorem 1.A.2, the same characterization restated via a common random source: $X \le_{st} Y$ iff there is a random variable $Z$ and functions $\psi_1 \le \psi_2$ with $X =_{st} \psi_1(Z)$ and $Y =_{st} \psi_2(Z)$.
• Theorem 1.A.3(a), closure under monotone transformations: $X \le_{st} Y$ and $g$ increasing gives $g(X) \le_{st} g(Y)$ (reversed for $g$ decreasing).
• Theorem 1.A.3(b), closure under increasing functions of independent families and, as its corollary, under convolution: independent $X_i \le_{st} Y_i$ and $\psi$ increasing gives $\psi(X_1,\dots,X_m) \le_{st} \psi(Y_1,\dots,Y_m)$, in particular $\sum_i X_i \le_{st} \sum_i Y_i$.
• Theorem 1.B.1, the first link of the book's implication chain: $X \le_{hr} Y \implies X \le_{st} Y$.

Significance

The usual stochastic order is the weakest and most widely used of the book's orders, and the coupling theorem is the tool that makes it tractable: comparing tail probabilities for every threshold is an infinite family of inequalities, while exhibiting one coupling on one space settles the comparison in a single stroke. This is the technique behind, among many applications in the book and the wider literature, comparing waiting times across queueing disciplines, bounding the effect of parameter uncertainty on a risk measure, and proving monotonicity results for Markov chains by coupling their sample paths. The closure properties (Theorem 1.A.3) are what let such comparisons survive composition with a monotone payoff function or a sum of independent components — exactly the operations a queueing or inventory model performs on its primitives.

Formalizing this theorem establishes, in one place, both the statement and the exact shape of its existential witness (a genuine ∃ over a probability space and two identically distributed random variables, not merely two abstractly-known-to-exist objects), which is the piece every later chapter's own coupling theorem in this series needs to get right independently. No proof is attempted in this mission; the book's own three-line construction ($\hat X = F^{-1}(U)$, $\hat Y = G^{-1}(U)$ for a uniform $U$) is a natural target for a future proof-bearing pass.

Difficulty

The definitional trap is the "for all $x$" in $\le_{st}$: it is tempting to shortcut it into a comparison of one summary statistic (a mean, an essential supremum, a specific quantile), which is uniformly weaker and would make Theorem 1.A.1 either false or a different, easier theorem. The coupling theorem itself has a second trap in its existential structure: the common probability space $(\Omega'',\rho)$ must be genuinely quantified — fixed neither to $\Omega$ nor $\Omega'$ in advance — and "$\hat X =_{st} X$" is equality of the two random variables' laws, not almost-sure equality of $\hat X$ and $X$ themselves (they typically do not share a domain before the construction). Theorem 1.A.3(b)'s general statement, for an arbitrary increasing $\psi:\mathbb{R}^m \to \mathbb{R}$ on independent families, is easy to understate as only its convolution corollary; the book gives both, and the general statement is the one with the actual content (the sum is recovered by taking $\psi$ to be the coordinate sum, itself increasing).

Formalization scope

Random variables are represented as measurable functions into $\mathbb{R}$ from arbitrary measurable spaces, and "equality in law" is Mathlib's native ProbabilityTheory.IdentDistrib, which is defined for two (possibly different) probability spaces and requires almost-everywhere measurability rather than fixing an ambient space in advance — matching the book's own treatment of $X \le_{st} Y$ as a comparison between distributions. UsualOrder μ ν X Y and HazardRateOrder μ ν X Y both take $X:\Omega\to\mathbb{R}$ on $(\Omega,\mu)$ and $Y:\Omega'\to\mathbb{R}$ on a separate $(\Omega',\nu)$, so no theorem here can be trivialized by silently forcing $X$ and $Y$ onto one shared space. HazardRateOrder is stated via the survival-function cross-product inequality (Eq. 1.B.4), the form that needs no absolute-continuity hypothesis, rather than via a derivative-based hazard rate, so it applies to the same general random variables as UsualOrder without an extra regularity hypothesis the book itself does not require at this level of generality. Independence in Theorem 1.A.3(b) is Mathlib's ProbabilityTheory.iIndepFun; the random variable $Z$ of Theorem 1.A.2 is left valued in an arbitrary measurable space, matching the book's unrestricted statement, rather than narrowed to $\mathbb{R}$-valued for convenience. A trivializing formalization is ruled out explicitly: $\le_{st}$ is not formalized as a comparison of means, medians, or any single moment, and the coupling theorems' ∃ is a genuine existential over a probability space, not a hypothesis smuggling in the witness's existence.

This mission draws on no platform prior art (repeated searches for "stochastic order", "coupling", "Strassen" and "identically distributed" turned up nothing on-topic as of 2026-09-18); it is the first mission in a nine-chapter series covering the whole book, and its own definitions are not imported by later chapters — each restates locally what it needs, per the series' own convention that draft items cannot import another draft's definitions. Reusable beyond this mission: the UsualOrder/HazardRateOrder shape (parametrizing over two separate probability spaces) is the pattern every later chapter's own order definition follows.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

Every convex optimization algorithm in machine learning — from projected gradient descent to support vector machines to the mirror-descent methods of later chapters of this book — is justified by a small set of optimality certificates: a checkable condition on a candidate solution that guarantees it actually solves the problem, without searching the whole feasible set. The most widely used such certificate is the Karush–Kuhn–Tucker (KKT) system: a set of gradient and complementary-slackness equations that a solution of a convex program with differentiable data must satisfy, and that (under a mild constraint qualification) is also sufficient. It is the tool a practitioner reaches for to check optimality of a numerical solver's output, and the tool a theorist reaches for to derive an algorithm (dual ascent, augmented Lagrangian, interior point methods) in the first place. Every convex machine learning model introduced in Chapter 1 of this book — regularized least squares, support vector machines, logistic regression with constraints — is an instance of the general convex program these milestones analyze.

The result traces back to Kuhn and Tucker's 1951 paper Nonlinear Programming, with Karush's 1939 unpublished thesis establishing the same conditions independently and earlier; Slater's 1950 unpublished note is the source of the constraint qualification that bears his name and that makes the necessity direction possible. Lan's Chapter 2 gives a compact, modern, purely finite-dimensional derivation of the whole chain — separation, duality, saddle points, KKT — from first principles, self-contained in about twenty pages, aimed squarely at the convex programs that appear in machine learning.

Setting

Fix $n, m, p \in \mathbb{N}$ and work in $\mathbb{R}^n$ with its standard inner product $\langle \cdot,\cdot\rangle$. A convex program (2.3.16) is

$$f^* \equiv \min_{x \in X} f(x) \quad \text{s.t.} \quad g_i(x) \le 0\ (i=1,\dots,m), \quad h_j(x) = 0\ (j=1,\dots,p),$$

where $X \subseteq \mathbb{R}^n$ is a nonempty closed convex set, $f, g_1,\dots,g_m : X \to \mathbb{R}$ are convex, and $h_1,\dots,h_p$ are affine. A point $x \in X$ is feasible if it satisfies every $g_i(x)\le 0$ and $h_j(x)=0$; $x^*$ is optimal if it is feasible and $f(x^*)\le f(x)$ for every feasible $x$.

The normal cone of $X$ at $x$ is $N_X(x) := \{w \in \mathbb{R}^n : \langle w, y-x\rangle \le 0 \ \forall y \in X\}$ — the set of directions that make an obtuse angle with every direction into $X$ from $x$; it is $\{0\}$ when $X = \mathbb{R}^n$, recovering unconstrained first-order optimality. The Lagrangian is $L(x,\lambda,y) := f(x) + \sum_i \lambda_i g_i(x) + \sum_j y_j h_j(x)$ for multipliers $\lambda \ge 0$, $y \in \mathbb{R}^p$; the Lagrange dual value is $\varphi(\lambda,y) := \min_{x\in X} L(x,\lambda,y)$, and the Lagrange dual problem is $\varphi^* := \max_{\lambda\ge 0,\,y}\varphi(\lambda,y)$. Weak duality, $\varphi^*\le f^*$, holds unconditionally by construction. Slater's condition asks for $\bar x \in \operatorname{int} X$ with $g(\bar x) < 0$, $h(\bar x)=0$; the restricted Slater condition weakens the interior requirement to the relative interior $\operatorname{rint} X$ while keeping strict inequality for every (here: every) nonlinear constraint.

Formalization targets

Goal — Theorem 2.8(b), KKT necessity

$$x^* \text{ optimal (with a restricted-Slater point)} \implies \exists\, \lambda^*\ge 0,\, y^*: \ \nabla f(x^*) + \sum_i \lambda_i^* \nabla g_i(x^*) + \sum_j y_j^* \nabla h_j(x^*) \in N_X(x^*), \ \lambda_i^* g_i(x^*) = 0\ \forall i.$$

Companion — Theorem 2.8(a), KKT sufficiency

$$\exists\, \lambda^* \ge 0,\, y^* \text{ satisfying stationarity and complementary slackness at a feasible, differentiable } x^* \implies x^* \text{ optimal.}$$

Supporting milestones, in attack order

• Theorem 2.1 (separation): a point outside a closed convex set is strictly separated from it by a hyperplane.
• Proposition 2.9 (Convex Theorem on Alternative): insolvability of a strict-inequality system, plus a Slater point, forces solvability of a dual multiplier system.
• Theorem 2.6 (strong duality): under Slater's condition, $\varphi^* = f^*$ and the dual is solvable.
• Theorem 2.7(a)/(b) (saddle points): $x^*$ is optimal iff it extends to a saddle point of $L$ (the "only if" needs Slater's condition; the "if" needs nothing beyond the saddle inequalities).

Each of these five is stated the way the book states it — no constant is hard-coded, no O(·) is involved, and every hypothesis (closedness, convexity, Slater/restricted-Slater) is exactly the one the corresponding proof uses.

Significance

The KKT system is the interface between convex optimization theory and every algorithm that exploits it: primal-dual methods track approximate KKT residuals as a stopping criterion, and the derivation of the Lagrange dual (used throughout the book's later treatment of composite and constrained problems) rests on strong duality, milestone strong_duality here. The saddle-point characterization (saddle_point_sufficient/saddle_point_necessary) is the standard route to designing an algorithm: a method that provably drives a pair $(x_k,\lambda_k)$ to a saddle point of $L$ is provably convergent to an optimal $x^*$, without ever needing to verify optimality directly against the primal problem.

None of the six substantive results here has a machine-checked proof on Prove2Me. The platform holds a genuinely weaker unconstrained-in-$K$ condition (OnlineConvexOpt.ConvexBasics. kkt_optimality, Hazan's Theorem 2.2: $\langle\nabla f(x^*), y-x^*\rangle \ge 0$ for $y \in K$, with no inequality/equality constraints or multipliers at all) and a structurally different, strictly more general cone-based Lagrange-duality development (VectorSpaceOpt.lagrange_duality and VectorSpaceOpt.lagrangian_saddle_sufficient_pointed, from Luenberger, which bundle all constraints into a single map into a convex cone in a general normed space, rather than Lan's explicit $\mathbb{R}^m$ inequality / $\mathbb{R}^p$ equality split). Formalizing this mission produces the finite-dimensional convex-program version of KKT in exactly the shape it is used and taught: separate multiplier vectors for inequality and equality constraints, an explicit normal cone rather than a cone-map abstraction, and both directions of the necessity/sufficiency split.

Difficulty

The separation theorem (Theorem 2.1) itself is routine once the projection onto a closed convex set is available. The real difficulty is entirely in the direction of the Convex Theorem on Alternative that Proposition 2.9 states: the naive idea — "insolvability of (I) should give a separating hyperplane between $\{x : f(x)<c\}$ and $\{x: g(x)\le 0\}$ directly" — fails, because these are sets in $\mathbb{R}^n$ and separating them there does not produce a sign-definite multiplier vector. Lan's proof instead lifts to $\mathbb{R}^{m+1}$ and separates the epigraph-like set $T = \{u : \exists x\in X,\ f(x)\le u_0, g(x)\le u_{1:m}\}$ from the open orthant-like set $S = \{u: u_0<c, u_{1:m}\le 0\}$; only in this lifted space does the separating normal's sign constraint (forced by $S$'s unboundedness in the positive directions) translate into $\lambda \ge 0$. Getting the sign of the $0$-th coordinate strictly positive — needed to normalize and divide — is itself a small separate argument using the Slater subsystem's solution. The KKT necessity direction (the goal) then chains three of these already-nontrivial results (separation → CTA → strong duality → saddle necessity) before translating the saddle-point condition on $L$ into the gradient/normal-cone form via differentiability of $f, g$ at $x^*$.

Formalization scope

All milestones are stated over EuclideanSpace ℝ (Fin n) with Convex/ConvexOn from Mathlib. Affine equality constraints $h_j$ are represented by explicit witnesses $w_j \in \mathbb{R}^n, b_j \in \mathbb{R}$ with $h_j(x) = \langle w_j, x\rangle + b_j$, so that $\nabla h_j = w_j$ is available without a separate affine-differentiability lemma. The normal cone $N_X^*(x)$ is Lan's own primal-space object (normalCone); the restricted Slater condition uses Mathlib's intrinsicInterior ℝ X for $\operatorname{rint} X$, distinct from the plain interior X used by the un-restricted Slater condition of Theorems 2.6/2.7(b). Primal optimal values and Lagrange dual values are stated via IsGLB/pointwise-inequality forms rather than raw sInf, so that no hypothesis is silently made true by an empty or unbounded set defaulting sInf to a junk value — in every milestone here the relevant set is guaranteed nonempty by the Slater-point hypothesis already present.

A trivializing formalization this mission rules out: stating kkt_necessary/kkt_sufficient with $X = \mathbb{R}^n$ (no set constraint) and empty $g, h$ (no functional constraints) would collapse the normal-cone condition to $\nabla f(x^*) = 0$ and make the whole KKT apparatus vacuous of any duality content; the milestones here keep $X$, $g$ and $h$ as genuine free parameters (the theorems are stated for arbitrary m, p : ℕ, including but not restricted to the degenerate case) so that the constrained content of Lan's theorem is what gets proved.

Reusable beyond this mission: normalCone and lagrangian are generic enough that any later chapter of this book needing Lagrangian duality or normal-cone stationarity (none of the current first-wave chapters 03/06 needs them directly) could import them once published rather than redeclaring. Contributions most welcome on the two hardest milestones, cta_solvable_of_insolvable and kkt_necessary, since they carry the mission's real difficulty; separation_point_closed can likely be discharged quickly via Mathlib's geometric_hahn_banach_point_closed.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 2. https://doi.org/10.1007/978-3-030-39568-1
• H. W. Kuhn and A. W. Tucker, "Nonlinear Programming," Proceedings of the Second Berkeley Symposium on Mathematical Statistics and Probability, 1951, pp. 481–492.
• W. Karush, "Minima of Functions of Several Variables with Inequalities as Side Constraints," M.Sc. thesis, University of Chicago, 1939.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (standard modern reference for the separation theorem and Lagrangian duality used throughout).

Ordering how strongly two variables move together

The first eight chapters of Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) compare single random variables — location, variability, convexity. Chapter IX turns to a different question: given two coordinates of a random vector, how strongly do they tend to move together? "Large values of $X_1$ go with large values of $X_2$" is a qualitative property (positive dependence); comparing how much two bivariate distributions exhibit it, holding their individual marginals fixed, is what this chapter's positive dependence orders make precise. This mission formalizes the two central ones — the PQD order and the supermodular order — and the supermodular order's closure properties, the chapter's own capstone result.

The PQD and supermodular orders

Let $X=(X_1,\dots,X_n)$ and $Y=(Y_1,\dots,Y_n)$ be two random vectors, with joint survival function $\bar F(x)=P\{X_1>x_1,\dots,X_n>x_n\}$ and joint distribution function $F(x)=P\{X_1\le x_1,\dots,X_n\le x_n\}$ (similarly $\bar G, G$ for $Y$). $X$ is smaller than $Y$ in the PQD order, written $X\le_{PQD}Y$, if

$$\bar F(x)\le\bar G(x)\ \text{ and }\ F(x)\le G(x) \quad\text{for every }x\in\mathbb{R}^n.$$

(It follows, though it need not be assumed, that $X$ and $Y$ then share the same univariate marginals — the two inequalities together pin the marginals down, unlike a single one alone.) This is Lehmann's positive-quadrant-dependence order in its general multivariate form: $Y$'s coordinates cluster together, in both the upper and lower "quadrants," at least as strongly as $X$'s.

A function $\varphi:\mathbb{R}^n\to\mathbb{R}$ is supermodular if $\varphi(x)+\varphi(y)\le\varphi(x\wedge y)+\varphi(x\vee y)$ for the coordinatewise meet/join — the function-level notion the platform's Topkis/Supermodularity series already formalizes for games and lattices, reused here directly. $X$ is smaller than $Y$ in the supermodular order, written $X\le_{sm}Y$, if $E[\varphi(X)]\le E[\varphi(Y)]$ for every supermodular $\varphi$ for which the two expectations exist. Because the indicator of any upper or lower orthant is itself supermodular, $X\le_{sm}Y\implies X\le_{PQD}Y$ (Eq. 9.A.17): the supermodular order is strictly finer than the PQD order, and for $n=2$ the two coincide.

Formalization targets

Goal: closure properties of the supermodular order (Theorem 9.A.9(a),(c))

$$(X_1,\dots,X_n)\le_{sm}(Y_1,\dots,Y_n) \implies (g_1(X_1),\dots,g_n(X_n))\le_{sm}(g_1(Y_1),\dots,g_n(Y_n))$$

whenever every $g_i$ is increasing, or every $g_i$ is decreasing (part a); and

$$X\le_{sm}Y \implies X_I\le_{sm}Y_I \quad\text{for every } I\subseteq\{1,\dots,n\}$$

(part c, closure under marginalization). These are two of Theorem 9.A.9's five closure properties — the theorem the brief for this mission recommends as its goal — chosen as the ones that need no further definitional machinery beyond the orders themselves (composition and a coordinate projection, both plain pushforwards of the vector's law).

Supporting milestone

• Theorem 9.A.4, the general multivariate closure of the PQD order under independent pairing: if $X\le_{PQD}Y$, $U\le_{PQD}V$, with $X,U$ independent and $Y,V$ independent, then $(\varphi_1(X_1,U_1),\dots,\varphi_n(X_n,U_n))\le_{PQD}(\varphi_1(Y_1,V_1),\dots,\varphi_n(Y_n,V_n))$ for all increasing $\varphi_i$ — the closure property the chapter opens with (as Theorem 9.A.1, the bivariate case), generalized to $n$ dimensions.

Significance

Positive dependence orders formalize a comparison operations research and risk management need constantly but rarely state precisely: two portfolios, insurance lines, or queueing networks with identical individual risk profiles can still differ sharply in how their components co-move, and that co-movement — not the marginals — is often what drives tail risk, correlated failures, or aggregate variability. The supermodular order is the standard tool for comparing this directly: Theorem 9.A.9's closure properties are what let a comparison established for primitive components survive the operations a model actually performs on them — relabeling by a monotone transform (part a), reading off a subset of coordinates (part c), combining independent sub-vectors (part b), conditioning on a covariate (part d), or passing to a distributional limit (part e). Chapter VI's multivariate stochastic order and Chapter VII's multivariate convex order are the two other multivariate orders in the book; the supermodular order is the one built specifically to compare dependence structure rather than location or spread, and it connects directly to the platform's existing Topkis/Supermodularity series, whose function-level predicate this mission reuses rather than restates.

Formalizing Theorem 9.A.9 fixes the exact shape a supermodular-order closure claim takes when built as a pushforward of the vector's law — the natural Mathlib-idiomatic rendering once the order is stated on laws rather than on variables tied to a fixed ambient space — for any future mission in this series or elsewhere that needs to state a closure property of a vector-valued stochastic order. No proof is attempted; both drafted parts of Theorem 9.A.9 have short book proofs (part (a) from the fact that composing a supermodular function with all-increasing or all-decreasing coordinate maps is again supermodular; part (c) the book calls "easy to prove"), making them plausible future proof targets.

Difficulty

The chapter's central definitional trap is that the PQD order's defining condition — even in its general multivariate form — determines the marginals as a consequence of the two joint inequalities holding together, not as a separate hypothesis to add; adding same-marginals as an extra explicit condition on top of Eqs. (9.A.13)-(9.A.14) would not be false, but it would present as a hypothesis something the theorem's own two conditions already force. A second trap is specific to Theorem 9.A.9(a): the $g_i$ must be uniformly increasing or uniformly decreasing across all coordinates, not an arbitrary per-coordinate mix — a mixed-monotonicity version is a materially different, unproven claim, since it is exactly the all-same-direction condition that keeps a composition with a supermodular function supermodular. A third, more basic trap common to every function-class order in this book: "for every supermodular $\varphi$" must be a genuine universal quantifier with the two expectations' existence stated as an explicit hypothesis, not a global assumption or a specific test function standing in for the whole class.

Formalization scope

Unlike the univariate orders formalized elsewhere in this series (which take random variables $X:\Omega\to\mathbb{R}$, $Y:\Omega'\to\mathbb{R}$ on two possibly-different probability spaces), PQDOrder and SupermodularOrder here are stated directly on the two vectors' laws — measures $P,Q$ on $\iota\to\mathbb{R}$ for a finite index type $\iota$ — since the book's own comparisons never reference a joint law of $X$ and $Y$ together, only their separate distributions. This is also what lets Theorem 9.A.9(a)'s coordinatewise composition and (c)'s marginalization be stated as plain pushforwards (Measure.map) of one law, without carrying an ambient sample space through the statement. The index type is left an arbitrary finite type (Fintype ι, not fixed to Fin n) so the same two declarations serve both a full $n$-vector and any marginal sub-vector obtained by restricting to a subset $I$ of coordinates — the shape Theorem 9.A.9(c) itself needs. Supermodularity reuses the platform's own Supermodularity.Monotonicity.SupermodularOn (from the Topkis series, via a kind: reference item) with its relativizing set argument fixed to Set.univ, its plain unrelativized form — checked to match the book's φ(x)+φ(y)≤φ(x∧y)+φ(x∨y) on ι → ℝ's own coordinatewise lattice structure exactly, not a games- or player-scoped variant. Independence in Theorem 9.A.4 is formalized by taking the joint law of the two independent vectors to be the product measure of their marginals — the standard way to construct an independent coupling with prescribed marginals — rather than adding a separate independence hypothesis about pre-existing random variables. Measurable hypotheses are added on every map a Measure.map is taken along, guarding against the pushforward's junk-zero-measure convention for a non-measurable map; none narrows what the book's own theorems claim, since every map used (a monotone/antitone composition, a coordinate projection) is genuinely measurable. A trivializing formalization is ruled out explicitly: the supermodular quantifier ranges over the reused, already-audited Topkis predicate rather than a hand-rolled or restricted one, and the "for all increasing $\varphi_i$" of Theorem 9.A.4 is a genuine universal over jointly-monotone functions of two arguments, not a fixed example.

This mission draws on the platform's own Topkis/Supermodularity series for its supermodular function-level building block (Supermodularity.Monotonicity.SupermodularOn, reused as a reference item — the strongest prior-art connection of the whole nine-chapter series, per the series plan) but on no prior art for the orders themselves (repeated searches for "PQD", "positive dependence", "Fréchet bound" and "supermodular" returned nothing on-topic beyond the Topkis series as of 2026-09-18). Reusable beyond this mission: the laws-only, arbitrary-Fintype- index formalization pattern is available to any later mission in this series needing a multivariate order (Chapter VI's multivariate stochastic order, Chapter VII's multivariate convex order) that wants marginalization or coordinatewise composition stated as plain pushforwards.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5
• E. L. Lehmann, "Some concepts of dependence", Annals of Mathematical Statistics, 37(5), 1966, 1137–1153. https://doi.org/10.1214/aoms/1177699260

From "more spread out" to "more spread out in every direction"

Chapter III's convex order compares two real-valued random variables by "how spread out" they are, holding the mean fixed. Chapter VII lifts the same idea to random vectors: $X$ is smaller than $Y$ in the multivariate convex order if every convex function of $X$ has smaller expectation than the same function of $Y$. This mission formalizes that order, its increasing-convex companion, and their martingale-coupling characterizations — the direct $n$-dimensional generalizations of Chunk 03's and Chunk 04's own goal theorems — plus a cheap mean-equality corollary and a simple standalone scaling result.

The multivariate convex and increasing convex orders

Let $X$ be a random vector taking values in $\mathbb{R}^n$ on $(\Omega,\mu)$, and $Y$ a random vector taking values in $\mathbb{R}^n$ on $(\Omega',\nu)$. $X$ is smaller than $Y$ in the multivariate convex order, $X\le_{cx}Y$, if

$$E[\varphi(X)] \le E[\varphi(Y)] \quad \text{for every convex } \varphi:\mathbb{R}^n\to\mathbb{R} \text{ for which the two expectations exist},$$

and smaller than $Y$ in the increasing convex order, $X\le_{icx}Y$, if the same holds for every $\varphi$ that is both increasing (coordinatewise) and convex. Since each coordinate projection $\varphi_i(x)=x_i$ and its negation are both convex, $X\le_{cx}Y$ forces $E[X]=E[Y]$ componentwise (Eq. 7.A.5) — unlike $\le_{icx}$, which only forces $E[X]\le E[Y]$.

Formalization targets

Goal: the martingale-coupling characterization (Theorem 7.A.1)

$$X \le_{cx} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}^n\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ E[\hat Y\mid\hat X]=\hat X\text{ a.s.}$$

The direct $n$-dimensional generalization of Theorem 3.A.4 (Strassen's martingale coupling, Chunk 03's own goal theorem): a joint law on a common probability space realizing $X\le_{cx}Y$ as a genuine martingale pairing between copies of $X$ and $Y$. The book states no further "Furthermore" strengthening here, unlike the univariate and increasing-convex cases.

Companion: the submartingale-coupling characterization (Theorem 7.A.2, increasing convex case)

$X\le_{icx}Y$ iff there exist $\hat X,\hat Y$ on a common space with $\hat X=_{st}X$, $\hat Y=_{st}Y$, and $\{\hat X,\hat Y\}$ a submartingale, $E[\hat Y\mid\hat X]\ge\hat X$ a.s. — the direct generalization of Theorem 4.A.5's increasing-convex case (Chunk 04's own goal theorem), proved by the book's own cross-reference "by essentially the same method" as the goal. The book's bracketed increasing-concave companion is a genuinely separate statement (swapped conditioning) and is not drafted here for budget (see STATUS.md).

Supporting milestones

• Eq. (7.A.5), the mean-equality corollary: $X\le_{cx}Y\implies E[X]=E[Y]$ (componentwise), provided the expectations exist — a one-line consequence of ConvexOrder's own defining quantifier applied to $\pm$ each coordinate projection.
• Theorem 7.A.9, a simple standalone application: an independent, mean-one random scale factor $U$ always makes a random vector larger in the convex order, $X\le_{cx}UX$.

Significance

The multivariate convex order is the natural tool for comparing the variability of random vectors — portfolios of returns, multi-resource cost vectors, correlated component lifetimes — in a way that respects every direction of the space simultaneously rather than coordinate by coordinate. Its martingale-coupling characterization is the same tool that makes Strassen's theorem useful in the univariate case: it turns the intractable "for every convex $\varphi:\mathbb{R}^n\to\mathbb{R}$" quantifier into a single explicit joint construction, and because it generalizes directly (the book's own proof of Theorem 7.A.4, not drafted here, applies the univariate Theorem 3.A.4 coordinate by coordinate to build the multivariate coupling), it is the natural second data point — after Chunk 03's univariate case and Chunk 06's usual-order case — for what a "coupling-characterization" mission in this book's series looks like once both the order and the dimension vary. Theorem 7.A.9's scaling result is a compact, self-contained illustration of how the order behaves under a common operation (randomized scaling) that appears throughout the book's later risk and insurance examples.

No platform prior art exists: GET /theorems?q=convex+order and q=martingale return only false positives (checked at this book's triage time, re-confirmed this session). This mission restates the multivariate convex and increasing convex orders and their coupling characterizations as a self-contained pair, parallel in structure to Chunks 03 and 04's univariate missions but independently drafted, since drafts cannot import each other's Lean.

Difficulty

The chief formalization risk this chapter's own brief flags is confusing "convex" for $\varphi:\mathbb{R}^n\to\mathbb{R}$ (ordinary convexity, Mathlib's ConvexOn) with a coordinatewise or lattice-based notion — in particular, with Chunk 09's supermodular functions, a different and weaker condition. A second risk is the "increasing" half of IcxOrder: unlike convexity, "increasing" genuinely is the coordinatewise order (matching Chunk 06's convention), so IcxOrder mixes two different kinds of predicate on the same φ (Monotone in the coordinatewise sense, ConvexOn in the ordinary sense) and getting either one wrong silently changes which order is being stated. A third risk, specific to Theorem 7.A.2, is the bracketed icx/icv alternative: as in Chunk 04, the two cases are not symmetric rewrites of each other (the conditioning variable swaps), so a Lean statement conflating them with Or would misstate one case — this mission avoids the risk by drafting only the increasing-convex case and recording the omission explicitly rather than attempting an unsound unification.

Formalization scope

Random vectors are drafted as functions into Fin n → ℝ from arbitrary measurable spaces. ConvexOrder μ ν X Y quantifies over φ : (Fin n → ℝ) → ℝ with ConvexOn ℝ Set.univ φ (ordinary convexity) and Integrable (φ ∘ X) μ/Integrable (φ ∘ Y) ν inside the ∀; IcxOrder adds Monotone φ in Mathlib's default coordinatewise (Pi) order on Fin n → ℝ — the same order Chunk 06's MultivariateOrder uses — as a genuinely separate definition from ConvexOrder, not one derived from the other, since Theorem 7.A.12 (not drafted here) relates the two nontrivially and conflating them would trivialize such a relationship. Equality in law is ProbabilityTheory.IdentDistrib; the martingale/submartingale conditions use Mathlib's conditional-expectation notation ρ[Ŷ | m] =ᵐ[ρ] X̂ (resp. X̂ ≤ᵐ[ρ] ρ[Ŷ | m]) with m generated by X̂, here genuinely Fin n → ℝ-valued (well-defined since Fin n → ℝ is a finite-dimensional, hence complete, normed space over ℝ) — restated locally rather than imported from Chunks 03/06, since drafts cannot import another mission's definitions. Theorem 7.A.9's scaling U·X is Mathlib's scalar multiplication on the ℝ-module Fin n → ℝ.

Two deliberate scope restrictions, recorded rather than silently applied: (1) Theorem 7.A.2 is drafted only for the increasing-convex case, per this chapter's own pitfall 3 (the icv companion's swapped conditioning structure is a genuinely different predicate, not a sign-flipped rewrite, and budget did not justify a fourth definition/theorem pair to draft it separately, unlike Chunk 04 which had budget for both cases of its analogous theorem); (2) Theorem 7.A.5 through 7.A.8's closure properties (mixtures, convolutions, weak limits, the random-sum generalization) are left out entirely — each needs conditional-distribution or convergence-in-distribution machinery this mission's four items do not otherwise require, and none is on the goal's own attack chain.

A trivializing formalization this mission rules out: drafting IcxOrder by deriving it from ConvexOrder and a separate monotonicity wrapper in a way that makes their relationship (Theorem 7.A.12: $X\le_{st}Y\implies X\le_{icx}Y\wedge X\le_{icv}Y$, not drafted here) provable by unfolding rather than by genuine content — the two are kept as independently-quantified predicates for this reason. This mission draws on no platform prior art (searches for "convex order" and "martingale" as of 2026-09-18 return only false positives). Reusable beyond this mission: the ConvexOrder/IcxOrder pattern and their martingale/submartingale coupling shape parallel Chunks 03/04's univariate pair and Chunk 06's multivariate usual-order pair closely enough that a future pass drafting the icv companion, or Chapter VII's later dispersion and transform orders, could restate the same shape with minimal adaptation.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 7 (Multivariate Variability and Related Orders), §7.A.1–7.A.2. https://doi.org/10.1007/978-0-387-34675-5
• This series' Chunk 03 (StochasticOrders.Convex) and Chunk 04 (StochasticOrders.MonotoneConvex), for the univariate convex and increasing convex orders and their martingale/submartingale couplings this chapter directly generalizes; Chunk 06 (StochasticOrders.Multivariate), for the multivariate usual stochastic order and its own coupling characterization.