The OR Formalization Drive

Why revenue sharing

A supplier who sells to an independent retailer through a plain per-unit wholesale price faces double marginalization: the retailer orders less than the quantity that maximizes the profit of the supply chain as a whole, because each unit costs him the wholesale price rather than the production cost. Supply chain contracting studies payment schemes under which the retailer's own optimum coincides with the system optimum. Such a scheme is said to coordinate the channel. The usual examples are buy-back contracts (Pasternack, 1985), quantity-flexibility contracts (Tsay and Lovejoy, 1999) and quantity discounts (Jeuland and Shugan, 1983; Moorthy, 1987).

Cachon and Lariviere study revenue sharing, in which the retailer pays a low wholesale price and also hands over a fixed fraction of his revenue. The scheme was common in video-cassette rental in the late 1990s, where it let rental chains stock far more copies of new releases. This mission formalizes the paper's single-retailer result: revenue sharing coordinates the channel, and the supplier can choose any split of the channel's maximal profit. It also includes the three further results of the paper that use the same argument.

The source is the authors' working paper of June 2000. Its results are unnumbered, so every item cites a section, a displayed equation and a printed page. The 2005 Management Science version renumbers and revises the material.

Setting

A supplier sells to one retailer, who orders $q \ge 0$ units before a selling season. The retailer's expected revenue is a function $R(q)$ of the quantity alone. Leftover units have zero salvage value, and the supplier produces each unit at cost $c > 0$. The paper's standing assumptions (Sec. 1, p. 5) are:

• $R$ is strictly concave and differentiable for $q \ge 0$, with marginal revenue $R'(q)$;
• the product is viable: $R'(0) > c$;
• a finite quantity is optimal: $R'(\infty) < c$.

A revenue-sharing contract $\{\phi, w\}$ has two terms. The retailer pays the wholesale price $w \ge 0$ per unit, and he keeps the share $\phi$ of the revenue and transfers $(1-\phi)R(q)$ to the supplier. The case $\phi = 1$ is the plain wholesale-price contract. The profits of the supply chain, the retailer and the supplier are

The integrated channel quantity $q_I$ is the maximizer of $\Pi$ over $q \ge 0$. In Lean these objects are RevShareCoord.Single.Model (fields R, R', c and the three assumptions) and its functions Pi, retailerProfit and supplierProfit.

Formalization targets

Goal: revenue sharing coordinates the channel (Sec. 2.2, p. 6)

Let $\phi \in (0,1]$ and $w(\phi) = \phi c$. Then

The statement fixes no revenue function and no share. It holds for every model and every $\phi \in (0, 1]$, which is what "the supplier can take any share of the channel profit" means.

Milestones on the way

1. Eq. (1), p. 6. $q_I$ exists, is unique and positive, and is the only positive root of $R'(q_I) = c$.
2. Retailer's first-order condition, p. 6. If $R'(0) > w/\phi$, an order $\hat q \ge 0$ is optimal for the retailer exactly when $\hat q > 0$ and $\phi R'(\hat q) = w$. The retailer has at most one optimal order.
3. Profit identities, p. 6. Under $\{\phi, \phi c\}$, $\pi_r(q) = \phi\Pi(q)$ and $\pi_s(q) = (1-\phi)\Pi(q)$ at every $q$.
4. Heterogeneous retailers, p. 7. Given $c$ and $\phi$, a single wholesale price, chosen before the revenue function, coordinates every retailer of the model.

Further results on the same argument

5. Buy-back equivalence, Sec. 2.3, p. 9. Take the fixed-price newsvendor and the buy-back contract $b^* = p(1-\phi)$, $w_b^* = p(1-\phi)+\phi c$. It gives the retailer and the supplier the same realized profits as $\{\phi, \phi c\}$, for every order and every demand realization.
6. Endogenous price, Sec. 3.1 and footnote 3, p. 11. Let revenue $\mathrm{Rev}(q,p)$ be any function of quantity and price, with costs linear in quantity. Then $\pi_r(q,p) = \phi\,\Pi(q,p)$ under $\{\phi,\phi c\}$, and the integrated optimum $(q_I,p_I)$, assumed unique, is the retailer's unique optimum.

Significance

The result separates coordination from profit division. A contract family coordinates for every value of a parameter, and that parameter then moves profit between the firms without changing the quantity, so the contract terms can be settled by bargaining power alone. The heterogeneous-retailer milestone gives the practical advantage over quantity discounts: the coordinating terms do not depend on the retailer's demand, so one price list serves retailers who face different markets. The Sec. 2.3 equivalence shows that, in the fixed-price newsvendor, buy-backs are a special case of revenue sharing. The Sec. 3.1 statement shows that revenue sharing still coordinates when the retailer also sets the price, a setting in which Emmons and Gilbert (1998) showed buy-backs fail.

All of these results are proved in the paper, and none is open. The mission adds a machine-checked version of the single-retailer theory for a general strictly concave revenue function. A related newsvendor version is already formalized on the platform: SupplyChainTheory.revenue_sharing_coordinates, from Snyder and Shen, Fundamentals of Supply Chain Theory, Thm 14.6. That version has a newsvendor revenue with salvage values and goodwill costs, and it concludes the optimality of three profits, not the $\phi$-split of this paper. It is a different statement, so it is not reused here.

Difficulty

The algebra is short. The identity $\pi_r = \phi\Pi$ under $w = \phi c$ is a single line, and it is a milestone, not the goal. The work lies in the optimization claims over a half-line with only one-sided information at $0$. The integrated optimum must be shown to exist. $R'(\infty) < c$ gives only an eventual bound on the derivative, so the existence argument needs the continuity of a concave function and its supergradient inequality. It must also be shown positive, which uses $R'(0) > c$ as a one-sided derivative. Its uniqueness rests on strict concavity. The retailer's first-order condition needs the same machinery for $\phi R - wq$, including the observation that the boundary point $0$ is never optimal. A stationary point of $\pi_r$ is not enough. The goal asserts that $q_I$ is the unique maximizer over all of $[0,\infty)$.

Formalization scope

• Quantities, prices and shares are real numbers. $R$ and $R'$ are functions $\mathbb R \to \mathbb R$, constrained only on $[0,\infty)$. Differentiability is HasDerivWithinAt R (R' q) (Set.Ici 0) q for $q \ge 0$, so it is one-sided at $0$. Strict concavity is StrictConcaveOn ℝ (Set.Ici 0) R.
• $R'(\infty) < c$ is encoded as "$R'(Q) < c$ for some $Q \ge 0$". For a decreasing $R'$ this is equivalent, and it allows $R' \to -\infty$.
• "Optimal" means IsMaxOn over $[0,\infty)$ (over $[0,\infty)\times P$ in Sec. 3.1), and "unique" means every other maximizer equals it.
• The supplier's profit $\pi_s$ is not displayed in the paper. It is read off the sequence of events of Sec. 1.
• The goal and the first-order condition take $\phi \in (0,1]$. At $\phi = 0$ the retailer's profit is identically zero and $q_I$ is not the unique optimum. The profit identities and the buy-back identities hold for all real parameters and are stated that way.
• Corrected slips. (a) Eq. (1) is introduced with "$R'(0) \ge c$". This contradicts the standing assumption $R'(0) > c$: with equality, $q_I = 0$ is not positive. The statement uses $R'(0) > c$. (b) The display $\pi_r(q_I) = \phi R(q_I) - q_I c = \phi\Pi(q_I)$ has a wrong middle term, which should read $\phi R(q_I) - q_I\phi c$. The outer equality is stated.
• The first-order-condition milestone adds the converse direction and uniqueness to the paper's "must satisfy". It does not claim that an optimum exists, which may fail when $w/\phi < c$.
• Sec. 3.1 is stated in the generality of footnote 3: an arbitrary revenue function $\mathrm{Rev}(q,p)$ and a set $P$ of admissible prices, with the integrated optimum's uniqueness as a hypothesis, as the paper assumes it. The paper's monotonicity of $F(x,p)$ in $p$ is unused and omitted.
• Sec. 2.3 is formalized pathwise. The expected-profit equations (2)–(4) are not part of the mission.
• A goal that only asserts $\pi_r(\phi, \phi c, q) = \phi\,\Pi(q)$ would be an unfolding of definitions. The goal therefore carries the argmax-and-uniqueness claim, which needs strict concavity and the model's assumptions.
• Needed infrastructure: first-order conditions for concave functions on a closed half-line with one-sided derivatives, and existence of maximizers from an eventual derivative bound. Both are reusable beyond this mission. Contributions of that general kind are welcome.

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
• B. A. Pasternack, Optimal pricing and return policies for perishable commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• K. S. Moorthy, Managing channel profits: Comment, Marketing Science 6(4):375–379, 1987. https://doi.org/10.1287/mksc.6.4.375
• A. A. Tsay, W. S. Lovejoy, Quantity flexibility contracts and supply chain performance, Manufacturing & Service Operations Management 1(2):89–111, 1999. https://doi.org/10.1287/msom.1.2.89
• H. Emmons, S. M. Gilbert, Note: The role of returns policies in pricing and inventory decisions for catalogue goods, Management Science 44(2):276–283, 1998. https://doi.org/10.1287/mnsc.44.2.276
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Ch. 14. https://doi.org/10.1002/9781119584445

Motivation

Many selection problems assign a value to each subset of a finite collection: the coverage supplied by chosen facilities, the influence reached by chosen seeds, or the value of a coalition. A submodular set function has diminishing returns in the precise sense that the combined value of two sets, counting their overlap once, does not exceed the sum of their separate values. When the function is also monotone, taking more elements never hurts. The unconstrained problem studied here permits nonmonotone functions, so both accepting and rejecting an element can matter. The question is what a single pass through the elements can guarantee when the function is available through value queries. Buchbinder et al., FOCS 2012

The randomized algorithm in this mission attains an expected one-half approximation for every nonnegative submodular function. The paper presents this as tight in the value-oracle setting: it recalls the earlier result of Feige, Mirrokni and Vondrák that a fixed improvement beyond one-half requires exponentially many queries. The contribution here is therefore both the guarantee and a short adaptive rule that attains it in a linear number of iterations. The local proposal follows the FOCS 2012 version of the paper; its theorem numbering differs from the later SIAM Journal on Computing article. Buchbinder et al., §I.A and Theorem I.2

Setting

Let $\mathcal N$ be a finite ground set, and let $f:2^{\mathcal N}\to\mathbb R_{\ge0}$ assign a nonnegative real value to every subset. The unconstrained submodular maximization problem asks for the largest value $f(S)$ among all $S\subseteq\mathcal N$. Write $OPT$ for that value when no confusion arises, and $O$ for a set attaining it. Submodularity means

There is no monotonicity or normalization assumption: $f(\varnothing)$ and $f(\mathcal N)$ may both be positive. A value oracle returns $f(S)$ for a requested subset $S$. The paper's complexity claim counts such queries, assuming a query takes constant time. Buchbinder et al., §I and footnotes 1–2

Algorithm 2 visits the elements once in an arbitrary order $u_1,\ldots,u_n$. It keeps two sets, starting at $X_0=\varnothing$ and $Y_0=\mathcal N$. At step $i$, it measures the gain $a_i$ from adding $u_i$ to $X_{i-1}$ and the gain $b_i$ from removing $u_i$ from $Y_{i-1}$. It clips each gain at zero, giving $a'_i=\max(a_i,0)$ and $b'_i=\max(b_i,0)$. It adds $u_i$ to $X$ with probability $a'_i/(a'_i+b'_i)$ and otherwise removes it from $Y$. When both clipped gains vanish, the paper defines the add probability as one. After all elements have been processed, the two sets coincide, and the algorithm returns their common value. The state law is adaptive: its probability at step $i$ depends on the actual pair of sets produced by earlier choices. Buchbinder et al., Algorithm 2

Formalization targets

The main target is Theorem I.2 for this exact algorithm and for every enumeration of the ground set:

The milestone statements retain the paper's key local quantities. For a comparison optimum $O$, set $OPT_i=(O\cup X_i)\cap Y_i$. Lemma II.1 asserts $a_i+b_i\ge0$. The endpoint statement identifies $OPT_0=O$ and $OPT_n=X_n=Y_n$. Inequality (3) bounds the conditional loss in the positive-gain case; Lemma III.1 compares the expected change of $OPT_i$ with the expected combined change of $X_i$ and $Y_i$. The telescoped display keeps the initial endpoint values $f(\varnothing)$ and $f(\mathcal N)$ before using nonnegativity. Buchbinder et al., Lemmas II.1 and III.1, inequality (3), proof of Theorem I.2

A companion target is Theorem I.4 via its second proof. For two normalized monotone submodular utilities $f_1,f_2$, let $g(S)=f_1(S)+f_2(\mathcal N\setminus S)$. The maximum of $g$ is exactly the optimal welfare of a two-player partition. Algorithm 2 on $g$ is asked to satisfy

This is the paper's three-quarter guarantee in its welfare application. Buchbinder et al., Theorem I.4 and Proof (2)

Significance

The main theorem gives a specific randomized rule whose expected value is at least half the best subset value, even when accepting an element can lower the objective. It applies without restricting the cardinality or shape of the chosen subset. The welfare corollary shows that keeping the initial endpoint values in the analysis yields a stronger guarantee for the objective formed from two monotone players. Buchbinder et al., Theorems I.2 and I.4

This mission formalizes the statement of the algorithm, its intermediate state laws, its comparison set, and the paper's numbered proof targets. The algorithmic guarantee is proved in the source paper; the local Lean theorem files are open statements with sorry and do not yet give machine-checked proofs of these results. A completed development would supply a reusable formal model of an adaptive finite random process over pairs of subsets, as well as the specific submodular inequalities. The published Submodular and OPT definitions from the earlier Feige–Mirrokni–Vondrák formalization are reused here.

Difficulty

The two possible updates cannot be assessed independently. The probability of each choice depends on the current state, and the comparison set $OPT_i$ can gain or lose the processed element in a way that differs from the two algorithm sets. A bound on the expected value of $X_i$ alone does not control the movement of $OPT_i$. The proof must handle the clipped gains, including the case when both are zero, while preserving the exact joint law of $(X_i,Y_i)$. Buchbinder et al., proof of Lemma III.1

Formalization scope

The ground set is a finite Lean type; subsets are Finset X, and values are real numbers. An order is a list with no repeated elements that covers the type, including the empty type. The run is an explicit finite mass function on pairs of subsets after every prefix of the list. Expectation is a finite weighted sum, so it has no integrability exception. The transition clips the two real marginal gains and handles $0/0$ by assigning probability one to the add branch, exactly as Algorithm 2 specifies. The optimum is the published maximum over all subsets. No ratio divides by a possibly zero optimum.

The theorem fixes Algorithm 2 itself; an arbitrary process with nested sets or a process defined by its desired approximation property does not satisfy this scope. The Lean goal states the value bound and leaves the paper's linear-time claim outside the formal theorem. The algorithm uses four value evaluations per processed element in its printed rule; the Lean development represents those evaluations, not an implementation cost model. The statement that its two final sets coincide is a separate milestone.

The source's main-text decreasing-returns definition has an overbroad quantifier on the added element. This development uses the equivalent lattice inequality given in the paper's footnote, which permits nonmonotone functions. The proof of Lemma II.1 also has a set-index slip, and the proof of Theorem I.2 prints $F$ for $f$ in one display; neither slip is copied into a formal statement. The one-step inequality (3) is stated for any nested pair with the processed element in $Y\setminus X$, a generalization of the conditioned reachable states in the paper. Contributions proving the endpoint invariant, conditional inequality, one-step expected estimate, and final bound are all within scope.

Selected references

• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, Proceedings of the 53rd IEEE Symposium on Foundations of Computer Science, 2012. FOCS version used here.
• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5), 2015. DOI: 10.1137/130929205. The cited statement indices above refer to the FOCS version.

Motivation

Discounted dynamic programming with bounded cost per stage is the standard setting in which infinite-horizon sequential decision problems are well posed: the optimal cost exists, satisfies Bellman's equation, and can be computed by iterating the DP operator. Shapley proved this for stochastic games in 1953 (Shapley 1953), Blackwell for discounted Markov decision processes in 1965 (Blackwell 1965), and Denardo observed in 1967 that the arguments use only two properties of the DP operator: monotonicity and contraction in the supremum norm (Denardo 1967). Bertsekas (1975, 1977) and Bertsekas and Shreve (1978) turned this observation into an abstract dynamic programming framework, in which a single mapping $H$ encodes stochastic, deterministic, minimax and multiplicative-cost problems at once (Bertsekas 1977).

Chapter 4 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case, is the contraction part of that framework. Its results are the abstract form of what every course on Markov decision processes proves for the discounted case, and they are what later work on abstract DP (Bertsekas, Abstract Dynamic Programming, 2022) and on robust and regularized MDPs builds on.

Setting

A model consists of a state space $S$, a control space $C$, a nonempty constraint set $U(x)\subseteq C$ for each $x\in S$, a mapping $H:S\times C\times F\to[-\infty,\infty]$, where $F$ is the set of functions $S\to[-\infty,\infty]$, and a function $J_0\in F$ with $J_0>-\infty$. $H$ is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$.

A selector is a function $\mu:S\to C$ with $\mu(x)\in U(x)$; $M$ is the set of selectors, and a policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ in $M$. The operators are

The cost of $\pi$ is $J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(J_0)(x)$, the optimal cost is $J^*(x)=\inf_{\pi}J_\pi(x)$, and $J_\mu$ is the cost of the stationary policy $(\mu,\mu,\dots)$.

$B$ is the Banach space of bounded real functions on $S$ with $\|J\|=\sup_x|J(x)|$. Assumption C asks for a closed set $\bar B\subseteq B$ containing $J_0$ and invariant under $T$ and every $T_\mu$; that every limit defining $J_\pi$ exist and be real; and that for some integer $m\ge1$ and scalars $0<\rho<1$, $\alpha>0$,

Formalization targets

Goal: Proposition 4.2

Under Assumption C,

$T(J')\le J'$ implies $J^*\le J'$ and $J'\le T(J')$ implies $J'\le J^*$ for $J'\in\bar B$; each $J_\mu$ is the unique fixed point of $T_\mu$ in $\bar B$; and for every $J\in\bar B$

The statement carries no constants beyond those of Assumption C.

Milestones

• Fixed Point Theorem (p. 55): an $m$-step contraction of a nonempty closed subset of a Banach space has a unique fixed point, which attracts every orbit.
• Proposition 4.1 (p. 53): $J_\pi$ does not depend on the terminal function in $\bar B$; $\inf_\pi(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)=T^N(J)$; $T^m$ and $T_\mu^m$ are $\rho$-contractions on $\bar B$.
• Proposition 4.3 (p. 56): $(\mu^*,\mu^*,\dots)$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$; pointwise optimal policies yield a stationary optimal one; stationary $\varepsilon$-optimal policies exist.
• Proposition 4.4 (p. 57): compactness of the sets $\{u\in U(x)\mid H[x,u,T^k(\bar J)]\le\lambda\}$ gives policies attaining the DP infimum, and their accumulation points are optimal stationary policies.
• Proposition 4.11 (p. 69): the discounted minimax model with $0\le g\le b$ and $\alpha<1$ satisfies Assumption C with $\bar B=B$, $m=1$, $\rho=\alpha$.

Further result

• Proposition 4.5 (p. 59), a draft theorem of this mission that is not a milestone: the error bound $J^*\le J_\mu\le J^*+(2\alpha\varepsilon_1+\varepsilon_2)(1+\alpha+\cdots+\alpha^{m-1})/(1-\rho)$.

Significance

Proposition 4.2 is the existence-and-uniqueness theorem for Bellman's equation in the contraction regime, together with the convergence of value iteration from an arbitrary start in $\bar B$. Propositions 4.3 to 4.5 turn it into statements about policies: when a stationary optimal policy exists, how one is found from the DP algorithm, and how much is lost when Bellman's equation is solved only approximately. Proposition 4.11 shows the assumption is met by a concrete class of problems, discounted minimax control, and so certifies that the abstract theorems are not vacuous.

The results are classical and have been proved in print since 1978; none of them is open. What this mission adds is a machine-checked version of the abstract theory itself, rather than of a single model. Mathlib has the Banach fixed point theorem for a contracting map of a complete space (ContractingWith) and a lemma for contracting iterates, but not the version on a closed subset with norm convergence of every orbit, and nothing on abstract DP. The platform has proved the finite-state discounted case for a concrete model (BertsekasDP.discounted_main_theorem); the abstract statements here cover infinite state spaces, minimax problems and $m$-step contractions, and are reused by the later missions of this series (generalized models, Chapter 6) and by papers that cite the book.

Difficulty

The first idea is to apply the contraction mapping principle to $T$ and read off $J^*$ as its fixed point. That gives a fixed point of $T$ but says nothing about $J^*$, which is defined as an infimum over all, generally nonstationary, policies of limits of compositions. The identification of the fixed point with $J^*$ is the content of the proposition, and it is where the Lipschitz condition (2) on all of $B$, not only on $\bar B$, enters.

Two further features block a direct appeal to Mathlib. The contraction is only $m$-step, so neither $T$ nor $T_\mu$ need be a contraction. And $H$ takes extended-real values, so every passage between $F$ and the Banach space $B$ must be justified by the invariance of $\bar B$.

Formalization scope

The state and control spaces are arbitrary types. $F$ is S → EReal; $B$ is Mathlib's lp (fun _ : S => ℝ) ⊤, whose norm is the supremum norm, and toF embeds $B$ into $F$. $\bar B$ is an arbitrary closed subset of $B$, not $B$ itself, and uniqueness of fixed points is asserted within $\bar B$. Policies are sequences ℕ → M; $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ applies $T_{\mu_{N-1}}$ first. $J_\pi$ is the pointwise limit (limUnder), which exists and is real under Assumption C; $J^*$ is the infimum over all policies.

The book computes in $[-\infty,\infty]$ with $\infty-\infty=\infty$, whereas Mathlib's EReal has $\bot+\top=\bot$. No statement adds infinities of opposite sign. A norm bound $\|J-J'\|\le c$ between functions of $F$ is the predicate SupDistLe: both functions are real at every point and differ by at most $c$, which is what the bound means under the book's arithmetic. Condition (2) is imposed on all of $B$, as on p. 53. The scalars $m,\rho,\alpha$ of Assumption C are explicit parameters, so the constant of Proposition 4.5 is the book's exact expression. The Fixed Point Theorem assumes $\bar B$ nonempty, which the page leaves implicit and without which the statement is false.

Defining $J^*$ as the fixed point of $T$, or replacing it by the infimum over stationary policies, would make the goal trivial. Neither is done here: $J^*$ is the infimum of the policy costs, exactly as in Eq. (8) of Chapter 2.

A complete development needs the $m$-step fixed point theorem on closed subsets of a Banach space, which can be reused well beyond dynamic programming; the elementary calculus of SupDistLe and of the embedding of $B$ into S → EReal; and the monotone-operator inequalities of Section 2.1. Contributions of any of these, or alternative proofs of the milestones, are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific reprint 1996, Chapter 4. http://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977) 438–464. https://doi.org/10.1137/0315031
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9 (1967) 165–177. https://doi.org/10.1137/1009030
• D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
• L. S. Shapley, Stochastic games, Proc. Natl. Acad. Sci. USA 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific 2022. https://web.mit.edu/dimitrib/www/abstractdp_MIT.html

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

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

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,

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$,

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.