Operations Research

Motivation

One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in $(0,1)$. It is the model behind cutting stock (cutting rolls of paper or steel to ordered widths), memory and file allocation, and batch scheduling on identical machines, and it is NP-hard. Its algorithmic study is therefore about approximation: how close to the optimum a polynomial-time algorithm can guarantee to come.

• 1961–1963: Gilmore and Gomory introduce the configuration linear program for cutting stock and solve it by column generation (Gilmore–Gomory 1961).
• 1974: Johnson, Demers, Ullman, Garey and Graham analyse First Fit and related heuristics, with asymptotic ratio $17/10$ and $11/9$ (Johnson et al. 1974).
• 1981: Fernandez de la Vega and Lueker give the first asymptotic approximation scheme, packing within $(1+\varepsilon)\,OPT(I) + 1$ bins in time linear in $n$ for fixed $\varepsilon$, using elimination of small pieces and linear grouping (Fernandez de la Vega–Lueker 1981).
• 1982: Karmarkar and Karp replace the enumeration of configurations by an approximate solution of the configuration LP and a rounding step, obtaining an additive term polynomial in $1/\varepsilon$ (this mission), and, with geometric grouping, $OPT(I) + O(\log^2 OPT(I))$ (Karmarkar–Karp 1982).
• 2013–2017: Rothvoß and then Hoberg–Rothvoß improve the additive term to $O(\log OPT \cdot \log\log OPT)$ and $O(\log OPT)$ (Hoberg–Rothvoß 2017).

Setting

An instance $I$ is a finite multiset of piece sizes, each in the open interval $(0,1)$. Write $n(I)$ for the number of pieces, $m(I)$ for the number of distinct sizes, and $SIZE(I)$ for the sum of all sizes. A packing of $I$ is a finite multiset of bins, each a multiset of sizes, whose union is exactly $I$ and in which every bin has total size at most $1$. Its cost is the number of bins, and $OPT(I)$ is the minimum cost.

A configuration of $I$ is a nonempty multiset of sizes occurring in $I$ with total at most $1$. With $b_t$ the number of pieces of size $t$ and $a_{tc}$ the number of occurrences of $t$ in configuration $c$, the fractional bin-packing problem is the linear program

$$\min\ \mathbf 1\cdot x\quad\text{s.t.}\quad x\ge 0,\qquad \sum_c a_{tc}x_c \ge b_t\ \ \text{for every size } t,$$

whose optimal value is $LIN(I)$. A basic feasible solution is an extreme point of its feasible region.

For instances $I,J$, write $I\le J$ if there is a one-to-one map $f$ from the pieces of $I$ into the pieces of $J$ with $x\le f(x)$. Linear grouping with parameter $k$ sorts $I$ non-increasingly, cuts it into groups $G_1,\dots,G_q$ of $k$ consecutive pieces (the last possibly shorter), rounds every piece of $G_i$ up to the largest size of $G_i$ to get $G_i'$, and outputs $J = \bigcup_{i\ge 2} G_i'$ and $J' = G_1$.

ALGORITHM 1 takes $I$ and $\varepsilon>0$: (1) discard the pieces of size $\le \max(1/n(I), \varepsilon/2)$, leaving $J$; (2) apply linear grouping to $J$ with $k = \lceil n(J)\varepsilon^2\rceil$, giving $K$ and $K'$; (3) put each piece of $K'$ in its own bin; (4) obtain from a Fractional Bin-Packing subroutine a basic feasible solution $x$ of the LP of $K$ with $\mathbf 1\cdot x\le LIN(K)+1$; (5) round $x$ to a packing of $K$ with at most $\mathbf 1\cdot x + (m(K)+1)/2$ bins; (6) shrink the pieces back to obtain a packing of $J$; (7) insert the discarded pieces, opening a new bin only when a piece fits nowhere. $A(I)$ is the cost of the resulting packing.

Formalization targets

Goal: Theorem 3, as its proof establishes it

$$A(I) \le (1+2\varepsilon)\,OPT(I) + \frac{1}{2\varepsilon^2} + 3 \qquad\text{for every } \varepsilon>0,\ \text{every instance } I,\ \text{every run of ALGORITHM 1.}$$

The additive term depends on $\varepsilon$ only, so ALGORITHM 1 is an asymptotic approximation scheme. The paper prints the factor $1+\varepsilon$, which fails for ALGORITHM 1 as printed (see Formalization scope); running the algorithm with $\varepsilon/2$ gives the paper's main result (4), $A(I)\le(1+\varepsilon)OPT(I)+O(\varepsilon^{-2})$, stated as a separate corollary with the explicit term $2/\varepsilon^2+3$.

Milestones

1. Lemma 1: $OPT(I)\le 2\,SIZE(I)+1$.
2. Lemma 2: $SIZE(I)\le LIN(I)\le OPT(I)\le LIN(I)+\frac{m(I)+1}{2}$.
3. Corollary 1: every basic feasible solution $x$ can be rounded to a packing of cost $\le \mathbf 1\cdot x + \frac{m(I)+1}{2}$.
4. Lemma 3: inserting pieces of size $\le g/2$ last, with new bins only when necessary, costs at most $\max(A, (1+g)\,OPT(I)+1)$.
5. Monotonicity: $I\le J$ implies $OPT$, $LIN$ and $SIZE$ do not decrease.
6. Lemma 4: linear grouping loses at most $k$ in $OPT$, $LIN$ and $SIZE$.
7. Proof steps (ii)–(iii) (corrected): $k\le 2\varepsilon\,OPT(I)+1$.
8. Proof step (iv): $m(K)\le 1/\varepsilon^2$.
9. Proof step (vii): $\mathbf 1\cdot x\le OPT(I)+1$.
10. Proof step (viii) (corrected): the packing of Step 6 has at most $(1+2\varepsilon)OPT(I)+\frac{1}{2\varepsilon^2}+\frac52$ bins.

Significance

The result showed that the configuration LP, of exponential size in general, can be used for a guaranteed approximation: its value is within $(m+1)/2$ of the integer optimum, and grouping reduces $m$ at small cost. The same template (eliminate small items, group, solve the configuration LP, round a basic solution, reinsert) underlies later schemes for bin packing, cutting stock, bin packing with cardinality constraints and scheduling, and the LP-based analysis is the starting point of the Rothvoß and Hoberg–Rothvoß improvements.

The theorems are proved in the literature; none of them has a machine-checked proof on the platform or, to our knowledge, in Mathlib. This mission produces a checked analysis of the algorithm, including a correction: the printed approximation factor is not valid for the algorithm as printed, and the checked statement records the factor its proof yields. The definitions (instances, packings, the configuration LP, basic solutions, the order $I\le J$, any-fit insertion) are reusable for the second mission of the series and for other bin-packing results.

Difficulty

The Lean statements are short, but several proofs need linear-programming structure that is not in Mathlib in this form. Lemma 2 and Corollary 1 use that an extreme point of $\{x\ge0,\ Ax\ge b\}$ has at most as many nonzero coordinates as there are rows of $A$; the configuration LP is indexed by a finite but implicitly described set of multisets. Monotonicity of $LIN$ under $I\le J$ ("clearly" in the paper) requires transporting a fractional solution across a piece-to-piece matching whose images are types, not pieces. The existence of a run requires an optimal basic feasible solution of the configuration LP. Lemma 3 concerns an insertion process with unrestricted order and bin choice, so its bound has to hold for every execution, not for one greedy rule.

Formalization scope

• Sizes are real numbers in the open interval $(0,1)$; the paper says "a rational number between 0 and 1". Real sizes generalize rational ones; the open interval is what the paper's arguments use.
• Instances are Multiset ℝ; packings are Multiset (Multiset ℝ) with join equal to the instance, bin loads at most $1$, empty bins allowed and counted. $OPT$ is a natural-number infimum over a set that is always nonempty.
• LP solutions are Multiset ℝ →₀ ℝ supported on configurations. $LIN$ is a real infimum over a set that is nonempty (singleton configurations) and bounded below by $0$. "Basic" is the extreme-point property; the bound on the number of nonzero coordinates is a consequence, not the definition.
• The Fractional Bin-Packing subroutine is modelled by its contract only (§5, p. 315): any basic feasible solution of cost at most $LIN(K)+1$. The ellipsoid method of §6 is not modelled.
• ALGORITHM 1 is a relation Alg1Run ε I P: $P$ is a possible output. Every open choice is quantified: the subroutine's output, the packing of Step 5 (any packing within the stated bound), the size reduction of Step 6 (bin by bin), and the insertion of Step 7 (any order, any fitting bin). The goal holds for every run, and a separate item states that a run exists, so the goal is not vacuous.
• The paper's $O(\cdot)$ in result (4) is replaced by the explicit $2/\varepsilon^2+3$.
• Corrected statements. The printed Theorem 3 bound $(1+\varepsilon)OPT(I)+\frac{1}{2\varepsilon^2}+3$ fails: for $\varepsilon=1/10$ and $19\,000$ pieces of size $0.051$, some run uses $1180$ bins while the bound is $1153$. The failing step is (ii), $SIZE(J)\ge\varepsilon\,n(J)$, since Step 1 discards only pieces $\le\varepsilon/2$. Steps (ii)–(iii) and (viii) are stated with $2\varepsilon$; step (iv) is stated as $m(K)\le 1/\varepsilon^2$ because its first link $m(K)\le n(K)/k$ fails when the last group is short.
• Running time (Theorem 3's first half, Corollary 1's time bound, the function $T$) is out of scope.
• Trivializations are ruled out: "some packing has at most the bound" is not the goal; the goal constrains every output of the algorithm, and the packing property of that output is part of its conclusion.

Proofs of any item are welcome; Lemma 2, Corollary 1 and the monotonicity display are the most reusable.

Selected references

• N. Karmarkar, R. M. Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd FOCS (SFCS 1982), IEEE, pp. 312–320. https://doi.org/10.1109/sfcs.1982.61
• W. Fernandez de la Vega, G. S. Lueker, Bin packing can be solved within 1+ε in linear time, Combinatorica 1 (1981) 349–355. https://doi.org/10.1007/BF02579456
• P. C. Gilmore, R. E. Gomory, A Linear Programming Approach to the Cutting-Stock Problem, Operations Research 9 (1961) 849–859. https://doi.org/10.1287/opre.9.6.849
• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM J. Comput. 3 (1974) 299–325. https://doi.org/10.1137/0203025
• R. Hoberg, T. Rothvoß, A Logarithmic Additive Integrality Gap for Bin Packing, Proc. SODA 2017, 2616–2625. https://doi.org/10.1137/1.9781611974782.172

Motivation

In a shared-memory multiprocessor, each processor keeps copies of memory blocks in its own cache, and all caches listen ("snoop") on a common bus. Every bus cycle spent keeping these copies consistent is a cycle not available for useful work, so the protocol that decides when a block is shared by several caches and when it is private to one cache directly controls bus traffic. The decision has to be made on-line, without knowing which processor will touch the block next.

Karlin, Manasse, Rudolph and Sleator (Algorithmica 1988) introduced competitive analysis for this problem and gave a deterministic algorithm with competitive ratio $2$, which is optimal among deterministic algorithms. Karlin, Manasse, McGeoch and Owicki (Algorithmica 1994) showed that randomization helps: against an oblivious adversary the optimal ratio for block snoopy caching is $e_p/(e_p-1)$, where $p$ is the cost of transferring a block. The same paper develops a general method for "nonuniform" problems, in which some state transitions are much more expensive than others, and the snoopy-caching result is its first application.

Setting

Fix $n$ processors and one memory block $B$ holding $p-1$ variables; transferring $B$ over the bus costs $p$ bus cycles. The block is in one of $n+1$ states: shared between all caches, or private to the cache of processor $i$.

A request is a read $\mathrm{R}_i$ or a write $\mathrm{W}_i$ by processor $i$. Moving from a private state to any other state costs $p$; moving from the shared state is free. A read $\mathrm{R}_i$ costs $0$ if $B$ is shared or private to $i$ and $+\infty$ otherwise. A write $\mathrm{W}_i$ costs $0$ if $B$ is private to $i$, $1$ if $B$ is shared (one bus cycle broadcasts the new value), and $+\infty$ otherwise.

Before request $j$ the system is in state $s_{j-1}$. A read is a look-ahead-one request: the algorithm may change state at the moment of the request, after seeing it. A write is a look-ahead-zero request: it is served in whatever state the system is in. After either kind, the algorithm may move again. The cost of a request is the cost of the move to the serving state, plus the task cost there, plus the cost of the move afterwards. Every write is preceded by a read to the same block, so in an admissible sequence each write $\mathrm{W}_i$ directly follows $\mathrm{R}_i$ or $\mathrm{W}_i$.

The off-line optimum $C_{opt}(s_0,\sigma)$ is the least total cost of serving $\sigma$ from the initial state $s_0$ with full knowledge of $\sigma$. A randomized on-line algorithm $A$ is a probability distribution over deterministic on-line algorithms; its expected cost on $\sigma$ is $\mathbf{E}C_A(\sigma)$. $A$ is $c$-competitive against an oblivious adversary from $s_0$ if there is a constant $a$ with

$$\mathbf{E}C_A(\sigma)\le c\cdot C_{opt}(s_0,\sigma)+a$$

for every admissible $\sigma$. Put

$$e_p=\left(1+\frac1p\right)^p .$$

Formalization targets

Goal: Theorem 4

For $n\ge 2$, $p\ge 1$ and every initial state $s_0$:

$$\Big(\forall A\ \forall c:\ A \text{ is } c\text{-competitive from } s_0 \Rightarrow c\ge \tfrac{e_p}{e_p-1}\Big)\ \wedge\ \exists A:\ A \text{ is } \tfrac{e_p}{e_p-1}\text{-competitive from } s_0 .$$

The two conjuncts are milestones of their own: the lower bound (Theorem 4, first claim) and attainment (Theorem 4, second claim).

The phase linear program (§3.2, pp. 552–554)

For $p\ge1$, real $\pi_1,\dots,\pi_{p+1}$ with $\pi_{p+1}=1$, and real $\alpha$ with

$$\pi_{k+1}p+\sum_{i=1}^{k}(1-\pi_i)\le\alpha k\qquad(k=0,\dots,p),$$

one has $\alpha\ge e_p/(e_p-1)$. Conversely, at $\alpha=e_p/(e_p-1)$ the choice $\pi_k=(\alpha-1)\big(((p+1)/p)^{k-1}-1\big)$ satisfies $\pi_{p+1}=1$, $0\le\pi_1\le\dots\le\pi_{p+1}$, and makes every constraint an equality.

Significance

The theorem settles the randomized competitive ratio of block snoopy caching exactly: $2$ at $p=1$, $9/5$ at $p=2$, decreasing to $e/(e-1)\approx1.582$ as $p\to\infty$, against the deterministic optimum $2$. The same ratio $e/(e-1)$ is the randomized optimum for the continuous ski-rental and spin-block problems treated later in the paper, and the snoopy-caching case is its discrete counterpart with ratio $e_p/(e_p-1)$. The phase-LP method used here recurs in the paper's two-server results.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of the snoopy-caching task system with look-ahead-zero requests, of randomized algorithms against an oblivious adversary with infinite task costs allowed, and of the off-line optimum, together with the exact optimal ratio. The platform's fractional ski-rental result (PrimalDualOnline.SkiRental.fractional_competitive) proves an $e_B/(e_B-1)$ bound for a different model: one deterministic fractional algorithm, with no lower bound over randomized algorithms. It is related work, not a special case.

Difficulty

The linear program is elementary. The gap is between the LP and the algorithms. The paper's lower bound reduces arbitrary randomized algorithms to phase-based ones, whose state distribution at the end of each phase agrees with the optimal algorithm's known state, and whose behaviour inside a phase depends only on the number of writes so far. This reduction (Theorems 1 and 3 of the paper, pp. 545–549) is where the argument is not routine. An algorithm may keep the block private to a processor that is not the active one, may randomize over histories rather than over phase lengths, and the off-line optimum is not a sum of per-phase costs at the ends of the sequence. The obvious approach, bounding a single adversarial phase, does not suffice, because an algorithm may pay more in one phase and recover it in the next; the additive constant $a$ and the infinite horizon have to be handled. For attainment, the mixture of threshold algorithms must be written as a genuine distribution over on-line algorithms, with the initial phase from a private state absorbed into the additive constant.

Formalization scope

Everything lives in the namespace NonuniformCompetitive.Snoopy. States are Option (Fin n) (none = shared). Costs are in ℝ≥0∞; $+\infty$ is a genuine outcome, so an algorithm that ever pays $+\infty$ with positive probability on an admissible sequence is not competitive. A deterministic on-line algorithm is a pair of functions of the request prefix (the state at the moment of the last request, and the state after it), with the look-ahead-zero rule as a field. Moves "immediately before" a request are made without knowledge of it and are recorded as moves after the previous request. A randomized algorithm is a probability space with a measurable cost on every sequence, and its expected cost is a lower Lebesgue integral. The off-line optimum is an infimum in ℝ≥0∞ over schedules starting in $s_0$; it is finite on admissible sequences.

Conventions added to the printed statement, all from the paper's setting: (i) $n\ge2$, since with one processor the block can stay private for free; (ii) one block, since the proof of Theorem 4 splits a multi-block system into independent blocks (p. 551); (iii) admissibility in the form "each write of $i$ directly follows a read or write of $i$", the reading of "every write is preceded by a read to the same block" that the proof uses; without it every algorithm is defeated by a write from a processor whose block copy was invalidated; (iv) $p\in\mathbb{N}$, $p\ge1$; (v) both claims from every initial state, with an additive constant depending on $n$, $p$, $s_0$.

The lower bound is over all randomized algorithms, not over phase-based or deterministic ones; a statement restricted to phase-based algorithms, or the LP alone in place of the goal, would not be Theorem 4. The LP variables are free, as in the paper.

Welcome contributions: a formal version of the phase reduction (Theorems 1 and 3 of the paper) for this task system, which is reusable for the paper's other nonuniform problems; the threshold algorithms and their mixture; and a proof that the off-line optimum decomposes by write runs up to a bounded error.

Selected references

• A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), 542–571. https://doi.org/10.1007/BF01189993
• A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3 (1988), 79–119. https://doi.org/10.1007/BF01762111
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.

Motivation

Models of learning in games, and discrete choice models in econometrics, describe an agent who does not always pick the best alternative. Two descriptions of such an agent are standard. In the additive random utility model (McFadden 1981; Anderson, de Palma and Thisse 1992) the agent maximizes payoffs perturbed by random shocks. In the deterministic perturbation model (Fudenberg and Levine 1998) the agent chooses a probability vector and pays a deterministic, strictly convex cost for it. The logit choice rule arises from both: from i.i.d. extreme-value shocks, and from the entropy cost $V(y) = \eta \sum_j y_j \ln y_j$.

Hofbauer and Sandholm (Econometrica 70 (2002)) show that the second description is general enough to cover the first for every shock distribution with a strictly positive density, not only for logit. Their analysis of stochastic fictitious play rests on this: the deterministic representation provides the perturbed payoff functions from which Lyapunov functions for the learning dynamics are built, for arbitrary noise. This mission formalizes that discrete choice theorem, Theorem 2.1 of the paper, together with the steps of its proof.

Setting

Fix $n \ge 1$ alternatives $A = \{1, \dots, n\}$ with base payoffs $\pi = (\pi_1, \dots, \pi_n) \in \mathbb{R}^n$. A random vector $\varepsilon = (\varepsilon_1, \dots, \varepsilon_n)$ has a strictly positive density $f : \mathbb{R}^n \to \mathbb{R}$, whose law does not depend on $\pi$. The agent chooses the alternative whose total payoff $\pi_j + \varepsilon_j$ is largest, which gives the choice probability function $C : \mathbb{R}^n \to \mathbb{R}^n$,

$$C_i(\pi) = P\big(\operatorname{argmax}_j\, \pi_j + \varepsilon_j = i\big).$$

The probability simplex is $\Delta A = \{x \in \mathbb{R}^n_+ : \sum_j x_j = 1\}$, with relative interior $\operatorname{int}(\Delta A)$ (all coordinates positive) and tangent space $\mathbb{R}^n_0 = \{z \in \mathbb{R}^n : \sum_j z_j = 0\}$.

A deterministic perturbation is a function $V : \operatorname{int}(\Delta A) \to \mathbb{R}$. Because $V$ lives on the relative interior, its gradient $\nabla V(y)$ is the vector of $\mathbb{R}^n_0$ with $V(y + hz) = V(y) + (\nabla V(y) \cdot z) h + o(h)$ for all $z \in \mathbb{R}^n_0$, and its second derivative $D^2 V(y)$ is a quadratic form on $\mathbb{R}^n_0$. The perturbation is admissible if $V$ is twice continuously differentiable along the simplex, $D^2V(y)$ is positive definite on $\mathbb{R}^n_0$ for every $y$, and $\|\nabla V(y)\| \to \infty$ as $y$ approaches the boundary of $\Delta A$.

Formalization targets

Goal: Theorem 2.1

If $\varepsilon$ has a strictly positive density and $C$ is continuously differentiable, then there is an admissible $V$ such that, for every $\pi \in \mathbb{R}^n$,

$$C(\pi) = \operatorname*{argmax}_{y \in \operatorname{int}(\Delta A)} \big( y \cdot \pi - V(y) \big),$$

with a unique maximizer. The perturbation $V$ is one function serving all payoff vectors at once.

Milestones

The milestones are the steps of the paper's proof (pp. 5–7), in order:

1. Eq. (4). $DC(\pi)$ is symmetric, $\partial C_i/\partial \pi_j = \partial C_j / \partial \pi_i$, and its off-diagonal terms are strictly negative.
2. Eq. (5). $\partial C_i/\partial \pi_i = -\sum_{j \ne i} \partial C_j/\partial \pi_i$, and $DC(\pi)\mathbf{1} = 0$.
3. Eq. (6). $z \cdot DC(\pi) z > 0$ whenever $z$ is not proportional to $\mathbf{1}$.
4. Shift invariance and injectivity. $C(\pi + c\mathbf{1}) = C(\pi)$, and $C$ is one-to-one on $\mathbb{R}^n_0$.
5. Range observation. If the payoffs $\pi_j$, $j \in J$, stay bounded while the others tend to $+\infty$, then $C_j(\pi) \to 0$ for $j \in J$.
6. Convex potential. There is $W : \mathbb{R}^n \to \mathbb{R}$ with $\nabla W \equiv C$, strictly convex on $\mathbb{R}^n_0$.
7. Range. $C$ takes values in $\operatorname{int}(\Delta A)$, and $C(\mathbb{R}^n_0) = \operatorname{int}(\Delta A)$.

Significance

The result. Theorem 2.1 lets any smooth additive random utility model be replaced by an optimizing agent with a strictly convex, boundary-repelling cost. In the paper this is the bridge from the perturbed best response dynamic to a deterministic perturbed-payoff formulation, which yields Lyapunov functions for zero-sum games, games with an interior evolutionarily stable strategy, and potential games (§4 of the paper), and so the almost sure convergence of stochastic fictitious play under general noise (Theorem 6.1). Without it those convergence results would be restricted to noise distributions whose choice rule has a known deterministic representation, essentially logit. The paper also shows (Proposition 2.2) that the converse fails when $n \ge 4$: deterministic perturbations generate strictly more choice rules than random utility.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it is known. The mission asks for a formal proof of Theorem 2.1 and the seven steps above. Along the way it requires symmetric Jacobians of probability integrals, a gradient-field potential on $\mathbb{R}^n$, and the Legendre transform of a strictly convex function restricted to a hyperplane. None of these is currently packaged in Mathlib in the needed form.

Difficulty

The obvious argument is to take $V$ to be the Legendre transform of the potential $W(\pi) = \mathbb{E}\max_j(\pi_j + \varepsilon_j)$ and read off the first-order conditions. Three steps of that argument are not routine. First, the derivative identity (4) is a change of variables inside an $(n-1)$-fold integral over a moving region, and its strict sign needs the density to be positive on the relevant hyperplane sections. Second, the Legendre transform is well defined on all of $\operatorname{int}(\Delta A)$ only if $C$ maps $\mathbb{R}^n_0$ onto the whole open simplex. The paper takes this from Theorem 26.5 of Rockafellar (1970), whose hypotheses (essential smoothness, strict convexity, identification of the conjugate's domain) must be checked here. Third, positive definiteness of $D^2V$ and the gradient blow-up at the boundary are statements about the inverse of $C$ on $\mathbb{R}^n_0$. They need an inverse function argument on a subspace and a properness argument, not only pointwise convexity.

Verifying that $C(\pi)$ satisfies the first-order condition for one fixed $\pi$ does not suffice: the goal requires a single $V$ for all $\pi$, and a unique maximizer.

Formalization scope

Alternatives are indexed by Fin n with $n \ge 1$; vectors are Fin n → ℝ with its sup norm. The density is a real function $f$ that is continuous, strictly positive at every point, and has $\int f = 1$; the law of $\varepsilon$ is Lebesgue measure weighted by $f$. The paper's formula (4) evaluates $f$ on hyperplanes, which is meaningful for a continuous $f$. Without continuity the theorem can fail: a density that is positive everywhere but tends to zero near a hyperplane can make $C$ continuously differentiable with a vanishing off-diagonal derivative, and then no twice differentiable $V$ represents $C$. Continuous differentiability of $C$ is a hypothesis, as in the paper, stated as ContDiff ℝ 1 of the map $\pi \mapsto C(\pi)$. The event "$i$ is the argmax" uses strict inequalities; ties have probability zero.

$V$ is a function on $\mathbb{R}^n$ of which only the values on $\operatorname{int}(\Delta A)$ enter. Its smoothness and second derivative are taken in the chart $z \mapsto V(y + z)$ on the subspace $\mathbb{R}^n_0$. $\nabla V(y)$ is the tangent gradient of the paper's footnote 3, not an ambient gradient of an extension. The boundary blow-up is stated uniformly: for every $M$ there is $\delta > 0$ such that every tangent gradient at an interior point with some coordinate below $\delta$ has norm above $M$.

The goal cannot be satisfied trivially. $V$ must be chosen before $\pi$, all three admissibility conditions are part of the definition, and the maximizer must be unique. Weakening any of these (a $V$ depending on $\pi$, a $V$ without second derivatives, a non-strict maximum) changes the theorem.

Reusable infrastructure: differentiation of choice probabilities under a density, potentials of symmetric $C^1$ vector fields on $\mathbb{R}^n$, and Legendre duality for strictly convex functions on a subspace. Contributions of any of these as separate lemmas are welcome, as are alternative proofs of the milestones, for instance obtaining the potential directly as $\mathbb{E}\max_j(\pi_j + \varepsilon_j)$.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376 (theorem numbers and pages here follow the authors' manuscript of February 21, 2002).
• D. Fudenberg and D. K. Levine, The Theory of Learning in Games, MIT Press, 1998.
• S. P. Anderson, A. de Palma and J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.
• D. McFadden, Econometric Models of Probabilistic Choice, in C. F. Manski and D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

This mission continues chapter 11's account of the M♮-concave/M♮-convex exchange-economy model begun in mission 14-economic-equilibrium, placing seven of that chunk's own results that were previously left out-of-cone: the two gross-substitutes-style characterizations of M♮-concavity (§11.3), the transfer theorem that lifts an equilibrium of the continuous relaxation to one for indivisible commodities (§11.4), and the explicit polyhedral description of the equilibrium price set together with its feasibility criterion (§11.5).

Setting

Mission 14-economic-equilibrium built the exchange-economy vocabulary this mission redeclares in full (UDom, ArgMaxBot/ArgMinTop, PriceShift/PriceShiftConvex, DemandSet/SupplySet, IsEquilibrium, MNaturalConcave, IsMNaturalConvexSet, the concave/convex closures ConcaveClosureR/ConvexClosureR and their continuous analogues ContDemandSet/ContSupplySet/ IsContEquilibrium) and placed the qualitative structural theorems (Theorems 11.1-11.3, 11.4, 11.16-11.18, 11.23-11.24). This mission adds the gross-substitutes axioms (−M♮-GS[Z], the price-monotonicity property NegGS, and −M♮-SWGS[Z], its one-price-at-a-time refinement NegSWGS), the M♮-convex-set transfer machinery connecting a continuous equilibrium to a discrete one, and the equilibrium price polyhedron built from the three bound families ℓ(j), u(j), u(i,j) (Eqs. (11.40)-(11.42)) that make Theorem 11.16's qualitative L♮-convex-polyhedron fact concrete and linear-programming-checkable.

Formalization targets

Goal: The equilibrium price set is the explicit L♮-convex polyhedron (11.43) (Theorem 11.21)

For a fixed allocation (x,y), the set P* of all equilibrium price vectors is an L♮-convex polyhedron and equals the polyhedron cut out by max{0,ℓ(j)} ≤ p(j) ≤ u(j) and p(j)-p(i) ≤ u(i,j). Chosen as goal: it is the sharpest structural result of chapter 11's computation section, upgrading Theorem 11.16's qualitative fact to a concrete description, and is what Theorem 11.22 (also placed) builds on directly.

Supporting structural targets

Theorem 11.5 and Theorem 11.6 characterize M♮-concavity via the gross-substitutes and stepwise gross-substitutes properties, completing chapter 11's suite of M♮-concavity characterizations begun with Theorem 11.4 (mission 14). Theorem 11.15 is the general transfer theorem (continuous equilibrium ⟹ discrete equilibrium) that mission 14's own Theorem 11.14 invokes as a special case. Theorem 11.22 gives the feasibility criterion for the existence of an equilibrium price vector, the mission's second theorem built on the equilibrium price polyhedron.

Significance

Together with mission 14-economic-equilibrium, this mission completes the book's account of how M♮-concavity/convexity — a purely combinatorial exchange condition — reproduces, and sharpens, the classical gross-substitutes theory of competitive equilibrium for economies with indivisible goods: existence transfers from the continuous relaxation, and the equilibrium price set itself has a description exact enough to reduce to a linear feasibility question. None of these results are open — they are Murota's own account (attributed in the book's own notes to Danilov-Koshevoy- Lang and Murota-Tamura for the gross-substitutes theorems, and to Murota-Tamura for the equilibrium price polyhedron); this mission contributes a faithful, machine-checked formal statement of each (see Formalization scope).

Difficulty

Two of this chunk's seven BRIEF.md results are not drafted this pass, for a disclosed time- budget reason rather than any faithfulness failure: Proposition 11.19 and Theorem 11.20 require the H,L-indexed bipartite MSFP2 flow-network vocabulary (separate vertex sets V+_e, V+_l, V-_h, an M-convex/M-concave-combining flow objective) that neither this mission nor mission 14 builds, and building it in proportion to placing exactly these two results was judged disproportionate to the remaining time in this pass; see HARD.md and STATUS.md. This is explicitly not a hard exclusion — both results are well-posed and provable from the book's own complete proofs — and is recorded as an honest scope limitation for a future pass. Theorem 11.22's own trailing algorithmic remark (that equilibrium prices can be found via a shortest-path computation, yielding a polynomial-time equilibrium-checking algorithm) is a computational/ complexity claim outside this series' propositional-formalization methodology and is omitted; the mathematical "iff feasibility" content is placed in full. See HARD.md.

Formalization scope

Ground set K is a Fintype with DecidableEq; consumer/producer index sets H, L are Fintypes (Nonempty where the price-bound formulas (11.40)-(11.42) need a nonempty sup'/inf' range). All base vocabulary is redeclared fresh from mission 14-economic-equilibrium's own definitions, since this draft cannot import that sibling mission. The gross-substitutes axioms are formalized directly from their defining inequalities (Eqs. preceding (11.19) and following, and p.331); the equilibrium price polyhedron's bound families ℓ(j)/u(j)/u(i,j) are formalized literally from Eqs. (11.40)-(11.42), extracting each WithBot ℝ/WithTop ℝ operand to ℝ before subtracting (since WithBot ℝ carries no subtraction instance). Two results (Proposition 11.19, Theorem 11.20) are not drafted this pass for the disclosed time-budget reason above; one result (Theorem 11.22's trailing algorithmic remark) is scoped out as computational content. Contributions completing any of the five sorrys, or building the MSFP2 vocabulary to place Proposition 11.19/Theorem 11.20 in a follow-up mission, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• V. Danilov, G. Koshevoy, K. Murota, "Discrete convexity and equilibria in economies with indivisible goods and money," Mathematical Social Sciences, 41 (2001), pp. 251-273 [33] (origin of the gross-substitutes characterization, Theorem 11.6).
• K. Murota, A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [160] (origin of the equilibrium price polyhedron, Theorems 11.20-11.22).

Motivation

Two strategic levers shape the balance of power between a manufacturer and the retailer that resells its product. The first is strategic inventory: a buyer that orders more than it sells today, and carries the surplus into the next period, weakens the supplier's leverage over tomorrow's wholesale price. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period channel the buyer withholds inventory exactly when its unit holding cost is below $\alpha/4$. The second is supplier encroachment: a supplier that can sell directly to consumers competes with its own buyer. Arya, Mittendorf and Sappington (Marketing Science 2007) showed that the threat of encroachment can lower wholesale prices and benefit both parties.

Guan, Gurnani, Geng and Luo, Strategic Inventory and Supplier Encroachment (MSOM 2019), combine the two levers in one game. Their headline qualitative finding is Proposition 4.2. When the supplier's direct channel is costly, but not quite too costly to use, the buyer keeps withholding inventory at every finite holding cost. This contrasts with the $\alpha/4$ cutoff of Anand et al. This mission formalizes that proposition, together with the equilibrium characterizations of Appendix A on which it rests.

Setting

There is one supplier and one buyer, two periods, deterministic demand and complete information. In each period the market price is $p = \alpha - q$, where $q$ is the total quantity sold in that period and $\alpha > 0$ is the demand intercept. The buyer pays a per-unit holding cost $h \ge 0$ on inventory carried into period 2. The supplier pays a per-unit direct selling cost $s \ge 0$. All other costs and the salvage value are zero. The moves are:

1. The supplier quotes a wholesale price $w_1 \ge 0$.
2. The buyer orders $Q_1$ and sells $q_1$, with $0 \le q_1 \le Q_1$. It carries the inventory $I = Q_1 - q_1$ into period 2.
3. The supplier quotes $w_2 \ge 0$.
4. The buyer orders $Q_2 \ge 0$ and sells $q_2$, with $0 \le q_2 \le I + Q_2$.
5. Having observed everything, the supplier sells $q_s \ge 0$ directly. The period-2 price is $\alpha - q_2 - q_s$.

The total profits are

$$\Pi_b = (\alpha - q_1)q_1 - w_1 Q_1 - hI + (\alpha - q_2 - q_s)q_2 - w_2 Q_2, \qquad \Pi_s = w_1 Q_1 + w_2 Q_2 + (\alpha - q_2 - q_s - s)q_s .$$

A strategy profile assigns an action to every history at which a player moves. It is a subgame perfect equilibrium (SPE) if, at every feasible history, the mover's prescribed action is feasible and no feasible alternative, followed by the profile afterwards, raises the mover's total profit. The equilibrium path is the outcome the profile generates; the equilibrium inventory is $I$ on that path. Following the paper (§4), the goal theorem sets $\alpha = 1$.

Formalization targets

Goal: Proposition 4.2

With $\alpha = 1$,

$$\forall h > 0\ \ \exists \epsilon > 0\ \ \forall s \in \big(\tfrac56 - \epsilon, \tfrac56\big):\quad \text{an SPE exists, and every SPE has } I > 0 \text{ and } hI < \tfrac{11}{72}.$$

Here $\epsilon$ may depend on $h$, and the bound $11/72$ applies at the same $(h, s)$.

Milestones, in attack order

1. Stage-3 best response (§3.1.1): in every SPE, the supplier sells $q_s = (\alpha - q_2 - s)^+/2$ at every history.
2. Eq. (1) (§3.1.1): with no inventory, the buyer's period-2 quantity is the four-branch function $q_b(w)$ of the period-2 wholesale price $w$.
3. Proposition 4.1, existence half: an SPE exists for every $h \ge 0$ and $s \ge 0$.
4. Region 8 (Tables A.1 and A.4): for $h < h_{11}$ with $s_3 \le s < 5\alpha/6$, or for $h < \alpha/4$ with $5\alpha/6 \le s < \alpha$, every SPE has $I = 5(\alpha - 4h)/34$ and the path of Table A.4.
5. Region 7, second part (Tables A.1 and A.3): for $h_{11} < h < h_{10}$ and $s_3 \le s < 5\alpha/6$, every SPE has $I = I^* = (2\alpha - 3s + x)/2$ and the path of Table A.3.
6. Region 10, second part (Tables A.1 and A.4): for $h > h_7$ and $2\alpha/3 < s < 5\alpha/6$, every SPE has $I = 0$.

The thresholds $x$, $s_3$, $h_7$, $h_{10}$, $h_{11}$ are explicit algebraic functions of $s$, given in Appendix A.

Significance

Proposition 4.2 separates the combined model from the two models it merges. Without a direct channel, inventory disappears once $h \ge \alpha/4$. With a direct channel, a threat of encroachment that is only barely credible keeps inventory alive at every holding cost. The total holding cost nevertheless stays below a constant, because the inventory shrinks as $h$ grows. Milestone 6 shows the flip side: for a fixed $s < 5\alpha/6$, a large enough $h$ removes the inventory. This is why the window $\epsilon$ must depend on $h$.

The paper's proofs are in an online appendix that is not reproduced in the article. The article itself gives the equilibrium only as tables. A formal development would supply a checked backward-induction proof of those tables in the regions near $s = 5\alpha/6$. It would also give a machine-checked SPE framework for multi-stage pricing-and-quantity games in supply chains, which none of the following exists for: Stackelberg pricing, sequential quantity competition, or dual-channel encroachment. No part of this paper has been formalized before.

Difficulty

The equilibrium is found by backward induction through five stages. Each stage's value function is only piecewise smooth, because the supplier's direct-channel response $(\cdot)^+$ switches on and off. As a result the buyer's period-2 profit has kinks, the supplier's period-2 profit as a function of $I$ has several local maxima, and the period-1 problems must compare branches whose boundaries are the irrational thresholds of Appendix A. The obvious approach, solving the first-order conditions stage by stage, fails at the kinks. At some region boundaries it also misses that the supplier is indifferent between two first-period prices, which makes the equilibrium path change discontinuously. Proposition 4.2 then needs uniform control of $h_7$, $h_{10}$ and $h_{11}$ as $s \uparrow 5/6$, where the denominator $3s - 2 - x$ of $h_7$ tends to $0$.

Formalization scope

• Representation. Strategies are functions of the full history, not Markov rules in $I$. IsSPE imposes optimality at every feasible history, including off-path ones. All actions are real numbers; wholesale prices and quantities are nonnegative, with $q_1 \le Q_1$ and $q_2 \le I + Q_2$.
• Normalization. The goal instantiates $\alpha = 1$ as the paper does from §4 on. The milestones keep a general $\alpha > 0$.
• Uniqueness is not stated. Proposition 4.1's uniqueness claim is false for strategy profiles: after the off-path price $w_2 = 0$, every order $Q_2 \ge q_2 - I$ is optimal. The goal and the region milestones therefore quantify over every SPE and carry existence as a separate conjunct.
• Corrected hypotheses.
  • The printed $s_3 = (\sqrt{(37 - 3\sqrt{65})/34} + 4/6)\alpha \approx 1.28\alpha$ is replaced by $(\sqrt{37 - 3\sqrt{65}}/34 + 4/6)\alpha \approx 0.772\alpha$, which matches the paper's "≈0.77".
  • Eq. (1) excludes the corner $w = 0$, $s < \alpha/3$, where its second branch is wrong.
  • Region 8 drops its boundary $h = h_{11}$ and Region 7 drops $h = h_{10}$, because the equilibrium path switches there and need not be unique.
• Ruled-out trivialization. The inventory in the goal is the inventory on the path of an SPE of the game above. It is not the closed form $5(1 - 4h)/34$ or $I^*$ from the tables, and the regional characterization is not a hypothesis. Otherwise the goal would reduce to algebra about the thresholds.
• Infrastructure and contributions. The definitions Game, IsSPE and Thresholds are shared by every statement. Welcome contributions include:
  • lemmas on maximizing concave piecewise-quadratic functions on half-lines;
  • a reusable backward-induction lemma for finite-stage games with real action sets;
  • interval-arithmetic facts about $x$, $h_7$, $h_{10}$ and $h_{11}$ near $s = 5/6$;
  • proofs of the paper's other regions.

Selected references

• T. Guan, H. Gurnani, X. Geng, Y. Luo, Strategic Inventory and Supplier Encroachment, Manufacturing & Service Operations Management 21(3):536–555, 2019. https://doi.org/10.1287/msom.2018.0705
• K. Anand, R. Anupindi, Y. Bassok, Strategic Inventories in Vertical Contracts, Management Science 54(10):1792–1804, 2008. https://doi.org/10.1287/mnsc.1080.0894
• A. Arya, B. Mittendorf, D. Sappington, The Bright Side of Supplier Encroachment, Marketing Science 26(5):651–659, 2007. https://doi.org/10.1287/mksc.1070.0280

Motivation

Chapter 9 is where discrete convex analysis meets classical network flow theory: the minimum cost flow problem's three hallmark properties — an optimality criterion by potentials, an optimality criterion by negative cycles, and integrality of optimal solutions — are shown to survive, in a precise and increasingly general form, first for arbitrary polyhedral convex costs (MCFP3), then for the M-convex submodular flow problem (MSFP2/MSFP3), the chapter's own combinatorial generalization of the classical problem. This mission places the potential criterion (Theorem 9.4) and its cascade of six corollaries and generalizations, the block of results this book's own text uses to carry every other result in the chapter.

Setting

A digraph G = (V,A) with tail/head maps ∂⁺,∂⁻ : A → V. A flow ξ : A → R has boundary ∂ξ(v) = Σ{ξ(a) : ∂⁺a=v} − Σ{ξ(a) : ∂⁻a=v}. A potential p : V → R has coboundary δp(a) = p(∂⁺a) − p(∂⁻a). The minimum cost flow problem MCFP3 minimizes Γ₃(ξ) = Σₐ fₐ(ξ(a)) + f(∂ξ) over flows, for polyhedral convex arc costs fₐ : R → R∪{+∞} and boundary cost f : Rⱽ → R∪{+∞}; MCFP0 is its linear-cost, fixed-supply special case. The M-convex submodular flow problem MSFP3 is MCFP3 with f additionally M-convex; MSFP2 is its linear-arc-cost special case.

Formalization targets

Goal: The potential criterion for MCFP3 (Theorem 9.4)

For a feasible flow ξ, ξ is optimal for MCFP3 iff there is a potential p with ξ(a) a minimizer of the reduced arc cost fₐ[δp(a)] for every arc and ∂ξ a minimizer of the reduced boundary cost f[−p]; and any such optimal potential characterizes optimality of every feasible flow. This is the hub result of the whole chunk: the book states Theorem 9.14 is "immediate" from it, and every other placed result either specializes it directly or builds on that specialization.

Supporting structural targets

Theorem 9.5 reformulates MCFP0's optimality as the absence of a negative cycle in an auxiliary network; Theorem 9.6 gives MCFP0's primal and dual integrality, the latter identifying the optimal-potential set as an L-convex polyhedron. Theorem 9.14 specializes the goal to MSFP3; Theorem 9.15 upgrades this to a full polyhedral and integrality structure theorem for MSFP3's optimal-flow-boundary and optimal-potential sets (M2-convex and L-convex polyhedra respectively); Theorem 9.16 is the integer-flow analogue, with the boundary set now literally M2-convex and the integer-optimal-potential set literally L-convex. Theorems 9.18 and 9.20 give the negative-cycle reformulation for MSFP2, real and integer flows respectively, generalizing Theorem 9.5 by admitting a third class of auxiliary arcs governed by the M-convex boundary cost's directional derivative (or its discrete difference, in the integer case).

Significance

This is the chapter's demonstration that M-convexity is not merely an abstract combinatorial axiom but the exact structural hypothesis under which classical network-flow duality survives intact: every one of the four "nice properties" the book opens the chapter with (potentials, negative cycles, integrality, efficient algorithms) is preserved verbatim in the M-convex generalization, and this mission's eight results are the proof of that claim for the first three. The chunk's own internal dependency structure — one foundational theorem (9.4) from which every other placed result descends by specialization or direct generalization — is itself characteristic of how this book organizes its combinatorial machinery around a single convex- analytic core.

None of these results are open — they are Murota's own account of network flow duality under M-convexity (sections 9.1, 9.4, and 9.5). What this mission contributes is a faithful, machine-checked formal statement of each, extending the platform's coverage of chapter 9 begun in mission 12-network-flows (which covered §9.1.1-9.1.2 and §9.3, the feasibility and max-flow min-cut results, deliberately leaving this block for later apparatus); no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The eight results span real- and integer-flow versions of two nested problem hierarchies (MCFP0 ⊂ MCFP3, MSFP2 ⊂ MSFP3) and two distinct optimality certificates (potentials, negative cycles), which this mission handles by building one shared apparatus — FeasibleFlowMCFP3, Gamma3, OptimalFlowMCFP3, IsOptimalPotential — that MCFP0 and MSFP3 both instantiate (MCFP0 literally as the linear-cost/singleton-boundary special case of Eq. (9.11)), and one shared generic cycle/negative-cycle apparatus (IsCycle, CycleLength, HasNegativeCycle) instantiated three times with different auxiliary-arc types (A⊕A for MCFP0, A⊕A⊕(V×V) for MSFP2's extra Cξ arcs governed by the boundary cost's directional derivative). "Primal integral" and "dual integral" polyhedral convex functions (the book's own C[Z|R→R]/C[R→R|Z] notation, used in Theorem 9.15) needed a modeling decision, since the book's own definition of these classes lies outside this chunk's page range; see Formalization scope.

Formalization scope

Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity vocabulary is redeclared from prior missions in this series. "Primal integral" (C[Z|R→R], M[Z|R→R]) is formalized as integer effective domain (IsDomainIntegerArc/IsDomainIntegerR); "dual integral" (C[R→R|Z], M[R→R|Z]) is formalized as the existence of an integer subgradient at every domain point (IsDualIntegralArc/IsDualIntegralR) — a standard equivalent characterization for polyhedral convex functions, and a deliberate modeling choice recorded in MODERATION_NOTES.md rather than a literal transcription of the book's own (out-of-range) definition of these two notation classes. All eight numbered results found in this chunk's page range are placed in full, with no partial-coverage scope reduction. Contributions completing any of the eight sorrys are welcome; the goal and Theorem 9.15 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• R. T. Rockafellar, Network Flows and Monotropic Optimization, Wiley, 1984 [178] (the classical potential/Fenchel-duality framework this mission's Theorem 9.4 adapts).
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (the Lagrange duality and negative-cycle theory of section 9.5 this mission's Theorems 9.18 and 9.20 draw from).

Motivation

Mission 29-ch08b-conjugacyduality opened chapter 8's account of M2-convex functions — sums of M-convex functions — proving their domains and minimizers are M2-convex and that they are integrally convex. This mission completes that program and builds its exact mirror for L2-convex functions (integer infimal convolutions of L-convex functions), the class that appears on the opposite side of Edmonds's intersection theorem's min-max relation from M2-convexity. It proves optimality and proximity theorems for both classes, shows their subdifferentials add (a discrete analogue of the classical subdifferential sum rule), derives how the Legendre-Fenchel transform interacts with the sum/infimal-convolution operation, and — the technically hardest result in the whole cluster — establishes that L♮₂-convex functions are integrally convex, by a genuinely different and more intricate argument than the M2-side analogue required.

Setting

Fix a finite ground set $V$. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is L2-convex if $g = g_1 \square g_2$, the integer infimal convolution $g_1\square g_2(p) = \inf\{g_1(p_1)+g_2(p_2) : p_1+p_2=p\}$, of two L-convex functions $g_1, g_2$; L$^\natural_2$-convex if the summands are L$^\natural$-convex. An M2-convex function is a sum $f_1+f_2$ of two M-convex functions (mission 29-ch08b-conjugacyduality). The integer subdifferential $\partial_{\mathbb Z} f(x)$ and real subdifferential $\partial_{\mathbb R} f(x)$ generalize the subgradient set to integer- and real-valued perturbation directions respectively.

Formalization targets

Goal: L$^\natural_2$-convex functions are integrally convex (Theorem 8.42)

Every L$^\natural_2$-convex function is integrally convex, and in particular every L$^\natural_2$-convex set is integrally convex. The book's own proof is the most intricate argument in this cluster: given $p$ in the Minkowski sum $D_1+D_2$ of two L-convex sets, it constructs an explicit representation of $p$ as a convex combination of finitely many integer points of $D_1+D_2$, all lying in $p$'s own integral neighborhood, via the sorted fractional-part values of a chosen decomposition $p=p_1+p_2$ — a genuinely different technique from the M2-side analogue (Theorem 8.31), whose proof is a two-line consequence of convex extensibility.

Supporting structural targets

Eleven further results build the M2-/L2-convex theory in parallel. Theorems 8.33-8.34 give the M2-optimality criterion (a nonnegative-sum condition over cyclic exchange families) and its scaling-based proximity theorem; Theorem 8.35 shows subdifferentials of a sum of M$^\natural$- convex functions add, and that subdifferentials of M2-/M$^\natural_2$-convex functions are L2-/L$^\natural_2$-convex; Theorem 8.36 computes the conjugate of a sum as the infimal convolution of conjugates, with biconjugacy recovering the original sum. Propositions 8.39-8.41 transfer L-(natural-)convexity from summands to the domain and minimizer set of an L2-convex function, and give the precise attainment condition under which a linearly-perturbed infimal convolution's minimizer set splits additively. Theorems 8.43-8.44 give the L2-optimality and L2-proximity theorems, the exact L-side mirrors of Theorems 8.33-8.34; Theorem 8.45 mirrors Theorem 8.35 for subdifferentials of an infimal convolution; and Theorem 8.46 (found by direct reading, immediately following 8.45 and explicitly named by the book as 8.36's counterpart) shows biconjugacy for L$^\natural$-convex infimal convolutions.

Significance

The M2-/L2-convex function classes are where discrete convex analysis's abstract machinery meets concrete combinatorial optimization: Edmonds's matroid intersection theorem and its generalizations are literally statements about M2-convex minimization, with the L2-convex side supplying the dual bound. Theorem 8.35's subdifferential additivity is the discrete analogue of the classical Moreau-Rockafellar sum rule, and its proof (via the M-convex intersection theorem, already a milestone of mission 10-conjugacy-i) shows the sum rule holding without the constraint-qualification technicalities the continuous theory needs — a case where the discrete theory is cleaner than its continuous ancestor. Theorem 8.42's harder, dedicated proof technique is itself informative: it demonstrates that L2-convexity's combinatorial structure is not a routine transcription of the M2-convex case, foreshadowing the book's broader theme that M- and L-convexity, while conjugate, are not interchangeable in how their proofs actually work.

None of these results are open — they are Murota's account of the sum/infimal-convolution closure properties of M-convex and L-convex functions, continuing chapter 8's duality program into its most combinatorially concrete corner. What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Theorem 8.46) the platform's own automated extractor missed, extending the shared Lean vocabulary (InfConv, L2Convex, M2ConvexSet) mission 29-ch08b-conjugacyduality began; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to adapt the M2-side integral-convexity proof (a direct appeal to convex extensibility) verbatim; the book's own proof shows this does not work, requiring instead a from-scratch construction: decompose $p=p_1+p_2$, take fractional parts $a_1 = p_1-\lfloor p_1\rfloor$ and $a_2=\lceil p_2\rceil-p_2$, sort their combined distinct values, build threshold sets exactly as in the Lovász-extension construction, and verify each resulting integer point $q_i = \lfloor p_1\rfloor+\chi_{U_{1i}}+\lceil p_2\rceil-\chi_{U_{2i}}$ both lies in $D_1+D_2$ (via L-convex-set closure properties, Theorem 5.10) and in $p$'s integral neighborhood (a case split on whether $p(v)$ is itself an integer) — a genuinely multi-stage combinatorial argument with no single-inequality shortcut, unlike almost every other result in this mission.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; M2-/L2-convex functions are (V→ℤ)→WithTop ℝ. All twelve numbered results found in this chunk's page range are placed, with no partial-coverage scope reduction needed — every clause of every result, including all three parts of Theorems 8.35 and 8.45 and the full cyclic-exchange condition of Theorems 8.33-8.34, is stated in full. One numbered result nominally in this chunk's page range, Theorem 8.32, is not re-placed here: it was already found and placed as a milestone in mission 29-ch08b-conjugacyduality, whose own page range overlaps this chunk's by one page (PDF245) — see HARD.md. "g1□g2 > −∞" hypotheses are omitted rather than translated, since WithTop ℝ has no −∞ element to violate. This mission's base vocabulary is redeclared verbatim from mission 29-ch08b-conjugacyduality rather than imported, since sibling drafts in this series cannot yet reference one another; ConvexConjugate is redeclared from mission 10-conjugacy-i. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 8.35 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "Extreme points of a generalized polymatroid," Discrete Applied Mathematics, 152 (2005), pp. 268-278 [153] (the L2-convex integral-convexity proof this mission's goal is drawn from).
• K. Murota and A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [162] (the M2-proximity theorem, Theorem 8.34).

Motivation

Chapter 8 is where discrete convex analysis explains why it needed two separate notions — M-convexity (exchangeability) and L-convexity (submodularity) — rather than one. The answer is conjugacy: under the classical Legendre-Fenchel transform, the two classes turn out to be exactly dual to each other, the discrete analogue of the fact that convex analysis's transform is self-dual within a single class of convex functions. Mission 10-conjugacy-i proved the integer-lattice version of this fact (Theorem 8.12) but explicitly deferred the polyhedral version — Theorem 8.4, the chapter's own headline "Conjugacy theorem" — noting it needed a real-variable M-/L-convex-function layer the series had not yet built. That layer now exists, built across missions 23-24-ch06*-mconvexfunctions and 26-27-ch07*-lconvexfunctions. This mission proves Theorem 8.4 and its companions: the polar-cone correspondence it induces, its nonpolyhedral generalization, the separation and Fenchel-duality theorems for M♮-/L♮-convex functions, and the basic theory of M2-convex functions (sums of M-convex functions), which the Edmonds intersection theorem's own combinatorics is built from.

Setting

Fix a finite ground set $V$. For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$, the Legendre-Fenchel transform is $f^\bullet(p) = \sup_x [\langle p,x\rangle - f(x)]$. A polyhedral convex function $f$ is M-convex ($f \in M[\mathbb R \to \mathbb R]$) if it satisfies (M-EXC[R]); $g$ is L-convex ($g \in L[\mathbb R \to \mathbb R]$) if it satisfies (SBF[R]) and (TRF[R]). A concave function $h$ is always represented via $h_2 = -h$, an ordinary convex function, so every "$f \ge h$" hypothesis is restated as "$f + h_2 \ge 0$" — an equivalent formulation avoiding any need to represent $-\infty$ in the codomain. A polyhedral cone's polar is $C^\circ = \{y : \langle y,x\rangle \le 0\ \forall x \in C\}$. A function is M2-convex if it is the sum of two M-convex functions.

Formalization targets

Goal: the conjugacy theorem (Theorem 8.4)

The classes of polyhedral M-convex functions and polyhedral L-convex functions are in one-to-one correspondence under the Legendre-Fenchel transform: $f \in M \Rightarrow f^\bullet \in L$, $g \in L \Rightarrow g^\bullet \in M$, and the transform is an involution ($f^{\bullet\bullet}=f$, $g^{\bullet\bullet}=g$) on each class, with the identical statement for the M$^\natural$/L$^\natural$ variants. This is the theorem mission 10-conjugacy-i deferred, citing exactly the missing infrastructure this series has since built.

Supporting structural targets

Twelve further results build the surrounding theory. Proposition 8.2 gives the easy two-variable case of the general submodularity-preservation fact (Theorem 8.1, already a milestone of mission 10-conjugacy-i); Proposition 8.3 is the technical minimizer-difference lemma the goal's harder direction is built from. Theorem 8.5 derives the M-convex/L-convex cone polarity from the goal, and Theorem 8.6 extends the correspondence beyond the polyhedral case to general closed proper convex functions. Proposition 8.14 and Theorems 8.15-8.16 build the separation theory for M♮-/L♮-convex and concave function pairs, with integral witnesses when the functions are integer valued; Theorem 8.21 (parts 1-2) derives the Fenchel-type strong-duality equality these separation theorems make possible. Propositions 8.29-8.30 and Theorem 8.31 (plus Theorem 8.32, found by direct reading immediately after 8.31) build the basic theory of M2-convex functions: their domains and minimizer sets are M2-convex, they are integrally convex, and their global optimality reduces to a finite local check.

Significance

The goal is the theorem that retroactively explains this entire series' two-track structure: missions 20-25 (M-convex sets and functions) and 08/21/26-28 (L-convex sets and functions) are not two independent theories that happen to share techniques — they are conjugate images of each other, so every theorem proved on one side has a dual counterpart automatically available on the other via Theorem 8.4. This is made concrete immediately: Theorem 8.5's cone polarity and the diagram the book draws connecting $M_0[\mathbb R]$, $0L[\mathbb R\to\mathbb R]$, and submodular set functions $S[\mathbb R]$ (already correspondences this series proved independently, in missions 24-ch06d-mconvexfunctions and 28-ch07d-lconvexfunctions) are shown to be facets of one single conjugacy fact rather than three separate coincidences. The separation and Fenchel duality theorems (8.15, 8.16, 8.21) are the discrete analogues of the two theorems every convex optimization course opens with, and the book is explicit that they are not corollaries of the classical versions plus convex extensibility — they carry genuinely combinatorial content, specializing to Frank's discrete separation theorem and Edmonds's intersection theorem as examples the book itself gives.

None of these results are open — they are Murota's account of the duality at the heart of discrete convex analysis, the reason the theory needed two dual notions rather than one. What this mission contributes is a faithful, machine-checked formal statement of each, completing a theorem mission 10-conjugacy-i explicitly left for a future session once the necessary polyhedral apparatus existed, and including one result (Theorem 8.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal's harder direction (L⇒M) would try to verify the exchange inequality for $g^\bullet$ directly from the definition of the transform; the book's actual proof instead identifies the exchange inequality with a statement about weighted minimizers of $g$ itself via Proposition 8.3 (the minimizer-difference bound), converting a claim about the conjugate function into a claim about $g$'s own combinatorial structure — a genuine change of perspective, not a direct calculation. Proposition 8.3's own proof is the hardest single argument in this block: it derives the minimizer-difference bound by a contradiction argument that constructs an explicit pair of "worse" minimizers via a join/meet perturbation and derives a strict inequality from Theorem 7.29's translation inequality — a multi-step combinatorial argument with no direct shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; convex functions are WithTop ℝ valued throughout (never EReal, except for the Legendre-Fenchel transform itself, whose defining supremum/infimum can genuinely be infinite). All thirteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus Theorem 8.32 — are placed, with one documented scope reduction: Theorem 8.21 states only its real-attainment parts (1)-(2), not the integer-attainment refinement of parts (3)-(4), which needs a separate argument no other result in this chunk requires — see HARD.md. Concave functions $h$ are always represented via $h_2 = -h$ and every inequality $f \ge h$ restated as $f + h_2 \ge 0$, avoiding WithTop ℝ negation entirely. This chunk's own BRIEF.md inherited the chapters-4-7 page-offset boilerplate (printed = PDF $-$ 19); chapter 8 uses offset 18, confirmed against the PDF's own footers — every citation here uses the corrected offset. This mission's base vocabulary is redeclared from missions 10-conjugacy-i, 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the thirteen sorrys are welcome; the goal and Proposition 8.3 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 [152] (the polyhedral M-/L-convex conjugacy theory this mission's real-variable results are drawn from).

Motivation

The Legendre-Fenchel transform is the single most structurally important operation in convex analysis: for a proper closed convex function $f$, its conjugate $f^\bullet(p) = \sup_x \{\langle p,x\rangle - f(x)\}$ is again proper closed convex, and the transform is an involution — $f^{\bullet\bullet} = f$. This one fact underlies duality theory across optimization: every strong-duality theorem is, at bottom, a statement about conjugate pairs. Chapters 6 and 7 of this book developed M-convex and L-convex functions as if they were two separate theories, each with its own exchange axiom, optimality criterion, and proximity theorem. Chapter 8 reveals they were never separate: the Legendre-Fenchel transform, suitably discretized, is a bijection between the two classes. This mission formalizes that discrete conjugacy theorem together with its classical real-valued precursor and a genuine function-level generalization of Edmonds's intersection theorem, completing the picture that chunks 06 through 09 built the two halves of.

Setting

Let $V$ be a finite ground set. For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$, the Legendre-Fenchel transform is $f^\bullet(p) = \sup\{\langle p,x\rangle - f(x) : x \in \mathbb R^V\}$; $f$ is submodular if $f(x)+f(y) \ge f(x\vee y)+f(x\wedge y)$ and supermodular under the reverse inequality. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$, the discrete Legendre-Fenchel transform restricts the same supremum formula to $p \in \mathbb Z^V$: $f^\bullet(p) = \sup\{\langle p,x\rangle - f(x) : x \in \mathbb Z^V\}$ for $p \in \mathbb Z^V$ — a genuinely different object from the real-valued transform, since the supremum is now over integer $x$ only, and the codomain is checked back against the discrete M-/L-convexity axioms of chunks 06–09. The integer biconjugate $f^{\bullet\bullet}$ is the transform applied twice. $f$ is integer valued if every finite value it takes is an integer (the classes $M[\mathbb Z\to\mathbb Z]$, $L[\mathbb Z\to\mathbb Z]$ of the goal theorem are exactly the M-/L-convex functions with this property).

Formalization targets

Goal: Theorem 8.12 (the discrete conjugacy theorem)

(1) The classes $M[\mathbb Z\to\mathbb Z]$ and $L[\mathbb Z\to\mathbb Z]$ are in one-to-one correspondence under the discrete Legendre-Fenchel transform: for $f \in M[\mathbb Z\to\mathbb Z]$ and $g \in L[\mathbb Z\to\mathbb Z]$, $f^\bullet \in L[\mathbb Z\to\mathbb Z]$, $g^\bullet \in M[\mathbb Z\to\mathbb Z]$, $f^{\bullet\bullet}=f$, and $g^{\bullet\bullet}=g$. (2) The same correspondence holds between $M^\natural[\mathbb Z\to\mathbb Z]$ and $L^\natural[\mathbb Z\to\mathbb Z]$.

Milestones: Theorem 8.1, Proposition 8.11, Theorem 8.17

Theorem 8.1: the conjugate of a real-valued submodular function is always supermodular — the classical warm-up, and evidence that submodularity/supermodularity is not symmetric under conjugation on its own (the converse fails). Proposition 8.11: the integer biconjugate recovers $f$ at any point with a nonempty integer subdifferential — the fact that makes discrete biconjugation meaningful at all. Theorem 8.17 (the M-convex intersection theorem): a point jointly minimizes a sum of two M$^\natural$-convex functions if and only if a single linear functional separately certifies it as a minimizer of each perturbed function — the function-level generalization of chunk 04's Edmonds's intersection theorem for M-convex sets.

Significance

The result itself. The discrete conjugacy theorem is, in the book's own words, "the unifying result of the entire book": every theorem proved separately for M-convex functions (chunks 06–07) has an exact mirror for L-convex functions (chunks 08–09) precisely because the Legendre-Fenchel transform carries one class to the other. Theorem 8.17's function-level Edmonds generalization shows the payoff directly — the classical matroid-intersection-style min-max duality of chunk 04 was never really about sets; it is a special case (indicator functions) of a duality that holds for the whole class of M-convex functions.

Formalizing it. No matching item exists on the platform for conjugate functions, discrete conjugacy, or this generality of intersection theorem. This mission gives the first formal statement of the discrete conjugacy theorem, distinguishing it carefully from its real-valued (polyhedral) precursor, Theorem 8.4 — a genuinely different, harder theorem this mission does not draft (see Formalization scope), since the integer bijection needs the M-/L-proximity theorems of chunks 06–09 to control integrality under convex extension, while the real-valued case does not.

Difficulty

The obvious approach — try to prove the discrete conjugacy theorem directly by mimicking the real-valued proof (Theorem 8.4) with ℤ in place of ℝ everywhere — fails, because the real-valued proof's key step (Proposition 8.3, an infimal-convolution argument comparing arg min sets of perturbed polyhedral functions) has no immediate discrete analogue: a discrete arg min need not vary continuously with the perturbation the way a polyhedral one does. The book's actual strategy instead routes through the convex extension of the discrete function (chunk 06/08's bridge to chapter 3's integral convexity), applies the already-proved real-valued conjugacy theorem to the extension, and then must separately argue that the resulting conjugate, restricted back to integer points, is again integer-valued and satisfies the discrete exchange axiom — an argument that needs different treatment depending on whether the original function's domain is bounded or unbounded (an exhaustion argument via restriction to a growing integer interval, invoking chunk 06's proximity theorem to control convergence). Skipping this discreteness argument and treating the real-valued theorem as if it settled the integer case would silently discard exactly the chapter's own point.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq. ConvexConjugate (the discrete transform) has domain and codomain both (V → ℤ) → WithTop ℝ, obtained by taking the defining supremum in EReal (a complete lattice, so it is always total) and projecting back via a new FromEReal map — this is what lets the biconjugate f•• typecheck as an equality of functions of the same type as f. ConvexConjugateR (the real-valued transform, used only by the milestone Theorem 8.1) is a separate object with no shared code, per the explicit warning against conflating the two transforms; the two never appear in the same item.

A trivializing formalization of the goal would draft only the real-valued case (Theorem 8.4) as if it were the discrete theorem, or would silently allow WithTop ℝ's subtraction-avoidance convention to change which values are compared; neither is done. Theorem 8.4 itself (the polyhedral conjugacy theorem) is not drafted in this mission at all — it would require a fresh, otherwise-unused polyhedral M-/L-convex-function layer on Rⱽ that no other item here needs (see MODERATION_NOTES.md). The M-/L-separation theorems (8.15, 8.16) and the Fenchel-type duality theorem (8.21) are likewise left for a follow-on mission; contributions building the polyhedral bridge or the separation theorems, which depend on machinery this mission establishes, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

Motivation

A differentiable convex function on $\mathbb{R}^n$ is determined, up to an additive constant, by its gradient, and a vector field is a gradient of a convex function exactly when it satisfies a monotonicity condition along closed cycles. Convex analysis and optimization need the same statement for nonsmooth and extended-valued functions on infinite-dimensional spaces: the subdifferential replaces the gradient, and the question becomes which multivalued maps from a Banach space to its dual arise as subdifferentials, and how much of the function they determine. The answer underlies the treatment of optimality conditions, variational inequalities and evolution equations governed by subdifferentials, where one works with the operator $\partial f$ and needs to recover $f$ from it.

Timeline.

• 1966: R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (DOI 10.2140/pjm.1966.17.497), studied cyclically monotone operators and stated the characterization of subdifferentials as the maximal cyclically monotone operators (its Theorem 3), together with the maximal monotonicity of subdifferentials (its Theorem 4).
• 1969: H. Brézis pointed out a gap in the 1966 proofs of maximality and uniqueness: a family of dual vectors $x_\varepsilon^*$ used in the argument might increase unboundedly in norm as $\varepsilon \to 0$.
• 1970: Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (DOI 10.2140/pjm.1970.33.209), repaired the argument for arbitrary real Banach spaces, proving Theorem A (maximal monotonicity of $\partial f$) and Theorem B (the characterization treated here).

Setting

Let $E$ be a real Banach space with dual $E^*$, and write $\langle x, x^* \rangle$ for the value of $x^* \in E^*$ at $x \in E$. A proper convex function on $E$ is a function $f : E \to (-\infty, +\infty]$, not identically $+\infty$, with $f((1-\lambda)x + \lambda y) \le (1-\lambda)f(x) + \lambda f(y)$ for all $x, y \in E$ and $0 < \lambda < 1$. It is lower semicontinuous (lsc) in the norm topology. Its subdifferential is the multivalued map

$$\partial f(x) = \{\, x^* \in E^* \mid f(y) \ge f(x) + \langle y - x, x^* \rangle \ \ \forall y \in E \,\}.$$

A multivalued map $T : E \to E^*$ is a cyclically monotone operator if

$$\langle x_0 - x_1, x_0^* \rangle + \cdots + \langle x_{n-1} - x_n, x_{n-1}^* \rangle + \langle x_n - x_0, x_n^* \rangle \ge 0 \qquad\text{whenever } x_i^* \in T(x_i),\ i = 0, \dots, n,$$

and maximal cyclically monotone if, in addition, its graph $\{(x, x^*) \mid x^* \in T(x)\}$ is not properly contained in the graph of any other cyclically monotone operator. The conjugate of $f$ is $f^*(x^*) = \sup_{x \in E} (\langle x, x^* \rangle - f(x))$ on $E^*$, and $j(x) = \tfrac12\|x\|^2$. In the Lean development these are ProperConvex, subdiff, IsCyclicallyMonotone, IsMaximalCyclicallyMonotone, conj and halfSqNorm, in the namespace RockafellarMaxMono.Cyclic.

Formalization targets

Goal: Theorem B (p. 210)

For every multivalued map $T : E \to E^*$ on a real Banach space $E$,

$$\bigl(\exists f \text{ lsc proper convex with } T = \partial f\bigr) \iff T \text{ is maximal cyclically monotone},$$

and if $f$ and $g$ are lsc proper convex with $\partial f = T = \partial g$, then $g = f + c$ for a real constant $c$. Both halves are one statement.

Milestones, in attack order

1. (3.7) For a finite continuous convex function $f$ on a real Banach space, $\partial f(x)$ is nonempty and weak* compact and $f'(x;u) = \max\{\langle u, x^* \rangle \mid x^* \in \partial f(x)\}$.
2. Finite continuous case (pp. 214–215). For finite continuous convex $f, g$ on a real Banach space, $\partial g(x) \supset \partial f(x)$ for all $x$ implies $g = f + \mathrm{const}$.
3. (3.1) $\partial(f + j)(x) = \partial f(x) + \partial j(x)$ for lsc proper convex $f$.
4. Proposition 1 $x^{**} \in \partial f^*(x^*)$ if and only if $x^{**}$ is a weak** limit of a bounded net $x_i$ with $x_i^* \in \partial f(x_i)$, $x_i^* \to x^*$ in norm.
5. (p. 213) $(f + j)^*$ is finite and continuous on $E^*$.
6. (p. 211) $f^{**}$ restricted to $E$ is $f$.
7. (3.6) For lsc proper convex $f, g$: $\partial g(x) \supset \partial f(x)$ for all $x$ implies $g = f + \mathrm{const}$.

Significance

The result. Theorem B gives an intrinsic description of subdifferential maps: an operator is the subdifferential of a closed proper convex function if and only if it satisfies the cycle inequality and cannot be enlarged without violating it. The uniqueness clause says that a closed convex function is recovered from its subdifferential up to a constant, the nonsmooth counterpart of recovering a function from its gradient. Milestone 7 is stronger than uniqueness: a one-sided inclusion $\partial f \subseteq \partial g$ already forces $g = f + c$, and this is what gives maximality.

Formalizing it. The theorem is proved in the paper, and nothing of it is formalized on the platform. Mathlib has convex functions, continuous duals, biduals and weak-* topologies, but not extended-valued subdifferentials on Banach spaces, conjugate duality in the nonreflexive setting, or monotone operator theory. This mission produces formal statements of the paper's steps, the standard max formula for directional derivatives on a Banach space, and the Fenchel conjugate facts the argument uses, each as a separate target.

Difficulty

In a reflexive space the argument is short, because $\partial f^*$ is the inverse of $\partial f$. In a nonreflexive space it is not: $\partial f^*$ maps $E^*$ into $E^{**}$, and points of $E^{**} \setminus E$ appear. The naive route, transferring the inclusion $\partial f \subseteq \partial g$ to the conjugates by inverting the maps, breaks down there, and the 1966 argument failed at a related step, where the dual vectors in an approximation could be unbounded. Relating $\partial f^*$ to $\partial f$ without reflexivity is where the difficulty sits; the boundedness of the approximating nets in Proposition 1 is essential and cannot be dropped. The finite continuous case and the max formula (3.7) are needed on an arbitrary Banach space, including the dual $E^*$, not only on $E$.

Formalization scope

$E$ is a real Banach space (NormedAddCommGroup, NormedSpace ℝ, CompleteSpace); $E^*$ is StrongDual ℝ E with the operator norm, $E^{**}$ is StrongDual ℝ (StrongDual ℝ E), and $E \hookrightarrow E^{**}$ is NormedSpace.inclusionInDoubleDual. No reflexivity, inner product or finite dimension is assumed. Explicit readings:

• Values in $(-\infty, +\infty]$ are EReal with the requirement $f(x) \ne -\infty$; convexity is the paper's inequality for $0 < \lambda < 1$ in EReal arithmetic. Lower semicontinuity is in the norm topology.
• A multivalued map is E → Set (StrongDual ℝ E); $T = \partial f$ means $T(x) = \partial f(x)$ for every $x$.
• The cycle inequality quantifies over all $n \in \mathbb{N}$ and points indexed by Fin (n + 1) with wrap-around addition, so the last term is $\langle x_n - x_0, x_n^* \rangle$. Maximality is graph inclusion among cyclically monotone operators, not among monotone operators.
• The uniqueness constant is a real number, never $\pm\infty$.
• "$\supset$" in (3.6) is non-strict inclusion, and the hypothesis is one-sided.
• A net is a nonempty directed partially ordered index type with convergence along atTop; weak** convergence is pointwise convergence on $E^*$; "bounded" is a uniform norm bound.
• "Finite and continuous" for $(f+j)^*$ means equal everywhere to a continuous real-valued function. The max in (3.7) is IsGreatest, so it is attained; the directional derivative is the limit along $\lambda \to 0^+$.
• The print's "$\partial(f + j) = \partial f(x) + \partial j(x)$" in (3.1) is read as $\partial(f+j)(x)$.

A formalization that drops lower semicontinuity, allows an extended-real constant, or replaces "maximal cyclically monotone" by "maximal monotone" states a different, and in the first two cases false or trivial, theorem; the statements here keep all three.

The proof reduces Theorem B to milestone 7 through Theorem 1 of Rockafellar (1966) and its Corollary 2, which are not stated in this paper and are not milestones; formal statements of them are welcome as supporting theorems. Contributions of reusable infrastructure are welcome: extended-valued subdifferentials and conjugates on normed spaces, the Fenchel–Moreau identity on $E$, the sum rule with a continuous function, and the max formula for directional derivatives.

Selected references

• R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
• R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (1966), 497–510. https://doi.org/10.2140/pjm.1966.17.497
• G. J. Minty, On the monotonicity of the gradient of a convex function, Pacific J. Math. 14 (1964), 243–247. https://doi.org/10.2140/pjm.1964.14.243
• J.-J. Moreau, Fonctionnelles convexes, mimeographed lecture notes, Collège de France, 1967.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

A gambler watching a sequence unfold has to decide, at each moment and knowing only the past, whether to take what is on the table or wait for something better. That is the whole of optimal stopping, and it is one of the few problems in stochastic control with a clean and completely general answer: the value of the problem is the smallest superharmonic function dominating the immediate payoff. Snell (1952) proved the martingale form; the dynamic-programming form is due to Chow, Robbins and Siegmund. It is the structure behind the pricing of American options, the secretary problem, sequential hypothesis testing, and the bandit problems of Chapter 5.

Bäuerle and Rieder's Chapter 10 (Markov Decision Processes with Applications to Finance, Springer, 2011) derives this from their own Markov-decision machinery rather than from martingale theory, which makes the whole development elementary and self-contained: a stopping problem is a Markov Decision Problem whose action space is {continue, stop}, so Chapter 2's finite-horizon theory and Chapter 7's unbounded-horizon theory apply to it verbatim. The chapter then runs the resulting theory on three classical problems and solves each one in closed form.

Setting

The problem. A Markov process (X_n) on a Borel space E is observed. A stopping time is a random time τ with {τ ≤ n} ∈ F_n — "upon observing the process until time n we can decide whether or not τ has already occurred". Stopping at τ collects

$$R_\tau := \sum_{k=0}^{\tau-1} c_k(X_k) + g_\tau(X_\tau),$$

a running reward c_k while continuing and a stopping reward g_τ at the end, and the problem is to find V_N^*(x) := sup_{τ ≤ N} E_x[R_τ] (10.1). Assumption (B_N) — finiteness of the supremum of the positive parts — is what makes this well posed.

The reduction (Theorem 10.1.2). Take A = {0,1}, let a = 0 mean continue and a = 1 mean stop, and make the transition law uncontrollable on continuation and absorbing on stopping. A policy π = (f_0,…,f_{N-1}) induces the stopping time τ_π = inf{n | f_n(X_n) = 1} ∧ N, and conversely every stopping time is a history-dependent policy. The theorem says the two suprema agree: the extra history buys nothing.

The recursion (Theorems 10.1.3, 10.1.5). The Bellman operator becomes a two-branch maximum,

$$\mathcal{T}v(x) = \max\Big\{g(x),\ c(x) + \beta\int v(x')Q^X(dx'|x)\Big\},$$

with no action variable left in it. In the stationary case J_0 = g, J_n = \mathcal{T}J_{n-1}; the J_n increase, the sets S_n^* = {J_n = g} shrink — "the tendency to stop is non-decreasing as time goes by" — and the optimal rule is "stop on first entry into S_{N-n}^*".

The unbounded horizon (§10.2). Now the reward is discounted, R_τ = Σ β^k c(X_k) + β^τ g(X_τ) for τ < ∞, the value is V_∞^*(x) = sup_{τ<∞} E_x[R_τ], and there is no terminal condition to induct from. Three candidate values present themselves: V_∞^*; G = sup_π liminf_n J_{nπ}, a supremum over policies of limits of finite-horizon values; and J = lim_n J_n, which exists by monotonicity. Theorem 10.2.2, the goal, says all three coincide, that the common value solves J = \mathcal{T}J and satisfies 0-free bounds, and — the characterization — that it is the smallest c-superharmonic function majorizing g.

Turning the value into a rule (Theorems 10.2.3, 10.2.7, Corollaries 10.2.6, 10.2.8). Knowing the value is not knowing when to stop. Theorem 10.2.3 produces the stopping region as S^* = {J = g} = {d ≥ 0} where d = lim_n d_n, under two conditions that Corollary 10.2.6 then gives three checkable sufficient conditions for. Theorem 10.2.7 is the practical one, the One-Step-Look-Ahead Rule: if the set where stopping now beats stopping one step later is closed under the transition law, then the myopic rule is globally optimal. Corollary 10.2.8 adds monotonicity and gets a threshold.

Three applications (§10.3). The house seller who receives i.i.d. offers and pays maintenance on each rejection should accept the first offer above an explicit threshold, obtained as the maximiser of a one-dimensional function (Theorem 10.3.1). The secretary problem's value function is computed exactly (Proposition 10.3.2), giving the classical rule — reject the first k^*, then take the first leader — with success probability (k^*/N)h(k^*) and k^*(N)/N → 1/e (Theorem 10.3.3). And when the offers' distribution has an unknown parameter, MTP_2 of the likelihood propagates into monotonicity of the value in the information state (Theorem 10.3.4), with a fully explicit solution for the exponential/Inverse-Gamma conjugate pair (Theorem 10.3.6).

What is being asked

Formalize Theorem 10.2.2 in full: the three-way equality of V_∞^*, G and J, the fixed point equation, and — the part that carries the theorem — minimality among all functions that are both c-superharmonic and above g. Asserting only that J is such a function, or only one of the two conditions, is a strictly weaker and different claim.

The twelve milestones are the rest of the chapter, in attack order: the reduction and the two recursions, then the unbounded-horizon apparatus, then the three worked problems.

The stopping-time apparatus is built rather than assumed — the chain's law pinned by its finite-dimensional distributions, stopping times valued in ℕ ∪ {∞}, rewards vanishing at ∞ — because every theorem here is the identification of a supremum over stopping times with something computable, and carrying the value as an abstract function would make them vacuous. Every supremum is taken as a least upper bound against an explicit set of achievable values rather than by sSup, so that a set unbounded above is not silently given the value 0.