Revenue Management and Pricing

Motivation

A retailer choosing which products to display, a platform choosing which items to recommend, and a broadcaster choosing which content to stream all face an assortment problem: offer a set of products, observe what customers buy, and earn the revenue of the purchased item. The standard demand model is the multinomial logit (MNL) model, under which the optimal assortment without capacity constraints consists of the most profitable products (Talluri and Van Ryzin, 2004). When the customers' preferences are unknown, the seller must learn them from sales, and the quality of a learning policy is measured by its regret: the cumulative revenue lost relative to an omniscient seller.

When the product catalogue is very large, or products are described by a continuous attribute such as quality, the discrete model becomes a continuum. Peeters, den Boer and Mandjes (arXiv:1807.06497, published in Operations Research, 2022) introduced a continuous analogue of the MNL model and studied learning in it. Their first main result, the goal of this mission, is that a simple stochastic approximation policy has worst-case regret of order $\log T$ over $T$ customers.

• 1951: Robbins and Monro introduce stochastic approximation for finding the root of a function observed with noise (doi:10.1214/aoms/1177729586).
• 2010: Rusmevichientong, Shen and Shmoys give adaptive policies for capacitated MNL assortment (doi:10.1287/opre.1100.0866).
• 2011: Broadie, Cicek and Zeevi give mean-square rates for Kiefer–Wolfowitz type stochastic approximation (doi:10.1287/opre.1110.0970).
• 2019: Agrawal, Avadhanula, Goyal and Zeevi give an $\tilde O(\sqrt{NT})$-regret UCB policy for discrete MNL bandits (doi:10.1287/opre.2018.1832).
• 2021/2022: Peeters, den Boer and Mandjes prove $O(\log T)$ worst-case regret for the continuum model, with a matching $\Omega(\log T)$ lower bound.

Setting

The products are the points $x\in[0,1]$, and the revenue function $w:[0,1]\to[0,1]$ is continuously differentiable with $w'\ge k>0$. An assortment is a Borel set $S\subseteq[0,1]$; $\mathcal S$ is the set of all of them. A customer offered $S$ buys a product in a Borel set $A\subseteq S$, or buys nothing ($\emptyset$), with probabilities

where the preference function $v$ is unknown to the seller. The expected revenue of $S$ is $r(S,v)=\int_S vw\big/(1+\int_S v)$, and $\varrho^*=\max_{S\in\mathcal S}r(S,v)$.

The class $\mathcal V(\underline v,\overline v,D)$ (Assumption 1) contains the integrable $v$ with $\underline v\le v\le\overline v$ on $[0,1]$ that are differentiable on $(0,1)$ with $|v'|\le D$, where $\overline v>\underline v>0$ and $\overline v>w(0)/\int_0^1(w-w(0))$.

The generalized inverse is $w^{-1}(\varrho)=\min\{x\in[0,1]:w(x)\ge\varrho\}$, and $h(\varrho)=r([w^{-1}(\varrho),1],v)$. The policy SAP$(\alpha,\beta)$ starts at $\varrho_1\in[0,1]$, offers $S_t=[w^{-1}(\varrho_t),1]$ in period $t$, observes the revenue $R_t=w(X_t)\mathbf 1\{X_t\in S_t\}$, and updates

Given the history, the purchase $X_t$ has the law of $X^{S_t}$. The regret over $T$ periods is $\Delta_\pi(T,v)=\sum_{t=1}^T\mathbb E_\pi[\varrho^*-r(S_t,v)]$.

Formalization targets

Goal: Theorem 1 (p.12)

For $\alpha\ge\overline v+1$ and $\beta\ge\max\{0,\alpha-1\}$ there is $\overline C>0$ such that for all $T\ge2$

The constant depends on $w$, the class and the policy, but not on $T$ or $v$.

Milestones, in proof order

1. Well-posedness: an SAP purchase process exists for every horizon.
2. §4.1: the optimum over $\mathcal S$ is attained by an interval $[w^{-1}(\varrho),1]$.
3. Lemma 4: $h(\varrho^*)=\varrho^*$; the drift inequality (23) $(\varrho-\varrho^*)(h(\varrho)-\varrho)\le-(\varrho-\varrho^*)^2/(1+\overline v)$; the derivative $g'=(g-w)\xi$ and the curvature bound (27); the quadratic gap (24) $h(\varrho^*)-h(\varrho)\le C(\varrho-\varrho^*)^2$ with $C$ uniform over $\mathcal V$.
4. The iterates stay in $[0,1]$, and $\mathbb E[R_t\mid\text{history}]=h(\varrho_t)$.
5. The recursion (25) $\delta_{t+1}\le\delta_t\big(1-\frac{2}{1+\overline v}\frac{\alpha}{t+\beta}\big)+\frac{\alpha^2}{(t+\beta)^2}$ for $\delta_t=\mathbb E[(\varrho_t-\varrho^*)^2]$, and Lemma 5, $\delta_t\le\kappa/(t+\beta)$.
6. The regret identity $\Delta_\pi(T,v)=\sum_t\mathbb E[h(\varrho^*)-h(\varrho_t)]$ and $\sum_{t=1}^T(t+\beta)^{-1}\le3\log T$.

Significance

The theorem shows that in the continuum logit model the seller does not need to estimate the preference function: a one-dimensional Robbins–Monro recursion on the observed revenue finds the optimal revenue level, and the loss is logarithmic in the horizon. This is faster than the $\sqrt T$ rates typical of continuum-armed bandits, and the paper's Theorem 2 shows it is optimal. The bound is worst-case over a class of preference functions, which matters when nothing is known about the customers beyond the class.

The result is proved on paper. No part of it is formalized on the platform. The mission adds the platform's first continuum-indexed choice model, a measure-theoretic model of a sequential learning policy whose decisions depend on the full purchase history, and a complete regret analysis for a stochastic approximation policy. The discrete MNL bandit of Agrawal et al. is on the platform as MNLBandit.UCB; it is a related, not a reused, model.

Difficulty

The policy itself is three lines; the difficulty is in the analysis of the map $h$. The obvious route — "$h$ is a contraction, so the iterates converge" — fails: $h$ is not a contraction, and $\varrho\mapsto h(\varrho)$ is flat below $w(0)$ and drops to zero above $w(1)$. The proof instead needs the one-sided drift inequality (23), whose constant must use the upper bound $\overline v$, and the quadratic gap (24), which requires a second-order Taylor expansion of $g(y)=r([y,1],v)$ with a curvature bound (27) that is uniform over the class. The bound (27) needs $v$ differentiable, and the uniformity of $C$ and $\kappa$ over $\mathcal V$ is what turns per-instance bounds into a worst-case one.

The induction in the proof of Lemma 5 multiplies by $1-2\alpha/((1+\overline v)(t+\beta))$, which is negative for small $t$ when $\overline v$ is small; the printed $\kappa=\max\{1+\beta,\alpha(1+\overline v)\}$ does not follow from the printed step there, although the lemma's statement (some $\kappa>0$) remains true.

Formalization scope

Products are reals and purchases live in ℝ ⊕ Unit (Sum.inr () is no-purchase). $w,v:\mathbb R\to\mathbb R$ carry hypotheses only on $[0,1]$ and $(0,1)$. $\mathcal S$ is the measurable subsets of $[0,1]$ (the uncapacitated case $c=1$), and $\varrho^*$ is a supremum (sSup), shown to be a maximum in a milestone. The paper's $\min\{x:w(x)\ge\varrho\}$ is empty for $\varrho>w(1)$, which SAP can reach since $\varrho_1\in[0,1]$ is arbitrary; there $w^{-1}(\varrho):=1$, so the offered assortment $\{1\}$ is a null set. Lean's sInf ∅ = 0 would instead offer $[0,1]$ and break (23). The class has a fixed derivative bound $D$, since Assumption 1(ii)'s supremum over all admissible $v$ is otherwise infinite.

Time is 0-based ($n=t-1$). A horizon-$T$ process is a probability space with measurable purchases $X_0,\dots,X_{T-1}$ whose conditional law given the history is the choice law of the offered assortment, written as an identity of measures on history events. A Lean proof that the SAP iterate is a measurable function of the history exists, so the expectations in the regret are genuine integrals. The goal quantifies over all such processes, and a milestone asserts that one exists, so the goal is not vacuous.

A complete development needs: second-order calculus for parameter integrals $y\mapsto\int_y^1$; the construction of a process from a history-dependent kernel (Ionescu–Tulcea, ProbabilityTheory.Kernel.traj, or an iterated Measure.bind); and conditional expectations given a history σ-algebra. The mean-square recursion and the harmonic-sum bound are reusable for other Robbins–Monro analyses. Contributions to any milestone are welcome, in any order; milestones 2–3 and 6 are independent of the process construction.

Selected references

• Y. Peeters, A. V. den Boer, M. Mandjes, Continuous Assortment Optimization with Logit Choice Probabilities under Incomplete Information, arXiv:1807.06497v4, 2021; Operations Research, 2022. https://arxiv.org/abs/1807.06497
• H. Robbins, S. Monro, A Stochastic Approximation Method, Annals of Mathematical Statistics 22(3), 1951. https://doi.org/10.1214/aoms/1177729586
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic Assortment Optimization with a Multinomial Logit Choice Model and Capacity Constraint, Operations Research 58(6), 2010. https://doi.org/10.1287/opre.1100.0866
• M. Broadie, D. Cicek, A. Zeevi, General Bounds and Finite-Time Improvement for the Kiefer-Wolfowitz Stochastic Approximation Algorithm, Operations Research 59(5), 2011. https://doi.org/10.1287/opre.1110.0970
• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5), 2019. https://doi.org/10.1287/opre.2018.1832

Motivation

Retailers rarely sell one item at a time. A shopper fills a basket with, say, one book, one film and one game, and the decision to buy in one category is linked to the others: if nothing in the store is attractive enough, the shopper leaves without buying anything. Assortment optimization asks which products a retailer should offer so as to maximize expected revenue under a model of customer choice. For single-item purchases under the multinomial logit (MNL) model the answer is classical: some revenue-ordered set is optimal (Talluri and van Ryzin 2004). For basket purchases the natural choice model in the marketing literature is the multivariate MNL (MVMNL) model (Russell and Petersen 2000), and its assortment problem was open.

Jasin, Lyu, Najafi and Zhang (SSRN 3818886; Manufacturing & Service Operations Management, 2023) study this problem. Their first result is for the case without interaction terms across groups. The problem is NP-hard there (by a reduction from PARTITION), but it has a fully polynomial-time approximation scheme (FPTAS), Algorithm U1. This mission formalizes that FPTAS and its analysis.

Setting

There are $J$ groups of products and $I$ products in each group; $(i,j)$ is product $i$ of group $j$. A customer buys a bundle $y=(y_j)_{j=1}^J$, at most one product per group: $y_j=i$ buys product $i$ of group $j$, and $y_j=0$ buys nothing there. An assortment $x\in\{0,1\}^{JI}$ offers product $(i,j)$ iff $x_{i,j}=1$, and a bundle is permissible when it buys only offered products.

Each product has a weight $v_{i,j}=e^{\theta_{i,j}}>0$ and a revenue $r_{i,j}\ge0$. The empty bundle has weight $v_0=e^{\mu_0}>1$, the value of the global outside option. Without interaction terms, a nonempty bundle has weight $\prod_{j:y_j\neq0}v_{y_j,j}$. A bundle is chosen with probability proportional to its weight among the permissible bundles, so the expected total revenue is

Within each group, the products are ordered by non-increasing revenue. A revenue-ordered assortment offers a prefix $\{1,\dots,i(j)\}$ of every group. Write $\gamma_j(x_j)=1+\sum_i v_{i,j}x_{i,j}$, $\Gamma(x)=\prod_j\gamma_j(x_j)$ and $\beta=\max_j(1+\sum_i v_{i,j})$.

Formalization targets

Goal: Theorem 1 (p.14)

There is a universal constant $C$ such that for all $J,I\ge1$, every instance and every $\epsilon\in(0,1)$, Algorithm U1 run with $\epsilon'=\epsilon/(2J)$ returns $\bar x^*$ with

The paper prints $\log^2\beta$. That bound fails as $\beta\to1$, because the algorithm always performs at least one operation. The goal uses $(1+\log\beta)^2$, which agrees with the printed bound up to a factor 4 when $\beta\ge e$.

Milestones, in proof order

1. Lemma 1 and (5): $P_{i,j}(x)=v_{i,j}x_{i,j}\prod_{j'\neq j}\gamma_{j'}/(v_0-1+\Gamma(x))$, hence a closed form of $R(x)$.
2. (7): $R(x)=\sum_j R_j(x)$ with $R_j(x)=\sum_i r_{i,j}v_{i,j}x_{i,j}\big/\big([\tfrac{v_0-1}{\Gamma(x)}+1]\gamma_j(x_j)\big)$.
3. (EC.1) and Lemma 2: with the other groups fixed, $R$ is linear-fractional in $x_j$, and some revenue-ordered assortment is optimal.
4. (EC.5): rounding each $\gamma_j$ up to a power of $1+\epsilon'$ changes each $R_j$ by at most $(1+\epsilon')^{J-1}$ one way and $(1+\epsilon')^J$ the other.
5. Algorithm U1, step 2 and EC.3 feasibility: the output maximizes the rounded objective $\bar R$ over revenue-ordered assortments, and $K=J$ always gives a candidate.
6. (EC.6) and the Taylor step: $R(\bar x^*)\ge R(x)/(1+\epsilon')^{2J}\ge(1-2J\epsilon')R(x)$.
7. The running time: $O(J^3M^2I)$ operations, and $M\le1+4J\log\beta/\epsilon$ (corrected from $O(2J\epsilon^{-1}\log\beta)$).

Significance

The theorem shows that the problem, NP-hard even without interactions, can still be approximated to any accuracy in time polynomial in the input and $1/\epsilon$. Its structural facts carry over to the rest of the paper. Lemma 1 turns a sum over $(I+1)^J$ bundles into a product over groups, and Lemma 2 cuts the search to $(I+1)^J$ revenue-ordered candidates. The rounding-plus-DP scheme is the template for the algorithms with pairwise group interactions and with a capacity constraint (Theorems 2–4).

The result is proved in the paper; nothing here is open mathematics. No machine-checked version is known. The formalization adds three things:

• a reusable basket-choice model with a global outside option, the first multivariate choice model on the platform;
• a fully specified version of Algorithm U1 with an explicit cost model;
• corrected running-time bounds with explicit constants, and an explicit sign condition $r\ge0$ on revenues, which the paper leaves implicit but which Theorem 1 needs.

Difficulty

Without interactions, the revenue still does not separate across groups. The denominator $v_0-1+\Gamma(x)$ couples every group, so the natural idea of optimizing each group's threshold separately fails; the paper's Table 2 shows the loss can be large. A DP that guesses $\Gamma(x^*)$ exactly has exponentially many states. Algorithm U1 rounds every $\gamma_j$ to a power $(1+\epsilon')^{m_j}$, so the DP state becomes the integer exponent $k\in\{0,\dots,JM\}$.

Formally, the hard parts are the following.

• The DP correctness of step 2. One must show that the backward table over integer states, followed by the traceback, attains the maximum of $\bar R$ over revenue-ordered assortments with $\bar\Gamma=(1+\epsilon')^K$. One must also show that every revenue-ordered assortment falls under some enumerated $K\in\{J,\dots,JM\}$.
• The operation count of an explicit program.
• The finite-sum identity of Lemma 1, whose proof the paper omits.

Formalization scope

Groups are Fin J and products Fin I. Assortments are Fin J → Fin I → Bool, and bundles are Fin J → Option (Fin I), with none meaning nothing is bought from that group. The data are $v$, $v_0$ and $r$ themselves ($\theta=\log v$, $\mu_0=\log v_0$). The empty bundle weighs $v_0$, and $R$ is defined by the bundle formula (4), never by its closed forms (5) or (7), which are milestones. Interaction terms $\psi$ are part of the instance, and "no interaction terms" is a hypothesis. The standing assumptions are $J,I\ge1$, $v>0$, $v_0>1$, $r\ge0$, and $r$ non-increasing within each group.

Algorithm U1 is an explicit program algU1 in the unit-cost model CapacitatedAssort.General.Work, reused from the platform. The following operations are charged where they execute: $+,-,\times,/$, comparisons, $\lceil\cdot\rceil_+$, array reads and writes, and loop dispatch. The program evaluates no logarithm or exponential. It finds each rounding exponent by a multiplication loop, indexes DP states by integers, and breaks ties by the first maximizer. The universal constants $C$ and $C_1$ are quantified before $J$, $I$, the instance and $\epsilon$. This rules out a trivial reading in which an existential "some algorithm" could enumerate all $2^{JI}$ assortments.

Contributions are welcome on any milestone. The bundle-sum factorization (Lemma 1) and the DP-correctness lemma are the largest pieces. The model module is reusable for other basket-choice results.

Selected references

• S. Jasin, C. Lyu, S. Najafi, H. Zhang, Assortment Optimization with Multi-Item Basket Purchase under Multivariate MNL Model, SSRN 3818886 (2023); Manufacturing & Service Operations Management, 2023. https://ssrn.com/abstract=3818886, https://doi.org/10.1287/msom.2021.0526
• G. J. Russell, A. Petersen, Analysis of cross category dependence in market basket selection, Journal of Retailing 76(3), 2000. https://doi.org/10.1016/S0022-4359(00)00030-0
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147

Motivation

The Nested Logit model is one of the most widely used discrete choice models in revenue management. It captures substitution that the Multinomial Logit model cannot: products are grouped into nests, a customer first chooses a nest and then a product in it (Davis, Gallego, Topaloglu, 2014; Gallego, Topaloglu, 2014). A retailer that decides which products to offer under a limit on shelf space or budget faces capacitated assortment optimization. Earlier constant-factor approximations depend on restricted forms of the model, such as dissimilarity parameters in $[0,1]$ or no nest-level no-purchase option, and Segev (SSRN #3553264) removes those restrictions with an approximation scheme.

Setting

There are $n$ products partitioned into nests $N_1,\dots,N_M$. Product $i$ has a price $r_i>0$, a preference weight $w_i>0$ and a cost $c_i$. Nest $m$ has a dissimilarity parameter $\gamma_m$ and a no-purchase weight $w_{0m}$, and $w_0$ is the outside no-purchase weight. An assortment is $S=(S_1,\dots,S_M)$ with $S_m\subseteq N_m$. For $T\subseteq N_m$ write $w_+(T)=\mathbb I[T\ne\emptyset](w_{0m}+w(T))$ and $\mathcal R_m(T)=\sum_{i\in T}r_iw_i/w_+(T)$. The expected revenue is

An assortment is $\mathcal C$-feasible when $\sum_m c(S_m)\le\mathcal C$. The objective is a $\mathcal C$-feasible assortment of maximum revenue.

Formalization targets

Goal

The goal is Theorem 1.1, stated about one explicit instrumented program fptas. There is a universal $K$ such that, for every $\epsilon>0$: the program returns an assortment whenever a $\mathcal C$-feasible one exists; every assortment $\tilde S$ it returns is $\mathcal C$-feasible; and

and on rational instances it uses at most

operations, with $\gamma^+=\max\{1,\gamma_1,\dots,\gamma_M\}$ and $\gamma^-=\min\{1,\gamma_1,\dots,\gamma_M\}$.

Milestones

In proof order: the representation (1); Lemma 2.1 on the dual; the single-nest results, Lemmas 4.1–4.3 and Theorem 3.1; the ranges of §3.3; the recursion (4) and the final selection, as properties of the program; Lemmas 3.3, 3.5, 3.6, 3.4 and 3.2; and the running time of §3.4.

Significance

The theorem shows that the revenue of the capacitated problem can be approached to any accuracy by combinatorial means, in the full generality of the model: parameters $\gamma_m>1$, nest-level no-purchase weights, and arbitrary costs. It is the first fully polynomial-time approximation scheme for this problem when $\gamma^+/\gamma^-$ is polynomial in the input size, a dependence the paper explains in §5.

The result is proved on paper and not machine-checked. This mission adds the first approximation scheme for the Nested Logit model on the platform, an instrumented dual dynamic program with a rounding-path analysis, and a formal count of its operations. It also records three defects of the printed construction with their counterexamples: the grids stop at the range of a single nest, the grid for $\rho$ starts too high, and the single-nest search can return the empty set. The headline theorem survives with minimal changes to the algorithm, at the cost of $\log M$ and constant factors. The Operations Research version was not consulted, so it is unknown whether it already contains these repairs.

Difficulty

The obvious dynamic program, tracking the sums $\omega$ and $\rho$ across nests, fails in two places. First, the single-nest problem with exact targets is NP-hard, so the targets must be relaxed to a neighbourhood; the difficulty is that $w_+(T)^{\gamma}$ and $\mathcal R_k(T)w_+(T)^{\gamma}$ are not additive over products, and their sensitivity changes direction at $\gamma=1$. Secondly, the grids are not closed under subtraction, so the recursion cannot split $\omega$ exactly into $\omega_k$ and $\omega-\omega_k$. The recursion splits it superadditively and $\rho$ subadditively, and a rounded path must be shown admissible at every nest, with distortion only $(1+\xi_\omega)^{M}$ and $(1-\xi_\rho)^{M}$ over $M$ levels. Rounding one nest at a time, the natural first idea, accumulates errors in the wrong direction unless the factor $(1+\xi_\omega)^{M-k}$ decreases along the path.

Formalization scope

Products are Fin n, the partition is a map nest : Fin n → Fin M, and an assortment is a Finset (Fin n). Standing assumptions are $r_i,w_i>0$, $M\ge1$, nonempty nests, $\gamma_m>0$, and $w_0,w_{0m}\ge0$; costs and $\mathcal C$ are real of any sign. $\hat\epsilon=\min(\epsilon,1)$ enters the parameters, and $\epsilon$ the guarantees.

Without the program the accuracy claim is trivial, because the optimum itself exists. So the goal is about fptas, in the cost monad Work of CapacitatedAssort.General: it uses unit-cost arithmetic, comparisons, $\lfloor\cdot\rfloor$, $\lceil\cdot\rceil$, Real.rpow, Real.log and array accesses, each charged where it executes, and it enumerates no subset of products. This is the accounting of §3.4 and §4.2 of the paper, and exact powers are irrational for rational data, so no bit model is claimed for them.

The neighbourhood of (3) is stated multiplied out, with $\emptyset$ only at $\omega_k=\rho_k=0$. The grids are corrected as described in the docstrings of Pomega and Lrho, the table of the single-nest step distinguishes nonempty subsets, and each difference is declared on its item.

A complete development needs estimates for real powers on both sides of $\gamma=1$, correctness and cost lemmas for the imperative tables, and bit-length bounds for the logarithmic factors (logs_le_inputSize). The cost lemmas for tabulate and for nested loops are reusable. Contributions to any milestone are welcome, and the analysis of the single-nest step can be done independently of the rest.

Selected references

• D. Segev, Approximation Schemes for Capacity-Constrained Assortment Optimization under the Nested Logit Model, SSRN #3553264, March 2020. https://ssrn.com/abstract=3553264 (published as a Technical Note in Operations Research, 2022, https://doi.org/10.1287/opre.2022.2336; the numbering of this mission follows the SSRN version).
• J. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014. https://doi.org/10.1287/opre.2014.1256
• G. Gallego, H. Topaloglu, Constrained assortment optimization for the nested logit model, Management Science 60(10), 2014. https://doi.org/10.1287/mnsc.2014.1931

Why pricing along one vector

Charging every customer segment its own optimal prices is the most a seller can extract with a posted price per segment, and solving each segment's problem is often easy. Finding one optimal non-personalized price vector is harder, because aggregate demand may be much more complex than the segments' demands, so single-factor heuristics are used instead. A natural question is how much is lost.

For one product, Bergemann, Castro and Weintraub bound the ratio of personalized to uniform profit by two when each type's profit is concave and demand is positive on a common compact set; Malueg and Snyder bound it by the number of types under milder conditions; and Elmachtoub, Gupta and Hamilton give bounds in terms of summary statistics of the demand distribution. For several products, Berbeglia and Joret analyse uniform pricing in the special case of envy-free pricing. Gallego and Berbeglia state the first tight bound of this kind for general multi-product demand, against the personalized optimum rather than the non-personalized one.

The pricing model

A firm sells a finite nonempty set $N$ of products to customer types $t\in T$, distributed according to a probability measure $\mu$. In the paper $T$ is finite with weights $\theta_j>0$; its remark on p.5 extends the result to continuous types. Write $d_{t,i}(p)\ge0$ for the demand of type $t$ for product $i$ at the price vector $p\ge0$. The type profit is $R_t(p)=\sum_{i\in N}p_id_{t,i}(p)$ and the aggregate profit is $R(p)=\int R_t(p)\,d\mu(t)$.

Let $\bar p_t$ be an optimal price vector of type $t$ (Assumption A0: optimal prices exist and are positive and finite). The personalized profit is $\bar{\mathcal R}=\int R_t(\bar p_t)\,d\mu(t)$. Pricing along a positive vector $f$ earns $\mathcal R^f=\sup_{q>0}R(qf)$; $f=e$ is uniform pricing. For $q\ge0$, the filtered demand $G(q)$ is the $f$-weighted demand at the personalized optima, keeping the pairs $(i,t)$ with $q\le\bar p_{t,i}/f_i$, and $H(q)=\int\sum_{i\in N}f_id_{t,i}(qf)\,d\mu(t)$. Assumption A1 is $G(q)\le H(q)$ for all $q\ge0$. Finally, $q_{\min}$ and $q_{\max}$ are the infimum and supremum of the ratios $\bar p_{t,i}/f_i$.

Formalization targets

The bound

for every finite nonempty product set, every probability space of types, every positive $f$ and every selection $\bar p$ of optimal prices, under A0 and A1, with $q_{\min}>0$ and integrable demands.

Exact tightness

For every $\rho>1$ there is an instance with one product, $f=1$, $q_{\min}=1$, $q_{\max}=\rho$, $\mathcal R^f>0$ and

Best constant over finite instances

For every $\rho>1$ and $c<1+\ln\rho$ there is an instance with one product, $f=1$, finitely many types, $q_{\min}=1$, $q_{\max}=\rho$, $\mathcal R^f>0$ and $\bar{\mathcal R}>c\,\mathcal R^f$.

All three are clauses of the goal theorem, SingleFactorPricing.LogBound.theorem_1. The milestones are the displayed steps of the paper's proof (the integral forms of the profits, the split at $q_{\min}$, the identity $R(qf)=qH(q)$, the pointwise bound on $qG(q)$) and its tight instance.

What the result gives

Since $\mathcal R^f\le\mathcal R^*\le\bar{\mathcal R}$, where $\mathcal R^*$ is the optimal non-personalized profit, one inequality yields a guarantee for single-factor heuristics against non-personalized pricing and a bound on the value of personalization. The constant depends only on the spread of the optimal prices measured against $f$, not on the number of products or types. For example, $\bar p_{ij}\in[h,7.38h]$ gives $\bar{\mathcal R}\le3\mathcal R^e$. The paper also gives sufficient conditions for A1 that hold in linear, multinomial logit and envy-free models, and uses the bound to compare linear with non-linear pricing.

The result is proved in the paper. This mission adds a machine-checked version: the bound over a general type space, where the paper only remarks that the proof carries over; both meanings of tightness, of which the paper states neither separately; and an explicit probability law for the instance. No formalization of this bound for general demand is known. The platform has narrower statements of the same shape: RevenueOrdered.UDPmin.uniform_pricing_log_ratio_bound for envy-free pricing and ValuePersPricing.Deviation.theorem_2 for one product.

Where the difficulty lies

The obvious comparison fails. Personalized optimal prices need not lie on a single ray $\{qf\}$, so no single $q$ can be compared with them, and A1 compares two sums at the same $q$ rather than two profits. The bound therefore has no term-by-term proof, and the factor $\beta$ is not visible from any one type.

Three points need care in Lean. Over a general type space, $\bar{\mathcal R}$ involves an exchange of integrals for functions that are only assumed integrable in the type. The second line of the printed chain contains $\int R(qf)\,dq/q$, and nothing makes $q\mapsto R(qf)$ measurable. And "tight" cannot mean equality with finitely many types: when $q_{\min}<q_{\max}$ and $\mathcal R^f>0$, $G$ is a step function and equality is impossible, so the exact statement and the finite statement are independent, and the instance for each needs its own computation.

Formalization scope

The type space is T with a probability measure μ, and demand is d : T → (N → ℝ) → N → ℝ with N a nonempty Fintype. Non-negativity and optimality are required for $p\ge0$ only. KallMayerSLP.ICC.discreteLaw θ id, a published finite law, recovers the paper's finite model, and regularity is then automatic. $q_{\min}$, $q_{\max}$ and $\mathcal R^f$ are fixed by IsGLB, IsLUB and IsLUB, so a real ⨆ is not used; $\mathcal R^f$ need not be attained. The filter uses the paper's non-strict inequality. The optimality of $\bar p$ stays in AssumptionA0 although the bound does not use it, so that $\bar{\mathcal R}$ is the personalized optimum and not the profit of arbitrary prices. There is no cost vector (footnote 1 of the paper).

Trivial tightness is excluded: the clauses assert $\mathcal R^f>0$, and LogBoundInstance fixes $q_{\min}=1$ and $q_{\max}=\rho$ as the true infimum and supremum of the ratios, not bounds on them.

A complete development needs integrals over the product of the type space and $(0,\infty)$, the logarithmic integral, the moments and tail of the truncated law tailLaw, and an explicit family of finite instances for the last clause. The definitions are general enough to reuse for the other results of the paper. Proofs of the milestones and of the goal are welcome, as are the omitted results (Corollary 1, Proposition 1, Theorem 2), which would be separate statements.

Selected references

• G. Gallego, G. Berbeglia, Bounds and Heuristics for Multi-Product Personalized Pricing, arXiv preprint, 2021. https://arxiv.org/abs/2102.03038
• G. Berbeglia, G. Joret, Assortment optimisation under a general discrete choice model: A tight analysis of revenue-ordered assortments, Algorithmica 82(4), 2020. https://arxiv.org/abs/1606.01371
• D. Bergemann, F. Castro, G. Y. Weintraub, Uniform pricing versus third-degree price discrimination, Cowles Foundation Discussion Paper, 2020. https://cowles.yale.edu/sites/default/files/2022-08/d2213-r.pdf
• A. N. Elmachtoub, V. Gupta, M. Hamilton, The value of personalized pricing, Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3821
• D. A. Malueg, C. M. Snyder, Bounding the relative profitability of price discrimination, International Journal of Industrial Organization 24(5), 2006. https://doi.org/10.1016/j.ijindorg.2005.11.006