The OR Formalization Drive

Motivation

Many large convex programs have the form "minimize a strictly convex function $f$ subject to linear equations $Ax=b$". Examples are entropy maximization under moment constraints, the estimation of a matrix with prescribed row and column sums (the matrix-scaling or RAS problem of transportation and input–output analysis), and least-norm solutions of linear systems. When $A$ is large and sparse, methods that touch one equation at a time are attractive: each step needs only one row of $A$.

L. M. Bregman's 1967 paper (doi:10.1016/0041-5553(67)90040-7) introduced such a method. §1 defines a "relaxation" for finding a common point of closed convex sets $A_i$, in which each step replaces the current point by its $D$-projection onto one set: the minimizer of a distance-like function $D(\cdot,y)$ over that set. §2 chooses $D$ from the objective $f$ itself, $D(x,y)=f(x)-f(y)-(g(y),x-y)$ with $g$ the gradient of $f$; this function is now called the Bregman divergence. Theorem 3 of the paper, the target of this mission, shows that with this choice the relaxation does more than find a feasible point: started at a suitable point, its limit minimizes $f$ over the feasible set. The resulting row-action methods underlie later work on entropy optimization and matrix balancing (Censor and Zenios, Parallel Optimization, 1997) and the Bregman-projection techniques of modern optimization.

Setting

Work in the Euclidean space $E^p$ with inner product $(\cdot,\cdot)$. Let $S\subset E^p$ be a convex set with closure $\bar S$ and interior $\operatorname{int}S$. Let $f$ be strictly convex and continuously differentiable over $S$, with gradient $g(x)$ at $x\in S$, and continuous over $\bar S$. Let $A$ be an $m\times p$ matrix with nonzero rows $A_1,\dots,A_m$ and $b\in E^m$. The problem (2.1)–(2.3) is

$$\text{minimize } f(x)\quad\text{subject to}\quad Ax=b,\ x\in\bar S,$$

with feasible set $R=\{x\in E^p\mid Ax=b,\ x\in\bar S\}$, assumed nonempty. A point of $R$ minimizing $f$ over $R$ is a solution.

The function (1.4) is

$$D(x,y)=f(x)-f(y)-\bigl(g(y),x-y\bigr),$$

and $A_i$ also denotes the hyperplane $\{x\mid (A_i,x)=b_i\}$. The paper assumes that $D$ satisfies its conditions I–VI of §1 with respect to these hyperplanes; among them, condition II provides, for every $y\in S$, a $D$-projection $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$. It also assumes condition (2): if $y^n\in S$ and $y^n\to y^*\in\bar S$, then $D(y^*,y^n)\to 0$.

A relaxation sequence with control $(i_n)_{n\ge0}$ starts at $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$. The control is any sequence of row indices. Finally,

$$Z=\{x\in S\mid g(x)=uA=\textstyle\sum_i u_iA_i\ \text{for some } u\in E^m\}$$

is the set of points of $S$ at which the gradient lies in the row space of $A$.

Formalization targets

Goal: Theorem 3

Assume that the $D$-projection of every point of $\operatorname{int}S$ onto every $A_i$ lies in $\operatorname{int}S$. For every control and every relaxation sequence with $x^0\in Z\cap\operatorname{int}S$ that converges to a point $x^*\in R$,

$$f(x^*)\le f(y)\qquad\text{for every } y\in R .$$

Convergence of the sequence is a hypothesis; the theorem says what the limit is, whichever control produced it.

Milestones

1. Lemma 3. If $y^*\in R\cap\bar Z$, then $y^*$ is a solution of (2.1)–(2.3).
2. (2.7)–(2.8). For $x\in\operatorname{int}S$ there is $\lambda\in\mathbb R$ with $g(P_ix)=g(x)+\lambda A_i$ and $(A_i,P_ix)=b_i$.
3. Invariance of $Z$. $P_i$ maps $Z\cap\operatorname{int}S$ into $Z\cap\operatorname{int}S$.

An additional item states Note 2: the point and the multiplier in (2.7)–(2.8) are unique.

Significance

Theorem 3 converts a feasibility algorithm into an optimization algorithm for equality-constrained convex programs. Each step solves a one-dimensional problem (the multiplier $\lambda$ of a single equation), so the method scales to systems with very many equations, and with the controls of Theorems 1–2 of the same paper it gives a complete algorithm. Specializations include iterative proportional fitting for entropy objectives and Kaczmarz-type projections for $f(x)=\tfrac12\|x\|^2$.

The theorem and its proof are classical and have been reproved many times, but no machine-checked proof is known to exist. A formalization produces a verified bridge between three standard pieces of convex analysis: first-order optimality on an affine set, the supporting-hyperplane inequality for a differentiable convex function extended to the closure of its domain, and the passage of a Lagrange condition to a limit. Each is reusable in other row-action and mirror-descent developments.

Difficulty

The obvious argument says: the limit is feasible, and the gradient at every iterate lies in the row space of $A$, so the limit satisfies the Karush–Kuhn–Tucker conditions. Two steps of this argument fail as stated. First, the gradient is only known on $S$, the limit may lie on the boundary of $S$ (or outside $S$, in $\bar S$), and $g$ need not extend continuously there, so the multipliers $u^n$ need not converge and no Lagrange condition holds at the limit. Lemma 3 must therefore reach optimality without a gradient at $y^*$. Second, the Lagrange condition (2.7) at an iterate requires the projection to be an interior minimizer, which is why the theorem carries the hypothesis that $P_i$ preserves $\operatorname{int}S$; on the boundary of $S$ a minimizer over $A_i\cap S$ need not satisfy (2.7).

Formalization scope

The space is EuclideanSpace ℝ (Fin p), rows are vectors a i, and $(A_i,x)$ is the real inner product. The gradient $g$ is explicit data tied to $f$ by HasGradientWithinAt f (g x) S x for $x\in S$ and continuous on $S$; $S$ is not assumed open, and Mathlib's gradient is not used. The relevant explicit choices are:

• The $D$-projection is a fixed map $P$; condition II says $P_iy$ minimizes $D(\cdot,y)$ over $A_i\cap S$, and condition III is stated for that map.
• Condition IV is assumed in its one-sided directional form (implied by the paper's), so theorems under it are at least as strong as the paper's.
• "Compact" in conditions V and VI is sequential compactness. Condition V is assumed for the points of $R\cap S$.
• Condition (2) is assumed for limits $y^*\in\bar S$; the page prints $y^*\in S$, but its use at a feasible point needs $\bar S$.
• Translation slips are corrected in the statements and recorded: condition II's "$D(z,x)$" and "$i\in T$", (2.7)'s "$g(x^{n-1})$" (read $g(x^{n+1})$), and "Theorems 1 − 3" (read Theorems 1–2).
• The control is an arbitrary sequence of indices in $\{0,\dots,m-1\}$; λ is named lam.
• Note 2 is stated for candidate points $y,z\in S$, where $g$ is meaningful.

The goal does not conclude that the relaxation converges; a statement asserting convergence is a different, unproved theorem. Equally, it must not be weakened to a fixed control, to an open $S$, or to a limit assumed to lie in $Z$: any of these would trivialize the passage to the limit that the theorem is about.

A complete development needs the first-order condition for a local minimum on an affine hyperplane, the gradient inequality $f(x)\ge f(y)+(g(y),x-y)$ for $x\in\bar S$, $y\in S$, and an induction along the relaxation sequence. Proofs of the milestones and of Note 2 are welcome independently.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Comput. Math. Math. Phys. 7(3) (1967) 200–217. doi:10.1016/0041-5553(67)90040-7
• Y. Censor, S. A. Zenios, Parallel Optimization: Theory, Algorithms, and Applications, Oxford University Press, 1997. doi:10.1093/oso/9780195100624.001.0001
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, J. Optim. Theory Appl. 34 (1981) 321–353. doi:10.1007/BF00934676

Motivation

A supplier that sells through independent retailers usually loses part of the profit an integrated firm would earn: each retailer orders to maximize its own profit, not the channel's. Supply chain coordination asks which contracts make the decentralized choices coincide with the integrated optimum. Cachon and Lariviere study revenue-sharing contracts, under which a retailer pays a per-unit wholesale price and keeps only a fraction $\phi$ of its revenue, the rest going to the supplier. The contracts were made prominent by the video rental industry around 1998, where studios lowered tape prices in exchange for a share of rental income.

With a single retailer, revenue sharing at the wholesale price $\phi c$ coordinates the channel and splits its profit in the proportion $\phi$. This mission formalizes the extension in Section 3.2 of the paper to competing retailers: several locations whose revenues depend on each other's stock, so that one retailer's order lowers the others' revenue. Competition creates externalities the single-retailer argument does not have, and the question is whether revenue sharing still coordinates, and at what prices. Section 4.1.2 then works out a Cournot example in closed form, measuring how far the supplier's own optimal wholesale price leaves the channel from the integrated profit.

The source is the authors' working paper of June 2000; the published version (Management Science 51(1), 2005) renumbers and revises the results. The working paper numbers no theorem, so results are cited by section, displayed equation and page.

Setting

A single supplier sells one product through $n$ locations $i = 1,\dots,n$, each run by an independent retailer. A stocking profile is $\bar q = (q_1,\dots,q_n)$, and the revenue at location $i$ is $R_i(\bar q)$, which may depend on every location's quantity. The system revenue is $R(\bar q) = \sum_i R_i(\bar q)$, every unit costs the supplier $c > 0$, and the integrated system profit is

$$\Pi(\bar q) = R(\bar q) - c\sum_{i=1}^n q_i .$$

Write $R_j^i(\bar q) = \partial R_j(\bar q)/\partial q_i$: the superscript is the variable differentiated, the subscript the revenue function. The paper assumes that each $R_i$ is continuous, that $\partial^2 R_i/\partial q_i\partial q_j \le 0$ for $j \ne i$ (locations are substitutes), and that $R_i$ is unimodal in $q_i$. The system-optimal profile $\bar q^I$ has positive entries and solves the first-order system

$$R_i^i(\bar q^I) + \sum_{j\ne i} R_j^i(\bar q^I) = c, \qquad i = 1,\dots,n. \tag{6}$$

Under a revenue-sharing contract $(\phi, w_i)$ retailer $i$ earns $\pi_{r_i}(\bar q,\phi,\bar w) = \phi R_i(\bar q) - w_i q_i$ and the supplier earns $\pi_s(\bar q,\phi,\bar w) = \sum_i\big((1-\phi)R_i(\bar q) + w_i q_i\big) - c\sum_i q_i$; the wholesale-price contract is $\phi = 1$, with profits written $\pi_{r_i}(\bar q,\bar w)$ and $\pi_s(\bar q,\bar w)$. A Nash equilibrium in order quantities is a profile $\bar q \ge 0$ from which no retailer gains by changing its own quantity to any $x \ge 0$. The coordinating wholesale prices are

$$w_i^I = c - \sum_{j\ne i} R_j^i(\bar q^I).$$

The Cournot example (7) is $R_i(\bar q) = q_i\big(1 - q_i - \beta\sum_{j\ne i} q_j\big)$ with $0 \le \beta < 1$.

Formalization targets

Goal: revenue sharing supports $\bar q^I$ (Sec. 3.2, p. 14)

For $\phi\in[0,1]$ and $w_i(\phi) = \phi w_i^I$:

$$\bar q^I \text{ is a Nash equilibrium},\quad \pi_{r_i}(\bar q^I,\phi,\phi\bar w^I) = \phi\,\pi_{r_i}(\bar q^I,\bar w^I),\quad \pi_s(\bar q^I,\phi,\phi\bar w^I) = (1-\phi)\Pi(\bar q^I) + \phi\,\pi_s(\bar q^I,\bar w^I).$$

Wholesale-price contracts (Sec. 3.2, pp. 13–14)

An interior equilibrium satisfies $R_i^i(\bar q^N) = w_i$ (Eq. (8)), so marginal-cost pricing does not support $\bar q^I$ when a location imposes a negative externality; the prices $\bar w^I$ make $\bar q^I$ an equilibrium; $w_i^I \ge c$ when cross-effects are nonpositive; and $\bar w^I$ supports exactly the split $\pi_s(\bar q^I,\bar w^I) = \sum_i q_i^I\sum_{j\ne i}(-R_j^i(\bar q^I))$.

Revenue sharing (Sec. 3.2, p. 14)

An interior equilibrium satisfies $\phi R_i^i(\bar q^N) = w_i(\phi)$; the two profit identities hold for every $\phi$; and $\pi_{r_i}(\bar q^I,\bar w^I) \ge 0$.

The Cournot example (Sec. 4.1.2, pp. 19–20)

At a common price $w<1$ the unique equilibrium is $q_i^N = (1-w)/(2+\beta(n-1))$; the integrated optimum is $q_i^I = (1-c)/(2+2\beta(n-1))$; the coordinating price $w^I = c + \beta(n-1)(1-c)/(2+2\beta(n-1))$ increases in $\beta$ and $n$; the supplier's optimal price is $w^* = (1+c)/2$; and the efficiency at $w^*$ is

$$\frac{\Pi(\bar q^N(w^*))}{\Pi(\bar q^I)} = 1 - \frac{1}{(2+\beta(n-1))^2}.$$

Significance

The goal shows that the single-retailer coordination result survives competition, with one change: the coordinating price must charge each retailer for the externality it imposes on the others, so it depends on every location's revenue function, and $w^I_i$ exceeds the production cost. The supplier's profit then moves along a line between what wholesale prices alone give her and the whole system profit, which is how revenue sharing provides a profit split that linear prices cannot. The Cournot results make the comparison quantitative: when retailers compete intensely, the supplier's own optimal wholesale price already achieves most of the integrated profit, so revenue sharing, which has administrative costs, is less attractive.

No machine-checked proof of these results is known. The mission produces a reusable formal description of an $n$-player quantity game under per-retailer linear contracts, equilibrium conditions for it, and a fully worked Cournot instance, including a uniqueness claim for equilibria among all (not only symmetric) profiles.

Difficulty

The equilibrium claims are global: a retailer must not gain from any nonnegative deviation, not only from small ones. A first-order condition at $\bar q^I$ does not give this by itself. The page assumes $R_i$ unimodal in $q_i$, but unimodality does not survive subtracting the linear purchase cost, so the first-order condition is not sufficient under that assumption alone; the formalization uses concavity in the own quantity, under which it is. The participation claim $\pi_{r_i}(\bar q^I,\bar w^I) \ge 0$ is stated on the page without proof and needs a bound on the revenue of a location that stocks nothing.

In the Cournot example, uniqueness of the equilibrium must exclude asymmetric profiles and profiles where some retailers stock nothing, and the supplier's optimal price must be compared against every equilibrium at every price, including prices at which the retailers order nothing.

Formalization scope

Locations are Fin n; a profile is Fin n → ℝ; revenues are R : Fin n → (Fin n → ℝ) → ℝ, and dR i j q is $R_j^i(\bar q) = \partial R_j/\partial q_i$, given as a partial derivative at every profile with all entries positive. A deviation of retailer $i$ to $x$ is Function.update q i x, and Nash equilibria quantify over all $x \ge 0$. The standing assumptions of Section 3.2 are fields of the structure Model: $c > 0$; continuity of $R_i$ on the nonnegative orthant; the partial derivatives; $\partial^2 R_i/\partial q_i\partial q_j \le 0$, encoded as "$R_i^i$ does not increase in $q_j$"; and concavity of $R_i$ in $q_i$, which is the formalization's reading of "unimodal in $q_i$". The paper's assumption that marginal revenue eventually falls below every $\delta > 0$ is used only for existence of an equilibrium, which is not formalized, and is omitted.

Deviations from the page, each disclosed in the item concerned:

• $\bar q^I$ is taken as any positive solution of (6); its optimality for $\Pi$ is not used.
• "$\bar q^*$ is a Nash equilibrium" (p. 13) is read as $\bar q^I$.
• In $\phi(R_i(\bar q^I) - q_i^I w_i)$ (p. 14), $w_i$ is read as $w_i^I$.
• "$R_i^i(\bar q^I) > c$" needs a negative externality $\sum_{j\ne i}R_j^i(\bar q^I) < 0$, which is assumed.
• "$R_j^i(\bar q) \le 0$" is not a standing assumption, so it is a hypothesis of $w_i^I \ge c$, and strictness needs some strictly negative cross-effect.
• $\pi_{r_i}(\bar q^I,\bar w^I) \ge 0$ assumes nonnegative revenue at a location that stocks nothing.
• In the Cournot example the implicit $w < 1$ and $0 < c < 1$ are hypotheses; all retailers pay a common price; "increasing" is strict exactly where it holds ($n \ge 2$ for $\beta$, $\beta > 0$ for $n$).

A formalization that defines "the prices coordinate" as "the prices satisfy the first-order condition at $\bar q^I$" restates (6) and is ruled out: every equilibrium claim here is the game-theoretic statement about unilateral deviations. Contributions welcome: proofs of the equilibrium lemmas from concavity and the derivative, the Cournot uniqueness argument, and a general existence theorem for the quantity game.

Selected references

• G. P. Cachon, M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, working paper, June 2000. Published version: Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
• D. Fudenberg, J. Tirole, Game Theory, MIT Press, 1991 (Theorem 1.2, existence of pure-strategy equilibria).
• F. Bernstein, A. Federgruen, Pricing and Replenishment Strategies in a Distribution System with Competing Retailers, Operations Research 51(3):409–426, 2003. https://doi.org/10.1287/opre.51.3.409.14957
• J. Tirole, The Theory of Industrial Organization, MIT Press, 1988.

Motivation

Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.

Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping $H$ that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the $N$-stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.

Setting

Let $S$ (states) and $C$ (controls) be sets, and for each $x\in S$ let $U(x)\subseteq C$ be a nonempty control constraint set. Write $R^*=[-\infty,\infty]$ and let $F$ be the set of all functions $J:S\to R^*$, ordered pointwise. A mapping $H:S\times C\times F\to R^*$ is given, subject to the Monotonicity Assumption: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for all $x\in S$, $u\in U(x)$.

A selector is a function $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$. A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors. Define

$$T_\mu(J)(x)=H[x,\mu(x),J],\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),$$

and let $T^k$ be the $k$-fold composition of $T$. A terminal function $J_0\in F$ with $J_0(x)>-\infty$ for all $x$ is fixed. The $N$-stage cost of $\pi$ and the $N$-stage optimal cost are

$$J_{N,\pi}=(T_{\mu_0}T_{\mu_1}\cdots T_{\mu_{N-1}})(J_0),\qquad J^*_N(x)=\inf_{\pi}J_{N,\pi}(x).$$

A policy is uniformly $N$-stage optimal if each tail $(\mu_i,\mu_{i+1},\dots)$ is $(N-i)$-stage optimal, and $N$-stage $\varepsilon$-optimal if $J_{N,\pi}(x)\le J^*_N(x)+\varepsilon$ where $J^*_N(x)>-\infty$ and $J_{N,\pi}(x)\le-1/\varepsilon$ where $J^*_N(x)=-\infty$.

The three conditions on $H$ used in the chapter are F.1 (continuity of $H$ along nonincreasing sequences $J_k$ with $H(x,u,J_1)<\infty$), F.2 (there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$), and F.3 (a quantitative selection property with a constant $\beta>0$).

Formalization targets

Goal: Proposition 3.1

Under F.1, if $J_{k,\pi}(x)<\infty$ for all $x,\pi$ and $k=1,\dots,N$; or under F.2, if $J^*_k(x)>-\infty$ for all $x$ and $k=1,\dots,N$:

$$J^*_N=T^N(J_0),$$

and under F.2, for every $\varepsilon>0$ there is $\pi_\varepsilon$ with $J^*_N\le J_{N,\pi_\varepsilon}\le J^*_N+\varepsilon$.

Milestones

• Proposition 3.3: $\pi^*$ is uniformly $N$-stage optimal iff $(T_{\mu^*_k}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$. Needs monotonicity only.
• Corollary 3.3.1: a uniformly $N$-stage optimal policy exists iff every infimum $T^{k+1}(J_0)(x)=\inf_{u}H[x,u,T^k(J_0)]$ is attained, and then $J^*_N=T^N(J_0)$.
• Proposition 3.4: if $C$ is Hausdorff and every sublevel set $\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}$ is compact, then $J^*_N=T^N(J_0)$ and a uniformly $N$-stage optimal policy exists.
• Proposition 3.7: the minimax mapping $H(x,u,J)=\sup_{w\in W(x,u)}\{g+\alpha J[f]\}$ satisfies F.2 with constant $\alpha$.
• Proposition 3.6: the multiplicative mapping $H(x,u,J)=E\{g\,J[f]\mid x,u\}$ over a countable disturbance set satisfies F.1, and F.2 with constant $b$ when $0\le g\le b$.
• Proposition 3.2: under F.3 and the finiteness of $J_{k,\pi}$, $J^*_N=T^N(J_0)$ and, for $\varepsilon_n\downarrow0$, policies with $\{\varepsilon_n\}$-dominated convergence to optimality exist.
• Corollary 3.7.1(a): for minimax control with $J_0=0$ and $J^*_k>-\infty$, the DP algorithm gives $J^*_N$ and $N$-stage $\varepsilon$-optimal policies exist.

Significance

The identity $J^*_N=T^N(J_0)$ says that an infimum over an infinite-dimensional policy space equals $N$ nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in $T^N(J_0)$. Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.

These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.

Difficulty

The obvious argument interchanges the infimum over policies with the composition of operators: $\inf_\pi T_{\mu_0}(\cdots)=T(\inf_{\pi'}\cdots)$. The inequality $T^N(J_0)\le J^*_N$ follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside $H$ (F.1) or bounding how errors at later stages propagate through $H$ (F.2, F.3). Both steps break at infinite values. With $J^*_k(x)=-\infty$ there may be no $\varepsilon$-optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is $-\infty$, which is why F.3 and the definition of $\varepsilon$-optimality have two cases.

Formalization scope

The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. $T^N$ is m.T^[N], and $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ is a recursion that applies $T_{\mu_{N-1}}$ first. All values lie in EReal. The book's convention $\infty-\infty=\infty$ never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns $+\infty$ when the positive part diverges). Every theorem assumes $J_0>-\infty$ and $N\ge1$. Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants $b$ and $\alpha$.

$J^*_N$ is defined as an infimum over policies of the composed operators, never through $T$, so the goal is not true by definition. A formalization in which $J_{N,\pi}$ already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.

Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, Chapters 2–3. https://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3) (1977) 438–464. https://doi.org/10.1137/0315031
• D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press 1976.
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific 2022. https://web.mit.edu/dimitrib/www/abstractdp_MIT.html

Motivation

In network design games, selfish users build a shared network and split the cost of every edge among the users of that edge. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008), DOI 10.1137/070680096) studied the fair connection game, in which the cost of an edge is shared equally (the Shapley value) among its users. In this game the worst equilibrium can cost $k$ times the optimum, so the relevant measure is the price of stability: the ratio between the cheapest pure Nash equilibrium and the optimal centralized design. Their Theorem 2.1 bounds it by the harmonic number $H(k)=1+\frac12+\dots+\frac1k$ in every directed graph, and that bound is tight for directed graphs.

For undirected graphs the paper notes that $H(k)$ is not tight and calls the correct bound "an interesting open problem". Its Section 4 settles the smallest case: two players with a common terminal. The general theorem gives $H(2)=3/2$ there; Claim 4.1 improves this to $4/3$, and a three-node example shows that $4/3$ is the right value.

Timeline. Rosenthal (1973) showed that congestion games have pure Nash equilibria through a potential function. Anshelevich et al. (FOCS 2004; journal version 2008) introduced the price of stability for the fair connection game, proved the $H(k)$ bound and the two-player undirected bound $4/3$ treated here. Subsequent work studied the undirected multi-player case, which remains without a matching upper and lower bound in general.

Setting

Let $G=(V,E)$ be a finite undirected simple graph, with a cost $c_e\ge0$ on every edge $e$. There are two players, a common terminal $s\in V$ and personal terminals $t_1,t_2\in V$. A strategy of player $i$ is a set of edges $S_i\subseteq E$ that connects $t_i$ with $s$: in the graph $(V,S_i)$, $t_i$ and $s$ lie in the same connected component. A profile is a pair $S=(S_1,S_2)$ of strategies.

Under fair cost sharing each edge is paid for equally by the players using it. With $x_e\in\{1,2\}$ the number of players whose strategy contains $e$, player $i$ pays

$$C_i(S)=\sum_{e\in S_i}\frac{c_e}{x_e}.$$

A pure Nash equilibrium is a profile in which no player can lower its payment by switching to another strategy while the other player's strategy stays fixed. The total cost of a profile is the cost of the network it builds,

$$\mathrm{cost}(S)=\sum_{e\in S_1\cup S_2}c_e .$$

For a set $F$ of edges write $\mathrm{cost}(F)=\sum_{e\in F}c_e$. For a profile $(S_1,S_2)$, the quantities $x_1=\mathrm{cost}(S_1\setminus S_2)$, $x_2=\mathrm{cost}(S_2\setminus S_1)$ and $x_3=\mathrm{cost}(S_1\cap S_2)$ split the total cost into the private and the shared parts.

The game is an instance of a congestion game, with per-user latency $c_e/x$ on edge $e$; the mission builds on the published congestion-game layer CongestionPoA.AsymSum.Model.

Formalization targets

Goal: Claim 4.1 and its tightness

If the game has a profile, then some pure Nash equilibrium $S$ satisfies

$$\mathrm{cost}(S)\ \le\ \tfrac43\,\mathrm{cost}(P)\qquad\text{for every profile }P.$$

Moreover, in the three-node example (nodes $s,t_1,t_2$, edges $(s,t_1),(s,t_2)$ of cost $2$, edge $(t_1,t_2)$ of cost $1+\varepsilon$, with $0<\varepsilon<1$) the cheapest pure Nash equilibrium costs exactly $4$ and the optimum costs exactly $3+\varepsilon$, so the ratio $4/(3+\varepsilon)$ approaches $4/3$.

Milestones

1. (4.1). From every profile $(S_1,S_2)$, some pure Nash equilibrium $(S'_1,S'_2)$ has $y_1+y_2+\frac32y_3\le x_1+x_2+\frac32x_3$, where $y_i$ are the quantities of $(S'_1,S'_2)$.
2. Deviation inequalities. If $(S'_1,S'_2)$ is a Nash equilibrium and each $S_i$ is an inclusion-minimal strategy, then $y_1+\frac{y_3}2\le x_1+x_2+\frac{y_2}2+\frac{y_3}2$ and symmetrically for player 2.
3. (4.2). Under the same hypotheses, $\frac{y_1}2+\frac{y_2}2\le 2x_1+2x_2$.
4. The three-node example, as in the second half of the goal.

Significance

The result shows that the price of stability of fair cost sharing depends on the network: the $H(k)$ bound, tight for directed graphs, is not tight for undirected ones even with two players. It is the first undirected bound below $H(k)$ and the starting point for the later study of undirected fair network design, where the question for many players is still open.

The theorem is proved in the paper; this mission formalizes it. A search of the Prove2Me library found no formalization of the price of stability of fair connection games. Beyond the theorem itself, the mission produces a reusable undirected layer over the congestion-game library: connectivity strategies stated with Mathlib's graph reachability, fair cost sharing as a congestion game, and the total-cost functional. A checked proof of the potential inequality (4.1) is the two-player case of the potential argument behind Theorem 2.1.

Difficulty

The obvious argument starts from an optimal solution, follows improving moves to an equilibrium and compares potentials. For two players this only yields the factor $H(2)=3/2$: the potential counts shared edges with weight $3/2$, so a potential inequality alone cannot rule out an equilibrium in which both players share expensive edges. The improvement to $4/3$ needs a second inequality, (4.2), obtained from a specific deviation of each player in the equilibrium, and that deviation is valid only because of the undirected structure: the private parts of the two optimal paths together connect $t_1$ with $t_2$, and the deviating player can then follow the other player's equilibrium route to $s$. Making this connectivity claim precise for edge sets rather than drawn paths is where the formal work lies. It holds when the optimal strategies are inclusion-minimal, which is why the deviation milestones carry that hypothesis.

Formalization scope

• Vertices form a Fintype with decidable equality; edges are unordered pairs Sym2 V; the graph is a SimpleGraph V. Edge costs are a real function c with 0 ≤ c e for every e.
• A strategy of player i : Fin 2 (the paper's players 1 and 2 are 0 and 1) is a Finset of edges contained in G.edgeSet such that t i and s are Reachable in SimpleGraph.fromEdgeSet. Strategies are not restricted to paths.
• The game is a CongestionGame from CongestionPoA.AsymSum.Model with latency $c_e/x$; profiles, player costs and pure Nash equilibria are that library's IsProfile, cost and IsPureNash.
• "Price of stability at most $4/3$" is stated in existence form: some pure Nash equilibrium costs at most $\frac43$ times every profile. A formalization quantifying over all equilibria would be false (the price of anarchy is $2$), and one dropping the Nash condition would be trivial; neither is acceptable. The tightness half fixes a concrete instance and asserts both that an equilibrium of cost $4$ exists and that every equilibrium costs at least $4$.
• The deviation inequalities and (4.2) assume inclusion-minimal reference strategies; this hypothesis is implicit in the paper and does not appear in the goal, which quantifies over all profiles.

Contributions welcome: a proof of the potential inequality (finite improvement paths in the two-player fair game), the graph-theoretic lemma that the symmetric difference of two simple paths with a common endpoint connects their other endpoints, and a computation of the three-node example.

Selected references

• E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler, T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM Journal on Computing 38(4):1602–1623, 2008. https://doi.org/10.1137/070680096
• R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, International Journal of Game Theory 2:65–67, 1973. https://doi.org/10.1007/BF01737559
• D. Monderer, L. S. Shapley, Potential games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
• G. Christodoulou, E. Koutsoupias, The price of anarchy of finite congestion games, STOC 2005, 67–73. https://doi.org/10.1145/1060590.1060600

Motivation

Sequential decisions often change the distribution of future states. A planner choosing an action today must account for both its immediate reward and the later rewards made possible by the resulting state. The mathematical question is whether an optimal rule can be chosen once and reused at every stage, even when a competing plan may randomize and use the entire observed history. In Discounted Dynamic Programming, Blackwell studies this question on general Borel state and action spaces, beyond the finite models in which a direct comparison of actions is available.

The paper distinguishes several strengths of optimality. For each distribution of the initial state, an approximately optimal stationary plan exists, but a single plan that is approximately optimal at every initial state need not exist in a general Borel problem. Essential countability of the actions restores uniform approximate stationary optimality; essential finiteness yields exact stationary optimality. These are different mathematical claims, and the mission keeps their different quantifiers visible. Blackwell 1965, pp. 227, 229, 232–234.

Setting

A state is an element $s$ of a nonempty standard Borel space $S$, and an action is an element $a$ of a nonempty standard Borel space $A$. The transition kernel $q(\cdot\mid s,a)$ gives a probability distribution for the next state after action $a$ in state $s$. The reward $r(s,a,s')\in\mathbb R$ may depend on that next state $s'$; it is bounded and Borel measurable. Future rewards are discounted by $\beta$ with $0\le\beta<1$. These are the objects of Blackwell’s Sections 2–3. Blackwell 1965, pp. 227–228.

A plan $\pi=(\pi_1,\pi_2,\ldots)$ assigns a probability distribution of actions to each possible history before a decision. At stage $n$, that history contains $n-1$ completed state-action pairs and the current state. Thus plans may randomize and depend on earlier states and actions. A Markov plan instead uses a Borel function $f_n:S\to A$ at each stage; a stationary plan uses the same function $f$ at every stage and is denoted $f^{(\infty)}$. Starting from state $s$, the plan has discounted expected return

$$I(\pi)(s)=\sum_{n=1}^{\infty}\beta^{n-1}\,\mathbb E_s^\pi\bigl[r(\sigma_n,\alpha_n,\sigma_{n+1})\bigr].$$

Here $\sigma_n$ and $\alpha_n$ are the state and action at stage $n$. The comparison class for an optimal plan is all such plans, including randomized and history-dependent ones. Blackwell 1965, pp. 228–229.

Two actions are equivalent at state $s$ when they have the same reward $r(s,a,s')$ for every next state $s'$ and the same transition measure $q(\cdot\mid s,a)$. An action set is essentially countable by a Markov plan $(f_1,f_2,\ldots)$ if, for every $(s,a)$, one of the actions $f_n(s)$ is equivalent to $a$ at $s$. It is essentially finite by that plan if $S$ has a countable Borel partition $(S_n)$ such that, for $s\in S_n$, one of $f_1(s),\ldots,f_n(s)$ is equivalent to every action $a$ at $s$. A finite action set is a special case. Blackwell 1965, pp. 233–234.

Formalization targets

For a probability distribution $p$ on $S$ and $\varepsilon>0$, $(p,\varepsilon)$-optimality asks for a stationary $f$ with

$$p\{s:I(\pi)(s)>I(f^{(\infty)})(s)+\varepsilon\}=0\qquad\text{for every plan }\pi.$$

Theorem 6(b) asserts that such an $f$ always exists. Under essential countability, Theorem 7(a) obtains a stronger, uniform $\varepsilon$-optimality statement: for every $\varepsilon>0$ there is a stationary $f$ with $I(\pi)(s)\le I(f^{(\infty)})(s)+\varepsilon$ for all $\pi,s$. Its other targets identify the optimal return with the fixed point of the operator $U_\pi u=\sup_nT_{f_n}u$ and with the unique bounded solution of the optimality equation $u=\sup_{a\in A}T_au$. Blackwell 1965, pp. 232–234.

The mission’s goal is Theorem 7(b). Under essential finiteness, it asks for a stationary $f$ with exact optimality:

$$I(\pi)(s)\le I(f^{(\infty)})(s)\qquad\text{for every plan }\pi\text{ and state }s.$$

The milestone list also includes the paper’s operator identity, approximate selection result, contraction criterion, generated-plan comparison, and upper-bound criterion. Each has its own source index and statement. Blackwell 1965, pp. 231–234.

Significance

The exact result says that, under a condition weaker than a globally finite action set, repeated use of one measurable state-based rule matches or exceeds the return of every adaptive randomized plan. It is a structural result about what information and randomization can add to discounted control. The preceding approximate results specify what can still be guaranteed when that condition is relaxed; Blackwell’s examples show that the distinctions cannot simply be ignored. Blackwell 1965, pp. 229–230, 234.

Blackwell proved these statements in 1965. The formalization work here is to give machine-checked proofs for the Borel-space model and its full comparison class, together with reusable definitions of history-dependent kernels, returns, stationary rules, and Bellman operators. The draft theorem statements compile as Lean declarations, but their proofs remain open. The milestone results are intended to make both the final theorem and its supporting measure-theoretic objects independently usable.

Difficulty

On an uncountable Borel action space, the pointwise supremum of available action values does not automatically come with a Borel action selector. Choosing a maximizing action separately at each state may fail to define a measurable rule, and a supremum need not be attained. Also, a Markov or stationary comparison cannot by itself certify optimality against plans that depend on full histories. These issues are real in the paper’s examples: general Borel problems may lack an $\varepsilon$-optimal plan, and a given plan need not be uniformly approximated by a Markov plan. Blackwell 1965, pp. 229–230.

Formalization scope

The Lean model uses nonempty StandardBorelSpace types for $S$ and $A$. “Baire function” is read as Borel measurable on these metrizable spaces. The problem stores a Markov transition kernel, a bounded measurable real reward on $S\times A\times S$, and $0\le\beta<1$; $\beta=0$ is included. A plan contains a probability kernel on each finite history, and the return is the actual absolutely convergent series of expected one-stage rewards. The first decision is indexed by $0$ in Lean, corresponding to the paper’s index $1$. The finite history law is assembled through kernel composition products, and a stationary rule is represented by deterministic kernels. The integrals and series therefore express the paper’s expected return, including the cases where the reward depends on the next state.

For the operator results, $M(S)$ means bounded and measurable real functions. The suprema defining $U_\pi$ and the optimal return are real suprema over nonempty families bounded by the reward and discount; they are used only in that setting. The abstract operator in Theorem 5 maps $M(S)$ into itself. The action equivalence predicate uses the paper’s explicit equality of reward functions and transition laws; the later “i.e.” phrasing on p. 234 is weaker when interpreted as equality of operators alone. A partition piece may be empty, and Lean’s piece $n$ corresponds to the paper’s $S_{n+1}$, with rules $f_1,\ldots,f_{n+1}$.

An optimality claim here always compares with every randomized history-dependent plan. Restricting that quantifier to Markov or stationary plans would trivialize the target. A complete development needs measure-theoretic facts about history laws and their bounded integrals, the discounted series, measurable partitions and selections, and the sup-norm contraction of bounded Borel functions. The history-law and bounded-function infrastructure can be reused outside this mission. Contributions to those foundations and to the numbered milestone theorems are welcome.

Selected references

• David Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1), 226–235, 1965. DOI: 10.1214/aoms/1177700285.

Motivation

A revenue-sharing contract $\{\phi, w\}$ lets a supplier charge a retailer a wholesale price $w$ per unit and, in addition, collect the share $1 - \phi$ of the retailer's revenue. The video-rental industry adopted such contracts at scale in the late 1990s, and Cachon and Lariviere showed that in a broad class of models they coordinate the supply chain: the retailer's privately optimal decisions coincide with those that maximize total channel profit, and the profit can be split arbitrarily between the firms (missions 1 and 2 of this series).

The same authors also studied where revenue sharing breaks down. The most practically relevant limitation is retailer effort: shelf space, service, store cleanliness and promotion raise demand, cost the retailer money, and cannot be written into a contract. Once the retailer gives away part of its revenue, it earns only a share of the return on its effort while still paying the whole cost. This mission formalizes Section 4.2 of the authors' working paper, which shows that revenue sharing then cannot coordinate the channel while leaving the supplier any profit, and, in an explicit linear-demand example, determines exactly when the supplier is better off with the plain wholesale-price contract.

The source is the June 2000 working paper (Cachon and Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations), whose results are displayed claims inside numbered sections rather than numbered theorems; the milestones cite section, printed page and display. The published version appeared in Management Science 51(1), 2005.

Setting

General model (Sec. 4.2.1). A supplier produces at unit cost $c > 0$. The retailer chooses an order quantity $q \ge 0$ and an effort level $e \ge 0$ after observing the contract $\{\phi, w\}$. Expected revenue $R(q, e)$ is continuous, differentiable, strictly increasing in $e$ and concave in $q$; effort costs the retailer $g(e)$, where $g$ is continuous, increasing, differentiable and convex with $g(0) = 0$. The profits of the integrated channel, the retailer and the supplier are

$$\Pi(q, e) = R(q, e) - g(e) - qc,\qquad \pi_r(q, e) = \phi R(q, e) - g(e) - qw,\qquad (1-\phi)R(q, e) + q(w - c).$$

The integrated solution $(q_I, e_I)$ maximizes $\Pi$ over $q, e \ge 0$.

Linear example (Sec. 4.2.2). Inverse demand is $P(q, e) = 1 - q + 2\tau e$ with an effort-impact parameter $\tau \ge 0$, revenue is $R(q, e) = qP(q, e)$ and effort costs $g(e) = e^2$. For a share $\phi$ the supplier's profit when the retailer responds optimally to $\{\phi, w\}$ is $\pi_s(w, \phi)$, and the supplier's optimal profit is

$$V(\phi) = \sup_{w \ge 0} \pi_s(w, \phi).$$

The share $\phi = 1$ is the wholesale-price contract.

Formalization targets

Goal: the supplier's choice of contract

For $0 \le \tau < 1$, $0 < c < 1$ and every $\phi \in (0, 1]$, the supremum defining $V(\phi)$ is attained at the price $w(\phi) = \phi\big((1-\tau^2)\phi + c(1-\phi\tau^2)\big)/\big(1 + \phi(1-2\tau^2)\big)$, and

$$V(\phi) = \frac{(1 - c)^2}{4\big(1 + \phi(1 - 2\tau^2)\big)} .$$

Consequently $V$ is strictly increasing on $(0, 1]$ if $\tau > 1/\sqrt 2$ (the wholesale-price contract is the supplier's unique best share), constant if $\tau = 1/\sqrt 2$, and strictly decreasing if $\tau < 1/\sqrt 2$, with $V(\phi) \to (1-c)^2/4$ as $\phi \to 0^+$.

Milestones

1. Sec. 4.2.1, p. 22: with $w = \phi c$ and $\phi < 1$ the retailer's optimal effort at $q_I$ is below $e_I$.
2. Sec. 4.2.1, p. 22: if $(q_I, e_I)$ is optimal for the retailer, then $\phi = 1$, $w = c$, and the supplier earns nothing.
3. Sec. 4.2.2, p. 23: the retailer's unique optimal effort at quantity $q$ is $e(q) = \phi\tau q$.
4. Sec. 4.2.2, pp. 23–24: the retailer's reduced profit $q[\phi - q(\phi - \phi^2\tau^2) - w]$, its unique joint optimum $\big(q(w,\phi), e(q(w,\phi))\big)$ with $q(w, \phi) = (\phi - w)/(2(\phi - \phi^2\tau^2))$ for $w < \phi$ and $0$ otherwise, and the optimal profit $(\phi - w)^2/(4(\phi - \phi^2\tau^2))$.
5. Sec. 4.2.2, p. 24: the integrated retail price $p_I = (1 + c(1-2\tau^2))/(2(1-\tau^2))$, increasing in $c$ if $\tau < 1/\sqrt 2$ and decreasing if $\tau > 1/\sqrt 2$.
6. Sec. 4.2.2, p. 24: $\pi_s(\cdot, \phi)$ is strictly concave where the retailer orders, and $w(\phi)$ is its unique maximizer over $w \ge 0$.
7. Sec. 4.2.2, p. 24: $\pi_s(w(\phi), \phi) = (1-c)^2/\big(4(1 + \phi(1-2\tau^2))\big)$.

Significance

The general result (milestones 1–2) is a clean impossibility statement: with non-contractible effort, the only contract in the revenue-sharing family that coordinates the channel is the wholesale-price contract at marginal cost, which leaves the supplier zero profit. It marks the boundary of the coordination results of the earlier sections, and contrasts with the price-dependent newsvendor, where revenue sharing does coordinate price and quantity because the cost of expanding demand is captured in the revenue function and shared by both firms.

The example turns the impossibility into a design rule. Because coordination is out of reach, the supplier compares contracts by her own profit, and the threshold $\tau = 1/\sqrt 2$ separates two regimes: when effort matters a lot she should leave the retailer all revenue and charge only a wholesale price ("a smaller share of a larger pie"); when it matters little she should take as much revenue as possible. The same threshold governs the counterintuitive comparative static that the integrated channel's retail price falls as production cost rises.

All results are proved on paper in the source. None has a machine-checked proof; this mission produces the first. The example is a fully explicit two-stage optimization problem, so the formal development also yields a verified computation of a Stackelberg equilibrium with moral hazard that other contract-design missions can reuse.

Difficulty

The individual calculations are elementary, and the work lies in getting the optimization statements right. The page solves the retailer's problem sequentially (effort first, then quantity) and writes the supplier's objective by substituting closed forms. A faithful proof must instead show that these closed forms are global optima over the constrained domains: the retailer optimizes jointly over the quadrant $q, e \ge 0$, the corner $q = 0$ is optimal whenever $w \ge \phi$, and the supplier's objective is a quadratic on $w \le \phi$ glued to the zero function on $w \ge \phi$, which is not concave on all of $w \ge 0$. The first-order-condition argument of the general model similarly needs an interior integrated optimum and a strictly positive marginal effect of effort, which "strictly increasing in $e$" alone does not provide.

Formalization scope

All quantities are real numbers. The general model is a structure RevShareCoord.Effort.Model carrying $R$, its partial derivatives, $g$, $g'$ and $c$; derivatives are one-sided within $[0, \infty)$, and joint differentiability of $R$ is replaced by its partial derivatives and joint continuity. The example lives in RevShareCoord.Effort.Linear. "Optimal" always means a maximizer over the whole admissible set ($q, e \ge 0$ for the retailer, $w \ge 0$ for the supplier), and the supplier's value $V(\phi)$ is defined as the supremum of her attainable profits, not by the printed formula.

Deviations from the page, each disclosed in the item's Formalization Note:

• $\tau < 1$ instead of $\tau \in [0, 1]$: at $\tau = 1$ the integrated problem is unbounded and $p_I$ divides by zero. The page's "jointly concave in $q$ and $\tau$" is read as $q$ and $e$.
• $0 < c < 1$: $c > 0$ is the standing assumption of Sec. 1, and $c < 1$ is needed for a positive integrated quantity.
• $\phi \in (0, 1]$ in the example: at $\phi = 0$ the retailer keeps no revenue and $q(w, \phi)$ divides by zero. The page's optimal share "$\phi = 0$" for $\tau < 1/\sqrt 2$ is stated as strict decrease on $(0, 1]$ with the limit at $0^+$.
• The printed second derivative $-\big(1 - \phi(1-2\tau^2)\big)/\big(2\phi^2(1-\phi\tau^2)^2\big)$ has a sign slip in the numerator; the Lean states $-\big(1 + \phi(1-2\tau^2)\big)/\big(2\phi^2(1-\phi\tau^2)^2\big)$.
• "Otherwise decreasing" fails at $\tau = 1/\sqrt 2$, where $V$ and $p_I$ are constant; the trichotomy is stated.
• In the general model, the integrated optimum is interior, $\partial R/\partial e > 0$ at it, and, for milestone 1, $\pi_r(q_I, \cdot)$ is strictly concave in $e$ (the page asserts this but it does not follow from the assumptions).

Plugging the printed $w(\phi)$ into $\pi_s$ and comparing across $\phi$ would turn the dichotomy into a statement about an arbitrary price schedule; the goal instead asserts that $w(\phi)$ attains the supremum over all $w \ge 0$, with the retailer best-responding jointly in $(q, e)$.

No external library beyond Mathlib's real analysis and convexity is needed. Contributions welcome: proofs of the milestones, reusable lemmas on maximizing strictly concave quadratics over orthants, and a generalization of milestone 2 to non-interior optima.

Selected references

• G. P. Cachon, M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, working paper, June 2000. Published version: Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science 11, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7
• S. Desiraju, S. Moorthy, Managing a Distribution Channel under Asymmetric Information with Performance Requirements, Management Science 43(12), 1997. https://doi.org/10.1287/mnsc.43.12.1628

Motivation

A supplier who sells to a retailer at a per-unit wholesale price above her own production cost induces the retailer to order less than an integrated firm would. This effect, double marginalization, goes back to Spengler (1950) and is the standard benchmark against which supply chain contracts are judged: a contract coordinates the channel if it makes the decentralized decisions coincide with the integrated optimum. Revenue-sharing contracts, as used in the video-rental industry, coordinate the channel; the plain wholesale-price contract does not. Whether a supplier should bother with the administrative cost of revenue sharing depends on how much the wholesale-price contract actually loses and how much of the remaining profit the supplier keeps.

Cachon and Lariviere answer that question for a retailer whose revenue depends only on the quantity ordered, in Section 4.1.1 of their working paper Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations (June 2000; the 2005 Management Science version renumbers and revises the material). They show that the answer is governed by the curvature of the marginal revenue curve, and they compute it exactly for a one-parameter family. The source is the June 2000 working paper, whose results are unnumbered; every item cites its section, page and display.

Setting

A supplier produces at unit cost $c > 0$ and sells to a single retailer. The retailer's expected revenue from $q$ units is $R(q)$, where $R(0) = 0$, $R$ is strictly concave and differentiable on $[0,\infty)$ with derivative $R'$ (the marginal revenue), $R'$ is differentiable on $(0,\infty)$ with derivative $R''$, the product is viable ($R'(0) > c$), and a finite quantity is optimal ($R'(q) < c$ for some $q$). The supply chain profit is $\Pi(q) = R(q) - qc$; the integrated quantity $q_I$ maximizes $\Pi$ over $q \ge 0$.

Under a wholesale-price contract with price $w$, the retailer orders $q$ to maximize $R(q) - wq$. Each order $q \ge 0$ is induced by exactly one price, $w(q) = R'(q)$, so the supplier can be thought of as choosing $q$. Her profit, the retailer's profit, and their sum are then

$$\pi_s(q) = q\,(R'(q) - c), \qquad \pi_r(q) = R(q) - qR'(q), \qquad \pi_s(q) + \pi_r(q) = \Pi(q).$$

Following the paper, $q \mapsto R'(q) + qR''(q)$ is assumed decreasing, which makes $\pi_s$ unimodal. The supplier's optimal quantity to induce $q^*$ maximizes $\pi_s$ over $q \ge 0$, and $w(q^*)$ is her optimal wholesale price. The efficiency of the contract and the supplier's profit share are

$$\frac{\pi_s(q^*) + \pi_r(q^*)}{\Pi(q_I)} \qquad\text{and}\qquad \frac{\pi_s(q^*)}{\Pi(q^*)} .$$

In the α-family, $R(q) = q - q^{\alpha+1}/(\alpha+1)$ for $\alpha > 0$ and $q \in [0,1]$, so $R'(q) = 1 - q^\alpha$: marginal revenue is convex for $\alpha < 1$, linear for $\alpha = 1$ and concave for $\alpha > 1$.

Formalization targets

Goal: the α-family

For $\alpha > 0$ and $0 < c < 1$, the quantities $q^* = \left(\frac{1-c}{1+\alpha}\right)^{1/\alpha}$ and $q_I = (1-c)^{1/\alpha}$ are the unique maximizers of $\pi_s$ and $\Pi$ on $[0,1]$, the profit share is $(1+\alpha)/(2+\alpha)$, and

$$\frac{\pi_s(q^*) + \pi_r(q^*)}{\Pi(q_I)} = \frac{2+\alpha}{(1+\alpha)^{\frac{1+\alpha}{\alpha}}},$$

a quantity that does not depend on $c$, is strictly increasing in $\alpha$, tends to $2/e$ as $\alpha \to 0^+$ and to $1$ as $\alpha \to \infty$.

Milestones for a general revenue function

1. The price $w(q) = R'(q)$ makes $q$ the retailer's unique optimum (Eq. (9)).
2. $0 < q^* < q_I$.
3. $w(q^*) = c - q^*R''(q^*)$, and $w(q^*) > c$.
4. The profit share is at most (at least) $2/3$ when $R'$ is convex (concave), strictly under strict convexity (concavity).
5. $2q^* \le q_I$ ($\ge q_I$) when $R'$ is convex (concave), strictly under strict convexity (concavity).
6. $\Pi(q_I) - \Pi(q^*) = \int_{q^*}^{q_I}(R'(z) - c)\,dz$ is at least (at most) $\tfrac12\pi_s(q^*)$ when $R'$ is convex (concave), strictly under strict convexity (concavity).

Milestones for the α-family

7. The closed forms of $q^*$, $q_I$, $\pi_r(q^*)$, $\pi_s(q^*)$ and $\Pi(q_I)$.
8. $E(\alpha) = (2+\alpha)/(1+\alpha)^{(1+\alpha)/\alpha}$ is strictly increasing on $(0,\infty)$ with limits $2/e$ and $1$.

Significance

The general milestones turn the paper's area argument (the triangle under the tangent to marginal revenue at $q^*$) into three comparisons: convex marginal revenue makes the wholesale-price contract worse for the chain and leaves the supplier at most two thirds of a smaller pie, concave marginal revenue the opposite. The α-family makes the trade-off exact: efficiency never falls below $2/e \approx 0.736$, while the supplier's share $(1+\alpha)/(2+\alpha)$ moves much faster than efficiency, which is the paper's argument for why revenue sharing is most attractive when marginal revenue is convex.

These results are proved on paper but, to our knowledge, not machine-checked anywhere; Mathlib has no supply chain contract theory. The formalization provides a reusable single-retailer wholesale-price model, a checked version of the convex/concave tangent comparisons, and a corrected statement of the α-family's monotonicity (see the scope section).

Difficulty

The general comparisons are short on paper but rest on a picture: they need the first-order condition at an interior maximizer, the tangent-line inequality for a convex or concave derivative, and the fundamental theorem of calculus for a function whose derivative is known only on a half-line and one-sided at $0$. Strictness needs a strictly positive integrand on a nondegenerate interval.

The α-family is where the analysis is not routine. The closed forms involve real powers with exponents $1/\alpha$ and $(1+\alpha)/\alpha$, which must be combined carefully. The limit $(1+\alpha)^{1/\alpha} \to e$ as $\alpha \to 0^+$ is classical, but the monotonicity of $\log(2+\alpha) - \frac{1+\alpha}{\alpha}\log(1+\alpha)$ on all of $(0,\infty)$ is not a one-line derivative sign check: the derivative mixes $\log(1+\alpha)/\alpha^2$ with rational terms, and its sign has to be established uniformly near $0$ and near $\infty$.

Formalization scope

Quantities and prices are real numbers. "Optimal" always means a maximizer over all admissible quantities (IsMaxOn on $[0,\infty)$, or on $[0,1]$ in the α-family, as the page restricts), never a root of a first-order condition. The derivative $R'$ of the general model is linked to $R$ by a one-sided derivative hypothesis on $[0,\infty)$; $R''$ is required only on $(0,\infty)$, since for $\alpha < 1$ it blows up at $0$. In the α-family the marginal revenue is deriv of $R$, not a separate function, and $0 < c < 1$ is assumed (implicit on the page: $c > 0$ and $R'(0) = 1 > c$). Efficiency and profit share are real divisions; their denominators are positive at the optimal quantities.

Deviations from the page, all disclosed in the items:

• $R(0) = 0$ is added to the model. It is implicit in the paper's area reading of the retailer's profit, and the $2/3$ comparison fails without it.
• The paper states the curvature comparisons strictly ("less (more) than 2/3rds", "$q^* > q_I/2$ ($< q_I/2$)", "more (less) than 50%") under convexity (concavity). Linear marginal revenue is both and gives equality, so each item states the weak inequality under convexity or concavity and the strict one under strict convexity or concavity.
• Printed slip. The page says "Efficiency is a decreasing function of α, i.e., efficiency improves as the marginal revenue curve becomes more concave". $E$ is in fact strictly increasing ($E(0^+) = 2/e \approx 0.7358$, $E(1) = 0.75$, $E(10) \approx 0.858$), as the second half of the sentence and the two limits say. The Lean states the increasing form; the milestone text is kept verbatim. The numerical gloss "$2/e \approx 0.73$" is not formalized.

A trivializing formalization is ruled out: the efficiency in the goal is the ratio of profits computed from $R$ at the maximizers, not a definition equal to $(2+\alpha)/(1+\alpha)^{(1+\alpha)/\alpha}$, and the maximizers are characterized as unique argmaxes rather than assumed.

Welcome contributions: proofs of the general tangent comparisons, which are reusable for any concave revenue model; the real-analysis lemmas on $(1+\alpha)^{1/\alpha}$; and the α-family closed forms.

Selected references

• G. P. Cachon and M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, working paper, June 2000. Published version: Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
• J. J. Spengler, Vertical Integration and Antitrust Policy, Journal of Political Economy 58(4):347–352, 1950. https://doi.org/10.1086/256964
• M. A. Lariviere and E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971