Operations Research

Motivation

Airlines, hotels and rail operators sell many products (itinerary–fare combinations) that share scarce capacity. When customers choose among whatever is on offer, the seller's lever is the offer set: the subset of products made available at each moment. Choice-based network revenue management, as set up by Liu and van Ryzin (2008), optimizes over offer sets through the choice-based deterministic linear program (CDLP), whose columns are indexed by all $2^n$ subsets of the $n$ products. Solving it by column generation requires, at every iteration, a subproblem that picks the best offer set against the current dual prices; the paper's decomposition heuristic needs subproblems of the same form.

For a general choice model this subproblem is a hard combinatorial optimization. Under the multinomial logit (MNL) model with disjoint customer segments it separates by segment, and each segment's problem is solved by ranking the products. This observation is the reason the CDLP is computationally practical under MNL, and it is the content of Proposition 6 of the paper. The same structural fact, that under MNL the optimal assortment is revenue-ordered, was shown by Gallego, Iyengar, Phillips and Dubey (2004) and is related to the single-leg analysis of Talluri and van Ryzin (2004). It underlies a large later literature on assortment optimization.

Setting

Fix one customer segment. Its consideration set is a finite set $\iota$ of products, of size $s$. Each product $j \in \iota$ has an MNL preference weight $v_j > 0$, and not buying has a no-purchase weight $v_0 \ge 0$. When the set $S \subseteq \iota$ is offered, a customer of the segment buys $j \in S$ with probability

$$P_j(S) = \frac{v_j}{\sum_{i \in S} v_i + v_0}.$$

Each product also carries a real score $w_j$; in the paper's application $w_j = r_j - \pi^\top A_j$ is the product's revenue minus the dual prices of the legs it uses, so $w_j$ may be negative. The expected score per customer when $S$ is offered is

$$f(S) = \frac{\sum_{j \in S} w_j v_j}{\sum_{j \in S} v_j + v_0},$$

and the offer-set problem (the paper's (14)) is $\max_{S \subseteq \iota} f(S)$. The paper writes offer sets as binary vectors $y \in \{0,1\}^s$ with $y_j = 1$ iff $j$ is offered; the formalization uses subsets.

The paper's proof passes through the relaxation (17): with $z_j = v_j y_j$ allowed to range over the whole interval $[0, v_j]$, maximize

$$h(z) = \frac{\sum_j w_j z_j}{\sum_j z_j + v_0}$$

over the box $\mathcal{D} = [0, v_1] \times \cdots \times [0, v_s]$. When $v_0 = 0$ the paper sets $h(0) := 0$ (and likewise $f(\emptyset) = 0$).

In Lean, mnlObjective v w v₀ S is $f(S)$ and relaxedObjective w v₀ z is $h(z)$; the box is Set.Icc 0 v in the componentwise order.

Formalization targets

Goal: Proposition 6, the top-ranked products are an optimal offer set

Assume $v_j > 0$ for all $j$, $v_0 \ge 0$, and that some score is nonnegative. Then there is a product $k \in \iota$ such that

$$f(S) \;\le\; f\bigl(\{ j \in \iota : w_j \ge w_k \}\bigr) \qquad \text{for every } S \subseteq \iota.$$

Here $w_k$ is the paper's $w_{[k^*]}$, the $k^*$-th largest score; the threshold set contains every product tied with it.

Milestones (all from the Appendix, proof of Proposition 6, p. 309)

1. Claim (17). The relaxation has the same optimal value: $\max_{z \in \mathcal{D}} h(z) = \max_{S \subseteq \iota} f(S)$, both maxima attained.
2. Quasiconvexity. $h$ is quasiconvex on $\mathcal{D}$, including the case $v_0 = 0$ with $h(0) := 0$.
3. Nested relaxed optimum. If $w_1 \ge \cdots \ge w_s$ and some $w_i \ge 0$, there is $1 \le i^* \le s$ such that $z^* = (v_1, \dots, v_{i^*}, 0, \dots, 0)$ is an optimal solution of the relaxation.

Significance

The result. Proposition 6 reduces a search over $2^s$ offer sets to a search over at most $s$ nested sets, one per possible threshold. Under MNL with disjoint segments, it lets the CDLP column-generation subproblem, and the inner offer-set problems of the leg-level dynamic programs in the decomposition heuristic, be solved by checking at most $s$ candidate sets per segment, $s$ being the size of the segment's consideration set. Revenue-ordered assortments are the reference point against which later models (nested logit, mixtures of logits, constrained assortments) are measured.

Formalizing it. The proposition is proved on paper, twice (Gallego et al. 2004; Liu and van Ryzin 2008, Appendix), and no machine-checked version is known to the platform. The mission produces a checked statement of the ranking property with its hypotheses made exact, including the case the printed statement gets wrong (see below), and the supporting facts about the linear-fractional relaxation: that the box relaxation loses nothing, and that its objective is quasiconvex. These facts about ratios of affine functions over boxes are reusable beyond revenue management, for instance in fractional combinatorial optimization.

Difficulty

The objective is a ratio, so neither the numerator nor the denominator can be optimized alone, and adding a product with a positive score can lower $f$ by diluting the probability mass of better products. The optimal threshold is not a fixed number such as $0$: it depends on the optimal value itself. A proof must therefore relate every one of the $2^s$ offer sets to a threshold set without enumerating them. Ties among scores, ties between a score and the optimal value, and the degenerate case $v_0 = 0$ (where the denominator vanishes at the empty offer set) all have to be handled; in the relaxation, ties make interior points optimal, so an argument that every optimum is a vertex of the box is false.

Formalization scope

• Offer sets are subsets S : Finset ι of a finite type ι (the consideration set); the binary vectors of the paper correspond one-to-one. The milestone on sorted scores uses Fin s with Antitone w, so indices are 0-based and $i^*$ is an element of Fin s.
• Ranking. The goal does not formalize a sorting permutation: "$w_j \ge w_{[k^*]}$ for some $1 \le k^* \le s$" is stated as "$w_j \ge w_k$ for some product $k$". With ties this is exactly the printed rule; it is not "the first $k^*$ products of a chosen sort order", which differs under ties.
• Optimality means "is an optimal solution": the chosen set (or point) is compared with every $S \subseteq \iota$ (every $z \in \mathcal{D}$). Uniqueness is not claimed, since ties produce several optima.
• Division by zero. $v_0 = 0$ is allowed, as in the paper's numerical study; the only zero denominator is at $S = \emptyset$ (or $z = 0$), where Lean's $0/0 = 0$ implements the paper's convention $h(0) := 0$.
• Repair. As printed, Proposition 6 (and the nested optimum in its proof) requires $1 \le k^*$, i.e. a nonempty offer set, and is false when every score is negative: for $s = 1$, $w_1 = -1$, $v_1 = v_0 = 1$, the empty set has value $0$ and the only admissible set has value $-1/2$. Such scores occur in the paper's own application. The goal and milestone 3 therefore add the hypothesis that some score is nonnegative. The hypothesis is not strengthened to "all scores nonnegative", which would exclude the cases the column-generation subproblem actually meets.
• Ruling out trivializations. The objective is the full MNL ratio with $v_0$ in the denominator, the comparison ranges over every subset (not only threshold sets), and the consideration set is arbitrary, so the goal cannot be discharged by checking nested sets against each other or by a special case.
• Infrastructure. Mathlib's QuasiconvexOn (and QuasilinearOn) and Finset sums suffice; there is no Mathlib lemma on quasiconvexity of linear-fractional functions, which milestone 2 would supply. Proofs of any milestone, and alternative routes to the goal that bypass the relaxation, 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. doi:10.1287/msom.1070.0169
• G. Gallego, G. Iyengar, R. Phillips, A. Dubey. Managing flexible products on a network. CORC Technical Report TR-2004-01, Columbia University, 2004. CORC technical reports
• K. Talluri, G. van Ryzin. Revenue management under a general discrete choice model of consumer behavior. Management Science 50(1):15–33, 2004. doi:10.1287/mnsc.1030.0147
• M. Avriel. Nonlinear Programming: Analysis and Methods. Prentice Hall, 1976.

Motivation

Airlines, hotels and rail operators sell many products (an itinerary combined with a fare class) that share a network of finite resources (flight legs, room-nights). When customers choose among whatever products are on offer, the firm's control is no longer "accept or reject a request for product $j$" but which set of products to offer at each moment. The exact dynamic program for this problem is intractable for realistic networks, so practice and theory rely on a deterministic approximation, the choice-based deterministic linear program (CDLP) of Gallego, Iyengar, Phillips and Dubey (2004), which decides for how long each offer set should be offered.

The CDLP has one variable per offer set, so $2^n$ variables for $n$ products, and it is solved by column generation. Knowing in advance which offer sets can never receive positive time in an optimal solution cuts this search space. Liu and van Ryzin (MSOM 2008) extended the single-leg notion of an efficient offer set from Talluri and van Ryzin (Management Science 2004) to networks and showed that only efficient sets are used by an optimal CDLP solution. This mission formalizes that section of their paper (§5).

Setting

A network has $m$ legs and $n$ products $N = \{1,\dots,n\}$. Product $j$ earns revenue $r_j$, and the 0–1 incidence matrix $A = [a_{ij}]$ records which legs product $j$ uses. An offer set is a subset $S \subseteq N$. When $S$ is offered, an arriving customer buys product $j$ with probability $P_j(S) \ge 0$, where $P_j(S) = 0$ for $j \notin S$, and buys nothing with probability $P_0(S) \ge 0$, with $\sum_{j\in S} P_j(S) + P_0(S) = 1$. The expected revenue per arriving customer and the vector of expected capacity consumption are

$$R(S) = \sum_{j\in S} r_j P_j(S), \qquad Q(S) = A\,P(S) \in \mathbb{R}^m .$$

An offer set $T$ is inefficient if some convex weights $\alpha(S) \ge 0$, $\sum_S \alpha(S) = 1$, over all offer sets satisfy

$$R(T) < \sum_S \alpha(S) R(S), \qquad Q(T) \ge \sum_S \alpha(S) Q(S) \ \text{(componentwise)};$$

otherwise $T$ is efficient.

With arrival probability $\lambda \in (0,1]$ per period, capacities $c \in \mathbb{R}^m_{\ge 0}$ and a horizon of length $\tau \ge 0$, the CDLP is

$$\max \sum_{S\subseteq N} \lambda R(S)\,t(S) \quad\text{s.t.}\quad \sum_{S} \lambda Q(S)\,t(S) \le c,\quad \sum_S t(S) \le \tau,\quad t(S) \ge 0,$$

where $t(S)$ is the total time during which $S$ is offered. Its dual has prices $\pi \in \mathbb{R}^m_{\ge 0}$ on the legs and $\sigma \ge 0$ on time. Finally, the frontier function is

$$\bar R(q) = \max_\alpha\Big\{\sum_S \alpha(S)R(S) : \sum_S \alpha(S)Q(S) \le q,\ \sum_S\alpha(S) = 1,\ \alpha \ge 0\Big\}, \qquad q \in [0,1]^m .$$

In the Lean development these objects are ChoiceNetwork m n (with revenue and consumption), IsEfficient, IsCDLPFeasible / cdlpObjective / IsCDLPOptimal, and frontier, all in the namespace ChoiceCDLP.Efficient.

Formalization targets

Goal: Proposition 4

If $t^*$ is an optimal solution of the CDLP and $T$ is an offer set with $t^*(T) > 0$, then $T$ is efficient:

$$t^* \text{ optimal for the CDLP},\ \ t^*(T) > 0 \ \Longrightarrow\ T \text{ efficient}.$$

The statement covers every optimal solution, not only basic ones.

Milestones

1. Frontier function (Appendix, p. 307): $\bar R$ is increasing and concave on $[0,1]^m$.
2. Proposition 3 (p. 296): $T$ is efficient if and only if, for some $\pi \ge 0$, $T$ maximizes $R(S) - \pi^\top Q(S)$ over all offer sets $S$.
3. Reduced cost at the optimal dual (proof of Proposition 4, p. 296): if $t^*$ is optimal and $t^*(T) > 0$, some optimal dual solution $(\pi^*,\sigma^*)$ satisfies $\lambda R(S) - \lambda \pi^{*\top}Q(S) - \sigma^* \le 0$ for every $S$, with equality at $S = T$.
4. Proposition 5 (p. 297): for efficient $S_1, S_2$, $Q(S_2) \ge Q(S_1)$ implies $R(S_2) \ge R(S_1)$.

Significance

Proposition 4 says that efficiency is a property of every offer set an optimal CDLP solution actually uses. Inefficient sets can therefore be removed from the column space of the CDLP, and Proposition 3 describes the remaining sets as the maximizers of revenue net of leg prices, which is the pricing subproblem of column generation. The paper also uses Proposition 4 to argue that its asymptotically optimal policy (Proposition 2 of the same paper) uses only efficient sets. Proposition 5 gives the partial order of efficient sets in the network, the analogue of the total order that drives nested policies in the single-leg model.

The results are proved in the paper; none of them has a machine-checked proof. A formalization provides a checked statement of the network notion of efficiency and its price characterization, which the single-leg results already on the platform do not cover (there $Q(S)$ is a scalar), and a checked link between LP duality for the CDLP and the structure of its optimal solutions.

Difficulty

The paper's proof of Proposition 4 appeals to "the optimal basis" of the CDLP, while the statement is about every optimal solution, including non-basic ones, so the simplex-tableau argument as written does not cover the statement; the existence of optimal dual prices with the required reduced-cost properties has to be established for an arbitrary optimal solution. The "only if" half of Proposition 3 is argued in the paper by a supporting hyperplane to the concave function $\bar R$ at $Q(T)$, followed by an informal argument that the hyperplane's slope is nonnegative; $Q(T)$ may lie on the boundary of $[0,1]^m$, where a supporting hyperplane of a concave function need not exist in the naive sense, and the sign argument is stated in one line. Concavity of $\bar R$ is the concavity of an LP's optimal value in its right-hand side, which the paper cites from Bertsimas and Tsitsiklis without proof and which Mathlib does not provide.

Formalization scope

• Products and legs are Fin n and Fin m; offer sets are Finset (Fin n), so sums over "all $S \subseteq N$" are sums over Finset.univ. All quantities are real. Vector inequalities ($Q(T) \ge \sum_S\alpha(S)Q(S)$, $c \ge 0$, $\pi \ge 0$, $Q(S_2) \ge Q(S_1)$) are componentwise, and $\pi^\top Q(S)$ is dotProduct.
• The choice probabilities are generic, as in the paper: nonnegative, zero outside the offer set, and summing with $P_0(S)$ to one. Revenues are arbitrary reals.
• The CDLP horizon is written $\tau$ (the paper's $T$) to keep $T$ for an offer set. "An optimal solution" is a feasible $t$ whose objective is at least that of every feasible vector.
• Repairs of the printed statements. (i) In Propositions 3 and 4, "$T$ is the optimal solution" is read as "$T$ is an optimal solution": with a unique-maximizer reading, Proposition 3's "only if" direction is false whenever two offer sets have the same $R$ and $Q$ (for instance, $T'$ is $T$ plus a product that is never bought from $T'$); both are then efficient, and neither is a unique maximizer. (ii) Proposition 4 assumes $\lambda > 0$, the paper's standing assumption that $\lambda$ is an arrival probability; at $\lambda = 0$ every feasible $t$ is optimal and inefficient sets can receive positive time. The milestone texts remain verbatim.
• $\bar R$ is a real supremum (sSup) over attainable mixed revenues; on $[0,1]^m$ the set is nonempty (the weight concentrated on the empty offer set is feasible because $Q(\emptyset) = 0$) and bounded above by $\max_S R(S)$, so it is the paper's maximum.
• A trivializing formalization is ruled out: efficiency quantifies over all convex weights on offer sets (not only single dominating sets), the price vector in Proposition 3 is required to be nonnegative, and the optimum in Proposition 4 is over the full feasible set of the CDLP.
• A complete development needs finite-dimensional LP duality with complementary slackness (or Farkas' lemma) and concavity of the optimal value of a parametric LP. Both are reusable well beyond this mission; contributions of either as standalone results 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
• G. Gallego, G. Iyengar, R. Phillips, A. Dubey, Managing Flexible Products on a Network, CORC Technical Report TR-2004-01, Columbia University, 2004 (no DOI; cited as Gallego et al. 2004 in the paper).
• 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
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 5.1, p. 213).

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

Motivation

Retailers that sell many substitutable products must set all their prices at once, and a customer's reaction to one price depends on what else is on the shelf. The nested logit model captures this by grouping similar products into nests, so that raising one price shifts demand mostly to close substitutes. The $d$-level nested logit model extends the familiar two-level version to a whole taxonomy tree of depth $d$ (for example category → brand → size). It is consistent with random utility maximization (McFadden 1978) and is widely used in demand estimation.

Pricing under logit-type models is harder than it looks. Already for the multinomial logit model, which is the one-level case, Hanson and Martin (1996) point out that the expected revenue is not necessarily concave in the prices. For the two-level nested logit, Gallego and Wang (2014) show that the expected revenue is not concave and can have several local maxima. Li, Rusmevichientong and Topaloglu (Oper. Res. 63(2), 2015) treat the general $d$-level model. Their pricing result, Theorem 7.3, is the target of this mission. It shows that a simple gradient-free iteration, the push-up-then-push-down (PUPD) algorithm, produces prices that converge to a stationary point of the expected revenue.

Setting

The products $l=1,\dots,n$ are the leaves of a rooted tree $T=(V,E)$, all at depth $d$. A further leaf, node $0$ (the no-purchase option), hangs directly from $\mathrm{root}$. Every other node $j$ is a nonleaf node with a nonempty set $\mathrm{Children}(j)$ and a parameter $\eta_j$. The standing assumptions are $\eta_j\in(0,1]$ for nonleaf $j\neq\mathrm{root}$ and $\eta_{\mathrm{root}}=0$. Each product carries parameters $\alpha_l\in\mathbb R$ and $\beta_l>0$, and node $0$ carries $\alpha_0\in\mathbb R$.

Given a price vector $\mathbf p=(p_1,\dots,p_n)$, where the no-purchase price is fixed at $p_0=0$, the preference weights are computed bottom-up:

$$V_l(\mathbf p)=e^{\alpha_l-\beta_lp_l},\qquad V_0(\mathbf p)=e^{\alpha_0},\qquad V_j(\mathbf p)=\Big(\sum_{k\in\mathrm{Children}(j)}V_k(\mathbf p)\Big)^{\eta_j}.$$

The expected revenues are $R_l(\mathbf p)=p_l$, $R_0(\mathbf p)=0$, and

$$R_j(\mathbf p)=\frac{\sum_{k\in\mathrm{Children}(j)}V_k(\mathbf p)R_k(\mathbf p)}{\sum_{k\in\mathrm{Children}(j)}V_k(\mathbf p)}$$

at a nonleaf node. The expected revenue of $\mathbf p$ is $R_{\mathrm{root}}(\mathbf p)$. A customer walks down from $\mathrm{root}$, choosing a child with probability proportional to its weight. The probability $\theta_l(\mathbf p)$ of ending at product $l$ is the product, over the levels $h=1,\dots,d$, of $V_{\mathrm{An}(l,h)}/\sum_{k\in\mathrm{Sibling}(\mathrm{An}(l,h))}V_k$, where $\mathrm{An}(l,h)$ is the ancestor of $l$ in level $h$.

Top-down, the scalars $u_j(\mathbf p)$ are $u_{\mathrm{root}}=R_{\mathrm{root}}$ and $u_j=\eta_ju_{\mathrm{Parent}(j)}+(1-\eta_j)R_j$. A stationary point of $R_{\mathrm{root}}$ is a price vector at which the gradient of $R_{\mathrm{root}}$ is zero.

The PUPD algorithm starts from $\mathbf p^0=\mathbf 0$. Given $\mathbf p^s$, it sets $t^s_{\mathrm{root}}=R_{\mathrm{root}}(\mathbf p^s)$ and, for every other nonleaf node,

$$t^s_j=\max\big\{t^s_{\mathrm{Parent}(j)},\ \eta_jt^s_{\mathrm{Parent}(j)}+(1-\eta_j)R_j(\mathbf p^s)\big\}.$$

It then updates $p^{s+1}_l=1/\beta_l+t^s_{\mathrm{Parent}(l)}$ for every product $l$.

Formalization targets

Goal: Theorem 7.3 (p. 336)

$$\exists\,\mathbf p^*\in\mathbb R^n:\qquad \lim_{s\to\infty}\mathbf p^s=\mathbf p^* \quad\text{and}\quad \nabla R_{\mathrm{root}}(\mathbf p^*)=0 .$$

The whole sequence converges and its limit is stationary. No rate is claimed, and none is asked for.

Milestones

• Lemma 7.1 (p. 335). For $\mathbf p\in\mathbb R^n_+$ and every product $l$,

$$\frac{\partial R_{\mathrm{root}}}{\partial p_l}(\mathbf p)=-\theta_l(\mathbf p)\,\beta_l\Big(p_l-\frac1{\beta_l}-u_{\mathrm{Parent}(l)}(\mathbf p)\Big).$$

• Corollary 7.2 (p. 336). For $\mathbf p\in\mathbb R^n_+$, $\mathbf p$ is a stationary point of $R_{\mathrm{root}}$ if and only if $p_l=1/\beta_l+u_{\mathrm{Parent}(l)}(\mathbf p)$ for all $l$.

Significance

The result itself. Theorem 7.3 turns a nonconcave, many-product pricing problem into an iteration that needs no gradient evaluations and no step size. Each iteration costs one bottom-up and one top-down pass over the tree. The paper's numerical experiments (§8) report that it reaches a stationary point much faster than gradient ascent. Lemma 7.1 gives the gradient of the expected revenue in closed form for any depth. Corollary 7.2 turns stationarity into a fixed-point equation in the prices, which is what makes a price-update scheme like PUPD natural.

Formalizing it. The proofs of Lemma 7.1 and Theorem 7.3 are in the paper's online Appendix E. The acknowledgments (pp. 340–341) record that an error found in an earlier version led to a new proof that the revenues under the PUPD algorithm are always bounded. A machine-checked proof would settle the convergence claim independently of that history. No nested logit or multinomial logit pricing result, and no part of this one, has a machine-checked proof on Prove2Me.

Difficulty

Lemma 7.1 is a chain-rule computation through a tree of power means, and it is technical rather than deep. The hard part is Theorem 7.3. The obvious fixed-point iteration $p^{s+1}_l=1/\beta_l+u_{\mathrm{Parent}(l)}(\mathbf p^s)$ suggested by Corollary 7.2 is not the algorithm. PUPD replaces $u$ by the scalars $t^s$, which involve a maximum, and the update direction $\mathbf p^{s+1}-\mathbf p^s$ is in general not parallel to the gradient. So neither contraction arguments for the plain fixed-point map nor the standard ascent analysis of gradient methods applies directly. $R_{\mathrm{root}}$ is not concave and may have several stationary points, so convergence of the whole sequence, not only of a subsequence or of the gradient norms, is the substance of the claim.

Formalization scope

The node type is Option (Fin n) ⊕ Inner. Sum.inl (some l) is product $l$, indexed by Fin n, so the paper's products $1,\dots,n$ are $0,\dots,n-1$. Sum.inl none is node $0$. Inner is a finite type of nonleaf nodes containing root, with a parent map into Inner and a level function that encodes the $d$ levels. Every nonleaf node has a child. Prices are Fin n → ℝ, so node $0$ has no price coordinate, and all $n$ products are priced (there is no assortment decision). The conventions:

• Powers $x^{\eta_j}$ are Real.rpow. Since $\eta_{\mathrm{root}}=0$, $V_{\mathrm{root}}=1$ and it is never used. Division is Lean's, but every denominator is positive under the standing assumptions.
• $R_{\mathrm{root}}$, $\theta_l$ and $u_j$ are defined on all of $\mathbb R^n$ by the paper's formulas. The paper restricts to $\mathbb R^n_+$, and Lemma 7.1 and Corollary 7.2 keep that hypothesis as printed.
• The partial derivative in Lemma 7.1 is HasDerivAt of $x\mapsto R_{\mathrm{root}}(\mathbf p$ with $p_l:=x)$ at $p_l$. "Stationary point" is HasFDerivAt R_root 0 p (the gradient is zero). This is the unconstrained gradient, as on p. 335, with no boundary condition, and it is the same notion in Corollary 7.2 and in the goal.
• $\theta_l$ is defined by the printed product along the root-to-leaf path, and $\mathrm{An}(l,h)$ is reached by $d-h$ parent steps. $\theta_l$ is not a free parameter.
• The PUPD iterates are a definition (pupd) with $\mathbf p^0=\mathbf 0$ and the max-based $t^s$, and $t^s_{\mathrm{root}}=R_{\mathrm{root}}(\mathbf p^s)$. The goal is not stated for an arbitrary start point or for the $u$-based iteration.

A trivializing formalization is ruled out: convergence is Filter.Tendsto of the full sequence to a point at which HasFDerivAt holds with derivative $0$. It is not a statement about limit points, gradient norms, or an arbitrary sequence satisfying a hypothesis.

A complete development needs derivatives of Real.rpow compositions over a finite tree, positivity of the weights and choice probabilities, and a convergence argument for the PUPD iteration. The weight and revenue recursions over a finite rooted tree could be reused for the assortment half of the same paper and for other tree-structured choice models. Contributions to any milestone, and alternative proofs of Lemma 7.1, are welcome.

Selected references

• H. Li, P. Rusmevichientong, H. Topaloglu, The d-Level Nested Logit Model: Assortment and Price Optimization Problems, Operations Research 63(2):325–341, 2015. https://doi.org/10.1287/opre.2015.1355
• G. Gallego, R. Wang, Multiproduct Price Optimization and Competition Under the Nested Logit Model with Product-Differentiated Price Sensitivities, Operations Research 62(2):450–461, 2014. https://doi.org/10.1287/opre.2013.1249
• W. Hanson, K. Martin, Optimizing Multinomial Logit Profit Functions, Management Science 42(7):992–1003, 1996. https://doi.org/10.1287/mnsc.42.7.992
• D. McFadden, Modelling the Choice of Residential Location, in A. Karlqvist et al. (eds.), Spatial Interaction Theory and Planning Models, North-Holland, 1978, 75–96 (cited as McFadden 1978 on p. 328 of Li et al.).

Motivation

A retailer or an airline chooses which products to offer, and customers choose among what is offered. The assortment problem asks for the offer set that maximizes expected revenue when customer choice follows a given probabilistic model. Under the multinomial logit model the answer has a simple shape: an optimal assortment is revenue ordered, i.e. it consists of all products whose revenue exceeds some threshold (Talluri and van Ryzin, 2004). The multinomial logit model treats all products as equally substitutable, and nested logit models relax this by grouping products into nests whose utilities are correlated.

The $d$-level nested logit model organizes the products as the leaves of a tree with $d$ levels, each level refining the grouping of the previous one (for instance category, brand, size). Li, Rusmevichientong and Topaloglu (Oper. Res. 63(2), 2015) characterized an optimal assortment under this model for every $d$. Timeline: the one-level case (multinomial logit) is due to Talluri and van Ryzin (2004); the two-level case with an arbitrary number of nests is due to Davis, Gallego and Topaloglu (2014); Li, Rusmevichientong and Topaloglu (2015) treat arbitrary depth $d$. This mission formalizes the 2015 characterization and the three statements of §4 of that paper that lead to it.

Setting

There are $n$ products $1,\dots,n$ and a no-purchase option $0$. A product tree $T$ is a finite rooted tree with $d$ levels whose leaves are exactly the $n+1$ products: the leaves $1,\dots,n$ lie at depth $d$, and leaf $0$ is a child of the root. Each node $j$ other than the root has a parent $\mathrm{Parent}(j)$; $\mathrm{Children}(j)$ is the set of its children, and $N_j\subseteq\{0,\dots,n\}$ is the set of leaves below $j$. Each nonleaf node carries a nest parameter $\eta_j\in(0,1]$, with $\eta_{\mathrm{root}}=0$. Each product carries an attractiveness $v_l>0$, and each product $l\ge1$ a revenue $r_l\in\mathbb R$.

An assortment is a set $S\subseteq\{1,\dots,n\}$; the no-purchase option is always available. The preference weight of a node is defined bottom-up: $V_l=v_l$ at an offered product leaf, $V_l=0$ at a product leaf that is not offered, $V_0=v_0$, and at a nonleaf node

$$V_j(S_j)=\Big(\sum_{k\in\mathrm{Children}(j)}V_k(S_k)\Big)^{\eta_j},$$

so $V_{\mathrm{root}}=1$. A customer at a nonleaf node $j$ moves to child $k$ with probability $V_k/\sum_{l}V_l$. The expected revenue from a customer at node $j$ is $R_l=r_l$ at an offered product leaf, $0$ at an unoffered leaf and at leaf $0$, and

$$R_j(S_j)=\frac{\sum_{k\in\mathrm{Children}(j)}V_k(S_k)R_k(S_k)}{\sum_{k\in\mathrm{Children}(j)}V_k(S_k)}$$

at a nonleaf node. The assortment problem is

$$Z^*=\max_{S\subseteq\{1,\dots,n\}}R_{\mathrm{root}}(S_{\mathrm{root}}).\tag{3}$$

Given an optimal assortment $S^*$, the thresholds $t^*_j$ are computed top-down by

$$t^*_j=\max\{t^*_{\mathrm{Parent}(j)},\ \eta_jt^*_{\mathrm{Parent}(j)}+(1-\eta_j)R_j(S^*_j)\},\qquad t^*_{\mathrm{Parent}(\mathrm{root})}=0,$$

and the local problem at node $j$ is

$$\max_{S_j\subseteq N_j}\ V_j(S_j)\big(R_j(S_j)-t^*_{\mathrm{Parent}(j)}\big).\tag{4}$$

Formalization targets

Goal: Corollary 4.3 (revenue comparison)

For every product tree and parameters in the ranges above, and for every optimal assortment $S^*$ with its thresholds $t^*$,

$$\hat S=\{\,l\in\{1,\dots,n\}:\ r_l\ge t^*_{\mathrm{Parent}(l)}\,\}\quad\text{satisfies}\quad R_{\mathrm{root}}(S_{\mathrm{root}})\le R_{\mathrm{root}}(\hat S_{\mathrm{root}})\ \text{ for all } S\subseteq\{1,\dots,n\}.$$

Milestones

• Proposition 4.1. For an optimal $S^*$ and every node $j$, $S^*_j=S^*\cap N_j$ is an optimal solution of the local problem (4) at $j$.
• The root observation (§4, p. 329). The objective of the local problem at the root equals $R_{\mathrm{root}}$, and a set solves the local problem at the root exactly when it solves (3).
• Theorem 4.2. At a nonleaf node $j$, if $\hat S_k\subseteq N_k$ solves the local problem at each child $k$, then $\bigcup_{k\in\mathrm{Children}(j)}\hat S_k$ solves the local problem at $j$.

Significance

The corollary says that an optimal assortment is determined by one comparison per product: a product is offered exactly when its revenue reaches a threshold attached to its parent node. Within each group of sibling products the optimal assortment is therefore revenue ordered, which reduces the search from $2^n$ subsets to a structured family, and it is the basis of the paper's polynomial-time algorithm (§5). For one level it recovers the revenue-ordered result for multinomial logit, and for two levels the characterization of Davis, Gallego and Topaloglu (2014). Theorem 4.2, the synthesis of local solutions, is the property that makes a bottom-up dynamic program over the tree correct.

The result is proved in the paper; the proofs of Proposition 4.1 and Theorem 4.2 are in its online appendix. No machine-checked version of any nested logit assortment result is known to exist. A formalization would give a verified statement of the model itself (recursive preference weights with real exponents, conditional revenues, top-down thresholds), which is reusable for the paper's pricing results and for other tree-structured choice models.

Difficulty

The objective $R_{\mathrm{root}}$ is a nested ratio of sums raised to fractional powers, neither concave nor monotone in the offer set, so the usual exchange argument for revenue-ordered sets does not apply directly: adding a product to a nest changes that nest's weight, and through the exponents $\eta_j$ the weight of every ancestor. The thresholds $t^*_j$ are defined from an optimal assortment that is not known in advance, so every statement is a property of an unknown optimum rather than a computation. The local problems couple across levels only through these thresholds, and relating the optimum of the problem at a node to the optima at its children is the step that requires work. A proof that tries to compare $\hat S$ with $S^*$ product by product meets the fact that $\hat S$ and $S^*$ may differ at ties.

Formalization scope

The tree is a structure ProductTree n with a finite node type, a root, a parent map, a depth function (root at depth $0$, children one level deeper, all depths at most $d$, product leaves at depth exactly $d$, leaf $0$ a child of the root) and an injective leaf map Fin (n + 1) → Node. Assortments are finsets of Fin (n + 1) not containing $0$; the no-purchase leaf always contributes $v_0$. Preference weights use Real.rpow, so $x^0=1$ gives $V_{\mathrm{root}}=1$. Conventions fixed in Lean and silent on the page:

• $\eta_{\mathrm{root}}=0$ and $\eta_j\in(0,1]$ at the other nonleaf nodes (StandingEta);
• $v_0,\dots,v_n>0$ is a hypothesis of every theorem: the page never states a sign, but the model presupposes it, and it makes every denominator in (2) positive; revenues carry no sign condition;
• $R_j(\emptyset)=0$ at a nonleaf node whose subtree offers nothing (Lean's x / 0 = 0 on the page's $0/0$); in $t^*$ this value yields $t^*_j=t^*_{\mathrm{Parent}(j)}$;
• the thresholds are a function of the given optimal $S^*$, and the goal holds for every optimal $S^*$;
• optimality means "no assortment has larger objective", with a finite quantifier, never a supremum.

A trivializing formalization is ruled out: the thresholds are not free parameters or computed from $\hat S$, and the conclusion is optimality of $\hat S$ against every assortment, not an existence statement.

A complete development needs facts about the recursive definitions (unfolding at leaves and nonleaf nodes, $N_{\mathrm{root}}=\{0,\dots,n\}$, disjointness of the $N_k$ of siblings), monotonicity and concavity properties of $x\mapsto x^{\eta}$ on $[0,\infty)$ from Mathlib, and induction over the tree by depth. Tree-induction lemmas and the model layer are reusable by the companion pricing mission. Contributions of a proof of any milestone, of alternative proofs of Theorem 4.2, and of the special cases $d=1$ and $d=2$ are welcome.

Selected references

• H. Li, P. Rusmevichientong, H. Topaloglu, The d-Level Nested Logit Model: Assortment and Price Optimization Problems, Operations Research 63(2):325–341, 2015. https://doi.org/10.1287/opre.2015.1355
• J. M. Davis, G. Gallego, H. Topaloglu, Assortment Optimization Under Variants of the Nested Logit Model, Operations Research 62(2):250–273, 2014. https://doi.org/10.1287/opre.2014.1256
• 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

Motivation

A seller who does not know its demand curve has to learn it from the sales it makes. Each price it charges earns revenue now and also produces information for later. This learning-and-earning problem is basic to revenue management and online retail. The most common heuristic is certainty-equivalence pricing: fit the demand model by least squares, then charge the price that would be optimal if the fit were exact. The heuristic can fail. Its prices may settle at a wrong value, so that estimation stops improving, a phenomenon called incomplete learning (Lai and Robbins 1982; den Boer and Zwart 2013). The regret then grows linearly in the horizon.

Keskin and Zeevi (2014) first show that no policy can have regret below order $\sqrt T$ (the subject of the first mission in this series). They then give two simple, checkable conditions on a policy's price path that guarantee regret of order $\sqrt T \log T$. The conditions cover a whole family of modified least squares policies, including the "MLE-cycle" policy of Broder and Rusmevichientong (2012) and the "controlled variance" policy of den Boer and Zwart. This mission formalizes those sufficient conditions (Theorem 2 of the paper).

Setting

A seller charges prices $p_t \in [l,u]$, $0 \le l < u$, in periods $t = 1, 2, \dots$ and observes the demand

$$D_t = \alpha + \beta p_t + \varepsilon_t .$$

The unknown parameter $\theta = (\alpha,\beta)$ lies in a rectangle $\Theta = [a_{\min},a_{\max}]\times[b_{\min},b_{\max}]$ with $b_{\max} < 0$. The demand shocks $\varepsilon_t$ are i.i.d. with mean $0$ and variance $\sigma^2 > 0$, and they are light-tailed: $\mathbb{E}[e^{z\varepsilon_t}] < \infty$ for $|z| \le z_0$, for some $z_0 > 0$. The expected revenue is $r_\theta(p) = p(\alpha+\beta p)$, maximized at the myopic price $\varphi(\theta) = -\alpha/(2\beta)$. The model assumes $\varphi(\theta) \in (l,u)$ for all $\theta \in \Theta$.

A pricing policy $\pi$ charges a constant $p_1$ and then $p_{t+1} = \pi_{t+1}(H_t)$, where $\pi_{t+1}$ is a measurable function of the history $H_t = (D_1,p_1,\dots,D_t,p_t)$ with values in $[l,u]$. The regret of $\pi$ under $\theta$ is

$$\Delta^\pi_\theta(T) = T\,r_\theta(\varphi(\theta)) - \mathbb{E}^\pi_\theta\Big[\sum_{t=1}^T r_\theta(p_t)\Big].$$

After $t$ periods the empirical Fisher information is $\mathcal{J}_t = \sum_{s=1}^t \begin{bmatrix}1 & p_s\\ p_s & p_s^2\end{bmatrix}$. The least squares estimate is $\hat\theta_t = \mathcal{J}_t^{-1}(\sum_s D_s, \sum_s D_s p_s)^{\mathsf T}$, and the truncated estimate $\vartheta_t$ is the Euclidean projection of $\hat\theta_t$ onto $\Theta$. The information metric is $J_t = \sum_{s=1}^t (p_s - \bar p_t)^2$ with $\bar p_t = t^{-1}\sum_{s=1}^t p_s$. The greedy least squares price in period $s+1$ is $\varphi(\vartheta_s)$.

Formalization targets

Goal: Theorem 2 (sufficient conditions for asymptotic optimality)

Let $\theta \in \Theta$, let $\kappa_0,\kappa_1 > 0$, and let $\pi$ satisfy, almost surely for all $t \ge 2$,

$$\text{(i)}\ \ J_t \ge \kappa_0\sqrt t, \qquad \text{(ii)}\ \ \sum_{s=2}^t \big(\varphi(\vartheta_s) - p_{s+1}\big)^2 \le \kappa_1 \sqrt t .$$

Then there is a finite $C > 0$ with

$$\Delta^\pi_\theta(T) \le C\sqrt T \log T \quad\text{for all } T \ge 3 .$$

The goal fixes no constant. It asserts only the rate $\sqrt T\log T$.

Milestones

1. Lemma 2 (corrected constant). For any prices in $[l,u]$, $\mu_{\min}(\mathcal{J}_t) \ge J_t/(1+u^2+(u-l)^2)$.
2. Lemma 3. There are $\rho, k > 0$ such that for every policy, every $\theta\in\Theta$, all $\delta,m>0$ and $t\ge 2$,

$$\mathbb{P}^\pi_\theta\{\lVert\hat\theta_t-\theta\rVert>\delta,\ J_t\ge m\} \le k\,t\,e^{-\rho(\delta\wedge\delta^2)m}.$$

3. (A10). $\mathbb{E}(\varphi(\theta)-p_{t+1})^2 \le 2\mathbb{E}(\varphi(\theta)-\varphi(\vartheta_t))^2 + 2\mathbb{E}(\varphi(\vartheta_t)-p_{t+1})^2$.
4. (A11). Under (i), there are $K>0$ and $N$ with $\mathbb{E}(\varphi(\theta)-p_{t+1})^2 \le K\log t/\sqrt t + 2\mathbb{E}(\varphi(\vartheta_t)-p_{t+1})^2$ for $t \ge \max\{N,2\}$.
5. Regret identity. $\Delta^\pi_\theta(T) = -\beta\sum_{t=1}^T \mathbb{E}(p_t-\varphi(\theta))^2$.

Significance

The result. Theorem 2 turns the design of a near-optimal learning policy into two pathwise constraints on the price sequence. Condition (i) requires enough price dispersion to keep learning. Condition (ii) requires the policy to stay close to the greedy price so that it keeps earning. Any least squares variant that satisfies both constraints is optimal up to a logarithmic factor, and together with the $\sqrt T$ lower bound this fixes the minimax rate of the problem. The constrained-ILS and decaying-perturbation policies of §3.3 are certified this way, and the same template reappears in the paper's incumbent-price and multiproduct results.

Formalizing it. The theorem is proved in the paper. It has no machine-checked proof, and the platform has no dynamic-pricing results so far. A formalization would contribute a reusable model of adaptively chosen designs with a least squares estimator, an exponential concentration bound for least squares under adaptive prices (Lemma 3), and the regret decomposition. The formalization also checks the paper's constants: one of them, in Lemma 2, is misprinted (see Formalization scope).

Difficulty

The prices are chosen by the policy from past noise, so the regression design is random and adapted. The classical fixed-design analysis of least squares does not apply, and neither does a union bound over a fixed set of designs. Lemma 3 needs a tail bound for $\hat\theta_t - \theta$ that is uniform over all directions in the plane and holds only on the event where $J_t$ is large, with noise that is only light-tailed rather than Gaussian or bounded. Converting the eigenvalue of $\mathcal{J}_t$ into the scalar $J_t$ (Lemma 2) is elementary but easy to get wrong, as the misprinted constant shows. Summing the per-period bounds into the $\sqrt T\log T$ rate is where conditions (i) and (ii) interact.

Formalization scope

Periods are indexed from $1$. The noise is a family ε : ℕ → Ω → ℝ on a probability space, with ε t used in period $t$. The price process of a policy is built by recursion from the noise, which realises the paper's law on demand sequences. A policy is a family of measurable maps from histories Fin t → ℝ × ℝ of (demand, price) pairs into $[l,u]$, and it sees neither $\theta$ nor the noise. Expectations are Bochner integrals of bounded measurable functions. Probabilities are ENNReal values. Real.log is the natural logarithm. The least squares estimate uses Mathlib's matrix inverse, which is $0$ on singular matrices. Every statement uses $\hat\theta_t$ only where $J_t > 0$, which is equivalent to $\det\mathcal{J}_t = tJ_t > 0$. The truncation onto $\Theta$ is coordinatewise clamping, the Euclidean projection onto a rectangle. The smallest eigenvalue is the infimum of the Rayleigh quotient over unit vectors. Constants sit in the paper's quantifier positions: $C$ after $\theta$ and $\pi$ in the goal; $\rho, k$ before the policy in Lemma 3.

Corrections of the printed statements.

• Theorem 2, condition (i). The page requires (i) "almost surely for all $t$". At $t=1$, $J_1 = 0 < \kappa_0$, so read literally no policy satisfies the hypotheses and the theorem is vacuous. Conditions (i) and (ii) are required for $t \ge 2$, as the proof uses them.
• Theorem 2, condition (ii). The page's sum starts at $s=0$, but $\vartheta_0$ and $\vartheta_1$ are undefined for a general policy because $\mathcal{J}_0$ and $\mathcal{J}_1$ are singular. The sum starts at $s = 2$. This only weakens the hypothesis.
• Lemma 2. The printed constant $\gamma = 2/(1+2u-l)^2$ is false. For $l = 9.9$, $u=10$, $p = (9.9, 10)$ one gets $\mu_{\min} \approx 5.0\cdot10^{-5} < \gamma J_2 \approx 8.1\cdot10^{-5}$. The statement uses $\gamma' = 1/(1+u^2+(u-l)^2)$, and downstream results use only $\gamma' > 0$.
• (A11). The paper's explicit constants $4\tilde K_0/(\rho\kappa_0)$ and $N$ depend on the existential constants of Lemma 3. They are therefore stated as existential $K$ and $N$, uniform in $\theta$ and $\pi$.

Trivializing formalizations ruled out. Hypotheses that no policy can satisfy (conditions required at $t=1$) are excluded by the $t \ge 2$ form. A policy type that could read $\theta$ or the noise is excluded by construction. Junk values of the matrix inverse and of $\bar p_0$ never enter a hypothesis or conclusion.

A complete development needs the price-process recursion and its measurability, exponential supermartingales for adaptively weighted sums of light-tailed noise, a covering argument on the unit circle, and the layer-cake formula for $\mathbb{E}\lVert\hat\theta_t-\theta\rVert^2$. The model, the least squares estimator and Lemmas 2–3 can be reused for the incumbent-price variant (mission IV of this series) and for other least-squares-based pricing and bandit policies. Contributions of any milestone are welcome, and Lemma 3 on its own is a useful statement.

Selected references

• N. B. Keskin and A. Zeevi, Dynamic Pricing with an Unknown Demand Model: Asymptotically Optimal Semi-Myopic Policies, Operations Research 62(5):1142–1167, 2014. https://doi.org/10.1287/opre.2014.1294
• J. Broder and P. Rusmevichientong, Dynamic Pricing under a General Parametric Choice Model, Operations Research 60(4):965–980, 2012. https://doi.org/10.1287/opre.1120.1057
• A. V. den Boer and B. Zwart, Simultaneously Learning and Optimizing Using Controlled Variance Pricing, Management Science 60(3):770–783, 2014. https://doi.org/10.1287/mnsc.2013.1788
• T. L. Lai and H. Robbins, Iterated Least Squares in Multiperiod Control, Advances in Applied Mathematics 3(1):50–73, 1982. https://doi.org/10.1016/0196-8858(82)90003-1