All missions

Motivation

A directed polymer in a random environment is a random walk whose paths are weighted by the disorder they encounter. The walk favors paths with large accumulated weight, and its endpoint distribution can concentrate on a small number of sites even though the number of possible paths grows exponentially. Understanding how much probability remains spread across many small endpoint masses is a basic question about localization. The distinction matters especially beyond exactly solvable polymer models, where explicit formulas for the endpoint law are rarely available. Bates and Chatterjee study this question for independent disorder in every spatial dimension $d\geq1$ under a finite exponential-moment condition Bates and Chatterjee, 2021.

The paper separates two temperature regimes using the limiting free energy. Earlier localization statements detected persistent large atoms. The target here asks whether those atoms account for all endpoint probability in a time-averaged sense. It also specifies the complementary high-temperature behavior, where a suitable vanishing mass threshold captures asymptotically none of the probability. The result is Theorem 1.1 of the preprint, restated as Theorem 6.3 Bates and Chatterjee, 2021, pp. 16, 43.

Setting

Fix $d\geq1$. A path starts at the origin in $\mathbb Z^d$ and makes one of its $2d$ nearest-neighbor moves at each integer time. The environment $(X_{i,x})$ consists of independent, identically distributed real random variables with common law $\mathfrak L$. The disorder law is nondegenerate: it is not concentrated at one number. An inverse temperature $\beta\geq0$ determines the weight of a path $\gamma$ of length $n$:

$$w_\beta(\gamma)=\exp\!\left(\beta\sum_{i=1}^{n}X_{i,\gamma(i)}\right),\qquad Z_n=(2d)^{-n}\sum_{\gamma}w_\beta(\gamma).$$

The endpoint mass function $f_n(x)$ is the sum of weights of paths ending at $x$, divided by the sum of all path weights. Thus $f_n$ is a probability mass function on $\mathbb Z^d$. For $\varepsilon>0$, the $\varepsilon$-atoms are the sites $\mathcal A_n^\varepsilon=\{x:f_n(x)>\varepsilon\}$, and $\rho_n(\omega_n\in\mathcal A_n^\varepsilon)$ is their total mass. The strict inequality matters at a threshold equal to an atom mass.

Write $F_n=\log Z_n/n$ for $n\geq1$, with $F_0=0$, and $\lambda(\alpha)=\log\mathbb E_{\mathfrak L}e^{\alpha X}$. The standing condition is that this exponential moment is finite for every $\alpha\in[-2\beta,2\beta]$. The paper's Theorem A characterizes the high-temperature phase by $\lim_n\mathbb E F_n=\lambda(\beta)$ and the low-temperature phase by $\lim_n\mathbb E F_n<\lambda(\beta)$ Bates and Chatterjee, 2021, pp. 4–5.

Formalization targets

Asymptotic pure atomicity

The goal is both clauses of Theorem 1.1. For every positive deterministic sequence $\varepsilon_i\to0$, low temperature gives

$$\frac1n\sum_{i=0}^{n-1}\rho_i(\omega_i\in\mathcal A_i^{\varepsilon_i})\longrightarrow1 \quad\text{almost surely}.$$

At high temperature there exists a positive deterministic sequence $\varepsilon_i\to0$ for which the same average converges almost surely to $0$. The sequence in this second clause is selected independently of the realized environment. Together the clauses characterize the paper's stronger, almost-sure form of asymptotic pure atomicity Bates and Chatterjee, 2021, Theorems 1.1 and 6.3.

The milestones are fifteen statements of the paper, in the order the proof of the goal uses them:

• the triangle inequality for the distance $d$ on partitioned subprobability measures (Lemma 2.3) and sequential compactness of $(\mathcal S,d)$ (Theorem 2.8);
• continuity of the update law $f\mapsto\mathcal Tf$ into $(\mathcal P(\mathcal S),\mathcal W)$ and of the log moments $f\mapsto\mathbb E\log^q\widetilde F$ (Proposition 3.2);
• convergence of the empirical endpoint measures $\mu_n=\frac1n\sum_{i<n}\delta_{f_i}$ to the fixed-point set $\mathcal K$ (Corollary 4.3); invariant laws charge only states of mass $0$ or $1$ (Proposition 4.4);
• the variational formula for the free energy: $|F_n-\mathcal R(\mu_n)|\to0$ (Proposition 4.5), the lower bound (Proposition 4.6), the key inequality $\sum_{i<n}\mathcal R(\mathcal T^i\delta_{f_0})\ge\mathbb E\log Z_n$ (Lemma 4.8), and $\lim F_n=\inf_{\nu\in\mathcal K}\mathcal R(\nu)$ (Theorem 4.7);
• convergence of $\mu_n$ to the minimizing set $\mathcal M$ (Theorem 4.9), the extrema of $R$ (Lemma 5.1) and the fixed-point characterization of the two phases (Theorem 5.2);
• semicontinuity of the atom functionals (Lemma 6.1), a fixed-threshold criterion for pure atomicity (Lemma 6.2), and a Dini theorem for semicontinuous functions (Lemma 6.4).

Significance

The low-temperature conclusion rules out a residual diffuse component in the time-averaged endpoint law. A vanishing threshold may still be used to collect almost all of the polymer's probability. The high-temperature clause shows that this property distinguishes the phases under the stated moment assumption. The result strengthens a statement that only asks for a positive amount of mass on large atoms, and gives an almost-sure conclusion for the Cesàro averages Bates and Chatterjee, 2021, §§1.2.3, 6.

A formal development would supply a reusable compactification of endpoint probability measures and a checked route from its invariant laws to localization observables. The milestones expose the pieces that need separate verification, and the compactification and variational formula are reusable for the companion mission on geometric localization. The paper proves the mathematical theorem; this mission asks for its Lean proof and the supporting definitions. A compiled statement with sorry is a proof obligation, not a completed machine-checked result.

Difficulty

The endpoint distribution may move through space as time grows, so ordinary pointwise convergence of mass functions does not capture concentration. The compact state space used by the paper permits separated clusters to live on different copies of $\mathbb Z^d$. Its distance identifies translated representatives and loses information about remote mass. A direct application of weak convergence to the event $f(x)>\varepsilon$ also fails at a threshold, because the mass-above-threshold functional is not continuous. The proof must handle its one-sided semicontinuity and the limiting behavior of the update law Bates and Chatterjee, 2021, §§2–3, 6.

Formalization scope

Lean represents sites as Fin d → ℤ and paths as finite step sequences, so the starting point, the $2d$ choices per step, and the normalization of $Z_n$ are explicit. An environment is a measurable independent family on a probability space with common law $\mathfrak L$. The unused time-zero row comes from indexing cells by $\mathbb N$; only rows with index at least one enter the polymer. The moment condition includes the full interval $[-2\beta,2\beta]$, and the disorder law must be nondegenerate. Both phase predicates refer to the canonical product environment, making the classification depend on $\mathfrak L$, $d$, and $\beta$ rather than on an arbitrary realization.

Partitioned subprobability measures are structures of nonnegative summable functions with mass at most one. Their topology is generated by the paper's distance balls. The Borel representation identifies states at distance zero, corresponding to the paper's separation quotient $\mathcal S$. Finite partial isometries carry the degree penalty $2^{-\deg\varphi}$ through an infimum over admissible degrees. The update uses an extended nonnegative sum before conversion to a real denominator. The intended probability law requires the almost-sure finiteness of that denominator and measurability of the update. The real-valued energy integrals require the stated moment condition; a default value for a nonintegrable integral cannot serve as the paper's expectation, and a non-measurable update would make the pushforward $\mathcal Tf$ the zero measure, which is not the paper's object either. The infimum $\inf_{\nu\in\mathcal K}\mathcal R(\nu)$ is taken over the set $\mathcal K$ itself, never as a real infimum whose empty inner range defaults to $0$. The intermediate results in §§3–4 and Lemma 5.1 use the standing $\beta>0$ range. Theorems 1.1 and 5.2 explicitly include $\beta=0$. Wasserstein cost imports the published RWPI.SqrtLasso.transportCost definition.

Solvers can contribute proofs of the compactness, continuity, variational-formula, invariant-law, and atom-functional milestones, or of reusable supporting results such as Lemma 2.11 (measurability of the update) and Corollary 2.5 (when $d(f,g)=0$). The strict positivity of thresholds, nondegenerate disorder, genuine probability laws, and full phase hypotheses are essential: removing any of them could make a formally easy statement unrelated to Theorem 1.1.

Selected references

• Erik Bates and Sourav Chatterjee, The endpoint distribution of directed polymers, Annals of Probability 48 (2020); preprint arXiv:1612.03443v5 (2021). Preprint.

Motivation

Two classical extremal results bound the number of edges of an $n$-vertex graph under a single restriction. Turán's theorem (1941) says that a graph with no clique on $k+1$ vertices has at most $t(n,k)$ edges, the edge count of the balanced complete $k$-partite graph. The Erdős–Gallai theorem (1959) gives the maximum number of edges of an $n$-vertex graph whose largest matching has at most $s$ edges. N. Alon and P. Frankl, Turán graphs with bounded matching number (arXiv:2210.15076v1; J. Combin. Theory Ser. B, 2024, DOI 10.1016/j.jctb.2023.12.002), combine the two restrictions. Their Theorem 1.1 determines the maximum for the clique constraint and every $n\ge 2s+1$ (mission 1 of this series). Their Proposition 3.1, the goal here, treats a whole class of forbidden graphs, the color-critical ones, when $s$ is large in terms of the forbidden graph and $n$ is large in terms of $s$.

Color-critical graphs are the natural class for exact Turán results: by a theorem of M. Simonovits (1968), for a color-critical $H$ of chromatic number $k+1$ the Turán graph $T(N,k)$ is extremal for $H$-freeness once $N$ is large. Proposition 3.1 is the analogue of Simonovits' theorem under a matching constraint.

Setting

All graphs are finite and simple. For a graph $G$, a matching is a set of pairwise disjoint edges, and the matching number $\nu(G)$ is the largest size of a matching. For a graph $H$, $G$ is $H$-free if it contains no subgraph (not necessarily induced) isomorphic to $H$. The chromatic number $\chi(H)$ is the least number of colors in a proper vertex coloring. $H$ is color-critical if it has an edge $e$ with $\chi(H-e)<\chi(H)$; examples are complete graphs and odd cycles.

The Turán graph $T(n,k)$ is the complete $k$-partite graph on $n$ vertices with classes of sizes as equal as possible; $t(n,k)$ is its number of edges. For $k\ge 2$ and $2s\le n$, the graph $G(n,k,s)$ is the complete $k$-partite graph on $n$ vertices consisting of $k-1$ classes of sizes as equal as possible whose total size is $s$, and one further class of size $n-s$. Its number of edges is $g(n,k,s)$.

In the Lean development, vertices of $G$ are Fin n; the shared objects of this series live in TuranMatching.Clique.Setting: $\nu$ is matchingNumber, $t(n,k)$ is turanNum n k (Mathlib's turanGraph), $G(n,k,s)$ is bigGraph n k s, $g(n,k,s)$ is gNum n k s, color-criticality is IsColorCritical, and the set $X$ of vertices of degree exceeding $2s$ is highDeg G s.

Formalization targets

Goal: Proposition 3.1 (p. 5)

There is $n_0:\mathbb N\to\mathbb N$ such that for every color-critical $H$ with $\chi(H)=k+1>2$ there is $s_0(H)$ with: for all $s>s_0(H)$ and $n>n_0(s)$,

$$\max\{|E(G)| : |V(G)|=n,\ G\ H\text{-free},\ \nu(G)\le s\}=g(n,k,s).$$

The maximum is stated as an upper bound for every admissible $G$ together with an admissible graph attaining $g(n,k,s)$. The thresholds $s_0$ and $n_0$ are left existential, as on the page.

Milestones (pp. 5–6)

1. $G(n,k,s)$ is $k$-colorable, $H$-free for every $H$ with $\chi(H)=k+1$, and $\nu(G(n,k,s))=s$ (for $2s\le n$).
2. If $\nu(G)\le s$ then at most $s$ vertices have degree exceeding $2s$: $|X|\le s$.
3. If every degree is at most $2s$ and $\nu(G)\le s$, then $|E(G)|\le(2s+1)s$.
4. If $\nu(G)\le s$ and $|X|<s$, then $|E(G)|<(s-1)n+2(s+1)s$.
5. $(s-1)n+2(s+1)s<g(n,k,s)$ for $n>3s^2+2s$.
6. If $\nu(G)\le s$ and $|X|=s$, then $V-X$ is independent.
7. Simonovits' theorem: an $H$-free graph on $N\ge N_0(H)$ vertices has at most $t(N,k)$ edges.
8. If $|X|=s$, $V-X$ is independent, $Z$ is disjoint from $X$ with $|Z|=\lfloor s/(k-1)\rfloor$ and $G[X\cup Z]$ has at most $t(s+\lfloor s/(k-1)\rfloor,k)$ edges, then $|E(G)|\le g(n,k,s)$.

Significance

The proposition settles, for every color-critical $H$ and large parameters, the Turán problem with a bounded matching number, and identifies the extremal graph $G(n,k,s)$, which does not depend on $H$ beyond its chromatic number. For $H=K_{k+1}$ it agrees with the large-$n$ case of Theorem 1.1 of the same paper. The structural steps (few high-degree vertices, the independence of the low-degree side) are reusable in other degree-based arguments under matching constraints.

The result is proved in the paper; none of it is formalized. The mission produces, besides the goal, two classical theorems absent from Mathlib in the forms needed here: the matching-number consequence of Vizing's theorem (milestone 3) and Simonovits' exact Turán theorem for color-critical graphs (milestone 7). Milestone 7 is a cited classical theorem, not a result of Alon and Frankl; it is posed because the proof rests on it. Mathlib currently has Turán's theorem for cliques and the Erdős–Stone–Simonovits density theorem, but not the exact result for color-critical graphs.

Difficulty

Milestones 1, 2, 4, 5, 6 and 8 are elementary counting arguments, though each requires building matchings or explicit counts in Lean. Milestone 8 contains the paper's "easy to see" isomorphism, which in Lean is an identity between two edge counts, $t(s+m,k)+(n-s-m)s=g(n,k,s)$ with $m=\lfloor s/(k-1)\rfloor$.

Milestone 3 needs Vizing's edge-coloring theorem (a graph of maximum degree $\Delta$ is properly $(\Delta+1)$-edge-colorable). A naive greedy edge coloring gives only $2\Delta-1$ colors, which bounds the edge count by about $(4s-1)s$ and is too weak for the comparison in milestones 4 and 5.

Milestone 7 is the hardest item. The density version (Erdős–Stone–Simonovits) gives $t(N,k)+o(N^2)$ edges only; the exact bound for color-critical $H$ requires Simonovits' stability method, an argument that an almost-extremal $H$-free graph is close to $T(N,k)$ followed by a cleaning step that uses the critical edge.

Formalization scope

Graphs are SimpleGraph (Fin n) with decidable adjacency; edges are counted by #G.edgeFinset. The matching number is the supremum, in $\mathbb N$, of the edge counts of matching subgraphs; the set is nonempty and bounded, so this is the true maximum and not a junk value. $g(n,k,s)$ is defined as the edge count of the graph $G(n,k,s)$, not by a closed formula. Chromatic numbers live in $\mathbb N\cup\{\infty\}$ (Mathlib's chromaticNumber), both in the definition of color-critical and in the hypothesis $\chi(H)=k+1$. $H$-freeness is Mathlib's SimpleGraph.Free (no subgraph copy). The vertex type of $H$ is any finite type in the lowest universe.

Conventions committed to:

• $k\ge 2$ is the page's $k+1>2$; it is needed because $G(n,k,s)$ has $k-1$ classes and the proof divides by $k-1$.
• Quantifier order is the page's: $n_0$ is a function of $s$ alone and is chosen before $H$; $s_0$ depends on $H$ only.
• Milestone 1 states $k$-colorability for the page's "$k$ chromatic", and carries $2s\le n$, which the page leaves implicit.
• Milestone 3 bounds edges where the page writes "the number of vertices"; the vertex count is not bounded.
• Milestone 5 uses the threshold $n>3s^2+2s$. The page's "$n$ exceeding, say, $3s^2$" is too small: for $k=2$, $s=2$, $n=13$ one has $(s-1)n+2(s+1)s=25>22=g(13,2,2)$. The goal is unaffected, since $n_0(s)$ is unspecified.
• Milestone 4 carries $s\ge 1$ so that $s-1$ is honest natural-number subtraction.

A formalization that states only the upper bound, without an attaining graph, or that places the existential $n_0$ after $s$ is fixed as a constant independent of $s$, or that defines $\nu$ or $g$ so that they take junk values, is a different and weaker statement and is ruled out.

Infrastructure that would be reusable beyond this mission: a matching-number API on Mathlib's Subgraph.IsMatching (in particular $\nu(G)\le\nu(G')$ for $G\le G'$ and the behaviour under induced subgraphs); Vizing's theorem; and Simonovits' theorem. Contributions of any of these, and of partial results toward milestone 7 (for example the case $H=C_{2\ell+1}$), are welcome.

Selected references

• N. Alon and P. Frankl, Turán graphs with bounded matching number, arXiv:2210.15076v1, 2022; J. Combin. Theory Ser. B, 2024. https://arxiv.org/abs/2210.15076, https://doi.org/10.1016/j.jctb.2023.12.002
• M. Simonovits, A method for solving extremal problems in graph theory, stability problems, in: Theory of Graphs (Proc. Colloq., Tihany, 1966), Academic Press, 1968, pp. 279–319.
• P. Erdős and T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959), 337–356. https://doi.org/10.1007/BF02024498
• P. Turán, On an extremal problem in graph theory (in Hungarian), Mat. Fiz. Lapok 48 (1941), 436–452.
• V. G. Vizing, On an estimate of the chromatic class of a p-graph, Diskret. Analiz 3 (1964), 25–30.

Motivation

Many allocation problems divide indivisible goods among agents who are entitled to different shares but cannot pay with real money: course seats among students, shifts among workers, inherited items among heirs. A standard mechanism gives each agent a budget of artificial currency and lets a market run. When budgets are equal this is the competitive equilibrium from equal incomes (CEEI) of Varian (1974), the basis of the course-allocation mechanism of Budish (2011). With indivisible items, however, an equilibrium can fail to exist: one item and two agents with equal budgets already admit none, because whoever does not get the item could afford it at any price the owner can pay.

Babaioff, Nisan and Talgam-Cohen (arXiv 2017; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) ask whether this failure is robust or a knife edge, and answer for two agents with additive preferences: an arbitrarily small, strict inequality between the budgets restores existence. Budish's approximate CEEI perturbs budgets randomly for the same reason; this mission formalizes the exact two-agent result.

Setting

A discrete Fisher market has a set $M$ of $m$ indivisible items and two agents. Agent $i$ has a valuation $v_i$ assigning a real value to every bundle $S\subseteq M$, and a budget $b_i>0$. Valuations are additive ($v_i(S)=\sum_{j\in S}v_i(\{j\})$), normalized ($v_i(M)=1$), non-negative, monotone ($v_i(S)<v_i(T)$ when $S\subsetneq T$) and strict (different bundles have different values). Budgets are normalized, $b_1+b_2=1$; money has no value to the agents.

An allocation $\mathcal S=(\mathcal S_1,\mathcal S_2)$ is a partition of all items between the agents. Item prices $p_j\ge 0$ give bundle prices $p(S)=\sum_{j\in S}p_j$. Agent $i$ demands $S$ if $p(S)\le b_i$ and $p(T)>b_i$ for every bundle $T$ with $v_i(T)>v_i(S)$. A competitive equilibrium (CE) is a pair $(\mathcal S,p)$ in which each agent demands her own bundle. An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent.

Agent $i$'s budget-proportional share is $b_i$ (her budget times $v_i(M)=1$). Her truncated share is the best value she gets in a PO allocation that gives her at most that share:

$$b_i^-=\max\{v_i(\mathcal S_i):\ \mathcal S\ \text{PO},\ v_i(\mathcal S_i)\le b_i\}.$$

The Lean development uses the same names: bundle σ i for $\mathcal S_i$, price, IsCE, IsPO, IsStandardValuation, GetsTruncatedShare.

Formalization targets

Goal: Theorem 7.1 (p. 17)

For every two-agent additive market there is $\epsilon>0$ such that every budget pair with

$$b_2<b_1\le b_2+\epsilon$$

admits a CE $(\mathcal S,p)$ in which $v_j(\mathcal S_j)\ge b_j^-$ for both agents. The goal fixes no value of $\epsilon$; it asserts only that one exists for each market.

Milestones

1. Proposition 4.1 (p. 10): for a PO allocation with non-empty bundles and budget-exhausting prices, CE is equivalent to a pairwise swap condition, Condition (1).
2. Lemma 4.3 (p. 11): a budget-exhausting combination pricing $p_j=\alpha v_1(\{j\})+\beta v_2(\{j\})$ ($\alpha,\beta\ge0$, $\max\{\alpha,\beta\}>0$) at a PO allocation is a CE.
3. Proposition 5.1 (p. 12): budget-proportional and anti-proportional PO allocations are supported in a CE.
4. Lemma 5.5 (p. 14): without budget-proportional or PO anti-proportional allocations, agent $i$'s augmented-share minimizer is agent $k$'s truncated-share maximizer.
5. Lemma 6.3 (p. 15): if the budgets avoid the finite exceptional set $R_i$ and the rectangle of allocations $T_i$ is empty, a CE with truncated shares exists.
6. Case 1 of the proof (p. 18): a CE at budgets $(\tfrac12,\tfrac12)$ remains a CE, after rescaling prices, when agent 1's budget is raised slightly.
7. $R_i$ avoidance (p. 19): almost equal but unequal budgets lie outside $R_i$.

Two companion statements are drafted without being milestones: Theorem 4.4 (second welfare theorem) and Theorem 5.2 (a budget-proportional allocation implies a CE).

Significance

The result. Theorem 7.1 shows that the non-existence of CEEI with indivisible goods is a measure-zero phenomenon for two additive agents: equal budgets are the only bad point near equality, and the equilibrium obtained is also fair in the truncated-share sense. It justifies tie-breaking by tiny budget differences in practice. It is the two-agent base case of the paper's main open question (§9.1, p. 20), whether generic almost-equal budgets guarantee a CE for more than two agents; the paper also leaves open two agents with arbitrary generic budgets and non-identical preferences (p. 21). For arbitrary, not almost-equal, budgets, Segal-Halevi (AAMAS 2018) shows that genericity does not guarantee existence for four additive agents.

Formalizing it. No machine-checked proof of any result of this paper is known. The paper's own argument for one case of the goal is incomplete: in Case 2(b) of the proof of Theorem 7.1 (p. 19) it asserts that the two candidate allocations are mirror images of each other and that the rectangles $T_1,T_2$ are empty. Both claims fail on an explicit three-item market. Theorem 7.1 itself held in every one of 6000 markets checked numerically during planning, including that one, where a CE with truncated shares exists at prices proportional to one agent's valuation. A formal proof therefore has to supply an argument the paper does not contain; the two false steps are not posed as milestones.

Difficulty

The milestones 1–5 are finite combinatorics on the Pareto frontier with sign bookkeeping. The difficulty sits in Case 2(b) of the goal: every allocation gives one agent more than $\tfrac12$ and the other less. The natural route, invoking Lemma 6.3, needs some $T_i$ to be empty, and in that case both can be non-empty. Lemma 6.3 does not cover it, and the paper's symmetry argument cannot be repaired by choosing $\epsilon$ smaller, since in the counterexample the two candidate allocations stay the same for every small $\epsilon$. A complete proof must show directly that one of the two "as fair as possible" allocations is supported by suitable prices.

Formalization scope

Items are Fin m and agents Fin 2; the paper's agents 1, 2 are indices 0, 1, so "$b_1>b_2$" reads b 1 < b 0. An allocation is a map σ : Fin m → Fin 2, which builds in that every item is allocated exactly once. All quantities are real numbers. Demand quantifies over every bundle, with strict inequality $p(T)>b_i$. Prices are non-negative by definition of a CE. The truncated share is a maximum over PO allocations only.

Two conventions are disclosed restrictions or additions:

1. Strictness without identical items. The paper allows identical items as the single exception to strict preferences (p. 6). Here each valuation is injective on bundles, so markets with identical items are excluded.
2. Rescaled prices in Case 1. The page says the perturbed CE uses unchanged prices; at normalized budgets the prices must be divided by $1+\epsilon$, and the milestone says so.

In the goal $\epsilon$ is chosen after the valuations and before the budgets. A formalization in which $\epsilon$ depends on the budgets, demand ranges over a restricted family of bundles, allocations need not allocate every item, prices may be negative, or the truncated share is a maximum over all allocations, would be a different and in several cases trivial statement; all of these are ruled out.

The definitions file GenericBudgets.AlmostEqual.Setting holds the market, CE, PO, the fairness notions, combination pricing, Condition (1), $T_i$ and $R_i$, and is reusable for any two-agent indivisible-goods market with budgets. Proofs of the milestones, a repaired argument for Case 2(b), and general $n$-agent versions of the CE and PO infrastructure are welcome.

Selected references

• M. Babaioff, N. Nisan, I. Talgam-Cohen, Competitive Equilibrium with Indivisible Goods and Generic Budgets, arXiv:1703.08150v2, 2018; Mathematics of Operations Research 46(1), 2021. https://arxiv.org/abs/1703.08150v2, https://doi.org/10.1287/moor.2020.1062
• H. R. Varian, Equity, envy, and efficiency, Journal of Economic Theory 9(1), 1974. https://doi.org/10.1016/0022-0531(74)90075-1
• E. Budish, The combinatorial assignment problem: approximate competitive equilibrium from equal incomes, Journal of Political Economy 119(6), 2011. https://doi.org/10.1086/664613
• E. Segal-Halevi, Competitive equilibrium for almost all incomes, Proceedings of AAMAS 2018, pp. 1267–1275. https://arxiv.org/abs/1705.04212

Motivation

A lower bound $K$ on the Ricci curvature of a Riemannian manifold and an upper bound $N$ on its dimension can be expressed without coordinates in two ways. The Bakry–Émery condition $\mathrm{BE}(K,N)$ is a property of the heat semigroup and its generator: the iterated carré du champ $\Gamma_2$ dominates $K\Gamma+\frac1N(\Delta f)^2$ (Bakry–Émery 1985). The Riemannian curvature-dimension conditions $\mathrm{RCD}(K,\infty)$ and $\mathrm{RCD}^*(K,N)$ are properties of a metric measure space, defined through optimal transport (Ambrosio–Gigli–Savaré 2014). A basic test for any notion of "Ricci curvature at least $K$, dimension at most $N$" is its behaviour under products: on a product of manifolds, Ricci curvature bounds combine and dimensions add.

The paper of Ambrosio, Gigli and Savaré (arXiv:1209.5786) proves that $\mathrm{BE}(K,\infty)$ and $\mathrm{RCD}(K,\infty)$ coincide on a natural class of Dirichlet-form spaces, and draws from it, in its §5.1, two tensorization results. The first (Theorem 5.1) is the stability of $\mathrm{RCD}(K,\infty)$ under products. This had been proved in Ambrosio–Gigli–Savaré 2014 only under a nonbranching assumption on the factors; the equivalence removes that assumption. The second (Theorem 5.2) is the dimensional statement: the product of two Riemannian Energy measure spaces satisfying $\mathrm{BE}(K,N_X)$ and $\mathrm{BE}(K,N_Y)$ satisfies $\mathrm{BE}(K,N_X+N_Y)$, the bound on the dimension of the product that the smooth case predicts.

Setting

Let $X$ be a complete separable metric space with a Borel measure $\mathfrak m$. A Dirichlet form is a quadratic, $L^2$-lower semicontinuous, Markovian functional $\mathcal E:L^2(X,\mathfrak m)\to[0,\infty]$ with dense domain $\mathbb V$. Its generator $\Delta_{\mathcal E}$ is defined by $\mathcal E(f,g)=-\int g\,\Delta_{\mathcal E}f\,d\mathfrak m$ for all $g\in\mathbb V$, and its heat flow $\mathsf P_t$ solves $\frac{d}{dt}\mathsf P_tf=\Delta_{\mathcal E}\mathsf P_tf$. The carré du champ $\Gamma(f)$ is the density of $\varphi\mapsto\mathcal E(f,f\varphi)-\frac12\mathcal E(f^2,\varphi)$. For $\nu=1/N\ge0$, $\mathrm{BE}(K,N)$ is the weak form (2.33) of $\Gamma_2\ge K\Gamma+\nu(\Delta f)^2$, written through the functional $\mathsf A_t[f;\varphi](s)=\frac12\int(\mathsf P_{t-s}f)^2\mathsf P_s\varphi\,d\mathfrak m$.

The intrinsic distance is $\mathsf d_{\mathcal E}(x,y)=\sup\{|\psi(y)-\psi(x)|:\psi\text{ continuous},\ \Gamma(\psi)\le1\}$. An Energy measure space (Definition 3.6) is a strongly local Dirichlet form on a space whose metric is $\mathsf d_{\mathcal E}$, with full-support measure and an exhausting function; a Riemannian Energy measure space (Definition 3.16) is in addition upper regular, and every $\psi$ with $\Gamma(\psi)\le1$ has a continuous version. An $\mathrm{RCD}(K,\infty)$ space (Definition 3.1) is a length metric measure space with the growth bounds (MD.b) and (MD.exp) on which the relative entropy has an $\mathrm{EVI}_K$ gradient flow in $(\mathscr P_2(X),W_2)$.

The product (5.1) of $(X,\mathsf d_X,\mathfrak m_X)$ and $(Y,\mathsf d_Y,\mathfrak m_Y)$ is $Z=X\times Y$ with

$$\mathsf d((x,y),(x',y'))=\sqrt{\mathsf d_X^2(x,x')+\mathsf d_Y^2(y,y')},\qquad\mathfrak m=\mathfrak m_X\times\mathfrak m_Y,$$

and the Cartesian Dirichlet form (5.2) is

$$\mathcal E(f)=\int_Y\mathcal E^X(f^y)\,d\mathfrak m_Y(y)+\int_X\mathcal E^Y(f^x)\,d\mathfrak m_X(x),$$

where $f^y=f(\cdot,y)$ and $f^x=f(x,\cdot)$.

Formalization targets

Goal: Theorem 5.2

If $(X,\mathcal E^X,\mathfrak m_X)$ and $(Y,\mathcal E^Y,\mathfrak m_Y)$ are Riemannian Energy measure spaces satisfying (MD.exp), $\mathrm{BE}(K,N_X)$ and $\mathrm{BE}(K,N_Y)$, then

$$(Z,\mathcal E,\mathfrak m)\ \text{is a Riemannian Energy measure space with}\ \mathsf d_{\mathcal E}=\mathsf d\ \text{and}\ \mathrm{BE}(K,N_X+N_Y).$$

In the parametrization $\nu=1/N$ the product satisfies $\mathrm{BE}$ with $\nu_Z=\nu_X\nu_Y/(\nu_X+\nu_Y)$.

Milestones

1. Corollary 4.18 (i), p. 58: under (MD+exp) and a quadratic Cheeger energy, the length property together with the gradient bound

$$|\mathrm D\mathsf P_tf|^2\le e^{-2Kt}\mathsf P_t(|\mathrm Df|_w^2)\tag{4.30}$$

implies $\mathrm{RCD}(K,\infty)$. 2. Theorem 5.1, p. 60: the product of two $\mathrm{RCD}(K,\infty)$ spaces is $\mathrm{RCD}(K,\infty)$. 3. The elementary inequality of p. 62: $\nu_Xa^2+\nu_Yb^2\ge\frac{\nu_X\nu_Y}{\nu_X+\nu_Y}(a+b)^2$ for positive $\nu_X,\nu_Y$ and nonnegative $a,b$. 4. Lemma 5.3, p. 62: $\Delta_Zf(x,y)=\Delta_Xf^y(x)+\Delta_Yf^x(y)$ under the fibrewise regularity (5.9), for the RCD factors and their Cheeger forms fixed in §5.1.

Significance

Theorem 5.1 shows that $\mathrm{RCD}(K,\infty)$ is closed under products with no nonbranching condition on the factors, the hypothesis under which Ambrosio–Gigli–Savaré 2014 had obtained it. Theorem 5.2 gives the dimensional version for Dirichlet-form spaces, $\mathrm{BE}(K,N_X)\times\mathrm{BE}(K,N_Y)\Rightarrow\mathrm{BE}(K,N_X+N_Y)$: a product of spaces of finite dimension has finite dimension, with the bound $N_X+N_Y$ of the smooth case, while the condition $\mathrm{BE}(K,\infty)$ alone loses all dimensional information.

Both results are proved in the paper; none of them, nor the objects they are stated for, has a machine-checked proof. The mission produces a Lean statement of the Cartesian Dirichlet form and of the product structure, the statements of the two tensorization theorems, and the characterization of $\mathrm{RCD}(K,\infty)$ that drives Theorem 5.1. A formal proof would also check the measure-theoretic steps that the paper takes for granted: the measurability of $y\mapsto\mathcal E^X(f^y)$, the Fubini arguments of Lemma 5.3, and the identification of the domain of the Cartesian form (cited from [Ambrosio–Gigli–Savaré 2014], Theorem 6.18).

Difficulty

The obvious argument works fibre by fibre: apply $\mathrm{BE}(K,N_X)$ to each section $f^y$ and $\mathrm{BE}(K,N_Y)$ to each $f^x$, and add. This fails as stated, because $\mathsf P_t$ on $Z$ does not act on the sections separately: $(\mathsf P_tf)^y$ is an average over $y'$ of the semigroup of $X$ applied to $f^{y'}$, weighted by the heat kernel of $Y$, so fibrewise gradient and Laplacian bounds have to be transported through this average. For Theorem 5.2 a second step is not fibrewise at all: before any dimensional estimate, the product has to be shown to be a Riemannian Energy measure space whose intrinsic distance is the product distance, which in the paper goes through Theorem 5.1 and hence through the equivalence $\mathrm{BE}(K,\infty)\Leftrightarrow\mathrm{RCD}(K,\infty)$ of Theorem 4.17.

Formalization scope

Functions on $X$ are X → ℝ, and $L^2$ membership is MemLp f 2 m; every object is invariant under $\mathfrak m$-a.e. equality. Dirichlet forms take values in $[0,\infty]$ and are $+\infty$ off $L^2$. Heat flows are passed as functions pinned by the predicate IsHeatSemigroup. $\Gamma(f)$ is a predicate on a density. $\mathrm{BE}(K,N)$ is parametrized by $\nu=1/N\ge0$; $\nu_Z=\nu_X\nu_Y/(\nu_X+\nu_Y)$ is $0$ when either factor has $N=\infty$. The product $Z$ is WithLp 2 (X × Y), whose metric is the $\ell^2$ distance (5.1); the plain type X × Y would carry the max-metric. The second term of (5.2) uses $\mathcal E^Y$, correcting the printed $\mathcal E^X(f^x)$. Factors are σ-finite.

Theorem 5.2 assumes (MD.exp) for both factors: its proof invokes Theorem 5.1, whose factors must be $\mathrm{RCD}(K,\infty)$, which a Riemannian Energy measure space with $\mathrm{BE}(K,\infty)$ is only under (MD.exp). In Corollary 4.18, the minimal weak gradient is written as $|\mathrm Df|_w^2=\Gamma(f)$, the identity that (QCh) asserts. Lemma 5.3 carries the RCD and Cheeger-form assumptions established at the opening of §5.1. The elementary inequality retains the printed $a,b\ge0$; applying it to signed Laplacians requires its all-real extension.

The goal is not met by stating $\mathrm{BE}$ on the product with $\nu_Z=0$: that is $\mathrm{BE}(K,\infty)$, a strictly weaker claim; nor by defining the product form through the Cheeger energy of $Z$ instead of (5.2).

A complete development needs the Cartesian form's domain theorem, a pointwise version of the heat semigroups, Theorem 4.17 of the paper and the converse $\mathrm{RCD}(K,\infty)\Rightarrow\mathrm{BE}(K,\infty)$ from [Ambrosio–Gigli–Savaré 2014]. The product layer (sections, Cartesian form, Lemma 5.3) is reusable for any tensorization argument on Dirichlet forms. Proofs of the elementary inequality and of Lemma 5.3 are the natural first contributions.

Selected references

• L. Ambrosio, N. Gigli, G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43(1), 339–404, 2015. arXiv:1209.5786v4
• L. Ambrosio, N. Gigli, G. Savaré, Metric measure spaces with Riemannian Ricci curvature bounded from below, Duke Math. J. 163(7), 1405–1490, 2014. arXiv:1109.0222
• D. Bakry, M. Émery, Diffusions hypercontractives, Séminaire de Probabilités XIX, Lecture Notes in Math. 1123, 177–206, 1985. doi:10.1007/BFb0075847

Motivation

Brands that sell consumer goods are held responsible by the public for the labour and safety practices of their suppliers. After the 2013 Rana Plaza collapse in Bangladesh, about 200 clothing brands and retailers signed the Accord on Fire and Building Safety and inspect roughly 1,600 factories jointly; pharmaceutical companies such as Pfizer and GSK audit their suppliers jointly through the Pharmaceutical Supply Chain Initiative (both examples from the paper, pp. 4 and 14). Two features of such supply bases matter for auditing. Competing brands often share a common supplier, so a scandal at that supplier hurts both of them. And brands compete downstream, so a scandal that hurts only a rival can help a brand.

Chen, Qi and Dawande (MSOM 2020; accepted manuscript SSRN 2889889) model two competing buyers with one common and two independent suppliers. Their Proposition 2 shows that, when each buyer audits on his own, competition drives the buyers away from the common supplier: in every equilibrium it is left unaudited. This mission formalizes their Proposition 3. It shows that a coalition that audits jointly, and splits the cost by a Shapley-value rule, does audit the common supplier and is stable. A companion mission (Supplier Centrality … I) covers Proposition 2.

Setting

Two buyers $B_1, B_2$ source from three suppliers: $B_i$ from its independent supplier $S_i$, and both from the common supplier $S_c$. Each supplier is compliant with probability $e\in(0,1)$. A non-compliant supplier that passes an audit of effort $x\in[0,1]$ (probability $1-x$) is exposed in public with probability $r\in(0,1]$. An independent supplier audited with effort $x$ therefore causes damage with probability $\lambda_I(x)=r(1-e)(1-x)$. The three suppliers offend independently.

If buyer $B_i$ has $n_i\in\{0,1,2\}$ exposed suppliers, its demand intercept falls from $\alpha$ to $\alpha-d_M$ (by $d_M>0$ once, however many offend). Each exposed supplier also raises its unit input cost from $w$ to $\hat w\ge w$. The buyers then play a Cournot game with differentiated products (substitution $\beta\in(0,1]$). Buyer $B_1$'s equilibrium profit is $\pi^b_1(n_1,n_2)=(q^*_1)^2$, where

$$q^*_1=\frac{2(A_1-c_1)-\beta(A_2-c_2)}{4-\beta^2},\qquad A_i=\alpha-d_M\mathbf 1\{n_i\ge1\},\quad c_i=(2-n_i)w+n_i\hat w.$$

The aggregate ex post profit is $\pi^b(i\,d_M,j\,d_M)=\pi^b_1(i,j)+\pi^b_2(i,j)$. Auditing a supplier with effort $x$ costs $K\mathbf 1\{x>0\}+\tfrac a2x^2$.

Unilateral auditing. Each buyer audits at most one of his two suppliers. $\Pi^b_i$ is buyer $B_i$'s expected profit net of his own audit costs. An equilibrium is a pair of mutual best responses in which, by the paper's tie-breaking rule, a buyer who audits strictly prefers it to not auditing. The effort $\hat e_I$ of eq. (2) is a buyer's optimal effort on his own supplier when the rival does not audit.

Joint auditing. The coalition chooses efforts $x=(e_{c1},e_{cc},e_{c2})\in[0,1]^3$ on $S_1,S_c,S_2$, auditing at most two suppliers, and pays each audited supplier's cost once. The buyers still compete downstream. With $R^b_i(x)$ the buyers' expected profits excluding audit costs, the coalition's profit is

$$\Pi^b(x)=R^b_1(x)+R^b_2(x)-\sum_{j\in\{1,c,2\}}\Big[K\mathbf 1\{e_{cj}>0\}+\tfrac a2e_{cj}^2\Big].$$

The difference of the buyers' profits is $\Delta\Pi=R^b_1-R^b_2$. The cost shares are $\Gamma_{1,2}=\tfrac12[\text{total cost}\pm\Delta\Pi]$ (eq. (3)). The analysis assumes the scenario

$$\pi^b(0,0)\ge\pi^b(d_M,0)\ge\pi^b(d_M,d_M)\ge\pi^b(2d_M,d_M)\ge\pi^b(2d_M,2d_M).$$

Formalization targets

Goal: Proposition 3

There are thresholds $K^L_c\le K^H_c$ such that, for every $K\ge0$, an optimal joint plan

$$\begin{cases}\text{audits } S_1 \text{ and } S_c,\ \Delta\Pi>0, & K<K^L_c,\\ \text{audits only } S_c,\ \Delta\Pi=0, & K^L_c\le K<K^H_c,\\ \text{audits nothing}, & K\ge K^H_c.\end{cases}$$

The coalition is also stable. At an optimal plan its aggregate profit is at least the buyers' aggregate profit in any unilateral equilibrium. After paying $\Gamma_i$, each buyer earns at least his profit in a symmetric unilateral equilibrium.

Milestones

The coalition's profit as a sum of unilateral profits (proof of Lemma OA9). Lemma OA9: $S_c$ beats one independent supplier, and beats no audit for $K<\hat K$. Lemma OA10: $S_c$ with $S_1$ beats $S_1$ with $S_2$. Lemma OA11: $S_1$ with $S_c$ beats $S_c$ alone for $K<\tilde K$. The fair shares (3). The case analysis with $K^L_c=\min\{\frac{\hat K+\tilde K}2,\tilde K\}$ and $K^H_c=\max\{\frac{\hat K+\tilde K}2,\hat K\}$. Stability.

Significance

The result separates two effects of downstream competition on responsible sourcing. Under unilateral auditing, a buyer gains nothing private from auditing the shared supplier: the reduction in risk accrues equally to his rival. The joint coalition removes this free-riding. The common supplier is audited whenever anything is, and the Shapley-type split (3) charges the buyer who also has his own supplier audited for the competitive advantage this gives him ($\Gamma_1>\Gamma_2$ exactly when $\Delta\Pi>0$). The paper's welfare comparison (Proposition 4) builds on this proposition and on Proposition 2.

The proof in the e-companion argues through four comparisons of candidate plans and short cost-sharing algebra. None of it is machine-checked. A formal proof fixes the model (in particular which costs the coalition pays and what "at most two suppliers" excludes) and checks each comparison. In one place it also corrects the printed claim: the per-firm stability argument is given only for the symmetric unilateral equilibrium, and it does not extend to the asymmetric one (see Formalization scope).

Difficulty

All objects are explicit polynomials in the efforts. The difficulty is in the comparisons. Lemmas OA9 and OA10 compare different audit plans through the scenario ordering of aggregate ex post profits, an assumption on the stage-2 closed form that is not implied by the standing conditions. The obvious attempt, comparing first-order conditions, fails because the coalition's profit is discontinuous at zero effort (the fixed cost) and the feasible set is not convex: "at most two of three" is a union of faces of the cube. The thresholds $\hat K$, $\tilde K$ are differences of maxima, so the case analysis has to handle ties and the boundary $K=K^H_c$ with weak inequalities. Stability needs the unilateral equilibria of Proposition 2, so the full goal reaches into the companion mission's game.

Formalization scope

• Model. Params holds $\alpha,\beta,w,\hat w,d_M,e,r,a$ with $\beta\in[0,1]$, $w\le\hat w$, $d_M>0$, $e\in(0,1)$, $r\in(0,1]$, $a>0$ and the three positivity conditions of p. 8. Every statement adds $\beta>0$ (Sec. 4.3 continues the competing case) and the p. 13 scenario as five inequalities between piAgg values. Their arguments count exposed suppliers: $\pi^b(2d_M,d_M)$ is a label, not a damage of $2d_M$.
• Expected profits are 8-outcome expectations of the closed-form stage-2 profit. The coalition's profit charges each audited supplier once, and the common supplier's damage probability under a joint audit is $r(1-e)(1-e_{cc})$.
• Thresholds $\hat K,\tilde K$ are the maxima at $K=0$ written as sSup over $[0,1]$ and $[0,1]^2$. At $K=0$ the profit is a polynomial, so these suprema are attained.
• "Yields the highest aggregate profit" is read as "some maximizer over the feasible plans has this pattern"; uniqueness is not claimed. $\Delta\Pi$ is evaluated at that maximizer (its mirror image, which audits $S_2$, has $\Delta\Pi<0$).
• Cost shares use the total cost of the plan. For plans with $e_{c2}=0$ they are the printed formulas (3).
• Unilateral benchmark. The equilibrium includes the tie-breaking rule of p. 10, and the interior-effort assumption of p. 10 is encoded as $\hat e_I<1$, with $\hat e_I$ given by eq. (2).
• Stability, corrected. Condition (b) of Sec. 4.3 (each firm earns more) is stated against symmetric unilateral equilibria only, the case the paper's proof treats. Against the asymmetric equilibrium, where one buyer audits with $\hat e_I$ and the other audits nothing, it fails. Take $\alpha=10$, $\beta=1$, $w=1$, $\hat w=3$, $d_M=\tfrac12$, $e=\tfrac1{10}$, $r=1$, $a=50$, $K=0.2$: the coalition optimally audits nothing, yet the auditing buyer earns more unilaterally than half of the coalition's profit. Condition (a) is stated against every equilibrium. "Higher" is stated as $\ge$.
• The goal's thresholds are existential and come before $\forall K$. Choosing $K^L_c=K^H_c$ does not trivialize it, because the three cases must cover every $K\ge0$. The milestone on part (2) fixes the thresholds explicitly.
• The source is the authors' SSRN accepted manuscript. Main-text page numbers equal PDF pages, and e-companion page ec$k$ is PDF page $28+k$.

Contributions welcome: proofs of Lemmas OA9–OA11, which are self-contained polynomial inequalities; existence of maximizers on the non-convex feasible set (upper semicontinuity); and the link to the unilateral equilibria needed for stability.

Selected references

• F. Chen, A. Qi, M. Dawande, Supplier Centrality and Auditing Priority in Socially-Responsible Supply Chains, Manufacturing & Service Operations Management, 2020; accepted manuscript, SSRN 2889889. https://ssrn.com/abstract=2889889
• E. L. Plambeck, T. A. Taylor, Supplier evasion of a buyer's audit: Implications for motivating supplier social and environmental responsibility, Manufacturing & Service Operations Management 18(2):184–197, 2016. https://doi.org/10.1287/msom.2015.0550
• N. Singh, X. Vives, Price and quantity competition in a differentiated duopoly, RAND Journal of Economics 15(4):546–554, 1984. https://doi.org/10.2307/2555525

Motivation

In the adversarial multi-armed bandit problem a learner repeatedly picks one of $K$ arms and observes only the loss of the arm it picked, while an adversary chooses the losses, possibly reacting to the learner's past choices. The minimax pseudo-regret of this problem is of order $\sqrt{KT}$ after $T$ rounds, and the classical algorithm Exp3 achieves only $\sqrt{KT\log K}$ (Auer et al., 2002). Online mirror descent with a Tsallis-entropy regularizer interpolates between Exp3 (negative Shannon entropy) and the log-barrier, and the choice of the Tsallis parameter $\alpha$ decides which logarithmic factor appears in the bound.

Timeline:

• 2002: Auer, Cesa-Bianchi, Freund and Schapire, Exp3, pseudo-regret $O(\sqrt{KT\log K})$.
• 2009: Audibert and Bubeck, the Poly-INF algorithm, the first $O(\sqrt{KT})$ adversarial bound (COLT 2009).
• 2015: Abernethy, Lee and Tewari analyse gradient-based prediction with Tsallis regularization for $\alpha\in(0,1]$ with a horizon-dependent learning rate (NeurIPS 2015).
• 2017: Agarwal, Luo, Neyshabur and Schapire analyse the log-barrier ($\alpha=0$) (COLT 2017).
• 2019/2021: Zimmert and Seldin give a single anytime analysis covering every $\alpha\in[0,1]$, Theorem 3 of arXiv:1807.07623v6 (JMLR 22(28), 2021).

Setting

There are $K\ge1$ arms and rounds $t=1,2,\dots$. At round $t$ the learner draws an arm $I_t$ from a probability vector $w_t$ in the simplex $\Delta^{K-1}$, the adversary fixes a loss vector $\ell_t\in[0,1]^K$, which may depend on $I_1,\dots,I_{t-1}$ and on the adversary's internal randomization, and the learner observes $\ell_{t,I_t}$. The pseudo-regret is

$$\overline{Reg}_T=\mathbb E\Big[\sum_{t=1}^T\ell_{t,I_t}\Big]-\min_i\mathbb E\Big[\sum_{t=1}^T\ell_{t,i}\Big],$$

with the expectation over both sources of randomness.

The importance-weighted (IW) estimator is $\hat\ell_{t,i}=\mathbb 1(I_t=i)\,\ell_{t,i}/w_{t,i}$ and $\hat L_{t}=\sum_{s\le t}\hat\ell_s$. For $\alpha\in(0,1)$ and $\xi_i>0$ the α-Tsallis regularizer is

$$\Psi(w)=-\sum_i\frac{w_i^\alpha-\alpha w_i}{\alpha(1-\alpha)\xi_i},\qquad\Psi_t=\Psi/\eta_t ,$$

with symmetric regularization $\xi_i=1$. α-Tsallis-INF is online mirror descent:

$$w_t=\arg\max_{w\in\Delta^{K-1}}\ \langle w,-\hat L_{t-1}\rangle-\Psi_t(w),$$

and the potential is $\Phi_t(Y)=\max_{w\in\Delta^{K-1}}\langle w,Y\rangle-\Psi_t(w)$. The pseudo-regret splits into a stability term $\mathbb E[\sum_t\ell_{t,I_t}+\Phi_t(-\hat L_t)-\Phi_t(-\hat L_{t-1})]$ and a penalty term $\mathbb E[\sum_t\Phi_t(-\hat L_{t-1})-\Phi_t(-\hat L_t)-\ell_{t,i^*_T}]$, where $i^*_T$ is a best arm in expectation in hindsight. Theorem 3 uses the learning rate

$$\eta_t=\sqrt{\frac{K^{1-2\alpha}-K^{-\alpha}}{1-\alpha}\cdot\frac{1-t^{-\alpha}}{\alpha t}} .$$

Formalization targets

Goal: Theorem 3, $\alpha\in(0,1)$

$$\overline{Reg}_T\le2\sqrt{\min\Big\{\frac{1}{\alpha-\alpha^2},\frac{\log K}{\alpha},\frac{\log T}{1-\alpha}\Big\}KT}+1\qquad\text{for every }T\ge1 .$$

The goal fixes the constants of the paper; it holds against every randomized adaptive adversary.

Milestones

1. Lemma 11 part 1: the per-round stability is at most $\min\{\sum_i\frac{\eta_t\xi_i}{2}\mathbb E[w_{t,i}]^{1-\alpha},1\}$.
2. The maximum of $\sum_i z_i^{1-\alpha}$ over the simplex is $K^\alpha$.
3. Lemma 20: the penalty is bounded by increments of the inverse learning rate times differences of $\Psi$, plus $\langle u-e_{i^*_T},L_T\rangle$.
4. Lemma 12 part 1: for non-increasing positive learning rates the penalty is at most $\frac{(K^{1-\alpha}-1)(1-T^{-\alpha})}{(1-\alpha)\alpha\eta_T}+1$.
5. Lemma 14: $(1-y^{-x})/x$ is non-increasing on $x>0$, tends to $\log y$, and is at most $\min\{x^{-1},\log y\}$.

Companions

Theorem 3 at the boundaries: $\alpha=1$ (negative-entropy regularizer, rate $\lim_{\alpha\to1}\eta_t=\sqrt{\log(K)(1-t^{-1})/(Kt)}$, bound $2\sqrt{\log(K)KT}+1$) and $\alpha=0$ (log-barrier, rate $\sqrt{(K-1)\log(t)/t}$, bound $2\sqrt{\log(T)KT}+1$).

Significance

Theorem 3 gives one anytime bound for the whole Tsallis family. At $\alpha=\tfrac12$ it is $O(\sqrt{KT})$, the minimax rate, without knowledge of $T$; at $\alpha\to1$ it recovers the Exp3 rate and at $\alpha\to0$ the log-barrier rate, with constants matching Abernethy et al. without tuning the learning rate to the horizon. It is the adversarial half of the paper's study of α-Tsallis-INF, whose stochastic half (Theorem 4) shows why $\alpha=\tfrac12$ is the only value that is optimal in both regimes.

The result is proved in the paper. As far as is known, no machine-checked proof of any Tsallis-INF or Poly-INF regret bound exists. The mission produces a formal model of randomized adaptive adversaries together with online mirror descent for bandits, and formal stability and penalty lemmas for the Tsallis family, which are the standard building blocks of later best-of-both-worlds analyses.

Difficulty

The obvious route, bounding the regret of each fixed seed and action sequence and averaging, fails: the IW estimates have second moments of order $1/w_{t,i}$, which are unbounded, and only their expectation under the learner's own sampling is controlled. The stability term therefore has to be bounded in expectation, for a regularizer whose convex conjugate has no closed form for general $\alpha$. The penalty term involves a learning rate that changes every round, so the potentials of consecutive rounds are not directly comparable. The expectation of the run is over a law that couples the adversary's seed with the learner's random actions, so every step that the paper writes as "take expectations" has to be carried out over that law.

Two features of the printed proof need care. Theorem 3's learning rate is $0$ at $t=1$, where $\Psi_1=\Psi/\eta_1$ is undefined, and for small $\alpha$ it increases between $t=2$ and $t=3$, while Lemma 12 part 1 assumes a non-increasing sequence of positive learning rates. A complete proof of the goal has to handle these first rounds.

Formalization scope

Arms are Fin K with $K\ge1$; action sequences are maps $h:\mathbb N\to$ Fin K with $h(t)=I_t$ and $h(0)$ unused. The adversary is a seed $\omega$ drawn from a probability measure $\mu$ together with one published RegretBandits.Adversarial.Adversary K per seed (losses in $[0,1]$, depending on past actions only), with losses measurable in the seed. The expectation of a quantity at horizon $T$ is $\int\sum_{a}(\prod_{t\le T}w_{t,a_t})F\,d\mu$. The learner's weights are an argmax predicate on a weight function: for every round, the objective $\eta_t\langle w,-\hat L_{t-1}\rangle-\Psi(w)$ is maximized over the simplex. This is the paper's rule whenever $\eta_t>0$, and at $\eta_1=0$ it makes $w_1$ the minimizer of $\Psi$, the uniform vector, which is the initialisation of online mirror descent. No hypothesis on the weights is added beyond this rule. $\Phi_t$ is a real supremum over the simplex, attained because the simplex is compact and nonempty. Powers are real powers; $\log$ is the natural logarithm.

The goal and the milestones take $\alpha\in(0,1)$ (the page: $\alpha\in[0,1]$); the boundary values are separate companion theorems, with the limiting regularizers of §3.2 and the limiting learning rates of p. 12, and the log-barrier companion restricts the weights to the open simplex. Lemmas 12 and 20 are stated, as on the page, for any loss estimator that is conditionally unbiased given the seed and the past, depends on the actions through its own round only, and is measurable and integrable under the run law. The page prints the $\alpha\to1$ limit of the learning rate as $\sqrt{\log(K)(1-t^{-1})/t}$; the true limit carries an extra factor $1/K$ under the root, and the $\alpha=1$ companion uses the true limit. In Lemma 20 the term $\langle u-e_{i^*_T},L_T\rangle$ sits inside the expectation, since $L_T$ is random under an adaptive adversary.

A trivializing formalization is ruled out: the weights are not chosen by a choice function, and an algorithm whose weights are arbitrary at $\eta_1=0$ is excluded because the predicate pins $w_1$.

A complete development needs: convex conjugates of separable regularizers on the simplex, the stability argument via a second-order bound, telescoping of potentials, unbiasedness of IW estimators under the run law, and elementary real-analysis estimates (Lemma 14, the simplex maximum). The run law, the IW estimator and the potential are reusable in the companion missions on Theorem 1 and Theorem 4. Contributions to any milestone, and to reusable lemmas about the run law, are welcome.

Selected references

• J. Zimmert, Y. Seldin, Tsallis-INF: An Optimal Algorithm for Stochastic and Adversarial Bandits, J. Mach. Learn. Res. 22(28), 2021; arXiv:1807.07623v6. https://arxiv.org/abs/1807.07623
• J. Abernethy, C. Lee, A. Tewari, Fighting Bandits with a New Kind of Smoothness, NeurIPS 2015. https://arxiv.org/abs/1505.00340
• A. Agarwal, H. Luo, B. Neyshabur, R. E. Schapire, Corralling a Band of Bandit Algorithms, COLT 2017. https://arxiv.org/abs/1612.06246
• J.-Y. Audibert, S. Bubeck, Minimax Policies for Adversarial and Stochastic Bandits, COLT 2009. https://www.learningtheory.org/colt2009/papers/024.pdf
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM J. Comput. 32(1), 2002. https://doi.org/10.1137/S0097539701398375