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.