All missions

Motivation

Many estimation problems in statistics, signal processing and machine learning ask for a low-rank positive semidefinite matrix: phase retrieval, matrix sensing, PCA-type problems and the Burer–Monteiro approach to semidefinite programs. A standard formulation is

$$\min_{X\in\mathbb S^{p\times p},\ X\succeq0,\ \operatorname{rank}(X)=r} f(X),\qquad 0<r\le p, \tag{1}$$

and Riemannian optimization solves it by treating the feasible set as a smooth manifold. Two geometries are in common use. In the embedded geometry the set of rank-$r$ PSD matrices is a submanifold of $\mathbb R^{p\times p}$ with the Euclidean metric. In the quotient geometry one writes $X=YY^\top$ with a full-column-rank factor $Y$ and optimizes over equivalence classes $[Y]=\{YO:O\text{ orthogonal}\}$. Algorithms built on the two geometries behave similarly in experiments, and landscape results (absence of spurious local minima, strict saddles) have been proved separately for each. Luo, Li and Zhang (arXiv:2110.12121, Mathematics of Operations Research 2024) explain this by an explicit dictionary between the Riemannian gradients and Hessians of the two geometries. This mission formalizes their first main result, Theorem 3, for the full-rank factorization of PSD matrices.

Setting

Matrices carry the Frobenius inner product $\langle A,B\rangle=\operatorname{tr}(A^\top B)$. The objective $f:\mathbb R^{p\times p}\to\mathbb R$ is twice continuously differentiable and symmetric, $f(X)=f(X^\top)$ (the paper's standing assumptions); $\nabla f$ and $\nabla^2f$ are its Euclidean gradient and Hessian.

Embedded geometry. $\mathcal M_{r+}=\{X\in\mathbb S^{p\times p}:X\succeq0,\ \operatorname{rank}X=r\}$, viewed as $\mathcal M^e_{r+}\subset\mathbb R^{p\times p}$. Its tangent space $T_X\mathcal M^e_{r+}$ is the span of the tangent cone. The Riemannian gradient $\operatorname{grad}f(X)$ is the orthogonal projection of $\nabla f(X)$ onto $T_X\mathcal M^e_{r+}$, and the Riemannian Hessian quadratic form $\operatorname{Hess}f(X)[\xi,\xi]$ is the derivative $\frac{d}{dt}\langle\operatorname{grad}f(c(t)),\xi\rangle$ at $t=0$ along any $C^1$ curve $c$ in $\mathcal M_{r+}$ with $c(0)=X$, $c'(0)=\xi$.

Quotient geometry. The total space is $\mathbb R_*^{p\times r}$, the $p\times r$ matrices of full column rank, with the objective $\bar h_{r+}(Y)=f(YY^\top)$ (18a). A weight $Y\mapsto W_Y$, smooth and symmetric positive definite, defines the metric $\bar g_Y(\eta,\theta)=\operatorname{tr}(W_Y\eta^\top\theta)$. The vertical space $\mathcal V_Y=\{Y\Omega:\Omega^\top=-\Omega\}$ is tangent to the orbit $[Y]$, and the horizontal space $\mathcal H_Y$ is its $\bar g_Y$-orthogonal complement. Tangent vectors of the quotient $\mathcal M^{q_1}_{r+}=\mathbb R_*^{p\times r}/\mathbb O_r$ are represented by horizontal vectors: $\overline{\operatorname{grad}h_{r+}([Y])}$ is the horizontal part of the total-space gradient $\nabla\bar h_{r+}(Y)W_Y^{-1}$, and $\overline{\operatorname{Hess}h_{r+}([Y])}[\theta,\theta]=\bar g_Y(\bar\nabla_\theta\operatorname{grad}\bar h,\theta)$ for horizontal $\theta$, where $\bar\nabla$ is the Levi-Civita connection of $\bar g$ (Koszul formula).

Comparison data. $\mathcal L^{r+}_Y(\theta)=Y\theta^\top+\theta Y^\top$; $U\in\mathrm{St}(r,p)$ spans the top $r$ eigenspace of $X=YY^\top$, $P=U^\top Y$, $Y^\dagger=(Y^\top Y)^{-1}Y^\top$. For a quadratic form on a $d$-dimensional space with inner product $g$, $\lambda_k$ is its $k$-th largest eigenvalue relative to $g$ ($1\le k\le d$). $\sigma_1,\sigma_r$ are the extreme singular values of an $r\times r$ matrix.

Formalization targets

Goal: Theorem 3 (p. 21)

If in addition $W_Y=OW_{YO}O^\top$ for all orthogonal $O$, then for every $Y\in\mathbb R_*^{p\times r}$ and $X=YY^\top$,

$$\operatorname{grad}f(X)=\Big(\overline{\operatorname{grad}h_{r+}([Y])}W_YY^\dagger+\big(\overline{\operatorname{grad}h_{r+}([Y])}W_YY^\dagger\big)^\top(I_p-YY^\dagger)\Big)/2,\qquad\overline{\operatorname{grad}h_{r+}([Y])}=2\operatorname{grad}f(X)YW_Y^{-1},$$

and if $[Y]$ is a Riemannian first-order stationary point of (18a),

$$\overline{\operatorname{Hess}h_{r+}([Y])}[\theta,\theta]=\operatorname{Hess}f(X)[\mathcal L^{r+}_Y(\theta),\mathcal L^{r+}_Y(\theta)]\quad\forall\theta\in\mathcal H_Y,$$

both Hessians have $d=pr-(r^2-r)/2$ eigenvalues, and $\lambda_i(\overline{\operatorname{Hess}h_{r+}([Y])})$ lies between $2\sigma_r(PW_Y^{-1}P^\top)\lambda_i(\operatorname{Hess}f(X))$ and $4\sigma_1(PW_Y^{-1}P^\top)\lambda_i(\operatorname{Hess}f(X))$.

Milestones

1. Lemma 6: $Y_1Y_1^\top=Y_2Y_2^\top$ iff $Y_2=Y_1O$; $U_1B_1U_1^\top=U_2B_2U_2^\top$ iff $U_2=U_1O$, $B_2=O^\top B_1O$; $\mathcal M_{r+}=\{YY^\top\}=\{UBU^\top\}$.
2. Lemma 3: $\mathcal M^e_{r+}$ is a smooth embedded submanifold of dimension $pr-r(r-1)/2$, with tangent space in the block form (14).
3. Lemma 4 (i): explicit $\mathcal V_Y$, $\mathcal H_Y$ and their dimensions.
4. Lemma 1 on $\mathbb R_*^{p\times r}$: the total-space gradient is already horizontal.
5. Proposition 1, embedded bullet: the formulas (19) for $\operatorname{grad}f$ and $\operatorname{Hess}f$.
6. Proposition 1, quotient bullet: the formulas (20) for the lifted gradient and Hessian.
7. Proposition 2: $\mathcal L^{r+}_Y$ is a bijection $\mathcal H_Y\to T_X\mathcal M^e_{r+}$.
8. Proposition 2, (23): $2\sigma_r(PW_Y^{-1}P^\top)\bar g_Y(\theta,\theta)\le\|\mathcal L^{r+}_Y\theta\|_F^2\le4\sigma_1(PW_Y^{-1}P^\top)\bar g_Y(\theta,\theta)$.
9. Theorem 2: the abstract sandwich inequality for spectra of two quadratic forms related by a bijection with bounded metric distortion.

Significance

Theorem 3 says that at stationary points the two geometries see the same second-order landscape: the Hessians are congruent through $\mathcal L^{r+}_Y$, so their eigenvalues have the same signs and comparable magnitudes, with explicit factors depending on $W_Y$ and the spectrum of $X$. The paper derives from it (Corollary 1) that first-order stationary points, second-order stationary points and strict saddles correspond between the embedded and quotient formulations, so a landscape result proved in one geometry transfers to the other. The choice of weight $W_Y$ (flat $I_r$, right-invariant $(Y^\top Y)^{-1}$, or $Y^\top Y$) changes the comparison constants, which is how the paper relates the conditioning of the two approaches.

The result is proved in the paper; it is not formalized anywhere. A formal development adds machine-checked Riemannian gradients and Hessians on a concrete embedded submanifold and on a concrete quotient, a checked horizontal-space computation, and a reusable abstract sandwich theorem for max–min eigenvalues. Corollary 1 and the parallel results for the polar factorization and for general rank-$r$ matrices (Theorems 4–7) are natural follow-up missions on the same definitions.

Difficulty

The identities (19), (20) and (34) are matrix calculus once the geometric objects are pinned down; the difficulty is that the definitions are intrinsic. The embedded Hessian requires differentiating the tangent projection $P_{T_X\mathcal M^e_{r+}}$ along the manifold, which produces the curvature term $2\langle\nabla f(X),U_\perp D\Sigma^{-1}D^\top U_\perp^\top\rangle$; the obvious computation that ignores the moving tangent space gives the wrong Hessian. The quotient Hessian involves the derivative of the weight $W_Y$ and needs the horizontal-space description of Lemma 4 to see that the projection in (5) can be dropped. Identifying $\operatorname{span}$ of the tangent cone with the block form (14) needs an explicit chart of the rank-$r$ PSD set. The final sandwich requires a max–min (Courant–Fischer) argument relative to two different inner products, and the order of the bounds flips for negative eigenvalues.

Formalization scope

• $\mathbb R^{a\times b}$ is EuclideanSpace ℝ (Fin a × Fin b) (Frobenius inner product) with matrix views toMat/ofMat. The weight $W$ takes values in $\mathbb R^{r\times r}$ in the same form so that $\mathrm DW_Y$ is defined.
• The embedded tangent space and Riemannian gradient are the published platform definitions ProjLikeRetr.Retractor.tangentSpace (span of the tangent cone) and ZORiem.RGD.rgrad (projected Euclidean gradient); "smooth embedded submanifold of dimension $d$" is the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold k d, for every $k$.
• The embedded Hessian is a curve-defined predicate on a quadratic form; the quotient Hessian is the Koszul-formula form $\bar g_Y(\mathrm DG[\theta],\theta)+\tfrac12\mathrm D\bar g(\theta,\theta)[G]$. Neither is defined by the paper's formulas (19), (20) or (34): those are theorems, and a formalization that defined the Hessians or gradients by them would make the mission trivial.
• $\lambda_k$ is the max–min value over $k$-dimensional subspaces (the paper's Lemma 13); "sandwiched between $a$ and $b$" means $\min(a,b)\le\mu\le\max(a,b)$; $\sigma_1,\sigma_r$ of the symmetric positive definite $PW_Y^{-1}P^\top$ are its extreme Rayleigh quotients.
• Conventions: $0<r\le p$; $f$ is $C^2$ and symmetric; $W_Y$ is positive definite on $\mathbb R_*^{p\times r}$ and $W$ is smooth there (the meaning of "Riemannian metric"); "$U$ spans the top $r$ eigenspace of $YY^\top$" is $U^\top U=I_r$, $UU^\top Y=Y$; $Y^\dagger=(Y^\top Y)^{-1}Y^\top$; $\mathcal L^{r+}_Y$ is defined as $Y\theta^\top+\theta Y^\top$ rather than by the block formula (22).
• In Theorem 2 the map $\mathcal L$ is assumed linear, as in every application in the paper, and the printed domain $\mathcal H_X$ in (12)–(13) is read as $\mathcal H_Z$.
• Not encoded: the half of Lemma 3 about general rank-$r$ matrices, Lemma 4 (ii) (no quotient-manifold structure in Mathlib), the polar factorization geometry and Theorems 4–7, Corollaries 1–2.

Useful contributions include Mathlib-level lemmas on the tangent cone of the rank-$r$ PSD set, Courant–Fischer for a form relative to a non-standard inner product, and matrix-calculus lemmas for $\mathrm D(W^{-1})$.

Selected references

• Y. Luo, X. Li, A. R. Zhang, On Geometric Connections of Embedded and Quotient Geometries in Riemannian Fixed-rank Matrix Optimization, Mathematics of Operations Research, 2024; arXiv:2110.12121v2. https://arxiv.org/abs/2110.12121
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244
• M. Journée, F. Bach, P.-A. Absil, R. Sepulchre, Low-rank optimization on the cone of positive semidefinite matrices, SIAM Journal on Optimization 20(5), 2010. https://doi.org/10.1137/080731359
• B. Vandereycken, S. Vandewalle, A Riemannian optimization approach for computing low-rank solutions of Lyapunov equations, SIAM J. Matrix Anal. Appl. 31(5), 2010. https://doi.org/10.1137/090764566
• R. Bhatia, Matrix Analysis, Springer GTM 169, 1997. https://doi.org/10.1007/978-1-4612-0653-8

Pricing under customer heterogeneity

A seller who offers $n$ products and sets one price vector for all customers must price for a heterogeneous population. The finite-mixture logit (FML) model describes such a population with a small number of segments. Each segment follows its own multinomial logit (MNL) demand, so this is the simplest heterogeneous extension of the MNL model. It is widely used in empirical demand estimation (Train, 2009). Pricing under it is harder than under a single MNL. The single-segment MNL revenue is not concave in prices (Hanson and Martin, 1996), but it becomes concave once it is written in market shares (Li and Huh, 2011). With two or more segments that change of variables fails, and the revenue can be multimodal (Li et al., 2019). Local search then gives no quality guarantee.

van de Geer and den Boer give an algorithm with a guarantee: for every $\varepsilon > 0$ it returns prices whose revenue is at least $(1-\varepsilon)$ times the optimum. This mission formalizes that guarantee, Theorem 1 of the paper (published in Management Science, doi:10.1287/mnsc.2021.4272).

Setting

There are $m \ge 1$ segments $c \in M$ with shares $w_c > 0$, $\sum_c w_c = 1$, and $n \ge 1$ products $j \in N$. Segment $c$ values product $j$ at $a_{cj} \in \mathbb R$. The price sensitivity $b_j > 0$ depends on the product but not on the segment. At prices $p \in \mathbb R^n$, a segment-$c$ customer buys product $i$, or nothing, with probability

$$q_{ci}(p) = \frac{e^{a_{ci} - b_i p_i}}{1 + \sum_{j} e^{a_{cj} - b_j p_j}}, \qquad q_{c0}(p) = \frac{1}{1 + \sum_{j} e^{a_{cj} - b_j p_j}},$$

and the expected revenue is $\Pi(p) = \sum_c w_c \sum_j p_j\, q_{cj}(p)$.

All maximizers of $\Pi$ lie in a box $[\underline p, \bar p]$, where $\underline p_j = b_j^{-1}$ and $\bar p_j$ adds to $b_j^{-1}$ the largest single-segment revenue. The no-purchase vector is $q_0(p) = (q_{10}(p), \dots, q_{m0}(p))$, and $X = \{q_0(p) : p \in [\underline p, \bar p]\}$ is the set of attainable no-purchase vectors. Fix $x \in X$ and substitute $z_j = e^{-b_j p_j}$. The best revenue among prices with $q_0(p) = x$ is then the value $\pi(x)$ of a concave program $\texttt{cnstr-rev}(x)$ with linear constraints $1 + \sum_j s_{cj} z_j = 1/x_c$, where $s_{cj} = e^{a_{cj}}$.

Algorithm 1, $\mathrm{BNB}(\varepsilon)$, searches the $m$-dimensional set $X$ by branch and bound over boxes $R(x, r)$ of sup-norm radius $r$ around centers $x$, clipped to $[q_0(\underline p), q_0(\bar p)]$. It keeps a lower bound $\underline\pi$, an upper bound $\bar\pi \in [-\infty, \infty]$, and an incumbent $x^\star$. In each pass and for each box that meets $X$, it solves a linear program $\mathrm{LP}(x, r)$. A map $\chi$ turns the solution into an attainable point $x^\delta$ in the box. The pass then evaluates $\pi(x^\delta)$, compares an upper bound $U(x^\delta, r^\delta)$ with $\underline\pi$, and keeps or discards the box. Kept boxes are split into $2^m$ boxes of half the radius. The loop runs while $(1-\varepsilon)\bar\pi > \underline\pi$.

Formalization targets

Goal: Theorem 1 (p. 19)

For every $\varepsilon > 0$, $\mathrm{BNB}(\varepsilon)$ terminates after finitely many passes, and every maximizer $z'$ of $\texttt{cnstr-rev}(x^\star)$ gives prices $p'_j = -\log(z'_j)/b_j$ with

$$\Pi(p') \ge (1 - \varepsilon) \max_{p \in \mathbb R^n} \Pi(p).$$

The goal is posed for every bounding rule $U$ with two properties, for some constant $K_0$ and all $x \in X$, $r > 0$:

$$\text{(U1)}\ \max_{\tilde x \in R(x,r) \cap X} \pi(\tilde x) \le U(x, r), \qquad \text{(U2)}\ U(x, r) \le \pi(x) + r K_0.$$

It is also posed for every choice of LP solution and every visiting order of the boxes.

Milestones

1. Proposition 1: a global maximizer of $\Pi$ exists, and all of them lie in $[\underline p, \bar p]$.
2. Lemma 1: for $x \in X$, the price problem under $q_0(p) = x$ is equivalent to the concave program $\texttt{cnstr-rev}(x)$.
3. Equation (5): $\max_{x \in X} \pi(x) = \max_{p \in [\underline p, \bar p]} \Pi(p)$.
4. Proposition 2: a $(1-\varepsilon)$-optimal $x' \in X$ yields $(1-\varepsilon)$-optimal prices.
5. Proposition 6: the derivative-free relaxation $\pi^\xi(x, r)$ bounds $\pi$ on $R(x, r) \cap X$.
6. Proposition 7: $R(x, r) \cap X \neq \emptyset$ if and only if $\mathrm{LP}(x, r)$ is feasible.
7. Corollary 1: the point $\chi$ built from an LP solution lies in $R(x, r) \cap X$, and equals $x$ when $x \in X$.

Significance

Theorem 1 is an approximation scheme for a non-concave revenue function. The search space has dimension $m$, the number of segments, rather than $n$, the number of products. The reduction behind it (Lemma 1, Equation (5) and Proposition 2) applies to any search over no-purchase probabilities, not only to branch and bound. Proposition 7 and Corollary 1 give an exact LP test for whether a box of no-purchase probabilities contains an attainable point.

The results are proved on paper. None of them has a machine-checked proof, and the platform has no FML model, no no-purchase reparameterization and no pricing branch and bound. A formal proof would also settle two printed defects found in planning. First, Proposition 4 (a Lipschitz bound used inside the paper's bounding rule $\pi^u$) is false as printed: it pairs a sup-norm gradient bound with a sup-norm displacement. Second, the printed constraints (15)–(16) of $\mathrm{LP}(x, r)$ make Proposition 7 false for centers outside $[q_0(\underline p), q_0(\bar p)]$, and Algorithm 1 creates such centers. The mission states the corrected versions.

Difficulty

The obvious argument is the one in the paper: boxes that may contain a maximizer are never discarded, and the gap between the bounds shrinks with the radius. Writing it out runs into two problems.

1. The paper's upper bound $\pi^u$ rests on Proposition 4, which is false. A valid rule needs a Lipschitz constant for $\pi$ on $X$. $\pi$ is the value of a parametric concave program whose feasible polytope moves with $x$, so bounding its variation requires quantitative stability of polyhedra, not just differentiation.
2. The inner loop over boxes is sequential. The lower bound $\underline\pi$ updated for one box is read when the next box is tested, so the covering invariant has to be carried through an ordered fold, for every visiting order.

Proposition 1 is the heaviest analytic milestone. It needs coercivity of $\Pi$ in every direction, including negative prices, and a first-order argument for the box.

Formalization scope

Segments and products are Fin m and Fin n, and vectors are functions on them. The norm on Fin m → ℝ is the sup norm, as on p. 17. The standing assumptions are $m, n \ge 1$, $w_c > 0$ with $\sum_c w_c = 1$ (the page writes $w_c \in (0,1)$), and $b_j > 0$. $\pi$, $\bar p$ and $\pi^\xi$ are real suprema, read only where their sets are nonempty and bounded. $\bar\pi$ is an extended real, so line 2 sets it to $+\infty$, line 6 to $-\infty$, and $(1-\varepsilon)\bar\pi$ follows extended-real arithmetic.

Algorithm 1 is a definition, not a hypothesis. One pass is a left fold over an enumeration of the finite set of centers. The run is an iterate of the pass, and the state after the first failed loop test is the output. The departures from the page are these:

• the bounding rule $\pi^u$ of (12) is replaced by any $U$ satisfying (U1)–(U2), because Proposition 4 fails;
• line 9's "a solution" is any minimizer of $\mathrm{LP}(x, r)$;
• $x^\star$, never initialised on the page, starts at $q_0(\underline p)$;
• constraints (15)–(16) are taken in the two-sided form $\mu_c(\bar x_c) \le \mu_c(x) - \delta^+_c + \delta^-_c \le \mu_c(\underline x_c)$ that the proof of Proposition 7 derives from them;
• Proposition 7 and Corollary 1 are stated for $x$ with positive entries, which is stronger than $(0,1)^m$.

The counterexample to Proposition 4 has $m = n = 2$: $a = ((0.07, -2.6), (-0.32, -0.3))$, $b = (1.6, 1.57)$, $w = (0.17, 0.83)$, and $r = 0.001$. The point $x + r(1, 1) \in R(x, r) \cap X$ then has $\pi = 0.2251959$, which exceeds $\pi(x) + r L(x, r) = 0.2251255$. Propositions 3, 4, 5 and 8, Theorem 2 (running time) and the competition extension of §5 are not posed.

(U1) and (U2) together say exactly that $\pi$ is $K_0$-Lipschitz on $X$, and $U(x, r) = \pi(x) + r K_0$ then satisfies both. The goal is therefore not vacuous. It cannot be trivialized either: it concerns the defined algorithm, with every line except the bounding rule kept, and its conclusion compares $\Pi(p')$ with a global maximum of $\Pi$ over all of $\mathbb R^n$.

A complete development needs elementary analysis of logit probabilities, concavity of $-y\log y$, compactness on boxes, finite LP attainment, and an invariant proof for an iterated fold. The no-purchase reparameterization (Lemma 1, Equation (5), Proposition 2) is reusable for other FML pricing results. Proofs of the milestones, a Lean proof that $\pi$ is Lipschitz on $X$ (which makes (U2) concrete), and a corrected Proposition 4 are all welcome.

Selected references

• R. van de Geer and A. V. den Boer, Price Optimization Under the Finite-Mixture Logit Model, Management Science, 2022; authors' version of August 26, 2021. https://doi.org/10.1287/mnsc.2021.4272, https://ssrn.com/abstract=3235432
• W. Hanson and K. Martin, Optimizing multinomial logit profit functions, Management Science 42(7):992–1003, 1996. https://doi.org/10.1287/mnsc.42.7.992
• H. Li and W. T. Huh, Pricing multiple products with the multinomial logit and nested logit models: Concavity and implications, Manufacturing & Service Operations Management 13(4):549–563, 2011. https://doi.org/10.1287/msom.1110.0344
• H. Li, S. Webster, N. Mason and K. Kempf, Product-line pricing under discrete mixed multinomial logit demand, Manufacturing & Service Operations Management 21(1):14–28, 2019. https://doi.org/10.1287/msom.2017.0675
• K. E. Train, Discrete Choice Methods with Simulation, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511805271

Motivation

Schools, universities and public employers that run affirmative action decide whom to admit from a set of applicants who are ranked by a priority ordering (exam scores, lottery numbers, seniority) and who belong to a minority or a majority group. The procedures used in practice, such as the reserve and quota systems of Boston, Chicago and New York school choice, or the reservation system of India's public sector, are choice rules: functions from the set of applicants, their types and their priorities to the set of admitted students. Market design needs these rules to be substitutable (a chosen student stays chosen when other applicants withdraw), because substitutability is the condition under which centralized clearinghouses produce stable matchings (Hatfield and Milgrom, 2005; Hatfield and Kojima, 2008).

B. Doğan and K. Yıldız, Choice with Affirmative Action (SSRN 3626941; Management Science, doi:10.1287/mnsc.2022.4447), ask which affirmative action rules are substitutable and also respond monotonically to the minority students they are meant to help. Their Theorem 1 says that such rules are exactly reserve rules whose reserve number changes by at most one in response to a type or priority change. This mission formalizes the direction of Theorem 1 that the paper proves correctly: every such rule is a bounded reserve rule.

Setting

Fix a nonempty finite set $\mathcal S$ of students and a capacity $q\ge3$. A problem $(S,\tau,\succ)$ is a set $S\subseteq\mathcal S$ of applicants, a type function $\tau$ ($\tau(s)=1$ minority, $\tau(s)=0$ majority) and a strict priority ordering $\succ$ on $S$. The rank of $s$ is one plus the number of students with higher priority. The top tier $T$ is the set of students of rank at most $q$, the students a pure priority rule would admit; the bottom tier is $B=S\setminus T$. Superscripts $m$ and $M$ select minority and majority students: $T^m$, $T^M$, $B^m$, $S^M$.

A choice rule $C$ picks a subset $C(S,\tau,\succ)\subseteq S$ of at most $q$ students. $C^m$ is the set of chosen minorities and $C^A=C^m\cap B$ the minorities chosen via affirmative action. The axioms are:

• capacity-filling: $|C(S,\tau,\succ)|=\min\{|S|,q\}$;
• neutrality: whether the $k$-th ranked student is chosen depends only on the sequence of types by rank;
• priority-compatibility: a chosen student may have lower priority than a rejected one only if the former is a minority and the latter a majority student.

An affirmative action rule satisfies these three. Substitutability requires $s\in C(S',\tau|_{S'},\succ|_{S'})$ whenever $s\in C(S,\tau,\succ)$ and $s\in S'\subseteq S$. MPI (monotonicity in priority improvements) requires that improving the priority of a chosen minority student does not reject any chosen minority student. MTC (monotonicity in type changes) requires that turning a chosen minority student into a majority student does not reject any other chosen minority student.

A reserve function $R$ gives each problem a number $R(S,\tau,\succ)\le|T^M|$ that depends only on the types of the students of ranks $1,\dots,q$. $C$ admits a reserve representation via $R$ if $C$ chooses all of $T^m$, then the $R$ highest-priority students of $B^m$ (all of them if fewer), then the highest-priority majority students until the seats are filled. The representation is bounded if $R$ satisfies Condition B: changing the type of a top-tier minority, improving a top-tier minority's rank, or worsening a top-tier majority's rank changes $R$ by $0$ or $+1$, and worsening the rank of a top-tier majority $M$ leaves $R$ unchanged when $M$ is among the $R$ lowest-ranked top-tier majorities.

Formalization targets

Goal: Theorem 1 (⇒), p. 10

$$C \text{ substitutable affirmative action rule},\ C\models\mathrm{MPI},\ C\models\mathrm{MTC}\ \Longrightarrow\ \exists R:\ R \text{ reserve function},\ R\models\mathrm{B1\text{–}B3},\ C=C^{R}.$$

Milestones

1. Lemma 1 (p. 20): for a substitutable affirmative action rule, two problems with the same students and types and coinciding top tiers have the same number of chosen minority students.
2. The reserve of the proof (p. 20): the function $R_C(S,\tau,\succ)$, the largest $|C^A|$ among problems with the same top-tier type configuration, is a reserve function, and $C$ is represented by it. No monotonicity axiom is needed.
3. Satisfies B1, B2, B3-i, B3-ii (pp. 20–22): under MPI and MTC, $R_C$ satisfies each part of Condition B.

Milestones 2 and 3 together give the goal, with $R=R_C$.

Significance

The result describes every substitutable, monotone affirmative action rule by one integer per top-tier type configuration, constrained by local bounds. A designer who wants substitutability, so that the rule can be plugged into a deferred-acceptance clearinghouse, and wants monotonicity in the minority students' favour, therefore only has to choose a reserve schedule. The paper's lexicographic and stepwise-adjusted–reserves rules (§5) are built on this description.

Formalizing it has a second purpose. Theorem 1 is printed as an equivalence, but its (⇐) half is false. Take $q=3$ and the reserve $R=1$ when the top tier has at most one minority, $R=0$ otherwise. This $R$ satisfies B1–B3. With priorities $a\succ b\succ c\succ d\succ e$ and minorities $d,e$, the rule chooses $\{a,b,d\}$ from $\{a,b,c,d,e\}$ but $\{a,d,e\}$ from $\{a,b,d,e\}$, so removing the rejected student $c$ rejects $b$, and substitutability fails. The same failure occurs in the paper's Example 1 ($q=100$), and the error sits in Case 3 of the (⇐) proof on p. 23. The mission therefore poses only the (⇒) half, which planning checked by exhaustive search for every capacity $q\le5$ and every universe of up to seven students. A machine-checked proof would settle that half for every $q$ and every universe. No formalization of this result, or of affirmative action choice rules in this model, exists on the platform or in Mathlib.

Difficulty

The reserve that represents $C$ has to be defined from $C$ alone. The obvious candidate, the number of affirmative-action admissions at the problem itself, is not a reserve function: it depends on how many minorities happen to sit in the bottom tier, while a reserve function may depend only on the top tier. Showing that a well-defined reserve exists already uses neutrality, substitutability and capacity-filling together (Lemma 1). The bounds of Condition B then compare reserves at problems whose top tiers differ. The monotonicity axioms give only the lower half of each bound, "the reserve does not fall"; the upper half, "the reserve rises by at most one", and the equality of B3 (ii) are not consequences of MPI or MTC and need substitutability. Small universes are a further obstacle: the paper's argument works with problems containing $q$ minority students and more than $2q$ students, which a small $\mathcal S$ does not contain, while the goal makes no assumption on $|\mathcal S|$.

Formalization scope

Everything lives in the namespace AffirmativeChoice.Reserve, in one definitions file and seven theorems.

• A Problem holds S : Finset 𝒮, τ : 𝒮 → Bool (true = minority) and pri : 𝒮 → ℕ with s ≻ s' ↔ pri s < pri s', injective on S. Only values on S matter; restriction keeps τ and pri.
• Ranks are 1-based; the top tier is rank ≤ q; the type of the k-th ranked student is an Option Bool, none beyond |S|.
• A ChoiceRule 𝒮 q carries only C P ⊆ P.S, |C P| ≤ q and nonemptiness for nonempty S; the axioms are separate predicates.
• The reserve procedure is a closed set formula, reserveChoice, with the majority cap $q-|T^m|-\min\{R,|B^m|\}$.
• B2 and B3 are read with the moving student in the top tier before the move, as the proof uses them. The printed typos on p. 6 ("$S\in\mathcal S$", "$\tau(s)=\tau'(s)$") are read as $S\subseteq\mathcal S$ and $\tau(s')=\tau'(s')$.
• The reserve of the proof is canonicalReserve, an sSup on ℕ over problems with the same top-tier type configuration. It agrees with the paper's $R(\rho)$ whenever the paper's witness problem exists.
• The goal assumes $q\ge3$ (the paper's standing assumption) and no lower bound on $|\mathcal S|$.

Ruled out: problems encoded as type words, which quotients away neutrality; reserve functions defined only on type words; axioms built into the choice-rule structure; an existential $R$ that is not required to be a reserve function; or a reserve procedure that may admit bottom-tier majority students. Each of these would make the goal different from, or weaker than, the paper's. The (⇐) half and the full equivalence are not stated in any item.

Contributions welcome: the finite-order combinatorics of ranks, tiers and improvements, which is reusable for other priority-based choice models (reserves, quotas, slot-specific priorities); proofs of the milestones in any order; and a formal proof of the counterexample to the (⇐) half.

Selected references

• B. Doğan and K. Yıldız, Choice with Affirmative Action, SSRN working paper 3626941, version of October 17, 2021; Management Science (2023). https://ssrn.com/abstract=3626941, https://doi.org/10.1287/mnsc.2022.4447
• J. W. Hatfield and P. Milgrom, Matching with Contracts, American Economic Review 95(4), 2005. https://doi.org/10.1257/0002828054825466
• J. W. Hatfield and F. Kojima, Matching with Contracts: Comment, American Economic Review 98(3), 2008. https://doi.org/10.1257/aer.98.3.1189
• H. Chernoff, Rational Selection of Decision Functions, Econometrica 22(4), 1954. https://doi.org/10.2307/1907363

Motivation

Sponsored-search platforms sell ad impressions through auctions in which advertisers submit both per-impression bids and a budget that caps their total spend. The platform then decides which auctions to run, subject to everybody's budget. Most auction theory treats budgets as exogenous constraints. In practice an advertiser chooses the budget, and committing capital has a cost, so budgets and bids are chosen together, strategically.

Ciocan and Iyer (SSRN 3240995; published in Operations Research, doi:10.1287/opre.2020.2052) study this joint choice. Exact equilibria of the resulting game are intractable: when budgets bind, the platform's allocation is the solution of a linear program, and an advertiser's best response depends on everybody else's budget in a complicated way. The paper shows that in large markets a simple, explicit strategy profile is an approximate equilibrium. This mission formalizes that result.

Setting

There are $m$ bidders $j \in [m]$ and $n$ items $i \in [n]$. Bidder $j$ has private valuations $V_{ij}$, all independent, with $V_{ij} \sim \mathrm{Exp}(\lambda_j)$. Committing a budget $B_j$ costs her $r_j B_j$, with $r_j \ge 0$. The platform earns an outside value $\delta > 0$ per unit of an unallocated item.

A strategy $\sigma_j$ maps $V_j = (V_{ij})_i$ to a budget $B_j(V_j) \ge 0$ and bids $b_j(V_j) = (b_{ij})_i$. Given bids $b$, the price of item $i$ to bidder $j$ is the next lower bid,

$$p^b(i,j) = \max_{k \ne j,\ b_{ik} \le b_{ij}} b_{ik} \quad (\text{and } 0 \text{ if } b_{ij} \text{ is the lowest bid}).$$

The platform picks an allocation $Y(B,b)$ that is optimal for the linear program

$$\max_{Y \ge 0}\ \sum_{i,j} p^b(i,j) Y_{ij} + \delta \sum_i \Big(1 - \sum_j Y_{ij}\Big) \quad \text{s.t.} \quad \sum_i p^b(i,j) Y_{ij} \le B_j,\ \ \sum_j Y_{ij} \le 1.$$

Bidder $j$'s spend is $\Psi_j = \sum_i p^b(i,j) Y_{ij}$, her payoff is $\pi_j = \sum_i (V_{ij} - p^b(i,j)) Y_{ij} - r_j B_j$, and her modified profit is $\tilde\pi_j = \pi_j + r_j(B_j - \Psi_j)$, the payoff she would get with a budget equal to her spend.

Write $\theta_j = \lambda_j(1+r_j) \in [\theta_{\min}, \theta_{\max}]$ and $\vartheta = \theta_{\max}/\theta_{\min}$, and assume $0 < \delta \le \log(4/3)/\theta_{\max}$. Let $W_{ij} = V_{ij}/(1+r_j)$, let $W^{(2)}_i$ be the second highest $W_{ik}$ on item $i$, and let $\bar\Psi_j = \sum_i W^{(2)}_i \mathbf 1\{j \text{ has the highest } W \text{ on } i\}$. The profile $\sigma^*$ has bidder $j$ bid $W_j$ with budget

$$B^*_j = \mathbb E_{-j}[\bar\Psi_j]\,\Big(1 + \frac{2\vartheta}{m^{1/\vartheta}}\Big),$$

where $\mathbb E_{-j}$ averages over the other bidders' valuations. A profile $\sigma$ is an $\epsilon$-equilibrium if no bidder can raise her expected payoff above $\mathbb E[\pi_j(\sigma)](1+\epsilon)$ by a unilateral deviation.

Formalization targets

Goal: Theorem 1 (p. 20)

There is a constant $C > 0$ such that if $m \ge \max\{(2\vartheta)^\vartheta, \exp(3\vartheta + 5\vartheta\log\vartheta + 1)\}$ and $n \ge 6\vartheta m^{2(\vartheta + 1/\vartheta)}\log(m)/C$, then for every bidder $j$ and every deviation $\sigma_j$,

$$\mathbb E\big[\pi_j(\sigma_j, \sigma^*_{-j})\big] \le \mathbb E\big[\pi_j(\sigma^*)\big]\Big(1 + \frac{11\vartheta^2 \log m}{m^{1/\vartheta}}\Big),$$

so $\sigma^*$ is an $\epsilon$-equilibrium with $\epsilon = 11\vartheta^2\log(m)/m^{1/\vartheta}$.

Milestones

The paper's own lemmas, in the order of its proof: the pathwise slack bound (Lemma 2), the dual-multiplier comparison (Lemma 4), greediness of the equilibrium allocation (Lemma 6), the key no-profitable-deviation lemma on a typical event (Lemma 3, corrected, see below), an order-statistic bound (Lemma 18), the probability of the typical event (Lemma 7), and the expected bounds on modified profit and spend (Lemmas 17, 15, 5, 16).

Significance

The theorem shows that a strategy which needs only each bidder's own distribution is an approximate equilibrium: shade each valuation by $1 + r_j$ and declare a budget slightly above the expected unbudgeted spend. The error vanishes as the number of bidders grows, and Theorem 2 of the paper adds that the platform's optimal allocation under $\sigma^*$ is then a per-item second-price auction with high probability. Together these justify analysing budgeted ad markets through a simple, decoupled model.

The result is proved in the paper but not machine-checked. Formalizing it means building an LP-based allocation model with measurable selections, order statistics of independent exponentials, and concentration bounds for sums over items. The formalization also records a correction: Lemma 3 as printed is false (see Formalization scope), and the corrected statement still yields Theorem 1.

Difficulty

The obvious route fails because a deviating bidder can change the allocation of every other bidder. If bidder $j$ overbids on an item that bidder $k$ would win, she raises $k$'s price, and $k$ can run out of budget and leave other items for $j$ to buy cheaply. Underbidding creates a similar effect. So the deviation's effect on the market is not small, and mean-field arguments do not apply. The budgets $B^*$ have to absorb these effects on a typical event, while the expected cost of the unspent budget, $r_j\,\mathbb E[B^*_j - \Psi_j]$, has to stay small next to the bidder's profit. Both requirements must hold uniformly over all deviations, including ones whose budget constraint binds, where the optimal allocation is not greedy.

Formalization scope

The model is one Lean structure Market (sizes, rates $\lambda_j$, $r_j$, the interval $[\theta_{\min}, \theta_{\max}]$, $\delta$) with the standing assumptions of p. 18 in Market.Standing. Valuations are a function Fin m → Fin n → ℝ with the product law of independent exponentials. The conventions are:

• Allocation rule. The platform uses a measurable map $(B,b) \mapsto Y(B,b)$ that returns an optimal solution of the LP for every nonnegative budget vector. Every theorem holds for every such selection.
• Strategies. Strategies are deterministic and measurable, with finite nonnegative budgets. A randomized deviation is a mixture of these.
• Budgets $B^*_j$. $B^*_j$ is an integral over the product law with bidder $j$'s coordinate fixed, so it is a canonical function, not a conditional expectation defined only almost everywhere.
• The constant $C$. $C$ is quantified before the market: it is universal.
• Pathwise lemmas. Lemmas 2, 4 and 6 are stated under the paper's no-ties convention (p. 14) and positive valuations; these hold almost surely.
• Lemma 3. Lemma 3 carries the added hypothesis $E_j(\sigma^*_j)$. The printed version, with only $E_j(\sigma_j)$, fails on an explicit instance ($m = 3$, $n = 2$) in which the deviation's modified profit is $2.7165$ against at most $0.4202$ under $\sigma^*$, for every optimal selection.

No allocation rule is fixed by fiat, and none may ignore budgets: the rule must be LP-optimal for all nonnegative budgets, and the sanity check exhibits a market satisfying the standing assumptions, so the goal is neither vacuous nor provable by choosing a convenient allocation.

A complete development needs measurable selections of LP optima, LP duality and complementary slackness (both available on the platform as general theorems), order statistics of independent exponential variables, and a Bernstein-type concentration bound (available as HighDimProb.Concentration.bernstein_unweighted). The order-statistic and concentration layers are reusable beyond this mission. Contributions of the appendix lemmas (Lemmas 9, 23–26) as intermediate results are welcome.

Selected references

• D. F. Ciocan and K. Iyer, Tractable Equilibria in Sponsored Search with Endogenous Budgets, SSRN working paper 3240995 (undated; the version cited throughout). https://ssrn.com/abstract=3240995
• D. F. Ciocan and K. Iyer, Tractable Equilibria in Sponsored Search with Endogenous Budgets, Operations Research (journal version; not the text used here). https://doi.org/10.1287/opre.2020.2052

Motivation

A retail store manager does two kinds of work that the firm cannot observe directly: operational effort, which keeps shelves stocked, and marketing effort, which draws customers. The firm sees only the outcomes, namely how much inventory was available and how much was sold. Sales are the smaller of inventory and demand, so whenever the shelf runs empty the true demand is hidden. This is demand censoring, and it links the two tasks: a sales figure equal to the inventory level says little about how hard the manager worked on marketing.

T. Dai, R. Ke and C. T. Ryan (SSRN 3235866; Management Science, doi:10.1287/mnsc.2020.3651) study the principal–agent problem this creates, with a risk-neutral, limited-liability manager whose pay lies between $0$ and a cap $\bar w$. With the bang-bang approach of their §4, they show that an optimal plan pays either nothing or the full bonus $\bar w$, according to whether a weighted likelihood-ratio statistic of the observed pair (inventory, sales) clears a trigger $t$. In the two-effort-level case, the bonus region has a distinctive mast-and-sail shape. Their §6 asks whether such a plan is monotone, meaning that more inventory or more sales never lowers the pay. A non-monotone plan invites ex post moral hazard: the manager would gain by discarding stock. The goal of this mission is the paper's answer, Proposition 5.

Setting

Inventory $I$ takes values in $[0,\bar I]$ and demand $Q$ in $[0,\bar Q]$, with $0<\bar I<\bar Q$. Under low and high operational effort, inventory has densities $f(\cdot\mid e^L_o)$ and $f(\cdot\mid e^H_o)$; under low and high marketing effort, demand has densities $g(\cdot\mid e^L_m)$ and $g(\cdot\mid e^H_m)$, with distribution function $G(\cdot\mid e_m)$. Inventory and demand are independent. Each density is continuous, strictly positive on its closed support, and integrates to $1$ there. The monotone likelihood ratio property (MLRP) holds: $f(i\mid e^L_o)/f(i\mid e^H_o)$ is nonincreasing in $i$, and $g(s\mid e^L_m)/g(s\mid e^H_m)$ is nonincreasing in $s$.

Sales are $S=\min\{I,Q\}$. A compensation plan $w(i,s)$ is defined on the domain $D=\{(i,s):0\le s\le i\le\bar I\}$. Points with $s<i$ are no-stockout (NSO) outcomes and points with $s=i$ are stockout (SO) outcomes. The firm wants both efforts high. For nonnegative weights $\omega_{e^H_o,e^L_m},\omega_{e^L_o,e^H_m},\omega_{e^L_o,e^L_m}$ summing to $1$, one for each deviation, define

$$\varphi^{NSO}(i,s)=\sum\omega_{e_o,e_m}\Big(1-\frac{f(i\mid e_o)\,g(s\mid e_m)}{f(i\mid e^H_o)\,g(s\mid e^H_m)}\Big),\qquad \varphi^{SO}(i)=\sum\omega_{e_o,e_m}\Big(1-\frac{f(i\mid e_o)\,(1-G(i\mid e_m))}{f(i\mid e^H_o)\,(1-G(i\mid e^H_m))}\Big).$$

The plan (11) pays $\bar w$ on the sail $B^{NSO}=\{(i,s)\in D:s<i,\ \varphi^{NSO}(i,s)\ge t\}$ and on the mast $B^{SO}=\{(i,i)\in D:\varphi^{SO}(i)\ge t\}$, and pays $0$ elsewhere. The critical inventories are $i_s$, the least $i$ with $\varphi^{NSO}(i,i)\ge t$, and $i_m$, the least $i$ with $\varphi^{SO}(i)\ge t$; each equals $\bar I$ when no such $i$ exists. The sail boundary $s^*(i)$ is the least $s$ with $\varphi^{NSO}(i,s)\ge t$.

A plan is monotone in $i$ (in $s$) if raising inventory (sales) within $D$ never lowers pay. It is jointly monotone if $w(i',s')\le w(i'',s'')$ whenever both points lie in $D$, $i'<i''$ and $s'<s''$.

Formalization targets

Goal: Proposition 5 (p. 16)

For every plan $w$ of the form (11) with $\bar w>0$:

$$\text{(i) } w \text{ is monotone in } s;\quad \text{(ii) } i_s=i_m\Rightarrow w \text{ is monotone in } i \text{ and jointly monotone};\quad \text{(iii) } i_s>i_m\Rightarrow w \text{ is neither}.$$

Milestones

• Lemma 1 (p. 12): the joint distribution function of $(I,S)$, $\Pr(I\le i,S\le s)=F(s)+G(s)[F(i)-F(s)]$ for $s<i$ and $F(i)$ for $s=i$.
• Lemma OA3 (p. oa4): the ratios $f_L/f_H$, $(1-G_L)/(1-G_H)$ and $g_L/g_H$ are nonincreasing, and nonconstant when the distributions differ.
• Survival versus density (proof of Proposition 3, p. oa6): $(1-G_L(i))/(1-G_H(i))\le g_L(i)/g_H(i)$, strictly under strict MLRP of $g$.
• Proposition 1 (p. 14): $B^{NSO}=\{(i,s):i\ge i_s,\ s^*(i)\le s<i\}$, with $s^*$ nonincreasing and continuous and $i_s\in(0,\bar I]$.
• Proposition 2 (p. 14): $B^{SO}=\{(i,i):i\ge i_m\}$ with $i_m\in(0,\bar I]$.
• Proposition 3 (p. 14): $i_s\ge i_m$.

By Proposition 3, part (ii) and part (iii) of the goal together cover every plan.

Significance

Proposition 5 shows that a mast-and-sail plan fails to be monotone in inventory exactly when the mast starts strictly below the sail. In that case a manager whose sales $s\in[i_m,i_s)$ fall just short of the inventory level would gain by discarding the unsold units. The outcome then becomes a stockout $(s,s)$ on the mast, which earns the bonus, instead of a no-stockout point below the sail, which earns nothing. This ex post moral hazard is the paper's motivation for studying the cost of imposing monotonicity in its later sections. Propositions 1–3 describe the optimal plan's bonus region completely, and Lemma OA3 records the stochastic-order facts the analysis rests on: MLRP implies a hazard-rate ordering of the demand distributions.

The results are proved in the paper and its online appendix. No machine-checked version of any of them is known. The mission states them under the standing assumptions made explicit, about canonical thresholds rather than existential witnesses, and for every plan of the form (11) rather than only optimal ones. Under this reading Propositions 3 and 5 are slightly stronger than printed. Two printed claims need an added hypothesis to be true, and the mission states these honestly: the continuity of $s^*$ in Proposition 1, and the strict survival-versus-density inequality.

Difficulty

The goal's statement is elementary, but every step depends on joint properties of the two ratio functions on the whole domain. These are monotonicity of $\varphi^{NSO}$ in both arguments, monotonicity of $\varphi^{SO}$, continuity, and the comparison $\varphi^{SO}(i)\ge\varphi^{NSO}(i,i)$. The last of these is a hazard-rate statement about integrated tails, not a pointwise MLRP fact. The thresholds are infima of level sets, so each part of the goal requires showing that the infimum is attained, and handling the empty cases (an empty sail, an empty mast) where the thresholds default to $\bar I$. Joint monotonicity is strict in both coordinates, so it does not follow from the product order on $\mathbb R^2$.

Formalization scope

All objects live in MastSail.Monotone. A model bundles $\bar I$, $\bar Q$ and the four densities as real functions, which are read only on $[0,\bar I]$ or $[0,\bar Q]$. Distribution functions are interval integrals from $0$. Pairs are ordered (inventory, sales). The standing assumptions add two things to the printed model: strict positivity of the densities on the closed supports (from §4, p. 9) and $\bar I<\bar Q$ (the paper has $\bar Q\ge\bar I$). These ensure that every ratio has a positive denominator, so no ratio defaults to division by zero. The paper's "$\min\{\cdot:\varphi=t\}$" is read as the least point with $\varphi\ge t$. The weights range over the three deviations from the target. Optimality of the plan is never assumed. Proposition 1 additionally takes strict MLRP of $g$ and $t>0$; Proposition 2 takes $0<t\le\varphi^{SO}(\bar I)$. The goal takes only $\bar w>0$.

The plan and the thresholds are the model's own definitions. A Proposition 5 stated for abstract regions shaped like a mast and a sail, or for thresholds supplied as hypotheses, would be set geometry and does not count. A complete development needs interval integrals, monotone level sets of continuous functions, and product measures with densities (for Lemma 1). The likelihood-ratio-to-hazard-rate comparison for densities on an interval can be reused well beyond this mission. Proofs of any milestone are welcome, as are proofs of the strict variants under weaker hypotheses.

Selected references

• T. Dai, R. Ke, C. T. Ryan, Incentive Design for Operations-Marketing Multitasking, Management Science, 2021; accepted version SSRN 3235866. https://ssrn.com/abstract=3235866, https://doi.org/10.1287/mnsc.2020.3651
• S. J. Grossman, O. D. Hart, An Analysis of the Principal-Agent Problem, Econometrica 51(1), 1983. https://doi.org/10.2307/1912246
• W. P. Rogerson, The First-Order Approach to Principal-Agent Problems, Econometrica 53(6), 1985. https://doi.org/10.2307/1911033
• A. Barvinok, A Course in Convexity, AMS Graduate Studies in Mathematics 54, 2002. https://doi.org/10.1090/gsm/054

Motivation

Many sequential decision problems in operations research are learned online while the environment changes: demand responds to prices differently from week to week, click-through rates drift, and the value of an action in a recommendation or auto-loan pricing system decays as conditions move. The stochastic linear bandit is the standard model for such problems when actions are described by feature vectors. The classical algorithms for it (OFUL of Abbasi-Yadkori, Pál and Szepesvári, 2011) assume the unknown parameter is fixed, and they can incur linear regret when it drifts.

Besbes, Gur and Zeevi (2014, 2015) introduced the variation budget $B_T$, a bound on the total movement of the environment over the horizon, and showed that the right benchmark is then the dynamic regret: the loss against the sequence of per-round optimal actions. Cheung, Simchi-Levi and Zhu, Hedging the Drift: Learning to Optimize under Non-Stationarity (arXiv:1903.01461v4, 2021; Management Science, doi:10.1287/mnsc.2021.4024), study the drifting linear bandit. Their SW-UCB algorithm attains the minimax rate when $B_T$ is known. Their Bandit-over-Bandit (BOB) algorithm needs no knowledge of $B_T$: it hedges over window sizes with an adversarial bandit learner. This mission formalizes BOB's dynamic regret bound, Theorem 4 of the paper, together with the chain of results that leads to it.

Setting

A drifting linear bandit instance consists of a horizon $T$, finite nonempty decision sets $D_t\subseteq\mathbb R^d$, and unknown parameters $\theta_t\in\mathbb R^d$ for $t=1,\dots,T$, all fixed in advance. In round $t$ the learner picks $X_t\in D_t$ and observes $Y_t=\langle X_t,\theta_t\rangle+\eta_t$. The noises $\eta_t$ are i.i.d., centred and $R$-sub-Gaussian: $\mathbb E[e^{s\eta_t}]\le e^{s^2R^2/2}$. The constants $L,S$ bound $\|X\|_2\le L$ and $\|\theta_t\|_2\le S$, and $|\langle X,\theta_t\rangle|\le1$. Assumption 1 asks that every action be a multiple of one vector of a fixed orthonormal basis. The variation constraint is

$$\sum_{t=1}^{T-1}\|\theta_{t+1}-\theta_t\|_2\le B_T ,$$

and the dynamic regret of a policy is $\mathcal R_T=\mathbb E\big[\sum_{t=1}^T\langle x_t^*-X_t,\theta_t\rangle\big]$ with $x_t^*\in\arg\max_{x\in D_t}\langle x,\theta_t\rangle$.

SW-UCB with window size $w$ and regularisation $\lambda>0$ estimates $\theta_t$ by ridge regression on the last $w$ rounds only:

$$V_{t-1}=\lambda I+\sum_{s=1\vee(t-w)}^{t-1}X_sX_s^\top,\qquad \hat\theta_t=V_{t-1}^{-1}\sum_{s=1\vee(t-w)}^{t-1}X_sY_s ,$$

and plays $\arg\max_{x\in D_t}\{x^\top\hat\theta_t+\beta\|x\|_{V_{t-1}^{-1}}\}$ with $\beta=R\sqrt{d\ln((1+wL^2/\lambda)/\delta)}+\sqrt\lambda S$.

BOB cuts the horizon into blocks of $H=\lfloor dT^{1/2}\rfloor$ rounds. Before each block an EXP3 learner draws an index $j\in\{0,\dots,\Delta\}$, $\Delta=\lceil\ln H\rceil$, and BOB restarts SW-UCB with window $\lfloor H^{j/\Delta}\rfloor$. The block's total reward, divided by $Q=2H+4R\sqrt{H\ln(T/\sqrt H)}$ and shifted by $\tfrac12$, is EXP3's feedback.

Formalization targets

Goal: Theorem 4

$$\mathcal R_T(\text{BOB})=\widetilde O\big(d^{2/3}B_T^{1/3}T^{2/3}+d^{1/2}T^{3/4}\big),$$

read as: for fixed $R,L,S,\lambda$ there are $C,k$ such that the expected regret is at most $C(1+\ln(dT))^k$ times the bracket, for every $d$, $T$, $B_T$, instance and noise.

Milestones

1. Lemma 3 (drift term of the estimator bounded by the window's variation, under Assumption 1).
2. Lemma 4 (sliding-window self-normalized bound).
3. Theorem 2 (confidence bound $|x^\top(\hat\theta_t-\theta_t)|\le L\sum\|\theta_s-\theta_{s+1}\|_2+\beta\|x\|_{V_{t-1}^{-1}}$).
4. Lemma 5 (sliding-window potentials dominated by restarted ones).
5. Theorem 3 ($\mathcal R_T(\text{SW-UCB})=\widetilde O(wB_T+dT/\sqrt w)$).
6. Lemma 1 (block rewards bounded by $H\nu+2R\sqrt{H\ln(T/\sqrt H)}$ with probability $\ge1-2/T$).
7. Proposition 1 ($\mathcal R_T(\text{BOB})=\widetilde O(w^\dagger B_T+dT/\sqrt{w^\dagger}+Q\sqrt{|J|T/H})$).

Significance

Theorem 4 shows that a learner ignorant of how fast the environment drifts can still be no-regret against the moving optimum. When $B_T\ge d^{-1/2}T^{1/4}$ it matches, up to logarithmic factors, the $d^{2/3}B_T^{1/3}T^{2/3}$ rate of SW-UCB tuned with knowledge of $B_T$, which matches the paper's minimax lower bound (Theorem 1) up to logarithmic factors. The bandit-over-bandit template, in which an adversarial bandit chooses among configurations of a base algorithm run on restarted blocks, is applied in the same paper to generalized linear and combinatorial semi-bandits, and by the same authors to non-stationary reinforcement learning.

The result is proved in the paper; nothing in this chain is machine-checked. The platform has an Exp3 regret bound and an elliptical-potential lemma, but no non-stationary bandit, no sliding-window estimator and no bandit-over-bandit result. A complete development would give a checked proof of the decomposition, of the per-block reduction to SW-UCB, and of the interaction between EXP3 and the high-probability normalisation, which the printed proof treats briefly.

Difficulty

The obvious argument for SW-UCB is to copy OFUL's analysis. It fails at the elliptical-potential step, because the sliding-window Gram matrices are not monotone in $t$ (old observations leave the window). Lemma 5 replaces it, and the drift bias of the estimator (Lemma 3) needs Assumption 1. Lemma 3 is false for actions in general position.

For BOB, the obvious idea is to treat each window size as an expert with bounded rewards. Block rewards are not bounded, though: they carry sub-Gaussian noise, and the normalised reward lies in $[0,1]$ only on a high-probability event (Lemma 1). EXP3's guarantee must be combined with that event. The restarts are also essential: without them a block's reward would depend on earlier EXP3 choices, and EXP3's adversary would no longer be oblivious.

Formalization scope

• Vectors and rounds. Vectors are Fin d → ℝ, matrices are Matrix (Fin d) (Fin d) ℝ, and rounds are numbered $1,\dots,T$. The window of round $t$ for a run started at round $t_0$ is $[\max(t_0,t-w),t-1]$.
• Decision sets and argmax. Decision sets are finite and nonempty. Ties in every argmax are broken by the first maximiser in a fixed enumeration of $D_t$.
• Noise and policies. The noise is a sequence of measurable, mutually independent, identically distributed, centred, $R$-sub-Gaussian random variables. Non-anticipatory policies are measurable functions of past noise.
• EXP3's randomisation. It is a finite mixture over choice sequences, weighted by $\prod_i p_{j_i,i}$.
• SW-UCB's inputs. SW-UCB uses $\lambda$ with $\lambda S^2\ge1$ and $\delta=1/T$, the choices of the paper's Appendix C.
• The budget. $B_T$ is any upper bound on the variation; the asymptotic regime $B_T=\Theta(T^\rho)$ is not imposed.
• Added hypotheses. Lemma 4 and Theorem 2 add $d\ge2$ and $\delta>0$: the printed radius is too small at $d=1$. Theorem 3 adds $w\le T$, without which its bound fails. Lemma 1 adds $1\le H\le T$.
• Ruling out trivial readings. The constants of every $\widetilde O$ are fixed before $d$, $T$, $B_T$ and the instance, since otherwise $C=2T$ would trivialise every regret bound. Every expected-regret conclusion also asserts integrability, so a non-integrable regret (whose integral Lean sets to $0$) cannot satisfy it vacuously.

A complete development needs:

• sub-Gaussian concentration for martingale sums with a self-normalized bound (method of mixtures);
• matrix monotonicity of inverses of positive-definite Gram matrices;
• the EXP3 regret bound of Auer et al. (2002) with uniform mixing;
• measurability of the algorithms' trajectories.

The self-normalized bound, matrix-inverse monotonicity and the EXP3 bound are reusable well beyond this mission. Contributions to any milestone, and to these general lemmas, are welcome.

Selected references

• W. C. Cheung, D. Simchi-Levi, R. Zhu, Hedging the Drift: Learning to Optimize under Non-Stationarity, arXiv:1903.01461v4, 2021; Management Science 68(3), 2022. https://arxiv.org/abs/1903.01461
• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• O. Besbes, Y. Gur, A. Zeevi, Stochastic Multi-Armed-Bandit Problem with Non-stationary Rewards, NeurIPS 2014. https://arxiv.org/abs/1405.3316
• O. Besbes, Y. Gur, A. Zeevi, Non-stationary Stochastic Optimization, Operations Research 63(5), 2015. https://doi.org/10.1287/opre.2015.1408