All missions

Motivation

In many operational problems (shortest paths, assignment, planning) the decision solves a linear program whose cost vector is unknown at decision time and is predicted from contextual features. The predict-then-optimize pipeline fits a model $f$ that maps a feature vector $x$ to a predicted cost vector $\hat c=f(x)$, and then acts on the decision that is optimal for $\hat c$. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed to measure the quality of such a model not by the prediction error but by the SPO loss (Smart Predict-then-Optimize loss): the excess true cost of the decision induced by the prediction over the best decision in hindsight.

The question is whether a small SPO loss on the training sample implies a small SPO loss on new data, uniformly over the models a training procedure may return. The SPO loss is neither convex nor continuous in the prediction, so the standard Lipschitz-based bounds for regression do not apply. El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3, Mathematics of Operations Research 2023; a preliminary version appeared at NeurIPS 2019) give the first such generalization bounds. This mission formalizes their first one, for polyhedral feasible regions, which treats every vertex of the feasible region as a class label of a multiclass classification problem. The bound has since been used by later work, e.g. Hu, Kallus and Mao (Fast rates for contextual linear optimization, Management Science 2022), who sharpen it by a $\sqrt{\log n}$ factor (as noted on p. 4 of the paper).

Setting

A feasible region $S\subseteq\mathbb R^d$ is nonempty, compact and convex. For a cost vector $c\in\mathbb R^d$ the nominal problem is $\min_{w\in S}c^\top w$. An optimization oracle is a fixed map $w^*:\mathbb R^d\to S$ with $w^*(c)\in\arg\min_{w\in S}c^\top w$ for every $c$; nothing is assumed about how it breaks ties. The SPO loss of a prediction $\hat c$ when the realized cost is $c$ is

$$\ell_{\rm SPO}(\hat c,c)=c^\top w^*(\hat c)-c^\top w^*(c)\ \ge 0 .$$

The linear optimization gap is $\omega_S(c)=\max_{w\in S}c^\top w-\min_{w\in S}c^\top w$, and for a set $\mathcal C$ of cost vectors $\omega_S(\mathcal C)=\sup_{c\in\mathcal C}\omega_S(c)$; the SPO loss of a cost in $\mathcal C$ lies in $[0,\omega_S(\mathcal C)]$.

Data are pairs $(x,c)$ drawn from a distribution $\mathcal D$ on $\mathcal X\times\mathcal C$. A hypothesis class $\mathcal H$ is a family of predictors $f:\mathcal X\to\mathbb R^d$. The SPO risk is $R_{\rm SPO}(f)=\mathbb E_{\mathcal D}[\ell_{\rm SPO}(f(x),c)]$, and on an i.i.d. sample $(x_1,c_1),\dots,(x_n,c_n)$ the empirical SPO risk is $\hat R_{\rm SPO}(f)=\frac1n\sum_i\ell_{\rm SPO}(f(x_i),c_i)$. The empirical Rademacher complexity with respect to the SPO loss is

$$\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)=\mathbb E_\sigma\Big[\sup_{f\in\mathcal H}\frac1n\sum_{i=1}^n\sigma_i\,\ell_{\rm SPO}(f(x_i),c_i)\Big]$$

with independent uniform signs $\sigma_i\in\{\pm1\}$, and $\mathfrak R^n_{\rm SPO}(\mathcal H)$ is its expectation over the sample.

The decisions induced by $\mathcal H$ form the class $w^*(\mathcal H)=\{x\mapsto w^*(f(x)):f\in\mathcal H\}$. A class $\mathcal F$ N-shatters a finite set $\mathbb X\subseteq\mathcal X$ if there are two labelings $g_1,g_2$ that differ at every point of $\mathbb X$ such that every mixture of them (follow $g_1$ on a subset $T$, $g_2$ on the rest) is realized by some member of $\mathcal F$. The Natarajan dimension $d_N(\mathcal F)$ is the largest size of an N-shattered set. When $S$ is a polyhedron, $\mathfrak S$ denotes its finite set of extreme points.

Formalization targets

Goal: Theorem 2, second display (p. 11)

For a polyhedral $S$ and every $\delta>0$, with probability at least $1-\delta$ over an i.i.d. sample of size $n$, every $f\in\mathcal H$ satisfies

$$R_{\rm SPO}(f)\le\hat R_{\rm SPO}(f)+2\,\omega_S(\mathcal C)\sqrt{\frac{2d_N(w^*(\mathcal H))\log(n|\mathfrak S|^2)}{n}}+\omega_S(\mathcal C)\sqrt{\frac{\log(1/\delta)}{2n}} .$$

Milestones, in attack order

1. Theorem 1 (p. 9): with probability $1-\delta$, $R_{\rm SPO}(f)\le\hat R_{\rm SPO}(f)+2\mathfrak R^n_{\rm SPO}(\mathcal H)+\omega_S(\mathcal C)\sqrt{\log(1/\delta)/(2n)}$ for all $f\in\mathcal H$.
2. Massart step (Appendix B.1, p. 31): for a fixed sample with costs in $\mathcal C$, $\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)\le\omega_S(\mathcal C)\sqrt{2\log|\mathfrak F_{|\mathbb X}|/n}$, where $\mathfrak F_{|\mathbb X}$ is the set of decision vectors $(w^*(f(x_1)),\dots,w^*(f(x_n)))$.
3. Natarajan lemma (cited on p. 31; proved on the platform as UnderstandingML.natarajan_lemma): a class from an $m$-point set to $k$ labels with Natarajan dimension $d$ has at most $m^d k^{2d}$ members.
4. Empirical bound (Appendix B.1, p. 31): for a fixed sample, $\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)\le\omega_S(\mathcal C)\sqrt{2d_N(w^*(\mathcal H))\log(n|\mathfrak S|^2)/n}$.
5. Theorem 2, first display (p. 11): the same bound for the expected complexity $\mathfrak R^n_{\rm SPO}(\mathcal H)$.

Significance

The bound controls the out-of-sample decision cost of every predictor in the class, not only of an empirical risk minimizer, so it applies to any training procedure (SPO+ surrogate minimization, decision trees, heuristics) that returns a member of $\mathcal H$. Its dependence on the feasible region is only through $\omega_S(\mathcal C)$ and $\log|\mathfrak S|$: the number of vertices of a combinatorial polytope is typically exponential in $d$, and enters only logarithmically. For linear predictors $x\mapsto Bx$ the paper's Corollary 2 bounds $d_N(w^*(\mathcal H_{\rm lin}))$ by $dp$, giving a rate of order $\sqrt{dp\log(n|\mathfrak S|)/n}$.

The results are proved in the paper; this mission formalizes them. No statement about predict-then-optimize or the SPO loss is known to have a machine-checked proof. The platform already has the Natarajan lemma (proved) and several Massart-type lemmas for generic classes; this mission connects that multiclass machinery to decision losses, and its Theorem 1 is a reusable Rademacher generalization bound for a loss with range $[0,\omega]$.

Difficulty

The obvious route through Lipschitz contraction fails: the SPO loss jumps when the prediction crosses a point where the optimum is not unique, so the Rademacher complexity of the composed class cannot be bounded by that of $\mathcal H$ times a Lipschitz constant. Any argument through the finitely many vertices of $S$ needs the decisions $w^*(f(x_i))$ to take finitely many values on a sample, i.e. the oracle to return vertices; for an oracle that returns a non-vertex optimal point under ties, $w^*(\mathcal H)$ may take infinitely many values on a sample. On the probabilistic side, the passage from the empirical to the expected complexity and the McDiarmid concentration step (Theorem 1) require the suprema over an uncountable class to be measurable, which the paper does not discuss.

Formalization scope

Lean works in $\mathbb R^d$ = EuclideanSpace ℝ (Fin d); cost vectors and decisions live in the same space and $c^\top w$ is the inner product. The standing assumptions of §2 are hypotheses of every theorem: $S$ nonempty, compact and convex; $w^*$ an arbitrary oracle (a hypothesis IsOracle S w, never a specific selection); $\mathcal C$ nonempty and bounded, with the cost component of $\mathcal D$ in $\mathcal C$ almost surely (or, for fixed-sample statements, every $c_i\in\mathcal C$); $n\ge1$. "Polyhedron" means the solution set of finitely many linear inequalities; with compactness it is a polytope, and $|\mathfrak S|$ is the cardinality of Set.extremePoints ℝ S. The expectation over signs is the exact average over the $2^n$ sign vectors; $R_{\rm SPO}$ and $\mathfrak R^n_{\rm SPO}$ are Bochner integrals. "With probability at least $1-\delta$" is stated as: the product measure of the set of samples on which some $f\in\mathcal H$ violates the bound is at most $\delta$.

The formalization commits to the following disclosed additions:

• In the empirical bound, Theorem 2 and its first display, the oracle returns extreme points of $S$. This is the proof's own "w.l.o.g." (p. 31), made explicit because p. 10 allows non-vertex outputs under ties. The hypothesis is needed: on the unit square, an oracle that returns distinct interior points of an edge under ties can have $d_N(w^*(\mathcal H))=1$ and empirical complexity near $\frac12$, which exceeds the printed bound for large $n$.
• The Natarajan dimension is not defined as a number (a supremum in $\mathbb N$ would silently be $0$ for unboundedly large shattered sets). Statements carry a natural number $k$ bounding the size of every N-shattered set, in place of $d_N(w^*(\mathcal H))$. This is equivalent when $d_N$ is finite; the printed bound is vacuous otherwise.
• Theorem 1 and the goal carry three measurability hypotheses: each loss function $z\mapsto\ell_{\rm SPO}(f(z_1),z_2)$ is measurable; the uniform deviation $\sup_f(R_{\rm SPO}(f)-\hat R_{\rm SPO}(f))$ and, for each sign vector, the signed supremum $\sup_f\frac1n\sum_i\sigma_i\ell_{\rm SPO}(f(x_i),c_i)$ are almost-everywhere measurable functions of the sample. Without them the integral defining $\mathfrak R^n_{\rm SPO}$ could default to $0$.
• The Massart step assumes $\mathfrak F_{|\mathbb X}$ finite, the case in which its printed right-hand side is finite.

A formalization that let $d_N$ be an sSup in $\mathbb N$, or chose a specific tie-breaking oracle inside the definitions, would prove a different and in part trivial statement; both are excluded.

Infrastructure needed: McDiarmid's bounded-differences inequality and symmetrization for the product measure; Massart's finite-class lemma (a proved version is on the platform as RademacherMassart.rad_le_massart, with its own normalization); the Natarajan lemma (proved, UnderstandingML.natarajan_lemma, stated with its own but identical notion of N-shattering over finite types); finiteness and nonemptiness of the extreme points of a nonempty polytope. Theorem 1 and the Massart step do not use polyhedrality and are reusable for any bounded decision loss. Contributions of these infrastructure lemmas are welcome.

Selected references

• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, arXiv:1905.11488v3, 2022; Mathematics of Operations Research, 2023. https://arxiv.org/abs/1905.11488
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 9–26, 2022. https://arxiv.org/abs/1710.08005
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian complexities: risk bounds and structural results, Journal of Machine Learning Research 3, 463–482, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• B. K. Natarajan, On learning sets and functions, Machine Learning 4(1), 67–97, 1989. https://doi.org/10.1007/BF00114804
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014 (Lemma 29.4). https://doi.org/10.1017/CBO9781107298019
• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018 (Theorem 3.3, Corollary 3.8). https://cs.nyu.edu/~mohri/mlbook/

Motivation

In Witten's cubic open string field theory (Witten 1986) the interaction glues half-strings together, and in the usual center-of-mass variables the action contains infinitely many time derivatives. Such a theory has no evident initial value formulation, which obstructs a Hamiltonian treatment and a direct discussion of causality.

Erler and Gross (2004) show that after a unitary change of basis in which the string field depends on the lightcone component of the string midpoint $x^+(\pi/2)$ (and on transverse center-of-mass coordinates), the cubic vertex contains no derivatives with respect to lightcone time. This reduces to five linear relations among the Neumann coefficients of the three-string vertex, the midpoint identities (A.6)–(A.10) of the paper. One of them, (A.8), is a closed numerical identity: a specific infinite series built from Neumann coefficients equals $-\ln\frac{27}{16}$, where $\ln\frac{27}{16}=V_{00}$ is the zero-mode Neumann coefficient. This mission formalizes that identity and the chain of intermediate results the paper uses to prove it (Appendix B), together with a divergence statement from Section 2 explaining why other midpoint bases fail.

Setting

Define real constants $A_k$ ($k\ge0$) by the expansion

$$\left(\frac{1+iz}{1-iz}\right)^{1/3}=\exp\!\left(\tfrac{2i}{3}\tan^{-1}z\right)=1+\sum_{n\ge1}A_{2n}z^{2n}+i\sum_{n\ge1}A_{2n-1}z^{2n-1}.$$

For real $z$ the left side is $\cos(\tfrac23\arctan z)+i\sin(\tfrac23\arctan z)$, so $A_{2n}$ is the $2n$-th Taylor coefficient of $\cos(\tfrac23\arctan z)$ at $0$ (e.g. $A_2=-\tfrac29$). The even Neumann vector and the vector $\beta$ are

$$m_{2n}=-\frac23\,\frac{A_{2n}}{\sqrt{2n}},\qquad \beta_k=\frac{\cos(k\pi/2)}{\sqrt k},\quad\text{so }\beta_{2n}=\frac{(-1)^n}{\sqrt{2n}}.$$

In Lean these are ErlerGross.neumannA, ErlerGross.neumannMEven (with neumannMEven n $=m_{2n}$) and ErlerGross.betaVec. Two auxiliary objects appear in the proof: the (B.3) terms

$$b_n=\frac{2}{2n-1}-\frac{1}{2n-\frac23}-\frac{1}{2n-\frac43}\qquad(n\ge1),$$

(ErlerGross.b3Term) and the $\kappa$-basis integrand

$$g(\kappa)=\frac{1-\cosh\frac{\pi\kappa}{2}}{1+2\cosh\frac{\pi\kappa}{2}}\cdot\frac{1}{2\kappa\sinh\frac{\pi\kappa}{2}}$$

(ErlerGross.kappaIntegrand), which arises from the continuous spectrum $\kappa\in\mathbb R$ of the Neumann matrices (Rastelli–Sen–Zwiebach 2001).

Formalization targets

Goal — midpoint identity (A.8)

$$\ln\frac{27}{16}+\sum_{n\ge1}3\,m_{2n}\beta_{2n}=0,$$

formalized as: the series $\sum_{n\ge1}3m_{2n}\beta_{2n}$ converges absolutely (Lean HasSum) to $-\ln\frac{27}{16}$.

Milestones (Appendix B and Section 2)

• $\kappa$-basis representation: $g$ is integrable and $\sum_{n\ge1}3m_{2n}\beta_{2n}=2\int_{\mathbb R}g$.
• Residue evaluation: $\int_{\mathbb R}g=\sum_{n\ge1}b_n$.
• Eq. (B.3): $\sum_{n\ge1}3m_{2n}\beta_{2n}=2\sum_{n\ge1}b_n$.
• Auxiliary series: $\sum_{n\ge1}\frac{1}{n(2n+1)}=2-2\ln2$ and $\sum_{n\ge1}\frac{1}{n(9n^2-1)}=\frac32(\ln3-1)$.
• Closed form: $\sum_{n\ge1}b_n=-\frac12\ln\frac{27}{16}$.
• Integral formula: $\int_0^\infty\frac{\cosh ax}{\cosh bx}\,dx=\frac{\pi}{2b}\frac{1}{\cos\frac{\pi a}{2b}}$ for complex $a,b$ with $|\Re a|<\Re b$.
• Section 2: for any real regulator with $\omega_{2n}\to0$, $\sum_{n\ge1}\frac{((-1)^n-\omega_{2n})^2}{2n}=+\infty$.

Significance

In the paper, (A.8) is one of the relations which, together with (A.6), (A.7), (A.9), (A.10), removes lightcone-time derivatives from the cubic vertex. This is what gives the theory an initial value formulation in lightcone time and makes the Hamiltonian BRST quantization of Section 4 possible. Unlike the other four identities, which are relations between distributions and are verified in the paper's spectral basis, (A.8) is an equality of real numbers. It can therefore be checked completely in Lean.

A complete formalization would produce a machine-checked proof of a Neumann-coefficient identity. It would also add reusable material: Taylor coefficients of $\exp(\tfrac{2i}{3}\arctan z)$, the $\cosh/\cosh$ integral, and digamma-type evaluations of rational series.

Difficulty

The goal defines $m_{2n}$ through Taylor coefficients, which have no closed form. The paper does not sum the series in the mode basis. It moves to the continuous $\kappa$ basis of the Neumann spectrum and closes a contour. That step rests on eigenvector expansions $v_{2n}(\kappa)$ and the principal-value distribution $\beta(\kappa)$, neither of which is in Mathlib. A direct route has to connect the coefficients $A_{2n}$ to the integral $\int g$, or to the series $\sum b_n$, some other way. The terms of $\sum b_n$ decay like $n^{-2}$. The terms $(-1)^nA_{2n}/n$ of the goal series decay only like $n^{-5/3}$, so the goal series converges slowly.

Formalization scope

• All quantities are real. $A_k$ is given as $f^{(k)}(0)/k!$ for $f=\cos(\tfrac23\arctan\cdot)$ (even $k$) or $\sin(\tfrac23\arctan\cdot)$ (odd $k$), using Mathlib's iteratedDeriv.
• Series are indexed from $n=1$ by shifting the Lean index $n\mapsto n+1$. HasSum is unconditional (equivalently absolute) convergence. Every statement asserts convergence, so no statement can hold only because Lean assigns $0$ to a divergent tsum.
• $g(0)=0$ by Lean's convention $x/0=0$. This single point does not affect the integral.
• Source misprints corrected: the paper's first auxiliary formula prints $\sum\frac{1}{n(2n+1)}=2-\ln2$. The true value is $2-2\ln2\approx0.6137$, and that value is formalized. The formula for $m_{2n}$ is printed with left side $m_{2m}$.
• In the Section 2 statement the dimension factor $D>0$ is omitted, and only divergence to $+\infty$ is asserted, not the logarithmic rate.
• Not formalized: the identities (A.6), (A.7), (A.9), (A.10), eq. (B.2), and the eigenvectors $v_n(\kappa)$. Contributions that build this spectral machinery are welcome.

Selected references

• T. G. Erler, D. J. Gross, Locality, Causality, and an Initial Value Formulation for Open String Field Theory, 2004. https://arxiv.org/abs/hep-th/0406199
• E. Witten, Noncommutative Geometry and String Field Theory, Nucl. Phys. B 268 (1986) 253. https://doi.org/10.1016/0550-3213(86)90155-0
• L. Rastelli, A. Sen, B. Zwiebach, Star Algebra Spectroscopy, JHEP 2002. https://arxiv.org/abs/hep-th/0111281

Motivation

The index theorem says that among several Markov reward processes, of which one may be advanced at each decision time, the right one to advance is the one of greatest Gittins index. Chapter 4 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks how far this extends when the constituents are not reward processes but decision processes, each with its own controls: a research project that can be run in several ways, a job that can be processed at different speeds, a sampling process that may be stopped and exploited. A family of such superprocesses requires two choices at every decision time, which superprocess to continue and with which control, and an index policy in the sense of Chapter 2 need not be optimal (Example 4.1). Whittle (1980) identified the condition under which it is: Condition D, that when a superprocess is played against a standard bandit process paying a constant rent, the control one should apply to it does not depend on the rent. Under that condition the index theorem survives (Theorem 4.3), the index is characterized (Note 4.2), stoppable bandit processes with improving stopping options satisfy the condition (Lemma 4.4), and the chapter adds two results about indices themselves: any index that works for all bandit processes is a strictly increasing function of the Gittins index (Theorem 4.8), and a policy that is within $\varepsilon$ of the index policy loses at most $\varepsilon\gamma^{-1}(1-e^{-\gamma})^{-1}$ (Theorem 4.18).

Setting

A decision process $D$ on a countable state space $S$ has in each state $x$ a nonempty finite set $\Gamma(x)$ of controls; applying $u$ yields the reward $r(x, u)$ and moves the state by $P(\cdot \mid x, u)$. Adding the freeze control, which leaves the state unchanged and yields nothing, makes $D$ a superprocess $S$. Operating $D$ under a feasible deterministic stationary Markov policy $g$ (that is, $g(x) \in \Gamma(x)$) gives an ordinary bandit process $D_g$, and the superprocess index is

$$\nu(S, x, u) = \sup_{g : g(x) = u} \nu(D_g, x), \qquad \nu(S, x) = \max_{u \in \Gamma(x)} \nu(S, x, u), \tag{4.1}$$

with $\nu(D_g, x)$ the Gittins index of the Bandit Algorithms model. A simple family of alternative superprocesses (SFAS) is $n$ superprocesses on a common $(S, U)$; at each decision time $0, 1, 2, \dots$ exactly one is continued, with a control from its control set, the others being frozen, and rewards are discounted by $a^t$. A policy is a Markov kernel per decision time from the history to the pair (superprocess, control); it is optimal if it is feasible and attains the supremum of the discounted payoff over feasible policies from every initial state-vector, and it is an index policy if it always continues a superprocess and control of maximal $\nu(S_i, x_i, u)$.

Condition D. Let $\Lambda$ be a standard bandit process with parameter $\lambda$ (one state, reward $\lambda$). $S$ satisfies Condition D if there is a function $g$ such that, for every $x$ and $\lambda$ for which it is optimal in the family $\{S, \Lambda\}$ to select $S$ in state $x$, it is optimal to apply the control $g(x)$. A stoppable bandit process is a bandit process with a stop control that makes it behave as a standard bandit process with parameter $\mu(x)$; its stopping option is improving if $\mu(x(t))$ is almost surely nondecreasing in process time.

Formalization targets

Goal: Theorem 4.3

For a decision process with bounded rewards and a Condition-D control $g$, every index policy with respect to $\nu(D, \cdot, \cdot)$ that applies $g(x_i)$ to the superprocess $i$ it continues is optimal for the family of $n$ superprocesses:

$$\text{index policy } \pi \implies \pi \text{ feasible and } R_\pi(x) = \sup_{\pi' \text{ feasible}} R_{\pi'}(x)\ \text{ for every } x \in S^n.$$

Milestones

Note 4.2 (under Condition D, $S$ is selected in $\{S, \Lambda(\lambda)\}$ iff $\nu(S, x) \ge \lambda$, and at $\lambda = \nu(S, x)$ a control $u$ is optimal iff $\nu(S, x, u) = \nu(S, x)$; the printed equivalence fails for $\lambda < \nu(S, x)$); Lemma 4.4 (Condition D for stoppable bandit processes with improving stopping options); Theorem 4.8 (an index for the bandit processes with discount factor $a$ is strictly increasing in $\nu$); Theorem 4.18 (the $\varepsilon$-index bound, $\varepsilon/(1-a)^2$ for the discrete-time index).

Significance

Theorem 4.3 is the widest form in which the index theorem holds without further structure, and Condition D is exactly the right hypothesis: it says the superprocess has a canonical control, and once it does the family reduces to a family of bandit processes and the prevailing-charge argument goes through. Lemma 4.4 gives the model where the condition is known to hold, a research project that may be exploited at any time; the buyer's problem of Bergman and Bather is the case where it fails. Theorem 4.8 explains why every index theorem in the book is about the Gittins index: any function that orders bandit processes optimally must order them as $\nu$ does. Theorem 4.18 is the quantitative version of the index theorem that heuristics and computations rely on.

Nothing here is machine-checked. The mission builds the first controlled multi-armed model on the platform, a run law for families of decision processes with an explicit feasibility constraint, and states Whittle's condition as a property of the two-member family, which is how the literature uses it. Theorems 4.8 and 4.18 are statements about the existing Bandit Algorithms model and are usable by any later work on that model.

Difficulty

The obvious attack on Theorem 4.3, "replace each superprocess by the bandit process $D_{g}$ for its Condition-D policy $g$ and apply the index theorem", is the second half of the book's proof; the first half is to show that an optimal policy never gains by applying a control other than $g(x_i)$ to a superprocess it continues, and that uses the prevailing-stake accounting of §4.3 with the other superprocesses treated as one bandit process, plus the observation that the class of policies deviating at most $k$ times is $\varepsilon$-exhaustive. Both halves require the whole run law of the family to be related to the run laws of its constituents, which is where a formalization spends its effort. Note 4.2 is short on the page but needs the optimal-stopping characterization of Chapter 2 for the bandit process $D_g$ under charge $\lambda$. Theorem 4.8 is elementary given the value of $\{B, \Lambda\}$ under a freezing rule, $R_f(B) + \lambda\gamma^{-1} - \lambda W_f(B)$, but that identity is itself a computation on the run law. Theorem 4.18 has no proof in the book (Glazebrook 1982c); the natural route is the prevailing-charge upper bound with the charges perturbed by $\varepsilon$.

Formalization scope

Decision processes carry their control sets as finsets with a nonemptiness proof and their kernels as Markov kernels; the state space is countable with measurable singletons (so stationary kernels and control-dependent maps are measurable without side conditions) and the control type is finite with measurable singletons. The family's run law is built decision time by decision time as the Bandit Algorithms model builds markovBanditMeasure, with the policy's kernel producing the pair (superprocess, control). Feasibility is an almost-sure condition on the policy kernel, and optimality is the book's: feasible, and the supremum from every initial state-vector. The superprocess index is a real supremum over feasible stationary policies with $g(x) = u$, bounded by the reward bound and nonempty for $u \in \Gamma(x)$; for an unavailable $u$ it is a default value that no index policy consults. Condition D is stated on the family $\{S, \Lambda\}$ on $S \oplus \mathrm{Unit}$, where the standard state has every control available, all equivalent. A stoppable bandit process is the decision process with control type Bool. Theorem 4.8 quantifies over index functions defined on every measurable state space and takes as hypothesis only what its proof uses, optimality of $\mu$-index policies for the families $\{B, \Lambda\}$. Theorem 4.18 is on the $k$-armed Bandit Algorithms model with $\varepsilon \ge 0$ and the bound $\varepsilon/(1-a)^2$: the book's $\varepsilon\gamma^{-1}(1 - e^{-\gamma})^{-1}$ is in continuous-time index units, $\gamma/(1-a)$ times the discrete-time index used here, and read with the discrete index it is false for $a < 1/e$. Theorem 4.3's index policy applies the Condition-D control $g$ to the superprocess it continues, as the book's proof does; an index policy that breaks ties among controls otherwise need not be optimal.

Trivializing readings are excluded: index policies must be feasible, optimality is required from every initial state, and Condition D is a statement about optimal policies of a genuine two-member family, not about a chosen policy. Welcome contributions: the relation between the family's run law and the constituents' chain laws, the freezing-rule value identity behind Theorem 4.8, and the prevailing-stake accounting of §4.3.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 4. doi:10.1002/9780470980033
• P. Whittle, Multi-armed bandits and the Gittins index, Journal of the Royal Statistical Society B 42(2), 1980. doi:10.1111/j.2517-6161.1980.tb01111.x
• K. D. Glazebrook, Stoppable families of alternative bandit processes, Journal of Applied Probability 16(4), 1979. doi:10.2307/3213152
• K. D. Glazebrook, On the evaluation of suboptimal strategies for families of alternative bandit processes, Journal of Applied Probability 19(3), 1982. doi:10.2307/3213524
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Motivation

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

Setting

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

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

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

Formalization targets

Goal: Theorem 3.6

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

$$\text{optimal}(\sigma) \iff \forall k,\ \forall i:\ \frac{p_i (1-q_i)^{N_i(k)} q_i}{c_i} \le \frac{p_{\sigma_k}(1-q_{\sigma_k})^{N_{\sigma_k}(k)} q_{\sigma_k}}{c_{\sigma_k}}.$$

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

Setting

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

$$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

An initial value problem $y' = f(x,y)$, $y(x_0) = y_0$, is the standard way a law of motion, a growth model or a circuit equation is written down, and only a small minority of such problems can be integrated in closed form. Single-step methods advance the solution by small increments: Euler's method takes the tangent line at the current point, and the higher-order Runge-Kutta schemes refine the same idea. What justifies them is a pair of theorems: that the problem has a unique solution at all, and that the computed polygon approaches that solution as the step size decreases.

This mission is the seventh in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 9, Métodos Numéricos para EDO's, up to the convergence of Euler's method.

Setting

Consider the initial value problem

$$y' = f(x,y), \\qquad y(x_0) = y_0,$$

with $f$ defined on a rectangle $D = [x_0-a, x_0+a]\\times[y_0-b, y_0+b]$.

Picard's method replaces the differential equation by the integral equation $y(x) = y_0 + \\int_{x_0}^{x} f(t, y(t))\\,dt$ and iterates it:

$$y_0(x) = y_0, \\qquad y_{k+1}(x) = y_0 + \\int_{x_0}^{x} f(t, y_k(t))\\,dt .$$

With $M = \\max_D |f|$, $N = \\max_D |\\partial f/\\partial y|$ and $h = \\min\\{a, b/M\\}$, the source states the bound $|\\varphi(x) - y_k(x)| \\le \\frac{M N^{k-1}}{k!}h^k$ on $[x_0-h, x_0+h]$, where $\\varphi$ is the exact solution.

Euler's method with step $h$ produces $y_{i+1} = y_i + h f(x_i, y_i)$, $x_i = x_0 + ih$. Its local error is $O(h^2)$ per step and its global error $O(h)$.

Target

The goal theorem is the global error statement: for an initial value problem whose exact solution $\\varphi$ is twice continuously differentiable on $[x_0, X]$ and whose right-hand side is Lipschitz in $y$ there, there is a constant $C$ such that for every step size $h \\in (0,1]$ and every grid point $x_0 + ih \\le X$,

$$|y_i - \\varphi(x_0+ih)| \\le C h .$$

This is the precise form of the source's assertion $E = O(h)$.

The milestones are the results the chapter states on the way: local existence and uniqueness for the initial value problem under a Lipschitz condition in $y$ (Teorema 9.4.1), the Picard error bound, the convergence of the Picard iterates to the solution, and the one-step Taylor identity behind Euler's method.

Significance

The global error bound is what makes Euler's method a method rather than a heuristic: it converts an arbitrary choice of step size into a guaranteed accuracy, and it exhibits the characteristic loss of one order between the local error $O(h^2)$ and the global error $O(h)$ that recurs for every single-step scheme. The existence and uniqueness theorem is the prerequisite for all of it — without uniqueness there is no well-defined object for the numerical solution to approximate — and the Picard iteration is both the constructive proof of that theorem and a method in its own right.

Difficulty

The global error proof has to handle the interaction of two error sources: the local truncation error at each step and the amplification of previous errors by the Lipschitz constant, which gives the discrete Gronwall recursion $e_{i+1} \\le (1+hL)e_i + Ch^2$. Carrying that recursion to the closed-form bound, and doing it uniformly in $h$, is the core of the mission. The Picard bound requires the iterates to remain inside the rectangle so that the hypotheses on $f$ continue to apply — that is what the choice $h = \\min\\{a, b/M\\}$ is for — and an induction on $k$ with the factorial denominator.

Formalization scope

The unknown is a real function of a real variable and $f$ is a function of two real variables. A solution is a function $\\varphi$ satisfying $\\varphi(x_0)=y_0$ and having derivative $f(x,\\varphi(x))$ at every point of the relevant interval. The Lipschitz condition in the second variable is stated explicitly, $|f(x,u)-f(x,v)| \\le L|u-v|$, in place of the source's hypothesis that $\\partial f/\\partial y$ is bounded; for the global-error goal it is assumed for all real $u,v$ and all $x$ in the interval, and in the Picard milestones only inside the rectangle. Uniqueness is stated as agreement of any two solutions on the interval, not as uniqueness of a function on all of $\\mathbb{R}$, since a solution is unconstrained outside the interval. Euler's iterates and the Picard iterates are explicit recursive definitions; the Picard integral is the interval integral, which is total, so no integrability side condition appears in the definition. The constant $C$ in the goal is asserted to exist and to be positive, uniformly over step sizes in $(0,1]$; the restriction $h \\le 1$ merely normalizes the range of steps considered.

Selected references

• S. R. Freitas, Métodos Numéricos, Departamento de Computação e Estatística, Universidade Federal de Mato Grosso do Sul, 2000. Chapter 9, Métodos Numéricos para EDO's, pp. 183–213. (Course notes supplied with this mission.)

Motivation

Chapter 2's tail bounds mostly rest on moment-generating-function control, obtained either directly (sub-Gaussianity) or through explicit combinatorial arguments (Hoeffding, bounded differences). The entropic method offers a different, more structural route: bound a specific information-theoretic quantity — the $\varphi$-entropy of $e^{\lambda X}$ — and convert that bound mechanically into a tail bound via a short ODE argument (the Herbst argument). This method's real payoff appears once it is combined with the tensorization property of entropy across independent coordinates, which is what lets it handle Lipschitz functions of many independent variables — including cases, such as separately convex functions, that elude the purely martingale-based techniques of Chapter 2. This mission formalizes the entropic method's two foundational entropy-to-tail conversions and its central Lipschitz-concentration application, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 3.

Setting

For $\varphi(u):=u\log u$ ($u>0$), $\varphi(0):=0$, the $\varphi$-entropy of a nonnegative random variable $Z$ is $H(Z):=\mathbb E[Z\log Z]-\mathbb E[Z]\log\mathbb E[Z]$ (Eqs. (3.1)-(3.2)). Writing $\varphi_X(\lambda):=\mathbb E[e^{\lambda X}]$ for the moment generating function of $X$, the entropy of $e^{\lambda X}$ has the explicit form $H(e^{\lambda X}) = \lambda\varphi_X'(\lambda) -\varphi_X(\lambda)\log\varphi_X(\lambda)$ (Eq. (3.3)).

A function $f:\mathbb R^n\to\mathbb R$ is separately convex if, for each coordinate $k$, the univariate function obtained by fixing every coordinate but the $k$-th is convex — strictly weaker than joint convexity of $f$ itself. $f$ is $L$-Lipschitz with respect to the Euclidean norm if $|f(x)-f(x')|\le L\|x-x'\|_2$ for all $x,x'$.

Formalization targets

Goal — Theorem 3.4 (separately convex Lipschitz concentration)

Let $\{X_i\}_{i=1}^n$ be independent, each supported on $[a,b]$, and $f$ separately convex and $L$-Lipschitz. Then for all $\delta>0$,

$$\mathbb P[f(X)\ge\mathbb E[f(X)]+\delta] \;\le\; \exp\Big(-\frac{\delta^2}{4L^2(b-a)^2}\Big).$$

Milestone — Proposition 3.2 (the Herbst argument)

If $H(e^{\lambda X})\le\tfrac12\sigma^2\lambda^2\varphi_X(\lambda)$ for all $\lambda\in I$ ($I=[0,\infty)$ or $\mathbb R$), then $\log\mathbb E[e^{\lambda(X-\mathbb E[X])}]\le \tfrac12\lambda^2\sigma^2$ for all $\lambda\in I$ — the basic entropy-to-sub-Gaussian-tail conversion.

Milestone — Proposition 3.3 (the Bernstein entropy bound)

The sub-exponential analogue: if $H(e^{\lambda X})\le\lambda^2\{b\varphi_X'(\lambda)+ \varphi_X(\lambda)(\sigma^2-b\mathbb E[X])\}$ for $\lambda\in[0,1/b)$, then $\log\mathbb E[e^{\lambda(X-\mathbb E[X])}]\le\sigma^2\lambda^2(1-b\lambda)^{-1}$ on the same range.

Significance

Propositions 3.2 and 3.3 are the two basic entropy-to-tail conversions the entire chapter's entropic method rests on — every subsequent Lipschitz-concentration result in the chapter (including Theorem 3.4 and the more advanced Theorem 3.24) is obtained by first establishing an entropy bound of one of these two forms and then invoking the corresponding proposition. Theorem 3.4 is itself the direct analogue, for independent bounded variables, of Chapter 2's Gaussian Lipschitz concentration (Theorem 2.26) — but crucially requires the extra hypothesis of separate convexity, which the Gaussian case does not need and which cannot be dropped in general.

Formalizing it. No faithful prior art exists on the platform. The one candidate flagged in BRIEF.md, Talagrand.lipschitz_concentration, was read in full: it is a weighted-Hamming- distance concentration bound for functions on a finite-alphabet product space Fin n → α, proved via Talagrand's convex-distance method — a different underlying space (finite alphabet vs. real-valued bounded coordinates) and a different Lipschitz norm (weighted Hamming vs. Euclidean) from Theorem 3.4, and not reused here. A search for "log-Sobolev" and "Herbst" turned up bousquet_herbst_cgf_le_phi_via_herbst/bousquet_herbst_cgf_le_phi_double_integration: these are abstract calculus lemmas about a generic function $G$ satisfying an ODE-type growth condition ($G''\le ve^x$), concluding $G(L)\le v(e^L-1-L)$ — a genuinely different statement shape from Proposition 3.2/3.3's entropy-to-CGF conversions (which conclude a quadratic, not exponential, bound on $\log\mathbb E[e^{\lambda(X-\mathbb EX)}]$), and not a faithful match. All three theorems here are drafted as open goals (:= by sorry).

Difficulty

The naive approach to Theorem 3.4 — try to adapt the bounded-differences (martingale) method of Chapter 2 directly — fails, because the bounded-differences method needs $f$ to have small coordinatewise oscillation in an absolute sense, while separate convexity alone gives no such uniform bound (a separately convex function can vary arbitrarily fast within the interior of its domain, only its slope is controlled by the Lipschitz condition). The entropic method sidesteps this by working with the $\varphi$-entropy of $e^{\lambda f(X)}$ directly: entropy has a tensorization property across independent coordinates (not itself part of this mission, but what the entropic method's proof of Theorem 3.4 uses) that reduces a multivariate entropy bound to a sum of "one coordinate at a time" contributions, each of which convexity and the Lipschitz condition jointly control — a route with no analogue in the bounded-differences approach.

Formalization scope

Separate convexity and Euclidean-Lipschitzness are both restated locally in this chapter's own sub-namespace (HighDimStat.Concentration), per this book series' rule against importing another chapter's draft definitions, even though Chapter 2 already defines an IsLLipschitz for the same Euclidean condition. φ_X'(\lambda)$ (Proposition 3.3) is realized via Mathlib's deriv, a legitimate way to state a hypothesis on a derivative without separately proving differentiability, appropriate at the draft-statement stage. Explicit Integrable` hypotheses guard the Bochner integral's junk value on non-integrable functions throughout (trap 2), not literal in the book's own propositions but implied by what "the entropy $H(e^{\lambda X})$ exists" (an explicit qualifier the book itself makes when introducing Eq. (3.2)) means.

Goal substitution, disclosed. BRIEF.md recommends Theorem 3.24 (the two-sided, jointly convex analogue) as the primary goal, but explicitly names Theorem 3.4 as a fallback "if 3.24's dependence on the unnumbered transportation-cost inequality (Eq. 3.73, attributed to Samson) proves too heavy to state faithfully in the time available." Theorem 3.24's proof route depends on Theorem 3.19 (a general "transportation cost implies concentration" result for an abstract metric measure space, itself needing a from-scratch formalization of the transportation-cost inequality (3.58) and the concentration function $\alpha_{P,(\mathcal X,\rho)}$) plus the unproven-in-chapter Eq. (3.73). Building this full stack faithfully was judged to exceed this chunk's time budget; Theorem 3.4 is drafted instead, using this mission's own budget on Propositions 3.2 and 3.3 (the two most load-bearing entropy-to-tail conversions of the chapter) rather than the heavier transportation-cost machinery. Theorem 3.19, Theorem 3.24, and Eq. (3.73) are all out of scope for this mission and named here as natural follow-on work.

Selected references

• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 3.
• M. Ledoux, The Concentration of Measure Phenomenon, American Mathematical Society, 2001.
• I. Herbst, unpublished (the argument bearing his name is attributed in Ledoux (2001) and standard references on log-Sobolev inequalities).