Probability

Machine Learning Statistics·Captain: mikedeng1

High-Dimensional Statistics VI: The Lasso's l2-Error Bound under Restricted EigenvalueTextbook

Motivation

Modern regression problems routinely have far more candidate predictors than observations: genomics with tens of thousands of genes and a few hundred patients, signal recovery from far fewer measurements than the signal's ambient dimension, image reconstruction from an undersampled set of linear projections. In every such setting the classical least-squares estimator is either undetermined or hopelessly noisy, and the ordinary theory of linear regression, built for $n \gg d$ , has nothing to say.

The Lasso — $\ell_1$ -penalized least squares, introduced by Tibshirani (1996) — is the workhorse response: penalize the least-squares objective by the $\ell_1$ -norm of the coefficient vector, which both drives many coordinates exactly to zero and remains a convex, tractable program. What is far from obvious a priori is that this convex relaxation is not just computationally convenient but statistically correct: under a condition on the design matrix, its estimation error is controlled at a rate matching what one could hope for even knowing the true support in advance. Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 7, gives the deterministic backbone of this guarantee — the part of the argument that holds for any noise vector and any design matrix satisfying a single geometric condition, before any probability is introduced.

Setting

Consider the linear model $y = X\theta^* + w$ , where $X \in \mathbb R^{n\times d}$ is a known design matrix, $\theta^* \in \mathbb R^d$ is an unknown coefficient vector, and $w \in \mathbb R^n$ is a noise vector, observed together with the response $y \in \mathbb R^n$ . Write $\|\theta\|_1 := \sum_{j=1}^d|\theta_j|$ and $\|v\|_\infty := \max_j |v_j|$ . The Lagrangian Lasso is the convex program

\hat\theta \in \operatorname*{arg\,min}_{\theta \in \mathbb R^d} \left\{ \frac{1}{2n}\|y - X\theta\|_2^2 + \lambda_n \|\theta\|_1 \right\},

with regularization parameter $\lambda_n > 0$ chosen by the user.

Say $\theta^*$ is supported on $S \subseteq \{1,\dots,d\}$ if $\theta^*_j = 0$ for every $j \notin S$ , and write $|S| = s$ for its sparsity. For a subset $S$ and a constant $\alpha \ge 1$ , the cone

C_\alpha(S) := \{\Delta \in \mathbb R^d \mid \|\Delta_{S^c}\|_1 \le \alpha \|\Delta_S\|_1\}

collects the directions in which an estimation error concentrated near the true support can plausibly point. The matrix $X$ satisfies the restricted eigenvalue (RE) condition over $S$ with parameters $(\kappa,\alpha)$ if

\frac{1}{n}\|X\Delta\|_2^2 \ge \kappa \|\Delta\|_2^2 \qquad \text{for all } \Delta \in C_\alpha(S).

Ordinarily, when $d > n$ , the quadratic cost's Hessian $X^TX/n$ is rank-deficient and has a large flat subspace, so no uniform positive-curvature bound like this can hold over all of $\mathbb R^d$ ; the RE condition asks for curvature only along the cone $C_\alpha(S)$ that the Lasso's own optimality actually forces its error into.

The companion notion — the restricted nullspace property, $C_1(S) \cap \mathrm{null}(X) = \{0\}$ — is the noiseless analogue: it is exactly the condition under which the $\ell_1$ -relaxed basis pursuit program $\min_\theta \|\theta\|_1$ s.t. $X\theta = y$ exactly recovers every $S$ -sparse $\theta^*$ from $y = X\theta^*$ (Theorem 7.8). A small pairwise incoherence $\delta_{PW}(X) := \max_{j,k} |\langle X_j,X_k\rangle/n - \mathbb 1[j=k]|$ is one simply-checked sufficient condition for it (Proposition 7.9).

Formalization targets

Goal (Theorem 7.13(a) and its final sentence)

Under (A1) $\theta^*$ supported on $S$ , $|S|=s$ , and (A2) $X$ satisfies the RE condition over $S$ with parameters $(\kappa,3)$ : for any $\hat\theta$ solving the Lagrangian Lasso with $\lambda_n \ge 2\|X^Tw/n\|_\infty$ ,

\|\hat\theta - \theta^*\|_2 \le \frac{3}{\kappa}\sqrt{s}\,\lambda_n, \qquad \|\hat\theta - \theta^*\|_1 \le 4\sqrt{s}\,\|\hat\theta-\theta^*\|_2.

Milestones

Theorem 7.8. The restricted nullspace property is equivalent to exact recovery by basis pursuit for every $S$ -sparse vector.
Proposition 7.9. $\delta_{PW}(X) \le 1/(3s)$ implies the restricted nullspace property for every $S$ with $|S|\le s$ .

Significance

The bound is the deterministic core underneath every high-dimensional consistency guarantee for the Lasso: once a statistician checks that a particular random design (Gaussian, sub-Gaussian, or otherwise) satisfies the RE condition with high probability, and bounds $\|X^Tw/n\|_\infty$ using concentration of the noise, this one inequality converts directly into a rate — Wainwright's own Examples 7.14–7.15 do exactly this for the classical Gaussian linear model and for compressed sensing. It also isolates why the Lasso is competitive with an oracle that already knows the support: the rate $\sqrt{s/n}$ (up to log factors, once $\lambda_n$ is instantiated) is the same order one would get regressing only on the $s$ true coordinates.

The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the bound together with its two supporting structural results, in a form that composes with the rest of this book's formalized chapters and with any future formalization of the concentration arguments (Chapters 2–6) that supply $\lambda_n$ 's numerical value in specific models.

Difficulty

The proof is short but every step leans on getting the cone membership exactly right. The first hurdle is showing the error $\Delta := \hat\theta - \theta^*$ lands in $C_3(S)$ at all — this needs the Lagrangian basic inequality (from $\hat\theta$ 's optimality against $\theta^*$ ), not the simpler constrained-Lasso argument used for parts (b)/(c), and the constant $3$ (not $1$ ) comes precisely from the factor of $2$ in the $\lambda_n$ bound combined with Hölder's inequality on the noise term. A tempting shortcut is to assume the uniform curvature bound (7.24), $\|X\Delta\|_2^2/n \ge \kappa\|\Delta\|_2^2$ for all $\Delta \ne 0$ — but in the regime $d > n$ this uniform bound is never satisfiable, since $X^TX/n$ has a $(d-n)$ -dimensional null space; the entire point of the restricted eigenvalue condition is to demand curvature only on the cone the optimality argument already produces.

Formalization scope

$X$ , $\theta^*$ , $\hat\theta$ , $w$ are unconstrained vectors/matrices over Fin n/Fin d-indexed reals; $S$ is a Finset (Fin d). The RE condition's constant $\kappa$ is required positive, since the book divides by it throughout the discussion of Theorem 7.13 even though Definition 7.12 itself states the condition schematically; $\alpha=3$ is fixed to the book's own value, not a free parameter of the goal. The $\ell_\infty$ - and pairwise-incoherence suprema are real iSups over finite index types, which default to Mathlib's junk value $0$ at dimension $0$ — a degenerate corner with no vector to measure, not a trivializing case of the theorem's actual content. A trivializing formalization would drop the final-sentence $\ell_1$ -bound as "a trivial Cauchy–Schwarz corollary" or silently substitute the stronger, later-defined restricted isometry property for the restricted eigenvalue condition; this mission does neither. Parts (b) (constrained Lasso) and (c) (relaxed basis pursuit) of Theorem 7.13, and the primal–dual-witness support-recovery result (Theorem 7.21), are out of this mission's scope; a full-strength companion mission covering them, including the RIP-based Proposition 7.11 and the random-design certification Theorem 7.16, is natural future work.

Selected references

Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 7. DOI: 10.1017/9781108627771.
Tibshirani, R. "Regression shrinkage and selection via the Lasso." Journal of the Royal Statistical Society: Series B, 58(1), 1996, 267–288.
Chen, S. S., Donoho, D. L., Saunders, M. A. "Atomic decomposition by basis pursuit." SIAM Journal on Scientific Computing, 20(1), 1998, 33–61.

13 thms2 active users

Operations Research Statistics Stochastic Systems·Captain: mikedeng1

Stochastic Orders VI: The Multivariate Stochastic OrderTextbook

From "larger" to "larger in every direction"

Chapter I's usual stochastic order compares two real-valued random variables by "how large" they tend to be. Chapter VI lifts the same idea to random vectors: $X$ is smaller than $Y$ in the usual multivariate stochastic order if $X$ is less likely than $Y$ to land in any upper set of $\mathbb{R}^n$ — any region defined by "at least this large in every coordinate." This mission formalizes that order and its two founding characterizations: a coupling theorem (the direct $n$ -dimensional generalization of Chapter I's own coupling theorem) and a common-source representation, plus two closure properties that make the order usable in practice.

The usual multivariate stochastic order

Let $X$ be a random vector taking values in $\mathbb{R}^n$ on a probability space $(\Omega,\mu)$ , and let $Y$ be a random vector taking values in $\mathbb{R}^n$ on a (possibly different) probability space $(\Omega',\nu)$ . $X$ is smaller than $Y$ in the usual multivariate stochastic order, written $X \le_{st} Y$ , if

P\{X\in U\} \le P\{Y\in U\} \quad \text{for every upper set } U\subseteq\mathbb{R}^n,

where an upper set is one closed upward under the coordinatewise partial order on $\mathbb{R}^n$ ( $x\le y$ iff $x_i\le y_i$ for every $i$ ). Equivalently, $X\le_{st}Y$ iff $E[\varphi(X)]\le E[\varphi(Y)]$ for every increasing $\varphi:\mathbb{R}^n\to\mathbb{R}$ (increasing with respect to that same coordinatewise order) for which the two expectations exist — the form this mission drafts as the definition, exactly parallel to the univariate order's own equivalent form.

Formalization targets

Goal: the coupling characterization (Theorem 6.B.1)

X \le_{st} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}^n\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ P\{\hat X\le\hat Y\}=1.

This is the direct $n$ -dimensional generalization of Chunk 01's Theorem 1.A.1: a joint law on the random vectors' shared space realizing $X\le_{st}Y$ as an almost-sure coordinatewise inequality between copies. The book does not give this direction's proof here (an explicit construction appears later, in a special case irrelevant to a statements-only mission), and the claim is exactly as citable either way.

Supporting milestones

Theorem 6.B.2, the common-source restatement: $X\le_{st}Y$ iff there is a real-valued random variable $Z$ and $\mathbb{R}^n$ -valued functions $\psi_1\le\psi_2$ (coordinatewise, at every $z\in\mathbb{R}$ ) with $X=_{st}\psi_1(Z)$ , $Y=_{st}\psi_2(Z)$ — the multivariate analogue of Theorem 1.A.2, an immediate restatement of the goal.
Theorem 6.B.16(b), closure under conjunctions: independent $X_i\le_{st}Y_i$ ( $i=1,\dots,m$ ) give $\psi(X_1,\dots,X_m)\le_{st}\psi(Y_1,\dots,Y_m)$ for any increasing $\psi:\mathbb{R}^k\to\mathbb{R}$ — note the codomain $\mathbb{R}$ , so this closure conclusion is itself the univariate order applied to vector-valued inputs. Specializing $\psi$ to a coordinatewise sum gives closure under convolutions.
Theorem 6.B.16(c), closure under marginalization: $X\le_{st}Y$ implies $X_I\le_{st}Y_I$ for every sub-index set $I\subseteq\{1,\dots,n\}$ — a special case of part (b), included separately for its own simple, widely-used content.

Significance

The usual multivariate stochastic order is the natural tool for comparing random vectors — costs, resource-usage profiles, portfolio returns — that must be ranked simultaneously across several coordinates rather than reduced to a single scalar summary first. It underlies simulation comparisons (via the coupling and common-source characterizations, both constructive), reliability comparisons of multi-component systems (whose component lifetimes are naturally vector-valued), and comparative-statics arguments in queueing and inventory models with several state variables. The closure properties are what make the order compositional: conjunction closure says a vector-by-vector comparison of independent inputs survives any coordinatewise-increasing post-processing, and marginalization closure says a joint comparison restricts consistently to any sub-collection of coordinates — together they are the two properties an analyst reaches for first when reducing a multivariate comparison to a more tractable one.

No platform prior art exists: GET /theorems?q=stochastic+order and q=coupling return zero genuine hits (checked at this book's triage time, re-confirmed this session). This mission restates the usual multivariate stochastic order and its two founding theorems as a self-contained foundation, in the same spirit as Chunk 01's univariate mission but independently drafted, since drafts cannot import each other's Lean.

Difficulty

The chief formalization risk this chapter's own brief flags is conflating "increasing" for $\varphi:\mathbb{R}^n\to\mathbb{R}$ with some order other than the coordinatewise one (a total order via a fixed embedding, or a lexicographic order): the book's order on $\mathbb{R}^n$ is always the componentwise partial order, and Mathlib gives Fin n → ℝ exactly that order by default (its Pi/product order), so Monotone φ for φ : (Fin n → ℝ) → ℝ already means what the book means with no extra predicate to get wrong — but it would be easy to instead encode ℝ^n-valued objects some other way (e.g. a fixed linear functional into ℝ) that silently swaps in a different, weaker order. The second risk is Theorem 6.B.16(b)'s literal codomain: the book states $\psi:\mathbb{R}^k\to\mathbb{R}$ (scalar), so the closure conclusion is a genuinely univariate stochastic-order statement about $\psi$ applied to vector inputs, not a vector-to-vector closure (that is part (a), not drafted here) — stating it as a multivariate conclusion by mistake would silently strengthen a theorem the book does not claim.

Formalization scope

Random vectors are drafted as functions into Fin n → ℝ from arbitrary measurable spaces, which inherit Mathlib's default coordinatewise (Pi) order — the same order the book uses throughout this chapter, requiring no separate order predicate. MultivariateOrder μ ν X Y quantifies over φ : (Fin n → ℝ) → ℝ with Monotone φ in that order and Integrable (φ ∘ X) μ/Integrable (φ ∘ Y) ν stated inside the ∀, exactly matching "for which the expectations exist." Equality in law is ProbabilityTheory.IdentDistrib. Theorem 6.B.2's random variable $Z$ is drafted as $\mathbb{R}$ -valued specifically (not an arbitrary-type common source), matching the book's own "for all $z\in\mathbb{R}$ " quantification exactly.

Theorem 6.B.16(b) is drafted for a common dimension $n$ across all $X_i,Y_i$ rather than the book's per- $i$ dimension $k_i$ : the concatenated input then lives in Fin m → Fin n → ℝ (nested Pi types, carrying the coordinatewise order on $\mathbb{R}^{mn}$ exactly as needed), avoiding a dependent-sum concatenation of vectors of genuinely different lengths that a mission of this size does not justify. This is the "closed under convolutions" special case the book itself names as a corollary of the general statement, not a different claim — but it is a genuine restriction of scope, recorded here rather than silently applied, and the general varying-dimension statement is left for a future pass (see STATUS.md). The theorem's conclusion is stated as the univariate order's own defining inequality on ℝ (∀ x, μ {ω | x < ψ(X_∙ ω)} ≤ ν {ω | x < ψ(Y_∙ ω)}), restated locally rather than importing Chunk 01's UsualOrder, since drafts cannot import another mission's definitions. Theorem 6.B.16(c)'s sub-index set $I\subseteq\{1,\dots,n\}$ of size $k$ is encoded as an injective reindexing r : Fin k → Fin n, with $X_I,Y_I$ drafted as X, Y precomposed coordinatewise with r, matching the book's own subvector notation (6.A.1) exactly.

A trivializing formalization this mission rules out: drafting MultivariateOrder with an order on Fin n → ℝ other than the coordinatewise one (for instance, a fixed linear functional collapsing the vector to a scalar and reusing the univariate order), which would silently state a different, generally weaker order under the same name; and drafting Theorem 6.B.16(b)'s conclusion with a vector-valued (rather than the book's literal scalar-valued) $\psi$ , which would silently strengthen a theorem the book states only for real-valued $\psi$ . This mission draws on no platform prior art (searches for "stochastic order" and "coupling" as of 2026-09-18 return zero genuine matches). Reusable beyond this mission: the MultivariateOrder definition pattern and its coupling/common-source characterization parallel Chunk 01's univariate pair closely enough that a future chapter needing a multivariate order's own coupling theorem (Chapter VII's multivariate convex order is the direct next instance in this series) could restate the same shape with minimal adaptation.

Selected references

M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 6 (Multivariate Stochastic Orders), §6.A–6.B. https://doi.org/10.1007/978-0-387-34675-5
This series' Chunk 01 (StochasticOrders.Usual), for the univariate usual stochastic order and its coupling/common-source characterizations this chapter directly generalizes.

8 thms2 active users

Completed

Machine Learning Statistics·Captain: mikedeng1

Support Vector Machines V: Bernstein's Inequality for Independent Hilbert-Space-Valued Random VariablesTextbook

Motivation

Every statistical guarantee for a learning algorithm ultimately rests on a concentration inequality: a bound on how far an empirical average can stray from its expectation. For real-valued averages, Bernstein's inequality (1924, refined through the 20th century) is the classical tool — sharper than Hoeffding's inequality whenever the summands' variance is small compared to their range. Modern learning theory, however, frequently needs to control averages of objects that are not real numbers but elements of a Hilbert space: feature vectors $\Phi(x_i)y_i$ , gradients of a loss, or the values a kernel machine's empirical risk functional takes. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter 6, develop exactly the vector-valued extension needed for the book's own SVM consistency proofs: Theorem 6.14, Bernstein's inequality for independent random variables taking values in a separable Hilbert space, and its corollaries.

Setting

Fix a probability space $(\Omega,\mathcal A,P)$ and a separable real Hilbert space $H$ . Random variables $\xi_1,\dots,\xi_n : \Omega \to H$ are independent if the family is mutually independent (not merely pairwise), and $\xi_i$ has essential supremum bound $B$ , $\|\xi_i\|_\infty \le B$ , if $\|\xi_i(\omega)\|_H \le B$ for $P$ -almost every $\omega$ . Writing $\mathbb E$ for $\mathbb E_P$ , the quantities of interest are the mean $\mathbb E\,\xi_i \in H$ (a Bochner integral) and the variance bound $\sigma^2$ , an upper bound on $\mathbb E\,\|\xi_i\|_H^2$ .

The classical scalar case (Theorem 6.12, itself a refinement of Hoeffding's inequality, Theorem 6.10) bounds $P\big(\frac1n\sum_i \xi_i \ge \varepsilon\big)$ for real-valued, mean-zero, range- and variance-bounded $\xi_i$ . The tool behind both the scalar and the vector-valued case is a general exponential-moment inequality (Theorem 6.13) valid for independent, integrable random variables taking values in any separable Banach space $E$ :

P\Big(\Big\|\sum_{i=1}^n \xi_i\Big\| \ge \varepsilon n\Big) \le \exp\Big(-t\varepsilon n + t\,\mathbb E\Big\|\sum_{i=1}^n \xi_i\Big\| + \sum_{i=1}^n \mathbb E\big(e^{t\|\xi_i\|}-1-t\|\xi_i\|\big)\Big), \qquad \varepsilon,t \ge 0.

Formalization targets

Goal: Theorem 6.14 (Bernstein's inequality in Hilbert spaces)

P\left(\Big\|\frac1n\sum_{i=1}^n \xi_i\Big\|_H \ge \sqrt{\frac{2\sigma^2\tau}{n}} + \sqrt{\frac{\sigma^2}{n}} + \frac{2B\tau}{3n}\right) \le e^{-\tau}, \qquad \tau>0,

for independent, mean-zero $\xi_1,\dots,\xi_n : \Omega \to H$ with $\|\xi_i\|_\infty \le B$ and $\mathbb E\|\xi_i\|_H^2 \le \sigma^2$ . This is the weakest stable form of the claim: it is stated for a general separable Hilbert space (not a fixed finite dimension), with the tail written as a sum of three explicit terms rather than folded into an unspecified constant, so it survives specialization to any concrete $H$ without modification.

Supporting facts

Theorem 6.13 (above) is the direct tool Theorem 6.14's own proof invokes ("we will prove the assertion by applying Theorem 6.13"); Theorem 6.12 is the scalar analogue Theorem 6.14 generalizes, included to make the generalization's exact form (three terms, not two) checkable against its source; Corollary 6.15, Hoeffding's inequality in Hilbert spaces, is the immediate mean-free-of-a-variance-bound consequence of Theorem 6.14 obtained by centering, reused directly in the book's own oracle-inequality proof (§6.4).

Significance

Theorem 6.14 is the concentration inequality behind the book's later empirical-process arguments for SVMs: whenever an SVM's analysis needs to bound the deviation of an empirical average of Hilbert-space-valued quantities (feature-map evaluations, loss gradients) from its mean, this is the tool invoked, via Corollary 6.15 in the book's own oracle-inequality derivation. Its distinct contribution over simply applying the scalar Theorem 6.12 coordinate-by-coordinate (which is not available without a fixed, finite orthonormal basis, and even then would produce dimension- dependent bounds) is that the bound here is entirely dimension-free: it depends on $H$ only through the variance bound $\sigma^2$ and the range bound $B$ , not through $\dim H$ .

The scalar Bernstein inequality is classical (Bernstein 1924, refined by Bennett 1962 and others to the sharper multiplicative form used here); its Banach- and Hilbert-space generalizations (via the martingale-difference / Yurinskii-type argument Theorem 6.13's proof uses) are standard in the empirical-process-theory literature by the time of this book (see, e.g., Pinelis 1994 for closely related Banach-space martingale inequalities). No machine-checked Lean proof of the Hilbert-space form is known to exist on the platform at the time of writing (the platform's own HighDimProb.Concentration.bernstein_unweighted, from the Vershynin series, is a different, sub-exponential-norm scalar statement — see Formalization scope); this mission asks for the book's own bounded-summand, explicit-constant Hilbert-space form.

Difficulty

The natural first attempt generalizes the scalar proof's Markov-inequality argument directly: bound $\mathbb E\,e^{t\|\sum_i\xi_i\|}$ using independence. This breaks immediately because $\|\cdot\|_H$ is not linear, so $e^{t\|\sum_i \xi_i\|}$ does not factor over $i$ the way $e^{t\sum_i \xi_i}$ does in the scalar case — there is no vector-valued analogue of the moment generating function that tensorizes under independence directly. Theorem 6.13's proof resolves this with a martingale-difference decomposition (writing the deviation as a telescoping sum of conditional-expectation differences $X_k$ across the filtration generated by $\xi_1,\dots,\xi_k$ ) rather than a direct product-of-moment-generating-functions argument, at the cost of needing $E$ separable (for the conditional expectations and the resulting sums to be well-defined and measurable). Deriving Theorem 6.14 from Theorem 6.13 then requires controlling the two extra terms Theorem 6.13 introduces (the mean-norm term and the per-summand correction) using only the Hilbert-space-specific facts $\mathbb E\langle\xi_i,\xi_j\rangle=0$ for $i\ne j$ (from independence and mean-zero) and the scalar bound on $\mathbb E\|\xi_i\|^2$ — which is exactly where the tail's extra $\sqrt{\sigma^2/n}$ term originates, and is not obtainable by naively reusing the scalar Theorem 6.12's two-term optimization over $t$ unchanged.

Formalization scope

$H$ (and, for Theorem 6.13, $E$ ) is an arbitrary separable real (Hilbert, resp. Banach) space — not fixed to a Euclidean space of any dimension — matching the book's own generality, which is essential since the theorem's dimension-independence is part of its content. $\|\xi_i\|_\infty \le B$ is formalized as the almost-sure bound ∀ᵐ ω ∂P, ‖ξ i ω‖ ≤ B, matching the book's $L^\infty(P)$ convention rather than requiring the bound to hold for literally every $\omega$ . Independence is the mutual independence of the whole family (Mathlib's iIndepFun), matching Theorem 6.13's proof, which uses independence of $\xi_k$ from $\sum_{i\ne k}\xi_i$ for every $k$ simultaneously, not merely pairwise independence.

A trivializing formalization would state the conclusion in terms of the scalar random variable $\|\xi_i\|_H$ rather than the vector-valued average's norm $\big\|\frac1n\sum_i \xi_i\big\|_H$ — this would collapse the theorem to an easier scalar statement about a nonnegative random variable and lose the whole point of the vector-valued generalization; it is ruled out here by writing the norm of the sum (not a sum of norms) inside the probability. Likewise, dropping the $\sqrt{\sigma^2/n}$ middle term of the tail bound (present here, absent from the scalar Theorem 6.12) would silently understate the genuine dimension-independent cost of vector-valued concentration; all three terms are kept.

Theorem 6.13's general Banach-space statement, and the scalar Theorem 6.12, are reusable beyond this mission (Theorem 6.13 is the tool any future Banach-space-valued concentration mission in this series would reach for first). The platform's existing HighDimProb.Concentration. bernstein_unweighted/hoeffding_rademacher (Vershynin series) are not reused as kind: reference items here: they use a sub-Gaussian/sub-exponential-Orlicz-norm parameterization and a universal (unspecified) constant, a genuinely different hypothesis structure from this chapter's explicit $L^\infty$ -bounded, exact-constant form — reusing them would misrepresent this chapter's own, sharper statement. Completing the four sorrys (Theorems 6.12-6.14, Corollary 6.15) is welcome; the martingale-difference argument behind Theorem 6.13 is the natural starting point, since the other three all reduce to it directly.

Selected references

I. Steinwart & A. Christmann, Support Vector Machines, Springer, Information Science and Statistics, 2008. https://doi.org/10.1007/978-0-387-77242-4 (Chapter 6, §6.2, pp. 210-217).
S. Bernstein, "On a modification of Chebyshev's inequality and of the error formula of Laplace," Ann. Sci. Inst. Sav. Ukraine, Sect. Math. 1(4), 1924 (original scalar inequality).
G. Bennett, "Probability inequalities for the sum of independent random variables," Journal of the American Statistical Association 57(297), 1962, pp. 33-45. https://doi.org/10.1080/01621459.1962.10482149
I. Pinelis, "Optimum bounds for the distributions of martingales in Banach spaces," Annals of Probability 22(4), 1994, pp. 1679-1706. https://doi.org/10.1214/aop/1176988477

5 thms2 active usersReviewed

Completed

Operations Research Statistics Stochastic Systems·Captain: mikedeng1

Stochastic Orders V: The Laplace Transform OrderTextbook

Comparing distributions by their Laplace transforms

Many of the orders in Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) are built by fixing a class of test functions $\varphi$ and declaring $X \le Y$ whenever $E[\varphi(X)] \le E[\varphi(Y)]$ for every $\varphi$ in that class: all increasing functions give the usual stochastic order, all convex functions give the convex order. This mission formalizes the order obtained from the single function $\varphi_s(x) = -e^{-sx}$ , $s > 0$ — the Laplace transform order — together with its principal alternative characterization and three of its closure properties. Unlike almost every other order in the book, this one has essentially no dependence on material from earlier chapters, which is why it is a natural standalone mission.

The Laplace transform order

Let $X$ be a real-valued random variable on a probability space $(\Omega,\mu)$ , and let $Y$ be a real-valued random variable on a (possibly different) probability space $(\Omega',\nu)$ . $X$ is smaller than $Y$ in the Laplace transform order, written $X \le_{Lt} Y$ , if

E[e^{-sX}] \ge E[e^{-sY}] \quad \text{for every } s > 0.

The order is meant for nonnegative random variables: the book's own standing convention for the whole of §5.A is that every random variable mentioned is nonnegative, since otherwise $E[e^{-sX}]$ need not even be finite. Every theorem below carries that hypothesis explicitly rather than folding it into the order's own definition, so the definition itself is stated exactly as broadly as the book's raw equation (5.A.1) is — a comparison of two expectations, for two random variables that need not share a probability space, since $\le_{Lt}$ is a comparison of distributions.

A second definition supports one of the milestones: a function $\varphi : [0,\infty) \to \mathbb{R}$ is completely monotone if all its derivatives exist and $(-1)^n\varphi^{(n)}(x) \ge 0$ for every $x > 0$ and every $n = 0, 1, 2, \dots$ . Every $\varphi_s(x) = e^{-sx}$ , $s > 0$ , is completely monotone, which is what connects the raw definition of $\le_{Lt}$ to its function-class characterization below.

Formalization targets

Goal: the integrated-survival-function characterization (Theorem 5.A.1)

X \le_{Lt} Y \iff \int_0^\infty e^{-sx}\bar F(x)\,dx \le \int_0^\infty e^{-sx}\bar G(x)\,dx \quad \text{for every } s > 0,

where $\bar F(x) = P\{X>x\}$ and $\bar G(x) = P\{Y>x\}$ are the survival functions of $X$ and $Y$ . This is the book's principal restatement of the order, obtained from the identity $\int_0^\infty e^{-sx}\bar F(x)\,dx = s^{-1}(1-E[e^{-sX}])$ : instead of comparing the raw Laplace transforms of $X$ and $Y$ themselves, it compares the Laplace transforms of their survival functions, weighted the same way. It is the natural goal for a standalone chapter mission: the chapter's own defining equation plus one elementary identity is exactly the book's own proof, and it is the form of the order that the chapter's closure properties are stated against.

Supporting milestones

Eq. (5.A.5), the mean inequality: $X \le_{Lt} Y \implies E[X] \le E[Y]$ , provided the expectations exist — obtained by dividing the defining inequality by $s$ and letting $s \downarrow 0$ .
Theorem 5.A.3, the function-class characterization: $X \le_{Lt} Y$ iff $E[\varphi(X)] \ge E[\varphi(Y)]$ for every completely monotone $\varphi$ , provided the expectations exist — the order's analogue of "all increasing functions" for $\le_{st}$ or "all convex functions" for $\le_{cx}$ .
Theorem 5.A.7(a), closure under functions with a completely monotone derivative: $X \le_{Lt} Y$ and $g$ positive with $g'$ completely monotone gives $g(X) \le_{Lt} g(Y)$ .
Theorem 5.A.7(d), the convolution corollary: independent $X_i \le_{Lt} Y_i$ , $i=1,\dots,m$ , gives $\sum_i X_i \le_{Lt} \sum_i Y_i$ .

Significance

The Laplace transform order is the natural comparison for nonnegative quantities that arise as sums or mixtures of exponential-type random variables — waiting times, workloads, service completion times — precisely because it is preserved under convolution (Theorem 5.A.7(d)) and under the broad class of transformations with a completely monotone derivative (Theorem 5.A.7(a)), which includes every concave power $x^p$ , $0<p\le 1$ . It sits strictly between the convex-type orders and weaker moment comparisons: Eq. (5.A.5) shows it implies ordered means, but (unlike $\le_{cx}$ ) it does not require equal means, and (unlike $\le_{icx}$ ) it is not implied by a pointwise comparison of integrated tails alone — it is its own, genuinely different order, useful whenever a modeler's comparison naturally arises through Laplace-transform (equivalently, moment-generating-function-at- negative-argument) calculations rather than through a coupling or a tail-probability argument. Theorem 5.A.3's function-class form is the bridge that lets the order be verified either way: by a single-parameter family of exponential test functions, or by the full class of completely monotone functions of which they are the extreme rays.

Difficulty

The chapter's own first warning applies directly: the order's every characterization requires $X,Y \ge 0$ , and dropping that hypothesis anywhere — as opposed to carrying it explicitly on each theorem, per this mission's convention — would silently change which statements are even well-posed, since $E[e^{-sX}]$ can diverge for $X$ unbounded below. The quantifier " $\forall s > 0$ " in both the raw definition and Theorem 5.A.1 ranges over the whole positive half-line, not a bounded or discretized set of test points; narrowing it would produce a strictly weaker order. In CompletelyMonotone, the phrase "all its derivatives exist" is a genuine hypothesis, not a formality: stating only the sign condition on iteratedDeriv n φ x without also requiring φ to be C^∞ would let the definition be satisfied vacuously wherever a derivative fails to exist (a classic junk-value trap), which is why the mission's definition bundles smoothness explicitly. Theorem 5.A.7(a)'s " $g$ positive" is a hypothesis on $g$ 's values at the nonnegative reals that $X$ and $Y$ actually take, not on all of $\mathbb{R}$ , and must not be silently strengthened to " $g$ everywhere positive" or weakened to " $g$ nonnegative" (which would let $g$ vanish and break the order's need for $e^{-sg(X)}$ to be well-behaved).

Formalization scope

LaplaceOrder μ ν X Y takes $X : \Omega \to \mathbb{R}$ on $(\Omega,\mu)$ and $Y : \Omega' \to \mathbb{R}$ on a separate $(\Omega',\nu)$ , matching the series' convention (e.g. StochasticOrders.Usual.UsualOrder) that the order compares distributions, not jointly defined variables. Nonnegativity of $X$ and $Y$ is an explicit hypothesis ∀ ω, 0 ≤ X ω / ∀ ω, 0 ≤ Y ω on every theorem, never built into LaplaceOrder itself. CompletelyMonotone φ is ContDiff ℝ ⊤ φ ∧ ∀ n x, 0 < x → 0 ≤ (-1)^n * iteratedDeriv n φ x — the smoothness conjunct guards the junk-value trap described above. The survival function $\bar F(x) = P\{X>x\}$ in the goal theorem is formalized inline as (μ {ω | x < X ω}).toReal, valid since μ is a probability measure (so the underlying ENNReal value is finite and the conversion to ℝ loses no information); the integral $\int_0^\infty$ is Bochner integration over Set.Ici (0 : ℝ). "Provided the expectations exist" becomes explicit Integrable hypotheses per statement (on $X$ , $Y$ themselves for Eq. 5.A.5; on $\varphi \circ X$ , $\varphi \circ Y$ for each $\varphi$ in Theorem 5.A.3), rather than a blanket integrability assumption that would understate which expectations the book actually needs. Independence in the convolution corollary is ProbabilityTheory.iIndepFun, one family per side, as in Chunk 01's own convolution corollary. A trivializing formalization is ruled out: $\le_{Lt}$ is not restated as a comparison of one moment or of the raw random variables' means, and the "universal function class" of Theorem 5.A.3 is exactly the completely monotone functions the book names, not a fixed finite subfamily or a narrowed subclass (e.g. only the exponentials themselves, which would make Theorem 5.A.3 a restatement of the definition rather than its own theorem).

This mission draws on no platform prior art: repeated searches for "Laplace transform" and "completely monotone" during this session return only unrelated analytic-number-theory formalizations (a Langlands–Tunnell Laplace–Mellin transform identity) and no hits at all, respectively — confirming BRIEF.md's expectation that this subarea is untouched on the platform. It is one of nine missions in a series covering the whole book; per the series' own convention, its definitions are not imported by any other chapter's mission, and it does not import any other chapter's definitions in turn (the chapter itself has essentially no cross-chapter dependence, the reason it was flagged as the series' most self-contained chunk).

Selected references

M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

8 thms2 active usersReviewed

Completed

Machine Learning Statistics·Captain: mikedeng1

High-Dimensional Statistics IV: Dudley's Entropy Integral BoundTextbook

Motivation

Many of the central questions of high-dimensional statistics reduce to bounding the expected supremum of a stochastic process: the maximum correlation of noise with a family of candidate signals, the operator norm of a random matrix, the uniform deviation of an empirical process from its mean. Whenever the index set of the process is infinite or exponentially large, a naive union bound over "all" indices is either vacuous or requires re-deriving a tail bound from scratch for every new problem. Chaining is the general-purpose technique that removes this need: it bounds the expected supremum of a process purely in terms of the geometry of its index set, measured by how many balls of a given radius are needed to cover it. The classical form of this bound is due to Dudley (1967), building on ideas that trace to Kolmogorov; the exposition here follows Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 5.

Setting

Fix an index set $T$ and a collection of zero-mean random variables $\{X_\theta,\theta\in T\}$ . Say this collection is a sub-Gaussian process with respect to a (pseudo)metric $\rho_X$ on $T$ (Definition 5.16) if

\mathbb E\big[e^{\lambda(X_\theta-X_{\theta'})}\big] \;\le\; e^{\lambda^2\rho_X(\theta,\theta')^2/2} \qquad \text{for all } \theta,\theta'\in T,\ \lambda\in\mathbb R.

This single condition covers, as special cases, the canonical Gaussian process $X_\theta = \langle\theta, w\rangle$ for $w$ a standard Gaussian vector (with $\rho_X$ the Euclidean metric) and the Rademacher process built from i.i.d. Rademacher signs.

A $\delta$ -cover of $T$ with respect to a metric $\rho$ is a finite set $\{\theta_1,\dots,\theta_N\}\subset T$ such that every $\theta\in T$ lies within $\rho$ -distance $\delta$ of some $\theta_i$ ; the $\delta$ -covering number $N(\delta;T,\rho)$ is the size of the smallest such cover (Definition 5.1). The quantity $\log N(\delta;T,\rho)$ is the metric entropy of $T$ at scale $\delta$ . Writing $D:=\sup_{\theta,\theta'\in T}\rho_X(\theta,\theta')$ for the diameter of $T$ , the $\delta$ -truncated Dudley entropy integral is

J(\delta; D) \;:=\; \int_\delta^D \sqrt{\log N(u;T)}\,du.

Formalization targets

Goal — Theorem 5.22 (Dudley's entropy integral bound)

\mathbb E\Big[\sup_{\theta,\theta'\in T}(X_\theta-X_{\theta'})\Big] \;\le\; 2\,\mathbb E\Big[\sup_{\substack{\gamma,\gamma'\in T\\\rho_X(\gamma,\gamma')\le\delta}}(X_\gamma-X_{\gamma'})\Big] + 32\,J(\delta/4; D), \qquad \text{for any } \delta\in[0,D].

The bound holds for every zero-mean sub-Gaussian process, with no further structure on $T$ beyond its metric entropy — this is what makes it a general-purpose tool rather than a bound tailored to one model.

Milestone — Proposition 5.17 (one-step discretization bound)

The same conclusion with $32\,J(\delta/4;D)$ replaced by the cruder single-scale term $4\sqrt{D^2\log N(\delta;T)}$ , under the extra technical hypothesis $N(\delta;T)\ge 10$ . This is the one-step precursor whose refinement — iterating the discretization over a geometric sequence of scales instead of applying it once — is exactly what chaining improves.

Milestone — Theorem 5.25 (the Gaussian comparison principle)

A general comparison principle for pairs of centered Gaussian random vectors whose pairwise covariances are ordered coordinatewise and tested against a function with matching sign conditions on its mixed second partial derivatives: $\mathbb E[F(X)]\le\mathbb E[F(Y)]$ . This is the source, by specializing $F$ and the covariance-ordering sets, of both Slepian's inequality and the Sudakov–Fernique comparison, the two workhorse tools of Gaussian process theory used elsewhere in the chapter to obtain sharper, Gaussian-specific bounds than the sub-Gaussian chaining bound above.

Significance

Dudley's bound is the single most-used tool for controlling suprema of stochastic processes in high-dimensional statistics and empirical process theory: Gaussian complexity bounds for convex bodies, operator-norm bounds for random matrices, and uniform laws of large numbers for function classes are all obtained by computing a covering-number bound for the relevant index set and substituting it into Theorem 5.22 (see, for instance, Examples 5.18–5.21 later in the same chapter, and Chapters 13–14 of the book). Its significance is exactly its generality: it converts a purely geometric quantity — how "big" a set is under a metric — into a probabilistic bound, uniformly over every sub-Gaussian process on that set.

Formalizing it. The mathematical proof (interpolation-free, based on chaining and repeated union bounds) is well understood and not itself in question; what this mission produces is a faithful Lean statement of the theorem, its immediate one-step precursor, and the general Gaussian comparison principle that underlies the chapter's complementary (Gaussian-specific) results, each against Mathlib's own measure-theoretic and Gaussian-process infrastructure. All three theorems are currently stated as open goals (:= by sorry); no claim is made here that they are already formalized elsewhere on the platform (a fresh prior-art search for "Dudley," "chaining," "Slepian," "Sudakov," and "Gaussian comparison" returned no faithful matches).

Difficulty

The naive approach — apply Proposition 5.17's one-step discretization once, at whatever scale $\delta$ seems best — cannot see improvement past the cruder $\sqrt{D^2\log N(\delta;T)}$ scaling of the metric entropy at a single resolution. The chaining argument that proves Theorem 5.22 instead telescopes the supremum across a geometric ladder of covers at scales $D2^{-1},D2^{-2},\dots$ , paying for each scale's approximation with a union bound over its own (much smaller, for a small $\delta$ ) covering number, and only then summing the resulting terms into an integral. The difficulty is not any single step of this argument — each step is an elementary sub-Gaussian tail bound — but bookkeeping the composition correctly: the recursive "best approximation at level $m$ of the best approximation at level $m+1$ " chain (Eq. (5.47)) must be built explicitly, and the telescoping sum of $L$ union bounds, each over a set that itself depends on the level $m$ , is what converts into an integral only in the $L\to\infty$ limit as the covers refine to $T$ itself.

Formalization scope

The index set $T$ is formalized as a nonempty Fintype, rather than the book's general totally bounded metric space: this keeps every covering number, diameter, and supremum in this mission a genuine maximum over a finite, nonempty family (realized via ⨆/sInf over finite index types), rather than requiring the full apparatus of totally bounded infinite metric spaces to state the covering-number definition (Definition 5.1) faithfully without risking a vacuous or ill-defined infimum. This is a genuine narrowing of the book's stated generality, disclosed here rather than left implicit — the underlying mathematics of the proof does not depend on finiteness, but a faithful formalization of a general totally bounded space's covering number was judged out of scope for this mission's budget.

The constant $32$ in the goal theorem is kept exactly as stated; the book's own remark that "there is no particular significance to the constant 32, which could be improved with a more careful analysis" is not license to substitute a sharper constant, since doing so would no longer match what this particular proof establishes. Expectations are Bochner integrals against an explicit probability measure Prob, with integrability required as an explicit hypothesis in the sub-Gaussian process definition (SubGaussianProcess) rather than left implicit, since Mathlib's Bochner integral silently returns $0$ for a non-integrable function — a trivializing formalization this mission's definitions and hypotheses rule out.

Theorem 5.25's "centered Gaussian random vector" is formalized using Mathlib's own ProbabilityTheory.HasGaussianLaw predicate (a genuine multivariate Gaussian law, not merely Gaussian marginals) together with an explicit coordinatewise mean-zero hypothesis, and its mixed second partial derivative condition is formalized via iteratedFDeriv ℝ 2 F applied to the relevant pair of standard basis vectors, keeping the sign pattern over the disjoint index sets $A$ and $B$ exact rather than collapsing it to a global convexity assumption on $F$ .

Out of scope for this mission: Sudakov's minoration (the complementary lower bound on the expected supremum of a genuinely Gaussian process, Theorem 5.30, misidentified as "Theorem 5.36" in this mission's planning brief — the correct Sudakov minoration statement is Theorem 5.30, p. 148; Theorem 5.36 is instead a tail-bound generalization of Dudley's bound to $\psi_q$ -Orlicz processes) and the Slepian/Sudakov–Fernique corollaries of Theorem 5.25 (Corollary 5.26, Theorem 5.27) — both natural follow-on work for a later contribution, once the Gaussian comparison principle formalized here is in place.

Selected references

M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 5.
R. M. Dudley, "The sizes of compact subsets of Hilbert space and continuity of Gaussian processes," Journal of Functional Analysis, 1(3):290–330, 1967.
M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991.

9 thms2 active usersReviewed

Completed

Machine Learning Random Matrix Theory Statistics·Captain: mikedeng1

High-Dimensional Probability VII: Slepian's Inequality for Gaussian ProcessesTextbook

Motivation

A Gaussian process is a family $(X_t)_{t\in T}$ of jointly Gaussian real random variables indexed by an arbitrary set $T$ — not necessarily time. The canonical example is $X_t = \langle g, t\rangle$ for $t$ ranging over a subset $T\subseteq\mathbb R^n$ and $g$ a standard Gaussian vector in $\mathbb R^n$ ; this single family already encodes questions as varied as the operator norm of a random matrix, the size of a random projection, and the metric complexity of a convex body. In every one of these applications the object of interest reduces to the same quantity: $E\sup_{t\in T} X_t$ , the expected supremum of the process.

Bounding $E\sup_{t\in T} X_t$ directly is hard — computing it exactly is possible only in special cases, such as the reflection principle for Brownian motion. Slepian's inequality (David Slepian, 1962) sidesteps this by comparison: if a second Gaussian process $(Y_t)_{t\in T}$ has matching variances and at-least-as-large pairwise increments as $(X_t)_{t\in T}$ , then $Y$ 's supremum stochastically dominates $X$ 's. This turns a hard direct estimate into a search for a simpler comparison process — the technique that Sudakov and Fernique later sharpened by dropping the equal-variance hypothesis (Theorem 7.2.11), and that Sudakov used to derive a purely geometric lower bound on $E\sup_{t\in T}X_t$ from the covering numbers of $(T,d)$ (Theorem 7.4.1, Sudakov's minoration inequality). Together these results are the entry point to the theory of Gaussian width and generic chaining that occupies the rest of the book (Chapters 7–9, 11), and they underlie sharp bounds on random matrices (Section 7.3), random projections (Chapter 9), and high-dimensional geometry more broadly (Adler and Taylor, Random Fields and Geometry, Springer, 2007; Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014).

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ . A random process indexed by a set $T$ is a family $(X_t)_{t\in T}$ of real random variables on $\Omega$ . It is a Gaussian process if every finite linear combination $\sum_{t\in T_0} a_t X_t$ ( $T_0\subseteq T$ finite, $a_t\in \mathbb R$ ) is a (possibly degenerate) normal random variable — equivalently, every finite marginal $(X_t)_{t\in T_0}$ is a multivariate Gaussian vector. A process is mean zero if $EX_t = 0$ for every $t$ .

For a mean zero process, the increments $d(t,s) := \lVert X_t - X_s\rVert_{L^2} = (E(X_t - X_s)^2)^{1/2}$ always define a (pseudo)metric on $T$ — the canonical metric — turning the otherwise unstructured index set into a metric space. For a metric space $(T,d)$ and $\varepsilon

0 $, the **covering number**$ N(T,d,\varepsilon) $is the smallest cardinality of a finite subset$ N\subseteq T $such that every point of$ T $is within$ \varepsilon $of some point of$ N $(an$ \varepsilon $-net);$ N(T,d,\varepsilon) := \infty$ if no finite net exists.

Because $T$ need not be countable, $\sup_{t\in T} X_t(\omega)$ need not be a measurable function of $\omega$ . Following the book's own convention, every quantity built from this supremum — $E\sup_{t\in T}X_t$ and $P\{\sup_{t\in T}X_t\ge\tau\}$ — is instead defined through the process's finite-dimensional marginals: as the supremum, over finite nonempty $T_0\subseteq T$ , of $E\max_{t\in T_0}X_t$ (respectively $P\{\max_{t\in T_0}X_t\ge\tau\}$ ). This sidesteps the measurability question entirely, at the cost of the quantity possibly being $+\infty$ .

Formalization targets

Slepian's inequality (Theorem 7.2.1, goal)

Let $(X_t)_{t\in T}$ and $(Y_t)_{t\in T}$ be mean zero Gaussian processes with $EX_t^2 = EY_t^2$ and $E(X_t-X_s)^2 \le E(Y_t-Y_s)^2$ for all $t,s\in T$ . Then for every $\tau\in\mathbb R$ ,

P\{\sup_{t\in T} X_t \ge \tau\} \le P\{\sup_{t\in T} Y_t \ge \tau\},

and consequently $E\sup_{t\in T} X_t \le E\sup_{t\in T} Y_t$ .

Sudakov-Fernique's inequality (Theorem 7.2.11, milestone)

Under only the increment hypothesis $E(X_t-X_s)^2 \le E(Y_t-Y_s)^2$ (no equal-variance hypothesis),

E\sup_{t\in T} X_t \le E\sup_{t\in T} Y_t.

This is the weaker-hypothesis, strictly more applicable form: it is what Sudakov's minoration inequality and the sharp Gaussian random matrix bound of Section 7.3 both invoke.

Sudakov's minoration inequality (Theorem 7.4.1, milestone)

Let $(X_t)_{t\in T}$ be a mean zero Gaussian process with canonical metric $d$ . For every $\varepsilon\ge 0$ at which $N(T,d,\varepsilon)=:N$ is finite,

E\sup_{t\in T} X_t \ge c\,\varepsilon\,\sqrt{\log N}

for an absolute constant $c>0$ . This is the weakest, most stable form of the bound: it names no numerical value for $c$ , so it survives any later sharpening of the constant.

Slepian's inequality, finite-dimensional case (Theorem 7.2.9, milestone)

The vector-indexed special case of Theorem 7.2.1 ( $T$ finite), proved first by Gaussian interpolation and then extended to the general index set.

Significance

The results themselves. Slepian's inequality is the founding comparison theorem for Gaussian processes; Sudakov-Fernique's inequality is its practically indispensable generalization, used routinely to bound suprema of Gaussian processes without needing to track variances explicitly. Sudakov's minoration inequality is the first bridge from the probability of a Gaussian process to the metric geometry of its index set, complementing Dudley's upper bound (Chapter 8) and together giving matching bounds — up to a logarithmic factor, and exactly in many cases of interest — on $E\sup_{t\in T}X_t$ purely from the covering numbers of $(T,d)$ . Downstream, this machinery gives the sharp bound $E\lVert A\rVert \le \sqrt m + \sqrt n$ on Gaussian random matrices (Section 7.3), underlies the Gaussian width used throughout convex geometry and compressed sensing (Chapters 9, 11), and bounds the covering numbers of polytopes and other convex sets (Corollary 7.4.4).

Formalizing it. All three inequalities are proved by the book (Gaussian interpolation and integration by parts for Slepian/Sudakov-Fernique; a direct application of Sudakov-Fernique to a well-chosen comparison process for Sudakov's minoration), so this mission's work is formalizing the statements faithfully and precisely — including the finite-marginal convention needed to make $E\sup_{t\in T}X_t$ and $P\{\sup_{t\in T}X_t\ge\tau\}$ meaningful for an uncountable index set without begging the underlying measurability question. The Gaussian interpolation technique itself (Lemmas 7.2.3, 7.2.5, 7.2.7) is not part of this mission's formalization scope; it is the proof method for the milestones and belongs to solvers closing them.

Difficulty

The obvious first idea — bound $E\sup_t X_t$ by controlling each $X_t$ separately, e.g. via a union bound over a net — throws away exactly the structure Slepian-type comparisons exploit: the joint Gaussianity across $t$ , not marginal tail behavior at each fixed $t$ . A union bound needs a net and a modulus of continuity to begin with; Slepian's and Sudakov-Fernique's inequalities need neither — they compare two processes directly through their covariance structure, which is what makes the technique (Gaussian interpolation: continuously deform the covariance of one process into the other's, and track how a smooth, nearly-indicator functional behaves along the path) work with no assumption on $T$ beyond the two hypotheses stated. The genuine difficulty is the smooth-interpolation argument itself — showing that $E f(Z(u))$ is monotone in $u$ for the right choice of test function $f$ — which is exactly the part left as a milestone for solvers to formalize, not sketched here per the mission format's own rule against proof ideas.

Formalization scope

$E\sup_{t\in T}X_t$ (ProcessESup) is valued in EReal, not ℝ: the finite-marginal supremum a real-valued definition would silently default to the junk value $0$ when the set of finite-marginal expectations is unbounded above — exactly the case the book itself records as $E\sup_{t\in T}X_t=\infty$ (Exercise 7.4.2, a non-relatively-compact index set). P\{\sup_{t\in T}X_t\ge\tau\} (ProcessTailProb) stays real-valued, since it is always bounded in $[0,1]$ and so carries no such risk. Both are defined through finite nonempty subsets of $T$ , per the book's own footnote to Section 7.2; no separability, continuity, or countability assumption is placed on $T$ itself.

Gaussianity is Mathlib's ProbabilityTheory.IsGaussianProcess — every finite restriction of the process has a Gaussian law — which is definitionally the book's Definition 7.1.10 ("every finite linear combination is Gaussian"); mean-zero is stated as an explicit hypothesis alongside it. Integrability of every quantity appearing under an expectation is not stated as a separate hypothesis: Fernique's theorem (already in Mathlib for general Gaussian measures) guarantees a Gaussian process has finite moments of every order, exactly as the book takes for granted.

Sudakov's minoration inequality (Theorem 7.4.1) is formalized for the case the book's own proof actually covers — $N(T,d,\varepsilon)$ finite, taken as a hypothesis = (N : ℕ) rather than as a case split inside the conclusion — since the book itself defers the infinite-covering-number case to a separate, unproved exercise (7.4.2). This keeps $T$ fully general (still possibly uncountable) at every fixed $\varepsilon$ where the net is finite, which rules out a trivializing reading of the theorem: nothing here forces $T$ itself to be finite or countable, only the covering number at the scale $\varepsilon$ in play, which is the book's own hypothesis.

Definitions reusable beyond this mission: ProcessESup, ProcessTailProb, CanonicalMetric, and CoveringNumber are exactly the substrate Chapters 8 ("Dudley's Integral Inequality"), 9 ("The Matrix Deviation Inequality"), and 11 ("Dvoretzky-Milman's Theorem") need for Gaussian width and generic chaining; per this series' plan those missions restate them locally (drafts cannot import another draft's definitions), using this chunk's forms as the faithful reference. Contributions closing the Gaussian-interpolation machinery (Lemmas 7.2.3–7.2.8) as a reusable definitions layer, beyond what any one milestone needs, are welcome.

Selected references

Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018. https://www.math.uci.edu/~rvershyn/papers/HDP-book/HDP-book.pdf
D. Slepian, "The one-sided barrier problem for Gaussian noise", Bell System Technical Journal 41 (1962), 463–501.
V. N. Sudakov, "Gaussian random processes and measures of solid angles in Hilbert space", Soviet Mathematics Doklady 12 (1971), 412–415.
X. Fernique, "Regularité des trajectoires des fonctions aléatoires gaussiennes", in École d'Été de Probabilités de Saint-Flour IV-1974, Springer Lecture Notes in Mathematics 480 (1975), 1–96.
M. Talagrand, Upper and Lower Bounds for Stochastic Processes: Modern Methods and Classical Problems, Springer, 2014.

11 thms2 active usersReviewed

Machine Learning Statistics Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning IV: Support Vector Machines and the Margin BoundTextbook

Motivation

Support vector machines were, for two decades, the workhorse of applied classification, and the reason offered for their success was always geometric: SVMs maximize the margin between the two classes. Chapter 3's VC-dimension bound cannot explain why this should help — for linear hypotheses in $\mathbb R^N$ its bound depends on $N+1$ and is uninformative whenever the feature dimension is large relative to the sample size, exactly the regime (kernel-induced or high-dimensional features) where SVMs are most often used. Chapter 5 answers the question this leaves open: a generalization bound for a real-valued hypothesis, stated in terms of its margin on the training sample, that does not depend on the ambient dimension at all. This is also the template every later chapter's margin bound specializes (multi-class classification, ranking, and, indirectly, boosting all reuse the same Rademacher-complexity-of-a-Lipschitz-loss argument developed here).

Setting

A hypothesis here is a real-valued function $h:X\to\mathbb R$ , not (as in Chapters 2-3) a function into $\{-1,+1\}$ : for a labeled point $(x,y)$ with $y\in\{-1,+1\}$ , the sign of $h(x)$ gives the prediction and $|h(x)|$ is read as the classifier's confidence. The confidence margin of $h$ at $(x,y)$ is $y\,h(x)$ ; it is positive exactly when $h$ classifies $x$ correctly. For $\rho>0$ , the $\rho$ -margin loss $\Phi_\rho:\mathbb R\to\mathbb R$ (Definition 5.5) is

\Phi_\rho(x) = \min\Big(1,\max\Big(0,1-\frac x\rho\Big)\Big),

equal to $1$ when $x\le 0$ (misclassified), $0$ when $x\ge\rho$ (classified with confidence at least $\rho$ ), and interpolating linearly in between; it is $1/\rho$ -Lipschitz. The empirical margin loss on a sample $S=(x_1,\dots,x_m)$ with labels $y_1,\dots,y_m$ (Definition 5.6) is $\hat R_{S,\rho}(h) = \frac1m\sum_{i=1}^m\Phi_\rho(y_ih(x_i))$ — the fraction of training points misclassified or classified with confidence below $\rho$ , a strictly stronger requirement than plain misclassification. The (population) generalization error is $R(h)=\Pr_{(x,y)\sim D}[y\,h(x)\le 0]$ . Rademacher complexity, $\hat R_S(H)$ and $R_m(H)$ (Definitions 3.1-3.2, restated here since chunk 03-rademacher-vc's own copies are still drafts), measure how well a real-valued hypothesis class $H$ correlates with random sign noise on a sample, and are the vehicle through which the margin bound's complexity term is expressed.

Formalization targets

Lemma 5.7 (Talagrand's lemma, milestone). For $l$ -Lipschitz $\Phi_1,\dots,\Phi_m:\mathbb R\to\mathbb R$ and any hypothesis set $H$ of real-valued functions,

\frac1m\,\mathbb E_\sigma\Big[\sup_{h\in H}\sum_{i=1}^m\sigma_i(\Phi_i\circ h)(x_i)\Big] \le l\,\hat R_S(H).

Theorem 5.10 (Rademacher complexity of bounded-norm linear hypotheses, milestone). For $S\subseteq\{x:\|x\|\le r\}$ and $H=\{x\mapsto w\cdot x:\|w\|\le\Lambda\}$ ,

\hat R_S(H) \le \sqrt{r^2\Lambda^2/m}.

Corollary 5.11 (margin bound for linear hypotheses, milestone). For the same $H$ and $X\subseteq\{x:\|x\|\le r\}$ , fixing $\rho>0$ , with probability at least $1-\delta$ ,

R(h) \le \hat R_{S,\rho}(h) + 2\sqrt{\frac{r^2\Lambda^2/\rho^2}{m}} + \sqrt{\frac{\log(1/\delta)}{2m}} \quad\text{for all } h\in H.

Theorem 5.8 — the mission's goal. For any set $H$ of real-valued functions and $\rho>0$ , with probability at least $1-\delta$ , both

R(h) \le \hat R_{S,\rho}(h) + \frac2\rho R_m(H) + \sqrt{\frac{\log(1/\delta)}{2m}}

R(h) \le \hat R_{S,\rho}(h) + \frac2\rho \hat R_S(H) + 3\sqrt{\frac{\log(2/\delta)}{2m}}

hold simultaneously for all $h\in H$ .

Significance

Theorem 5.8 is genuinely dimension-free: unlike Chapter 3's VC-dimension bound (5.36 in the book, restated from Corollary 3.19), it holds regardless of the ambient feature dimension $N$ , depending instead only on the hypothesis class's Rademacher complexity and the chosen margin $\rho$ . Specialized to bounded-norm linear hypotheses (Corollary 5.11), this gives the theoretical justification most often cited for SVMs and every other margin-maximization algorithm: whenever the training data admits a large geometric margin, the empirical margin loss at that margin is small (often zero, in the separable case) and the bound is tight regardless of $N$ . Every later chapter's own margin bound (multi-class in Chapter 9, ranking in Chapter 10) is a direct structural descendant of Theorem 5.8's proof technique. No prior art on the Prove2Me platform is faithful: GET /theorems?q=support+vector+machine and q=margin+bound return no hits on this book's model (the two q=margin+bound hits found, both from the Aether Catalog, state a different comparison — a VC-type bound is eventually worse than a fixed Rademacher-type bound as a function of dimension — not Theorem 5.8 itself); q=Talagrand and q=contraction+principle return several hits (Ledoux/Talagrand convex-distance concentration, Rudin's Banach-space contraction-mapping theorem, a generic Rademacher-sign contraction lemma for quadratic sums) but every one states either a different mathematical object (metric-space fixed points, Talagrand's concentration inequality on product spaces) or a different idiom (squared vs. linear coordinate sums) from Lemma 5.7's function-composition contraction — none reused. All nine items are drafted fresh.

Not formalized here: Theorem 5.4 (the SVM sparsity/leave-one-out bound). It is listed as a candidate milestone in BRIEF.md, but its statement and proof depend on the primal/dual SVM optimization problem itself (the Lagrangian, KKT conditions, and the resulting definition of a "support vector" as a training point with nonzero dual coefficient) — a materially different, non-margin-based proof technique (leave-one-out stability of the trained hypothesis, via Lemma 5.3) that shares no definitions with the margin-bound family this mission's goal and other milestones are built on. Formalizing it faithfully would require standing up the SVM primal/dual formalism (Lagrangian, complementary slackness, the "support vector" predicate itself) from scratch, which is disproportionate to a single additional milestone within this mission's budget; per the captain brief's guidance to leave out, rather than approximate, a statement that cannot be made faithful in the time available, it is omitted.

Difficulty

The proof of Theorem 5.8 needs the empirical margin loss's zero-one-loss upper bound ( $\mathbb 1_{u\le 0}\le\Phi_\rho(u)$ ) applied before invoking Theorem 3.3's Rademacher generalization bound on the composed class $\tilde{\tilde H}=\{\Phi_\rho\circ f: f\in\tilde H\}$ , $\tilde H=\{(x,y)\mapsto y\,h(x):h\in H\}$ — reversing this order (bounding $R(h)$ by a Rademacher complexity computed on the zero-one loss directly) does not work, because the zero-one loss is not Lipschitz. Talagrand's lemma is exactly what lets the $1/\rho$ -Lipschitz surrogate $\Phi_\rho$ be pulled outside the Rademacher complexity, at the cost of a factor $1/\rho$ and no worse; its own proof is an induction removing one Rademacher variable at a time, using a two-point supremum argument (fixing $\epsilon>0$ , choosing near-optimal $h_1,h_2$ ) that does not simplify to anything less than genuine care with suprema of non-smooth objects — a formalization attempting to replace this with a naive linearity-of-expectation argument would be proving a false or vacuous statement, since $\sup$ does not commute with linear combinations. Theorem 5.10's bound needs the Cauchy-Schwarz and Jensen inequalities used in the particular order the book uses them (Cauchy-Schwarz on the empirical sup, then Jensen on the expectation of a norm, then the independence of the $\sigma_i$ s) — the bound $\hat R_S(H)\le r\Lambda/\sqrt m$ does not follow from either inequality alone.

Formalization scope

EmpiricalRademacherComplexity/RademacherComplexity are restated locally in SVM, byte-identical to chunk 03-rademacher-vc's own copies (a draft item cannot import another chunk's draft module); this duplication collapses once 03-rademacher-vc is uploaded and listed in missions/README.md's "Published definitions" table. MarginGeneralizationError is a new, real-valued-hypothesis specialization of Definition 2.1 (R(h) = P[y h(x) ≤ 0]), distinct from every earlier chunk's {-1,+1}-valued GeneralizationError, since no earlier chunk's own copy matches this chapter's real-valued convention. PhiRho/EmpiricalMarginLoss are new. The goal theorem (margin_bound_binary_classification) states H's own Rademacher complexity computed on the marginal X-distribution (D.map Prod.fst), matching the book's final displayed form — the proof's intermediate step (the lifted class $\tilde H=\{(x,y)\mapsto y h(x)\}$ having the same Rademacher complexity as $H$ itself, since $y\in\{-1,+1\}$ ) is not separately drafted, only the theorem's statement. Theorem 5.10/Corollary 5.11 generalize the book's ambient $\mathbb R^N$ to an arbitrary real inner-product space X ([NormedAddCommGroup X] [InnerProductSpace ℝ X]), a harmless generalization since the book's proof (Cauchy-Schwarz, Jensen, orthogonality of Rademacher signs) uses only the inner-product structure, never finite dimension; [BorelSpace X] is added to Corollary 5.11's statement to make the measurable structure under which MarginGeneralizationError is well-posed explicit, since every x ↦ ⟨w, x⟩ is automatically Borel-measurable — not a substantive restriction, the book never discusses measurability of linear functionals. No numerical constant in any of the four theorems is altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Theorem 5.8 only for a Finset/finite H (which would make it a disguised instance of Chapter 2's finite-hypothesis bound rather than the chapter's genuinely new, complexity-based argument) — H : Set (X → ℝ) is left fully general, exactly as the book states it.

Selected references

M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 5.
C. Cortes, V. Vapnik, "Support-vector networks," Machine Learning 20(3), 1995, 273-297.
M. Talagrand, "Sharper bounds for Gaussian and empirical processes," The Annals of Probability 22(1), 1994, 28-76.
P. Bartlett, S. Mendelson, "Rademacher and Gaussian complexities: risk bounds and structural results," Journal of Machine Learning Research 3, 2002, 463-482.

12 thms2 active users

Machine Learning Statistics·Captain: mikedeng1

High-Dimensional Statistics III: A Uniform Law via Rademacher ComplexityTextbook

Motivation

Many statistical estimators are defined by minimizing an empirical average over a class of candidate models — empirical risk minimization, maximum likelihood, and binary classification all fit this template. Analyzing such an estimator's excess risk reduces, in each case, to controlling how far the empirical average of a whole class of functions can deviate from its population expectation, not just a single fixed function — a much stronger requirement than the ordinary law of large numbers, which only controls one function at a time. This mission formalizes the central non-asymptotic tool for this problem, the Rademacher complexity-based uniform law, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 4.

Setting

Let $F$ be a class of real-valued functions with a common domain, indexed as $F=\{f_j, j\in\iota\}$ , and let $X_1,\dots,X_n$ be i.i.d. samples from a distribution $P$ . The empirical process deviation (Eq. (4.7)) is

\|\mathbb P_n-P\|_F \;:=\; \sup_{f\in F}\Big|\frac1n\sum_{i=1}^n f(X_i) - \mathbb E[f(X)]\Big|.

Given an independent Rademacher sequence $\varepsilon_1,\dots,\varepsilon_n$ (each $\varepsilon_i=\pm1$ equiprobably), the symmetrized process (Eq. (4.19)) and the Rademacher complexity (Eq. (4.13)) of $F$ are

\|S_n\|_F := \sup_{f\in F}\Big|\frac1n\sum_{i=1}^n\varepsilon_if(X_i)\Big|, \qquad R_n(F) := \mathbb E_{X,\varepsilon}[\|S_n\|_F].

A class $F$ is $b$ -uniformly bounded if $\|f\|_\infty\le b$ for every $f\in F$ .

Formalization targets

Goal — Theorem 4.10 (a uniform law via Rademacher complexity)

For any $b$ -uniformly bounded class $F$ , any $n\ge1$ , and any $\delta\ge0$ ,

\|\mathbb P_n-P\|_F \;\le\; 2R_n(F)+\delta

with $P$ -probability at least $1-\exp(-n\delta^2/2b^2)$ .

Milestone — Proposition 4.11 (symmetrization sandwich)

For any convex non-decreasing $\Phi$ , $\mathbb E[\Phi(\tfrac12\|S_n\|_{\bar F})] \le \mathbb E[\Phi(\|\mathbb P_n-P\|_F)] \le \mathbb E[\Phi(2\|S_n\|_F)]$ , where $\bar F$ is the recentered class. This generalizes the specific symmetrization step used in Theorem 4.10's own proof (the case $\Phi(t)=t$ ) to an entire family of moment comparisons.

Milestone — Eq. (4.16) (concentration around the mean)

For a $b$ -uniformly bounded, i.i.d.-sampled class $F$ , $\|\mathbb P_n-P\|_F - \mathbb E[\|\mathbb P_n-P\|_F] \le t$ with $P$ -probability at least $1-e^{-nt^2/2b^2}$ , obtained via the bounded-differences method. Combined with Proposition 4.11's bound on $\mathbb E[\|\mathbb P_n-P\|_F]$ by $2R_n(F)$ , this is exactly Theorem 4.10's proof.

Significance

Theorem 4.10 is the general-purpose engine behind the classical Glivenko–Cantelli theorem (recovered by taking $F$ to be the class of half-line indicator functions, Example 4.6) and behind uniform convergence guarantees for empirical risk minimization more broadly (Section 4.1.2): whenever a task can be reduced to bounding the Rademacher complexity of a specific function class — a purely combinatorial/geometric quantity independent of any particular statistical model — Theorem 4.10 converts that bound directly into a high-probability uniform convergence guarantee. Proposition 4.11 is separately significant as the general symmetrization principle from which Theorem 4.10's specific bound, and many similar bounds throughout empirical process theory, are instances.

Formalizing it. No faithful prior art exists on the platform: a fresh search for "uniform law," "symmetrization," "Rademacher complexity," "Glivenko-Cantelli," and "empirical process" found only unrelated hits and the existing RademacherSymmetrization.*/RademacherMassart.* items, which are specific to finite function classes (Finset (X → ℝ)) — a strictly narrower setting than Theorem 4.10's fully general (possibly infinite) function classes, and not reused here. All three theorems are drafted as open goals (:= by sorry).

Difficulty

The naive approach to bounding $\|\mathbb P_n-P\|_F$ — apply a scalar concentration bound to each $f\in F$ individually and union-bound over $F$ — fails outright when $F$ is infinite (there is no union bound to take). The two-step resolution captured by this mission's milestones avoids this entirely: first, $\|\mathbb P_n-P\|_F$ itself, viewed as a single function of the $n$ samples, is shown to concentrate sharply around its own mean via the bounded-differences method (no union bound over $F$ needed — the argument treats $\sup_{f\in F}(\cdots)$ as one Lipschitz function of the samples). Second, the mean $\mathbb E[\|\mathbb P_n-P\|_F]$ itself, a single deterministic number, is bounded via symmetrization: introducing an independent "ghost sample" $Y_i$ with the same law as $X_i$ converts the un-symmetric quantity $\mathbb E[\sup_f|(1/n)\sum f(X_i)-\mathbb E f|]$ into the manifestly symmetric $\mathbb E[\sup_f|(1/n)\sum\varepsilon_i (f(X_i)-f(Y_i))|]$ , and it is only after this symmetrization that the supremum over $F$ becomes tractable via the geometry of $F$ (its Rademacher complexity) rather than requiring $F$ finite.

Formalization scope

The function class $F$ is realized as the range of an index family $f:\iota\to D\to\mathbb R$ rather than a Set (D → ℝ), matching the standard representation of a (possibly infinite) function class by an index type; ι carries no finiteness assumption, matching the book's own full generality (in contrast to the platform's existing RademacherSymmetrization/ RademacherMassart items, which are finite-class-specific). The population expectation $\mathbb E[f(X)]$ is realized via an explicit population variable $X_0$ sharing the samples' common law, rather than a separately axiomatized abstract distribution object. The Rademacher sequence and the samples are packaged into one jointly independent family Z : ℕ → Ω → D × ℝ with an explicit hypothesis that the two coordinates are themselves independent at each index — capturing " $\varepsilon$ independent of $X$ , both i.i.d." exactly, without a bespoke joint-independence predicate.

Theorem 4.10's own qualitative corollary ("consequently, $\|\mathbb P_n-P\|_F\xrightarrow{a.s.}0$ whenever $R_n(F)=o(1)$ ") is not included in the goal's conclusion: it concerns an infinite sequence of samples and asymptotic convergence via the Borel–Cantelli lemma, a substantially different formal object (requiring Filter.Tendsto over ℕ→∞ and ∀ᵐ almost-sure convergence) from the single- $n$ non-asymptotic tail bound (4.14) this mission's goal states, and is left as natural follow-on work, alongside a direct formalization of the classical Glivenko–Cantelli theorem (Theorem 4.4) as a corollary.

Lemma 4.14 (the polynomial-discrimination route to bounding Rademacher complexity for VC-type classes) is out of scope for this mission: its displayed inequality is extracted with heavily garbled math layout from the source PDF (a known, disclosed limitation of this book's text extraction at that specific page), and confirming it character-for-character against the rendered page image was judged out of budget for this chunk relative to Proposition 4.11 and Eq. (4.16), both of which are directly load-bearing in Theorem 4.10's own proof and extracted cleanly.

Selected references

M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 4.
M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991 (the symmetrization technique).
V. N. Vapnik and A. Y. Chervonenkis, "On the uniform convergence of relative frequencies of events to their probabilities," Theory of Probability and Its Applications, 16(2):264–280, 1971.

9 thms2 active usersReviewed

Operations Research Statistics Stochastic Systems·Captain: mikedeng1

Stochastic Orders III: The Convex Order and Strassen's Martingale CouplingTextbook

Comparing variability, not just location

Chapter I's usual stochastic order compares "how large" two random variables tend to be. A different, equally common question in operations research is "how spread out" a random variable is: two portfolios with the same expected loss can differ sharply in how much that loss varies, and a risk-averse decision maker or a convex cost function cares about exactly that difference. Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) formalizes this comparison as the convex order, the book's mean-preserving-spread order (known outside OR and probability circles as the Rothschild–Stiglitz order from economics). This mission formalizes the order and its central structural result: Strassen's martingale-coupling characterization.

The convex order

Let $X$ be a real-valued random variable on a probability space $(\Omega,\mu)$ , and let $Y$ be a real-valued random variable on a (possibly different) probability space $(\Omega',\nu)$ . $X$ is smaller than $Y$ in the convex order, written $X \le_{cx} Y$ , if

E[\varphi(X)] \le E[\varphi(Y)] \quad \text{for every convex } \varphi:\mathbb{R}\to\mathbb{R} \text{ for which the two expectations exist.}

Convex functions take their relatively largest values on the "extreme" regions outside some interval, so $X \le_{cx} Y$ says $Y$ is more likely than $X$ to take extreme values: $Y$ is "more variable" than $X$ . Unlike the usual stochastic order, $X \le_{cx} Y$ forces the two means to agree ( $E[X]=E[Y]$ , taking $\varphi(x)=\pm x$ , both convex) — the convex order compares spread holding location fixed, exactly the mean-preserving-spread reading. Two equivalent forms make it tractable: comparing tail integrals of the survival/distribution functions (Theorem 3.A.1), and comparing mean absolute deviations $E|X-a|$ from every point $a$ (Theorem 3.A.2).

Formalization targets

Goal: Strassen's martingale-coupling characterization (Theorem 3.A.4)

X \le_{cx} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ E[\hat Y\mid\hat X]=\hat X\text{ a.s.}

Furthermore, $\hat X,\hat Y$ can be chosen so that the conditional law $[\hat Y\mid\hat X=x]$ stochastically increases with $x$ (in $\le_{st}$ ). This is the convex-order analogue of Chapter I's Theorem 1.A.1: instead of one variable dominating the other pathwise, $Y$ 's copy is a fair (martingale) randomization of $X$ 's copy whose spread only grows in the conditioning value. The book itself calls the constructive direction "not easy to prove"; this mission states the theorem faithfully, including the "Furthermore" strengthening, without attempting a proof.

Supporting milestones

Theorem 3.A.1, the tail-integral characterizations: for $X,Y$ with $E[X]=E[Y]$ , $X\le_{cx}Y$ iff $\int_x^\infty\bar F(u)\,du\le\int_x^\infty\bar G(u)\,du$ for all $x$ , and iff $\int_{-\infty}^x F(u)\,du\le\int_{-\infty}^x G(u)\,du$ for all $x$ — the two integrated forms the book's own sketch of Theorem 3.A.4 uses.
Theorem 3.A.2, the absolute-deviation characterization: for $X,Y$ with $E[X]=E[Y]$ , $X\le_{cx}Y$ iff $E|X-a|\le E|Y-a|$ for every real $a$ .
Theorem 3.A.12(d), closure under convolution: independent $X_i\le_{cx}Y_i$ for $i=1,\dots,m$ gives $\sum_i X_i \le_{cx} \sum_i Y_i$ — the convex-order analogue of Chapter I's Theorem 1.A.3(b).

Significance

The convex order is the standard way operations research and actuarial science formalize "more variable, same average": comparing the riskiness of two portfolios with matched expected return, the effect of aggregation or diversification on total claim size, or the value of information in a stochastic program (where a random variable degenerates to its mean exactly when the decision maker learns everything, the two extremes of a convex-order chain). Strassen's characterization is what turns "compare against every convex function" — an intractable universal quantifier — into a single explicit construction: exhibit one martingale coupling and the comparison is settled for every convex function at once, by Jensen's inequality. This is the technique behind bounding the effect of information or risk aggregation without checking convexity function by function, and the "Furthermore" monotonicity clause is what makes the coupling itself informative about how the spread grows with the conditioning variable, not merely that some fair coupling exists.

Formalizing this theorem fixes, for the whole book series, the exact shape every later coupling theorem for a variability-type order (the increasing convex/concave orders of Chapter IV via a submartingale, the multivariate convex order of Chapter VII) is expected to restate. No proof is attempted; the book's own remark that the constructive direction is "not easy" marks it as a genuine target for a future proof-bearing pass, not a formality.

Difficulty

The definitional trap mirrors Chapter I's: "for every convex $\varphi$ " must be a genuine universal quantifier over Mathlib's own convexity predicate, with the existence of both expectations stated as an explicit integrability hypothesis inside the quantifier, not assumed globally or dropped. The coupling theorem doubles the difficulty of Theorem 1.A.1's: the conditional-expectation condition $E[\hat Y\mid\hat X]=\hat X$ a.s. is with respect to the $\sigma$ -algebra generated by $\hat X$ , not an informal "expected value given $\hat X$ ", and must use the martingale API's own convention (Mathlib's condExp) precisely. The "Furthermore" clause compounds this: it is a claim about the regular conditional distribution of $\hat Y$ given $\hat X=x$ for every point $x$ , not merely the conditional expectation, and dropping it silently (as a "remark" rather than part of the theorem) would understate what Theorem 3.A.4 actually claims — the chapter brief flags this explicitly as a trap, and it is kept as a conjunct of the same existential witness here.

Formalization scope

Random variables are again measurable functions into $\mathbb{R}$ from arbitrary measurable spaces, ConvexOrder μ ν X Y taking $X$ on $(\Omega,\mu)$ and $Y$ on a separate $(\Omega',\nu)$ , matching Chapter I's convention and this series' own pattern. Convexity is Mathlib's ConvexOn ℝ Set.univ φ; "equality in law" is again ProbabilityTheory.IdentDistrib. The martingale condition uses Mathlib's conditional-expectation notation ρ[Ŷ | m] =ᵐ[ρ] X̂ with m the $\sigma$ -algebra MeasurableSpace.comap X̂ inferInstance generated by X̂ — the martingale API's own convention, not a hand-rolled gloss. The "Furthermore" clause uses Mathlib's ProbabilityTheory.condDistrib, the regular conditional distribution kernel of Ŷ given X̂ (available since ℝ is a standard Borel space), and states "increasing in x in ≤st" via the kernel's survival function being monotone in x at every threshold — restating, locally to this chapter's namespace, the same tail-probability shape Chapter I's UsualOrder uses (drafts cannot import another mission's definitions, per this series' convention). A trivializing formalization is ruled out explicitly: the martingale and monotonicity conjuncts are both kept as genuine content of the existential witness in the goal theorem, not weakened to a bare coupling or dropped as an optional remark.

This mission draws on no platform prior art (searches for "convex order", "Strassen", "martingale", "Jensen" returned only unrelated geometry/algorithm/physics results as of 2026-09-18); Mathlib's Probability/Martingale/* supplies the conditional-expectation and kernel machinery the coupling condition and its "Furthermore" clause are built from, but no platform theorem states the convex order or its coupling characterization itself. Reusable beyond this mission: the condExp/condDistrib-based martingale-coupling pattern is the shape Chapter IV's analogous submartingale coupling (Theorem 4.A.5) and Chapter VII's multivariate convex order (Theorem 7.A.1) are each expected to restate independently.

Selected references

M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5
M. Rothschild and J. E. Stiglitz, "Increasing risk: I. A definition", Journal of Economic Theory, 2(3), 1970, 225–243. https://doi.org/10.1016/0022-0531(70)90038-4

6 thms2 active users

Machine Learning Statistics·Captain: mikedeng1

Support Vector Machines I: Zhang's Inequality Relating the Hinge Risk and the Classification RiskTextbook

Motivation

Binary classification asks for a rule that predicts a label $y \in \{-1,1\}$ from an observation $x$ . The natural loss for this task, the classification loss $L_{\mathrm{class}}$ , is a step function: minimizing its empirical average over a class of functions $f$ is generally NP-hard, because the objective is non-convex and discontinuous in $f$ . Every practical classification algorithm — logistic regression, boosting, and the support vector machine this book is about — sidesteps this by minimizing a convex surrogate loss instead, such as the hinge loss $L_{\mathrm{hinge}}(y,t) := \max\{0, 1-yt\}$ , and hoping that a small surrogate risk implies a small classification risk.

Zhang (2004) and Bartlett, Jordan & McAuliffe (2006) put this hope on a rigorous footing: for a wide class of convex surrogates, controlling the excess surrogate risk controls the excess classification risk, with an explicit quantitative relationship. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter 2, develop the special case of the hinge loss in closed form as Theorem 2.31 ("Zhang's inequality"), the sharpest and most self-contained instance of this calibration phenomenon: an exact equality for bounded functions, not merely an inequality.

Setting

Fix a measurable space $(X,\mathcal A)$ and a closed label set $Y \subset \mathbb R$ ; throughout this mission $Y := \{-1,1\}$ . A loss function is a measurable map $L : X \times Y \times \mathbb R \to [0,\infty)$ , read as the cost $L(x,y,f(x))$ of predicting $y$ by $f(x)$ when $x$ is observed. Given a distribution $P$ on $X \times Y$ , the $L$ -risk of a measurable $f : X \to \mathbb R$ is the average cost $R_{L,P}(f) := \int_{X\times Y} L(x,y,f(x))\,dP(x,y)$ , and the Bayes risk $R^*_{L,P} := \inf_f R_{L,P}(f)$ is the smallest risk any measurable function can achieve.

The classification loss is $L_{\mathrm{class}}(y,t) := \mathbf 1_{(-\infty,0]}(y \cdot \operatorname{sgn} t)$ — it charges $1$ exactly when the sign of the prediction $t$ disagrees with the label $y$ — where $\operatorname{sgn}$ is the sign function with the book's convention $\operatorname{sgn}(0):=1$ . The hinge loss is $L_{\mathrm{hinge}}(y,t) := \max\{0,1-yt\}$ , a convex, piecewise-linear upper bound on $L_{\mathrm{class}}$ up to a factor of $2$ . Writing $\eta(x) := P(y=1\mid x)$ for the conditional probability of the positive label given $x$ , the Bayes classification function is $f^*_{L_{\mathrm{class}},P}(x) := \operatorname{sgn}(2\eta(x)-1)$ : it predicts the majority label at $x$ .

A loss $L$ can be clipped at $M>0$ if truncating every prediction to $[-M,M]$ never increases the loss: $L(x,y,\widehat t) \le L(x,y,t)$ for the clipped value $\widehat t$ of $t$ . Both $L_{\mathrm{class}}$ and $L_{\mathrm{hinge}}$ can be clipped at $M=1$ .

Formalization targets

Goal: Zhang's inequality (Theorem 2.31)

R_{L_{\mathrm{hinge}},P}(f) - R^*_{L_{\mathrm{hinge}},P} = \int_X |f(x) - f^*_{L_{\mathrm{class}},P}(x)| \cdot |2\eta(x)-1| \, dP_X(x) \qquad (f : X \to [-1,1])

R_{L_{\mathrm{class}},P}(f) - R^*_{L_{\mathrm{class}},P} \;\le\; R_{L_{\mathrm{hinge}},P}(f) - R^*_{L_{\mathrm{hinge}},P} \qquad (f : X \to \mathbb R)

The first target is an exact identity for bounded predictors: the excess hinge risk equals a weighted $L^1$ distance to the Bayes classifier. The second, weaker but unrestricted, statement is what makes the hinge loss a valid classification surrogate for arbitrary real-valued scores: no matter how large $|f|$ grows, the excess classification risk it incurs is bounded by its excess hinge risk. Because the second statement is the one actually used downstream (Chapter 6's oracle inequality composes it with a bound on the excess hinge risk to bound the excess classification risk), it is the weakest stable form of the calibration claim and the natural target to keep in mind when judging whether a variant formalization is still faithful.

Significance

Zhang's inequality is the single fact that licenses every consistency and rate-of-convergence result for SVM classification in the rest of the book (flagged explicitly on p. 38: "we will show in Section 3.4 that the other margin-based losses ... are also reasonable surrogates," and reused directly, e.g., in Chapter 6's oracle inequality via its restatement as Theorem 6.24 in Chapter 6 of this series). Its role is entirely mechanical but load-bearing: every SVM consistency proof reduces to bounding an excess surrogate risk, and Theorem 2.31 is what converts that bound back into a statement about the classification error anyone actually cares about.

The result itself has been known since Zhang (2004) and Bartlett–Jordan–McAuliffe (2006) in more general form (arbitrary convex margin losses, with an explicit " $\psi$ -transform" relating excess risks); Theorem 2.31 is the closed-form hinge-loss instance, with the equality (not just an inequality) available because the hinge loss's clipped value is exactly linear in $\eta$ . No machine-checked proof of either the general or the hinge-specific statement is known to exist in a public Lean/Mathlib development at the time of writing (see prior-art search below); this mission asks for a formalization of the hinge-specific case exactly as the book states it.

Difficulty

The natural first attempt is to expand both risk differences directly as integrals over $P$ and compare integrands. This works for the equality (bounded $f$ ), because the hinge loss is piecewise linear in $t$ and the calculation collapses to the algebraic identity $1+f(x)(1-2\eta(x)) = |f(x)-f^*_{L_{\mathrm{class}},P}(x)|\cdot|2\eta(x)-1|$ once $f^*$ is spelled out by cases on the sign of $2\eta(x)-1$ . It fails for the inequality on unbounded $f$ : neither risk difference has a closed algebraic form once $f$ is allowed to leave $[-1,1]$ , and the excess classification risk itself is genuinely discontinuous in $f$ . The book's proof resolves this by clipping $f$ first (Lemma 2.23: clipping a convex loss at a minimizer's interval only decreases its risk) and observing the excess classification risk is invariant under clipping — this reduces the general case to the bounded case, at the cost of needing Lemma 2.23 as a genuine prerequisite rather than a routine remark. The remaining pointwise step (Lemma 2.30) is a case-by-case real-variable inequality with no probabilistic content of its own, but gets the boundary case $\eta = 1/2$ (equivalently $2\eta-1=0$ , where the book's sign convention $\operatorname{sgn}(0):=1$ is load-bearing) wrong if that convention is not tracked precisely.

Formalization scope

$X$ is an arbitrary measurable space; $Y$ is fixed to $\{-1,1\} \subset \mathbb R$ throughout. A loss is represented as a plain function Loss X := X → ℝ → ℝ → ℝ; nonnegativity and the restriction of the middle argument to $\{-1,1\}$ are supplied as explicit hypotheses at each use site rather than built into the type, since only some lemmas of the chapter need them (Lemma 2.23 needs neither). risk/bayesRisk are ordinary real-valued Bochner integrals/infima, not extended-real-valued as in the book; consequently every assertion that could otherwise degrade to a vacuous 0 - 0 from a non-integrable loss carries an explicit Integrable hypothesis on the relevant loss composed with $f$ — automatic in the book's own setting (bounded losses on a probability space) but not implied by the Lean types alone. $\eta(x) := P(y=1\mid x)$ is represented by its defining disintegration identity, $P(A\times\{1\}) = \int_{x\in A}\eta(x)\,dP_X(x)$ for every measurable $A \subseteq X$ , rather than via a general regular-conditional-probability construction — a specific, checkable representation of "the conditional probability of $y=1$ given $x$ " rather than a synonym for it.

A trivializing formalization would let $f^*_{L_{\mathrm{class}},P}$ or $\eta$ be an unconstrained hypothesis unconnected to $P$ and $L_{\mathrm{class}}$ (making the goal a tautology about whatever function is supplied); this is ruled out here by deriving $f^*_{L_{\mathrm{class}},P}$ from $\eta$ by the book's own formula $\operatorname{sgn}(2\eta-1)$ and constraining $\eta$ by the disintegration identity above, not taking either as a free unconstrained parameter.

Lemma 2.23, Lemma 2.30, L_class/L_hinge, risk/bayesRisk and CanBeClipped/clip are reusable beyond this mission: Lemma 2.23 and the risk/Bayes-risk vocabulary recur throughout the book (clippability is used again in Section 7.4 and, per this series' README, this chapter's Theorem 2.31 itself is restated inside Chapter 6's oracle inequality). Contributions completing the two milestone proofs and the goal's sorry are welcome; a from-scratch alternative proof avoiding Lemma 2.23 (e.g. by a direct case analysis on $f$ outside $[-1,1]$ ) would also be a valid solution to the goal, since the milestones are the book's own attack path, not a required lemma structure.

Selected references

I. Steinwart & A. Christmann, Support Vector Machines, Springer, Information Science and Statistics, 2008. https://doi.org/10.1007/978-0-387-77242-4 (Chapter 2, pp. 21-47).
T. Zhang, "Statistical behavior and consistency of classification methods based on convex risk minimization," Annals of Statistics 32(1), 2004, pp. 56-85. https://doi.org/10.1214/aos/1079120130
P. L. Bartlett, M. I. Jordan & J. D. McAuliffe, "Convexity, classification, and risk bounds," Journal of the American Statistical Association 101(473), 2006, pp. 138-156. https://doi.org/10.1198/016214505000000907

6 thms2 active users

Machine Learning Statistics Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning II: Rademacher Complexity and VC-DimensionTextbook

Motivation

Chapter 2's finite-hypothesis-set learning bound is uninformative the moment $H$ is infinite — $\log|H|$ diverges — yet most hypothesis sets used in practice (linear separators, neural networks, decision trees) are infinite. Chapter 3 answers the question the previous chapter's own worked example (axis-aligned rectangles, Example 2.4) leaves open: is efficient learning from a finite sample still possible for an infinite hypothesis set, and can this be shown in general rather than case by case? The chapter's answer runs through two complementary notions of complexity — Rademacher complexity, a data-dependent measure of how well a function family correlates with random noise, and the VC-dimension, a purely combinatorial measure of the number of distinct labelings a hypothesis set can realize on a finite point set — connected by Massart's lemma and Sauer's lemma, and culminating in a generalization bound that replaces $\log|H|$ with the VC-dimension $d$ .

Setting

For a family $G$ of functions $Z\to[0,1]$ and a sample $S=(z_1,\dots,z_m)$ , the empirical Rademacher complexity $\hat R_S(G) = \mathbb E_\sigma[\sup_{g\in G}\frac1m\sum_i\sigma_i g(z_i)]$ (Definition 3.1) measures how well $G$ fits random sign noise $\sigma$ on $S$ ; the Rademacher complexity $R_m(G) = \mathbb E_{S\sim D^m}[\hat R_S(G)]$ (Definition 3.2) averages this over samples. Theorem 3.3 converts a Rademacher-complexity bound directly into a generalization bound via McDiarmid's inequality. For binary hypothesis sets $H\subseteq(X\to\{-1,+1\})$ , the growth function $\Pi_H(m)$ (Definition 3.6) counts the maximum number of distinct dichotomies $H$ realizes on $m$ points, and the VC-dimension $\mathrm{VCdim}(H)$ (Definition 3.10) is the largest $m$ for which $\Pi_H(m)=2^m$ (i.e. $H$ shatters some set of $m$ points). Massart's lemma (Theorem 3.7) is the purely combinatorial tool bounding the expected maximum of a sum of signed vector components by $\sqrt{\log|A|}$ , and Sauer's lemma (Theorem 3.17) bounds the growth function itself, by induction on $m+d$ , whenever the VC-dimension is finite.

Formalization targets

Theorem 3.3 (Rademacher generalization bound, milestone). For $G:Z\to[0,1]$ and any $\delta>0$ , with probability at least $1-\delta$ over an i.i.d. sample $S$ of size $m$ , for all $g\in G$ : $\mathbb E[g(z)] \le \frac1m\sum_i g(z_i) + 2R_m(G) + \sqrt{\log(1/\delta)/(2m)}$ .

Theorem 3.7 (Massart's lemma, milestone). For a finite $A\subseteq\mathbb R^m$ with $r=\max_{x\in A}\|x\|_2$ : $\mathbb E_\sigma[\frac1m\sup_{x\in A}\sum_i\sigma_i x_i] \le r\sqrt{2\log|A|/m}$ .

Theorem 3.17 (Sauer's lemma, milestone). For $H$ with $\mathrm{VCdim}(H)=d$ , for all $m\in\mathbb N$ : $\Pi_H(m) \le \sum_{i=0}^d\binom{m}{i}$ .

Corollary 3.19 — the mission's goal. For $H\subseteq(X\to\{-1,+1\})$ with $\mathrm{VCdim}(H)=d$ and any $\delta>0$ , with probability at least $1-\delta$ , for all $h\in H$ :

R(h) \le \hat R_S(h) + \sqrt{\frac{2d\log(em/d)}{m}} + \sqrt{\frac{\log(1/\delta)}{2m}}.

Significance

Corollary 3.19 is the chapter's answer to the question chapter 2 leaves open: it is Theorem 2.13's direct infinite-hypothesis-set generalization, replacing $\log|H|$ (undefined for infinite $H$ ) with the VC-dimension $d$ (finite even for many infinite hypothesis sets, such as halfspaces in $\mathbb R^k$ , which have VC-dimension $k+1$ ). It is also the template every later margin bound in the book specializes (Chapters 5, 9, 10's SVM, multi-class and ranking margin bounds all replace this bound's uniform $\log|H|$ /VC-dimension term with a scale-sensitive complexity measure derived from the same Rademacher-complexity machinery), and Sauer's lemma is independently one of the most cited results in learning theory and extremal combinatorics. No prior art on the Prove2Me platform is faithful to any of this chapter's content: RademacherSymmetrization.radS_chernoff (Aether Catalog) proves a different, Massart-optimized Chernoff bound for the empirical Rademacher complexity of a finite class — a different object (empirical vs. population) with a different bound form from Theorem 3.3/3.5 — and sauerShelah_full proves only the trivial identity sauerShelahBound k k = 2^k, not Sauer's lemma itself. A further hit, sauer_shelah (Aether Catalog, Algebra/SauerShelah.lean), does state the Sauer-Shelah bound itself (F.card ≤ ∑_{i≤d} C(n,i) for a family F of subsets of Fin n shattering no set larger than d) — checked and not reused: it is a different idiom from Theorem 3.17 as this chunk needs it, a fixed finite ambient domain Fin n with F a Finset of its subsets directly, rather than the book's own growth function Π_H(m) (a supremum over point-tuples drawn from an arbitrary, possibly infinite X, Definition 3.6) that this chunk's other items and the goal (Corollary 3.19) are built on; reusing it would require either abandoning GrowthFunction/HasVCDim (needed faithfully by the goal itself) or a nontrivial reduction lemma this mission's budget does not include, so sauer_lemma is drafted fresh against this chunk's own GrowthFunction/HasVCDim. All ten items are drafted fresh.

Difficulty

Sauer's lemma's proof is a genuine two-parameter induction (on $m+d$ ) with a real combinatorial construction: restricting $H$ to a sample $S$ of size $m$ , then splitting the restricted family into $G_1$ (its restriction to the first $m-1$ points) and $G_2$ (the concepts whose membership in $G$ changes with the addition of the $m$ -th point), with $|G_1|+|G_2|=|G|$ and $\mathrm{VCdim}(G_2) \le \mathrm{VCdim}(G)-1$ — a genuinely combinatorial argument, not a statement that unfolds by simp; a weaker restatement using only the trivial bound $\Pi_H(m)\le 2^d$ would be true but is explicitly not what Theorem 3.17 states (BRIEF.md's named trivializing formalization for this chapter). Massart's lemma needs the expectation of a supremum over a finite set of $2^m$ -many sign patterns kept as an honest average, not silently replaced by a looser union bound. Corollary 3.19's own $em/d$ term inside the logarithm needs the side condition $d\le m$ carried through explicitly — Corollary 3.18's own domain restricts to $m\ge d$ , and the bound is false, not merely unproved, without it (at $m<d$ , $em/d$ can be smaller than $1$ , making the logarithm negative).

Formalization scope

GeneralizationError/EmpiricalError are restated locally in this chunk's RademacherVC namespace (byte-identical in content to chunk 02-pac's own copies), since a draft item cannot import another chunk's draft module; this duplication is expected and will collapse once 02-pac is moderated, uploaded and listed as reusable in missions/README.md's "Published definitions" table. EmpiricalRademacherComplexity/Massart's lemma model the Rademacher signs σ as ranging over the finite type Fin m → Bool rather than a measure-theoretic i.i.d. process, so the "expectation over σ" in both is the exact finite uniform average over its 2^m outcomes — faithful and simpler than a MeasureTheory construction, since σ's distribution really is uniform on a finite set of outcomes for every finite m. GrowthFunction takes a tuple of m points (Fin m → X) rather than a size-m subset of X, a harmless generalization (repeated points never increase the dichotomy count) documented in the item's own docstring. HasVCDim is a Prop parametrized by the candidate dimension rather than a total ℕ/ℕ∞-valued function, so it does not cover the book's VCdim(H)=+\infty case (Examples 3.15-3.16); every theorem using it takes HasVCDim H d as an explicit hypothesis, matching the book's own "let H... with VCdim(H)=d." Theorem 3.3 adds an explicit measurability hypothesis on G (hGm) beyond the book's own displayed statement, needed to keep the Bochner integral ∫ z, g z ∂D from silently evaluating to 0 for a non-measurable g — this is the book's own standing assumption (footnote 3, p. 30) made an explicit hypothesis rather than an implicit one. No numerical constant in any of the four theorems is altered from the book's own; Corollary 3.19's side condition d ≤ m is kept explicit, per BRIEF.md's pitfall note.

Not formalized: Lemma 3.4 and Theorem 3.5 (the binary-classification specialization of Theorem 3.3 via the zero-one-loss identity $\hat R_S(G)=\frac12\hat R_{S_X}(H)$ ), Corollary 3.8 and Corollary 3.9 (the intermediate Rademacher-to-growth-function and growth-function generalization bounds), and Corollary 3.18 (the VC-dimension bound on the growth function, $\Pi_H(m)\le(em/d)^d$ for $m\ge d$ ) — five intermediate results in the proof chain Theorem 3.3 → Theorem 3.5 → Corollary 3.8/3.9 → Sauer's lemma → Corollary 3.18 → Corollary 3.19 that are not independently drafted as milestones, per the budget guidance to keep a chunk to a goal plus its most load-bearing 3-8 milestones rather than every numbered result on the page; the three drafted milestones (Theorem 3.3, Massart's lemma, Sauer's lemma) are the chain's three genuinely distinct proof techniques (McDiarmid's inequality, a probabilistic-maximum bound, and a combinatorial induction), and the goal theorem's own statement is Corollary 3.19 exactly as displayed, not a restatement of any intermediate corollary. Radon's theorem (Theorem 3.13, background for the hyperplane VC-dimension example) and the worked VC-dimension examples (intervals, hyperplanes, rectangles, convex polygons, sine functions) are illustrations, not general results, and are not formalized — drafting only the example computations (e.g. VCdim(hyperplanes) = d+1) instead of the general finite-H machinery is exactly the trivializing formalization this mission avoids.

Selected references

M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 3.
V. Vapnik, A. Chervonenkis, "On the uniform convergence of relative frequencies of events to their probabilities," Theory of Probability and its Applications 16(2), 1971, 264-280.
N. Sauer, "On the density of families of sets," Journal of Combinatorial Theory, Series A 13(1), 1972, 145-147.

12 thms2 active users

Machine Learning Statistics Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning I: The PAC Learning FrameworkTextbook

Motivation

How many labeled examples does a learning algorithm need to see before its output generalizes well to unseen data? Chapter 2 of Foundations of Machine Learning answers this question for the simplest nontrivial setting — a finite hypothesis set — and in doing so introduces the book's central object, the Probably Approximately Correct (PAC) learning framework: a distribution-free, high-probability guarantee relating a learner's sample size to the accuracy and confidence of its output. Every later chapter's generalization bound (VC-based, Rademacher-based, margin-based) is a variant of the same "probability of a bad event is small" argument this chapter proves in its most elementary form, so getting the chapter's core definitions and its two bracketing theorems (consistent and inconsistent finite- $H$ ) right is the foundation the rest of the book's guarantees build on.

Setting

A learner sees a sample $S = (x_1,\dots,x_m)$ drawn i.i.d. from a fixed but unknown distribution $D$ on an instance space $X$ , labeled by an unknown target concept $c$ drawn from a concept class $C$ ; a hypothesis $h$ from a fixed hypothesis set $H$ is judged by its generalization error $R(h) = \Pr_{x\sim D}[h(x)\ne c(x)]$ (Definition 2.1) against its empirical error $\hat R_S(h) = \frac1m\sum_i \mathbb 1_{h(x_i)\ne c(x_i)}$ (Definition 2.2) on the observed sample. A concept class is PAC-learnable (Definition 2.3) if some algorithm, given a polynomially-bounded number of samples, returns a hypothesis whose generalization error is at most $\epsilon$ with probability at least $1-\delta$ , for every accuracy $\epsilon$ and confidence $\delta$ and every distribution $D$ — the "distribution-free" and "for all target concepts" character of the definition is what makes it a genuine worst-case learning guarantee rather than an average-case one tailored to a particular data-generating process.

Formalization targets

Theorem 2.5 (consistent case, milestone). If $H$ is finite and algorithm $A$ always returns a hypothesis consistent with the target concept on the training sample ( $\hat R_S(h_S)=0$ ), then $\Pr_{S\sim D^m}[R(h_S)\le\epsilon]\ge1-\delta$ whenever $m \ge \frac1\epsilon(\log|H|+\log\frac1\delta)$ .

Corollary 2.11 (single-hypothesis Hoeffding bound, milestone). For a fixed hypothesis $h:X\to\{0,1\}$ and any $\delta>0$ , with probability at least $1-\delta$ , $R(h) \le \hat R_S(h) + \sqrt{\log(2/\delta)/(2m)}$ .

Theorem 2.13 (inconsistent case, goal). For a finite hypothesis set $H$ and any $\delta>0$ , with probability at least $1-\delta$ , simultaneously for every $h\in H$ ,

R(h) \le \hat R_S(h) + \sqrt{\frac{\log|H|+\log(2/\delta)}{2m}}.

Significance

Theorem 2.13 is the chapter's capstone because it removes Theorem 2.5's consistency requirement — the typical case in practice, where no hypothesis in $H$ perfectly fits the training data — while paying only an additive $\log|H|$ price inside the square root, via a union bound over $H$ applied to Corollary 2.11's per-hypothesis concentration bound. It is also the template every later generalization bound in the book refines: Chapter 3 replaces $\log|H|$ with the growth function / VC-dimension to handle infinite hypothesis sets, and Chapter 3's Rademacher-complexity bound is the direct machine-independent generalization of the same argument. No prior art on the Prove2Me platform is faithful to this chapter's PAC-learning content (GET /theorems?q=PAC-learnable returns no hits), so all six items are drafted fresh.

Difficulty

Theorem 2.13's own proof is a short combination of two ideas already present in the chapter (Corollary 2.11's Hoeffding bound plus a union bound over $|H|$ hypotheses), but each ingredient carries its own faithfulness burden. Corollary 2.11 needs the sample $S$ and the target hypothesis $h$ kept in the right relationship — $h$ fixed, $S$ random — for the bound to be Hoeffding's inequality and not a vacuous statement about a random hypothesis. Theorem 2.13 needs the $\forall h\in H$ quantifier placed inside the probability event (a single sample $S$ must work for every $h$ at once), not outside it (which would only assert each $h$ 's bound holds with high probability for a sample chosen depending on $h$ ) — the difference between a uniform convergence bound and $|H|$ separate, weaker statements. Definition 2.3's "polynomial function $\mathrm{poly}(\cdot,\cdot,\cdot,\cdot)$ " is a genuine formalization judgment call, addressed below.

Formalization scope

GeneralizationError/EmpiricalError are typed generally over $X, Y$ (matching Definition 2.1/2.2's own general statement, " $h : X\to Y$ "), since Theorem 2.5 itself is stated for general $Y$ , not just $Y=\mathrm{Bool}$ ; Corollary 2.11 and Theorem 2.13 specialize to $h : X\to\mathrm{Bool}$ , matching their own explicit " $h:X\to\{0,1\}$ " (Corollary 2.11) and the surrounding inconsistent-case section's restriction to binary classification. The i.i.d. sample $S\sim D^m$ is modeled as the identity random variable on the product-measure space $(\mathrm{Fin}\ m \to X,\ \mathrm{Measure.pi}(\lambda\_.\ D))$ in both Corollary 2.11 and Theorem 2.13, matching the book's own $S\sim D^m$ notation exactly. IsPACLearnable (Definition 2.3) makes "polynomial function" precise as a function bounded above by $K\cdot(a+b+n+s+1)^k$ for some constants $K>0$ , $k\in\mathbb N$ , uniform in its (nonnegative) arguments — the standard reading of "polynomial in its arguments" in the absence of a ready-made multivariate polynomial-growth predicate in Mathlib; dropping this constraint entirely (stating only "there is some threshold function") would silently weaken Definition 2.3 to a strictly easier notion of learnability, since virtually any finite or well-behaved concept class admits some (possibly super-polynomial) sample-complexity threshold — this is exactly the distinction Example 2.7 (the universal concept class) uses to demonstrate a class that is not PAC-learnable despite admitting a consistent hypothesis set. No numerical constant in Theorem 2.5, Corollary 2.11 or Theorem 2.13 is altered from the book's own; no upper bound on $\delta$ is added anywhere the book itself leaves it unrestricted (the theorems remain true, if vacuous, for $\delta>1$ ). Not formalized: the "efficiently PAC-learnable" running-time clause of Definition 2.3 (a second, independent polynomial-time condition on $A$ not needed by either milestone or the goal); Corollary 2.10 (the raw two-sided Hoeffding statement Corollary 2.11 is immediately derived from by solving for $\epsilon$ , making it redundant with Corollary 2.11 as a formalization target); the axis-aligned-rectangles worked example (Example 2.4–2.9), which illustrates the framework rather than proving a new general result, and the trivializing formalization this chapter invites — reusing Mathlib's rectangle machinery to encode only the specific two-dimensional geometric argument rather than the general finite- $H$ theorems — is exactly what this mission avoids by drafting Theorems 2.5 and 2.13 in their general, hypothesis-set-agnostic form.

Selected references

M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 2.
W. Hoeffding, "Probability inequalities for sums of bounded random variables," Journal of the American Statistical Association 58(301), 1963, 13-30.

9 thms2 active users

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Introduction to Stochastic Programming IV: Nested Decomposition for Multistage ProgramsTextbook

Motivation

Sequential planning problems — inventory replenishment, hydro-thermal power scheduling, asset-liability management — routinely span more than two decision epochs, with information about the future revealed gradually as each period unfolds. A two-stage recourse model (decide now, observe once, recourse once) is too coarse for these: it either collapses the whole horizon into a single "wait and see" observation or forces an ad-hoc rolling-horizon heuristic with no optimality guarantee. The multistage stochastic program is the natural model that keeps the full sequence of decisions and observations, and Benders (L-shaped) decomposition is the workhorse algorithm the field has used to solve it since Van Slyke and Wets [1969] introduced it for the two-stage case. Ho and Manne [1974] and Glassey [1973] first proposed nested decomposition for deterministic multistage models; Louveaux [1980] extended it to multistage quadratic stochastic programs, and Birge [1985] gave the linear multistage generalization this mission formalizes, later implemented at scale by Pereira and Pinto [1985] and Gassmann [1990] and still the basis of production stochastic-programming solvers today.

Setting

A multistage stochastic linear program unfolds over $H$ stages $t = 1,\dots,H$ . At each stage, uncertainty resolves into one of finitely many realizations, so the whole process of realizations forms a scenario tree: a single scenario at $t=1$ (the root), branching into finitely many scenarios at $t=2$ , each of those again branching at $t=3$ , and so on. Write $k$ for a scenario (a tree node) and $a(k)$ for its ancestor, the scenario at stage $t-1$ that $k$ descends from; $D^{t+1}(j)$ is the set of scenario $j$ 's descendants at the next stage. Each scenario $k$ at stage $t$ carries its own decision vector $x^t_k \ge 0$ , bounded above ( $x^t_k \le u^t_k$ , coordinatewise), subject to the linear constraint

W^t x^t_k = h^t_k - T^{t-1}_k x^{t-1}_{a(k)},

where the recourse matrix $W^t$ depends only on the stage (fixed recourse) while the transition matrix $T^{t-1}_k$ and right-hand side $h^t_k$ may vary scenario by scenario. Stacking every scenario's constraint over the whole tree gives the deterministic equivalent linear program, minimizing the probability-weighted total cost $\sum_k p_k (c^t_k)^\top x^t_k$ over this feasible region — problem (3.4.1) in the source.

The nested L-shaped method solves (3.4.1) by decomposition rather than forming this (typically enormous) single LP directly. Each scenario $k$ owns a small subproblem, $\mathrm{NLDS}(t,k)$ , that looks exactly like a two-stage L-shaped subproblem: it has $k$ 's own constraint and bound, plus a running set of feasibility cuts and optimality cuts accumulated so far, plus, if $k$ has descendants, an approximation variable $\theta^t_k$ standing in for the (unknown, convex, piecewise-linear) future cost $Q^{t+1}_k$ of everything downstream of $k$ . Solving $\mathrm{NLDS}(t,k)$ either finds it infeasible — in which case a feasibility cut is derived from the infeasibility certificate and sent up to $k$ 's parent — or finds an optimal dual solution, whose aggregate over all of $j$ 's children (weighted by conditional probability) becomes a candidate optimality cut for $j = a(k)$ . The method sweeps forward and backward across the tree, feasibility and optimality cuts accumulating at every internal node, until no node's subproblem produces a fresh cut.

Formalization targets

Goal (Chapter 6, Theorem 1)

\text{if every }\Xi_t\text{ is finite and every }x_t\text{ has a finite upper bound, then the nested L-shaped method}

\text{converges finitely to an optimal solution of the deterministic equivalent (3.4.1), or correctly certifies its infeasibility.}

This is the chapter's only numbered result and the weakest faithful statement of "the method works": it makes no claim about the number of iterations beyond finiteness, and none about which sequencing protocol (forward-forward-back, or any other) is used to choose which subproblem to solve next.

Significance

Finite convergence is what separates an algorithm from a heuristic: without it, nothing rules out an infinite sequence of ever-finer cuts that never certifies optimality or infeasibility. Birge's 1985 result is the reason nested Benders decomposition can be used as an exact method rather than an approximation, and every later refinement (bunching, sifting, multicuts, parallel implementations, all mentioned in the source text) modifies how cuts are generated or which subproblem is solved next without touching this finiteness guarantee — they are all still instances of the same cut-generation mechanism this mission formalizes. The two-stage case (Chapter 5, Theorem 2) is the $H=2$ special case of this theorem; the mission's tree-indexed state and transition relation are written to specialize to the two-stage development directly when the tree has one branching level, though the two developments are not connected by an import (see Formalization scope). No machine-checked proof of either the two-stage or multistage case appears to exist prior to this series; formalizing it here produces the first Lean statement of the mechanism nested Benders decomposition rests on.

Difficulty

The obvious first idea — prove finiteness by bounding the total number of cuts a node can ever receive, the way a flat scenario set bounds the two-stage method's cut count by its number of LP bases — fails because a node's own subproblem is not a fixed-size LP: every cut recorded at node $k$ becomes a new row of $k$ 's own constraint set, so the "number of possible bases" at $k$ keeps changing as the algorithm runs, and the bound at $k$ depends recursively on how many cuts $k$ 's own children could ever produce. The book's actual argument (p. 290) is a genuine induction on the stage index, from the last stage backward: assume the bound holds for every node at stage $t+1$ , then combinatorially bound the finite number of extended bases at stage $t$ that this permits, then take the finite union over every possible extension size. This mission's Lean development commits to a scope that keeps a node's basis a fixed-size object (see below) rather than re-deriving that combinatorial bound.

Formalization scope

Every stage shares one decision dimension $n$ and one constraint dimension $m$ (Fin n, Fin m); the book allows these to vary by stage but nothing in Theorem 1's statement needs that generality. Scenario probabilities p are the unconditional probability of reaching a node, required strictly positive and summing to $1$ within each stage (Instance.hp_pos, Instance.hp_sum); the aggregation formulas use only the ratio $p_k/p_j$ for $k$ a child of $j$ , which reads the same whether p is unconditional or conditional, so this is a normalization choice, not a substantive restriction. The upper bound ub is ℝ-valued rather than extended-real-valued, which is Theorem 1's own hypothesis ("finite upper bounds"), not an added convention.

The one deliberate scope-narrowing choice, flagged here and in MODERATION_NOTES.md, and strengthened in this revision after moderator review (2026-09-19, CHANGES_REQUESTED.md #2): a node $k$ 's dual witness (Basis, FeasBasis) is read off $k$ 's original constraint (1.2) alone — the fixed-size recourse matrix $W^{\mathrm{stage}(k)}$ — never off the extended constraint set (1.2)-(1.4). The gap this leaves is broader than "accumulated cuts are ignored": $k$ 's own continuation variable $\theta_k$ — present in (1.1)'s objective, and fixed to $0$ from Step 0 onward, not merely absent until cuts accumulate — has no representation at all in Basis, multiplier, basisValue, or the optimality-cut coefficients optCutCoeffs computes for a parent $j$ of $k$ . Consequently, whenever a child $k$ used in an optimality cut is itself an interior node ( $k$ has children of its own, i.e. $\mathrm{stage}(k) < H-1$ , which happens for every $H \geq 3$ tree), the mechanized cut coefficients are not the book's $(E^{t-1}_j, e^{t-1}_j)$ of Eq. (1.1) and are not the printed algorithm's mechanism at that node — they are the dual of $k$ 's plain sub-LP alone, omitting $k$ 's own contribution to the recourse value entirely, not only the portion contributed by $k$ 's accumulated cuts. This gap is inert exactly when every child aggregated in a cut is a last-stage node ( $H \le 2$ , where the mechanism coincides with the already-published two-stage sibling 05-two-stage-methods) and active for every deeper cut, which is most of what a general Tree H actually exercises. Concretely: as mechanized, the optimality-cut half of Step (Bases.optCutCoeffs, Step.opt) is faithful to the printed nested L-shaped method's cut-generation step only when every child it aggregates over is a last-stage node; for an interior child it computes a value that omits that child's own $\theta$ term rather than the book's recursive one. The feasibility-cut half (Bases.feasCutCoeffs, Step.feas) has no such gap — feasibility does not involve $\theta$ at any stage — and the tree/instance layer (Tree, Instance) and the goal theorem's own outer shape are unaffected: thm1_finite_convergence's statement (existence of a finite, Step-reachable state that is infeasible-certified or globally optimal) is not weakened, but the reader should treat the mechanized Step relation itself, for H ≥ 3, as a documented variant of Steps 1-2 rather than a literal transcription of them at every node — see STATUS.md's Revision section for the moderator exchange this responds to. Reworking cut generation to consume each child's own current $(x_k, \theta_k)$ witness directly, so that an interior child's continuation value is no longer dropped, is left to a future revision; it is a materially larger change (the child's local optimum is then piecewise-linear rather than linear in its own parent's decision, so the duality argument needs a genuinely different — not merely extended — basis notion) than this session's time budget allows. This keeps every basis type a fixed-size Fin m → Fin n object, exactly as in the two-stage method, and keeps the algorithm's finite-step bound an explicit, provable cardinality (|Node × FeasBasis| + |Node → Basis|) rather than the book's own implicit, recursively-defined one. The trivializing formalization this scope choice must not fall into — declaring victory by proving the plain two-stage case is what convergence "reduces to" without ever quantifying over the tree — is avoided because every definition and the goal statement itself are stated for a general Tree H with unrestricted branching, not merely $H = 2$ ; what is disclosed above is a gap in how faithfully Step models the book's own cut-generation mechanism at depth, not a restriction of the statement to $H = 2$ .

Reusable beyond this mission: Def_StochasticProg_Multistage_Tree (the finite scenario tree) is a natural building block for 07-integer-programs (an integer restriction of the same two-stage subproblem) and 10-multistage-approximations (multistage Jensen bounds, which need the same tree). Contributions welcome: a faithful account of the extended-basis induction sketched above, and a formalization of Chapter 6, Theorem 3 (finite termination of the quadratic nested decomposition of Section 6.2), which this mission omits for time (see STATUS.md).

Selected references

J.R. Birge, "Decomposition and Partitioning Methods for Multistage Stochastic Linear Programs", Operations Research 33(5), 1985.
R.M. Van Slyke, R. Wets, "L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming", SIAM Journal on Applied Mathematics 17(4), 1969. https://doi.org/10.1137/0117061
H.I. Gassmann, "MSLiP: A Computer Code for the Multistage Stochastic Linear Programming Problem", Mathematical Programming 47, 1990. https://doi.org/10.1007/BF01580858
M.V.F. Pereira, L.M.V.G. Pinto, "Stochastic Optimization of a Multireservoir Hydroelectric System: A Decomposition Approach", Water Resources Research 21(6), 1985. https://doi.org/10.1029/WR021i006p00779
J.R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, 2011. https://doi.org/10.1007/978-1-4614-0237-4

6 thms2 active users

Completed

Mathematical Physics·Captain: lisamegawatts

Finite Reflection Positivity Methods II: Split-Gibbs Normalization and ClosureTextbook

Motivation

Reflection positivity turns a factorized weight across a reflection plane into a positive-semidefinite kernel of observables. The first mission in this series certified that finite split-weight mechanism and its two-observable chessboard inequality. A physical finite-volume Gibbs model needs one more layer before it can consume those results: its unnormalized weight must have a strictly positive partition function, normalization must preserve the split representation, and the hypotheses used for probability normalization must not be confused with those used for reflection positivity.

This mission isolates that finite algebraic layer. It does not present the results as new mathematics; its purpose is to make the interfaces and their failure modes explicit enough for later clock and XY consumers.

Setting

Let $X$ be a finite half-configuration space and let a full configuration be $(x,y)\in X\times X$ . A split weight is

W(x,y)=\sum_{a\in A}c_a\phi_a(x)\phi_a(y),

where $A$ is finite, $c_a\in\mathbb R$ , and $\phi_a:X\to\mathbb R$ . Its partition function and normalized weight are

Z=\sum_{x,y\in X}W(x,y),\qquad \widehat W(x,y)=\frac{W(x,y)}{Z}.

For observables $F_i:X\to\mathbb R$ , define the reflected kernel

K_{ij}=\sum_{x,y\in X}\widehat W(x,y)F_i(x)F_j(y).

Positive semidefiniteness means symmetry together with nonnegativity of every real quadratic form.

Formalization targets

The mission keeps two logically independent requirements visible. Nonnegative split coefficients $c_a\ge0$ give reflection positivity through a weighted Gram factorization. Pointwise nonnegativity $W(x,y)\ge0$ , together with one strictly positive value, gives $Z>0$ and probability normalization. Neither requirement is silently substituted for the other.

The positive targets prove:

finite normalization of a nonnegative, nonzero weight;
closure of split data under common half-factors;
closure of split data under pointwise products;
preservation of reflection positivity under division by $Z>0$ ; and
the combined probability, PSD-kernel, and chessboard conclusions

K_{ij}^{2}\le K_{ii}K_{jj}.

Two controls freeze the boundary. The symmetric two-point matrix with diagonal $1$ and off-diagonal $2$ is pointwise positive and normalizes to a probability weight, but its raw and normalized delta-observable kernels are not PSD. Conversely, zero split data have nonnegative coefficients and PSD raw kernels, but $Z=0$ and their formally normalized weight is not a probability weight.

Significance

The result is a reusable adapter between an unnormalized finite Gibbs factorization and the previously certified reflection-positive kernel API. It prevents a later model proof from treating pointwise positivity as if it were a Gram representation, or treating reflection positivity as if it guaranteed a nonzero normalizer. The next physical consumer can therefore focus on proving an explicit nonnegative factorization of its cross-plane Boltzmann weight.

Scope

All types and sums used for normalization and kernels are finite, and all weights, coefficients, features, observables, and matrices are real. The mission proves no clock- or XY-specific Gibbs factorization, no spectral or Gaussian-domination theorem, no thermodynamic limit, and no Kosterlitz--Thouless conclusion. Those require separate missions. Physical $R1$ and $G1$ are not conclusions here.

References

J. Fröhlich, R. Israel, E. H. Lieb, and B. Simon, Phase transitions and reflection positivity. I. General theory and long range lattice models, Communications in Mathematical Physics 62 (1978), 1--34. https://doi.org/10.1007/BF01940327
Prove2Me mission Finite Reflection Positivity Methods I: Split Weights and Infrared Modes, mission db962332-7a71-4d34-a01c-e85cdee243ce.
LeanProofs, ReflectionPositivityInfraredBound.lean, repository snapshot dbf503b2909cc17787d40a21eb75a0c9354cc6ef: https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.lean

12 thms2 active usersReviewed

Completed

Markov Chain Stochastic Systems·Captain: naimengye

Introduction to Stochastic Networks II: Kolmogorov's Criterion for ReversibilityTextbook

Motivation

A Markov process is reversible when, in equilibrium, transitions from $x$ to $y$ occur at the same average rate as transitions from $y$ to $x$ . Algebraically this is the detailed balance condition $\pi(x)q(x,y)=\pi(y)q(y,x)$ , and it is the single most useful structural property a network process can have: it replaces a global linear system by one equation per pair of states, and it hands you the equilibrium measure as a product of rate ratios rather than as the solution of anything.

The catch is that detailed balance mentions $\pi$ , which is exactly what one is trying to find. Chapter 2 of Richard Serfozo's Introduction to Stochastic Networks (Springer, 1999) removes the circularity. Kolmogorov's criterion characterizes reversibility by a condition on the rates alone: around every closed path, the product of the forward rates equals the product of the backward rates. And the proof is constructive — once the criterion holds, the invariant measure is

\pi(x)=\prod_{i=1}^{n}\frac{q(x_{i-1},x_i)}{q(x_i,x_{i-1})}

along any path from a fixed origin $x^0$ to $x$ , the criterion being precisely what makes the answer independent of the path chosen.

Setting

$q(x,y)$ is a non-negative rate function on a state space $\mathbb E$ , with the two-way communication property that $q(x,y)$ and $q(y,x)$ are positive together — a process failing this is visibly not reversible, since some transition would be possible but its reverse would not. A path $x_0,\dots,x_n$ is a sequence with $q(x_{i-1},x_i)>0$ throughout, and $q$ is assumed irreducible: every state is reachable from every other along a path. Write $\rho(x,y)=q(x,y)/q(y,x)$ for the rate ratio.

$q$ is reversible when some positive $\pi$ satisfies the detailed balance equations. Such a $\pi$ is automatically an invariant measure, the total balance equations being the sum of the detailed ones.

Formalization targets

Goal — Theorem 2.8, Kolmogorov's criterion and the canonical measure

Three statements are equivalent:

$q$ is reversible;
(Kolmogorov's criterion) for every closed sequence $x_0,\dots,x_n=x_0$ ,

\prod_{i=1}^{n}q(x_{i-1},x_i)=\prod_{i=1}^{n}q(x_i,x_{i-1});

for every path, $\prod_{i=1}^n\rho(x_{i-1},x_i)$ depends on the path only through its endpoints.

And when they hold, fixing any origin $x^0$ there is a positive $\pi$ with $\pi(x^0)=1$ satisfying detailed balance and given at every state by the product of ratios along any path from $x^0$ .

Supporting levels

The canonical form (2.2), that $q$ is reversible with respect to $\pi$ exactly when $q(x,y)=\gamma(x,y)/\pi(x)$ for a symmetric non-negative $\gamma$ ; Example 2.1, the birth–death process with $\pi(x)=\prod_{n=1}^{x}\lambda(n-1)/\mu(n)$ ; Theorem 2.2, that a process whose communication graph is a tree is reversible; and Theorem 2.5, the time-reversal criterion, which identifies a stationary distribution from a candidate reversed rate function without mentioning reversibility at all.

Significance

The results themselves. Kolmogorov's criterion is the working test. It is how one checks that a birth–death process, a random walk on a tree, a reversible Jackson network or a Whittle network with reversible routing is reversible, and it is a finite check on cycles rather than a search for an unknown measure. The ratio form (iii) is what gets used in practice: it says the product of ratios along a path is a well-defined function of the endpoints, which is exactly what licenses defining $\pi$ by that product.

Theorem 2.2 is the structural special case with no computation at all — a tree has no cycles, so the criterion is vacuous and reversibility is automatic. Theorem 2.5 points in a different direction: it identifies a stationary distribution from a guess at the time-reversed rates, and it is the tool Serfozo uses later to prove the Whittle equilibrium theorem a second way and to establish that departure processes from networks are Poisson.

Formalizing them. Mathlib has no reversibility theory for Markov processes: no detailed balance, no Kolmogorov criterion, no time reversal of a rate function. It has SimpleGraph.IsTree, which the tree item uses, and nothing else that bears on this chapter. The whole apparatus is contributed here.

Difficulty

The goal is a genuine equivalence with a constructive core, and the three implications are of quite different character.

(i) $\Rightarrow$ (ii) is the easy one: multiply the detailed balance equations around the closed path and cancel the $\pi$ 's, which is legitimate because the $\pi$ values are positive. Note the criterion is asserted for arbitrary closed sequences, not only for paths; the two-way property is what makes both sides vanish together when some rate is zero.

(ii) $\Leftrightarrow$ (iii) is a cycle-splicing argument: two paths with the same endpoints concatenate, one reversed, into a closed path, and the criterion says its forward and backward products agree, which is the equality of ratio products.

(ii) $\Rightarrow$ (i) is where the construction lives. Fix an origin $x^0$ ; irreducibility gives a path to every state; define $\pi$ by the ratio product; (iii) makes it well defined; and then detailed balance at an edge follows by extending a path by that edge. Serfozo's Remark 2.9 gives the same construction as a recursion over the sets $\mathbb E_n$ of states reachable in $n$ steps, which may be the easier route to organize.

The birth–death item is a telescoping recursion, $\pi(x+1)\mu(x+1)=\pi(x)\lambda(x)$ , and the observation that the two families of detailed balance equations — for $y=x+1$ and for $y=x-1$ — are the same family. Theorem 2.2 is a cut argument: removing an edge of a tree splits the state space into two pieces joined by that edge alone, so the flow balance across the cut is the detailed balance equation for that edge. Theorem 2.5 is two lines of rearrangement once the sums are known to converge.

Formalization scope

The state space is an arbitrary type and $q$ is an arbitrary non-negative real rate function; nothing here needs a process, a measure space or even countability, because reversibility as Serfozo defines it "applies to any nonnegative rates or probabilities as an algebraic property, not necessarily associated with a stochastic process". The same statements therefore cover discrete-time chains with $q$ read as transition probabilities, which is what the book points out.

Paths are functions $\{0,\dots,n\}\to\mathbb E$ with positive consecutive rates. A path of length zero is a single state and its ratio product is the empty product $1$ , which is consistent with $\pi(x^0)=1$ .

Kolmogorov's criterion is stated for arbitrary closed sequences, exactly as the book states it, not only for closed paths. Under two-way communication the two readings agree — if one rate in the sequence vanishes then so does its reverse and both products are zero — but the book's form is the one that is directly checkable.

The canonical measure is not defined by a choice function. Instead the conclusion asserts the existence of a positive $\pi$ with $\pi(x^0)=1$ satisfying detailed balance and agreeing with the ratio product along every path from the origin. That is the content of (2.9) without needing to pick a path for each state.

Theorem 2.2 is stated for a finite state space. Serfozo assumes the process is ergodic, and the cut-flow argument then sums the balance equations over one side of the cut; on an infinite state space that summation needs an integrability condition that the book leaves implicit in "ergodic". Finiteness makes the rearrangement unconditional and the statement clearly true; the general case is listed under contributions.

Theorem 2.5 is stated as the conclusion that $\pi$ satisfies the balance equations, with explicit summability hypotheses for the three families of sums involved. That $\pi$ is the stationary distribution additionally requires it to be normalized and the process to be ergodic, neither of which is part of the algebraic content.

Contributions welcome beyond the listed items: Theorem 2.4, the characterization of reversibility by invariance of the finite-dimensional distributions under time reversal; Remark 2.9's recursive construction of the canonical measure; Theorem 2.22 on reversible network processes with batch movements; Theorem 2.31 and the partition-reversible processes of Sections 2.8 and 2.9; and the reversibility criteria for Jackson and Whittle networks in Examples 2.24 and 2.25.

Selected references

Richard Serfozo, Introduction to Stochastic Networks, Applications of Mathematics 44, Springer, 1999, chapter 2, pp. 44–51; (2.1), (2.2), Example 2.1, Theorems 2.2, 2.5 and 2.8, Remark 2.9. DOI 10.1007/978-1-4612-1482-3
A. N. Kolmogoroff, Zur Theorie der Markoffschen Ketten, Mathematische Annalen 112 (1936), 155–160. DOI 10.1007/BF01565412
F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979; reissued Cambridge University Press, 2011, chapter 1. DOI 10.1017/CBO9781139226424
P. Whittle, Systems in Stochastic Equilibrium, Wiley, 1986, chapters 1 and 10.

6 thms2 active usersReviewed

Completed

Analysis Stochastic Systems·Captain: naimengye

Probability Theory and Examples V: Blumenthal's 0-1 Law and the Local Behaviour of Brownian PathsTextbook

Motivation

A Brownian path is continuous, and that is essentially all it is. It has no derivative anywhere, it crosses zero infinitely often in every interval $(0,\epsilon)$ , and it becomes positive and negative immediately after time zero. None of this is visible from the finite-dimensional distributions; it is a statement about the germ of the path at a point, and the tool that unlocks it is a zero-one law.

Chapter 7 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) develops that tool. The natural filtration $\mathcal F^{0}_{s}=\sigma(B_r:r\le s)$ is enlarged to $\mathcal F^{+}_{s}=\bigcap_{t>s}\mathcal F^{0}_{t}$ , which allows "an infinitesimal peek at the future" — a quantity like $\limsup_{t\downarrow s}(B_t-B_s)/f(t-s)$ is $\mathcal F^{+}_{s}$ -measurable but not $\mathcal F^{0}_{s}$ -measurable. Blumenthal's 0-1 law (Theorem 7.2.3) says that at $s=0$ this enlargement buys nothing probabilistically: the germ $\sigma$ -field $\mathcal F^{+}_{0}$ is trivial.

Everything local follows. If the path had any chance of staying non-positive on some interval $(0,\epsilon)$ , that would be a germ event of probability at least $1/2$ by symmetry, so it has probability one — and the path enters $(0,\infty)$ immediately. Continuity then forces it to return to zero immediately as well. Combined with the time inversion $X_t=tB(1/t)$ , which turns the germ at $0$ into the tail at $\infty$ , the same law gives $\limsup_{t\to\infty}B_t/\sqrt t=\infty$ and the recurrence of one-dimensional Brownian motion.

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space and $B:\mathbb R_{\ge0}\to\Omega\to\mathbb R$ a Brownian motion: its finite-dimensional laws are centred Gaussian with covariance $\operatorname{cov}(B_s,B_t)=s\wedge t$ , and almost every path is continuous. In particular $B_0=0$ almost surely, so this is Durrett's $\mathbb P_0$ .

Three $\sigma$ -fields organize the chapter:

\mathcal F^{0}_{t}=\sigma(B_s:s\le t),\qquad \mathcal F^{+}_{0}=\bigcap_{t>0}\mathcal F^{0}_{t},\qquad \mathcal T=\bigcap_{t\ge0}\sigma(B_s:s\ge t).

The first is the past, the second the germ at time zero, the third the tail at infinity.

A path $f$ is Lipschitz at the point $s$ with constant $C$ when $|f(t)-f(s)|\le C|t-s|$ for all $t$ within some positive distance of $s$ . A path differentiable at $s$ is Lipschitz at $s$ , so failing this at every point and for every constant is a strong form of nowhere differentiability.

Formalization targets

Goal — Theorem 7.2.3, Blumenthal's 0-1 law

A\in\mathcal F^{+}_{0}\quad\Longrightarrow\quad \mathbb P(A)\in\{0,1\}.

In words: the germ $\sigma$ -field is trivial. Nothing about the path in an arbitrarily short initial interval is genuinely random.

Supporting levels

Theorem 7.1.5, that Brownian paths are Hölder continuous of every exponent $\gamma<1/2$ on every bounded interval; Theorem 7.1.6, that with probability one they are not Lipschitz at any point, hence nowhere differentiable — the Paley–Wiener–Zygmund theorem in the proof of Dvoretsky, Erdős and Kakutani; Theorem 7.2.4, that the path enters $(0,\infty)$ immediately; Theorem 7.2.5, that its zero set accumulates at $0$ ; and Theorem 7.2.8, that $\limsup_{t\to\infty}B_t/\sqrt t=+\infty$ and $\liminf_{t\to\infty}B_t/\sqrt t=-\infty$ .

Significance

The results themselves. Blumenthal's law is the gateway to every local path property of Brownian motion, and Durrett uses it immediately for exactly that. Theorems 7.2.4 and 7.2.5 together say the path oscillates across zero infinitely often in every initial interval — the reason the zero set is an uncountable closed set of Lebesgue measure zero, and the reason the "first return to zero" is not a useful notion at time $0$ . Theorem 7.2.8 is the same law pushed to $t\to\infty$ by time inversion, and it is what makes one-dimensional Brownian motion recurrent (Theorem 7.2.9).

The Hölder pair is the sharp description of path regularity. Exponent $\gamma<1/2$ always works, $\gamma>1/2$ never does, and the borderline $1/2$ is subtle: $\mathbb P(t\in H_{1/2})=0$ for each fixed $t$ , but Davis (1983) showed $\mathbb P(H_{1/2}\ne\emptyset)=1$ . Nowhere differentiability is the historical headline — Paley, Wiener and Zygmund (1933) — and the proof given here is a short covering argument rather than a series construction.

Formalizing them. Mathlib has the object but almost none of the theory. It defines IsPreBrownianReal and IsBrownianReal, proves that a centred Gaussian process with covariance $s\wedge t$ is pre-Brownian, and supplies the invariances — negation, scaling $t\mapsto c^{-1/2}B(ct)$ , the shift $t\mapsto B(t_0+t)-B(t_0)$ , and the time inversion $t\mapsto tB(1/t)$ — together with the weak Markov property IsPreBrownianReal.indepFun_shift. It does not have the germ or tail $\sigma$ -fields, Blumenthal's law, the strong Markov property, any path-regularity result, or the Kolmogorov–Chentsov continuity theorem: Probability/Process/Kolmogorov.lean defines IsKolmogorovProcess, the hypothesis, and stops there. So this mission supplies the $\sigma$ -fields and then everything Durrett proves with them.

Difficulty

The goal reduces to Durrett's Theorem 7.2.2, that $\mathbb E(Z\mid\mathcal F^{+}_{s})=\mathbb E(Z\mid\mathcal F^{0}_{s})$ for bounded path-measurable $Z$ ; at $s=0$ , $\mathcal F^{0}_{0}=\sigma(B_0)$ is trivial because $B_0=0$ almost surely, so $\mathbf 1_A=\mathbb E(\mathbf 1_A\mid\mathcal F^{+}_{0})=\mathbb P(A)$ almost surely, and an indicator almost surely equal to a constant forces that constant to be $0$ or $1$ . Theorem 7.2.2 itself is a monotone class argument on top of the Markov property, and the Markov property in this setting is Mathlib's indepFun_shift plus the observation that the conditional expectation of a product $\prod_m f_m(B_{t_m})$ over $\mathcal F^{+}_{s}$ lands in $\mathcal F^{0}_{s}$ . Assembling that is the work.

Theorem 7.2.4 is then three lines — $\mathbb P_0(\tau\le t)\ge\mathbb P_0(B_t>0)=1/2$ by symmetry of the Gaussian, let $t\downarrow0$ , apply the goal — provided the event has been shown to lie in the germ field, which is where continuity of paths enters. Theorem 7.2.5 follows from 7.2.4 applied to $B$ and $-B$ together with the intermediate value theorem.

Theorem 7.1.5 needs the Kolmogorov–Chentsov continuity theorem, which has to be built: from $\mathbb E|B_t-B_s|^{2m}=C_m|t-s|^m$ one gets Hölder- $\gamma$ control for $\gamma<(m-1)/2m$ , and $m\to\infty$ gives every $\gamma<1/2$ . The dyadic chaining and Borel–Cantelli step is the substance, and it is worth building as a general theorem about IsKolmogorovProcess rather than only for Brownian motion.

Theorem 7.1.6 is self-contained and short: fix $C$ , let $A_n$ be the event that some $s\in[0,1]$ has $|B_t-B_s|\le C|t-s|$ whenever $|t-s|\le3/n$ , and bound $\mathbb P(A_n)\le n\,\mathbb P(|B_1|\le5Cn^{-1/2})^3\le n\{10Cn^{-1/2}(2\pi)^{-1/2}\}^3\to0$ ; since $A_n$ increases, every $\mathbb P(A_n)=0$ .

Theorem 7.2.8 needs the tail 0-1 law, Theorem 7.2.7, which is the goal transported through the time inversion $X_t=tB(1/t)$ — Mathlib's IsPreBrownianReal.inv — because the tail field of $B$ is the germ field of $X$ . With that, $\mathbb P_0(B_n/\sqrt n\ge K\ \text{i.o.})\ge\mathbb P_0(B_1\ge K)>0$ by scaling, so the probability is one, and $K$ is arbitrary.

Formalization scope

The process is Mathlib's IsBrownianReal, indexed by ℝ≥0, on an abstract probability space — not the canonical path space $C[0,\infty)$ that Durrett uses. This is why the shift operators $\theta_s$ and the family $\{\mathbb P_x\}$ do not appear: there is one measure, the process starts at $0$ almost surely, and each statement is about that process. Theorem 7.2.7 as Durrett states it quantifies over all starting points and has no direct analogue here; the tail 0-1 law for the process started at $0$ does, and is listed under contributions as the route to Theorem 7.2.8.

The three $\sigma$ -fields are built as suprema and infima in the lattice of $\sigma$ -algebras on $\Omega$ : pastSigma B t is the supremum of the pullbacks of the Borel field along $B_s$ for $s\le t$ , and germSigma B, tailSigma B are the corresponding infima. The goal carries the hypothesis that each $B_t$ is measurable, not merely almost-everywhere measurable, which is what IsPreBrownianReal gives and what puts these $\sigma$ -fields below the ambient one; the canonical construction satisfies it, and without it " $\mathbb P(A)$ " for a germ event would be an outer measure.

Hölder continuity is stated locally — for almost every path, every $T$ admits a constant — since global Hölder continuity on $[0,\infty)$ is false. The order of quantifiers puts the null set first, so a single path works for every $T$ at once.

The hitting statements avoid an infimum over a possibly empty set. " $\tau=0$ almost surely" is written as: almost surely, for every $\epsilon>0$ there is $t\in(0,\epsilon)$ with $B_t>0$ ; and " $T_0=0$ almost surely" as the same with $B_t=0$ . These are equivalent to Durrett's statements and say what the infimum is there to say. Similarly Theorem 7.2.8 is written with ∃ᶠ … in atTop rather than as an extended-real $\limsup$ , which is what " $\limsup=+\infty$ " means and avoids a coercion.

LipschitzAtPoint f s C is "there is a scale $\delta>0$ on which $|f(t)-f(s)|\le C|t-s|$ ". Its negation for every $s$ and every $C$ is Theorem 7.1.6, and it has content in both directions: the identity path is Lipschitz at every point with $C=1$ , while $t\mapsto\sqrt t$ is not Lipschitz at $0$ with $C=1$ — both checked in Lean before publishing.

Existence is not part of this mission. Mathlib proves nothing of the form "a Brownian motion exists", and nothing here needs it: every item takes a Brownian motion as a hypothesis. That the hypothesis is satisfiable is a theorem — Durrett's 7.1.1, via Kolmogorov extension and the continuity theorem — and it is listed under contributions, where it belongs, since building it is a project of its own.

Contributions welcome beyond the listed items: Kolmogorov–Chentsov as a general statement about IsKolmogorovProcess; Theorem 7.1.1, the existence of Brownian motion; Theorem 7.2.2 in full, for every $s$ ; the tail 0-1 law and Theorem 7.2.9, recurrence; the strong Markov property and the reflection principle of section 7.3; and Exercise 7.1.5, that no path is Hölder of any exponent $\gamma>1/2$ .

Selected references

Rick Durrett, Probability: Theory and Examples, Version 5 (11 January 2019), chapter 7, sections 7.1 and 7.2 (pp. 353–365); Theorems 7.1.5, 7.1.6, 7.2.3, 7.2.4, 7.2.5, 7.2.8. Published as the 5th edition, Cambridge University Press, 2019, DOI 10.1017/9781108591034
R. M. Blumenthal, An extended Markov property, Transactions of the American Mathematical Society 85 (1957), 52–72. DOI 10.1090/S0002-9947-1957-0088102-2
R. E. A. C. Paley, N. Wiener and A. Zygmund, Notes on random functions, Mathematische Zeitschrift 37 (1933), 647–668. DOI 10.1007/BF01474606
A. Dvoretzky, P. Erdős and S. Kakutani, Nonincrease everywhere of the Brownian motion process, Proceedings of the Fourth Berkeley Symposium II (1961), 103–116.
N. Wiener, Differential space, Journal of Mathematics and Physics 2 (1923), 131–174. DOI 10.1002/sapm192321131
I. Karatzas and S. E. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer, 1991, chapter 2. DOI 10.1007/978-1-4612-0949-2

7 thms2 active usersReviewed

Completed

Markov Chain Stochastic Systems·Captain: naimengye

Probability Theory and Examples III: The Markov Chain Convergence TheoremTextbook

Motivation

A Markov chain forgets. Run it long enough and the distribution of its position stops depending on where it started — that is the intuition behind shuffling a deck, behind Markov chain Monte Carlo, behind PageRank, and behind the stationary analyses of every queueing model. Chapter 5 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) makes it a theorem, and identifies exactly what can go wrong.

Two things can. The chain may fail to reach parts of the state space, and the answer is irreducibility. Or it may reach them only on a lattice of times — a chain alternating between two halves of its state space never forgets whether the clock is even or odd — and the answer is aperiodicity. Theorem 5.6.6 says that is the complete list: an irreducible, aperiodic chain with a stationary distribution has $p^n(x,y)\to\pi(y)$ , for every pair of states, whatever the starting point.

Setting

Let $S$ be a countable state space and $p(x,y)$ a transition probability: non-negative, with each row summing to one. The $n$ -step transition probabilities are the matrix powers, $p^0(x,y)=\delta_{xy}$ and $p^{n+1}(x,y)=\sum_z p(x,z)p^n(z,y)$ .

Hitting is described by the first-passage probabilities $f^n(x,y)=\mathbb{P}_x(T_y=n)$ , given by $f^1(x,y)=p(x,y)$ and $f^{n+1}(x,y)=\sum_{z\ne y}p(x,z)f^n(z,y)$ — the chain moves once and then reaches $y$ for the first time, having avoided it meanwhile. Summing them gives

\rho_{xy}=\mathbb{P}_x(T_y<\infty)=\sum_{n\ge1}f^n(x,y),\qquad \mathbb{E}_yT_y=\sum_{n\ge1}n\,f^n(y,y).

A state is recurrent when $\rho_{yy}=1$ , the chain is irreducible when $\rho_{xy}>0$ for all $x,y$ , and a state $x$ is aperiodic when the greatest common divisor of $I_x=\{n\ge1:p^n(x,x)>0\}$ is $1$ . A stationary distribution is a probability vector $\pi$ with $\sum_x\pi(x)p(x,y)=\pi(y)$ .

Formalization targets

Goal — Theorem 5.6.6, the convergence theorem

p \text{ irreducible},\ \text{aperiodic},\ \text{with stationary distribution } \pi \quad\Longrightarrow\quad p^n(x,y)\longrightarrow\pi(y)\ \text{ for all } x,y .

The goal asserts pointwise convergence of the transition probabilities, not convergence in total variation and not a rate; those are strengthenings, and stating the weakest useful form is what keeps the theorem stable.

Supporting levels

Theorem 5.3.1, that a state is recurrent exactly when $\sum_n p^n(y,y)$ diverges — the bridge between the hitting picture and the matrix picture; Theorem 5.3.2, that recurrence is contagious; Theorem 5.5.10, that every state in the support of a stationary distribution is recurrent; and Theorem 5.5.11, that for an irreducible chain with a stationary distribution $\pi(x)=1/\mathbb{E}_xT_x$ .

Significance

The result itself. Theorem 5.6.6 is what licenses reading a stationary distribution as a long-run frequency. Without it, $\pi$ is merely a fixed point of a linear map; with it, $\pi(y)$ is the limiting probability of being at $y$ , from any start. Theorem 5.5.11 then gives the quantity a second, purely local meaning — $\pi(x)$ is the reciprocal of the mean return time to $x$ — which is the identity behind every renewal-reward computation in applied probability and behind the "expected time between visits" estimates that Monte Carlo methods rely on. The two necessary hypotheses are sharp: a periodic chain has $p^n(x,y)$ oscillating rather than converging, and Durrett's Theorem 5.7.2 gives the corrected statement in that case.

Formalizing it. Mathlib has no countable-state Markov chain theory. It has ProbabilityTheory.Kernel and an Irreducible notion for kernels, but nothing about recurrence, transience, first-passage decompositions, stationary measures or the convergence theorem, and nothing that specializes to a transition matrix on a countable set. The mission therefore contributes the whole apparatus of sections 5.3, 5.5 and 5.6 — the $n$ -step and first-passage probabilities, $\rho_{xy}$ , the mean return time, recurrence, irreducibility, aperiodicity and stationarity — together with the results that make it usable.

Difficulty

The usual proof of the goal is a coupling argument, and it is short but not obvious: run two independent copies of the chain, one from $x$ and one from $\pi$ , on the product space $S\times S$ with transition probability $\bar p((x_1,x_2),(y_1,y_2))=p(x_1,y_1)p(x_2,y_2)$ ; aperiodicity plus irreducibility make the product chain irreducible, $\pi\times\pi$ is stationary for it, so it is recurrent and the two copies meet almost surely; after they meet they can be exchanged. Each step of that is a separate obligation, and the one that consumes aperiodicity is the irreducibility of the product chain — for a periodic chain it fails, which is exactly why the theorem does.

The number-theoretic ingredient is worth flagging: irreducibility of the product needs that $I_x=\{n:p^n(x,x)>0\}$ , being closed under addition with $\gcd 1$ , contains every sufficiently large integer. That is the numerical semigroup fact, and it is where aperiodicity is actually used.

Formalization scope

The state space is any countable type with decidable equality, and the transition probability is a plain function $S\times S\to\mathbb{R}$ constrained by IsTransition: non-negative entries, summable rows, rows summing to one. Sums over the state space are unconditional sums, so no finiteness is assumed anywhere.

The chain's law is not constructed. Every quantity here — $p^n$ , $f^n$ , $\rho_{xy}$ , $\mathbb{E}_yT_y$ — is defined by an explicit recursion on the transition matrix, not as an expectation against a measure on path space. This is a deliberate choice: building the path measure is a substantial project of its own, and none of the statements in these sections need it. The recursions are the standard ones and they are the definitions the book's own computations use. The cost is that probabilistic statements about paths, such as Theorem 5.6.1 on the almost-sure limit of the visit counts $N_n(y)/n$ , cannot be phrased in this language and are not part of the mission.

Conventions: $p^0$ is the identity matrix; $f^n$ vanishes at $n=0$ ; $\rho_{xy}$ and $\mathbb{E}_yT_y$ are unconditional sums over $n\ge1$ , so an infinite mean return time appears as a non-summable series rather than as an extended real. Theorem 5.5.11 is therefore stated as summability together with $\pi(x)\cdot\mathbb{E}_xT_x=1$ , which asserts finiteness of the mean return time rather than silently relying on a division convention.

Aperiodicity is "the only natural number dividing every element of $I_x$ is $1$ ", which is $\gcd I_x=1$ written without needing a gcd of a set; it is false when $I_x$ is empty, which is correct, since the period of such a state is undefined.

The goal is not vacuous: the hypotheses are satisfiable by any strictly positive transition matrix on a finite set.

Contributions welcome beyond the listed items: Theorem 5.3.3 on finite closed sets; the decomposition theorem 5.3.5; existence of a stationary measure from a recurrent state (5.5.7) and its uniqueness (5.5.9); the equivalence of positive recurrence and the existence of a stationary distribution (5.5.12); Theorem 5.7.2 for the periodic case; and the path-level results of section 5.6, which need the chain's law on path space.

Selected references

Rick Durrett, Probability: Theory and Examples, Version 5 (11 January 2019), chapter 5, sections 5.3, 5.5 and 5.6 (pp. 281–320); Theorems 5.3.1, 5.3.2, 5.5.10, 5.5.11, 5.6.6. Published as the 5th edition, Cambridge University Press, 2019, DOI 10.1017/9781108591034
J. R. Norris, Markov Chains, Cambridge University Press, 1998, chapter 1. DOI 10.1017/CBO9780511810633
D. A. Levin and Y. Peres, Markov Chains and Mixing Times, 2nd ed., American Mathematical Society, 2017. DOI 10.1090/mbk/107
W. Doeblin, Exposé de la théorie des chaînes simples constantes de Markoff à un nombre fini d'états, Revue Mathématique de l'Union Interbalkanique 2 (1938), 77–105.

6 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: naimengye

Stochastic Networks V: Random Access and the Critical Rate of Backoff SchemesTextbook

Motivation

When many stations share one broadcast channel, something has to decide who transmits. A token passed around the stations works when there are few of them and none is silent for long, but it scales badly and breaks if the token is lost. The alternative is to let stations transmit whenever they like and use randomness to recover from the resulting collisions. That is the design of ALOHA, built in the 1970s to connect terminals across the Hawaiian islands, and of Ethernet, and of essentially every contention-based access protocol since.

Chapter 5 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) asks what such protocols can achieve, and the answers are largely negative. ALOHA with a fixed retransmission probability jams: with probability one there is a finite random time after which every slot contains a collision and no packet ever succeeds again, for every positive arrival rate. Ethernet's binary exponential backoff does better, but only just: it has a positive critical arrival rate, above which only finitely many packets are ever transmitted, and it is still not positive recurrent at rates where it does transmit infinitely many. The chapter's general statement is the one this mission targets: any backoff slower than exponential jams at every positive arrival rate.

Setting

Time is slotted, and a transmission attempt occupies exactly one slot. New packets arrive in a Poisson stream of rate $\nu$ , so the number arriving in a slot is Poisson with mean $\nu$ . A slot in which exactly one station transmits carries its packet successfully; a slot in which two or more transmit is a collision and carries nothing.

In an acknowledgement-based scheme a station learns nothing about the channel except whether its own transmissions succeeded. A packet arriving in slot $t$ attempts transmission in slots $t+x_0, t+x_1, \dots$ with $1 = x_0 < x_1 < \cdots$ , the sequence chosen independently for each packet, and

h(x) = \mathbb{P}(x \in X), \qquad h(1) = 1

is the retransmission function. For ALOHA, $h(x) = f$ for every $x > 1$ ; for Ethernet's binary exponential backoff, $\sum_{r \le t} h(r) \sim \log_2 t$ .

Now imagine the channel externally jammed from time $0$ , so that every retransmission actually occurs. The attempts in slot $t$ are then Poisson with mean $\nu\sum_{r=1}^{t}h(r)$ , and the probability that fewer than two attempts are made in slot $t$ is

P_t=\Bigl(1+\nu\sum_{r=1}^{t}h(r)\Bigr)\exp\Bigl(-\nu\sum_{r=1}^{t}h(r)\Bigr).

The expected number of such slots is $H(\nu)=\sum_{t\ge1}P_t$ , which is decreasing in $\nu$ , and the critical rate is

\nu_c=\inf\{\nu : H(\nu)<\infty\}.

Theorem 5.11 of the book says $\nu_c$ deserves its name: below it infinitely many packets are transmitted with probability one, above it only finitely many.

Formalization targets

Goal — condition (5.7): slower-than-exponential backoff has $\nu_c=0$

\frac{1}{\log t}\sum_{x=1}^{t}h(x)\longrightarrow\infty \quad\Longrightarrow\quad H(\nu)=\sum_{t\ge1}P_t<\infty \ \text{ for every } \nu>0 .

Since $H(\nu)<\infty$ for every positive $\nu$ , the critical rate is $\nu_c=0$ , and by Theorem 5.11 the expected number of successful transmissions is finite at every positive arrival rate. The goal fixes no constant and no rate: it says only that the dividing line between "jams always" and "has a positive capacity" sits at logarithmic growth of $\sum_{x\le t}h(x)$ , which is exponential growth of the backoff.

Supporting levels

The ALOHA drift calculation of section 5.1 and its consequence that the drift is positive once the backlog is large enough; the summability $\sum_n p(n)<\infty$ that combines with Borel–Cantelli to give Proposition 5.3; the monotonicity of $P_t$ in $\nu$ ; the opposite extreme, that a scheme with $\sum_x h(x)<\infty$ — one that gives up on a packet after finitely many attempts — has $\nu_c=\infty$ ; that ALOHA's own retransmission function satisfies condition (5.7); and the bound of Remark 5.14, that a positive recurrent acknowledgement-based scheme needs $\nu\le e^{-\nu}$ and hence $\nu<0.5672$ , which is strictly below Ethernet's $\nu_c=\log 2$ .

Significance

The result itself. Condition (5.7) is the chapter's structural statement about random access, and it is a sharp one. Any retransmission rule under which a packet keeps trying at a rate that does not decay fast enough — a fixed probability, a polynomially growing backoff, anything short of exponential — has critical rate zero: the channel jams at every positive load. Exponential backoff is not a tuning choice, it is the minimum that makes the protocol work at all, and the $\log b$ formula for a backoff by factor $b$ (Exercise 5.7) then says how much capacity each choice of $b$ buys. The gap recorded in Remark 5.14 is the other half of the picture: even above the threshold, "infinitely many packets get through" is much weaker than "the backlog is stable", and between $0.567$ and $\log 2 \approx 0.693$ Ethernet does the first and provably not the second.

Formalizing it. None of this is open; the analysis is due to Kelly and MacPhee (1987) and Aldous (1987). What the mission contributes is a machine-checked account of the analytic core: the definitions of $P_t$ , $H(\nu)$ and $\nu_c$ , the two extremes of the classification, and the ALOHA calculations. Mathlib has no protocol analysis and nothing about random access channels.

Difficulty

The obstacle is a modelling one and it is worth stating plainly rather than discovering halfway through. The chapter's headline results — Proposition 5.3 that ALOHA jams almost surely, Theorem 5.11 that $\nu_c$ is the critical rate, Theorem 5.15 that geometric Ethernet is transient — are statements about sample paths of a Markov chain built on a Poisson arrival stream, and their proofs are coupling arguments comparing a system started empty with one started with a backlog. Nothing in Mathlib supports that construction, and building it is a research-scale project rather than a chapter. This mission therefore formalizes the analytic half and quotes the probabilistic half, which is the same division the book itself makes when it computes $\nu_c$ for a scheme: Theorem 5.11 is proved once, and every subsequent statement about a protocol is a convergence question about $\sum_t P_t$ .

Within that analytic half the difficulty is real but ordinary. The summand $P_t$ is a product of a factor growing with $\sum_{r\le t}h(r)$ and one decaying exponentially in it, so the growth hypothesis has to be turned into a summable bound without assuming any regularity of $h$ beyond non-negativity — in particular $\sum_{r\le t}h(r)$ need not be eventually monotone in any useful quantitative sense, only divergent faster than $\log t$ .

Formalization scope

The retransmission function is any non-negative real sequence; the normalization $h(1)=1$ is not imposed, since none of the statements need it and imposing it would exclude the comparison schemes. $P_t$ and the partial sums are real-valued, and " $H(\nu)<\infty$ " is stated as summability of the sequence rather than as a bound on an extended-real sum, so convergence is asserted rather than assumed. The goal is stated for each fixed $\nu>0$ separately, which is what makes $\nu_c=0$ ; it is not stated as a claim about the infimum, because the infimum of the set $\{\nu : H(\nu)<\infty\}$ adds nothing once the set is known to be all of $(0,\infty)$ .

The growth hypothesis is the book's condition (5.7) verbatim: $\bigl(\log t\bigr)^{-1}\sum_{x\le t}h(x)\to\infty$ . Note that at $t=0$ and $t=1$ the quotient involves $\log t \le 0$ and is not meaningful; divergence to infinity is an eventual statement, so this costs nothing, but it is why the hypothesis is a limit rather than a pointwise bound.

The mission is not vacuous in either direction: the ALOHA milestone exhibits a retransmission function satisfying the hypothesis, and the $\sum_x h(x)<\infty$ milestone exhibits one that fails it as strongly as possible, with $H(\nu)=\infty$ for every $\nu$ .

Contributions welcome beyond the listed items: Ethernet's $\sum_{r\le t}h(r)\sim\log_2 t$ and the resulting $\nu_c=\log 2$ ; the generalization $\nu_c=\log b$ of Exercise 5.7; the scheme $h(x)=1/(x\log x)$ with $\nu_c=\infty$ ; the continuous-time halving $\nu_c=\frac12\log b$ of Kelly and MacPhee; and, for anyone willing to build the probabilistic layer, Proposition 5.3 and Theorem 5.11 themselves.

Selected references

Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 5 (pp. 108–132); Definition 5.1, Proposition 5.3, Theorems 5.11 and 5.15, condition (5.7), Examples 5.8, 5.12 and 5.13, Remark 5.14. DOI 10.1017/cbo9781139565363
N. Abramson, The ALOHA system — another alternative for computer communications, AFIPS Conference Proceedings 37 (1970), 281–285. DOI 10.1145/1478462.1478502
F. P. Kelly and I. M. MacPhee, The number of packets transmitted by collision detect random access schemes, Annals of Probability 15 (1987), 1557–1568. DOI 10.1214/aop/1176991992
D. J. Aldous, Ultimate instability of exponential back-off protocol for acknowledgement-based transmission control of random access communication channels, IEEE Transactions on Information Theory 33 (1987), 219–223. DOI 10.1109/TIT.1987.1057295
R. M. Metcalfe and D. R. Boggs, Ethernet: distributed packet switching for local computer networks, Communications of the ACM 19 (1976), 395–404. DOI 10.1145/360248.360253

8 thms2 active usersReviewed

Completed

Machine Learning Random Matrix Theory Statistics·Captain: mikedeng1

High-Dimensional Probability II: Concentration Inequalities for Sums of Independent Random VariablesTextbook

Motivation

The central limit theorem tells us that a normalized sum of independent random variables converges in distribution to a Gaussian. For applications — bounding the failure probability of a randomized algorithm, controlling the error of a Monte Carlo estimator, proving a generalization bound in learning theory — a limiting distribution is not enough: what is needed is a single, explicit, non-asymptotic inequality that holds for every fixed sample size $N$ , not merely as $N \to \infty$ . Hoeffding's inequality (Wassily Hoeffding, 1963) and Bernstein's inequality (Sergei Bernstein, 1920s–1940s, in the form used here due to Vadim Bennett and later authors) are the two archetypal answers: both give an explicit Gaussian-type tail bound for a weighted sum of independent random variables, valid for every $N$ , with all constants made explicit. They are the workhorses behind concentration of measure, high-dimensional statistics, and the non-asymptotic analysis of randomized algorithms; a textbook trying to reach the Johnson–Lindenstrauss lemma, random matrix norms, or the restricted isometry property has to pass through this chapter first, because every one of those results is itself an application of a weighted-sum concentration inequality to a specific choice of random variables.

The central limit theorem's own error term is the obstruction that direct concentration inequalities are built to avoid: the Berry–Esseen theorem (Andrew C. Berry, 1941; Carl-Gustav Esseen, 1942) bounds the normal approximation's error at order $1/\sqrt N$ , which is too slow to recover a genuinely exponential tail bound for finite $N$ . Hoeffding's and Bernstein's inequalities are proved instead by a direct argument — bounding the moment generating function of the sum and optimizing a Markov/Chernoff exponential tilt — that never invokes the central limit theorem or its error term at all.

The sub-gaussian and sub-exponential norms

Fix a probability space $(\Omega, \mathcal F, P)$ . For a real random variable $X$ on $(\Omega, \mathcal F, P)$ , define its sub-gaussian norm

\|X\|_{\psi_2} := \inf\{t > 0 : \mathbb E \exp(X^2/t^2) \text{ is finite and } \le 2\}

and its sub-exponential norm

\|X\|_{\psi_1} := \inf\{t > 0 : \mathbb E \exp(|X|/t) \text{ is finite and } \le 2\}.

In both definitions, the requirement that the exponential moment be finite (i.e. that the moment-generating integrand be integrable), and not merely satisfy " $\le 2$ " as a bare inequality, is essential: without it a moment that is genuinely infinite for a given $t$ would vacuously count as " $\le 2$ " under the Bochner integral's convention that a non-integrable function integrates to $0$ , and every random variable — however heavy-tailed — would trivially have norm $0$ . $X$ is called sub-gaussian (respectively sub-exponential) when this infimum is over a nonempty set, i.e. when some finite $t$ makes the moment finite and at most $2$ . These are genuine norms (up to the identification of almost-surely-equal random variables) on the vector space of random variables for which they are finite, and they are the natural non-asymptotic yardsticks for tail heaviness: $\|X\|_{\psi_2} < \infty$ characterizes a Gaussian-type tail $P\{|X| \ge t\} \le 2\exp(-ct^2/\|X\|_{\psi_2}^2)$ , while $\|X\|_{\psi_1} < \infty$ characterizes an exponential-type tail $P\{|X| \ge t\} \le 2\exp(-ct/\|X\|_{\psi_1})$ . Every bounded random variable — in particular every Bernoulli or Rademacher (symmetric Bernoulli) random variable — is sub-gaussian, and the square of a sub-gaussian random variable is sub-exponential; a genuinely sub-exponential (not sub-gaussian) example is the squared coordinate $g_i^2$ of a standard Gaussian vector, or the exponential distribution itself.

Formalization targets

Goal — Theorem 2.8.2 (Bernstein's inequality, weighted sum). Let $X_1, \dots, X_N$ be independent, mean-zero, sub-exponential random variables on $(\Omega, \mathcal F, P)$ , and let $a = (a_1, \dots, a_N) \in \mathbb R^N$ . Then, for every $t \ge 0$ ,

P\Bigl\{\Bigl|\sum_{i=1}^N a_i X_i\Bigr| \ge t\Bigr\} \;\le\; 2\exp\left[-c\min\left(\frac{t^2}{K^2\|a\|_2^2}, \frac{t}{K\|a\|_\infty}\right)\right],

where $K = \max_i \|X_i\|_{\psi_1}$ and $c > 0$ is an absolute constant that does not depend on $N$ , the $X_i$ , $a$ , or $t$ .

The goal is deliberately the weighted and sub-exponential form, the weakest of the chapter's results that is still stable under the improvements a solver might find: it neither fixes $a_i \equiv 1$ (the unweighted Theorem 2.8.1, a special case) nor restricts to the lighter sub-gaussian tail (Theorem 2.6.3, which follows from a strictly stronger hypothesis). Both weaker theorems, plus Hoeffding's and Chernoff's inequalities, are included as milestones because Bernstein's own proof is built directly from them.

Significance

The result itself. Bernstein's inequality is the two-tail-regime concentration bound: a sub-gaussian tail $\exp(-ct^2/(K\|a\|_2)^2)$ near the mean, transitioning to a heavier sub-exponential tail $\exp(-ct/(K\|a\|_\infty))$ far from it, exactly the behavior one should expect from a mixture of light-tailed terms with one heavy-tailed outlier. It underlies the concentration of quadratic forms (Chapter 6's Hanson–Wright inequality controls $\sum \varepsilon_i \varepsilon_j$ -type terms, which are themselves products of sub-gaussians and hence sub-exponential by Lemma 2.7.7), and it is the standard tool for bounding empirical-process suprema whose summands are not bounded but merely light-tailed.

Formalizing it. No formalization of Bernstein's inequality — in either the weighted or unweighted, or sub-gaussian or sub-exponential form — exists yet on Prove2Me (GET /theorems?q=Bernstein and q=sub-exponential return no relevant hits, checked 2026-09-17). What this mission produces is not just the statement but the machinery underneath it: a working Orlicz-norm treatment of $\psi_1$ and $\psi_2$ that a later mission (the Hanson–Wright inequality, or any future chapter that needs sub-exponential concentration) can build on directly.

Difficulty

The obvious first idea — squaring both sides and applying Chebyshev, as one does to prove the weak law of large numbers — gives only a polynomial tail bound decaying like $1/N$ , far too weak to be useful (this is exactly the point made by the chapter's opening discussion of the coin-tossing example, comparing the linear decay from Chebyshev against the target exponential decay). The central limit theorem promises the right shape of tail asymptotically but, per Berry–Esseen, with an error of order $1/\sqrt N$ that swamps any exponential gain for large deviations — the CLT approximation is simply not valid in the tail regime the inequality needs. The actual argument instead controls the moment generating function of the full sum directly and optimizes an exponential (Chernoff) tilt; this is why the sub-gaussian and sub-exponential norms — MGF-control objects, not moment or tail objects per se — are the right technical vehicle, even though Proposition 2.5.2 and 2.7.1 show all these characterizations are equivalent up to constants. The min of two terms in Bernstein's exponent is not an artifact of a loose proof: it reflects a genuinely two-regime tail (Gaussian near the mean, exponential in the far tail), and collapsing it to a single term in either direction would either be false (dropping the exponential term) or needlessly weak (dropping the Gaussian term, which is what a naive union bound over the worst single term would give).

Formalization scope

Random variables are ℝ-valued functions on an explicit probability space (Ω, mΩ, P) (Ω : Type, MeasurableSpace Ω, P : Measure Ω, [IsProbabilityMeasure P]), matching the book's setup throughout. Independence is Mathlib's ProbabilityTheory.iIndepFun, and tail probabilities are stated with P.real, Mathlib's ℝ-valued measure evaluation, which corresponds directly to the book's $P\{\cdot\}$ .

Both Orlicz norms are defined locally, as genuine infima matching Definitions 2.5.6 and 2.7.5 verbatim (subgaussianNorm, subexponentialNorm, each sInf {t > 0 : Integrable (fun ω => E[...]) P ∧ E[...] ≤ 2}), rather than reused from Mathlib's HasSubgaussianMGF (Mathlib.Probability.Moments.SubGaussian). The Integrable conjunct is not optional dressing: Mathlib's Bochner integral of a non-integrable function is 0 by convention, so a bare E[...] ≤ 2 (without asserting integrability) would be satisfied by every t for which the moment is actually infinite, collapsing the sub-gaussian norm of a standard Gaussian (and, symmetrically, the sub-exponential norm of any heavy-tailed variable) to 0 — a trivializing formalization the mission was moderated to rule out. The same Integrable conjunct appears in every moment hypothesis (general_hoeffding, bernstein_unweighted, bernstein_weighted): ∃ s > 0, Integrable (...) P ∧ ∫ ... ≤ 2, so that the hypothesis is not satisfied vacuously by non-integrable exponential moments either. HasSubgaussianMGF bounds the moment generating function directly with a variance-proxy parameter $\sigma^2$ (E exp(tX) ≤ exp(c t²/2)), which is a different object definitionally from the Orlicz $\psi_2$ norm — equivalent up to a constant factor by the book's own Proposition 2.5.2, but not interchangeable without restating that equivalence — and Mathlib has no sub-exponential analogue at all. Since the goal theorem and two of its milestones need the sub-exponential norm, one consistent convention (the book's own Orlicz norms) is used for both $\psi_1$ and $\psi_2$ throughout the mission, rather than mixing Mathlib's MGF-based sub-gaussian convention with a locally defined sub-exponential one.

Every occurrence of the book's " $c$ is an absolute constant" is formalized as a genuine existential quantifier fixed before the random variables, the vector a, and t are introduced: ∃ c : ℝ, 0 < c ∧ ∀ ..., P.real {...} ≤ 2 * Real.exp (-(c * ...)). No numeral is substituted for c anywhere; a solver's proof may use any positive constant it can establish, exactly mirroring the book's own non-constructive existence claims. The trivializing formalization this rules out is fixing c to a specific small numeral (which would be a strictly stronger, easier, and unfaithful claim) or, in the other direction, weakening the statement by allowing c to depend on N, the $X_i$ , a, or t (which would make the theorem vacuous, since any such bound trivially holds for a small enough $c$ depending on the instance).

Chernoff's inequality (Theorem 2.3.1) needs no Orlicz norm — Bernoulli parameters $p_i$ are given directly via P.real {X i = 1} = p i ∧ P.real {X i = 0} = 1 - p i, and the conclusion uses Real.rpow (^ on ℝ → ℝ → ℝ) for the real exponent $t$ in $(e\mu/t)^t$ . Hoeffding's inequality for symmetric Bernoulli variables (Theorem 2.2.2) is likewise self-contained, needing only the two-point probability hypothesis defining the Rademacher distribution.

Selected references

W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301), 1963. https://doi.org/10.2307/2282952
S. Bernstein, The Theory of Probabilities, Gastehizdat Publishing House, Moscow, 1946 (Russian; the inequality is due to Bernstein's earlier 1920s–1930s work, this textbook states the modern sub-exponential form following later expositions).
A. C. Berry, The Accuracy of the Gaussian Approximation to the Sum of Independent Variates, Transactions of the American Mathematical Society 49(1), 1941. https://doi.org/10.2307/1990053
C.-G. Esseen, On the Liapunoff Limit of Error in the Theory of Probability, Arkiv för Matematik, Astronomi och Fysik A28, 1942.
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 2. https://doi.org/10.1017/9781108231596

7 thms2 active usersReviewed

Completed

Machine Learning Random Matrix Theory Statistics·Captain: mikedeng1

High-Dimensional Probability I: Approximate Carathéodory's TheoremTextbook

Motivation

Many arguments in high-dimensional geometry, statistics and computer science need to approximate a point of a convex set by an average of a handful of extreme points, rather than represent it exactly. The classical Carathéodory theorem (1907) answers the exact question: every point of the convex hull of a set $T \subseteq \mathbb{R}^n$ is a convex combination of at most $n+1$ points of $T$ . That bound is tight and grows with the dimension $n$ , which makes it useless whenever $n$ is large — exactly the regime of interest in high-dimensional probability.

B. Maurey's empirical method — an unpublished 1980–81 result reported by G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle 1980–1981 — and later applied by B. Carl to bound covering numbers of operators between Banach spaces (Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces, Ann. Inst. Fourier 35(3), 1985, 79–118), replaces the exact question with an approximate one and removes the dimension dependence entirely: to approximate $x$ to accuracy $\varepsilon$ , the number of points needed depends only on $\varepsilon$ , never on $n$ . Vershynin's High-Dimensional Probability opens with this result as its "Appetizer," using it to illustrate the book's central theme — that randomness is a tool for constructing deterministic combinatorial objects — before any probabilistic machinery has been introduced.

Setting

A convex combination of finitely many points $z_1, \dots, z_m \in \mathbb{R}^n$ is a sum $\sum_{i=1}^m \lambda_i z_i$ with $\lambda_i \ge 0$ and $\sum_i \lambda_i = 1$ . The convex hull $\operatorname{conv}(T)$ of a set $T \subseteq \mathbb{R}^n$ is the set of all convex combinations of all finite collections of points of $T$ . The diameter of $T$ is $\operatorname{diam}(T) = \sup\{\|s-t\|_2 : s, t \in T\}$ , the Euclidean norm throughout.

The classical Carathéodory theorem states that every $x \in \operatorname{conv}(T)$ is a convex combination of at most $n+1$ points of $T$ — with $n+1$ generally unavoidable, attained by a simplex. The question this mission answers is different: given that we are willing to approximate $x$ rather than represent it exactly, and willing to use only combinations with equal coefficients $1/k$ (an average of $k$ points, with repetition allowed), how large must $k$ be as a function of the desired accuracy?

Formalization targets

Goal — Theorem 0.0.2, Approximate Carathéodory's theorem

\text{diam}(T) \le 1,\ x \in \operatorname{conv}(T),\ k \in \mathbb{Z}_{>0} \ \Longrightarrow\ \exists\, x_1,\dots,x_k \in T:\quad \left\| x - \frac{1}{k}\sum_{j=1}^{k} x_j \right\|_2 \le \frac{1}{\sqrt{k}}.

The quantifiers are exactly this order: for every bounded $T$ , every point of its convex hull, and every target $k$ , such an averaging set exists. This is the weakest stable statement carrying the theorem's content — the number of points $k$ does not depend on the dimension $n$ , and the coefficients are forced to be uniform — and it is the form the corollary below invokes directly.

Milestone — Corollary 0.0.4, Covering polytopes by balls

P = \operatorname{conv}(T),\ |T| = N,\ \operatorname{diam}(P) \le 1,\ \varepsilon > 0 \ \Longrightarrow\ \exists\, C,\ |C| \le N^{\lceil 1/\varepsilon^2 \rceil}:\quad P \subseteq \bigcup_{c \in C} \overline{B}(c, \varepsilon).

This is a direct application of the goal to computational geometry's covering problem: how many balls of radius $\varepsilon$ are needed to cover a polytope, and where should they be centered.

Significance

The result itself. The approximate Carathéodory theorem is the prototype of a dimension-free approximation result: whenever a set is bounded, a fixed number of points (depending only on the target accuracy, not the ambient dimension) suffices to approximate any point of its convex hull. This is what makes possible dimension-independent covering-number bounds such as Corollary 0.0.4, which in turn are the starting point for the book's later treatment of entropy, packing and generic chaining (Chapters 4, 7–8). The technique generalizes far beyond $\mathbb{R}^n$ : it underlies covering-number bounds for operators between Banach spaces (Carl's original application) and is a recurring device in learning theory for bounding the size of an $\varepsilon$ -net of a hypothesis class.

Formalizing it. Both results are elementary and already fully proved in the literature; no open mathematical content remains. What this mission contributes is a machine-checked, faithful Lean statement of Maurey's construction and its corollary, phrased over Mathlib's existing convex-hull and metric-diameter machinery, so that later missions in this series (concentration inequalities, Johnson–Lindenstrauss, chaining) can build on a verified base case of "probability constructs a deterministic covering," and so that the empirical method itself becomes a reusable, linked component on the platform. The proof of the goal (via the probabilistic argument sketched by the book: interpret a convex combination as a probability distribution, average $k$ i.i.d. samples, and bound the variance) is left open for solvers.

Difficulty

The identity that makes the proof work — averaging $k$ independent copies of a random vector concentrates around its mean at rate $1/\sqrt{k}$ in mean-square — is a two-line computation once the convex combination is reinterpreted probabilistically. The step that is easy to miss is this reinterpretation itself: nothing in the statement mentions probability, so the "obvious" attack of manipulating the convex-combination weights directly, or trying to construct $x_1,\dots,x_k$ by some explicit combinatorial recipe, does not see a path to a bound independent of $n$ . The probabilistic argument produces the points non-constructively, via an averaging/existence argument (the expected squared distance is small, so some realization achieves it) rather than an explicit formula — a solver has to introduce a probability space and a random vector that does not appear anywhere in the formal statement to be proved.

Formalization scope

Both results are stated over EuclideanSpace ℝ (Fin n) for an explicit dimension n : ℕ, so ‖·‖ is the Euclidean norm and Mathlib's Metric.diam is used directly for $\operatorname{diam}(T) = \sup\{\|s-t\|_2\}$ . The convex hull is Mathlib's convexHull ℝ T; by Mathlib's convexHull_eq, this already coincides with the book's own definition of a convex combination of finitely many points of $T$ , so no bespoke convex-combination definition is introduced — this mission needs no supporting definitions of its own. In the corollary, "a polytope $P$ with $N$ vertices" is formalized, following the book's own proof, as $P = \operatorname{conv}(T)$ for a finite vertex set $T$ with $\#T = N$ , rather than via a separate Polytope structure (which Mathlib does not provide and the book's argument does not need). The covering bound $N^{\lceil 1/\varepsilon^2\rceil}$ is an exponent, not a product with $N$ — matching the book's own proof, which counts the $N^k$ ordered $k$ -tuples of vertices with repetition, $k := \lceil 1/\varepsilon^2\rceil$ ; the typeset " $N\lceil 1/\varepsilon^2\rceil$ " in the corollary statement is the same juxtaposition-as-exponent notation the proof uses for " $N^k$ " one line earlier.

A trivializing formalization is ruled out explicitly: the goal must hold for every integer $k > 0$ and every $x \in \operatorname{conv}(T)$ , not merely some convenient choice — e.g. $k = 1$ together with $x \in T$ trivially satisfies the inequality but proves nothing about the theorem's actual content, that a fixed, dimension-independent $k$ works uniformly over all points of the hull. The formal statement quantifies $T$ , then $x$ , then $k$ , and only then asserts existence of the $x_1,\dots,x_k$ , exactly in that order.

Classical Carathéodory (Theorem 0.0.1, stated for context in the source but not used by either formalized result's proof) is not drafted here: Mathlib already proves the corresponding statement via affine independence (Caratheodory.eq_pos_convex_span_of_mem_convexHull, Analysis/Convex/Caratheodory.lean), from which the book's " $n+1$ points" bound follows via AffineIndependent.card_le_finrank_succ. It is not added as a kind: reference milestone because no corresponding theorem is yet published on the Prove2Me platform to point at (checked 2026-09-17: GET /theorems?q=Caratheodory returns only unrelated tropical-convexity results), and re-drafting existing Mathlib content as a new platform theorem would duplicate rather than reuse it.

Selected references

R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, DOI 10.1017/9781108231596, Appetizer (pp. 1–5).
G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle (Maurey–Schwartz), 1980–1981, exposé no. 5. numdam.org/item/SAF_1980-1981____A5_0
B. Carl, "Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces," Annales de l'Institut Fourier, 35(3), 1985, 79–118. numdam.org/item/AIF_1985__35_3_79_0

2 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Introduction to Stochastic Programming VI: Jensen and Edmundson-Madansky BoundsTextbook

Motivation

Two-stage stochastic programs with recourse require evaluating $Q(x) = \mathbb E_\xi[Q(x,\xi)]$ , the expected value of a recourse function, at every candidate first-stage decision $x$ . When $\xi$ is high-dimensional or continuously distributed, this expectation is a multivariate integral of a piecewise-linear, generally nondifferentiable integrand, and classical quadrature rules — built for smooth integrands in low dimension — do not apply (Birge & Louveaux, §8.1). What does apply is convexity: $Q(x,\cdot)$ is convex whenever the recourse problem is a linear program in $\xi$ , and convexity alone is enough to sandwich $\mathbb E_\xi[Q(x,\xi)]$ between two computable discrete approximations. This chapter develops that sandwich, and it is the standard device used throughout the stochastic-programming literature to bound and iteratively refine the recourse function: the lower bound goes back to Jensen [1906]; the upper bound is due to Edmundson [1956] and Madansky [1959], with the mean-consistent LP refinement due to Madansky [1960] and Gassmann & Ziemba [1986]. Refinements of both bounds appear in Huang, Ziemba & Ben-Tal [1977], Kall & Stoyan [1982] and Frauendorfer [1988].

Setting

Fix a probability space $(\Omega, \mathcal F, P)$ and an integrand $g : D \times \Xi \to \mathbb R$ , where $\Xi \subseteq E$ is the (convex, closed) support of a random vector $\xi : \Omega \to \Xi$ and $E$ is a real vector space (in the recourse application, $g(x,\cdot) = Q(x,\cdot)$ and $D$ is the first-stage feasible region). Write $\mathbb E(g(x)) = \mathbb E_\xi[g(x,\xi)] = \int_\Xi g(x,\xi)\, P(d\xi)$ .

A partition of $\Xi$ into $\nu$ measurable blocks $S^\nu = \{S_1,\dots,S_\nu\}$ determines, for each block, its probability $p_l = P[\xi \in S_l]$ and its conditional mean $\xi^l = \mathbb E[\xi \mid S_l]$ . Equivalently — and this is the convention this mission's Lean development uses — the blocks may be taken directly on the sample space as the pulled-back sets $S_l = \xi^{-1}(\text{region}_l) \subseteq \Omega$ , with $p_l = P(S_l)$ and $\xi^l = p_l^{-1}\int_{S_l}\xi\,dP$ the Bochner integral average of $\xi$ over the block; the two descriptions coincide.

Formalization targets

Goal — Chapter 8, Theorem 1 (Jensen lower bound), p. 346

g(x,\cdot) \text{ convex on } \Xi \ \Longrightarrow\ \mathbb E(g(x)) \ \ge\ \sum_{l=1}^{\nu} p_l\, g(x,\xi^l).

This is the sharpest statement the chapter proves for the lower bound: it holds for every finite measurable partition, with no assumption beyond convexity of $g(x,\cdot)$ and integrability.

Chapter 8, Theorem 2 (Edmundson-Madansky upper bound), pp. 347-348

For $\Xi$ compact, let $\mathrm{ext}\,\Xi$ be the extreme points of $\mathrm{co}\,\Xi$ , carrying the Borel field of all its subsets. If, for every $\xi \in \Xi$ , $\varphi(\xi,\cdot)$ is a probability measure on $\mathrm{ext}\,\Xi$ with barycenter $\xi$ (i.e. $\int_{\mathrm{ext}\,\Xi} e\,\varphi(\xi,de) = \xi$ ) and $\omega \mapsto \varphi(\xi(\omega), A)$ is measurable for every $A$ , then

\mathbb E(g(x)) \ \le\ \int_{\mathrm{ext}\,\Xi} g(x,e)\, \lambda(de), \qquad \lambda(A) = \int_\Omega \varphi(\xi(\omega), A)\, P(d\omega).

Together the two targets give the chapter's headline sandwich: for convex $g(x,\cdot)$ , the finite-partition Jensen value and the Edmundson-Madansky value bracket the true expectation, and refining the partition (resp. the disintegration) tightens both sides toward it.

Significance

The Jensen bound is the workhorse of discrete-distribution approximation in stochastic programming: it is what makes $Q^\nu(x) = \sum_l p_l Q(x,\xi^l)$ a valid, refinable lower-approximation of the true recourse function, and it underlies the partition-refinement schemes (§8.2, following Birge & Wets [1986] and Frauendorfer & Kall [1988]) used inside the $L$ -shaped method and separable-programming solvers described later in the chapter (§8.3). The Edmundson-Madansky bound is its indispensable upper counterpart: without it there is no certificate of how far a lower approximation can be from the truth, and the mean-consistent LP refinement (eq. 2.9, not part of this mission) reduces to a moment-problem computation over $\lambda$ . Both bounds are, to date, unformalized: the platform holds no theorem matching either a finite-partition conditional-Jensen inequality or an extreme-point disintegration bound (searched GET /theorems?q=... for "Jensen", "conditional expectation", "Edmundson Madansky", "partition convex" — no relevant hits), so this mission is a first formalization of both, not a reformulation of existing platform content. Mathlib supplies the raw convexity substrate this mission is built from — finite Jensen (Analysis/Convex/Jensen.lean) and, critically, the set-average integral Jensen inequality (ConvexOn.map_set_average_le in Analysis/Convex/Integral.lean), exactly the per-block step the book's proof of Theorem 1 performs — but no existing lemma assembles these into the partitioned, conditional-mean statement the book actually states.

Difficulty

The obvious shortcut is to prove "convex functions lie above their tangent line" and stop — this captures no partition structure at all and is not the theorem the book states (the theorem is about $\Sigma_l p_l g(x,\xi^l)$ , a sum over blocks, not a single linearization). The real content is bookkeeping across the partition: writing $\mathbb E(g(x))$ as $\sum_l P(S_l)\,\mathbb E[g(x,\xi)\mid S_l]$ (an exact identity, no convexity needed), then applying ordinary Jensen inside each block to replace $\mathbb E[g(x,\xi)\mid S_l]$ by $g(x,\xi^l)$ from below — the inequality only enters at the second step, once per block. Proving this in Lean means correctly discharging, for every block, the side conditions Mathlib's integral-Jensen lemma needs (closedness of $\Xi$ , continuity of $g(x,\cdot)$ on $\Xi$ , integrability on the block) and then summing the $\nu$ per-block inequalities against weights $p_l$ that themselves depend on the partition — an easy step to get wrong by, e.g., letting $\xi^l$ be an arbitrary point of $S_l$ rather than exactly its conditional mean, which understates what Jensen actually forces. Theorem 2 additionally requires setting up the disintegration $\lambda$ correctly: $\lambda$ is a probability measure defined as an integral of the kernel-like family $\varphi$ against $P\circ\xi^{-1}$ , and both the barycenter condition on $\varphi$ and the measurability of $\omega \mapsto \varphi(\xi(\omega),A)$ are load-bearing — dropping either makes $\lambda$ ill-defined or the bound's proof inapplicable.

Formalization scope

$\Xi \subseteq E$ for $E$ a complete real normed vector space (NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E); no finite-dimensionality is assumed since neither theorem's proof needs it. The parameter $x$ ranges over an arbitrary type $\alpha$ with $D \subseteq \alpha$ , and $g$ is left as a bare function α → E → ℝ, matching the book's level of abstraction (the recourse LP's own data $A,b,c,q,W,T,h$ is never used in either proof).

The partition is formalized directly on the sample space $\Omega$ (a Partition structure: pairwise-disjoint measurable blocks covering $\Omega$ , each of positive measure) rather than on $\Xi$ , per the equivalence noted under Setting; $\xi^l$ is defined as the Bochner-integral average $p_l^{-1}\int_{S_l}\xi\,dP$ , so it is forced to be the conditional mean and cannot be weakened to an arbitrary sample point of the block — the change the chunk brief flags as the main faithfulness trap for this chapter.

Two explicit hypotheses are added beyond the book's own statement of Theorem 1, both needed by Mathlib's integral-Jensen lemma rather than narrowings of the mathematical content: ContinuousOn (g x) Ξ (finite-dimensional convex functions are automatically continuous on the interior of their domain, which is what the book implicitly relies on; stated explicitly since $E$ is not assumed finite-dimensional) and integrability of $\xi$ and of $g(x,\xi(\cdot))$ (needed for $\mathbb E(g(x))$ and each $\xi^l$ to be well-defined). For Theorem 2, the disintegrating family $\varphi$ is E → Measure Ext for an abstract type Ext (standing for $\mathrm{ext}\,\Xi$ ) with the discrete MeasurableSpace (every subset measurable, matching the book's "Borel field ... the collection of all subsets"), mapped into $E$ by an embedding toE whose range is exactly (convexHull ℝ Ξ).extremePoints ℝ; the measure $\lambda$ (named μExt in the Lean code, since λ is a reserved keyword) is a hypothesis satisfying its defining equation (2.6) rather than constructed, since constructing a measure from a set function is a separate, book-external piece of measure theory the chapter's own proof does not perform either — it simply asserts $\lambda$ is the probability measure with that value on every set.

A trivializing formalization is ruled out explicitly: a version that lets $\xi^l$ range over an arbitrary point of $S_l$ , or that proves only the ordinary (unconditional) Jensen inequality without ever introducing the partition, states something strictly weaker than the book and is not what is formalized here.

Both draft theorems end in := by sorry; a full Lean proof of Theorem 1 combines Mathlib's ConvexOn.map_set_average_le applied per block with the exact decomposition of $\int_\Omega$ into $\sum_l \int_{S_l}$ over the partition's disjoint, covering blocks. Reusable beyond this mission: the Partition structure and its weight/condMean accessors generalize to any chapter needing a finite measurable partition with conditional means (this book's later approximation schemes, §8.2-8.5 and Chapter 10, all build on the same device). Contributions solving either theorem, or formalizing the partition-refinement monotonicity $\mathbb E(g(x)) \ge \mathbb E^{\nu+1}(g(x)) \ge \mathbb E^\nu(g(x))$ (eq. 2.3, not part of this mission's milestone list since it is not itself a numbered theorem) as a follow-up, are welcome.

Selected references

J.R. Birge, 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
J.L.W.V. Jensen, Sur les fonctions convexes et les inégalités entre les valeurs moyennes, Acta Mathematica 30 (1906), 175-193. https://doi.org/10.1007/BF02418571
H.P. Edmundson, Bounds on the expectation of a convex function of a random variable, The RAND Corporation, Paper 982, 1956.
A. Madansky, Bounds on the expectation of a convex function of a multivariate random variable, Annals of Mathematical Statistics 30 (1959), 743-746. https://doi.org/10.1214/aoms/1177706207
A. Madansky, Inequalities for stochastic linear programming problems, Management Science 6 (1960), 197-204. https://doi.org/10.1287/mnsc.6.2.197
H.I. Gassmann, W.T. Ziemba, A tight upper bound for the expectation of a convex function of a multivariate random variable, Mathematical Programming Study 27 (1986), 39-53. https://doi.org/10.1007/BFb0121114
J.R. Birge, R.J-B. Wets, Designing approximation schemes for stochastic optimization problems, in particular for stochastic programs with recourse, Mathematical Programming Study 27 (1986), 54-102. https://doi.org/10.1007/BFb0121122

3 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Introduction to Stochastic Programming II: The Value of Perfect Information and of the Stochastic SolutionTextbook

Motivation

Every stochastic program is, in practice, compared against a shortcut. A decision maker facing genuine uncertainty is tempted either to replace the random data by its mean and solve one deterministic problem, or to imagine that perfect information about the future were available and solve a separate deterministic problem per scenario. Both temptations have precise answers: the expected value of perfect information (EVPI) measures how much a decision maker should be willing to pay for a perfect forecast, and the value of the stochastic solution (VSS) measures the cost of ignoring uncertainty altogether by solving the mean-value problem. Both concepts originate in decision analysis — EVPI traces to Raiffa and Schlaifer (1961) — and were brought into stochastic programming by Madansky (1960), who proved the first chain of inequalities relating the wait-and-see value, the recourse value and the expected-value-solution's cost. Birge and Louveaux, Introduction to Stochastic Programming, 2nd ed. (Springer, 2011), Chapter 4, gives the standard modern treatment, including a refined family of bounds — built from pairs subproblems against a chosen reference scenario — that sharpen VSS beyond the original mean-scenario comparison. This mission formalizes that chapter's capstone: the five-quantity, four-inequality chain that pins VSS between two computable optimal values.

Setting

Fix a two-stage stochastic program with fixed recourse: a finite family of K scenarios $\xi_1,\dots,\xi_K$ in $\mathbb R^d$ , each occurring with probability $p_k \ge 0$ , $\sum_k p_k = 1$ ; a first-stage feasible set $K_1 \subseteq \mathbb R^{n_1}$ ; and, for every first-stage decision $x \in \mathbb R^{n_1}$ and every scenario $\xi \in \mathbb R^d$ , a scenario cost $z(x,\xi)$ — the optimal value of $c^Tx + \min\{q^Ty \mid Wy = h(\xi) - Tx,\ y \ge 0\}$ . By convention $z(x,\xi) = +\infty$ when $x$ has no feasible second-stage recourse under $\xi$ , and $z(x,\xi) = -\infty$ when the second-stage program is unbounded below.

From $z$ , five basic quantities are defined (Birge & Louveaux §4.1–§4.2):

The recourse problem's value, $RP = \min_{x \in K_1} \mathbb E_\xi\, z(x,\xi)$ — the best a decision maker can do without foreknowledge of $\xi$ (the "here-and-now" solution).
The wait-and-see value, $WS = \mathbb E_\xi\big[\min_{x \in K_1} z(x,\xi)\big]$ — the average cost if $\xi$ were revealed before choosing $x$ .
The expected value of perfect information, $EVPI = RP - WS$ .
The expected value problem's solution $\bar x(\bar\xi)$ , optimal for the deterministic problem at the mean scenario $\bar\xi = \mathbb E(\xi)$ ; its recourse cost, the expected result of using the EV solution, is $EEV = \mathbb E_\xi\, z(\bar x(\bar\xi), \xi)$ .
The value of the stochastic solution, $VSS = EEV - RP$ — the extra cost of implementing the mean-scenario decision instead of solving the recourse problem.

Section 4.6 refines VSS by replacing the mean scenario with an arbitrary reference scenario $\xi^r$ (not necessarily one of the $K$ possible scenarios, e.g. a worst case), with assumed probability $p_r = P(\xi=\xi^r)$ :

$\bar x^r$ , optimal for $\min_{x\in K_1} z(x,\xi^r)$ , gives the expected value of the reference-scenario solution, $EVRS = \mathbb E_\xi\, z(\bar x^r,\xi)$ , and the generalized $VSS = EVRS - RP$ .
For each scenario $\xi^k$ , the pairs subproblem of $\xi^r$ and $\xi^k$ treats them as a two-point distribution with weights $p_r$ and $1-p_r$ : its optimal value is $\min_{x\in K_1}\big[p_r\,z(x,\xi^r) + (1-p_r)\,z(x,\xi^k)\big]$ , attained at some $\bar x^k$ . Averaging these optimal values over $k$ (rescaled by $1/(1-p_r)$ ) gives the sum of pairs expected values, $SPEV$ . Taking, instead, the smallest full expected cost $\mathbb E_\xi\,z(\bar x^k,\xi)$ among the $K{+}1$ candidate solutions $\{\bar x^1,\dots,\bar x^K,\bar x^r\}$ gives the expectation of pairs expected value, $EPEV$ .

Formalization targets

Goal — Chapter 4, Theorem 9 (p. 174)

0 \;\le\; EVRS - EPEV \;\le\; VSS \;\le\; EVRS - SPEV \;\le\; EVRS - WS .

Four links, each with independent content: nonnegativity of the leftmost gap, then two genuine inequalities (from the pairs-subproblem comparisons of Propositions 7 and 8), then the identity $VSS = EVRS - RP$ folded against $RP \ge WS$ 's reverse-direction cousin. This is the weakest statement that keeps all five quantities distinct — stating only the outer bound $0 \le VSS \le EVRS-WS$ would erase exactly the refinement (via pairs subproblems) that makes the chapter's method useful.

Supporting propositions (milestones, in attack order)

Proposition 1 (p. 166): $WS \le RP \le EEV$ .
Proposition 5(a) (pp. 167–168): $0 \le EVPI$ and $0 \le VSS$ (mean-scenario form), for any stochastic program.
Proposition 7 (p. 173): $WS \le SPEV \le RP$ .
Proposition 8 (p. 174): $RP \le EPEV \le EVRS$ .

Significance

The chain gives a decision maker two computable, non-obvious bounds on VSS — a quantity that is otherwise expensive to pin down exactly, since $RP$ itself already requires solving the full recourse problem. $EVRS - EPEV$ and $EVRS - SPEV$ are both computable from $K+1$ (or $K$ ) two-scenario LPs, far cheaper than the full $K$ -scenario recourse problem, so Theorem 9 turns an expensive exact quantity into a pair of cheap certified bounds. Formalizing it fixes, once and for all, the exact hypotheses and quantifier structure of Madansky's original inequality (Proposition 1) together with the later pairs-subproblem refinement (Propositions 6–8, Birge 1982), often cited informally as "the VSS bounds" without distinguishing $EEV$ , $EVRS$ , $EPEV$ and $SPEV$ . No part of this chain is on Mathlib or Formalpedia today (checked by concept query, not title); this is a first, from-scratch treatment of two-stage recourse value-of-information theory as formal objects.

Difficulty

The obvious first idea — collapse $RP$ , $WS$ , $EV$ , $EEV$ , $EVRS$ , $EPEV$ , $SPEV$ to one "the optimal value of the LP" and prove a single inequality — throws away the entire content of the chapter. Each quantity restricts the minimization to a different feasible object: $RP$ minimizes jointly over $x$ ; $WS$ swaps the order of $\min$ and $\mathbb E$ ; $EEV$ / $EVRS$ evaluate one fixed $x$ under every scenario; $SPEV$ and $EPEV$ each minimize over a family of pairs subproblems rather than the full $K$ -scenario problem. The chain's proof (Propositions 7–8) depends on this precisely: Proposition 7's lower bound uses that each pairs-subproblem-optimal $(\bar x^k,\bar y^k)$ is feasible (not necessarily optimal) for the single-scenario problem at $\xi^r$ , and its upper bound uses that the recourse-optimal $(x^*, y^*(\xi^r), y^*(\xi^k))$ is feasible (not necessarily optimal) for the pairs subproblem — a feasible-but-not-optimal argument in each direction, not a direct comparison of objective values. Losing track of which solution is fixed and which is optimized destroys the argument entirely.

Formalization scope

An Instance bundles the finite scenario set (Fin K, probabilities p : Fin K → ℝ with p ≥ 0, ∑ p = 1, scenarios xi : Fin K → (Fin d → ℝ)), the first-stage feasible set K1 : Set (Fin n1 → ℝ), and the scenario cost z : (Fin n1 → ℝ) → (Fin d → ℝ) → EReal, using the extended reals to carry the book's own +∞/−∞ conventions for infeasibility and unboundedness rather than silently restricting to a finite-valued special case (a genuine risk of trivialization here, since Example 2 of the chapter exhibits $EEV = +\infty$ ). All optimal values (RP, WS, EV, EVPI, EEV, VSS, EVRS, generalized VSS, SPEV, EPEV) are defined directly from z, matching the book's own level of abstraction in this chapter (which never unfolds z into the underlying LP's $A,b,c,q,W,T,h$ data — those appear only in Chapter 3). Because EEV, the mean-scenario VSS, EVRS, the generalized VSS, and EPEV are each defined relative to an optimal solution of some sub-problem — the book itself only ever says "let $\bar x(\bar\xi)$ denote some optimal solution" — every theorem using them states that solution and its optimality as explicit hypotheses (x ∈ K1 and z x … = ⨅ …), never baking it into a Classical.choiced value; this keeps the quantifier structure faithful to the book's own "let ... be an optimal solution" phrasing. Proposition 5's part (b) — the upper bound $EVPI \le EEV-EV$ , $VSS \le EEV-EV$ "for stochastic programs with fixed recourse matrix and fixed objective coefficients" — needs a different scope: that hypothesis is a structural property of the underlying LP data ( $W$ , $c$ , $q$ fixed across scenarios) invisible once $z$ is abstracted away as above, and pinning it down would require modeling the LP's $A,b,c,q,W,T,h(\xi)$ data explicitly (as Chapter 3's mission does for its convexity theorem). That part is out of scope here and is not needed for Theorem 9's own chain, which rests only on Proposition 5(a).

Collapsing any two of $RP$ , $WS$ , $EV$ , $EEV$ , $EVRS$ , $EPEV$ , $SPEV$ to a single "value of the LP" — the trivialization this book-wide series flags for Chapter 4 — is ruled out by construction: each is its own definition over its own feasible object, and Theorem 9's statement names all five quantities in the chain rather than only its outer bound. The two occurrences of "VSS" in the chapter (the original mean-scenario $EEV-RP$ of §4.2, and the reference-scenario $EVRS-RP$ generalization of §4.6, used only in Theorem 9) are likewise kept as two distinct definitions rather than conflated under one name.

Every addition and subtraction between EReal values in this mission — inside expect, WS, EVPI, VSS, EVRS's appearance in VSSRef, the pair sum inside pairsValue, the sum inside SPEV, and all four differences in Theorem 9's own chain — uses three explicit operations, badd/bsub/bsum, that implement the book's own convention (p. 164) that +∞ (infeasibility) dominates, i.e. (+∞)+(−∞)=+∞, rather than Mathlib's native EReal addition, whose ⊤+⊥=⊥ would make VSS ≥ 0 (Proposition 5(a)) and the goal's own leftmost inequality false whenever a witness solution is infeasible in a positive-probability scenario — exactly the situation of the book's own Example 2 (pp. 174-175). The reference scenario's probability $p_r=\Pr(\xi=\xi^r)$ (p. 172) is likewise not a free parameter but a definition, refProb, computed from the instance itself as $\sum_{k:\,\xi^k=\xi^r}p_k$ ; SPEV's sum is correspondingly restricted to the scenarios other than the reference scenario ( $\xi^k\ne\xi^r$ ), matching the book's own proof of Proposition 7, which uses $\sum_{k\ne r}p_k=1-p_r$ . The single hypothesis refProb I xir < 1 on Propositions 7, 8 and the goal says that some other scenario remains possible, which the book's own $(1-p_r)^{-1}$ factor presupposes.

Reusable beyond this mission: the Instance definition and the RP/WS/EV quantities are the natural base for any later chapter of this series that needs the two-stage recourse value (e.g. Chapter 3's convexity mission, Chapter 5's L-shaped method); contributions extending this Instance to the full LP data of the underlying two-stage program, or adding Proposition 5(b) and Proposition 2's Jensen-inequality argument on top of it, are welcome.

Selected references

J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, 2011, Chapter 4. DOI: 10.1007/978-1-4614-0237-4
A. Madansky, "Inequalities for Stochastic Linear Programming Problems", Management Science 6(2), 1960, 197–204.
H. Raiffa and R. Schlaifer, Applied Statistical Decision Theory, Harvard Business School, 1961.
J.R. Birge, "The Value of the Stochastic Solution in Stochastic Linear Programs with Fixed Recourse", Mathematical Programming 24(1), 1982, 314–325.

7 thms2 active usersReviewed

Analysis Partial Differential Equations·Captain: Lucas

Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper

Motivation

Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical $\Phi^4_3$ model $\partial_t u = \Delta u - u^3 + \xi$ on the three-dimensional torus, the KPZ equation $\partial_t h = \partial_x^2 h + (\partial_x h)^2 - \infty + \xi$ , and the parabolic Anderson model $\partial_t u = \Delta u + u\,\xi$ all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's A theory of regularity structures (Invent. Math. 198 (2014) 269–504, arXiv:1303.5113) develops a calculus in which such products, and the resulting fixed-point problems, become well posed.

The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on $\mathbb{R}^d$ with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper.

Setting

Fix a dimension $d$ and a scaling $s = (s_1,\dots,s_d)$ of positive integers, with $|s| = \sum_i s_i$ , and put $\|x\|_s = \max_i |x_i|^{1/s_i}$ . For $\delta > 0$ , a point $x \in \mathbb{R}^d$ and a test function $\varphi$ , the rescaled test function is

(S^{\delta}_{s,x}\varphi)(y) = \delta^{-|s|}\,\varphi\!\left(\frac{y_1-x_1}{\delta^{s_1}},\dots,\frac{y_d-x_d}{\delta^{s_d}}\right).

Write $\mathcal{B}^r_{s,0}$ for the set of test functions supported in $\{\|y\|_s \le 1\}$ whose derivatives up to order $r$ are bounded by $1$ . For $\alpha<0$ , a distribution $\xi$ belongs to the Hölder–Besov space $\mathcal{C}^\alpha_s$ if, on every compact set $K$ , $|\langle \xi, S^{\delta}_{s,x}\eta\rangle| \le C\delta^{\alpha}$ uniformly over $x\in K$ , $\delta \in (0,1]$ and $\eta \in \mathcal{B}^r_{s,0}$ with $r=-\lfloor\alpha\rfloor$ .

A regularity structure $(A,T,G)$ consists of an index set $A \subseteq \mathbb{R}$ containing $0$ , bounded below and locally finite; a graded vector space $T = \bigoplus_{\alpha\in A} T_\alpha$ with $T_0 \cong \mathbb{R}$ spanned by a unit $\mathbf{1}$ ; and a group $G$ of linear operators on $T$ with $\Gamma a - a \in \bigoplus_{\beta<\alpha}T_\beta$ for $a \in T_\alpha$ , and $\Gamma\mathbf{1} = \mathbf{1}$ . Elements of $T_\alpha$ are "homogeneous of order $\alpha$ ": they are placeholders for objects whose size at scale $\varepsilon$ is $\varepsilon^{\alpha}$ .

A model $(\Pi,\Gamma)$ assigns to each point $x$ a linear map $\Pi_x : T \to \mathcal{D}'(\mathbb{R}^d)$ and to each pair $(x,y)$ an element $\Gamma_{xy}\in G$ , subject to $\Gamma_{xx}=\mathrm{id}$ , $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$ , $\Pi_y = \Pi_x\circ\Gamma_{xy}$ and, locally uniformly, the analytic bounds

|(\Pi_x a)(S^{\delta}_{s,x}\varphi)| \lesssim \|a\|_\ell\,\delta^{\ell}, \qquad \|\Gamma_{xy}a\|_m \lesssim \|a\|_\ell\,\|x-y\|_s^{\ell-m}, \qquad a \in T_\ell,\; m<\ell.

A modelled distribution of order $\gamma$ is a function $f : \mathbb{R}^d \to T_{<\gamma}$ such that on every compact $K$

|||f|||_{\gamma;K} = \sup_{x\in K,\ \beta<\gamma}\|f(x)\|_\beta + \sup_{\substack{x,y \in K,\ \|x-y\|_s\le 1 \\ \beta<\gamma}} \frac{\|f(x)-\Gamma_{xy}f(y)\|_\beta}{\|x-y\|_s^{\gamma-\beta}} < \infty;

the space of these is $\mathcal{D}^\gamma$ , and $\mathcal{D}^\gamma(V)$ if $f$ takes values in a sector $V$ , that is, a graded $G$ -invariant subspace vanishing in degrees below its regularity.

Formalization targets

Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$

With $\alpha = \min A < 0$ and $r$ the order attached to $A$ , for every $f \in \mathcal{D}^\gamma$ with $\gamma>0$ there is a unique distribution $\mathcal{R}f \in \mathcal{C}^\alpha_s$ with

\big|(\mathcal{R}f - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \lesssim \delta^{\gamma} \qquad (x \in K,\ \delta\in(0,1],\ \eta\in\mathcal{B}^r_{s,0}).

The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants.

Milestone level — the calculus around the reconstruction operator

The uniqueness clause of Theorem 3.10 in isolation; the existence of a linear reconstruction operator for arbitrary $\gamma \in \mathbb{R}$ (for $\gamma\le 0$ the bound no longer pins it down); Corollary 3.16, improving the regularity of $\mathcal{R}f$ to $\mathcal{C}^\beta_s$ when $f$ takes values in a sector of regularity $\beta$ ; Proposition 3.31, that for $\nu>0$ the action of $\Pi$ on $T_\nu$ is determined by $\Gamma$ and by $\Pi$ in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of $f_1 \in \mathcal{D}^{\gamma_1}(V)$ and $f_2\in\mathcal{D}^{\gamma_2}(W)$ lies in $\mathcal{D}^{\gamma}$ with $\gamma = (\gamma_1+\alpha_2)\wedge(\gamma_2+\alpha_1)$ .

Significance

The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces $\mathcal{D}^\gamma$ carry no information about actual distributions.

Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces $\mathcal{C}^\alpha_s$ that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the $\Phi^4_3$ and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one.

Difficulty

The naive construction fails: setting $\mathcal{R}f := \Pi_x f(x)$ for a fixed $x$ is wrong away from $x$ , and the pointwise limit $\lim_{\delta\to0}$ of localisations of $\Pi_x f(x)$ around each $x$ does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling $s$ : one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the $\mathcal{D}^\gamma$ bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for $\gamma>0$ is by contrast short, and is listed as a separate milestone.

Formalization scope

The development commits to the following conventions, fixed in the mission's definition files. Points of $\mathbb{R}^d$ are Fin d → ℝ. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by $0$ to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's $\mathcal{B}^r_{s,0}$ consists of $C^r$ functions; here it consists of smooth ones, which defines the same spaces $\mathcal{C}^\alpha_s$ . The model space is the algebraic direct sum $\bigoplus_{a\in A} T_a$ over the index set, each $T_a$ a real normed space, with $Q_a$ the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces $V_a \subseteq T_a$ ; Hairer's requirement that each $V_a$ admit a complement is automatic in this algebraic setting. The integer $r$ appearing in the model bounds is the smallest one with $\ell > -r$ for all $\ell \in A$ , which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in $\mathcal{C}^\alpha_s$ , and uniqueness simultaneously.

Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on $\mathbb{R}^d$ , the elementary theory of $\mathcal{C}^\alpha_s$ (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates.

Selected references

M. Hairer, A theory of regularity structures, Inventiones Mathematicae 198 (2014) 269–504. arXiv:1303.5113, DOI:10.1007/s00222-014-0505-4
T. Lyons, Differential equations driven by rough signals, Revista Matemática Iberoamericana 14 (1998) 215–310. DOI:10.4171/RMI/240
M. Gubinelli, Controlling rough paths, Journal of Functional Analysis 216 (2004) 86–140. arXiv:math/0306433
M. Gubinelli, P. Imkeller, N. Perkowski, Paracontrolled distributions and singular PDEs, Forum of Mathematics Pi 3 (2015) e6. arXiv:1210.2684
Y. Bruned, M. Hairer, L. Zambotti, Algebraic renormalisation of regularity structures, Inventiones Mathematicae 215 (2019) 1039–1156. arXiv:1610.08468

13 thms2 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: burkh4rt

The Bunkbed Conjecture is FalseResearch Paper

Motivation

Let $G=(V,E)$ be a finite connected graph. In Bernoulli bond percolation each edge is independently retained with probability $P$ and deleted otherwise, and one writes $\mathbb{P}_P[u \leftrightarrow v]$ for the probability that vertices $u$ and $v$ lie in the same component of the resulting random subgraph. Comparing such connection probabilities is a basic and genuinely hard problem: computing them exactly is $\#\mathsf{P}$ -hard.

The bunkbed graph is built from two copies of $G$ , joined by vertical edges called posts above a chosen set $T \subseteq V$ of transversal vertices. Percolation is performed on the two copies while every post is retained. Writing $v$ for a vertex in the lower copy and $v'$ for its counterpart upstairs, Kasteleyn conjectured in 1985 that being connected within a level is always at least as likely as crossing between levels.

The conjecture is intuitively compelling — crossing levels appears to require "using up" a post — and it resisted proof for forty years. A short timeline:

1985 — Kasteleyn formulates the conjecture; it is recorded as Remark 5 of van den Berg–Kahn (2001), which is how the source cites it.
Positive results accumulate for special cases: wheels, complete graphs, complete bipartite graphs, graphs symmetric with respect to an automorphism exchanging $u$ and $v$ , one or two transversal vertices, and in the $P \uparrow 1$ limit.
2024 — Hollom refutes the $3$ -uniform hypergraph analogue. This alone does not settle the graph case: it is impossible to simulate a single $3$ -hyperedge by bond percolation on a gadget graph.
2025 — Gladkov, Pak and Zimin disprove the conjecture outright, with an explicit counterexample and without computer assistance.

Section 7 of the source is a candid account of a large-scale machine-learning-guided search that failed to find a counterexample, and of why the problem is unusually ill-suited to experimental testing.

Setting

Fix a finite graph with vertex set $V$ and edge set $E$ , and a retention function $w : E \to [0,1]$ (the uniform case is $w \equiv P$ ). A configuration is a subset $S \subseteq E$ of open edges, occurring with probability

\mathbb{P}(S) \;=\; \prod_{e \in S} w(e) \prod_{e \in E \setminus S} \bigl(1 - w(e)\bigr),

and $\mathbb{P}[u \leftrightarrow v]$ is the total probability of those $S$ for which $u$ and $v$ are connected in $(V, S)$ .

Given $T \subseteq V$ , the bunkbed graph has vertex set $V \times \{0,1\}$ . Its edges are a copy of $E$ in each level together with a post $\{(t,0),(t,1)\}$ for every $t \in T$ . In bunkbed percolation the two level-copies are percolated independently while all posts are retained; $\mathbb{P}^{\mathrm{bb}}$ denotes the resulting connection probabilities.

Formalization targets

Goal — the bunkbed conjecture is false

\neg\;\Bigl(\forall\,G \text{ connected},\ \forall\,T \subseteq V,\ \forall\,0<P<1,\ \forall\,u,v \in V:\quad \mathbb{P}^{\mathrm{bb}}_P[u \leftrightarrow v] \;\ge\; \mathbb{P}^{\mathrm{bb}}_P[u \leftrightarrow v'] \Bigr)

Supporting target — the explicit counterexample (Theorem 1.2)

\exists\, G,\ |V| = 7{,}222,\ |E| = 14{,}442,\ |T| = 3,\ \exists\, u,v:\qquad \mathbb{P}^{\mathrm{bb}}_{1/2}[u \leftrightarrow v] \;<\; \mathbb{P}^{\mathrm{bb}}_{1/2}[u \leftrightarrow v']

Supporting target — hyperedge simulation (Lemma 4.1)

For the gadget $G_n$ on $n+1$ vertices,

P_{abc}\,P_{a|b|c} \;-\; P_{ab|c}\,P_{ac|b} \;>\; \Bigl(n\tfrac{1-P}{1+P} - 1\Bigr) P_{a|bc}.

Significance

The result itself. A forty-year-old conjecture in percolation theory is false, and prior positive results are thereby sharpened rather than superseded: it becomes interesting to delimit exactly which families of graphs do satisfy the inequality. The refutation also settles the Counting, Weighted, Alternative and Computational variants listed in §8.1, and shows the random-cluster analogue cannot be pushed from $q=2$ down to $q=1$ .

Formalizing it. Nothing here is open; the mission produces machine-checked versions of published results, and as a by-product the first percolation theory in Lean. Mathlib currently contains no percolation of any kind — no connection probabilities, no bunkbed graph, no hypergraph percolation. That infrastructure is reusable far beyond this mission. The source itself notes (§8.2) that its central combinatorial lemma was independently verified by computer; a formal proof would replace that check with a certificate.

Difficulty

The obvious approach — exhibit a small graph and compute both probabilities — is hopeless, and the source explains why at length. A graph with $m$ edges has $2^m$ configurations; for the counterexample here the probability gap is on the order of $10^{-4331}$ , so no sampling argument can detect it, and exact enumeration is out of reach. Section 7 records a substantial computational search that found nothing and, in hindsight, could not have.

The proof is instead structural, and its difficulty is concentrated in one place. Hollom's refutation of the hypergraph version cannot be transferred directly, because a single $3$ -hyperedge cannot be simulated by bond percolation on any gadget graph. The source's answer is to prove a robust version of Hollom's lemma (Lemma 3.3) which survives the inexact simulation that gadget graphs do provide, and this robustness is what Lemma 4.1's inequality quantifies. Lemma 3.3 is proved by constructing a weight-preserving involution on a refined configuration space — the technical heart, and the milestone a solver should expect to spend the most effort on.

Formalization scope

The development commits to the following conventions.

Everything is finite and rational-valued, hence computable: connection probabilities are ℚ and evaluate by #eval, and small instances close by decide.
A graph is given by an explicit edge Finset and realised through SimpleGraph.fromEdgeSet; connectivity is Mathlib's SimpleGraph.Reachable.
Percolation is a sum over the powerset of the edge set, weighted as displayed above, of a reachability indicator. Edge weights are per-edge (Sym2 V → ℚ), since the gadget $G_n$ genuinely needs two different weights: its spokes are retained with probability $1-P$ and its path edges with probability $P$ .
In the bunkbed, level 0 is the lower copy; posts over T are unconditionally present and are not percolated. The two levels are percolated independently.
⚠️ Planarity is omitted from the goal. Theorem 1.2 asserts the counterexample is planar, and Mathlib has no notion of a planar graph — no IsPlanar, no Euler formula, no Kuratowski. Building one is a larger project than this mission. The formalized statement of Theorem 1.2 is therefore strictly weaker than the published one, and the goal is instead the negation of the conjecture, which is exactly the source's own "In particular, the BBC is false." Contributions adding planarity are welcome and would strengthen the milestone.
Ruling out a trivializing reading: the conjecture must be negated as stated, over all connected graphs, transversal sets and $0<P<1$ . Weakening it to a fixed graph, or to $P \in \{0,1\}$ , or dropping connectivity, would make the refutation vacuous.

Infrastructure. Mathlib supplies SimpleGraph, boxProd, Reachable with a DecidableRel instance, fromEdgeSet, edgeFinset and Finset.powerset. It supplies no percolation, so this mission ships two definition files: Bernoulli bond percolation with the bunkbed construction and the five triple-partition probabilities, and hypergraph percolation with Hollom's hypergraph and the Wierman–Ziff five-state model. One known gap: Mathlib's Reachable decision procedure enumerates walks and is far too slow to evaluate the $64$ -configuration check of Lemma 3.1 by decide. A solver will want a linear-time reachability procedure together with a proof that it agrees with Reachable; that is itself a worthwhile reusable contribution.

Selected references

J. van den Berg and J. Kahn, A correlation inequality for connection events in percolation, Ann. Probab. 29 (2001), 123–126 — Kasteleyn's conjecture appears as Remark 5.
T. Hollom, A new proof of the bunkbed conjecture in the $p \uparrow 1$ limit, Discrete Math. 347 (2024), 113711.
T. Hollom, The bunkbed conjecture is not robust to generalisation, arXiv:2406.01790 (2024).
T. Hutchcroft, P. Nizić-Nikolac, A. Kent, The bunkbed conjecture holds in the $p \uparrow 1$ limit, Comb. Probab. Comput. 32 (2023), 363–369.
N. Gladkov, I. Pak, A. Zimin, The bunkbed conjecture is false, Proc. Natl. Acad. Sci. USA 122 (2025), no. 24, e2420725122. doi:10.1073/pnas.2420725122; preprint arXiv:2410.02545.
J. C. Wierman and R. M. Ziff, Self-dual planar hypergraphs and exact bond percolation thresholds, Electron. J. Combin. 18 (2011).
G. R. Grimmett, Percolation, 2nd ed., Springer, 1999.

38 thms2 active usersReviewed

Completed

Machine Learning·Captain: naimengye

Speculative Actions: Cost-Latency Analysis for Agentic SpeculationResearch Paper

Motivation

An LLM agent acting in an environment spends most of its wall-clock time waiting. Each step — a model call, a tool or MCP request, a browser action, sometimes a human reply — must complete before the next can be issued, and the round trips dominate end-to-end latency: a chess game between two reasoning agents runs for hours, and an operating-system tuning task for tens of minutes. When a training or prompt-optimization loop repeats such a run thousands of times, the waiting is the cost.

Speculative actions (Ye, Ahuja, Liargkovas, Lu, Kaffes, Peng, ICLR 2026) transplants a classical systems idea — speculative execution in microprocessors, and speculative decoding for LLM inference — to the agent's environment loop. A cheap, fast speculator guesses the action a slow, authoritative actor is about to produce, the guess is used to launch the next environment call early, and the work is committed only when the actor's real action confirms the guess. The interface stays sequential and lossless; the internals run in parallel.

What makes this a formalization target rather than an engineering report is the paper's §5 cost–latency analysis. Speculating more branches buys hit probability but costs tokens, and the paper derives closed-form expressions for both sides of that trade — a self-contained piece of applied probability sitting underneath a systems paper. This mission asks for those expressions, machine-checked.

Setting

Fix a horizon $T$ and index steps $t = 0, 1, \dots, T-1$ . At each step a policy maps the state to an API call; the actor executes it with latency $\mathrm{Exp}(\beta)$ , while the speculator proposes candidate actions with latency $\mathrm{Exp}(\alpha)$ , where $\beta < \alpha$ (the speculator is faster in expectation). A speculative branch hits when the action it guesses implies the same next call the actor's true action would have implied; branches hit independently across steps with probability $p$ .

Two knobs define the two regimes analyzed. Breadth $k$ : at each step, launch $k$ independent one-step speculations in parallel, each immediately followed by a real call. At least one of the $k$ succeeds with probability

p(k) \;=\; 1 - (1-p)^k .

Depth: follow a single branch, extending it whenever a speculative or real call returns and pruning subtrees the actor contradicts.

The quantity driving both results is $S_n$ , the expected number of hits by round $n$ . A hit consumes the following step's speculation window — after a correct guess the next call is already cached, so no new speculation is launched there — which yields the two-term recursion

S_0 = 0, \qquad S_1 = p, \qquad S_n = p\,(1 + S_{n-2}) + (1-p)\,S_{n-1}.

Write $T_{\mathrm{seq}}, M_{\mathrm{seq}}$ for the latency and token cost of strictly sequential execution, and $T_{\mathrm{spec}}, M_{\mathrm{spec}}$ for their speculative counterparts. In the depth regime latencies are taken deterministic: $a$ for a real call, $b < a$ for a speculative one.

Target

The goal theorem is the finite-horizon latency ratio for breadth-focused speculation (Proposition 1), with $p(k)$ abbreviated $p_k$ :

\frac{\mathbb{E}[T_{\mathrm{spec}}]}{\mathbb{E}[T_{\mathrm{seq}}]} = 1 - \frac{1}{T}\,\frac{\alpha}{\alpha+\beta} \left[\frac{(T-1)p_k}{1+p_k} + \frac{p_k^2}{(1+p_k)^2} - \frac{p_k^2}{(1+p_k)^2}(-p_k)^{T-1}\right].

The supporting targets, ordered as the analysis builds them:

the closed form $S_n = \frac{p}{1+p}n + \frac{p^2}{(1+p)^2}\bigl(1 - (-p)^n\bigr)$ solving the recursion;
the per-hit saving $\mathbb{E}[(B-A)^+] = \frac{\alpha}{\beta(\alpha+\beta)}$ for independent $A \sim \mathrm{Exp}(\alpha)$ , $B \sim \mathrm{Exp}(\beta)$ ;
the $T \to \infty$ limit $1 - \frac{p_k}{1+p_k}\cdot\frac{\alpha}{\alpha+\beta}$ , and the resulting 50% ceiling: the latency reduction is strictly below $\tfrac12$ for every $p_k \le 1$ ;
the cost counterpart (Theorem 4), finite-horizon and in the limit, with $\tilde k$ the number of distinct actions across the $k$ branches;
the depth-focused time and cost identities (Theorem 6), whose latency coefficient is $p$ rather than $\frac{p}{1+p}$ — raising the speedup ceiling from $\tfrac12$ to $1$ ;
the structure of confidence-aware selective speculation (Theorem 3 and Corollary 5): with sorted per-branch confidences, the marginal hit-probability gain is non-increasing, so the optimal breadth is the greedy threshold rule "add a branch while $\Delta^\star \delta q(m) \ge c$ ".

Significance

The analysis is what turns speculation from a trick into a tunable system. Proposition 1 and Theorem 4 are governed by the same quantity $p_k$ , so a practitioner who can estimate hit probability can choose $k$ offline against a latency/cost budget rather than by trial. The 50% ceiling is a genuine negative result — it says breadth alone cannot do better, and motivates the depth regime, where the ceiling becomes 1. Theorem 3 explains why confidence-based branch selection is cheap in practice: the whole dynamic program collapses to one scalar continuation value, so a runtime system sorts confidences and adds branches greedily in $O(k)$ per step.

The paper's proofs are pen-and-paper and, as far as we are aware, none of these results has a machine-checked proof. Three parts reward formalization specifically. The recursion's closed form is derived by a characteristic-equation argument with a particular solution that collides with the homogeneous part — routine but error-prone. The per-hit saving is an honest two-dimensional integral over independent exponentials. And Theorem 6's cost expression is stated in the paper with a floor function and then immediately replaced by an approximation, so formalizing it forces a decision about which claim is actually being asserted (see Formalization scope).

Difficulty

The obvious first move on the recursion — guess a constant particular solution — fails, because $r = 1$ is a root of the characteristic polynomial $r^2 - (1-p)r - p$ and a constant trial collides with the homogeneous family; the particular solution is linear in $n$ , and the $\frac{p^2}{(1+p)^2}$ coefficient comes out of matching both initial conditions, not one.

The interesting hypothesis is the one the recursion's shape encodes and the prose states only in passing: a hit at round $t$ removes the speculation window at round $t+1$ . Drop it and the recursion becomes one-term and the answer changes.

For the per-hit saving, the difficulty is analytic rather than algebraic: the inner antiderivative of $(b-a)\alpha e^{-\alpha a}$ must be handled, and the outer integral runs over an unbounded interval, so integrability has to be established rather than assumed.

The asymptotic statements need the oscillating term $(-p_k)^{T-1}$ controlled uniformly — it is bounded, not vanishing termwise in an obvious way — before the $\tfrac1T$ prefactor can be taken to zero.

Formalization scope

Everything is over $\mathbb{R}$ . The model lives in one definition bundle, Def_SpecActions_model, in namespace SpecActions; the mission's Lean names match the prose symbols ( $S_n$ is hits, $p(k)$ is phit, $\tilde k$ is kt).

The model is formalized at the level the paper's own proofs use: $\mathbb{E}[T]$ and $\mathbb{E}[M]$ are defined by the expressions Appendix A derives for them (specTime, specCost, and their depth analogues), and the theorems assert the algebraic and asymptotic identities relating those quantities. Deriving those expressions from a measure-theoretic model of the execution trace is deliberately not in scope — with one exception: milestone 2 states the per-hit saving as a genuine iterated integral against the exponential densities, so the one probabilistic step the paper actually computes is formalized as an integral rather than assumed.

Conventions a solver should know before starting:

Statements are quantified over $\alpha, \beta > 0$ and $0 \le p_k \le 1$ ; the standing assumption $\beta < \alpha$ is not imposed, since none of the identities need it.
Finite-horizon statements carry $1 \le T$ , and $T-1$ is natural-number subtraction — the $T = 0$ case is excluded rather than silently truncated.
hits takes $p_k$ (the per-step hit probability $p(k)$ ), not the per-branch $p$ ; phit relates the two, and Thm_SpecActions_phit_bounds supplies the $0 \le p(k) \le 1$ range facts the other statements assume.
Theorem 6's cost is stated as the exact identity, not the paper's approximation. The paper gives an exact expression involving $\lfloor a/b \rfloor$ and then an $\approx$ form with $\frac{a}{2b} - \frac12$ ; these coincide only when $a/b$ is an integer. The milestone asserts the exact floor version, which is what the proof establishes.
The 50% ceiling is stated as the strict bound $\frac{p_k}{1+p_k}\cdot\frac{\alpha}{\alpha+\beta} < \frac12$ , which holds for all admissible parameters; the paper's "upper bound of 50%, occurring when $p=1$ and $\alpha = \infty$ " describes an unattained supremum.
Theorem 3's dynamic program is formalized as the two facts that carry its content — diminishing marginal returns, and optimality of the greedy threshold breadth — rather than as a Bellman recursion over a mode process, which would require a full MDP development.

Reusable beyond this mission: the two-term linear recursion solved in milestone 1, and the $\mathbb{E}[(B-A)^+]$ computation for independent exponentials, which is a standard fact absent from Mathlib. Contributions extending the model toward an actual measure on execution traces — deriving specTime rather than defining it — are welcome as follow-on work.

Selected references

Naimeng Ye, Arnav Ahuja, Georgios Liargkovas, Yunan Lu, Kostis Kaffes, Tianyi Peng. Speculative Actions: A Lossless Framework for Faster Agentic Systems. ICLR 2026. arXiv:2510.04371 — Proposition 1 (p. 4), Appendix A (pp. 13–14), Theorem 3 (p. 10), Theorem 4 (p. 19), Corollary 5 (p. 22), Theorem 6 (p. 23).
Yaniv Leviathan, Matan Kalman, Yossi Matias. Fast Inference from Transformers via Speculative Decoding. ICML 2023. arXiv:2211.17192 — the speculate-verify pattern at token level.
Wenyue Hua, Mengting Wan, Shashank Vadrevu, Ryan Nadel, Yongfeng Zhang, Chi Wang. Interactive Speculative Planning. 2024. arXiv:2410.00079 — depth-oriented speculation on a single planning branch.
Yilin Guan et al. Dynamic Speculative Agent Planning. 2025. arXiv:2509.01920 — online RL for choosing speculation depth under a cost-latency trade-off.
Robert M. Tomasulo. An Efficient Algorithm for Exploiting Multiple Arithmetic Units. IBM Journal of Research and Development, 1967. DOI:10.1147/rd.111.0025 — speculative execution in hardware.

13 thms2 active usersReviewed

Missions

High-Dimensional Statistics VI: The Lasso's l2-Error Bound under Restricted EigenvalueTextbook

Motivation

Setting

Formalization targets

Goal (Theorem 7.13(a) and its final sentence)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Orders VI: The Multivariate Stochastic OrderTextbook

From "larger" to "larger in every direction"

The usual multivariate stochastic order

Formalization targets

Goal: the coupling characterization (Theorem 6.B.1)

Supporting milestones

Significance

Difficulty

Formalization scope

Selected references

Support Vector Machines V: Bernstein's Inequality for Independent Hilbert-Space-Valued Random VariablesTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 6.14 (Bernstein's inequality in Hilbert spaces)

Supporting facts

Significance

Difficulty

Formalization scope

Selected references

Stochastic Orders V: The Laplace Transform OrderTextbook

Comparing distributions by their Laplace transforms

The Laplace transform order

Formalization targets

Goal: the integrated-survival-function characterization (Theorem 5.A.1)

Supporting milestones

Significance

Difficulty

Formalization scope

Selected references

High-Dimensional Statistics IV: Dudley's Entropy Integral BoundTextbook

Motivation

Setting

Formalization targets

Goal — Theorem 5.22 (Dudley's entropy integral bound)

Milestone — Proposition 5.17 (one-step discretization bound)

Milestone — Theorem 5.25 (the Gaussian comparison principle)

Significance

Difficulty

Formalization scope

Selected references

High-Dimensional Probability VII: Slepian's Inequality for Gaussian ProcessesTextbook

Motivation

Setting

Formalization targets

Slepian's inequality (Theorem 7.2.1, goal)

Sudakov-Fernique's inequality (Theorem 7.2.11, milestone)

Sudakov's minoration inequality (Theorem 7.4.1, milestone)

Slepian's inequality, finite-dimensional case (Theorem 7.2.9, milestone)

Significance

Difficulty

Formalization scope

Selected references

Foundations of Machine Learning IV: Support Vector Machines and the Margin BoundTextbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

High-Dimensional Statistics III: A Uniform Law via Rademacher ComplexityTextbook

Motivation

Setting

Formalization targets

Goal — Theorem 4.10 (a uniform law via Rademacher complexity)

Milestone — Proposition 4.11 (symmetrization sandwich)

Milestone — Eq. (4.16) (concentration around the mean)