Probability

Motivation

The economic order quantity (EOQ) is the most widely used formula in inventory management. It assumes that demand is a deterministic constant stream. Real demand is random, and the model that accounts for this, the continuous-review $(Q, r)$ policy with stochastic demand, has no closed-form optimum: for decades its optimal parameters were computed numerically, one instance at a time, which gave little insight into how the stochastic system behaves. Practitioners nevertheless kept using the EOQ quantity in stochastic systems and observed that the cost penalty was small (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), without an analytical explanation.

Zheng (Management Science 38(1), 1992) supplied that explanation. By minimising the average cost first over the reorder point and then over the order quantity, he obtained two simple optimality equations and compared the stochastic model with the EOQ model under the same cost structure. One of the results is the goal of this mission: for every leadtime-demand distribution, using the EOQ order quantity in the stochastic system raises the average cost by at most one eighth. The paper extends Federgruen and Zheng (1988), who treated the discrete-demand version of the cost function.

Setting

A single item faces demand at rate $\lambda > 0$. Orders are delivered after a fixed leadtime $L > 0$, and stockouts are backordered. Each order costs a fixed $K > 0$. Inventory is held at cost rate $h > 0$ per unit and backorders are penalised at cost rate $p > 0$ per unit. Let $D \ge 0$ be the demand during a leadtime, with mean $E(D) = \lambda L$. The newsvendor cost

$$G(y) = E\big[h(y - D)^+ + p(D - y)^+\big]$$

is the rate at which expected inventory costs accrue at time $t + L$ when the inventory position at time $t$ is $y$. It is convex, and it is assumed, as in the paper, to attain its minimum at a unique point $y^0$.

A $(Q, r)$ policy orders $Q$ units whenever the inventory position falls to the reorder point $r$. Its long-run average cost is

$$c(Q, r) = \frac{\lambda K + \int_r^{r+Q} G(y)\,dy}{Q}. \qquad (1)$$

For a fixed $Q > 0$ let $r(Q)$ be an optimal reorder point, and set

$$H(Q) = G(r(Q)) \ (Q > 0),\quad H(0) = G(y^0),\quad C(Q) = c(Q, r(Q)),\quad A(Q) = Q H(Q) - \int_0^Q H(y)\,dy .$$

$C(Q)$ is the average cost when the reorder point is chosen optimally for $Q$; an order quantity $Q^* > 0$ minimising $C$ over $Q > 0$ is the optimal order quantity, and $C^* = C(Q^*)$ is the optimal cost.

The EOQ model is the special case in which the leadtime demand is the constant $\lambda L$. Its cost rate is $G_d(y) = h(y - \lambda L)^+ + p(\lambda L - y)^+$, and its optimal order quantity is

$$Q^*_d = \sqrt{\frac{2\lambda K(h+p)}{hp}} .$$

The subscript $d$ marks every object of the EOQ model ($r_d$, $H_d$, $A_d$).

Formalization targets

Goal: Theorem 5

$$R = \frac{C(Q^*_d) - C^*}{C^*} \;\le\; \frac18 - \frac12\left(\frac12 - \frac{Q^*_d}{Q^*}\right)^2 \;\le\; \frac18 .$$

$C(Q^*_d)$ is the stochastic cost at the EOQ quantity with the reorder point re-optimised for it. The bound holds for every leadtime-demand distribution and every value of the parameters.

Milestones

In the order the goal's proof uses them:

• Lemma 1 (joint convexity of $c$), Lemma 2 ($r = r(Q) \iff G(r) = G(r+Q)$), Lemma 3 (properties of $r(Q)$), Corollary 1 ($G(r(Q)) \le \max(G(r), G(r+Q))$);
• Eq. (7) ($C(Q) = (\lambda K + \int_0^Q H)/Q$), Lemma 4 ($H$ increasing, convex, asymptotic slope $hp/(h+p)$), Lemma 5 ($C$ convex), Eq. (8) ($H(Q^*) = C(Q^*)$), Theorem 1 ($(Q, r)$ optimal iff $c(Q,r) = G(r) = G(r+Q)$), Lemma 6 ($A$ increasing convex, $Q = Q^* \iff A(Q) = \lambda K$, comparative statics in $K$);
• Eqs. (18), (20) (the EOQ model: $H_d(Q) = hpQ/(h+p)$ and the formula for $Q^*_d$), Eq. (22) ($G_d \le G$), Lemma 7 ($H_0 \le H_d \le H$, $A \le A_d$), and the first inequality of Theorem 2, $Q^*_d \le Q^*$.

Significance

The theorem is a distribution-free worst-case guarantee for the most common heuristic in inventory practice. It says that the EOQ formula, which needs only the mean demand rate and three cost parameters, loses at most $12.5\%$ against the true optimum, and that the loss is smaller when $Q^*_d/Q^*$ is close to $\frac12$ or to $1$. Combined with the paper's Theorem 2 (the gap $Q^* - Q^*_d$ is bounded as $K$ grows), it implies that the relative loss vanishes as the fixed ordering cost grows. The milestones along the way (the optimality conditions of Theorem 1, the monotonicity of the optimal reorder point, the comparison of $H$ with its EOQ counterpart) are the standard structural facts about continuous $(Q, r)$ systems and are reused throughout the inventory literature.

The result is proved in the paper. No machine-checked version of it, or of the $(Q, r)$ optimality conditions for the continuous cost (1), is known to exist. The platform has related but different formalizations: the discrete cost function with integer $Q$ (InventoryControl_rqDiscrete), the $(R, Q)$ cost under normal demand (InventoryControl_rq), and the EOQ without backorders (InventoryControl_eoq). A complete development here provides the continuous $(Q, r)$ machinery for an arbitrary leadtime-demand distribution.

Difficulty

The paper's proofs differentiate $r(Q)$ and $H(Q)$ twice (Eqs. (4), (5)), which presupposes a leadtime demand with a smooth density. The formalization does not assume one, so that discrete demand, such as the Poisson demand of the paper's own numerical study, is covered. Every step that the paper takes through derivatives, in particular the convexity of $H$ and the slope bound $H' \le hp/(h+p)$, has to be established by other means: through one-sided derivatives or chord arguments for the convex function $G$, whose kinks are where the derivative-based argument breaks. The definition of $r(Q)$ as a minimiser also means its existence and uniqueness must be proved before any property of $H$, $C$ or $A$ can be used.

Formalization scope

• The model is a probability measure $\mu$ on $\mathbb{R}$ (the law of $D$), concentrated on $[0,\infty)$, integrable, with mean $\lambda L$; $G$ is the integral of $h\max(y-x,0) + p\max(x-y,0)$ against $\mu$. The standing assumptions are bundled in IsQRModel: $\lambda, L, h, p > 0$, the conditions on $\mu$, and the unique minimiser of $G$ (paper, p. 90). $K > 0$ is a separate hypothesis. No density is assumed.
• $c$, $r(Q)$, $y^0$, $H$, $H_0$, $C$, $A$ and optimality of an order quantity are defined for an arbitrary cost rate $G$ and applied both to the newsvendor cost and to $G_d$; the EOQ objects $r_d$, $H_d$, $A_d$ are these definitions at $G_d$, and Eqs. (18), (20) are theorems.
• $r(Q)$ is a chosen minimiser of $c(Q,\cdot)$ (never defined by $G(r) = G(r+Q)$, which is Lemma 2). $H(0) := G(y^0)$; right-continuity of $H$ at $0$ is part of the Lemma 4 milestone. Order quantities range over $(0,\infty)$ for $c$ and $C$ and over $[0,\infty)$ for $H$, $H_0$, $A$.
• $Q^*$ in the goal is any $Q > 0$ with $C(Q) \le C(Q')$ for all $Q' > 0$; Lemma 6 asserts that exactly one exists, so the goal is not vacuous. $Q^*_d$ is the explicit square-root formula.
• Readings of informal words: "increasing" in Lemmas 4 and 6 means strictly increasing on $[0,\infty)$; "$Q^*$ increasing, $r^*$ decreasing in $K$" means strictly; "asymptotic slope $hp/(h+p)$" means that every chord of $H$ on $[0,\infty)$ has slope at most $hp/(h+p)$ and $H(Q)/Q \to hp/(h+p)$; Lemma 3 part 3 is stated as strict monotonicity of $r(Q)$ and $r(Q) + Q$, and its derivative clause $-1 < r'(Q) < 0$ is omitted because $r$ need not be differentiable without a density; "the optimal order quantity" means existence and uniqueness; Lemma 7 is stated for $Q \ge 0$.
• A trivializing formalization is ruled out: $C(Q^*_d)$ is the stochastic cost with the reorder point re-optimised in the stochastic model (not the EOQ reorder point $r^*_d$), and no positivity of $C^*$ is assumed (it follows from the model).
• Out of scope: the discrete cost (2), the §4 numerical study, and the unnumbered remarks after Theorem 5.
• Needed infrastructure: interval integrals of convex functions, partial minimisation of jointly convex functions, Jensen's inequality for $\mu$, and one-sided derivatives of convex functions. The generic $(Q, r)$ machinery (optimality conditions for arbitrary convex $G$) is reusable for other continuous-review models. Proofs of any milestone, and alternative proofs that avoid the paper's differentiability assumptions, are welcome.

Selected references

• Yu-Sheng Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• Awi Federgruen and Yu-Sheng Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808
• Paul H. Zipkin, Inventory Service-Level Measures: Convexity and Approximation, Management Science 32(8):975–981, 1986. https://doi.org/10.1287/mnsc.32.8.975
• George Hadley and Thomson M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• Daniel P. Heyman and Matthew J. Sobel, Stochastic Models in Operations Research, Vol. II, McGraw-Hill, 1984.

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

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

Motivation

Many estimation problems are naturally posed over matrices rather than vectors: recommender systems (Netflix-style matrix completion), multivariate regression with correlated responses, vector autoregressive time series, and phase retrieval all reduce to estimating an unknown matrix $\Theta^*$ that is low-rank, or well approximated by one. A rank constraint alone makes the natural least-squares estimator non-convex and generally intractable; replacing it with the nuclear norm — the sum of the matrix's singular values, the tightest convex surrogate for rank — yields a tractable semidefinite program. Wainwright's High-Dimensional Statistics (2019), Chapter 10, shows that this substitution costs nothing statistically: nuclear-norm-regularized least squares achieves error rates matching what one could hope for even knowing the rank in advance, by specializing Chapter 9's general decomposable-regularizer framework (mission 09-decomposability) directly to the nuclear norm.

Setting

For matrices $A,B\in\mathbb R^{d_1\times d_2}$, the trace inner product is $\langle\!\langle A,B\rangle\!\rangle := \mathrm{trace}(A^TB) = \sum_{j_1,j_2}A_{j_1j_2}B_{j_1j_2}$ (Eq. 10.1), inducing the Frobenius norm $\|\!|A|\!\|_F$. Given design matrices $X_1,\dots,X_n\in\mathbb R^{d_1\times d_2}$ and responses $y_i=\langle\!\langle X_i,\Theta^*\rangle\!\rangle+w_i$, the observation operator $\mathcal X_n(\Theta):=(\langle\!\langle X_i,\Theta\rangle\!\rangle)_{i=1}^n$ and its adjoint $\mathcal X_n^*(u):=\sum_iu_iX_i$ (Eqs. 10.2-10.3) are the matrix analogs of a vector design matrix and its transpose. The nuclear norm $\|\!|\Theta|\!\|_{\mathrm{nuc}}:=\sum_j\sigma_j(\Theta)$ (Eq. 10.5) — the sum of singular values — is a decomposable regularizer (in the sense of Chapter 9) with respect to the subspace pair spanned by the top singular vectors of any target matrix, and its dual norm (Table 9.1) is the $\ell_2$-operator (spectral) norm $\|\!|\cdot|\!\|_2$. The estimator under study is nuclear-norm-regularized least squares,

$$\hat\Theta \in \operatorname*{arg\,min}_{\Theta\in\mathbb R^{d_1\times d_2}} \left\{ \frac{1}{2n}\|y-\mathcal X_n(\Theta)\|_2^2 + \lambda_n\|\!|\Theta|\!\|_{\mathrm{nuc}} \right\} \tag{10.16}$$

with $\lambda_n>0$ user-chosen.

Formalization targets

Goal (Proposition 10.6)

Suppose $\mathcal X_n$ satisfies the restricted strong convexity condition (10.17), $\|\mathcal X_n(\Delta)\|_2^2/(2n) \ge \kappa/2\|\!|\Delta|\!\|_F^2 - c_0\frac{d_1+d_2}{n}\|\!|\Delta|\!\|_{\mathrm{nuc}}^2$ for all $\Delta$, with $\kappa>0$, $c_0\ge 0$. Conditioned on the good event $\mathcal G(\lambda_n)=\{\|\!|\frac1n\sum_iw_iX_i|\!\|_2 \le\lambda_n/2\}$, any optimal $\hat\Theta$ satisfies, for any $r\in\{1,\dots,d'\}$ with $r\le\kappa n/(128c_0(d_1+d_2))$,

$$\|\!|\hat\Theta-\Theta^*|\!\|_F^2 \le \frac{9}{2}\frac{\lambda_n^2}{\kappa^2}r + \frac{1}{\kappa}\left\{2\lambda_n\sum_{j=r+1}^{d'}\sigma_j(\Theta^*) + \frac{32c_0(d_1+d_2)}{n}\left(\sum_{j=r+1}^{d'}\sigma_j(\Theta^*)\right)^2\right\}.$$

Milestone (Proposition 10.7)

Under the alternative $\Phi^*$-curvature condition (10.20) (a curvature bound on the gradient map rather than the Taylor error), with $\mathrm{rank}(\Theta^*)<\kappa/(64\tau_n)$: conditioned on $\mathcal G(\lambda_n)=\{\|\!|\frac1n\mathcal X_n^*(w)|\!\|_2\le\lambda_n/2\}$, any optimal $\hat\Theta$ satisfies $\|\!|\hat\Theta-\Theta^*|\!\|_2 \le 3\sqrt2\,\lambda_n/\kappa$ — an operator-norm bound the book notes is, in conjunction with the cone-like constraint (10.15), strictly stronger than Proposition 10.6's Frobenius-norm bound.

Significance

Proposition 10.6 is this chapter's direct payoff from Chapter 9's general machinery: it shows that the deterministic backbone of the Lasso's guarantee (mission 07-sparse-linear) extends essentially verbatim to the matrix setting, with the sparsity level $s$ replaced by the target rank $r$ and the ambient dimension $d$ replaced by $d_1+d_2$ — exactly the "degrees of freedom" scaling one would predict by counting the parameters needed to specify a rank-$r$ matrix. Every one of the chapter's later corollaries (matrix compressed sensing, multivariate regression, matrix completion) is obtained by verifying the restricted strong convexity condition (10.17) holds with high probability for a specific random design, then reading the rate directly off Proposition 10.6 — the same two-step recipe Chapter 9's own Theorem 9.19 established abstractly. Proposition 10.7's operator-norm bound is what subsequently controls the individual singular values of the estimation error, needed for exact-rank-recovery guarantees.

Difficulty

Both results are direct specializations of Chapter 9's general oracle inequalities (Theorem 9.19 and Theorem 9.24 respectively) to the nuclear norm as regularizer and the Frobenius/operator norm pair, so their formalization difficulty lies almost entirely in getting the matrix-specific objects right rather than in new proof machinery: the nuclear norm requires an actual notion of singular values (realized via the eigenvalues of the Gram matrix $\Theta^T\Theta$, using Mathlib's Hermitian-matrix spectral theorem), the operator norm requires the correct rectangular generalization of the symmetric-matrix Rayleigh-quotient characterization used in mission 08-pca, and the restricted-strong-convexity and curvature conditions must be instantiated against the correctly-adjointed observation operator $\mathcal X_n^*$. A further subtlety is keeping Proposition 10.6's Frobenius-norm conclusion and Proposition 10.7's operator-norm conclusion cleanly distinct — the book itself warns against conflating the norms used across different chapters of Part II (the vector $\ell_2$-norm of chunks 07-sparse-linear/08-pca versus the matrix Frobenius and operator norms here).

Formalization scope

Scope cut, disclosed here and in STATUS.md. BRIEF.md recommends Corollary 10.10 (the sample-complexity bound for the $\Sigma$-Gaussian random matrix ensemble) as the goal theorem. Corollary 10.10 is a genuinely probabilistic statement — it asserts a bound holding "with probability at least $1-2e^{-2n\delta^2}$" over $n$ i.i.d. draws of design matrices from a $\Sigma$-Gaussian ensemble (Theorem 10.8's own high-probability restricted-strong-convexity certification for that ensemble) — and formalizing it faithfully would require a genuine multivariate-Gaussian-measure infrastructure on matrix space (a probability space, an i.i.d. sequence of $\Sigma$-covariance-structured Gaussian matrices, and Mathlib's measure-theoretic probability API) that is disproportionate to this mission's time budget, and orthogonal to what Chapter 10 itself contributes (the chapter's own text stresses that Propositions 10.6 and 10.7 are the chapter's deterministic core, with probability entering only in Section 10.3's ensemble-specific certification — precisely mirroring chunk 09-decomposability's own "Theorem 9.19 is actually a deterministic result" framing). This mission instead takes Proposition 10.6 as its goal — explicitly named in BRIEF.md's own candidate list as "the nuclear-norm oracle inequality, an explicit corollary of Theorem 9.19" — the natural, tractable, still highly citable deterministic title result of Section 10.2, together with its companion Proposition 10.7. Theorem 10.8 (the $\Sigma$-Gaussian ensemble's RSC certification), Corollary 10.9 (noiseless exact recovery) and Corollary 10.10 itself are left for a future mission with a dedicated probability-theory budget. The cone-like constraint (Eq. 10.15) — whose own faithful statement requires the same explicit subspace-pair machinery ($\mathcal M(U_r,V_r),\bar{\mathcal M}(U_r,V_r)$) chunk 09-decomposability built for the general theory — is similarly left out, since Propositions 10.6 and 10.7's own numbered statements never expose these subspaces directly (only their proofs do, via instantiating Theorem 9.19/9.24). singularValues and nuclearNorm are noncomputable, defined via Mathlib's Hermitian-matrix eigenvalue spectral theorem; c0 ≥ 0 and λn > 0 are made explicit, matching this book's running conventions for RSC tolerance constants and regularization weights (see MODERATION_NOTES.md).

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 10. DOI: 10.1017/9781108627771.
• Negahban, S., Wainwright, M. J. "Estimation of (near) low-rank matrices with noise and high-dimensional scaling." Annals of Statistics, 39(2), 2011, 1069–1097.
• Recht, B., Fazel, M., Parrilo, P. A. "Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization." SIAM Review, 52(3), 2010, 471–501.

Motivation

Linear methods like SVMs work only when the classes are linearly separable, but most real data is not. Chapter 6 shows how to get non-linear decision boundaries for free: replace the input space's inner product with a kernel $K$ that implicitly computes an inner product in a (possibly very high- or infinite-dimensional) feature space, without ever explicitly computing the feature mapping. This works for any positive definite symmetric (PDS) kernel — and the chapter's central theorem shows that such a kernel always induces a genuine Hilbert space (the reproducing kernel Hilbert space, RKHS) in which the kernel is literally an inner product. The chapter's capstone, the representer theorem, then shows that a broad class of optimization problems over this (possibly infinite-dimensional) Hilbert space always has a solution expressible as a finite linear combination of kernel evaluations at the training points — turning an infinite-dimensional problem into a finite, $m$-dimensional one.

Setting

A kernel $K:X\times X\to\mathbb R$ is PDS (Definition 6.3) if for every finite sample $\{x_1,\dots,x_m\}\subseteq X$, the Gram matrix $[K(x_i,x_j)]$ is symmetric positive semidefinite. Theorem 6.8 shows every PDS kernel is an inner product $K(x,x')=\langle \Phi(x),\Phi(x')\rangle$ in some Hilbert space $H$ (the RKHS), which further has the reproducing property $h(x)=\langle h,K(x,\cdot)\rangle$ for every $h\in H$ — evaluating $h$ at a point is itself an inner product with the kernel section at that point. Theorem 6.10 shows PDS kernels are closed under sum, product, tensor product, pointwise limit, and power-series composition, letting complex kernels (Gaussian, and many others) be built from simple ones (polynomial kernels) without re-verifying positive-semidefiniteness from scratch. Section 6.3's representer theorem (Theorem 6.11) then considers minimizing, over $h\in H$, an objective $F(h)=G(\|h\|_H)+L(h(x_1),\dots,h(x_m))$ that depends on $h$ only through its norm and its values at $m$ fixed points.

Formalization targets

Theorem 6.8 (RKHS existence, milestone). For a PDS kernel $K$, there exist a Hilbert space $H$ and $\Phi:X\to H$ with $K(x,x')=\langle\Phi(x),\Phi(x')\rangle$, and $H$ has the reproducing property $h(x)=\langle h,K(x,\cdot)\rangle$ for all $h\in H$, $x\in X$.

Theorem 6.10 (closure properties, milestone). PDS kernels are closed under sum, product, tensor product, pointwise limit, and power-series composition with non-negative coefficients.

Theorem 6.11 — the mission's goal. For any non-decreasing $G:\mathbb R\to\mathbb R$ and any loss $L:\mathbb R^m\to\mathbb R\cup\{+\infty\}$, $\mathrm{argmin}_{h\in H} G(\|h\|_H)+ L(h(x_1),\dots,h(x_m))$ admits a solution $h^\star=\sum_{i=1}^m\alpha_i K(x_i,\cdot)$; if $G$ is increasing, every solution has this form.

Significance

Theorem 6.11 is the chapter's payoff and one of the most widely used structural results in kernel methods: it explains, in one general statement covering SVMs, kernel ridge regression, Gaussian process MAP estimation and many other algorithms simultaneously, why the dual (finite, $m$-coefficient) formulation always suffices — the RKHS's infinite dimensionality never has to be confronted directly. Theorem 6.8 is the structural fact the whole chapter (and every later kernelized algorithm in the book, chapters 9-11, 15) depends on: without it, "PDS kernel" would be a purely combinatorial condition on Gram matrices with no guarantee it corresponds to any actual inner product. No prior art on the Prove2Me platform is faithful to any of this chapter's content: GET /theorems?q=Representer theorem and q=reproducing kernel return no faithful match (one unrelated hit concerns a Gaussian-measure reproducing kernel in a different, probabilistic context, not this chapter's PDS-kernel/RKHS construction). All six items are drafted fresh.

Difficulty

Theorem 6.8's proof is a genuine construction: define $H_0$ as finite linear combinations of kernel sections $\Phi(x)=K(x,\cdot)$, define an inner product on $H_0$ using $K$ itself, verify it is well-defined (independent of the representation), positive semidefinite (via the PDS hypothesis), and — via the Cauchy-Schwarz-for-PDS-kernels lemma (Lemma 6.7) — actually positive definite, then complete $H_0$ to a genuine Hilbert space $H$ in which it is dense, and finally extend the reproducing property from the dense subspace $H_0$ to all of $H$ by a continuity argument. This is substantial analysis, not a restatement. Theorem 6.11's proof uses the orthogonal decomposition $H=H_1\oplus H_1^\perp$ (where $H_1=\mathrm{span}\{K(x_i, \cdot)\}$) and the reproducing property to show the orthogonal component $h^\perp$ never helps and, when $G$ is strictly increasing, strictly hurts — a short argument, but one that depends essentially on Theorem 6.8's reproducing property holding for the specific $H$ constructed, not just any Hilbert space with the kernel as its inner product.

Formalization scope

IsPDS uses the book's own second SPSD characterization (c^T K c ≥ 0 for every finite sample and coefficient vector c) rather than the non-negative-eigenvalues characterization, avoiding spectral theory for a Prop-valued definition; the book states the two are equivalent. IsRKHSOf and IsMinimizer are formalization scaffolding, not book-numbered definitions: IsRKHSOf packages Theorem 6.8's own two displayed equations (6.8, 6.9) as a reusable predicate shared between Theorem 6.8 (its conclusion) and Theorem 6.11 (its "H its corresponding RKHS" hypothesis), using an explicit evaluation map ev : H → X → ℝ to stand in for "elements of H are functions on X," since Mathlib's abstract Hilbert spaces are not themselves spaces of functions; IsMinimizer packages argmin. Both X in Theorem 6.8's existential and Theorem 6.11's ambient type are plain Type rather than Type*, avoiding universe-polymorphic quantification over the constructed Hilbert space's own type — a harmless simplification, since every application in this book instantiates X at a concrete, small type (typically $\mathbb R^N$ or a finite set). Theorem 6.11's loss codomain ℝ ∪ {+∞} is WithTop ℝ, not EReal (which would also admit -∞, an unstated generalization the book's own display does not license, since EReal's ⊤+⊥=⊥ collapse is a genuine faithfulness risk the book's own L:\mathbb R^m\to\mathbb R\cup\{+\infty\} avoids by construction). WithTop ℝ on its own does not avoid every collapse, though: an unconstrained L may be the constant function ⊤ (a legal instance of ℝ∪\{+\infty\}), forcing the objective identically ⊤ and every point to vacuously minimize it, which would make the theorem's second conjunct false. An added hypothesis, ∃ h₀, F h₀ ≠ ⊤, makes explicit the book's own implicit assumption that the objective is finite somewhere — see the Formalization scope note below. Theorem 6.11's two clauses are otherwise kept exactly as distinct as the book states them: existence needs only Monotone G (non-decreasing); "any solution has this form" needs StrictMono G (increasing) as an added hypothesis on the second conjunct only — per this chunk's own BRIEF.md, the crux of the theorem, and the trap this mission is most careful to avoid collapsing. Theorem 6.10's five closure clauses are stated as one conjunction (matching the book's single theorem, not five separate items); the power-series clause keeps the book's own radius-of-convergence domain restriction and adds an explicit summability hypothesis guarding the ∑' term.

Not formalized: Theorem 6.2 (Mercer's condition) — not needed by the goal's own proof chain (it is an equivalent characterization of PDS mentioned before the RKHS construction, not a premise Theorem 6.8's or 6.11's proof invokes) and its own hypotheses (compact $X\subset \mathbb R^N$, continuous $K$, an eigenfunction expansion of a compact self-adjoint integral operator) are real analytic content this mission's budget does not include; Lemma 6.7 (Cauchy-Schwarz for PDS kernels) and Lemma 6.9 (normalized PDS kernels) — supporting lemmas for Theorem 6.8's proof, not independently numbered results the goal cites; Theorem 6.12/Corollary 6.13 (Rademacher complexity/margin bounds for kernel-based hypotheses) — the chapter's optional further milestone, connecting to chunks 03/05's machinery, cut for budget; §6.5-6.8 (sequence kernels, weighted transducers, rational kernels, Bochner's theorem, approximate feature maps) — explicitly out of scope per this chunk's own BRIEF.md, a distinct, applications-heavy topic.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 6, §6.1-6.4.
• B. Schölkopf, R. Herbrich, A. J. Smola, "A generalized representer theorem," COLT 2001, Lecture Notes in Computer Science 2111, 2001, 416-426.
• N. Aronszajn, "Theory of reproducing kernels," Transactions of the American Mathematical Society 68(3), 1950, 337-404.

Motivation

Random matrices with independent entries appear whenever a system is measured through many noisy, roughly independent channels: shot noise in a sensor array, edges in an Erdős–Rényi-type random graph, or the design matrix of a linear model with independent covariates. A basic question about any such matrix $A$ is how far it can stretch a vector — its operator norm $\|A\|$ — since this single number controls the stability of every linear statistic computed from $A$: least-squares estimates, spectral clustering, covariance estimation, and random projections all reduce, at some point, to bounding $\|A\|$.

The theory traces to Marchenko and Pastur's 1967 asymptotic law for the spectrum of large random matrices, and to Bai and Yin's 1988 almost-sure limit $\|A\|/\sqrt n \to 2$ for $n \times n$ matrices with i.i.d. mean-zero, unit-variance entries. Those results are asymptotic: they say what happens as the dimension $n \to \infty$, for a fixed matrix shape. The result formalized here, Theorem 4.4.5 of Vershynin's High-Dimensional Probability (2018) (DOI 10.1017/9781108231596), belongs to the more recent non-asymptotic strand of the theory: it gives an explicit, dimension-free bound that holds at every fixed $m, n$, with an explicit failure probability — the form of statement needed for finite-sample guarantees in statistics and data science, rather than limiting behavior.

Setting

Let $A$ be an $m \times n$ real matrix. Equip $\mathbb R^n$ and $\mathbb R^m$ with the Euclidean norm $\|\cdot\|_2$; $A$ acts as a linear map $\ell_2^n \to \ell_2^m$. Its operator norm (§4.1.2) is

$$\|A\| \;:=\; \max_{x \in S^{n-1}} \|Ax\|_2 ,$$

the largest factor by which $A$ can stretch a unit vector; equivalently, the largest singular value of $A$.

A real random variable $X$ is sub-gaussian with the mission's own convention (matching the Orlicz $\psi_2$ norm this series already carries as a published definition, HighDimProb.Concentration.subgaussianNorm) if

$$\|X\|_{\psi_2} \;:=\; \inf\{t > 0 : \mathbb E \exp(X^2/t^2) \le 2\} \;<\; \infty .$$

Bounded random variables and Gaussians are sub-gaussian; a Bernoulli($p$) variable and a $\pm 1$-valued coin flip both qualify, which is why the theorem below directly covers random matrices with i.i.d. Rademacher or Gaussian entries as special cases.

The mission's proof technique is the ε-net argument, developed in §4.2 and used nowhere before this chapter of the book: a metric space $(T,d)$, a subset $K \subseteq T$, and $\varepsilon > 0$ give rise to an ε-net $N \subseteq K$ — a finite set such that every point of $K$ is within $\varepsilon$ of some point of $N$ — and a covering number $N(K, d, \varepsilon)$, the smallest cardinality of such a net. The technique reduces a statement that must hold uniformly over an infinite (compact) set to a statement about finitely many points, paid for by a union bound whose cost is controlled by the covering number.

Formalization targets

Goal (Theorem 4.4.5)

$$\exists\, C > 0 \;\text{such that}\; \forall\, t > 0,\quad \mathrm{Prob}\bigl\{\, \|A\| \le CK(\sqrt m + \sqrt n + t) \,\bigr\} \;\ge\; 1 - 2\exp(-t^2),$$

for any $m \times n$ random matrix $A$ with independent, mean-zero, sub-gaussian entries $A_{ij}$ and $K = \max_{i,j} \|A_{ij}\|_{\psi_2}$. This is the weakest stable form of the bound — it fixes no numerical value for $C$, only its existence and absoluteness (independence from $m$, $n$, $A$, $t$), so later refinements of the constant do not invalidate it.

Significance

The result itself. The bound $\|A\| \lesssim \sqrt m + \sqrt n$ is sharp up to the constant: for entries of unit variance, $\mathbb E\|A\| \ge \tfrac14(\sqrt m + \sqrt n)$ for large $m, n$ (the book's Exercise 4.4.7), so no non-asymptotic bound of this shape can be improved beyond constants. It is the entry point to the rest of the book's random matrix theory: Corollary 4.4.8 specializes it to symmetric matrices, and it underlies the community-detection (§4.5) and covariance-estimation (§4.7) applications later in the same chapter, neither of which is part of this mission.

Formalizing it. The theorem is a classical, fully proved result; nothing about its truth is open. What this mission contributes is a machine-checked formal statement — together with the two pieces of chapter infrastructure its own textbook proof names by number (Corollary 4.2.13, Exercise 4.4.3(a)) — and a third, self-contained application of the same covering-number machinery (Theorem 4.3.5) that exercises the shared IsEpsNet/coveringNumber definitions on a different metric space (the Hamming cube), independently of the Euclidean case. Mathlib and the Prove2Me platform currently have no ε-net, covering-number, or packing-number infrastructure (checked by q=random matrix, q=operator norm, q=covering number, q=net on the platform, and by filename search in Mathlib): this mission is the first to introduce it, restated inside its own namespace since it is not otherwise available to build on.

Difficulty

The obvious first approach is to bound $\|A\| = \max_{x \in S^{n-1}} \|Ax\|_2$ directly by union-bounding a concentration inequality over the sphere $S^{n-1}$. This fails outright: $S^{n-1}$ is infinite (indeed uncountable) for $n \ge 2$, so no union bound over its points can converge — the naive approach gives $\infty \cdot (\text{tail probability})$. The ε-net argument is the fix, but it is not just "discretize and hope": the reduction from the sphere to a finite net (quadratic_form_on_net, Exercise 4.4.3(a)) loses a multiplicative factor $1/(1-2\varepsilon)$ that must be tracked, and the net's cardinality (covering_numbers_of_euclidean_ball_and_sphere, Corollary 4.2.13) is exponential in the dimension ($9^n$ at $\varepsilon = 1/4$) — so the per-point tail probability from Hoeffding-type concentration must itself decay fast enough (quadratically in the exponent) to survive multiplying by $9^{m+n}$ many points. Getting the union bound to close requires choosing the threshold $u$ in the tail bound proportionally to $\sqrt m + \sqrt n + t$, not to $t$ alone — the $\sqrt m + \sqrt n$ term is exactly what pays for the net's exponential size.

Formalization scope

$A$ is represented as Ω → Matrix (Fin m) (Fin n) ℝ; its entries A ω i j are the individual real random variables. Independence of the $mn$ entries is iIndepFun over the index type Fin m × Fin n; mean-zero is the vanishing of each entry's Bochner integral. The operator norm is the norm of the associated continuous linear map between EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m) (matrixOpNorm, every linear map between finite-dimensional normed spaces being automatically continuous), matching the book's maxₓ∈Sⁿ⁻¹ ‖Ax‖₂ exactly. The sub-gaussian norm $K$ reuses this series' own published definition, HighDimProb.Concentration.subgaussianNorm, rather than a re-derivation. Covering numbers (coveringNumber) are restricted to finite (Finset) ε-nets, the only kind this chapter uses; this is a deliberate restriction, not a general-purpose covering-number formalization, and is disclosed as such. A hard-coded numeral for $C$, or an unquantified "with high probability" in place of the explicit failure probability $2\exp(-t^2)$, would each trivialize the statement and is ruled out: $C$ is existentially bound ahead of every other quantifier, and $t > 0$ is a free parameter with its own explicit bound, exactly as the book states it.

Definitions reusable beyond this mission: IsEpsNet and coveringNumber are stated for a general PseudoMetricSpace and apply unchanged to any later chapter's covering-number needs (e.g. Chapter 8's VC-dimension covering numbers), though per this series' rule that drafts cannot import drafts, a later chunk would restate rather than import them until this mission is published. matrixOpNorm is likewise chapter-agnostic. Contributions completing the sorry proofs of any of the four theorem items are welcome and independent of one another; the covering number and net-reduction items (covering_numbers_of_euclidean_ball_and_sphere, quadratic_form_on_net) are the standard prerequisites for the goal's own volumetric/ε-net proof.

Selected references

• Vershynin, R. High-Dimensional Probability: An Introduction with Applications in Data Science. Cambridge University Press, 2018. DOI 10.1017/9781108231596
• Bai, Z. D., Yin, Y. Q. "Necessary and sufficient conditions for almost sure convergence of the largest eigenvalue of a Wigner matrix." Annals of Probability 16 (1988), 1729–1741.
• Marchenko, V. A., Pastur, L. A. "Distribution of eigenvalues for some sets of random matrices." Mathematics of the USSR-Sbornik 1 (1967), 457–483.