Probability

Motivation

Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed $\pm 1$ so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.

Timeline

• 1963. Steinitz-type vector balancing questions circulate; Bárány and Grinberg later (1981) show any norm admits a dimension-dependent bound $2d$, setting the theme: how much of the dependence on dimension is real?
• 1981. Beck and Fiala (Discrete Appl. Math.) prove degree-$t$ set systems have discrepancy at most $2t - 1$, by the floating-colors argument, and conjecture $O(\sqrt{t})$.
• 1980s. Komlós poses the vector form — unit $\ell^2$-norm columns, constant $\ell^\infty$ discrepancy — which implies the Beck–Fiala conjecture; it circulates through Spencer's Ten Lectures (1987) as the central open problem of the area.
• 1985. Spencer (Trans. AMS) proves "six standard deviations suffice": discrepancy $6\sqrt{n}$ for $n$ sets on $n$ points, beating random signing via the partial-coloring method.
• 1998. Banaszczyk (Random Struct. Algorithms) proves the Komlós bound $O(\sqrt{\log n})$ by a recursive Gaussian-measure argument over convex bodies.
• 2010–2016. The constructive era: Bansal (2010) makes Spencer algorithmic by SDP random walks, Lovett and Meka (2012) simplify, and Bansal, Dadush, and Garg (STOC 2016) give a polynomial-time algorithm matching Banaszczyk's bound.
• 2023. Kunisky (SIAM J. Discrete Math.) constructs instances from unsatisfiable formulas with discrepancy approaching $1+\sqrt{2}$ — the strongest lower bound on the conjectured constant.
• 2025. Bansal and Jiang (arXiv:2508.03961) break the Banaszczyk barrier: $\tilde{O}((\log n)^{1/4})$ for Komlós, and the Beck–Fiala conjecture resolved for $t \ge \log^2 n$ — the first movement in nearly thirty years. The gap between $2.414\ldots$ and $\tilde{O}((\log n)^{1/4})$ is the conjecture.

Setting

Fix $n$ vectors $v_1, \dots, v_n \in \mathbb{R}^m$ with Euclidean norm $\lVert v_i \rVert_2 \le 1$. A sign vector is an $\varepsilon \in \{-1, +1\}^n$: one sign $\varepsilon_i \in \{\pm 1\}$ per vector. Writing $v_{ij}$ for the $j$-th coordinate of the vector $v_i$, the discrepancy of the family under $\varepsilon$ is the largest coordinate, in absolute value, of the signed sum $\sum_i \varepsilon_i v_i$ — that is, $\max_{j \le m} \lvert \sum_{i \le n} \varepsilon_i v_{ij} \rvert$, the $\ell^\infty$ norm of the signed sum. The Komlós property at constant $K$ — KomlosBound K — says that every such family, in every $n$ and every $m$, admits a sign vector with every coordinate of the signed sum at most $K$ in absolute value.

Set systems embed as the special case of $0/1$-incidence matrices: if $A$ is an $m \times n$ matrix of $0$s and $1$s in which every column has at most $t$ ones (every element lies in at most $t$ sets), the columns scaled by $1/\sqrt{t}$ have norm at most one, so the Komlós property gives discrepancy $K\sqrt{t}$ — the Beck–Fiala conjecture.

Formalization targets

Goal — the Komlós conjecture

$$\exists\, K \in \mathbb{R}: \quad \text{every } v_1, \dots, v_n \in \mathbb{R}^m \text{ with } \lVert v_i\rVert_2 \le 1 \text{ admits } \varepsilon \in \{\pm 1\}^n \text{ with } \max_j \Big|\sum_i \varepsilon_i v_{ij}\Big| \le K.$$

The goal fixes no value of $K$: any finite universal constant settles it, so the statement survives every improvement in the constant.

Milestones — the known ladder

Eight results over the same definitions: Beck–Fiala's $2t - 1$ for degree-$t$ set systems; Spencer's $6\sqrt{n}$ for $n$ sets on $n$ points; Banaszczyk's $O(\sqrt{\log n})$ for the Komlós setting; its corollary $O(\sqrt{t \log n})$ for set systems; the reduction "Komlós at $K$ implies Beck–Fiala at $K\sqrt{t}$"; Kunisky's lower bound $K \ge 1 + \sqrt{2}$; and the two 2025 Bansal–Jiang breakthroughs — $\tilde{O}((\log n)^{1/4})$ for the Komlós setting, and the Beck–Fiala conjecture's bound $O(\sqrt{t})$ in the regime $t = \Omega(\log^2 n)$.

Significance

The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.

None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.

Difficulty

Random signs lose: they give $\Theta(\sqrt{n})$, not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below $2t - O(1)$ by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at $\sqrt{\log n}$ by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least $1 + \sqrt{2}$ — so any proof must handle instances strictly harder than the set-system case.

Formalization scope

The Lean model commits to: vectors as EuclideanSpace ℝ (Fin m), whose norm is the $\ell^2$ norm (the hypothesis $\lVert v_i \rVert \le 1$ reads ‖v i‖ ≤ 1); the $\ell^\infty$ conclusion written coordinatewise as ∀ j, |∑ i, ε i * v i j| ≤ K, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with ε i = 1 ∨ ε i = -1; and set systems as matrices A : Fin m → Fin n → ℝ with an entrywise $0/1$ hypothesis and column-degree counted by Set.ncard. Quantifier order matters everywhere: in KomlosBound K the constant is fixed before $n$ and $m$ — a $K$ depending on $n$ would make the statement the trivial $\sqrt{n}$ bound. In beck_fiala the hypothesis $t \ge 1$ is required (the degree-$0$ system has discrepancy $0 > 2t-1$ otherwise); the Banaszczyk-form bounds use $\log(n+2)$ so that the bound is positive already at $n \le 1$. In the Bansal–Jiang milestones the asymptotic $\tilde{O}$ and $\Omega$ are rendered by existential constants quantified before all instances: the hidden $\mathrm{poly}(\log\log n)$ factor becomes $(\log\log(n+8))^{\gamma}$ for some fixed $\gamma > 0$ (the inner shift $+8$ keeps the iterated logarithm positive), and the threshold $t = \Omega(\log^2 n)$ becomes $C_0 \log^2(n+2) \le t$ for some fixed $C_0 > 0$.

Welcome contributions: any milestone in any order — beck_fiala and komlos_implies_beck_fiala are self-contained finite arguments and the natural entry points; spencer_six_deviations and banaszczyk_bound each import a major technique; komlos_lower_bound needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.

Selected references

• J. Beck, T. Fiala, "Integer-making" theorems, Discrete Applied Mathematics 3 (1981). doi:10.1016/0166-218X(81)90022-6
• J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985). doi:10.1090/S0002-9947-1985-0784009-0
• W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998). doi link
• N. Bansal, D. Dadush, S. Garg, An algorithm for Komlós conjecture matching Banaszczyk's bound, FOCS 2016 / SIAM J. Comput. arXiv:1605.02882
• N. Bansal, H. Jiang, Decoupling via affine spectral-independence: Beck–Fiala and Komlós bounds beyond Banaszczyk, 2025. arXiv:2508.03961
• D. Kunisky, The discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant, SIAM J. Discrete Math. 37 (2023). arXiv:2111.02974
• B. Chazelle, The Discrepancy Method, Cambridge University Press, 2000. author's page

Motivation

An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to $+\infty$ with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout policy to maximize the expected discounted dividends paid before ruin. This is the optimal dividend problem. It is one of the basic stochastic control problems of actuarial mathematics and corporate finance, and it serves as a test case for singular control of processes with jumps.

The classical answer is a barrier strategy: pay out whatever lifts the surplus above a level $a$ and nothing else. Jeanblanc and Shiryaev (1995) proved this optimal when the surplus is a Brownian motion with drift, and Gerber and Shiu studied the same Brownian setting. Azcue and Muler (2005) showed that it can fail in the Cramér–Lundberg model, where the optimal policy may be a band strategy. Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007) 156–180) treated a general spectrally negative Lévy process, a process with stationary independent increments and only downward jumps. They found the value of every barrier strategy in closed form through the scale function of the process and identified the best barrier level $c^*$. They also gave a verification condition under which the barrier at $c^*$ is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.

Setting

Let $X=(X_t)_{t\ge0}$ be a spectrally negative Lévy process on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ with $X_0=0$ and Lévy triplet $(c,\sigma,\nu)$. Its Laplace exponent is $\psi(\theta)=\log\mathbf E[e^{\theta X_1}]$, finite for $\theta\ge0$:

$$\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}\bigl(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}}\bigr)\nu(dy).$$

Increments after time $s$ are independent of $\mathcal F_s$. Initial capital $x$ is added to $X$. The standing assumptions are the following: $X$ does not have monotone paths, $\mathbf E[X_1]>-\infty$, and either $\sigma>0$, $\int_{(-1,0)}|y|\,\nu(dy)=\infty$, or $\nu$ has a density.

A dividend strategy is a nondecreasing, left-continuous, adapted process $L$ with $L_0=0$. The risk process is $U_t=x+X_t-L_t$ and the ruin time is $\sigma^L=\inf\{t\ge0:U_t<0\}$. The strategy is admissible ($L\in\Pi$) if no lump sum exceeds the current reserves. Its value is

$$v_L(x)=\mathbf E\Bigl[\int_0^{\sigma^L}e^{-qt}\,dL_t\Bigr],\qquad v_*(x)=\sup_{L\in\Pi}v_L(x),$$

with discount rate $q>0$. For $C\in[0,\infty]$, $\Pi_{\le C}$ consists of the admissible strategies that keep $U_t\le C$ for $t>0$.

The $q$-scale function $W=W^{(q)}$ is the unique continuous nondecreasing function on $[0,\infty)$ with $\int_0^\infty e^{-\theta y}W(y)\,dy=1/(\psi(\theta)-q)$ for large $\theta$. It is extended by $W=0$ on $(-\infty,0)$. The barrier strategy $\pi_a$ reflects $x+X$ at the level $a$, paying $(x-a)^+$ at time $0$. The paper computes its value

$$v_a(x)=\frac{W(x)}{W'(a)}\ (0\le x\le a),\qquad v_a(x)=x-a+\frac{W(a)}{W'(a)}\ (x>a),$$

and the optimal barrier level is $c^*=\inf\{a>0: W'(a)\le W'(x)\ \forall x>0\}$, read as $0$ when this set is empty and $W'(0+)\le W'(x)$ for all $x>0$. The generator is

$$\Gamma f(x)=\tfrac{\sigma^2}{2}f''(x)+cf'(x)+\int_{(-\infty,0)}[f(x+y)-f(x)-f'(x)y\mathbf 1_{\{|y|<1\}}]\,\nu(dy).$$

Formalization targets

Goal: Theorem 2 (p. 14)

Assume $\sigma>0$, or $X$ has bounded variation, or $v_{c^*}\in C^2(0,\infty)$. Then $c^*<\infty$ and:

$$\text{(i)}\quad \pi_{c^*}\in\Pi_{\le c^*},\qquad v_{\pi_{c^*}}(x)=v_{c^*}(x)=\sup_{\pi\in\Pi_{\le c^*}}v_\pi(x)\quad(x\ge0);$$ $$\text{(ii)}\quad (\Gamma v_{c^*}-qv_{c^*})(x)\le0\ \ \forall x>c^*\ \Longrightarrow\ v_*(x)=v_{c^*}(x)\ (x\ge0),\ \ \pi_*=\pi_{c^*}.$$

The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.

Milestones

• Proposition 1 (p. 7): $v_{\pi_a}(x)=W(x)/W'(a)$ for $a>0$, $x\in[0,a]$.
• Lemma 2(i) (p. 15): $c^*<\infty$.
• Proposition 3(i) (p. 15): $v_a(x)\le v_{c^*}(x)$ for $x\in[0,c^*]$, $a\ge0$.
• Lemma 3(i) (p. 16): $v_{c^*}'(x)\ge1$ for $x>0$.
• Proposition 4(i) (p. 18): a $C^2$ (unbounded variation) or $C^1$ (bounded variation) solution $w$ of $\max\{\Gamma w-qw,1-w'\}=0$ on $(0,C)$ dominates $\sup_{\Pi_{\le C}}v_\pi$.
• Lemma 4 (p. 20): $(\Gamma v_{c^*}-qv_{c^*})(x)=0$ on $(0,c^*)$ when $c^*>0$.

Significance

The theorem gives an explicit solution to a singular control problem for a general Lévy model. The candidate value function and barrier level are expressed through one special function, $W^{(q)}$, and optimality over all strategies reduces to one inequality on $(c^*,\infty)$. It is the basis of the later literature on scale-function methods in dividend problems (Loeffen 2008, Kyprianou–Rivero–Song 2010, and the refracted and Parisian variants). Part (i) holds with no condition on the Lévy measure. Part (ii) shows exactly where barrier optimality can fail.

The paper's proofs use fluctuation identities (exit problems, excursion theory) and Itô's formula for semimartingales with jumps. None of these is in Mathlib. As far as is known, none of these results has been machine-checked. A formalization would produce a Lévy-process and scale-function layer, a formal model of singular control with jumps and lump-sum payments, and a checked verification argument. Each of these can be reused beyond this paper.

Difficulty

The analytic part is elementary once the value formula (5.1) is available: the choice of $c^*$, Proposition 3(i) and Lemma 3(i) follow from the shape of $W'$. The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for $X$. Those identities rest on excursion theory, or on the martingale property of $e^{-qt}W(X_t)$ up to exit. The verification step, Proposition 4(i), needs Itô's formula for $w(U_t)$. Here $U$ is a jump process controlled by a left-continuous finite-variation process that may itself jump. The change-of-variables formula must also run under only $C^1$ regularity when $X$ has bounded variation. Just proving that $\Gamma w-qw\le0$ and $w'\ge1$ imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of $X$ enter the Itô expansion separately and must each be bounded.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a structure carrying the triplet $(c,\sigma,\nu)$ and pathwise càdlàg paths with only downward jumps. It also carries independence of increments from the filtration and stationarity. Its law is fixed by the Laplace transform $\mathbf E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$. The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument $W$ (it is unique). $W'(0+)$ is an extended real, since it is $+\infty$ for unbounded variation without a Gaussian part.

Values of strategies and value functions lie in $[0,\infty]$. The dividend integral is a Lebesgue–Stieltjes integral over $[0,\sigma^L)\cup\{0\}$: it counts the lump sum at time $0$ and excludes a payment at the ruin instant.

Several conventions are fixed, and each is disclosed in the item it affects:

• Admissibility. The paper requires $L_{t+}-L_t<U_t$. The formalization uses $\le$, because the paper's own strategy of paying out everything at once needs it.
• Barrier level (5.2). Printed over $a>0$ and "all $x$", the defining set is empty for Brownian motion with nonpositive drift. The printed set (with $x>0$) is kept whenever it is nonempty; when it is empty and $W'(0+)\le W'(x)$ for all $x>0$ — the second alternative in the proof of Lemma 2(i) — $c^*=0$, and otherwise $c^*=\infty$.
• Printed slips. The integral $\int_{-1}^0 x\,\nu(dx)$ in (3.3) is read as $\int|x|\,\nu(dx)$. In (3.4), $e^{-\theta x}$ is read as $e^{-\theta y}$, and in Theorem 2(i), $\pi^*_c$ is read as $\pi_{c^*}$.
• Proposition 4(i) is stated for initial capital $x\le C$. Beyond $C$, $w$ is unconstrained and the printed claim fails.
• Lemma 4 carries the smoothness proviso of Theorem 2 on $(0,c^*)$.

A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and $c^*<\infty$ is a conclusion.

A complete development needs:

• Lévy processes and their Laplace exponents;
• scale functions and the exit identity $\mathbf E_x[e^{-qT}\mathbf 1_{\{X_T=a\}}]=W(x)/W(a)$;
• reflected processes;
• Itô's formula for jump semimartingales with finite-variation controls.

The Lévy and scale-function layer is shared with the companion mission on the bail-out problem. Contributions of general lemmas (Stieltjes integration by parts, optional stopping for càdlàg martingales) are welcome.

Selected references

• F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
• P. Azcue, N. Muler, Optimal reinsurance and dividend distribution policies in the Cramér–Lundberg model, Math. Finance 15 (2005) 261–308.
• M. Jeanblanc-Picqué, A. N. Shiryaev, Optimization of the flow of dividends, Russian Math. Surveys 50 (1995) 257–277.
• R. L. Loeffen, On optimality of the barrier strategy in de Finetti's dividend problem for spectrally negative Lévy processes, Ann. Appl. Probab. 18 (2008) 1669–1680.
• A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

Motivation

Distributionally robust optimization evaluates a decision against a set of plausible probability laws rather than against a single estimated law. A common way to specify that set is to choose a nominal law $P_0$ and allow every law $P$ whose discrepancy from $P_0$ is below a radius $\varepsilon$. Different discrepancies produce different ambiguity sets, so comparing them tells a modeler what one constraint guarantees about another. Rahimian and Mehrotra collect such constructions in their survey and state a chain of comparisons among variation, Hellinger, Kullback–Leibler, and J-divergences in Lemma 5.4 (arXiv:1908.05659v1, pp. 31, 34–35). The chain connects four common ways of controlling model error without requiring a finite outcome space or a common density chosen in advance.

The source is the 2019 arXiv v1 preprint of a survey. Its proof of Lemma 5.4 cites earlier work rather than giving a full derivation. The preprint also prints an additional J-to-$\chi^2$ comparison that is false; this mission isolates the part that holds for every pair of probability measures. The distinction matters when an ambiguity set is used to certify a bound under a different divergence: an inclusion based on the false link can certify laws that are outside the intended set.

Setting

Let $(\Xi,\mathcal F)$ be a measurable space, and let $\mathfrak M(\Xi,\mathcal F)$ be its probability measures. Given $P_1,P_2\in\mathfrak M(\Xi,\mathcal F)$, a $\phi$-divergence $\mathfrak D^\phi(P_1,P_2)$ compares their densities using a function $\phi:[0,\infty)\to[0,\infty]$ with $\phi(1)=0$. The paper assumes $\phi$ is convex. To account for measures that are not mutually absolutely continuous, take the common dominating measure $\nu=P_1+P_2$ and write $p=dP_1/d\nu$ and $q=dP_2/d\nu$. The integrand is $q\phi(p/q)$ when $q>0$ and $p\phi'(\infty)$ when $q=0$, where $\phi'(\infty)=\lim_{t\to\infty}\phi(t)/t$; a point with $p=q=0$ contributes zero (§5.1.2, p. 31).

Table 1 gives four generators used here:

$$\phi_v(t)=|t-1|,\qquad \phi_h(t)=(\sqrt t-1)^2,\qquad \phi_{\mathrm{kl}}(t)=t\log t-t+1,\qquad \phi_j(t)=(t-1)\log t.$$

The first two divergences are the full $L^1$ variation discrepancy and the unhalved squared Hellinger discrepancy. In particular, $\mathfrak D^{\phi_v}=2d_{\mathrm{TV}}$, where $d_{\mathrm{TV}}$ is the total variation distance defined later in the paper. The J generator has $\phi_j(0)=+\infty$, understood as its limit at zero; $\phi_{\mathrm{kl}}(0)=1$ under $0\log0=0$. The recession slopes of the four generators, in the displayed order, are $1,1,+\infty,+\infty$ (Table 1, p. 31; §5.1.3, p. 35).

For a nominal probability measure $P_0$ and a nonnegative radius $\varepsilon$, equation (5.9) defines the ambiguity ball

$$\mathcal P^\phi(P_0;\varepsilon) =\{P\in\mathfrak M(\Xi,\mathcal F):\mathfrak D^\phi(P,P_0)\le\varepsilon\}.$$

Formalization targets

The three milestone comparisons are the valid initial part of (5.10), for every $P,P_0\in\mathfrak M(\Xi,\mathcal F)$:

$$\frac14\bigl(\mathfrak D^{\phi_v}(P,P_0)\bigr)^2 \le\mathfrak D^{\phi_h}(P,P_0) \le\mathfrak D^{\phi_{\mathrm{kl}}}(P,P_0) \le\mathfrak D^{\phi_j}(P,P_0).$$

The middle comparison is also stated in footnote 18. The mission goal is the corrected Lemma 5.4: it joins these three comparisons to the resulting valid part of (5.11), for every nominal $P_0$ and radius $\varepsilon$:

$$\mathcal P^{\phi_j}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_{\mathrm{kl}}}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_h}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_v}(P_0;2\sqrt\varepsilon).$$

Each inclusion has the direction induced by the preceding divergence inequality: a stronger divergence constraint gives a smaller ball. The first comparison retains the paper's factor $1/4$, and the final ball retains its radius $2\sqrt\varepsilon$ (Lemma 5.4, p. 34).

Significance

The result allows a J-divergence or KL-divergence ambiguity model to carry a simultaneous bound in Hellinger and full variation divergence. A Hellinger radius $\varepsilon$ yields the explicit variation radius $2\sqrt\varepsilon$; this makes the scale change visible when comparing two models built with different discrepancies. Without a general-measure statement, a finite-outcome approximation does not itself cover continuous laws or pairs with a singular component.

The paper presents the inequalities as known and cites sources for them. A finite-alphabet TV–Hellinger–KL chain and a general-measure KL–affinity bound already have machine-checked results in the platform catalog. The work here is to formalize the four generators with one shared general-measure divergence, close the remaining inequalities in that representation, and connect them to the ambiguity-ball inclusions. This also provides reusable definitions for other distributionally robust models that use the same divergence convention.

Difficulty

Writing the density ratio only with respect to $P_0$ loses the part of $P$ singular to $P_0$. That would change both variation and Hellinger divergence and make the stated chain an unreliable comparison of the paper's objects. At the opposite boundary, $P$ can vanish on a set that $P_0$ charges. There the J generator must be infinite, although a direct use of a total real logarithm at zero can assign it an incorrect finite value. These two edge cases make an apparently routine pointwise comparison insufficient for the full measurable-space theorem.

Formalization scope

Lean represents $P$ and $P_0$ as ProbabilityMeasure Ξ on an arbitrary MeasurableSpace Ξ. It computes Radon–Nikodym densities relative to $P+P_0$, evaluates the divergence with an extended nonnegative Lebesgue integral, and represents both divergence values and radii in ENNReal. The generic definition computes the recession slope as a limsup; for the four Table 1 generators this is the limit in the paper. The formal ambiguity ball contains probability measures only. A top radius is allowed by the type; the finite nonnegative radii are the paper's intended model parameters. The generic operation does not take a convexity certificate, but the four named generators are the only ones used in the theorem.

The formalization must not turn a nondominated pair into divergence zero or assign $\phi_j(0)=0$: either choice changes the claimed chain. It must also retain the full variation divergence, without the half factor used for total variation distance. The definitions of the common-measure divergence, its four generators, and the ambiguity ball are intended for reuse. Contributions establishing properties of the recession slopes, comparison lemmas on arbitrary measurable spaces, and their ambiguity-set consequences are within scope.

The paper's final inequality in (5.10), $\mathfrak D^{\phi_j}\le\mathfrak D^{\phi_{\mathrm{ca}^2}}$, and the associated first inclusion in (5.11) are removed. They are false even on a two-point space: with $P_0=(1/2,1/2)$ and $P=(0,1)$, J-divergence is $+\infty$ while the order-two $\chi$-divergence is $1$. Thus $P$ lies in the latter ball of radius $1$ but outside the J ball of that radius. The source's footnote 18 separately notes an error in a cited Hellinger–KL comparison; the corrected Hellinger–KL inequality is retained (pp. 34–35).

Selected references

• H. Rahimian and S. Mehrotra, Distributionally Robust Optimization: A Review, arXiv preprint arXiv:1908.05659v1, 2019. Preprint.

Motivation

Every generalization bound presented so far in this series is for classification, where the error of a prediction is binary (correct or not). Regression asks a different question: predictions are real-valued, and error is measured by the magnitude of the deviation from the true label, via a loss function L. Chapter 11 develops generalization theory for bounded regression, showing that the same two complexity measures used for classification — Rademacher complexity and a VC-dimension analogue — extend naturally, once the loss function itself is folded into the machinery via a Lipschitz-contraction argument (Rademacher route) or a reduction to classification via level-set thresholding (pseudo-dimension route).

Setting

A regression hypothesis h:X→ℝ is scored by a loss L:ℝ×ℝ→ℝ against a joint distribution D on X×ℝ (the stochastic scenario, since regression labels are rarely exactly reproducible); R(h) = E_{(x,y)~D}[L(h(x),y)] (Eq. 11.1) and R̂_S(h) = (1/m)∑L(h(x_i),y_i) (Eq. 11.2). For a finite hypothesis set, Theorem 11.1 gives a Hoeffding/union-bound guarantee directly, the regression analogue of chunk 02-pac's finite-hypothesis bound. For infinite H, §11.2.2 develops a Rademacher-complexity route: Proposition 11.2 shows that if L is µ-Lipschitz in its first (predicted-value) argument, the Rademacher complexity of the loss-composed family G = {(x,y)↦L(h(x),y) : h∈H} is controlled by µ times H's own Rademacher complexity, via Talagrand's contraction lemma (chunk 05-svm's Lemma 5.7); Theorem 11.3 combines this with chunk 03's Theorem 3.3 to give the chapter's headline bound. §11.2.3 develops an independent, purely combinatorial route: pseudo-dimension (Definition 11.5), a real-valued analogue of VC-dimension defined via threshold-witnessed shattering (Definition 11.4, restated via its own Eq. 11.3 as the VC-dimension of a thresholded indicator family); Theorem 11.8 gives a pseudo-dimension generalization bound by reducing regression to a family of classification problems (one per threshold t), using the tail-integral identity Eq. 11.5.

Formalization targets

Theorem 11.1 (milestone). For L bounded by M and H finite: for any δ>0, with probability at least 1-δ, for all h∈H: R(h) ≤ R̂_S(h) + M√((log|H|+log(1/δ))/(2m)).

Proposition 11.2 (milestone). For L non-negative, bounded by M, µ-Lipschitz in its first argument: for any sample S, R̂_S(G) ≤ µR̂_S(H).

Theorem 11.3 — the mission's goal. Under Proposition 11.2's hypotheses on L: for any δ>0, with probability at least 1-δ, for all h∈H: E[L(h(x),y)] ≤ (1/m)∑L(h(x_i),y_i) + 2µR_m(H) + M√(log(1/δ)/(2m)), and also with 2µR̂_S(H) + 3M√(log(2/δ)/(2m)).

Theorem 11.8 (milestone). For Pdim(G)=d, L non-negative bounded by M: for any δ>0, with probability at least 1-δ over a sample of size m, for all h∈H: R(h) ≤ R̂_S(h) + M√(2d log(em/d)/m) + M√(log(1/δ)/(2m)).

Significance

Theorem 11.3 is the chapter's own choice of headline result (§11.2's stated goal is to show "how the Rademacher complexity bounds of theorem 3.3 can be used to derive generalization bounds for regression"), and its proof genuinely reuses two pieces of prior machinery from this series — chunk 03's Theorem 3.3 and chunk 05's Talagrand's-lemma-style contraction — combined via a new observation (Proposition 11.2) specific to loss-composed families, not a restatement of either. Theorem 11.8 is the chapter's second, structurally independent technique: its em/d bound parallels chunk 03's Corollary 3.19 (both ultimately reduce to a VC-dimension-style growth-function argument), but the reduction itself — regression to a continuum of threshold classification problems, via the Lebesgue-integral tail identity Eq. (11.5) applied to |R(h)-R̂_S(h)| — is genuinely new content for this book, and pseudo-dimension has no prior art on the platform or in Mathlib. No prior art exists for this chapter's overall content either: GET /theorems?q=generalization%20bound%20regression and GET /theorems?q=pseudo-dimension both return zero hits.

Difficulty

Proposition 11.2's proof needs Talagrand's contraction lemma applied with the Lipschitz constant taken in the first argument of L only — the predicted value h(x_i), holding the true label y_i fixed — exactly the pitfall BRIEF.md names: a loss Lipschitz in the wrong argument, or in both arguments jointly, would not license this step. Theorem 11.8's proof is the chapter's most involved: it defines, for every h∈H and threshold t≥0, a classifier c(h,t):(x,y)↦1_{L(h(x),y)>t}, bounds |R(h)-R̂_S(h)| by M·sup_{t∈[0,M]}|R(c(h,t))- R̂_S(c(h,t))| via the tail-integral identity, and then applies a VC-dimension-style classification bound (Corollary 3.19) to the family of thresholded classifiers — whose VC-dimension is, by Eq. (11.3), exactly Pdim(G) by construction. A formalization that conflated pseudo-dimension with ordinary VC-dimension, or reused chunk 03's HasVCDim definition by relabeling, would misrepresent this chapter's genuinely different (real-valued, threshold-witnessed) combinatorial notion — precisely the pitfall BRIEF.md flags.

Formalization scope

Y := ℝ throughout (the book's own "Y a measurable subset of ℝ"), a harmless simplification consistent with every hypothesis, loss and Lipschitz condition in this chapter being stated for real-valued scores and labels. EmpiricalRademacherComplexity/ RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2 locally, since a draft item cannot import another chunk's draft module. Shatters/PseudoDim are formalized via the book's own equivalent reformulation (Eq. 11.3, the thresholded-indicator form), rather than the sign-function form of Definition 11.4 directly, since the two coincide except at a measure-zero boundary the book itself does not address; PseudoDim mirrors chunk 03's HasVCDim Prop-valued pattern (does not cover Pdim(G)=+∞; every consuming theorem takes it as an explicit hypothesis) but is a structurally distinct definition built on Shatters, never a relabeling of HasVCDim, per BRIEF.md's pitfall note. Proposition 11.2's and Theorem 11.3's Lipschitz hypothesis (hLlip) is stated with the true label y' universally quantified outside the two-point comparison y1, y2 (the predicted values), matching "for any fixed y' ∈ Y, y ↦ L(y,y') is µ-Lipschitz" exactly — Lipschitzness in the first argument only, per BRIEF.md's pitfall note. RademacherComplexity (Measure.map Prod.fst D) H m gives the book's R_m(H) (H's Rademacher complexity under the marginal sampling distribution of the inputs x, i.e. D's first marginal). No numerical constant is altered from the book in any of the four theorems.

Not formalized: the L_p-loss worked example following Theorem 11.3's proof (an instantiation of the general theorem for a specific loss family, not a separate numbered theorem); Theorem 11.6 and Theorem 11.7 (worked pseudo-dimension examples for hyperplanes and vector spaces, background/illustration rather than the chapter's general machinery — drafting only these examples instead of the general Theorem 11.8 would be this chapter's trivializing formalization); the two-sided variant of Theorem 11.1 mentioned immediately after its proof (an unnumbered remark, not a separately displayed/numbered theorem); and all of §11.3 (linear regression, kernel ridge regression, SVR, Lasso and their online variants), which is applications-heavy per BRIEF.md's chapter restriction to §11.1-11.2.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 11 (§11.1-11.2).
• D. Haussler, "Decision theoretic generalizations of the PAC model for neural net and other learning applications," Information and Computation 100(1), 1992 (pseudo-dimension's origin).
• D. Pollard, Convergence of Stochastic Processes, Springer, 1984 (the tail-integral identity Eq. 11.5's classical antecedent).

Motivation

Banks lend to one another, and the shape of the resulting network decides how a loss at one bank reaches the others. A long line of work, starting with Allen and Gale (2000) and continued by Acemoglu, Ozdaglar and Tahbaz-Salehi (2015), compares the ring network, where each bank is owed money by one neighbour, with the complete network, where every bank holds an equal share of every other bank's debt. That literature studies contagion after shocks hit and finds that the complete network spreads losses thinly and can absorb small shocks better.

Shu's paper (Management Science, doi:10.1287/mnsc.2022.01519) asks the ex-ante question: when banks choose how much risk to take, knowing the network they sit in, which network makes them take more? A successful bank subsidizes its failed counterparties through the clearing of interbank debt, and anticipating that subsidy pushes it toward riskier projects. Proposition 4 of the paper says that this effect is stronger in the complete network. This mission formalizes that proposition and the computation behind it.

Setting

There are $N\ge2$ banks. In a regular network with share matrix $\Theta=[\theta_{ij}]$, bank $j$ owes bank $i$ the face value $\theta_{ij}\bar d$, every bank has total interbank liability $\bar d>0$, and every bank also owes a senior deposit $v>0$. The two networks of Definition 3 are

$$\Theta^R:\ \theta_{ij}=1 \text{ iff } j\equiv i-1 \pmod N,\qquad \Theta^C=\tfrac{1}{N-1}\big(\mathbb 1_{N,N}-I_N\big).$$

Each bank $i$ chooses a project $Z_i$ in a common interval $[\underline Z,\overline Z]$. The project pays $Z_i$ with probability $P(Z_i)$ and $0$ otherwise, independently across banks. Assumption 1 requires $P(Z)\in(0,1)$, $P$ decreasing, and $P(Z)\,Z$ concave. The standing assumption $\underline Z\ge v+\bar d$ says a successful bank never defaults.

After the state $\omega\in\{s,f\}^N$ is realized, interbank payments clear. A payment equilibrium is a vector $d$ with

$$d_i=\Big\{\min\Big[\textstyle\sum_j\theta_{ij}d_j+e_i-v,\ \bar d\Big]\Big\}^+,$$

where $e_i=Z_i$ if bank $i$ succeeds and $0$ if it fails. Bank $i$'s profit is $\big(\sum_j\theta_{ij}d^*_j+e_i-v-d^*_i\big)^+$. A risk-taking equilibrium is a profile $Z^*$ in which each $Z^*_i$ maximizes bank $i$'s expected profit given $Z^*_{-i}$. Equilibria need not be unique, and the paper selects the least one.

The key quantity is the network risk-taking distortion

$$\mathcal D_i(Z_{-i})=\sum_{\omega_{-i}}\Big(\bar d-\sum_j\theta_{ij}d^*_j(\omega^{i=s})\Big)\Pr(\omega_{-i}),$$

which is bank $i$'s expected net interbank payment to the other banks when its own project succeeds. In a regular network, expected profit equals $P(Z_i)(Z_i-v)-P(Z_i)\,\mathcal D_i(Z_{-i})$, so $\mathcal D_i$ acts like extra debt that the bank repays only when it succeeds. Superscripts $C$ and $R$ mark the complete and ring networks.

Formalization targets

Goal: Proposition 4

With $Z^C$ the least equilibrium of the complete network and $Z^R$ the least equilibrium of the ring,

$$Z^R_i\le Z^C_i\qquad\text{for every bank } i.$$

Milestones

1. Clearing in the complete network (IA p. 15): a failed bank pays $\big(\bar d-\frac{N-1}{S}v\big)^+$, where $S$ is the number of successful banks.
2. (I.13): with $q$ the common success probability of the other banks and $\Pr(m)=\binom{N-1}{m}(1-q)^mq^{N-1-m}$,

$$\mathcal D^C_i=\sum_{m=1}^{N-1}\min\Big(\frac{mv}{N-m},\frac{m\bar d}{N-1}\Big)\Pr(m).$$

3. (I.14): in the ring, a failed bank pays $(\bar d-K_iv)^+$, where $K_i$ counts the consecutive failed banks upstream of $i$, starting with $i$ itself.
4. (I.15): the conditional distribution, given $m$ failures, of what a successful bank receives in the ring.
5. Closed form of $\mathcal D^R_i$ (IA p. 16, also p. 14).
6. Lemma I.A (ii): $\sum_{l=r}^n\binom lr(n-l)=\binom{n+1}{r+1}\frac{n-r}{r+2}$. Part (i), the classical hockey-stick identity, is already published and proved on the platform and is included by reference.
7. Lemma I.B: $\sum_i A_i^+\ge(\sum_iA_i-B)^++B$ whenever $B<\max_iA_i$.
8. $\mathcal D^R_i\le\mathcal D^C_i$ when all other banks choose the same project.

Significance

The result. Proposition 4 reverses the conventional reading of the complete network as the safer structure. The co-insurance that makes it resilient after a shock is the same cross-subsidy that weakens incentives before the shock. Two networks with the same face-value liabilities $\bar d+v$ therefore induce different equilibrium risk-taking. Liabilities alone are not a sufficient statistic for risk incentives, and the network topology matters in its own right. The same comparison is the template for the paper's later results on the number of banks and on central clearing.

Formalizing it. The proposition is proved in the paper, not open, and none of it is machine-checked yet. A formal proof must establish the two clearing vectors, the counting identity behind (I.15), and the two closed forms of the distortion. The printed argument also leaves a step to be supplied: its final appeal to "the monotone selection theorem" needs the distortion comparison at every profile of the other banks. It is proved only when they all choose the same project, and it is false in general. The goal is nevertheless stated for least equilibria exactly as in the paper, and its formal proof has to bridge that gap. The milestones are true as stated.

Difficulty

The distortion of the ring is not a function of the number of failures alone. What a successful bank receives depends on the length of the run of failed banks immediately upstream of it, so the closed form needs an exact count of the binary strings with a given number of failures and a given initial run length. The comparison of the two distortions is not termwise either: the positive part sits inside a sum on the ring side and outside it on the complete side.

The obvious final step is to say that the distortion is larger in the complete network, and that a larger distortion raises the optimal risk exposure. That step does not go through as stated. The equilibrium comparison needs control of the best-response maps at every profile, while the distortion comparison holds only on the diagonal, where all other banks choose the same project. Some further structure of the two games is needed to restrict attention to that diagonal.

Formalization scope

Banks are Fin N with $N\ge2$, and states are Fin N → Bool with true meaning success. The paper's general model is specialized to a regular network given by $(\Theta,\bar d,v)$, which covers both networks of Definition 3. Every expectation is a finite sum over the $2^N$ states, so no measure theory is involved. The payment equilibrium $d^*$ is the greatest solution of the clearing system, because the paper asserts only generic uniqueness. Every bank's project lies in $[\underline Z,\overline Z]$, and $\underline Z\ge v+\bar d$ is a hypothesis of every statement.

The distortion milestones (2, 5 and 8) are stated at the constant profile in which every bank chooses the same $z$, which is how the page's single $P(Z_{-i})$ reads. At $m=N-1$, where every other bank fails, the printed ring binomial has lower index $-1$, and the weight is fixed explicitly to $1$ at $l=N-1$. Proposition 4 is stated for least equilibria and weak inequality. It adds one hypothesis the page does not state, continuity of $P$ on $[\underline Z,\overline Z]$, so that best responses and least equilibria exist. Without it the IsLeast hypotheses could be unsatisfiable and the goal vacuous.

Trivializing encodings are ruled out: $d^*$ is an actual solution of the clearing system, not a junk supremum, and the run length $K_i$ is only used in states where some bank succeeds.

A complete development needs Knaster–Tarski on the box $[0,\bar d]^N$, the clearing computations for the two networks, binomial identities, and a monotone comparative statics argument for the equilibria. Published Topkis results on supermodular games (existence of least equilibria, and monotonicity of least fixed points in a parameter) are included by reference as tools. The clearing and counting lemmas are reusable for the paper's other results on ring and complete networks. Proofs of any milestone, and of the goal, are welcome.

Not posed here: Proposition 1 (strategic complementarity in any network, a separate mission), Proposition 2 (existence), and the later comparative statics in the number of banks, central clearing and bailouts.

Selected references

• C. Shu, Endogenous Risk Exposure and Systemic Instability, Management Science (accepted manuscript, 17 Sep 2024). https://doi.org/10.1287/mnsc.2022.01519
• F. Allen and D. Gale, Financial Contagion, Journal of Political Economy 108(1), 2000. https://doi.org/10.1086/262109
• D. Acemoglu, A. Ozdaglar and A. Tahbaz-Salehi, Systemic Risk and Stability in Financial Networks, American Economic Review 105(2), 2015. https://doi.org/10.1257/aer.20130456
• L. Eisenberg and T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2), 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Motivation

Demand, prices and click-through rates often follow seasonal cycles: weekly, monthly, yearly. A decision maker who repeatedly chooses among options whose expected payoffs repeat in time faces a non-stationary multi-armed bandit. Chen, Wang and Wang (arXiv:2005.08088v4, Operations Research, 2025) study the model in which each arm's mean reward is periodic with its own unknown period. They give a two-stage policy whose regret is $\tilde O(\sqrt{T\sum_k T_k})$, and a lower bound showing that no policy, even one told the periods, does better than $\Omega(\sqrt{T\max_k T_k})$. This mission formalizes that lower bound, Theorem 3 of the paper. A companion mission of the same series covers the upper bound.

Lower bounds of this kind fix what is achievable. For the stationary $K$-armed bandit, the minimax regret is of order $\sqrt{TK}$ (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020, Ch. 15). In the periodic model a learner effectively faces $\sum_k T_k$ "effective arms" (arm $k$ at each phase of its cycle), which suggests the rate $\sqrt{T\sum_k T_k}$. The paper proves the weaker but general bound $\sqrt{T\max_k T_k}/(32e)$, which matches the upper bound up to a factor $\sqrt K$ and logarithms.

Setting

There are $K \ge 2$ arms and epochs $t = 1, \dots, T$. An instance $\nu$ is a family of mean rewards $\mu_{k,t}$. If arm $k$ is pulled at epoch $t$, the reward is drawn from the Gaussian law $\mathcal N(\mu_{k,t}, 1)$, independently of the past given the arm.

A sequence $f$ has minimum period $p \ge 1$ if $f(t+p) = f(t)$ for all $t \ge 1$ and no smaller positive integer has this property.

A policy $\pi$ chooses the arm $\pi_t$ at epoch $t$ at random, from a distribution that depends on the previous arms and rewards. Its expected regret on $\nu$ is display (1) of the paper:

$$\mathbb E_\nu[R^\pi_T] = \sum_{t=1}^T\Big(\max_k \mu_{k,t} - \mathbb E[\mu_{\pi_t,t}]\Big).$$

Three classes of instances appear, all with unit-variance Gaussian rewards and means in $[0,1]$ (Assumption 1):

1. $\mathcal E_1$: every arm is stationary;
2. $\mathcal E_2(T_1)$: the first arm's mean has minimum period $T_1$, the other arms are stationary;
3. $\mathcal E_3(T_1,\dots,T_K)$: arm $k$'s mean has minimum period $T_k$.

The proof compares instances through the metric (B-48),

$$\mathcal M(\nu_1,\nu_2) = \Big(\sum_{k=1}^K\sum_{p=1}^{T_k}\big(\mu^{(\nu_1)}_{k,p} - \mu^{(\nu_2)}_{k,p}\big)^2\Big)^{1/2}.$$

The periods satisfy Assumption 3 with the parameters (7): with $n = \lfloor\sqrt{T/K}\rfloor$ and $g = \lceil\sqrt n\rceil$, $T > 4K$, $g \ge 2$ and $T_k < n/(2g)$ for every $k$.

Formalization targets

Goal: Theorem 3 (p. 24)

For every policy $\pi$ there is $\nu \in \mathcal E_3(T_1,\dots,T_K)$ with

$$\mathbb E_\nu[R^\pi_T] \ge \frac{1}{32e}\sqrt{T\max_k T_k}.$$

Milestones

1. Lemma 12 (p. 23). Stationary Gaussian bandits whose arms other than the first have known mean $1/2$: every policy has regret at least $\sqrt T/(8\sqrt2 e)$ on some choice of $\mu_1 \in [0,1]$.
2. Lemma 13 (p. 23). One periodic arm: every policy has regret at least $\sqrt{TT_1}/(16e)$ on some instance of $\mathcal E_2(T_1)$ whose other arms have mean $1/2$.
3. Fact 1 (proof of Theorem 3, p. 48). $\mathcal E_3$ is dense in $\mathcal E_2 \cup \mathcal E_3$ under $\mathcal M$: an instance of $\mathcal E_2(T_1)$ can be perturbed on the arms other than the first into an instance of $\mathcal E_3(T_1,\dots,T_K)$ at $\mathcal M$-distance less than any $\delta > 0$.
4. Fact 2 (proof of Theorem 3, p. 48). The regret $f_\pi(\nu) = \mathbb E_\nu[R^\pi_T]$ is continuous in $\nu$ on $\mathcal E_2 \cup \mathcal E_3$ for $\mathcal M$, uniformly in $\pi$.

Significance

Theorem 3 shows that knowing the periods does not remove the cost of learning them phase by phase: the regret must grow like $\sqrt{T\max_k T_k}$, not like $\sqrt{TK}$. Together with the paper's upper bound $\tilde O(\sqrt{T\sum_k T_k})$ and the inequality $\sqrt{T\max_k T_k} \ge \sqrt{T\sum_k T_k}/\sqrt K$, it shows the two-stage policy is near-optimal when $K$ is fixed. The intermediate results are reusable: Lemma 12 is a clean two-point Gaussian lower bound, Lemma 13 is a phase-decomposition argument that applies to any bandit model with known cyclic structure, and facts 1 and 2 give a continuity framework for the regret as a function of the instance.

The result has a published proof. As far as the platform's records show, none of it has been machine-checked. The stationary minimax lower bound of Lattimore and Szepesvári (a different family and constant) exists on the platform, together with the Bretagnolle–Huber inequality, the Gaussian KL divergence and the divergence decomposition, which this mission lists as tools.

Difficulty

The two-point argument of Lemma 12 is standard, but its constant needs $\Delta = \sqrt{1/(2T)} < 1/2$, so small horizons must be handled separately. Lemma 13 decomposes the problem into $T_1$ phase problems; making this rigorous means showing that a policy on the periodic problem induces, on each phase, a policy on a stationary problem of horizon $\lfloor T/T_1\rfloor$, with a history law that factorizes accordingly. The phase-wise instances produced by the decomposition need not have minimum period exactly $T_1$ (all phases may coincide), so a perturbation is needed to land in $\mathcal E_2(T_1)$; the constant has slack for it. Fact 2 asks for continuity of an integral against the law of a $T$-round adaptive process, uniformly over all policies, which needs a domination argument that does not depend on the policy's kernels.

Formalization scope

• Arms are Fin K, 0-based: the paper's first arm is index $0$. Epochs are 1-based natural numbers; history coordinate $i$ is epoch $i+1$. Values of the means at $t = 0$ are ignored.
• A policy is the platform's BanditAlgorithm.BanditPolicy K: one Markov kernel per round from the history to the next arm. The history law periodicMeasure reuses the platform's step kernel with the Gaussian bandit of the current epoch's means; with constant means it is BanditAlgorithm.banditMeasure of BanditAlgorithm.gaussianBandit. Lemma 12 is stated with the platform's banditRegret, $T\mu^* - \mathbb E[\sum_t X_t]$, which equals (1) for Gaussian arms; the other statements use (1) directly.
• Assumption 1 is stated on epochs $1,\dots,T$. Minimum periods are exact.
• Every lower bound has the order "for every policy there is an instance", with the instance in the class, so the policy may depend on $K$, $T$ and the periods; this is the paper's "policy that knows $T_k$". The supremum over the class is replaced by an attained instance, which is the stronger form.
• Added hypotheses, all disclosed: $K \ge 2$ (with one arm the regret is $0$); $T_k \ge 1$ (the paper's $T_k \in \mathbb N^+$); in Lemmas 12 and 13, the means of the arms other than the first are $1/2$, which is how "a policy that knows $\mu_k$ for $k \ge 2$" is read (with arbitrary known values the printed lemmas fail). Assumption 3 with (7) is the standing assumption of Appendix B.4.
• A statement with the quantifiers in the order "there is an instance for every policy", without the $[0,1]$ clause, or without exact minimum periods, would be false or trivial; none of these is the target.

Welcome contributions: the bridge between periodicMeasure with constant means and banditMeasure, the phase decomposition of the history law, and the uniform continuity of the regret in the means.

Selected references

• N. Chen, C. Wang, L. Wang, Learning and Optimization with Seasonal Patterns, Operations Research, 2025; arXiv:2005.08088v4, 2021. https://arxiv.org/abs/2005.08088v4
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401
• 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

Motivation

When many independent users share a network, each routes its own traffic to minimize its own delay, and nobody optimizes the system as a whole. Koutsoupias and Papadimitriou asked how much this lack of coordination can cost: how far the social cost of a Nash equilibrium can be from the social optimum, in the worst case. Their paper Worst-case equilibria (STACS 1999; journal version 2009, doi:10.1016/j.cosrev.2009.04.003) introduced this ratio, later named the price of anarchy, and studied it on the simplest network: parallel links between one source and one destination. The ratio has since become a standard measure of the inefficiency of equilibria in routing, scheduling and auctions (see Chapters 17–20 of Nisan, Roughgarden, Tardos and Vazirani, Algorithmic Game Theory, 2007).

Most of the paper concerns links of equal capacity. Its last result, Theorem 4, turns to two links of different speeds and shows that unequal speeds make equilibria worse: the worst-case ratio rises from $3/2$ for two identical links to the golden ratio $\varphi=(1+\sqrt5)/2\approx1.618$.

Timeline. 1999: Koutsoupias and Papadimitriou define the coordination ratio; for two identical links they prove it is exactly $3/2$, and for two links with speeds they give the golden-ratio lower bound of Theorem 4. 2002–2003: Mavronicolas and Spirakis, Koutsoupias, Mavronicolas and Spirakis, and Czumaj and Vöcking determine the asymptotic order of the price of anarchy for $m$ identical and for $m$ related links (Czumaj–Vöcking, ACM TALG 2007).

Setting

There are $n$ agents and $m$ parallel links. Agent $i$ has an amount of traffic $w_i>0$, and link $j$ has a speed $s_j>0$. A pure profile $a=(a_1,\dots,a_n)$ sends each agent's whole traffic over one link $a_i$. The load of link $j$ is $L_j(a)=\sum_{k:\,a_k=j}w_k$, and an agent on link $j$ experiences the delay $L_j(a)/s_j$.

A mixed strategy of agent $i$ is a probability distribution $(p_i^1,\dots,p_i^m)$ over the links; the agents randomize independently. The expected cost of agent $i$ is its expected delay. A profile $p$ is a Nash equilibrium if no agent can lower its expected cost by changing its own distribution. The expected traffic on link $j$ is $M^j=\sum_i p_i^jw_i$, and the cost to agent $i$ of placing its traffic on link $j$ is

$$c_i^j=\frac{M^j+(1-p_i^j)\,w_i}{s_j}. \tag{8}$$

The social cost of $p$ is the expected makespan, the expected maximum delay over the links,

$$\operatorname{cost}(p)=\sum_a\Big(\prod_i p_i^{a_i}\Big)\max_j\frac{L_j(a)}{s_j},$$

and $\operatorname{opt}=\min_a\max_j L_j(a)/s_j$ is the optimal makespan over pure assignments. The price of anarchy is the largest ratio $\operatorname{cost}(p)/\operatorname{opt}$ over instances and equilibria.

Formalization targets

Goal: Theorem 4 (PDF p. 6)

For two links with speeds $0<s_1\le s_2\le\varphi s_1$, there is an instance with positive traffic and a Nash equilibrium $p$ with $\operatorname{opt}>0$ and

$$\operatorname{cost}(p)=R\cdot\operatorname{opt},\qquad R=1+\frac{s_2}{s_1+s_2};$$

moreover $R\le\varphi$ on this range, and $R=\varphi$ when $s_2=\varphi s_1$.

Milestones

1. (8): the expected delay of a pure deviation is $c_i^j=(M^j+(1-p_i^j)w_i)/s_j$.
2. Support property (§2, applied with speeds): at an equilibrium each agent puts positive probability only on links minimizing $c_i^j$, and its expected cost is $c_i=\min_jc_i^j$.
3. For $s_1\le s_2$, the probabilities $p_1^1=s_1^2/(s_2(s_1+s_2))$ and $p_2^1=1-s_2^2/(s_1(s_1+s_2))$ lie in $[0,1]$ if and only if $s_2\le\varphi s_1$.
4. With $w_1=s_2$, $w_2=s_1$, this profile is a Nash equilibrium.
5. Its social cost is $(s_1+2s_2)/(s_1+s_2)$.
6. The instance has $\operatorname{opt}=1$.
7. $R\le\varphi$, with equality at $s_2/s_1=\varphi$.

Significance

The result. Theorem 4 shows that the price of anarchy of parallel links depends on the heterogeneity of the links, not only on their number: two identical links have price of anarchy $3/2$ (Theorems 1 and 3 of the paper), while two links of different speeds already reach $\varphi$. The setting is that of related (uniformly related) machines, the model in which Czumaj and Vöcking later proved the asymptotic order of the price of anarchy for $m$ links.

Formalizing it. The result is proved on paper; this mission produces a machine-checked proof. Beyond the theorem, it yields reusable statements about mixed equilibria of load-balancing games on the published agt_games vocabulary: the closed form (8) of a pure deviation's expected cost and the support characterization of equilibria, both stated for any number of agents and links. A search of the Prove2Me catalog (October 2026) found no formalization of any part of this result.

Difficulty

The arithmetic of the instance is elementary, so the work lies in connecting the paper's computations to the definitions. The paper's notion of equilibrium quantifies over all mixed deviations, and its expected costs are sums over all $m^n$ pure profiles; the proof reasons instead with the per-link costs $c_i^j$ of (8) and the indifference of each agent between the links it uses. Turning that into a proof requires showing that an agent's expected cost is the $p_i$-weighted average of the $c_i^j$ (linearity over independent randomization) and that the average over $2^2$ outcomes reduces to the paper's four-term formula. A naive approach that checks only pure deviations does not give the equilibrium property directly; one must pass from pure to mixed deviations. The restriction $s_2\le\varphi s_1$ is not cosmetic: beyond it the second agent's probability is negative.

Formalization scope

The game is defined in WorstCaseEq.Speeds.Model on top of the published agt_games definitions (AGT.IsMixedNash, AGT.expectedPayoff, AGT.profileProb). These maximize payoffs, so an agent's payoff is minus its delay. Agents and links are Fin n and Fin m, indexed from $0$, so the paper's links 1, 2 and agents 1, 2 are 0, 1. A mixed profile is a real matrix p i j; being a family of probability distributions is part of the Nash condition. Makespan, social cost and opt require at least one link (NeZero m).

The paper does not print the social cost for links with speeds; the computation in the proof of Theorem 4 uses the expected maximum of load divided by speed, and that is the definition. It is not the maximum of the expected loads, a smaller quantity. The page numbers cited are PDF page indices of the journal version (dated April 29, 2009), which prints no page numbers after page 1.

"The price of anarchy is at least $R$" is formalized as the existence of an instance and an equilibrium whose social cost equals $R$ times a positive optimum. A quotient $\operatorname{cost}/\operatorname{opt}$ is avoided because it takes the junk value $0$ when $\operatorname{opt}=0$, and the requirement $\operatorname{opt}>0$ rules out degenerate witnesses with no traffic. The ratio conditions $s_2/s_1\le\varphi$ and $s_2/s_1=\varphi$ are written $s_2\le\varphi s_1$ and $s_2=\varphi s_1$ (equivalent since $s_1>0$), and $\varphi$ is Mathlib's Real.goldenRatio.

Contributions welcome: proofs of any milestone. Milestones 1 and 2 are general facts about mixed equilibria of weighted load-balancing games and are reusable beyond this mission.

Selected references

• E. Koutsoupias and C. Papadimitriou, Worst-case equilibria, STACS 1999, LNCS 1563, pp. 404–413, doi:10.1007/3-540-49116-3_38; journal version, Computer Science Review 3(2), 2009, pp. 65–69, doi:10.1016/j.cosrev.2009.04.003.
• A. Czumaj and B. Vöcking, Tight bounds for worst-case equilibria, ACM Transactions on Algorithms 3(1), 2007, doi:10.1145/1186810.1186814.
• N. Nisan, T. Roughgarden, É. Tardos and V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 20, doi:10.1017/CBO9780511800481.

Motivation

The multi-armed bandit problem asks how to share effort sequentially among several independent projects, each of which evolves only while it is worked on. It models the scheduling of jobs on a single machine, the order in which to explore candidate sites, sequential clinical trials and the allocation of research effort among competing projects. Before 1972 the problem had no general solution: dynamic programming over the joint state of all projects is intractable as soon as there are more than a few of them.

J. C. Gittins and D. M. Jones (1974) announced, and Gittins (1979) set out in full, a solution of a striking form: each project can be assigned a number depending only on its own current state, its dynamic allocation index (DAI, now the Gittins index), and it is optimal to work on a project whose index is largest.

Timeline. Gittins and Jones presented the index result at the European Meeting of Statisticians in 1972 (proceedings 1974). Gittins (1979) gave the general discrete-time formulation, stated the Forwards Induction Theorem and the DAI Theorem without proof, and proved the attainment Lemma of its Section 4. Whittle (1980) gave a dynamic-programming proof through the retirement formulation, Weber (1992) the prevailing-charge interchange argument, and Tsitsiklis (1994) a short inductive proof. Gittins, Glazebrook and Weber (2011) is the standard monograph; Lattimore and Szepesvári (2020, Chapter 35) give a measure-theoretic treatment on general state spaces.

Setting

A bandit process $D$ is a Markov chain $x(0), x(1), \dots$ on a measurable state space $\Theta$ with transition kernel $P$. Applying the continuation control at process time $t$ earns the discounted reward $a^t R(x(t))$, with $0<a<1$, and moves the chain one step; the freezing control leaves the state unchanged and earns nothing. For a stopping time $\tau$ of the chain (possibly infinite) write

$$R_\tau(D,x)=E\Big\{\sum_{t=0}^{\tau-1}a^tR(x(t))\,\Big|\,x(0)=x\Big\},\qquad W_\tau(D,x)=E\Big\{\sum_{t=0}^{\tau-1}a^t\,\Big|\,x(0)=x\Big\}.$$

The dynamic allocation index of $D$ in state $x$ is the largest reward per unit of discounted time obtainable by continuing for at least one step:

$$\nu(D,x)=\sup_{\tau>0}\nu_\tau(D,x),\qquad \nu_\tau(D,x)=\frac{R_\tau(D,x)}{W_\tau(D,x)}. \tag{2}$$

A simple family of alternative bandit processes consists of $k$ bandit processes. At each stage $n=0,1,2,\dots$ a policy chooses exactly one of them to continue, possibly at random and as a function of the whole past; the others are frozen. A policy is optimal if it attains the supremum of the total expected discounted reward over all policies.

The Lean development uses the published objects markovChainMeasure P x (the chain law), IsPositiveStoppingTime, stoppedRatio P r α τ x ($\nu_\tau$), gittinsIndex P r α x ($\nu$), MarkovBanditPolicy k S, markovBanditMeasure P π x n (the law of the first $n$ stages) and markovBanditDiscountedValue P r α π x (the total expected discounted reward), with $a$ written α and $R$ written r.

Formalization targets

Goal: the DAI Theorem (Section 3, p. 154)

For every policy $\pi$ and initial state vector $x$,

$$V_\pi(x)=\sup_{\pi'}V_{\pi'}(x)\iff \forall n,\ \text{a.s. under the play of }\pi\text{ from }x:\ \ \pi_n\Big(\big\{i:\nu(x_i(n))=\max_j\nu(x_j(n))\big\}\Big)=1 .$$

Milestones

1. Section 4, Lemma (p. 154). For $\Theta_0=\{y:\nu(D,y)<\nu(D,x)\}$ and $\tau$ the first $t\ge1$ with $x(t)\in\Theta_0$,

$$\nu_\tau(D,x)=\nu(D,x).$$

2. The "if" half of the DAI Theorem. A policy that selects a process of maximal index on every history is optimal: the published BanditAlgorithm.gittins_index_theorem, already Proved.
3. Section 4, Corollary 1 (p. 155). For the $M$-horizon index $\nu^M(D,x)=\sup_{0<\tau\le M}\nu_\tau(D,x)$ (5), the rule that stops at the first $t\in\{1,\dots,M-1\}$ with $\nu^{M-t}(D,x(t))<\nu^M(D,x)$, and at $M$ otherwise, attains $\nu^M(D,x)$.

Significance

The result. The DAI Theorem replaces a dynamic program on the product of $k$ state spaces by $k$ one-dimensional optimal stopping problems. The "only if" half says more than that the index rule is one optimal policy: it characterizes every optimal policy, so any rule that departs from the index on a set of positive probability loses reward. The Lemma identifies the stopping rule that attains the index, which is how indices are computed in practice, and Corollary 1 is the finite-horizon version on which the paper's numerical algorithm (Section 7) rests.

Formalizing it. The sufficiency half is formalized: BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári Theorem 35.9) is Proved on the platform, together with gittins_index_policy_dominates, gittins_stopping_ratio_le_index and gittins_epsilon_optimal_stopping. The attainment Lemma is Proved only for countable state spaces with bounded rewards (AllocationIndices.optimal_stopping_set, Gittins–Glazebrook–Weber Lemma 2.2), and the necessity half is on no platform item. This mission asks for the Lemma on general standard Borel state spaces with integrable rewards, the finite-horizon Corollary 1, and the full equivalence. The Forwards Induction Theorem of p. 153, which needs superprocesses and forwards induction policies, is outside its scope.

Difficulty

The "only if" direction is the new content, and it does not follow from the sufficiency theorem: knowing that one index policy is optimal says nothing about a policy that sometimes plays a lower-index process. The deviation must be shown to cost a strictly positive amount whenever it happens with positive probability, which requires a strict comparison that survives discounting, ties in the index and infinite stopping times. A second obstacle is measure-theoretic. On a general state space the index is a supremum over uncountably many stopping times, its measurability is not available, and the Lemma's stopping rule is a stopping time only if $\{y:\nu(D,y)<\nu(D,x)\}$ is measurable; the arguments of the countable case, which treat each state separately, do not transfer.

Formalization scope

All objects are the published discounted $k$-armed Markov bandit of Def_GittinsIndex and the stopping-time quantities of Def_AllocationIndices_Index; time is indexed from $0$, stopping times are $\mathbb N\cup\{\infty\}$-valued and adapted to the coordinate filtration, and the index is the real supremum over stopping times $\tau\ge1$. The explicit readings committed to are:

• "Optimal" means attaining $\sup_{\pi'}V_{\pi'}(x)$ from the given initial state vector, over all randomized history-dependent policies; this supremum is finite because the values are bounded uniformly in the policy under the integrability hypothesis.
• "At each stage … almost always" means: for every stage $n$, almost surely under the law of the first $n$ stages of $\pi$ from $x$, the selection kernel puts mass one on the processes of maximal current index. Requiring the index rule on every history would make "only if" false.
• "The supremum of the total expected reward is finite" (p. 151) is read as $E_x\sum_t a^t|R(x(t))|<\infty$ for every state $x$.
• "$\nu(D,\cdot)$ is an $\mathcal X$-measurable function" (p. 151) is an explicit hypothesis of the Lemma and of the goal; the measurability of every $\nu^m(D,\cdot)$ is a hypothesis of Corollary 1.
• "The supremum is attained by setting $\Theta_0$" means that the first hitting time of $\Theta_0$ from time $1$ on is a positive stopping time whose ratio equals the index.
• The state space is standard Borel (the paper asks only for measurable singletons), and all processes share one kernel and one reward function; a family of different processes is encoded on the disjoint union of their state spaces.

A trivializing formalization is ruled out: the goal is not stated for index policies on every history (which would only restate the referenced theorem), the index is the published supremum over stopping times rather than a one-step reward or a finite-horizon quantity, competitors are not restricted to Markov or deterministic policies, and the Lemma's stopping rule starts at time $1$, so it never stops at once. A one-point state space satisfies all hypotheses together and admits a policy.

Useful infrastructure, reusable beyond this mission: measurability of the Gittins index on standard Borel spaces, a measurable selection of a maximal-index arm, and an interchange argument for $k$-armed Markov bandits on general state spaces. Proofs of any milestone, and of either half of the goal, are welcome.

Selected references

• J. C. Gittins, Bandit Processes and Dynamic Allocation Indices, J. R. Statist. Soc. B 41(2), 148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
• J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 241–266, 1974.
• P. Whittle, Multi-armed bandits and the Gittins index, J. R. Statist. Soc. B 42(2), 143–149, 1980. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
• R. Weber, On the Gittins index for multiarmed bandits, Ann. Appl. Probab. 2(4), 1024–1033, 1992. https://doi.org/10.1214/aoap/1177005588
• J. N. Tsitsiklis, A short proof of the Gittins index theorem, Ann. Appl. Probab. 4(1), 194–199, 1994. https://doi.org/10.1214/aoap/1177005207
• J. C. Gittins, K. D. Glazebrook and R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033
• T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401