The OR Formalization Drive

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

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

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.

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

$$W_p(Q,Q') = \left(\inf_{\pi \in \Pi(Q,Q')} \int_{E\times E} \|\xi-\xi'\|^p\, \pi(d\xi,d\xi')\right)^{1/p},$$

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

$$B_{\varepsilon,p}(\hat P_N) = \{Q \in \mathcal{P}(\Xi) : W_p(Q,\hat P_N) \le \varepsilon\},$$

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

$$R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} \mathbb{E}_Q[\ell(\xi)],$$

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

$$R_{\varepsilon,p}(\hat P_N,\ell) = \inf_{\gamma \ge 0}\ \mathbb{E}_{\hat P_N}[\ell_\gamma(\xi)] + \gamma\varepsilon^p,\qquad \ell_\gamma(\xi) = \sup_{z\in\Xi} \ell(z) - \gamma\|z-\xi\|^p.$$

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

$$W_p^p(Q,Q') = \sup\left\{\int \psi\,dQ' - \int \varphi\,dQ : \varphi,\psi \text{ bounded continuous},\ \psi(\xi)-\varphi(\xi') \le \|\xi-\xi'\|^p\right\}$$ $$W_1(Q,Q') = \sup_{\mathrm{Lip}(\varphi)\le 1} \int \varphi\,dQ - \int \varphi\,dQ'$$

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

$$R_{\varepsilon,p}(\hat P_N,\ell) \le R(\hat P_N,\ell) + \varepsilon\cdot\mathrm{Lip}(\ell)$$ $$R_{\varepsilon,p}(\hat P_N,\ell) \ge \sup\left\{\tfrac1N\textstyle\sum_i \ell(\hat\xi_i+\theta_i) : \hat\xi_i+\theta_i\in\Xi,\ \tfrac1N\textstyle\sum_i\|\theta_i\|^p\le\varepsilon^p\right\}$$

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

Exact case — Theorem 10

$$\Xi = \mathbb{R}^m,\ \ell \text{ convex},\ p=1 \implies R_{\varepsilon,1}(\hat P_N,\ell) = R(\hat P_N,\ell) + \varepsilon\,\mathrm{Lip}(\ell)$$

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

Distributionally robust optimization (DRO) hedges a decision against every distribution within some ambiguity set around an estimated (nominal) distribution, rather than trusting the estimate exactly. When the ambiguity set is a ball of radius $\varepsilon$ around the empirical distribution $\hat P_N$ in the type-$p$ Wasserstein metric, the resulting worst-case risk problem inherits attractive statistical guarantees (Mohajerin Esfahani & Kuhn 2018) but is, in general, an optimization problem over an infinite-dimensional space of measures. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter surveys when this problem becomes computationally tractable. One route — the subject of this mission — discards everything about the nominal distribution except its mean vector and covariance matrix and replaces the Wasserstein ball with a set built only from these two moments, the Gelbrich hull. The construction is due to Gelbrich (1990), who first bounded the Wasserstein distance between two distributions using only their means and covariances.

Setting

Fix $\Xi \subseteq \mathbb{R}^m$, a nominal distribution $\hat P_N \in \mathcal{P}(\Xi)$, a radius $\varepsilon > 0$ and an exponent $p \ge 1$. The type-$p$ Wasserstein distance between two probability measures $Q, Q'$ on $\mathbb{R}^m$ is

$$W_p(Q,Q') = \Big(\inf_{\pi \in \Pi(Q,Q')} \int \|\xi-\xi'\|^p \, d\pi(\xi,\xi')\Big)^{1/p},$$

the infimum over couplings $\pi$ (probability measures on $\mathbb{R}^m \times \mathbb{R}^m$ with marginals $Q$ and $Q'$) of the $p$-th root of the expected $p$-th power of Euclidean distance. The Wasserstein ambiguity set is $B_{\varepsilon,p}(\hat P_N) = \{Q \in \mathcal{P}(\Xi) : W_p(Q,\hat P_N) \le \varepsilon\}$, and the worst-case risk of a loss function $\ell$ is $R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} E_Q[\ell(\xi)]$.

Suppose $\hat P_N$ has mean vector $\hat\mu$ and covariance matrix $\hat\Sigma \in S^m_+$ (the positive semidefinite $m\times m$ matrices). The mean-covariance uncertainty set is

$$U_\varepsilon(\hat\mu,\hat\Sigma) = \Big\{(\mu,\Sigma) \in \mathbb{R}^m \times S^m_+ : \|\hat\mu-\mu\|_2^2 + \mathrm{Tr}\big[\hat\Sigma+\Sigma-2(\hat\Sigma^{1/2}\Sigma\hat\Sigma^{1/2})^{1/2}\big] \le \varepsilon^2\Big\},$$

where $\Sigma^{1/2}$ is the positive-semidefinite square root. The Gelbrich hull is $G_\varepsilon(\hat\mu,\hat\Sigma) = \{Q \in \mathcal{P}(\Xi) : (E_Q[\xi],\mathrm{Cov}_Q[\xi]) \in U_\varepsilon(\hat\mu,\hat\Sigma)\}$: the distributions on $\Xi$ whose own mean and covariance lie in $U_\varepsilon(\hat\mu,\hat\Sigma)$. An elliptical distribution $E_g(\mu,\Sigma)$ has density $f(\xi) = C \cdot \det(\Sigma)^{-1} g\big((\xi-\mu)^\top\Sigma^{-1}(\xi-\mu)\big)$ for a density generator $g$ and normalizing constant $C$; two elliptical distributions "have the same density generator" when their $g$ coincide (e.g. both Gaussian, both Student-$t_\nu$ for the same $\nu$).

Formalization targets

Goal (Theorem 13, Gelbrich hull). For every $p \ge 2$,

$$B_{\varepsilon,p}(\hat P_N) \subseteq G_\varepsilon(\hat\mu,\hat\Sigma).$$

This is an outer approximation: every distribution within $\varepsilon$ of $\hat P_N$ in Wasserstein distance has a mean and covariance inside $U_\varepsilon(\hat\mu,\hat\Sigma)$, so optimizing over the Gelbrich hull instead of the Wasserstein ball can only enlarge the feasible set, never shrink it below the truth.

Supporting results. Theorem 4 (Gelbrich bound) gives the moment-only lower bound on $W_2$ that Theorem 13 is built from, with equality for elliptical distributions sharing a generator. Proposition 1 sharpens the goal's containment to an equality on the mean-covariance projection itself, under the same two conditions ($\Xi = \mathbb{R}^m$, $\hat P_N$ elliptical). Corollary 1 propagates the goal's set containment to the risk level: $R_{\varepsilon,p}(\hat P_N,\ell) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell)$ for every $\ell$, where $R_\varepsilon(\hat\mu,\hat\Sigma,\ell) = \sup_{Q \in G_\varepsilon(\hat\mu,\hat\Sigma)} E_Q[\ell(\xi)]$ is the Gelbrich risk.

Significance

Theorem 13 is the hinge between an intractable infinite-dimensional worst-case-risk problem and a tractable one: the paper goes on (Theorem 16, outside this mission's scope) to show that for quadratic loss functions and elliptical nominal distributions the Gelbrich risk itself equals the optimal value of a semidefinite program with two linear matrix inequality constraints — and that, under those same conditions, the Wasserstein worst-case risk, the Gelbrich risk and the SDP value all coincide. Corollary 1 is what makes the Gelbrich risk usable as a conservative surrogate even outside that special case: it upper-bounds the true worst-case risk for any loss function and any $p \ge 2$, at the cost of discarding all but first- and second-order information about the nominal distribution. Formalizing the goal and Corollary 1 gives the exact scope in which this moment-relaxation is licensed — the $p \ge 2$ restriction and the outer-approximation direction are both easy to get backwards, and this mission's Lean encoding fixes both irreversibly.

Difficulty

The obvious first argument is to prove containment pointwise: fix $Q \in B_{\varepsilon,p}(\hat P_N)$ and show its mean and covariance land in $U_\varepsilon(\hat\mu,\hat\Sigma)$. That reduces Theorem 13 to Proposition 1's containment half, which in turn reduces to the Gelbrich bound (Theorem 4) applied to the pair $(Q,\hat P_N)$ — the inequality direction of Theorem 4 suffices for containment; only the sharper equality direction (needed for Proposition 1's own equality clause) requires the elliptical hypothesis. The non-obvious step is Theorem 4 itself: bounding $W_2(Q,Q')$ below by a closed-form expression in the two distributions' first two moments only, for arbitrary $Q,Q'$ with those moments, requires an argument that survives every coupling $\pi$ — the paper's proof goes through a lower bound on the coupling's cross-covariance term via the eigenvalues of $\Sigma^{1/2}\Sigma'\Sigma^{1/2}$, not a direct manipulation of $W_2$'s definition.

Formalization scope

$\mathbb{R}^m$ is EuclideanSpace ℝ (Fin m); a "distribution" is a MeasureTheory.Measure on it constrained by Q Set.univ = 1 (probability) and Q Ξᶜ = 0 (support in Ξ). The Wasserstein distance is ENNReal-valued (Definition 1's infimum over couplings, matching 01-duality's convention); the worst-case and Gelbrich risks are EReal-valued suprema restricted to loss functions integrable under the candidate distribution, avoiding Mathlib's junk value for a non-integrable Bochner integral. $\Sigma^{1/2}$ is the positive-semidefinite matrix square root, picked by choice from its defining existential and applied in this mission only to matrices hypothesized (or, per Section 2.3's standing assumption, given) positive semidefinite. Elliptical distributions (IsElliptical) are represented by the paper's own density formula (a measure equal to volume.withDensity of C·det(Σ)⁻¹·g((ξ-μ)ᵀΣ⁻¹(ξ-μ)) for some C>0), together with the mean/covariance facts every theorem in this chunk reads off directly; an earlier draft kept only the latter, under which "same density generator" held vacuously for any moment-matched pair — corrected after moderation flagged it (see STATUS.md). Because 01-duality (Wasserstein distance, ambiguity set, worst-case risk) is not yet a published mission, this chunk redefines those objects locally in its own namespace rather than importing an unpublished draft, per the series' definition-reuse policy; a future upload can retire the duplication once 01-duality is live. A formalization that dropped Theorem 4's "same density generator" condition from its equality clause, or that stated the goal's containment for all $p\ge 1$ rather than $p \ge 2$, would be trivializing or simply false — both are explicit hypotheses in the Lean statements. Matrix.PosSemidef and its Loewner order carry the $S^m_+$ constraints; no elliptical-distribution or Gelbrich-hull infrastructure exists elsewhere on the platform, so this mission's definitions are original contributions reusable by any later extension (Theorem 16/17, Lemma 1/2's SDP representations) of this series.

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. https://doi.org/10.1287/educ.2019.0198
• Gelbrich, M. (1990). On a formula for the L2 Wasserstein metric between measures on Euclidean and Hilbert spaces. Mathematische Nachrichten, 147(1), 185–203.
• Mohajerin Esfahani, P., & Kuhn, D. (2018). Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations. Mathematical Programming, 171(1), 115–166.

Motivation

A decision maker who solves a distributionally robust optimization (DRO) problem over a Wasserstein ball chooses a radius $\varepsilon$ by hand, and it is natural to ask what guarantee that choice actually buys: how large must $\varepsilon$ be, as a function of the sample size $N$ and a desired confidence level, before the resulting worst-case risk is provably not an underestimate of the true (unknown-distribution) risk? Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter answers this for the mean-covariance relaxation of Wasserstein DRO introduced via the Gelbrich hull (Section 2.3): Theorem 21 gives a concentration inequality for how fast the sample mean and covariance approach the true mean and covariance, and Theorem 22 turns that concentration bound into a finite-sample statistical guarantee for the Gelbrich risk itself. This mission formalizes both.

Setting

Fix $m \in \mathbb{N}$. Let $P$ be the unknown true distribution on $\mathbb{R}^m$ with mean vector $\mu$ and covariance matrix $\Sigma \in S^m_+$, and suppose $P$ is light-tailed: there exist $\alpha > 2$ and $A > 0$ with $E_P[\exp(\|\xi\|_2^\alpha)] \le A$. Let $\hat\xi_1,\dots,\hat \xi_N$ be $N$ independent, identically distributed samples from $P$; write $P^N$ for their joint law (the $N$-fold product measure) and $\hat\mu, \hat\Sigma$ for the resulting sample mean and sample covariance, i.e. the mean and covariance of the empirical distribution $\hat P_N = \frac{1}{N}\sum_i \delta_{\hat\xi_i}$. Recall from the Gelbrich construction the mean-covariance uncertainty set $U_\varepsilon(\hat\mu,\hat\Sigma) = \{(\mu,\Sigma) \in \mathbb{R}^m \times S^m_+ : \|\hat\mu-\mu\|_2^2 + \mathrm{Tr}[\hat\Sigma+\Sigma-2(\hat\Sigma^{1/2} \Sigma\hat\Sigma^{1/2})^{1/2}] \le \varepsilon^2\}$, and the Gelbrich risk $R_\varepsilon(\hat\mu,\hat\Sigma,\ell) = \sup_{Q \in G_\varepsilon(\hat\mu,\hat\Sigma)} E_Q[\ell(\xi)]$ of a loss function $\ell$ over the Gelbrich hull $G_\varepsilon(\hat\mu,\hat \Sigma)$.

Formalization targets

Milestone (Theorem 21, concentration inequalities II). There is $c > 1$, depending on $P$ only through $\mu,\Sigma,\alpha,A,m$ (not on any finer feature of $P$), such that for every $\eta \in (0,1]$,

$$P^N\big[(\mu,\Sigma) \in U_\varepsilon(\hat\mu,\hat\Sigma)\big] \ge 1-\eta \quad \text{whenever} \quad \varepsilon \ge \varepsilon_N(\eta) := \frac{\log(c/\eta)}{\sqrt N}.$$

Goal (Theorem 22(a), finite sample guarantees II). Under the same hypotheses, for every $\eta \in (0,1)$ and $\varepsilon \ge \varepsilon_N(\eta)$,

$$P^N\Big\{R(P,\ell) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell) \;\; \forall \ell \in L\Big\} \ge 1-\eta.$$

With probability at least $1-\eta$ over the draw of the training sample, the Gelbrich risk computed from that sample upper-bounds the true risk of every admissible loss function simultaneously — not just of one fixed $\ell$ chosen in advance. (The paper's part (b), the analogous guarantee $P^N\{R(P,\ell^\star) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell^\star)\} \ge 1-\eta$ for the specific optimizer $\ell^\star$ of the Gelbrich risk minimization problem, is not formalized in this mission — see Formalization scope.)

Significance

Theorem 22 is what makes the Gelbrich-risk relaxation of Wasserstein DRO more than a computational convenience: it certifies that solving the tractable Gelbrich risk minimization problem gives a decision whose true out-of-sample risk is, with high probability, no worse than the value the solver reports — a genuine confidence guarantee, not merely an approximation of the Wasserstein worst-case risk. Theorem 21's rate, $\varepsilon_N(\eta) = O(N^{-1/2})$, is also of independent interest: it is dimension-free (no curse of dimensionality), in contrast to the paper's earlier general-distribution concentration result (Theorem 18, out of scope for this mission) whose rate degrades with $m$. Formalizing Theorem 21 fixes, machine-checkably, the exact functional form of $\varepsilon_N(\eta)$ and the precise sense in which $c$ is "distribution-free" given $(\mu,\Sigma,\alpha,A,m)$ — a subtlety easy to state informally but easy to get wrong formally (see Difficulty).

Difficulty

The central formalization difficulty is not proving the theorems (both are left as sorry in this draft) but stating the existential constant $c$ correctly. The paper says $c$ "depends on $P$ only through $\mu,\Sigma,\alpha,A,m$" — informally, a promise that $c$ is uniform across every distribution $P$ sharing those five parameters, not merely that some $c$ exists for each $P$ separately (a vacuously true, much weaker statement obtained by naively quantifying $c$ after $P$). The correct encoding places $\exists c$ before the universal quantifier over $P$: for fixed $(\mu,\Sigma,\alpha,A,m)$, one $c$ must work for every $P$ with that mean, covariance, and tail bound. Getting this quantifier order backwards silently converts a genuine finite-sample guarantee into a triviality (FAITHFULNESS_TRAPS.md trap 8).

Formalization scope

Distributions live on EuclideanSpace ℝ (Fin m); $P^N$, the law of $N$ iid samples, is the $N$-fold product measure MeasureTheory.Measure.pi (fun _ => P) on Fin N → EuclideanSpace ℝ (Fin m) — an event about the random sample sequence is a set of such tuples, and "$P^N[\text{event}] \ge 1-\eta$" is that product measure's mass on the event set. All risk and uncertainty-set definitions (meanVector, covarianceMatrix, meanCovarianceUncertaintySet, gelbrichHull, gelbrichRisk, nominalRisk, empiricalDistribution) are redefined locally in this chapter's own namespace, matching 02-gelbrich's conventions exactly, since neither 01-duality nor 02-gelbrich is yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once those missions are live. The existential constant c is placed before the universal quantifier over P in both theorems, exactly capturing "depends on P only through µ,Σ,α,A,m" — see Difficulty. Only Theorem 22's part (a) (the uniform bound over a loss class L) is formalized; part (b) — the bound for the specific optimizer ℓ* of the Gelbrich risk minimization problem (19) — is left out, because it requires first formalizing "ℓ* is an optimizer of problem (19)" as an object (an infimum-attaining selection over a data-dependent optimization problem), which is additional infrastructure this mission's time budget did not cover; formalizing it as an unconditional bound over an arbitrary data-dependent ℓ* (dropping the optimality hypothesis) would be unfaithful — the guarantee genuinely depends on ℓ* being an optimizer, not an arbitrary measurable function of the sample. The goal theorem also carries hΞ, stating Ξ contains the support of P (the paper's own standing assumption, p. 6, for every later use of Ξ), and hLInt, an Integrable ℓ P guard for every ℓ ∈ L, matching Assumption 1 (p. 9); both were added after moderation found the goal's original statement, without them, admitted a counter-instance (Ξ = ∅ collapses the Gelbrich hull to empty and the risk supremum to ⊥, making the guarantee provably false rather than merely undisclosed). Theorem 18 (the general, dimension- dependent concentration inequality with its piecewise ε_N(η) formula) and Theorems 19/20/23 (its downstream guarantees and the asymptotic-consistency results) are out of scope for this mission, which targets the Gelbrich-risk branch (Theorems 21/22) specifically.

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. https://doi.org/10.1287/educ.2019.0198
• Fournier, N., & Guillin, A. (2015). On the rate of convergence in Wasserstein distance of the empirical measure. Probability Theory and Related Fields, 162(3), 707–738.
• Gao, R., & Kleywegt, A. J. (2023). Distributionally robust stochastic optimization with Wasserstein distance. Mathematics of Operations Research, 48(2), 603–655.

Motivation

Regularization — adding a penalty on model complexity to an empirical risk minimization objective — is one of the oldest and most reliably effective tools in statistical learning: ridge regression, LASSO, and margin-based support vector machines all fit this template. For decades the regularization weight and penalty function were chosen heuristically or by cross-validation, with only asymptotic or worst-case generalization bounds explaining why they help. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter on Wasserstein distributionally robust optimization (DRO) gives regularization a different, non-asymptotic justification: a decision rule that is robust to adversarial perturbations of its training data, measured in Wasserstein distance, is exactly a regularized empirical risk minimizer — no approximation, no asymptotics. This mission formalizes the general form of that equivalence, Theorem 10 (p. 14), which underlies every regularization-by-robustification result the chapter derives for classification and regression alike.

Setting

Fix a normed space $\Xi = \mathbb{R}^m$, a convex loss function $\ell : \Xi \to \mathbb{R}$, a radius $\varepsilon \ge 0$, and $N$ training samples $\hat\xi_1,\dots,\hat\xi_N \in \Xi$ ($N \ge 1$). The empirical distribution is $\hat P_N = \frac{1}{N}\sum_{i=1}^N \delta_{\hat\xi_i}$. The worst-case risk of $\ell$ at radius $\varepsilon$ (eq. (6), p. 6) is

$$R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} E_Q[\ell(\xi)],$$

where $B_{\varepsilon,p}(\hat P_N)$ is the type-$p$ Wasserstein ball of radius $\varepsilon$ around $\hat P_N$ (Definition 1, p. 3) — the set of probability measures on $\Xi$ within Wasserstein distance $\varepsilon$ of the empirical distribution, under a norm $\|\cdot\|$ on $\Xi$ and its transportation exponent $p$. The Lipschitz modulus $\mathrm{Lip}(\ell) = \sup_{\xi\ne\xi'} \frac{|\ell(\xi)-\ell(\xi')|}{\|\xi-\xi'\|}$ (possibly $+\infty$) measures how fast $\ell$ can grow.

Formalization targets

Goal (Theorem 10, convex loss and $p=1$). If $\ell$ is convex and $p=1$, then the worst-case risk of $\ell$ over the type-1 Wasserstein ball around the empirical distribution coincides with the Lipschitz-regularized empirical loss:

$$R_{\varepsilon,1}(\hat P_N,\ell) = R(\hat P_N,\ell) + \varepsilon \cdot \mathrm{Lip}(\ell),$$

where $R(\hat P_N,\ell) = \frac{1}{N}\sum_{i=1}^N \ell(\hat\xi_i)$ is the ordinary empirical risk. The left side is the worst-case expected loss under adversarial perturbations of the training data of bounded aggregate Wasserstein cost; the right side is the ordinary empirical risk plus a regularization term proportional to the perturbation radius $\varepsilon$ and the loss's own Lipschitz modulus — no approximation, an exact equality for every convex $\ell$.

Significance

This is the single result underlying every specific regularization-by-robustification corollary the chapter derives — the $\ell_2$-regularized SVM and its $\ell_1$/$\ell_\infty$ variants, regularized logistic regression, and the regression analogue with a Lipschitz loss (Proposition 3) — because each of those is obtained by substituting a specific convex, Lipschitz loss (hinge, logloss, a linear-model margin loss) for the general $\ell$ here and reading off $\mathrm{Lip}(\ell)$ in closed form. Theorem 10 is exact ($p=1$, Ξ = R^m) precisely because a type-1 transportation cost is dual to the Lipschitz modulus (a consequence of the Kantorovich- Rubinstein duality this book's earlier duality theorems establish), whereas the corresponding statement for $p \ge 2$ (Theorem 11 elsewhere in the chapter) needs a strictly stronger hypothesis on $\ell$. Formalizing Theorem 10 fixes, machine-checkably, the exact scope of the equivalence — which losses qualify (convex, no boundedness or smoothness needed), which transportation exponent is required ($p=1$, not any $p\ge1$), and that the equality is exact, not an upper or lower bound — the single fact every classification- and regression-specific robustification corollary in the chapter cites without re-deriving.

Difficulty

The natural first attempt treats the worst-case risk as an instance of the general finite convex reduction (Theorem 8, which needs $\ell$ or a related concave/convex-conjugate structure and applies for a general norm exponent $p,q$ with $1/p+1/q=1$) and specializes it to $p=1$. This is not the paper's own route for Theorem 10: at $p=1$ the dual exponent $q=\infty$, and the general finite-convex-program reduction (11) degenerates in a way that is more naturally derived directly from the type-1 Wasserstein distance's own dual (Kantorovich-Rubinstein) representation — a Lipschitz test function pairs exactly with a type-1 transportation cost, which is why the answer is Lipschitz-regularization and not some other penalty. The Lean statement records only the final equality (the proof itself, via Theorem 8 or the direct Kantorovich-Rubinstein route, is left as sorry, as required for a draft item), but the choice of which milestones would support that proof is exactly this: the type-1/Lipschitz-modulus duality is a structurally different argument from the finite-convex-program machinery Theorem 8 needs for other $p$, which is why this chapter's earlier draft mistakenly tried to reach a specialization of Theorem 10 (Proposition 2, restated for a labeled, $\kappa=\infty$ ambiguity set) through a finite-atom shortcut that does not actually capture the general type-1 ball Theorem 10's own proof needs — see Formalization scope.

Formalization scope

$\Xi$ is EuclideanSpace ℝ (Fin m) (fixed to Set.univ, matching the theorem's own "Ξ = R^m" hypothesis) with an arbitrary fixed norm as a type-class parameter, not specialized to Euclidean. The worst-case risk, Wasserstein distance, ambiguity set, nominal risk, empirical distribution and Lipschitz modulus are all redefined locally in this chapter's own namespace, verbatim restatements of 01-duality's own drafts of the same objects (identical EReal/ENNReal/Integrable conventions), because 01-duality is not yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once it is live. hN : 0 < N excludes the empty-sample case the paper's own "N training samples" presupposes; hℓ : Integrable ℓ (empiricalDistribution ξhat) guards the empirical risk's Bochner integral (automatically satisfied under any real-valued ℓ since the empirical distribution is a finite convex combination of Dirac masses, but stated explicitly rather than assumed silently). No constant is pinned to a numeral. This mission originally targeted Proposition 2 (regularization by robustification for classification, p. 25), a specialization of Theorem 10 to a labeled, κ=∞ input-output ambiguity set — but that draft's κ=∞ ambiguity set restricted admissible perturbations to a finite family of exactly N atoms, each sample's entire mass moving as one indivisible unit, which is a strict, non-faithful subset of the true κ=∞ Wasserstein ball (splitting a sample's mass across several destinations is a legitimate, and for a convex loss strictly more powerful, perturbation by Jensen's inequality). This made the goal theorem false for at least one of the three loss functions (Table 1) the mission itself certified as covered (logloss), not merely narrower than the paper's claim — moderation caught this and required either a faithful general-ambiguity-set reformulation or retargeting the goal. This mission takes the latter: Theorem 10 itself, already correctly and generally stated using the unrestricted Wasserstein ball throughout, is now the goal, with no further milestone (no other numbered result in this chunk's scope is needed for Theorem 10's own statement beyond the shared definitions above). A future mission in this series can revisit Proposition 2/3 with a properly general labeled ambiguity set once that construction (label-pinned marginal plus an aggregate coupling condition on the input coordinate, rather than a finite atom family) is built.

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. https://doi.org/10.1287/educ.2019.0198
• Shafieezadeh-Abadeh, S., Esfahani, P. M., & Kuhn, D. (2015). Distributionally robust logistic regression. Advances in Neural Information Processing Systems, 28.
• Blanchet, J., Kang, Y., & Murthy, K. (2019). Robust Wasserstein profile inference and applications to machine learning. Journal of Applied Probability, 56(3), 830–857.

Motivation

Minimum mean square error (MMSE) estimation — predicting a signal $x$ from a noisy observation $y$ by minimizing expected squared prediction error — underlies linear systems theory, linear regression, Kalman filtering, and multiple-input multiple-output signal processing. Its classical solution assumes the joint distribution of $(x,y)$ is known exactly; in practice it is estimated from data, and the estimator inherits sampling error and model risk. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter shows that hedging the MMSE objective against every distribution in a Wasserstein ball around the empirical distribution — an infinite-dimensional worst case over an intractable set of measures, a priori — collapses to a tractable, finite-dimensional convex semidefinite program (Theorem 25, p. 29), building on the Gelbrich-hull machinery of Section 2.3. This mission formalizes that reduction.

Setting

Fix $m_x, m_y \in \mathbb{N}$ and let $\xi = (x,y) \in \mathbb{R}^{m_x} \times \mathbb{R}^{m_y}$ be a random vector: $x$ the signal to be estimated, $y$ the observation. An estimator is a measurable function $\psi : \mathbb{R}^{m_y} \to \mathbb{R}^{m_x}$; write $\Psi$ for the family of all estimators. The distribution of $\xi$ is only known to lie in a type-2 Wasserstein ball $B_{\varepsilon,2}(\hat P_N)$ centered at an elliptical nominal distribution $\hat P_N = E_g(\hat\mu,\hat\Sigma)$ with nominal mean $\hat\mu \in \mathbb{R}^m$ ($m=m_x+m_y$), nominal covariance $\hat\Sigma \in S^m_+$, and density generator $g$. The distributionally robust MMSE estimation problem is

$$\inf_{\psi \in \Psi} \sup_{Q \in B_{\varepsilon,2}(\hat P_N)} E_Q\big[\|x-\psi(y)\|_2^2\big]. \tag{35}$$

Writing $\hat\Sigma = \begin{pmatrix}\hat\Sigma_{xx}&\hat\Sigma_{xy}\\\hat\Sigma_{yx}& \hat\Sigma_{yy}\end{pmatrix}$ blockwise, the nonlinear convex SDP

$$\max_S f(S) = \mathrm{Tr}[S_{xx} - S_{xy}S_{yy}^{-1}S_{yx}] \quad \text{s.t.} \quad S = \begin{pmatrix}S_{xx}&S_{xy}\\S_{yx}&S_{yy}\end{pmatrix} \succeq 0,\; S_{xx} \succeq 0,\; S_{yy} \succeq 0,\; \mathrm{Tr}[S+\hat\Sigma-2(\hat\Sigma^{1/2}S\hat\Sigma^{1/2})^{1/2}] \le \varepsilon^2,\; S \succeq \lambda_{\min}(\hat\Sigma) I \tag{36}$$

is the finite-dimensional relaxation the chapter builds toward.

Formalization targets

Goal (Theorem 25, distributionally robust MMSE estimator). If $\hat\Sigma \succ 0$, then the optimal value of problem (35) equals the optimal value of SDP (36). Moreover, if $S^\star$ is optimal in (36) with $S^\star_{yy}$ invertible, then the affine function

$$\psi^\star(y) = S^\star_{xy}(S^\star_{yy})^{-1}(y-\hat\mu_y) + \hat\mu_x$$

attains the outer infimum of (35) — it is a distributionally robust MMSE estimator, exhibited in closed form from an SDP optimizer.

Significance

Theorem 25 reduces an a priori infinite-dimensional, worst-case functional optimization problem (an infimum over all measurable estimators of a supremum over all distributions within a Wasserstein ball) to a finite convex program with one linear matrix inequality, one Loewner-order lower bound, and one trace/matrix-square-root constraint — solvable in polynomial time, with the optimal estimator recovered in closed form from the SDP's optimal block matrix. It shows that robustifying MMSE estimation against distributional ambiguity does not sacrifice tractability: the resulting estimator remains affine, the same functional form as the classical (non-robust) best linear unbiased estimator, only with its coefficients drawn from a regularized covariance estimate rather than the raw sample covariance. Formalizing it fixes, machine-checkably, the exact shape of that regularization — which SDP constraints are load-bearing (the Loewner lower bound in particular rules out a numerically unstable near-singular $S_{yy}$) and which conditions ($\hat\Sigma \succ 0$, $S^\star_{yy}$ invertible) the closed-form estimator formula actually needs.

Difficulty

The paper's own remark (p. 29) names the two nontrivial steps: first, "establishing a minimax theorem for (35) and exploiting the properties of elliptical distributions" to show the outer infimum is attained by an affine estimator — a priori (35) ranges over all measurable $\psi$, and there is no obvious reason the worst case forces linearity. Second, "combining this structural insight with Theorem 16" (the SDP-representability result for indefinite quadratic losses under an elliptical nominal distribution, itself a nontrivial closed-form reduction of an infinite-dimensional worst-case risk) to convert the now-restricted problem over affine estimators into the finite SDP (36). Neither step is a routine consequence of the ambiguity-set definitions alone; each requires structural facts about elliptical distributions and quadratic losses proved earlier in the chapter.

Formalization scope

The signal-observation space is EuclideanSpace ℝ (Fin mx ⊕ Fin my), with $x$ and $y$ recovered as the two summand projections; the block matrix $S$ is Matrix (Fin mx ⊕ Fin my) (Fin mx ⊕ Fin my) ℝ, and Matrix.toBlocks₁₁/toBlocks₁₂/toBlocks₂₁/toBlocks₂₂ give its four blocks. The constraint "$S_{xy}=S_{yx}^\top$" is not stated as a separate hypothesis: it follows automatically once $S$ is symmetric (implied by S.PosSemidef), so encoding the feasible set from a single symmetric S rather than four independently-quantified blocks makes it structurally impossible to drop — see pitfall 4 of BRIEF.md. The outer infimum of problem (35) ranges only over measurable $\psi$ (Measurable ψ on the binder), matching the paper's own definition of $\Psi$ as "the family of all possible measurable estimators" (p. 29) exactly. λ_min(Σ̂) is taken as a hypothesis parameter characterized by the two properties that make it the minimum ("≤ every eigenvalue of Σ̂, and attained by some eigenvalue"), rather than invoking a specific Mathlib min-eigenvalue API by name. S_{yy}⁻¹ uses the ordinary matrix inverse (junk zero matrix when singular), matching the paper's literal notation; S^\star_{yy} invertible is stated as an added hypothesis, not present verbatim on the page, because the paper leaves the formula's well-definedness implicit — disclosed per pitfall 5 rather than silently assumed away. The paper's own "which is always solvable" clause is not asserted: Theorem 25 states, as part of itself, that SDP (36) attains its maximum (an unconditional existence claim for an optimal $S^\star$); this formalization states only the conditional consequences of such an $S^\star$ existing, not that one does — proving or asserting solvability is out of this mission's scope, so the Lean statement is strictly weaker than Theorem 25's own conclusion on this point, disclosed rather than silently dropped. All risk-style suprema are EReal-valued and Integrable-guarded, matching the series' convention. No milestone theorem is included: the paper's own proof sketch derives (33)'s and by extension (36)'s SDP "via Theorem 16", but Theorem 16 (indefinite quadratic loss and $p=2$, eq. 23) was itself judged too heavy to state faithfully in 02-gelbrich's time budget and is not redefined here either — see STATUS.md. Theorem 24 (the Wasserstein shrinkage estimator, this chapter's originally recommended goal) is out of scope: its closed-form eigenvalue transformation (eq. 34a/34b) requires transcribing nested square roots from a rendered PDF page that this session's time budget did not allow verifying to the standard the brief demands (pitfall 1); the brief's own documented fallback to Theorem 25 was taken instead.

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. https://doi.org/10.1287/educ.2019.0198
• Nguyen, V. A., Shafieezadeh-Abadeh, S., Yue, M.-C., Kuhn, D., & Wiesemann, W. (2021). Optimistic distributionally robust optimization for nonparametric likelihood approximation. Advances in Neural Information Processing Systems, 32.
• Shafieezadeh-Abadeh, S., Nguyen, V. A., Kuhn, D., & Mohajerin Esfahani, P. (2018). Wasserstein distributionally robust Kalman filtering. Advances in Neural Information Processing Systems, 31.

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]).