Operations Research

Motivation

A seller with a fixed stock must choose prices before knowing when customers will arrive or what they will be willing to pay. If customers can wait for a later price, the seller must also account for how today's price changes their purchasing decisions. Chen and Farias study this problem with strategic customers and identify a simple inventory-based policy that can be compared with the best attainable revenue. Their Theorem 1 shows that this policy, with discount rate $\beta=1/(1.42T)$ for a season of length $T$, earns at least $0.29$ of the optimal expected revenue. The policy posts the price that is optimal in the canonical discounted revenue-management problem with myopic customers (Gallego and van Ryzin, 1994; Farias and Van Roy, 2010) at the current inventory level. This mission targets the lower-bound half of its argument, stated as Lemma 9: a comparison between the policy's revenue over a fixed selling season and a discounted, infinite-horizon value. The latter comparison is meaningful independently of the paper's strategic-customer benchmark.

Setting

The seller begins with inventory $x_0\in\mathbb N$ and sells at most one item to each customer. Customers arrive at rate $\lambda>0$. Their nonnegative valuations have density $f$ with total mass one. Write $\bar F(p)=\int_p^\infty f(v)\,dv$ for the probability that a valuation exceeds price $p$. A customer who behaves myopically buys at a posted price $p$ exactly when the valuation is high enough, so sales occur at rate $\lambda\bar F(p)$ while that price is posted.

The paper's Assumption 1 concerns the virtual value $\psi(p)=p-\bar F(p)/f(p)$: it is nondecreasing on nonnegative prices and has a nonnegative root. The simple policy is built from a discount rate $\beta>0$ and an infinite-horizon Bellman value $V:\mathbb N\to\mathbb R$. It has $V(0)=0$ and, for $x\ge1$, satisfies the sign-corrected recursion

$$\beta V(x)=\sup_{p\ge0}\lambda\bar F(p)\bigl(p+V(x-1)-V(x)\bigr).$$

At inventory $x\ge1$ the root price $\pi(x)$ is the unique nonnegative solution of $\psi(\pi(x))=V(x)-V(x-1)$. The price posted just before a sale is $\pi(x)$, and the inventory then becomes $x-1$. At zero inventory the posted price is infinity and there are no more sales. The expected sum of prices paid at sales by time $T$ is denoted $J(x_0,T)$. These objects come from §§2–3.1 of the paper.

Formalization targets

The goal is Lemma 9, for every $\lambda,\beta,T>0$ and every initial inventory $x_0$:

$$V(x_0)\le\left(1+\frac{e^{-\beta T}}{\beta T}\right)J(x_0,T).$$

The coefficient is part of the target. No choice of $\beta$ is fixed. The milestones follow the results stated in the paper: inventory monotonicity of $V$, price monotonicity, pathwise monotonicity of the price and its revenue rate (Lemma 7), the expected-rate identity, revenue-per-time monotonicity (Lemma 8), the identification of $V$ with discounted policy revenue, and the comparison through an independent exponential horizon. The last milestone evaluates $\mathbb E[\max\{1,X/T\}]$ exactly for $X\sim\operatorname{Exp}(\beta)$.

Significance

The bound quantifies how much of the discounted value this explicit policy earns within a finite selling season. Its factor depends only on the dimensionless product $\beta T$; it does not depend on inventory, arrival rate or valuation density. Together with the paper's separate upper bound on its strategic benchmark, Lemma 9 contributes to the advertised $0.29$ comparison. The full comparison requires definitions and equilibrium arguments beyond this mission, so the goal here is precisely the fixed-horizon lower bound.

Chen and Farias proved these statements in the published paper. The Lean items in this proposal are statements awaiting machine-checked proofs. A completed development would establish the discounted-value verification step and the fixed-horizon comparison for an explicit pure-death sales process. Its constructions of inventory-dependent sale times and finite-horizon revenue could also be reused in other pricing models with Poisson arrivals.

Difficulty

The Bellman value is specified by an optimization equation, while $J(x_0,T)$ is defined from the actual sales process. Their equality at an exponential horizon does not follow by unfolding a definition. The price chosen through the virtual-value equation must be connected to the Bellman optimum, and the inventory-dependent process must be related to the same value. The paper also relies on the fact that the root price falls as inventory rises, citing Lemma 1 of Farias and Van Roy; that fact does not follow merely from monotonicity of $\psi$ without control of the marginal values $V(x)-V(x-1)$. Lemma 8 then concerns expected revenue over two different horizons, including paths that sell out early.

Formalization scope

The Lean model uses a nonnegative integrable density on $\mathbb R$, zero on negative valuations and normalized to mass one. It adds $f(p)>0$ for every $p\ge0$. This disclosed condition excludes bounded-support densities: without it the paper's quotient $\bar F(p)/f(p)$ can divide by zero and Lean would assign a spurious value. The paper says the root equation has a unique solution under Assumption 1, but nondecreasing $\psi$ alone does not guarantee existence or uniqueness. Accordingly, the root policy is characterized by its equation and an explicit uniqueness condition. The Bellman recursion uses a least-upper-bound predicate rather than a real supremum with a default value on an empty or unbounded set. The corrected sign in the recursion matches the paper's root equation and discounted-revenue equation.

For stock $x_0$, the model uses $x_0$ independent rate-one exponential clocks. At inventory $x$, the next holding time is the next clock divided by $\lambda\bar F(\pi(x))$. Sales are numbered $1,\ldots,x_0$, and sale $k$ earns $\pi(x_0-k+1)$. The law is the myopic sales process with intensity $\lambda\bar F(\pi(x))$. Expected revenues are lower integrals in the extended nonnegative reals; nonnegative prices make their real-to-extended conversion exact. An independent $X\sim\operatorname{Exp}(\beta)$ is represented by an outer integral over its law. The factor $\lambda$ missing from the paper's printed compensator display is restored, and the paper's intermediate $1+e^{-\beta T}/T$ is read with the missing $\beta$ restored.

The strategic-customer types, stopping rules, perfect Bayesian equilibrium, and the identification of the strategic policy's revenue with myopic-sales revenue are not formalized here. Neither are Theorem 1's $\mathrm{OPT}$ and $J^*$ benchmarks: their specification is not pinned down sufficiently in the paper for this proposal. In particular, $J$ is constructed from sale times and payments, never from $V$, and $V$ is specified by the Bellman equation, never as the policy's revenue. Contributions toward the goal include the individual milestones and reusable facts about the clock process, its revenue, and the exponential horizon.

Selected references

• Y. Chen and V. F. Farias, Robust Dynamic Pricing with Strategic Customers, Mathematics of Operations Research 43(4):1119–1142, 2018. DOI: 10.1287/moor.2017.0897.
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. DOI: 10.1287/mnsc.40.8.999.
• V. F. Farias and B. Van Roy, Dynamic Pricing with a Prior on Market Response, Operations Research 58(1):16–29, 2010. DOI: 10.1287/opre.1090.0729.
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. DOI: 10.1007/978-1-4684-9477-8.

Motivation

A seller who changes prices while learning demand faces two costs: a price experiment may earn less revenue now, while insufficient experimentation leaves later prices poorly calibrated. Customer features make the balance harder because both willingness to buy and sensitivity to price may vary between customers. Ban and Keskin study this problem when the number of recorded features can be large relative to the selling horizon. Their known-support policy, ILSX, provides the upper bound formalized here Ban and Keskin, 2021, §§2 and 4.1.

The paper's result is a statement about learning a demand model while serving sequential customers, rather than about fitting that model after all observations are available. A price at period $t$ must use information then available, including the arriving customer's features but excluding that customer's demand shock. The seller therefore needs a policy whose expected revenue loss can be bounded uniformly over the unknown parameters in a specified model Ban and Keskin, 2021, pp. 5552–5556.

Setting

In each period $t=1,2,\ldots$, a customer arrives with a feature vector $Z_t\in\mathbb R^d$. The seller observes the augmented vector $X_t=[1;Z_t]$, posts a price $p_t\in[\ell,u]$ with $0<\ell<u$, and then observes demand. In the linear demand model, demand equals

$$D_t=\alpha\cdot X_t+(\beta\cdot X_t)p_t+\varepsilon_t.$$

The intercept and slope vectors $\alpha,\beta$ are unknown. The seller knows the sparsity structure $\mathcal S$: outside this set of coordinate indices, both parameter vectors vanish. The compressed parameter $\theta_{\mathcal S}=(\alpha_{\mathcal S},\beta_{\mathcal S})$ lies in a compact coordinate rectangle $\Theta_{\mathcal S}$, and $s=|\mathcal S|\ge1$. The compressed customer vector is $X_{\mathcal S,t}=(X_{t,i})_{i\in\mathcal S}$ Ban and Keskin, 2021, pp. 5552–5555.

At price $p$, expected single-period revenue is $r(p,\theta_{\mathcal S},x)=p[\alpha_{\mathcal S}\cdot x+(\beta_{\mathcal S}\cdot x)p]$. The clairvoyant price is $\varphi(\theta_{\mathcal S},x)=-(\alpha_{\mathcal S}\cdot x)/(2\beta_{\mathcal S}\cdot x)$ when the slope is negative. The paper assumes this price is in $(\ell,u)$ throughout its model domain. Expected regret $\Delta^{\pi}_{\theta_{\mathcal S}}(T)$ is the expected sum, through period $T$, of the clairvoyant revenue minus the revenue at the policy's price Ban and Keskin, 2021, (2)–(4), p. 5553–5554.

The ILSX policy charges one fixed experimental price $m_1$ at periods $1,4,9,\ldots$ and a distinct price $m_2$ at periods $2,5,10,\ldots$. At every other period it estimates the compressed demand parameter by least squares using experimental observations, projects the estimate onto $\Theta_{\mathcal S}$, and applies $\varphi$ to the projected estimate and the current customer vector. Both prices lie in $[\ell,u]$ Ban and Keskin, 2021, (7), (8), (12), pp. 5555–5556.

Formalization targets

The goal is Theorem 2: for the stated model and ILSX policy, a finite positive constant $C$ exists such that

$$\Delta^{\mathrm{ILSX}(m_1,m_2)}_{\theta_{\mathcal S}}(T)\le Cs\sqrt T\log T\qquad(\theta_{\mathcal S}\in\Theta_{\mathcal S},\ T\ge2).$$

The constant is chosen after the model, shock process, experimental prices, and estimator selection are fixed, but before the parameter and horizon. The theorem and Remark 5 are on pp. 5556–5557 of Ban and Keskin, 2021.

The milestones reproduce the paper's route into this claim: the experimental-period count following (7); the growth bound (15) for the price-variation statistic $J_t$; Lemma 1's minimum-eigenvalue probability bound for the experimental information matrix $\widetilde{\mathcal J}_{\mathcal S,t}$; and Lemma 2's high-probability bound for its noise-driven estimation error. The least-squares error identity (11) is included as a supporting item on invertible samples, not as a milestone. The constants and thresholds in these targets remain existential where the article leaves them existential Ban and Keskin, 2021, pp. 5555–5556.

Significance

The theorem gives a guarantee for a concrete pricing policy under feature-dependent price sensitivity. The bound grows with the horizon at order $\sqrt T\log T$ for a fixed known support, with an explicit factor $s$ in the published statement. It lets a seller compare the cost of this policy with the revenue of a seller who knew the demand coefficients before pricing. The paper presents its result as matching its lower-bound benchmark up to logarithmic factors, under the paper's respective hypotheses Ban and Keskin, 2021, Theorems 1–2, pp. 5554–5556.

The mathematical result was published in 2021. This mission seeks a machine-checked statement and proof of the known-support guarantee and its stated intermediate results. The checked Prove2Me prior-art catalog contains featureless dynamic-pricing results and separate least-squares results, but no matching formalization of ILSX. A completed development would add reusable definitions for a feature-dependent price regressor, experimental information matrix, nonanticipating estimator selection, and expected regret. The article places its proofs in an electronic companion, which is not included in the held source PDF; this mission does not reproduce those proofs as source material.

Difficulty

The policy learns from a sparse set of deliberately chosen periods, while its regret accumulates at every period. A pointwise least-squares identity alone does not control the regret: the information matrix can be singular at early periods, and the customer features and shocks are random. In particular, the printed inverse identity (11) says “for all $t\ge2$”, although at $t=2$ the matrix has rank at most two and cannot be invertible when $s\ge2$. The formal statement therefore confines the inverse identity to invertible samples. Lemma 2's event also includes invertibility so a default inverse of a singular matrix cannot make its error bound automatic Ban and Keskin, 2021, (9)–(11), Lemma 2, p. 5556.

Formalization scope

Lean uses one-based periods and a support subtype of the augmented feature coordinates. Coordinate zero is the paper's intercept coordinate one. The parameter has coordinates $(j,i)$ for demand intercept or price slope $j\in\{0,1\}$ and support index $i\in\mathcal S$. The regressor $[1;p]\otimes X_{\mathcal S,t}$ gives the information matrix in (10). Euclidean squared norms are explicit sums of squares, and the minimum-eigenvalue claim is the equivalent Rayleigh inequality. The parameter rectangle is nonempty, and its Euclidean projection is coordinatewise clamping.

The standing assumptions are $d\ge1$, $s\ge1$, $0<\ell<u$, distinct experimental prices in $[\ell,u]$, bounded i.i.d. features with mean zero and positive-definite covariance, and a fixed shock process with conditional mean zero, bounded conditional second moment, and finite conditional exponential moments near zero. The feature process is measurable and integrable. The model additionally states independence of the next customer's features from the past primitives, the reading of the paper's joint probability construction used here. The slope is negative and the clairvoyant price lies in $(\ell,u)$ for every allowed parameter and realized feature. These conditions ensure that the price formula represents a genuine revenue maximum. The phrase about continuous features having positive measure in the interior of their domains is omitted because the page does not specify the domains or a reference measure Ban and Keskin, 2021, §2, pp. 5552–5554.

The estimator is any measurable minimizer of the experimental least-squares objective for histories with at least two observations. Its type depends only on earlier observations; at nonexperimental periods the recorded pseudo-observations are ignored by the objective. The shock law is fixed while the parameter varies. Expected regret uses a nonnegative integral, and conditional second and exponential moments use nonnegative conditional expectations. The theorem binds $C$ before the parameter and horizon, while leaving support size fixed with the model. Consequently, the stronger uniformity in $s$ suggested by Remark 5 is outside this statement. These choices exclude vacuous integrals, unconstrained estimators, and accidental bounds from a singular matrix inverse. Work on the probability estimates, least-squares identity, and regret bound is welcome under these exact definitions.

Selected references

• G.-Y. Ban and N. B. Keskin, Personalized Dynamic Pricing with Machine Learning: High-Dimensional Features and Heterogeneous Elasticity, Management Science 67(9):5549–5568, 2021. DOI: 10.1287/mnsc.2020.3680.

Motivation

Online combinatorial optimization is a repeated game in which a learner selects, round after round, a structured object (a subset of fixed size, a path, a matching, a spanning tree) encoded as a 0/1 vector, and an adversary assigns a cost to every coordinate. It models routing, ranking, scheduling and many other sequential decision problems in operations research and machine learning, and it contains prediction with expert advice as the special case of one-hot vectors.

The most widely used algorithm for this game is the exponentially weighted forecaster, which keeps a weight on every action and multiplies it by $\exp(-\eta\cdot\text{loss})$ after each round. Applied to a combinatorial action set it is called EXP2 (Audibert, Bubeck and Lugosi), or Expanded Hedge in the full-information case (Koolen, Warmuth and Kivinen, COLT 2010). Its standard analysis gives regret of order $m^{3/2}\sqrt{n\log(d/m)}$, while online mirror descent with the negative entropy (Component Hedge) achieves $m\sqrt{n\log(d/m)}$, which is optimal. Koolen, Warmuth and Kivinen left open whether a better tuning or a better analysis of EXP2 could close this gap.

Timeline.

• 1997: Freund and Schapire analyse Hedge for experts.
• 2010: Koolen, Warmuth and Kivinen introduce Component Hedge, prove the $m\sqrt{n\log(d/m)}$ bound, and ask whether Expanded Hedge can match it.
• 2012–2014: Audibert, Bubeck and Lugosi (arXiv:1204.4710; Math. Oper. Res. 39(1), 2014) answer negatively: Theorem 1 exhibits an action set on which EXP2's full-information regret is at least $0.01\,d^{3/2}\sqrt n$ for every learning rate.

Setting

Fix integers $d$ (the dimension) and $n$ (the number of rounds). An action set is a nonempty finite set $\mathcal A\subseteq\{0,1\}^d$ whose elements all have the same number $m$ of ones: $\|a\|_1=m$ for every $a\in\mathcal A$. At each round $t=1,\dots,n$:

1. the player chooses a probability distribution $p_t$ on $\mathcal A$ and draws $a_t\sim p_t$;
2. simultaneously, the adversary chooses a loss vector $z_t\in[0,1]^d$;
3. the player pays $a_t^\top z_t$ and, in the full-information game, observes $z_t$.

The regret after $n$ rounds is

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

EXP2 with learning rate $\eta$ starts from the uniform distribution $p_1$ on $\mathcal A$ and updates, for every $a\in\mathcal A$,

$$p_{t+1}(a)=\frac{\exp(-\eta\,a^\top z_t)\,p_t(a)}{\sum_{b\in\mathcal A}\exp(-\eta\,b^\top z_t)\,p_t(b)} .$$

In the Lean development IsBinaryActionSet A m is the action-set condition, exp2Weights A η z t is $p_{t+1}$, and exp2Regret A η z n is $R_n$ against a fixed loss sequence $z$. thmOneSet d, adv1 d and adv2 d ε are the action set and the two adversaries of the paper's proof.

Formalization targets

Goal: Theorem 1 (p. 6)

For $n\ge d$ with $d$ a multiple of $4$, there is an action set $\mathcal A\subseteq\{0,1\}^d$ with constant $\|a\|_1$ such that for every $\eta\ge0$ some adversary with losses in $[0,1]^d$ makes EXP2 pay

$$R_n\ \ge\ 0.01\,d^{3/2}\sqrt n .$$

The action set is chosen before the learning rate, and the adversary after it.

Milestones (App. A and App. C)

1. Lemma 3 (p. 19): for $k\ge1$ and $1\le c\le 2$,

$$\frac{\sum_{i=0}^k(1-i/k)\binom ki^2c^i}{\sum_{i=0}^k\binom ki^2c^i}\ \ge\ \frac13 .$$

2. First adversary (p. 15): on the action set of App. A, against the alternating adversary, $R_n=\frac{nd}{16}\tanh\frac{\eta d}{8}$ for $n$ even.
3. Second adversary (p. 16): against the constant adversary with $\varepsilon=\min(\log2/(\eta n),1)$, $R_n\ge\min\bigl(\frac{d\log2}{12\eta},\frac{nd}{12}\bigr)$ for $\eta>0$.
4. Optimization over $\eta$ (pp. 14–15): for every $\eta>0$,

$$\max\Bigl(\tfrac{nd}{16}\tanh\tfrac{\eta d}{8},\ \min\bigl(\tfrac{d\log2}{12\eta},\tfrac{nd}{12}\bigr)\Bigr)\ \ge\ \min\bigl(0.04\,nd,\ 0.01\,d^{3/2}\sqrt n\bigr).$$

Significance

The result. Theorem 1 shows that the gap between EXP2 and mirror descent with the negative entropy is not an artefact of the analysis: on an action set with $m=d/2$, where the optimal rate is of order $d\sqrt n$, no learning rate brings EXP2 below $0.01\,d^{3/2}\sqrt n$. Exponential weights over the actions are therefore provably suboptimal in online combinatorial optimization, which motivates working with the convex hull of $\mathcal A$ (mirror descent) rather than with the actions themselves. The construction is also a template for algorithm-specific lower bounds: two adversaries, one punishing large and one punishing small learning rates.

Formalizing it. The result is proved in the paper (App. A, with Lemma 3 in App. C); to our knowledge none of it is machine-checked. A formalization yields a checked algorithm-specific lower bound for exponential weights, an exact closed-form regret computation for EXP2 on a structured action set, and a rigorous proof of Lemma 3, whose printed proof checks $k\le10^6$ numerically before an asymptotic argument with Stirling's formula.

Difficulty

The statements are elementary, but each step hides a real computation. The first adversary requires the exact distribution of EXP2 on a set of $2\binom{d/2}{d/4}$ actions over alternating rounds, and a regret identity rather than a bound. The second requires controlling EXP2's expected loss over all $n$ rounds against a constant adversary on the same exponentially large set. Lemma 3 is the hardest piece: at $c=2$ it is tight at $k=1$, while the ratio tends to $1-\sqrt2/(1+\sqrt2)\approx0.414$ as $k\to\infty$; the printed proof verifies $k\le10^6$ numerically, so a formal proof needs an argument valid for every $k$. A naive attempt to prove the goal with a single adversary fails: one adversary only defeats either large or small learning rates.

Formalization scope

• Actions are real vectors Fin d → ℝ with entries in $\{0,1\}$, so $a^\top z$ is the dot product. Coordinates and rounds are 0-based: the paper's odd rounds are the even indices.
• EXP2 is defined by the recursion of Figure 2 with $\tilde z_t=z_t$, starting uniform on $\mathcal A$; its closed form $p_t(a)\propto\exp(-\eta\sum_{s<t}a^\top z_s)$ is a consequence, not the definition.
• The regret is defined against a deterministic, oblivious loss sequence, for which the expectation is a finite sum. Exhibiting such an adversary proves the paper's $\sup_{\text{adversary}}$, since it is a special case of the paper's adaptive adversaries.
• The minimum over $\mathcal A$ is a Finset.inf'; every statement requires $\mathcal A$ nonempty, so no junk value enters.
• Added hypotheses: $4\mid d$ in the goal (the proof's own simplifying assumption; the printed statement fails at $d=1$, where any constant-norm $\mathcal A$ is a singleton); $\eta>0$ and $n\ge1$ wherever $1/\eta$ or $1/(\eta n)$ appears. The goal does not assume $n$ even, although App. A does; the second-adversary milestone does not need it either.
• The action set of App. A is printed with "or"; it is formalized with exactly one of the two intervals filled, as the prose and the constant norm $\|a\|_1=d/2$ require.
• Ruled out: an existential over $\eta$, an adversary chosen before $\eta$, an action set depending on $\eta$, unbounded losses, and an empty action set with a junk minimum would each make the goal trivial or different; the statement quantifies as above.

Contributions welcome: proofs of the milestones, a proof of Lemma 3 by any method, and reusable lemmas on exponential weights (normalization, closed form, monotonicity of weights along a constant adversary). The paper's proofs are in its App. A and App. C.

Selected references

• J.-Y. Audibert, S. Bubeck, G. Lugosi, Regret in Online Combinatorial Optimization, Math. Oper. Res. 39(1), 2014; arXiv:1204.4710v2. https://arxiv.org/abs/1204.4710
• W. M. Koolen, M. K. Warmuth, J. Kivinen, Hedging Structured Concepts, Proceedings of COLT 2010 (reference [26] of the paper above).
• Y. Freund, R. E. Schapire, A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting, J. Comput. Syst. Sci. 55(1), 1997. https://doi.org/10.1006/jcss.1997.1504
• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Found. Trends Mach. Learn. 5(1), 2012; arXiv:1204.5721. https://arxiv.org/abs/1204.5721