Probability

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

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.

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

1. 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)}$.
2. 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$.
3. 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}$.
4. Signal image (pp. 22–23): the signal points are sent outside that region.
5. 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.
6. 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

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.

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

1. Monotone risk (§2.1, pp. 4–5): (1) and (2) make $R$ nonincreasing on $\Lambda$.
2. 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$.
3. Failure implies a low bound at $\lambda^\dagger$ (p. 26, corrected): deterministically, $R(\hat\lambda) > \alpha$ implies $\widehat R^+(\lambda^\dagger) < \alpha$.
4. 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

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

1. 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).
2. 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$.
3. 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$.
4. Coefficient count: $\#\{I\in\mathbb N^n : |I|\le d\}=\#\{I\in\mathbb N^{n+1} : |I|=d\}=(d+n)!/(d!\,n!)$.
5. 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

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

1. $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 .$$

2. $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

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)

1. Tail bound, for every $x > T$:

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

2. 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].$$

3. The prophet's upper tail:

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

4. 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