Probability

Motivation

A firm that sets prices without knowing how demand responds to them has to learn the demand curve from its own sales. Each price it charges is both a revenue decision and an experiment. The natural policy, certainty equivalent pricing, re-estimates the demand parameters after every period and charges the price that would be optimal if the estimates were exact. den Boer and Zwart show that this policy can fail: with positive probability its prices settle at a suboptimal value, because they converge too fast for the estimates to keep improving (den Boer–Zwart 2014, Proposition 1, the subject of the companion mission). The same phenomenon was found by Lai and Robbins (1982) for a linear control problem.

Their remedy, Controlled Variance Pricing (CVP), keeps certainty equivalent pricing but forces the sample variance of the chosen prices to decay no faster than $t^{\alpha-1}$. The main result is that this small amount of enforced exploration gives regret $O(T^\alpha + T^{1-\alpha}\log T)$, hence $O(T^{1/2+\delta})$ for every $\delta > 0$, for a broad class of demand models that are specified only through their first two moments. Keskin and Zeevi (2014) later placed CVP in a larger family of semi-myopic policies with $\sqrt T\log T$ regret for linear demand.

Setting

A seller chooses in each period $t = 1, 2, \dots$ a price $p_t \in [p_l, p_h]$, with $0 < p_l < p_h$, and then observes demand $d_t$. Demand at price $p$ has mean $h(a_0^{(0)} + a_1^{(0)}p)$ and variance $\sigma^2 v(h(a_0^{(0)} + a_1^{(0)}p))$, where the link $h$ and variance function $v$ are known and $C^2$ on $[0,\infty)$, $\dot h > 0$, and the parameter $a^{(0)} = (a_0^{(0)}, a_1^{(0)})$ with $a_0^{(0)} > 0 > a_1^{(0)}$ is unknown. The noise $e_t = d_t - h(a_0^{(0)} + a_1^{(0)}p_t)$ is a martingale difference with conditional variance $\sigma^2 v(\cdot)$ and a uniformly bounded conditional moment of some order $r > 3$.

The expected revenue is $r(p, a) = p\,h(a_0 + a_1p)$. Near $a^{(0)}$ it has a unique maximizer $p(a)$ in the open interval $(p_l, p_h)$ with $\partial_p^2 r < 0$ there, and $p_{\mathrm{opt}} = p(a^{(0)})$. The regret of a policy is

$$\operatorname{Regret}(T) = \mathbb E\Big[\sum_{t=1}^T r(p_{\mathrm{opt}}, a^{(0)}) - r(p_t, a^{(0)})\Big].$$

The estimate $\hat a_t$ is the maximum quasi-likelihood estimate (MQLE), the root of the quasi-score equation (3), $\sum_{i\le t} \frac{\dot h}{\sigma^2 v(h)}(1, p_i)^\top(d_i - h(\hat a_0 + \hat a_1 p_i)) = 0$. With $\bar p_t$ and $\operatorname{Var}(p)_t$ the sample mean and variance of $p_1,\dots,p_t$, the taboo interval is $\mathrm{TI}(t) = (\bar p_t - w_t, \bar p_t + w_t)$ with $w_t = \sqrt{c[(t+1)^\alpha - t^\alpha](t+1)/t}$. CVP starts from two distinct prices $p_1, p_2$, fixes $\alpha \in (0,1)$ and $0 < c < 2^{-\alpha}(p_1-p_2)^2\min\{1,(3\alpha)^{-1}\}$, and for $t \ge 2$: if $\hat a_t$ does not exist or has the wrong signs, it charges whichever of $p_1, p_2$ is farther from $\bar p_t$; otherwise it charges $p(\hat a_t)$ if that keeps $\operatorname{Var}(p)_{t+1} \ge c(t+1)^{\alpha-1}$, and the best price outside $\mathrm{TI}(t)$ if not.

Formalization targets

Goal: Theorem 1

$$\operatorname{Regret}(T, \mathrm{CVP}) = O\big(T^\alpha + T^{1-\alpha}\log T\big) \qquad (1/2 < \alpha < 1),$$

stated as: there is $K > 0$, depending on the model, $\alpha$, $c$ and the initial prices but not on $T$, with $\operatorname{Regret}(T) \le K(T^\alpha + T^{1-\alpha}\log T)$ for all $T \ge 1$. The constant is left free, so the statement survives any sharpening of the constants.

Milestones

1. Proposition 2: $\operatorname{Var}(p)_t \ge c\,t^{\alpha-1}$ for all $t \ge 2$ along every CVP path.
2. Lemma 1: $\lambda_{\max}(P_t) \le (1+p_h^2)t$ and $t\operatorname{Var}(p)_t \le (1+p_h^2)\lambda_{\min}(P_t)$ for the design matrix $P_t = \sum_{i\le t}(1,p_i)^\top(1,p_i)$.
3. Proposition 3: $\hat a_t$ eventually exists, $\hat a_t \to a^{(0)}$ a.s., and for some $\rho_0$, $\mathbb E[T_{\rho_0}^{1/2}] < \infty$ and $\mathbb E[\|\hat a_t - a^{(0)}\|^2\mathbf 1_{t > T_{\rho_0}}] = O(\log t/t^\alpha)$.
4. Eq. (11): in the normal–linear case, $\mathbb E\|\hat a_t - a^{(0)}\|^2 = O(\log t / t^\alpha)$.
5. Eqs. (17), (18), (20): the quadratic revenue gap, the local Lipschitz bound on $p(a)$, and $|p_{t+1} - p(\hat a_t)| \le |\mathrm{TI}(t)|$ for large $t$.
6. The closing bound $\mathbb E[(p_t - p_{\mathrm{opt}})^2] = O(t^{\alpha-1} + \log t/t^\alpha)$.

Significance

The theorem shows that a policy that is certainty equivalent almost all of the time, with a single interpretable tuning parameter $\alpha$, attains regret $O(T^{1/2+\delta})$ in generalized linear demand models, without distributional assumptions beyond two moments. It explains the role of $\alpha$ precisely: $T^\alpha$ is the cost of exploration and $T^{1-\alpha}\log T$ the cost of estimation error. Proposition 2 and Lemma 1 are reusable for any policy that enforces a variance floor on its actions, and (11) is a self-contained rate for least squares under adaptively chosen designs.

The result is proved in the paper, with Proposition 3 delegated to den Boer and Zwart (2012) for general links. To our knowledge none of it has been machine-checked. A formalization would verify the delegated consistency argument, fix the conditions under which it applies (see Formalization scope), and provide a Lean development of adaptive least squares and quasi-likelihood rates that the related Keskin–Zeevi missions also need.

Difficulty

The deterministic parts are short. The difficulty is Proposition 3. The prices are chosen adaptively from past data, so the regressors are not independent of the noise, and standard rates for (quasi-)likelihood estimates do not apply. The natural argument, bounding $\|\hat a_t - a^{(0)}\|^2$ by $Q_t/\lambda_{\min}(P_t)$ with $Q_t$ a self-normalized martingale quadratic form, needs a bound $\mathbb E[Q_t] = O(\log t)$ that holds in expectation and not only almost surely, as in Lai and Wei (1982). For a non-linear link the MQLE is defined only implicitly, and its existence near $a^{(0)}$ has to be shown first, with a moment bound on the last time it fails. That is the random time $T_\rho$. Turning almost-sure consistency into a rate in expectation is where most of the work lies.

Formalization scope

All declarations live in the namespace CVPricing.Regret. Periods are 1-based. Prices, demands and parameters are real; $a = (a_0, a_1) \in \mathbb R \times \mathbb R$ with the Euclidean norm (euclidNorm), not Mathlib's sup norm. The design matrix, sample mean and $t\operatorname{Var}(p)_t$ are the published Keskin–Zeevi definitions fisherOf, avgPriceOf, infoMetricOf. Every $O(\cdot)$ is "there is $K > 0$ such that for all $t$", with $K$ quantified after the model data. Rates are stated for $t \ge 2$ and the regret for $T \ge 1$. $h$ and $v$ are total functions constrained on $[0,\infty)$. A root of (3) counts only where $\hat a_0 + \hat a_1 p_i \ge 0$ for every observed $p_i$. CVP is a predicate on a realized path that allows every maximizer in (7) and (8).

Disclosed deviations from the page:

• the model requires $a_0^{(0)} + a_1^{(0)}p_h > 0$ (printed: $\ge 0$), because in the boundary case the policy's case (c) fires infinitely often and the proof of Theorem 1 does not cover it;
• (3) is assumed to have at most one root (the page notes roots need not be unique, and the policy cannot select the root nearest $a^{(0)}$);
• the neighbourhood assumption is read as a unique maximizer over $[p_l, p_h]$ lying in $(p_l, p_h)$;
• the demand process is given by its conditional mean, its conditional variance and (2), with integrable noise moments, not by a fixed law $D(p)$;
• the initial prices are deterministic.

Corrected slips: Proposition 2 is stated for $c \le 2^{-\alpha}(p_1-p_2)^2\min\{1/2,(3\alpha)^{-1}\}$, because the printed range fails at $t=2$ ($\operatorname{Var}(p)_2 = (p_1-p_2)^2/4$, not $/2$). Theorem 1 keeps the printed range. Eq. (20) is stated for $p_{t+1}$ and for $t$ beyond an explicit threshold.

The goal does not assume the variance bound, consistency or (20). The policy contains the variance check and the taboo interval, and the regret is the expectation over the actual price process. A statement that assumed any of these, or that dropped the taboo step, would be trivial or false. Contributions are welcome on adaptive least squares (Sherman–Morrison and determinant-ratio bounds), martingale last-time moment bounds, and the implicit-function step (18).

Selected references

• A. V. den Boer, B. Zwart, Simultaneously Learning and Optimizing Using Controlled Variance Pricing, Management Science 60(3):770–783, 2014. https://doi.org/10.1287/mnsc.2013.1788
• A. V. den Boer, B. Zwart, Mean square convergence rates for maximum quasi-likelihood estimators, Stochastic Systems 4(2):375–403, 2014 (cited as 2012 working paper). https://doi.org/10.1214/12-SSY086
• T. L. Lai, C. Z. Wei, Least squares estimates in stochastic regression models with applications to identification and control of dynamic systems, Annals of Statistics 10(1):154–166, 1982. https://doi.org/10.1214/aos/1176345697
• T. L. Lai, H. Robbins, Iterated least squares in multiperiod control, Advances in Applied Mathematics 3(1):50–73, 1982. https://doi.org/10.1016/S0196-8858(82)80005-5
• N. B. Keskin, A. Zeevi, Dynamic Pricing with an Unknown Demand Model: Asymptotically Optimal Semi-Myopic Policies, Operations Research 62(5):1142–1167, 2014. https://doi.org/10.1287/opre.2014.1294

Why myopic pricing is a problem

A seller who does not know how demand responds to price has to learn the demand curve from its own sales while it is selling. The most natural policy is certainty equivalent pricing (also called myopic pricing or passive learning): after every period, estimate the unknown demand parameters from all data collected so far, and charge the price that would be optimal if the estimates were the truth. It is simple, uses all data, and is what a price manager would do without further thought.

den Boer and Zwart (Management Science 60(3):770–783, 2014) show that this policy can fail. In the linear-demand, Gaussian-noise model, the prices it produces fail to converge to the optimal price with positive probability: the policy is not strongly consistent. The result motivates the paper's main contribution, controlled variance pricing, which adds just enough price dispersion to keep learning (treated in the companion mission of this series).

The phenomenon has a history in adaptive control:

• 1976. Anderson and Taylor study the linear system $y_t = a_0 + a_1x_t + \epsilon_t$ controlled by a certainty equivalent rule that steers $y_t$ to a target, and examine by simulation the statistical properties of the least squares estimates it produces (Econometrica 44(6), 1976).
• 1982. Lai and Robbins (Adv. Appl. Math. 3(1), 1982) prove that there are parameter values for which the certainty equivalent controls converge with positive probability to a value different from the optimal control.
• 2014. den Boer and Zwart adapt the argument to revenue maximization with linear demand, without the conditions Lai and Robbins place on the initial inputs and the input bounds: any two different initial prices in $[p_l, p_h]$ give the failure with positive probability.

Setting

A monopolist sells one product in periods $t = 1, 2, \dots$ at prices $p_t$ from an interval $[p_l, p_h]$ with $0 < p_l < p_h$. The demand in period $t$ is

$$d_t = a_0^{(0)} + a_1^{(0)} p_t + e_t ,$$

where $e_1, e_2, \dots$ are independent $N(0, \sigma^2)$ random variables. The parameters are unknown to the seller and satisfy $\sigma > 0$, $a_0^{(0)} > 0$, $a_1^{(0)} < 0$, $a_0^{(0)} + a_1^{(0)}p_h \ge 0$. The expected revenue at price $p$ is $r(p, a_0, a_1) = p(a_0 + a_1p)$, maximized at the optimal price

$$p_{\mathrm{opt}} = -\frac{a_0^{(0)}}{2a_1^{(0)}}, \qquad p_l < p_{\mathrm{opt}} < p_h .$$

Certainty equivalent pricing charges two different initial prices $p_1 \ne p_2$ in $[p_l, p_h]$. After $t \ge 2$ periods it computes the least squares estimates $\hat a_t = (\hat a_{0t}, \hat a_{1t})$, the solution of the normal equations $\sum_{i \le t}(1, p_i)^{\mathsf T}(d_i - \hat a_{0t} - \hat a_{1t}p_i) = 0$, and charges

$$p_{t+1} = \arg\max_{p \in [p_l, p_h]} p\,(\hat a_{0t} + \hat a_{1t}p),$$

with $p_{t+1} = p_h$ when the estimated slope $\hat a_{1t}$ is nonnegative.

Formalization targets

Goal: Proposition 1

$$P\big(p_t \not\to p_{\mathrm{opt}}\big) > 0 .$$

The goal states only the failure of convergence, for every admissible parameter and every pair of different initial prices; it does not fix where the prices go.

Stronger: the prices stick at the boundary

$$P\big(p_t = p_h \ \text{for all } t \ge 3\big) > 0 .$$

This is what the paper's argument establishes; since $p_{\mathrm{opt}} < p_h$ it implies the goal.

Milestones

The milestones are the displayed steps of the appendix proof, in attack order: the determinant of the coefficient matrix of the linear system (12); the bound $P(\sup_{t \ge 3}|(t-2)^{-1}\sum_{i=3}^t e_i| > \epsilon) \le 8\sigma^2\epsilon^{-2} < 1$ for $\epsilon > \sqrt 8\,\sigma$; positivity of the probability of an explicit event $A_\delta$ on the noise for large $\delta$; the case $t = 2$ (the first fitted line pushes $p_3$ to $p_h$); the representation $\hat a_t - a^{(0)} = (\bar e_t - \bar p_tC_t/V_t,\ C_t/V_t)$ of the least squares error; recursive and closed forms of $V_t$ and $C_t$; and the deterministic induction that every noise path in $A_\delta$ keeps the price at $p_h$ forever.

Significance

The result is the standard counterexample to certainty equivalence in dynamic pricing. It shows that estimation and optimization cannot be separated naively: a policy that always exploits its current estimate can lock itself into a price at which the data no longer move the estimate enough to correct it. Every later policy in this literature that forces exploration (controlled variance pricing, semi-myopic policies, constrained iterated least squares) is designed against this failure, and its necessity is argued by pointing to results of this kind.

The result is proved in the paper; nothing here is open. To our knowledge it has no machine-checked proof. Formalizing it adds:

• a verified pathwise analysis of the least squares recursion along a price path, reusable for other proofs about adaptive estimation with two parameters;
• a verified maximal bound for running means of i.i.d. Gaussian noise, of the kind used in many consistency proofs;
• a clean probabilistic statement of the failure, against which consistency results for exploration policies can later be contrasted.

Difficulty

The obvious heuristic, "with positive probability the first two observations are so noisy that the fitted slope is wrong", is not enough: one bad estimate is corrected by later data unless the policy stops generating informative data. The proof has to control the whole infinite future. It does so by showing that on a single event, defined through the first two noise values and a uniform bound on all later running means, the price stays at $p_h$ forever, which requires the closed form of the least squares estimate along a price path that is constant from period 3 on. That event involves infinitely many noise variables, so its probability is positive only through a maximal inequality, and independence between $(e_1, e_2)$ and the later noise. A second subtlety is the choice of constants: the size of the band $\delta$ enters the conditions on $(e_1, e_2)$, so the order in which $\delta$ and the set of admissible $(e_1, e_2)$ are chosen matters (the printed proof picks them in a circular order; a non-circular choice exists).

Formalization scope

• Model. CVPricing.CertEquiv.Model bundles $p_l, p_h, a_0^{(0)}, a_1^{(0)}, \sigma$ with the standing assumptions of §2 as fields, including $p_l < p_{\mathrm{opt}} < p_h$ (the paper's neighbourhood assumption specialized to linear demand). The noise is the referenced published definition RobustBooking.Shared.GaussianNoise (measurable, mutually independent, each $N(0, \sigma^2)$); its Lean index $k$ is period $k+1$, so the paper's $e_i$ is ε (i - 1).
• Policy. cePrice is a deterministic recursion on a noise path, so the random price process is obtained by evaluating it at $\omega$. Periods are 1-based. The least squares estimate is the referenced KeskinZeevi.SufficientConditions.lsEstimateOf, the solution of the normal equations (4), unique whenever $p_1 \ne p_2$. The certainty equivalent rule is the projection of $-\hat a_{0t}/(2\hat a_{1t})$ onto $[p_l, p_h]$ when $\hat a_{1t} < 0$, and $p_h$ when $\hat a_{1t} \ge 0$; the latter is the convention the paper's proof adopts for wrong-signed estimates.
• Corrected slips. The definition of the event $A$ is printed with "$\delta|\bar e_t| \le \delta$" (read $|\bar e_t| \le \delta$) and with its second line missing a factor $\delta$ on the term $(2p_h - p_1 - p_2)$; both are restored as in (12) and the last display of the proof. The intercept of the first fitted line is printed without $a_0^{(0)}$; the correct intercept is stated, and the printed condition remains sufficient for $p_3 = p_h$.
• WLOG. The steps of the proof assume $p_1 < p_2$ and are stated under that ordering; the goal and the stronger statement cover $p_1 \ne p_2$.
• No trivialization. The goal is a statement about the Gaussian law of the noise: a theorem that exhibits one bad noise path, or that assumes $P(A) > 0$, does not prove it. The event in the goal is a set of outcomes whose measurability is not asserted.
• Welcome contributions. Kolmogorov's maximal inequality for sums of independent square-integrable variables; least squares identities for two-parameter regression; the independence argument separating $(e_1, e_2)$ from the later noise.

Selected references

• A. V. den Boer, B. Zwart, Simultaneously Learning and Optimizing Using Controlled Variance Pricing, Management Science 60(3):770–783, 2014. https://doi.org/10.1287/mnsc.2013.1788
• T. L. Lai, H. Robbins, Iterated least squares in multiperiod control, Advances in Applied Mathematics 3(1):50–73, 1982. https://doi.org/10.1016/S0196-8858(82)80005-5
• T. W. Anderson, J. B. Taylor, Some experimental results on the statistical properties of least squares estimates in control problems, Econometrica 44(6):1289–1302, 1976. https://doi.org/10.2307/1914261
• Y. S. Chow, H. Teicher, Probability Theory: Independence, Interchangeability, Martingales, 3rd ed., Springer, 2003. https://doi.org/10.1007/978-1-4612-1950-7

Motivation

The lost-sales inventory problem with lead times is a basic model of operations management. A retailer reviews one product's stock each period and places an order that arrives $L$ periods later. Demand that cannot be met from stock on hand is lost, and the retailer pays a holding cost $h$ per unit left on the shelf and a penalty $p$ per unit of lost demand. The optimal policy depends on the whole pipeline of outstanding orders, so the state space grows with $L$, and the problem is computationally hard for long lead times. Simple base-stock (order-up-to) policies are therefore the standard heuristic, and Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 2009) showed they are asymptotically optimal as the lost-sales penalty grows.

Agrawal and Jia (arXiv:1905.04337) study the learning version, in which the demand distribution is unknown and only sales, not demands, are observed. They give an algorithm whose regret against the best base-stock policy is $\tilde O(L\sqrt T)$, improving the earlier bound of Zhang, Chao and Shi, which grows exponentially in $L$. The improvement rests on one structural fact: started from two different states, the base-stock system accumulates expected costs that differ by an amount linear in $L$ and independent of the horizon. That fact, Lemma 2.5 of the paper, is the goal of this mission.

Setting

Fix a lead time $L\ge 0$ and a base-stock level $x$. A state is a vector $\mathbf s=(s(0),s(1),\dots,s(L))$ of real numbers. Its entry $s(0)$ is the on-hand inventory after the current period's arrival, and $s(1),\dots,s(L)$ are the outstanding orders, $s(L)$ the most recent. Under a base-stock policy with level $x$ the states lie in

$$\mathcal S^x=\Big\{\mathbf s : s(i)\ge 0\ \text{for all } i,\ \sum_{i=0}^{L}s(i)=x\Big\}.$$

In each period $t$ a demand $d_t\ge 0$ is drawn, independently across periods, from a distribution $F$ on $[0,\infty)$. The sales are $y_t=\min\{s_t(0),d_t\}$ and the on-hand inventory is $I_t=s_t(0)$. The policy reorders exactly what was sold, so for $L\ge 1$ the next state is

$$\mathbf s_{t+1}=\big(s_t(0)-y_t+s_t(1),\ s_t(2),\ \dots,\ s_t(L),\ y_t\big),$$

and for $L=0$ the state $(x)$ never changes. The pseudo-cost of period $t$ is $C^x_t=h(s_t(0)-y_t)-p\,y_t$, and the value over horizon $T$ from the start state $\mathbf s$ is

$$V^x_T(\mathbf s)=\mathbb E\Big[\sum_{t=1}^{T}C^x_t\ \Big|\ \mathbf s_1=\mathbf s\Big].$$

Along a demand path, $n^x_T(\mathbf s)=\sum_{t=1}^T y_t$ is the total sales and $m^x_T(\mathbf s)=\sum_{t=1}^T I_t$ the total on-hand inventory.

States are compared by the order of Definition B.1: $\mathbf s'\succeq\mathbf s$ if $\mathbf s'-\mathbf s=\delta$ with $\sum_i\delta_i=0$ and some $0\le k\le L-1$ such that $\delta_i\ge 0$ for $i\le k$ and $\delta_i\le 0$ for $i>k$. Thus $\mathbf s'$ holds the same total, shifted toward the shelf. The state $\hat{\mathbf s}=(x,0,\dots,0)$ dominates every state of $\mathcal S^x$.

Formalization targets

Goal: Lemma 2.5 (p. 8)

For every $x$, every horizon $T$, all costs $h,p\ge 0$, every demand law $F$ and all $\mathbf s,\mathbf s'\in\mathcal S^x$,

$$V^x_T(\mathbf s)-V^x_T(\mathbf s')\le 36\max(h,p)\,L\,x .$$

The constant is the paper's printed one. The proof's last display gives $18(h+p)Lx$, a stronger bound, which is deliberately not the goal.

Milestones (Appendix B and the proof of Lemma 2.5)

All of the following hold for $L\ge 1$, along any single demand path that drives both chains:

1. Lemma B.2 (p. 20). If $\mathbf s'_1\succeq\mathbf s_1$ then for $t\le L+1$ the cumulative sales satisfy $Y'_t-Y_t\le\max_{0\le k\le t-1}(\delta_0+\dots+\delta_k)$.
2. Lemma B.3 (p. 20). If moreover $I'_t\ge I_t$ for $t=1,\dots,L+1$, then $n_T(\mathbf s'_{L+1})=n_T(\mathbf s_{L+1})$ for every $T$.
3. Lemma B.5 (p. 21). At the successive first crossing times $\sigma_i,\tau_i$ of Definition B.4, the state order alternates: $\mathbf s'_{\sigma_i}\succeq\mathbf s_{\sigma_i}$ and $\mathbf s'_{\tau_i}\preceq\mathbf s_{\tau_i}$ whenever these times exist.
4. Lemma B.6 (p. 21). If $\mathbf s'\succeq\mathbf s$ in $\mathcal S^x$ then $|n^x_T(\mathbf s')-n^x_T(\mathbf s)|\le 3x$.
5. Lemma B.7 (p. 23). If $\mathbf s'\succeq\mathbf s$ in $\mathcal S^x$ then $|m^x_T(\mathbf s)-m^x_T(\mathbf s')|\le 6Lx$.
6. Proof of Lemma 2.5 (p. 9). $\hat{\mathbf s}\succeq\mathbf s$ for every $\mathbf s\in\mathcal S^x$.
7. Proof of Lemma 2.5 (p. 9). $|V^x_T(\mathbf s)-V^x_T(\hat{\mathbf s})|\le 9(h+p)Lx$.

Significance

Lemma 2.5 bounds the dependence of the base-stock chain's finite-horizon cost on its starting state, uniformly in the horizon. In the paper it yields three consequences: the long-run average cost (the loss) of a base-stock policy does not depend on the initial state (Lemma 2.6), the bias of the chain is bounded by $36\max(h,p)Lx$ (Lemma 2.8), and finite-horizon average costs concentrate around the loss (Lemma 2.10). These feed the regret bound of Theorem 1.3. The lemma is also a statement about the base-stock lost-sales system alone, without any learning, so it is of independent interest for coupling arguments on lost-sales chains.

The paper's proof is complete on paper, but nothing in it has a machine-checked proof. Neither the lost-sales base-stock chain with lead times started from an arbitrary pipeline state nor any of the coupling lemmas of Appendix B is formalized elsewhere. This mission produces a checked proof of the goal and of the pathwise comparison lemmas. Theorem 1.3 is not posed: its supporting lemmas rely on limits whose existence the paper settles only by an informal discretization (Remark 4).

Difficulty

The obvious argument couples the two chains on a common demand path and waits until they coalesce. Coalescence is guaranteed only after $L$ consecutive periods of zero demand, an event of probability exponentially small in $L$, so this argument gives a bound exponential in $L$. That is the bound of earlier work.

The linear bound needs a finer pathwise accounting. The two coupled chains do not stay ordered: the one that starts with more inventory on the shelf sells more at first, then runs short and sells less. The order $\succeq$ between the two states alternates along a sequence of times, and the sales gained in one phase must be shown to be lost again in the next, so that the cumulative difference stays bounded by a constant multiple of $x$ for every horizon. Turning this alternation into a bound requires tracking how the pipeline vectors evolve between alternation times, including the boundary cases in which the chains coalesce or the horizon ends inside a phase.

Formalization scope

All declarations live in the namespace LostSalesLearning.ValueGap. A state is a function Fin (L + 1) → ℝ, a demand path is a function ℕ → ℝ≥0, and time is 0-based: traj s d 0 is the paper's $\mathbf s_1$, traj s d t is $\mathbf s_{t+1}$, and $\sum_{t=1}^T$ is a sum over Finset.range T. The demand law $F$ is a probability measure on ℝ≥0, and the demand path has the product law Measure.infinitePi (fun _ => F). The value is the expectation of the summed pseudo-costs, which equals Definition 2.4 by the tower property and is the form used in the paper's proof.

Committed conventions:

• The costs satisfy $h\ge 0$ and $p\ge 0$, the reading of "per unit holding cost and per unit lost sales penalty".
• No assumption is placed on $F$. The paper's assumptions $F(0)>0$ and bounded demand belong to other results.
• The goal holds for every $L\ge 0$; the Appendix B milestones carry $L\ge 1$, as Appendix B does.
• The order $\succeq$ is Definition B.1 verbatim, with the equal-sum clause and the split index $k\le L-1$.
• The pathwise milestones quantify over every demand path and drive both chains with the same path.
• The first crossing times of Definition B.4 are represented by alternationTimes; an absent next crossing is none.

Two trivializing formalizations are ruled out. A comparison of the two values on different or fixed demand paths would be a different statement: the goal compares two expectations under the same law, and each pathwise milestone uses one common path. A Bochner integral of a non-integrable function would be $0$. The integrand here is measurable and bounded by $T(h+p)x$ on $\mathcal S^x$, so the values are genuine expectations.

A complete development needs the elementary dynamics of the chain, including invariance of $\mathcal S^x$ and the shift of trajectories, which is reusable for other lost-sales models. It also needs the alternation times of Definition B.4, and measurability of the trajectory in the demand path. Proofs of individual milestones, alternative proofs of the goal, and sharper constants as separate statements are all welcome.

Selected references

• S. Agrawal and R. Jia, Learning in Structured MDPs with Convex Cost Functions: Improved Regret Bounds for Inventory Management, arXiv:1905.04337v1, 2019. https://arxiv.org/abs/1905.04337
• W. T. Huh, G. Janakiraman, J. A. Muckstadt and P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945
• H. Zhang, X. Chao and C. Shi, Closing the Gap: A Learning Algorithm for Lost-Sales Inventory Systems with Lead Times, Management Science 66(5), 2020. https://doi.org/10.1287/mnsc.2019.3288
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

A decision maker choosing a random outcome $X$ (a portfolio return, a policy's cost savings, a schedule's throughput) often has a reference outcome $Y$, the result of a benchmark policy, and wants the new outcome to be preferable to it for every risk-averse decision maker, not just on average. Expected-utility theory (von Neumann and Morgenstern) makes this precise: $X$ is preferred to $Y$ by every decision maker with a concave nondecreasing utility function $u$ exactly when $X$ dominates $Y$ in the second order, $X\succeq_{(2)}Y$. Requiring $X\succeq_{(2)}Y$ as a constraint in an optimization problem avoids having to elicit any particular utility function, which is rarely possible in practice and impossible when several decision makers must agree.

Dentcheva and Ruszczyński (preprint 2002, published in SIAM J. Optim. 14(2), 2003) introduced optimization problems with stochastic dominance constraints and developed their optimality and duality theory. The central finding is that the Lagrange multiplier of a second-order dominance constraint is itself a concave nondecreasing utility function: the optimal solution maximizes the objective plus an expected utility, for a utility function implied by the problem. This interpretation underlies the later literature on dominance-constrained portfolio optimization, risk-averse stochastic programming, and the dual (quantile) theory of stochastic orders.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $\mathcal L^1=\mathcal L^1(\Omega,\mathcal F,P)$ the space of integrable random variables with its norm topology. For $X\in\mathcal L^1$ the distribution function is $F(X;\eta)=P[X\le\eta]$ and the second-order shortfall function is

$$F_2(X;\eta)=\int_{-\infty}^{\eta}F(X;\alpha)\,d\alpha,\qquad \eta\in\mathbb R. \tag{2.1}$$

Changing the order of integration gives $F_2(X;\eta)=\mathbb E[(\eta-X)_+]$ (2.6), where $(\cdot)_+=\max(0,\cdot)$. The relation $X\succeq_{(2)}Y$ means $F_2(X;\eta)\le F_2(Y;\eta)$ for all $\eta$, and $A_2(Y)=\{X\in\mathcal L^1:X\succeq_{(2)}Y\}$.

The problem data are a reference outcome $Y\in\mathcal L^1$, a convex closed set $C\subseteq\mathcal L^1$, a functional $f$ that is concave and continuous on $C$, and an interval $[a,b]$. The paper studies the relaxation in which dominance is enforced on $[a,b]$:

$$\max f(X)\quad\text{subject to}\quad\mathbb E[(\eta-X)_+]\le\mathbb E[(\eta-Y)_+]\ \ \text{for all }\eta\in[a,b],\qquad X\in C. \tag{3.1–3.3}$$

The uniform dominance condition (Definition 4.1) asks for some $\tilde X\in C$ with $\inf_{\eta\in[a,b]}\{F_2(Y;\eta)-F_2(\tilde X;\eta)\}>0$.

The multiplier class $\mathcal U_1$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave and nondecreasing, vanish on $[b,\infty)$, and are affine on $(-\infty,a]$: $u(t)=u(a)+c(t-a)$ for $t\le a$, with a constant $c\ge0$. The Lagrangian is

$$L(X,u)=f(X)+\mathbb E[u(X)]-\mathbb E[u(Y)]. \tag{4.1}$$

Formalization targets

Goal: Theorem 4.2

Assume the uniform dominance condition. If $\hat X$ is an optimal solution of (3.1)–(3.3), there is $\hat u\in\mathcal U_1$ with

$$L(\hat X,\hat u)=\max_{X\in C}L(X,\hat u)\quad(4.2)\qquad\text{and}\qquad\mathbb E[\hat u(\hat X)]=\mathbb E[\hat u(Y)].\quad(4.3)$$

Conversely, if for some $\hat u\in\mathcal U_1$ a maximizer $\hat X\in C$ of $L(\cdot,\hat u)$ satisfies (3.2) and (4.3), then $\hat X$ is optimal for (3.1)–(3.3).

Milestones

The milestones follow the paper's proof. They are: finiteness of $\mathbb E[u(X)]$ for $u\in\mathcal U_1$; the identity (2.6), already proved on the platform; Proposition 2.3 (convexity and closedness of $A_2(Y)$, and its recession cone); the concavity of the constraint operator $G(X)(\eta)=F_2(Y;\eta)-F_2(X;\eta)$ with respect to the cone of nonnegative functions; the existence of a nonnegative measure multiplier $\hat\mu$ on $[a,b]$ satisfying (4.5)–(4.6); the facts that the function $u_\mu(t)=-\int_t^b\mu([\tau,b])\,d\tau$ ($t<b$), $u_\mu(t)=0$ ($t\ge b$) of a nonnegative measure lies in $\mathcal U_1$ and that every $u\in\mathcal U_1$ is $u_\mu$ for exactly one $\mu$; the key identity

$$\int_a^b F_2(X;\eta)\,d\mu(\eta)=-\mathbb E[u_\mu(X)]; \tag{4.9}$$

and the weak-duality step: (3.2) implies $\mathbb E[u(X)]\ge\mathbb E[u(Y)]$ for every $u\in\mathcal U_1$.

Further: Theorem 5.1

With $D(u)=\sup_{X\in C}L(X,u)$, the dual problem $\min_{u\in\mathcal U_1}D(u)$ has a solution, its value equals the primal optimal value, and its solutions are exactly the $\hat u\in\mathcal U_1$ satisfying (4.2)–(4.3).

Significance

Theorem 4.2 turns an infinite family of constraints, one for each $\eta\in[a,b]$, into a single scalar trade-off: at the optimum, the decision maker behaves as an expected-utility maximizer for an implicit utility $\hat u$, and the dominance constraint is active exactly in the sense $\mathbb E[\hat u(\hat X)]=\mathbb E[\hat u(Y)]$. Theorem 5.1 makes $\mathcal U_1$ the space of dual variables, which is the starting point of dual decomposition and cutting-plane methods for dominance-constrained problems and of their extensions to several constraints and to higher orders (Sections 6–7 of the paper, not part of this mission).

All results are proved in the paper. Apart from the identity (2.6), which is proved on the platform, none of them is formalized as far as the platform records show. A machine-checked development would provide, on top of the paper, a rigorous treatment of the measure–utility correspondence that the paper obtains from a textbook theorem "after an obvious adaptation", and a careful account of the multiplier class itself (see the scope section on the constant $c$). The definitions of $F_2$ and of the identity (2.6) are shared with the platform's missions on Dual Stochastic Dominance and Related Mean-Risk Models (Ogryczak and Ruszczyński, 2002).

Difficulty

The necessity half needs a Lagrange multiplier for a constraint taking values in the infinite-dimensional space $\mathcal C([a,b])$; finite-dimensional convex duality does not apply, and the multiplier first appears as a nonnegative measure on $[a,b]$, an element of the dual of $\mathcal C([a,b])$. A Slater-type point is required: without the uniform dominance condition the multiplier may not exist. This is why the dominance relation, which the paper first poses on all of $\mathbb R$, is relaxed to a bounded interval $[a,b]$: for a reference outcome with a smallest value $y_1$, $F_2(Y;y_1)=0$, so no $\tilde X$ can dominate $Y$ strictly near $y_1$.

The second obstacle is the translation of that measure into a utility function. The identity (4.9) requires an interchange of integrals over $\mathbb R\times[a,b]$ and an integration by parts against the distribution function of an arbitrary integrable $X$, followed by a limit in which the integrability of $X$ controls the linear growth of $u$ at $-\infty$. The converse direction needs every $u\in\mathcal U_1$ to be represented by a unique measure, through the left derivative of a concave function.

Formalization scope

Outcomes are elements of Mathlib's $L^1$ space Ω →₁[P] ℝ over a probability measure P, coerced to functions inside integrals; no statement is pointwise in $\omega$. $F_2$ is the published definition DualSSD.Shared.secondPerformance, a Bochner integral of $P[X\le\alpha]$ over $(-\infty,\eta]$. The problem data form a structure whose fields include every standing assumption of the paper: $C$ convex and closed, $f$ concave and continuous on $C$. The constraint (3.2) is stated in its printed expectation form, while Definition 4.1 and the proof objects use $F_2$, as printed; their equality is (2.6).

Committed conventions:

• $\mathcal U_1$ uses $c\ge0$. The paper prints $c>0$. With $c>0$ the necessity half of Theorem 4.2 is false: take $Y\equiv0$, $[a,b]=[1,2]$, $f(X)=\mathbb EX$ and $C$ the constant random variables with values in $[0,1]$. Then $\tilde X\equiv1$ satisfies Definition 4.1, $\hat X\equiv1$ is optimal, and (4.3) forces $c=0$. The proof itself produces $c=\mu([a,b])$, which vanishes for the zero multiplier of a slack constraint, and the paper calls $\mathcal U_1$ a convex cone, which must contain $0$.
• Definition 4.1's infimum is encoded as a positive lower bound $\varepsilon$ on $[a,b]$. "$=\max_{X\in C}$" is encoded as membership in $C$ plus an upper bound over $C$.
• A nonnegative measure in $\mathbf{rca}([a,b])$ is a finite Borel measure on $\mathbb R$ giving zero mass to the complement of $[a,b]$, which is the paper's own extension by zero. Integrals $\int_a^b\cdot\,d\mu$ are over the closed interval, so atoms at $a$ and $b$ count.
• No relation between $a$ and $b$ is assumed. For $a>b$ every statement remains meaningful: the constraint is vacuous and $\mathcal U_1=\{0\}$.
• Theorem 5.1's dual function takes values in the extended reals.

A trivializing formalization is ruled out: a junk-valued expectation (a Bochner integral of a non-integrable function, which Lean sets to $0$) cannot occur for $u\in\mathcal U_1$, and its integrability is a milestone. Dropping the concavity of $f$ or the convexity of $C$ would make the necessity half false, so these assumptions are fields of the problem data.

Infrastructure a complete development needs: convex duality for cone constraints in $\mathcal C([a,b])$ (or a direct separation argument in $\mathbb R\times\mathcal C([a,b])$), the Riesz representation of nonnegative functionals on $\mathcal C([a,b])$, Fubini and integration by parts for Stieltjes measures, and the measure of a left-continuous monotone function. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The extensions to several dominance constraints and to higher-order dominance are not included.

Selected references

• D. Dentcheva and A. Ruszczyński, Optimization with stochastic dominance constraints, preprint dated December 27, 2002 (Stochastic Programming E-Print Series); published in SIAM Journal on Optimization 14(2):548–566, 2003. https://doi.org/10.1137/S1052623402420528
• W. Ogryczak and A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM Journal on Optimization 13(1):60–78, 2002. https://doi.org/10.1137/S1052623400375075
• J. F. Bonnans and A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.