Statistics

Completed

Freedman–Madore 2023: Quantifying the Hubble TensionResearch Paper

Motivation

The Hubble constant $H_0$ is the present expansion rate of the universe. It is the slope of Hubble's law $v = H_0\, d$ , which relates a galaxy's recession velocity $v$ (km s $^{-1}$ ) to its distance $d$ (Mpc). Two families of measurements currently disagree. Local, distance-ladder measurements calibrated with Cepheid variables give $H_0 \approx 73$ km s $^{-1}$ Mpc $^{-1}$ (SH0ES: $73.04 \pm 1.04$ , Riess et al. 2022). The value inferred from the cosmic microwave background under $\Lambda$ CDM is $67.4 \pm 0.5$ (Planck 2018). Calibrations with the tip of the red giant branch (TRGB) fall in between: $69.8 \pm 0.6\,(\text{stat}) \pm 1.6\,(\text{sys})$ (Freedman 2021). This disagreement is the Hubble tension. If it is real, it points to physics beyond $\Lambda$ CDM.

The review Freedman & Madore 2023 surveys this landscape and makes a series of quantitative claims about it. Some are agreement or disagreement claims ("agrees at better than $0.2\sigma$ ", "differs at the $2\sigma$ level"). Others convert magnitudes to distances ("a 1.5% measurement", "corresponds to a 6% shift in $H_0$ "). The central one, in §10, is a sensitivity argument: the claimed $5\sigma$ tension falls below $3\sigma$ if the local uncertainty has been underestimated by a factor of about $1.5$ . This mission takes these claims literally and checks them against their stated numbers.

Setting

A measurement is reported as $x \pm \sigma$ . Two independent uncertainties are combined in quadrature, $\operatorname{quadSum}(s,t) = \sqrt{s^2+t^2}$ . This is the field's standard convention, used here for a quoted $x \pm s\,(\text{stat}) \pm t\,(\text{sys})$ . The tension between independent measurements $a \pm \sigma_a$ and $b \pm \sigma_b$ , in units of standard deviations, is

\operatorname{tension}(a,\sigma_a,b,\sigma_b) = \frac{|a-b|}{\sqrt{\sigma_a^2+\sigma_b^2}}.

The distance modulus of an object at distance $d$ parsecs is $\mu = 5\log_{10}(d/10)$ , and conversely $d = 10^{\mu/5+1}$ pc ( $\operatorname{distanceFromModulus}$ ). A modulus difference $\Delta\mu$ therefore multiplies distances by $10^{\Delta\mu/5}$ . Through Hubble's law, $\operatorname{hubbleConstant}(v,d) = v/(d/10^6)$ (with $d$ in pc), the same difference divides the inferred $H_0$ by $10^{\Delta\mu/5}$ .

Formalization targets

Goal (§10, p. 25)

4.5 \le \operatorname{tension}(73.04, 1.04, 67.4, 0.5) < 5.5,\qquad \operatorname{tension}(72.0, 1.5, 67.4, 0.5) < 3,\qquad 1.5 \le \operatorname{tension}(72.0, 2.0, 67.4, 0.5) < 2.5.

These are the " $5\sigma$ " SH0ES–Planck tension, the "less than $3\sigma$ " for $H_0 = 72.0 \pm 1.5$ , and the " $2\sigma$ " for $H_0 = 72.0 \pm 2.0$ . Every rounded value (" $5\sigma$ ", " $2\sigma$ ") is read as the half-open interval of reals that round to it.

Milestones

Distance modulus and distance are inverse to each other on $d > 0$ .
Hubble's law under a modulus shift: $H_0$ rescales by $10^{-\Delta/5}$ . As consequences, the JWST " $+0.45$ mag farther" correction lowers $H_0$ (Summary, p. 26), and the R16→R22 offset of $-0.123$ mag is a $6\%$ shift (Summary, p. 27).
NGC 4258 (§5.3): modulus $29.397$ is $7.6$ Mpc, and $\pm 0.033$ mag is a $1.5\%$ measurement. The TRGB modulus agrees with the maser modulus at $<0.2\sigma$ and $<1\%$ . The Milky-Way-anchored Cepheid modulus differs by $7\%$ at the $2\sigma$ level.
LMC (§5.1): $18.477 \pm 0.004 \pm 0.026$ is a $1.2\%$ distance uncertainty, $\sim 1\%$ from the Key Project value $18.5$ .
TRGB vs Cepheid (§4.1): $69.8 \pm 0.6 \pm 1.6$ agrees with $73.04 \pm 1.04$ at better than $2\sigma$ .

Significance

The statements make the review's arithmetic exact and auditable. Each verbal claim of the form " $k\sigma$ " or " $p\%$ " becomes an explicit inequality under an explicit convention (quadrature, half-open rounding intervals). A reader can then see which claims follow from the quoted numbers and which do not. For example, under the quadrature convention the §4.1 statement that the TRGB value "differs only at the $1.2\sigma$ level" from Planck evaluates to about $1.35\sigma$ . That claim is therefore not included as a milestone. The definitions (quadrature, tension, distance modulus, Hubble's law) are reusable for any distance-ladder mission. None of these statements has a machine-checked proof yet.

Difficulty

The mathematics is elementary. The difficulty is certified real-number bounds involving square roots and real powers $10^{x}$ with non-integer $x$ , where a careless rounding direction flips a conclusion. Bounds on $10^{p/q}$ reduce to comparing $c^q$ with $10^p$ for large $q$ . This requires care with exponent sizes, or an analytic bound on $\exp$ / $\log$ .

Formalization scope

All quantities are real numbers (ℝ). Distances are in parsecs inside distanceFromModulus, and hubbleConstant converts to Mpc. Velocities are in km s $^{-1}$ . Uncertainties are taken at face value as independent Gaussian standard deviations. Statistical and systematic errors are combined in quadrature, and no asymmetric errors are used. A rounded figure is encoded as the half-open interval of values rounding to it. "Better than $x$ " is a strict inequality. "At the $2\sigma$ level" is $2 \le t < 3$ . Real.logb 10 and Real.sqrt are total functions; every statement uses them only on positive arguments. Solutions should go through the given definitions rather than replacing them with decimal approximations.

Selected references

W. L. Freedman and B. F. Madore, Progress in Direct Measurements of the Hubble Constant, JCAP (2023). https://arxiv.org/abs/2309.05618
A. G. Riess et al., A Comprehensive Measurement of the Local Value of the Hubble Constant with 1 km/s/Mpc Uncertainty from HST and the SH0ES Team, ApJL 934 (2022) L7. https://arxiv.org/abs/2112.04510
Planck Collaboration, Planck 2018 results. VI. Cosmological parameters, A&A 641 (2020) A6. https://arxiv.org/abs/1807.06209
W. L. Freedman, Measurements of the Hubble Constant: Tensions in Perspective, ApJ 919 (2021) 16. https://arxiv.org/abs/2106.15656
M. J. Reid, D. W. Pesce and A. G. Riess, An Improved Distance to NGC 4258 and Its Implications for the Hubble Constant, ApJL 886 (2019) L27. https://arxiv.org/abs/1908.05625

12 thms2 active usersReviewed

Completed

Probability·Captain: Lucas

Zipf's Law: the Zipf Distribution, its Infinite Extension and Related LawsTextbook

Motivation

Zipf's law is the empirical observation that when a set of measured values is sorted in decreasing order, the value of the $n$ -th entry is often approximately inversely proportional to $n$ . Its best-known instance is word frequency in natural language: in the Brown Corpus the most frequent word, "the", accounts for nearly $7\%$ of all word occurrences, the second, "of", for slightly over $3.5\%$ , and so on. The same rank–size relation has been reported for city populations (Auerbach 1913), firm sizes (Axtell 2001), and many other data sets; it is named after the linguist George Kingsley Zipf (1932, 1935, 1949) and remains a central concept of quantitative linguistics (Piantadosi 2014).

In mathematical statistics the law is formalized as the Zipf distribution, a family of discrete probability distributions whose rank–frequency relation is an inverse power law, together with its relatives: the zeta distribution (Lotka's law), the Zipf–Mandelbrot law and the Yule–Simon distribution. Several generative explanations — random typing (Miller 1957, Li 1992) and preferential attachment — produce power laws by provable mechanisms.

Timeline of the results formalized here:

1913–1932 — Auerbach (city sizes), Estoup (1916), Dewey (1923), Condon (1928) and Zipf (1932) observe the inverse rank–frequency relation.
1957 — Miller: a power law emerges in randomly generated texts (doi:10.2307/1419346).
1992 — Li: in random texts with equiprobable letters, word frequency follows Zipf's macro-trend (doi:10.1109/18.165464).

Setting

For a real exponent $s$ and an integer $N \ge 1$ , the generalized harmonic number is

H_{N,s} = \sum_{k=1}^{N}\frac{1}{k^s}, \qquad H_N = H_{N,1}.

The Zipf distribution on $N$ elements with exponent $s$ assigns to the element of rank $k \in\{1,\dots,N\}$ the probability

f(k;N,s) = \frac{1}{H_{N,s}}\,\frac{1}{k^{s}} .

The classical Zipf law is $s=1$ . The source lists the parameter range $s\ge0$ , $N\in\{1,2,3,\dots\}$ .

The Riemann zeta function is $\zeta(s)=\sum_{k\ge1}k^{-s}$ for $s>1$ . The Hurwitz zeta function is $\zeta(s,a)=\sum_{n\ge0}(n+a)^{-s}$ . The Zipf–Mandelbrot law on ranks $k=1,2,\dots$ with shift $q$ and exponent $s$ is $f(k;q,s)=\frac{1}{C}\frac{1}{(k+q)^s}$ with $C=\zeta(s,q+1)$ . The Yule–Simon distribution with parameter $\rho>0$ is $f(k;\rho)=\rho\,B(k,\rho+1)=\rho\,\Gamma(k)\Gamma(\rho+1)/\Gamma(k+\rho+1)$ , $k = 1, 2, \dots$ .

Formalization targets

Goal — the infinite-item extension

For $s \ge 0$ :

\sum_{k\ge1}\frac1{k^s}<\infty \iff s>1;\qquad s>1 \implies H_{N,s}\xrightarrow[N\to\infty]{}\zeta(s);\qquad s\le1 \implies H_{N,s}\xrightarrow[N\to\infty]{}\infty .

That is, the generalized Zipf distribution extends to infinitely many items exactly when $s>1$ , in which case the normalizing constant becomes Riemann's zeta function.

Milestones

Normalization: $\sum_{k=1}^N f(k;N,s)=1$ .
CDF: $\sum_{k=1}^n f(k;N,s)=H_{n,s}/H_{N,s}$ for $n\le N$ .
Mean: $\sum_{k} k\,f(k;N,s)=H_{N,s-1}/H_{N,s}$ .
Variance: $\frac{H_{N,s-2}}{H_{N,s}}-\frac{H_{N,s-1}^2}{H_{N,s}^2}$ .
Entropy: $\frac{s}{H_{N,s}}\sum_{k=1}^N\frac{\ln k}{k^s}+\ln H_{N,s}$ .
Mode: rank $1$ is a most probable element (for $s \ge 0$ ).
Ratio: $f(1;N,s)/f(n;N,s)=n^s$ — "the most common word occurs about $n$ times the $n$ -th most common one" when $s = 1$ .
Log–log linearity: $\ln f(k;N,s) = -s\ln k-\ln H_{N,s}$ , an affine function of $\ln k$ with slope $-s$ .
Zipf–Mandelbrot: with $C=\zeta(s,q+1)$ the law is a probability distribution ( $s>1$ , $q\ge0$ ).
Yule–Simon tail: $f(k;\rho)\sim C/k^{\rho+1}$ for some constant $C>0$ .
Random typing (Li): word probability is bounded above and below by a power of the rank.
Benford connection: the leading digits of a Zipf ( $s=1$ ) random rank follow Benford's law as $N\to\infty$ .

Significance

The goal pins down exactly when "Zipf's law with infinitely many items" makes sense, and identifies the resulting distribution (the zeta distribution) with Riemann's zeta function. The milestones are the infobox facts that statisticians use when fitting Zipf models (CDF, mean, variance, entropy, mode), the log–log diagnostic used to test data against the law, two of the related laws the source lists (Zipf–Mandelbrot, Yule–Simon), one of the generative explanations (random typing), and the stated link to Benford's law.

The results are classical; the work is formalizing them. Most milestones are finite algebra about $H_{N,s}$ ; the goal, the Yule–Simon tail, the random-typing bound and the Benford connection need analysis.

Difficulty

The finite identities are routine once the support conventions are fixed. The analytic content is concentrated in four places. The goal needs the $p$ -series test and the identification of the limit with Mathlib's complex riemannZeta, which is defined by analytic continuation rather than by the series. The Yule–Simon tail needs the asymptotics $\Gamma(k)/\Gamma(k+a)\sim k^{-a}$ . The random-typing bound requires controlling the rank of a word through the number of strictly shorter words, uniformly over every rank order compatible with the probabilities. The Benford connection requires comparing the harmonic sums over each block of integers with a fixed leading digit with $\ln(1+1/d)$ , with an error that is negligible against $H_N\sim\ln N$ .

Formalization scope

$H_{N,s}$ uses a real exponent (Real.rpow); $H_{0,s}=0$ .
zipfPMF N s k is defined for every natural $k$ and is $0$ outside the support $\{1,\dots,N\}$ . Statements that need a nonempty support assume $N\ge1$ .
The goal states convergence to the complex number riemannZeta s of the real partial sums viewed as complex numbers, and divergence as Tendsto … atTop atTop. The source's parameter range $s\ge0$ is kept as a hypothesis.
The Hurwitz zeta function is defined by its series (value $0$ when the series diverges); the Zipf–Mandelbrot law is the infinite-item version on ranks $k\ge1$ , with $q\ge0$ .
The Yule–Simon distribution is defined through the Gamma function; the tail statement asserts existence of a positive constant, matching the source's "[constant]".
Random typing is formalized in Li's equiprobable model: $m\ge2$ letters each typed with probability $q>0$ , a space with probability $1-mq>0$ , and a word $w$ has probability $q^{|w|}(1-mq)$ . "Sorted by rank" means any bijection $e$ from $\mathbb N$ onto the nonempty words along which the probability is non-increasing; the conclusion is a two-sided power-law bound with exponent $\log_m(1/q)$ .
The Benford connection uses the leading decimal digit of the rank $k$ , with $k$ drawn from the Zipf distribution with $s=1$ .
Not formalized: the empirical claims (word, city, income data), the atlas-model result, Belevitch's Taylor-series argument, the parabolic fractal distribution and the Pareto exchange of variables; their statements in the source are not precise enough to formalize faithfully.

Selected references

G. K. Zipf, Human Behavior and the Principle of Least Effort, Addison-Wesley, 1949. https://archive.org/details/in.ernet.dli.2015.90211
E. U. Condon, Statistics of vocabulary, Science 67 (1928), 300. https://doi.org/10.1126/science.67.1733.300
G. A. Miller, Some effects of intermittent silence, American Journal of Psychology 70 (1957), 311–314. https://doi.org/10.2307/1419346
W. Li, Random texts exhibit Zipf's-law-like word frequency distribution, IEEE Trans. Inform. Theory 38 (1992), 1842–1845. https://doi.org/10.1109/18.165464
B. Conrad, M. Mitzenmacher, Power laws for monkeys typing randomly: the case of unequal probabilities, IEEE Trans. Inform. Theory 50 (2004), 1403–1414. https://doi.org/10.1109/TIT.2004.830752
R. L. Axtell, Zipf distribution of U.S. firm sizes, Science 293 (2001), 1818–1820. https://doi.org/10.1126/science.1062081
M. E. J. Newman, Power laws, Pareto distributions and Zipf's law, Contemporary Physics 46 (2005), 323–351. https://arxiv.org/abs/cond-mat/0412004
S. T. Piantadosi, Zipf's word frequency law in natural language: a critical review and future directions, Psychon. Bull. Rev. 21 (2014), 1112–1130. https://doi.org/10.3758/s13423-014-0585-6
Wikipedia, Zipf's law. https://en.wikipedia.org/wiki/Zipf%27s_law

19 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Operations Research·Captain: mikedeng1

Distribution-Free Contextual Dynamic Pricing 2: Every Algorithm Has Expected Regret at Least C₀ C_p T₀ on Some Perturbed Linear Bandit with Perturbation C_pResearch Paper

Motivation

Dynamic pricing asks a seller to post prices to a stream of customers and learn demand from purchase decisions alone. Luo, Sun and Liu study the contextual version in which a customer's valuation is linear in a covariate vector plus noise with an unknown distribution (arXiv:2109.07340v2; Mathematics of Operations Research, 2024). Their DIP policy estimates the linear part, discretizes the remaining price residual, and then runs an upper-confidence-bound rule on the discretized problem. Because the linear part is only estimated, the discretized problem is not an ordinary linear bandit: its reward parameter drifts from period to period by an amount controlled by the estimation error. The paper calls this a perturbed linear bandit (PLB) and proves an upper bound for it whose dominant extra term is linear in the perturbation size times the horizon.

This mission formalizes the matching statement: no algorithm can avoid that linear term. It is the paper's Proposition 2 (p. 22), proved in its Appendix A (pp. 44–46).

Setting

Fix a dimension $d$ . A perturbed linear bandit with perturbation constant $C_p$ consists of parameters $\xi_1,\xi_2,\ldots\in\mathbb R^d$ , finite action sets $\mathcal A_1,\mathcal A_2,\ldots\subset\mathbb R^d$ and noise variables $\eta_1,\eta_2,\ldots$ , with $\|\xi_s-\xi_t\|_\infty\le C_p$ for all periods $s,t$ . In period $t$ an algorithm $\mathcal A^*$ sees the action set $\mathcal A_t$ and the history of its past actions and rewards, plays $A_t\in\mathcal A_t$ , and observes the reward

Z_t=\langle\xi_t,A_t\rangle+\eta_t .

The algorithm may randomize. The parameters $\xi_t$ are never observed.

For a central parameter $\tilde\xi\in\mathbb R^d$ the paper defines the parameter set

PB(\tilde\xi,C_p)=\{\xi\in\mathbb R^d:\ \|\xi-\tilde\xi\|_\infty\le C_p/2\},

so any sequence in $PB(\tilde\xi,C_p)$ has perturbation at most $C_p$ .

The PLB regret over $T_0$ periods compares each action with the best action of the current period:

R^{PLB}_{T_0}(\mathcal A^*)=\sum_{t=1}^{T_0}\Big(\max_{a\in\mathcal A_t}\langle\xi_t,a\rangle-\langle\xi_t,A_t\rangle\Big)\ \ge 0 .

The expectation $\mathbb E$ is over the algorithm's randomness and the noise.

Formalization targets

Goal: Proposition 2 (p. 22)

For every $\tilde\xi$ with positive entries (and $d\ge2$ ) there is $C_0>0$ depending only on $\tilde\xi$ such that for every $C_p\ge0$ with $C_p/2<\min_i\tilde\xi_i$ and every algorithm $\mathcal A^*$ there are parameters $\xi_t\in PB(\tilde\xi,C_p)$ and action sets $\mathcal A_t$ with

\mathbb E\big(R^{PLB}_{T_0}(\mathcal A^*)\big)\ \ge\ C_0\,C_p\,T_0\qquad\text{for all }T_0\ge1 .

The formal statement also records that the constructed instance is a PLB with perturbation $C_p$ , that its action sets are nonempty, and that every action has a single nonzero entry with $|\langle\xi_t,a\rangle|\le1$ , which places the hard instance inside the class covered by the paper's upper bound (Lemma 3, Conditions 1 and 3).

Milestones

Two-point construction (proof of Proposition 2, p. 44). With $C=C_p/2$ , two coordinates $j_u\ne j_v$ , $u=\tilde\xi_{j_u}$ , $v=\tilde\xi_{j_v}$ , actions $U=e_{j_u}/(u+C)$ , $V=e_{j_v}/(v+C)$ and parameters $\xi_u,\xi_v$ obtained from $\tilde\xi$ by moving the two coordinates by $\mp C$ , $\pm C$ :

\xi_u,\xi_v\in PB(\tilde\xi,C_p),\qquad\langle\xi_u,U\rangle=\tfrac{u-C}{u+C}\le1=\langle\xi_v,U\rangle,\qquad\langle\xi_v,V\rangle=\tfrac{v-C}{v+C}\le1=\langle\xi_u,V\rangle .

Per-period bound (pp. 45–46). If $u\le v$ , $A$ is a random action in $\{U,V\}$ , and $\xi_t=\xi_u$ when $P(A=U)\ge1/2$ and $\xi_t=\xi_v$ otherwise, then

\mathbb E(r_t)\ \ge\ C_0C_p,\qquad C_0=\frac1{4v}.

Significance

The result. Lemma 3 of the paper bounds the regret of its M-LinUCB algorithm on a PLB by a $\sqrt{T_0}$ -type term plus $2a_{\max}C_pT_0$ . Proposition 2 shows that the second term is not an artefact of the analysis: an adversary who may move the parameter inside a box of width $C_p$ forces every algorithm to pay order $C_pT_0$ . In the pricing application the perturbation is proportional to the estimation error $\|\hat\theta-\theta_0\|_1$ of the linear part, so the lower bound explains why the paper's pricing regret bound (Theorem 1) carries a term linear in the accumulated estimation error. The result also separates the PLB from the zero-perturbation linear bandit, where $\tilde O(\sqrt{T_0})$ regret is achievable.

Formalizing it. The proposition is proved in the paper; it has not been machine-checked. A formal proof requires an explicit model of randomized, history-dependent algorithms interacting with an adversarially chosen but deterministic parameter sequence, which the mission supplies. The model and the two-point construction are reusable for other two-hypothesis lower bounds in linear and contextual bandits.

Difficulty

The obvious argument fixes one hard instance and shows that every algorithm suffers on it. That fails: for a fixed parameter sequence, an algorithm that always plays the optimal action of that sequence has zero regret. The instance must therefore be chosen after the algorithm, and it must be chosen period by period, because the law of the period- $t$ action depends on the rewards of periods $1,\dots,t-1$ , which depend on the parameters already chosen. The parameters must nevertheless be deterministic: the adversary may react to the law of the algorithm's action, not to its realization. Making this recursive construction precise, together with the measurability needed for "the probability that $A_t=U$ " to be meaningful, is the main formal work. The arithmetic of each period is elementary.

A second point concerns the dimension: the construction needs two distinct coordinates, and for $d=1$ the statement fails, since every parameter in $PB(\tilde\xi,C_p)$ is then positive and playing the largest action has zero regret.

Formalization scope

Model. Arms are coordinates Fin d (0-based); periods are 1-based. Vectors are Fin d → ℝ, and $\|\cdot\|_\infty$ is Mathlib's sup norm on that type. Action sets are finite sets (Finset). The maximum over an empty action set is set to $0$ ; every statement requires nonempty action sets.
Algorithms. An algorithm is a decision rule that maps a sample point $\omega$ of a probability space (its internal randomness), the past actions and rewards, and the current action set to an action of that set; it is jointly measurable in $\omega$ and the history. The trajectory $(A_t,Z_t)$ is defined recursively from the rule, the parameters, the action sets and the noise. Since the rule sees all of $\omega$ , it may also depend on the noise; this only enlarges the class over which the lower bound holds.
Noise. The goal quantifies over every measurable noise process. The paper's PLB asks for conditionally sub-Gaussian noise; since $\eta\equiv0$ is allowed, the formal statement is stronger than the printed existence statement, and the paper's proof uses no property of the noise.
Instance. The parameters and action sets are deterministic and are chosen after the algorithm, the probability space and the noise. The constant $C_0$ is chosen after $\tilde\xi$ and before $C_p$ , the algorithm and $T_0$ , which is the formal content of "only dependent on $\tilde\xi$ ".
Added hypotheses. $d\ge2$ (necessary, see above) and $C_p\ge0$ (otherwise $PB(\tilde\xi,C_p)$ is empty).
Expectation. Expected regret is the lower Lebesgue integral of the nonnegative regret, so no integrability convention can make the bound hold vacuously. The bound is positive whenever $C_p>0$ ; a formalization in which the expectation could collapse to a default value, or the algorithm class could be empty, is ruled out (the class contains every fixed-choice rule).
Source. The source is the arXiv v2 preprint (6 March 2023); the paper's proofs are in its Appendix A.

Contributions welcome: proofs of the two milestones, the measurability of the recursively defined actions, and the summation step from the per-period bound to the goal.

Selected references

Y. Luo, W. W. Sun, Y. Liu, Distribution-Free Contextual Dynamic Pricing, Mathematics of Operations Research, 2024. Preprint arXiv:2109.07340v2; DOI 10.1287/moor.2023.1369.
Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS, 2011. link
T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. doi:10.1017/9781108571401

5 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Solving Chance-Constrained Problems via a Smooth Sample-Based Nonlinear Approximation 1: Smoothed Sample Feasible Sets Lie in the True Feasible Set with Probability ≥ 1 − ⌈1/β⌉⌈2LD/t⌉ⁿ exp(−2NM²)Research Paper

Motivation

A chance-constrained program minimizes a cost $f(x)$ over a closed set $X\subseteq\mathbb R^n$ subject to a constraint that must hold with high probability rather than surely:

\min_{x\in X} f(x)\quad\text{s.t.}\quad \mathbb P\bigl(C(x,\xi)\le 0\bigr)\ge 1-\alpha,

where $\xi$ is a random vector, $C(x,\xi)=\max_j c_j(x,\xi)$ collects the uncertain constraints, and $\alpha\in(0,1)$ is the tolerated risk. Such models are used in power-system dispatch, portfolio selection, and supply-chain and process design, wherever a constraint may be violated in rare scenarios at a controlled rate.

The probability is rarely computable, so in practice it is replaced by an estimate from an i.i.d. sample $\xi_1,\dots,\xi_N$ . The empirical frequency is a step function of $x$ and yields a mixed-integer program. Peña-Ordieres, Luedtke and Wächter (arXiv:1905.07377v2; SIAM J. Optim. 30(3), 2020) replace the indicator by a smooth approximation, which turns the sample problem into a smooth nonlinear program that standard solvers can handle. The question this mission addresses is whether a point accepted by the smoothed sample problem is actually feasible for the true chance constraint, and with what probability.

Timeline. Luedtke and Ahmed (SIAM J. Optim. 19 (2008)) proved finite-sample feasibility guarantees for the empirical (non-smooth) sample approximation, first for finite $X$ and then, under a Lipschitz condition on $C$ , for bounded $X$ (their Theorem 10). Peña-Ordieres, Luedtke and Wächter (2020) extended these guarantees to the smoothed approximation (Theorems 3.8, 3.11 and 3.13 of the preprint).

Setting

Let $\varepsilon>0$ and let $\gamma_\varepsilon:[-\varepsilon,\varepsilon]\to[0,1]$ be admissible: strictly decreasing, symmetric in the sense $\gamma_\varepsilon(-y)=1-\gamma_\varepsilon(y)$ , and such that the smoothed indicator

\Gamma_\varepsilon(y)=\begin{cases}1& y\le-\varepsilon\\ \gamma_\varepsilon(y)&-\varepsilon<y<\varepsilon\\ 0& y\ge\varepsilon\end{cases}

is differentiable on $\mathbb R$ . The paper's concrete choice is a quartic-kernel polynomial (its (2.6)).

For a decision $x$ and a level $t$ , define

the true cdf $F(t;x)=\mathbb P(C(x,\xi)\le t)$ ;
the smoothed cdf $F_\varepsilon(t;x)=\int\Gamma_\varepsilon(C(x,\xi)-t)\,d\mathbb P_\xi$ ;
the smoothed sample cdf $F^N_\varepsilon(t;x)=\frac1N\sum_{i=1}^N\Gamma_\varepsilon(C(x,\xi_i)-t)$ .

The true feasible set is $X_\alpha=\{x\in X\mid F(0;x)\ge1-\alpha\}$ , and the shifted sample feasible set with shift $t$ and sample risk level $\delta$ is

X^{N,t}_{\varepsilon,\delta}=\{x\in X\mid F^N_\varepsilon(-t;x)\ge 1-\delta\}.

Throughout, $C(x,\xi)$ has a continuous distribution for each $x\in X$ (Assumption 3.1). The margin of a point is $M_x=F(0;x)-F_\varepsilon(-t;x)+(\alpha-\delta)$ ; Assumption 3.7 asks that $\delta\in[0,\alpha]$ and $M:=\inf_{x\in X}M_x>0$ .

Formalization targets

Goal: Theorem 3.13

Suppose $X$ is bounded with sup-norm diameter $D$ , that $|C(x,\xi)-C(y,\xi)|\le L\|x-y\|_\infty$ for all $x,y\in X$ with probability one (Assumption 3.12), and that Assumption 3.7 holds with $t>0$ and $\delta>0$ . Then for every $\beta\in(0,\delta]$ ,

\mathbb P\bigl(X^{N,2t}_{\varepsilon,(\delta-\beta)}\subseteq X_\alpha\bigr)\ge 1-\lceil1/\beta\rceil\,\lceil 2LD/t\rceil^n\exp\{-2NM^2\}.

Milestones

Theorem 3.8. For $x\in X\setminus X_\alpha$ , $\ \mathbb P(F^N_\varepsilon(-t;x)\ge1-\delta)\le\exp\{-2NM_x^2\}$ .
Theorem 3.11. For finite $X$ , $\ \mathbb P(X^{N,t}_{\varepsilon,\delta}\subseteq X_\alpha)\ge 1-|X\setminus X_\alpha|\exp\{-2NM^2\}$ .
The net claim (proof of Theorem 3.13). Each slice $X_j$ of $X$ by the value of $F(0;\cdot)$ at resolution $1/\lceil1/\beta\rceil$ has a finite subset $Z_j$ with $|Z_j|\le\lceil2LD/t\rceil^n$ that is a $t/L$ -net of $X_j$ in $\|\cdot\|_\infty$ .
(3.5). Theorem 3.11 applied to the net $Z$ with levels $\alpha-\beta$ and $\delta-\beta$ .
The transfer step. $x\in X^{N,2t}_{\varepsilon,(\delta-\beta)}$ and $\|x-z\|_\infty\le t/L$ imply $F^N_\varepsilon(-t;z)\ge1-\delta+\beta$ .
Corollary 3.9 (companion). If $C(x,\xi)$ has a density strictly decreasing on $(-\varepsilon,\varepsilon)$ and $F(0;x)<1-\alpha$ , then $\beta_x=F(0;x)-F_\varepsilon(0;x)>0$ and $\mathbb P(F^N_\varepsilon(0;x)\ge1-\alpha)\le\exp\{-2N\beta_x^2\}$ .

Significance

The result. Theorem 3.13 gives an explicit, non-asymptotic sample size $N$ under which every point accepted by the smoothed sample problem (with a small shift $2t$ and a slightly tightened risk level $\delta-\beta$ ) is feasible for the original chance constraint, uniformly over an infinite decision set. Solving the smooth approximation therefore yields certifiably feasible solutions with a quantified failure probability, the bound depending on the dimension $n$ only through the covering number $\lceil 2LD/t\rceil^n$ . Corollary 3.9 adds that, under a monotone density near zero, the unshifted smoothed approximation is conservative.

Formalizing it. The results are proved in the paper; none is formalized anywhere to our knowledge. A formal development would produce a machine-checked one-sided Hoeffding bound for averages of bounded functions of an i.i.d. sample, a union bound over a finite candidate set, and a sup-norm covering lemma, assembled into a uniform feasibility guarantee. These ingredients are reused across the sample-average-approximation literature.

Difficulty

The obvious argument is a union bound over $X$ , which fails for infinite $X$ : the event $X^{N,2t}_{\varepsilon,(\delta-\beta)}\subseteq X_\alpha$ involves uncountably many points, and is not even obviously measurable. Discretizing $X$ by a sup-norm grid is not enough on its own either: a grid point may be infeasible while nearby points are feasible, and the true cdf $F(0;\cdot)$ need not be continuous in $x$ . The paper's device is to discretize simultaneously in $x$ and in the value of $F(0;x)$ , which requires covering each level slice separately and then transferring sample feasibility from a point to its representative, at the price of the shift $2t\to t$ and the level change $\delta\to\delta-\beta$ . Keeping the constants exactly as printed, with $\lceil1/\beta\rceil$ slices and $\lceil 2LD/t\rceil^n$ points per slice, is part of the task.

Formalization scope

Decisions are Fin n → ℝ, whose Mathlib norm is the sup norm $\|\cdot\|_\infty$ used in Assumption 3.12 and Theorem 3.13. $X$ is closed (the paper's standing hypothesis).
$\xi$ takes values in a measurable space $\Xi$ with probability law $\mathbb P_\xi$ . The sample is $N\ge1$ measurable maps $\xi_i:\Omega\to\Xi$ on a probability space, mutually independent, each with law $\mathbb P_\xi$ . $C(x,\cdot)$ is assumed measurable for $x\in X$ (a disclosed addition: it makes $C(x,\xi)$ a random variable). Assumption 3.1 is encoded as $\mathbb P_\xi(C(x,\xi)=y)=0$ for all $y$ .
Statements of the form " $\mathbb P(A)\ge1-b$ " are stated as $\mathbb P(\text{not }A)\le b$ with $\mathbb P$ evaluated as an outer measure; this implies the printed form and assumes no measurability of the event.
Assumption 3.7's infimum $M$ is a parameter with $M>0$ and $M\le M_x$ on $X$ , equivalent to the infimum because the bounds decrease in $M$ .
"Bounded with diameter $D$ " is $\|x-y\|_\infty\le D$ on $X$ with $D>0$ . Positivity is necessary: for a single infeasible point and $n\ge1$ the printed bound with $D=0$ would read $\mathbb P\ge1$ .
A formalization in which these hypotheses are unsatisfiable, the event is assumed measurable, or $M$ is a junk infimum is ruled out: a sorry-free sanity file exhibits the quartic kernel (2.6) as admissible and a one-point instance meeting the goal's diameter and margin hypotheses.
Not posed: Hoeffding's inequality (Theorem 3.6), whose one-sided form is in Mathlib (ProbabilityTheory.measure_sum_ge_le_of_iIndepFun with hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero); and Corollary 3.10, whose printed exponent does not follow from its proof.

Contributions welcome: proofs of any milestone, in particular the sup-norm covering lemma and the Hoeffding step, which are reusable beyond this mission.

Selected references

A. Peña-Ordieres, J. R. Luedtke, A. Wächter, Solving chance-constrained problems via a smooth sample-based nonlinear approximation, SIAM J. Optim. 30(3), 2020; preprint arXiv:1905.07377v2. https://arxiv.org/abs/1905.07377 , https://doi.org/10.1137/19M1261985
J. Luedtke, S. Ahmed, A sample approximation approach for optimization with probabilistic constraints, SIAM J. Optim. 19(2), 2008. https://doi.org/10.1137/070702928
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 1963. https://doi.org/10.1080/01621459.1963.10500830

8 thms2 active usersReviewed

Machine Learning Operations Research Optimal Transport·Captain: mikedeng1

Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality 3: Under T₂(τ), W₂-Robust Loss at Radius ρ̃ₙ Bounds True Loss up to 4r⋆+2εₙ+ħρ̃ₙ²Research Paper

Motivation

Wasserstein distributionally robust optimization (Wasserstein DRO) replaces the empirical loss $\mathbb E_{\mathbb P_n}[f]$ of a decision by its worst case over all distributions within Wasserstein distance $\rho$ of the empirical distribution $\mathbb P_n$ . It is used in operations research (newsvendor, portfolio selection) and machine learning (adversarially robust training, regularized regression) because the robust loss is a computable upper estimate of the unknown true loss. The question every user faces is how large $\rho$ must be. Measure-concentration results for the empirical measure in Wasserstein distance (Fournier and Guillin, 2015) require $\rho\sim n^{-1/d}$ on a $d$ -dimensional space, which is useless in high dimension.

Gao (arXiv:2009.04382, Operations Research 2023) shows that a radius of order $1/\sqrt n$ suffices, with no dependence on dimension, as long as the true distribution satisfies a transportation-information inequality and the loss class has controlled complexity. This mission covers the paper's result for the 2-Wasserstein distance, where the robust loss is linked to gradient regularization. Two sibling missions cover the variation-concentration inequality (Theorem 1) and the 1-Wasserstein / Lipschitz case (Corollary 4).

Setting

$\mathcal Z$ is a separable real Banach space with norm $\|\cdot\|$ and dual norm $\|\cdot\|_*$ . $\mathcal P_2(\mathcal Z)$ is the set of Borel probability measures with finite second moment, and $\mathcal W_2$ is the 2-Wasserstein distance: $\mathcal W_2(\mathbb P,\mathbb Q)^2$ is the infimum of $\mathbb E_\pi\|\tilde z-z\|^2$ over couplings $\pi$ of $\mathbb P$ and $\mathbb Q$ .

The Wasserstein regularizer of a loss $f$ at a nominal distribution $\mathbb Q$ and radius $\rho\ge0$ is

\mathcal R_{\mathbb Q,2}(\rho;f)=\sup\{\mathbb E_{\mathbb P}[f]:\mathbb P\in\mathcal P_2(\mathcal Z),\ \mathcal W_2(\mathbb P,\mathbb Q)\le\rho\}-\mathbb E_{\mathbb Q}[f].

A distribution $\mathbb P$ satisfies the transportation-information inequality $T_2(\tau)$ if $\mathcal W_2(\mathbb Q,\mathbb P)\le\sqrt{\tau H(\mathbb Q\|\mathbb P)}$ for every $\mathbb Q\in\mathcal P_2(\mathcal Z)$ , with $H$ the relative entropy. Gaussian measures are the standard example.
A class $\mathcal F$ of losses satisfies Assumption 2 with constant $\hbar>0$ if each $f\in\mathcal F$ is differentiable and $\|\nabla f(\tilde z)-\nabla f(z)\|_*\le\hbar\|\tilde z-z\|$ .
The gradient norm of $f$ under $\mathbb Q$ is $\|\|\nabla f\|_*\|_{\mathbb Q,2}=(\mathbb E_{\mathbb Q}\|\nabla f\|_*^2)^{1/2}$ .
A sample $z_1,\dots,z_n$ is i.i.d. from $\mathbb P_{\mathrm{true}}$ , and $\mathbb E_\otimes$ is expectation over it. The Rademacher complexity of a class $\mathcal H$ is $\mathbb E_\otimes[\mathfrak R_n(\mathcal H)]$ , with $\mathfrak R_n(\mathcal H)=\mathbb E_\sigma\sup_{h\in\mathcal H}\frac1n\sum_i\sigma_ih(z_i)$ and $\sigma_i$ independent uniform signs.
The normalized gradient class is $\mathcal G=\{\|\nabla f\|_*^2/\|\|\nabla f\|_*\|^2_{\mathbb P_{\mathrm{true}},2}:f\in\mathcal F\}$ .
Assumption 5 asks for a sub-root function $\psi_n$ (non-negative, non-decreasing, non-constant, with $\psi_n(r)/\sqrt r$ non-increasing) that dominates the localized complexities $\mathbb E_\otimes[\mathfrak R_n(\{cf:f\in\mathcal F,0\le c\le1,c^2\|\|\nabla f\|_*\|^2_{\mathbb P_{\mathrm{true}},2}\le r\})]$ . Its positive fixed point is $r_{n\star}$ .

In Lean the mission's own objects live in the namespace WassFSG.Grad: W2sq, IsP2, regularizer, IsT2, GradLipBound, gradNorm, empGradNorm, gradClass, localized, SubRootLocalComplexity, productRegularizer, epsN, rhoN and rhoTilde. The empirical mean and measure (empMean, empMeasure), the Rademacher complexity (radComp, expectedRad), sub-root functions (IsSubRoot), the class −F (negClass) and the probability count (peelCount) are the shared definitions of the series in WassFSG.Lip.

Formalization targets

Goal: Corollary 6 (2-Wasserstein DRO), pp. 11–12

Write $\epsilon_n=(\hbar\tau t+1+\mathbb E_\otimes[\mathfrak R_n(\mathcal G)])/n$ and $\rho_n=2\sqrt{\tau t/n}\,(1+\mathbb E_\otimes[\mathfrak R_n(\mathcal G)])+\sqrt{4r_{n\star}+2\epsilon_n}$ . Assume in addition that $\|\nabla f(z)\|_*/\|\|\nabla f\|_*\|_{\mathbb P_{\mathrm{true}},2}\le\kappa_g$ , and set $\tilde\rho_n=\rho_n(1+2\mathbb E_\otimes[\mathfrak R_n(\mathcal G)]+\kappa_g^2\sqrt{t/(2n)})$ . If $2\mathbb E_\otimes[\mathfrak R_n(\mathcal G)]+\kappa_g^2\sqrt{t/(2n)}<1/2$ , then with probability at least $1-(N_2+1)e^{-t}$ , every $f\in\mathcal F$ satisfies

\mathbb E_{\mathbb P_{\mathrm{true}}}[f]\le\mathbb E_{\mathbb P_n}[f]+\tilde\rho_n\|\|\nabla f\|_*\|_{\mathbb P_n,2}+4r_{n\star}+2\epsilon_n

and

\mathbb E_{\mathbb P_{\mathrm{true}}}[f]\le\mathbb E_{\mathbb P_n}[f]+\mathcal R_{\mathbb P_n,2}(\tilde\rho_n;f)+4r_{n\star}+2\epsilon_n+\hbar\tilde\rho_n^2,

where $N_2=\max(0,\lceil\log_2(\gamma_2\sqrt{\tau tn})\rceil)+1$ .

Milestones, in proof order

Lemma 7 (symmetrization).
Lemma 9 for $p=2$ : a uniform deviation bound with the transport term $\mathcal R_{\otimes,2}(\sqrt{\tau t/n};-\mathcal F)$ .
Lemma 13: the transport term is bounded by gradient norms plus $\hbar\tau t/n$ .
Lemma 14: peeling, which turns the class supremum into each $f$ 's own gradient norm.
Lemma 10: the fixed-point bound $B^2\le r_0\le2A+B^2$ .
Theorem 3: distribution-dependent gradient regularization, $\mathbb E_{\mathbb P_{\mathrm{true}}}[f]\le\mathbb E_{\mathbb P_n}[f]+\rho_n\|\|\nabla f\|_*\|_{\mathbb P_{\mathrm{true}},2}+4r_{n\star}+2\epsilon_n$ .
Lemma 2: $|\mathcal R_{\mathbb Q,2}(\rho;f)-\rho\|\|\nabla f\|_*\|_{\mathbb Q,2}|\le\hbar\rho^2$ .

Significance

Corollary 6 says that solving 2-Wasserstein DRO at a radius $\tilde\rho_n=O(1/\sqrt n)$ gives, with high probability, an upper bound on the true loss of every decision, up to an $O(1/n)$ gap. This holds whenever $\mathbb E_\otimes[\mathfrak R_n(\mathcal G)]=O(1)$ and $r_{n\star}=O(1/n)$ , for example for finite-VC gradient classes, smooth neural networks and Markowitz portfolios (Section 5 of the paper). Combined with the robust-solution argument of Remark 1, this gives $\tilde O(1/\sqrt n)$ excess-risk bounds for the robust solution. Theorem 3 alone is a generalization bound for gradient-norm regularization, an estimator used in its own right.

None of these results is known to be machine-checked. The mission produces a Lean statement of the full chain from a transportation inequality to the DRO guarantee. It also produces reusable infrastructure: the 2-Wasserstein regularizer on a Banach space, transportation-information inequalities, local Rademacher complexities with sub-root bounds, and a peeling argument. The printed failure probability needs a correction (see below), so the formal statement is itself a contribution.

Difficulty

The obvious route is to bound $\mathbb E_{\mathbb P_{\mathrm{true}}}[f]-\mathbb E_{\mathbb P_n}[f]$ by $\mathcal W_2(\mathbb P_n,\mathbb P_{\mathrm{true}})$ times a gradient bound. It fails because $\mathcal W_2(\mathbb P_n,\mathbb P_{\mathrm{true}})$ decays like $n^{-1/d}$ . The radius must instead come from concentration of the loss, and the result has to hold uniformly over $\mathcal F$ , which requires symmetrization and a localization in the gradient norm.

Three points carry the weight:

The transport term of Lemma 9 has to be converted into a gradient norm with a quadratic remainder. This is the step that uses smoothness.
The population gradient norm, which is unknown, has to be replaced by its empirical counterpart in Corollary 6. This needs a separate concentration step for the class $\mathcal G$ .
Every constant (the $(1+\mathbb E_\otimes[\mathfrak R_n(\mathcal G)])$ factors, $\epsilon_n$ , $\tilde\rho_n$ ) appears in the statement and must come out exactly.

Formalization scope

The source is arXiv:2009.04382 (preprint basis); its printed page numbers equal the PDF's.

Standing conventions:

$\mathcal Z$ is a complete, second-countable real normed space with its Borel $\sigma$ -algebra. The paper says "Banach space"; separability and Borel are the setting of the transport results it cites.
$n\ge1$ .
$\nabla f$ is the Fréchet derivative, and its norm is the operator (dual) norm.
$\mathcal W_2$ is used through its square, via the published optimal-transport cost.
Expectations inside the regularizer and Rademacher complexities are extended integrals in $\overline{\mathbb R}$ . $\mathbb E_{\mathbb P_{\mathrm{true}}}[f]$ is the Bochner integral, which is integrable because Assumption 2 gives quadratic growth and $T_2(\tau)$ a finite second moment.
"With probability at least $1-\delta$ , for every $f$ " is the outer measure of the set of samples where some $f$ fails, bounded by $\delta$ .
The page's $\min_{\lambda\ge0}$ in $\mathcal R_{\otimes,2}$ is read as an infimum.

Added hypotheses, all implicit on the page:

$\|\|\nabla f\|_*\|_{\mathbb P_{\mathrm{true}},2}>0$ for $f\in\mathcal F$ , so that $\mathcal G$ and $\kappa_g$ are defined.
$\mathbb E_\otimes[\mathfrak R_n(\mathcal G)]$ is finite. It is passed as a real number; if it is infinite, the bounds are vacuous.
The class bound $\gamma_2$ in Lemma 14, which its proof uses.
$r_{n\star}>0$ .
Continuity and integrability of the family in Lemma 7.

Corrected slip. The printed failure probability $\lceil\log_2(\sqrt{\gamma_2\tau tn})\rceil e^{-t}$ (Theorem 3, Corollary 6) is negative for small $\gamma_2\sqrt{\tau tn}$ and disagrees with Lemma 14, and the peeling in Lemma 14's proof misses one band. The Lean uses $N_2=\max(0,\lceil\log_2(\gamma_2\sqrt{\tau tn})\rceil)+1$ events (and $N_2+1$ in Corollary 6). Milestone texts keep the printed count. Lemma 13's printed proof contains a step that is false in general for signed Rademacher sums. The statement is posed as printed; a correct argument uses the non-negativity of $\mathcal G$ .

Ruled out. A trivializing encoding would take $r_{n\star}=0$ , let the radii be free existentials, use a real supremum (which is $0$ on unbounded sets), or rely on Lean's $x/0=0$ for $\mathcal G$ . None of these is used: every radius is the printed formula, and each degenerate case is excluded by a hypothesis.

Welcome contributions include proofs of the milestones and general lemmas on the Wasserstein regularizer (Lemma 2 is a first-order expansion). McDiarmid's inequality, which Corollary 6's proof uses, is not a milestone and is a welcome general-purpose result.

Selected references

R. Gao, Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality, Operations Research, 2023. arXiv:2009.04382
P. L. Bartlett, O. Bousquet, S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. doi:10.1214/009053605000000282
N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162, 2015. doi:10.1007/s00440-014-0583-7
R. Gao, X. Chen, A. J. Kleywegt, Wasserstein distributionally robust optimization and variation regularization, Operations Research, 2024. arXiv:1712.06050
N. Gozlan, C. Léonard, Transport inequalities. A survey, Markov Processes and Related Fields 16, 2010. arXiv:1003.3852

14 thms2 active usersReviewed

Machine Learning Operations Research Optimal Transport·Captain: mikedeng1

Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality 2: Under T₁(τ), W₁-Robust Loss at Radius 2√(τt/n)+√(4r⋆+2/n) Bounds the True LossResearch Paper

Why the radius of a Wasserstein ball matters

Wasserstein distributionally robust optimization (DRO) replaces the empirical loss $\mathbb E_{\mathbb P_n}[f]$ of a decision or model $f$ by its worst case over all distributions within a Wasserstein distance $\rho$ of the empirical distribution $\mathbb P_n$ . It is used in operations research (newsvendor, portfolio and inventory problems) and in machine learning (robust classification and regression), and it is attractive because the worst-case loss is often a computable convex program (Mohajerin Esfahani and Kuhn 2018; Gao and Kleywegt 2023).

The practical question is how large $\rho$ must be for the robust loss to upper-bound the true, unknown loss $\mathbb E_{\mathbb P_{\mathrm{true}}}[f]$ with high probability. The classical answer goes through measure concentration of $\mathbb P_n$ around $\mathbb P_{\mathrm{true}}$ in Wasserstein distance (Fournier and Guillin 2015), which forces $\rho_n \asymp n^{-1/d}$ in dimension $d$ : the curse of dimensionality. Rui Gao's paper (arXiv:2009.04382; Operations Research, 2023) shows that a radius of order $n^{-1/2}$ suffices, independently of $d$ , under a transportation-information inequality and a complexity assumption on the loss class. This mission formalizes the paper's result for the 1-Wasserstein distance (Sec. 4.2, Theorem 2 and Corollary 4).

Setting

Let $\mathcal Z$ be a separable real Banach space with norm $\|\cdot\|$ . $\mathcal P_1(\mathcal Z)$ is the set of Borel probability measures $\mathbb Q$ with $\mathbb E_{\mathbb Q}\|z\|<\infty$ . The 1-Wasserstein distance is

\mathcal W_1(\mathbb P,\mathbb Q)=\inf\{\mathbb E_\pi\|\tilde z-z\| : \pi \text{ has marginals }\mathbb P,\mathbb Q\}.

For a loss $f:\mathcal Z\to\mathbb R$ the Wasserstein regularizer is the gap between robust and nominal loss,

\mathcal R_{\mathbb Q,1}(\rho;f)=\sup\{\mathbb E_{\mathbb P}[f]:\mathbb P\in\mathcal P_1(\mathcal Z),\ \mathcal W_1(\mathbb P,\mathbb Q)\le\rho\}-\mathbb E_{\mathbb Q}[f].

The Lipschitz norm $\|f\|_{\mathrm{Lip}}$ is the best Lipschitz constant of $f$ .

The data are $n$ i.i.d. samples $z_1,\dots,z_n$ from $\mathbb P_{\mathrm{true}}$ , with empirical distribution $\mathbb P_n=\frac1n\sum_i\delta_{z_i}$ . $\mathbb P_\otimes$ and $\mathbb E_\otimes$ refer to the product law. The distribution $\mathbb P_{\mathrm{true}}$ satisfies the transportation-information inequality $T_1(\tau)$ if $\mathcal W_1(\mathbb Q,\mathbb P_{\mathrm{true}})\le\sqrt{\tau H(\mathbb Q\|\mathbb P_{\mathrm{true}})}$ for every $\mathbb Q\in\mathcal P_1(\mathcal Z)$ , where $H$ is relative entropy. It holds, for example, for every distribution with a sub-Gaussian norm.

The loss class $\mathcal F$ satisfies Assumption 1(I) if $f(\tilde z)-f(z)\le\gamma_1\|\tilde z-z\|$ for all $f\in\mathcal F$ , with $\gamma_1>0$ . It satisfies Assumption 1(II) if $\mathcal Z$ is unbounded and each $f$ attains its Lipschitz norm at infinity, i.e. $\limsup_{\|z-z_0\|\to\infty}(f(z)-f(z_0))/\|z-z_0\|=\|f\|_{\mathrm{Lip}}$ for some $z_0$ .

The Rademacher complexity of a class $\mathcal G$ on the sample is $\mathfrak R_n(\mathcal G)=\mathbb E_\sigma[\sup_{g\in\mathcal G}\frac1n\sum_i\sigma_i g(z_i)]$ , with i.i.d. uniform signs $\sigma_i$ . Assumption 5 asks for a sub-root function $\psi_n$ that dominates the localized complexities:

\psi_n(r)\ge\mathbb E_\otimes\big[\mathfrak R_n(\{cf:f\in\mathcal F,\ 0\le c\le1,\ \|cf\|^2_{\mathrm{Lip}}\le r\})\big].

Sub-root means non-negative, non-decreasing, non-constant, with $\psi_n(r)/\sqrt r$ non-increasing. Its positive fixed point is $r_{n\star}=\psi_n(r_{n\star})$ .

Formalization targets

Goal: Corollary 4 (1-Wasserstein DRO)

Set $\rho_n=2\sqrt{\tau t/n}+\sqrt{4r_{n\star}+2/n}$ and $N_1(t,n)=\max(0,\lceil\log_2(\gamma_1\sqrt{\tau tn})\rceil)+1$ . Under $T_1(\tau)$ , Assumption 1 and Assumption 5, for $t>0$ , with probability at least $1-N_1(t,n)e^{-t}$ ,

\mathbb E_{\mathbb P_{\mathrm{true}}}[f]\le\mathbb E_{\mathbb P_n}[f]+\mathcal R_{\mathbb P_n,1}(\rho_n;f)+4r_{n\star}+\frac2n\qquad\forall f\in\mathcal F.

Milestones

Lemma 7 (symmetrization): $\mathbb E_\otimes\sup_h\{\mathbb E_{\mathbb P_{\mathrm{true}}}h-\mathbb E_{\mathbb P_n}h\}\le2\mathbb E_\otimes[\mathfrak R_n(\mathcal H)]$ .
Lemma 9 ( $p=1$ ): uniform concentration with the product regularizer $\mathcal R_{\otimes,1}(\sqrt{\tau t/n};-\mathcal F)$ .
Lemma 11: the same with $\sqrt{\tau t/n}\sup_{f\in\mathcal F}\|f\|_{\mathrm{Lip}}$ .
Lemma 12 (peeling): each $f$ 's own $2\sqrt{\tau t/n}\|f\|_{\mathrm{Lip}}$ , at cost $1/n$ and $N_1$ events.
Lemma 10: the largest root $r_0$ of $B\sqrt r+A=r$ lies in $[B^2,2A+B^2]$ .
Theorem 2 (Lipschitz regularization): the goal with $\mathcal R_{\mathbb P_n,1}(\rho_n;f)$ replaced by $\rho_n\|f\|_{\mathrm{Lip}}$ ; needs Assumption 1(I) only.
Lemma 1: $\mathcal R_{\mathbb Q,1}(\rho;f)\le\rho\|f\|_{\mathrm{Lip}}$ , with equality under Assumption 1(II).

Significance

Corollary 4 justifies a radius of order $1/\sqrt n$ whenever $r_{n\star}=\tilde O(1/n)$ , which the paper verifies for kernel classes and other examples (Sec. 5). That rate is the one used in practice, and it was not covered by the concentration-based theory. Theorem 2 is a dimension-free generalization bound for Lipschitz-regularized learning in its own right. Lemma 1 links the two by identifying the 1-Wasserstein regularizer with Lipschitz regularization.

The results are proved in the paper. As far as known, none of them is machine-checked. A formalization would check the paper's peeling and fixed-point arguments, which turn out to need a corrected failure-probability count (see Formalization scope). It would also produce reusable Lean infrastructure: Rademacher complexity in the $\frac1n$ , no-absolute-value normalization, localized classes, sub-root functions, $T_1(\tau)$ , and the Wasserstein regularizer on a Banach space.

Difficulty

The obvious route bounds $\mathcal W_1(\mathbb P_n,\mathbb P_{\mathrm{true}})$ and uses Kantorovich–Rubinstein duality. It fails because $\mathcal W_1(\mathbb P_n,\mathbb P_{\mathrm{true}})$ is of order $n^{-1/d}$ , so no dimension-free radius comes out. A dimension-free bound must therefore hold uniformly over an infinite loss class without passing through the distance between $\mathbb P_n$ and $\mathbb P_{\mathrm{true}}$ , and the bound must scale with each function's own Lipschitz norm rather than the class-wide constant $\gamma_1$ . The statements also need measure-theoretic infrastructure that Mathlib lacks or has only partly: transport inequalities, Rademacher averages over classes, and suprema of uncountable families inside expectations.

Formalization scope

Space. $\mathcal Z$ is a real Banach space with its Borel $\sigma$ -algebra, and second countable (separable). The paper says "Banach space"; Borel and separability are implicit in the transport and duality results it cites. The Borel structure is load-bearing for transport costs.
Distances and expectations. $\mathcal W_1$ is the published RWPI.SqrtLasso.transportCost with cost $\|u-w\|$ . Expectations inside regularizers and complexities are extended integrals $\int\varphi^+-\int\varphi^-$ in $[-\infty,\infty]$ (published ModelRiskOT.Duality.extIntegral). $\mathbb E_{\mathbb P_{\mathrm{true}}}[f]$ is the Bochner integral; it is the true expectation because a Lipschitz $f$ is integrable under $\mathbb P_{\mathrm{true}}\in\mathcal P_1$ . Relative entropy is Mathlib's klDiv.
High-probability statements. "With probability at least $1-\delta$ , for every $f\in\mathcal F$ " is the bound $\mathbb P_\otimes\{z:\exists f\in\mathcal F\text{ violating the bound}\}\le\delta$ in outer measure, so the quantifier over $f$ sits inside the event. $\mathcal R_{\mathbb P_n,1}$ uses the empirical distribution of the same sample.
Samples and constants. $n\ge1$ . $r_{n\star}>0$ is a positive fixed point of $\psi_n$ ; taking $r_{n\star}=0$ when $\psi_n(0)=0$ would trivialize the goal and is excluded. $\rho_n$ is the printed formula, not a free radius. Assumption 1(II)'s $\operatorname{diam}(\mathcal Z)=\infty$ is stated as " $\mathcal Z$ is unbounded".
Corrected probability count. The paper prints the failure probability of Lemma 12, Theorem 2 and Corollary 4 as $\lceil\log_2(\sqrt{\gamma_1\tau tn})\rceil e^{-t}$ . That count is negative when $\gamma_1\sqrt{\tau tn}\le1/2$ , which makes the printed claim false. It also puts $\gamma_1$ inside the root, against the proof's own choice of $K$ , and the proof's peeling shells leave a band of Lipschitz norms uncovered. All three statements use the corrected count $N_1(t,n)$ .
Other readings. $\mathcal R_{\otimes,1}$ uses an infimum where the page writes $\min$ . Lemma 9 is stated for $p=1$ only. In Lemma 7 the family consists of continuous, $\mathbb P_{\mathrm{true}}$ -integrable functions. Continuity makes every supremum inside an expectation lower semicontinuous, hence measurable, and the same holds automatically for the Lipschitz classes of the other statements.

Lemma 5 (concentration on the product space under $T_p(\tau)$ , used in Lemma 9's proof) belongs to the companion mission on variation-based concentration and is not restated here. Contributions are welcome at every level: sub-root fixed-point facts, symmetrization, the peeling lemma, and Lemma 1's two directions are independent entry points.

The source is arXiv:2009.04382; its printed page numbers equal the PDF's page numbers.

Selected references

R. Gao, Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality, Operations Research, 2023. https://arxiv.org/abs/2009.04382
P. L. Bartlett, O. Bousquet, S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
R. Gao, X. Chen, A. J. Kleywegt, Wasserstein distributionally robust optimization and variation regularization, Operations Research, 2024. https://arxiv.org/abs/1712.06050
P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162, 2015. https://doi.org/10.1007/s00440-014-0583-7
N. Gozlan, C. Léonard, Transport inequalities. A survey, Markov Processes and Related Fields 16, 2010. https://arxiv.org/abs/1003.3852

12 thms2 active usersReviewed

Optimal Transport Probability·Captain: mikedeng1

Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality 1: Under T_p(τ), True Loss ≤ Empirical Loss + R(√(τt/n); −f) w.p. ≥ 1 − e^(−t)Research Paper

Motivation

Wasserstein distributionally robust optimization (Wasserstein DRO) replaces the expected loss under an empirical distribution by the worst-case expected loss over all distributions within a Wasserstein distance $\rho$ of it. It is used in operations research, statistics and machine learning to guard decisions and predictors against the gap between the sample and the population. The statistical question it raises is how large $\rho$ must be for the robust loss to bound the true loss with high probability. Classical answers go through the concentration of the empirical measure in Wasserstein distance, which forces $\rho\asymp n^{-1/d}$ in dimension $d$ : the curse of dimensionality.

Gao (arXiv:2009.04382; Operations Research, 2023) shows that a radius of order $n^{-1/2}$ suffices, independently of the dimension. The first ingredient, and the subject of this mission, is a new concentration inequality for the empirical mean of a single loss function, whose rate is governed by the Wasserstein regularizer itself.

Setting

Let $\mathcal Z$ be a separable Banach space with norm $\|\cdot\|$ and let $p\in[1,2]$ . $\mathcal P_p(\mathcal Z)$ is the set of Borel probability measures with $\mathbb E[\|z\|^p]<\infty$ , and the Wasserstein distance of order $p$ is

\mathcal W_p(\mathbb P,\mathbb Q)^p=\inf_\pi\ \mathbb E_{(\tilde z,z)\sim\pi}\big[\|\tilde z-z\|^p\big],

the infimum over couplings $\pi$ of $\mathbb P$ and $\mathbb Q$ . For a loss $f:\mathcal Z\to\mathbb R$ , a nominal distribution $\mathbb Q$ and a radius $\rho\ge0$ , the Wasserstein regularizer is the excess of the robust loss over the nominal loss,

\mathcal R_{\mathbb Q,p}(\rho;f)=\sup_{\mathbb P\in\mathcal P_p(\mathcal Z)}\big\{\mathbb E_{\mathbb P}[f]:\mathcal W_p(\mathbb P,\mathbb Q)\le\rho\big\}-\mathbb E_{\mathbb Q}[f].

The data are $n$ i.i.d. samples $z_1,\dots,z_n$ from an unknown $\mathbb P_{\rm true}$ ; $\mathbb P_\otimes$ is their joint law and $\mathbb E_{\mathbb P_n}[f]=\frac1n\sum_i f(z_i)$ is the empirical loss. A distribution $\mathbb P$ satisfies the transportation-information inequality $T_p(\tau)$ if

\mathcal W_p(\mathbb Q,\mathbb P)\le\sqrt{\tau\,H(\mathbb Q\|\mathbb P)}\qquad\forall\,\mathbb Q\in\mathcal P_p(\mathcal Z),

with $H$ the relative entropy. $T_1$ holds for every distribution with a Gaussian moment $\mathbb E[e^{a\|z\|^2}]<\infty$ , and $T_2$ (Talagrand's inequality) is implied by a log-Sobolev inequality.

The rate function is built from

\Phi_g(t)=\mathbb E_{z\sim\mathbb P_{\rm true}}\Big[\sup_{\tilde z\in\mathcal Z}\big\{t(g(\tilde z)-g(z))-\|\tilde z-z\|^p\big\}\Big],\qquad \mathcal I_p(\varepsilon;g)^p=\sup_{t>0}\{\varepsilon t-\Phi_g(t)\}.

Formalization targets

Goal: Theorem 1 (variation-based concentration, p. 7)

If $f\le M+L\|z\|^p$ with $M,L>0$ and $\mathbb P_{\rm true}$ satisfies $T_p(\tau)$ , then for every $\varepsilon>0$

\mathbb P_\otimes\big\{\mathbb E_{\mathbb P_n}[f]-\mathbb E_{\mathbb P_{\rm true}}[f]<-\varepsilon\big\}\le\exp\big(-n\,\mathcal I_p(\varepsilon;-f)^2/\tau\big),

and for every $t>0$ , with probability at least $1-e^{-t}$ ,

\mathbb E_{\mathbb P_{\rm true}}[f]\le\mathbb E_{\mathbb P_n}[f]+\mathcal R_{\mathbb P_{\rm true},p}\Big(\sqrt{\tfrac{\tau t}{n}};-f\Big).

Milestones

Lemma 4 (p. 21): if $\mathbb P$ satisfies $T_p(\tau)$ , the product $\mathbb P^{\otimes n}$ satisfies $T_p(\tau n^{2/p-1})$ for the $\ell_p$ product distance $\mathsf d_p(z,\tilde z)^p=\sum_i\|z_i-\tilde z_i\|^p$ .
Identity (5) (p. 21): the relative entropy of an exponential tilt, $H(\nu^{(g)}\|\nu)=\mathbb E_{\nu^{(g)}}[g]-\ln\mathbb E_\nu[e^g]$ . Already proved on the platform and referenced.
Proposition 1 (p. 6): $\mathcal I_p(\cdot;f)$ inverts the regularizer, $\mathcal I_p(\mathcal R_{\mathbb P_{\rm true},p}(\rho;f);f)=\rho$ when the dual minimizer $\lambda_o$ of the strong-duality problem (1) exceeds the growth rate $\underline\lambda$ of $f$ , and $\ge\rho$ when they coincide.
Lemma 5 (p. 21): the same two bounds for a general $F:\mathcal Z^n\to\mathbb R$ with $\mathbb E_\otimes[F]=0$ and $p$ -growth, with rate $\mathcal J(\varepsilon;F)$ and bound $\mathcal R(\sqrt{\tau t/n};F)$ .
Corollary 1 (p. 7), two items: for $p=1$ under a uniform Lipschitz bound, $\mathbb E_{\mathbb P_{\rm true}}[f]\le\mathbb E_{\mathbb P_n}[f]+\sqrt{\tau t/n}\,\|f\|_{\rm Lip}$ ; for $p=2$ under a Lipschitz gradient, the bound $\sqrt{\tau t/n}\,\|\|\nabla f\|_*\|_{\mathbb P_{\rm true},2}+\hbar\tau t/n$ .

Significance

Theorem 1 says that the large-deviation rate of the empirical loss is the inverse of the Wasserstein regularizer, and that the regularizer at radius $\sqrt{\tau t/n}$ is a valid high-probability correction of the empirical loss. Neither involves the dimension of $\mathcal Z$ or the complexity of a covering of it. The paper builds its covering-number and local-Rademacher guarantees for Wasserstein DRO (Sections 4.1–4.2, the subject of two companion missions) on this single-function result, and Corollary 1 recovers, for $p=1$ , the Lipschitz-norm bound known from transportation inequalities while sharpening it for $p=2$ .

The results are proved in the paper; none is formalized. A complete development would give a machine-checked tensorization of transportation-information inequalities on Banach spaces and a Marton–Herbst-type concentration argument, both of which are used well beyond DRO.

Difficulty

The proof combines three ingredients that Mathlib does not yet connect. Tensorization (Lemma 4) needs disintegration of a measure on $\mathcal Z^n$ and the chain rule for relative entropy, together with a gluing of couplings and Hölder's inequality for the dimension constant. Lemma 5 combines $T_p$ with Kantorovich duality for the cost $\frac1n\mathsf d_p^p$ and the entropy of an exponential tilt, then optimizes a Young-inequality split over two parameters for $p<2$ , and extends from bounded $F$ to $p$ -growth by monotone truncation. Proposition 1 rests on the strong duality (1) of Gao and Kleywegt, an external result, and on the first-order optimality condition of a convex perspective function. A naive approach that bounds the deviation by $\mathcal W_p(\mathbb P_n,\mathbb P_{\rm true})$ fails: that distance decays like $n^{-1/d}$ , which is exactly the curse the theorem avoids.

Formalization scope

The source is arXiv:2009.04382; its printed page numbers equal the PDF's. The Lean development lives in the namespace WassFSG.Conc and uses these conventions:

$\mathcal Z$ is a real Banach space with its Borel $\sigma$ -algebra and is second countable (separable), as the cited duality results require; $\mathcal W_p^p$ is the published optimal transport cost with cost $\|u-w\|^p$ , and $H$ is Mathlib's klDiv.
Expectations of a loss inside the robust supremum are extended integrals $\int f^+-\int f^-$ in $[-\infty,\infty]$ ; the regularizer is valued in $[-\infty,\infty]$ .
$\mathcal I_p^p$ and $\mathcal J^p$ are read as $\max(0,\sup_{t>0}\{\cdots\})\in[0,\infty]$ , since the paper's declared codomain $\mathbb R_+\cup\{+\infty\}$ fails without it; an infinite rate gives the bound $0$ , never $1$ .
Lemma 5's printed "min" is an infimum, and Proposition 1's printed limit $\underline\lambda$ is a $\limsup$ .
The product space carries the $\ell_p$ -sum cost, not the sup metric.
"With probability at least $1-\delta$ " bounds the outer measure of the bad set by $\delta$ ; the sample size satisfies $n\ge1$ .
Added hypotheses: measurability and $\mathbb P_{\rm true}$ -integrability of $f$ in Theorem 1 and Proposition 1, measurability of $F$ in Lemma 5, and a nontrivial $\mathcal Z$ and $\mathbb P_{\rm true}\in\mathcal P_p(\mathcal Z)$ (presupposed by the dual problem (1)) in Proposition 1.
Theorem 1's growth hypothesis is kept as printed, an upper bound on $f$ . When $-f$ has no $p$ -growth bound, both conclusions hold trivially (the rate is $0$ and the regularizer is $+\infty$ ).

A formalization that reads an infinite $\mathcal I_p$ through a real coercion would turn the tail bound into the trivial bound $1$ ; the conventions above rule this out. Likewise a regularizer whose supremum ranged only over measures supported on the sample, or a $T_p$ condition over a restricted class of $\mathbb Q$ , would be a different statement.

Contributions welcome: Lemma 4 and Corollary 1 are independent entry points; a proof of the duality (1) under the paper's growth condition would be reusable by every Wasserstein DRO mission.

Selected references

R. Gao, Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality, Operations Research, 2023; preprint arXiv:2009.04382.
R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research, 2023; arXiv:1604.02199.
C. Villani, Optimal Transport: Old and New, Springer, 2009; doi:10.1007/978-3-540-71050-9.
N. Gozlan and C. Léonard, Transport Inequalities. A Survey, Markov Processes and Related Fields, 2010; arXiv:1003.3852.
F. Bolley and C. Villani, Weighted Csiszár–Kullback–Pinsker inequalities and applications to transportation inequalities, Annales de la Faculté des Sciences de Toulouse, 2005; doi:10.5802/afst.1095.

10 thms2 active usersReviewed

Completed

Functional Analysis Probability·Captain: mikedeng1

Distance Covariance in Metric Spaces 2: Without Negative Type Some Law Has Negative Distance Covariance, and Without Strong Negative Type Some Non-Product Law Has ZeroResearch Paper

Motivation

Distance covariance was introduced by Székely, Rizzo and Bakirov (2007) as a measure of dependence between random vectors in Euclidean spaces: it is zero exactly when the vectors are independent, and its empirical version gives a consistent test of independence that needs no moment beyond the first. Lyons (2013) asked for which metric spaces the same holds. His Theorem 3.11 shows that it holds whenever both spaces have strong negative type. This mission formalizes the complementary result, Proposition 3.15 of the same paper: the hypothesis on the space cannot be removed. Without negative type, distance covariance can even be negative; without strong negative type, it can vanish on a law that is not a product. Together with Theorem 3.11, the proposition locates the boundary of metric spaces on which distance covariance is a valid test of independence.

Timeline. 2007: Székely, Rizzo and Bakirov define distance covariance on $\mathbb R^p\times\mathbb R^q$ and prove the independence characterization there. 2013: Lyons extends the theory to metric spaces of negative type, characterizes the spaces where it remains a test of independence as those of strong negative type, and proves Proposition 3.15. 2018 and 2021: two errata by the author correct several statements of the paper; the first of them adds the standing assumption that all metric spaces are separable. Proposition 3.15 is not affected by the corrections.

Setting

Let $(\mathcal X,d)$ and $(\mathcal Y,d)$ be separable metric spaces, each with its Borel $\sigma$ -field. A finite Borel measure $\mu$ on $\mathcal X$ has a finite first moment if $\int d(o,x)\,d\mu(x)<\infty$ for some point $o$ . For such $\mu$ put

a_\mu(x):=\int d(x,x')\,d\mu(x'),\qquad D(\mu):=\int d(x,x')\,d\mu^2(x,x'),

and define the doubly centred distance $d_\mu(x,x'):=d(x,x')-a_\mu(x)-a_\mu(x')+D(\mu)$ . For two probability measures $\mu_1,\mu_2$ with finite first moments, $D(\mu_1-\mu_2)$ is the energy of their difference,

D(\mu_1-\mu_2)=\iint d\,d\mu_1^2-2\iint d\,d(\mu_1\times\mu_2)+\iint d\,d\mu_2^2 .

Let $\theta$ be a Borel probability measure on $\mathcal X\times\mathcal Y$ whose marginals $\mu$ on $\mathcal X$ and $\nu$ on $\mathcal Y$ have finite first moments. Its distance covariance is

\operatorname{dcov}(\theta):=\int d_\mu(x,x')\,d_\nu(y,y')\,d\theta^2\big((x,y),(x',y')\big).

$\theta$ is a product measure if $\theta=\mu\times\nu$ .

$\mathcal X$ has negative type if for every $n$ , all points $x_1,\dots,x_n$ and all reals $\alpha_1,\dots,\alpha_n$ with $\sum_i\alpha_i=0$ ,

\sum_{i,j\le n}\alpha_i\alpha_j\,d(x_i,x_j)\le 0. \tag{3.1}

On such a space $D(\mu_1-\mu_2)\le 0$ for all probability measures with finite first moments, and $\mathcal X$ has strong negative type if moreover equality holds only when $\mu_1=\mu_2$ . Write $\delta(y)$ for the point mass at $y$ .

Formalization targets

Goal: Proposition 3.15

Let $\mathcal Y$ have at least two points.

If $\mathcal X$ is not of negative type, there is a probability measure $\theta$ on $\mathcal X\times\mathcal Y$ whose marginals have finite first moments and

\operatorname{dcov}(\theta)<0.

If $\mathcal X$ is not of strong negative type, there is a probability measure $\theta$ on $\mathcal X\times\mathcal Y$ whose marginals have finite first moments, with

\operatorname{dcov}(\theta)=0\quad\text{and}\quad \theta\neq\mu\times\nu .

The space $\mathcal Y$ is arbitrary apart from having two points, so the statement fixes nothing about it.

Milestones (all from the proof on p. 17)

For probability measures $\mu_1,\mu_2$ with finite first moments and $y_1\ne y_2$ , the law $\theta=\big(\mu_1\times\delta(y_1)+\mu_2\times\delta(y_2)\big)/2$ has $\operatorname{dcov}(\theta)=-d(y_1,y_2)\,D(\mu_1-\mu_2)/8$ .
If $\mathcal X$ is not of negative type, there are probability measures $\mu_1\neq\mu_2$ with finite first moments and $D(\mu_1-\mu_2)>0$ .
If $x_1\neq x_2$ then $D(\delta(x_1)-\delta(x_2))<0$ .
If $D(\mu_1-\mu_2)\ge 0$ and $x_1\ne x_2$ , some $\gamma\in(0,1]$ makes $\tau_i:=\gamma\mu_i+(1-\gamma)\delta(x_i)$ satisfy $D(\tau_1-\tau_2)=0$ .
For $\mu_1\ne\mu_2$ with $D(\mu_1-\mu_2)\ge0$ , $x_1\ne x_2$ , $\gamma\in(0,1]$ and $y_1\ne y_2$ , the law $\big(\tau_1\times\delta(y_1)+\tau_2\times\delta(y_2)\big)/2$ is not a product measure.

Significance

The result. Theorem 3.11 of the paper shows that strong negative type of both spaces suffices for $\operatorname{dcov}(\theta)=0$ to characterize independence. Proposition 3.15 shows the hypothesis on each factor is necessary: a single failure of (3.1) already produces a law with negative distance covariance, so $\operatorname{dcov}$ is not even a nonnegative quantity there, and a single pair of distinct laws with $D(\mu_1-\mu_2)=0$ produces a dependent law that the test cannot detect. Consequently, any use of distance covariance on general metric data (graphs, $\ell^p$ spaces with $p>2$ , spaces of distributions under Wasserstein metrics) has to verify strong negative type first. Since the two-point space $\mathcal Y$ is arbitrary, the failure is a property of $\mathcal X$ alone.

Formalizing it. The proposition is proved in the paper; no machine-checked proof of it, or of any result about distance covariance, is known to exist. The mission produces a formal definition of distance covariance on separable metric spaces, of negative and strong negative type in the paper's measure-theoretic form, and the computation of $\operatorname{dcov}$ on two-point mixtures. These are the same objects as in the sibling mission on Theorem 3.11, so the two together give a formal account of when distance covariance characterizes independence.

Difficulty

The step the paper calls "a little algebra" is the bulk of the work: $\operatorname{dcov}$ is a four-fold integral of a product of doubly centred distances, each of which is itself built from integrals against a marginal of $\theta$ , and every manipulation of it happens inside Bochner integrals over product measures whose integrability has to be derived from first moments alone. In a formal setting nothing about these integrals is automatic. The passage from a violation of the finite-sum condition (3.1) to two probability measures with $D(\mu_1-\mu_2)>0$ is left implicit in the paper. The non-product claim also uses a fact the page does not state: that $\tau_1\neq\tau_2$ , which follows from $D(\mu_1-\mu_2)\ge 0$ and is false without it.

Formalization scope

All metric spaces carry their Borel $\sigma$ -field and are assumed second countable, which for metric spaces is separability; this is the author's own correction, Errata (i), which makes $d$ measurable on the product. Measures are Mathlib measures with values in $[0,\infty]$ ; mixture weights such as $\gamma$ , $1-\gamma$ and $1/2$ enter as extended nonnegative reals, and $\gamma$ is always restricted to $(0,1]$ . Because Mathlib's Bochner integral does not integrate against signed measures, $D(\mu_1-\mu_2)$ is defined as the bilinear energy expansion displayed above. "Not a product measure" means $\theta$ differs from the product of its own marginals, never from some other product.

Several formalizations of this statement would be trivially true and are excluded. A Bochner integral of a non-integrable function is $0$ in Lean, so every statement either assumes or concludes the finite first moments that make $\operatorname{dcov}$ and $D$ genuine integrals. Negative type is the finite-sum condition (3.1) and strong negative type the measure condition of p. 11, never an embedding property. The product condition is tested against $\theta$ 's own marginals, not against free factors. $\mathcal Y$ is quantified before $\theta$ is chosen, and part 2's hypothesis is the full negation of strong negative type, which includes spaces of negative type.

A complete development needs integrability of $d_\mu\,d_\nu$ under $\theta^2$ from first moments (Lemma 2.1 of the paper), linearity of the energy in each measure, push-forwards of mixtures of product measures, and the intermediate value theorem. The integrability and energy-bilinearity lemmas are reusable for any work on energy distance or distance covariance. Contributions of these general lemmas, as well as of proofs of the individual milestones, are welcome.

Selected references

R. Lyons, Distance covariance in metric spaces, Ann. Probab. 41 (2013), 3284–3305, https://doi.org/10.1214/12-AOP803; author's version arXiv:1106.5758 (version of 19 Dec. 2020, with errata). https://arxiv.org/abs/1106.5758
R. Lyons, Errata to "Distance covariance in metric spaces", Ann. Probab. 46 (2018), 2400–2405; reproduced as pp. 24–29 of arXiv:1106.5758 (version of 19 Dec. 2020). https://arxiv.org/abs/1106.5758
R. Lyons, Second errata to "Distance covariance in metric spaces", Ann. Probab. 49 (2021), 2668–2670; reproduced as pp. 30–32 of arXiv:1106.5758 (version of 19 Dec. 2020). https://arxiv.org/abs/1106.5758
G. J. Székely, M. L. Rizzo, N. K. Bakirov, Measuring and testing dependence by correlation of distances, Ann. Statist. 35 (2007), 2769–2794. https://doi.org/10.1214/009053607000000505

9 thms2 active usersReviewed

Completed

Functional Analysis Probability·Captain: mikedeng1

Distance Covariance in Metric Spaces 1: On Spaces of Strong Negative Type, Zero Distance Covariance Forces a Product MeasureResearch Paper

Motivation

Testing whether two random quantities are independent is one of the basic tasks of statistics. Classical correlation only detects linear dependence. Distance covariance, introduced by Székely, Rizzo and Bakirov (Ann. Statist. 2007) for random vectors in Euclidean spaces, is a dependence measure that vanishes exactly under independence. It only needs the distances between sample points, and its empirical version is a simple V-statistic. These properties made it a standard tool for nonparametric independence testing.

Lyons (Ann. Probab. 41 (2013), arXiv:1106.5758) asked in which metric spaces this characterization of independence survives. The answer is the class of metric spaces of strong negative type, which includes all separable Hilbert spaces. On such spaces, distance covariance gives a test of independence that is consistent against every alternative. This mission formalizes that result, Theorem 3.11 of the paper, together with the chain of results its proof rests on.

Timeline. Schoenberg (1937, 1938) characterized metric spaces of negative type by isometric embeddings of $(\mathcal X,d^{1/2})$ into Hilbert space. Székely, Rizzo and Bakirov (2007) defined distance covariance on $\mathbb R^p\times\mathbb R^q$ and proved that it vanishes only under independence. Lyons (2013) extended the theory to general metric spaces and identified strong negative type as the exact condition. The Errata (Ann. Probab. 46 (2018), 2400–2405; included in arXiv:1106.5758, pp. 24–29) added a standing separability assumption and repaired a gap in Lemma 3.8. The Second Errata appeared in Ann. Probab. 49 (2021).

Setting

Let $(\mathcal X,d)$ and $(\mathcal Y,d)$ be separable metric spaces with their Borel $\sigma$ -fields. A finite measure $\mu$ on $\mathcal X$ has a finite first moment if $\int d(o,x)\,d\mu(x)<\infty$ for some (equivalently every) $o\in\mathcal X$ . For such $\mu$ define

a_\mu(x)=\int d(x,x')\,d\mu(x'),\qquad D(\mu)=\int d(x,x')\,d\mu^2(x,x'),

d_\mu(x,x')=d(x,x')-a_\mu(x)-a_\mu(x')+D(\mu).

For a probability measure $\theta$ on $\mathcal X\times\mathcal Y$ whose marginals $\mu$ and $\nu$ have finite first moments, the distance covariance is

\operatorname{dcov}(\theta)=\int d_\mu(x,x')\,d_\nu(y,y')\,d\theta^2\big((x,y),(x',y')\big).

$\theta$ is a product measure if $\theta=\mu\times\nu$ .

$(\mathcal X,d)$ has negative type if $\sum_{i,j\le n}\alpha_i\alpha_j d(x_i,x_j)\le0$ for all $n$ , all points $x_1,\dots,x_n$ and all real weights with $\sum_i\alpha_i=0$ . For finite measures $\mu_1,\mu_2$ with finite first moments, $D(\mu_1-\mu_2)$ is the integral of $d$ against $(\mu_1-\mu_2)^2$ . On spaces of negative type $D(\mu_1-\mu_2)\le0$ for probability measures $\mu_1,\mu_2$ . The space has strong negative type if, in addition, $D(\mu_1-\mu_2)=0$ only when $\mu_1=\mu_2$ .

An embedding is a map $\phi:\mathcal X\to H$ into a real Hilbert space with $d(x,x')=\|\phi(x)-\phi(x')\|^2$ . Its barycenter map is $\beta_\phi(\mu)=\int\phi\,d\mu$ . The tensor embedding $(x,y)\mapsto\phi(x)\otimes\psi(y)$ takes values in the Hilbert tensor product $H\otimes K$ . $M^1(\mathcal X)$ denotes the finite signed measures whose variation has finite first moment. $M^{1,1}(\mathcal X\times\mathcal Y)$ denotes those on the product whose variation has marginals of finite first moment.

Formalization targets

Goal: Theorem 3.11

If $\mathcal X$ and $\mathcal Y$ have strong negative type and the marginals $\mu,\nu$ of the probability measure $\theta$ have finite first moments, then

\operatorname{dcov}(\theta)=0\ \Longrightarrow\ \theta=\mu\times\nu .

Milestones

Lemma 2.1: $d_\mu\in L^2(\mu\times\mu)$ . The integrability of $d_\mu(x,x')d_\nu(y,y')$ against $\theta^2$ (p. 4) follows, so $\operatorname{dcov}(\theta)$ is a genuine integral.
Schoenberg's theorem (p. 9): a separable space has negative type if and only if it has an embedding into $\ell^2(\mathbb N)$ .
Identity (3.4): $D(\mu)=-2\|\beta_\phi(\mu)\|^2$ when $\mu(\mathcal X)=0$ . Proposition 3.1: strong negative type holds iff $\beta_\phi$ is injective on probability measures with finite first moment.
Proposition 3.5: $d_\mu(x,x')=-2\langle\phi(x)-\beta_\phi(\mu),\phi(x')-\beta_\phi(\mu)\rangle$ , together with $a_\mu(x)=\|\phi(x)-\beta_\phi(\mu)\|^2+D(\mu)/2$ and $D(\mu)=2\operatorname{Var}(\phi(X))$ .
Proposition 3.7: $\operatorname{dcov}(\theta)=4\|\beta_{\phi\otimes\psi}(\theta-\mu\times\nu)\|^2$ .
Lemma 3.9 (injectivity of $\beta_\phi$ on $M^1(\mathcal X)$ ) and Lemma 3.8 in its errata form (injectivity of $\beta_{\phi\otimes\psi}$ on $M^{1,1}(\mathcal X\times\mathcal Y)$ ).

The converse, that a product measure has $\operatorname{dcov}(\theta)=0$ (p. 5), is included as a companion statement.

Significance

The result. Theorem 3.11 makes the empirical distance covariance a consistent test of independence against all alternatives on any pair of separable metric spaces of strong negative type. Examples are separable Hilbert spaces and their subsets, and every space of negative type after replacing $d$ by $d^r$ , $0<r<1$ . Its companion, Proposition 3.15 (a separate mission of this series), shows that strong negative type is exactly the right hypothesis. Proposition 3.7 also identifies distance covariance with Brownian covariance and with the original Euclidean definition, through specific choices of embedding.

Formalizing it. The result is proved, with the gap in Lemma 3.8 closed by the Errata (2018). No part of it has a machine-checked proof that we know of. A formalization needs barycenters of Hilbert-space-valued maps against measures, the Hilbert tensor product of two real Hilbert spaces, and Schoenberg's embedding theorem. None of these is in Mathlib in this form, and all are reusable well beyond distance covariance.

Difficulty

The obvious route reads $\operatorname{dcov}(\theta)=0$ as "the barycenters of $\theta$ and of $\mu\times\nu$ coincide in $H\otimes K$ " and concludes by injectivity. Strong negative type only gives injectivity of $\beta_\phi$ on probability measures, while $\theta-\mu\times\nu$ is a signed measure on a product space. Getting from injectivity on single factors to injectivity on $M^{1,1}$ of the product is where the original proof had a gap: an auxiliary signed measure built from $\theta$ was not shown to have a finite first moment. The errata version changes the embeddings so that this can be done. Two smaller obstacles are integrability (the definition of $\operatorname{dcov}$ is meaningful only by Lemma 2.1) and the construction of the Hilbert space in Schoenberg's theorem.

Formalization scope

All spaces are Lean metric spaces with their Borel $\sigma$ -fields and SecondCountableTopology. This is the separability the author adds in Errata (i), which makes $d$ measurable on the product. Measures are Mathlib Measures. A probability $\theta$ on $\mathcal X\times\mathcal Y$ has marginals θ.map Prod.fst and θ.map Prod.snd. "Product measure" means $\theta$ equals the product of these marginals. Hilbert spaces are real (Errata (viii)). Existential embeddings land in $\ell^2(\mathbb N)$ , which suffices for separable spaces. The Hilbert tensor product is the completion of the algebraic tensor product with its inner product. $D(\mu_1-\mu_2)$ is defined by its bilinear expansion. Injectivity on $M^1$ and $M^{1,1}$ is stated for pairs of finite measures, which is equivalent to injectivity on signed measures via the Jordan decomposition.

Every integral here is a Bochner integral, which is $0$ for a non-integrable integrand. Each statement therefore carries the finite-first-moment hypotheses of the paper, and integrability itself is a milestone. Negative type and strong negative type are defined by (3.1) and by the condition on $D(\mu_1-\mu_2)$ , not through an embedding or a barycenter map, so Schoenberg's theorem and Proposition 3.1 are not definitional. A statement with a "product measure" whose factors are free, or with dcov defined without the moment hypotheses, would be a different and trivializable theorem.

Welcome contributions: barycenter calculus for Hilbert-valued integrals, tensor-product integrals, Schoenberg's theorem, and proofs of any milestone.

Selected references

R. Lyons, Distance covariance in metric spaces, Ann. Probab. 41 (2013), 3284–3305. https://doi.org/10.1214/12-AOP803 ; author's version with both errata: https://arxiv.org/abs/1106.5758
R. Lyons, Errata to "Distance covariance in metric spaces", Ann. Probab. 46 (2018), 2400–2405; reproduced in https://arxiv.org/abs/1106.5758 (version of 19 Dec. 2020), pp. 24–29
G. J. Székely, M. L. Rizzo, N. K. Bakirov, Measuring and testing dependence by correlation of distances, Ann. Statist. 35 (2007), 2769–2794. https://doi.org/10.1214/009053607000000505
I. J. Schoenberg, Metric spaces and positive definite functions, Trans. Amer. Math. Soc. 44 (1938), 522–536. https://doi.org/10.1090/S0002-9947-1938-1501980-0

11 thms2 active usersReviewed

Bandit Algorithms Operations Research·Captain: mikedeng1

Dynamic Assortment Personalization in High Dimensions 1: The Nuclear-Norm Explore-Then-Exploit Policy Has Regret at Most ((Cr(m+n)+3) log T + 1)ωResearch Paper

Motivation

An online retailer that serves many kinds of customers must decide, for each arriving customer, which handful of products to display. Showing too many items is impossible (screen space, shelf space), and which items sell depends on who is looking. The retailer does not know the customers' preferences in advance and learns them only from the choices customers make among the items shown. This is dynamic assortment personalization: an online learning problem in which every display both earns revenue and produces data.

Kallus and Udell (arXiv:1610.05604) study the regime in which the number of customer types $m$ and the number of items $n$ are both large, so that learning each type's preferences separately would take on the order of $mn$ interactions. Their premise is that preferences across types are governed by a few latent features, which makes the matrix of preference parameters approximately low rank. The non-contextual problem — one customer type, multinomial-logit choice — was studied by Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013); the paper extends it to many types and proposes an explore-then-exploit policy whose estimates come from nuclear-norm regularized maximum likelihood, the standard convex surrogate for low rank used in matrix completion.

Setting

There are $m$ customer types and $n$ items. Each type $i$ has a revenue vector $W_i\in\mathbb R^n$ (row $i$ of $W\in\mathbb R^{m\times n}$ ; $W_{ij}$ is the expected revenue when type $i$ buys item $j$ ) and a preference vector $\Theta^\star_i$ (row $i$ of the unknown matrix $\Theta^\star\in\mathbb R^{m\times n}$ ). Types arrive independently from an unknown distribution $\mu^\star$ in the simplex $\Delta^m$ .

For an assortment $S\subseteq\{1,\dots,n\}$ and a parameter vector $\theta\in\mathbb R^n$ , the multinomial-logit (MNL) choice probability of item $j\in S$ is

p_j(S;\theta)=\frac{e^{\theta_j}}{1+\sum_{j'\in S}e^{\theta_{j'}}},

and the customer buys nothing with probability $1/(1+\sum_{j'\in S}e^{\theta_{j'}})$ . The expected revenue of $S$ is $F(S;w,\theta)=\sum_{j\in S}p_j(S;\theta)w_j$ , and $S^\star(w,\theta;K)$ is the set of maximizers of $F(\cdot;w,\theta)$ over $|S|\le K$ . The revenue gap $\delta(w,\theta;K)$ is the optimal revenue minus the best revenue of a non-optimal assortment.

In round $t=1,2,\dots$ a customer of type $i_t\sim\mu^\star$ arrives, the retailer offers $S_t$ with $|S_t|\le K$ , and the customer chooses $j_t$ from the MNL law with parameters $\Theta^\star_{i_t}$ . The regret (Definition 1) of a policy after $T$ rounds is the expected revenue of the $\Theta^\star$ -greedy policy, which always offers an element of $S^\star(W_{i_t},\Theta^\star_{i_t};K)$ , minus the expected revenue of the policy.

Algorithm 2, $\pi_{\text{nuc-norm}}(C,\lambda)$ , keeps a sample $\mathcal O$ of exploration observations. At round $t$ , if $|\mathcal O|\le Cr(m+n)\log t$ it explores: it offers a uniformly random subset of size exactly $K$ and records $(i_t,j_t,S_t)$ . Otherwise it exploits: it offers an element of $S^\star(W_{i_t},\widehat\Theta_{i_t};K)$ , where $\widehat\Theta$ is a solution of

\min_{\Theta}\ L(\Theta)+\lambda\|\Theta\|_*\quad\text{s.t.}\quad\|\Theta\|_\infty\le\alpha/\sqrt{mn},\tag{5}

with $L$ the average negative log-likelihood (4) of the sample, $\|\cdot\|_*$ the nuclear norm and $\|\Theta\|_\infty$ the largest absolute entry.

Formalization targets

Goal: Theorem 6

Let $r\ge\operatorname{rank}\Theta^\star$ , $1/\rho\le m\mu^\star_i\le\rho$ for all $i$ , $\|\Theta^\star\|_\infty\le\alpha/\sqrt{mn}$ , $\min_i\delta(W_i,\Theta^\star_i;K)\ge\delta>0$ and $0\le W$ , $\max_{ij}|W_{ij}|\le\omega$ . With

C=\frac{4194304\,K^6\rho^3\omega^2\alpha^2e^{16\alpha}}{\delta^2},\qquad\lambda=8\sqrt{\frac{\rho K}{Crmn}},\tag{12}

for every selection of $\widehat\Theta$ from the solutions of (5) and of the exploited assortment,

\mathrm{Regret}(T;\pi_{\text{nuc-norm}}(C,\lambda))\le\big((Cr(m+n)+3)\log T+1\big)\,\omega\qquad\text{for }1\le T\le(m+n)^{mn/(Cr(m+n))}.

Milestones

From the printed proof of Theorem 6 (pp. 47–48): the Lipschitz bound $|p_j(S;\theta)-p_j(S;\theta')|\le\frac14\sqrt{|S|}\|\theta-\theta'\|_2$ ; the revenue bound $|F(S;w,\theta)-F(S;w,\theta')|\le\frac14\|w\|_\infty K^{3/2}\|\theta-\theta'\|_2$ ; the comparison $F(S';w,\theta)\ge F(S;w,\theta)-\frac12\|w\|_\infty K^{3/2}\|\theta-\theta'\|_2$ of optimal sets; the stability of the optimal set; and the count of exploration rounds. From the deterministic part of the recovery analysis (Sec. 8): Lemma 2 (a quadratic lower bound on the Bregman divergence of $L$ ), Lemma 5 (an upper bound from the regularized objective) and Lemma 6 (the nuclear-norm error is controlled by $\sqrt r$ times the Frobenius error and the spectral tail of $\Theta^\star$ ).

Significance

Theorem 6 is the paper's guarantee that a policy exploiting low-rank structure pays regret of order $r(m+n)\log T$ rather than the order $mn\log T$ that the paper shows (Theorem 5) for policies treating each type separately. The intermediate results are reusable: the Lipschitz bounds for MNL choice probabilities and revenue apply to any MNL assortment policy that plugs in estimated parameters, and Lemmas 2, 5 and 6 are the deterministic core of nuclear-norm regularized estimation for a likelihood that is not an entrywise loss.

To the best of current knowledge none of these results has a machine-checked proof. The mission produces a formal model of a contextual MNL assortment process with an adaptive policy, its trajectory law and regret, together with formal statements and proofs of the Lipschitz and stability facts that any explore-then-exploit analysis of MNL assortment needs. Several printed statements needed correction (see Formalization scope); machine-checked proofs settle the corrected forms.

Difficulty

The goal is a statement about the law of a $T$ -round adaptive process: the offered set at round $t$ depends on the whole past through the exploration test and through an estimate defined only as some minimizer of (5). Any argument must handle this dependence exactly, for every admissible selection of minimizer and of optimal assortment, rather than for one convenient choice.

The constants are explicit and the horizon is restricted, so the inequality has to hold with the paper's normalization exactly as stated, including the box constraint of (5). The printed proof routes through the paper's high-probability recovery bound (Theorem 3), which is believed false as printed and is not part of this mission, so a proof cannot simply cite it. Lemmas 5 and 6 require Hölder's inequality for the spectral/nuclear pairing and a decomposition of the error relative to the singular subspaces of $\Theta^\star$ ; Lemma 2 requires a curvature estimate for the log-sum-exp function uniformly on the box.

Formalization scope

The source is the arXiv preprint arXiv:1610.05604, an unstamped PDF pinned by sha256 2b010481…216a; its printed page numbers equal the PDF page numbers.

Types and items are Fin m and Fin n, 0-based; the no-purchase option is none. Matrices are MatrixCompletion.RealMatrix m n; the nuclear, spectral and Frobenius norms, the Frobenius inner product and $\|\cdot\|_\infty$ are the published MatrixCompletion definitions, and $F$ is the published ChoiceCDLP.MNL.mnlObjective with weights $e^{\theta_j}$ and no-purchase weight $1$ . All probabilities and expectations are finite sums over histories in Fin T → Fin m × Finset (Fin n) × Option (Fin n). Regret is Definition 1 after the tower property: the greedy policy earns $\sum_i\mu^\star_i\max_{|S|\le K}F(S;W_i,\Theta^\star_i)$ per round and Algorithm 2 earns $F(S_t;W_{i_t},\Theta^\star_{i_t})$ in expectation. The gap condition $\delta(w,\theta;K)\ge d$ is stated as "every non-optimal assortment of size at most $K$ earns at most the optimum minus $d$ ", since $\delta$ itself is undefined when every assortment is optimal.

Added hypotheses and corrections, each disclosed in the item's note:

Theorem 6 assumes $W\ge0$ , $\delta>0$ , $1\le K\le n$ , $m,n\ge1$ and $T\ge1$ . The horizon is read as $T\le(m+n)^{mn/(Cr(m+n))}$ (the page sets $r$ beside the fraction in the exponent); for $r\ge1$ this is the smaller range. If $r=0$ , Lean's division by zero gives $\lambda=0$ and horizon $T\le1$ .
The stability of the optimal set (p. 47) is false as printed (an equality of optimal sets) and is stated as the inclusion $S^\star(w,\theta';K)\subseteq S^\star(w,\theta;K)$ under the page's (non-strict) closeness hypothesis, multiplied out.
The exploration count (p. 48) is stated as $Cr(m+n)\log T+1$ , the form the next display uses, instead of the printed $C\log T+1$ .
Lemma 2 is false as printed and carries an extra factor $\frac12$ ; it assumes $\Theta^\star$ and $\Theta^\star+\Delta$ both feasible for (5).
Lemmas 5 and 6 carry the standing assumptions of Sec. 8: $\widehat\Theta$ solves (5), $\Theta^\star$ is feasible, $\lambda>0$ .

Theorem 3 (static recovery) and Lemma 4 (gradient concentration) are not posed: both are believed false as printed. Lemmas 3 and 7 are not posed either.

A trivializing formalization is ruled out: the estimator is any minimizer of (5) with its box constraint, the exploited set is any optimal assortment for the estimate, and both are quantified universally; exploration draws uniformly from subsets of size exactly $K$ ; and the benchmark is the $\Theta^\star$ -greedy policy under the same arrival law. Fixing the estimator to $\Theta^\star$ , dropping the box, or comparing to the best fixed assortment would change the theorem.

Contributions welcome: proofs of the milestones (the Lipschitz lemmas are calculus on the softmax function; Lemmas 5 and 6 are matrix analysis reusable for other nuclear-norm estimators), a proof that the definition of $\nabla L$ is the gradient of $L$ , and a proof that the history weights form a probability distribution.

Selected references

N. Kallus, M. Udell, Dynamic Assortment Personalization in High Dimensions, arXiv preprint, 2016–2017; Operations Research 68(4), 2020. https://arxiv.org/abs/1610.05604
P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic assortment optimization with a multinomial logit choice model and capacity constraint, Operations Research 58(6), 2010. https://doi.org/10.1287/opre.1100.0866
D. Sauré, A. Zeevi, Optimal dynamic assortment planning with demand learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.1120.0412
B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://doi.org/10.1137/070697835

15 thms2 active usersReviewed

Completed

Linear Optimization Machine Learning·Captain: mikedeng1

Fast Rates for Contextual Linear Optimization 3: Under the Margin Condition, a Plug-In Policy Whose Estimate Has Pointwise Sub-Gaussian Tails at Rate aₙ Has Regret O(B·aₙ^(−(1+α)/2))Research Paper

Why estimate-then-optimize

Many operational decisions are linear programs whose cost vector is uncertain but predictable from side information: routing with travel times that depend on weather and time of day, procurement with prices that depend on market signals, assignment with costs that depend on observed features. Contextual linear optimization (CLO) formalizes this: observe features $X$ , choose a decision $z$ in a polytope $\mathcal Z$ , pay $Y^\top z$ for an unobserved random cost vector $Y$ .

Two families of data-driven methods compete. Estimate-then-optimize (ETO) fits a regression $\hat f(x) \approx \mathbb E[Y \mid X = x]$ and then solves the linear program with the estimated costs. Integrated methods (for example the SPO+ approach of Elmachtoub and Grigas, 2022) choose a decision rule by minimizing the empirical decision cost directly over a policy class, on the argument that a regression fit ignores how its errors affect decisions. Hu, Kallus and Mao (arXiv:2011.03030v3, Management Science 2022) show that, under a margin condition on the problem, the comparison goes the other way: ETO attains faster regret rates than any method that only uses a policy class.

This mission formalizes their ETO upper bound, Theorem 8. It is the third of a three-mission series on the paper; the first formalizes the upper bound for empirical risk minimization over a policy class (Theorem 6) and the second the matching lower bound for policy-class methods (Theorem 7).

Setting

Write $\mathbb R^k$ for Euclidean space with inner product $u^\top v$ and norm $\|\cdot\|$ .

Decisions. The polytope $\mathcal Z = \{z \in \mathbb R^d : Az \le b\}$ is nonempty and satisfies $\|z\| \le B$ for all $z \in \mathcal Z$ , with $B > 0$ . Its set of extreme points is $\mathcal Z^\angle$ , a finite set.
Data. Features $X \in \mathbb R^p$ have law $\mathbb P_X$ ; costs $Y \in \mathbb R^d$ satisfy $\|Y\| \le 1$ . The regression function is $f^*(x) = \mathbb E[Y \mid X = x]$ . The data $\mathcal D$ are $n$ i.i.d. copies of $(X, Y)$ .
Optimal decisions. $\mathcal Z^*(x) = \arg\min_{z \in \mathcal Z} f^*(x)^\top z$ .
Gap. If $\mathcal Z^*(x) \ne \mathcal Z$ , the gap is

\Delta(x) = \min_{z \in \mathcal Z^\angle \setminus \mathcal Z^*(x)} f^*(x)^\top z - \min_{z \in \mathcal Z} f^*(x)^\top z,

the extra cost of the best suboptimal vertex; otherwise $\Delta(x) = 0$ .

Noise condition (Assumption 2). For some $\alpha, \gamma \ge 0$ ,

\mathbb P_X\bigl(0 < \Delta(X) \le \delta\bigr) \le (\gamma\delta/B)^\alpha \quad \text{for all } \delta > 0.

It always holds with $\alpha = 0$ ; larger $\alpha$ means less mass near dual degeneracy.

Plug-in policy. For an estimate $f$ , a plug- $f$ -in policy $\pi_f$ chooses at every $x$ an extreme point in $\arg\min_{z \in \mathcal Z} f(x)^\top z$ . The ETO policy is $\pi_{\hat f}$ , where $\hat f = \hat f_{\mathcal D}$ is computed from the data.
Regret. $\mathrm{Regret}(\hat\pi) = \mathbb E_{\mathcal D}\mathbb E_X\bigl[f^*(X)^\top \hat\pi_{\mathcal D}(X) - \min_{z \in \mathcal Z} f^*(X)^\top z\bigr]$ .

In Lean the polytope is FastCLO.ETO.Polytope, the distribution is FastCLO.ETO.Instance (the law $\mu$ of $X$ and the conditional law $\kappa$ of $Y$ given $X$ ), and optVal, Zstar, gap, NoiseCond, IsPlugIn and regret are the objects above.

Formalization targets

Goal: Theorem 8

Fix $\alpha, \gamma \ge 0$ and $C_1, C_2 > 0$ . There is a constant $C$ depending only on these such that, for every instance satisfying the noise condition, every $n$ , every $a_n > 0$ and every estimator $\hat f$ with

\mathbb P_{\mathcal D}\bigl(\|\hat f(x) - f^*(x)\| \ge \delta\bigr) \le C_1 \exp(-C_2 a_n \delta^2) \quad \text{for every } \delta > 0 \text{ and almost every } x,

the plug-in policy satisfies

\mathrm{Regret}(\pi_{\hat f}) \le C\,B\,a_n^{-(1+\alpha)/2}.

The constant is existential, as on the page; the proof gives an explicit value, but the goal does not commit to it.

Milestones

The milestones are the displayed steps of the paper's proof (Appendix A.5, p. 30), in order:

Pointwise bound. The plug-in decision's excess cost at a point is at most $2B\|f^*(x) - \hat f(x)\|$ .
Implication display. If the plug-in decision is strictly suboptimal at $x$ and $\|f^*(x) - \hat f(x)\| \le \varepsilon$ , then $0 < \Delta(x) \le 2B\varepsilon$ .
Peeled bound. For every $\delta > 0$ ,

\mathrm{Regret}(\pi_{\hat f}) \le 2B\delta\,\mathbb P(0 < \Delta(X) \le 2B\delta) + B\delta\sum_{r \ge 1} 2^{r+1}\,\mathbb P\bigl(\|f^*(X) - \hat f(X)\| > 2^{r-1}\delta,\ 0 < \Delta(X) \le 2^{r+1}B\delta\bigr).

Bound after iterating expectations. Under the hypotheses of Theorem 8, for every $\delta > 0$ ,

\mathrm{Regret}(\pi_{\hat f}) \le B\gamma^\alpha(2\delta)^{\alpha+1} + B\gamma^\alpha C_1\delta^{\alpha+1}\sum_{r \ge 1} 2^{(r+1)(\alpha+1)} e^{-C_2 a_n (2^{r-1}\delta)^2}.

Significance

For well-specified least squares regression, $a_n$ is of order $n$ up to a logarithmic factor (Corollary 4 of the paper), and Theorem 8 gives regret of order $n^{-(1+\alpha)/2}$ up to logarithms. Theorem 7 of the same paper shows that no algorithm that only uses a policy class of Natarajan dimension $\eta$ can beat $n^{-(1+\alpha)/(2+\alpha)}$ in the worst case over such instances. Since $(1+\alpha)/2 > (1+\alpha)/(2+\alpha)$ for every $\alpha \ge 0$ , the two results separate ETO from integrated methods when the regression model is well specified. This runs against the common intuition behind end-to-end learning. The noise condition is the CLO analogue of the Tsybakov margin condition in classification (Tsybakov, 2004): the gap $\Delta$ plays the role of the distance of the regression function from the decision boundary.

The result is proved in the paper; as far as is known it has not been machine-checked. Formalizing it fixes the exact hypotheses (which quantifiers the tail condition carries, what "universal" means for $C_1, C_2$ , and the measurability the regret integral needs) and yields reusable pieces: the extreme-point argument behind the implication display and the peeling bound in $[0, \infty]$ .

Difficulty

The obvious argument bounds regret by $2B\,\mathbb E\|f^*(X) - \hat f(X)\|$ , which gives only the rate $a_n^{-1/2}$ and ignores the noise condition (this is Theorem 4 of the paper). The faster rate needs two things the naive bound does not use. First, a wrong decision at $x$ is possible only where the gap $\Delta(x)$ is positive and at most a multiple of the estimation error. This uses that plug-in decisions are extreme points, so a strictly suboptimal decision is at least $\Delta(x)$ worse than optimal; it requires finiteness of $\mathcal Z^\angle$ , which must be proved for an H-polytope. Second, the error must be controlled pointwise in $x$ , with sub-Gaussian tails over the data, and combined with the noise condition shell by shell, through a Fubini exchange between the data and the feature.

Formalization scope

Representation. Vectors live in EuclideanSpace ℝ (Fin k). The polytope bundles $A$ , $b$ , $B > 0$ , nonemptiness and the bound $\|z\| \le B$ . The distribution is a probability measure $\mu$ on features and a Markov kernel $\kappa$ with $\kappa(x)\{\|y\| > 1\} = 0$ ; $f^*(x) = \int y\,\kappa(x)(dy)$ , and the data law is the $n$ -fold product of $\mu \otimes \kappa$ .
Conventions. Optimal values and gaps are real infima, taken over nonempty bounded (indeed finite or compact) sets. The regret is measured against the optimal value, which equals the paper's $f^*(X)^\top\pi^*(X)$ . Probabilities are $[0, \infty]$ -valued measures; $(\gamma\delta/B)^\alpha$ is a real power with $0^0 = 1$ .
Disclosed additions. Plug-in policies are any selection from the argmin with values in $\mathcal Z^\angle$ (the paper's consistent tie-breaking is dropped, which strengthens the upper bound). The estimator and the policy are jointly measurable in the data and the feature. $C_1, C_2 > 0$ and $a_n > 0$ . The constant $C$ is chosen after $\alpha, \gamma, C_1, C_2$ and before the instance, the sample size, the estimator and $a_n$ .
Ruled out. The tail hypothesis bounds the probability over the data for each fixed $x$ , for every $\delta > 0$ ; it is not a probability over $X$ and not a single $\delta$ . The conclusion is uniform: one constant for all instances, estimators and $a_n$ . The peeled bound is stated in $[0, \infty]$ , because a divergent real series would sum to $0$ .
Infrastructure needed. Finiteness of the extreme points of a bounded H-polytope and attainment of linear minima at extreme points; measurability of $x \mapsto \Delta(x)$ ; Fubini–Tonelli on the product of the data law and $\mu$ ; summability of $\sum_r 2^{(r+1)(\alpha+1)} e^{-c\,4^r}$ . The polytope facts are reusable well beyond this mission.

Selected references

Y. Hu, N. Kallus, X. Mao, Fast Rates for Contextual Linear Optimization, arXiv:2011.03030v3, 2021; Management Science, 2022. https://arxiv.org/abs/2011.03030v3
A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 2004. https://doi.org/10.1214/aos/1079120131
P. Massart, É. Nédélec, Risk bounds for statistical learning, Annals of Statistics 34(5), 2006. https://doi.org/10.1214/009053606000000786

9 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

Dynamic Assortment Personalization in High Dimensions 2: The Empirical Type Frequencies Satisfy ‖μ̂ − μ⋆‖_q ≤ min{8√((τ+m)/N), m^{1/q}√((τ+log 2m)/(2N))} with Probability at Least 1 − e^{−τ}Research Paper

Motivation

A retailer that personalizes the set of products it shows to each customer needs to know who its customers are. In the low-rank multinomial-logit model of Kallus and Udell, Dynamic Assortment Personalization in High Dimensions (arXiv:1610.05604), every arriving customer belongs to one of $m$ customer types, and the type of each arrival is drawn independently from an unknown type distribution $\mu^\star$ . Planning a non-personalized assortment, or weighting the per-type preference estimates, requires an estimate of $\mu^\star$ from the observed types. When $m$ is large (types may be fine-grained customer profiles), the question is how many observations are needed before that estimate is reliable, and in which norm.

Theorem 4 of the paper answers this for the simplest estimator, the empirical frequencies, with an explicit, non-asymptotic bound in every $\ell_q$ norm, $1\le q\le\infty$ . The bound has two regimes: one that is good when the sample size $N$ is only slightly larger than $m$ , and one that is good when $N$ is large compared with $m^{2/q}$ .

Setting

Customer types are labelled $1,\dots,m$ . The type distribution is a vector $\mu^\star$ in the probability simplex

\Delta^m=\Big\{\mu\in\mathbb R^m:\ \mu_i\ge0,\ \sum_{i=1}^m\mu_i=1\Big\}.

The observation model (Sec. 3.2, p. 13) consists of $N$ records $(i_t,j_t,S_t)$ , $t=1,\dots,N$ : the type $i_t$ of the $t$ -th customer, the item $j_t$ the customer chose, and the assortment $S_t$ offered. The types $i_1,\dots,i_N$ are independent and identically distributed with $\mathbb P(i_t=i)=\mu^\star_i$ . The items and assortments play no role for the type distribution.

The empirical type frequencies (Sec. 3.2.1, p. 14) are

\hat\mu_i=\frac1N\sum_{t=1}^N\mathbb I[i_t=i],\qquad i=1,\dots,m.

For $v\in\mathbb R^m$ and $q\in[1,\infty]$ the $\ell_q$ norm is $\|v\|_q=(\sum_i|v_i|^q)^{1/q}$ , and $\|v\|_\infty=\max_i|v_i|$ ; the convention $m^{1/q}=1$ at $q=\infty$ is used throughout.

The proof works with the empirical Rademacher complexity of the sample: with $I_t=e_{i_t}$ the indicator vector of the $t$ -th type,

\widehat{\mathfrak R}_N=\frac1{2^N}\sum_{\epsilon\in\{-1,+1\}^N}\ \sup_{\|v\|_\infty\le1}\ \frac1N\sum_{t=1}^N\epsilon_t\,v^TI_t .

Formalization targets

Goal: Theorem 4 (p. 18)

For every $\tau\ge0$ and $q\in[1,\infty]$ , with probability at least $1-e^{-\tau}$ ,

\|\hat\mu-\mu^\star\|_q\ \le\ \min\left\{8\sqrt{\frac{\tau+m}{N}},\ \frac{m^{1/q}}{\sqrt2}\sqrt{\frac{\tau+\log(2m)}{N}}\right\}.

The goal keeps the paper's constants and its single statement over all $q\in[1,\infty]$ , including $q=\infty$ .

Milestones (proof of Theorem 4, p. 44)

The coordinatewise tail bound, for $\eta\ge0$ :

\mathbb P(\|\hat\mu-\mu^\star\|_q>\eta)\le\sum_{i=1}^m\mathbb P\big(|\hat\mu_i-\mu^\star_i|>\eta/m^{1/q}\big)\le2m\exp(-2N\eta^2/m^{2/q}).

The deterministic complexity bound, for every sample:

\widehat{\mathfrak R}_N=\frac1N\sum_{i=1}^m\frac1{2^N}\sum_{\epsilon}\Big|\sum_{t=1}^N\mathbb I[i_t=i]\epsilon_t\Big|\le\frac1{\sqrt N}\sum_{i=1}^m\sqrt{\hat\mu_i}\le\sqrt{\frac mN}.

The $\ell_1$ tail bound, for $\eta\ge0$ :

\mathbb P(\|\mu^\star-\hat\mu\|_1>\eta)\le e^{\,m-N\eta^2/64}.

Significance

The first term of the minimum shows that $\hat\mu$ is consistent in every $\ell_q$ norm as soon as $N$ grows faster than $m$ , and gives $\sqrt{m/N}$ -consistency in $\ell_1$ , i.e. in total variation. A coordinatewise argument alone cannot give this: for $q=1$ it yields a bound that does not vanish unless $N$ grows faster than $m^2$ . The second term is the sharper one in the regime $N\gg m^{2/q}$ , for instance in $\ell_\infty$ , where it gives the familiar $\sqrt{\log(m)/N}$ rate. In the paper the estimate of $\mu^\star$ enters non-personalized assortment planning, where the expected revenue of an assortment is averaged over types.

On the formalization side, the result is proved in the paper; nothing about it is open. As far as a search of the Prove2Me catalog shows, no machine-checked version of this statement, or of an $\ell_q$ concentration bound for empirical frequencies with these constants, exists. A complete development would also supply, in finite and elementary form, a coordinatewise Hoeffding bound for binomial proportions and an $\ell_1$ deviation bound for categorical samples, both reusable well beyond this mission.

Difficulty

The second term is a union bound and a binomial tail bound. The first term is where the work is. The obvious route, bounding each coordinate separately and summing, costs a factor $m$ in the $\ell_1$ norm and gives a useless rate when $N$ is comparable to $m$ . The proof instead treats $\|\hat\mu-\mu^\star\|_1$ as the supremum of an empirical process over the $\ell_\infty$ unit ball, controls its mean through the Rademacher complexity (where the absolute value of a sum of $N\hat\mu_i$ random signs must be bounded by $\sqrt{N\hat\mu_i}$ ), and then needs concentration of the supremum around its mean with constants good enough to produce the stated $8$ and $1/64$ . The paper's p. 44 citation of a symmetrization result states it with the empirical rather than the expected complexity, so that step has to be redone with care rather than transcribed.

Formalization scope

Source. The arXiv preprint arXiv:1610.05604. The PDF has no arXiv stamp, version or date and is pinned by its sha256 2b0104810fa9d656f2b79f8a44f791b2a3da388f3f6707564f4619da2050216a. Its printed page numbers equal the PDF page numbers.
Types and samples. Types are Fin m and draws Fin N, both 0-based. A sample is a map x : Fin N → Fin m.
Probability. The i.i.d. law is explicit: the probability of an event is the finite sum, over the samples in the event, of $\prod_t\mu^\star_{x_t}$ . No measure theory is used. Restricting the observations $(i_t,j_t,S_t)$ to the types is exact, because the types are i.i.d. $\mu^\star$ regardless of the items and assortments.
Standing assumptions. $\mu^\star\in\Delta^m$ (Mathlib's stdSimplex), which forces $m\ge1$ , and $N\ge1$ , added because $\hat\mu$ is undefined for an empty sample. The milestones' tail bounds assume $\eta\ge0$ , which the paper leaves implicit. For $\eta<0$ the events are certain and the printed bounds can be smaller than $1$ .
Norms and exponents. $\|\cdot\|_q$ is Mathlib's PiLp norm on $\mathbb R^m$ for $q\in[1,\infty]$ , with $q$ an extended nonnegative real; $m^{1/q}$ and $m^{2/q}$ use an exponent defined as $0$ at $q=\infty$ and $1/q$ otherwise. $\log$ is the natural logarithm.
The Rademacher complexity is defined by the paper's supremum over the $\ell_\infty$ unit ball, a nonempty index set on which the objective is bounded, so the supremum is genuine.
Corrected misprint. On p. 44 the Hoeffding display prints $2m\exp(-2n\eta^2/m^{2/q})$ with $n$ , the number of items. The formal statement uses the sample size $N$ , which is what the argument produces and what Theorem 4 needs. In the complexity chain, the binomial coefficient printed as $\binom{m}{\lceil N\hat\mu_i/2\rceil}$ should be $\binom{N\hat\mu_i}{\lceil N\hat\mu_i/2\rceil}$ ; that line is not part of the formal statement.
Not a trivialization. The probability is taken under the i.i.d. product law of $\mu^\star$ , not for a fixed sample and not under the uniform law on samples. The events use the paper's strict and non-strict inequalities as printed.
Welcome contributions. An elementary Hoeffding bound for the binomial proportion; a bounded-differences (McDiarmid) inequality for functions of finitely many independent finite-valued draws; a symmetrization inequality relating $\mathbb E\|\hat\mu-\mu^\star\|_1$ to the Rademacher complexity; and alternative proofs of the $\ell_1$ term.

Selected references

N. Kallus, M. Udell, Dynamic Assortment Personalization in High Dimensions, arXiv preprint, 2016; Operations Research 68(4), 2020. https://arxiv.org/abs/1610.05604
P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3, 463–482, 2002 (the paper cites it as 2003). https://www.jmlr.org/papers/v3/bartlett02a.html
W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301), 13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830
C. McDiarmid, On the Method of Bounded Differences, Surveys in Combinatorics, London Mathematical Society Lecture Note Series 141, 148–188, 1989. https://doi.org/10.1017/CBO9781107359949.008

6 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

Robustness May Be at Odds with Accuracy 1: Every Classifier with Standard Accuracy ≥ 1 − δ Has ℓ∞ Robust Accuracy ≤ pδ/(1 − p) Against ε ≥ 2ηResearch Paper

Motivation

Classifiers trained to be robust against small, adversarially chosen input perturbations routinely lose standard accuracy. Adversarial training (Madry et al., 2018) improves worst-case accuracy under an $\ell_p$ -bounded attack, but on MNIST, CIFAR-10 and ImageNet the resulting models are measurably less accurate on unperturbed inputs, and the loss grows with the attack radius. A natural reading is that this is an artefact of training procedures or of finite data.

Tsipras, Santurkar, Engstrom, Turner and Mądry (ICLR 2019) argue otherwise: they exhibit a simple distribution on which every classifier faces the trade-off, so that the tension is a property of the data distribution itself and survives infinite data, including for the Bayes-optimal classifier. The argument isolates a distinction that has since been influential: robust features, moderately correlated with the label and stable under small perturbations, versus non-robust features, individually weak but jointly highly predictive and easily flipped. This mission formalizes the paper's first theorem, Theorem 2.1, and its proof in Appendix C.

Setting

Fix $d \in \mathbb N$ , a probability $p$ with $\tfrac12 \le p < 1$ , and $\eta \ge 0$ . The distribution $\mathcal D$ of an input-label pair $(x, y)$ , $x = (x_1, x_2, \dots, x_{d+1}) \in \mathbb R^{d+1}$ , is the data model (3):

y \sim \mathrm{Unif}\{-1,+1\}, \qquad x_1 = \begin{cases} +y & \text{w.p. } p\\ -y & \text{w.p. } 1-p\end{cases}, \qquad x_2, \dots, x_{d+1} \overset{\text{i.i.d.}}{\sim} \mathcal N(\eta y, 1),

with $x_1$ and $(x_2, \dots, x_{d+1})$ independent given $y$ . Write $G_+$ and $G_-$ for the law $\mathcal N(\pm\eta, 1)^{\otimes d}$ of the weak features given $y = +1$ and $y = -1$ .

A classifier is a measurable map $f : \mathbb R^{d+1} \to \{-1, +1\}$ . Its standard accuracy is $\Pr_{(x,y)\sim\mathcal D}[f(x) = y]$ , the objective (1) of the paper with the 0–1 loss. Its $\ell_\infty$ robust accuracy at radius $\varepsilon$ is

\mathrm{acc}_\varepsilon(f) = \Pr_{(x,y)\sim\mathcal D}\big[f(x + \delta) = y \text{ for every } \delta \in \mathbb R^{d+1} \text{ with } \|\delta\|_\infty \le \varepsilon\big],

the objective (2) with the 0–1 loss and perturbation set $\Delta = \{\|\delta\|_\infty \le \varepsilon\}$ . In Lean these are stdAcc d p η f and robustAcc d p η f ε, each an average with weight $\tfrac12$ of the two class-conditional probabilities. The proof also uses $p_{ij}$ , the probability that $f$ predicts $+1$ when $x_1 = i$ and the weak features follow $G_j$ (pij), and the shift adversary $x_i \mapsto x_i - 2\eta y$ for $i \ge 2$ (shiftAdv, accuracy shiftAcc).

Formalization targets

Goal: Theorem 2.1 (p. 5)

For every measurable classifier $f$ and every $\delta \in \mathbb R$ ,

\Pr[f(x) = y] \ge 1 - \delta \ \Longrightarrow\ \mathrm{acc}_\varepsilon(f) \le \frac{p}{1-p}\,\delta \qquad \text{for every } \varepsilon \ge 2\eta.

The statement quantifies over all classifiers, not a parametric family, and over every radius $\varepsilon \ge 2\eta$ .

Milestones (App. C, pp. 14–16)

The shift $z_i \mapsto z_i - 2\eta y$ pushes $\mathcal N(\eta y, 1)^{\otimes d}$ forward to $\mathcal N(-\eta y, 1)^{\otimes d}$ : it changes $G_+$ to $G_-$ and vice versa.
For $\varepsilon \ge 2\eta \ge 0$ , robust accuracy is at most the accuracy against the shift adversary.
$\Pr[f(x) = y] = \tfrac12\big(p(1 + p_{++} - p_{--}) + (1-p)(1 + p_{-+} - p_{+-})\big)$ .
$\Pr[f(x_{\mathrm{adv}}) = y] = \tfrac12\big(p(1 + p_{+-} - p_{-+}) + (1-p)(1 + p_{--} - p_{++})\big)$ .
With $a = 1 - p_{++} + p_{--} \ge 0$ and $b = 1 - p_{-+} + p_{+-}$ : $1 - \tfrac12(pa + (1-p)b) \ge 1 - \delta$ implies $\tfrac12((1-p)a + pb) \le \tfrac{p}{1-p}\delta$ .

Companion statements (§2.1, pp. 4–5)

Tightness. $\mathrm{sign}(x_1)$ has standard accuracy $p$ and robust accuracy $p$ for $0 \le \varepsilon < 1$ ; at $\delta = 1-p$ the bound of Theorem 2.1 is attained.
Standard classification is easy. For $f_{\mathrm{avg}}(x) = \mathrm{sign}(\tfrac1d\sum_{i\ge2} x_i)$ , $\Pr[f_{\mathrm{avg}}(x) = y] = \Pr[\mathcal N(\eta, 1/d) > 0]$ , which exceeds $99\%$ when $\eta \ge 3/\sqrt d$ .

Significance

Theorem 2.1 converts the empirical observation into a statement about a distribution: on $\mathcal D$ , standard accuracy $1 - \delta$ caps robust accuracy at $\frac{p}{1-p}\delta$ , so as $\delta \to 0$ robust accuracy falls to $0$ , while the adversary's budget $\varepsilon = 2\eta = \Theta(1/\sqrt d)$ is small compared with the feature scale $\pm 1$ . Together with the companion statements it shows that the model admits a classifier with accuracy above $99\%$ and a classifier with robust accuracy $p$ , but no classifier with both. It underlies the paper's conclusion that robust training must give up non-robust features, and the later line of work on robust versus non-robust features.

The result is proved in the paper, with an elementary argument. As far as the platform record and a search of the literature show, it has not been machine-checked. The formalization adds an exact, convention-explicit version of the model and of robust accuracy (worst case over a closed $\ell_\infty$ ball, outer measure of a possibly non-measurable event), a Lean statement of the shift-invariance property of Gaussian products that the argument rests on, and a reusable template for 0–1-loss adversarial objectives that later missions on robustness in Gaussian models can follow.

Difficulty

The obvious attempt is to bound robust accuracy for a specific classifier, or for linear classifiers, where the adversary's best response is explicit. That does not reach the theorem: the claim is about every measurable $f$ , for which no best response is computable and the robust event need not even be measurable. On the formal side, the statements involve the pushforward of a product of Gaussians under a coordinatewise shift, the decomposition of the class-conditional law into the two-point law of $x_1$ and the product $G_\pm$ , and a measure applied to a possibly non-measurable robust event; none of these is available as a ready-made lemma for this model.

Formalization scope

Inputs live in Fin (d + 1) → ℝ; coordinate 0 is $x_1$ and coordinate i.succ is $x_{i+2}$ . The Mathlib norm on this type is the sup norm, so ‖δ‖ ≤ ε is exactly the $\ell_\infty$ ball. Labels and predictions are the reals $\pm1$ . The class-conditional law is ((x1Law p y).prod (weakLaw d η y)).map (Matrix.vecCons ·.1 ·.2) with weakLaw d η y = Measure.pi (fun _ => gaussianReal (y * η) 1). Accuracies are real numbers in $[0,1]$ computed with toReal. The robust event is measured by its outer measure, i.e. under the completion of $\mathcal D$ ; no measurability of that event is assumed.

The standing assumption $p \ge \tfrac12$ of model (3) is a hypothesis of every statement. Four hypotheses implicit on the page are explicit: $p < 1$ in the goal (the bound divides by $1-p$ , and Lean's $p/0 = 0$ would make the statement false at $p = 1$ ); $\eta \ge 0$ (the page takes $\eta$ large, $\Theta(1/\sqrt d)$ ; with $\eta < 0$ the case $\varepsilon = 0$ has no adversary and the statement fails); measurability of $f$ ; and $f(x) \in \{\pm1\}$ for every $x$ .

A trivializing formalization is ruled out: the goal is stated for every measurable $\{\pm1\}$ -valued classifier and for the worst case over the full $\ell_\infty$ ball of every radius $\varepsilon \ge 2\eta$ , not for linear classifiers, not for the fixed shift adversary, and not with the $p_{ij}$ among its hypotheses; those appear only in milestones.

The development needs Mathlib's gaussianReal, Measure.pi, product measures and pushforwards. Welcome contributions: the Gaussian shift identity (reusable for any Gaussian location model), the disintegration of condLaw along $x_1$ , and the two accuracy formulas.

Selected references

D. Tsipras, S. Santurkar, L. Engstrom, A. Turner, A. Mądry, Robustness May Be at Odds with Accuracy, ICLR 2019; arXiv:1805.12152v5 (2019). https://arxiv.org/abs/1805.12152
A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018. https://arxiv.org/abs/1804.11285

7 thms2 active usersReviewed

Linear Optimization Machine Learning·Captain: mikedeng1

Fast Rates for Contextual Linear Optimization 2: Any Algorithm Choosing from a Policy Class of Natarajan Dimension η Has Regret ≥ (ρ(Z)/2e⁴)((η−1)/n)^((1+α)/(2+α)) on Some Margin-α InstanceResearch Paper

Motivation

In contextual linear optimization (CLO) a decision maker observes a covariate $X$ (features of a day, a customer, a network state) and then chooses a decision $z$ from a polytope $\mathcal Z$ to minimise an uncertain linear cost $Y^\top z$ . Shortest-path routing with predicted travel times and inventory or portfolio decisions driven by forecasts are standard instances. Since $Y$ is unknown at decision time, the relevant cost is $f^*(X)^\top z$ with $f^*(x) = \mathbb E[Y \mid X = x]$ , and a policy is learned from $n$ past observations $(X_i, Y_i)$ .

Hu, Kallus and Mao (arXiv:2011.03030, Management Science 2022) compare two families of methods: estimate-then-optimize (fit $f^*$ , then optimise) and induced empirical risk minimisation (search a policy class directly for low empirical cost). Their main finding is that under a noise condition that controls how often two vertices of $\mathcal Z$ are nearly tied, the regret decays faster than the usual $n^{-1/2}$ . For ERM over a policy class of Natarajan dimension $\eta$ they prove the rate $(\eta/n)^{(1+\alpha)/(2+\alpha)}$ up to logarithms (their Theorem 6). This mission formalizes the matching lower bound, their Theorem 7: no algorithm that only knows the true optimal policy lies in the class can do better.

Setting

A polytope $\mathcal Z = \{z \in \mathbb R^d : Az \le b\}$ is nonempty with $\sup_{z \in \mathcal Z}\|z\| \le B$ , $B > 0$ . Its set of extreme points is $\mathcal Z^\angle$ . An instance is a law $\mathbb P_X$ of $X \in \mathbb R^p$ together with a conditional law of $Y \in \mathbb R^d$ given $X = x$ , with $\|Y\| \le 1$ ; $f^*(x)$ is the conditional mean. The optimal set is $\mathcal Z^*(x) = \arg\min_{z\in\mathcal Z} f^*(x)^\top z$ and the gap is

\Delta(x) = \inf_{z \in \mathcal Z^\angle \setminus \mathcal Z^*(x)} f^*(x)^\top z - \min_{z \in \mathcal Z} f^*(x)^\top z

when $\mathcal Z^*(x) \ne \mathcal Z$ , and $\Delta(x) = 0$ otherwise. The noise condition (Assumption 2) with parameters $\alpha, \gamma \ge 0$ is

\mathbb P_X\big(0 < \Delta(X) \le \delta\big) \le (\gamma\delta/B)^\alpha \qquad \forall \delta > 0.

A policy is a map $\pi : \mathbb R^p \to \mathcal Z^\angle$ . A class $\Pi$ of policies Natarajan-shatters $\eta$ points if there are $x_1, \dots, x_\eta$ and values $s_i \ne s_i'$ such that every pattern in $\{0,1\}^\eta$ is realised by some $\pi \in \Pi$ choosing $s_i$ or $s_i'$ at $x_i$ ; the Natarajan dimension is the largest such $\eta$ . An algorithm maps a sample $\mathcal D$ of $n$ i.i.d. draws of $(X, Y)$ to a policy $\hat\pi_{\mathcal D} \in \Pi$ , and its regret is

\mathrm{Regret}(\hat\pi) = \mathbb E_{\mathcal D}\,\mathbb E_X\Big[f^*(X)^\top \hat\pi_{\mathcal D}(X) - \min_{z\in\mathcal Z} f^*(X)^\top z\Big].

The scale of the bound is the vertex separation

\rho(\mathcal Z) = \inf_{z \in \mathcal Z^\angle,\ z' \in \mathrm{conv}(\mathcal Z^\angle \setminus \{z\})} \|z - z'\|.

Formalization targets

Goal: Theorem 7

Fix $\alpha \ge 0$ , a polytope $\mathcal Z$ , a class $\Pi$ of Natarajan dimension at least $\eta \ge 1$ , and $n \ge 2^{2+\alpha}(\eta - 1)$ . For every algorithm $\mathcal D \mapsto \hat\pi_{\mathcal D} \in \Pi$ there is an instance with $\|Y\| \le 1$ on which some $\pi^* \in \Pi$ is optimal at every $x$ , the noise condition holds with the given $\alpha$ and $\gamma = B/\rho(\mathcal Z)$ , and

\mathrm{Regret}(\hat\pi) \;\ge\; \frac{\rho(\mathcal Z)}{2e^4}\Big(\frac{\eta - 1}{n}\Big)^{\frac{1+\alpha}{2+\alpha}}.

Milestones

$\rho(\mathcal Z) > 0$ when $\mathcal Z$ has two extreme points (Theorem 3, p. 7).
Eq. (25): the vertex-separating directions $w(z)$ have norm at most one and separate $z$ from the other vertices by exactly $\rho(\mathcal Z)$ .
Eq. (14): the error of any estimate of a hidden bit is at least the minimum Bayes risk.
The posterior identity of p. 21.
The Jensen step of p. 21.
The binomial bound $\mathbb E|N^1 - N^0| \le \sqrt{nq}$ of pp. 21–22.
The exponential bound in Eq. (15).
The closing calculation of the proof of Theorem 7 (p. 30).

Significance

Theorem 7 shows that the fast rate of Theorem 6 is optimal in both $n$ and $\eta$ , up to logarithmic factors, among methods that exploit only the well-specification of the policy class. The paper uses this to explain why estimate-then-optimize, which also exploits the structure of the regression class, can beat ERM: it is not subject to this lower bound. At $\alpha = 0$ the bound recovers the order of the paper's slow-rate lower bound (Theorem 3), and as $\alpha \to \infty$ it approaches $\eta/n$ .

The result is proved in the paper; no machine-checked proof of it or of its milestones is known. Formalizing it produces a checked minimax lower bound for a decision problem over an arbitrary polytope, together with a reusable toolkit for Assouad-type arguments over hypercubes of hard instances: the binary Bayes-risk bound, the closed-form posterior for a biased coin, the Jensen step, and the binomial mean absolute deviation bound.

Difficulty

The statement quantifies over every algorithm, including non-measurable and randomisation-free ones, so the argument cannot analyse a specific estimator. The standard route averages the regret over a family of $2^{\eta-1}$ instances and reduces it to hidden-bit estimation, but two features of CLO make the construction delicate. First, the instances must keep $\|Y\| \le 1$ while giving each shattered point a prescribed gap between its optimal vertex and every other vertex of an arbitrary polytope; this is where $\rho(\mathcal Z)$ and the directions of Eq. (25) enter. Second, each instance must satisfy the noise condition with the given $\alpha$ and $\gamma = B/\rho(\mathcal Z)$ , which fixes how much probability mass the near-tied points may carry; the mass cannot simply be spread uniformly as in the slow-rate argument. The constants have to be tracked exactly, since the goal states the explicit constant $1/(2e^4)$ .

Formalization scope

Everything lives in the namespace FastCLO.LowerBound. Vectors are EuclideanSpace ℝ (Fin k). A polytope bundles its constraint rows, right-hand sides, a radius $B > 0$ , nonemptiness and boundedness. An instance is a probability measure $\mu$ on $\mathbb R^p$ and a Markov kernel $\kappa$ with $\kappa(x)(\{\|y\| > 1\}) = 0$ ; $f^*$ is the kernel mean, and the sample law is the $n$ -fold product of $\mu \otimes \kappa$ . Every joint law disintegrates this way. The regret is measured against the optimal value $\min_{z\in\mathcal Z} f^*(x)^\top z$ , which equals the paper's comparison with $\pi^*$ . Natarajan dimension "at least $\eta$ " is the existence of a shattered $\eta$ -tuple. Infima are real infima over sets that are nonempty and bounded under the hypotheses. Probabilities in the noise condition are in $[0,\infty]$ , and $(\gamma\delta/B)^\alpha$ is a real power.

The paper prints Theorem 7 with the distribution chosen before $n$ ; its proof builds the distribution from $n$ , and the formal goal is stated in the proved order: for every $n$ and every algorithm there is an instance. The hypothesis $\eta \ge 1$ excludes the empty case. No measurability is assumed of the algorithm. The algorithm must return a member of $\Pi$ for every sample, and the instance must satisfy $\|Y\| \le 1$ , the optimality of some member of $\Pi$ everywhere, and the noise condition. Dropping any of these would make the bound trivial or false, and none of them is relaxed.

A complete development needs finiteness of the extreme points of a polytope, projections onto convex hulls, products of finitely supported measures, and elementary binomial identities. The generic milestones (3–7) are reusable for other hypercube lower bounds. Proofs of individual milestones are welcome independently of the goal.

The companion missions Fast Rates for Contextual Linear Optimization 1 (the ERM upper bound, Theorem 6) and 3 (the estimate-then-optimize bound, Theorem 8) use the same model.

Selected references

Y. Hu, N. Kallus, X. Mao, Fast Rates for Contextual Linear Optimization, arXiv:2011.03030v3, 2021; Management Science 68(6), 2022. https://arxiv.org/abs/2011.03030
L. Devroye, G. Lugosi, Lower bounds in pattern recognition and learning, Pattern Recognition 28(7), 1995. https://doi.org/10.1016/0031-3203(95)00002-Z
A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 2004. https://doi.org/10.1214/aos/1079120131
B. K. Natarajan, On learning sets and functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804
O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization bounds in the predict-then-optimize framework, NeurIPS 2019. https://arxiv.org/abs/1905.11488

12 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

A Modern Introduction to Online Learning XV: Online Learning Bounds Rademacher Complexity, Giving Massart's Lemma G∞√(2 ln d)/√TTextbook

Why random signs matter in learning

Learning theory asks whether a rule that fits an observed sample will also perform well on future observations. A class with many functions can fit accidental patterns in the sample, so its size and geometry affect the reliability of empirical risk estimates. Empirical Rademacher complexity measures this ability to fit noise: attach an independent random sign to each observed point, let the class choose its best function after seeing all signs, and average the resulting signed score. A smaller value supports tighter uniform generalization bounds. Orabona, §16.1, pp. 270–271

Online learning studies a different protocol. A learner chooses a prediction before each round's loss is revealed, and its regret compares its cumulative loss with that of a fixed competitor chosen in hindsight. Chapter 16 of Orabona's book connects these two quantities. The connection matters because an online algorithm's regret estimate can be used to control the statistical complexity of a class of predictors, even though the online game and the random-sign experiment are defined differently. Orabona, Theorem 16.4, p. 272

Setting and notation

Fix a horizon $T\ge1$ and vectors $z_1,\ldots,z_T\in\mathbb R^d$ . For each $t$ , let $\varepsilon_t$ be an independent Rademacher sign, equal to $1$ or $-1$ with probability one half each. Given a nonempty bounded set $V\subseteq\mathbb R^d$ , define its linear class by

H_{\mathrm{lin}}=\{z\mapsto\langle x,z\rangle:x\in V\}.

The empirical complexity on the fixed sample $S=(z_1,\ldots,z_T)$ is

\widehat{\mathfrak R}_S(H_{\mathrm{lin}}) =\frac1T\mathbb E_\varepsilon\left[ \sup_{x\in V}\sum_{t=1}^T\varepsilon_t\langle x,z_t\rangle \right].

This is a finite expectation over the $2^T$ possible sign assignments. The supremum is over the same comparison set $V$ for every assignment; the chosen $x$ may depend on the signs. The book's general Definition 16.1 allows an arbitrary class of real-valued functions, while this mission uses its linear specialization from the discussion immediately preceding Theorem 16.4. Orabona, Definition 16.1 and §16.1, pp. 270–272

For the final bound, $V$ is the probability simplex $\Delta^{d-1}=\{x\in\mathbb R^d:x_i\ge0,\ \sum_i x_i=1\}$ . The supremum of a linear score over this simplex is the maximum of its $d$ coordinate scores. Write $G_\infty$ for a common bound on the infinity norm of the sample vectors, so $|z_{t,i}|\le G_\infty$ for every round and coordinate. Orabona, Corollary 16.7, p. 273

Formalization targets

The central target is Corollary 16.7, called Massart's Lemma in the book:

\frac1T\mathbb E_\varepsilon\left[ \max_{1\le i\le d}\sum_{t=1}^T\varepsilon_tz_{t,i} \right] \le \frac{G_\infty\sqrt{2\ln d}}{\sqrt T}.

Its constant and dependence on $d$ and $T$ are part of the target. The result includes $d=1$ : in that case the expectation and the bound are both zero. Orabona, Corollary 16.7, p. 273

Two statements supply the chapter's route to this target. Theorem 16.4 says that if a nonanticipating online linear algorithm has worst-case regret at most $R(T)$ for all loss vectors in a symmetric set $Z$ , then $\widehat{\mathfrak R}_S(H_{\mathrm{lin}})\le R(T)/T$ for any sample in $Z$ . The Exponentiated Gradient regret bound of §6.6 gives, on the simplex, $\sum_t(\ell_t(x_t)-\ell_t(u))\le(\ln d)/\eta+(\eta/2)\sum_t\|g_t\|_\infty^2$ for every simplex competitor $u$ . The milestone list quotes both source statements. Orabona, Theorem 16.4, p. 272; §6.6, p. 81

What the result provides

The goal supplies a sample-dependent complexity bound using only a coordinate bound, the number of coordinates, and the sample size. Its square-root dependence on $\ln d$ explains why a simplex-indexed class can have much smaller complexity than a crude bound that scales directly with $d$ . In applications where a generalization estimate contains empirical Rademacher complexity, this result gives a concrete quantity to insert for a finite coordinate class. Orabona, §16.1, pp. 271–273

The mathematical statements are proved in the book. This mission asks for machine-checked proofs of the exact finite-sign formulation of the goal, the regret-to-complexity reduction, and the source's Exponentiated Gradient regret estimate. The local proposal currently contains statements with proof placeholders; it does not claim that these three items have already been proved in Lean. The resulting finite-sign and bounded-supremum definitions can also support other empirical-process arguments.

Where the work is difficult

The reduction has to respect the order of the online game. A bound for a learner allowed to inspect the current random sign would not imply the same complexity estimate: it could choose its round- $t$ point using information that a genuine online learner lacks. The algorithm therefore needs a precise causality condition, as well as a regret guarantee that holds for every admissible gradient sequence. Orabona, proof of Theorem 16.4, p. 272

The simplex result also depends on the exact regret coefficient. A generic $O(\sqrt T)$ estimate does not recover the displayed $\sqrt{2\ln d}$ constant. At the boundaries, real division and logarithms in Lean are total, so the statements must say when $T$ and $d$ are positive. The one-dimensional case is meaningful and must stay in the theorem.

Formalization scope

Vectors are functions Fin d → ℝ, representing $\mathbb R^d$ with its coordinate pairing. Samples, predictions and gradients use rounds $1,\ldots,T$ ; index zero is unused. The random-sign expectation is an exact average over Boolean assignments, with no measure-theoretic integrability convention. Both Rademacher averages require $T\ge1$ . The signed linear supremum is real-valued and receives evidence that $V$ is nonempty and bounded. Theorem 16.4 also records the book's closedness hypothesis.

Theorem 16.4 formalizes deterministic online algorithms. The source permits internal randomization as well; that extension requires an independent probability model for the algorithm's random choices. The Exponentiated Gradient item represents losses by real-valued functions and requires the subgradient inequality on the simplex, where the book evaluates them. Its run predicate requires $\eta>0$ and includes the uniform initial point and coordinate update of Algorithm 6.2. The goal itself has no algorithm hypothesis. Its infinity-norm assumption is expressed as coordinate absolute-value bounds.

The definitions exclude an empty comparison class or an unbounded real supremum being silently assigned a default Lean value. A complete development needs finite-sign averaging identities, properties of real suprema over bounded sets, simplex geometry, and the regret analysis of Exponentiated Gradient. Contributions to these reusable components, to the two milestones, and to the goal are in scope. The PAC-Bayes and time-uniform concentration parts of Chapter 16 are reserved for separate work because they need different probability and measure-theory objects.

Selected references

Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 16 and §6.6. arXiv

5 thms2 active usersReviewed

Functional Analysis Markov Chain Probability·Captain: mikedeng1

Spectral Gaps for a Metropolis–Hastings Algorithm in Infinite Dimensions I: The pCN Algorithm Has a Wasserstein Spectral Gap Uniform in the Dimension When the Potential Is Globally LipschitzResearch Paper

Motivation

Sampling from a distribution described relative to a Gaussian reference law is common in Bayesian inverse problems, where an unknown function or initial condition is inferred from noisy observations. Such a distribution is naturally infinite dimensional before it is approximated on a computer. A numerical method must therefore behave reliably as the approximation dimension grows. Hairer, Stuart and Vollmer study this question for Metropolis–Hastings chains and prove that the preconditioned Crank–Nicolson (pCN) chain admits a Wasserstein mixing bound with an iteration count independent of the projection dimension Hairer, Stuart and Vollmer (2014). This mission formalizes their globally Lipschitz case, Theorem 2.12.

The central practical concern is concrete: refining a discretization should improve the target approximation without forcing the number of Markov steps needed for a fixed contraction to grow with the number of coordinates. A bound on each finite dimensional chain separately would not settle that concern, because its constants could deteriorate with dimension. The theorem requires one set of constants for the infinite dimensional chain and every finite dimensional projection.

Setting

Let $H$ be a separable real Hilbert space. Its Gaussian reference measure $\gamma$ has mean zero and a covariance eigenbasis $e_1,e_2,\ldots$ . The subspace $K_m$ is the span of the first $m$ eigenvectors, and $\gamma_m$ is the law of the orthogonal projection of a $\gamma$ -distributed vector onto $K_m$ . The potential $\Phi:H\to\mathbb R$ determines the target measures

\mu(dx)=M e^{-\Phi(x)}\gamma(dx),\qquad \mu_m(dx)=M_m e^{-\Phi(x)}\gamma_m(dx),

where $M$ and $M_m$ normalize each measure. The paper's finite dimensional chain has state space $K_m$ , rather than the whole space $H$ with unused coordinates Hairer, Stuart and Vollmer (2014), (1.1)–(1.2).

At step size $0<\delta\le1/2$ , the pCN proposal from $x$ is $y=\sqrt{1-2\delta}\,x+\sqrt{2\delta}\,\xi$ , with $\xi$ drawn from $\gamma$ or $\gamma_m$ as appropriate. The move is accepted with probability $1\wedge e^{\Phi(x)-\Phi(y)}$ ; rejection leaves the state at $x$ . Write $P$ and $P_m$ for these transition kernels Hairer, Stuart and Vollmer (2014), (1.3), (1.5)–(1.6).

The potential is globally Lipschitz, $e^{-\Phi}$ is $\gamma$ -integrable, and the acceptance probability has a positive lower bound in specified balls centered at $\sqrt{1-2\delta}\,x$ outside a bounded region. These are Assumptions 2.10 and 2.11 Hairer, Stuart and Vollmer (2014), p. 12. The allowed ball radius is either a positive constant or $r_0\|x\|^a$ with $r_0>0$ and $1/2<a<1$ .

Formalization targets

Uniform Wasserstein contraction

For $\varepsilon>0$ , set $d_\varepsilon(x,y)=1\wedge\|x-y\|/\varepsilon$ . Choose the Lyapunov function $V(x)=\|x\|^i$ , where $i\ge1$ , or, in the growing-radius case, $V(x)=e^{v\|x\|}$ with $v>0$ . The weighted cost is $\widetilde d(x,y)=\sqrt{d_\varepsilon(x,y)(1+V(x)+V(y))}$ , and $W_{\widetilde d}$ is its infimum over couplings.

Theorem 2.12 asserts that $\mu$ and each $\mu_m$ are the unique invariant probability measures of $P$ and $P_m$ . It also asserts that, for every sufficiently small $\varepsilon$ , there is one integer $\widetilde n$ satisfying both bounds for all probability measures on the respective spaces and for every $m$ Hairer, Stuart and Vollmer (2014), p. 12:

W_{\widetilde d}(\nu_1P^{\widetilde n},\nu_2P^{\widetilde n})\le\tfrac12 W_{\widetilde d}(\nu_1,\nu_2),

W_{\widetilde d_m}(\nu_1P_m^{\widetilde n},\nu_2P_m^{\widetilde n})\le\tfrac12 W_{\widetilde d_m}(\nu_1,\nu_2).

Here $\widetilde d_m$ is the same formula restricted to $K_m$ . The milestone list includes the uniform Lyapunov, contraction and smallness claims and the cited weak Harris theorem; the Gaussian projection comparison of Lemma 3.1 is a further stated lemma of the mission. Fernique's Gaussian exponential-moment result is linked to its existing published formalization.

Significance

The result bounds the number of pCN iterations needed for a fixed Wasserstein contraction uniformly over the finite dimensional approximations. It also identifies the intended target as the only invariant probability measure, so the contraction describes convergence toward the measure used by the inverse problem. The weighted Wasserstein cost permits this statement on an unbounded Hilbert space, where an ordinary total variation small-set argument would impose a different kind of regularity Hairer, Stuart and Vollmer (2014), §§2.2–2.3.

The paper proved Theorem 2.12 in 2014. The remaining work here is a machine-checked development of the pCN kernels, Gaussian projections, Wasserstein estimates, and weak Harris application. A formalized Fernique theorem already exists in the platform library; the pCN estimates and Theorem 2.12 are open draft statements in this proposal. They will be reusable in the locally Lipschitz pCN regime and in analyses of other Metropolis kernels that satisfy the same abstract contraction conditions.

Difficulty

The pCN proposal contracts the starting points, but the accept–reject step can break that direct coupling: one chain may accept a proposal while the other rejects it. A bound on the proposal distance alone therefore does not imply a bound on the transition laws. The probability of that mismatched decision must be controlled near each pair of starting points, while the acceptance lower bound must remain uniform on the projected spaces. Large starting points also require a Lyapunov estimate to enter the bounded region used by the weak Harris theorem Hairer, Stuart and Vollmer (2014), §§3.1.1–3.1.3.

Formalization scope

The Lean development represents $H$ as a complete separable real inner product space with Borel measurable structure, $\gamma$ as a centered Gaussian probability measure, and the chosen Hilbert basis as diagonalizing its covariance. Second countability is stated explicitly for the measurable pCN construction; for a separable metric space it follows from the standing setting. The projected law is the pushforward by the orthogonal projection onto $K_m$ , a reading of the Karhunen–Loève formula in the paper. A measurable map is essential here: Mathlib's pushforward returns zero for a nonmeasurable map.

The target is Mathlib's normalized tilted measure. The theorem explicitly concludes that both the infinite dimensional and projected targets are probability measures, so the possible junk zero from a nonintegrable tilt cannot satisfy the result. Wasserstein costs and Lyapunov expectations use extended nonnegative integrals. This avoids the junk zero of a nonintegrable Bochner integral and the junk values of a real infimum. Couplings are measures with the prescribed marginals. The acceptance kernel uses the paper's $1\wedge e^{\Phi(x)-\Phi(y)}$ , including the first proposal and its rejection probability.

“Sufficiently small $\varepsilon$ ” means $\exists\varepsilon_0>0\,\forall\varepsilon\in(0,\varepsilon_0]$ . The iteration count is chosen before $m$ and before the input probability measures. Positive radius, positive power exponent and positive exponential coefficient exclude empty acceptance balls and the constant Lyapunov function. The $m=0$ projection is retained as the zero dimensional subspace. Contributions that establish the Gaussian comparison, the three pCN estimates, or the abstract weak Harris statement are within scope.

Selected references

M. Hairer, A. M. Stuart and S. J. Vollmer, Spectral gaps for a Metropolis–Hastings algorithm in infinite dimensions, Annals of Applied Probability 24(6), 2014, 2455–2490. arXiv:1112.1392v4, DOI:10.1214/13-AAP982.

10 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research·Captain: mikedeng1

Explore First, Exploit Next: The True Shape of Regret in Bandit Problems III: A Strategy Smarter Than Uniform Draws Every Arm at Least (T/K)(1 − √(2T K_inf)) TimesResearch Paper

Why early exploration needs a lower bound

A stochastic multi-armed bandit learner repeatedly selects one of finitely many arms and sees only the reward from the selected arm. The learner must gather information about uncertain rewards while trying to select high-mean arms. Expected regret summarizes the lost reward relative to always selecting an optimal arm, but regret alone does not explain how much sampling each particular arm must receive. Garivier, Ménard, and Stoltz study this allocation question directly in Explore First, Exploit Next: The True Shape of Regret in Bandit Problems. Their Section 3 gives lower bounds for small horizons, before the longer-run logarithmic behavior becomes dominant.

The paper's first small-horizon result concerns strategies that allocate at least a uniform share to every optimal arm, on every problem in a specified model. This requirement excludes a strategy that always selects one fixed label and succeeds only when that label happens to be best. Such a requirement still permits many adaptive policies; it constrains their performance on optimal arms rather than prescribing their decisions round by round. The result establishes a compulsory initial allocation to every arm, including one whose mean is below the best mean. It is Theorem 2 on page 10 of the pinned arXiv:1602.07182v3.

Bandit problems, models, and strategies

A bandit problem $\underline\nu=(\nu_a)_{a=1}^K$ consists of $K$ probability laws on $\mathbb R$ . At each round, a strategy $\psi$ chooses an arm using the observed past and randomization, then receives an independent reward drawn from that arm's law. The mean reward of arm $a$ is $\mu_a=\mathbb E_{\nu_a}[X]$ . Write $\mu^*=\max_a\mu_a$ , and call an arm optimal when $\mu_a=\mu^*$ . The count $N_{\psi,a}(T)$ is the number of times arm $a$ is chosen during the first $T$ rounds. These objects and the information available to a strategy are specified in Section 1.1, pages 2–3.

A model $\mathcal D$ is a collection of possible arm laws, each a probability measure with an expectation. The notation $\underline\nu\in\mathcal D$ means that every arm law $\nu_a$ belongs to $\mathcal D$ . A strategy is smarter than uniform on $\mathcal D$ when, for every bandit problem in the model, every optimal arm $a^*$ , and every integer $T\ge1$ , it satisfies

\mathbb E_{\underline\nu}[N_{\psi,a^*}(T)]\ge\frac{T}{K}.

This is Definition 2 on page 10. It imposes a lower bound on each optimal arm, even when several arms tie. The requirement is evaluated across the whole model, so a strategy cannot be declared smarter based only on its behavior on the one problem used in the theorem.

For a law $P$ , a real threshold $x$ , and the model $\mathcal D$ , the information number $\mathcal K_{\inf}(P,x,\mathcal D)$ is the infimum of $\mathrm{KL}(P,Q)$ over those $Q\in\mathcal D$ whose mean exceeds $x$ . The infimum is $+\infty$ if there is no such $Q$ . This is the definition on page 4. It measures how close an arm law is, in Kullback–Leibler divergence, to another admissible law that would give it a mean above the present optimum.

Formalization targets

The main target is Theorem 2. For a model $\mathcal D$ , a strategy $\psi$ smarter than uniform on it, a bandit problem $\underline\nu\in\mathcal D$ , every arm $a$ , and every integer $T\ge1$ , the finite- $\mathcal K_{\inf}$ case states

\mathbb E_{\underline\nu}[N_{\psi,a}(T)]\ge \frac{T}{K}\left(1-\sqrt{2T\mathcal K_{\inf}(\nu_a,\mu^*,\mathcal D)}\right).

The theorem includes optimal and suboptimal arms. Its printed companion says that when $T\le 1/(8\mathcal K_{\inf})$ , the arm receives at least $T/(2K)$ expected selections. In the formal statement this threshold is $8T\mathcal K_{\inf}\le1$ , which also expresses the intended case $\mathcal K_{\inf}=0$ . Both claims come from Theorem 2, page 10.

The milestone list follows the source's intermediate claims. Lemma 6, page 20 bounds Bernoulli relative entropy using the maximum of $x(1-x)$ over an interval. The proof of Theorem 2 on page 11 states that Bernoulli relative entropy increases in its second argument on the interval starting at its first argument. The same page applies the paper's fundamental inequality (6) to the fraction of rounds spent on one arm, then states a lower bound against a single alternative arm law. These are the four curated milestones for the main theorem.

What the result supplies

The theorem turns a model-relative performance condition into a numerical constraint on early sampling. If an arm's law is close in divergence to a law that would make it best, then the bound keeps its expected pull count near the uniform allocation until the horizon is large enough for the term under the square root to matter. It identifies the divergence scale $1/\mathcal K_{\inf}$ at which this particular guarantee becomes weak. The paper contrasts this absolute bound with later relative and collective bounds that capture different dependencies on the number of arms in Section 3, pages 10–14.

The mathematical result is proved in the paper. The remaining work in this mission is a machine-checked development of the statement and its source-backed intermediate inequalities in the canonical stochastic-bandit model. The published bandit structure, policy kernels, and information number provide reusable foundations. Shared definitions supply the Bernoulli divergence, model predicate, and expected pull counts; the local strategy class makes the hypothesis of this particular theorem explicit. The Bernoulli inequalities and the pull-count change-of-measure statement can be reused in other lower-bound results.

Where the difficulty lies

A performance condition about optimal arms does not directly constrain an arm that is suboptimal in the problem of interest. The small-horizon bound must remain valid even though the strategy may adapt to observed rewards, and the relevant alternative arm laws can have divergences approaching an infimum without attaining it. The paper's lower bound is therefore sensitive to the exact orientation of the two bandit problems, the expected count multiplying their divergence, and the boundary conventions for Bernoulli relative entropy. Replacing the infimum with a chosen alternative or changing a divergence to an ordinary real with an arbitrary boundary value would alter the statement.

Formalization scope

Lean uses arms Fin K, indexed from zero; the paper indexes them from one. The horizon is a natural number, and counts are integrated against the probability measure on $T$ -round histories generated by a stochastic kernel policy. Such kernels represent the arm-and-reward histories induced by the paper's strategies with auxiliary randomization. The model is a set of probability measures on $\mathbb R$ whose identity function is integrable. The published StochasticBandit, BanditPolicy, and ConsistentBanditPolicy definitions supply the basic problem, history measure, pull count, means, and $\mathcal K_{\inf}$ .

Bernoulli divergence and $\mathcal K_{\inf}$ take values in $[0,+\infty]$ . The real square-root formula assumes $\mathcal K_{\inf}<+\infty$ : when it is infinite, the paper's right-hand side is $-\infty$ , while converting infinity directly to Lean's real value would produce a false numerical bound. The starting bandit problem is explicitly in $\mathcal D$ , a condition needed for the proof's use of Definition 2 on a one-arm modification, although the printed quantifier on page 10 omits it. The arm parameter guarantees $K\ge1$ ; every target assumes $T\ge1$ , so its real divisions by $K$ and $T$ have the stated meaning.

A faithful development must retain Definition 2's quantification over all model problems and each optimal arm, rather than only over the bandit problem used in the conclusion. It must use the full Bernoulli relative entropy, including infinite endpoint values, and the infimum over precisely those model laws with mean greater than $\mu^*$ . The local instance of (6) also assumes integrable arm rewards in both bandit problems, as Section 1.1 requires. Contributions that establish the four milestones, the companion threshold claim, or reusable count-integrability and divergence facts are in scope.

Selected references

Aurélien Garivier, Pierre Ménard, and Gilles Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research, 2019; arXiv:1602.07182v3.
Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, Cambridge University Press, 2020; DOI:10.1017/9781108571401. The published bandit definitions used here follow its canonical framework.

11 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research·Captain: mikedeng1

Explore First, Exploit Next: The True Shape of Regret in Bandit Problems IV: Under Pairwise Symmetry a Suboptimal Arm Is Drawn T/K Times or Almost as Often as an Optimal ArmResearch Paper

Motivation

Lower bounds for stochastic multi-armed bandits are usually stated for a large horizon: Lai and Robbins (1985) and Burnetas and Katehakis (1996) show that a consistent strategy pulls a suboptimal arm at least about $\ln T / \mathcal{K}_{\inf}$ times. These bounds say nothing about the small-horizon regime, the first rounds in which a strategy has not yet had time to separate the arms. Garivier, Ménard and Stoltz (arXiv:1602.07182v3, Mathematics of Operations Research, 2019) describe that regime through one information-theoretic inequality, their (6), and derive several lower bounds from it. This mission formalizes their relative lower bound, Theorem 3 (p. 11): under a mild symmetry assumption on the strategy, a suboptimal arm is either pulled at the uniform rate $T/K$ or, on average, almost as often as an optimal arm. It is the statement behind the title's claim that bandit strategies must first explore.

Setting

There are $K$ arms. A bandit problem $\underline{\nu} = (\nu_1, \dots, \nu_K)$ assigns to each arm $a$ a probability distribution $\nu_a$ on $\mathbb{R}$ with expectation $\mu_a$ . The optimal mean is $\mu^\star = \max_a \mu_a$ , the gap of arm $a$ is $\Delta_a = \mu^\star - \mu_a$ ; arm $a$ is optimal if $\Delta_a = 0$ and suboptimal if $\Delta_a > 0$ .

A model $\mathcal{D}$ is a set of distributions on $\mathbb{R}$ , each with an expectation; a bandit problem is in $\mathcal{D}$ when every $\nu_a$ belongs to $\mathcal{D}$ .

At each round $t$ a strategy $\psi$ picks an arm $A_t$ , possibly at random, as a function of the past arms and rewards, and receives a reward $Y_t$ drawn from $\nu_{A_t}$ . The number of pulls of arm $a$ in the first $T$ rounds is

N_{\psi,a}(T) = \sum_{t=1}^{T} \mathbb{1}\{A_t = a\},

and $\mathbb{E}_{\underline{\nu}}$ denotes expectation when $\psi$ plays against $\underline{\nu}$ . Write $N^+_{\psi,a}(T) = \max\{N_{\psi,a}(T), 1\}$ .

Kullback–Leibler divergence. $\mathrm{KL}(P, Q) \in [0, +\infty]$ is the Kullback–Leibler divergence between distributions, and $\mathrm{kl}(p, q)$ the divergence between Bernoulli laws of parameters $p$ and $q$ .

Pairwise symmetry (Definition 3, p. 11). A strategy $\psi$ is pairwise symmetric for optimal arms on $\mathcal{D}$ if for every bandit problem $\underline{\nu}$ in $\mathcal{D}$ , every pair of optimal arms $a^\star, a_\star$ with $\nu_{a^\star} = \nu_{a_\star}$ and every $T \ge 1$ , the pairs $(N_{\psi,a^\star}(T), N_{\psi,a_\star}(T))$ and $(N_{\psi,a_\star}(T), N_{\psi,a^\star}(T))$ have the same distribution. A strategy that uses only the observed payoffs, and not the labels of the arms, has this property.

Formalization targets

Goal: Theorem 3 (p. 11)

For every model $\mathcal{D}$ , every strategy $\psi$ pairwise symmetric for optimal arms on $\mathcal{D}$ , every bandit problem $\underline{\nu}$ in $\mathcal{D}$ , every suboptimal arm $a$ , every optimal arm $a^\star$ with $\mathrm{KL}(\nu_a, \nu_{a^\star}) < \infty$ and every $T \ge 1$ ,

\mathbb{E}_{\underline{\nu}}\big[N_{\psi,a}(T)\big] \ge \frac{T}{K} \quad\text{or}\quad \mathbb{E}_{\underline{\nu}}\left[\frac{N^+_{\psi,a}(T)}{N^+_{\psi,a^\star}(T)}\right] \ge 1 - 2\sqrt{\frac{2T\,\mathrm{KL}(\nu_a, \nu_{a^\star})}{K}} .

Companion: the "in particular" clause

For $T \le K / (32\,\mathrm{KL}(\nu_a, \nu_{a^\star}))$ the second alternative becomes $\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}(T)/N^+_{\psi,a^\star}(T)] \ge 1/2$ .

Milestones (p. 12)

The symmetry identity: for the alternative problem $\underline{\nu}'$ obtained by replacing $\nu_a$ by $\nu_{a^\star}$ , $\mathbb{E}_{\underline{\nu}'}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})] = 1/2$ .
Inequality (12): $\mathbb{E}_{\underline{\nu}}[N_{\psi,a}(T)]\,\mathrm{KL}(\nu_a, \nu'_a) \ge \mathrm{kl}\big(\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})], 1/2\big)$ .
The Jensen display: $\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})] \le r/(1+r)$ with $r = \mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/N^+_{\psi,a^\star}]$ .
The bound $r/(1+r) \ge 1/2 - \sqrt{T\,\mathrm{KL}(\nu_a,\nu'_a)/(2K)}$ in the case $\mathbb{E}_{\underline{\nu}}[N_{\psi,a}(T)] \le T/K$ , $r \le 1$ .

Significance

The theorem shows that in the initial phase a symmetric strategy cannot discard a suboptimal arm quickly: unless the arm is already sampled at the uniform rate, it is sampled, in ratio, nearly as often as an optimal arm, as long as $T$ is small compared with $K / \mathrm{KL}(\nu_a, \nu_{a^\star})$ . Together with Theorem 2 (absolute lower bound) and Theorem 4 (collective lower bound) it describes the regret curve before the logarithmic regime: roughly linear growth, then a transition. It requires no assumption on the model beyond the existence of expectations, and it involves the divergence between the two arms themselves rather than the model-dependent quantity $\mathcal{K}_{\inf}$ .

The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a Lean statement of Theorem 3 on the canonical bandit model already used on the platform (StochasticBandit, BanditPolicy), a formal version of the symmetry assumption that sibling missions reuse (mission V, the collective lower bound, uses the same Definition 3), and the four intermediate steps of the proof as separate targets.

Difficulty

The proof compares $\underline{\nu}$ with an alternative problem $\underline{\nu}'$ that differs from it only in arm $a$ , and transfers information between them through the fundamental inequality (6) of §2, a data-processing argument on the law of the whole history. The step specific to Theorem 3 is the choice of the test variable: the expectation of $N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})$ is known exactly under $\underline{\nu}'$ only because the strategy is pairwise symmetric, and the symmetry is a statement about joint laws of pull counts, not about their expectations. A version of the assumption that only equates expected pull counts does not determine the expectation of this ratio. The ratio expectation then has to be extracted from a bound on $\mathbb{E}[x/(1+x)]$ , which needs Jensen's inequality in the right direction and a case split on whether $r \le 1$ .

Formalization scope

Arms are Fin K (0-based). The horizon $T$ is a natural number. A strategy is a published BanditPolicy: a family of Markov kernels from the observed history of (arm, reward) pairs to the next arm. Every strategy of the paper, which may use auxiliary uniform random variables, induces such a kernel with the same law of arms and rewards. The law of the history is the published banditMeasure, and $N_{\psi,a}(T)$ is the published armPullCount. The model is a set of measures on $\mathbb{R}$ , and every statement assumes the paper's standing hypothesis (§1.1, p. 3) that each member is a probability measure with an integrable identity, together with $\underline{\nu}$ in $\mathcal{D}$ .

Committed conventions:

$\mathrm{KL}$ and $\mathrm{kl}$ take values in $[0, +\infty]$ ; the Bernoulli divergence is the Kullback–Leibler divergence of two Bernoulli laws on $\mathbb{R}$ , not a real formula with finite values at $q \in \{0, 1\}$ .
Theorem 3 adds the hypothesis $\mathrm{KL}(\nu_a, \nu_{a^\star}) < \infty$ . When the divergence is infinite the paper's bound reads $\ge -\infty$ and is empty; reading $+\infty$ as the real number $0$ would make the statement false.
The "in particular" clause is stated as $32\,T\,\mathrm{KL}(\nu_a,\nu_{a^\star}) \le K$ in $[0, +\infty]$ , which needs no finiteness assumption.
Definition 3 is an equality of joint laws (push-forwards of the history law), for every $T \ge 1$ , only for optimal arms of problems in $\mathcal{D}$ with equal distributions. Invariance under all permutations of the arms would strengthen the hypothesis and weaken the theorem.
Ratios use $\max\{N, 1\}$ as real numbers, so no division by zero occurs; all integrands are bounded by $T$ .

A formalization in which the symmetry assumption equates only expected pull counts, in which the divergence is a real number with junk value $0$ at $+\infty$ , or in which the disjunction is replaced by its second alternative, is not this theorem.

The mission builds on the published definitions StochasticBandit and BanditPolicy. A complete development needs the fundamental inequality (6) for kernel policies (the divergence decomposition, published as BanditAlgorithm.bandit_divergence_decomposition, plus data processing for the Bernoulli test), Pinsker's inequality for Bernoulli laws (proved on the platform as BanditAlgorithm.bernoulli_relative_entropy_pinsker), Jensen's inequality for concave functions (Mathlib), and a lemma that the law of the history is unchanged in distribution when two identically distributed optimal arms are relabelled. The measurability of pull counts and the relation between the extended-real and real Bernoulli divergences are reusable beyond this mission. Proofs of any milestone, and of the general fundamental inequality, are welcome.

Selected references

A. Garivier, P. Ménard, G. Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research 44(2), 2019. arXiv:1602.07182v3, doi:10.1287/moor.2017.0928
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6(1), 1985. doi:10.1016/0196-8858(85)90002-8
A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Advances in Applied Mathematics 17(2), 1996. doi:10.1006/aama.1996.0007
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. doi:10.1017/9781108571401

8 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research·Captain: mikedeng1

Explore First, Exploit Next: The True Shape of Regret in Bandit Problems II: Uniformly Fast Convergent Strategies Draw Every Suboptimal Arm at Least ln T / K_inf Times AsymptoticallyResearch Paper

Why this lower bound matters

In a stochastic multi-armed bandit, a player repeatedly chooses one of finitely many arms and sees only the reward from the chosen arm. To earn a high reward, the player must favor arms that appear best. Yet an arm that currently appears inferior might be best under another plausible reward law. That uncertainty forces any strategy with uniformly strong long-run performance to keep testing apparently inferior arms. The asymptotic number of tests is a basic benchmark for comparing bandit algorithms: an algorithm that matches the bound uses no more exploration than the information in the model demands. Garivier, Ménard, and Stoltz restate this general benchmark as Theorem 1 and derive it within their analysis of the shape of regret Garivier–Ménard–Stoltz, §2.2.

The quantity controlling the benchmark comes from Burnetas and Katehakis. It measures the least information needed to replace one suboptimal arm by a plausible arm that is strictly better than the current best. The paper cites their quantity on page 4, and its Theorem 1 applies it to every suboptimal arm separately Garivier–Ménard–Stoltz, pp. 4, 9. This per-arm form matters when different arms have different reward laws and different amounts of information are needed to rule them out.

Bandit setting and notation

A bandit problem $\underline\nu=(\nu_a)_{a=1}^K$ has $K$ arms. Each $\nu_a$ is a probability distribution on real rewards with a finite expectation $\mu_a=\mathbb E_{\nu_a}X$ . A strategy $\psi$ chooses an arm at each round using the preceding chosen arms and observed rewards, and it may randomize. Let $N_{\psi,a}(T)$ be the number of times arm $a$ is chosen in the first $T$ rounds. The optimal mean is $\mu^\star=\max_a\mu_a$ , and the gap of arm $a$ is $\Delta_a=\mu^\star-\mu_a$ . An arm is suboptimal when $\Delta_a>0$ . These are the objects of §1.1 of the paper Garivier–Ménard–Stoltz, pp. 2–3.

A model $\mathcal D$ is a collection of possible real-valued reward distributions, each with a finite expectation. A bandit problem belongs to $\mathcal D$ when every one of its arm laws does. The Kullback–Leibler divergence $\mathrm{KL}(P,Q)$ measures the information discrepancy from one reward law $P$ to another $Q$ ; it may be infinite. For an arm law $P$ and a real threshold $x$ , define the minimal information cost

\mathcal K_{\inf}(P,x,\mathcal D) =\inf\{\mathrm{KL}(P,Q):Q\in\mathcal D,\ \mathbb E_QX>x\}.

The infimum is $+\infty$ if there is no qualifying alternative. The strict inequality in the set matters: the replacement law must make the arm better than the original optimal mean, not merely tied with it Garivier–Ménard–Stoltz, p. 4.

Definition 1 calls $\psi$ uniformly fast convergent on $\mathcal D$ when, on every bandit problem in the model, the expected draw count of every suboptimal arm grows more slowly than $T^\alpha$ for each $0<\alpha\le1$ :

\mathbb E_{\underline\nu}N_{\psi,a}(T)=o(T^\alpha).

Here $T$ tends to infinity through integer horizons. This condition is uniform in which problem and suboptimal arm are considered; it does not mean one numerical convergence rate is shared by all problems Garivier–Ménard–Stoltz, p. 9, Definition 1.

Formalization target

The goal is the paper's Theorem 1: for every model $\mathcal D$ , every uniformly fast convergent strategy $\psi$ , every bandit problem $\underline\nu$ in the model, and every suboptimal arm $a$ ,

\liminf_{T\to\infty} \frac{\mathbb E_{\underline\nu}N_{\psi,a}(T)}{\ln T} \ge\frac1{\mathcal K_{\inf}(\nu_a,\mu^\star,\mathcal D)}.

The bound states the minimum logarithmic exploration of each arm. It leaves the model and strategy arbitrary within the stated class. The milestones follow four statements from the proof on page 9: the Bernoulli entropy estimate in (11), the one-arm divergence chain in (10), the eventual bound on draws of the alternative's other arms, and the bound for one alternative law before taking the infimum. Their source text is recorded beside the local drafts Garivier–Ménard–Stoltz, p. 9.

What the result gives

If $\mathcal K_{\inf}$ is finite and positive, the theorem gives a concrete coefficient of $\ln T$ that any uniformly fast convergent strategy must spend on arm $a$ . A small information cost means that the arm is hard to distinguish from a better alternative and must be sampled more often. If the cost is infinite because the model contains no better replacement, the reciprocal is zero and the bound makes no positive demand. If the cost is zero, the reciprocal is infinite: the normalized expected draw count must diverge. The extended-value convention is part of the target, not a choice of a finite stand-in Garivier–Ménard–Stoltz, pp. 4, 9.

The theorem is proved in the paper, while the Lean statements in this proposal are proof targets. A completed development would supply a machine-checked bridge from the canonical stochastic-bandit policy model through Bernoulli relative entropy and change of measure to the per-arm asymptotic claim. Its model and divergence definitions can also support lower bounds for other bandit classes. The existing Prove2Me StochasticBandit, BanditPolicy, and ConsistentBanditPolicy definitions provide the bandit law, policy, draw count, means, and $\mathcal K_{\inf}$ used here; Definition 1's exact strategy class is supplied locally.

Difficulty

The central issue is the quantification over every alternative law in an arbitrary model. A suboptimal arm may become uniquely optimal after changing only its law, while the strategy must remain uniformly fast on that new problem. The information cost is an infimum over such changes, including an empty set or costs arbitrarily close to zero. A statement that reasons about just one convenient alternative does not yield the coefficient in Theorem 1. The proof also passes from finite-horizon information inequalities to a liminf as $T$ grows, so endpoint values of Bernoulli divergence and the extended-value arithmetic must agree with the source Garivier–Ménard–Stoltz, pp. 6, 9.

Formalization scope

Lean indexes the paper's arms $1,\ldots,K$ by Fin K, starting at zero, and uses natural-number horizons. A strategy is a history-dependent Markov kernel, whose generated probability measure describes the sequence of chosen arms and rewards. The pull count is bounded by $T$ , so its expectation is a genuine Bochner integral. The model explicitly requires probability laws with integrable identity; this ensures that each mean in $\mathcal K_{\inf}$ is genuine. Bernoulli relative entropy and arm-law KL take values in extended nonnegative reals. The goal's liminf is also in extended nonnegative reals, avoiding a default real liminf for an unbounded sequence. The first two horizons, where $\ln T\le0$ , cannot affect an asymptotic liminf.

The theorem sentence on page 9 says “all bandit problems” without restricting the original problem to $\mathcal D$ . Its proof applies Definition 1 to that problem, so the proposal states that its arms belong to $\mathcal D$ . Without this condition a strategy can behave arbitrarily outside the model. The source's other standing conventions are kept: every reward law has an expectation, the improvement condition in $\mathcal K_{\inf}$ is strict, and uniform fast convergence ranges over all model problems, all suboptimal arms, and all $0<\alpha\le1$ . These choices rule out an empty strategy class or a special hard-coded bandit as a trivial route to the target.

Useful contributions include the finite-horizon change-of-measure inequality, endpoint-correct Bernoulli KL estimates, identities for sums of expected pull counts, and asymptotic lemmas for reciprocal infima. The milestone drafts identify the paper statements those contributions must support.

Selected references

Aurélien Garivier, Pierre Ménard, and Gilles Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research, 2019; cited here from arXiv:1602.07182v3, §§1–2.
Apostolos N. Burnetas and Michael N. Katehakis, Optimal Adaptive Policies for Sequential Allocation Problems, Advances in Applied Mathematics, 1996. DOI:10.1006/aama.1996.0007.

9 thms2 active usersReviewed

Completed

Machine Learning Reinforcement Learning·Captain: mikedeng1

The Statistical Complexity of Interactive Decision Making IV: Log-Loss Regret Controls Hellinger Estimation Error, Est_H ≤ Reg_KL + 2 log(1/δ) with Probability 1−δResearch Paper

Motivation

Interactive decision methods often need an estimate of an unknown outcome law after each round. A learner can be good at decisions only if its model of the observations is accurate where future decisions will sample. Foster, Kakade, Qian and Rakhlin measure this accuracy by a cumulative squared Hellinger distance and use it in their regret bounds for decision making with structured observations. They connect that estimation quantity to online log-loss regret, a standard objective for sequential probability prediction. The connection lets a regret guarantee for a density predictor supply the estimation guarantee needed by a decision method. Foster et al., Appendix A.3 and §4.1.1.

This mission isolates the online estimation result, Lemma A.14, from the rest of the paper. It addresses a learner that predicts a conditional outcome distribution before the next covariate and outcome are revealed. The covariates may respond to the entire preceding history. This matters in interactive decision making, where the learner's earlier choices change what it observes next. Foster et al., pp. 75–76.

Setting

There are $T$ rounds. At round $t$ , the learner has a history $H_{<t}=((x_s,y_s))_{s<t}$ of past covariates and outcomes. It predicts a probability distribution $\widehat g_t(\cdot\mid x;H_{<t})$ for every possible next covariate $x$ . Nature draws $x_t$ from a history-dependent distribution $c_t(\cdot\mid H_{<t})$ , then draws $y_t$ from the conditional law of a distinguished true expert $i^\star$ . An expert class indexed by $I$ supplies laws $g_{i,t}(\cdot\mid x;H_{<t})$ ; realizability means $g_{i^\star,t}$ is the actual outcome law at every round. The prediction $\widehat g_t$ is selected from the past history, before $x_t$ is observed. Foster et al., Assumption A.1, p. 76.

For a predicted distribution $q$ , the log loss on observation $y$ is $-\log q(y)$ . The learner's log-loss regret $\mathrm{Reg}_{\mathrm{KL}}$ is its cumulative log loss minus the smallest cumulative loss of an expert in $I$ . This is a realized quantity: both sums use the covariates and outcomes that actually occurred. The squared Hellinger distance is

D_{\mathrm H}^2(P,Q)=\sum_y\bigl(\sqrt{P(y)}-\sqrt{Q(y)}\bigr)^2.

The Hellinger estimation error $\mathrm{Est}_{\mathrm H}$ is different from a sum evaluated only at realized covariates. At each round it averages $D_{\mathrm H}^2(\widehat g_t(\cdot\mid x),g_{i^\star,t}(\cdot\mid x))$ over the conditional law of the next covariate $x$ , given $H_{<t}$ , then sums these conditional errors. Thus the error measures prediction quality in the distribution the learner is about to face. Foster et al., (99)–(100), pp. 75–76.

Formalization targets

Main high-probability bound

The main target is Lemma A.14 (102): for every $\delta\in(0,1)$ ,

\Pr\!\left\{\mathrm{Est}_{\mathrm H} \le \mathrm{Reg}_{\mathrm{KL}}+2\log(1/\delta)\right\}\ge 1-\delta.

The coefficient $2$ and the absence of a factor $1/2$ in $D_{\mathrm H}^2$ are part of the claim. The probability is under the complete history law generated by the adaptive covariate process and the true expert. Foster et al., Lemma A.14, p. 76.

Supporting results

The first milestone is Lemma A.4, an anytime conditional exponential-moment bound. It controls one event on which an adapted inequality fails at any horizon through $T$ , without replacing it by a single fixed-horizon claim. The second milestone is the affinity identity used in the proof of Lemma A.14:

\sum_y\sqrt{P(y)Q(y)}=1-\tfrac12D_{\mathrm H}^2(P,Q).

The proposal also states the expectation clause $\mathbb E[\mathrm{Est}_{\mathrm H}]\le\mathbb E[\mathrm{Reg}_{\mathrm{KL}}]$ from (101) and the predictable-mask clause (103), which bounds error accumulated only on rounds selected from the past. Foster et al., pp. 70, 76, 79.

Significance

The high-probability bound lets an online density estimator serve as an estimation oracle for the paper's interactive decision bounds. A user can choose a predictor because it has a log-loss regret guarantee, then obtain control of Hellinger estimation error under adaptive observations. The expectation clause supplies the corresponding average guarantee. The masked clause handles applications that evaluate accuracy only on rounds selected before the current observation. Foster et al., Proposition 4.1 and Lemma A.14.

The result is already proved in the source paper. This mission asks for machine-checked proofs of the finite-alphabet statements and a reusable interface for sequential probability kernels, conditional error and log-loss regret. The published FoundationsRL Hellinger definition supplies the same normalization used by the paper; the mission does not propose a new distance. These items have no machine-checked proof in this proposal yet. The source also gives Vovk's aggregation guarantee for finite expert classes, but that algorithmic bound is outside the current item list. Foster et al., Lemma A.15, p. 76.

Difficulty

The quantity to be bounded is conditional on the past. A pathwise distance at the observed $x_t$ is a different random quantity and does not give (102). Adaptive covariates add another dependence on history, while the learner must choose its prediction before seeing $x_t$ . A fixed covariate law would therefore omit a central feature of the theorem. The anytime milestone likewise concerns all prefixes of one process at once; separate claims at each fixed horizon do not preserve its statement. Foster et al., pp. 70, 75–79.

The log-loss formula also has a boundary. A zero predicted probability gives infinite loss in the paper, whereas Lean's real logarithm returns a finite default at zero. The formal statements must keep that default from affecting a positive-probability observation. Squared Hellinger distance has its own normalization convention, so the affinity identity checks the factor needed in the high-probability constant.

Formalization scope

The paper uses measurable covariate and outcome spaces and regular conditional densities. This mission specializes to finite covariates $X$ , finite outcomes $Y$ , and a finite nonempty expert class $I$ . Each kernel is represented by a nonnegative vector summing to one. Complete histories are finite sequences, and the probability of a history is the product of its covariate and true-expert outcome probabilities. Expectations and event probabilities are finite sums. Time is indexed from zero; round $t$ in Lean corresponds to round $t+1$ in the paper.

The learner, experts and covariate kernel may all depend on preceding history. The learner and experts predict a law for every possible covariate while seeing only that history. A Boolean mask for (103) has the same information restriction. The Hellinger error sums conditional averages over the next covariate, and the probability guarantee is expressed as a bound on the total mass of histories where the displayed inequality fails.

The real-valued log loss requires one additional condition: on every complete history of positive probability, the learner and every expert give the observed outcome positive probability at every round. The condition is imposed only where the history law has support. It excludes Lean's default value for $\log 0$ ; it is a scope restriction from the paper's extended-valued formulation. A normalized history law and a distinguished true expert are explicit, so the probability statement cannot be discharged by an empty event space or an unnormalized zero law. The sequential-kernel definitions can be reused in other finite online learning results, and the probability, affinity, expectation and masked bounds are separate proof targets.

Selected references

Dylan J. Foster, Sham M. Kakade, Jian Qian, Alexander Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint arXiv:2112.13487v3, 2023. arXiv.

8 thms2 active usersReviewed

Completed

Information Theory Machine Learning·Captain: mikedeng1

The Statistical Complexity of Interactive Decision Making I: Subadditivity of Squared Hellinger Distance for Sequential Laws, D²_H(P,Q) ≤ 10² log(n)·E_P[Σᵢ D²_H(P⁽ⁱ⁾, Q⁽ⁱ⁾)] for n ≥ 2Research Paper

Motivation

Lower bounds for interactive decision making (bandits, reinforcement learning, and the general decision making with structured observations framework of Foster, Kakade, Qian and Rakhlin, arXiv:2112.13487) compare what a learner observes under two different environments. A learner's whole interaction history is generated one step at a time: each observation is drawn from a conditional law that depends on everything seen before. Statistical estimation guarantees, by contrast, are stated one step at a time, as bounds on the divergence between the conditional laws at each round. Passing from the per-step guarantees to a statement about the laws of entire histories requires a chain rule for the divergence in use.

For the Kullback–Leibler divergence the chain rule is an identity. The paper's guarantees, however, are stated in the squared Hellinger distance, which is bounded, symmetric, and the natural loss for density estimation with the logarithmic loss. Hellinger distance has no exact chain rule. Lemma A.13 of the paper (App. A.2, p. 73) supplies an approximate one, losing a factor logarithmic in the number of steps, and the paper uses it in the proof of its main regret lower bound (Theorem 3.2, via App. C.1.3).

Setting

Fix $n \in \mathbb N$ and finite sets $\mathcal X_1, \dots, \mathcal X_n$ . A sequence is $x = (x_1, \dots, x_n)$ with $x_i \in \mathcal X_i$ , and $x_{1:i-1} = (x_1, \dots, x_{i-1})$ denotes its prefix; $\mathcal X^{(i-1)} = \prod_{t=1}^{i-1} \mathcal X_t$ .

For probability distributions $p, q$ on a finite set, the squared Hellinger distance, the Hellinger distance and the Kullback–Leibler divergence are

D^2_{\mathrm H}(p, q) = \sum_a \big(\sqrt{p(a)} - \sqrt{q(a)}\big)^2, \qquad D_{\mathrm H} = \sqrt{D^2_{\mathrm H}}, \qquad D_{\mathrm{KL}}(p\,\|\,q) = \sum_a p(a) \log\frac{p(a)}{q(a)},

the last one set to $+\infty$ when $p$ charges a point that $q$ does not. Note that the paper's $D^2_{\mathrm H}$ carries no factor $\tfrac12$ , so $0 \le D^2_{\mathrm H} \le 2$ .

A family of sequential kernels $P = (P^{(i)})_{i=1}^n$ assigns to each $i$ and each prefix $x_{1:i-1}$ a probability distribution $P^{(i)}(\cdot \mid x_{1:i-1})$ on $\mathcal X_i$ . Its sequential law is the law of $X_1, \dots, X_n$ under $X_i \sim P^{(i)}(\cdot \mid X_{1:i-1})$ :

\mathbb P(x) = \prod_{i=1}^n P^{(i)}(x_i \mid x_{1:i-1}).

For a second family $Q$ with law $\mathbb Q$ , the quantity controlled by per-step estimation is

\mathbb E_{\mathbb P}\Big[\sum_{i=1}^n D^2_{\mathrm H}\big(P^{(i)}(\cdot \mid X_{1:i-1}), Q^{(i)}(\cdot \mid X_{1:i-1})\big)\Big].

In Lean these are IsSeqKernel, seqLaw and condHellingerSum, with hellingerSq and klDivDiscrete the published discrete divergences.

Formalization targets

Goal: Lemma A.13, (97), for $n \ge 2$

D^2_{\mathrm H}(\mathbb P, \mathbb Q) \le 10^2 \log(n) \cdot \mathbb E_{\mathbb P}\Big[\sum_{i=1}^n D^2_{\mathrm H}\big(P^{(i)}(\cdot \mid X_{1:i-1}), Q^{(i)}(\cdot \mid X_{1:i-1})\big)\Big].

The constant $10^2$ is the paper's; the shape that matters downstream is the logarithmic dependence on $n$ with no assumption on the kernels beyond their being probability kernels.

Companion: Lemma A.13, (98)

If $V \ge e$ and $P^{(i)}(A \mid x_{1:i-1}) \le V\, Q^{(i)}(A \mid x_{1:i-1})$ for every $i$ , prefix and event $A$ , then $D^2_{\mathrm H}(\mathbb P, \mathbb Q) \le 3\log(V) \cdot \mathbb E_{\mathbb P}[\sum_i D^2_{\mathrm H}(P^{(i)}, Q^{(i)})]$ .

Milestones

Lemma A.10 (p. 72): $D_{\mathrm{KL}}(p\,\|\,q) \le (2 + \log V)\, D^2_{\mathrm H}(p, q)$ under a likelihood-ratio bound $V$ (referenced, finite case).
Lemma A.5 (p. 71): $D^2_{\mathrm{TV}} \le D^2_{\mathrm H} \le D_{\mathrm{KL}}$ (referenced, finite case).
The triangle inequality for $D_{\mathrm H}$ (proof of Lemma A.13, p. 73).
The chain rule $D_{\mathrm{KL}}(\mathbb Q\,\|\,\mathbb P) = \mathbb E_{\mathbb Q}[\sum_i D_{\mathrm{KL}}(Q^{(i)}\,\|\,P^{(i)})]$ for sequential laws (p. 73).
Convexity of $D^2_{\mathrm H}$ in its second argument (p. 74).
Lemma A.11 (p. 72), the multiplicative Pinsker-type inequality: $|\mathbb E_P h - \mathbb E_Q h| \le \sqrt{2R(\mathbb E_P h + \mathbb E_Q h) D^2_{\mathrm H}(P, Q)}$ and $\mathbb E_P h \le 3\mathbb E_Q h + 4R\, D^2_{\mathrm H}(P, Q)$ for $0 \le h \le R$ .

Significance

The result. Inequality (97) converts per-round Hellinger estimation error into a bound on the Hellinger distance between the laws of complete interaction histories, under no boundedness assumption on likelihood ratios. In the paper this is the step that lets the lower bound of Theorem 3.2 relate any algorithm's behaviour under a reference model to its behaviour under alternatives, and hence express the minimax regret through the decision-estimation coefficient. Without it, only the KL chain rule is available, which requires bounded likelihood ratios (the situation of (98)) or loses more than a logarithmic factor. Lemma A.11, a milestone here, is used independently in the same lower bound and in the paper's tabular reinforcement learning analysis.

Formalizing it. The lemma is proved in the paper; no machine-checked proof exists. The published layer on the platform has the discrete divergences and the comparisons of Lemmas A.5 and A.10; the sequential-law objects, the triangle inequality, the convexity of $D^2_{\mathrm H}$ , the discrete chain rule and Lemma A.11 are new. A completed development gives a reusable chain-rule toolkit for any later formalization of lower bounds over adaptive interaction histories.

Difficulty

The squared Hellinger distance does not tensorize along adaptive sequences: the natural attempt to write $1 - \tfrac12 D^2_{\mathrm H}(\mathbb P, \mathbb Q)$ as a product of conditional affinities fails because the conditional affinities are random, depending on the prefix, and their expectation does not factor. Bounding $D^2_{\mathrm H}$ by $D_{\mathrm{KL}}$ and applying the KL chain rule fails in the other direction: the conditional KL divergences are not controlled by the conditional Hellinger distances unless the likelihood ratios are bounded, and in (97) they are not. The difficulty is to obtain a bound that pays only $\log n$ for an unbounded ratio, with explicit constants that survive the final numerical comparison.

Formalization scope

Finite alphabets. The paper works over measurable spaces. This mission formalizes the finite-alphabet case, as the published FoundationsRL divergence layer does: each $\mathcal X_i$ is a Fintype, distributions are probability vectors, expectations are finite sums. Coordinates are indexed by Fin n (0-based) and the alphabets may differ from coordinate to coordinate.
Kernels. A kernel family is a function P i x of the whole sequence that is a probability vector and depends only on the coordinates j < i; this is what makes seqLaw P the law the paper describes.
Added hypothesis $n \ge 2$ in (97). The paper states (97) for every $n$ ; at $n = 1$ the right side vanishes because $\log 1 = 0$ while the left side is positive whenever $P^{(1)} \ne Q^{(1)}$ , and the proof's last step $2(6\log(96n) + \tfrac{18}{96n}) \le 10^2\log n$ holds only for $n \ge 2$ . The goal is stated for $n \ge 2$ , with the constant unchanged.
Likelihood ratios are stated multiplicatively, $P(A) \le V\,Q(A)$ , so that a zero denominator does not make a hypothesis vacuous; KL divergences are compared to Hellinger distances in $[0, \infty]$ .
Lemma A.11 holds "almost surely under $P$ and $Q$ ", which becomes: $0 \le h \le R$ at every point charged by $P$ or $Q$ .
Ruling out trivial forms. The goal's hypotheses are satisfiable with $\mathbb P \ne \mathbb Q$ and $n \ge 2$ (checked in a sanity file). A formalization in which the kernels may read coordinates beyond the prefix, in which $\log$ is applied to $n \le 1$ , or in which the ratio bound of (98) is checked through a quotient that is vacuous at zero denominators, is not the paper's statement.

Contributions welcome: proofs of any milestone and of the fact that seqLaw is a probability vector.

Selected references

D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv:2112.13487v3, 2023. https://arxiv.org/abs/2112.13487
Y. Yang, A. Barron, An asymptotic property of model selection criteria, IEEE Transactions on Information Theory 44(1), 1998. https://doi.org/10.1109/18.650993
Y. Polyanskiy, Y. Wu, Lecture Notes on Information Theory, 2014. https://people.lids.mit.edu/yp/homepage/data/itlectures_v5.pdf
D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv:2312.16730v1, 2023. https://arxiv.org/abs/2312.16730

9 thms2 active usersReviewed

Convex Optimization Random Matrix Theory·Captain: mikedeng1

Noisy Matrix Completion: Understanding Statistical Guarantees for Convex Relaxation via Nonconvex Optimization: Convex Relaxation Attains Near-Optimal Frobenius, Entrywise and Spectral Norm ErrorsResearch Paper

Motivation

Matrix completion asks for a low-rank matrix from a small random subset of its entries. It models collaborative filtering (recommendation systems), sensor-network localisation, and structure from motion. In practice the revealed entries are corrupted by noise, and the most widely used estimator is nuclear-norm regularized least squares: fit the observed entries in squared error while penalizing the sum of singular values. The estimator is a convex program, so it is solved reliably by proximal and singular-value-thresholding methods, and it needs no knowledge of the rank.

Its statistical accuracy was not understood. In the noiseless case, convex relaxation recovers the matrix exactly from nearly the information-theoretic minimum number of samples (Candès–Recht 2009, Candès–Tao 2010, Gross 2011). With noise, the available bounds for the plain convex program (Candès–Plan 2010) give $\|Z_{\rm cvx}-M^\star\|_F\lesssim\sigma n^{3/2}$ under random noise. That can be a factor of order $\sqrt{n^2p}$ above the oracle lower bound, and the numerical performance of the program is far better. Sharper rates were known only for modified estimators: Negahban–Wainwright 2012 add a spikiness constraint, Koltchinskii–Lounici–Tsybakov 2011 use a different estimator. In 2019, Chen, Chi, Fan, Ma and Yan (arXiv:1902.07698; SIAM J. Optim. 30(4), 2020, doi:10.1137/19M1290000) showed that the unmodified convex program attains near-optimal error in the Frobenius, entrywise and spectral norms simultaneously. Their argument goes through nonconvex gradient descent. This mission formalizes that theorem.

Setting

The unknown matrix is $M^\star\in\mathbb R^{n\times n}$ of rank $r\ge1$ , with singular value decomposition $M^\star=U^\star\Sigma^\star V^{\star\top}$ . The columns of $U^\star,V^\star\in\mathbb R^{n\times r}$ are orthonormal, and $\Sigma^\star=\mathrm{diag}(\sigma^\star_1,\dots,\sigma^\star_r)$ with $\sigma_{\max}=\max_k\sigma^\star_k$ , $\sigma_{\min}=\min_k\sigma^\star_k>0$ and condition number $\kappa=\sigma_{\max}/\sigma_{\min}$ . Write $\|A\|_{2,\infty}$ for the largest Euclidean norm of a row of $A$ . $M^\star$ is $\mu$ -incoherent if $\|U^\star\|_{2,\infty}\le\sqrt{\mu r/n}$ and $\|V^\star\|_{2,\infty}\le\sqrt{\mu r/n}$ (Definition 1). Incoherence says that the energy of $M^\star$ is not concentrated on a few rows or columns.

Under Assumption 1, each index $(i,j)$ enters the observed set $\Omega$ independently with probability $p$ . One observes $M_{ij}=M^\star_{ij}+E_{ij}$ for $(i,j)\in\Omega$ , where the $E_{ij}$ are i.i.d., zero-mean, and have sub-Gaussian norm $\|E_{ij}\|_{\psi_2}=\sup_{q\ge1}q^{-1/2}(\mathbb E|E_{ij}|^q)^{1/q}\le\sigma$ . Let $\mathcal P_\Omega$ keep the entries indexed by $\Omega$ and zero the rest. The convex estimator is any minimizer $Z_{\rm cvx}$ of

g(Z)=\tfrac12\|\mathcal P_\Omega(Z-M)\|_F^2+\lambda\|Z\|_*,\qquad\lambda=C_\lambda\sigma\sqrt{np},\qquad(3)

Formalization targets

Goal: Theorem 2

Suppose $n^2p\ge C\kappa^4\mu^2r^2n\log^3n$ and $\sigma\sqrt{n/p}\le c\,\sigma_{\min}/\sqrt{\kappa^4\mu r\log n}$ . Then with probability $1-O(n^{-3})$ , every minimizer of (3) satisfies

\|Z_{\rm cvx}-M^\star\|_F\lesssim\kappa\tfrac{\sigma}{\sigma_{\min}}\sqrt{\tfrac np}\|M^\star\|_F,\quad\|Z_{\rm cvx}-M^\star\|_\infty\lesssim\sqrt{\kappa^3\mu r}\tfrac{\sigma}{\sigma_{\min}}\sqrt{\tfrac{n\log n}p}\|M^\star\|_\infty,\quad\|Z_{\rm cvx}-M^\star\|\lesssim\tfrac{\sigma}{\sigma_{\min}}\sqrt{\tfrac np}\|M^\star\|.

Every best rank- $r$ approximation $Z_{{\rm cvx},r}$ is within $n^{-3}\frac\sigma{\sigma_{\min}}\sqrt{n/p}\,\|M^\star\|$ of $Z_{\rm cvx}$ in Frobenius norm, and satisfies the same three bounds.

Milestones

Deterministic layer: Lemma 20 (balancing an SVD factorization), Claim 3, Claim 2 and Lemma 2. Lemma 2 says that a point $(X,Y)$ with $\|\nabla f(X,Y)\|_F\le c\frac{\sqrt{c_{\rm inj}p}}{\kappa}\frac\lambda p\sqrt{\sigma_{\min}}$ for the factored objective

f(X,Y)=\tfrac1{2p}\|\mathcal P_\Omega(XY^\top-M)\|_F^2+\tfrac\lambda{2p}(\|X\|_F^2+\|Y\|_F^2)

satisfies $\|XY^\top-Z_{\rm cvx}\|_F\le2304\,\frac{\kappa}{c_{\rm inj}\sqrt{\sigma_{\min}}}\|\nabla f(X,Y)\|_F$ under Conditions 1–2. 2. Probabilistic layer: Lemma 3 (Condition 1(a)), Lemma 19, Lemmas 7 and 8, and Lemma 4. Lemma 4 gives Conditions 1(b) and 2 uniformly over an $\ell_{2,\infty}$ neighbourhood of the truth. 3. Algorithmic layer: Lemma 5, the error bounds and the small-gradient iterate of gradient descent started at the truth, and (31), its consequence for $X^tY^{t\top}-M^\star$ .

Significance

The bounds of Theorem 2 match the minimax lower bounds up to logarithmic factors when $r$ and $\kappa$ are bounded. This holds in all three norms and for noise of any size below a threshold. The theorem also shows that the convex solution is nearly of rank $r$ . Neither statement requires modifying the estimator, so practitioners running standard solvers get the guarantee as is. The entrywise bound (11b) shows an implicit regularization: the convex program spreads its error over all entries without being told to.

The theorem has a complete published proof. What this mission adds is a machine-checked version, which has value of its own here. The proof chains about twenty lemmas, including a leave-one-out analysis of gradient descent with polynomially many iterations. Its constants are hidden behind " $\lesssim$ " at nearly every step. The formal development fixes the quantifier order of every such constant. It also records the hypotheses the proof uses without stating them, such as the independence of the sampling pattern from the noise. No part of this paper has been formalized before. The deterministic layer (Lemmas 20, 2, Claims 2–3) applies to any Burer–Monteiro factorization of a nuclear-norm problem, not only to this one.

Difficulty

The obvious approach is to analyse the convex program directly through a dual certificate, as in the noiseless theory. With noise there is no exact recovery, and the certificate approach loses a factor polynomial in $n$ . The difficulty is to transfer statistical bounds from a point one can control, the nonconvex iterate, to a point one cannot construct, the convex minimizer. The two are compared through an approximate first-order condition. That comparison is useful only if injectivity and concentration hold uniformly over all factor pairs near the truth, because the iterates depend on $\Omega$ and on the noise. A fixed-tangent-space injectivity bound, the usual tool, does not suffice. The entrywise control of the iterates requires leave-one-out sequences, and those sequences make up most of the appendix.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ and factors Matrix (Fin n) (Fin r) ℝ, using the published matrix_completion_basic, _svd and _tangent definitions (nuclear norm, SVD data, $\mathcal P_\Omega$ , $\mathcal P_T$ , spectral, Frobenius and entrywise norms). $M^\star$ comes with an explicit SVD with $r\ge1$ positive singular values, so its rank is exactly $r$ . Definition 1 is MatrixCompletion.A0. The sub-Gaussian bound is the moment form of [Ver12, Definition 5.7] above, not Mathlib's MGF form. The randomness lives on an arbitrary probability space. The sampling indicators and the noise entries are each mutually independent, and the two families are independent of each other. This last independence is an added hypothesis, which the paper's proofs use. "With probability $1-O(n^{-k})$ " is stated as an outer-measure bound $C_{\rm fail}n^{-k}$ on the failure event. Every unnamed constant (" $\lesssim$ ", "sufficiently large $C$ ", "sufficiently small $c$ ") is an existential placed before $n$ and all data, together with an $n_0$ . Explicit constants of the paper are kept: the exponents $-3$ and $-10$ , $\lambda/8$ , $1/(32\kappa)$ , $72\kappa$ , $8\sqrt\kappa$ , $t_0=n^{18}$ , $n^{-5}$ , the factors $3$ in (31), the $1/n^3$ in (12), and $2304=32\cdot72$ in Lemma 2.

The goal keeps the randomness in the statement. A version with fixed $\Omega$ and $E$ that assumes Conditions 1–2 or the conclusions of Lemma 5 would be Lemma 2 plus (31), not Theorem 2, and is not acceptable as a proof of the goal. The goal quantifies over every minimizer of (3) and every best rank- $r$ approximation. Excluded: Theorem 1 (the $r,\kappa=O(1)$ corollary), the noise condition of Remark 4, approximate minimizers (Remark 6), Lemmas 1 and 6, and the internal lemmas of the leave-one-out analysis (App. D), which solvers may add as supporting theorems. The development needs nuclear-norm subgradients, Weyl's inequality, matrix Bernstein and spectral-norm bounds for sparse random matrices. These are reusable well beyond this mission, and contributions of them are welcome. Theorem and equation numbers are those of the authors' preprint (Sep. 2019, arXiv:1902.07698) and may differ in the SIAM typesetting.

Selected references

Y. Chen, Y. Chi, J. Fan, C. Ma, Y. Yan, Noisy Matrix Completion: Understanding Statistical Guarantees for Convex Relaxation via Nonconvex Optimization, SIAM J. Optim. 30(4), 2020. https://doi.org/10.1137/19M1290000 (preprint: https://arxiv.org/abs/1902.07698)
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, Y. Plan, Matrix Completion With Noise, Proc. IEEE 98(6), 2010. https://doi.org/10.1109/JPROC.2009.2035722
S. Negahban, M. J. Wainwright, Restricted strong convexity and weighted matrix completion: optimal bounds with noise, J. Mach. Learn. Res. 13, 2012. https://jmlr.org/papers/v13/negahban12a.html
V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011. https://doi.org/10.1214/11-AOS894
C. Ma, K. Wang, Y. Chi, Y. Chen, Implicit Regularization in Nonconvex Statistical Estimation, Found. Comput. Math. 20, 2020. https://doi.org/10.1007/s10208-019-09429-9
R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, CUP, 2012. https://arxiv.org/abs/1011.3027

17 thms2 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

Distribution-Free, Risk-Controlling Prediction Sets II: The Waudby-Smith–Ramdas Betting Bound Is a (1 − δ) Upper Confidence Bound for the Mean Loss (Proposition 5)Research Paper

Motivation

A risk-controlling prediction set is a set-valued predictor $\mathcal T$ that, with probability at least $1-\delta$ over a calibration sample, has expected loss at most a target level $\alpha$ . Bates, Angelopoulos, Lei, Malik and Jordan (arXiv:2101.02703, J. ACM 2021) build such sets for any black-box predictor and any bounded loss by a procedure called upper confidence bound (UCB) calibration: for each value of a tuning parameter $\lambda$ , compute from the calibration data an upper confidence bound $\widehat R^+(\lambda)$ for the risk $R(\lambda)$ , and pick the smallest $\lambda$ beyond which all these bounds sit below $\alpha$ . The guarantee of the procedure (their Theorem 1) holds for any choice of the pointwise bound, so the size of the resulting sets is governed by how tight that bound is.

The paper compares several such bounds: Hoeffding, Bentkus, the empirical Bernstein bound of Maurer and Pontil, and a bound adapted from the hedged capital confidence interval of Waudby-Smith and Ramdas (arXiv:2010.09686). The last one, the Waudby-Smith–Ramdas (WSR) bound, adapts to the unknown variance of the loss and is the one the authors recommend for non-binary losses; their experiments use it throughout. Proposition 5 of the paper states that the WSR bound is a valid $(1-\delta)$ upper confidence bound for the mean of a $[0,1]$ -valued loss. This mission formalizes that proposition.

Timeline: Ville (1939) proved the maximal inequality for nonnegative supermartingales that underlies all betting-based confidence bounds. Waudby-Smith and Ramdas (2020) introduced the hedged capital process and its confidence sequences for bounded means. Bates et al. (2021) extracted the one-sided, fixed-sample variant stated as Proposition 5, with the explicit betting fractions $\nu_i$ below.

Setting

Fix the tuning parameter $\lambda$ ; it is dropped from the notation. The calibration losses $L_1, \dots, L_n$ are independent and identically distributed with law $Q$ on $[0,1]$ (the loss is nonnegative and, by the standing assumption of §3.1 of the paper, bounded by one), and their mean is the risk

R = \int x \, dQ(x).

Fix a level $\delta \in (0,1)$ . For $i \ge 0$ define the running mean and variance

\hat\mu_i = \frac{1/2 + \sum_{j=1}^{i} L_j}{1+i}, \qquad \hat\sigma^2_i = \frac{1/4 + \sum_{j=1}^{i} (L_j - \hat\mu_j)^2}{1+i},

so $\hat\sigma^2_0 = 1/4$ , and for $i \ge 1$ the betting fraction

\nu_i = \min\left\{1, \sqrt{\frac{2\log(1/\delta)}{n\,\hat\sigma^2_{i-1}}}\right\},

which depends only on $L_1, \dots, L_{i-1}$ . For a candidate mean $R' \in \mathbb R$ , the capital process is

\mathcal K_i(R') = \prod_{j=1}^{i} \bigl\{1 - \nu_j (L_j - R')\bigr\}, \qquad \mathcal K_0(R') = 1,

the wealth of a gambler who, starting with one unit, bets the fraction $\nu_j$ of their wealth against the hypothesis that the mean is $R'$ . The WSR bound is

\widehat R^+_{\mathrm{WSR}} = \inf\Bigl\{R' \ge 0 : \max_{i=1,\dots,n} \mathcal K_i(R') > \frac1\delta\Bigr\},

the smallest candidate mean the gambler has discredited by multiplying their wealth by more than $1/\delta$ . In Lean these are obs, muHat, sigmaSqHat, nu, K and wsrUCB in the namespace RiskControl.WSR, and $\mathcal F_i = \sigma(L_1,\dots,L_i)$ is filt n.

Formalization targets

Goal: Proposition 5 (p. 7)

For $n \ge 1$ and $\delta \in (0,1)$ ,

\mathbb P\bigl(\widehat R^+_{\mathrm{WSR}} < R\bigr) \le \delta, \qquad\text{that is}\qquad \mathbb P\bigl(R \le \widehat R^+_{\mathrm{WSR}}\bigr) \ge 1-\delta,

the probability being the product law $Q^{\otimes n}$ of the sample.

Milestones (proof of Proposition 5, p. 26)

Nonnegative factors. $\nu_i \in [0,1]$ , and for losses in $[0,1]$ and $R \in [0,1]$ , $1 - \nu_j(L_j - R) \ge 0$ .
Martingale. At the true mean, $i \mapsto \mathcal K_{\min(i,n)}(R)$ is a martingale for $(\mathcal F_i)$ :

\mathbb E\bigl[\mathcal K_i(R) \mid \mathcal F_{i-1}\bigr] = \mathcal K_{i-1}(R).

Ville's inequality (referenced, already proved on the platform): a nonnegative supermartingale started at most $1$ exceeds $1/\delta$ with probability at most $\delta$ .
Monotonicity. For losses in $[0,1]$ , $R' \mapsto \mathcal K_i(R')$ is nondecreasing on $[0,\infty)$ .
Inclusion. For losses in $[0,1]$ and $R \ge 0$ , $\widehat R^+_{\mathrm{WSR}} < R$ implies $\max_{i \le n} \mathcal K_i(R) \ge 1/\delta$ .

Significance

The result is the validity half of the WSR bound: with it, UCB calibration (Theorem 1 of the paper) applied to $\widehat R^+_{\mathrm{WSR}}$ gives the paper's Theorem 4, a risk-controlling prediction set built from the variance-adaptive bound that the experiments of the paper use for classification, segmentation and protein-structure tasks. It is also a self-contained instance of the betting approach to confidence bounds for bounded means, which now underlies a family of nonasymptotic, variance-adaptive procedures in statistics and machine learning.

The proposition is proved in the paper (p. 26), following the proof of Theorem 4 of Waudby-Smith and Ramdas. To our knowledge neither it nor the hedged capital construction has a machine-checked proof. The mission produces one: a Lean statement of the WSR bound with its exact constants, and a proof that reuses the platform's Ville inequality. The capital process and its martingale property are the reusable part; the same construction with other predictable betting fractions gives other confidence bounds.

Difficulty

The bound is not obtained by inverting a tail inequality for the empirical mean, so Hoeffding- or Bernstein-type arguments do not apply. The probabilistic core is the martingale step: one must show that $\nu_i$ is a measurable function of $L_1,\dots,L_{i-1}$ only (it involves $\hat\sigma^2_{i-1}$ , which involves every $\hat\mu_j$ for $j < i$ ), and compute a conditional expectation on the product space $\mathbb R^n$ using independence of the coordinates. Ville's inequality then holds only at the true mean $R$ , a single unknown point, while $\widehat R^+_{\mathrm{WSR}}$ is an infimum over all candidate means; the passage between them needs the monotonicity of $\mathcal K_i$ in its argument, which fails without the bound $L_j \le 1$ (a factor can turn negative). A union bound over candidate means, the first idea, gives nothing here.

Formalization scope

The sample is $\omega : \mathrm{Fin}\,n \to \mathbb R$ under Measure.pi (fun _ => Q), with $L_j = \omega(j-1)$ for $1 \le j \le n$ (1-based indices as on the page). $Q$ is the law of the loss $L(Y, \mathcal T_\lambda(X))$ for the fixed $\lambda$ , assumed concentrated on $[0,1]$ : this is the §3.1 standing assumption together with $L \ge 0$ . The goal adds two hypotheses implicit on the page: $n \ge 1$ and $0 < \delta < 1$ (so that $\log(1/\delta) > 0$ ). The empty sum gives $\hat\sigma^2_0 = 1/4$ ; " $\max_{i=1,\dots,n} \mathcal K_i > 1/\delta$ " is written as an existential over $i \in \{1,\dots,n\}$ ; the infimum is an extended-real infimum, equal to $+\infty$ when no candidate qualifies. The failure probability is bounded through the outer measure of $\{\widehat R^+_{\mathrm{WSR}} < R\}$ , which equals the page's statement for a measurable event. The martingale is extended constantly past time $n$ so that it is indexed by $\mathbb N$ .

Two printed slips are corrected: the proof's "then $P(\max_i \mathcal K_i \ge 1/\delta)$ " (a stray $P$ ) is stated as the event, and "increasing in $R$ " is stated as nondecreasing on $R \ge 0$ .

The infimum must not be a real infimum: a real sInf of an empty set is $0$ , which would make $\widehat R^+_{\mathrm{WSR}} < R$ true for every positive mean and the goal false; with the extended-real infimum the empty case gives $+\infty$ , and the goal is the paper's proposition, not a vacuous one.

Contributions welcome: the measurability of $\nu_i$ with respect to $\mathcal F_{i-1}$ , conditional expectations of products of independent coordinates under Measure.pi, and a finite-horizon form of Ville's inequality (Mathlib's Doob maximal inequality MeasureTheory.maximal_ineq is an alternative route).

Selected references

S. Bates, A. Angelopoulos, L. Lei, J. Malik, M. I. Jordan, Distribution-Free, Risk-Controlling Prediction Sets, J. ACM 68(6), 2021. arXiv:2101.02703v3
I. Waudby-Smith, A. Ramdas, Estimating means of bounded random variables by betting, J. R. Stat. Soc. B, 2024. arXiv:2010.09686
J. Ville, Étude critique de la notion de collectif, Gauthier-Villars, 1939.
A. Maurer, M. Pontil, Empirical Bernstein Bounds and Sample Variance Penalization, COLT 2009. arXiv:0907.3740

7 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

Distribution-Free, Risk-Controlling Prediction Sets I: Upper Confidence Bound Calibration Selects a λ̂ Whose Risk Is at Most α with Probability at Least 1 − δ (Theorem 1)Research Paper

Motivation

A trained classifier or regressor returns a point prediction, but many uses of machine learning need a prediction set: a set of plausible labels together with a guarantee about how often, or how badly, it misses the truth. Medical imaging, protein structure prediction and multi-label classification are examples where a user wants a set whose expected loss is bounded, not just a best guess. Bates, Angelopoulos, Lei, Malik and Jordan (arXiv:2101.02703, J. ACM 68(6), 2021) give a procedure that wraps any black-box predictor and returns sets whose risk is controlled, with no assumption on the data distribution beyond i.i.d. calibration data.

The procedure generalizes split conformal prediction (Vovk, Gammerman and Shafer, 2005) and the tolerance regions of Wilks (1941), which control only the probability of missing the label, to an arbitrary monotone loss on sets (false-negative rate, coverage of a segmentation mask, a hierarchical loss). This mission formalizes its central guarantee, Theorem 1 (p. 5), together with the abstract form Theorem A.1 (p. 26) from which the paper derives it.

Setting

Let $(X, Y)$ be a random pair in $\mathcal X \times \mathcal Y$ with law $P$ , and let $\mathcal Z$ be a set of labels. A set-valued predictor is a map $\mathcal T : \mathcal X \to 2^{\mathcal Z}$ . The paper considers a family $\{\mathcal T_\lambda\}_{\lambda \in \Lambda}$ indexed by a closed set $\Lambda \subseteq \mathbb R \cup \{\pm\infty\}$ that is nested:

\lambda_1 < \lambda_2 \implies \mathcal T_{\lambda_1}(x) \subseteq \mathcal T_{\lambda_2}(x). \tag{1}

A loss on sets $L(y, S) \ge 0$ is required to decrease as the set grows:

S \subseteq S' \implies L(y, S) \ge L(y, S'). \tag{2}

The risk of $\mathcal T_\lambda$ is $R(\lambda) = \mathbb E[L(Y, \mathcal T_\lambda(X))]$ , and the section assumes some $\lambda_{\max} \in \Lambda$ with $R(\lambda_{\max}) = 0$ .

A risk-controlling prediction set at levels $(\alpha, \delta)$ (Definition 1, p. 2) is a data-dependent predictor $\mathcal T$ with $R(\mathcal T) \le \alpha$ with probability at least $1 - \delta$ .

Given an i.i.d. calibration sample $D = ((X_1, Y_1), \dots, (X_n, Y_n))$ , a pointwise upper confidence bound is a function $\widehat R^+(\lambda) = \widehat R^+(D, \lambda)$ with

P\big(R(\lambda) \le \widehat R^+(\lambda)\big) \ge 1 - \delta \quad \text{for each fixed } \lambda. \tag{3}

UCB calibration selects

\hat\lambda = \inf\big\{\lambda \in \Lambda : \widehat R^+(\lambda') < \alpha \ \ \forall \lambda' \in \Lambda,\ \lambda' \ge \lambda\big\}. \tag{4}

In Lean, the risk is RiskControl.UCB.risk P L T lam, the calibration set of (4) for one realization r of $\widehat R^+$ is calSet Λ r α, and $\hat\lambda$ is lambdaHat Λ r α.

Formalization targets

Goal: Theorem 1 (p. 5)

In the setting above, if (3) holds for every $\lambda \in \Lambda$ and $R$ is continuous on $\Lambda$ , then

P^n\big(R(\mathcal T_{\hat\lambda}) \le \alpha\big) \ge 1 - \delta .

Nothing is assumed of $\widehat R^+$ beyond (3); $\alpha$ and $\delta$ are arbitrary reals.

Milestones

Monotone risk (§2.1, pp. 4–5): (1) and (2) make $R$ nonincreasing on $\Lambda$ .
The failure point (proof of Theorem A.1, p. 26, corrected): $\lambda^\dagger = \sup\{\lambda \in \Lambda : R(\lambda) > \alpha\}$ lies in $\Lambda$ and $R(\lambda^\dagger) \ge \alpha$ .
Failure implies a low bound at $\lambda^\dagger$ (p. 26, corrected): deterministically, $R(\hat\lambda) > \alpha$ implies $\widehat R^+(\lambda^\dagger) < \alpha$ .
Theorem A.1 (p. 26): for any continuous nonincreasing $R : \Lambda \to \mathbb R$ and any $\widehat R^+$ satisfying (3) on an abstract probability space, $P(R(\hat\lambda) \le \alpha) \ge 1 - \delta$ .

Significance

Theorem 1 turns a confidence bound for one fixed parameter into a guarantee for a parameter chosen from the data. No uniform convergence over $\Lambda$ is needed, so any concentration inequality for a mean (Hoeffding, Bentkus, the betting bound of Waudby-Smith and Ramdas) yields a calibration procedure immediately; the paper's Theorems 2–5 and 9–10 are of exactly this form, and the later Learn-then-Test and conformal risk control frameworks build on the same template.

The result is proved in the paper; nothing here is open. What the mission adds is a machine-checked version of an argument whose printed form has a gap. The printed proof of Theorem A.1 introduces $\lambda^* = \inf\{\lambda \in \Lambda : R(\lambda) \le \alpha\}$ and asserts $R(\lambda^*) = \alpha$ "by continuity", which is false when $\Lambda$ is not an interval. Finite grids, the usual choice of $\Lambda$ in practice, are not intervals. The theorem remains true, and milestones 2 and 3 state the corrected steps. No formalization of risk-controlling prediction sets or of conformal prediction is known to exist in Lean or on this platform.

Difficulty

The obvious argument applies the confidence bound at $\hat\lambda$ ; that fails because $\hat\lambda$ depends on the data, so (3) says nothing at $\lambda = \hat\lambda$ . The proof must find one deterministic point at which a failure of calibration forces a failure of (3). The paper's choice $\lambda^*$ works only when $R$ attains the value $\alpha$ on $\Lambda$ ; on $\Lambda = \{0, 1\}$ with $R(0) = 1$ , $R(1) = 0$ , $\alpha = 1/2$ and the exact bound $\widehat R^+ = R$ , the event $\{\widehat R^+(\lambda^*) < \alpha\}$ has probability one, so the printed last step does not bound anything. The second difficulty is boundary behaviour: $\Lambda$ may contain $\pm\infty$ , the infimum in (4) may be over an empty set, and the calibration set need not contain its own infimum.

Formalization scope

$\Lambda$ is a closed subset of EReal (the extended reals with the order topology); $\lambda$ is only compared, never added. Continuity of $R$ is in the subspace topology of $\Lambda$ .
Set-valued predictions are Set 𝒵, i.e. $\mathcal Y' = 2^{\mathcal Z}$ (the paper uses $2^{\mathcal Y}$ for most of its examples).
The risk is the published definition WassersteinDRO.Duality.nominalRisk, a Bochner integral. Because a non-integrable integrand integrates to $0$ in Lean, Theorem 1 assumes $(x, y) \mapsto L(y, \mathcal T_\lambda(x))$ is $P$ -integrable for every $\lambda \in \Lambda$ .
The standing assumptions of §2.1 are hypotheses of Theorem 1: $\Lambda$ closed, (1) on $\Lambda$ , (2), $L \ge 0$ , and $R(\lambda_{\max}) = 0$ for some $\lambda_{\max} \in \Lambda$ . The monotonicity of $R$ is not assumed in Theorem 1; it is milestone 1. Theorem A.1 assumes it, as printed.
The i.i.d. sample is Fin n → 𝒳 × 𝒴 under the product measure $P^n$ . $\widehat R^+$ is an arbitrary real function of the sample and of $\lambda$ ; an infinite bound is represented by any value $\ge \alpha$ .
"With probability at least $1 - \delta$ " is written as a failure probability at most $\delta$ , measured as an outer measure; no measurability of $\widehat R^+$ or $\hat\lambda$ is assumed. For a measurable event this is the page's statement.
$\hat\lambda$ is an infimum in EReal, so $\inf \emptyset = +\infty$ as on the page. Since $+\infty$ need not belong to $\Lambda$ , the failure event is "the set in (4) is nonempty and $R(\hat\lambda) > \alpha$ "; when the set is nonempty, $\hat\lambda \in \Lambda$ . When it is empty the procedure certifies nothing, and the natural output is $\mathcal T_{\lambda_{\max}}$ , of risk $0$ .
Corrections of the print: Theorem A.1's conclusion reads $P(R(\lambda) \le \alpha)$ , stated here with $\hat\lambda$ ; the proof's point $\lambda^*$ and the claim $R(\lambda^*) = \alpha$ are replaced by $\lambda^\dagger = \sup\{\lambda \in \Lambda : R(\lambda) > \alpha\}$ and $R(\lambda^\dagger) \ge \alpha$ , which coincide with the page for an interval $\Lambda$ .
A formalization that assumes $R$ monotone in Theorem 1, quantifies over $\widehat R^+$ inside the event, takes a real-valued infimum (which is $0$ on unbounded sets) or drops the integrability guard would state a different theorem; the statement here does none of these.

Needed infrastructure is small: closed subsets of EReal and their infima and suprema (IsClosed.sInf_mem, IsClosed.sSup_mem), continuity within a set, monotonicity of the Bochner integral, and monotonicity of outer measure. Proofs of the milestones are welcome individually; the deterministic milestones 2 and 3 are reusable for every UCB-calibration theorem of the paper.

Selected references

S. Bates, A. Angelopoulos, L. Lei, J. Malik, M. I. Jordan, Distribution-Free, Risk-Controlling Prediction Sets, J. ACM 68(6), 2021; arXiv:2101.02703v3. https://arxiv.org/abs/2101.02703
V. Vovk, A. Gammerman, G. Shafer, Algorithmic Learning in a Random World, Springer, 2005. https://doi.org/10.1007/b106715
S. S. Wilks, Determination of sample sizes for setting tolerance limits, Ann. Math. Statist. 12(1), 1941. https://doi.org/10.1214/aoms/1177731788
I. Waudby-Smith, A. Ramdas, Estimating means of bounded random variables by betting, arXiv:2010.09686, 2020. https://arxiv.org/abs/2010.09686

7 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Methanol Limit on a Drifting Proton-to-Electron Mass Ratio (Bagdonaite et al. 2013)Research Paper

Motivation

The Standard Model of particle physics does not explain the values of its dimensionless constants, nor does it require them to be constant in time. The proton-to-electron mass ratio $\mu = m_p/m_e \approx 1836$ is one such constant: it compares the scale of the strong interaction (which sets most of the proton mass) with the electroweak scale (which sets the electron mass). A measured change of $\mu$ over cosmic time would signal physics beyond the Standard Model, while a tight null result constrains models with additional scalar fields.

The standard test compares the frequencies of molecular transitions observed in distant galaxies with laboratory values. Different transitions respond differently to a change of $\mu$ , so a relative shift between them cannot be confused with the overall cosmological redshift.

Timeline. Optical studies of molecular hydrogen at redshifts $z>2$ reached $|\Delta\mu/\mu| < 10^{-5}$ (Malec et al. 2010; van Weerdenburg et al. 2011). Ammonia inversion lines, about 100 times more sensitive, moved the field to radio astronomy and gave constraints at the $10^{-7}$ level toward the lensing galaxy of PKS 1830−211 at $z=0.89$ (Henkel et al. 2009; Kanekar 2011). Jansen et al. (2011) and Levshakov, Kozlov & Reimers (2011) pointed out that methanol transitions have sensitivity coefficients ranging from about $-42$ to $+53$ . Ellingsen et al. (2012) gave a first methanol limit from two lines. Bagdonaite et al. (Science, 2013) observed four methanol lines in PKS 1830−211 with the Effelsberg 100-m telescope and derived the limit $\Delta\mu/\mu = (0.0\pm1.0)\times10^{-7}$ at a look-back time of about 7 billion years.

Setting

A transition with frequency $\nu$ has sensitivity coefficient $K_\mu$ defined by

\frac{\Delta\nu}{\nu} = K_\mu\,\frac{\Delta\mu}{\mu},

or, in infinitesimal form, $K_\mu = \frac{\mu}{\nu}\frac{d\nu}{d\mu}$ . Pure rotational transitions have frequency inversely proportional to the reduced mass, hence to $\mu$ , so $K_\mu=-1$ . Mixed torsion–rotation transitions of methanol have strongly enhanced coefficients (Table 1 of the paper: $-32.8$ and $-7.4$ ).

Each observed line is assigned a position $V$ , a velocity (km/s) on a common scale centred on redshift $z=0.88582$ . If $\mu$ in the absorbing galaxy differs from the laboratory value by $\Delta\mu = \mu_z-\mu_{\mathrm{lab}}$ , the positions satisfy

\frac{V}{c} = -K_\mu\,\frac{\Delta\mu}{\mu}

up to a velocity offset common to all lines, where $c$ is the speed of light. Plotting $V$ against $K_\mu$ and fitting a straight line $V = a + bK_\mu$ therefore gives $\Delta\mu/\mu = -b/c$ .

The fit is a weighted least-squares fit with weights $1/\sigma_i^2$ , where $\sigma_i$ is the 1σ uncertainty of the $i$ -th position. With $S=\sum 1/\sigma_i^2$ , $S_K=\sum K_i/\sigma_i^2$ , $S_V=\sum V_i/\sigma_i^2$ , $S_{KK}=\sum K_i^2/\sigma_i^2$ , $S_{KV}=\sum K_iV_i/\sigma_i^2$ and $\Delta=SS_{KK}-S_K^2$ , the slope, intercept and slope standard error are $b=(SS_{KV}-S_KS_V)/\Delta$ , $a=(S_{KK}S_V-S_KS_{KV})/\Delta$ and $\sigma_b=\sqrt{S/\Delta}$ . The reduced chi-squared is $\chi^2_\nu=\frac{1}{n-2}\sum_i\big((V_i-a-bK_i)/\sigma_i\big)^2$ .

The data (Table 1) are four lines: $3_{-1}$ – $2_0\,E$ ( $K_\mu=-32.8$ , $V=9.06\pm0.67$ ), $0_0$ – $1_0\,A^+$ ( $-1$ , $8.40\pm0.10$ ), $0_0$ – $1_0\,E$ ( $-1$ , $9.12\pm0.30$ ) and $2_{-1}$ – $1_0\,E$ ( $-7.4$ , $9.83\pm0.43$ ). Because A- and E-symmetry methanol behave as separate species that may be spatially segregated, the fiducial fit uses only the three E lines.

Formalization targets

Goal: the headline limit

With the E-line estimate $\widehat{\Delta\mu/\mu}=-b/c$ , its statistical error $\sigma_{\mathrm{stat}}=\sigma_b/c$ and the adopted systematic error $\sigma_{\mathrm{sys}}=7.0\times10^{-8}$ ,

\big|\widehat{\Delta\mu/\mu}\big| < 0.05\times10^{-7},\qquad \Big|\sqrt{\sigma_{\mathrm{stat}}^2+\sigma_{\mathrm{sys}}^2}-1.0\times10^{-7}\Big| < 0.05\times10^{-7},

i.e. $\Delta\mu/\mu=(0.0\pm1.0)\times10^{-7}$ to the printed precision.

Milestones

Pure rotational transitions ( $\nu\propto1/\mu$ ) have $K_\mu=-1$ .
Under the exact relation $V_i=a-c\,\delta\,K_i$ , the weighted fit returns $-b/c=\delta$ and intercept $a$ .
E-line fit: $\Delta\mu/\mu=(-0.1\pm7.6)\times10^{-8}$ , $\chi^2_\nu\approx2.0$ .
The E-line result is consistent with $\Delta\mu=0$ at the $1.5\times10^{-7}$ (two-standard-error) level.
Four-line fit: $\Delta\mu/\mu=(11.0\pm6.8)\times10^{-8}$ , $\chi^2_\nu\approx6.4$ .
The $0_0$ – $1_0$ $A^+$ and $E$ lines are separated by $0.72\pm0.32$ km/s.
The $A^+$ anchor line shifted by $0.48\pm0.26$ km/s between December 2011 and April 2012.

Significance

The result. The authors report the limit as statistically more constraining than previous radio-domain tests of a drifting $\mu$ . Because it uses a single molecular species, it is much less exposed to the main systematic of multi-species comparisons, namely that different molecules sit in different gas at slightly different velocities. The milestones record the internal evidence behind the choice of the fiducial fit: the poor four-line $\chi^2_\nu$ and the A–E velocity separation.

Formalizing it. The physical inputs (sensitivity coefficients, measured positions, the systematic budget) are taken as data. What the mission checks by machine is the chain from those data to the printed numbers: the definition of the sensitivity coefficient and its value for rotational lines, the correctness of the line-fit estimator, and the arithmetic of every reported fit, separation and error combination.

Difficulty

The numerical milestones are exact statements about explicit rational data, but they involve nested sums, quotients and square roots, so a certified proof requires careful interval bounds rather than floating-point evaluation. The paper's numbers are rounded from unrounded measurements: recomputing from the rounded Table 1 entries gives, for example, $\sigma_b/c\approx7.69\times10^{-8}$ instead of $7.6\times10^{-8}$ , and $\chi^2_\nu\approx6.27$ instead of $6.4$ for the four-line fit. Tolerances therefore had to be chosen so that every statement is both faithful to the printed value and true for the tabulated data. The general recovery milestone requires showing that the normal equations are nondegenerate whenever the $K_i$ are not all equal.

Formalization scope

All quantities are real numbers in Lean; data are finite families indexed by Fin n. Velocities are in km/s and $c=299792.458$ km/s.
The sensitivity coefficient is the logarithmic derivative $(\mu/\nu(\mu))\,\nu'(\mu)$ using Mathlib's deriv.
The fit uses the closed-form weighted least-squares formulas above; the reduced chi-squared divides by $n-2$ .
The systematic uncertainty $7.0\times10^{-8}$ is an input; the variability model behind it is out of scope, as are the radiative-transfer column densities and the spectroscopic computation of $K_\mu$ for mixed transitions.
"95% confidence level" is formalized as the two-standard-error interval.
Trivializing readings are excluded: every numerical statement is a closed statement about the tabulated data, with no free hypotheses, and the general recovery statement requires non-constant $K$ and nonzero uncertainties.

Reusable pieces: the weighted least-squares definitions and the exact-recovery lemma apply to any straight-line fit with known uncertainties.

Selected references

J. Bagdonaite, P. Jansen, C. Henkel, H. L. Bethlem, K. M. Menten, W. Ubachs, A Stringent Limit on a Drifting Proton-to-Electron Mass Ratio from Alcohol in the Early Universe, Science, 2013. https://doi.org/10.1126/science.1224898
P. Jansen, L.-H. Xu, I. Kleiner, W. Ubachs, H. L. Bethlem, Methanol as a sensitive probe for spatial and temporal variations of the proton-to-electron mass ratio, Phys. Rev. Lett. 106, 100801, 2011. https://doi.org/10.1103/PhysRevLett.106.100801
S. P. Ellingsen, M. A. Voronkov, S. L. Breen, J. E. J. Lovell, First cosmological constraints on the proton-to-electron mass ratio from observations of rotational transitions of methanol, Astrophys. J. Lett. 747, L7, 2012. https://doi.org/10.1088/2041-8205/747/1/L7
Ph. R. Bevington, D. K. Robinson, Data Reduction and Error Analysis for the Physical Sciences, 3rd ed., McGraw-Hill, 2003.

9 thms2 active usersReviewed

Missions

Freedman–Madore 2023: Quantifying the Hubble TensionResearch Paper

Motivation

Setting

Formalization targets

Goal (§10, p. 25)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Zipf's Law: the Zipf Distribution, its Infinite Extension and Related LawsTextbook

Motivation

Setting

Formalization targets

Goal — the infinite-item extension

Milestones

Significance

Difficulty

Formalization scope

Selected references

Distribution-Free Contextual Dynamic Pricing 2: Every Algorithm Has Expected Regret at Least C₀ C_p T₀ on Some Perturbed Linear Bandit with Perturbation C_pResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (p. 22)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Solving Chance-Constrained Problems via a Smooth Sample-Based Nonlinear Approximation 1: Smoothed Sample Feasible Sets Lie in the True Feasible Set with Probability ≥ 1 − ⌈1/β⌉⌈2LD/t⌉ⁿ exp(−2NM²)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.13

Milestones

Significance

Difficulty

Formalization scope

Selected references

Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality 3: Under T₂(τ), W₂-Robust Loss at Radius ρ̃ₙ Bounds True Loss up to 4r⋆+2εₙ+ħρ̃ₙ²Research Paper

Motivation

Setting

Formalization targets

Goal: Corollary 6 (2-Wasserstein DRO), pp. 11–12

Milestones, in proof order

Significance

Difficulty

Formalization scope

Selected references

Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality 2: Under T₁(τ), W₁-Robust Loss at Radius 2√(τt/n)+√(4r⋆+2/n) Bounds the True LossResearch Paper

Why the radius of a Wasserstein ball matters

Setting

Formalization targets

Goal: Corollary 4 (1-Wasserstein DRO)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality 1: Under T_p(τ), True Loss ≤ Empirical Loss + R(√(τt/n); −f) w.p. ≥ 1 − e^(−t)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (variation-based concentration, p. 7)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Distance Covariance in Metric Spaces 2: Without Negative Type Some Law Has Negative Distance Covariance, and Without Strong Negative Type Some Non-Product Law Has ZeroResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.15

Milestones (all from the proof on p. 17)

Significance

Difficulty