Revenue Management and Pricing

Motivation

A seller offering several substitutable products must decide whether to charge one common price or a different price for each product. Customers may compare every product's net utility, or they may buy the cheapest product that they can afford. The second behavior is min-buying: a customer checks whether each product's valuation covers its price and selects the cheapest acceptable product. The distinction changes how inexpensive products divert purchases from expensive ones. Cui, Hamilton, Lamperski, and Ganjizadeh Tari study the resulting value of uniform pricing in symmetric and asymmetric valuation environments. The source for this mission is the September 27, 2026 manuscript, including its electronic companion.

Setting

There are $n\ge1$ products. A customer has a nonnegative random valuation vector $V=(V_1,\ldots,V_n)$. A feasible price vector $p=(p_1,\ldots,p_n)$ has nonnegative coordinates. The customer's payment is the smallest $p_i$ among products satisfying $V_i\ge p_i$, or zero if there is no acceptable product. Equal prices create no payment ambiguity. This defines expected differentiated-pricing revenue $R_{\mathrm{DP}}(p)$ and uniform-pricing revenue $R_{\mathrm{UP}}(q)=R_{\mathrm{DP}}(q,\ldots,q)$.

The optimal revenues are $R_{\mathrm{DP}}$ and $R_{\mathrm{UP}}$. The source explicitly assumes that these optima are finite, attained, and that $R_{\mathrm{UP}}>0$. The formal model records those conditions. It does not impose finite expected valuations: fixed finite prices have bounded payments even for valuation laws with infinite first moments. General joint probability measures describe dependent valuations; product measures describe independent valuations.

A law is exchangeable when permuting its product coordinates leaves it unchanged. It is affiliated when it has a joint density or probability mass function $f$ satisfying $f(v)f(w)\le f(v\vee w)f(v\wedge w)$ for every pair of valuation vectors. A nonnegative marginal law is regular when its revenue-quantile curve is concave. Regularity uses interior quantiles, with endpoint conventions stated explicitly; it is not replaced by the stronger monotone-hazard-rate condition.

Formalization targets

Goal: Theorem 4, the exact tight regular-distribution guarantee

For independent, absolutely continuous regular valuation distributions, the target is

$$R_{\mathrm{UP}}\ge x^\star R_{\mathrm{DP}}.$$

The constant is defined exactly. Let $A(0)=0$ and $A(x)=-\log(1-x^2)/x$ for $0<x<1$, and let $c$ solve

$$c'(x)=A'(x)(1-xc(x)),\qquad c(0)=1.$$

Then $x^\star$ is the unique point in $(0,1)$ with $x^\star c(x^\star)=1$. The main target includes this nondegenerate root characterization, the universal guarantee, and sharpness: for every $\varepsilon>0$ there is a finite independent continuous regular instance with $R_{\mathrm{DP}}/R_{\mathrm{UP}}>1/x^\star-\varepsilon$. The number of products can vary with $\varepsilon$. The manuscript's decimal $x^\star\approx0.6986$ is explanatory; no decimal is substituted for the exact constant. These are the two conclusions of Theorem 4, p.17.

Symmetric-market results

Theorems 1 and 2, pp.10 and 13, assert $R_{\mathrm{DP}}=R_{\mathrm{UP}}$ for IID valuations and for exchangeable affiliated valuations, respectively. Supporting targets state the stronger policy comparison proved in the manuscript: every price vector is dominated by a uniform price selected from that vector. Theorem 3, p.15, gives an exchangeable nonnegative valuation law for every positive $n$ such that

$$R_{\mathrm{DP}}\ge\frac{3}{32}\log(n)R_{\mathrm{UP}}.$$

This last construction is discrete and does not carry a density assumption.

Supporting targets

The milestone list includes the independent-revenue identities, the affiliated conditional-threshold comparison, Lemmas 1–4 on triangular and canonical distributions, Lemmas EC.1–EC.2 on rejection probabilities and continuous approximation, and the analytic properties used to specify the exact constant. Additional interface targets identify the concrete triangular probability laws and connect the canonical continuation formulas to actual min-buying revenues. All main results and numbered supporting lemmas of the source are represented in this one mission.

Significance

The symmetric results specify settings where charging different prices gives no revenue advantage. The asymmetric result gives an exact worst-case guarantee and establishes that a better universal fraction cannot hold throughout the stated regular class. The exchangeable lower bound distinguishes symmetry alone from symmetry combined with affiliation. These interpretations follow from the paper's statements and comparisons in Sections 3–4.

The formalization makes the customer payment rule, probability classes, optimization assumptions, and sharpness quantifiers explicit. It also separates an ODE-defined constant from its numerical approximation. The current deliverable consists of locally compiled definitions and open theorem statements, with independent blind read-backs. Statement compilation is not a proof of a theorem; completed Lean proofs are the mission's remaining work.

Mathematical difficulties

Atomic cap distributions require inclusive purchasing and strict rejection probabilities. Substituting a right-continuous CDF for strict rejection at a cap would change the revenue. Affiliation must be used in its density-or-mass-function meaning; the conditional-tail comparison is a theorem to establish. Discrete order statistics can contain ties and need the corresponding multiplicity treatment. The tightness claim must ultimately hold for continuous regular distributions, although several intermediate extremal distributions have atoms. The continuous approximation lemma is therefore part of the target list.

The exact constant requires existence, uniqueness, and maximum properties of its concrete integral benchmark. Those properties are separate conclusions, not hypotheses of the market model. The canonical continuation value is revenue from the designated cap prices; it is not defined to equal the optimal differentiated revenue.

Formalization scope

Valuation and price vectors are real functions on a finite index type. Joint laws are probability measures; no finite support or moment restriction is inserted into the general pricing theorems. The original continuous-market conventions and positive attained optimum conditions are explicit where used. Atomic triangular laws and the exchangeable lower-bound witness have their appropriate separate scopes. Prices are optimized over all nonnegative real vectors, with no fixed ordering imposed on the feasible set; sorted order is required only in formulas that use it.

Regularity is concavity of $qF^{-1}(1-q)$ for $0<q<1$, avoiding undefined endpoint quantiles. For a nonnegative curve this is equivalent to concavity of its zero-endpoint extension. Affiliation covers both a Lebesgue density and a probability mass function on real-valued vectors. The ODE benchmark is an explicit integrating-factor integral; the main goal proves that its root is unique and lies strictly between zero and one. No desired revenue comparison or extremal bound is assumed inside a definition.

Reusable components include the min-buying payment model, strict-rejection identities, quantile regularity, exchangeability and affiliation, triangular laws, and finite-to-continuous comparison. Proofs of these components and of the paper's complete targets are welcome. All code targets Lean 4.33.1 and the pinned Mathlib environment.

Selected references

• Titing Cui, Michael L. Hamilton, Jourdain Lamperski, and Kasra Ganjizadeh Tari, Unit-Demand Pricing for Min-Buying Customers, September 27, 2026 manuscript. SSRN / DOI.

Motivation

A seller can often predict a customer's willingness to pay from observed features, yet may be limited to a small number of prices. The decisions are then coupled: the seller must choose both the customer groups and the price assigned to each group. Grouping customers first and optimizing prices afterward does not generally solve the joint problem. Cui and Hamilton study this joint optimization in Optimal Feature-Based Market Segmentation and Pricing, using the structure of a regression model with a common prediction error.

The central question is when that statistical structure makes optimal segmentation tractable. The main positive result is Theorem 2. The companion results describe hardness without the additional shape condition, approximation by greedy price-menu selection, and the value of allowing more segments. The source for the page-specific formalization is the October 22, 2025, 60-page manuscript available under SSRN 4151103.

Setting

Let $M=\mu(X)\ge0$ denote a predicted valuation and let $E$ denote a mean-zero error independent of the observed features. Realized valuation is $V=M+E$. The general model uses separate probability laws $\nu$ for $M$ and $\eta$ for $E$, with finite first moments. Independence is represented by the shared location family: every customer with predicted value $x$ has valuation law $x+E$.

The inclusive survival function is $S(t)=\Pr(E\ge t)$. At nonnegative price $p$, expected customer revenue is $r(x,p)=pS(p-x)$. Inclusive survival is essential when the error distribution has atoms. A finite price menu $P$ earns

$$F(P)=\int \max\bigl(\{0\}\cup\{r(x,p):p\in P\}\bigr)\,d\nu(x).$$

For a fixed menu, assigning every customer to a revenue-maximizing menu price optimizes its segmentation. Write $R_k=\sup_{|P|\le k}F(P)$, $R_\infty=\int\sup_{p\ge0}r(x,p)\,d\nu(x)$, and $R_k^0$ for the same finite-menu problem with zero error. The MHR condition is encoded for density-bearing error laws by log-concavity of survival on its positive domain, the formulation used in the proof of Lemma 2(b). This permits bounded support and zero purchase probabilities.

Formalization targets

Goal: Theorem 2, optimal computation

For $n$ distinct, sorted predicted values with positive probability masses, independent mean-zero MHR error, and a primitive oracle that returns an optimal block price and its attained revenue, construct a globally optimal policy with at most $k$ contiguous index blocks. Its revenue must equal the specified Bellman recurrence, and the reconstructed policy must dominate every assignment of types to $k$ arbitrary nonnegative prices. If each nonempty block-oracle call costs at most $m$, the specified memoized schedule has

$$T(n,k,m)=O\bigl(n^2(k+m)\bigr).$$

The draft states an explicit upper bound $5n^2(k+m)$ for oracle charges, Bellman candidate evaluations, and backtracking. This is an oracle-operation model for already sorted data; it is not a bit-complexity assertion about evaluating arbitrary real probabilities.

Companion results

Theorem 1 asserts NP-hardness even with finitely supported independent mean-zero noise of polynomial support size. Its target uses an explicit binary encoding of rational input data and polynomial-time finite Turing-machine reductions; $k$ is part of the input. Remark 2 targets normalized, monotone, submodular menu revenue and the greedy guarantee

$$F(G_k)\ge(1-e^{-1})\max_{A\subseteq P,\ |A|\le k}F(A).$$

A separate finite-support target shows that nonnegative realized valuations, together with zero, suffice as candidate prices. Theorem 4 states

$$R_\infty-R_k\le\frac{U-L}{k}$$

for any finite almost-sure prediction bounds $L\le M\le U$. Theorem 5 states diminishing increments,

$$R_{k+2}-R_{k+1}\le R_{k+1}-R_k,\qquad k\ge1,$$

under MHR error. These two targets retain general prediction distributions. Theorem 3 includes almost-sure nonnegative realized valuations. Corollary 2 uses this same setting and includes the factor two confirmed by the author during review.

Significance

Theorem 2 replaces a search over arbitrary segmentations with an optimal interval policy and a quadratic-size block table. The performance results explain how a small menu approaches feature-based personalized pricing and when the incremental value of another segment diminishes. The hardness and approximation targets delineate what remains possible when the MHR restriction is removed.

The draft makes ties, atoms, support endpoints, optimizer attainment, and computational costs explicit. Generic proofs of monotone finite-menu assignment under a TP2 revenue condition and Bellman optimality have been checked locally in the pinned Lean environment. The full paper theorems remain open formal proof obligations; well-formed statements are not completed proofs.

Mathematical difficulties and author-confirmed corrections

The interval argument needs an attaining assignment that is monotone despite ties and all-zero revenue rows. Division by survival probabilities would exclude legitimate bounded-support cases. The complexity claim also needs the block oracle's attained revenue, not merely its price. The hardness target requires an actual polynomial-time reduction and careful centering of the constructed error while preserving nonnegative predicted means.

The author confirmed two corrections on October 30, 2026. Theorem 3 now explicitly assumes $V=M+E\ge0$ almost surely. Corollary 2 now includes the factor two:

$$R_\infty-R_k\le2\sqrt{\frac{2\sigma(\mathbb E[M]+\sigma)}{k}}.$$

Corollary 2 retains the same nonnegative realized-valuation setting used in the corrected Theorem 3. Both results are definitive milestone targets in this draft. Two earlier draft records are retained as clearly labeled superseded copies, with their mathematical statements corrected as well; they are not milestones. The nonnegative-valuation assumption supports the proof's bound $R_\epsilon(x)\le x$. For Corollary 2, minimizing $2j\sigma/k+(\mathbb E[M]+\sigma)/j$ gives the corrected factor two. Formal proofs must still handle conditional truncation, boundary atoms, and zero variance.

Formalization scope

General revenue targets use probability measures on the real line, nonnegative integrable predictions, and integrable mean-zero error. The finite computational model uses strictly increasing predicted values and positive weights summing to one. At most $k$ price slots are allowed; repeated cuts represent unused slots. Index intervals include every type, including the largest support point. Least optimal prices implement a deterministic tie convention; no interior first-order condition or uniqueness assumption is imposed.

The definition layer contains no proof placeholders or new axioms. Real suprema and infima are defined from the feasible economic objects; their attainment and boundedness must be proved where needed. The MHR-to-TP2 bridge is a theorem target, not an assumption that deletes the analytic content. The Bellman recurrence, its partition relation, and its charged evaluation schedule are separate objects. The goal connects that recurrence to the original unrestricted assignment problem and an actual feasible reconstruction.

The general model, the rational binary-input hardness model, and the discrete candidate-price model are explicit interfaces. Their connecting lemmas, optimizer existence, the analytic MHR argument, interval-to-DP reconstruction, and the source's companion results remain available proof obligations. The optional derivative refinement of Lemma 1 and appendix extension/necessity theorems are outside this first proposal. Every uploaded item includes an independent read-back for comparison with its intended mathematical content.

Selected references

• Titing Cui and Michael L. Hamilton, Optimal Feature-Based Market Segmentation and Pricing, Operations Research 74(3), 1354–1370 (2026). DOI. Page citations refer to the October 22, 2025 manuscript, SSRN 4151103.
• Adrien Saumard and Jon A. Wellner, Log-concavity and strong log-concavity: a review, Statistics Surveys 8, 45–114 (2014), Section 11, cited in the source's proof of Lemma 2(b). DOI.