All missions

Motivation

Firms that sell to the same customers over time learn who bought from whom. Behavior-based pricing (BBP) — charging a firm's own past customers one price and the rival's past customers another — has been studied since Fudenberg and Tirole (2000) and Villas-Boas (1999). A second instrument is the disclosure of product quality: free samples, demonstrations and trial versions reveal the quality of a new product, at a cost per customer reached. With purchase histories, a firm can disclose differently to its own customers and to the rival's: behavior-based disclosure (BBD). The classical disclosure model is Jovanovic (1982), in which costly disclosure leads a firm to reveal quality only above a threshold.

Zhang and Li (2025) combine the two instruments in a two-period Hotelling duopoly and compare BBD with uniform disclosure. Their Proposition 1 shows that BBD always raises second-period profits; this mission is about the whole game, where the answer depends on the disclosure cost.

Setting

A unit mass of customers is uniformly distributed on $[0,1]$; firm A is at $0$, firm B at $1$, the transportation cost is $1$, marginal costs are $0$ and the market is fully covered.

Period 1. The firms charge prices $p_{a1},p_{b1}\ge 0$. The first-period purchase splits the line at $x_1$: A's old customers are $[0,x_1]$ (A's turf), B's are $[x_1,1]$ (B's turf).

Period 2. Each firm $i$ launches a new product of quality $q_i$, with $q_a,q_b$ independent and uniform on $[0,1]$. A firm discloses its quality to a segment iff it exceeds a disclosure threshold $\hat q$; disclosing costs $c$ per customer reached. A segment that sees no disclosure believes the quality is $\hat q/2$. Under uniform disclosure each firm has one threshold $\hat q_i$ for the whole line; under BBD it has $\hat q_{io}$ for its own customers and $\hat q_{in}$ for the rival's. On each turf the two firms then play a price game (A charges $p_{ao}$ and B charges $p_{bn}$ on A's turf; $p_{an}$ and $p_{bo}$ on B's turf), and customers stay or switch according to their beliefs and prices.

Forward-looking customers. The share $x_1$ is the location of the marginal consumer, who compares the two first-period options including the expected second-period surplus of staying or switching ((6) for uniform disclosure, (15) for BBD):

$$-x_1-p_{a1}+\max\{-(1-x_1)+E(\tilde q_{bn}-p^*_{bn}),\,-x_1+E(\tilde q_{ao}-p^*_{ao})\}=-(1-x_1)-p_{b1}+\max\{-x_1+E(\tilde q_{an}-p^*_{an}),\,-(1-x_1)+E(\tilde q_{bo}-p^*_{bo})\}.$$

Two-period profits (8) are $\Pi_a=p_{a1}x_1+E(\pi_{a2})$ and $\Pi_b=p_{b1}(1-x_1)+E(\pi_{b2})$, with $E(\pi_{i2})$ the ex ante second-period profit at share $x_1$. A symmetric subgame-perfect equilibrium is a common first-period price $p^*$ together with a second-period equilibrium at every share and a consistent share at every price pair, such that neither firm gains from any other nonnegative first-period price. Its total profits are $\Pi^*_a,\Pi^*_b$.

The standing assumption is $0<c<5/36$ (p. 8515).

Formalization targets

Goal: Proposition 3(a)

There is a cutoff $c_l\in(0,5/36)$ such that for every $c\in(0,5/36)$, symmetric subgame-perfect equilibria exist under both regimes and, for any two of them,

$$c>c_l\;\Rightarrow\;\Pi^{*,U}_i<\Pi^{*,BBD}_i,\qquad c<c_l\;\Rightarrow\;\Pi^{*,BBD}_i<\Pi^{*,U}_i\qquad (i=a,b).$$

The value of $c_l$ is left unfixed, as in the paper.

Milestones

1. (5) and (14): the ex ante second-period profit as a function of $x_1$ and the equilibrium thresholds, in region 1, e.g. under BBD

$$E(\pi_{a2})=\tfrac{(1+2x_1)^2+(3-4x_1)^2}{18}+\tfrac{4-\hat q_{ao}^3-\hat q_{an}^3-\hat q_{bo}^3-\hat q_{bn}^3}{216}-c\,[1-x_1\hat q_{ao}-(1-x_1)\hat q_{an}].$$

2. (7) and (16): in region 1 the first-period share is $x_1=\tfrac12+\tfrac38(p_{b1}-p_{a1})$ under both regimes.
3. (9) and (17): existence of symmetric equilibria, and their prices

$$p^{*,U}=\tfrac23\big(2-c+\tfrac{c}{\sqrt{1+27c}}\big),\qquad p^{*,BBD}=\tfrac43-\tfrac{c(5+54c)}{3\sqrt{1+12c}}+\tfrac{c(5+162c)}{3\sqrt{1+108c}},$$

with share $x_1^*=\tfrac12$. 4. Table 1, total profits, both regimes, in closed form. 5. Proposition 2: a cutoff $c_h\in(0,5/36)$ across which the comparison of first-period prices and profits reverses.

Significance

Proposition 3(a) is the paper's answer to the managerial question in its title. BBD lets a firm disclose to its own customers more often than to the rival's (retention-focused disclosure), which improves the efficiency of disclosure and raises second-period profits. In the first period, however, BBD changes how hard firms compete for customers, and when disclosure is cheap the first-period loss dominates. The result locates the sign change of the total effect at a single cutoff, and together with Proposition 2 ($c_l<c_h$) it separates three regimes of $c$: total profits fall, total profits rise despite lower first-period profits, and both rise.

None of these results is formalized anywhere. The paper's proofs are in an Online Appendix and its displayed formulas are the end points of long computations. A complete development would produce:

• a machine-checked solution of a two-period Hotelling model with behavior-based pricing, including corner regions of the second-period price game;
• a costly-disclosure equilibrium in the Jovanovic style;
• a verified single-crossing analysis of algebraic functions of $c$.

Difficulty

The model nests three equilibrium notions: a clamped price game on each turf, threshold disclosure as a best response to the rival and to the induced beliefs, and first-period pricing with forward-looking customers. The first-order condition behind (9) and (17) involves the derivative of $E(\pi_{a2})$ in $x_1$, and every threshold, including the rival's, moves with $x_1$; treating the rival's thresholds as fixed gives a wrong price.

The symmetric first-order condition alone does not settle the equilibrium. A deviation in first-period price can push the share outside the region where all second-period prices are interior, into the corner regions 2 and 3 of Lemma 1/2, where the second-period profit has a different form. The paper checks these deviations only in its Online Appendix.

The final comparison is a sign analysis of an expression with three different square roots on $(0,5/36)$. The difference of total profits is small throughout: for example, about $-5\cdot10^{-4}$ at $c=0.01$ and $3.5\cdot10^{-3}$ at $c=0.1$.

Formalization scope

• Representation. Qualities are integrated by iterated interval integrals over $[0,1]$. The base value $v$ cancels and is omitted; full coverage is built in. Prices are nonnegative, turf shares are clamped to the turf, and the nondisclosure belief stays $\hat q/2$ when a firm considers a deviation.
• Equilibria, not formulas. Second-period prices are Nash equilibria of the clamped turf games for every belief pair in $[0,1]^2$. Thresholds are best responses ("disclose iff $q>\hat q$" is optimal), never roots of the indifference equation. The share satisfies (6)/(15) as printed, a maximum of two expectations, with corner shares $x_1\in\{0,1\}$ read through nearby interior shares (at an endpoint one turf is empty and its second-period prices are not pinned down, so (6)/(15) is not evaluated there). First-period deviations range over all nonnegative prices, and the second-period profile is an equilibrium at every share, including shares reached only after a deviation.
• Readings. "In region 1" for (5), (7), (14), (16) means that every belief pair on the support is in region 1: $\tfrac12-\hat q_{bn}/8<x_1<\tfrac12+\hat q_{an}/8$ (BBD), $\tfrac12-\hat q_b/8<x_1<\tfrac12+\hat q_a/8$ (uniform). Table 1's uniform total profit is used; the sentence on p. 8517 prints $\sqrt{1+72c}$ for $\sqrt{1+27c}$.
• Ruled out. Hard-wiring $x_1=\tfrac12$, defining thresholds or prices by their closed forms, or stating the goal on the Table 1 formulas alone would each trivialize the mission; the cutoff is quantified before $c$ and lies strictly inside $(0,5/36)$, and existence of equilibria is part of the goal.
• Not posed. Proposition 3(b), (c) (consumer surplus and welfare are defined in the paper only by their Table 1 values) and Proposition 4.
• Needed. Piecewise-quadratic integrals over the belief support; Nash equilibria of clamped linear-demand games; existence of a consistent first-period share (an intermediate-value argument on a suitable equilibrium selection); and sign analysis with square roots. The second-period model is the same as in the companion mission on Proposition 1, and lemmas about it are reusable there. Contributions of any of the milestones, of Lemma 1/2 in all regions, or of the corner-region versions of (4), (5), (13), (14) are welcome.

Selected references

• J. Zhang and K. J. Li, Retention or Acquisition? Behavior-Based Quality Disclosure, Management Science 71(10), 8510–8525, 2025. https://doi.org/10.1287/mnsc.2022.01081
• D. Fudenberg and J. Tirole, Customer Poaching and Brand Switching (cited in Zhang and Li as "Customer poaching and firm switching"), RAND Journal of Economics 31(4), 634–657, 2000.
• J. M. Villas-Boas, Dynamic Competition with Customer Recognition, RAND Journal of Economics 30(4), 604–631, 1999.
• B. Jovanovic, Truthful Disclosure of Information, Bell Journal of Economics 13(1), 36–44, 1982.

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

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

A correlated equilibrium (Aumann, 1974) is an equilibrium of a game with a mediator: the mediator draws a profile of recommendations from a known distribution and tells each player privately what to play. The distribution is an equilibrium if no player gains by deviating from the recommendation they receive. Correlated equilibria can give higher payoffs than Nash equilibria, they are cheaper to compute, and many adaptive learning procedures converge to them.

Mean field games describe symmetric games with many players, each of whom interacts with the others only through the empirical distribution of their states. The standard justification of a mean field model is an approximation theorem: a solution of the limit game induces approximate equilibria of the games with $N$ players, with an error that vanishes as $N\to\infty$.

Correlated solutions of discrete-time mean field games were introduced by Campi and Fischer (arXiv:2004.07936) for restricted strategies, in which both the recommendations and the deviations are Markov in the player's own state. Bonesini, Campi and Fischer (arXiv:2212.01656) keep restricted recommendations but allow the deviating player to use progressive strategies, which see the whole history of the system, together with a private randomization device. This mission formalizes their main approximation result, Theorem 6.2.

Setting

Time runs over $[\![0,T]\!]$. States lie in a finite set $\mathcal X$ and actions in a finite set $\Gamma$. Noise variables are uniform on $\mathcal Z=[0,1]$; their law is $\nu$. The set $\mathcal P(\mathcal X)$ of probability measures on $\mathcal X$ carries the metric $\mathrm{dist}(\mu,\tilde\mu)=\frac12\sum_x|\mu(x)-\tilde\mu(x)|$. A player's state moves by

$$X_{t+1}=\Psi(t,X_t,\mu_t,u_t,\xi_{t+1}),$$

where $\mu_t$ is the distribution of the other players' states, $u_t\in\Gamma$ is the player's action and $\xi_{t+1}\sim\nu$ is idiosyncratic noise. The player pays a running cost $f(t,X_t,\mu_t,u_t)$ and a terminal cost $F(X_T,\mu_T)$.

A restricted strategy $\varphi\in\mathcal R$ is a map $(t,x)\mapsto\varphi(t,x)\in\Gamma$. A progressive strategy $\varphi\in\widehat{\mathcal R}$ chooses the action at time $t$ as a Borel function of the player's state history $x^{(t)}$ and the history $m^{(t)}$ of the measure flow.

$N$-player game. The mediator draws $(\Phi_1,\dots,\Phi_N)$ from a correlated suggestion $\gamma^N$. Every player $j$ applies $\Phi_j$ to their own state path and to the empirical measure $\mu^{j,N}$ of the other $N-1$ players. A strategy modification of player $i$ replaces $\Phi_i$ by a progressive strategy $\tilde\Phi_i$. At time $t$ the component $\tilde\Phi_i(t,\cdot)$ may depend on $\Phi_i$ and on an independent uniform variable $\vartheta_t$; the set of joint laws of $(\Phi_i,\tilde\Phi_i)$ obtained this way is $\mathcal N^N_{\gamma^N_i}$. Player $i$'s expected cost is $J^N_i(\mathfrak m^N,\gamma^N,\tilde\gamma)$. The suggestion $\gamma^N$ is an $\varepsilon$-correlated equilibrium if no player gains more than $\varepsilon$ by any modification.

Mean field game. The mediator draws a pair $(\Phi,\mu)$ from $\rho\in\mathcal P(\mathcal R\times\mathcal P(\mathcal X)^{T+1})$: a restricted recommendation and a random flow of measures. The representative player may deviate through any map $w:\mathcal R\to\widehat{\mathcal R}$. The pair $\rho$ is a correlated solution if following the recommendation is optimal (Opt), and if, in that case, $\mu_t$ is the conditional law of $X_t$ given the whole flow $\mu$ (Con).

Formalization targets

Goal: Theorem 6.2

Assume (A1)–(A3), and let $\rho$ be a correlated solution with initial law $\mathfrak m_0$ satisfying (R1)–(R2). Write $\rho(d\varphi,dm)=\rho_1(d\varphi|m)\rho_2(dm)$. Then there are $\varepsilon_N\ge0$ with $\varepsilon_N\to0$ such that, for every $N\ge2$,

$$\gamma^N(C_1\times\cdots\times C_N)=\int\prod_{j=1}^N\rho_1(C_j|m)\,\rho_2(dm)$$

is an $\varepsilon_N$-correlated equilibrium with initial law $\mathfrak m_0^{\otimes N}$.

Milestones

The milestones follow the proof:

• the identification of $\gamma^N$ (Remark 6.3) and the two disintegrations (6.4), (6.5);
• convergence of the cost when nobody deviates, (6.2);
• the conditional dynamic programming principle for the value function $V_\varphi$ of a player who received the suggestion $\varphi$ (Proposition 5.5), and the equivalence of closed-loop and open-loop solutions (Proposition 5.6);
• three limits in the coupling of the deviation argument, (6.20), Claim 6.4 and (6.34);
• the lower bound for a deviating player, (6.3).

An additional milestone, (4.3), states that the cost does not depend on the realization.

Significance

The theorem justifies correlated mean field solutions as models of large games with a mediator. It applies when the mediator's recommendations and the population flow are genuinely random, and when deviators may use the full history of the system. The paper's Section 7 gives an explicit example satisfying all its hypotheses. In that example the flow of measures is non-deterministic, so the correlated solution is not a mixture of Nash solutions.

No part of this result has a machine-checked proof. Formalizing it requires:

• a complete account of correlated equilibria for dynamic games in Lean: suggestions, randomized strategy modifications, realizations;
• a conditional law of large numbers for empirical measures;
• the open-loop/closed-loop equivalence of Section 5.

These components are reusable beyond this paper.

Difficulty

When the flow $\mu$ is deterministic, the usual propagation-of-chaos argument for Nash approximation applies. Here it does not, for three reasons.

• The flow is random, and every player's recommendation is correlated with it. Convergence must therefore be proved conditionally on the flow, and the disintegrations (6.4)–(6.5) are needed for this.
• The deviating player sees the empirical measures of the others and may use extra randomness. The limit of their behaviour is not a closed-loop strategy of the mean field game. Optimality against it requires the open-loop formulation, Proposition 5.6, whose proof uses a conditional dynamic programming principle under (R1).
• The empirical measure seen by the deviator is perturbed by the deviation itself. Claim 6.4 and (6.34) control this perturbation through the continuity assumption (A2).

Formalization scope

Lean conventions:

• Spaces. $\mathcal X$ and $\Gamma$ are Fintypes with the discrete σ-algebra. $\mathcal P(\mathcal X)$ is stdSimplex ℝ X with its subspace topology and Borel σ-algebra. $\nu$ is volume on unitInterval.
• Indexing. States and flows are indexed by Fin (T+1), and actions and noises by Fin T; the noise $\xi_{t+1}$ has index $t$. Players are Fin N, and the paper's player 1 is index 0.
• Strategies. Progressive strategies are non-anticipative, measurable functions of full paths. $N$-player strategies read empirical measures of $N-1$ points, so $\widehat{\mathcal R}_N$ is finite and carries the discrete σ-algebra.
• The private coin. Condition v) of Definition 3.1 says that $\tilde\Phi_i(t,\cdot)$ is $\sigma(\Phi_i,\vartheta_t)$-measurable. It is stated literally. $\mathcal N^N_\gamma$ is defined from kernels as in (3.1).
• Realizations. A realization is a structure on a probability space Ω : Type. Conditions i)–iv) form a single product-law identity, and the dynamics hold almost surely. Completeness of the spaces and filtrations is dropped. Costs are the expected costs of realizations, and every inequality or limit between costs is required for every realization (or sequence of realizations) of each side.
• Equilibrium. In the $\varepsilon_N$-equilibrium, one $\varepsilon_N$ serves every player and every modification. All $N$-player statements assume $N\ge2$, and sequences run along $N=n+2$.
• (Con) conditions on $\sigma(\mu)$ of the whole flow, via Lean's condExp.
• (R2) is read in distribution (Remark 6.1). $\rho_1$ is any kernel that disintegrates $\rho$ along its second marginal.
• Implicit hypotheses made explicit. Joint measurability of $\Psi$ is added. (A3) is stated as Lipschitz continuity in the measure argument with one constant.
• $V_\varphi$ (Proposition 5.5) is defined through the explicit representation (5.10) of the conditional cost, a sum over flows weighted by $\mathbb P_\varphi(\mu=m'\mid\mu^{(t)}=m^{(t)})$, rather than by conditioning on events. The proposition is stated with $V_\varphi(t+1,\dots)$ on the right, as in its proof; the printed statement has $t$.
• (6.3) is stated for every sequence of modifications, which is equivalent to the paper's near-minimizing sequence. A $\liminf$ bound is written as "for every $\delta>0$, eventually".

Ruled out: none of the following is a faithful formalization of this mission:

• a deterministic flow (a Dirac $\rho_2$);
• deviations without the private coin, or restricted to $\mathcal R$;
• (Con) conditioned on $\mu^{(t)}$ only;
• an arbitrary kernel in place of the disintegration $\rho_1$.

Sorry-free checks in the workspace show that realizations of both games and the coupling exist, so the realization predicates are not vacuous.

Needed infrastructure, and welcome contributions:

• conditional laws of large numbers for empirical measures of finite-state particles;
• propagation of chaos in the sense of Kac–Sznitman;
• disintegration lemmas for finite product kernels.

Selected references

• O. Bonesini, L. Campi, M. Fischer, Correlated Equilibria for Mean Field Games with Progressive Strategies, arXiv preprint, 2022. https://arxiv.org/abs/2212.01656
• L. Campi, M. Fischer, Correlated equilibria and mean field games: a simple model, Mathematics of Operations Research 47(3):2240–2259, 2022. https://arxiv.org/abs/2004.07936
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1(1), 1974. https://doi.org/10.1016/0304-4068(74)90037-8
• A. D. Gottlieb, Markov Transitions and the Propagation of Chaos, PhD thesis, University of California, Berkeley, 1998 (the chaos theorem cited as Theorem A.1). https://arxiv.org/abs/math/0001076