All missions

Motivation

Many graph-colouring questions ask whether a proper colouring can be produced indirectly, from local data, instead of being assigned vertex by vertex. In the 1-2-3 Conjecture, the colours are produced by weighting the edges of a graph and colouring each vertex with the sum of the weights at it. Karoński, Łuczak and Thomason asked in 2004 whether weights from $\{1,2,3\}$ always suffice (J. Combin. Theory Ser. B 91 (2004)). The question started as a local version of the irregularity strength problem, where all vertices, not only adjacent ones, must receive different sums. It became one of the most studied problems on graph labellings. Surveys: Seamone (arXiv:1211.5122) and Grytczuk (DOI 10.1016/j.ejc.2020.103213).

Timeline.

• 2004: Karoński, Łuczak, Thomason state the conjecture and prove it for 3-colourable graphs.
• 2007: Addario-Berry, Dalal, McDiarmid, Reed and Thomason give the first finite bound, $k=30$; later $k=16$ (Addario-Berry et al.) and $k=13$ (Wang and Yu).
• 2010: Kalkowski, Karoński and Pfender reach $k=5$ (J. Combin. Theory Ser. B 100 (2010)).
• Before 2023: Przybyło proves the conjecture for $d$-regular graphs with $d\ge 10^8$ and for graphs with minimum degree $\delta(G)\ge C\log\Delta(G)$; Zhong proves it for graphs with minimum degree at least $0.99985|V|$ (references [20], [21], [31] of the paper).
• 2023: Keusch reaches $k=4$ with a maximum-cut and flow argument (Combinatorica 43 (2023), 651–658; reference [18] of the paper).
• 2024: Keusch proves the conjecture, $k=3$ (J. Combin. Theory Ser. B (2024), arXiv:2303.02611).

Setting

Let $G=(V,E)$ be a finite simple graph and write $N(v)$ for the neighbourhood of a vertex $v$. A $k$-edge-weighting is a function $\omega:E\to\{1,\dots,k\}$. The weighted degree of $v$ is

$$s_\omega(v)=\sum_{w\in N(v)}\omega(\{v,w\}).$$

Two adjacent vertices $v,w$ have a coloring conflict if $s_\omega(v)=s_\omega(w)$. The weighting is vertex-coloring if no edge is a coloring conflict, that is, if $s_\omega$ is a proper vertex colouring of $G$.

If $G$ has a connected component consisting of a single edge $\{v,w\}$ (a component isomorphic to $K_2$), then $s_\omega(v)=s_\omega(w)=\omega(\{v,w\})$ for every $\omega$, so no weighting is vertex-coloring. This is the only obstruction.

The proof uses a few further objects:

• for $W\subseteq V$, $\deg_W(v)=|N(v)\cap W|$;
• for disjoint $S,T\subseteq V$, the bipartite subgraph $G(S,T)$ with vertex set $S\cup T$ and the edges of $G$ between $S$ and $T$;
• a good R-B-partition (Definition 6): a partition $V=R\cup B$ with $R$ independent, $G(R,B)$ connected and $|B|$ even;
• a maximum cut $C=(S,T)$ and an auxiliary unit-capacity flow network $G_{C,F,\sigma}$ built from it (Lemma 4).

The Lean names are wdeg G ω v for $s_\omega(v)$, IsWeighting G k ω, IsVertexColoring G ω, NoK2Component G and IsGoodPartition G U R B.

Formalization targets

Goal: Theorem 1 (p. 2)

If no connected component of $G$ is isomorphic to $K_2$, then there is $\omega:E\to\{1,2,3\}$ with

$$\sum_{u\in N(v)}\omega(\{u,v\})\ne\sum_{u\in N(w)}\omega(\{u,w\})\qquad\text{for every edge }\{v,w\}\in E.$$

The connected case (p. 14)

Every finite connected graph with $|V|\ge 3$ has a vertex-coloring $\{1,2,3\}$-edge-weighting. This is the statement the case analysis of the proof establishes. Theorem 1 follows by treating each component separately.

Milestones along the proof

In the order the proof uses them:

• Lemma 2: an independent set $R$ with $G(R,V\setminus R)$ connected, alternating along a shortest path.
• Lemma 4: a flow of value $|F|$ in $G_{C,F,\sigma}$.
• Lemma 3: a weighting and odd designated colours $f$, proper on $G$, with $|s_\omega+h-f|=1$.
• Lemma 5: a bipartite weighting with prescribed parities on $R$ and exact weighted degrees on $B$, plus a second version with extra control along a fixed path.
• Lemmas 7, 8 and 9: the three basic situations in which a good R-B-partition of $G$, or of $G$ minus one vertex, yields a vertex-coloring weighting.
• Lemma 10: every connected graph of minimum degree at least $2$ has an edge whose removal, together with its two ends, leaves a connected graph.

Significance

The result. Theorem 1 settles a conjecture that was open for nineteen years. The constant is optimal: the triangle $K_3$ has no vertex-coloring $\{1,2\}$-weighting (two of its three edges get the same weight, and then two vertices tie), and deciding whether a vertex-coloring $\{1,2\}$-weighting exists is NP-complete (Dudek and Wajc, 2011). Theorem 1 also closes the sequence of upper bounds $30,16,13,6,5,4$ on the number of weights needed. Variants remain open: total weightings with vertex weights $\{1,2\}$ and edge weights $\{1,2\}$ (the 1-2 Conjecture), and list versions.

Formalizing it. The theorem is proved, in a 16-page paper. As far as is known it has no machine-checked proof. A formal proof would verify the case analysis at the end of the paper (pp. 11–14, about fifteen sub-cases with three auxiliary graphs), which is where errors in such arguments usually hide. The flow lemma is quoted from the 2023 paper and not reproved here. Formalizing it means proving an integral max-flow statement for a specific unit-capacity network, and the result can be reused for other flow-based weighting arguments.

Difficulty

The obvious approach is to fix the weights greedily, edge by edge or vertex by vertex. This fails because changing one edge weight changes two weighted degrees at once, so a repair at one vertex can create a conflict at a neighbour. With only three weights there is no room to absorb this. Every earlier bound above $3$ used the extra weight as slack.

The difficulty in the paper is parity. The construction needs the set $B$ of blue vertices to have even cardinality, and $|B|$ cannot always be made even. The proof therefore removes one or two vertices, applies one of three base lemmas, and re-inserts the vertices. That re-insertion may need one more round of weight changes along a path. Each sub-case has to keep track of parities, of exact weighted degrees on $B$, and of the connectivity of $G(R,B)$ simultaneously.

Formalization scope

Representation.

• Graphs are SimpleGraph V on a finite vertex type V with decidable adjacency. The paper's "graph" is a finite simple graph: weighted degrees are finite sums, and the proof uses a maximum cut and vertex orderings.
• An edge-weighting is a function ω : Sym2 V → ℕ on unordered pairs. IsWeighting G k ω requires $\omega(e)\in\{1,\dots,k\}$ for every edge $e$ of $G$; values on non-edges are unconstrained and never used.
• The weighted degree sums over G.neighborFinset v. Since $\{u,v\}=\{v,u\}$ in Sym2, the single sum equals both sides of Theorem 1's displayed inequality.
• "No component isomorphic to $K_2$" uses Mathlib's connected components and graph isomorphism. A sanity file proves it equivalent to "no edge both of whose ends have degree 1".
• $G(R,B)$ is Mathlib's G.between R B, induced on $R\cup B$ wherever that vertex set is not all of $V$.

Conventions that differ from the page. There are two, both disclosed in the item statements:

1. The vertex type is finite.
2. The flow of Lemma 4 is integral. The page says "an $s$-$t$-flow"; the paper uses integrality immediately afterwards, and the two versions are equivalent by the integrality theorem.

Lemma 5's condition $\alpha(v)\in\{2\deg(v)-1,2\deg(v),2\deg(v)+1\}$ is stated in $\mathbb Z$, and Lemma 3's $|s_\omega+h-f|=1$ is computed in $\mathbb Z$.

Ruled out. None of the following formalizations is faithful:

• weights allowed to be $0$, which deletes edges;
• weights constrained off the edges;
• the $K_2$ hypothesis strengthened to minimum degree at least $2$, or to connectivity;
• "adjacent vertices" replaced by "all pairs of vertices", which is the irregularity-strength problem.

Infrastructure. A complete development needs:

• spanning trees and parity arguments on trees (Lemma 5);
• depth-first search trees (Lemma 10);
• maximum cuts and an integral max-flow or augmenting-path argument for $G_{C,F,\sigma}$ (Lemma 4), together with path decompositions of unit flows (the proof of Lemma 3).

The flow and cut definitions are stated for arbitrary finite graphs and can be reused. Contributions are welcome at every level: proofs of individual lemmas, general flow-decomposition results, and the final case analysis.

Selected references

• R. Keusch, A Solution to the 1-2-3 Conjecture, J. Combin. Theory Ser. B, 2024. arXiv:2303.02611v4, DOI 10.1016/j.jctb.2024.01.002
• R. Keusch, Vertex-coloring graphs with 4-edge-weightings, Combinatorica 43 (2023), 651–658. Cited as [18] in arXiv:2303.02611v4.
• M. Karoński, T. Łuczak, A. Thomason, Edge weights and vertex colours, J. Combin. Theory Ser. B 91 (2004), 151–157. DOI 10.1016/j.jctb.2003.12.001
• M. Kalkowski, M. Karoński, F. Pfender, Vertex-coloring edge-weightings: towards the 1-2-3-conjecture, J. Combin. Theory Ser. B 100 (2010). DOI 10.1016/j.jctb.2009.06.002
• A. Dudek, D. Wajc, On the complexity of vertex-coloring edge-weightings, Discrete Math. Theor. Comput. Sci. 13 (2011), 45–50. Cited as [11] in arXiv:2303.02611v4.
• B. Seamone, The 1-2-3 Conjecture and related problems: a survey, 2012. arXiv:1211.5122
• J. Grytczuk, From the 1-2-3 Conjecture to the Riemann Hypothesis, European J. Combin. 91 (2021), 103213. DOI 10.1016/j.ejc.2020.103213

Motivation

In a stochastic multi-armed bandit, a player repeatedly chooses one of $K$ arms and receives a random reward drawn from the chosen arm's unknown distribution. The classical lower bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) describe the regret of good strategies when the horizon $T$ tends to infinity: it grows like $\ln T$, with a constant determined by Kullback–Leibler divergences. They say nothing about small horizons.

Garivier, Ménard and Stoltz (Math. Oper. Res., 2019; arXiv:1602.07182v3) show that the regret has a definite shape over the whole range of $T$: it is almost linear at first ("explore first"), and only afterwards logarithmic ("exploit next"). Their §3 gives three non-asymptotic lower bounds for the initial phase, each for a natural class of strategies. This mission is the third of them, Theorem 4 (p. 13): a collective lower bound on the total number of pulls of all suboptimal arms. It is the bound that remains informative when many arms are suboptimal, and it is the one illustrated for large $K$ in the paper's §3.4.

Setting

A bandit problem $\underline\nu=(\nu_a)_{a=1,\dots,K}$ is a family of probability distributions on $\mathbb R$, each with an expectation $\mu_a=E(\nu_a)$. A model $\mathcal D$ is a set of such distributions, and $\underline\nu$ is in $\mathcal D$ when every $\nu_a\in\mathcal D$. Put $\mu^\star=\max_a\mu_a$.

At each round $t\ge1$ a strategy $\psi$ chooses an arm $A_t$ from the past rewards (possibly with auxiliary randomization) and observes a reward $Y_t\sim\nu_{A_t}$. The number of pulls of arm $a$ up to round $T$ is $N_{\psi,a}(T)=\sum_{t=1}^T\mathbb 1\{A_t=a\}$, and $\mathbb E_{\underline\nu}$ is the expectation when $\psi$ interacts with $\underline\nu$.

The set of optimal arms is $\mathcal A^\star(\underline\nu)=\{a:\mu_a=\mu^\star\}$, of cardinality $A^\star_{\underline\nu}$, and the set of worst arms is $\mathcal W(\underline\nu)$, the arms of smallest mean. The paper defines a partial order: $\underline\nu'\preccurlyeq\underline\nu$ when $\nu'_a=\nu_a$ for every optimal arm $a$ of $\underline\nu$ and $E(\nu'_a)\le E(\nu_a)$ for every other arm. Two classes of strategies enter the theorem.

1. $\psi$ is pairwise symmetric for optimal arms on $\mathcal D$ (Definition 3, p. 11) if, for every $\underline\nu$ in $\mathcal D$ and every pair of optimal arms $a^\star,a_\star$ with $\nu_{a^\star}=\nu_{a_\star}$, for all $T\ge1$, 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.
2. $\psi$ is monotonic on $\mathcal D$ (Definition 4, p. 13) if for all $\underline\nu'\preccurlyeq\underline\nu$ in $\mathcal D$, $\sum_{a^\star\in\mathcal A^\star(\underline\nu')}\mathbb E_{\underline\nu'}[N_{\psi,a^\star}(T)]\ge\sum_{a^\star\in\mathcal A^\star(\underline\nu)}\mathbb E_{\underline\nu}[N_{\psi,a^\star}(T)]$: on an easier problem the optimal arms are pulled at least as often.

With $\mathrm{KL}$ the Kullback–Leibler divergence, the constant of the theorem is

$$\mathcal K^{\max}_{\underline\nu}=\min_{w\in\mathcal W(\underline\nu)}\ \max_{a^\star\in\mathcal A^\star(\underline\nu)}\mathrm{KL}(\nu_w,\nu_{a^\star}).$$

The Bernoulli divergence is $\mathrm{kl}(p,q)=p\ln\frac pq+(1-p)\ln\frac{1-p}{1-q}$, (5).

Formalization targets

Goal: Theorem 4 (main display), p. 13

For every model $\mathcal D$, every strategy $\psi$ pairwise symmetric for optimal arms and monotonic on $\mathcal D$, every bandit problem $\underline\nu$ in $\mathcal D$ and every $T\ge1$,

$$\sum_{a\notin\mathcal A^\star(\underline\nu)}\mathbb E_{\underline\nu}\big[N_{\psi,a}(T)\big]\ \ge\ T\left(1-\frac{A^\star_{\underline\nu}}K-\frac{A^\star_{\underline\nu}\sqrt{2T\mathcal K^{\max}_{\underline\nu}}}K-\frac{2A^\star_{\underline\nu}T\mathcal K^{\max}_{\underline\nu}}K\right).$$

Milestones, in the order of the paper's proof

1. Lemma 2 (p. 14): if $(x-\alpha)^2\le\beta x$ with $\alpha,\beta\ge0$, then $x\le\alpha+\beta+\sqrt{\alpha\beta}$.
2. Lemma 6 (p. 20): for $0\le p<q\le1$, $\mathrm{kl}(p,q)\ge(p-q)^2/(2\max_{x\in[p,q]}x(1-x))\ge(p-q)^2/(2q)$.
3. Monotonicity reduction (p. 13): with $\tilde w$ a worst arm and $\underline{\underline\nu}$ equal to $\underline\nu$ on the optimal arms and to $\nu_{\tilde w}$ elsewhere, $\sum_{a\notin\mathcal A^\star(\underline\nu)}\mathbb E_{\underline\nu}[N_{\psi,a}(T)]\ge\sum_{a\notin\mathcal A^\star(\underline{\underline\nu})}\mathbb E_{\underline{\underline\nu}}[N_{\psi,a}(T)]$.
4. Uniform split (p. 13): if all arms of $\underline{\tilde\nu}$ carry the same distribution, $\mathbb E_{\underline{\tilde\nu}}[N_{\psi,a}(T)]=T/K$ for every arm.
5. The kl display (p. 14): $T A^\star_{\underline\nu}\mathcal K^{\max}_{\underline\nu}/K\ge\mathrm{kl}(A^\star_{\underline\nu}/K,x)$ with $x=\frac1T\sum_{a^\star\in\mathcal A^\star(\underline\nu)}\mathbb E_{\underline{\underline\nu}}[N_{\psi,a^\star}(T)]$.
6. Equation (14) (p. 14): $x\le\frac{A^\star_{\underline\nu}}K\big(1+2T\mathcal K^{\max}_{\underline\nu}+\sqrt{2T\mathcal K^{\max}_{\underline\nu}}\big)$.

Significance

Theorem 4 bounds the regret from below through $R_{\psi,\underline\nu,T}\ge(\min_{a\notin\mathcal A^\star}\Delta_a)\sum_{a\notin\mathcal A^\star}\mathbb E_{\underline\nu}[N_{\psi,a}(T)]$, (13). While $T$ is small compared with $K/(A^\star_{\underline\nu}\mathcal K^{\max}_{\underline\nu})$, the right-hand side of the theorem is of order $T(1-A^\star/K)$, so the regret is linear: a reasonable strategy cannot avoid spending a constant fraction of the first rounds on the suboptimal arms. Unlike the per-arm bounds of Theorems 2 and 3, the bound concerns all suboptimal arms at once and does not degrade as $K$ grows; §3.4 of the paper shows numerically that it gives the stronger regret bound for many arms.

The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. A formal proof would exercise the published canonical bandit model of the platform (StochasticBandit, BanditPolicy, banditMeasure) on a genuine lower-bound argument with two auxiliary bandit problems, together with a local Pinsker inequality for Bernoulli divergences in $[0,+\infty]$ that is reusable in other bandit lower bounds.

Difficulty

The obvious attempt applies the fundamental inequality (6) to $\underline\nu$ and an alternative in which one suboptimal arm becomes optimal, as in Theorem 2. That gives a bound arm by arm, which deteriorates with $K$ and does not see the number $A^\star$ of optimal arms; it also needs a hypothesis of the type "smarter than uniform", which is not assumed here. Nothing is known about how a general $\psi$ behaves on $\underline\nu$ itself, so the two hypotheses on $\psi$ must carry all the information, and both are weak: Definition 3 only constrains pairs of optimal arms with equal laws, and only through the joint distribution of their pull counts under the canonical bandit measure; Definition 4 only compares problems ordered by $\preccurlyeq$. On the analytic side, the classical Pinsker inequality $\mathrm{kl}(p,q)\ge2(p-q)^2$ loses the factor $A^\star/K$ and gives a weaker theorem, so a local refinement is required, and every divergence is valued in $[0,+\infty]$.

Formalization scope

Arms are indexed by Fin K (the paper's arm $a$ is index $a-1$), with $K\ge1$ assumed in the goal. A bandit problem is the published BanditAlgorithm.StochasticBandit K, a strategy is a published BanditPolicy K (a family of Markov kernels from histories to arms; every strategy of the paper with auxiliary uniform randomization induces one with the same law of arms and rewards), and $\mathbb E_{\underline\nu}[N_{\psi,a}(T)]$ is the integral of the pull count against banditMeasure. A model is a Set (Measure ℝ) whose members are probability measures with an integrable identity, the standing assumption of §1.1–§1.2. Definitions 3 and 4 leave $T$ implicit and are read "for all $T\ge1$"; in Definition 3 equality of distributions is equality of the image measures of the pair of counts, not of their expectations. $\mathrm{KL}$, $\mathrm{kl}$ and $\mathcal K^{\max}$ take values in $[0,+\infty]$; the goal assumes $\mathcal K^{\max}_{\underline\nu}<+\infty$, since otherwise the printed bound is $-\infty$ and a real-valued conversion would silently replace $+\infty$ by $0$. The Bernoulli divergence is defined as the divergence between two Bernoulli laws on $\mathbb R$, so it is $+\infty$ where (5) is, rather than a finite junk value. The auxiliary problems of the proof are not constructed; the milestones quantify over them with their defining properties.

The paper's "In particular" clause, $\sum_{a\notin\mathcal A^\star}\mathbb E[N_{\psi,a}(T)]\ge\frac T2(1-A^\star/K)$ for $T\le K/(8A^\star\mathcal K^{\max})$, is not stated: it follows from the main display only when $A^\star/K+\sqrt{A^\star/K}\le1/2$ (at $A^\star/K=1/2$ the main bound is negative), and whether it holds in general is not known here.

A formalization that weakens the strategy classes (full permutation symmetry, or equality of expected counts in Definition 3), drops the requirement that the problems lie in the model, or uses a real Bernoulli divergence with finite values at $q\in\{0,1\}$ does not count.

A complete development needs the fundamental inequality (6) on the canonical bandit model (the subject of mission I of this series; the chain rule for the divergence of bandit measures is already proved on the platform), the symmetry argument on the canonical measure, Lemma 6 and Lemma 2. Contributions of any of these, and of the identity $\sum_a N_{\psi,a}(T)=T$ integrated against banditMeasure, are welcome; Lemma 6 and the symmetry lemma are reusable beyond this mission.

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, 2019; arXiv:1602.07182v3. https://arxiv.org/abs/1602.07182, https://doi.org/10.1287/moor.2017.0928
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Advances in Applied Mathematics, 1996. https://doi.org/10.1006/aama.1996.0007
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

Why early exploration needs a lower bound

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

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

Bandit problems, models, and strategies

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

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

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

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

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

Formalization targets

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

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

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

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

What the result supplies

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

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

Where the difficulty lies

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

Formalization scope

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

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

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

Selected references

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

Why the large-horizon bound matters

In a stochastic multi-armed bandit, a decision maker repeatedly chooses one of several unknown reward sources. Sampling an arm reveals its reward but uses a round that could have been spent on a better arm. A good strategy must therefore reduce sampling of inferior arms, yet it cannot stop sampling them too early: it must still distinguish the current problem from a nearby one in which an apparently inferior arm is best. This tension produces the logarithmic lower bounds that benchmark bandit algorithms.

Garivier, Ménard and Stoltz revisit that benchmark in Explore First, Exploit Next. Their Theorem 5 gives a finite-horizon lower bound with explicit terms beyond the leading logarithm. It concerns every uniformly super-fast convergent strategy on a well-behaved model, not a particular algorithm. The distinction matters when comparing an algorithm's upper bound to what any strategy with that uniform performance guarantee must pay. The theorem is proved in the paper; this mission asks for a machine-checked statement and proof of that established result.

Bandit model and information cost

There are $K$ arms. Arm $a$ has an unknown probability distribution $\nu_a$ over real rewards, with finite mean $\mu_a$. The vector $\underline\nu=(\nu_a)_{a=1}^K$ is a bandit problem. Its best mean is $\mu^*=\max_a\mu_a$, and the gap of arm $a$ is $\Delta_a=\mu^*-\mu_a$. An arm with $\Delta_a>0$ is suboptimal. A strategy $\psi$ selects an arm each round using the previous arms and rewards, possibly with randomization. Write $N_{\psi,a}(T)$ for the number of times it selects arm $a$ by round $T$, and $\mathbb E_{\underline\nu}[N_{\psi,a}(T)]$ for the expected count under the problem $\underline\nu$.

A model $\mathcal D$ specifies the probability distributions that an arm may have. All its laws have a finite first moment, and a bandit problem is in $\mathcal D$ when every arm law belongs to it. For a law $P$ and a target mean $x$, the paper's minimal information cost is

$$\mathcal K_{\inf}(P,x,\mathcal D) =\inf\{\mathrm{KL}(P,Q):Q\in\mathcal D,\ \mathrm E(Q)>x\},$$

where an empty infimum is $+\infty$. This measures how much the law of an arm must change to make its mean exceed $x$. The Bernoulli divergence $\mathrm{kl}(p,q)$ used in the intermediate change-of-measure bound keeps its infinite values at the boundary.

Let $E(\mathcal D)$ be the interior of the set of expectations of laws in $\mathcal D$. A model is well behaved when positive functions $\varepsilon_{\mathcal D}$ and $\omega_{\mathcal D}$ satisfy, whenever $P\in\mathcal D$, $x\in E(\mathcal D)$, $\mathrm E(P)<x$, and $0<\varepsilon<\varepsilon_{\mathcal D}(x)$,

$$\mathcal K_{\inf}(P,x+\varepsilon,\mathcal D) \le \mathcal K_{\inf}(P,x,\mathcal D)+\varepsilon\omega_{\mathcal D}(P,x).$$

A strategy is uniformly super-fast convergent with constant $C_{\psi,\mathcal D}$ when $\mathbb E_{\underline\nu}[N_{\psi,a}(T)]\le C_{\psi,\mathcal D}\ln T/\Delta_a^2$ for every problem in $\mathcal D$, every suboptimal arm, and every $T\ge2$. The same constant applies throughout. Finally, $H(\underline\nu)=\sum_{a:\Delta_a>0}\Delta_a^{-2}$ records the inverse-squared gaps of all suboptimal arms.

Formalization targets

For each suboptimal arm let $\mathcal K=\mathcal K_{\inf}(\nu_a,\mu^*,\mathcal D)$. The goal is Theorem 5, with $\varepsilon_T=(\ln T)^{-4}$ and

$$a_T=\frac{\omega_{\mathcal D}(\nu_a,\mu^*)}{\mathcal K}\varepsilon_T, \qquad b_T=C_{\psi,\mathcal D}H(\underline\nu)\frac{\ln T}{T}, \qquad c_T=\frac{\ln(KC_{\psi,\mathcal D}(\ln T)^9)}{\ln T}.$$

For every $T\ge2$ satisfying $\varepsilon_T<\varepsilon_{\mathcal D}(\mu^*)$, $a_T<1$, $b_T<1$, and $0\le c_T<1$, the target is

$$\mathbb E_{\underline\nu}[N_{\psi,a}(T)] \ge \frac{\ln T}{\mathcal K}\bigl(1-(a_T+b_T+c_T)\bigr) -\frac{\ln 2}{\mathcal K}.$$

The milestones follow the paper's displayed bounds: the one-alternative inequality (15), the optimized inequality (17), the inverse-information-cost bound after (17), and the product inequality quoted immediately before Theorem 5. They preserve the same constants and the same $H(\underline\nu)$.

What the result supplies

The leading term $\ln T/\mathcal K$ is the familiar distribution-dependent sampling barrier. The explicit $a_T$, $b_T$, and $c_T$ quantify the correction at a finite horizon; the paper observes that their combined contribution has order $\ln\ln T$ under its conditions. This makes the result useful when an algorithm's upper bound includes a second-order term and one wants to know the scale that a lower bound permits. It also identifies precisely which model regularity and uniform strategy guarantee support that comparison.

Formalizing Theorem 5 would add a reusable finite-horizon lower bound to the bandit library. The published definitions of stochastic bandits, policies, pull counts, and $\mathcal K_{\inf}$ supply the base model; this mission adds the paper's well-behavedness and super-fast convergence predicates and states the intermediate inequalities as separate targets. The paper's proof is established mathematically, while these mission statements remain open Lean theorems until solvers supply machine-checked proofs.

Main difficulty

The information cost is an infimum over alternative reward laws, so the finite-horizon bound must remain meaningful when the feasible set is empty or its divergence is infinite. The displayed formulas also divide by that information cost and use logarithms of quantities involving the strategy's uniform constant. For Theorem 5, the explicit correction factors must all lie in the range where the paper's final product inequality applies. A purely asymptotic statement would discard exactly the constants and horizon conditions that distinguish this theorem.

Formalization scope

Arms are Fin K, so the paper's arm $a\in\{1,\ldots,K\}$ has Lean index $a-1$. A strategy is represented by Markov kernels on observed arm-reward histories; its expected pull count is an integral of a bounded count. The model consists of probability measures on $\mathbb R$ with integrable identity. The information cost and Bernoulli divergence live in $[0,+\infty]$; a finite positive cost is converted to a real number only where a displayed reciprocal requires it. The goal contains a suboptimal arm, which rules out the empty-arm and single-arm cases. The model's witness functions are total in Lean, with requirements only on their paper-defined domains.

The theorem explicitly assumes $\mu^*\in E(\mathcal D)$ and $0<\mathcal K<+\infty$, which are implicit in the paper's use of $\varepsilon_{\mathcal D}(\mu^*)$ and $1/\mathcal K$. It also assumes $c_T\ge0$: the printed proof invokes a product inequality requiring that sign, although the theorem prints only $c_T<1$. The version of (17) in the milestone list assumes $b_T\le1$ in the case of a negative logarithm. These conditions and the model's integrability prevent vacuous or totalized-value readings of the lower bound. Contributions toward the four displayed milestones, the required measure-theoretic change of measure, and the finite-horizon arithmetic are in scope.

Selected references

• Aurélien Garivier, Pierre Ménard, and Gilles Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research 44 (2019); arXiv:1602.07182v3, DOI:10.1287/moor.2017.0928.
• Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, Cambridge University Press (2020), Chapters 4 and 16; DOI:10.1017/9781108571401.

Motivation

A seller with several goods can sell them one at a time or offer a mechanism that links allocation and payment across goods. Separate selling asks the seller to solve a one-good pricing problem for each item. A general mechanism can offer lotteries and menus whose outcomes depend on the buyer's whole valuation vector. The difference matters because the buyer's private information covers several values at once, and an optimal multidimensional mechanism need not resemble an ordinary posted price. Hart and Nisan ask how much revenue is guaranteed by simple selling rules when the joint valuation distribution is unrestricted apart from the stated independence assumptions (Hart and Nisan, arXiv:1204.1846v3).

This mission isolates their two-good, identically distributed result, Theorem B. The paper first gives a one-half guarantee for two independent goods with potentially different distributions, then improves the guarantee to $e/(e+1)$ when their distributions agree. The improvement is a claim about every probability law on nonnegative values. It assumes neither a density nor a regularity condition on the tail of that law. The paper proves the result in Appendix A.1 after stating it in the introduction (Hart and Nisan, pp. 6 and 31–35).

Setting

There is one risk-neutral buyer and one seller. For two goods, the buyer's private valuation is a vector $(Y,Z)$ with $Y,Z\ge0$. Values are additive: receiving both goods is worth $Y+Z$. The seller knows the distribution of the vector but not the realized values. In this mission, $Y$ and $Z$ are independent and have the same arbitrary probability law $\nu$ on $\mathbb R_{\ge0}$. A law, rather than a named pair of random variables on a probability space, carries all the data needed by the revenue quantities.

A direct mechanism $\mu=(q,s)$ takes a reported pair $x=(y,z)$ and returns an allocation probability $q_i(x)\in[0,1]$ for each good and a real payment $s(x)$ to the seller. The buyer's payoff from reporting truthfully is $b(x)=q(x)\cdot x-s(x)$. The mechanism is incentive compatible (IC) if truthful reporting is at least as good as any other report for every possible valuation, and individually rational (IR) if truthful payoff is nonnegative everywhere. These requirements hold on the whole nonnegative orthant, as in Section 2.1 of the paper (Hart and Nisan, pp. 11–14).

Write $R(\mu;X)$ for the expected payment under a valuation law $X$ and $\operatorname{Rev}(X)$ for the supremum of $R(\mu;X)$ over feasible, IC, IR mechanisms. For one good, write $\operatorname{Rev}_1(\nu)$. The separate-selling revenue for two identically distributed goods is $\operatorname{SRev}(Y,Z)=2\operatorname{Rev}_1(\nu)$. Equation (1) of the paper identifies the one-good value with the supremum of posted-price revenue $p\Pr[Y\ge p]$; the supremum formulation covers laws for which no maximizing price exists (Hart and Nisan, p. 12; Myerson, 1981).

Formalization targets

Theorem B: the guarantee for two i.i.d. goods

The goal is the exact upper bound written at the start of the paper's proof:

$$\operatorname{Rev}(Y,Z)\le\frac{e+1}{e}\bigl(\operatorname{Rev}(Y)+\operatorname{Rev}(Z)\bigr)=\frac{e+1}{e}\operatorname{SRev}(Y,Z).$$

Equivalently, separate selling guarantees at least $e/(e+1)$ of optimal revenue whenever the ratio has an ordinary meaning. The inequality itself is the stable formulation at zero and infinite revenues. The formal goal uses the exact constant $(e+1)/e$, not the rounded percentage in the theorem's prose (Hart and Nisan, Theorem B, p. 6; proof, p. 31).

Supporting targets

The milestones include the one-good posted-price identity, the fact that nonnegative payments suffice when optimizing, symmetrization for identical independent goods, Lemma 19's lower-valuation revenue bound, equation (12), and the two expectation estimates and final numerical bound used after it. Proposition 5's IC characterization is also a draft theorem, though it is not a milestone. Each statement retains its source's domain and the constant $1/e$. The final inequality for the right side of (12) is stated for every nondecreasing allocation function into $[0,1]$, as required by the paper's argument on pp. 33–35.

Significance

Theorem B gives a distribution-free quantitative guarantee for an easy-to-describe selling rule in a setting where the optimal rule may depend on the buyer's entire two-dimensional private type. Its $e/(e+1)$ guarantee is stronger than the one-half guarantee for merely independent goods stated as Theorem A. The conclusion concerns the best revenue available from all feasible IC and IR mechanisms, so the benchmark includes randomized allocations and payments depending on both reported values (Hart and Nisan, pp. 6 and 11–13).

The formalization target is a machine-checked version of a proved result, not a new conjecture. The proposal currently contains compiled Lean statements with unproved theorem bodies. A completed development would prove the stated inequality and its selected supporting results. It would also supply reusable definitions for direct mechanisms with additive nonnegative values, extended-real revenue, optimal revenue as a supremum, and symmetry of two-good mechanisms. No machine-checked proof of these proposed Hart–Nisan statements is claimed here.

Difficulty

The one-good posted-price formula does not directly control an arbitrary two-good mechanism: allocation of either good and the payment can depend on both reported values. Applying a one-good bound separately to the two coordinates therefore leaves terms that depend on the other coordinate. In particular, a direct comparison between each marginal posted-price optimum and the total payment loses the improved constant. The proof has to control the dependence created by a joint mechanism while retaining the exact $1/e$ numerical estimate. A second formal difficulty is that an admissible mechanism can have a negative expected payment even though optimal revenue is nonnegative, while an unrestricted law can give infinite optimal revenue. Replacing every expectation by an ordinary real integral or clipping each mechanism's revenue would change Lemma 19 and the intermediate inequalities (Hart and Nisan, pp. 31–35).

Formalization scope

Valuations are finite vectors $\iota\to\mathbb R_{\ge0}$; the main theorem fixes $\iota=\operatorname{Fin}(2)$. The two-good law is the product of the same one-good probability measure in both coordinates, so independence and identical distribution are built into the data. The model represents allocation probabilities as real numbers with explicit bounds $0\le q_i\le1$. It requires IC and IR pointwise on all reports. No positive transfer (NPT) means $s(x)\ge0$ and is imposed only on supporting statements where the paper uses it. Following the paper's footnote 12, admissibility also requires the payment function to be measurable.

An individual expected payment is an extended real difference of positive and negative Lebesgue integrals. For IC mechanisms, the negative part is finite because the payment is bounded below by its value at zero. Optimal revenue is the supremum of the nonnegative clips of admissible mechanisms' expected payments; the zero mechanism makes this the same supremum as in the paper. Lemma 19 and equation (12) keep individual revenue in the extended reals. Supporting inequalities that write $r=\operatorname{Rev}_1(\nu)$ as a real number explicitly assume $r<\infty$; Theorem B does not. Integrals of bounded threshold functions use ordinary real expectation, while the nonnegative term $W$ uses a nonnegative Lebesgue integral. The goal cannot be satisfied by a correlated joint law, a bounded-support special case, a vacuous assumption on $\nu$, or a rounded constant.

The reusable work includes one-good posted-price revenue for arbitrary laws, a nonnegative-transfer reduction, a faithful single-mechanism revenue type, and probability identities for two independent coordinates. Theorem A, Theorem 7, Theorem 16, and a full formalization of the paper's other selling rules are outside this mission.

Selected references

• Sergiu Hart and Noam Nisan, Approximate Revenue Maximization with Multiple Items, Journal of Economic Theory, 2017. Source used here: arXiv:1204.1846v3.
• Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. DOI:10.1287/moor.6.1.58.

Motivation

The Decision-Estimation Coefficient (DEC) of Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) is a single complexity measure that bounds the minimax regret of interactive decision making (bandits, reinforcement learning, and their structured variants) from above and from below. Its lower bound (Theorem 3.2 of the paper) states that every algorithm suffers expected regret at least a constant times $\mathsf{dec}_\gamma(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}) \cdot T$, so concrete lower bounds on regret follow from concrete lower bounds on the DEC of localized model classes.

The multi-armed bandit is the first test of this program. Its minimax regret $\Theta(\sqrt{AT})$ is classical (Auer et al., 2002; Audibert and Bubeck, 2010). Section 5.1 of the paper recovers it through the DEC: posterior sampling (Proposition 5.1) and inverse gap weighting (Proposition 5.2) bound the DEC by $A/\gamma$ from above, and Proposition 5.3 bounds it by $2^{-6} A/\gamma$ from below. The lower bound is proved through a hard family of models (Definition 5.1, Lemma 5.1), the device that the paper reuses for linear, ReLU and gap-dependent lower bounds in §§6–7.

Setting

A decision space $\Pi$ is a finite set; here $\Pi = [A] = \{1, \dots, A\}$, the arms. A model $M$ assigns to every arm $\pi$ a distribution $M(\pi)$ over rewards in $\mathcal{R} = [0,1]$ (observations are trivial). Its mean reward is $f^M(\pi) = \mathbb{E}_{r \sim M(\pi)}[r]$, and $\pi_M \in \arg\max_\pi f^M(\pi)$ is an optimal arm. The squared Hellinger distance between distributions $P, Q$ on a finite set is $D^2_{\mathrm{H}}(P, Q) = \sum_y (\sqrt{P(y)} - \sqrt{Q(y)})^2$ (no factor $\tfrac12$, the paper's (5)).

For a class $\mathcal{M}$ of models, a reference model $\overline{M}$ and $\gamma > 0$, the DEC (2) is

$$\mathsf{dec}_\gamma(\mathcal{M}, \overline{M}) = \inf_{p \in \Delta(\Pi)} \sup_{M \in \mathcal{M}} \mathbb{E}_{\pi \sim p}\Bigl[ f^M(\pi_M) - f^M(\pi) - \gamma \cdot D^2_{\mathrm{H}}\bigl(M(\pi), \overline{M}(\pi)\bigr) \Bigr].$$

With $g^M(\pi) = f^M(\pi_M) - f^M(\pi)$, the $L_\infty$-localized class (12) is $\mathcal{M}^\infty_\varepsilon(\overline{M}) = \{ M \in \mathcal{M} : |g^M(\pi) - g^{\overline{M}}(\pi)| \le \varepsilon\ \forall \pi \}$.

A reference model $\overline{M} \in \mathcal M$ and models $M_1, \dots, M_N \in \mathcal M$, $N \ge 2$, form an $(\alpha, \beta, \delta)$-family (Definition 5.1) if there are $u_i, v_i : \Pi \to [0,1]$ with $\sum_i u_i(\pi) \le N/2$, $\sum_i v_i(\pi) \le 1$, $f^{M_i}(\pi_{M_i}) - f^{M_i}(\pi) \ge \alpha(1 - u_i(\pi))$ and $D^2_{\mathrm{H}}(M_i(\pi), \overline{M}(\pi)) \le \beta v_i(\pi) + \delta$. $\mathrm{Ber}(q)$ is the Bernoulli distribution with mean $q$.

Formalization targets

Goal: Proposition 5.3

For $A \ge 2$ arms, $\overline{M}(\pi) = \mathrm{Ber}(\tfrac12)$ and every $\gamma \ge A/3$, with $\varepsilon_\gamma = \frac{A}{12\gamma}$,

$$\mathsf{dec}_\gamma\bigl(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}\bigr) \ge 2^{-6} \cdot \frac{A}{\gamma}.$$

Milestones

1. Lemma A.7: $D^2_{\mathrm{H}}(\mathrm{Ber}(p), \mathrm{Ber}(q)) \le (p-q)^2\bigl(\frac{1}{p+q} + \frac{1}{2-p-q}\bigr)$, and in particular $D^2_{\mathrm{H}}(\mathrm{Ber}(\tfrac12 + \Delta), \mathrm{Ber}(\tfrac12)) \le 3\Delta^2$ for $\Delta \in (0, \tfrac12)$.
2. Lemma 5.1: an $(\alpha, \beta, \delta)$-family $\mathcal{M}'$ with $\beta \ge 0$ satisfies $\mathsf{dec}_\gamma(\mathcal{M}', \overline{M}) \ge \frac{\alpha}{2} - \gamma(\frac{\beta}{N} + \delta)$ for all $\gamma > 0$.
3. The hard family of the proof: $M_i(\pi) = \mathrm{Ber}(\tfrac12 + \Delta\,\mathbb{I}\{\pi = i\})$ is a $(\Delta, 3\Delta^2, 0)$-family around $\mathrm{Ber}(\tfrac12)$.
4. Localization: this family lies in $\mathcal{M}^\infty_\Delta(\overline{M})$.

Companions

The mission also states monotonicity of the DEC in the class (the step from the family to the localized class), Proposition 5.1 (posterior sampling bounds the dual square-loss DEC by $A/\gamma$), and Proposition 6.7, the gap-dependent variant: for bandits with gap exactly $\Delta \in (0, \tfrac18)$, some $\overline{M}$ in the class has $\mathsf{dec}_\gamma(\mathcal{M}^\infty_\Delta(\overline{M}), \overline{M}) \ge \frac{\Delta}{4}\mathbb{I}\{\gamma \le \frac{A}{48\Delta}\}$. Proposition 5.2 (inverse gap weighting) and the decoupling step of Proposition 5.1 are already proved on the platform and are included as references.

Significance

Proposition 5.3 is the DEC half of the $\Omega(\sqrt{AT})$ minimax lower bound for multi-armed bandits: combined with Theorem 3.2 and $\gamma \asymp \sqrt{AT}$, it shows that the general DEC theory loses nothing in rate on the most basic interactive problem, and that the $A/\gamma$ upper bounds of Propositions 5.1 and 5.2 are tight up to constants. Lemma 5.1 is reusable: any lower bound on the DEC of a class can be obtained by exhibiting a hard family, and the paper uses it for linear bandits (Proposition 6.2), ReLU bandits (Proposition 6.6) and gap-dependent bounds (Propositions 6.7, 6.8).

The results are proved in the paper. As far as is known, none of them is machine-checked. A formal development provides a verified Bernoulli Hellinger bound, a reusable hard-family lemma for the DEC as published on the platform, and the first verified DEC lower bound for a concrete class.

Difficulty

The DEC is an inf-sup, so a lower bound must hold against every exploration distribution $p$. A natural first attempt picks a single alternative model and compares; this fails because $p$ can concentrate on the arm where that alternative differs and then the Hellinger penalty cancels the regret. The family must be spread so that no single $p$ is good for all of its members at once, and the constants must balance the regret term against the information term at the chosen $\Delta$. In Lean, an additional difficulty is that the DEC is written with real sInf/sSup, which are $0$ on empty or unbounded sets: every lower bound requires showing that the relevant sets are nonempty and bounded, and passing from the family to the localized class needs monotonicity of the DEC, which the paper uses without comment.

Formalization scope

• Finite alphabets. The paper works over measurable spaces; this mission formalizes the finite-alphabet case, as the published FoundationsRL layer does. A model is m : S → Y → ℝ with every m π a probability vector; expectations are finite sums. The DEC is the published FoundationsRL.GeneralDM.decGf, the Hellinger distance hellingerSq, the mean reward fM.
• Bernoulli subclass. The bandit class is the Bernoulli bandits (Y = Bool, reward $1$ on true), a subclass of the paper's all-distributions-on-$[0,1]$ class. The DEC is monotone in the class and the localized class shrinks with the class, so the Bernoulli lower bounds imply the paper's.
• Optimal-arm selector. $\pi_M$ is a parameter piStar with the hypothesis that it picks a maximizer of $f^M$; every statement holds for every such selector, so for whichever maximizer the paper meant (the reference $\mathrm{Ber}(\tfrac12)$ has every arm optimal).
• Added or dropped hypotheses. Lemma 5.1 makes the page's nonempty decision space explicit; its optimal-arm selector also implies nonemptiness. It adds $\beta \ge 0$, necessary for the printed averaging argument: without it, even identical models can contradict (52). The family definition includes membership of the reference and family models in a probability-model class. The localization claim inherits $A \ge 2$ from Proposition 5.3. Proposition 6.7 states $A \ge 2$, implicit on the page since a gap needs two arms. Proposition 5.1 represents models by their mean vectors and priors as finitely supported (footnote 5).
• Constants. All constants are the page's: $2^{-6}$, $A/(12\gamma)$, $\gamma \ge A/3$, $3\Delta^2$, $5\Delta^2$, $\Delta/4$, $A/(48\Delta)$. The page's proof of Proposition 6.7 names a $(\Delta, 5\Delta^2, 0)$-family but computes with $12\Delta^2$; the stated proposition is the one its arithmetic supports.
• No trivialization. A formalization in which the localized class could be empty, or the payoffs unbounded, would make decGf evaluate to the junk value $0$; the goal is stated over a class containing $\overline{M}$ with bounded rewards, so the inequality is the genuine one, and its right side $2^{-6} A/\gamma$ is strictly positive.

Contributions welcome: proofs of the milestones in attack order, sorry-free lemmas on nonemptiness and boundedness of the DEC's inner sets (reusable for every DEC lower bound in this series), and a proof of the gap-dependent companion.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, 2021 (v3, 2023). https://arxiv.org/abs/2112.13487
• D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, lecture notes, 2023. https://arxiv.org/abs/2312.16730
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• J.-Y. Audibert, S. Bubeck, Regret Bounds and Minimax Policies under Partial Monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
• D. J. Foster, A. Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, ICML, 2020. https://arxiv.org/abs/2002.04926

Motivation

Generalized Turán problems ask for the maximum number of copies of a fixed graph $H$ in an $n$-vertex graph that avoids a family $\mathcal F$ of forbidden subgraphs. The ordinary Turán number counts edges ($H = K_2$); Alon and Shikhelman (arXiv:1506.03397) started the systematic study of the general function $\mathrm{ex}(n, H, \mathcal F)$, building on earlier results of Erdős on cliques, Bollobás and Győri on pentagons in triangle-free graphs, and Győri and Li on triangles in graphs without a long odd or even cycle. Counting cycles in graphs with forbidden cycles is closely tied to extremal problems for Berge hypergraphs, and the constructions used are sparse hypergraphs of large girth.

Gerbner, Győri, Methuku and Vizer, Generalized Turán problems for even cycles (arXiv:1712.07079, J. Combin. Theory Ser. B, 2020), determine or bound $\mathrm{ex}(n, C_{\ell}, \mathcal F)$ for many cycle families. This mission covers one of their results in §6.2: the number of odd cycles $C_{2l+1}$ in a graph in which every shorter cycle is forbidden and, in addition, one longer odd cycle $C_{2k+1}$ is forbidden. Its companion (Theorem 17, a separate mission of this series) forbids a longer even cycle $C_{2k}$ instead, and there the paper obtains a sub-quadratic upper bound; with an odd extra cycle only a quadratic upper bound is proved.

Setting

All graphs are finite and simple. For an integer $a \ge 3$, $C_a$ is the cycle of length $a$. For a set $A$ of integers $a \ge 3$, write $\mathcal C_A = \{C_a : a \in A\}$; a graph is $\mathcal C_A$-free if it contains no $C_a$ with $a \in A$ as a (not necessarily induced) subgraph. The family $\mathcal C_{2l}$ consists of all cycles $C_3, C_4, \dots, C_{2l}$.

For graphs $H$ and $G$, $\mathcal N(H, G)$ is the number of copies of $H$ in $G$: subgraphs of $G$ isomorphic to $H$, counted without labelling. The generalized Turán number is

$$\mathrm{ex}(n, H, \mathcal F) = \max\{\mathcal N(H, G) : G \text{ has } n \text{ vertices and contains no member of } \mathcal F\}.$$

For a vertex $v$ of $G$, $N_i(v)$ is the set of vertices at distance exactly $i$ from $v$.

A hypergraph is a finite set of hyperedges (vertex sets); it is $r$-uniform if each hyperedge has $r$ vertices. A Berge cycle of length $j \ge 2$ is a sequence $v_1, h_1, v_2, h_2, \dots, v_j, h_j, v_1$ of distinct vertices and distinct hyperedges with $v_i, v_{i+1} \in h_i$ and $v_j, v_1 \in h_j$. The girth of a hypergraph is the length of its shortest Berge cycle; "girth at least $s$" means there is no Berge cycle of length $2, \dots, s-1$.

Formalization targets

Goal: Theorem 18

For all integers $k > l \ge 2$, as $n \to \infty$,

$$\Omega\big(n^{1+\frac{1}{2k+2}}\big) = \mathrm{ex}\big(n, C_{2l+1}, \mathcal C_{2l} \cup \{C_{2k+1}\}\big) = O(n^2).$$

Both the lower and the upper bound are part of the goal; the implied constants may depend on $k$ and $l$ only.

Milestones

1. Theorem 29 (Nešetřil–Rödl). For $r \ge 2$, $s \ge 3$ and all large $n$ there is an $r$-uniform hypergraph on $n$ vertices of girth at least $s$ with at least $n^{1+1/s}$ hyperedges.
2. The construction. Replacing each hyperedge of a $(2l+1)$-uniform hypergraph of girth at least $2k+2$ by a copy of $C_{2l+1}$ yields a graph with no cycle of length at most $2k+1$ other than $2l+1$, and with at least as many copies of $C_{2l+1}$ as hyperedges.
3. Cycles through a vertex. In a $\mathcal C_{2l} \cup \{C_{2k+1}\}$-free graph there is no edge inside $N_i(v)$ for $i < l$, every $C_{2l+1}$ through $v$ uses exactly one edge inside $N_l(v)$, and so the number of $C_{2l+1}$'s through $v$ is at most the number of edges inside $N_l(v)$.
4. Claim 19. In a $\mathcal C_{2l} \cup \{C_{2k+1}\}$-free graph the number of edges inside $N_l(v)$ is at most $C(k,l)\,|N_l(v)| \le C(k,l)\, n$.

The supporting published theorem erdos_gallai_path_conjecture (the Erdős–Gallai path theorem: a graph on $n$ vertices with no path of $m+1$ edges has at most $mn/2$ edges) is included as a reference item; the paper's proof of Claim 19 invokes it.

Significance

Theorem 18 shows that forbidding all cycles up to length $2l$ together with one odd cycle $C_{2k+1}$ still permits polynomially more than $n$ copies of $C_{2l+1}$, at least $n^{1 + 1/(2k+2)}$, and at most $O(n^2)$. Compared with Theorem 17, where an even cycle $C_{2k}$ is forbidden and the count is $O(n^{1+l/(l+1)})$, it isolates the role of the parity of the extra forbidden cycle. The authors conjecture that the true order is sub-quadratic (Conjecture 34, §8 of the paper), so the gap between the two exponents in Theorem 18 is a stated open question; a formal development of the known bounds is the base on which any improvement would be checked.

The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces: a reusable encoding of generalized Turán numbers for cycle families on top of Mathlib's copyCount; Berge cycles and the girth of uniform hypergraphs; distance layers $N_i(v)$; and a formal statement of the Nešetřil–Rödl existence theorem, which is used as a black box by many extremal constructions.

Difficulty

The upper bound requires careful bookkeeping of distance layers around a vertex in a graph without short cycles. The obvious estimate, bounding the copies of $C_{2l+1}$ through $v$ by the number of pairs of vertices of $N_l(v)$, gives only $|N_l(v)|^2$ per vertex and hence nothing better than the trivial bound overall; the content of Claim 19 is that forbidding the single cycle $C_{2k+1}$ makes the edge count inside $N_l(v)$ linear, and the parity of $2k+1$ is used essentially.

The lower bound rests on Theorem 29, a cited result that is not proved in the paper, and for which Mathlib has no supporting theory of uniform hypergraphs or Berge cycles. For the construction itself, the paper only asserts that the cycle-replacement graph has no short cycle other than the inserted $C_{2l+1}$'s; a cycle of the graph may wander through many hyperedges, and relating it to the girth of the hypergraph is the step a formal proof has to supply.

Formalization scope

• Vertices of an $n$-vertex graph are Fin n; graphs are SimpleGraph (Fin n). Cycles are Mathlib's SimpleGraph.cycleGraph, and $\mathcal N(H, G)$ is Mathlib's unlabelled copyCount.
• $\mathcal C_{2l} \cup \{C_{2k+1}\}$ is encoded as the set of lengths Set.Icc 3 (2 * l) ∪ {2 * k + 1}: every length $3, \dots, 2l$, not only $2l$.
• $\mathrm{ex}(n, H, \mathcal C_A)$ is the supremum of a nonempty finite set of natural numbers, hence a true maximum (checked in a sanity file).
• $N_i(v)$ uses the extended distance edist, so vertices of other components lie in no layer.
• Hypergraphs are Finset (Finset V); "girth at least $s$" is a predicate (no Berge cycle of length $2, \dots, s-1$), not an infimum, so a hypergraph without Berge cycles has every girth.
• $\Omega$ and $O$ are Mathlib's Asymptotics.IsBigO along atTop, with real exponents; both directions of the goal are stated.
• Claim 19's $O(\cdot)$ is a single constant chosen before $n$, the graph and the vertex. The milestone on cycles through $v$ uses the page's $\mathcal C_{2l} \cup \{C_{2k+1}\}$-freeness assumption.

A formalization that states only the upper bound, uses labelled copies, lets a constant depend on the graph, omits the short cycles $C_3, \dots, C_{2l-1}$ from the forbidden family, or defines $\mathrm{ex}$ by a supremum that can take a junk value, does not prove this theorem.

Contributions welcome: proofs of the milestones, a proof of Theorem 29, and general lemmas on breadth-first layers in graphs of large girth, which are reusable by the companion missions of this series.

Selected references

• D. Gerbner, E. Győri, A. Methuku, M. Vizer, Generalized Turán problems for even cycles, J. Combin. Theory Ser. B (2020); arXiv:1712.07079v3. https://arxiv.org/abs/1712.07079, https://doi.org/10.1016/j.jctb.2020.05.005
• N. Alon, C. Shikhelman, Many T copies in H-free graphs, J. Combin. Theory Ser. B 121 (2016). https://arxiv.org/abs/1506.03397
• J. Nešetřil, V. Rödl, On a probabilistic graph-theoretical method, Proc. Amer. Math. Soc. 72(2), 417–421 (1978). https://www.ams.org/journals/proc/1978-072-02/
• P. Erdős, T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959). https://doi.org/10.1007/BF02024498