Machine Learning

Motivation

An agent learning to control an unknown environment must balance rewards it can collect now against information that improves later decisions. In a finite Markov decision process (MDP), every action changes the distribution of the next state, so a mistaken transition estimate can affect decisions many steps later. Regret measures this loss against a policy that already knows the transition probabilities. The paper of Azar, Osband and Munos gives high-probability regret bounds for two variants of upper confidence bound value iteration (UCBVI) in finite-horizon reinforcement learning. This mission targets its Chernoff–Hoeffding variant, UCBVI-CH, whose bonus depends only on the horizon and the visit count. Theorem 1 improves the paper's cited earlier dependence on the number of states from $S$ to $\sqrt S$ in the leading term for sufficiently many interactions. Azar, Osband and Munos, 2017, pp. 2, 4–5.

The paper was released in 2017 alongside work on the attainable dependence of episodic regret on the horizon $H$, state count $S$, action count $A$, and total interaction time $T$. Its second algorithm, UCBVI-BF, uses a variance-dependent bonus and is the subject of the next mission in this series. UCBVI-CH has a simpler bonus and its own explicit bound, making it a distinct mathematical target. Azar, Osband and Munos, 2017, pp. 1–5.

Setting

The state set $\mathcal S$ and action set $\mathcal A$ are finite and nonempty, with cardinalities $S$ and $A$. A stationary transition kernel $P(y\mid x,a)$ gives the probability of moving to state $y$ after action $a$ in state $x$; each row is nonnegative and sums to one. The known, deterministic reward $R(x,a)$ lies in $[0,1]$. An episode lasts $H\ge1$ steps. The environment chooses its starting state $x_{k,1}$ before episode $k$ and may base that choice on earlier episodes. It cannot see the current episode's future random draws. Azar, Osband and Munos, 2017, §2 and Assumption 1, pp. 2–3.

A policy $\pi$ selects an action from the current state and the step number. Its value $V_h^\pi(x)$ is the expected sum of rewards from step $h$ through step $H$ when starting in state $x$. The terminal value is $V_{H+1}^\pi=0$, and $V_h^*(x)$ is the maximum of $V_h^\pi(x)$ over all such policies. Since the state, action and step sets are finite, this maximum is over a finite nonempty policy class. The paper's sentence describing $H-h$ rewards uses a shifted terminal convention; this series follows the $H$ reward steps of Algorithms 1–2. Azar, Osband and Munos, 2017, pp. 3–4.

At the start of episode $k$, UCBVI-CH forms visit counts $N_k(x,a,y)$ and $N_k(x,a)$ from earlier completed transitions. On a visited pair it uses the empirical row $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$. Algorithm 2 computes values backward from zero at the terminal step. For a visited pair, $Q_{k,h}(x,a)$ is the minimum of the preceding episode's $Q_{k-1,h}(x,a)$, $H$, and the empirical Bellman value plus Algorithm 3's bonus. For an unvisited pair, $Q_{k,h}(x,a)=H$. A maximizing action is chosen at every state, including states outside the realized path. Azar, Osband and Munos, 2017, Algorithms 1–3, pp. 3–4.

Formalization targets

Theorem 1: UCBVI-CH regret

For $K$ episodes and $T=KH$, regret sums the gap $V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})$. The goal is the paper's printed bound, with its constants:

$$\Pr\!\left\{\operatorname{Regret}(K)>20H^{3/2}L\sqrt{SAK}+250H^2S^2AL^2\right\}\le\delta, \qquad L=\ln(5HSAT/\delta),\quad \delta>0.$$

Algorithm 3 itself uses $L_{\rm alg}=\ln(5SAT/\delta)$ in its bonus $7HL_{\rm alg}/\sqrt{N_k(x,a)}$. Both logarithms remain as printed. The probability is over the MDP's next-state draws, for every admissible starting-state rule and every way of breaking ties between maximizing actions. Azar, Osband and Munos, 2017, Algorithm 3, p. 4; Theorem 1, p. 5.

Supporting results

Four milestones retain the source's indexed attack path: the Bernstein bound (9) for the empirical value error, the count-deviation display before (11), Lemma 18 on optimism, and the weighted recursion displayed in the proof of Lemma 3. The last milestone preserves the signed weights that appear before the paper's final simplification. Azar, Osband and Munos, 2017, pp. 17, 20–21, 28.

Significance

Theorem 1 gives a finite-sample failure probability with explicit dependence on $H,S,A,K$ and $\delta$. It covers a learner whose initial state can change between episodes, a feature that matters in episodic learning where the experimenter does not fix a single starting distribution. For the regime stated after Theorem 1, the leading rate is $\widetilde O(H\sqrt{SAT})$. This is a result claimed by the paper; the present Lean declarations are open proof targets, not machine-checked proofs of that claim. Azar, Osband and Munos, 2017, p. 5.

Formalizing the result creates reusable finite objects for adaptive interaction: a constructed probability law on complete paths, empirical transition counts pooled across steps, a policy value defined by its expected reward, and confidence events with their domains stated explicitly. The concentration and optimism milestones can then be investigated independently of the final regret bound. The later UCBVI-BF mission uses the same paper's model with a different bonus. Azar, Osband and Munos, 2017, pp. 3–5, 14–17.

Difficulty

The visit count $N_k(x,a)$ is random and depends on earlier observations and decisions. A concentration inequality for a predetermined number of samples therefore does not immediately give a statement that holds at every episode start. The algorithm also reuses the previous episode's $Q$ estimate through a minimum. Any optimism claim must account for this dependence across episodes as well as the backward dependence across steps. In the regret analysis, the terms called martingale differences can have either sign, so replacing a positive weight by a larger common bound can reverse an inequality. These are concrete obstacles to the printed chain of estimates. Azar, Osband and Munos, 2017, pp. 4, 17, 20–21, 28.

Formalization scope

States, actions, steps, episodes and complete outcome arrays are finite. Probabilities are finite sums of products of transition rows. The transition-row predicate is a published general definition; this mission defines the paper-specific reward-bounded MDP, policies, UCBVI-CH recursion, and path law on top of it. The starting-state rule can inspect only earlier episodes. Greedy tie-breaking is universally quantified. $V^*$ is a maximum over policies, and the bonus is read only at positive counts. A model that assigns an arbitrary probability law, fixes one starting state, or omits Algorithm 2's minimum does not represent this target. Azar, Osband and Munos, 2017, pp. 2–4.

Lean uses steps $0,\dots,H-1$ and terminal index $H$ in place of the paper's algorithmic $1,\dots,H+1$. The appendix sometimes puts the terminal value at $H$. The weighted recursion therefore runs through the final reward step, rather than ending one step early. Its typical-state threshold is $4H^2L$, as required by (34)–(36), whereas Appendix B.1 prints $2H^2L$. The proof's correction term $c_4$ dominates its other terms under $A\ge2$, which is made explicit in that milestone. The printed (11) loses a factor of two from the count display before it; only the preceding display is a milestone. Lemma 18 is stated under the empirical-model part of the confidence event and $\delta\le1$, the domain on which its bonus comparison holds. The weighted milestone retains its coefficients because the bracketed martingale terms can be negative. Azar, Osband and Munos, 2017, pp. 14–17, 20–21, 28.

The goal retains Theorem 1's constant $20$. Appendix C.1 cites Lemmas 15 and 18, but the sketch of Lemma 15 does not track that constant explicitly. Formalizing the printed bound may therefore expose a gap in its proof; the mission records the claim without weakening its constants. Contributions establishing or repairing the explicit bound, as well as the four stated milestones and reusable finite concentration results, are within scope. Azar, Osband and Munos, 2017, pp. 5, 27, 29.

Selected references

• M. G. Azar, I. Osband and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Pinned preprint.

Motivation

Online decision makers often have to choose an action before seeing the cost assigned to it. A no-regret algorithm performs almost as well, in total, as the best single action that could have been chosen after the costs were known. In a related repeated-game problem, Blackwell approachability asks a player to keep the average of vector payoffs close to a desired set despite an adversary's choices. These two performance criteria look different: one compares scalar costs to a fixed benchmark, while the other measures a geometric distance. Abernethy, Bartlett, and Hazan establish algorithmic reductions between them, with explicit finite-horizon bounds in their COLT 2011 paper. This mission isolates the direction that turns an approachability algorithm into an online linear optimization algorithm.

The bound matters even when the input algorithm has no known rate. It relates the regret of the resulting online algorithm to the actual distance attained on the corresponding sequence. Any subsequent guarantee on that distance then yields a regret guarantee through the same reduction. The paper also gives the reverse reduction and an application to calibrated forecasting; those are separate missions in this series.

Setting

Fix a dimension $d$ and a nonempty compact convex decision set $K\subseteq\mathbb R^d$. On round $t$, an algorithm selects $x_t\in K$ using only the preceding cost vectors $f_1,\ldots,f_{t-1}$. The adversary then reveals $f_t$ in the Euclidean unit ball $B_2(1)$. The incurred linear cost is $\langle f_t,x_t\rangle$. For a horizon $T$, regret compares these costs with the cost of the best single point of $K$ evaluated on all $T$ rounds:

$$\operatorname{Regret}_T = \sum_{t=1}^T\langle f_t,x_t\rangle - \min_{x\in K}\sum_{t=1}^T\langle f_t,x\rangle.$$

The minimum exists because $K$ is nonempty and compact. No probabilistic model for the cost sequence is assumed. The round index begins at one, and $x_t$ cannot depend on $f_t$.

The reduction uses $\kappa=\max_{x\in K}\|x\|$, the maximum norm of a decision. Write $a\oplus x$ for Euclidean concatenation of a scalar and a vector, an element of $\mathbb R^{d+1}$. The generated cone of a set $M$ consists of its nonnegative scalar multiples, $\operatorname{cone}(M)=\{\alpha m:\alpha\ge0,\ m\in M\}$. For a set $C$, its polar cone is $C^0=\{\theta:\langle\theta,z\rangle\le0\text{ for every }z\in C\}$. This negative-sign convention is fixed throughout the mission.

Algorithm 1 of the paper constructs a vector-payoff game. Its player actions are $K$, its adversary actions are $B_2(1)$, its payoff and target are

$$u(x,f)=\bigl(\langle f,x\rangle/\kappa\bigr)\oplus(-f), \qquad S=\operatorname{cone}(\{\kappa\}\times K)^0.$$

A Blackwell approachability algorithm for this game chooses each $x_t$ from the preceding adversary moves. Its finite-horizon approachability rate on a given sequence is $D_T(A)=\operatorname{dist}(T^{-1}\sum_{t=1}^T u(x_t,f_t),S)$, where distance means the Euclidean distance from a point to a set. The online algorithm created by Algorithm 1 uses precisely the same choices $x_t$.

Formalization targets

The goal is Theorem 16 of the paper. For every admissible history-based algorithm, every sequence of unit-ball costs, and every $T\ge1$, it asserts

$$\frac{\operatorname{Regret}_T}{T}\le 2\kappa D_T(A).$$

This is a statement about the rate actually obtained on the chosen cost sequence. It assumes no upper bound on $D_T(A)$ and does not require an oracle call in the statement. Thus it also covers algorithms whose behavior is specified directly rather than through an implementation of the oracle.

The milestone targets are the distance formula of Lemma 13, the conic distance identity in display (8) of Theorem 16's proof, and the existence of a valid halfspace oracle in Lemma 15. Lemma 13 says distance to a nonempty convex cone equals the attained maximum of a linear functional over the polar cone's unit ball. Display (8) specializes this geometry to Algorithm 1's lifted target. Lemma 15 says that every halfspace containing that target admits a player action whose payoff remains in the halfspace against every permitted adversary move. Together these statements specify the geometry and the oracle needed by the reduction.

Significance

Theorem 16 gives a numerical transfer rule: a bound on approachability distance for Algorithm 1's game immediately bounds average regret for the same sequence. Its factor depends only on the size $\kappa$ of the decision set. This permits comparison of algorithms in a common finite-horizon language, without replacing the online cost sequence by a distribution or an asymptotic limit. The source paper uses this direction as one half of its equivalence between approachability and no-regret learning Abernethy, Bartlett, and Hazan, 2011.

The mathematical results are established in that paper; the goal here is a machine-checked Lean development of their statements and eventually their proofs. The mission also supplies reusable definitions of generated and polar cones, a Euclidean lift, a finite-history online algorithm, and regret over a compact decision set. Lemma 13 is useful outside this reduction whenever distance to a cone is compared with linear functionals on its polar. The proposed theorem items currently carry open proofs, while their statements and definition files are checked for elaboration in the pinned Lean environment.

Difficulty

The main obstacle is the change of viewpoint from a scalar regret comparison to distance from a set of lifted vector payoffs. A direct comparison of individual round costs does not describe that distance. The target is a polar cone in one additional Euclidean dimension, so a faithful account must keep the lift's geometry, the cone's sign convention, and the normalization by $\kappa$ aligned. The distance formula also asserts that its maximum is attained. An encoding that merely writes an infimum or supremum with default values can silently make an edge case look valid without representing the paper's claim.

The oracle milestone has a separate quantifier demand. One selected action must work against every adversary move for each halfspace containing the target. It cannot be replaced by a possibly different action for each move, or by a claim only about tangent halfspaces. The theorem includes halfspaces with arbitrary offsets and zero normals because the source oracle accepts any containing halfspace.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d), and $a\oplus x$ lives in EuclideanSpace ℝ (Fin (d+1)) with the Euclidean norm. The generated cone uses exactly one nonnegative multiple of a point of the generating set, as in Definition 11. The polar uses $\langle\theta,z\rangle\le0$, the opposite sign from a positive dual-cone convention. Distances are Euclidean point-to-set distances. All arithmetic is over exact real numbers, and the regret minimum ranges over the image of the nonempty compact set $K$.

The statements require $\kappa>0$ because the source payoff divides by $\kappa$. This excludes the degenerate case $K=\{0\}$, in which the source instance is undefined. They require $T\ge1$ wherever an average is formed. Admissible histories consist of unit-ball adversary moves, and each round's decision belongs to $K$. The dimension may be zero syntactically, but the positive-$\kappa$ hypothesis excludes that case in results using Algorithm 1. These conditions keep the bound from being satisfied through Lean's default values for division by zero, distance to an empty set, or infima over empty sets.

The paper's display (8) writes $\operatorname{cone}(\kappa\oplus K)$ and labels its unit ball with dimension $d$; the formalization uses the cone of $\{\kappa\}\times K$ in $\mathbb R^{d+1}$, matching Algorithm 1. Lemma 12's printed bipolar claim omits closedness; this mission does not use that uncorrected sentence as a milestone. The oracle statement covers all containing halfspaces. Contributions are welcome for the distance identity, the oracle existence result, and the final regret inequality, as well as geometric lemmas supporting those proofs.

Selected references

• Jacob Abernethy, Peter L. Bartlett, and Elad Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, Proceedings of the 24th Annual Conference on Learning Theory, JMLR Workshop and Conference Proceedings 19, 2011, pp. 27–46. Published paper.

Motivation

Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of $k$ slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next request is furthest in the future is optimal (Bélády, 1966). Without that knowledge, no deterministic algorithm is better than $k$-competitive, and the best randomized algorithms are $\Theta(\log k)$-competitive (Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991).

Lykouris and Vassilvitskii asked what happens in between: an online algorithm receives, with every request, a machine-learned prediction of the element's next arrival time. A good predictor should make the algorithm nearly as good as Bélády's rule (consistency), and a bad predictor should never make it worse than a classical algorithm (robustness). Their paper (arXiv:1802.05399v4; J. ACM 2021) is one of the founding papers of learning-augmented algorithms, and its algorithm, Predictive Marker, is the reference point for the later literature on caching with predictions.

Timeline.

• 1966: Bélády's furthest-in-future rule is optimal offline.
• 1985: Sleator and Tarjan show that deterministic online paging is at best $k$-competitive.
• 1991: Fiat et al. introduce the Marker algorithm, $2H_k$-competitive, and the clean-element lower bound on the optimum.
• 2018: Lykouris and Vassilvitskii (arXiv:1802.05399) introduce Predictive Marker, with ratio $2\min(1+2S_\ell(\epsilon), 2H_k)$ for an $\epsilon$-accurate predictor.
• 2020: Rohatgi (arXiv:1910.12172, SODA 2020) and Wei (arXiv:2005.13716, APPROX/RANDOM 2020) improve the dependence on the error.

Setting

A request sequence $\sigma = (z_1, \dots, z_n)$ lists elements of a set $Z$. A cache of size $k \ge 1$ starts empty. A request for a cached element is a hit; otherwise it is a miss, the element is loaded, and if the cache is full some element is evicted first. The offline optimum $\mathrm{Opt}(\sigma)$ is the least number of misses over all eviction schedules chosen with knowledge of $\sigma$.

With each request $z_i$ the algorithm receives a real prediction $h_i$. The true label $y_i$ is the position of the next request of $z_i$, or $n+1$ if there is none. For a loss function $\ell \ge 0$, the error of the predictions is $\eta_\ell(h,\sigma) = \sum_i \ell(y_i, h_i)$, and the predictions are $\epsilon$-accurate when $\eta_\ell(h,\sigma) \le \epsilon \cdot \mathrm{Opt}(\sigma)$.

The spread of $\ell$ measures how cheaply a predictor can get the order of arrivals completely wrong: $S_\ell(m)$ is the least length $T \ge 1$ such that every strictly increasing integer sequence $a_1 < \dots < a_T$ and every non-increasing real sequence $b_1 \ge \dots \ge b_T$ have total loss $\sum_i \ell(a_i, b_i) \ge m$.

Predictive Marker (Algorithm 1) works in the phases of the Marker algorithm. Requested elements are marked. A phase ends when the cache is full, every cached element is marked, and a miss occurs; then all marks are removed. An element requested in a phase but not in the previous one is clean, and $Q(\sigma)$ is the total number of clean elements. Each clean miss starts a chain. An element evicted in the current phase that is requested again (a stale miss) extends the chain in which it was evicted. Evictions are among unmarked elements. As long as the chain's length $n(r,c)$ is at most $H_k = 1 + \tfrac12 + \dots + \tfrac1k$, the evicted element is one with the largest prediction. After that it is chosen uniformly at random. The expected number of misses of Predictive Marker is $\mathrm{cost}_{PM}(\sigma)$.

Formalization targets

Goal: Theorem 3.3

If $S$ is concave on $[0,\infty)$ and majorizes the spread, then for every $\epsilon \ge 0$, every tie-breaking rule, and every sequence with $\epsilon$-accurate predictions,

$$\mathbb E\bigl[\mathrm{cost}_{PM}(\sigma)\bigr] \le 2\cdot\min\bigl(1 + 2S(\epsilon),\ 2H_k\bigr)\cdot \mathrm{Opt}(\sigma).$$

Milestones

• Claim 1 (Fiat et al.): $Q(\sigma) \le 2\,\mathrm{Opt}(\sigma)$.
• Proof of Theorem 3.3, last sentence: $\mathrm{Opt}(\sigma) \le Q(\sigma)$.
• Lemma 3.3: a chain that evicts by the predictions only has length $n(r,c) \le 1 + S(\eta_{r,c})$, where $\eta_{r,c}$ is the error of the predictions on the elements evicted into it.
• Lemma 3.4: $\mathbb E[n(r,c)] \le \mathbb E[\min(1 + 2S(\eta_{r,c}), 2H_k)]$.

Significance

The result. Theorem 3.3 gives both guarantees at once. For an exact predictor ($\epsilon = 0$) the ratio is a constant, $2(1 + 2S(0))$, independent of $k$; for an arbitrary predictor it is $4H_k$, within a constant factor of the optimal randomized ratio. In between, the ratio degrades with the error at the rate of the spread: for the absolute loss the spread grows like $\sqrt m$, so the ratio grows like $\sqrt\epsilon$. The spread and the chain decomposition are the tools later papers build on to trade consistency against robustness.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it, of the Marker analysis, or of the clean-element bound of Fiat et al. is known. A formalization supplies a precise model of a randomized online algorithm with predictions. It also settles the details the paper leaves implicit: the eviction missing from the clean branch of Algorithm 1 as printed, the cap $2H_k$ printed as $2\log k$ in Lemma 3.4, and the behaviour of the spread at $0$.

Difficulty

The obvious argument charges every miss to a chain and bounds each chain separately. That works for chains that follow the predictions, but a chain that switches to random evictions interacts with every other chain of the phase, because all of them evict from the same pool of unmarked elements. A bound on its expected length must hold whatever the other chains evict, including evictions that depend on earlier coin flips. A second difficulty is summing. The chain errors $\eta_{r,c}$ and the chain lengths are both random, while the hypothesis controls only the total error $\eta_\ell(h,\sigma)$ against $\mathrm{Opt}(\sigma)$, not the number of chains $Q(\sigma)$ in which the error is spread.

Formalization scope

Elements form a type with decidable equality. A request sequence is a list; predictions are one real per request, and every real sequence is allowed. Labels are 1-based next-arrival positions, with $n+1$ for elements never requested again. The paper prints the label with equal features; the element is meant. $\mathrm{Opt}$ is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. $H_k$ is harmonic k as a real number, never $\log k$.

Predictive Marker is a PMF over final states. The random eviction of line 21 is uniform over the unmarked cached elements, and ties in the arg max are a parameter quantified universally. The eviction of lines 23–24 is also performed after a clean miss; as printed, it sits only in the stale branch. The expected cost lies in $[0,\infty]$.

The spread takes real arguments and lengths $T \ge 1$. $S$ must be concave on $[0,\infty)$, finite, and at least the spread. It must also be continuous at $0$, which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays $0$ over several lengths. $\epsilon$-accuracy is the pointwise condition on the given pair $(\sigma, h)$. The competitive ratio is written as a product, so $\mathrm{Opt}(\sigma) = 0$ needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has $2H_k$ in place of the printed $2\log k$, with the minimum inside the expectation because $\eta_{r,c}$ is random.

The statement must not be trivialized. $\mathrm{Opt}$ is the true offline optimum, not Bélády's rule applied to the predictions. The expectation is taken over Predictive Marker's own run, never compared with itself. The spread hypothesis is satisfiable; for example, the constant loss $1$ has spread $\max(1,\lceil m\rceil) \le m + 1$.

Out of scope: Lemma 3.2 (the special-marking algorithm SM, which enters only through Lemma 3.4's proof); Lemma 3.1 and Corollaries 1–2, whose printed constants are false for small $m$ or disagree with Theorem 3.3; the lower bounds of §3.1 and §3.4; the extensions of §4; the experiments of §5; running time and learnability.

Welcome contributions: the Marker phase structure and its equivalence with the combinatorial phases, the clean-element bounds $Q/2 \le \mathrm{Opt} \le Q$ (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.

Selected references

• T. Lykouris, S. Vassilvitskii, Competitive Caching with Machine Learned Advice, arXiv:1802.05399v4, 2020; J. ACM 68(4), 2021. https://arxiv.org/abs/1802.05399v4
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12(4), 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• L. A. Bélády, A study of replacement algorithms for a virtual-storage computer, IBM Systems Journal 5(2), 1966. https://doi.org/10.1147/sj.52.0078
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2), 1985. https://doi.org/10.1145/2786.2793
• D. Rohatgi, Near-optimal bounds for online caching with machine learned advice, SODA 2020. https://arxiv.org/abs/1910.12172
• A. Wei, Better and simpler learning-augmented online caching, APPROX/RANDOM 2020. https://arxiv.org/abs/2005.13716

Motivation

A retailer who sells several products from shared, non-replenishable inventory over a finite season must set prices without knowing how demand responds to them. Every price posted is both a sale and an experiment. This is the network revenue management problem with demand learning, and it sits between two literatures: dynamic pricing with inventory, where demand is known and the fluid linear program of Gallego and van Ryzin (1997) is the standard benchmark, and multi-armed bandits, where learning is the whole problem but there are no resource constraints.

Ferreira, Simchi-Levi and Wang (Oper. Res. 2018) combine Thompson sampling with a linear-programming step: sample a demand model from the posterior, solve the fluid LP for that model, and randomize prices according to its solution. The same paper extends the scheme to continuous price sets, contextual pricing and bandits with knapsacks.

Timeline of the relevant results:

• 1997: Gallego and van Ryzin introduce the fluid LP upper bound for network revenue management with known demand.
• 2012: Besbes and Zeevi give a non-Bayesian network pricing algorithm with worst-case regret $O(K^{5/3}T^{2/3}\sqrt{\log T})$.
• 2013: Badanidiyuru, Kleinberg and Slivkins (bandits with knapsacks) give worst-case regret $O(\sqrt{KT\log T})$.
• 2013–2014: Bubeck and Liu and Russo and Van Roy give prior-free Bayesian regret bounds for Thompson sampling in unconstrained bandits.
• 2018: Ferreira, Simchi-Levi and Wang prove the $O(\sqrt{TK\log K})$ Bayesian regret bound for TS-fixed (Theorem 1), the target of this mission.

Setting

There are $N$ products and $M$ resources. One unit of product $i$ consumes $a_{ij}\ge0$ units of resource $j$, and resource $j$ starts with inventory $I_j\ge0$ that is never replenished. The season has $T$ periods. In each period the retailer posts one of $K$ price vectors $p_k=(p_{1k},\dots,p_{Nk})$ or a shut-off price $p_\infty$ under which demand is zero.

Given the posted price $p_k$, the demand vector $D(t)\in\mathbb R^N_+$ has law $F(\cdot\,;p_k,\theta)$, where $\theta\in\Theta$ is unknown and drawn from a known, arbitrary prior $\mu_0$. Demand is independent of the past given the posted price and $\theta$, and is bounded: $D_i(t)\in[0,\bar d_i]$. Write $d_{ik}(\rho)$ for the mean demand of product $i$ under $p_k$ and parameter $\rho$, and $d=d(\theta)$.

When inventory covers all demand, all demand is sold. Otherwise the satisfied demand $\tilde D(t)$ satisfies $0\le\tilde D_i(t)\le D_i(t)$, leaves every inventory nonnegative, and leaves at least one resource at zero; no other rule is imposed. Revenue is $\mathrm{Rev}(T)=\sum_t\sum_i\tilde D_i(t)P_i(t)$.

For a mean-demand matrix $d$ and capacities $c_j=I_j/T$, the linear program $\mathrm{LP}(d)$ is

$$\max_{x\ge0}\ \sum_{k=1}^K\Bigl(\sum_{i=1}^N p_{ik}d_{ik}\Bigr)x_k\quad\text{s.t.}\quad\sum_{k=1}^K\Bigl(\sum_{i=1}^N a_{ij}d_{ik}\Bigr)x_k\le c_j\ \ \forall j,\qquad\sum_{k=1}^K x_k\le1,$$

with optimal value $\mathrm{OPT}(d)$.

TS-fixed (Algorithm 1): in each period, sample $\theta(t)$ from the posterior of $\theta$ given the history of posted prices and observed demands; let $x(t)$ be an optimal solution of $\mathrm{LP}(d(\theta(t)))$; post $p_k$ with probability $x_k(t)$ and $p_\infty$ with the remaining probability; observe demand and update the posterior.

Finally $p_{\max}=\max_k\sum_ip_{ik}\bar d_i$ and $p^j_{\max}=\max_{i:a_{ij}\neq0,\,k}p_{ik}/a_{ij}$.

Formalization targets

Goal: Theorem 1 against the LP benchmark

For $K\ge2$, $T\ge1$, every prior, every bounded demand family, every admissible fulfilment rule and every run of TS-fixed,

$$\mathbb E\bigl[\mathrm{OPT}(d)\bigr]\cdot T-\mathbb E\bigl[\mathrm{Rev}(T)\bigr]\ \le\ \Bigl(18\,p_{\max}+37\sum_{i=1}^N\sum_{j=1}^M p^j_{\max}a_{ij}\bar d_i\Bigr)\sqrt{TK\log K}.$$

The paper prints this bound for $\mathrm{BayesRegret}(T)=\mathbb E[\mathrm{Rev}^*(T)]-\mathbb E[\mathrm{Rev}(T)]$, where $\mathrm{Rev}^*$ is the revenue of the optimal policy that knows $\theta$; see Formalization scope for why the LP benchmark is stated instead.

Milestones

The article states Theorem 1 and says that its proof is in the online appendix (Supplemental Material at the DOI). The article itself contains no numbered lemma. The milestone list is therefore empty; the appendix's lemmas will be added as milestones once the appendix is held.

Significance

The bound is prior-free and has explicit constants that depend only on prices, consumption rates and demand bounds. Its dependence on $T$ matches the $\Omega(\sqrt{KT})$ lower bound for Bayesian regret in unconstrained bandits with rewards in $[0,1]$, a special case of the model with no inventory constraints (Bubeck and Cesa-Bianchi 2012, Theorem 3.5). It shows that the posterior-sampling principle survives the addition of resource constraints, lost sales and randomized LP-based pricing, and it is the template for the paper's later results (TS-update, contextual pricing, bandits with knapsacks).

The theorem is proved on paper but, as far as a platform search shows, not formalized anywhere. The platform has a formal proof of the unconstrained Bayesian Thompson sampling bound $\sqrt{kn\log k/2}$ (BanditAlgorithm.thompson_sampling_bayesian_regret, Lattimore–Szepesvári Theorem 36.5) and an open single-product deterministic upper bound in revenue management (RevenueManagement.deterministic_upper_bound). Neither has inventory, an LP subroutine, or lost sales. A formal proof here would supply the first machine-checked analysis of Thompson sampling under resource constraints and would check the paper's constants.

Difficulty

In an unconstrained bandit, Thompson sampling's regret reduces to a sum of per-period gaps between an upper confidence bound and the sampled reward, because the sampled optimal arm and the true optimal arm are identically distributed given the history. Here the action is a randomized mixture $x(t)$ from an LP, the reward is not additive in the prices chosen, and revenue is lost when inventory runs out. Two quantities must be controlled: the revenue the algorithm would collect if all demand could be served, and the revenue lost to stock-outs. The second depends on the random time at which each resource is exhausted under a pricing rule that was optimized for a sampled, not the true, demand, and on an arbitrary fulfilment rule once some resource is empty. Standard bandit arguments do not bound such lost sales, which are a nonlinear function of the whole trajectory.

Formalization scope

Lean representation. Products, resources and price vectors are indexed by Fin N, Fin M, Fin K; the posted price is an Option (Fin K) with none the shut-off price. Periods are 0-based ($t=0,\dots,T-1$ stands for the paper's $1,\dots,T$). $\Theta$ is a standard Borel space with a probability measure $\mu_0$; demand is a Markov kernel $F$ from $\Theta\times$Fin K to $\mathbb R^N$, bounded in $[0,\bar d_i]$ for every parameter. A run of TS-fixed is a family of random variables on a probability space satisfying, almost surely and via conditional expectations: $\theta\sim\mu_0$; the posterior-sampling property of $\theta(t)$ given everything before period $t$; the price draw with probabilities $x(\theta(t))$ for a measurable optimal LP selection $x$; the demand law given the past, $\theta(t)$ and the posted price; and fulfilment rules (a)/(b). The logarithm is natural. Prices, consumption and inventory are nonnegative (implicit in the paper). $\mathrm{OPT}(d)$ is a supremum over a nonempty bounded feasible set, so it has no junk value.

Corrections to the printed statement.

1. $K\ge2$ is added. At $K=1$ the printed right-hand side is $0$, yet on a one-price instance with Bernoulli$(0.8)$ demand, $I=T/2$ and a point-mass prior, TS-fixed loses about $0.2p\sqrt T$ in expectation.
2. The LP benchmark replaces $\mathbb E[\mathrm{Rev}^*(T)]$. Section 3.1.1 bounds $\mathbb E[\mathrm{Rev}^*(T)\mid d]$ by $\mathrm{OPT}(d)\cdot T$, citing Gallego–van Ryzin. Under the paper's fulfilment rule this fails when products use disjoint resources: with two products, $I=(T,1)$, $p_1=(1,0)$, $p_2=(1/2,0)$ and deterministic demand $(1,1)$, the known-$\theta$ policy earns at least $T$ while $\mathrm{OPT}(d)\cdot T=1$. The paper states that its proof bounds the gap to "the LP benchmark defined in Section 3.1.1" (p. 1594), and the last display of Section 3.1.1 bounds $\mathrm{BayesRegret}(T)$ by exactly $\mathbb E[\mathrm{OPT}(d)]\cdot T-\mathbb E[\mathrm{Rev}(T)]$. Wherever the Gallego–van Ryzin bound holds, the corrected goal implies the printed one.

Ruled out. A bound for the "ideal" revenue $\sum_iD_i(t)P_i(t)$ instead of the satisfied revenue, or for an arbitrary policy whose prices are merely close to the LP solution, is not Theorem 1; the goal carries the full TS-fixed run and the lost-sales accounting.

Infrastructure needed. Posterior-sampling identities for general (standard Borel) priors, a Hoeffding/Azuma-type concentration for bounded demand along the price-selection process, LP sensitivity with respect to the mean-demand matrix, and a pathwise bound on lost sales under an arbitrary fulfilment rule. The LP and fluid-benchmark definitions are reusable for later missions on TS-update (Theorem 2), contextual pricing (Theorem 4) and bandits with knapsacks (Theorem 5). Contributions welcome: proofs of the goal, and formal statements of the online appendix's lemmas.

Selected references

• K. J. Ferreira, D. Simchi-Levi, H. Wang, Online Network Revenue Management Using Thompson Sampling, Operations Research 66(6):1586–1602, 2018. https://doi.org/10.1287/opre.2018.1755
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1):24–41, 1997. https://doi.org/10.1287/opre.45.1.24
• O. Besbes, A. Zeevi, Blind Network Revenue Management, Operations Research 60(6):1537–1550, 2012. https://doi.org/10.1287/opre.1120.1057
• A. Badanidiyuru, R. Kleinberg, A. Slivkins, Bandits with Knapsacks, FOCS 2013. https://arxiv.org/abs/1305.2545
• S. Bubeck, C.-Y. Liu, Prior-free and Prior-dependent Regret Bounds for Thompson Sampling, NeurIPS 2013. https://arxiv.org/abs/1311.0466
• D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4):1221–1243, 2014. https://doi.org/10.1287/moor.2014.0650
• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://arxiv.org/abs/1204.5721
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 36. https://doi.org/10.1017/9781108571401

Motivation

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

Setting

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

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

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

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

is the finite-dimensional relaxation the chapter builds toward.

Formalization targets

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Nguyen, V. A., Shafieezadeh-Abadeh, S., Yue, M.-C., Kuhn, D., & Wiesemann, W. (2021). Optimistic distributionally robust optimization for nonparametric likelihood approximation. Advances in Neural Information Processing Systems, 32.
• Shafieezadeh-Abadeh, S., Nguyen, V. A., Kuhn, D., & Mohajerin Esfahani, P. (2018). Wasserstein distributionally robust Kalman filtering. Advances in Neural Information Processing Systems, 31.

Motivation

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

Setting

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

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

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

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

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

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

Formalization targets

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

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Gelbrich, M. (1990). On a formula for the L2 Wasserstein metric between measures on Euclidean and Hilbert spaces. Mathematische Nachrichten, 147(1), 185–203.
• Mohajerin Esfahani, P., & Kuhn, D. (2018). Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations. Mathematical Programming, 171(1), 115–166.

Motivation

Every consistency guarantee for an empirical-risk-minimization procedure — the Lasso, kernel ridge regression, maximum likelihood — ultimately rests on relating an empirical average to its population expectation, uniformly over the class of candidate functions or parameters being searched. Chapter 4 established the classical form of this connection: a uniform law of large numbers, bounding $\sup_{f\in F}|\|f\|_n^2-\|f\|_2^2|$ by an absolute quantity governed by the (unlocalized) complexity of $F$. Such a bound is often wasteful: it treats a function with small population norm the same as one with large population norm, when intuitively the empirical and population norms of a small function should already agree closely. This mission formalizes the sharper, localized form of this uniform law — the same localization principle Chapter 13 used for nonparametric least squares, now applied directly to the empirical-versus-population norm comparison itself, giving relative rather than absolute control and recovering optimal convergence rates that the unlocalized theory misses.

Setting

Fix a probability distribution $P$ over a covariate space $X$ and $n$ i.i.d. samples $x_1,\dots,x_n\sim P$. For $f:X\to\mathbb R$, the population norm is $\|f\|_2^2:=\int_Xf(x)^2\,P(dx)$ and the empirical norm is $\|f\|_n^2:=\frac1n\sum_{i=1}^nf(x_i)^2$; by linearity of expectation, $\mathbb E[\|f\|_n^2]=\|f\|_2^2$, so the question is how tightly $\|f\|_n^2$ concentrates around $\|f\|_2^2$, uniformly over a function class $F$. A class $F$ is star-shaped around the origin if $f\in F,\alpha\in[0,1]\implies\alpha f\in F$, and $b$-uniformly bounded if $\|f\|_\infty\le b$ for every $f\in F$. The relevant complexity measure is the population localized Rademacher complexity

$$R_n(\delta;F) := \mathbb E_{\varepsilon,x}\Big[\ \sup_{f\in F,\ \|f\|_2\le\delta}\ \Big| \tfrac1n\sum_{i=1}^n\varepsilon_if(x_i)\Big|\ \Big],$$

where $\varepsilon_1,\dots,\varepsilon_n$ are i.i.d. Rademacher signs independent of the samples — note that, unlike Chapter 13's Gaussian complexity for fixed design points, this expectation integrates out the randomness of the samples themselves, since this chapter treats $\{x_i\}$ as genuinely random throughout. A critical radius $\delta_n$ is any positive solution of $R_n(\delta;F)\le\delta^2/b$.

Formalization targets

Theorem 14.1 (goal). Given $F$ star-shaped and $b$-uniformly bounded, and $\delta_n$ solving the critical inequality, for any $t\ge\delta_n$,

$$\Big|\|f\|_n^2-\|f\|_2^2\Big|\le\frac12\|f\|_2^2+\frac{t^2}2 \qquad\text{for all }f\in F,$$

with probability at least $1-c_1e^{-c_2nt^2/b^2}$; and if additionally $n\delta_n^2\ge\frac2{c_2}\log(4\log(1/\delta_n))$,

$$\big|\|f\|_n-\|f\|_2\big|\le c_0\delta_n \qquad\text{for all }f\in F,$$

with probability at least $1-c_1'e^{-c_2'n\delta_n^2/b^2}$.

Significance

Theorem 14.1 is the technical engine behind two of the book's other sharp results: Example 14.2's derivation of the optimal $n^{-1/2}$ rate for bounded quadratic function classes (where the unlocalized analogue of this theorem only achieves the slower $n^{-1/4}$ rate), and, more broadly, every later argument in the book that needs to translate an empirical-norm guarantee (as produced directly by an M-estimator's optimality, e.g. Chapter 13's nonparametric least-squares bounds) into a population-norm guarantee, or vice versa. The gap between the "absolute" uniform law of Chapter 4 and the "relative" one here is exactly the difference between a bound that is only informative for functions of order-one population norm, and one that remains sharp arbitrarily close to the origin — which is precisely where a consistent estimator's error eventually lives. Formalizing the statement produces, for the first time on the platform, the localized-Rademacher-complexity vocabulary at the population level (as opposed to Chapter 13's fixed-design Gaussian-complexity version), reusable by any future mission needing to pass between empirical and population norms.

Difficulty

The naive approach — apply Hoeffding's inequality to $|\|f\|_n^2-\|f\|_2^2|$ for a fixed $f$, then union-bound (or apply the unlocalized Rademacher-complexity uniform law of Chapter 4) over $F$ — gives a bound whose complexity term does not shrink as $\|f\|_2\to0$, since it uses the complexity of all of $F$ regardless of a given function's own size. This is exactly the sub-optimality Example 14.2 exhibits concretely: the naive bound gives rate $n^{-1/4}$ where the truth is $n^{-1/2}$. The fix is not merely technical bookkeeping — it requires a genuine peeling argument over dyadic norm-scales (exactly as in Chapter 13's proof of Theorem 13.13), applying the localized complexity $R_n(\delta;F)$ at the scale $\delta=\|f\|_2$ appropriate to each individual $f$, and controlling the resulting geometric sum of tail probabilities across scales. A reader's first instinct — bound $\|f\|_2$ in terms of $\|f\|_n$ and substitute — is circular, since $\|f\|_n$ is itself the random quantity being controlled.

Formalization scope

The covariate space X carries an arbitrary MeasurableSpace structure (no topology needed for the statement); the sample sequence and the Rademacher signs are both represented as families of measurable functions on a shared probability space Ω, with their joint independence stated as a single IndepFun between the two vector-valued sequences (rather than building a combined-index iIndepFun), since it is the two sequences — not each pair of individual variables — whose independence the book invokes. The two conclusions of Theorem 14.1 are stated as a conjunction with the second gated behind its own extra hypothesis, never collapsed into a single implication, since the book's own statement keeps them syntactically and logically distinct (the second requires a strictly stronger and additional condition on top of the first's). The universal constants (c1,c2,c0,c1',c2') are quantified before every instance object, so they cannot secretly depend on the function class, sample size, or radius. Every f ∈ F is required measurable (hF_meas, added in revision): the book's own framing implicitly restricts to measurable, square-integrable f throughout (p. 454), and without this hypothesis the population norm popNormSq, which appears directly in the goal's conclusion, could silently take Mathlib's Bochner-integral junk value 0 for a non-measurable, pointwise-bounded member of a star-shaped, uniformly-bounded F. The trivializing formalization ruled out here is stating the localization constraint at the empirical rather than population norm in popRademacherComplexity — this chapter's whole point (contrast Chapter 13's Gn, correctly localized at the empirical norm since there the design is fixed) is that $R_n(\delta;F)$'s localization is a population-level object, precisely because the samples are random here. Welcome future contributions: Corollary 14.3's covering-number sufficient condition for the empirical version of the critical inequality, and Theorem 14.20's Lipschitz/strongly-convex cost-function uniform law, both deferred from this mission (see STATUS.md) as they need substantial additional apparatus (metric entropy integrals; cost functions and strong convexity) beyond what Theorem 14.1 itself requires.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 14. https://doi.org/10.1017/9781108627771
• P. Bartlett, O. Bousquet and S. Mendelson, "Local Rademacher complexities," Annals of Statistics, 33(4):1497-1537, 2005. https://doi.org/10.1214/009053605000000282
• V. Koltchinskii, "Local Rademacher complexities and oracle inequalities in risk minimization," Annals of Statistics, 34(6):2593-2656, 2006. https://doi.org/10.1214/009053606000001019

Motivation

Many high-dimensional data sets — gene-expression profiles, sensor networks, social interactions — come with no natural ordering of variables, only pairwise dependencies whose structure is itself the object of interest. A graphical model encodes these dependencies as an undirected graph: vertices are variables, and edges mark direct (conditional) dependence. Recovering the graph from samples — graphical model selection — is a combinatorial problem masquerading as a statistical one: there are $2^{\binom{d}{2}}$ candidate graphs on $d$ vertices, far too many to search directly. For Gaussian data, however, graph structure is exactly the sparsity pattern of the inverse covariance (precision) matrix, which turns graph selection into $d$ coupled sparse-regression problems — one per vertex — each of which the Lasso theory of Chapter 7 already knows how to solve. This mission formalizes the theorem, due to Meinshausen and Bühlmann (2006), that shows this reduction actually works: solving $d$ independent Lasso problems and combining the results recovers the exact graph with high probability, at a sample complexity governed by the same kind of incoherence condition that governs Lasso support recovery itself.

Setting

An undirected graphical model on a finite vertex set $V$ pairs a graph $G=(V,E)$ with a random vector $X=(X_j)_{j\in V}$. Two equivalent structural properties connect $X$ to $G$ (Theorem 11.8, Hammersley-Clifford): $X$ factorizes according to $G$ if its density is a product of nonnegative functions, one per clique of $G$, each depending only on the variables in that clique (Definition 11.1); $X$ is Markov with respect to $G$ if, for every vertex cutset $S$ separating $V$ into disjoint pieces $A$ and $B$, the sub-vectors $X_A$ and $X_B$ are conditionally independent given $X_S$ (Definition 11.5). For a strictly positive density, these are the same condition.

For a zero-mean $d$-dimensional Gaussian vector with covariance $\Sigma^*$ and precision matrix $\Theta^*=(\Sigma^*)^{-1}$, the graph structure is exactly the support of $\Theta^*$: $(j,k)\in E \iff \Theta^*_{jk}\ne0$. The neighborhood $N(j):=\{k\mid(j,k)\in E\}$ of each vertex is itself a vertex cutset (separating $\{j\}$ from everything else), so the conditional independence $X_j\perp X_{V\setminus N^+(j)}\mid X_{N(j)}$ holds, and — by standard Gaussian conditioning — $X_j$ decomposes as a linear function of $X_{V\setminus\{j\}}$ plus independent Gaussian noise, with regression coefficients supported exactly on $N(j)$. Neighborhood regression exploits this directly: for each vertex $j$, solve the Lasso

$$\hat\theta_j \in \arg\min_{\theta\in\mathbb R^{d-1}}\ \frac1{2n}\|X_j-X_{\setminus\{j\}}\theta\|_2^2 +\lambda_n\|\theta\|_1,$$

read off $\hat N(j):=\{k\mid\hat\theta_{j,k}\ne0\}$, and combine the $d$ per-vertex estimates into a single edge set via the OR rule ($(j,k)\in\hat E_{\mathrm{OR}}$ iff $k\in\hat N(j)$ or $j\in\hat N(k)$) or the more conservative AND rule (iff both hold). The relevant incoherence condition, analogous to Chapter 7's, is stated for a positive definite matrix $\Gamma$ and subset $S$: $\Gamma$ is $\alpha$-incoherent with respect to $S$ if $\max_{k\notin S}\|\Gamma_{kS}(\Gamma_{SS})^{-1}\|_1\le1-\alpha$.

Formalization targets

Theorem 11.8 (Hammersley-Clifford). Factorizes G p ↔ IsMarkov G X P for any strictly positive density $p$.

Theorem 11.12 (goal — graph selection consistency). Suppose for every $j$, $\Sigma^*_{\setminus\{j\}}$ is $\alpha$-incoherent with respect to $N(j)$, and $|\!|\!|(\Sigma^*_{N(j),N(j)})^{-1}|\!|\!|_\infty\le b$. With $\lambda_n=c_0\frac1\alpha(\sqrt{\log d/n}+\delta)$, the neighborhood-Lasso estimate combined via either rule satisfies, with probability at least $1-c_2e^{-c_3n\min(\delta^2,1/m)}$:

$$\hat E\subseteq E \qquad\text{and}\qquad \forall (j,k):\ |\Theta^*_{jk}|\ge7b\lambda_n \implies (j,k)\in\hat E.$$

Significance

Theorem 11.12 is the statistical justification for one of the two standard approaches to Gaussian graphical model selection (the other being the penalized-likelihood "graphical Lasso" of §11.2.1). Its significance is computational as much as statistical: rather than solving one $d$-dimensional penalized-likelihood problem, neighborhood regression solves $d$ independent, embarrassingly parallel Lasso problems, each of dimension $d-1$ — a substantial practical advantage at scale, with (as this theorem shows) no loss in statistical guarantee. Formalizing it produces, for the first time on the platform, statement-level infrastructure for undirected graphical models (Hammersley-Clifford, the Markov property via vertex cutsets, neighborhood structure) together with the random-design analogue of the Lasso support-recovery machinery — a genuinely different technical regime from Chapter 7's fixed-design Lasso theory, since here the "design matrix" $X_{\setminus\{j\}}$ is itself Gaussian and statistically coupled to the response $X_j$ through the very covariance structure being estimated. As with the other missions in this series, only the statements are formalized here; the proofs (an extension of the primal-dual witness technique to random design, per the book's own proof sketch) are left as the draft goal for future proof contributions.

Difficulty

The proof of Theorem 7.21 (Chapter 7's Lasso support-recovery guarantee) is for a deterministic design matrix, with all randomness confined to the additive noise. Here the "design" $X_{\setminus\{j\}}$ is itself random and Gaussian, and — critically — it is statistically dependent on the very quantity ($N(j)$, encoded in $\Theta^*$'s support) the Lasso is trying to recover, since $X_{\setminus\{j\}}$'s own covariance structure is exactly what the incoherence condition constrains. The naive approach of just conditioning on the realized design matrix and invoking Theorem 7.21 fails, because the deterministic-design incoherence condition would then need to hold for the sample covariance $\Gamma=\frac1n X_{\setminus\{j\}}^TX_{\setminus\{j\}}$, not the population covariance $\Sigma^*_{\setminus\{j\}}$ that is actually assumed — and controlling the gap between sample and population incoherence under the joint (not fixed) randomness of predictors and response is exactly the extra step the book's proof needs, handled via an extension of the primal-dual witness technique that tracks both sources of randomness together.

Formalization scope

The vertex set V is an arbitrary finite type; the covariate space for X is ℝ throughout (all variables jointly Gaussian). The Gaussian design is characterized via its one-dimensional projections (every linear combination is univariate Gaussian with the matching variance) rather than via Mathlib's multivariate-Gaussian machinery directly, to keep the definition self-contained. IsAlphaIncoherent's ambient index set is realized as a subset of the full vertex type rather than as a literal submatrix, since the book's condition never references an entry outside it. The theorem states the conclusion jointly for both the OR-rule and AND-rule estimated edge sets on one shared high-probability event, matching "based on either rule" literally rather than picking one. The trivializing formalization ruled out here is treating the neighborhood-Lasso estimate as a fixed-design Lasso problem (silently dropping the joint randomness of predictors and response) — every design realization in this formalization is the actual random vector Xdes i ω, not a deterministic parameter, and the Gaussian design hypothesis (IsIIDGaussianDesign) is stated over the same probability space Ω as the least-squares residual. Theorem 11.8 (Hammersley–Clifford) is formalized only for the continuous case — a random vector with a density with respect to Lebesgue measure — matching what the Gaussian goal (Theorem 11.12) actually needs; the book's own Definition 11.1 also permits a discrete (counting-measure) density, with the Ising model (Example 11.4) as a worked instance, which this mission does not cover. Contributions welcome: the graphical Lasso's own guarantees (Propositions 11.9, 11.10, deferred from this mission — see STATUS.md), and the proof of Theorem 11.12 itself via the primal-dual witness extension the book sketches.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 11. https://doi.org/10.1017/9781108627771
• N. Meinshausen and P. Bühlmann, "High-dimensional graphs and variable selection with the Lasso," Annals of Statistics, 34(3):1436-1462, 2006. https://doi.org/10.1214/009053606000000281
• J. Hammersley and P. Clifford, "Markov fields on finite graphs and lattices," unpublished manuscript, 1971.

Motivation

A striking fact discovered by Dvoretzky in the 1960s (conjectured by Grothendieck, and sharpened into its modern quantitative form by Milman in 1971) is that every high-dimensional convex body, however irregular, contains a round slice: a random low-dimensional section (or projection) of any bounded convex set in $\mathbb R^n$ is, with high probability, close to a Euclidean ball — provided the dimension of the slice is small enough relative to a single geometric parameter of the body. This is remarkable because it holds for every bounded set, arbitrarily irregular; no special structure is assumed beyond boundedness. This chapter proves the theorem in its Gaussian form, as a culmination of every geometric and probabilistic tool the book develops: chaining and Dudley's inequality (Chapter 8), the matrix deviation inequality (Chapter 9), and Gaussian width and the stable dimension (Chapter 7) all combine into a single closing argument.

Setting

Fix a subset $T\subseteq\mathbb R^n$. For a standard Gaussian vector $g\sim N(0,I_n)$, the Gaussian width of $T$ is $w(T) := \mathbb E\sup_{x\in T}\langle g,x\rangle$ (Chapter 7), and the stable dimension of a bounded $T$ is $d(T) := w(T)^2/\mathrm{diam}(T)^2$ up to an absolute constant factor (Definition 7.6.2) — a robust substitute for the ordinary linear-algebraic dimension of $T$, which can jump discontinuously under a small perturbation of $T$, unlike $d(T)$.

An $m\times n$ Gaussian random matrix with i.i.d. $N(0,1)$ entries is a random matrix $A$ each of whose $mn$ entries is an independent standard normal random variable.

Formalization targets

Goal (Theorem 11.3.3, Dvoretzky-Milman's theorem, Gaussian form)

$$\exists\,c>0:\quad m\le c\varepsilon^2 d(T) \;\Longrightarrow\; \mathbb P\bigl[(1-\varepsilon)B \subseteq \mathrm{conv}(AT) \subseteq (1+\varepsilon)B\bigr] \ge 0.99$$

for every $m\times n$ Gaussian random matrix $A$ with i.i.d. $N(0,1)$ entries, every bounded $T\subseteq\mathbb R^n$ containing the origin, and every $\varepsilon\in(0,1)$, where $B$ is the Euclidean ball of radius $w(T)$ centered at the origin. The probability $0.99$ is the book's own literal numeral, not a free parameter — this is the theorem the book actually states, not a family of theorems indexed by a confidence level.

Significance

Dvoretzky-Milman's theorem is one of the foundational results of the local theory of Banach spaces (asymptotic geometric analysis): it says every $n$-dimensional normed space contains an almost-Euclidean subspace of dimension proportional to (a geometric invariant closely related to) $\log n$ in the worst case, and much larger for spaces whose unit ball is already well-behaved (the stable dimension of the cube $[-1,1]^n$, for instance, is proportional to $n$ itself — Example 11.3.6). This underlies results throughout convex geometry, compressed sensing, and high-dimensional statistics wherever a random low-dimensional projection needs to be shown to preserve geometric structure. The book's own framing makes clear why this chapter is placed last: the theorem's proof is a genuine capstone, invoking Chevet's inequality (itself built from the matrix deviation inequality of Chapter 9, which is built from chaining, Chapter 8) as its main technical tool.

The theorem and its proof are classical (Milman 1971; this book's specific route via Chevet's inequality is a standard modern exposition). This mission formalizes the goal theorem's statement — including its two supporting geometric quantities, Gaussian width and stable dimension, and the notion of a Gaussian random matrix — as a complete, faithful target for a solver, in the book's own sub-namespace built for this chapter (no dependency here is reusable from an earlier chunk, since none of this book series' Chapter 7 or Chapter 9 definitions has yet been published).

Difficulty

The natural first idea — bound $\mathrm{conv}(AT)$ directly using concentration of $\|Ax\|_2$ for each fixed $x\in T$ — runs into exactly the uniform-supremum obstacle the whole book has been building tools to overcome: a bound that holds for one $x$ at a time, even with a union bound over a net of $T$, does not obviously extend to the full convex hull without first controlling $\sup_{x\in T}|\langle Ax,y\rangle - w(T)\|y\|_2|$ uniformly over both $x\in T$ and $y$ on the unit sphere of the target space — a two-parameter supremum. The book's actual route goes through Chevet's inequality, itself proved using the matrix deviation inequality's own chaining-based argument, to control this two-sided supremum, and then converts the resulting inequality into the containment $(1-\varepsilon)B\subseteq\mathrm{conv}(AT)\subseteq(1+\varepsilon)B$ via a support- function duality argument (a convex body is pinned down by its support function, so bounding $\sup_{x\in T}\langle Ax,y\rangle$ uniformly over $y$ on the sphere is exactly what is needed).

Formalization scope

A is Ω → Matrix (Fin m) (Fin n) ℝ with an explicit IsGaussianMatrix hypothesis (entries i.i.d. $N(0,1)$, formalized entrywise with joint independence). conv(AT) is convexHull ℝ of the image of T under A's mulVec, round-tripped through EuclideanSpace's continuous linear equivalence with the underlying function type. w(T) reuses this mission series' ExpSup/GaussianWidth convention (redefined locally, per the drafts-cannot-import-drafts rule, following the same ProbabilityTheory.stdGaussian-based realization of a standard Gaussian vector as 08-matrix-deviation). The stable dimension $d(T)$ is formalized directly as $w(T)^2/ \mathrm{diam}(T)^2$ rather than via the book's literal (but only asymptotically equivalent, per Exercise 7.6.1) definition through a squared Gaussian width $h(T-T)^2$ — the goal theorem's own proof uses only the inequality direction of that equivalence, and the goal's hypothesis already carries an unpinned absolute constant that absorbs the equivalence constant, so this substitution preserves the theorem's exact truth content (see StableDimension's own doc-comment and MODERATION_NOTES.md for the full argument) rather than approximating it.

Ball-center deviation, disclosed. The book's printed theorem statement carries no hypothesis that $T$ contains the origin; its proof opens by translating $T$ so that it does ("Translating $T$ if necessary, we can assume that $T$ contains the origin"), and Remark 11.3.4 then confirms the ball is centered at the origin in that case. This mission states the WLOG-reduced case directly — adding $0\in T$ as an explicit hypothesis — rather than also formalizing the translation argument that recovers the fully general (untranslated) statement. This is disclosed as a genuine narrowing of the literal printed statement, though not of what the book's own proof actually establishes.

This mission covers Theorem 11.3.3 only, with no milestones: BRIEF.md explicitly instructs that if the chapter's full proof chain (general matrix deviation inequality, Chevet's inequality, random projections of sets — Theorems 11.1.5, 11.2.4, 11.3.1) proves too heavy for the session, milestones should be cut rather than the goal substituted. All three are left out, not approximated, given this chapter's five from-scratch definitions already needed for the goal's own statement. ExpSup, GaussianWidth, StableDimension and IsGaussianMatrix are reusable by any later development needing Gaussian width, the stable dimension, or a Gaussian random matrix. Solvers' contributions are welcome on the goal theorem itself and, beyond this mission's current scope, on the three named milestones.

Selected references

• A. Dvoretzky, Some results on convex bodies and Banach spaces, Proc. Internat. Sympos. Linear Spaces (Jerusalem, 1960), 123–160.
• V. D. Milman, A new proof of A. Dvoretzky's theorem on cross-sections of convex bodies, Funkcional. Anal. i Priložen. 5 (1971), 28–37.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 11. https://doi.org/10.1017/9781108231596