Probability

Operations Research·Captain: mikedeng1

A Note on Probability Distributions with Increasing Generalized Failure Rates I: X Is IGFR iff log X Is IFR iff X ⪯hr λX for All λ ≥ 1 iff Φ̄(ξ/θ) Is TP₂Research Paper

Motivation

In pricing and supply-chain contracting, demand or valuations are random, and the profit functions that arise are unimodal only under a shape condition on the distribution. A firm facing demand $D(p) = \bar\Phi(p)$ at price $p$ maximizes revenue $\pi(p) = p\bar\Phi(p)$ ; the first-order condition is $\bar\Phi(p)(1 - g(p)) = 0$ , where $g$ is the generalized failure rate introduced by Lariviere and Porteus (2001). When $g$ is increasing, it crosses $1$ at most once and the optimal price is unique. The same condition makes the supplier's problem unimodal in the price-only newsvendor contract (Lariviere and Porteus, 2001) and appears throughout revenue management. The condition is useful but often hard to verify for a given distribution.

Lariviere (2006) gives three equivalent reformulations of the condition (Theorem 1), two sufficient conditions (Corollary 1), and uses them to show that every beta distribution has an increasing generalized failure rate. The parts of the equivalence had appeared separately: Keilson and Sumita (1982) showed the equivalence of parts 2 and 3, and Ma (1999) linked parts 3 and 4.

Setting

Let $X$ be a nonnegative random variable with distribution function $\Phi$ and survival function $\bar\Phi(\xi) = 1 - \Phi(\xi)$ . Assume $\Phi$ has a density $\varphi$ , and let the support of $X$ be $(\alpha,\beta)$ with $0 \le \alpha < \beta \le \infty$ . The failure rate of $X$ is $h(\xi) = \varphi(\xi)/\bar\Phi(\xi)$ , and its generalized failure rate is

g(\xi) = \xi\,h(\xi).

$X$ is IFR if $h$ is weakly increasing on $\{\xi : \Phi(\xi) < 1\}$ , and IGFR if $g$ is weakly increasing on that set. Every IFR variable is IGFR; many variables with decreasing failure rate are IGFR as well.

Write $X_L = \log X$ , with distribution $\Phi_L$ , density $\varphi_L$ , survival $\bar\Phi_L$ and failure rate $h_L$ . Two nonnegative variables with failure rates $h_1, h_2$ are ordered in the hazard rate order, $X_1 \preceq_{hr} X_2$ , if $h_1(\xi) \ge h_2(\xi)$ for all $\xi \ge 0$ . A function $f(x,y)$ is totally positive of order 2 (TP₂) if

f(x_1,y_1)f(x_2,y_2) - f(x_1,y_2)f(x_2,y_1) \ge 0 \qquad\text{for } x_1 < x_2,\ y_1 < y_2 .

A function is log-concave if its logarithm is concave.

In the Lean development these are survival, failureRate, genFailureRate, IsIFR, IsIGFR, HazardRateLE and IsTP2On in the namespace LariviereIGFR.Char, and log-concavity is the platform predicate ConvexOptimization.LogConcaveOn.

Formalization targets

Goal: Theorem 1 (p. 603)

The following are equivalent:

\text{(1) } X \text{ is IGFR};\quad \text{(2) } X_L \text{ is IFR};\quad \text{(3) } X \preceq_{hr} \lambda X \text{ for all } \lambda \ge 1;\quad \text{(4) } f(\xi,\theta) = \bar\Phi(\xi/\theta) \text{ is TP}_2 .

Milestones (the clauses of the proof)

$\bar\Phi_L(\xi) = \bar\Phi(e^\xi)$ , and $\varphi_L(\xi) = e^\xi\varphi(e^\xi)$ is a density of $X_L$ .
$h_L(\xi) = g(e^\xi)$ and $h_L'(\xi) = e^\xi g'(e^\xi)$ .
Parts 1 and 2 are equivalent.
The generalized failure rate of $\lambda X$ is $g_\lambda(\xi) = g(\xi/\lambda)$ .
Parts 1 and 3 are equivalent.
A law on $\mathbb R$ is IFR if and only if $\bar\Phi(\xi - \theta)$ is TP₂ (Barlow and Proschan 1965).
$\bar\Phi_L(\xi - \theta)$ is TP₂ on $\mathbb R^2$ if and only if $\bar\Phi(\xi/\theta)$ is TP₂ on $(0,\infty)^2$ .

Companion statements

Corollary 1. If $\varphi(e^\xi)$ is log-concave, or $\xi\varphi(\xi)$ is increasing, on the support, then $X$ is IGFR.
Beta distributions. For all $a, b > 0$ the beta distribution is IGFR.
Powers (Paul 2005). If $X$ is IGFR, so is $\delta X^\nu$ for $\delta, \nu > 0$ .

Significance

Theorem 1 converts the IGFR condition into conditions with an established theory. Through part 2, every closure and comparison property of IFR distributions transfers to IGFR distributions under the logarithm: the lognormal distribution is IGFR because its logarithm is normal, and $\delta X^\nu$ inherits IGFR from $X$ . Part 3 has a direct operational reading: as a market scales up, a supplier selling to a newsvendor sells more and a service provider charges more. Part 4 places IGFR in the theory of total positivity. Corollary 1 gives density-level tests that need no closed form for $\Phi$ , which is what makes the beta family tractable.

The results are proved in the paper; none of them is formalized. A machine-checked development would supply reusable facts about image laws under $\log$ and scaling with explicit densities, the failure-rate form of the hazard rate order, and the classical Barlow–Proschan characterization of IFR distributions by total positivity, which is used well beyond this paper.

Difficulty

Parts 1 ⇔ 2 and 1 ⇔ 3 are computations once the laws of $\log X$ and $\lambda X$ and their densities are identified, but that identification is a change of variables for measures, together with a check that the transported density is again the derivative of the distribution function on the support. The substance is the Barlow–Proschan step, part 2 ⇔ 4. Monotonicity of $h_L$ is a pointwise statement about a density, while TP₂ of $\bar\Phi_L(\xi - \theta)$ is an inequality between products of tail probabilities; the bridge is log-concavity of $\bar\Phi_L$ on the support, and its extension across the endpoints of the support, where $\bar\Phi_L$ equals $1$ on one side and $0$ on the other. A naive reading that differentiates everywhere fails at those endpoints and wherever the density is changed on a null set.

Formalization scope

Laws, not random variables. $X$ is a probability measure $\mu$ on $\mathbb R$ with $\mu((-\infty,0)) = 0$ . $X_L$ is the image of $\mu$ under Real.log, and $\lambda X$ is the image under $x \mapsto \lambda x$ ; both maps are measurable, so the images are genuine probability laws. The junk value $\log 0 = 0$ is harmless because $\mu$ has no atom at $0$ .
The density version is pinned. A density is determined only up to a null set, while IFR and IGFR read it pointwise; with an arbitrary version Theorem 1 is false. Every statement assumes IsRegDensity μ φ: $\varphi \ge 0$ , $\mu$ has density $\varphi$ , $\varphi = \Phi'$ at every point of $\{0 < \Phi < 1\} = (\alpha,\beta)$ , and $\varphi = 0$ where $\Phi = 0$ . The derived densities $e^\xi\varphi(e^\xi)$ and $\varphi(\xi/\lambda)/\lambda$ are proved to be regular as well (milestones 1 and 4).
Rates are read on $\{\Phi < 1\}$ . Lean's $x/0 = 0$ would otherwise make $h$ vanish where $\bar\Phi = 0$ . The hazard rate order compares $h_1(\xi) \ge h_2(\xi)$ for $\xi \ge 0$ with $\Phi_1(\xi) < 1$ ; at the other points the paper's $h_1$ is $+\infty$ and the inequality is automatic.
Monotonicity is weak, as in the paper's "weakly increasing". Part 3 quantifies over $\lambda \ge 1$ exactly; for $\lambda < 1$ the order reverses.
Part 4's domain is $(0,\infty)^2$ : $\theta > 0$ is forced by $\xi/\theta$ , and for $\xi \le 0$ the survival is identically $1$ , so nothing is lost. The Barlow–Proschan milestone is stated for an arbitrary law on $\mathbb R$ , because $X_L$ can be negative.
No trivialization. Part 2 is about the image law of $\log X$ , never a function such as $\xi \mapsto g(e^\xi)$ written in by hand, and part 3 is about the image law of $\lambda X$ ; otherwise the equivalences would hold by definition.
Additions disclosed. Corollary 1's conditions are read on the support, where the density is positive; "increasing" is read as weakly increasing. Corollary 2 (products of IGFR variables) is not included: the page omits the independence it needs, and the existence of a regular density version for the product was not established.

Contributions welcome: the change-of-variables lemmas for Measure.map with explicit densities, the identification of $\{0 < \Phi < 1\}$ as an open interval, and the Barlow–Proschan equivalence, which is reusable for any IFR result.

Selected references

M. A. Lariviere, A note on probability distributions with increasing generalized failure rates, Operations Research 54(3):602–604, 2006. https://doi.org/10.1287/opre.1060.0282
M. A. Lariviere and E. L. Porteus, Selling to the newsvendor: an analysis of price-only contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971
R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965 (reprinted SIAM, 1996). https://doi.org/10.1137/1.9781611971194
J. Keilson and U. Sumita, Uniform stochastic ordering and related inequalities, Canadian Journal of Statistics 10(3):181–198, 1982.
S. M. Ross, Stochastic Processes, Wiley, 1983.

10 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Primal and Dual Linear Decision Rules in Stochastic and Robust Optimization 2: With Random Recourse, the SDP (3.14) Conservatively Approximates the Linear Decision Rule Problem, Exactly for l = 1Research Paper

Linear decision rules for stochastic programs with random recourse

In a one-stage stochastic program a decision maker observes a random outcome $\xi$ and then picks a decision $x(\xi)$ , subject to constraints that depend on $\xi$ , so as to minimize expected cost. The optimization variable is a whole function $x$ , and computing the optimal value is #P-hard even for a uniform distribution on the unit cube (Dyer and Stougie, 2006, cited in the paper as [16, Theorem 3.2]). A standard tractable approximation, introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried to stochastic programming by Shapiro–Nemirovski and Chen–Sim–Sun, restricts decisions to linear decision rules $x(\xi)=X\xi$ . This restriction gives an upper bound on the optimal value.

Kuhn, Wiesemann and Georghiou (2009/2011) study these approximations systematically. Their §3 treats the case where the constraint matrix itself depends on $\xi$ (random recourse). Linear decisions then produce constraints that are quadratic in $\xi$ , and the paper reformulates the resulting semi-infinite problem as a semidefinite program. This mission formalizes that reformulation, the primal half of the paper's Theorem 2.

Setting

Uncertainty is a probability measure $\mathbb P$ on $\mathbb R^k$ , with outcomes $\xi$ . The support $\Xi$ of $\mathbb P$ is the smallest closed set of probability one. It is assumed to have the form

\Xi=\{\xi\in\mathbb R^k:\ e_1^\top\xi=1,\ \ \xi^\top W_\ell\xi\ge0,\ \ell=1,\dots,l\}\qquad(3.11)

for symmetric matrices $W_1,\dots,W_l$ , where $e_1$ is the first standard basis vector. The first coordinate of every outcome is therefore $1$ , so linear functions of $\xi$ are affine functions of the remaining coordinates. $\Xi$ is assumed nonempty and bounded, and its linear hull is assumed to be $\mathbb R^k$ . Let $\mathbb S$ denote the symmetric $k\times k$ matrices and $M=\mathbb E(\xi\xi^\top)$ the second-moment matrix.

The data are $C\in\mathbb R^{n\times k}$ (cost $c(\xi)=C\xi$ ), $B\in\mathbb R^{m\times k}$ (right-hand side $b(\xi)=B\xi$ , with rows $b_\mu^\top$ ), and $A_1,\dots,A_m\in\mathbb R^{k\times n}$ , where the $\mu$ th row of the recourse matrix $A(\xi)$ is $\xi^\top A_\mu$ . The stochastic program $\mathcal{SP}$ minimizes $\mathbb E(c(\xi)^\top x(\xi))$ over square-integrable $x$ subject to $A(\xi)x(\xi)\le b(\xi)$ almost surely. It is strictly feasible if some square-integrable $\bar x,\bar s$ and some $\varepsilon>0$ satisfy $A(\xi)\bar x(\xi)+\bar s(\xi)=b(\xi)$ and $\bar s(\xi)\ge\varepsilon e$ almost surely.

With linear decisions $X\xi$ and quadratic slacks $\xi^\top S_\mu\xi$ , $S_\mu\in\mathbb S$ , one obtains the primal approximation

\mathcal{SP}^u:\quad \min\ \operatorname{Tr}(MC^\top X)\ \ \text{s.t.}\ \ \xi^\top A_\mu X\xi+\xi^\top S_\mu\xi=b_\mu^\top\xi,\ \ \xi^\top S_\mu\xi\ge0\ \ \mathbb P\text{-a.s.},\ \mu=1,\dots,m,

and the SDP (3.14)

\min\ \operatorname{Tr}(MC^\top X)\ \ \text{s.t.}\ \ \tfrac12(A_\mu X+X^\top A_\mu^\top)+S_\mu=\tfrac12(e_1b_\mu^\top+b_\mu e_1^\top),\ \ S_\mu-\textstyle\sum_\ell\Lambda_{\mu\ell}W_\ell\succeq0,\ \ \Lambda\ge0 .

Formalization targets

Goal: Theorem 2, primal half (p. 17)

\operatorname{Feas}(3.14)\ \text{projects into}\ \operatorname{Feas}\mathcal{SP}^u,\qquad \operatorname{val}\mathcal{SP}^u\le\operatorname{val}(3.14),

l=1\ \text{and}\ \mathcal{SP}\ \text{strictly feasible}\ \Longrightarrow\ \operatorname{val}\mathcal{SP}^u=\operatorname{val}(3.14).

Milestones

§3.2, (3.13), p. 12. The $\mu$ th equality constraint of $\mathcal{SP}^u$ holds almost surely if and only if $H_\mu:=\tfrac12(A_\mu X+X^\top A_\mu^\top-e_1b_\mu^\top-b_\mu e_1^\top)+S_\mu=0$ .
Lemma 1 (S-lemma), p. 12. If $\bar\xi^\top W\bar\xi>0$ for some $\bar\xi$ , then $[\xi^\top W\xi\ge0\Rightarrow\xi^\top S\xi\ge0]\iff\exists\lambda\ge0:\ S\succeq\lambda W$ . This is linked to the platform's proved S-procedure, of which it is the homogeneous case.
Proposition 6, p. 12. For symmetric $S$ : $\exists\lambda\ge0$ with $S-\sum_\ell\lambda_\ell W_\ell\succeq0$ implies $\xi^\top S\xi\ge0$ almost surely, and the converse holds when $l=1$ .

Significance

The theorem replaces a problem with infinitely many constraints, one per outcome, by a semidefinite program with $O(mk^2+ml)$ variables. Its value is always an upper bound on $\mathcal{SP}^u$ , and hence on $\mathcal{SP}$ . When the support is a single ellipsoid in the hyperplane $e_1^\top\xi=1$ ( $l=1$ ), the bound loses nothing beyond the restriction to linear decisions. For $l>1$ the gap is unavoidable in general: an exact tractable reformulation would decide copositivity, which is NP-hard (Remark 7). Random recourse arises whenever technology or yield coefficients are uncertain, for example in production planning and portfolio problems with uncertain returns.

The result is proved in the paper. As far as is known it has no machine-checked proof. A formalization adds a precise statement of the hypotheses. Writing those hypotheses out showed that the unnumbered §3.2 step needs $\Xi$ to have dimension $k-1$ , which spanning alone does not give for nonconvex $\Xi$ (see Formalization scope). The other half of Theorem 2, about the lower-bounding SDP (3.18), is false in this preprint and is not part of the mission.

Difficulty

The semi-infinite constraints hold only $\mathbb P$ -almost surely. The first step is to pass from "almost surely" to "for every $\xi\in\Xi$ ", which uses that $\Xi$ is exactly the support and that the constraint functions are continuous. A bound $\mathbb P(\Xi)=1$ alone is not enough. For the equality constraints, a quadratic form that vanishes on $\Xi$ must vanish identically. This requires $\Xi$ to be large enough, and the obvious argument from " $\Xi$ spans $\mathbb R^k$ " fails when $\Xi$ is a finite set. For the inequality constraints with $l=1$ , the implication $\xi^\top W_1\xi\ge0\Rightarrow\xi^\top S\xi\ge0$ must be established on all of $\mathbb R^k$ and not only on the slice $e_1^\top\xi=1$ . Doing so needs boundedness of $\Xi$ (no recession directions) and a strictly feasible point for the S-lemma. The S-lemma itself is a nonconvex duality statement. It is available on the platform.

Formalization scope

Outcomes live in Fin k → ℝ, with $k\ge1$ carried in the setting. Indices are 0-based: $\xi_1$ is coordinate 0, and $\mu,\ell$ range over Fin m, Fin l. " $\Xi$ is the support of $\mathbb P$ " is stated as: $\Xi$ is closed, $\mathbb P(\Xi^{\mathrm c})=0$ , and every ball centred in $\Xi$ has positive measure. Mathlib has no Measure.support at this revision. The standing assumptions (probability measure, symmetric $W_\ell$ , support, nonempty, bounded, spanning) form one predicate assumed by every theorem. Decision rules are Borel measurable square-integrable functions. Optimal values are infima in EReal, $+\infty$ for an empty feasible set and $-\infty$ for an unbounded one. "Equivalent" means equal optimal values. Each $S_\mu$ is required symmetric in both problems; $\succeq$ is positive semidefiniteness and $\Lambda\ge0$ is componentwise. Strict feasibility of $\mathcal{SP}$ in §3 is the paper's condition (2.9) of §2 with $A$ replaced by $A(\xi)$ . The paper uses the phrase without restating it.

Repairs and narrowings:

Only the clauses of Theorem 2 about (3.14) and $\mathcal{SP}^u$ are stated. The clauses about (3.18) and $\mathcal{SP}^l$ are false in this preprint: a strictly feasible instance with $l=1$ has $\operatorname{val}(3.18)\approx1.170>\ln3=\operatorname{val}\mathcal{SP}$ . Propositions 7–9 serve only that half and are not included. "Polynomial size, efficiently solvable" is informal and omitted.
The §3.2 milestone carries the extra hypothesis that $\Xi$ contains a relatively open piece of the hyperplane $e_1^\top\xi=1$ (the paper's "dimension $k-1$ ", p. 10). Without it the claim is false for $l\ge2$ . For $l=1$ the hypothesis follows from the standing assumptions, so the goal is unaffected.
Strict feasibility is kept in the $l=1$ clause as printed, although the argument does not use it.

The goal cannot be trivialized through its definitions. Feasibility is quantified $\mathbb P$ -almost surely for a measure whose support is $\Xi$ , not over an empty or arbitrary set. Both optimal values are infima of the same real objective over the problems' own feasible sets. The standing assumptions are satisfiable, for instance by $k=2$ , $W_1=\operatorname{diag}(1,-1)$ , and $\mathbb P$ the uniform law on $\{1\}\times[-1,1]$ .

The definitions (support of a measure, $\mathcal L^2$ decision rules, the random-recourse data) are reusable for the other sections of the paper and for related work on decision rules. Proofs of any milestone, Lean lemmas on quadratic forms vanishing on open cones, and an almost-sure-to-support transfer lemma are welcome.

Selected references

D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Optimization Online 2009/02/2218 (2009); Math. Program. 130 (2011) 177–209. https://optimization-online.org/wp-content/uploads/2009/02/2218.pdf, https://doi.org/10.1007/s10107-009-0331-4
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM Studies in Applied Mathematics 15, 1994 (the paper's source for Lemma 1). https://doi.org/10.1137/1.9781611970777
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, Appendix B (the S-procedure as stated on the platform). https://web.stanford.edu/~boyd/cvxbook/
I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007) 371–418. https://doi.org/10.1137/S003614450444614X
M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Math. Program. 106 (2006) 423–432. https://doi.org/10.1007/s10107-005-0597-0

7 thms2 active usersReviewed

Machine Learning Random Matrix Theory Statistics·Captain: mikedeng1

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

Motivation

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

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

Setting

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

The matrix completion basis is

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

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

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

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

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

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

The stochastic error is the random matrix

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

Formalization targets

Goal: Theorem 4

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

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

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

12 thms2 active usersReviewed

Completed

Functional Analysis·Captain: marwahaha

Independent products in real L1: asymptotic midpoint convexity without AUC renormingsOpen Problem

Motivation

Independent positive multipliers on a branching tree generate concrete subspaces of real L1. Their asymptotic geometry can distinguish midpoint estimates from AUC renormability. The pinned manuscript supplies the research context.

Setting

A nonconstant positive multiplier has probability law μ, mean one and finite second moment. Path products are multiplied along nonempty prefixes, and their L1 classes generate a closed real span.

Formalization target

The selected goal is OAI.IndependentProducts.main_general. Its central assertion is

\dim\operatorname{productSpan}(\mu)=\infty,\qquad\neg\exists\text{ equivalent AUC norm}.

The theorem states that, for any Borel measure μ on ℝ satisfying the multiplier hypotheses, the closed real L¹ span of the path products is infinite-dimensional, and no equivalent norm on it is AUC. The hypotheses say that μ is a probability measure, almost every value is positive, μ is not almost surely equal to any constant, its mean is 1, and the identity function has a finite second moment (is in L²). Vertices are finite lists of positive integers, a sample assigns a real number to each nonroot vertex, and the product measure is the infinite product of independent copies of μ, one per nonroot vertex. The path product of a vertex v multiplies the sample values at the nonempty prefixes of v, and is 1 for the root. productSpan(μ) is the topological closure, in L¹ of the product measure, of the real linear span of the classes equal almost everywhere to some path product. The theorem concludes first that productSpan(μ) is not finite-dimensional over ℝ. Second, for every seminorm N on productSpan(μ) that is an equivalent norm, meaning there are constants 0<a≤b with a‖x‖≤N(x)≤b‖x‖ for all x, N fails the AUC property, which requires that, for every t>0, the one-sided asymptotic modulus of N at t is strictly positive. That modulus is the infimum over N-unit vectors x of the supremum over closed finite-codimension subspaces F of the infimum of N(x+ty)−1 over y in F with N(y)=1. The statement is given as an admitted theorem without proof.

Significance and status

The selected general target asserts infinite dimension and absence of AUC renormings. Specific exponential and Gaussian-square midpoint estimates are separate published targets, retained as additional references. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The obstruction must work for every admissible multiplier distribution and every equivalent norm, rather than only a particular exponential example.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

OAI.IndependentProducts.main_exponential (Open).
OAI.IndependentProducts.main_gaussian_12 (Open).
OAI.IndependentProducts.main_gaussian_24 (Open).

Selected references

OpenAI, Independent products in real L1: asymptotic midpoint convexity without AUC renormings, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

35 thms2 active usersReviewed

Completed

Quantum Information·Captain: marwahaha

Threshold parallel repetition for finite-dimensional entangled gamesOpen Problem

Motivation

Parallel repetition is useful for amplifying errors in nonlocal games, but a joint entangled strategy can correlate outcomes across repetitions. Independence of the sampled questions does not imply independence of wins. The pinned manuscript supplies the research context.

Setting

A finite two-player game has a probability distribution on question pairs and a Boolean acceptance predicate. Its entangled value is a supremum over finite-dimensional states and local positive-operator measurements.

Formalization target

The selected goal is OAI.ThresholdParallelRepetition.threshold_parallel_repetition. Its central assertion is

P\{W_k\geq\lceil(v+\delta)k\rceil\}\leq\exp\!\left(-\kappa_0\frac{\delta^{13}k}{1+\log(|A||B|)}\right).

The theorem states that there is a universal constant κ₀>0 such that the following holds for every two-player nonlocal game G with question sets of sizes x+1 and y+1 and answer sets of sizes a+1 and b+1, given by a probability distribution on question pairs and a Boolean acceptance predicate on questions and answers, whose entangled value is strictly less than 1. Here the entangled value is the supremum of the winning probability over finite-dimensional entangled strategies, which consist of a unit state on a bipartite space, positive semidefinite measurement operators for Alice and Bob summing to the identity for each question, with answer probabilities given by the Born rule. For every δ with 0<δ<1−entangledValue(G) and every number of repetitions k≥1, consider k-fold parallel repetition, where k independent question pairs are drawn from G's distribution and the players answer all coordinates at once. The threshold probability of a repeated entangled strategy S is the probability that the number of coordinates won is at least ⌈(entangledValue(G)+δ)k⌉. The theorem asserts that this probability is at most exp(−κ₀ δ¹³ k /(1+ln((a+1)(b+1)))) for every repeated strategy S, and that the threshold value, defined as the supremum of the threshold probability over all repeated strategies, satisfies the same bound. The statement is admitted without proof in the source.

Significance and status

The selected published Lean exponent is δ^13, not the manuscript abstract's δ^5 or its distribution-dependent cubic rate. Both every-strategy and supremum conclusions are included. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The estimate must hold uniformly over finite dimensions and collective strategies. Taking the supremum cannot assume that an optimal strategy exists.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

OpenAI, Threshold parallel repetition for finite-dimensional entangled games, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

2 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: marwahaha

Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive DisorderOpen Problem

Motivation

Random site energies change the spectral behavior of a lattice Schrödinger operator. Identifying its almost-sure spectrum is one part of the planar Anderson problem. The pinned manuscript supplies the research context.

Setting

The lattice is the integer plane. A state is a square-summable complex function on its sites, and the potential at each site is independently uniform on the interval from −h to h, with h positive.

Formalization target

The selected goal is OAI.PlanarAnderson.anderson_spectrum_ae. Its central assertion is

\sigma(H_v)=[-4-h,4+h].

The theorem states that for every real h>0, for almost every disorder configuration v under disorderLaw(h), there exists a bounded complex-linear operator H on the Hilbert space ℓ²(ℤ², ℂ) of square-summable complex functions on the planar lattice ℤ×ℤ such that H is an Anderson operator for v, H is self-adjoint, and the spectrum of H in ℂ equals the real interval [-4-h, 4+h] (embedded in ℂ as the points with imaginary part 0). Here a configuration is a real-valued function v on lattice sites, and disorderLaw(h) is the infinite product measure over sites of the uniform distribution (Lebesgue measure conditioned on the interval) on [-h,h], so the potential values are independent. H is an Anderson operator for v when, for every u in ℓ² and every site x=(a,b), (Hu)(a,b) = u(a+1,b)+u(a-1,b)+u(a,b+1)+u(a,b-1)+v(a,b)u(a,b), the sum of the four nearest-neighbour values plus the local potential times u at x. The statement is recorded as an admitted theorem.

Significance and status

The selected goal asserts existence, self-adjointness and the spectrum interval. Pure-point spectral type, a complete eigenbasis and dynamical localization are not conclusions of this published target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The interval must be identified almost surely for an infinite random operator, including both exclusion of spectrum outside the interval and inclusion of its interior.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

OpenAI, Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

2 thms2 active usersReviewed

Completed

Representation Theory·Captain: marwahaha

Optimal-order mixing of the Thorp shuffleOpen Problem

Motivation

The full permutation of a deck can remain far from uniform after each individual card is nearly uniform. The source analyzes Thorp mixing through representation estimates; the available goal isolates a reciprocal-dimension estimate and its Fourier consequence. The source is OpenAI's September 2026 manuscript.

Setting

A Specht module is a complex representation of a symmetric group associated with a partition. Sum the reciprocals of these dimensions over all partitions of $n$ , and let $C_1$ be the supremum of these sums for positive $n$ . A permutation distribution is compared with uniform through its averaged action on an irreducible representation.

Formalization targets

\sup_{n\ge1}\sum_{\lambda\vdash n}\frac1{\dim S^\lambda}<\infty,\qquad\|\widehat\nu(\rho)\|\le\sqrt{32C_1}(\dim\rho)^{-5/16}.

A conjunction of two parts. First, for each n let reciprocalFirst(n) be the sum, over all partitions p of n, of 1/deg(p), where deg(p) is the complex dimension of the Specht module of shape p (the span of the permutation-group translates of the polytabloid built from the canonical tableau, inside the space of tabloids). Let C1 be the supremum of reciprocalFirst(n) over n ≥ 1. The theorem asserts that this set of values is bounded above, that reciprocalFirst(n) ≤ C1 for every n ≥ 1, and that exceptionalFirst(n) tends to 0 as n → ∞, where exceptionalFirst(n) is the same sum of 1/deg(p) restricted to partitions p whose defect n − max(first row length, first column length) is positive. Second, for every d ≥ 3, every bijection e between the set of positions {0,1}^d (functions Fin d → Bool) and Fin 8 × Fin(2^(d−3)), every finite-dimensional complex inner product space E, and every irreducible complex representation ρ of the symmetric group on the positions, acting on E by inner-product-preserving maps, the following holds. Let ν be a probability distribution on this symmetric group (nonnegative values summing to 1) such that, for each i in Fin 8 and each group element g, the total ν-mass of the coset g·B_i is at most 4·|Sym(2^(d−3))|/|Sym(positions)|, where B_i is the subgroup of permutations that act through e by an arbitrary permutation of the i-th block of 2^(d−3) points and fix all other points. Then the operator norm of Σ_g ν(g)ρ(g) is at most √(32·C1)·(dim E)^(−5/16).

The goal is OAI.Thorp.Current.first_reciprocal_main.

Significance

The goal also proves that the reciprocal sum over shapes of positive defect tends to zero. The Fourier bound applies to distributions satisfying the specified eight-block coset-mass condition. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

One-card mixing does not control high-dimensional permutation representations. The bound must account for small-dimensional exceptional shapes and quantify contraction in every admissible irreducible representation.

Formalization scope

The Fourier clause has $d\ge3$ , positions on a $d$ -bit cube, a bijection into eight equal blocks, and unitary irreducible complex representations. Its coset-mass hypothesis is retained exactly. The target is a supporting representation estimate, not the paper’s final $1600d$ -shuffle total-variation theorem.

The shared definitions are supplied by ThorpFirstReciprocal. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

OpenAI, Optimal-order mixing of the Thorp shuffle, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

40 thms2 active usersReviewed

Completed

Combinatorics·Captain: marwahaha

Renewal and changes of law for critical honeycomb walksOpen Problem

Motivation

An external force rewards self-avoiding walks whose endpoints move in a chosen direction. The source studies critical honeycomb scaling; the available formal goal supplies existence of the forced free-energy limit. The source is OpenAI's September 2026 manuscript.

Setting

For an $n$ -step self-avoiding walk, the endpoint displacement is embedded in the complex plane. Its projection onto $e$ is the real part of $\overline e$ times that displacement. The partition sum weights the walk by critical activity to the $n$ th power and an exponential force reward.

Formalization targets

\frac1n\log\!\sum_{\gamma\in\operatorname{SAW}_n(o)}\rho^n e^{s\operatorname{Re}(\overline e\,\Delta\gamma)}\longrightarrow F(o,e,s),\qquad\rho=(2+\sqrt2)^{-1/2}.

For every starting vertex o of the honeycomb lattice, every complex number e and every real number s, the sequence logPartition(o,e,s)(n) converges as n tends to infinity to freeEnergy(o,e,s). Here vertices are triangular-up or triangular-down sites labeled by integer column and row, each up vertex being adjacent to three down vertices and vice versa, with planar positions given in the complex plane. saws(o,n) is the set of self-avoiding walks of n steps from o, meaning vertex lists with no repetition. For such a walk γ, its displacement is the position of its endpoint minus the position of o, and its projection onto e is the real part of conj(e) times the displacement. The partition function is the sum over γ in saws(o,n) of ρ^n exp(s times that projection), with ρ = 1/√(2+√2). logPartition is log of this partition function divided by n, and freeEnergy is defined as the limit of logPartition at infinity, using Lean's limUnder convention. The statement therefore asserts that this limit exists and equals freeEnergy; it is a stated theorem whose proof is admitted in the source.

The goal is OAI.HoneycombForce.logPartition_tendsto.

Significance

The conclusion makes the defined free energy an actual convergent limit for every starting point, direction parameter, and real force. It establishes the thermodynamic quantity underlying later asymptotic questions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Finite sums at each length do not guarantee convergence after normalization. Self-avoidance couples concatenated pieces, so ordinary independent-product arguments are unavailable without additional work.

Formalization scope

The target allows any complex $e$ and real $s$ , without a unit-direction restriction. Length counts steps, and walk lists contain $n+1$ distinct vertices. The spatial exponent, thermal laws, and small-force exponent from the manuscript are not attached conclusions.

The shared definitions are supplied by HoneycombFreeEnergy. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

OpenAI, Renewal and changes of law for critical honeycomb walks, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

4 thms2 active usersReviewed

Completed

Information Theory·Captain: marwahaha

The exact reconstruction threshold for the three-state symmetric channelOpen Problem

Motivation

Broadcasting a label through noisy tree edges models how information decays with distance. The source studies when observations far from the root retain information about its three-state label. The source is OpenAI's September 2026 manuscript.

Setting

The symmetric channel preserves the input with probability $(1+2\lambda)/3$ and sends it to each other state with probability $(1-\lambda)/3$ . Reconstruction advantage is the expected total variation between the posterior root law and the uniform prior.

Formalization targets

b\ge2,\quad-1/2\le\lambda\le1,\quad b\lambda^2>1\quad\Longrightarrow\quad\operatorname{Advantage}_n\to L>0.

For every natural number b ≥ 2 and every real λ that is admissible, meaning −1/2 ≤ λ ≤ 1, if b·λ² > 1 then the sequence of regular-tree advantages reconstructs. Here a three-state spin (an element of Fin 3) is passed through a symmetric channel that keeps the spin with probability (1+2λ)/3 and moves to each other spin with probability (1−λ)/3. The observation at depth 0 is the root spin, and the observation at depth n+1 is a multiset of depth-n observations, one for each of the offspring of the root, where the offspring count is the constant b (the regular case) and each child spin is obtained by passing the parent spin through the channel and then observed recursively. With a uniformly random root spin, the posterior of each spin given an observation is its conditional probability, defaulting to 1/3 when the observation has probability zero. The advantage of a family of laws indexed by the root spin is the sum over observations y of the marginal probability of y times half the sum over spins i of |posterior(y,i) − 1/3|. The regular advantage at depth n is this advantage for the regular b-ary observation law. Reconstructs means that this sequence in n converges to some limit L > 0. The statement is an admitted theorem, with its proof left as sorry.

The goal is OAI.ThreeState.regular_supercritical. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

Significance

The selected goal is the regular-tree supercritical direction. Supporting published targets give Poisson reconstruction and equivalent supercritical formulations in a second definition group. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The observation contains the full nested collection of descendants, and the posterior depends on correlated information inherited from their common ancestor. A single root-to-leaf correlation is insufficient to describe reconstruction.

Formalization scope

Observations are nested multisets with a uniform three-state root. The attached targets establish reconstruction above the displayed threshold; non-reconstruction at or below equality and stochastic-block-model recovery are outside this draft’s formal scope.

The shared definitions are supplied by ThreeStateSupercritical, ThreeStateTreeClauses. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

OpenAI, The exact reconstruction threshold for the three-state symmetric channel, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

21 thms2 active usersReviewed

Stochastic Systems·Captain: marwahaha

Directional transience implies ballisticityOpen Problem

Motivation

Escape to infinity can be arbitrarily slow for a general stochastic process. The source asks whether independent uniformly elliptic lattice environments force a positive deterministic speed whenever a direction is transient. The source is OpenAI's September 2026 manuscript.

Setting

Uniform ellipticity provides one positive lower bound for all step probabilities, almost surely at every site. Directional transience means the position projected onto a fixed unit vector tends to positive infinity almost surely under the law averaging environment and walk.

Formalization targets

\langle X_n,\ell\rangle\to+\infty\ \text{a.s.}\quad\Longrightarrow\quad\exists v:\ X_n/n\to v\ \text{a.s.},\quad\langle v,\ell\rangle>0.

The theorem (admitted, not proved here) states that, for every dimension d ≥ 2 and every Borel probability measure ν on the set of transition rows (a row is a probability vector p over the 2d nearest-neighbour directions ±e_i of ℤ^d, with entries nonnegative and summing to 1), the following holds. Suppose ν is uniformly elliptic, meaning there is κ > 0 with p(e) ≥ κ for every direction e, for ν-almost every row p. Let ℓ be a unit vector in ℝ^d (ℓ·ℓ = 1), and suppose the walk is directionally transient in direction ℓ. Here the environment assigns to each site of ℤ^d an independent ν-distributed row, the walk starts at the origin and at each step moves from its current site x in direction e with probability given by the row at x, and the annealed law averages over the environment and the walk. Directional transience means that, almost surely under this annealed law, the inner product of the walk position X_n with ℓ tends to +∞ as n → ∞. The conclusion is that there exists a vector v ∈ ℝ^d with v·ℓ > 0 such that the walk has asymptotic velocity v, that is, X_n/n → v as n → ∞ almost surely under the annealed law. In other words, directional transience of an i.i.d. uniformly elliptic random walk in random environment in dimension at least two implies ballisticity with a nonzero velocity having positive component along ℓ.

The goal is OAI.DirectionalTransience.directional_transience_implies_ballisticity. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

positive probability transience velocity hemisphere.

Significance

The chosen central target converts almost-sure transience to a velocity statement in every dimension at least two. The separate dimension-at-least-three statement starts from positive probability and identifies the transient hemisphere. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Transience controls eventual direction but not the time spent in traps. A law of large numbers with positive projected velocity needs quantitative control of these delays.

Formalization scope

The main statement assumes $d\ge2$ , a unit direction, and an independent identically distributed uniformly elliptic environment. The supporting hemisphere target assumes $d\ge3$ and a nonzero direction. Their original definition groups stay separate.

The shared definitions are supplied by DirectionalBallisticity, VelocityHemisphere. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

OpenAI, Directional transience implies ballisticity, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

6 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: marwahaha

Buffered comparison and stopping-band resolution in critical IsingOpen Problem

Motivation

Conditioning on an explored Ising interface fixes many spins and can create alternating signs. The source develops comparison estimates that remain valid with arbitrary common pinned spins. The source is OpenAI's September 2026 manuscript.

Setting

A ferromagnetic Ising law weights sign configurations by the exponential of nonnegative pair couplings plus real external fields. Two probability mixtures prescribe source spins on $J$ , while the same spins are pinned on $F$ and a target event is prescribed on $I$ .

Formalization targets

e^{-4\operatorname{artanh}q_0}\le\frac{\mu_{\mathrm{mix}}(\sigma_I=a\mid\sigma_F=\tau)}{\mu_{\mathrm{mix}'}(\\sigma_I=a\\mid\\sigma_F=\\tau)}\\le e^{4\\operatorname{artanh}q_0}.

A comparison bound for a ferromagnetic Ising model on a finite graph with n vertices and m separately indexed edges (parallel edges allowed, no loops, nonnegative couplings K_e) and an arbitrary real external field h. A configuration σ has energy equal to the sum over edges of K_e σ_u σ_v plus the sum over vertices of h_v σ_v, with spins ±1, and weight exp(energy). Take pairwise disjoint vertex sets I, J, F, and kept vertices i ∈ I and j ∈ J that lie outside F. Fix spin configurations a and τ. For a configuration b, the conditional probability of σ_I = a given σ_J = b and σ_F = τ is the ratio of the total weight of configurations satisfying all three agreements to the total weight of those agreeing with b on J and τ on F. For any two probability mixtures mix and mix' on configurations (nonnegative weights summing to 1), the mixture probability is the mix-weighted average of these conditional probabilities over b; only the restriction of b to J matters. Let q be the terminal connection probability in the zero-field random-cluster (FK) model with q=2 on the graph with F deleted (not pinned): edges e are open with probability 1-exp(-2K_e), the vertices of I are identified together and those of J are identified together, and q is the probability that i and j lie in the same cluster. Then the ratio of the mixture probability under mix to that under mix' lies between exp(-4 artanh q) and exp(4 artanh q), for every such pair of mixtures, uniformly in h, a and τ. The theorem is stated with its proof admitted (sorry).

The goal is OAI.BufferedIsing.finite_graph_comparison.

Significance

The estimate controls likelihood ratios uniformly over mixtures, fields, and common signs. It is the finite-graph comparison component of the manuscript. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Pinning a vertex changes neighboring fields; deleting it does something different. The comparison probability must come from the graph with the common pins deleted, with each terminal class contracted separately.

Formalization scope

The graph is finite with indexed edges, allowing parallel edges and excluding loops before contraction. The sets $I,J,F$ are pairwise disjoint and each terminal class contains a supplied vertex. The zero-field random-cluster weight has cluster parameter two. The stopping-band approximation theorem is not an attached target.

The shared definitions are supplied by BufferedIsing. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

OpenAI, Buffered comparison and stopping-band resolution in critical Ising, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

28 thms2 active usersReviewed

Completed

Group Theory Representation Theory·Captain: wurtle

From partial permutation information to Fourier boundsResearch Paper

Motivation: when do partial observations of a permutation force full randomness?

Many random permutations are analysed through what they do to a few labels at a time: the joint positions of $k$ chosen cards in a shuffle, or the images of a list of inputs under a block cipher built from a shuffle. Such partial information does not by itself control the whole permutation. The uniform law on the alternating group already has uniform images on every set of at most $n-2$ labels, yet it is at total-variation distance $1/2$ from uniform on $S_n$ . Converting partial-permutation estimates into full-permutation estimates therefore needs an additional argument, and this is the bottleneck in recent work on the Thorp shuffle, where fixed fractions of the deck were known to randomize quickly (Czumaj–Vöcking 2014; Czumaj 2015) long before the full deck was.

Timeline

1954 — Frame, Robinson and Thrall prove the hook-length formula for the degrees of irreducible representations of $S_n$ (Canad. J. Math. 1954).
1981 — Diaconis and Shahshahani analyse random transpositions by Fourier analysis on $S_n$ , establishing the upper-bound-lemma framework (Z. Wahrsch. 1981).
2004 — Liebeck and Shalev show that the Witten zeta sums $\sum_{\lambda\vdash n}(f^\lambda)^{-u}$ tend to $2$ for every fixed $u>0$ (J. Algebra 2004).
2009, 2013 — Morris uses entropy and trajectory comparison to prove $O((\log n)^4)$ and $O((\log n)^3)$ mixing bounds for the Thorp shuffle (Ann. Probab. 2009; CPC 2013).
2014–2015 — Czumaj and Vöcking show that a fixed fraction of the cards randomizes in $O((\log n)^2)$ layers; Czumaj obtains full-permutation sampling by recursively applying partial randomizers on shrinking sets.
2026 — The OpenAI preprint From partial permutation information to Fourier bounds (OpenAI Math Release, September 26, 2026) proves that coset caps for complementary blocks control every Fourier matrix (Theorem 1.1). It has not been peer reviewed.

Setting

Let $X$ be a finite set of $n$ labels and $G=\mathrm{Sym}(X)$ , acting as maps from initial labels to final positions. For $M\subseteq X$ , let $H_M\le G$ be the block subgroup of permutations that fix every label outside $M$ . Two permutations have the same images on $X\setminus M$ exactly when they lie in the same left coset $gH_M$ , so a bound on the law of those images is a bound on coset masses.

For a nonnegative weight $f$ on $G$ and a unitary representation $\rho$ of $G$ on a finite-dimensional complex inner-product space $V$ , the Fourier transform is $\widehat f(\rho)=\sum_{g\in G}f(g)\rho(g)$ , with $D=\dim V$ . The Hilbert–Schmidt norm is unnormalized, $\|A\|_{\mathrm{HS}}^2=\operatorname{tr}(A^*A)$ . For $u>0$ the symmetric degree constant is

C_u=\sup_{m\ge1}\ \sum_{\lambda\vdash m} D_\lambda^{-u},

where $D_\lambda$ ranges over the degrees of the irreducible complex representations of $S_m$ .

Formalization targets

Goal: complementary cosets control Fourier matrices (Theorem 1.1)

Partition $X$ into $b\ge1$ nonempty blocks $M_1,\dots,M_b$ and put $H_i=H_{M_i}$ . Let $f\ge0$ on $G$ have total mass at most one and satisfy

f(gH_i)\le \frac{B}{[G:H_i]}\qquad(g\in G,\ 1\le i\le b).

Then for every $u>0$ and every irreducible unitary $\rho$ of degree $D$ ,

\|\widehat f(\rho)\|_{\mathrm{HS}}^2\le b\,B\,C_u\,D^{-1+(u+2)/b} \qquad\text{and}\qquad \|\widehat f(\rho)\|_{\mathrm{op}}^2\le b\,B\,C_u\,D^{-1+(u+2)/b}.

No restriction is placed on the block sizes or on multiplicities in the restriction of $\rho$ to $H_1\times\dots\times H_b$ . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Theorem 1.1 is a quantitative transfer principle: a single law whose complementary partial images are never much heavier than uniform has a power saving in every irreducible representation of $S_n$ . With $b=8$ and $u=1$ it gives $\|\widehat f(\rho)\|_{\mathrm{HS}}^2\le 8C_1D^{-5/8}$ , which is enough for the principal application in the source (Corollary 3.6, p. 9): if the images of a uniformly chosen set of $7n/8$ labels are close to uniform in average total variation and the sign mean tends to zero, then the product of just two independent copies of the permutation converges to uniform. This is the step used by the companion Thorp-shuffle preprints to turn fixed-list estimates into full-deck mixing in $O(\log n)$ shuffles. The statement concerns arbitrary laws on $S_n$ and does not depend on any shuffle.

Formalizing it. The theorem is a finite inequality with explicit constants, so it is a natural target for machine checking. A proof would certify the partial-to-full transfer used by the Thorp mixing arguments, and would require reusable infrastructure: isotypic decompositions of restrictions to products of subgroups, Schur averaging, Hilbert–Schmidt and operator norms of group-algebra elements, and uniform bounds on symmetric-group Witten zeta sums. None of this is formalized yet.

Difficulty

The natural approach decomposes $\rho$ restricted to $H_1\times\dots\times H_b$ into tensor products of irreducibles of the blocks and bounds $\widehat f(\rho)$ on each piece. This fails when a block type occurs with large multiplicity: a dimension count that pays for every copy gives no decay in $D$ . The bound must count each irreducible type of a block subgroup once, regardless of multiplicity, and must hold uniformly over all block sizes, which is why the constant $C_u$ is a supremum over every symmetric group. The Hilbert–Schmidt bound is harder than the operator bound, because it must control the whole Fourier matrix rather than its action on one vector.

Formalization scope

$X$ is an arbitrary Fintype with decidable equality; blocks are M : Fin b → Set X, nonempty, pairwise disjoint and covering. The block subgroup is blockSubgroup (M i), the permutations fixing each point outside M i.
The coset cap is LeftCosetCap f H B: for every $g$ , $\sum_{h\in H}f(gh)\le B/[G:H]$ , with the index H.index.
$\rho$ is any irreducible representation on a finite-dimensional complex inner-product space with $\langle\rho(g)x,\rho(g)y\rangle=\langle x,y\rangle$ ; the Fourier transform is complexFourier ρ f; hsNormSq is $\operatorname{Re}\operatorname{tr}(A^*A)$ ; the operator norm is that of the associated continuous linear map; $D$ is Module.finrank ℂ V and the exponent is a real power.
Irreducible representations of $S_m$ are indexed by the isotypic components of the regular representation of Equiv.Perm (Fin m), and $C_u$ is symmetricDegreeConstant u, an sSup over $m\ge1$ . The supremum is finite for every $u>0$ ; a solver must prove this boundedness, since sSup of an unbounded real set would be $0$ .
Needed infrastructure: isotypic decomposition and Schur's lemma for finite groups, degree bounds for $S_m$ (hook-length or tableau counting), and uniform Witten zeta bounds. The degree layer is reusable for any random walk on $S_n$ .

Selected references

J. S. Frame, G. de B. Robinson and R. M. Thrall, The hook graphs of the symmetric group, Canad. J. Math. 6 (1954), 316–324. https://doi.org/10.4153/CJM-1954-030-1
P. Diaconis and M. Shahshahani, Generating a random permutation with random transpositions, Z. Wahrsch. Verw. Gebiete 57 (1981), 159–179. https://doi.org/10.1007/BF00535487
G. D. James, The Representation Theory of the Symmetric Groups, Lecture Notes in Math. 682, Springer, 1978.
B. E. Sagan, The Symmetric Group, 2nd ed., Graduate Texts in Math. 203, Springer, 2001. https://doi.org/10.1007/978-1-4757-6804-6
M. W. Liebeck and A. Shalev, Fuchsian groups, coverings of Riemann surfaces, subgroup growth, random quotients and random walks, J. Algebra 276 (2004), 552–601. https://doi.org/10.1016/S0021-8693(03)00515-5
E. O. Thorp, Nonrandom shuffling with applications to the game of faro, J. Amer. Statist. Assoc. 68 (1973), 842–847. https://doi.org/10.1080/01621459.1973.10481434
B. Morris, Improved mixing time bounds for the Thorp shuffle and L-reversal chain, Ann. Probab. 37 (2009), 453–477. https://doi.org/10.1214/08-AOP409
B. Morris, Improved mixing time bounds for the Thorp shuffle, Combin. Probab. Comput. 22 (2013), 118–132. https://doi.org/10.1017/S0963548312000478
A. Czumaj and B. Vöcking, Thorp shuffling, butterflies, and non-Markovian couplings, ICALP 2014, LNCS 8572, 344–355. https://doi.org/10.1007/978-3-662-43948-7_29
A. Czumaj, Random permutations using switching networks, STOC 2015, 703–712. https://doi.org/10.1145/2746539.2746629
OpenAI, From partial permutation information to Fourier bounds, OpenAI Math Release preprint, September 26, 2026 (source; Theorem 1.1, p. 1–2; Corollary 3.6, p. 9). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/From-partial-permutation-information-to-Fourier-bounds-September-26-2026/main.pdf

46 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: wurtle

Variance of the Random k-SAT Hitting TimeResearch Paper

Motivation

Add random clauses one at a time to a Boolean formula on $n$ variables until it first becomes unsatisfiable. The index $H_n$ of that first failure is the satisfiability hitting time of random $k$ -SAT. Its mean, divided by $n$ , converges to the satisfiability threshold; its variance measures the width of the transition window. Friedgut's sharp-threshold theorem shows the window is $o(n)$ , but quantitative widths have remained far from the $\sqrt n$ scale suggested by lower bounds. This mission asks for the order of the variance of $H_n$ for every fixed $k\ge3$ .

Timeline

1981. Efron and Stein prove their variance inequality, the basic tool for fluctuation bounds of functions of independent inputs (doi:10.1214/aos/1176345462).
1999. Friedgut, with an appendix by Bourgain, proves a sharp threshold sequence for each fixed $k$ (doi:10.1090/S0894-0347-99-00305-7).
2002. Wilson proves an $\Omega_k(\sqrt n)$ separation of central quantiles for the proper-clause model (doi:10.1002/rsa.10050).
2005. Boucheron, Bousquet, Lugosi and Massart give moment inequalities for functions of independent variables (doi:10.1214/009117904000000856).
2022. Ding, Sly and Sun prove the satisfiability conjecture for large $k$ (doi:10.4007/annals.2022.196.1.1).
2026. Carenini proves an $O_{k,\eta}(n/\log n)$ window (ECCC TR26-145, arXiv:2609.26222) and then a polynomial window $O_{k,\eta}(n^{1/2+1/k})$ with variance $O_k(n^{1+2/k})$ , resolving the satisfiability conjecture for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026); priority for that resolution belongs to Carenini. A companion OpenAI preprint gives an alternative proof of the limiting threshold.

The source of this mission is an OpenAI preprint dated September 27, 2026.

Setting

Fix $k\ge3$ and $n\ge k$ . A proper $k$ -clause is an OR of literals on $k$ distinct variables; let $C_1,C_2,\dots$ be independent uniform choices among the $2^k\binom nk$ signed proper clauses (signs fair, whole clauses may repeat). Put

F_m=C_1\wedge\dots\wedge C_m,\qquad F_0=\text{true},\qquad H_n=\min\{m\ge1:\ F_m\ \text{unsatisfiable}\},

and, for fixed $B>0$ , the capped hitting time $T_{n,B}=\min\{H_n,\lfloor Bn\rfloor\}$ . Since each assignment survives a clause with probability $1-2^{-k}$ , $H_n$ is a.s. finite with all moments. Write

\ell_k(n)=\begin{cases}\log(en),&k=3,\\1,&k\ge4,\end{cases}\qquad U_k=\frac{\log2}{-\log(1-2^{-k})}.

Formalization targets

Goal: Theorem 1.1

There are constants $C_k,c_k>0$ with

\operatorname{Var}(H_n)\le C_k\,n\,\ell_k(n)\quad(n\ge k),\qquad \operatorname{Var}(H_n)\ge c_kn\quad(n\ \text{large}),

and for every fixed $B>0$ a constant $C_{k,B}$ with $\operatorname{Var}(T_{n,B})\le C_{k,B}\,n\,\ell_k(n)$ ; if $B>U_k$ then also $\operatorname{Var}(T_{n,B})\ge c_kn$ for large $n$ . Hence $\operatorname{Var}(H_n)=\Theta_k(n)$ for $k\ge4$ . Lean: OAI.RandomKSAT.variance_main, open on the platform.

Milestone: Propositions A.1–A.2 (optimality of exponents)

The killing-probability exponent $\beta=k/(k-1)$ in the lifetime bound $\tau_k(S)q_d(S)^\beta\le C_kd^\beta$ (Proposition 2.3) cannot be decreased, and the block-error term $g^{-(k-1)}$ in the replacement lemma cannot be improved to $o(g^{-(k-1)})$ uniformly. Lean: OAI.RandomKSAT.sharpness.

Significance

For $k\ge4$ the theorem determines the variance of the hitting time up to constants, so the transition window has width $\Theta_k(\sqrt n)$ in the variance sense, matching Wilson's lower bound and improving Carenini's $O_k(n^{1+2/k})$ variance bound. For $k=3$ it leaves only a logarithmic gap, closed in a companion OpenAI preprint. Chebyshev's inequality then gives concentration of $H_n$ about $\mathbb EH_n$ at scale $\sqrt{n\ell_k(n)}$ .

The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.

Difficulty

The Efron–Stein inequality reduces the upper bound to the expected squared delay caused by deleting one clause, which counts pairs of prefixes at which that clause is pivotal. Controlling this occupation time requires a uniform estimate relating how quickly a set of assignments is killed by shorter $(k-1)$ -clauses to its lifetime under $k$ -clauses, valid for every assignment set with no lower cutoff. Earlier arguments truncate the number of clauses incident to the deleted clause's variables at a logarithmic level, which costs a logarithm; keeping that number as a random parameter without destroying independence is the main obstacle. Appendix A shows the relevant exponents are sharp.

Formalization scope

Clause n k is a dependent pair of a $k$ -element Finset (Fin n) and a sign vector on it; clauseLaw is uniform; streamLaw is the infinite product (Measure.infinitePi).
firstFailure ω is the least $m$ with an unsatisfiable prefix, valued in ℕ∞; H = (firstFailure ω).toNat; T B ω = (min (firstFailure ω) ⌊Bn⌋).toNat. The infinite case has probability zero.
variance is ProbabilityTheory.variance under streamLaw n k; ell, U are as displayed.
In the milestone, blockKill u s S g is the probability that $g$ independent proper $s$ -clauses kill $S$ , and lifetime u k S $=\sum_m\mathbb P(S\text{ survives }m\text{ clauses})$ is $\tau_k(S)$ .

Infrastructure: product measures on clause streams, Efron–Stein, conditioning on incidence patterns. Formalizations of Proposition 2.3 (lifetime from shorter-clause killing), Proposition 4.3 (conditional squared delay), Corollary 5.2 and Proposition 6.2 (linear variance lower bound) are welcome.

Selected references

OpenAI, Variance of the Random k-SAT Hitting Time, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Variance-of-the-Random-k-SAT-Hitting-Time-September-27-2026/article.pdf
OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
G. Carenini, The scaling window of random k-SAT, ECCC TR26-145, 2026. https://arxiv.org/abs/2609.26222
E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
D. B. Wilson, On the critical exponents of random k-SAT, Random Structures Algorithms, 2002. https://doi.org/10.1002/rsa.10050
J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
B. Efron, C. Stein, The jackknife estimate of variance, Ann. Statist., 1981. https://doi.org/10.1214/aos/1176345462
S. Boucheron, O. Bousquet, G. Lugosi, P. Massart, Moment inequalities for functions of independent random variables, Ann. Probab., 2005. https://doi.org/10.1214/009117904000000856

32 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: wurtle

A Limiting Satisfiability Threshold for Every Fixed Clause SizeResearch Paper

Motivation

A random $k$ -SAT formula on $n$ Boolean variables is a conjunction of $m$ independent random clauses, each an OR of $k$ literals on distinct variables. As the clause density $m/n$ grows, the formula changes from almost surely satisfiable to almost surely unsatisfiable. Random $k$ -SAT is a central model in probabilistic combinatorics, the theory of algorithms and statistical physics: its threshold is where hard instances are expected to concentrate, and it is a proving ground for methods from spin-glass theory. The satisfiability conjecture, formulated explicitly by Chvátal and Reed, asserts that for each fixed $k$ the transition happens at a limiting density $\alpha_k$ that does not drift with $n$ .

Timeline

1992. Chvátal and Reed settle $k=2$ and formulate the conjecture for every fixed clause size (doi:10.1109/SFCS.1992.267789); Goerdt gives an independent proof for $k=2$ (doi:10.1006/jcss.1996.0081).
1999. Friedgut, with an appendix by Bourgain, proves a sharp transition around a sequence of densities, leaving open whether the sequence converges (doi:10.1090/S0894-0347-99-00305-7).
2002, 2006. Mézard, Parisi and Zecchina, and Mertens, Mézard and Zecchina, predict threshold values via the cavity method (doi:10.1126/science.1073287, doi:10.1002/rsa.20090).
2004. Achlioptas and Peres prove bounds $2^k\log2-O(k)$ (doi:10.1090/S0894-0347-04-00464-3).
2013, 2014. Bayati, Gamarnik and Tetali develop combinatorial interpolation for sparse random structures (doi:10.1214/12-AOP816); Abbe and Montanari study concentration of solution counts (doi:10.1002/rsa.20501).
2016. Coja-Oghlan and Panagiotou locate the threshold sequence within $o_k(1)$ of $2^k\log2-(1+\log2)/2$ (doi:10.1016/j.aim.2015.11.007).
2022. Ding, Sly and Sun prove the conjecture for all sufficiently large $k$ , with the 1RSB value (doi:10.4007/annals.2022.196.1.1).
2026. Carenini proves a polynomial scaling window and resolves the conjecture for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026; https://eccc.weizmann.ac.il/report/2026/229/). Priority for the resolution belongs to Carenini.

The source of this mission is an OpenAI preprint dated September 25, 2026, which gives an alternative proof of the existence of the limiting threshold.

Setting

Fix $k\ge3$ . For $n\ge k$ , a proper $k$ -clause chooses $k$ distinct variables among $x_1,\dots,x_n$ uniformly and gives each an independent fair sign, so each of the $2^k\binom nk$ clauses is equally likely. Let $C_1,C_2,\dots$ be independent such clauses (sampled with replacement: two positions may hold the same clause) and

F_{n,m}=\bigwedge_{i=1}^mC_i,\qquad P_n(m)=\mathbb P(F_{n,m}\ \text{is satisfiable}),\qquad P_n(0)=1 .

The ratio $c=m/n$ is the clause density.

Formalization targets

Goal: Theorem 1.1

For every fixed integer $k\ge3$ there is $\alpha_k\in(0,\infty)$ such that

\lim_{n\to\infty}P_n(\lfloor cn\rfloor)=\begin{cases}1,&0\le c<\alpha_k,\\ 0,&c>\alpha_k.\end{cases}

No assertion is made at $c=\alpha_k$ , and the value of $\alpha_k$ is not identified. Lean: OAI.FixedClauseThreshold.main, open on the platform.

Significance

The theorem settles, for every fixed $k\ge3$ , the existence half of the threshold question: Friedgut's sharp transition happens at a location that converges. Previously this was known only for large $k$ (Ding–Sly–Sun) and for $k=2$ . Existence is a prerequisite for questions about the value of $\alpha_k$ , its computability, and the fluctuations of the satisfiability hitting time, which companion OpenAI preprints address. The proof here proceeds through concentration of a capped last satisfiable index and a comparison between system sizes; it does not rely on Carenini's window.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

A sharp-threshold theorem gives a narrow window at each $n$ but no control of how the window's center moves with $n$ . Convergence needs a comparison between different system sizes, and interpolation methods from spin-glass theory deliver free-energy bounds, not hard satisfiability statements, and often only for even arity. The center must also be shown to concentrate polynomially, which requires bounding how many variables are forced along the clause process.

Formalization scope

ProperClause n k is a function Fin n → Option Bool with exactly $k$ defined entries; some b at $i$ is the literal satisfied when $\sigma_i=b$ .
Formula n k m := Fin m → ProperClause n k (ordered, with replacement); properSATProbability n k m is the exact ratio of satisfiable formulas to all formulas, which equals $P_n(m)$ under the uniform product law.
Degenerate sizes: $m=0$ gives probability $1$ ; for $n<k$ and $m>0$ the ensemble is empty and the ratio is $0$ by convention, affecting only finitely many $n$ .
HasLimitingThreshold k asserts $\exists\,\alpha>0$ with limits $1$ for $0\le c<\alpha$ and $0$ for $c>\alpha$ at $m=\lfloor cn\rfloor$ .

Infrastructure: finite counting of formulas, Efron–Stein-type variance bounds, a deterministic concentration-to-convergence lemma (Theorem 5.1), and the Poisson/interpolation comparison with the transfer back to proper clauses. Formalizations of Proposition 2.2 (integrated forcing), Proposition 3.3 (polynomial concentration) and Theorem 5.1 are welcome.

Selected references

OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
V. Chvátal, B. Reed, Mick gets some (the odds are on his side), FOCS 1992. https://doi.org/10.1109/SFCS.1992.267789
E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
D. Achlioptas, Y. Peres, The threshold for random k-SAT is $2^k\log2-O(k)$ , J. Amer. Math. Soc., 2004. https://doi.org/10.1090/S0894-0347-04-00464-3
A. Coja-Oghlan, K. Panagiotou, The asymptotic k-SAT threshold, Adv. Math., 2016. https://doi.org/10.1016/j.aim.2015.11.007
J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
M. Bayati, D. Gamarnik, P. Tetali, Combinatorial approach to the interpolation method and scaling limits in sparse random graphs, Ann. Probab., 2013. https://doi.org/10.1214/12-AOP816
E. Abbe, A. Montanari, On the concentration of the number of solutions of random satisfiability formulas, Random Structures Algorithms, 2014. https://doi.org/10.1002/rsa.20501

20 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: wurtle

Critical bond and site percolation on the cubic latticeResearch Paper

Motivation

Bernoulli percolation is the simplest model of a random medium: each edge (or each vertex) of a lattice is independently kept open with probability $p$ , and one studies the connected components (clusters) of open edges or vertices. As $p$ increases, an infinite cluster appears at a critical parameter $p_c$ . Whether an infinite cluster already exists at $p_c$ decides whether the phase transition is continuous, and it is the basic question about critical behaviour. On the nearest-neighbour cubic lattice $\mathbb Z^3$ it has been a central open problem of probability and statistical physics since the 1980s; the dimensions where it was settled were $d=2$ and sufficiently high $d$ .

Timeline

1957. Broadbent and Hammersley introduce percolation as a model of transport through a random medium (doi:10.1017/S0305004100032680).
1960. Harris proves that there is no infinite cluster at $p=1/2$ for bond percolation on $\mathbb Z^2$ (doi:10.1017/S0305004100034241).
1980. Kesten identifies the square-lattice bond threshold as $1/2$ , which with Harris's theorem gives critical nonpercolation for planar bonds (doi:10.1007/BF01197577).
1981. Russo proves critical nonpercolation for site percolation on the square lattice (doi:10.1007/BF00535742).
1990. Hara and Slade establish mean-field critical behaviour, including $\theta(p_c)=0$ , in sufficiently high dimension via the lace expansion (doi:10.1007/BF02108785). Grimmett and Marstrand prove that slab thresholds converge to $p_c$ and develop dynamic renormalization (doi:10.1098/rspa.1990.0100).
1996. Benjamini and Schramm conjecture that $\theta(p_c)=0$ on every quasi-transitive graph with $p_c<1$ (doi:10.1214/ECP.v1-978).
2016. Duminil-Copin, Sidoravicius and Tassion prove critical nonpercolation for bond percolation on slabs $\mathbb Z^2\times\{0,\dots,k\}$ (doi:10.1002/cpa.21641); this does not by itself give the full $\mathbb Z^3$ result.
2017. Fitzner and van der Hofstad reach the nearest-neighbour bond range $d\ge 11$ (doi:10.1214/17-EJP56).
2020. Heydenreich and Matzke give a detailed site lace-expansion treatment in high dimension (doi:10.1007/s10955-020-02607-y).
2024. Kozma and Nitzan reduce $\theta(p_c)=0$ to a conjectured multiplicative gluing inequality (arXiv:2401.12397).
2026. Public, non-peer-reviewed announcements report AI-assisted proofs of critical nonpercolation, including a reported Lean formalization for bonds on $\mathbb Z^d$ , $d\ge2$ (Leder, August 2026).

The source of this mission is an OpenAI preprint dated September 24, 2026, giving a self-contained argument for both bond and site percolation on $\mathbb Z^3$ .

Setting

Vertices are $x\in\mathbb Z^3$ ; $x$ and $y$ are nearest neighbours if $y=x\pm e_i$ for a coordinate vector $e_i$ .

Bond model. Each edge $\{x,x+e_i\}$ is open independently with probability $p$ . Two vertices are connected if an open path joins them (a path of zero edges is allowed).
Site model. Each vertex is open independently with probability $p$ . Two vertices are connected if a nearest-neighbour path joins them with every vertex open, endpoints included; in particular the cluster of a closed vertex is empty.

Let $\mathbb P_p$ be the product law, $\theta(p)=\mathbb P_p(\text{the cluster of }0\text{ is infinite})$ , and

p_c=\inf\{p\in[0,1]:\theta(p)>0\},

defined separately for bonds ( $p_c^{\mathrm{bond}}$ ) and sites ( $p_c^{\mathrm{site}}$ ).

Formalization targets

Goal: Theorem 1.1

\mathbb P_{p_c^{\mathrm{bond}}}\bigl(\text{every bond cluster in }\mathbb Z^3\text{ is finite}\bigr)=1,\qquad \mathbb P_{p_c^{\mathrm{site}}}\bigl(\text{every site cluster in }\mathbb Z^3\text{ is finite}\bigr)=1.

The Lean statement OAI.CriticalZ3.critical_no_infinite is the conjunction of these two almost-sure statements. It is open on the platform.

Significance

Theorem 1.1 gives continuity of the percolation probability at the transition: $\theta(p)\to0$ as $p\downarrow p_c$ (the paper derives this on p. 1 from the theorem and finite-box approximation). It is the three-dimensional case of the Benjamini–Schramm criticality question and of the classical $\theta(p_c)=0$ problem, which had resisted both planar methods (which rely on duality unavailable in three dimensions) and the lace expansion (which needs high dimension). The site statement is not a formal consequence of the bond statement: site bits become hyperedges with an endpoint convention that must be preserved.

The result is proved in an OpenAI preprint, which has not been peer reviewed. A public announcement reports a Lean formalization of the bond case on $\mathbb Z^d$ ; no machine-checked proof of this exact statement exists on the platform, and the site case is not covered by that announcement's formalization. A formal proof here would certify both models in one development.

Difficulty

The natural route is renormalization: show that if an infinite cluster exists at $p_c$ , then good finite-box events have high probability, persist at some $q<p_c$ , and can be glued into an infinite cluster at $q$ . The gluing step is where the obvious argument fails. Positive correlation (Harris–FKG) controls the probability that two increasing events both occur, but here one needs the probability of reaching a relay set and then a target, conditioned on an explored region; without a comparison inequality of the form $\mathbb P(o\leftrightarrow A,\ o\leftrightarrow T)\ge \mathbb P(o\leftrightarrow A)\min_{a\in A}\mathbb P(a\leftrightarrow T)$ the losses compound. Slab results do not suffice: extinction at each slab threshold plus convergence of thresholds does not give extinction on $\mathbb Z^3$ .

Formalization scope

Vertex := Fin 3 → ℤ; bonds are pairs (x, i) representing the edge from x to step x i = x + e_i, so each edge appears once.
bondLaw p and siteLaw p are Measure.infinitePi of bernoulliMeasure true false, giving mass $p$ to "open"; parameter clamps $p$ into $[0,1]$ .
Connectivity is Relation.ReflTransGen of the open-adjacency relation; siteCluster ω x is empty unless ω x = true, matching the endpoint convention.
bondCritical and siteCritical are sInf of $\{p\in[0,1]:\mathbb P_p(\text{cluster of }0\text{ infinite})>0\}$ . The statement does not assume $p_c<1$ ; it is a known fact for $\mathbb Z^3$ , and a solver may need to prove it to rule out the empty-set convention.
The conclusion quantifies over all vertices: almost surely every cluster is finite.

A complete development needs product Bernoulli measures on countable index sets, monotone coupling, increasing events and Harris–FKG, the finite hyperedge comparison inequality, and a planar boundary-counting lemma. The percolation infrastructure is reusable for the quasi-transitive generalization in the same family. Contributions formalizing Proposition 2.1 (joint connection comparison), Corollary 2.3 (failure comparison), Lemma 4.1 (extension estimate) and Lemma 5.1 (neighbouring-box relay) are welcome.

Selected references

OpenAI, Critical bond and site percolation on the cubic lattice, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Critical-bond-and-site-percolation-on-the-cubic-lattice-September-24-2026/paper.pdf
I. Benjamini, O. Schramm, Percolation beyond $\mathbb Z^d$ , many questions and a few answers, Electron. Commun. Probab., 1996. https://doi.org/10.1214/ECP.v1-978
S. R. Broadbent, J. M. Hammersley, Percolation processes. I. Crystals and mazes, Proc. Cambridge Philos. Soc., 1957. https://doi.org/10.1017/S0305004100032680
T. E. Harris, A lower bound for the critical probability in a certain percolation process, Proc. Cambridge Philos. Soc., 1960. https://doi.org/10.1017/S0305004100034241
H. Kesten, The critical probability of bond percolation on the square lattice equals 1/2, Comm. Math. Phys., 1980. https://doi.org/10.1007/BF01197577
L. Russo, On the critical percolation probabilities, Z. Wahrsch. Verw. Gebiete, 1981. https://doi.org/10.1007/BF00535742
T. Hara, G. Slade, Mean-field critical behaviour for percolation in high dimensions, Comm. Math. Phys., 1990. https://doi.org/10.1007/BF02108785
G. R. Grimmett, J. M. Marstrand, The supercritical phase of percolation is well behaved, Proc. R. Soc. Lond. A, 1990. https://doi.org/10.1098/rspa.1990.0100
H. Duminil-Copin, V. Sidoravicius, V. Tassion, Absence of infinite cluster for critical Bernoulli percolation on slabs, Comm. Pure Appl. Math., 2016. https://doi.org/10.1002/cpa.21641
R. Fitzner, R. van der Hofstad, Mean-field behavior for nearest-neighbor percolation in d>10, Electron. J. Probab., 2017. https://doi.org/10.1214/17-EJP56
M. Heydenreich, K. Matzke, Critical site percolation in high dimension, J. Stat. Phys., 2020. https://doi.org/10.1007/s10955-020-02607-y
G. Kozma, S. Nitzan, A reduction of the θ(p_c)=0 problem to a conjectured inequality, preprint, 2024. https://arxiv.org/abs/2401.12397

2 thms2 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: wurtle

A Sharp Threshold Bound for Monotone Graph PropertiesResearch Paper

Motivation: how sharp is the threshold of a graph property?

Many questions about random graphs ask when a property — connectivity, containing a triangle, having a perfect matching — appears in the Erdős–Rényi random graph $G(n,p)$ , where each of the $\binom n2$ possible edges is present independently with probability $p$ . For an increasing property the probability $\mu_p(\mathcal P)$ rises from $0$ to $1$ as $p$ grows, and the threshold width measures how quickly: the length of the interval of $p$ over which $\mu_p(\mathcal P)$ climbs from $\varepsilon$ to $1-\varepsilon$ . Friedgut and Kalai showed in 1996 that symmetry alone forces every such transition to be narrow, and conjectured the optimal universal width. This question links probabilistic combinatorics with the Fourier analysis of Boolean functions, and the influence inequalities developed for it are now standard tools in theoretical computer science and statistical physics.

Timeline

1981 — Russo's formula (the Margulis–Russo identity) expresses $\frac{d}{dp}\mu_p(\mathcal P)$ as a total influence (Russo 1981).
1988 — Kahn, Kalai and Linial prove that every balanced Boolean function has a coordinate of influence $\Omega(\log N/N)$ (KKL, FOCS 1988).
1992 — Bourgain, Kahn, Kalai, Katznelson and Linial extend the influence theorem to product measures (BKKKL, Israel J. Math. 1992).
1996 — Friedgut and Kalai prove that every monotone graph property on $n$ vertices has threshold width at most $C\log(1/(2\varepsilon))/\log n$ (Theorem 1.1) and conjecture the bound with $(\log n)^2$ in the denominator (Conjecture 1.2) (Friedgut–Kalai, Proc. AMS 1996). The property of containing a clique of order proportional to $\log n$ shows $(\log n)^{-2}$ would be optimal.
1997 — Bourgain and Kalai, using the action of the symmetry group on sets of coordinates, obtain width $C_{\eta,\varepsilon}(\log n)^{-2+\eta}$ for every $\eta>0$ (Bourgain–Kalai, GAFA 1997).
2020 — Kelman, Kindler, Lifshitz, Minzer and Safra prove, at $p=1/2$ , the graph-symmetric influence bound $I_{1/2}(f)\ge c\,(\log n)^2(\log\log n)^{-2}\operatorname{Var}_{1/2}(f)$ (KKLMS, GAFA 2020).
2022 — Friedgut surveys the influence method (ICM 2022).
2026 — An OpenAI preprint, A Sharp Threshold Bound for Monotone Graph Properties (OpenAI Math Release, September 25, 2026), claims the conjectured bound with explicit constant $2^{19}$ . The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Fix an integer $n\ge2$ and let $E_n=\binom{[n]}{2}$ be the set of unordered pairs of vertices. A graph configuration is a map $x:E_n\to\{0,1\}$ (in Lean GraphConfig n := GraphEdge n → Bool, where GraphEdge n is the type of 2-element subsets of Fin n). A Boolean function $f$ on configurations is

vertex invariant if $f(\pi\cdot x)=f(x)$ for every permutation $\pi$ of the vertices, where $\pi$ acts on edges by relabelling endpoints;
increasing if $x\le y$ edgewise and $f(x)=1$ imply $f(y)=1$ ;
nontrivial if it takes both values.

For $p\in\mathbb R$ the graph mean is $\mu_p(f)=\sum_x \prod_{e} p^{x_e}(1-p)^{1-x_e}\, f(x)$ , the probability that $G(n,p)$ has the property when $p\in[0,1]$ . For $0<a<1$ the quantile is

p_a(f)=\inf\{p\in[0,1]:\ \mu_p(f)\ge a\}.

Formalization targets

Goal: the Friedgut–Kalai sharp-threshold conjecture (Theorem 1.1)

For every $n\ge2$ , every vertex-invariant, increasing, nontrivial $f$ , and every $0<\varepsilon<1/2$ ,

p_{1-\varepsilon}(f)-p_\varepsilon(f)\ \le\ \frac{2^{19}}{(\log n)^2}\,\log\frac{1}{2\varepsilon}.

The constant $2^{19}$ is the source's explicit choice and is not claimed to be sharp; the content is the order $(\log n)^{-2}$ with linear dependence on $\log(1/(2\varepsilon))$ . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The bound is uniform over all monotone graph properties and is of optimal order in $n$ for fixed $\varepsilon$ , as the clique example of Friedgut and Kalai shows. It settles the exponent question left open between the $(\log n)^{-1}$ bound of 1996 and the $(\log n)^{-2+\eta}$ bound of 1997. The driving estimate in the source, Theorem 1.2 (variance is at most $2^{17}(\log n)^{-2}$ times total influence, for every $0<p<1$ and without monotonicity), is a graph-symmetric influence inequality of independent interest; it removes the $(\log\log n)^2$ loss of the 2020 bound and holds at every bias.

Formalizing it. A formal proof would certify a universal statement over all graph properties with an explicit constant. The supporting library — Fourier–Walsh analysis on biased product spaces, pivotal influences, the Margulis–Russo derivative formula, and random restrictions — is reusable for other threshold and influence results, none of which are currently formalized in Mathlib in this form.

Difficulty

The classical route bounds the derivative $\frac{d}{dp}\mu_p$ from below through the largest influence, using only that the symmetry group acts transitively on edges; transitivity alone cannot give better than $(\log n)^{-1}$ , because there are transitive families (on non-graph coordinate sets) whose thresholds are that wide. Reaching $(\log n)^{-2}$ requires using the vertex structure of the symmetry group, and the bound must hold uniformly for every bias $p\in(0,1)$ , including very small $p$ where hypercontractive estimates degrade. Influence estimates at $p=1/2$ alone do not suffice, since a width bound requires control throughout the transition interval.

Formalization scope

Configurations are GraphEdge n → Bool; the measure is the explicit finite sum graphMean p f with product weights $p$ or $1-p$ ; logarithms are natural (Real.log).
graphQuantile a f is sInf of $\{p\in[0,1]:\mu_p(f)\ge a\}$ . For a nontrivial increasing $f$ , $\mu_1(f)=1$ , so this set is nonempty and the infimum is not a junk value; the hypotheses NontrivialGraphProperty and $0<\varepsilon<1/2$ exclude the degenerate cases.
The theorem quantifies over all $n\ge 2$ , all such $f$ , and all real $\varepsilon\in(0,1/2)$ ; no asymptotic or "sufficiently large $n$ " assumption is used.
Needed infrastructure: biased Fourier expansion on $\{0,1\}^{E_n}$ , influences and the Russo derivative formula, the action of $S_n$ on edges, and integration of a differential inequality for the quantile. Contributions formalizing Theorem 1.2 (variance–influence) or Russo's formula separately are welcome as stepping stones.

Selected references

E. Friedgut and G. Kalai, Every monotone graph property has a sharp threshold, Proc. Amer. Math. Soc. 124 (1996), 2993–3002. https://doi.org/10.1090/S0002-9939-96-03732-X
J. Bourgain and G. Kalai, Influences of variables and threshold intervals under group symmetries, Geom. Funct. Anal. 7 (1997), 438–461. https://doi.org/10.1007/s000390050015
J. Kahn, G. Kalai and N. Linial, The influence of variables on Boolean functions, FOCS 1988, 68–80. https://doi.org/10.1109/SFCS.1988.21923
J. Bourgain, J. Kahn, G. Kalai, Y. Katznelson and N. Linial, The influence of variables in product spaces, Israel J. Math. 77 (1992), 55–64. https://doi.org/10.1007/BF02808010
L. Russo, On the critical percolation probabilities, Z. Wahrsch. Verw. Gebiete 56 (1981), 229–237. https://doi.org/10.1007/BF00535742
E. Kelman, G. Kindler, N. Lifshitz, D. Minzer and M. Safra, Towards a proof of the Fourier–entropy conjecture?, Geom. Funct. Anal. 30 (2020), 1097–1138. https://doi.org/10.1007/s00039-020-00544-2
E. Friedgut, KKL's influence on me, Proc. ICM 2022, Vol. 6, 4568–4581. https://doi.org/10.4171/ICM2022/78
OpenAI, A Sharp Threshold Bound for Monotone Graph Properties, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Sharp-Threshold-Bound-for-Monotone-Graph-Properties-September-25-2026/paper.pdf

2 thms2 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: wurtle

The second Kahn–Kalai conjectureResearch Paper

Motivation

When does the Erdős–Rényi random graph $G(n,p)$ contain a copy of a prescribed graph $H$ ? A necessary condition is visible from first moments: if some subgraph $F\subseteq H$ has expected copy count below a constant, then $H$ is unlikely to appear. Kahn and Kalai conjectured in 2007 that this elementary obstruction determines the containment threshold up to a logarithmic factor, uniformly over all target graphs, including spanning ones such as perfect matchings, Hamilton cycles or cubes (CPC 2007). Their abstract conjecture for general increasing families (the "first" conjecture) was proved by Park and Pham; the graph-specific "second" conjecture compares the threshold with the smaller, purely subgraph-count-based graph expectation threshold, and is not implied by the abstract theorem.

This mission asks for a formal proof of the second Kahn–Kalai conjecture with explicit constants, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

1960–1981 — Erdős and Rényi's evolution of random graphs (1960) and perfect matchings (1966); Bollobás determines thresholds for fixed subgraphs (Math. Proc. Camb. Phil. Soc. 1981).
2007 — Kahn and Kalai state both conjectures (CPC 2007).
2010 — Talagrand introduces fractional expectation thresholds (STOC 2010).
2021 — Frankston, Kahn, Narayanan and Park prove $p_c=O(q_f\log\ell)$ (Annals 2021), building on the sunflower methods of Alweiss–Lovett–Wu–Zhang (Annals 2021).
2022–2025 — Mossel, Niles-Weed, Sun and Zadik obtain a single-log bound for a modified graph threshold (arXiv:2209.03326) and a Bayesian proof of the spread lemma (RSA 2025).
2024 — Park and Pham prove the abstract Kahn–Kalai conjecture (JAMS 2024).
2025 — Dubroff, Kahn and Park prove $p_c=O(p_E\log^3n)$ and special cases (arXiv:2508.14269, arXiv:2510.02005).
2026 — Tran reduces the loss to $O(\log^2(2e(H)))$ and proves the conjecture for trees and other classes (arXiv:2609.20546); the OpenAI preprint claims the general case (Theorem 1.1, p. 1).

Setting

For finite simple graphs $G,F$ let $N(G,F)$ be the number of subgraphs of $G$ isomorphic to $F$ (ordinary, non-induced copies). $G(n,p)$ is the random graph on $[n]$ with each of the $\binom n2$ edges present independently with probability $p$ . For a graph $H$ with at least one edge and at most $n$ vertices,

p_c(n,H)=\inf\{p\in[0,1]:\ \Pr[N(G(n,p),H)>0]\ge\tfrac12\},

p_E(n,H)=\inf\{p\in[0,1]:\ \mathbb E\,N(G(n,p),F)\ge\tfrac12\ \text{for every subgraph }F\subseteq H\}.

The first is the containment threshold, the second the graph expectation threshold; always $p_E\le p_c$ . Write $h=e(H)$ for the number of edges.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every $n\ge2$ and every finite simple graph $H$ with $h\ge1$ edges and at most $n$ vertices,

p_c(n,H)\ \le\ \min\bigl\{1,\ 2048\,e^{50}\,p_E(n,H)\,(1+\log_2 h)\bigr\},\qquad p_c(n,H)\ \le\ 6144\,e^{50}\,p_E(n,H)\log_2 n .

The constants are explicit and universal; $H$ may vary with $n$ .

Significance

The result itself. The bound says that, up to a universal constant times $\log h$ , the only obstruction to containing $H$ is a subgraph with too few expected copies. The logarithm cannot be removed: for a perfect matching $p_E=\Theta(1/n)$ while $p_c=\Theta(\log n/n)$ , because isolated vertices must disappear. This settles the problem left by the abstract Park–Pham theorem, whose bound is in terms of the possibly larger integral expectation threshold of the family of graphs containing $H$ .

Formalizing it. Both thresholds are finite, explicit optimization problems over Bernoulli product measures on the edges of $K_n$ , so the statement is fully elementary. Mathlib has SimpleGraph.copyCount but no random-graph or threshold theory; the spread-family resampling lemma and the tree covering theorem would be reusable for other threshold results (Park–Pham, Frankston–Kahn–Narayanan–Park). No machine-checked proof of any Kahn–Kalai-type theorem is known.

Difficulty

The abstract theorem compares $p_c$ with the integral expectation threshold of the family $\mathcal F_H$ of edge sets containing a copy of $H$ , and covers of $\mathcal F_H$ may be much cheaper than the copies of a single subgraph, so it does not give a bound in terms of $p_E$ . Previous graph-specific approaches lost extra logarithms because each conditional extension step paid the sampling cost again. The preprint (Section 1.2, pp. 3) builds a tree of nested subgraph extensions with geometrically growing, pairwise disjoint labels along each path, and must reuse one random set at every level of the tree while keeping the spread property under conditioning (Theorem 3.1, p. 6).

Formalization scope

$G(n,p)$ is encoded as a Bernoulli product weight on Finset (Edge n), where Edge n is the type of non-diagonal Sym2 (Fin n); expectations and probabilities are finite sums, defined for every real $p$ but used only on $[0,1]$ .
expectedCopies and containmentProbability use Mathlib's copyCount of the graph built from the edge set; both are ordinary (non-induced) copies.
criticalThreshold and expectationThreshold are sInf over $p\in[0,1]$ ; the sets are nonempty (they contain $p=1$ when $H$ has at most $n$ vertices), so the infima are the true thresholds. The expectation constraint ranges over all H.Subgraphs, including subgraphs with isolated vertices, whose constraints are automatically satisfied.
$H$ is a SimpleGraph on an arbitrary finite type V with Fintype.card V ≤ n, 2 ≤ n and at least one edge; logTwo is $\log x/\log 2$ .
The constants $2048e^{50}$ and $6144e^{50}$ are hard-coded, as in the source.

Selected references

OpenAI, The second Kahn–Kalai conjecture, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-second-Kahn-Kalai-conjecture-September-24-2026/paper.pdf
J. Kahn, G. Kalai, Thresholds and expectation thresholds, Combin. Probab. Comput. 16 (2007), 495–502. https://doi.org/10.1017/S0963548307008474
J. Park, H. T. Pham, A proof of the Kahn–Kalai conjecture, J. Amer. Math. Soc. 37 (2024), 235–243. https://doi.org/10.1090/jams/1028
K. Frankston, J. Kahn, B. Narayanan, J. Park, Thresholds versus fractional expectation-thresholds, Ann. of Math. 194 (2021), 475–495. https://doi.org/10.4007/annals.2021.194.2.2
R. Alweiss, S. Lovett, K. Wu, J. Zhang, Improved bounds for the sunflower lemma, Ann. of Math. 194 (2021), 795–815. https://doi.org/10.4007/annals.2021.194.3.5
M. Talagrand, Are many small sets explicitly small?, STOC 2010. https://doi.org/10.1145/1806689.1806693
E. Mossel, J. Niles-Weed, N. Sun, I. Zadik, On the second Kahn–Kalai conjecture, arXiv:2209.03326 (2022). https://arxiv.org/abs/2209.03326v1
E. Mossel, J. Niles-Weed, N. Sun, I. Zadik, A Bayesian proof of the spread lemma, Random Structures Algorithms 66 (2025), e70008. https://doi.org/10.1002/rsa.70008
Q. Dubroff, J. Kahn, J. Park, On the "second" Kahn–Kalai conjecture, arXiv:2508.14269 (2025). https://arxiv.org/abs/2508.14269v1
T. Tran, Fractional expectation thresholds and the "second" Kahn–Kalai conjecture, arXiv:2609.20546 (2026). https://arxiv.org/abs/2609.20546v2
B. Bollobás, Threshold functions for small subgraphs, Math. Proc. Cambridge Philos. Soc. 90 (1981), 197–206. https://doi.org/10.1017/S0305004100058655

47 thms2 active usersReviewed

Completed

Machine Learning Theoretical Computer Science·Captain: wurtle

Subsphere methods for memory-sample lower bounds in noiseless Gaussian regressionResearch Paper

Motivation

An exact linear equation can carry arbitrarily fine real information: $d$ independent Gaussian equations $Y_t = \langle X_t, s\rangle$ determine a vector $s \in \mathbb{R}^d$ almost surely. A streaming learner that keeps only finitely many persistent states cannot retain those equations at arbitrary precision. The question is how many fresh equations such a learner needs to estimate a direction to angular accuracy $\epsilon$ when the information passed between observations is bounded in bits.

This preprint proves an explicit answer for memory $o(d^2)$ : at least $2^{-16}\, d\log_2(1/\epsilon)$ samples, uniformly in $0 < \epsilon \le 1/10$ . With real-valued registers, randomized Kaczmarz needs only order $d\log(1/\epsilon)$ samples, so the bound shows that bounded memory cannot beat that scale.

Background

2015. Steinhardt and Duchi show memory restrictions affect statistical risk in sparse noisy regression.
2016. Steinhardt, Valiant and Wager relate bounded-memory inference to communication and statistical queries and pose a quadratic-memory versus exponential-sample question for parity learning; Raz proves the separation through finite-width branching programs.
2019. Sharan, Sidford and Valiant prove, for Gaussian covariates with uniform noise of half-width $2^{-d/5}$ , memory at most $d^2/4$ bits and Euclidean accuracy $d^{-r}$ , an $\Omega(d\log r)$ sample lower bound; their Section 7 uses high moments with independent copies and successive orthogonalization. Dagan, Kur and Shamir prove space lower bounds for different linear-prediction tasks.
2026. The OpenAI preprint Subsphere methods for memory-sample lower bounds in noiseless Gaussian regression (dated September 27, 2026) proves the explicit $2^{-16}d\log_2(1/\epsilon)$ bound for exact observations. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Fix $d \ge 2$ , $M \ge 0$ , $T \ge 0$ , and $0 < \epsilon \le 1/10$ . For a signal $s \in S^{d-1}$ the observations are $X_t \sim N(0, I_d)$ independent and $Y_t = \langle X_t, s\rangle$ exactly. A finite-state Gaussian stream learner reads the pairs in order; at every index its persistent state has at most $2^M$ values. Transition and stopping rules may depend on the index, $d, M, T, \epsilon$ , the current state, the whole current pair and fresh randomness, with unrestricted computation. It stops at some $\tau \le T$ and outputs $\hat s \in S^{d-1}$ from the terminal state, $\tau$ and fresh randomness. A shared seed may choose the rules; seed and initial state are independent of the signal and rows. The experiment is jointly measurable.

For a linear space $H$ and $z \perp H$ , $r > 0$ with $\|z\|^2 + r^2 = 1$ , the affine subsphere $z + rS(H)$ is a test set of dimension $\dim H$ . A block of $b$ exact Gaussian rows leaves the target, conditionally, uniform on a random residual subsphere of dimension $\dim H - b$ .

In Lean (OAI.SubsphereCurrent), learners are SeededLearner d M T Ω built from KernelLearners (Markov-kernel transitions on completed observations, states Fin (2^M)), with Admissible measurability, uniformSuccess and per-signal success.

Formalization targets

Goal: `full_current_main_scope`

The conjunction of the paper's main statements:

Theorem 1.2 with Corollary 1.3 (explicit noiseless precision bound). For every $M(d) = o(d^2)$ there is a threshold such that for larger $d$ , every $0 < \epsilon \le 1/10$ and every learner with uniform-prior success at least $2/3$ , or success at least $2/3$ at every signal,

T \ge 2^{-16}\, d \log_2(1/\epsilon).

Corollary 6.3: with uniform-prior success at least $1/2$ , $T \ge c\, d\log_2(1/\epsilon)$ for an absolute $c > 0$ .
Theorem 6.1 (radius-weighted block estimate, with its terminal bound), Proposition 7.1 (all-affine suffix bound), Proposition 8.1 (dimension-parameterized success bound: for $m$ -dimensional targets, $jk$ samples and $2^{d^2}$ states, $\Pr\{\|\hat s - s\| \le \eta\} \le (C^{j+1}\eta)^{d/32}$ ), and the beta-mixture estimate of Section 9.

Significance

The result. Theorem 1.2 gives explicit constants for the $\Omega(d\log(1/\epsilon))$ memory–sample bound with exact Gaussian observations and $o(d^2)$ memory, e.g. $T \ge 2^{-16} r\, d\log_2 d$ at accuracy $d^{-r}$ . The block estimates are statements about uniform measures on random affine subspheres that are independent of the learning application.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Companion missions on the same family of preprints (memory and precision, posterior replicas, projection moments) share the learner model; this one is distinguished by explicit constants.

Difficulty

Conditioning on an exact Gaussian block makes the posterior of the signal singular: it is uniform on a lower-dimensional residual subsphere determined by the data. Density-based information arguments therefore fail after one block. The bound must control the success probability of the remaining computation, started from any state, averaged over every affine subsphere of large dimension, uniformly over learners that may process each real-valued pair without limit.

Formalization scope

Vector d = EuclideanSpace ℝ (Fin d), signals in the unit sphere with normalized surface measure, rows i.i.d. stdGaussian.
Thresholds: success $\ge 2/3$ (and $\ge 1/2$ for the Corollary 6.3 conjunct), in ℝ≥0∞; the constant $2^{-16}$ is written (2:ℝ)⁻¹ ^ 16 and the logarithm is Real.logb 2.
Block sizes are natural-number floors d/16, d/32, d/8; the fixed-length estimate uses Fin (2^(d^2)) states.
The seed space is an arbitrary probability space; randomized learners are covered by seeds.

The goal cannot be satisfied vacuously: hypotheses range over all admissible learners and the success thresholds are attainable with large $T$ .

Needed infrastructure: Haar measure on Grassmannians or orthogonal groups, beta laws of projected directions, spherical caps, measurable selection of Borel rule versions. Contributions proving individual conjuncts are welcome.

Selected references

OpenAI, Subsphere methods for memory-sample lower bounds in noiseless Gaussian regression, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Subsphere-methods-for-memory-sample-lower-bounds-in-noiseless-Gaussian-regression-September-27-2026/paper.pdf
V. Sharan, A. Sidford, G. Valiant, Memory-Sample Tradeoffs for Linear Regression with Small Error, STOC 2019. https://doi.org/10.1145/3313276.3316403
J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
J. Steinhardt, G. Valiant, S. Wager, Memory, Communication, and Statistical Queries, COLT 2016. https://proceedings.mlr.press/v49/steinhardt16.html
R. Raz, Fast Learning Requires Good Memory, 2016. https://arxiv.org/abs/1602.05161
Y. Dagan, G. Kur, O. Shamir, Space Lower Bounds for Linear Prediction in the Streaming Model, COLT 2019. https://proceedings.mlr.press/v99/dagan19b.html
P. Frankl, H. Maehara, Some Geometric Applications of the Beta Distribution, Ann. Inst. Statist. Math. 42 (1990).

45 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Optimization of Convex Risk Functions 3: A Distribution-Invariant Risk Function Is Consistent with the Increasing Convex Order Iff It Is Monotone and Risk AverseResearch Paper

Motivation

Risk-averse optimization replaces the expected cost $\mathbb E[X]$ of a random outcome by a risk function $\rho(X)$ that also penalizes dispersion: mean–deviation, mean–semideviation, conditional value-at-risk (CVaR) and their combinations are the standard examples in stochastic programming and portfolio selection. A decision maker who uses $\rho$ should not prefer an outcome that every risk-averse expected-utility maximizer rejects. For costs, the order that expresses this agreement among risk-averse agents is the increasing convex order: $X_2$ is worse than $X_1$ if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every increasing convex disutility $u$ . It is the counterpart, for costs, of second-order stochastic dominance.

Whether a given mean–risk model is consistent with stochastic dominance was settled model by model: Ogryczak and Ruszczyński for mean–semideviation models (Eur. J. Oper. Res. 1999, Math. Program. 2001, SIAM J. Optim. 2002) and Pflug for CVaR (2000). Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) gave a single criterion, Theorem 5.1, which contains these results as special cases: among risk functions that depend only on the distribution of the outcome, consistency with the increasing convex order is equivalent to two structural properties, monotonicity and risk aversion.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $p\in[1,\infty)$ . The space of outcomes is $\mathcal X=\mathcal L_p(\Omega,\mathcal F,P)$ , the real random variables with $\mathbb E|X|^p<\infty$ . An outcome is a cost: smaller is better. A risk function is a map $\rho:\mathcal X\to\mathbb R$ .

The cdf of $X$ is $F_X(t)=P(X\le t)$ . $\rho$ is distribution invariant (Definition 5.2) if $F_{X_1}=F_{X_2}$ implies $\rho(X_1)=\rho(X_2)$ .
$\rho$ satisfies (A2) (monotonicity) if $X\le Y$ almost surely implies $\rho(X)\le\rho(Y)$ .
$\rho$ is risk averse (Definition 5.1) if for every $\sigma$ -algebra $\mathcal G\subset\mathcal F$ and every $X\in\mathcal X$ ,

\rho(X)\ \ge\ \rho\big(\mathbb E[X\mid\mathcal G]\big),

for every version of the conditional expectation.

For random variables $X_1,X_2$ , the usual stochastic order $X_2\succeq_{\mathrm{st}}X_1$ holds if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every nondecreasing $u:\mathbb R\to\mathbb R$ for which both expectations exist; the increasing convex order $X_2\succeq_{\mathrm{icx}}X_1$ is the same with $u$ ranging over the increasing convex functions.
$\rho$ is consistent with an order $\succeq$ if $X_2\succeq X_1$ implies $\rho(X_2)\ge\rho(X_1)$ for all $X_1,X_2\in\mathcal X$ .

The paper places one more standing assumption on §5.2: the space is rich enough to carry a uniform random variable, a measurable $U:\Omega\to\mathbb R$ with $P(U\le t)=t$ for all $t\in[0,1]$ .

In Lean these are IsUniformRV, cdfOf, cdfInv, DistInvariant, A2, RiskAverse, StLE, ConsistentSt and ConsistentIcx in the namespace ConvexRiskFn.Order; the increasing convex order is the published StochasticOrders.MonotoneConvex.IcxOrder P P X₁ X₂, read as $X_1\preceq_{\mathrm{icx}}X_2$ .

Formalization targets

Goal: Theorem 5.1 (p. 446)

Under the standing assumptions, for every distribution-invariant $\rho:\mathcal X\to\mathbb R$ ,

\rho\ \text{consistent with}\ \succeq_{\mathrm{icx}}\quad\Longleftrightarrow\quad \rho\ \text{satisfies (A2) and is risk averse}.

No convexity, translation equivariance or positive homogeneity of $\rho$ is assumed.

Milestones

The usual stochastic order and the cdf (§5.2, p. 445): $X_2\succeq_{\mathrm{st}}X_1$ iff $F_{X_2}(t)\le F_{X_1}(t)$ for all $t$ .
The quantile coupling (proof of Lemma 5.1, p. 446): $F_X^{-1}(U)$ has the law of $X$ , and $F_{X_2}\le F_{X_1}$ gives $F_{X_1}^{-1}(U)\le F_{X_2}^{-1}(U)$ almost surely.
Lemma 5.1 (p. 445): a distribution-invariant $\rho$ is consistent with $\succeq_{\mathrm{st}}$ iff it satisfies (A2).
Conditional expectation is icx-smaller (proof of Theorem 5.1, p. 446): $\mathbb E[X\mid\mathcal G]\in\mathcal X$ and $\mathbb E[X\mid\mathcal G]\preceq_{\mathrm{icx}}X$ .
Strassen's coupling on $\Omega$ (proof of Theorem 5.1, p. 446): if $X_1\preceq_{\mathrm{icx}}X_2$ , there are $\widehat X_1\overset{D}{\sim}X_1$ , $\widehat X_2\overset{D}{\sim}X_2$ on the same $\Omega$ with $\widehat X_1\le\mathbb E[\widehat X_2\mid\widehat X_1]$ a.s.

Significance

Theorem 5.1 reduces a property quantified over all pairs of ordered distributions to two properties that can be checked on the risk function directly. Monotonicity is usually immediate, and risk aversion follows for the main examples from the dual representation of the risk function (the paper verifies it for mean–semideviation and for CVaR-based models in §5.1). The theorem then yields at once the consistency of these models with the increasing convex order, which was previously proved case by case. It also explains the failures: a law-invariant risk function that violates (A2), such as mean–deviation for $p>1$ under the paper's condition $(*)$ , cannot be consistent with any increasing integral stochastic order.

The result has a complete published proof. What the mission adds is a machine-checked version of it on the paper's own space $\mathcal L_p(\Omega,\mathcal F,P)$ , together with reusable pieces of stochastic-order theory: the cdf characterization of the usual stochastic order, the quantile coupling, conditional Jensen in increasing-convex form, and Strassen's martingale coupling realized on a given space carrying a uniform random variable. Mathlib has conditional Jensen for convex functions (ConvexOn.map_condExp_le_univ) but not the stochastic orders, the quantile coupling or Strassen's theorem. Strassen's theorem for laws on $\mathbb R^n$ , with a coupling on some probability space, is posed separately on Prove2Me but not proved.

Difficulty

The forward direction is short given milestone 4. The reverse direction is where the work is. Consistency compares $\rho(X_1)$ and $\rho(X_2)$ for random variables that are related only through their laws: $X_1\preceq_{\mathrm{icx}}X_2$ says nothing about $X_1(\omega)$ versus $X_2(\omega)$ , so neither (A2) nor risk aversion applies to the pair as given. The argument has to replace the pair by another pair, with the same laws, on the same space $\Omega$ , related by a conditional expectation; only then can monotonicity and risk aversion be chained. Producing that pair is Strassen's theorem, a nonconstructive existence result about martingale couplings, and it has to be realized on the given $\Omega$ , not on a product space built for the purpose, because $\rho$ is defined only on $\mathcal L_p(\Omega,\mathcal F,P)$ . That is the role of the uniform random variable, and transporting the coupling onto $\Omega$ through it is a separate measure-theoretic step. The first-order analogue, Lemma 5.1, needs the same kind of transfer, through quantile functions, whose values at $0$ and $1$ must be handled.

Formalization scope

$\mathcal L_p$ is encoded by functions $\Omega\to\mathbb R$ satisfying MemLp X p P with 1 ≤ p and p ≠ ⊤, not by almost-everywhere classes. $\rho$ is a function (Ω → ℝ) → ℝ; every definition quantifies only over MemLp arguments, so its values elsewhere play no role. $\rho$ is real valued, as in Definition 5.2.
The order in (A2) is the almost-sure order, the order of $\mathcal L_p$ (p. 434).
"For which the expectations exist" is integrability of $u\circ X_1$ and $u\circ X_2$ , as in the published increasing convex order.
Risk aversion quantifies over every sub- $\sigma$ -algebra $\mathcal G\subseteq\mathcal F$ and every $\mathcal G$ -measurable version of Mathlib's conditional expectation P[X|m].
The uniform random variable and $p\in[1,\infty)$ appear as hypotheses of the goal, of Lemma 5.1 and of milestone 5, exactly where the paper's standing assumptions of §5.2 apply. Milestones 1 and 4 do not need them.
The quantile $F^{-1}(t)=\inf\{s:F(s)\ge t\}$ is a real infimum, which is $0$ where the paper's value is $\pm\infty$ ( $t\notin(0,1)$ ); milestone 2 is therefore stated almost surely.
The goal mentions neither quantiles, nor $U$ beyond its existence, nor any coupling. A statement that assumed convexity of $\rho$ , dropped distribution invariance, restricted to bounded or pointwise-ordered outcomes, or replaced risk aversion by the single $\sigma$ -algebra $\{\emptyset,\Omega\}$ would be a different and weaker theorem and does not count.

Needed infrastructure: equality in law from equality of cdfs, the quantile transform, conditional Jensen's inequality (in Mathlib) turned into the increasing convex order, and Strassen's theorem in dimension one with the transfer of a coupling to a space carrying a uniform random variable. The last two are reusable well beyond this mission. Proofs of any milestone, and of supporting lemmas such as the cdf characterization of equality in law, are welcome.

Selected references

A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
A. Müller, D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002 (Theorem 1.2.8, Corollary 1.5.21). https://www.wiley.com/en-us/Comparison+Methods+for+Stochastic+Models+and+Risks-p-9780471494461
V. Strassen, The existence of probability measures with given marginals, Annals of Mathematical Statistics 36(2):423–439, 1965. https://doi.org/10.1214/aoms/1177700153
D. Blackwell, Equivalent comparisons of experiments, Annals of Mathematical Statistics 24(2):265–272, 1953. https://doi.org/10.1214/aoms/1177729032
W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM Journal on Optimization 13(1):60–78, 2002. https://doi.org/10.1137/S1052623400375075
M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

8 thms2 active usersReviewed

Machine Learning Statistics·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

Selected references

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

19 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Distributionally Robust Optimization and Its Tractable Approximations 3: The Infimal Convolution of π¹, π², π³ Bounds the Worst Case over the Intersected Families and Improves on EachResearch Paper

Motivation

Two-stage and multistage stochastic programs ask for decisions that react to uncertainty revealed over time. When the distribution of the uncertainty is known only partially, one optimizes against the worst distribution in a family $\mathbb F$ consistent with what is known: a support set, a range for the mean, a covariance matrix, bounds on how fast the tails decay. Goh and Sim (Oper. Res. 58(4), 2010) show that once linear and deflected linear decision rules are imposed, the recourse costs of such models reduce to worst-case expectations of positive parts,

\sup_{\mathbb P\in\mathbb F}E_{\mathbb P}\big((r^0+r'\tilde\zeta)^+\big),

of affine functions of a random vector $\tilde\zeta$ . These quantities are generally intractable, so the paper bounds them by optimization problems that are. Each kind of partial information gives its own bound, and in practice a modeller usually has several kinds at once. Theorem 4 of the paper, the target here, combines the separate bounds into a single one that uses all of the information.

Timeline: Scarf (1958) gave, for a newsvendor problem, the worst-case expected positive part of a scalar with known mean and variance. Chen, Sim and Sun (Oper. Res. 55(6), 2007) introduced the forward and backward deviations used here to describe tails of independent components. Chen and Sim (Oper. Res. 57(2), 2009) introduced the combination of bounds by infimal convolution that Theorem 4 restates in the present setting. Goh and Sim (2010) assemble the three kinds of information into one model and use the combined bound for their bideflected linear decision rules.

Setting

A distribution $\mathbb P$ is a probability measure on $\mathbb R^{N_E}$ , the law of the uncertain vector $\tilde\zeta$ ; its mean is $\hat\zeta=E_{\mathbb P}(\tilde\zeta)$ . Fix data: sets $\mathcal V,\hat{\mathcal V}\subseteq\mathbb R^{N_E}$ , matrices $F\in\mathbb R^{N\times N_E}$ , $\Sigma\in\mathbb R^{N\times N}$ , $F_\sigma\in\mathbb R^{N_\sigma\times N_E}$ , a vector $g_\sigma\in\mathbb R^{N_\sigma}$ , a set $\hat{\mathcal W}_\sigma\subseteq\mathbb R^{N_\sigma}$ and vectors $\sigma_f,\sigma_b\ge0$ in $\mathbb R^{N_\sigma}$ . Three families encode three kinds of information:

Mean and support: $\mathbb F_1=\{\mathbb P:\hat\zeta\in\hat{\mathcal V},\ \mathbb P(\tilde\zeta\in\mathcal V)=1\}$ .
Mean and covariance: $\mathbb F_2=\{\mathbb P:\hat\zeta\in\hat{\mathcal V},\ E_{\mathbb P}(F(\tilde\zeta-\hat\zeta)(\tilde\zeta-\hat\zeta)'F')=\Sigma\}$ .
Mean and directional deviations: $\mathbb F_3$ is the set of $\mathbb P$ with $\hat\zeta\in\hat{\mathcal V}$ such that $\tilde z_\sigma=F_\sigma\tilde\zeta+g_\sigma$ has independent components whose forward and backward deviations

\sigma_{f\mathbb P}(\tilde z_{\sigma,j})=\sup_{\theta>0}\sqrt{\tfrac{2}{\theta^2}\ln E_{\mathbb P}e^{\theta(\tilde z_{\sigma,j}-\hat z_{\sigma,j})}},\qquad \sigma_{b\mathbb P}(\tilde z_{\sigma,j})=\sup_{\theta>0}\sqrt{\tfrac{2}{\theta^2}\ln E_{\mathbb P}e^{-\theta(\tilde z_{\sigma,j}-\hat z_{\sigma,j})}}

are at most $\sigma_{f,j}$ and $\sigma_{b,j}$ .

The bounds are the optimal values $\pi^1,\pi^2,\pi^3$ of (21), (22) and (24) of the paper. For instance

\pi^1(r^0,r)=\inf_{s}\Big(\sup_{\hat\zeta\in\hat{\mathcal V}}s'\hat\zeta+\sup_{\zeta\in\mathcal V}\max\{r^0+r'\zeta-s'\zeta,-s'\zeta\}\Big),

$\pi^2$ is an infimum over $y$ with $F'y=r$ of a supremum over $\hat{\mathcal V}$ of a Scarf-type expression, and $\pi^3$ is an infimum over $(s^0,s,x^0,x)$ with $x^0+x'g_\sigma=r^0$ , $F_\sigma'x=r$ that involves the function

\psi(x^0,x)=\inf_{\lambda>0}\frac{\lambda}{e}\exp\Big(\frac1\lambda\sup_{\hat z_\sigma\in\hat{\mathcal W}_\sigma}\{x^0+x'\hat z_\sigma\}+\frac{\|u\|_2^2}{2\lambda^2}\Big),\qquad u_j=\max\{x_j\sigma_{f,j},-x_j\sigma_{b,j}\}.

For $S\subseteq\{1,2,3\}$ the unified bound is the infimal convolution

\pi(r^0,r)=\min\Big\{\sum_{s\in S}\pi^s(r^{0,s},r^s):\ r^0=\sum_{s\in S}r^{0,s},\ r=\sum_{s\in S}r^s\Big\}.\qquad(25)

All values lie in $[-\infty,+\infty]$ , with the paper's convention that an infeasible minimization has value $+\infty$ and an infeasible maximization $-\infty$ .

Formalization targets

Goal: Theorem 4 (p. 911)

With $\mathbb F=\bigcap_{s\in S}\mathbb F_s$ ,

\sup_{\mathbb P\in\mathbb F}E_{\mathbb P}\big((r^0+r'\tilde\zeta)^+\big)\le\pi(r^0,r)\le\pi^s(r^0,r)\qquad\forall s\in S.\qquad(26)

Milestones

Theorem 1, upper-bound part: $\sup_{\mathbb F_1}E_{\mathbb P}((r^0+r'\tilde\zeta)^+)\le\pi^1(r^0,r)$ .
Theorem 2, upper-bound part: $\sup_{\mathbb F_2}E_{\mathbb P}((r^0+r'\tilde\zeta)^+)\le\pi^2(r^0,r)$ .
Theorem 3: $\sup_{\mathbb F_3}E_{\mathbb P}((r^0+r'\tilde\zeta)^+)\le\pi^3(r^0,r)$ .
The right inequality of (26): $\pi(r^0,r)\le\pi^s(r^0,r)$ for every $s\in S$ .

The tightness halves of Theorems 1 and 2 are the subject of the two companion missions of this series; Theorem 4 does not use them.

Significance

The unified bound turns heterogeneous partial information into one tractable upper bound. When a modeller knows a support set, a covariance and tail information for some independent factors, $\pi$ is valid for the intersected family and is never worse than the best of the separate bounds; it is the bound the paper's deflected and bideflected linear decision rules (§6, (31) onward) use for every recourse term. Theorem 4 is thus the guarantee behind the paper's main approximation scheme, and the same infimal-convolution device applies to any collection of valid bounds on a common convex objective.

The theorems are proved in the paper's electronic companion. To the knowledge of this mission none of them has a machine-checked proof: the Lean library has neither a Scarf-type bound nor a bound on expected positive parts from deviation measures. Formalizing Theorem 3 in particular produces reusable facts about moment generating functions of independent sums under deviation bounds.

Difficulty

The left inequality of (26) looks like bookkeeping, but it rests on three separate bounds, each with its own argument: a weak-duality argument for $\pi^1$ , a Scarf-type mean–variance inequality for $\pi^2$ , and an exponential-moment argument for $\pi^3$ that needs independence of the components of $\tilde z_\sigma$ to factor a moment generating function and the deviation bounds to control each factor. Each piece must be carried out with all values in the extended reals: suprema can be $+\infty$ , families can be empty, and a term equal to $-\infty$ in a sum can absorb a $+\infty$ . The right inequality depends on how each $\pi^s$ behaves at the zero objective, which for $\pi^3$ is an infimum over $\lambda>0$ that is not attained. The naive idea of proving (26) by attainment of the minimum in (25) does not work: the minimum need not be attained, and the statement must hold for every feasible split.

Formalization scope

A distribution is a Measure on Fin N_E → ℝ with IsProbabilityMeasure; $\tilde\zeta$ is the identity map. The mean is the published MomentDRO.Conf.meanVec. $\mathbb F_1$ and $\mathbb F_3$ require integrable coordinates and $\mathbb F_2$ finite second moments, so that means and covariances exist. $\mathbb P(\tilde\zeta\in\mathcal V)=1$ is an almost-everywhere statement. In $\mathbb F_3$ , independence is iIndepFun of the coordinates of $\tilde z_\sigma$ ; every exponential moment $E e^{\theta\tilde z_{\sigma,j}}$ is required finite; and the deviation bounds are the published predicates FwdDevLe, BwdDevLe applied to the law of each coordinate, which state $\frac{2}{\theta^2}\ln E e^{\theta(\tilde z_{\sigma,j}-\hat z_{\sigma,j})}\le\sigma_{f,j}^2$ for all $\theta>0$ , equivalent to the square-root form above for $\sigma_{f,j}\ge0$ .

Worst cases and bounds take values in EReal; the printed "min" of (25) and "inf" of (21), (22), (24) are read as infima, without attainment. In $\psi$ the supremum over $\hat{\mathcal W}_\sigma$ is taken outside the increasing exponential, which gives the same value whenever $\hat{\mathcal W}_\sigma$ is nonempty. The index set $S$ is a nonempty Finset (Fin 3) with index $0,1,2$ for the paper's $1,2,3$ , and vector indices are 0-based.

Two hypotheses come from the paper's model rather than its theorem statements: $\sigma_f,\sigma_b\ge0$ (deviations are square roots), and $F_\sigma\hat\zeta+g_\sigma\in\hat{\mathcal W}_\sigma$ for every $\hat\zeta\in\hat{\mathcal V}$ , which follows from $\hat{\mathcal W}_\sigma=H_\sigma\hat{\mathcal W}$ , $\hat{\mathcal V}=\{\hat\zeta:F\hat\zeta+g\in\hat{\mathcal W}\}$ , $F_\sigma=H_\sigma F$ and $g_\sigma=H_\sigma g$ (pp. 905, 908, 910).

The bounds are defined by (21), (22), (24) and (25) verbatim; a formalization that defines $\pi$ through the worst case itself, sets some $\pi^s$ to $+\infty$ , drops the exponential integrability from $\mathbb F_3$ , or uses real-valued suprema (which return $0$ on unbounded sets) would trivialize or falsify the statement and is ruled out.

Contributions welcome: proofs of the three upper bounds, a Scarf inequality $E X^+\le\frac12(EX+\sqrt{(EX)^2+\operatorname{Var}X})$ as a reusable lemma, and the EReal lemmas about infimal convolutions of extended-real functions.

Selected references

J. Goh, M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4):902–917, 2010. https://doi.org/10.1287/opre.1090.0795
X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441
W. Chen, M. Sim, Goal-Driven Optimization, Operations Research 57(2):342–357, 2009. https://doi.org/10.1287/opre.1080.0570
H. Scarf, A Min-Max Solution of an Inventory Problem, in Studies in the Mathematical Theory of Inventory and Production, K. Arrow, ed., Stanford University Press, 1958, 201–209.

10 thms2 active usersReviewed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Overbooking with Substitutable Inventory Classes: With Semigroup Survivals the Expected Net Revenue Is Componentwise Concave and Submodular in the Overbooking LevelsResearch Paper

Motivation

Airlines, hotels and car-rental firms sell reservations ahead of service, and a fraction of those reservations cancel or do not show up. Overbooking — accepting more reservations than there is capacity — recovers revenue that cancellations would otherwise destroy, at the risk of denying service to some customers. In practice inventory is often substitutable: a passenger booked in economy can be upgraded to business, a guest booked in a standard room can be given a suite. With substitution, the right overbooking level for one reservation class depends on the levels of all the others.

Karaesmen and van Ryzin (Operations Research 52(1):83–104, 2004) model this as a two-period problem: overbooking decisions in a reservation period, followed by an optimal assignment of the customers who actually show up to inventory classes in a service period. Their structural result, Theorem 2, establishes the shape of the expected net revenue as a function of the overbooking levels. That shape is what justifies critical-level booking policies and the stochastic-gradient method of their §4, and it is the textbook account of joint overbooking with substitution (Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004, Proposition 4.4).

Setting

There are $n$ reservation classes $i = 1, \dots, n$ and $m + 1$ inventory classes $j = 0, 1, \dots, m$ . Class $j = 0$ is virtual: assigning a customer to it means the customer is denied service.

Reservation period. The firm holds $x_i$ reservations of class $i$ and chooses overbooking levels $u_i \ge x_i$ . Accepting a class- $i$ reservation earns $r_i$ ; a cancellation of class $i$ is refunded $q_i$ , with $q_i \le r_i$ . The number of class- $i$ customers who survive to the service period is a random variable $Z_i(u_i)$ with values in $\{0, 1, 2, \dots\}$ . The family $\{Z_i(u_i)\}$ has the semigroup property: if $Y_1$ and $Y_2$ are independent with the laws of $Z_i(u_i)$ and $Z_i(s_i)$ , then $Y_1 + Y_2$ has the law of $Z_i(u_i + s_i)$ . The binomial model ( $Z_i(u_i) \sim \mathrm{Bin}(u_i, p_i)$ for integer $u_i$ ) and the Poisson model ( $Z_i(u_i) \sim \mathrm{Poisson}(u_i p_i)$ ) both have it. The survivals of different classes are independent.

Service period. Given the survivals $z = (z_1, \dots, z_n) \ge 0$ , net benefits $a_{ij}$ (of either sign) and capacities $c_j$ , the firm solves the transportation problem

V_0(z, c) = \max \sum_{i=1}^n \sum_{j=0}^m a_{ij} y_{ij} \quad \text{s.t.} \quad \sum_{j=0}^m y_{ij} = z_i, \ \ \sum_{i=1}^n y_{ij} \le c_j, \ \ y_{ij} \ge 0.

Expected net revenue. The objective of the reservation period is

G(u) = \sum_{i=1}^n r_i (u_i - x_i) - \mathbb E\Big[\sum_{i=1}^n q_i\big(u_i - Z_i(u_i)\big)\Big] + \mathbb E\big[V_0(Z(u), c)\big],

to be maximized over $u \ge x$ .

A function $f$ on $\mathbb R^n$ is submodular on $S$ if $f(s \vee s') + f(s \wedge s') \le f(s) + f(s')$ for $s, s' \in S$ , with $\vee, \wedge$ the componentwise maximum and minimum.

Formalization targets

Goal: Theorem 2

For every $u$ with levels in the parameter set $P$ , every class $i$ and all $\varepsilon, \alpha \in P$ ,

G(u + (\varepsilon + \alpha) e_i) - G(u + \alpha e_i) \le G(u + \varepsilon e_i) - G(u),

and $G$ is submodular on $P^n$ :

G(u \vee u') + G(u \wedge u') \le G(u) + G(u').

The first statement is the paper's componentwise concavity (6); the second is its submodularity, proved in the paper through the pairwise inequality (7) and Theorem 1.

Milestones

LP duality for the transportation problem (§2.2, p. 86): for $z \ge 0$ the primal attains its optimum and equals the dual optimum.
Lemma 1: $V_0(\cdot, c)$ is submodular on $\mathbb R^n_{\ge 0}$ .
Lemma 2: $V_0$ is concave in $(z_1, \dots, z_n)$ and concave in $(c_1, \dots, c_m)$ .
Theorem 1: on a product set, submodularity is equivalent to decreasing differences.
Under the semigroup property, $\mathbb E[Z_i(u_i)]$ is additive in $u_i$ .
The semigroup representation $\mathbb E[V_0(Z(u + \varepsilon e_i))] = \mathbb E[V_0(Z(u) + Y e_i)]$ with $Y$ independent of $Z(u)$ and distributed as $Z_i(\varepsilon)$ .
The sample-path inequalities of the proof: nonincreasing increments of $V_0$ along one coordinate, and the pairwise submodularity inequality for two coordinates.

Significance

Componentwise concavity of $G$ implies that for each reservation class there is a critical booking level beyond which expected revenue does not increase, other levels held fixed. Submodularity implies that these critical levels are nonincreasing in the bookings accepted for any other class: heavier overbooking in one class leaves less spare substitute capacity for the others. These two properties underpin the heuristics and the stochastic-gradient optimization of §4–§5 of the paper.

The result is proved in the paper (for $n = 2$ , with the general case described as straightforward). A machine-checked version would cover the general semigroup case, which includes the binomial model the paper calls realistic, real-valued levels and arbitrary step sizes. The platform already holds a proved special case, RevenueManagement.joint_overbooking_concave_submodular (Talluri–van Ryzin, Proposition 4.4): Poisson survivals, integer levels and unit steps only. This mission generalizes it in all three respects and also formalizes the transportation-problem facts (LP duality, submodularity and concavity of $V_0$ ) as reusable statements.

Difficulty

The obvious route — differentiate $G$ and use concavity of $V_0$ — fails twice. First, $V_0$ is piecewise linear and the survivals are discrete, so there is nothing to differentiate; under the binomial model $G$ is only defined at integer levels. Second, concavity of $V_0$ alone does not survive the expectation: $\mathbb E[V_0(Z(u))]$ is a mixture over laws that change with $u$ , and a concave function of a random vector whose law moves with the parameter need not be concave in the parameter. The semigroup property is what replaces a change of law by the addition of an independent block of survivors, and that coupling must be built for every coordinate and every pair of coordinates at once. On the LP side, submodularity of a transportation-problem value in its demands is a lattice-programming fact (Topkis, Theorem 3.4.1; Shapley 1962), not a consequence of concavity.

Formalization scope

All declarations are in the namespace SubstOverbooking.Structure. Reservation classes are Fin n (0-based), inventory classes Fin (m + 1) with 0 the virtual denied-service class. Conventions committed to:

Uncapacitated virtual class. The paper gives class 0 "finite but very high capacity" and then needs it to absorb every survivor; with Poisson survivals no finite capacity does. Constraint (4) is imposed only for $j \ne 0$ , $c_0$ is unused, and the dual fixes $\lambda_0 = 0$ . Capacities satisfy $c_j \ge 0$ for $j \ne 0$ .
$V_0$ on real demands. $V_0$ is the supremum of the TP objective over feasible assignments, for real $z$ ; every statement assumes $z \ge 0$ , where the supremum is attained and finite.
Survival laws. Each class has a family $u \mapsto L_i(u)$ of probability mass functions on $\mathbb N$ , with finite means. Levels range over a parameter set $P \subseteq [0, \infty)$ that contains $0$ and is closed under addition and under nonnegative differences: $P = \mathbb N$ covers the binomial model, $P = [0, \infty)$ the Poisson model. The semigroup property is the identity of laws $L_i(u + s) = (L_i(u) \otimes L_i(s)) \circ (+)^{-1}$ for $u, s \in P$ , and independence across classes is the product law.
Concavity is stated as the increment inequality (6), which is meaningful on a discrete $P$ ; submodularity of $G$ is lattice submodularity on $P^n$ via the published SupermodularOn applied to $-G$ .
Theorem 1 is stated for product sets $S = T_1 \times \dots \times T_n$ ; as printed for arbitrary $S \subset \mathbb R^n$ it is false, and every set the paper applies it to is a product.
The refund condition $q_i \le r_i$ is kept as a hypothesis of the goal, as on the page.

A formalization that fixes Poisson laws, integer levels or unit steps, or that defines $G$ or $V_0$ through the inequalities to be proved, is the already-proved special case or an empty statement, and is not the goal.

A complete development needs finite LP duality for the transportation problem, the lattice-programming argument for Lemma 1, product measures and image measures on $\mathbb N^n$ , and the coupling of the semigroup property. The LP and lattice parts are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Lemma 1 (for instance via monotonicity of optimal duals, after Erlenkotter 1970).

Selected references

I. Karaesmen and G. van Ryzin, Overbooking with Substitutable Inventory Classes, Operations Research 52(1):83–104, 2004. https://doi.org/10.1287/opre.1030.0079
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004, §4.4. https://doi.org/10.1007/b139000
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998, Theorem 3.4.1. https://doi.org/10.1515/9781400822539
R. K. Sundaram, A First Course in Optimization Theory, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511804526
L. S. Shapley, Complements and substitutes in the optimal assignment problem, Naval Research Logistics Quarterly 9(1):45–48, 1962. https://doi.org/10.1002/nav.3800090106
M. Shaked and J. G. Shanthikumar, Stochastic convexity and its applications, Advances in Applied Probability 20(2):427–446, 1988. https://doi.org/10.2307/1427398

11 thms2 active usersReviewed

Bandit Algorithms Operations Research·Captain: mikedeng1

Linearly Parameterized Bandits 2: Under Smooth Best Arm Response, the Phased Exploration and Greedy Exploitation Policy Has Regret at Most a₁(‖z‖ + 1/‖z‖)r√TResearch Paper

Motivation

In a linearly parameterized bandit, a decision maker repeatedly chooses an arm from a possibly infinite set of vectors and receives a noisy reward whose mean is linear in an unknown parameter. Classical bandit policies treat arms as independent and must try each arm, so their regret grows with the number of arms (Lai and Robbins 1985); in applications such as marketing, where similar products are expected to have similar sales, the linear structure lets one observation inform many arms, and the regret can be made independent of the number of arms. Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, Mathematics of Operations Research 2010) show that when the arms form the unit sphere of $\mathbb R^r$ , no policy has Bayes risk below order $r\sqrt T$ . This mission concerns their matching upper bound: a simple policy that alternates exploration and greedy exploitation in cycles of growing length attains regret of order $r\sqrt T$ whenever the best arm depends smoothly on the parameter.

The linearly parameterized bandit was studied earlier by Abe and Long (1999), Auer (2002) and, independently of this paper, Dani, Hayes and Kakade (2008), whose policies rely on confidence regions for the parameter. The result here shows that for arm sets with a smooth best arm, such as balls and, by Polovinkin (1996), ellipsoids, a phase-based policy with a single least squares estimate per cycle suffices.

Setting

Let $r \ge 2$ and let $\mathcal U_r \subset \mathbb R^r$ be a compact set of arms. Playing arm $u$ in period $t$ yields the reward

X^u_t = u'Z + W^u_t,

where $Z \in \mathbb R^r$ is an unknown parameter and the errors $W^u_t$ are independent of each other and of $Z$ , identically distributed in $t$ for each arm, with mean zero.

Assumption 1 fixes constants $\sigma_0, \bar u, \lambda_0 > 0$ that do not depend on $r$ : (a) every error satisfies $\mathbb E[e^{xW^u_t}] \le e^{x^2\sigma_0^2/2}$ for all $x \in \mathbb R$ ; (b) every arm has $\|u\| \le \bar u$ , and $\mathcal U_r$ contains linearly independent arms $b_1, \dots, b_r$ with $\lambda_{\min}(\sum_k b_kb_k') \ge \lambda_0$ .

The smooth best arm response condition SBAR( $J$ ) requires that every $z \ne 0$ have a unique best arm $u^*(z)$ , the maximizer of $v'z$ over $\mathcal U_r$ , and that $\|u^*(z) - u^*(y)\| \le J\|z - y\|$ for unit vectors $z, y$ .

The PEGE policy (Phased Exploration and Greedy Exploitation) runs in cycles $c = 1, 2, \dots$ . In cycle $c$ it plays $b_1, \dots, b_r$ once each, computes the ordinary least squares estimate

\widehat Z(c) = \frac1c\Big(\sum_{k=1}^r b_kb_k'\Big)^{-1}\sum_{s=1}^c\sum_{k=1}^r b_k X^{b_k}(s)

from all exploration rewards so far, and then plays a greedy arm $G(c) \in \arg\max_{v \in \mathcal U_r} v'\widehat Z(c)$ for $c$ periods, ties broken arbitrarily.

The regret given $Z = z$ over $T$ periods is $\mathrm{Regret}(z, T, \mathrm{PEGE}) = \sum_{t=1}^T \mathbb E[\max_{v \in \mathcal U_r} v'z - U_t'z \mid Z = z]$ , where $U_t$ is the arm played in period $t$ , and the risk is $\mathrm{Risk}(T, \mathrm{PEGE}) = \mathbb E[\mathrm{Regret}(Z, T, \mathrm{PEGE})]$ for a prior on $Z$ .

Formalization targets

Goal: Theorem 3.1 (p. 15)

Under Assumption 1 and SBAR( $J$ ), there is $a_1 > 0$ depending only on $\sigma_0, \bar u, \lambda_0, J$ such that for every $r \ge 2$ , every $z \ne 0$ and $T \ge r$ ,

\mathrm{Regret}(z, T, \mathrm{PEGE}) \le a_1\Big(\|z\| + \frac1{\|z\|}\Big) r\sqrt T,

and, if $\mathbb E\|Z\| \le M$ and $\mathbb E[1/\|Z\|] \le M$ for every $r$ , there is $a_2$ depending only on $\sigma_0, \bar u, \lambda_0, J, M$ with

\mathrm{Risk}(T, \mathrm{PEGE}) \le a_2\, r\sqrt T.

The constants are unspecified; only the order $r\sqrt T$ and its uniformity in $r$ are asserted.

Milestones on the way

Lemma 3.4 (p. 16): $\mathbb E[\|\widehat Z(c) - z\|^2 \mid Z = z] \le h_1 r/c$ .
Lemma 3.5 (p. 17): $\|w/\|w\| - z/\|z\|\| \le 2\|w - z\|/\max\{\|z\|, \|w\|\}$ .
Lemma 3.6 (p. 17): $\mathbb E[\max_{u} z'(u - G(c)) \mid Z = z] \le r h_2/(c\|z\|)$ .
Sec. 3.1 (p. 18): $\mathrm{Regret}(z, rK + \sum_{c=1}^K c, \mathrm{PEGE}) \le h_3 r\|z\|K + h_4\sum_{c=1}^K r/\|z\|$ .

Further results

Lemma 3.2 (p. 16): a density condition near the origin gives $\mathbb E[1/\|Z\|] \le M$ ; for $Z \sim N(0, I_r/r)$ , $\mathbb E\|Z\| \le 1$ and $\mathbb E[1/\|Z\|] \le \sqrt\pi$ .
The unit ball and the unit sphere satisfy SBAR(1) (pp. 15–16).
Corollary 3.3 (p. 16): on the unit sphere with standard normal errors, $\mathrm{Regret} \le a_3(\|z\| + 1/\|z\|)r\sqrt T$ and, under the prior $N(0, I_r/r)$ , $\mathrm{Risk} \le a_3 r\sqrt T$ .

Significance

Theorem 3.1 with the lower bound of Theorem 2.1 of the same paper identifies $r\sqrt T$ as the optimal order of the regret and the Bayes risk on the unit sphere, and Corollary 3.3 makes this precise. The bound is achieved by a policy with no confidence sets and no per-period optimization beyond one linear maximization per cycle. The factor $\|z\| + 1/\|z\|$ shows how the difficulty depends on the size of the parameter; combined with the trivial bound $2\bar u\|z\|T$ , the regret does not deteriorate as $\|z\| \to 0$ .

The results are proved in the paper; none of them is machine-checked. A formalization yields a verified dimension-explicit regret bound for an explore–exploit policy with a continuum of arms, the least squares error bound under sub-Gaussian noise (Lemma 3.4), and Lipschitz properties of normalization and of the best-arm map on balls, all of which are reusable.

Difficulty

The expected instantaneous regret of a greedy arm computed from a noisy estimate is not obviously small: for a general compact arm set the best arm may jump under a small perturbation of the parameter, and the regret is then of order $\|z\|$ however good the estimate is. The SBAR condition prevents such jumps, but only for unit vectors, so the estimation error must be transferred to the direction of the estimate, which costs a factor $1/\|z\|$ . The estimate may also vanish with positive probability when the errors are discrete, where the greedy arm is arbitrary. Finally, the constants must be uniform in the dimension $r$ : a bound with an $r$ -dependent constant is immediate from $\mathrm{Regret} \le 2\bar u\|z\|T$ , so the content of the theorem lies in keeping every constant independent of $r$ and of the arm set.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin r), so the norm is Euclidean and the inner product is $u'z$ . The model's standing assumptions are encoded as follows: $\mathcal U_r$ is compact; the errors of each arm have mean zero and a law $\nu_u$ ; Assumption 1(a) requires the moment generating function to exist and satisfy the sub-Gaussian bound; Assumption 1(b) writes $\lambda_{\min}(\sum_k b_kb_k') \ge \lambda_0$ as $\lambda_0\|x\|^2 \le \sum_k (b_k'x)^2$ . Every constant is quantified before the dimension $r$ , the arm set, the error laws, the exploration arms, the tie-breaking rule, the prior, $z$ and $T$ ; a version with constants depending on $r$ or on the instance is trivial and is excluded by this quantifier order.

PEGE uses exactly the exploration arms $b_k$ of Assumption 1(b), which are an argument of the policy. The greedy rule is any measurable selection of a maximizer; measurability, implicit on the page, is a hypothesis. Since PEGE uses only exploration rewards, the expectation is over an independent table of exploration errors $W^{b_k}(s)$ with laws $\nu_{b_k}$ , with the parameter fixed to $z$ ("given $Z = z$ "). Regret and risk are lower Lebesgue integrals of nonnegative gaps, valued in $[0, \infty]$ , so an upper bound is never satisfied by a default value of an integral. The moment conditions on the prior are lower Lebesgue integrals, so $\mathbb E[1/\|Z\|] = \infty$ if the prior charges the origin.

Two printed statements are adjusted. Lemma 3.6 is printed "for any $z \in \mathbb R^r$ ", but its bound $r h_2/(c\|z\|)$ is undefined at $z = 0$ ; it is stated for $z \ne 0$ . The p. 18 cycle-sum display is likewise stated for $z \ne 0$ . In Corollary 3.3, the exploration arms are those of Assumption 1(b) with $\bar u = \lambda_0 = 1$ , as in its proof. Measurability of the density in Lemma 3.2(a) is added.

The source is arXiv:0812.3465v2; its printed page numbers equal the PDF page numbers. Contributions welcome: proofs of the milestones, a sub-Gaussian least squares library, and the Lipschitz analysis of best-arm maps.

Selected references

P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, arXiv:0812.3465v2, 2010; Mathematics of Operations Research 35(2), 2010. https://arxiv.org/abs/0812.3465v2
V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT 2008. https://www.learningtheory.org/colt2008/papers/80-Dani.pdf
P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
E. S. Polovinkin, Strongly convex analysis, Sbornik: Mathematics 187(2), 1996. https://doi.org/10.1070/SM1996v187n02ABEH000111

13 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Distributionally Robust Optimization and Its Tractable Approximations 2: Under a Mean Set and a Known Covariance, the Bound π² Equals the Worst-Case Expected Positive PartResearch Paper

Motivation

Many operations models contain terms of the form $E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big)$ : expected shortfall or overflow of an affine function of an uncertain vector. Inventory and newsvendor costs, penalties for violated soft constraints, and the Conditional Value-at-Risk of a linear decision rule all reduce to it. In practice the distribution $\mathbb P$ of the uncertainty is rarely known; what is known are a few descriptive statistics, such as a range for the mean and an estimate of the covariance. Distributionally robust optimization then replaces the expectation by its supremum over every distribution consistent with that information.

The question goes back to Scarf (1958), who solved a single-product newsvendor problem against the worst distribution with known mean $\mu$ and variance $\sigma^2$ , using the fact that $\sup E(X^+) = \tfrac12\big(\mu + \sqrt{\mu^2 + \sigma^2}\big)$ over such laws; Gallego and Moon (1993) simplified the argument. El Ghaoui, Oks and Oustry (2003) obtained conic representations of worst-case Value-at-Risk under mean and covariance information, and Delage and Ye (2010) studied stochastic programs with uncertain mean and covariance. Goh and Sim (2010) use bounds of this kind inside a general framework for linear optimization under uncertainty with recourse: after a piecewise-linear decision rule is introduced, every expectation in the reformulated problem is of the form above, and the framework needs a tractable, ideally exact, value for its worst case. Section 5.2 of the paper provides it when the information consists of a set containing the mean and the exact covariance.

Setting

A primitive uncertainty $\tilde z \in \mathbb R^{N}$ is represented through a segregated uncertainty $\tilde\zeta \in \mathbb R^{N_E}$ , $N_E \ge N$ , and a fixed matrix $F \in \mathbb R^{N\times N_E}$ and vector $g \in \mathbb R^{N}$ with $\tilde z = F\tilde\zeta + g$ (equation (9) of the paper). The paper notes that $F$ has full row rank. Write $n = N_E$ .

The distributional information is:

a set $\hat{\mathcal V} \subseteq \mathbb R^{n}$ known to contain the mean $\hat\zeta = E_{\mathbb P}(\tilde\zeta)$ (the mean is uncertain, its "support" is $\hat{\mathcal V}$ );
the exact covariance $\Sigma \in \mathbb R^{N \times N}$ of the primitive vector $\tilde z$ .

The family is

\mathbb F_2 = \Big\{\mathbb P :\ \hat\zeta = E_{\mathbb P}(\tilde\zeta) \in \hat{\mathcal V},\ E_{\mathbb P}\big(F(\tilde\zeta - \hat\zeta)(\tilde\zeta - \hat\zeta)'F'\big) = \Sigma\Big\}.

For $r^0 \in \mathbb R$ and $r \in \mathbb R^{n}$ the worst-case expected positive part is $\sup_{\mathbb P \in \mathbb F_2} E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big)$ , and the bound of (22) is

\pi^2(r^0, r) = \inf_{y:\, F'y = r}\ \sup_{\hat\zeta \in \hat{\mathcal V}} \Big\{ \tfrac12 (r^0 + r'\hat\zeta) + \tfrac12 \sqrt{(r^0 + r'\hat\zeta)^2 + y'\Sigma y} \Big\}.

Following the paper (p. 909), an infeasible minimization has value $+\infty$ ; all values are in $[-\infty, +\infty]$ .

Formalization targets

Goal: Theorem 2 (p. 910)

For $F$ of full row rank, $\Sigma$ positive semidefinite and $\hat{\mathcal V}$ nonempty,

\sup_{\mathbb P \in \mathbb F_2} E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big) = \pi^2(r^0, r) \qquad \text{for all } r^0, r.

This is an exact identity; it contains no constants that later work could improve.

Milestones

Upper-bound part of Theorem 2: $\sup_{\mathbb F_2} E_{\mathbb P}((r^0 + r'\tilde\zeta)^+) \le \pi^2(r^0, r)$ , with no hypotheses.
Remark after Theorem 2: for $\Sigma \succeq 0$ , $f(u) = \tfrac12 u + \tfrac12\sqrt{u^2 + y'\Sigma y}$ is nondecreasing in $u$ .
(23): for $\Sigma \succeq 0$ and $\hat{\mathcal V} \neq \emptyset$ ,

\pi^2(r^0, r) = \inf_{u,\, y}\Big\{\tfrac12 u + \tfrac12\sqrt{u^2 + y'\Sigma y} :\ r^0 + \sup_{\hat\zeta \in \hat{\mathcal V}} r'\hat\zeta \le u,\ F'y = r\Big\}.

Tightness part of Theorem 2: $\pi^2(r^0, r) \le \sup_{\mathbb F_2} E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$ under the goal's hypotheses.

Significance

Theorem 2 says that the deterministic problem (22) evaluates the worst case exactly, not merely bounds it. Through (23) it becomes a second-order cone program whenever $\hat{\mathcal V}$ is conic representable, so distributionally robust constraints and objectives with mean–covariance information can be handed to an off-the-shelf conic solver without loss. In the paper, $\pi^2$ is one of three building blocks (with the mean–support bound $\pi^1$ and the directional-deviation bound $\pi^3$ ) that are combined by infimal convolution into the unified bound of Theorem 4, which in turn prices the deflected linear decision rules of §6. Specialized to $N = n$ , $F = I$ and a singleton mean set, it recovers Scarf's mean–variance bound.

The theorem is proved in the paper's online appendix; no machine-checked proof of it, nor of Scarf's bound in this multivariate form, is known to exist. A formalization would certify the exact value, including the cases the printed statement treats only implicitly: $r$ outside the range of $F'$ (both sides $+\infty$ ), a degenerate quadratic form $y'\Sigma y = 0$ , and unbounded mean sets.

Difficulty

The upper bound is a moment inequality and is the easier half. The difficulty is tightness. The supremum over $\mathbb F_2$ is in general not attained, so the proof must exhibit, for every point of $\hat{\mathcal V}$ , distributions on $\mathbb R^{n}$ that meet the full covariance constraint on $F\tilde\zeta$ exactly while driving the expected positive part of the single linear functional $r'\tilde\zeta$ to the bound. The constraint fixes $N(N+1)/2$ second moments, not just the variance of $r'\tilde\zeta$ , so the scalar extremal laws behind Scarf's bound do not directly give members of $\mathbb F_2$ . The case $F'y = r$ infeasible requires showing that the worst case is $+\infty$ , i.e. that $\mathbb F_2$ contains distributions with arbitrarily large expectations; this is where the full-rank assumption on $F$ enters.

Formalization scope

The random vector is the identity on Fin n → ℝ and a distribution is a measure P on it. The mean, the covariance matrix and the finite-second-moment condition come from the published definition MomentDRO_Conf_Setting (meanVec, covMat, HasSecondMoments). The covariance condition is $F\,\mathrm{Cov}_{\mathbb P}(\tilde\zeta)\,F' = \Sigma$ , which equals the paper's $E_{\mathbb P}(F(\tilde\zeta - \hat\zeta)(\tilde\zeta - \hat\zeta)'F')$ by linearity; it constrains the covariance of the primitive vector, an $N \times N$ matrix, not the covariance of $\tilde\zeta$ . The positive part is max · 0. The worst case and $\pi^2$ take values in EReal: an infimum over an empty set is $+\infty$ and a supremum over an empty set is $-\infty$ , matching the paper's convention for infeasible problems. The paper's "inf" and "sup" are not claimed to be attained.

Readings fixed by this mission, each implicit in the paper:

Full row rank of $F$ (p. 906, "F has to be full rank"), stated as surjectivity of $x \mapsto Fx$ ;
$\Sigma$ positive semidefinite, as a covariance matrix must be;
$\hat{\mathcal V}$ nonempty.

Each is needed for the equality: without it $\mathbb F_2$ can be empty (worst case $-\infty$ ) while $\pi^2$ is finite or $+\infty$ . No convexity or closedness of $\hat{\mathcal V}$ is assumed; the theorem does not need it. A formalization that takes the infimum in $\mathbb R$ (where an empty infimum is $0$ ) or states only the inequality $\le$ would trivialize or weaken the theorem and is ruled out.

A complete development needs a Scarf-type mean–variance inequality for $E(X^+)$ , constructions of multivariate distributions with a prescribed mean and covariance (Gaussian or finitely supported laws), and the monotonicity and continuity facts behind (23). The scalar inequality and the constructions of distributions with given first two moments are reusable well beyond this mission. Proofs of any milestone, and supporting lemmas on moment-constrained families, are welcome.

Selected references

J. Goh and M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4), 902–917, 2010. https://doi.org/10.1287/opre.1090.0795
H. Scarf, A min-max solution of an inventory problem, in K. Arrow (ed.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 201–209, 1958.
G. Gallego and I. Moon, The distribution free newsboy problem: Review and extensions, Journal of the Operational Research Society 44(8), 825–834, 1993. https://doi.org/10.1057/jors.1993.141
L. El Ghaoui, M. Oks and F. Oustry, Worst-case value-at-risk and robust portfolio optimization: A conic programming approach, Operations Research 51(4), 543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
E. Delage and Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3), 595–612, 2010. https://doi.org/10.1287/opre.1090.0741
X. Chen, M. Sim, P. Sun and J. Zhang, A linear decision-based approximation approach to stochastic programming, Operations Research 56(2), 344–357, 2008. https://doi.org/10.1287/opre.1070.0441

8 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Convex Quadratic and Semidefinite Programming Relaxations in Scheduling III: Optimal Nonpreemptive Schedules Are Within 3 of Preemptive Ones for R | rᵢⱼ | Σ wⱼCⱼ, Within 2 Without Release DatesResearch Paper

Motivation

In machine scheduling, preemption means that a job may be interrupted and resumed later, possibly on a different machine. Allowing it can only lower the optimal cost, and a basic question for every scheduling model is how much it can lower it: the ratio between the best nonpreemptive and the best preemptive schedule, often called the power of preemption. For identical parallel machines and the total weighted completion time, McNaughton (1959) showed that preemption does not help at all (doi:10.1287/mnsc.6.1.1). For unrelated machines, where every job has its own processing time on every machine, and with release dates, it does help, and no exact relation is known.

Skutella's paper (J. ACM 48 (2001), doi:10.1145/375827.375840) gives approximation algorithms for unrelated-machine scheduling based on convex quadratic programming relaxations. Its §4 adapts the relaxation of §3 to preemptive schedules and rounds it to a nonpreemptive schedule. A by-product is a constant bound on the power of preemption for $R\mid r_{ij}\mid\sum w_jC_j$ : the factor $3$ , and $2$ without release dates. This mission formalizes that bound together with the steps of §4 that produce it.

Setting

There are $n$ jobs $j$ and $m$ unrelated machines $i$ . Job $j$ has a weight $w_j\ge0$ , and on machine $i$ a processing time $p_{ij}>0$ and a release date $r_{ij}\ge0$ before which it may not be processed there.

A preemptive schedule is a finite list of pieces: job $j$ runs on machine $i$ during $[s,e]$ . Running job $j$ for $\ell$ time units on machine $i$ completes the fraction $\ell/p_{ij}$ of it. A schedule is feasible if every piece of $j$ on $i$ starts no earlier than $r_{ij}$ , two pieces on the same machine never overlap, two pieces of the same job never overlap, and the fractions of every job add up to exactly $1$ . The completion time $C_j$ is the end of the last piece of $j$ , and the objective is $\sum_j w_jC_j$ . A schedule is nonpreemptive if every job consists of a single piece.

Smith's order $\prec_i$ on machine $i$ orders the jobs by nonincreasing ratio $w_j/p_{ij}$ , ties broken by index. On each machine the release dates sorted nondecreasingly are $\rho_{i_1}\le\dots\le\rho_{i_n}$ , with $\rho_{i_{n+1}}:=\infty$ , and the time slot $i_k$ is $[\rho_{i_k},\rho_{i_{k+1}})$ . For a preemptive schedule, $a_{i_kj}$ is the fraction of job $j$ processed on machine $i$ inside slot $i_k$ . The convex quadratic program $(CQP'_p)$ asks for $a\ge0$ and $Z$ with $\sum_{i,k}a_{i_kj}=1$ , slot capacities $\sum_j a_{i_kj}p_{ij}\le\rho_{i_{k+1}}-\rho_{i_k}$ , $a_{i_kj}=0$ when $\rho_{i_k}<r_{ij}$ , and

Z\ \ge\ \sum_j w_j\sum_{i,k}a_{i_kj}\Bigl(\rho_{i_k}+\frac{a_{i_kj}}{2}p_{ij}+\sum_{j'\prec_ij}a_{i_kj'}p_{ij'}\Bigr),\qquad Z\ \ge\ \sum_j w_j\sum_{i,k}a_{i_kj}p_{ij}.

Randomized rounding puts job $j$ into slot $i_k$ with probability $a_{i_kj}$ , pairwise independently over jobs, and schedules each slot's jobs back to back in Smith's order from the slot's start.

Formalization targets

Goal: Corollary 4.6, the power of preemption

For every feasible preemptive schedule $P$ there is a feasible nonpreemptive schedule $S$ with

\sum_j w_jC_j(S)\ \le\ 3\sum_j w_jC_j(P),

and if all $r_{ij}=0$ , one with $\sum_j w_jC_j(S)\le 2\sum_j w_jC_j(P)$ . This is the paper's ratio of optima, stated so that no existence of optimal schedules is needed.

Milestones

(24): $\sum_j w_jC_j\ge\sum_j w_j\sum_{i,k}a_{i_kj}p_{ij}$ for every preemptive schedule.
Exchange inequality (proof of Lemma 4.2): inside one slot, Smith's order minimizes $\sum_j a_jw_j\sum_{j'\text{ before }j}a_{j'}p_{ij'}$ over all orders.
(25): the bound (23) with $\prec_i$ replaced by the order of completion times in the schedule.
Lemma 4.2: every preemptive schedule satisfies (23) and (24).
$(CQP'_p)$ is a relaxation: the fractions of every preemptive schedule, with $Z=\sum_j w_jC_j$ , are feasible.
Lemma 4.3: rounding any feasible $(\bar a,Z)$ yields feasible nonpreemptive schedules with $\mathbb E[\sum_j w_jC_j]\le 3Z$ , and $\le 2Z$ when all release dates are $0$ .

Significance

The result gives a constant bound on how much preemption can help on unrelated machines with release dates, a model in which both the preemptive and the nonpreemptive problems are NP-hard (for the preemptive problem even without weights and release dates, by Sitters, J. Algorithms 57 (2005), doi:10.1016/j.jalgor.2004.06.011). The bound comes from an algorithm: a single relaxation that is valid for preemptive schedules, rounded to a nonpreemptive one. The same rounding is a randomized $3$ -approximation for $R\mid r_{ij},pmtn\mid\sum w_jC_j$ and a $2$ -approximation for $R\mid pmtn\mid\sum w_jC_j$ (Theorem 4.5), and since it never preempts, these bounds hold under any communication delays between machines.

The paper proves all of this on paper. As far as a search of the platform shows, none of it is formalized: the only formal preemption result found is McNaughton's theorem for identical machines. The mission produces a machine-checked model of preemptive schedules on unrelated machines with release dates, a checked lower bound on such schedules by a convex quadratic function of their slot fractions, and a checked analysis of pairwise-independent rounding into nonpreemptive schedules.

Difficulty

The natural first idea is to reuse the nonpreemptive relaxation $(CQP)$ of §3, which already allows fractional assignments. It fails. Example 4.1 of the paper gives two jobs on two machines where an optimal preemptive schedule costs $7$ but the corresponding $(CQP)$ value is $7.25$ , so $(CQP)$ is not a relaxation of the preemptive problem. The relaxation must be weakened: the term $(1+a_{i_kj})/2$ of §3 becomes $a_{i_kj}/2$ , and this weakening is what raises the factor from $2$ to $3$ .

Proving that the weaker program is a relaxation (Lemma 4.2) takes real work. The fractions of a job inside a slot of an arbitrary preemptive schedule are scattered, so the bound needs a rearrangement inside each slot by completion times, then an exchange argument that compares this order with Smith's order slot by slot. On the rounding side, Lemma 4.3 reduces to the analysis of §3 (each job's expected completion time is at most twice its value in the relaxation) and, without release dates, to Theorem 2.1 of §2. Both have to be redone here on the slot model.

Formalization scope

Jobs, machines and slots are Fin n, Fin m, Fin n (0-based). The standing assumptions $p_{ij}>0$ , $w_j\ge0$ , $r_{ij}\ge0$ of p. 2 are hypotheses of every theorem. Smith's order is cross-multiplied ( $w_jp_{ik}>w_kp_{ij}$ ), equivalent to the ratio form because $p>0$ . Sorted release dates come from Tuple.sort. The last slot of each machine has no right end, so $\rho_{i_{n+1}}=\infty$ is never a real number, and the slot capacity constraint is imposed only for slots with a successor. A preemptive schedule is a List of pieces with migration allowed and any number of pieces; nonpreemptive means one piece per job. Completion time is the latest end time among a job's pieces.

Added constraint. The display of $(CQP'_p)$ on p. 22 omits the condition $a_{i_kj}=0$ if $\rho_{i_k}<r_{ij}$ (constraint (18) of §3). Without it the rounding can place a job in a slot that opens before its release date, and "computes a nonpreemptive schedule" in Lemma 4.3 fails. It is included here. The fractions of every feasible preemptive schedule satisfy it, so the program remains a relaxation.

Randomized rounding is a probability weight on the finite set of slot assignments with marginals $\bar a$ and pairwise products $\bar a\bar a'$ . Pairwise independence is required, full independence is not, and the expectation is a finite sum. "Without nontrivial release dates" is read as $r_{ij}=0$ for all $i,j$ . Communication delays are not modelled: without them the preemptive class is the largest, so the goal implies the bound for every delay model.

Not formalized: polynomial running time, solving $(CQP'_p)$ within an additive error $\varepsilon$ , derandomization by conditional probabilities (Theorem 4.5), and Corollary 4.4.

The goal is not trivial. Feasible preemptive schedules exist and are not vacuous, since each job's fractions must sum to $1$ and no machine runs two pieces at once. The nonpreemptive schedule is required to be feasible in the same model, and its value is compared with the given schedule's real objective, not with a relaxation value.

A complete development needs: the slot schedule (15)–(17) and its feasibility, the bound $\mathbb E[C_j]\le2\bar C_j$ of §3 (Lemma 3.5) and Theorem 2.1 of §2, both restated on this slot model, and a product-measure argument showing that pairwise-independent rounding exists. The preemptive-schedule model and the slot machinery are reusable for other unrelated-machine results. Contributions to any milestone are welcome, and so are alternative proofs of Lemma 4.2.

Selected references

M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, J. ACM 48(2) (2001) 206–242. https://doi.org/10.1145/375827.375840
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
R. McNaughton, Scheduling with deadlines and loss functions, Management Science 6(1) (1959) 1–12. https://doi.org/10.1287/mnsc.6.1.1
A. S. Schulz and M. Skutella, Scheduling unrelated machines by randomized rounding, SIAM J. Discrete Math. 15(4) (2002) 450–469. https://doi.org/10.1137/S0895480199357078
R. Sitters, Complexity of preemptive minsum scheduling on unrelated parallel machines, J. Algorithms 57(1) (2005) 37–48. https://doi.org/10.1016/j.jalgor.2004.06.011

10 thms2 active usersReviewed

Missions

A Note on Probability Distributions with Increasing Generalized Failure Rates I: X Is IGFR iff log X Is IFR iff X ⪯hr λX for All λ ≥ 1 iff Φ̄(ξ/θ) Is TP₂Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 603)

Milestones (the clauses of the proof)

Companion statements

Significance

Difficulty

Formalization scope

Selected references

Primal and Dual Linear Decision Rules in Stochastic and Robust Optimization 2: With Random Recourse, the SDP (3.14) Conservatively Approximates the Linear Decision Rule Problem, Exactly for l = 1Research Paper

Linear decision rules for stochastic programs with random recourse

Setting

Formalization targets

Goal: Theorem 2, primal half (p. 17)

Milestones

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Goal: Theorem 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Independent products in real L1: asymptotic midpoint convexity without AUC renormingsOpen Problem

Motivation

Setting

Formalization target

Significance and status

Difficulty

Formalization scope

Selected references

Threshold parallel repetition for finite-dimensional entangled gamesOpen Problem

Motivation

Setting

Formalization target

Significance and status

Difficulty

Formalization scope

Selected references

Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive DisorderOpen Problem

Motivation

Setting

Formalization target

Significance and status

Difficulty

Formalization scope

Selected references

Optimal-order mixing of the Thorp shuffleOpen Problem

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Renewal and changes of law for critical honeycomb walksOpen Problem

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

The exact reconstruction threshold for the three-state symmetric channelOpen Problem

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope