Probability

Completed

Operations Research Optimization Statistics·Captain: mikedeng1

Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization 1: Empirical Burg-Ball DRO Bounds Cover E[h(x;ξ)] with Probability Tending to 1 − αResearch Paper

Motivation

Stochastic programs and chance-constrained models in operations research contain expectations of the form

Z_0(x)=\mathbb E_0[h(x;\xi)],

where $\xi$ is a random input under an unknown distribution $P_0$ , $x$ is a decision and $h$ is a known loss. In practice $P_0$ is seen only through i.i.d. data $\xi_1,\dots,\xi_n$ . Distributionally robust optimization (DRO) replaces the unknown expectation by the worst case over a set of plausible distributions, and a recurring question is how large that set should be so that the robust value is a statistically valid bound, without being needlessly conservative.

The usual answer, for divergence-based sets on a finite support of size $k$ , sets the radius from a $\chi^2_{k-1}$ quantile (Ben-Tal et al. 2013). This guarantee holds simultaneously for every function of the distribution, and so it is loose for a single expectation, and it degrades as $k$ grows. H. Lam (arXiv:1605.09349, Operations Research 2019) observed that if the ball is placed around the empirical distribution and measured with the Burg entropy, the right radius uses one degree of freedom, whatever the support. The DRO bounds then form an asymptotically exact confidence interval for $Z_0(x)$ . The mechanism is the empirical likelihood method of Owen (Owen 1988; Owen 2001).

Timeline:

1988: Owen proves the empirical likelihood theorem for a mean (−2 log of the profile likelihood ratio tends to $\chi^2_1$ ), the nonparametric analogue of Wilks' theorem.
2013: Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen calibrate $\varphi$ -divergence balls on a finite support with $\chi^2_{k-1}$ quantiles.
2016: Lam (this paper) connects the empirical Burg-ball DRO to empirical likelihood, with pointwise (Theorem 2) and uniform (Theorem 4) coverage.
2016–2021: Duchi, Glynn and Namkoong (arXiv:1610.03425) develop the general $f$ -divergence version and exact coverage of optimal values.

Setting

Data: $\xi_1,\xi_2,\dots$ are i.i.d. random elements of a measurable space $\Xi$ under $P_0$ . A decision $x\in\mathbb R^m$ is fixed, and $h(x;\cdot):\Xi\to\mathbb R$ is measurable with $0<\operatorname{Var}_0 h(x;\xi)<\infty$ .

The empirical Burg-entropy divergence ball of radius $\eta$ is the set of weight vectors on the $n$ data points

\mathcal U_n(\eta)=\Big\{w\in\mathbb R^n:\ -\frac1n\sum_{i=1}^n\log(nw_i)\le\eta,\ \sum_{i=1}^n w_i=1,\ w_i\ge0\Big\},

with $\log 0=-\infty$ . It is the $\varphi$ -divergence ball around the uniform weights $1/n$ for the Burg generator $\varphi(t)=-\log t+t-1$ . Let $\chi^2_{1,1-\alpha}$ be the $(1-\alpha)$ -quantile of the $\chi^2_1$ law, i.e. $P(Y^2\le\chi^2_{1,1-\alpha})=1-\alpha$ for $Y\sim N(0,1)$ . The empirical DRO bounds are

\underline Z_n(x)=\min_{w\in\mathcal U_n(\chi^2_{1,1-\alpha}/(2n))}\sum_{i=1}^n h(x;\xi_i)w_i,\qquad \overline Z_n(x)=\max_{w\in\mathcal U_n(\chi^2_{1,1-\alpha}/(2n))}\sum_{i=1}^n h(x;\xi_i)w_i .

For a sample $z\in\mathbb R^n$ and a value $\mu$ , the profile empirical likelihood statistic is

-2\log R(\mu)=\min\Big\{-2\sum_{i=1}^n\log(nw_i):\ \sum_i w_iz_i=\mu,\ \sum_i w_i=1,\ w_i\ge0\Big\},

equal to $+\infty$ when no weight vector is feasible.

Formalization targets

Goal: Theorem 2 (p. 11)

\lim_{n\to\infty}P\big(\underline Z_n(x)\le Z_0(x)\le\overline Z_n(x)\big)=1-\alpha .

The event is two-sided and joint. No rate is claimed.

Milestones

Proposition 2 (p. 23). For every data vector and $\kappa\ge0$ ,

\min_{\mathcal U_n(\kappa/(2n))}\textstyle\sum_i w_iz_i\le\mu\le\max_{\mathcal U_n(\kappa/(2n))}\sum_i w_iz_i\iff -2\log R(\mu)\le\kappa .

Theorem 1, the empirical likelihood theorem (p. 10). $-2\log R(Z_0(x))\Rightarrow\chi^2_1$ .
The pointwise steps of the paper's proof of Theorem 1 (the proof of Theorem 5 with a one-point index set): Lemma 3 (p. 38), $\max_{i\le n}|Y_i|=o(n^{1/2})$ a.s. for square-integrable i.i.d. $Y_i$ ; the closed form (49)–(50) (pp. 25–26) of the optimal weights; the multiplier bound (52) (p. 27); the expansion (68) (p. 30), $-2\log R=n s^{-1}\bar h^2+o_p(1)$ .

Significance

Theorem 2 says that a robust optimization formulation with a data-driven Burg ball of radius $\chi^2_{1,1-\alpha}/(2n)$ yields an asymptotically exact $(1-\alpha)$ confidence interval for an expected loss, independently of the support size of $\xi$ . Proposition 2 is the bridge: it identifies the DRO interval with the empirical likelihood confidence region, so any distributional result on $-2\log R$ transfers to the DRO bounds. This is the pointwise basis of the paper's later results on feasibility of chance and expectation constraints.

The result is proved in the paper, and Theorem 1 is classical. To our knowledge none of these statements has a machine-checked proof. Formalizing them requires the empirical likelihood theorem in Lean, which is reusable well beyond DRO (empirical likelihood tests and intervals for means). The Open platform theorem GenEmpLik.Coverage.theorem_3 (Duchi, Glynn and Namkoong) implies the goal when its decision set is the single point $\{x\}$ and its generator is $2\varphi$ with radius $\chi^2_{1,1-\alpha}$ ; it is a different, more general statement and is not proved. Likewise the Open GenEmpLik.Expansion.lemma_7 implies Lemma 3, and the Proved NumStochOpt.ListScheduling.lemma_8_1_i_max_over_sqrt_ae gives Lemma 3 after passing to $|Y_i|$ .

Difficulty

Proposition 2 is a finite-dimensional convexity statement, but it needs attainment of the minimum defining $-2\log R$ , which holds only because the objective blows up at the boundary of the simplex. The central difficulty is Theorem 1. The optimal weights are explicit only through a Lagrange multiplier $\lambda$ that solves a nonlinear equation; to expand $-2\log R$ one must first show $\lambda=O_p(n^{-1/2})$ , which requires controlling the largest observation by Lemma 3 together with the law of large numbers for $s$ , and then bound the cubic Taylor remainder of $\log(1+\lambda\tilde h_i)$ uniformly in $i$ . A direct appeal to the central limit theorem for the sample mean does not suffice, since $-2\log R$ is an implicitly defined optimal value, not a smooth function of the mean.

Formalization scope

The sample is a sequence ξ : ℕ → Ω → Ξ, measurable, mutually independent and identically distributed, indexed from $0$ ; the size- $n$ sample is fun i : Fin n => h x (ξ i ω).
The moment assumption is MemLp (h x ∘ ξ 0) 2 together with 0 < variance. Positive variance cannot be dropped: for a constant loss the coverage is $1$ .
The quantile is pinned by gaussianReal 0 1 {y | y^2 ≤ q} = ofReal (1 - α) with $0<\alpha<1$ ; it is not a free parameter, and it is not the normal quantile.
The upper bound is the published GenEmpLik.Expansion.robustMean burg (q/2) (its ball has radius $\rho/n$ , so $\rho=q/2$ ); the lower bound is its infimum twin robustLower. The ball uses the published probUncertaintySet and phiDiv.
The Burg generator is $+\infty$ at $t\le0$ , and the statistic elStat minimizes over strictly positive weights with the empty infimum equal to $+\infty$ . Lean's junk value $\log 0=0$ therefore never enters: a formalization with $w_i\ge0$ and real logarithms would admit boundary weights with spurious finite divergence and is ruled out. For $n\ge1$ the value sets of the DRO bounds are nonempty and bounded, so the real infimum and supremum are not junk values.
The decision set $\Theta$ is dropped (the statements are pointwise in $x$ ). Theorem 1 is stated as convergence of distribution functions at every $t$ , which is equivalent to $\Rightarrow\chi^2_1$ since the limit is continuous. Proposition 2 is stated for general $\kappa\ge0$ and every data vector, as displayed on p. 11. Milestones (49)–(50), (52), (68) are the one-point ( $\Theta=\{x\}$ ) specialisations of the proof of Theorem 5.
Probabilities of events are outer probabilities; no measurability of events is assumed, as the paper ignores these issues (p. 14).
Not posed: the headline Theorem 4 (uniform calibration over $\Theta$ by the quantile of a $\chi^2$ -process supremum), Theorem 5 and Lemma 2, which need Donsker classes and weak convergence in $\ell^\infty(\Theta)$ , for which Mathlib has no substrate.

Contributions welcome: proofs of Proposition 2 and Lemma 3 (from the Proved reference), the KKT analysis (49)–(52), and a Lean empirical likelihood theorem.

Selected references

H. Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization, arXiv:1605.09349v1, 2016; Operations Research 67(4), 2019. https://arxiv.org/abs/1605.09349v1
A. B. Owen, Empirical likelihood ratio confidence intervals for a single functional, Biometrika 75(2), 1988. https://doi.org/10.1093/biomet/75.2.237
A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
J. C. Duchi, P. W. Glynn, H. Namkoong, Statistics of robust optimization: a generalized empirical likelihood approach, Mathematics of Operations Research 46(3), 2021. https://arxiv.org/abs/1610.03425

13 thms2 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Posted Price Mechanisms and Optimal Threshold Strategies for Random Arrivals I: Under Random Arrival Order, Nonadaptive Thresholds Earn a 1 − 1/e Fraction of E[max Xᵢ]Research Paper

Motivation

In a prophet inequality, a gambler sees prizes one at a time and must decide when to stop, while a prophet knows every realization and takes the largest. A stopping guarantee compares the gambler’s expected prize with the prophet’s. The order of arrival changes the problem: here the prizes are independent but can have different distributions, and every permutation of their arrival is equally likely. Before seeing any prize, the gambler chooses a threshold for each distribution and accepts the first prize above its threshold. Such a rule has no need to update thresholds after observing rejections. Correa, Foncea, Hoeksma, Oosterwijk, and Vredeveld prove that this restricted rule still earns at least a $1-1/e$ fraction of the prophet’s expected maximum (Theorem 1, pp. 1455, 1459).

The random-arrival stopping model also supplies guarantees for posted-price mechanisms. A posted price gives a buyer a take-it-or-leave-it offer; the first buyer who accepts ends the sale. The paper explains the connection between its stopping rules and expected revenue under random buyer arrival (§1.1 and §5). This mission formalizes the stopping theorem itself, which is the mathematical guarantee used before that economic translation.

Setting

Let $n\ge1$ , and let $X_1,\ldots,X_n$ be independent, nonnegative real random variables with known, possibly different distributions. Their realizations arrive in a uniformly random order. A nonadaptive threshold rule chooses constants $\tau_i\in[0,\infty]$ before any realization is observed. It accepts the first arriving index $i$ with $X_i>\tau_i$ and receives $X_i$ . If no prize crosses its threshold, its reward is zero. An infinite threshold deliberately excludes an index. The strict comparison matches Theorem 1, even though an earlier description in §1.2 uses a weak comparison (pp. 1454–1455).

For fixed realized prizes, write $Y_i=\mathbf1_{\{X_i>\tau_i\}}$ . Conditional on the set of indices with $Y_i=1$ , each accepted index is equally likely to arrive first. The conditional expected reward is therefore

R_\tau(X)=\frac{\sum_{i=1}^{n}X_iY_i}{\sum_{i=1}^{n}Y_i},\qquad 0/0:=0.

The prophet benchmark is $X^*=\max_i X_i$ . The theorem compares $\mathbb E R_\tau(X)$ with $\mathbb E X^*$ , including distributions for which either expectation may be infinite. The variables need no common distribution and no atomlessness assumption.

The paper’s main supporting result is the Bernoulli Selection Lemma. It starts with independent Bernoulli indicators $Y_i$ of success probabilities $q_i$ , fixed real prizes $b_i$ , and a chosen subset $S$ . Its payoff is the average $\sum_{i\in S}b_iY_i/\sum_{i\in S}Y_i$ , again zero when the denominator vanishes. The lemma compares the best subset with a finite linear optimization problem over $0\le z_i\le q_i$ and $\sum_i z_i\le1$ (Lemma 1, p. 1455).

Formalization targets

Nonadaptive threshold guarantee

The goal is the exact constant of Theorem 1:

\exists\tau\in[0,\infty]^n:\quad \mathbb E R_\tau(X)\ \ge\ (1-e^{-1})\,\mathbb E X^*.

The quantifiers range over every finite nonempty family of independent nonnegative variables. The thresholds are deterministic and indexed by the distributions, and the assertion covers atoms as well as continuous laws. This is the paper’s headline nonadaptive result (Theorem 1, p. 1459).

Bernoulli selection and comparison steps

The milestone list includes the paper’s multilinear formulation (4), its substitution (5), Proposition A.1, Lemmas 2 and 3, and the Bernoulli Selection Lemma. The latter states, in particular, that the maximum expected selected average dominates $(1-e^{-1})$ times the optimum over feasible $z$ . Two further milestones express the decomposition of the expected maximum and the upper-tail comparison used for continuous distributions (§2–3 and Appendix A). These targets fix the finite selection problem and the probabilistic quantities that the goal must connect.

Significance

The guarantee identifies what fixed, distribution-specific thresholds can achieve under random arrival: the expected accepted prize reaches a constant fraction of the prophet’s benchmark for every collection of independent nonnegative distributions. The paper also gives examples showing why a rule that keeps every positive prize is inadequate and studies where the $1-e^{-1}$ factor is tight (§2.1 and §3.1). These are claims about the performance of a restricted class of stopping rules, not about an optimal adaptive strategy.

The paper proves Theorem 1; a machine-checked proof of this mission’s goal remains to be supplied. The finite Bernoulli model, its subset optimum, and the nonnegative expectation conventions would be reusable for other random-order stopping and allocation results. This mission makes the paper’s claimed constants, event comparisons, and boundary cases explicit in the theorem statements so a later proof has a fixed target.

Difficulty

Taking the first value above a single low threshold can accept a modest prize before a rare large one arrives. Raising every threshold can instead reject too many prizes. The paper’s example with a constant prize and a rare large prize shows that accepting all available values does not meet the claimed factor (p. 1460). The difficulty is obtaining one set of fixed thresholds that balances those risks across different distributions, while the benchmark selects the largest realization after seeing them all. The Bernoulli selection inequality carries the sharp constant; connecting it to general distributions must also account for ties and atoms.

Formalization scope

Lean represents the index set by Fin n with $n\ge1$ , so its index zero is the paper’s index one. The existing published definition SamuelCahnProphet.Median.Setting.maxX supplies the sample maximum; this mission defines the strict accepted set and its real-valued reward ratio. Thresholds live in $[0,\infty]$ because the paper explicitly uses $\infty$ to exclude a variable. Expectations are nonnegative extended integrals of ENNReal.ofReal, preserving infinite values and avoiding a default zero for nonintegrable real integrals. The source’s nonnegativity assumption is represented almost surely, which is enough for these expectations and does not restrict the distributions further.

The Bernoulli law is a finite product formula. Its probabilities lie in $[0,1]$ , while prizes are arbitrary real numbers as in the printed lemma. The feasibility condition includes $z_i\ge0$ : these variables are probabilities, and allowing negative values would change the optimization problem. The finite subset optimum is an attained maximum. Proposition A.1 is stated for $M\ne\varnothing$ ; an empty $M$ contradicts the budget conclusion for $a>0$ . It also includes the printed $a=0$ case. Lemma 2 includes $y=1$ as printed: the removable division by zero in (6) is assigned its continuous value $2/e$ . The comparison milestones for continuous distributions assume atomlessness explicitly; the goal does not.

The accepted set depends only on fixed thresholds and the realized values. It cannot depend on the sampled arrival order or on prior observations. A constant choice such as accepting every positive prize does not prove the target guarantee. Contributions that establish the finite Bernoulli selection result, its analytic bounds, the random-order reward identity, or the passage from continuous to arbitrary distributions all serve the stated goal. The random-order identity and the discontinuous case are further work beyond the current milestone list.

Selected references

José Correa, Patricio Foncea, Ruben Hoeksma, Tim Oosterwijk, and Tjark Vredeveld, Posted Price Mechanisms and Optimal Threshold Strategies for Random Arrivals, Mathematics of Operations Research 46(4), 1452–1478, 2021. DOI: 10.1287/moor.2020.1105.

12 thms2 active usersReviewed

Completed

Mechanism Design Operations Research Stochastic Systems·Captain: mikedeng1

Pricing and Matching with Forward-Looking Buyers and Sellers 1: Waiting-Adjusted Fixed Prices with Greedy Matching Earn at Least 1 − (1 + 2(b+h)T/(3(p−w)))/√µ* of the Fluid Profit BoundResearch Paper

Why this market matters

An intermediary such as a ride platform must attract buyers and sellers who arrive at different times. A buyer may wait for a seller; a seller may wait for a buyer. Both sides can choose when to request a match, so an ask price and a bid price affect participation as well as the intermediary's margin. Chen and Hu study whether a simple posted-price policy remains profitable despite this waiting and the uncertainty of arrivals. Their submitted manuscript proves a finite-market guarantee and an asymptotic rate for the policy used here. The proof appears in its Supplemental Note, while the model and theorem are in the main text.

Market and benchmarks

Buyers arrive during a horizon $[0,T]$ as a Poisson process of rate $\lambda^d>0$ , and sellers arrive independently at rate $\lambda^s>0$ . A buyer's valuation $v$ has density $f^d$ on $[\underline v,\overline v]$ and a seller's cost $c$ has density $f^s$ on $[\underline c,\overline c]$ . Marks are independent of arrival times. A buyer and a seller each trade at most one unit. If they wait after arrival, they incur costs $b$ and $h$ per unit time, respectively. The paper assumes regularity: the buyer's virtual value $V^d(v)=v-\bar F^d(v)/f^d(v)$ and the seller's virtual cost $V^s(c)=c+F^s(c)/f^s(c)$ are weakly increasing on their supports. Here $\bar F^d=1-F^d$ .

A clairvoyant assignment knows all arrivals through $T$ . For each possible buyer–seller pair it assigns virtual surplus $V^d(v)-V^s(c)$ less the waiting cost determined by their arrival order. It chooses a partial matching with greatest total value, denoted $\bar J(H^T)$ . A separate fluid program chooses a measurable, nonnegative pair of price trajectories that clears demand and supply at every time. Its optimal value is $\bar J^*$ . These are different objects: $\bar J(H^T)$ is random and uses indivisible agents, whereas $\bar J^*$ is a deterministic continuous-flow optimum. Lemma 2 of the manuscript compares their values in expectation.

Let $\mu^*$ be the greatest volume in $[0,\min\{\lambda^dT,\lambda^sT\}]$ with nonnegative marginal virtual surplus. The buyer and seller prices $p^*,w^*$ are inverse-distribution prices at that volume. Proposition 1 states that these constant prices attain the fluid optimum and $\bar J^*=(p^*-w^*)\mu^*$ .

Formalization targets

The greedy matching policy pairs requests first come, first served. Under the waiting-adjusted fixed-price policy, a buyer's posted ask is $p^*$ minus $b$ times a conditional expected wait per match probability; the seller's posted bid is $w^*$ plus the corresponding $h$ term. The buyer adjustment is conditioned on the observed pre-arrival inventory signal. Agents request immediately exactly when their valuation or cost crosses the base-price threshold. The policy's expected profit $J$ is computed from posted prices paid by successfully matched agents.

The first target is the paper's finite-market bound:

\frac{J}{\bar J^*}\ge 1-\left(1+\frac{2(b+h)T}{3(p^*-w^*)}\right)\frac{1}{\sqrt{\mu^*}}.

When $J\ge0$ , the benchmark comparison also gives $J/\mathbb E[\bar J(H^T)]\ge J/\bar J^*$ . For scaled systems with arrival rates $n^{\alpha_d}\lambda^d$ and $n^{\alpha_s}\lambda^s$ , where both exponents are positive, the second target is a constant $C$ independent of $n$ such that

\frac{J^{(n)}}{\bar J^{*,(n)}}\ge 1-\frac{C}{\sqrt{n^{\min\{\alpha_d,\alpha_s\}}}}\qquad(n\ge1).

The milestone list follows the source's Proposition 1, Lagrangian relaxation, Lemma 2, Poisson request counts, policy profit identity, Gallego–van Ryzin moment bound, and Lemma S.5 on arrival-rate monotonicity. The last three supply the finite bound and its scaling statement in the Supplemental Note.

What the result gives

The finite bound quantifies the cost of using fixed base prices and greedy matching instead of the fluid ideal. Its two terms separate the loss from random mismatch and the extra waiting adjustment. The scaled bound says that, as both sides' arrival rates grow, the fraction of the fluid value lost by this policy vanishes at a rate governed by the slower-growing side. This offers a concrete reason to use a simple policy when the market is large, while keeping the smaller-market correction visible.

The paper already proves these claims. This mission asks for machine-checked proofs of their precise statements. The fluid optimizer, the clairvoyant matching problem, the marked Poisson arrival model, and the policy-profit identity are reusable mathematical objects beyond this theorem. The positive-part moment bound is an already published theorem and is referenced rather than posed again.

Where the argument is difficult

The obvious comparison between posted-price profit and fluid revenue misses the cost of requests that wait or never match. The price corrections themselves are conditional expectations divided by conditional match probabilities; their effect cannot be captured by simply subtracting a constant waiting charge. The proof must connect those corrections to the time integral of the queue imbalance, then control the imbalance of two Poisson request streams. A second difficulty is that the fluid optimum and the expected clairvoyant optimum are defined through different feasible sets, so their comparison needs a separate relaxation argument. These obstacles are visible in the source's proof of Lemma 2 and Theorem 2.

Formalization scope

The density and virtual-value environment is the published bilateral-trade definition, imported through a local name alias required by the frozen shared market module. Lean represents arrivals by independent Poisson counts and independent identically distributed time-and-value marks. This is equal in law to the paper's homogeneous marked Poisson processes on $[0,T]$ . Arrival time marks are uniform probability laws, and valuation and cost marks use the source densities. Simultaneous requests are ordered by index; such ties have probability zero. The deterministic program ranges over measurable, nonnegative, market-clearing paths with interval-integrable objective terms. Its value is the supremum of their objectives, not a formula involving $p^*$ and $w^*$ ; Proposition 1 must establish that formula. The clairvoyant value uses the published partial-assignment-game worth, so negative-weight pairs may remain unmatched.

The density functions are continuous on their supports, an explicit addition needed for the inverse prices and maximum volume used by Proposition 1. The lower support endpoints are nonnegative so the constant prices belong to the nonnegative fluid price domain; this fills an implicit domain convention in the manuscript. For Theorem 2 the overlap condition is strict, $\underline c<\overline v$ , ensuring positive $\mu^*$ and $p^*-w^*$ . The printed chain comparing $J/\mathbb E[\bar J]$ and $J/\bar J^*$ is stated under $J\ge0$ : when the numerator is negative, the claimed direction fails. Both expectations used as finite numbers are accompanied by integrability conclusions. Division by a zero match probability at the terminal time uses a zero convention on a set of arrival times with probability zero.

The policy model builds in the myopic request behavior that Theorem 1 identifies as an equilibrium; its strategic proof is outside this mission. The policy profit is the expectation of actual posted-price payments, and the waiting compensations are literal tagged-arrival conditional ratios. Contributions that prove the inverse-distribution properties, Poisson thinning, queue profit identity, fluid optimization, or final moment estimate all address parts of the stated target.

Selected references

Y. Chen and M. Hu, Pricing and Matching with Forward-Looking Buyers and Sellers, Manufacturing & Service Operations Management 22(4), 2020; submitted manuscript, SSRN 2859864.

12 thms2 active usersReviewed

Completed

Algebraic Topology Computational Geometry Machine Learning·Captain: mikedeng1

Persistence-Based Clustering in Riemannian Manifolds: With High Probability the Algorithm Returns as Many Clusters as the Density Has d₂-Prominent PeaksResearch Paper

Motivation

Mode-seeking clustering groups data points by the peak of an underlying probability density that they "flow up" to. Methods of this kind (mean-shift, graph-based hill climbing) are widely used, but their output depends heavily on noise: a density estimated from finitely many samples has many spurious local maxima, and each of them becomes a cluster. Chazal, Guibas, Oudot and Skraba (INRIA RR-6968, 2009; journal version J. ACM 60(6), 2013, doi:10.1145/2535927) combine graph-based hill climbing with topological persistence. Persistence measures how prominent each peak is, and peaks of low prominence are merged into their neighbours. The paper's main guarantee says when this algorithm recovers the right number of clusters from random samples. It holds on Riemannian manifolds that may be non-compact, and the clustering method is now known as ToMATo.

Setting

Let $\mathbb X$ be an $m$ -dimensional Riemannian manifold, possibly with boundary, with geodesic distance $d_{\mathbb X}$ and $m$ -dimensional Hausdorff measure $\mathcal H^m$ . The strong convexity radius $\varrho_c(\mathbb X)$ is the infimum over $x$ of the largest $r$ such that any two points of the closed ball $B_{\mathbb X}(x,r)$ are joined by a unique shortest path, and that path stays in the ball. Let $f:\mathbb X\to\mathbb R$ be a probability density with respect to $\mathcal H^m$ that is $c$ -Lipschitz, and write $\mathbb F^\alpha=f^{-1}([\alpha,+\infty))$ for its superlevel sets.

Persistence diagram. As $\alpha$ decreases from $+\infty$ to $-\infty$ , path components of $\mathbb F^\alpha$ are born at peaks of $f$ and die when they merge into an older component. The 0-th persistence diagram $D_0f$ records each component as a point $(p_x,p_y)$ of the extended plane $\overline{\mathbb R}^2$ , with birth $p_x$ and death $p_y\le p_x$ ; a component that never dies has $p_y=-\infty$ . The prominence of the peak is $p_x-p_y$ . The diagonal is added with infinite multiplicity. $f$ is tame when this structure is of finite type. For $d_2>d_1\ge0$ , $D_0f$ is $(d_1,d_2)$ -separated when every off-diagonal point either has prominence $<d_1$ (noise), or has prominence $\ge d_2$ and birth $>d_2$ (signal).

Algorithm. The input is $n$ sample points $x_1,\dots,x_n$ , the values $f(x_i)$ , the matrix of distances $d_{\mathbb X}(x_i,x_j)$ and parameters $\delta,\tau$ . The Rips graph $R_\delta$ joins two points at distance $\le\delta$ . The algorithm processes the points by decreasing $f$ and keeps a union-find structure whose entries are rooted at their highest point. When a point is processed, every neighbouring entry whose root is less than $\tau$ higher than the point is merged into the point's entry. The point's own entry is then merged into the neighbouring entry with the highest root, if its own root is less than $\tau$ higher than the point. The output is the set of final entries whose root has value $\ge\tau$ .

Sampling quantities. $\mathcal N_r(A)$ is the least number of closed geodesic balls of radius $r$ covering $A$ , and $\mathcal V_r(A)=\inf_{x\in A}\mathcal H^m(B_{\mathbb X}(x,r))$ .

Formalization targets

Goal: Theorem 4.8 (p. 22)

Assume $\varrho_c(\mathbb X)>0$ , $f$ is a tame $c$ -Lipschitz density, $D_0f$ is $(d_1,d_2)$ -separated, $0<\delta<\min\{\varrho_c(\mathbb X),\frac{d_2-d_1}{5c}\}$ and $\tau\in(d_1+2c\delta,\,d_2-3c\delta)$ . Then for $n$ i.i.d. samples from $f$ ,

\Pr\big[\#\text{clusters}\ne\#\{\text{peaks of prominence}\ge d_2\}\big]\le\mathcal N_{\delta/8}(\mathbb F^{c\delta})\,e^{-n\frac34c\delta\,\mathcal V_{\delta/8}(\mathbb F^{c\delta})}.

Milestones

Lemma 4.3 (p. 17): for $\varepsilon>0$ and $\alpha>c\varepsilon$ , the sample is a geodesic $\varepsilon$ -sample of $\mathbb F^\alpha$ except with probability at most $\mathcal N_{\varepsilon/2}(\mathbb F^\alpha)e^{-n(\alpha-c\varepsilon)\mathcal V_{\varepsilon/2}(\mathbb F^\alpha)}$ .
Theorem 4.5 (p. 19): if a finite $L$ is a geodesic $\delta/4$ -sample of $\mathbb F^\alpha$ , there is a multi-bijection between $D_0f$ and the diagram $D_0\mathcal R^f_\delta(L)$ of the upper-star Rips filtration. Above $\alpha$ it moves points by at most $c\delta$ , and in the lower-right quadrant it moves births by at most $c\delta$ .
Noise image (proof of Thm 4.8, p. 22): the noise points are sent into $\Delta^N_{d_1+2c\delta}\cup\Lambda^W_{d_1+2c\delta}$ .
Signal image (pp. 22–23): the signal points are sent outside that region.
Partition and count (p. 23): for $\tau$ in the range, $D_0\mathcal R^f_\delta(L)$ has exactly as many points in $\Delta^S_\tau\cap\Lambda^E_\tau$ as $D_0f$ has peaks of prominence $\ge d_2$ ; for the tame $D_0f$ both counts are finite.
Algorithm output (p. 23, with §3): for $\tau>0$ the algorithm returns exactly one cluster per point $q$ of the Rips diagram with $q_x-q_y\ge\tau$ and $q_x\ge\tau$ .

Significance

The theorem gives a sample-complexity guarantee for a practical clustering algorithm, with an explicit failure probability. It needs neither compactness of the manifold nor a density bounded away from zero; dense sampling of one superlevel set is enough. The separation hypothesis is a signal-to-noise condition, and it tells the user which range of $\tau$ recovers the true number of clusters.

On the formalization side, the paper's results are proved on paper, but nothing about them is machine-checked. Of the steps, the paper proves Lemma 4.3 and the region analysis. Theorem 4.5 rests on the Rips-filtration analysis of Chazal–Guibas–Oudot–Skraba, SODA 2009, the interleaving and stability results of Chazal et al., SoCG 2009, and the paper's Lemma 4.6. The algorithm-output step (milestone 6) is asserted in the paper, not proved. The mission therefore asks for formal proofs of all six steps. A by-product is the first library of 0-dimensional persistence diagrams, multi-bijections and Rips filtrations on the platform.

Difficulty

The probabilistic step is a union bound over a minimal cover, but it has a gap. Covering balls need not be centred in $\mathbb F^\alpha$ , while $\mathcal V$ is an infimum over balls centred in $\mathbb F^\alpha$ , so the comparison between the two is not justified on a general manifold. Theorem 4.5 is the hardest step. The obvious route, a bottleneck stability theorem, does not apply, because the sample covers only one superlevel set and not $\mathbb X$ . This is why the conclusion distinguishes the quadrant above $\alpha$ , where both coordinates are controlled, from the quadrant below, where only births are. Milestone 6 is a correctness proof for a union-find procedure with ties: entries are not path components, because prominent entries stay separate after their components meet.

Formalization scope

Manifold. $\mathbb X$ is a metric space carrying Mathlib's Riemannian manifold structure (IsRiemannianManifold, a ModelWithCorners for the boundary), so $d_{\mathbb X}$ is dist.
Measures and probability. $\mathcal H^m$ is Mathlib's unnormalized Hausdorff measure of dimension $\dim E$ ; the statements are invariant under rescaling it. Samples are product measures on Fin n → X. "With probability at least $1-B$ " is an upper bound $B\in[0,\infty]$ on the outer measure of the failure event. $e^{-aV}$ uses $e^{-\infty}=0$ and $0\cdot\infty=0$ .
Convexity radius. It is computed in $[0,+\infty]$ , with shortest paths as isometric embeddings of $[0,d(y,y')]$ .
Diagrams. A diagram's multiplicities are computed from the rank function of the filtration, so they are not free data.
Tameness is pinned in a 0-dimensional form: finitely many path components at each level, finitely many critical values, and empty superlevel sets at high levels.
Multi-bijections are bijections between copies of points, the diagonal contributing countably many copies of each of its points.
Separation is imposed on off-diagonal points only. On the diagonal the literal definition is unsatisfiable when $d_1=0$ .
Algorithm. It runs Procedures 1–2 with an explicit union-find state, over every processing order compatible with the sort. The upper star of a point is its set of neighbours processed earlier.
Added hypotheses. $c>0$ in Theorem 4.8 and milestones 3–5 (the paper divides by $c$ ), and $\tau>0$ in milestone 6.

No formalization in which the number of clusters is defined as a count of diagram points, or in which the diagram is a free parameter, is acceptable: either one empties the goal. The running-time and memory claims of §3, the basin approximation of Theorem 4.9 and the Morse-theoretic material of §2.3 are out of scope. Lemma 4.3 is stated as printed, with covering balls centred anywhere, and its proof gap is an open risk that Theorem 4.8 inherits.

Contributions are welcome on every milestone. The persistence-diagram layer (rank functions, multiplicities, multi-bijections) and the union-find correctness proof are reusable beyond this mission.

Selected references

F. Chazal, L. J. Guibas, S. Y. Oudot, P. Skraba, Persistence-Based Clustering in Riemannian Manifolds, INRIA Research Report RR-6968, 2009. https://inria.hal.science/inria-00389390
F. Chazal, L. J. Guibas, S. Y. Oudot, P. Skraba, Persistence-Based Clustering in Riemannian Manifolds, Journal of the ACM 60(6), 2013. https://doi.org/10.1145/2535927
F. Chazal, D. Cohen-Steiner, M. Glisse, L. J. Guibas, S. Y. Oudot, Proximity of Persistence Modules and their Diagrams, Proc. 25th ACM Symposium on Computational Geometry, 2009. https://doi.org/10.1145/1542362.1542407
D. Cohen-Steiner, H. Edelsbrunner, J. Harer, Stability of Persistence Diagrams, Discrete & Computational Geometry 37, 2007. https://doi.org/10.1007/s00454-006-1276-5
F. Chazal, L. J. Guibas, S. Y. Oudot, P. Skraba, Analysis of Scalar Fields over Point Cloud Data, SODA 2009. https://doi.org/10.1137/1.9781611973068.112

41 thms2 active usersReviewed

Markov Chain Stochastic Systems·Captain: mikedeng1

Generalized Couplings and Ergodic Rates for SPDEs and Other Markov Models: A Generalized Coupling and a Lyapunov Function Give a Unique Invariant Measure and Wasserstein Ergodic RatesResearch Paper

Motivation

Many Markov processes that arise as solutions of stochastic partial differential equations, stochastic delay equations, or other infinite-dimensional models are not strong Feller: their transition probabilities from two nearby starting points can be mutually singular. For such processes convergence to equilibrium cannot hold in total variation, and the classical Harris theorem (a Lyapunov function plus a minorization on a small set) does not apply. Hairer, Mattingly and Scheutzow ([23], 2011) replaced total variation by a coupling distance $W_d$ built from a suitable distance-like function $d$ , and proved a weak Harris theorem: contraction of $W_d$ on the whole space, $d$ -smallness of the level sets of a Lyapunov function, and the Lyapunov drift together give a unique invariant measure and a rate of convergence. Butkovsky ([6], 2014) extended it to subgeometric rates, and Kulik's monograph ([25], 2017) gives a systematic account.

The remaining difficulty is to verify the contraction hypothesis for a concrete model. Butkovsky, Kulik and Scheutzow (arXiv:1806.00395, Ann. Appl. Probab. 2020) show that it suffices to build a generalized coupling: a pair of processes whose first component has the correct law, whose second component is only close in law to the process started at the other point, and whose components approach each other. Their abstract theorem of §2 is the input to the paper's applications to stochastic functional differential equations and to the 2D Navier–Stokes, Euler-type and Boussinesq SPDEs of §4.

Setting

Let $(E,\rho)$ be a Polish space with Borel $\sigma$ -field $\mathcal E$ , and let $\{P_t\}_{t\ge0}$ be a Markov transition function: Markov kernels with $P_0(x,\cdot)=\delta_x$ and the Chapman–Kolmogorov identity. Write $P_tf(x)=\int f(y)\,P_t(x,dy)$ . The semigroup is Feller if $P_t$ maps bounded continuous functions to continuous functions.

A distance-like function $d:E\times E\to\mathbb R_+$ is symmetric, lower semicontinuous and vanishes exactly on the diagonal. A premetric $\theta$ is lower semicontinuous and vanishes exactly on the diagonal, but need not be symmetric. For probability measures $\mu,\nu$ , $\mathcal C(\mu,\nu)$ is the set of couplings and

W_d(\mu,\nu)=\inf_{\lambda\in\mathcal C(\mu,\nu)}\int d\,d\lambda\in[0,\infty].

$d_{TV}(\mu,\nu)=\sup_{A}|\mu(A)-\nu(A)|$ is the total variation distance.

A measurable $V\ge0$ satisfies the Lyapunov condition if, for a concave differentiable $\varphi:\mathbb R_+\to\mathbb R_+$ increasing to infinity with $\varphi(0)=0$ and a constant $K>0$ ,

P_tV(x)\le V(x)-\int_0^tP_s(\varphi\circ V)(x)\,ds+Kt,\qquad t\ge0,\ x\in E.

Put $H_\varphi(x)=\int_1^x du/\varphi(u)$ for $x\ge1$ .

Assumption A asks for a non-increasing $r$ with $r(t)\to0$ , a locally bounded $L$ , and for every $x,y$ a pair of processes $(X^{x,y},Y^{x,y})$ with $\mathrm{Law}(X^{x,y})=\mathsf P_x$ ,

d_{TV}\bigl(\mathrm{Law}(Y^{x,y}_t),P_t(y,\cdot)\bigr)\le L(t)\theta(x,y),\qquad \mathsf E\,\theta(X^{x,y}_t,Y^{x,y}_t)\le r(t)\theta(x,y).

Assumption B1 for a set $B$ and $t_0>0$ : for every $\varepsilon>0$ there is a set $D$ with $\inf_{x\in B}P_{t_0}(x,D)>0$ and $\sup_{x,y\in D}\theta(x,y)\le\varepsilon$ . Assumption B2 is a generalized-coupling version of B1 on a set $B$ . The paper's auxiliary distance is $d_N=N\theta(x,y)\wedge N\theta(y,x)\wedge1$ .

Formalization targets

Goal: Theorem 2.5

Assume $P$ is Feller, $V$ satisfies the Lyapunov condition, $\rho\wedge1\le\theta$ , Assumption A holds, and there is $t_0>0$ such that B1 holds for every level set $\{V\le M\}$ and $t_0$ . Then $(P_t)$ has a unique invariant probability measure $\pi$ , and for every $\delta\in(0,1)$ there are $C_1,C_2>0$ with

W_{\rho\wedge1}(P_t(x,\cdot),\pi)\le\frac{C_1\bigl(1+\varphi(V(x))^\delta\bigr)}{\varphi\bigl(H_\varphi^{-1}(C_2t)\bigr)^\delta},\qquad x\in E,\ t\ge0.

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

Companion: Theorem 2.6

In the exponential case $\varphi(x)=\gamma x$ , hypothesis B1 on all level sets may be replaced by B2 on the single level set $\{V\le4K/\gamma\}$ ; the same bound then holds and is exponential in $t$ .

Milestones

In attack order: $d_N$ is distance-like (2.6); the coupling lemma, the gluing lemma and the reimbursement bound used inside the proof of Theorem 2.3(i); Theorem 2.3(i) (contractivity of $d_N$ under A) and (ii) ( $d_N$ -smallness under B1); the remark after Definition 2.2 that contractivity and smallness give (2.3)–(2.4); the non-expansion step of the proof of Theorem 2.5; Proposition 2.1 (cited weak Harris theorem); and, for the companion, Theorem 2.3(iii), Proposition 2.2 (cited) and Theorem 2.6.

Significance

Theorem 2.5 turns the verification of the weak Harris theorem into two checks that can be carried out model by model: construct a controlled process that is close in law to the true one (Assumption A), and check a support condition on level sets (B1). It covers subexponential rates, given by the function $\varphi$ of the Lyapunov drift, and the Wasserstein distance it controls metrizes weak convergence. Theorem 2.6 is the abstract result behind the exponential ergodicity statements for SPDEs in §4 of the paper.

The results are proved in the paper; none of them, nor the weak Harris theorems of [6] and [23] they rely on, has a machine-checked proof. Mathlib has Markov kernels, their composition and invariant measures, but no coupling distances for lower semicontinuous costs, no maximal coupling or gluing lemma on Polish spaces, and no weak Harris theorem. Propositions 2.1 and 2.2 are cited by the paper, not proved there; formalizing them is part of the mission.

Difficulty

The obvious route to contraction is a true coupling of $P_t(x,\cdot)$ and $P_t(y,\cdot)$ whose components meet or approach. For processes without the strong Feller property, such a coupling is generally not available explicitly; the generalized coupling only gives the second marginal up to a total variation error. Turning the error-in-law bound into a statement about $W_{d_N}$ needs a maximal coupling of two laws on a Polish space and a gluing of two couplings along a common marginal, both of which rest on disintegration of measures. The cited Proposition 2.1 is itself a substantial result: existence of an invariant measure needs tightness from the Lyapunov drift and the Feller property, and the subexponential rate needs a careful interpolation between the drift and the contraction.

Formalization scope

The state space is any type with MetricSpace, CompleteSpace, SeparableSpace and the Borel σ-algebra; $\rho$ is dist. Time is ℝ≥0 and $P$ is a map ℝ≥0 → Kernel E E with Markov kernels, $P_0=\mathrm{id}$ , Chapman–Kolmogorov, and measurability of $s\mapsto P_s(x,A)$ , which the time integral in (2.2) presupposes. Expectations, $P_tV$ and $W_d$ are lower Lebesgue integrals in $[0,\infty]$ , and (2.2) is stated without subtraction ( $P_tV+\int_0^tP_s(\varphi\circ V)\,ds\le V+Kt$ ), which is equivalent. A pair of processes is represented by its joint law on path space; $\mathrm{Law}(X^{x,y})=\mathsf P_x$ is read through the one-dimensional marginals $\mathrm{Law}(X^{x,y}_t)=P_t(x,\cdot)$ , a weaker hypothesis. Total variation is the published MarkovChainCLT.tvDist, without a factor 2. "Unique invariant measure" means unique among probability measures, with invariance $\int P_t(x,\cdot)\,\pi(dx)=\pi$ for every $t$ . $H_\varphi^{-1}(C_2t)$ is encoded by quantifying over every $u\ge1$ with $H_\varphi(u)=C_2t$ ; such a $u$ exists and is unique under the Lyapunov condition. In Proposition 2.1 condition 2 is stated as $\rho\wedge1\le d$ , which is Proposition 2.1 for the equivalent complete metric $\rho\wedge1$ and is the form the proof of Theorem 2.5 uses.

No statement relies on a junk value: no Bochner integral of a possibly non-integrable function, no real-valued infimum over a possibly empty or unbounded set, no Measure.map along a non-measurable map, no default-valued inverse of $H_\varphi$ (which would make the bound read $W\le0$ ), and "invariant" is never used without "probability".

A complete development needs: Kantorovich-type coupling distances for lower semicontinuous costs, maximal couplings and gluing on Polish spaces, the transfer of $W_d$ -bounds through Markov kernels, and the weak Harris theorem with subexponential rates. All of these are reusable well beyond this mission. Contributions to any milestone, including the cited Propositions 2.1 and 2.2, are welcome.

Selected references

O. Butkovsky, A. Kulik, M. Scheutzow, Generalized couplings and ergodic rates for SPDEs and other Markov models, Ann. Appl. Probab. 30(1), 2020. arXiv:1806.00395, doi:10.1214/19-AAP1485
M. Hairer, J. C. Mattingly, M. Scheutzow, Asymptotic coupling and a general form of Harris' theorem with applications to stochastic delay equations, Probab. Theory Related Fields 149, 2011. arXiv:0902.4495
O. Butkovsky, Subgeometric rates of convergence of Markov processes in the Wasserstein metric, Ann. Appl. Probab. 24(2), 2014. arXiv:1211.4273
A. Kulik, Ergodic Behavior of Markov Processes, De Gruyter, Berlin, 2017. doi:10.1515/9783110458930
C. Villani, Optimal Transport: Old and New, Springer, 2009 (coupling lemma, Theorem 4.1; gluing, p. 23). doi:10.1007/978-3-540-71050-9

15 thms2 active usersReviewed

Markov Chain Optimal Transport·Captain: mikedeng1

Coupling and Convergence for Hamiltonian Monte Carlo 2: Lyapunov Bounds and Local Contractivity Give W_ρ(νπⁿ, ηπⁿ) ≤ e^{−cn}W_ρ(ν, η) + βⁿλⁿ⁻¹(∫ψdν + ∫ψdη)δ(C)Research Paper

Motivation

Markov chain Monte Carlo methods approximate a target probability measure by the law after $n$ steps of a Markov chain. A quantitative guarantee for such a method is a bound on the distance between the law after $n$ steps and the target, or between the laws of two copies of the chain started from different initial distributions. A standard route to such bounds is contractivity in a Kantorovich (Wasserstein) distance: if one step of the chain contracts the distance between any two initial laws by a factor $e^{-c}<1$ , the laws converge geometrically.

For many chains of practical interest, including Hamiltonian Monte Carlo with a numerical integrator, contractivity can only be proved on a bounded region of the state space. Outside it, the integrator may be unstable, or the coupling used to prove contraction may fail. Bou-Rabee, Eberle and Zimmer (arXiv:1805.00452, Ann. Appl. Probab. 30(3), 2020) isolate a general principle that turns such local contractivity into a global distance bound. It requires two Lyapunov functions: one controls how quickly the chain can leave the region of contraction, and one controls the distance once it has left. The principle is their Theorem 2.11. It is stated for an arbitrary Markov kernel on a complete separable metric space, and they apply it to adjusted numerical HMC (their Theorem 2.12).

Setting

Let $(S,\rho)$ be a complete separable metric space with Borel $\sigma$ -algebra $\mathcal B(S)$ , and let $\pi(x,dy)$ be a Markov transition kernel on $S$ . For a probability measure $\nu$ , the law after $n$ steps is $\nu\pi^n$ , where $\pi^0(x,\cdot)=\delta_x$ and $\pi^{n+1}=\pi\pi^n$ . For a non-negative function $f$ , $(\pi f)(x)=\int f(y)\,\pi(x,dy)$ .

A coupling of probability measures $\nu,\eta$ on $S$ is a probability measure on $S\times S$ with marginals $\nu$ and $\eta$ ; $C(\nu,\eta)$ is the set of couplings. The Kantorovich distance is

\mathcal W_\rho(\nu,\eta)=\inf_{\gamma\in C(\nu,\eta)}\int\rho(x,y)\,\gamma(dx\,dy)\in[0,\infty].

Assumption 2.3 asks for a constant $C\in(0,\infty)$ and measurable functions $\psi,\varphi:S\to(0,\infty)$ such that:

(C1) main Lyapunov condition: for some $\lambda\in[1,\infty)$ , $(\pi\psi)(x)\le\lambda\psi(x)$ whenever $\psi(x)\le C$ ;
(C2) global Lyapunov condition: for some $\beta\in[1,\infty)$ , $(\pi\varphi)(x)\le\beta\varphi(x)$ and $\rho(x,y)\le\varphi(x)+\varphi(y)$ for all $x,y$ ;
(C3) local contractivity: there are a probability space $(\Omega,\mathcal A,P)$ , a constant $c\in(0,\infty)$ and a measurable map $(X',Y'):S\times S\times\Omega\to S\times S$ . For every $x,y$ , the pair $(X'(x,y,\cdot),Y'(x,y,\cdot))$ is a coupling of $\pi(x,\cdot)$ and $\pi(y,\cdot)$ , and $E[\rho(X'(x,y,\cdot),Y'(x,y,\cdot))]\le e^{-c}\rho(x,y)$ whenever $\psi(x)\le C$ and $\psi(y)\le C$ .

Finally,

\delta(C)=\sup\Big\{\frac{\varphi(x)+\varphi(y)}{\psi(x)+\psi(y)}:x,y\in S,\ \psi(x)>C\text{ or }\psi(y)>C\Big\}\in[0,\infty].

Formalization targets

Goal: Theorem 2.11

Under Assumption 2.3, for every $n\in\mathbb N$ and all probability measures $\nu,\eta$ on $(S,\mathcal B(S))$ ,

\mathcal W_\rho(\nu\pi^n,\eta\pi^n)\le e^{-cn}\mathcal W_\rho(\nu,\eta)+\beta^n\lambda^{n-1}\Big(\int\psi\,d\nu+\int\psi\,d\eta\Big)\delta(C).\tag{42}

The constants are those of the paper and are not weakened. Each quantity may be infinite, and the bound is read in $[0,\infty]$ .

Milestones

Lemma 6.1. If a measurable coupling contracts $\rho$ by $e^{-c}$ in one step from every pair in $A\times A$ , then for every initial coupling $\gamma$ there is a coupled Markov chain $(X_n,Y_n)$ with $(X_0,Y_0)\sim\gamma$ and both marginals Markov with kernel $\pi$ . Along this chain, $M_n=e^{c(n\wedge T)}\rho(X_{n\wedge T},Y_{n\wedge T})$ is a non-negative supermartingale, where $T$ is the exit time from $A\times A$ .
(134). $e^{cn}E[\rho(X_n,Y_n);n\le T]\le E[M_n]\le\int\rho\,d\gamma$ .
(135). $E[\rho(X_n,Y_n);n>T]\le\beta^nE[\psi(X_T)+\psi(Y_T);n>T]\,\delta(C)$ , through the intermediate bounds by $\varphi$ .
(136). $E[\psi(X_T)+\psi(Y_T);n>T]\le\lambda^{n-1}\big(\int\psi\,d\nu+\int\psi\,d\eta\big)$ .

Significance

The result. Theorem 2.11 separates two tasks that are usually entangled in convergence proofs for Markov chains on unbounded spaces. One is a contraction estimate that only has to hold on a sublevel set $\{\psi\le C\}$ . The other is a pair of drift conditions that control excursions out of that set. The second term of (42) is made small by choosing $C$ large, and the first by choosing $n$ large. In the paper this gives $\mathcal W^1$ bounds to the invariant measure for adjusted numerical HMC (Theorem 2.12), whose contraction (Theorems 2.4 and 2.7) is only established on a ball. The theorem uses nothing about HMC and applies to any chain with a locally contractive coupling and the two Lyapunov conditions. Examples are other discretized diffusions and Metropolis-adjusted samplers.

Formalizing it. The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization requires constructing a Markovian coupling on a general measurable space and working with a generalized, $[0,\infty]$ -valued supermartingale stopped at an exit time. It also needs the Markov property with respect to the joint filtration of a coupled pair. Both pieces are reusable in coupling arguments for Markov chains in general.

Difficulty

Contraction on $\{\psi\le C\}^2$ gives no control once either copy leaves that set, and the exit time $T$ is random and may be infinite. The bound therefore has to be split at $T$ . On $\{n\le T\}$ the contraction accumulates, which requires optional stopping for a supermartingale that need not be integrable, because $\int\rho\,d\gamma$ may be $+\infty$ . On $\{n>T\}$ the distance at time $n$ has to be bounded by quantities at the random time $T$ . This requires the Markov property of each copy with respect to the filtration of the pair: the event $\{T=k\}$ depends on both copies. A Markov property of each copy in its own filtration does not suffice. Finally, $\psi$ at the exit time has to be controlled by its initial integral, which is a second stopped supermartingale built from (C1).

Formalization scope

$(S,\rho)$ is a Lean MetricSpace with its Borel $\sigma$ -algebra, complete and separable; $\rho$ is dist. $\pi$ is a Markov kernel (Kernel S S with IsMarkovKernel), and $\nu\pi^n$ is the bind of $\nu$ with the $n$ -fold composition of $\pi$ .
Every expectation of a non-negative quantity, every $\int\psi\,d\nu$ , $\delta(C)$ and $\mathcal W_\rho$ is valued in $[0,\infty]$ (lower Lebesgue integrals, ℝ≥0∞). No Bochner integral appears, so a non-integrable quantity can never be replaced by a junk $0$ . In particular, $\int\psi\,d\nu=\infty$ is allowed, as on the page.
Couplings are the published definition MongeKantorovichYao.transferencePlans.
(C3)'s probability space and coupling map are parameters of the theorem, which then holds for every such realization.
$\lambda^{n-1}$ is an integer power, so $n=0$ is included (and (42) is then trivially true).
Lemma 6.1's chain is the coordinate process on the path space $(S\times S)^{\mathbb N}$ , which is determined up to its law. The supermartingale property is the generalized one, $E[M_{n+1};F]\le E[M_n;F]$ for $F\in\mathcal F_n$ . Mathlib's Supermartingale requires integrability, which the page does not assume. The exit time is $\mathbb N\cup\{\infty\}$ -valued, and $n\wedge T=n$ when the chain never leaves.
The marginal Markov property is stated with respect to the filtration of the pair. This is what the proof of (135) and (136) uses, and it implies the marginal Markov property in each copy's own filtration.
The proof on p. 43 applies Lemma 6.1 "with $A=\{\psi>C\}$ ". The set on which (C3) contracts and whose exit time is $T$ is $\{\psi\le C\}$ , and that set is used. The text before (135) says " $\{n<T\}$ " where its displays use $\{n>T\}$ , and the displays are formalized.
A formalization in which $\mathcal W_\rho$ or $\delta(C)$ is a real number obtained by truncating $+\infty$ , or in which the measures need not be probability measures (so that the coupling set is empty and $\mathcal W_\rho=\infty$ ), would make (42) vacuous and is excluded.

A complete development needs Ionescu-Tulcea's construction of a Markov chain on a general measurable space (ProbabilityTheory.Kernel.traj in Mathlib), the measurability of the coupling kernel $(x,y)\mapsto P\circ(X',Y')(x,y,\cdot)^{-1}$ , and optional stopping for $[0,\infty]$ -valued supermartingales stopped at an exit time. Contributions are welcome on the milestones individually. The optional-stopping and joint-Markov-property lemmas are reusable beyond this mission.

Selected references

N. Bou-Rabee, A. Eberle, R. Zimmer, Coupling and convergence for Hamiltonian Monte Carlo, Ann. Appl. Probab. 30(3), 2020. arXiv:1805.00452 (v2 is the version cited here).
A. Joulin, Y. Ollivier, Curvature, concentration and error estimates for Markov chain Monte Carlo, Ann. Probab. 38(6), 2010. doi:10.1214/10-AOP541
C. Villani, Optimal Transport: Old and New, Springer, 2009. doi:10.1007/978-3-540-71050-9

7 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning·Captain: mikedeng1

A Tutorial on Thompson Sampling II: Under Thompson Sampling, Per-Period Expected Regret Splits into a Pessimism Term and a Width Term for Any History-Determined U_tResearch Paper

Motivation

An online decision maker repeatedly chooses an action, observes an outcome, and receives a reward. In a Bayesian model, an unknown parameter controls the outcomes, and the decision maker begins with a prior distribution for that parameter. Thompson sampling acts by drawing a parameter from its current posterior distribution and choosing an action that would be best if that draw were correct. This makes it applicable when an agent can simulate a plausible model and optimize an action for that model. Russo, Van Roy, Kazerouni, Osband, and Wen explain this rule for general online decision problems in Section 4 of their tutorial.

The tutorial's Section 8.1.2 asks how to analyze the rule's expected regret. An upper confidence bound method chooses an action using an optimistic score and can analyze regret through the score's optimism and its uncertainty width. Thompson sampling does not choose its actions by maximizing such a score. Yet the tutorial shows that any score computed from the observed past can be used to split Thompson sampling's expected regret into the same two types of terms. The result is stated on pp. 72–73, equation (8.4) and the display that follows.

Setting

Let $\mathcal X$ be a finite, nonempty set of actions, $Y$ a finite set of outcomes, and $\Theta$ a measurable parameter space. A prior probability measure $P$ is placed on the unknown parameter $\theta\in\Theta$ . If action $x\in\mathcal X$ is selected, the outcome is sampled from a probability kernel $q_\theta(\cdot\mid x)$ on $Y$ . A known function $r:Y\to\mathbb R$ turns an outcome into a reward. The mean reward of action $x$ under parameter $\theta$ is

\mu(x,\theta)=\sum_{y\in Y}q_\theta(y\mid x)r(y).

For each $\theta$ , choose an action $x^*(\theta)$ maximizing $\mu(\cdot,\theta)$ . This choice uses a fixed tie-break and is measurable. The same selector is used throughout the mission. A length- $t$ history $H_t$ records the first $t$ action–outcome pairs. A policy $\pi$ assigns an action distribution to every such history. The prior, the policy, and the outcome kernel together determine the law of all histories: first draw $\theta$ from $P$ , then choose each action from $\pi$ using the past history, and finally generate its outcome using $q_\theta$ .

After history $h$ , the posterior law of $x^*$ is obtained by reweighting the prior by the likelihood of the observed outcomes. Thompson sampling draws a parameter from this posterior and plays the selected optimum for that parameter. Thus the law of its next action, given $h$ , is the posterior law of $x^*$ given $h$ . The policy remains defined even for a history with zero likelihood; choices there do not affect expectations.

For a period $t$ , let $U_t(x)$ be any real score that uses the action $x$ and the observed history $H_{t-1}$ . The score is fixed before the period's outcome or the unknown parameter can be inspected. The period regret is $\mu(x^*,\theta)-\mu(x_t,\theta)$ , with expectation taken over the prior, the policy's randomization, and the outcome process.

Formalization targets

Probability matching and equation (8.4)

The first target makes posterior sampling precise. For every feasible history $h$ and action $a$ , the probability that Thompson sampling next plays $a$ , together with observing $h$ , equals the joint probability that the selected optimum is $a$ and the history is $h$ . Consequently, for every history-determined $U_t$ ,

\mathbb E_\pi[U_t(x_t)] =\mathbb E_\pi[U_t(x^*)].

This is equation (8.4) on p. 72. It asserts equality of unconditional expectations while preserving the fact that $U_t$ may depend on the past. It does not assert that $x_t$ and $x^*$ have the same joint law with $\theta$ .

Per-period regret decomposition

The goal is the full chain of equalities displayed on p. 73:

\begin{aligned} \mathbb E_\pi[\mu(x^*,\theta)-\mu(x_t,\theta)] &=\mathbb E_\pi[\mu(x^*,\theta)-U_t(x_t)] +\mathbb E_\pi[U_t(x_t)-\mu(x_t,\theta)]\\ &=\underbrace{\mathbb E_\pi[\mu(x^*,\theta)-U_t(x^*)]}_{\text{pessimism}} +\underbrace{\mathbb E_\pi[U_t(x_t)-\mu(x_t,\theta)]}_{\text{width}}. \end{aligned}

The theorem holds for every score $U_t$ determined by the past history. In particular, $U_t$ need not be a confidence bound for the identity to hold. Being a useful upper confidence bound matters when one later estimates the two terms.

Significance

The equality permits analyses built around optimistic scores to be transferred to Thompson sampling. It separates expected regret into a term measuring whether the score falls below the true optimal mean and another measuring the gap between the score and the true mean at the sampled action. The tutorial cites Russo and Van Roy for the surrounding regret bounds; the identity here is the precise bridge used in that discussion.

The result is already proved in the tutorial. This mission seeks a machine-checked proof of its finite-action, finite-outcome form, including the posterior-sampling law, the policy-dependent history distribution, and the conditioning behind equation (8.4). The goal and milestones are open Lean statements, not completed machine-checked proofs. Their definitions can be reused in later finite Bayesian decision models with a general measurable parameter.

Difficulty

The central issue is that $x_t$ and $x^*$ are not interchangeable inside an expression that depends on $\theta$ . The sampled action and the selected optimum have the same distribution after conditioning on the observed past, but generally have different dependence on the true parameter. For example, replacing $U_t$ by $\mu(\cdot,\theta)$ would make the claimed equality false. A formal proof therefore has to respect the boundary between history-derived scores and parameter-dependent quantities, and it must use the same history law to interpret every expectation. Histories of zero probability also require a consistent posterior convention.

Formalization scope

The Lean model uses finite action and outcome types and a general measurable parameter type. This is a disclosed specialization of the tutorial, which also allows infinite actions and more general outcome spaces. The kernel $q_\theta$ is nonnegative, sums to one over outcomes, and is measurable in $\theta$ . The prior is a probability measure. The reward function is real valued and bounded because its domain is finite. The optimal-action selector has measurable fibers and maximizes the mean reward for every parameter. These conditions make the integrands measurable and bounded, avoiding default values of nonintegrable Lean integrals.

Histories are functions from a finite period index to action–outcome pairs. Policies are normalized, nonnegative behavioural action probabilities. The likelihood of a history multiplies both its policy action factors and its kernel outcome factors. The posterior uses only outcome likelihood factors, which give the Bayes update on every positive-evidence history. The Thompson-sampling predicate enforces the posterior action probabilities on those histories and permits any normalized policy on impossible ones. Lean period $s$ denotes the tutorial's period $t=s+1$ .

The shared tie-break is essential: Thompson sampling and $x^*$ use the same selected maximizer. The score has type $H_{t-1}\to\mathcal X\to\mathbb R$ , so it cannot inspect $\theta$ or the current outcome. No definition is allowed to supply regret or the decomposition as a predetermined constant; the expectation is built from the prior, policy and outcome kernel. The development needs reusable definitions for the Bayesian model, finite histories, behavioural policies, likelihoods, posterior masses, and the two regret terms. Contributions proving probability matching, equation (8.4), and the final identity are welcome.

Selected references

Daniel J. Russo, Benjamin Van Roy, Abbas Kazerouni, Ian Osband, and Zheng Wen, A Tutorial on Thompson Sampling, Foundations and Trends in Machine Learning 11(1), 2018. DOI: 10.1561/2200000070.

4 thms2 active usersReviewed

Markov Chain Numerical Analysis Optimal Transport·Captain: mikedeng1

Coupling and Convergence for Hamiltonian Monte Carlo 1: Exact HMC Contracts the Concave Kantorovich Distance W_ρ at Rate c = (1/10)·min(1, ½KT²(1+ℛ/T)e^{−ℛ/(2T)})·e^{−2ℛ/T}Research Paper

Why convergence bounds for Hamiltonian Monte Carlo matter

Hamiltonian Monte Carlo (HMC) is one of the most widely used Markov chain Monte Carlo methods for sampling from a probability density $\mu(dx)\propto e^{-U(x)}\,dx$ on $\mathbb R^d$ . It is the default sampler of probabilistic programming systems such as Stan, and it is used throughout Bayesian statistics, molecular dynamics and machine learning. In practice the chain is run for a finite number of steps, and a user needs to know how many steps make its law close to $\mu$ . That requires a quantitative, dimension-explicit convergence bound.

Before the paper of Bou-Rabee, Eberle and Zimmer, such bounds were known essentially only when $U$ is strongly convex everywhere: then two copies of the chain driven by the same random velocity contract deterministically (Mangoubi and Smith, arXiv:1708.07114). Bou-Rabee, Eberle and Zimmer (arXiv:1805.00452, Ann. Appl. Probab. 30(3), 2020) remove global convexity. They require $U$ to be strongly convex only outside a ball, and they introduce a coupling of two HMC transitions under which a suitably concave distance contracts on average for every pair of starting points. This mission formalizes that contraction theorem for exact HMC, together with its consequence, exponential convergence in the $L^1$ Wasserstein distance.

Setting

Let $U:\mathbb R^d\to\mathbb R$ be four times continuously differentiable with $\int e^{-U}<\infty$ . The Hamiltonian is $H(x,v)=U(x)+\tfrac12|v|^2$ , and the exact Hamiltonian flow $(q_t,p_t)$ solves

\tfrac{d}{dt}q_t=p_t,\qquad \tfrac{d}{dt}p_t=-\nabla U(q_t),\qquad (q_0(x,v),p_0(x,v))=(x,v).

Fix a duration $T>0$ . One step of exact HMC from $x$ draws a fresh velocity $\xi\sim N(0,I_d)$ and moves to $X'(x)=q_T(x,\xi)$ ; its transition kernel is $\pi(x,\cdot)=\mathrm{law}(q_T(x,\xi))$ , and $\mu$ is invariant for $\pi$ .

(x-y)\cdot(\nabla U(x)-\nabla U(y))\ge K|x-y|^2\quad\text{whenever }|x-y|\ge\mathcal R.

The coupling. For two starting points $x,y$ with $z=x-y$ , $e=z/|z|$ , both copies use the same $\xi$ . If $|x-y|\ge2\mathcal R$ the second copy also uses $\xi$ (synchronous coupling). If $|x-y|<2\mathcal R$ it uses

\eta=\begin{cases}\xi+\gamma z&\text{if }\tilde{\mathcal U}\le\varphi_{0,1}(e\cdot\xi+\gamma|z|)/\varphi_{0,1}(e\cdot\xi),\\ \xi-2(e\cdot\xi)e&\text{otherwise,}\end{cases}

with $\tilde{\mathcal U}\sim\mathrm{Unif}(0,1)$ independent of $\xi$ and $\varphi_{0,1}$ the standard normal density. This is a maximal coupling of $N(0,I_d)$ with its shift by $\gamma z$ , completed by a reflection. The coupled positions are $X'=q_T(x,\xi)$ and $Y'=q_T(y,\eta)$ , with $R'(x,y)=|X'-Y'|$ .

The distance and the parameters. With $\gamma=\min(T^{-1},\mathcal R^{-1}/4)$ , $a=T^{-1}$ and $R_1=\tfrac52(\mathcal R+T)$ , set

f(r)=\int_0^r e^{-a\min(s,R_1)}\,ds,\qquad \rho(x,y)=f(|x-y|),

and let $\mathcal W_\rho(\nu,\eta)=\inf_{\gamma\in C(\nu,\eta)}\int\rho\,d\gamma$ be the Kantorovich distance over couplings $C(\nu,\eta)$ .

Formalization targets

Goal: Theorem 2.3

Under Assumption 2.1 and $LT^2\le\min(K/L,\tfrac14,\tfrac1{16\Lambda})$ with $\Lambda=16L\mathcal R^2$ , for all $x,y\in\mathbb R^d$ ,

E\bigl[f(R'(x,y))\bigr]\le(1-c)\,f(|x-y|),\qquad c=\frac1{10}\min\Bigl(1,\frac12KT^2\Bigl(1+\frac{\mathcal R}{T}\Bigr)e^{-\mathcal R/(2T)}\Bigr)e^{-2\mathcal R/T}.

This is the paper's main result for exact HMC, stated with its own constants.

Milestones (in the order of the proof)

(112)–(116): the parameter inequalities $\gamma T\le1$ , $LT\le\gamma/4$ , $\gamma\mathcal R\le\tfrac14$ , $aT\ge1$ , $R_1\ge\tfrac52(1+\gamma T)\mathcal R$ .
Lemma 3.4 ( $h=0$ ): $|q_t(x,v)-q_t(y,v)|^2\le(1-Kt^2/2)|x-y|^2$ for $|x-y|\ge2\mathcal R$ .
Theorem 2.1: the synchronous coupling contracts far-apart points, $R'^2\le(1-\tfrac12KT^2)r^2$ .
(119)–(120): $\inf_{r>0}rf'(r)/f(r)\ge\max(1,aR_1)e^{-aR_1}$ , and the resulting bound on $c_1$ .
Lemma 3.2 ( $h=0$ ): first-variation bounds for the flow.
Term I: on $\{\eta=\xi+\gamma z\}$ , $R'\le(1-\tfrac34\gamma T)r$ .
Lemma 3.7 (62): $P[\xi-\eta\ne-\gamma z]\le|\gamma z|/\sqrt{2\pi}$ .
(123): the truncated loss on the reflection event is at most $(\gamma T/\sqrt{2\pi})\,rf'(r)$ .
Term III: $E[(R'-R_1)^+;\,\xi-\eta\ne-\gamma z]\le\tfrac54\gamma rT$ .
(127): $\tfrac15\gamma T\max(1,2a\mathcal R)e^{-2a\mathcal R}\ge\tfrac1{10}e^{-2\mathcal R/T}$ .

Companions

The coupling property ( $\eta\sim N(0,I_d)$ , p. 9), Corollary 2.8 ( $\mathcal W_\rho(\nu\pi^n,\eta\pi^n)\le e^{-cn}\mathcal W_\rho(\nu,\eta)$ , the $\mathcal W^1$ bound with factor $M=e^{\frac52(1+\mathcal R/T)}$ , and the step count (41)), and the comparison (133), $e^{-aR_1}|x-y|\le\rho(x,y)\le|x-y|$ .

Significance

Theorem 2.3 gives a contraction rate for exact HMC that depends on $d$ only through the constants $L$ , $K$ and $\mathcal R$ of the potential, and that holds without global convexity. Through the coupling characterization of $\mathcal W_\rho$ it yields Corollary 2.8, an explicit number of steps after which the law of the chain is within $\epsilon$ of $\mu$ in $\mathcal W^1$ . The same coupling and concave-distance technique underlies the paper's results for numerical (velocity Verlet) HMC and later work on Langevin and HMC couplings.

The theorems are proved in the paper; none of them is machine-checked. Formalizing them requires the Hamiltonian ODE flow and its first-variation estimates, a Gaussian maximal/reflection coupling, and the transfer from one-step contraction to Kantorovich contraction of Markov kernels. Each of these is reusable well beyond HMC. A formal development also settles the constants. Three printed displays of the proof are not delivered by the printed argument, and Theorem 2.1 as printed is false, while the goal itself survives: see Formalization scope.

Difficulty

The obvious argument fails for nearby points. When $|x-y|<2\mathcal R$ , $U$ may be non-convex between them, and the synchronous coupling can push the two trajectories apart. The coupling must therefore change the velocity of one copy, and doing so makes the contraction only hold on average, on the event $\eta=\xi+\gamma z$ . On the complementary reflection event the distance can grow, and the growth must be paid for by the concavity of $f$ , through the truncation at $R_1$ and the tail term. Balancing these terms, uniformly in $x$ , $y$ and $d$ , is the heart of the proof. For far-apart points the difficulty is different: the contraction of Lemma 3.4 needs the trajectories to stay outside the non-convex region over the whole time interval, which is where the condition $LT^2<K/L$ enters.

Formalization scope

Space and objects. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d); $\nabla U$ is Mathlib's gradient, and $\nabla^kU$ is iteratedFDeriv. $L,M,N$ are upper bounds on the derivative norms, which is equivalent for every statement here. The flow is pinned by a predicate on $(q,p)$ (initial values and the ODE for all $t\in\mathbb R$ ); it is never a free function. Assumption 2.1 includes the standing hypotheses of §2.1: $U\in C^4$ , $\int e^{-U}<\infty$ , and $T$ deterministic.
Probability. The randomness of one step is $(\xi,\tilde{\mathcal U})$ with law $N(0,I_d)\otimes\mathrm{Unif}(0,1)$ . Expectations of nonnegative quantities are Lebesgue integrals in $[0,\infty]$ . The signed expectation in (123) uses a Bochner integral together with an explicit integrability conclusion, so no bound can hold because a non-integrable integral is read as $0$ . Kantorovich distances take values in $[0,\infty]$ over the published set of couplings MongeKantorovichYao.transferencePlans. The $n$ -step kernel is the iterated composition $\pi^{n+1}=\pi\circ\pi^n$ .
Conventions at $\mathcal R=0$ . $\gamma$ is $T^{-1}$ and $LT^2\le1/(16\Lambda)$ is written $256L^2\mathcal R^2T^2\le1$ , so that no division by zero decides a constant.
Corrections. The strict condition (56) in Lemma 3.4 is written $L^2t^2<K$ , which preserves its meaning at $L=0$ . Theorem 2.1 is stated as its proof delivers it, $R'^2\le(1-\tfrac12KT^2)r^2$ . The printed $R'\le(1-\tfrac12KT^2)r$ fails for $U(x)=\tfrac12|x|^2$ , where $R'=|\cos T|\,r$ . The displays (117), (122), the last inequality of (124), and (126) are not posed, because the printed argument does not deliver their constants. The goal's rate $c$ of (32) is nevertheless unaffected: under the step condition and $d\ge1$ , $c=\tfrac1{20}KT^2(1+\mathcal R/T)e^{-5\mathcal R/(2T)}$ , which lies below both corrected rates $c_1$ and $c_2$ .
Ruled out. The goal is not trivialized by a vacuous hypothesis: the hypotheses are met by $U(x)=\tfrac12|x|^2$ , $L=K=1$ , $\mathcal R=0$ , $T=\tfrac12$ . Nor is it trivialized by a junk value: $f$ , $R'$ and the integral are genuine, and the flow is the unique solution of the ODE.
Contributions welcome. Gronwall-type first-variation bounds for Lipschitz Hamiltonian flows, the Gaussian maximal/reflection coupling (Lemma 3.7 and the coupling property), and the general passage from a one-step average contraction to $\mathcal W_\rho$ contraction of a Markov kernel.

Selected references

N. Bou-Rabee, A. Eberle, R. Zimmer, Coupling and convergence for Hamiltonian Monte Carlo, Ann. Appl. Probab. 30(3), 2020. arXiv:1805.00452, doi:10.1214/19-AAP1528
O. Mangoubi, A. Smith, Rapid mixing of Hamiltonian Monte Carlo on strongly log-concave distributions, 2017. arXiv:1708.07114
A. Eberle, Reflection couplings and contraction rates for diffusions, Probab. Theory Related Fields 166, 2016. arXiv:1305.1233
A. Eberle, A. Guillin, R. Zimmer, Couplings and quantitative contraction rates for Langevin dynamics, Ann. Probab. 47(4), 2019. arXiv:1703.01617

13 thms2 active usersReviewed

Machine Learning Statistics·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 Statistics·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

Douglas 2003: Statistics of String Vacua — Flux Counting and Gaussian EnsemblesResearch Paper

Motivation

String/M theory appears to admit a very large number of four-dimensional vacua, and M. R. Douglas's 2003 paper The statistics of string/M theory vacua proposes to study them statistically: instead of constructing vacua one at a time, one places a measure on a space of effective theories and computes expected numbers and distributions of vacua. Two concrete mathematical ingredients of that programme are the subject of this mission.

The first is the Bousso–Polchinski counting of flux vacua (Section 3.6 of the paper, following Bousso–Polchinski 2000). Quantized fluxes form an integer vector $N\in\mathbb Z^J$ , and the flux energy is a positive quadratic form in $N$ . The number of flux choices with energy below $V$ controls whether a small cosmological constant can be realised; the paper evaluates the number distribution (3.13) by replacing the lattice sum with an integral, obtaining a density proportional to $V^{J/2-1}\,dV$ .

The second is the Gaussian ensemble of superpotentials (Section 4 and 4.1): a random polynomial superpotential whose coefficients are independent complex Gaussians, with an explicit normalising constant and an explicit count of coefficients.

Setting

Fix an integer $J\ge 0$ (the number of independent flux quanta, $J=b_{p+1}$ in the paper) and a constant $c>0$ (in the paper $c=M_{pl}^2/(M^{2p}V_{p+1}^2)$ ). For a flux vector $N=(N_1,\dots,N_J)\in\mathbb Z^J$ the flux potential is

V(N)=c\sum_{i=1}^J N_i^2 ,

and the flux vacua count below level $V$ is

\mathcal N_J(c,V)=\#\{N\in\mathbb Z^J : V(N)\le V\}.

This is the cumulative distribution function of the measure $d\mu(V)=\sum_N\delta(V-V(N))$ of eq. (3.13). The unit ball in $\mathbb R^J$ has volume $\omega_J=\pi^{J/2}/\Gamma(J/2+1)$ , and the unit sphere has area $\mathrm{Vol}(S^{J-1})=2\pi^{J/2}/\Gamma(J/2)=J\omega_J$ .

For the superpotential ensemble, a polynomial in $n$ variables of degree at most $d$ has one coefficient per monomial $z^{I}=z_1^{I_1}\cdots z_n^{I_n}$ with $|I|\le d$ ; the paper states there are $c(d,n)=(d+n)!/(d!\,n!)$ of them. The coefficients $w_I\in\mathbb C$ are given the weight $(\alpha/\pi)^{c(d,n)}\prod_I d^2w_I\,e^{-\alpha|w_I|^2}$ , $\alpha>0$ , which the paper says is unit normalised.

Formalization targets

Goal: asymptotic count of flux vacua

\lim_{V\to\infty}\frac{\mathcal N_J(c,V)}{(V/c)^{J/2}}=\frac{\pi^{J/2}}{\Gamma(J/2+1)} .

This is the precise, integrated form of the approximation in (3.13): integrating $\tfrac12\mathrm{Vol}(S^{J-1})\,c^{-J/2}v^{J/2-1}$ from $0$ to $V$ gives exactly $\omega_J (V/c)^{J/2}$ .

Milestones

Finiteness: for every $V$ , only finitely many $N\in\mathbb Z^J$ satisfy $V(N)\le V$ (so $\mathcal N_J$ is a genuine count).
Continuum volume: the Lebesgue volume of $\{x\in\mathbb R^J : c\sum x_i^2\le V\}$ equals $\omega_J (V/c)^{J/2}$ for $V\ge 0$ .
Continuum density (3.13): for $0\le V_1\le V_2$ and $J\ge1$ , the volume of the shell $\{V_1<c\sum x_i^2\le V_2\}$ equals $\int_{V_1}^{V_2}\tfrac12\mathrm{Vol}(S^{J-1})\,c^{-J/2}\,v^{J/2-1}\,dv$ .
Coefficient count: $\#\{I\in\mathbb N^n : |I|\le d\}=\#\{I\in\mathbb N^{n+1} : |I|=d\}=(d+n)!/(d!\,n!)$ .
Normalisation of the complex Gaussian ensemble: $\int_{\mathbb C^m}(\alpha/\pi)^m e^{-\alpha\sum_I|w_I|^2}\,d^{2m}w=1$ for every $m$ and $\alpha>0$ .

Significance

The goal makes rigorous the step "replace the sum with an integral" that underlies the Bousso–Polchinski estimate of how many flux vacua lie below a given energy, with the exact constant appearing in (3.13). Milestones 4 and 5 certify the combinatorial and analytic constants of the Gaussian ensemble (4.6) on which the paper's densities (4.7)–(4.10) are built. None of these results is new mathematics: the goal is the $J$ -dimensional analogue of the Gauss circle problem at leading order, and the milestones are classical. What the mission adds is a machine-checked version of the precise constants used in the paper.

Difficulty

The goal requires comparing a lattice-point count with a volume. The naive bound, counting unit cubes centred at lattice points, must be controlled uniformly: cubes meeting the boundary of the ball contribute an error of order $R^{J-1}$ with $R=\sqrt{V/c}$ , and one has to show that this is $o(R^J)$ . The volume formula for Euclidean balls expressed through the Gamma function, and its transport to the product space $\mathbb R^J$ with the sum-of-squares form, is further required infrastructure.

Formalization scope

Flux vectors are functions Fin J → ℤ; the count uses Set.ncard, whose value on an infinite set would be $0$ — milestone 1 rules out that degenerate reading.
Continuum statements use the product Lebesgue measure on Fin J → ℝ (not EuclideanSpace), with the quadratic form $c\sum x_i^2$ written out explicitly.
The Gaussian ensemble is formalised only for complex coefficients (the "GUE" case). For real coefficients the paper's constant $(\alpha/\pi)^{c(d,n)}$ would not normalise the measure (the correct constant is $(\alpha/\pi)^{c(d,n)/2}$ ), so the real case is deliberately omitted.
The paper's finiteness conjecture (3.16) for full string compactifications, and the densities (4.7)–(4.10), are not formalised; they are not stated precisely enough in the source.
Definitions: DouglasVacua.fluxPotential, DouglasVacua.fluxVacuaCount.

Selected references

M. R. Douglas, The statistics of string/M theory vacua, JHEP 05 (2003) 046. https://doi.org/10.1088/1126-6708/2003/05/046 — arXiv:hep-th/0303194
R. Bousso, J. Polchinski, Quantization of four-form fluxes and dynamical neutralization of the cosmological constant, JHEP 06 (2000) 006. https://arxiv.org/abs/hep-th/0004134

7 thms2 active usersReviewed

Information Theory Machine Learning Statistics·Captain: mikedeng1

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

Motivation

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

Setting

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

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

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

Formalization targets

Gibbs optimization

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

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

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

Expected population risk

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

10 thms2 active usersReviewed

Convex Optimization Functional Analysis Machine Learning+1·Captain: mikedeng1

Kernel Distributionally Robust Optimization: Generalized Duality Theorem and Stochastic Approximation: The Worst-Case Risk over an RKHS Ambiguity Set Equals Its Support-Function DualResearch Paper

Motivation

Distributionally robust optimization (DRO) chooses a decision $\theta$ that minimizes the expected loss under the worst distribution in an ambiguity set $\mathcal K$ of plausible distributions, $\min_\theta\sup_{P\in\mathcal K}\int l(\theta,\xi)\,dP(\xi)$ . It sits between stochastic optimization, which trusts a single distribution, and worst-case robust optimization, which trusts none. The inner supremum is a problem of moments, studied since Stieltjes and made computable by duality (Isii 1962; Shapiro 2001; Bertsimas and Popescu 2005). Existing tractable reformulations require the ambiguity set to be described by finitely many moments, a $\phi$ -divergence or a Wasserstein ball, and they usually require a structural property of the loss: affine or quadratic form, or a known Lipschitz constant.

Zhu, Jitkrittum, Diehl and Schölkopf (AISTATS 2021; arXiv:2006.06981) describe the ambiguity set through kernel mean embeddings: a distribution is represented by its mean in a reproducing kernel Hilbert space, and the ambiguity set is the set of distributions whose embedding lies in a convex set $\mathcal C$ of that space. Moment sets, MMD balls, scenario polytopes and the whole space (worst-case RO) all arise for suitable kernels and sets $\mathcal C$ . Their Generalized Duality Theorem (Theorem 3.1) turns the inner worst-case problem into a minimization over a function of the RKHS that majorizes the loss, with no assumption on the loss beyond upper semicontinuity.

Setting

Let $\mathcal X$ be a compact metric space (in the paper, a compact $\mathcal X\subset\mathbb R^d$ ) with its Borel $\sigma$ -algebra, and $\mathcal P$ the set of Borel probability measures on $\mathcal X$ . Let $\mathcal H$ be a real Hilbert space and $\varphi:\mathcal X\to\mathcal H$ a continuous feature map; $k(x,y)=\langle\varphi(x),\varphi(y)\rangle_{\mathcal H}$ is then a continuous positive definite kernel, and an element $f\in\mathcal H$ acts on $\mathcal X$ by the reproducing property $f(\xi)=\langle f,\varphi(\xi)\rangle_{\mathcal H}$ (rkhsEval).

The mean embedding of $P\in\mathcal P$ is $\mu_P=\int\varphi\,dP\in\mathcal H$ (meanEmbedding).
For $\mathcal C\subseteq\mathcal H$ , the ambiguity set is $\mathcal K_{\mathcal C}=\{P\in\mathcal P:\mu_P\in\mathcal C\}$ (ambiguitySet).
The support function of $\mathcal C$ is $\delta^*_{\mathcal C}(f)=\sup_{\mu\in\mathcal C}\langle f,\mu\rangle_{\mathcal H}\in[-\infty,\infty]$ (supportFun).
A loss is a function $l:\Theta\times\mathcal X\to[-\infty,\infty)$ , where $\Theta$ is an arbitrary set of decisions; $\int l\,dP$ is the extended-real expectation.

For fixed $\theta$ (written $l=l(\theta,\cdot)$ ), the primal inner problem (11) and the dual inner problem (12) are

\mathrm{(P)}_\theta=\sup_{P\in\mathcal K_{\mathcal C}}\int l\,dP,\qquad \mathrm{(D)}_\theta=\inf\Big\{f_0+\delta^*_{\mathcal C}(f):\ f_0\in\mathbb R,\ f\in\mathcal H,\ l(\xi)\le f_0+f(\xi)\ \forall\xi\in\mathcal X\Big\}

(primalValue, dualValue, with the constraint IsDualFeasible). Assumption 3.1 of the paper asks that each $l(\theta,\cdot)$ be proper (not identically $-\infty$ ) and upper semicontinuous, that $\mathcal C$ be closed and convex, and that $\mathrm{ri}(\mathcal K_{\mathcal C})\neq\emptyset$ .

The PDF prints no page numbers; every page cited in this mission is the PDF page of arXiv:2006.06981v3.

Formalization targets

Goal: Theorem 3.1 (Generalized Duality), p. 5

Under the hypotheses above, with $\mathcal K_{\mathcal C}\ne\emptyset$ ,

\forall\theta\in\Theta:\quad \sup_{P\in\mathcal K_{\mathcal C}}\int l(\theta,\xi)\,dP(\xi)=\inf_{\substack{f_0\in\mathbb R,\,f\in\mathcal H\\ l(\theta,\cdot)\le f_0+f}}f_0+\delta^*_{\mathcal C}(f),

and consequently $\mathrm{(P)}=\inf_\theta\mathrm{(P)}_\theta=\inf_\theta\mathrm{(D)}_\theta=\mathrm{(D)}$ , the equality of the Kernel DRO problem (2) and its dual (4).

Milestones (the proof of Proposition A.1, pp. 13–15, and Appendix D, pp. 22–23)

The reproducing identity $\int f\,dP=\langle f,\mu_P\rangle_{\mathcal H}$ (p. 13).
Lemma D.1: $\int(l-f_0-f)\,dP\le0$ for all $P$ iff $l\le f_0+f$ on $\mathcal X$ .
Weak duality: $\int l\,dP\le f_0+\delta^*_{\mathcal C}(f)$ for $P\in\mathcal K_{\mathcal C}$ and feasible $(f_0,f)$ (p. 6).
Lemmas D.2–D.4: $\mathcal T(\mathcal P)=\{\mu_P\}$ , $\mathcal C\cap\mathcal T(\mathcal P)$ and $\mathcal K_{\mathcal C}$ are compact.
Primal attainment (p. 15), via the upper semicontinuity of $P\mapsto\int l\,dP$ (a supporting lemma the paper uses without stating).
The separation (14), the sign $\tau<0$ with the rescaled dual feasible point, and $\mathrm{(D)}\le\mathrm{(P)}+\epsilon$ (p. 15).
Proposition A.1: $\mathrm{(P)}_\theta=\mathrm{(D)}_\theta$ (p. 13).

Companions

Lemma A.2 (complementarity (19)), Corollary 3.1.3 (the optimal majorant interpolates $l$ $P^*$ -a.e.), the support function $\frac1N\sum_i f(\xi_i)+\epsilon\|f\|_{\mathcal H}$ of the RKHS norm ball (Table 1), and the weak-duality content of Corollary 3.1.1 for integral probability metrics.

Significance

The theorem replaces an optimization over probability measures by a semi-infinite program over $(f_0,f)\in\mathbb R\times\mathcal H$ , whose objective is explicit for the common choices of $\mathcal C$ (Table 1). The majorant $f_0+f$ needs no Lipschitz constant and no parametric form of the loss, and the dual variable $f^*$ doubles as a witness function for the MMD. This is the basis of the paper's batch and stochastic functional gradient algorithms, and it places moment-based DRO, scenario optimization, MMD-ball DRO and worst-case RO in one framework.

The result is proved on paper; it has no machine-checked proof that we know of. Formalizing it builds the duality theory of moment problems with infinitely many moment constraints, on top of Mathlib's Hilbert spaces, Bochner integrals and the weak topology on probability measures. The formal statements also fix points the paper leaves loose: the infimum in place of the printed "min", the reading of the Slater condition, and the role of the continuity of the kernel.

Difficulty

Weak duality is a two-line computation. The work is strong duality. The paper's route separates the cone $A=\{(\int1\,dP,\int\varphi\,dP,\int l\,dP):P\in\mathrm{co}(\mathcal P)\}$ from $B_\epsilon=\{(1,\mu,t+\epsilon):\mu\in\mathcal C\}$ in $\mathbb R\times\mathcal H\times\mathbb R$ . A Hahn–Banach strict separation needs one set compact or the two at positive distance, and $A$ is neither obviously closed nor bounded. The step goes through only because $\mathcal K_{\mathcal C}$ is compact in the weak topology and $P\mapsto\int l\,dP$ is upper semicontinuous, which also gives primal attainment and the sign $\tau<0$ . The loss may take the value $-\infty$ , so every expectation lives in $[-\infty,\infty)$ . The infinite primal case also needs an argument of its own.

Formalization scope

$\mathcal X$ is a compact metric space with a Borel $\sigma$ -algebra; a compact subset of $\mathbb R^d$ is an instance. $\mathcal P$ is ProbabilityMeasure X with its topology of weak convergence; the paper's MMD topology agrees with it for a universal continuous kernel.
The RKHS is in feature-map form: a real Hilbert space $\mathcal H$ and a continuous $\varphi$ . Continuity of the kernel is not written in Assumption 3.1 but is used by Appendix D.
Losses are X → EReal, upper semicontinuous, never $+\infty$ , and not identically $-\infty$ . Expectations use the published definition WassersteinDRO.Duality.erealExpectation, which for such losses is the usual $\int l\,dP\in[-\infty,\infty)$ .
Support function, primal and dual values are extended reals. $\delta^*_\emptyset=-\infty$ ; $\delta^*_{\mathcal H}(f)=+\infty$ for $f\ne0$ ; an empty ambiguity set gives primal value $-\infty$ ; an infeasible dual gives $+\infty$ . The sum $f_0+\delta^*_{\mathcal C}(f)$ adds a real to an extended real, so $+\infty+(-\infty)$ never occurs.
The Slater clause $\mathrm{ri}(\mathcal K_{\mathcal C})\ne\emptyset$ names no topology on measures and is used only to obtain a primal solution (p. 15). It is read as $\mathcal K_{\mathcal C}\ne\emptyset$ , which it implies under any reading, so the formal goal is at least as strong as the paper's.
Every printed "min" is read as an infimum. Dual attainment is not proved and can fail: for $\mathcal X=[0,1]$ , $\varphi(x)=x$ , $\mathcal C=(-\infty,0]$ and $l(x)=\sqrt x$ , the dual infimum $0$ is not attained.
The dual variable ranges over $\mathcal H$ , never over arbitrary functions on $\mathcal X$ . Over all bounded functions, the choice $f=l$ would make the duality trivial (Example 3.3). The goal is also not closed by unfolding: for $\mathcal C=\mathcal H$ it says $\sup_P\int l\,dP=\sup_\xi l(\xi)$ , worst-case RO.
Corollary 3.1.2 (p. 6) is not stated: it is false under Assumption 3.1 alone (for $\mathcal C=\mathcal H$ and $l=\mathbf 1_{\{0\}}$ , (2) equals $1$ while (6) equals $0$ ).

Reusable pieces: the kernel mean embedding and its continuity on ProbabilityMeasure X, compactness of RKHS ambiguity sets, and the upper semicontinuity of $P\mapsto\int l\,dP$ for upper semicontinuous $l$ (a portmanteau-type fact not yet in Mathlib). Proofs of any milestone are welcome. So are support-function computations for the other rows of Tables 1 and 3.

Selected references

J.-J. Zhu, W. Jitkrittum, M. Diehl, B. Schölkopf, Kernel Distributionally Robust Optimization: Generalized Duality Theorem and Stochastic Approximation, AISTATS 2021 (PMLR 130); cited here as arXiv:2006.06981v3, 2021. https://arxiv.org/abs/2006.06981
A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, Kluwer, 2001. https://doi.org/10.1007/978-1-4757-3403-4_7
K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14, 1962. https://doi.org/10.1007/BF02868641
D. Bertsimas, I. Popescu, Optimal inequalities in probability theory: a convex optimization approach, SIAM Journal on Optimization 15(3), 2005. https://doi.org/10.1137/S1052623401399903
A. Gretton, K. Borgwardt, M. Rasch, B. Schölkopf, A. Smola, A kernel two-sample test, Journal of Machine Learning Research 13, 2012. https://jmlr.org/papers/v13/gretton12a.html
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050

15 thms2 active usersReviewed

Information Theory Machine Learning Statistics·Captain: mikedeng1

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

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1 (p. 4)

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

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

Selected references

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

7 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning·Captain: mikedeng1

A Tutorial on Thompson Sampling III: In the Known-Standard Problem, Every Stationary Deterministic Strategy Has Linearly Growing Expected Regret Under Some PriorResearch Paper

Why randomize actions

Thompson sampling (TS) selects each action by sampling a parameter from the current posterior and playing the action that is optimal for the sample. It is a stationary randomized strategy: the distribution of the action is a fixed function of the posterior, the same in every period, and the action is drawn at random from it. Its Bayesian regret bounds, surveyed in §8.1 of the tutorial by Russo, Van Roy, Kazerouni, Osband and Wen (Found. Trends Mach. Learn. 11(1), 2018), grow sublinearly in the horizon $T$ .

A natural question is whether the randomization is essential. A strategy that maps the posterior to an action deterministically, for example "play the action with the highest posterior mean", is equally stationary and conceptually simpler. §8.1.3 of the tutorial answers the question with Example 8.1 (A Known Standard), taken from Russo and Van Roy, Learning to optimize via information-directed sampling (Operations Research 66(1), 2018): in a two-action problem with a known baseline action, every stationary deterministic strategy suffers linearly growing expected regret under some prior. The example is the standard justification for why posterior sampling, and not a deterministic function of the posterior, is the right stationary rule.

Setting

There are two actions $\mathcal X=\{1,2\}$ and a binary unknown parameter $\theta\in\{0,1\}$ with prior

\theta\sim\mathrm{Bernoulli}(p_0),\qquad \mathbb P(\theta=1)=p_0 .

In each period $t=1,2,\dots$ the agent selects an action $x_t$ and observes a binary reward $r_t$ . Rewards are conditionally independent across periods given $\theta$ and the actions:

action $1$ (the known standard) pays $\mathrm{Bernoulli}(1/2)$ , whatever $\theta$ is;
action $2$ pays $\mathrm{Bernoulli}(3/4)$ if $\theta=1$ and $\mathrm{Bernoulli}(1/4)$ if $\theta=0$ .

The mean reward $\mu(x,\theta)$ of action $x$ is its success probability, and the optimal action $x^*$ is action $2$ if $\theta=1$ and action $1$ if $\theta=0$ , so $\mu(x^*,\theta)=3/4$ or $1/2$ .

The history $\mathbb H_t$ lists the actions and rewards of the first $t$ periods. The posterior $p_t=\mathbb P(\theta=1\mid\mathbb H_t)$ is given by Bayes' rule (4.2) of the tutorial, applied period by period:

p_t=\frac{p_0\,L_1(\mathbb H_t)}{p_0\,L_1(\mathbb H_t)+(1-p_0)\,L_0(\mathbb H_t)},\qquad L_\theta(\mathbb H_t)=\prod_{s=1}^{t}\mathbb P_\theta(r_s\mid x_s),

with $p_0$ the prior on the empty history.

A stationary deterministic strategy is one function $f$ from posterior probabilities to actions, used in every period: $x_t=f(p_{t-1})$ . The expected cumulative regret (Bayesian regret, p. 71) of running $f$ from the prior $p_0$ for $T$ periods is

\mathbb E[\mathrm{Regret}(T)]=\mathbb E\Big[\sum_{t=1}^T\big(\mu(x^*,\theta)-\mu(x_t,\theta)\big)\Big],

the expectation taken over $\theta$ and the rewards. The Lean development names these objects succProb ( $\mu$ ), optMean ( $\mu(x^*,\cdot)$ ), post ( $p_t$ ), Strategy ( $f$ ), lawGiven (the probability of a history given $\theta$ ) and expRegret.

Formalization targets

Goal: some prior forces linear regret

\forall f\ \ \exists\,p_0\in(0,1]\ \ \exists\,c>0\ \ \forall T\in\mathbb N:\qquad \mathbb E_{p_0}[\mathrm{Regret}(T)]\ \ge\ c\,T .

This is the sentence "for any deterministic stationary strategy, there exists a prior probability $p_0$ such that expected cumulative regret grows linearly with time" (p. 79). The prior is chosen after the strategy. No constant is fixed; only the linear shape is asserted.

Milestones: the two cases of the example

$x_1=1$ for some $p_0>0$ . If $f(p_0)=1$ for some $p_0\in(0,1]$ , then on every history of positive probability $p_t=p_0$ and $x_t=1$ for all $t$ , and

\mathbb E_{p_0}[\mathrm{Regret}(T)]=\tfrac{p_0}{4}\,T .

$x_1=2$ for all $p_0>0$ . If $f(p)=2$ for every $p\in(0,1]$ , then for every $p_0\in(0,1]$ , on every history of positive probability $x_t=2$ for all $t$ , and

\mathbb E_{p_0}[\mathrm{Regret}(T)]=\tfrac{1-p_0}{4}\,T .

Significance

The example separates two properties that regret analyses often conflate: being a function of the posterior alone (stationarity) and achieving sublinear Bayesian regret. It shows that a stationary strategy with sublinear regret on all priors must randomize, which is the structural reason TS samples rather than maximizes. It also explains why deterministic algorithms with good regret, such as upper confidence bound methods, are necessarily nonstationary: their confidence radii depend on the period and on counts, not only on the posterior.

The tutorial gives the argument in one paragraph. A formal version makes precise what is left implicit there: that the posterior is the actual conditional probability computed from the history, that "uninformative" means the posterior is invariant under action $1$ , and that under action $2$ the posterior never leaves $(0,1]$ . The result is a closed-form regret identity in each case, not only an asymptotic statement. As far as is known, neither the example nor its source in Russo and Van Roy (2018) has been machine-checked.

Difficulty

The mathematics is elementary; the work lies in the bookkeeping of a history-dependent strategy. The strategy's action in period $t$ depends on the whole history through $p_{t-1}$ , so the law of $\mathbb H_T$ is a product of indicator factors, each evaluating $f$ at a posterior computed from a prefix of the same history. A direct computation of the regret must show that every history of positive probability follows a single action path, and that is a statement about the posterior along every prefix, not only at the first period. A first attempt that defines the posterior by a recursion in which "the posterior stays at $p_0$ " is built in proves nothing about the example; the posterior must be Bayes' rule applied to the history.

Formalization scope

Paper action $1$ is 0 : Fin 2, action $2$ is 1 : Fin 2; $\theta=1$ is true; a reward of $1$ is true. Lean period s : Fin T is the paper's period $s+1$ .
Histories are Fin t → Fin 2 × Bool; every probability and expectation is a finite sum, so no measure theory is needed.
The posterior post is the closed form of iterated Bayes' rule (4.2). The probabilities with which the strategy picks its actions are $0$ or $1$ and do not depend on $\theta$ ; on histories of positive probability they cancel, so post is the true conditional probability there. For $0<p_0\le1$ its denominator is positive, so Lean's convention $x/0=0$ is never used.
A strategy is a function ℝ → Fin 2; its values outside $[0,1]$ are never used. The same function acts in every period, which is what "stationary" means.
The prior ranges over $p_0\in(0,1]$ : the text requires $p_0>0$ , and $p_0\le1$ because it is a probability.
"Grows linearly with time" is read as a lower bound $cT$ with $c>0$ for all $T$ . The constant $c>0$ is part of the claim; $c=0$ would make the goal trivial. The quantifiers are in the order of the text, every strategy first and then a prior; the reverse order (one prior for all strategies) is a different statement that the tutorial does not claim.
Contributions welcome: proofs of the two milestones and of the goal from them, and lemmas on the posterior (invariance under an uninformative action, positivity) that are reusable for other Bayesian bandit examples.

The tutorial's argument for the example is on p. 79; the tutorial attributes the example to Russo and Van Roy (2018).

Selected references

D. J. Russo, B. Van Roy, A. Kazerouni, I. Osband, Z. Wen, A Tutorial on Thompson Sampling, Foundations and Trends in Machine Learning 11(1):1–96, 2018. https://doi.org/10.1561/2200000070 (Example 8.1, p. 79; Bayes' rule (4.2), p. 19; Bayesian regret, p. 71)
D. Russo, B. Van Roy, Learning to Optimize via Information-Directed Sampling, Operations Research 66(1):230–252, 2018. https://doi.org/10.1287/opre.2017.1663 (arXiv: https://arxiv.org/abs/1403.5556)
D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4):1221–1243, 2014. https://doi.org/10.1287/moor.2014.0650
W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25(3/4):285–294, 1933. https://doi.org/10.2307/2332286

4 thms2 active usersReviewed

Bandit Algorithms Information Theory Machine Learning·Captain: mikedeng1

A Tutorial on Thompson Sampling I: Any Algorithm Whose Information Ratio Is at Most Γ̄ Has Expected Regret at Most √(Γ̄·H(x*)·T)Research Paper

Motivation

Thompson sampling (TS) chooses each action with the posterior probability that it is optimal. Its practical success in online advertising, recommendation and experimentation raised the question of why it works and when it does not. The tutorial of Russo, Van Roy, Kazerouni, Osband and Wen (Found. Trends Mach. Learn. 11(1), 2018) answers part of that question in §8.1 with an information-theoretic regret bound due to Russo and Van Roy (JMLR 17, 2016). The bound applies to every algorithm, not only TS. It reduces the analysis of a particular algorithm to one quantity, the information ratio: the squared expected regret of a period divided by the information the period yields about the optimal action.

Timeline:

2016: Russo and Van Roy, An information-theoretic analysis of Thompson sampling (JMLR 17), introduce the information ratio with the regret and the mutual information both conditioned on a realised history, and prove the regret bound and bounds on the ratio for TS (for example $|\mathcal X|/2$ for $|\mathcal X|$ -armed bandits and $d/2$ for linear bandits).
2018: Russo and Van Roy, Learning to optimize via information-directed sampling (Oper. Res. 66), design algorithms that minimise the information ratio directly.
2018: Russo and Van Roy, Satisficing in time-sensitive bandit learning (arXiv:1803.02855), observe that the same bounds hold with the information ratio averaged over histories. This is the form (8.7) the tutorial uses (footnote 1, p. 75).
2018: the tutorial gives the bound as (8.8), with a three-line proof on p. 76 whose last step is cited from the 2016 paper.

Setting

An agent acts in periods $t=1,2,\dots$ . In each period it selects an action $x_t$ from a finite set $\mathcal X$ and observes an outcome $y_t$ from a finite set $\mathcal Y$ . An unknown parameter $\theta$ , taking values in a measurable space $\Theta$ , has a prior distribution $P$ . Given $\theta$ and the action $x$ , the outcome is drawn from a probability vector $q_\theta(\cdot\mid x)$ that depends measurably on $\theta$ . The agent receives the reward $r(y_t)$ for a known function $r$ . The mean reward of action $x$ is

\mu(x,\theta)=\sum_{y}q_\theta(y\mid x)\,r(y),

and the optimal action $x^*=x^*(\theta)$ is a measurable selector of $\arg\max_x\mu(x,\theta)$ . Ties may be broken in any measurable way, and every result holds for every selector.

The history $\mathbb H_t$ is the list $(x_1,y_1),\dots,(x_t,y_t)$ . An algorithm $\pi$ assigns to every history a probability vector over $\mathcal X$ , from which the next action is drawn. The joint law of $(\theta,\mathbb H_t)$ is $P(d\theta)\prod_{s\le t}\pi(x_s\mid\mathbb H_{s-1})\,q_\theta(y_s\mid x_s)$ , and every expectation below is taken under it. The expected cumulative regret, or Bayesian regret, is

\mathbb E[\mathrm{Regret}(T)]=\mathbb E\Big[\sum_{t=1}^T\big(\mu(x^*,\theta)-\mu(x_t,\theta)\big)\Big].

The entropy of the prior distribution of $x^*$ is $H(x^*)=-\sum_a\mathbb P(x^*=a)\log\mathbb P(x^*=a)$ . The conditional mutual information $I(x^*;(x_t,y_t)\mid\mathbb H_{t-1})$ is the expected information that the period- $t$ observation carries about $x^*$ given the past, averaged over the past. The information ratio of period $t$ is (8.7):

\Gamma_t=\frac{\big(\mathbb E[\mu(x^*,\theta)-\mu(x_t,\theta)]\big)^2}{I(x^*;(x_t,y_t)\mid\mathbb H_{t-1})}.

Formalization targets

Goal: (8.8)

For every model and every algorithm, every horizon $T$ and every $\bar\Gamma\ge0$ with $\big(\mathbb E[\mu(x^*,\theta)-\mu(x_t,\theta)]\big)^2\le\bar\Gamma\,I(x^*;(x_t,y_t)\mid\mathbb H_{t-1})$ for $t=1,\dots,T$ ,

\mathbb E[\mathrm{Regret}(T)]\le\sqrt{\bar\Gamma\,H(x^*)\,T}.

When every mutual information is positive, the least such $\bar\Gamma$ is $\max_{t\le T}\Gamma_t$ , which is the tutorial's $\bar\Gamma$ . A companion theorem states that literal form under the positivity hypothesis.

Milestones, in the order of the p. 76 proof

Regret is additive over periods:

\mathbb E[\mathrm{Regret}(T)]=\sum_{t=1}^T\mathbb E[\mu(x^*,\theta)-\mu(x_t,\theta)].

The Jensen (Cauchy–Schwarz) step: if $\delta_t^2\le\bar\Gamma I_t$ for every $t$ and $\sum_tI_t\le H$ , then $\sum_t\delta_t\le\sqrt{T\bar\Gamma H}$ . This milestone is the published, proved theorem BanditAlgorithm.information_ratio_cumulative_bound_signed. It states the step in the form the proof uses, with the entropy budget as a hypothesis.
The entropy budget:

\sum_{t=1}^T I\big(x^*;(x_t,y_t)\mid\mathbb H_{t-1}\big)\le H(x^*).

Significance

The result. (8.8) separates the regret analysis of an algorithm into two independent problems. One is a per-period bound on the information ratio, which depends on the structure of the problem and the algorithm. The other is the entropy of the optimal action, which depends only on the prior. Combined with the bound $\bar\Gamma\le|\mathcal X|/2$ that Russo and Van Roy (2016) prove for TS on $|\mathcal X|$ -armed bandits, and with $H(x^*)\le\log|\mathcal X|$ , it gives $\sqrt{|\mathcal X|\,T\log|\mathcal X|/2}$ . On the shortest-path problem of p. 76, $\bar\Gamma\le d/2$ makes the regret depend on the number $d$ of edges and on $H(x^*)$ , not on the exponentially large number of paths. The same inequality is the design criterion of information-directed sampling, which chooses actions to minimise the ratio.

Formalizing it. The bound and its proof are known. The work here is to make the probabilistic model explicit, with a general parameter space, an outcome kernel and randomized algorithms; to formalize the per-period decomposition of the regret and the chain-rule argument behind the entropy budget, which the tutorial cites rather than proves; and to obtain (8.8) for every algorithm in one statement. The Proved platform results for Lattimore and Szepesvári's Bayesian adversarial bandit (Theorem 36.5 and its chain-rule lemmas) are about a different model: one algorithm (TS), the best arm in hindsight of a reward matrix, and the budget $\log k$ . To our knowledge, (8.8) itself has not been formalized.

Difficulty

The Cauchy–Schwarz step is elementary and already proved on the platform. Milestone 1 is bookkeeping: the cumulative regret integrates over histories of length $T$ , while the period- $t$ term integrates over histories of length $t$ , and later periods must be integrated out.

The substance is the entropy budget. The obvious attempt bounds each period's information by $H(x^*)$ , which loses a factor $T$ . The bound is uniform in $T$ only because the per-period informations telescope: their sum is the information that the whole history carries about $x^*$ , which is at most the entropy of $x^*$ . Each step requires conditional distributions of $x^*$ given histories, where $\theta$ lives in a general measurable space and is integrated against the prior. Zero-probability histories must also be handled consistently with the convention $0\log0=0$ .

Formalization scope

$\mathcal X$ and $\mathcal Y$ are finite types; $\Theta$ is an arbitrary measurable space with a probability measure $P$ . The tutorial allows infinite action sets and general outcomes. The finite specialization makes $H(x^*)$ and every mutual information a finite sum. The kernel $q_\theta(\cdot\mid x)$ of §4 replaces the noise representation $y_t=g(x_t,\theta,w_t)$ of p. 70; both describe the same laws.
Standing hypotheses: $q_\theta(y\mid x)\ge0$ , $\sum_yq_\theta(y\mid x)=1$ , measurability of $\theta\mapsto q_\theta(y\mid x)$ , measurability of the level sets of $x^*$ , and $\mu(x,\theta)\le\mu(x^*(\theta),\theta)$ . They make every integrand bounded and measurable, so no integrability hypothesis is added.
An algorithm is a behavioural policy, giving a probability vector over actions for each history. Under perfect recall this is equivalent to an algorithm with internal randomization. Periods are 0-based in Lean: Lean period $s$ is tutorial period $t=s+1$ .
Logarithms are natural in both $I$ and $H$ . The conditional mutual information is defined directly as an average of Kullback–Leibler divergences, with joint probabilities. It is not defined as a difference of unconditional mutual informations: that would make the chain rule true by definition and empty milestone 3. $\Gamma_t$ is never written as a quotient in the goal, so a period with zero information cannot turn the bound into one with $\bar\Gamma=0$ .
Needed infrastructure: marginalisation over later periods of the history law, the chain rule of conditional mutual information for finite variables averaged against a general prior, and $I(x^*;\mathbb H_T)\le H(x^*)$ . The Proved platform results InformationTheory.kernel_average_categorical_kl_le_marginal_entropy and its _general variant (average KL to the mixture is at most the mixture's entropy), and the adversarial-bandit lemmas BanditAlgorithm.bayesian_ts_conditional_information_gain_chain_rule and bayesian_history_mutualInformation_endpoint_bound, are related tools. A chain-rule library for this history model would be reusable beyond this mission, for example for information-directed sampling. Proofs of auxiliary lemmas are welcome.

The tutorial's argument is on pp. 75–76. The tutorial cites Russo and Van Roy (2016) for the original results, including the entropy budget.

Selected references

D. J. Russo, B. Van Roy, A. Kazerouni, I. Osband, Z. Wen, A Tutorial on Thompson Sampling, Foundations and Trends in Machine Learning 11(1):1–96, 2018. https://doi.org/10.1561/2200000070
D. Russo, B. Van Roy, An Information-Theoretic Analysis of Thompson Sampling, Journal of Machine Learning Research 17(68):1–30, 2016. https://jmlr.org/papers/v17/14-087.html (arXiv: https://arxiv.org/abs/1403.5341)
D. Russo, B. Van Roy, Learning to Optimize via Information-Directed Sampling, Operations Research 66(1):230–252, 2018. https://doi.org/10.1287/opre.2017.1663
D. Russo, B. Van Roy, Satisficing in Time-Sensitive Bandit Learning, arXiv preprint, 2018. https://arxiv.org/abs/1803.02855
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 36. https://doi.org/10.1017/9781108571401

5 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models: C(π_r∞)/OPT(L) ≤ 1 + h((1−γ)g)⁻¹(E[D] − r∞ + (eϑ(L+1))⁻¹)γ^{L+1} for Every Lead Time L ≥ 1Research Paper

Why lost-sales inventory with lead times matters

In many retail and spare-parts settings, demand that cannot be met from stock is lost rather than backlogged, and replenishment orders arrive only after a positive lead time. The resulting lost-sales inventory model is a basic model of inventory theory. Its optimal policy depends on the whole pipeline of outstanding orders, so dynamic programming over that state becomes intractable as the lead time grows. This is why the model is often replaced by its backlogged counterpart, even when that approximation is poor (Bijvank and Vis, 2011).

Simple heuristics are therefore of practical interest. The simplest is the constant-order policy, which orders the same amount in every period regardless of the state. Reiman (2004, unpublished manuscript) showed that the best constant-order policy sometimes outperforms the base-stock policy, and Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante (arXiv:1211.4063, Math. Oper. Res. 2016) proved that it is asymptotically optimal as the lead time grows, with a gap that decays polynomially in the lead time. Xin and Goldberg (arXiv:1409.1499v2, Oper. Res. 2016) proved that for the infinite-horizon average-cost problem the gap actually decays exponentially, with an explicit rate and explicit constants. This mission formalizes that result.

Timeline:

1958: Karlin and Scarf introduce the lost-sales model with a positive lead time; convexity results follow in Karlin and Scarf (1958) and Morton (1969).
1962: Kingman bounds how fast the expected waiting time of an initially empty GI/G/1 queue approaches its steady-state value (doi).
2004: Reiman finds that the best constant-order policy can outperform the base-stock policy.
2009: Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 55(3)) prove base-stock policies asymptotically optimal as the lost-sales penalty grows.
2011: Huh, Janakiraman and Nagarajan (Operations Research 59(1)) give the existence of stationary optimal policies used by the paper.
2015–2016: Goldberg et al. prove asymptotic optimality of constant-order policies as the lead time grows; Xin and Goldberg prove exponential decay of the gap.

The setting

Demands $D_1,D_2,\dots$ are i.i.d. copies of a nonnegative random variable $D$ with law $\mathcal D$ , finite mean $\mathbb E[D]$ and strictly positive variance. The lead time $L\ge1$ is an integer, $h>0$ is the unit holding cost and $p>0$ the unit lost-sales penalty. At the start of period $t$ there is on-hand inventory $I_t$ and a pipeline $\mathbf x_t=(x_{1,t},\dots,x_{L,t})$ of orders placed but not yet delivered. In each period, $x_{1,t}$ arrives, a new order is placed (it enters the end of the pipeline), demand $D_t$ is realized, and the period cost

C_t=h\,(I_t+x_{1,t}-D_t)^++p\,(I_t+x_{1,t}-D_t)^-

is incurred; then $I_{t+1}=(I_t+x_{1,t}-D_t)^+$ . The system starts empty. A policy $\pi$ chooses orders from the information available, and its long-run average cost is $C(\pi)=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$ . The optimal cost is $\mathrm{OPT}(L)=\inf_\pi C(\pi)$ .

The constant-order policy $\pi_r$ orders $r$ in every period. Its cost is governed by the random walk $jr-\sum_{i=1}^jD_i$ through

I^r_\infty=\sup_{j\ge0}\Big(jr-\sum_{i=1}^jD_i\Big),\qquad I^r_L=\max_{j=0,\dots,L}\Big(jr-\sum_{i=1}^jD_i\Big),

the steady-state and $L$ -th waiting times of a single-server queue with interarrival law $\mathcal D$ and constant service time $r$ . The best constant order $r_\infty$ is the least minimizer of $C(\pi_r)$ over $0\le r\le\mathbb E[D]$ . The rate and constants are

\gamma=\inf_{\theta\ge0}e^{\theta r_\infty}\mathbb E[e^{-\theta D}],\qquad g=\inf_{x\in\mathbb R}\mathbb E\big[h(x-D)^++p(x-D)^-\big],

with $\vartheta$ the largest minimizer in the definition of $\gamma$ ( $\vartheta=\infty$ if the infimum is not attained, and $1/\infty=0$ ).

Formalization targets

Goal: Theorem 1 (p. 8)

\frac{C(\pi_{r_\infty})}{\mathrm{OPT}(L)}\le1+h\big((1-\gamma)g\big)^{-1}\Big(\mathbb E[D]-r_\infty+\big(e\vartheta(L+1)\big)^{-1}\Big)\gamma^{L+1}\qquad\text{for all }L\ge1 .

The quantities $r_\infty,\gamma,\vartheta,g$ depend on $\mathcal D,h,p$ but not on $L$ .

Milestones, in the order the proof uses them

Eq. (3): $C(\pi_r)=h\,\mathbb E[I^r_\infty]+p\,\mathbb E[D]-pr$ for $r\in[0,\mathbb E[D])$ .
Sec. 2.2: the best constant exists and $r_\infty<\mathbb E[D]$ ; Sec. 2.3: $\vartheta>0$ , $\gamma\in[0,1)$ , $g>0$ and $\mathrm{OPT}(L)\ge g$ .
Observation 1 (convexity of $\mathfrak f_{\mathbf d}$ and a Jensen bound) and Lemma 2: $\mathrm{OPT}(L)\ge C_L(r_L)$ and the decomposition (5) of $C(\pi_{r_\infty})-\mathrm{OPT}(L)$ .
Lemma 3 (Kingman's series and the tail bound), Lemma 4 ( $r_\infty\le r_L$ ), Lemma 5 ( $\sum_n\mathbb P(nr_\infty\ge\sum_{i\le n}D_i)\ge p/h$ ), the Chernoff step $\mathbb P(nr_\infty\ge\sum_{i\le n}D_i)\le\gamma^n$ , and the bound on the term (6).
Further: Lemma 1 (monotonicity of $\gamma$ in $p/h$ ) and Corollary 1 (the closed form for exponential demand).

Significance

The theorem shows that a lead time of order $\log(\epsilon^{-1})$ suffices for the constant-order policy to be within a factor $1+\epsilon$ of optimal, whereas the earlier bounds of Goldberg et al. needed a lead time polynomial in $\epsilon^{-1}$ . The constants are explicit and computable from the demand law: for exponential demand with $p=h$ and $L=1$ the bound is already about $3.36$ , and it approaches $1$ quickly as $L$ grows (Table 1 of the paper). Lemma 1 adds that the rate $\gamma$ worsens as $p/h$ grows, the regime opposite to the one in which base-stock policies are known to be nearly optimal.

The result is proved on paper; no machine-checked proof is known to exist. A formalization would produce a checked infinite-horizon lost-sales model and a checked statement of Kingman's random-walk identities for this queue. It would also produce checked comparisons of an arbitrary history-dependent policy with constant-order policies through convexity. The statement here is taken over a policy class at least as large as the paper's, so a proof also extends the result to randomized history-dependent policies.

Difficulty

The cost of the constant-order policy is the expected supremum of a random walk, while the optimal policy has no closed form and may not even induce a stationary distribution. The paper avoids the steady state of the optimal policy by constructing a random vector with the needed stationarity properties (Theorem 2). That construction is not part of this mission. Here, the lower bound on $\mathrm{OPT}(L)$ in Lemma 2 instead goes through the published, proved lower certificate for the full policy class. The second obstacle is quantitative: the exponential rate comes from comparing the minimizers $r_\infty$ and $r_L$ of two different convex functions (Lemma 4) and from a first-order optimality condition involving a non-differentiable expectation (Lemma 5). Neither follows from the observation that one function dominates the other.

Formalization scope

The model is the published CappedBaseStock model: zero-based time, an empty initial state, demand laws on $[0,\infty)$ with finite positive mean, and costs and long-run averages in $[0,\infty]$ . $\mathrm{OPT}(L)$ is the infimum over all measurable, history-dependent, possibly randomized policies. That class contains the paper's Markov deterministic class $\Pi$ , so every statement involving $\mathrm{OPT}(L)$ is at least as strong as printed. "Strictly positive variance" is encoded as "the demand law is not a point mass". It is a hypothesis wherever the paper's argument needs it; the Chernoff step, eq. (3) and Corollary 1 do not need it.

$C(\pi_r)$ is the model's long-run cost of the constant policy, not formula (3), and $\mathbb E[I^r_\infty]$ is a lower integral in $[0,\infty]$ , so that eq. (3) and Lemma 3 are not true by definition. $r_\infty$ and $r_L$ are infima of the argmin sets, whose nonemptiness is a milestone. $1/\vartheta$ is encoded with the paper's convention $1/\infty=0$ . Lemma 3's tail bound is stated additively in $[0,\infty]$ , and the series in Lemmas 3 and 5 are extended-real series indexed from $0$ . The goal's ratio is taken in $[0,\infty]$ , where $x/0=\infty$ for $x\neq0$ . None of $\gamma<1$ , $g>0$ or $r_\infty<\mathbb E[D]$ is assumed: all three are milestones. A formalization that defines $\mathrm{OPT}$ over constant-order policies only, fixes $r$ instead of $r_\infty$ , treats $\gamma,\vartheta,g$ as free parameters, or takes the ratio in $\mathbb R$ after truncating infinite costs would make the goal trivial and is ruled out. The objects are defined from the full parameter record, which includes $L$ . That they do not depend on $L$ follows from eq. (3) and the existence milestone.

No statement corrects a printed slip. Theorem 2 (existence of the stationary vector) and eq. (2) (bounded stationary optimal policies) are not stated; Observation 1 instead takes Theorem 2's properties (i)–(iii) as hypotheses on an arbitrary law. The source is arXiv:1409.1499v2, whose printed page numbers equal the PDF's. Useful infrastructure: Lindley-type random-walk suprema, Spitzer–Kingman identities, Chernoff bounds for i.i.d. sums (Mathlib's measure_le_le_exp_mul_mgf), and Cesàro limits of expected costs. All of it is reusable for other queueing and inventory missions. Proofs of any milestone are welcome, and the Chernoff step is the natural entry point.

Selected references

L. Xin, D. A. Goldberg, Optimality gap of constant-order policies decays exponentially in the lead time for lost sales models, Operations Research 64(6), 2016; preprint arXiv:1409.1499v2. https://arxiv.org/abs/1409.1499v2
D. A. Goldberg, D. A. Katz-Rogozhnikov, Y. Lu, M. Sharma, M. S. Squillante, Asymptotic optimality of constant-order policies for lost sales inventory models with large lead times, Mathematics of Operations Research, 2016; preprint arXiv:1211.4063. https://arxiv.org/abs/1211.4063
J. F. C. Kingman, Some inequalities for the queue GI/G/1, Biometrika 49, 1962. https://doi.org/10.1093/biomet/49.3-4.315
M. Bijvank, I. F. A. Vis, Lost-sales inventory theory: a review, European Journal of Operational Research 215(1), 2011. https://doi.org/10.1016/j.ejor.2011.02.004
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236

19 thms2 active usersReviewed

Operations Research Optimal Transport Optimization·Captain: mikedeng1

Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes 4: A Worst-Case Distribution Is the Law of X + √δ G A(X)⁻¹β, Spending the Whole Budget δResearch Paper

Why the worst case matters

Distributionally robust optimization (DRO) replaces the expected loss $E_{P_0}[\ell(\beta^{\mathsf T}X)]$ of a linear decision rule $\beta$ by its worst case over all data laws $P$ within transport distance $\delta$ of the baseline $P_0$ . When $P_0$ is an empirical distribution this covers regularized regression and classification (Blanchet, Kang, Murthy 2019; Esfahani, Kuhn 2018). The optimal value is one number; a practitioner also wants to know which distribution realizes it, the adversary's best response. It shows which data points the robust model guards against, it gives stress-test scenarios, and its structure is what the paper's comparative statics (Theorem 7) and iterative schemes build on.

J. Blanchet, K. Murthy and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes (arXiv:1810.02403v3; Math. Oper. Res. 47(2), 2022), answer this for a state-dependent Mahalanobis cost. Theorem 6 of that paper describes the worst-case distribution through the solution of the one-dimensional dual problem. This mission formalizes Theorem 6.

Setting

The data $X$ take values in $\mathbb R^d$ with law $P_0$ , a Borel probability measure. The decision $\beta$ ranges over a convex set $B\subseteq\mathbb R^d$ (a standing assumption of the paper). Moving mass from $x$ to $x'$ costs

c(x,x')=(x-x')^{\mathsf T}A(x)(x-x'),

where $A(x)$ is positive definite. Assumption 1 asks that $c$ be lower semicontinuous and that $\rho_{\min}\|v\|^2\le v^{\mathsf T}A(x)v\le\rho_{\max}\|v\|^2$ for $P_0$ -almost every $x$ , with $\rho_{\min}>0$ . The optimal transport cost $D_c(P_0,P)$ is the least value of $E_\pi[c(X,X')]$ over couplings $\pi$ of $P_0$ and $P$ . For $\delta>0$ the worst-case objective is

\sup_{P:\,D_c(P_0,P)\le\delta}E_P\bigl[\ell(\beta^{\mathsf T}X)\bigr].\tag{6}

Assumption 2 asks that the loss $\ell:\mathbb R\to\mathbb R$ be convex, that the growth exponent $\kappa=\inf\{s\ge0:\sup_u(\ell(u)-su^2)<\infty\}$ be finite, and that $E_{P_0}\|X\|^4<\infty$ .

The dual side is built from

F(\gamma,\beta,\lambda;x)=\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,\beta^{\mathsf T}A(x)^{-1}\beta\bigr)-\lambda\sqrt\delta\bigl(\gamma^2\beta^{\mathsf T}A(x)^{-1}\beta-1\bigr),

the robust loss $\ell_{\rm rob}(\beta,\lambda;x)=\sup_{\gamma}F$ , the dual objective $f_\delta(\beta,\lambda)=E_{P_0}[\ell_{\rm rob}(\beta,\lambda;X)]\in\mathbb R\cup\{\infty\}$ and the maximizer set $\Gamma^*(\beta,\lambda;x)=\arg\max_\gamma F(\gamma,\beta,\lambda;x)$ . By the paper's Theorem 1, (6) equals $\inf_{\lambda\ge0}f_\delta(\beta,\lambda)$ , and a minimizer $\lambda_*(\beta)$ , the dual optimizer, exists. The threshold is $\lambda_{thr}(\beta)=\kappa\sqrt\delta\,\mathrm{ess\,sup}_{P_0}\,\beta^{\mathsf T}A(X)^{-1}\beta$ ; below it $f_\delta=\infty$ .

Formalization targets

Goal: Theorem 6(c)

Let $\beta\ne0$ and $\lambda_*(\beta)>\lambda_{thr}(\beta)$ . Let $G_\pm(x)\in\Gamma^*(\beta,\lambda_*(\beta);x)$ be measurable selections with the largest and smallest square, $\bar c=E[G_+^2\beta^{\mathsf T}A(X)^{-1}\beta]$ , $\underline c=E[G_-^2\beta^{\mathsf T}A(X)^{-1}\beta]$ , and let $Z\sim\mathrm{Bernoulli}(q)$ be independent of $X$ with $q=(\bar c-1)/(\bar c-\underline c)\in[0,1]$ . Then

X^*=X+\sqrt\delta\,\bigl(ZG_-+(1-Z)G_+\bigr)A(X)^{-1}\beta,\qquad E[c(X,X^*)]=\delta,

and the law of $X^*$ attains the supremum in (6).

Milestones

Lemma 1: $\Gamma^*\ne\emptyset$ and $\ell_{\rm rob}<\infty$ when $\lambda>\kappa\sqrt\delta\,\beta^{\mathsf T}A(x)^{-1}\beta$ , and $\ell_{\rm rob}=\infty$ below that; hence $\{\lambda>\lambda_{thr}\}\subseteq\{f_\delta<\infty\}\subseteq\{\lambda\ge\lambda_{thr}\}$ .
Lemma 3(a): $\sqrt\delta|g|\beta^{\mathsf T}A(x)^{-1}\beta\le1+C_1\varepsilon^{-1}(1+|\beta^{\mathsf T}x|)$ for $g\in\Gamma^*$ once $\lambda\ge(\kappa+\varepsilon)\sqrt\delta\beta^{\mathsf T}A(x)^{-1}\beta$ .
Proposition 2 (a) and its $\lambda$ -part: the one-sided $\lambda$ -derivatives of $\ell_{\rm rob}$ are the minimum and the maximum of $-\sqrt\delta(\gamma^2\beta^{\mathsf T}A(x)^{-1}\beta-1)$ over $\Gamma^*$ .
The one-sided $\lambda$ -derivatives of $f_\delta$ on $\{\lambda>\lambda_{thr}\}$ :

\partial_\pm f_\delta/\partial\lambda=\sqrt\delta\bigl(1-E[\beta^{\mathsf T}A(X)^{-1}\beta\,\inf/\sup_{g\in\Gamma^*}g^2]\bigr).

[Blanchet–Murthy 2019, Theorem 1]: strong duality and complementary slackness (already proved on the platform).

Companion statements

Theorem 6(a): $\lambda_*>0$ unless $\ell$ is constant. Theorem 6(b): $\lambda_*\ge\lambda_{thr}$ . Theorem 6(d), as the paper's example: for $\ell(u)=u^2-|u|(1-e^{-|u|})$ , $P_0=\delta_0$ , $A=I$ and $\|\beta\|=1$ , $\lambda_*=\lambda_{thr}=\sqrt\delta$ and no distribution attains the value $\delta$ . Theorem 6(e), with Lemma 8: if $\ell''\le M$ and $\lambda_*>\tfrac12M\sqrt\delta\,\mathrm{ess\,sup}\,\beta^{\mathsf T}A(X)^{-1}\beta$ , then $\Gamma^*$ is a singleton $\{G(x)\}$ almost surely and the law of $X+\sqrt\delta G(X)A(X)^{-1}\beta$ is the unique worst case.

Significance

The result reduces a search over all probability measures to a scalar problem per data point. Each point is pushed along the single direction $A(x)^{-1}\beta$ , by an amount read off the maximizers of $F$ , and the budget $\delta$ is always spent completely. When the maximizer is not unique, randomization between two extreme maximizers is needed and suffices. Part (d) shows that the threshold condition cannot be removed, and part (e) gives a deterministic transport map (a Monge solution) under smoothness. Theorem 7 of the paper, the monotone growth of worst-case displacements in $\delta$ , is a statement about the random variable $G$ produced here.

None of these statements has been machine-checked before. The general strong duality with complementary slackness of Blanchet–Murthy (arXiv:1604.01446) is proved on the platform, so this mission connects that abstract theorem to an explicit worst-case law. A formal proof also has to settle one point the printed text leaves loose: which extreme maximizers enter the mixture (see Formalization scope).

Difficulty

The first idea is to take the pointwise maximizers of $F$ at $\lambda_*$ and push $P_0$ forward. That works only when the maximizer is unique and the budget constraint happens to be tight. In general the maximizer set is not a singleton, and the derivative of $f_\delta$ at $\lambda_*$ only lies between a left and a right derivative. Turning the first-order condition $\partial_+f_\delta\ge0\ge\partial_-f_\delta$ into an exact cost $\delta$ needs three things. The one-sided derivatives must be identified as expectations over $\Gamma^*$ , an envelope theorem under an integral with a non-compact parameter set. The extreme maximizers must be compact and measurably selectable. Finally the resulting coupling must be certified optimal through complementary slackness. Each step needs a hypothesis that is easy to lose: the growth control of Lemma 3, the essential supremum in $\lambda_{thr}$ , measurability of selections.

Formalization scope

Points of $\mathbb R^d$ are EuclideanSpace ℝ (Fin d), $\beta^{\mathsf T}x$ is the inner product, and $\beta^{\mathsf T}A(x)^{-1}\beta$ is quadInv A β x. $\ell_{\rm rob}$ and $f_\delta$ are extended-real valued; $f_\delta$ uses the published extended integral ModelRiskOT.Duality.extIntegral. The worst-case objective (6) is the published primal problem primalValue: a supremum over couplings $\pi$ with first marginal $P_0$ and $\int c\,d\pi\le\delta$ (primalFeasible). A distribution attains (6) when a coupling with that second marginal has value primalValue. The random worst case $X^*$ is encoded by the joint law of $(X,X^*)$ , a mixture of two graph couplings, because $E[c(X,X^*)]$ depends on the pair. A dual optimizer is a real $\lambda_*\ge0$ minimizing $f_\delta(\beta,\cdot)$ on $[0,\infty)$ .

Standing hypotheses on every statement: $P_0$ a probability measure, Assumptions 1 and 2, $\delta>0$ , $B$ convex. The following departures from the printed text are disclosed in each item:

In (c), $G_\pm$ are the selections of extreme square used in the proof (p. 40), not $\inf\Gamma^*$ and $\sup\Gamma^*$ as printed; a two-point example shows the printed choice can fail.
In (e), "for every $x$ " is read as "for $P_0$ -almost every $x$ ", which is what the proof gives.
Lemma 8 is stated for $\beta\ne0$ .
Proposition 2 is formalized for part (a) and the $\lambda$ -derivatives only.

Every expectation used in the goal ( $\bar c$ , $\underline c$ ) carries an integrability conjunct. The cost identity and optimality are asserted for the measure itself, so no junk value of a non-integrable integral can make the goal hold vacuously. A statement asserting only first-order conditions for $\lambda_*$ would not be Theorem 6. The goal asserts primal attainment and the exact cost.

Needed infrastructure, reusable beyond this mission: envelope (Danskin) theorems for one-sided derivatives of suprema, differentiation of convex integral functionals, measurable selection of argmax sets, and complementary slackness through the published Blanchet–Murthy theorem. Contributions of any of these as standalone lemmas are welcome.

Selected references

J. Blanchet, K. Murthy, F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Math. Oper. Res. 47(2), 2022. arXiv:1810.02403v3, doi:10.1287/moor.2021.1178
J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2), 2019. arXiv:1604.01446
J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019. doi:10.1017/jpr.2019.49
P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171, 2018. doi:10.1007/s10107-017-1172-1
D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (Proposition 7.50, measurable selection).

13 thms2 active usersReviewed

Operations Research Optimal Transport Optimization·Captain: mikedeng1

Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes 1: Mahalanobis-Transport Worst-Case Loss Equals inf over λ ≥ 0 of E_P0[ℓ_rob(β, λ; X)]Research Paper

Motivation

Distributionally robust optimization chooses a decision against a range of plausible probability laws instead of a single fitted law. Here the decision is a linear rule evaluated through a loss function. The range of laws is specified by how much probability mass may be transported away from a baseline law. A conventional transport cost depends only on the displacement. Blanchet, Murthy and Zhang allow the cost of moving a point to depend on its starting location, so the uncertainty model can reflect local information. Their introduction gives a portfolio example: uncertainty about returns may differ across market conditions, and a state dependent cost can encode that difference. The paper develops a dual reformulation as the basis for its later convexity, optimizer, and algorithmic results.

The theorem in this mission is the first structural result of that development. It says that evaluating the worst-case loss does not require optimizing directly over all probability distributions. A dual objective built from the baseline law gives the same value, and its nonnegative scalar multiplier attains the best value. The earlier general transport duality theorem of Blanchet and Murthy is already formalized and proved on Prove2Me; the remaining target here is the state dependent Mahalanobis specialization and its explicit scalar form.

Setting

Let $X\in\mathbb R^d$ have a baseline law $P_0$ , and let $B\subseteq\mathbb R^d$ be a convex set of decisions. A decision $\beta\in B$ incurs loss $\ell(\beta^{\mathsf T}X)$ , where $\ell:\mathbb R\to\mathbb R$ . The transport cost of moving $x$ to $x'$ is

c(x,x')=(x-x')^{\mathsf T}A(x)(x-x'),

where $A(x)$ is positive definite at every $x$ . Under Assumption 1, $c$ is lower semicontinuous, and the eigenvalues of $A(x)$ lie between fixed positive bounds $\rho_{\min}$ and $\rho_{\max}$ for $P_0$ -almost every $x$ . Since $A$ depends on the starting point, $c$ need not be symmetric. For two laws $P_0$ and $P$ , $D_c(P_0,P)$ is the least expected cost among couplings whose first and second marginals are $P_0$ and $P$ . The ambiguity set at radius $\delta>0$ consists of laws satisfying $D_c(P_0,P)\le\delta$ . The paper writes the worst-case loss as an equivalent supremum over couplings with first marginal $P_0$ and cost at most $\delta$ (§2.1, p. 9).

For $x,\beta\in\mathbb R^d$ , write $q_A(\beta,x)=\beta^{\mathsf T}A(x)^{-1}\beta$ . The paper introduces a pointwise robust loss from

F(\gamma,\beta,\lambda;x)=\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,q_A(\beta,x)\bigr)-\lambda\sqrt\delta\bigl(\gamma^2q_A(\beta,x)-1\bigr),

by setting $\ell_{\rm rob}(\beta,\lambda;x)=\sup_{\gamma\in\mathbb R}F(\gamma,\beta,\lambda;x)$ and $f_\delta(\beta,\lambda)=E_{P_0}[\ell_{\rm rob}(\beta,\lambda;X)]$ . This expectation may be extended real. These are the objects of display (7) and Theorem 1 on p. 10.

Formalization targets

The goal is Theorem 1 of the paper. If $\ell$ is upper semicontinuous and the baseline loss is integrable, then for each $\beta\in B$ ,

\sup_{P:\,D_c(P_0,P)\le\delta}E_P[\ell(\beta^{\mathsf T}X)]=\inf_{\lambda\ge0}f_\delta(\beta,\lambda),

and a multiplier $\lambda^*(\beta)\ge0$ attains the infimum. The target retains the state dependence of $A$ , the full range of $\beta$ in $B$ , and the possible extended value of the worst-case loss. It asserts both the value identity and attainment; the latter is part of the printed theorem.

The milestone list follows the paper's proof on p. 32: the previously proved general strong duality theorem, the quadratic minimum under a linear constraint, and pointwise equality (25) between the transport envelope and $\ell_{\rm rob}$ . The quadratic minimum is stated with attainment. The pointwise equality includes $\beta=0$ and records the change from the original transport multiplier to the scaled multiplier used in $F$ .

Significance

The formula replaces a search over probability laws with a scalar outer optimization and an expectation under $P_0$ . That representation is the paper's starting point for examining the shape of $f_\delta$ , locating dual optimizers, describing worst-case laws, and designing iterative schemes. Without a faithful dual identity, those later claims would concern a function whose connection to the original distributional problem had not been established (Theorems 2–7).

The general Blanchet–Murthy strong duality theorem has a machine-checked proof on Prove2Me. This mission supplies the specialized model, the quadratic reduction, and the equality with the paper's $f_\delta$ . Those declarations can then serve as a stable interface for the remaining missions in this series. The current goal and its new milestones are open Lean statements; the paper result itself is proved in the cited work.

Difficulty

The general duality theorem returns a dual problem whose envelope is a supremum over destination points in $\mathbb R^d$ . The paper's formula instead uses one scalar $\gamma$ , and its multiplier is scaled by $\sqrt\delta$ . Showing that these describe the same value requires controlling a positive definite quadratic cost with a state dependent matrix at every starting point. At $\beta=0$ , the hyperplane formula used in the nonzero case has a zero denominator, while equation (25) remains meaningful. Extended values also matter: the pointwise supremum can be infinite, and replacing it with a real-valued approximation could alter the theorem.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), laws are Borel probability measures, and matrices are real positive definite matrices. The local Setting definition fixes $c$ , $q_A$ , $F$ , $\ell_{\rm rob}$ , and $f_\delta$ using the paper's notation. The worst-case objective reuses the published coupling form ModelRiskOT.Duality.primalValue; its feasible plans already enforce the first marginal and cost budget. EReal carries the primal value, pointwise supremum, integral, and outer infimum. The extended integral is the published ModelRiskOT.Duality.extIntegral, with its documented convention for a difference of two infinite parts. The multiplier ranges over $\lambda\ge0$ , and $\delta>0$ is explicit so its square root can be used in the rescaling.

The goal retains the paper's standing convexity of $B$ , Assumption 1, and $\beta\in B$ . It adds integrability of $x\mapsto\ell(\beta^{\mathsf T}x)$ , required by the cited general duality theorem but omitted from the printed Theorem 1. This addition is disclosed so the statement's scope is clear. The goal equates the primal worst-case loss with the explicit infimum of $f_\delta$ and asserts attainment; an identity between two dual notations would leave the main claim unaddressed. Contributions to the positive definite quadratic minimization, the pointwise envelope equality, and their connection to the general duality theorem are in scope. The shared Setting layer is intended for reuse in the later convexity and worst-case-law missions.

Selected references

J. Blanchet, K. Murthy and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3
J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446v2

12 thms2 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Asymptotic Optimality of Constant-Order Policies for Lost Sales Inventory Models with Large Lead Times: The Best Constant-Order Policy Costs at Most 1 + ε Times the Optimum Once L ≥ y(ε)Research Paper

Motivation

The lost-sales inventory model with a positive lead time is one of the basic models of inventory theory. A retailer reviews stock once per period, places an order that arrives $L$ periods later, and loses (rather than backlogs) any demand that cannot be met from stock on hand. Lost sales are the norm in retail, where a customer facing an empty shelf buys elsewhere. The optimal policy is the solution of a dynamic program whose state is the on-hand inventory together with the whole pipeline of $L$ outstanding orders. The state dimension therefore grows with the lead time, and computing the optimal policy is intractable beyond small $L$ : for a lead time of four and geometric demand the dynamic program already has 228,581 states (Zipkin 2008a, Operations Research 56(5), 1256–1263).

Heuristics (base-stock, myopic, cost-balancing) have been studied at length. Reiman (2004) analyzed an open-loop policy that orders one unit at fixed intervals in a continuous-review lost-sales model with Poisson demand. Zipkin (2008a) observed numerically that ordering the same constant amount every period performs well already at lead time four. Huh, Janakiraman, Muckstadt and Rusmevichientong (2009) proved that order-up-to policies are asymptotically optimal as the lost-sales penalty grows. Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante proved that a constant-order policy is asymptotically optimal as the lead time grows, with an explicit threshold. This mission formalizes that result, Theorem 1 of their paper.

Setting

Fix a holding cost $h>0$ per unit left over at the end of a period, a lost-demand penalty $c>0$ per unit of unmet demand, a lead time $L\ge1$ , and a horizon $T>L$ . Demands $D_1,D_2,\dots$ are i.i.d. with a law $\mathcal D$ on $[0,\infty)$ that has a finite third moment and is not deterministic. At the start of period $t$ the system holds inventory $I_t$ and a pipeline $\mathbf x_t=(x_{1,t},\dots,x_{L,t})$ of outstanding orders. First $x_{1,t}$ arrives; then an order is placed and joins the end of the pipeline; then $D_t$ is realized, and

I_{t+1}=(I_t+x_{1,t}-D_t)^+,\qquad C_t=hI_{t+1}+c\,(I_t+x_{1,t}-D_t)^-.

The system starts empty. A policy chooses each order from the information available before the period's demand, possibly with randomization. Problem (1) is

\mathrm{OPT}(L,T)=\inf_{\pi}\sum_{t=L+1}^{T+L}\mathbb E[C^\pi_t].

For $r\ge0$ let $I^r_\infty=\sup_{k\ge0}\big(kr-\sum_{i=1}^kD_i\big)$ , the steady-state waiting time of a GI/D/1 queue. For $r<\mathbb E[D]$ the constant-order policy $\pi_r$ orders the random amount $I^r_\infty+r$ (drawn independently of the demands) in the first period and $r$ in every later period. The best constant is $z=\arg\min_{v\ge0}(h\mathbb E[I^v_\infty]-cv)$ (the smallest minimizer). With $Q$ the $c/(c+h)$ quantile of $\mathcal D$ , $g=h\mathbb E[(Q-D)^+]+c\mathbb E[(D-Q)^+]$ , $\sigma$ the standard deviation and $\zeta$ the skewness of $D$ , set $m=\lceil(26(3\zeta+c(h\sigma)^{-1}\mathbb E[D]+1))^2\rceil$ and

y(\epsilon)=\max\Big(2^{14}h(Q+2^{3/2}\mathbb E[D])(\mathbb E^2[D]+\mathbb E[D^2])^3\sigma^{-6}m^3g^{-1}\epsilon^{-1},\ \big(12c\,\mathbb E[D]\,g^{-1}((2ch^{-1})^{1/2}+3)\big)^2\epsilon^{-2}\Big).

Formalization targets

Goal: Theorem 1

For all $\epsilon\in(0,1)$ , $L\ge y(\epsilon)$ and $T\ge(1+3\epsilon^{-1})L$ ,

\mathbb E\Big[\sum_{t=L+1}^{T+L}C^{\pi_z}_t\Big]\ \le\ (1+\epsilon)\,\mathrm{OPT}(L,T).

Milestones

The milestones follow the paper's argument in its order:

the cost of $L$ consecutive periods from a given state (Lemma 3) and under $\pi_r$ (Lemma 4);
a bounded optimal policy (Lemma 5) and the existence of a most favourable state $(\mathbf x^*,\mathcal I^*)$ (§5);
lower bounds on the optimal cost over $L$ periods (Lemmas 6, 7);
random-walk estimates ((26) and Lemma 9) and the per-window gap of $\pi_{r^*}$ , $r^*=L^{-1}\sum_ix^*_i$ (Theorem 8);
an explicit Lipschitz CLT rate (Theorem 11), the separation $\mathbb E[D]-r^*\ge\frac12\sigma m^{-1/2}$ (Lemma 10), and the resulting explicit gap (Corollary 12);
the newsvendor bound $\mathbb E[C^\pi_t]\ge g$ (§3.1) and the stationary cost of $\pi_r$ , (25).

Significance

The theorem says that the policy which ignores the state entirely, ordering the same amount every period after a single randomized first order, loses at most a factor $1+\epsilon$ against the optimal policy once the lead time exceeds an explicit threshold. The threshold depends only on $h$ , $c$ and the demand law. Optimal policies are out of computational reach precisely when $L$ is large, so this is the first guarantee of near-optimality whose computation does not grow with the lead time. The paper's Corollary 2 (the ratio tends to $1$ as $L\to\infty$ ) follows directly.

The result is proved in the paper (up to the correction below); this platform holds no formalization of it or of its lemmas. A formalization would produce reusable statements about suprema of random walks with negative drift (Lemma 9, (26)), a quantitative central limit theorem for Lipschitz test functions (Theorem 11), and the finite-horizon lost-sales problem built on the published model of this platform.

Difficulty

The obvious comparison fails. An optimal policy may vary its orders arbitrarily over time, so its pipeline need not look like a constant stream. Comparing it period by period with $\pi_r$ gives nothing, because the inventory of $\pi_r$ is driven by an unbounded random-walk supremum.

The paper instead bounds the optimal cost over any $L$ consecutive periods by the cost from the most favourable state. It then has to show that the average $r^*$ of that state's pipeline stays bounded away from $\mathbb E[D]$ uniformly in $L$ . This last step is the crux. The components of $\mathbf x^*$ may vary considerably over the window, and a qualitative central limit theorem is not enough: the argument needs an explicit rate (Theorem 11) with constants that survive summation over $L$ windows. On the probabilistic side, the expectations of random indices $i^r_k$ at which random walks attain their maxima are not adapted to the demand filtration. They are controlled only through the distributional identity of Lemma 9 and the geometric tail (26).

Formalization scope

The model is the published CappedBaseStock_Model. Its parameter record supplies $L\ge1$ , $h>0$ and the penalty $c>0$ (field p; the record is called prm). Its demand law supplies a probability law on $[0,\infty)$ with finite positive mean. The finite third moment and non-determinism are explicit hypotheses. $Q$ and $g$ are the published newsvendorLevel and backorderCost. The conventions:

Time is zero-based: Lean period $t$ is the paper's period $t+1$ , and a window starting at Lean $t_0$ is the paper's $\tau=t_0+1$ . Pipeline slot $i$ is $x_{i+1}$ .
Costs, OPT and expectations of nonnegative quantities are lower integrals in $[0,\infty]$ , and $I^r_\infty$ is valued in $[0,\infty]$ . Real expectations appear only for integrable quantities.
OPT is the infimum over the model's admissible policies: measurable functions of past demands and a private uniform seed. This class contains the paper's policy class, so OPT is at most the paper's and the goal is at least as strong as the page.
"Conditional on $\mathbf x^\pi_\tau=\mathbf x$ , $I^\pi_\tau=\mathcal I$ " is rendered by running the system from that state. Lemma 3 states that this integrates back to the policy's cost.
Lemmas 6–7, Theorem 8 and Corollary 12 are stated for every policy that almost surely never orders more than $Q$ , which includes the paper's optimal $\bar\pi$ ; their proofs use only that bound.
$\pi_r$ draws its first order as the quantile function of $I^r_\infty$ at the policy's uniform seed.
The ratio of Theorem 1 is stated multiplicatively. A ratio would read $0$ at $\mathrm{OPT}=0$ , whereas $\mathrm{OPT}(L,T)\ge Tg>0$ .

A correction. As printed, the second term of $y(\epsilon)$ (p. 5) and of Corollary 12 (p. 14) lack a factor $\mathbb E[D]$ . The proof of Corollary 12 establishes $\mathcal I^*\le(\lceil(2ch^{-1}L)^{1/2}\rceil+2)\mathbb E[D]$ , and the printed bounds are not invariant under rescaling the demand. Both are stated here with the factor restored, and each item's note says so.

Neither a long-run average cost nor a restricted comparator (stationary, Markov, or bounded-order) may replace the finite-horizon OPT. The demand law may not be specialized, and $\pi_r$ may not order $r$ in its first period: each change makes the goal a different, easier theorem.

A complete development needs Lindley-type recursions and the stationarity of the GI/D/1 waiting time, Chernoff and moment bounds for random-walk maxima, a Stein-method CLT rate, and the existence of optimal policies for a finite-horizon problem with a continuous state. The random-walk and CLT parts are independent of inventory theory and reusable. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

D. A. Goldberg, D. A. Katz-Rogozhnikov, Y. Lu, M. Sharma, M. S. Squillante, Asymptotic Optimality of Constant-Order Policies for Lost Sales Inventory Models with Large Lead Times, Mathematics of Operations Research, 2016; preprint arXiv:1211.4063v2 (cited version). https://arxiv.org/abs/1211.4063
P. Zipkin, Old and New Methods for Lost-Sales Inventory Systems, Operations Research 56(5), 1256–1263, 2008.
P. Zipkin, On the Structure of Lost-Sales Inventory Models, Operations Research 56(4), 937–944, 2008.
W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science 55(3), 404–420, 2009.
M. Reiman, A New and Simple Policy for a Continuous Review Lost-Sales Inventory Model, unpublished manuscript, 2004.
L. H. Y. Chen, Q.-M. Shao, Stein's Method for Normal Approximation, in An Introduction to Stein's Method, 1–59, 2005.
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003.

21 thms2 active usersReviewed

Analysis Linear algebra Random Matrix Theory·Captain: mikedeng1

User-Friendly Tail Bounds for Sums of Random Matrices V: The Matrix Azuma Inequality for Adapted Sequences with Semidefinite Bounds on the Squared DifferencesResearch Paper

Motivation

Sums of random matrices appear throughout numerical linear algebra, statistics, combinatorics and quantum information: randomized sketching and sparsification, covariance estimation, graph sparsifiers, and the analysis of random features all reduce to controlling the largest eigenvalue of a sum of random self-adjoint matrices. Scalar concentration inequalities (Chernoff, Hoeffding, Bernstein, Azuma) have matrix analogues, and J. A. Tropp's User-Friendly Tail Bounds for Sums of Random Matrices (arXiv:1004.4389v7, Found. Comput. Math. 12 (2012) 389–434, doi:10.1007/s10208-011-9099-z) gives a unified derivation of them with explicit constants.

Many applications do not have independent summands: adaptive algorithms, online learning and sequential estimation produce sums whose terms depend on the past. The scalar tool for such sums is Azuma's inequality for martingales with bounded differences, and its corollary, McDiarmid's bounded differences inequality (McDiarmid 1998). This mission is the fifth of a series formalizing Tropp's paper; it targets §7, the matrix Azuma inequality.

Timeline. Ahlswede and Winter (2002) introduced a matrix analogue of the Laplace transform bound for independent sums; Oliveira (2010) gave the variant used in this paper. Tropp (this paper, 2010–2012) proved the matrix Azuma and McDiarmid inequalities below. More refined matrix martingale inequalities appear in Oliveira (2010) and in Tropp's Freedman's inequality for matrix martingales (2011), which the paper cites (p. 27) as requiring additional machinery.

Setting

All matrices are $d\times d$ with complex entries, $d\ge 1$ . A matrix is self-adjoint (s.a.) when it is Hermitian. For s.a. $A$ , $\lambda_{\max}(A)$ is its largest eigenvalue and $\|A\|$ its spectral norm. Functions of s.a. matrices are defined spectrally: if $A=Q\Lambda Q^*$ then $e^{A}=Qe^{\Lambda}Q^*$ , and $\log$ is defined the same way on positive-definite matrices. $A\preceq B$ is the semidefinite order: $B-A$ is positive semidefinite.

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space with a filtration $\mathcal F_0\subset\mathcal F_1\subset\cdots\subset\mathcal F$ , and write $\mathbb E_k[\,\cdot\,]=\mathbb E[\,\cdot\mid\mathcal F_k]$ . The expectation and the conditional expectation of a random matrix are taken entrywise. A sequence $X_1,\dots,X_n$ of random matrices is adapted when each $X_k$ is $\mathcal F_k$ -measurable. A matrix martingale is an adapted sequence of s.a. matrices $Y_k$ with $\mathbb E\|Y_k\|<\infty$ and $\mathbb E_{k-1}Y_k=Y_{k-1}$ ; its difference sequence $X_k=Y_k-Y_{k-1}$ satisfies $\mathbb E_{k-1}X_k=0$ .

The hypotheses of the main theorem are: $X_1,\dots,X_n$ is an adapted sequence of random s.a. matrices, and $A_1,\dots,A_n$ is a fixed (non-random) sequence of s.a. matrices, with

\mathbb E_{k-1}X_k = 0 \qquad\text{and}\qquad X_k^2\preceq A_k^2\ \text{ almost surely.}

The variance parameter is $\sigma^2 := \big\|\sum_k A_k^2\big\|$ .

Formalization targets

Goal: Theorem 7.1 (Matrix Azuma), p. 27

For all $t\ge 0$ ,

\mathbb P\Big\{\lambda_{\max}\Big(\sum_{k}X_k\Big)\ge t\Big\}\le d\cdot e^{-t^2/8\sigma^2}.

Milestones

In the order they are used:

Display (2.6), Golden–Thompson: $\operatorname{tr}e^{A+H}\le\operatorname{tr}(e^Ae^H)$ for s.a. $A,H$ .
Proposition 3.1, the Laplace transform method: $\mathbb P\{\lambda_{\max}(Y)\ge t\}\le\inf_{\theta>0}e^{-\theta t}\,\mathbb E\operatorname{tr}e^{\theta Y}$ .
Corollary 3.3: $\mathbb E\operatorname{tr}\exp(H+X)\le\operatorname{tr}\exp(H+\log\mathbb E e^{X})$ .
Lemma 4.3, Rademacher half: $\mathbb E e^{\varepsilon\theta A}\preceq e^{\theta^2A^2/2}$ .
Lemma 7.6 (Symmetrization): $\mathbb E\operatorname{tr}e^{H+X}\le\mathbb E\operatorname{tr}e^{H+2\varepsilon X}$ when $\mathbb EX=0$ and $\varepsilon$ is an independent Rademacher variable.
Lemma 7.7 (Azuma cgf): $\log\mathbb E[e^{2\varepsilon\theta X}\mid X]\preceq2\theta^2A^2$ when $X^2\preceq A^2$ .
Display (7.5): $\mathbb E\operatorname{tr}\exp(\sum_k\theta X_k)\le\operatorname{tr}\exp(2\theta^2\sum_kA_k^2)$ under the hypotheses of the goal.

Further statements

Corollary 7.2 is the martingale form, $\mathbb P\{\lambda_{\max}(Y_n-\mathbb EY_n)\ge t\}\le d\,e^{-t^2/8\sigma^2}$ . Corollary 7.5 (Matrix Bounded Differences) is the matrix McDiarmid inequality, $\mathbb P\{\lambda_{\max}(H(z)-\mathbb EH(z))\ge t\}\le d\,e^{-t^2/8\sigma^2}$ for a matrix-valued function $H$ of independent variables whose changes in one coordinate $k$ have squares bounded by $A_k^2$ .

Significance

The result. The bound has the scalar subgaussian shape with two matrix features: a dimensional factor $d$ , and a variance parameter equal to the norm of the sum $\sum_kA_k^2$ rather than the sum of the norms $\sum_k\|A_k\|^2$ . In the commuting case the two coincide; in general the first can be smaller by a factor of up to $n$ . The theorem needs no independence, so it covers adapted constructions such as Doob martingales. Corollary 7.5, obtained from it, is the standard matrix tool for concentration of matrix-valued functions of independent data. With independent summands the theorem gives a matrix Hoeffding inequality (Theorem 1.3 of the paper).

Formalizing it. The result is proved in the paper; none of it is formalized. Mathlib has the continuous functional calculus, conditional expectation and filtrations, but no Golden–Thompson inequality, no Lieb concavity theorem, and no matrix tail inequality. A formalization produces a machine-checked matrix Azuma inequality, the Golden–Thompson inequality, and a symmetrization lemma for the trace exponential, all of which have uses beyond this paper.

Difficulty

The scalar proof of Azuma's inequality multiplies conditional moment generating functions, $\mathbb E e^{\theta\sum X_k}=\mathbb E\big[e^{\theta\sum_{k<n}X_k}\,\mathbb E_{n-1}e^{\theta X_n}\big]$ , and bounds each factor. For matrices this fails: $e^{A+B}\neq e^Ae^B$ unless $A$ and $B$ commute, and $\operatorname{tr}e^{A+B+C}\le\operatorname{tr}(e^Ae^Be^C)$ is false, so the Golden–Thompson inequality cannot be iterated over $n$ terms. The paper itself notes (p. 28) that the classical approach does not seem to extend. A second obstacle is that the hypothesis $X_k^2\preceq A_k^2$ bounds squares, not the matrices themselves; it does not give $X_k\preceq A_k$ , so the scalar Hoeffding lemma for bounded centred variables has no direct matrix analogue. The infrastructure is also heavy: Lieb's concavity theorem underlies Corollary 3.3, and operator monotonicity of the logarithm is needed.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ, self-adjointness is IsHermitian, and $\preceq$ is Mathlib's order under MatrixOrder. Matrix exponential and logarithm are cfc Real.exp and cfc Real.log. $\lambda_{\max}$ is the supremum of the real spectrum, which is why $d\ge1$ is assumed (NeZero d). Expectation and conditional expectation of matrices are entrywise Bochner integrals; adaptedness is entrywise strong measurability with respect to a Mathlib Filtration ℕ. The summands are indexed by $k=1,\dots,n$ , so $\mathcal F_{k-1}$ is never truncated. The bound $X_k^2\preceq A_k^2$ is required almost surely. The bounds $A_k$ are deterministic matrices. The infimum over $\theta>0$ in Proposition 3.1 is posed as the bound for each $\theta>0$ at which the expectation is finite.

The hypotheses must not be made vacuous. Integrability of each $X_k$ is assumed explicitly, because for a non-integrable variable Lean's conditional expectation is $0$ and the centring hypothesis would say nothing. The $X_k$ are not assumed independent: an independence hypothesis would turn the goal into the weaker matrix Hoeffding inequality.

Two readings are recorded in the statements. In Lemma 7.7 the conditional expectation given $X$ is replaced by the expectation over $\varepsilon$ at each fixed value $x$ with $x^2\preceq A^2$ ; by independence these agree. Corollary 7.2 adds the hypothesis that $Y_0$ is almost surely constant, without which $Y_n-\mathbb EY_n\neq\sum_kX_k$ .

A complete development needs: Golden–Thompson; Lieb's concavity theorem (or Corollary 3.3 directly); operator monotonicity of the matrix logarithm; monotonicity of the trace exponential; conditional expectation of matrix-valued variables and its interaction with the semidefinite order. All of these are reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.1, Corollary 3.3 and Lemma 4.3 are also milestones of other missions in this series.

Selected references

J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, Found. Comput. Math. 12 (2012) 389–434; cited version arXiv:1004.4389v7 (2011). https://arxiv.org/abs/1004.4389v7
R. Ahlswede and A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://doi.org/10.1109/18.985947
R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821
J. A. Tropp, Freedman's inequality for matrix martingales, Electron. Commun. Probab. 16 (2011) 262–270. https://arxiv.org/abs/1101.3039
R. I. Oliveira, Concentration of the adjacency matrix and of the Laplacian in random graphs with independent edges, arXiv:0911.0600 (2010). https://arxiv.org/abs/0911.0600
C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer (1998) 195–248. https://doi.org/10.1007/978-3-662-12788-9_6
R. Bhatia, Matrix Analysis, Springer GTM 169 (1997), Sec. IX.3. https://doi.org/10.1007/978-1-4612-0653-8
E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X

10 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Hedging Inventory Risk Through Market Instruments I: Hedging Raises the Risk-Averse Newsvendor's Optimal Order QuantityResearch Paper

Motivation

A retailer who orders a seasonal product before demand is known faces the newsvendor trade-off. Ordering too much leaves unsold stock, and ordering too little forgoes sales. A risk-neutral newsvendor orders a critical fractile of demand. A risk-averse one orders less, since inventory is a risky investment, and this reduction has been shown under constant and decreasing absolute risk aversion (Eeckhoudt, Gollier and Schlesinger, Management Science 41(5), 1995, doi:10.1287/mnsc.41.5.786). Agrawal and Seshadri (2000) and Chen and Federgruen (2000) reached related conclusions.

Demand for many products moves with traded financial quantities: a stock index, a commodity price, an exchange rate. V. Gaur and S. Seshadri (Manufacturing & Service Operations Management 7(2), 2005, pp. 103–120, doi:10.1287/msom.1040.0061) ask what happens when the newsvendor can trade a financial instrument correlated with demand. Their Proposition 7 answers one half of the question: hedging moves the risk-averse newsvendor's order up, towards the risk-neutral quantity. This mission formalizes Proposition 7 and the steps of its appendix proof. The source is the published article, a library scan.

Setting

Let $S_T$ be the price at time $T$ of a traded asset, with law $\nu$ on $\mathbb R$ . Demand is $D=a+b(S_T+\varepsilon)$ with $b>0$ . Here $\varepsilon$ is the scaled forecast error, independent of $S_T$ , with law $G$ , $E[\varepsilon]=0$ and $E[\varepsilon^2]<\infty$ . The unit selling price, cost and salvage value are $p>ce^{rT}>s$ . In the paper's scaled units ((11), p. 110) these collapse into one cost parameter $c_1$ with $0<c_1$ and $c_1b<1$ , and an initial-wealth term $W$ .

A hedge is a portfolio with time- $T$ payoff $X_T=\varphi(S_T)$ for a nondecreasing function $\varphi$ , and time-0 price $X_0$ . It is a fair gamble, $E[X_T]=X_0e^{rT}$ (display (12)). A firm that stocks $I>\max\{a,0\}$ units and shorts $\alpha$ units of the hedge ends with the scaled wealth (14)

\Pi_H(I,\alpha)=W+\min\Big\{S_T+\varepsilon,\ \frac{I-a}{b}\Big\}-c_1I-\alpha X_T+\alpha X_0e^{rT}.

A decision maker with utility $u:\mathbb R\to\mathbb R$ ranks $(I,\alpha)$ by $E[u(\Pi_H(I,\alpha))]$ , and $I^*(\alpha)$ maximizes it over $I$ .

The absolute risk aversion is $R_A(w)=-u''(w)/u'(w)$ and the absolute prudence is $-u'''(w)/u''(w)$ . The utility displays DARA or CARA when $R_A$ is decreasing or constant, and DAP when prudence is decreasing or constant.

The hedge ratio is bounded by $\bar\alpha$ , chosen so that $E_\varepsilon[\Pi_H(I,\alpha)\mid S_T]$ is nondecreasing in $S_T$ for $0\le\alpha\le\bar\alpha$ . Beyond $\bar\alpha$ the firm over-hedges: its expected profit falls as the asset price rises.

Formalization targets

Goal: Proposition 7 (p. 112)

For an increasing, concave, differentiable utility with constant or decreasing absolute risk aversion and constant or decreasing absolute prudence,

\frac{dI^*}{d\alpha}\ \ge\ 0\qquad\text{for }0\le\alpha\le\bar\alpha,

stated as: $\alpha\mapsto I^*(\alpha)$ is nondecreasing on $[0,\bar\alpha]$ .

Milestones

Lemma 2 (p. 118), in its weak form. If $f$ is decreasing with $E[f(X)]=0$ , then $E[w(X)f(X)]\ge0$ for decreasing nonnegative $w$ , and $E[w(X)f(X)]\le0$ for increasing nonnegative $w$ .
Utility facts of §3.2 (p. 111). DARA or CARA implies $u'''\ge0$ , and DAP implies that $u'''$ is decreasing.
Steps of the proof (pp. 118–119).
- $E_\varepsilon[u''(\Pi)\mid S_T]$ is increasing in $S_T$ .
- The first term of the cross-partial representation (25) is nonnegative.
- The quantity $(1/b)R_A(\Pi_0)u'(\Pi_0)\Pr\{\varepsilon>(I-a)/b-S_T\}\,\partial\Pi/\partial\alpha$ has nonpositive mean.
- $\partial^2E[u(\Pi)]/\partial I\partial\alpha\ge0$ , as increasing differences of $E[u(\Pi_H(I,\alpha))]$ on $(\max\{a,0\},\infty)\times[0,\bar\alpha]$ .

Significance

Proposition 7 reverses the conclusion of Eeckhoudt et al. Those authors find that an additional uncorrelated background risk lowers the risk-averse newsvendor's order. Here a correlated financial position that offsets the inventory risk raises it. Hedging therefore increases expected profit as well as reducing variance, and brings a risk-averse firm's operational decision closer to the risk-neutral one. The result is one of the basic statements linking operational and financial risk management in supply-chain finance.

The formalization adds three things.

Corrected lemmas. The proof rests on a one-variable Chebyshev inequality (Lemma 2) whose printed strict form is false, and on a cross-partial computation that differentiates under the expectation without comment. A machine-checked proof fixes the correct hypotheses: the weak inequalities, and the integrability under which (24)–(25) hold.
Reusable monotone comparative statics. The steps from increasing differences in (inventory, hedge ratio) to a monotone argmax apply to other stochastic inventory models with expected-utility objectives.
Formal status. The result is proved in the paper. To our knowledge no part of it has been formalized.

Difficulty

The obvious argument signs the cross-partial derivative directly: $E[u''(\Pi)\,\partial\Pi/\partial I\,\partial\Pi/\partial\alpha]$ , with $\partial\Pi/\partial\alpha=X_0e^{rT}-X_T$ of mean zero. That needs the sign of a covariance between $\partial\Pi/\partial\alpha$ and $u''(\Pi)\,\partial\Pi/\partial I$ , a weight that depends on both $S_T$ and $\varepsilon$ and is not monotone in either.

The paper first conditions on $S_T$ and splits the weight into two terms. The first is a conditional mean of $u''(\Pi)$ . The second is concentrated on the sell-out event. Each term then needs its own monotonicity in $S_T$ .

For the second term, monotonicity comes from DARA alone.
For the first term, $E_\varepsilon[u''(\Pi)\mid S_T]$ , a second application of the Chebyshev inequality, in $\varepsilon$ , is needed. It uses prudence (DAP) and the bound $\alpha\le\bar\alpha$ .

Neither ingredient can be dropped. Without $\alpha\le\bar\alpha$ the conditional mean payoff decreases in $S_T$ and the first term changes sign.

Two further obstacles are technical:

the expectation is not differentiable in $I$ where $\varepsilon=(I-a)/b-S_T$ has an atom;
the hedge $\varphi$ is only monotone, hence differentiable only almost everywhere.

Formalization scope

Representation.

$S_T\sim\nu$ and $\varepsilon\sim G$ are probability measures on $\mathbb R$ , and every expectation is taken over $\nu\otimes G$ . Independence is built in, and $E_\varepsilon[\,\cdot\mid S_T=s]$ is the integral over $G$ at fixed $s$ .
The parameters are the scaled $W,a,b,c_1$ of (11). The constraint $p>ce^{rT}>s$ becomes $0<c_1$ and $c_1b<1$ , an exact reparametrization.
The hedge is a nondecreasing, measurable, $\nu$ -integrable $\varphi$ with $\int\varphi\,d\nu=X_0e^{rT}$ . The paper's "piecewise continuous, differentiable a.e." is dropped, so the formal statement is more general.
$R_A$ is the platform's Arrow–Pratt coefficient MDPFinance.FinancialMarkets.arrowPrattCoefficient, referenced rather than redefined.

Conventions.

"Increasing, concave, differentiable" is taken as $C^3$ with $u'>0$ and $u''<0$ on all of $\mathbb R$ . Absolute prudence $-u'''/u''$ requires $u''\ne0$ , and the proof uses $u''<0$ .
DARA/CARA and DAP are stated as $R_A$ and the prudence being nonincreasing.
$\bar\alpha$ is any value for which the conditional mean payoff is nondecreasing in $S_T$ for every $\alpha\in[0,\bar\alpha]$ and every admissible $I>\max\{a,0\}$ .
$I^*$ is any selection of maximizers over $I>\max\{a,0\}$ ; the maximizer is unique by strict concavity.
$dI^*/d\alpha\ge0$ is stated as monotonicity of $I^*$ . The cross-partial claim is stated as increasing differences.
Lemma 2 and "the second term is negative" are weakened to the non-strict inequalities, because the printed strict forms fail for constant weights.

Integrability. The goal and the increasing-differences milestone assume integrability of $u(\Pi)$ , $u'(\Pi)$ , $u''(\Pi)$ and of their products with $\partial\Pi/\partial\alpha$ on the whole region, which is the regularity the proof uses. Without it a Bochner integral would silently be $0$ : the objective would be constant in $I$ and every $I$ a maximizer. A hypothesis set that forces $\bar\alpha=0$ would also trivialize the goal. A sorry-free check file exhibits the utility class, the standing assumptions and the $\bar\alpha$ -condition with $\bar\alpha=1/2$ for $u(w)=-e^{-w}$ , $\varepsilon=\pm1$ with equal probability and $\varphi(s)=\min\{s,-1/2\}$ .

Infrastructure and contributions. A one-variable Chebyshev association inequality for monotone functions is needed. So are differentiation under the integral, or an integrated mean-value argument, for piecewise-linear payoffs, and the step from increasing differences plus a unique maximizer to a monotone argmax. All three are reusable. Proofs of the milestones in any order are welcome, as are alternative arguments that avoid the cross-partial derivative altogether.

Selected references

V. Gaur, S. Seshadri, Hedging Inventory Risk Through Market Instruments, Manufacturing & Service Operations Management 7(2), 103–120, 2005. https://doi.org/10.1287/msom.1040.0061
L. Eeckhoudt, C. Gollier, H. Schlesinger, The Risk-Averse (and Prudent) Newsboy, Management Science 41(5), 786–794, 1995. https://doi.org/10.1287/mnsc.41.5.786
M. S. Kimball, Precautionary Saving in the Small and in the Large, Econometrica 58(1), 53–73, 1990. https://doi.org/10.2307/2938334
K. J. Arrow, Essays in the Theory of Risk-Bearing, North-Holland, 1971.
P. Milgrom, C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479

11 thms2 active usersReviewed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Making Gradient Descent Optimal for Strongly Convex Stochastic Optimization 3: SGD with Full Averaging Suffers an Ω(log(T)/T) Rate on a Non-Smooth Strongly Convex ProblemResearch Paper

Motivation

Stochastic gradient descent (SGD) is the standard first-order method for stochastic convex optimization and for training linear predictors on large data sets: at each step it queries a noisy subgradient of the objective, takes a step against it and projects back onto the feasible set. When the objective is strongly convex, the classical online-learning analysis of SGD with step sizes $\eta_t=\Theta(1/t)$ bounds the expected suboptimality of the averaged iterate $\bar w_T=\frac1T(w_1+\dots+w_T)$ by $O(\log(T)/T)$ (Hazan, Agarwal, Kale 2007). The information-theoretically optimal rate for this problem class is $O(1/T)$ , and it is attained by other algorithms (Hazan, Kale 2011; Juditsky, Nesterov 2010).

This left a concrete question: is the logarithmic factor an artifact of the analysis, or a property of SGD with averaging? Rakhlin, Shamir and Sridharan (arXiv:1109.5647v7, ICML 2012) answer it by exhibiting strongly convex problems on which averaged SGD provably loses the logarithm. The same paper shows that for objectives that are smooth at the optimum the averaged iterate attains $O(1/T)$ , and that averaging only a suffix of the iterates restores $O(1/T)$ in general. This mission is the lower-bound half of that picture; the two upper bounds are sibling missions of the same series.

Setting

Points live in $\mathbb R^d$ , $d\ge1$ , with the Euclidean norm; for a point $w$ , $w_1$ denotes its first coordinate. A stochastic gradient oracle for an objective $F$ returns, at a query point $w_t$ , a random vector $\hat g_t$ whose mean is a subgradient of $F$ at $w_t$ . Projected SGD on a domain $W$ with step sizes $\eta_t=c/t$ , $c>0$ , starts at a point $w_1\in W$ and sets

w_{t+1}=\Pi_W\big(w_t-\eta_t\hat g_t\big),\qquad t=1,2,\dots,

where $\Pi_W$ is the Euclidean projection onto $W$ . The output studied here is the average $\bar w_T=\frac1T(w_1+\dots+w_T)$ . Throughout, $Z_1,Z_2,\dots$ are independent random variables, each uniformly distributed on $[-1,3]$ .

Example A. $W=[0,1]^d$ , $F(w)=\tfrac12\|w\|^2+w_1$ , and the oracle returns $\hat g_t=w_t+(Z_t,0,\dots,0)$ . The global minimum over $W$ is at $w^*=0$ , a corner of the box.

Example B. $W=[-1,1]^d$ and

F(w)=\tfrac12\|w\|^2+\begin{cases}w_1&w_1\ge0\\-7w_1&w_1<0,\end{cases}\qquad \hat g_t=w_t+\begin{cases}(Z_t,0,\dots,0)&w_{t,1}\ge0\\(-7,0,\dots,0)&w_{t,1}<0.\end{cases}

Here $F$ is $1$ -strongly convex and non-smooth along the hyperplane $w_1=0$ , and its minimizer $w^*=0$ lies in the interior of $W$ . The oracle is state-dependent: which branch it uses depends on the sign of the first coordinate of the query point. In both examples $\mathbb E[\hat g_t]$ is a subgradient of $F$ at $w_t$ and $\mathbb E\|\hat g_t\|^2$ is bounded for fixed $d$ .

Formalization targets

Goal: Theorem 4 (p. 5)

In Example B, for every $c>0$ , every starting point $w_1\in W$ with $w_{1,1}\ge0$ , $T_0=\max\{2,6c+1\}$ and every integer $T\ge T_0+2$ ,

\mathbb E\big[F(\bar w_T)-F(w^*)\big]\ \ge\ \frac{3c}{16T}\sum_{t=T_0+2}^{T}\frac1t-\frac{T_0}{T}.

For fixed $c$ this is $\Omega(\log(T)/T)$ . The goal is the paper's statement with its constants.

Milestones

Theorem 3 (p. 5). In Example A, for every $c>0$ , every $w_1\in W$ , $T_0=\max\{2,c/2\}$ and every integer $T\ge T_0+1$ ,

\mathbb E\big[F(\bar w_T)-F(w^*)\big]\ \ge\ \frac{c}{16T}\sum_{t=T_0}^{T-1}\frac1t.

Eq. (9) (p. 16). The pathwise recursion of the first coordinate in Example B:

w_{t+1,1}=\Pi_{[-1,1]}\Big(\big(1-\tfrac ct\big)w_{t,1}-\begin{cases}Z_t\,c/t&w_{t,1}\ge0\\-7c/t&w_{t,1}<0\end{cases}\Big).

App. B.5, p. 17. In Example B, whenever $c/t<1$ ,

\Pr\big(w_{t,1}\notin[0,c/t]\ \big|\ w_{t-1,1}\ge0\big)\ \ge\ \tfrac34 .

Significance

The result. Theorem 4 shows that the $O(\log(T)/T)$ guarantee for SGD with full averaging is tight up to constants on strongly convex problems, even when the optimum is interior. It separates SGD with averaging from algorithms that reach $O(1/T)$ , and it is the reason the paper introduces $\alpha$ -suffix averaging. It also explains why smoothness at the optimum (the paper's §3) matters: Example B is non-smooth exactly at $w^*$ .

Formalizing it. The result is proved on paper but, as far as the platform's index shows, has no machine-checked proof. Formalization adds a verified lower bound with explicit constants. It also settles the paper's own argument. The printed proof of Theorem 4 relies on Lemma 4 (p. 16), whose first claim uses $Z_t\ge-1$ where the recursion subtracts $(c/t)Z_t$ with $Z_t$ up to $3$ , so Lemma 4 fails with positive probability. Theorem 4 is believed true, but a complete proof needs a repaired argument. Theorem 3's printed proof uses $\eta_t\le1$ in step (8), while $t\ge T_0$ only gives $\eta_t\le2$ . Numerical checks of Theorem 3 itself found no violation.

Difficulty

An expectation lower bound on the average needs control of every iterate $w_t$ , not just of the last one, and the iterates form a non-linear Markov chain because of the projection and, in Example B, because of the state-dependent oracle. Upper-bound techniques do not transfer: they bound $\mathbb E\|w_t-w^*\|^2$ from above, which says nothing about the sign of $w_{t,1}$ . In Example B, the natural first idea is to argue that $w_{t,1}$ never stays negative, so that it behaves like the constrained Example A; this is the claim of the paper's Lemma 4, and as stated it does not hold, because a single noise draw near $3$ can push the first coordinate below the level the lemma asserts. A proof must handle that event with explicit constants and still produce the $T_0/T$ slack of the statement.

Formalization scope

Space. $\mathbb R^d$ is UnderstandingML.Vec d = EuclideanSpace ℝ (Fin d) with [NeZero d]; the paper's first coordinate is index 0.
Projection. $\Pi_W$ onto the box $[lo,hi]^d$ is coordinatewise clamping $v_i\mapsto\max\{lo,\min\{hi,v_i\}\}$ , which is the Euclidean projection onto the box.
Indexing. sgdRun … k is the paper's $w_{k+1}$ ; the step at index $k$ uses $\eta_{k+1}=c/(k+1)$ and the noise value $Z$ at index $k$ . The starting point is arbitrary (not $0$ ), as in Theorems 3–4.
Noise. Each $Z_t$ has law ProbabilityTheory.cond volume (Set.Icc (-1) 3) (uniform on $[-1,3]$ ); a horizon- $T$ sequence has the product law UnderstandingML.iidLaw. Expectations are Bochner integrals over it.
Constants and ranges. $c>0$ is the only condition on $c$ . $T_0$ is real; $T$ is a natural number; $\sum_{t=T_0}^{T-1}$ is over the integers $\lceil T_0\rceil\le t\le T-1$ , and $\sum_{t=T_0+2}^{T}$ over $\lceil T_0\rceil+2\le t\le T$ . $F(w^*)$ is written $F(0)$ .
No junk integrals. Theorems 3 and 4 also assert integrability of $F(\bar w_T)-F(0)$ , so the inequality cannot hold because an integral defaulted to $0$ . The probability milestone is stated multiplicatively, $\Pr(A\cap B)\ge\frac34\Pr(B)$ , rather than through ProbabilityTheory.cond, which would be the zero measure on a null conditioning event.
Not trivializable. The examples (the constant $7$ , the noise interval $[-1,3]$ , the boxes $[0,1]^d$ , $[-1,1]^d$ ) are fixed by the paper; replacing the oracle or the domain is a different theorem. Since $F(\bar w_T)\ge F(0)$ always, Theorem 4 is immediate whenever its right-hand side is negative, but it is a non-trivial inequality for large $T$ , and the statement quantifies over all $T\ge T_0+2$ .
Not posed. Lemma 4 (false as stated), step (8) of App. B.4, and Eq. (10) with the displays after it in App. B.5 (they depend on Lemma 4).
Infrastructure. Measurability of the SGD run in the noise sequence, independence of $Z_t$ from the past iterates under the product law, and probabilities of intervals under the uniform law are reusable for any analysis of SGD on explicit examples. Proofs of the milestones, a repaired proof of Lemma 4's role, and a complete proof of Theorem 4 are all welcome.

Selected references

A. Rakhlin, O. Shamir, K. Sridharan, Making Gradient Descent Optimal for Strongly Convex Stochastic Optimization, ICML 2012; arXiv:1109.5647v7, 2012. https://arxiv.org/abs/1109.5647v7
E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69, 2007. https://doi.org/10.1007/s10994-007-5016-8
E. Hazan, S. Kale, Beyond the regret minimization barrier: an optimal algorithm for stochastic strongly-convex optimization, COLT 2011. https://proceedings.mlr.press/v19/hazan11a.html
A. Juditsky, Y. Nesterov, Primal-dual subgradient methods for minimizing uniformly convex functions, 2010. https://hal.science/hal-00508933
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19(4), 2009. https://doi.org/10.1137/070704277

7 thms2 active usersReviewed

Bandit Algorithms Machine Learning Statistics·Captain: mikedeng1

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

Motivation

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

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

Timeline.

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

Setting

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

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

The regret after $T$ rounds is

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

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

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

Formalization targets

Goal: Theorem 1 (p. 3)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

Conventions.

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

Added hypotheses and corrections.

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

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

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

Selected references

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

17 thms2 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Matroid Prophet Inequalities 3: Stopping at the First Value Above E[max X_i]/2 Earns at Least Half the Prophet's Expected MaximumResearch Paper

Motivation

A prophet inequality compares two players facing the same random sequence of rewards $X_1, X_2, \dots, X_n$ . The gambler sees the values one at a time and must decide, as each value arrives, whether to stop and collect it; a value passed over is lost. The prophet knows the whole sequence in advance and simply takes its maximum. In 1978 Krengel, Sucheston and Garling showed that when the $X_i$ are independent, non-negative and $\mathbb E[\max_i X_i] < \infty$ , the gambler has a stopping rule $\tau$ with

2\,\mathbb E[X_\tau] \;\ge\; \mathbb E\big[\max_i X_i\big],

and that the factor $2$ cannot be improved. This inequality, labelled (1) in Kleinberg and Weinberg's Matroid Prophet Inequalities (arXiv:1201.4764, STOC 2012), is the starting point of optimal stopping theory's prophet inequalities and, more recently, of a large literature in online algorithms and algorithmic mechanism design, where it is the reason that a single posted price can extract a constant fraction of the optimal welfare or revenue.

Timeline.

1977: Krengel and Sucheston prove the inequality with factor 4 in place of 2 (Bull. Amer. Math. Soc. 83).
1978: Krengel and Sucheston publish the result attributed to Krengel, Sucheston and Garling, the factor-2 inequality (1) for independent non-negative rewards with $\mathbb E[\max_i X_i] < \infty$ ; the factor $2$ cannot be improved.
1984: Samuel-Cahn shows that a single threshold suffices: stopping at the first value above a threshold $T$ with $\Pr[\max_i X_i > T] = \tfrac12$ (a median of $\max_i X_i$ ) already achieves the factor $2$ (doi:10.1214/aop/1176993223).
2012: Kleinberg and Weinberg, introducing the matroid prophet inequality, give in §3.1 a second single-threshold rule, with threshold $T = \mathbb E[\max_i X_i]/2$ , and a half-page proof that it earns at least $T$ . This rule and its analysis are the rank-one case of their matroid algorithm.

This mission formalizes that §3.1 result.

Setting

Let $(\Omega, \mathcal F, \mathbb P)$ be a probability space and $n \ge 1$ . Let $X_1, \dots, X_n$ be real random variables on $\Omega$ that are independent (as a family), non-negative, and such that the prophet's value $\max_i X_i$ has finite expectation. Define

T = \tfrac12\,\mathbb E\big[\max_i X_i\big], \qquad p = \Pr\big[\max_i X_i \ge T\big].

The single-threshold rule observes $X_1, X_2, \dots$ in order and stops at the first time $\tau$ with $X_\tau \ge T$ , collecting $X_\tau$ . If no $X_i$ reaches $T$ , the rule accepts nothing and collects $0$ . Write $X_\tau$ for the amount collected; it equals $X_{\tau(\omega)}(\omega)$ on the event $\{\max_i X_i \ge T\}$ , which has probability $p$ , and $0$ off it.

In Lean the variables are X : Fin n → Ω → ℝ with [NeZero n]; $\max_i X_i$ is maxX X, $T$ is thr P X, $p$ is stopProb P X, and $X_\tau$ is reward P X, all in the namespace MatroidProphetKW.RankOne.

Formalization targets

Goal: the half-mean threshold rule

\mathbb E[X_\tau] \;\ge\; T \;=\; \tfrac12\,\mathbb E\big[\max_i X_i\big].

This is inequality (1) for an explicit rule, which is stronger than (1)'s existence statement. The constant $\tfrac12$ is sharp, so the goal is stated with it.

Milestones (in the order the paper's argument uses them)

Tail bound, for every $x > T$ :

\Pr[X_\tau > x] \;\ge\; (1-p)\sum_{i=1}^n \Pr[X_i > x].

Comparison with the prophet's tail, for every $x > T$ :

\Pr[X_\tau > x] \;\ge\; (1-p)\,\Pr\big[\max_i X_i > x\big].

The prophet's upper tail:

\int_T^\infty \Pr\big[\max_i X_i > x\big]\,dx \;\ge\; T.

The gambler's lower tail:

\int_0^T \Pr[X_\tau > x]\,dx \;\ge\; pT.

Significance

The result. A threshold that depends on the distributions only through one number, $\mathbb E[\max_i X_i]$ , already matches the optimal worst-case guarantee of the best stopping rule. Because it is a single price, the rule translates directly into a posted-price mechanism: a seller who posts the price $T$ to arriving buyers obtains half of the expected maximum value. The same accounting, in which accepted value is charged against the threshold and rejected value against the probability of having accepted nothing, is what Kleinberg and Weinberg generalize to matroids (missions 1 and 2 of this series).

Formalizing it. The result is proved and classical; the work here is to formalize its known proof. No machine-checked proof of the factor-2 prophet inequality is in Mathlib, and none was found among the platform's published theorems in October 2026. A completed development provides the inequality itself, the tail comparisons, and the layer-cake bookkeeping for a stopped reward, all of which are reusable for other single-threshold prophet inequalities (Samuel-Cahn's median rule, $k$ -choice and posted-price variants).

Difficulty

The expected reward of the rule is not a function of the marginals of the individual $X_i$ alone in an obvious way: the event that the rule is still running when $X_i$ arrives depends on $X_1, \dots, X_{i-1}$ , and the reward is $X_\tau$ at a random index. The natural first attempt, comparing $X_\tau$ and $\max_i X_i$ pointwise, fails, since on a given outcome the rule may stop early at a value just above $T$ while the maximum comes later. The comparison has to be made between distributions, at each level $x$ , and it has to use independence to decouple "nothing accepted before time $i$ " from " $X_i > x$ ". The rest is measure-theoretic bookkeeping that is routine on paper and not routine in Lean: expressing expectations of non-negative variables as integrals of tail probabilities, splitting them at $T$ , and keeping track of integrability.

Formalization scope

Probability space. Ω with a MeasurableSpace, P : Measure Ω with [IsProbabilityMeasure P].
Variables. X : Fin n → Ω → ℝ, [NeZero n]; each X i measurable; iIndepFun X P (mutual independence); 0 ≤ X i ω for all i, ω; Integrable (maxX X) P, which is the paper's $\mathbb E[\max_i X_i] < \infty$ .
Maximum. Finset.sup' over the nonempty index set; no junk supremum.
Expectations and probabilities. Bochner integrals (∫ ω, … ∂P) and Measure.real probabilities. Tail integrals are Lebesgue integrals of $x \mapsto \Pr[\cdot > x]$ over $(T, \infty)$ and $(0, T]$ .
Weak and strict inequalities are as printed: the rule stops at $X_\tau \ge T$ , $p = \Pr[\max_i X_i \ge T]$ , tails are $\Pr[\cdot > x]$ , for $x > T$ .
The rule may accept nothing. The reward is $0$ when no value reaches $T$ ; the rule is not forced to stop at $X_n$ .

The threshold $T$ is a definition, $\mathbb E[\max_i X_i]/2$ , not a free parameter constrained by hypotheses; a formalization in which $T$ is arbitrary and the upper-tail bound is assumed would make the goal a rearrangement of its hypotheses, and is ruled out.

Infrastructure that a complete development needs, and that is welcome as separate contributions: the layer-cake formula $\mathbb E[Y] = \int_0^\infty \Pr[Y > x]\,dx$ for non-negative integrable $Y$ split at a level $T$ (Mathlib has the unsplit form, MeasureTheory.integral_eq_integral_meas_lt); measurability and integrability of the stopped reward (it is dominated by $\max_i X_i$ ); and the probability of the event "the first $i-1$ values are below $T$ and $X_i > x$ " as a product under iIndepFun.

Selected references

Robert Kleinberg and S. Matthew Weinberg, Matroid Prophet Inequalities, STOC 2012, pp. 123–136; preprint arXiv:1201.4764v1, 2012. https://arxiv.org/abs/1201.4764 (doi:10.1145/2213977.2213991)
Ulrich Krengel and Louis Sucheston, Semiamarts and finite values, Bulletin of the American Mathematical Society 83, 1977, pp. 745–747.
Ulrich Krengel and Louis Sucheston, On semiamarts, amarts, and processes with finite value, Advances in Probability and Related Topics 4, 1978, pp. 197–266.
Ester Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Annals of Probability 12(4), 1984, pp. 1213–1216. https://doi.org/10.1214/aop/1176993223

5 thms2 active usersReviewed

Missions

Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization 1: Empirical Burg-Ball DRO Bounds Cover E[h(x;ξ)] with Probability Tending to 1 − αResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Posted Price Mechanisms and Optimal Threshold Strategies for Random Arrivals I: Under Random Arrival Order, Nonadaptive Thresholds Earn a 1 − 1/e Fraction of E[max Xᵢ]Research Paper

Motivation

Setting

Formalization targets

Nonadaptive threshold guarantee

Bernoulli selection and comparison steps

Significance

Difficulty

Formalization scope

Selected references

Pricing and Matching with Forward-Looking Buyers and Sellers 1: Waiting-Adjusted Fixed Prices with Greedy Matching Earn at Least 1 − (1 + 2(b+h)T/(3(p*−w*)))/√µ* of the Fluid Profit BoundResearch Paper

Why this market matters

Market and benchmarks

Formalization targets

What the result gives

Where the argument is difficult

Formalization scope

Selected references

Persistence-Based Clustering in Riemannian Manifolds: With High Probability the Algorithm Returns as Many Clusters as the Density Has d₂-Prominent PeaksResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.8 (p. 22)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Generalized Couplings and Ergodic Rates for SPDEs and Other Markov Models: A Generalized Coupling and a Lyapunov Function Give a Unique Invariant Measure and Wasserstein Ergodic RatesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.5

Companion: Theorem 2.6

Milestones

Significance

Difficulty

Formalization scope

Selected references

Coupling and Convergence for Hamiltonian Monte Carlo 2: Lyapunov Bounds and Local Contractivity Give W_ρ(νπⁿ, ηπⁿ) ≤ e^{−cn}W_ρ(ν, η) + βⁿλⁿ⁻¹(∫ψdν + ∫ψdη)δ(C)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.11

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Tutorial on Thompson Sampling II: Under Thompson Sampling, Per-Period Expected Regret Splits into a Pessimism Term and a Width Term for Any History-Determined U_tResearch Paper

Motivation

Setting

Formalization targets

Probability matching and equation (8.4)

Per-period regret decomposition

Significance

Difficulty

Formalization scope

Selected references

Coupling and Convergence for Hamiltonian Monte Carlo 1: Exact HMC Contracts the Concave Kantorovich Distance W_ρ at Rate c = (1/10)·min(1, ½KT²(1+ℛ/T)e^{−ℛ/(2T)})·e^{−2ℛ/T}Research Paper

Why convergence bounds for Hamiltonian Monte Carlo matter

Setting

Formalization targets

Goal: Theorem 2.3

Milestones (in the order of the proof)

Companions

Significance

Difficulty

Pricing and Matching with Forward-Looking Buyers and Sellers 1: Waiting-Adjusted Fixed Prices with Greedy Matching Earn at Least 1 − (1 + 2(b+h)T/(3(p−w)))/√µ* of the Fluid Profit BoundResearch Paper