Probability

Motivation

In a contextual bandit problem a learner repeatedly observes a context (a user, a patient, a query), chooses one of $K$ actions, and observes the reward of the chosen action only. It competes with the best policy of a fixed class $\Pi$ of maps from contexts to actions. This is the standard model for news and advertisement recommendation, adaptive clinical assignment and other interactive decision problems in which counterfactual rewards are never observed.

Two requirements pull against each other. Statistically, the optimal regret against a finite class is of order $\sqrt{KT\ln|\Pi|}$, attained by the exponential-weights algorithm Exp4 (Auer et al. 2002), whose running time is linear in $|\Pi|$ per round. Computationally, practical policy classes are exponentially large and are accessed only through a supervised learning routine. Agarwal, Hsu, Kale, Langford, Li and Schapire (2014) give ILOVETOCONBANDITS, which reaches the optimal regret while touching $\Pi$ only through an arg-max oracle, and only $\tilde O(\sqrt{KT/\ln|\Pi|})$ times in $T$ rounds.

Timeline. Exp4 (2002) attains $O(\sqrt{KT\ln|\Pi|})$ against adversarial rewards with running time $\Omega(|\Pi|)$. Epsilon-greedy and Epoch-Greedy (Langford and Zhang 2007) are oracle-efficient but have regret of order $T^{2/3}$. Exp4.P (Beygelzimer et al. 2011) proves the optimal bound with high probability. RandomizedUCB (Dudík et al. 2011) is the first oracle-based algorithm with optimal regret in the i.i.d. model, but its number of oracle calls is a large polynomial in $T$. ILOVETOCONBANDITS (2014) keeps the regret and reduces the calls to $\tilde O(\sqrt{KT/\ln(|\Pi|/\delta)})$.

Setting

There are $K$ actions, a measurable context space $X$, and a finite nonempty policy class $\Pi$ of measurable maps $X\to\{0,\dots,K-1\}$. A distribution $\mathcal D$ on $X\times[0,1]^K$ generates context/reward-vector pairs $(x_t,r_t)$, $t=1,2,\dots$, independently. In round $t$ the learner sees $x_t$, draws an action $a_t$ with probability $p_t(a_t)$, and observes only $r_t(a_t)$. The history $H_t$ is the list of records $(x_i,a_i,r_i(a_i),p_i(a_i))$, $i\le t$.

The expected reward of a policy is $\mathcal R(\pi)=\mathbb E_{(x,r)\sim\mathcal D}[r(\pi(x))]$, $\pi_\star$ is any maximizer over $\Pi$, and $\mathrm{Reg}(\pi)=\mathcal R(\pi_\star)-\mathcal R(\pi)$. The regret after $T$ rounds is the empirical cumulative quantity $\sum_{t=1}^T\bigl(r_t(\pi_\star(x_t))-r_t(a_t)\bigr)$.

The inverse propensity scoring estimate is $\widehat{\mathcal R}_t(\pi)=\frac1t\sum_{i\le t}r_i(a_i)\mathbb 1\{\pi(x_i)=a_i\}/p_i(a_i)$, and $\widehat{\mathrm{Reg}}_t(\pi)=\max_{\pi'}\widehat{\mathcal R}_t(\pi')-\widehat{\mathcal R}_t(\pi)$. For nonnegative weights $Q$ on $\Pi$ with total mass at most one, the smoothed projection is $Q^\mu(a\mid x)=(1-K\mu)\sum_{\pi:\pi(x)=a}Q(\pi)+\mu$.

ILOVETOCONBANDITS takes an epoch schedule $0=\tau_0<\tau_1<\cdots$ and $\delta\in(0,1)$, sets $d_t=\ln(16t^2|\Pi|/\delta)$ and $\mu_m=\min\{1/(2K),\sqrt{d_{\tau_m}/(K\tau_m)}\}$. At the end of epoch $m$ (round $\tau_m$) it chooses weights $Q_m$ solving the optimization problem (OP): with $b_\pi=\widehat{\mathrm{Reg}}_{\tau_m}(\pi)/(100\mu_m)$,

$$\sum_\pi Q(\pi)b_\pi\le2K,\qquad \widehat{\mathbb E}_{x\sim H_{\tau_m}}\bigl[1/Q^{\mu_m}(\pi(x)\mid x)\bigr]\le2K+b_\pi\ \ \forall\pi\in\Pi.$$

During epoch $m+1$ it puts the leftover mass on the empirical maximizer $\pi_{\tau_m}$, obtaining a distribution $\widetilde Q_m$, and draws $a_t\sim\widetilde Q_m^{\mu_m}(\cdot\mid x_t)$.

Formalization targets

Goal: Theorem 2 in the explicit form of Lemma 17

Assume $\tau_{m+1}\le2\tau_m$ for $m\ge1$ and let $m_0=\min\{m\ge1:d_{\tau_m}/\tau_m\le1/(4K)\}$, $\rho=\sup_{m\ge m_0}\sqrt{\tau_m/\tau_{m-1}}$, $c_0=4\rho(1+94.1)$, $C_0=400+c_0$, and $m(T)=\min\{m:T\le\tau_m\}$. For every $T$, with probability at least $1-\delta$,

$$\sum_{t=1}^T\bigl(r_t(\pi_\star(x_t))-r_t(a_t)\bigr)\le C_0\Bigl(4Kd_{\tau_{m_0-1}}+\sqrt{8Kd_{\tau_{m(T)}}\tau_{m(T)}}\Bigr)+\sqrt{8T\ln(2/\delta)}.$$

It holds for every (OP)-solution selection and every tie-breaking rule. Since $\tau_{m(T)}\le2(T-1)$ once $\tau_{m(T)-1}\ge1$, this is the paper's $O\bigl(\sqrt{KT\ln(T|\Pi|/\delta)}+K\ln(T|\Pi|/\delta)\bigr)$.

Milestones

Freedman's inequality (Lemma 9); the uniform deviation of true from empirical variances (Lemma 10); the deviation of the IPS estimates (Lemma 11); on the event $\mathcal E$ where both deviations hold, the variance bound (Lemma 12), the two-sided comparison of $\mathrm{Reg}$ and $\widehat{\mathrm{Reg}}_t$ (Lemma 13), and the low regret of the sampling distribution (Lemma 14); and the deterministic sums of the $\mu_m$ (Lemmas 15, 16).

Significance

The theorem shows that optimal regret in the i.i.d. contextual bandit problem does not require enumerating the policy class: a sequence of convex feasibility problems, each solvable with few oracle calls (Theorem 3, the companion mission), suffices. The inverse-propensity variance constraint of (OP) and the epoch-and-warm-start structure became the template for later oracle-based methods, and the paper's Online Cover variant is implemented in the Vowpal Wabbit learning system.

The result is proved in the paper; none of it is formalized. The platform holds Exp4 (Bandit Algorithms VIII, adversarial rewards and expert advice) and SquareCB (Foundations of RL II, regression oracles), both different algorithms in different models, and Azuma–Hoeffding (bounded_diff_martingale_two_sided), which the proof of Lemma 17 uses. This mission adds the first inverse-propensity estimator, the first oracle-based policy-class bandit algorithm, and Freedman's inequality with a conditional-variance sum. Several statements are proved in the paper only in outline: Lemma 10 has a proof sketch that defers to Dudík et al. (2011), and the paper asserts $\Pr(\mathcal E)\ge1-\delta/2$ without spelling out how the first case of (14) follows from Lemma 11.

Difficulty

The regret of the algorithm depends on the quality of its own data. The estimates $\widehat{\mathcal R}_t$ have variance governed by the distributions $\widetilde Q_m$ the algorithm chose earlier, and those distributions were chosen from the estimates. A direct union bound over $\Pi$ with the worst-case variance $1/\mu$ gives regret of order $T^{2/3}$, the Epoch-Greedy rate. The argument that avoids this must show that a policy with large variance was already known to be bad, and the estimated and true regrets must be compared inductively over epochs with constants that do not grow ($\theta_2\ge8\rho$). The inequality must also hold for every solution of (OP), not a particular one.

The martingale structure requires care: the action of round $t$ is drawn from a distribution that depends on the whole past and must not look at $r_t$, and Lemma 10 must hold uniformly over all distributions $P$ on $\Pi$, not just finitely supported ones.

Formalization scope

The formalization commits to the following representation and conventions.

• Actions are Fin K with 0 < K (NeZero K); $\Pi$ is a nonempty Finset (X → Fin K) of measurable maps; weights on $\Pi$ are real functions on its subtype. $\mathcal D$ is a probability measure on X × (Fin K → ℝ) with rewards in $[0,1]$ almost surely.
• The run lives on a probability space carrying $Z_t=(x_t,r_t)$ i.i.d. with law $\mathcal D$ and $U_t$ i.i.d. uniform on $[0,1]$, independent of the $Z$'s. The action is the inverse distribution function of $\widetilde Q^{\mu}(\cdot\mid x_t)$ at $U_t$, so it has the right law and is independent of $r_t$ given the past and $x_t$. The tie-breaking rule and the (OP)-selection are arbitrary measurable functions of the observable history (a list of records). The selection must return an (OP) solution for every history of length $\tau_m$; such selections exist by Theorem 3.
• Rounds and epochs are $1,2,\dots$ as in the paper; $\ln$ is Real.log.
• $\mu_0:=1/(2K)$. The printed formula is $0/0$ at $\tau_0=0$, and the proofs of Lemmas 12 and 14 use this value.
• The goal and Lemmas 13–14 assume $m_0\ge2$, i.e. $d_{\tau_1}/\tau_1>1/(4K)$, which holds e.g. for $\tau_1=1$. It replaces the paper's "$\tau_1=O(1)$". It makes $d_{\tau_{m_0-1}}$ finite and $\rho\le\sqrt2$, so $\rho$ is a genuine real supremum.
• Explicit constants: $\psi=100$, $\theta_1=94.1$, $\theta_2=\psi/6.4$, $c_0=4\rho(1+\theta_1)$, $C_0=4\psi+c_0$, $6.4$, $75$, $6.3$, $81.3$, $e-2$. $\rho$ is not replaced by $\sqrt2$.
• Where the paper allows $\lambda=0$ or $\mu_m=0$ (Lemmas 9–11), the bound is $+\infty$. These cases are excluded ($\lambda>0$, $\mu_m>0$) because $x/0=0$ in Lean. Lemma 9 adds measurability and integrability of $X_t$ and $X_t^2$.
• Probability statements bound the (outer) measure of the failure event by $\delta$.

A statement about "a policy mixture with small regret", about the pseudo-regret $\sum_t\mathrm{Reg}$ of the chosen policies, about a specially chosen (OP) solution, or about actions that may depend on $r_t$ is not Theorem 2; none of these is accepted. With these constants the bound exceeds $T$ unless $T$ is very large, which is a property of the paper's constants, not of the encoding.

Needed infrastructure: Freedman's inequality for the natural filtration, a uniform-over-distributions concentration argument (the probabilistic method of Dudík et al.), measurability of the algorithm's run, and Azuma–Hoeffding. Freedman's inequality and the IPS estimator are reusable beyond this mission. Proofs of any milestone, and sharper or cleaner restatements proved as separate lemmas, are welcome.

Selected references

• A. Agarwal, D. Hsu, S. Kale, J. Langford, L. Li, R. E. Schapire, Taming the Monster: A Fast and Simple Algorithm for Contextual Bandits, ICML 2014; arXiv:1402.0555v2. https://arxiv.org/abs/1402.0555
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM J. Comput. 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• A. Beygelzimer, J. Langford, L. Li, L. Reyzin, R. E. Schapire, Contextual bandit algorithms with supervised learning guarantees, AISTATS 2011. https://arxiv.org/abs/1002.4058
• M. Dudík, D. Hsu, S. Kale, N. Karampatziakis, J. Langford, L. Reyzin, T. Zhang, Efficient optimal learning for contextual bandits, UAI 2011. https://arxiv.org/abs/1106.2369
• J. Langford, T. Zhang, The epoch-greedy algorithm for contextual multi-armed bandits, NIPS 2007. https://papers.nips.cc/paper/3178-the-epoch-greedy-algorithm-for-multi-armed-bandits-with-side-information
• D. A. Freedman, On tail probabilities for martingales, Ann. Probab. 3(1), 1975. https://doi.org/10.1214/aop/1176996452

Motivation

A retailer or manufacturer that stocks several grades of the same item (memory chips of different speeds, steel of different strengths, seats in fare classes) can often meet demand for a lower grade with a higher one when the lower grade runs out. This downward substitution changes the stocking decision: each product now protects the demand of every class below it, so the optimal stock of one product depends on the stock of all the others, and the single-product newsvendor answer no longer applies product by product.

Bassok, Anupindi and Akella (Operations Research 47(4), 1999) set up a single-period model with $N$ products and full downward substitution and showed that the optimal ordering policy still has a simple structure: there is a base-stock vector $y^*$; products below it are ordered up to it, and a product already at or above its base-stock level is not ordered at all. Earlier work on multiproduct ordering, Veinott (1965) and Ignall and Veinott (1969), gave monotonicity conditions through a substitute matrix condition on the Hessian of the cost, which is hard to verify for a general $N$-product substitution structure; the paper works instead with concavity, submodularity and explicit first partial derivatives. Two-product substitution models had been analysed by McGillivray and Silver (1978) and Parlar and Goyal (1984).

Setting

There are $N$ products and $N$ demand classes, both numbered $1,\dots,N$. Class $i$ can be served by product $j$ whenever $j \le i$, at a unit substitution cost $b$ when $j < i$. Each class $i$ has unit revenue $p_i$ and unit backorder cost $\pi_i$; each product $j$ has unit purchase cost $c_j$ and effective unit salvage value $s_j$ (salvage value minus holding cost, possibly negative). Put $a_{ji} = p_i$ if $j = i$, $a_{ji} = p_i - b$ if $j < i$, and $T_k = p_k + \pi_k - b$. The standing assumptions are: (1) $\pi_i + p_i \ge \pi_j + p_j$ for $i < j$; (2) $s_i \ge s_j$ for $i < j$; (3) $a_{ij} + \pi_j - s_i \ge 0$ for $i \le j$.

The sequence of events: the starting inventory $x$ is observed; stock is raised to $y \ge x$ at unit costs $c$; the demand vector $d$ is realized; stock is allocated to classes; leftovers are salvaged. For fixed $y$ and $d$ the allocation is the linear program

$$G(y,d) = \max \sum_{i}\sum_{j \le i} a_{ji} w_{ji} + \sum_i s_i v_i - \sum_i \pi_i u_i$$

subject to $u_i + \sum_{j\le i} w_{ji} = d_i$, $v_j + \sum_{i \ge j} w_{ji} = y_j$, and $w, u, v \ge 0$, where $w_{ji}$ is the amount of product $j$ given to class $i$, $u_i$ the shortage of class $i$ and $v_j$ the leftover of product $j$. The expected profit is

$$P(x,y) = -\sum_k c_k (y_k - x_k) + \mathbb E\, G(y, D),$$

and the ordering problem is $\max_{y \ge x} P(x,y)$; a maximizer is an optimal level $\bar y(x)$.

Allocation Algorithm (A) serves the classes in the order $1,2,\dots,N$, class $i$ first from product $i$ and then from the leftovers of products $i-1,\dots,1$. The subproblem shortage $S^k_j$ is the unmet demand of class $j$ when (A) runs on the classes $k,\dots,j$ with the products $k,\dots,j$ only; $\vec S^k_{a,n} = 0$ means $S^k_m = 0$ for all $a \le m \le n$. The paper's first partial derivatives of $P$ are sums of salvage values, substitution costs and the $T_k$, weighted by probabilities of such shortage events.

Formalization targets

Goal: Theorem 2

With $y^*$ a maximizer of $P(0,\cdot)$ over $y \ge 0$, every optimal level $\bar y$ for every starting inventory $x \ge 0$ satisfies

$$x_i \ge y^*_i \implies \bar y_i = x_i .$$

Milestones

• Proposition 1: Algorithm (A) is feasible and optimal for the allocation LP, and its value is $G(y,d)$.
• Proposition 2: $y \mapsto P(x,y)$ is concave and submodular on $\{y \ge 0\}$.
• Eq. (4): the explicit formula for $\partial P/\partial y_i$ in terms of shortage probabilities.
• Theorem 1: there is $y^* \ge 0$ with $\bar y(x) = y^*$ whenever $0 \le x \le y^*$.
• Lemmas 1, 2, 3, 5: identities and monotonicity properties of the shortage probabilities used to compare $\partial P/\partial y_i$ and $\partial P/\partial y_{i+1}$.

Significance

Theorems 1 and 2 give the optimal ordering policy of the substitution model its base-stock form: a vector $y^*$, computed once, determines the decision for every starting inventory in the region $x \le y^*$ and fixes the order of every overstocked product elsewhere. The paper builds its bounds on $y^*$, its iterative algorithm for two products and its computational study of the value of substitution (§3) on this structure. Proposition 1 turns the second-stage linear program into a closed-form greedy allocation, which is what makes the derivative formula (4) explicit.

The results are proved in the paper, but none of them has been machine-checked. Several steps of the paper are informal: Proposition 1 is proved by reference to Monge sequences of transportation problems, the proof of Theorem 2 treats only the adjacent pair $j = i+1$, and the paper uses independence of demand classes, densities and a unique optimal level without stating them. A formal development makes these hypotheses explicit and checks each step. The model, the greedy allocation and the shortage calculus are reusable for other multi-product newsvendor and assortment models.

Difficulty

The obvious argument for Theorem 2 is the one-dimensional one: if $x_i \ge y^*_i$ then $\partial P/\partial y_i \le 0$ at $\bar y$, so product $i$ should not be raised. It fails because $\partial P/\partial y_i$ depends on the other coordinates: at $\bar y$ some products are raised above $x$ and others kept at $x_j > y^*_j$, and concavity plus submodularity alone do not control the sign. For a general concave submodular function the conclusion is false; a three-variable quadratic in which raising one coordinate lowers the optimal level of a second one, which in turn raises the marginal value of the first, is a counterexample. The proof has to use the specific structure of the substitution model, through the pairwise comparison of the partial derivatives in Eq. (4). The derivative formula itself requires a careful account of how an extra unit of product $i$ propagates through the greedy allocation of every later class.

Formalization scope

Products and classes are indexed by Fin N (the paper's index $k$ is Lean index $k-1$); stocks, demands and prices are real. The allocation LP is encoded with the upward arcs $w_{ji}$, $i < j$, forbidden (fixed to $0$), as in the paper's proof of Proposition 1; $G$ is the supremum of the LP objective. The demand law is a product $\nu_1 \otimes \dots \otimes \nu_N$. Submodularity is the lattice inequality $P(x, y \vee y') + P(x, y \wedge y') \le P(x,y) + P(x,y')$, which is equivalent to the paper's nonpositive cross partials (Definition 2) for twice differentiable functions. Derivatives are stated with HasDerivAt, and the derivative inequalities of Lemmas 2 and 5 in the stronger monotone form, so that no statement is made true by a junk value of deriv. The "…" in Eq. (4) and in the lemmas are expanded as finite sums with the general term inferred from the printed first and last terms.

Hypotheses the paper uses without stating, made explicit here:

• the substitution cost is nonnegative, $b \ge 0$ (Proposition 1 is false for $b < 0$);
• the demand classes are independent (product forms in Lemma 3 and Appendix B);
• each demand is nonnegative, has finite mean and has a density;
• $s_i < c_i < p_i + \pi_i$ for every product (Theorem 1's proof);
• every demand law charges every nonempty open interval of $[0,\infty)$, standing in for the uniqueness of the optimal level $\bar y(x)$ that the notation presupposes (Theorems 1 and 2).

The goal quantifies over every maximizer $y^*$ of $P(0,\cdot)$ and every optimal $\bar y$; it is not an existence statement, and $y^*$ is not chosen by the prover. Without the full-support hypothesis the universal statement fails already for one product (a flat-topped profit). Lemmas 4 and 6 of the paper are not included: under the definitions used here both are false as printed (small two- and three-product computations with exponential demands show it), and Theorem 3 comes after the goal and fails as printed for $x_i \ge y^*_i$.

A proof needs integrals of piecewise-linear functions of the demand vector, differentiation under the integral sign, and facts about product measures. Contributions of any of the milestones, and of general lemmas on the greedy allocation (monotonicity of $S^k_j$ in $y$ and $d$), are welcome.

Selected references

• Y. Bassok, R. Anupindi, R. Akella, Single-Period Multiproduct Inventory Models with Substitution, Operations Research 47(4):632–642, 1999. https://doi.org/10.1287/opre.47.4.632
• A. F. Veinott, Jr., Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• E. Ignall, A. F. Veinott, Jr., Optimality of Myopic Inventory Policies for Several Substitute Products, Management Science 15(5):284–304, 1969. https://doi.org/10.1287/mnsc.15.5.284
• A. J. Hoffman, On Simple Linear Programming Problems, in V. Klee (ed.), Convexity, Proceedings of Symposia in Pure Mathematics, Vol. 7, AMS, 1963.

Pooling inventory among independent retailers

Retailers that sell the same product can raise their joint profit by pooling: stock left over at one location is shipped to meet unmet demand at another, and stock can be held in shared warehouses until demand is known (Eppen 1979; Eppen and Schrage 1981). When the retailers are independent firms, pooling creates two questions at once. After demand is realized, the extra profit from shipping must be split in a way no group of retailers would reject. Before demand is realized, each retailer chooses its own stock, and that choice depends on how the split will be made. A split that is fair ex post may lead to stocking decisions that are poor for the system as a whole.

Anupindi, Bassok and Zemel (MSOM 2001) model the ex-post split as a cooperative game, the ex-ante stocking as a non-cooperative game, and ask whether a single allocation rule can serve both. Their framework is a standard reference for "coopetition" models in supply chains, where firms compete on stocking decisions and cooperate on redistribution.

Setting

There are retailers $\mathcal N=\{1,\dots,N\}$ and warehouses $\mathcal W=\{1,\dots,W\}$. Retailer $n$ has unit cost $c_n$, revenue $r_n$ and salvage value $v_n$; warehouse $w$ has purchasing cost $c_w$ and salvage value $v_w$. Shipping from location $i$ to retailer $n$ costs $t_{i,n}$ per unit, and a fraction $\beta_{i,n}\in[0,1]$ of the customers at $n$ accept service from $i$.

Before demand, retailer $n$ chooses a position $\vec Z_n=(X_n,Y_{1,n},\dots,Y_{W,n})$: local stock $X_n$ and claims $Y_{w,n}$ on warehouse stock, so warehouse $w$ holds $Y_w=\sum_nY_{w,n}$. A profile is $[Z]=(\vec Z_1,\dots,\vec Z_N)$. Demand $\vec D$ is random with law $\mu$. After demand, retailer $n$ has local sales $S_n=\min\{X_n,D_n\}$, residual inventory $H_n=\max\{X_n-D_n,0\}$ and residual demand $E_n=\max\{D_n-X_n,0\}$.

The snapshot allocation game SAG$([Z],\vec D)$ gives each coalition $\mathcal S\subseteq\mathcal N$ the value $W^*_{\mathcal S}([Z],\vec D)$: the optimal value of the linear program (6), which ships $q_{i,n}$ units from $i\in\mathcal S\cup\mathcal W$ to $n\in\mathcal S$ at profit $r_n-v_i-t_{i,n}$ per unit, subject to $\sum_nq_{i,n}\le H_i$, $\sum_nq_{w,n}\le\sum_{n\in\mathcal S}Y_{w,n}$ and $\sum_iq_{i,n}/\beta_{i,n}\le E_n$. Its core is the set of allocations $\alpha$ with $\sum_{j\in\mathcal S}\alpha_j\ge W^*_{\mathcal S}$ for every $\mathcal S$ and $\sum_{j\in\mathcal N}\alpha_j=W^*_{\mathcal N}$ (7).

An allocation rule AR-$m$ assigns surplus $\alpha^m_n([Z],\vec D)$; retailer $n$ earns

$$P^m_n([Z],\vec D)=r_nS_n+v_nH_n-c_nX_n-\sum_w(c_w-v_w)Y_{w,n}+\alpha^m_n([Z],\vec D)\qquad(9)$$

and expects $J^m_n([Z])=E_{\vec D}P^m_n$. A Nash equilibrium (10) is a profile at which no retailer gains by changing its own position. The first-best profile $[Z]^{c*}$ maximizes the expected centralized profit $J^c_{\mathcal N}([Z])=E_{\vec D}P^c_{\mathcal N}([Z],\vec D)$, where $P^c_{\mathcal N}=\sum_n[r_nS_n+v_nH_n-c_nX_n]-\sum_w(c_w-v_w)Y_w+W^*_{\mathcal N}$.

The fractional rule AR-f (11) pays $\alpha^f_n=\theta_nP^c_{\mathcal N}-[\,r_nS_n+v_nH_n-c_nX_n-\sum_w(c_w-v_w)Y_{w,n}]$ with fixed shares $\theta_n\in(0,1)$, $\sum_n\theta_n=1$. The dual allocation (8) is $\alpha^d_n=\nu_nH_n+\sum_w\gamma_wY_{w,n}+\delta_nE_n$ for optimal dual prices $(\nu,\gamma,\delta)$ of (6) for $\mathcal N$. The modified rule AR-c is $\alpha^c_n([Z],\vec D)=\alpha^f_n([Z],\vec D)+w_n([Z]^{c*},\vec D)$ with $w_n=\alpha^d_n([Z]^{c*},\cdot)-\alpha^f_n([Z]^{c*},\cdot)$.

Formalization targets

Goal: Corollary 5.1 (p. 361)

For a first-best profile $[Z]^{c*}$ and a measurable choice of dual prices at $[Z]^{c*}$,

$$[Z]^{c*}\ \text{is a pure Nash equilibrium under AR-c, and}\ \ \alpha^c([Z]^{c*},\vec D)\in\operatorname{Core}\big(\mathrm{SAG}([Z]^{c*},\vec D)\big)\ \ \forall\vec D,$$

with integrable side payments.

Milestones

• Examples 1 and 2 (pp. 358–359): a transfer-price allocation outside the core; the dual allocation $(8,8,8,0)$ and the non-dual core allocation $(0,0,0,24)$.
• Theorem 4.1 (p. 358): if all inventory is claimed, the core of SAG$([Z],\vec D)$ is nonempty and contains the dual allocation (8) for every optimal dual.
• Theorem 5.2 (p. 361): under AR-f every first-best profile is a Nash equilibrium.
• Theorem 5.1 (p. 361): for any rule and any of its equilibria $[Z]^{m*}$ there are integrable demand-dependent side payments that leave the set of equilibria unchanged and put the allocations at $[Z]^{m*}$ in the core for every $\vec D$.

Significance

The goal answers the paper's central question positively: there is an allocation mechanism under which the centrally optimal stock levels are an equilibrium of the decentralized stocking game, while every ex-post split of the pooling surplus is stable against all coalitions. Theorem 4.1 is the ex-post half: shadow prices of the shipping LP give a stable split for every realization, independently of who owns which units. The paper also shows (Proposition 5.1, not included here) that the dual allocation alone does not induce first-best stocking, which is why the side payments of Theorem 5.1 are needed.

The results are proved in the paper; Theorem 4.1 is proved there only by reference to the LP-game literature (Owen 1975; Samet and Zemel 1984). None of them has a machine-checked proof. The mission would produce the first formal treatment on Prove2Me of a linear-production (LP) game and its core, and of a model combining a cooperative second stage with a non-cooperative first stage.

Difficulty

Theorem 4.1 is an instance of Owen's theorem on LP games, but the instance is not a standard linear production game: coalition LPs have variables only on arcs inside the coalition, warehouse capacity is limited to the coalition's own claims, and the acceptance constraint divides by $\beta_{i,n}$, which may be zero, so the general theorem cannot be quoted as it stands. The paper leaves the dual of (6) unwritten, and Mathlib has no ready-made LP duality in this form.

The stochastic layer is the other obstacle. Expected payoffs are integrals, and the side payment is built from a choice of dual prices for each demand realization. Its integrability requires measurability of that choice and of the LP value as a function of demand; neither is given by the paper, which treats the side payments as "constants".

Formalization scope

Retailers are Fin N, warehouses Fin W, locations Fin N ⊕ Fin W; quantities, prices and demands are real numbers; demand is a probability measure on Fin N → ℝ; expectations are Bochner integrals. $W^*_{\mathcal S}$ is the real supremum of (6a) over the feasible set, and profiles are required to be nonnegative, which makes the feasible set nonempty and bounded. Arcs with $\beta_{i,n}=0$ carry no shipment. The core is the platform definition Supermodularity.Cooperative.Core. The dual of (6) is written out explicitly (the paper does not state it). The paper's continuous-CDF assumption is not used and is dropped.

Pinned readings:

1. "Dual prices" means any optimal solution of the dual of (6) for $\mathcal N$; Theorem 4.1 is stated for every such solution.
2. "Induces the same equilibrium inventory levels as the first-best" (Theorem 5.2) and "the NE using $\alpha^c$ is first-best" (Corollary 5.1) are stated as "every first-best profile is a Nash equilibrium", the direction the proofs give.
3. "$[Z]^{\tilde m*}=[Z]^{m*}$" (Theorem 5.1) is stated as equality of the two sets of equilibria; the continuity and unimodality assumptions, which only guarantee existence of an equilibrium, are dropped because the equilibrium is a hypothesis.
4. "An appropriate way of breaking ties" is a measurable choice of optimal dual prices; demand is almost surely nonnegative; the rule's payoffs in Theorem 5.1 are integrable.
5. The shares $\gamma_n$ of Theorem 5.2 are written $\theta_n$, and Eq. (11) is used with $+v_nH_n$ in the bracket (printed $-v_nH_n$), as the proof on p. 367 requires.

Not acceptable: a core without the efficiency equation (7b); a feasible set that lets $q_{i,n}/0=0$ sell to customers who balk; an arbitrary side payment instead of the constructed one; or a Nash equilibrium evaluated through non-integrable payoffs, whose Bochner integral is $0$ and makes every profile an equilibrium.

Useful infrastructure: finite-dimensional LP duality in inequality form, measurable selection of LP optimal solutions, and continuity of LP values in the right-hand side. All of it can be reused in other LP-game and two-stage stochastic programming missions.

Selected references

• R. Anupindi, Y. Bassok, E. Zemel, A General Framework for the Study of Decentralized Distribution Systems, Manufacturing & Service Operations Management 3(4):349–368, 2001. https://doi.org/10.1287/msom.3.4.349.9973
• G. Owen, On the core of linear production games, Mathematical Programming 9:358–370, 1975. https://doi.org/10.1007/BF01681356
• D. Samet, E. Zemel, On the core and dual set of linear programming games, Mathematics of Operations Research 9(2):309–316, 1984. https://doi.org/10.1287/moor.9.2.309
• G. D. Eppen, Effects of centralization on expected costs in a multi-location newsboy problem, Management Science 25(5):498–501, 1979. https://doi.org/10.1287/mnsc.25.5.498

Motivation

Stochastic approximation finds a root $x^*$ of an unknown map $R:\mathbb R^N\to\mathbb R^N$ from noisy evaluations $y_t=R(x_{t-1})+\xi_t$, by the Robbins–Monro recursion $x_t=x_{t-1}-\gamma_ty_t$. It underlies stochastic gradient descent, recursive estimation in statistics, adaptive control and simulation-based optimization. The classical theory (Sacks 1958) shows that the fastest attainable rate, $\sqrt t(x_t-x^*)\Rightarrow N(0,G^{-1}S(G^{-1})^T)$ with $G=R'(x^*)$ and $S$ the noise covariance, is achieved by the matrix step $\gamma_t=t^{-1}G^{-1}$, which requires knowing $G$.

Polyak and Juditsky (SIAM J. Control Optim. 30 (1992) 838–855) proved that the same optimal covariance is attained without any knowledge of $G$: run the recursion with scalar steps that decrease more slowly than $1/t$ and output the running average $\bar x_t$ of the iterates. Ruppert (Cornell ORIE technical report, 1988) obtained the one-dimensional case independently. The method, known as Polyak–Ruppert averaging, is the standard device for variance reduction in stochastic approximation.

Timeline:

• 1951, Robbins and Monro: the recursion and its convergence in probability.
• 1958, Sacks: asymptotic normality of $x_t$ for $\gamma_t=\gamma/t$.
• 1988, Ruppert: averaging in one dimension, i.i.d.-type noise.
• 1990–1992, Polyak; Polyak and Juditsky: averaging in $\mathbb R^N$ for linear problems with martingale-difference noise (Theorem 1) and nonlinear problems (Theorem 2).

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},P)$ be a filtered probability space and $(\xi_t)_{t\ge1}$ an adapted $\mathbb R^N$-valued noise process. Given a nonrandom $x_0\in\mathbb R^N$ and step sizes $\gamma_t>0$, algorithm (7) is

$$x_t=x_{t-1}-\gamma_t\bigl(R(x_{t-1})+\xi_t\bigr),\qquad\bar x_t=\frac1t\sum_{i=0}^{t-1}x_i .$$

The error is $\Delta_t=x_t-x^*$ and the estimation error is $\bar\Delta_t=\bar x_t-x^*$.

The hypotheses are:

• Assumption 3.1: a Lyapunov function $V$ with $V(x)\ge\alpha|x|^2$, Lipschitz gradient, $V(0)=0$, $\nabla V(x-x^*)^TR(x)>0$ for $x\neq x^*$, and $\nabla V(x-x^*)^TR(x)\ge\lambda_1V(x-x^*)$ near $x^*$.
• Assumption 3.2: $|R(x)-G(x-x^*)|\le K_1|x-x^*|^{1+\lambda}$ near $x^*$, with $0<\lambda\le1$ and every eigenvalue of $G$ having positive real part.
• Assumption 3.3: $\xi_t$ is a martingale difference with $E(|\xi_t|^2\mid\mathcal F_{t-1})+|R(x_{t-1})|^2\le K_2(1+|x_{t-1}|^2)$. It splits as $\xi_t=\xi_t(0)+\zeta_t$, where $\xi_t(0)$ is a martingale difference whose conditional covariance tends to $S\succ0$ in probability and whose conditional second moments are uniformly integrable, and $E(|\zeta_t|^2\mid\mathcal F_{t-1})\le\delta(x_{t-1}-x^*)$ with $\delta(x)\to0$ as $x\to0$.
• Assumption 3.4: $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$, $\sum_t\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, $\gamma_t\to0$ and $\sum_t\gamma_t^2<\infty$.

The linear case, algorithm (2), is $R(x)=Ax-b$ with every eigenvalue of $A$ having positive real part.

Formalization targets

Goal: Theorem 2

Under Assumptions 3.1–3.4,

$$\bar x_t\to x^*\ \text{a.s.},\qquad\sqrt t\,(\bar x_t-x^*)\xrightarrow{D}N\bigl(0,\;G^{-1}S(G^{-1})^T\bigr).$$

Milestones

• Lemma 1, Part 2: under condition (4) on the steps, $t\gamma_t\to\infty$.
• Lemma 1: the matrices $\varphi_j^t=A^{-1}-\gamma_j\sum_{i=j}^{t-1}\prod_{k=j}^{i-1}(I-\gamma_kA)$ are uniformly bounded, and $\frac1t\sum_{j<t}\|\varphi_j^t\|\to0$.
• Lemma 2: the representation (A9) of $\sqrt t\,\bar\Delta_t$ for the linear error recursion.
• Theorem 1(a): the linear case, $\sqrt t(\bar x_t-x^*)\Rightarrow N(0,A^{-1}S(A^{-1})^T)$.
• Proof of Theorem 2, Part 1: $V(\Delta_t)$ converges almost surely to a finite limit.
• Proof of Theorem 2, p. 850: $x_t\to x^*$ almost surely.
• Proof of Theorem 2, Part 4: the average of the linearised process $\Delta^1_t=\Delta^1_{t-1}-\gamma_t(G\Delta^1_{t-1}+\xi_t)$ satisfies $\sqrt t(\bar\Delta^1_t-\bar\Delta_t)\to0$ almost surely.

Significance

Theorem 2 shows that averaging turns a robust, slowly-stepped recursion into an asymptotically efficient estimator. The covariance $G^{-1}S(G^{-1})^T$ is the lower bound for this class of problems: for linear recursive estimates with independent noise it is the bound of [26] in the paper. Downstream, the result is what is invoked for the asymptotic efficiency of averaged stochastic gradient descent (Theorem 3 of the paper) and of recursive M-estimators in regression (Theorem 4).

The result is proved, with a published proof, but has no machine-checked version. As far as a search of the platform shows, no statement of Theorem 1 or Theorem 2 exists on Prove2Me. The platform does have a scalar martingale central limit theorem (Martingale.clt_of_mds, proved, with unconditional Lindeberg condition), which is usable through the Cramér–Wold device. Formalizing Theorem 2 also requires the Robbins–Siegmund almost-supermartingale theorem, a multivariate CLT for martingale differences under conditional Lindeberg and conditional covariance conditions, and the Kronecker lemma. Mathlib has none of these three in the required form, and each is reusable well beyond this mission. Non-asymptotic SGD rates already on the platform (the Bottou–Curtis–Nocedal and Lan missions) are different results.

Difficulty

The obvious approach analyses $x_t$ directly. It fails: with steps decreasing more slowly than $1/t$, $\sqrt t(x_t-x^*)$ diverges, and only the average has the $\sqrt t$ rate. The average must be compared with the averaged noise through the matrix sums of Lemma 1, whose bounds are uniform in both indices. Those bounds rely on the step condition $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$ in a quantitative way.

The nonlinear case adds a second difficulty. The iterates are first shown to converge almost surely, by a Lyapunov argument. The nonlinear error is then transferred to a linearised process at the $\sqrt t$ scale, which needs a summability estimate on $|\Delta_i|^{1+\lambda}i^{-1/2}$ obtained through stopping times. A central limit theorem for the linear process alone does not give the result, because the linearisation error must vanish after multiplication by $\sqrt t$.

Formalization scope

Points are in EuclideanSpace ℝ (Fin N) and matrices are Matrix (Fin N) (Fin N) ℝ, acting through Matrix.toEuclideanLin. Matrix norms are operator norms. Conditional expectations are MeasureTheory.condExp on a Filtration ℕ. "Given $\mathcal F_{t-1}$" is written with shifted indices ($\xi_{t+1}$ given $\mathcal F_t$). The algorithm is a recursive definition from $(x_0,\gamma,R,\xi)$, with $\gamma_0,\xi_0$ unused and $\bar x_t$ averaging $x_0,\dots,x_{t-1}$. Convergence in distribution is TendstoInDistribution to multivariateGaussian 0 V. Convergence of conditional covariances in probability is entrywise TendstoInMeasure. A limsup or supremum "tending to 0 in probability" is unfolded into its $\eta$–$\delta$ definition.

Corrections of the printed text, each used by the paper's own proof:

1. Assumption 3.1 prints $V(x^*)=0$ and $\ge\lambda V(x)$. Stated as $V(0)=0$ and $\ge\lambda_1V(x-x^*)$ (as printed they force $x^*=0$). The drift constant is renamed $\lambda_1$, since the paper uses $\lambda$ also in Assumption 3.2.
2. Eq. (10) is garbled as printed. It is stated as $\sum\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, the form of Assumptions 4.7 and 5.6 and of p. 851.
3. Assumption 3.3's $\delta(x_{t-1})$ is stated as $\delta(x_{t-1}-x^*)$.
4. $\gamma_t\to0$ and $\sum\gamma_t^2<\infty$ are added to Assumption 3.4. The proof uses them (p. 849), and they do not follow from it.
5. $R$ is assumed continuous. The paper states no regularity of $R$, but its proof of almost sure convergence (pp. 849–850) needs $\nabla V(x-x^*)^TR(x)$ bounded away from $0$ on annuli around $x^*$, which continuity and Assumption 3.1 provide.
6. Lemma 1 and Theorem 1(a) are stated under condition (4) only. The constant-step condition (3) is false as printed ($A=\mathrm{diag}(1,10)$, $\gamma=1$), and Theorem 2 does not use it.
7. (A3) is stated with the norm inside, as its proof establishes.
8. (A9) and the linearised process of Part 4 are stated with $-\gamma_t\xi_t$ noise signs, and with $\Delta^1_0=\Delta_0$. The printed $+$ signs contradict (A8) at $t=2$.

Several formalizations would make the goal trivial, and all are ruled out:

• conditional expectations of non-integrable functions, which are $0$ in Lean (every noise process is required to be in $L^2$);
• a real supremum for the uniform integrability in Assumption 3.3, which is $0$ on unbounded families;
• an arbitrary process with a property in place of the recursion (7);
• a degenerate Dirac target (the covariance $G^{-1}S(G^{-1})^T$ is positive definite under the hypotheses).

Welcome contributions: the Robbins–Siegmund theorem, a vector martingale CLT under conditional Lindeberg conditions, the Kronecker lemma, and the matrix estimates of Lemma 1.

Selected references

• B. T. Polyak, A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
• H. Robbins, S. Monro, A stochastic approximation method, Ann. Math. Statist. 22, 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• J. Sacks, Asymptotic distribution of stochastic approximation procedures, Ann. Math. Statist. 29, 373–405, 1958. https://doi.org/10.1214/aoms/1177706619
• D. Ruppert, Efficient estimations from a slowly convergent Robbins–Monro process, Cornell University ORIE Technical Report 781, 1988 (no stable online link located).
• H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 233–257, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8