Statistics

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization 3: The Big-M Relaxation Is at Least as Strong as PR(∞) for M ≤ ½√(λ0/λ2) and at Most as Strong for M ≥ √(λ0/λ2)Research Paper

Motivation

Best subset selection with a ridge term, the $\ell_0\ell_2$ -regularized least squares problem

\min_{\beta\in\mathbb R^p}\ \tfrac12\|y - X\beta\|_2^2 + \lambda_0\|\beta\|_0 + \lambda_2\|\beta\|_2^2,

is a standard model for sparse linear regression. It can be solved to certified optimality by branch-and-bound (BnB) over a mixed integer formulation, and the speed of BnB depends on how tight the lower bounds of its node relaxations are. Two mixed integer formulations are in common use: the Big-M formulation, which links each coefficient to a binary indicator through a box $|\beta_i| \le M z_i$ (Bertsimas, King and Mazumder, 2016), and the perspective formulation, which replaces $\beta_i^2$ by an auxiliary variable constrained by a rotated second-order cone (Frangioni and Gentile, 2006; Günlük and Linderoth, 2010). Which formulation gives the stronger continuous relaxation decides which one a solver should be built on.

Hazimeh, Mazumder and Saab (2021) compare the relaxations in Section 2. Their Proposition 2 compares the interval relaxation of the Big-M formulation with that of the perspective formulation without a box, $\mathrm{PR}(\infty)$ , studied by Dong, Chen and Linderoth (2015). This mission formalizes that comparison.

Setting

Fix a design matrix $X \in \mathbb R^{n\times p}$ , a response $y \in \mathbb R^n$ , parameters $\lambda_0, \lambda_2 > 0$ and a bound $M > 0$ . Write $[p] = \{1,\dots,p\}$ and $\|\beta\|_\infty \le M$ for $|\beta_i| \le M$ for every $i \in [p]$ .

The Big-M formulation (2) is

\min_{\beta, z}\ \tfrac12\|y - X\beta\|_2^2 + \lambda_0\sum_{i\in[p]} z_i + \lambda_2\|\beta\|_2^2 \quad\text{s.t.}\quad -Mz_i \le \beta_i \le Mz_i,\ z_i\in\{0,1\}.

Its interval relaxation replaces $z_i \in \{0,1\}$ by $z_i \in [0,1]$ ; its optimal value is $V_{B(M)}$ . Eliminating $z$ gives the equivalent form (37),

V_{B(M)} = \min_{\|\beta\|_\infty\le M} H(\beta),\qquad H(\beta) = \tfrac12\|y - X\beta\|_2^2 + \sum_{i\in[p]}\Big(\frac{\lambda_0}{M}|\beta_i| + \lambda_2\beta_i^2\Big).

The reverse Huber penalty is $\mathcal B(t) = |t|$ for $|t| \le 1$ and $\mathcal B(t) = (t^2+1)/2$ for $|t| \ge 1$ , and $\psi_1(b;\lambda_0,\lambda_2) = 2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0})$ . The interval relaxation of $\mathrm{PR}(\infty)$ has the value (6),

V_{PR(\infty)} = \min_{\beta\in\mathbb R^p} G(\beta),\qquad G(\beta) = \tfrac12\|y - X\beta\|_2^2 + \sum_{i\in[p]}\psi_1(\beta_i;\lambda_0,\lambda_2).

Let $\mathcal S(\lambda_2)$ be the set of minimizers of $G$ , and, as in (9),

\mathcal L(M) = \{\lambda_2 > 0 \;:\; \exists\beta\in\mathcal S(\lambda_2) \text{ with } \|\beta\|_\infty \le M\}.

The comparison runs through the scalar function $t(b) = 2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0}) - \frac{\lambda_0}{M}|b| - \lambda_2 b^2 = \psi_1(b) - \big(\tfrac{\lambda_0}{M}|b| + \lambda_2 b^2\big)$ and through $v^*(M) = \min_{\|\beta\|_\infty\le M} G(\beta)$ .

Formalization targets

Goal: Proposition 2 (p. 7)

V_{B(M)} \ge V_{PR(\infty)}\quad\text{if } M \le \tfrac12\sqrt{\lambda_0/\lambda_2},\qquad (10)

V_{B(M)} \le V_{PR(\infty)}\quad\text{if } M \ge \sqrt{\lambda_0/\lambda_2} \text{ and } \lambda_2 \in \mathcal L(M).\qquad (11)

Milestones, in the order of the paper's proof

(37): $V_{B(M)} = \min_{\|\beta\|_\infty\le M} H(\beta)$ , attained.
(10) on its own.
Lemma 1: for $M \ge \sqrt{\lambda_0/\lambda_2}$ and $b \in [-M, M]$ , $t(b) \ge 0$ .
(41): for $M \ge \sqrt{\lambda_0/\lambda_2}$ , $v^*(M) \ge V_{B(M)}$ .

The mission also contains the scalar inequality (39) as a supporting statement (not a milestone): for $M \le \frac12\sqrt{\lambda_0/\lambda_2}$ and $|b| \le M$ , $t(b) = (2\sqrt{\lambda_0\lambda_2} - \lambda_0/M)|b| - \lambda_2 b^2 \le 0$ .

Significance

Proposition 2 says that neither relaxation dominates the other. For a tight Big-M bound the Big-M relaxation yields the larger lower bound; for a loose one, provided some optimal solution of $\mathrm{PR}(\infty)$ lies in the box, the perspective relaxation does. Equivalently, with the other data fixed, a small $\lambda_2$ favours the Big-M relaxation and a large $\lambda_2$ favours $\mathrm{PR}(\infty)$ (p. 8). Together with Proposition 1 of the same paper, which shows that the box-constrained perspective relaxation $\mathrm{PR}(M)$ beats both when $\sqrt{\lambda_0/\lambda_2} > M$ , this motivates the paper's choice of $\mathrm{PR}(M)$ as the formulation on which its BnB solver is built.

The proposition is proved in the paper (Appendix A, pp. 29–30). No machine-checked proof of it, of the reformulation (37), or of any property of the reverse Huber penalty exists on the platform. The mission produces a formal statement of both inequalities with every hypothesis explicit, and the definitions of the two relaxation values in a form that later missions on perspective relaxations can reuse.

Difficulty

The scalar inequalities (39) and Lemma 1 are elementary but split into cases at the kink of the reverse Huber penalty, $|b| = \sqrt{\lambda_0/\lambda_2}$ , and at the sign of $2\sqrt{\lambda_0\lambda_2} - \lambda_0/M$ . The passage from coordinatewise inequalities to optimal values is where care is needed. $V_{B(M)}$ is defined over pairs $(\beta, z)$ , and its identification with a minimum of $H$ over a compact box requires eliminating $z$ and showing attainment. For (11) a pointwise comparison of $G$ and $H$ on the box only bounds $V_{B(M)}$ by the box-restricted value $v^*(M)$ , not by $V_{PR(\infty)}$ , which is an infimum over all of $\mathbb R^p$ ; the hypothesis $\lambda_2 \in \mathcal L(M)$ is what closes this gap, and dropping it gives a statement the paper does not prove.

Formalization scope

Optimal values are real infima (sInf): $V_{B(M)}$ over the feasible pairs $(\beta, z)$ of the interval relaxation, $V_{PR(\infty)}$ over all of $\mathbb R^p$ , $v^*(M)$ over the box. For $\lambda_0, \lambda_2 > 0$ each set of values is nonempty ( $\beta = z = 0$ ) and bounded below by $0$ , so no infimum takes Lean's junk value. $V_{PR(\infty)}$ is defined as the displayed minimum (6); its identification with the interval relaxation of $\mathrm{PR}(\infty)$ is a result of Dong, Chen and Linderoth that the paper cites and does not prove, and it is not part of this mission. $\mathcal S(\lambda_2)$ is the set of minimizers of $G$ , as the paper uses it in the proof of (11).

All theorems assume $\lambda_0, \lambda_2, M > 0$ . The paper remarks that Proposition 2 applies for any $M \ge 0$ ; $M = 0$ is excluded because $H$ and $t$ divide by $M$ . The goal is stated for optimal values, not for the objective functions at a single point: a pointwise comparison of $H$ and $G$ is a milestone, not the proposition. Milestone (37) is stated with IsLeast, so it asserts attainment as well as the value.

The paper states no $O(\cdot)$ bounds in this result, so no constants are instantiated. Contributions welcome: proofs of the scalar lemmas, of (37) (which needs compactness of the box and continuity of $H$ ), and of the goal.

Selected references

H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, 2021; Mathematical Programming, 2022. https://arxiv.org/abs/2004.06152
H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv preprint, 2015. https://arxiv.org/abs/1510.06083
D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, The Annals of Statistics 44(2), 813–852, 2016. https://doi.org/10.1214/15-AOS1388
A. Frangioni, C. Gentile, Perspective cuts for a class of convex 0–1 mixed integer programs, Mathematical Programming 106(2), 225–236, 2006. https://doi.org/10.1007/s10107-005-0594-3
O. Günlük, J. Linderoth, Perspective reformulations of mixed integer nonlinear programs with indicator variables, Mathematical Programming 124(1–2), 183–205, 2010. https://doi.org/10.1007/s10107-010-0360-z
A. B. Owen, A robust hybrid of lasso and ridge regression, Contemporary Mathematics 443, 59–72, 2007 (the reverse Huber penalty).

11 thms2 active usersReviewed

Information Theory Machine Learning Probability·Captain: mikedeng1

Information-Theoretic Analysis of Generalization Capability of Learning Algorithms III: The Gibbs Algorithm Has Excess Risk at Most (1/β)log(1/Q(wₒ)) + β/(2n) (Corollary 2)Research Paper

Motivation

Statistical learning algorithms fit hypotheses to data that are available during training, while their performance is judged on new data. A rule that minimizes training loss can fit peculiarities of the sample, so its training loss and population loss need not agree. Xu and Raginsky study this difference through information quantities associated with the sample and the algorithm's output. Their Gibbs example shows how a probability distribution chosen before seeing the data can guide a randomized learner and yield a population-risk guarantee with explicit dependence on the sample size and the prior's mass at a good hypothesis. This mission formalizes their countable-hypothesis result, Corollary 2, and the steps of Section 4.3 and Appendix D that support it. Xu and Raginsky, 2017

Setting

Let $\mathcal Z$ be an instance space and $\mathcal W$ a hypothesis space, each with a measurable structure. A probability measure $\mu$ on $\mathcal Z$ generates a sample $S=(Z_1,\ldots,Z_n)$ of $n$ independent observations. A loss $\ell(w,z)$ measures the cost of hypothesis $w$ on instance $z$ . Its population risk is $L_\mu(w)=\mathbb E_{Z\sim\mu}\ell(w,Z)$ ; its empirical risk on a realized sample $s$ is $L_s(w)=n^{-1}\sum_{i=1}^n\ell(w,z_i)$ . These definitions match equations (1)–(3) of the paper. Xu and Raginsky, 2017, p. 2

A randomized learning rule is a Markov kernel $P_{W|S}$ : for each observed sample $s$ , it gives a probability distribution for an output hypothesis $W$ . Together with the sample law $\mu^{\otimes n}$ , it determines the joint law of $(S,W)$ . The expected generalization error is $\operatorname{gen}(\mu,P_{W|S})=\mathbb E[L_\mu(W)-L_S(W)]$ , as in equation (4). A probability distribution $Q$ on $\mathcal W$ serves as a prior. The Gibbs rule at inverse temperature $\beta>0$ weights a hypothesis by its prior mass times $e^{-\beta L_s(w)}$ , then normalizes across the hypothesis space. Thus it favors low empirical risk without discarding the prior. Xu and Raginsky, 2017, pp. 2, 6

The associated optimization problem balances expected empirical risk against the conditional Kullback–Leibler divergence from the learning kernel to $Q$ : $D(P_{W|S}\Vert Q\mid P_S)=\int D(P_{W|S=s}\Vert Q)\,\mu^{\otimes n}(ds)$ . This penalty measures how much the output distribution changes from the prior after observing the sample. The paper's Theorem 5 identifies the Gibbs kernel as an optimizer of this relaxed problem. Xu and Raginsky, 2017, p. 6

Formalization targets

Gibbs optimization

For nonnegative loss, Theorem 5 asserts that the Gibbs kernel is a Markov learning rule, has the normalized exponential distribution at each sample, and minimizes the relaxed objective over learning kernels:

P^*_{W|S=s}(dw)=\frac{e^{-\beta L_s(w)}Q(dw)}{\mathbb E_Q[e^{-\beta L_s(W)}]}.

The milestone list also records the Appendix D empirical-risk comparison with a fixed hypothesis, its identity $D(\delta_w\Vert Q)=-\log Q(\{w\})$ when the prior has positive mass at $w$ , and the Gibbs generalization bound quoted in equation (28). Xu and Raginsky, 2017, pp. 6–7, 13

Expected population risk

The goal is Corollary 2. If $\mathcal W$ is countable, $0\le\ell\le1$ , $w_o$ achieves the minimum population risk, and $Q(\{w_o\})>0$ , then

\mathbb E[L_\mu(W)]\le\inf_{w\in\mathcal W}L_\mu(w) +\frac1\beta\log\frac1{Q(\{w_o\})}+\frac\beta{2n}.

The first excess term reflects the prior mass on a population-risk minimizer; the second is controlled by sample size and inverse temperature. The target keeps the infimum over the whole hypothesis space and the constants of equation (29). Xu and Raginsky, 2017, p. 7

Significance

Corollary 2 gives a quantitative way to choose a prior and temperature: a prior that puts more mass on a good hypothesis reduces the logarithmic term, while changing $\beta$ changes both terms in opposite directions. It also connects the optimization characterization of a randomized algorithm to the population risk that matters for learning. Without the empirical-risk comparison and the separate generalization estimate, optimizing the training objective alone would not give this population statement. Xu and Raginsky, 2017, pp. 6–7, 13

The cited paper proves Corollary 2 and Theorem 5; the present task is to supply machine-checked proofs of their faithful Lean statements. The Donsker–Varadhan inequality and a tilted-measure identity are already published and proved on the platform, and the basic sample-law and risk definitions are already published. The Gibbs optimization, the Appendix D comparisons, and the quoted bound (28) are posed here as new targets. This work would leave reusable definitions for randomized learning kernels, their Gibbs specialization, and objectives with potentially infinite divergence.

Difficulty

The Gibbs rule is defined separately at every sample, but a learning algorithm must be a measurable kernel on the entire sample space. Establishing the normalized density pointwise does not by itself establish this kernel property. The relaxed objective also combines an integral of empirical risk with a conditional divergence, either of which can be infinite before bounded-loss assumptions are imposed. Equation (28), which the paper attributes to earlier work, needs a sharp $\beta/(2n)$ constant; the looser information bound discussed immediately before it has a different dependence on $\beta$ . These are separate mathematical obligations even though the final displayed inequality is short. Xu and Raginsky, 2017, pp. 6–7, 13

Formalization scope

The Lean development represents a sample as Fin n → Z, its law as Measure.pi, and a randomized learner as Kernel (Fin n → Z) W. Population and empirical risks come from the published LearnStability.Characterization.Setting definition. The Gibbs kernel is built by a normalized density over the probability prior $Q$ ; Theorem 5 explicitly asserts it is a Markov kernel. The relaxed objective takes values in $\mathbb R_{\ge0}\cup\{\infty\}$ , so an infinite KL cost is not lost through real conversion. Generalization error remains the real expectation of the population-risk minus empirical-risk difference. The stated loss bounds ensure those real expectations are meaningful in the bounded-loss results.

The paper assumes a nonnegative loss in its general setting and requires $\ell\in[0,1]$ for the later bounds. The Lean statements add joint measurability of $\ell$ and $n>0$ explicitly. Corollary 2 also makes the named minimizer's defining property and positive prior mass explicit: countability alone does not ensure an attained infimum, and a zero prior mass makes the printed logarithmic bound infinite. Theorem 5 retains its general measurable hypothesis space and nonnegative loss; countability appears only where the paper invokes it. Theorem 5 states optimality over all Markov kernels, the displayed Gibbs formula, and, for each sample, uniqueness of the Gibbs distribution as the minimizer of the samplewise problem (C.12) of Appendix C. The goal concerns the Gibbs kernel's actual population risk, rather than only the existence of a minimizer of the relaxed objective.

Useful contributions include probability-kernel measurability, control of conditional divergence and its finite conversions, the fixed-hypothesis comparison, and the sharp bounded-loss generalization estimate. The point-mass KL identity and the extended objective can be reused in other Gibbs and PAC-Bayesian formalizations. Xu and Raginsky, 2017, pp. 2, 6–7, 13

Selected references

A. Xu and M. Raginsky, Information-Theoretic Analysis of Generalization Capability of Learning Algorithms, Advances in Neural Information Processing Systems 30, 2017. arXiv:1705.07809v2

10 thms2 active usersReviewed

Information Theory Machine Learning Probability·Captain: mikedeng1

Information-Theoretic Analysis of Generalization Capability of Learning Algorithms I: The Expected Generalization Error Is at Most √(2σ²I(S;W)/n) (Theorem 1)Research Paper

Motivation

A learning algorithm trained on a finite sample generalizes when its empirical risk on that sample is close to its risk on fresh data. Classical guarantees come from uniform convergence over the hypothesis class (VC dimension, Rademacher complexity) or from algorithmic stability, such as uniform stability (Bousquet and Elisseeff, 2002) and on-average stability (Shalev-Shwartz et al., 2010). Both families look at the class or at the algorithm's worst-case sensitivity, not at how much the trained hypothesis actually depends on the data it was trained on.

Russo and Zou (arXiv:1511.05219, 2016) bounded the bias of adaptive data analysis by mutual information, and Xu and Raginsky (arXiv:1705.07809, NIPS 2017) turned this into a generalization bound for learning algorithms: the expected generalization error is at most $\sqrt{2\sigma^2 I(S;W)/n}$ , where $I(S;W)$ is the mutual information between the training sample and the output hypothesis. This bound started the line of information-theoretic generalization bounds, later refined to individual-sample mutual information (Bu, Zou and Veeravalli, 2020), conditional mutual information (Steinke and Zakynthinou, 2020) and chaining variants (Asadi, Abbe and Verdú, 2018).

Timeline:

2016, Russo and Zou: bias of adaptive analysis bounded by $I(\Lambda_{\mathsf W}(S);W)$ , the information carried by the vector of empirical risks, for a finite hypothesis space.
2017, Xu and Raginsky: the bound with the input–output mutual information $I(S;W)$ , for arbitrary hypothesis spaces (Theorem 1); high-probability versions and an analysis of the Gibbs algorithm.
2018–2020: chaining, individual-sample and conditional mutual information refinements.

Setting

There is an instance space $\mathsf Z$ , a hypothesis space $\mathsf W$ and a nonnegative loss $\ell:\mathsf W\times\mathsf Z\to\mathbb R_+$ , written ℓ : W → Z → ℝ in Lean. Data are drawn from an unknown probability measure $\mu$ on $\mathsf Z$ ; a dataset of size $n$ is an i.i.d. sample $S=(Z_1,\dots,Z_n)\sim\mu^{\otimes n}$ (sampleLaw μ n).

A learning algorithm is a Markov kernel $P_{W|S}$ (κ : Kernel (Fin n → Z) W): given the dataset, it outputs a random hypothesis $W$ . The pair $(S,W)$ has joint law $P_{S,W}=\mu^{\otimes n}\otimes P_{W|S}$ (sampleLaw μ n ⊗ₘ κ), with marginals $P_S=\mu^{\otimes n}$ and $P_W$ .

The population risk and the empirical risk of a hypothesis $w$ are

L_\mu(w)=\int_{\mathsf Z}\ell(w,z)\,\mu(dz),\qquad L_S(w)=\frac1n\sum_{i=1}^n \ell(w,Z_i)

(risk ℓ μ w, empRisk ℓ s w). The expected generalization error is

\mathrm{gen}(\mu,P_{W|S})=\mathbb E\big[L_\mu(W)-L_S(W)\big],

the expectation taken under $P_{S,W}$ (genError ℓ μ κ).

The mutual information of a pair $(X,Y)$ with joint law $P_{X,Y}$ is the relative entropy $I(X;Y)=D(P_{X,Y}\,\|\,P_X\otimes P_Y)\in[0,\infty]$ (mutualInfo). A real random variable $U$ is $\sigma$ -subgaussian if $\log\mathbb E[e^{\lambda(U-\mathbb EU)}]\le\lambda^2\sigma^2/2$ for all $\lambda\in\mathbb R$ .

Formalization targets

Goal: Theorem 1 (p. 4)

If $\ell(w,Z)$ is $\sigma$ -subgaussian under $\mu$ for every $w\in\mathsf W$ , then

\big|\mathrm{gen}(\mu,P_{W|S})\big|\le\sqrt{\frac{2\sigma^2}{n}\,I(S;W)} .

The statement fixes no structure on $\mathsf W$ (it may be uncountable) and no bound on the loss beyond subgaussianity.

Milestones

(A.1), Donsker–Varadhan (p. 11), the inequality $\int F\,d\pi-D(\pi\|\rho)\le\log\int e^F\,d\rho$ . Already proved on the platform and referenced.
Lemma 1 (p. 3), the decoupling estimate: if $f(\bar X,\bar Y)$ is $\sigma$ -subgaussian under $P_X\otimes P_Y$ , then

\big|\mathbb E f(X,Y)-\mathbb E f(\bar X,\bar Y)\big|\le\sqrt{2\sigma^2 I(X;Y)} .

Subgaussianity of the empirical risk (§3.2, p. 4): for every $w$ , $L_S(w)-L_\mu(w)$ is $\sigma/\sqrt n$ -subgaussian under $\mu^{\otimes n}$ .
The mixture step (§3.2, p. 4, corrected): under $P_S\otimes P_W$ , $f(\bar S,\bar W)=L_{\bar S}(\bar W)-L_\mu(\bar W)$ is $\sigma/\sqrt n$ -subgaussian with mean $0$ .

Significance

The result. Theorem 1 makes generalization a property of the dependence between data and output rather than of the size of the hypothesis class. It applies to randomized algorithms on uncountable or infinite-dimensional hypothesis spaces, where uniform convergence gives nothing, and to unbounded subgaussian losses. Any mechanism that limits $I(S;W)$ , such as noise injection, differential privacy, compression or relative-entropy regularization, inherits a generalization guarantee. A loss with values in $[a,b]$ is $(b-a)/2$ -subgaussian for every $\mu$ , so the theorem covers all bounded losses. The bound is also the template for the later refinements listed above, which share Lemma 1's decoupling argument.

Formalizing it. The result is proved on paper; no machine-checked proof is known. A formalization supplies a reusable statement of mutual information as a relative entropy of a joint law on general measurable spaces, a decoupling lemma for subgaussian functions, and the mixture argument for subgaussian families, all of which recur in the later literature. It also settles a point the paper leaves loose: the printed proof applies Lemma 1 to the uncentred empirical risk, which is not subgaussian in general; the milestones state the corrected step.

Difficulty

The two halves of the proof are short on paper, but each step that "follows" uses a fact the page does not state. The decoupling estimate needs $\mathbb E f(X,Y)$ to be finite, which holds only because finite relative entropy and exponential integrability under the product together force integrability under the joint law. The mixture step needs the moment-generating-function bound of each section $w\mapsto f(\cdot,w)$ to integrate over $P_W$ , which requires joint measurability and the centring of every section at its own mean: the uncentred empirical risk $L_{\bar S}(\bar W)$ mixes laws with different means and is not subgaussian.

A natural first attempt applies Lemma 1 directly to $f(s,w)=L_s(w)$ as printed; it fails on the example $\ell(w,z)=w$ with $W$ uniform on $\{0,1\}$ and independent of $S$ .

Formalization scope

Objects. The sample law, $L_\mu$ and $L_S$ are reused from the published LearnStability.Characterization.Setting. This mission defines mutualInfo P := klDiv P (P.fst.prod P.snd) (values in $[0,\infty]$ ) and genError, the integral of the pointwise difference $L_\mu(w)-L_s(w)$ under sampleLaw μ n ⊗ₘ κ. Samples are Fin n → Z; the algorithm is a Markov kernel.
Subgaussianity is Mathlib's HasSubgaussianMGF of the centred variable, whose parameter is the variance proxy: $\sigma^2$ for the loss, $\sigma^2/n$ for the empirical risk.
Added hypotheses, all implicit on the page: $n\ge1$ (the bound divides by $n$ ); joint measurability of $\ell$ (so that $L_\mu(W)$ and $L_S(W)$ are random variables); and $I\ne\infty$ in Lemma 1 and Theorem 1, because Lean's conversion of $\infty$ to a real number gives $0$ , which would turn the page's vacuous bound into a false claim. The page's nonnegativity of $\ell$ is kept. No integrability hypothesis on $f$ or on the losses is assumed beyond subgaussianity.
Correction of the print. The page says that $f(\bar S,\bar W)=L_{\bar S}(\bar W)$ is $\sigma/\sqrt n$ -subgaussian; milestone 4 states it for the centred $L_{\bar S}(\bar W)-L_\mu(\bar W)$ , together with its mean being $0$ . Equation (9) is not posed separately.
Ruled out. The goal is stated for genError and the mutual information of the algorithm's own joint law; a version through Lemma 1's abstract pair $(\bar X,\bar Y)$ , through $I(\Lambda_{\mathsf W}(S);W)$ (Theorem 2, out of scope), or with $I$ truncated to a real number would not be this theorem.
Infrastructure. Integrability transfer from $P_X\otimes P_Y$ to $P_{X,Y}$ under finite relative entropy; sums of independent subgaussian variables on Measure.pi (Mathlib has HasSubgaussianMGF.sum_of_iIndepFun); mixtures of mean-zero subgaussian families under a product measure. These are reusable beyond this mission, and contributions of each are welcome.

Selected references

A. Xu, M. Raginsky, Information-theoretic analysis of generalization capability of learning algorithms, NIPS 2017; arXiv:1705.07809v2. https://arxiv.org/abs/1705.07809
D. Russo, J. Zou, Controlling bias in adaptive data analysis using information theory, AISTATS 2016. https://arxiv.org/abs/1511.05219
S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, stability and uniform convergence, JMLR 11, 2010. https://jmlr.org/papers/v11/shalev-shwartz10a.html
O. Bousquet, A. Elisseeff, Stability and generalization, JMLR 2, 2002. https://www.jmlr.org/papers/v2/bousquet02a.html
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013 (Donsker–Varadhan, Cor. 4.15). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
A. Asadi, E. Abbe, S. Verdú, Chaining mutual information and tightening generalization bounds, NeurIPS 2018. https://arxiv.org/abs/1806.03803
Y. Bu, S. Zou, V. Veeravalli, Tightening mutual information based bounds on generalization error, IEEE JSAIT 2020. https://arxiv.org/abs/1901.04609
T. Steinke, L. Zakynthinou, Reasoning about generalization via conditional mutual information, COLT 2020. https://arxiv.org/abs/2001.09122

7 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization 2: When √(λ0/λ2) > M the Perspective Relaxation Is at Least as Strong as the Big-M and PR(∞) RelaxationsResearch Paper

Motivation

Best subset selection with ridge shrinkage asks for a coefficient vector $\beta\in\mathbb R^p$ that fits a response $y\in\mathbb R^n$ through a design matrix $X\in\mathbb R^{n\times p}$ while using few nonzero coefficients:

\min_{\beta\in\mathbb R^p}\ \tfrac12\|y-X\beta\|_2^2 + \lambda_0\|\beta\|_0 + \lambda_2\|\beta\|_2^2 .

This $\ell_0\ell_2$ -regularized least squares problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (BnB). The speed of BnB is governed by the strength of the continuous relaxation solved at every node: a larger relaxation value prunes more nodes. Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) build the solver L0BnB on a perspective formulation and compare its relaxation with two standard alternatives. Their Proposition 1 quantifies that comparison, and their experiments (Section 4.2.1 of the paper) report speed-ups of more than 90× from using the perspective formulation with a tight bound $M$ instead of the bound-free formulation.

The mission formalizes Proposition 1 together with the three steps of its proof in the paper's Appendix A.

Setting

Fix $X$ , $y$ , regularization parameters $\lambda_0,\lambda_2>0$ and a bound $M>0$ on $\|\beta\|_\infty$ ; write $[p]=\{1,\dots,p\}$ .

The Big-M formulation $B(M)$ introduces indicators $z_i$ and minimizes $\tfrac12\|y-X\beta\|_2^2+\lambda_0\sum_i z_i+\lambda_2\|\beta\|_2^2$ subject to $-Mz_i\le\beta_i\le Mz_i$ , $z_i\in\{0,1\}$ . Its interval relaxation lets $z_i\in[0,1]$ ; its optimal value is $V_{B(M)}$ .

The reverse Huber penalty is $\mathcal B(t)=|t|$ for $|t|\le1$ and $(t^2+1)/2$ for $|t|\ge1$ . Put

\psi_1(b;\lambda_0,\lambda_2)=2\lambda_0\,\mathcal B\big(b\sqrt{\lambda_2/\lambda_0}\big),\qquad \psi_2(b;\lambda_0,\lambda_2,M)=\Big(\frac{\lambda_0}{M}+\lambda_2M\Big)|b|,

and let $\psi=\psi_1$ if $\sqrt{\lambda_0/\lambda_2}\le M$ and $\psi=\psi_2$ if $\sqrt{\lambda_0/\lambda_2}>M$ . The paper's Theorem 1 shows that the interval relaxation of the perspective formulation $\mathrm{PR}(M)$ is equivalent to

\min_{\|\beta\|_\infty\le M} F(\beta),\qquad F(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi(\beta_i;\lambda_0,\lambda_2,M), \tag{5}

and $V_{PR(M)}$ denotes the optimal value of (5). Without a bound, the relaxation value of $\mathrm{PR}(\infty)$ is

V_{PR(\infty)}=\min_{\beta\in\mathbb R^p}G(\beta),\qquad G(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi_1(\beta_i;\lambda_0,\lambda_2). \tag{6}

Finally $h(\lambda_0,\lambda_2,M)=\lambda_0/M+\lambda_2M-2\sqrt{\lambda_0\lambda_2}$ , and $\beta^*$ denotes an optimal solution of (5).

Formalization targets

Goal: Proposition 1

For $\sqrt{\lambda_0/\lambda_2}>M$ ,

V_{PR(M)}\ \ge\ V_{B(M)}+\lambda_2\big(M\|\beta^*\|_1-\|\beta^*\|_2^2\big), \tag{7}

V_{PR(M)}\ \ge\ V_{PR(\infty)}+h(\lambda_0,\lambda_2,M)\,\|\beta^*\|_1. \tag{8}

Milestones

(37): $V_{B(M)}=\min_{\|\beta\|_\infty\le M}H(\beta)$ with $H(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_i\big(\tfrac{\lambda_0}{M}|\beta_i|+\lambda_2\beta_i^2\big)$ ; the Big-M relaxation expressed in $\beta$ alone. It holds for every $M>0$ .
(7) alone.
The linear case of $\psi_1$ : if $|b|\le M<\sqrt{\lambda_0/\lambda_2}$ then $\psi_1(b;\lambda_0,\lambda_2)=2|b|\sqrt{\lambda_0\lambda_2}$ .
(8) alone (the paper's (38)).

The goal is the conjunction of milestones 2 and 4.

Significance

In the regime $\sqrt{\lambda_0/\lambda_2}>M$ both added terms are nonnegative: $M\|\beta^*\|_1\ge\|\beta^*\|_2^2$ because $\|\beta^*\|_\infty\le M$ , and $h>0$ because $\lambda_0/M+\lambda_2M>2\sqrt{\lambda_0\lambda_2}$ whenever $M\ne\sqrt{\lambda_0/\lambda_2}$ . So the perspective relaxation is at least as strong as both the Big-M relaxation and $\mathrm{PR}(\infty)$ , strictly so as soon as one coordinate of $\beta^*$ lies strictly inside $(0,M)$ in absolute value (for (7)) or $\beta^*\ne0$ (for (8)). The bounds are explicit in the relaxation's own solution, so they can be evaluated at a BnB node. This is the theoretical justification for the paper's design choice of building its solver on $\mathrm{PR}(M)$ with a valid, tight $M$ ; the regime $\sqrt{\lambda_0/\lambda_2}\le M$ , where (5) is (6) with the additional box constraint $\|\beta\|_\infty\le M$ , is complementary.

Proposition 1 is proved in the paper; it has no machine-checked proof. The mission produces one, together with reusable Lean definitions of the three relaxation values and of the reverse Huber penalty that other statements about perspective relaxations of sparse regression can be stated against.

Difficulty

The arithmetic of the coordinate-wise penalties is short. The substance is in comparing optimal values that are defined as infima over different feasible sets. The obvious argument " $V_{PR(M)}-V_{B(M)}\ge F(\beta^*)-H(\beta^*)$ " requires that the Big-M relaxation, which is posed over pairs $(\beta,z)$ , have value at most $H(\beta^*)$ ; that is the content of (37), a statement about a different feasible set in more variables. Likewise (8) needs $V_{PR(\infty)}\le G(\beta^*)$ , i.e. that the infimum in (6) is a genuine lower bound of a set bounded below, and both inequalities use the regime $\sqrt{\lambda_0/\lambda_2}>M$ , in which $\psi=\psi_2$ . Dropping the regime hypothesis makes (8) false in general: for $\sqrt{\lambda_0/\lambda_2}\le M$ one has $\psi=\psi_1$ and $h\ge0$ , and the right side can exceed $V_{PR(M)}=V_{PR(\infty)}$ .

Formalization scope

All objects live in the namespace L0BnB.Strength. Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M as hypotheses; $[p]$ is Fin p. Norms are explicit sums: $\|v\|_2^2$ is ∑ i, v i ^ 2, $\|\beta\|_1$ is ∑ i, |β i|, and $\|\beta\|_\infty\le M$ is ∀ i, |β i| ≤ M. The regime is written M < Real.sqrt (lam0 / lam2).

Optimal values are sInf of the image of the feasible set in ℝ. Each set is nonempty ( $\beta=0$ , $z=0$ ) and bounded below by $0$ under the positivity hypotheses, so sInf is the true infimum and never a junk value. $V_{B(M)}$ is defined over pairs $(\beta,z)$ with $z_i\in[0,1]$ , not through $H$ ; (37) is a theorem. $V_{PR(\infty)}$ is (6) as printed: the paper attributes to its reference [21] the identification of (6) with the interval relaxation of $\mathrm{PR}(\infty)$ in $(\beta,z,s)$ variables, and that identification is not part of the mission. $V_{PR(M)}$ is the value of (5), which is the paper's definition; Theorem 1 (the equivalence of (5) with the $(\beta,z,s)$ relaxation) belongs to a sibling mission.

The optimal solution $\beta^*$ is a binder with the hypotheses $\|\beta^*\|_\infty\le M$ and $F(\beta^*)\le F(\beta)$ for every $\beta$ in the box. A formalization in which $\beta^*$ is an arbitrary feasible point, or in which $V_{B(M)}$ or $V_{PR(\infty)}$ is defined through a chosen minimizer, would change the statement and is ruled out. The paper uses no $O(\cdot)$ in this result, so no constant is instantiated.

Needed infrastructure is light: continuity of $H$ and compactness of the box for the attainment in (37), and csInf lemmas on ℝ. Contributions of proofs of any milestone, and of the attainment of the infimum in (5), are welcome.

Selected references

H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, 2021; Mathematical Programming (2022). https://arxiv.org/abs/2004.06152
H. Hazimeh, R. Mazumder, Fast Best Subset Selection: Coordinate Descent and Local Combinatorial Optimization Algorithms, Operations Research 68(5), 1517–1537, 2020. https://doi.org/10.1287/opre.2019.1919
H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv e-prints, 2015 (the paper's reference [21], source of (6) for $\mathrm{PR}(\infty)$ ). https://arxiv.org/abs/1510.06083

7 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization 1: The Perspective Interval Relaxation Is a Least Squares Problem with a Separable Reverse-Huber or ℓ1 PenaltyResearch Paper

Motivation

Best subset selection with ridge shrinkage asks for a sparse linear model: given a design matrix $X\in\mathbb R^{n\times p}$ and responses $y\in\mathbb R^n$ , minimize

\tfrac12\|y-X\beta\|_2^2+\lambda_0\|\beta\|_0+\lambda_2\|\beta\|_2^2 ,

where $\|\beta\|_0$ counts nonzero coefficients. The problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (Bertsimas, King, Mazumder 2016). The speed of branch-and-bound is governed by two things: how tight the continuous relaxation at each node is, and how cheaply that relaxation can be solved.

Hazimeh, Mazumder and Saab (arXiv:2004.06152v2; Mathematical Programming 2022) build a branch-and-bound solver whose node relaxations are solved by first-order methods rather than by a conic interior-point solver. Their starting point is the perspective formulation, a standard device for strengthening relaxations of mixed integer programs with indicator variables (Frangioni, Gentile 2006; Günlük, Linderoth 2010). Theorem 1 of the paper shows that the interval relaxation of this formulation is a box-constrained least squares problem with a separable penalty in $\beta$ alone. This mission formalizes Theorem 1.

Timeline. Owen (2007) introduced the reverse Huber penalty as a hybrid of lasso and ridge. Dong, Chen, Linderoth (2015) showed that the interval relaxation of the perspective formulation without a Big-M bound reduces to least squares with a reverse Huber penalty. Hazimeh, Mazumder and Saab (2020–2021) added the Big-M constraint and obtained Theorem 1, with a second regime in which the penalty becomes $\ell_1$ .

Setting

Fix $X\in\mathbb R^{n\times p}$ , $y\in\mathbb R^n$ , $\lambda_0>0$ , $\lambda_2>0$ and $M>0$ , and write $[p]=\{1,\dots,p\}$ . The perspective formulation $\mathrm{PR}(M)$ is problem (3) of the paper:

\min_{\beta,z,s}\ \tfrac12\|y-X\beta\|_2^2+\lambda_0\sum_{i\in[p]}z_i+\lambda_2\sum_{i\in[p]}s_i \quad\text{s.t.}\quad \beta_i^2\le s_iz_i,\ \ -Mz_i\le\beta_i\le Mz_i,\ \ z_i\in\{0,1\},\ \ s_i\ge0 .

Here $z_i$ indicates whether $\beta_i$ may be nonzero, $s_i$ stands in for $\beta_i^2$ through the rotated second-order cone constraint $\beta_i^2\le s_iz_i$ , and $M$ bounds $|\beta_i|$ . The interval relaxation replaces $z_i\in\{0,1\}$ with $z_i\in[0,1]$ .

The reverse Huber penalty (4) is $\mathcal B(t)=|t|$ for $|t|\le1$ and $\mathcal B(t)=(t^2+1)/2$ for $|t|\ge1$ . Put

\psi_1(b;\lambda_0,\lambda_2)=2\lambda_0\,\mathcal B\big(b\sqrt{\lambda_2/\lambda_0}\big),\qquad \psi_2(b;\lambda_0,\lambda_2,M)=\Big(\frac{\lambda_0}{M}+\lambda_2M\Big)|b|,

and let $\psi=\psi_1$ if $\sqrt{\lambda_0/\lambda_2}\le M$ and $\psi=\psi_2$ if $\sqrt{\lambda_0/\lambda_2}>M$ . The reduced relaxation (5) is

\min_{\beta\in\mathbb R^p}\ F(\beta):=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi(\beta_i;\lambda_0,\lambda_2,M)\quad\text{s.t.}\quad\|\beta\|_\infty\le M ,

with optimal value $V_{\mathrm{PR}(M)}$ . For one coordinate $b$ , $\omega(b;\lambda_0,\lambda_2,M)$ is the minimum of $\lambda_0z+\lambda_2s$ over $b^2\le sz$ , $-Mz\le b\le Mz$ , $z\in[0,1]$ , $s\ge0$ .

Formalization targets

Goal: Theorem 1 (Reduced Relaxation), p. 6

The interval relaxation of (3) is equivalent to (5):

\exists\,(z,s):\ (\beta,z,s)\ \text{feasible}\iff\|\beta\|_\infty\le M,\qquad \min_{z,s}\Big\{\tfrac12\|y-X\beta\|_2^2+\lambda_0\textstyle\sum_i z_i+\lambda_2\sum_i s_i\Big\}=F(\beta)\ \ (\|\beta\|_\infty\le M),

and both problems attain the common optimal value $V_{\mathrm{PR}(M)}$ .

Milestones (proof of Theorem 1, p. 28)

Reduction to (36). For $|b|\le M$ , the smallest feasible $z$ is $\hat z=\max\{b^2/s,|b|/M\}$ , so

\omega(b;\lambda_0,\lambda_2,M)=\min_{s\ge b^2}\max\Big\{\lambda_0\tfrac{b^2}{s}+\lambda_2s,\ \lambda_0\tfrac{|b|}{M}+\lambda_2s\Big\}.

Case I. If $\sqrt{\lambda_0/\lambda_2}\le M$ and $|b|\le M$ , then $\omega(b;\lambda_0,\lambda_2,M)=2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0})$ .
Case II. If $\sqrt{\lambda_0/\lambda_2}>M$ and $|b|\le M$ , then $\omega(b;\lambda_0,\lambda_2,M)=(\lambda_0/M+\lambda_2M)|b|$ .

Significance

The result. Theorem 1 removes the $2p$ auxiliary variables $z,s$ and all conic constraints from the node relaxation. What remains is a composite problem, a smooth least squares loss plus a separable, convex penalty under a box constraint, to which coordinate descent and proximal methods apply directly. The paper's solver, its active-set strategy, and the dual bounds of its Section 3 are all built on (5). The theorem also exposes a regime change: when $\sqrt{\lambda_0/\lambda_2}>M$ , the ridge term of the perspective formulation disappears from the relaxation and the penalty is pure $\ell_1$ . Propositions 1 and 2 of the paper, which compare the strengths of the perspective, Big-M and $\mathrm{PR}(\infty)$ relaxations, use this reduced form.

Formalizing it. The result is proved in the paper (Appendix A) by a coordinatewise argument. To our knowledge it has no machine-checked proof. Formalizing it gives a verified bridge from the conic mixed integer formulation to the penalized form that later results of the paper use, and a checked case analysis at the regime boundary $\sqrt{\lambda_0/\lambda_2}=M$ , where the two formulas must agree with the stated tie-breaking.

Difficulty

The obvious approach, "minimize over $z$ and $s$ coordinate by coordinate", is correct in outline, but each step hides a boundary case. The rotated cone constraint $\beta_i^2\le s_iz_i$ degenerates at $s_i=0$ or $z_i=0$ , where $\beta_i^2/s_i$ is undefined, and the paper's convention for $\beta_i=s_i=0$ must be handled. The one-variable problem (36) is a minimum of a pointwise maximum of two functions of $s$ , one convex and decreasing then increasing, the other increasing. Its minimizer lies either in the interior of the region where the first term dominates or on the crossover $s=|b|M$ , depending on the regime. The paper's proof describes the cases loosely: it optimizes the Case I term without imposing the side condition that Case I attains the maximum. A complete argument must prove the lower bound over all feasible $s$ , not just evaluate at a candidate. Finally, the minimum over $(z,s)\in\mathbb R^{2p}$ must be shown to split into a sum of coordinate minima, each attained.

Formalization scope

Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, and reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M; the paper's $[p]$ is Fin p. The squared norm $\|y-X\beta\|_2^2$ is the explicit sum $\sum_r(y_r-(X\beta)_r)^2$ , and $\|\beta\|_\infty\le M$ is $|\beta_i|\le M$ for all $i$ . The cone constraint is kept in product form $\beta_i^2\le s_iz_i$ . In $\hat z$ and (36), Lean's $b^2/0=0$ coincides with the paper's convention $\beta_i^2/s_i=0$ for $\beta_i=s_i=0$ . Every "min" is stated with IsLeast (membership plus lower bound), so attainment is part of each statement. $V_{\mathrm{PR}(M)}$ is defined as a real infimum over the box, and Theorem 1 asserts that this infimum is attained by both problems. No normalization of $X$ or $y$ is assumed; the paper's unit-norm assumption starts in Section 3. The paper writes no $O(\cdot)$ in these results, so there are no constants to instantiate.

A goal stating only one inequality (that $F(\beta)$ is achieved by some $(z,s)$ , or that it bounds the relaxation from below), or a goal over $z_i\in\{0,1\}$ , would not be Theorem 1. The IsLeast form rules out both. The goal uses $\psi$ with both regimes.

A complete development needs: a two-variable convexity argument for $\lambda_0b^2/s+\lambda_2s$ on $s>0$ ; a lemma that the infimum of a separable objective over a product of feasible sets is the sum of the coordinate infima; and continuity of $F$ with compactness of the box to obtain an optimal $\beta$ . The coordinate lemmas and the definition of the reverse Huber penalty are reusable in the companion missions on relaxation strength and Lagrangian duality. Contributions to any milestone, or an alternative proof of the goal, are welcome.

Selected references

H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2 (2021); Mathematical Programming (2022). https://arxiv.org/abs/2004.06152v2
A. Frangioni, C. Gentile, Perspective cuts for a class of convex 0–1 mixed integer programs, Mathematical Programming 106(2), 225–236, 2006. https://doi.org/10.1007/s10107-005-0594-3
O. Günlük, J. Linderoth, Perspective reformulations of mixed integer nonlinear programs with indicator variables, Mathematical Programming 124(1–2), 183–205, 2010. https://doi.org/10.1007/s10107-010-0360-z
H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv:1510.06083, 2015. https://arxiv.org/abs/1510.06083
A. B. Owen, A robust hybrid of lasso and ridge regression, Contemporary Mathematics 443, 59–72, 2007. https://doi.org/10.1090/conm/443/08555
D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 813–852, 2016. https://doi.org/10.1214/15-AOS1388

6 thms2 active usersReviewed

Bandit Algorithms Machine Learning Probability·Captain: mikedeng1

Thompson Sampling: An Asymptotically Optimal Finite-Time Analysis: Bernoulli Thompson Sampling Has Regret (1+ε)Σ Δ_a(ln T + ln ln T)/K(μ_a, μ*) + CResearch Paper

Motivation

Thompson Sampling is the oldest bandit algorithm: Thompson proposed it in 1933 for allocating patients between two treatments (Thompson 1933). It keeps a posterior distribution over the unknown mean reward of every action, draws one sample from each posterior, and plays the action whose sample is largest. It is simple, widely used, and in experiments competitive with index policies designed for optimality. For decades it had no matching theoretical guarantee.

The benchmark for a stochastic bandit algorithm is the lower bound of Lai and Robbins (1985): every consistent policy draws a suboptimal arm $a$ at least $(1-o(1))\ln T/K(\mu_a,\mu^*)$ times in $T$ rounds, where $K$ is the Kullback–Leibler divergence. A policy that attains this rate is called asymptotically optimal.

Timeline.

1933: Thompson introduces the algorithm, without analysis.
1985: Lai and Robbins prove the lower bound and construct asymptotically optimal (but complex) policies.
2011–2012: KL-UCB (Garivier and Cappé 2011) and Bayes-UCB (Kaufmann, Cappé and Garivier 2012) attain the bound for Bernoulli rewards with simpler index rules.
2012: Agrawal and Goyal give the first logarithmic regret bound for Thompson Sampling, $O\big((\sum_a 1/\Delta_a^2)^2\ln T\big)$ , which does not have the optimal constant.
2012: Kaufmann, Korda and Munos (arXiv:1205.4217) prove that Thompson Sampling with uniform priors is asymptotically optimal for Bernoulli rewards, with a finite-time bound. This mission formalizes that result.

Setting

There are $K\ge2$ arms. Arm $a$ yields reward $1$ with probability $\mu_a\in(0,1)$ and $0$ otherwise. Arm $1$ is the unique optimal arm: $\mu^*=\mu_1>\mu_a$ for every $a\neq1$ . The gap of arm $a$ is $\Delta_a=\mu^*-\mu_a$ , and $\mu_2$ denotes the largest mean among the suboptimal arms.

Thompson Sampling with uniform priors. Let $N_{a,t}$ be the number of times arm $a$ has been drawn before round $t$ and $S_{a,t}$ the number of rewards equal to $1$ among those draws. With a uniform prior, the posterior of $\mu_a$ is $\mathrm{Beta}(S_{a,t}+1,\,N_{a,t}-S_{a,t}+1)$ . In round $t$ the algorithm draws, independently, a sample $\theta_{a,t}$ from each posterior, plays $A_t=\arg\max_a\theta_{a,t}$ , and observes the reward of $A_t$ .

The regret after $T$ rounds is

\mathcal R(T)=T\mu^*-\mathbb E\Big[\sum_{t=1}^T R_t\Big]=\sum_a\Delta_a\,\mathbb E[N_{a,T}],

where $N_{a,T}$ now counts the draws of $a$ in rounds $1,\dots,T$ . The Bernoulli divergence is $K(p,q)=p\ln\frac pq+(1-p)\ln\frac{1-p}{1-q}$ .

The analysis compares the Thompson samples with two index rules. For an arm with $S$ successes in $N$ draws, at round $t$ of a horizon $T$ , the KL-UCB index is $u=\sup\{x\in[S/N,1):N\,K(S/N,x)\le\ln t+\ln\ln T\}$ , and the Bayes-UCB index $q$ is the quantile of order $1-\frac1{t\ln T}$ of the posterior $\mathrm{Beta}(S+1,N-S+1)$ .

Formalization targets

Goal: Theorem 1 (p. 3)

For every $\epsilon>0$ there is a constant $C$ , depending on $\epsilon$ and the instance, such that for every horizon $T$ ,

\mathcal R(T)\le(1+\epsilon)\sum_{a:\,\mu_a\neq\mu^*}\frac{\Delta_a(\ln T+\ln\ln T)}{K(\mu_a,\mu^*)}+C.

Only the existence of $C$ is asserted; its value is not fixed, so improvements of the lower-order terms do not invalidate the goal.

Milestones

Eq. (1): $\mathcal R(T)=T\mu^*-\mathbb E[\sum_{t=1}^T R_t]=\sum_a\Delta_a\,\mathbb E[N_{a,T}]$ .
Theorem 2 (p. 4): for each suboptimal $a$ and $\epsilon>0$ , $\mathbb E[N_{a,T}]\le(1+\epsilon)\frac{\ln T+\ln\ln T}{K(\mu_a,\mu_1)}+C$ .
Proposition 1 (p. 4): there is $b\in(0,1)$ with $\sum_{t\ge1}\mathbb P(N_{1,t}\le t^b)<\infty$ .
Display (4) (p. 5): $\mathbb E[N_{a,T}]\le A+B+2$ , an under-estimation term $A$ for arm $1$ plus a KL-UCB term $B$ .
Lemma 1 (p. 5): $\sum_t\mathbb P\big(\theta_{1,t}\le\mu_1-\sqrt{6\ln t/N_{1,t}}\big)\le N_0(b)+3+C_b$ .
Lemma 2 (p. 6): $B\le(1+\epsilon)\frac{\ln T+\ln\ln T}{K(\mu_a,\mu_1)}+D$ for large $T$ .
Lemma 3 (p. 9), in its analytic form (§3.4): a bound on the probability that the optimal arm's samples stay below $\mu_2+\delta$ for $f$ rounds.
Lemma 4 (p. 9): saturated suboptimal arms rarely produce samples above $\mu_a+\delta_a$ .
§2 (p. 3): the Beta–Binomial identity (referenced) and the comparison $q<u$ of the two indices.

Significance

The result. Theorem 1 shows that the leading constant of Thompson Sampling's regret equals the Lai–Robbins constant, so no consistent policy does asymptotically better on Bernoulli bandits. It settled a question open since 1933 and is the starting point for later optimality proofs of Thompson Sampling for exponential families and Gaussian rewards. Proposition 1, a summable tail bound on the event that the optimal arm is under-sampled, is the reusable core: it is a deviation inequality for the number of draws of the optimal arm, which a bound on its expectation does not imply.

The formalization. The result is proved on paper; no machine-checked proof of an optimal-constant bound for Bernoulli Thompson Sampling exists. The platform already has the Gaussian frequentist analysis of Lattimore and Szepesvári (Theorem 36.3) and the non-optimal Agrawal–Goyal bound. This mission adds the Bernoulli, Beta-posterior case with the KL constant, the KL-UCB and Bayes-UCB indices with the $\ln t+\ln\ln T$ exploration rate, and the optimal-arm tail bound. Corrected statements are part of the output: the explicit constant $D$ printed at the end of Lemma 2's proof is too small, the constant $C_{\lambda,\mu_1,\mu_2}$ printed for Lemma 3 has the wrong sign, and Lemma 3 as printed quantifies over arbitrary random intervals, which its proof does not support.

Difficulty

The standard proof for an optimistic index policy bounds the draws of a suboptimal arm by an under-estimation term $\sum_t\mathbb P(l_{1,t}<\mu_1)$ and a concentration term. For Thompson Sampling the under-estimation term is not small: once the posterior of arm $1$ is concentrated, $\mathbb P(\theta_{1,t}<\mu_1)$ is close to $1/2$ in every round. Comparing $\theta_{1,t}$ with a lower confidence bound $\mu_1-\sqrt{6\ln t/N_{1,t}}$ instead only helps if $N_{1,t}$ is large with overwhelming probability, and a bound on $\mathbb E[N_{1,t}]$ does not give that.

Proposition 1 supplies it, and it carries most of the difficulty. It must control long stretches of rounds in which arm $1$ is never drawn while several suboptimal arms compete, and it needs the samples of arm $1$ conditioned on its successes at a random time while the arm is not played, an optional-skipping step that the paper leaves implicit and that is the main measure-theoretic obstacle in Lean.

Formalization scope

Representation. The algorithm is the published Thompson Sampling run (AgrawalGoyalTS_TwoArmed_ThompsonSampling) on the published Bernoulli bandit (bernoulliRelativeEntropy). That run is Agrawal–Goyal's Algorithm 2, which passes each reward through a Bernoulli trial of success probability equal to the reward; for $\{0,1\}$ rewards the trial returns the reward almost surely, so the posterior is exactly the paper's. Probabilities are values of tsLaw in $[0,\infty]$ , expectations of counts and the regret are lower integrals in $[0,\infty]$ , and every bound compares with the embedding of a real right-hand side.

Conventions.

Lean arm $0$ is the paper's arm $1$ . Lean round $t$ is the paper's round $t+1$ ; $N_{a,t}$ , $S_{a,t}$ are the counts when $\theta_{a,t}$ is drawn, and the paper's $\ln t$ is $\ln(t+1)$ at Lean round $t$ .
$\sqrt{6\ln t/N_{1,t}}=\infty$ when $N_{1,t}=0$ (p. 4), encoded by cases.
The KL-UCB supremum ranges over $x<1$ , because the real-valued divergence at $q=1$ is a finite junk value; $u=1$ when $N=0$ or $S=N$ , cases the page leaves undefined.
Every constant with a printed dependence list ( $C$ , $D$ , $N$ , $b$ , $C_b$ ) is chosen after the instance (and $\epsilon$ , the arm) and before $T$ .

Added hypotheses and corrections.

$0<\mu_a<1$ for every arm, and $K\ge2$ : not stated in the paper but used by its proof (it divides by $\mu_1(1-\mu_1)$ , and $K(\mu_a,1)=\infty$ ).
Arm $1$ is the unique optimal arm (the paper's standing assumption of §2; its reduction of several optimal arms to one is cited, not proved).
Display (4) and the index comparison are stated for $T\ge3$ (the page's $T\ge e$ ) and rounds $1\le t\le T$ .
Lemma 2 asserts only the existence of $D$ ; Lemma 3 is formalized as the analytic bound of §3.4 with the sign-corrected constant; Lemma 1's $C_b$ is read with the pre-draw count.

Trivializations ruled out. Thompson Sampling is not characterized by a predicate that an arbitrary policy could satisfy: it is the published run, which fixes the posterior draws, the argmax and the updates. The constant is quantified as $\forall\epsilon\,\exists C\,\forall T$ , never $\forall T\,\exists C$ , and no real number is extracted from a possibly infinite expectation.

Infrastructure and contributions. A complete development needs Beta–Binomial duality, Chernoff–Hoeffding bounds for binomial tails, optional skipping for the reward stacks of the played arms, and the KL-UCB counting argument. The Beta–Binomial identity is an open milestone shared with the Agrawal–Goyal mission. Proofs of any milestone, in particular Proposition 1, Lemma 4 and the analytic Lemma 3, are welcome; Lemma 3's bound and the index comparison are pure real analysis and reusable beyond bandits.

Selected references

E. Kaufmann, N. Korda, R. Munos, Thompson Sampling: An Asymptotically Optimal Finite Time Analysis, ALT 2012 (LNCS 7568); arXiv:1205.4217v2. https://arxiv.org/abs/1205.4217
W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25, 1933. https://doi.org/10.2307/2332286
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
S. Agrawal, N. Goyal, Analysis of Thompson Sampling for the multi-armed bandit problem, COLT 2012; arXiv:1111.1797. https://arxiv.org/abs/1111.1797
A. Garivier, O. Cappé, The KL-UCB algorithm for bounded stochastic bandits and beyond, COLT 2011; arXiv:1102.2490. https://arxiv.org/abs/1102.2490
E. Kaufmann, O. Cappé, A. Garivier, On Bayesian upper confidence bounds for bandit problems, AISTATS 2012. https://proceedings.mlr.press/v22/kaufmann12.html

17 thms2 active usersReviewed

Machine Learning Probability Random Matrix Theory·Captain: mikedeng1

Nuclear-Norm Penalization and Optimal Rates for Noisy Low-Rank Matrix Completion 3: Uniform Matrix Completion with |Yᵢ| ≤ η — With Probability ≥ 1 − e^{−t} the Oracle Bound (3.5) Holds for All AResearch Paper

Motivation

Matrix completion asks to recover a large matrix from a small number of its entries. It is the abstraction behind collaborative filtering (recommender systems in which a users × items rating matrix is observed on a sparse set of pairs), sensor localization from partial distance information, and system identification. Without structure the problem is hopeless; the standard structural assumption is that the unknown matrix has low rank, and the standard convex surrogate for rank is the nuclear norm, the sum of singular values.

In the noiseless case, exact recovery by nuclear-norm minimization from about $r(m_1\vee m_2)\,\mathrm{polylog}$ uniformly sampled entries was established by Candès and Recht (2009) and refined by Candès and Tao (2010) and Gross (2011). With noisy observations the relevant question is a rate: how fast does an estimator's error decrease with the number $n$ of observed entries? Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256, Ann. Statist. 2011) introduced a nuclear-norm penalized estimator that uses the known sampling distribution, showed that in matrix completion it is an explicit soft thresholding of the singular values of a rescaled data matrix, and proved for it sharp oracle inequalities (leading constant 1) whose rates are optimal up to logarithmic factors. This mission formalizes the version of that result for bounded responses: Theorem 4 of the paper, together with the probabilistic lemma and the matrix Bernstein inequality it rests on.

Setting

Fix positive integers $n, m_1, m_2$ and write $\mathbb R^{m_1\times m_2}$ for the real $m_1\times m_2$ matrices, with scalar product $\langle A,B\rangle=\operatorname{tr}(A^\top B)$ , Frobenius norm $\|A\|_2$ , nuclear norm $\|A\|_1$ (sum of singular values) and operator norm $\|A\|_\infty$ (largest singular value). Set $m=m_1+m_2$ and write $m_1\wedge m_2=\min(m_1,m_2)$ .

The matrix completion basis is

\mathcal X=\{e_j(m_1)e_k^\top(m_2):1\le j\le m_1,\ 1\le k\le m_2\},

where $e_k(m)$ are the canonical basis vectors of $\mathbb R^m$ . One observes $n$ independent random pairs $(X_i,Y_i)$ , where $X_i$ is uniformly distributed on $\mathcal X$ and $Y_i$ is real, following the trace regression model

\mathbb E(Y_i\mid X_i)=\operatorname{tr}(X_i^\top A_0),

for an unknown $A_0\in\mathbb R^{m_1\times m_2}$ . Thus $Y_i$ is a noisy reading of the entry of $A_0$ selected by $X_i$ ; this is matrix completion under uniform sampling at random (USR), entries possibly sampled more than once.

The estimator is, for a regularization parameter $\lambda>0$ ,

\hat A^\lambda=\operatorname*{argmin}_{A\in\mathbb R^{m_1\times m_2}}\Big(\frac1{m_1m_2}\|A\|_2^2-\Big\langle\frac2n\sum_{i=1}^nY_iX_i,A\Big\rangle+\lambda\|A\|_1\Big).

The stochastic error is the random matrix

\mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big).

Formalization targets

Goal: Theorem 4

Assume $\max_i|Y_i|\le\eta$ almost surely. For $t>0$ and

\lambda\ge4\eta\max\Big\{\sqrt{\frac{t+\log m}{(m_1\wedge m_2)n}},\ \frac{2(t+\log m)}{n}\Big\},

with probability at least $1-e^{-t}$ , simultaneously for all $A\in\mathbb R^{m_1\times m_2}$ ,

\|\hat A^\lambda-A_0\|_2^2\le\|A-A_0\|_2^2+m_1m_2\min\Big\{2\lambda\|A\|_1,\ \Big(\frac{1+\sqrt2}2\Big)^2m_1m_2\lambda^2\operatorname{rank}(A)\Big\}.

Milestones

(1.4): $\|A\|_{L_2(\Pi)}^2=\frac1n\sum_i\mathbb E\langle A,X_i\rangle^2=(m_1m_2)^{-1}\|A\|_2^2$ for the uniform design.
Theorem 1 for USR matrix completion: at every sample point where $\lambda\ge2\|\mathbf M\|_\infty$ , the inequality above holds for all $A$ (a deterministic statement).
Proposition 1 (matrix Bernstein): for independent centred $m_1\times m_2$ random matrices $Z_i$ with $\|Z_i\|\le U$ a.s., with probability at least $1-e^{-t}$ ,

\Big\|\frac{Z_1+\dots+Z_n}n\Big\|\le2\max\Big\{\sigma_Z\sqrt{\frac{t+\log m}n},\ U\frac{t+\log m}n\Big\}.

(6.2): for $X$ uniform on $\mathcal X$ , $\|X\|=1$ , $\|\mathbb EX\|=(m_1m_2)^{-1/2}$ , $\sigma_X^2=1/(m_1\wedge m_2)$ .
Lemma 1: with probability at least $1-e^{-t}$ , $\|\mathbf M\|\le2\eta\max\{\sqrt{(t+\log m)/((m_1\wedge m_2)n)},\ 2(t+\log m)/n\}$ .

Significance

Theorem 4 is a non-asymptotic, sharp oracle inequality: the leading constant in front of $\|A-A_0\|_2^2$ is 1, so the bound applies to misspecified targets ( $A_0$ not low rank) without loss. Taking $A=A_0$ and $t$ of order $\log m$ gives a normalized Frobenius error of order $\eta^2(m_1\vee m_2)\operatorname{rank}(A_0)\log(m)/n$ , which the paper's minimax lower bounds (§4) show to be optimal up to the logarithm. Because no model is needed for Lemma 1, the same probability bound also drives the paper's statistical-learning reformulation (Theorem 9).

The theorems here are proved in the paper. What is open is their formalization: no matrix Bernstein inequality, and no oracle inequality for nuclear-norm penalized estimators, has a machine-checked proof on this platform. Proposition 1 in particular is a reusable concentration tool well beyond this paper (covariance estimation, random graphs, sketching).

Difficulty

The deterministic part (milestone 2) needs the subdifferential of the nuclear norm, which is not in Mathlib. The probabilistic part is where the obvious argument fails. Bounding $\|\mathbf M\|_\infty$ entrywise and summing, or bounding it by the Frobenius norm, loses a factor polynomial in the dimension; a union bound over a net of the unit sphere loses the factor $m_1\wedge m_2$ that makes the rate optimal. The correct rate requires a noncommutative Bernstein inequality, controlling the operator norm of a sum of independent random matrices through the matrix variance $\sigma_Z^2$ at the price of only a $\log(m_1+m_2)$ factor. The matrix-analytic machinery such inequalities depend on (trace inequalities for matrix exponentials, the passage from rectangular to symmetric matrices) is not currently available in Mathlib.

Formalization scope

All objects are local to the namespace KLTNuclear.Completion, built on the published MatrixCompletion definitions (RealMatrix, nuclearNorm, spectralNorm, frobeniusNormSq, matrixInner, coordinateMatrix). Conventions:

The probability space carries IsProbabilityMeasure; $n,m_1,m_2\ge1$ are hypotheses. $\log$ is the natural logarithm; $m=m_1+m_2\ge2$ .
The design is encoded by uniform random indices $I_i\in[m_1]\times[m_2]$ with $X_i=e_{j_i}e_{k_i}^\top$ . Mathlib has no $\sigma$ -algebra on Matrix, so measurability, independence and conditioning on a random matrix use its entry array with the product $\sigma$ -algebra; expectations of matrices are entrywise.
The model (1.1) is a conditional expectation given $\sigma(X_i)$ . Independence of the pairs $(X_i,Y_i)$ is the paper's standing assumption (p. 1) and is assumed in Lemma 1 and Theorem 4, whose proof applies Proposition 1 to $Z_i=Y_iX_i-\mathbb E(Y_iX_i)$ ; the $Y_i$ are not assumed identically distributed. $\lambda>0$ is the standing assumption of (1.6). Integrable responses are assumed in milestone 2, bounded measurable responses in Lemma 1 and Theorem 4.
$\hat A^\lambda$ is any minimizer of (3.1) at each sample point (it exists and is unique, but neither fact is assumed); the soft-thresholding formula (3.2) is not used as a definition.
"With probability at least $1-e^{-t}$ " is encoded as an upper bound $e^{-t}$ on the outer measure of the failure set; in Theorem 4 the failure set is $\{\omega:\exists A,\ \text{(3.5) fails}\}$ , so the bound is uniform in $A$ . A formalization that fixes $A$ before the probability is weaker and is not the target.
No printed slip affects these statements; Corollary 2(ii) of the paper, whose $\lambda$ falls below (3.6), is deliberately not included.

The source is the arXiv preprint arXiv:1011.6256v4. Welcome contributions: a general matrix Bernstein inequality (Hermitian and rectangular forms), the nuclear-norm subdifferential, and proofs of the deterministic milestone.

Selected references

V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011; preprint arXiv:1011.6256v4. https://arxiv.org/abs/1011.6256
J. A. Tropp, User-friendly tail bounds for sums of random matrices, Found. Comput. Math. 12, 2012. https://doi.org/10.1007/s10208-011-9099-z
E. J. Candès, B. Recht, Exact matrix completion via convex optimization, Found. Comput. Math. 9, 2009. https://doi.org/10.1007/s10208-009-9045-5
E. J. Candès, T. Tao, The power of convex relaxation: near-optimal matrix completion, IEEE Trans. Inform. Theory 56, 2010. https://doi.org/10.1109/TIT.2010.2044061
D. Gross, Recovering low-rank matrices from few coefficients in any basis, IEEE Trans. Inform. Theory 57, 2011. https://doi.org/10.1109/TIT.2011.2104999

12 thms2 active usersReviewed

Completed

Machine Learning Theoretical Computer Science·Captain: wurtle

Memory and precision in noiseless Gaussian regressionResearch Paper

Motivation

A single exact linear equation $y = \langle x, s\rangle$ about an unknown unit vector $s \in \mathbb{R}^d$ carries arbitrarily fine information: $d$ independent Gaussian equations determine $s$ almost surely, provided all of them can be kept. A learner that reads the equations once, in order, and keeps only a bounded number of bits between them faces a different problem. The question asked here is how many noiseless measurements such a learner needs in order to reach a prescribed angular precision $\epsilon$ , as a function of its memory.

This is a question about memory–sample trade-offs: how much a bound on persistent memory forces a learning procedure to read more data. With unbounded real registers, the randomized Kaczmarz update $z_t = z_{t-1} + \frac{y_t - \langle x_t, z_{t-1}\rangle}{\|x_t\|^2} x_t$ satisfies $\mathbb{E}\|z_t - s\|^2 = (1 - 1/d)^t$ on isotropic Gaussian rows, so order $d\log(1/\epsilon)$ samples suffice. That update stores real numbers and gives no finite-bit upper bound; the question is whether a learner with roughly $d^2$ bits can do better than this scale.

Background

1937. Kaczmarz introduces the projection method for linear systems; Strohmer and Vershynin (2009) give the randomized version with exponential convergence.
2014. Shamir's finite-message framework for online and distributed learning includes bounded-memory online processing as a special case.
2015. Steinhardt and Duchi prove memory-dependent minimax rates for sparse linear regression with noise.
2016. Steinhardt, Valiant and Wager relate memory, communication and statistical queries and pose a quadratic-memory versus exponential-sample conjecture for parity learning; Raz proves a time–space lower bound for parity learning, and in 2017 extends the method to a large class of learning problems.
2019. Sharan, Sidford and Valiant prove that for Gaussian regression with tiny uniform additive noise, a learner with at most $d^2/4$ bits needs $\Omega(d\log r)$ samples to reach Euclidean accuracy $d^{-r}$ , in a stated range of $r$ , and ask (Section 1.1) whether the first-order sample dependence on precision is optimal under bounded memory. In the same year Dagan, Kur and Shamir prove quadratic-space lower bounds for two different linear-prediction tasks in the streaming model.
2026. The OpenAI preprint Memory and precision in noiseless Gaussian regression (dated September 27, 2026) states an $\Omega_A(d\log(1/\epsilon))$ lower bound for exact observations and memory $Ad^2$ . It has not been peer reviewed, and the Lean statement of its main theorem is open on this platform.

Setting

Fix integers $d \ge 2$ , $M \ge 0$ , $T \ge 0$ . A signal $s$ lies on the unit sphere $S^{d-1} \subset \mathbb{R}^d$ . At step $t \in \{1,\dots,T\}$ the learner receives the pair $(x_t, y_t)$ with $x_t \sim N(0, I_d)$ independent and $y_t = \langle x_t, s\rangle$ exactly (no noise).

A finite-state learner with $M$ bits keeps a state in a set of at most $2^M$ elements. A data-independent shared seed $\omega$ (drawn from a probability space $(\Omega,\rho)$ ) may select its rules. Given the seed, the current state, the step index and the current pair, a transition chooses the next state and whether to stop; it may perform unrestricted computation but retains only the next state. The learner must stop by the deterministic horizon $T$ . Its output $\hat s \in S^{d-1}$ is a function of the terminal state, the stopping index and the seed only; a discarded observation cannot be read again. Success at precision $\epsilon$ means angular error $\arccos\langle \hat s, s\rangle \le \epsilon$ .

Write $\sigma_d$ for the uniform probability measure on $S^{d-1}$ . Uniform success is the probability of success when $S \sim \sigma_d$ is drawn independently of the rows and the seed.

In Lean (OAI.NoiselessRegression), the state space is Fin (2 ^ M), a learner is a structure Learner d M T Ω with fields initialChoice, transition, output, the sample law is the product of stdGaussian on EuclideanSpace ℝ (Fin d), and uniformSuccess and success are the probabilities defined above. Randomness during the run is represented through the arbitrary seed space $\Omega$ .

Formalization targets

Goal: `OAI.NoiselessRegression.main`

The goal is the conjunction of two statements.

Fixed quadratic memory (Theorem 1.2): for every $A > 0$ there are $c_A > 0$ and $d_A$ such that, for $d \ge d_A$ , $M \le A d^2$ , $0 < \epsilon \le 1/10$ , and every admissible learner,

\Pr_{S\sim\sigma_d}\big\{\arccos\langle \hat s, S\rangle \le \epsilon\big\} \ge \tfrac23 \;\Longrightarrow\; T \ge c_A\, d \log(1/\epsilon).

Subquadratic memory (Corollaries 1.3 and 1.4): there is an absolute $c > 0$ such that for every memory sequence $M(d) = o(d^2)$ there is $d_0$ with the same conclusion $T \ge c\, d\log(1/\epsilon)$ for $d \ge d_0$ , under either uniform success at least $2/3$ or success at least $2/3$ for every fixed signal $s$ .

No relation between $\epsilon$ and $M$ is assumed; the constant is absolute in the subquadratic case.

Milestone: supporting estimates (`OAI.MemoryPrecision.main`)

A single bundled statement collecting the paper's projection-density and backward-block estimates (Theorem 3.1, Propositions A.1, A.4, A.5, B.6, B.7, Corollary 8.2), the cube-prior precision bound (Proposition 8.3), and the explicit success bound after a bounded number of samples (Proposition 5.3):

\Pr\{\arccos\langle \hat s, S\rangle \le \epsilon\} \le \min\Big\{1, \Big[2\epsilon\, e^{C(1+M/d^2)\lceil T/q\rceil}\Big]^{(d-1)/2}\Big\},\qquad q = \lfloor (d-1)/8 \rfloor.

Significance

The result. Theorem 1.2 answers, for exact observations and isotropic Gaussian rows, the precision question raised in Section 1.1 of Sharan–Sidford–Valiant: with $O(d^2)$ bits, the $d\log(1/\epsilon)$ scale achieved by real-valued Kaczmarz cannot be improved, uniformly over all $0<\epsilon\le 1/10$ . Because an exact-observation learner can simulate added noise, the preprint derives from it an $\Omega_A(d r \log d)$ lower bound in the noisy experiment of Sharan–Sidford–Valiant at accuracy $d^{-r}$ , which strengthens their $\Omega(d\log r)$ bound in that range.

Formalizing it. The result is proved only in an unrefereed preprint; no machine-checked proof exists. A formal proof would certify a lower bound whose model (randomized measurable rules, early stopping, shared seeds, measurability conventions) is delicate, and the conventions are already fixed in the Lean definitions. Remaining work: the full formal proof, and as a variant the every-signal version of Theorem 1.2 for fixed $A$ (Corollary 1.4), which the Lean goal states only in the subquadratic case.

Difficulty

Conditioning the uniform prior on one exact observation confines the signal to a hyperplane section of the sphere, a law singular with respect to the original spherical measure; information-theoretic arguments that track a posterior density therefore break down after a single step. Arguments for noisy observations, such as Sharan–Sidford–Valiant's, rely on the noise to keep posteriors spread out and do not transfer to the more informative exact experiment. The bound must also hold uniformly in $\epsilon$ with no relation between $\epsilon$ and $M$ , so a learner with $\Theta(d^2)$ bits must be prevented from storing $\log(1/\epsilon)$ bits per coordinate for very small $\epsilon$ .

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d); signals and outputs in Metric.sphere 0 1. The uniform sphere law is the normalized toSphere measure; rows are i.i.d. stdGaussian.
States are Fin (2 ^ M); the first component of each action is the stop flag. Runs that never stop are forced to terminate at index $T$ .
Learner.Admissible requires a.e.-measurability of the initial choice, transitions (against Gaussian × Lebesgue on pairs), outputs, and of the full experiment under each fixed signal and under the uniform prior.
Probabilities are ℝ≥0∞-valued; the threshold is $2/3$ ; angular error is Real.arccos ⟪ŝ, s⟫; $\log$ is natural.
The seed space $\Omega$ is an arbitrary probability space in universe u, so randomized learners are covered by placing their randomness in the seed.

The goal cannot be satisfied trivially: the hypotheses range over all admissible learners, and the success threshold $2/3$ is achievable (with large $T$ ), so the implication has content.

A complete development needs Gaussian measures on Euclidean space, spherical measure and cap estimates, Gram determinants and affine distances, $L^q$ densities of Gaussian projections, and measurable selection of Borel versions of kernels. The projection-density estimates are reusable beyond this mission. Contributions toward the bundled milestone, or toward any of its component estimates, are welcome.

Selected references

OpenAI, Memory and precision in noiseless Gaussian regression, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Memory-and-precision-in-noiseless-Gaussian-regression-September-27-2026/paper.pdf
V. Sharan, A. Sidford, G. Valiant, Memory-Sample Tradeoffs for Linear Regression with Small Error, STOC 2019. https://doi.org/10.1145/3313276.3316403 (full version https://arxiv.org/abs/1904.08544)
R. Raz, Fast Learning Requires Good Memory: A Time-Space Lower Bound for Parity Learning, 2016. https://arxiv.org/abs/1602.05161
R. Raz, A Time-Space Lower Bound for a Large Class of Learning Problems, FOCS 2017. https://doi.org/10.1109/FOCS.2017.73
J. Steinhardt, G. Valiant, S. Wager, Memory, Communication, and Statistical Queries, COLT 2016. https://proceedings.mlr.press/v49/steinhardt16.html
J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
O. Shamir, Fundamental Limits of Online and Distributed Algorithms for Statistical Learning and Estimation, NeurIPS 2014. https://proceedings.neurips.cc/paper_files/paper/2014/hash/cc427d934a7f6c0663e5923f49eba531-Abstract.html
Y. Dagan, G. Kur, O. Shamir, Space Lower Bounds for Linear Prediction in the Streaming Model, COLT 2019. https://proceedings.mlr.press/v99/dagan19b.html
T. Strohmer, R. Vershynin, A Randomized Kaczmarz Algorithm with Exponential Convergence, J. Fourier Anal. Appl. 15 (2009). https://doi.org/10.1007/s00041-008-9030-4

18 thms2 active usersReviewed

Linear algebra Machine Learning·Captain: mikedeng1

Nuclear-Norm Penalization and Optimal Rates for Noisy Low-Rank Matrix Completion 4: The Estimator Never Overestimates rank(A₀), Recovers It Above a Singular-Value Gap, and Obeys a Matching Lower BoundResearch Paper

Motivation

Noisy low-rank matrix completion asks to reconstruct an $m_1\times m_2$ matrix $A_0$ from $n$ noisy observations of randomly chosen entries. It is the statistical model behind collaborative filtering (recommender systems), sensor localization and system identification, and the nuclear-norm penalized least-squares estimator is its standard convex method. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4, Ann. Statist. 2011) proved sharp oracle inequalities for this estimator and showed that its Frobenius error is of order $\operatorname{rank}(A_0)(m_1\vee m_2)\log(m_1+m_2)/n$ up to normalization, which matches the minimax lower bound up to a logarithmic factor.

An upper bound alone does not say whether the estimator really attains this rate on a given matrix, nor whether it reports the correct rank. Section 5.1 of the paper answers both questions with a single deterministic theorem, Theorem 8: with a slightly inflated regularization parameter the estimator never overestimates the rank of $A_0$ ; if the nonzero singular values of $A_0$ are separated from zero it recovers the rank exactly, and its error is then bounded below by a quantity of the same order as the upper bounds. Rank recovery is the property practitioners rely on when they use the estimator for model selection (choosing the number of latent factors). This mission formalizes Theorem 8 and the steps of its proof.

Setting

Fix integers $m_1,m_2,n\ge1$ . The matrix completion basis is $\mathcal X=\{e_j(m_1)e_k(m_2)^\top\}$ , the $m_1m_2$ matrices with a single entry equal to $1$ . A sample consists of $n$ pairs $(X_i,Y_i)$ with $X_i\in\mathcal X$ (an observed position $(j_i,k_i)$ ) and $Y_i\in\mathbb R$ (a noisy observation of the corresponding entry of the unknown matrix $A_0$ ). Write $\langle A,B\rangle=\operatorname{tr}(A^\top B)$ , $\|A\|_2$ for the Frobenius norm, $\|A\|_1$ for the nuclear norm (the sum of the singular values) and $\|A\|_\infty$ for the operator norm (the largest singular value). The singular values of $B$ are $\sigma_1(B)\ge\sigma_2(B)\ge\dots\ge\sigma_{m_1\wedge m_2}(B)\ge0$ .

From the sample form

\mathbf X=\frac{m_1m_2}{n}\sum_{i=1}^nY_iX_i,\qquad \mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big).

In the paper's model $\mathbb E(Y_i\mid X_i)=\langle A_0,X_i\rangle$ with $X_i$ uniform on $\mathcal X$ , so $\mathbb E(Y_iX_i)=A_0/(m_1m_2)$ and $\mathbf X-A_0=m_1m_2\mathbf M$ : the matrix $\mathbf M$ is the stochastic error. For $\lambda>0$ the estimator (3.1) is

\hat A^\lambda=\operatorname{argmin}_{A\in\mathbb R^{m_1\times m_2}}\Big(\|A-\mathbf X\|_2^2+\lambda m_1m_2\|A\|_1\Big).

The objective is strictly convex, so the minimizer is unique; by (3.2) it is obtained from a singular value decomposition of $\mathbf X$ by soft thresholding every singular value at level $\lambda m_1m_2/2$ .

Formalization targets

Goal: Theorem 8 (p. 20)

Let $\lambda\ge2\|\mathbf M\|_\infty$ , $0<\delta<1$ and $\lambda'=\lambda/(1-\delta)$ , and put $\hat r=\operatorname{rank}(\hat A^{\lambda'})$ . Then

\hat r\le\operatorname{rank}(A_0).\tag{5.1}

If in addition $\min_{j:\sigma_j(A_0)\ne0}\sigma_j(A_0)\ge\lambda'm_1m_2$ , then

\hat r\ge\operatorname{rank}(A_0)\tag{5.2}

and

\|\hat A^{\lambda'}-A_0\|_2^2\ge\frac{\delta^2}{4(1-\delta)^2}\operatorname{rank}(A_0)\,(\lambda m_1m_2)^2.\tag{5.3}

Milestones

The milestones follow the proof on p. 20 in order:

the singular value perturbation display $|\sigma_j(\mathbf X)-\sigma_j(A_0)|\le\sigma_1(\mathbf X-A_0)=m_1m_2\|\mathbf M\|_\infty\le\lambda m_1m_2/2$ ;
the rank of $\hat A^\lambda$ equals the number of singular values of $\mathbf X$ above $\lambda m_1m_2/2$ (the consequence of (3.2) the proof uses);
(5.1);
(5.2);
$\|\mathcal P(\hat A^{\lambda'}-\mathbf X)\|_2=\sqrt r\,\lambda'm_1m_2/2$ when $\hat r=r$ , for the projector $\mathcal P$ onto the span of the top $r$ singular pairs $u_j(\mathbf X)v_j(\mathbf X)^\top$ ;
$\|\mathcal P(\mathbf X-A_0)\|_2\le\sqrt r\|\mathbf M\|_\infty m_1m_2\le\sqrt r\lambda m_1m_2/2$ .

Significance

The result. Theorem 8 turns the paper's upper bounds into two-sided statements. Combined with a probability bound for $\|\mathbf M\|_\infty$ (Corollary 3 of the paper), it shows that with high probability the estimator selects the true rank and that its error on well-conditioned low-rank matrices is not smaller than the rate of the upper bounds, so those bounds cannot be improved for this estimator. Because the theorem is deterministic given the event $\lambda\ge2\|\mathbf M\|_\infty$ , it applies unchanged to any noise model for which such a bound on the stochastic error is available.

Formalizing it. The theorem is proved in the paper; nothing in it is open. The mission produces a machine-checked version and, along the way, reusable linear algebra that is not on the platform in this form: Weyl's perturbation inequality for singular values in operator norm, the rank of a nuclear-norm proximal point, and the Frobenius norm of a projection onto a span of orthonormal rank-one matrices. The soft-thresholding representation (3.2) itself is the open platform item CaiCandesShen.Convergence.shrink_eq_prox (Cai–Candès–Shen, Theorem 2.1, after halving the objective); this mission references it rather than posing it again, and a proof of it would serve both missions.

Difficulty

The arithmetic of the proof is three lines; the content is in two facts about singular values that the paper takes from the literature. The first is Weyl's inequality $|\sigma_j(B)-\sigma_j(C)|\le\|B-C\|_\infty$ , which needs the min–max (Courant–Fischer) characterization of singular values; Mathlib defines singular values through the eigenvalues of $T^*T$ but has neither the min–max principle for them nor this inequality. The second is the description of the minimizer of $\|A-\mathbf X\|_2^2+\lambda m_1m_2\|A\|_1$ : one needs the subdifferential of the nuclear norm (2.1), or an equivalent von Neumann trace inequality, to show that soft thresholding is optimal, and then that its rank and its projection onto the top singular pairs are what the formula suggests. A naive approach that compares the estimator with $\mathbf X$ entrywise gives nothing about the rank; the proof needs the spectral structure.

Formalization scope

Matrices are MatrixCompletion.RealMatrix m₁ m₂ (Matrix (Fin m₁) (Fin m₂) ℝ) with the published norms frobeniusNormSq, frobeniusNorm, nuclearNorm, spectralNorm and SVD data SVD. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin, 0-based: the Lean singularValue B j is the paper's $\sigma_{j+1}(B)$ . The conventions committed to:

The statements are realization-wise: positions idx : Fin n → Fin m₁ × Fin m₂ and responses y : Fin n → ℝ are fixed, and every theorem holds for every data set satisfying $\lambda\ge2\|\mathbf M\|_\infty$ . The matrix $\mathbf M$ is written as $\frac1n\sum_iY_iX_i-A_0/(m_1m_2)$ , which is (2.2) under the model (1.1) and the uniform design; this is the paper's "Note that $\mathbf X-A_0=m_1m_2\mathbf M$ ". The probabilistic hypotheses are used for nothing else.
$n,m_1,m_2\ge1$ and $\lambda>0$ are assumed, as in the paper.
The estimator is any minimizer of (3.1) over all matrices, never the soft-thresholding formula; replacing the minimizer by formula (3.2) would assume the open Cai–Candès–Shen item.
$\min_{j:\sigma_j(A_0)\ne0}\sigma_j(A_0)\ge\lambda'm_1m_2$ is written "for every $j$ with $\sigma_j(A_0)\ne0$ "; for $A_0=0$ it is vacuous, as on the page. No real infimum over a possibly empty set is used.
The projector $\mathcal P$ is built from a singular value decomposition of $\mathbf X$ carried as data, with decreasing singular values, from its first $r$ pairs.

No printed slip was found in Theorem 8 or its proof; no hypothesis beyond the above is added.

Contributions welcome: Weyl's inequality for singular values (generally useful), the rank and top- $r$ projection of the nuclear-norm proximal point, and a proof of CaiCandesShen.Convergence.shrink_eq_prox.

The source is the arXiv preprint arXiv:1011.6256v4; all page and display numbers refer to it.

Selected references

V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011; preprint arXiv:1011.6256v4. https://arxiv.org/abs/1011.6256
J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20(4), 2010. https://doi.org/10.1137/080738970
G. W. Stewart, J.-G. Sun, Matrix Perturbation Theory, Academic Press, 1990 (reference [25] of the paper, p. 203).
E. J. Candès, Y. Plan, Matrix completion with noise, Proc. IEEE 98(6), 2010. https://doi.org/10.1109/JPROC.2009.2035722

13 thms2 active usersReviewed

Convex Optimization Random Matrix Theory·Captain: mikedeng1

Robust Principal Component Analysis?: Principal Component Pursuit with λ = 1/√n Exactly Recovers an Incoherent Low-Rank Matrix from a Constant Fraction of Randomly Located Gross ErrorsResearch Paper

Motivation

Principal component analysis finds the best low-rank approximation of a data matrix, and it is used everywhere data come as a table: images, video, genomics, web and survey data. Its weakness is well known: a single grossly corrupted entry can move the classical principal components arbitrarily far. In many applications the corruptions are not small noise but gross errors at a fraction of the entries: occlusions and specularities in face images, moving foreground objects in surveillance video, corrupted or adversarial records. Robust variants of PCA built on robust statistics or on alternating heuristics came without guarantees of exact recovery.

Candès, Li, Ma and Wright (J. ACM 58(3), 2011) showed that a single convex program recovers both the low-rank part and the corruptions exactly, under a randomness assumption on the corruption pattern only, with a weight that needs no tuning.

Timeline.

2009: Candès and Recht prove exact matrix completion by nuclear-norm minimization under incoherence (FoCM 2009). Their concentration results reappear here as Theorem 2.6 and Lemma 3.2.
2009: Chandrasekaran, Sanghavi, Parrilo and Willsky give deterministic conditions for the same convex decomposition (SIAM J. Optim. 2011, arXiv:0906.2220). As compared on p. 7 of the present paper, these conditions allow only a vanishing fraction $O((nr)^{-1/2})$ of corrupted entries, and they leave the weight $\lambda$ to be searched for.
2009: Gross introduces the golfing scheme for constructing dual certificates (IEEE Trans. Inf. Theory 2011, arXiv:0910.1879). This paper adapts it.
2009–2011: the present paper (preprint of 17 December 2009) proves Theorem 1.1: a constant fraction of corrupted entries and rank up to $n/(\log n)^2$ .

Setting

Let $L_0\in\mathbb R^{n\times n}$ have rank $r$ and compact singular value decomposition $L_0=\sum_{k=1}^r\sigma_k u_kv_k^*$ with $\sigma_k>0$ , where $U=[u_1,\dots,u_r]$ and $V=[v_1,\dots,v_r]$ have orthonormal columns. The nuclear norm $\|M\|_*$ is the sum of the singular values of $M$ , and $\|M\|_1=\sum_{ij}|M_{ij}|$ is the entrywise $\ell_1$ norm. Given $M=L_0+S_0$ , Principal Component Pursuit (PCP) solves

\text{minimize }\ \|L\|_*+\lambda\|S\|_1\qquad\text{subject to}\qquad L+S=M. \tag{1.1}

PCP is exact when $(L_0,S_0)$ is its unique solution.

$L_0$ satisfies the incoherence condition with parameter $\mu$ when

\max_i\|U^*e_i\|^2\le\frac{\mu r}{n},\qquad\max_i\|V^*e_i\|^2\le\frac{\mu r}{n},\qquad\|UV^*\|_\infty\le\sqrt{\frac{\mu r}{n^2}},\tag{1.2–1.3}

where $\|X\|_\infty=\max_{ij}|X_{ij}|$ . This excludes low-rank matrices that are themselves sparse, which no method could tell apart from corruptions.

The sparse component is $S_0=\mathcal P_\Omega S$ , where $S$ is an arbitrary fixed matrix and $\mathcal P_\Omega$ keeps the entries in a random support $\Omega$ and zeros the others. In Theorem 1.1, $\Omega$ is uniform among all subsets of $[n]\times[n]$ of cardinality $m$ . In the Bernoulli model $\Omega\sim\mathrm{Ber}(\rho)$ each entry belongs to $\Omega$ independently with probability $\rho$ . Nothing is assumed about the magnitudes or signs of $S$ .

The proof works with the tangent space $T=\{UX^*+YV^*\}$ of the rank- $r$ matrices at $L_0$ , its orthogonal projections $\mathcal P_T$ and $\mathcal P_{T^\perp}$ , and the operator norm $\|\cdot\|$ (largest singular value).

Formalization targets

Goal: Theorem 1.1, square case

There are positive numerical constants $c,\rho_r,\rho_s$ such that, whenever $L_0$ obeys (1.2)–(1.3) and

\operatorname{rank}(L_0)\le\rho_r\,n\,\mu^{-1}(\log n)^{-2}\qquad\text{and}\qquad m\le\rho_s\,n^2,\tag{1.4}

PCP with $\lambda=1/\sqrt n$ is exact with probability at least $1-c\,n^{-10}$ over the support of $S_0$ .

The constants are not specified, so the goal survives any improvement of them.

Milestones

They are listed in the order the proof uses them:

the coordinate bound (2.2);
the elimination theorem (Theorem 2.2): exactness passes to trimmed sparse components;
the transfer from the Bernoulli model to the uniform model (§7.1);
derandomization (Theorem 2.3): random signs suffice;
the dual certificate conditions (Lemma 2.4, Lemma 2.5, (2.4));
the concentration results (Theorem 2.6, Corollary 2.7, Lemmas 3.1 and 3.2);
the two halves of the certificate: the golfing certificate $W^L$ (Lemma 2.8) and the least-squares certificate $W^S$ (Lemma 2.9).

Significance

The result. Theorem 1.1 is the founding guarantee of robust PCA by convex optimization. It allows a constant fraction of arbitrarily large corruptions and a rank as large as $n/(\log n)^2$ , with a universal weight $\lambda=1/\sqrt n$ . It supports applications such as background modeling in video and the removal of shadows and specularities from face images, and it is the template for later work on noisy and partially observed variants, e.g. stable PCP (Zhou et al., ISIT 2010, arXiv:1001.2363).

Formalizing it. The theorem is proved on paper; no machine-checked proof of it is known. A formal proof would check a chain that combines convex duality for the nuclear and $\ell_1$ norms, operator concentration for random sampling, and a probabilistic coupling. The reusable parts are general: the elimination and derandomization arguments, the certificate lemmas, the golfing scheme and the Bernoulli-to-uniform transfer. They also serve matrix completion and other sparse-plus-low-rank problems. The matrix-completion definitions this mission builds on are already published on the platform.

Difficulty

The obvious plan is to write down the subgradient optimality conditions of (1.1) and exhibit a dual certificate. The difficulty is the exact certificate (2.3). It requires $\mathcal P_\Omega(UV^*+W)=\lambda\operatorname{sgn}(S_0)$ exactly, and at the same time $\|W\|<1$ and $\|\mathcal P_{\Omega^\perp}(UV^*+W)\|_\infty<\lambda$ , with $\Omega$ a constant fraction of all entries. The natural least-squares candidate cannot be controlled in the sup norm on $\Omega^\perp$ by moment methods at this sparsity level.

A second difficulty is probabilistic. The theorem allows fixed, adversarial signs. The concentration tools need independence, which fixed signs do not give.

Finally, every step must hold uniformly with failure probability $O(n^{-10})$ and with constants independent of $n$ , $L_0$ and $S$ .

Formalization scope

All statements are for square real matrices RealMatrix n n. The rectangular sentences of the paper are not stated. The mission reuses the published matrix-completion definitions for the following objects:

the nuclear norm (sum of Mathlib singular values);
the operator norm;
the Frobenius norm and inner product;
$\|\cdot\|_\infty$ and $\mathcal P_\Omega$ ;
SVD data SVD L0 r, with $UV^*$ = signMatrix;
$\mathcal P_T$ and $\mathcal P_{T^\perp}$ ;
the Bernoulli and uniform laws on supports.

The following conventions are fixed:

Rank. The rank is carried by SVD data SVD L0 r with positive singular values, so $r=\operatorname{rank}L_0$ . Every statement holds for every such decomposition.
Exactness. "Exact" means unique optimality: every other feasible pair has a strictly larger objective.
Probabilities. Probabilities are finite sums of product weights. Operator norms of operators on matrices are taken with respect to the Frobenius norm.
Rank condition. It is written multiplied out, $r\mu(\log n)^2\le\rho_rn$ , with the natural logarithm.
Constants. "With high probability" means probability at least $1-c\,n^{-10}$ , with $c$ a numerical constant. Every numerical constant is quantified before $n$ , the matrices and the parameters.
Least-squares certificate. $W^S$ is defined by the Neumann series (2.7), which the paper gives as an equivalent definition of (2.6), and it is used only on the event $\|\mathcal P_\Omega\mathcal P_T\|<1/2$ .
Golfing. The golfing sets are indexed from $0$ .
Citations. Theorem numbers and pages are those of the preprint dated 17 December 2009, which is the cited source of the J. ACM article.

Trivializing formalizations are excluded. A constant $c$ chosen after $n$ would make the goal vacuous, so all constants come first. A non-strict "optimal" would make exactness much weaker, so exactness is strict. The values of $S_0$ are fixed before the support is drawn.

Contributions of any kind are welcome. Proofs of the deterministic milestones (Theorem 2.2, Lemmas 2.4 and 2.5, (2.4), (2.2)) are self-contained convex analysis and linear algebra. The concentration milestones need matrix Bernstein-type inequalities and operator concentration, which are reusable well beyond this mission.

Selected references

E. J. Candès, X. Li, Y. Ma, J. Wright, Robust principal component analysis?, Journal of the ACM 58(3), Article 11, 2011. https://doi.org/10.1145/1970392.1970395
E. J. Candès, B. Recht, Exact matrix completion via convex optimization, Foundations of Computational Mathematics 9(6), 717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
D. Gross, Recovering low-rank matrices from few coefficients in any basis, IEEE Transactions on Information Theory 57(3), 1548–1566, 2011. https://arxiv.org/abs/0910.1879
V. Chandrasekaran, S. Sanghavi, P. A. Parrilo, A. S. Willsky, Rank-sparsity incoherence for matrix decomposition, SIAM Journal on Optimization 21(2), 572–596, 2011. https://arxiv.org/abs/0906.2220
Z. Zhou, X. Li, J. Wright, E. J. Candès, Y. Ma, Stable principal component pursuit, ISIT 2010. https://arxiv.org/abs/1001.2363

20 thms2 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

Optimal Aggregation of Classifiers in Statistical Learning: The Adaptive Classifier Attains the Optimal Fast Rate up to a Logarithmic Factor Simultaneously on All Classes (Theorem 3)Research Paper

Motivation

Binary classification asks for a rule that predicts a label $Y\in\{0,1\}$ from a feature vector $X\in\mathbb R^d$ , given $n$ labelled examples. A classical way to measure how hard this is, due to Mammen and Tsybakov (1999), treats classification as the estimation of a set, the region where label $1$ is more likely, and asks how fast the excess misclassification risk of a data-driven classifier can tend to zero. The answer depends on two parameters: the complexity $\rho$ of the class of candidate sets, measured by entropy with bracketing, and the margin parameter $\kappa$ , which measures how sharply the conditional probability of label $1$ moves away from $1/2$ near the decision boundary.

Tsybakov (2004) showed that empirical risk minimization over a suitable net attains the rate $n^{-\kappa/(2\kappa+\rho-1)}$ , which approaches $n^{-1}$ ("fast rates") for favourable margins and simple classes, and that this rate is minimax optimal. In practice neither $\rho$ nor $\kappa$ is known. The main result of the paper, Theorem 3, constructs a single classifier that adapts to both and attains the optimal rate up to a logarithmic factor simultaneously over a whole family of classes. The margin condition introduced here, often called the Tsybakov margin (or noise) condition, became a standard assumption of statistical learning theory, used for instance in the analysis of support vector machines and of plug-in rules (Audibert and Tsybakov 2007).

Setting

Observations are i.i.d. pairs $(X_1,Y_1),\dots,(X_n,Y_n)$ with law $\pi$ . Write $P_X$ for the law of $X$ and $\eta(x)=P(Y=1\mid X=x)$ for the regression function. A classifier is a Borel set $G\subseteq\mathbb R^d$ , predicting $1$ on $G$ . The Bayes classifier is $G^*=\{x:\eta(x)\ge1/2\}$ , and the excess risk of $G$ is

d(G,G^*)=\int_{G\triangle G^*}|2\eta(x)-1|\,P_X(dx)=R(G)-R(G^*),

where $R(G)=P(Y\ne I(X\in G))$ . Two pseudodistances between sets are used: $d_\triangle(G,G')=P_X(G\triangle G')$ and its empirical analogue $d_{\triangle,e}(G,G')=\frac1n\sum_iI(X_i\in G\triangle G')$ . The empirical risk is $R_n(G)=\frac1n\sum_i(Y_i-I(X_i\in G))^2$ .

A class $\mathcal G$ of sets has complexity bound $\rho>0$ if its $\delta$ -entropy with bracketing for $d_\triangle$ is at most $A\delta^{-\rho}$ for $0<\delta\le1$ . The margin assumption (A1) requires $d(G,G^*)\ge c_0\,d_\triangle^\kappa(G,G^*)$ whenever $d_\triangle(G,G^*)\le\varepsilon_0$ , with $\kappa\ge1$ . A class $\mathcal P$ of distributions is a $(\mathcal G^*,\kappa,\rho)$ -class if every $\pi\in\mathcal P$ has $G^*_\pi\in\mathcal G^*$ , satisfies (A1), and $\mathcal G^*$ has complexity bound $\rho<1$ (Definition 4).

Aggregation. Given classes $\mathcal G_1,\dots,\mathcal G_N$ with complexities $\rho_1\le\dots\le\rho_N$ and nested approximating sets $\mathcal N_1\subseteq\dots\subseteq\mathcal N_N$ , let $G_{nk}$ minimize $R_n$ over $\mathcal N_k$ . With the thresholds

T_{nk}(G,G')=(\log^2n)\max\Big\{n^{-1/(1+\rho_k)},\ \tfrac1{\sqrt n}d_{\triangle,e}^{(1-\rho_k)/2}(G,G')\Big\},

an index $j$ is admissible if, for every $k\ge j$ , some $G\in\mathcal N_j$ has $|R_n(G)-R_n(G_{nk})|\le T_{nk}(G,G_{nk})$ . The adaptive classifier is $G^*_n=G_{n\hat j}$ with $\hat j$ the smallest admissible index.

Formalization targets

Goal: Theorem 3

Under assumptions (A3)–(A4), with $\mathcal P_j$ a $(\mathcal G_j,\kappa,\rho_j)$ -class for each $j$ , $N=O(n^\beta)$ , and $\rho_1=\rho_{\min}$ , $\rho_N=\rho_{\max}$ fixed, there is $C<\infty$ such that for all $n>1$ and every $j$ ,

\sup_{\pi\in\mathcal P_j}E_{\pi,n}\,d(G^*_n,G^*)\le C\left(\frac{\log^4n}{n}\right)^{\kappa/(2\kappa+\rho_j-1)}.

Milestones

Appendix, Lemmas 7–11: exponential tail bounds for suprema of ratio-type empirical processes over a class with complexity bound $\rho$ .
Theorem 1: ERM over an $an^{-1/(1+\rho)}$ -net of $\mathcal G^*$ attains $\sup_{\pi}E\,d(\hat G_n,G^*)=O(n^{-\kappa/(2\kappa+\rho-1)})$ .
Lemma 2: the deterministic comparison inequalities (27)–(28) for an admissible index.
Lemma 1: $\sup_\pi P(\hat j>j^*)=o(1/n)$ .
Lemmas 3, 5, 6, 4: the moment and probability bounds that combine into Theorem 3.

Significance

Theorem 3 says that a procedure which knows neither the class containing $G^*$ nor the margin parameter loses at most a factor $(\log n)^{4\kappa/(2\kappa+\rho_j-1)}$ against the optimal rate on every class at once; combined with the lower bound of Theorem 2 it identifies the optimal adaptive rate up to logarithms. Corollary 1 extends it to a continuum of classes $\{\mathcal G_\rho\}_{\rho\in[\rho_{\min},\rho_{\max}]}$ . The selection rule is a Lepski-type pairwise comparison of empirical risks, and the analysis is one of the early results on adaptation to the margin.

The result is proved in the paper, with an Appendix that derives the empirical-process inequalities from van de Geer (2000). No part of it is known to have a machine-checked proof. A formalization would produce reusable infrastructure: entropy with bracketing for classes of sets, ratio-type deviation inequalities for empirical processes, and the excess-risk identity for 0–1 loss.

Difficulty

The obvious argument controls each $G_{nk}$ separately and takes a union bound over $k$ . That fails: the bound for $G_{nk}$ at a class $\mathcal G_k$ that does not contain $G^*$ says nothing about $d(G_{nk},G^*)$ , and the adaptive rule compares classifiers from different classes through random thresholds that depend on the empirical distance $d_{\triangle,e}$ . The central steps are to show that the true index $j^*$ is admissible with probability $1-o(1/n)$ uniformly over a polynomially growing number of classes, and to replace $d_{\triangle,e}$ by $d_\triangle$ inside the thresholds at a constant-factor cost. Both rest on exponential, ratio-type deviation bounds for suprema over classes of infinite entropy, which are not in Mathlib.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, labels are Bool with true ↔ 1, and a distribution is a pair $(P_X,\eta)$ with $P_X$ a probability measure and $\eta$ measurable with values in $[0,1]$ ; the law of a pair is the published UnderstandingML.condLaw ( $X\sim P_X$ , then $Y\sim\mathrm{Bernoulli}(\eta(X))$ ). Classifiers are sets, risk is measured by $d$ via identity (2), and the complexity bound is stated as "some bracketing with $\log m\le A\delta^{-\rho}$ exists".

The Section 3 data ( $N_n$ , classes, nets, complexities, distribution classes) are indexed by $n$ . The formalization commits to the following readings of the page, all disclosed in the items:

one constant $A$ , $c_0$ , $\varepsilon_0$ for all classes;
condition (7) uniformly over the whole family unless $\varepsilon_0=1$ ;
complexity bounds for the design law of every distribution in the family;
constants in Theorem 3 and Lemmas 1, 3–6 uniform in the class index $j$ ;
"arg min" as any minimizer;
the pseudoclassifier $G_{nkj}$ extended by its fallback branch to $j>k$ ;
Lemmas 8–10 stated for every $c_1$ (or $c_2$ ), with constants that may depend on it.

Expectations are Lebesgue integrals over the sample, so each one carries the hypothesis that the data-dependent set is jointly measurable in (sample, point). This rules out the trivializing formalization in which a non-measurable classifier has integral $0$ and every rate bound holds for free. Probabilities of events involving suprema over uncountable classes are outer measures. Appendix suprema are real suprema over index sets bounded above. The goal is not vacuous: a solution-folder check exhibits a setup satisfying all hypotheses with $\hat j=1$ .

Contributions welcome: bracketing-entropy chaining bounds, the van de Geer inequalities (5.42)–(5.43), and the Appendix lemmas as standalone results.

Selected references

A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Ann. Statist. 32(1), 135–166, 2004. https://doi.org/10.1214/aos/1079120131
E. Mammen and A. B. Tsybakov, Smooth discrimination analysis, Ann. Statist. 27(6), 1808–1829, 1999. https://doi.org/10.1214/aos/1017939240
S. van de Geer, Empirical Processes in M-Estimation, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511802256
J.-Y. Audibert and A. B. Tsybakov, Fast learning rates for plug-in classifiers, Ann. Statist. 35(2), 608–633, 2007. https://doi.org/10.1214/009053606000001217
L. Devroye, L. Györfi and G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. https://doi.org/10.1007/978-1-4612-0711-5

19 thms2 active usersReviewed

Completed

Machine Learning Optimization·Captain: mikedeng1

Robust Regression and Lasso 1: Under Feature-Wise Norm-Bounded Column Disturbances, Worst-Case Least-Norm Regression Is Exactly ℓ1-Regularized Regression ‖b − Ax‖₂ + Σ cᵢ|xᵢ|Research Paper

Why robustness and the Lasso belong together

The Lasso (Tibshirani 1996; Chen, Donoho and Saunders 1998) fits a linear model $b \approx Ax$ by penalizing the ℓ¹ norm of the coefficients. It is one of the standard tools of high-dimensional statistics and signal processing, and its usual justification is statistical or geometric: the ℓ¹ penalty is a convex surrogate for sparsity, or the negative log-density of a Laplace prior. Xu, Caramanis and Mannor (arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7), 2010) give a different justification: an ℓ¹-regularized regression is exactly a robust regression, the problem of fitting the data well in the worst case when every feature of the observation matrix may be corrupted by a bounded disturbance.

This observation is the foundation of the rest of their paper (dual-norm regularizers from coupled disturbances, sparsity from robustness, consistency of the Lasso through a worst-case-expectation reading). It also connects two literatures. On the robust side, El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) computed the worst-case residual when the whole data matrix $[A\ b]$ is disturbed in a Frobenius-norm ball, obtaining $\|Ax-b\|+\sqrt{\|x\|^2+1}$ ; that result is already on the platform as RobustLS.Unstructured.worst_case_residual_closed_form. On the distributional side, Blanchet, Kang and Murthy (J. Appl. Probab. 56(3), 2019) obtained the square-root Lasso as a Wasserstein distributionally robust problem (RWPI.SqrtLasso.theorem_1). The present mission formalizes the feature-wise result that sits between them.

Setting

Fix integers $n$ (samples) and $m$ (features). The observation matrix $A\in\mathbb R^{n\times m}$ has columns $a_1,\dots,a_m\in\mathbb R^n$ , the features. The response is $b\in\mathbb R^n$ and a coefficient vector is $x\in\mathbb R^m$ , so that $Ax=\sum_{i=1}^m x_i a_i$ . All norms on $\mathbb R^n$ are Euclidean, $\|\cdot\|_2$ .

A disturbance of $A$ is a family $\Delta A=(\delta_1,\dots,\delta_m)$ of vectors $\delta_i\in\mathbb R^n$ , one per column; the disturbed matrix $A+\Delta A$ has columns $a_i+\delta_i$ . Given budgets $c_1,\dots,c_m\ge 0$ , the feature-wise uncoupled uncertainty set is

\mathcal U=\bigl\{(\delta_1,\dots,\delta_m)\;\big|\;\|\delta_i\|_2\le c_i,\ i=1,\dots,m\bigr\}. \tag{2}

Each feature is disturbed independently: no constraint couples the $\delta_i$ . The robust objective is the worst-case residual

R(x)=\sup_{\Delta A\in\mathcal U}\|b-(A+\Delta A)x\|_2,

and robust linear regression is problem (1), $\min_{x\in\mathbb R^m} R(x)$ . The ℓ¹-regularized regression problem is (3), $\min_{x\in\mathbb R^m} L(x)$ with

L(x)=\|b-Ax\|_2+\sum_{i=1}^m c_i|x_i| .

The loss in $L$ is the norm of the residual, not its square. In the Lean development, $Ax$ is matVec a x, $\mathcal U$ is uncertaintySet c, $R$ is robustObjective a b c, $L$ is l1RegularizedObjective a b c, and the disturbance $\delta_i^*=-c_i\,\mathrm{sgn}(x_i)\,u$ of the proof is worstCaseDisturbance c x u.

Formalization targets

Goal: Theorem 1 (p. 4)

For $n\ge1$ and budgets $c_i\ge 0$ , problem (1) with uncertainty set (2) is equivalent to problem (3): for every $x\in\mathbb R^m$ ,

x\ \text{minimizes}\ R\iff x\ \text{minimizes}\ L,\qquad\text{and}\qquad \inf_{x} R(x)=\inf_x L(x).

No minimizer is asserted to exist; the paper does not claim one.

Milestones (in the order the proof uses them)

Eq. (4), the upper bound: for every $\Delta A\in\mathcal U$ , $\|b-(A+\Delta A)x\|_2\le\|b-Ax\|_2+\sum_i|x_i|c_i$ .
Eq. (5), the attained worst case: with $u$ a unit vector equal to $(b-Ax)/\|b-Ax\|_2$ when $Ax\ne b$ , the disturbance $\delta_i^*=-c_i\,\mathrm{sgn}(x_i)\,u$ lies in $\mathcal U$ and

\|b-(A+\Delta A^*)x\|_2=\|b-Ax\|_2+\sum_i c_i|x_i| .

The per- $x$ identity stated at the start of the proof: for every $x$ ,

\max_{\Delta A\in\mathcal U}\|b-(A+\Delta A)x\|_2=\|b-Ax\|_2+\sum_{i=1}^m c_i|x_i|,

with the maximum attained.

Significance

The result. Theorem 1 turns a min–max problem whose inner maximization is nonconvex into a single convex, second-order-cone-representable problem, and it gives the regularization weights a concrete meaning: $c_i$ is the size of the disturbance feature $i$ is protected against. With equal budgets $c_i=c$ it recovers the Lasso with the unsquared loss, which coincides with the usual Lasso up to a data-dependent change of the regularization coefficient. Every later result of the paper (Theorem 3 for arbitrary norms, the coupled uncertainty sets of Corollary 1, the sparsity theorems of §IV, the kernel-density reading of §V) builds on this identity or its proof pattern.

Formalizing it. The theorem is proved in the paper; the mission formalizes that proof. No machine-checked version of it exists on the platform or, to our knowledge, elsewhere. The definitions here (the uncertainty set, the worst-case objective as a genuine supremum, the explicit worst-case disturbance) are the base on which the companion missions of this series (coupled norms, sparsity, worst-case expectation) restate their own objects.

Difficulty

The upper bound (4) is the triangle inequality. The substance is the lower bound: one must exhibit a single admissible disturbance that makes every column perturbation push the residual in the same direction, and check that it is admissible and that the resulting norm adds up exactly. Two edge cases make the obvious argument fail as written. When $Ax=b$ the direction $(b-Ax)/\|b-Ax\|_2$ is undefined and an arbitrary unit vector must be used instead, which requires $n\ge1$ ; for $n=0$ the identity reads $0=\sum_i c_i|x_i|$ and is false. When $x_i=0$ the sign must be $0$ , not $\pm1$ , for the computation in (5) to go through. Passing from the per- $x$ identity to the equivalence of the two minimization problems is then routine, but it must be done without assuming that either problem has a minimizer.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $A$ is the family of its columns a : Fin m → EuclideanSpace ℝ (Fin n), and $Ax=\sum_i x_i\,a_i$ . Indices $1,\dots,m$ are Fin m. A disturbance is δ : Fin m → EuclideanSpace ℝ (Fin n), and $(A+\Delta A)x$ is matVec (a + δ) x.
Readings of "max" and "min". The paper writes "max" over $\mathcal U$ . $R(x)$ is defined as the supremum over $\mathcal U$ taken in EReal, so it is $-\infty$ on an empty set and $+\infty$ on an unbounded one and carries no junk value. That the maximum is attained is stated separately, as IsGreatest of the set of residual norms (milestone 3). "min" in (1) and (3) is read as: the same set of minimizers (IsMinOn … Set.univ) and the same infimum, computed in EReal. No existence of minimizers is claimed.
Added hypothesis. $n\ge1$ (0 < n), which the paper leaves implicit. The budgets $c_i\ge0$ are the paper's own assumption on (2).
Sign convention. $\mathrm{sgn}$ is Real.sign, with $\mathrm{sgn}(0)=0$ .
Trivializing formalizations ruled out. The robust objective is defined as the supremum over $\mathcal U$ , never by its closed form $\|b-Ax\|_2+\sum_i c_i|x_i|$ , which would make milestone 3 and the goal hold by definition; and no real sSup with junk value $0$ is used, so the identities cannot hold vacuously.
Not in scope. The remark that (3) "recovers the well-known Lasso" (it has the unsquared loss), §II-B and Theorem 2 (probabilistic construction of the budgets), and the other sections of the paper, which are separate missions.
Infrastructure. Only Mathlib's inner-product-space and EReal order theory are needed. The squared-loss Lasso definitions already on the platform (XuMannorRobust.Lasso.*, LassoDantzig.*) are different objects and are not used. Contributions are welcome on each milestone independently; a proof of the per- $x$ identity for an arbitrary norm on $\mathbb R^n$ would also serve Theorem 3 of the paper.

Selected references

H. Xu, C. Caramanis, S. Mannor, Robust Regression and Lasso, arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7):3561–3574, 2010. https://arxiv.org/abs/0811.1790v1, https://doi.org/10.1109/TIT.2010.2048503
R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1):267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
S. S. Chen, D. L. Donoho, M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20(1):33–61, 1998. https://doi.org/10.1137/S1064827596304010
L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein profile inference and applications to machine learning, J. Appl. Probab. 56(3):830–857, 2019. https://doi.org/10.1017/jpr.2019.49

5 thms2 active usersReviewed

Machine Learning Optimization·Captain: mikedeng1

Additive Logistic Regression: A Statistical View of Boosting 1: The Exponential Criterion E[e^{−yF(x)}] Is Minimized at Half the Log-Odds ½ log[P(y=1|x)/P(y=−1|x)]Research Paper

Motivation

AdaBoost (Freund and Schapire, 1996) combines many weak classifiers, such as small decision trees, into a single strong classifier by repeatedly reweighting the training data. In the late 1990s it was among the most accurate off-the-shelf classifiers, but why it worked was unclear. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) gave a statistical explanation: AdaBoost fits an additive model by stagewise minimization of the exponential criterion $E(e^{-yF(x)})$ , and the population minimizer of that criterion is half the log-odds of the class probability. Boosting is therefore a form of additive logistic regression. This reading underlies gradient boosting, LogitBoost, and the later theory of classification-calibrated surrogate losses.

The exponential criterion was introduced by Schapire and Singer (1998) as an upper bound on misclassification error, and Breiman (1997) used it in his analysis of AdaBoost. Lemma 1 of the 2000 paper is the statement that identifies its population minimizer.

Setting

A feature $x$ ranges over a measurable space $X$ and a label $y$ takes the values $-1$ and $1$ . The pair $(x, y)$ has a joint law $\nu$ , a probability measure on $X \times \{-1, 1\}$ , with marginal $\nu_X$ on $X$ . Disintegrating $\nu$ gives the conditional class probabilities $P(y = 1 \mid x)$ and $P(y = -1 \mid x)$ .

For a function $F : X \to \mathbb R$ the exponential criterion (11) is the joint expectation

J(F) = E\big(e^{-yF(x)}\big) = \int e^{-yF(x)}\, d\nu(x, y),

a number in $[0, \infty]$ . Its conditional version at $x$ is $E(e^{-yF(x)} \mid x)$ . Given a current estimate $F$ , the weighted conditional expectation with weight $w(x, y) = e^{-yF(x)}$ is

E_w[g(x, y) \mid x] = \frac{E[w(x, y)\, g(x, y) \mid x]}{E[w(x, y) \mid x]},

and $P_w(y = \pm 1 \mid x) = E_w[1_{[y = \pm 1]} \mid x]$ . The half log-odds is

F^\star(x) = \tfrac12 \log \frac{P(y = 1 \mid x)}{P(y = -1 \mid x)}.

Formalization targets

Goal: Lemma 1

Assume $0 < P(y = 1 \mid x) < 1$ for $\nu_X$ -almost every $x$ . Then $F^\star$ is measurable, and for every measurable $F : X \to \mathbb R$ ,

E\big(e^{-yF^\star(x)}\big) \le E\big(e^{-yF(x)}\big),

and, for $\nu_X$ -almost every $x$ , (13) and (14) hold:

P(y = 1 \mid x) = \frac{e^{F^\star(x)}}{e^{-F^\star(x)} + e^{F^\star(x)}}, \qquad P(y = -1 \mid x) = \frac{e^{-F^\star(x)}}{e^{-F^\star(x)} + e^{F^\star(x)}}.

Milestones

The conditional criterion (proof of Lemma 1): $E(e^{-yF(x)} \mid x) = P(y = 1 \mid x) e^{-F(x)} + P(y = -1 \mid x) e^{F(x)}$ , and $J(F)$ is the $\nu_X$ -average of the conditional criterion for measurable $F$ .
Its derivative in $F(x)$ : $-P(y = 1 \mid x) e^{-F(x)} + P(y = -1 \mid x) e^{F(x)}$ .
Corollary 3: at an optimal $F$ , the weighted conditional mean of $y$ vanishes, $E_w(y \mid x) = 0$ almost everywhere.
Result 2 with (23)–(24): for a measurable current estimate $F$ , the Real AdaBoost step $f(x) = \tfrac12 \log\big(P_w(y = 1 \mid x)/P_w(y = -1 \mid x)\big)$ minimizes $J(F + f)$ over measurable $f$ , and $F + f = F^\star$ almost everywhere.
Corollary 1: on a region where $F$ is a constant $c$ , the average of $e^{-y_i c}$ is minimized at $c = \tfrac12 \log(n_+/n_-)$ , and the sample proportions are the symmetric logistic transform of that $c$ .
Display (15): $e^{F}/(e^{-F} + e^{F}) = e^{2F}/(1 + e^{2F})$ , so the symmetric logistic transform of (13) is the usual logistic model with a factor $2$ .

Significance

Lemma 1 is what makes the rest of the paper a statement about logistic regression. Because the minimizer of $J$ is the half log-odds, an additive model $F = \sum_m f_m$ built by minimizing $J$ estimates $\tfrac12 \operatorname{logit} P(y = 1 \mid x)$ , and the transform (13) converts it into a class probability. Result 2 shows that one population step of Real AdaBoost from any starting point already reaches $F^\star$ , so the many iterations used in practice come from the crude approximation of conditional expectations by trees, not from the criterion. Corollary 3 gives the first-order condition used to interpret the AdaBoost weights. The other missions of this series (Discrete AdaBoost, LogitBoost, Gentle AdaBoost, multiclass LogitBoost) all rest on these population facts.

All of these results are proved in the paper; none is open. What this mission adds is a machine-checked version in the population setting, with conditional probabilities obtained from an honest disintegration of the joint law instead of being postulated. No formalization of the exponential criterion's population minimizer is known to exist on the platform or in Mathlib. The pointwise calculus is elementary; the work is in the measure-theoretic layer.

Difficulty

The paper's proof minimizes the conditional criterion pointwise and sets the derivative to zero. Turning this into a statement about $J$ requires three things the one-line proof does not mention. First, the joint expectation must be rewritten as an iterated integral, which needs the disintegration of $\nu$ and measurability of everything integrated. Second, the pointwise minimizer $F^\star$ must itself be a measurable function of $x$ , which the calculus says nothing about. Third, the comparison is against every measurable competitor, including those with $J(F) = \infty$ , so integrability cannot be assumed. Corollary 3 has a further difficulty: it assumes nothing about the class probabilities, so a proof must show that optimality of $F$ forces them strictly between $0$ and $1$ almost everywhere, a fact the paper's one-line proof does not address.

Formalization scope

Labels live on Bool, with sgn true = 1 and sgn false = -1. The joint law is ν : Measure (X × Bool) with [IsProbabilityMeasure ν] on an arbitrary measurable space X. $P(y = b \mid x)$ is (ν.condKernel x {b}).toReal, read off Mathlib's conditional kernel. It is determined only $\nu_X$ -almost everywhere, so (13), (14), Corollary 3 and the identity of Result 2 are almost-everywhere statements; the conditional formula and its derivative hold at every $x$ . $J$ is a lower Lebesgue integral in $[0, \infty]$ . Competitors range over all measurable functions $X \to \mathbb R$ . Derivatives are stated with HasDerivAt.

The hypothesis $0 < P(y = 1 \mid x) < 1$ almost everywhere is added to Lemma 1 and Result 2. Without it the ratio in (12) is $0$ or undefined, Real.log 0 = 0 would give a junk value, and no minimizer of $J$ exists. Corollary 1 assumes both labels occur in the region, which is the sample counterpart.

Several formalizations would make the targets trivial, and none is used here. Defining $J$ through its conditional formula would make milestone 1 a definition and the goal pointwise, so $J$ is the joint expectation under $\nu$ . A Bochner integral would return $0$ for a non-integrable $e^{-yF}$ and make every such $F$ a minimizer, so $J$ takes values in $[0, \infty]$ . A bare deriv is $0$ at points of non-differentiability. Writing the logistic transform as $1/(1 + e^{-F})$ in place of $e^{F}/(e^{-F} + e^{F})$ would lose the factor $2$ that (15) records.

A complete development needs the disintegration of a measure on $X \times \mathrm{Bool}$ , iterated lower integrals, measurability of the conditional kernel, and elementary calculus of $t \mapsto a e^{-t} + b e^{t}$ . Lemmas about conditional expectations against condKernel on a finite label set, and the measurability of $x \mapsto P(y = 1 \mid x)$ , are reusable in the other missions of this series. Contributions of either kind are welcome.

Selected references

J. Friedman, T. Hastie and R. Tibshirani, Additive logistic regression: a statistical view of boosting (with discussion), Annals of Statistics 28(2), 337–407, 2000. https://doi.org/10.1214/aos/1016218223
Y. Freund and R. E. Schapire, Experiments with a new boosting algorithm, Proceedings of ICML, 148–156, 1996. https://dl.acm.org/doi/10.5555/3091696.3091715
R. E. Schapire and Y. Singer, Improved boosting algorithms using confidence-rated predictions, Proceedings of COLT, 80–91, 1998; Machine Learning 37, 297–336, 1999. https://doi.org/10.1023/A:1007614523901
L. Breiman, Prediction games and arcing algorithms, Technical Report 504, Statistics Department, UC Berkeley, 1997; Neural Computation 11(7), 1493–1517, 1999. https://doi.org/10.1162/089976699300016106

8 thms2 active usersReviewed

Machine Learning Optimization·Captain: mikedeng1

Additive Logistic Regression: A Statistical View of Boosting 5: J-Class LogitBoost Is the Base-Class-Averaged Diagonal Quasi-Newton Step on the Multinomial Log-LikelihoodResearch Paper

Motivation

Boosting combines many weak classifiers into a strong one. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) explained the two-class AdaBoost algorithms statistically: in the population, boosting fits an additive logistic regression model by stagewise optimization of a criterion on the log-odds scale. Section 5 of that paper carries the explanation to $J>2$ classes. It answers two questions a practitioner faces when boosting a multiclass problem:

what the widely used AdaBoost.MH algorithm of Schapire and Singer (1998) actually estimates;
how to obtain a coupled multiclass procedure whose class probabilities sum to one.

The paper's answer to the second question is LogitBoost for $J$ classes (Algorithm 6). Result 6 asserts that it takes quasi-Newton steps on the multinomial log-likelihood. Algorithm 6 underlies later multiclass gradient boosting, where the per-class Newton step with a diagonal Hessian and the factor $(J-1)/J$ reappears (Friedman, Ann. Statist. 29 (2001)).

Setting

Fix $J\ge2$ classes, labelled $1,\dots,J$ , and a measurable space $X$ of features. A probability measure $\nu$ on $X\times\{1,\dots,J\}$ is the joint law of the feature $x$ and the class $y$ . The classes are mutually exclusive.

The indicator responses are $y^*_j = \mathbf 1_{[y=j]}$ , and the $\{-1,1\}$ responses are $y_j = 2y^*_j-1$ .
Conditional expectations $E(\cdot\mid x)$ are integrals against the conditional law $\nu(\cdot\mid x)$ of the class given $x$ .
The class probabilities are $p_j(x) = P(y_j=1\mid x)$ .

Definition 1 (p. 354) introduces the symmetric multiple logistic transformation

F_j(x) = \log p_j(x) - \frac1J\sum_{k=1}^J\log p_k(x),\tag{39}

and states that it is equivalent to

p_j(x) = \frac{e^{F_j(x)}}{\sum_{k=1}^J e^{F_k(x)}},\qquad \sum_{k=1}^J F_k(x) = 0.\tag{40}

For $J=2$ this is the two-class $F(x) = \frac12\log[p(x)/(1-p(x))]$ .

AdaBoost.MH (Algorithm 5) treats each class against the rest. Its population criterion is $\sum_{j=1}^J E\,e^{-y_jG_j(x)}$ .

LogitBoost ( $J$ classes) (Algorithm 6, population version) keeps a fit $F(x) = (F_1(x),\dots,F_J(x))$ and the probabilities $p_j(x)$ given by (40). For each class $j$ it forms the working response and weight

z_j = \frac{y^*_j-p_j(x)}{p_j(x)(1-p_j(x))},\qquad w_j = p_j(x)(1-p_j(x)).

It takes the weighted conditional mean $f_j(x) = E_{w_j}(z_j\mid x) = E(w_jz_j\mid x)/E(w_j\mid x)$ , and updates

F_j(x)\ \leftarrow\ F_j(x) + \frac{J-1}{J}\Big(f_j(x) - \frac1J\sum_{k=1}^Jf_k(x)\Big).

The multilogit parametrization with base class $b$ writes $G_j(x) = F_j(x)-F_b(x)$ , so that $G_b = 0$ . The multinomial log-likelihood of one observation is

l(G) = \sum_{j\ne b}y^*_jG_j - \log\Big(1+\sum_{k\ne b}e^{G_k}\Big).

Formalization targets

Goal: Result 6 (p. 356), as its Derivation (p. 357) makes precise

Result 6 states that the LogitBoost algorithm ( $J$ classes, population version) uses quasi-Newton steps for fitting an additive symmetric logistic model by maximum likelihood. The goal states, for every $x$ and every current fit $F$ , the three facts the Derivation makes precise:

For every base class $b$ and $j,k\ne b$ , the score and Hessian of $g\mapsto E(l(G+g)\mid x)$ at $g = 0$ are

s_j(x) = E\big(y^*_j-p_j(x)\mid x\big),\qquad H_{j,k}(x) = -p_j(x)\big(\delta_{jk}-p_k(x)\big).

The diagonal step $g^{(b)}_j = -H_{j,j}(x)^{-1}s_j(x)$ is well defined and equals $E(y^*_j-p_j(x)\mid x)/(p_j(x)(1-p_j(x)))$ .
The Algorithm 6 update is the average over all base classes of the symmetrized diagonal step:

F_j(x) + \frac{J-1}{J}\Big(f_j - \frac1J\sum_k f_k\Big) = F_j(x) + \frac1J\sum_{b=1}^J\Big(g^{(b)}_j - \frac1J\sum_{k=1}^J g^{(b)}_k\Big).

Milestones

Definition 1: the equivalence of (39) and (40), and the two-class case.
The multilogit coordinates with base class $b$ .
Derivation steps 1, 2 and 3 separately.
The population form of Algorithm 6's weighted least-squares fit.
For $J=2$ , Algorithm 6 reduces to two-class LogitBoost (Algorithm 3).
Result 5 (p. 355): population AdaBoost.MH fits $J$ uncoupled models

G_j(x) = \tfrac12\log\frac{p_j(x)}{1-p_j(x)},

each minimizing the class- $j$ -against-the-rest exponential criterion.

Significance

The result places J-class LogitBoost inside likelihood theory. Its population step is a Newton-type step for multinomial maximum likelihood. Two approximations separate it from the full Newton step: the Hessian is replaced by its diagonal, and the base class is averaged out. Result 5 shows that AdaBoost.MH, in contrast, solves $J$ decoupled one-against-the-rest problems whose implied probabilities need not sum to one. That contrast is the paper's argument for the coupled procedure.

All statements here are proved in the paper by direct calculation. They have not been formalized before. The mission produces machine-checked versions of the population claims and of the algebra behind them. That algebra comprises the softmax/centred-logit equivalence, the multinomial score and Hessian in base-class coordinates, and the base-class averaging identity. These pieces are reusable for any multinomial logistic or softmax model.

Difficulty

There is no deep step. The work lies in keeping two parametrizations apart: the base-class multilogit coordinates $G$ , with $J-1$ free entries, and the symmetric centred coordinates $F$ , with $J$ entries summing to zero. The derivatives are taken in $G$ . The algorithm and (40) live in $F$ . The step is converted back by symmetrization. Mixing the two makes the averaging identity false or vacuous.

A second point is that the update is not the Newton step $-H^{-1}s$ . The page states this explicitly: for full Newton stepping the symmetrization would be redundant. The tempting shortcut of proving that Algorithm 6 equals the full Newton step therefore does not prove Result 6.

Formalization scope

Classes are Fin J, with $J\ge2$ where needed.
$\nu$ is a probability measure on $X\times$ Fin J.
Conditional expectations given $x$ are integrals against Mathlib's ν.condKernel x.
The constants $1/J$ and $(J-1)/J$ are real numbers.
Every statement about Result 6 is conditional on a fixed $x$ and holds for every $x$ , with no integrability or positivity hypothesis on the true class probabilities.
The model probabilities (40) lie strictly in $(0,1)$ when $J\ge2$ , so $p_j(1-p_j)\ne0$ is proved, not assumed.
The page fixes the base class $J$ . Here the base class is a parameter $b$ , as the averaging in step 3 requires.
The AdaBoost.MH criteria are lower Lebesgue integrals in $[0,\infty]$ .
Result 5 adds the hypothesis $0<p_j(x)<1$ for almost every $x$ , because the log-odds is undefined at $0$ and $1$ .
Definition 1 is stated for positive probability vectors.

Trivializing encodings are ruled out:

Derivatives are stated with HasDerivAt along coordinate lines, and the Hessian is the derivative of an explicitly given partial derivative, never a deriv equation that would be a junk $0$ at non-differentiable points.
The conditional expectations $E(y^*_j\mid x)$ are integrals against the conditional law of the joint $\nu$ , not a free vector.
The exponential criteria are never Bochner integrals, which would return $0$ on non-integrable integrands.
(40) is the softmax of the centred scores itself.

All objects are defined in one definitions file in the namespace AddLogReg.Multiclass. Proofs of any of the milestones are welcome. Lemmas on the softmax map, such as positivity, the derivative of log-sum-exp in base coordinates and shift invariance, are reusable beyond this mission.

Selected references

J. Friedman, T. Hastie, R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2) (2000) 337–407. https://doi.org/10.1214/aos/1016218223
R. E. Schapire, Y. Singer, Improved boosting algorithms using confidence-rated predictions, Machine Learning 37 (1999) 297–336 (COLT 1998). https://doi.org/10.1023/A:1007614523901
J. Friedman, Greedy function approximation: a gradient boosting machine, Ann. Statist. 29(5) (2001) 1189–1232. https://doi.org/10.1214/aos/1013203451

11 thms2 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

Fast Rates for Support Vector Machines Using Gaussian Kernels 1: Under Tsybakov and Geometric Noise, Gaussian-Kernel SVMs Reach Excess Risk Cx²n^{−β+ε} with Probability 1 − e^{−x}Research Paper

Motivation

Support vector machines classify observations by choosing a real-valued function from a reproducing kernel Hilbert space and using its sign as the predicted label. The Gaussian kernel is widely used because it gives a flexible class of functions, but that flexibility alone does not explain how quickly classification error approaches the best possible error as the training sample grows. Steinwart and Scovel's 2007 paper identifies distributional conditions under which a Gaussian-kernel SVM achieves a polynomial, and sometimes nearly linear, excess-risk rate. The conditions describe both ambiguity in the labels and the location of data relative to the decision boundary.

The article's result is already proved mathematically. This mission asks for machine-checked statements and proofs of its finite-geometric-exponent, no-offset rate and selected supporting results. It uses arXiv:0708.1838v1, the electronic reprint of the Annals of Statistics article. Its printed page number equals its PDF page number throughout; all page references below use those numbers.

Setting

Let $X$ be the closed unit ball of $\mathbb R^d$ , where $d>0$ , and let the label set be $Y=\{-1,1\}$ . A distribution $P$ on $X\times Y$ has input marginal $\mu=P_X$ and a measurable regression function $\eta(x)=P(y=1\mid x)$ . In the Lean representation, $\mu$ and one version of $\eta$ are carried explicitly; the joint law gives conditional masses $\eta(x)$ and $1-\eta(x)$ to the two labels. Classification predicts $\operatorname{sign}f(x)$ , with $\operatorname{sign}(0)=1$ . Write $R_P(f)$ for its error probability and $R_P$ for the smallest such risk over measurable decision functions.

The hinge loss is $\ell(y,t)=\max\{0,1-yt\}$ . The Gaussian kernel with parameter $\sigma>0$ is $k_\sigma(x,x')=\exp(-\sigma^2\|x-x'\|^2)$ , and $H_\sigma(X)$ is its restricted RKHS. Given a sample $T$ of size $n$ , an SVM without offset minimizes $\lambda\|f\|^2_{H_\sigma(X)}+R_{\ell,T}(f)$ over that space. The approximation error $a_\sigma(\lambda)$ is the infimum of the corresponding population objective minus the unrestricted Bayes hinge risk; equation (6) uses that unrestricted baseline.

Two assumptions describe the distribution. It has Tsybakov noise exponent $q\in[0,\infty]$ if, for sufficiently small $t>0$ , $\mu\{|2\eta-1|\le t\}\le C t^q$ for some $C>0$ . To define geometric noise exponent $\alpha>0$ , partition $X$ according to whether $\eta$ is below, above, or equal to $1/2$ . The distance $\tau_x$ goes from a point in either strict class to the opposite strict class together with the equal-probability class. The geometric condition is

\int_X |2\eta(x)-1|\exp(-\tau_x^2/t)\,d\mu(x) \le C t^{\alpha d/2}\qquad(t>0).

These are Definitions 2.2 and 2.3 and equation (7) of the paper.

Formalization targets

The goal is the finite- $\alpha$ , no-offset clause of Theorem 2.8. With the paper's two-case exponent $\beta=\beta(\alpha,q)$ , set $\lambda_n=n^{-(\alpha+1)\beta/\alpha}$ and $\sigma_n=n^{\beta/(\alpha d)}$ . For every $\varepsilon>0$ , one constant $C>0$ works uniformly for $x\ge1$ and $n\ge1$ :

\Pr^*\!\left\{T:R_P(f_{T,\lambda_n}) \le R_P+C x^2n^{-\beta+\varepsilon}\right\}\ge1-e^{-x}.

Here $\Pr^*$ is outer probability, and the statement applies to every empirical minimizer. The formula for $\beta$ is $\alpha/(2\alpha+1)$ in the first case, $\alpha\le(q+2)/(2q)$ , and $2\alpha(q+1)/(2\alpha(q+2)+3q+4)$ otherwise; the paper's limiting convention specifies $q=\infty$ .

Three milestones record results used on this path. Theorem 2.1 bounds empirical covering numbers of Gaussian RKHS balls, uniformly in $\sigma$ and the sample. Lemma 4.1 locates balls of radius $\tau_x$ inside the corresponding enlarged decision class. Theorem 2.7 bounds the approximation error by

a_\sigma(\lambda)\le c_d\bigl(\sigma^d\lambda+C(2d)^{\alpha d/2}\sigma^{-\alpha d}\bigr),

where $c_d$ depends only on dimension. Their exact source text and page positions appear in the milestone list.

Significance

Theorem 2.8 gives a quantitative guarantee for classification risk, rather than only convergence of the regularized hinge objective. The rate responds to both the label-noise exponent and the concentration of input mass near the decision boundary. In the regimes discussed after the theorem, the exponent can approach one; the paper's Remark 2.9 compares it with the $n^{-1/2}$ benchmark.

Formalizing this result adds a concrete Gaussian RKHS norm compatible with a kernel parameter that changes with $n$ , an explicit binary-law model, extended-valued risks and covering numbers, and source-indexed bounds on approximation and complexity. Those objects can be reused in later SVM and kernel-learning statements. The paper's argument is a published proof; the Lean theorem files here are open proof obligations, while the definition files have compiled bodies. No claim of a machine-checked proof of the rate is made.

Difficulty

It is not enough to combine a general consistency theorem with the noise assumptions. The kernel parameter grows with sample size, so the relevant hypothesis class changes with $n$ ; a complexity estimate for one fixed class gives no uniform rate. Geometric noise controls approximation error, while Tsybakov noise controls a different fluctuation quantity, and neither by itself supplies the stated exponent. The probability statement also concerns an event defined by empirical minimizers, whose measurability the source deliberately avoids by using outer probability. These are the points at which a direct fixed-class or ordinary-probability statement would fail to match Theorem 2.8.

Formalization scope

Lean represents functions on all of $\mathbb R^d$ but uses only their restrictions to $X$ . The joint distribution is built from a probability marginal and a fixed measurable $\eta:\mathbb R^d\to[0,1]$ . This makes the paper's choice of regression-function version explicit. The Gaussian RKHS squared norm is the supremum over finite normalized kernel-section combinations; it is $+\infty$ outside the RKHS. A covering number is the least positive finite cardinality of a cover with centers in the ambient empirical function space, or $+\infty$ if there is no such cover. Hinge and classification risks are extended nonnegative integrals, and Bayes risks range over measurable functions.

The assumptions $d>0$ and $n\ge1$ give the divisions and powers their intended domains. For $q=\infty$ , the small- $t$ noise bound uses zero on the right, as in the source convention. The paper leaves distance to an empty set unstated; this mission pins $d(x,\varnothing)=0$ . With the infinite-distance convention, Lemma 4.1 and Theorem 2.7 fail for a one-class regression function. The proof display (25) has a volume-factor slip in high dimension; Theorem 2.7 is stated with its printed conclusion, and the issue is recorded in the moderation notes. The goal event includes existence of an empirical minimizer, a fact stated in the paper's setup, and quantifies over every minimizer. This excludes a vacuous SVM predicate. The constant $C$ is chosen before $x$ and $n$ .

The clauses for $\alpha=\infty$ and an SVM with offset are outside this mission. The separate series mission addresses the implication from an envelope assumption to geometric noise. Further contributions toward the §5 empirical-process estimates, §6 variance estimates, and §7 shrinking and general-rate theorems are welcome; they are not asserted as milestones in this draft.

Selected references

Ingo Steinwart and Clint Scovel, Fast Rates for Support Vector Machines Using Gaussian Kernels, Annals of Statistics 35(2), 2007, 575–607. arXiv:0708.1838v1, DOI:10.1214/009053606000001226.

11 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

On Tail Probabilities for Martingales 2: For |X_n| ≤ 1 and E{X_n | ℱ_{n−1}} = 0, the Conditional Variance W_a Used to Cross a Satisfies E exp[−f(λ)W_a] ≥ exp[−λ(a+1)]Research Paper

Motivation

Exponential tail bounds for sums of bounded martingale differences (Bernstein, Bennett, Hoeffding, Freedman) are the workhorses of probability, statistics and learning theory. They bound how far a martingale can travel in a given amount of conditional variance. The converse question is just as basic: how much conditional variance does a martingale need before it reaches a given level? An answer controls the time a martingale spends below a barrier, and it is the ingredient that turns the upper half of a law of the iterated logarithm into the lower half.

David A. Freedman's paper On Tail Probabilities for Martingales (Ann. Probab. 3 (1975) 100–118) derives both kinds of result from a single observation: the exponential process $Q_\lambda(T_n, S_n)$ is a supermartingale and $R_\lambda(T_n, S_n)$ a submartingale. The first gives the inequality now called Freedman's inequality (Theorem (1.6)/(4.1)); the second gives Theorem (1.8), the subject of this mission, a lower bound on the Laplace transform of the conditional variance accumulated up to the first crossing of a level. From (1.8) the paper derives Corollary (1.9), the tail bound $P\{W_a \ge b\} < 5(a+1)/b^{1/2}$ , Lévy's theorem that $\sup_n S_n = \infty$ almost surely on $\{\sum V_i = \infty\}$ (Corollary (4.5)), and, through a separate analytic argument, the lower-tail bound (1.10).

Setting

Let $(\Omega, \mathcal F, P)$ be a probability space and $\mathcal F_0 \subset \mathcal F_1 \subset \cdots$ an increasing sequence of sub- $\sigma$ -fields of $\mathcal F$ . Let $X_1, X_2, \dots$ be real random variables with $X_n$ measurable with respect to $\mathcal F_n$ , satisfying the standing condition (1.1):

|X_n| \le 1 \quad\text{and}\quad E\{X_n \mid \mathcal F_{n-1}\} = 0 \qquad (n \ge 1).

The conditional variance of the $n$ -th step is $V_n = \operatorname{Var}\{X_n \mid \mathcal F_{n-1}\}$ . The partial sums are $S_n = X_1 + \cdots + X_n$ and the intrinsic time is $T_n = V_1 + \cdots + V_n$ , with $S_0 = T_0 = 0$ .

For a real $\lambda$ , let $f(\lambda) = e^{-\lambda} - 1 + \lambda$ (positive for $\lambda > 0$ ), and $R_\lambda(v, y) = \exp\{\lambda y - f(\lambda) v\}$ .

A stopping time is a random variable $\sigma$ with values in $\{0, 1, 2, \dots, \infty\}$ such that $\{\sigma = n\} \in \mathcal F_n$ for every $n$ ; it is uniformly bounded if $\sigma \le N$ everywhere for some integer $N$ .

Fix a level $a > 0$ . The crossing time $\tau_a$ is the least $n$ with $S_n \ge a$ , and $\tau_a = \infty$ if there is none. The crossing variance is

W_a = T_{\tau_a} = \sum_{i=1}^{\tau_a} V_i \in [0, \infty],

the total conditional variance the process needs to cross the level $a$ if it crosses, and otherwise the total conditional variance $\sum_{i \ge 1} V_i$ , which may be infinite.

Formalization targets

Goal: Theorem (1.8)

For every $\lambda > 0$ and $a > 0$ ,

E\{\exp[-f(\lambda) W_a]\} \ge \exp[-\lambda(a+1)],

with the convention $\exp[-f(\lambda)\cdot\infty] = 0$ .

Milestones

The two-point cases of (3.7): for $X$ taking only the values $-1$ and $a > 0$ (Case 1), or only $-b$ and $a$ with $0 < b \le 1$ (Case 2), with $E(X) = 0$ and $\lambda \ge 0$ ,

E\{\exp(\lambda X)\} \ge \exp\{f(\lambda) \operatorname{Var} X\}.

Inequality (3.7): the same bound for every random variable $X \ge -1$ with $E(X) = 0$ .
Proposition (3.6): under (1.1), $E\{R_\lambda(T_\sigma, S_\sigma)\} \ge 1$ for every $\lambda \ge 0$ and every uniformly bounded stopping time $\sigma$ .
From (4.2): $S_n \le a + 1$ for $n \le \tau_a$ , and for every $n$ ,

1 \le E\{\exp[\lambda S_{\tau_a\wedge n} - f(\lambda)T_{\tau_a\wedge n}]\} \le \exp[\lambda(a+1)]\cdot E\{\exp[-f(\lambda)T_{\tau_a\wedge n}]\}.

Significance

The result. Theorem (1.8) says that the Laplace transform of $W_a$ cannot be small, so $W_a$ cannot be large: a bounded martingale difference sequence crosses any level after a finite amount of conditional variance with high probability. The paper turns this into the explicit tail estimate (1.9), into Lévy's theorem that a bounded martingale with divergent conditional variance is almost surely unbounded above and below, and, combined with the upper bound (4.8) on the same Laplace transform, into the lower-tail estimate (1.10) that gives the lower half of the law of the iterated logarithm for martingales in intrinsic time. Example (4.3) of the paper shows the theorem fails when the increments are only bounded below, so the two-sided bound in (1.1) is needed.

Formalizing it. The result is classical and proved in the paper; to the best of current knowledge it has no machine-checked proof. Mathlib has conditional variance, stopping times and optional stopping for bounded stopping times, but no reverse moment-generating-function inequality such as (3.7), no submartingale property for exponential processes in intrinsic time, and no crossing-time variables valued in $[0,\infty]$ . The mission produces these, with the conventions at infinity made explicit, as a base for the remaining results of the paper (Corollary (1.9), Corollary (4.5), the lower-tail bound (1.10)).

Difficulty

The obvious route is optional stopping at $\tau_a$ itself. It fails: $\tau_a$ is unbounded and may be infinite with positive probability, and Proposition (3.6) holds only for uniformly bounded stopping times. The argument must stop at $\tau_a \wedge n$ , use the overshoot bound $S_{\tau_a \wedge n} \le a + 1$ (which relies on $X_n \le 1$ ), and pass to the limit $n \to \infty$ in a way that sends the integrand to $0$ on $\{W_a = \infty\}$ ; the limit exchange needs $T_n \to W_a$ in $[0, \infty]$ and $f(\lambda) > 0$ . A second obstacle is the one-step inequality (3.7): it is a lower bound on a moment-generating function, valid for random variables bounded only from below, where $E\exp(\lambda X)$ may be infinite; the usual convexity bounds go in the opposite direction.

Formalization scope

The source is the published Annals of Probability article (a scanned copy); all page numbers are the journal's.

Conventions. Increments are a sequence X : ℕ → Ω → ℝ used from index $1$ ; $X_0$ is never read. Measurability is " $X_n$ is $\mathcal F_n$ -strongly measurable for $n \ge 1$ ", and the two parts of (1.1) are assumed almost surely. $V_n$ is Mathlib's condVar of $X_n$ given $\mathcal F_{n-1}$ ; under (1.1) every $X_n$ is square-integrable, so this is a genuine conditional variance and no square-integrability hypothesis is added to the martingale statements. Stopping times are Ω → WithTop ℕ (⊤ is $\infty$ ). $\tau_a$ is WithTop ℕ-valued and $W_a$ is $[0,\infty]$ -valued (ℝ≥0∞), built from the nonnegative parts of the $V_i$ , which agree with $V_i$ almost surely. The integrand of the goal is the function that equals $e^{-f(\lambda) W_a}$ on $\{W_a < \infty\}$ and $0$ on $\{W_a = \infty\}$ ; replacing it by $\exp(-f(\lambda)\cdot\mathrm{toReal}(W_a))$ , which is $1$ on $\{W_a = \infty\}$ , would formalize a strictly weaker statement and is ruled out. In (3.7), where $\exp(\lambda X)$ need not be integrable, the expectation is a lower Lebesgue integral in $[0,\infty]$ , and $X$ is assumed square-integrable so that $\operatorname{Var} X$ is finite.

Corrected misprints. Definition (1.2)(e) prints $R_\lambda(v,y) = \exp\{\lambda h - f(\lambda) v\}$ ; $h$ is read as $y$ . The display in (4.2) prints the last factor without its expectation sign; the $E$ is restored.

Ranges. The goal uses $\lambda > 0$ and $a > 0$ as in (1.2) and (1.7); (3.6), (3.7) and its two cases are stated for $\lambda \ge 0$ as on p. 107.

Lemma (3.1) ( $g(x) = (e^x - 1 - x)/x^2$ is increasing), used in Case 2, is posed in the companion mission on Freedman's inequality and not here. Contributions welcome: proofs of the milestones, a general lemma that $R_\lambda(T_n, S_n)$ is a submartingale, and Corollary (1.9) as a follow-up.

Selected references

David A. Freedman, On Tail Probabilities for Martingales, The Annals of Probability 3(1), 1975, 100–118. https://doi.org/10.1214/aop/1176996452
Paul Lévy, Théorie de l'addition des variables aléatoires, Gauthier-Villars, 1937 (Theorem 68, p. 247, cited in (4.5)).

10 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Residual Life Time at Great Age 6: For 0 < ξ < α, Residual Life Attraction to Γ_α Is Equivalent to a Finite ξ-th Moment and E((X/t)^ξ | X > t) → (1 − ξ/α)^{−1}Research Paper

Motivation

Actuaries, reliability engineers and demographers ask how much longer an item or a person will live given that it has already survived to a great age $t$ . For a lifetime $X$ with distribution function $F$ , this is the law of the residual life time $X - t$ given $X > t$ , and the question is what this law looks like as $t \to \infty$ . Balkema and de Haan (Ann. Probab. 2 (1974) 792–804) determined all possible limit laws of the suitably normed residual life time and the distribution functions attracted to each. When only a scale normalization is allowed, the possible continuous limits are the exponential law and the Pareto-type laws $\Gamma_\alpha$ , the counterparts in residual-life theory of the Gumbel and Fréchet laws of extreme value theory. Both theories rest on Karamata's theory of regular variation (de Haan 1970).

Section 5 of the paper restates the domain of attraction of $\Gamma_\alpha$ in terms of moments: weak convergence of the scaled residual life times is equivalent to convergence of a single conditional moment of the scaled residual life. For an exponential limit the analogous link between weak convergence and first moments had been studied by Meilijson (1972). Moment conditions of this form underlie the mean-excess and Hill-type diagnostics used in heavy-tail statistics and in the peaks-over-threshold method (Pickands 1975).

Setting

Let $X$ be a real random variable with law $\mu$ and distribution function $F$ , and write $R(x) = 1 - F(x) = P\{X > x\}$ for its tail. The standing assumption is $F(x) < 1$ for every real $x$ , i.e. $R(x) > 0$ : $X$ has no finite upper endpoint, and conditioning on $\{X > t\}$ makes sense for every $t$ .

For $t > 0$ , the conditional distribution function of $X/t$ given $X > t$ is

P\Big\{\frac{X}{t} \le x \,\Big|\, X > t\Big\} = \frac{P\{t < X \le xt\}}{P\{X > t\}},

which vanishes for $x \le 1$ . For a real exponent $\xi$ , the conditional $\xi$ -th moment is

E\Big(\Big(\frac{X}{t}\Big)^{\xi}\,\Big|\,X > t\Big) = \frac{1}{P\{X>t\}}\int_{(t,\infty)} \Big(\frac{y}{t}\Big)^{\xi} dF(y).

For $\alpha > 0$ the limit law $\Gamma_\alpha$ is $\Gamma_\alpha(x) = 1 - (1+x)^{-\alpha}$ for $x \ge 0$ and $\Gamma_\alpha(x) = 0$ for $x < 0$ . The shifted function $\Gamma_\alpha(x-1)$ equals $1 - x^{-\alpha}$ for $x \ge 1$ : the Pareto law of index $\alpha$ on $[1,\infty)$ . The distribution function $F$ is in the domain of residual life time attraction $D_r(\Gamma_\alpha)$ when

\lim_{t\to\infty} P\Big\{\frac{X}{t} \le x \,\Big|\, X > t\Big\} = \Gamma_\alpha(x-1) \qquad \text{for all } x > 0 .

In Lean the tail is BalkemaDeHaan.LimitTypes.tail; the scaled conditional distribution and moment are BalkemaDeHaan.Moments.scaledResidualCDF and BalkemaDeHaan.Moments.condMoment. The limit law is BalkemaDeHaan.ParetoBounds.GammaLaw.

Formalization targets

Goal: Theorem 8(a), corrected

For $F(x) < 1$ for all $x$ and $0 < \xi < \alpha$ :

F \in D_r(\Gamma_\alpha) \iff \int_0^\infty y^\xi\, dF(y) < \infty \ \text{ and } \ \lim_{t\to\infty} E\Big(\Big(\frac{X}{t}\Big)^{\xi}\,\Big|\,X > t\Big) = \Big(1 - \frac{\xi}{\alpha}\Big)^{-1}.

Milestones

The identity in the proof of Theorem 8(a): for $x > 0$ , with a finite $\xi$ -th moment,

\frac{\int_x^\infty y^\xi dF(y)}{x^\xi(1-F(x))} = \xi\,\frac{\int_x^\infty y^{\xi-1}(1-F(y))\,dy}{x^\xi(1-F(x))} + 1,

the left side being $E((X/x)^\xi \mid X > x)$ . 2. The value of the limit: $\int_0^\infty x^\xi\, d\Gamma_\alpha(x-1) = (1-\xi/\alpha)^{-1}$ for $0 < \xi < \alpha$ . 3. The "only if" half: $F \in D_r(\Gamma_\alpha)$ implies a finite $\xi$ -th moment and convergence of the conditional moment to $(1-\xi/\alpha)^{-1}$ . 4. The "if" half, corrected: the converse.

Significance

The theorem replaces a distributional limit, required at every $x > 0$ , by one numerical limit, for any order $\xi \in (0,\alpha)$ . In statistics this justifies testing or estimating heavy-tail behaviour through empirical conditional moments above a high threshold, and it identifies the limit value $(1-\xi/\alpha)^{-1}$ , from which $\alpha$ can be read off. Combined with Theorem 4 of the same paper ( $D_r(\Gamma_\alpha) = D(\Phi_\alpha)$ ), it gives a moment criterion for the Fréchet domain of attraction of extreme value theory.

The result is classical and proved, by reduction to Karamata's theorem on integrals of regularly varying functions. No machine-checked proof is known. Mathlib has no theory of regular variation, no Karamata theorem and no domains of attraction, so a formal proof also produces a reusable piece of the theory of regularly varying tails: the direct and converse halves of Karamata's integral theorem for tails of probability laws.

Difficulty

Both directions pass through the asymptotics of $\int_x^\infty y^{\xi-1}R(y)\,dy$ against $x^\xi R(x)$ . The direct half requires uniform control of $R(tx)/R(t)$ over $x \in (1,\infty)$ to exchange the limit $t\to\infty$ with an integral over an unbounded range; pointwise convergence of the tail ratio alone does not dominate the integrand. The converse half must recover regular variation of $R$ from the behaviour of a single integral functional, and here the limit value matters: the page's hypothesis that the limit merely exists does not identify $\alpha$ (see below), so an argument that never uses the value $(1-\xi/\alpha)^{-1}$ cannot succeed.

Formalization scope

The law of $X$ is μ : Measure ℝ with IsProbabilityMeasure μ; $F(x) < 1$ for all $x$ is ∀ x, 0 < μ (Set.Ioi x). All conditional quantities divide by μ (Set.Ioi t), which this hypothesis keeps nonzero.
" $\int_0^\infty y^\xi dF(y)$ is finite" is IntegrableOn (fun y => y ^ ξ) (Set.Ioi 0) μ (real power on positive bases). In the "only if" half it is part of the conclusion, never an assumption; Lean's value $0$ for a non-integrable Bochner integral therefore cannot make the statements hold trivially. Milestone 1 asserts integrability of $y^{\xi-1}R(y)$ on $(x,\infty)$ as well.
" $\lim_{t\to\infty}$ " is Tendsto … atTop along real $t$ ; the limit form of $D_r(\Gamma_\alpha)$ is required for every $x > 0$ , as printed (the limit $\Gamma_\alpha(x-1)$ is continuous, so this is weak convergence). The goal uses this explicit form, the one given after "i.e." on the page, not a separate definition of $D_r$ .
$\int_0^\infty x^\xi d\Gamma_\alpha(x-1)$ is the integral against a probability measure whose distribution function (ProbabilityTheory.cdf) is $x \mapsto \Gamma_\alpha(x-1)$ ; milestone 2 asserts such a measure exists and computes the moment for every such measure.
Corrected statement. The source is the published article (Annals of Probability, DOI 10.1214/aop/1176996548). As printed, the "if" direction asks only that $c = \lim E((X/t)^\xi \mid X>t)$ exist and be finite. That is false: the tail $R(x) = x^{-\beta}$ for $x \ge 1$ , with $\beta > \xi$ and $\beta \ne \alpha$ , has a finite $\xi$ -th moment and $E((X/t)^\xi\mid X > t) = (1-\xi/\beta)^{-1}$ for all $t \ge 1$ , but its limit law is $\Gamma_\beta(x-1)$ . The goal and milestone 4 require $c = (1-\xi/\alpha)^{-1}$ , the value the page itself states in "Then $c = (1-\xi/\alpha)^{-1}$ ". The "only if" direction is exactly the page's.
No hypothesis beyond the page is added; $\alpha > 0$ follows from $0 < \xi < \alpha$ .

A complete development needs regularly varying functions, uniform convergence (or Potter bounds) for regularly varying tails, and Karamata's integral theorem with its converse; all are reusable beyond this mission. Proofs of the milestones, of these general tools, and of the Pareto moment computation are welcome.

Selected references

A. A. Balkema and L. de Haan, Residual life time at great age, Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970 (Theorem 1.2.1 and Remark 1.2.1).
N. H. Bingham, C. M. Goldie and J. L. Teugels, Regular Variation, Cambridge University Press, 1987. https://doi.org/10.1017/CBO9780511721434
I. Meilijson, Limiting properties of the mean residual lifetime function, Annals of Mathematical Statistics 43 (1972), 354–357. https://doi.org/10.1214/aoms/1177692729
J. Pickands III, Statistical inference using extreme order statistics, Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003

8 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Residual Life Time at Great Age 2: The Domain of Residual Life Time Attraction of the Exponential Law Is D(Λ) ∩ D₀Research Paper

Motivation

A lifetime observed only after it has survived to a high age is described by its residual life: the additional time until failure, conditional on survival so far. Reliability analysis asks whether these conditional distributions settle into a stable shape after scaling and shifting. Extreme-value theory asks a related question about the largest observation in a large independent sample. Balkema and de Haan identify an exact connection between these questions for the exponential residual-life limit and the Gumbel maxima limit in Theorem 3 of their 1974 article. The connection lets one recognize the asymptotic form of old-age lifetimes from the domain of attraction of sample maxima, provided the lifetime distribution has no finite upper endpoint.

The article studies several residual-life limits. This mission isolates its exponential case, where the limiting conditional excess has distribution function $\Pi(x)=1-e^{-x}$ for $x\ge0$ . The other continuous family $\Gamma_\alpha$ and the paper's discrete limits have separate hypotheses and attraction domains; they are outside this theorem.

Setting

Let $X$ have a probability distribution function $F$ on $\mathbb R$ , and let its survival function be $R(x)=\Pr(X>x)=1-F(x)$ . For a threshold $t$ with $R(t)>0$ , the residual-life distribution function is

F_t(x)=\Pr(X-t\le x\mid X>t)=\frac{\Pr(t<X\le t+x)}{R(t)}.

It is zero for $x<0$ . The class $D_0$ consists of the distributions with $R(x)>0$ for every real $x$ . This says that the upper endpoint is infinite and makes $F_t$ meaningful at every threshold.

A law $F$ belongs to the domain of residual-life attraction $D_r(G)$ when $F\in D_0$ and there are a positive scale $a(t)$ and a shift $b(t)$ such that $F_t(b(t)+xa(t))$ converges weakly to $G(x)$ as $t\to\infty$ . The shift here acts on $X-t$ , the residual lifetime. Weak convergence means convergence at every continuity point of the limiting distribution function; it does not require convergence at a jump.

For maxima, $F$ belongs to the domain of attraction $D(G)$ if there are sequences $a_n>0$ and $b_n$ for which $F(a_nx+b_n)^n$ converges weakly to $G(x)$ as $n\to\infty$ . The power is the distribution function of the maximum of $n$ independent observations after the indicated normalization. The relevant limit laws are the exponential residual-life law and the Gumbel law:

\Pi(x)=\begin{cases}0,&x<0,\\1-e^{-x},&x\ge0,\end{cases}\qquad \Lambda(x)=e^{-e^{-x}}\quad(x\in\mathbb R).

These definitions and formulas come from the introduction and §2 of the published article, printed pages 792–793 and 798.

Formalization targets

Theorem 3: the exact domain identity

The goal is the identity stated on printed page 798:

D_r(\Pi)=D(\Lambda)\cap D_0.

Both inclusions are required. In particular, membership in the maxima domain alone is insufficient: the maximum of a sample can have a Gumbel limit even when the underlying distribution has a finite upper endpoint, while residual life cannot be conditioned on survival beyond that endpoint. The $D_0$ condition is therefore part of the mathematical claim.

Supporting targets

The milestone list follows the statements used in the article's treatment of Theorem 3: the convergence-of-types remark on page 795; Lemma 3's asymptotic ratio $R(x-0)/R(x+0)\to1$ ; the tail criterion $nR(b_n+xa_n)\to e^{-x}$ associated with Gumbel attraction; the inclusion $D(\Lambda)\cap D_0\subseteq D_r(\Pi)$ ; and the passage from this tail limit on $x>0$ to all $x\in\mathbb R$ . The last step retains the same normalization sequences. The article presents the criterion in one direction and relies on its converse at the end; the formal milestone records both directions with the same sequences.

Significance

The identity translates a conditional limit at a moving high threshold into a classical maxima-domain statement. A theorem about sample extremes can therefore characterize whether normalized remaining lifetime is asymptotically exponential. Conversely, observing exponential residual-life attraction determines a Gumbel maxima limit once the tail normalization is extended across the real line. The condition $D_0$ marks exactly where the conditional lifetime exists; omitting it would misstate the equivalence.

The article proves the result mathematically. The Lean targets here provide a precise representation of its distributions, normalizations, and limiting claims, with Theorem 3 still posed for formal proof. A complete development would add proofs of the supporting tail and convergence-of-types statements, then establish both inclusions. The definitions of weak convergence at continuity points, survival functions, and attraction domains can also support later formalizations of the paper's Pareto and discrete cases.

Difficulty

The simple comparison $F(a_nx+b_n)^n\approx e^{-nR(a_nx+b_n)}$ only relates the two limits after a suitable normalization is already available. The reverse direction starts with conditional residual-life convergence indexed by real thresholds, whereas maxima attraction needs a sequence indexed by integers. Sampling thresholds must preserve the tail asymptotics despite possible atoms. More seriously, the residual-life statement initially yields the required scaled-tail convergence only for positive arguments. The maxima limit must hold on the whole real line. A proof confined to that half-line cannot establish $D(\Lambda)$ ; the continuation across its left boundary is the central difficulty highlighted by the article on printed pages 798–799.

Formalization scope

Lean represents $F$ as the cumulative distribution function of a probability measure on $\mathbb R$ and uses real-valued probabilities of intervals for $R$ and $F_t$ . The residual-life denominator is positive wherever $D_r$ is asserted. The extrema normalization is indexed by natural numbers, while the residual-life normalization is indexed by real thresholds. The scale is positive at every index; only large indices affect the limit. Weak convergence is encoded at every continuity point of the limit. As $\Pi$ and $\Lambda$ are continuous, their particular domain conditions amount to convergence at every real argument.

The paper uses two shift conventions: $F_t(b(t)+xa(t))$ shifts $X-t$ , while the scaled-tail expressions $R(b_n+xa_n)$ shift $X$ . Each statement uses the convention of its source passage. The convergence-of-types remark makes explicit the antitonicity and right-continuity of its limiting tails and states its identity where both arguments lie in the half-line on which convergence is known. Gnedenko's criterion is formalized as an equivalence: the printed sentence states the forward implication, and the conclusion of Theorem 3 uses the converse. The page-799 expression $R(b(t)+xa(t))/(t)$ has a missing $R$ in the denominator; the formal statement uses the intended $R(t)$ , consistent with conditional probability and with equation (11). These choices prevent a zero-denominator quotient or an out-of-domain limit identity from trivializing a target. In particular, $D_0$ is part of the definition of $D_r(G)$ : without it a law with a finite upper endpoint would have $R(t)=0$ for large $t$ , the conditional distribution would be the junk quotient $0/0=0$ , and the domain would be mis-specified. In Lemma 3 the limit $G$ is the distribution function of a probability measure, assumed continuous on all of $\mathbb R$ .

The development needs measure-theoretic cumulative distributions and interval probabilities, filters for limits, and real exponential identities. The domain definitions and scaled-tail predicate are reusable beyond this theorem. Contributions that prove the stated milestones, or supply general lemmas about weak convergence and normalized tails, fit the scope.

Selected references

A. A. Balkema and L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2(5), 792–804 (1974). DOI: 10.1214/aop/1176996548.
B. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44(3), 423–453 (1943). DOI: 10.2307/1968974.

11 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Residual Life Time at Great Age 3: F Is in the Domain of Residual Life Time Attraction of Π_{p,c} iff It Is Tail Equivalent to a Discrete Law with Gap Ratios → e^{pc} and Tail Ratios → e^{−p}Research Paper

Residual life at great age

A component that has survived to age $t$ has a residual life time $X - t$ , and in reliability, actuarial work and the analysis of excesses over high thresholds the question is what its conditional law looks like when $t$ is large. Balkema and de Haan (Ann. Probab. 2 (1974), 792–804) answered this in full generality: after an affine normalization, the only possible limit laws are the exponential law $\Pi$ , the Pareto-type laws $\Gamma_\alpha$ , and a two-parameter family of discrete laws $\Pi_{p,c}$ . The continuous half of their classification became the Pickands–Balkema–de Haan theorem behind the peaks-over-threshold method of extreme-value statistics. The discrete half is less known, and this mission treats it: Theorem 5 of the paper (§3, p. 800) describes exactly which lifetimes are attracted to $\Pi_{p,c}$ .

Discrete limits appear only when the normalization is allowed both a scale and a shift. They describe lifetimes that live, asymptotically, on a lattice-like set of ages whose spacing grows geometrically, with a fixed fraction of survivors failing at each lattice point.

The source is the published article in The Annals of Probability (DOI 10.1214/aop/1176996548); page numbers below are the journal's.

Setting

Let $X$ be a real random variable with law $\mu$ , distribution function $F$ and tail $R(x) = 1 - F(x) = P\{X > x\}$ , and assume $F(x) < 1$ for every $x$ . The residual life distribution function at age $t$ is (1), p. 792,

F_t(x) = P\{X - t \le x \mid X > t\} = \frac{\mu((t, t+x])}{\mu((t,\infty))}.

A family of distribution functions $H_t$ converges weakly to $G$ if $H_t(x) \to G(x)$ at every continuity point $x$ of $G$ . The domain of residual life time attraction $D_r(G)$ (p. 798) is the set of $F$ with $F(x) < 1$ for all $x$ for which some $a(t) > 0$ and $b(t)$ give

F_t(b(t) + x a(t)) \to G(x) \quad \text{weakly as } t \to \infty.

For $p > 0$ and $c \ge 0$ the discrete limit law is (p. 793), for $x \ge 0$ ,

\Pi_{p,c}(x) = 1 - \exp\Big(-p\Big[1 + \frac{\log(1+cx)}{cp}\Big]\Big) \ (c > 0), \qquad \Pi_{p,0}(x) = 1 - \exp\Big(-p\Big[1 + \frac{x}{p}\Big]\Big),

and $\Pi_{p,c}(x) = 0$ for $x < 0$ ; $[\,\cdot\,]$ is the integer part. Its tail takes the values $e^{-p}, e^{-2p}, \dots$ and jumps at $(e^{kpc} - 1)/c$ , $k = 0, 1, \dots$ (at $kp$ if $c = 0$ ).

A distribution function $F_0 = 1 - R_0$ is discrete with jump sequence $t_0 < t_1 < \cdots$ if the $t_n$ are unbounded, each carries positive mass and there is no other mass. Two distribution functions with $F_i(x) < 1$ for all $x$ are tail equivalent if $1 - F_1(x) \sim 1 - F_2(x)$ as $x \to \infty$ . The conditions of §3 are

\text{(12a)}\ \ \frac{t_{n+1} - t_n}{t_n - t_{n-1}} \to e^{pc}, \qquad \text{(12b)}\ \ \frac{R_0(t_{n+1})}{R_0(t_n)} \to e^{-p}.

Formalization targets

Goal: Theorem 5 (p. 800)

For $p > 0$ and $c \ge 0$ ,

F \in D_r(\Pi_{p,c}) \iff F \text{ is tail equivalent to a discrete } F_0 \text{ whose jumps satisfy (12a) and whose tail satisfies (12b).}

Milestones

(§3, pp. 799–800) A discrete $F$ satisfying (12a) and (12b) lies in $D_r(\Pi_{p,c})$ .
(§3, p. 800) If $F_1$ is tail equivalent to $F_2 \in D_r(\Pi_{p,c})$ , then $F_1 \in D_r(\Pi_{p,c})$ . Milestones 1 and 2 give the "if" half.
(Proof of Theorem 5, p. 800) If $F \in D_r(\Pi_{p,c})$ , there are $b_n \uparrow \infty$ with $R(b_{n+1})/R(b_n) \to e^{-p}$ and a discrete $F_0$ , tail equivalent to $F$ , with $R_0(t_n) = R(b_n)$ at its jumps.
(Proof of Theorem 5, pp. 800–801) Such an $F_0$ satisfies (12b) and (12a). Milestones 3 and 4 give the "only if" half.

Significance

Theorem 5, together with Theorems 1, 3 and 4 of the paper, completes the description of residual-life attraction: every nondegenerate limit is of one of the listed types, and each type's domain of attraction is identified. For the discrete types the answer is a statement purely about the geometry of the atoms of an approximating law, which makes membership checkable for concrete lifetimes (geometric-type laws on $\{0, 1, 2, \dots\}$ fall under $c = 0$ , laws on a geometric grid $\{\lambda^n\}$ under $c > 0$ ). It also explains why discrete limits are invisible when only a scale normalization is allowed.

The theorem has been proved since 1974; it has not been formalized. A machine-checked development would supply weak convergence of distribution functions at continuity points, residual-life normalizations and tail equivalence as reusable objects, and would check a proof that the paper compresses into a page, including a convergence-of-types step on a half line that the paper cites from its own §1.

Difficulty

The "if" half is close to a computation, but the computation is about weak convergence to a step function: the normed tails converge only off the jumps, and the normalization must be extended from the jump times $t_n$ to all real ages $t$ .

The "only if" half is the core. From $F \in D_r(\Pi_{p,c})$ alone one has to manufacture the atoms $t_n$ of a discrete law that $F$ itself need not have. The obvious attempt, reading the atoms off the jumps of $F$ , fails because $F$ may be continuous: membership in $D_r(\Pi_{p,c})$ only says that $F$ drops by a factor close to $e^{-p}$ over short stretches, relative to the normalization, and never by an intermediate factor. Making "never by an intermediate factor" precise uniformly in the age $t$ , with normalizations $a(t), b(t)$ about which nothing but their existence is known, is where the work lies; the same lack of control over $a(t)$ is what makes the gap ratio (12a) hard to extract.

Formalization scope

A law is a measure μ : Measure ℝ with IsProbabilityMeasure μ; the tail $R(x)$ is (μ (Set.Ioi x)).toReal, and $F_t(x)$ is μ((t, t+x]) / μ((t,∞)). $D_r(G)$ (InDr) includes $F(x) < 1$ for all $x$ , normalizations $a(t) > 0$ for all real $t$ , and "weakly" means convergence at every continuity point of $G$ and nowhere else; requiring convergence at the jumps of $\Pi_{p,c}$ would make $D_r(\Pi_{p,c})$ empty. $\Pi_{p,c}$ (piPC) is defined by cases $c = 0$ / $c > 0$ with Int.floor, so that $c = 0$ is not the junk value of a division by zero; it is used only with $p > 0$ , $c \ge 0$ . A discrete law with jump sequence $t$ (IsDiscreteWithJumps) has $t$ strictly increasing and tending to $\infty$ , positive mass at each $t_n$ and no mass elsewhere. (12a) is indexed from $n = 1$ . Tail equivalence (TailEquiv) includes $F_i(x) < 1$ for both laws.

Conventions and disclosed readings:

The page proves the "if" direction by showing convergence to a function of the type of $1 - \Pi_{p,c}$ ; since $D_r$ lets $a, b$ be chosen freely, milestone 1 is stated with $\Pi_{p,c}$ itself.
The proof of Theorem 5 uses the normalization (2)–(3) of p. 794, where $b(t)$ shifts $X$ rather than $X - t$ ; milestone 3 only asserts the existence of the sequence $b_n$ with $R(b_{n+1})/R(b_n) \to e^{-p}$ , so no convention enters its statement.
" $F_0$ only takes the values $F(b_n)$ " is formalized as $R_0(t_n) = R(b_n)$ for all $n$ , the form the next paragraph of the page uses. This identity is a hypothesis of milestone 4, as on the page, and cannot be dropped: a law tail equivalent to $F$ may carry extra atoms of vanishing relative mass, at which (12a) and (12b) fail.
The page identifies the limit of the gap ratios as the scale constant $A$ of a functional equation; milestone 4 states it as $e^{pc}$ , the gap ratio of the jumps of $\Pi_{p,c}$ .
Theorem 5 prints "distribution fuction"; this typo is kept in the quoted text only.

No statement is trivialized: $D_r(\Pi_{p,c})$ is nonempty (the geometric law on $\{0,1,2,\dots\}$ lies in $D_r(\Pi_{p,0})$ ), and Theorem 5 is not a definitional unfolding, since $D_r$ is defined by weak convergence and the right-hand side by discrete approximation.

A complete development needs: weak convergence of distribution functions at continuity points, a convergence-of-types lemma on a half line (the Remark after Lemma 1 of the paper, p. 795), and elementary facts on step functions. The first two are reusable across the whole paper and across extreme-value theory. Contributions of either half of the theorem, or of the convergence-of-types lemma, are welcome.

Selected references

A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003
B. V. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44 (1943), 423–453. https://doi.org/10.2307/1968974
L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970.

9 thms2 active usersReviewed

Algorithmic Game Theory Machine Learning Probability·Captain: mikedeng1

Asymptotic Calibration: The Regret-Balancing Randomised Forecast on the Grid {0, 1/k, …, 1} with k ≥ 1/ε² Is ε-Calibrated against Every Adaptive NatureResearch Paper

Motivation

A probability forecast is useful only when its stated frequencies bear a stable relation to outcomes. If a forecaster repeatedly announces a 70% chance of rain, calibration asks whether rain occurs on about 70% of those days. This is a minimal reliability requirement for probabilistic prediction, even though calibration alone does not rank every pair of forecasts by usefulness. Foster and Vohra study the difficulty of obtaining this property when the weather sequence is chosen in response to a forecaster's past behavior. A deterministic rule can be forced into a persistent calibration error; the article shows how randomized forecasts evade that obstruction when Nature sees past forecasts but cannot see the current random draw. Foster and Vohra, 1998.

The work sits at an intersection of sequential probability forecasting and repeated games. Its opponent can adapt to the whole observed history, including the forecaster's earlier random outcomes. The simultaneity of each round matters: before choosing that round's wet or dry outcome, Nature knows the distribution of the next forecast but not which forecast is realized. The paper's main result is about a specified forecasting rule constructed from regret balances, rather than merely the existence of some successful randomized strategy. Foster and Vohra, 1998, §§3, 5.

Timeline. Dawid (1982) proposed calibration as a criterion for sequential probability forecasts and showed that a coherent Bayesian expects to be calibrated (doi). Oakes (1985), with Dawid's accompanying comment, showed that no deterministic forecaster is calibrated against every outcome sequence: Nature may rain exactly when the forecast is at most $1/2$ (doi). Foster and Vohra circulated the present randomized construction from 1994 (received August 1994, published 1998); their 1997 Games and Economic Behavior paper used a calibrated forecaster built on the same pairwise-regret flow equations to reach correlated equilibria (doi). Hart and Mas-Colell (2000) later turned the same internal-regret quantities into regret matching (doi).

Setting

At round $s$ , the outcome $X_s$ is $1$ for wet and $0$ for dry. The forecaster selects a probability from the finite grid $G_k=\{0,1/k,\ldots,1\}$ , where $k$ is a positive integer. A forecast $p$ is represented by the binary probability vector $(1-p,p)$ ; the second coordinate is the forecast chance of rain. The forecaster chooses $i/k$ with probability $\mu_s^i$ . The Brier loss of that possible forecast is $L_s^i=(X_s-i/k)^2$ .

After $t$ rounds, $n_t(p)$ counts the realized forecasts equal to $p$ , and $\rho_t(p)$ is the observed fraction of wet outcomes on those rounds. The quadratic calibration score is

C_t=\sum_{p\in G_k}\frac{n_t(p)}{t}\bigl(\rho_t(p)-p\bigr)^2.

A forecast never issued has zero count and contributes zero. The paper also uses a weighted calibration score $\widetilde C_t$ , in which the realized indicator that $i/k$ was chosen is replaced by its conditional probability $\mu_s^i$ . Its weighted count is $\widetilde n_t(i/k)=\sum_{s<t}\mu_s^i$ , and its weighted wet frequency is $\widetilde\rho_t(i/k)=\sum_{s<t}\mu_s^i X_s/\widetilde n_t(i/k)$ when the denominator is positive.

For grid points $i/k$ and $j/k$ , the pairwise regret $R_t^{i\to j}$ is the positive part of the cumulative weighted reduction in Brier loss that would result from replacing $i/k$ by $j/k$ on rounds weighted by $\mu_s^i$ . The algorithm chooses its next distribution so that the regret flow out of each $i$ equals the flow into $i$ :

\mu_s^i\sum_j R_{s-1}^{i\to j} =\sum_j\mu_s^j R_{s-1}^{j\to i}.

These equations use only regret from previous rounds. They specify a distribution after every possible history, including histories created by Nature's adaptive choices. Foster and Vohra, 1998, §5.

Formalization targets

Main theorem

The target is Theorem 1: for every $\varepsilon>0$ , choose $k\ge1/\varepsilon^2$ and let the forecaster follow the regret-flow equations. Against every adaptive Nature, the realized score eventually satisfies

\Pr\{C_t<\varepsilon\}>1-\varepsilon.

The time after which the inequality holds may depend on the forecaster, Nature, and $\varepsilon$ . The statement fixes the algorithm and the grid scale; a general existence theorem would leave out its central content. Foster and Vohra, 1998, Theorem 1 and §6 Corollary.

Supporting targets

The milestones record the source's attack path: solvability of the flow equations, a history-adapted forecaster satisfying them, the counting-process bounds and convergence of $C_t-\widetilde C_t$ in probability, the algebraic link between calibration and regret, the bound on the smoothed regret potential, and the deterministic bound on $\widetilde C_t$ . Theorem 3's last constant is written as $(k+1)/(2\delta)$ and the corollary's horizon as $8k^2/\varepsilon^2$ ; the printed constants are inconsistent with the paper's $k+1$ grid points and its derived rate, respectively. The provenance and corrections are recorded with those milestones. Foster and Vohra, 1998, §6.

Significance

The result gives a concrete randomized forecaster whose realized empirical frequencies remain reliable even when outcomes react to past forecasts. The game model includes fixed outcome sequences as a special case, but its adaptive Nature can condition future choices on every earlier realized forecast and outcome. The theorem therefore identifies a particular sequential rule, its finite forecast grid, and the information boundary under which its guarantee holds. Foster and Vohra, 1998, §§3, 5–6.

The published Foster–Vohra 1997 formalization already supplies reusable definitions of finite probability vectors, history laws, pairwise regret, and calibration scores, together with a proved finite flow-conservation theorem. This mission extends that substrate to the 1998 paper's Brier-loss grid algorithm. Theorem 1 and its supporting results are proved on paper but not yet formalized; the earlier formal existence theorem for some calibrated forecaster does not establish this algorithm's guarantee, which is the content of the goal.

Difficulty

The weighted score $\widetilde C_t$ is controlled by quantities known from the chosen mixtures, while $C_t$ depends on the actual random draws. A direct deterministic bound on $C_t$ therefore does not follow from the regret equations. The gap requires a quantitative comparison of realized counts and weighted counts under an adaptive history law, followed by a passage from those count errors to the nonlinear calibration score. The regret itself has a positive-part kink, so its aggregate bound is stated through the paper's smoothed potential. Foster and Vohra, 1998, §6.

Formalization scope

The Lean model uses binary outcomes, $k+1$ grid indices Fin (k + 1), and histories ordered from oldest to newest. Rounds start at index $0$ : the paper's $R_{s-1}$ in round $s$ is the regret over the preceding $s$ indices. Forecast and outcome are drawn independently conditional on the past by the published histLaw; Nature is any map from complete past histories to a probability distribution on the two outcomes. The forecast rule is likewise a map from histories to grid distributions. For each earlier round it reads only that round's prefix, so the current outcome cannot influence its mixture.

The goal uses the realized quadratic score calibScore2Hj h 1, whose second vector coordinate is the wet probability. The map $i\mapsto(1-i/k,i/k)$ is injective for $k>0$ . The weighted score is a separate definition used in supporting results. A forecaster satisfying the flow equations is shown to exist by a milestone, so the goal's algorithm hypothesis has content. The statement covers adaptive Nature; replacing Nature by a fixed sequence or replacing $C_t$ by $\widetilde C_t$ would change the claim.

Every theorem requiring the grid has the explicit $k>0$ condition. Deterministic calibration bounds assume binary outcomes and probability-vector weights; the history-law theorems obtain these properties from Fin 2 and PMF. When a weighted count is zero, Lean's division convention gives weighted wet frequency $0$ ; nonnegative weights make its numerator zero as well. At horizon $0$ , the weighted calibration score is $0$ . The probability event is measured with the history law's outer measure in $\mathbb R_{\ge0}\cup\{\infty\}$ . Reusable work includes finite-history martingale estimates, weighted calibration comparisons, and finite regret-potential bounds.

Selected references

D. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85(2):379–390, 1998. DOI: 10.1093/biomet/85.2.379.
A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77:605–613, 1982. DOI: 10.1080/01621459.1982.10477856.
D. Oakes, Self-calibrating priors do not exist, Journal of the American Statistical Association 80:339, 1985, with comments by A. P. Dawid (pp. 340–341) and M. Schervish (pp. 341–342). DOI: 10.1080/01621459.1985.10478117.
D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21:40–55, 1997. DOI: 10.1006/game.1997.0595.
D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6:1–8, 1956. DOI: 10.2140/pjm.1956.6.1.
S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68:1127–1150, 2000. DOI: 10.1111/1468-0262.00153.

14 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Some Theoretical Aspects of Road Traffic Research I: Time-Mean Speed Equals Space-Mean Speed plus σₛ²/v̄ₛ, so v̄ₜ ≥ v̄ₛ with Equality Only Without Speed VariationResearch Paper

Why two traffic speed averages differ

A speed recorded as a vehicle passes a fixed point and a speed recorded among vehicles occupying a road segment answer different questions. Fast vehicles pass a detector more often per unit time; slow vehicles remain visible along the segment for longer. Traffic studies therefore need to identify which distribution a measurement samples before comparing average speeds. J. G. Wardrop made this distinction explicit in his 1952 treatment of road traffic, then quantified it through the variance of the spatial speed distribution (Wardrop 1952, pp. 327–331 and Appendix II).

The result belongs to the paper's mathematical account of traffic flow. It is useful even when the subsidiary streams do not describe a random vehicle process: the identities concern finite positive flows and speeds. The paper also applies the same distributions to speed samples from radar and aerial photographs and to an idealized count of overtaking events (Wardrop 1952, pp. 330, 333–334).

Traffic streams and their two distributions

A road's traffic stream is divided into $C$ subsidiary streams, indexed by $i=1,\ldots,C$ . Stream $i$ has flow $q_i$ , the number of vehicles passing a point per unit time, and speed $v_i$ . Its concentration is $k_i=q_i/v_i$ , the number of vehicles occupying a unit road length. Total flow and concentration are $Q=\sum_i q_i$ and $K=\sum_i k_i$ . The time frequency $f_i=q_i/Q$ weights each stream by how often its vehicles pass a point. The space frequency $f'_i=k_i/K$ weights it by the fraction of vehicles present along the road.

The time-mean speed is $\bar v_t=\sum_i q_i v_i/Q=\sum_i f_i v_i$ . The space-mean speed is $\bar v_s=\sum_i k_i v_i/K=\sum_i f'_i v_i$ . Both are averages of the same speeds; the weights differ. Wardrop defines the space-distribution variance independently as $\sigma_s^2=\sum_i k_i(v_i-\bar v_s)^2/K$ , and the corresponding coefficient of variation as $c_s=\sigma_s/\bar v_s$ (equations (1)–(3), (7), pp. 328–331).

These are finite sums, not limits of a stochastic process. The model requires at least one subsidiary stream and positive flow and speed for each stream. Positive flows ensure that every speed in the equality criterion belongs to a present stream; positive speeds make concentration meaningful. The count $C$ is allowed to be one. In that case both means coincide and the variance is zero, as the formulas require.

Formalization targets

The main target is Wardrop's equation (6), together with its stated comparison and equality case (p. 330; Appendix II, p. 356):

\bar v_t=\bar v_s+\frac{\sigma_s^2}{\bar v_s},\qquad \bar v_s\le\bar v_t,\qquad \bar v_t=\bar v_s\iff v_i=v_j\text{ for every }i,j.

The subsidiary targets follow the paper's order. Equation (4) says $k_i v_i=q_i$ for each stream, giving equation (5), $Q=K\bar v_s$ . Appendix II then uses the centered identity $\sum_i f'_i(v_i-\bar v_s)=0$ and rewrites the time mean as $\bar v_t=(\sum_i f'_i v_i^2)/\bar v_s$ . These three claims are the mission milestones. Equation (8) is included as a companion formulation:

\bar v_t=\bar v_s(1+c_s^2).

The mission also records the paper's formulas for equally weighted time and space speed samples and the equivalent space- and time-frequency formulas for the idealized overtaking count. These companions use the same definitions without changing the main target (pp. 330–334).

What the result supplies

The identity gives an exact size and direction for the difference between the two averages. Since the variance is nonnegative and $\bar v_s$ is positive, the time mean cannot fall below the space mean. If all constituent speeds are equal, the difference vanishes; if any two present streams have different speeds, the difference is positive. The formula therefore lets a reader decide whether two reported speed averages can be compared directly, and it identifies the spatial variance as the quantity needed to convert between them.

The sample formulas sharpen that interpretation. Equal weights among vehicles passing a point make the time mean the arithmetic mean of the sampled speeds and the space mean their harmonic mean. Equal concentrations reverse which mean is arithmetic; the time mean becomes $\sum_i v_i^2/\sum_i v_i$ . The overtaking formulas express a single pairwise count using either frequency system, provided the speeds are ordered and the paper's assumption of no interference with overtaking is used (Wardrop 1952, pp. 330, 333–334).

Wardrop proved these formulas in print. The remaining work in this mission is a machine-checked proof of the finite-sum identities and their strict equality case. The proposal supplies typed statements and definitions, but the theorem proofs are open. The resulting concentration and frequency definitions are reusable in other traffic-flow formalizations; the statements also provide small algebraic interfaces for testing more elaborate traffic models.

Where the formal proof needs care

The relation looks like a routine identity for weighted means, but the two weight systems are coupled through $k_i=q_i/v_i$ . One cannot treat the time and space frequencies as independent arbitrary probability vectors and still obtain equation (6). The strict case needs more than nonnegativity of the variance: it needs the fact that every space weight is positive, so zero variance forces every constituent speed to equal the mean. The single-stream case and every denominator need the same attention.

The overtaking statement has a separate modelling boundary. Its algebraic equalities use a rate defined by pairwise speed differences. Wardrop's physical interpretation of that rate assumes that overtaking does not interfere with other overtaking. The mission records the identities for that idealized rate, without claiming that a measured road necessarily meets the physical assumption.

Formalization scope

Lean uses Fin C for the streams and real numbers for $q_i$ , $v_i$ , $k_i$ , both means, the variance, and the overtaking rate. Finite sums are taken over all streams. The theorem hypotheses require $0<C$ , $0<q_i$ , and $0<v_i$ for every $i$ . These requirements make $Q$ , $K$ , and $\bar v_s$ positive; Lean's total division would otherwise assign a zero value at a zero denominator that has no meaning in the paper's model. For the overtaking identity, StrictMono v retains Wardrop's ordering $v_1<\cdots<v_C$ .

The variance is defined from equation (7), $\sum_i k_i(v_i-\bar v_s)^2/K$ . Defining it by rearranging equation (6) would make the target true by definition and would erase the mathematical claim. The standard deviation uses the real square root of that variance. An observation in the sample companion is represented as one subsidiary stream of equal time or space weight; this is the formal reading of the paper's sampling paragraphs. No probability-measure library is needed, since $f_i$ and $f'_i$ are explicit finite weights.

A complete proof needs finite-sum rearrangements, elementary real division under positive denominators, nonnegative weighted squares, and the equality case of a positive weighted sum of squares. The definitions and the mean identities are welcome as separate reusable contributions. The mission does not include the paper's normal approximation for overtaking density in equation (11), which Wardrop presents as an approximation rather than an exact finite-sum theorem.

Selected references

J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers, Part II 1 (1952), 325–362. DOI: 10.1680/ipeds.1952.11259.

5 thms2 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Some Aspects of the Sequential Design of Experiments I: Greedy Sampling with Density-Zero Forced Draws Earns max(α, β) per Draw from Any Two Populations with Finite MeansResearch Paper

Motivation

An experimenter can draw observations from two populations $A$ and $B$ , one at a time, and wants the sum of the observations to be as large as possible. The populations might be two treatments, two seed varieties or two manufacturing processes; their means are unknown. Each draw both earns a reward and tells the experimenter something about the population it came from. This is the two-armed bandit problem. Herbert Robbins posed it in its modern form in his 1952 address to the American Mathematical Society, Some aspects of the sequential design of experiments, the paper usually credited with founding the field.

Section 2 of that paper asks a basic question (display (12), p. 532): is there any sampling rule whose average reward per draw approaches the larger of the two means, whatever the populations are? Robbins answers yes, for any two populations with finite means, using one explicit rule: forced sampling along a sparse schedule, greedy choice otherwise. This mission formalizes that answer.

Timeline:

1933. Thompson proposes a randomized rule for choosing between two treatments (Biometrika 25).
1952. Robbins states the problem for general populations and gives the rule $\bar R$ with $\lim_n L_n(A,B,\bar R) = 0$ for any two populations with finite means. The argument is only indicated ("it can be shown").
1985. Lai and Robbins replace $o(n)$ loss by the optimal logarithmic regret for parametric families (Adv. Appl. Math. 6).
2020. Lattimore and Szepesvári give the textbook account of explore-then-commit and $\varepsilon$ -greedy rules, which descend from forced sampling (Bandit Algorithms).

Setting

Population $A$ has distribution function $F$ and population $B$ has $G$ , with expectations

\alpha = \int_{-\infty}^{\infty} x\,dF(x), \qquad \beta = \int_{-\infty}^{\infty} x\,dG(x),

assumed to exist, i.e. to be finite (display (1), p. 529). Nothing else is assumed about $F$ and $G$ .

A sampling rule $R$ draws $x_1, x_2, \dots$ one at a time; the population of the $i$ -th draw may depend on $x_1, \dots, x_{i-1}$ , and given that choice $x_i$ is a fresh draw from the chosen population. Write $S_n = x_1 + \cdots + x_n$ . The loss of $R$ after $n$ draws (display (9), p. 531) is

L_n(A, B, R) = \max(\alpha, \beta) - E\!\left(\frac{S_n}{n}\right),

the average shortfall per draw compared with someone who knows the better population and samples only from it.

The forcing schedule (display (13), p. 532) is a pair of disjoint, strictly increasing sequences of positive integers

1 = a_1 < a_2 < \cdots, \qquad 2 = b_1 < b_2 < \cdots

of density zero: the fraction of the integers $1, \dots, n$ that are an $a$ or a $b$ tends to $0$ .

The rule $\bar R$ : at draw $i$ , sample $A$ if $i$ is an $a$ , sample $B$ if $i$ is a $b$ , and otherwise sample $A$ if the mean of the previous observations from $A$ is strictly larger than the mean of the previous observations from $B$ , and $B$ if it is not (a tie goes to $B$ ).

Formalization targets

Goal: Section 2, Eq. (16)

For every pair of populations with finite means and every forcing schedule,

\lim_{n\to\infty} L_n(A, B, \bar R) = 0.

The goal is about the specific rule $\bar R$ and every schedule, not about the mere existence of a rule. It contains no rate and no constant, so it stays valid when the rule is analysed more finely.

Milestone: Eq. (14), almost-sure average

\lim_{n\to\infty} \frac{S_n}{n} = \max(\alpha, \beta) \quad\text{with probability } 1.

Milestone: Eq. (15), expected average

\lim_{n\to\infty} E\!\left(\frac{S_n}{n}\right) = \max(\alpha, \beta).

The goal follows from (15) by the definition (9); the paper's chain is (14) ⇒ (15) ⇒ (16).

Significance

The result. The theorem answers question (12) and shows that "learning while earning" costs nothing in the long run, per draw, under no assumption beyond finite means: no bounded support, no variance, no parametric family. It is the first consistency result for an adaptive allocation rule, and it fixes the benchmark later refined by logarithmic-regret theory. In modern terms, a forced-exploration greedy policy has regret $o(n)$ on every two-armed bandit with integrable rewards.

Formalizing it. The paper gives no proof; it says the results "can be shown". A machine-checked proof records the argument in full. The platform already has finite-horizon regret bounds for $\varepsilon$ -greedy with bounded rewards (FoundationsRL.Bandits.epsilon_greedy_regret_bound), consistency in the stronger Lai–Robbins sense as a definition (ConsistentBanditPolicy), and a forced-sample tail bound for the Lasso bandit (BastaniBayati.LassoBandit.forced_sample_estimator_tail). None of these covers a deterministic greedy rule, almost-sure convergence, or unbounded rewards with only a first moment, and none of them proves (14)–(16).

Difficulty

The obvious argument is: each population is sampled infinitely often because of the forced draws, so each running mean converges by the strong law, so greedy eventually picks the better population, and the forced draws are negligible. Two steps are not routine.

First, the strong law applies to i.i.d. sequences, while the observations from $A$ arrive at random, history-dependent times. The values seen from $A$ have to be identified, in law, with an i.i.d. sequence that is independent of the times at which they are used.

Second, passing from (14) to (15) needs uniform integrability of $S_n/n$ , and only first moments are available. No second moment is assumed, so variance bounds are not available.

When $\alpha = \beta$ greedy need not settle on either population; the statement must hold anyway, and an argument that waits for greedy to "lock in" does not cover this case.

Formalization scope

The populations are a published two-armed BanditAlgorithm.StochasticBandit 2. $A$ is arm 0 and $B$ is arm 1; $\alpha$ and $\beta$ are banditArmMean. A rule is a published BanditPolicy 2, and $E$ is the integral against the published infinite-horizon law banditTrajMeasure, whose coordinate $t$ is the paper's draw $t+1$ . Explicit readings of the paper's phrases:

"the expectations exist" means both reward laws are Integrable. This is the only assumption on the populations: the class $D$ of the paper is left arbitrary, and $\alpha = \beta$ is allowed.
"density 0" means #({1,…,n} ∩ (range a ∪ range b)) / n → 0 in $\mathbb R$ . The sequences are infinite and 0-indexed (a 0 = 1, b 0 = 2).
"according as … exceeds or does not exceed": $A$ exactly when mean $_A$ > mean $_B$ , so ties go to $B$ .
"with probability 1" is ∀ᵐ under the trajectory law, and "lim" is Tendsto … atTop along $n \in \mathbb N$ .
$S_n/n$ uses real division; its value at $n = 0$ plays no role.

Trivializing formalizations are excluded. Without integrability the means and expectations are junk zeros; this is ruled out by the integrability hypothesis. Replacing $\bar R$ by "there exists a rule" would weaken the goal to (12). Finite forcing sets would make the statement false.

The needed infrastructure is a representation of the adaptive sampling process by per-population i.i.d. reward sequences, the strong law along random subsequences, and a uniform-integrability argument for averages under only a first moment. All three are reusable for other forced-exploration and greedy policies. Contributions of these general lemmas as separate theorems are welcome.

Selected references

H. Robbins, Some aspects of the sequential design of experiments, Bull. Amer. Math. Soc. 58(5) (1952), 527–535. https://doi.org/10.1090/S0002-9904-1952-09620-8
W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25 (1933), 285–294. https://doi.org/10.2307/2332286
T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6 (1985), 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

8 thms2 active usersReviewed

Optimization Probability·Captain: mikedeng1

A Stochastic Approximation Method: If M Is Nondecreasing, M(θ) = α and M′(θ) > 0, the Robbins–Monro Iterates with Steps of Type 1/n Converge to θ in Mean SquareResearch Paper

Motivation

Many problems in statistics and engineering ask for the level $\theta$ at which an unknown function takes a prescribed value $\alpha$ : the dose at which a fraction $\alpha$ of subjects respond, the setting at which a noisy device reaches a target output, the $\alpha$ -quantile of a distribution that can only be probed by yes/no experiments. When the function can only be observed through noisy measurements, classical root-finding does not apply. Robbins and Monro (Ann. Math. Statist. 22 (1951) 400–407) proposed a recursive procedure that uses one noisy observation per step and proved that it converges in mean square. The paper started the field of stochastic approximation, which today underlies stochastic gradient descent, temporal-difference learning and adaptive control.

Timeline. Robbins and Monro (1951) prove mean-square convergence for bounded responses under conditions (5′) or (33)–(35). Kiefer and Wolfowitz (1952) adapt the scheme to finding a maximum. Blum (1954) proves almost-sure convergence under weaker moment conditions. Dvoretzky (1956) gives a general convergence theorem covering both schemes. Later work (Robbins and Siegmund, 1971; Ljung, 1977; Kushner and Clark, 1978; Benaïm, 1999) develops the supermartingale and ODE methods.

Setting

To each real level $x$ corresponds a random response $Y(x)$ with distribution function $H(y \mid x)$ , and the regression function is

M(x) = \int_{-\infty}^{\infty} y \, dH(y \mid x).

The responses are bounded: there is $C > 0$ with $\Pr[|Y(x)| \le C] = 1$ for all $x$ (condition (4)). Fix constants $\alpha, \theta$ and positive step sizes $a_n$ . The Robbins–Monro process starts at an arbitrary constant $x_1$ and sets

x_{n+1} - x_n = a_n(\alpha - y_n), \qquad \Pr[y_n \le y \mid x_n] = H(y \mid x_n),

so $y_n$ is a fresh response observed at the current level $x_n$ . The quantity of interest is the mean squared error $b_n = E(x_n - \theta)^2$ .

A sequence $\{a_n\}$ is of type $1/n$ if

\sum_{n=1}^{\infty} a_n^2 < \infty \quad (6), \qquad \sum_{n=2}^{\infty} \frac{a_n}{a_1 + \cdots + a_{n-1}} = \infty \quad (26);

$a_n = 1/n$ is the standard example. The proof also uses $d_n = E[(x_n-\theta)(M(x_n)-\alpha)]$ , $e_n = E[\int (y-\alpha)^2\,dH(y\mid x_n)]$ and $A_n = |x_1 - \theta| + [C+|\alpha|](a_1 + \cdots + a_{n-1})$ .

Formalization targets

Goal: Theorem 2 (p. 405)

If $\{a_n\}$ is of type $1/n$ , (4) holds, and $M$ is nondecreasing with $M(\theta) = \alpha$ and $M'(\theta) > 0$ , then, whatever $x_1$ ,

\lim_{n \to \infty} E(x_n - \theta)^2 = 0.

Milestones

The one-step identity (14): $b_{n+1} - b_n = a_n^2 e_n - 2a_n d_n$ .
The signs and bound after (14): $d_n \ge 0$ and $0 \le e_n \le [C+|\alpha|]^2$ .
(17)–(18): $\sum a_n^2e_n$ and $\sum a_n d_n$ converge, and $b = \lim b_n = b_1 + \sum a_n^2e_n - 2\sum a_nd_n$ exists with $b \ge 0$ .
Lemma 1: if $d_n \ge k_n b_n$ with $k_n \ge 0$ and $\sum a_n k_n = \infty$ , then $b = 0$ .
(22): $\Pr[|x_n - \theta| \le A_n] = 1$ .
(24): $d_n \ge \bar k_n b_n$ , where $\bar k_n$ is the infimum of $(M(x)-\alpha)/(x-\theta)$ over $0 < |x-\theta| \le A_n$ .
(27): (26) implies $\sum a_n = \infty$ .
Lemma 2: if $\bar k_n \ge K/A_n$ for some $K > 0$ and large $n$ , and (26) holds, then $b = 0$ .
(42): under (33)–(35), $(M(x)-\alpha)/(x-\theta) \ge \delta M'(\theta)/2A_n$ on $0 < |x-\theta| \le A_n$ .

Companion results

Theorem 1 (p. 404: the same conclusion under (5′), $M(x) \le \alpha - \delta$ for $x < \theta$ and $M(x) \ge \alpha + \delta$ for $x > \theta$ ); convergence in probability under the hypotheses of Theorem 2 (p. 401); the quantile estimator of §4, (48); and (30), that $c'/n \le a_n \le c''/n$ gives a sequence of type $1/n$ .

Significance

Theorem 2 is the first convergence theorem for a recursive root-finding procedure under noise. It shows that a procedure using no knowledge of $M$ or of the noise distribution, beyond a monotone crossing and a positive slope at the root, is consistent. Section 4 turns it into a distribution-free consistent estimator of a quantile from response/nonresponse data, the up-and-down designs of bioassay and sensitivity testing. Its step-size conditions, $\sum a_n^2 < \infty$ with a divergence condition, remain the standard conditions for stochastic gradient methods.

The theorem has been proved since 1951 and strengthened many times. As far as is known it has no machine-checked proof, and Mathlib has no stochastic approximation theory. Formalizing it requires conditional laws given by Markov kernels, integration against a composition of a measure with a kernel, and deterministic series arguments. A finished formalization would be a base for formalizing the almost-sure theorems (Blum, Robbins–Siegmund) and the ODE method.

Difficulty

The obvious argument fails at one step. Monotonicity of $M$ and a positive derivative at $\theta$ do not give a uniform positive lower bound on the slope $(M(x)-\alpha)/(x-\theta)$ : away from $\theta$ the slope can decay to $0$ , for example when $M$ is bounded, as (4) forces. So the drift towards $\theta$ is not uniformly strong, and the newcomer's first idea, a uniform contraction $b_{n+1} \le (1 - c\,a_n) b_n + O(a_n^2)$ , is not available under (33)–(35). This is why the theorem needs the divergence condition (26), which is stronger than $\sum a_n = \infty$ , and not only (6). On the formal side, the expectations come from integrating against the joint law of $(x_n, y_n)$ , and they need integrability bounds before any identity can be used.

Formalization scope

Everything is in the namespace RobbinsMonroSA.Conv, over a probability space $(\Omega, P)$ with IsProbabilityMeasure P. Indices are 0-based: Lean's x 0, a 0 are the paper's $x_1$ , $a_1$ , and Lean's bigA … n is the paper's $A_{n+1}$ . The committed conventions are:

$H$ is a Kernel ℝ ℝ with IsMarkovKernel H (each $H(\cdot\mid x)$ is a probability law, measurable in $x$ ).
(4) is 0 < C ∧ ∀ x, H x [-C, C] = 1. It is a hypothesis of every item that mentions an expectation, and it is what keeps the Bochner integrals defining $b_n$ , $d_n$ , $e_n$ and $M$ from defaulting to $0$ .
(8) is the joint-law equation: the law of $(x_n, y_n)$ is the law of $x_n$ composed with $H$ . (7) holds surely, and $x_n$ , $y_n$ are measurable. No Markov property or filtration beyond (8) is assumed.
Every " $= \infty$ " for a series ((19), (26), (27)) is divergence of partial sums to $+\infty$ . " $b = 0$ " is $b_n \to 0$ .
$M'(\theta) > 0$ is HasDerivAt M M' θ with 0 < M'.
The infimum $\bar k_n$ of (23) is never formed. (24) and (25) are stated with lower bounds on $(M(z)-\alpha)/(z-\theta)$ over $0<|z-\theta|\le A_n$ . This avoids the junk value $0$ that Lean's real infimum gives on the empty range ( $A_n = 0$ ), where the paper's infimum is $+\infty$ .

The standing assumptions of §3, (4), (5) and (6), are hypotheses of Lemma 1, Lemma 2 and the displays of §3 whose proofs use them. In Theorems 1 and 2, (5) follows from (5′) or from (33)–(34), and (6) is part of "type $1/n$ ".

The goal cannot be trivialized. It mentions neither $d_n$ , $e_n$ , $A_n$ nor any constant, and the process must satisfy (8) for every $n$ . Without (8), $y_n$ would be arbitrary and the statement false; with $y_n = M(x_n)$ it would be deterministic.

Contributions welcome: proofs of the milestones, reusable lemmas on integrating against μ ⊗ₘ κ, and a proof that $a_n = 1/n$ satisfies (26).

Selected references

H. Robbins and S. Monro, A stochastic approximation method, Ann. Math. Statist. 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586
J. Kiefer and J. Wolfowitz, Stochastic estimation of the maximum of a regression function, Ann. Math. Statist. 23 (1952), 462–466. https://doi.org/10.1214/aoms/1177729392
J. R. Blum, Approximation methods which converge with probability one, Ann. Math. Statist. 25 (1954), 382–386. https://doi.org/10.1214/aoms/1177728794
A. Dvoretzky, On stochastic approximation, Proc. Third Berkeley Symp. Math. Statist. Prob. 1 (1956), 39–55. https://projecteuclid.org/euclid.bsmsp/1200501645
H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics (1971), 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, LNM 1709 (1999), 1–68. https://doi.org/10.1007/BFb0096509

11 thms2 active usersReviewed

Probability·Captain: mikedeng1

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality I: P(√n sup(F − F̂ₙ) > λ) ≤ exp(−2λ²) for λ ≥ min(√(log 2/2), 1.0841 n^(−1/6))Research Paper

Motivation

The Kolmogorov–Smirnov statistics measure how far the empirical distribution of a sample lies from a hypothesised distribution. They are the standard goodness-of-fit test for continuous data, and their tail probabilities are the basic tool for confidence bands around a distribution function. A test is only usable at a fixed sample size if those tail probabilities are controlled for every $n$ , not just in the limit.

Timeline.

1933–1944. Kolmogorov and Smirnov introduce the statistics, prove that their laws do not depend on the continuous distribution, and find the limit laws, e.g. $\lim_n P(D_n^->\lambda)=\exp(-2\lambda^2)$ . Smirnov (1944) also gives the exact law of the one-sided statistic and the expansion $P(D_n^->\lambda)=\exp(-2\lambda^2)\bigl(1-\frac{2\lambda}{3\sqrt n}+O(n^{-1})\bigr)$ .
1956. Dvoretzky, Kiefer and Wolfowitz prove $P(D_n^->\lambda)\le C\exp(-2\lambda^2)$ for every $n$ , with an unspecified constant $C$ (Ann. Math. Statist. 27).
1958. Birnbaum and McCarty conjecture that $C=1$ is admissible.
1979–1985. Explicit constants: $C\le306$ (Devroye and Wise), $C\le29$ (Shorack and Wellner), $C\le2\sqrt2$ (Hu).
1990. Massart proves the conjecture under a mild lower bound on $\lambda$ , and deduces the two-sided bound with the optimal constant $2$ (Ann. Probab. 18).

Setting

Let $x_1,\dots,x_n$ ( $n\ge1$ ) be independent, identically distributed real random variables with a continuous distribution function $F$ . The empirical distribution function is

\hat F_n(x)=\frac1n\sum_{i=1}^n\mathbb 1_{(x_i\le x)},

and the centred, normalised empirical process is $Z_n=\sqrt n(\hat F_n-F)$ . The statistics are

D_n^+=\sup_{x\in\mathbb R}Z_n(x),\qquad D_n^-=\sup_{x\in\mathbb R}\bigl(-Z_n(x)\bigr),\qquad D_n=\sup_{x\in\mathbb R}|Z_n(x)|.

In Lean the sample is X : Fin n → Ω → ℝ, independent (iIndepFun X P) with common law μ (HasLaw (X i) μ P), $F$ is cdf μ, and the statistics are Dplus μ X, Dminus μ X, Dtwo μ X. The parameter $\lambda$ is written l.

The proof works with Smirnov's point probabilities $p_{\lambda,n}(j)=\lambda\sqrt n\,(j+\lambda\sqrt n)^{j-1}(n-j-\lambda\sqrt n)^{n-j}n^{-n}\binom nj$ , whose sum over $0\le j<n-\lambda\sqrt n$ is $P(D_n^->\lambda)$ , with Csáki's density $f_\lambda(s)=\frac{\lambda}{\sqrt{2\pi}}s^{-3/2}(1-s)^{-1/2}\exp\bigl(-\frac{\lambda^2}{2s(1-s)}\bigr)$ of the first passage of a Brownian bridge at level $\lambda$ , and with the ratio $C_{\lambda,n}=\exp(2\lambda^2)P(D_n^->\lambda)$ .

Formalization targets

Goal: Theorem 1

For every $n\ge1$ and every $\lambda\ge\sqrt{\log(2)/2}\wedge\gamma n^{-1/6}$ , with $\gamma=1.0841$ ,

P(D_n^->\lambda)\le\exp(-2\lambda^2).

Here $\wedge$ is the minimum. The constant $1$ in front of the exponential is the point of the theorem; the threshold on $\lambda$ is the paper's.

Milestones

The milestones follow the proof in the paper's order of attack:

the reduction to the uniform law, and Smirnov's exact formula (2.3);
the identity $\int_0^1f_\lambda=\exp(-2\lambda^2)$ (2.4);
the local comparison of $p_{\lambda,n}(j)$ with $f_\lambda$ : (2.7), Lemma 2, Claims 1–3, and Proposition 1;
the midpoint bound for log-convex integrands (Lemma 3) and the closed forms of Lemma 4;
the nonasymptotic expansion (2.11), the negativity of its right side $\eta_n$ , and with them Theorem 1 for $n\ge39$ , $\lambda\le\sqrt n/2$ ;
Proposition 2 on the slope of $C_{\lambda,n}$ , the crude bounds (2.13)–(2.14), and the finite grid check (2.15) for $n\le38$ .

Companions

The equality in law of $D_n^+$ and $D_n^-$ , Comment 1 ((1.4) whenever $\exp(-2\lambda^2)\le1/2$ ), the reduction $P(D_n>\lambda)\le2P(D_n^->\lambda)$ , and Corollary 1:

P(D_n>\lambda)\le2\exp(-2\lambda^2)\qquad(\lambda>0).

Significance

The result. Theorem 1 and Corollary 1 give non-asymptotic Kolmogorov–Smirnov bands with the asymptotic constants, $1$ and $2$ , which cannot be improved because of the limit laws. Corollary 1 is the form in which the DKW inequality is quoted throughout statistics and learning theory: confidence bands for distribution functions, sample-size calculations for quantile estimation, and as a building block in bandit and empirical-risk analyses. Comment 1 says that the one-sided test is never anti-conservative at levels up to 50%, whatever the sample size.

Formalizing it. The result is proved on paper but not machine-checked. A formal development would give a verified, constant-explicit DKW inequality that downstream statistical results can import as a black box instead of carrying an unspecified $C$ . The milestones also produce reusable pieces: Smirnov's exact law of the one-sided statistic, the Brownian-bridge first-passage integral, and a family of explicit elementary inequalities. The proof uses computer-checked numerics ((2.15), Lemma 2, $\eta_{39}$ ); turning those into checked certificates is part of the work.

Difficulty

The obvious route is to compare the exact sum (2.3) term by term with the integral (2.4). The local comparison $P(\tau_n=t)\le\frac1nf_\lambda(t-\varepsilon/3)$ is only nearly true: a corrective factor is needed, and it is largest on the tail, where the crossing time $t$ is close to $\varepsilon=\lambda/\sqrt n$ . Controlling that factor uniformly in $j$ while keeping the leading constant exactly $1$ is what forces the delicate constants ( $\theta=0.4833$ , $\beta=0.826$ , $\mu=0.4345$ , $\gamma=1.0841$ ). For small $n$ the analytic bounds are too weak, and the proof closes the gap with a Lipschitz bound on $\lambda\mapsto C_{\lambda,n}$ plus a finite numerical check over a grid; neither half suffices alone.

Formalization scope

Conventions:

$n\ge1$ ; the sample is indexed by Fin n; $F$ is cdf μ with Continuous (cdf μ) assumed, as in Theorem 1.
Probabilities are measures of events in $[0,\infty]$ and are compared with ENNReal.ofReal of the bound. Each supremum defining a statistic is of a function with values in $[-1,1]$ , hence a genuine real supremum.
$p_{\lambda,n}(j)$ uses an integer power at $j-1$ , so that $p_{\lambda,n}(0)=(1-\varepsilon)^n$ . $C_{\lambda,n}$ is defined from the exact formula (2.3); it equals $\exp(2\lambda^2)P(D_n^->\lambda)$ by the (2.3) milestone, so the analytic milestones carry no probability.
Statements that the page gives through derivatives of $C_{\lambda,n}$ (Proposition 2(i), (iii)) are stated as monotonicity and as an increment bound, because $C_{\lambda,n}$ has kinks.

Additions and corrections relative to the page, each disclosed in its item: the printed slips in (2.1) (range of $j$ ), (2.8) (swapped numerators) and Proposition 2(i) (" $\ge0$ " for nonincreasing) are corrected; Claim 2 carries the hypothesis $\varepsilon\le3s'$ , without which the corrected claim is false; Lemma 3 uses strict inequalities $\delta<s<1-\delta$ ; Comment 1 makes the implicit $\lambda>0$ explicit; (2.14) carries Proposition 2's standing range $n\ge2$ , $0<\lambda<\sqrt n$ .

The goal does not mention $p_{\lambda,n}$ , $f_\lambda$ , $C_{\lambda,n}$ , the case split at $n=39$ , or the computer check; a formalization of the goal through those objects, or with the threshold read as a maximum instead of a minimum, would be a different and weaker statement.

Infrastructure a complete development needs: the empirical process of an i.i.d. sample and its reduction to the uniform law by the probability integral transform; Smirnov's exact one-sided law (a ballot-type combinatorial identity); Gaussian-type integrals on $]0,1[$ ; elementary but delicate real inequalities; and certified interval arithmetic for the numerical steps. The first two are reusable for any work on empirical processes. Contributions on any milestone are welcome, in particular formal proofs of (2.3), of the numerical steps, and of the companions.

Selected references

P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Ann. Probab. 18(3):1269–1283, 1990. https://doi.org/10.1214/aop/1176990746
A. Dvoretzky, J. Kiefer, J. Wolfowitz, Asymptotic minimax character of the sample distribution function and of the classical multinomial estimator, Ann. Math. Statist. 27:642–669, 1956. https://doi.org/10.1214/aoms/1177728174
Z. W. Birnbaum, R. C. McCarty, A distribution-free upper confidence bound for P(Y<X), based on independent samples of X and Y, Ann. Math. Statist. 29:558–562, 1958.
N. V. Smirnov, Approximate laws of distribution of random variables from empirical data, Uspekhi Mat. Nauk 10:179–206, 1944.
E. Csáki, Investigations concerning the empirical distribution function, Magyar Tud. Akad. Mat. Fiz. Oszt. Közl. 23:239–327, 1974; English translation in Selected Transl. Math. Statist. Probab. 15:229–317, 1981.
G. R. Shorack, J. A. Wellner, Empirical Processes with Applications to Statistics, Wiley, 1986.

23 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality II: Binomial Tail Bound P(S − np > nε) ≤ exp(−nε²/(2(p + ε/3)(q − ε/3))) for 0 < ε ≤ qResearch Paper

Motivation

Exponential bounds for the tails of the binomial distribution are among the most frequently used tools in probability, statistics and the analysis of algorithms: they control the number of successes in independent trials, the deviation of an empirical frequency from its mean, and, through counting arguments, the empirical distribution function itself. The two classical bounds are Hoeffding's inequality, which ignores the variance, and Bernstein's inequality, which uses the variance $pq$ but loses accuracy for large deviations. Both are recorded in Shorack and Wellner, Empirical Processes with Applications to Statistics (1986), p. 440.

In his 1990 paper establishing the tight constant $2$ in the Dvoretzky–Kiefer–Wolfowitz inequality, P. Massart obtained, as a by-product of the proof, a binomial tail bound that implies both classical inequalities and, in his words, "does not seem to be known" (Massart 1990, p. 1271). Its ingredient, a lower bound for the Cramér transform of the Bernoulli law (Lemma 1), is also used in the proof of the main DKW result. This mission formalizes that by-product: Theorem 2, Lemma 1 and the Cramér–Chernoff bound (Comment 3) through which they are combined.

Setting

Fix an integer $n \ge 0$ and a success probability $p \in [0,1]$ , and write $q = 1 - p$ . A random variable $S$ has the binomial distribution $\mathcal B(n,p)$ if it counts the successes in $n$ independent trials, each succeeding with probability $p$ : $P(S = k) = \binom nk p^k q^{n-k}$ for $k = 0,\dots,n$ . Its mean is $np$ . The quantity of interest is the upper tail $P(S - np > n\varepsilon)$ for a deviation $\varepsilon$ with $0 < \varepsilon \le q$ (for $\varepsilon > q$ the event is empty).

Two auxiliary functions appear in Lemma 1. For $0 < \varepsilon \le q < 1$ (so that $p > 0$ ),

h(p,\varepsilon) = (p+\varepsilon)\log\frac{p+\varepsilon}{p} + (q-\varepsilon)\log\frac{q-\varepsilon}{q},

which is the Cramér transform of the Bernoulli law with parameter $p$ at the point $p + \varepsilon$ , i.e. the relative entropy between the Bernoulli laws with parameters $p+\varepsilon$ and $p$ . For $t \ge 0$ ,

\varphi(t) = t - \frac{t^2}{2(1 + 2t/3)} - \log(1+t).

In the Lean development these are MassartDKW.Binom.h and MassartDKW.Binom.phi.

Formalization targets

Goal: Theorem 2 (p. 1271)

If $S$ has the binomial distribution $\mathcal B(n,p)$ and $q = 1 - p$ , then for every $\varepsilon$ with $0 < \varepsilon \le q$ ,

P(S - np > n\varepsilon) \le \exp\!\left(-\frac{n\varepsilon^2}{2(p+\varepsilon/3)(q-\varepsilon/3)}\right).

Milestones

Lemma 1(i) (p. 1272): $\varphi$ is positive, increasing and convex on $[0,\infty)$ , with $\varphi(t)/t \to 1/4$ as $t \to \infty$ .
Lemma 1(ii) (p. 1272): for $0 < \varepsilon \le q = 1 - p < 1$ and $t = \varepsilon/(q-\varepsilon)$ ,

h(p,\varepsilon) \ge \frac{\varepsilon^2}{2(p+\varepsilon/3)(q-\varepsilon/3)} + \frac{\varepsilon\varphi(t)}{t}.

Comment 3 (p. 1273): for $S \sim \mathcal B(n,p)$ , $P(S - np > n\varepsilon) \le \exp(-n\,h(p,\varepsilon))$ .

Significance

The result. Theorem 2 has the shape of Bernstein's inequality with the variance proxy $pq + \varepsilon/3$ replaced by the smaller $(p+\varepsilon/3)(q-\varepsilon/3)$ ; the second factor shrinks as $\varepsilon$ approaches $q$ , so the bound is sharper in the large-deviation range, and it implies both Bernstein's and Hoeffding's inequalities for binomial tails. Lemma 1(ii) is a quantitative lower bound on the Bernoulli relative entropy, with an explicit nonnegative correction term $\varepsilon\varphi(t)/t$ , which is reusable wherever Chernoff bounds for Bernoulli sums are converted into closed-form exponents. In the paper, the same lemma is a step of the proof of the tight Dvoretzky–Kiefer–Wolfowitz inequality.

Formalizing it. The result is proved on the page, by a short calculus argument for Lemma 1 and the classical Cramér–Chernoff computation for Comment 3. To our knowledge none of the three statements has a machine-checked proof. The work this mission asks for is formalizing that known proof: the analysis of $\varphi$ (signs of derivatives, the limit at infinity), the inequality between $h$ and the explicit quadratic term, the exponential-moment computation for the binomial law in Mathlib's measure-theoretic setting, and the bookkeeping of the boundary cases $\varepsilon = q$ , $p = 0$ and $n = 0$ .

Difficulty

The obvious route to Theorem 2 is to bound the binomial moment generating function and optimize; this reproduces Comment 3, and the exponent it gives is the transcendental function $h(p,\varepsilon)$ , not the rational expression in the theorem. The step that needs care is the comparison of $h$ with $\varepsilon^2/[2(p+\varepsilon/3)(q-\varepsilon/3)]$ uniformly in $0 < \varepsilon \le q$ : a second-order Taylor expansion of $h$ in $\varepsilon$ gives only the local behaviour near $\varepsilon = 0$ , and a bound proved by Taylor expansion alone does not survive up to $\varepsilon = q$ , where the second logarithm of $h$ degenerates and $t = \varepsilon/(q-\varepsilon)$ blows up. The endpoint $\varepsilon = q$ therefore has to be treated as a limit.

Formalization scope

The binomial law is Mathlib's ProbabilityTheory.binomial n p : Measure ℕ with p : unitInterval; $S$ is an $\mathbb N$ -valued map on a probability space $(\Omega, P)$ with HasLaw S (binomial n p) P. Probabilities are values of the measure in $[0,\infty]$ , compared with real bounds through ENNReal.ofReal. The event is the strict upper tail $\{(n:\mathbb R)\varepsilon < S - np\}$ . The goal assumes only $0 < \varepsilon \le 1 - p$ , as on the page: $n = 0$ and $p = 0$ are allowed, and the denominator $2(p+\varepsilon/3)(q-\varepsilon/3)$ is positive on the whole range.

Conventions and added hypotheses ( $q$ is written out as $1 - p$ throughout):

Lean's $\log 0 = 0$ and $x/0 = 0$ : $h$ is only meaningful for $p > 0$ , so Lemma 1(ii) and Comment 3 assume $0 < p$ (the page's $q < 1$ ). The goal does not.
Lemma 1(ii) is stated in two cases. For $\varepsilon < q$ , $t = \varepsilon/(q-\varepsilon)$ is a real number. For $\varepsilon = q$ , $t = \infty$ and the correction term is its limit $\varepsilon/4$ ; reading $t = \varepsilon/0 = 0$ in Lean would give a weaker statement, which is ruled out.
"Positive" in Lemma 1(i) is stated for $t > 0$ , since $\varphi(0) = 0$ ; "increasing" is strict monotonicity on $[0,\infty)$ .

A formalization that states the goal with the exponent $n\,h(p,\varepsilon)$ , or assumes Lemma 1 or Comment 3 as hypotheses, or restricts to $\varepsilon < q$ , is not this theorem: the goal carries the explicit constants and the full range $0 < \varepsilon \le q$ .

Needed infrastructure: elementary real analysis of $\log$ (derivatives, monotonicity from derivative sign, limits at infinity), the moment generating function of the binomial law (or of a sum of independent Bernoulli variables) and Markov's inequality. The bound on the Bernoulli relative entropy and the binomial Chernoff bound are reusable beyond this mission. Contributions welcome: proofs of the three milestones, and helper lemmas computing $\mathbb E[e^{\theta S}] = (q + pe^\theta)^n$ for Mathlib's binomial.

Selected references

P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Annals of Probability 18(3):1269–1283, 1990. https://doi.org/10.1214/aop/1176990746
G. R. Shorack and J. A. Wellner, Empirical Processes with Applications to Statistics, Wiley, 1986 (p. 440: Hoeffding's and Bernstein's inequalities for binomial tails). https://doi.org/10.1137/1.9780898719017
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58:13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830

5 thms2 active usersReviewed

Missions

Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization 3: The Big-M Relaxation Is at Least as Strong as PR(∞) for M ≤ ½√(λ0/λ2) and at Most as Strong for M ≥ √(λ0/λ2)Research Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (p. 7)

Milestones, in the order of the paper's proof

Significance

Difficulty

Formalization scope

Selected references

Information-Theoretic Analysis of Generalization Capability of Learning Algorithms III: The Gibbs Algorithm Has Excess Risk at Most (1/β)log(1/Q(wₒ)) + β/(2n) (Corollary 2)Research Paper

Motivation

Setting

Formalization targets

Gibbs optimization

Expected population risk

Significance

Difficulty

Formalization scope

Selected references

Information-Theoretic Analysis of Generalization Capability of Learning Algorithms I: The Expected Generalization Error Is at Most √(2σ²I(S;W)/n) (Theorem 1)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 4)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization 2: When √(λ0/λ2) > M the Perspective Relaxation Is at Least as Strong as the Big-M and PR(∞) RelaxationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization 1: The Perspective Interval Relaxation Is a Least Squares Problem with a Separable Reverse-Huber or ℓ1 PenaltyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (Reduced Relaxation), p. 6

Milestones (proof of Theorem 1, p. 28)

Significance

Difficulty

Formalization scope

Selected references

Thompson Sampling: An Asymptotically Optimal Finite-Time Analysis: Bernoulli Thompson Sampling Has Regret (1+ε)Σ Δ_a(ln T + ln ln T)/K(μ_a, μ*) + CResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 3)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Nuclear-Norm Penalization and Optimal Rates for Noisy Low-Rank Matrix Completion 3: Uniform Matrix Completion with |Yᵢ| ≤ η — With Probability ≥ 1 − e^{−t} the Oracle Bound (3.5) Holds for All AResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Memory and precision in noiseless Gaussian regressionResearch Paper

Motivation

Background

Setting

Formalization targets

Goal: OAI.NoiselessRegression.main

Milestone: supporting estimates (OAI.MemoryPrecision.main)

Significance

Goal: `OAI.NoiselessRegression.main`

Milestone: supporting estimates (`OAI.MemoryPrecision.main`)