Proposition 3 — rationing is optimal if $\bar U\ge U_c$ ; otherwise serve the whole market at the low price

Proved

LiuVanRyzin.optimal_stocking

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1rationingrevenue-managementstrategic-customers

A monopolist sells to $N>0$ customers whose valuations are uniform on $[0,\bar U]$ , at prices $p_1$ in period 1 and $p_2$ in period 2 with $\alpha<p_2<p_1$ , where $\alpha$ is the unit cost. Customers have power utility $u(x)=x^\gamma$ , $0<\gamma<1$ . Let $v^0>p_1$ be the solution of the first-order condition (7),

\left(\frac{v^0-p_1}{v^0-p_2}\right)^\gamma\left(1+\frac{\gamma(p_1-p_2)}{v^0-p_1}\right)=\frac{p_1-\alpha}{p_2-\alpha},

and let

U_c=\frac{(p_2+\gamma(p_1-\alpha))v^0-p_2(p_1+\gamma(p_2-\alpha))}{v^0-p_1+\gamma(p_1-p_2)}.

Let $\Pi(v)$ be the segmented-market profit (6) and $\Pi^{NS}=(p_2-\alpha)\frac{N}{\bar U}(\bar U-p_2)$ the profit of serving the entire market at the low price. Then:

If $\bar U\ge U_c$ , inducing segmentation by rationing is optimal: $v^0\in[p_1,\bar U]$ , $v^0$ maximizes $\Pi$ over $[p_1,\bar U]$ , and $\Pi(v^0)\ge\Pi^{NS}$ . The optimal solution is $v^*=v^0$ , fill rate $q^*=q^0=((v^0-p_1)/(v^0-p_2))^\gamma$ and stocking quantity $C^*=C^0=\frac N{\bar U}(\bar U-v^0+(v^0-p_2)q^0)$ .
If $\bar U<U_c$ , serving the entire market at the low price is optimal: $\Pi(v)\le\Pi^{NS}$ for every $v\in[p_1,\bar U]$ . The optimal solution is $v^*=\bar U$ , $q^*=1$ , $C^*=\frac N{\bar U}(\bar U-p_2)$ .

Here "optimal" is the paper's: the firm's optimal profit is the larger of the segmented optimum $\Pi^0=\max_{p_1\le v\le\bar U}\Pi(v)$ and $\Pi^{NS}$ . The theorem says rationing pays exactly when there are enough high-value customers.

Formalization Note The paper uses $0\le p_2<\bar U$ without stating it: the uniform law gives $N\bar F(p_2)=\frac N{\bar U}(\bar U-p_2)$ only for $p_2\in[0,\bar U]$ , and it makes $\bar U>0$ . The optimal $q^0$ and $C^0$ are fillRate and capacity at $v^0$ (definition module), so they are not restated as conjuncts.

Preamble

import Mathlib
import Definitions.Def_LiuVanRyzin_PowerModel

Formal statement

namespace LiuVanRyzin

/-- Proposition 3 (Liu–van Ryzin 2008, p. 1122). Let `v⁰` be the root of (7) and `U_c` as in
(8). If `Ū ≥ U_c`, segmentation at `v⁰` is optimal: `v⁰` maximizes `Π` on `[p₁, Ū]` and
`Π(v⁰) ≥ Π^NS`. Otherwise serving the entire market at the low price is optimal:
`Π(v) ≤ Π^NS` for every `v ∈ [p₁, Ū]`. -/
theorem optimal_stocking (N Ubar p₁ p₂ α γ v₀ : ℝ) (hN : 0 < N) (hα : α < p₂)
    (hp : p₂ < p₁) (hγ0 : 0 < γ) (hγ1 : γ < 1) (hp₂ : 0 ≤ p₂) (hpU : p₂ < Ubar)
    (hv₀ : p₁ < v₀) (hroot : focLHS p₁ p₂ α γ v₀ = 0) :
    (criticalU p₁ p₂ α γ v₀ ≤ Ubar →
        v₀ ∈ Set.Icc p₁ Ubar ∧
          IsMaxOn (segProfit N Ubar p₁ p₂ α γ) (Set.Icc p₁ Ubar) v₀ ∧
          lowPriceProfit N Ubar p₂ α ≤ segProfit N Ubar p₁ p₂ α γ v₀) ∧
      (Ubar < criticalU p₁ p₂ α γ v₀ →
        ∀ v ∈ Set.Icc p₁ Ubar, segProfit N Ubar p₁ p₂ α γ v ≤ lowPriceProfit N Ubar p₂ α) := by sorry

end LiuVanRyzin

Source

Liu, van Ryzin, Strategic Capacity Rationing to Induce Early Purchases, Management Science 54(6):1115–1131 (2008), p. 1122, Proposition 3 (with Eqs. (6)–(8); optimality as max(Π⁰, Π^NS), p. 1121)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

This statement concerns seven real numbers $N, \bar U, p_1, p_2, \alpha, \gamma, v_0 \in \mathbb{R}$ . It uses four functions imported from the module Definitions.Def_LiuVanRyzin_PowerModel. Their definitions are not shown in the code provided, so this read-back treats them only by name and by the arguments they take:

$F(p_1, p_2, \alpha, \gamma, v)$ — focLHS, a real-valued expression in $p_1, p_2, \alpha, \gamma$ and a point $v$ ;
$U_c(p_1, p_2, \alpha, \gamma, v)$ — criticalU, a real-valued expression in the same arguments;
$\Pi_{\mathrm{seg}}(v) = \Pi_{\mathrm{seg}}^{N, \bar U, p_1, p_2, \alpha, \gamma}(v)$ — segProfit, a real function of $v$ that depends on all six parameters;
$\Pi_{\mathrm{low}} = \Pi_{\mathrm{low}}(N, \bar U, p_2, \alpha)$ — lowPriceProfit, a real number that depends only on $N, \bar U, p_2, \alpha$ (it does not take $p_1$ or $\gamma$ ).

The theorem assumes the following hypotheses:

0 < N, \qquad \alpha < p_2, \qquad 0 \le p_2 < p_1, \qquad 0 < \gamma < 1, \qquad p_2 < \bar U, \qquad p_1 < v_0, \qquad F(p_1, p_2, \alpha, \gamma, v_0) = 0.

There is no lower bound on $\alpha$ , so it may be negative. There is also no hypothesis relating $\bar U$ to $p_1$ or to $v_0$ .

Under these hypotheses, the theorem asserts both of the following. Write $U_c := U_c(p_1, p_2, \alpha, \gamma, v_0)$ .

If $U_c \le \bar U$ , then all three of these hold:
- $v_0 \in [p_1, \bar U]$ . Since $p_1 < v_0$ is assumed, the new content is $v_0 \le \bar U$ .
- $v_0$ is a maximizer of $\Pi_{\mathrm{seg}}$ on the closed interval $[p_1, \bar U]$ :

\Pi_{\mathrm{seg}}(v) \le \Pi_{\mathrm{seg}}(v_0) \quad \text{for every } v \text{ with } p_1 \le v \le \bar U.

$\Pi_{\mathrm{low}}(N, \bar U, p_2, \alpha) \le \Pi_{\mathrm{seg}}(v_0)$ .

If $\bar U < U_c$ , then

\Pi_{\mathrm{seg}}(v) \le \Pi_{\mathrm{low}}(N, \bar U, p_2, \alpha) \quad \text{for every } v \text{ with } p_1 \le v \le \bar U.

The two cases are complementary, since exactly one of $U_c \le \bar U$ and $\bar U < U_c$ holds. The theorem does not assert that a $v_0$ satisfying $F = 0$ exists or is unique. It is a statement about any $v_0 > p_1$ that happens to be a root. Because $F$ is not visible here, this read-back cannot determine whether the root hypothesis can be satisfied together with the other hypotheses. If it cannot, the theorem is vacuous.

Degenerate cases. The hypotheses force $N > 0$ , $\gamma \in (0,1)$ and $0 \le p_2 < p_1 < v_0$ , so none of these can be zero or collapse. However, $\bar U$ is only required to exceed $p_2$ , which permits $p_2 < \bar U < p_1$ or $p_1 \le \bar U < v_0$ .

When $\bar U < p_1$ , the interval $[p_1, \bar U]$ is empty. Part 2 then holds vacuously, as does the maximizer clause of part 1. But the membership clause $v_0 \in [p_1, \bar U]$ would be false. So in that situation the theorem in effect asserts that $U_c \le \bar U$ cannot occur.
More generally, part 1 asserts, as a conclusion rather than an assumption, that $U_c \le \bar U$ implies $v_0 \le \bar U$ .
When $\bar U = p_1$ , the interval is the single point $\{p_1\}$ . Part 2 then compares only $\Pi_{\mathrm{seg}}(p_1)$ with $\Pi_{\mathrm{low}}$ , and part 1 again requires $v_0 \le p_1$ , which contradicts $p_1 < v_0$ .
No division, natural-number subtraction, integral or supremum appears in the statement itself. Any such operations, and any default "junk" values they return (for instance a division by zero yielding $0$ ), would sit inside the unseen definitions of $F$ , $U_c$ , $\Pi_{\mathrm{seg}}$ and $\Pi_{\mathrm{low}}$ . This read-back cannot say what those definitions produce at such arguments.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proposition 3 — rationing is optimal if Uˉ≥Uc\bar U\ge U_cUˉ≥Uc​; otherwise serve the whole market at the low price

Proposition 3 — rationing is optimal if $\bar U\ge U_c$ ; otherwise serve the whole market at the low price