Optimization

Motivation

Retailers accept large volumes of returned merchandise, and a common default is the full refund: a buyer who is unhappy with a product brings it back and gets the whole price back. Many consumers only learn how much they value a product after they have it at home — clothes that do not fit, a gadget that does not suit the buyer's needs. A returns policy therefore plays two roles at once. It raises the buyer's willingness to pay before purchase, and after purchase it decides which units stay with consumers and which go back to the seller to be salvaged.

Xuanming Su's paper Consumer Returns Policies and Supply Chain Performance (SSRN 1020451; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240) puts this effect into a newsvendor model with random demand. The earlier literature it builds on, notably Che (1996) and Davis, Gerstner and Hagerty (1995), asked whether a seller should offer full refunds or no returns at all. Su's model makes the refund amount a separate decision variable. The answer it gives is closed-form and sharp: the optimal refund equals the salvage value. This mission formalizes Sections 3–4 of the paper: the single-seller model, the full-refund benchmark, and the optimal partial refund.

Setting

A seller stocks a quantity $q \ge 0$ before a selling season at unit cost $c$. Unsold and returned units are salvaged at value $s$. Market demand is a nonnegative random variable $X$ with law $D$, distribution function $F$ and $\bar F = 1 - F$. Each consumer who buys learns a valuation $V$ after purchase. Valuations are i.i.d. with law $\nu$ and finite mean $\mu = EV$, and the standing assumption is $\mu > c > s \ge 0$.

The seller chooses a price $p$, a quantity $q$ and a refund $r$. Once a consumer has bought, they keep the product if $V \ge r$ and return it otherwise. The keep and return probabilities are

Before purchase a consumer's expected utility from buying is $E\max(V, r)$, so this is the reservation price. Every consumer buys if $p \le E\max(V, r)$ and nobody buys otherwise (the demand rule (6)). With $E\min(X, q)$ the expected sales of a stock $q$, the seller's expected profit (7)–(8) is

and $-(c-s)q$ otherwise. Two special cases serve as benchmarks. Under full refunds ($r = p$) every consumer buys and the profit is $\Pi_{\text{full}}(p,q) = (p-s)\bar G(p)E\min(X,q) - (c-s)q$, from (1)–(2). Under no returns the price is $\mu$ and the profit is $\Pi_{\text{no}}(q) = (\mu - s)E\min(X,q) - (c-s)q$, from (3). Social welfare (12)–(13) is the sum of consumer surplus and seller profit, $SW(p,q,r) = \int_{[r,\infty)}(v-s)\,d\nu(v)\cdot E\min(X,q) - (c-s)q$, again subject to the demand rule.

Formalization targets

Goal: Proposition 2 (p. 11)

With $p^* = E\max(V,s)$, $r^* = s$ and any $q^*$ satisfying

the triple $(p^*, q^*, r^*)$ maximizes $\Pi$ over all prices, all refunds and all quantities $q \ge 0$:

Milestones

1. The reservation price splits as $E\max(V,r) = rG(r) + \int_{[r,\infty)} v\,d\nu$, which is the step (28)→(29) of the proof (p. 26).
2. At $p = E\max(V,r)$ the per-unit margin $(p-s)\bar G(r) + (p-r)G(r)$ equals $\int_{[r,\infty)}(v-s)\,d\nu$, displays (27)–(30), p. 26.
3. This integral is maximized at $r = s$ (p. 26).
4. Hence $(E\max(V,s), s)$ maximizes the margin subject to $p \le E\max(V,r)$, the first step of the proof (p. 26).
5. The newsvendor critical fractile, a reference to a proved platform theorem (p. 26).
6. Proposition 1(i) (p. 9): under full refunds, $p^* \in \arg\max_p (p-s)\bar G(p)$ with $\bar F(q^*) = (c-s)/((p^*-s)\bar G(p^*))$ is optimal.
7. Proposition 1(ii) at $s = 0$ (p. 26): with nonnegative valuations, no returns beats every full-refund policy.
8. Corollary 1 (p. 12): the inequality $(p-s)\bar G(p) \le E\max(V,s) - s$ (p. 26), and its consequence that partial refunds earn at least the full-refund profit and, for strictly increasing $F$, stock at least as much.
9. Corollary 2 (p. 13): the triple of Proposition 2 also maximizes social welfare.

Significance

The result separates two things that a full refund ties together: the price and the refund. Setting $r = s$ sends every unit back to its more valuable use. Consumers who value the product above its salvage value keep it, and the rest return it to be salvaged. The price $E\max(V,s)$ then extracts the whole expected surplus. Consequences follow directly. Partial refunds dominate both full refunds and no returns (Corollary 1). They raise the stocking quantity, which benefits an upstream manufacturer paid per unit ordered. With valuation uncertainty resolved only after purchase, the monopoly outcome is welfare-maximizing (Corollary 2). Section 5 of the paper, formalized in the companion mission, uses Proposition 2's triple as the first-best target that supply chain contracts must implement.

The results are proved on paper with short arguments in Appendix A of the paper. None of them has a machine-checked proof. The mission's contribution is a formal model of consumer returns with the demand rule built in, plus checked versions of Propositions 1–2 and Corollaries 1–2 for general valuation laws (with atoms), not only densities.

Difficulty

The paper's proof treats the problem as separable: first maximize the margin over $(p, r)$, then solve a newsvendor problem in $q$. Two steps that are routine on paper need care. First, the margin bound must hold over the whole constrained region $p \le E\max(V, r)$, including refunds above the price and negative prices. It rests on comparing $\int_{[r,\infty)}(v-s)\,d\nu$ with $\int_{[s,\infty)}(v-s)\,d\nu$, which needs the closed half-line convention to hold up at atoms of $\nu$. Second, the newsvendor step must be done for a demand law that may have atoms, where $\bar F$ has no inverse. Without the demand rule the problem is not separable at all: formula (8) alone is unbounded in $p$. Without nonnegativity of demand and quantity it is unbounded in the other direction.

Formalization scope

Lean represents all prices, refunds, costs, quantities and profits as real numbers. The valuation law is a probability measure ν on ℝ with integrable identity, so a density is not required. The demand law is a probability measure D on ℝ with D (Set.Iio 0) = 0. $\bar G(r)$ is (ν (Set.Ici r)).toReal and $G(r)$ is (ν (Set.Iio r)).toReal, following the page's tie rule (keep iff $V \ge r$). $E\min(X,q)$ is SupplyChainTheory.expSales D q from the published module SupplyChainTheory_contracts, and $\bar F$ is 1 - ProbabilityTheory.cdf D. Printed page numbers equal PDF page numbers throughout the source.

Committed conventions and readings:

• Demand rule inside the objectives. Profit and welfare are zero-demand cash flows when $p > E\max(V,r)$.
• Nonnegativity. Stocking quantities range over $q \ge 0$ and demand is nonnegative. Both are the page's words ("stocking quantity", "a mass of infinitesimal consumers"), and without them the profit is unbounded.
• Salvage value. $0 \le s$, as on p. 26.
• Optimality, not uniqueness. Every optimum is stated as optimality of the page's closed-form triple. Uniqueness fails when $\nu$ has gaps: if $\nu$ puts no mass on $[s, r)$, the refund $r$ is optimal too.
• No continuity of $F$ for the goal. The goal assumes no continuity of $F$. Existence of $q^*$ is not claimed.
• Corollary 1, quantity part. The quantity comparison assumes $F$ strictly increasing on $[0,\infty)$, which the proof's $\bar F^{-1}$ presumes. Without it the statement is false.
• Proposition 1(ii) at $s = 0$. This case assumes nonnegative valuations. The "sufficiently low" form of Proposition 1(ii) is not formalized.

A trivializing formalization is ruled out: $p^*$ and $r^*$ are the explicit values $E\max(V,s)$ and $s$, not an argmax chosen by Classical.choose. The maximization ranges over all $(p, r)$ and all $q \ge 0$, not a set restricted to $r = s$. The returned-units cash flow $(p - r + s)G(r)$ appears in the profit.

The newsvendor step reuses the proved platform theorem SupplyChainTheory.chain_optimal_fractile. The other pieces needed are elementary lemmas on integrals over half-lines and the concavity of $q \mapsto E\min(X,q)$. They are reusable for any newsvendor-type model. Proofs of any milestone, and a general-law newsvendor optimality lemma that does not need a continuous $F$, are welcome.

Selected references

• X. Su, Consumer Returns Policies and Supply Chain Performance, SSRN working paper 1020451, version of August 2008. https://ssrn.com/abstract=1020451 — published in Manufacturing & Service Operations Management 11(4), 2009. https://doi.org/10.1287/msom.1080.0240
• Y.-K. Che, Customer Return Policies for Experience Goods, Journal of Industrial Economics 44(1), 1996. https://doi.org/10.2307/2950560
• S. Davis, E. Gerstner, M. Hagerty, Money Back Guarantees in Retailing: Matching Products to Consumer Tastes, Journal of Retailing 71(1), 1995. https://doi.org/10.1016/0022-4359(95)90010-1

Motivation

Monotone comparative statics asks when the optimal choice of an agent moves in a predictable direction as a parameter of the problem changes: does a firm hire more of every input when the output price rises, does a monopolist raise its price when its marginal cost rises? Topkis (1978) gave a cardinal answer: if the objective $f(x,t)$ is supermodular in the choice $x$ and has increasing differences in $(x,t)$, the set of maximizers is nondecreasing in $t$. Milgrom and Shannon (1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed in their Monotonicity Theorem that the ordinal conditions are both necessary and sufficient for the argmax to be monotone in the parameter and the constraint set.

Supermodularity is therefore never necessary for monotone comparative statics. Theorem 10 of Milgrom and Shannon identifies a setting where it is: when the objective must keep the ordinal properties after adding an arbitrary linear price term $p\cdot x$ (or subtracting an arbitrary nonnegative cost $w\cdot x$), the only objectives that qualify are the supermodular ones. This is the situation of a price-taking firm whose revenue or cost is linear in its activity levels, and the result explains why supermodularity is the natural assumption in such models even though the ordinal theory does not require it.

Setting

Let $X$ be a lattice: a partially ordered set in which every two elements $x, y$ have a least upper bound $x \vee y$ (join) and a greatest lower bound $x \wedge y$ (meet). On $\mathbb{R}^n$ the order is componentwise, so $x \vee y$ and $x \wedge y$ are the componentwise maximum and minimum; on a product $\mathbb{R}^n \times \mathbb{R}$ the order is the product order. For $p, x \in \mathbb{R}^n$, $p \cdot x = \sum_i p_i x_i$.

A function $g : X \to \mathbb{R}$ is supermodular if $g(x) + g(y) \le g(x \vee y) + g(x \wedge y)$ for all $x, y \in X$. It is quasisupermodular if, for all $x, y \in X$, (i) $g(x) \ge g(x \wedge y)$ implies $g(x \vee y) \ge g(y)$, and (ii) $g(x) > g(x \wedge y)$ implies $g(x \vee y) > g(y)$.

Let $T$ be a partially ordered set and $f : X \times T \to \mathbb{R}$. The function $f$ has increasing differences in $(x, t)$ if for $x' \ge x''$ the difference $f(x', t) - f(x'', t)$ is nondecreasing in $t$. It has the single crossing property in $(x; t)$ if for all $x' > x''$ and $t' > t''$, $f(x', t'') > f(x'', t'')$ implies $f(x', t') > f(x'', t')$, and $f(x', t'') \ge f(x'', t'')$ implies $f(x', t') \ge f(x'', t')$. The function $f$ is quasisupermodular in $x$ if $f(\cdot, t)$ is quasisupermodular for every $t$, and nondecreasing in $x$ if $f(\cdot, t)$ is nondecreasing for every $t$.

In the Lean development the domain $\mathbb{R}^n$ is Fin n → ℝ, $f$ is curried as f : (Fin n → ℝ) → ℝ → ℝ, $p \cdot x$ is p ⬝ᵥ x, and supermodularity and increasing differences are the published Supermodularity.Monotonicity.SupermodularOn and IncreasingDifferencesOn with the domain Set.univ.

Formalization targets

Goal: Theorem 10 (p. 166)

Let $f : \mathbb{R}^n \times \mathbb{R} \to \mathbb{R}$. Then

and, if $f$ is nondecreasing in $x$,

Here "$f$ is supermodular" means supermodular on the lattice $\mathbb{R}^n \times \mathbb{R}$, jointly in $(x,t)$.

Milestones

1. Every supermodular function on a lattice is quasisupermodular (p. 164, remark after Theorem 5).
2. Every function with increasing differences in $(x, t)$ has the single crossing property in $(x; t)$ (same remark).
3. If $g + p\cdot x$ is quasisupermodular on $\mathbb{R}^n$ for every $p \in \mathbb{R}^n$, then $g$ is supermodular (the converse step of the proof of Theorem 10).
4. The first sentence of Theorem 10 on its own.

Significance

The result. The Monotonicity Theorem shows that the ordinal conditions are exactly what monotone comparative statics needs for a single objective. Theorem 10 shows that the cardinal conditions are exactly what is needed for a family of objectives closed under linear prices. It separates two questions that are often conflated: whether a particular optimization problem has monotone solutions (ordinal), and whether a model's monotonicity conclusion is robust to the prices or costs the modeller adds to it (cardinal). The second sentence specializes to the economically common case of nonnegative input costs, where the restriction to $w \ge 0$ is offset by the monotonicity of $f$.

Formalizing it. The result is proved in the paper, with the converse direction given in detail only for the step "supermodular in $x$" and the remaining cases left as "similar arguments". The mission produces machine-checked proofs of both equivalences, including the cases the paper does not write out: the recovery of increasing differences from the single crossing property under all price perturbations, and the recovery under the sign restriction $w \ge 0$. No part of Milgrom and Shannon's paper was found formalized on the platform when this mission was drafted; Topkis's supermodularity theory is partly available on the platform as the Supermodularity.* series.

Difficulty

The forward direction is a chain of short implications. The content is in the converse: from purely ordinal information about many functions one must recover a cardinal inequality. The single crossing property and quasisupermodularity only compare values of one function at two points, so a single perturbation can never yield an inequality between sums of four values; the argument must choose, for each violating configuration, a price vector that makes two of the four values tie, and the choice must be compatible with the sign constraint $w \ge 0$ in the second statement. That compatibility is where the hypothesis that $f$ is nondecreasing in $x$ enters, and without it the second equivalence fails. A second subtlety is the decomposition of joint supermodularity on $\mathbb{R}^n \times \mathbb{R}$ into supermodularity in $x$ and increasing differences in $(x,t)$, which the paper uses without statement; the platform does not yet have it.

Formalization scope

• $\mathbb{R}^n$ is Fin n → ℝ with Mathlib's pointwise order and lattice operations; $n \ge 0$ is arbitrary. The product $\mathbb{R}^n \times \mathbb{R}$ carries Mathlib's product order.
• $f : \mathbb{R}^n \times \mathbb{R} \to \mathbb{R}$ is curried. "$f$ is supermodular" is read as joint supermodularity on $\mathbb{R}^n \times \mathbb{R}$, as the paper's proof confirms ("If $f$ is supermodular in $(x, t)$ …"); with supermodularity in $x$ only, the "if" direction would be false.
• Quasisupermodularity and the single crossing property are the paper's definitions verbatim: strict comparisons $x' > x''$, $t' > t''$ in the single crossing property, both the weak and the strict implication in both notions, and quantification over all ordered pairs. The paper's single crossing property is stated for a lattice $X$; the Lean definition only uses the order.
• The quantifier over $p$ (and over $w \ge 0$) is universal and covers both properties at once. The second equivalence keeps $- w\cdot x$ with $w \ge 0$ componentwise and has "nondecreasing in $x$" as its hypothesis only.
• Trivializing formalizations are ruled out: an existential quantifier over $p$, supermodularity in $x$ only on the right-hand side, merging the two sentences with $p = -w$, or dropping the monotonicity hypothesis would each state a different, false or weaker theorem.
• The definitions QuasiSupermodularOn and SingleCrossing are shared with the two sibling missions on Milgrom and Shannon's Theorems 4 and 8 and will be merged with them. A lemma decomposing supermodularity on a product lattice into supermodularity in each factor and increasing differences would be reusable well beyond this mission; contributions of such general lattice lemmas are welcome.

Selected references

• P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
• D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 305–321, 1978. https://doi.org/10.1287/opre.26.2.305
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Motivation

Many algorithms for convex bodies need the body to be well rounded: sandwiched between two concentric ellipsoids whose size ratio is controlled by the dimension. The ellipsoid method, volume and integration algorithms, and preconditioning for linear programming use such roundings. For a polytope given by its vertices $a_1,\dots,a_m \in \mathbb{R}^n$, John's theorem guarantees an ellipsoid $E$ with

the minimum-volume circumscribed (Löwner–John) ellipsoid scaled about its centre; for centrally symmetric sets the factor improves to $\sqrt n$. The associated D-optimal design problem is a convex optimization problem. Khachiyan (1996) uses this connection to obtain a finite approximation algorithm.

Khachiyan shows that barycentric coordinate descent (BCD) computes a $(1+\varepsilon)n$-rounding in $O(mn^2(\varepsilon^{-1} + \ln n + \ln\ln m))$ arithmetic operations. For fixed dimension and tolerance, this is linear in the number of points; the iteration bound depends on that number only through $\ln\ln m$. Khachiyan (1996)

The paper builds on the Kiefer–Wolfowitz optimality conditions (1960). Later work revisits the method's complexity and variants; see Todd and Yıldırım (2007).

Setting

Let $a_1,\dots,a_m \in \mathbb{R}^n$ and let $S$ be the unit simplex of weights $p \ge 0$, $\sum_i p_i = 1$. For $p \in S$ write

and let $S_F = \{p \in S \mid \det A(p) > 0\}$. Maximizing $F$ over $S$ is the D-optimal design problem (2.3); $F^*$ is its optimal value. A point $p \in S_F$ satisfies the $\varepsilon$-relaxed optimality conditions (2.10) if $w_j(p) \le (1+\varepsilon)n$ for every $j$; the accuracy $\varepsilon(p) = \max_j w_j(p)/n - 1$ is the least such $\varepsilon$.

The BCD method starts at $p_0 = (1/m,\dots,1/m)$ and repeats

where $r$ is an index with largest $w_r(p_k)$ and $e_r$ is the $r$th vertex of $S$: it moves weight towards the worst-covered point by the exact line-search step.

For a centrally symmetric set ($\mathcal A = -\mathcal A$) the ellipsoid $E_p = \{x \mid x^{\mathsf T}A(p)^{-1}x \le 1\}$ is the candidate rounding. For a general set the method runs on the lift $\mathcal A' = \{\pm(a_j;1)\} \subset \mathbb{R}^{n+1}$, and the rounding ellipsoid $E$ is the intersection of $\sqrt{1 + (1+\varepsilon)n}\,E'_p$ with the hyperplane $\{y = 1\}$, where $E'_p$ is the ellipsoid (3.4) of the block matrix with blocks $\sum_j p_j a_j a_j^{\mathsf T}$, $\sum_j p_j a_j$ and $1$, and $p_j$ aggregates the weights of $\pm(a_j;1)$.

Formalization targets

Goal: Theorem 2 (p. 317)

There is a universal constant $C$ such that for every $n \ge 1$, every $\mathcal A = \{a_1,\dots,a_m\}$ with affine hull $\mathbb{R}^n$, every $\varepsilon > 0$ and every BCD run on $\mathcal A'$, some iterate $p_k$ with

meets the stopping test with $\varepsilon' = \frac{n}{n+1}\varepsilon$ and yields an ellipsoid $E$ with

the shrinking taken about the centre of $E$.

The centrally symmetric case: Theorem 1 (p. 314)

For centrally symmetric full-dimensional $\mathcal A$, $n \ge 2$: within $C\,n(\varepsilon^{-1} + \ln n + \ln\ln m)$ iterations,

Milestones

Lemma 1 ($\sum_j p_j w_j(p) = n$), existence of a maximizer, the line identity (2.6), the Kiefer–Wolfowitz conditions (2.9), Lemma 2(i)–(ii) (relaxed optimality gives value and rounding guarantees), Lemma 3 (the per-step increase and the gap bound), the three steps (2.25), (2.27) and the halving bound of the proof of Lemma 4, Lemma 4 (the iteration bound), the rank-one update of $A(p_k)^{-1}$, Theorem 1, and Lemma 5 (from the lift back to $\mathcal A$). Three further items complete §4: Lemma 2(iii), the slicing property (4.1) and Theorem 3 (approximating the Löwner ellipsoid to relative volume accuracy $\varepsilon$).

Significance

The result gives a rounding of a vertex-described polytope at nearly the cost of reading the input, using only rank-one updates; the same iteration approximates the minimum-volume enclosing ellipsoid, a basic primitive in statistics (D-optimal design, outlier detection), computational geometry (core sets) and convex optimization (initialization of interior-point and ellipsoid methods). The doubly logarithmic dependence on $m$ is what makes the method practical for large point sets, and the analysis is the template for the later Frank–Wolfe-type analyses of minimum-volume ellipsoid algorithms.

The results are proved in the paper; none of them has a machine-checked proof. The platform has the Löwner–John ellipsoid itself (existence, uniqueness, John's $n$-rounding) and the concavity of $\ln\det$, but no algorithmic statement about it. This mission produces a verified iteration bound for a concrete method, together with the D-optimal design identities (Lemma 1, (2.6), (2.9)) and the rank-one update, which are reusable for any later formalization of optimal design or of Frank–Wolfe methods on the simplex.

Difficulty

The accuracy $\varepsilon_k$ need not decrease at every step, so a bound based on per-step improvement in $\varepsilon_k$ fails. The determinant objective and the geometric rounding condition are different quantities: controlling one must be shown to control the other, including the inner inclusion of the ellipsoid. For a general set, the lift changes the dimension and the relevant ellipsoid is a slice at $y=1$; the inner inclusion for this slice needs a separate geometric justification.

Formalization scope

Points are vectors Fin n → ℝ; $\mathcal A$ is the range of a family a : Fin m → Fin n → ℝ (repetitions allowed). The definitions take any finite index, so they apply both to $\mathcal A$ and to the lift, indexed by Fin m ⊕ Fin m. $S$ is Mathlib's stdSimplex. $F$ uses Real.log, which returns $0$ rather than $-\infty$ on singular matrices, so every comparison of values of $F$ is restricted to $S_F$ and $F^*$ is the supremum over $S_F$. Ellipsoids are the published LinearOptimization.ellipsoid; scaled ellipsoids about the origin use the pointwise scalar multiple, and shrinking a non-centred ellipsoid is the homothety about its centre.

Standing assumptions are hypotheses: in §2, central symmetry (2.1), full dimension (2.2) and $n \ge 2$ (p. 309); in §3, full dimension (3.1) and $n \ge 1$. Items that do not need them drop them. The BCD run is a predicate on sequences that allows any maximizing index at every step, with no tolerance parameter; the tolerance enters only through the stopping test.

Each $O(\cdot)$ is a universal constant $C > 0$ quantified before the dimension, the points, $\varepsilon$ and the run. The paper counts arithmetic operations; the formal statements bound the index of an iterate meeting the stopping test, and the $O(nm)$ cost per iteration and the $O(mn^2)$ initialization are not formalized. The goal's bound is stated in the lifted parameters $(n+1, 2m)$, which agrees with the page's up to the constant and stays positive at $n = 1$.

The goal assumes nothing about the run beyond its definition: the stopping test, the positive definiteness of $A(p_k)$, the rounding inclusions and the iteration bound are all conclusions. A statement in which the constant may depend on the instance, or in which a shrunken ellipsoid is scaled about the origin, would be a different, trivial or false, theorem.

Contributions welcome: the determinant and inverse identities ((2.6), Lemma 1, the rank-one update) are self-contained linear algebra; Lemma 2 needs the KKT characterisation of the minimum-volume ellipsoid; Lemma 5 is finite-dimensional convex geometry.

Selected references

• L. G. Khachiyan, Rounding of polytopes in the real number model of computation, Mathematics of Operations Research 21(2):307–320, 1996. https://doi.org/10.1287/moor.21.2.307
• J. Kiefer, J. Wolfowitz, The equivalence of two extremum problems, Canadian Journal of Mathematics 12:363–366, 1960. https://doi.org/10.4153/CJM-1960-030-4
• L. G. Khachiyan, M. J. Todd, On the complexity of approximating the maximal inscribed ellipsoid for a polytope, Mathematical Programming 61:137–159, 1993. https://doi.org/10.1007/BF01582144
• M. J. Todd, E. A. Yıldırım, On Khachiyan's algorithm for the computation of minimum-volume enclosing ellipsoids, Discrete Applied Mathematics 155:1731–1744, 2007. https://doi.org/10.1016/j.dam.2007.02.013

Motivation

A controller of a finite Markov chain often cares about more than one long-run quantity: an inventory manager wants a high average profit while keeping the long-run fraction of stock-outs below a target; a communication network maximizes throughput subject to bounds on average delay or power. Such problems are constrained Markov decision problems: maximize one average reward while other averages, all linear in the long-run frequencies of state-action pairs, are kept below given bounds. Unlike unconstrained problems, they need not have a pure stationary optimal policy, and in general not even a stationary one.

Derman (Finite State Markovian Decision Processes, 1970, Ch. 7) treated the case in which every stationary policy induces a chain with one ergodic class, and solved it by linear programming. Derman and Veinott (1972) proposed a decomposition algorithm for the general multichain case, remarking that until the faces of the relevant polytope are known, routine use of the simplex method is not possible. Section 4.7 of Kallenberg's 1983 monograph (CWI repository) describes that polytope explicitly for the multichain case and derives from one linear program an optimal Markov policy, with conditions under which a stationary optimal policy can be read off. Kallenberg notes that Veinott knew the characterization of the polytope by 1973.

Setting

A finite Markov decision model has a finite state set $E$, for each state $i$ a finite nonempty set $A(i)$ of actions, rewards $r_{ia}$ and transition probabilities $p_{iaj}\ge0$ with $\sum_j p_{iaj}=1$. A policy $R$ chooses, at each time $t=1,2,\dots$, an action in $A(i_t)$ at random, with probabilities that may depend on the entire history $(i_1,a_1,\dots,a_{t-1},i_t)$. Special classes are the Markov policies $C_M$ (the rule at time $t$ ignores the past), the stationary policies $C_S$, written $\pi^\infty$ (one rule $\pi$, with $\pi_{ia}\ge0$ and $\sum_a\pi_{ia}=1$, at every time), and the pure stationary policies $C_D$, written $f^\infty$ with $f(i)\in A(i)$. All policies form the class $C$.

Fix an initial distribution $\beta$: $\beta_j\ge0$ and $\sum_j\beta_j=1$, with zeros allowed. The expected state-action frequencies in the first $T$ periods are

$X(R)$ is the set of limit points of $\{x^T(R)\}_{T\ge1}$, and $C_1$ the class of policies with exactly one limit point $x(R)$. For a class $C'$, $L(C')$ collects the limit points of all $R\in C'$, giving $L$, $L(M)$, $L(C)$ (for $C_1$), $L(S)$ and $L(D)$. For a stationary $\pi$, $P(\pi)_{ij}=\sum_a p_{iaj}\pi_{ia}$, $P^*(\pi)$ is its Cesàro limit, and $x_{ja}(\pi)=[\beta^TP^*(\pi)]_j\pi_{ja}$.

The polytope $X$ is the set of $x$ for which some $y$ satisfies

Given constraint data $q_{iak}$ and $b_k$, the constrained problem (4.7.5) is $\sup_{R\in C_1}\{\phi(\beta,R)\mid\sum_i\sum_aq_{iak}x_{ia}(R)\le b_k,\ k=1,\dots,m\}$, with $\phi(\beta,R)$ the lim inf of the average expected reward, and the linear program (4.7.6) maximizes $\sum_i\sum_ar_{ia}x_{ia}$ over $X$'s constraints together with $\sum_i\sum_aq_{iak}x_{ia}\le b_k$.

Formalization targets

Goal: Theorem 4.7.2

Every limit point of the expected state-action frequencies of any policy lies in the polytope $X$, and every point of $X$ is such a limit point.

Milestones

• Theorem 4.7.1. $\overline{L(D)}=\overline{L(S)}=L(C)=L(M)=L$, the bar being the closed convex hull.
• Lemma 4.7.1. For $R\in C_1$, $x_{ja}(R)=\lim_{\alpha\uparrow1}(1-\alpha)\sum_{t\ge1}\alpha^{t-1}\sum_i\beta_i\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$.
• Theorem 4.7.3. Problems (4.7.5) and (4.7.6) have the same feasibility and the same optimum; an optimal policy yields an optimal $x(R)$; a Markov policy reproducing a mixture of pure stationary policies with the optimal $x$ is optimal.
• Theorems 4.7.4–4.7.5. If the stationary rule $\pi^*$ built from an optimal $(x^*,y^*)$ by (4.7.14) satisfies $x^*=x(\pi^*)$, then $(\pi^*)^\infty$ is optimal; two sufficient conditions for $x^*=x(\pi^*)$.
• Theorem 4.7.9. If $\pi\mapsto x(\pi)$ is continuous, then $X=L(S)$.
• Lemma 4.6.1 and Theorem 4.7.10. If every pure stationary policy is unichain, so is every stationary one, and then $X=L(S)$.

Significance

The goal identifies the set of achievable long-run behaviours of a multichain Markov decision process with a polytope given by $2|E|$ linear equations. Any objective and any constraints that are linear in the frequencies then become one linear program (Theorem 4.7.3), and optimal policies are recovered from its solution. This is the basis of the linear programming approach to constrained average-reward control, later developed by Altman (Constrained Markov Decision Processes, 1999) and others.

The results of this section are proved in the monograph; none has a machine-checked proof. The mission produces a formal account of state-action frequencies under history-dependent policies on a finite model, their limit points, and the multichain LP polytope. The unichain special case is related to Derman's statements posed on the platform (DermanSeqDecisions.LinProg.*, completely ergodic models); the multichain statements here are not posed elsewhere.

Difficulty

The inclusion $L\subseteq X$ needs a limit point of a history-dependent policy to satisfy the second family of equations, which involves the auxiliary vector $y$; for stationary policies $y$ comes from the deviation matrix, but a general policy has no such matrix. The reverse inclusion cannot be obtained by realizing each $x\in X$ with a stationary policy: Example 4.7.1 of the book exhibits a model where $L(S)\neq X$, and a point of $L(D)$ that is not an extreme point of $X$. The natural candidate, the stationary rule $x_{ia}/\sum_ax_{ia}$, is not defined on states with $\sum_a x_{ia}=0$, and filling in $y$ there does not in general reproduce $x$ (Theorem 4.7.5 gives conditions under which it does). In the converse direction, frequencies of general policies need not converge, so arguments must work with all limit points, not with a limit.

Formalization scope

• The model is the platform definition MarkovDecisionProcesses_AverageReward (reference item): StationaryMDP S A with finite state type S, a common finite action type A, a nonempty admissible Finset per state, rewards, and transition rows that sum to one; policies are its AvgHRPolicy, history-dependent and randomized. Frequency vectors are indexed by the admissible pairs.
• $\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$ is a finite recursive sum over histories; no measure theory is used. Lean's time index starts at $0$ (the book's $t-1$).
• $X(R)$ is the set of limits of convergent subsequences of $x^T(R)$. Policy classes are predicates that constrain only the weights of admissible actions.
• $P^*$ is the limUnder of the Cesàro means $\frac1n\sum_{k=1}^nP^k$; its existence is the book's Theorem 2.4.1(i) and is not assumed as a hypothesis.
• $\beta$ is a probability vector with zeros allowed; $\beta\gg0$ is never assumed.
• The optima in Theorem 4.7.3 are compared in the extended reals, so the infeasible case reads $-\infty=-\infty$.
• "One ergodic set" is the platform's IsUnichainMatrix (any two recurrent states communicate); Assumption 4.7.1 is IsUnichain.
• Trivializing formalization ruled out: $L$ ranges over all history-dependent randomized policies. Restricting it to stationary policies would replace $L$ by $L(S)$, for which $L(S)=X$ fails in general.

A complete development needs Cesàro limits of stochastic matrices (Theorem 2.4.1), the stationary-policy correspondence of §4.3, a separating hyperplane in finite dimension, and the Derman–Strauch construction of a Markov policy matching a mixture of policies (Theorem 2.5.1). The frequency and limit-point infrastructure is reusable for any average-reward model on a finite state space. Proofs of any milestone, and of the auxiliary facts above as separate theorems, are welcome.

Selected references

• L.C.M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
• C. Derman, Finite State Markovian Decision Processes, Academic Press, New York, 1970.
• C. Derman and A.F. Veinott, Constrained Markov decision chains, Management Science 19 (1972), 389–390. https://doi.org/10.1287/mnsc.19.4.389
• C. Derman and R.E. Strauch, A note on memoryless rules for controlling sequential control problems, Annals of Mathematical Statistics 37 (1966), 276–278. https://doi.org/10.1214/aoms/1177699617
• E. Altman, Constrained Markov Decision Processes, Chapman & Hall/CRC, 1999. https://doi.org/10.1201/9781315140223

Why offer sets matter

A seller with one limited inventory pool can choose which fare products to show in each selling period. When customers choose among the displayed products, showing another fare can both add sales and divert buyers from a more expensive fare. A fixed ranking of fares therefore does not by itself tell the seller which products to offer. Talluri and van Ryzin's working paper studies the optimal offer decision under a general discrete choice model, without specifying a logit or independent-demand formula for customer choice (working paper, 2001, pp. 5–8; published article, 2004). The present mission concerns the paper's first main result: how to reduce the collection of possible offer sets and how the best choice changes with inventory and time.

Model and notation

There are $n$ fare products, indexed by $N=\{1,\ldots,n\}$. Product $j$ earns a nonnegative revenue $r_j$. In each period, a customer arrives with probability $\lambda\in[0,1]$, independent of the remaining time. The seller offers a set $S\subseteq N$. Conditional on arrival, the customer buys product $j\in S$ with probability $P_j(S)$ or buys nothing with the remaining probability. Thus $P_j(S)\ge0$ and $Q(S)=\sum_{j\in S}P_j(S)\le1$. The purchase probability is $Q(S)$, while the expected revenue conditional on arrival is $R(S)=\sum_{j\in S}P_j(S)r_j$. The empty set is a possible offer; it has $Q=R=0$.

Time is counted backward: $t$ is the number of periods still available, and $x$ is the number of inventory units left. Let $V_t(x)$ be the maximum expected revenue from that state, with $V_0(x)=V_t(0)=0$. For $t,x\ge1$, the marginal value of capacity is $\Delta V_{t-1}(x)=V_{t-1}(x)-V_{t-1}(x-1)$. The Bellman equation is

The paper calls a set $T$ dominated if a randomization over offer sets achieves either strictly more expected revenue with no greater purchase probability, or no less expected revenue with strictly lower purchase probability. A set is nondominated if neither comparison applies. This two-clause definition is specific to the paper. It differs from the one-clause “efficient set” used for a related model in Talluri and van Ryzin's book; the published formalization of that book's optimal policy theorem is therefore related work rather than a replacement for this goal.

Formalization targets

Nondominated frontier

Proposition 1 characterizes the nondominated sets by a positive tradeoff value $v$: a set $T$ lies on the relevant frontier exactly when it maximizes $R(S)-vQ(S)$ for some $v>0$. Proposition 2 says that dominated sets can be excluded from the Bellman maximization when $\Delta V_{t-1}(x)>0$, and that a nondominated optimum exists when the marginal value is zero. Proposition 3 orders the nondominated sets $S_1,\ldots,S_m$ so that both $Q_k=Q(S_k)$ and $R_k=R(S_k)$ are nondecreasing (working paper, pp. 8–12).

Largest optimal index

Among indices maximizing $R_k-Q_kv$, let $k^*(v)$ be the greatest one when there are ties. Lemmas 1 and 2 say that $k^*(v)$ is nonincreasing in $v$. The paper's Lemmas 3 and 4 say that marginal capacity values decrease as inventory increases and increase as the number of remaining periods increases. For the admissible states $t,x\ge1$, the goal is Theorem 1:

where $S_{k^*}$ is an optimal offer, and the greatest optimal index $k^*$ is nondecreasing in $x$ and nonincreasing in $t$ (working paper, pp. 12–15, Theorem 1). These are claims about the index in the nondominated ordering; the offer sets themselves need not be nested by inclusion.

What the result gives

Theorem 1 replaces a search over all $2^n$ offer sets at each state with a search over the nondominated sets. It also tells an operator how the preferred position in that ordered list changes as seats are sold or as the selling horizon shortens. The later sections of the paper add conditions under which this ordering corresponds to fare-order nesting; those conditions are treated in separate missions (working paper, §3).

The model's value recursion and the marginal-value inequalities already have published Prove2Me formalizations in the Talluri–van Ryzin book setting. The book's marginal-value theorem is proved and serves here as a referenced milestone after reindexing its forward time convention. The paper's two-clause dominance concept, its ordered frontier, and Theorem 1 itself remain the formalization work of this mission. Keeping those distinctions explicit makes the resulting definitions reusable for other choice models with the same purchase and revenue coordinates.

Main difficulty

A set with high expected revenue need not be attractive when capacity is scarce: it may also consume inventory more often. Ranking sets by revenue alone therefore fails. Conversely, an offer set can tie another at a single marginal value, so selecting an arbitrary maximizer does not give a monotone index across states. The paper resolves ties by taking the greatest optimal index. Formalization must also retain the full randomized dominance relation: using only strict revenue improvement would leave sets on the wrong frontier. These issues arise even with finitely many products and without a specialized formula for $P_j(S)$.

Formalization scope

Products are Fin n, and offers are finite subsets of them. The published RevenueManagement_singleResource definition supplies the choice-model predicate, $Q$, $R$, and the backward value recursion. This mission defines the paper's own dominance relation, stage objective, exhaustive ordered list of nondominated sets, and greatest-maximizer predicate. Every possible offer set, including the empty set, participates in the Bellman maximum. The list must contain all nondominated sets exactly once; otherwise choosing from it would weaken Theorem 1.

The assumptions $0\le\lambda\le1$ and $r_j\ge0$ are the model's arrival-probability and nonnegative-fare conventions. The paper indexes fares in decreasing order, but Section 2's claims do not use that order, so the Lean targets omit it. Proposition 2's assertion that a dominated set is never optimal requires $\lambda>0$; that condition is placed on that clause alone. Decisions and marginal values are stated for $t,x\ge1$. The paper prints Lemma 3 also at $x=1$, where its right side $\Delta V_t(0)$ is undefined; the referenced formalization states the meaningful range $x\ge2$. The imported book theorem uses forward time, reindexed here as the number of periods remaining. The goal does not assume the dominance reduction or the marginal-value monotonicities that its milestones supply.

A complete development uses finite sums and maxima, the choice-value recursion, a finite frontier argument for Proposition 1, and order properties of the stage objective. The dominance and ordered-frontier definitions can support later results on nested policies. Contributions that establish the stated milestones under the same conventions are within scope.

Selected references

• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, UPF Economics Working Paper 533, October 21, 2001, pp. 5–15. Working paper.
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004, pp. 15–33. DOI: 10.1287/mnsc.1030.0147.