Probability

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.

Motivation

Two-stage stochastic linear programming with recourse models a decision made before uncertainty resolves (the first-stage variables $x$) followed by a corrective decision made after (the second-stage, or recourse, variables $y$). Solving such a program means minimizing $c^{\mathsf T}x + Q(x)$, where $Q(x)$ is the expected cost of the best recourse action given $x$ -- an object defined only implicitly, as the value of an embedded linear program that must be solved (or bounded) for every realization of the uncertain data. Before any algorithm for this problem can be justified -- the L-shaped method, stochastic decomposition, scenario decomposition, all developed in later chapters of Birge & Louveaux, Introduction to Stochastic Programming (Springer, 2011) -- one needs to know that $Q$ is well-behaved enough to optimize over at all: that the feasible region is closed and convex, that $Q$ itself is a finite, Lipschitz, convex function on it, that an optimal solution is actually attained rather than only approached in the limit, and finally what an optimality condition for the resulting nonsmooth convex program even looks like. This mission formalizes exactly that foundational layer, Chapter 3, Section 3.1 of the book.

Setting

Fix natural numbers $n_1, n_2, m_1, m_2$ and a finite scenario count $K$. A two-stage recourse instance consists of first-stage data $A \in \mathbb{R}^{m_1 \times n_1}$, $b \in \mathbb{R}^{m_1}$, $c \in \mathbb{R}^{n_1}$, a fixed recourse matrix $W \in \mathbb{R}^{m_2 \times n_2}$, and, for each scenario $k = 1,\dots,K$, a cost vector $q_k \in \mathbb{R}^{n_2}$, a right-hand side $h_k \in \mathbb{R}^{m_2}$, a technology matrix $T_k \in \mathbb{R}^{m_2 \times n_1}$, and a probability $p_k \ge 0$ with $\sum_k p_k = 1$ (Eq. (1.1)). The first-stage feasible region is $K_1 = \{x \mid Ax = b,\ x \ge 0\}$.

For a fixed $x$ and scenario $k$, the second-stage value is

$$Q(x,\xi_k) = \min_{y}\{q_k^{\mathsf T}y \mid Wy = h_k - T_k x,\ y \ge 0\}$$

(Eq. (1.6)), taken as an extended real: $+\infty$ if no feasible $y$ exists, $-\infty$ if the inner program is unbounded below. The expected recourse value is $Q(x) = \sum_k p_k\, Q(x,\xi_k)$ (Eq. (1.3)), combined so that $+\infty + (-\infty) = +\infty$ -- the book's own convention (p. 109): infeasibility in one scenario is treated as fatal even if another scenario is unboundedly favorable. The second-stage feasibility set is $K_2 = \{x \mid Q(x) < \infty\}$, and the deterministic-equivalent objective is $z(x) = c^{\mathsf T}x + Q(x)$ (Eq. (1.2)). For $x$ with $Q(x)$ finite, the subdifferential $\partial Q(x)$ is the set of $\eta$ satisfying $Q(x) + \eta^{\mathsf T}(y-x) \le Q(y)$ for every $y$ (p. 115).

A simple-recourse instance is the special case $W = [I,-I]$: the recourse cost splits as $q = (q^+,q^-)$, and $Q(x)$ decomposes componentwise via the closed form of Eq. (1.9)-(1.10) using the (left- and right-limit) distribution functions $F_i^-, F_i^+$ of each $h_i$.

Formalization targets

Goal -- Chapter 3, Theorem 9 (p. 116)

$$x^* \in K_1 \text{ is optimal in (1.2)} \iff \exists\, \lambda^* \in \mathbb{R}^{m_1},\ \mu^* \in \mathbb{R}^{n_1}_{\ge 0},\ (\mu^*)^{\mathsf T}x^* = 0,\ \text{ s.t. } -c + A^{\mathsf T}\lambda^* + \mu^* \in \partial Q(x^*),$$

given that (1.2) has a finite optimal value. This is the KKT-style necessary and sufficient optimality condition for the two-stage recourse LP, and the weakest of the mission's targets in the sense that everything else supports it: convexity and finiteness of $Q$ (Theorem 6) are what make the left-to-right implication meaningful, closedness/convexity of $K_2$ (Theorem 5) makes the feasible region well-posed, and attainment (Theorem 8) is what makes "$x^*$ is optimal" a statement about a point that exists rather than an infimum that may not be reached.

Supporting milestones

• Theorem 5(a) (p. 111): $K_2$ is closed and convex.
• Theorem 6(a) (p. 112): $Q$ is finite on $K_2$, and Lipschitzian and convex there.
• Theorem 8 (p. 115): under boundedness of $K_1 \cap K_2$ or eventual linearity of $Q$ along recession directions, a finite optimal value is attained.
• Corollary 10 (p. 116): Theorem 9 specialized to simple recourse, with $\partial Q(x^*)$ replaced by its explicit componentwise description.

Significance

Theorem 9 is the hinge on which the rest of the book's algorithmic chapters turn. The L-shaped method (Chapter 5) is a cutting-plane scheme whose cuts are literally elements of $\partial Q(x)$; stochastic decomposition and sampling-based methods use the same subdifferential structure with estimated cuts; the differentiable specialization (Eq. (1.14), $c + \nabla Q(x^*) = A^{\mathsf T}\lambda^* + \mu^*$) underlies nonlinear-programming approaches to the smooth case. None of this is meaningful without first knowing $Q$ is convex, finite where it needs to be, and that a minimizer exists to characterize. Formalizing this mission's four milestones from the actual definition of $Q$ as an embedded linear program's value -- rather than assuming these properties -- is exactly the content the book itself proves (or, for Theorem 6, explicitly cites to Wets [1972] and Kall [1976] rather than proving); this mission asks for genuine Lean proofs of Theorems 5, 8, 9 and Corollary 10 from the LP structure of $Q$, and records Theorem 6 as a stated (not re-derived) input, matching the book's own presentation.

Difficulty

The obvious shortcut is to treat $Q$ as an opaque convex function and apply a textbook convex-KKT theorem off the shelf. This fails to capture what Theorem 9 actually is: a statement about the specific function $Q(x) = \sum_k p_k \min_y\{q_k^{\mathsf T}y \mid Wy = h_k - T_k x,\ y \ge 0\}$, built from finitely many parametric linear programs, each of which can be infeasible ($Q(x,\xi_k) = +\infty$) or unbounded ($Q(x,\xi_k) = -\infty$) depending on $x$. Convexity of $Q$ must come from convexity of the value function of a parametric LP in its right-hand side (the book's Theorem 2 argument: a convex combination of optimal solutions at two right-hand sides is feasible, hence suboptimal, at the combined right-hand side) -- not from an assumed hypothesis. Handling $\pm\infty$ correctly is a second, easy-to-miss source of error: the book fixes an explicit, non-default convention ($+\infty$ dominates $-\infty$) for combining per-scenario values, the opposite of the convention Mathlib's own extended-real arithmetic uses, so any formalization that reaches for EReal's built-in addition to aggregate $Q$ silently states a different theorem. Theorem 8's attainment condition is a genuine existence result, not an automatic consequence of convexity: continuity alone does not give attainment on an unbounded feasible region, and the book's own counterexample (Eq. (1.11), a negative-exponential tail with infimum $0$ attained by no finite $x$) shows the boundedness/recession hypotheses are load-bearing.

Formalization scope

The scenario set is modeled as Fin K, a finite discrete random variable, matching Section 3.1b's development; under this model "$\xi$ has finite second moments" (the standing hypothesis of Theorems 4-11 in the general, possibly-continuous case) holds automatically and so does not appear as a separate hypothesis anywhere in this mission. Q(x,\xi_k) is defined as an EReal via sInf of the second-stage LP's feasible objective values -- sInf of the empty set is ⊤, and of a set unbounded below is ⊥ -- and is genuinely derived from that inner minimization rather than assumed convex; this rules out the chapter's trivializing formalization, which the paper-level triage explicitly warns against: taking Q(x) as an opaque convex-function hypothesis instead of deriving its properties from the inner LP's structure. Aggregating the $K$ per-scenario values into $Q(x)$ uses a bespoke bookAdd operation implementing the book's stated convention $+\infty+(-\infty)=+\infty$, since Mathlib's EReal addition is defined with the opposite convention ($\bot+\top=\top+\bot=\bot$). $\partial Q(x)$ is the ordinary subgradient-inequality set for this extended-real-valued function.

Theorem 8's condition (b) is stated with the book's own quantifier structure: the threshold $\bar\lambda$ and the recession value depend on the point $x$ and direction $v$ exactly as written, with no strengthening. Theorem 6(a)'s Lipschitz bound is stated, not derived -- the book itself cites it to Wets [1972] and Kall [1976] without proof -- so a faithful Lean proof of that milestone is expected to remain out of scope for this mission. Corollary 10 similarly takes the closed form of $\partial Q_i(x)$ from Eq. (1.10) as a hypothesis on an abstract $Q$, matching how the book itself uses (1.10) as an already-established fact rather than re-deriving it from the second-stage LP in the corollary's own proof. Theorem 11's subdifferential-decomposition result ($\partial Q(x) = E_\omega[\partial Q(x,\xi(\omega))] + N(K_2,x)$) is deliberately left out of this mission's scope: it is not needed by Theorem 9's own proof, and its normal-cone term would require relatively-complete-recourse machinery this mission does not otherwise need. No prior-art match was found on the platform: VectorSpaceOpt.fenchel_duality and the Luenberger-derived VectorSpaceOpt.generalized_kuhn_tucker / kkt_complementary_slackness family use a differentiable (Gateaux-derivative) or conjugate-function KKT model over general normed spaces, not this chapter's finite-dimensional, possibly-nondifferentiable subgradient formulation over the specific polyhedral set $K_1$, so none is a faithful match and all items here are original drafts.

Selected references

• J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• R.J-B. Wets, "Programming Under Uncertainty: The Equivalent Convex Program," SIAM Journal on Applied Mathematics 14 (1966), 89-105 (Lipschitz continuity of the recourse function, cited by the book as Wets [1972] for the closely related result used in Theorem 6). https://doi.org/10.1137/0114008
• D.P. Walkup and R.J-B. Wets, "Stochastic Programs with Recourse," SIAM Journal on Applied Mathematics 15 (1967), 1299-1314 (finiteness of the recourse function and coincidence of the possibility and expectation feasibility sets, underlying Proposition 3 and Theorem 4). https://doi.org/10.1137/0115113

Motivation

The whole series so far lived in discrete time on finite state spaces. Chapters 20–21 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) lift both restrictions. Running the jumps of a chain at the arrivals of a rate-one Poisson clock produces the continuous-time chain, whose transition semigroup — the heat kernel — converges to stationarity for every irreducible chain, with no aperiodicity hypothesis: continuous time washes out periodicity. On countable state spaces, existence of a stationary distribution is no longer automatic, and the trichotomy of transience, null recurrence, and positive recurrence replaces it; the convergence theorem survives exactly on the positive-recurrent class. The chapter's crown jewel — and this mission's goal — is Pólya's theorem: simple random walk on the lattice $\mathbb Z^d$ is recurrent in dimensions one and two and transient in dimension three and higher. "A drunk man will find his way home, but a drunk bird may get lost forever."

Setting

Continuous time (Ch. 20). For a finite chain $P$, the heat kernel at time $t\ge0$ is defined by Poissonization,

$$H_t(x,y)=\sum_{k=0}^{\infty}e^{-t}\frac{t^k}{k!}\,P^k(x,y),$$

the law at time $t$ of a walk taking $P$-steps at Poisson arrival times ($=e^{t(P-I)}$ as a matrix exponential). With $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$, the continuous distance and mixing time are $d^{\mathrm{cont}}(t)=\max_x\|H_t(x,\cdot)-\pi\|_{TV}$ and $t^{\mathrm{cont}}_{\mathrm{mix}}(\varepsilon)=\inf\{t\ge0:d^{\mathrm{cont}}(t)\le\varepsilon\}$. The lazy version of a discrete chain is $\tfrac12(I+P)$; from Mission VII, the spectral gap $\gamma$ is $1-\lambda_2$ with $\lambda_2$ the largest eigenvalue $\ne1$. The product chain on a product of $n$ coordinate spaces picks a uniform coordinate and updates it by that coordinate's chain.

Countable state spaces (Ch. 21). A chain on a countable state space $V$ is a function $P$ with nonnegative entries and rows summing to one (as convergent series); $t$-step probabilities $P^t(x,y)$ are defined recursively, and trajectory probabilities are countable sums of path weights. The first return time to $x$ is $\tau_x^+=\min\{t\ge1:X_t=x\}$; a state is recurrent when $\mathbb P_x\{\tau_x^+<\infty\}=1$ (tails tend to zero), positive recurrent when moreover $\mathbb E_x(\tau_x^+)<\infty$ (tails summable), and null recurrent when recurrent but not positive recurrent. A stationary distribution is a nonnegative $\pi$ summing to one with $\pi P=\pi$ (as convergent series). Simple random walk on $\mathbb Z^d$ steps from $x$ to one of its $2d$ nearest neighbours uniformly at random.

Formalization targets

Goal

Pólya's theorem (§21.2, Examples 21.8–21.9), the capstone of Chapters 20–21:

1. for $d\le2$, simple random walk on $\mathbb Z^d$ is recurrent — it returns to its starting point with probability one;
2. for $d\ge3$, it is transient — with positive probability it never returns.

Milestones

• Theorem 20.1 — for any irreducible finite chain, aperiodic or not, the heat kernel converges: $d^{\mathrm{cont}}(t)\to0$ as $t\to\infty$.
• Theorem 20.3 — the two-way comparison between lazy discrete and continuous mixing: eventual $\varepsilon$-mixing of the lazy chain at time $k$ gives $2\varepsilon$-mixing of the heat kernel at time $k$, and $\varepsilon$-mixing of the heat kernel at time $m$ gives $2\varepsilon$-mixing of the lazy chain at time $4m$.
• Theorem 20.6 — the spectral bound for reversible chains: $\bigl|H_t(x,y)-\pi(y)\bigr|\le\sqrt{\pi(y)/\pi(x)}\;e^{-\gamma t}$.
• Theorem 20.7 — mixing of continuous-time product chains: with all coordinate gaps $\ge\gamma$ and coordinate stationary masses bounded below, $t^{\mathrm{cont}}_{\mathrm{mix}}(\varepsilon)\le(2\gamma)^{-1}n\log n+\gamma^{-1}n\log(1/(c_0\varepsilon))$, with a matching $\tfrac{n}{2\gamma}\log n$ lower bound when the gaps are equal — the $n\log n$ product-chain phenomenon.
• Proposition 21.3 — the recurrence dichotomy on countable spaces: a state is recurrent exactly when its Green's function $\sum_tP^t(x,x)$ diverges, and for an irreducible chain one recurrent state makes all states recurrent.
• Theorem 21.12 — an irreducible countable chain is positive recurrent if and only if it has a stationary distribution.
• Lemma 21.13 (Kac) — for an irreducible chain with stationary distribution $\pi$ and any nonempty set $S$: $\sum_{x\in S}\pi(x)\,\mathbb E_x(\tau_S^+)=1$; in particular $\mathbb E_x(\tau_x^+)=1/\pi(x)$.
• Theorem 21.14 — the convergence theorem on countable spaces: an irreducible, aperiodic, positive recurrent chain has a unique stationary distribution $\pi$, and $\|P^t(x,\cdot)-\pi\|_{TV}\to0$ from every start.
• Theorem 21.17 — in the null recurrent case, $P^t(x,y)\to0$ for all pairs of states: no stationary profile is approached.

Significance

The results. Theorem 20.1 explains why laziness and aperiodicity pervade the discrete theory — periodicity is an artifact of the discrete clock. The product-chain theorem 20.7 is the cleanest instance of the $n\log n$ paradigm (independent coordinates mix in relaxation time $\times\log(\text{number of coordinates})$) and the template for the hypercube cutoff of Mission XI. Chapter 21's trichotomy is the backbone of applied Markov chain theory — queueing, branching, renewal — and Kac's lemma with the convergence theorem 21.14 is the standard equipment of any probability course. Pólya's theorem is one of the most celebrated results of twentieth-century probability, the birth of the random-walk-in-dimension-$d$ paradigm.

Formalizing them. Mathlib has no continuous-time Markov chains, no Poissonization, and no recurrence/transience theory (its PMF random walks stop far short). The countable-state layer built here — summable stationary equations, tail-sum return times, the recurrence dichotomy — is the missing infrastructure for formalized applied probability; Pólya's theorem is a famous target in its own right, and the $d\ge3$ half has never been formalized in any assistant to our knowledge.

Difficulty

The heat kernel is an infinite series of matrices: convergence (dominated by the Poisson weights), the semigroup property, and the interchange of the series with matrix products and limits must all be established by hand over tsum. Theorem 20.1 avoids aperiodicity by the number-theoretic fact that the Poisson distribution smears over residue classes — formally, the continuous chain is automatically aperiodic because $H_t(x,x)>0$ for $t>0$. The product-chain bounds need the $\ell^2$ machinery of Mission VII applied coordinatewise and a careful union bound; the lower bound is a Gaussian-free second-moment argument. On the countable side, everything is series bookkeeping in the absence of Fintype: the recurrence dichotomy is a generating-function (renewal) identity $G(x,x)=1/\mathbb P_x\{\tau_x^+=\infty\}$ handled through partial sums; Kac's lemma is a mass-transport double-count over trajectories; and Theorem 21.14 needs an aperiodicity-based coupling on a countable product space, the technical summit of the mission. Pólya's theorem itself combines a local central-limit-type estimate for the return probabilities ($P^{2t}(0,0)\asymp t^{-d/2}$, obtained by Stirling in $d=1,2$ and by a comparison argument in higher dimension) with the dichotomy of Proposition 21.3.

Formalization scope

Chapter 20 lives on finite state spaces: the heat kernel is a tsum over $k$ of Poisson weights times matrix powers (summability is provable, not assumed), continuous distance is a supremum over states, and the continuous mixing time is an sInf over nonnegative reals (junk $0$ if the set were empty — excluded under the theorems' hypotheses). Discrete-vs-continuous comparison (Theorem 20.3) is stated with eventual thresholds ($\exists K,\forall k\ge K$), matching the book's asymptotic phrasing. Chapter 21 lives on a Countable type: stochasticity and stationarity are HasSum statements, $t$-step powers are defined recursively with tsum convolutions, return-time tails are countable sums of path weights over finite horizons, and recurrence/positive recurrence are the tail-limit and tail-summability conditions above — measure theory never enters. Pólya's theorem is stated for the origin of $\mathbb Z^d$ with the walk defined by nearest-neighbour steps; the $d\le2$ and $d\ge3$ halves are separate conjuncts of one statement.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• G. Pólya, Über eine Aufgabe der Wahrscheinlichkeitsrechnung betreffend die Irrfahrt im Straßennetz, Math. Ann. 84 (1921). https://doi.org/10.1007/BF01458701
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968.
• D. Aldous, J. A. Fill, Reversible Markov Chains and Random Walks on Graphs, 2002. https://www.stat.berkeley.edu/~aldous/RWG/book.html

Motivation

How fast does a Markov chain forget its starting point? For a reversible chain the complete answer is coded in the eigenvalues of its transition matrix: the largest eigenvalue is always $1$, and the size of the gap between $1$ and the rest of the spectrum is the chain's fundamental time constant — a large gap means fast mixing, a small gap means slow mixing. Chapters 12–13 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop this spectral theory and culminate in the discrete Cheeger inequality of Jerrum–Sinclair and Lawler–Sokal, which says that the spectral gap $\gamma$ (an analytic quantity, defined below) and the bottleneck constant $\Phi_\star$ (a geometric quantity from Mission IV, also recalled below) control each other:

$$\frac{\Phi_\star^2}{2}\;\le\;\gamma\;\le\;2\,\Phi_\star.$$

A chain mixes rapidly exactly when its state space has no bottleneck. This inequality is the backbone of the Markov-chain approach to approximate counting and of spectral graph theory at large; alongside it the chapters provide Wilson's method — the sharpest general technique for mixing-time lower bounds — and the comparison machinery that transfers spectral estimates between chains.

Setting

All chains live on a finite state space $V$. A chain with transition matrix $P$ and stationary distribution $\pi$ is reversible when the detailed balance equations $\pi(x)P(x,y)=\pi(y)P(y,x)$ hold; reversibility is the standing assumption of both chapters. The yardsticks of the series are the total variation distance $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$, the worst-case distance to stationarity $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$, and the mixing time $t_{\mathrm{mix}}(\varepsilon)=\min\{t: d(t)\le\varepsilon\}$, with $t_{\mathrm{mix}}=t_{\mathrm{mix}}(1/4)$; we write $\pi_{\min}=\min_x\pi(x)$.

The spectral vocabulary: an eigenfunction of $P$ is a nonzero $f:V\to\mathbb R$ with $Pf=\lambda f$, where $(Pf)(x)=\sum_yP(x,y)f(y)$; the number $\lambda$ is then an eigenvalue. Out of the spectrum one forms

• $\lambda_2$, the largest eigenvalue different from $1$, and the spectral gap $\gamma=1-\lambda_2$;
• $\lambda_\star$, the largest absolute value of an eigenvalue different from $1$, the absolute gap $\gamma_\star=1-\lambda_\star$, and the relaxation time $t_{\mathrm{rel}}=1/\gamma_\star$.

Functions on $V$ carry the weighted inner product $\langle f,g\rangle_\pi=\sum_xf(x)g(x)\pi(x)$ — the geometry, denoted $\ell^2(\pi)$, in which a reversible $P$ is self-adjoint — and the Dirichlet form

$$\mathcal E(f)=\tfrac12\sum_{x,y}\bigl[f(x)-f(y)\bigr]^2\,\pi(x)P(x,y),$$

the average squared variation of $f$ along the chain's transitions. Finally, from Mission IV: the bottleneck ratio of a set $S$ of states is $\Phi(S)=\sum_{x\in S,\,y\notin S}\pi(x)P(x,y)\,/\,\pi(S)$, the conditional probability at stationarity of escaping $S$ in one step, and the bottleneck constant is $\Phi_\star=\min\{\Phi(S):\varnothing\ne S,\ \pi(S)\le\tfrac12\}$.

Formalization targets

Goal

Theorem 13.14, the discrete Cheeger inequality: for a reversible irreducible chain,

$$\frac{\Phi_\star^2}{2}\;\le\;\gamma\;\le\;2\,\Phi_\star.$$

Milestones

• Lemma 12.1 — every eigenvalue satisfies $|\lambda|\le1$; for an irreducible chain the eigenfunctions of the eigenvalue $1$ are the constant functions; an irreducible aperiodic chain does not have $-1$ as an eigenvalue.
• Lemma 12.2 — the spectral representation: a reversible chain admits eigenfunctions $f_1,\dots,f_{|V|}$, orthonormal with respect to $\langle\cdot,\cdot\rangle_\pi$, with eigenvalues $\lambda_j$, such that $P^t(x,y)/\pi(y)=\sum_jf_j(x)f_j(y)\lambda_j^t$ for all $t,x,y$.
• Theorem 12.3 — mixing is at most relaxation times a log factor: $t_{\mathrm{mix}}(\varepsilon)\le\log\bigl(1/(\varepsilon\,\pi_{\min})\bigr)\,t_{\mathrm{rel}}+1$.
• Theorem 12.4 — mixing is at least the relaxation time: $t_{\mathrm{mix}}(\varepsilon)\ge(t_{\mathrm{rel}}-1)\log\bigl(1/(2\varepsilon)\bigr)$.
• §12.3.1 — the model computation: simple random walk on the $n$-cycle has the numbers $\cos(2\pi j/n)$, $j=0,\dots,n-1$, among its eigenvalues.
• Theorem 13.1 — if every pair of states admits a coupling of the two one-step distributions that contracts some metric $\rho$ on $V$ by a factor $\theta$ in expectation, then $\lambda_\star\le\theta$.
• Theorem 13.5, Wilson's method — an eigenfunction $\Phi$ with eigenvalue $\lambda\in(\tfrac12,1)$ whose one-step increments have second moment at most $R$ yields the explicit lower bound $t_{\mathrm{mix}}(\varepsilon)\ge\bigl[2\log(1/\lambda)\bigr]^{-1}\bigl[\log\bigl((1-\lambda)\Phi(x)^2/(2R)\bigr)+\log\bigl((1-\varepsilon)/\varepsilon\bigr)\bigr]$.
• Lemmas 13.11–13.12 — the variational characterization: $\gamma$ is the minimum of $\mathcal E(f)$ over functions with mean zero ($\sum_xf(x)\pi(x)=0$) and unit norm ($\langle f,f\rangle_\pi=1$), and the minimum is attained.
• Lemma 13.22 — the comparison method: if a second reversible chain $\tilde P$ on the same space, with stationary distribution $\tilde\pi$, Dirichlet form $\tilde{\mathcal E}$, and gap $\tilde\gamma$, satisfies $\tilde{\mathcal E}(f)\le B\,\mathcal E(f)$ for every $f$, then $\tilde\gamma\le\bigl[\max_x\pi(x)/\tilde\pi(x)\bigr]B\,\gamma$.

Significance

The results. Theorems 12.3–12.4 sandwich the mixing time between $t_{\mathrm{rel}}$ and $t_{\mathrm{rel}}\log(1/\pi_{\min})$ — the fundamental equivalence of spectral and mixing estimates for reversible chains, prerequisite for the cutoff criterion of Mission XI. The Cheeger inequality converts isoperimetry into spectral bounds; it is the mathematical core of the Jerrum–Sinclair program of polynomial-time approximate counting, and its graph version underlies expander theory. Wilson's method produced the sharp lower bounds for adjacent transpositions and hypercube-type chains; the comparison lemma is the engine behind the shuffle bounds cited in Mission V (§16.1).

Formalizing them. Mathlib has the spectral theorem for symmetric matrices but nothing connecting spectra to Markov chains: no spectral gap, no relaxation time, no Dirichlet forms, no Cheeger inequality in any form. A formalized discrete Cheeger inequality would be a landmark reusable well outside this series (spectral graph theory, expanders); the eigenvalue and Rayleigh-quotient layer built here is what Missions IX (tree relaxation, block dynamics) and XI (cutoff criterion) consume.

Difficulty

Everything routes through one change of basis: conjugating $P$ by the diagonal matrix with entries $\sqrt{\pi(x)}$ produces a matrix that is symmetric precisely because the chain is reversible, so Mathlib's spectral theorem applies — but transporting the resulting eigenbasis back to $\ell^2(\pi)$, keeping track of orthonormality with respect to the weighted inner product, is a genuine formal-linear-algebra project; nothing about it is deep, all of it is fussy. The definitions of $\lambda_2$ and $\lambda_\star$ as suprema over the set of non-unit eigenvalues (finite, and nonempty once $|V|\ge2$) must be reconciled with the eigenbasis enumeration before any variational argument runs. The upper half of Cheeger is direct from the variational characterization — test it on the indicator function of a bottleneck set $S$, recentred to have mean zero; the lower half is the hard half: the standard proof takes an optimal $f$, decomposes it over its level sets $\{f>c\}$, and applies Cauchy–Schwarz twice, and formalizing that level-set sweep is the main effort of the mission. Wilson's method needs a supermartingale-style iteration of the eigenfunction estimate; its constants are exact, so the inequalities cannot be rounded.

Formalization scope

Eigenvalues are defined by real eigenvectors ($\exists f\ne0,\ Pf=\lambda f$); for reversible chains this captures the whole spectrum, and all statements assume reversibility wherever the book does. $\lambda_2$ and $\lambda_\star$ are suprema of explicit sets of reals; on a one-point space these sets are empty and the supremum takes a junk value, so the affected statements carry the explicit hypothesis $|V|\ge2$, matching the book's implicit assumption of a non-degenerate chain. $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$ with total inverse. Theorem 12.3 carries an explicit $+1$ absorbing the rounding of a real-valued bound to an integer time. The cycle eigenvalue statement exhibits eigenvalues (existence of eigenfunctions); completeness of that list is not asserted. The variational characterization asserts both the minimization identity and its attainment, so it can be used in either direction.

Welcome contributions: the symmetrization API (conjugation by $\mathrm{diag}(\sqrt{\pi})$), Rayleigh-quotient lemmas, level-set (layer-cake) infrastructure — all reused by Missions IX and XI.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• M. Jerrum, A. Sinclair, Approximating the permanent, SIAM J. Comput. 18 (1989). https://doi.org/10.1137/0218077
• G. F. Lawler, A. D. Sokal, Bounds on the L² spectrum for Markov chains and Markov processes, Trans. Amer. Math. Soc. 309 (1988). https://doi.org/10.1090/S0002-9947-1988-0930082-9
• D. B. Wilson, Mixing times of lozenge tiling and card shuffling Markov chains, Ann. Appl. Probab. 14 (2004). https://doi.org/10.1214/aoap/1042765669