Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Functional Analysis Harmonic Analysis·Captain: mikedeng1

Isotropic Gaussian Random Fields on the Sphere: Regularity, Fast Simulation and Stochastic Partial Differential Equations I: u ∈ V^η(−1,1) iff Σ u_ℓ²(2ℓ+1)(1+ℓ^{2η}) < ∞Research Paper

Motivation

A centered isotropic Gaussian random field $T$ on the unit sphere $\mathbb S^2$ is determined by its angular power spectrum $(A_\ell)_{\ell \ge 0}$ : its covariance is

\mathbb E\big(T(x)T(y)\big) = \sum_{\ell=0}^\infty A_\ell\,\frac{2\ell+1}{4\pi}\,P_\ell(\langle x,y\rangle) = k_I(\langle x, y\rangle),

with $P_\ell$ the Legendre polynomials. Such fields model the cosmic microwave background and other data on the sphere (Marinucci and Peccati, 2011). In applications one often prescribes the kernel $k_I$ rather than the spectrum, while simulation and error analysis (the Karhunen–Loève truncation, sample regularity, approximation of stochastic PDEs on the sphere) are governed by the decay of $A_\ell$ . Section 3 of Lang and Schwab (2015) connects the two: the regularity of $k_I$ on $[-1,1]$ , measured in weighted Sobolev spaces, is equivalent to weighted square summability of $(A_\ell)$ . The authors call this result, Theorem 3.1, their main result.

This mission is the first of four from the same paper; the others treat sample Hölder regularity, Karhunen–Loève truncation rates and a stochastic heat equation.

Setting

Functions are real functions on the open interval $(-1,1)$ .

The Legendre polynomials are $P_\ell(\mu) = 2^{-\ell}\frac{1}{\ell!}\frac{\partial^\ell}{\partial\mu^\ell}(\mu^2-1)^\ell$ , $\ell \in \mathbb N_0$ .
The Fourier–Legendre coefficients of $u \in L^2(-1,1)$ are $u_\ell = \int_{-1}^1 u(x)P_\ell(x)\,dx$ , so that $u = \sum_\ell u_\ell \frac{2\ell+1}{2}P_\ell$ in $L^2(-1,1)$ . With $A_\ell = 2\pi u_\ell$ this is the kernel expansion above.
For $j \in \mathbb N_0$ the weighted seminorm is $|u|^2_{V^j(-1,1)} = \int_{-1}^1 |\partial^j u(\mu)|^2(1-\mu^2)^j\,d\mu$ , and $\|u\|^2_{V^n(-1,1)} = \sum_{j=0}^n |u|^2_{V^j(-1,1)}$ . The weighted Sobolev space $V^n(-1,1)$ is the closure of the smooth functions in this norm. The weight $(1-\mu^2)^j$ vanishes at the endpoints, so for $n \ge 1$ the space $V^n(-1,1)$ is strictly larger than the Sobolev space $H^n(-1,1)$ .
For $n < \eta < n+1$ , the space $V^\eta(-1,1)$ is the real interpolation space $(V^n(-1,1), V^{n+1}(-1,1))_{\eta-n,2}$ , with norm $\|u\|^2_{V^\eta} = \int_0^\infty t^{-2(\eta-n)}|K(t,u)|^2\,\frac{dt}{t}$ , where $K(t,u) = \inf_{u=v+w}(\|v\|_{V^n}+t\|w\|_{V^{n+1}})$ is the K-functional.
The weighted sequence space $\ell_\eta$ is $\ell^2$ with weights $\frac{2\ell+1}{2}(1+\ell^{2\eta})$ .

Formalization targets

Goal: Theorem 3.1 (p. 11)

For $\eta \ge 0$ there are constants $c_1, c_2 > 0$ such that for every $u \in L^2(-1,1)$ : $u \in V^\eta(-1,1)$ if and only if the weighted sum is finite, and then

c_1\sum_{\ell=0}^\infty u_\ell^2\,\frac{2\ell+1}{2}\,(1+\ell^{2\eta}) \;\le\; \|u\|^2_{V^\eta(-1,1)} \;\le\; c_2\sum_{\ell=0}^\infty u_\ell^2\,\frac{2\ell+1}{2}\,(1+\ell^{2\eta}).

The constants depend on $\eta$ only. They are not given explicitly, and the goal does not fix them.

Milestones

Orthogonality of the derivatives (pp. 12–13): for $n \le \ell, \ell'$ , $\int_{-1}^1 P_\ell^{(n)}P_{\ell'}^{(n)}(1-\mu^2)^n\,d\mu = \delta_{\ell\ell'}\frac{2}{2\ell+1}\frac{(\ell+n)!}{(\ell-n)!}$ .
Weighted Parseval identity (p. 13): $|u|^2_{V^n} = \sum_{\ell \ge n}u_\ell^2\frac{2\ell+1}{2}\frac{(\ell+n)!}{(\ell-n)!}$ for smooth $u$ .
Factorial bounds (p. 13): $c_1(n)\ell^{2n} \le (\ell+n)!/(\ell-n)! \le c_2(n)\ell^{2n}$ for $n \le \ell$ .
The integer case (pp. 11–12): $V^n(-1,1) \cong \ell_n$ through $u \mapsto (u_\ell)$ , with equivalent norms.
Stein–Weiss for weighted $\ell^2$ (cited on p. 12): $(\ell^2(w_0),\ell^2(w_1))_{\theta,2} = \ell^2(w_0^{1-\theta}w_1^\theta)$ with equivalent norms.
Weight equivalence (p. 12): $\big(\frac{2\ell+1}{2}(1+\ell^{2n})\big)^{1-\theta}\big(\frac{2\ell+1}{2}(1+\ell^{2(n+1)})\big)^{\theta} \simeq \frac{2\ell+1}{2}(1+\ell^{2(n+\theta)})$ , uniformly in $\ell$ .

Significance

For an isotropic field, Theorem 3.1 turns a question about the kernel into a question about the spectrum. A kernel of prescribed smoothness has a spectrum with prescribed weighted summability, and conversely. Decay rates of $(A_\ell)$ control the truncation error of the Karhunen–Loève expansion and the convergence rates of spectral methods for SPDEs on the sphere, which the later sections of the paper derive. Theorem 3.1 lets these rates be stated in terms of kernel regularity. The weighted spaces $V^\eta(-1,1)$ are the natural ones because the weight $(1-\mu^2)^j$ reflects the singularity of $\mu = \cos\vartheta$ at the poles.

The theorem has a published proof; to our knowledge no part of it has been machine-checked. A Lean development would give Lean its first weighted Sobolev spaces on an interval, the first K-functional and real interpolation spaces in a concrete setting, the Stein–Weiss identification for weighted $\ell^2$ , and the orthogonality relations of the derivatives of Legendre polynomials (equivalently, of Gegenbauer polynomials). None of these is in Mathlib.

Difficulty

The integer case is a computation once the orthogonality and Parseval identities are available. Its difficulty is analytic: the closure $V^n(-1,1)$ consists of functions whose classical derivatives need not exist up to the endpoints, so the Parseval identity has to be passed from smooth functions to limits. One then has to check that the closure norm is well defined, i.e. that the weighted norm is closable.

The fractional case does not follow by applying the integer formula with $n$ replaced by $\eta$ , because $V^\eta(-1,1)$ is defined by interpolation and not by a fractional derivative. The paper transfers the isomorphism $V^n \cong \ell_n$ , $V^{n+1} \cong \ell_{n+1}$ to the interpolation spaces through the interpolation property of the real method. This requires a single map that is an isomorphism at both levels at once, plus the Stein–Weiss description of the interpolated sequence space. Neither the interpolation property nor Stein–Weiss is available in Lean.

Formalization scope

Functions are ℝ → ℝ. Every definition looks only at their values on $(-1,1)$ : $L^2$ membership and convergence are with respect to Lebesgue measure on the open interval, and decompositions $u = v + w$ hold almost everywhere there.
$V^n(-1,1)$ is the closure of the $C^\infty$ functions on $\mathbb R$ , not of $H^n(-1,1)$ as on the page. The two closures coincide, since smooth functions are dense in $H^n(-1,1)$ and the $H^n$ norm dominates the $V^n$ norm. Membership requires an approximating sequence that converges in $L^2(-1,1)$ and is Cauchy for the weighted norm. The norm is the limit of the weighted norms along such a sequence.
Norms, K-functionals, interpolation norms and weighted sums are valued in $[0,+\infty]$ , so " $< +\infty$ " is a genuine condition and no undefined integral or infimum takes a default value. The paper's $\eta \in \mathbb R_+$ is taken as $\eta \ge 0$ ; the case split $\eta \in \mathbb N_0$ versus $n < \eta < n+1$ is exactly the paper's. Powers $\ell^{2\eta}$ are real powers with $0^0 = 1$ .
The constants of the norm equivalences are quantified before the function $u$ (respectively before $\ell$ , or before the weights in the Stein–Weiss milestone). With the constants after $u$ the equivalence would be trivial, and that reading is excluded.
Correction: the page states the weighted Parseval identity for $k_I$ with the factor $\frac{2\ell+1}{2(4\pi)^2}$ . From the orthogonality relation the factor is $\frac{2(2\ell+1)}{(4\pi)^2}$ , which is $\frac{2\ell+1}{2}$ in terms of $u_\ell$ . The milestone is stated in the $u_\ell$ form; finiteness statements are unaffected.
Not formalized: the second paragraph of Theorem 3.1, which restates the integer case through weak derivatives of $k_I$ ; Theorem 3.2 (the $\mathbb S^{d-1}$ version); and Proposition A.4 of the appendix.

Contributions are welcome on all six milestones. The orthogonality and Parseval milestones need only polynomial calculus and interval integrals. The Stein–Weiss milestone is a self-contained statement about weighted sequences and can be reused well beyond this mission.

Selected references

A. Lang, Ch. Schwab, Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations, Ann. Appl. Probab. 25(6), 2015, 3047–3094; arXiv:1305.1170v3 (cited version). https://arxiv.org/abs/1305.1170, https://doi.org/10.1214/14-AAP1067
J. Bergh, J. Löfström, Interpolation Spaces: An Introduction, Grundlehren 223, Springer, 1976. https://doi.org/10.1007/978-3-642-66451-9
H. Triebel, Interpolation Theory, Function Spaces, Differential Operators, 2nd ed., Johann Ambrosius Barth, Heidelberg, 1995 (ISBN 3-335-00420-5).
G. Szegő, Orthogonal Polynomials, 4th ed., AMS Colloquium Publications 23, 1975. https://doi.org/10.1090/coll/023
D. Marinucci, G. Peccati, Random Fields on the Sphere, London Math. Soc. Lecture Note Series 389, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511751677

11 thms2 active usersReviewed

Machine Learning Operations Research Optimization·Captain: mikedeng1

A Modern Introduction to Online Learning IX: Cover's Universal Portfolio with Uniform or Dirichlet(1/2) Prior Has Logarithmic Regret Against Constantly Rebalanced PortfoliosTextbook

Why sequential portfolios matter

A portfolio manager chooses fractions of current wealth to place in several stocks before seeing that day’s market gains. The gains need not follow a statistical model: a sequence may be selected adversarially, with some stocks losing all value on a given day. A useful benchmark is the best constantly rebalanced portfolio, which holds the same fractions each day but trades at the end of every round to restore them. Its fixed allocation is an active strategy, and it can grow even when buying and holding each individual stock does not. Chapter 10 of Orabona’s online learning text studies guarantees against this benchmark without imposing a positive lower bound or a finite upper bound on nonzero market gains.

The chapter presents a universal portfolio: an allocation determined by a prior distribution over all fixed portfolios and reweighted according to their wealth so far. The mission focuses on the uniform-prior part of Theorem 10.1. It asks for a worst-case logarithmic regret guarantee against every fixed comparator and every admissible market sequence. This is a deterministic guarantee; no distributional assumption about the market enters its statement.

Market and strategy

There are $d\ge2$ stocks and $T\ge1$ rounds. In round $t$ , the market supplies a vector $w_t\in\mathbb R_{≥0}^d\setminus\{0\}$ of nonnegative gains. A portfolio is $u\in\Delta^{d-1}$ , the simplex of vectors with nonnegative coordinates summing to one. If one unit is invested initially and the allocation stays fixed, its wealth after $T$ rounds is

W_T(u)=\prod_{t=1}^{T}\langle w_t,u\rangle.

A sequential strategy chooses $x_t\in\Delta^{d-1}$ before seeing $w_t$ , and has wealth $W_T=\prod_{t=1}^{T}\langle w_t,x_t\rangle$ . The quantity of interest is the difference between the logarithms of benchmark wealth and sequential wealth. A fixed portfolio can have zero wealth when all the stocks it holds have a zero gain on some day; its log wealth is then $-\infty$ in the mathematical convention of the book.

Algorithm 10.1 begins with a prior $F$ on the simplex. Before round $t$ , it gives each fixed portfolio $u$ weight proportional to its wealth $W_{t-1}(u)$ , and chooses the resulting mean allocation:

x_t(i)=\frac{\int_{\Delta^{d-1}}u_i W_{t-1}(u)\,F(du)}{\int_{\Delta^{d-1}}W_{t-1}(u)\,F(du)}.

For this mission, $F$ is the uniform probability measure on the simplex. It is represented by Lebesgue measure in the first $d-1$ coordinates, scaled by $(d-1)!$ ; the final coordinate is one minus their sum. This explicit density fixes what “uniform” means and prevents the prior from being chosen to suit a particular market sequence.

Formalization targets

The goal is the uniform-prior case of Theorem 10.1. With the notation above, for every fixed portfolio of positive wealth,

\log W_T(u)-\log W_T \le \log\binom{T+d-1}{d-1} \le (d-1)\left[\log\left(\frac{T}{d-1}+1\right)+1\right].

The goal also asserts $W_T>0$ , so the algorithm’s logarithmic wealth is defined. The first inequality gives an exact finite-horizon combinatorial bound; the second displays its logarithmic dependence on $T$ for fixed $d$ . The book also states a Dirichlet $(1/2,\ldots,1/2)$ prior bound in the same theorem. That companion branch is not among this proposal’s draft items; its gamma-function normalization and integral identities would require a separate audited definition layer. The fixed series title follows the chapter plan, while the goal and milestone list specify the precise scope delivered here.

The attack path records four source statements. Lemma 10.5 bounds a ratio of nonnegative sums by the largest component ratio. Lemma 10.6 reduces a universal portfolio’s wealth ratio to a maximum over sequences of single-stock choices. Theorem 10.4 bounds the size of a type class, the set of sequences with the same empirical fractions of symbols. Equation (10.5) computes the monomial integral under the uniform simplex prior. These statements are from the chapter’s proof of Theorem 10.1; the equation is referred to as an exercise in Problem 10.3.

What the result provides

The theorem ensures that the uniform-prior strategy keeps its log wealth within $O(d\log(1+T/d))$ of the best constantly rebalanced portfolio, while making no bounded-gain assumption. In particular, a stock may have gain zero on one day or a very large gain on another. The guarantee is pathwise: it applies to the realized market vectors, regardless of how they were chosen. For a fixed number of stocks, dividing regret by $T$ therefore gives a vanishing average shortfall in log wealth.

The mathematical result is already proved in the cited text. This mission’s work is to give its exact algorithm, prior measure, combinatorial objects, and finite-horizon constants machine-checked statements and then proofs. The density-based prior, finite type classes, and simplex monomial integrals can also be reused in online aggregation and universal coding developments. The draft statements currently have Lean placeholders for proofs; a successful submission will still require solvers to close them.

Main difficulty

Applying a generic online convex optimization bound to the loss $-\log\langle w_t,x\rangle$ runs into unbounded gradients when a chosen portfolio has small gain. A bound based on one global Lipschitz constant cannot cover the market sequences allowed here. The integral strategy creates a different obstacle: its denominator must be positive at every round, including histories with zero gains for many fixed portfolios. Its uniform prior is a measure on a $(d-1)$ -dimensional simplex embedded in $\mathbb R^d$ , so ambient $d$ -dimensional volume would give it mass zero. A proof must work with the intrinsic coordinate measure and its normalization. The exact binomial coefficient also depends on counting all sequences of one type without losing the boundary cases where some symbol occurs zero times.

Formalization scope

Lean represents a portfolio as a function Fin d → ℝ in Mathlib’s stdSimplex; a market is a one-based sequence of vectors of the same type. The coordinate chart maps $\mathbb R^{d-1}$ into the simplex, and a scaled restricted Lebesgue measure is pushed forward to define the uniform prior. The chart’s measurability is proved in the definition file. Algorithm 10.1 is a componentwise ratio of real integrals, and the main theorem asserts positive realized wealth. All market vectors on rounds $1,\ldots,T$ are nonnegative and nonzero. The parameter restrictions $d\ge2$ and $T\ge1$ make the dimension and printed denominators meaningful.

For Lemma 10.5, quotients use extended nonnegative reals, with $a/0=+\infty$ when $a>0$ and $0/0=0$ as printed. Lemma 10.6 is stated for a generic prior concentrated on the simplex, with its ratios in extended nonnegative reals under the same conventions, and with the hypothesis that the normalizing integral of Algorithm 10.1 is positive in every round, which is what makes the algorithm's prediction defined. A comparator with zero wealth is omitted only from the real-log statement, corresponding to log wealth $-\infty$ in the source. The prior cannot be replaced by an arbitrary point mass: the theorem names the chart-based uniform measure, and the prediction is the exact integral ratio. Contributions proving normalization, support, the integral identity, and the final regret bound are all within scope.

Selected references

Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 10 and Appendix A.2.2. arXiv

7 thms2 active usersReviewed

Functional Analysis Number Theory·Captain: waitingintime

Connes–Weil arithmetic lower bound: cofinal actual-quartet certificatesOpen Problem

Why an arithmetic lower bound is needed

The Riemann hypothesis asks whether every nontrivial zero of the actual Riemann zeta function has real part one half. The Connes formalization has a certified implication from positivity of the Weil distribution to RH. That implication supplies a criterion; its positivity hypothesis still needs a proof. The Green realization formalization supplies an independently certified physical carrier, actual-zero columns and bounded synthesis operators. Their construction does not establish the arithmetic inequality.

This open problem isolates a finite-certificate formulation of that inequality. The goal is new research within the existing formal development, not a theorem asserted by the cited papers. It is an RH-equivalent target. A proof of the reductions below is already available; a proof of the target itself is not.

The relevant historical distinction is explicit: Riemann stated the zero-location hypothesis in 1859; Connes' 1999 paper relates trace-formula and positivity questions to the zeros; the present Lean development certifies the conditional positivity criterion and the Green realization. None of these citations is offered as an unconditional proof of the new arithmetic certificate bound.

Actual zeros and the fixed physical carrier

Let $Z$ be the subtype of complex numbers $\rho$ satisfying $\zeta(\rho)=0$ and $0<\operatorname{Re}\rho<1$ . Multiplicities are the existing natural analytic multiplicities. Reflection is $\rho\mapsto1-\overline\rho$ , and conjugation is $\rho\mapsto\overline\rho$ . For each actual zero, let $S_\rho$ be its finite reflection/conjugation orbit, called its quartet. Repeated orbit elements are removed by the finite-set construction, so the term does not assert four distinct zeros.

At a positive support radius $T$ , the physical carrier $H_T$ is the existing closed Dirichlet energy-image completion on $[-T,T]$ . Its energy convention is the integral of $|u'|^2+|u|^2/4$ . Source lifts, Green columns and their pair normalization retain their published definitions. The original admissible tests are smooth compactly supported functions; the carrier is not defined from an arbitrary replacement zero family.

Write $p_{T,\tau}$ for the original positive column of an actual zero $\tau$ , with the original reflected-pair and multiplicity normalization. Their complete squared-norm sum is certified summable at each positive radius. For a finite set $F\subset Z$ , $P_F$ is the published synthesis of exactly these positive columns into $H_T$ . Let $N_S$ be the original selected negative synthesis on the coefficient space for the unchanged quartet $S=S_\rho$ .

Formalization target

For a positive accuracy $\delta$ , define the already-published operators

B_F=P_F^*P_F+\delta I_F,\qquad C_{F,S}=P_F^*N_S,

and the selected coefficient correction

D_S(T,F,\delta)=\delta I_S-N_S^*N_S+C_{F,S}^*B_F^{-1}C_{F,S}.

The positive regularization makes $B_F$ strictly positive, including dependent or repeated columns. Its ring inverse is certified to be a genuine inverse for positive $\delta$ .

The goal is

\forall\rho\in Z\;\forall b\in\mathbb R\;\exists T>\max(b,0)\;\forall\delta>0\;\exists F\subset Z\text{ finite}:

S_\rho\subseteq F,\quad F\text{ is reflection-closed},\quad \sum_{\tau\notin F}\|p_{T,\tau}\|^2<\delta,\quad D_{S_\rho}(T,F,\delta)\succeq0.

Here $T>\max(b,0)$ abbreviates the two strict inequalities in the Lean statement. The window is chosen before accuracy. The finite cutoff can depend on accuracy, but the selected negative quartet remains unchanged. The same accuracy occurs in the complete omitted tail and the correction operator.

What this target would establish

The certified fixed-window theorem identifies all-accuracy finite certificates with the original Picard marker being at least half the identity. The certified cofinal quartet criterion identifies arbitrarily large such quartet windows with Mathlib's Riemann hypothesis. Their composition has also been checked independently in the native Lean environment against the exact goal statement.

These two reductions are the principal milestones, alongside the existing literature-form positivity implication. Shared definitions and supporting theorems remain reusable library nodes. Certification of a reduction is distinct from establishing the nonnegative correction demanded by the goal. The goal is currently unproved and carries no RH or desired-positivity hypothesis.

The remaining difficulty

Finite tail cutoffs exist by summability, and regularized coefficient inverses exist by strict positivity. Those facts leave the sign of $D_S$ undetermined. An arithmetic representation of the full Weil operator alone also leaves that sign undetermined. The selected negative packet and the unselected negative background are different parts of the original signed operator; replacing one by the other changes the obligation.

The arithmetic transfer audit ZP-WEIL-MARKER-TRANSFER / RH-ZERO-PROV-2 records this distinction. Endpoint estimates or neutral-shell arguments contribute only when they supply the original lower bound with the required window and accuracy quantifiers. A bound at one boundary, an accuracy-dependent choice of window, or an estimate with a positive residual error floor does not supply the displayed target. No easier status is implied by its finite coefficient representation.

Formalization scope

The proposal uses Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474, with the published original quartet and selected-correction definitions. A separate native audit uses the existing Lean 4.34.0 repository environment. Complex Hilbert inner products are conjugate-linear in the first argument. Operator nonnegativity uses the existing continuous-linear-map order. Infinite tails are unordered sums on the actual-zero complement.

No simple-zero assumption, independence of columns, unregularized Gram inverse, replacement carrier, changed coefficient metric or silently restricted zero family is permitted. Quartets include zeros on the critical line; an empty actual-zero subtype would make the universal target vacuous, exactly as specified by the existing actual-zero indexing. New auxiliary definitions belong in shared definition bundles, and reusable algebraic lemmas belong in the library. The existing Green milestone history and dependency graph are retained.

Selected references

B. Riemann, Ueber die Anzahl der Primzahlen unter einer gegebenen Grösse, Monatsberichte der Berliner Akademie, 1859. Original paper and translations.
A. Connes, Trace formula in noncommutative Geometry and the zeros of the Riemann zeta function, Selecta Mathematica 5, 1999. arXiv:math/9811068. Source of the conditional positivity/RH context, not the new certificate inequality.
H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Springer, 2011. DOI. Functional-analytic background for the certified carrier.
Published Lean results: cofinal quartet criterion, fixed-window selected certificates, and selected-correction definitions.
monocap-tech/provenance, RH-ZERO-PROV-2 arithmetic-transfer checkpoint, 2026. Its stated status is representation complete, lower-bound theorem open, RH not proved.

Literature and source audit

The exact cofinal-quartet finite-certificate goal remains open. An independent Lean audit verifies its equivalence to Mathlib RiemannHypothesis by composing the two certified milestone reductions. The window is chosen before every positive regularization parameter; the selected actual-zero quartet is fixed, and the same parameter controls the full positive tail and selected correction. Tail summability and existence of inverses alone do not establish the required sign.

The foreign graph export ConnesRZ.weil_positivity_implies_RH matches the native ConnesRZClosed.weil_positivity_implies_RH: the older native ConnesRZ theorem takes explicitFormula as an input, discharged in Closed. The foreign record has a staged source qualification; it has not been edited.

Arithmetic transfer checkpoint: monocap-tech/provenance 178c83225b2300506ff622899d08ec3c987137d5, rh/checkpoints/RH_ZERO_PROV_2_EULER_WEIL_MARKER_TRANSFER_20260920.md, SHA256 0bb48b950f09220f7b2f193c16b45b15add0333906f919f8b50ca915f77a1a0d. Retained local Git bytes were verified; public availability is unverified. Critical-window location, the prescribed ordered-limit interface, and arithmetic endpoint/neutral-shell control remain open. RH is not established.

7 thms2 active usersReviewed

Combinatorics Linear algebra Markov Chain+1·Captain: mikedeng1

High Order Random Walks: Beyond Spectral Gap 1: On a One-Sided λ-Local Spectral Expander, ‖M⁺_k φ‖ ≤ ((k+1)/(k+2) + (k+1)λ/2)‖φ‖ for Every k-Cochain φ Orthogonal to the ConstantsResearch Paper

Motivation

A high dimensional expander is a simplicial complex whose local structure forces global expansion. The high order random walks on such a complex move from a $k$ -face to a $k$ -face through a common $(k+1)$ -face. They were studied for their connection to agreement tests in probabilistically checkable proofs (Dinur–Kaufman 2017; Kaufman–Mass 2017), and they later became a tool for sampling. Anari, Liu, Oveis Gharan and Vinzant (arXiv:1811.01816) used the mixing bound of this mission to prove the Mihail–Vazirani conjecture: the bases-exchange walk of every matroid mixes rapidly.

Timeline:

1973. Garland (Ann. of Math. 97) shows that spectral gaps in the links of a complex control its cohomology. Inner products are localized to links; this is now called Garland's method.
2017. Kaufman and Mass (arXiv:1604.02947) bound the second eigenvalue of the high order walks on complexes with well-expanding links. Dinur and Kaufman obtain the optimal bound under a two-sided spectral gap in the links, as Kaufman–Oppenheim explain.
2018. Oppenheim (Discrete Comput. Geom. 59) shows how spectral gaps descend from top-dimensional links to lower ones ("trickling down").
2017–2021. Kaufman and Oppenheim (arXiv:1707.02799v3) obtain the optimal mixing bound under a one-sided gap only: negative eigenvalues of the links do not matter. This is the target of this mission.

Setting

Let $V$ be a type of vertices. A pure $n$ -dimensional finite simplicial complex $X$ is a finite family of finite subsets of $V$ that is closed under subsets, has faces of at most $n+1$ elements, and has every face contained in a face of exactly $n+1$ elements. A face with $k+1$ elements is a $k$ -face; $X(k)$ is the set of $k$ -faces, and $X(-1)=\{\emptyset\}$ .

A weight function is a map $m$ from the faces of $X$ to $(0,\infty)$ that is balanced: for $-1\le k\le n-1$ and $\tau\in X(k)$ ,

m(\tau)=\sum_{\sigma\in X(k+1),\ \tau\subseteq\sigma}m(\sigma).

A $k$ -cochain is a function $\phi:X(k)\to\mathbb R$ . The cochains carry the inner product $\langle\phi,\psi\rangle=\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)\psi(\sigma)$ and the norm $\|\cdot\|$ . The cochains orthogonal to the constants form $C^k_0(X,\mathbb R)=\{\phi:\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)=0\}$ .

The upper random walk $M^+_k$ acts on $k$ -cochains by

M^+_k\phi(\tau)=\frac{1}{k+2}\,\phi(\tau)+\sum_{\tau'\in X(k),\ \tau\cup\tau'\in X(k+1)}\frac{m(\tau\cup\tau')}{(k+2)\,m(\tau)}\,\phi(\tau').

It stays put with probability $1/(k+2)$ , and otherwise moves to a neighbouring $k$ -face with probability proportional to the weight of their union.

The link of a face $\tau$ is $X_\tau=\{\eta\in X:\eta\cap\tau=\emptyset,\ \tau\cup\eta\in X\}$ , weighted by $m_\tau(\eta)=m(\tau\cup\eta)$ . On the vertices of $X_\tau$ , the non-lazy upper walk $(M')^+_{\tau,0}=2M^+_{\tau,0}-I$ is the weighted random walk on the 1-skeleton of the link. Let $\mu_\tau$ be its second largest eigenvalue. $X$ is a one-sided $\lambda$ -local spectral expander if $\mu_\tau\le\lambda$ for every face $\tau$ of dimension $-1,\dots,n-2$ . The empty face is included, and its link is $X$ itself.

Formalization targets

Goal: Theorem 5.4 (p. 17)

Let $0\le\lambda\le1$ and let $X$ be a one-sided $\lambda$ -local spectral expander. Then for every $0\le k\le n-1$ and every $\phi\in C^k_0(X,\mathbb R)$ ,

\|M^+_k\phi\|\le\Big(\frac{k+1}{k+2}+\frac{k+1}{2}\,\lambda\Big)\|\phi\|.

Milestones

They follow the paper's proof order:

Lemma 3.6 and Corollary 3.7: the adjoint $d^*$ of the signless differential $d$ , and the factorizations $d^*d=(k+2)M^+_k$ , $dd^*=(k+1)M^-_k$ .
Proposition 4.1 (1)–(3), Garland's localization identities, and Proposition 4.2:

\|d\phi\|^2=\|d^*\phi\|^2+\|\phi\|^2+\sum_{\tau\in X(k-1)}\langle (M')^+_{\tau,0}(I-M^-_{\tau,0})\phi_\tau,\phi_\tau\rangle .

Lemma 4.3, which bounds the link terms by $(k+1)\mu\|\phi\|^2$ .
Lemma 5.1.
Theorem 5.2 (the Decomposition Theorem).
Corollary 5.3, in its general and its one-sided form:

\|d\phi\|^2\le\sum_{j=0}^{k}\Big(k+1-j+\frac{(k+j+2)(k+1-j)}{2}\lambda\Big)\|\phi^j\|^2,\qquad \|\phi\|^2=\sum_{j=0}^k\|\phi^j\|^2.

Significance

The result. The coefficient $\frac{k+1}{k+2}$ is the baseline in the paper's mixing bound, and the bound is optimal up to the $O(\lambda)$ term. It needs a gap on one side only: links may have eigenvalues near $-1$ . This matters in two places. The links of a matroid's independence complex are only one-sided expanders, so the matroid application needs exactly this case. And the links of Ramanujan complexes are one-sided expanders, so this bound gives optimal mixing on them; the two-sided bound of Dinur–Kaufman does not apply to them.

Formalizing it. The theorem is proved on paper; the Lean statements in this mission are proof targets. Completing the mission would give machine-checked proofs of the mixing bound, Garland's localization identities, and the Decomposition Theorem, built on definitions of weighted simplicial complexes, links, and their random walks. Lemma 4.3 and Corollary 5.3 are stated with a correction: as printed they are false when a link eigenvalue bound is negative (see Formalization scope).

Difficulty

The obvious argument fails. The tempting route bounds the second eigenvalue of $M^+_k$ directly from the link spectra, by induction on $k$ . But $M^+_k$ has large eigenvalues near $\frac{k+1-j}{k+2}$ for every $j$ , coming from cochains of the form $d\psi$ with $\psi$ of lower degree. A single spectral-gap estimate cannot separate these levels from one another. The paper instead splits $\phi$ into contributions from every degree $j\le k$ ; this is the Decomposition Theorem, and each piece is controlled separately. Formally, the main costs are:

the double-counting behind Proposition 4.1 (Appendix A, pp. 28–29);
a square root of a positive self-adjoint operator on a weighted finite-dimensional space (Theorem 5.2);
the bookkeeping of degrees and links.

Formalization scope

Faces are Finset V. $X$ is a Finset (Finset V), and $X(k)$ is cells X (k + 1): faces are indexed by their number of vertices. Cochains are functions Finset V → ℝ that are read only on the relevant faces. Every operator is zero off $X$ . The weight is positive on faces; the paper writes $\mathbb R^+$ , and $m$ appears in denominators. Every goal-level statement carries the standing assumption of §2: $X$ is pure $n$ -dimensional and $m$ is a weight. Orthogonality to the constants is always weighted by $m$ (or by $m_\tau$ in a link).

The adjoint $d^*$ is defined by its explicit formula; that it is the adjoint is Lemma 3.6. The eigenvalue condition $\mu_\tau\le\lambda$ is stated in Rayleigh form: $\langle (M')^+_{\tau,0}g,g\rangle\le\lambda\|g\|^2$ for every $g$ on the vertices of $X_\tau$ that is $m_\tau$ -orthogonal to the constants. It is equivalent to the eigenvalue form even for disconnected links. A Rayleigh bound over all $g$ , constants included, would be unsatisfiable for $\lambda<1$ and would make the goal vacuous; it is ruled out. The predicate quantifies over every face of dimension $-1$ to $n-2$ , including $\emptyset$ .

Corrections, all disclosed in the items:

Lemma 4.3 is stated with a bound $\mu\ge\max(\mu_k,0)$ . The printed version with $\mu_k<0$ fails already for the complete graph on three vertices.
Corollary 5.3 accordingly takes $\mu_i\ge0$ and $\lambda\ge0$ . Its two formal statements retain the page's assumption that every link of dimension at least one is connected, including $X$ itself.
The proof of Theorem 5.4 ends with $(k+1)\lambda$ ; the statement's $\frac{k+1}{2}\lambda$ is formalized.

Welcome contributions: proofs of any milestone. Reusable lemmas on finite weighted inner products, on double counting over faces of a Finset (Finset V), and on links are useful beyond this mission; the companion mission on two-sided expanders uses the same objects.

Selected references

T. Kaufman, I. Oppenheim, High Order Random Walks: Beyond Spectral Gap, arXiv:1707.02799v3, 2021. https://arxiv.org/abs/1707.02799
N. Anari, K. Liu, S. Oveis Gharan, C. Vinzant, Log-concave polynomials II: High-dimensional walks and an FPRAS for counting bases of a matroid, STOC 2019. https://arxiv.org/abs/1811.01816
H. Garland, p-adic curvature and the cohomology of discrete subgroups of p-adic groups, Ann. of Math. 97:375–423, 1973. https://doi.org/10.2307/1970781
T. Kaufman, D. Mass, High dimensional random walks and colorful expansion, ITCS 2017. https://arxiv.org/abs/1604.02947
I. Oppenheim, Local spectral expansion approach to high dimensional expanders Part I: Descent of spectral gaps, Discrete Comput. Geom. 59(2):293–330, 2018. https://arxiv.org/abs/1709.04431

13 thms2 active usersReviewed

Linear algebra Mathematical Physics Quantum Information·Captain: mikedeng1

Quantum Algorithm for Simulating Real Time Evolution of Lattice Hamiltonians 2: Strictly Local Lieb–Robinson Bound ‖[A_X(t),B_Y]‖ ≤ 2‖A‖‖B‖|X|(2ζ₀|t|)^ℓ/ℓ! with ℓ = ⌊dist(X,Y)⌋Research Paper

Motivation

Simulating the time evolution $e^{-iHt}$ of a many-body Hamiltonian is one of the main proposed uses of quantum computers. For a Hamiltonian $H = \sum_X h_X$ whose terms act on small, nearby groups of sites of a lattice, Haah, Hastings, Kothari and Low give a quantum algorithm whose gate count is nearly linear in the space-time volume $n t$ , and show that this is optimal up to logarithmic factors. The algorithm decomposes $e^{-iHt}$ into evolutions of overlapping blocks, and the error of each step is controlled by a Lieb–Robinson bound: in a locally interacting system, an operator evolved for time $t$ stays, up to a superexponentially small error, inside a region whose size grows linearly with $t$ .

Lieb–Robinson bounds go back to Lieb and Robinson (1972), who proved a finite propagation speed for quantum spin systems. Hastings (2004), Nachtergaele and Sims (2006) and Hastings and Koma (2006) gave the commutator form used today and applied it to the decay of correlations in gapped ground states. Appendix C of the paper re-derives the bound in a self-contained way. Section C.4 treats strictly local interactions, where every term is supported on a set of diameter at most $1$ , and obtains a bound with an explicit factor $(2\zeta_0|t|)^\ell/\ell!$ . This mission formalizes that bound.

Setting

Let $\Lambda$ be a finite set of sites with a metric $\mathrm{dist}$ . Every site carries $\mathbb{C}^q$ , and operators act on $\bigotimes_{x \in \Lambda} \mathbb{C}^q$ ; all norms $\|\cdot\|$ are operator norms. An operator is supported on $X \subseteq \Lambda$ if it has the form $m \otimes \mathbb{1}_{\Lambda \setminus X}$ . For finite sets of sites, $\mathrm{dist}(X, Y) = \min_{x \in X, y \in Y} \mathrm{dist}(x, y)$ , $\mathrm{diam}(X) = \max_{x, x' \in X} \mathrm{dist}(x, x')$ , and $X \sim Y$ means $X \cap Y \ne \emptyset$ .

A Hamiltonian is a family $(h_X)_{X \subseteq \Lambda}$ of Hermitian operators, $h_X$ supported on $X$ , with $H = \sum_{X \subseteq \Lambda} h_X$ ; for a region $\Omega$ , $H_\Omega = \sum_{Z \subseteq \Omega} h_Z$ . The Heisenberg evolution of an operator $O$ is $O(t; J) = e^{iJt} O e^{-iJt}$ , and $O(t) = O(t; H)$ . The interaction is strictly local if $h_X = 0$ whenever $\mathrm{diam}(X) > 1$ , and its strength is measured by

\zeta_0 = \max_{x \in \Lambda} \sum_{Q \ni x} |Q|\, \|h_Q\| .

The proof works with two auxiliary quantities attached to a fixed operator $B$ supported on $Y$ :

C_B(X, t) = \sup_{A \in \mathcal{A}_X,\ \|A\| \le 1} \|[A(t), B]\|, \qquad D_B(X, t) = \|[h_X(t), B]\|,

where $\mathcal{A}_X$ is the algebra of operators supported on $X$ . A tuple $(Z_1, \dots, Z_k)$ is linked from $X$ if $X \sim Z_1 \sim \cdots \sim Z_k$ .

Formalization targets

Goal: display (48)

For $A$ supported on $X$ , $B$ supported on $Y$ , $\ell = \lfloor \mathrm{dist}(X, Y) \rfloor$ and every real $t$ ,

\|[A(t), B]\| \le 2\,\|A\|\,\|B\|\,|X|\,\frac{(2\zeta_0|t|)^{\ell}}{\ell!} .

Milestones

The elementary bounds (28): $C_B(Z, 0) \le 2\|B\|\delta_{Z \sim Y}$ , $C_B(Z, t) \le 2\|B\|$ , and the same for $D_B$ with an extra factor $\|h_Z\|$ .
The integral inequality (24): $C_B(X, t) \le C_B(X, 0) + \sum_{Z \sim X} 2\int_0^{|t|} D_B(Z, s)\, ds$ .
The closed recursion (42): $C_B(X, t) \le C_B(X, 0) + 2\sum_{Z : X \sim Z} \|h_Z\| \int_0^{|t|} C_B(Z, s)\, ds$ .
The truncated iteration (44): $C_B(X, t) \le 2\|B\| \frac{(2|t|)^\ell}{\ell!} \sum_{Z_1, \dots, Z_\ell : \text{linked}} \prod_j \|h_{Z_j}\|$ .
The counting bounds (45)–(46): $\sum_{Q : P \sim Q \sim S} \|h_Q\| \le \zeta_0 \sum_{p \in P} \delta_{\mathrm{dist}(p, S) \le 1}$ and its weighted, distance-tracking companion.
Lemma 5, eq. (4) = (49): $\|O_X(t; H) - O_X(t; H_\Omega)\| \le |X|\,\|O_X\|\,(2\zeta_0|t|)^\ell/\ell!$ with $\ell = \lfloor \mathrm{dist}(X, \Lambda \setminus \Omega) \rfloor$ , under the added hypothesis $\mathrm{dist}(X, \Lambda \setminus \Omega) \ge 1$ .

The goal is (48) rather than Lemma 5 because (48) is proved in full on pp. 26–27, while Lemma 5 is obtained "by manipulation analogous to Eq. (39)" and is false as printed when $\ell = 0$ .

Significance

The bound (48) states that commutators with distant operators are suppressed by a factor that, at fixed $t$ , decays faster than any exponential in the distance. The same factor controls Lemma 5, which is what the decomposition lemmas of the paper (Lemma 6 and its corollaries) use to bound the error of replacing a global evolution by evolutions of overlapping blocks; that in turn gives the paper's gate counts. Bounds of this type also underlie the exponential clustering of correlations in gapped ground states and the quasi-adiabatic continuation technique.

The results are proved in the literature and in this paper. A search of the local Prove2Me prior-art index found no matching formal statement for this finite spin-system bound. The mission seeks a machine-checked proof of the strictly local bound with its explicit constant, together with reusable infrastructure: operators supported on subsets of a tensor product of matrix algebras, their Heisenberg evolution, and an integral inequality for commutator growth.

Difficulty

The obvious argument expands $A(t) = \sum_k (it)^k \mathrm{ad}_H^k(A)/k!$ and notes that the first $\ell$ nested commutators with $B$ vanish. This does not give the stated bound: the norm of $\mathrm{ad}_H^k(A)$ grows like $k!$ times the number of growing clusters of terms, and the tail of the series is not controlled by its leading term. The explicit factor $(2\zeta_0|t|)^\ell/\ell!$ , with no exponential prefactor, requires precise control of the time-dependent supremum $C_B(Z,s)$ and the combinatorics of linked chains. A second difficulty is Lemma 5, whose printed form is false at $\ell = 0$ and whose proof in the paper is a one-line reference to an analogous computation.

Formalization scope

Sites are an arbitrary finite metric space $\Lambda$ ([Fintype Λ] [MetricSpace Λ]); operators are matrices Matrix (Λ → Fin q) (Λ → Fin q) ℂ in the product basis, with the same local dimension $q$ at every site. This generalizes the paper's qubits on a lattice in $\mathbb{R}^D$ . The norm is the $L^2$ operator norm (Matrix.Norms.L2Operator), never the entrywise or Frobenius norm. SupportedOn X M states $M = m \otimes \mathbb{1}$ entrywise, and is not vacuous: a nonzero operator on a single site satisfies it, and only scalars are supported on $\emptyset$ . The Hamiltonian is time-independent and sums over every subset of $\Lambda$ ; strict locality is the hypothesis $1 < \mathrm{diam}(X) \Rightarrow h_X = 0$ on the terms. The constant $\zeta_0$ is carried as an upper bound of the site sums $\sum_{Q \ni x} |Q|\,\|h_Q\|$ , which is equivalent to the paper's maximum for these monotone bounds; no bound $\|h_X\| \le 1$ is assumed. $\mathrm{dist}(X, Y)$ is a minimum over nonempty sets and $0$ if a set is empty, $\ell$ is its natural-number floor, and $C_B$ is a real supremum over a nonempty set bounded by $2\|B\|$ . The integral milestones (24) and (42) are stated for $t \ge 0$ ; the goal, (44) and Lemma 5 hold for every real $t$ . Lemma 5 carries one disclosed added hypothesis, $\mathrm{dist}(x, y) \ge 1$ for $x \in X$ , $y \notin \Omega$ , without which it is false.

None of the statements is trivialized: the goal mentions neither $C_B$ nor linked sums, its norm is the operator norm, the integrals are of continuous functions on compact intervals, the supremum is over a nonempty bounded set, and no disjointness of $X$ and $Y$ is assumed, so it covers $\ell = 0$ as well.

A complete development needs the derivative of $t \mapsto e^{iHt} A e^{-iHt}$ , unitarity of $e^{iHt}$ for Hermitian $H$ , commutation of operators with disjoint supports, Grönwall-type iteration of integral inequalities, and the simplex-volume identity $\int_{\Delta^k} dt = |t|^k/k!$ . The support and evolution layer is reusable for any lattice-system result. Contributions that prove the milestones in order, or that develop the support calculus independently, are welcome.

Selected references

J. Haah, M. B. Hastings, R. Kothari, G. H. Low, Quantum algorithm for simulating real time evolution of lattice Hamiltonians, SIAM J. Comput. (2021); arXiv:1801.03922v4 (2020). https://arxiv.org/abs/1801.03922
E. H. Lieb, D. W. Robinson, The finite group velocity of quantum spin systems, Comm. Math. Phys. 28 (1972) 251–257. https://doi.org/10.1007/BF01645779
M. B. Hastings, Lieb–Schultz–Mattis in higher dimensions, Phys. Rev. B 69 (2004) 104431. https://arxiv.org/abs/cond-mat/0305505
B. Nachtergaele, R. Sims, Lieb–Robinson bounds and the exponential clustering theorem, Comm. Math. Phys. 265 (2006) 119–130. https://arxiv.org/abs/math-ph/0506030
M. B. Hastings, T. Koma, Spectral gap and exponential decay of correlations, Comm. Math. Phys. 265 (2006) 781–804. https://arxiv.org/abs/math-ph/0507008

10 thms2 active usersReviewed

Machine Learning Optimization Probability·Captain: mikedeng1

Stochastic Model-Based Minimization of Weakly Convex Functions 2: The Proximal Stochastic Subgradient Method Drives E‖∇φ_{1/ρ̄}(x_{t*})‖² to Zero at Rate O(1/√T)Research Paper

Motivation

The proximal stochastic subgradient method is the workhorse of large-scale learning: to minimize a regularized population risk $\varphi(x) = f(x) + r(x)$ with $f(x) = \mathbb E_{\xi \sim P}[f(x,\xi)]$ , it samples a data point, takes a step against a sampled subgradient of $f$ , and applies the proximal map of the regularizer $r$ . Its sample complexity is classical for convex problems ( $O(\varepsilon^{-2})$ samples for function accuracy $\varepsilon$ ) and for smooth nonconvex problems ( $O(\varepsilon^{-4})$ samples for gradient norm $\varepsilon$ , Ghadimi–Lan 2013). For problems that are both nonsmooth and nonconvex, however, no complexity bound was known for any reasonably broad class before Davis–Drusvyatskiy 2019.

Many such problems — robust phase retrieval, nonlinear least squares with an $\ell_1$ loss, conditional value-at-risk minimization with smooth losses, covariance estimation — are weakly convex: they become convex after adding a quadratic $\frac{\rho}{2}\|x\|^2$ . This mission formalizes the complexity guarantee of Davis and Drusvyatskiy for the proximal stochastic subgradient method on weakly convex problems.

Timeline. Nurminskii (1973) showed that for weakly convex $f(\cdot,\xi)$ and $r = 0$ the stochastic subgradient method has limit points that are stationary, without a rate. Ghadimi and Lan (2013) proved the $O(\varepsilon^{-4})$ rate for smooth $f$ . Davis and Drusvyatskiy (arXiv 2018, SIAM J. Optim. 2019) proved the first rate for the proximal stochastic subgradient method under weak convexity, measured by the gradient of the Moreau envelope; this is Theorem 3.4 of their paper.

Setting

Work in $\mathbb R^d$ with the Euclidean norm. Let $r : \mathbb R^d \to \mathbb R \cup \{+\infty\}$ be closed (its epigraph is closed) and convex, with nonempty domain $D = \operatorname{dom} r$ , and let $f : \mathbb R^d \to \mathbb R$ be $\rho$ -weakly convex: $x \mapsto f(x) + \frac{\rho}{2}\|x\|^2$ is convex. Set $\varphi = f + r$ .

The subdifferential $\partial\psi(x)$ of a function $\psi$ at a point $x$ of its domain is the set of vectors $v$ with $\psi(y) \ge \psi(x) + \langle v, y - x\rangle + o(\|y - x\|)$ as $y \to x$ ; it is empty off the domain. For $\lambda > 0$ the Moreau envelope and the proximal map are

\psi_\lambda(x) = \min_y \Big\{\psi(y) + \tfrac{1}{2\lambda}\|y - x\|^2\Big\}, \qquad \operatorname{prox}_{\lambda\psi}(x) = \operatorname*{argmin}_y \Big\{\psi(y) + \tfrac{1}{2\lambda}\|y - x\|^2\Big\}.

Assumption A (stochastic subgradient oracle): on a probability space $(\Omega, \mathcal F, P)$ one can draw i.i.d. samples $\xi_0, \xi_1, \dots \sim P$ (A1); there are an open set $U \supseteq D$ and a measurable map $G$ with $\mathbb E_\xi[G(x,\xi)] \in \partial f(x)$ for all $x \in U$ (A2); and $\mathbb E_\xi\|G(x,\xi)\|^2 \le L^2$ for all $x \in D$ (A3).

Algorithm 3.1 starts at $x_0 \in D$ and, for $t = 0, \dots, T$ , samples $\xi_t$ and sets $x_{t+1} = \operatorname{prox}_{\alpha_t r}(x_t - \alpha_t G(x_t, \xi_t))$ . It returns $x_{t^*}$ with $t^*$ drawn from $\{0, \dots, T\}$ with probability $\alpha_t / \sum_i \alpha_i$ .

Formalization targets

Goal: Theorem 3.4, (3.15) and (3.16)

For $\bar\rho \in (\rho, 2\rho]$ and stepsizes $\alpha_t \in (0, 1/\bar\rho]$ ,

\mathbb E\big[\|\nabla\varphi_{1/\bar\rho}(x_{t^*})\|^2\big] \le \frac{\bar\rho}{\bar\rho - \rho}\cdot\frac{\big(\varphi_{1/\bar\rho}(x_0) - \min\varphi\big) + 2\bar\rho L^2\sum_{t=0}^T\alpha_t^2}{\sum_{t=0}^T\alpha_t},

and with $\alpha_t = \gamma/\sqrt{T+1}$ , $\gamma \in (0, \frac{1}{2\rho}]$ ,

\mathbb E\big[\|\nabla\varphi_{1/(2\rho)}(x_{t^*})\|^2\big] \le 2\cdot\frac{\big(\varphi_{1/(2\rho)}(x_0) - \min\varphi\big) + 4\rho L^2\gamma^2}{\gamma\sqrt{T+1}}.

Milestones

In the order the proof uses them: Lemma 2.1 (subdifferential characterization of weak convexity), the existence of $\hat v_t \in \partial f(\hat x_t)$ with $\bar\rho(x_t - \hat x_t) \in \partial r(\hat x_t) + \hat v_t$ (§3.2), Lemma 3.2 ( $\hat x_t$ is a proximal point of $r$ ), Lemma 3.3 (one-step contraction towards $\hat x_t$ ), Lemma 2.2 (the envelope is $C^1$ with $\nabla\varphi_\lambda(x) = \lambda^{-1}(x - \operatorname{prox}_{\lambda\varphi}(x))$ ), and the one-step descent estimate (3.14).

Significance

The result. A small $\|\nabla\varphi_\lambda(x)\|$ certifies that $x$ is within $\lambda\|\nabla\varphi_\lambda(x)\|$ of a point $\hat x$ with $\varphi(\hat x) \le \varphi(x)$ and $\operatorname{dist}(0, \partial\varphi(\hat x)) \le \|\nabla\varphi_\lambda(x)\|$ . Theorem 3.4 therefore gives a sample complexity of $O(\varepsilon^{-4})$ for reaching an $\varepsilon$ -nearly stationary point, matching the smooth rate, for a method that is run in practice without modification. The underlying observation — the method is an approximate descent method on the Moreau envelope — is reused in the paper's model-based analysis (Theorem 4.3) and in subsequent work on stochastic nonsmooth nonconvex optimization.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A complete development produces reusable infrastructure: the Fréchet subdifferential of extended-valued functions, weak convexity and its subgradient characterization, Moreau envelopes of weakly convex functions and their differentiability, nonexpansiveness of convex proximal maps, and the bookkeeping of iterates driven by i.i.d. samples under a product measure.

Difficulty

The obvious argument — show that $\varphi(x_t)$ decreases in expectation — fails: neither $\varphi(x_t) - \min\varphi$ nor $\operatorname{dist}(0, \partial\varphi(x_t))$ need tend to zero, and the latter is discontinuous in $x$ . Progress must be measured on the Moreau envelope, which requires comparing the iterate $x_{t+1}$ with the proximal point $\hat x_t$ of $\varphi$ , not of $r$ . In Lean, the heaviest single ingredient is Lemma 2.2 (differentiability of the envelope of an extended-valued weakly convex function), and the direction $4 \Rightarrow 1$ of Lemma 2.1, which in the paper rests on Rockafellar–Wets' characterization of convexity by monotonicity of the subdifferential.

Formalization scope

Carrier. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). An extended-valued function is a pair (domain $D$ , real values on $D$ ); closedness is closedness of $\{(x,t) : x \in D,\ \psi(x) \le t\}$ . The subdifferential is the published regular subgradient NonconvexSplitting.Shared.IsRegularSubgrad of the $+\infty$ -extended lift.
Proximal map. prox a z is a function constrained, for every $a > 0$ , to return a minimizer over $D$ of $r(y) + \frac{1}{2a}\|y - z\|^2$ ; this determines it uniquely.
Randomness. The samples $\xi_0, \dots, \xi_T$ form a point of $\Omega^{T+1}$ under the product measure $P^{\otimes(T+1)}$ ; $\mathbb E$ is the Bochner integral, and every bounded expectation is accompanied by a conclusion that its integrand is integrable. The conditional expectation $\mathbb E_t$ in Lemma 3.3 is the integral over one sample with the iterate held fixed.
Output index. Because $t^*$ is independent of the samples, $\mathbb E\|\nabla\varphi_{1/\bar\rho}(x_{t^*})\|^2$ is the $\alpha$ -weighted average of $\mathbb E\|\nabla\varphi_{1/\bar\rho}(x_t)\|^2$ , as in the paper's (3.17).
$\min\varphi$ is an arbitrary real lower bound $\varphi^*$ of $\varphi$ on $D$ .
Corrected constant in (3.14). The paper prints the last term of (3.14) as $\alpha_t^2\bar\rho L^2$ ; its proof, and the unfolded sum leading to (3.15), give $2\alpha_t^2\bar\rho L^2$ , and that is what is stated. (3.15) and (3.16) are stated as printed.
Lemma 2.1 is stated for items 1–4; the clause for $C^2$ -smooth functions is not stated. Lemma 2.2 adds the implicit hypotheses that $\varphi$ is closed and proper, and includes existence and uniqueness of the proximal point.
Ruling out trivializations. The proximal map is tied to $r$ , $G$ is tied to $\partial f$ by (A2), $\min\varphi$ is not a real infimum, and integrability is concluded, so neither a junk value nor an unconstrained selection can make the statements hold vacuously; the hypotheses are satisfied by $r = f = 0$ , $G = 0$ .
Contributions welcome: proofs of the milestones, general lemmas on Moreau envelopes of weakly convex functions, and the nonexpansiveness of convex proximal maps on a closed convex domain.

Selected references

D. Davis and D. Drusvyatskiy, Stochastic Model-Based Minimization of Weakly Convex Functions, SIAM J. Optim. 29(1), 2019; arXiv:1803.06523v3, 2018. https://arxiv.org/abs/1803.06523
S. Ghadimi and G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM J. Optim. 23(4), 2013. https://doi.org/10.1137/120880811
R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22(3), 1951. https://doi.org/10.1214/aoms/1177729586

12 thms2 active usersReviewed

Linear Optimization Operations Research Probability+1·Captain: mikedeng1

Greed Works – Online Algorithms For Unrelated Machine Stochastic Scheduling 2: Greedy Assignment With Nominal Start Times Is (7.216 + 3.608Δ)h(Δ)-Competitive in the Online-Time ModelResearch Paper

Motivation

Scheduling jobs on parallel machines to minimize the total weighted completion time $\sum_j w_jC_j$ is a basic model of service and computing systems. Two features of practice are hard to combine with performance guarantees: jobs are not known in advance but arrive over time, and their processing times are random, with only their distributions known when they arrive. Machines are moreover often unrelated: a job's processing time distribution depends arbitrarily on the machine, and some jobs cannot run on some machines at all.

Gupta, Moseley, Uetz and Xie (arXiv:1703.01634, Math. Oper. Res. 2020) give the first performance guarantee for this combination: a simple greedy policy whose expected cost is within a factor depending only on the variability of the processing times of the best nonanticipatory policy, which knows all jobs in advance.

Timeline. For deterministic jobs arriving over time, Hall, Schulz, Shmoys and Wein (1997) gave an 8-competitive algorithm on unrelated machines. Megow, Uetz and Vredeveld (2006) introduced the stochastic online model and analysed greedy policies on identical machines with modified release dates. Skutella, Sviridenko and Uetz (2016) gave LP-based approximation algorithms for offline stochastic scheduling on unrelated machines, with guarantees linear in the squared coefficient of variation. The present paper (conference version IPCO 2017) treats the online, stochastic, unrelated case with release dates.

Setting

There is a finite set $M$ of machines and jobs $j=1,\dots,n$ . Job $j$ is released at an integer time $r_j\ge0$ , jobs are indexed so that $r_1\le\dots\le r_n$ , and job $j$ has weight $w_j\ge0$ . If job $j$ runs on machine $i$ its processing time is a random variable $P_{ij}$ with values in $\{0,1,2,\dots\}$ ; on forbidden pairs the page writes $\mathbb E[P_{ij}]=\infty$ , and every job has an allowed machine. On allowed pairs $\mathbb E[P_{ij}]\ge1$ and the variance is finite. Different jobs are independent; one job's times on different machines need not be. The squared coefficient of variation is $\mathbb{CV}[P_{ij}]^2=\operatorname{Var}[P_{ij}]/\mathbb E[P_{ij}]^2$ , and $\Delta$ bounds it on every allowed pair.

A policy decides, for each job, a machine and a start time; jobs are nonpreemptive and a machine runs one job at a time. It is nonanticipatory if its decisions up to time $t$ use only what is known at $t$ : the processing time of a job is learned when the job completes. $\mathsf{OPT}$ is the least expected cost $\mathbb E[\sum_jw_jC_j]$ of a nonanticipatory policy that knows all jobs, release dates and distributions in advance.

The greedy algorithm (§6.1) is first defined for deterministic times $p_{ij}$ . On machine $i$ job $j$ gets the modified release date $r_{ij}=\max\{r_j,c\,p_{ij}\}$ . On arrival, job $j$ is assigned to a machine $m(j)$ minimizing an explicit upper bound $\operatorname{cost}(j\to i)$ on the increase of the objective (Definition 4), and each machine runs WSPT (largest $w_k/p_{ik}$ first) among its jobs whose modified release dates have passed. Run on $p_{ij}=\mathbb E[P_{ij}]$ with $c=\frac23$ it yields the nominal schedule $(m,s)$ . The stochastic greedy policy (§6.3) keeps $m$ and the nominal order on each machine, and starts the $\ell$ th job on machine $i$ at $S_{i,\ell}=\max\{s_{i,\ell},S_{i,\ell-1}+P_{i,\ell-1}\}$ , never before its nominal start. Its expected cost is $\mathsf{ALG}$ , and

h(\Delta)=1+\tfrac{\sqrt\Delta}2\ (\Delta\le1),\qquad h(\Delta)=1+\tfrac{\Delta}{\Delta+1}\ (\Delta\ge1).

Formalization targets

Goal: Theorem 4

\mathsf{ALG}\;\le\;(7.216+3.608\,\Delta)\,h(\Delta)\,\mathsf{OPT}.

The goal is stated against every admissible nonanticipatory policy, for every tie-breaking of the greedy algorithm.

Milestones

Lemma 6: the deterministic greedy schedule has $\mathsf{ALG}\le\sum_j\operatorname{cost}(j\to m(j))$ .
Lemma 7, feasibility: with $\alpha_j=\operatorname{cost}(j\to m(j))$ , $\beta_{i,t}$ the weight of jobs on machine $i$ released by $t$ and unfinished at $t$ , and the speed-scaled values (12), $(\alpha^f/a,\beta^f/b)$ is feasible for the dual $(\mathrm D_r)$ when $af\ge2(2+c)$ , $1/c\le f(a-1)$ , $af\ge b$ .
(13): $z^{P_r}\le(1+\frac\Delta2)z^{S_r}\le(1+\frac\Delta2)\mathsf{OPT}$ for the time-indexed relaxations with release dates.
Lemma 10: $\mathbb E[(X-\mu)^+]\le\mu\sqrt\Delta/2$ for $\Delta\le1$ and $\le\mu\Delta/(\Delta+1)$ for $\Delta\ge1$ .
Lemma 8: $\mathbb E[S_j]\le h(\Delta)\,s_j$ for every job.

Significance

The result. Theorem 4 is the first constant-factor guarantee, for fixed $\Delta$ , for stochastic online scheduling on unrelated machines with release dates, and it is achieved by a combinatorial policy that needs no LP solution. For deterministic jobs ( $\Delta=0$ , $h=1$ ) it gives a deterministic 7.216-competitive algorithm (Theorem 3), improving the ratio 8 of Hall et al.; for exponential processing times ( $\Delta=1$ ) the factor is $(7.216+3.608)\cdot\frac32$ . The order $O(\Delta)$ matches earlier offline results on unrelated machines and online results on identical machines.

Formalizing it. The result is proved on paper and has no machine-checked proof. A formalization needs nonanticipatory policies with machine choice, a time-indexed LP relaxation with countably many variables and its weak duality, and a dual-fitting argument. It also exposes a gap: the second sentence of Lemma 7, the bound $z^{D_r}(\alpha^f/a,\beta^f/b)\ge\mathsf{ALG}/(7+\frac{11}{51})$ , fails as printed. On one machine with jobs $r=(0,0,0,5)$ , $p=(\frac54,\frac54,1,3)$ , $w=(2,1,\frac1{1000},\frac1{100})$ the greedy schedule has $\mathsf{ALG}=\frac{6049}{600}$ while $z^{D_r}=\frac{8879}{6400}<\mathsf{ALG}/(7+\frac{11}{51})=\frac{4471}{3200}$ . The step $\sum_{i,s}\beta^f_{is}=\mathsf{ALG}/f$ counts a job at $\lfloor C_k/f\rfloor-\lceil r_k/f\rceil+1$ integer slots, up to one more than $C_k/f$ . A complete proof of the goal has to close this gap.

Difficulty

Three parts are hard. First, the comparison is with an optimal adaptive policy, so the lower bound has to come from a relaxation that every nonanticipatory policy satisfies in expectation. Writing the time-indexed LP for policies that choose machines at start time, idle deliberately and start at real times, and showing it is a relaxation, requires nonanticipation and job independence to decouple a job's machine from its own processing time. Second, the dual fitting runs through a speed-scaled instance with a non-integer speed $f=\frac{23}6$ , so the dual's integer slots and the schedule's real times do not align; this is where the printed objective bound breaks. Third, the obvious stochastic policy, WSEPT list scheduling without forced idleness, fails: Remark 2 of the paper gives an instance where it has $\mathbb E[C]=\Omega(n)$ against $O(1)$ . The analysis therefore has to work with deliberately delayed starts.

Formalization scope

Machines are a Fintype, Nonempty type; jobs are Fin n in release order. Processing times are ℕ-valued measurable functions on a probability space, with finite second moment and mean at least one on eligible pairs, and with jobs independent (iIndepFun over jobs of the machine-indexed vectors). Forbidden pairs are an eligibility relation, never a zero or junk mean. Release dates are natural numbers: the relaxation of §6.2 has integer slots $s\ge r_j$ , and (13) is false for a fractional release date. Weights are nonnegative; $\Delta$ is any upper bound on the squared coefficients of variation, which is at least as strong as the page's maximum.

$\mathsf{OPT}$ is never written as an infimum. The goal and (13) quantify over every admissible policy: a map from realizations to machines and real start times that is feasible (eligible machine, start at or after release, disjoint half-open processing intervals per machine), nonanticipatory, and has integrable completion times. A non-integrable comparator would have Bochner integral $0$ and would make the bound trivial or false; the integrability requirement rules this out. The greedy algorithm is a predicate on an outcome (assignment and start times): cost-minimal assignment, no start before the modified release date, no unnecessary idleness, and the WSPT priority. Every tie-breaking is covered, and the goal fixes $c=\frac23$ . The stochastic policy is the recursion $S_{i,\ell}=\max\{s_{i,\ell},S_{i,\ell-1}+P_{i,\ell-1}\}$ itself. LP feasibility includes summability of every series, and LP optima appear only through "for every feasible point there is a feasible point" statements.

A complete development needs: weak duality for $(\mathrm P_r)$ / $(\mathrm D_r)$ with countably many variables; the identity $\mathbb E[C_j]=C^S_j$ for the expected occupation variables of a nonanticipatory policy (reusable for any time-indexed stochastic scheduling relaxation); Lemma 10, a self-contained probability inequality; and the dual fitting. Contributions are welcome on each milestone and on a repaired objective bound for Lemma 7.

Selected references

V. Gupta, B. Moseley, M. Uetz, Q. Xie, Greed Works – Online Algorithms For Unrelated Machine Stochastic Scheduling, Mathematics of Operations Research, 2020; arXiv:1703.01634v4. https://arxiv.org/abs/1703.01634, https://doi.org/10.1287/moor.2019.0999
L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Mathematics of Operations Research 22:513–544, 1997. https://doi.org/10.1287/moor.22.3.513
N. Megow, M. Uetz, T. Vredeveld, Models and algorithms for stochastic online scheduling, Mathematics of Operations Research 31(3):513–525, 2006. https://doi.org/10.1287/moor.1060.0201
M. Skutella, M. Sviridenko, M. Uetz, Unrelated machine scheduling with stochastic processing times, Mathematics of Operations Research 41(3):851–864, 2016. https://doi.org/10.1287/moor.2015.0757

11 thms2 active usersReviewed

Functional Analysis Markov Chain Probability+1·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Uniform Wasserstein contraction

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

10 thms2 active usersReviewed

Linear Optimization Operations Research Probability+1·Captain: mikedeng1

Greed Works – Online Algorithms For Unrelated Machine Stochastic Scheduling 1: Greedy Assignment With WSEPT Sequencing Is (4 + 2Δ)-Competitive in the Online-List ModelResearch Paper

Motivation

Online scheduling asks for decisions before the full job set is known. In the online-list model, jobs are revealed one at a time and each must be assigned to a machine before the next job is revealed; the scheduler may choose the processing order after the list is complete. When processing durations are random and machines are unrelated, the same job may have different duration distributions on different machines. An assignment decision therefore affects both its own completion time and the waiting time of other jobs. Gupta, Moseley, Uetz and Xie study a greedy assignment rule for this setting and prove a bound against a scheduler that knows all distributions and all jobs in advance but cannot see future processing-time realizations (arXiv:1703.01634v4, §§2–5). This comparison is relevant to systems that must commit work to heterogeneous servers as requests arrive, while service times remain uncertain.

Setting

Let $M$ be a nonempty finite set of machines and $J=\{0,\ldots,n-1\}$ a finite set of jobs indexed by their presentation order. Job $j$ has a nonnegative weight $w_j$ . An eligibility relation $E\subseteq M\times J$ records which machines can process each job; every job has at least one eligible machine. For an eligible pair $(i,j)$ , $P_{ij}$ is a nonnegative integer-valued random processing time with mean $\mu_{ij}=\mathbb E[P_{ij}]\ge1$ and a finite second moment. The vector $(P_{ij})_{i\in M}$ for one job may have dependence across machines, but the vectors for different jobs are independent. A parameter $\Delta\ge0$ bounds $\operatorname{Var}(P_{ij})/\mu_{ij}^{2}$ for all eligible pairs. These conventions follow the standing model and coefficient-of-variation bound in the paper (§2, pp. 4–6 and Definition 3, p. 7).

The greedy assignment sends each newly presented job to an eligible machine that minimizes the instantaneous increase in expected total weighted completion time. For a fixed machine, jobs are sequenced by decreasing ratio $w_j/\mu_{ij}$ , with job index breaking equal-ratio ties. This is the weighted shortest expected processing time, or WSEPT, order. The algorithm runs each machine continuously from time zero in that order. Its expected objective, $\mathrm{ALG}$ , is the expectation of $\sum_j w_j C_j$ for the resulting realized completion times, not a value assigned by a closed formula (§4, pp. 8–9).

A comparator policy can choose machines and start times as earlier jobs finish. It must schedule nonpreemptively, use only information available when a decision is made, and have integrable completion times. It may know the full job set and every processing-time distribution before time zero, but not the future realizations. Write $C_j^\Pi$ for its realized completion time and $\mathrm{OPT}$ for the least expected weighted completion cost among such policies when an optimum exists (§2.1, pp. 5–6).

Formalization targets

The goal is the paper's Theorem 1 (p. 11). It compares every eligible-minimum greedy assignment, including every tie choice, with every admissible nonanticipatory comparator $\Pi$ :

\mathrm{ALG}\le(4+2\Delta)\,\mathbb E\!\left[\sum_{j\in J}w_j C_j^\Pi\right].

This universal comparison expresses $\mathrm{ALG}\le(4+2\Delta)\mathrm{OPT}$ without requiring an optimizer to exist. The milestone list contains the paper's integer tail identities (Lemma 1), the completion-time expression for one job (Lemma 9), the comparison of two time-indexed relaxations and its policy consequence (Lemma 2 and Corollary 1), and the three dual-variable claims used around the greedy algorithm (Lemmas 3–5). Their printed indices and formulas are attached to the proposal in proof order.

Significance

The result supplies a performance guarantee for a combinatorial online algorithm on heterogeneous machines with random durations. The factor varies explicitly with the processing-time variability: for deterministic eligible processing times, $\Delta=0$ and the bound is $4$ ; greater permitted variability increases it linearly. Forbidden machine-job pairs are included, so the claim applies when some jobs have a restricted set of possible servers. The comparator may postpone machine selection until processing begins and adapt to completed work, so the bound is not limited to fixed-assignment schedules (Theorem 1 and §2.1).

The theorem is proved in the cited paper. In this proposal, the Lean statements and definitions have compiled, while the theorem modules still contain sorry; the remaining formalization work is to supply machine-checked proofs. A completed development would contribute reusable definitions for nonanticipatory unrelated-machine policies, time-indexed stochastic scheduling relaxations, and comparisons with countably many LP variables. Those interfaces can support later scheduling results that use the same information structure.

Difficulty

The most immediate comparison treats the greedy assignment costs as dual variables. For this paper's linear program, the direct halved dual point is feasible, but the resulting dual objective is zero, so feasibility alone gives no useful upper bound on $\mathrm{ALG}$ (Lemmas 3–4 and the beginning of §5). The random processing times also require care when translating occupancy probabilities into completion costs: the time-indexed expression uses both first and second moments, and a policy's start decision must not depend on the job's unobserved duration. The proof must reconcile the greedy order, those probability identities, and a comparison with policies that may change machines and start times adaptively.

Formalization scope

The Lean model uses Fin n in arrival order and permits $n=0$ ; the empty instance gives a trivial inequality. The machine type is finite and nonempty. Processing times are natural-valued random variables, while policy start times are real. Processing intervals are half-open, so a zero-duration job occupies no machine time. An ineligible pair is represented by the eligibility relation, never by a zero mean. Each eligible processing time has finite second moment and mean at least one; $\Delta$ is any nonnegative upper bound on squared coefficients of variation. The paper leaves $w_j\ge0$ implicit; it is included because negative weights invalidate the comparison. Dependence across machines for the same job is allowed, and the entire time vector is independent across jobs.

Nonanticipation is stated by comparing two realizations that agree on the durations observed by time $t$ and on the fact that running jobs have not yet completed. Admissible comparator policies must work for every realization and have integrable completion times, preventing a default zero value for a nonintegrable integral. The goal quantifies over all such policies, so it cannot be made true by choosing a restricted benchmark. The greedy predicate reads only earlier assignments and admits every eligible minimizing machine; it does not fix a favorable tie choice.

The LP variables $y_{ijs}$ are real and nonnegative, supported on eligible pairs, and their countable sums and time-weighted sums must converge. LP comparisons use feasible witnesses instead of a real infimum, whose value would be misleading for an empty feasible set. A source-level discretization issue is isolated in Lemma 4: $\sum_s\beta_{is}$ counts whole slots up to a nominal completion time, so the printed second equality requires integer means. Its first equality and the goal do not take that condition. A complete proof needs measurable-policy reasoning, tail-sum identities, summability arguments, WSEPT order properties and dual weak duality. Definitions and lemmas that isolate those components are welcome.

Selected references

V. Gupta, B. Moseley, M. Uetz and Q. Xie, Greed Works – Online Algorithms For Unrelated Machine Stochastic Scheduling, accepted version of Mathematics of Operations Research, 2020. arXiv:1703.01634v4; DOI:10.1287/moor.2019.0999.

11 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

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

Motivation

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3 (p. 11)

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

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

Companion: the "in particular" clause

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

Milestones (p. 12)

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

Significance

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

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

Difficulty

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

Formalization scope

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

Committed conventions:

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

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

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

Selected references

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

8 thms2 active usersReviewed

Dynamical Systems Markov Chain Probability+1·Captain: mikedeng1

Coexistence and Extinction for Stochastic Kolmogorov Systems 1: If Every Boundary Ergodic Measure Repels, X Converges Exponentially Fast in Total Variation to a Unique Interior Stationary LawResearch Paper

Motivation

Whether interacting species can coexist in a fluctuating environment is one of the basic questions of mathematical ecology. Deterministic models (Lotka–Volterra competition, predator–prey systems, food chains) answer it through invasion criteria: a population persists if, whenever it is rare, it grows. In a random environment the analogous criterion is phrased through Lyapunov exponents (long-run per-capita growth rates) computed against stationary distributions of the subcommunities in which some species are absent. Schreiber, Benaïm and Atchadé ([SBA11], J. Math. Biol. 62 (2011), MR 2786721) proved such a criterion for stochastic differential equations on a compact state space; A. Hening and D. H. Nguyen (arXiv:1704.06984, Ann. Appl. Probab. 2018) extended it to the non-compact orthant $\mathbb R^n_+$ , which is where population sizes actually live, and added an exponential rate of convergence.

Timeline. [SBA11] (2011) gave the compact-state SDE criterion via a minimax principle; Hening and Nguyen (2017/2018) removed compactness, proved convergence in total variation at a geometric rate, and in the same paper gave matching extinction results (the second and third missions of this series).

Setting

Let $n\ge1$ be the number of populations and $X(t)=(X_1(t),\dots,X_n(t))\in\mathbb R^n_+=[0,\infty)^n$ their sizes. The stochastic Kolmogorov system is

dX_i(t)=X_i(t)f_i(X(t))\,dt+X_i(t)g_i(X(t))\,dE_i(t),\qquad i=1,\dots,n,

where $f_i$ are per-capita growth rates, $g_i$ noise intensities, and $E(t)=\Gamma^\top B(t)$ with $B$ an $n$ -dimensional standard Brownian motion and $\Sigma=\Gamma^\top\Gamma=(\sigma_{ij})$ . Write $\mathbb R^{n,\circ}_+=(0,\infty)^n$ for the states with all species present, $\partial\mathbb R^n_+$ for its complement (some species absent) and $\|x\|=\sum_i|x_i|$ .

Assumption 1.1 (standing) requires: the matrix $(g_i(x)g_j(x)\sigma_{ij})$ is positive definite on $\mathbb R^n_+$ ; $f_i,g_i$ are locally Lipschitz; and for some $c\in\mathbb R^{n,\circ}_+$ , $\gamma_b>0$ ,

\limsup_{\|x\|\to\infty}\Big[\frac{\sum_ic_ix_if_i(x)}{1+c^\top x}-\frac12\frac{\sum_{i,j}\sigma_{ij}c_ic_jx_ix_jg_i(x)g_j(x)}{(1+c^\top x)^2}+\gamma_b\Big(1+\sum_i(|f_i(x)|+g_i^2(x))\Big)\Big]<0,

a dissipativity condition satisfied by logistic and competitive Lotka–Volterra models.

$P_X(t,x,\cdot)$ is the law of $X(t)$ started at $x$ . A probability measure $\mu$ is invariant if $\int P_X(t,x,\cdot)\,\mu(dx)=\mu$ for all $t$ ; ergodic invariant measures are the extreme points of that convex set. $\mathcal M$ is the set of ergodic invariant probability measures supported on $\partial\mathbb R^n_+$ (it contains the Dirac mass $\delta^*$ at $0$ ), and $\mathrm{Conv}(\mathcal M)$ its finite convex combinations. The Lyapunov exponent of species $i$ at $\mu$ is

\lambda_i(\mu)=\int\Big(f_i(x)-\frac{\sigma_{ii}g_i^2(x)}{2}\Big)\mu(dx).

Assumption 1.2: $\max_i\lambda_i(\mu)>0$ for every $\mu\in\mathrm{Conv}(\mathcal M)$ — every boundary state is invadable by some missing species.

Formalization targets

Goal: Theorem 1.1 (p. 6)

Under Assumptions 1.1 and 1.2 there is an invariant probability measure $\pi^*$ with $\pi^*(\mathbb R^{n,\circ}_+)=1$ , it is the only invariant probability measure concentrated on $\mathbb R^{n,\circ}_+$ , and for some $r\in(0,1)$ and every $x\in\mathbb R^{n,\circ}_+$ there is $C_x$ with

\|P_X(t,x,\cdot)-\pi^*\|_{TV}\le C_x\,r^t,\qquad t\ge0.

This is strong stochastic persistence (Definition 1.1) with an exponential rate; it leaves the rate $r$ and the constants unspecified, as the paper does.

Milestones

The milestones follow the proof: well-posedness, invariant faces and the moment bound (3.6) (Lemma 3.1); uniform moment bounds and the Feller property (Lemma 3.2); integrability under invariant measures (Lemma 3.3); $\delta^*\in\mathcal M$ ; convergence of occupation-measure integrals (Lemma 3.4); the log-Laplace bound (Lemma 3.5); irreducibility, aperiodicity and petite compacts for the skeleton chain (Lemma 3.6); the weighted invasion rate (4.1); boundary repulsion on average (Lemma 4.1); the Lyapunov contraction near the boundary (Proposition 4.1); the geometric drift (4.18); geometric ergodicity of the skeleton chain (4.26).

Significance

The result. Theorem 1.1 turns coexistence into a checkable condition on boundary subcommunities: one computes invasion rates of missing species against the stationary laws of the smaller systems. It is the persistence half of a dichotomy whose extinction half (Theorems 1.2–1.3) uses the same exponents, and it underlies the classification of stochastic food chains in the paper's own §2 (Theorem 2.1). The exponential rate gives quantitative mixing and supports further limit theorems for time averages.

Formalizing it. The theorem is proved in the paper but no machine-checked proof is recorded in this mission. A formalization exercises a chain of tools largely absent from current libraries: strong solutions of SDEs with locally Lipschitz coefficients on a closed orthant, the Feller property, tightness and weak limits of occupation measures, invariant and ergodic measures of diffusions, Meyn–Tweedie theory for skeleton chains, and log-Laplace (cumulant) estimates. Each milestone is a self-contained target; several (Lemma 3.5, the Meyn–Tweedie step) are independent of the population model.

Difficulty

The naive argument — positive invasion rates at each boundary ergodic measure imply that the process is pushed away from the boundary — fails twice. First, the state space is non-compact, so occupation measures need not be tight and the growth-rate functionals are unbounded; Assumption 1.1(3) and the moment bounds of Lemmas 3.2–3.4 are what replace compactness. Second, invasion rates are averages along the boundary dynamics, not pointwise drifts: the Lyapunov function $V(x)=(1+c^\top x)/\prod_ix_i^{p_i}$ decreases only on average over a time window of length $T^*$ , and turning this into a uniform contraction of $V^\theta$ requires controlling the full log-Laplace transform of the increment $\ln V(X(T))-\ln V(x)$ (Proposition 4.1), not just its mean. Uniformity of all constants in the starting point is the delicate part.

Formalization scope

The process is a family X x of strong solutions, one from each $x\in\mathbb R^n_+$ , on one probability space driven by one Brownian motion, using the published Ethier–Kurtz definitions SolvesBrownianSDE and IsStandardBrownian on $\mathbb R^n=$ SDEState n. Coordinates are Fin n; $n\ge1$ . The coefficients are functions on $\mathbb R^n$ read at the positive part $x^+$ , which agrees with the model on $\mathbb R^n_+$ . The norm is $\ell^1$ . Invariance is stated through the transition probabilities $P_X(t,x,\cdot)=$ law of $X^x(t)$ ; ergodic means extremal invariant. The $\limsup<0$ of (1.2) is written as " $\le-\varepsilon$ for $\|x\|\ge R$ ". Total variation is the published MarkovChainCLT.tvDist, $\sup_A|\mu(A)-\nu(A)|$ ; the paper does not fix the factor $2$ , and geometric convergence is insensitive to it. The constants $M>0,\delta_0$ of §3 are data satisfying (3.1), (3.2); $H$ is the supremum (3.5).

Deviations, all disclosed in the items: aperiodicity is the Meyn–Tweedie notion (no cycle of $d\ge2$ nonempty disjoint sets), because the literal definition on p. 15 makes every chain aperiodic; (4.1), cited from [SBA11, Lemma 4], retains the attained minimum $2\rho^*$ and is stated only in the direction used. Lemma 3.5 allows $K_2$ to depend on the fixed $\theta_0$ as its proof requires, despite the page saying “only on $K_1$ ”. Expectations of nonnegative quantities are lower Lebesgue integrals; wherever a Bochner integral appears, its integrability is part of the conclusion.

Trivializing readings are excluded: uniqueness is among invariant measures on $\mathbb R^{n,\circ}_+$ only (boundary invariant measures always exist), $\mathcal M$ is nonempty ( $\delta^*\in\mathcal M$ is a milestone, so Assumption 1.2 is never vacuous), and every existential constant is quantified before the points it must be uniform in. The logistic model on p. 4 gives a nonvacuous instance of Assumption 1.1.

Contributions welcome: general SDE well-posedness on invariant closed sets, Feller and tightness results for diffusions, Meyn–Tweedie geometric ergodicity for kernels, and cumulant-generating-function bounds, all reusable beyond this mission.

Selected references

A. Hening, D. H. Nguyen, Coexistence and extinction for stochastic Kolmogorov systems, Ann. Appl. Probab. 28(3), 2018. arXiv:1704.06984v1. https://arxiv.org/abs/1704.06984
S. J. Schreiber, M. Benaïm, K. A. S. Atchadé, Persistence in fluctuating environments, J. Math. Biol. 62(5), 655–683, 2011. MR 2786721, https://mathscinet.ams.org/mathscinet-getitem?mr=2786721
S. P. Meyn, R. L. Tweedie, Stability of Markovian processes I: criteria for discrete-time chains, Adv. Appl. Probab. 24(3), 542–574, 1992. MR 1174380, https://mathscinet.ams.org/mathscinet-getitem?mr=1174380
R. Khasminskii, Stochastic Stability of Differential Equations, 2nd ed., Springer, 2012. MR 2894052, https://mathscinet.ams.org/mathscinet-getitem?mr=2894052

20 thms2 active usersReviewed

Dynamical Systems Harmonic Analysis Machine Learning+1·Captain: mikedeng1

Approximation Bounds for Random Neural Networks and Reservoir Systems II: Echo State Networks with Random Weights Approximate Regular Functionals with an Explicit L² Error Bound (Theorem 2)Research Paper

Motivation

Reservoir computing learns an input/output system from data in two stages. A dynamical system, the reservoir, is driven by the input sequence and its state is recorded; then only a linear readout of that state is trained, by least squares. The echo state network (ESN) is the most widely used reservoir: its state evolves by $x_t = \sigma(Ax_{t-1} + Cz_t + \zeta)$ , with the matrices $A, C$ and the vector $\zeta$ drawn at random and never trained. ESNs predict chaotic systems well in practice (Jaeger & Haas, Science 2004), and they are known to be universal: for every fading-memory input/output map some ESN approximates it (Grigoryeva & Ortega, Neural Netw. 2018). Universality does not explain the practice, where the reservoir weights are random and fixed in advance. Gonon, Grigoryeva & Ortega (Ann. Appl. Probab. 2023) prove that an ESN whose weights are drawn from an explicit distribution that does not depend on the target approximates every sufficiently regular target, with an explicit $L^2$ error bound. This mission formalizes that result, Theorem 2, and the chain of results its proof rests on.

Setting

Time runs over $\mathbb Z_- = \{0, -1, -2, \dots\}$ . Inputs take values in a set $D_d$ with $0 \in D_d \subset B_M \subset \mathbb R^d$ , where $B_M$ is the closed Euclidean ball of radius $M > 0$ . The input $Z = (Z_t)_{t \in \mathbb Z_-}$ is a $D_d$ -valued process with law $\mu_Z$ . The target is a functional $H^* : (D_d)^{\mathbb Z_-} \to \mathbb R$ , the present output as a function of the whole input history. All norms are Euclidean.

Regularity. Fix weights $w_{-i} > 0$ with $\sum_i i\, w_{-i} < \infty$ . $H^*$ is $w$ -Lipschitz with constant $L > 0$ if $|H^*(u) - H^*(v)| \le L\sum_{i \ge 0} w_{-i}\|u_{-i} - v_{-i}\|$ . Assumption 1 asks, in addition, for every $T \ge 1$ : with $q = d(T+1)$ , the truncation $H^*_T(z_0, \dots, z_{-T}) = H^*(\dots, 0, z_{-T}, \dots, z_0)$ has a Fourier representation $H^*_T(u) = \int_{\mathbb R^q} e^{i\langle w, u\rangle} g_T(w)\,dw$ on $(D_d)^{T+1}$ , with $g_T \in L^1$ and $\int \max(1, \|w\|^3)|g_T(w)|^2\,dw < \infty$ .

The random ESN. Fix $T, N \ge 1$ , $R > 0$ , and a bound $M_T$ with $\|(Z_0, \dots, Z_{-T})\| \le M_T$ almost surely. Draw $A_1, \dots, A_N$ i.i.d. uniform on $B_R \subset \mathbb R^q$ and, independently, $\zeta_1, \dots, \zeta_N$ i.i.d. uniform on $[-\max(M_TR,1), \max(M_TR,1)]$ . With $S$ the block shift on $\mathbb R^q$ and $c$ the embedding of $\mathbb R^d$ into the first block, and $a$ the matrix with rows $A_i^\top$ , put

\bar A = \begin{pmatrix} S & 0\\ aS & 0\end{pmatrix},\quad \bar C = \begin{pmatrix} c\\ ac\end{pmatrix},\quad \bar\zeta = \begin{pmatrix} 0\\ \zeta\end{pmatrix},\quad A = \begin{pmatrix}\bar A & -\bar A\\ -\bar A & \bar A\end{pmatrix},\quad C = \begin{pmatrix}\bar C\\ -\bar C\end{pmatrix},\quad \zeta = \begin{pmatrix}\bar\zeta\\ -\bar\zeta\end{pmatrix}.

The ESN is $X_t = \sigma(AX_{t-1} + CZ_t + \zeta)$ , $Y_t = WX_t$ , with $\sigma(x) = \max(x, 0)$ and state space $\mathbb R^{2(N+d(T+1))}$ .

Formalization targets

Goal: Theorem 2 (p. 54)

For every $H^*$ satisfying Assumption 1 there is a readout $W$ , a function of the random weights alone, such that the ESN has the echo state property (a unique state sequence for every input) and

\mathbb E\big[|Y_0 - H^*(Z)|^2\big]^{1/2} \le \frac{\sqrt{C_{T,R}}}{\sqrt N} + \int_{\mathbb R^q \setminus B_R}|g_T(u)|\,du + LM\sum_{i > T} w_{-i},

with $C_{T,R} = 16\max(M_TR,1)\mathrm{Vol}_q(B_R)(M_T+1)^2(M_T^3+M_T+16)\int_{B_R}\max(1,\|u\|^3)|g_T(u)|^2\,du$ .

Milestones

(8), p. 33: a scalar identity expressing $e^{iz} - iz - 1$ as an integral of ReLU ramps.
Proposition 2, pp. 31–32: under a Fourier condition, $f$ is an integral of ReLU ridge functions with a compactly supported, square-integrable weight $\pi$ .
Proposition 3, pp. 41–42: a static ReLU network with uniformly sampled inner weights achieves mean-square error $C^*/N$ .
Corollary 1, p. 43: the same with a dimension-free integrability condition and a truncation term.
Remark 10, p. 53: the shift reservoir is nilpotent, has $K = I$ and stores the last $T+1$ inputs.
Proposition 6, p. 51: a linear reservoir with a random ReLU readout satisfies the bound (54).
(64)–(66), pp. 55–56: every solution of the ESN reduces to the linear shift reservoir, which gives uniqueness.

Significance

Theorem 2 is the first approximation bound for echo state networks whose recurrent and input weights are sampled from a generic distribution rather than constructed from the target. The bound separates three error sources: a Monte Carlo term decaying like $N^{-1/2}$ , a truncation term in the sampling radius $R$ , and a memory term in the window length $T$ . Because the readout can be taken to be the least-squares readout, the bound also controls the trained networks used in practice, and it is the input to the paper's rate and universality corollaries (Corollaries 4 and 5).

Status: the result is proved on paper. No part of it is formalized; the only reservoir-computing material on the platform is the published definition ReservoirESN (the state equation), which this mission reuses. A formal proof would supply the first machine-checked random-feature approximation bound with explicit constants.

Difficulty

The obvious argument fails in two places. First, the classical integral representations of Barron type place the inner weights on unbounded sets, which cannot be sampled uniformly; Proposition 2 needs a change of variables that makes the weight compactly supported while keeping it square integrable, and this costs the factor $R^{-(2q+2)}$ and the condition (5). Second, a ReLU network is not contractive, so the echo state property of the ESN cannot be taken from the standard contraction criterion; it has to be derived from the block structure of $A$ , which makes the difference of the two state halves follow a nilpotent linear recursion.

Formalization scope

$\mathbb R^q$ is EuclideanSpace ℝ (Fin (T+1) × Fin d), block $k$ holding $z_{-k}$ ; input sequences are ℕ → EuclideanSpace ℝ (Fin d) with index $k = -t$ , and $x_t = F(x_{t-1}, z_t)$ is the published ReservoirESN.IsSolution. Points of $\mathbb R^{q+1}$ are pairs with norm $(\|w\|^2 + u^2)^{1/2}$ . The uniform laws are Lebesgue measure conditioned on the ball or interval; $N$ i.i.d. rows have the product law. The input is independent of the weights (§4.1) and $D_d$ -valued with $0 \in D_d \subset B_M$ (§5.1): expectations are iterated lower Lebesgue integrals over $\mu_Z$ and the product law, and probability- $(1-\delta)$ statements bound the product measure of the bad set. The scalar output case $m = 1$ is used, as in the paper. Assumption 1 is required for every $T \ge 1$ , as printed.

A readout allowed to depend on the input would make every bound trivial; in every statement the readout is a measurable function of the inner weights alone.

Departures from the print, each disclosed in the item: the last term of Proposition 6 is the $L^2(\mu_Z)$ norm of $\|K^{-1}S^{T+1}X_{-T-1}\|$ , which the page prints outside the expectation; the state space of the linear reservoir (52) is a parameter $D_N$ , as in §2.1, and its solution is assumed to be a random process; Proposition 3 omits " $C^* > 0$ " (the explicit value (33) is used); measurability of the Fourier density $g$ is stated where the page leaves it implicit.

A complete development needs Fourier integrals on Euclidean spaces, change of variables under linear maps, product measures and Fubini–Tonelli, and an importance-sampling variance bound. The static results (Propositions 2, 3, Corollary 1) are reusable for random-feature models beyond reservoir computing. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

L. Gonon, L. Grigoryeva, J.-P. Ortega, Approximation bounds for random neural networks and reservoir systems, Ann. Appl. Probab. 33(1), 28–69, 2023. https://doi.org/10.1214/22-AAP1806
L. Grigoryeva, J.-P. Ortega, Echo state networks are universal, Neural Netw. 108, 495–508, 2018. https://doi.org/10.1016/j.neunet.2018.08.025
H. Jaeger, H. Haas, Harnessing nonlinearity: predicting chaotic systems and saving energy in wireless communication, Science 304, 78–80, 2004. https://doi.org/10.1126/science.1091277
A. R. Barron, Universal approximation bounds for superpositions of a sigmoidal function, IEEE Trans. Inf. Theory 39, 930–945, 1993. https://doi.org/10.1109/18.256500
J. M. Klusowski, A. R. Barron, Approximation by combinations of ReLU and squared ReLU ridge functions with ℓ1 and ℓ0 controls, IEEE Trans. Inf. Theory 64, 7649–7656, 2018. https://doi.org/10.1109/tit.2018.2874447
C. Cuchiero, L. Gonon, L. Grigoryeva, J.-P. Ortega, J. Teichmann, Discrete-time signatures and randomness in reservoir computing, IEEE Trans. Neural Netw. Learn. Syst., 2021. https://doi.org/10.1109/TNNLS.2021.3076777

11 thms2 active usersReviewed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

A Two-Timescale Stochastic Algorithm Framework for Bilevel Optimization: Complexity Analysis and Application to Actor-Critic: Explicit Error Bounds for TTSA with a Strongly Convex Outer ObjectiveResearch Paper

Motivation

Bilevel optimization asks for an outer decision while an inner optimization problem responds to that decision. In hyperparameter selection, for example, the outer objective evaluates a model whose parameters are chosen by a training problem. A two-timescale algorithm updates both levels in one stochastic loop, so its outer step uses an inner solution that has not yet settled. The resulting error bound must account for both the outer decision and the inner tracking error. Hong, Wai, Wang and Yang study this setting and give finite-time bounds for their two-timescale stochastic approximation (TTSA) algorithm in the strongly convex outer case Hong et al., arXiv:2007.05170v4, §§1–3.

The paper states its main rates using $\lesssim$ , with numerical constants omitted. Appendix A gives explicit bounds for the two errors. This mission targets those displayed bounds, retaining their constants and the actual stochastic update. The selected source is the arXiv v4 preprint: page numbers and theorem labels below refer to that version Hong et al., Theorem 1 and App. A.

Setting

Let $X\subseteq\mathbb R^{d_1}$ be closed and convex. For an outer point $x\in X$ , the inner solution $y^\star(x)\in\mathbb R^{d_2}$ minimizes $g(x,\cdot)$ . The outer objective is $\ell(x)=f(x,y^\star(x))$ , and $x^\star\in X$ is an optimal outer point. The inner objective is strongly convex in $y$ , which gives a unique inner minimizer. The paper’s derivative and Lipschitz assumptions control how that minimizer and the outer gradient change as $x$ and $y$ move Hong et al., Assumptions 1–2, pp. 5–6.

The algorithm keeps iterates $x^k\in X$ and $y^k\in\mathbb R^{d_2}$ . With deterministic step sizes $\alpha_k,\beta_k$ and stochastic estimates $h_f^k,h_g^k$ , it updates

y^{k+1}=y^k-\beta_k h_g^k,\qquad x^{k+1}=P_X(x^k-\alpha_k h_f^k),

where $P_X$ is the Euclidean nearest-point projection onto $X$ . The inner estimate targets $\nabla_y g(x^k,y^k)$ . The outer estimate targets the surrogate gradient

\bar\nabla_xf(x,y)=\nabla_xf(x,y)-\nabla^2_{xy}g(x,y) [\nabla^2_{yy}g(x,y)]^{-1}\nabla_yf(x,y),

with a bias bounded by $b_k$ . Assumption 3 bounds the conditional variances given the histories $\mathcal F_k$ and $\mathcal F'_k$ . The surrogate at $y^\star(x)$ is the paper’s $\nabla\ell(x)$ Hong et al., Algorithm 1, (5)–(7c), p. 6.

The two quantities being bounded are the outer error $\Delta_x^k=\mathbb E\|x^k-x^\star\|^2$ and inner tracking error $\Delta_y^k=\mathbb E\|y^k-y^\star(x^{k-1})\|^2$ . At $k=0$ , the convention is $x^{-1}=x^0$ . The constants $L$ and $L_y$ are the exact functions of the derivative bounds in (13); $\widetilde\sigma_f^2=\sigma_f^2+3\sup_{x\in X}\|\nabla\ell(x)\|^2$ is finite by the paper’s standing assumption after (14). The products $G^{(1)}_{m:n}$ and $G^{(2)}_{m:n}$ are those of (48) Hong et al., pp. 8–9, 20.

Formalization targets

The first target is the explicit inner bound (55): for every $k\ge0$ ,

\Delta_y^{k+1}\le G^{(1)}_{0:k}\Delta_y^0+C_y^{(1)}\beta_k, \qquad C_y^{(1)}=\frac8{\mu_g}\left\{\sigma_g^2+ \frac{4c_0^2L_y^2}{\mu_g}(\widetilde\sigma_f^2+3b_0^2)\right\}.

The goal also includes the explicit outer bound displayed after (59):

\begin{aligned} \Delta_x^{k+1}\le{}&G^{(2)}_{0:k} \left\{\Delta_x^0+\left[\frac{2L^2}{\mu_\ell^2} +\frac{3\alpha_0L^2}{\mu_\ell}\right]\Delta_y^0\right\}\\ &+\frac2{\mu_\ell}\left[\frac{2\widetilde c_b}{\mu_\ell} +\widetilde\sigma_f^2+3b_0^2\right]\alpha_k\\ &+\frac{2c_1}{\mu_\ell}\left[\frac{2L^2}{\mu_\ell}+3\alpha_0L^2\right] C_y^{(1)}\alpha_k^{2/3}. \end{aligned}

These formulas use the paper’s step-size conditions (20a)–(20b), the bias condition $b_k^2\le\widetilde c_b\alpha_{k+1}$ , and a positive outer modulus $\mu_\ell$ . The milestones are the source’s Lemma 2 (12a), (14), (50), Lemma 10, (55), Lemma 11 and Lemma 4 (29). They supply independently stated targets for the two error quantities and the deterministic product estimates Hong et al., pp. 7–8, 13, 20–22, 34.

Significance

The bounds separate the effect of initialization from persistent stochastic error. Each $G$ product carries an initial-error term, while the remaining terms show how the current step sizes, variance and bias govern the residual error. This makes the dependencies on $L$ , $L_y$ , the strong convexity moduli and the estimator variances explicit, rather than hiding them in rate notation. The paper uses this strongly convex case as one part of its broader complexity analysis Hong et al., §3, Table 1.

The source proves the claimed rates on paper; this local development currently provides compiled Lean statements with open proofs. Completing it would add reusable formal interfaces for conditional stochastic-gradient assumptions, a moving strongly convex minimizer, and weighted products of varying contraction factors. The local mission does not claim a machine-checked proof of Theorem 1 yet.

Difficulty

The outer estimate depends on $y^{k+1}$ , while the inner tracking error is measured against the minimizer at the preceding outer iterate. Treating the outer estimate as an ordinary unbiased gradient at $x^k$ loses both the surrogate-gradient discrepancy and the bias. A distance contraction for the inner step alone also does not settle the outer error, because the target $y^\star(x^k)$ moves with $x^k$ . The assumptions must keep the two histories and their conditional estimates distinct Hong et al., (7a)–(7c), (17), App. A.

Formalization scope

Lean represents both spaces by EuclideanSpace ℝ (Fin d) with $d_1,d_2\ge1$ , and Hessian blocks by continuous linear maps with operator norm. The mixed block maps inner directions to outer directions. The inner solution map is required to minimize $g(x,\cdot)$ on every $x\in X$ ; the projection is characterized as a nearest-point map on the closed convex set. These clauses prevent an arbitrary solution map or arbitrary outer update from satisfying the theorem. The $\nabla\ell$ used in (2) is defined by the displayed surrogate formula (5), so boundary points of $X$ have the same meaning as in the source.

The run starts at deterministic $(x^0,y^0)$ and uses measurable estimates with integrable squared norms. Conditional expectations are almost-sure statements relative to the sigma-algebras generated by the iterates, and $\Delta_x,\Delta_y$ are Bochner integrals. These regularity assumptions prevent totalized conditional expectation or integral operations from giving spurious zero values. The supremum defining $\widetilde\sigma_f^2$ is taken over $X$ and has an explicit bounded-above hypothesis; $X$ is nonempty because $x^0\in X$ . The goal uses positive, nonincreasing step sizes, in line with the ratio conditions and the auxiliary lemmas. The paper prints $3/4$ in the $\alpha$ ratio of (20a), while its application of Lemma 10 with $q=2$ needs $1/2$ ; the stronger ratio is disclosed in the Lean hypotheses. The initial error uses $x^{-1}=x^0$ , and real exponents use nonnegative bases.

The definition file and the seven milestone theorems are open for proof contributions. Theorem 1’s two explicit bounds are the mission goal. Lemma 3 (28) is excluded because its printed product uses a $1/2$ factor where (55) uses $1/4$ ; (55) is the selected inner target Hong et al., pp. 13, 21.

Selected references

M. Hong, H.-T. Wai, Z. Wang and Z. Yang, A Two-Timescale Stochastic Algorithm Framework for Bilevel Optimization: Complexity Analysis and Application to Actor-Critic, SIAM Journal on Optimization, 2023; arXiv preprint v4, 2022. arXiv:2007.05170v4.

10 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

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

Why this lower bound matters

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

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

Bandit setting and notation

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

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

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

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

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

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

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

Formalization target

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

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

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

What the result gives

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

9 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Generalized Turán Problems for Even Cycles 7: The Maximum Number of Paths on l Vertices in a C_{2k+1}-Free Graph on n Vertices Is (1+o(1))(n/2)^lResearch Paper

Motivation

An extremal graph problem asks how many copies of a chosen small graph can occur when a different graph is forbidden. The usual Turán problem counts edges; counting paths or cycles gives a more detailed view of the structure that can survive a forbidden subgraph. Gerbner, Győri, Methuku and Vizer study these generalized Turán numbers for paths and cycles in their paper on even-cycle problems. Their Theorem 23 asks for the leading number of paths when a specified odd cycle is absent. The answer has the same leading term as a balanced complete bipartite graph, despite the fact that excluding one odd cycle is weaker than requiring a graph to be bipartite. Gerbner et al., Theorem 23

The spectral theorem cited by the authors gives a useful threshold for this setting. For a graph with no cycle of length $2k+1$ , it bounds the adjacency spectral radius once the vertex count exceeds $320(2k+1)$ . This threshold is explicit and stays visible in the finite-size milestone. Gerbner et al., Theorem 32, citing Nikiforov (2008).

Setting

A simple graph $G$ has finitely many vertices and no loops or parallel edges. For $a\ge3$ , $C_a$ is the cycle on $a$ vertices, and $P_l$ is the path on $l$ vertices. Thus $P_l$ has $l-1$ edges, following the paper's convention. A copy of $H$ in $G$ is a subgraph of $G$ isomorphic to $H$ ; copies are unlabelled, so reversing a path does not create a second copy. Write $\mathcal N(H,G)$ for their number. Gerbner et al., pp. 2–3

For a set $A$ of lengths, a graph is $\mathcal C_A$ -free if it has no subgraph isomorphic to $C_a$ for any $a\in A$ . The mission mainly uses $A=\{2k+1\}$ : exactly one odd cycle length is forbidden, while shorter and longer cycles may still occur. The generalized Turán number is the maximum

\operatorname{ex}(n,H,\mathcal C_A) =\max_{\substack{|V(G)|=n\\G\text{ is }\mathcal C_A\text{-free}}}\mathcal N(H,G).

The adjacency matrix $A_G$ records whether each pair of vertices is adjacent. Because the graph is undirected, this is a real symmetric matrix. Its spectral radius $\mu(G)$ is the largest absolute value of an eigenvalue of $A_G$ . The graph $B_{n,a}$ is the complete bipartite graph with parts of sizes $a$ and $n-a$ ; the balanced choice uses $a=\lfloor n/2\rfloor$ . Gerbner et al., §§7.1–7.2

Formalization targets

Main result: Theorem 23

For each fixed $k\ge1$ and $l\ge2$ , as $n\to\infty$ ,

\operatorname{ex}(n,P_l,\mathcal C_{\{2k+1\}}) =(1+o(1))\left(\frac n2\right)^l.

The equality gives both sides of the asymptotic estimate. The $o(1)$ term may depend on the fixed parameters $k,l$ and tends to zero as the number of vertices grows. Gerbner et al., Theorem 23, p. 8

Supporting targets

The milestone list records the balanced complete bipartite lower bound, the comparison between paths and walks in equation (7), a spectral bound on the walk sum, Nikiforov's stated spectral estimate, and the resulting finite-size upper bound. In particular, the last two targets retain the paper's constants:

n>320(2k+1),\qquad \mu(G)\le\sqrt{n^2/4},\qquad \mathcal N(P_l,G)\le(n/2)^l.

The milestone statements identify which assertions concern every graph and which require the forbidden-cycle condition. Gerbner et al., pp. 30, 32

Companion: even cycles (Theorem 24)

For fixed $k\ge1$ and $l\ge2$ ,

\operatorname{ex}(n,C_{2l},\mathcal C_{\{2k+1\}})=(1+o(1))\,\frac{1}{2l}\left(\frac{n^2}{4}\right)^{l},

and Remark 3 records the inequality $\mathcal N(P_{2l},G)\ge 2l\,\mathcal N(C_{2l},G)$ for every graph $G$ , which links this count to Theorem 23. Gerbner et al., Theorem 24, p. 11; Remark 3, p. 32

Significance

Theorem 23 fixes the leading coefficient for the maximum path count for every fixed path length and forbidden odd-cycle length in its range. A balanced complete bipartite graph reaches that coefficient asymptotically, so the result identifies an extremal construction at first order. The lower-bound milestone formalizes this construction with balanced parts, including the one-vertex rounding needed when $n$ is odd. The matrix and spectral milestones can also be reused when counting walks or paths under different graph restrictions. Gerbner et al., §7.2

The paper proves these results on paper. In this mission, the definitions and theorem statements are checked by Lean, while proofs of the draft theorems remain to be supplied. A completed development would make the path-count theorem and its stated spectral dependency machine checked in the pinned Mathlib environment. It would also expose where a general graph identity suffices and where the odd-cycle prohibition matters.

Difficulty

Counting paths directly is difficult because the available information about a graph with one forbidden odd-cycle length does not control each vertex degree tightly enough to determine a sharp path count. Counting walks is easier algebraically, but walks may revisit vertices, so their number is generally larger than the number of paths. A graph-wide spectral bound is needed to control the walk total sharply, and the cited Nikiforov estimate has to be carried with its forbidden-cycle hypothesis and vertex threshold. A generic bound based only on the maximum degree would not yield the coefficient in Theorem 23. Gerbner et al., §§7.1–7.2

Formalization scope

Graphs on $n$ vertices are represented as SimpleGraph (Fin n). Mathlib's cycleGraph a and pathGraph l represent $C_a$ and the path on $l$ vertices, and copyCount counts unlabelled subgraph copies. The finite set of real adjacency eigenvalues defines $\mu(G)$ through a maximum of absolute values. On an empty vertex type this value is zero. The extremal number is a natural-number supremum over feasible graphs; for the odd-cycle family the feasible set is nonempty and finite, so this supremum is attained.

The goal has $k\ge1$ and $l\ge2$ , exactly as Theorem 23 states. The lower-bound item chooses parts of sizes $\lfloor n/2\rfloor$ and $\lceil n/2\rceil$ . Equation (7) requires $l\ge2$ : for $l=1$ the claimed factor of two is false. The finite spectral and path bounds require $n>320(2k+1)$ . These conditions are explicit in the Lean statements. Natural subtraction appears only in expressions whose hypotheses make the intended quantity meaningful, including $l-1$ ; the bipartite part size is computed with natural division. The asymptotic statements use real sequences tending to zero and eventual comparisons or equality.

The result must include the lower bound as well as the upper bound. It uses unlabelled path copies, an attained extremal maximum, and a forbidden family consisting of the specified odd cycle. An upper bound alone, labelled copies, or a supremum over an empty class would change the theorem. The needed infrastructure consists of graph-copy counts, adjacency-matrix walk counts, finite-dimensional spectral facts, and the cited odd-cycle spectral theorem. The page states Theorem 24 "for any $k,l$ "; the Lean statement and Remark 3 require $k\ge1$ and $l\ge2$ , the only values for which $C_{2k+1}$ and $C_{2l}$ are cycles. Contributions proving the milestones or developing reusable interfaces for those objects are within scope.

Selected references

D. Gerbner, E. Győri, A. Methuku and M. Vizer, Generalized Turán problems for even cycles, Journal of Combinatorial Theory, Series B, 2020. arXiv:1712.07079v3; DOI:10.1016/j.jctb.2020.05.005.
V. Nikiforov, A spectral condition for odd cycles in graphs, Linear Algebra and its Applications 428 (2008), 1492–1498. Cited as [34] in arXiv:1712.07079v3.

9 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Finding Cliques in Social Networks: A New Distribution-Free Model 3: For Every c ≥ 2 and n ≥ c There Is a c-Closed Graph on n Vertices with Ω(c^(−3/2)·2^(c/2)·n^(3/2)) Maximal CliquesResearch Paper

Motivation

Social networks exhibit triadic closure: two people with many common friends tend to be friends themselves. Fox, Roughgarden, Seshadhri, Wei and Wein (arXiv:1804.07431, SIAM J. Comput. 2020) turn this empirical regularity into a deterministic graph class, the $c$ -closed graphs, and ask how hard a classical NP-hard problem, enumerating maximal cliques, becomes on it. In general graphs the number of maximal cliques can be exponential: Moon and Moser showed that the maximum over $n$ -vertex graphs is $3^{n/3}$ (Moon–Moser 1965). The paper proves that on $c$ -closed graphs the count is polynomial in $n$ for every fixed $c$ , with upper bounds of order $3^{(c-1)/3} n^2$ and $4^{(c+4)(c-1)/2} n^{2-2^{1-c}}$ .

This mission formalizes the matching lower bound of the paper (Section 4): the exponent of $n$ cannot be pushed below $3/2$ , and the dependence on $c$ must be exponential.

Prior work: Eschen, Hoàng, Spinrad and Sritharan (2011) studied the $2$ -closed graphs under a different name (graphs without an induced $C_4$ or diamond) and showed that they have $O(n^{3/2})$ maximal cliques, with a matching lower bound from incidence graphs of finite projective planes. Fox et al. (2018) extended the lower bound to every $c$ by blowing up a graph of girth $5$ .

Setting

All graphs are finite, simple and undirected. For vertices $u, v$ of a graph $G=(V,E)$ , $N(u)\cap N(v)$ is the set of their common neighbours.

A graph is $c$ -closed (Definition 1.1) if any two distinct vertices with at least $c$ common neighbours are adjacent. Every $c$ -closed graph is $c'$ -closed for $c' \ge c$ ; $1$ -closed graphs are exactly disjoint unions of cliques.
A maximal clique is a set of pairwise adjacent vertices to which no further vertex of $G$ can be added. $\#\mathrm{MC}(G)$ denotes the number of maximal cliques of $G$ .
The girth of $H$ is the length of its shortest cycle ( $\infty$ for a forest). Girth at least $5$ means: no triangle and no $4$ -cycle.
The blow-up $H^{(h)}$ of a graph $H$ replaces each vertex $x$ by a set $U_x$ of $h$ vertices $(x,0),\dots,(x,h-1)$ and joins

(x,i)\sim(y,j)\iff i\neq j\ \text{ and }\ \bigl(x=y\ \text{ or }\ xy\in E(H)\bigr).

Each $U_x$ is a clique; for an edge $xy$ of $H$ the bipartite graph between $U_x$ and $U_y$ is $K_{h,h}$ minus a perfect matching; non-adjacent $x,y$ give no edges between $U_x$ and $U_y$ . The paper takes $h = c/2$ .

Formalization targets

Goal: Theorem 4.1

There is an absolute constant $C>0$ such that for all integers $c\ge 2$ and $n\ge c$ there is a $c$ -closed graph $G$ on $n$ vertices with

\#\mathrm{MC}(G)\ \ge\ C\,c^{-3/2}\,2^{c/2}\,n^{3/2}.

The constant is absolute; the dependence on $c$ is explicit. This is the paper's Theorem 4.1 (restatement of Theorem 1.7: "for any positive integer $c$ , there are $c$ -closed graphs with $n$ vertices and $\Omega(c^{-3/2}2^{c/2}n^{3/2})$ maximal cliques") with the two hypotheses $c \ge 2$ and $n \ge c$ made explicit; see Formalization scope.

Milestones

Girth-five graphs with many edges (cited from [29] on p. 12): there is $C>0$ such that for every $v\ge 2$ some graph on $v$ vertices has girth at least $5$ and at least $C v^{3/2}$ edges.
§1.4, p. 5: a graph of girth at least $5$ is $2$ -closed and each of its edges is a maximal clique, so $\#\mathrm{MC}(H)\ge |E(H)|$ .
Claim 4.2: for $h\ge 1$ and $H$ of girth at least $5$ , the blow-up $H^{(h)}$ is $2h$ -closed.
Claim 4.3 (corrected count): there is an absolute $C>0$ such that for every $k\ge1$ and $h\ge2$ one can choose a girth-at-least- $5$ graph $H$ on $2k$ vertices whose blow-up satisfies

\#\mathrm{MC}\bigl(H^{(h)}\bigr)\ \ge\ C\,(2h)^{-3/2}\,2^h\,(2kh)^{3/2}.

Significance

The result. Together with the paper's upper bounds, Theorem 4.1 brackets the maximum number of maximal cliques in a $c$ -closed $n$ -vertex graph between $n^{3/2}$ and $n^{2-2^{1-c}}$ , up to factors depending on $c$ . It shows that the exponential dependence on $c$ in the upper bounds is unavoidable, so fixed-parameter tractability in $c$ is the right notion, and that no bound of the form $f(c)\,n^{a}$ with $a<3/2$ holds. Determining the true exponent of $n$ is stated as an open problem in Section 5 of the paper.

Formalizing it. The result is proved on paper; no machine-checked proof is known. A formal development produces a verified lower-bound construction for maximal cliques, a reusable blow-up operation with its clique structure, and, through milestone 1, a formal proof of the classical $\Omega(v^{3/2})$ lower bound for $C_4$ -free graphs, which Mathlib does not yet contain.

Difficulty

The combinatorial core (Claims 4.2 and 4.3) is a finite case analysis, but the paper's own count is not correct as printed: of the $2^{c/2}$ cliques obtained from an edge $xy$ , two are $U_x$ and $U_y$ , which every edge at $x$ or $y$ produces again, so they are not distinct across edges. The corrected per-edge count is $2^{c/2}-2$ , and for $c=2$ the blow-up is edgeless, so small $c$ must be handled by $H$ itself.

The main difficulty is milestone 1. Graphs of girth $5$ with $\Omega(v^{3/2})$ edges for every $v$ require an algebraic construction (polarity graphs of projective planes over $\mathbb F_q$ , or incidence graphs, which have girth $6$ ) together with a density-of-primes argument to pass from $v \approx q^2$ to arbitrary $v$ . Random graphs do not suffice: deletion arguments give only $\Omega(v^{4/3})$ edges. Finally, Theorem 4.1 is stated for all $n \ge c$ and all $c \ge 2$ , while the construction works for even $c$ and $c \mid n$ ; the paper notes that the reduction loses only an absolute constant factor, but a complete proof has to carry it out uniformly in $c$ and $n$ , including the range where $n$ is close to $c$ .

Formalization scope

Graphs on $n$ vertices are SimpleGraph (Fin n); the blow-up lives on V × Fin h. Common neighbours are counted with Set.ncard, and "at least $c$ " is c ≤, not c <.
$\#\mathrm{MC}(G)$ counts finite vertex sets that are maximal (Mathlib's Maximal) among cliques; it does not count all cliques, nor cliques of a fixed size.
Girth is Mathlib's egirth (valued in $\mathbb N\cup\{\infty\}$ ): "girth $\ge 5$ " is 5 ≤ H.egirth, which admits forests. The ℕ-valued girth, which is $0$ for forests, is not used. Edge counts are H.edgeSet.ncard.
The perfect matching between $U_x$ and $U_y$ is fixed as $(x,i)\leftrightarrow(y,i)$ for every edge of $H$ , one admissible choice in the paper's construction (which allows any perfect matching).
Powers $c^{-3/2}$ , $2^{c/2}$ , $n^{3/2}$ are real powers.
Added hypotheses, disclosed. The goal adds $c\ge 2$ and $n\ge c$ to the printed "for any positive integer $c$ ". Without $c\ge 2$ the statement is false, since a $1$ -closed graph has at most $n$ maximal cliques. Without $n \ge c$ it is false, since Moon–Moser caps every $n$ -vertex graph at $3^{n/3}$ maximal cliques, which is below $c^{-3/2}2^{c/2}n^{3/2}$ when $n$ is small compared with $c$ . The construction itself assumes that $n$ is a positive multiple of $c$ . Claim 4.3 is restricted to $h\ge 2$ : for $h=1$ the blow-up is edgeless. Its proof counts $(2^h-2)|E(H)|$ distinct mixed cliques, correcting the paper's printed per-edge count while retaining its $\Omega$ conclusion. The reductions to even $c$ and $c\mid n$ are part of the proof, not hypotheses.
Ruled out. The constant $C$ is chosen before $c$ and $n$ ; a statement with $C$ depending on $c$ or $n$ would make the factor $c^{-3/2}2^{c/2}$ meaningless. Milestone 1 requires both the girth condition and the edge bound; either alone is trivial (the complete graph, or the empty graph). Counting all cliques instead of maximal ones, or reading "at least $c$ " as "more than $c$ ", changes the theorem.
The shared CClosedGraphs.Peeling.Setting supplies IsCClosed and the maximal-clique counts; CClosedGraphs.LowerBound.Setting defines the blow-up. Contributions of a general Mathlib-style theory of $C_4$ -free extremal graphs (polarity graphs, Turán number of $C_4$ ) are especially welcome and reusable beyond this mission.

Selected references

J. Fox, T. Roughgarden, C. Seshadhri, F. Wei, N. Wein, Finding cliques in social networks: a new distribution-free model, arXiv:1804.07431v1, 2018; SIAM J. Comput. 49(2), 2020. https://arxiv.org/abs/1804.07431, https://doi.org/10.1137/18M1210459
E. M. Eschen, C. T. Hoàng, J. P. Spinrad, R. Sritharan, On graphs without a $C_4$ or a diamond, Discrete Appl. Math. 159(7):581–587, 2011. https://arxiv.org/abs/0909.4719
Z. Füredi, M. Simonovits, The history of degenerate (bipartite) extremal graph problems, in Erdős Centennial, Bolyai Soc. Math. Stud. 25, Springer, 2013, pp. 169–264. https://arxiv.org/abs/1306.5167
J. W. Moon, L. Moser, On cliques in graphs, Israel J. Math. 3(1):23–28, 1965. https://doi.org/10.1007/BF02760024
W. G. Brown, On graphs that do not contain a Thomsen graph, Canad. Math. Bull. 9:281–285, 1966. https://doi.org/10.4153/CMB-1966-036-2

7 thms2 active usersReviewed

Bandit Algorithms Machine Learning Reinforcement Learning·Captain: mikedeng1

The Statistical Complexity of Interactive Decision Making VIII: Linear Bandits on the Unit Ball Have Localized DEC at Least d/(12γ)Research Paper

Why a lower bound on the DEC for linear bandits

In a linear bandit a learner repeatedly chooses a decision $\pi$ from a set $\Pi \subseteq \mathbb{R}^d$ and observes a noisy reward whose mean is $\langle \theta^\star, \pi\rangle$ for an unknown parameter $\theta^\star$ . It is the standard model for sequential decisions with many correlated actions, such as ad placement, routing and recommendation, and its minimax regret over $T$ rounds is known to scale as $d\sqrt{T}$ up to logarithmic factors (Dani, Hayes and Kakade, COLT 2008; see Lattimore and Szepesvári, 2020, Ch. 19–24).

Foster, Kakade, Qian and Rakhlin (2021) introduce the Decision-Estimation Coefficient (DEC), a single complexity measure that yields both upper and lower bounds on the regret of every interactive decision problem. A complexity measure of this kind is only useful if it is tight on the classical examples. Proposition 6.2 of that paper checks this for linear bandits on the Euclidean unit ball: the localized DEC is at least of order $d/\gamma$ , which, through the paper's general lower bound (Theorem 3.2), gives the regret lower bound $\Omega(\sqrt{dT})$ . Proposition 6.8 gives the analogous statement for linear bandits whose models have a fixed gap $\Delta$ .

Setting

Let $\mathbb{B}^d = \{v \in \mathbb{R}^d : \|v\|_2 \le 1\}$ be the closed Euclidean unit ball. It is both the decision space $\Pi$ and the parameter set $\Theta$ . A model with parameter $\theta \in \Theta$ returns, at decision $\pi$ , an outcome in $\{-1, +1\}$ drawn from the Rademacher distribution $\mathrm{Rad}(\langle\theta,\pi\rangle)$ , which puts mass $(1+\mu)/2$ on $+1$ and $(1-\mu)/2$ on $-1$ when its mean is $\mu$ . The mean reward is $f^\theta(\pi) = \langle \theta, \pi\rangle$ .

A maximizer selector $\theta \mapsto \pi_\theta$ picks a decision with $\langle\theta,\pi\rangle \le \langle\theta,\pi_\theta\rangle$ for all $\pi$ . The regret of a decision is $g^\theta(\pi) = f^\theta(\pi_\theta) - f^\theta(\pi)$ . Two outcome laws are compared by the squared Hellinger distance $D^2_{\mathrm{H}}(P,Q) = \sum_y (\sqrt{P(y)}-\sqrt{Q(y)})^2$ .

Given a reference model $\overline{M}$ , the $L_\infty$ -localized class at radius $\varepsilon$ is

\mathcal{M}^\infty_\varepsilon(\overline{M}) = \{ M \in \mathcal{M} : |g^M(\pi) - g^{\overline{M}}(\pi)| \le \varepsilon \ \ \forall \pi \in \Pi \},

and the DEC at scale $\gamma > 0$ is

\mathsf{dec}_\gamma(\mathcal{M}', \overline{M}) = \inf_{p \in \Delta(\Pi)} \sup_{M \in \mathcal{M}'} \mathbb{E}_{\pi\sim p}\bigl[ g^M(\pi) - \gamma\, D^2_{\mathrm{H}}(M(\pi), \overline{M}(\pi)) \bigr],

the infimum running over all Borel probability measures $p$ on $\Pi$ .

Formalization targets

Goal: Proposition 6.2

For all $d \ge 4$ and $\gamma \ge 2d/3$ there is $\overline{M} \in \mathcal{M}$ with

\mathsf{dec}_\gamma\bigl(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}\bigr) \ge \frac{d}{12\gamma}, \qquad \varepsilon_\gamma = \frac{2d}{3\gamma}.

The page prints $\varepsilon_\gamma = d/(3\gamma)$ . The hard family of its proof has regret functions $\Delta(1-\pi_i)$ , which reach $2\Delta$ at $\pi = -e_i$ while the reference regret is identically $0$ , so the family lies in the class of radius $2\Delta$ and not in the class of radius $\Delta$ . The goal is stated at the radius the proof supports.

Milestones

Lemma A.8: $D^2_{\mathrm{H}}(\mathrm{Rad}(\mu), \mathrm{Rad}(0)) \le \tfrac34\mu^2$ on $[-1,1]$ , together with the two general bounds of the lemma.
Lemma 5.1: an $(\alpha,\beta,\delta)$ -family forces $\mathsf{dec}_\gamma \ge \alpha/2 - \gamma(\beta/N + \delta)$ , stated for a general measurable decision space.
The hard family $\theta_i = \Delta e_i$ : regret $\Delta(1-\pi_i)$ and $D^2_{\mathrm{H}}(M_i(\pi), \mathrm{Rad}(0)) \le \tfrac34\Delta^2\pi_i^2$ . With the coordinate bounds $\sum_i \pi_i \le \sqrt d \le d/2$ ( $d \ge 4$ ) and $\sum_i \pi_i^2 \le 1$ , stated as a separate item, this makes the family a $(\Delta, \tfrac34\Delta^2, 0)$ -family.
Localization: the family lies in $\mathcal{M}^\infty_{2\Delta}(\mathrm{Rad}(0))$ .

Companion: Proposition 6.8

For $\Delta \in (0, 1/4)$ and $d \ge 2$ , an explicit class of linear bandit models on $\{e_1,\dots,e_d\}$ , each with gap $\Delta$ , satisfies $\mathsf{dec}_\gamma(\mathcal{M}^\infty_\Delta(\overline{M}),\overline{M}) \ge (\Delta/4)\,\mathbb{I}\{\gamma \le d/(12\Delta)\}$ for all $\gamma > 0$ .

Significance

The bound shows that the DEC of linear bandits under Euclidean geometry is of order $d/\gamma$ , which matches, up to constants, the upper bound $\mathsf{dec}^{\mathrm{Sq}}_\gamma \le d/(4\gamma)$ on the square-loss variant of the DEC certified by the strategy of Proposition 6.1. Through Theorem 3.2 it gives the regret lower bound $\Omega(\sqrt{dT})$ for every algorithm. Proposition 6.8 shows that the DEC gives meaningful lower bounds even for classes of models with a fixed gap.

All results are proved in the paper. None has a machine-checked proof. The mission produces a formal statement of the linear-bandit lower bound with its radius corrected, the hard-family lemma (Lemma 5.1) in a form that applies to infinite decision spaces and to range-free $u_i$ , and the Rademacher Hellinger estimates that later DEC lower bounds reuse.

Difficulty

The arithmetic of the construction is short. The work is in the infrastructure.

The infimum runs over all Borel probability measures on the ball, not over finitely supported ones. Lemma 5.1 must therefore be proved for Bochner integrals, with the integrability of the payoff established from its continuity on the compact ball.
The bound $\sum_i \pi_i \le \sqrt d \le d/2$ is Cauchy–Schwarz on $\mathbb{R}^d$ and needs $d \ge 4$ .
The value $\langle\theta_i, \pi_{\theta_i}\rangle = \Delta$ must come from the selector hypothesis plus Cauchy–Schwarz, because the selector is not given explicitly.
Lemma 5.1 cannot be applied in the form printed in Definition 5.1: there $u_i$ takes values in $[0,1]$ , but the family's $u_i(\pi) = \pi_i$ can be negative. The lemma is needed without the range conditions.

Formalization scope

Outcomes. They are finite: the $\pm1$ outcome is encoded on Bool, and models are the Rademacher laws $\mathrm{Rad}(\langle\theta,\pi\rangle)$ , identified with their parameters $\theta \in \mathbb{B}^d$ . The paper's class contains every reward law on $[-1,1]$ with linear mean. The Rademacher subclass has a smaller localized class, so a lower bound for it implies the paper's.
Decisions. For the goal they range over the ball itself (an infinite space with its Borel $\sigma$ -algebra), and decision distributions are arbitrary ProbabilityMeasures on it.
The DEC is unfolded. For every $p$ some model of the localized class attains the bound. This is what the proof shows, and it implies the inf–sup inequality.
Selectors. $\pi_M$ is a selector with a maximizer hypothesis, so statements hold for every choice of maximizer.
Added hypotheses. Lemma 5.1 carries $\alpha, \beta \ge 0$ and integrability of its four functions. Proposition 6.8 carries $d \ge 2$ .
No trivializing reading. The integrals in the goal are genuine: the integrand is bounded and continuous, and a sanity file proves integrability, so the Bochner convention $\int f = 0$ for non-integrable $f$ never applies. The goal's quantifier over $p$ is not restricted. The radius $2d/(3\gamma)$ is the smallest the construction allows.
Definitions and reuse. The mission defines the unit ball, $\mathrm{Rad}$ , the linear model, the regret $g^\theta$ , and the localized class over a measurable decision space. It references the published hellingerSq, fM and decGf. The general Lemma 5.1 and Lemma A.8 are reusable for every DEC lower bound in §§5–7.

Contributions welcome: proofs of the milestones, a version of the goal through an explicit inf–sup definition of the DEC over measures, and the general model class with arbitrary reward laws on $[-1,1]$ .

Selected references

D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, v3, 2023. https://arxiv.org/abs/2112.13487
T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020 (linear bandits, Ch. 19–24). https://doi.org/10.1017/9781108571401
D. J. Foster, C. Gentile, M. Mohri, J. Zimmert, Adapting to Misspecification in Contextual Bandits, NeurIPS 2020 (Proposition 6.1's strategy). https://arxiv.org/abs/2107.05745

11 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Operations Research+1·Captain: mikedeng1

Approximate Revenue Maximization with Multiple Items 5: Bundling Is Optimal for Two I.I.D. Goods Whose Density on [a, ∞) Satisfies x f′(x) + (3/2) f(x) ≤ 0Research Paper

Motivation

A seller with several goods and a single buyer of unknown, additive valuation faces the multi-dimensional revenue maximization problem. For one good the answer is classical: by Myerson's theorem (Myerson 1981) a single posted price is optimal. For two or more goods no such simplification exists in general: optimal mechanisms may randomize, may offer menus of lotteries, and are rarely known in closed form. Selling the grand bundle at one price is the simplest multi-good mechanism, and it is used widely in practice.

Hart and Nisan (arXiv:1204.1846, J. Econ. Theory 2017) quantify how much revenue simple mechanisms lose. Most of their results are approximation bounds. Section 7.2 of the paper also contains an exact result: for two independent and identically distributed goods whose density decays fast enough, in the sense of a differential inequality, bundling is exactly optimal. This mission formalizes that theorem, Theorem 16, and the steps of its proof in Appendix A.6.

Timeline. Manelli and Vincent (2006) gave conditions under which a bundled mechanism is optimal for a multiple-good monopolist. Hart and Nisan's preprint (2012, revised 2017) proved Theorem 16 with the condition $x f'(x) + \tfrac32 f(x) \le 0$ . Daskalakis, Deckelbaum and Tzamos (2017) later gave a strong duality theory for the multiple-good monopolist, based on optimal transport.

Setting

There are two goods and one buyer. A valuation is a vector $x = (y, z) \in \mathbb{R}^2_+$ . The buyer's values $Y, Z$ are i.i.d. with a one-good law $F$ on $\mathbb{R}_+$ .

A mechanism $\mu = (q, s)$ assigns to each reported valuation $x$ an allocation vector $q(x) \in [0,1]^2$ ( $q_i(x)$ is the probability that good $i$ is sold) and a payment $s(x) \in \mathbb{R}$ . The buyer's payoff is $b(x) = q(x)\cdot x - s(x)$ . The mechanism is

incentive compatible (IC) if $b(x) \ge q(\tilde x)\cdot x - s(\tilde x)$ for all $x, \tilde x \in \mathbb{R}^2_+$ ;
individually rational (IR) if $b(x) \ge 0$ for all $x$ ;
NPT (no positive transfer) if $s \ge 0$ .

The revenue of $\mu$ is $R(\mu; X) = \mathbb{E}[s(X)]$ , and the optimal revenue is $\mathrm{Rev}(X) = \sup R(\mu; X)$ over all IC and IR mechanisms. The bundled revenue is $\mathrm{BRev}(X) = \mathrm{Rev}(Y + Z)$ , the optimal revenue from selling the bundle as a single good.

A two-good mechanism is symmetric if $q_1(y,z) = q_2(z,y)$ and $s(y,z) = s(z,y)$ . For a level $a \ge 0$ , the bundled majorant $\hat\mu = (\hat q, \hat s)$ of $\mu$ is

\hat q(y,z) = \bigl(q_1(y+z-a, a),\ q_1(y+z-a, a)\bigr), \qquad \hat s(y,z) = \hat q(y,z)\cdot(y,z) - b(y+z-a, a).

It depends on $(y,z)$ only through $y + z$ , so it is a bundled mechanism.

Formalization targets

Goal: Theorem 16

Let $a > 0$ and let $F$ have a density $f$ supported in $[a, \infty)$ , differentiable on $(a,\infty)$ , with

x f'(x) + \tfrac32 f(x) \le 0 \qquad (x > a). \tag{9}

Then for two i.i.d.- $F$ goods,

\mathrm{Rev}(X_1, X_2) = \mathrm{BRev}(X_1, X_2) = \mathrm{Rev}(X_1 + X_2).

The substance is $\mathrm{Rev} \le \mathrm{BRev}$ . The reverse inequality holds for every law, and the second equality is the definition of $\mathrm{BRev}$ .

Milestones

Proposition 5 (at least one good): IC holds if and only if $b$ is convex and $q(x)$ is a subgradient of $b$ at every $x$ .
Proposition 6 (iii) (at least one good): the supremum defining $\mathrm{Rev}$ may be restricted to NPT mechanisms.
Symmetrization (p. 32): for i.i.d. goods, the symmetrization $\bar\mu$ is IC, IR, NPT and symmetric, and it has the same revenue.
Display (18): for symmetric IC $\mu$ and $y, z \ge a$ , $b(y,z) \le b(y+z-a, a)$ .
$\hat\mu$ is feasible, IC and IR on the quadrant $[a,\infty)^2$ , and bundled.
Under (9), $R(\mu; X) \le R(\hat\mu; X)$ for symmetric IC, IR and NPT $\mu$ .

Companion: Corollary 17

For two i.i.d. goods with the equal-revenue law $\mathbb{P}[V \ge p] = 1/p$ ( $p \ge 1$ ),

\mathrm{Rev}(V_1,V_2) = \mathrm{BRev}(V_1,V_2) = 2(w+1) \approx 2.56,

where $w e^{w+1} = 1$ .

Significance

Theorem 16 is one of the few closed-form optimality results for multi-good monopoly. It gives an explicit, checkable condition: $x^{3/2} f(x)$ is nonincreasing. The condition covers the equal-revenue distribution and Pareto distributions with index $\alpha \ge 1/2$ . On these distributions the optimal revenue reduces to a one-dimensional pricing problem for $Y + Z$ . Corollary 17 is the resulting exact value for two equal-revenue goods. Elsewhere in the paper, Theorems C and D use the equal-revenue law as the extremal example for the approximation ratios.

The theorem is proved in the paper. As far as is known it has not been machine-checked. The mission formalizes the model and every step of the proof as a separate milestone. These steps are Rochet's characterization (Proposition 5), the NPT reduction, symmetrization, the convexity majorization (18), and the revenue comparison under (9). Propositions 5 and 6 (iii) and symmetrization are shared with other missions of this series, so they are reusable beyond Theorem 16.

Difficulty

The obvious approach is to show that the optimal mechanism is bundled by exhibiting it. This fails because nothing is known about the optimal mechanism, and it need not exist. The proof instead compares an arbitrary symmetric mechanism with its bundled majorant $\hat\mu$ . A pointwise comparison fails: $\hat b \ge b$ does not imply $\hat s \ge s$ . The comparison holds only in expectation and only for densities satisfying (9); without (9) bundling is not optimal in general.

Making this rigorous requires several things:

the a.e. differentiability of the convex function $b$ , together with $q_1 = \partial b/\partial y$ a.e.;
integration by parts on truncated squares $[a, M]^2$ with possibly infinite total revenue;
control of the boundary term at $y = a$ , where $f$ need not be bounded or continuous;
the extension of $\hat\mu$ , defined on $[a,\infty)^2$ , to an IC and IR mechanism on all of $\mathbb{R}^2_+$ .

Formalization scope

Valuations are functions $\mathrm{Fin}\ 2 \to \mathbb{R}_{\ge 0}$ , and random valuations are given by their laws. "Two i.i.d. goods" is the product measure $\nu \otimes \nu$ . The law $\nu$ is the image on $\mathbb{R}_{\ge0}$ of $f(x)\,dx$ , so no mass is lost because $f = 0$ below $a > 0$ . "Density function" means: $f$ measurable, $f \ge 0$ , $\int f = 1$ , and $f = 0$ on $(-\infty, a)$ . Continuity of $F$ is then automatic. Differentiability of $f$ is required at every $x > a$ , the range of (9). Nothing is assumed about $f$ at $a$ ; in particular $f$ may blow up there.

Admissible mechanisms are feasible, IC, IR and have a measurable payment function. The paper allows measurability without loss of generality (footnote 12). Revenue $R(\mu;X)$ is an extended real, so a non-integrable payment never collapses to $0$ . $\mathrm{Rev}$ takes values in $[0,\infty]$ and may be infinite under (9), for instance for $f(x) = c\,x^{-3/2}$ on $[a,\infty)$ . Milestone 5 states IC and IR of $\hat\mu$ on the quadrant only, as the paper defines $\hat\mu$ there. Off the quadrant, $y + z - a$ is truncated at $0$ .

The goal must not be stated as the second equality alone, which is definitional. Nor may it assume the law is bounded or that $f(a)$ is finite: these would replace the theorem with a special case. The display (17) and the limit formula (16) are not posed, because their boundary term $2a f(a)\int b(a,z) f(z)\,dz$ refers to the value of $f$ at $a$ , which the hypotheses do not control.

A complete development needs Rochet's characterization, a.e. gradients of convex functions on $\mathbb{R}^2_+$ , Fubini–Tonelli on the product law, one-dimensional integration by parts with an absolutely continuous weight, and Myerson's one-good formula for Corollary 17. Contributions of any of these as standalone lemmas are welcome.

Selected references

S. Hart and N. Nisan, Approximate Revenue Maximization with Multiple Items, J. Econ. Theory 172 (2017); arXiv:1204.1846v3. https://arxiv.org/abs/1204.1846
R. Myerson, Optimal Auction Design, Math. Oper. Res. 6 (1981) 58–73. https://doi.org/10.1287/moor.6.1.58
J.-C. Rochet, The taxation principle and multi-time Hamilton–Jacobi equations, J. Math. Econ. 14 (1985) 113–128. https://doi.org/10.1016/0304-4068(85)90015-1
A. Manelli and D. Vincent, Bundling as an optimal selling mechanism for a multiple-good monopolist, J. Econ. Theory 127 (2006) 1–35. https://doi.org/10.1016/j.jet.2005.08.007
S. Hart and P. Reny, Maximal revenue with multiple goods: nonmonotonicity and other observations, Theoretical Economics 10 (2015) 893–922. https://doi.org/10.3982/TE1517
C. Daskalakis, A. Deckelbaum and C. Tzamos, Strong duality for a multiple-good monopolist, Econometrica 85 (2017) 735–767. https://doi.org/10.3982/ECTA12618

9 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Operations Research+1·Captain: mikedeng1

Approximate Revenue Maximization with Multiple Items 1: For Independent Groups of Goods Y and Z, Rev(Y, Z) ≤ Rev(Y) + Rev(Z) + BRev(Y) + BRev(Z)Research Paper

Motivation

A seller who offers several goods to a buyer with private values has to choose a selling mechanism. For one good the optimal mechanism is known: post the best take-it-or-leave-it price (Myerson 1981). For two or more goods the optimal mechanism can be complicated: it may use lotteries, its menu may be infinite, and it may not be computable in closed form even for simple value distributions. Sellers therefore use simple mechanisms, such as selling each good separately or selling all goods as one bundle, and the question is how much revenue this costs.

Hart and Nisan (arXiv:1204.1846v3, J. Econ. Theory 2017) answer this with guaranteed fractions of the optimal revenue. Their basic tool is a decomposition theorem: when the goods split into two groups whose values are independent, the optimal revenue from all goods together is bounded by revenues computed from each group separately. This mission formalizes that theorem (Theorem 7) and the paper's first headline result, Theorem A, which is its two-good case.

Setting

There are $k \ge 1$ goods and one buyer with additive values. A valuation is a vector $x \in \mathbb{R}^k_+$ , and a $k$ -good random valuation $X$ is a random vector in $\mathbb{R}^k_+$ whose law the seller knows.

A mechanism $\mu = (q, s)$ consists of an allocation $q : \mathbb{R}^k_+ \to [0,1]^k$ , where $q_i(x)$ is the probability that the buyer receives good $i$ when reporting $x$ , and a payment $s : \mathbb{R}^k_+ \to \mathbb{R}$ . The buyer's payoff from truthful reporting is $b(x) = q(x)\cdot x - s(x)$ . The mechanism is

incentive compatible (IC) if $b(x) \ge q(\tilde x)\cdot x - s(\tilde x)$ for all $x, \tilde x \in \mathbb{R}^k_+$ ;
individually rational (IR) if $b(x) \ge 0$ for all $x$ ;
no positive transfer (NPT) if $s(x) \ge 0$ for all $x$ .

Let $\mathcal M$ be the class of IC and IR mechanisms. The expected revenue of $\mu \in \mathcal M$ is $R(\mu; X) = \mathbb{E}[s(X)]$ , which lies in $(-\infty, +\infty]$ , and the optimal revenue is

\mathrm{Rev}(X) = \sup_{\mu \in \mathcal M} R(\mu; X) \in [0, \infty].

Two benchmarks reduce to one-good problems: the separate revenue $\mathrm{SRev}(X) = \mathrm{Rev}(X_1) + \dots + \mathrm{Rev}(X_k)$ and the bundled revenue $\mathrm{BRev}(X) = \mathrm{Rev}(X_1 + \dots + X_k)$ . Finally $\mathrm{Val}(X) = \mathbb{E}[\sum_i X_i]$ is the expected total value.

For the decomposition, $Y$ is a random valuation for $k_1 \ge 1$ goods and $Z$ one for $k_2 \ge 1$ goods. The coordinates of $Y$ may be arbitrarily dependent, and so may those of $Z$ , but the vectors $Y$ and $Z$ are independent. $\mathrm{Rev}(Y, Z)$ is the optimal revenue from selling all $k_1 + k_2$ goods together, and $X\mathbf 1_{X \in A}$ is the random valuation equal to $X$ on the event $X \in A$ and to $0$ otherwise.

Formalization targets

Goal: Theorem 7 (p. 18)

If $Y$ and $Z$ are independent, then

\mathrm{Rev}(Y, Z) \le \mathrm{Rev}(Y) + \mathrm{Rev}(Z) + \mathrm{BRev}(Y) + \mathrm{BRev}(Z) \le 2\big(\mathrm{Rev}(Y) + \mathrm{Rev}(Z)\big).

Both inequalities are part of the goal, with the same middle term.

Milestones, in the order of the paper's proof

Proposition 6 (iii), p. 14: $\mathrm{Rev}(X)$ is the supremum of $R(\mu; X)$ over IC, IR and NPT mechanisms.
The NPT split, p. 20: $\mathrm{Rev}(Y,Z) \le \mathrm{Rev}\big((Y,Z)\mathbf 1_{\sum_i Y_i \ge \sum_j Z_j}\big) + \mathrm{Rev}\big((Y,Z)\mathbf 1_{\sum_j Z_j \ge \sum_i Y_i}\big)$ .
Proposition 6 (iv), p. 14: for $\mu \in \mathcal M$ and a set $A$ of values, $\mathbb{E}[s(X)\mathbf 1_{X\in A}] \le \mathrm{Rev}(X\mathbf 1_{X\in A}) \le \mathrm{Rev}(X)$ .
Lemma 8, p. 19: $\mathrm{Rev}\big((Y,Z)\mathbf 1_{(Y,Z)\in A}\big) \le \mathrm{Rev}(Y) + \mathrm{Val}\big(Z\mathbf 1_{(Y,Z)\in A}\big)$ .
Lemma 9, p. 20: for one-dimensional independent $Y, Z$ , $\mathrm{Val}(Z\mathbf 1_{Y \ge Z}) \le \mathrm{Rev}(Y)$ .
Lemma 10, p. 20: $\mathrm{Val}\big(Z\mathbf 1_{\sum_i Y_i \ge \sum_j Z_j}\big) \le \mathrm{BRev}(Y)$ .
BRev ≤ Rev, p. 18.

Companions

Theorem A in the form (2), p. 16: for two independent goods $Y, Z$ , $\mathrm{Rev}(Y, Z) \le 2(\mathrm{Rev}(Y) + \mathrm{Rev}(Z))$ . Also posed is display (5), p. 17: $z\cdot\mathbb{P}[Y \ge z] \le \mathrm{Rev}(Y)$ for one good and every $z \ge 0$ .

Significance

Theorem A says that for two independent goods, selling them separately guarantees half of the optimal revenue, whatever the distributions. Theorem 7 extends this to two independent groups of goods. It is the induction step behind the paper's bounds for many goods: separate selling guarantees a fraction $c/\log^2 k$ of the optimal revenue for $k$ independent goods (Theorem C), and bundling guarantees $c/\log k$ for $k$ i.i.d. goods (Theorem D). These are other missions of this series, and both use Theorem 7 as a black box. The same approach underlies later work on simple versus optimal mechanisms, for example Babaioff, Immorlica, Lucier and Weinberg (FOCS 2014) and Li and Yao (PNAS 2013).

All results posed here are proved in the paper. As far as we know, none has a machine-checked proof. A formal proof would give a reusable development of mechanism design with multi-dimensional types: IC and IR mechanisms on $\mathbb{R}^k_+$ , revenue as an extended-real expectation, restriction of mechanisms to subdomains, and marginal mechanisms obtained by fixing some coordinates of an independent product.

Difficulty

The proofs are short on paper but rest on measure theory the prose passes over. Lemma 8 conditions on $Z = z$ and applies Proposition 6 (iv) to a one-group mechanism for each fixed $z$ . Formally this is a Tonelli argument on a product measure, with an integrand that may be negative on part of the space and $+\infty$ in expectation. The induced mechanism $s^z(y) = s(y, z) - \sum_j q_j(y,z) z_j$ involves the allocation $q$ , which is not assumed measurable. Proposition 6 (iv) bounds a mechanism with possibly negative payments by the optimal revenue on a modified valuation $X\mathbf 1_{X \in A}$ , and this requires shifting the mechanism to make it NPT. Finally, every revenue may be infinite, so the inequalities must be handled in $[0,\infty]$ and in the extended reals, without cancelling.

A natural first idea is to apply Theorem A coordinate by coordinate. This fails, because the coordinates inside $Y$ may be dependent. Only the independence of $Y$ from $Z$ is available, and the bound must go through the bundled revenue $\mathrm{BRev}$ .

Formalization scope

Valuations as laws. A random valuation is represented by its law, a probability measure on ι → ℝ≥0 for a finite type ι of goods. Every quantity of the paper depends only on the law. One good is ι = Unit.
Independence as a product law. The law of $(Y,Z)$ is the product of the laws of $Y$ and $Z$ , transported to ι₁ ⊕ ι₂ → ℝ≥0. Theorems that need independence are never stated over an arbitrary joint law with given marginals, since they are false for correlated groups. The NPT split in the proof of Theorem 7 is stated for independent groups, as on the page. Proposition 6 applies to an arbitrary law.
The class $\mathcal M$ . $\mathcal M$ requires $q \in [0,1]^k$ , IC, IR and a measurable payment $s$ , the last as allowed by the paper's footnote 12. $q$ is not required to be measurable.
Revenue. $R(\mu;X)$ is $\int s^+ - \int s^-$ in the extended reals, so that $\mathbb{E}[s(X)] = +\infty$ is kept. Since $s \ge s(0)$ under IC, the negative part is finite. The Bochner integral is not used, because it would assign $0$ to a non-integrable payment. $\mathrm{Rev}$ , $\mathrm{SRev}$ , $\mathrm{BRev}$ and $\mathrm{Val}$ take values in $[0,\infty]$ .
Subdomains. $X\mathbf 1_{X\in A}$ is the image law under $x \mapsto x\mathbf 1_A(x)$ , and $A$ is assumed measurable. The regions of the proof of Theorem 7 are both closed, so the diagonal is counted twice, as in the paper.
Not trivializable. A formalization in which $\mathrm{Rev}$ is computed with a Bochner integral, the expected revenue is clipped before comparing a single mechanism with $\mathrm{Rev}$ , or independence is dropped does not state the paper's theorem, and none of these is used.
Not posed. The ratio form of Theorem A ( $\mathrm{GFOR} \ge 1/2$ ) is not posed, because of its conventions $0/0 = 1$ and $\infty/\infty$ . Theorems B, C, D, 16 and 33 are separate missions of this series.

Contributions are welcome at every level: Proposition 6 (the NPT shift and subdomain restriction), the marginal-mechanism construction behind Lemma 8, and the one-good facts (5) and Lemma 9 are all reusable in the sibling missions on Theorems C and D.

Selected references

S. Hart and N. Nisan, Approximate Revenue Maximization with Multiple Items, Journal of Economic Theory 172 (2017); preprint arXiv:1204.1846v3, 2017. https://arxiv.org/abs/1204.1846
R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6 (1981) 58–73. https://doi.org/10.1287/moor.6.1.58
S. Hart and P. J. Reny, Maximal Revenue with Multiple Goods: Nonmonotonicity and Other Observations, Theoretical Economics 10 (2015) 893–922. https://doi.org/10.3982/TE1517
M. Babaioff, N. Immorlica, B. Lucier and S. M. Weinberg, A Simple and Approximately Optimal Mechanism for an Additive Buyer, FOCS 2014. https://arxiv.org/abs/1405.6146
X. Li and A. C.-C. Yao, On Revenue Maximization for Selling Multiple Independently Distributed Items, PNAS 110 (2013) 11232–11237. https://doi.org/10.1073/pnas.1309533110

9 thms2 active usersReviewed

Dynamical Systems Machine Learning Probability·Captain: mikedeng1

Approximation Bounds for Random Neural Networks and Reservoir Systems III: Echo State Networks with Output Feedback and Random Weights Approximate Contracting Reservoirs (Theorem 4)Research Paper

Motivation

An echo state network with output feedback is a recurrent model whose previous output is fed back into its next hidden-state update. In reservoir computing only the linear output weights are trained, while the internal weights are fixed, typically after being drawn at random. This raises a quantitative question: if the internal rows are sampled from a fixed law, can a network with $N$ blocks of random rows and a suitable linear readout approximate a given input–output rule, and at what rate in $N$ ? Gonon, Grigoryeva and Ortega answer this for targets generated by contracting reservoir systems. Their Theorem 4 (p. 63) gives, with explicit constants, a probability bound and an excess-risk bound of order $1/\sqrt N$ , plus a term decaying geometrically in the length $T$ of the observation window. The input set is not required to be bounded: the bound depends on the input process only through $\mathbb E[\max_{t}\|Z_t\|]$ over the window.

Setting

Inputs are vectors in a set $D_d\subseteq\mathbb R^d$ and an input history is $z=(z_t)_{t\in\mathbb Z_-}$ , with $\mathbb Z_-=\{0,-1,-2,\dots\}$ . A target reservoir is a map $F^*:\mathbb R^{N^*}\times D_d\to B_M$ , with $B_M$ the closed Euclidean ball of radius $M$ , such that $F^*(\cdot,v)$ is an $r$ -contraction for every $v\in D_d$ , with $r\in(0,1)$ . Its reservoir functional is $H^*(z)=x^*_0$ , where $x^*_t=F^*(x^*_{t-1},z_t)$ for all $t\in\mathbb Z_-$ . The output dimension is $m=N^*$ .

The approximating network has $N$ blocks of $N^*$ rows. Each row is a vector $\omega=(a,c,\zeta)\in\mathbb R^{N^*+d+1}$ , and the $\bar N=NN^*$ rows $U_j^{(i)}$ of $[A,C,\zeta]$ are i.i.d. with law $\pi$ . With an activation $\sigma$ and a readout matrix $W\in\mathbb M_{m,\bar N}$ , the system is

x_t=\sigma(Ay_{t-1}+Cz_t+\zeta),\qquad y_t=Wx_t,\qquad t=-T,\dots,0,\qquad y_{-T-1}=\Xi,

with $T\ge1$ and $\|\Xi\|\le M$ ; its functional is $H^{A,C,\zeta}_W(z)=y_0$ . For each $k\ge1$ and $j=1,\dots,N^*$ a signed measure $\pi_j^k\ll\pi$ defines the integral map

F_j^{*,N}(x,v)=\int\sigma((x,v,1)\cdot\omega)\,\pi_j^N(d\omega).

The constant $C_*=4\sqrt3L_\sigma\sup_{k}\sum_j(\int\|\omega\|^2(d\pi_j^k/d\pi)^2d\pi)^{1/2}$ measures the size of these densities, and $s_N=\mathbb E[\max_{t\in\{0,\dots,-T\}}\sup_{x\in B_{M+1}}\|F^{*,N}(x,Z_t)-F^*(x,Z_t)\|]$ is the approximation error of $F^{*,N}$ . The input process $Z$ is independent of $(A,C,\zeta)$ , $Y_0$ is an integrable target, and the loss $L\ge0$ is Lipschitz with constant $L_L$ . The echo state event $\Omega_{\mathrm{ESP}}$ of (87) is the event that $\|WF^{A,C,\zeta}(x,Z_t)\|\le M+1$ for all $x\in B_{M+1}$ and $t\in\{0,\dots,-T\}$ , where $F^{A,C,\zeta}(x,v)=\sigma(Ax+Cv+\zeta)$ .

Formalization targets

Steps of the proof

The milestones are the displayed estimates of the proof, in attack order:

(89): one step of the error recursion on $\Omega_{\mathrm{ESP}}$ , $\mathbb E[\|Y_t-X^*_t\|\mathbb 1_{\Omega_{\mathrm{ESP}}}]\le\mathbb E[\sup_{y}\|\cdots\|]+s_N+r\,\mathbb E[\|Y_{t-1}-X^*_{t-1}\|\mathbb 1_{\Omega_{\mathrm{ESP}}}]$ ;
(90): splitting into coordinates and symmetrization of the uniform error of the random map;
(91): a deterministic bound on Rademacher averages,

\mathbb E_\varepsilon\sup_{y\in B_{M+1}}\Big|\sum_{i=1}^N v_i\varepsilon_i\sigma((y,z,1)\cdot u_i)\Big|\le2L_\sigma\Big((M+1)\big(\textstyle\sum_iv_i^2\|a_i\|^2\big)^{1/2}+\|z\|\big(\sum_iv_i^2\|c_i\|^2\big)^{1/2}+\big(\sum_iv_i^2\zeta_i^2\big)^{1/2}\Big);

(92)–(93): for each fixed input $z\in D_d$ ,

\mathbb E\sup_{y\in B_{M+1}}\Big\|\frac1N\sum_{i=1}^NW_i\sigma(A^{(i)}y+C^{(i)}z+\zeta^{(i)})-F^{*,N}(y,z)\Big\|\le\frac{(M+2+\|z\|)C_*}{\sqrt N};

(96): $\mathbb P(\Omega\setminus\Omega_{\mathrm{ESP}})\le2(M+2+\mathbb E[\max_t\|Z_t\|])C_*/\sqrt N+2s_N$ .

Goal: Theorem 4

There is a readout $W$ , a function of $(A,C,\zeta)$ alone, such that for every $\delta\in(0,1)$ and every $\|\Xi\|\le M$ , with probability at least $\max(1-\delta-2C_*(M+2+\mathbb E[\max_t\|Z_t\|])/\sqrt N-2s_N,0)$ , the event $\Omega_{\mathrm{ESP}}$ holds and

|\mathcal R(H^{A,C,\zeta}_W)-\mathcal R(H^*)|\le \frac{L_L}{\delta}\Big[\frac{(M+2+\max_t\mathbb E\|Z_t\|)C_*}{(1-r)\sqrt N}+\frac{s_N}{1-r}+2(M+1)r^{T+1}\Big],

where $\mathcal R(H)=\mathbb E[L(H(Z),Y_0)]$ is evaluated at fixed network weights.

Significance

The bound separates three sources of error: sampling $N$ blocks of random rows (rate $1/\sqrt N$ ), the approximation of $F^*$ by the integral map $F^{*,N}$ ( $s_N$ ), and the finite initialization of the feedback recursion ( $r^{T+1}$ ). Only the readout depends on the target; the internal weights are generated without it. The theorem also bounds the probability that the random feedback map leaves the state ball on which the recursion is controlled, which is the form in which the echo state property enters. Via Theorem 3 (p. 62), which specializes the densities through the paper's Proposition 2, it gives approximation rates for ReLU output-feedback networks.

The paper proves the result on pp. 63–68. No part of it is formalized. A complete development would give machine-checked Rademacher symmetrization and contraction estimates for random features, uniform-over-a-ball bounds for sampled integral maps, and a treatment of finite feedback recursions on product probability spaces, all reusable outside reservoir computing.

Difficulty

A pointwise approximation of $F^*$ by the sampled map does not control the feedback system, because the next feedback value is itself the random output of the previous update. The comparison must hold uniformly over the state ball $B_{M+1}$ and over the whole input window, and the event that the recursion leaves the ball must be charged to an explicit probability. The uniform bound requires symmetrization and the Ledoux–Talagrand contraction principle for a supremum over a continuum of states, with per-index contractions; Lipschitz continuity of $\sigma$ alone does not supply the vanishing at zero that principle needs. The input is unbounded, so the input dependence must be tracked through $\|z\|$ and integrated at the end.

Formalization scope

States, inputs, outputs and rows are Euclidean spaces (EuclideanSpace); a row is indexed by $(\{1..N^*\}\sqcup\{1..d\})\sqcup\{\ast\}$ and the rows by $\{1..N\}\times\{1..N^*\}$ . Time $t\in\mathbb Z_-$ is the index $-t\in\mathbb N$ ; the equation (78) is the published ReservoirESN.IsSolution. The rows have law $\pi^{\otimes NN^*}$ on their own space and $(Z,Y_0)$ lives on a separate probability space; the probability is under the product law, which encodes the independence of §6.1. Signed measures $\pi_j^k$ are their Radon–Nikodym densities with respect to $\pi$ , with integrability and first-moment hypotheses. $C_*$ , $s_N$ and $\mathbb E[\max_t\|Z_t\|]$ are extended nonnegative integrals and suprema, converted to reals only under their finiteness hypotheses; the risk integrals are finite under the loss Lipschitz bound, integrable target and input-moment assumption; the supremum in (87) is unfolded. $F^*$ is assumed jointly measurable, the standing convention that makes $s_N$ and $H^*(Z)$ random variables; the standing assumptions $d,N^*\ge1$ and $M>0$ (p. 30) and $T\ge1$ (§6.1) are hypotheses.

Trivialization ruled out. The readout is a measurable function of the rows only and is chosen before $\delta$ and $\Xi$ . A readout allowed to look at the input $Z$ would make the claim a different and much weaker statement.

Correction of the print. The goal and milestones (91), (93), (96) assume $\sigma(0)=0$ : the contraction principle cited at (91) needs contractions vanishing at zero, while the printed theorem states only that $\sigma$ is Lipschitz. ReLU, the paper's application, satisfies it. The goal retains the printed full risk difference. Its proof passes through (88), where an indicator depending on $Z$ is moved inside a risk integral; this step needs further justification. The milestone quotations keep the printed text.

Contributions are welcome on each milestone, on general Rademacher symmetrization and contraction lemmas for suprema over compact parameter sets, on measurability of suprema of continuous random fields, and on the printed form of the risk bound.

Selected references

L. Gonon, L. Grigoryeva and J.-P. Ortega, Approximation bounds for random neural networks and reservoir systems, The Annals of Applied Probability 33(1), 2023, 28–69. https://doi.org/10.1214/22-AAP1806
M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991 (Theorem 4.12, the contraction principle). https://doi.org/10.1007/978-3-642-20212-4

8 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Cycle Lengths in Expanding Graphs 1: Every α-Expander on n Vertices Has a Cycle of Length in [ℓ, ℓ+O(1/α)] for Every Integer ℓ from O(1/α)·log n up to 2^(−O(log(1/α)/α))·nResearch Paper

Motivation

Which cycle lengths a graph must contain is a long-standing theme of extremal graph theory, studied for graphs of given minimum degree, chromatic number or density. A natural class in which to ask it is that of expanders: graphs in which every not-too-large vertex set has many neighbours outside it (Hoory, Linial and Wigderson). It is known that an $\alpha$ -expander on $n$ vertices has a cycle of length $\Omega_\alpha(n)$ and a cycle of length $O_\alpha(\log n)$ (Krivelevich's survey, Corollary 3.2 and Theorem 7.4, arXiv:1812.11562); the question is what happens between these extremes.

One cannot hope for a full interval of cycle lengths: the complete bipartite graph $K_{\alpha n/2,(1-\alpha/2)n}$ is an $\alpha$ -expander without odd cycles, and subdividing every edge of a bounded-degree expander $m$ times gives an $\Omega(\alpha/m)$ -expander all of whose cycle lengths are divisible by $m+1$ . L. Friedman and M. Krivelevich (Cycle lengths in expanding graphs, Combinatorica 41 (2021); arXiv:1912.11011v2) show that this is the only obstruction: the cycle lengths of an $\alpha$ -expander are well spread, in the sense that every window of $O(1/\alpha)$ consecutive integers between logarithmic and linear length contains one. This mission formalizes that theorem (Theorem 1 of the paper) together with the lemmas of its §2.

Setting

Let $G=(V,E)$ be a finite simple graph on $n$ vertices. For $U\subseteq V$ , the external neighbourhood is $N_G(U)=\{v\in V\setminus U : v\text{ has a neighbour in }U\}$ .

For reals $k>0$ , $\alpha>0$ , $G$ is a $(k,\alpha)$ -expander if $|N_G(U)|\ge\alpha|U|$ for every $U\subseteq V$ with $|U|\le k$ .
$G$ is an $\alpha$ -expander if $|N_G(U)|\ge\alpha|U|$ for every $U$ with $|U|\le\lceil n/2\rceil$ .
A cycle of length $\ell\ge3$ is a closed walk with $\ell$ edges and no repeated vertex; $L(G)$ is the set of lengths of cycles of $G$ .
$B_G(v,r)$ is the ball of radius $r$ : the vertices at distance at most $r$ from $v$ .
For a tree $T\subseteq G$ rooted at $v_0$ , the level of a vertex is one plus its distance from $v_0$ in $T$ , so $L_1=\{v_0\}$ , and $T_{[j_1,j_2]}=\bigcup_{i=j_1}^{j_2}L_i$ .
Contracting the parts $V_1,\dots,V_r$ of a partition of $V$ gives the graph on $\{1,\dots,r\}$ in which $i\ne j$ are adjacent when some edge of $G$ joins $V_i$ and $V_j$ .

All logarithms are base $2$ . In Lean these objects are extNbhd, IsKAlphaExpander, IsAlphaExpander, cycleLengths, ball, contract, level and levelSet, in the namespace CycleLengthsExp.WellSpread.

Formalization targets

Goal: Theorem 1 (p. 3)

For every $0<\alpha\le1$ there are positive constants $A=O(1/\alpha)$ , $a_1=O(1/\alpha)$ and $a_2=2^{-O(\log(1/\alpha)/\alpha)}$ such that for all large $n$ , every $\alpha$ -expander $G$ on $n$ vertices satisfies

\forall\,\ell\in\mathbb Z\cap[a_1\log n,\ a_2n]\quad\exists\,L\in L(G):\ \ell\le L\le\ell+A .

The goal fixes only the shape of the dependence on $\alpha$ , not the constants, so an improvement of the constants does not invalidate it.

Milestones (§2, in the order the proof uses them)

Ball growth (p. 4): in a $(k,\alpha)$ -expander, $|B_G(v,r)|\ge\min\{k,(1+\alpha)^r\}$ .
Lemma 2.1 (p. 4): a component of a $(\delta n,\alpha)$ -expander ( $0<\delta<1$ , $0<\alpha\le1$ ) has diameter at most $\frac7{\delta\alpha}\log n$ .
Lemma 2.2 (p. 5): removing $\epsilon n$ vertices, $0<\epsilon\le\alpha^2k/(8n)$ , from a $(k,\alpha)$ -expander leaves an induced $(k,\alpha/2)$ -expander on $(1-3\epsilon/\alpha)n$ vertices.
Lemma 2.3 (p. 5): an $\alpha$ -expander has $t\alpha/(1+\alpha)$ vertex-disjoint paths between any two sets of size at least $t$ .
Lemma 2.4 (p. 6): contracting parts of size at most $C$ yields a $(k/C,\alpha/C)$ -expander on $r\ge n/C$ vertices.
Lemma 2.5 (p. 6): if every $k$ -set has at least $\ell$ external neighbours, a path of length $\ell$ starts at every vertex whose component has at least $k$ vertices.
Lemma 2.6 (p. 6): a set $W$ with $|W|>n/2$ and $|N_G(W)|\le\alpha\epsilon n$ contains an induced $((\tfrac12-2\epsilon)n,\alpha/2)$ -expander on more than $(\tfrac12-2\epsilon)n$ vertices.
Lemma 2.7 (p. 7): a tree rooted at any $v_0$ with levels $k_0\le C_0\log n$ , $k_1-k_0\le C_1$ , $k_2-k_1\le C_2$ , bounded degree $\Delta$ on $T_{[k_1,k_2]}$ , and an $(n/10,\alpha/5)$ -expander on at least $n/10$ vertices inside $T_{[k_1,k_2]}$ .

Significance

The result. Theorem 1 says that, up to an additive error of order $1/\alpha$ , an $\alpha$ -expander contains every cycle length from $O(\log n/\alpha)$ up to a constant fraction of $n$ . The additive error is optimal in its dependence on $\alpha$ by the subdivision example, and the logarithmic lower end is necessary because expanders can have logarithmic girth. It implies that $|L(G)|$ is linear in $n$ for every $\alpha$ -expander; the companion mission of this series (Theorem 2 of the paper) improves the dependence on $\alpha$ in that count. The lemmas of §2, especially the robust sub-expander lemmas 2.2 and 2.6, the disjoint-paths lemma 2.3 and the depth-first-search lemma 2.5, are general-purpose statements about vertex expanders that do not depend on the cycle-length question.

Formalizing it. The theorem is proved on paper; none of it is machine-checked. Mathlib has walks, paths, cycles, distances and induced subgraphs, but no vertex expansion, no Menger theorem, no depth-first-search path lemma and no breadth-first-tree construction. This mission produces formal statements of all of these at the level of generality the paper uses, and a complete development would supply reusable lemmas about vertex expanders on finite simple graphs.

Difficulty

The obvious argument fails at the step of hitting a prescribed length. Expansion easily gives long paths and long cycles, but controlling the length of a cycle to within an additive $O(1/\alpha)$ requires a structure with many cycles whose lengths differ by small, controlled amounts. The paper builds it from two breadth-first trees joined by many short disjoint paths, a long path routed through bounded-size subtrees, and a pigeonhole selection that avoids spoiling too many subtrees; the explicit constants of Lemma 2.7 then have to be propagated through Theorem 1. Lemma 2.3 additionally needs Menger's theorem, which is not in Mathlib, and Lemma 2.5 is a depth-first-search argument whose formal invariant is not short.

Formalization scope

Graphs are SimpleGraph (Fin n); the ball-growth milestone uses any finite vertex type. Sizes are Set.ncard; inequalities involving $\alpha$ , $\epsilon$ , $\delta$ or logarithms are stated in ℝ. $\lceil n/2\rceil$ is (n + 1) / 2. Logarithms are Real.logb 2.
$O(\cdot)$ constants: one absolute $K>0$ quantified before $\alpha$ . In Theorem 1, $A\le K/\alpha$ , $a_1\le K/\alpha$ , $a_2\ge2^{-K\log_2(2/\alpha)/\alpha}$ ; in Lemma 2.7, $\Delta,C_1\le K/\alpha^5$ and $C_0,C_2\le K/\alpha$ . Inside the $O$ , $\log(1/\alpha)$ is read as $\log_2(2/\alpha)$ , which agrees up to a constant for $\alpha\le1/2$ and avoids the value $0$ at $\alpha=1$ .
Thresholds: Theorem 1's "for large enough $n$ " is $n\ge n_0$ with $n_0$ depending on $\alpha$ only. Lemma 2.7 is also stated for $n\ge n_0(\alpha)$ : an addition, disclosed in the item, because the paper's proof suppresses rounding and needs $n$ large against $1/\alpha$ , and Theorem 1 uses the lemma only for large $n$ .
Induced subgraphs: " $G[U]$ is an expander" and "contains an expander" use G.induce U, the edges of $G$ , never the edges of a tree.
Lemma 2.1 is stated in its "In particular" form, as a bound on G.dist u v for $u,v$ in one component. The first inequality of the lemma is false as printed (the path $P_n$ with $k=1$ ) and is not posed. Lemma 2.7, item 4, is posed with $\alpha/5$ as printed, although its proof gives $\alpha/2$ .
Trivializing readings are ruled out: the $O$ -constants are bounded by one $K$ fixed before $\alpha$ ; cycles are Walk.IsCycle, never closed walks; Lemma 2.1 never uses G.diam, which is $0$ for a disconnected graph; and no statement divides by $\log(1/\alpha)$ .
Welcome contributions: Menger's theorem for vertex sets in finite simple graphs; the depth-first-search long-path lemma; breadth-first trees with level bookkeeping; and proofs of the milestones in any order.

Selected references

L. Friedman, M. Krivelevich, Cycle lengths in expanding graphs, Combinatorica 41 (2021). arXiv:1912.11011v2, doi:10.1007/s00493-020-4434-0
M. Krivelevich, Expanders — how to find them, and what to find in them, Surveys in Combinatorics 2019, LMS Lecture Note Series 456, 115–142. arXiv:1812.11562
S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bulletin of the AMS 43 (2006), 439–561. doi:10.1090/S0273-0979-06-01126-8

10 thms2 active usersReviewed

Algorithmic Game Theory Combinatorics Operations Research+1·Captain: mikedeng1

Online Contention Resolution Schemes with Applications to Bayesian Selection Problems 5: A (b, c)-Selectable Greedy OCRS Rounds x ∈ bP to E[f(S)] ≥ c·F(x) for Monotone Submodular fResearch Paper

Motivation

Many online selection problems ask an algorithm to accept or reject items one at a time, irrevocably, while keeping the accepted set feasible: independent in a matroid, a matching in a graph, or within a knapsack budget. In Bayesian versions, such as prophet inequalities and posted-price mechanisms, a fractional point $x$ of a relaxation of the feasible sets is available in advance, and each item is active independently with probability $x_e$ . An online contention resolution scheme (OCRS), introduced by Feldman, Svensson and Zenklusen, turns this random active set into a feasible selection as items arrive.

The quality of an OCRS is measured by its selectability: the probability that every element is accepted when it is active, whatever the arrival order. Applications, however, care about the value of the selected set, often a submodular function such as a coverage or a utility with diminishing returns. Theorem 1.10 of the paper is the bridge between the two: a selectability guarantee $c$ yields an approximation guarantee $c$ for every monotone submodular objective, and $c/4$ for non-monotone ones, even against an adversary who sees every random outcome before fixing the order. The other four missions of this series construct selectable OCRSs for matroids, matchings and knapsacks and combine them; this mission formalizes what such a guarantee is worth.

The offline counterpart is the theory of contention resolution schemes (CRSs) of Chekuri, Vondrák and Zenklusen (SIAM J. Comput. 2014), whose Theorem 1.3 shows that a monotone balanced CRS rounds the multilinear extension of a submodular function with the balancedness factor. The proof of Theorem 1.10 reduces the online statement to that offline result.

Setting

Let $N$ be a finite ground set and $\mathcal F\subseteq 2^N$ a down-closed family of feasible sets. A polytope $P\subseteq[0,1]^N$ is a relaxation of $\mathcal F$ if it contains exactly the characteristic vectors $\mathbf 1_I$ with $I\in\mathcal F$ among the $\{0,1\}$ -points. For $x\in[0,1]^N$ , the random set $R(x)$ contains every $e$ independently with probability $x_e$ .

A greedy OCRS fixes, for each input $x$ , a down-closed family $\mathcal F_x\subseteq\mathcal F$ containing $\emptyset$ (deterministically, or drawn from a distribution independent of $R(x)$ ). The elements then arrive one by one; an arriving active element is selected if, together with the elements already selected, it forms a set in $\mathcal F_x$ . An element $e$ is selectable for the active set $A$ if $I\cup\{e\}\in\mathcal F_x$ for every $I\subseteq A$ with $I\in\mathcal F_x$ . For $b,c\in[0,1]$ the OCRS is $(b,c)$ -selectable if for every $x\in bP$ and every $e\in N$

\Pr\big[I\cup\{e\}\in\mathcal F_x\ \ \forall I\subseteq R(x),\ I\in\mathcal F_x\big]\ge c .

The arrival order is chosen by the almighty adversary, which knows $R(x)$ , the realized family $\mathcal F_x$ and every random bit of the algorithm before choosing it.

For $f:2^N\to\mathbb R$ , the multilinear extension is $F(x)=\mathbb E[f(R(x))]$ . The function $f$ is submodular if $f(A\cup B)+f(A\cap B)\le f(A)+f(B)$ for all $A,B$ , and monotone if $A\subseteq B$ implies $f(A)\le f(B)$ . For a set $S$ , $S(1/2)$ keeps every element of $S$ independently with probability $1/2$ .

An (offline) CRS $\pi$ for $P$ maps each $S\subseteq N$ , possibly at random, to a subset $\pi(S)\subseteq S$ with $\mathbf 1_{\pi(S)}\in P$ . It is $(b,c)$ -balanced if $\Pr[e\in\pi(R(x))\mid e\in R(x)]\ge c$ for $x\in bP$ and $x_e>0$ , and monotone if $\Pr[e\in\pi(S_1)]\ge\Pr[e\in\pi(S_2)]$ whenever $e\in S_1\subseteq S_2$ . The characteristic CRS of a greedy OCRS is $\bar\pi(A)=\{e\in A : e \text{ selectable for } A\}$ .

Formalization targets

Goal: Theorem 1.10

Let $P$ be a relaxation of $\mathcal F$ , let $\pi$ be a $(b,c)$ -selectable greedy OCRS for $P$ , let $x\in bP$ , and let $f\ge0$ be submodular. Against every almighty adversary, the selected set $S$ satisfies

\mathbb E[f(S)]\ge c\cdot F(x)\quad\text{if } f \text{ is monotone},\qquad \mathbb E[f(S(1/2))]\ge \frac c4\cdot F(x)\quad\text{in general},

where in the second case the coins defining $S(1/2)$ are known to the adversary. The constants are the paper's and are not parameters to be improved here.

Milestones

Observation 3.3: for every greedy family, active set and order, $\bar\pi(A)$ is contained in the selected set.
The remark after Definition 3.2: $\bar\pi$ is a CRS for $P$ .
Lemma 3.4: the characteristic CRS of a $(b,c)$ -selectable greedy OCRS is $(b,c)$ -balanced and monotone.
Lemma 3.5 (from Chekuri–Vondrák–Zenklusen): for every non-negative submodular $f$ there is a pruning map $\eta_f$ , with $\eta_f(S)\subseteq S$ , such that $\mathbb E[f(\eta_f(\pi(R(x))))]\ge c\cdot F(x)$ for every monotone $(b,c)$ -balanced CRS $\pi$ and every $x\in bP$ .
Lemma 3.6 (Feige–Mirrokni–Vondrák, Lemma 2.2): if $T_p\subseteq T$ contains every element of $T$ with probability $p$ , not necessarily independently, then $\mathbb E[g(T_p)]\ge(1-p)g(\emptyset)+p\,g(T)$ for submodular $g$ .
Lemma 3.7 (Buchbinder–Feldman–Naor–Schwartz, Lemma 2.2): if $N_p$ contains every element with probability at most $p$ , then $\mathbb E[g(N_p)]\ge(1-p)g(\emptyset)$ for non-negative submodular $g$ .

Significance

Theorem 1.10 is what makes selectability useful. Combined with the paper's OCRSs for matroids, matchings and knapsacks (Theorem 1.8) and the combination rule (Theorem 1.9), it gives constant-factor online algorithms for submodular objectives under intersections of these constraints, and through them the paper's applications to prophet inequalities, posted-price mechanisms and stochastic probing. The guarantee holds against the strongest adversary considered, so it applies whatever arrival order the application imposes.

The theorem and its proof are published; none of the statements of this mission has a machine-checked proof. Formalizing it produces a reusable interface between online and offline contention resolution, and machine-checked versions of two standard lemmas on correlated random subsets of submodular functions (Lemmas 3.6 and 3.7) used throughout submodular maximization. Lemma 3.5 is the substantial imported ingredient: its formal proof amounts to formalizing the rounding theorem of Chekuri, Vondrák and Zenklusen for non-monotone objectives.

Difficulty

The first idea is to compare the online selection directly with $F(x)$ element by element: each element is selected with probability at least $c\,x_e$ . For a linear objective this suffices. For a submodular objective it does not, because the marginal value of an element depends on which other elements are selected, and the adversary controls this through the order. The reduction to the characteristic CRS removes the order, but the offline rounding result (Lemma 3.5) then needs the full CRS machinery, including a pruning step that depends on $f$ alone.

For non-monotone $f$ , selecting extra elements can lose value, and the adversary decides which elements beyond $\bar\pi(A)$ are selected, after seeing the coins. Controlling this requires the correlated-sampling bounds of Lemmas 3.6 and 3.7 rather than independence.

Formalization scope

The ground set is a finite type α : Type with decidable equality; sets are Finset α; vectors are α → ℝ. All probabilities and expectations are exact finite sums of product weights, without measure theory. $bP$ is the pointwise scaling b • P, which handles $b=0$ . The multilinear extension and submodularity are the published definitions NonmonotoneSubmod.Shared.F and NonmonotoneSubmod.Shared.Submodular.

A randomized greedy OCRS is a weight function on families Finset (Finset α), a CRS a weight function on maps Finset α → Finset α; a deterministic OCRS is a point mass. The almighty adversary is any function from the realized family and active set (and, in part 2, the coin set $C$ , with $S(1/2)=S\cap C$ and $C$ uniform and independent of everything else) to an order listing every element once. The standing assumptions of Definition 1.3 are explicit hypotheses: $\mathcal F$ down-closed, $P$ a polytope contained in $[0,1]^N$ and a relaxation of $\mathcal F$ , and $b,c\in[0,1]$ . A polytope is encoded as the convex hull of finitely many vectors. Every greedy family contains $\emptyset$ , so the empty family cannot make every element vacuously selectable, and the inputs $x\in bP$ lie in $[0,1]^N$ , so the product weights are probabilities.

Definition 3.1 is printed with " $\ge c\cdot x_e$ "; the formalization uses " $\ge c$ ", as the proof of Lemma 3.4 and Definition 4.5 do. Lemma 3.5 keeps the paper's quantifier order: $\eta_f$ is fixed before $P$ , $b$ , $c$ , $\pi$ and $x$ .

Welcome contributions: proofs of the milestones in any order; Lemmas 3.6 and 3.7 are self-contained and reusable; Lemma 3.5 may be split further along the proof of Chekuri–Vondrák–Zenklusen.

Selected references

M. Feldman, O. Svensson, R. Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015; Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM J. Comput. 50(2), 2021. https://arxiv.org/abs/1508.00142v2
C. Chekuri, J. Vondrák, R. Zenklusen, Submodular Function Maximization via the Multilinear Relaxation and Contention Resolution Schemes, SIAM J. Comput. 43(6), 2014. https://doi.org/10.1137/110839655
U. Feige, V. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4), 2011. https://doi.org/10.1137/090779346
N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, Submodular Maximization with Cardinality Constraints, SODA 2014. https://doi.org/10.1137/1.9781611973402.106

12 thms2 active usersReviewed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Online Contention Resolution Schemes with Applications to Bayesian Selection Problems 3: A Knapsack Polytope Has a (b, (1−2b)/(2−2b))-Selectable Randomized Greedy OCRS for b ≤ 1/2Research Paper

Motivation

In online selection, useful items arrive one at a time and must be accepted or rejected before the next arrival. A knapsack constraint limits the total size of accepted items to one unit. When the order may depend on all of the random outcomes, an algorithm needs a guarantee that survives every such order. Feldman, Svensson, and Zenklusen introduced online contention resolution schemes (OCRSs) to provide this guarantee for fractional relaxations of selection problems. Their knapsack theorem gives an explicit guarantee for a randomized greedy scheme and contrasts with a size-dependent obstruction for deterministic greedy schemes (Feldman–Svensson–Zenklusen, §2.3).

The knapsack result is one of the three concrete existence results summarized in Theorem 1.8 of the paper. The surrounding framework is designed to convert fractional solutions into feasible online selections under an almighty adversary, who knows the active items and the scheme's random choices before choosing their arrival order. This makes the selectability requirement stronger than a performance claim for one fixed order (Feldman–Svensson–Zenklusen, Definitions 1.3–1.5).

Setting

Let $N$ be a finite ground set. Each element $e\in N$ has a size $s_e\in[0,1]$ . A subset $I\subseteq N$ is feasible when its total size is at most one. The natural fractional polytope is

P=\left\{x\in[0,1]^N:\sum_{e\in N}s_ex_e\le1\right\}.

For a vector $x\in[0,1]^N$ , the random active set $R(x)$ includes each element $e$ independently with probability $x_e$ . A greedy family $F_x$ is a downward-closed family of feasible subsets. The online rule accepts an active arriving element when adding it to the accepted set keeps that set inside $F_x$ . A randomized greedy OCRS chooses the family at random, independently of $R(x)$ . The paper studies the probability that an element $e$ is selectable: for every possible accepted set $I\subseteq R(x)$ with $I\in F_x$ , the enlarged set $I\cup\{e\}$ still belongs to $F_x$ . Such an event makes $e$ acceptable regardless of the arrival order (Feldman–Svensson–Zenklusen, §1.1).

Write $bP=\{bp:p\in P\}$ . An OCRS is $(b,c)$ -selectable when, for every $x\in bP$ and every $e\in N$ , the probability that $e$ is selectable is at least $c$ . The paper divides elements at size $1/2$ : $N_{\mathrm{big}}=\{e:s_e>1/2\}$ , while equality belongs to the small elements. Its construction randomly chooses between the feasible subsets using only big elements and those using only small elements (Feldman–Svensson–Zenklusen, proof of Theorem 2.9).

Formalization targets

Main theorem

Theorem 2.9 asserts that for every $b\in[0,1/2]$ and every such knapsack polytope, a randomized greedy OCRS exists with

c=\frac{1-2b}{2-2b}.

The goal quantifies over every finite ground set and every allowed size vector. At the endpoint $b=1/2$ , the claimed lower bound is zero; at $b=0$ , it is $1/2$ . The denominator remains positive throughout the stated interval. The goal is an existence statement; its witnesses are arbitrary randomized greedy families meeting the definition, so the paper's particular construction is named separately in the supporting definitions (Feldman–Svensson–Zenklusen, Theorem 2.9, p. 14).

Supporting targets

The milestones include the paper's bound $0\le b_{\mathrm{big}}\le b$ for $b_{\mathrm{big}}=\sum_{e\in N_{\mathrm{big}}}s_ex_e$ , the big and small element selectability bounds for the paper's construction, and Proposition 2.8. That proposition says that, for every ground-set size $n\ge1$ , some knapsack constraint defeats every deterministic greedy OCRS whenever $c>(1-b)^{n-1}$ for $b\in[0,1]$ (Feldman–Svensson–Zenklusen, §2.3, pp. 14–15).

Significance

The theorem supplies a concrete selectable OCRS for the natural fractional knapsack relaxation. Its guarantee applies to every element and every fractional point in $bP$ , under the paper's strongest arrival-order adversary. Proposition 2.8 explains why randomization matters here: a deterministic greedy scheme cannot retain an analogous positive constant independent of the number of elements on every knapsack instance. These results serve as the knapsack component in the paper's broader OCRS framework and can be combined with schemes for other constraints in the paper's later combination result (Feldman–Svensson–Zenklusen, Theorem 1.9).

The mathematical theorem and proposition have proofs in the cited paper. This mission asks for machine-checked proofs of their formal statements and of the stated intermediate bounds. The current draft declarations contain proof placeholders; compilation establishes only that their statements and definitions are well formed. A completed development would also leave reusable finite active-set probabilities, greedy-family predicates, and explicit knapsack constructions for later online-rounding work.

Difficulty

A family that contains every feasible subset is not automatically useful for online selection: one active set may contain several subsets whose accepted elements block the tested element. The requirement quantifies over every feasible accepted subset of the realized active set, reflecting the almighty adversary rather than a fixed order. In a knapsack, elements larger than one half behave differently from smaller ones, and a single deterministic family cannot give a ground-set-independent selectability guarantee on all instances. The randomized construction must assign valid probabilities to its two families and obtain the same lower bound in both size regimes (Feldman–Svensson–Zenklusen, Proposition 2.8 and Theorem 2.9).

Formalization scope

The Lean ground set is a finite type, and subsets are Finsets. The polytope is the set of real vectors satisfying both the box inequalities and the unit-capacity inequality. The feasible family uses the same sizes and unit capacity. Active-set and family-choice probabilities are finite sums, with independent Bernoulli factors for $R(x)$ . The scaling $bP$ is pointwise set scalar multiplication, so the case $b=0$ retains its intended meaning. The size assumptions $s_e\in[0,1]$ and the ranges of $b$ are explicit theorem hypotheses. No nonemptiness assumption is added to the ground set; the statements include the empty case.

The greedy-family definition requires the empty set, making it impossible to satisfy selectability by using an empty family. Every family chosen with positive probability is downward closed and consists of feasible sets. The polytope's box constraints keep every active-set weight a probability. The construction's mixing probability is used exactly on $x\in bP$ ; on other vectors its totalized value chooses the small family, where the paper makes no performance claim. The two branch weights are added if their families coincide, as they can on an empty ground set.

One display on page 15 includes the tested element in a load sum, while the next displayed equality treats that element as excluded. The pointwise supporting item uses the excluded-element form needed for the stated argument; the printed display is preserved in the milestone quotation and the discrepancy is detailed in MODERATION_NOTES.md. Contributions toward either size regime, the finite probability bounds, or the deterministic obstruction are welcome. The finite probability and greedy-family definitions are the parts most directly reusable beyond knapsack.

Selected references

Moran Feldman, Ola Svensson, and Rico Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015, §1.1 and §2.3, pp. 2–4 and 14–15. arXiv.

8 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Exact Solution of the Hypergraph Turán Problem for k-Uniform Linear Paths: For k ≥ 4 and Large n, the Turán Numbers of P_{2t+1} and P_{2t+2} and Their Unique Extremal FamiliesResearch Paper

Motivation

Hypergraph Turán problems ask how many edges a $k$ -uniform hypergraph on $n$ vertices can have without containing a fixed sub-hypergraph. For graphs ( $k=2$ ) the theory is well developed; for $k\ge 3$ exact answers are rare and are known mostly for small, dense configurations such as the Fano plane or expanded triangles. Paths are the natural sparse test case. For graphs, Erdős and Gallai (1959) showed that a graph on $n$ vertices without a path of length $\ell$ has at most $\frac12(\ell-1)n$ edges. For hypergraphs there are several notions of path: Berge paths (Győri, Katona and Lemons, 2010), loose paths (Mubayi and Verstraëte, 2007, asymptotic bounds) and the most restrictive notion, linear paths. The case of two edges was solved by Frankl (1977), and the case $\ell<k$ asymptotically by Frankl and Füredi (1987).

Füredi, Jiang and Seiver (arXiv:1108.1247v1, published in Combinatorica 34 (2014), doi:10.1007/s00493-014-2838-4) determined the Turán number of every $k$ -uniform linear path exactly, for $k\ge4$ and $n$ large, together with the unique extremal families. It is one of the few exact hypergraph Turán results for an infinite family of forbidden hypergraphs.

Setting

The vertex set is $[n]=\{1,\dots,n\}$ . A family $\mathcal F$ is a set of subsets of $[n]$ ; it is $k$ -uniform if $\mathcal F\subseteq\binom{[n]}{k}$ , the set of all $k$ -element subsets.

A linear path of length $\ell$ is a sequence of distinct sets $F_1,\dots,F_\ell$ such that

|F_i\cap F_{i+1}|=1\ \text{ for each } i,\qquad F_i\cap F_j=\emptyset\ \text{ whenever } |i-j|>1.

The $k$ -uniform linear path of length $\ell$ is written $\mathbb P^{(k)}_\ell$ ; a family contains it if some $\ell$ of its members form a linear path. The Turán number $\mathbf{ex}_k(n,\mathbb P^{(k)}_\ell)$ is the maximum size of a $k$ -uniform family on $[n]$ that does not contain $\mathbb P^{(k)}_\ell$ .

Two counting functions describe the answer:

f(n,k,t)=\sum_{i=1}^{t}\binom{n-i}{k-1},\qquad g(n,k,t)=f(n,k,t)+\binom{n-t-2}{k-2}.

For a set $S\subseteq[n]$ of $t$ elements, $f(n,k,t)$ is the number of $k$ -sets meeting $S$ (the star family of $S$ ), and $g(n,k,t)$ adds the $k$ -sets of $[n]\setminus S$ that contain two fixed vertices $u,v$ (the even family).

The proof is phrased in the language of the delta-system method: $s$ -stars (sets pairwise meeting in a common kernel), the kernel degree $\deg^*_{\mathcal F}(W)$ (the largest $s$ for which an $s$ -star with kernel $W$ exists), $(k,s)$ -homogeneous families (k-partite families whose intersections follow a single intersection-closed pattern $\mathcal J$ of subsets of $[k]$ , each intersection being the kernel of an $s$ -star), the rank of $\mathcal J$ , the kernel graph of $\mathcal F$ , and the $k$ -blowup $H^{(k)}$ of a graph $H$ .

Formalization targets

Goal: Theorem 2.4

For every $k\ge 4$ and $t\ge1$ there is $n_0$ such that for all $n\ge n_0$ :

\mathbf{ex}_k(n,\mathbb P^{(k)}_{2t+1})=f(n,k,t),\qquad \mathbf{ex}_k(n,\mathbb P^{(k)}_{2t+2})=g(n,k,t),

and in each case a $k$ -uniform, path-free family of that size is exactly the star family of some $t$ -set $S$ (odd case), respectively the even family of some $t$ -set $S$ and two distinct vertices $u,v\notin S$ (even case).

Milestones

In the order the proof uses them:

the star and even families are path-free and have $f$ and $g$ members (lower bound);
Lemma 3.1, Füredi's intersection semilattice lemma;
Lemma 3.3 and Proposition 3.4, the rank bound $|\mathcal F^*|\le\binom np$ ;
Lemma 3.6 and Corollary 3.7, the structure of patterns of rank $k$ and $k-1$ ;
Theorem 3.8, blowups of trees in homogeneous families of rank $k$ or type 2;
Theorem 3.9, the canonical partition of a path-free family;
Lemmas 4.2–4.4, from kernel graphs to blowups, the edge count $(k-1)|\mathcal F|\le e(H')\binom{n-2}{k-2}$ , and the Erdős–Gallai circumference bound;
Theorem 4.5, $\mathbf{ex}_k(n,\mathbb P_{2t+2}^{(k)})\le t\binom{n-1}{k-1}+O(n^{k-2})$ ;
the bound (1), $\mathbf{ex}_k(n,\mathbb P^{(k)}_\ell)\le(k-1)(\ell-1)\binom{n-1}{k-1}$ for every $n$ ;
Erdős' matching theorem for large $n$ (Theorem 1.1) and the $r$ -intersecting Erdős–Ko–Rado theorem;
Claims 2–3 of §5: a near-extremal family has a $t$ -set joined in the kernel graph to all but $O(\sqrt n)$ vertices.

Significance

The theorem gives the exact extremal number and the unique extremal configuration for every linear path when $k\ge4$ , and its proof yields a stability statement (Theorem 5.1 of the paper): a path-free family of nearly extremal size is close to a star family. The method is the standard template for exact results on sparse hypergraphs: delta-system decomposition, an asymptotic bound from a graph theorem applied to a kernel graph, then stability and cleaning.

The result is proved in the paper. As far as the platform's catalog shows, none of it is formalized: Mathlib has the intersecting Erdős–Ko–Rado theorem ( $r=1$ ) but not the $r$ -intersecting version with uniqueness for large $n$ , not Erdős' matching theorem, not the Erdős–Gallai circumference theorem, and no delta-system machinery. A formalization would produce reusable libraries for each of these, and the first machine-checked exact hypergraph Turán number for an infinite family.

Difficulty

The obvious argument — bound the number of members through each vertex and sum — gives only $O(n^{k-1})$ with a wrong leading constant, because a path-free family can have $t$ vertices of almost full degree. Exactness needs three layers that do not reduce to one another. First, the intersection semilattice lemma (Lemma 3.1) is a deep structural theorem with a doubly exponential constant; it is cited, not proved, in the paper. Second, the asymptotic bound passes through the Erdős–Gallai circumference theorem, itself a nontrivial graph result. Third, the exact value requires a stability argument with several error terms ( $O(n^{k-3/2})$ , $O(\sqrt n)$ ) that must be balanced, followed by Erdős' matching theorem and the 2-intersecting Erdős–Ko–Rado theorem for large $n$ , both with uniqueness. The structural lemmas of §§3–4 are elementary but involve greedy embeddings in which disjointness of the new vertices has to be maintained carefully.

Formalization scope

Vertices are Fin n; families are Finset (Finset (Fin n)); $k$ -uniformity is 𝓕 ⊆ univ.powersetCard k. A linear path is an injective map Fin ℓ → Finset (Fin n) into the family with consecutive members meeting in exactly one vertex and non-consecutive members disjoint. The Turán number is a Finset.sup of cardinalities over all path-free $k$ -uniform subfamilies, a finite attained maximum for $\ell\ge1$ ; at $\ell=0$ the feasible set is empty and Lean returns zero, which no theorem here uses. Partitions into $k$ parts are part maps Fin n → Fin k; stars are finsets of distinct petals; the rank is a minimum computed with sInf, exact because intersection patterns consist of proper subsets of $[k]$ . "Sufficiently large $n$ " and every $O(\cdot)$ are explicit existential constants chosen before $n$ and the family.

Hypotheses added relative to the page: Theorem 3.8 assumes the homogeneous family is nonempty (the empty family is homogeneous for every pattern, and the proof starts from a member). Lemma 4.2 states $k\ge2$ , implicit in the paper's definition of a blowup using $k-2$ new vertices; it excludes a false zero-threshold case at $k=0$ . Lemma 4.3 is stated for an arbitrary choice of a vertex $c(F)\in F$ in each member, a generalization of the printed lemma, whose proof uses only $c(F)\in F$ . Bound (1) is posed for $k\ge2$ . Claims 2–3 are stated stand-alone with the $t$ -set $S$ existentially quantified.

Trivializing formalizations are ruled out: the goal asserts the value and the uniqueness of the extremal family, the Turán number is a true maximum rather than a junk supremum, the linear path requires intersections of size exactly one and disjointness of non-consecutive members, and all constants are quantified before $n$ .

Needed infrastructure: the delta-system method (Lemma 3.1), Erdős–Gallai for circumference, Erdős' matching theorem and $r$ -intersecting Erdős–Ko–Rado for large $n$ . Each is reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

Z. Füredi, T. Jiang, R. Seiver, Exact solution of the hypergraph Turán problem for k-uniform linear paths, Combinatorica 34 (2014). arXiv:1108.1247, doi:10.1007/s00493-014-2838-4
Z. Füredi, On finite set-systems whose every intersection is a kernel of a star, Discrete Math. 47 (1983) 129–132. doi:10.1016/0012-365X(83)90081-X
P. Erdős, T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959) 337–356. doi:10.1007/BF02024498
P. Erdős, A problem on independent r-tuples, Ann. Univ. Sci. Budapest. Eötvös Sect. Math. 8 (1965) 93–95.
P. Erdős, C. Ko, R. Rado, Intersection theorems for systems of finite sets, Quart. J. Math. Oxford 12 (1961) 313–320. doi:10.1093/qmath/12.1.313
P. Frankl, Z. Füredi, Exact solution of some Turán-type problems, J. Combin. Theory Ser. A 45 (1987) 226–262. doi:10.1016/0097-3165(87)90016-7
D. Mubayi, J. Verstraëte, Minimal paths and cycles in set systems, European J. Combin. 28 (2007) 1681–1693. doi:10.1016/j.ejc.2006.07.008

19 thms2 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Isotropic Gaussian Random Fields on the Sphere: Regularity, Fast Simulation and Stochastic Partial Differential Equations I: u ∈ V^η(−1,1) iff Σ u_ℓ²(2ℓ+1)(1+ℓ^{2η}) < ∞Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.1 (p. 11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Modern Introduction to Online Learning IX: Cover's Universal Portfolio with Uniform or Dirichlet(1/2) Prior Has Logarithmic Regret Against Constantly Rebalanced PortfoliosTextbook

Why sequential portfolios matter

Market and strategy

Formalization targets

What the result provides

Main difficulty

Formalization scope

Selected references

Connes–Weil arithmetic lower bound: cofinal actual-quartet certificatesOpen Problem

Why an arithmetic lower bound is needed

Actual zeros and the fixed physical carrier

Formalization target

What this target would establish

The remaining difficulty

Formalization scope

Selected references

Literature and source audit

High Order Random Walks: Beyond Spectral Gap 1: On a One-Sided λ-Local Spectral Expander, ‖M⁺_k φ‖ ≤ ((k+1)/(k+2) + (k+1)λ/2)‖φ‖ for Every k-Cochain φ Orthogonal to the ConstantsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.4 (p. 17)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Two WordRAM models: equivalence with polylogarithmic overheadTextbook

References:

Quantum Algorithm for Simulating Real Time Evolution of Lattice Hamiltonians 2: Strictly Local Lieb–Robinson Bound ‖[A_X(t),B_Y]‖ ≤ 2‖A‖‖B‖|X|(2ζ₀|t|)^ℓ/ℓ! with ℓ = ⌊dist(X,Y)⌋Research Paper

Motivation

Setting

Formalization targets

Goal: display (48)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Model-Based Minimization of Weakly Convex Functions 2: The Proximal Stochastic Subgradient Method Drives E‖∇φ_{1/ρ̄}(x_{t*})‖² to Zero at Rate O(1/√T)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.4, (3.15) and (3.16)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Greed Works – Online Algorithms For Unrelated Machine Stochastic Scheduling 2: Greedy Assignment With Nominal Start Times Is (7.216 + 3.608Δ)h(Δ)-Competitive in the Online-Time ModelResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Uniform Wasserstein contraction