Operations Research

Motivation

In 1955 E. M. L. Beale showed how Dantzig's simplex method, which was built for linear objectives, can be carried over to certain nonlinear convex objectives that are minimized subject to linear inequalities (Beale 1955). Section 4 of that paper treats one such objective: the sum of the $t$ largest of a set of $g$ linear forms. Beale's motivation comes from the theory of games: "if the enemy has to choose $t$ out of a set of $g$ possible actions, and $L_f$ represents his average gain through using the $f$th", then the defender wants to minimize the sum of the $t$ largest $L_f$.

The same objective can be written as a linear program. One introduces a bound $u$ and requires every sum of $t$ forms to be at most $u$. That formulation has $\binom{g}{t}$ constraints, which is unwieldy once $t>1$ and $g$ is large. Beale's alternative works with the nonlinear objective directly, and he needs a test that tells him when the current basic solution is already optimal. This mission formalizes that test, Theorem 1 of the paper.

The objective reappears in later work under other names: the sum of the $k$ largest components of a vector, the "top-$k$ sum", and $k$ times the conditional value-at-risk of an empirical distribution. Beale's paper is an early source for its optimality conditions.

Setting

There are real variables $z_l$, indexed by $l$ in a finite set (possibly empty), and $u_1,\dots,u_s$. Two linear forms in these variables are given,

$$A=A_0+\sum_l A_l z_l+\sum_{f=1}^{s}\varphi_f u_f,\qquad L_0=c_{00}+\sum_l c_{0l} z_l+\sum_{f=1}^{s}\theta_f u_f,$$

together with $s$ further forms

$$L_f=L_0-u_f\qquad(f=1,\dots,s).$$

For an integer $\tau\ge0$ the objective is

$$C=A+\bigl(\text{sum of the }\tau\text{ largest of }L_0,L_1,\dots,L_s\bigr).$$

The sum of the $\tau$ largest of $s+1$ numbers is the largest total of any $\tau$ of them. Ties do not make it ambiguous.

The feasible region is fixed by a set $F$ of indices. The variables $z_l$ with $l\in F$ and all the $u_f$ are free, and every other $z_l$ is restricted to $z_l\ge0$. At the origin $z=0$, $u=0$ all $s+1$ forms are equal to $c_{00}$, so the origin is where $C$ fails to be differentiable. In Beale's algorithm the origin is the current basic solution: the $u_f$ measure how far the "borderline" forms sit from a chosen critical form, and $A$ collects the forms that are certainly among the largest.

Write $a_l=A_l+\tau c_{0l}$ and $w_f=\varphi_f+\tau\theta_f$.

Formalization targets

Goal: Theorem 1 (a), p. 179

For $\tau\le s$, $C$ is minimized over the feasible region when all the $z_l$ and $u_f$ vanish if and only if

$$\begin{aligned} &a_l\ge0\ \text{for all } l, \qquad a_l=0\ \text{for all } l\in F,\\ &0\le w_f\le1\ \text{for all } f,\qquad \tau-1\le\sum_{f=1}^{s}w_f\le\tau . \end{aligned}\tag{4.5}$$

"Minimized" means a global minimum: $C(0,0)\le C(z,u)$ at every feasible point.

Milestones

1. Convexity (p. 179). $C$ is a convex function of $(z,u)$ for $\tau\le s+1$.
2. Descent rules (second half of Theorem 1 (a), p. 179). When a condition of (4.5) fails, a stated move of one variable, or of all $u_f$ together, lowers $C$ below $C(0,0)$ for every small enough step. There are six moves: $z_l\uparrow$ if $a_l<0$; $z_l\downarrow$ if $a_l>0$ and $l\in F$; $u_f\uparrow$ if $w_f<0$; $u_f\downarrow$ if $w_f>1$; all $u_f\uparrow$ if $\sum w_f<\tau-1$; all $u_f\downarrow$ if $\sum w_f>\tau$.
3. The rearrangement identity (proof of Theorem 1 (a), p. 180). If $1\le\tau\le s$, $u'_1\le\dots\le u'_s$ and $u'_\tau\le0$, then

$$C=A_0+\tau c_{00}+\sum_l a_l z'_l+\sum_{f=1}^{\tau}(w_f-1)(u'_f-u'_\tau)+\sum_{f=\tau+1}^{s}w_f(u'_f-u'_\tau)+\Bigl\{\sum_{f=1}^{s}w_f-\tau\Bigr\}u'_\tau .$$

4. Theorem 1 (b) (p. 180). For $\tau=s+1$, the origin is a minimum if and only if (4.5) holds and $w_f=1$ for every $f$. Otherwise some value of $u_f$ with the sign opposite to $w_f-1$ lowers $C$.

Significance

Theorem 1 is the optimality test of Beale's simplex method for the sum-of-largest objective. The algorithm on pp. 178–179 changes nonbasic variables one at a time. When no single change is profitable it applies Theorem 1: either (4.5) holds and the current solution is optimal, or one of the six descent rules names the variable to change next. The test is exact even though the objective is not differentiable at the current point. It is a closed-form description of the subdifferential of a top-$\tau$ sum at a point where all the forms tie. The theorem is also the base case of the multi-group generalization that Beale mentions on p. 181.

The paper proves Theorem 1 by hand. To our knowledge neither the theorem nor the rearrangement identity behind it has been formalized in any proof assistant. The mission produces:

• a checked statement and proof of the test, including the degenerate cases $\tau=0$ and $s=0$, which the paper does not discuss separately;
• the boundary case $\tau=s+1$;
• a reusable Lean definition of the sum of the $\tau$ largest entries of a finite real family, with its convexity.

Difficulty

Necessity, the "only if" direction, is the part the paper calls obvious: each descent rule changes $C$ linearly for small steps. Two features still have to be handled explicitly. The step must be small only in rule-dependent ways, and the ordering of the forms changes along the moves of rules 4 and 6.

Sufficiency is where the work lies. The naive argument, "the directional derivative in every coordinate direction is non-negative, so the origin is a minimum", fails because $C$ is not differentiable at the origin. Nonnegative derivatives along the coordinate axes do not control mixed directions in which several $u_f$ move by different amounts, which reorders the forms. Which $\tau$ forms are the largest then depends on the point, and the paper settles the configurations in which $L_0$ is among the $\tau$ largest by an informal appeal to the "essential symmetry" between $L_0$ and the other forms. A formal proof cannot leave that appeal informal: the forms are parametrised relative to $L_0$ (each $L_f$ is $L_0-u_f$), so the symmetry is a change of variables that has to be written down and shown to preserve (4.5).

Formalization scope

• Data. The variables are z : Fin r → ℝ (any r, including $0$) and u : Fin s → ℝ. The paper's $u_f$ for $f=1,\dots,s$ is Lean's u f for $f=0,\dots,s-1$. The coefficients $(A_0,A_l,\varphi_f,c_{00},c_{0l},\theta_f)$ form a structure Forms r s.
• Forms. The family $L_0,\dots,L_s$ is Fin (s+1) → ℝ, with index $0$ for $L_0$ and index f.succ for $L_0-u_f$. The free set $F$ is a Finset (Fin r), and $\tau$ is a natural number cast to $\mathbb R$ wherever it multiplies a coefficient.
• Sum of the largest. sumLargest τ v is the maximum over $\tau$-element subsets $S$ of $\sum_{i\in S}v_i$ (Finset.sup' over powersetCard). It is the junk $0$ for $\tau$ larger than the number of entries, a case no statement uses.
• Minimality. "Minimized when all variables vanish" is the global statement $C(0,0)\le C(z,u)$ for all $(z,u)$ with $z_l\ge0$ for $l\notin F$. It is not a local minimum, and the sign constraints on restricted $z_l$ are kept: they are why the first condition of (4.5) is an inequality.
• Descent. "$C$ can be decreased by moving $x$ from zero" is a strict decrease for all step sizes in some interval $(0,\varepsilon)$, with every other variable at zero.
• No trivialization. The goal is an equivalence with no hypothesis beyond $\tau\le s$. Neither direction can be satisfied vacuously, and the cases $\tau=0$ and $s=0$ are included, as on the page.
• Added hypotheses. The rearrangement milestone assumes $\tau\ge1$, because the paper's $u'_\tau$ does not exist at $\tau=0$. Its second line uses $c_{0l}$ where the page misprints $c_l$.

Needed infrastructure:

• basic lemmas on sumLargest: its value at a constant family, at a family sorted by a monotone shift, and under adding a common constant;
• the change of variables behind the paper's symmetry between $L_0$ and the other forms.

These lemmas are reusable for any top-$k$-sum or empirical-CVaR objective. Contributions are welcome at any level: lemmas about sumLargest, any of the milestones, or an alternative sufficiency proof through convexity and one-sided directional derivatives.

Not in scope: the pivoting rules (4.2)–(4.4), the degeneracy discussion on pp. 180–181, and the multi-group generalization, which the paper says is "cumbersome to state" and does not state.

Selected references

• E. M. L. Beale, On Minimizing a Convex Function Subject to Linear Inequalities, Journal of the Royal Statistical Society, Series B 17(2), 173–184, 1955. https://doi.org/10.1111/j.2517-6161.1955.tb00191.x
• G. B. Dantzig, A. Orden and P. Wolfe, The generalized simplex method for minimizing a linear form under linear inequality restraints, Pacific Journal of Mathematics 5(2), 183–195, 1955. https://doi.org/10.2140/pjm.1955.5.183
• R. T. Rockafellar and S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3), 21–41, 2000. https://doi.org/10.21314/JOR.2000.038

Motivation

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

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

Setting

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

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

so its generator is

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

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

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

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

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

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

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

Formalization targets

Goal: the exponential density satisfies the BAR under conormal reflection

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

With unlimited inventory, the expected revenue of the policy is

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

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

Formalization targets

Goal: Proposition 3

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

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

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

Milestones from the paper's proof

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

Significance

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

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

Difficulty

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

Formalization scope

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

Readings of the paper's informal words:

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

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 1 and Corollary 1

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Readings of the paper's words:

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

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

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

Selected references

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