All missions

Motivation

We generalize an efficient exact synthesis algorithm for single-qubit unitaries over the Clifford+T gate set which was presented by Kliuchnikov, Maslov and Mosca. Their algorithm takes as input an exactly synthesizable single-qubit unitary--one which can be expressed without error as a product of Clifford and T gates--and outputs a sequence of gates which implements it. The algorithm is optimal in the sense that the length of the sequence, measured by the number of T gates, is smallest possible. In this paper, for each positive even integer $n$ we consider the "Clifford-cyclotomic" gate set consisting of the Clifford group plus a z-rotation by $\fracπ{n}$. We present an efficient exact synthesis algorithm which outputs a decomposition using the minimum number of $\fracπ{n}$ z-rotations. For the Clifford+T case $n=4$ the group of exactly synthesizable unitaries was shown to be equal to the group of unitaries with entries over the ring $\mathbb{Z}[e^{i\fracπ{n}},1/2]$. We prove that this characterization holds for a handful of other small values of $n$ but the fraction of positive even integers for which it fails to hold is 100%.

This mission is the statement-level formalization of Exact synthesis of single-qubit unitaries over Clifford-cyclotomic gate sets (arXiv:1501.04944v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Existence of an alternating-axis canonical decomposition (Lemma 3.1, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

2 results of the paper are not stated yet, because the library lacks an interface they need:

• Main result (A): Canonical reduced dyadic integral-basis input codec and executable fixed-n Bloch-cancellation machine with charged bit operations, termination and actual output extraction (hard)
• Algorithm to compute the canonical form: Canonical reduced dyadic integral-basis input codec and executable fixed-n Bloch-cancellation machine with charged bit operations, termination and actual output extraction (hard)

Selected references

• Exact synthesis of single-qubit unitaries over Clifford-cyclotomic gate sets, arXiv:1501.04944v2, https://arxiv.org/abs/1501.04944v2

Motivation

We prove the security of the Bennett-Brassard (BB84) quantum key distribution protocol for an arbitrary source whose averaged states are basis-independent, a condition that is automatically satisfied if the source is suitably designed. The proof is based on the observation that, to an adversary, the key extraction process is equivalent to a measurement in the sigma_x-basis performed on a pure sigma_z-basis eigenstate. The dependence of the achievable key length on the bit error rate is the same as that established by Shor and Preskill for a perfect source, indicating that the defects in the source are efficiently detected by the protocol.

This mission is the statement-level formalization of Secure quantum key distribution with an uncharacterized source (arXiv:quant-ph/0208155v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Local auxiliary measurement constructs a basis-independent source (Source-design paragraph preceding Protocol 1, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

5 results of the paper are not stated yet, because the library lacks an interface they need:

• Protocol 1 main security result: Constructed nine-step accepted-protocol instrument, transcript, random-position code family and net-key rate semantics (hard)
• Protocols 1–3, I1=I2<=I3: Actual Protocol 1/2/3 joint key/transcript/Eve experiments and causal preparation-game supremum (hard)
• Sampling paragraph before Eq.(3): A valid domain/asymptotic regime for the printed exponent epsilon^2/[4(delta-delta^2)] (source-ambiguity)
• Null-outcome extension after Eq.(13): Basis-independent null/valid filter composed with the constructed accepted QKD experiment (hard)
• Role reversal and rate paragraph: Role-exchanged operational QKD instrument with trusted source-half qubit measurement and no detector-to-Eve communication (hard)

Selected references

• Secure quantum key distribution with an uncharacterized source, arXiv:quant-ph/0208155v2, https://arxiv.org/abs/quant-ph/0208155v2

Motivation

A matching in a graph is a set of edges no two of which share a vertex. Maximum-cardinality matching is one of the basic problems of combinatorial optimization, and the fastest known algorithm for it in general graphs is the Micali–Vazirani (MV) algorithm (Micali–Vazirani, FOCS 1980), which runs in $O(m\sqrt n)$ time. It follows the phase structure of Hopcroft and Karp (SIAM J. Comput. 1973) and Karzanov: in each phase, find a maximal set of disjoint shortest augmenting paths. In bipartite graphs one phase is a breadth-first search. In general graphs it is not, and the MV algorithm went without a complete, accepted correctness proof for decades. Vazirani's paper (Math. Oper. Res. 49(3) 2024) supplies it, by building a structure theory of shortest alternating paths whose central result is its Theorem 3.

Timeline:

• 1965: Edmonds' blossom algorithm, the first polynomial algorithm for matching in general graphs. Its blossoms ignore path lengths.
• 1973: Hopcroft–Karp and Karzanov: $O(\sqrt n)$ phases of shortest augmenting paths suffice.
• 1980: Micali and Vazirani publish the $O(m\sqrt n)$ algorithm, without a full proof.
• 1994: a first proof attempt (Vazirani, Combinatorica 14(1):71–109), which the 2024 paper describes as having "serious shortcomings" (p.2009).
• 2024: the present paper gives the theory and the proof.

Setting

Fix a finite simple graph $G=(V,E)$ and a matching $M$. A vertex is unmatched if no edge of $M$ contains it. An alternating path is a simple path whose edges alternate between $M$ and $E\setminus M$; an augmenting path is one that starts and ends at unmatched vertices, and $l_m$ is the length of a shortest one ($\infty$ if none).

The even level $\mathrm{even\ level}(v)$ (odd level $\mathrm{odd\ level}(v)$) is the length of a shortest alternating path of even (odd) length from an unmatched vertex to $v$, or $\infty$. Such a path is an even level($v$) path (odd level($v$) path). The min level and max level are the smaller and larger of the two. The tenacity of $v$ is $\mathrm{tenacity}(v)=\mathrm{even\ level}(v)+\mathrm{odd\ level}(v)$, and $t_m$ is the minimum tenacity of a vertex. The tenacity of an unmatched edge $(u,v)$ is $\mathrm{even\ level}(u)+\mathrm{even\ level}(v)+1$, and of a matched edge $\mathrm{odd\ level}(u)+\mathrm{odd\ level}(v)+1$.

If $(u,v)$ is the last edge of a min level($v$) path, $u$ is a predecessor of $v$ and $(u,v)$ is a prop; every other edge is a bridge. An odd $t$ with $t_m\le t<l_m$ is an eligible tenacity.

For a shortest alternating path $p$ to $v$, the base of $v$ with respect to $p$, $F(p,v)$, is the vertex of $p$ farthest from the start among those of tenacity greater than $\mathrm{tenacity}(v)$; $B(v)$ is the set of all $F(p,v)$. When $B(v)=\{b\}$, $b=\mathrm{base}(v)$. An even level($b;v$) path is a shortest even alternating path from $b$ to $v$ starting with an unmatched edge (odd likewise). The blossom $B_{b,t}$ of tenacity $t$ and base $b$ consists of the vertices of tenacity $t$ with base $b$ together with the blossoms $B_{w,t-2}$ for $w$ among those vertices and $b$.

Formalization targets

Goal: Theorem 3

For every eligible tenacity $t$ and every $v$ with $\mathrm{tenacity}(v)=t$:

$$\begin{aligned} &\text{(1) every max level}(v)\text{ path contains a bridge of tenacity } t;\\ &\text{(2) } B(v) \text{ is a singleton};\\ &\text{(3) every even (odd) level}(v)\text{ path} = \text{even level}(b)\text{ path} \cdot \text{even (odd) level}(b;v)\text{ path} \subseteq B_{b,t}\cup\{b\};\\ &\text{(4) blossoms of tenacity } t \text{ are disjoint; blossoms of tenacity} \le t \text{ form a laminar family};\\ &\text{(5) on an even level}(u)\text{ path through } w,\ \mathrm{tenacity}(w)=t:\ \mathrm{base}(w)\in p \text{ and } p[\mathrm{base}(w)\text{ to }w] \text{ is shortest.} \end{aligned}$$

No constant is fixed: the statement holds for every finite graph, every matching and every eligible $t$.

Milestones

The induction basis $t=t_m$ (Lemmas 4–6, 11, 13, 14 and Corollaries 2–4, including the uniqueness of the bridge in Lemma 5), the edge lemmas of §6 (Lemmas 1 and 3), the limited BFS honesty of Theorem 2, and the induction-step facts Lemmas 17, 19 and 20.

Significance

Statement 1 is what makes the MV algorithm correct: processing bridges in order of tenacity, and running double depth-first search from each bridge, reaches every shortest alternating path. Statements 2–5 make the base and the nested blossoms well defined and describe how shortest paths traverse them; the algorithm's path-finding procedure relies on them. Without Theorem 3 the $O(m\sqrt n)$ bound for general-graph matching rests on an unproved algorithm.

The theorem is proved in the paper; no machine-checked proof of it exists. A formal proof would certify the structure theory on which the fastest matching algorithm depends. It would also provide reusable Lean infrastructure for shortest alternating paths in general graphs, which Mathlib does not have.

Difficulty

In bipartite graphs every prefix of a shortest alternating path is itself shortest ("BFS honesty"), so levels can be computed layer by layer. In general graphs this fails: the prefix of an even level($v$) path to an intermediate vertex can be arbitrarily longer than that vertex's level of the same parity, because the short path to it would have to reuse vertices. The obvious argument, induction along the path, therefore breaks.

The paper breaks a circularity: proving that $B(v)$ is a singleton needs blossoms, and blossoms need bases. It does so by induction on eligible tenacities, using blossoms of smaller tenacity. Lemma 13 is the main technical step, a long case analysis on how a shortest path can enter and leave a blossom.

Formalization scope

Vertices form a Fintype; G : SimpleGraph V; M : G.Subgraph with M.IsMatching. Alternating paths are Walk.IsPath walks satisfying the published BergeMatching.Core.IsAlternatingWrt, starting at a vertex satisfying BergeMatching.Core.IsNeutral (unmatched). Levels, tenacities, $l_m$ and $t_m$ live in ℕ∞ and are infima, so they are $\infty$ exactly when no path exists. The base is the relation IsBase M v b :↔ baseSet M v = {b}; no function picks a junk base. The blossom is one recursion on $t$, and "the blossoms of tenacity $t$" are those with base basal at stage $t$ and of tenacity greater than $t$, as in Definition 31. The subpath $p[b\text{ to }u]$ is read from $b$, whichever of $b,u$ comes first on $p$.

Two printed statements are adjusted, and the changes are declared on the items: Lemma 3, clause 2 needs finite tenacity (counterexample proved in Lean), and Lemma 20's last blossom is taken at tenacity $\min(s_i-2,t)$, the reading under which it is always defined.

The statement is not trivial: a sanity file proves that in a triangle with one matched edge, $t=3$ is eligible, the base of each matched vertex is the unmatched vertex, and the blossom of tenacity 3 is nonempty.

Useful contributions: lemmas about splitting and reversing simple walks, monotonicity of levels, and proofs of the §6 lemmas.

Selected references

• V. V. Vazirani, A Theory of Alternating Paths and Blossoms from the Perspective of Minimum Length, Math. Oper. Res. 49(3):2009–2047, 2024. https://doi.org/10.1287/moor.2020.0388
• S. Micali, V. V. Vazirani, An $O(\sqrt{|V|}\cdot|E|)$ algorithm for finding maximum matching in general graphs, FOCS 1980. https://doi.org/10.1109/SFCS.1980.12
• J. E. Hopcroft, R. M. Karp, An $n^{5/2}$ algorithm for maximum matchings in bipartite graphs, SIAM J. Comput. 2(4), 1973. https://doi.org/10.1137/0202019
• J. Edmonds, Paths, trees, and flowers, Canad. J. Math. 17, 1965. https://doi.org/10.4153/CJM-1965-045-4
• V. V. Vazirani, A theory of alternating paths and blossoms for proving correctness of the $O(\sqrt V E)$ general graph maximum matching algorithm, Combinatorica 14(1):71–109, 1994 (cited as [34] in the 2024 paper).

Why perfectly correlated service and patience

Many-server queues with customer abandonment are the standard model of call and contact centers. The textbook model, the Erlang-A queue $M/M/n+M$, assumes that a customer's patience is independent of its service requirement. In practice a customer's patience depends on its service requirement, as empirical studies of contact centers and restaurants cited by the paper show. Yu and Perry (arXiv:2008.12890, Mathematics of Operations Research 2023) study the extreme case, in which patience and service requirement are perfectly correlated, and ask how the system behaves under the square-root staffing rule of the Halfin–Whitt regime.

Timeline of the relevant limits:

• Halfin and Whitt (1981): the diffusion limit of the Erlang-C queue $M/M/n$ under square-root staffing with $\beta>0$.
• Garnett, Mandelbaum and Reiman (2002, doi:10.1287/msom.4.3.208.7753): the Erlang-A diffusion limit, valid for every $\beta\in\mathbb R$, with drift $-(\beta+\theta x)$ above $0$.
• Pang, Talreja and Whitt (2007, doi:10.1214/06-PS091): martingale proofs of these limits, including the continuity of the integral representation used below.
• Yu and Perry (2020): with perfectly correlated patience the diffusion limit is the Erlang-C one for every $\beta\in\mathbb R$, even though customers abandon. For $\beta\le0$ the queue lives on the larger scale $n^{3/4}$ and time scale $n^{1/4}$.

The model

System $n$ has $n$ statistically identical servers and an infinite buffer. Customers arrive in a Poisson process of rate $\lambda_n$, are served in arrival order (FIFO), and a server never idles while a customer waits. Time is measured in units of mean service time ($\mu=1$). Each customer carries a pair $(S,T)$ with $S\sim\mathrm{Exp}(1)$ its service requirement and $T=S/\theta$ its patience, $\theta>0$. If the wait in queue reaches $T$ before service starts, the customer abandons. By memorylessness, a customer who has waited $w$ has service time $\theta w+\hat S$ with $\hat S\sim\mathrm{Exp}(1)$: a deterministic phase 1 of length $\theta w$ and an exponential phase 2 (2.1).

$X^n(t)$ is the number of customers in the system, $Q^n(t)$ the number waiting, and $Z^n(t)=X^n(t)\wedge n$ the number in service. At time $0$ the system may hold customers who have already waited ($\ell_i$, their elapsed waits) and customers in service with residual phase-1 times $r_j$. Their total is $L^n(0)=\sum_j r_j+\sum_i\ell_i$ (3.8). The square-root staffing rule is

$$\beta_n=\frac{n-\lambda_n}{\sqrt n}\to\beta\in\mathbb R\qquad(1.1).$$

The diffusion-scaled process is $\hat X^n=n^{-1/2}(X^n-n)$. The initial condition (Ia) requires $\hat X^n(0)\Rightarrow X_0$ and $n^{-1/2}L^n(0)\Rightarrow0$.

Formalization targets

Goal: Theorem 2* (p.10)

Under (1.1) and (Ia),

$$\hat X^n\Rightarrow\hat X_C\quad\text{in }D,\qquad d\hat X_C=m_C(\hat X_C)\,dt+\sqrt2\,dB,\quad \hat X_C(0)=X_0,$$

with $m_C(x)=-\beta$ for $x\ge0$ and $m_C(x)=-(\beta+x)$ for $x<0$, and $X_0$ independent of $B$. Theorem 2 (p.7) is the case $L^n(0)=0$.

Milestones

The milestones follow the proof. They work on the LOF scale: $\tilde Y^n(t)=n^{-3/4}Y^n(n^{1/4}t)$, with $\tilde w^n(t)=n^{1/4}w^n(n^{1/4}t)$ for the head-of-line wait $w^n$. These results hold under (1.1) and the weaker initial condition (Ib).

1. Proposition 5.2(a): the initial customers are negligible, and the time $T^n_0$ at which the initial queue clears tends to $0$.
2. Lemma 6.1: $\tilde Q^n$ is stochastically bounded.
3. Proposition 5.2(b): the scaled arrival, service and abandonment martingales vanish.
4. Lemma 6.2: $\tilde w^n$ is stochastically bounded.
5. Lemma 6.3: $F^n(\cdot,t)$ (4.9) is a martingale, and $e^{\theta t}\sup_{s\le t}|F^n(s,t)|$ is a submartingale.
6. Proposition 5.2(c),(d): the correction terms $U^n_1,U^n_2$ vanish.
7. Lemma 6.4: the asymptotic form (6.12) of the term $V^n$.
8. Lemma 6.5: $\tilde X^n,\tilde Z^n,\tilde Z^n_1-\tilde Z^n_0,\tilde Z^n_2+\tilde Z^n_0$ are stochastically bounded.
9. Proposition 5.3: $\tilde Q^n$ is C-tight.
10. Display (6.25): $\tilde Q^n-\tilde Q^n_0-\tilde w^n\Rightarrow0$.

Under (Ia) on the diffusion scale:

11. The claim on p.31: $n^{1/4}T^n_0\Rightarrow0$.
12. Proposition 5.1: the residual terms vanish, and $(\hat M^n_A,\hat M^n_S,\hat M^n_R)\Rightarrow(B_1,B_2,0)$.
13. Display (5.3), stated jointly with $\hat X^n(0)$: the noise term converges to $\sqrt2B$.

The last step, continuity of the solution map of $x(t)=x(0)-\beta t-\int_0^tx(s)\wedge0\,ds+y(t)$ (5.4), is Theorem 4.1 of Pang–Talreja–Whitt. It is already an open item on the platform (MartingaleHT.InfiniteServer.theorem_4_1_i, with $h(x)=-\min(x,0)$) and is not posed again.

Significance

The theorem says that, in the Halfin–Whitt regime, perfectly correlated abandonment does not change the diffusion limit of the number in system: abandonment removes customers whose service would have been short, and the customers who stay pay for their wait with an equal amount of phase-1 service. Consequently, for $\beta<0$ the diffusion limit is transient although every prelimit is positive recurrent. The paper then identifies the $n^{3/4}$ scale on which the queue does stabilize (Theorems 4 and 5, not part of this mission). The comparison with the Erlang-A limit, whose drift $-(\beta+\theta x)$ above $0$ keeps the process recurrent for every $\beta$, shows that how patience depends on service changes the qualitative behaviour of the QED regime.

The result is proved in the paper; none of it is formalized. The mission adds a machine-checked model of a non-Markovian many-server queue with customer-level primitives, an explicit FIFO recursion, and the martingale and LOF-scale estimates on which the proof rests. It is the platform's second Halfin–Whitt process limit next to the open Erlang-A theorem.

Difficulty

The obvious route fails. $X^n$ is not Markov. Its departure process depends on how long each customer waited, so the generator and martingale methods of the Erlang-A proof do not apply directly. The paper's representation (4.12) carries three correction terms ($U^n_1$, $U^n_2$, $V^n$) built from the head-of-line wait. The paper shows that they vanish on the diffusion scale by first controlling them on the larger LOF scale, where the queue and the head-of-line wait are of order one. Two further hazards are known. The printed proof of Proposition 5.2(d) uses a time-invariance of $F^n(s,t)$ that does not hold: the window quantity $F^n(t,t)-F^n(s,t)$ is shift-invariant, and the union bound must be run on it. And the representation (4.12) is off by one customer at the head of the line.

Formalization scope

The model is a pathwise construction (PerfCorrMSQ.FifoAbandon, PerfCorrMSQ.System). Customers who ever wait are indexed in FIFO order: the initial waiting customers first, then the arrivals. A served customer starts at $\max(\text{arrival},\text{earliest free server})$ and is served iff that time is strictly before its deadline. Every process of the paper is a function of this construction. Abandonment is therefore tied to service through $T=S/\theta$, not modelled by an independent Poisson clock, which would give the Erlang-A model. The probabilistic hypotheses (PerfCorrMSQ.IsModel) are:

• independent exponential primitives;
• an initial state independent of them, with an arbitrary joint law;
• remaining patience $\mathrm{Exp}(\theta)$ for initial waiting customers.

The paper leaves the last two implicit.

Time is real and used for $t\ge0$. Counts are Set.ncard. "$\Rightarrow0\eta$" is uniform convergence on compacts in probability. Convergence to a random limit is PuhaWardFluid.Limit.ConvInDist ($J_1$, coupling form). Statements about a limit object assert both that the object exists and that the convergence holds to every such object, so no statement is vacuous. The limit SDE is the public ErlangA.Diffusion.IsDiffusionSolution with abandonment rate $0$. Display (5.3) is stated with the sign that follows from (5.2): the printed $-\int\hat X^n\wedge0$ is a typo for $+\int$. The list on p.13 prints $Q^n$ in the definition of $\tilde Q^n_0$, a typo for $Q^n_0$; the statements use $Q^n_0$.

Reusable beyond this mission: the generic FIFO recursion with abandonment, and the natural-filtration submartingale notion. Contributions on the Poisson FCLT, the martingale FCLT and the continuity of (5.4), all open on the platform, serve this mission and others.

Selected references

• L. Yu, O. Perry, Many-Server Heavy-Traffic Limits for Queueing Systems with Perfectly Correlated Service and Patience Times, arXiv:2008.12890v1, 2020; Mathematics of Operations Research, 2023. https://arxiv.org/abs/2008.12890
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• O. Garnett, A. Mandelbaum, M. Reiman, Designing a call center with impatient customers, Manufacturing & Service Operations Management 4(3), 2002. https://doi.org/10.1287/msom.4.3.208.7753
• G. Pang, R. Talreja, W. Whitt, Martingale proofs of many-server heavy-traffic limits for Markovian queues, Probability Surveys 4, 2007. https://doi.org/10.1214/06-PS091

Motivation

A retailer choosing which products to display, a platform choosing which items to recommend, and a broadcaster choosing which content to stream all face an assortment problem: offer a set of products, observe what customers buy, and earn the revenue of the purchased item. The standard demand model is the multinomial logit (MNL) model, under which the optimal assortment without capacity constraints consists of the most profitable products (Talluri and Van Ryzin, 2004). When the customers' preferences are unknown, the seller must learn them from sales, and the quality of a learning policy is measured by its regret: the cumulative revenue lost relative to an omniscient seller.

When the product catalogue is very large, or products are described by a continuous attribute such as quality, the discrete model becomes a continuum. Peeters, den Boer and Mandjes (arXiv:1807.06497, published in Operations Research, 2022) introduced a continuous analogue of the MNL model and studied learning in it. Their first main result, the goal of this mission, is that a simple stochastic approximation policy has worst-case regret of order $\log T$ over $T$ customers.

• 1951: Robbins and Monro introduce stochastic approximation for finding the root of a function observed with noise (doi:10.1214/aoms/1177729586).
• 2010: Rusmevichientong, Shen and Shmoys give adaptive policies for capacitated MNL assortment (doi:10.1287/opre.1100.0866).
• 2011: Broadie, Cicek and Zeevi give mean-square rates for Kiefer–Wolfowitz type stochastic approximation (doi:10.1287/opre.1110.0970).
• 2019: Agrawal, Avadhanula, Goyal and Zeevi give an $\tilde O(\sqrt{NT})$-regret UCB policy for discrete MNL bandits (doi:10.1287/opre.2018.1832).
• 2021/2022: Peeters, den Boer and Mandjes prove $O(\log T)$ worst-case regret for the continuum model, with a matching $\Omega(\log T)$ lower bound.

Setting

The products are the points $x\in[0,1]$, and the revenue function $w:[0,1]\to[0,1]$ is continuously differentiable with $w'\ge k>0$. An assortment is a Borel set $S\subseteq[0,1]$; $\mathcal S$ is the set of all of them. A customer offered $S$ buys a product in a Borel set $A\subseteq S$, or buys nothing ($\emptyset$), with probabilities

$$\mathbb P(X^S\in A)=\frac{\int_A v(x)\,dx}{1+\int_S v(x)\,dx},\qquad \mathbb P(X^S=\emptyset)=\frac{1}{1+\int_S v(x)\,dx},$$

where the preference function $v$ is unknown to the seller. The expected revenue of $S$ is $r(S,v)=\int_S vw\big/(1+\int_S v)$, and $\varrho^*=\max_{S\in\mathcal S}r(S,v)$.

The class $\mathcal V(\underline v,\overline v,D)$ (Assumption 1) contains the integrable $v$ with $\underline v\le v\le\overline v$ on $[0,1]$ that are differentiable on $(0,1)$ with $|v'|\le D$, where $\overline v>\underline v>0$ and $\overline v>w(0)/\int_0^1(w-w(0))$.

The generalized inverse is $w^{-1}(\varrho)=\min\{x\in[0,1]:w(x)\ge\varrho\}$, and $h(\varrho)=r([w^{-1}(\varrho),1],v)$. The policy SAP$(\alpha,\beta)$ starts at $\varrho_1\in[0,1]$, offers $S_t=[w^{-1}(\varrho_t),1]$ in period $t$, observes the revenue $R_t=w(X_t)\mathbf 1\{X_t\in S_t\}$, and updates

$$\varrho_{t+1}=\varrho_t+\frac{\alpha}{t+\beta}\,(R_t-\varrho_t).$$

Given the history, the purchase $X_t$ has the law of $X^{S_t}$. The regret over $T$ periods is $\Delta_\pi(T,v)=\sum_{t=1}^T\mathbb E_\pi[\varrho^*-r(S_t,v)]$.

Formalization targets

Goal: Theorem 1 (p.12)

For $\alpha\ge\overline v+1$ and $\beta\ge\max\{0,\alpha-1\}$ there is $\overline C>0$ such that for all $T\ge2$

$$\sup_{v\in\mathcal V}\Delta_\pi(T,v)\le\overline C\log T.$$

The constant depends on $w$, the class and the policy, but not on $T$ or $v$.

Milestones, in proof order

1. Well-posedness: an SAP purchase process exists for every horizon.
2. §4.1: the optimum over $\mathcal S$ is attained by an interval $[w^{-1}(\varrho),1]$.
3. Lemma 4: $h(\varrho^*)=\varrho^*$; the drift inequality (23) $(\varrho-\varrho^*)(h(\varrho)-\varrho)\le-(\varrho-\varrho^*)^2/(1+\overline v)$; the derivative $g'=(g-w)\xi$ and the curvature bound (27); the quadratic gap (24) $h(\varrho^*)-h(\varrho)\le C(\varrho-\varrho^*)^2$ with $C$ uniform over $\mathcal V$.
4. The iterates stay in $[0,1]$, and $\mathbb E[R_t\mid\text{history}]=h(\varrho_t)$.
5. The recursion (25) $\delta_{t+1}\le\delta_t\big(1-\frac{2}{1+\overline v}\frac{\alpha}{t+\beta}\big)+\frac{\alpha^2}{(t+\beta)^2}$ for $\delta_t=\mathbb E[(\varrho_t-\varrho^*)^2]$, and Lemma 5, $\delta_t\le\kappa/(t+\beta)$.
6. The regret identity $\Delta_\pi(T,v)=\sum_t\mathbb E[h(\varrho^*)-h(\varrho_t)]$ and $\sum_{t=1}^T(t+\beta)^{-1}\le3\log T$.

Significance

The theorem shows that in the continuum logit model the seller does not need to estimate the preference function: a one-dimensional Robbins–Monro recursion on the observed revenue finds the optimal revenue level, and the loss is logarithmic in the horizon. This is faster than the $\sqrt T$ rates typical of continuum-armed bandits, and the paper's Theorem 2 shows it is optimal. The bound is worst-case over a class of preference functions, which matters when nothing is known about the customers beyond the class.

The result is proved on paper. No part of it is formalized on the platform. The mission adds the platform's first continuum-indexed choice model, a measure-theoretic model of a sequential learning policy whose decisions depend on the full purchase history, and a complete regret analysis for a stochastic approximation policy. The discrete MNL bandit of Agrawal et al. is on the platform as MNLBandit.UCB; it is a related, not a reused, model.

Difficulty

The policy itself is three lines; the difficulty is in the analysis of the map $h$. The obvious route — "$h$ is a contraction, so the iterates converge" — fails: $h$ is not a contraction, and $\varrho\mapsto h(\varrho)$ is flat below $w(0)$ and drops to zero above $w(1)$. The proof instead needs the one-sided drift inequality (23), whose constant must use the upper bound $\overline v$, and the quadratic gap (24), which requires a second-order Taylor expansion of $g(y)=r([y,1],v)$ with a curvature bound (27) that is uniform over the class. The bound (27) needs $v$ differentiable, and the uniformity of $C$ and $\kappa$ over $\mathcal V$ is what turns per-instance bounds into a worst-case one.

The induction in the proof of Lemma 5 multiplies by $1-2\alpha/((1+\overline v)(t+\beta))$, which is negative for small $t$ when $\overline v$ is small; the printed $\kappa=\max\{1+\beta,\alpha(1+\overline v)\}$ does not follow from the printed step there, although the lemma's statement (some $\kappa>0$) remains true.

Formalization scope

Products are reals and purchases live in ℝ ⊕ Unit (Sum.inr () is no-purchase). $w,v:\mathbb R\to\mathbb R$ carry hypotheses only on $[0,1]$ and $(0,1)$. $\mathcal S$ is the measurable subsets of $[0,1]$ (the uncapacitated case $c=1$), and $\varrho^*$ is a supremum (sSup), shown to be a maximum in a milestone. The paper's $\min\{x:w(x)\ge\varrho\}$ is empty for $\varrho>w(1)$, which SAP can reach since $\varrho_1\in[0,1]$ is arbitrary; there $w^{-1}(\varrho):=1$, so the offered assortment $\{1\}$ is a null set. Lean's sInf ∅ = 0 would instead offer $[0,1]$ and break (23). The class has a fixed derivative bound $D$, since Assumption 1(ii)'s supremum over all admissible $v$ is otherwise infinite.

Time is 0-based ($n=t-1$). A horizon-$T$ process is a probability space with measurable purchases $X_0,\dots,X_{T-1}$ whose conditional law given the history is the choice law of the offered assortment, written as an identity of measures on history events. A Lean proof that the SAP iterate is a measurable function of the history exists, so the expectations in the regret are genuine integrals. The goal quantifies over all such processes, and a milestone asserts that one exists, so the goal is not vacuous.

A complete development needs: second-order calculus for parameter integrals $y\mapsto\int_y^1$; the construction of a process from a history-dependent kernel (Ionescu–Tulcea, ProbabilityTheory.Kernel.traj, or an iterated Measure.bind); and conditional expectations given a history σ-algebra. The mean-square recursion and the harmonic-sum bound are reusable for other Robbins–Monro analyses. Contributions to any milestone are welcome, in any order; milestones 2–3 and 6 are independent of the process construction.

Selected references

• Y. Peeters, A. V. den Boer, M. Mandjes, Continuous Assortment Optimization with Logit Choice Probabilities under Incomplete Information, arXiv:1807.06497v4, 2021; Operations Research, 2022. https://arxiv.org/abs/1807.06497
• H. Robbins, S. Monro, A Stochastic Approximation Method, Annals of Mathematical Statistics 22(3), 1951. https://doi.org/10.1214/aoms/1177729586
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic Assortment Optimization with a Multinomial Logit Choice Model and Capacity Constraint, Operations Research 58(6), 2010. https://doi.org/10.1287/opre.1100.0866
• M. Broadie, D. Cicek, A. Zeevi, General Bounds and Finite-Time Improvement for the Kiefer-Wolfowitz Stochastic Approximation Algorithm, Operations Research 59(5), 2011. https://doi.org/10.1287/opre.1110.0970
• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5), 2019. https://doi.org/10.1287/opre.2018.1832

Motivation

An online experiment has two audiences. The experimenter who cares about welfare wants to stop assigning people to inferior treatments as quickly as possible; the statistician wants an accurate estimate of how much better one treatment is than another. A multi-armed bandit policy serves the first and starves the second: an arm that is played rarely is estimated badly. A randomized controlled trial does the opposite, at the price of regret linear in the sample size. Simchi-Levi and Wang (SSRN 4224969, published in Management Science, 2024) study this trade-off for stochastic bandits and give a design, EXP3EG, whose single parameter $\alpha\in[0,1]$ moves along it. This mission formalizes the finite-sample inference guarantee of that design.

Setting

There are $K\ge2$ arms. Pulling arm $a$ yields a reward with law $P_a$ on $[-1,1]$ and mean $\mu_a$. The treatment effect of arm $i$ against arm $j$ is $\Delta^{(i,j)}=\mu_i-\mu_j$.

EXP3EG (Algorithm 2) takes inputs $\alpha\in[0,1]$ and $\delta$, and sets $C=(4K^2(e^2+1)+2)^2(\log(2/\delta))^2$, $\varepsilon_t=1/\sqrt{Ct}$ and $\alpha_t=1/(Kt^\alpha)$. It keeps an active set $\mathcal A_t$, starting from all arms, and inverse-propensity-weighted cumulative estimates $\hat R_t(a)$, starting from $0$. In round $t$, each arm outside $\mathcal A_t$ gets probability $\pi_t(a)=\alpha_t$ (forced exploration), and the remaining mass $1-|\mathcal A_t^c|\alpha_t$ is split over $\mathcal A_t$ in proportion to $e^{\varepsilon_{t-1}\hat R_{t-1}(a)}$. The arm $A_t\sim\pi_t$ is pulled, the reward $R_t$ is observed, and

$$\hat R_t(a)=\hat R_{t-1}(a)+\frac{R_t}{\pi_t(a)}\mathbb I_{a=A_t},\qquad\mathcal A_{t+1}=\mathcal A_t\setminus\{a:\hat R_t^{\max}-\hat R_t(a)>2\sqrt{Ct}\}.$$

The estimate of the treatment effect is $\hat\Delta_t^{(i,j)}=(\hat R_t(i)-\hat R_t(j))/t$, and its error is $e(n,\hat\Delta^{(i,j)})=\mathbb E|\Delta^{(i,j)}-\hat\Delta_n^{(i,j)}|$.

Formalization targets

Goal: Theorem 7

For every $\alpha\in[0,1]$, $\delta\in(0,2/e)$, instance with rewards in $[-1,1]$, $i\ne j$ and $t\ge1$, with probability at least $1-\delta$,

$$\big|\hat\Delta_t^{(i,j)}-\Delta^{(i,j)}\big|\le\frac{4(2+2K^2(1+e^2))\log(2/\delta)}{\sqrt{t^{1-\alpha}}},$$

and there is $c$ depending only on $K$ such that, with $\delta=1/(2n^2)$,

$$\max_{i<j\le K}e(n,\hat\Delta^{(i,j)})\le\frac c{\sqrt{n^{1-\alpha}}}\quad\text{for all }n\ge1,\ \alpha\in[0,1]\text{ and all instances}.$$

Milestones

In the order the paper's proof uses them: the propensity bound (EC.7); the martingale $\hat R_t(a)-t\mu_a$; unbiasedness of $\hat\Delta_t^{(i,j)}$; the increment bound; the conditional second-moment bound (EC.11); the bound $V_t^{(i,j)}\le(2C'+1)(t+1)^{1+\alpha}$ on the variance proxy, with $C'=K^2(1+e^2)$; the real inequality (EC.12); and Bernstein's inequality for martingales (Theorem EC.1).

Significance

Theorem 7 is the only result of the paper about EXP3EG with explicit constants. Together with the paper's regret bound $\tilde O(n^{1-\alpha})$, it says that one design attains error $O(1/\sqrt{n^{1-\alpha}})$ at every point of the trade-off, for every pair of arms and without a gap assumption. The paper's headline, a characterization of Pareto optimality (Theorem 8), is not the goal here: Pareto optimality there compares quantities only by their order in $n$, ignoring constants and logarithms, so it has no fixed formal content. Theorem 7 is the precise statement underneath it.

The result is proved on paper, not previously formalized. This mission adds a machine-checked model of an adaptive design whose estimators are inverse-propensity weighted, on top of the published BanditAlgorithm canonical bandit model.

Two statements are deliberately not the printed ones. "With probability at least $1-\delta$, for all $t\in[n]$" in Theorem 7, and the same clause in Theorem EC.1, are false as uniform-in-time claims: with $K=2$, $\alpha=0$, $\delta=1/2$ and arms taking values $\pm1$ with means $\pm1/2$, the law of the iterated logarithm for martingales (Stout 1970) makes the bound fail infinitely often almost surely, and for Theorem EC.1 i.i.d. $\pm1$ steps do the same. Both are stated for each fixed $t$. The paper's $O(\cdot)$ clause is pinned as above; it is true, but it does not follow by integrating the high-probability bound, which leaves a factor $\log n$.

Difficulty

The natural martingale has increments of size $1/\pi_t(a)$, and forced exploration makes these grow like $Kt^\alpha$ for eliminated arms. So neither Azuma–Hoeffding with a fixed range nor a fixed-variance Bernstein bound applies directly. The range and the variance both grow with $t$, and they must be controlled along the adaptive run by a deterministic sequence, separately for active and eliminated arms, before any concentration inequality can be invoked. The active-arm bound (EC.7) depends on the interplay of the elimination threshold $2\sqrt{Ct}$ and the learning rate, not on any property of the reward laws.

Formalization scope

The bandit is the published BanditAlgorithm.StochasticBandit K, a policy the published BanditPolicy K, and the law of $n$ rounds the published banditMeasure, the canonical law of the observed history. Only the observed history matters, so the joint law of the rewards of different arms is not modelled. Rewards in $[-1,1]$ are a hypothesis (RewardsBounded), not part of the bandit.

EXP3EG is a deterministic recursion on the observed history in the module BanditExpDesign.EXP3EG: $\hat R_t$ is computed by the update above and is never defined from the means. Conventions: arms are Fin K; rounds are numbered from $1$, and a history of $n$ rounds is a function on Fin n; the logarithm is natural; $t^\alpha$ is Real.rpow; $\varepsilon_0=0$, which is irrelevant since $\hat R_0=0$; and $\hat R_t^{\max}$ is the maximum over the active set. The paper's p.13 writes the maximum over all arms, under which the active set can empty and $\pi_t$ stops being a probability vector; its proofs use the active-set maximum. The module proves that $\mathcal A_t\ne\emptyset$, that $\pi_t>0$ and $\sum_a\pi_t(a)=1$, and that the kernel is measurable.

A trivializing reading is excluded: expectations come with integrability in the statements where the Bochner integral's junk value could otherwise hide the claim.

A complete development needs a martingale concentration library around Theorem EC.1, conditional expectations under banditMeasure, and a one-step disintegration of the law of the history; these are reusable for other adaptive-experiment results. Contributions to any milestone are welcome.

Selected references

• D. Simchi-Levi, C. Wang, Multi-armed Bandit Experimental Design: Online Decision-making and Adaptive Inference, SSRN 4224969. https://ssrn.com/abstract=4224969; published in Management Science, 2024. https://doi.org/10.1287/mnsc.2023.00492
• D. A. Freedman, On tail probabilities for martingales, Annals of Probability 3(1), 100–118, 1975. https://doi.org/10.1214/aop/1176996452
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 48–77, 2002. https://doi.org/10.1137/S0097539701398375
• W. F. Stout, A martingale analogue of Kolmogorov's law of the iterated logarithm, Zeitschrift für Wahrscheinlichkeitstheorie 15, 279–290, 1970. https://doi.org/10.1007/BF00534922

Why error bounds for conic feasibility

The conic feasibility problem asks for a point of $(\mathcal L+a)\cap\mathcal K$, where $\mathcal K$ is a closed convex cone in a finite dimensional Euclidean space, $\mathcal L$ is a subspace and $a$ is a point. An error bound estimates the distance from a trial point $x$ to that intersection using only the two individual distances $\operatorname{dist}(x,\mathcal K)$ and $\operatorname{dist}(x,\mathcal L+a)$. Such estimates control how far an approximately feasible point is from a truly feasible one, and they enter convergence rate analysis of first-order methods (Liu and Lourenço, arXiv:2008.12968) and the computation of Kurdyka–Łojasiewicz exponents.

The history for one family of cones runs as follows. For the $p$-cones $\mathcal K_p^{n+1}=\{(x_0,\bar x):x_0\ge\|\bar x\|_p\}$, the cases $p=1,\infty$ are polyhedral, so Lipschitzian bounds hold by Hoffman's lemma (1952). For $p=2$ the exponent $\frac12$ follows from the Luo–Sturm analysis of second-order cones. Lourenço (Amenable cones, 2021) introduced facial residual functions and conjectured exponent $\frac1p$ for every $p$-cone. Lindstrom, Lourenço and Pong (2022) extended the framework to non-amenable cones. The paper formalized here, arXiv:2109.11729v4, determines the optimal exponents for all $p\in(1,\infty)$, and they differ from the conjecture.

The setting

Fix a finite dimensional Euclidean space $\mathcal E$. Write $\operatorname{dist}(x,C)=\inf_{y\in C}\|x-y\|$ and $P_C$ for the projection onto $C$. Two closed convex sets $C_1,C_2$ with $C_1\cap C_2\ne\emptyset$ satisfy a uniform Hölderian error bound with exponent $\gamma\in(0,1]$ if for every bounded $B$ there is $\kappa_B>0$ with

$$\operatorname{dist}(x,C_1\cap C_2)\le\kappa_B\max\{\operatorname{dist}(x,C_1),\operatorname{dist}(x,C_2)\}^\gamma\qquad\forall x\in B.$$

The case $\gamma=1$ is Lipschitzian. The partial-polyhedral Slater condition is a constraint qualification under which a Lipschitzian bound holds.

For $z\in\mathcal K^*$, the set $\mathcal F=\mathcal K\cap\{z\}^\perp$ is an exposed face. A one-step facial residual function (1-FRF) $\psi$ bounds $\operatorname{dist}(x,\mathcal F)$ by $\psi(\epsilon,\|x\|)$ whenever $\operatorname{dist}(x,\mathcal K)\le\epsilon$ and $\langle x,z\rangle\le\epsilon$. A consistent error bound function $\Phi$ is a monotone function with $\Phi(0,b)=0$ that bounds $\operatorname{dist}(x,\bigcap_iC_i)$ by $\Phi(\max_i\operatorname{dist}(x,C_i),\|x\|)$; this notion covers Hölderian bounds and more general ones.

For $p,q\in(1,\infty)$ with $\frac1p+\frac1q=1$, the dual of $\mathcal K_p^{n+1}$ is $\mathcal K_q^{n+1}$. For $z=(z_0,\bar z)$ put $J_z=\{i:\bar z_i\ne0\}$ and

$$\alpha_z=\begin{cases}\frac12&|J_z|=n,\\\frac1p&|J_z|=1,\ p<2,\\\min\{\frac12,\frac1p\}&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 4.3

Let $n\ge2$, $p\in(1,\infty)$, $\frac1p+\frac1q=1$, and $(\mathcal L+a)\cap\mathcal K_p^{n+1}\ne\emptyset$. If this intersection is $\{0\}$ or meets $\operatorname{ri}\mathcal K_p^{n+1}$, a Lipschitzian bound holds. Otherwise a vector $z\in\partial\mathcal K_q^{n+1}\cap\mathcal L^\perp\cap\{a\}^\perp$, $z\ne0$, exists, and every such $z$ gives a uniform Hölderian error bound with exponent $\alpha_z\ge\min\{\frac12,\frac1p\}$. Moreover, for every $z\in\partial\mathcal K_q^{n+1}\setminus\{0\}$, every consistent error bound function $\Phi$ for $\mathcal K_p^{n+1},\{z\}^\perp$ and every $\hat\eta>0$,

$$s^{\alpha_z}\le\hat\kappa\,\Phi(\hat\kappa s,\hat\eta)\qquad\forall s\in[0,s_0],$$

for some $\hat\kappa,s_0>0$, and no Hölderian exponent $\hat\alpha\in(\alpha_z,1]$ is possible.

Milestones

• General framework: Proposition 2.1, Lemma 2.3, Lemma 2.5, Theorem 2.2, Theorem 3.1, Theorem 3.2, Corollary 3.1. These hold for any closed convex cone.
• The $p$-cone: the basic facts of §4, the exposing vector of the proof of Theorem 4.3, the face formula (4.5), Lemma 4.1, Theorem 4.1, Lemmas 4.2 and 4.3, Theorem 4.2.

What the result gives

The theorem gives the sharp behaviour of feasibility residuals over every $p$-cone with no constraint qualification. In the source it yields Kurdyka–Łojasiewicz exponents for $p$-norm regularized least squares, and a short proof that most $p$-cones are neither self-dual nor homogeneous. The optimality statement is stronger than a claim about exponents, since it compares against all consistent error bound functions.

The paper's result is proved, and a search of the platform found no machine-checked proof of it. This mission states the results at full strength. The formal work is the proof of these statements, and a library of error bounds for sets. The platform currently has Hoffman's theorem as a proved result, and nothing on facial residual functions.

Where the difficulty lies

Without a constraint qualification, the first natural step, estimating $\operatorname{dist}(x,(\mathcal L+a)\cap\mathcal K)$ by a compactness argument, gives no rate: the constant degenerates exactly near the face where $\mathcal L+a$ touches $\mathcal K$. The obvious guess, one exponent $\frac1p$ for all faces, fails because the local shape of $\partial\mathcal K_p^{n+1}$ near an extreme ray depends on the zero pattern of the exposing vector. Near a nonzero entry of the ray the boundary has order two, and near a zero entry it has order $p$. The two directions then have to be combined along every possible approach to the face, and the matching lower bound needs an explicit curve for each case, and the list of cases differs between $n=2$ and $n\ge3$.

Formalization scope

$\mathbb R^{n+1}$ is EuclideanSpace ℝ (Fin (n + 1)), with $x_0$ = x 0 and $\bar x_i$ = x i.succ. The $p$-norm is an explicit sum of real powers. Distances are Metric.infDist on nonempty sets, the dual cone is ProperCone.innerDual, $\operatorname{ri}$ is intrinsicInterior ℝ, and $\partial$ is frontier, the topological boundary, also for lower-dimensional cones. Projections are the predicate IsProj. The quantity $\gamma_{z,\eta}$ lies in ENNReal, with the empty infimum equal to $+\infty$. Functions on $\mathbb R_+$ are functions on ℝ with their conditions on Set.Ici 0. Definition 2.1 keeps "for every bounded $B$ there is $\kappa_B$" in that order: a single global constant would be a different, false claim for $\alpha_z<1$. The optimality clause quantifies over consistent functions, which exist, so it is not vacuous.

A complete development needs: projections onto cones and hyperplanes, the Bauschke–Borwein–Li bound for Proposition 2.1 (the polyhedral case can use Hoffman's theorem, already proved on the platform), Hölder equality analysis, and separation for the exposing vector. The general framework is reusable for other cones, and contributions to it are welcome separately from the $p$-cone part. Theorem 4.4 and the applications of §5 are out of scope.

Selected references

• S. B. Lindstrom, B. F. Lourenço, T. K. Pong, Optimal error bounds in the absence of constraint qualifications with applications to the p-cones and beyond, arXiv:2109.11729v4, 2024. https://arxiv.org/abs/2109.11729
• S. B. Lindstrom, B. F. Lourenço, T. K. Pong, Error bounds, facial residual functions and applications to the exponential cone, Mathematical Programming 200, 2022. https://doi.org/10.1007/s10107-022-01883-8
• B. F. Lourenço, Amenable cones: error bounds without constraint qualifications, Mathematical Programming 186, 2021. https://doi.org/10.1007/s10107-019-01439-3
• T. Liu, B. F. Lourenço, Convergence analysis under consistent error bounds, arXiv:2008.12968. https://arxiv.org/abs/2008.12968
• B. F. Lourenço, M. Muramatsu, T. Tsuchiya, Facial reduction and partial polyhedrality, SIAM Journal on Optimization 28(3), 2018. https://doi.org/10.1137/15M1051634
• H. H. Bauschke, J. M. Borwein, W. Li, Strong conical hull intersection property, bounded linear regularity, Jameson's property (G), and error bounds in convex optimization, Mathematical Programming 86(1), 1999. https://doi.org/10.1007/s101070050083

Motivation

Dynamic programs in operations research and economics are routinely used to ask comparative statics questions: when a parameter of the model increases, does the optimal decision increase? For Markov decision processes the classical answer, going back to Topkis (1978) and his book Supermodularity and Complementarity (1998, cited by the paper as Topkis (2011)), concerns the policy function $g(s)$, the decision taken in a given state. In a stochastic model the decision maker's future states are random, so the decision in a future period is a random variable from the point of view of period 1. Light (2021) asks the stochastic version of the question: does the expected decision in every future period increase with the parameter? The same quantity is the aggregate decision of a continuum of agents facing idiosyncratic shocks, which is the object of interest in stationary equilibrium and mean field models.

Timeline. Monotone optimal policies in Markov decision processes via increasing differences: Topkis (1978); Lovejoy (1987) and Hopenhayn and Prescott (1992) prove that the maximum over an ascending feasible set preserves increasing differences and use it for stochastic monotonicity of dynamic economies. Comparison of Markov chains in integral stochastic orders: Müller and Stoyan (2002, Chapter 5). Light (arXiv 2019, Mathematics of Operations Research 2021) combines the two to derive comparative statics of expected future decisions from the primitives of the model, including the first general result that the policy increases with the discount factor.

Setting

A discounted dynamic program is a tuple $(S,A,\Gamma,p,r,\beta)$. The state space $S$ is a measurable space with a partial order $\le$. The action space is $A\subseteq\mathbb R$, and $\Gamma(s)\subseteq A$ is the non-empty set of feasible actions in state $s$. The transition probability $p(s,a,\cdot)$ is the law of the next state, $r(s,a)$ is the single-period payoff, and $0<\beta<1$ is the discount factor. For $f:S\to\mathbb R$,

$$h(s,a,f)=r(s,a)+\beta\int_S f(s')\,p(s,a,ds'),\qquad Tf(s)=\max_{a\in\Gamma(s)}h(s,a,f).$$

The value function $V$ satisfies $TV=V$ and is the uniform limit of the iterates $T^n0$. The optimal policy correspondence is $G(s)=\{a\in\Gamma(s):V(s)=h(s,a,V)\}$ and the policy function is $g(s)=\max G(s)$.

Starting from $s(1)$ and following $g$, the state of period $t$ has law $\mu^t$: $\mu^1=\delta_{s(1)}$ and $\mu^{t+1}(B)=\int_S p(s,g(s),B)\,\mu^t(ds)$. The expected decision in period $t$ is $\mathbb E^t(g)=\int_S g\,d\mu^t$.

A function $f(x,e)$ has increasing differences if $f(x_2,e_2)-f(x_2,e_1)\ge f(x_1,e_2)-f(x_1,e_1)$ whenever $x_1\le x_2$ and $e_1\preceq e_2$. The transition $p$ is monotone if $\int f\,dp(s,a,\cdot)$ is increasing in $(s,a)$ for every increasing $f$, and has stochastically increasing differences if $p(s,a,B)$ has increasing differences for every upper set $B$. A correspondence $\Gamma$ is ascending if $s_1\le s_2$, $b\in\Gamma(s_1)$, $b'\in\Gamma(s_2)$ imply $\min\{b,b'\}\in\Gamma(s_1)$ and $\max\{b,b'\}\in\Gamma(s_2)$. Assumption 1 asks that $r$ be increasing in $s$ with increasing differences in $(s,a)$, that $p$ be monotone with stochastically increasing differences, and that $\Gamma(s_1)\subseteq\Gamma(s_2)$ for $s_1\le s_2$.

Formalization targets

Goal: Theorem 3

Under Assumption 1 with $\Gamma$ ascending:

1. for $0<\beta_1\le\beta_2<1$,

$$g(s,\beta_2)\ge g(s,\beta_1)\ \ \forall s,\qquad \mathbb E^t_2(g(\beta_2))\ge\mathbb E^t_1(g(\beta_1))\ \ \forall t\in\mathbb N,\ \forall s(1);$$

2. for a payoff $r(s,a,c)$ with increasing differences in $(a,c)$ and in $(s,c)$ and $c_2\succeq c_1$,

$$g(s,c_2)\ge g(s,c_1)\ \ \forall s,\qquad \mathbb E^t_2(g(c_2))\ge\mathbb E^t_1(g(c_1))\ \ \forall t\in\mathbb N,\ \forall s(1).$$

Milestones

• Theorem 1: if $P_2$ is $D$-preserving and $P_2(s,\cdot)\succeq_D P_1(s,\cdot)$ for all $s$, then $\mu_2^t\succeq_D\mu_1^t$ for all $t$.
• Corollary 1: if $g_1\le g_2$, $g_2$ is increasing and $p$ is monotone, then $\mathbb E^t_2(g_2)\ge\mathbb E^t_1(g_1)$ for all $t$ and every initial state.
• Proposition 5: $h(\cdot,\cdot,f)$ has increasing differences for increasing $f$; with $\Gamma$ ascending, $G$ is ascending and $g$ increasing; $Tf$ and $V$ are increasing.
• Proposition 6: the maximum over an ascending $\Gamma$ of a function with pairwise increasing differences in $(s,a)$, $(s,e)$, $(a,e)$ has increasing differences in $(s,e)$.
• Proof of Theorem 3, p.21: $h(s,a,\beta,f)$ has increasing differences in $(a,\beta)$ and $(s,\beta)$.
• Proof of Theorem 3, pp.21–22: $V(s,\beta)$ has increasing differences in $(s,\beta)$ and is increasing in $s$.

Significance

The theorem gives sign predictions for the whole future path of decisions, not only for the current one: a more patient decision maker, or one whose payoff rewards higher actions more, invests, saves or prices higher now and in expectation in every later period. In aggregate models this is the comparative statics of the cross-sectional mean decision, which the applications of the paper (capital accumulation with adjustment costs, reference-price dynamic pricing, controlled random walks) use directly.

The result is proved in the paper; nothing here is open mathematics. The paper's proofs of Propositions 5 and 6 are citations, and the proof of part (ii) of Theorem 3 is omitted. As far as is known, none of these statements has a machine-checked proof. The platform has Topkis's finite-horizon monotonicity theorem and the argmax monotonicity theorem in published form; this mission adds the infinite-horizon fixed-point argument and the Markov-chain comparison.

Difficulty

The first idea, applying Topkis's monotonicity theorem to $h(s,a,\beta,V)$ in $(a,\beta)$, needs increasing differences of $V$ in $(s,\beta)$, and $V$ is only known as a fixed point. Increasing differences must be carried through every value iterate, which needs Proposition 6, and that needs $\Gamma$ ascending; Assumption 1(iii) alone does not suffice (Proposition 5(ii) as printed fails without it, see the milestone). The stochastic part has its own obstacle: the policy comparison $g_1\le g_2$ alone does not order the future state distributions, because the distributions are generated by different policies; the comparison needs $g_2$ increasing and $p$ monotone so that the transition under $g_2$ preserves increasing functions, and then an induction over periods with unbounded integrands.

Formalization scope

The state space is any measurable space with a partial order; the paper's Borel $S\subseteq\mathbb R^n$ with the componentwise order is an instance. Actions are reals in $A$, and $p$ is a Markov kernel on $S\times\mathbb R$; hypotheses on $p$ and $r$ are imposed for $a\in A$. The maximum in $T$ is sSup with its attainment assumed explicitly, since sSup of an unbounded set is $0$ in Lean. The standing assumptions of p.6 are hypotheses: $T^n0\to V$ uniformly, $V=TV$ with the maximum attained, attainment along the iterates, and measurability and integrability of the iterates and of $V$ (footnote 9). The policy $g$ is the greatest element of $G(s)$ and measurable, and the Lean period index starts at $0$. Integrals are Bochner integrals, so every integrand carries its integrability hypothesis; without them the comparison of expected decisions could hold for the trivial reason that both integrals are $0$. Proposition 5(ii) carries the added hypothesis "$\Gamma$ ascending".

Increasing differences and the induced set order are the published definitions Supermodularity.Monotonicity.IncreasingDifferencesOn and Supermodularity.Lattices.InducedSetOrder. A complete development needs the layer-cake formula for integrals of increasing functions against measures with stochastically increasing differences, integration against Measure.bind, monotone and dominated convergence for truncations of unbounded increasing functions, and uniform limits of functions with increasing differences. The chain comparison (Theorem 1) and Proposition 6 are reusable for other monotone dynamic programs. Proofs of any milestone, and alternative proofs of Theorem 3(ii), are welcome.

Selected references

• Bar Light, Stochastic Comparative Statics in Markov Decision Processes, arXiv:1904.05481v2, 2020; Mathematics of Operations Research 46(2), 2021. https://arxiv.org/abs/1904.05481
• Donald M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 1978. https://doi.org/10.1287/opre.26.2.305
• Donald M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998 (paperback 2011). https://doi.org/10.1515/9781400822539
• William S. Lovejoy, Ordered Solutions for Dynamic Programs, Mathematics of Operations Research 12(2), 1987. https://doi.org/10.1287/moor.12.2.269
• Hugo A. Hopenhayn and Edward C. Prescott, Stochastic Monotonicity and Stationary Distributions for Dynamic Economies, Econometrica 60(6), 1992. https://doi.org/10.2307/2951541
• Alfred Müller and Dietrich Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002, ISBN 978-0-471-49446-1.