Operations Research

Bandit Algorithms Statistics·Captain: mikedeng1

Dynamic Assortment Personalization in High Dimensions 1: The Nuclear-Norm Explore-Then-Exploit Policy Has Regret at Most ((Cr(m+n)+3) log T + 1)ωResearch Paper

Motivation

An online retailer that serves many kinds of customers must decide, for each arriving customer, which handful of products to display. Showing too many items is impossible (screen space, shelf space), and which items sell depends on who is looking. The retailer does not know the customers' preferences in advance and learns them only from the choices customers make among the items shown. This is dynamic assortment personalization: an online learning problem in which every display both earns revenue and produces data.

Kallus and Udell (arXiv:1610.05604) study the regime in which the number of customer types $m$ and the number of items $n$ are both large, so that learning each type's preferences separately would take on the order of $mn$ interactions. Their premise is that preferences across types are governed by a few latent features, which makes the matrix of preference parameters approximately low rank. The non-contextual problem — one customer type, multinomial-logit choice — was studied by Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013); the paper extends it to many types and proposes an explore-then-exploit policy whose estimates come from nuclear-norm regularized maximum likelihood, the standard convex surrogate for low rank used in matrix completion.

Setting

There are $m$ customer types and $n$ items. Each type $i$ has a revenue vector $W_i\in\mathbb R^n$ (row $i$ of $W\in\mathbb R^{m\times n}$ ; $W_{ij}$ is the expected revenue when type $i$ buys item $j$ ) and a preference vector $\Theta^\star_i$ (row $i$ of the unknown matrix $\Theta^\star\in\mathbb R^{m\times n}$ ). Types arrive independently from an unknown distribution $\mu^\star$ in the simplex $\Delta^m$ .

For an assortment $S\subseteq\{1,\dots,n\}$ and a parameter vector $\theta\in\mathbb R^n$ , the multinomial-logit (MNL) choice probability of item $j\in S$ is

p_j(S;\theta)=\frac{e^{\theta_j}}{1+\sum_{j'\in S}e^{\theta_{j'}}},

and the customer buys nothing with probability $1/(1+\sum_{j'\in S}e^{\theta_{j'}})$ . The expected revenue of $S$ is $F(S;w,\theta)=\sum_{j\in S}p_j(S;\theta)w_j$ , and $S^\star(w,\theta;K)$ is the set of maximizers of $F(\cdot;w,\theta)$ over $|S|\le K$ . The revenue gap $\delta(w,\theta;K)$ is the optimal revenue minus the best revenue of a non-optimal assortment.

In round $t=1,2,\dots$ a customer of type $i_t\sim\mu^\star$ arrives, the retailer offers $S_t$ with $|S_t|\le K$ , and the customer chooses $j_t$ from the MNL law with parameters $\Theta^\star_{i_t}$ . The regret (Definition 1) of a policy after $T$ rounds is the expected revenue of the $\Theta^\star$ -greedy policy, which always offers an element of $S^\star(W_{i_t},\Theta^\star_{i_t};K)$ , minus the expected revenue of the policy.

Algorithm 2, $\pi_{\text{nuc-norm}}(C,\lambda)$ , keeps a sample $\mathcal O$ of exploration observations. At round $t$ , if $|\mathcal O|\le Cr(m+n)\log t$ it explores: it offers a uniformly random subset of size exactly $K$ and records $(i_t,j_t,S_t)$ . Otherwise it exploits: it offers an element of $S^\star(W_{i_t},\widehat\Theta_{i_t};K)$ , where $\widehat\Theta$ is a solution of

\min_{\Theta}\ L(\Theta)+\lambda\|\Theta\|_*\quad\text{s.t.}\quad\|\Theta\|_\infty\le\alpha/\sqrt{mn},\tag{5}

with $L$ the average negative log-likelihood (4) of the sample, $\|\cdot\|_*$ the nuclear norm and $\|\Theta\|_\infty$ the largest absolute entry.

Formalization targets

Goal: Theorem 6

Let $r\ge\operatorname{rank}\Theta^\star$ , $1/\rho\le m\mu^\star_i\le\rho$ for all $i$ , $\|\Theta^\star\|_\infty\le\alpha/\sqrt{mn}$ , $\min_i\delta(W_i,\Theta^\star_i;K)\ge\delta>0$ and $0\le W$ , $\max_{ij}|W_{ij}|\le\omega$ . With

C=\frac{4194304\,K^6\rho^3\omega^2\alpha^2e^{16\alpha}}{\delta^2},\qquad\lambda=8\sqrt{\frac{\rho K}{Crmn}},\tag{12}

for every selection of $\widehat\Theta$ from the solutions of (5) and of the exploited assortment,

\mathrm{Regret}(T;\pi_{\text{nuc-norm}}(C,\lambda))\le\big((Cr(m+n)+3)\log T+1\big)\,\omega\qquad\text{for }1\le T\le(m+n)^{mn/(Cr(m+n))}.

Milestones

From the printed proof of Theorem 6 (pp. 47–48): the Lipschitz bound $|p_j(S;\theta)-p_j(S;\theta')|\le\frac14\sqrt{|S|}\|\theta-\theta'\|_2$ ; the revenue bound $|F(S;w,\theta)-F(S;w,\theta')|\le\frac14\|w\|_\infty K^{3/2}\|\theta-\theta'\|_2$ ; the comparison $F(S';w,\theta)\ge F(S;w,\theta)-\frac12\|w\|_\infty K^{3/2}\|\theta-\theta'\|_2$ of optimal sets; the stability of the optimal set; and the count of exploration rounds. From the deterministic part of the recovery analysis (Sec. 8): Lemma 2 (a quadratic lower bound on the Bregman divergence of $L$ ), Lemma 5 (an upper bound from the regularized objective) and Lemma 6 (the nuclear-norm error is controlled by $\sqrt r$ times the Frobenius error and the spectral tail of $\Theta^\star$ ).

Significance

Theorem 6 is the paper's guarantee that a policy exploiting low-rank structure pays regret of order $r(m+n)\log T$ rather than the order $mn\log T$ that the paper shows (Theorem 5) for policies treating each type separately. The intermediate results are reusable: the Lipschitz bounds for MNL choice probabilities and revenue apply to any MNL assortment policy that plugs in estimated parameters, and Lemmas 2, 5 and 6 are the deterministic core of nuclear-norm regularized estimation for a likelihood that is not an entrywise loss.

To the best of current knowledge none of these results has a machine-checked proof. The mission produces a formal model of a contextual MNL assortment process with an adaptive policy, its trajectory law and regret, together with formal statements and proofs of the Lipschitz and stability facts that any explore-then-exploit analysis of MNL assortment needs. Several printed statements needed correction (see Formalization scope); machine-checked proofs settle the corrected forms.

Difficulty

The goal is a statement about the law of a $T$ -round adaptive process: the offered set at round $t$ depends on the whole past through the exploration test and through an estimate defined only as some minimizer of (5). Any argument must handle this dependence exactly, for every admissible selection of minimizer and of optimal assortment, rather than for one convenient choice.

The constants are explicit and the horizon is restricted, so the inequality has to hold with the paper's normalization exactly as stated, including the box constraint of (5). The printed proof routes through the paper's high-probability recovery bound (Theorem 3), which is believed false as printed and is not part of this mission, so a proof cannot simply cite it. Lemmas 5 and 6 require Hölder's inequality for the spectral/nuclear pairing and a decomposition of the error relative to the singular subspaces of $\Theta^\star$ ; Lemma 2 requires a curvature estimate for the log-sum-exp function uniformly on the box.

Formalization scope

The source is the arXiv preprint arXiv:1610.05604, an unstamped PDF pinned by sha256 2b010481…216a; its printed page numbers equal the PDF page numbers.

Types and items are Fin m and Fin n, 0-based; the no-purchase option is none. Matrices are MatrixCompletion.RealMatrix m n; the nuclear, spectral and Frobenius norms, the Frobenius inner product and $\|\cdot\|_\infty$ are the published MatrixCompletion definitions, and $F$ is the published ChoiceCDLP.MNL.mnlObjective with weights $e^{\theta_j}$ and no-purchase weight $1$ . All probabilities and expectations are finite sums over histories in Fin T → Fin m × Finset (Fin n) × Option (Fin n). Regret is Definition 1 after the tower property: the greedy policy earns $\sum_i\mu^\star_i\max_{|S|\le K}F(S;W_i,\Theta^\star_i)$ per round and Algorithm 2 earns $F(S_t;W_{i_t},\Theta^\star_{i_t})$ in expectation. The gap condition $\delta(w,\theta;K)\ge d$ is stated as "every non-optimal assortment of size at most $K$ earns at most the optimum minus $d$ ", since $\delta$ itself is undefined when every assortment is optimal.

Added hypotheses and corrections, each disclosed in the item's note:

Theorem 6 assumes $W\ge0$ , $\delta>0$ , $1\le K\le n$ , $m,n\ge1$ and $T\ge1$ . The horizon is read as $T\le(m+n)^{mn/(Cr(m+n))}$ (the page sets $r$ beside the fraction in the exponent); for $r\ge1$ this is the smaller range. If $r=0$ , Lean's division by zero gives $\lambda=0$ and horizon $T\le1$ .
The stability of the optimal set (p. 47) is false as printed (an equality of optimal sets) and is stated as the inclusion $S^\star(w,\theta';K)\subseteq S^\star(w,\theta;K)$ under the page's (non-strict) closeness hypothesis, multiplied out.
The exploration count (p. 48) is stated as $Cr(m+n)\log T+1$ , the form the next display uses, instead of the printed $C\log T+1$ .
Lemma 2 is false as printed and carries an extra factor $\frac12$ ; it assumes $\Theta^\star$ and $\Theta^\star+\Delta$ both feasible for (5).
Lemmas 5 and 6 carry the standing assumptions of Sec. 8: $\widehat\Theta$ solves (5), $\Theta^\star$ is feasible, $\lambda>0$ .

Theorem 3 (static recovery) and Lemma 4 (gradient concentration) are not posed: both are believed false as printed. Lemmas 3 and 7 are not posed either.

A trivializing formalization is ruled out: the estimator is any minimizer of (5) with its box constraint, the exploited set is any optimal assortment for the estimate, and both are quantified universally; exploration draws uniformly from subsets of size exactly $K$ ; and the benchmark is the $\Theta^\star$ -greedy policy under the same arrival law. Fixing the estimator to $\Theta^\star$ , dropping the box, or comparing to the best fixed assortment would change the theorem.

Contributions welcome: proofs of the milestones (the Lipschitz lemmas are calculus on the softmax function; Lemmas 5 and 6 are matrix analysis reusable for other nuclear-norm estimators), a proof that the definition of $\nabla L$ is the gradient of $L$ , and a proof that the history weights form a probability distribution.

Selected references

N. Kallus, M. Udell, Dynamic Assortment Personalization in High Dimensions, arXiv preprint, 2016–2017; Operations Research 68(4), 2020. https://arxiv.org/abs/1610.05604
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
D. Sauré, A. Zeevi, Optimal dynamic assortment planning with demand learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.1120.0412
B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://doi.org/10.1137/070697835

15 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Distributionally Robust Convex Optimization IV: An Absolute Mean Spread Bound Describes Exactly the z̃-Marginals of a Lifted Ambiguity SetResearch Paper

Motivation

Distributionally robust optimization handles an uncertain parameter $\tilde z\in\mathbb R^P$ whose distribution is only partly known. A decision must satisfy an expectation constraint for every distribution in an ambiguity set, the set of distributions consistent with the available information. Wiesemann, Kuhn and Sim (Optimization Online preprint 3757, 2013; Operations Research 62(6), 2014, doi:10.1287/opre.2014.1314) introduce a standardized ambiguity set. Its members are joint distributions of $\tilde z$ and auxiliary random vectors $\tilde u$ , constrained by expectation conditions and by probability bounds on conic confidence sets. Worst-case expectation constraints over such a set have tractable conic reformulations. The practical question is which kinds of distributional information this format can express. A set over $(\tilde z,\tilde u)$ describes information about $\tilde z$ through its $\tilde z$ -marginals, so the precise claim is that some set of distributions of $\tilde z$ equals the projection of a standardized set.

Section 3 of the paper settles this question for several common descriptors of dispersion. One of them is the absolute mean spread, the gap between the mean of a random variable above a threshold and its mean below it. Levi, Perakis and Uichanco used it to describe demand uncertainty in data-driven newsvendor models (Oper. Res. 63(6), 2015). The paper notes that, unlike variance or coefficient-of-variation bounds, spread information "can no longer be constructed via straightforward application of Theorem 5", its general lifting result for conic-representable moment bounds. Proposition 2 provides a dedicated lifting instead.

Setting

Fix $f\in\mathbb R^P$ , a threshold $\theta\in\mathbb R$ , a spread budget $\sigma\ge0$ and a probability level $\rho\in(0,1)$ . For a probability distribution $\mathbb Q$ on $\mathbb R^P$ under which $f^\top\tilde z$ has a finite mean, write

\mathbb E_{\mathbb Q}[f^\top\tilde z\mid A]=\frac{\mathbb E_{\mathbb Q}[f^\top\tilde z\,\mathbf 1_A]}{\mathbb Q[A]},\qquad A\in\{f^\top\tilde z\ge\theta\},\ \{f^\top\tilde z<\theta\}.

The absolute mean spread of $f^\top\tilde z$ at $\theta$ is $\mathbb E_{\mathbb Q}[f^\top\tilde z\mid f^\top\tilde z\ge\theta]-\mathbb E_{\mathbb Q}[f^\top\tilde z\mid f^\top\tilde z<\theta]$ . The target set (spreadSet) consists of the $\mathbb Q$ with $\mathbb Q[f^\top\tilde z\ge\theta]=\rho$ whose spread is at most $\sigma$ .

The lifted ambiguity set $\mathcal P$ (liftedSpreadSet) consists of the probability distributions $\mathbb P$ of $(\tilde z,\tilde u,\tilde v,\tilde w)$ on $\mathbb R^P\times\mathbb R^3$ with $\mathbb E_{\mathbb P}[\tilde w]=\sigma$ and $\mathbb P[f^\top\tilde z\ge\theta]=\rho$ , satisfying almost surely

f^\top\tilde z=\theta+\tilde u-\tilde v,\qquad \tilde w\ge\rho^{-1}\tilde u+(1-\rho)^{-1}\tilde v,\qquad \tilde u,\tilde v\ge0 .

The marginal $\Pi_{\tilde z}\mathbb P$ is the law of $\tilde z$ under $\mathbb P$ , and $\Pi_{\tilde z}\mathcal P=\{\Pi_{\tilde z}\mathbb P:\mathbb P\in\mathcal P\}$ .

For the companion result, the Huber loss (8) is $H_\delta(z)=\tfrac12z^2$ if $|z|\le\delta$ and $\delta(|z|-\tfrac12\delta)$ otherwise, for $\delta>0$ .

Formalization targets

Goal: Proposition 2 (Absolute Mean Spread), pp. 17–18

\Pi_{\tilde z}\mathcal P=\Big\{\mathbb Q\in\mathcal P_0(\mathbb R^P):\ \mathbb E_{\mathbb Q}[f^\top\tilde z\mid f^\top\tilde z\ge\theta]-\mathbb E_{\mathbb Q}[f^\top\tilde z\mid f^\top\tilde z<\theta]\le\sigma,\ \mathbb Q[f^\top\tilde z\ge\theta]=\rho\Big\}.

The page states the conclusion as $\mathbb Q^0\in\Pi_{\tilde z}\mathcal P=\{\dots\}$ for a given $\mathbb Q^0$ in the right-hand set. The set identity is the content, and it is the goal.

Milestones

The milestones follow the two inclusions of the proof (pp. 40–41).

For every $\mathbb P\in\mathcal P$ :

\mathbb E_{\mathbb P}[f^\top\tilde z\mid f^\top\tilde z\ge\theta]\le\rho^{-1}\mathbb E_{\mathbb P}[\tilde u]+\theta,\qquad \mathbb E_{\mathbb P}[f^\top\tilde z\mid f^\top\tilde z<\theta]\ge(1-\rho)^{-1}\mathbb E_{\mathbb P}[-\tilde v]+\theta.

Combining them gives

\text{spread}\le\rho^{-1}\mathbb E_{\mathbb P}[\tilde u]+(1-\rho)^{-1}\mathbb E_{\mathbb P}[\tilde v]\le\mathbb E_{\mathbb P}[\tilde w]=\sigma,

and hence $\Pi_{\tilde z}\mathcal P$ is contained in the target set. 2. For $\mathbb Q$ in the target set, $\tilde u=[f^\top\tilde z-\theta]^+$ and $\tilde v=[\theta-f^\top\tilde z]^+$ satisfy

\mathbb E[\tilde u]=\rho\,\mathbb E_{\mathbb Q}[f^\top\tilde z\mid f^\top\tilde z\ge\theta]-\rho\theta,\qquad \mathbb E[\tilde v]=(1-\rho)\,\mathbb E_{\mathbb Q}[-f^\top\tilde z\mid f^\top\tilde z<\theta]+(1-\rho)\theta .

Consequently $\mathbb E[\rho^{-1}\tilde u+(1-\rho)^{-1}\tilde v]$ equals the spread, and the target set is contained in $\Pi_{\tilde z}\mathcal P$ . 3. A companion, Proposition 3, assertion 3 (p. 21): for $\delta>0$ and $g\ge0$ , the distributions with $\mathbb E_{\mathbb Q}[H_\delta(f^\top\tilde z)]\le g$ are exactly the $\tilde z$ -marginals of a lifted set on $\mathbb R^P\times\mathbb R^5_+$ with auxiliary variables $\tilde u,\tilde v,\tilde w,\tilde s,\tilde t$ .

Significance

The proposition places absolute mean spread information inside the paper's standardized framework. Every result proved there for standardized sets therefore applies to spread-constrained ambiguity sets. The lifted set of Proposition 2 violates the paper's nesting condition (N), so Theorem 1's exact reformulation does not apply. Instead, Theorem 3 and Observation 1 give conservative approximations, which here are linear programs (p. 18). The Huber companion does the same for an expected Huber loss bound, a robust alternative to a variance bound.

Both results are proved in the paper. Neither has a machine-checked proof that this mission is aware of. A formalization adds three things: a checked equality of the two sets, with every integrability and positivity side condition made explicit; reusable lemmas on elementary conditional means of a scalar projection; and a check of the companion. The companion's printed proof contains an incorrect intermediate identity (see Difficulty), although the proposition itself holds.

Difficulty

The obvious reading of the inclusion $\Pi_{\tilde z}\mathcal P\subseteq$ target is "the constraint on $\tilde w$ bounds the spread pointwise". That reading fails, because the spread is a ratio of expectations over two complementary events, and $\tilde u$ and $\tilde v$ are not determined by $\tilde z$ . Only their difference is fixed, almost surely. The bound must hold for every coupling of $(\tilde u,\tilde v)$ with $\tilde z$ that respects the constraints. The reverse inclusion needs an explicit lift of an arbitrary $\mathbb Q$ . The lift has to meet the moment condition $\mathbb E[\tilde w]=\sigma$ exactly, not just as an inequality. The paper leaves that step implicit.

In Lean the main friction is measure-theoretic bookkeeping: integrability of the auxiliary coordinates (which is derived, not assumed), set integrals over the two half-spaces, and push-forwards along the first projection. In the Huber companion, the identity the proof states for the minimized integrand is false in general: with $\delta=1$ and $\tilde u=\tilde v=\tfrac12$ the left side is $\tfrac14$ and the right side is $\tfrac12$ . The inclusion $\Pi_{\tilde z}\mathcal P\subseteq\{\dots\}$ needs a different pointwise inequality.

Formalization scope

$\mathbb R^P$ is Fin nP → ℝ, with $f^\top z$ written f ⬝ᵥ z. The lifted outcome space is (Fin nP → ℝ) × (ℝ × ℝ × ℝ), and $\tilde u,\tilde v,\tilde w$ are the projections uOf, vOf, wOf. The Huber lift uses Fin 5 → ℝ with components $0,\dots,4=\tilde u,\tilde v,\tilde w,\tilde s,\tilde t$ .
The marginal $\Pi_{\tilde z}\mathbb P$ is μ.map Prod.fst. Both theorems are stated as set identities between Set (Measure _).
Conditional means are elementary: $\mathbb E[f^\top\tilde z\,\mathbf 1_A]/\mathbb Q[A]$ (condMeanGe, condMeanLt). σ-algebra conditioning is not used. Both events have probability $\rho$ or $1-\rho$ , both positive because $\rho\in(0,1)$ , so no division by zero occurs.
Integrability convention.
- Members of the target set have $f^\top\tilde z$ integrable, and members of $\mathcal P$ have $\tilde w$ integrable. These are the expectations the page writes, and Lean's integral of a non-integrable function is $0$ , so without these clauses the sets would contain junk members.
- Integrability of $\tilde u$ , $\tilde v$ and $f^\top\tilde z$ under $\mathbb P\in\mathcal P$ is not assumed. It follows from $0\le\tilde u\le\rho\tilde w$ and $0\le\tilde v\le(1-\rho)\tilde w$ almost surely.
- In the companion, $H_\delta(f^\top\tilde z)$ is required to be integrable under $\mathbb Q$ .
Hypotheses are the page's: $\sigma\ge0$ and $0<\rho<1$ ; for the companion, $\delta>0$ and $g\ge0$ . Nothing is added.
Printed typo. Proposition 3.3 prints $H_\delta(t^\top\tilde z)$ in its conclusion. No $t$ occurs there, and the hypothesis and the proof use $f^\top\tilde z$ , so the Lean states $f^\top\tilde z$ .
No trivializing reading. Neither side is empty by construction: the law $\tfrac12(\delta_{-1}+\delta_1)$ on $\mathbb R^1$ with $f=1$ , $\theta=0$ , $\rho=\tfrac12$ , $\sigma=2$ lies in the target set and is the marginal of a member of $\mathcal P$ , as checked in a sorry-free sanity file. For $P=0$ both sides are empty, consistently.
Infrastructure. Elementary conditional means of a scalar projection over complementary half-spaces, set integrals of positive and negative parts, and push-forwards along Prod.fst are reusable beyond this mission. Proofs of the individual milestones are welcome, as are reusable lemmas on lifts of the form $z\mapsto(z,\phi(z))$ .

Selected references

W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Optimization Online preprint 3757 (version of September 22, 2013); Operations Research 62(6):1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6):1294–1306, 2015. https://doi.org/10.1287/opre.2015.1422
P. J. Huber, Robust Estimation of a Location Parameter, Annals of Mathematical Statistics 35(1):73–101, 1964. https://doi.org/10.1214/aoms/1177703732

12 thms2 active usersReviewed

Completed

Dynamic Programming Markov Chain Optimization·Captain: mikedeng1

Robust Markov Decision Processes 1: Over s-Rectangular Ambiguity Sets, Robust Policy Improvement Is Solved by a Stationary Randomized Policy and the Fixed Point of the Robust Bellman MapResearch Paper

Motivation

A Markov decision process (MDP) is evaluated with a transition kernel that, in practice, is estimated from data. The expected total reward of a policy can be very sensitive to small errors in that estimate (Mannor, Simester, Sun and Tsitsiklis, 2007). Robust MDPs address this by letting the kernel range over an ambiguity set and optimizing the worst-case expected reward. Iyengar (2005) and Nilim and El Ghaoui (2005) showed that when the ambiguity set is (s, a)-rectangular (the transition law of each state–action pair varies independently of all others), the robust problem is solved by a robust Bellman recursion and a deterministic stationary policy is optimal.

Wiesemann, Kuhn and Rustem (Robust Markov Decision Processes, Mathematics of Operations Research 38(1), 2013) widen this to s-rectangular ambiguity sets, in which the transition laws of different actions in the same state may be coupled. Their Theorem 4.1 shows that robust policy improvement over such sets is still solved by a robust Bellman fixed point, but the optimal stationary policy may need to randomize. This mission formalizes that theorem and the chain of results its proof uses.

Timeline:

2005: Iyengar; Nilim and El Ghaoui — robust dynamic programming over (s, a)-rectangular sets, deterministic stationary optimal policies.
2010–2013: Wiesemann, Kuhn and Rustem — s-rectangular sets with affinely parametrized kernels; robust value iteration for evaluation (Theorem 3.2) and improvement (Theorem 4.1); randomization needed in general.

Setting

States form a finite set $\mathcal S$ , actions a finite set $\mathcal A$ . Choosing action $a$ in state $s$ and moving to $s'$ pays a reward $r(s,a,s')\ge 0$ ; rewards are discounted by $\lambda\in(0,1)$ and the initial state has a known law $p_0$ in the probability simplex $\mathcal M(\mathcal S)$ .

The uncertain parameter $\xi$ lies in

\Xi=\{\xi\in\mathbb R^q:\ \xi^\top O_l\xi+o_l^\top\xi+\omega_l\ge 0,\ l=1,\dots,L\},

with $O_l$ symmetric negative semidefinite, $\Xi$ bounded and containing a Slater point. Transition probabilities are affine in the parameter, $p^\xi(\cdot\mid s,a)=k_{sa}+K_{sa}\xi\in\mathcal M(\mathcal S)$ for $\xi\in\Xi$ . The ambiguity set $\mathcal P$ is the set of kernels $(p^\xi(\cdot\mid s,a))_{s,a}$ , $\xi\in\Xi$ . It is s-rectangular if $\mathcal P=\times_{s}\mathcal P_s$ , where $\mathcal P_s$ collects the blocks $(P_{s1},\dots,P_{sA})$ of members of $\mathcal P$ : the parameter may be chosen separately in each state.

A stationary randomized policy $\pi\in\Pi$ assigns to each state a distribution $\pi(\cdot\mid s)$ over actions. It induces the Markov reward process

\widehat P_{ss'}(\pi;\xi)=\sum_a\pi(a\mid s)p^\xi(s'\mid s,a),\qquad \widehat r_s(\pi;\xi)=\sum_a\pi(a\mid s)\sum_{s'}p^\xi(s'\mid s,a)r(s,a,s'),

and the reward to-go $v(\pi;\xi)=\sum_{t\ge0}[\lambda\widehat P(\pi;\xi)]^t\widehat r(\pi;\xi)$ . The worst-case expected total reward of $\pi$ is $\inf_{\xi\in\Xi}p_0^\top v(\pi;\xi)$ .

Two robust Bellman maps on $\mathbb R^S$ carry the results:

\phi_s(\pi;w)=\min_{\xi\in\Xi}\Big\{\widehat r_s(\pi;\xi)+\lambda\sum_{s'}\widehat P_{ss'}(\pi;\xi)w_{s'}\Big\},\qquad \varphi_s(w)=\max_{\pi\in\Pi}\phi_s(\pi;w).

In Lean these are phiEval and phiImprove, in the namespace WiesemannRMDP.SRect.

Formalization targets

Goal: Theorem 4.1 (robust policy improvement)

For an s-rectangular $\mathcal P$ , $\varphi$ has a unique fixed point $w^*$ , per-state maximizers $\pi^s\in\arg\max_{\pi\in\Pi}\phi_s(\pi;w^*)$ exist, and the glued policy $\pi^*(a\mid s)=\pi^s(a\mid s)$ together with the constant function $\vartheta^*\equiv w^*$ attains

\sup_{\pi\in\Pi}\ \sup_{\vartheta:\Xi\overset{c}{\to}\mathbb R^S}\Big\{\inf_{\xi\in\Xi}p_0^\top\vartheta(\xi):\ \vartheta(\xi)\le\widehat r(\pi;\xi)+\lambda\widehat P(\pi;\xi)\vartheta(\xi)\ \forall\xi\in\Xi\Big\}=p_0^\top w^*.

Milestones

Proposition 3.1 (b), (c), (a): $v(\pi;\xi)$ is the unique solution of $w=\widehat r+\lambda\widehat Pw$ ; every sub-solution lies below it; $v$ is Lipschitz on $\Pi\times\Xi$ .
Reformulation (10): for fixed $\pi$ , $\inf_\xi p_0^\top v(\pi;\xi)$ equals the inner supremum above, over all and over continuous $\vartheta$ .
$\phi(\pi;\cdot)$ is a contraction (proof of Theorem 3.2).
Theorem 3.2: for s-rectangular $\mathcal P$ and fixed $\pi$ , the constant fixed point of $\phi(\pi;\cdot)$ solves the evaluation problem (10).
From the proof of Theorem 4.1: the glued policy satisfies $w^*=\phi(\pi^*;w^*)$ , and $\varphi$ is a contraction.

Significance

Theorem 4.1 reduces robust policy improvement over s-rectangular sets to computing the fixed point of one map on $\mathbb R^S$ , each evaluation of which is a finite convex program; the paper derives a polynomial-time method from it (Corollary 4.2). It also shows that the optimal policy is stationary but generally randomized, which separates s-rectangular from (s, a)-rectangular robust MDPs. Theorem 3.2 is the evaluation counterpart and is used again when the paper compares s-rectangular and general ambiguity sets (Proposition 3.10).

The results are proved in the paper; none is formalized. On the platform, the (s, a)-rectangular analogue with deterministic policies and costs (Nilim and El Ghaoui) and a related robust linear-programming characterization in another model (Derman, Geist and Mannor) exist, but neither covers coupled actions, randomized policies or rewards depending on the next state. A complete development would give machine-checked robust value iteration for s-rectangular sets and reusable facts on the reward to-go of a finite Markov reward process.

Difficulty

The obvious argument copies the nominal proof: the optimum of the constant- $\vartheta$ restriction is the fixed point $w^*$ , so the constant function is optimal. That only solves the restriction to constant $\vartheta$ ; the problems optimize over all continuous reward to-go functions $\vartheta:\Xi\to\mathbb R^S$ , and showing that no non-constant $\vartheta$ does better is where s-rectangularity enters. Without it the claim is false: the paper's Example 3.11 gives a non-rectangular set where the constant bound is strictly below the worst-case reward. A second subtlety is that $\phi_s(\pi;w)$ depends on $\pi$ only through the row $\pi(\cdot\mid s)$ , which is what lets per-state maximizers be assembled into a single policy; the maximizers are in general not deterministic.

Formalization scope

States and actions are finite nonempty types; policies are functions $\pi(a\mid s)$ satisfying the published IsPolicy, and the simplex condition on $p^\xi(\cdot\mid s,a)$ is the published IsTransitionKernel. $\widehat P$ and $\widehat r$ are built from the published InducedTransition and InducedReward. The model is a structure Model with the standing assumptions in Model.Standing. The reward to-go is defined by the series $\sum_t[\lambda\widehat P]^t\widehat r$ , not as the solution of the evaluation equation, so Proposition 3.1 (b) is not definitional. The minimum over $\Xi$ and the maximum over $\Pi$ are infima and suprema over subtypes, attained under the standing assumptions; the objective $\inf_\xi p_0^\top\vartheta(\xi)$ is used only for $\vartheta$ continuous on $\Xi$ , and where arbitrary $\vartheta$ appear (the middle line of (10)) the infimum is taken in the extended reals. Inequalities on $\mathbb R^S$ are componentwise; contractions are with respect to the sup norm. The paper's $\omega$ in (3b) carries the index $l$ , as elsewhere in the paper.

A statement that compares the fixed point only with constant reward to-go functions, or that takes $w^*$ and $\pi^*$ as hypotheses satisfying the conclusion, is not Theorem 4.1; the goal asserts existence and uniqueness of $w^*$ , existence of the maximizers, and optimality against every policy and every continuous feasible $\vartheta$ .

Useful infrastructure: Neumann series for $\lambda$ times a row-stochastic matrix, continuity of infima over compact parameter sets, and contraction properties of min/max Bellman operators. Proofs of the milestones, and of nonvacuity of richer instances, are welcome.

Selected references

W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov Decision Processes, Mathematics of Operations Research 38(1):153–183, 2013. https://doi.org/10.1287/moor.1120.0566 (formalized from the Optimization Online revision of February 9, 2012: https://optimization-online.org/wp-content/uploads/2010/05/2610.pdf)
G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
S. Mannor, D. Simester, P. Sun, J. N. Tsitsiklis, Bias and Variance Approximation in Value Function Estimates, Management Science 53(2):308–322, 2007. https://doi.org/10.1287/mnsc.1060.0614
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

14 thms2 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Distributionally Robust Convex Optimization II: The Naïve Approximation Implies the Infimal Convolution Bound, Which Implies the Distributionally Robust ConstraintResearch Paper

Motivation

A constraint $\mathbb E[v(x,\tilde z)] \le w$ on a decision $x$ needs the distribution of the random vector $\tilde z$ , which in practice is known only through partial information: a support, some moments, the probability mass of a few regions. Distributionally robust optimization requires the constraint for every distribution consistent with that information. Wiesemann, Kuhn and Sim (Optimization Online 3757, 2013; Oper. Res. 62(6), 2014) introduced a standardized ambiguity set built from expectation conditions and probability bounds on confidence sets. Their Theorem 1 shows that the worst-case constraint over such a set is equivalent to a finite conic system, provided the confidence sets satisfy a nesting condition: any two are strictly nested or disjoint.

Many natural ambiguity sets violate nesting, for instance two overlapping confidence ellipsoids. For these the paper (§2.2) proposes two conservative approximations, the naïve approximation and the infimal convolution bound, and Theorem 3 orders them: the naïve approximation implies the infimal convolution bound, which implies the robust constraint. Infimal convolution bounds of this type had been used in classical and distributionally robust optimization before, e.g. in Goh and Sim (2010), Theorem 4. This mission formalizes Theorem 3, the steps of its proof, and Proposition 1, which compares partitions.

Setting

The random vector is $\tilde z \in \mathbb R^P$ , with an auxiliary $\tilde u \in \mathbb R^Q$ . A proper cone $\mathcal K$ is a closed convex cone with $\mathcal K\cap(-\mathcal K)=\{0\}$ and nonempty interior, and $x \preccurlyeq_{\mathcal K} y$ means $y - x\in\mathcal K$ . For $i \in \mathcal I = \{1,\dots,I\}$ the confidence sets are $\mathcal C_i = \{(z,u) : C_iz + D_iu \preccurlyeq_{\mathcal K_i} c_i\}$ , and the ambiguity set is

\mathcal P = \Big\{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \ \mathbb P[(\tilde z,\tilde u)\in\mathcal C_i]\in[\underline p_i,\overline p_i]\ \ \forall i\in\mathcal I\Big\}.

The standing conditions are: (C1) $\mathcal C_I$ is bounded with $\underline p_I = \overline p_I = 1$ (it is the support); (C2) some $\mathbb P\in\mathcal P$ meets every non-degenerate probability bound strictly; (C3) $v(x,z) = \max_{l}\,[(S_lz+s_l)^\top x + \mathbf t_l^\top z + t_l]$ , a maximum of finitely many bi-affine pieces, so $v$ is convex in $x$ . The distributionally robust constraint (3) is $\mathbb E_{\mathbb P}[v(x,\tilde z)]\le w$ for all $\mathbb P\in\mathcal P$ .

Write $A \Subset B$ when $A$ lies in the interior of $B$ . A partition $\{\mathcal I_j\}_{j\in\mathcal J}$ of $\mathcal I$ , with $J = |\mathcal J|$ blocks, satisfies the weak nesting condition (N′) if within each block any two distinct confidence sets are strictly nested or disjoint. The outer approximation $\mathcal P^j$ keeps the expectation condition and only the probability bounds of block $j$ :

\mathcal P^j = \Big\{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \ \mathbb P[(\tilde z,\tilde u)\in\mathcal C_i]\in[\underline p_i,\overline p_i]\ \ \forall i\in\mathcal I_j\Big\}.

With $\Gamma(x) = \{(y,\delta) : \sum_j y_j = x,\ \sum_j\delta_j = 1,\ \delta > 0\}$ , the naïve approximation (6) and the infimal convolution bound (7) are

\min_{j\in\mathcal J}\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}[v(x,\tilde z)]\le w,\qquad \inf_{(y,\delta)\in\Gamma(x)}\sum_{j\in\mathcal J}\delta_j\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}[v(y_j/\delta_j,\tilde z)]\le w.

Formalization targets

Goal: Theorem 3 (p. 13)

\text{(6)}\ \Longrightarrow\ \text{(7)}\ \Longrightarrow\ \text{(3)},\qquad\text{and (3)} \Longrightarrow \text{(7)},\ \text{(3)}\Longrightarrow\text{(6)}\ \text{ if } J = 1,

under (C1)–(C3), (N′) and one disclosed added hypothesis, the uniform first-moment bound (see Formalization scope).

Milestones (proof of Theorem 3, p. 37; Proposition 1, p. 14)

$\mathcal P\subseteq\mathcal P^j$ for every $j$ (p. 12).
The chain: for $(y,\delta)\in\Gamma(x)$ , $\sum_j\delta_j\sup_{\mathcal P^j}\mathbb E[v(y_j/\delta_j,\tilde z)] \ge \sum_j\delta_j\sup_{\mathcal P}\mathbb E[v(y_j/\delta_j,\tilde z)] \ge \sup_{\mathcal P}\mathbb E[v(x,\tilde z)]$ .
(7) $\Rightarrow$ (3).
The limiting display: with $\delta_{j^\star}(k) = 1-1/k$ , $y_{j^\star} = x$ and $\delta_j(k) = 1/(k(J-1))$ , $y_j = 0$ otherwise,

\sum_j\delta_j(k)\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}[v(y_j/\delta_j(k),\tilde z)]\ \xrightarrow[k\to\infty]{}\ \sup_{\mathbb P\in\mathcal P^{j^\star}}\mathbb E_{\mathbb P}[v(x,\tilde z)].

(6) $\Rightarrow$ (7).
If $J = 1$ then $\mathcal P = \mathcal P^1$ .
Proposition 1: if one partition refines another, both satisfying (N′), then (7) for the finer partition implies (7) for the coarser one.

Significance

The result. Theorem 1 of the paper needs nesting; Theorem 3 is what remains when nesting fails. It certifies that both surrogates are safe (a decision satisfying either satisfies the robust constraint) and that the infimal convolution bound is never looser than the naïve one. The paper also shows that (7), with $\Gamma(x)$ replaced by a closed approximation, has a conic reformulation (Observation 1), while optimizing over (6) with several constraints is strongly NP-hard (Theorem 4). Proposition 1 then says coarser partitions give tighter bounds, which guides the choice of partition.

Formalizing it. The result is proved in the paper; no machine-checked version is known. Formalizing it produces a reusable layer of extended-real worst-case expectations over sets of probability measures, with the infimal convolution and the perspective $\delta\,v(y/\delta,\cdot)$ , and it corrects a gap in the printed proof of (6) $\Rightarrow$ (7) (see below).

Difficulty

The implications (7) $\Rightarrow$ (3) and Proposition 1 are short on paper; in Lean the work lies in extended-real arithmetic, where $-\infty+\infty=-\infty$ , and in the integrability of $v(x,\tilde z)$ . The step (6) $\Rightarrow$ (7) is the delicate one. The constraint $\delta>0$ forbids putting all weight on the minimizing block, so the bound is reached only in a limit, and the limit requires every block's worst-case expectation of $v(0,\tilde z)$ , and of $\delta\,v(x/\delta,\tilde z)$ uniformly in $\delta$ , to be controlled. The outer approximations drop the support condition (C1) for blocks that do not contain $I$ , so these worst-case values can be $+\infty$ , and the printed justification fails.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ; the outcome space is $(\texttt{Fin nP → ℝ})\times(\texttt{Fin nQ → ℝ})$ with its Borel σ-algebra. Indices are 0-based: $\mathcal I$ is Fin (nI + 1) (so $I\ge1$ ), $\mathcal C_I$ is index Fin.last nI, and $\mathcal J$ is Fin nJ. A partition is a surjective block map blk : Fin (nI + 1) → Fin nJ, so every block is nonempty; " $J=1$ " is nJ = 1. Distributions in $\mathcal P$ and in every $\mathcal P^j$ are probability measures with a finite first moment, since a Lean integral of a non-integrable function is $0$ . Worst-case expectations, (6) and (7) take values in EReal, with $\sup\emptyset=-\infty$ ; the minimum in (6) is a finite infimum, and $y_j/\delta_j$ is used only on $\Gamma(x)$ , where $\delta>0$ . Constraint (3) is in its $\forall$ -form.

Added hypothesis. The goal, milestone 4 and milestone 5 assume a uniform first-moment bound: for every $j$ , $\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}\|\tilde z\| < \infty$ . Without it (6) $\Rightarrow$ (7) is false: with $P=1$ , $\mathcal C_1=[0,\tfrac12]$ of probability at least $\tfrac12$ , $\mathcal C_2=[0,1]$ of probability $1$ , the singleton partition, $v(x,z)=z$ and $w=1$ , (6) holds through $\mathcal P^2$ , while $\mathcal P^1$ contains $\tfrac12\delta_0+\tfrac12\delta_M$ for every $M$ , so (7) fails. The bound holds whenever every block contains a bounded confidence set with $\underline p_i=1$ . No other hypothesis is added; (N′), (C1) and the cone conditions are kept as on the page although the proofs do not use them.

The definitions rule out the trivializing formalizations: no expectation is a junk integral, empty blocks are excluded by surjectivity, the ambiguity set is nonempty under (C2), and no real-valued supremum or division by a zero weight appears. Contributions welcome: proofs of the milestones, and reusable lemmas on EReal suprema of integrals and on perspectives of piecewise-affine functions.

Selected references

W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Optimization Online preprint 3757, version of September 22, 2013. https://optimization-online.org/wp-content/uploads/2013/02/3757.pdf
W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Operations Research 62(6):1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
J. Goh, M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4):902–917, 2010. https://doi.org/10.1287/opre.1090.0712

9 thms2 active usersReviewed

Bandit Algorithms Probability·Captain: mikedeng1

A Primal-Dual Learning Algorithm for Personalized Dynamic Pricing with an Inventory Constraint: The Primal-Dual Learning Algorithm Has Regret at Most C(log n)^(2+δ) n^(−1/2)Research Paper

Motivation

A firm selling a fixed stock of a perishable product over a finite season must set prices without knowing how demand responds to them. Online retail and travel platforms often see a customer's segment before quoting a price, so they can price-discriminate across consumer types. Learning a separate demand curve for each type, however, seems to cost more exploration as the number of types grows. Chen and Gallego (arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022) give a learning algorithm whose regret does not depend on the number of types. Their key step is to learn a single scalar first: the shadow price of inventory.

Earlier work on the single-type problem frames the question. Besbes and Zeevi (Operations Research, 2009) defined the regret against the fluid benchmark and showed that no policy can achieve regret decaying faster than $n^{-1/2}$ . Wang, Deng and Ye (Operations Research, 2014) gave a single-product algorithm whose regret matches this rate up to logarithmic factors. Chen and Gallego extend the rate to $M$ types with one inventory constraint.

Setting

There are $M\ge1$ consumer types, a season $[0,T]$ and an inventory $c$ . When the firm charges price $p$ to type $m$ , type- $m$ consumers arrive at rate $d_m(p)$ . Prices range over $[0,p_\infty]$ , where $p_\infty$ is a choke price with $d_m(p_\infty)=0$ . Assumption 1 asks that each $d_m$ be strictly decreasing, bounded and Lipschitz, and that the revenue rate $r_m(\lambda)=\lambda d_m^{-1}(\lambda)$ be Lipschitz and twice differentiable, with $0<M_3\le-r_m''\le M_4$ .

The fluid problem (2) maximizes $\sum_m\int_0^Tp_m(t)d_m(p_m(t))\,dt$ subject to $\sum_m\int_0^Td_m(p_m(t))\,dt\le c$ . Its optimal value is $J^D(T,c)$ . Its dual is one-dimensional. With

\mathcal R_m(z)=\max_{p}d_m(p)(p-z),\qquad \mathcal P_m(z)=\operatorname*{argmax}_pd_m(p)(p-z),\qquad g(z)=cz+T\sum_m\mathcal R_m(z),

the dual optimum is $z^*=\operatorname{argmin}_{z\ge0}g(z)$ , and the optimal fluid prices are the constants $p^*_m=\mathcal P_m(z^*)$ .

In the $n$ -th system demand and inventory scale together: type $m$ arrives as a Poisson process with rate $n\,d_m(p)$ , and the inventory is $nc$ . The firm does not know $d_m$ . It knows $T$ , $c$ , $n$ , the constants of Assumption 1 and, by Assumption 2, intervals $[\underline p,\overline p]$ and $[0,\overline z]$ that contain every $p^*_m$ and $z^*$ . A policy $\pi$ has expected revenue $J^\pi_n(T,c)$ , and its regret is

R^\pi_n(T,c)=1-\frac{J^\pi_n(T,c)}{J^D_n(T,c)}.

Algorithm 1, the primal-dual learning algorithm, runs phases $k=1,\dots,K$ of shrinking lengths $\tau^{(k)}$ . In each learning phase it tests a price grid inside the current interval estimators of every $p^*_m$ . It then minimizes an empirical dual function on a grid of $z$ and re-centres the interval estimators of $z^*$ and $p^*_m$ . In the last phase it either charges a marked-up price (sufficient capacity), or tests two prices and interpolates between them so that total sales end close to $nc$ (insufficient capacity). Its tuning depends on a constant $\epsilon>0$ .

Formalization targets

Goal: Theorem 1 (p. 17)

For every $\delta>0$ one can choose $\epsilon>0$ and a constant $C$ , independent of $n$ , such that

R^\pi_n(T,c)\le C(\log n)^{2+\delta}n^{-1/2}\qquad\text{for all }n\ge3.

The two capacity regimes (Propositions 2–3)

z^*=0:\ R^\pi_n=O\big((\log n)^{2+16\epsilon}n^{-1/2}\big),\qquad z^*>0:\ R^\pi_n=O\big((\log n)^{2+18\epsilon}n^{-1/2}\big).

Milestones

Proposition 1: the fluid problem is solved by the constant prices $p^*$ , with complementary slackness; and the monotonicity, convexity and derivative of $\mathcal P_m$ and $\mathcal R_m$ .
Lemmas 9 and 10: a Poisson tail bound decaying faster than any power, and $\mathbb E|X-\lambda|\le\sqrt\lambda$ .
Lemmas 1 and 2: $K\le3\log n+3$ , and the learning phases take at most half the season.
Lemmas 3–5: the interval estimators contain $z^*$ , $p^*_m$ and $\mathcal P_m$ on the dual interval, except with probability $O((\log n)^2/n)$ .
Lemmas 6–7: the sales at the start of the last phase are close to the fluid level.
Lemma 8: when $z^*>0$ , $\mathbb E|S(T)-nc|=O((\log n)^\epsilon n^{1/2})$ .

Significance

Theorem 1 states that personalized pricing for $M$ types under a shared inventory constraint is learnable at the single-type rate $n^{-1/2}$ , up to logarithms, with a constant independent of $n$ . Combined with the Besbes–Zeevi lower bound, the algorithm is rate-optimal. Learning the scalar shadow price $z^*$ , instead of the joint optimum of an $M$ -dimensional problem, is what avoids the curse of dimensionality.

The result is proved in the paper; no machine-checked version exists. A formalization would add to the platform a multi-type Poisson pricing model with stock-outs, the one-dimensional Lagrangian dual of the fluid revenue-management problem, an exactly specified multi-phase learning algorithm, and reusable Poisson deviation lemmas. Lemmas 1, 2, 9 and 10 and Proposition 1 can be proved independently of the probabilistic analysis.

Difficulty

The obvious argument estimates every $p^*_m$ directly and charges the estimate. With interval estimators of width $n^{-1/4}$ this loses revenue of order $n^{-1/4}$ per unit time when the inventory constraint binds ( $z^*>0$ ), because $p^*_m$ is then not the unconstrained maximizer of $p\,d_m(p)$ . The paper's (11) and (19) show the loss. The bound $n^{-1/2}$ requires steering the total sales to within $O(n^{1/2})$ of the inventory, which is Lemma 8, and a second-order expansion of the revenue around $p^*$ that uses the first-order condition $r_m'(d_m(p^*_m))=z^*$ .

Formally, a further difficulty is the closed loop: the prices of a phase depend on the counts of earlier phases, and the counts are Poisson only conditionally, through the random time change $N_m(n\int_0^td_m(P_m(s))\,ds)$ .

Formalization scope

All declarations live in the namespace PrimalDualPricing.Regret. Printed page numbers equal PDF page numbers in the cited preprint.

Model. Types are Fin M. Each $d_m:\mathbb R\to\mathbb R$ satisfies Assumption 1 on $[0,p_\infty]$ and is otherwise any extension with $0\le d_m\le M_1$ ; the last-phase prices $\underline p^{(K)}_m-\alpha$ and $\overline p^{(K)}_m+\alpha$ can leave $[0,p_\infty]$ . $d_m(p_\infty)=0$ encodes the choke price. $\mathcal P_m$ and $z^*$ are fields carrying their optimality properties.
Assumption 2 is read with $z^*\in[0,\overline z)$ ; the page prints $(0,\overline z)$ , which would drop the case $z^*=0$ that Proposition 2 and Theorem 1 cover. The price interval is placed in the domain, $0\le\underline p<\overline p\le p_\infty$ .
Remark 2 assumes $M_3\le g''\le M_4$ ; this is read on $[0,\overline z]$ , because globally it is unsatisfiable. Each $\mathcal P_m$ is $M_2$ -Lipschitz.
The fluid value $J^D$ is the supremum of (2) over measurable price paths. The identity $J^D=T\sum_mp^*_md_m(p^*_m)$ is Proposition 1.4, a milestone, and is not built into the definition.
The algorithm. The grid sizes $N^{(k)}$ , $N_z^{(k)}$ are rounded up. Grid spacing is $\Delta_m/N$ for prices and $\Delta_z/(N_z+1)$ for duals: the text and Table 1, respectively the text and line 15, agree on these, and Algorithm 1 line 7 and Table 1 print the other forms. Ties in (8)–(9) go to the smallest index. $\theta$ in (14) is projected onto $[0,1]$ , with $\theta=0$ when (14) is degenerate. An empty $p^l$ period in step 4 follows the pseudo-code. The decision rules never take $d_m$ , $\mathcal P_m$ or $z^*$ as arguments.
The system. $M$ independent unit-rate Poisson processes (the published IsPoissonProcess) with right-continuous, jointly measurable paths. The inventory of the $n$ -th system is $\lfloor nc\rfloor$ units, and nothing is sold after the stock-out. Lemmas 6–8 use the uncapped sales of the paper's modified system (§4).
Asymptotics. " $O(f(n))$ " is read as $\exists C$ , independent of $n$ and the phase index, for all $n\ge3$ . "Sufficiently small $\epsilon$ " is read as every $\epsilon\in(0,\epsilon_0)$ . The algorithm needs $n\ge3$ for $K$ to exist.
Corrected misprints. Proposition 1.2 prints $\mathcal R_m'=-\sum_md_m(\mathcal P_m)$ with the index reused; the statement is $-d_m(\mathcal P_m(z))$ . Proposition 1.3 and the global form of the bound in 1.1 fail at the kinks of $\mathcal P_m$ . Part 1's derivative bound is stated as a Lipschitz bound, and part 3 is omitted. Lemmas 3–4 are stated in product form. Propositions 2–3 are stated through their regret conclusions. The printed comparison $\tilde J^\pi_n\le J^\pi_n$ (pp. 13–14) can fail when a last-phase price exceeds $\overline p$ , so it is not used.

A formalization that lets the policy read the true demand, measures regret against anything other than $J^D_n$ , ignores the stock-out in $J^\pi_n$ , or assumes the high-probability events of Lemma 5 would trivialize the goal; none of these is done here.

Contributions to the reusable parts are welcome: Poisson tails, the envelope theorem for $\mathcal R_m$ , and the time-change construction of policy-driven Poisson sales.

Selected references

N. Chen, G. Gallego, A Primal-dual Learning Algorithm for Personalized Dynamic Pricing with an Inventory Constraint, arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1812.09234
O. Besbes, A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6), 2009. https://doi.org/10.1287/opre.1080.0640
Z. Wang, S. Deng, Y. Ye, Close the Gaps: A Learning-While-Doing Algorithm for Single-Product Revenue Management Problems, Operations Research 62(2), 2014. https://doi.org/10.1287/opre.2013.1249
G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24

21 thms2 active usersReviewed

Completed

Algorithmic Game Theory·Captain: mikedeng1

Intrinsic Robustness of the Price of Anarchy I: Every Coarse Correlated Equilibrium of a Smooth Game Has Expected Cost at Most the Robust Price of Anarchy Times OptimalResearch Paper

Motivation

The price of anarchy (POA) of a game measures how much selfish behaviour costs: it is the ratio between the largest cost of an equilibrium and the cost of an optimal outcome, for a nonnegative objective such as the sum of the players' costs. Since Koutsoupias and Papadimitriou (1999) and Roughgarden and Tardos (2002), POA bounds have been proved for routing, scheduling, facility location, auctions and many other models, mostly for pure Nash equilibria.

Pure Nash equilibria need not exist, are hard to compute in general, and are not what players running learning algorithms converge to. A bound that holds only at pure Nash equilibria therefore says little about realized play. Roughgarden's paper (J. ACM 62(5), 2015; conference version STOC 2009) observes that most known POA proofs follow one template, the smoothness argument, and proves that any bound obtained this way extends automatically to much broader equilibrium concepts. This mission formalizes the static half of that result: the extension to coarse correlated equilibria (Theorem 3.2) and to their approximate versions (Theorem 4.1).

Timeline:

1999: Koutsoupias and Papadimitriou introduce the worst-case ratio of equilibria to optimum.
2005: Awerbuch–Azar–Epstein and Christodoulou–Koutsoupias prove the bound 5/2 for linear congestion games; their arguments are smoothness arguments in hindsight.
2009: Roughgarden (STOC) isolates smoothness and proves the extension theorems; the journal version (2015) adds the tightness results for congestion games.
2009–2015: smoothness is adapted to auctions (Syrgkanis–Tardos 2013) and to local and approximate variants.

Setting

A cost-minimization game has finitely many players $i$ . Player $i$ chooses a strategy $s_i$ from an arbitrary set $S_i$ ; an outcome is a vector $s = (s_i)_i$ , and player $i$ pays a real cost $C_i(s)$ . Write $(s_i', s_{-i})$ for the outcome in which player $i$ switches to $s_i'$ and the others stay put. The joint cost is $C(s) = \sum_i C_i(s)$ , assumed nonnegative.

An outcome $s$ is a pure Nash equilibrium if $C_i(s) \le C_i(s_i', s_{-i})$ for every $i$ and $s_i' \in S_i$ . For $\epsilon \ge 0$ it is an $\epsilon$ -Nash equilibrium if $C_i(s) \le (1+\epsilon) C_i(s_i', s_{-i})$ .

A coarse correlated equilibrium is a probability distribution $\sigma$ over outcomes with

\mathbf{E}_{s\sim\sigma}[C_i(s)] \le \mathbf{E}_{s\sim\sigma}[C_i(s_i', s_{-i})] \quad\text{for every } i \text{ and } s_i' \in S_i,

and an $\epsilon$ -coarse correlated equilibrium satisfies the same with a factor $(1+\epsilon)$ on the right. Every pure Nash, mixed Nash and correlated equilibrium is a coarse correlated equilibrium, and coarse correlated equilibria are exactly the limits of play in which every player has vanishing external regret.

The game is $(\lambda,\mu)$ -smooth if for every two outcomes $s, s^*$

\sum_i C_i(s_i^*, s_{-i}) \le \lambda\, C(s^*) + \mu\, C(s).

The robust price of anarchy is $\rho(G) = \inf\{\lambda/(1-\mu) : \mu < 1,\ G \text{ is } (\lambda,\mu)\text{-smooth}\}$ .

Formalization targets

Goal: Theorem 3.2 (static extension theorem)

For every game $G$ with robust POA $\rho(G)$ , every coarse correlated equilibrium $\sigma$ and every outcome $s^*$ ,

\mathbf{E}_{s\sim\sigma}[C(s)] \le \rho(G)\cdot C(s^*).

Milestones

Claim (3)–(5), p. 5: in a $(\lambda,\mu)$ -smooth game with $\lambda > 0$ , $\mu < 1$ , every pure Nash equilibrium $s$ satisfies $C(s) \le \frac{\lambda}{1-\mu} C(s^*)$ for an optimal $s^*$ .
§4.1, p. 16: every $\epsilon$ -Nash equilibrium satisfies $C(s) \le \frac{(1+\epsilon)\lambda}{1-\mu(1+\epsilon)} C(s^*)$ for an optimal $s^*$ .
The chain (16)–(21), p. 13: for one fixed pair $(\lambda,\mu)$ with $\mu < 1$ , $\mathbf{E}_{s\sim\sigma}[C(s)] \le \frac{\lambda}{1-\mu} C(s^*)$ for every coarse correlated equilibrium $\sigma$ and every outcome $s^*$ .
Theorem 4.1, p. 16: for every $\epsilon$ -coarse correlated equilibrium,

\mathbf{E}_{s\sim\sigma}[C(s)] \le \frac{(1+\epsilon)\lambda}{1-\mu(1+\epsilon)}\cdot C(s^*).

Significance

Theorem 3.2 says that the robust POA of a game bounds the expected cost of every coarse correlated equilibrium, which contains every other equilibrium concept in the hierarchy. Combined with the companion result for no-regret sequences (Theorem 3.3, mission II of this series), it makes POA bounds meaningful for learning dynamics: whenever players use no-regret algorithms, their average cost is within the robust POA of optimal. For linear congestion games, which are $(5/3, 1/3)$ -smooth, it yields the bound $5/2$ for all coarse correlated equilibria at once. Theorem 4.1 shows that the bounds degrade gracefully when the equilibrium condition holds only approximately, which covers equilibria computed to finite accuracy.

The results are proved in the paper; their proofs are short. No machine-checked version is known to exist. The mission's value is a reusable, platform-wide definition layer for cost-minimization games, smoothness, the robust POA and the equilibrium hierarchy, on which later results can be stated: the bicriteria bounds of §4.2, the tightness theorem for congestion games (mission III), and smoothness bounds for specific models such as auctions, routing and scheduling.

Difficulty

The mathematics is linear: it uses only linearity of expectation and one rearrangement. The difficulty lies in the encoding. The robust POA is an infimum over a set that may be empty (then $\rho(G) = +\infty$ on the page) and need not be attained. Passing from the fixed-pair bound to the infimum uses $C(s^*) \ge 0$ . Theorem 4.1's printed side condition $\epsilon < 1/\mu - 1$ is meaningless when $\mu = 0$ and reverses its meaning when $\mu < 0$ . Each of these must be handled so that the formal statement is neither false nor vacuous.

Formalization scope

Players form a finite type with decidable equality, and strategy sets are arbitrary types with no finiteness assumed. Outcomes are dependent functions, and the deviation $(s_i', s_{-i})$ is Function.update s i s'ᵢ. Costs are real-valued, and $\lambda, \mu$ are unconstrained reals except $\mu < 1$ . Probability distributions are finitely supported weight functions that are nonnegative with total mass $1$ . Expectations are therefore finite sums with no integrability side conditions. This covers all finite games and all mixed and correlated equilibria of finite games, but not distributions with infinite support.

The robust POA is an extended-real (EReal) infimum over the smoothness pairs with $\mu < 1$ , so it is $+\infty$ when no such pair exists, and the goal compares the expected cost with $\rho(G)\cdot C(s^*)$ in EReal. The goal carries two explicit hypotheses:

the joint cost is nonnegative, which is the paper's standing assumption (§1, p. 2; §2.4, p. 10);
some smoothness pair with $\mu < 1$ exists, so that $\rho(G) < +\infty$ .

Without the second, a game with no smoothness pair and $C(s^*) = 0$ would be claimed to have expected cost at most $0$ (EReal sets $(+\infty)\cdot 0 = 0$ ), which the page does not assert. A formalization in which the distribution may have total mass $0$ , or in which $\rho(G)$ is an infimum over all pairs rather than over the smoothness pairs with $\mu < 1$ , trivializes or falsifies the goal, and is ruled out by the definitions.

In Theorem 4.1 and the $\epsilon$ -Nash bound:

" $\epsilon < 1/\mu - 1$ " is encoded as $\mu(1+\epsilon) < 1$ , which agrees with it for $0 < \mu < 1$ ;
$\epsilon \ge 0$ is assumed, the implicit domain of an approximation parameter.

The $\epsilon$ -coarse correlated equilibrium is the extension of (15) that the paper says is "defined in the same way" as $\epsilon$ -Nash equilibria (p. 15). Remark 4.4 writes out the payoff analogue.

Claim (3)–(5) and the $\epsilon$ -Nash bound keep the paper's hypotheses $\lambda > 0$ and optimality of $s^*$ , although the inequalities hold without them. Example 4.2 is not posed: its printed bound $(5-5\epsilon)/(2-\epsilon)$ should read $(5+5\epsilon)/(2-\epsilon)$ .

Contributions welcome:

proofs of the four milestones and of the goal;
a measure-theoretic version for distributions with infinite support, with explicit integrability hypotheses;
reuse of the definitions in other smoothness results.

Selected references

T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, J. ACM 62(5), Article 32, 2015. https://doi.org/10.1145/2806883
T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, Proc. 41st ACM STOC, 513–522, 2009. https://doi.org/10.1145/1536414.1536485
E. Koutsoupias, C. Papadimitriou, Worst-Case Equilibria, Proc. STACS, LNCS 1563, 404–413, 1999. https://doi.org/10.1007/3-540-49116-3_38
G. Christodoulou, E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, Proc. 37th ACM STOC, 67–73, 2005. https://doi.org/10.1145/1060590.1060600
B. Awerbuch, Y. Azar, A. Epstein, The Price of Routing Unsplittable Flow, Proc. 37th ACM STOC, 57–66, 2005. https://doi.org/10.1145/1060590.1060599
V. Syrgkanis, É. Tardos, Composable and Efficient Mechanisms, Proc. 45th ACM STOC, 211–220, 2013. https://doi.org/10.1145/2488608.2488635

8 thms2 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models 2: Customization Raises the Optimal Expected Revenue by at Most a Factor m, and the Factor Is TightResearch Paper

Motivation

An assortment decision determines which products a seller makes available to a customer. When customers differ, the seller may first choose a limited collection of products and then decide which of those products to display to each arriving customer. This is a concrete way to represent personalized product pages or offers with a common inventory or display budget. The benefit of that second decision is not immediate from a single-customer model: personalization can remove products that dilute one type's purchases while retaining them for another type. El Housni and Topaloglu quantify this benefit for a mixture of multinomial logit choice models.

Their Theorem 3.1 compares optimal expected revenue with and without customer-type customization. It gives a universal factor depending only on the number of types and an explicit family showing that this order can occur. The result is already proved in the authors' SSRN version of December 7, 2021. This mission concerns the statements and proof in that version; the published Operations Research article appeared in 2023 and may use different numbering.

Setting

There are $n$ products $N=\{1,\ldots,n\}$ and $m$ customer types $M=\{1,\ldots,m\}$ . Product $i$ earns revenue $r_i>0$ when purchased. Customer type $j$ arrives with probability $\theta_j\ge0$ , with $\sum_{j\in M}\theta_j=1$ . Its preference weight for product $i$ is $v_{ij}\ge0$ ; the no-purchase alternative has weight one. An assortment $S\subseteq N$ offered to type $j$ yields MNL expected revenue

\operatorname{Rev}_j(S)=\frac{\sum_{i\in S}r_i v_{ij}}{1+\sum_{i\in S}v_{ij}}.

The seller may initially carry at most $K$ products. In the customized assortment problem (CAP), it chooses $S$ and, after seeing the type, offers a subset $S_j\subseteq S$ . For a fixed carried set, write $f_j(S)=\max_{T\subseteq S}\operatorname{Rev}_j(T)$ and $f^C(S)=\sum_{j\in C}\theta_j f_j(S)$ for any collection $C$ of types. Thus $f^M(S)$ is the expected personalized revenue. In the mixed multinomial logit problem (MMNL), the same carried assortment $S$ is offered to every type. Both models obey the same first-stage cardinality limit:

z_{\rm CAP}=\max_{S\subseteq N,\ |S|\le K}f^M(S),\qquad z_{\rm MMNL}=\max_{S\subseteq N,\ |S|\le K}\sum_{j\in M}\theta_j\operatorname{Rev}_j(S).

This formulation follows §2 and §3 of the December 2021 SSRN version, pp. 5–7. A zero preference weight is allowed: the authors' tightness instance assigns zero to products a type does not consider.

Formalization targets

Theorem 3.1: universal comparison

For every valid model and every first-stage budget $K$ , the target is

z_{\rm MMNL}\le z_{\rm CAP}\le m\,z_{\rm MMNL}.

The factor counts customer types, not products. The result covers $K=0$ as well: both values are zero. It does not assume the products are sorted by revenue, since the numerical indexing convention in §2 is unnecessary for this comparison and is incompatible with the paper's tightness family.

Theorem 3.1: order-tight family

The same theorem says that there are instances for which the CAP value is $\Omega(m)$ times the MMNL value. The formal target uses the instance constructed in its proof, pp. 8–9 and records the explicit bound implied there:

z_{\rm MMNL}>0,\qquad z_{\rm CAP}\ge\frac{m}{6}\,z_{\rm MMNL}\qquad(m\ge2).

In this family $n=K=m$ . With $\alpha=(\sum_{j=1}^m a^{-j})^{-1}$ , the parameters are $\theta_j=\alpha/a^j$ , $r_i=a^i$ , and $v_{ij}=b^{m-i+1}$ when $i\le j$ and zero otherwise. The proof chooses $b=m-1$ and $a=2m(m-1)^m$ . The goal also asserts that this family satisfies the model assumptions. The accompanying milestones are the paper's typewise comparison, the CAP lower bound, equation (3.1), its two term bounds, and the MMNL upper bound.

Significance

The universal inequality limits the improvement that type-specific displays can offer in this model using only the number of types. The family in the second part shows that no bound independent of $m$ can replace it across all valid instances. Thus the comparison locates the possible value of customization even when the seller may carry every product. It also distinguishes the effect of a shared display from the effect of the common product budget, since the example has $K=n$ .

The paper already proves both claims. A complete formal development would check the exact MNL revenue formula, the two finite optimization problems, and the asymptotic example within one Lean environment. It would leave reusable definitions for personalized and common assortments under a mixture of choice models. The statements in this draft compile with proof placeholders; this mission does not claim that the theorem has a machine-checked proof yet. It welcomes proofs of the listed milestones, lemmas about finite maxima and nonnegative MNL revenue, and a proof of the combined goal.

Difficulty

For each type, personalization maximizes revenue over its own subset of $S$ ; MMNL must use one subset for all types. Exchanging the sum over types with a maximum over assortments would erase that distinction and is generally invalid. A simple comparison of the two optima gives the first inequality but cannot explain the precise factor $m$ or why it can be approached in order. The tightness family also balances rapidly changing revenues and arrival probabilities against preference weights. Its boundary case $m=2$ has $b=1$ , so a claim needing $b>1$ would miss a valid member of the family.

Formalization scope

Lean represents products by Fin n, customer types by Fin m, and assortments by Finset (Fin n). The paper's one-based product $i$ is Lean's index i.val + 1: $a^i$ becomes a ^ (i.val + 1), and $b^{m-i+1}$ becomes b ^ (m - i.val). The preference function takes product first and type second, matching $v_{ij}$ . The common revenue calculation imports the published ChoiceCDLP.MNL.mnlObjective with no-purchase weight one.

All maxima are Finset.sup' over nonempty finite families. The feasible family contains the empty assortment for every natural-number budget; the personal subassortment family contains the empty set as well. This makes the values genuine finite maxima, including at zero budget. No real sSup fallback value is used. The standing assumptions are positive revenues, nonnegative preference weights, nonnegative arrival probabilities, and a probability sum of one. The explicit instance is restricted to $m\ge2$ , has positive MMNL value, and satisfies each standing assumption. These conditions exclude a vacuous $\Omega(m)$ ratio based on zero MMNL value or an instance outside the model.

The complete development needs elementary facts about finite sums, powers, ordered Finsets, finite maxima, and nonnegative rational functions. The MNL objective is already a separate published definition; the paper-specific CAP, MMNL, and instance definitions are local. The proof targets are the claims printed in the December 2021 SSRN version, with the constant $1/6$ disclosed as an explicit pin from its proof.

Selected references

O. El Housni and H. Topaloglu, Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models: Value of Personalized Assortments, SSRN 3830082, version of December 7, 2021, §§2–3, pp. 5–9; published in Operations Research, 2023. SSRN

10 thms2 active usersReviewed

Completed

Optimization Theoretical Computer Science·Captain: mikedeng1

Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models 1: Augmented Greedy Earns a (1 − 1/e) Fraction of the Optimal Revenue from the Complete Customer TypesResearch Paper

Motivation

Retailers that carry a limited range of products often know something about a customer before choosing which of those products to display. The customized assortment problem asks which products to carry when the displayed assortment may be tailored to the arriving customer's type. This separates the first-stage capacity decision from the later offer decision. El Housni and Topaloglu study the problem under a mixture of multinomial logit choice models and develop an approximation framework for it in their SSRN paper. This mission isolates their structural guarantee for Augmented Greedy, Theorem 4.2 of the PDF version dated 7 December 2021. The theorem identifies the revenue recovered from customer types whose optimal personalized offers agree with a chosen product subset.

The paper contrasts this setting with ordinary assortment optimization, where every type sees the same products. Its later approximation results use the structural guarantee here as a component. The classical comparison is the cardinality-constrained greedy bound for monotone submodular functions, associated with Nemhauser, Wolsey and Fisher (1978). The paper's Appendix B gives an instance in which the customized revenue function lacks global submodularity, so that classical result does not apply directly. El Housni and Topaloglu, §§4 and App. B.

Setting

Let $N=\{1,\ldots,n\}$ be a finite product set. Product $i$ has positive revenue $r_i$ , and products are indexed with $r_1\ge\cdots\ge r_n>0$ . Let $M=\{1,\ldots,m\}$ be customer types. A type- $j$ customer arrives with probability $\theta_j\ge0$ , with $\sum_{j\in M}\theta_j=1$ , and assigns each product $i$ a nonnegative preference weight $v_{ij}$ . The no-purchase option has weight one. Offering an assortment $T\subseteq N$ to that customer gives MNL expected revenue

\operatorname{Rev}_j(T)= \frac{\sum_{i\in T}r_i v_{ij}}{1+\sum_{i\in T}v_{ij}}.

If the retailer initially carries only $S\subseteq N$ , it can still choose the best offer to each customer type. Thus $f_j(S)=\max_{T\subseteq S}\operatorname{Rev}_j(T)$ . For $C\subseteq M$ , write $f^C(S)=\sum_{j\in C}\theta_j f_j(S)$ , and abbreviate $f=f^M$ . The first-stage capacity is $K$ ; an optimal solution $S^*$ of CAP maximizes $f(S)$ among sets with at most $K$ products. These definitions and the standing data assumptions are stated in §2 and §4 of the paper.

For each product $i$ , the prefix $V_i=\{1,\ldots,i\}$ contains products at least as early in the revenue ordering. Greedy starts at the empty set, repeatedly adds an available product that maximizes the new objective value, and stops at cardinality $k$ or when the prefix is exhausted. Augmented Greedy runs Greedy on $V_i$ for each $i$ , using $S\mapsto\sum_{j\in C}\theta_j\min(f_j(S),r_i)$ , and returns whichever candidate has the greatest $f^C$ value. Both stages may break ties arbitrarily. El Housni and Topaloglu, §4.1.

For type $j$ , use the optimal personalized assortment $S_j^*=\{i\in S^*:r_i\ge f_j(S^*)\}$ , characterized by Lemma E.1. A type $j\in C$ is complete with respect to $P\subseteq N$ when $P\cap S_j^*=P\cap S^*$ ; let $C_P$ collect these types. The threshold choice matters because zero-weight products can be present in other optimal offers without helping a customer. El Housni and Topaloglu, Definition 4.1 and App. E.

Formalization targets

Theorem 4.2: complete-type revenue

For every $C\subseteq M$ , $P\subseteq N$ , $k$ with $|P\cap S^*|\le k$ , and every output $\Delta$ of Augmented Greedy on $C,k$ ,

f^C(\Delta)\ge(1-1/e)\,f^{C_P}(P\cap S^*).

This is the mission goal, the structural performance statement of Theorem 4.2, p. 11. It does not assert a constant-factor approximation to all of CAP: it identifies the contribution from complete customer types.

Supporting targets

The milestone list follows the results used with this bound: monotonicity of $f_j$ from Appendix C; the MNL threshold assortment of Lemma E.1; submodularity of $S\mapsto\min(f_j(S),r_i)$ on $V_i$ from Lemma 4.3; and the cited $1-1/e$ Greedy guarantee for a nonnegative monotone submodular objective. The greedy milestone compares its output against every feasible set of cardinality at most $k$ .

Significance

The theorem says that one algorithmic output captures a fixed fraction of the benchmark supplied by complete types, despite the absence of global submodularity of $f$ . It connects the local behavior of truncated type revenues to the full customized assortment objective. The paper uses this result in the development of later algorithms; without it, the standard submodular greedy theorem gives no immediate conclusion for CAP. El Housni and Topaloglu, §§4–5.

The mathematical results are proved in the 2021 paper. The formalization work here is to give machine-checkable statements for the objective, the algorithm with all its legal tie choices, and the four supporting targets, then supply proofs. The MNL revenue formula is already available as a published platform definition; the local CAP and algorithm definitions specify the extra model needed by this theorem. A completed development could also support later CAP missions that use the same threshold and submodularity properties.

Difficulty

The tempting argument applies the classical greedy guarantee directly to $f$ , since $f$ increases when more products are carried. Appendix B of the paper shows that this fails: even for one customer type, $f$ need not be submodular. Restricting the ground set to a revenue prefix and truncating each $f_j$ at that prefix's revenue level changes the submodularity question, but the final guarantee must still concern the untruncated $f^C$ objective. The threshold condition in the definition of $C_P$ is what makes that comparison meaningful. El Housni and Topaloglu, App. B, Lemma 4.3 and Theorem 4.2.

Formalization scope

Products and types are Fin n and Fin m; their zero-based Lean indices correspond to the paper's indices plus one. Assortments and type groups are finite sets. The model assumes $r_i>0$ , $v_{ij}\ge0$ , $\theta_j\ge0$ , $\sum_j\theta_j=1$ , and decreasing revenue order. The no-purchase weight is exactly one. CAP and personalized revenue use maxima over nonempty finite powersets, so empty input sets have their intended value rather than an arbitrary real supremum. The theorem keeps the source's optimality assumption on $S^*$ , even though its particular inequality uses less.

The Greedy predicate describes each successive maximizer and the exact stopping rule. Augmented Greedy requires a Greedy output at every prefix and an $f^C$ -maximizing choice among them. Thus the output is constrained by the printed algorithm, and the statement covers every tie-break. The type- $j$ assortment is defined from $S^*$ by the Lemma E.1 threshold, rather than supplied as a free set. These choices rule out a size-only output condition, an arbitrarily chosen $S_j^*$ , a vacuous run predicate, and real supremum defaults. The target includes the corner cases $k=0$ , $C=\varnothing$ , and $P\cap S^*=\varnothing$ , where its right side is zero. Arrival probabilities summing to one force $m\ge1$ ; Augmented Greedy has an output only when at least one product exists.

The reusable parts are the MNL threshold characterization, finite-set submodularity and the general Greedy bound. Contributions toward those lemmas, the paper's case analysis for Lemma 4.3, and the final structural theorem are in scope. Runtime claims, the paper's later logarithmic approximation theorems and its computational experiments are outside this mission.

Selected references

Omar El Housni and Huseyin Topaloglu, Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models: Value of Personalized Assortments, SSRN 3830082, version of 7 December 2021; published as Operations Research 71(4), 2023. SSRN preprint. The mission's numbering and page citations use the pinned 2021 PDF.
George L. Nemhauser, Laurence A. Wolsey and Marshall L. Fisher, An Analysis of Approximations for Maximizing Submodular Set Functions—I, Mathematical Programming 14, 265–294, 1978. DOI.

9 thms2 active usersReviewed

Algorithmic Game Theory Optimization·Captain: mikedeng1

Intrinsic Robustness of the Price of Anarchy III: For Every Set of Cost Functions, Congestion Games Are Tight — the Worst-Case Pure Price of Anarchy Equals the Best Smoothness BoundResearch Paper

Motivation

In a congestion game, each player chooses resources and pays a cost that depends on how many players use each chosen resource. Such games model shared facilities and network use, where independently chosen strategies can cost more in total than a coordinated choice. The price of anarchy measures this inefficiency by comparing the social cost of an equilibrium with the minimum social cost. A familiar way to bound it is to prove a smoothness inequality that applies to every pair of strategy profiles. That inequality has a useful reach: once established, it bounds not only pure Nash equilibria but also broader equilibrium notions. The question in this mission is how much that reach costs in sharpness. Roughgarden (2015) proves that for congestion games it costs nothing at the level of the worst case over any fixed collection of allowed resource cost functions.

For affine resource costs, earlier analyses had already identified a worst-case value of $5/2$ , attained by a finite congestion game and matched by a smoothness bound. The 2015 paper asks whether this agreement reflects affine costs or a general property of congestion games. Its Theorem 5.8 gives the latter answer, even when the collection of allowed functions is infinite and has no prescribed formula. The mission treats the theorem at that generality, while giving the finite positive case and the boundary case their own supporting targets. Roughgarden (2015), §§2.3 and 5.

Setting

A finite congestion game has a finite player set, a finite resource set $E$ , and for each player $i$ a nonempty set $S_i$ of subsets of $E$ called strategies. Each resource $e$ has a cost function $c_e:\mathbb N\to\mathbb R$ . For a strategy profile $A=(A_i)_i$ , its load $x_e(A)$ is the number of players whose selected strategy contains $e$ . Player $i$ pays $C_i(A)=\sum_{e\in A_i}c_e(x_e(A))$ , and the social cost is $C(A)=\sum_i C_i(A)$ . A profile is a pure Nash equilibrium when no player can lower its own cost by changing its strategy alone. These are the objects of Example 2.5 in Roughgarden (2015).

Fix a nonempty set $\mathcal C$ of resource cost functions, each nonnegative, nondecreasing, and not identically zero on positive loads. The class $\mathcal G(\mathcal C)$ contains every finite congestion game whose resource functions belong to $\mathcal C$ . It permits any finite number of players and resources and any nonempty strategy families. The pure price of anarchy $\rho_{\mathrm{pure}}(G)$ is the largest equilibrium-to-optimum cost ratio in one game, allowing $+\infty$ when an equilibrium costs more than zero but the optimum costs zero.

A game is $(\lambda,\mu)$ -smooth if, for every two feasible profiles $A,A^*$ , the sum of the player costs after each player individually switches from $A_i$ to $A_i^*$ is at most $\lambda C(A^*)+\mu C(A)$ . The set $\mathcal A(\mathcal G(\mathcal C))$ consists of pairs with $\mu<1$ that satisfy this inequality for every game in the class. A related resourcewise set $\mathcal A(\mathcal C)$ asks, for every $c\in\mathcal C$ , current load $x\ge0$ , and comparison load $x^*\ge1$ , that

c(x+1)x^*\le\lambda c(x^*)x^*+\mu c(x)x.

Its best ratio is $\gamma(\mathcal C)=\inf_{(\lambda,\mu)\in\mathcal A(\mathcal C)}\lambda/(1-\mu)$ , with value $+\infty$ if there is no admissible pair. The bounded-load versions $\mathcal A(\mathcal C,n)$ and $\gamma(\mathcal C,n)$ use $0\le x\le n$ and $1\le x^*\le n$ . Roughgarden (2015), equations (34)–(36) and (41).

Formalization targets

Tightness of the congestion-game class

Theorem 5.8, in the form of equation (34), is the goal:

\sup_{G\in\mathcal G(\mathcal C)}\rho_{\mathrm{pure}}(G) =\inf_{(\lambda,\mu)\in\mathcal A(\mathcal G(\mathcal C))}\frac{\lambda}{1-\mu}.

It applies to every nonempty set $\mathcal C$ satisfying the standing cost-function conditions, whether finite, countable, or uncountable. Neither the number of players nor the number of resources is fixed. The equality is stronger than the routine upper bound from smoothness: it says that the best upper bound available from a uniform smoothness argument matches actual worst-case pure-equilibrium inefficiency. Roughgarden (2015), Theorem 5.8 and (34).

Resourcewise characterization

The paper also identifies the common value with $\gamma(\mathcal C)$ :

\sup_{G\in\mathcal G(\mathcal C)}\rho_{\mathrm{pure}}(G)=\gamma(\mathcal C).

The milestone list follows the paper's statements: the general upper bound; nonnegativity of $\mu$ ; passage from resource constraints to game smoothness; the bound for one game; the two finite optimization lemmas; the finite lower-bound theorem; the infinite-price boundary case; the countable case; and the characterization by $\gamma(\mathcal C)$ . The finite lower-bound target uses the one-sided conclusion established in the proof of Theorem 5.6. Roughgarden (2015), §§5.1–5.5.

Significance

The equality rules out a uniform improvement of the worst-case pure price-of-anarchy bound by using features of pure Nash equilibrium that a smoothness argument ignores. In this domain the broader applicability of smoothness does not force a worse class-wide bound. For a chosen cost-function family, the resourcewise characterization expresses that bound through explicit inequalities rather than a search over every possible finite game. Roughgarden (2015), §§2.4 and 5.5.

The result is proved in the paper. The remaining work here is a machine-checked proof of its formal statement and supporting theorems. The published congestion-game model supplies loads, player costs, feasible profiles, and pure Nash equilibria. The definitions of smoothness parameters and prices of anarchy built for this mission can also support later work on other cost-function classes and equilibrium bounds. The goal statement itself is a proof target, not an already verified result.

Difficulty

The smoothness inequality immediately gives an upper bound on equilibrium costs, but it does not by itself show that a game attains or approaches that bound. The difficult direction relates a small family of resourcewise constraints to actual games with inefficient equilibria. For finite positive cost-function sets, the optimum parameter value may be attained or may be approached only at infinity in parameter space; the two cases have different statements in Lemmas 5.3 and 5.5. The general theorem must also cover functions that vanish at a positive load, unbounded worst-case ratios, and sets of functions of arbitrary cardinality. Simply optimizing a bound for one fixed game would miss the supremum over the entire class. Roughgarden (2015), §§5.2–5.4.

Formalization scope

Lean represents players and resources by Fin k and Fin m and quantifies over every $k,m\in\mathbb N$ . A strategy is a finite resource subset, a strategy family is finite and nonempty, and all costs are real-valued at each load. The value $c(0)$ is unrestricted because it is unused in a player's cost and is multiplied by zero in (35). The all-zero function is excluded as in §5.1. Nonemptiness of $\mathcal C$ , stated at the start of that section, is carried into the finite optimization lemmas because their conclusions select functions from $\mathcal C$ . Zero-player and zero-resource games are allowed and do not raise the worst-case supremum.

Prices of anarchy and the values $\gamma$ are extended nonnegative reals. Thus an empty smoothness-parameter set has infimum $+\infty$ ; a positive equilibrium cost over zero optimum gives $+\infty$ ; and a game with no equilibrium contributes zero to the supremum. The paper's finite congestion games with nonempty strategy sets do have pure equilibria. The conversion of a real ratio $\lambda/(1-\mu)$ into this type does not truncate admissible class-wide ratios: if some cost function has $c(1)>0$ , a one-resource game forces the ratio to be at least one; if none does, the parameter set is empty. Smoothness and optimum quantify over feasible profiles only. These choices prevent the equality from becoming vacuous through an empty real infimum, total division by zero, or a supremum over a fixed small game size.

The complete development needs finite-set sums, function updates, extended nonnegative infima and suprema, and the published congestion-game definitions. Reusable contributions include lemmas about the resourcewise parameter sets and their relation to game smoothness. The paper's uncountable approximation paragraph has a gap for flat cost functions; the theorem remains the stated target, and a formal proof may use a different argument at that stage. Roughgarden (2015), pp. 31–32.

Selected references

Tim Roughgarden, Intrinsic Robustness of the Price of Anarchy, Journal of the ACM 62(5), Article 32, 2015. DOI. The source used here is the author's final version dated July 14, 2015; the cited page numbers are its printed pages.

13 thms2 active usersReviewed

Bandit Algorithms Machine Learning Statistics·Captain: mikedeng1

Explore First, Exploit Next: The True Shape of Regret in Bandit Problems III: A Strategy Smarter Than Uniform Draws Every Arm at Least (T/K)(1 − √(2T K_inf)) TimesResearch Paper

Why early exploration needs a lower bound

A stochastic multi-armed bandit learner repeatedly selects one of finitely many arms and sees only the reward from the selected arm. The learner must gather information about uncertain rewards while trying to select high-mean arms. Expected regret summarizes the lost reward relative to always selecting an optimal arm, but regret alone does not explain how much sampling each particular arm must receive. Garivier, Ménard, and Stoltz study this allocation question directly in Explore First, Exploit Next: The True Shape of Regret in Bandit Problems. Their Section 3 gives lower bounds for small horizons, before the longer-run logarithmic behavior becomes dominant.

The paper's first small-horizon result concerns strategies that allocate at least a uniform share to every optimal arm, on every problem in a specified model. This requirement excludes a strategy that always selects one fixed label and succeeds only when that label happens to be best. Such a requirement still permits many adaptive policies; it constrains their performance on optimal arms rather than prescribing their decisions round by round. The result establishes a compulsory initial allocation to every arm, including one whose mean is below the best mean. It is Theorem 2 on page 10 of the pinned arXiv:1602.07182v3.

Bandit problems, models, and strategies

A bandit problem $\underline\nu=(\nu_a)_{a=1}^K$ consists of $K$ probability laws on $\mathbb R$ . At each round, a strategy $\psi$ chooses an arm using the observed past and randomization, then receives an independent reward drawn from that arm's law. The mean reward of arm $a$ is $\mu_a=\mathbb E_{\nu_a}[X]$ . Write $\mu^*=\max_a\mu_a$ , and call an arm optimal when $\mu_a=\mu^*$ . The count $N_{\psi,a}(T)$ is the number of times arm $a$ is chosen during the first $T$ rounds. These objects and the information available to a strategy are specified in Section 1.1, pages 2–3.

A model $\mathcal D$ is a collection of possible arm laws, each a probability measure with an expectation. The notation $\underline\nu\in\mathcal D$ means that every arm law $\nu_a$ belongs to $\mathcal D$ . A strategy is smarter than uniform on $\mathcal D$ when, for every bandit problem in the model, every optimal arm $a^*$ , and every integer $T\ge1$ , it satisfies

\mathbb E_{\underline\nu}[N_{\psi,a^*}(T)]\ge\frac{T}{K}.

This is Definition 2 on page 10. It imposes a lower bound on each optimal arm, even when several arms tie. The requirement is evaluated across the whole model, so a strategy cannot be declared smarter based only on its behavior on the one problem used in the theorem.

For a law $P$ , a real threshold $x$ , and the model $\mathcal D$ , the information number $\mathcal K_{\inf}(P,x,\mathcal D)$ is the infimum of $\mathrm{KL}(P,Q)$ over those $Q\in\mathcal D$ whose mean exceeds $x$ . The infimum is $+\infty$ if there is no such $Q$ . This is the definition on page 4. It measures how close an arm law is, in Kullback–Leibler divergence, to another admissible law that would give it a mean above the present optimum.

Formalization targets

The main target is Theorem 2. For a model $\mathcal D$ , a strategy $\psi$ smarter than uniform on it, a bandit problem $\underline\nu\in\mathcal D$ , every arm $a$ , and every integer $T\ge1$ , the finite- $\mathcal K_{\inf}$ case states

\mathbb E_{\underline\nu}[N_{\psi,a}(T)]\ge \frac{T}{K}\left(1-\sqrt{2T\mathcal K_{\inf}(\nu_a,\mu^*,\mathcal D)}\right).

The theorem includes optimal and suboptimal arms. Its printed companion says that when $T\le 1/(8\mathcal K_{\inf})$ , the arm receives at least $T/(2K)$ expected selections. In the formal statement this threshold is $8T\mathcal K_{\inf}\le1$ , which also expresses the intended case $\mathcal K_{\inf}=0$ . Both claims come from Theorem 2, page 10.

The milestone list follows the source's intermediate claims. Lemma 6, page 20 bounds Bernoulli relative entropy using the maximum of $x(1-x)$ over an interval. The proof of Theorem 2 on page 11 states that Bernoulli relative entropy increases in its second argument on the interval starting at its first argument. The same page applies the paper's fundamental inequality (6) to the fraction of rounds spent on one arm, then states a lower bound against a single alternative arm law. These are the four curated milestones for the main theorem.

What the result supplies

The theorem turns a model-relative performance condition into a numerical constraint on early sampling. If an arm's law is close in divergence to a law that would make it best, then the bound keeps its expected pull count near the uniform allocation until the horizon is large enough for the term under the square root to matter. It identifies the divergence scale $1/\mathcal K_{\inf}$ at which this particular guarantee becomes weak. The paper contrasts this absolute bound with later relative and collective bounds that capture different dependencies on the number of arms in Section 3, pages 10–14.

The mathematical result is proved in the paper. The remaining work in this mission is a machine-checked development of the statement and its source-backed intermediate inequalities in the canonical stochastic-bandit model. The published bandit structure, policy kernels, and information number provide reusable foundations. Shared definitions supply the Bernoulli divergence, model predicate, and expected pull counts; the local strategy class makes the hypothesis of this particular theorem explicit. The Bernoulli inequalities and the pull-count change-of-measure statement can be reused in other lower-bound results.

Where the difficulty lies

A performance condition about optimal arms does not directly constrain an arm that is suboptimal in the problem of interest. The small-horizon bound must remain valid even though the strategy may adapt to observed rewards, and the relevant alternative arm laws can have divergences approaching an infimum without attaining it. The paper's lower bound is therefore sensitive to the exact orientation of the two bandit problems, the expected count multiplying their divergence, and the boundary conventions for Bernoulli relative entropy. Replacing the infimum with a chosen alternative or changing a divergence to an ordinary real with an arbitrary boundary value would alter the statement.

Formalization scope

Lean uses arms Fin K, indexed from zero; the paper indexes them from one. The horizon is a natural number, and counts are integrated against the probability measure on $T$ -round histories generated by a stochastic kernel policy. Such kernels represent the arm-and-reward histories induced by the paper's strategies with auxiliary randomization. The model is a set of probability measures on $\mathbb R$ whose identity function is integrable. The published StochasticBandit, BanditPolicy, and ConsistentBanditPolicy definitions supply the basic problem, history measure, pull count, means, and $\mathcal K_{\inf}$ .

Bernoulli divergence and $\mathcal K_{\inf}$ take values in $[0,+\infty]$ . The real square-root formula assumes $\mathcal K_{\inf}<+\infty$ : when it is infinite, the paper's right-hand side is $-\infty$ , while converting infinity directly to Lean's real value would produce a false numerical bound. The starting bandit problem is explicitly in $\mathcal D$ , a condition needed for the proof's use of Definition 2 on a one-arm modification, although the printed quantifier on page 10 omits it. The arm parameter guarantees $K\ge1$ ; every target assumes $T\ge1$ , so its real divisions by $K$ and $T$ have the stated meaning.

A faithful development must retain Definition 2's quantification over all model problems and each optimal arm, rather than only over the bandit problem used in the conclusion. It must use the full Bernoulli relative entropy, including infinite endpoint values, and the infimum over precisely those model laws with mean greater than $\mu^*$ . The local instance of (6) also assumes integrable arm rewards in both bandit problems, as Section 1.1 requires. Contributions that establish the four milestones, the companion threshold claim, or reusable count-integrability and divergence facts are in scope.

Selected references

Aurélien Garivier, Pierre Ménard, and Gilles Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research, 2019; arXiv:1602.07182v3.
Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, Cambridge University Press, 2020; DOI:10.1017/9781108571401. The published bandit definitions used here follow its canonical framework.

11 thms2 active usersReviewed

Bandit Algorithms Machine Learning Statistics·Captain: mikedeng1

Explore First, Exploit Next: The True Shape of Regret in Bandit Problems IV: Under Pairwise Symmetry a Suboptimal Arm Is Drawn T/K Times or Almost as Often as an Optimal ArmResearch Paper

Motivation

Lower bounds for stochastic multi-armed bandits are usually stated for a large horizon: Lai and Robbins (1985) and Burnetas and Katehakis (1996) show that a consistent strategy pulls a suboptimal arm at least about $\ln T / \mathcal{K}_{\inf}$ times. These bounds say nothing about the small-horizon regime, the first rounds in which a strategy has not yet had time to separate the arms. Garivier, Ménard and Stoltz (arXiv:1602.07182v3, Mathematics of Operations Research, 2019) describe that regime through one information-theoretic inequality, their (6), and derive several lower bounds from it. This mission formalizes their relative lower bound, Theorem 3 (p. 11): under a mild symmetry assumption on the strategy, a suboptimal arm is either pulled at the uniform rate $T/K$ or, on average, almost as often as an optimal arm. It is the statement behind the title's claim that bandit strategies must first explore.

Setting

There are $K$ arms. A bandit problem $\underline{\nu} = (\nu_1, \dots, \nu_K)$ assigns to each arm $a$ a probability distribution $\nu_a$ on $\mathbb{R}$ with expectation $\mu_a$ . The optimal mean is $\mu^\star = \max_a \mu_a$ , the gap of arm $a$ is $\Delta_a = \mu^\star - \mu_a$ ; arm $a$ is optimal if $\Delta_a = 0$ and suboptimal if $\Delta_a > 0$ .

A model $\mathcal{D}$ is a set of distributions on $\mathbb{R}$ , each with an expectation; a bandit problem is in $\mathcal{D}$ when every $\nu_a$ belongs to $\mathcal{D}$ .

At each round $t$ a strategy $\psi$ picks an arm $A_t$ , possibly at random, as a function of the past arms and rewards, and receives a reward $Y_t$ drawn from $\nu_{A_t}$ . The number of pulls of arm $a$ in the first $T$ rounds is

N_{\psi,a}(T) = \sum_{t=1}^{T} \mathbb{1}\{A_t = a\},

and $\mathbb{E}_{\underline{\nu}}$ denotes expectation when $\psi$ plays against $\underline{\nu}$ . Write $N^+_{\psi,a}(T) = \max\{N_{\psi,a}(T), 1\}$ .

Kullback–Leibler divergence. $\mathrm{KL}(P, Q) \in [0, +\infty]$ is the Kullback–Leibler divergence between distributions, and $\mathrm{kl}(p, q)$ the divergence between Bernoulli laws of parameters $p$ and $q$ .

Pairwise symmetry (Definition 3, p. 11). A strategy $\psi$ is pairwise symmetric for optimal arms on $\mathcal{D}$ if for every bandit problem $\underline{\nu}$ in $\mathcal{D}$ , every pair of optimal arms $a^\star, a_\star$ with $\nu_{a^\star} = \nu_{a_\star}$ and every $T \ge 1$ , the pairs $(N_{\psi,a^\star}(T), N_{\psi,a_\star}(T))$ and $(N_{\psi,a_\star}(T), N_{\psi,a^\star}(T))$ have the same distribution. A strategy that uses only the observed payoffs, and not the labels of the arms, has this property.

Formalization targets

Goal: Theorem 3 (p. 11)

For every model $\mathcal{D}$ , every strategy $\psi$ pairwise symmetric for optimal arms on $\mathcal{D}$ , every bandit problem $\underline{\nu}$ in $\mathcal{D}$ , every suboptimal arm $a$ , every optimal arm $a^\star$ with $\mathrm{KL}(\nu_a, \nu_{a^\star}) < \infty$ and every $T \ge 1$ ,

\mathbb{E}_{\underline{\nu}}\big[N_{\psi,a}(T)\big] \ge \frac{T}{K} \quad\text{or}\quad \mathbb{E}_{\underline{\nu}}\left[\frac{N^+_{\psi,a}(T)}{N^+_{\psi,a^\star}(T)}\right] \ge 1 - 2\sqrt{\frac{2T\,\mathrm{KL}(\nu_a, \nu_{a^\star})}{K}} .

Companion: the "in particular" clause

For $T \le K / (32\,\mathrm{KL}(\nu_a, \nu_{a^\star}))$ the second alternative becomes $\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}(T)/N^+_{\psi,a^\star}(T)] \ge 1/2$ .

Milestones (p. 12)

The symmetry identity: for the alternative problem $\underline{\nu}'$ obtained by replacing $\nu_a$ by $\nu_{a^\star}$ , $\mathbb{E}_{\underline{\nu}'}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})] = 1/2$ .
Inequality (12): $\mathbb{E}_{\underline{\nu}}[N_{\psi,a}(T)]\,\mathrm{KL}(\nu_a, \nu'_a) \ge \mathrm{kl}\big(\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})], 1/2\big)$ .
The Jensen display: $\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})] \le r/(1+r)$ with $r = \mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/N^+_{\psi,a^\star}]$ .
The bound $r/(1+r) \ge 1/2 - \sqrt{T\,\mathrm{KL}(\nu_a,\nu'_a)/(2K)}$ in the case $\mathbb{E}_{\underline{\nu}}[N_{\psi,a}(T)] \le T/K$ , $r \le 1$ .

Significance

The theorem shows that in the initial phase a symmetric strategy cannot discard a suboptimal arm quickly: unless the arm is already sampled at the uniform rate, it is sampled, in ratio, nearly as often as an optimal arm, as long as $T$ is small compared with $K / \mathrm{KL}(\nu_a, \nu_{a^\star})$ . Together with Theorem 2 (absolute lower bound) and Theorem 4 (collective lower bound) it describes the regret curve before the logarithmic regime: roughly linear growth, then a transition. It requires no assumption on the model beyond the existence of expectations, and it involves the divergence between the two arms themselves rather than the model-dependent quantity $\mathcal{K}_{\inf}$ .

The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a Lean statement of Theorem 3 on the canonical bandit model already used on the platform (StochasticBandit, BanditPolicy), a formal version of the symmetry assumption that sibling missions reuse (mission V, the collective lower bound, uses the same Definition 3), and the four intermediate steps of the proof as separate targets.

Difficulty

The proof compares $\underline{\nu}$ with an alternative problem $\underline{\nu}'$ that differs from it only in arm $a$ , and transfers information between them through the fundamental inequality (6) of §2, a data-processing argument on the law of the whole history. The step specific to Theorem 3 is the choice of the test variable: the expectation of $N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})$ is known exactly under $\underline{\nu}'$ only because the strategy is pairwise symmetric, and the symmetry is a statement about joint laws of pull counts, not about their expectations. A version of the assumption that only equates expected pull counts does not determine the expectation of this ratio. The ratio expectation then has to be extracted from a bound on $\mathbb{E}[x/(1+x)]$ , which needs Jensen's inequality in the right direction and a case split on whether $r \le 1$ .

Formalization scope

Arms are Fin K (0-based). The horizon $T$ is a natural number. A strategy is a published BanditPolicy: a family of Markov kernels from the observed history of (arm, reward) pairs to the next arm. Every strategy of the paper, which may use auxiliary uniform random variables, induces such a kernel with the same law of arms and rewards. The law of the history is the published banditMeasure, and $N_{\psi,a}(T)$ is the published armPullCount. The model is a set of measures on $\mathbb{R}$ , and every statement assumes the paper's standing hypothesis (§1.1, p. 3) that each member is a probability measure with an integrable identity, together with $\underline{\nu}$ in $\mathcal{D}$ .

Committed conventions:

$\mathrm{KL}$ and $\mathrm{kl}$ take values in $[0, +\infty]$ ; the Bernoulli divergence is the Kullback–Leibler divergence of two Bernoulli laws on $\mathbb{R}$ , not a real formula with finite values at $q \in \{0, 1\}$ .
Theorem 3 adds the hypothesis $\mathrm{KL}(\nu_a, \nu_{a^\star}) < \infty$ . When the divergence is infinite the paper's bound reads $\ge -\infty$ and is empty; reading $+\infty$ as the real number $0$ would make the statement false.
The "in particular" clause is stated as $32\,T\,\mathrm{KL}(\nu_a,\nu_{a^\star}) \le K$ in $[0, +\infty]$ , which needs no finiteness assumption.
Definition 3 is an equality of joint laws (push-forwards of the history law), for every $T \ge 1$ , only for optimal arms of problems in $\mathcal{D}$ with equal distributions. Invariance under all permutations of the arms would strengthen the hypothesis and weaken the theorem.
Ratios use $\max\{N, 1\}$ as real numbers, so no division by zero occurs; all integrands are bounded by $T$ .

A formalization in which the symmetry assumption equates only expected pull counts, in which the divergence is a real number with junk value $0$ at $+\infty$ , or in which the disjunction is replaced by its second alternative, is not this theorem.

The mission builds on the published definitions StochasticBandit and BanditPolicy. A complete development needs the fundamental inequality (6) for kernel policies (the divergence decomposition, published as BanditAlgorithm.bandit_divergence_decomposition, plus data processing for the Bernoulli test), Pinsker's inequality for Bernoulli laws (proved on the platform as BanditAlgorithm.bernoulli_relative_entropy_pinsker), Jensen's inequality for concave functions (Mathlib), and a lemma that the law of the history is unchanged in distribution when two identically distributed optimal arms are relabelled. The measurability of pull counts and the relation between the extended-real and real Bernoulli divergences are reusable beyond this mission. Proofs of any milestone, and of the general fundamental inequality, are welcome.

Selected references

A. Garivier, P. Ménard, G. Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research 44(2), 2019. arXiv:1602.07182v3, doi:10.1287/moor.2017.0928
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6(1), 1985. doi:10.1016/0196-8858(85)90002-8
A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Advances in Applied Mathematics 17(2), 1996. doi:10.1006/aama.1996.0007
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. doi:10.1017/9781108571401

8 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Probability·Captain: mikedeng1

Approximate Revenue Maximization with Multiple Items 2: Selling Two I.I.D. Goods Separately Guarantees at Least e/(e + 1) ≈ 73% of the Optimal RevenueResearch Paper

Motivation

A seller with several goods can sell them one at a time or offer a mechanism that links allocation and payment across goods. Separate selling asks the seller to solve a one-good pricing problem for each item. A general mechanism can offer lotteries and menus whose outcomes depend on the buyer's whole valuation vector. The difference matters because the buyer's private information covers several values at once, and an optimal multidimensional mechanism need not resemble an ordinary posted price. Hart and Nisan ask how much revenue is guaranteed by simple selling rules when the joint valuation distribution is unrestricted apart from the stated independence assumptions (Hart and Nisan, arXiv:1204.1846v3).

This mission isolates their two-good, identically distributed result, Theorem B. The paper first gives a one-half guarantee for two independent goods with potentially different distributions, then improves the guarantee to $e/(e+1)$ when their distributions agree. The improvement is a claim about every probability law on nonnegative values. It assumes neither a density nor a regularity condition on the tail of that law. The paper proves the result in Appendix A.1 after stating it in the introduction (Hart and Nisan, pp. 6 and 31–35).

Setting

There is one risk-neutral buyer and one seller. For two goods, the buyer's private valuation is a vector $(Y,Z)$ with $Y,Z\ge0$ . Values are additive: receiving both goods is worth $Y+Z$ . The seller knows the distribution of the vector but not the realized values. In this mission, $Y$ and $Z$ are independent and have the same arbitrary probability law $\nu$ on $\mathbb R_{\ge0}$ . A law, rather than a named pair of random variables on a probability space, carries all the data needed by the revenue quantities.

A direct mechanism $\mu=(q,s)$ takes a reported pair $x=(y,z)$ and returns an allocation probability $q_i(x)\in[0,1]$ for each good and a real payment $s(x)$ to the seller. The buyer's payoff from reporting truthfully is $b(x)=q(x)\cdot x-s(x)$ . The mechanism is incentive compatible (IC) if truthful reporting is at least as good as any other report for every possible valuation, and individually rational (IR) if truthful payoff is nonnegative everywhere. These requirements hold on the whole nonnegative orthant, as in Section 2.1 of the paper (Hart and Nisan, pp. 11–14).

Write $R(\mu;X)$ for the expected payment under a valuation law $X$ and $\operatorname{Rev}(X)$ for the supremum of $R(\mu;X)$ over feasible, IC, IR mechanisms. For one good, write $\operatorname{Rev}_1(\nu)$ . The separate-selling revenue for two identically distributed goods is $\operatorname{SRev}(Y,Z)=2\operatorname{Rev}_1(\nu)$ . Equation (1) of the paper identifies the one-good value with the supremum of posted-price revenue $p\Pr[Y\ge p]$ ; the supremum formulation covers laws for which no maximizing price exists (Hart and Nisan, p. 12; Myerson, 1981).

Formalization targets

Theorem B: the guarantee for two i.i.d. goods

The goal is the exact upper bound written at the start of the paper's proof:

\operatorname{Rev}(Y,Z)\le\frac{e+1}{e}\bigl(\operatorname{Rev}(Y)+\operatorname{Rev}(Z)\bigr)=\frac{e+1}{e}\operatorname{SRev}(Y,Z).

Equivalently, separate selling guarantees at least $e/(e+1)$ of optimal revenue whenever the ratio has an ordinary meaning. The inequality itself is the stable formulation at zero and infinite revenues. The formal goal uses the exact constant $(e+1)/e$ , not the rounded percentage in the theorem's prose (Hart and Nisan, Theorem B, p. 6; proof, p. 31).

Supporting targets

The milestones include the one-good posted-price identity, the fact that nonnegative payments suffice when optimizing, symmetrization for identical independent goods, Lemma 19's lower-valuation revenue bound, equation (12), and the two expectation estimates and final numerical bound used after it. Proposition 5's IC characterization is also a draft theorem, though it is not a milestone. Each statement retains its source's domain and the constant $1/e$ . The final inequality for the right side of (12) is stated for every nondecreasing allocation function into $[0,1]$ , as required by the paper's argument on pp. 33–35.

Significance

Theorem B gives a distribution-free quantitative guarantee for an easy-to-describe selling rule in a setting where the optimal rule may depend on the buyer's entire two-dimensional private type. Its $e/(e+1)$ guarantee is stronger than the one-half guarantee for merely independent goods stated as Theorem A. The conclusion concerns the best revenue available from all feasible IC and IR mechanisms, so the benchmark includes randomized allocations and payments depending on both reported values (Hart and Nisan, pp. 6 and 11–13).

The formalization target is a machine-checked version of a proved result, not a new conjecture. The proposal currently contains compiled Lean statements with unproved theorem bodies. A completed development would prove the stated inequality and its selected supporting results. It would also supply reusable definitions for direct mechanisms with additive nonnegative values, extended-real revenue, optimal revenue as a supremum, and symmetry of two-good mechanisms. No machine-checked proof of these proposed Hart–Nisan statements is claimed here.

Difficulty

The one-good posted-price formula does not directly control an arbitrary two-good mechanism: allocation of either good and the payment can depend on both reported values. Applying a one-good bound separately to the two coordinates therefore leaves terms that depend on the other coordinate. In particular, a direct comparison between each marginal posted-price optimum and the total payment loses the improved constant. The proof has to control the dependence created by a joint mechanism while retaining the exact $1/e$ numerical estimate. A second formal difficulty is that an admissible mechanism can have a negative expected payment even though optimal revenue is nonnegative, while an unrestricted law can give infinite optimal revenue. Replacing every expectation by an ordinary real integral or clipping each mechanism's revenue would change Lemma 19 and the intermediate inequalities (Hart and Nisan, pp. 31–35).

Formalization scope

Valuations are finite vectors $\iota\to\mathbb R_{\ge0}$ ; the main theorem fixes $\iota=\operatorname{Fin}(2)$ . The two-good law is the product of the same one-good probability measure in both coordinates, so independence and identical distribution are built into the data. The model represents allocation probabilities as real numbers with explicit bounds $0\le q_i\le1$ . It requires IC and IR pointwise on all reports. No positive transfer (NPT) means $s(x)\ge0$ and is imposed only on supporting statements where the paper uses it. Following the paper's footnote 12, admissibility also requires the payment function to be measurable.

An individual expected payment is an extended real difference of positive and negative Lebesgue integrals. For IC mechanisms, the negative part is finite because the payment is bounded below by its value at zero. Optimal revenue is the supremum of the nonnegative clips of admissible mechanisms' expected payments; the zero mechanism makes this the same supremum as in the paper. Lemma 19 and equation (12) keep individual revenue in the extended reals. Supporting inequalities that write $r=\operatorname{Rev}_1(\nu)$ as a real number explicitly assume $r<\infty$ ; Theorem B does not. Integrals of bounded threshold functions use ordinary real expectation, while the nonnegative term $W$ uses a nonnegative Lebesgue integral. The goal cannot be satisfied by a correlated joint law, a bounded-support special case, a vacuous assumption on $\nu$ , or a rounded constant.

The reusable work includes one-good posted-price revenue for arbitrary laws, a nonnegative-transfer reduction, a faithful single-mechanism revenue type, and probability identities for two independent coordinates. Theorem A, Theorem 7, Theorem 16, and a full formalization of the paper's other selling rules are outside this mission.

Selected references

Sergiu Hart and Noam Nisan, Approximate Revenue Maximization with Multiple Items, Journal of Economic Theory, 2017. Source used here: arXiv:1204.1846v3.
Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. DOI:10.1287/moor.6.1.58.

11 thms2 active usersReviewed

Bandit Algorithms Machine Learning Statistics·Captain: mikedeng1

Explore First, Exploit Next: The True Shape of Regret in Bandit Problems II: Uniformly Fast Convergent Strategies Draw Every Suboptimal Arm at Least ln T / K_inf Times AsymptoticallyResearch Paper

Why this lower bound matters

In a stochastic multi-armed bandit, a player repeatedly chooses one of finitely many arms and sees only the reward from the chosen arm. To earn a high reward, the player must favor arms that appear best. Yet an arm that currently appears inferior might be best under another plausible reward law. That uncertainty forces any strategy with uniformly strong long-run performance to keep testing apparently inferior arms. The asymptotic number of tests is a basic benchmark for comparing bandit algorithms: an algorithm that matches the bound uses no more exploration than the information in the model demands. Garivier, Ménard, and Stoltz restate this general benchmark as Theorem 1 and derive it within their analysis of the shape of regret Garivier–Ménard–Stoltz, §2.2.

The quantity controlling the benchmark comes from Burnetas and Katehakis. It measures the least information needed to replace one suboptimal arm by a plausible arm that is strictly better than the current best. The paper cites their quantity on page 4, and its Theorem 1 applies it to every suboptimal arm separately Garivier–Ménard–Stoltz, pp. 4, 9. This per-arm form matters when different arms have different reward laws and different amounts of information are needed to rule them out.

Bandit setting and notation

A bandit problem $\underline\nu=(\nu_a)_{a=1}^K$ has $K$ arms. Each $\nu_a$ is a probability distribution on real rewards with a finite expectation $\mu_a=\mathbb E_{\nu_a}X$ . A strategy $\psi$ chooses an arm at each round using the preceding chosen arms and observed rewards, and it may randomize. Let $N_{\psi,a}(T)$ be the number of times arm $a$ is chosen in the first $T$ rounds. The optimal mean is $\mu^\star=\max_a\mu_a$ , and the gap of arm $a$ is $\Delta_a=\mu^\star-\mu_a$ . An arm is suboptimal when $\Delta_a>0$ . These are the objects of §1.1 of the paper Garivier–Ménard–Stoltz, pp. 2–3.

A model $\mathcal D$ is a collection of possible real-valued reward distributions, each with a finite expectation. A bandit problem belongs to $\mathcal D$ when every one of its arm laws does. The Kullback–Leibler divergence $\mathrm{KL}(P,Q)$ measures the information discrepancy from one reward law $P$ to another $Q$ ; it may be infinite. For an arm law $P$ and a real threshold $x$ , define the minimal information cost

\mathcal K_{\inf}(P,x,\mathcal D) =\inf\{\mathrm{KL}(P,Q):Q\in\mathcal D,\ \mathbb E_QX>x\}.

The infimum is $+\infty$ if there is no qualifying alternative. The strict inequality in the set matters: the replacement law must make the arm better than the original optimal mean, not merely tied with it Garivier–Ménard–Stoltz, p. 4.

Definition 1 calls $\psi$ uniformly fast convergent on $\mathcal D$ when, on every bandit problem in the model, the expected draw count of every suboptimal arm grows more slowly than $T^\alpha$ for each $0<\alpha\le1$ :

\mathbb E_{\underline\nu}N_{\psi,a}(T)=o(T^\alpha).

Here $T$ tends to infinity through integer horizons. This condition is uniform in which problem and suboptimal arm are considered; it does not mean one numerical convergence rate is shared by all problems Garivier–Ménard–Stoltz, p. 9, Definition 1.

Formalization target

The goal is the paper's Theorem 1: for every model $\mathcal D$ , every uniformly fast convergent strategy $\psi$ , every bandit problem $\underline\nu$ in the model, and every suboptimal arm $a$ ,

\liminf_{T\to\infty} \frac{\mathbb E_{\underline\nu}N_{\psi,a}(T)}{\ln T} \ge\frac1{\mathcal K_{\inf}(\nu_a,\mu^\star,\mathcal D)}.

The bound states the minimum logarithmic exploration of each arm. It leaves the model and strategy arbitrary within the stated class. The milestones follow four statements from the proof on page 9: the Bernoulli entropy estimate in (11), the one-arm divergence chain in (10), the eventual bound on draws of the alternative's other arms, and the bound for one alternative law before taking the infimum. Their source text is recorded beside the local drafts Garivier–Ménard–Stoltz, p. 9.

What the result gives

If $\mathcal K_{\inf}$ is finite and positive, the theorem gives a concrete coefficient of $\ln T$ that any uniformly fast convergent strategy must spend on arm $a$ . A small information cost means that the arm is hard to distinguish from a better alternative and must be sampled more often. If the cost is infinite because the model contains no better replacement, the reciprocal is zero and the bound makes no positive demand. If the cost is zero, the reciprocal is infinite: the normalized expected draw count must diverge. The extended-value convention is part of the target, not a choice of a finite stand-in Garivier–Ménard–Stoltz, pp. 4, 9.

The theorem is proved in the paper, while the Lean statements in this proposal are proof targets. A completed development would supply a machine-checked bridge from the canonical stochastic-bandit policy model through Bernoulli relative entropy and change of measure to the per-arm asymptotic claim. Its model and divergence definitions can also support lower bounds for other bandit classes. The existing Prove2Me StochasticBandit, BanditPolicy, and ConsistentBanditPolicy definitions provide the bandit law, policy, draw count, means, and $\mathcal K_{\inf}$ used here; Definition 1's exact strategy class is supplied locally.

Difficulty

The central issue is the quantification over every alternative law in an arbitrary model. A suboptimal arm may become uniquely optimal after changing only its law, while the strategy must remain uniformly fast on that new problem. The information cost is an infimum over such changes, including an empty set or costs arbitrarily close to zero. A statement that reasons about just one convenient alternative does not yield the coefficient in Theorem 1. The proof also passes from finite-horizon information inequalities to a liminf as $T$ grows, so endpoint values of Bernoulli divergence and the extended-value arithmetic must agree with the source Garivier–Ménard–Stoltz, pp. 6, 9.

Formalization scope

Lean indexes the paper's arms $1,\ldots,K$ by Fin K, starting at zero, and uses natural-number horizons. A strategy is a history-dependent Markov kernel, whose generated probability measure describes the sequence of chosen arms and rewards. The pull count is bounded by $T$ , so its expectation is a genuine Bochner integral. The model explicitly requires probability laws with integrable identity; this ensures that each mean in $\mathcal K_{\inf}$ is genuine. Bernoulli relative entropy and arm-law KL take values in extended nonnegative reals. The goal's liminf is also in extended nonnegative reals, avoiding a default real liminf for an unbounded sequence. The first two horizons, where $\ln T\le0$ , cannot affect an asymptotic liminf.

The theorem sentence on page 9 says “all bandit problems” without restricting the original problem to $\mathcal D$ . Its proof applies Definition 1 to that problem, so the proposal states that its arms belong to $\mathcal D$ . Without this condition a strategy can behave arbitrarily outside the model. The source's other standing conventions are kept: every reward law has an expectation, the improvement condition in $\mathcal K_{\inf}$ is strict, and uniform fast convergence ranges over all model problems, all suboptimal arms, and all $0<\alpha\le1$ . These choices rule out an empty strategy class or a special hard-coded bandit as a trivial route to the target.

Useful contributions include the finite-horizon change-of-measure inequality, endpoint-correct Bernoulli KL estimates, identities for sums of expected pull counts, and asymptotic lemmas for reciprocal infima. The milestone drafts identify the paper statements those contributions must support.

Selected references

Aurélien Garivier, Pierre Ménard, and Gilles Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research, 2019; cited here from arXiv:1602.07182v3, §§1–2.
Apostolos N. Burnetas and Michael N. Katehakis, Optimal Adaptive Policies for Sequential Allocation Problems, Advances in Applied Mathematics, 1996. DOI:10.1006/aama.1996.0007.

9 thms2 active usersReviewed

Combinatorics Optimization Probability·Captain: mikedeng1

Online Contention Resolution Schemes with Applications to Bayesian Selection Problems 2: The Degree Relaxation of Matching Has a (b, e^(−2b))-Selectable Randomized Greedy OCRSResearch Paper

Why online matching needs a stronger rounding guarantee

In online selection, candidate items reveal themselves one at a time and an algorithm must decide immediately whether to keep each one. When the kept items must form a matching, accepting one edge can prevent a later edge sharing an endpoint from being accepted. A fractional solution supplies useful marginal probabilities, but it does not by itself specify which active edges can be kept under an unfavorable arrival order. Online contention resolution schemes provide that missing rounding step: they turn independent edge activity into a feasible online selection while guaranteeing each edge a chance of selection. Feldman, Svensson, and Zenklusen introduced the strong selectability guarantee used here, which protects an edge even against an arrival order chosen with knowledge of all random outcomes (Feldman–Svensson–Zenklusen, §1.1).

This mission isolates the matching result of their paper. It concerns a degree relaxation that is weaker than the full matching polytope, so the result applies even when the input fractional point satisfies only local vertex constraints. The source states the existence theorem as Theorem 2.7 and gives its numerical guarantee explicitly (Theorem 2.7, p. 13).

Finite graphs, fractional edges, and greedy families

Let $G=(V,E)$ be a finite graph. An edge $g$ has two distinct endpoints; multiple edges may have the same endpoints. A matching is a set of edges with no shared vertex. For a vertex $u$ , write $\delta(u)$ for its incident edges. The degree relaxation is

P_G=\left\{x\in\mathbb R_{\ge0}^{E}:\sum_{g\in\delta(u)}x_g\le1\text{ for every }u\in V\right\}.

Since each edge meets a vertex, these constraints also give $x_g\le1$ . Every matching has a characteristic vector in $P_G$ . The degree relaxation can contain points outside the convex hull of matchings, which makes the theorem stronger than a statement restricted to the matching polytope (§2.2, p. 13).

For $x\in[0,1]^E$ , the active set $R(x)$ includes each edge $g$ independently with probability $x_g$ . A greedy family $\mathcal F_x$ is a downward closed family of matchings containing the empty set. A greedy online scheme accepts an active edge if adding it to the already accepted set remains in $\mathcal F_x$ . The family may itself be random, sampled independently of $R(x)$ .

An edge $g$ is selectable for a realized active set and greedy family when every member $I\in\mathcal F_x$ with $I\subseteq R(x)$ can be extended by $g$ while staying in $\mathcal F_x$ . Thus selectability promises acceptance regardless of which eligible active edges preceded $g$ . A scheme is $(b,c)$ -selectable if this event has probability at least $c$ for every $x\in bP_G$ and every edge. The probability includes both the active-set draw and any random family draw (Definitions 1.3–1.5, pp. 3–4).

Formalization targets

Theorem 2.7: a randomized matching scheme

For every $b\in[0,1]$ and every finite loopless graph $G$ ,

\exists\text{ a randomized greedy scheme for }P_G\text{ that is }(b,e^{-2b})\text{-selectable}.

Equivalently, for each $x\in bP_G$ and each edge $g\in E$ , the probability that $g$ is selectable is at least $e^{-2b}$ . The statement includes edges with $x_g=0$ ; the selectability event concerns the ability to add an edge, rather than the probability that it becomes active. The milestones are the steps the source states in its proof, in attack order (proof of Theorem 2.7, pp. 13–14):

for $t>0$ , $0\le(1-e^{-t})/t\le1$ , so that an edge can be put into a random set $K$ of potential edges with probability $(1-e^{-x_g})/x_g$ ;
drawing $K$ this way and using the matchings inside $K$ as the family is a randomized greedy scheme;
an edge $g'$ with ends $u,v$ is selectable exactly when $g'\in K$ and $A\cap K\cap(\delta(u)\cup\delta(v)\setminus\{g'\})=\varnothing$ ;
the probability of that event equals $\frac{1-e^{-x_{g'}}}{x_{g'}}\,e^{-\sum_{g\in\delta(u)\cup\delta(v)\setminus\{g'\}}x_g}$ ;
for $x\in bP_G$ , $\sum_{g\in\delta(u)\cup\delta(v)\setminus\{g'\}}x_g\le2(b-x_{g'})$ ;
for $t>0$ , $e^{t}(e^{t}-1)/t\ge1$ .

Remark (p. 14): the deterministic variant

Taking $K=E$ , the deterministic greedy scheme whose family is the set of all matchings is $(b,(1-b)^2)$ -selectable for $P_G$ , $b\in[0,1]$ :

\Pr_{A\sim R(x)}\big[g\text{ is selectable for }A\big]\ \ge\ (1-b)^2\qquad\forall x\in bP_G,\ \forall g\in E.

This companion is weaker than Theorem 2.7 for every $b\in(0,1]$ and is not used by it (Remark, p. 14).

What the result contributes

The theorem gives a constant probability bound against the paper's strongest, “almighty” arrival-order adversary. The guarantee is available from vertex degree inequalities alone. Consequently it applies to points of the exact matching polytope as well, without asking the online rounding procedure to exploit its additional odd-set inequalities. The paper places this result beside analogous existence claims for matroids and knapsacks in Theorem 1.8, and uses greedy schemes as components in more general selection results (Theorem 1.8, p. 4).

The existence theorem is proved in the source; it is an open formalization target here. A completed Lean development would supply a reusable finite model of independent active sets, random greedy families, edge selectability, and matching degree relaxations. It would also put the exact $e^{-2b}$ constant and its endpoint cases under machine checking. The definitions can support future formalizations of the paper's combination and application results, although this mission claims only Theorem 2.7 and its local proof milestones.

Where the argument is delicate

The local degree constraints bound the fractional weight at each endpoint separately, while selectability must survive conflicts at either endpoint under any arrival order. Merely ensuring that the algorithm outputs a matching gives no lower bound for a particular edge: the adversary can expose competing active edges first. The theorem therefore asks for a stronger event that certifies an edge could be added after every eligible previously selected matching. The numerical guarantee must hold uniformly over all edges, even when a coordinate is zero (Definitions 1.4–1.5, pp. 3–4; proof of Theorem 2.7, p. 13).

Formalization scope

The ground set is the finite edge type $E$ . The published EdmondsMatching65.Polyhedron.Graph structure represents a graph by a map from edges to unordered pairs of vertices and includes a proof excluding self-loops; its matching predicate is reused directly. This admits parallel edges, a harmless generalization of the page's graph language. Incident edge sets and matchings are finite sets. The polytope is the set of real edge vectors satisfying precisely the nonnegativity and vertex degree inequalities above. Scaling is the pointwise set operation $bP_G$ , so $b=0$ remains meaningful. The parameter range $0\le b\le1$ is explicit.

Probability is represented by finite sums of product weights. A randomized scheme is a weight function on finite greedy families, independent of the active-set draw. Each family contains the empty set and lies inside the matchings; allowing an empty family would make selectability vacuous. The degree inequalities keep relevant coordinates in $[0,1]$ , so active-set weights are genuine probabilities. The source's ratio $(1-e^{-x_g})/x_g$ is given its continuous value $1$ at $x_g=0$ . For inputs outside the nonnegative domain, which the theorem never uses, that inclusion probability is also assigned $1$ to keep the distribution well formed. These choices and the loopless graph convention are recorded with the draft statements.

The formalization needs finite product probability identities, elementary exponential inequalities, and set facts about matchings and incident edges. Contributions proving the six listed milestones, the deterministic Remark, or the full existential theorem are welcome. The finite model of active sets, greedy families and selectability is shared with the other missions of this series (matroids, knapsack, combinations of schemes, submodular rounding).

Selected references

Moran Feldman, Ola Svensson, and Rico Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015, preprint. Published as Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM Journal on Computing, 2021.

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Theoretical Computer Science·Captain: mikedeng1

Prophet Inequalities Made Easy: Stochastic Optimization by Pricing Nonstochastic Inputs III: Under a Consistent Allocation Rule, (α, β)-Balanced Prices Are Closed Under Maxima of ValuationsResearch Paper

Motivation

Posted prices turn an offline allocation problem into a sequential choice process: each agent sees a menu of outcomes and prices, then chooses an outcome without revealing its full valuation. The balanced prices framework of Dütting, Feldman, Kesselheim, and Lucier gives welfare guarantees by comparing the revenue collected from an allocation with the welfare that remains feasible after it. Its appeal is that the comparison can be checked in a deterministic full-information setting before any probability distribution over valuations enters the analysis. Dütting et al., 2020

One valuation class at a time would make that framework difficult to reuse. Combinatorial auction valuations are often built by taking pointwise maxima of simpler valuations or by adding values from separate markets. Section 5 of the paper asks whether a price construction balanced for the simple class remains balanced after these operations. Theorem 5.3 gives the maximum closure result; Theorem 5.4 gives addition across markets. Appendix B extends both to the weaker balancing condition used elsewhere in the paper. Dütting et al., 2020, §5 and Appendix B

Setting

There are $n$ agents in a fixed order. Agent $i$ receives an outcome $x_i$ from a space $X_i$ containing a null outcome. A profile $x=(x_i)_i$ is feasible when it lies in $\mathcal F$ . The model assumes downward closure: removing the outcomes of any group of agents from a feasible profile keeps it feasible. For a set of agents $S$ , write $x_S$ for the profile retaining $x_i$ on $S$ and assigning the null outcome elsewhere. The prefix $x_{[i-1]}$ retains only the agents before $i$ . Dütting et al., 2020, §2

A valuation profile $v$ assigns each agent a function $v_i:X_i\to\mathbb R$ . The welfare of $x$ is $v(x)=\sum_i v_i(x_i)$ . Every base valuation takes values in $[0,1]$ , the normalization stated in §2. For any set $S$ of profiles, $v(\operatorname{OPT}(v,S))$ denotes the best welfare achievable in $S$ . An allocation rule ALG chooses a feasible profile from a valuation profile. A pricing rule assigns a nonnegative, possibly infinite price $p_i(x_i\mid y)$ to outcome $x_i$ when the partial profile is $y$ ; an infeasible extension has infinite price. Dütting et al., 2020, pp. 547–548

An exchange-compatible family $(\mathcal F_x)_{x\in X}$ specifies a set of comparison profiles for each profile $x$ . It is exchange compatible when replacing any one coordinate of $x$ by the corresponding coordinate of any $y\in\mathcal F_x$ gives a feasible profile. This property is required for every $x$ in the full outcome space. A rule $p^v$ is $(\alpha,\beta)$ -balanced for valuation $v$ , ALG, and that family, for constants $\alpha>0$ and $\beta\ge0$ (Definition 3.1), when both inequalities hold for every feasible $x$ and every $x'\in\mathcal F_x$ :

\frac{v(\operatorname{ALG}(v))-v(\operatorname{OPT}(v,\mathcal F_x))}{\alpha} \le \sum_i p_i^v(x_i\mid x_{[i-1]}), \qquad \sum_i p_i^v(x'_i\mid x_{[i-1]}) \le \beta v(\operatorname{OPT}(v,\mathcal F_x)).

The maximum extension $V_i^{\max}$ of a base valuation space $V_i$ consists of nonempty finite pointwise maxima of elements of $V_i$ . A base profile $\tilde v$ supports an extended profile $v$ at $x$ if $\tilde v_i\le v_i$ at every outcome and $\tilde v_i(x_i)=v_i(x_i)$ for every agent. ALG is consistent when $\tilde v(\operatorname{ALG}(\tilde v))\ge\tilde v(\operatorname{ALG}(v))$ whenever $\tilde v$ supports $v$ at $\operatorname{ALG}(v)$ . The optimal allocation rule has this property by Lemma 5.2. Dütting et al., 2020, p. 554

Formalization targets

Closure under maxima

The goal is Theorem 5.3. Given one exchange-compatible family and a collection $(p^w)_{w\in V}$ balanced for every base profile, consistency of ALG preserves the same constants for every extended profile and every corresponding supporting base profile:

v\in V^{\max},\quad \tilde v\in V\text{ supports }v\text{ at }\operatorname{ALG}(v) \quad\Longrightarrow\quad p^{\tilde v}\text{ is }(\alpha,\beta)\text{-balanced for }v.

The milestone list records the welfare supremum comparison and the two price inequalities in the paper's proof. The family $\mathcal F_x$ remains the same for all base and extended profiles. Dütting et al., 2020, Theorem 5.3 and proof

Closure under addition and weak balancedness

Theorem 5.4 treats $m$ separate allocation problems. The joint outcome and feasible set are products; values and prices add across components; ALG applies each component's rule. It asserts balancedness with the same $\alpha$ and $\beta$ . Appendix B changes the second balancedness bound to $\beta_1v(\operatorname{OPT}(v,\mathcal F_x))+\beta_2v(\operatorname{ALG}(v))$ and requires strong consistency for maximum closure. Theorems B.2 and B.3 preserve $\alpha,\beta_1,\beta_2$ under maxima and addition, respectively. Dütting et al., 2020, Theorems 5.4, B.2, B.3

Significance

The maximum closure theorem lets a balanced-price construction for a simple valuation class cover finite maxima of that class without worsening its balancing constants. The addition theorem lets separately priced markets be combined by summing prices. Together these two operations account for the XOS composition discussed immediately after Theorem 5.4; the paper uses the results to connect its general framework to combinatorial auctions and multidimensional matroid settings. Dütting et al., 2020, p. 555

These results have paper proofs. The work here is to state their exact deterministic content in Lean so later formalizations of the price constructions can import the closure theorems. The definitions of supporting valuations, exchange-compatible families, and extended-real prices are reusable beyond this mission. The companion statements keep the product-market and weak-balancedness variants alongside the central theorem, while their proofs remain to be formalized.

Difficulty

For maximum closure, the prices are indexed by a base profile $\tilde v$ but must be balanced for a different profile $v$ that is pointwise larger. A supporting profile agrees with $v$ only at ALG's outcome $\operatorname{ALG}(v)$ , while condition (a) refers to $\operatorname{ALG}(\tilde v)$ , an outcome ALG chooses for a different input, and both conditions refer to optimal welfare over $\mathcal F_x$ , where $\tilde v$ and $v$ can differ. Balancedness of $p^{\tilde v}$ for $\tilde v$ therefore says nothing about $v$ on its own; without a hypothesis tying ALG's choices for $v$ and $\tilde v$ together the statement is false, which is why consistency (Definition 5.1) is part of the theorem. The formal statement must keep the real-valued optimum meaningful for maxima of base valuations, so the $[0,1]$ normalization of §2 is carried through to $V^{\max}$ . Dütting et al., 2020, Definition 5.1 and Theorem 5.3

For addition, a direct product of the component comparison families has an edge case: a component family can be empty while another is nonempty. The paper's displayed product family then makes the lower balancedness inequality too strong. The theorem statements ask for an exchange-compatible family to exist, as the printed theorems do; they do not require that failing product family. This discrepancy is recorded for review. Dütting et al., 2020, proof of Theorem 5.4

Formalization scope

Agents and markets use zero-based finite indices; the paper writes agent indices from one. A profile's prefix contains exactly the agents with smaller indices. Valuations are functions to $\mathbb R$ with base values in $[0,1]$ . The maximum extension uses a nonempty finite set of base functions, so its maximum is defined at every outcome. Optimal welfare is a real supremum; bounded valuations keep it finite, and the empty set has value zero. Prices are extended nonnegative reals so $+\infty$ is retained. The lower balancedness inequality embeds its real right side using ofReal, which handles a negative lower bound consistently with nonnegative prices. The upper inequality keeps the price sum in extended reals.

The maximum theorem quantifies over every extended profile and every supporting base profile, including genuinely new maxima. It keeps one exchange-compatible family for all valuations. The maximum-closure theorems require every base price to satisfy the pricing-rule condition and conclude it for the supporting price. ALG feasibility is assumed on $V^{\max}$ , which contains the base profiles. The product theorems construct joint outcomes, additive values, componentwise ALG, and summed prices from the component data; they do not admit an unrelated joint allocation rule. Downward closure and a zero price for the null outcome at feasible partial allocations are included for the product statements. The latter is a disclosed assumption satisfied by the paper's pricing examples and needed to handle empty component families. No distribution or posted-price run is part of this deterministic mission. Lemma 5.2 and the strong-consistency companion take an optimal rule to be one that attains the welfare supremum over $\mathcal F$ on every profile in $V^{\max}$ , the profiles to which Definitions 5.1 and B.1 apply it; the product companions additionally conclude that the summed prices form a pricing rule (infinite off $\mathcal F$ ). Their ALG feasibility premise concerns the component profiles supplied in the theorem.

The development needs finite dependent products and sums, finite maxima, real suprema of bounded sets, and extended nonnegative arithmetic. Contributions proving the three maximum-closure milestones, the goal, or the product-market companions are all within scope. A proof that specializes the supporting profile to $\tilde v=v$ would lose the intended maximum extension and does not satisfy the goal's universal quantification.

Selected references

P. Dütting, M. Feldman, T. Kesselheim, and B. Lucier, Prophet Inequalities Made Easy: Stochastic Optimization by Pricing Nonstochastic Inputs, SIAM Journal on Computing 49(3):540–582, 2020. DOI: 10.1137/20M1323850.

7 thms2 active usersReviewed

Bandit Algorithms Information Theory Machine Learning·Captain: mikedeng1

Regret in Online Combinatorial Optimization II: Under Bandit Feedback Every Strategy Has Minimax Regret at Least 0.02 m√(dn) on Some Set of Actions with m OnesResearch Paper

Why bandit feedback matters

An online player repeatedly chooses a subset of coordinates and pays the sum of their losses. In many applications the player sees only that sum, not the losses of the selected coordinates. This bandit feedback makes it harder to identify which coordinate within each chosen subset is responsible for a favorable or unfavorable outcome. Audibert, Bubeck and Lugosi studied how this information limit changes regret in online combinatorial optimization. Their Theorem 5 establishes a lower bound that scales linearly with the number of selected coordinates and with the square root of the ambient dimension and horizon. Audibert, Bubeck and Lugosi, 2013, pp. 13–14

The result is part of a comparison among full-information, semi-bandit and bandit feedback in the same action model. Under full information the player sees the complete loss vector after each round; under semi-bandit feedback the player sees losses at selected coordinates; under bandit feedback the player sees only one scalar. The paper proves upper bounds for semi-bandit play and a bandit lower bound. The latter is the target of this mission. Audibert, Bubeck and Lugosi, 2013, pp. 2–3, 14

The game and its regret

Fix a dimension $d$ , a horizon $n$ , and a finite nonempty set $\mathcal A\subseteq\{0,1\}^d$ . Each action $a\in\mathcal A$ has exactly $m$ entries equal to one. At round $t$ , the player selects a probability distribution on $\mathcal A$ , draws an action $a_t$ , and simultaneously an adversary selects a loss vector $z_t\in[0,1]^d$ . The player pays the scalar $a_t^\mathsf Tz_t$ . In the bandit protocol, that scalar is the only new information made available for the next round. A player strategy can use every previous action and observed scalar loss, and can randomize at every round. Audibert, Bubeck and Lugosi, 2013, pp. 2–3

The paper measures performance by pseudo-regret against the best fixed action in expectation:

R_n=\mathbb E\sum_{t=1}^{n}a_t^\mathsf Tz_t- \min_{a\in\mathcal A}\mathbb E\sum_{t=1}^{n}a^\mathsf Tz_t.

The expectation covers the player's randomization and, when present, the adversary's randomization. This benchmark chooses one action for the whole horizon after comparing expected cumulative losses. It is the sole notion of regret used in the paper. Audibert, Bubeck and Lugosi, 2013, p. 2 and footnote 1

For the lower bound, the appendix arranges the $d$ coordinates as $m$ parallel games with $k=d/m$ choices per game. An action selects one coordinate from each game. The adversary can associate a favoured choice $\alpha$ with each game and assign independent Bernoulli losses whose means are $1/2-\epsilon$ at the favoured coordinates and $1/2$ elsewhere. The player still sees only the sum of the $m$ selected losses. These are the $\alpha$ -adversaries that underlie the milestone statements. Audibert, Bubeck and Lugosi, 2013, pp. 16–17

Formalization targets

The goal is Theorem 5 with the divisibility condition used by its appendix construction. For $n\ge d\ge2m$ and $m\mid d$ , there is an action set $\mathcal A$ such that every bandit strategy faces some bounded loss law with

R_n\ge0.02\,m\sqrt{dn}.

The order of the choices is part of the claim: the action set is fixed first; then each player strategy may face its own adversary. The lower bound retains the paper's explicit constant $0.02$ . Audibert, Bubeck and Lugosi, 2013, p. 14, Theorem 5; p. 16

The milestones follow the appendix's stated results: Lemma 5 bounds a logarithm; Lemma 4 and its corrected second case bound the divergence between sums of independent Bernoulli variables; the one-round observation bound and the horizon bound control information revealed by bandit feedback. Equations (9), (10), and (11) connect that information to expected regret and symmetry. The final averaged bound on the chance of selecting a favoured choice closes the path to the goal. The milestones are stated for deterministic players, as in the first three steps of the appendix; the passage to randomized players (the appendix's fourth step) is part of the goal's proof and is not a separate milestone. Audibert, Bubeck and Lugosi, 2013, pp. 17–18, 20–21

What the result establishes

The theorem prevents a uniform regret guarantee of smaller order than $m\sqrt{dn}$ for this bandit action model. It shows that aggregating $m$ selected losses into a single observation imposes a cost beyond what a player can avoid by choosing a different randomized strategy. In particular, the quantifier over every strategy makes the claim about the feedback model, rather than about one named algorithm. The paper proves the result in Appendix B, with the Bernoulli-sum estimate in Appendix C. Audibert, Bubeck and Lugosi, 2013, pp. 14, 16–18, 20–21

The formalization work is to prove the existing paper result in Lean from a finite protocol that represents all behavioural player strategies, together with the finite laws of the appendix's adversaries. The resulting definitions of action paths, scalar observations, finite probability laws, and divergence estimates can support other finite-horizon bandit lower bounds. These statements are drafted as open Lean theorems; compilation checks their types, while proofs remain for solvers. The paper's mathematical proof does not itself constitute a machine-checked proof.

Where the difficulty lies

A scalar bandit observation sums losses from several games. The player cannot separate the contribution of the favoured coordinate in one game from the other selected losses by inspecting that observation. A bound for the divergence of a single Bernoulli variable therefore does not directly bound the information available to the player. The appendix's central estimate concerns sums of independent Bernoulli variables, followed by the law of the whole sequence of scalar observations. Audibert, Bubeck and Lugosi, 2013, pp. 16, 18, 20

There is also a correction to make explicit. Lemma 4 is false for some parameters allowed by its printed statement: taking $n=\ell=1$ , $p=q=1/2$ , and $p'=0.001$ violates the displayed bound. The error is in the second case of its proof, which applies Lemma 5 outside its range when $p'<p$ . The mission states Lemma 4 with the additional condition $p(1-p')\le2p'(1-p)$ , which holds whenever $p\le p'$ , and states the corrected second case separately: for $q=p>p'$ , $\mathrm{KL}(\mathcal B,\mathcal B')\le(p'-p)^2/((1-p)p'(n+2))$ . Through the corrected case, the one-round bound used by the goal holds for the full range $0<\epsilon<1/2$ , so Theorem 5 and its constant are unaffected. Audibert, Bubeck and Lugosi, 2013, pp. 20–21, Lemmas 4–5

Formalization scope

Actions are functions $\mathrm{Fin}(d)\to\mathbb R$ constrained to zero or one, with coordinate sum $m$ . Coordinates and rounds are indexed from zero. A behavioural strategy maps every history of chosen actions and real-valued observed losses to a probability distribution on the finite action set. Its domain includes every real history, even though the appendix's particular Bernoulli adversaries generate integer observations. The strategy may randomize; restricting the goal to deterministic players or allowing it to inspect an unobserved loss vector would change the game.

The goal's exhibited adversary is an oblivious, finitely supported probability law on loss sequences in $[0,1]^{n\times d}$ . It belongs to the broader adversary class of the paper, so this existential formulation is stronger. All expectations are finite sums. The regret comparator is a minimum over the nonempty action set, not a default value assigned to an empty set. The action set has binary entries and equal coordinate sums, and every loss lies in the unit interval; these clauses rule out trivial lower bounds from malformed actions or unbounded losses.

The hypothesis $m\mid d$ is added to the printed theorem because Appendix B assumes it to partition coordinates into equally sized games. When $m=0$ , it forces $d=0$ and the claimed lower bound is zero. The milestone model uses functions $\mathrm{Fin}(m)\to\mathrm{Fin}(k)$ with $d=mk$ , deterministic players, finite Bernoulli product laws, and a finite real KL sum. Its log ratios are meaningful on the common support ensured by the stated parameter bounds. Reusable contributions include the finite bandit protocol and observation laws, as well as proofs of the KL and averaging milestones.

Selected references

Jean-Yves Audibert, Sébastien Bubeck and Gábor Lugosi, Regret in Online Combinatorial Optimization, Mathematics of Operations Research 39(1), 2014. arXiv:1204.4710v2; DOI:10.1287/moor.2013.0598.

13 thms2 active usersReviewed

Algorithmic Game Theory Probability·Captain: mikedeng1

Prophet Inequalities Made Easy: Stochastic Optimization by Pricing Nonstochastic Inputs II: Posted Expected Weakly (α, β₁, β₂)-Balanced Prices Earn 1/(α(2β₁ + 4β₂)) of the Expected Welfare of ALGResearch Paper

Motivation

A prophet inequality compares an online decision maker, who sees random inputs one at a time and must commit irrevocably, with a "prophet" who sees all inputs in advance. The classic single-item version (Krengel–Sucheston, Samuel-Cahn) says that a well-chosen fixed threshold earns at least half of the expected maximum. In mechanism design the same statement reads: a posted-price mechanism, which offers each arriving buyer a take-it-or-leave-it menu of prices, extracts a constant fraction of the optimal expected welfare, and does so in a way that is truthful, simple and order oblivious.

Dütting, Feldman, Kesselheim and Lucier (SIAM J. Comput. 49 (2020)) reduce the construction of such prices to a deterministic question. If, for every fixed valuation profile $v$ , one can find prices $p^v$ that are balanced — high enough to pay for the welfare an early allocation destroys, low enough that whatever is still feasible stays affordable — then the expected prices $\mathbb E_{\tilde v}[p^{\tilde v}]$ , suitably scaled, give a prophet inequality. This is their Theorem 3.2 for $(\alpha,\beta)$ -balanced prices. For combinatorial auctions with bundles of size at most $d$ , MPH- $k$ valuations and related settings, the natural prices only satisfy a weaker condition, in which the affordability bound may also spend a multiple of the benchmark welfare. Theorem 3.5, the subject of this mission, is the extension theorem for that weak balancedness; it is what turns the paper's Theorem 4.1 (bundle size $d$ ) and Theorem 1.6 (MPH- $k$ ) into $O(d)$ - and $O(k)$ -approximate posted-price mechanisms.

Setting

There are $n$ agents $N=\{1,\dots,n\}$ . Agent $i$ has an outcome space $X_i$ containing a null outcome $\emptyset$ ; outcome profiles are $x\in X=X_1\times\cdots\times X_n$ . For $S\subseteq N$ , $x_S$ gives $x_i$ to the agents in $S$ and $\emptyset$ to the others, and $x_{[i-1]}$ keeps only the agents before $i$ . The feasible profiles form a set $\mathcal F\subseteq X$ that is downward closed ( $x\in\mathcal F\Rightarrow x_S\in\mathcal F$ ).

Agent $i$ has a valuation $v_i:X_i\to[0,1]$ , drawn independently from a known distribution $\mathcal D_i$ ; $\mathcal D=\prod_i\mathcal D_i$ . The welfare of $x$ is $v(x)=\sum_i v_i(x_i)$ , and $v(\mathrm{OPT}(v,S))=\sup_{x\in S}v(x)$ (zero on $S=\emptyset$ ). An allocation rule $\mathrm{ALG}$ maps every valuation profile to a feasible outcome.

A pricing rule assigns prices $p_i(x_i\mid y)\in[0,\infty]$ to outcome $x_i$ offered to agent $i$ given the partial allocation $y$ , with $p_i(x_i\mid y)=\infty$ when $(x_i,y_{-i})\notin\mathcal F$ . In the posted-price mechanism the agents are approached in index order; agent $i$ sees the prices $p_i(\cdot\mid x_{[i-1]})$ and buys a utility-maximizing outcome, utility being $v_i(x_i)-p_i(x_i\mid x_{[i-1]})$ .

A family $(\mathcal F_x)_{x\in X}$ of sets of profiles is exchange compatible if $(y_i,x_{-i})\in\mathcal F$ for every $x\in X$ , $y\in\mathcal F_x$ and $i$ . Given $\alpha>0$ and $\beta_1,\beta_2\ge0$ , a pricing rule $p^v$ is weakly $(\alpha,\beta_1,\beta_2)$ -balanced (Definition 3.4) with respect to $\mathrm{ALG}$ and $(\mathcal F_x)$ if for every $x\in\mathcal F$

\text{(a)}\quad \sum_i p^v_i(x_i\mid x_{[i-1]})\ \ge\ \tfrac1\alpha\bigl(v(\mathrm{ALG}(v))-v(\mathrm{OPT}(v,\mathcal F_x))\bigr),

\text{(b)}\quad \sum_i p^v_i(x'_i\mid x_{[i-1]})\ \le\ \beta_1\,v(\mathrm{OPT}(v,\mathcal F_x))+\beta_2\,v(\mathrm{ALG}(v))\quad\text{for all }x'\in\mathcal F_x.

A collection $(p^v)_{v}$ is weakly balanced if one exchange-compatible family works for every $v$ .

Formalization targets

Goal: Theorem 3.5 (p. 551)

If $(p^v)_v$ is weakly $(\alpha,\beta_1,\beta_2)$ -balanced with $\beta_1+\beta_2\ge1/\alpha$ , then with

\delta=\frac1{\beta_1+\max\{2\beta_2,1/\alpha\}},\qquad p_i(x_i\mid y)=\mathbb E_{\tilde v}\bigl[p^{\tilde v}_i(x_i\mid y)\bigr],

the posted-price mechanism with prices $\delta p$ , approaching agents in index order, satisfies

\mathbb E_v\Bigl[\sum_i v_i(x_i(v))\Bigr]\ \ge\ \frac1{\alpha(2\beta_1+4\beta_2)}\,\mathbb E_v\bigl[v(\mathrm{ALG}(v))\bigr].

Milestones (Appendix A, pp. 559–560)

Each agent's utility in the run is nonnegative.
(A.1): the total expected utility is at least the value of a ghost-sample deviation $x'(v,v')\in\mathcal F_{x(v)}$ minus its expected price.
(A.2): property (b) bounds that price by $\delta\beta_1\mathbb E[\tilde v(\mathrm{OPT}(\tilde v,\mathcal F_{x(v)}))]+\delta\beta_2\mathbb E[\tilde v(\mathrm{ALG}(\tilde v))]$ .
(A.3): $\mathbb E[\sum_iu_i]\ge(1-\delta\beta_1)\,\mathbb E[\tilde v(\mathrm{OPT}(\tilde v,\mathcal F_{x(v)}))]-\delta\beta_2\,\mathbb E[\tilde v(\mathrm{ALG}(\tilde v))]$ .
(A.4): property (a) bounds the expected revenue from below.
Case 1, $\beta_2\ge1/(2\alpha)$ , $\delta=1/(\beta_1+2\beta_2)$ : the goal's bound.
Case 2, $\beta_2<1/(2\alpha)$ , $\delta=1/(\beta_1+1/\alpha)$ : the bound with constant $(1-\alpha\beta_2)/(1+\alpha\beta_1)$ .
Case 2's last step: $(1-\alpha\beta_2)/(1+\alpha\beta_1)\ge1/(\alpha(2\beta_1+4\beta_2))$ under the theorem's constraints.

Significance

The result. Theorem 3.5 is the second of the paper's two extension theorems. Its hypothesis is a deterministic, full-information property of prices, which is often checkable by a direct combinatorial argument; its conclusion is a Bayesian guarantee for an online, truthful mechanism. The paper instantiates it with weakly $(1,1,d-1)$ -balanced fractional prices for combinatorial auctions with bundle size at most $d$ (Theorem 4.1) and for MPH- $k$ valuations (Theorem 1.6), obtaining approximation ratios linear in $d$ and $k$ , where $(\alpha,\beta)$ -balancedness alone would not apply.

Formalizing it. The theorem is proved on paper; no machine-checked version exists. The mission produces a formal account of the sequential posted-price mechanism with history-dependent prices (an online run defined by recursion over the agents), of the ghost-sample argument, and of the case analysis in $\delta$ . The definitions are general enough that the paper's applications — and other balanced-price arguments — can be stated on top of them. The printed proof has a slip: (A.1) is printed as an equality but only the inequality " $\ge$ " holds; the formalization states the inequality.

Difficulty

Two steps carry the content. First, the utility bound (A.1): agent $i$ could have bought its part of the deviation $x'(v,v')$ , but that deviation is defined from the run on a different profile. The argument needs that the partial allocation $x_{[i-1]}(v)$ does not depend on $v_i$ — the mechanism is online — and that exchanging $v_i$ with an independent copy $v'_i$ preserves the joint law. Making this exchange rigorous on a product measure, and handling an empty $\mathcal F_{x(v)}$ (where no deviation exists and the bound must come from $u_i\ge0$ ), is where the work lies. Second, $v(\mathrm{OPT}(v,\mathcal F_x))$ is a supremum that need not be attained, so "buy your part of OPT" must be replaced by near-optimal selections and a limit.

The tempting shortcut of treating weak balancedness as $(\alpha,\beta_1+\beta_2)$ -balancedness and applying Theorem 3.2 does not work: property (b) of Definition 3.1 bounds prices by a multiple of $v(\mathrm{OPT}(v,\mathcal F_x))$ alone, which can be zero while $v(\mathrm{ALG}(v))$ is not.

Formalization scope

Agents are Fin n, 0-based: the paper's agent $i$ is index $i-1$ , and "the order they are indexed" is the order of Fin n. Prices take values in ENNReal with $\infty=\top$ ; price sums are never converted to reals, and property (a) passes its right side through ENNReal.ofReal (a negative bound becomes $0$ , which is the page's meaning). $v(\mathrm{OPT}(v,S))$ is the real supremum sSup, zero on the empty set, meaningful because values lie in $[0,1]$ .

Valuations are given by type spaces $V_i$ and an evaluation $\mathrm{val}_i(w,x_i)\in[0,1]$ . The type spaces are countable with discrete σ-algebras — a disclosed restriction of the paper's general distributions, which makes every function measurable and every bounded one integrable. The null outcome is assumed free at feasible partial allocations ( $p^{\tilde v}_i(\emptyset\mid y)=0$ for $y\in\mathcal F$ ): every pricing rule in the paper has this property, and the proof needs its consequence $u_i(v)\ge0$ . Exchange compatibility is required for all $x\in X$ , as printed. The agents' behaviour is a choice rule that sees only the agent's own type and the earlier agents' outcomes and maximizes utility at every feasible partial allocation; at infeasible ones no requirement is made. The constant $\delta$ is written literally inside the posted prices, never as a free parameter.

The milestones (A.1)–(A.4) are stated for an arbitrary $\delta>0$ , and (A.1)–(A.2) for an arbitrary selector into $\mathcal F_{x(v)}$ in place of the maximizer, with an explicit zero when $\mathcal F_{x(v)}=\emptyset$ ; both are generalizations of the printed steps. A statement in which the agents' optimality hypothesis can never be met, or in which an infinite price sum is read as $0$ , would make the goal vacuous; the encoding above excludes both, and a sorry-free one-agent instance in the workspace confirms that all hypotheses of the goal can hold together.

Needed infrastructure: product measures and the swap of one coordinate with an independent copy, lower integrals of ENNReal-valued prices, the recursion defining the run, and near-maximizers of bounded suprema. The model and mechanism definitions are reusable for the paper's other extension theorem (Theorem 3.2) and its applications. Contributions are welcome on any milestone; the pure inequality of Case 2 is self-contained.

Selected references

P. Dütting, M. Feldman, T. Kesselheim, B. Lucier, Prophet inequalities made easy: Stochastic optimization by pricing nonstochastic inputs, SIAM Journal on Computing 49(3):540–582, 2020. https://doi.org/10.1137/20M1323850
U. Krengel, L. Sucheston, Semiamarts and finite values, Bulletin of the AMS 83(4):745–747, 1977. https://doi.org/10.1090/S0002-9904-1977-14378-4
E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Annals of Probability 12(4):1213–1216, 1984. https://doi.org/10.1214/aop/1176993150
R. Kleinberg, S. M. Weinberg, Matroid prophet inequalities, STOC 2012, 123–136. https://doi.org/10.1145/2213977.2213991

12 thms2 active usersReviewed

Completed

Machine Learning Optimization Probability·Captain: mikedeng1

Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming 3: The Two-Phase RSG Method Finds an (ε, Λ)-Solution within S(Λ)[N(ε) + T(ε, Λ)] Oracle CallsResearch Paper

Motivation

Stochastic optimization methods often see only noisy gradients. For a nonconvex objective, a useful guarantee is that an output point has a small gradient: this is a first-order stationarity certificate, even when there is no claim that the point is globally optimal. A guarantee on the expected squared gradient leaves open how often one particular run succeeds. The two-phase randomized stochastic gradient method of Ghadimi and Lan (2013) addresses that question by generating several candidates and using further oracle calls to select one. The paper gives an explicit bound on the probability of failure and on the number of oracle calls needed for a prescribed accuracy and confidence.

The work sits within stochastic approximation, where the objective may be a population expectation or another function accessible through noisy observations. The 2013 paper develops first- and zeroth-order methods for smooth nonconvex problems. This mission concerns its two-phase first-order result, Theorem 2.4, rather than the Gaussian smoothing results in its later section. The source for every index here is the arXiv v1 preprint; the printed page and PDF page coincide.

Setting

The objective is a differentiable function $f:\mathbb R^n\to\mathbb R$ bounded below, with true optimal value $f^*=\inf_x f(x)$ . Its gradient map $g=\nabla f$ is $L$ -Lipschitz: $\|g(y)-g(x)\|\le L\|y-x\|$ for all $x,y$ . The mission uses $L>0$ . No convexity is assumed.

A stochastic first-order oracle returns a vector $G(x_k,\xi_k)$ when called at the current iterate $x_k$ . Assumption A1 says that the oracle is unbiased at that iterate and has squared error of expectation at most $\sigma^2$ . The noise may depend on earlier calls. In the formal model, the mean is conditional on the past, and the oracle and squared-error random variables are integrable. This makes explicit the probabilistic assumptions used when the paper takes expectations. The model takes $\sigma>0$ because the paper's displayed stepsize and post-optimization sample size otherwise degenerate under Lean's total division convention.

A randomized stochastic gradient run starts at $x_1$ and uses $x_{k+1}=x_k-\gamma_k G(x_k,\xi_k)$ . It chooses an output index $R\in\{1,\ldots,N\}$ with the probability mass function in equation (2.3), independently of that run's oracle noise, and outputs $x_R$ . For a parameter $\widetilde D>0$ , the constant stepsize in equation (2.13) is $\gamma_k=\min\{1/L,\widetilde D/(\sigma\sqrt N)\}$ . The paper writes $D_f=\sqrt{2(f(x_1)-f^*)/L}$ and

\mathcal B_N=\frac{LD_f^2}{N}+\left(\widetilde D+\frac{D_f^2}{\widetilde D}\right)\frac{\sigma}{\sqrt N}.

The two-phase method makes $S$ independent RSG runs, yielding $\bar x_1,\ldots,\bar x_S$ . For each candidate it averages $T$ fresh oracle outputs into an estimated gradient $\widehat g_s$ . It selects a candidate $\bar x^*$ whose estimated-gradient norm is minimal. The post-optimization samples for different candidates may be recycled; the paper explicitly permits this. The candidate itself is known when its post-optimization samples are taken, so the conditional oracle assumption is stated relative to a filtration that contains it at time zero.

Formalization targets

The first target is the one-run mean bound of Corollary 2.2, $L^{-1}\mathbb E\|g(x_R)\|^2\le\mathcal B_N$ , followed by the one-run tail bound (2.19). Lemma 2.3(a) controls the squared norm of a sum of vector martingale differences. Equation (2.28) relates a selected candidate's true gradient to the best candidate and the estimation errors. Equation (2.29) factors the probability of simultaneous failure across independent runs and bounds it, while (2.30) bounds the other source of failure: every optimization run performing poorly, and at least one estimated gradient being inaccurate.

For arbitrary positive $S,N,T$ , Theorem 2.4(a) states the stronger quantitative tail bound

\Pr\left\{\|g(\bar x^*)\|^2\ge2\left(4L\mathcal B_N+\frac{3\lambda\sigma^2}{T}\right)\right\}\le\frac{S+1}{\lambda}+2^{-S}\qquad(\lambda>0).

The goal, Theorem 2.4(b), specializes those parameters to an accuracy $\varepsilon>0$ and failure probability $0<\Lambda<1$ . It sets

S=\left\lceil\log_2\frac2\Lambda\right\rceil,\qquad N=\left\lceil\max\left\{\frac{32L^2D_f^2}{\varepsilon},\left(\frac{32L(\widetilde D+D_f^2/\widetilde D)\sigma}{\varepsilon}\right)^2\right\}\right\rceil,\qquad T=\left\lceil\frac{24(S+1)\sigma^2}{\Lambda\varepsilon}\right\rceil.

An $(\varepsilon,\Lambda)$ -solution is a point satisfying $\Pr\{\|g(\bar x^*)\|^2\le\varepsilon\}\ge1-\Lambda$ . With those parameter values, the method computes such a point using at most $S(N+T)$ stochastic first-order oracle calls. The formulas and constants above are those of equations (2.24)–(2.27) of the preprint.

Significance

The result turns a mean stationarity bound into a confidence guarantee for one returned point, with an explicit accounting of both candidate generation and candidate assessment. It identifies how the number of independent runs, iterations per run, and gradient estimates scale with the requested accuracy and failure probability. Without the post-optimization phase, the paper's direct Markov estimate (2.19) gives a less favorable dependence on the failure probability for a single run.

The mathematical theorem is proved in the 2013 paper; the Lean declarations in this proposal are statements awaiting machine-checked proofs. A completed formalization would give reusable definitions for a dependent-noise gradient oracle, a random-output stochastic-gradient run, and a post-optimization selection procedure. The vector martingale estimate and finite-candidate inequality could also serve later stochastic-optimization developments. Contributions to the probability and measurability infrastructure, as well as the final rate proof, are within scope.

Difficulty

Selecting the candidate with the smallest estimated gradient need not select the one with the smallest true gradient. The estimates are random and are evaluated at candidates that are themselves random outputs of earlier oracle runs. A bound for a fixed point does not address this dependence. The argument needs a conditional oracle contract at each candidate and a separate guarantee that the optimization runs supply a sufficiently good candidate. The paper's intermediate display (2.31) applies a fixed-candidate tail estimate to the selected candidate even though the selection examines the same estimates; that step is not justified by the stated assumptions. The final bound can be phrased without treating (2.31) as a separate target.

Formalization scope

The space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Iterations and oracle samples retain the paper's one-based indexing; candidate runs use Fin S, which reindexes the paper's $1,\ldots,S$ . The objective's true infimum is carried by IsGLB (Set.range f) fstar, so $D_f$ cannot be weakened by substituting an arbitrary lower bound. Each candidate is generated by the RSG recursion and the mass function (2.3); the one-run performance bound is a theorem, not a hypothesis of the two-phase model. Independent candidate outputs are required for (2.29). The selected candidate may be any minimizer of the estimated-gradient norm, with any tie rule; no measurability of the selection is assumed.

All expectations are Bochner integrals, with integrability included in the oracle assumptions and in the one-run conclusion. Probabilities are ℝ≥0∞ values. The noise carrier is generalized from the paper's Borel subsets of Euclidean space to a measurable type. The general vector martingale lemma omits the paper's Polish-space and trivial-time-zero conditions; neither is needed for its squared-norm bound, and the latter would conflict with a candidate known at time zero. Its non-strict tail statement is restricted to a positive sum of variance bounds, because the printed version is false when every bound is zero. The goal reads the logarithm in (2.24) as base two, matching the paper's final $2^{-S}\le\Lambda/2$ comparison. Positive $\sigma$ and $\widetilde D$ avoid zero steps and an empty post-optimization average.

The formal goal states the probability guarantee. The $S(N+T)$ oracle-call bound follows directly from the algorithm's two loops and is recorded in the theorem's prose rather than in a separate operational semantics for calls. A complete proof may use Mathlib's conditional expectations, independent random variables, finite sums, and real logarithm and ceiling libraries. No assumption may simply postulate the one-run gradient bound or the final success probability.

Selected references

Saeed Ghadimi and Guanghui Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. arXiv:1309.5549v1.

11 thms2 active usersReviewed

Machine Learning Optimal Transport Optimization·Captain: mikedeng1

Wasserstein Distributionally Robust Optimization and Variation Regularization II: The ∞-Wasserstein Regularizer Equals ρ Times the Mean Local Slope up to ρ²‖H‖ Plus a Boundary TermResearch Paper

Motivation

In distributionally robust optimization, a decision is judged against probability laws near a nominal law rather than against the nominal law alone. The nominal law is often the empirical distribution of observed data. For a loss function, this produces a worst-case expected loss that depends on the size and geometry of the permitted changes to the data. The infinity-Wasserstein model restricts how far any observation can be moved, apart from null events in a coupling. It is a mathematical form of the bounded perturbations used in adversarial learning. Gao, Chen and Kleywegt study when this robust loss behaves like a regularizer based on variation or local slope.

For a finite data set, the nominal law has finite support. This makes the infinity-Wasserstein case especially concrete: each atom of the empirical law has a radius-limited set of possible destinations. Yet the objective still ranges over all probability measures, and the loss need not be bounded on a metric ball. The paper's finite-support duality result and its local-slope estimate together identify the regularization term that this distributional model produces.

Setting

Let $(Z,d)$ be a metric space and let $P,Q$ be probability laws on its Borel sets. A coupling $\pi$ of $P$ and $Q$ is a joint law on $Z\times Z$ with those two marginals. The infinity-Wasserstein distance is

W_\infty(P,Q)=\inf_{\pi\in\Gamma(P,Q)} \operatorname*{ess\,sup}_{(\tilde z,z)\sim\pi}d(\tilde z,z).

Given a real loss $f$ and a radius $\rho\ge0$ , the robust value is the supremum of $\mathbb E_P[f]$ over all $P$ satisfying $W_\infty(P,Q)\le\rho$ . The regularizer $R_{Q,\infty}(\rho;f)$ is this robust value minus $\mathbb E_Q[f]$ . For observations $z_1,\ldots,z_n$ , the empirical law is $P_n=n^{-1}\sum_{i=1}^n\delta_{z_i}$ .

The one-sided local slope $|\partial f|(z)$ records the greatest limiting rate at which $f$ can increase under a perturbation that tends to $z$ . The local growth $G_f(\delta,z)$ is the largest increase $f(\tilde z)-f(z)$ among destinations with $d(\tilde z,z)\le\delta$ . A set $D_f$ marks the interfaces between pieces of a piecewise loss. Its boundary contribution at $z$ is $(\delta-d(z,D_f))_+$ , where the distance to an empty set is infinite. These objects appear in Definition 2 and Assumption 5(I).

Formalization targets

Finite-support transport duality

For a nominal law $Q=\sum_j q_j\delta_{z_j}$ , the first targets assert that an optimal coupling exists when $W_\infty(P,Q)$ is finite and that

\sup_{P:W_\infty(P,Q)\le\rho}\mathbb E_P[f] =\sum_j q_j\sup_{d(\tilde z,z_j)\le\rho}f(\tilde z).

This is Lemma EC.2 in the appendix. The values are allowed to be infinite when a local loss supremum is infinite; the printed assertion of unconditional finiteness is not included.

Consistency

For an upper semicontinuous loss, the Proposition 1 case $p=\infty$ asserts

\lim_{\rho\downarrow0}R_{P_n,\infty}(\rho;f)=0=R_{P_n,\infty}(0;f).

It is a companion statement: it says that the regularizer vanishes, while the main target says at which rate.

Local-slope regularization

The main target is Theorem 1(I), in its general-metric form from Appendix B under Assumption 5(I). If $\delta_0>0$ , $M\ge0$ , and the local growth obeys

|G_f(\delta,z)-\delta|\partial f|(z)| \le H(z)\delta^2+M(\delta-d(z,D_f))_+ \quad(0\le\delta<\delta_0),

then, for a sufficiently small radius, every nonempty empirical sample and every loss in the class satisfy

\left|R_{P_n,\infty}(\rho;f) -\rho\frac1n\sum_{i=1}^n|\partial f|(z_i)\right| \le\rho^2\frac1n\sum_{i=1}^n|H(z_i)| +M\frac1n\sum_{i=1}^n(\rho-d(z_i,D_f))_+.

The finite-support duality and the identity between the empirical regularizer and the average of $G_f(\rho,z_i)$ are the mission's intermediate targets. The printed $\rho_n^2$ in Lemma EC.9 is read as $\rho^2$ , as in Theorem 1(I).

Significance

The estimate gives a precise first-order description of infinity-Wasserstein robustness: the mean local slope is its leading regularization term. The quadratic term measures local curvature or growth, while the boundary term records the effect of sample points close to interfaces between loss pieces. Setting $M=0$ gives the smooth-loss regime, where that interface correction vanishes. The result makes it possible to compare bounded data perturbations with explicit variation penalties using the same loss class and sample.

The paper proves the result. The formalization work here is to express its objects and quantified conditions in Lean, establish finite-support duality for the extended-real robust value, and then formalize the known local estimate. No machine-checked proof of these mission targets is claimed here. The transport and duality definitions can support other finite-support distributionally robust models; the local-slope definitions can be reused for other metric-space perturbation bounds.

Difficulty

The robust value is a supremum over probability laws, whereas the target bound is a finite average of pointwise quantities. Relating the two requires control of the infinity-Wasserstein constraint at every nominal atom, including cases where an infimum over couplings must be attained. A direct substitution of a pointwise supremum into an expectation does not establish the reverse inequality, and extended-real values need care when a loss is unbounded. At the local level, a slope is only a limit near a point; the inequality needed here holds uniformly for all losses, all points, and all sufficiently small radii, with a correction near $D_f$ .

Formalization scope

The Lean metric space uses its Borel measurable structure and is second countable, so the distance on the product is measurable. It has no isolated points, matching §3.4. Losses in the class are measurable. Sample indices are Fin n with $n>0$ , and $P_n$ is the published empirical probability law. Infinity-Wasserstein distance takes values in $[0,+\infty]$ ; robust values and local growth use extended reals. The theorem explicitly requires finite local slopes and finite growth values in the range where Assumption 5(I)'s real inequality is used. The regularizer is built from the supremum over all probability laws in the Wasserstein ball, and its finite-sample result states finiteness before converting its value to a real number. This rules out replacing the regularizer by the easier average of local growth.

The paper defines $D_f$ from intersections of closures of pieces and assumes it is null under a true law. The deterministic estimate uses only distances to $D_f$ , so this mission treats $D_f$ as supplied data and does not require nullity. Likewise, $H\in L^1(P_{\rm true})$ is needed for the paper's statistical setting but the target evaluates $H$ only at finite sample points, so no true law appears in this statement. The radius bound is placed before the sample because Assumption 5(I) supplies one common $\delta_0$ . These generalizations and the positive-radius reading of Assumption 5(I) are explicit in the item statements. Contributions toward the optimal-coupling lemma, extended-real finite-support duality, and the local estimate all advance the target.

Selected references

R. Gao and A. J. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research, 2023; arXiv:1604.02199. Source of the duality theory for finite $p$ that Lemma EC.1 quotes.
R. Gao, X. Chen and A. J. Kleywegt, Wasserstein Distributionally Robust Optimization and Variation Regularization, Operations Research, 2024; arXiv:1712.06050, source preprint dated 2020-10-30, especially Theorem 1(I), Assumption 5(I), Lemmas EC.2 and EC.9.

10 thms2 active usersReviewed

Completed

Optimization Probability Statistics·Captain: mikedeng1

Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization 1: Empirical Burg-Ball DRO Bounds Cover E[h(x;ξ)] with Probability Tending to 1 − αResearch Paper

Motivation

Stochastic programs and chance-constrained models in operations research contain expectations of the form

Z_0(x)=\mathbb E_0[h(x;\xi)],

where $\xi$ is a random input under an unknown distribution $P_0$ , $x$ is a decision and $h$ is a known loss. In practice $P_0$ is seen only through i.i.d. data $\xi_1,\dots,\xi_n$ . Distributionally robust optimization (DRO) replaces the unknown expectation by the worst case over a set of plausible distributions, and a recurring question is how large that set should be so that the robust value is a statistically valid bound, without being needlessly conservative.

The usual answer, for divergence-based sets on a finite support of size $k$ , sets the radius from a $\chi^2_{k-1}$ quantile (Ben-Tal et al. 2013). This guarantee holds simultaneously for every function of the distribution, and so it is loose for a single expectation, and it degrades as $k$ grows. H. Lam (arXiv:1605.09349, Operations Research 2019) observed that if the ball is placed around the empirical distribution and measured with the Burg entropy, the right radius uses one degree of freedom, whatever the support. The DRO bounds then form an asymptotically exact confidence interval for $Z_0(x)$ . The mechanism is the empirical likelihood method of Owen (Owen 1988; Owen 2001).

Timeline:

1988: Owen proves the empirical likelihood theorem for a mean (−2 log of the profile likelihood ratio tends to $\chi^2_1$ ), the nonparametric analogue of Wilks' theorem.
2013: Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen calibrate $\varphi$ -divergence balls on a finite support with $\chi^2_{k-1}$ quantiles.
2016: Lam (this paper) connects the empirical Burg-ball DRO to empirical likelihood, with pointwise (Theorem 2) and uniform (Theorem 4) coverage.
2016–2021: Duchi, Glynn and Namkoong (arXiv:1610.03425) develop the general $f$ -divergence version and exact coverage of optimal values.

Setting

Data: $\xi_1,\xi_2,\dots$ are i.i.d. random elements of a measurable space $\Xi$ under $P_0$ . A decision $x\in\mathbb R^m$ is fixed, and $h(x;\cdot):\Xi\to\mathbb R$ is measurable with $0<\operatorname{Var}_0 h(x;\xi)<\infty$ .

The empirical Burg-entropy divergence ball of radius $\eta$ is the set of weight vectors on the $n$ data points

\mathcal U_n(\eta)=\Big\{w\in\mathbb R^n:\ -\frac1n\sum_{i=1}^n\log(nw_i)\le\eta,\ \sum_{i=1}^n w_i=1,\ w_i\ge0\Big\},

with $\log 0=-\infty$ . It is the $\varphi$ -divergence ball around the uniform weights $1/n$ for the Burg generator $\varphi(t)=-\log t+t-1$ . Let $\chi^2_{1,1-\alpha}$ be the $(1-\alpha)$ -quantile of the $\chi^2_1$ law, i.e. $P(Y^2\le\chi^2_{1,1-\alpha})=1-\alpha$ for $Y\sim N(0,1)$ . The empirical DRO bounds are

\underline Z_n(x)=\min_{w\in\mathcal U_n(\chi^2_{1,1-\alpha}/(2n))}\sum_{i=1}^n h(x;\xi_i)w_i,\qquad \overline Z_n(x)=\max_{w\in\mathcal U_n(\chi^2_{1,1-\alpha}/(2n))}\sum_{i=1}^n h(x;\xi_i)w_i .

For a sample $z\in\mathbb R^n$ and a value $\mu$ , the profile empirical likelihood statistic is

-2\log R(\mu)=\min\Big\{-2\sum_{i=1}^n\log(nw_i):\ \sum_i w_iz_i=\mu,\ \sum_i w_i=1,\ w_i\ge0\Big\},

equal to $+\infty$ when no weight vector is feasible.

Formalization targets

Goal: Theorem 2 (p. 11)

\lim_{n\to\infty}P\big(\underline Z_n(x)\le Z_0(x)\le\overline Z_n(x)\big)=1-\alpha .

The event is two-sided and joint. No rate is claimed.

Milestones

Proposition 2 (p. 23). For every data vector and $\kappa\ge0$ ,

\min_{\mathcal U_n(\kappa/(2n))}\textstyle\sum_i w_iz_i\le\mu\le\max_{\mathcal U_n(\kappa/(2n))}\sum_i w_iz_i\iff -2\log R(\mu)\le\kappa .

Theorem 1, the empirical likelihood theorem (p. 10). $-2\log R(Z_0(x))\Rightarrow\chi^2_1$ .
The pointwise steps of the paper's proof of Theorem 1 (the proof of Theorem 5 with a one-point index set): Lemma 3 (p. 38), $\max_{i\le n}|Y_i|=o(n^{1/2})$ a.s. for square-integrable i.i.d. $Y_i$ ; the closed form (49)–(50) (pp. 25–26) of the optimal weights; the multiplier bound (52) (p. 27); the expansion (68) (p. 30), $-2\log R=n s^{-1}\bar h^2+o_p(1)$ .

Significance

Theorem 2 says that a robust optimization formulation with a data-driven Burg ball of radius $\chi^2_{1,1-\alpha}/(2n)$ yields an asymptotically exact $(1-\alpha)$ confidence interval for an expected loss, independently of the support size of $\xi$ . Proposition 2 is the bridge: it identifies the DRO interval with the empirical likelihood confidence region, so any distributional result on $-2\log R$ transfers to the DRO bounds. This is the pointwise basis of the paper's later results on feasibility of chance and expectation constraints.

The result is proved in the paper, and Theorem 1 is classical. To our knowledge none of these statements has a machine-checked proof. Formalizing them requires the empirical likelihood theorem in Lean, which is reusable well beyond DRO (empirical likelihood tests and intervals for means). The Open platform theorem GenEmpLik.Coverage.theorem_3 (Duchi, Glynn and Namkoong) implies the goal when its decision set is the single point $\{x\}$ and its generator is $2\varphi$ with radius $\chi^2_{1,1-\alpha}$ ; it is a different, more general statement and is not proved. Likewise the Open GenEmpLik.Expansion.lemma_7 implies Lemma 3, and the Proved NumStochOpt.ListScheduling.lemma_8_1_i_max_over_sqrt_ae gives Lemma 3 after passing to $|Y_i|$ .

Difficulty

Proposition 2 is a finite-dimensional convexity statement, but it needs attainment of the minimum defining $-2\log R$ , which holds only because the objective blows up at the boundary of the simplex. The central difficulty is Theorem 1. The optimal weights are explicit only through a Lagrange multiplier $\lambda$ that solves a nonlinear equation; to expand $-2\log R$ one must first show $\lambda=O_p(n^{-1/2})$ , which requires controlling the largest observation by Lemma 3 together with the law of large numbers for $s$ , and then bound the cubic Taylor remainder of $\log(1+\lambda\tilde h_i)$ uniformly in $i$ . A direct appeal to the central limit theorem for the sample mean does not suffice, since $-2\log R$ is an implicitly defined optimal value, not a smooth function of the mean.

Formalization scope

The sample is a sequence ξ : ℕ → Ω → Ξ, measurable, mutually independent and identically distributed, indexed from $0$ ; the size- $n$ sample is fun i : Fin n => h x (ξ i ω).
The moment assumption is MemLp (h x ∘ ξ 0) 2 together with 0 < variance. Positive variance cannot be dropped: for a constant loss the coverage is $1$ .
The quantile is pinned by gaussianReal 0 1 {y | y^2 ≤ q} = ofReal (1 - α) with $0<\alpha<1$ ; it is not a free parameter, and it is not the normal quantile.
The upper bound is the published GenEmpLik.Expansion.robustMean burg (q/2) (its ball has radius $\rho/n$ , so $\rho=q/2$ ); the lower bound is its infimum twin robustLower. The ball uses the published probUncertaintySet and phiDiv.
The Burg generator is $+\infty$ at $t\le0$ , and the statistic elStat minimizes over strictly positive weights with the empty infimum equal to $+\infty$ . Lean's junk value $\log 0=0$ therefore never enters: a formalization with $w_i\ge0$ and real logarithms would admit boundary weights with spurious finite divergence and is ruled out. For $n\ge1$ the value sets of the DRO bounds are nonempty and bounded, so the real infimum and supremum are not junk values.
The decision set $\Theta$ is dropped (the statements are pointwise in $x$ ). Theorem 1 is stated as convergence of distribution functions at every $t$ , which is equivalent to $\Rightarrow\chi^2_1$ since the limit is continuous. Proposition 2 is stated for general $\kappa\ge0$ and every data vector, as displayed on p. 11. Milestones (49)–(50), (52), (68) are the one-point ( $\Theta=\{x\}$ ) specialisations of the proof of Theorem 5.
Probabilities of events are outer probabilities; no measurability of events is assumed, as the paper ignores these issues (p. 14).
Not posed: the headline Theorem 4 (uniform calibration over $\Theta$ by the quantile of a $\chi^2$ -process supremum), Theorem 5 and Lemma 2, which need Donsker classes and weak convergence in $\ell^\infty(\Theta)$ , for which Mathlib has no substrate.

Contributions welcome: proofs of Proposition 2 and Lemma 3 (from the Proved reference), the KKT analysis (49)–(52), and a Lean empirical likelihood theorem.

Selected references

H. Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization, arXiv:1605.09349v1, 2016; Operations Research 67(4), 2019. https://arxiv.org/abs/1605.09349v1
A. B. Owen, Empirical likelihood ratio confidence intervals for a single functional, Biometrika 75(2), 1988. https://doi.org/10.1093/biomet/75.2.237
A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
J. C. Duchi, P. W. Glynn, H. Namkoong, Statistics of robust optimization: a generalized empirical likelihood approach, Mathematics of Operations Research 46(3), 2021. https://arxiv.org/abs/1610.03425

13 thms2 active usersReviewed

Algorithmic Game Theory Probability·Captain: mikedeng1

Posted Price Mechanisms and Optimal Threshold Strategies for Random Arrivals I: Under Random Arrival Order, Nonadaptive Thresholds Earn a 1 − 1/e Fraction of E[max Xᵢ]Research Paper

Motivation

In a prophet inequality, a gambler sees prizes one at a time and must decide when to stop, while a prophet knows every realization and takes the largest. A stopping guarantee compares the gambler’s expected prize with the prophet’s. The order of arrival changes the problem: here the prizes are independent but can have different distributions, and every permutation of their arrival is equally likely. Before seeing any prize, the gambler chooses a threshold for each distribution and accepts the first prize above its threshold. Such a rule has no need to update thresholds after observing rejections. Correa, Foncea, Hoeksma, Oosterwijk, and Vredeveld prove that this restricted rule still earns at least a $1-1/e$ fraction of the prophet’s expected maximum (Theorem 1, pp. 1455, 1459).

The random-arrival stopping model also supplies guarantees for posted-price mechanisms. A posted price gives a buyer a take-it-or-leave-it offer; the first buyer who accepts ends the sale. The paper explains the connection between its stopping rules and expected revenue under random buyer arrival (§1.1 and §5). This mission formalizes the stopping theorem itself, which is the mathematical guarantee used before that economic translation.

Setting

Let $n\ge1$ , and let $X_1,\ldots,X_n$ be independent, nonnegative real random variables with known, possibly different distributions. Their realizations arrive in a uniformly random order. A nonadaptive threshold rule chooses constants $\tau_i\in[0,\infty]$ before any realization is observed. It accepts the first arriving index $i$ with $X_i>\tau_i$ and receives $X_i$ . If no prize crosses its threshold, its reward is zero. An infinite threshold deliberately excludes an index. The strict comparison matches Theorem 1, even though an earlier description in §1.2 uses a weak comparison (pp. 1454–1455).

For fixed realized prizes, write $Y_i=\mathbf1_{\{X_i>\tau_i\}}$ . Conditional on the set of indices with $Y_i=1$ , each accepted index is equally likely to arrive first. The conditional expected reward is therefore

R_\tau(X)=\frac{\sum_{i=1}^{n}X_iY_i}{\sum_{i=1}^{n}Y_i},\qquad 0/0:=0.

The prophet benchmark is $X^*=\max_i X_i$ . The theorem compares $\mathbb E R_\tau(X)$ with $\mathbb E X^*$ , including distributions for which either expectation may be infinite. The variables need no common distribution and no atomlessness assumption.

The paper’s main supporting result is the Bernoulli Selection Lemma. It starts with independent Bernoulli indicators $Y_i$ of success probabilities $q_i$ , fixed real prizes $b_i$ , and a chosen subset $S$ . Its payoff is the average $\sum_{i\in S}b_iY_i/\sum_{i\in S}Y_i$ , again zero when the denominator vanishes. The lemma compares the best subset with a finite linear optimization problem over $0\le z_i\le q_i$ and $\sum_i z_i\le1$ (Lemma 1, p. 1455).

Formalization targets

Nonadaptive threshold guarantee

The goal is the exact constant of Theorem 1:

\exists\tau\in[0,\infty]^n:\quad \mathbb E R_\tau(X)\ \ge\ (1-e^{-1})\,\mathbb E X^*.

The quantifiers range over every finite nonempty family of independent nonnegative variables. The thresholds are deterministic and indexed by the distributions, and the assertion covers atoms as well as continuous laws. This is the paper’s headline nonadaptive result (Theorem 1, p. 1459).

Bernoulli selection and comparison steps

The milestone list includes the paper’s multilinear formulation (4), its substitution (5), Proposition A.1, Lemmas 2 and 3, and the Bernoulli Selection Lemma. The latter states, in particular, that the maximum expected selected average dominates $(1-e^{-1})$ times the optimum over feasible $z$ . Two further milestones express the decomposition of the expected maximum and the upper-tail comparison used for continuous distributions (§2–3 and Appendix A). These targets fix the finite selection problem and the probabilistic quantities that the goal must connect.

Significance

The guarantee identifies what fixed, distribution-specific thresholds can achieve under random arrival: the expected accepted prize reaches a constant fraction of the prophet’s benchmark for every collection of independent nonnegative distributions. The paper also gives examples showing why a rule that keeps every positive prize is inadequate and studies where the $1-e^{-1}$ factor is tight (§2.1 and §3.1). These are claims about the performance of a restricted class of stopping rules, not about an optimal adaptive strategy.

The paper proves Theorem 1; a machine-checked proof of this mission’s goal remains to be supplied. The finite Bernoulli model, its subset optimum, and the nonnegative expectation conventions would be reusable for other random-order stopping and allocation results. This mission makes the paper’s claimed constants, event comparisons, and boundary cases explicit in the theorem statements so a later proof has a fixed target.

Difficulty

Taking the first value above a single low threshold can accept a modest prize before a rare large one arrives. Raising every threshold can instead reject too many prizes. The paper’s example with a constant prize and a rare large prize shows that accepting all available values does not meet the claimed factor (p. 1460). The difficulty is obtaining one set of fixed thresholds that balances those risks across different distributions, while the benchmark selects the largest realization after seeing them all. The Bernoulli selection inequality carries the sharp constant; connecting it to general distributions must also account for ties and atoms.

Formalization scope

Lean represents the index set by Fin n with $n\ge1$ , so its index zero is the paper’s index one. The existing published definition SamuelCahnProphet.Median.Setting.maxX supplies the sample maximum; this mission defines the strict accepted set and its real-valued reward ratio. Thresholds live in $[0,\infty]$ because the paper explicitly uses $\infty$ to exclude a variable. Expectations are nonnegative extended integrals of ENNReal.ofReal, preserving infinite values and avoiding a default zero for nonintegrable real integrals. The source’s nonnegativity assumption is represented almost surely, which is enough for these expectations and does not restrict the distributions further.

The Bernoulli law is a finite product formula. Its probabilities lie in $[0,1]$ , while prizes are arbitrary real numbers as in the printed lemma. The feasibility condition includes $z_i\ge0$ : these variables are probabilities, and allowing negative values would change the optimization problem. The finite subset optimum is an attained maximum. Proposition A.1 is stated for $M\ne\varnothing$ ; an empty $M$ contradicts the budget conclusion for $a>0$ . It also includes the printed $a=0$ case. Lemma 2 includes $y=1$ as printed: the removable division by zero in (6) is assigned its continuous value $2/e$ . The comparison milestones for continuous distributions assume atomlessness explicitly; the goal does not.

The accepted set depends only on fixed thresholds and the realized values. It cannot depend on the sampled arrival order or on prior observations. A constant choice such as accepting every positive prize does not prove the target guarantee. Contributions that establish the finite Bernoulli selection result, its analytic bounds, the random-order reward identity, or the passage from continuous to arbitrary distributions all serve the stated goal. The random-order identity and the discontinuous case are further work beyond the current milestone list.

Selected references

José Correa, Patricio Foncea, Ruben Hoeksma, Tim Oosterwijk, and Tjark Vredeveld, Posted Price Mechanisms and Optimal Threshold Strategies for Random Arrivals, Mathematics of Operations Research 46(4), 1452–1478, 2021. DOI: 10.1287/moor.2020.1105.

12 thms2 active usersReviewed

Completed

Mechanism Design Probability Stochastic Systems·Captain: mikedeng1

Pricing and Matching with Forward-Looking Buyers and Sellers 1: Waiting-Adjusted Fixed Prices with Greedy Matching Earn at Least 1 − (1 + 2(b+h)T/(3(p−w)))/√µ* of the Fluid Profit BoundResearch Paper

Why this market matters

An intermediary such as a ride platform must attract buyers and sellers who arrive at different times. A buyer may wait for a seller; a seller may wait for a buyer. Both sides can choose when to request a match, so an ask price and a bid price affect participation as well as the intermediary's margin. Chen and Hu study whether a simple posted-price policy remains profitable despite this waiting and the uncertainty of arrivals. Their submitted manuscript proves a finite-market guarantee and an asymptotic rate for the policy used here. The proof appears in its Supplemental Note, while the model and theorem are in the main text.

Market and benchmarks

Buyers arrive during a horizon $[0,T]$ as a Poisson process of rate $\lambda^d>0$ , and sellers arrive independently at rate $\lambda^s>0$ . A buyer's valuation $v$ has density $f^d$ on $[\underline v,\overline v]$ and a seller's cost $c$ has density $f^s$ on $[\underline c,\overline c]$ . Marks are independent of arrival times. A buyer and a seller each trade at most one unit. If they wait after arrival, they incur costs $b$ and $h$ per unit time, respectively. The paper assumes regularity: the buyer's virtual value $V^d(v)=v-\bar F^d(v)/f^d(v)$ and the seller's virtual cost $V^s(c)=c+F^s(c)/f^s(c)$ are weakly increasing on their supports. Here $\bar F^d=1-F^d$ .

A clairvoyant assignment knows all arrivals through $T$ . For each possible buyer–seller pair it assigns virtual surplus $V^d(v)-V^s(c)$ less the waiting cost determined by their arrival order. It chooses a partial matching with greatest total value, denoted $\bar J(H^T)$ . A separate fluid program chooses a measurable, nonnegative pair of price trajectories that clears demand and supply at every time. Its optimal value is $\bar J^*$ . These are different objects: $\bar J(H^T)$ is random and uses indivisible agents, whereas $\bar J^*$ is a deterministic continuous-flow optimum. Lemma 2 of the manuscript compares their values in expectation.

Let $\mu^*$ be the greatest volume in $[0,\min\{\lambda^dT,\lambda^sT\}]$ with nonnegative marginal virtual surplus. The buyer and seller prices $p^*,w^*$ are inverse-distribution prices at that volume. Proposition 1 states that these constant prices attain the fluid optimum and $\bar J^*=(p^*-w^*)\mu^*$ .

Formalization targets

The greedy matching policy pairs requests first come, first served. Under the waiting-adjusted fixed-price policy, a buyer's posted ask is $p^*$ minus $b$ times a conditional expected wait per match probability; the seller's posted bid is $w^*$ plus the corresponding $h$ term. The buyer adjustment is conditioned on the observed pre-arrival inventory signal. Agents request immediately exactly when their valuation or cost crosses the base-price threshold. The policy's expected profit $J$ is computed from posted prices paid by successfully matched agents.

The first target is the paper's finite-market bound:

\frac{J}{\bar J^*}\ge 1-\left(1+\frac{2(b+h)T}{3(p^*-w^*)}\right)\frac{1}{\sqrt{\mu^*}}.

When $J\ge0$ , the benchmark comparison also gives $J/\mathbb E[\bar J(H^T)]\ge J/\bar J^*$ . For scaled systems with arrival rates $n^{\alpha_d}\lambda^d$ and $n^{\alpha_s}\lambda^s$ , where both exponents are positive, the second target is a constant $C$ independent of $n$ such that

\frac{J^{(n)}}{\bar J^{*,(n)}}\ge 1-\frac{C}{\sqrt{n^{\min\{\alpha_d,\alpha_s\}}}}\qquad(n\ge1).

The milestone list follows the source's Proposition 1, Lagrangian relaxation, Lemma 2, Poisson request counts, policy profit identity, Gallego–van Ryzin moment bound, and Lemma S.5 on arrival-rate monotonicity. The last three supply the finite bound and its scaling statement in the Supplemental Note.

What the result gives

The finite bound quantifies the cost of using fixed base prices and greedy matching instead of the fluid ideal. Its two terms separate the loss from random mismatch and the extra waiting adjustment. The scaled bound says that, as both sides' arrival rates grow, the fraction of the fluid value lost by this policy vanishes at a rate governed by the slower-growing side. This offers a concrete reason to use a simple policy when the market is large, while keeping the smaller-market correction visible.

The paper already proves these claims. This mission asks for machine-checked proofs of their precise statements. The fluid optimizer, the clairvoyant matching problem, the marked Poisson arrival model, and the policy-profit identity are reusable mathematical objects beyond this theorem. The positive-part moment bound is an already published theorem and is referenced rather than posed again.

Where the argument is difficult

The obvious comparison between posted-price profit and fluid revenue misses the cost of requests that wait or never match. The price corrections themselves are conditional expectations divided by conditional match probabilities; their effect cannot be captured by simply subtracting a constant waiting charge. The proof must connect those corrections to the time integral of the queue imbalance, then control the imbalance of two Poisson request streams. A second difficulty is that the fluid optimum and the expected clairvoyant optimum are defined through different feasible sets, so their comparison needs a separate relaxation argument. These obstacles are visible in the source's proof of Lemma 2 and Theorem 2.

Formalization scope

The density and virtual-value environment is the published bilateral-trade definition, imported through a local name alias required by the frozen shared market module. Lean represents arrivals by independent Poisson counts and independent identically distributed time-and-value marks. This is equal in law to the paper's homogeneous marked Poisson processes on $[0,T]$ . Arrival time marks are uniform probability laws, and valuation and cost marks use the source densities. Simultaneous requests are ordered by index; such ties have probability zero. The deterministic program ranges over measurable, nonnegative, market-clearing paths with interval-integrable objective terms. Its value is the supremum of their objectives, not a formula involving $p^*$ and $w^*$ ; Proposition 1 must establish that formula. The clairvoyant value uses the published partial-assignment-game worth, so negative-weight pairs may remain unmatched.

The density functions are continuous on their supports, an explicit addition needed for the inverse prices and maximum volume used by Proposition 1. The lower support endpoints are nonnegative so the constant prices belong to the nonnegative fluid price domain; this fills an implicit domain convention in the manuscript. For Theorem 2 the overlap condition is strict, $\underline c<\overline v$ , ensuring positive $\mu^*$ and $p^*-w^*$ . The printed chain comparing $J/\mathbb E[\bar J]$ and $J/\bar J^*$ is stated under $J\ge0$ : when the numerator is negative, the claimed direction fails. Both expectations used as finite numbers are accompanied by integrability conclusions. Division by a zero match probability at the terminal time uses a zero convention on a set of arrival times with probability zero.

The policy model builds in the myopic request behavior that Theorem 1 identifies as an equilibrium; its strategic proof is outside this mission. The policy profit is the expectation of actual posted-price payments, and the waiting compensations are literal tagged-arrival conditional ratios. Contributions that prove the inverse-distribution properties, Poisson thinning, queue profit identity, fluid optimization, or final moment estimate all address parts of the stated target.

Selected references

Y. Chen and M. Hu, Pricing and Matching with Forward-Looking Buyers and Sellers, Manufacturing & Service Operations Management 22(4), 2020; submitted manuscript, SSRN 2859864.

12 thms2 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

An Augmented Lagrangian Based Algorithm for Distributed Nonconvex Optimization 1: With ρ = 0, the ALADIN Dual Update Equals the Levenberg–Marquardt Dual Newton Step of Dual DecompositionResearch Paper

Motivation

Large optimization problems often split into blocks owned by different agents (subsystems of a power grid, vehicles in a formation, scenarios of a stochastic program) that are coupled only through a few linear constraints. Distributed optimization methods solve such problems by letting each agent work on its own block and exchanging a small amount of information, typically a vector of prices for the coupling constraints. The classical method of this kind is dual decomposition (Everett 1963; Bertsekas and Tsitsiklis, Parallel and Distributed Computation, 1989): fix the prices, let every agent solve its own subproblem, then update the prices by a gradient or Newton step on the concave dual function. Dual decomposition is reliable for strictly convex problems but has no convergence guarantee for nonconvex ones.

Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton), which adds a proximal term to the agents' subproblems and replaces the price update by a coupled equality-constrained quadratic program. ALADIN is used in distributed model predictive control and in power-system optimization. Remark 4.2 and Appendix A of the paper explain where it sits relative to the classical method: if the proximal term is switched off ( $\rho = 0$ ), the price update of ALADIN is exactly a regularized Newton step of dual decomposition. Lemma 5 is the precise statement of that equivalence, and it is the goal of this mission.

Setting

The problem (1.1) has $N$ blocks $x_i\in\mathbb R^n$ :

\min_x\ \sum_{i=1}^N f_i(x_i)\quad\text{s.t.}\quad \sum_{i=1}^N A_i x_i = b,\qquad h_i(x_i)\le 0,

with $f_i:\mathbb R^n\to\mathbb R$ , $h_i:\mathbb R^n\to\mathbb R^{n_h}$ twice continuously differentiable, $A_i\in\mathbb R^{m\times n}$ and $b\in\mathbb R^m$ . One iteration of Algorithm 2 (ALADIN) starts from a primal point $x$ and prices $\lambda\in\mathbb R^m$ and does the following.

Each agent solves the decoupled problem $\min_{y_i} f_i(y_i) + \lambda^\top A_i y_i + \frac\rho2\|y_i-x_i\|^2_{\Sigma_i}$ subject to $h_i(y_i)\le 0$ , returning a minimizer $y_i$ and a multiplier $\kappa_i\ge 0$ . With $\rho = 0$ this is the dual-decomposition subproblem (A.2).
Each agent forms the active-constraint Jacobian $C^*_i$ (rows $\nabla(h_i)_j(y_i)^\top$ for active $j$ , zero rows otherwise), chooses an approximation $C_i$ and a symmetric Hessian approximation $H_i$ , and computes the modified gradient $g_i = \nabla f_i(y_i) + (C^*_i - C_i)^\top\kappa_i$ .
For a parameter $\mu>0$ , a coordinator solves the coupled QP (3.3)

\min_{\Delta y, s}\ \sum_i\Big\{\tfrac12\Delta y_i^\top H_i\Delta y_i + g_i^\top\Delta y_i\Big\} + \lambda^\top s + \tfrac\mu2\|s\|_2^2\ \ \text{s.t.}\ \ \sum_i A_i(y_i+\Delta y_i) = b + s\ \mid\ \lambda_{\mathrm{QP}},\quad C_i\Delta y_i = 0,

and the new prices are $\lambda^+ = \lambda + \alpha_3(\lambda_{\mathrm{QP}}-\lambda)$ .

On the dual-decomposition side, $\nabla V(\lambda) = \sum_i A_i y_i - b$ (A.3) is the gradient of the dual function at $\lambda$ , and the (inexact) dual Newton step (A.4) with a symmetric negative semidefinite scaling matrix $M$ and step size $\alpha\in(0,1]$ is

\lambda^+_{\mathrm{DD}} = \lambda - \alpha\Big(M - \frac1\mu I\Big)^{-1}\nabla V(\lambda),

where $1/\mu$ plays the role of a Levenberg–Marquardt regularization parameter.

Formalization targets

Goal: Lemma 5 (p. 1123)

Assume every $f_i$ strictly convex, every $h_i$ convex, $C_i$ of full row rank, $H_i$ positive definite, $\rho = 0$ and $\alpha_3 = \alpha$ . Then for every $\mu>0$ , with

M = -\sum_{i=1}^N A_i\Big[H_i^{-1} - H_i^{-1}C_i^\top\big[C_iH_i^{-1}C_i^\top\big]^{-1}C_iH_i^{-1}\Big]A_i^\top,

the matrix $M - \frac1\mu I$ is invertible and

\lambda^+ = \lambda^+_{\mathrm{DD}} .

Milestones (the steps of the proof, pp. 1123–1124)

Slack elimination: $\min_s \frac\mu2\|s\|_2^2 - (\lambda_{\mathrm{QP}}-\lambda)^\top s = -\frac1{2\mu}\|\lambda_{\mathrm{QP}}-\lambda\|_2^2$ , attained only at $s = (\lambda_{\mathrm{QP}}-\lambda)/\mu$ .
Stationarity: with $\rho = 0$ , $0 = \nabla f_i(y_i) + A_i^\top\lambda + (C^*_i)^\top\kappa_i = g_i + A_i^\top\lambda + C_i^\top\kappa_i$ .
Explicit minimization over $\Delta y$ : for $H\succ 0$ and $C$ of full row rank, $-Pw$ with $P = H^{-1} - H^{-1}C^\top(CH^{-1}C^\top)^{-1}CH^{-1}$ minimizes $\frac12\Delta^\top H\Delta + w^\top\Delta$ on $\{C\Delta = 0\}$ , with value $-\frac12 w^\top Pw\le 0$ .
Argmax display: for $M$ symmetric negative semidefinite, $\lambda - (M - \frac1\mu I)^{-1}g$ is the unique maximizer of $\frac12(\nu-\lambda)^\top M(\nu-\lambda) + \nu^\top g - \frac1{2\mu}\|\nu-\lambda\|_2^2$ .

Significance

The result. Lemma 5 places ALADIN on a known map. With $\rho=0$ it inherits the convergence theory of dual decomposition for strictly convex problems for small step sizes, independently of how crude the approximations $H_i$ , $C_i$ are, as long as $H_i\succ 0$ . It also reinterprets the augmented-Lagrangian parameter $\mu$ as the inverse of a dual Levenberg–Marquardt parameter, and it isolates the proximal term $\frac\rho2\|y_i - x_i\|^2_{\Sigma_i}$ as the only ingredient that distinguishes ALADIN from dual decomposition and makes the nonconvex analysis of the paper possible.

Formalizing it. The lemma is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof certifies an identity whose printed form contains a typo (see below), and produces reusable linear-algebra facts: the closed-form solution of an equality-constrained strictly convex quadratic program via the reduced inverse $P$ , the semidefiniteness of $P$ , and the closed-form maximizer of a regularized concave quadratic.

Difficulty

The proof is a chain of exact eliminations, and the work is in carrying each one out without losing a sign or a hypothesis. The step most easily done wrong is the minimization over $\Delta y$ : the constraint $C_i\Delta y_i = 0$ couples the block coordinates, the minimizer is expressed through the inverse of $C_iH_i^{-1}C_i^\top$ (invertible only because $C_i$ has full row rank). A second trap is the sign convention for $\lambda_{\mathrm{QP}}$ : it must agree with footnote 4 ( $\lambda + \mu s - \lambda_{\mathrm{QP}} = 0$ ), or the conclusion flips. The tempting shortcut of treating the max–min dual of (3.3) abstractly runs into the fact that strong duality and attainment are not free; working from the KKT system of (3.3) avoids that.

Formalization scope

Vectors are Fin n → ℝ; blocks are indexed by Fin N; matrices are Mathlib Matrix over Fin index types; the gradient is the vector of partial derivatives computed with fderiv. The step-1 output $(y_i,\kappa_i)$ is a local minimizer of the decoupled problem together with KKT multipliers (the paper assumes LICQ for the lower-level constraints). The QP (3.3) and $\lambda_{\mathrm{QP}}$ enter through the KKT system of (3.3), not through a closed-form expression: defining $\lambda_{\mathrm{QP}}$ or $\Delta y$ by the formula of the conclusion would make the goal true by definition and is ruled out. $\nabla V(\lambda)$ is the formula (A.3); that it is the gradient of the dual function is a cited fact the lemma does not use. The invertibility of $M - \frac1\mu I$ is part of the conclusion, because Mathlib's matrix inverse returns $0$ on a singular matrix.

Correction of (A.6). As printed, (A.6) has the bracket $[C_iH_iC_i^\top]^\dagger$ . This is a typo for $[C_iH_i^{-1}C_i^\top]^\dagger$ , as in (A.5) on the same page and as the explicit minimization over $\Delta y$ forces; with the printed bracket the identity fails already for $N = 1$ , $H_1 = \mathrm{diag}(1,2)$ , $C_1 = (1,1)$ , $A_1 = I$ . The mission uses the corrected matrix and writes the pseudo-inverse as an inverse, which it is under the hypotheses.

The hypotheses of strict convexity of $f_i$ , convexity of $h_i$ and $\alpha\in(0,1]$ are kept as on the page although the identity does not use them. The related platform draft GoldfarbIdnani.DualQP.properties_2_6_to_2_9 (not proved) states properties of the same reduced inverse; it is not imported. Proofs of the four milestones and of the goal are welcome; the milestones are self-contained matrix and calculus facts and can be attacked independently.

Selected references

B. Houska, J. Frasch, M. Diehl, An augmented Lagrangian based algorithm for distributed nonconvex optimization, SIAM J. Optim. 26(2) (2016), 1101–1127. https://doi.org/10.1137/140975991
D. P. Bertsekas, J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice-Hall, 1989.
H. Everett, Generalized Lagrange multiplier method for solving problems of optimum allocation of resources, Oper. Res. 11(3) (1963), 399–417. https://doi.org/10.1287/opre.11.3.399
D. P. Bertsekas, Nonlinear Programming, 2nd ed., Athena Scientific, 1999.

7 thms2 active usersReviewed

Algorithmic Game Theory·Captain: mikedeng1

On the Complexity of Nash Equilibria and Other Fixed Points 3: In Every Nash Equilibrium of Bubelis's Gadget the Primary Player Plays 0 with Probability α, the Unique Root of f in [0, 1]Research Paper

Motivation

For games with three or more players, Nash equilibria can be irrational, so they cannot in general be computed exactly. Bubelis made this precise: any real root of any univariate polynomial arises as the probability of a particular strategy, or the payoff of a particular player, in a Nash equilibrium of a three-player game whose payoffs depend on the coefficients of the polynomial (Bubelis 1979).

Etessami and Yannakakis (SIAM J. Comput. 39 (2010)) restate Bubelis's construction as Lemma 7, in a form that controls the equilibrium probabilities rather than a payoff, and that guarantees the equilibrium is unique. They use it, for linear polynomials, as the single gadget behind every arithmetic operation in their reduction from PosSLP and SQRT-SUM to deciding properties of the unique Nash equilibrium of a three- or four-player game (their Theorem 4). The uniqueness clause is what makes the composed game itself have a unique equilibrium.

1951: Nash proves every finite game has an equilibrium in mixed strategies.
1979: Bubelis shows that every real algebraic number is an equilibrium probability or payoff of some three-player game (Theorem 2 of the cited paper).
2007–2010: Etessami and Yannakakis restate the construction as Lemma 7, with uniqueness and full support of the equilibrium, and use it to prove PosSLP- and SQRT-SUM-hardness of Nash equilibrium problems (FOCS 2007; journal version 2010).

Setting

Fix an integer $m \ge 0$ and real coefficients $c_0, \dots, c_m$ , and let

f(x) = c_0 x^m + c_1 x^{m-1} + \dots + c_m = \sum_{j=0}^m c_j\, x^{m-j},

so $c_j$ is the coefficient of $x^{m-j}$ ; the leading coefficient may vanish.

The gadget $G_f$ is a game with three players. The primary player 1 has the strategies $0, 1$ ; the auxiliary players 2 and 3 each have the strategies $0, 1, \dots, m$ . For a pure profile $s = (s_1, s_2, s_3)$ , and with $\chi(P)$ the indicator of a predicate $P$ , the payoffs are

h^f_1(s) = \begin{cases} c_{s_2} & s_1 = 1 \\ 0 & s_1 = 0 \end{cases}, \qquad h_2(s) = \chi(s_2 = s_3),

h_3(s) = \chi\big(s_2 + 1 \equiv s_3 \bmod (m+1)\big) - \chi(s_1 = 0)\,\chi(s_2 = s_3) - \chi(s_1 = 1)\,\chi(s_3 = 0).

The auxiliary payoffs do not depend on $f$ and take values in $\{0, 1, -1\}$ .

A mixed profile $x = (x_1, x_2, x_3)$ assigns to each player $p$ a probability vector $x_p$ on its strategies; the players randomize independently. Player $p$ 's expected payoff $u_p(x)$ is the expectation of its payoff under the product distribution, and $u_p((p:j); x_{-p})$ is its expected payoff when it switches to the pure strategy $j$ . A Nash equilibrium is a mixed profile in which no player can raise its expected payoff by switching unilaterally to any other mixed strategy. A profile is fully mixed if every pure strategy of every player has positive probability. Throughout, $\xi = x_1(0)$ , and $v_2$ , $v_3$ are the equilibrium payoffs of players 2 and 3.

Formalization targets

Goal: Lemma 7

Assume $f(0) \le 0$ , $f(1) \ge 0$ , and that $f$ has a unique root $\alpha$ in $[0,1]$ . Then every Nash equilibrium $x$ of $G_f$ satisfies

x_1(0) = \alpha, \qquad x_1(1) = 1 - \alpha,

and if $\alpha \ne 0$ and $\alpha \ne 1$ , then $G_f$ has exactly one Nash equilibrium, and it is fully mixed.

Milestones (proof of Lemma 7, p. 26)

In any finite game, at a Nash equilibrium, $u_p((p:j); x_{-p}) \le u_p(x)$ , with equality when $x_p(j) > 0$ .
In every Nash equilibrium of $G_f$ : $v_2 > 0$ and $v_3 \ge 0$ .
In every Nash equilibrium of $G_f$ : $x_2(j) = \xi^{m-j} \big/ \sum_{i=0}^m \xi^i$ for all $j$ .
In every Nash equilibrium of $G_f$ : $u_1((1:1); x_{-1}) = f(\xi) \big/ \sum_{i=0}^m \xi^i$ .
Under the hypotheses of Lemma 7 and $\alpha \ne 0$ : $x_3(j) = 1/(m+1)$ for all $j$ .

Milestones 2–4 hold for every coefficient vector; only milestone 5 and the goal use the hypotheses on $f$ .

Significance

The lemma is the arithmetic engine of the hardness results of Etessami and Yannakakis: a polynomial equation in one unknown is solved, exactly and uniquely, by the equilibrium of a fixed-size game whose auxiliary payoffs do not depend on the equation. With $f$ linear, the gadget implements addition, multiplication and division of probabilities in $(0,1)$ ; with higher degree it implements roots and fractional powers. Without the uniqueness clause, the composed games of Theorem 4 could have spurious equilibria, and the reduction would not apply to games promised to have a unique equilibrium.

The result is proved in the paper (pp. 25–26, following Bubelis). As far as is known, no part of it is machine-checked: there is no formal statement of Bubelis's gadget, and the support property of Nash equilibria is not on the platform in this vocabulary. This mission produces the first formal statement and proof of the gadget's equilibrium characterization, including the existence half of "has a unique Nash equilibrium", which the paper takes from Nash's theorem but which here is a concrete profile to check.

Difficulty

The gadget's equilibria are those of a three-player game, so the payoffs are cubic in the probabilities and no linear-programming argument applies. The obvious first idea, writing down the indifference conditions of players 2 and 3 and solving them, presupposes that every strategy of player 2 is played; nothing guarantees that in advance, and the profiles in which some strategies are unplayed have to be excluded. The boundary cases $\xi = 0$ and $\xi = 1$ are not covered by an indifference argument for the primary player and need the sign conditions $f(0) \le 0$ and $f(1) \ge 0$ separately. The strategy of player 3 is pinned down only when $\alpha \neq 0$ , which is why the uniqueness part of the lemma excludes the endpoints. Finally, existence of the equilibrium is part of the statement and cannot be delegated to Nash's theorem, which is not available on the platform.

Formalization scope

The game uses the published vocabulary agt_games (mixed profiles as weight functions, AGT.expectedPayoff, AGT.IsMixedNash with mixed deviations) and DGPNash.NashMap.purePayoff for $u_p((p:j); x_{-p})$ . The players are a three-element type primary | aux2 | aux3; strategies are Fin 2 and Fin (m+1), 0-based as on the page. The coefficients are c : Fin (m+1) → ℝ and $f$ is the explicit sum $\sum_j c_j \xi^{m-j}$ with natural-number exponent; the congruence $s_2 + 1 \equiv s_3$ is addition in Fin (m+1); $\xi^0 = 1$ for every $\xi$ , including $0$ .

Explicit readings committed to:

"has a unique root $\alpha$ in $[0,1]$ " is a named $\alpha$ with $0 \le \alpha \le 1$ , $f(\alpha) = 0$ , and $\beta = \alpha$ for every root $\beta \in [0,1]$ ;
"the game has a unique Nash equilibrium" is existence and uniqueness (∃! over mixed profiles);
"the NE is fully mixed" applies to all three players;
coefficients are real, generalizing the paper's rationals; the degree is at most $m$ ;
the support property is stated for an arbitrary finite game;
the last two clauses of Lemma 7 (auxiliary payoffs independent of $f$ , values in $\{0,1,-1\}$ ; primary payoff $c_{s_2}$ or $0$ ) hold by the definition of the gadget and are not separate theorems.

The goal is not trivialized by a pure-strategy notion of equilibrium (deviations are mixed), by dropping uniqueness of the root (without it $x_1(0) = \alpha$ is false), or by reading "unique equilibrium" as uniqueness alone. For $m = 0$ the hypotheses cannot hold, as on the page.

A complete development needs the support property (reusable for any finite game), the linearity of expected payoff in one player's strategy, and finite-sum manipulations for the geometric weights $\xi^{m-j}$ . Contributions of general lemmas about AGT.IsMixedNash and purePayoff are welcome and reusable well beyond this mission.

Selected references

K. Etessami and M. Yannakakis, On the complexity of Nash equilibria and other fixed points, SIAM J. Comput. 39(6) (2010) 2531–2597 (author manuscript; Lemma 7, pp. 25–26). https://doi.org/10.1137/080720826
K. Etessami and M. Yannakakis, On the complexity of Nash equilibria and other fixed points (extended abstract), Proc. FOCS 2007. https://doi.org/10.1109/FOCS.2007.48
V. Bubelis, On equilibria in finite games, Int. J. Game Theory 8(2) (1979) 65–79. https://doi.org/10.1007/BF01768703
J. Nash, Non-cooperative games, Ann. of Math. 54(2) (1951) 286–295. https://doi.org/10.2307/1969529

9 thms2 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

Variable Metric Method for Minimization: Davidon's Rank-One Variable-Metric Update Recovers the Inverse Hessian of a Quadratic in N Steps and Then Steps to the Exact MinimumResearch Paper

Motivation

Quasi-Newton methods minimize a smooth function $f:\mathbb R^n\to\mathbb R$ using gradients only, while building up an approximation to the inverse of the Hessian matrix from the changes of gradient they observe. They are the default algorithms of unconstrained nonlinear optimization: BFGS and its limited-memory variant L-BFGS sit inside most numerical optimization libraries and most large-scale fitting codes in statistics and machine learning.

The family starts with William C. Davidon's Argonne report ANL-5990 of 1959, Variable Metric Method for Minimization, rejected by a journal in 1957 and published only in 1991 as the first article of the SIAM Journal on Optimization, with a preface by the author (DOI 10.1137/0801001). The report's body describes a flowchart algorithm; its Appendix describes "a simplified method embodying some of the ideas" of that algorithm, in one and a half pages. That simplified method is what is now called the symmetric rank-one (SR1) update, and the Appendix contains its quadratic-termination property: on a quadratic, after at most $n$ steps the trial matrix equals the inverse Hessian, and the next step lands at the minimum.

Timeline.

1952: Hestenes and Stiefel's conjugate gradient method minimizes a strictly convex quadratic in at most $n$ steps (J. Res. NBS 49); Davidon cites it as [2].
1959: Davidon's ANL-5990, including the Appendix method treated here.
1963: Fletcher and Powell simplify the body's method into the DFP update and prove its quadratic termination with exact line searches (Comput. J. 6).
1967: Broyden's survey of quasi-Newton methods discusses the symmetric rank-one update (Math. Comp. 21); textbooks later analyse it under the name SR1.
1980: Nocedal's limited-storage BFGS, whose termination on quadratics with exact line searches is a separate Prove2Me mission (Math. Comp. 35).

Setting

Vectors are elements of $\mathbb R^n$ and matrices are real $n\times n$ . Fix a symmetric positive definite matrix $G$ and a point $\xi$ , and let

f(x)=\tfrac12\,(x-\xi)^{\mathsf T}G\,(x-\xi)+c ,

a quadratic with constant Hessian $G$ and minimum point $\xi$ . Its gradient is $\nabla(x)=G(x-\xi)$ , display (6) of the Appendix.

The method keeps a point $x_k$ and a symmetric trial matrix $H_k$ , which plays the role of $G^{-1}$ . Write $\nabla_k=\nabla(x_k)$ . One iteration is

x_{k+1}=x_k-H_k\nabla_k \quad\text{(2)},\qquad H_{k+1}=H_k+a_k\,(H_k\nabla_{k+1})(H_k\nabla_{k+1})^{\mathsf T}\quad\text{(3)},

a full step with no line search followed by a symmetric rank-one update. With the two scalars

N_k=\nabla_{k+1}^{\mathsf T}H_k\nabla_{k+1},\qquad M_k=\nabla_{k+1}^{\mathsf T}H_k\nabla_k ,

footnote 2 of the Appendix fixes the coefficient on a quadratic to $a_k=(M_k-N_k)^{-1}$ , which makes the paper's quality measure $\Delta$ of (4) vanish. Write $S_k=x_{k+1}-x_k$ for the step and $D_k=\nabla_{k+1}-\nabla_k$ for the change of gradient. The paper writes $x$ , $H$ , $\nabla$ for the current quantities and $x^{+}$ , $H^{+}$ , $\nabla^{+}$ for the updated ones, and uses the letter $N$ both for the number of variables and for the scalar $N_k$ ; here the number of variables is $n$ .

Formalization targets

Goal: termination in $n$ steps

If $H_0$ is symmetric and $M_k\ne N_k$ for every $k<n$ , then

H_n=G^{-1}\qquad\text{and}\qquad x_{n+1}=\xi .

This is the sentence after (8) on p. 17: "After no more than $N$ steps (for which $\Delta=0$ ), $H$ will equal $G^{-1}$ and the following step will be to the exact minimum."

Milestones

Display (6): the gradient of $f$ is $G(x-\xi)$ .
Display (8): with $a=(M-N)^{-1}$ and $M\ne N$ , $H^{+}GS=H^{+}D=S$ .
Display (7): if $HGu=u$ then $H^{+}Gu=u$ , for any coefficient $a$ .
The sentence "so that $S$ becomes another such eigenvector", read along the run: if $M_i\ne N_i$ for $i<k$ , then $H_kGS_j=S_j$ for every $j<k$ .

Further statements of the Appendix

Condition 1 (p. 16): if $H$ is positive definite and $R^{-1}\le\det H^{+}/\det H\le R$ with $R>1$ , then $H^{+}$ is positive definite.
The constraint remark (p. 17): for any function and any coefficients, if $H_0$ is symmetric and $H_0b=0$ , then every step is perpendicular to $b$ and $b\cdot x_k$ is conserved.
Table (5) (p. 16): for general (non-quadratic) $f$ , the coefficient $a$ that minimizes $\Delta$ subject to condition 1, and the minimum value, on each of five ranges of $M$ .

Significance

The termination theorem says that on a quadratic the rank-one update recovers the exact inverse Hessian from $n$ gradient differences, without line searches and without positive definiteness of the trial matrix, and then takes the Newton step. This is the property that justifies the name "variable metric": the metric $H_k$ converges to the one that makes the problem trivial. The secant equation (8) and the persistence of earlier secant equations (7) are the template for the analysis of every later quasi-Newton update, and the SR1 update remains in use in trust-region methods because it does not force positive definiteness.

The result is classical and its proof is short; what this mission adds is a machine-checked version stated in the paper's own form. In particular the hypothesis is the paper's: only that each of the first $n$ coefficients is defined. Textbook statements of SR1 termination often assume in addition that the steps are linearly independent; the paper does not, and the formal goal does not either. No Lean formalization of SR1, DFP or BFGS termination was found in Mathlib or on Prove2Me. On Prove2Me, the related open targets are L-BFGS termination (Nocedal 1980) and conjugate-gradient termination (Hestenes–Stiefel 1952); the definitions here are independent of theirs.

Difficulty

Each update changes $H$ by a rank-one term, and nothing in a single step forces $H_n$ to be $G^{-1}$ : the coefficient $a_k$ depends on the current iterate and the update could, a priori, destroy what earlier steps achieved, as general rank-one updates do. The obvious count — $n$ steps, $n$ conditions — does not by itself give $n$ independent conditions on $H_n$ ; the steps produced by the method are not chosen to be independent, and the only hypothesis available is that the denominators $M_k-N_k$ are nonzero. The difficulty is to get the full conclusion from that hypothesis alone, without assuming independence, positive definiteness of $H_0$ , or a line search.

Formalization scope

Vectors are Fin n → ℝ with 0-based indices, matrices Matrix (Fin n) (Fin n) ℝ; $u^{\mathsf T}Hv$ is u ⬝ᵥ (H *ᵥ v) and $(Hg)(Hg)^{\mathsf T}$ is vecMulVec (H *ᵥ g) (H *ᵥ g). The definition file DavidonVM.Termination.Method provides quad, grad, Nval, Mval, the run predicate IsRunWith for an arbitrary gradient field and coefficients, and IsQuadRun for the quadratic with $a_k=(M_k-N_k)^{-1}$ ; DavidonVM.Termination.Delta provides the update and the quantity $\Delta$ of (4).

Committed conventions, each a reading of something the paper leaves implicit:

The function is an explicit quadratic with constant symmetric positive definite $G$ ("in the neighborhood of a minimum"); the run's gradient field is $G(x-\xi)$ , and milestone 1 ties it to the quadratic. The goal uses positive definiteness; milestones use only symmetry where that suffices; the secant milestone needs nothing on $G$ .
Only $H_0$ is assumed symmetric (the paper, p. 4: "It is to be symmetric"); positive definiteness of $H_0$ is not assumed.
"Steps for which $\Delta=0$ " is read through footnote 2 as $M_k\ne N_k$ . Lean's real inverse gives $0^{-1}=0$ , so without this hypothesis the update would silently leave $H$ unchanged.
The stopping rule "provided that $N$ is greater than some preassigned $\varepsilon$ " is not modelled; the run continues for every $k$ , and the goal looks at steps $0,\dots,n$ only.
$G^{-1}$ is Mathlib's matrix inverse, the true inverse since $G$ is positive definite.

A statement of the goal with the extra hypothesis " $S_0,\dots,S_{n-1}$ are linearly independent", or with $H_k G S_j=S_j$ assumed, would be a weaker theorem than the paper's and is ruled out. The case $n=0$ is trivial; the hypotheses are jointly satisfiable for $n=1$ (checked locally).

Welcome contributions: proofs of the four milestones and the goal; general facts about rank-one updates (determinant and positive definiteness, Sherman–Morrison form of the inverse) that the further statements need and that are reusable for DFP, BFGS and trust-region analyses.

Selected references

W. C. Davidon, Variable Metric Method for Minimization, SIAM J. Optim. 1(1) (1991) 1–17 (Argonne report ANL-5990, 1959). https://doi.org/10.1137/0801001
M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, J. Res. Nat. Bur. Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
R. Fletcher and M. J. D. Powell, A rapidly convergent descent method for minimization, Comput. J. 6 (1963) 163–168. https://doi.org/10.1093/comjnl/6.2.163
C. G. Broyden, Quasi-Newton methods and their application to function minimisation, Math. Comp. 21 (1967) 368–381. https://doi.org/10.1090/S0025-5718-1967-0224273-2
J. Nocedal, Updating quasi-Newton matrices with limited storage, Math. Comp. 35 (1980) 773–782. https://doi.org/10.1090/S0025-5718-1980-0572855-7

7 thms2 active usersReviewed

Operations Research

Missions

Dynamic Assortment Personalization in High Dimensions 1: The Nuclear-Norm Explore-Then-Exploit Policy Has Regret at Most ((Cr(m+n)+3) log T + 1)ωResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6

Milestones

Significance

Difficulty

Formalization scope

Selected references

Distributionally Robust Convex Optimization IV: An Absolute Mean Spread Bound Describes Exactly the z̃-Marginals of a Lifted Ambiguity SetResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (Absolute Mean Spread), pp. 17–18

Milestones

Significance

Difficulty

Formalization scope

Selected references

Robust Markov Decision Processes 1: Over s-Rectangular Ambiguity Sets, Robust Policy Improvement Is Solved by a Stationary Randomized Policy and the Fixed Point of the Robust Bellman MapResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 (robust policy improvement)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Distributionally Robust Convex Optimization II: The Naïve Approximation Implies the Infimal Convolution Bound, Which Implies the Distributionally Robust ConstraintResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 13)

Milestones (proof of Theorem 3, p. 37; Proposition 1, p. 14)

Significance

Difficulty

Formalization scope

Selected references

A Primal-Dual Learning Algorithm for Personalized Dynamic Pricing with an Inventory Constraint: The Primal-Dual Learning Algorithm Has Regret at Most C(log n)^(2+δ) n^(−1/2)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 17)

The two capacity regimes (Propositions 2–3)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Intrinsic Robustness of the Price of Anarchy I: Every Coarse Correlated Equilibrium of a Smooth Game Has Expected Cost at Most the Robust Price of Anarchy Times OptimalResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2 (static extension theorem)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models 2: Customization Raises the Optimal Expected Revenue by at Most a Factor m, and the Factor Is TightResearch Paper

Motivation

Setting

Formalization targets

Theorem 3.1: universal comparison

Theorem 3.1: order-tight family

Significance

Difficulty

Formalization scope

Selected references

Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models 1: Augmented Greedy Earns a (1 − 1/e) Fraction of the Optimal Revenue from the Complete Customer TypesResearch Paper

Motivation

Setting

Formalization targets

Theorem 4.2: complete-type revenue

Supporting targets

Significance