All missions

Motivation

A seller who does not know how demand responds to price must learn it from sales while it sells. Each price it charges earns revenue, and each price also reveals something about demand. Choosing prices that serve both purposes is the learn-and-earn problem of dynamic pricing. Its standard yardstick is regret: the expected revenue lost, over a horizon of $T$ periods, relative to a seller who knew the demand curve from the start.

Keskin and Zeevi (Operations Research 62(5), 2014) study linear demand with unknown intercept and slope. They show that no policy can have worst-case regret of order below $\sqrt T$, and that simple least-squares-based policies attain $\sqrt T \log T$. They then consider a variant that is common in practice. A seller has charged one incumbent price $\hat p$ for a long time and knows the expected demand $\hat D$ at that price. Only the slope of the demand curve remains uncertain, and the incumbent price is the only price that carries no information about it. In this variant the achievable regret drops to order $\log T$. This mission formalizes the lower bound: no policy does better than $\log T$ (Theorem 3 of the paper). Earlier single-parameter models (Broder and Rusmevichientong, Operations Research 2012) assumed the intercept is known exactly, so that the only uninformative price is zero. The incumbent price model instead has a strictly positive uninformative price, and a seller that charges it stops learning.

Setting

Prices are chosen from an interval $[l,u]$ with $0 \le l < u$. The seller knows an incumbent price $\hat p \in [l,u]$ and an incumbent demand $\hat D \ne 0$. The unknown slope $\beta$ lies in a compact interval $\mathfrak B = [b_{\min}, b_{\max}]$ with $b_{\min} < b_{\max} < 0$. The expected demand at $\hat p$ is $\hat D$, which is the incumbent price relation $\hat D = \alpha + \beta \hat p$. Write the price in period $t$ as $p_t = \hat p + x_t$, where $x_t$ is the price deviation. Demand in period $t$ is

$$D_t = \hat D + \beta x_t + \epsilon_t, \qquad t = 1, 2, \dots,$$

where the demand shocks $\epsilon_1, \epsilon_2, \dots$ are i.i.d. $\mathcal N(0,\sigma^2)$ with $\sigma > 0$.

The single-period revenue of a deviation $x$ is $r_\beta(x) = (\hat p + x)(\hat D + \beta x)$. It is maximized at the optimal deviation

$$\psi(\beta) = -\frac{\hat p}{2} - \frac{\hat D}{2\beta}.$$

The model assumes that the optimal price $\hat p + \psi(\beta)$ lies strictly inside $(l,u)$ for every $\beta \in \mathfrak B$.

A pricing policy $\pi$ is a sequence of measurable functions. The first price $\pi_1$ is a constant, and the price in period $t+1$ is a function $\pi_{t+1}(H_t)$ of the observed history $H_t = ((D_1,p_1),\dots,(D_t,p_t))$, with values in $[l,u]$. A policy never observes $\beta$ or the shocks. The regret of $\pi$ under slope $\beta$ over $T$ periods is

$$\Delta^\pi_\beta(T) = T\,r_\beta(\psi(\beta)) - \mathbb E^\pi_\beta \sum_{t=1}^T r_\beta(x_t).$$

The worst-case regret excludes the slopes at which the incumbent price is itself optimal:

$$\Delta^\pi(T) = \sup\{\Delta^\pi_\beta(T) : b_{\min} \le \beta \le b_{\max},\ \psi(\beta) \ne 0\}.$$

The accumulated information is measured by $\hat J_t = \sum_{s=1}^t x_s^2$; the Fisher information of the history about $\beta$ is $\sigma^{-2}\mathbb E^\pi_\beta[\hat J_t]$.

In Lean these objects are Model (with fields l u pHat DHat bMin bMax σ and the standing assumptions), Policy, pricePath, dev, regret, worstRegret, sqErr and expInfo, all in the namespace KeskinZeevi.IncumbentLowerBound; the i.i.d. $\mathcal N(0,\sigma^2)$ shocks are the shared definition RobustBooking.Shared.GaussianNoise.

Formalization targets

Goal: Theorem 3 (p. 1149)

There is a finite positive constant $c$, depending only on the model, such that for every pricing policy $\pi$ and every horizon $T \ge 3$,

$$\Delta^\pi(T) \;\ge\; c \log T.$$

The constant is not fixed; the statement asserts only the logarithmic rate, uniformly over policies.

Milestones

1. Lemma 4 (p. 1149). There are finite positive constants $c_0, c_1$ such that for every policy $\pi$ and horizon $T$,

$$\sup_{\beta\in\mathfrak B,\,\psi(\beta)\ne0} \sum_{t=2}^T \mathbb E^\pi_\beta (x_t-\psi(\beta))^2 \;\ge\; \sum_{t=2}^T \frac{c_0}{c_1 + \sup_{\beta\in\mathfrak B}\mathbb E^\pi_\beta[\hat J_{t-1}]}.$$

2. The same bound with the information replaced by its trivial maximum (§A.3, p. 1158): the right side with $(u-l)^2(t-1)$ in place of $\sup_\beta \mathbb E^\pi_\beta[\hat J_{t-1}]$.
3. The regret identity and its lower bound (§A.3, p. 1159): with the constants of Lemma 4,

$$\Delta^\pi(T) = \sup_{\beta\in\mathfrak B,\,\psi(\beta)\ne0} \Big\{-\beta\sum_{t=1}^T \mathbb E^\pi_\beta (x_t - \psi(\beta))^2\Big\} \;\ge\; |b_{\max}| \sum_{t=2}^T \frac{c_0}{c_1 + (u-l)^2(t-1)}.$$

4. The harmonic bound (§A.3, p. 1159): there are $K_1, K_2 > 0$ with $\Delta^\pi(T) \ge K_1\sum_{t=1}^{T-1} 1/(K_2+t) \ge \frac{K_1}{1+K_2}\sum_{t=1}^{T-1} 1/t$.

Significance

Theorem 3 identifies $\log T$ as the minimal asymptotic loss rate of the incumbent price problem. Together with the matching upper bound (Theorem 4 of the paper, a separate mission in this series), it separates two regimes. When both demand parameters are unknown the rate is $\sqrt T$. When the demand at one strictly positive price is known it is $\log T$, even though an uninformative price exists and a myopic seller can stop learning. The lower bound is what makes "asymptotically optimal" meaningful for the semi-myopic policies the paper proposes. The paper places it next to the logarithmic lower bound of Broder and Rusmevichientong (2012, Theorem 4.5), whose binary-response model has no uninformative action; the incumbent price model adds one.

The result is proved on paper and, as far as the platform's corpus shows, not formalized anywhere. A formal development would produce a reusable model of history-dependent policies driven by i.i.d. noise, a scalar Van Trees (Bayesian Cramér–Rao) inequality for adaptively collected Gaussian data, and a template for minimax regret lower bounds that quantify over all policies. The companion missions of this series (the $\sqrt T$ lower bound, and the two upper bounds) share the model.

Difficulty

The bound quantifies over every non-anticipating policy, including policies that adapt their exploration to the observed history. A frequentist Cramér–Rao bound does not apply, because a policy's prices are neither unbiased estimators nor fixed designs, and the information $\mathbb E^\pi_\beta[\hat J_t]$ depends on the unknown $\beta$ through the policy's own choices. A two-point argument that compares two slopes controls the error at one pair of parameters. It does not by itself give the per-period trade-off between information and pricing error that must be summed over $t$. The set over which the worst case is taken also excludes the slope at which the incumbent price is optimal. The lower bound must therefore come from slopes where the seller is forced to deviate from $\hat p$, and every deviation earns information but also costs revenue.

Formalization scope

The model is a Lean structure carrying all standing assumptions as fields: $0 \le l < u$, $\hat p\in[l,u]$, $\hat D\ne 0$, $b_{\min}<b_{\max}<0$, $\sigma>0$, and interiority of the optimal price $\hat p/2-\hat D/(2\beta)$ for every $\beta\in\mathfrak B$. Two of these are corrections that make implicit hypotheses explicit. The first is $\hat p\in[l,u]$: p. 1148 calls $\hat p$ the uninformative price "within the feasible price domain", and the proof uses $\hat J_s\le(u-l)^2s$. The second is $\hat D\ne0$. With $\hat D = 0$ the optimal price $\hat p/2$ is known and the theorem is false. The paper's reading is $\hat D>0$, and $\hat D\neq 0$ is the weaker hypothesis the proof needs.

The optimal deviation $\psi$ is the closed form, which equals the maximizer (21) under the interiority assumption. Policies are deterministic. The rule of period $t+1$ is a Borel measurable map from histories encoded as Fin t → ℝ × ℝ into $[l,u]$. The price process is defined by recursion from the shocks on an arbitrary probability space $(\Omega,P)$, which realizes the law of the history under $\pi$ and $\beta$. Lean periods start at $0$ (Lean period $t$ is the paper's period $t+1$). Expectations are Bochner integrals of bounded measurable functions. The worst-case regret is a real supremum over the subtype $\{\beta\in\mathfrak B:\psi(\beta)\ne0\}$, which is nonempty and on which the regrets are uniformly bounded. The constant $c$ is quantified before the probability space, the noise, the policy and the horizon. A statement whose constant may depend on $\pi$ or $T$, whose supremum is over an empty or unbounded index set, or whose policies can read $\beta$ would be trivially true or false, and none of these is the theorem stated here.

A complete development needs the scalar Van Trees inequality, Fisher information of the Gaussian location-scale history density, measurability of the price process, and harmonic-sum estimates (Real.log against partial sums of $1/t$), on top of Mathlib's gaussianReal, iIndepFun and Bochner integration. The Van Trees inequality and the policy/price-process model are reusable beyond this mission. Proofs of the milestones individually, and a general Van Trees inequality in Mathlib style, are welcome.

Selected references

• N. Bora Keskin and Assaf 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
• Josef Broder and Paat Rusmevichientong, Dynamic Pricing Under a General Parametric Choice Model, Operations Research 60(4):965–980, 2012. https://doi.org/10.1287/opre.1120.1057
• Alexander Goldenshluger and Assaf Zeevi, Woodroofe's One-Armed Bandit Problem Revisited, Annals of Applied Probability 19(4):1603–1633, 2009. https://doi.org/10.1214/08-AAP589
• Richard D. Gill and Boris Y. Levit, Applications of the van Trees Inequality: A Bayesian Cramér–Rao Bound, Bernoulli 1(1–2):59–79, 1995. https://doi.org/10.2307/3318681

Motivation

Airlines, hotels and railways sell a fixed stock of capacity on several resources at once: a passenger flying from Boston to Los Angeles through Chicago uses a seat on two flight legs. Network revenue management decides which requests to accept, and the standard control is a bid price per leg: accept an itinerary if its fare exceeds the sum of the bid prices of the legs it uses. A good bid price is the marginal expected value of one more unit of capacity.

Talluri and van Ryzin (Transportation Science 33(2), 1999) proposed the randomized linear programming (RLP) method: simulate demand scenarios, solve a linear program with perfect knowledge of each scenario's demand, and average the optimal dual prices. Their main result (a companion mission) says the average is an unbiased estimate of the gradient of expected perfect-information revenue when that gradient exists. This mission is about their §3, the case where it does not: when the LP is degenerate with positive probability, the expected revenue has kinks, averaged dual prices estimate only a supergradient, and the right object is the directional derivative. Proposition 2 of the paper computes it as the expectation of an auxiliary LP value, which again gives an unbiased simulation estimator, now one direction at a time.

Setting

There are $m$ legs and $n$ itineraries. The incidence matrix $A \in \{0,1\}^{m \times n}$ has $a_{ij} = 1$ if itinerary $j$ uses leg $i$; every column $A^j$ is nonzero. Fares are $r \in \mathbb{R}^n$, $r \ge 0$; capacities are $x \in \mathbb{R}^m$. For a demand vector $Y \in \mathbb{R}^n$, $Y \ge 0$, the perfect-information LP value is

$$v(x, Y) = \max\{r^\top y : Ay \le x,\ 0 \le y \le Y\},$$

the best revenue obtainable if the demand $Y$ were known in advance. With $Y$ a random vector on a probability space $(\Omega, P)$, the perfect-information approximation of the value function is $J^{PI}(x) = \mathbb{E}\, v(x, Y)$.

The Lagrangian of the capacity constraints is

$$L(x, \mu) = \sum_{j=1}^n Y^j (r^j - \mu^\top A^j)^+ + \mu^\top x, \qquad \mu \ge 0,$$

and an optimal vector of dual prices is a minimizer of $L(x, \cdot)$ over $\mu \ge 0$. Since $z \mapsto v(z, Y)$ is concave on $z \ge 0$, its superdifferential at $x$ is

$$\partial v(x, Y) = \{\mu : v(z, Y) \le v(x, Y) + \mu^\top (z - x) \text{ for all } z \ge 0\}$$

(the paper calls its elements subgradients). For a direction $d \in \mathbb{R}^m$ let

$$u(x, Y; d) = \min\{d^\top \mu : \mu \text{ an optimal vector of dual prices}\},$$

and let $D(x; d) = \lim_{h \downarrow 0} \frac1h [J^{PI}(x + hd) - J^{PI}(x)]$ be the one-sided directional derivative of $J^{PI}$. In Lean these are piValue, JPI, lagr, IsDualOpt, superdiff and u in the namespace RLPBidPrice.Directional.

Formalization targets

Goal: Proposition 2 (corrected)

For $x$ with every $x^i > 0$, $Y$ measurable with $Y \ge 0$ almost surely, and every direction $d$,

$$D(x; d) = \lim_{h \downarrow 0} \frac1h\big[J^{PI}(x + hd) - J^{PI}(x)\big] = \mathbb{E}\, u(x, Y; d).$$

No condition on the distribution of $Y$ is imposed, which is the point: this is the nondifferentiable case.

Milestones

1. Lemma 2. $|v(x + h e^i, Y) - v(x, Y)| \le h \max_j r^j$ for $x, Y \ge 0$, $h \ge 0$.
2. §3.1, pointwise. An optimal dual price vector $\mu$ satisfies $v(z, Y) \le v(x, Y) + \mu^\top(z - x)$ for all $z \ge 0$.
3. §3.1, in expectation. For a measurable selection $\mu(\omega)$ of optimal dual prices and $x > 0$, $J^{PI}(z) \le J^{PI}(x) + (\mathbb{E}\mu)^\top(z - x)$.
4. Superdifferential. For $x > 0$, $\partial v(x, Y)$ equals the set of optimal dual prices and lies in $[0, \max_j r^j]^m$.
5. Pointwise directional derivative. For $x > 0$, $\lim_{h \downarrow 0} \frac1h[v(x + hd, Y) - v(x, Y)] = \inf\{d^\top\mu : \mu \in \partial v(x, Y)\}$.
6. Proposition 1. For a fixed measurable dual selection $f$ and pairwise independent samples $Y_i$ distributed as $Y$, $\frac1N\sum_{i \le N} f(Y_i)$ converges almost surely to a supergradient of $J^{PI}$ at $x$.

Significance

The result. In the differentiable case the RLP bid prices are the averaged dual prices. When degeneracy has positive probability, which happens for discrete demand and for many network structures, Proposition 2 is what remains true: the marginal value of capacity in any direction, in particular in the direction $A^j$ of an itinerary (the displacement cost of accepting it), is the expectation of a scenario-wise LP quantity. Averaging $u(x, Y_i; d)$ over simulated scenarios is an unbiased estimator of it. Milestone 3 and Proposition 1 say what the plain RLP average estimates in this case (a supergradient), and why the choice of LP algorithm matters for whether it converges at all.

Formalizing it. The paper's argument is a short paragraph; its printed version is not correct as stated (see the scope section), so a machine-checked proof also settles which version holds. The mission produces a formal theory of the parametric LP value $v(x, Y)$ in its right-hand side: concavity, the Lipschitz bound, the identification of its superdifferential with the Lagrangian dual optimal set, and its directional derivatives, together with the interchange of a one-sided limit and an expectation. As far as a search of the platform shows, none of this, and no revenue-management gradient result, is formalized yet; the platform's LP sensitivity theorem is for standard-form LPs with a full-row-rank matrix and does not cover this model.

Difficulty

The pointwise facts are classical convex analysis and LP duality, but they have to be proved for a supremum defined over a polytope, not quoted, and Mathlib has no LP duality theorem in this form. The identification of the superdifferential needs strong duality for the LP with the box $0 \le y \le Y$, and the box is exactly where the paper's own formula (22) goes wrong: the dual variables of $y \le Y$ cannot be dropped.

The step from the pointwise derivative to the expectation is a dominated convergence argument for one-sided difference quotients, which needs a bound uniform in $Y$ and measurability of $\omega \mapsto u(x, Y(\omega); d)$. The obvious route, differentiating under the integral sign as in the differentiable case, is not available: $J^{PI}$ is not differentiable, and a two-sided limit is false. The measurability of $u$ is not given by a formula; it has to come from $u$ being a limit of measurable difference quotients.

Formalization scope

Capacities, demands and fares are real vectors indexed by Fin m and Fin n; $A$ is a real matrix with 0/1 entries and nonzero columns (IsIncidence A); $r \ge 0$. The paper's remaining-time index $k$ is notation only and is dropped. $v$ is a real sSup over the feasible objective values: for $x \ge 0$, $Y \ge 0$ it is the LP maximum, and otherwise it is $0$, so every statement assumes $x \ge 0$ or $x > 0$ and $Y \ge 0$ (almost surely), and the superdifferential is taken over $z \ge 0$ only. Optimal dual prices are defined through the Lagrangian (13)–(14); they are the $\mu$-parts of the optimal solutions of the LP dual. $u$ is a real sInf, which would be $0$ on an empty set; for $x > 0$ the dual optimal set is nonempty and bounded, so $u$ is an attained minimum and the goal is not vacuous. Directional derivatives are one-sided limits (nhdsWithin 0 (Set.Ioi 0)). Expectations are Bochner integrals; no integrability of $Y$ is assumed or needed, since $v$ and $u$ are bounded.

The following corrections to the printed text are part of the statements, each with a counterexample to the printed version:

• Eq. (22) omits the duals of $y \le Y$: with one leg, one itinerary, $r = 1$, $x = 1$, $Y$ uniform on $[0, 2]$, $D(1; 1) = 1/2$, but the printed (22) gives $\mathbb{E}\,u = 3/4$. Here $u$ minimizes over the optimal dual prices of (14).
• The superdifferential formula in the proof of Proposition 2 has the same omission: for $r = 1$, $x = 1$, $Y = 1/2$ the printed set is $\{1/2\}$, the true one $\{0\}$.
• The §3.1 inequality is printed with $\ge$; $v$ is concave, and $r = 1$, $Y = 5$, $x = 1$, $\mu = 1$, $z = 10$ gives $5 \ge 10$. The expectation version also misprints $z - y$ for $z - x$.
• $x > 0$ is implicit: at a zero capacity the dual prices of that leg are unbounded and a direction leaving $x \ge 0$ makes the LP infeasible.
• Proposition 1 is formalized for an algorithm returning a fixed measurable function of the current demand ("initialized with the same data on each run"), with "always exists" read as almost sure convergence.

A statement of the goal with the printed (22), or with $u$ defined over an arbitrary or empty set so that sInf returns $0$, or with a two-sided limit, is ruled out: the first two are false or vacuous for the reasons above, the third is false.

A complete development needs LP duality for $\max\{r^\top y : Ay \le x, 0 \le y \le Y\}$, concavity and the Lipschitz bound of the value function, the directional derivative of a finite concave function on an open set, and dominated convergence (Mathlib's MeasureTheory.tendsto_integral_filter_of_dominated_convergence); Proposition 1 uses ProbabilityTheory.strong_law_ae. The LP duality and parametric value-function results are reusable for any mission about LP-based bid prices or two-stage stochastic programs. Contributions of any milestone separately are welcome.

Selected references

• K. Talluri, G. van Ryzin, A Randomized Linear Programming Method for Computing Network Bid Prices, Transportation Science 33(2):207–216, 1999. https://doi.org/10.1287/trsc.33.2.207
• M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993 (the paper cites p. 218 of this edition; 3rd ed. 2006: https://doi.org/10.1002/0471787779).
• K. Talluri, G. van Ryzin, An Analysis of Bid-Price Controls for Network Revenue Management, Management Science 44(11):1577–1593, 1998. https://doi.org/10.1287/mnsc.44.11.1577

Motivation

Airlines, hotels and railways sell fixed capacity on networks of resources. In network revenue management a request for an itinerary that uses several flight legs is accepted or rejected in real time, and the dominant industrial control is the bid-price control: every leg carries a price, and a request is accepted only if its fare is at least the sum of the bid prices of the legs it uses. A good bid price is the marginal expected value of one more seat on the leg, which is a gradient of an expected-revenue function with respect to capacity.

The classical way to compute bid prices, the deterministic linear program, replaces random demand by its mean and reads off the dual prices of the capacity constraints. It ignores all distributional information and gives a zero bid price to every leg whose mean demand is below capacity. Talluri and van Ryzin (Transp. Sci. 33(2), 1999) studied the randomized linear programming (RLP) method instead: simulate demand vectors $Y_1, \dots, Y_N$, solve one linear program per sample with the realized demand as an upper bound, and average the dual prices. Their Theorem 1 asserts that this average is an unbiased estimator of the gradient of the expected perfect-information revenue. For one leg and one fare class it recovers Littlewood's rule, $\frac{d}{dx}\mathbb{E}\,v(x,Y) = r\,P(Y > x)$ (Littlewood 1972, cited on p. 209 of the paper).

Setting

A network has $m$ legs and $n$ itineraries. The incidence matrix $A \in \{0,1\}^{m\times n}$ has $a_{ij} = 1$ exactly when itinerary $j$ uses leg $i$, and every column $A^j$ is nonzero. Fares are $r = (r^1, \dots, r^n) \ge 0$ and capacities are a real vector $x \ge 0$. Demand to come is a random vector $Y = (Y^1, \dots, Y^n) \ge 0$ on a probability space $(\Omega, P)$.

The perfect-information LP value is

$$v(x, Y) = \max\{\, r^\top y \;:\; Ay \le x,\ 0 \le y \le Y \,\},$$

the revenue obtainable if the demand were known in advance, and the perfect-information approximation of the value function is $J^{PI}(x) = \mathbb{E}\,v(x, Y)$. The Lagrangian dual function of the capacity constraints is

$$L(x, \mu) = \sum_{j=1}^n Y^j\,(r^j - \mu^\top A^j)^+ + \mu^\top x ,$$

and an optimal dual price vector $\mu(x, Y)$ is a minimizer of $L(x, \cdot)$ over $\mu \ge 0$. In Lean these are piValue, JPI, lagr and IsDualOpt in the namespace RLPBidPrice.Unbiased.

Two conditions govern the result. Condition C1′: whenever $x$ lies in the linear span of a set of columns of $[A\ I]$ (columns of $A$ and unit vectors $e^i$), that set spans $\mathbb{R}^m$. Condition 2: every distribution function $t \mapsto P(Y^j \le t)$ is continuous. The components $Y^1, \dots, Y^n$ are also assumed mutually independent.

Formalization targets

Goal: Theorem 1 (corrected)

Under C1′, Condition 2 and independence,

$$\nabla_x \mathbb{E}\,v(x, Y) = \mathbb{E}\,\nabla_x v(x, Y) = \mathbb{E}\,\mu(x, Y).$$

In Lean (theorem1_unbiased_gradient) this is three clauses: $v(\cdot, Y)$ is differentiable at $x$ almost surely; $J^{PI}$ is Fréchet differentiable at $x$ with derivative the expectation of the pathwise derivatives; and for every measurable, almost surely optimal dual selection $\mu$, $J^{PI}$ has gradient $\mathbb{E}\,\mu(x, Y)$ at $x$.

Milestones

1. Lemma 1 (Glasserman): a random function that is Lipschitz in $\theta$ with a constant $K$ and almost surely differentiable at $\theta$ can be differentiated under the expectation.
2. Lemma 2: $|v(x + h e^i, Y) - v(x, Y)| \le h\,\bar r$ with $\bar r = \max_j r^j$.
3. Differentiability and uniqueness (§2.1, p. 210): for $x > 0$, $v(\cdot, Y)$ is differentiable at $x$ if and only if the optimal dual price vector is unique.
4. Strong duality (§2.1, p. 211): an optimal $\mu_*$ exists, $v(x, Y) = L(x, \mu_*)$, $v(z, Y) \le v(x, Y) + \mu_*^\top(z - x)$ for all $z \ge 0$, and a unique $\mu_*$ is the gradient at $x > 0$.
5. Lemma 3 (corrected): under C1′, a feasible direction $d$ from $\mu_*$ with $d^\top A^j = 0$ on the index sets $E_0 \cup E_1$ of Eqs. (16)–(17) and $d^\top x = 0$ is zero.
6. Lemma 4 (corrected): under C1′, Condition 2 and independence, $\nabla_x v(x, Y)$ exists with probability one.

Significance

The theorem justifies a widely used method: it says that the simple procedure of averaging simulated LP dual prices targets the gradient of a well-defined expected-revenue function, and by the strong law of large numbers the average is also consistent. It separates the RLP method from the deterministic LP, whose dual prices are gradients of a different function, and it isolates exactly when that justification fails (degenerate LPs with positive probability, discussed in §2.2 of the paper and treated by directional derivatives in its §3).

The printed statement is false, and the formalization records that. Condition 1 of the paper looks only at the columns of $A$ and ignores the slack columns of $Ay \le x$; the paper's Condition 2 is marginal and does not rule out dependent demands whose sum hits capacity. The corrected statement, with C1′ and independence, is the one this mission targets. No machine-checked version of this result, or of LP sensitivity analysis under random right-hand sides of this kind, is known to exist; formalizing it gives a checked statement of the hypotheses under which the RLP estimator is unbiased.

Difficulty

The pathwise facts are LP duality; the delicate step is the almost-sure uniqueness of the dual prices. Degeneracy of an LP is a condition on finitely many bases, but the set of dual optima depends on $Y$, and the natural argument that fixes a direction $d$ and shows that $d^\top(x - \sum_{j} Y^j A^j) = 0$ has probability zero does not work as written: the direction depends on $Y$, and a direction that improves the Lagrangian may leave the orthant $\mu \ge 0$. This is precisely where the printed Condition 1 fails. A second difficulty is the passage from almost-sure differentiability of $v(\cdot, Y)$ to a full Fréchet derivative of $J^{PI}$ on $\mathbb{R}^m$, with the measurability of the random derivative and of the dual selection.

Formalization scope

Legs and itineraries are Fin m and Fin n; $A$ is a real matrix with entries in $\{0,1\}$ and nonzero columns; capacities are real vectors. The paper's remaining-time index $k$ is notation only and is dropped. $v$ is a real sSup over feasible objective values; since the feasible set is empty when $x$ or $Y$ has a negative entry (the value is then $0$), every statement assumes $x \ge 0$ and $Y \ge 0$ almost surely, and derivatives are taken where $x$ is interior (C1′ forces $x^i \neq 0$). Optimal dual prices are minimizers of the Lagrangian (13) over $\mu \ge 0$, which are the $\mu$-parts of the optimal solutions of the LP dual of (6)–(8). Gradients are Fréchet derivatives on Fin m → ℝ, encoded by the linear functional $h \mapsto \sum_i g^i h^i$ (gradCLM g). Condition 2 is continuity of $t \mapsto P(Y^j \le t)$; independence is iIndepFun. $Y$ is measurable; no integrability of $Y$ is assumed, since $0 \le v(x, Y) \le \bar r\sum_i x^i$.

Every correction is labelled in the statements. C1 → C1′: with $A$ having rows $(0,1,1),(1,1,0),(1,0,1)$, $r = (100,1,1)$, $x = (1,1,1)$ and $Y^j$ i.i.d. uniform on $[0,2]$, Conditions 1 and 2 hold but $\mathbb{E}\,v(\cdot, Y)$ has one-sided slopes of about $0.74$ and $50.5$ in the second coordinate at $x$. Independence added: with one leg, $x = 1$, fares $(2,1)$ and $Y^2 = 1 - Y^1$, $Y^1$ uniform on $[0,1]$, the LP is degenerate almost surely. Implicit hypotheses made explicit: $x \ge 0$, $Y \ge 0$, $r \ge 0$ (Lemma 2's bound needs $\bar r \ge 0$), nonzero 0/1 columns.

The goal is not trivialized by a selection: it states the selection-free identity $\nabla_x \mathbb{E}\,v = \mathbb{E}\,\nabla_x v$, and the dual-price form quantifies only over measurable selections that are optimal almost surely; it assumes neither almost-sure differentiability, nor almost-sure uniqueness of the dual, nor a joint density, nor nondegeneracy.

A complete development needs LP duality for bounded-variable LPs in Lagrangian form, concave polyhedral functions and their superdifferentials, a finite enumeration of bases of $[A\ I]$, and differentiation under the integral sign for Lipschitz integrands (Mathlib has hasFDerivAt_integral_of_dominated_loc_of_lip). The LP duality and sensitivity results are reusable for other revenue-management and stochastic-programming missions. Contributions of any milestone, of the counterexamples as formal statements, and of alternative proofs are welcome.

Selected references

• K. Talluri, G. van Ryzin, A Randomized Linear Programming Method for Computing Network Bid Prices, Transportation Science 33(2):207–216, 1999. https://doi.org/10.1287/trsc.33.2.207
• P. Glasserman, Perturbation Analysis of Production Networks, in D. Yao (ed.), Stochastic Modeling and Analysis of Manufacturing Systems, Springer-Verlag, Berlin, 1994 (source of Lemma 1; as cited in the paper).
• K. Littlewood, Forecasting and Control of Passengers, 12th AGIFORS Symposium Proceedings, 1972 (as cited in the paper).
• M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, John Wiley, New York, 1993, Chapter 6 (Lagrangian duality; as cited in the paper).

Motivation

Airlines sell the seats of one flight leg in several fare classes over a booking horizon of weeks. Each time a request arrives, the booking agent must decide whether to sell a seat now at the requested fare or keep it for a later, possibly higher-paying, customer. Real reservations are also cancelled, and some ticket holders fail to show up at departure, so airlines deliberately overbook and pay a penalty when more passengers show up than the airplane can carry. The question this mission formalizes is what an optimal accept/reject rule looks like when all three effects (multiple fares, cancellations, no-shows) are present.

For the model without cancellations and no-shows, Lee and Hersh (Transp. Sci. 27(3), 1993) showed that the optimal rule is given by booking limits: in each period and for each fare class there is a threshold on the number of seats sold, and a request is accepted exactly when the current bookings are below it. Subramanian, Stidham and Lautenbacher (Transp. Sci. 33(2), 1999) extend the model to state-dependent cancellations and binomial no-shows with a convex overbooking penalty. Their §1 shows that booking limits, now depending on both the stage and the fare class, are still optimal. The structural step behind this is the concavity of the value function, in the style of Lippman and Stidham's analysis of admission control to a queue (Oper. Res. 25(2), 1977).

Setting

There are $m$ fare classes and $N$ stages $n = N, N-1, \dots, 0$, counting the periods remaining: stage $N$ opens reservations, stage $0$ is departure. The state $x \in \{0,1,2,\dots\}$ is the number of seats reserved. At each stage $n \ge 1$ exactly one event happens:

• a request in fare class $i$, with probability $p_{in} \ge 0$;
• a cancellation, with probability $q_n(x)$, which is non-negative, nondecreasing and concave in $x$, with $q_n(0) = 0$;
• nothing, with probability $p_{0n}(x) = 1 - \sum_i p_{in} - q_n(x)$ (Eq. (1)).

Accepting a class-$i$ request at stage $n$ earns $r_{in} \ge 0$. At departure each reservation holder independently shows up with probability $1 - \beta$ ($0 \le \beta \le 1$), so the number who show up is $Y(x) \sim \mathrm{Bin}(x, 1-\beta)$. If $Y(x) = y$, an overbooking penalty $\pi(y)$ is paid. Here $\pi$ is non-negative, convex and nondecreasing on $y \ge 0$, and $\pi(y) = 0$ for $y \le C$, the capacity. Starting empty and accepting at most one request per stage, the states reachable at stage $n$ are $0 \le x \le N - n$, and $p_{0n}(x) \ge 0$ is assumed on that range.

The value functions $U_n$ are defined by the recursion (2)–(3):

$$U_0(x) = \mathrm{E}\big[-\pi(Y(x))\big],$$ $$U_n(x) = \sum_{i=1}^m p_{in}\max\{r_{in} + U_{n-1}(x+1),\,U_{n-1}(x)\} + q_n(x)\,U_{n-1}(x-1) + p_{0n}(x)\,U_{n-1}(x).$$

The first branch of each maximum is "accept", the second "reject". The booking limit of class $i$ at stage $n$ is Eq. (7):

$$b_{in} = \min\{x : U_{n-1}(x) - U_{n-1}(x+1) > r_{in}\},$$

with $b_{in} = \infty$ when there is no such $x$. The difference $U_{n-1}(x) - U_{n-1}(x+1)$ is the opportunity cost of one more booking. In Lean all of this is AirlineYieldMgmt.BookingLimits.Model with Model.U, Model.p0, Model.Standing and Model.bookingLimit.

Formalization targets

Goal: booking limits are optimal (§1, Eq. (7), p. 151)

For every stage $1 \le n \le N$, fare class $i$ and reachable state $0 \le x \le N - n$,

$$r_{in} + U_{n-1}(x+1) \;\ge\; U_{n-1}(x) \iff x < b_{in}.$$

The optimal rule accepts a class-$i$ request exactly while fewer than $b_{in}$ seats are booked.

Milestones

1. Lemma 1 (p. 151). If $f$ is nondecreasing and convex on $y \ge 0$ and $0 < \gamma < 1$, then $h(x) = \mathrm{E} f(\mathrm{Bin}(x,\gamma))$ is nondecreasing and convex in $x \in \{0,1,\dots\}$.
2. Terminal value (p. 151). $U_0$ is concave and nonincreasing.
3. All stages (p. 151). For every $0 \le n \le N$, $U_n$ is nonincreasing and concave on $\{0,\dots,N-n\}$, so $U_n(x) - U_n(x+1)$ is nondecreasing in $x = 0,\dots,N-n-1$.

Significance

The result. Booking limits are how single-leg seat inventory is controlled in practice. The theorem says this simple class of rules loses nothing, even with cancellations whose rate grows with the number of bookings and with random no-shows at departure. The limits depend on the stage, and they need not be nested across classes (Remark 3 of the paper). The same concavity property identifies $U_n(x) - U_n(x+1)$ as the optimal bid price for the leg. The companion mission (II, equivalent charging) reduces a model with class-dependent refunds to this one-dimensional recursion, so a formal proof of the present goal is the input needed to carry booking-limit optimality over to that model.

Formalizing it. The paper proves neither the concavity induction nor Lemma 1. It cites Lippman and Stidham (1977, Theorem 1) for the first and Shaked and Shanthikumar (1994, Example 6.A.2) for the second. The authors note that the cited induction carries over to their recursion (p. 151), but neither source states the result for exactly this recursion, with its state-dependent cancellation term and range-restricted probabilities. A machine-checked proof would therefore supply an argument the paper only points to, not just its bookkeeping. To our knowledge none of these statements has a machine-checked proof.

Difficulty

The goal follows quickly once milestone 3 is available. The work is in milestone 3. The obvious induction pushes concavity through each term of the recursion. It fails at the cancellation term $q_n(x)\,U_{n-1}(x-1)$: a product of a concave nondecreasing function and a concave nonincreasing one is not concave in general, so the term is not concave by itself. The null-event term $p_{0n}(x)\,U_{n-1}(x)$ has the same problem, because its coefficient depends on the state. Only the combination of the two terms, together with $\sum_i p_{in} + q_n(x) \le 1$ on the reachable range, keeps the result concave. That constraint holds only on the range, not for every $x$: in the linear case $q_n(x) = q_n x$ it fails for large $x$. This interaction between the range and the induction has to be handled with care. Lemma 1 is a separate, self-contained piece of discrete probability about binomial sums.

Formalization scope

• Fare classes are Fin m; the paper's class $i$ is i.val + 1. Stages and states are ℕ; probabilities, fares, $\beta$, $\pi$ and values are ℝ.
• Model.U is defined by structural recursion on the stage, for every $x \in \mathbb N$. Every theorem restricts its hypotheses and conclusions to the paper's range $0 \le x \le N - n$.
• $x - 1$ is natural-number subtraction. At $x = 0$ it is multiplied by $q_n(0) = 0$, a convention the page leaves implicit (a cancellation needs a reservation).
• The null-event probability is defined by Eq. (1), and its non-negativity is assumed only for $1 \le n \le N$, $0 \le x \le N-n$. This keeps the paper's linear-cancellation case inside the model.
• Concavity, convexity and monotonicity of functions on $\mathbb N$ are discrete (differences). $\pi$ is a real function, convex and nondecreasing on $[0,\infty)$ as on the page.
• Binomial expectations are finite sums $\sum_{k=0}^x \binom xk \gamma^k(1-\gamma)^{x-k} f(k)$. The milestone for $U_0$ allows $0 \le \beta \le 1$.
• The minimum in (7) ranges over the reachable states and lives in WithTop ℕ, with ⊤ meaning $b_{in} = \infty$.
• "An optimal policy accepts" means the accept branch attains the maximum in (2). No dynamic-programming optimality principle, policy space or claim about expected revenue is stated.
• Ruling out the trivializing formalization: $b_{in}$ is defined by Eq. (7) as a minimum of a strict-inequality set. It is not defined as the number of states where acceptance is optimal, a definition under which the goal would hold by construction and lose its content (that the accepted states form an initial segment).
• A proof needs finite binomial sums and discrete concavity arguments; Mathlib covers both. The discrete-concavity and binomial lemmas would carry over to other admission-control and inventory models. Proofs of any milestone, and of the goal assuming milestone 3, are welcome separately.

Selected references

• J. Subramanian, S. Stidham Jr., C. J. Lautenbacher, Airline Yield Management with Overbooking, Cancellations, and No-Shows, Transportation Science 33(2), 147–167, 1999. https://doi.org/10.1287/trsc.33.2.147
• S. A. Lippman, S. Stidham Jr., Individual versus Social Optimization in Exponential Congestion Systems, Operations Research 25(2), 233–247, 1977. https://doi.org/10.1287/opre.25.2.233
• T. C. Lee, M. Hersh, A Model for Dynamic Airline Seat Inventory Control with Multiple Seat Bookings, Transportation Science 27(3), 252–265, 1993. https://doi.org/10.1287/trsc.27.3.252
• M. Shaked, J. G. Shanthikumar, Stochastic Orders and Their Applications, Academic Press, San Diego, 1994 (Example 6.A.2).

Motivation

Consumers judge a price against a reference price, an internal standard formed from the prices they have seen before. A price below the reference is perceived as a gain and stimulates demand; a price above it is perceived as a loss and depresses demand. Prospect theory (Kahneman and Tversky 1979) adds that losses loom larger than gains of the same size: this is loss aversion. A firm that sets prices over many periods therefore faces a dynamic trade-off, because today's price moves tomorrow's reference price and with it tomorrow's demand.

Popescu and Wu (Operations Research 55(3), 2007) analyze this problem for general nonlinear demand. Earlier work of Kopalle, Rao and Assunção (1996) and of Fibich, Gavious and Lowengart (2003) had treated linear or piecewise-linear reference effects with explicit solutions. Popescu and Wu replace explicit solutions by structural arguments (supermodularity, monotone policies, comparison of value functions), which is what makes the results reusable for any demand model satisfying their assumptions. Their headline result for loss-averse consumers is that the long-run prices form a whole interval rather than a single point, and that optimal prices outside the interval move monotonically to its nearer endpoint.

Setting

A monopolist chooses a price $p_t$ from $P=[0,\bar p]$, $\bar p>0$, in each period $t=0,1,2,\dots$. The reference price follows exponential smoothing,

$$r_{t+1}=\alpha r_t+(1-\alpha)p_t,\qquad \alpha\in[0,1),$$

from a given initial reference price $r_0$. Demand is $D(p,r)=d(p)+R(r-p,r)$, where $d(p)=D(p,p)$ is the base demand and $R(x,r)$ is the reference effect of the perceived gain $x=r-p$, so that $R(0,r)=0$. The per-period profit (zero unit cost) is $\Pi(p,r)=p\,D(p,r)$, the base profit is $\pi(p)=p\,d(p)$, and $\lambda(r)$ denotes the slope of $R(\cdot,r)$ at $x=0$.

For a discount factor $\beta\in(0,1)$, the value function is the supremum of discounted profit over all price sequences in $P$:

$$V(r_0)=\sup_{(p_t)\in P^{\mathbb N}}\sum_{t\ge 0}\beta^t\,\Pi(p_t,r_t).$$

The Bellman objective is $W(p,r)=\Pi(p,r)+\beta V(\alpha r+(1-\alpha)p)$. The optimal pricing policy $p^*(r)$ is the largest maximizer of $W(\cdot,r)$ over $P$, and $q^*(r)=\alpha r+(1-\alpha)p^*(r)$ is the next reference price. The state path is $r^*_{t+1}=q^*(r^*_t)$ and the price path is $p^*_t=p^*(r^*_t)$. A steady state is a price $p^{**}\in P$ with $p^*(p^{**})=p^{**}$.

The standing Assumption 1 requires $D$ to be nonnegative, bounded and continuous, decreasing in $p$, increasing in $r$, and $R$ increasing in $x$. For a smooth (loss-neutral) $R$, Assumptions 2–3 require $R$ to be twice differentiable, $\pi$ to be nonmonotonic and concave, $\pi'(r)-r\lambda(r)$ to be strictly decreasing, and the reference profit $\Pi^R(p,r)=pR(r-p,r)$ to be concave in $p$ and supermodular.

Under loss aversion the reference effect is kinked: $R_K(x,r)=R_G(x,r)$ for gains $x\ge 0$ and $R_K(x,r)=R_L(x,r)$ for losses $x<0$. Assumption 4 makes $R_G$ and $R_L$ twice differentiable and increasing in $x$, makes $R_G-R_L$ single crossing, and imposes $\lambda_L(r)>\lambda_G(r)$. Assumption 5 requires the gain and loss profits to satisfy Assumption 3. The problems $(K)$, $(P_L)$ and $(P_G)$ are the pricing problem with reference effect $R_K$, $R_L$ and $R_G$, respectively, and $(P_\theta)$ uses $R_\theta=\theta R_G+(1-\theta)R_L$ for $\theta\in[0,1]$.

Formalization targets

Goal: Theorem 4 of the paper

There exist prices $p^{**}_L\le p^{**}_G$ such that $p^{**}_L$ is the unique steady state of $(P_L)$, $p^{**}_G$ is the unique steady state of $(P_G)$, and

$$\{\,r:\ r \text{ is a steady state of }(K)\,\}=[p^{**}_L,p^{**}_G].$$

Moreover, the following hold:

• from $r_0\in[p^{**}_L,p^{**}_G]$, the optimal price path of $(K)$ is constant, $p^*_t=r_0$;
• from $r_0<p^{**}_L$, the state path of $(K)$ is nondecreasing and converges to $p^{**}_L$, and so does the price path;
• from $r_0>p^{**}_G$, the state path is nonincreasing and converges to $p^{**}_G$, and so does the price path.

Milestones

In attack order, the milestones are:

• Remark 2 ($V$ increasing);
• Lemma 2 ($q^*$ increasing);
• Theorem 1, first sentence (a steady state is the unique solution of $\pi'(p)/(1-\beta)=p\lambda(p)/(1-\alpha\beta)$);
• Theorem 2 (a unique steady state exists and attracts every optimal path, with monotone state paths);
• Remark 3 (a steeper reference effect gives a lower steady state);
• Lemma 4 ($(P_\theta)$ satisfies Assumptions 1–3, $V_\theta\ge V_K$, and steady states of $(P_\theta)$ are steady states of $(K)$);
• the §5.2 statement that the steady states $p^{**}_\theta$ span $[p^{**}_L,p^{**}_G]$;
• the §A.11 identity $V_K(r_0)=V_L(r_0)$ for $r_0<p^{**}_L$.

Significance

The theorem separates loss-averse markets from loss-neutral ones. With a smooth reference effect, Theorem 2 gives one long-run price. Under loss aversion, every price in $[p^{**}_L,p^{**}_G]$ is self-sustaining: a firm that starts there gains nothing by moving. Prices therefore exhibit stickiness, an interval of rigid prices, which is the dynamic counterpart of the kink in the reference effect. The paper uses this result to derive price monotonicity under loss aversion (its Proposition 4) and the behavior of myopic firms (its Proposition 5).

The result is proved in the paper; nothing here is open. What the mission adds is a machine-checked proof, and that proof has to supply steps the paper passes over quickly. Among them are the existence of steady states in Theorem 2 (the paper argues it in two sentences) and the largest-maximizer bookkeeping when steady states are transferred from $(P_\theta)$ to $(K)$.

Difficulty

The bulk of the work sits in the infinite-horizon dynamic program itself. The value function is a supremum over infinite price sequences. Before any comparative statics can be done, one must show that it satisfies the Bellman equation (2), that it is continuous, and that the argmax is nonempty, so that the largest maximizer is well defined and actually maximizes. The monotonicity of $q^*$ does not follow from supermodularity of $\Pi$ alone, because the policy maximizes current profit plus a continuation value evaluated at a state that itself depends on the price.

For the kinked problem, $R_K$ is not differentiable at $x=0$, so the first-order analysis behind Theorem 1 does not apply to $(K)$. A first-order condition with one-sided derivatives is the natural first idea. It yields inequalities that every steady state must satisfy, but it establishes neither that steady states exist nor that the whole interval consists of steady states. The set equality also depends on the largest-maximizer convention, since a price that is merely a maximizer of the Bellman objective is not a steady state under the paper's definition.

Formalization scope

All declarations live in the namespace ReferencePricing.LossAversion.

• Data. The model data are a base demand d : ℝ → ℝ and reference effects R : ℝ → ℝ → ℝ, with demand d p + R (r - p) r. $R(0,r)=0$ is a field of Assumption 1.
• Value function. value takes the per-period profit as a parameter and is the real supremum ⨆ over sequences ℕ → Set.Icc 0 pbar of the tsum of discounted profits. It is not a function assumed to solve (2).
• Policy. optPrice is sSup of the set of maximizers in $P$ of the Bellman objective, following the paper's largest-maximizer convention. Nonemptiness of that set is to be proved, never assumed.
• Steady states. IsSteadyState r is r ∈ P ∧ optPrice r = r.
• Encodings. Monotonicity, concavity and supermodularity hypotheses are required on $P$ or $P\times P$, and monotonicity in $x$ and single crossing on the reachable gains $[r-\bar p,r]$. "Twice differentiable" means that the uncurried function and its Fréchet derivative are differentiable. "Nonmonotonic" means neither monotone nor antitone on $P$.
• Added hypotheses. Two hypotheses are added and disclosed in each item. The base demand $d$ is differentiable, because $\pi'$ appears in Assumption 3(b). The demands of $R_G$ and $R_L$ satisfy Assumption 1, which the paper's proof of Lemma 4 uses.
• Typos. The page's typo "$r_0>p^*_G$" in Theorem 4 is read as $p^{**}_G$.
• Ruling out trivial versions. The goal quantifies $p^{**}_L$ and $p^{**}_G$ existentially with uniqueness, so the existence of these steady states is part of the claim. It is not a formalization with arbitrary endpoints supplied as hypotheses, nor one with "some optimal policy" in place of the largest maximizer. The hypotheses are jointly satisfiable: the linear instance $\bar p=3/4$, $d(p)=1-p$, $R_L=x/4$, $R_G=x/8$ meets all of them.

A complete development needs:

• the Bellman equation and continuity of the value function for bounded continuous rewards on a compact action set (Berge's maximum theorem);
• Topkis-type monotone comparative statics on intervals;
• convergence of monotone bounded sequences.

The first two are reusable beyond this mission, and contributions of either as general lemmas are welcome.

Selected references

• I. Popescu and Y. Wu, Dynamic Pricing Strategies with Reference Effects, Operations Research 55(3):413–429, 2007. https://doi.org/10.1287/opre.1070.0393
• D. Kahneman and A. Tversky, Prospect Theory: An Analysis of Decision under Risk, Econometrica 47(2):263–291, 1979. https://doi.org/10.2307/1914185
• P. K. Kopalle, A. G. Rao and J. L. Assunção, Asymmetric Reference Price Effects and Dynamic Pricing Policies, Marketing Science 15(1):60–85, 1996. https://doi.org/10.1287/mksc.15.1.60
• G. Fibich, A. Gavious and O. Lowengart, Explicit Solutions of Optimization Models and Differential Games with Nonsmooth (Asymmetric) Reference-Price Effects, Operations Research 51(5):721–734, 2003. https://doi.org/10.1287/opre.51.5.721.16758
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• N. L. Stokey, R. E. Lucas and E. C. Prescott, Recursive Methods in Economic Dynamics, Harvard University Press, 1989. https://www.hup.harvard.edu/books/9780674750968

Motivation

Airlines, hotels and railways sell a fixed stock of perishable capacity (seats on flight legs, room-nights) to customers who arrive over a finite selling horizon. Network revenue management decides, at each moment, which products to keep open for sale. In the classical independent-demand model each product has its own demand stream. In practice customers choose among the products on offer, and closing a cheap fare shifts some of its demand to a more expensive one. Talluri and van Ryzin (Management Science 2004) modelled this with choice-based demand on a single resource: the firm chooses an offer set $S$, and an arriving customer buys product $j$ with probability $P_j(S)$.

On a network the exact dynamic program has one state per vector of remaining leg capacities, and cannot be solved at realistic sizes. Gallego, Iyengar, Phillips and Dubey (CORC Technical Report TR-2004-01, 2004) proposed replacing it with a linear program over the time allotted to each offer set, the choice-based deterministic linear program (CDLP). Liu and van Ryzin (MSOM 2008) analysed this LP. Their first result has two parts: the CDLP value is an upper bound on the optimal expected revenue, and the bound is asymptotically tight when capacity and horizon are scaled up together. For the independent-demand deterministic LP the analogous statement goes back to Gallego and van Ryzin (Operations Research 1997) and Cooper (Operations Research 2002). This mission targets the choice-based version.

Setting

A choice-based network instance has $m$ legs and $n$ products $N = \{1,\dots,n\}$, and consists of:

• an incidence matrix $A = [a_{ij}]$ with $a_{ij} \in \{0,1\}$, where $a_{ij}=1$ when product $j$ uses leg $i$; $A_j$ is its $j$th column;
• a revenue $r_j \in \mathbb{R}$ for each product (no sign assumed);
• an arrival probability $\lambda \in [0,1]$ per period;
• choice probabilities $P_j(S)$ for every offer set $S \subseteq N$, with $P_j(S) \ge 0$, $P_j(S)=0$ for $j \notin S$, and $\sum_{j\in S} P_j(S) \le 1$. The no-purchase probability is $P_0(S) = 1 - \sum_{j\in S}P_j(S)$.

$\lambda$ and $P$ are the same in every period. Each offer set has an expected revenue $R(S) = \sum_{j\in S} r_j P_j(S)$ and a capacity-consumption vector $Q(S) = AP(S)$.

The dynamic program. With remaining capacity $x \in \mathbb{N}^m$, an offer set is allowed if $x - A_j \ge 0$ for all $j \in S$ (no overbooking). The empty set is always allowed. The value with $k$ periods left is $V^{(0)} \equiv 0$ and

$$V^{(k+1)}(x) = \max_{S \text{ allowed at } x}\Big\{\sum_{j\in S}\lambda P_j(S)\big(r_j + V^{(k)}(x-A_j)\big) + \big(\lambda P_0(S)+1-\lambda\big)V^{(k)}(x)\Big\}.$$

The optimal expected revenue over $T$ periods from capacity $c \in \mathbb{N}^m$ is $V^*(c,T) = V^{(T)}(c)$ (dpValue).

The CDLP. Its variables are times $t(S) \ge 0$, one for each $S \subseteq N$, and

$$V^{\mathrm{CDLP}}(c,T) = \max\Big\{\sum_{S}\lambda R(S)t(S) \;:\; \sum_S \lambda Q(S)t(S) \le c,\ \sum_S t(S) \le T,\ t \ge 0\Big\}$$

(cdlpValue).

Scaling. For $\theta \in \mathbb{N}$, the $\theta$-scaled problems have capacities $\theta c$ and horizon $\theta T$. Write $V^*_\theta = V^*(\theta c,\theta T)$ and $V^{\mathrm{CDLP}}_\theta = V^{\mathrm{CDLP}}(\theta c, \theta T)$.

Formalization targets

Goal: Proposition 2 (p. 294)

$$\lim_{\theta\to\infty}\frac1\theta V^*_\theta \;=\; \lim_{\theta\to\infty}\frac1\theta V^{\mathrm{CDLP}}_\theta \;=\; V^{\mathrm{CDLP}}(c,T),$$

for every instance, every $c \in \mathbb{N}^m$ and every $T\in\mathbb{N}$. It is stated as two Tendsto statements along $\theta \to \infty$ in $\mathbb{N}$.

Milestones

1. Proposition 1 (p. 294): $V^*(c,T) \le V^{\mathrm{CDLP}}(c,T)$ for every $c$ and $T$.
2. Scaling of the CDLP (proof of Proposition 2, first paragraph): $V^{\mathrm{CDLP}}(\theta c,\theta T) = \theta\,V^{\mathrm{CDLP}}(c,T)$ for every $\theta \in \mathbb{N}$.
3. Lower half of the first limit (proof of Proposition 2, pp. 294–295): for every $\varepsilon>0$, eventually in $\theta$, $V^{\mathrm{CDLP}}(c,T) - \varepsilon \le \frac1\theta V^*_\theta$.

The goal follows from the three milestones.

Significance

The result. Proposition 1 makes the CDLP a certified upper bound on what any control policy can earn, whatever the choice model. Numerical studies use it to benchmark heuristics. Proposition 2 says the bound is exact to first order in large systems, so policies driven by the CDLP solution (time allocations, bid prices from its dual) lose only a vanishing fraction of revenue. It is the justification for the whole family of CDLP-based controls that the paper and later work study (column generation, decomposition, and later the affine and piecewise-linear relaxations of the choice-based network problem).

Formalizing it. The result is proved in the paper. No machine-checked version exists: no revenue-management DP with choice-based demand on a network, no CDLP, and no fluid-limit argument of this kind is on the platform. The existing RevenueManagement material from the Talluri–van Ryzin textbook covers single-resource and dynamic-pricing models. Formalizing the result produces a reusable network-RM DP with an offer-set action space, the CDLP as a Lean object, and a checked asymptotic-optimality theorem that other deterministic-approximation results (independent demand, bid-price heuristics) can follow.

Difficulty

The upper bound compares a stochastic dynamic program with a linear program. The natural route builds a feasible LP point from the optimal policy (expected times each set is offered), but the DP here is a recursion over capacity vectors, not a policy class with a notion of "expected time offered". That connection has to be made from the recursion itself.

The lower bound is harder. The paper's policy offers each set for a fractional number of periods and caps accepted demand at its mean after customers have chosen. Neither is an action available in the DP, where the firm can only pick an allowed offer set each period and must accept whatever the customer picks. The obvious transcription therefore does not type-check against the model: one needs a genuine DP policy whose revenue is $\theta V^{\mathrm{CDLP}} - o(\theta)$ while it respects capacity on every sample path. The no-overbooking rule forbids offering a set once any of its products would exceed remaining capacity. Negative revenues are allowed, and $\lambda$ may be $0$ or $1$.

Formalization scope

Legs are Fin m, products Fin n, offer sets Finset (Fin n). The instance is a structure ChoiceNetwork m n carrying $A$ (entries in $\mathbb{N}$, each $0$ or $1$), $r$, $\lambda\in[0,1]$ and $P$ with the three choice-model axioms. The DP and CDLP use one $\lambda$ and one $P$ for every period, matching the paper's time-homogeneous model. Capacities and horizon are natural numbers; CDLP times and all values are real. $\theta$ ranges over $\mathbb{N}$, because $\theta T$ must be a whole number of periods, and the limits use real division by $\theta$.

$V^*$ is defined by the Bellman recursion (1), which the paper states is equivalent to the stochastic control problem (4). No measure-theoretic policy class is built. The maximization runs over the offer sets allowed at the current capacity, so the DP can neither overbook nor pick products outside an offer set. The paper's boundary condition $V_t(0)=0$ is not imposed separately: it follows from the recursion whenever every product uses a leg, and imposing it on top could contradict the recursion. $V^{\mathrm{CDLP}}$ is sSup of the objective over the feasible set. That set is nonempty ($t=0$) and bounded ($0 \le t(S) \le T$), so the value is the LP optimum.

The goal is the limit equality with both capacity and horizon scaled. A statement with only the upper bound, only capacity scaled, or a DP that ignores capacity or chooses products freely would be a trivializing formalization, and the definitions rule each of these out. Milestone 3 is the paper's conclusion stated on the DP value, not on the paper's informal policy. It is not a repair.

A complete development needs: LP duality or a direct feasibility construction for Proposition 1; the scaling identity for the CDLP; and, for the lower bound, a concrete DP policy together with a law-of-large-numbers or concentration estimate for sums of per-period sales (Mathlib's ProbabilityTheory.strong_law_ae and Hoeffding-type bounds are available). A policy-evaluation lemma that bounds the DP value below by the expected revenue of any feasible offer-set policy is reusable beyond this mission, as is the CDLP scaling lemma. Contributions to either are welcome.

Selected references

• Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0169
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• G. Gallego, G. Iyengar, R. Phillips, A. Dubey, Managing Flexible Products on a Network, CORC Technical Report TR-2004-01, Columbia University, 2004.
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1):24–41, 1997. https://doi.org/10.1287/opre.45.1.24
• W. L. Cooper, Asymptotic Behavior of an Allocation Policy for Revenue Management, Operations Research 50(4):720–727, 2002. https://doi.org/10.1287/opre.50.4.720.2862