All missions

Motivation

A multiclass queueing network routes jobs of several classes through shared stations. Whether such a network is stable depends on the scheduling policy and not only on the load: the Lu–Kumar and Rybko–Stolyar examples are unstable under a static-priority policy with every station loaded below capacity (Bramson, Stability of Queueing Networks, 2008). A network operator who does not control, or does not know, the policy in use therefore wants robust stability: stability under every policy of a given family.

Zhao, Gurvich and Hasenbein (arXiv:2303.17746v3) study robust stability over the family of queue-ratio policies, which steer each station's workload towards fixed proportions across its classes and contain the static-priority and quadratic max-weight policies as special cases. Their analysis is hierarchical. Under a queue-ratio policy the fluid model first reaches state-space collapse and then follows a linear Skorohod problem. This mission formalizes the second layer: a purely algebraic sufficient condition for stability of that Skorohod problem holds for every queue-ratio policy as soon as it holds at the finitely many static-priority "corners".

Timeline. Dai (1995) reduced stability of the queueing network to stability of its fluid model. Delgado (2010) related fluid stability under state-space collapse to stability of a Skorohod problem. Chen (1996) gave the Chen-$\mathcal S$ sufficient condition for stability of a linear Skorohod problem. Zhao, Gurvich and Hasenbein (preprint 2023, Operations Research 2025) proved that Chen-$\mathcal S$ is inherited from the static-priority corners (their Theorem 4).

Setting

Fix an open network with $J$ stations and $K$ classes. Class $k$ is served at station $s(k)$, and the $J\times K$ constituency matrix $C$ has $C_{jk}=1$ if $s(k)=j$ and $0$ otherwise. $M=\operatorname{diag}(m_1,\dots,m_K)$ holds the mean service times $m_k>0$. $P$ is the substochastic routing matrix, and $\alpha\ge 0$ the vector of exogenous arrival rates. The network is open: $I+P+P^2+\cdots$ converges and $I-P^\top$ is invertible. Then $Q=(I-P^\top)^{-1}$, $\lambda=Q\alpha$ and the traffic intensities are $\rho=CM\lambda$.

A ratio matrix is a $K\times J$ matrix $\Delta$ with $\Delta_{kj}=\delta_k\ge 0$ if $s(k)=j$ and $\Delta_{kj}=0$ otherwise, normalized by

$$CM\Delta=I.$$

It is static-priority if at each station $j$ exactly one class $k$ with $s(k)=j$ has $\Delta_{kj}=1/m_k$ and all others have $\Delta_{lj}=0$. For a ratio matrix with $CMQ\Delta$ invertible, the reflection matrix and drift are

$$R_\Delta=(CMQ\Delta)^{-1},\qquad \theta_\Delta=R_\Delta(\rho-e).$$

A square matrix $R$ is an S-matrix if $Ru>0$ for some $u>0$, and completely-$\mathcal S$ if every principal sub-matrix is an S-matrix. The pair $(R,\theta)$ is Chen-$\mathcal S$ if $R$ is completely-$\mathcal S$ and some $h>0$ satisfies $h_a^\top[\theta_a+R_{ab}u]<0$ for every partition $(a,b)$ of the stations with $a\neq\emptyset$ and every $u\ge 0$ with $\theta_b+R_bu=0$. Ratio matrices are neighbors if they differ in at most one column.

Formalization targets

Goal: Theorem 4

If for every static-priority $\Delta$ the matrix $CMQ\Delta$ is invertible and $(R_\Delta,\theta_\Delta)$ is Chen-$\mathcal S$, and all $\det(CMQ\Delta)$ over static-priority $\Delta$ have one sign, then

$$\forall\,\Delta\ \text{ratio matrix}:\quad CMQ\Delta\ \text{invertible and}\ (R_\Delta,\theta_\Delta)\ \text{Chen-}\mathcal S.$$

The network is arbitrary: any $J$, $K$, routing and service times.

Milestones

For neighbors $\Delta_1,\Delta_2$ and $\Delta_3=\lambda\Delta_1+(1-\lambda)\Delta_2$ with $\lambda\in(0,1)$:

• Lemma 4. The $k$th rows of $R_{\Delta_1}$ and $R_{\Delta_2}$ are proportional with ratio $\det(CMQ\Delta_2)/\det(CMQ\Delta_1)$, and $R_{\Delta_3}$ is a rank-one update of either.
• Theorem 6. $R_{\Delta_3}=\beta R_{\Delta_1}+(1-\beta)R_{\Delta_2}$, with $\beta=\lambda\det R_{\Delta_2}/(\lambda\det R_{\Delta_2}+(1-\lambda)\det R_{\Delta_1})$.
• Lemma 3. Invertibility of $CMQ\Delta_3$ when the determinants of $CMQ\Delta_1$ and $CMQ\Delta_2$ share a sign.
• Theorem 5(i), (ii). Completely-$\mathcal S$, and Chen-$\mathcal S$ of $(R_\Delta,\theta_\Delta)$, pass from $\Delta_1,\Delta_2$ to $\Delta_3$.
• Theorem 3. The completely-$\mathcal S$ analogue of the goal.

Significance

By Chen's theorem, Chen-$\mathcal S$ of $(R_\Delta,\theta_\Delta)$ makes the Skorohod problem of the policy $\Delta$ stable. Theorem 4 reduces this requirement over a continuum of policies to a finite check, one per static-priority policy, and the paper combines it with a state-space-collapse result to certify robust queue-ratio stability of the DHV, push-started Lu–Kumar and Lu–Kumar networks. The orthogonal convexity of Theorem 5 is of independent interest: the Chen-$\mathcal S$ region of ratio matrices is in general not convex, yet it is convex along every axis-parallel segment.

The results are proved on paper and nothing in this mission has been machine-checked. A formal development checks the matrix algebra (adjugate and Sherman–Morrison identities, determinant-sign arguments) and settles the details the paper leaves out. The proof of Theorem 5(ii) is given there only as "an identical argument" to that of part (i). Theorem 6's claim $\beta\in(0,1)$ needs a same-sign hypothesis that the page omits (see below).

Difficulty

The obvious argument fails because the convexity is only orthogonal. The set of ratio matrices is a product of simplices. A convex combination of two arbitrary Chen-$\mathcal S$ ratio matrices need not be Chen-$\mathcal S$, and the inverse $R_\Delta=(CMQ\Delta)^{-1}$ is not affine in $\Delta$. Two pieces of structure must be found and exploited instead. Moving one column of $\Delta$ changes $CMQ\Delta$ in one column, which makes $R_\Delta$ move along a line in a reparametrized coordinate $\beta$. Then completely-$\mathcal S$ and Chen-$\mathcal S$, whose definitions quantify over all partitions and over the solution sets $\{u\ge 0:\theta_b+R_bu=0\}$, must be shown to survive that line. The latter sets move with $\beta$ in a way that does not follow from convexity of either endpoint's set. Passing from neighbors to all ratio matrices needs a column-by-column descent through faces of the product of simplices. Invertibility must be maintained along the way, which is where the common determinant sign at the corners enters.

Formalization scope

• Stations are Fin J, classes Fin K; the paper's index $i$ is Lean's $i-1$. The network is a structure Network J K with fields $s$, $m$, $P$, $\alpha$ and the hypotheses $m>0$, $P\ge 0$, row sums of $P$ at most one, $\alpha\ge 0$, summability of $P^n$, and invertibility of $I-P^\top$. The remark $K>J$ and the renewal arrivals are not used.
• $C$, $M=\operatorname{diag}(m)$, $Q=(I-P^\top)^{-1}$, $\lambda=Q\alpha$, $\rho=CM\lambda$ are definitions computed from the network. $R_\Delta$ and $\theta_\Delta$ are definitions computed from $\Delta$; $\theta_\Delta$ is never a free vector.
• Ratio matrices include $\delta\ge 0$. Without it the goal would assert extrapolation outside the polytope of ratio matrices.
• Lean's matrix inverse is $0$ on singular matrices. Every hypothesis on a corner and the goal's conclusion state invertibility of $CMQ\Delta$ explicitly.
• Partitions are a : Finset (Fin J) with $b=a^{\mathrm c}$; sub-matrices are indexed by the subtypes. Chen-$\mathcal S$ quantifies over $a\neq\emptyset$ (for $a=\emptyset$ the condition reads $0<0$ and would make Chen-$\mathcal S$ unsatisfiable and the goal vacuous); $b=\emptyset$ is allowed. Principal sub-matrices in completely-$\mathcal S$ are those of nonempty index sets.
• "All determinants have the same sign" is a single sign for all corners: either all are positive or all are negative.
• The "Then, $\Delta_1,\Delta_2,\Delta_3$ are ratio-matrix neighbors" sentence of Lemmas 3, 4 and Theorems 5, 6 is kept as a first conjunct.
• Deviation. Theorem 6 asserts $\beta\in(0,1)$ under invertibility alone, which fails when $\det R_{\Delta_1}$ and $\det R_{\Delta_2}$ have opposite signs. That clause is stated under $\det R_{\Delta_1}\det R_{\Delta_2}>0$; the two identities are stated unconditionally.

A complete development needs the adjugate and determinant identities for matrices differing in one column, a Sherman–Morrison formula for rank-one updates, and a decomposition of ratio matrices along faces of a product of simplices. The definitions of S-matrices, completely-$\mathcal S$ and Chen-$\mathcal S$ are reusable for other work on reflected processes. Proofs of the milestones, alternative proofs of Theorem 5 that avoid linear-programming duality, and counterexamples showing a hypothesis cannot be dropped are all welcome.

Selected references

• Y. Zhao, I. Gurvich, J. Hasenbein, A Hierarchical Approach to Robust Stability of Multiclass Queueing Networks, arXiv:2303.17746v3, 2024. https://arxiv.org/abs/2303.17746
• H. Chen, A sufficient condition for the positive recurrence of a semimartingale reflecting Brownian motion in an orthant, Annals of Applied Probability 6(3):758–765, 1996 (reference [5] of the source).
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1):49–77, 1995 (reference [10] of the source).
• R. Delgado, State space collapse and stability of queueing networks, Mathematical Methods of Operations Research 72(3):477–499, 2010 (reference [16] of the source).
• M. Bramson, Stability of Queueing Networks, Lecture Notes in Mathematics 1950, Springer, 2008. https://doi.org/10.1007/978-3-540-68896-9

Motivation

Multi-server queues model call centres, hospital wards, cloud server pools and any system in which $n$ identical servers work through one first-come-first-served (FCFS) line. Capacity planning for such systems needs bounds on the steady-state queue length and on the probability of delay (the chance that an arriving job finds every server busy) that are explicit, hold for every $n$, and stay informative as the load approaches capacity.

For a single server, Kingman's bound (Kingman 1962, ref. [89] of the paper) gives exactly this: the mean wait is at most a multiple of $1/(1-\rho)$ that depends only on the first two moments of the inter-arrival and service times. For $n$ servers with general distributions (the GI/GI/n queue), no comparable explicit bound was known.

Timeline.

• 1962: Kingman's single-server bound.
• 1981: Halfin and Whitt identify the heavy-traffic regime $\sqrt n(1-\rho)\to\beta$ in which the probability of delay is nondegenerate (Halfin and Whitt 1981).
• 2013: Gamarnik and Goldberg prove (for the GI/G/n queue) that the steady-state number waiting is stochastically dominated by the supremum of a process built from independent renewal processes (Gamarnik and Goldberg 2013). Their bound is not explicit and needs more than two service moments.
• 2017–2025: Li and Goldberg derive explicit bounds with $1/(1-\rho)$ scaling under $\mathbb E[A^2]<\infty$ and $\mathbb E[S^{2+\epsilon}]<\infty$ (arXiv:1706.04628, Mathematics of Operations Research 2025).

Setting

A GI/GI/n queue has $n\ge1$ identical servers and one FCFS line. Jobs arrive with i.i.d. inter-arrival times distributed as a nonnegative random variable $A$. Each job needs an i.i.d. service time distributed as a nonnegative random variable $S$, independent of the arrivals. An arriving job starts service at the first server to become free, in order of arrival.

Write $\mu_A=1/\mathbb E[A]$ and $\mu_S=1/\mathbb E[S]$ for the arrival and service rates, and $\rho=\mu_A/(n\mu_S)$ for the traffic intensity. The moment index is

$$r^*=\sup\{r:\mathbb E[S^r]<\infty\},$$

which may be $+\infty$. Normalised moments are $\mathbb E[(A\mu_A)^2]$ and $\mathbb E[(S\mu_S)^r]$.

$Q(t)$ is the number of jobs in the system (in service and waiting) at time $t$. "$Q(\infty)$ exists" means that, whatever the initial condition, $Q(t)$ converges in distribution as $t\to\infty$ to a random variable $Q(\infty)$. The steady-state number waiting is $L(\infty)=\max(0,Q(\infty)-n)$, and the steady-state probability of delay is $\mathbb P(Q(\infty)\ge n)$.

The milestones also use equilibrium renewal processes. For a nonnegative $X$ with finite mean, its equilibrium law $R(X)$ satisfies $\mathbb P(R>y)=\frac1{\mathbb E[X]}\int_y^\infty\mathbb P(X>z)\,dz$. An equilibrium renewal process with renewals distributed as $X$ has its first renewal interval distributed as $R(X)$ and the later ones distributed as $X$.

$A_e(t)$ counts the renewals in $[0,t]$ of such a process for $A$. $N_{e,1}(t),\dots,N_{e,n}(t)$ count those of $n$ independent such processes for $S$, also independent of $A_e$.

Formalization targets

Goal: Theorem 2 (pp. 9–10)

Assume

• $\mathbb E[A^2]<\infty$;
• $r^*>2.5$;
• $\mu_A<n\mu_S$;
• $Q(\infty)$ exists.

Then for all $x>0$ and all $r\in[2.5,r^*)$,

$$\mathbb P\Big(L(\infty)\ge\frac x{1-\rho}\Big)\le 2\cdot10^4\,\mathbb E[(S\mu_S)^2]\,(10^6)^r\Big(\mathbb E[(S\mu_S)^2]^{r-1}r^{2.5r}+r^{1.5r}\mathbb E[(S\mu_S)^r]\Big)x^{-\frac r2}+1.1\,e^{-.0225\,\mathbb E[(A\mu_A)^2]^{-1}x},$$ $$\mathbb P\big(Q(\infty)\ge n\big)\le 2\cdot10^4\,\mathbb E[(S\mu_S)^2]\,(10^7)^r\Big(\mathbb E[(S\mu_S)^2]^{r-1}r^{2.5r}+r^{1.5r}\mathbb E[(S\mu_S)^r]\Big)\big(n(1-\rho)^2\big)^{-\frac r2}+1.1\,e^{-.0028\,\mathbb E[(A\mu_A)^2]^{-1}n(1-\rho)^2}.$$

The paper states the infimum over $r$. With $r$ universally quantified the statement is equivalent, because the exponential term does not depend on $r$.

Milestones

They follow the paper's proof, in attack order:

• Lemma 1, the Gamarnik–Goldberg comparison $\mathbb P(L(\infty)\ge x)\le\mathbb P(\sup_{t\ge0}(A_e(t)-\sum_{i=1}^nN_{e,i}(t))\ge x)$;
• Lemma 2, which splits that supremum into an arrival part and a service part;
• Lemmas 8, 9 and 10, which reduce the arrival part to Kingman's bound with an explicit exponent;
• Lemma 3, the exponential bound for the arrival part;
• Lemma 4 and Theorem 10, conditional bounds from central moments of the pooled process $\sum_iN_{e,i}(t)$;
• Lemmas 5 and 6, those central-moment bounds;
• the explicit bound for $r\in(2.5,r^*)$ displayed on p. 28;
• Lemma 14, a transient comparison for a queue started with all servers busy;
• Lemma 7 and Corollary 5, comparisons with fewer servers that make the bound informative at the level $Q(\infty)\ge n$.

Significance

The result. The bounds hold for every $n$ and every load with $\rho<1$, and they depend on the distributions only through a few normalised moments. In the Halfin–Whitt regime, $n(1-\rho)^2$ stays bounded away from zero, so the delay bound stays informative. As $\rho\to1$ with $n$ fixed, the queue tail decays at the Kingman scale $1/(1-\rho)$. These are the first such bounds for general GI/GI/n queues; earlier explicit results needed Poisson arrivals or exponential service. The paper derives from Theorem 2 bounds at a fixed $r$ (Corollaries 1–2), a refinement beyond $1/(1-\rho)$ scaling when $n(1-\rho)^2$ is large (Corollary 3), and optimised bounds under growth conditions on $\mathbb E[(S\mu_S)^r]$ (Theorem 3).

Formalization. The theorem is proved in the paper, partly in a supplemental appendix, and none of it is formalized; there are no machine-checked results for multi-server queues with general distributions anywhere. A complete development would add to the platform the first FCFS multi-server queue with general distributions, its steady state, equilibrium renewal processes, and the Gamarnik–Goldberg comparison chain. Each is reusable for later work on many-server queues.

Difficulty

The obvious route is to compare the $n$-server queue with a single-server one, or to apply a heavy-traffic limit. The first loses a factor of $n$; the second gives limits but no bounds at a fixed $n$.

The paper's route needs two hard ingredients:

• Comparison with renewal processes. The stochastic comparison of Lemmas 1 and 14 is a theorem about the sample-path dynamics of FCFS service, not a calculation.
• Uniform moment bounds. Explicit control of $\mathbb E|\sum_{i=1}^nN_{e,i}(t)-nt|^r$ at the scale $(nt)^{r/2}$, uniformly in $n$ and $t$, is required. Classical renewal moment bounds are either asymptotic in $t$ or lose the dependence on $n$.

For the probability of delay, Lemma 1 at level $0$ gives only the trivial bound $1$. A second comparison across server counts (Lemma 7) is needed.

Formalization scope

Laws. $A$ and $S$ are represented by their laws $\mu_A,\mu_S$: probability measures on $\mathbb R$ carried by $[0,\infty)$, integrable, with positive mean. Positivity of the means is implicit in the paper, which needs $\mu_X=1/\mathbb E[X]$ finite; it is stated explicitly. $\mathbb E[(X\mu_X)^r]$ is a real integral and is used only where it is finite: $r<r^*$ for $S$, and $r=2$ with $\mathbb E[A^2]<\infty$ for $A$. $r^*$ is an extended real.

The queue.

• The queue is the Kiefer–Wolfowitz workload recursion, driven by an initial condition and i.i.d. pairs of inter-arrival and service times.
• An initial condition gives the first-arrival time and the residual service time at each server. No job waits at time $0$.
• "$Q(\infty)$ exists with law $\pi$" quantifies over every initial law of that kind, independent of the inputs. This class is narrower than the paper's, so the hypothesis is weaker and the stated theorem is stronger. The paper's proof uses only such initial conditions (Lemma 7 through Lemma 14).
• $L(\infty)$ is the truncated difference $\max(0,Q(\infty)-n)$.

Renewal processes.

• Counts are natural numbers, computed pathwise from the renewal intervals.
• Bounding families are arbitrary probability spaces carrying mutually independent intervals with the prescribed laws.
• Suprema of processes are taken in the extended reals.

Ruled out. None of the following trivializing formalizations is used:

• a steady-state hypothesis that no queue satisfies, or one restricted to an initial-condition class that drops what Lemma 7 needs;
• a real-valued supremum or infimum, which collapses to $0$ on unbounded families;
• a Bochner moment of a non-integrable function, which is $0$ in Lean.

The infimum over $r$ is stated as a universal quantifier.

Needed infrastructure. Equilibrium distributions and renewal counting processes, moment and maximal inequalities for sums of independent renewal processes, Kingman's exponential martingale bound, and the sample-path comparison of FCFS multi-server queues. Contributions on any of these are welcome: the renewal and random-walk results (Lemmas 5, 6, 8–10) are independent of queueing.

Selected references

• Y. Li and D. A. Goldberg, Simple and explicit bounds for multi-server queues with 1/(1−ρ) scaling, Mathematics of Operations Research, 2025; arXiv:1706.04628v3. https://arxiv.org/abs/1706.04628
• D. Gamarnik and D. A. Goldberg, Steady-state GI/G/n queue in the Halfin–Whitt regime, Annals of Applied Probability 23(6), 2382–2419, 2013. https://doi.org/10.1214/12-AAP905
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society B 24, 383–392, 1962 (ref. [89] of Li–Goldberg).
• J. F. C. Kingman, A martingale inequality in the theory of queues, Mathematical Proceedings of the Cambridge Philosophical Society 60(2), 359–361, 1964 (ref. [90] of Li–Goldberg; the source of Lemma 9).

Motivation

Many demand, traffic and click-through series are seasonal: their mean repeats after a fixed number of periods (a week of days, a year of months), while the length of that cycle is not known in advance. A retailer choosing among $K$ promotions, or a platform choosing among $K$ recommendations, then faces a multi-armed bandit whose arms have time-varying but periodic mean rewards. Standard stochastic bandit algorithms assume stationary means and fail here, and fully adversarial or arbitrarily drifting models give up the structure that periodicity offers.

N. Chen, C. Wang and L. Wang (arXiv:2005.08088, Operations Research, 2025) propose a two-stage policy for this problem: a spectral first stage that estimates every arm's period from a short exploration phase, and a confidence-bound second stage that learns and exploits the resulting "effective arms". Their main upper bound, Theorem 1, shows that the policy's regret grows like $\sqrt{T\sum_k T_k}$ up to logarithmic factors. This mission formalizes that theorem and the chain of lemmas behind it. The matching lower bound (Theorem 3 of the paper) is the subject of a separate mission of this series.

Setting

At each epoch $t=1,\dots,T$ a decision maker pulls one of $K$ arms. Pulling arm $k$ at epoch $t$ yields the reward $Y_{k,t}=\mu_{k,t}+\epsilon_t$. The mean $\mu_{k,t}$ has a minimum period $T_k\ge1$: $\mu_{k,t+T_k}=\mu_{k,t}$ for all $t\ge1$, and no smaller positive shift has this property. The standing assumptions are:

• Assumption 1: $\mu_{k,t}\in[0,1]$.
• Assumption 2: the noises $\epsilon_t$ are independent and sub-Gaussian with parameter $\sigma$, i.e. $\mathbb E[e^{\lambda\epsilon_t}]\le e^{\sigma^2\lambda^2/2}$ for all real $\lambda$ and $\mathbb P(|\epsilon_t|>x)\le2e^{-x^2/(2\sigma^2)}$.

The pseudo-regret of an arm sequence $\pi$ is $R^\pi_T=\sum_{t=1}^T(\max_k\mu_{k,t}-\mu_{\pi_t,t})$, and the number of effective arms is $d=\sum_{k=1}^KT_k$: arm $k$ at phase $t \bmod T_k$ is one effective arm.

Stage one (Algorithm 1). Each arm is pulled $n$ times in a row. From its $n$ rewards the policy computes the periodogram $|\tilde y_k(v)|$, the modulus of the discrete Fourier transform $\tilde y_k(v)=\frac1n\sum_sY_{k,s}e^{-2\pi ivs}$, on $v\in[0,1/2]$. A data-driven threshold $\tau_k$ is computed from the constants $U_1,U_2$ (sums of sinc-type maxima), $\bar\epsilon_v=\frac{2\sigma H}{1-\pi/24}\sqrt{\log(n)/n}$ and $\sup_v|\tilde y_k(v)|$. The algorithm repeatedly takes the highest peak above $\tau_k$ in $[g/n,1/2]$, snaps it to the nearest fraction $j_1/j_2$ with $j_2<n/(2g)$, and removes a $2g/n$-neighbourhood. The period estimate $\hat T_k$ is the least common multiple of the selected reciprocals.

Stage two (Algorithm 2). At every later epoch an $S$-round screening tournament, $S=\lfloor\log_2T\rfloor$, compares the arms at their current phases modulo $\hat T_k$. It uses estimated means $m^{(s)}_{k,t}$ and widths $w^{(s)}_{k,t}$ pooled from the stage-one samples and from round-specific index sets $\Psi^{(s)}(t)$. The weak oracle runs the same policy with the true periods in place of $\hat T_k$.

The parameters are fixed by (7): $n=\lfloor\sqrt{T/K}\rfloor$, $g=\lceil\sqrt n\rceil$, $H=\sqrt{1+\log n}$. Assumption 3 asks $T>4K$, $g\ge\max\{2,\sqrt n\}$ and $T_k<n/(2g)$. Assumption 4 asks the smallest present Fourier coefficient $b_k$ of each arm to dominate a combination of $\bar\epsilon_v$ and the largest coefficient $B_k$.

Formalization targets

Goal: Theorem 1

Under Assumptions 1–4 and (7), the two-stage policy satisfies

$$\mathbb E\big[R^\pi_T\big]\le C\sqrt{T\,d\,\log^2(T)\,\log(T/d)} ,$$

with $C$ depending only on $\sigma$ and $K$, and with Algorithm 2 run at $\delta=8/T$.

Stage one: correct period identification

• Lemma 1: uniform noise bound for the periodogram, $48n\exp(-(n\delta^2/4\sigma^2)(1-\pi/24)^2)$.
• Lemmas 2–3: leakage bounds $\pi B_kU_1$, $\pi B_kU_2$, and $B_k\le(\sup|\tilde\epsilon_k|+\sup|\tilde y_k|)/(1-\pi U_2)$.
• Lemmas 4–5: the threshold separates the neighbourhoods of the present frequencies from the rest, with probability $1-48/n^{H^2-1}$.
• Lemmas 6–7: the sharper noise bound near possible present frequencies, and the location of the peaks within $1/n$ of them.
• Theorem 2: $\mathbb P(\Lambda)\ge1-48K/n^{H^2-1}-200K/n^{0.867H^2-1}-200K/n^{0.6934H^2-1}$.

Stage two: the oracle's regret

• Lemma 15: an anytime sub-Gaussian deviation bound.
• Lemma 9: the confidence event $\mathcal E$ has probability at least $1-\delta S$.
• Lemma 10: on $\mathcal E$ the optimal arm survives screening, and each epoch's gap is at most $1$, $8\sigma/2^s$ or $2\sigma/\sqrt T$.
• Lemma 16: the summed widths of a round are at most $4\sigma\sqrt{|\Psi^{(s)}(T)|\,d\log(8T/\delta)\log(T/d)}$.
• Lemma 11: the oracle's expected regret is at most $C\sqrt{Td\log^2(T)\log(T/d)}$ with $C$ depending only on $\sigma$.

Significance

The theorem shows that unknown seasonality costs only the factor $\sqrt{d}=\sqrt{\sum_kT_k}$ that would be paid if every phase of every arm were a separate stationary arm. Up to logarithmic factors this matches the $\sqrt{TK}$ rate of the classical stationary bandit with $d$ arms in place of $K$. Together with the paper's lower bound $\Omega(\sqrt{T\max_kT_k})$ it locates the minimax regret of periodic bandits within a factor $\sqrt K$. Stage one is a non-asymptotic, finite-sample period-identification guarantee for a thresholded periodogram, which is of independent use in spectral estimation.

The paper proves these results; none of them is machine-checked. A complete development yields a verified finite-sample periodogram theory (noise bounds for random trigonometric polynomials, Dirichlet-kernel leakage estimates), a verified anytime sub-Gaussian inequality, and a verified analysis of a nested elimination algorithm with data reuse. The formalization also pins down several points the printed text leaves open: the constant $0.233$ of Lemma 6 and the exponent $0.694$ of Lemma 7 and Theorem 2 are slightly stronger than what the proofs give, and the printed claim that Theorem 1's constant is independent of $K$ is not established by the printed argument.

Difficulty

Two steps resist the obvious approach. In stage one, the periodogram has to be controlled at uncountably many frequencies at once. A union bound over $v$ is unavailable, and the leakage of each present frequency spreads over the whole spectrum, so both the noise and the signal must be bounded uniformly in $v$ with explicit constants. In stage two, the samples used to estimate an effective arm are selected with the estimated periods, which were computed from the same stage-one data, so the usual independence behind confidence bounds fails. Lemmas 9–11 are therefore stated for the weak oracle, whose sample selection does not depend on the data; on the event $\Lambda$ the definitions make the oracle's run and the policy's run the same function of the noise path.

Formalization scope

Epochs are natural numbers $t\ge1$; arms are Fin K (the paper's arm $k$ is index $k-1$), and $K\ge1$. The noise is a sequence $\epsilon:\mathbb N\to\Omega\to\mathbb R$ on a probability space, independent, with Mathlib's HasSubgaussianMGF at variance proxy $\sigma^2$, plus the printed tail clause. Both algorithms are defined in full, as deterministic functions of the noise path, with canonical tie-breaking: smallest maximizer, smallest closest candidate, smallest arm index. Algorithm 1's loop runs at most $n$ passes, and $\mathrm{LCM}(\hat v_i^{-1})$ is the least common multiple of the reduced denominators of the selected frequencies. Algorithm 2 takes its period vector as an argument; the two-stage policy and the oracle are its two instances. Expected regret is an outer expectation: an integrable majorant of the regret whose integral obeys the bound. Probability bounds bound the outer measure of the bad event. Every DFT uses the absolute stage-one epochs, as in Step 8 of Algorithm 1.

Disclosed deviations: Theorem 1's constant depends on $\sigma$ and $K$ (the printed proof does not give uniformity in $K$), and $\delta=8/T$ is fixed as in the proof of Lemma 11. Lemma 6 uses $0.2328$ for the printed $0.233$; Lemma 7 and Theorem 2 use $0.6934$ for the printed $0.694$. Lemma 7 covers the nonzero present frequencies. Lemma 11 states the standing Assumption 3 and the parameters (7) as hypotheses, as its proof uses them.

The algorithm is the object of the theorem. Replacing Algorithm 1 by "any estimator that is correct with high probability", or Algorithm 2 by "any policy with the oracle's regret", would make the goal a different and much weaker statement. So would placing the constant after the horizon or the instance, since the regret is at most $T$, or using a bare Lebesgue integral of a possibly non-measurable regret.

A complete development needs discrete Fourier analysis of finite sequences, Bernstein's inequality for complex polynomials on the unit disc (Lemma 14 of the paper, from Nagy and Totik), sinc-function estimates, anytime concentration for sub-Gaussian sums, and a bookkeeping layer for the nested index sets of Algorithm 2. The concentration and polynomial-inequality parts are reusable beyond this mission. Proofs of individual lemmas, helper lemmas such as the closed form (6) of the frequency components, and alternative arguments are welcome.

Selected references

• N. Chen, C. Wang, L. Wang, Learning and Optimization with Seasonal Patterns, arXiv:2005.08088v4, 2021; Operations Research, 2025. https://arxiv.org/abs/2005.08088
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• L. Li, Y. Lu, D. Zhou, Provably Optimal Algorithms for Generalized Linear Contextual Bandits, ICML 2017. https://arxiv.org/abs/1703.00048
• B. Nagy, V. Totik, Bernstein's Inequality for Algebraic Polynomials on Circular Arcs, Constructive Approximation 37, 223–232, 2013.

Motivation

Optimal control of partial differential equations under uncertainty arises whenever a physical system is steered by a control while its sources, coefficients or loads are only known in distribution. A typical requirement is a state constraint: the state (a temperature, a concentration, a displacement) must stay below a threshold everywhere in the domain. When the source term is random, demanding this for every realization is often impossible or too conservative, and the natural relaxation is a probabilistic (chance) constraint: the state must stay below the threshold uniformly on the domain with probability at least $p$.

Probabilistic constraints are classical in operations research (Prékopa, Stochastic Programming, 1995), but in a PDE setting the constraint is an infinite family of random inequalities, one per point of the domain, and the probability function is not differentiable in general. C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive optimality conditions for such problems in terms of the Clarke subdifferential, building on the spherical-radial decomposition of Gaussian vectors developed by Hantoute, Henrion and Pérez-Aros (Math. Program. 2019) and van Ackooij and Henrion. This mission formalizes the PDE half of §2 of that paper: explicit formulas for the subdifferential of the probability function and the resulting optimality conditions.

Setting

Let $D\subseteq\mathbb R^d$, $d\in\{1,2,3\}$, be a nonempty, open, bounded set of class S: there are $\gamma\in(0,1)$ and $r_0>0$ with $\operatorname{meas}(B_r(x)\setminus D)\ge\gamma\operatorname{meas}(B_r(x))$ for all $x\in\partial D$ and $0<r<r_0$. For $F\in L^2(D)$ the Dirichlet problem $-\Delta y=F$ in $D$, $y=0$ on $\partial D$ has a unique weak solution in $H^1_0(D)\cap C(\bar D)$; the solution operator $A^{-1}:L^2(D)\to C(\bar D)$ is linear and continuous.

Fix $f_0,\varphi_1,\dots,\varphi_m\in L^2(D)$ and a threshold $\alpha\in\mathbb R$. The control-to-state operator is

$$S(u,z)=A^{-1}\Big(u+f_0+\sum_{i=1}^m z_i\varphi_i\Big)=P(u,z)+y_0,\qquad P(u,z)=A^{-1}u+\sum_i z_iA^{-1}\varphi_i,\ y_0=A^{-1}f_0.$$

The random vector $\xi$ on a probability space $(\Omega,\mathcal F,\mathbb P)$ is Gaussian $\mathcal N(0,\Sigma)$ with $\Sigma$ positive definite, and $y(\cdot,\omega)=S(u,\xi(\omega))$ is the random state. With $g(u,z)=\max_{x\in\bar D}[S(u,z)](x)-\alpha$ and the probability function $\varphi(u)=\mathbb P(\omega\mid g(u,\xi(\omega))\le0)$, the problem is

$$\min_{u\in L^2(D)}F(u)\quad\text{s.t.}\quad \varphi(u)=\mathbb P\big(y(x,\omega)\le\alpha\ \ \forall x\in D\big)\ge p,\tag{24}$$

with $F$ convex and Fréchet differentiable and $p\in(0,1]$.

The analysis uses the spherical-radial decomposition. Let $\mu_\zeta$ be the uniform distribution on the unit sphere $\mathbb S^{m-1}$, $\mu_\eta$ the chi distribution with $m$ degrees of freedom and density $\chi(t)=Kt^{m-1}e^{-t^2/2}$, $\Sigma^{1/2}$ the square root of $\Sigma$. The radial probability function is $e(u,v)=\mu_\eta\{r\ge0\mid g(u,r\Sigma^{1/2}v)\le0\}$ and the radius function $\rho(u,v)\in[0,\infty]$ is the supremum of that set. For $x\in\bar D$, $u_x\in L^2(D)$ is defined by $(u_x,h)_{L^2(D)}=(A^{-1}h)(x)$, and

$$M^*(\bar u,v)=\{x\in\bar D\mid[P(0,\Sigma^{1/2}v)](x)>0,\ \bar y(x)+\rho(\bar u,v)[P(0,\Sigma^{1/2}v)](x)=\alpha\},\qquad \bar y=S(\bar u,0).$$

$\partial^C$ is the Clarke subdifferential, with $L^2(D)^*$ identified with $L^2(D)$, and integrals of set-valued maps are Aumann integrals.

Formalization targets

Goal: Theorem 2.16

Assume a control $\hat u$ with $\varphi(\hat u)>p$ (41), and let $u^*$ be feasible with expected state $\tilde y=S(u^*,0)$ satisfying $\tilde y(x)<\alpha$ on $\bar D$ (42). If $u^*$ solves (24), there is $\lambda\ge0$ with

$$DF(u^*)\in-\lambda\int_{\{v\mid\rho(u^*,v)<\infty\}}\chi(\rho(u^*,v))\cdot\operatorname{clco}\Big\{\frac{u_x}{[P(0,\Sigma^{1/2}v)](x)}\ \Big|\ x\in M^*(u^*,v)\Big\}\,d\mu_\zeta(v),$$ $$\lambda\big(\mathbb P(y^*(x,\omega)\le\alpha\ \forall x\in D)-p\big)=0,$$

and these conditions are sufficient when $M^*(u^*,v)$ is a singleton for $\mu_\zeta$-a.e. $v$ with $\rho(u^*,v)<\infty$, or the set $\{z\mid g(u^*,z)\le0\}$ is bounded. The goal has no hard-coded constants; it asserts the form of the optimality system.

Milestones

In attack order: well-posedness of the state equation with the bound $\|\hat y\|_{C(\bar D)}\le C(\|z\|_2+\|u+f_0\|_{L^2(D)})$ (Lemma 1.2); measurability of the random state (Lemma 1.4); convexity and global Lipschitz continuity of $g$ (Lemma 2.9); moderate growth (Lemma 2.10); the Lipschitz and subdifferential conclusions of the general theory under (26) (Corollary 2.11); the optimality conditions (21), (22) for (24) (Corollary 2.12); $\partial^C_ue(\bar u,v)=\{0\}$ when $\rho(\bar u,v)=\infty$ (Lemma 2.13); the explicit formula $\partial^C_ue(\bar u,v)=-\chi(\rho(\bar u,v))\cdot\operatorname{clco}\{u_x/[P(0,\Sigma^{1/2}v)](x)\mid x\in M^*(\bar u,v)\}$ when $\rho(\bar u,v)<\infty$ (Lemma 2.14); and the upper estimate (40) of $\partial^C\varphi(\bar u)$ with its equality cases (Theorem 2.15).

Significance

The result turns an abstract statement — $DF(u^*)$ lies in a multiple of the Clarke subdifferential of a probability function that has no closed form — into a condition written in the problem data: Green-type functions $u_x$, the expected state, and the radius function along each direction of the sphere. This is what makes the conditions usable for checking candidate controls and for designing algorithms, and Example 2.18 of the paper computes a solution this way. The sufficiency half identifies when the nonconvex chance-constrained problem behaves like a convex one.

The paper's proofs are on paper only; to our knowledge none of these results, nor the spherical-radial decomposition, Clarke calculus in Hilbert spaces, or Aumann integrals in $L^2$, has a machine-checked proof. Formalizing Theorem 2.16 requires connecting elliptic regularity, Gaussian measure theory and nonsmooth analysis, and the milestones are reusable on their own: Lemma 1.2 is a regularity statement for the Poisson equation, and Lemmas 2.13 and 2.14 are max-function subdifferential formulas in an infinite-dimensional space.

Difficulty

The obvious route — differentiate $\varphi$ and use a Lagrange multiplier — fails because $\varphi$ is generally not differentiable even for smooth data (Example 2.17 of the paper), and because $g$ is only Lipschitz, being a maximum over $\bar D$. The general subdifferential estimate (Theorem 2.2, from Hantoute–Henrion–Pérez-Aros) needs a growth condition and only gives an inclusion, since the radial probability function is not Clarke regular; the radius function $\rho(\cdot,v)$ is an infimum over the open set where $P(0,\Sigma^{1/2}v)>0$, which is neither compact nor independent of $u$, so standard max-function formulas do not apply directly. Directions with $\rho=\infty$ require a separate limiting argument through the Mordukhovich subdifferential (Lemma 2.13). The regularity input, continuity of solutions on $\bar D$ for class-S domains (Kinderlehrer–Stampacchia 1980), is not in Mathlib.

Formalization scope

All declarations are in the namespace ChanceStateCtrl.PDE. $\mathbb R^d$ and $\mathbb R^m$ are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m), indices are Fin m, $L^2(D)$ is Lp ℝ 2 (volume.restrict D). Weak derivatives are the published HunterPDE.Shared.HasWeakDeriv; a weak solution is a function continuous on $\bar D$, zero on $\partial D$, in $L^2(D)$ with weak first derivatives in $L^2(D)$, satisfying the weak form against $C_c^\infty(D)$.

Standing hypotheses on every theorem: $D$ open, bounded and nonempty, $d\in\{1,2,3\}$, class S, and CompactSpace (closure D) (a consequence of boundedness). Nonemptiness of $D$ is the one added hypothesis: Lean's supremum over an empty domain is $0$, not $-\infty$, and Lemma 2.9's identification of events fails for $D=\emptyset$. $A^{-1}$ is a continuous linear map to $C(\bar D)$ together with the hypothesis that it returns the weak solution; it is never an arbitrary operator. $m\ge1$, as the uniform distribution on $\mathbb S^{m-1}$ requires. $\Sigma^{1/2}$ is the positive semidefinite root; $\|\Sigma^{1/2}\|$ is its operator norm. The Clarke directional derivative is $\limsup_{u'\to u,t\downarrow0}(f(u'+th)-f(u'))/t$ (the page's denominator $h$ is a misprint). $\rho$ takes values in $[0,\infty]$. clco is the norm closure of the convex hull. The integral in (40)/(43) is over the restriction of $\mu_\zeta$ to $\{\rho<\infty\}$, not a renormalization. A solution is a global minimizer over $\{u\mid\varphi(u)\ge p\}$; the page's "solution to (9)" refers to this instance of the abstract problem (9).

Trivializing formalizations are ruled out: every Clarke subdifferential is taken at a point where the function is locally Lipschitz (proved in Corollary 2.11 and Theorem 2.15), the state operator is tied to the PDE, the multiplier carries its sign and complementarity, Aumann selections must be scalarly integrable, and optimality is global.

Needed infrastructure: elliptic regularity in $C(\bar D)$ for class-S domains; the spherical-radial decomposition of $\mathcal N(0,\Sigma)$; Clarke calculus (chain rule, max functions) on Hilbert spaces; Clarke's theorem on subdifferentials of integral functionals. Contributions of any of these as stand-alone theorems are welcome.

Selected references

• C. Geiersbach, R. Henrion, Optimality conditions in control problems with random state constraints in probabilistic or almost-sure form, arXiv:2306.03965v2, 2024; Math. Oper. Res., 2025. https://arxiv.org/abs/2306.03965
• A. Hantoute, R. Henrion, P. Pérez-Aros, Subdifferential characterization of probability functions under Gaussian distribution, Math. Program. 174 (2019), 167–194. https://doi.org/10.1007/s10107-018-1237-9
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983; SIAM reprint 1990. https://doi.org/10.1137/1.9781611971309
• D. Kinderlehrer, G. Stampacchia, An Introduction to Variational Inequalities and Their Applications, Academic Press, 1980; SIAM reprint 2000. https://doi.org/10.1137/1.9780898719451
• A. Prékopa, Stochastic Programming, Kluwer, 1995. https://doi.org/10.1007/978-94-017-3087-7

Motivation

Dividing indivisible goods among agents without money is a basic problem of fair division. The most widely used procedure is Round-Robin: the agents take turns, in a fixed order, picking their favourite remaining good. For agents with additive valuations, Round-Robin run on the agents' true preferences produces an allocation that is envy-free up to one good (EF1, Lipton et al. 2004). The agents, however, report their preferences, and a strategic agent may misreport. This raises the question of which allocations arise at the mechanism's equilibria, and whether equilibria exist at all.

For additive valuations, the existence of an exact pure Nash equilibrium was established in pieces over three papers (Bouveret–Lemaître 2016, Aziz–Goldberg–Walsh 2017, Amanatidis et al. 2021), through the bluff profile, in which every agent reports the order in which the truthful run hands out the goods. Amanatidis, Birmpas, Lazos, Leonardi and Reiffenhäuser (arXiv:2301.13652, Mathematics of Operations Research 2025) carry this programme beyond additive agents. For cancelable valuations the bluff profile is still an exact equilibrium (Theorem 3.2). For submodular valuations exact equilibria may fail to exist (Proposition 3.4), and the right generalization of the bluff profile is not obvious. This mission formalizes their answer for submodular agents: a greedy bluff profile that is always a $\tfrac12$-approximate equilibrium, with $\tfrac12$ best possible.

Setting

There are $n\ge1$ agents $N=[n]$ and a finite set $M$ of $m$ goods. Agent $i$ has a valuation $v_i:2^M\to\mathbb R$ that is normalized, $v_i(\emptyset)=0$, and non-decreasing. The marginal value of $g$ with respect to $S$ is $v_i(g\mid S)=v_i(S\cup\{g\})-v_i(S)$. The valuation is submodular if $v_i(g\mid S)\ge v_i(g\mid T)$ whenever $S\subseteq T$ and $g\notin T$.

Each agent reports a ranking $\succ_i$, a total order on $M$. Mechanism 1 (Round-Robin) runs $k=m/n$ rounds. In each round agents $1,\dots,n$ act in turn, and the acting agent receives the first good of $\succ_i$ that is still available. $v_i(\mathcal M(\succ))$ denotes agent $i$'s true value for the bundle she receives under the reported profile $\succ$. A profile of rankings is an $\alpha$-approximate pure Nash equilibrium (PNE) if no agent can multiply her value by more than $1/\alpha$ through reporting another ranking:

$$\alpha\cdot v_i\big(\mathcal M(\succ_i',\succ_{-i})\big)\le v_i\big(\mathcal M(\succ)\big)\quad\text{for all } i \text{ and all rankings }\succ_i'.$$

The submodular bluff profile comes from Algorithm 2 (p. 10), a hypothetical truthfully greedy run. Agents act in round-robin order, and the active agent $i$ takes a good of largest marginal value $v_i(g\mid X_i)$ with respect to her current goods $X_i$. Listing the goods in the order this run hands them out gives $h_1,\dots,h_m$, and the bluff profile $\boldsymbol\succ^{\mathrm b}$ is the profile in which every agent reports $h_1\succ^{\mathrm b}\cdots\succ^{\mathrm b}h_m$.

Formalization targets

Goal: Theorem 3.7 (p. 12)

When all valuations are submodular, the bluff profile is a $\tfrac12$-approximate PNE:

$$\tfrac12\, v_i\big(\mathcal M(\succ_i,\boldsymbol\succ^{\mathrm b}_{-i})\big)\le v_i\big(\mathcal M(\boldsymbol\succ^{\mathrm b})\big)\qquad\text{for every agent } i \text{ and every ranking }\succ_i .$$

Moreover, for every $\varepsilon>0$ there is an instance in which the bluff profile is not a $(\tfrac12+\varepsilon)$-approximate PNE. Both parts form the goal; the bound without the tightness is a weaker statement.

Milestones

1. Claim 3.6 (p. 12). If agent $i$'s deviation bundle beats her bluff bundle good-wise at some round $\ell$, then both runs have allocated the same goods before her $\ell$-th pick, and these include $y_1,\dots,y_\ell$.
2. Lemma 3.5 (p. 11). Good-wise domination: $v_i(x_j\mid X^{j-1}_-)\ge v_i(y_j\mid X^{j-1}_-)$ for every round $j$. Here $X=\{x_1,\dots,x_k\}$ is the bluff bundle in allocation order and $Y=\{y_1,\dots,y_k\}$ is the deviation bundle, ordered by Algorithm 3.
3. Per-round inequality (pp. 12–13): $v_i(X^j_-)-v_i(X^{j-1}_-)\ge v_i(X^{j-1}_-\cup Y^j_+)-v_i(X^j_-\cup Y^{j+1}_+)$.
4. Telescoped bound (p. 13): $v_i(X)\ge v_i(Y)-v_i(X)$.
5. Tight instance, bluff run (p. 13). On the two-agent instance with an additive and an OXS agent, the bluff order is $g_1\succ\cdots\succ g_5$, and the bluff run gives $v_1(A_1)=4-\varepsilon_1-\varepsilon_3$ and $v_2(A_2)=1$.
6. Tight instance, deviation (pp. 13–14). Agent 2 reaches $2-\varepsilon_1-\varepsilon_2$ by reporting $g_3\succ g_4\succ g_1\succ g_2\succ g_5$.

Companion statements: Theorem 3.8 (p. 14: the bluff allocation is $\tfrac12$-EF1, tight) and Proposition 3.4 (p. 10: an instance with no $(\tfrac34+\varepsilon)$-approximate PNE).

Significance

The theorem settles existence for a class where exact existence fails. Proposition 3.4 shows that submodular agents can make every profile unstable, so an approximate equilibrium is the most one can ask for, and Theorem 3.7 exhibits one with the explicit factor $\tfrac12$ by a polynomial-time construction. Theorem 3.8 turns the equilibrium bound into a fairness bound, $\tfrac12$-EF1 for the bluff allocation. The paper's §4 then shows that every approximate equilibrium of Round-Robin is approximately EF1 for submodular agents, so the existence result here is what makes those fairness guarantees non-vacuous.

The result is proved in the paper; none of it, nor Round-Robin as a mechanism, has a machine-checked proof that we know of. Formalizing it adds a reusable layer for discrete fair division: valuation classes, Round-Robin with step-level bookkeeping, approximate PNE and approximate EF1. On top of that layer come a rigorous proof of the coupling argument and a checked tight instance. The other three missions of this series reuse the same model.

Difficulty

The obvious approach compares agent $i$'s bundle under the bluff profile with her bundle after a deviation, one good at a time. In the cancelable case this works by a swapping argument. For submodular valuations the value of a good depends on what the agent already holds, so a good-wise comparison is only meaningful relative to a carefully chosen ordering of the deviation bundle. That ordering is Algorithm 3, which renames the goods backwards by minimum marginal value against prefixes of the bluff bundle.

Even with that ordering, the good-wise inequality of Lemma 3.5 does not by itself bound $v_i(Y)$ by $v_i(X)$; the analogue of the cancelable lemma that would do so is missing. The bound comes from an interleaving of prefixes of $X$ with suffixes of $Y$, and that is where the factor $2$ is lost. The proof of Lemma 3.5 must also follow how a single deviation shifts which goods every other agent receives, step by step, in two coupled runs of the mechanism. This counting is the bulk of the work in Lean.

Formalization scope

Agents are Fin n with [NeZero n]; goods are a Fintype with decidable equality. Valuations are real-valued and carry normalization and monotonicity. Submodularity is the paper's marginal form, not the lattice form. Rankings are lists that contain every good exactly once, and deviations in the PNE definition range over rankings only. Round-Robin is computed step by step: step $t$ (0-based) belongs to agent $t \bmod n$.

Committed conventions:

• $m=kn$ is a hypothesis of every statement. The paper assumes it "for simplicity" and calls it without loss of generality by appending dummy goods. That reduction is not formalized. The tight instance accordingly has a sixth, zero-value good.
• Greedy orders are relational. IsGreedyOrder v h admits every tie-breaking of Algorithm 2, and the theorems quantify over all of them, so they include the paper's lexicographic bluff profile. The tightness parts hold for every greedy order of the instance, and the instance must admit one.
• Algorithm 3 is relational as well: an injective listing of the deviation bundle whose $j$-th entry minimizes the marginal value against $\{x_1,\dots,x_{j-1}\}$ among $y_1,\dots,y_j$.

Trivializing formalizations are ruled out by four requirements. Deviations range over rankings, not arbitrary lists. The approximation factors are the paper's $\tfrac12$ and $\tfrac12+\varepsilon$ with $\varepsilon>0$. The bluff profile is Algorithm 2's output, not an arbitrary profile. The goal contains the tightness part.

Reusable beyond this mission: the Round-Robin model, valuation classes, approximate PNE and EF1. Welcome contributions include API lemmas about allocBefore and roundRobin (bundle sizes, the bluff run allocating $h$ in order, the effect of a single deviation) and the submodularity of OXS valuations.

Selected references

• G. Amanatidis, G. Birmpas, P. Lazos, S. Leonardi, R. Reiffenhäuser, Round-Robin Beyond Additive Agents: Existence and Fairness of Approximate Equilibria, arXiv:2301.13652v1, 2023; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2301.13652
• G. Amanatidis, G. Birmpas, F. Fusco, P. Lazos, S. Leonardi, R. Reiffenhäuser, Allocating Indivisible Goods to Strategic Agents: Pure Nash Equilibria and Fairness, WINE 2021, LNCS 13112, 149–166. https://arxiv.org/abs/2109.08644
• H. Aziz, P. Goldberg, T. Walsh, Equilibria in Sequential Allocation, ADT 2017, LNCS 10576, 270–283.
• S. Bouveret, M. Lemaître, Characterizing Conflicts in Fair Division of Indivisible Goods Using a Scale of Criteria, Autonomous Agents and Multi-Agent Systems 30(2), 259–290, 2016.
• R. J. Lipton, E. Markakis, E. Mossel, A. Saberi, On Approximately Fair Allocations of Indivisible Goods, EC 2004, 125–131. https://doi.org/10.1145/988772.988792
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial Auctions with Decreasing Marginal Utilities, Games and Economic Behavior 55(2), 270–296, 2006. https://doi.org/10.1016/j.geb.2005.02.006

Motivation

The European Union's General Data Protection Regulation (GDPR, 2018) requires a firm to obtain a consumer's explicit consent before it collects personal data. The common expectation, in policy debate and in much of the empirical literature, is that consent requirements cost firms money: they shrink the pool of consumer data that can be monetized through advertising, personalization or resale. Choe, Matsushima and Shekhar (ISER Discussion Paper No. 1246, 2024; published as Management Science, 2025) build a monopoly pricing model in which consent creates a new purchase option. A consumer who would not have bought the service under compulsory data sharing can now buy it without sharing. They then ask how the firm's equilibrium price, profit and consumer surplus change.

This mission formalizes the paper's analytic profit result. If the firm's revenue is mostly usage based, meaning its revenue per unit of collected data is small, then the firm earns strictly more in equilibrium after the GDPR than before. The result is the source of the paper's title. Regulation that is usually read as a cost to firms raises the profit of one well-defined class of firms.

Setting

A monopolist sells an online service at zero marginal cost and sets a price $p\in\mathbb R$. Negative prices are allowed: they pay consumers to use the service. A consumer type is a pair $(v,c)\in[0,1]^2$, where $v$ is the valuation of the service and $c$ the privacy cost of sharing data. Types are independent and uniform on the unit square, so the mass of a set of consumers is its area. A consumer who shares data receives an opt-in benefit $x\in(0,1)$. The utilities of opt-in purchase (buy and share) and opt-out purchase (buy without sharing) are

$$U_S(v,c)=v+(x-c)-p,\qquad U_N(v,c)=v-p .$$

The firm earns data revenue $\alpha\ge0$ per unit of collected data. Its profit is $\Pi=pD+\alpha D_S$, where $D$ is total demand and $D_S$ the mass of consumers who share data.

• Before the GDPR opt-out purchase is unavailable. A consumer buys, and shares, iff $U_S\ge0$. The demand $\widehat D(p)$ is the area of $\{(v,c)\in[0,1]^2: U_S\ge 0\}$, and the profit is $\widehat\Pi(p)=(p+\alpha)\widehat D(p)$.
• After the GDPR the opt-in buyers are $\{(v,c)\in[0,1]^2 : c\le v+x-p,\ c\le x\}$ and the opt-out buyers are $\{(v,c)\in[0,1]^2: v\ge p,\ c>x\}$. Their areas are $\widetilde D_S(p)$ and $\widetilde D_N(p)$, and the profit is $\widetilde\Pi(p)=p(\widetilde D_S(p)+\widetilde D_N(p))+\alpha\widetilde D_S(p)$.

An equilibrium price is a global maximizer of the profit over $p\in\mathbb R$: the firm moves first and consumers respond. The paper's thresholds are

$$\alpha_1(x)=\max\Big\{\frac{1-2x}{2},0\Big\},\qquad \alpha_2(x)=\max\Big\{\frac{2-4x+x^2}{2x},0\Big\}.$$

"Case 1a" (before) and "case 2a" (after) are the equilibria with $x<p^\star<1+x$, in which low-valuation consumers stay out of the market.

Formalization targets

Goal: Proposition A3, first bullet (p. 34)

If $\alpha<\alpha_1(x)$, both profit functions attain their maxima over $\mathbb R$, and

$$\max_{p\in\mathbb R}\widetilde\Pi(p)\;>\;\max_{p\in\mathbb R}\widehat\Pi(p),$$

that is, $\widetilde\Pi^\star_{2a}>\widehat\Pi^\star_{1a}$. The hypothesis forces $x<1/2$, because $\alpha\ge0$.

Milestones

1. Lemma A3, first bullet (p. 33): for $x\le 1/2$ and $\alpha<\alpha_1(x)$, every equilibrium price before the GDPR lies in $(x,1+x)$ (case 1a), and so does every equilibrium price after it (case 2a).
2. Equilibrium profit before the GDPR (p. 31): for $\alpha<\alpha_1(x)$, $\widehat\Pi^\star=2(1+x+\alpha)^3/27$.
3. Equilibrium profit after the GDPR (p. 32): for $\alpha<\alpha_2(x)$, $\widetilde\Pi^\star=\big(4+4x(x+2\alpha+2\alpha x)+x^2(x-2\alpha)^2\big)/16$.
4. Online Appendix §F, first display (OA p. 9): for $\alpha<\alpha_1(x)$, $\widetilde\Pi^\star-\widehat\Pi^\star=J(x,\alpha)/432$, with $J$ the explicit quartic polynomial printed there.
5. Online Appendix §F, conclusion (OA p. 9): $J(x,\alpha)>0$ whenever $0<x<1/2$ and $0\le\alpha<(1-2x)/2$.

Significance

The result. Proposition A3 separates firms by revenue model. A firm whose revenue is mostly usage based gains from the GDPR. The opt-out option brings in consumers with high privacy costs who did not buy before, and this extra demand lets the firm both raise its price and sell to more consumers. Together these outweigh the lost data revenue. The other two bullets of Proposition A3 treat firms with larger $\alpha$, for which the comparison can go either way. Their thresholds $\alpha_5(x)$ and $\alpha_6(x)$ are defined only as "the value of $\alpha$ that solves" an equation, with existence and uniqueness shown in plots, so they are not posed here. The paper's Propositions 1–4 are its main-text results at $x=1/4$. The price comparison (Proposition 1) is the $x=1/4$ instance of the general Proposition A1, the subject of the sibling mission in this series. Propositions 2–4, A2, A3 (bullets 2–3) and A4 rest on numerically located thresholds and are not posed.

Formalizing it. The paper's proof is in print, but no part of it has been machine-checked. The model is fully explicit (a uniform distribution, two areas, two profit functions on $\mathbb R$), so a complete formal proof would certify every link from the primitives to the inequality. That covers the computation of the polygon areas, the global maximization of a piecewise polynomial over all real prices, and the final polynomial inequality. The printed proof of the last step contains a slip: the value it gives for "$J(x,\alpha_1(x))$" is the value of $J/432$. A formalization fixes such details for good.

Difficulty

The closed forms are easy to verify once the equilibrium is known to be interior to case 1a and case 2a. The work lies elsewhere. Computing the demands requires the Lebesgue area of a family of polygons whose shape changes with $p$. Over all of $\mathbb R$ each demand is piecewise polynomial with several pieces, and the profits are piecewise cubic. Identifying the global maximizer means checking every piece, including negative prices before the GDPR and the corner pieces where demand saturates at $0$ or $1$. A first-order condition on one piece gives only a candidate. The comparison of the two maximal values then reduces to a two-variable quartic inequality on a triangle, which holds strictly on the open region but becomes tight at its corner $x\to0$, $\alpha\to1/2$, where $J(0,1/2)=0$.

Formalization scope

• Model. One definitions file, GDPRPrivacy.PriceRise.Model, shared with the sibling mission on the equilibrium price. A type is q : ℝ × ℝ with q.1 = v and q.2 = c. Demands are (volume S).toReal for the explicit sets $S\subseteq[0,1]^2$ above, with the opt-in and opt-out sets of p. 13 copied literally. Ties are assigned to opt-in, which changes only null sets. The file also defines $\alpha_1,\alpha_2,\beta,\Gamma$.
• Standing assumptions. Every theorem assumes $0<x<1$ and $\alpha\ge0$ (§3, pp. 7–8). No other hypothesis is added. Milestone 1 keeps the paper's $x\le 1/2$, and milestone 5 keeps its printed region $\alpha<(1-2x)/2$, $x<1/2$.
• Equilibria. An equilibrium price is any p with IsMaxOn (profitBefore x α) Set.univ p (respectively profitAfter). Every statement asserts that a maximizer exists and then quantifies over all maximizers.
• Ruled-out trivializations. The goal compares the maximal values of the two model profit functions. It does not compare the closed forms $2(1+x+\alpha)^3/27$ and $\widetilde\Pi^\star_{2a}$ (that is milestones 4–5 alone), it does not compare the profits at a common price, and it does not restrict the price range. The existence conjuncts prevent a vacuous "for every maximizer".
• Needed infrastructure. Areas of polygons in $\mathbb R^2$ via MeasureTheory.volume (Fubini or regionBetween), maximization of piecewise polynomials on $\mathbb R$, and polynomial inequalities. Lemmas computing the area of $\{(v,c)\in[0,1]^2: c\le v+t\}$ as a function of $t$ are reusable for other uniform-type screening and pricing models. Contributions of such lemmas, and of the explicit demand formulas (4)–(6) of the paper, are welcome.

Selected references

• C. Choe, N. Matsushima and S. Shekhar, The Bright Side of the GDPR: Welfare-Improving Privacy Management, ISER Discussion Paper No. 1246, Osaka University, June 2024. The artifact formalized here; theorem and page numbers refer to it.
• C. Choe, N. Matsushima and S. Shekhar, The Bright Side of the GDPR: Welfare-Improving Privacy Management, Management Science, 2025. https://doi.org/10.1287/mnsc.2024.06653
• S. P. Anderson and J. S. Gans, Platform Siphoning: Ad-Avoidance and Media Content, American Economic Journal: Microeconomics 3(4), 2011. https://doi.org/10.1257/mic.3.4.1
• Regulation (EU) 2016/679 (General Data Protection Regulation), Official Journal of the European Union L 119, 2016. https://eur-lex.europa.eu/eli/reg/2016/679/oj