All missions

Motivation

Ride-hailing, car-sharing and bike-sharing platforms price trips whose execution moves the resource itself: a car that takes a passenger from the suburbs to the airport is no longer available in the suburbs. Each price therefore sets both the revenue of the current request and the future spatial distribution of the fleet. Choosing prices to maximise long-run revenue is a Markov decision problem whose state, the number of resources at each location, has a number of configurations exponential in the number of locations. Exact dynamic programming is impossible at the scale of a city.

Balseiro, Brown and Chen (SSRN 3313737, version of May 23, 2020; published in Management Science, doi:10.1287/mnsc.2020.3735) study hub-and-spoke networks and propose a Lagrangian policy. The capacity constraint coupling the locations is relaxed with a dual variable, the relaxation separates into one small problem per spoke, and the per-spoke solutions are implemented in the real system. Earlier work on this model (Waserhole and Jost, 2016; Banerjee, Freund and Lykouris, 2016) uses fluid relaxations that lead to static prices, depending on the origin and destination but not on the resource levels. These are within a factor $m/(m+n-1)$ of the fluid bound, hence asymptotically optimal when the number of resources $m$ grows faster than the number of locations $n$. When $m$ and $n$ grow at the same rate, which is the regime of a large city with few vehicles per area, no static policy is asymptotically optimal (the paper's Example 5.1). The Lagrangian policy is a dynamic, state-dependent policy that is computable and asymptotically optimal in that regime.

Setting

A hub (location $0$) and $n$ spokes $i\in[n]$ share $m$ resources. In each period one request arrives: it asks to relocate a resource from spoke $i$ to the hub, type $(i,0)$, with probability $q_{i0}>0$, or from the hub to spoke $i$, type $(0,i)$, with probability $q_{0i}>0$; these probabilities sum to one and are independent across periods. The provider picks a demand level $d\in[0,1]$, equivalently a price. The request is fulfilled with probability $d$ if its origin holds a resource and is lost otherwise; the expected revenue is $r_{ij}(d)$. Assumption 2.1: each $r_{ij}$ is strictly concave on $[0,1]$, $r_{ij}(0)=0$, $\max r_{ij}\le\bar r$, $\max|r_{ij}'|\le\bar\omega$, and the maximiser is interior.

The state is the vector of spoke levels $x\in\mathcal X=\{x\in\mathbb N^n:\sum_ix_i\le m\}$, the hub holding $x_0=m-\sum_ix_i$. The optimal average revenue $V^{\mathrm{OPT}}$ (problem (1)) is the supremum, over non-anticipative feasible policies, of the long-run average expected revenue.

Penalising the spoke resources with a dual variable $\lambda\ge0$ yields, for each spoke, the spoke problem (6): maximise $\sum_xp_i(x)[q_{i0}r_{i0}(d_i(x,i,0))+q_{0i}r_{0i}(d_i(x,0,i))]-\lambda\sum_xx\,p_i(x)$ over a distribution $p_i$ on $[0:m]$ and controls satisfying the birth–death balance equations $p_i(x)q_{0i}d_i(x,0,i)=p_i(x+1)q_{i0}d_i(x+1,i,0)$. Its value is $h_i^\lambda$. The relaxation value is $\bar V^\lambda=m\lambda+\sum_ih_i^\lambda$ (4), the Lagrangian bound is $V^{\mathrm R}=\min_{\lambda\ge0}\bar V^\lambda$ (9), and the perturbed dual is $V^{\mathrm R}(\delta)=\min_{\lambda\ge0}\bar V^\lambda-\delta\lambda$ (11), with optimal solution $\lambda^*(\delta)$. The Lagrangian policy $\pi(\delta)$ (Definition 3.1) applies the controls of optimal solutions of (6) at $\lambda^*(\delta)$, spoke by spoke, and drops a hub request when the hub is empty. $V^{\pi(\delta)}$ is its average revenue and $\mathbb P[X_0(\delta)=0]$ the stationary probability that the hub is empty. In the relaxed system the hub may go negative; there the spokes are independent with laws $p_i$.

Formalization targets

Goal: Corollary 4.7

Under Assumption 4.1 ($\mathbb E[\tilde X_i(\delta)]\le c$ for every spoke, $c>0$ independent of $n$) and with $b=1/(1+c)$, for $0\le\delta<m$,

$$V^{\pi(\delta)}\le V^{\mathrm{OPT}}\le V^{\mathrm R}\le V^{\pi(\delta)}+\bar r\,\frac{\delta}{m-\delta}+(\bar r+\bar\omega)\exp\Big(-\frac b2\cdot\frac{\delta^2}{m+n}\Big),$$

and with $\delta=\sqrt{(1/b)(m+n)\ln n}$,

$$V^{\mathrm{OPT}}-V^{\pi(\delta)}=O\Big(\sqrt{\ln n/n}\Big)\quad\text{when }m\text{ and }n\text{ grow at the same rate.}$$

Milestones

The milestones follow the paper's proof. The spoke problem solves the spoke Bellman equation (Proposition 3.2), the relaxation's value is independent of the initial state, equals $m\lambda+\sum_ih_i^\lambda$ and bounds $V^{\mathrm{OPT}}$ (Proposition 3.1), and the controls are monotone (Proposition 3.3). The relaxed and original chains have stationary laws $\prod_ip_i$ and a unique $\mu$ (Corollaries B.10, B.11). The perturbation costs at most $\bar r\delta/(m-\delta)$ (Lemma 4.2), continuation-value differences are at most $\bar\omega$ (Lemma A.10), and the relaxed–original gap is controlled by hub depletion (Lemma 4.3), giving Theorem 4.1,

$$V^{\pi(\delta)}\le V^{\mathrm{OPT}}\le V^{\mathrm R}\le V^{\pi(\delta)}+\bar r\,\frac{\delta}{m-\delta}+(\bar r+\bar\omega)\,\mathbb P[X_0(\delta)=0].$$

Stochastic dominance between the two systems (Lemma 4.4) gives $\mathbb P[X_0(\delta)=0]\le\mathbb P[\tilde X_0(\delta)\le0]$ (Corollary 4.5). The spoke laws are log-concave (Proposition B.9), log-concave generating functions are dominated by geometric ones (Lemma A.14), a concentration bound for sums of log-concave variables follows (Lemma A.12), and the relaxed depletion probability is at most $\exp(-\tfrac b2\delta^2/(m+n))$ (Proposition 4.6).

Significance

The result. A policy computed from $n$ independent problems of size $m+1$ loses only $O(\sqrt{\ln n/n})$ per period against the optimal policy of a problem with exponentially many states. No static policy achieves a vanishing gap. Theorem 4.1 also yields a practical certificate: $V^{\mathrm R}$ is a computable upper bound, and the gap is governed by one observable quantity, the hub-depletion probability. The same structure extends to several hubs (the paper's Theorem 6.1).

Formalizing it. The result is proved in the paper; nothing here is open, and no part of it has been machine-checked. A formal proof would check a chain that combines average-reward dynamic programming, convex duality and sensitivity analysis, a coupling argument between two Markov chains, and a concentration inequality for log-concave variables. Several of these steps are stated in the paper with brief or cited arguments (the Bellman equation of the spoke problem, the class structure of the chains, Keilson's factorial-moment inequality behind Lemma A.14).

Difficulty

The natural first idea is to use the Lagrangian policy at the optimal dual $\lambda^*$ of (9). At $\lambda^*>0$ the relaxation keeps zero resources in the hub in expectation, so the real hub is empty a constant fraction of the time and every hub request lost there costs a constant. The perturbation $\delta$ is what makes the argument work. The key step is then to compare the relaxed system, where spokes are independent and the hub may go negative, with the original system, where the hub constraint couples all spokes. This needs both a loss bound per depletion event (Lemma A.10, which rests on the monotonicity of Proposition 3.3) and a pathwise coupling (Lemma 4.4). A Chebyshev bound on the hub level gives only a polynomial rate. The exponential rate requires the log-concavity of every spoke law and a geometric domination of its generating function.

Formalization scope

• No measure theory. Policies are deterministic functions of the observed history (past request types and fulfilment outcomes) and the current request type. The finite-horizon expected revenue is a finite recursion, and $V^{\mathrm{OPT}}$ is the supremum over feasible policies of the limsup of its time average. Stationary distributions are finite probability vectors, via the published definition MarkovChain.IsStationary. Sums of independent ℕ-valued variables are iterated convolutions.
• Primitives. The revenue functions $r_{ij}$ are primitives satisfying Assumption 2.1. Request types are Fin n ⊕ Fin n, spoke levels Fin (m+1), the hub level is $m-\sum_ix_i$, and the original chain lives on $\mathcal X$.
• Definitions. $h_i^\lambda$ is defined as the value of (6); Proposition 3.2 is stated as "(6)'s value solves (5)". The Lagrangian policy is built from any optimal solutions of (6) at any optimal $\lambda^*(\delta)$, with the paper's controls ($1$ and $0$) above the support.
• Disclosed choices. Assumption 4.1 is assumed only at the $\delta$ in use. "Grow at the same rate" is $\kappa_1n\le m\le\kappa_2n$, with the constant $C$ and the threshold $N_0$ chosen before the network.
• Non-vacuity. The goal includes an attainment clause: $\lambda^*(\delta)$, optimal solutions of (6) and a stationary distribution exist. A proof cannot pass through empty hypotheses, and suprema and infima are taken over nonempty, bounded index sets.
• Not formalized. Proposition 2.1 (continuous-time utilisation), Proposition 2.2 (Bellman equation (2)), Lemma 4.8 (primitive sufficient conditions for Assumption 4.1), §5–§6 and the appendices on algorithms are not formalized.
• Reusable pieces. The log-concavity and convolution vocabulary and Lemmas A.12/A.14 are independent of the model and reusable. Contributions to the class structure of finite birth–death product chains, and to Keilson's moment inequality (Lemma A.13), are welcome.

Selected references

• S. R. Balseiro, D. B. Brown, C. Chen, Dynamic Pricing of Relocating Resources in Large Networks, SSRN working paper 3313737, version of May 23, 2020. https://ssrn.com/abstract=3313737 ; Management Science, https://doi.org/10.1287/mnsc.2020.3735
• J. Keilson, A threshold for log-concavity for probability generating functions and associated moment inequalities, Annals of Mathematical Statistics 43(5), 1702–1708, 1972.
• S. Janson, Tail bounds for sums of geometric and exponential variables, Statistics & Probability Letters 135, 2018. https://arxiv.org/abs/1709.08157
• S. Banerjee, D. Freund, T. Lykouris, Pricing and optimization in shared vehicle systems: an approximation framework, 2016. https://arxiv.org/abs/1608.06819
• A. Waserhole, V. Jost, Pricing in vehicle sharing systems: optimization in queuing networks with product forms, EURO Journal on Transportation and Logistics 5(3), 293–320, 2016.

Motivation

Retailers, online travel agencies and search engines display products in an ordered list or on a physical layout, and customers inspect only a prefix of it. Display optimization asks how to assign products to positions so as to maximize expected revenue when each customer considers only the products shown in the first $k$ positions, with $k$ random. Aouad and Segev (SSRN 2709652; Management Science 67(6), 2021) study this problem with vertically differentiated locations (every customer who sees position $k+1$ also sees positions $1,\dots,k$) and multinomial logit (MNL) choice within the consideration set. The model covers assortment planning over time and product framing on web pages, and it was calibrated on Expedia hotel-search data in the paper's case study.

The paper's headline claim (Theorem 1.1) is a polynomial-time approximation scheme, obtained by a dynamic program over approximate assortments followed by a rounding of its actions into an assignment. The rounding analysis, Section 5.2, contains a self-contained chain of combinatorial inequalities about the rounded assignment. That chain is the subject of this mission.

Setting

There are $n$ items. Item $i\in[n]$ has a price $r_i>0$ and an MNL preference weight $w_i>0$; write $\rho_i=r_iw_i$ and, for an assortment $S\subseteq[n]$,

$$\rho(S)=\sum_{i\in S}\rho_i,\qquad w(S)=\sum_{i\in S}w_i,\qquad R(S)=\frac{\rho(S)}{1+w(S)} ,$$

the expected revenue of offering $S$ to an MNL customer with a no-purchase option of weight $1$. An assignment $\mathcal A$ is a bijection from positions $[n]$ to items; $\mathcal A[k]$ is the set of items in positions $1,\dots,k$, $R_k(\mathcal A)=R(\mathcal A[k])$, and with position weights $\lambda_k>0$ the objective is

$$\mathcal R(\mathcal A)=\sum_{k=1}^n\lambda_kR_k(\mathcal A).$$

The algorithm fixes an accuracy $\epsilon\in(0,1/5)$ and a guessed position $k_{\mathrm{mid}}$. A sequence of dynamic-programming actions consists of events $e_1,\dots,e_T\in[n]$ and pairs $(S^-_j,S^+_j)$ of item sets (a sub-assortment and a super-assortment), starting from $e_1=1$, $S^-_1=S^+_1=\{i_1\}$ and ending at $e_T=n$, $S^-_T=S^+_T=[n]$. Consecutive actions must satisfy seven constraints, (8)–(14) of the paper: nestedness $S^-_{j-1}\subseteq S^+_{j-1}\subseteq S^+_j$, the accuracy bounds $\rho(S^+_{j-1}\setminus S^-_{j-1})\le4\epsilon^2\rho(S^-_{j-1})$ and the same for $w$, a cardinality constraint linking sets to events, and three growth conditions on the proxies

$$\alpha_j=\frac{\rho(S^-_j)}{1+w(S^+_j)}$$

depending on the position of $e_{j-1},e_j$ relative to $k_{\mathrm{mid}}$. With $j_{\mathrm{mid}}$ the last index whose event is at most $k_{\mathrm{mid}}$, the actions are rounded into blocks $\Delta_1,\dots,\Delta_T$ of new items (from $S^-_j$ before $j_{\mathrm{mid}}$, from $S^+_j$ after), and the rounded assignment $\tilde{\mathcal A}$ lists the blocks in order, each by non-increasing price. The block boundaries are $\tilde e_j=|\Delta_1\cup\dots\cup\Delta_j|$, and $\tilde I_j$ are the position intervals between consecutive boundaries, split at $k_{\mathrm{mid}}$.

Formalization targets

Goal: the rounded assignment dominates the DP proxies

For every $1\le k_{\mathrm{mid}}\le n-1$, every feasible action sequence and every rounded assignment $\tilde{\mathcal A}$,

$$\mathcal R(\tilde{\mathcal A})\ \ge\ (1-8\epsilon)\left(\sum_{j=1}^{j_{\mathrm{mid}}}\lambda(\tilde I_j)\min\{\alpha_j,\alpha_{j+1}\}+\sum_{j=j_{\mathrm{mid}}+1}^{T}\lambda(\tilde I_j)\min\{\alpha_{j-1},\alpha_j\}\right),$$

with $\lambda(J)=\sum_{k\in J}\lambda_k$. This is inequality (15) of the paper combined with (16), in the proof of Lemma 5.4.

Milestones

1. The MNL identity $R(S\cup\{i\})=R(S)\frac{1+w(S)}{1+w(S)+w_i}+r_i\frac{w_i}{1+w(S)+w_i}$ for $i\notin S$ (§3.1).
2. $\tilde{\mathcal A}[\tilde e_j]\subseteq S^+_j$ (proof of Lemma 5.3), and Lemma 5.3: $w(\tilde{\mathcal A}[\tilde e_j])\le w(S^+_j)$.
3. Lemma 5.2: $\rho(\tilde{\mathcal A}[\tilde e_j])\ge(1-8\epsilon)\rho(S^-_j)$.
4. Inequality (16): $\min\{R_{\tilde e_j}(\tilde{\mathcal A}),R_{\tilde e_{j+1}}(\tilde{\mathcal A})\}\ge(1-8\epsilon)\min\{\alpha_j,\alpha_{j+1}\}$.
5. Claim 5.5: $k\mapsto R_k(\tilde{\mathcal A})$ is unimodal on each $[\tilde e_j,\tilde e_{j+1}]$.

Significance

The goal is the step that converts the dynamic program's value into a revenue guarantee for an actual assignment: whatever action sequence the dynamic program returns, the assignment built from it earns at least $(1-8\epsilon)$ times the interval-weighted minima of the program's proxies. Any repaired analysis of the scheme has to pass through a statement of this form, since the rounding of §4.4 is the only link between the program's actions and a display.

The remaining half of the paper's argument is not true as printed. Lemma 5.4, $\mathcal R(\tilde{\mathcal A})\ge(1-15\epsilon)\mathcal R(\mathcal A^*)$, and with it the approximation clause of Theorem 1.1, fail for the paper's own algorithm: with $n=4$, $w=(32,1,32,4)$, $\rho=(4,16,64,8)$, $\lambda=(0.85,0.45,0.40,0.34)$ and $\epsilon=1/80$, no feasible action sequence can place item 2 first, and every rounded assignment earns at most $75364/16625\approx4.53$ against an optimum of $165804/16625\approx9.97$. A formal proof of the true half isolates precisely where the published argument stops working. No part of this chain has a machine-checked proof.

Difficulty

The rounding discards items. Before $j_{\mathrm{mid}}$, block $\Delta_j$ keeps only the part of the sub-assortment $S^-_j$ that is new with respect to $S^+_{j-1}$, so the prefix of $\tilde{\mathcal A}$ can carry less $\rho$-mass than $S^-_j$. A loss bounded by the per-step accuracy $4\epsilon^2$ would accumulate over up to $n$ steps; Lemma 5.2's constant $1-8\epsilon$ is independent of $T$, and holds only because the growth constraint forces $\rho(S^-_j)$ to grow geometrically, which the obvious step-by-step bound does not use. The second obstacle is that the revenue between two block boundaries is not monotone; bounding it by the boundary values requires the unimodality of Claim 5.5, which depends on the price order inside each block and on the MNL convex-combination structure, not on the dynamic program.

Formalization scope

Items are Fin n; positions and DP indices are 1-based natural numbers as on the page, and an assignment is an equivalence Fin n ≃ Fin n from the 0-based position $k-1$ to the item at position $k$. A DP sequence stores events and set pairs as functions on ℕ, read through accessors implementing the root convention $e_{T+1}=e_T$, $\vec S_{T+1}=\vec S_T$ and $S^+_0=\emptyset$. Feasibility is exactly the boundary and root conditions plus (8)–(14), with (11) written without natural-number truncation and (14) in the lower-bound form printed on p. 19. The rounded assignment is a predicate: block contents fixed by $\Delta_j$, non-increasing prices within a block, ties in any order.

Conventions and additions relative to the page:

• $1\le k_{\mathrm{mid}}\le n-1$ is assumed. For $k_{\mathrm{mid}}=n$ the construction of §4.4 can leave an item unplaced, so no rounded assignment exists and the statement would be vacuous.
• The approximate assortments range over all subsets of $[n]$ rather than the families of Lemma 2.5, events may repeat, and Assumptions 2.1–2.2 enter only as positivity of prices and weights. Each of these makes the statements stronger.
• Every statement quantifies over all feasible action sequences, not only the optimal one.
• Theorem 1.1, Lemma 5.4, Lemma 5.1 and inequalities (17)–(19) are not formalized, because they fail for the paper's algorithm (counterexample above).

Feasibility and rounding are the page's constructions; neither predicate builds in Lemma 5.2, Lemma 5.3 or any revenue property, so the goal cannot be obtained by unfolding a hypothesis. A sorry-free sanity check exhibits an instance ($n=3$, $k_{\mathrm{mid}}=2$) satisfying all hypotheses at once.

The development needs only finite sums over Finset, real arithmetic and induction over the block index. Contributions of all milestones are welcome; the identity and Claim 5.5 are reusable for any MNL ranking or display model.

Selected references

• A. Aouad and D. Segev, Display Optimization for Vertically Differentiated Locations Under Multinomial Logit Preferences, Management Science 67(6):3519–3550, 2021; authors' version of 31/07/2019, SSRN 2709652. https://ssrn.com/abstract=2709652 — DOI https://doi.org/10.1287/mnsc.2020.3664

Why self-adjoint extensions

In quantum mechanics an observable is a self-adjoint operator, not just a symmetric one. A differential expression such as $-d^2/dx^2$ on an interval or a half-line first defines a symmetric operator on smooth functions with compact support, and this operator usually has many self-adjoint extensions or none. Each extension is a different physical theory, with its own spectrum and dynamics, and choosing one amounts to choosing boundary conditions. Voronov, Gitman and Tyutin (arXiv:quant-ph/0603187) give a self-contained account of this problem written for physicists. Its abstract result is a description of all self-adjoint extensions that does not require computing the deficient subspaces.

Timeline. von Neumann (1929–30) classified the self-adjoint extensions of a closed symmetric operator through isometries between its deficient subspaces. The classical treatments are Akhiezer–Glazman and Naimark (Linear Differential Operators), and the Cayley-transform form is in Teschl's Mathematical Methods in Quantum Mechanics (2009), Theorem 2.26. Voronov, Gitman and Tyutin (2006) restate the finite-index case as a restriction of the adjoint by asymmetry-form conditions (their Theorem 3, (35)). They then remove the deficient subspaces from the description altogether (Theorem 15). For differential operators this gives self-adjoint boundary conditions in terms of boundary forms (Theorem 16).

Setting

Let $\mathcal H$ be a complex Hilbert space whose inner product $(\cdot,\cdot)$ is linear in the second argument. Let $\hat f$ be a linear operator with domain $D_f\subseteq\mathcal H$. It is symmetric if $D_f$ is dense and $(\eta,\hat f\xi)=(\hat f\eta,\xi)$ for all $\xi,\eta\in D_f$. It then has an adjoint $\hat f^{+}$ extending it and a closure $\bar f$ with domain $D_{\bar f}$, and $\hat f\subseteq\bar f\subseteq\hat f^+$. An operator $\hat g$ is self-adjoint if $\hat g^{+}=\hat g$, domains included.

The deficient subspaces are $D_+=\ker(\hat f^{+}-i)$ and $D_-=\ker(\hat f^{+}+i)$. The deficiency indices are $m_\pm=\dim D_\pm$.

The asymmetry form of the adjoint is the sesquilinear form on $D_{f^+}$

$$\omega_*(\eta_*,\xi_*)=(\eta_*,\hat f^{+}\xi_*)-(\hat f^{+}\eta_*,\xi_*).$$

It vanishes identically exactly when $\hat f^{+}$ is symmetric.

Vectors $w_1,\dots,w_m\in D_{f^+}$ are linearly independent modulo $D_{\bar f}$ if $\sum_kc_kw_k\in D_{\bar f}$ forces $c_1=\dots=c_m=0$. Given such vectors, $\hat f_U$ denotes the restriction of $\hat f^{+}$ to their joint $\omega_*$-annihilator:

$$\hat f_U:\quad D_{f_U}=\{\psi\in D_{f^+}:\ \omega_*(w_k,\psi)=0,\ k=1,\dots,m\},\qquad \hat f_U\psi=\hat f^{+}\psi .$$

Formalization targets

Goal: Theorem 15 (p. 68)

Assume $m_+=m_-=m$ with $0<m<\infty$. Then

$$\{\hat g:\ \hat f\subseteq\hat g=\hat g^{+}\}=\Big\{\hat f_U\ :\ w_1,\dots,w_m\in D_{f^+}\ \text{linearly independent mod } D_{\bar f},\ \ \omega_*(w_k,w_l)=0\ \forall k,l\Big\}.$$

Both inclusions are part of the goal: every self-adjoint extension arises from such a family, and every such family gives a self-adjoint extension.

Milestones, in attack order

• Sec. 2.2 (p. 8): $\aleph_z=(R_{f-zI})^\perp=(R_{\bar f-zI})^\perp=\ker(\hat f^+-\bar z)$.
• Theorem 1 (p. 8), the first von Neumann theorem: $D_{f^+}=D_{\bar f}\dotplus\ker(\hat f^+-z)\dotplus\ker(\hat f^+-\bar z)$ for $\operatorname{Im}z\ne0$, with the action of $\hat f^+$ on the components.
• (13) (p. 11): $D_{\bar f}=\{\psi\in D_{f^+}:\omega_*(\xi_*,\psi)=0\ \forall\xi_*\in D_{f^+}\}$.
• (18)–(19) (p. 12): $\omega_*(\eta_*,\xi_*)=(z-\bar z)[(\eta_z,\xi_z)-(\eta_{\bar z},\xi_{\bar z})]$.
• Theorem 3, existence (p. 19): self-adjoint extensions exist iff $m_+=m_-$. This one is already proved on the platform and is referenced.
• Theorem 3, (33)–(35) (p. 20): for $U\in U(m)$ and $e_{U,k}=e_{+,k}+\sum_lU_{lk}e_{-,l}$, the self-adjoint extensions are exactly the operators cut out by the $e_{U,k}$, and distinct $U$ give distinct extensions.
• (141) (p. 65) and (142)–(143) (p. 66): the $e_{U,k}$ are admissible, and admissibility and the cut-out operator are invariant under $w_k\mapsto\sum_aX_{ak}w_a+\underline\xi_k$ with $\det X\ne0$ and $\underline\xi_k\in D_{\bar f}$.
• Proof of Theorem 15, pp. 67–68: for admissible $w_k=\sum_aX_{ak}e_{+,a}+\sum_aY_{ak}e_{-,a}+\underline\xi_k$, both $X$ and $Y$ are nonsingular and $YX^{-1}$ is unitary.

Significance

The result. Theorem 15 lists all self-adjoint extensions of $\hat f$ as solutions of $m$ linear conditions on $D_{f^+}$. The vectors $w_k$ can be any vectors of the adjoint's domain satisfying two checkable conditions. For a differential operator, $\omega_*$ reduces to a boundary form $[w_k,\psi]\big|_a^b$, and Theorem 16 of the paper turns Theorem 15 into a recipe for self-adjoint boundary conditions that never solves $\hat f^{+}\psi=\pm i\psi$. In von Neumann's parametrization that equation must be solved, and doing so is often the hardest part of a concrete calculation. The price is redundancy: families related by a nonsingular matrix give the same extension.

Formalizing it. The mathematics is known: von Neumann's theory is classical and Theorem 15 is proved on pp. 65–68. The Prove2Me platform has Teschl's Cayley-transform version of the existence criterion as a machine-checked proof. To our knowledge, the first von Neumann formula for LinearPMap, the asymmetry-form description of the closure, and the unitary-matrix parametrization are not formalized in Mathlib or on the platform. This mission produces those statements, together with Theorem 15 itself.

Difficulty

The forward direction rests on the unitary parametrization of Theorem 3, which in turn rests on the direct-sum decomposition of $D_{f^+}$. Each of these steps requires working with $D_{\bar f}$ rather than $D_f$, because $\hat f$ need not be closed. The converse is the substantial part. Linear independence modulo $D_{\bar f}$ and isotropy $\omega_*(w_k,w_l)=0$ are conditions on the $w_k$ as whole vectors. They say nothing directly about the deficient components, and relating an arbitrary admissible family to the deficient-subspace description of Theorem 3 is where the work lies. A count of dimensions alone does not give self-adjointness. Showing that a restriction of $\hat f^+$ is symmetric is easy; showing that its adjoint is no larger than itself is not.

Formalization scope

• $\mathcal H$ is a complex Hilbert space (InnerProductSpace ℂ H, CompleteSpace H), and operators are LinearPMaps H →ₗ.[ℂ] H. The adjoint, closure, extension order and self-adjointness are Mathlib's f.adjoint, f.closure, f ≤ g and IsSelfAdjoint g (g† = g). Mathlib's inner product is conjugate-linear in the first slot, as in the paper.
• Symmetry is the published TeschlQM.Shared.IsSymmetric, which includes density. The initial operator is not assumed closed.
• Deficient subspaces are kernels of the adjoint at $z=i$: kerAdd f.adjoint (-I) $=\ker(f^+-i)$ and kerAdd f.adjoint I $=\ker(f^++i)$, from the published TeschlQM.SelfAdjoint.addScalar. The index hypotheses are Module.finrank … = m with 0 < m, which forces both indices to be finite. Theorem 1 and (18)–(19) keep a general $z$ with $\operatorname{Im}z\ne0$, as the paper does.
• $\omega_*$ (asymForm) is defined only on f.adjoint.domain. Families are indexed by Fin m. Linear independence is modulo f.closure.domain. The operator (144) is cutOut f w, which is f.adjoint restricted to the annihilator.
• The goal is not trivialized by its encoding. The extension in (144) is $\hat f^+$ restricted to an explicitly defined subspace, not an operator chosen to fit. The conclusion is genuine self-adjointness, $g^\dagger=g$, not symmetry on the cut-out domain. Without the hypothesis $m>0$, an index with infinite-dimensional deficient subspaces would satisfy finrank = 0, so that hypothesis is kept.
• A complete development needs the following: the first von Neumann formula for unbounded LinearPMaps; closures of symmetric operators; the identity $\operatorname{Ran}(f-z)^\perp=\ker(f^+-\bar z)$; and the unitary-matrix parametrization. These are reusable beyond this mission, for example for Sturm–Liouville realizations and Theorem 16 of the paper. Contributions of any of them are welcome, as are proofs routed through the published Cayley-transform results.

Selected references

• B. L. Voronov, D. M. Gitman, I. V. Tyutin, Self-adjoint differential operators assosiated with self-adjoint differential expressions, preprint, 2006. https://arxiv.org/abs/quant-ph/0603187 (v2 is the cited version)
• J. von Neumann, Allgemeine Eigenwerttheorie Hermitescher Funktionaloperatoren, Math. Ann. 102 (1930), 49–131. https://doi.org/10.1007/BF01782338
• N. I. Akhiezer, I. M. Glazman, Theory of Linear Operators in Hilbert Space, Dover, 1993 (reprint of the 1961/1963 translation).
• M. A. Naimark, Linear Differential Operators, Part II, Ungar, 1968.
• G. Teschl, Mathematical Methods in Quantum Mechanics, Graduate Studies in Mathematics 99, AMS, 2009, Theorem 2.26. https://doi.org/10.1090/gsm/099

Motivation

Repeated games model long-run relationships: the same players meet stage after stage, observe what was played, and can condition today's behavior on the past. The folk theorem describes what such relationships can sustain. When players are patient, every payoff vector that is feasible and gives each player at least what the others can force on them is the payoff of an equilibrium, and the equilibrium can be chosen subgame perfect, so that every threatened punishment is itself credible. Economics, operations research and computer science use the result to explain cooperation and collusion and to reason about long-term contracts and repeated auctions.

The classical statement assumes stationary discounting: a payoff at stage $t$ is worth $\delta^{t-1}$ of a payoff today, and "patient" means $\delta\to1$. Experimental and behavioral evidence points instead to discount rates that change over time (hyperbolic and quasi-hyperbolic discounting), and planning problems with a finite or decaying horizon have weights that are not geometric at all. X. Li (later with D. Kim) asks whether the perfect folk theorem survives when the weight of stage $t$ is an arbitrary decreasing sequence, and gives a patience condition under which it does.

Timeline.

• 1986. Fudenberg and Maskin prove the perfect folk theorem for discounted repeated games with at least three players under a full-dimensionality condition on the feasible and individually rational set (Econometrica 54).
• 1986. Sorin shows that any feasible payoff can be written as a discounted sum of pure-action payoffs once $\delta$ is large, which removes the need for public randomization on the equilibrium path (Math. Oper. Res. 11).
• 1991. Fudenberg and Maskin use such decompositions to dispense with public randomization in the perfect folk theorem.
• 2019–2021. Li (SSRN 3407197) and Kim and Li (Math. Oper. Res., 2021) extend the asymptotic perfect folk theorem to time-dependent discounting.

The repeated game with time-dependent discounting

A finite set $I$ of players plays a stage game repeatedly. Player $i$ has a finite action set $A^i$, $A=\prod_iA^i$, and $g=(g^i)_{i\in I}:A\to\mathbb R^I$ gives the stage payoffs. At each stage $t\ge1$ every player observes the past actions $(a_1,\dots,a_{t-1})$ and chooses an action, possibly at random. A behavior strategy $\sigma^i$ assigns a mixed action to every finite history, and a profile $\sigma$ determines a distribution over infinite plays.

An evaluation is a sequence $\theta=(\theta_t)_{t\ge1}$ in $[0,1]$ that is decreasing and sums to one; the payoff of $\sigma$ is

$$\gamma_\theta(\sigma)=\mathbb E_\sigma\Big[\sum_{t\ge1}\theta_t\,g(a_t)\Big].$$

Stationary discounting is $\theta_t=(1-\delta)\delta^{t-1}$. After a history of $T-1$ stages the remaining game is evaluated by the continuation evaluation $\theta_t[T]=\theta_{T-1+t}/\sum_{s\ge T}\theta_s$; unlike the stationary case, $\theta[T]$ depends on $T$. A profile is a subgame perfect equilibrium of $\Gamma_\theta$ if, after every history $h_T$, the induced profile is a Nash equilibrium of the subgame $\Gamma_{\theta[T]}(h_T)$. $E_\theta\subseteq\mathbb R^I$ is the set of subgame perfect equilibrium payoffs.

The minmax level of player $i$ is

$$v^i=\min_{s\in\prod_{j\ne i}\Delta(A^j)}\ \max_{a^i\in A^i}\ \sum_{a^{-i}}s(a^{-i})\,g^i(a^i,a^{-i}),$$

the lowest payoff the others can hold $i$ to by mixing independently. $S=\operatorname{co}\{g(a):a\in A\}$ is the set of feasible payoffs and $\mathcal F=\{x\in S:x^i\ge v^i\ \forall i\}$ the set of feasible and individually rational payoffs.

A sequence of evaluations $(\theta^k)_{k\ge1}$ is patient if $\theta^k_t/\theta^k_{t+1}\to1$ as $k\to\infty$, uniformly in $t$.

Formalization targets

Goal: Theorem 3.1 (Asymptotic Perfect Folk Theorem)

If $\operatorname{int}\mathcal F\ne\emptyset$ and $(\theta^k)$ is patient, then

$$E_{\theta^k}\xrightarrow[k\to\infty]{}\mathcal F\quad\text{in the Hausdorff distance.}$$

The goal fixes no rate and no constants; it asserts only the limit.

Milestones

• Lemma 4.1: patience is equivalent to $\sum_{t=T}^{T+T_1}\theta^k_t\big/\sum_{t=T}^{T+T_2}\theta^k_t\to(T_1+1)/(T_2+1)$ uniformly in $T$.
• Lemma 4.2: for patient $(\theta^k)$, $\theta^k_1[T]\to0$ and $\theta^k_t[T]/\theta^k_{t+1}[T]\to1$, uniformly in $T$ and $t$.
• Claim 7.1 and Lemma 4.4: a perturbed decomposition $x=\sum_m\theta^k_m x'_{\varphi(m)}$ with each $x'_{\varphi(m)}$ near a vertex.
• Proposition 4.3, and its form for the continuation evaluations $\theta^k[T]$: every $x\in\mathcal F$ is the $\theta^k$-payoff of a pure path along which all continuation payoffs stay within $\eta$ of $x$.
• (5.1), Lemma 5.1, Lemma 5.2: the punishment length and the bounds that make punishments and rewards consistent.
• The one-shot deviation principle under general discounting (§5.1 Part C, footnote 12).
• Interior payoffs are equilibrium payoffs: every $x\in\operatorname{int}\mathcal F$ lies in $E_{\theta^k}$ for all large $k$.

Significance

The result. The theorem says that the set of credible long-run outcomes is the same under any patient time-dependent discounting as under stationary discounting with $\delta\to1$. Quasi-hyperbolic $(\beta,\delta)$ preferences with $\beta,\delta\to1$ and discount factors that vary by stage are special cases. Patience is stated through ratios of consecutive weights. The paper notes that this condition does not cover $T$-stage averages with $T\to\infty$, where the folk theorem is known to need extra assumptions. The equilibria use pure paths, with no public randomization.

Formalizing it. The result is proved in the paper; no part of it has a machine-checked proof. The mission builds a reusable Lean model of discounted repeated games with perfect monitoring: behavior strategies, the induced distribution over finite histories, continuation games, subgame perfection, minmax levels and the feasible and individually rational set. It then states the theorem and the lemmas of its proof. The one-shot deviation principle under general discounting and the pure-path decomposition (Proposition 4.3) are standard tools that the literature usually cites without proof, and both are useful well beyond this paper.

Difficulty

The stationary proof relies on the fact that every subgame looks like the original game: $\theta[T]=\theta$. Under time-dependent discounting the continuation evaluation changes with the starting stage. A punishment phase of fixed length therefore carries a different weight depending on when it starts, and the number of stages needed to deter a deviation depends on the stage. Two consequences make the obvious adaptation fail. First, a deviation during a punishment starts a new punishment whose length differs from the remaining length of the old one, so the incentive check splits into cases (Lemma 5.2). Second, the pure paths that deliver the reward payoffs have to work for every continuation evaluation at once, which needs the uniformity statements of Lemma 4.2 and the perturbed decomposition of Lemma 4.4. Replacing each continuation evaluation by a geometric one does not work, because nothing forces the weights of a patient sequence to be close to geometric.

Formalization scope

All declarations live in the namespace TimeDepFolk.Asymptotic. Stages are 0-based: Lean stage $s$ is the paper's $t=s+1$, a history of $n$ played stages is Fin n → (∀ i, A i), and cont θ n is the paper's $\theta[n+1]$, which is $0$ when the tail sum vanishes. Mixed actions are lotteries (AGT.IsLottery) and the minmax level uses AGT.expectedPayoff from the published definition agt_games, with independent mixing by the others. Action sets are finite, so expectations are finite sums over histories and the payoff is the series $\sum_s\theta_s\,\mathbb E_\sigma[g(a_s)]$; no measure theory is needed. Payoff vectors live in I → ℝ with the sup norm. Subgame perfection quantifies over all histories, the empty history included, and over all behavior-strategy deviations; the one-shot reduction is a milestone to prove, not part of the definition. The player set and every action set are finite and nonempty. "$\operatorname{int}\mathcal F$ nonempty and fully dimensional" is (interior (F g)).Nonempty.

The goal uses the extended-valued Hausdorff distance Metric.hausdorffEDist. The real-valued Metric.hausdorffDist is $0$ when one set is empty, so a goal stated with it would hold vacuously for every $k$ at which no equilibrium is known; the extended version makes nonemptiness of $E_{\theta^k}$ part of the claim. Stating the goal for a single payoff, with Nash instead of subgame perfect equilibrium, or with Theorem 3.2's discount factors in place of evaluations would each prove a different and weaker theorem.

A complete development needs the probability of finite histories under behavior strategies, the decomposition of the payoff into the first stage and the continuation, the one-shot deviation principle, Carathéodory's theorem (in Mathlib), and the barycentric sensitivity of Claim 7.1. The repeated-game layer and the one-shot deviation principle can be reused for any discounted repeated game with perfect monitoring. Contributions to any milestone, and alternative proofs of the decomposition results, are welcome.

Selected references

• X. Li, The folk theorem for repeated games with time-dependent discounting, SSRN Working Paper 3407197, version of August 16, 2019. https://ssrn.com/abstract=3407197
• D. Kim and X. Li, The folk theorem for repeated games with time-dependent discounting, Mathematics of Operations Research, 2021. https://doi.org/10.1287/moor.2021.1183
• D. Fudenberg and E. Maskin, The folk theorem in repeated games with discounting or with incomplete information, Econometrica 54(3), 1986. https://doi.org/10.2307/1911307
• S. Sorin, On repeated games with complete information, Mathematics of Operations Research 11(1), 1986. https://doi.org/10.1287/moor.11.1.147
• G. J. Mailath and L. Samuelson, Repeated Games and Reputations: Long-Run Relationships, Oxford University Press, 2006. https://doi.org/10.1093/acprof:oso/9780195300796.001.0001

Motivation

Retailers that sell many products set prices against one another, and the demand for each product depends on the prices of all of them. Affine demand models, $q(p)=a-Rp$, are the standard starting point for this kind of multi-product price competition in operations management and industrial organization. Two questions follow once an equilibrium is known to exist. Can the firms reach it, and does it matter where they start? A Nash equilibrium that the firms cannot find by adjusting their prices tells little about what prices will actually be observed.

Federgruen and Hu (Operations Research 69(1), 2021; submitted manuscript at SSRN 3010503) answer this for a general multi-firm, multi-product model with an arbitrary number of firms and arbitrary product assortments. The game has features that defeat the usual tools. Once the affine demands are extended so that no demand turns negative, the game is in general not supermodular. Example 1 of the paper, after McGuire and Staelin (1983/2008), is a duopoly that is not supermodular and has a continuum of equilibria. Earlier work (Federgruen and Hu, Operations Research 63(3), 2015) characterized the equilibria. One of them, the special equilibrium $(p^*|w)$, has a closed form. The 2021 paper shows that this equilibrium is reached from any starting price vector when every firm repeatedly plays a robust best response.

Setting

A finite set $\mathcal N$ of products is partitioned among firms. Firm $i$ sells the products $\mathcal N(i)$. The foundational demands are

$$q(p)=a-Rp,\qquad a\ge 0,$$

where $R$ is an $\mathcal N\times\mathcal N$ price-sensitivity matrix subject to three assumptions:

1. (P) $R$ is positive definite in the quadratic-form sense: $x^\top Rx>0$ for all $x\ne 0$. $R$ need not be symmetric.
2. (Z) $R$ is a Z-matrix: $R_{lm}\le 0$ for $l\ne m$, so the products are substitutes.
3. (IS) $R$ is symmetric within each firm: $R_{lm}=R_{ml}$ when $l,m\in\mathcal N(i)$.

Each firm has a cost vector, $w\in\mathbb R^{\mathcal N}_{++}$. Let $T(R)$ be the block-diagonal matrix of the transposed firm blocks $R^\top_{\mathcal N(i),\mathcal N(i)}$, and let $\Psi(R)=T(R)[R+T(R)]^{-1}$ and $Q(w')=\Psi(R)a-\Psi(R)Rw'$. The cost projection $w'=\Theta(w)$ solves the linear complementarity problem

$$w'\le w,\qquad Q(w')^\top(w-w')=0,\qquad Q(w')\ge 0,$$

and the special equilibrium is

$$(p^*|w)=w'+[R+T(R)]^{-1}(a-Rw').$$

Given the other firms' prices $p_{-\mathcal N(i)}$, firm $i$ sees the residual intercept $\alpha=a_{\mathcal N(i)}-R_{\mathcal N(i),-\mathcal N(i)}p_{-\mathcal N(i)}$. Its robust best response maximizes

$$(x-w_{\mathcal N(i)})^\top(\alpha-R_{\mathcal N(i),\mathcal N(i)}x)\quad\text{over } x\ge 0,\ \alpha-R_{\mathcal N(i),\mathcal N(i)}x\ge 0.$$

Prices are restricted to keep the firm's own affine demands nonnegative, so the firm needs only its own demand and cost data. Collecting all firms gives the map $RB$, and $RB^{(n)}$ is its $n$-fold iterate. Finally, $\Lambda(R)=I-[T(R)]^{-1}R$.

Formalization targets

Goal: Theorem 3 (global robust stability)

There exist a norm $\|\cdot\|$ on $\mathbb R^{\mathcal N}$ and a constant $0<\gamma<1$ such that

$$\|RB(\hat p)-RB(\tilde p)\|\le\gamma\|\hat p-\tilde p\|\quad(\hat p,\tilde p\ge 0),$$ $$\|RB^{(n)}(p)-(p^*|w)\|\le\gamma^n\|p-(p^*|w)\|,\qquad \lim_{n\to\infty}RB^{(n)}(p)=(p^*|w)\quad(p\ge 0).$$

Neither the norm nor $\gamma$ is fixed, because the paper asserts only that they exist.

Milestones

The milestones follow the paper's own proof:

• Lemma 1: $RB$ is well defined.
• The proof of Theorem 2: the projection LCP has a unique, nonnegative solution.
• Theorem 2: $(p^*|w)$ is a fixed point of $RB$.
• Lemma B.1(a), (c), (e), (f), (g): the M-matrix lemmas.
• Lemma 2: the per-firm comparison of robust best responses.
• Three claims from the proof of Theorem 3(a):
  • the componentwise bound $|RB(\hat p)-RB(\tilde p)|\le\Lambda(R)|\hat p-\tilde p|$;
  • $\Lambda(R)\ge 0$ with spectral radius $\rho(\Lambda(R))<1$;
  • for every $\varepsilon>0$, an absolute norm whose induced norm satisfies $\|\Lambda(R)\|\le\rho(\Lambda(R))+\varepsilon$.

Significance

Theorem 3 makes the special equilibrium an operational prediction. Firms that adjust prices myopically, each using only its own demand and cost information, converge to $(p^*|w)$ from any start. The convergence is geometric, so the number of rounds needed to come within $\epsilon$ grows only logarithmically in the initial distance. This holds although the game is not supermodular and can have infinitely many equilibria, so the lattice-theoretic stability results that cover supermodular games do not apply. Theorem 2 also identifies which of the possibly many equilibria the dynamics select.

The result is proved in the paper, but it has not been formalized. A machine-checked version has two parts: a model layer (affine multi-product demand, the cost projection, robust best responses), and an M-matrix layer (Lemma B.1: inverse-positivity, Schur complements of inverse M-matrices, spectral radius bounds). Mathlib has neither. The proof also rests on results that the paper cites without proof: Propositions 2 and 3 of Federgruen and Hu (2015), and Theorem 4(b) and Lemma B.2(d) of Federgruen and Hu (2016). A formalization has to supply them. In one place the proof cites Horn and Johnson (1985, Lemma 5.6.10) for an absolute norm close to the spectral radius. As stated there, that lemma does not give absoluteness for general matrices: $\begin{pmatrix}1&1\\-1&-1\end{pmatrix}$ has spectral radius $0$, but every absolute norm gives it induced norm at least $1$. The claim holds for the nonnegative matrix $\Lambda(R)$, and the corresponding milestone is stated for that matrix only.

Difficulty

The obvious route is to show that $RB$ is a contraction in the sup norm and invoke Banach's fixed-point theorem. This fails: $\|\Lambda(R)\|_\infty$ can exceed $1$ even though $\rho(\Lambda(R))<1$, and the bound $|RB(\hat p)-RB(\tilde p)|\le\Lambda(R)|\hat p-\tilde p|$ is all the structure gives. The norm must be adapted to $\Lambda(R)$ and must also be absolute, so that the componentwise bound transfers. The per-firm estimate behind that bound (Lemma 2) is itself not a Lipschitz estimate for an explicit formula. The robust best response is the solution of a constrained quadratic program whose active set changes with the competitors' prices, and the comparison goes through a componentwise minimum $\check p=\min\{\hat p,\tilde p\}$ and monotonicity in the intercept. Separately, the fixed-point property needs the cost projection $\Theta(w)$, an LCP whose unique solvability and nonnegativity depend on (IS).

Formalization scope

Products form a finite type ι and firms a type F, with firm : ι → F assigning each product to its firm. Vectors are ι → ℝ with the pointwise order. Matrices are Matrix ι ι ℝ, and every matrix inequality is entrywise. The commitments are:

• (P) is ∀ x ≠ 0, 0 < x ⬝ᵥ R *ᵥ x, not Mathlib's Matrix.PosDef, which would add global symmetry.
• The special equilibrium $(p^*|w)$ is written through any solution $w'$ of the LCP (12)–(14). The paper says this form is valid for all $w>0$. A milestone proves that the solution exists, is unique, and is nonnegative.
• The robust best response is a relation, "$q$ is a robust best response to $p$", with the feasibility constraint of (8) built in. Lemma 1 makes it single-valued. Part (b) of the goal is stated for every robust best-response sequence started at $p^0\ge 0$.
• "A norm on $\mathbb R^{\mathcal N}$" is a seminorm that vanishes only at $0$.
• The spectral radius is that of the matrix viewed over $\mathbb C$, so complex eigenvalues count.
• Matrix inverses use Mathlib's ⁻¹. Every inverted matrix is invertible under the hypotheses.

No trivializing reading is available. The norm must be definite, the robust best response keeps its feasibility constraint and is never defined by a closed form, and the convergence statement holds for every iterate. A sorry-free sanity check confirms that the standing assumptions, the cost projection and the fixed-point relation are all satisfiable on a two-firm example.

The following results are not formalized here:

• Theorem 1 and Proposition 1, which characterize the set of Nash equilibria and the existence of $(p^*|w)$ under the full LCP-extended demand. They are independent of the goal.
• Example 1, Lemma B.2, Lemma C.1 and Proposition 2 of Appendix D.

Contributions that would be reusable beyond this mission include:

• a general M-matrix library (inverse-positivity, Schur complements, Perron–Frobenius bounds);
• uniqueness for P-matrix LCPs;
• the existence of absolute norms close to the spectral radius for nonnegative matrices.

Selected references

• A. Federgruen, M. Hu, Technical Note—Global Robust Stability in a General Price and Assortment Competition Model, Operations Research 69(1) 164–174, 2021. https://doi.org/10.1287/opre.2020.2001 (submitted manuscript: https://ssrn.com/abstract=3010503)
• A. Federgruen, M. Hu, Multi-Product Price and Assortment Competition, Operations Research 63(3) 572–584, 2015.
• A. Federgruen, M. Hu, Sequential Multiproduct Price Competition in Supply Chain Networks, Operations Research 64(1) 135–149, 2016.
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985; Topics in Matrix Analysis, Cambridge University Press, 1991.
• I. N. Imam, The Schur complement and the inverse M-matrix problem, Linear Algebra and its Applications 62 235–240, 1984.
• T. W. McGuire, R. Staelin, An industry equilibrium analysis of downstream vertical integration, Marketing Science 27(1) 115–130, 2008 (reprint of Marketing Science 2(2), 1983).

Motivation

Congestion pricing charges road users for the delay they impose on others. The classical theory, going back to Beckmann, McGuire and Winsten (1956), assumes a single benevolent authority that sets every toll: charging each link its marginal toll makes the selfish (Wardrop) traffic pattern socially optimal. Many real networks are different. Roads, bridges and tunnels built under build-operate-transfer schemes are run by private operators who set their own prices to maximize their own revenue. When operators compete, an equilibrium of the pricing game need not exist, need not be unique, and can be far from optimal (Acemoglu and Ozdaglar 2007; Hayrapetyan, Tardos and Wexler 2007).

Correa, Guzmán, Lianeas, Nikolova and Schröder (2021) ask whether a regulator who can only impose price caps — an upper bound $\bar t_e$ on the toll of each link — can steer competing operators to the optimal flow. Their main result, Theorem 1, answers yes: optimal tolls bounded by the marginal tolls, used as caps, are the unique equilibrium of the capped game, even against coalitions of operators. This mission formalizes that theorem and the two monotonicity lemmas it rests on.

Setting

A network has links $e \in E$ and commodities $k \in K$; each commodity has a finite set $\mathcal P^k$ of routes, each route being a set of links. Commodity $k$ has a maximum demand $r_k \ge 0$ and a nonincreasing, continuous, nonnegative utility function $u_k$ on $[0, r_k]$; its aggregate utility is $U_k(y) = \int_0^y u_k(s)\,ds$. Each link has a latency function $\ell_e$ on $[0,\infty)$, nonnegative, nondecreasing, convex and smooth.

A flow assigns $x_P \ge 0$ to each route so that $r^k_x = \sum_{P \in \mathcal P^k} x_P \le r_k$; $X$ is the set of flows and $x_e = \sum_{P \ni e} x_P$ is the flow on link $e$. Under a toll vector $t \ge 0$, users settle in a Wardrop equilibrium, which is a maximizer over $X$ of the potential

$$\Phi_t(x) = \sum_{k \in K} U_k(r^k_x) - \sum_{e \in E} \int_0^{x_e} \big(\ell_e(y) + t_e\big)\,dy. \qquad (1)$$

The paper restricts to instances where this maximizer is unique (linkwise) for every $t \ge 0$, and writes $x(t)$ for it.

The social welfare of a flow is $SW(x) = \sum_k U_k(r^k_x) - \sum_e \ell_e(x_e)\,x_e$; an optimal flow $x^*$ maximizes it over $X$. The marginal tolls are $\hat t_e = x^*_e\,\ell'_e(x^*_e)$, and a toll vector $\bar t$ is optimal if $x(\bar t)$ is the optimal flow.

Each link is run by a separate operator, whose profit is $\pi_e(t) = t_e\,x_e(t)$. Given caps $\bar t \ge 0$, operator $e$ chooses $s_e \in [0, \bar t_e]$. A profile $t$ is a Nash equilibrium of the capped game if no operator gains by a unilateral change within its cap, and a strong Nash equilibrium if no nonempty coalition $E^\Delta$ has a joint change, within the caps and confined to $E^\Delta$, that strictly raises the profit of every member. By Definition 1, $\bar t$ is a (strong) cap equilibrium if $\bar t$ itself is the unique (strong) Nash equilibrium of the game with caps $\bar t$.

Formalization targets

Goal: Theorem 1

If $\bar t$ is an optimal toll vector with

$$\bar t_e \le \hat t_e = x^*_e\,\ell'_e(x^*_e) \quad \text{for all } e \in E,$$

then $\bar t$ is both a cap equilibrium and a strong cap equilibrium.

Milestones

1. Continuity (§2.1.2, p. 5). Each link flow $t \mapsto x_e(t)$ is continuous on $\{t \ge 0\}$.
2. Lemma 1 (p. 6). If $0 \le t \le t'$ and $E^< = \{e : t_e < t'_e\} \neq \emptyset$, there are $e_1, e_2 \in E^<$ with $x_{e_1}(t') \le x_{e_1}(t)$ and $[x_{e_2}(t') - x_{e_2}(t)][\ell_{e_2}(x_{e_2}(t')) + t'_{e_2} - \ell_{e_2}(x_{e_2}(t)) - t_{e_2}] \le 0$.
3. Lemma 2 (p. 7). If $t_e$ locally maximizes $\pi_e(\cdot, t_{-e})$, then $x_e(t)\,\ell'_e(x_e(t)) \le t_e$.
4. Remark 1 / first half of the proof (p. 7). Under the hypotheses of Theorem 1, no coalition has a capped deviation from $\bar t$ with $\pi_e(t') \ge \pi_e(\bar t)$ on the coalition and at least one strict inequality.
5. Second half of the proof (p. 8). Under the same hypotheses, every Nash equilibrium of the game with caps $\bar t$ equals $\bar t$.

Significance

Theorem 1 resolves, for capped games, the problems of existence, uniqueness and inefficiency that the literature on competing link operators identified: the regulator needs only to know the optimal flow and its marginal tolls, and then no operator, and no coalition of operators, has a reason to move away from the optimal tolls. The paper's consumer-surplus comparison (Theorem 2) is a comparison among such great tolls, and its extensions with operating costs, multi-link operators and complementary links (Theorems 3–6) follow the same pattern. The two lemmas are general facts about Wardrop flows under elastic demand — monotonicity in the tolls and a first-order bound at a profit maximum — that are reusable for any toll-setting or pricing question in nonatomic routing.

The result is proved in the paper; none of it is formalized. The mission produces a machine-checked version of the full argument, including the steps the paper states without proof.

Difficulty

The equilibrium flow $x(t)$ is defined only implicitly, as the maximizer of a concave potential that depends on the tolls, so every statement about operators' profits is a statement about a parametric optimization problem. Lemma 1 needs first-order optimality conditions of (1) on a polytope of route flows with elastic demand, and continuity needs a maximum-theorem argument in which only the link flows, not the route flows, are unique. Lemma 2 cannot simply differentiate $\pi_e$: $x_e(t)$ need not be differentiable in $t_e$, so the argument must work with one-sided difference quotients. The coalition part of Theorem 1 cannot be reduced to unilateral deviations; a deviation by many operators at once moves the flow on every link of the network simultaneously.

Formalization scope

All declarations live in the namespace NetworkPricing.Caps. Links, routes and commodities are Fin J, Fin R, Fin Sd; link flows are KellyStochasticNetworks.linkFlow of the published definition KellyStochasticNetworks_Wardrop. The model commits to the following conventions:

• Routes form an abstract finite route system with 0/1 incidence and a commodity per route; the $o_k$–$d_k$ paths of a graph are an instance, and the proofs never use the graph.
• $u_k$ and $\ell_e$ are functions $\mathbb R \to \mathbb R$ constrained only on $[0, r_k]$ and $[0, \infty)$. "Smooth" is read as differentiable on $\mathbb R$, and $\ell'_e$ is the derivative.
• The Wardrop flow is a hypothesis, not a definition: every theorem takes a selection flow with flow t a maximizer of (1) for each $t \ge 0$, together with the paper's uniqueness assumption on link flows.
• An optimal toll is $\bar t \ge 0$ whose Wardrop flow has the link flows of an optimal flow $x^*$; $\hat t$ is computed from $x^*$.
• In the capped game, unilateral and coalition deviations stay in $[0, \bar t]$, and coalitions are nonempty (with the empty coalition the page's formula would rule out every profile). Local optimality in Lemma 2 is relative to tolls $s_e \ge 0$.
• "(strong) cap equilibrium" in Theorem 1 is the conjunction of both notions.

Formalizations that make the goal trivial are ruled out: $x(t)$ must maximize the potential (1), not be an arbitrary function of $t$; uniqueness of the equilibrium is part of the conclusion, not just that $\bar t$ is an equilibrium; and the strong notion quantifies over all coalition deviations, not single-player ones.

A complete development needs first-order optimality conditions for concave maximization over polytopes, a version of Berge's maximum theorem, and convexity facts about differentiable functions. All of these are reusable well beyond this mission. Contributions are welcome on each milestone independently, and on general lemmas about parametric Wardrop flows.

Selected references

• J. Correa, C. Guzmán, T. Lianeas, E. Nikolova, M. Schröder, Network Pricing: How to Induce Optimal Flows Under Strategic Link Operators, Operations Research, Articles in Advance, 2021. https://doi.org/10.1287/opre.2020.2067
• M. Beckmann, C. B. McGuire, C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, New Haven, 1956 (book; no DOI).
• D. Acemoglu, A. Ozdaglar, Competition and Efficiency in Congested Markets, Mathematics of Operations Research 32(1), 2007. https://doi.org/10.1287/moor.1060.0231
• A. Hayrapetyan, É. Tardos, T. Wexler, A Network Pricing Game for Selfish Traffic, Distributed Computing 19(4), 2007. https://doi.org/10.1007/s00446-006-0012-4
• C. Berge, Topological Spaces: Including a Treatment of Multi-valued Functions, Vector Spaces, and Convexity, Oliver and Boyd, 1963; Dover reprint (book; no DOI).

Motivation

In a multiplayer multi-armed bandit, several agents repeatedly choose among the same finite set of arms, and two agents that choose the same arm collide and receive nothing. The model comes from cognitive radio and wireless networks: users share channels, a channel used by two users at once carries neither transmission, and the quality of a channel differs from user to user. Each user must learn the channel qualities from her own rewards while avoiding the others, and in a large network the users can neither exchange messages nor observe each other's choices.

When all players share the same arm means, the problem reduces to finding the $N$ best arms and spreading the players over them; algorithms such as Musical Chairs (Rosenski, Shamir and Szlak, 2016) do this. When each player has her own means $\mu_{n,i}$, the target is an optimal solution of an assignment problem, which couples the players. Bistritz and Leshem (arXiv:1810.11162, NeurIPS 2018; a journal version appeared in Mathematics of Operations Research) gave the first algorithm for this heterogeneous case that uses no communication at all and has near-logarithmic expected regret. This mission formalizes the main theorem of the preprint arXiv:1810.11162v7.

Setting

There are $N$ players and $M\ge N$ arms. At every turn $t=1,\dots,T$ each player $n$ picks an arm $a_n(t)$. The non-collision indicator $\eta_i(a)$ is $0$ if more than one player chose arm $i$ in the profile $a$ and $1$ otherwise. Player $n$ receives $r_{n,a_n(t)}(t)\,\eta_{a_n(t)}(a(t))$: the reward of her arm, or $0$ after a collision.

The rewards satisfy Definition II.1: for each $(n,i)$ the sequence $r_{n,i}(t)$ is i.i.d. with a continuous law, mean $\mu_{n,i}>0$, variance $\sigma^2_{n,i}$ and Bernstein's moment condition with parameter $b_{n,i}$, and the sequences are independent. Because the law is continuous, a zero reward reveals a collision almost surely; this is the only feedback a player gets. The horizon $T$ is unknown to the players.

Write $g_n(a)=\mu_{n,a_n}\eta_{a_n}(a)$. The benchmark is an optimal assignment $a^*\in\arg\max_a\sum_ng_n(a)$, assumed unique, and the total regret is

$$R=\sum_{t=1}^T\sum_{n=1}^Nr_{n,a^*_n}(t)\,\eta_{a^*_n}(a^*)-\sum_{t=1}^T\sum_{n=1}^Nr_{n,a_n(t)}(t)\,\eta_{a_n(t)}(a(t)),\qquad \bar R=\mathbb E\{R\}.$$

The Game of Thrones (GoT) algorithm (Algorithm 1) runs in epochs $k=1,2,\dots$, each with three phases: an exploration phase of $\lceil c_1k^\delta\rceil$ turns, where players sample arms uniformly and average their collision-free rewards into estimates $\mu^k_{n,i}$; a GoT phase of $\lceil c_2k^\delta\rceil$ turns, where players run a perturbed content/discontent dynamic with perturbation $\varepsilon$ and exponent $c$ on the game $u_n(a)=\mu^k_{n,a_n}\eta_{a_n}(a)$; and an exploitation phase of $c_32^k$ turns, where each player plays the arm with which she was most often content during the last $\lfloor k/2\rfloor+1$ GoT phases. The GoT dynamics form a Markov chain $P^\varepsilon$ on the states $Z=\prod_n(\mathcal A_n\times\{C,D\})$ (baseline arm and mood of every player), with optimal state $z^*=[a^*,C^N]$.

Formalization targets

Goal: Theorem III.1

With $J_1=\max_a\sum_ng_n(a)$, $J_0=\sum_n\max_ag_n(a)$, integers $c_1,c_2,c_3>0$, $\delta>0$ and $c>J_0-J_1$, there is $\varepsilon\in(0,1)$ such that for all large enough $T$

$$\bar R\le4\Big(\max_{n,i}\mu_{n,i}\Big)(c_1+c_2)\,N\log_2^{1+\delta}\Big(\frac T{c_3}+2\Big).$$

Milestones

1. Lemma IV.2. If $|\hat\mu_{n,i}-\mu_{n,i}|<\Delta\le(J_1-J_2)/(2N)$, every optimal assignment for $\hat\mu$ is optimal for $\mu$ ($J_2$ the second best objective).
2. Lemma IV.3, Eq. (20). $\mathbb P(\max_{n,i}|\mu^k_{n,i}-\mu_{n,i}|>\Delta_{\min}/4)\le2NMe^{-wc_1(k/2)^\delta k}+NMe^{-c_1(k/2)^\delta k/(36M^2)}$.
3. Lemma IV.3, Eq. (21). The same for the union over the last $\lfloor k/2\rfloor+1$ epochs.
4. Lemma V.3. The estimated assignment problem has a unique optimum almost surely.
5. Theorem V.6. If $c>\sum_nu_{n,\max}-J_1$, then $\pi_{z^*}>\frac1{2(1-\eta)}$ for every small enough $\varepsilon$.
6. Lemma V.7, Eq. (31). Markov-chain concentration of the visits to $z^*$ in one GoT phase.
7. Lemma V.8, Eq. (33). The GoT phases of the last $\lfloor k/2\rfloor+1$ epochs fail with probability at most $(C_0e^{-\Theta((k/2)^\delta)})^k$.

Significance

The theorem shows that full decentralization costs at most a factor $\log^\delta T$ in regret: the $\Omega(\log T)$ lower bound of Proposition II.3 holds already with full information, and GoT reaches $O(\log^{1+\delta}T)$ with no messages, no knowledge of $T$, and no observation of the other players. It is a learning-in-games result as much as a bandit result: the players reach the welfare-maximizing assignment of a game that is not interdependent, which the content/discontent dynamics of Marden, Young and Pao (2014) require, and the requirement on the exponent is $c>\sum_nu_{n,\max}-J_1$ instead of $c>N$.

The result is proved on paper and has no machine-checked proof; nothing in this mission is formalized yet. A formal proof would also settle points the paper leaves implicit, recorded in the formalization notes: one $\varepsilon$ must serve every epoch although the stationary threshold of Theorem V.6 depends on the epoch's estimated utilities, and the GoT chain has transient states, so the tree formula of Lemma V.5 and the norm $\|\phi_k\|_\pi$ must be applied to its closed class.

Difficulty

Each phase is analysed separately, and the work lies in the parts that are not standard. The exploration bound needs a concentration inequality for averages over a random number of collision-free samples. The GoT phase needs a lower bound on a stationary probability of a perturbed chain on $(2M)^N$ states, obtained by comparing the resistances of trees in the sense of Freidlin and Wentzell (Appendix A, pp. 15–18). It then needs a Chernoff bound for Markov chains (Chung, Lam, Liu and Mitzenmacher, 2012) in terms of the mixing time. Finally, the epochs interact: the estimates of epoch $k$ determine the chain of epoch $k$, the GoT phase starts from the end of an earlier GoT phase, and the exploitation phase votes over $\lfloor k/2\rfloor+1$ dependent phases.

The natural first idea, to treat each epoch's GoT run as a fixed ergodic chain and apply a stationary-mass bound, fails twice. The chain is random through the estimates, so the threshold on $\varepsilon$ must hold uniformly over a neighbourhood of the true means. The chain is also not irreducible: a state where a colliding player is content can never be entered.

Formalization scope

Players, arms and turns are 0-based (Fin N, Fin M, t : ℕ), and epochs are 1-based. The collision indicator is noColl, because $\eta$ also names the slack in Theorem V.6 and Lemmas V.7–V.8. The rewards live on a probability space as r n i t. The players' randomization is a family of private uniform seeds, jointly independent of the rewards, and every random choice of Algorithm 1 is realized from a seed with exactly the prescribed law. Each player's action and update read only her own memory, her own seeds and her own received reward; the means, $a^*$, $T$ and the other players' actions never enter a rule. Collisions are read off a zero reward, as in Algorithm 1. The regret is Eq. (3) with the realized comparison rewards. The GoT chain is an explicit matrix on Fin N → Fin M × Mood. Stationarity and the mixing time $T_m(1/8)$ (worst start, total variation) come from the published MarkovMixing definitions.

Conventions and disclosed additions:

• $c>J_0-J_1$ in the goal, because Theorem III.1 omits $c$;
• $\varepsilon<1$ for the goal's witness;
• $\Delta_{\min}>0$ in Lemma IV.3, Eq. (21);
• visited arms and positive estimates in Lemma V.3;
• positive utilities and $M\ge2$ in Theorem V.6 and Lemmas V.7–V.8;
• initial laws vanishing where $\pi$ vanishes in Lemmas V.7–V.8;
• Algorithm 1's GoT starting rule, rather than Lemma V.7's;
• ties in Eq. (15) broken toward the smallest index;
• the junk value $\mu^k=0$ for an unvisited arm.

A formalization in which a player's rule sees the instance would make the goal trivial (play $a^*$ from the start), and a policy class in place of Algorithm 1 would change the theorem. Neither is used. Irreducibility of the GoT chain is false, and no statement assumes it.

Needed infrastructure that Mathlib lacks: Bernstein's inequality for sums over random index sets, the Markov-chain tree theorem (already posed on the platform as YoungConventions.Perturbed.markov_chain_tree_formula), and a Chernoff bound for finite Markov chains. The last two are reusable well beyond this mission, and contributions of them as separate theorems are welcome.

Selected references

• I. Bistritz and A. Leshem, Game of Thrones: Fully Distributed Learning for Multiplayer Bandits, arXiv:1810.11162v7, 2021. https://arxiv.org/abs/1810.11162
• J. R. Marden, H. P. Young and L. Y. Pao, Achieving Pareto optimality through distributed learning, SIAM J. Control Optim. 52(5), 2014. https://doi.org/10.1137/12089705X
• K.-M. Chung, H. Lam, Z. Liu and M. Mitzenmacher, Chernoff–Hoeffding bounds for Markov chains: generalized and simplified, STACS 2012. https://arxiv.org/abs/1201.0559
• J. Rosenski, O. Shamir and L. Szlak, Multi-player bandits — a musical chairs approach, ICML 2016. https://arxiv.org/abs/1512.02866
• M. I. Freidlin and A. D. Wentzell, Random Perturbations of Dynamical Systems, Springer, 1984. https://doi.org/10.1007/978-1-4684-0176-9