Revenue Management and Choice Models

Which fares to open, and when to close them

An airline sells one flight, a hotel one night, a car-rental firm one day of one car: a fixed capacity, perishable at a deadline, sold to customers who arrive over time and are willing to pay different amounts. Chapter 2 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) is the theory of that single resource. Its three models answer the same question with increasing generality: Littlewood's two-class rule, the $n$-class static model and its dynamic-arrival version give the seller a protection level per class, a booking limit or a bid price, all three equivalent; the discrete-choice model, in which customers buy down when a cheaper fare is open, replaces classes by offer sets and shows that only the efficient sets, ordered by their purchase probability, are ever offered, with a higher set the more capacity or the less time remains. This mission formalizes that last result, Theorem 2.3, together with the structural results of the two earlier models that it generalizes.

Setting

Static model. Classes $1, \dots, n$ with prices $p_1 \ge \dots \ge p_n \ge 0$ arrive in stages, lowest class first, with demands $D_j$ distributed on $\mathbb N$. With $x$ units left at stage $j$ the seller observes $D_j$ and accepts $u \le \min\{D_j, x\}$ units; the value function is the Bellman equation (2.3), $V_j(x) = \mathbb E[\max_u \{p_j u + V_{j-1}(x-u)\}]$, $V_0 = 0$ (staticValue), and $\Delta V_j(x) = V_j(x) - V_j(x-1)$ is the marginal value of capacity. The protection level $y_j^* = \max\{x : p_{j+1} < \Delta V_j(x)\}$ (protLevel), the booking limit $b_j^* = C - y_{j-1}^*$ (bookLimit) and the bid price $\pi_{j+1}(x) = \Delta V_j(x)$ (bidPrice) define the three controls of Theorem 2.1.

Dynamic model. Over $T$ periods at most one request arrives per period, of class $j$ with probability $\lambda_j(t)$; the value function (2.17) is $V_t(x) = V_{t+1}(x) + \mathbb E[\max_{u \in \{0,1\}} (R(t) - \Delta V_{t+1}(x))u]$ (dynValue), with time-dependent protection levels (2.19), booking limits (2.20) and bid prices (2.18).

Choice model. When the set $S$ of classes is open an arriving customer buys class $j \in S$ with probability $P_j(S)$; $Q(S) = \sum_{j \in S} P_j(S)$ is the purchase probability and $R(S) = \sum_{j \in S} P_j(S) p_j$ the expected revenue (purchaseProb, expRevenue). The value function (2.26) is $V_t(x) = \max_{S} \lambda_t (R(S) - Q(S)\Delta V_{t+1}(x)) + V_{t+1}(x)$ (choiceValue). A set $T$ is inefficient (Definition 2.1, IsInefficient) if a randomization $\alpha$ over the subsets has $\sum_S \alpha(S) Q(S) \le Q(T)$ and $\sum_S \alpha(S) R(S) > R(T)$, and efficient otherwise.

Formalization targets

Goal: Theorem 2.3

In every period with capacity left, some efficient set maximizes (2.26); and, the efficient sets being ordered by $Q$, the largest optimal set is nondecreasing in the remaining capacity $x$ and nondecreasing in the period $t$: choice_optimal_policy. Monotonicity is stated as "every efficient optimal set at $(t, x)$ is matched by one at $(t, x')$, $x' \ge x$, with at least as large a purchase probability", and likewise in $t$.

Supporting targets

Littlewood's rule (2.1), $\Delta V_1(x) = p_1 \mathbb P(D_1 \ge x)$ and the acceptance criterion; Proposition 2.1, the marginal values of the static model are decreasing in $x$ and increasing in the stages remaining; Theorem 2.1, nested protection levels, nested booking limits and bid-price tables each attain the Bellman maximum at every stage; Proposition 2.2 and Theorem 2.2, the same two results for the dynamic model, with marginal values now decreasing in time; Proposition 2-2.A.4 of the appendix, the marginal values of the choice model are decreasing in $x$ and in $t$; Proposition 2.3, an inefficient set is never optimal; and the ordering of efficient sets, $Q(S) \le Q(S')$ implies $R(S) \le R(S')$ when $S'$ is efficient.

The continuous-demand optimality conditions (2.9) of Sect. 2.2.2.3, stated without proof, the computational and heuristic methods of Sects. 2.2.3-2.2.4, the overbooking models of Sect. 2.7 and the nested-policy characterization of Sect. 2.6.2.5 are not targets.

Significance

Theorem 2.3 is the structural result behind choice-based revenue management: it reduces the $2^n$ offer sets to the efficient frontier of $(Q(S), R(S))$, orders that frontier, and shows the optimal policy walks up it as capacity grows or the deadline nears. It was the analytical core of Talluri and van Ryzin's (2004) choice-model paper and is the reason the efficient sets, not the fare classes, are the unit of control when customers substitute between fares. The static and dynamic results, from Littlewood (1972) and Brumelle and McGill (1993) to Lee and Hersh (1993), are the foundation of every airline seat inventory control system; the equivalence of protection levels, booking limits and bid prices is what lets the same optimal policy be implemented on any of the three kinds of reservation system. None of these results has a machine-checked proof.

Difficulty

The two marginal-value propositions are inductions in which the inductive step is the discrete concavity of a max-plus convolution, Lemma 2-2.A.1 of the appendix: $x \mapsto \max_{0 \le a \le m}\{ap + g(x-a)\}$ is concave when $g$ is, which in Lean requires reasoning about the argmax on $\mathbb N$ and the truncated subtraction. The static model's expectation is a tsum against a pmf, so every step also needs summability of a bounded family. The protection-level theorems then need the down-set structure of $\{x : p_{j+1} < \Delta V_j(x)\}$ under monotonicity of $\Delta V_j$, and the three controls have to be shown to coincide unit by unit. For the choice model, Proposition 2.3 is a one-line convexity argument once $\Delta V \ge 0$ is known, and the monotonicity in Theorem 2.3 is a monotone comparative-statics argument on the objective $R(S) - Q(S)\Delta$, which is easy in $\Delta$ but must be combined with Proposition 2-2.A.4 in both $x$ and $t$; the existence of an efficient maximizer uses Proposition 2.3 and the finiteness of the subsets.

Formalization scope

Capacities, stages and periods are natural numbers, the value functions recurse on the stage or on the number of periods to go, and the book's ranges ($x \le C$, $t \le T$, $j \le n$) are hypotheses of the theorems. Demand in the static model is a pmf on $\mathbb N$ rather than a random variable, so the expectation in (2.3) is a tsum; the dynamic model's expectation over $R(t)$ is written out, including the no-arrival term, which vanishes under nonnegative prices. The choice model is defined by its compact form (2.26), and the maximization includes the empty offer set. Optimality of a control means attaining the inner maximum of the Bellman equation at every state, which is what the book's proofs establish. The bid-price control is formalized with the bid price $\pi_{j+1}(x + 1 - z)$ of the $z$-th unit allocated; the book prints $x - z$, which is one unit off from (2.5). The appendix's Proposition 2-2.A.4 prints its time monotonicity in the reverse direction; the formal statement is the direction consistent with Proposition 2.2 and Theorem 2.3. The ordering of efficient sets is stated with non-strict inequalities, since Definition 2.1 admits ties in revenue.

Selected references

• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 2. https://doi.org/10.1007/b139000
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• S. L. Brumelle and J. I. McGill, Airline seat allocation with multiple nested fare classes, Operations Research 41(1), 1993. https://doi.org/10.1287/opre.41.1.127
• T. C. Lee and M. Hersh, A model for dynamic airline seat inventory control with multiple seat bookings, Transportation Science 27(3), 1993. https://doi.org/10.1287/trsc.27.3.252
• K. T. Talluri and G. J. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• C. J. Lautenbacher and S. Stidham, The underlying Markov decision process in the single-leg airline yield-management problem, Transportation Science 33(2), 1999. https://doi.org/10.1287/trsc.33.2.136

How far to oversell

Every airline, hotel and car-rental firm sells more reservations than it has capacity, because some customers cancel or do not show. Chapter 4 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) is the theory of that decision. Its static models pick one overbooking limit from the show distribution; its dynamic model, a simplification of Chatwin's (1998), follows reservations, cancellations and refunds period by period and proves that the optimal control is still a limit, one that declines toward the deadline and falls when more demand is expected; and its substitutable-capacity model, from Karaesmen and van Ryzin (2004), sets joint limits for several classes whose oversold customers can be moved between resources, showing the expected net revenue is concave in each limit and submodular across them. This mission formalizes the chapter's four propositions and the corollary the book draws from the last.

Setting

Dynamic overbooking (Sect. 4.3.1). With $y$ reservations on hand in period $t$, $D_t$ new requests arrive; the firm books up to $x \in [y, y + D_t]$ at revenue $p(t)$ each, and every reservation survives the period with probability $q_t$, a cancellation refunding $r(t)$. At the deadline $T + 1$ the firm pays the convex denied-service cost $c(y - C)$ on reservations beyond capacity $C$, Eq. (4.11). The recursion is $v_{t+1}(x) = \mathbb E[V_{t+1}(Z_t(x)) - (x - Z_t(x))\,r(t)]$ with $Z_t(x) \sim \mathrm{Bin}(x, q_t)$ and $V_t(y) = \mathbb E[\max_{y \le x \le y + D_t}\{v_{t+1}(x) + (x - y)\,p(t)\}]$ (value, postValue). The greatest optimal overbooking limit $x^*(t)$ (overbookingLimit) is the largest level at which $v_{t+1}(x) + x\,p(t)$ is at least its value at every smaller level, an element of $\mathbb N \cup \{\infty\}$; the limit policy books $\min\{y + D_t, \max\{y, x^*\}\}$ (limitPolicy).

Substitutable capacity (Sect. 4.5). Classes $j = 1, \dots, n$ hold $y_j$ reservations and are overbooked to levels $x_j$; in the service period $Z_j \sim \mathrm{Poisson}(q_j x_j)$ customers show and are assigned to resources $i = 1, \dots, m$ of capacities $C_i$, or to the virtual resource $0$ (denied service), at net benefit $h_{ji}$, by the transportation problem (TP) with value $V(z, C)$ (serviceValue). The expected net revenue (4.21) is $G(x) = p^\top(x - y) - \mathbb E[s^\top(x - Z(x))] + \mathbb E[V(Z(x), C)]$ (expNetRevenue), and jointLimit is the greatest optimal limit of one class with the others fixed.

Formalization targets

Goal: Proposition 4.4

With Poisson show demands, $G$ has decreasing first differences in every direction: $G(x + e_i + e_j) - G(x + e_i) \le G(x + e_j) - G(x)$ for all $x$ and all classes $i, j$, which is component-wise concavity ($i = j$) and submodularity ($i \ne j$): joint_overbooking_concave_submodular.

Supporting targets

Proposition 4.1, with a convex denied-service cost the limit policy with the greatest optimal limit attains the maximum of the recursion at every state; Proposition 4.2, under $q_t(p(t) - p(t+1)) + (1 - q_t)(p(t) - r(t)) \ge 0$ the greatest optimal limits decline with time; Proposition 4.3, stochastically larger demand to come gives limits that are no larger; and the corollary of Sect. 4.5.2, the greatest optimal limit of class $i$ is nonincreasing in the level of any other class.

The static overbooking models of Sect. 4.2 (binomial, normal and Gram-Charlier approximations, Type 1 and Type 2 service levels), the net-bookings heuristics of Sect. 4.3.2, the combined capacity-control models of Sect. 4.4 and the stochastic-gradient algorithm of Appendix 4.A carry no numbered results and are not targets.

Significance

Proposition 4.4 is the structural fact that makes joint overbooking of related resources tractable: concavity gives each class a critical booking level and submodularity makes those levels move in opposite directions, so a stochastic-gradient or coordinate search on the limits is well behaved, and the pattern of Example 4.5, overbooking an early flight aggressively because its oversold passengers can be moved to later ones, is a consequence rather than a heuristic. The dynamic propositions are the theoretical support for the overbooking curves that reservation systems post, limits that fall as departure approaches, and they quantify the sense in which a static model, which ignores future demand, overbooks too much. The proof of Proposition 4.4 passes through the discrete concavity of the transportation problem's value in its supply vector, an M-natural-concavity fact in the sense of Murota, and the Poisson-expectation identity for second differences; none of this has a machine-checked proof.

Difficulty

The dynamic model needs the concavity of $V_t$ on $\mathbb N$ to be propagated through two operations, the binomial thinning $x \mapsto \mathbb E[V(\mathrm{Bin}(x, q))]$ and the windowed maximum $y \mapsto \max_{y \le x \le y + D} g(x)$, both of which preserve discrete concavity but require explicit manipulation of binomial sums and of the argmax; Propositions 4.2 and 4.3 then compare greatest maximizers of concave sequences through lower bounds on marginal values, with the value $\infty$ handled in ℕ∞. The substitutable-capacity goal is harder: the value of (TP) as a function of the integer supply vector must be shown to have decreasing differences, which is the submodularity of a max-weight transportation value in its supplies, a linear programming duality argument (or Murota's M-natural-concavity of min-cost flow), and the Poisson expectation of it, a tsum over $\mathbb N^n$, must be differenced in two coordinates using the identity $\mathbb E[f(N_{\mu + \delta})] - \mathbb E[f(N_\mu)]$ for Poisson pmfs. The linear terms of $G$ cancel in second differences and the refund term is linear in $x$.

Formalization scope

Periods are natural numbers with value t the value with $T + 1 - t$ periods to go, and the book's ranges $1 \le t \le T$ are hypotheses. The denied-service cost is normalized, $c(0) = 0$ and $c \ge 0$, as a cost "penalizing denied service" is. Convexity of the sequence alone is not enough, because (4.11) never reads $c(0)$. Demands are pmfs on $\mathbb N$ and cancellations exact binomial sums. The greatest optimal limit lives in $\mathbb N \cup \{\infty\}$ because a mild denied-service cost can make accepting every request optimal, in which case the book's critical value is $+\infty$; the limit policy then accepts everything. Proposition 4.3 is stated for two demand families ordered by first-order stochastic dominance rather than a parametrized family. In the substitutable-capacity model the virtual resource is uncapacitated, the book's "finite but very high" $C_0$ taken as infinite so that (TP) is feasible for every Poisson realization, and (TP) is over real assignments, whose optimum at integer supplies is integral. Eq. (4.21) is printed with $-\mathbb E[V(Z(x), C)]$; $V$ being the maximum net benefit, the expected net revenue adds it, and the definition uses $+$, without which Proposition 4.4 fails numerically on every sampled instance.

Selected references

• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 4. https://doi.org/10.1007/b139000
• R. E. Chatwin, Multiperiod airline overbooking with a single fare class, Operations Research 46(6), 1998. https://doi.org/10.1287/opre.46.6.805
• I. Karaesmen and G. J. van Ryzin, Overbooking with substitutable inventory classes, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0079
• M. Rothstein, OR and the airline overbooking problem, Operations Research 33(2), 1985. https://doi.org/10.1287/opre.33.2.237
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

Prices that respond to inventory

A retailer marking down a seasonal line, an airline raising fares as seats sell, a manufacturer pricing while restocking: each sets prices over time against a finite and changing inventory. Chapter 5 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) collects the structural theory of that problem. Without replenishment, the Bernoulli-arrival model of Gallego and van Ryzin (1994) gives a marginal value of capacity that falls with inventory and with time, hence prices that jump up at each sale and drift down between sales, and the deterministic fluid model bounds it from above. With replenishment, the model of Federgruen and Heching (1999) has a jointly concave and supermodular continuation value, from which the base-stock, posted-price policy follows: below a base-stock level order up to it and post a fixed price, above it order nothing and discount, more the higher the inventory. This mission formalizes those results with Proposition 5.3 as the goal.

Setting

Bernoulli demand (Sect. 5.2.2.2). One customer arrives per period with a random willingness to pay; the firm's decision is the demand rate $d \in [0, 1]$, the probability of a sale at the inverse-demand price $p(t, d)$, with revenue rate $r(t, d) = d\,p(t, d)$ (revenueRate). The value function (5.12) is $V_t(x) = \max_{d}\{r(t, d) - d\,\Delta V_{t+1}(x)\} + V_{t+1}(x)$, $V_{T+1} = 0$, $V_t(0) = 0$ (bernoulliValue), and $\Delta V_t(x) = V_t(x) - V_t(x-1)$ (bernoulliDelta). The deterministic model (5.1) maximizes $\sum_t r(t, d(t))$ over rates with $\sum_t d(t) \le C$ (deterministicValue).

Pricing with replenishment (Sect. 5.3.2). Inventory may be negative (backorders). In period $t$ with inventory $x$ the firm orders up to $y \ge x$ at unit cost $c_t$, chooses a rate $d \in [0, \bar d]$, sells the random demand $D(t, d, \xi_t) = a_t(\xi_t)\,d + b_t(\xi_t)$ (additive, multiplicative or mixed noise), and pays the convex cost $h_t$ on ending inventory. The value function (5.20) is $V_t(x) = \sup_{y \ge x,\, d}\{r(t, d) - c_t(y - x) + G_{t+1}(y, d)\}$ with the continuation value $G_{t+1}(y, d) = \mathbb E[V_{t+1}(y - D(t, d, \xi_t)) - h_t(y - D(t, d, \xi_t))]$ (ReplPricing.value, contValue). Assumption 7.2, marginal revenue decreasing, is the concavity of $r(t, \cdot)$.

Formalization targets

Goal: Proposition 5.3

For every period, $G_{t+1}$ is jointly concave on $\mathbb R \times [0, \bar d]$, $V_t$ is concave on $\mathbb R$, and $G_{t+1}$ has increasing differences in $(y, d)$, the supermodularity that the book states through its partial derivatives: replenishment_concave_supermodular.

Supporting targets

Proposition 5.2, the marginal value of capacity in the Bernoulli model decreases in $t$ and in $x$; the upper bound of Sect. 5.2.2.3, the optimal deterministic revenue dominates the optimal expected stochastic revenue; and the base-stock, posted-price structure of Sect. 5.3.2.1, derived from Proposition 5.3: below the unconstrained optimum $y^0$ order up to it and use $d^0$, above it order nothing and use a rate at least $d^0$ that is nondecreasing in the inventory.

Proposition 5.1 and Lemma 5-5.A.1 (the continuous-demand model without replenishment) are not targets; see the formalization scope. The deterministic sections (efficient prices, discrete price sets), the asymptotic optimality of the deterministic heuristic, the infinite-horizon stationary problem and the multiproduct and finite-population models carry no numbered results.

Significance

Proposition 5.3 is the structural core of joint pricing and inventory control: joint concavity makes the period problem a concave program, and supermodularity is what turns its solution into a policy, the base-stock, posted-price rule that Federgruen and Heching showed optimal and that later work on pricing with inventory builds on. Proposition 5.2 is the reason optimal dynamic prices in the stochastic single-item model rise at every sale and fall while inventory sits, the behaviour of Figure 5.5, and the deterministic upper bound is what justifies the fluid model as a benchmark and a heuristic, the pattern quantified in Table 5.6. None of these has a machine-checked proof; the replenishment result in particular needs the interplay of concavity, expectation and partial maximization on all of $\mathbb R$.

Difficulty

Proposition 5.2 is an induction whose step compares suprema over the rate interval, with the boundary condition $V_t(0) = 0$ breaking the recursion at $x = 1$ and requiring $r(t, 0) = 0$. The deterministic bound is an induction on periods that uses the concavity of the deterministic value in the inventory (a concave program's value) to absorb the two branches of the Bernoulli recursion. The goal needs: integrability and continuity of $V_{t+1}(y - D) - h_t(y - D)$ under bounded noise; that the expectation of a concave function of an affine map is jointly concave, and its increasing differences from those of the concave integrand; that a partial supremum of a jointly concave function over the convex feasible set $\{y \ge x\}$ is concave in $x$; and the boundedness of the objective so that every supremum is a real number. The base-stock item is the segment argument that moves an unconstrained maximizer onto the boundary $y = x$ and a monotone comparative-statics argument on the supermodular objective, with maxima attained by continuity on the compact rate interval.

Formalization scope

Periods are natural numbers with value t the value with $T + 1 - t$ periods to go, the maxima are suprema, and the book's ranges are hypotheses. The demand is affine in the rate, which is the additive and multiplicative models the book names; with a merely convex demand (Assumption 5.1) the joint concavity of Proposition 5.3 fails when $V_{t+1} - h_t$ is not monotone, and the noise has bounded support, strengthening Assumption 7.6. The partial-derivative statements (iii)-(iv) are in difference form. Proposition 5.1 is not formalized: its model (5.11) evaluates $V_{t+1}(x - D)$ at negative inventories the model does not define while truncating revenue at $x$, and its Lemma 5-5.A.1 (joint concavity of $r^+$) is false as stated, its Hessian argument mistaking an indefinite matrix for a negative definite one; a counterexample is in the mission's check. The deterministic model restricts rates to $[0, 1]$, the rates the Bernoulli model can realize.

Selected references

• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 5. https://doi.org/10.1007/b139000
• G. Gallego and G. J. van Ryzin, Optimal dynamic pricing of inventories with stochastic demand over finite horizons, Management Science 40(8), 1994. https://doi.org/10.1287/mnsc.40.8.999
• A. Federgruen and A. Heching, Combined pricing and inventory control under uncertainty, Operations Research 47(3), 1999. https://doi.org/10.1287/opre.47.3.454
• W. Elmaghraby and P. Keskinocak, Dynamic pricing in the presence of inventory considerations, Management Science 49(10), 2003. https://doi.org/10.1287/mnsc.49.10.1287.17315
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Why a reserve price, and why it does not matter which auction

Airlines selling last seats, Priceline's name-your-own-price, procurement of supply contracts: Chapter 6 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) treats auctions as pricing mechanisms and asks what revenue they earn and how to design them. Its centre is Myerson's (1981) theory for independent private values: whatever the mechanism, so long as bidders with higher valuations are more likely to win and the lowest type gains nothing, the firm's expected revenue is the expected virtual value $\sum_i J(v_i) y_i(v)$ of the winners, with $J(v) = v - (1 - F(v))/f(v)$ (Theorem 6.1, the revenue equivalence theorem). Maximizing that expression pointwise gives the optimal auction: the standard first- or second-price auction with a reserve price $v^*$ at the zero of $J$ (Theorem 6.2). This mission formalizes the second-price form of Theorem 6.2 as its goal, with the dominant-strategy and first-price equilibria of the informal analysis, Theorem 6.1, the optimal allocation and Proposition 6.1 on list prices as supporting results.

Setting

$N$ customers have i.i.d. valuations on $[0, \bar v]$ with a continuously differentiable, strictly increasing distribution $F$ and positive density $f$ (PrivateValues, IsRegular); the joint law is the product measure (joint). A direct-revelation mechanism (Mechanism) maps reported valuations to allocations $y_i(v) \in \{0, 1\}$, at most $C$ units in total, and payments $p_i(v)$. For a report $w$ by customer $i$, $P_i(w)$ is the win probability, $R_i(w)$ the expected payment and $S_i(w) = w P_i(w) - R_i(w)$ the surplus (winProb, expPayment, expSurplus); incentive compatibility, $S_i(w) \ge w P_i(w') - R_i(w')$, is the equilibrium condition of the direct mechanism (IsIncentiveCompatible). The chapter's mechanisms are the $C$-unit second-price auction with reserve price $r$ (secondPriceReserve: the $C$ highest valuations above $r$ win and pay the larger of $r$ and the highest losing valuation), the list-price mechanism for $N \le C$ (listPrice), and the single-unit first-price auction with its equilibrium bid $b^*(v) = v - \int_0^v P(s)\,ds / P(v)$, $P = F^{N-1}$ (firstPriceBid).

Formalization targets

Goal: Theorem 6.2

With $J$ strictly increasing (Assumption 7.2) and $v^*$ its zero, the $C$-unit second-price auction with reserve price $v^*$ is a feasible, incentive-compatible mechanism with monotone allocations and zero surplus at zero, and its expected revenue is at least that of every such mechanism: reserve_price_auction_optimal.

Supporting targets

Bidding one's valuation is dominant in the second-price auction (Sect. 6.2.2.1); the bid (6.4) solves the first-order condition (6.3), is a symmetric equilibrium of the first-price auction and shades below the valuation (Sect. 6.2.2.2); Theorem 6.1, revenue equals expected virtual surplus and each expected payment is $w P_i(w) - \int_0^w P_i$; the pointwise optimal allocation of Sect. 6.2.5; and Proposition 6.1, a list price at $v^*$ is optimal when $N \le C$.

Proposition 6.2 (asymptotic optimality of list prices, a law-of-large-numbers statement about scaled auctions), the first-price form of Theorem 6.2 with its equilibrium (6.9) stated without proof, and the dynamic, replenishment and network auctions of Sects. 6.3-6.5 (Propositions 6.3-6.11, from Vulcano, van Ryzin and Maglaras and from Cooper and Menich) are not targets of this mission.

Significance

Theorem 6.1 is the tool that lets revenue be computed from allocations alone, which is why the first- and second-price auctions of Examples 6.1-6.3 earn the same $(N-1)/(N+1)$ and why any dynamic pricing scheme that ends with the same winners earns the same as the optimal auction (Sect. 6.2.6.3). Theorem 6.2 says a firm with private-value customers cannot do better than a standard auction with the right reserve price, and Proposition 6.1 that with enough capacity a list price already does it: auctions are a small-numbers phenomenon. These are the foundations on which the chapter's dynamic auctions and the list-price comparisons of Sects. 6.3-6.4 rest, and Myerson's optimal auction has no machine-checked proof in its multi-unit form.

Difficulty

Theorem 6.1 is an envelope argument in measure-theoretic clothing: incentive compatibility gives the two-sided inequalities of Appendix 6.A, monotonicity of $P_i$ makes $S_i$ convex with derivative $P_i$ almost everywhere, so $S_i(w) = \int_0^w P_i$, and then an integration by parts against the density converts $\int (w P_i(w) - S_i(w)) f(w)\,dw$ into $\int J(w) P_i(w) f(w)\,dw$; the win probabilities are integrals over a product measure with one coordinate replaced, and Fubini is needed to return to $\mathbb E[J(v_i) y_i(v)]$. The goal then needs the reserve-price auction shown incentive compatible (a dominant-strategy argument on the threshold payment), measurable, monotone and with zero surplus at zero, and the pointwise optimal allocation integrated. The first-price item is calculus on an interval integral with a vanishing denominator at $0$ and a monotone comparative-statics argument for the equilibrium inequality.

Formalization scope

Mechanisms are direct-revelation mechanisms on $[0, \bar v]^N$, as the book reduces to in Sect. 6.2.3.1; expectations over the other customers are integrals over the joint law with customer $i$'s coordinate overwritten by the report. Payments are assumed bounded on reports in $[0, \bar v]^N$ (not on all of $\mathbb R^N$, where the second-price payment is unbounded) and the rules measurable. Ties in the second-price auction are broken by index, a null event, and when every customer wins the losing supremum is $0$ so the winner pays the reserve. Theorem 6.2 is stated for the second-price auction; the first-price version with reserve price, whose equilibrium (6.9) the book asserts without proof, is left out and noted. Optimality is over mechanisms satisfying conditions (i) and (ii) of Theorem 6.1 and incentive compatibility, which is the class the book compares against. The virtual value's zero $v^*$ is a parameter with $J(v^*) = 0$ rather than the maximum of (6.8), which under strict monotonicity is the same point.

Selected references

• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 6. https://doi.org/10.1007/b139000
• R. B. Myerson, Optimal auction design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• J. G. Riley and W. F. Samuelson, Optimal auctions, American Economic Review 71(3), 1981. https://www.jstor.org/stable/1802786
• P. Klemperer, Auction theory: a guide to the literature, Journal of Economic Surveys 13(3), 1999. https://doi.org/10.1111/1467-6419.00083
• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16(1), 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• E. Maskin and J. Riley, Optimal multi-unit auctions, in The Economics of Missing Markets, Information, and Games, Oxford University Press, 1989.

When competing firms settle on prices and allocations

Revenue management is practised by firms that compete: airlines matching fares while allocating seats, retailers ordering stock and then pricing to clear it, hotels protecting rooms for late high-paying guests. Chapter 8 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) surveys the economics behind these situations: monopoly pricing and mechanism design, the Coase problem, advance-purchase discounts, and oligopoly in quantities (Cournot), in prices (Bertrand, Bertrand–Edgeworth with capacities), in newsvendor capacities and in RM allocations. Most of its numbered results are quoted from the literature; what the book itself establishes is a family of equilibrium arguments built on Talluri's equilibrium graph: when each firm's best response moves monotonically with the rival's action, following best-response arcs must end in an equilibrium pair. This mission formalizes those arguments, with Proposition 8.3, existence of an equilibrium in offer sets under the multinomial-logit choice model, as the goal.

Setting

A two-firm game on finite chains of strategies has payoffs $u_1, u_2$, best responses and pure Nash equilibria (IsBestResponse1, IsNashEquilibrium); its equilibrium graph has no crossing arcs (NoCrossing1) when best-response arcs $(k_2, k_1)$, $(l_2, l_1)$ with $k_2 < l_2$ always have $k_1 \le l_1$. The chapter's games are: the RM duopoly of Sect. 8.4.1.3, two firms with capacity $C$ and fares $p_L < p_H$ whose high-fare demand spills over to the rival beyond its protection level (spilloverDemand), each firm answering with Littlewood's protection level (littlewoodResponse); the duopoly newsvendor of Example 8.16 with effective demands $R_1 = D_1 + (D_2 - x_2)^+$ (effectiveDemand); linear Cournot (cournotPayoff); Bertrand–Edgeworth price competition with capacity $C$ per firm, linear demand and efficient rationing (beSales, bePayoff, IsBEEquilibrium); the advance-purchase model of Sect. 8.3.6 (peakLoadRevenue, advancePurchaseRevenue); and the one-period offer-set game of Sect. 8.4.3.2, where a firm offering its first $k$ products earns $g(C_k)/(W_1(k) + W_2(l) + w_0)$ with $g(C_k) = \sum_{j \le k} w_j(p_j - \Delta) - w_0\delta$ (OfferFirm, offerPayoff1, CaseI, CaseII).

Formalization targets

Goal: Proposition 8.3

If both firms are in Case I ($g(G^*) \ge 0$) or both in Case II ($g < 0$ on every complete set), the offer-set game has a pure-strategy equilibrium in complete sets: mnl_offer_set_equilibrium.

Supporting targets

The equilibrium-graph lemma, monotone best responses for both firms give an equilibrium (Sect. 8.4.1.3); Proposition 8.1, Littlewood responses in the RM duopoly are monotone in the rival's protection level, and the resulting equilibrium of the RM duopoly game; Example 8.16, duopoly newsvendor capacities total at least the monopoly capacity; Example 8.15, the symmetric Cournot equilibrium and its price; Theorem 8.5 (i)-(ii), the pure-strategy Bertrand–Edgeworth equilibria; and the advance-purchase comparison of Sect. 8.3.6, $w_2 < \hat w$ and $V_{APD}(\hat w) \ge V_{peak}(w_2)$.

Not targets: Theorems 8.1-8.2 (the Coase problem, subgame-perfect equilibria of an infinite-horizon game, proofs in von der Fehr and Kühn), Theorem 8.3 (Harris–Raviv priority pricing, stated with a garbled price formula), Theorem 8.4 (existence via quasiconcavity, cited), Theorem 8.5 (iii), 8.6 and 8.7-8.8 (mixed-strategy and supergame equilibria of Kreps and Scheinkman and Benoit and Krishna), Proposition 8.2 and Proposition 8.4 (the dynamic offer-set game under condition (8.32), proved in Talluri's paper), and the Kreps–Scheinkman derivation of Sect. 8.4.1.6, which rests on Theorem 8.6.

Significance

The equilibrium graph is the chapter's own contribution: a bipartite picture of best responses on chains in which monotonicity, the absence of crossing arcs, forces an equilibrium. It is the finite, combinatorial form of the monotone comparative-statics route to Nash equilibrium (Tarski's fixed point on a chain), and it is what makes RM allocation games tractable: the two-class duopoly with Littlewood responses always has an equilibrium, and the offer-set duopoly does whenever the two firms face the same sign of $g$, while Example 8.18 shows a best-response cycle when they do not. The Bertrand–Edgeworth, Cournot and newsvendor results are the benchmarks the book uses to interpret RM competition: capacity constraints soften Bertrand's zero-profit outcome, competing in allocations tends to raise total capacity above the monopoly level, and advance-purchase discounts dominate peak-load pricing as a self-selection mechanism. None of these has a machine-checked proof.

Difficulty

The lemma and the goal are fixed-point arguments on finite chains: the largest best response is a monotone map of the rival's index, the composition of two monotone (or two antitone) maps on a finite chain has a fixed point, and for the offer-set game the monotonicity itself must be extracted from the ratio structure $g(C_k)/(W(k) + a)$ as in the appendix's inequalities (8.A.3)-(8.A.5), separately in the two cases. Proposition 8.1 is a monotonicity of tail probabilities under the pointwise order of effective demands. Example 8.16 is a short probabilistic argument that needs the identity $\{D > x_1 + x_2\} = \{R_1 > x_1\} \cap \{R_2 > x_2\}$ and the strict monotonicity of the tail. Theorem 8.5 requires computing efficient-rationing sales for every unilateral deviation from a symmetric profile, through the recursive definition of residual demand, and a quadratic inequality for upward deviations in part (ii). The advance-purchase item reduces to the identity $V_{APD}(w) - V_{peak}(w) = (1 - \alpha)w$ and the strict decrease of the first-order-condition function.

Formalization scope

Products, protection levels and complete sets are natural numbers; the offer-set game's strategies are the complete sets $C_1, \dots, C_n$ of the book, and its payoff is (8.31) up to the positive factor $\lambda$ and the terms independent of both offer sets. Prices decreasing in the product index are a hypothesis, as the nested-by-revenue order of Sect. 8.4.3.2. The RM duopoly is modeled through Littlewood's response, as the book's appendix argues, rather than through expected revenues. Efficient rationing is defined recursively over the firms priced strictly below a given firm, with equal sharing among firms at the same price. Example 8.16 is stated with the equilibrium conditions (8.23) and the strictly increasing distribution of aggregate demand as hypotheses. The advance-purchase item takes the first-order conditions (8.13) and (8.15) and the book's uniqueness assumption as hypotheses, the latter as $(v - w) - F(w)/f(w)$ strictly decreasing in $w$ (the page prints "increasing", but its footnote identifies it with the monotone marginal-revenue assumption, which is decreasing in the waiting cost). Theorem 8.5 is stated for its pure-strategy parts (i) and (ii) only.

Selected references

• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 8. https://doi.org/10.1007/b139000
• D. M. Kreps and J. A. Scheinkman, Quantity precommitment and Bertrand competition yield Cournot outcomes, Bell Journal of Economics 14(2), 1983. https://doi.org/10.2307/3003636
• S. A. Lippman and K. F. McCardle, The competitive newsboy, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.54
• S. Netessine and R. A. Shumsky, Revenue management games: horizontal and vertical competition, Management Science 51(5), 2005. https://doi.org/10.1287/mnsc.1040.0356
• I. L. Gale and T. J. Holmes, Advance-purchase discounts and monopoly allocation of capacity, American Economic Review 83(1), 1993. https://www.jstor.org/stable/2117500
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Motivation

Retailers of fashion and seasonal goods sell at a premium price early in the season and mark the remaining stock down later. When customers anticipate the markdown, some of them who would buy at the premium price instead wait, trading a lower price against the risk that the item sells out and against the decline of their own valuation over the season. How forward-looking ("strategic") customers respond to a markdown policy is the first question any model of such pricing has to answer, because the seller's optimal prices depend on it.

Aviv and Pazgal (MSOM 2008) model a seller with a fixed inventory, Poisson arrivals of customers with heterogeneous, exponentially declining valuations, and two pricing regimes: contingent pricing, where the discount depends on the inventory left at the markdown time, and announced fixed discounts. The first step of their analysis of contingent pricing is Theorem 1: whatever the other customers do, a customer's best response is a threshold rule on his current valuation, with a threshold that rises as the markdown approaches. Their numerical study of equilibria and of the value of price commitment (§§4.2–7) is built on this reduction.

Setting

A seller holds $Q$ units over a season $[0, H]$ split at a fixed time $T$ with $0 < T \le H$. On $[0, T)$ the premium price $p_1$ applies. At time $T$ the seller observes the remaining inventory $Q_T \in \{0, 1, \dots, Q\}$ and charges the discount menu price $p_2(Q_T)$, where $p_2(q) \le p_1$ for $q = 1, \dots, Q$. Customer $j$ has a base valuation $V_j$ and valuation $V_j(t) = V_j e^{-\alpha t}$ at time $t$, with a common decline factor $\alpha \ge 0$.

A customer arriving at $t < T$ either buys immediately at $p_1$ or waits until $T$, when he requests a unit if the discounted price leaves him a nonnegative surplus. Waiting is uncertain in two ways: the remaining inventory $Q_T$ is random, and when fewer units remain than customers request them, units are rationed at random. A belief is a probability mass function $\pi$ of $Q_T$ on $\{0, \dots, Q\}$ together with allocation probabilities $a(q) = \Pr\{\mathcal A \mid Q_T = q\} \in [0,1]$, $a(0) = 0$, where $\mathcal A$ is the event that the customer is allocated a unit. It is determined by the other customers' strategies, which are arbitrary.

With $\delta = e^{-\alpha(T-t)}$, the expected surplus of waiting of a customer with current valuation $\psi$ is

$$W_t(\psi) = \mathrm E_{Q_T}\!\left[\max\{\psi\delta - p_2(Q_T), 0\}\cdot \mathbf 1\{\mathcal A \mid Q_T\}\right] = \sum_{q=0}^{Q}\pi(q)\,a(q)\,\max\{\psi\delta - p_2(q), 0\}.$$

The paper's purchase rule (p. 344): buy immediately iff the current surplus $V(t) - p_1$ is nonnegative and at least $W_t(V(t))$.

Formalization targets

Goal: Theorem 1 and Corollary 1

Assume $p_1 \ge 0$, and $\alpha > 0$ or $\sum_q \pi(q)a(q) < 1$. For every $t \in [0,T)$ the equation

$$\psi - p_1 = W_t(\psi) \tag{2}$$

has a unique solution $\psi(t) \ge p_1$; a customer arriving at $t$ buys immediately under the purchase rule if and only if $V(t) \ge \psi(t)$; and the threshold function $\psi : [0, T) \to [p_1, \infty)$ is nondecreasing in $t$.

Milestones

1. The right-hand side of (2) is nonnegative and nondecreasing in $\psi$, with increments bracketed by $\delta\,\Pr\{\psi\delta \ge p_2(Q_T), \mathcal A\}$ at the two endpoints, and this slope is below one.
2. Equation (2) has a unique solution $\psi \ge p_1$.

Significance

Theorem 1 reduces a customer's strategy, a function of arrival time and valuation, to one threshold function $\psi$ on $[0, T)$. The segment sizes $\Lambda_I, \Lambda_S, \Lambda_W, \Lambda_L$ of §4.2, the seller's menu problem (3), the equilibrium iteration (4) and the closed form of Proposition 2 are all written in terms of $\psi$; without Theorem 1 none of them is defined. Corollary 1, that the threshold rises toward the markdown, is what the paper calls "useful in our analyses below"; the customer segments of Figure 1 are drawn with it.

The result is proved in the paper, with a short appendix argument. No machine-checked version exists. The mission produces a formal statement and proof of the reduction for an arbitrary belief, which fixes the exact hypotheses under which it holds: the paper's slope bound needs either valuation decline ($\alpha > 0$) or imperfect availability, and the monotonicity of the threshold needs a nonnegative premium price. A formal $W_t$ and threshold are the starting point for formalizing the equilibrium and pricing results of the paper.

Difficulty

The mathematics is one-dimensional. The difficulty is in stating it exactly. $W_t$ is piecewise linear with a kink wherever $\psi\delta$ crosses a menu price, so the paper's derivative is only a one-sided derivative, and the uniqueness argument has to use increments. The paper's bound "slope $< 1$" is false when $\alpha = 0$ and a unit is allocated with certainty; then (2) has either no finite solution or a half-line of them. The threshold's monotonicity in $t$ rests on $W_t(\psi)$ increasing in $t$ for fixed $\psi$, which needs $\psi \ge 0$; with a negative premium price the threshold can decrease. The naive reading of "optimal to use a threshold" as an abstract fixed-point fact about any monotone function with slope below one discards the model and is not the goal.

Formalization scope

Lean namespace SeasonalPricing.Contingent. Time, prices and valuations are real numbers. The belief is a pair pmf alloc : ℕ → ℝ restricted to {0, …, Q} (IsInventoryBelief), not a random variable on a probability space; only the law of $(Q_T, \mathbf 1\{\mathcal A\})$ enters (2). The menu is p2 : ℕ → ℝ with $p_2(q) \le p_1$ required on $\{1, \dots, Q\}$ only; $p_2(0)$ never matters because $a(0) = 0$. The belief does not depend on the arrival time, as in Eq. (4) of the paper. waitingSurplus is $W_t$ with $e^{-\alpha(T-t)}$ written Real.exp (-(α * (T - t))); buysNow is the purchase rule, stated on the current valuation $V(t)$.

Readings of the paper's words:

• "the unique solution" of (2): existence and uniqueness of a real $\psi \ge p_1$ (∃!). The paper's "$\psi \in [p_1, \infty]$" includes $\infty$ only in the case excluded by the added hypothesis.
• "it is optimal to base purchasing decisions on a threshold function": the purchase rule of p. 344 holds exactly when $V(t) \ge \psi(t)$.
• "derivative … $< 1$": a two-sided bracket on increments of $W_t$, with right slope $\delta\Pr\{\psi\delta \ge p_2(Q_T), \mathcal A\}$, below one.
• "increasing" (Corollary 1): nondecreasing (MonotoneOn), since $\psi$ is constant on an initial interval whenever no menu price is reachable (p. 347).

Added hypotheses, both named in the statements: $\alpha > 0$ or $\sum_q \pi(q)a(q) < 1$, the one hypothesis the paper's proof uses without stating it; and $p_1 \ge 0$, the model's convention that prices are nonnegative. Only the branch $0 \le t < T$ of the threshold $\theta$ is stated: for $t \ge T$ the paper's $\theta(t) = p_2$ is the model's rule for late customers. The belief enters through the explicit sum; a formalization with an unspecified monotone $W$, or with $\psi(t)$ defined by choice inside a definition, is not the target.

No new library is needed beyond finite sums, max and Real.exp. A lemma on unique roots of $\psi \mapsto \psi - c - f(\psi)$ for $f$ with increments bounded by $k(\psi' - \psi)$, $k < 1$, is reusable. Proofs of the milestones and the goal, in any order, are welcome.

Selected references

• Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• X. Su, Intertemporal Pricing with Strategic Customer Behavior, Management Science 53(5):726–741, 2007. https://doi.org/10.1287/mnsc.1060.0667
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999

Motivation

Retailers of fashion and seasonal goods sell at a premium price early in the season and mark down later. When customers anticipate the markdown, some of them wait, and the seller's pricing problem becomes a game between the seller and a population of forward-looking (strategic) customers. Aviv and Pazgal (MSOM 10(3), 2008) study this game in a model with limited inventory, stochastic arrivals and valuations that decline over the season, under two classes of seller policies: contingent pricing, where the discount depends on the inventory left, and announced fixed-discount pricing, where the seller commits to both prices upfront. Their numerical study (§7.3) compares the two classes and finds that precommitment can raise expected revenue by up to about 8%.

That comparison needs, for every announced price path, the customers' equilibrium response. Theorem 2 of the paper (p. 348) supplies it: a threshold purchasing policy, pinned down by a scalar fixed-point equation for the probability that a waiting customer is served. This mission formalizes Theorem 2. A companion mission of the same series formalizes Theorem 1, the contingent-pricing counterpart.

Setting

A seller has $Q \ge 1$ units to sell over a season $[0, H]$, split at a fixed time $T$ with $0 < T \le H$. Customers arrive by a Poisson process with rate $\lambda > 0$. Customer $j$ has a base valuation $V_j$ drawn from a continuous distribution $F$ (tail $\bar F = 1 - F$), and at time $t$ values the product at $V_j(t) = V_j e^{-\alpha t}$, where the decline factor $\alpha \ge 0$ is common to all customers.

Under an announced price path the seller commits to a premium price $p_1$ on $[0, T)$ and a discount price $p_2 \le p_1$ from $T$ on; $p_2$ does not depend on the remaining inventory. Customers know the initial inventory but not the current one.

A customer arriving at $t < T$ buys immediately if and only if (i) the current surplus $V(t) - p_1$ is nonnegative and (ii) it is at least the expected surplus of waiting,

$$\omega\cdot\max\{V(T) - p_2, 0\},$$

where $\omega$ is the probability that a unit will be allocated to the customer at time $T$. Units left at $T$ are rationed at random among the customers who request one.

For a threshold function $\psi$ on $[0, T)$ the paper defines three segment rates: $\Lambda_I(\psi)$, the expected number of customers who buy at $p_1$; $\Lambda_S(\psi, p_1, p_2)$, those who could buy at $p_1$ but wait and want to buy at $p_2$; and $\Lambda_W(p_1, p_2)$, those whose valuation was below $p_1$ and who want to buy at $p_2$. Each is $\lambda$ times an integral over $[0, T]$ of $\bar F$ at scaled prices (p. 345). With $P(x \mid \Lambda)$ the Poisson probabilities, the allocation probability of $q$ units is

$$A(q \mid \Lambda) = \sum_{y=0}^{\infty} \frac{q}{\max\{1+y, q\}}\,P(y \mid \Lambda).$$

Formalization targets

Goal: Theorem 2 (p. 348)

For $w \in [0,1]$ let

$$\psi_A(t) = \max\left\{p_1, \frac{p_1 - wp_2}{1 - we^{-\alpha(T-t)}}\right\},\qquad 0 \le t < T, \tag{7}$$

and suppose $w$ solves

$$w = \sum_{x=0}^{Q-1} P\big(x \mid \Lambda_I(\psi_A)\big)\cdot A\big(Q-x \mid \Lambda_S(\psi_A, p_1, p_2) + \Lambda_W(p_1, p_2)\big). \tag{8}$$

Then, when all other customers use $\psi_A$ (so that a waiting customer is served with the probability on the right of (8)), every customer arriving at $t \in [0, T)$ buys immediately if and only if $V(t) \ge \psi_A(t)$: the symmetric threshold profile is a Nash equilibrium.

Milestones: the two cases of the proof (p. 358)

1. If $e^{-\alpha(T-t)} \le p_2/p_1$, the threshold is $p_1$.
2. If $e^{-\alpha(T-t)} > p_2/p_1$, the threshold is $(p_1 - wp_2)/(1 - we^{-\alpha(T-t)}) \ge p_1$.

Significance

Theorem 2 reduces the customers' equilibrium under an announced path to a single scalar $w$. Everything downstream in §5 and §7 rests on it: the seller's expected revenue $\pi_{A/S}(p_1, p_2)$ (p. 348) is written in terms of $\psi_A$, the seller's optimal announced path maximizes it, and the comparison between announced and contingent pricing uses the resulting value $\pi^*_{A/S}$. The theorem also explains the qualitative prediction of the model: the threshold exceeds $p_1$ exactly when the announced discount is deep relative to the decline of valuations, and it rises with the perceived availability $w$.

The result is proved in the paper; to the best of our search it has no machine-checked proof. A formal development contributes the model objects (segment rates for threshold policies, the allocation probability for random rationing among Poisson requesters) in a form reusable by the rest of the series and by other strategic-customer pricing models, and a checked proof of the equilibrium property. The existence of a solution to (8) is not proved in the paper and is a natural further target.

Difficulty

The best-response part of the argument is elementary once the availability is known. The substance of the statement lies in the availability itself: the probability that a waiting customer is served is not a free parameter but the one generated, through (8), by the other customers' use of the same threshold. A formalization must connect the segment rates, the Poisson counts and random rationing into one expression and keep the fixed-point coupling between $w$ and $\psi_A$ intact; dropping it turns the theorem into a one-line inequality about an arbitrary $w$. The division by $1 - we^{-\alpha(T-t)}$ also degenerates when $w = 1$ and $\alpha = 0$, and has to be excluded explicitly.

Formalization scope

The Lean development lives in namespace SeasonalPricing.Announced. Conventions:

• Time is real; base valuations have law μ : Measure ℝ with IsProbabilityMeasure μ, $F$ = ProbabilityTheory.cdf μ, and continuity of $F$ (the paper's "continuous distribution") is a hypothesis of the goal. No support condition on $[0,\infty)$ is imposed; the statement quantifies over every real base valuation $V$.
• $\Lambda_I, \Lambda_S, \Lambda_W$ are interval integrals over $[0, T]$ exactly as printed. $P(x \mid \Lambda) = e^{-\Lambda}\Lambda^x/x!$ is written out; $A(q\mid\Lambda)$ is the infinite series (tsum) as printed, not its closed form.
• availability is the right-hand side of (8), with $\psi_A$ built from $w$ by (7).

Readings of the paper's informal words:

• "Nash equilibrium" is read as the best-response property the paper's proof checks: against the availability generated by (8), the immediate-purchase rule of p. 344 coincides with the threshold $\psi_A$ at every $t \in [0, T)$ and every valuation. The paper defines no strategy space beyond threshold rules.
• "$w$ is a solution to (8)": the theorem is conditional on a solution; its existence is neither assumed elsewhere nor claimed. The conditional statement has content only when (8) has a solution, which the paper does not prove.
• $w$ as a likelihood: $0 \le w \le 1$ is a hypothesis (it also follows from (8)).
• Added hypothesis: $\alpha > 0$ or $w < 1$, which keeps $1 - we^{-\alpha(T-t)} > 0$ for $t < T$; the paper's formula is undefined when it fails. In the milestones the same condition appears as $we^{-\alpha(T-t)} < 1$, and $0 < p_1$ is added so that $p_2/p_1$ is meaningful.
• The rule on $[T, H]$ (buy at $T$ iff $V(T) > p_2$) is part of the model and is not restated; $H$ does not enter the statements.

A formalization in which $w$ is an arbitrary number in $[0,1]$, not tied to (8), is ruled out: it is the best-response lemma alone, not Theorem 2. Contributions welcome: proofs of the two milestones and the goal; lemmas such as $0 \le A(q\mid\Lambda) \le 1$ and summability of its series; the closed form of $A(q \mid \Lambda)$ printed on p. 346; and an existence result for (8).

Selected references

• Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• X. Su, Intertemporal Pricing with Strategic Customer Behavior, Management Science 53(5):726–741, 2007. https://doi.org/10.1287/mnsc.1060.0667

Motivation

Retailers of seasonal goods (fashion, electronics, holiday items) sell a fixed stock over a short season and routinely cut prices toward its end. A markdown of this kind segments the market over time: customers with high valuations buy early at a premium price, and customers with lower valuations are served later at a discount price. Aviv and Pazgal (MSOM 2008) study how much such two-price schemes are worth when customers arrive over time, differ in their valuations, and may or may not anticipate the discount.

To measure the value of price segmentation, the paper compares every two-price scheme with the best fixed-price policy, a single price held for the whole season. Its benchmark is the case of myopic customers, who never delay a purchase strategically. Proposition 3 of the paper computes this benchmark in closed form in the simplest nontrivial setting: exponentially distributed valuations that do not decline over the season, and unlimited inventory. The resulting formula explains the pattern of the paper's Table 1, where the benefit of segmentation grows with the heterogeneity of valuations and with a late discount time.

Setting

A seller offers a product during the season $[0, H]$; throughout this mission $H = 1$, so time is measured as a fraction of the season. Customers arrive as a Poisson process with rate $\lambda > 0$. Customer $j$ has a base valuation $V_j$ drawn independently from a distribution $F$ with tail $\bar F(x) = 1 - F(x)$, and values the product at $V_j e^{-\alpha t}$ at time $t$, where $\alpha \ge 0$ is the decline factor. The paper reparametrizes it as $\rho = e^{-\alpha H}$, the fraction of the base valuation left at the end of the season.

In the numerical study, $F$ is a Gamma law with mean $\mu$ and coefficient of variation $c$ (standard deviation over mean): shape $1/c^2$ and rate $1/(\mu c^2)$. The paper sets $\mu = 1$. For $c = 1$ this is the exponential law with mean one, $\bar F(x) = e^{-x}$ for $x \ge 0$.

A contingent two-price policy posts the premium price $p_1$ on $[0, T)$, where $0 < T \le 1$ is fixed, and a discount price $p_2 \le p_1$ from time $T$ on. A myopic customer arriving at $t < T$ buys at $p_1$ if his valuation is at least $p_1$; otherwise he waits and buys at $T$ if his valuation is then at least $p_2$. Customers arriving at or after $T$ buy if their valuation is at least $p_2$. The numbers of customers in these groups are Poisson with means

$$\Lambda_I(p_1) = \lambda\int_0^T \bar F(p_1 e^{\alpha t})\,dt, \quad \Lambda_W(p_1,p_2) = \lambda\int_0^T \big[\bar F(\min\{p_1e^{\alpha t}, p_2e^{\alpha T}\}) - \bar F(p_1e^{\alpha t})\big]dt, \quad \Lambda_L(p_2) = \lambda\int_T^H \bar F(p_2e^{\alpha t})\,dt .$$

With unlimited inventory, the expected revenue of the policy is

$$R_{C/N}(p_1, p_2) = p_1\Lambda_I(p_1) + p_2\big(\Lambda_W(p_1,p_2) + \Lambda_L(p_2)\big),$$

and the expected revenue of a single price $p$ is $R_F(p) = p\,\lambda\int_0^H \bar F(p e^{\alpha t})\,dt$ (Eq. (9) of the paper). The optimal values are $\pi^*_{C/N} = \max_{p_2 \le p_1} R_{C/N}(p_1,p_2)$ and $\pi^*_F = \max_p R_F(p)$.

Formalization targets

Goal: Proposition 3

Suppose $c = 1$, $\rho = 1$ and $Q/\lambda \to \infty$ (unlimited inventory), with $\mu = 1$ and $H = 1$. Then

$$\pi^*_{C/N} = (\lambda e^{-1})\cdot e^{T/e} = \pi^*_F \cdot e^{T/e}.$$

Both maxima are attained. The goal states the two optimal values; it does not fix the optimal prices.

Milestones from the paper's proof

1. The reduced problem: for $0 \le p_2 \le p_1$, $R_{C/N}(p_1,p_2) = p_2\cdot\lambda e^{-p_2} + (p_1-p_2)\cdot\lambda T e^{-p_1}$.
2. Its solution: over $p_2 \le p_1$ the maximum is $\lambda e^{-1+T/e}$, attained exactly at $p_1^* = 2 - T/e \ge 1$, $p_2^* = p_1^* - 1 \le 1$.
3. The fixed-price optimum (a supporting item of the goal, stated in the proof on pp. 358–359): $p^* = \mu = 1$ is the unique optimal single price and $\pi^*_F = \lambda e^{-1}$.

Significance

Proposition 3 gives the relative benefit of contingent pricing over a single price, $e^{T/e} - 1$, as a function of the discount time alone. It increases in $T$ and is largest at $T = 1$, where it equals $e^{1/e} - 1 \approx 44.46\%$. This is the paper's analytic anchor for its numerical findings: segmentation is most valuable when valuations are heterogeneous and customers are carried to the discount at little cost, and a late discount exposes more customers to the premium price. Under strategic customers the same quantity serves as an upper bound on the benefit of segmentation (§6.1 of the paper).

The result is proved in the paper, in a short appendix argument that states the reduced problem and its solution without the calculus. No machine-checked version exists. Formalizing it produces a reusable Lean encoding of the paper's segment rates $\Lambda_I, \Lambda_W, \Lambda_L$ as integrals of a valuation tail, a Gamma valuation law through Mathlib's gammaMeasure, and a complete verification that the integral model reduces to the two-variable problem and that the stated prices are its unique maximizer.

Difficulty

The obvious route is to write the revenue in closed form and set the gradient to zero. Two steps of that route are not automatic. First, the reduction requires evaluating the three integrals with the piecewise tail of the exponential law, including the $\min$ inside $\Lambda_W$, and the reduced formula is valid only for nonnegative prices; negative prices must be handled separately in the model itself, where the tail equals one. Second, the reduced objective $p_2\lambda e^{-p_2} + (p_1-p_2)\lambda T e^{-p_1}$ is not concave on the region $p_2 \le p_1$, so a stationary point is not automatically a global maximizer, and the boundary $p_2 = p_1$ and unbounded directions have to be ruled out. Uniqueness of the maximizer, which the paper asserts, fails at $T = 0$ and needs $T > 0$.

Formalization scope

All declarations sit in the namespace SeasonalPricing.MyopicExp. Time, prices and rates are real numbers. The season is $[0, 1]$ with $0 < T \le 1$ and $\lambda > 0$. Integrals are interval integrals. The valuation tail is gammaValuationTail μ c x = 1 - cdf (gammaMeasure (1/c^2) (1/(μ c^2))) x, used at $\mu = c = 1$. The hypothesis $\rho = 1$ is decayRatio α 1 = 1 with $\alpha \ge 0$.

Readings of the paper's informal words:

• "$Q/\lambda \to \infty$" is read as unlimited inventory: the truncated Poisson mean $N(q,\Lambda)$ of §4.2 is replaced by $\Lambda$ and stock-outs never occur. This is what the proof computes, what p. 348 writes as $Q = \infty$, and what §7.1 calls inventory that is "practically unlimited". A limit of finite-inventory optimal revenues is not stated.
• "max" is an attained maximum (IsGreatest), not a supremum.
• The optimum is taken over all real prices with $p_2 \le p_1$, as printed; the paper never restricts signs, and negative prices are never optimal in the model.
• The seller's discount at $T$ is a best response to $p_1$ in the paper ($R(q \mid p_1)$, p. 349). With unlimited inventory it does not depend on the realized sales, and the nested maximum equals the joint maximum over $(p_1, p_2)$, which is what the goal states.
• "The solution … is" (milestone 2) and "the optimal single price is given by $p^* = \mu = 1$" (the fixed-price item) are read as unique maximizers.

The Gamma density printed on p. 349 has the exponent $1/(sc^2-1)$, a misprint for $1/c^2 - 1$; at $c = 1$ the exponent is $0$ either way.

A trivializing formalization would state the goal on the reduced two-variable function, dropping the model: the goal here is about $R_{C/N}$ built from $\Lambda_I, \Lambda_W, \Lambda_L$ and the Gamma tail, and about $R_F$ built from Eq. (9). The platform's BuyingToBundle.monopolyRevenue (definition monopoly_pricing) is a related object, $\sup_p p\,\nu([p,\infty))$; with $\rho = 1$ and $H = 1$, $\pi^*_F$ equals $\lambda$ times it for the exponential law, but it is a supremum without arrivals or time and is not reused.

Contributions welcome: closed forms of the segment rates for the exponential tail, a general lemma that negative prices are dominated, and the two-variable maximization.

Selected references

• Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• D. Besanko and W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999

Motivation

A make-to-stock manufacturer who also sells on a spot market must decide, at every moment, whether to keep producing and whether to accept or reject incoming orders at the prevailing price. Caldentey and Wein (Revenue Management of a Make-to-Stock Queue, Operations Research 54(5), 2006) study this problem in heavy traffic. The limit is a two-dimensional singular control problem for a diffusion: the inventory level and the logarithm of the price move jointly as a correlated Brownian motion, and the controls push the inventory only when it reaches one of two free boundaries. The optimal boundaries are characterized by an elliptic free-boundary problem that the authors could not solve in closed form.

The paper's way forward is an approximation: change the direction of reflection on the boundary so that the stationary distribution of the controlled process becomes an explicit exponential. Proposition 2 states that exponential form, and it turns the free-boundary problem into a calculus-of-variations problem for the two boundary curves. Explicit stationary densities of reflected diffusions in two dimensions are rare; the classical condition for an exponential stationary density of a reflected Brownian motion, and the characterization of the stationary law by a basic adjoint relation, are due to Harrison and Williams, Multidimensional reflected Brownian motions having exponential stationary distributions, Annals of Probability 15, 1987, the reference the paper cites. This mission formalizes the analytic core of Proposition 2: the exponential density satisfies that relation for the reflection field the proposition singles out.

Setting

Points of the plane are $(x,y)$, with $x$ the inventory level and $y$ the logarithm of the price. The limiting process $(\mathcal X,\mathcal Y)$ has drift $(\theta,0)$ and covariance matrix

$$\Sigma=\begin{pmatrix}\sigma^2&\sigma\delta\varrho\\ \sigma\delta\varrho&\delta^2\end{pmatrix},\qquad \sigma>0,\ \delta>0,\ -1<\varrho<1,$$

so its generator is

$$\Gamma=\theta\frac{\partial}{\partial x}+\frac{\sigma^2}{2}\frac{\partial^2}{\partial x^2}+\sigma\delta\varrho\frac{\partial^2}{\partial x\,\partial y}+\frac{\delta^2}{2}\frac{\partial^2}{\partial y^2}.$$

Two curves bound the region where the process lives: the rejection boundary $x=\eta(y)$ (below it, orders are rejected) and the idleness boundary $x=\xi(y)$ (above it, production stops). For $y_{\min}<y_{\max}$ the region is

$$\Omega=\{(x,y):\ y_{\min}<y<y_{\max},\ \eta(y)<x<\xi(y)\},$$

and its boundary splits into four pieces: $x=\eta(y)$, $x=\xi(y)$, $y=y_{\min}$, $y=y_{\max}$. Write $\vec n$ for the inward unit normal on $\partial\Omega$ and $dl$ for arc length. A reflection field $\vec v$ on $\partial\Omega$ gives the direction in which the process is pushed back into $\Omega$. The basic adjoint relation (BAR) of the paper, equation (43), is

$$\int_\Omega \Gamma f\,\pi_\Omega\,ds+\frac12\int_{\partial\Omega}\vec v\cdot\nabla f\,\pi_\Omega\,dl=0\quad\text{for all test functions } f,$$

and the paper cites Harrison and Williams for the fact that the stationary distribution $\pi_\Omega$ of the reflected process satisfies it. Proposition 2 introduces the eigen-decomposition $\Sigma=V'EV$ ($V$ a rotation whose rows are eigenvectors, $E$ diagonal), the whitening map $T=E^{-1/2}V$ and $\Omega^*=T(\Omega)$, and assumes that $T\vec v$ is normal to $\partial\Omega^*$. The exponents are

$$m_x=\frac{2\theta}{\sigma^2(1-\varrho^2)},\qquad m_y=\frac{-2\varrho\theta}{\sigma\delta(1-\varrho^2)}.\tag{47}$$

Formalization targets

Goal: the exponential density satisfies the BAR under conormal reflection

For $\eta,\xi$ continuously differentiable with $\eta<\xi$ on $[y_{\min},y_{\max}]$, $\pi(x,y)=e^{m_xx+m_yy}$, and every $C^2$ function $f$ on $\mathbb R^2$,

$$\int_\Omega \Gamma f\;\pi\,ds+\frac12\int_{\partial\Omega}(\Sigma\vec n)\cdot\nabla f\;\pi\,dl=0 .$$

The boundary integral is written out on the four pieces, with $\vec n\,dl$ equal to $(1,-\eta'(y))\,dy$, $(-1,\xi'(y))\,dy$, $(0,1)\,dx$ and $(0,-1)\,dx$ respectively. The normalizing constant is left out because the relation is linear in $\pi$.

Milestones

1. The interior equation: $\Gamma^*\pi=-\theta\pi_x+\frac{\sigma^2}{2}\pi_{xx}+\sigma\delta\varrho\,\pi_{xy}+\frac{\delta^2}{2}\pi_{yy}=0$ everywhere.
2. The zero-flux identity: $\frac12\Sigma\nabla\pi=(\theta,0)\,\pi$ everywhere.
3. The meaning of the hypothesis: with $T=E^{-1/2}V$, $(Tv)\cdot(Tw)=v\cdot\Sigma^{-1}w$, and for $n\neq0$, $Tv$ is orthogonal to $T$ of every vector orthogonal to $n$ exactly when $v$ is a multiple of $\Sigma n$.
4. The normalizing constant: $\pi$ is integrable on $\Omega$ and a unique $K_\Omega>0$ makes $K_\Omega\pi$ integrate to one.

Significance

For the operations model, Proposition 2 is what makes the problem computable. Once the stationary density is explicit, the long-run average cost of any pair of boundary curves is an explicit integral, and optimizing over $(\eta,\xi)$ becomes a variational problem with Euler–Lagrange equations; the paper's proposed policy and its numerical comparisons all rest on it.

For formalization, the mission produces a machine-checked version of a statement whose proof the paper does not contain (it is in an online companion) and whose hypothesis is stated only in words. The formal statements fix exactly which reflection field makes the claim true, which the prose leaves ambiguous. None of the statements has, to our knowledge, a machine-checked proof anywhere; the result itself is classical in spirit (an integration by parts on a planar region), but no divergence theorem on a region between two graphs with an anisotropic operator is currently available as a ready-made statement.

Difficulty

The interior equation and the zero-flux identity are finite computations with the exponential. The difficulty is the goal: it is an integration-by-parts identity on a curved planar region with an anisotropic second-order operator. The obvious first step, "apply Green's identity", presupposes a divergence theorem on a region bounded by two graphs $x=\eta(y)$, $x=\xi(y)$ and two horizontal segments, with the boundary integral written in the parametrization of each piece and the orientation of every normal tracked. Mathlib has the divergence theorem on rectangular boxes, not on such regions, and the moving limits $\eta(y)$, $\xi(y)$ are exactly where the terms in $\eta'$ and $\xi'$ of the boundary integral come from.

The second trap is the reflection field. The page describes the modification as substituting the inward unit normal $\vec n$ for $\vec v$; with $\vec v=\vec n$ the identity is false as soon as $\Sigma$ is not a multiple of the identity (on a random instance the residual is of order one). Only the conormal field $\Sigma\vec n$, which is what the hypothesis of Proposition 2 selects, gives a true statement.

Formalization scope

Everything lives in the namespace MakeToStockRM.ExpDensity. The plane is ℝ × ℝ with the inventory first; partial derivatives are Fréchet derivatives applied to (1, 0) and (0, 1), and the mixed partial is $\partial_x(\partial_y f)$. Parameters satisfy $\sigma>0$, $\delta>0$, $|\varrho|<1$; $\theta$ is any real number, and $\theta=0$ (then $\pi\equiv1$) is allowed.

This is the analytic, pinned-down content of Proposition 2. The identification "the BAR characterizes the stationary law of the reflected diffusion" (Harrison–Williams 1987) is out of scope: Mathlib has no reflected Brownian motion. Relative to the page, the formalization commits to the following:

• The reflection field is $\vec v=\Sigma\vec n$ with $\vec n$ the inward unit normal and $dl$ arc length. The hypothesis "$T\vec v$ is normal to $\partial\Omega^*$" fixes only the direction of $\vec v$ (milestone 3); the length $\Sigma\vec n$ is the one for which the BAR holds. The page's phrase "substituting the inward unit normal $\vec n$ for $\vec v$" is inconsistent with the proposition's own hypothesis and is not followed.
• The boundary curves are $C^1$ on $\mathbb R$ with $\eta<\xi$ on $[y_{\min},y_{\max}]$, and $y_{\min}<y_{\max}$, so $\Omega$ is a nonempty bounded region; the paper assumes this implicitly.
• Test functions are all $C^2$ functions on $\mathbb R^2$, which are bounded with bounded derivatives on the closure of $\Omega$ (the paper's "twice continuous and bounded").
• The constant $K_\Omega$ is dropped from the goal and treated in milestone 4.

The goal quantifies over every $C^2$ test function; restricting to functions supported inside $\Omega$ would delete the boundary term and reduce the goal to milestone 1, and that trivialization is ruled out. The second half of Proposition 2 ("(45)–(46) is equivalent to (48)–(49)"), Proposition 1, the heavy-traffic limit, the HJB equation and the proposed policy are not formalized: their normalizations or proofs are only in the online companion.

A complete development needs a divergence theorem on regions between two $C^1$ graphs, which is reusable for any planar PDE statement on such regions. Contributions of that lemma, and of the four milestones, are welcome.

Selected references

• R. Caldentey, L. M. Wein, Revenue Management of a Make-to-Stock Queue, Operations Research 54(5):859–875, 2006. https://doi.org/10.1287/opre.1060.0289
• J. M. Harrison, R. J. Williams, Multidimensional reflected Brownian motions having exponential stationary distributions, Annals of Probability 15(1):115–137, 1987. https://doi.org/10.1214/aop/1176992259
• F. John, Partial Differential Equations, 4th ed., Springer, 1982. https://doi.org/10.1007/978-1-4684-9333-7