The OR Formalization Drive

Motivation

In the single-machine scheduling problem $1|\mathrm{prec}|\sum w_jC_j$, a set $N$ of $n$ jobs, each with a processing time $p_j\ge 0$ and a weight $w_j\ge 0$, is processed on one machine without interruption, subject to precedence constraints given by a partial order $P$ on $N$. The aim is to minimize the weighted sum of completion times $\sum_j w_jC_j$. The problem is strongly NP-hard for general precedence constraints (Lawler 1978; Lenstra and Rinnooy Kan 1978), and its approximability was a recurring open question in scheduling theory (Schuurman and Woeginger 1999).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph $G^S_P$ built from the instance. Many problems on partial orders become polynomial when the order is an interval order, so it is natural to ask whether this one does too. Section 7 of Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 2011) answers no: the problem stays NP-hard on interval orders. The proof is a reduction from vertex cover in connected graphs of maximum degree 3. This mission formalizes the correctness of that reduction.

Setting

A poset $P=(N,P)$ is read as a reflexive relation: $(x,y)\in P$ means $x\le y$. Jobs $x,y$ are incomparable if neither $(x,y)$ nor $(y,x)$ is in $P$, and $\operatorname{inc}(P)$ is the set of ordered incomparable pairs. The vertex cover graph $G^S_P$ has one node $(i,j)$ for each incomparable pair, weighted $p_iw_j$. Two nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell)\in P$ and $(k,j)\in P$. Write $w(C_I)$ for the minimum weight of a vertex cover of $G^S_I$.

A poset is an interval order if each element $x$ can be assigned a closed real interval $[a_x,b_x]$ such that $x<y$ if and only if $b_x<a_y$.

The reduction starts from a graph $G=(V,E)$ with vertices $v_1,\dots,v_N$ and a spanning tree $T=(V,E_T)$ rooted at $v_1$, numbered so that each parent comes before its children. The paper uses a breadth-first search tree.

• Stage 1. The graph $G'$ is built from $T$. Each $v_i$ gets a pendant path $v_i - u^i_1 - u^i_2$. Each non-tree edge $\{v_i,v_j\}\in E\setminus E_T$ with $i<j$ gets the path $v_i - e^{ij}_1 - e^{ij}_2 - u^j_2$. The non-tree edges themselves are not edges of $G'$.
• Stage 2. The scheduling instance $S$ has jobs $s_0$, $s_1,\dots,s_N$, $m_1,\dots,m_N$, $e_1,\dots,e_N$, and $b_{ij}$ for each non-tree edge. Their intervals, processing times and weights are given in a table on p. 662. For example, $s_j$ has interval $[i,j]$, processing time $1/k^j$ and weight $k^i$, where $v_i$ is the parent of $v_j$. The precedence constraints $I$ are the interval order of these intervals. With $n$ the number of jobs, the parameter is $k=n^2+1$.
• The set $D$. It is $\{(s_0,s_1)\}\cup\{(s_i,s_j): v_i \text{ parent of } v_j\}\cup\{(s_i,m_i),(m_i,e_i)\}\cup\{(s_i,b_{ij}),(b_{ij},m_j)\}$. The graph $G'_I$ is the subgraph of $G^S_I$ induced by $D$.

Formalization targets

Goal: Theorem 7.1 (p. 661)

For every connected graph $G$ of maximum degree at most $3$, every parent-first spanning tree $T$ and every $m\in\mathbb N$, the precedence constraints $I$ of $S$ form an interval order, and

$$G \text{ has a vertex cover of size} \le m \iff \lfloor w(C_I)\rfloor \le m + |V| + |E\setminus E_T|.$$

Milestones, in the order the proof uses them

• Claim 1 (p. 662): $\tau(G') = \tau(G)+|V|+|E\setminus E_T|$, where $\tau$ is the vertex cover number.
• Remark 7.1 (p. 662): for jobs with intervals $[a,b]$ and $[c,d]$ and $a\le d$, $p_i\le 1/k^{\lceil b\rceil}$ and $w_j\le k^{\lceil c\rceil}$. On incomparable pairs $p_iw_j\in\{1\}\cup[0,1/k]$. Moreover, $p_iw_j\ge k$ forces $b<c$, and $p_iw_j=1$ forces $\lceil b\rceil=\lceil c\rceil$.
• Claim 2 (p. 663): an incomparable pair $(i,j)$ has $p_iw_j=1$ if it is in $D$, and $p_iw_j\le 1/k$ otherwise.
• Claim 3 (p. 663): $G'_I\cong G'$.
• §7, p. 664: with $k=n^2+1$, $\sum_{(i,j)\in\operatorname{inc}(I)\setminus D}p_iw_j<1$, and hence $w(C'_I)=\lfloor w(C_I)\rfloor$.

Significance

The result. Interval orders are a standard tractable class: several scheduling and order-theoretic problems that are hard in general become polynomial on them (Papadimitriou and Yannakakis 1979). Theorem 7.1 puts $1|\mathrm{prec}|\sum w_jC_j$ outside this pattern. Section 6 of the same paper shows that the problem nonetheless has a $3/2$-approximation on interval orders, so hardness and approximability are separated on this class. The paper also remarks that the proof makes weighted vertex cover NP-hard to approximate within some factor $r>1$ on the graphs $G^S_I$ arising from interval orders.

Formalizing it. The theorem is proved in the paper. Nothing in this mission is open, and none of it has been machine-checked before. The work splits into the following parts:

• a gadget argument on unweighted vertex covers (Claim 1, after Alimonti and Kann);
• an exact case analysis of incomparable pairs in a concrete interval order (Remark 7.1, Claim 2);
• a graph isomorphism (Claim 3);
• a rounding argument that links weighted and unweighted optima.

The definitions of $G^S_P$ and of minimum-weight vertex covers are shared with the other missions of this series.

Difficulty

The construction is explicit, and each step is elementary. The work is in the bookkeeping. Claim 2 requires classifying every incomparable pair of jobs, including pairs of different kinds such as $(b_{ij}, s_\ell)$, by comparing ceilings of interval endpoints. Half-integer endpoints ($m_i$, $b_{ij}$) are exactly what separates weight-one pairs from comparable ones. Claim 3 requires checking adjacency in $G^S_I$ for all pairs of nodes of $D$ in both directions. The paper writes out two cases in each direction and calls the rest similar.

Claim 1 has a direction that is not simply local. A vertex cover of $G'$ that misses both endpoints of a non-tree edge has to be repaired by swapping gadget vertices, and the repair must be repeated without increasing the size.

A natural first idea is to treat the light nodes (weight at most $1/k$) as negligible one at a time. This does not suffice: the argument needs their total weight to stay below $1$, which is what forces $k$ to grow with $n^2$.

Formalization scope

• Graph and tree. $G$ is a SimpleGraph (Fin N); vertex $v_{i+1}$ is i, and the root is index 0. The tree is a TreeLayout: a parent function returning none exactly at the root, with each parent of smaller index and adjacent in $G$. The statements hold for every such layout. This is stronger than the paper's breadth-first tree, and the proof uses only "parent before child".
• Hypotheses of the goal. Connectivity and the degree bound ((G.neighborSet v).ncard ≤ 3) are kept as in the paper. They matter only for the NP-completeness of the source problem.
• Jobs. The jobs form an inductive type with one constructor per row of the table. Their order is a PartialOrder instance: $x\le y$ iff $x=y$ or $b_x<a_y$. Processing times and weights are real numbers. Section 1 of the paper asks for nonnegative integers, but the instance uses $1/k^j$ and the formalization follows the instance as printed.
• Constants. The constants are explicit: $k=n^2+1$ with $n$ the cardinality of the job type, and $c=|V|+|E\setminus E_T|$. Remark 7.1 and Claim 2 are stated for every real $k>1$.
• Optimum values. $w(C_I)$ is a minimum over the finite family of vertex covers. Unweighted cover numbers are Mathlib's SimpleGraph.vertexCoverNum. The floor is Nat.floor, which agrees with the integer floor because $w(C_I)\ge 0$.
• Not formalized. The goal's wording ("NP-hard") is not formalized. Neither are the NP-completeness of degree-3 vertex cover (Garey, Johnson and Stockmeyer), the polynomial size of the construction, or Theorem 2.1 (cited), which turns a vertex cover of $G^S_I$ into a schedule. What is stated is the correctness of the reduction: the instance has interval-order constraints, and its optimum decides the vertex cover question.
• No trivialization. The instance $S$ is built from $G$ and $T$ exactly as in the table. The goal quantifies over all graphs and layouts, never over an instance $S$ assumed to have the properties.
• Contributions. Contributions are welcome on any milestone. Claims 1 and 3 are independent of the weights, and Claim 2 is independent of the graph theory.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-1
• J. R. Correa, A. S. Schulz, Single machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• P. Alimonti, V. Kann, Some APX-completeness results for cubic graphs, Theoret. Comput. Sci. 237(1–2):123–134, 2000. https://doi.org/10.1016/S0304-3975(98)00158-3
• M. R. Garey, D. S. Johnson, L. Stockmeyer, Some simplified NP-complete graph problems, Theoret. Comput. Sci. 1(3):237–267, 1976. https://doi.org/10.1016/0304-3975(76)90059-1
• C. H. Papadimitriou, M. Yannakakis, Scheduling interval-ordered tasks, SIAM J. Comput. 8(3):405–409, 1979. https://doi.org/10.1137/0208031

Why price without knowing demand

A seller with a fixed stock of a single product and a finite selling season has to set prices without knowing how demand responds to them. This is the standard situation in revenue management: airline seats, hotel rooms, fashion goods and event tickets. The classical theory of dynamic pricing (Gallego and van Ryzin, 1994) assumes that the demand function $\lambda(p)$, the rate of purchase requests at price $p$, is known. In practice it has to be learned from sales, while the season runs and the stock is consumed.

Besbes and Zeevi (2009) asked how much revenue is lost for not knowing $\lambda$. They answered it with explicit policies and matching-order bounds. Their setting differs from the multi-armed bandit literature it borrows from in three ways:

• the problem is constrained by an initial inventory;
• the set of prices is a continuum;
• the set of possible demand functions is a nonparametric class.

This mission formalizes their first main result, Proposition 1: a simple learn-then-price policy has worst-case relative regret of order $(\log n)^{1/2}n^{-1/4}$ in a market of size $n$.

Setting

Prices. Fix $0<\underline p<\overline p<\infty$ and an off price $p_\infty>0$ outside $[\underline p,\overline p]$. The seller may charge any price in $[\underline p,\overline p]\cup\{p_\infty\}$; charging $p_\infty$ stops demand.

Demand. Requests arrive as a Poisson process whose intensity at time $t$ is $\lambda(p(t))$. Let $N$ be a unit-rate Poisson process. By the time change (1), the cumulative requests up to time $t$ under a price path $p(\cdot)$ are $N\big(\int_0^t\lambda(p(s))\,ds\big)$. The seller starts with inventory $x$ and sells until either the horizon $T$ ends or the stock runs out. The expected revenue of a policy $\pi$ is $J^\pi(x,T;\lambda)$.

Demand class. $\mathcal L=\mathcal L(M,\underline K,\overline K,m)$ is the set of regular demand functions satisfying Assumption 1. Regular means:

• $\lambda\ge0$ and $\lambda(p_\infty)=0$;
• $\lambda$ is non-increasing on $[\underline p,\overline p]$, with inverse $\gamma$;
• the revenue rate $r(l)=l\gamma(l)$ is concave.

Assumption 1 requires:

• (i) $\lambda\le M$ on $[\underline p,\overline p]$;
• (ii) $\lambda$ is $\overline K$-Lipschitz and $\gamma$ is $\underline K^{-1}$-Lipschitz;
• (iii) $\max_p p\lambda(p)\ge m$.

Benchmark. The deterministic relaxation (5) replaces the random demand by its mean:

$$J^D(x,T\mid\lambda)=\sup\Big\{\int_0^T p(s)\lambda(p(s))\,ds:\int_0^T\lambda(p(s))\,ds\le x\Big\}.$$

The regret of a policy is $\mathcal R^\pi=1-J^\pi/J^D$.

Scaling. In a market of size $n$ the inventory is $nx$ and the demand function is $n\lambda$, as in (11). The corresponding quantities are $J^\pi_n$, $J^D_n=nJ^D$ and $\mathcal R^\pi_n$.

Algorithm 1, $\pi(\tau,\kappa)$. The policy has three phases.

1. Learning. On $[0,\tau]$ it tests $\kappa$ equally spaced prices $p_i=\underline p+(i-1)(\overline p-\underline p)/\kappa$, each for $\Delta=\tau/\kappa$ time units. It estimates $\lambda(p_i)$ by the normalized request counts $\hat\lambda(p_i)$.
2. Optimization. It chooses $\hat p^u=\arg\max_i p_i\hat\lambda(p_i)$ and $\hat p^c=\arg\min_i|\hat\lambda(p_i)-x/T|$, and sets $\hat p=\max\{\hat p^u,\hat p^c\}$.
3. Pricing. It charges $\hat p$ on $(\tau,T]$ until the stock runs out.

Formalization targets

Goal: Proposition 1

Let $\tau_n\asymp n^{-1/4}$ and $\kappa_n\asymp n^{1/4}$, and let $\pi_n=\pi(\tau_n,\kappa_n)$. Then there is a finite constant $C$, independent of $\lambda$ and $n$, such that

$$\sup_{\lambda\in\mathcal L}\mathcal R^{\pi}_n(x,T;\lambda)\le\frac{C(\log n)^{1/2}}{n^{1/4}}\qquad(n\ge2).$$

The constant is left unspecified, as in the paper. Its dependence on the class parameters, $x$ and $T$ is "somewhat complex" (p. 12), and the order $(\log n)^{1/2}n^{-1/4}$ is the content of the result.

Milestones

The milestones follow the proof in the appendix, in order:

• the scaling $J^D_n=nJ^D$ (p. 12);
• Fact 1, $J^D\ge m\min\{T,x/M\}$ on $\mathcal L$;
• Lemma 1, the solution of (5): charge $p^D=\max\{p^u,p^c\}$ until the stock runs out;
• Lemma 2, a Poisson deviation bound;
• the revenue lower bound (A-2);
• Lemma 3, the learned price is near $p^D$ with high probability;
• Lemma 4 and the Case 1 bound (A-11), for $\lambda(\overline p)\le x/T$;
• Lemma 5 and the Case 2 bound (A-15), for $\lambda(\overline p)>x/T$;
• the Step 4 bound $\mathcal R^\pi_n\le C_{12}(u_n+\tau_n)$, where $u_n=(\log n)^{1/2}\max\{1/\kappa_n,(n\Delta_n)^{-1/2}\}$.

Significance

Proposition 1 shows that a seller who knows only a nonparametric class of demand functions can approach the full-information revenue uniformly over the class. Learning costs a vanishing fraction of revenue, and the policy needs no parametric model. Together with the paper's lower bound of order $n^{-1/2}$ for every admissible policy (Proposition 2, not in this mission), it brackets the minimax regret of nonparametric pricing under an inventory constraint. The result is a reference point for the learning-and-earning literature in operations management that followed it.

The result is proved in the paper; to our knowledge, it has no machine-checked proof. Formalizing it requires:

• a working theory of policies driven by a time-changed Poisson process, with sales capped by an inventory;
• the deterministic relaxation of Gallego and van Ryzin for a continuum of prices with an off price;
• uniform (over the class) Poisson concentration bounds.

The mission produces Lean statements of all of these. A proof would also check every constant chain of the appendix, where the argument uses some displays in a form slightly different from their printed statement (see the scope section).

Difficulty

The obvious argument controls the estimation error at the tested prices and concludes that $\hat p$ is close to the optimal price. It breaks in two places.

First, $p^D$ is the larger of two prices, the revenue maximizer and the price that sells the inventory exactly. Near the boundary between these regimes, the revenue rate at $\hat p$ is not controlled by the error in $\hat p$ alone: it needs the concavity of the revenue rate and the inverse Lipschitz bound on $\gamma$.

Second, when demand at the highest price exceeds the inventory rate ($\lambda(\overline p)>x/T$), the revenue is limited by stock-outs rather than by the price. The bound must then show that nearly all of the inventory is sold during the pricing phase, uniformly over the class.

Throughout, every constant must be independent of the demand function, so the estimates have to hold uniformly over an infinite-dimensional class.

Formalization scope

• Poisson process. The demand is driven by IsPoissonProcess N 1 on a probability space $(\Omega,\mathbb P)$, a published platform definition: ℕ-valued, $N(0)=0$, monotone paths, independent Poisson increments. The time change (1) is rendered by evaluating $N$ at cumulative intensities.
• Inventory. The inventory of the market of size $n$ is $\lfloor nx\rfloor$ units, and sales are $\min\{N(\cdot),\lfloor nx\rfloor\}$. The cap is never dropped.
• Revenue. $J^\pi_n$ is the Bochner expectation of a bounded, finitely-valued revenue, so it is a genuine integral.
• Demand functions. A demand function is a map $\mathbb R\to\mathbb R$, nonnegative, with $\lambda(p_\infty)=0$. Regularity and Assumption 1 are imposed on $[\underline p,\overline p]$, and the inverse $\gamma$ is Function.invFunOn.
• Benchmark. $J^D$ is a supremum over measurable price paths with integrable demand rate. The supremum is genuine: the set of path revenues is nonempty and bounded.
• Algorithm. The grid excludes $\overline p$, as in the paper. Ties in the grid argmax and argmin go to the smallest index. The estimates compare $\hat\lambda(p_i)$ with $x/T$.
• Tuning. $\tau_n\asymp n^{-1/4}$ and $\kappa_n\asymp n^{1/4}$ are encoded with explicit constants $0<c\le c'$, with $\tau_n\in(0,T]$ and $\kappa_n\ge1$. Constants may depend on $c,c'$, the class parameters, the prices, $x$ and $T$, but never on $\lambda$ or $n$.
• Range of $n$. Bounds whose right side vanishes at $n=1$ because $\log1=0$ are stated for $n\ge2$: the goal and (A-15).
• Typo correction. Lemma 5's event uses $nx-C_9nu_n$, as in its proof, not the printed $nx-C_9u_n$.
• Ruled out. A specific demand curve, a fixed $n$, deterministic demand, a finite price set, a known $\lambda$, constants depending on $\lambda$, or dropping the inventory cap would each make the statement a different and easier theorem. None is used.
• Not included. The lower bound of Proposition 2 and the second assertion of Lemma 1 ($J^\pi\le J^D$ for all admissible policies) are not included.

Contributions are welcome at any level: proofs of the milestones (Fact 1, Lemma 1 and Lemma 2 are self-contained), measurability and integrability lemmas for the revenue functional, and a reusable Poisson concentration library built on Mathlib's poissonMeasure.

Selected references

• O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
• 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
• K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000

Why average cost is a control problem

A controller acting over an indefinite horizon must decide whether a lower cost today is worth a higher cost later. Average cost measures the expected expenditure per stage as the horizon grows. It is appropriate when operation has no natural terminal date, but its limiting definition makes it difficult to compute an optimal policy directly. Discounted cost assigns less weight to distant stages and has a more direct optimality equation. Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus survey these criteria for controlled Markov processes and state a condition under which solving one discounted problem yields a solution to an average-cost problem (Arapostathis et al., 1993, §5.1).

The condition is a common lower bound on the one-step probability of moving to a distinguished state. Ross's reduction, reported as Theorem 5.6 of the survey, uses that bound to define a new transition law and a specific discount factor. The survey's theorem states the reduction informally; its proof specifies the transformed law, the optimality equation and the resulting average-cost policy. Those claims are the targets of this mission (Arapostathis et al., 1993, pp. 303–304).

Controlled process and criteria

The state space is $S=\{0,1,2,\ldots\}$. In state $i$, the controller may choose an action $a$ from a nonempty compact set $U(i)$ in a metric action space. Choosing $a$ incurs the one-stage cost $c(i,a)\ge0$ and moves the state to $j$ with probability $P(j\mid i,a)$. The cost is measurable, and for each fixed $i,j$ its value and $P(j\mid i,a)$ vary continuously with $a$ on $U(i)$. Section 5 imposes these state and continuity conventions; §5.1 additionally assumes the costs are bounded (Arapostathis et al., 1993, pp. 284–288, 299, 301).

An admissible policy $\pi$ chooses a probability law for the next action from the entire observed history, and assigns probability one to admissible actions. A stationary deterministic policy is a map $f$ with $f(i)\in U(i)$; it always takes action $f(i)$ in state $i$. These are distinct classes. Let $J_N(i,\pi)$ be expected cost over the first $N$ stages from $i$, and let $J_\beta(i,\pi)$ be expected cost when stage $t$ is weighted by $\beta^t$, where $0<\beta<1$. The average-cost criterion is $J(i,\pi)=\limsup_{N\to\infty}J_N(i,\pi)/N$. The optimal values $J^*(i)$ and $J_\beta^*(i)$ are infima over all admissible policies, including randomized and history-dependent ones (Arapostathis et al., 1993, pp. 285–287).

The average cost optimality equation, or ACOE, asks for a scalar $\rho$ and a real function $h$ such that, for each state $i$,

$$\rho+h(i)=\min_{a\in U(i)}\left\{c(i,a)+\sum_{j\in S}P(j\mid i,a)h(j)\right\}.$$

The minimum is attained. The survey's verification theorem identifies $\rho$ with the optimal average cost when the terminal contribution of $h(X_t)$ vanishes after division by $t$ (Arapostathis et al., 1993, p. 299, (5.1), Theorem 5.1).

Formalization targets

The reduction

Assume that $P(0\mid i,a)\ge\alpha$ on every admissible state-action pair for a single constant $0<\alpha<1$. The transformed process $\widetilde M$ has the same admissible actions and costs and has transition probabilities

$$\widetilde P(j\mid i,a)=\frac{P(j\mid i,a)-\alpha\mathbf1_{\{j=0\}}}{1-\alpha}.$$

Write $\widetilde J^*_{1-\alpha}$ for its discounted value at discount factor $1-\alpha$. The goal states that this value is finite, a stationary deterministic discounted-optimal policy exists, and every such policy is average-cost optimal for the original process. It also identifies a constant optimal average cost for every initial state:

$$J^*(i)=\alpha\widetilde J^*_{1-\alpha}(0),\qquad i\in S.$$

The goal does not assume the average optimality that it asserts. It requires the transformed law to satisfy the displayed formula at every admissible state-action pair (Arapostathis et al., 1993, Theorem 5.6 and proof, pp. 303–304).

Supporting targets

The milestones establish that the transformed law gives a controlled Markov process, that the discounted problem has an optimal stationary deterministic policy, and that the transformed discounted value satisfies the original ACOE with $\rho=\alpha\widetilde J^*_{1-\alpha}(0)$. The final milestone is the ACOE verification theorem needed to identify the average cost. The source gives the first two discounted claims through Theorem 2.1 and writes out the transformed equation in the proof of Theorem 5.6 (Arapostathis et al., 1993, pp. 289, 299, 304).

What the result supplies

The theorem replaces an average-cost optimization problem by one discounted problem with a prescribed discount factor and transition law. It yields a stationary deterministic policy that is optimal even when compared with every history-dependent randomized policy, and it shows that the optimal average cost is independent of the initial state. Without the common return probability, neither this particular law nor this fixed discount factor follows from the survey's argument (Arapostathis et al., 1993, Theorem 5.6).

The survey reports this as a known result of Ross rather than an open conjecture. The formalization work is to give the path measures, value functions, transformed process and verification result machine-checkable meanings. The Lean declarations here are open theorem statements awaiting proofs; compiling a statement with sorry does not establish the mathematical theorem. The policy and cost definitions can also support the other countable-state missions drawn from §5.

Difficulty

The transformed probabilities have to form a measurable stochastic kernel, preserve the action continuity assumptions and yield a controlled process with the original feasible actions and costs. The discounted value must be finite and uniformly bounded before its real form can enter the ACOE. A simple comparison of numerical optimal values is insufficient: a policy chosen in the transformed model must be shown optimal for the original model against the full policy class. The verification theorem also requires control of the terminal expectation of $h(X_t)$ for arbitrary admissible policies, rather than only the stationary policies named in its printed condition (Arapostathis et al., 1993, pp. 299–300, 304).

Formalization scope

Lean uses $\mathbb N$ for the countable state space and Mathlib probability kernels for the transition and randomized decision rules. Strategic path measures are constructed from those kernels. Nonnegative expected costs and their infima live in $[0,\infty]$, so an unbounded integral cannot silently become a finite real value. The transformed discounted value is converted to a real only in conclusions that also assert its finiteness. The ACOE uses real sums with explicit summability and an attained minimum. The model requires a Borel metric action space, nonempty compact action sets, measurable costs, and coordinatewise action continuity of the transition probabilities.

The source's §5.1 bounded-cost assumption is explicit in the goal and its discounted milestones. The displayed transformation needs $\alpha<1$; the paper's theorem sentence gives only $\alpha>0$, so the case $\alpha=1$ is excluded from this version. The paper prints (5.2) for stationary deterministic policies, but the proof uses it for all admissible policies to compare with $J^*$; the verification milestone takes the stronger, proof-supported hypothesis. Expectations in that condition are explicitly integrable. The converse part of Theorem 5.1 is not used and is outside this mission.

The transformed process is represented by another CMP constrained to have exactly the source's action sets, admissible costs and transition formula. A milestone poses its existence. This representation keeps the definition layer free of an unproved stochastic-kernel construction. The discount-optimal policy conclusion ranges over every stationary deterministic policy attaining the transformed discounted value, while the values themselves take infima over all admissible policies. Definitions of admissible path laws and the verification theorem are reusable contributions; proofs of the transformed kernel, stationary discounted existence and ACOE identity are welcome.

Selected references

• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh and S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM Journal on Control and Optimization 31(2), 282–344, 1993. DOI: 10.1137/0331018.

Why learn demand while pricing?

A seller with a fixed inventory must choose prices before knowing how customers respond to them. A price that earns a high margin can sell too slowly; a price that sells quickly can exhaust stock before the selling season ends. Learning demand uses time and inventory, so the seller must account for the cost of its own experiments. This mission formalizes the parametric policy and regret bound of Besbes and Zeevi (2009), Proposition 3. Their setting differs from a finite-arm bandit: the permitted ordinary prices form an interval, customer arrivals are random, and the available stock caps total sales.

The paper first analyzes a nonparametric class with a slower upper bound in Proposition 1, then imposes a known finite-dimensional form on the unknown demand curve in Section 5. Proposition 3 shows how that additional information improves the regret rate for its Algorithm 2. The authors also prove a lower bound for a suitable parametric family in Proposition 4; that result is outside this mission's capstone, which concerns the performance guarantee of the concrete policy.

Market, demand, and policy

The selling horizon has length $T>0$, and the initial stock is $x>0$. An ordinary price $p$ lies in $[\underline p,\overline p]$, with $0<\underline p<\overline p$. The special price $p_\infty>0$ stops demand. At parameter $\theta\in\Theta\subseteq\mathbb R^k$, the demand rate is $\lambda(p;\theta)\ge0$. The parameter set $\Theta$ is nonempty, compact, and convex; $k$ is positive. The seller knows the family $\lambda(\cdot;\theta)$ but does not know the true parameter $\theta^*$.

For each parameter, demand is nonincreasing in the price and has an inverse $\gamma(\cdot;\theta)$ on the attainable rate interval. The rate revenue is $r(\ell;\theta)=\ell\gamma(\ell;\theta)$, a concave function of the rate. Every member of the family satisfies Assumption 1 with the same positive constants $M,\underline K,\overline K,m$: demand is at most $M$, its price variation is at most $\overline K$ times the price difference, its inverse is $\underline K^{-1}$-Lipschitz, and some ordinary price earns revenue rate at least $m$. These conditions define the class in which the bound is uniform. See §§3–4.2 of the source.

Customer requests follow a unit-rate Poisson process $N$ run on a demand-dependent clock. Under price $p(t)$, cumulative requests at time $t$ equal $N(\int_0^t\lambda(p(s);\theta^*)\,ds)$. The market of size $n$ has stock $nx$ and rate $n\lambda$. Sales stop when stock runs out. The deterministic relaxation $J_n^D$ is the best integrated rate revenue over measurable price paths satisfying the expected-demand stock constraint, with the same scaling. The policy revenue $J_n^\pi$ is its expected sales revenue, and its relative regret is $R_n^\pi=1-J_n^\pi/J_n^D$. Fact 1 states $J_n^D=nJ^D$ and gives a positive uniform lower bound on $J^D$.

Assumption 2 selects $k$ distinct ordinary test prices. Their mean rates identify the parameter through a Lipschitz inverse map $g$, and demand changes at most $\overline K_2\|\theta-\theta'\|_\infty$ as the parameter varies. The square root of each test-price rate is differentiable on $\Theta$. Algorithm 2 spends $\tau_n$ time units testing these prices in equal subintervals, estimates each rate from its Poisson count increment, and sets $\widehat\theta=g(\widehat d)$. It then posts $\widehat p=\max\{p^u(\widehat\theta),p^c(\widehat\theta)\}$, where $p^u$ maximizes revenue rate and $p^c$ minimizes the distance of demand to $x/T$. It keeps that price until time $T$ or stock-out. See §5.1–5.2.

Formalization targets

The capstone is the uniform bound in Proposition 3, equation (17). With $\tau_n\asymp n^{-1/3}$, the mission asks for one constant $C>0$, independent of $n$, $\theta^*$, the optimizer choices, and the probability space, such that

$$\forall\theta^*\in\Theta,\qquad R_n^\pi(x,T;\theta^*)\le C\frac{\sqrt{\log n}}{n^{1/3}}\quad(n\ge2).$$

The intermediate quantitative target is equation (A-25), which retains the learning time:

$$R_n^\pi\le\frac{C_3}{m^D}\left(\tau_n+\frac{\sqrt{\log n}}{\sqrt{n\tau_n}}\right),\qquad m^D=m\min\{T,x/M\}.$$

The milestone list also carries Fact 1, the optimal deterministic price path and value from the first assertion of Lemma 1, both Poisson tails of Lemma 2, the pricing-phase revenue bound (A-17), the deterministic stability bounds (A-19), (A-22), and (A-23), and the parameter-estimation bound of Lemma 6. The paper's assertion that the policy is “asymptotically optimal” follows from the displayed regret estimate together with nonnegative regret; the displayed numerical estimate is the formal goal.

What the result provides

A finite-dimensional demand model lets the seller learn from a fixed set of $k$ prices rather than probing an increasingly fine price grid. Proposition 3 quantifies the resulting revenue loss at $O(\sqrt{\log n}\,n^{-1/3})$, compared with the paper's $O(\sqrt{\log n}\,n^{-1/4})$ upper bound for its nonparametric learn-then-price policy. Both guarantees compare actual expected revenue with the full-information deterministic benchmark, including stock-out. These rates are proved in the article; the mission seeks machine-checked Lean proofs of the stated model, auxiliary bounds, and capstone. No such proof is claimed here.

The formalization would also provide reusable interfaces for a unit-rate Poisson counting process, deterministic inventory-constrained revenue optimization, measurable price selectors, and a random price chosen from normalized count observations. The later single-parameter policy in the paper uses related ideas but is a separate mission with different stages and a different rate.

Main difficulty

A rate estimate can be close to the true rate while the selected price changes between two different optimizers: the unconstrained revenue maximizer and the price that matches inventory to expected demand. A bound for only one optimizer does not control the maximum of the two. The learning price is random, and the number of requests in the pricing phase is evaluated at a random Poisson clock. Stock-out further couples the learning phase to the amount available for later sales. These features prevent a direct substitution of an ordinary parameter-estimation bound into the final revenue formula.

Formalization scope

Lean uses $\mathrm{Fin}(k)\to\mathbb R$ with its sup norm for parameter vectors, a finite positive off price, and a Poisson process on an arbitrary probability space. Each demand curve is defined on all real prices but is constrained on $[\underline p,\overline p]$ and at $p_\infty$; the inverse and concavity conditions apply on the attainable rate interval. The deterministic benchmark is a real supremum over measurable, integrable admissible price paths. The class assumptions make its value nonempty and bounded. Policy revenue uses a nonnegative integral of pathwise revenue, avoiding a default zero from a nonintegrable signed expectation.

Inventory is measured in whole units, so the cap is $\lfloor nx\rfloor$, equal to the paper's $nx$ when that quantity is integral. Test-price observations remain uncapped in the formula for $\widehat d$; if stock runs out during learning, capped later sales are already zero. The continuous optimizer choices are measurable selections satisfying the actual max/min properties for every member of $\Theta$. The bound is uniform over these choices and over all unit-rate Poisson processes.

The printed Assumption 2(i)b asks for a solution to the test-rate equations for every vector in $\mathbb R^k$. Such a solution cannot always lie in compact $\Theta$, although the proof applies Assumption 2(ii) to $\widehat\theta$. Here $g$ is a Lipschitz map into $\Theta$ that recovers each true parameter from its test-rate vector; it can be viewed as the unconstrained inverse followed by a nonexpansive projection in the paper's box example. This explicit convention is required to make the estimate and subsequent use of Assumption 2(ii) coherent. It is an interpretive repair of the printed condition.

The paper prints the regret bound for $n\ge1$, where $\sqrt{\log1}=0$. The exploration policy can lose revenue at $n=1$, so the formal theorem starts at $n\ge2$. The comparison $\tau_n\asymp n^{-1/3}$ is encoded by positive lower and upper multipliers after a fixed threshold, with $0<\tau_n\le T$ for all relevant market sizes. This admits the usual finite initial adjustments and leaves the bound uniform over the sequence. No fixed demand curve, known parameter, finite price grid, or uncapped sales model can satisfy this target by substitution.

Selected references

• Omar Besbes and Assaf Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6), 2009, authors' final manuscript revised December 16, 2007. DOI: 10.1287/opre.1080.0640.

Motivation

The problem $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ asks for a single-machine sequence of jobs, respecting precedence constraints, that minimizes the weighted sum of completion times. It has been known to be strongly NP-hard since Lawler (1978) and Lenstra and Rinnooy Kan (1978), several different 2-approximation algorithms are known, and closing the approximability gap is listed by Schuurman and Woeginger (1999) as one of ten outstanding open problems in scheduling theory. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) give the first inapproximability result for this problem: under a widely believed complexity assumption it has no polynomial-time approximation scheme (PTAS). The bridge to that result is a quantitative link, Lemma 9.1, between the optimal value of a special bipartite scheduling instance and the maximum edge biclique of a bipartite graph, a problem whose hardness of approximation was established by Ambühl, Mastrolilli and Svensson (FOCS 2007). This mission formalizes that link.

Setting

A schedule of a finite job set is a sequence $\sigma$ listing every job once; the machine processes the jobs in that order from time $0$ without idle time or pre-emption. Job $j$ has a processing time $p_j$ and a weight $w_j$; its completion time $C_j$ is the sum of the processing times of the jobs up to and including $j$, and the value of $\sigma$ is $\mathrm{val}(\sigma)=\sum_j w_jC_j$. Precedence constraints are a relation $P$ on jobs: $(i,j)\in P$ with $i\ne j$ means job $i$ must be completed before job $j$ starts. A schedule respecting all of them is feasible, and a feasible schedule $\sigma^*$ of least value is optimal.

Let $G=(U,V,E)$ be an $n$-by-$n$ bipartite graph: $|U|=|V|=n$ and $E\subseteq U\times V$. An edge biclique is a pair $A\subseteq U$, $B\subseteq V$ with $A\times B\subseteq E$, of value $|A|\cdot|B|$; the maximum edge biclique problem (Definition 9.1) asks for one of largest value. The bipartite scheduling instance $S_G$ has jobs $U\cup V$ and precedence constraints

$$P=(U\times V)\setminus E,$$

so $u\in U$ must precede $v\in V$ exactly when $(u,v)$ is not an edge. Jobs of $U$ have $p=1$, $w=0$; jobs of $V$ have $p=0$, $w=1$. Thus $\mathrm{val}(\sigma)=\sum_{v\in V}C_v$, where $C_v$ is the number of $U$-jobs scheduled before $v$. For $i\ge1$, $\sigma(i)$ denotes the number of $V$-jobs scheduled before $i$ jobs of $U$ have been scheduled.

In the Lean development these are weightedCompletion, IsOptimalSchedule, IsEdgeBiclique, maxBicliqueValue, precSG, procSG, weightSG, valSG, IsOptimalSG and vBefore in the namespace SingleMachinePrec.Biclique.

Formalization targets

Goal: Lemma 9.1 (p. 666)

If a maximum edge biclique of $G$ has value $an^2$ with $a\in(0,1]$, then $S_G$ has an optimal schedule and every optimal schedule $\sigma^*$ satisfies

$$n^2-an^2\Bigl(\ln\frac1a+2\Bigr)\le\mathrm{val}(\sigma^*)\le n^2-an^2 .$$

Milestones (proof of Lemma 9.1, §9, p. 666)

1. For every edge biclique $(A,B)$, a schedule in the block order $U\setminus A\to B\to A\to V\setminus B$ exists, and every such schedule is feasible with

$$\mathrm{val}(\sigma)=n^2-|A|\cdot|B| .$$

2. For every schedule, $\sigma(n+1)=n$ and

$$\mathrm{val}(\sigma)=\sum_{i=1}^n\bigl(\sigma(i+1)-\sigma(i)\bigr)i=n^2-\sum_{i=1}^n\sigma(i).$$

3. For every feasible schedule and $i=1,\dots,n$,

$$\sigma(i)(n-i+1)\le an^2,\qquad \sigma(i)\le n .$$

Significance

Lemma 9.1 shows that the optimal value of $S_G$ determines the maximum edge biclique of $G$ up to a factor of order $\ln(1/a)$ in the "area above the work line" $n^2-\mathrm{val}(\sigma^*)$. Combined with the hardness of approximating maximum edge biclique (Theorem 9.1, cited from Ambühl, Mastrolilli and Svensson 2007) it yields Theorem 9.2: $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ has no PTAS unless SAT can be decided by a probabilistic algorithm in time $2^{N^\epsilon}$ for every $\epsilon>0$. It also makes precise the two-dimensional Gantt chart picture of Eastman, Even and Isaacs (1964) and of Goemans and Williamson (2000), in which every point on the work line of a schedule defines an edge biclique.

The lemma is proved in the paper; it is not formalized anywhere to our knowledge. A formal proof certifies the combinatorial core of the no-PTAS result independently of the complexity-theoretic layer, and its definitions (the bipartite instance $S_G$, edge bicliques, the profile $\sigma(i)$) are reusable for the gap inequality behind Theorem 9.2.

Difficulty

The upper bound is a direct computation on one explicit schedule. The lower bound is a statement about every feasible schedule, of which there are exponentially many, and it must hold with the explicit constant $2$ and the factor $\ln(1/a)$ for every $a\in(0,1]$. The printed argument splits the sum at $i=(1-a)n$ and uses $\lfloor an\rfloor$, treating $an$ as an integer; for general $a$ (for example $n=3$, value $2$, $an=2/3$) the split point is not an integer, so the printed estimate does not apply verbatim and the constant $2$ has to be re-checked for non-integral $an$. On the formal side, the value identity requires relating completion times in a list to counting $U$-jobs before each $V$-job, with ties among zero-length jobs.

Formalization scope

Jobs are the disjoint union U ⊕ V of two finite types with Fintype.card U = Fintype.card V = n; $E$ is a relation U → V → Prop. A schedule is a duplicate-free list containing every job; feasibility is the published LawlerPrec.MinMax.IsFeasible and completion times are the published MooreLateJobs.Shared.completionTime (time $0$ start, no idle time). Processing times and weights are reals, here in $\{0,1\}$. The maximum edge biclique value is the maximum of $|A|\cdot|B|$ over all edge bicliques, the empty ones included, so the hypothesis $a>0$ means $E\ne\emptyset$. The logarithm is natural (Real.log).

Conventions and readings committed to:

• The goal is stated for every optimal schedule, and the existence of an optimal schedule is a separate conclusion, so the bounds cannot hold vacuously. Proving the bounds for one particular schedule, or for an optimal value defined as an infimum that could be a junk default, would not be this lemma.
• No integrality hypothesis on $an$ is added.
• Milestones 2 and 3 are stated for every schedule (respectively every feasible schedule), not only for $\sigma^*$; milestone 1 states the value of the block-order schedule as an equality, where the paper writes "$\le\cdots=$".
• The paper's $P=(U\times V)\setminus E$ is irreflexive; feasibility only constrains distinct jobs, so it agrees with the reflexive partial order of §1.

Not formalized: Theorem 9.1 (cited hardness of maximum edge biclique) and Theorem 9.2 (no PTAS under a complexity assumption); no polynomial-time or complexity-theoretic statement appears in the mission. Contributions welcome: proofs of the three milestones and of the goal; Mathlib's bounds on harmonic numbers (Mathlib/NumberTheory/Harmonic/Bounds.lean) are the relevant library.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, O. Svensson, Inapproximability results for sparsest cut, optimal linear arrangement, and precedence constraint scheduling, Proc. 48th IEEE FOCS, 329–337, 2007 (reference [4] of the paper).
• W. L. Eastman, S. Even, I. M. Isaacs, Bounds for the optimal scheduling of n jobs on m processors, Management Science 11(2):268–279, 1964 (reference [11]).
• M. X. Goemans, D. P. Williamson, Two-dimensional Gantt charts and a scheduling algorithm of Lawler, SIAM J. Discrete Math. 13(3):281–294, 2000 (reference [15]).
• P. Schuurman, G. J. Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 2(5):203–213, 1999 (reference [36]).

Motivation

Controlled Markov processes with the average cost criterion model systems that run indefinitely, such as queues, inventories, maintenance and communication networks, where only the long-run cost per unit time matters. The standard route to an optimal stationary policy goes through the average cost optimality equation (ACOE). The ACOE is usually obtained by the vanishing discount method: solve the discounted problem for each discount factor $\beta<1$ and let $\beta\to1$. The method works only when the differences of discounted values stay bounded as $\beta\to1$. Conditions that guarantee this are therefore central in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993), §5).

This mission formalizes one such condition, due to Ross: if the mean return time to a fixed state is bounded uniformly over all stationary policies and initial states, the differential discounted value functions are bounded uniformly in the discount factor and the state.

Timeline. Derman (Management Sci. 9 (1962); survey reference [38]) and Derman–Veinott (Ann. Math. Statist. 38 (1967); survey reference [43]) introduced recurrence conditions of this kind for countable-state processes. Ross (Ann. Math. Statist. 39 (1968), survey reference [147]; Introduction to Stochastic Dynamic Programming, 1983, survey reference [150]) showed, for bounded costs, that under a Derman–Veinott type recurrence condition $h_\beta$ is bounded uniformly in $\beta$, and obtained a bounded solution of the ACOE by letting $\beta\uparrow1$ (survey, pp. 291 and 301). Later work replaced the condition with weaker ones (survey Assumptions 5.1–5.3) and with Sennott's conditions (survey Theorem 5.9).

Setting

The state space is $S=\{0,1,2,\dots\}$. In each state $i$, an action $a$ is chosen from a nonempty compact set $U(i)$ of a metric space $A$. The one-stage cost $c(i,a)$ is nonnegative and the next state is drawn from the transition law $P(\cdot\mid i,a)$. For fixed $i,j$, the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$. A policy $\pi\in\Pi$ chooses the action at time $t$ at random, given the whole history, and must choose from $U(X_t)$. A stationary deterministic policy $f\in\Pi_{SD}$ is a map $f:S\to A$ with $f(i)\in U(i)$. $P^\pi_i$ and $E^\pi_i$ denote the law and the expectation of the controlled process $(X_t,A_t)$ started at $i$.

For a discount factor $\beta\in(0,1)$, the discounted cost and the optimal discounted cost are

$$J_\beta(i,\pi)=E^\pi_i\Big[\sum_{t=0}^\infty\beta^t c(X_t,A_t)\Big],\qquad J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi).$$

A policy $f\in\Pi_{SD}$ is $\beta$-discount optimal if $J_\beta(i,f)=J^*_\beta(i)$ for all $i$. The differential discounted value function is

$$h_\beta(i)=J^*_\beta(i)-J^*_\beta(0),$$

measured relative to the fixed state $0$. The return time to $0$ is

$$\tau=\min\{t\ge1:\ X_t=0\},$$

with $\tau=\infty$ if the process never returns. Throughout, as in §5.1 of the survey, the cost is bounded: $c(i,a)\le M$ on admissible pairs.

Formalization targets

Goal: Theorem 5.3

If there is a constant $K>0$ with

$$E^f_i[\tau]<K\qquad\text{for all } f\in\Pi_{SD},\ i\in S, \tag{5.7}$$

then there is a constant $B$ such that

$$|h_\beta(i)|\le B\qquad\text{for all }\beta\in(0,1),\ i\in S.$$

This is the theorem as printed: it asserts only uniform boundedness and fixes no constant.

Milestones

1. Theorem 2.1 (iii): for every $\beta\in(0,1)$, a $\beta$-discount optimal $f_\beta\in\Pi_{SD}$ exists.
2. (5.8): for such an $f_\beta$, $J^*_\beta(i)\le M\,E^{f_\beta}_i[\tau]+J^*_\beta(0)\,E^{f_\beta}_i[\beta^\tau]$.
3. (5.9): $J^*_\beta(i)-\beta J^*_\beta(0)\le MK$.
4. Jensen step: $J^*_\beta(i)\ge J^*_\beta(0)\,E^{f_\beta}_i[\beta^\tau]\ge J^*_\beta(0)\,\beta^K$.
5. (5.10): $J^*_\beta(0)-J^*_\beta(i)\le(1-\beta^K)J^*_\beta(0)\le(1-\beta^K)\frac{M}{1-\beta}\le MK$.
6. Explicit bound: $|h_\beta(i)|\le MK$. This is stronger than the goal and is the constant the survey's argument yields.

Significance

The result. Theorem 5.3 verifies the hypothesis of the vanishing discount theorem (Theorem 5.2 of the survey) from a condition on the uncontrolled dynamics of stationary policies. Theorem 5.2 then gives a bounded solution $(\rho,h)$ of the ACOE, an average optimal stationary policy, and the limit $\lim_{\beta\to1}(1-\beta)J^*_\beta(i)=\rho$. Mean return times can often be estimated directly, for instance through Foster–Lyapunov drift arguments on queues, which makes (5.7) checkable in applications. The explicit bound $MK$ also controls the span of the relative value function.

Formalizing it. The result is proved in the literature; to our knowledge it has not been machine-checked. A formal proof needs discounted dynamic programming on a countable state space with compact action sets, the existence of optimal stationary policies (Theorem 2.1 (iii), which the survey cites without proof), and the strong Markov property of the controlled chain at a return time. All of these are reusable well beyond this mission.

Difficulty

The estimates (5.9) and (5.10) are elementary once (5.8) and the existence of $f_\beta$ are available. The weight lies elsewhere.

• Optimal stationary policies. The infimum defining $J^*_\beta$ ranges over all history-dependent randomized policies. Bringing it down to a single stationary deterministic policy requires the discounted optimality equation, a measurable selection of minimizers on compact action sets, and a verification argument against arbitrary policies.
• Restarting at $\tau$. (5.8) splits the discounted cost at the random time $\tau$. The tail must be identified with $\beta^\tau$ times the discounted cost from state $0$. This is the strong Markov property for the process built by the Ionescu-Tulcea theorem, applied at a stopping time that may be infinite.

Formalization scope

• The state space is ℕ; the action space is a metric space with its Borel $\sigma$-algebra. The model CMP carries compact nonempty $U(i)$, a nonnegative measurable cost, and continuity of $c(i,\cdot)$ and $P(j\mid i,\cdot)$ on $U(i)$, the standing assumptions of §5.
• Policies are history-dependent, randomized and admissible. The path measure is Mathlib's Kernel.trajMeasure. $J^*_\beta$ is an infimum over all such policies, not over Markov or stationary policies only.
• Costs are lower Lebesgue integrals in $[0,\infty]$. $h_\beta$ is the difference of the real parts of $J^*_\beta(i)$ and $J^*_\beta(0)$. This is exact here because bounded cost gives $J^*_\beta\le M/(1-\beta)<\infty$.
• Explicit choices:
  • The bounded-cost hypothesis $c\le M$ on admissible pairs is a binder of every §5.1 statement. It is the section's standing assumption, and without it the theorem is false.
  • $\tau$ counts from $t\ge1$ and takes values in $\mathbb N\cup\{\infty\}$, so (5.7) applies from $i=0$ and forces $\tau<\infty$ almost surely; $\beta^\tau=0$ on $\{\tau=\infty\}$.
  • The typo $\beta^n$ in (5.8) is read as $\beta^t$.
  • $K\ge1$ in (5.10) is not assumed; it follows from (5.7).
• Theorem 2.1 is stated in the survey for Borel models under Assumptions 2.1–2.3. Here it is posed in the countable model, where those assumptions follow from the §5 continuity and compactness assumptions.
• The goal's bound $B$ is quantified before $\beta$ and $i$. A per-$\beta$ or per-state bound would be trivial, since every $h_\beta(i)$ is a finite number.
• Welcome contributions include discounted dynamic programming on countable state spaces, the strong Markov property for trajMeasure, and return-time estimates.

Selected references

• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
• C. Derman, On sequential decisions and Markov chains, Management Sci. 9 (1962) 16–24. https://doi.org/10.1287/mnsc.9.1.16
• C. Derman, A. F. Veinott Jr., A solution to a countable system of equations arising in Markovian decision processes, Ann. Math. Statist. 38 (1967) 582–584 (cited as [43] in the survey, https://doi.org/10.1137/0331018).
• S. M. Ross, Non-discounted denumerable Markovian decision models, Ann. Math. Statist. 39 (1968) 412–423 (cited as [147] in the survey, https://doi.org/10.1137/0331018).
• S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, 1983 (cited as [150] in the survey, https://doi.org/10.1137/0331018).

Motivation

A seller with a fixed stock of a single product and a finite selling season must post prices without knowing how demand responds to price. Revenue management treats this as a constrained stochastic control problem; with the demand curve known, the problem was solved by Gallego and van Ryzin (Management Science, 1994). When the curve is unknown, every price posted also serves as an experiment, so the seller faces an exploration–exploitation trade-off. Unlike a multi-armed bandit, this problem has a continuum of actions and a hard inventory constraint.

Besbes and Zeevi (Operations Research, 2009) measure a pricing policy by its worst-case relative revenue loss against a full-information benchmark, in an asymptotic regime where inventory and demand grow together. They give three upper bounds. This mission takes the third, Proposition 5: when the demand model has a single unknown scalar parameter, a policy that keeps re-estimating that parameter in stages of growing length has regret $O\big((\log\log n)(\log n)^{1/2}/n^{1/2}\big)$. The paper's lower bound for parametric families (Proposition 4) is of order $n^{-1/2}$, so the rate is optimal up to logarithmic factors.

Setting

Market. Prices lie in $[\underline p,\overline p]\cup\{p_\infty\}$ with $0<\underline p<\overline p<p_\infty$. Posting the off price $p_\infty$ stops demand. The seller starts with inventory $x>0$ and sells over the horizon $[0,T]$, $T>0$.

Demand. A demand function $\lambda$ maps a price to a demand rate. The class $\mathcal L(M,\underline K,\overline K,m)$ consists of the functions that are non-increasing with an inverse $\gamma$ on $[\underline p,\overline p]$, have a concave revenue rate $r(l)=l\gamma(l)$, are bounded by $M$, are $\overline K$-Lipschitz with a $\underline K^{-1}$-Lipschitz inverse, and attain a revenue rate $\max_p p\lambda(p)\ge m$. The parametric family is $\lambda(p;\theta)$, $\theta\in\Theta=[\theta_{\mathrm{lo}},\theta_{\mathrm{hi}}]$, with every member in the class (Assumption 1). Assumption 2 adds a test price $p_1$, differentiability of $\sqrt{\lambda(p_1;\cdot)}$ and the Lipschitz bound $|\lambda(p;\theta)-\lambda(p;\theta')|\le\overline K_2|\theta-\theta'|$. Assumption 3 requires $\inf_{p,\theta}\lambda(p;\theta)>l_0>0$ and an $\alpha$-Lipschitz solution map $d\mapsto g(p,d)$ of the equation $\lambda(p;\cdot)=d$.

Demand process. Let $N$ be a unit-rate Poisson process. Under a price path $p(\cdot)$ and parameter $\theta^*$, the cumulative demand up to time $t$ is $N\big(\int_0^t\lambda(p(s);\theta^*)\,ds\big)$. Sales stop when the inventory runs out.

Benchmark and regret. The deterministic relaxation $J^D(x,T\mid\theta)$ is the supremum of $\int_0^T p(s)\lambda(p(s);\theta)\,ds$ over price paths with $\int_0^T\lambda(p(s);\theta)\,ds\le x$. In the market of size $n$ the inventory is $nx$ and the demand $n\lambda$. If $J^\pi_n(x,T;\theta)$ is the expected revenue of a policy $\pi$, its regret is $\mathcal R^\pi_n=1-J^\pi_n/J^D_n$.

Algorithm 3. Start from $\hat p_1=p_1$ and use stages of lengths $\Delta^{(1)}_n,\dots,\Delta^{(\ell_n)}_n$ summing to $T$. Stage $i$ applies $\hat p_i$, estimates the demand rate $\hat d_i$ from the stage's demand, solves for $\hat\theta_i=g(\hat p_i,\hat d_i)$, and sets $\hat p_{i+1}=\max\{p^u(\hat\theta_i),p^c(\hat\theta_i)\}$. Here $p^u(\theta)$ maximizes $p\lambda(p;\theta)$ and $p^c(\theta)$ minimizes $|\lambda(p;\theta)-x/T|$. The tuning (19)–(20) is $\ell_n=(\log2)^{-1}\log\log n$ stages with $\Delta^{(m)}_n=\beta_n n^{(a_{\ell_n}/a_m)-1}$ and $a_m=2^{m-1}/(2^m-1)$.

Formalization targets

Goal: Proposition 5

$$\exists\,C>0,\ \exists\,n_0,\quad \forall n\ge n_0,\ \forall\theta\in\Theta:\qquad \mathcal R^{\pi_n}_n(x,T;\theta)\le C\,\frac{(\log\log n)(\log n)^{1/2}}{n^{1/2}} .$$

The constants are uniform in $\theta$ and $n$. This is the paper's (21): $\sup_\theta\mathcal R^{\pi}_n=O(\cdot)$.

Milestones, in proof order

1. Fact 1: $J^D_n=nJ^D$ and $J^D\ge m\min\{T,x/M\}$ on the class.
2. Lemma 1: the deterministic relaxation is solved by the fixed price $p^D=\max\{p^u,p^c\}$.
3. Lemma 2: Poisson deviation bounds at scale $(\log n/r_n)^{1/2}$.
4. (A-27): a revenue lower bound that splits the loss into stage-wise terms and an overflow term.
5. The per-stage revenue gap $r(p^D)-\mathbb E\,r(\hat p_i)\le C_2(n\Delta^{(i-1)}_n)^{-1/2}$.
6. (A-30): the stage-$i$ demand rate rarely exceeds the run-out rate.
7. The overflow bound $\mathbb E[(Y_n-nx)^+]\le nC_8(\log n)^{1/2}n^{a_{\ell_n}-1}$.
8. (A-31): the revenue ratio before the exponents are evaluated.
9. The rate estimate $n^{a_{\ell_n}-1}\le e\,n^{-1/2}$.

Milestones 6–8 hold in the case $\lambda(\overline p;\theta^*)\le x/T$, the only case the paper's proof treats in detail.

Significance

Proposition 5 shows that with one unknown parameter, learning while earning reaches the $n^{-1/2}$ rate, up to logarithms. The learn-then-price policies of Propositions 1 and 3 stop learning after an initial phase and reach only $n^{-1/4}$ and $n^{-1/3}$. The paper leaves open whether the multi-parameter case attains the lower bound.

The analysis combines a continuous-time controlled Poisson model, an inventory constraint and a staged estimator, which also appear in later work on dynamic pricing with learning. A formal development would provide a time-changed Poisson demand model with random stage boundaries, a deterministic-relaxation benchmark, and concentration bounds stated for the scales this literature uses.

The result is proved in the paper, but parts of the proof are only sketched. The case $\lambda(\overline p;\theta^*)>x/T$ is dismissed with "a similar result holds". The per-stage gap is obtained "by parallel reasoning". Display (A-30) has a typographical error in its threshold. To our knowledge, none of these results has been machine-checked.

Difficulty

The naive argument conditions each stage on its start time, as if that time were deterministic. It is not: the stage boundaries $\Lambda_i=\sum_{j\le i}n\lambda(\hat p_j;\theta^*)\Delta^{(j)}_n$ depend on all earlier observations, so every per-stage estimate needs the strong Markov property of the Poisson process at a random time. The inventory constraint makes the revenue a nonlinear function of the whole demand path. Bounding the loss therefore means controlling estimation error and overflow at the same time. The geometric stage lengths (20) are chosen so that the stage losses $\Delta^{(i)}_n/(n\Delta^{(i-1)}_n)^{1/2}$ are all of the same order. That balance has to be checked exactly, including the rounding of $\ell_n$ to an integer.

Formalization scope

• Poisson process. A structure on an arbitrary probability space: $N(0)=0$, monotone right-continuous paths, measurable marginals, Poisson increments, and independent increments over finite partitions. No process is published on the platform.
• Class and family. Conditions on $\lambda$ are imposed on $[\underline p,\overline p]\cup\{p_\infty\}$, the only prices a path uses. The inverse $\gamma$ is Function.invFunOn. $\Theta$ is a nonempty closed interval of $\mathbb R$.
• Assumption 3. As printed it cannot hold for $d>\sup_\theta\lambda(p;\theta)$. It is read as an $\alpha$-Lipschitz map $g(p,\cdot):[0,\infty)\to\Theta$ that inverts $\lambda(p;\cdot)$ on $\Theta$. $g$ is jointly measurable, so that estimates at random prices are random variables.
• Selections. $p^u,p^c$ are any measurable selections of the maximizer and minimizer; the statements hold for each.
• Inventory. The inventory is $\lfloor nx\rfloor$ units, and sales are capped cumulative counts.
• Time change. Eq. (1) is applied stage by stage with random stage boundaries.
• Typos. In Algorithm 3, "$\lambda(p_i,\theta)$" is read as $\lambda(\hat p_i;\theta)$ and "$x/t$" as $x/T$.
• Stages. $\ell_n=\lceil\log_2\log n\rceil$.
• Integrals. Expectations are lower Lebesgue integrals of nonnegative quantities, converted to reals. The relaxation is a real supremum over measurable paths.
• Asymptotics. The $O(\cdot)$ is rendered with an explicit $n_0$. The clause "asymptotically optimal" is omitted, since it needs the second half of Lemma 1.
• Ruled out. Each of the following would trivialize the statement: removing the inventory cap, replacing the random stage boundaries by deterministic ones, fixing $\theta$, letting $C$ depend on $\theta$, or using a non-measurable selection (whose expectation would be a junk value).

Contributions are welcome on every milestone. The Poisson process structure, its strong Markov property at stage boundaries, and Lemma 2 can be reused in other Poisson-demand pricing and queueing missions. Lemma 1 and Fact 1 are deterministic, and the rate estimate already has a local proof.

Selected references

• O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
• 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
• K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000