All missions

Motivation

Fast-fashion chains and flash-sale sites rotate their assortments: a product is on display for a short window and is then replaced. Retailers that do this face a choice that a classical assortment model cannot express. They can show the whole catalog at once, or they can conceal part of it and reveal products one at a time. In the classical discrete-choice models, which include multinomial logit, nested logit and Markov chain choice, each consumer buys at most one product, so the order in which products are revealed is immaterial.

Ferreira and Goh (HBS Working Paper 17-041; published in Management Science, 2021, doi:10.1287/mnsc.2020.3610) let consumers buy several products. Each additional purchase is worth less to the consumer than the previous one. This diminishing marginal utility goes back to Marshall and appears in the satiation model of Baucells and Sarin (2007). With it, the order of revelation matters, and the paper asks whether concealment pays.

Setting

A retailer has $N$ products with nonnegative prices $p_1,\dots,p_N$. A consumer has a random valuation shock $X_i$ for each product $i$. The shocks are mutually independent, continuous and integrable random variables on a probability space $(\Omega,\mathbb P)$. The quantity $X_i-p_i$ is the price-adjusted valuation of product $i$. Buying a set $S$ of products gives the consumer the utility

where the marginal utility $v:\mathbb N_0\to\mathbb R$ is nonnegative and decreasing.

• Fixed assortment. The retailer offers a subset $S$ of $M\le N$ products for the whole season. The consumer sees all realized shocks and buys a utility-maximizing set. Lemma 1 shows that she buys in an order $\sigma$ of decreasing price-adjusted valuation (Definition 1), so the retailer earns

• Sequential assortment. The retailer shows one product per period. A consumer who has already bought $k$ items buys the current product $i$ iff $v(k)+X_i-p_i\ge 0$. With $W_{i-1}$ purchases made before period $i$, the revenue is $R^s=\sum_i p_i\,\mathbb 1\{v(W_{i-1})+X_i-p_i\ge 0\}$. The quantity $R_k(n)$ is the revenue from the last $n$ products when the consumer enters them with $k$ purchases.
• Optimized strategies. $\mathbb E[R^f_*]$ is the largest expected fixed revenue over all subsets $S$, and $\mathbb E[R^s_*]$ the largest expected sequential revenue over all orders of all $N$ products. The value of concealment is $\mathrm{VoC}=\mathbb E[R^s_*]-\mathbb E[R^f_*]$.

In Lean a product is a pair (price, realized shock). seqRev v L k is the sequential revenue of a list L for a consumer starting with k purchases, fixedRev v L' is (4) along a list L', and ERsStar, ERfStar are the two optima.

Formalization targets

Goal: Theorem 1 (p. 15)

Let $S$ be an optimized fixed assortment, and let $R$ be the revenue of the sequential assortment showing the same products in decreasing order of prices. Then

Part (b) fixes no constants and asserts only the sign of the value of concealment, which can be zero (Theorem 2 of the paper).

Milestones

1. Lemma 1 (p. 11): buying the products $\sigma(1),\dots,\sigma(D^f)$ maximizes $u$.
2. Lemma 2 (p. 13): $R_{k+1}(n)\le R_k(n)\le \rho^*_n+R_{k+1}(n)$, with $\rho^*_n$ the highest remaining price.
3. Lemma 4 (p. 38): if the first product has the highest price and $X_1-p_1\le X_2-p_2$, interchanging products 1 and 2 does not raise the revenue.
4. Proof of Theorem 1 (p. 39): in a Definition-1 order the sequential revenue equals $R^f$.
5. Theorem 1(a) for every fixed assortment: $R\ge R^f$ pathwise.
6. Remark 1 (p. 12): appending a product never lowers $R^s$.

Significance

The result. Theorem 1 says that concealment never hurts a retailer facing multi-purchase consumers with diminishing marginal utility. Part (a) also gives a concrete policy, independent of the shock distributions: take the optimal fixed assortment and reveal its products from the most to the least expensive. The paper reads the gain as structural: the retailer learns nothing from offering products sequentially, yet it still gains from them. The rest of the paper builds on it. Theorem 2 characterizes when the value of concealment is zero, Theorem 3 gives its asymptotics, and §6 measures the decreasing-price heuristic numerically.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The mission produces a reusable model of a multi-purchase consumer under fixed and sequential presentation, together with its basic monotonicity facts (Lemma 2, Remark 1). The goal is also stated pathwise, which is stronger than the paper's "with probability 1".

Difficulty

The obvious approach compares the two strategies product by product, and it fails. Under the fixed assortment the purchase decision for a product depends on its rank among the realized price-adjusted valuations. Under the sequential assortment it depends on the number of earlier purchases, which in turn depends on every earlier shock. Neither revenue is monotone in the order of presentation. Swapping two adjacent products can raise or lower the revenue, depending on the realization and on which of the two is more expensive. Lemma 4 identifies the one swap whose sign is controlled, and Lemma 2 bounds how far an extra purchase can shift the remaining revenue. The difficulty is to arrange swaps of this kind into a sorting of the decreasing-price sequence into a Definition-1 order, and to keep the bookkeeping exact when prices or valuations tie.

Formalization scope

• Products are pairs (price, realized shock), sequences are lists, and positions are 0-based: the paper's position $i$ with $v(i-1)$ is list position $i-1$.
• The marginal utility $v$ is taken directly, nonnegative and antitone, rather than through the concave $V$ of (2).
• Prices are nonnegative. The paper leaves this implicit, and Lemma 2's lower bound needs it.
• The purchase rule is $v(k)+X-p\ge 0$ everywhere, including $R_k(n)$, for which (7) prints $>0$. The two differ only on a null event for continuous shocks.
• All "with probability 1" statements are proved for every realization. The milestones are stated for arbitrary lists, with ties in prices and in valuations allowed.
• $R^f(S)$ uses the canonical Definition-1 order, with ties broken by smaller index. Every other order gives the same revenue off the null event of a tie.
• $\mathbb E[R^s_*]$ is a maximum over the orders of all $N$ products, and $\mathbb E[R^f_*]$ a maximum over all subsets, the empty set and strict subsets included. Both maxima range over finite sets, and the revenues are bounded and measurable, so the integrals are genuine.
• Independence, continuity and integrability of the shocks are the paper's standing assumptions and stay in the goal, although the inequality does not use them.

Trivializing encodings are ruled out: $R^f$ is the positional formula (4), not the sequential revenue in $\sigma$-order. Restricting $R^s_*$ to the $M$ products of the fixed assortment, or $R^f_*$ to the full set, would change the claim and is not done.

The development needs only finite sums, lists and permutations from Mathlib, plus Bochner integrals of bounded random variables. The list-level lemmas about seqRev (Lemmas 2 and 4, Remark 1) apply to any sequential-purchase model with diminishing marginal utility. Contributions are welcome on every milestone, and on general list-sorting lemmas that carry an interchange argument from adjacent swaps to a full permutation.

Not formalized here: Lemma 3 and Corollaries 1–2 (optimal sequences under hazard-rate and IFR conditions), Theorems 2–3, the forward-looking consumer model of §5, and the numerical study of §6.

Selected references

• K. J. Ferreira and J. Goh, Assortment Rotation and the Value of Concealment, Harvard Business School Working Paper 17-041 (2020 revision); Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3610
• M. Baucells and R. K. Sarin, Satiation in discounted utility, Operations Research 55(1), 2007. https://doi.org/10.1287/opre.1060.0322
• F. Caro and V. Martínez-de-Albéniz, Product and price competition with satiation effects, Management Science 58(7), 2012. https://doi.org/10.1287/mnsc.1110.1484
• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

Schools, universities and public employers that run affirmative action decide whom to admit from a set of applicants who are ranked by a priority ordering (exam scores, lottery numbers, seniority) and who belong to a minority or a majority group. The procedures used in practice, such as the reserve and quota systems of Boston, Chicago and New York school choice, or the reservation system of India's public sector, are choice rules: functions from the set of applicants, their types and their priorities to the set of admitted students. Market design needs these rules to be substitutable (a chosen student stays chosen when other applicants withdraw), because substitutability is the condition under which centralized clearinghouses produce stable matchings (Hatfield and Milgrom, 2005; Hatfield and Kojima, 2008).

B. Doğan and K. Yıldız, Choice with Affirmative Action (SSRN 3626941; Management Science, doi:10.1287/mnsc.2022.4447), ask which affirmative action rules are substitutable and also respond monotonically to the minority students they are meant to help. Their Theorem 1 says that such rules are exactly reserve rules whose reserve number changes by at most one in response to a type or priority change. This mission formalizes the direction of Theorem 1 that the paper proves correctly: every such rule is a bounded reserve rule.

Setting

Fix a nonempty finite set $\mathcal S$ of students and a capacity $q\ge3$. A problem $(S,\tau,\succ)$ is a set $S\subseteq\mathcal S$ of applicants, a type function $\tau$ ($\tau(s)=1$ minority, $\tau(s)=0$ majority) and a strict priority ordering $\succ$ on $S$. The rank of $s$ is one plus the number of students with higher priority. The top tier $T$ is the set of students of rank at most $q$, the students a pure priority rule would admit; the bottom tier is $B=S\setminus T$. Superscripts $m$ and $M$ select minority and majority students: $T^m$, $T^M$, $B^m$, $S^M$.

A choice rule $C$ picks a subset $C(S,\tau,\succ)\subseteq S$ of at most $q$ students. $C^m$ is the set of chosen minorities and $C^A=C^m\cap B$ the minorities chosen via affirmative action. The axioms are:

• capacity-filling: $|C(S,\tau,\succ)|=\min\{|S|,q\}$;
• neutrality: whether the $k$-th ranked student is chosen depends only on the sequence of types by rank;
• priority-compatibility: a chosen student may have lower priority than a rejected one only if the former is a minority and the latter a majority student.

An affirmative action rule satisfies these three. Substitutability requires $s\in C(S',\tau|_{S'},\succ|_{S'})$ whenever $s\in C(S,\tau,\succ)$ and $s\in S'\subseteq S$. MPI (monotonicity in priority improvements) requires that improving the priority of a chosen minority student does not reject any chosen minority student. MTC (monotonicity in type changes) requires that turning a chosen minority student into a majority student does not reject any other chosen minority student.

A reserve function $R$ gives each problem a number $R(S,\tau,\succ)\le|T^M|$ that depends only on the types of the students of ranks $1,\dots,q$. $C$ admits a reserve representation via $R$ if $C$ chooses all of $T^m$, then the $R$ highest-priority students of $B^m$ (all of them if fewer), then the highest-priority majority students until the seats are filled. The representation is bounded if $R$ satisfies Condition B: changing the type of a top-tier minority, improving a top-tier minority's rank, or worsening a top-tier majority's rank changes $R$ by $0$ or $+1$, and worsening the rank of a top-tier majority $M$ leaves $R$ unchanged when $M$ is among the $R$ lowest-ranked top-tier majorities.

Formalization targets

Goal: Theorem 1 (⇒), p. 10

Milestones

1. Lemma 1 (p. 20): for a substitutable affirmative action rule, two problems with the same students and types and coinciding top tiers have the same number of chosen minority students.
2. The reserve of the proof (p. 20): the function $R_C(S,\tau,\succ)$, the largest $|C^A|$ among problems with the same top-tier type configuration, is a reserve function, and $C$ is represented by it. No monotonicity axiom is needed.
3. Satisfies B1, B2, B3-i, B3-ii (pp. 20–22): under MPI and MTC, $R_C$ satisfies each part of Condition B.

Milestones 2 and 3 together give the goal, with $R=R_C$.

Significance

The result describes every substitutable, monotone affirmative action rule by one integer per top-tier type configuration, constrained by local bounds. A designer who wants substitutability, so that the rule can be plugged into a deferred-acceptance clearinghouse, and wants monotonicity in the minority students' favour, therefore only has to choose a reserve schedule. The paper's lexicographic and stepwise-adjusted–reserves rules (§5) are built on this description.

Formalizing it has a second purpose. Theorem 1 is printed as an equivalence, but its (⇐) half is false. Take $q=3$ and the reserve $R=1$ when the top tier has at most one minority, $R=0$ otherwise. This $R$ satisfies B1–B3. With priorities $a\succ b\succ c\succ d\succ e$ and minorities $d,e$, the rule chooses $\{a,b,d\}$ from $\{a,b,c,d,e\}$ but $\{a,d,e\}$ from $\{a,b,d,e\}$, so removing the rejected student $c$ rejects $b$, and substitutability fails. The same failure occurs in the paper's Example 1 ($q=100$), and the error sits in Case 3 of the (⇐) proof on p. 23. The mission therefore poses only the (⇒) half, which planning checked by exhaustive search for every capacity $q\le5$ and every universe of up to seven students. A machine-checked proof would settle that half for every $q$ and every universe. No formalization of this result, or of affirmative action choice rules in this model, exists on the platform or in Mathlib.

Difficulty

The reserve that represents $C$ has to be defined from $C$ alone. The obvious candidate, the number of affirmative-action admissions at the problem itself, is not a reserve function: it depends on how many minorities happen to sit in the bottom tier, while a reserve function may depend only on the top tier. Showing that a well-defined reserve exists already uses neutrality, substitutability and capacity-filling together (Lemma 1). The bounds of Condition B then compare reserves at problems whose top tiers differ. The monotonicity axioms give only the lower half of each bound, "the reserve does not fall"; the upper half, "the reserve rises by at most one", and the equality of B3 (ii) are not consequences of MPI or MTC and need substitutability. Small universes are a further obstacle: the paper's argument works with problems containing $q$ minority students and more than $2q$ students, which a small $\mathcal S$ does not contain, while the goal makes no assumption on $|\mathcal S|$.

Formalization scope

Everything lives in the namespace AffirmativeChoice.Reserve, in one definitions file and seven theorems.

• A Problem holds S : Finset 𝒮, τ : 𝒮 → Bool (true = minority) and pri : 𝒮 → ℕ with s ≻ s' ↔ pri s < pri s', injective on S. Only values on S matter; restriction keeps τ and pri.
• Ranks are 1-based; the top tier is rank ≤ q; the type of the k-th ranked student is an Option Bool, none beyond |S|.
• A ChoiceRule 𝒮 q carries only C P ⊆ P.S, |C P| ≤ q and nonemptiness for nonempty S; the axioms are separate predicates.
• The reserve procedure is a closed set formula, reserveChoice, with the majority cap $q-|T^m|-\min\{R,|B^m|\}$.
• B2 and B3 are read with the moving student in the top tier before the move, as the proof uses them. The printed typos on p. 6 ("$S\in\mathcal S$", "$\tau(s)=\tau'(s)$") are read as $S\subseteq\mathcal S$ and $\tau(s')=\tau'(s')$.
• The reserve of the proof is canonicalReserve, an sSup on ℕ over problems with the same top-tier type configuration. It agrees with the paper's $R(\rho)$ whenever the paper's witness problem exists.
• The goal assumes $q\ge3$ (the paper's standing assumption) and no lower bound on $|\mathcal S|$.

Ruled out: problems encoded as type words, which quotients away neutrality; reserve functions defined only on type words; axioms built into the choice-rule structure; an existential $R$ that is not required to be a reserve function; or a reserve procedure that may admit bottom-tier majority students. Each of these would make the goal different from, or weaker than, the paper's. The (⇐) half and the full equivalence are not stated in any item.

Contributions welcome: the finite-order combinatorics of ranks, tiers and improvements, which is reusable for other priority-based choice models (reserves, quotas, slot-specific priorities); proofs of the milestones in any order; and a formal proof of the counterexample to the (⇐) half.

Selected references

• B. Doğan and K. Yıldız, Choice with Affirmative Action, SSRN working paper 3626941, version of October 17, 2021; Management Science (2023). https://ssrn.com/abstract=3626941, https://doi.org/10.1287/mnsc.2022.4447
• J. W. Hatfield and P. Milgrom, Matching with Contracts, American Economic Review 95(4), 2005. https://doi.org/10.1257/0002828054825466
• J. W. Hatfield and F. Kojima, Matching with Contracts: Comment, American Economic Review 98(3), 2008. https://doi.org/10.1257/aer.98.3.1189
• H. Chernoff, Rational Selection of Decision Functions, Econometrica 22(4), 1954. https://doi.org/10.2307/1907363

Motivation

A retail store manager does two kinds of work that the firm cannot observe directly: operational effort, which keeps shelves stocked, and marketing effort, which draws customers. The firm sees only the outcomes, namely how much inventory was available and how much was sold. Sales are the smaller of inventory and demand, so whenever the shelf runs empty the true demand is hidden. This is demand censoring, and it links the two tasks: a sales figure equal to the inventory level says little about how hard the manager worked on marketing.

T. Dai, R. Ke and C. T. Ryan (SSRN 3235866; Management Science, doi:10.1287/mnsc.2020.3651) study the principal–agent problem this creates, with a risk-neutral, limited-liability manager whose pay lies between $0$ and a cap $\bar w$. With the bang-bang approach of their §4, they show that an optimal plan pays either nothing or the full bonus $\bar w$, according to whether a weighted likelihood-ratio statistic of the observed pair (inventory, sales) clears a trigger $t$. In the two-effort-level case, the bonus region has a distinctive mast-and-sail shape. Their §6 asks whether such a plan is monotone, meaning that more inventory or more sales never lowers the pay. A non-monotone plan invites ex post moral hazard: the manager would gain by discarding stock. The goal of this mission is the paper's answer, Proposition 5.

Setting

Inventory $I$ takes values in $[0,\bar I]$ and demand $Q$ in $[0,\bar Q]$, with $0<\bar I<\bar Q$. Under low and high operational effort, inventory has densities $f(\cdot\mid e^L_o)$ and $f(\cdot\mid e^H_o)$; under low and high marketing effort, demand has densities $g(\cdot\mid e^L_m)$ and $g(\cdot\mid e^H_m)$, with distribution function $G(\cdot\mid e_m)$. Inventory and demand are independent. Each density is continuous, strictly positive on its closed support, and integrates to $1$ there. The monotone likelihood ratio property (MLRP) holds: $f(i\mid e^L_o)/f(i\mid e^H_o)$ is nonincreasing in $i$, and $g(s\mid e^L_m)/g(s\mid e^H_m)$ is nonincreasing in $s$.

Sales are $S=\min\{I,Q\}$. A compensation plan $w(i,s)$ is defined on the domain $D=\{(i,s):0\le s\le i\le\bar I\}$. Points with $s<i$ are no-stockout (NSO) outcomes and points with $s=i$ are stockout (SO) outcomes. The firm wants both efforts high. For nonnegative weights $\omega_{e^H_o,e^L_m},\omega_{e^L_o,e^H_m},\omega_{e^L_o,e^L_m}$ summing to $1$, one for each deviation, define

The plan (11) pays $\bar w$ on the sail $B^{NSO}=\{(i,s)\in D:s<i,\ \varphi^{NSO}(i,s)\ge t\}$ and on the mast $B^{SO}=\{(i,i)\in D:\varphi^{SO}(i)\ge t\}$, and pays $0$ elsewhere. The critical inventories are $i_s$, the least $i$ with $\varphi^{NSO}(i,i)\ge t$, and $i_m$, the least $i$ with $\varphi^{SO}(i)\ge t$; each equals $\bar I$ when no such $i$ exists. The sail boundary $s^*(i)$ is the least $s$ with $\varphi^{NSO}(i,s)\ge t$.

A plan is monotone in $i$ (in $s$) if raising inventory (sales) within $D$ never lowers pay. It is jointly monotone if $w(i',s')\le w(i'',s'')$ whenever both points lie in $D$, $i'<i''$ and $s'<s''$.

Formalization targets

Goal: Proposition 5 (p. 16)

For every plan $w$ of the form (11) with $\bar w>0$:

Milestones

• Lemma 1 (p. 12): the joint distribution function of $(I,S)$, $\Pr(I\le i,S\le s)=F(s)+G(s)[F(i)-F(s)]$ for $s<i$ and $F(i)$ for $s=i$.
• Lemma OA3 (p. oa4): the ratios $f_L/f_H$, $(1-G_L)/(1-G_H)$ and $g_L/g_H$ are nonincreasing, and nonconstant when the distributions differ.
• Survival versus density (proof of Proposition 3, p. oa6): $(1-G_L(i))/(1-G_H(i))\le g_L(i)/g_H(i)$, strictly under strict MLRP of $g$.
• Proposition 1 (p. 14): $B^{NSO}=\{(i,s):i\ge i_s,\ s^*(i)\le s<i\}$, with $s^*$ nonincreasing and continuous and $i_s\in(0,\bar I]$.
• Proposition 2 (p. 14): $B^{SO}=\{(i,i):i\ge i_m\}$ with $i_m\in(0,\bar I]$.
• Proposition 3 (p. 14): $i_s\ge i_m$.

By Proposition 3, part (ii) and part (iii) of the goal together cover every plan.

Significance

Proposition 5 shows that a mast-and-sail plan fails to be monotone in inventory exactly when the mast starts strictly below the sail. In that case a manager whose sales $s\in[i_m,i_s)$ fall just short of the inventory level would gain by discarding the unsold units. The outcome then becomes a stockout $(s,s)$ on the mast, which earns the bonus, instead of a no-stockout point below the sail, which earns nothing. This ex post moral hazard is the paper's motivation for studying the cost of imposing monotonicity in its later sections. Propositions 1–3 describe the optimal plan's bonus region completely, and Lemma OA3 records the stochastic-order facts the analysis rests on: MLRP implies a hazard-rate ordering of the demand distributions.

The results are proved in the paper and its online appendix. No machine-checked version of any of them is known. The mission states them under the standing assumptions made explicit, about canonical thresholds rather than existential witnesses, and for every plan of the form (11) rather than only optimal ones. Under this reading Propositions 3 and 5 are slightly stronger than printed. Two printed claims need an added hypothesis to be true, and the mission states these honestly: the continuity of $s^*$ in Proposition 1, and the strict survival-versus-density inequality.

Difficulty

The goal's statement is elementary, but every step depends on joint properties of the two ratio functions on the whole domain. These are monotonicity of $\varphi^{NSO}$ in both arguments, monotonicity of $\varphi^{SO}$, continuity, and the comparison $\varphi^{SO}(i)\ge\varphi^{NSO}(i,i)$. The last of these is a hazard-rate statement about integrated tails, not a pointwise MLRP fact. The thresholds are infima of level sets, so each part of the goal requires showing that the infimum is attained, and handling the empty cases (an empty sail, an empty mast) where the thresholds default to $\bar I$. Joint monotonicity is strict in both coordinates, so it does not follow from the product order on $\mathbb R^2$.

Formalization scope

All objects live in MastSail.Monotone. A model bundles $\bar I$, $\bar Q$ and the four densities as real functions, which are read only on $[0,\bar I]$ or $[0,\bar Q]$. Distribution functions are interval integrals from $0$. Pairs are ordered (inventory, sales). The standing assumptions add two things to the printed model: strict positivity of the densities on the closed supports (from §4, p. 9) and $\bar I<\bar Q$ (the paper has $\bar Q\ge\bar I$). These ensure that every ratio has a positive denominator, so no ratio defaults to division by zero. The paper's "$\min\{\cdot:\varphi=t\}$" is read as the least point with $\varphi\ge t$. The weights range over the three deviations from the target. Optimality of the plan is never assumed. Proposition 1 additionally takes strict MLRP of $g$ and $t>0$; Proposition 2 takes $0<t\le\varphi^{SO}(\bar I)$. The goal takes only $\bar w>0$.

The plan and the thresholds are the model's own definitions. A Proposition 5 stated for abstract regions shaped like a mast and a sail, or for thresholds supplied as hypotheses, would be set geometry and does not count. A complete development needs interval integrals, monotone level sets of continuous functions, and product measures with densities (for Lemma 1). The likelihood-ratio-to-hazard-rate comparison for densities on an interval can be reused well beyond this mission. Proofs of any milestone are welcome, as are proofs of the strict variants under weaker hypotheses.

Selected references

• T. Dai, R. Ke, C. T. Ryan, Incentive Design for Operations-Marketing Multitasking, Management Science, 2021; accepted version SSRN 3235866. https://ssrn.com/abstract=3235866, https://doi.org/10.1287/mnsc.2020.3651
• S. J. Grossman, O. D. Hart, An Analysis of the Principal-Agent Problem, Econometrica 51(1), 1983. https://doi.org/10.2307/1912246
• W. P. Rogerson, The First-Order Approach to Principal-Agent Problems, Econometrica 53(6), 1985. https://doi.org/10.2307/1911033
• A. Barvinok, A Course in Convexity, AMS Graduate Studies in Mathematics 54, 2002. https://doi.org/10.1090/gsm/054

Pricing without knowing demand

A firm launching a new product (a drug, a software package, a digital download) must choose a price before it has data on its demand curve. Classical monopoly pricing needs the whole demand curve: the optimal price balances marginal revenue against marginal cost, and both depend on the curve's shape. Cohen, Perakis and Pindyck (Management Science; accepted version SSRN 2673810) ask how well a firm can do when it knows only two numbers: its constant marginal cost $c$ and the maximum price $P_m$, the price at which consumers stop buying. Their answer is a rule that needs nothing else: charge the price that would be optimal if demand were linear through $(0, P_m)$. They give closed-form performance guarantees for this rule under several demand families. The guarantee that holds for an entire nonparametric class is the one for concave inverse demand, and that is the subject of this mission.

The setting matters in practice when the firm need not plan output in advance (zero or near-zero marginal cost, no capacity decision): then the only decision is the price, and the slope of the demand curve, which determines how much will be sold, is immaterial for choosing it.

Setting

A market consists of

• a maximum price $P_m$ and a marginal cost $c$ with $0 \le c < P_m$;
• a saturation quantity $Q_{\max} > 0$: no more than $Q_{\max}$ units can be sold, however low the price;
• the actual inverse demand $P_A(Q)$, the price at which exactly $Q$ units are demanded, defined on $[0, Q_{\max}]$, with $P_A(0) = P_m$, non-increasing and continuous.

Selling $Q$ units at the market-clearing price earns the profit $\Pi(Q) = (P_A(Q) - c)\,Q$. A firm that knew $P_A$ would choose an optimal quantity $Q^{**}$ maximizing $\Pi$ on $[0, Q_{\max}]$, charge the optimal price $P^{**} = P_A(Q^{**})$, and earn $\Pi^{**} = \Pi(Q^{**})$.

The demand at price $p$ is $Q_A(p) = \sup\{Q \in [0, Q_{\max}] : P_A(Q) \ge p\}$, the quantity sold when the firm charges $p$.

If demand were linear, $P(Q) = P_m - bQ$ with $b > 0$, the profit $(P_m - bQ - c)Q$ would be maximized at $Q^*_L = (P_m - c)/2b$, at the price

which does not depend on $b$. This is the linear price. The linear pricing rule charges $P^*$ whatever the true demand is, and earns $\Pi^* = (P^* - c)\,Q_A(P^*)$.

In Lean these objects are Market, Market.Standing, profit, IsOptQty, linPrice, demandAt and linProfit in the namespace LinearPriceRule.Concave.

Formalization targets

Goal: Proposition 5 (p. 13)

If $P_A$ is concave on $[0, Q_{\max}]$, then an optimal quantity exists, $\Pi^* > 0$, and every optimal quantity satisfies

Milestones

1. Eq. (1), §1.4, p. 4. Under linear inverse demand $P_m - bQ$, the profit is uniquely maximized at $Q^*_L = (P_m - c)/2b$, and the price there is $(P_m + c)/2$.
2. Theorem 1, concave case, p. 9. If $P_A$ is concave, every optimal price satisfies $P^{**} \ge P^*$.
3. Proof of Proposition 5, p. 26. $Q_A$ is non-increasing on $(-\infty, P_m]$, and $Q_A(P^{**}) = Q^{**}$, so $\Pi^{**} = (P^{**} - c)\,Q_A(P^{**})$.
4. Theorem 1, convex case, p. 9. If $P_A$ is convex and the optimum is interior ($Q^{**} < Q_{\max}$), then $P^{**} \le P^*$.
5. Remark after Proposition 5, p. 13. For a rectangular demand ($P_A \equiv P_m$ on $[0, Q_{\max}]$), $\Pi^{**}/\Pi^* = 2$, and $P^{**}/P^* = 2$ when $c = 0$.

Significance

Proposition 5 is a distribution-free guarantee: across the whole class of concave inverse demands, which contains linear, concave quadratic and many other shapes, a rule that uses only $P_m$ and $c$ loses at most half of the optimal profit. The rectangle shows that the factor $2$ cannot be improved within the class. Theorem 1 says in which direction the rule errs, under-pricing for concave and over-pricing for convex inverse demand, so a firm with qualitative information about curvature knows which way to adjust. The paper's parametric results (quadratic, monomial, semi-log, log-log demand) and its welfare comparisons are built on the same model.

The results are proved in the paper. As far as is known, none of them has been formalized. This mission provides a machine-checked model of a monopolist facing an unknown inverse demand on a bounded quantity interval, which other robust-pricing statements can reuse, together with the paper's argument for the concave case, carried out without the differentiability its Taylor-expansion proof of Theorem 1 assumes.

Difficulty

The paper's proof of Theorem 1 writes $P_A(Q) = P_m - bQ + f(Q)$, equates marginal revenue with marginal cost, and applies a second-order Taylor expansion. None of this is available for the statement as formalized: $P_A$ is only continuous and concave, it may have kinks (the rectangle has one at $Q_{\max}$), and the optimum may sit at the corner $Q^{**} = Q_{\max}$, where the first-order condition fails. A proof must compare the profit at $Q^{**}$ with profits at other quantities using only the defining inequality of concavity.

The second subtlety is the demand $Q_A$, a supremum over a set. Identifying $\Pi^*$ with the profit of an actual quantity, and $Q_A(P^{**})$ with $Q^{**}$, needs continuity and the optimality of $Q^{**}$: a flat stretch of $P_A$ at the optimal price would otherwise let $Q_A(P^{**})$ exceed $Q^{**}$.

The convex half of Theorem 1 is false at a corner optimum. For $P_A(Q) = 5 - Q/10$ on $[0, 1]$ and $c = 1$, the optimum is $Q^{**} = 1$ with $P^{**} = 4.9 > P^* = 3$. That milestone therefore assumes $Q^{**} < Q_{\max}$.

Formalization scope

• $P_A$ is a function $\mathbb R \to \mathbb R$. Only its values on $[0, Q_{\max}]$ matter: monotonicity, continuity, concavity and convexity are assumed on $[0, Q_{\max}]$, and optimality and $Q_A$ range over $[0, Q_{\max}]$. Concavity on all of $[0, \infty)$ together with nonnegativity would force $P_A$ to be constant, so it is not used.
• The standing assumptions are $0 \le c < P_m$, $0 < Q_{\max}$, $P_A(0) = P_m$, and $P_A$ non-increasing and continuous on $[0, Q_{\max}]$. Nonnegativity of $P_A$ is not assumed. Continuity guarantees that an optimum exists and that $Q_A(P^*)$ is actually sold at $P^*$.
• "Concave demand curve" is read as concavity of the inverse demand $P_A$ in $Q$. Proposition 5's proof invokes Theorem 1, which is about $P_A$.
• The firm optimizes over quantities, and $P^{**}$ is read off as $P_A(Q^{**})$. All bounds are stated for every optimal quantity, and existence is a separate clause.
• $Q_A(p)$ is the supremum of $\{Q \in [0, Q_{\max}] : P_A(Q) \ge p\}$, and $\Pi^* = (P^* - c)\,Q_A(P^*)$ is the profit of charging $P^*$, not the profit at some quantity.
• Ratios are real divisions, and the goal asserts $\Pi^* > 0$. Without the clauses "an optimum exists" and "$\Pi^* > 0$", the goal could hold vacuously or through the convention $x/0 = 0$. These clauses are part of the statement and rule out that trivialization.
• No differentiability is assumed anywhere.

Only Mathlib's convexity and order-theoretic infrastructure (ConcaveOn, ConvexOn, AntitoneOn, sSup on ℝ, the extreme value theorem on compact intervals) is needed. Proofs of the milestones are welcome in any order. The parametric Propositions 1–4, the welfare results (Propositions 6–7) and the uncertain-$P_m$ analysis of §3 are outside this mission.

Selected references

• M. C. Cohen, G. Perakis, R. S. Pindyck, A Simple Rule for Pricing with Limited Knowledge of Demand, Management Science. https://doi.org/10.1287/mnsc.2020.3602 — accepted version: SSRN 2673810, https://ssrn.com/abstract=2673810 (the version cited by page in this mission).

Procurement under a hard budget

A buyer with a fixed budget wants to hire a team from a pool of sellers, each of whom knows privately what participating would cost them. The buyer values teams through a set function and pays each hired seller. The sellers are strategic: they report whatever cost serves them best. A budget-feasible mechanism decides whom to hire and what to pay so that reporting the true cost is optimal for every seller, nobody is paid less than their reported cost, and the total payment never exceeds the budget. The model was introduced by Singer (FOCS 2010). It describes crowdsourcing marketplaces that recruit workers under a fixed task budget, and influence-maximization campaigns that recruit seed users of a social network.

Budget feasibility is what separates the model from classical mechanism design. The truthful VCG mechanism pays far more than any fixed budget. The question is how much value is lost when the payment rule must be truthful and stay within the budget.

Timeline (as surveyed in arXiv:1905.00848v2, pp. 2–5):

• Singer (FOCS 2010) gave a randomized $O(1)$-approximation mechanism for monotone submodular valuations.
• Chen, Gravin and Lu (SODA 2011) improved the ratio. They also gave a deterministic $O(1)$ mechanism that runs in superpolynomial time.
• Dobzinski, Papadimitriou and Singer (EC 2011) gave an $O(\log^2 n)$ mechanism for subadditive valuations. They also gave the first constant-factor mechanisms for one non-monotone class, cut functions.
• Bei, Chen, Gravin and Lu (STOC 2012; SIAM J. Comput. 2017) improved the subadditive ratio to $O(\log n/\log\log n)$. They gave a randomized $O(1)$ mechanism for XOS valuations that takes exponential time in the value query model.
• Amanatidis, Birmpas and Markakis (WINE 2017) gave $O(1)$ mechanisms for symmetric submodular valuations.

For general non-monotone submodular valuations no budget-feasible $O(1)$-approximation mechanism was known before Amanatidis, Kleer and Schäfer (arXiv 2019; Mathematics of Operations Research, 2022). Their offline result is the subject of this mission. The obstacle is that the payments of Singer-style greedy mechanisms can be unbounded once $v$ is not monotone.

Setting

There is a finite set $A$ of agents. Agent $i$ has a private cost $c_i\in[0,B]$, where $B>0$ is the budget. The valuation $v:2^A\to\mathbb R$ is normalized ($v(\emptyset)=0$), non-negative and submodular: $v(S\cup T)+v(S\cap T)\le v(S)+v(T)$. It need not be monotone. The marginal value of $i$ with respect to $S$ is $v(i\mid S)=v(S\cup\{i\})-v(S)$. The benchmark is

A deterministic mechanism consists of an outcome rule $f$, which maps declared costs $b$ to a set $f(b)$ of winners, and a payment rule. Throughout, payments are threshold payments: a winner is paid the largest bid with which it would still win, and a loser is paid nothing. A mechanism is truthful if declaring $c_i$ maximizes each agent's utility (payment minus cost if it wins, $0$ otherwise) whatever the others declare. It is individually rational if winners are paid at least their bids, and budget-feasible if the payments sum to at most $B$. A randomized mechanism is universally truthful if it is a probability distribution over deterministic mechanisms that are all truthful.

Simultaneous Greedy$(D,v,c,B,x)$ grows two candidate solutions $S_1,S_2$ with separate budgets $B_1=B_2=B$. It repeatedly takes the agent–solution pair $(\hat\imath,\hat\jmath)$ of largest positive marginal value and offers $\hat\imath$ the take-it-or-leave-it price $\frac{\beta B}{x}v(\hat\imath\mid S_{\hat\jmath})$. If $\hat\imath$ accepts and the price fits into $B_{\hat\jmath}$, it joins $S_{\hat\jmath}$; either way it is removed from the pool. The output is the best of $S_1,S_2$ and two unconstrained 2-approximate improvements $\mathrm{alg}_2(S_1),\mathrm{alg}_2(S_2)$. Sample-then-Greedy splits $A$ uniformly at random into $A_1,A_2$, estimates $x=v(\mathrm{alg}_1(A_1))$ with an $e$-approximation $\mathrm{alg}_1$ for the knapsack problem on $A_1$, and runs Simultaneous Greedy on $A_2$ with $\beta=9.185$. GenSm-Main hires the single most valuable agent $i^*$ with probability $p=0.201$ and runs Sample-then-Greedy otherwise.