Operations Research

Motivation

The proximal map of a convex function is the basic building block of proximal-point, forward–backward, Douglas–Rachford and ADMM methods, which are used throughout large-scale convex optimization, signal processing and operator splitting. All of these methods treat $\operatorname{prox}_g$ as a nonexpansive operator and use the fact that it is a gradient. The questions this mission formalizes go back to the paper that introduced the map: J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), 273–299 (DOI 10.24033/bsmf.1625). Which maps $p : H \to H$ are proximal maps, and how can a function be recognized as the "potential" of one?

Moreau's answer (Corollaire 10.c) is intrinsic. A map is a proximal map exactly when it is nonexpansive and selects, at every point, a subgradient of some convex function. This characterization is the Hilbert-space origin of later results on firmly nonexpansive operators and on resolvents of maximal monotone operators (Minty 1962; Rockafellar 1970). It is still how one checks that a given nonexpansive operator is a proximal map.

Setting

Throughout, $H$ is a real Hilbert space with inner product $(x \mid y)$ and norm $\|x\|$.

• $\Gamma_0(H)$ is the class of functions $f : H \to \,]-\infty, +\infty]$ that are convex (convex epigraph), lower semicontinuous and not identically $+\infty$.
• The dual function of $f$ is $g(y) = \sup_{x \in H}[(x \mid y) - f(x)]$. For $f \in \Gamma_0(H)$, $g \in \Gamma_0(H)$ and $f$ is the dual of $g$.
• A vector $y$ is a subgradient of $\varphi$ at $z$, written $y \in \partial\varphi(z)$, when $\varphi(z)$ is finite and $\varphi(z) + (u - z \mid y) \le \varphi(u)$ for all $u$. For $f \in \Gamma_0(H)$ this is the paper's condition $f(z) + g(y) = (z \mid y)$, i.e. $z$ and $y$ are conjugate points.
• For $f \in \Gamma_0(H)$ and $z \in H$, the function $u \mapsto \tfrac12\|u - z\|^2 + f(u)$ has a unique minimizer, the proximal point $\operatorname{prox}_f z$. A map $p : H \to H$ is a prox map when $p = \operatorname{prox}_g$ for some $g \in \Gamma_0(H)$.
• A multivalued map $z \mapsto Pz \subseteq H$ contracts distances when $x \in Pz$, $x' \in Pz'$ imply $\|x - x'\| \le \|z - z'\|$.
• For dual functions $f, g$, the primitive of $\operatorname{prox}_g$ is $\varphi(z) = \tfrac12\|\operatorname{prox}_g z\|^2 + f(\operatorname{prox}_f z)$. With $\mathcal{Q}(z) = \tfrac12\|z\|^2$, a function $\varphi$ is less convex than $\mathcal{Q}$ when $\varphi + \gamma = \mathcal{Q}$ for a convex $\gamma$, and $\theta$ is more convex than $\mathcal{Q}$ when $\theta = \mathcal{Q} + \gamma$ for a convex $\gamma$ with values in $]-\infty, +\infty]$.

The Lean names are GammaZero, conj, subgrad, IsProx, prox, IsProxMap, ContractsDistances, primitive, LessConvexThanQ, MoreConvexThanQ and IsProxPrimitive, all in the namespace MoreauProx.Characterization.

Formalization targets

Goal: Corollaire 10.c

For every map $p : H \to H$,

$$p \text{ is a prox map} \iff \Big(\|p(z) - p(z')\| \le \|z - z'\| \ \ \forall z, z'\Big) \ \wedge\ \exists \varphi \text{ convex},\ \forall z \in H,\ p(z) \in \partial\varphi(z).$$

Nothing is assumed of $\varphi$ beyond convexity.

Milestones, in the order of the paper

1. Proposition 3.a. For $f \in \Gamma_0(H)$, $u \mapsto \tfrac12\|u - z\|^2 + f(u)$ has a strict minimum.
2. Proposition 4.a (Moreau decomposition). For $f \in \Gamma_0(H)$ with dual $g$: $z = x + y$ and $f(x) + g(y) = (x \mid y)$ if and only if $x = \operatorname{prox}_f z$ and $y = \operatorname{prox}_g z$.
3. (5.1). Conjugate pairs are monotone: $(x - x' \mid y - y') \ge 0$.
4. Proposition 5.b. $\|\operatorname{prox}_f z - \operatorname{prox}_f z'\| \le \|z - z'\|$, so $\operatorname{prox}_f$ is continuous.
5. Proposition 7.b. The primitive $\varphi$ of $\operatorname{prox}_g$ lies in $\Gamma_0(H)$, and its dual is $g + \tfrac12\|\cdot\|^2$.
6. Proposition 7.d. $\varphi$ is Fréchet differentiable with $\nabla\varphi(z) = \operatorname{prox}_g z$.
7. Proposition 9.b. For $\varphi$: ($\varphi \in \Gamma_0(H)$ less convex than $\mathcal{Q}$) $\iff$ ($\varphi \in \Gamma_0(H)$ with dual more convex than $\mathcal{Q}$) $\iff$ ($\varphi$ is the primitive of a prox map).
8. Proposition 10.b. Each of these is equivalent to: $\varphi \in \Gamma_0(H)$ and $z \mapsto \partial\varphi(z)$ contracts distances.

Three further results of the paper are included as unmilestoned companions: Proposition 8.a ($\operatorname{prox}_g = \operatorname{prox}_{g'}$ implies $g' = g + K$), Proposition 9.a ($\mathcal{Q}$ is the only function equal to its dual) and Proposition 9.d (nonnegative combinations $\sum \alpha_i p_i$ of prox maps with $\sum \alpha_i \le 1$ are prox maps).

Significance

The result. Corollary 10.c turns "is a prox map" into two checkable properties of $p$, one metric and one variational, with no need to exhibit $g$. Proposition 9.d is one consequence: closure of prox maps under subconvex combinations. Proposition 10.b gives the dual picture, which recognizes primitives of prox maps among the functions of $\Gamma_0(H)$ by a Lipschitz condition on their subdifferential. The intermediate results are the standard toolkit of proximal analysis. They include the Moreau decomposition, the nonexpansiveness of $\operatorname{prox}_f$, and the smoothness of the Moreau envelope $\varphi(z) = \inf_u[\tfrac12\|u - z\|^2 + f(u)]$ (Remark 7.c) with gradient $z - \operatorname{prox}_f z = \operatorname{prox}_g z$.

Formalizing it. All statements were proved in 1965 and are textbook material (Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., 2017, Ch. 12–14 and 24). None of them has a machine-checked proof in Mathlib, which has no $\Gamma_0(H)$ class, no extended-valued Fenchel conjugate and no proximal map on a Hilbert space. A complete development here would give reusable infrastructure: the conjugate of extended-valued functions with the Fenchel–Moreau theorem, the proximal map and its nonexpansiveness, and the differentiability of the Moreau envelope. Downstream convergence proofs of proximal algorithms need this layer.

Difficulty

The necessity half of 10.c follows quickly from 5.b and 7.d once those are available. The sufficiency half is the hard one. Given only a nonexpansive $p$ and a convex $\varphi$ with $p(z) \in \partial\varphi(z)$, one must produce $g \in \Gamma_0(H)$ with $p = \operatorname{prox}_g$. The obvious move is to take $g$ to be something built from $\varphi$ directly. This fails because the candidate is only defined through a duality that needs $\varphi \in \Gamma_0(H)$ and a precise convexity comparison with $\mathcal{Q}$. Neither is given, and neither follows from a pointwise argument. The intermediate milestones involve biconjugation of extended-valued functions, upper envelopes of affine functions in infinite dimension, and lower semicontinuity of functions taking $+\infty$. These are the places where finite-dimensional or finite-valued shortcuts do not apply.

Formalization scope

Conventions committed to in Lean:

• $H$ is [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. Functions with values in $]-\infty, +\infty]$ are H → EReal.
• $\Gamma_0(H)$: never $-\infty$, somewhere finite, convex epigraph in $H \times \mathbb{R}$, lower semicontinuous in the norm topology. The paper defines $\Gamma_0(H)$ via upper envelopes of continuous affine functions and states this equivalent description on the same page.
• The dual function is ⨆ x, (⟪x, y⟫ : EReal) - f x, computed in EReal (a complete lattice).
• Subgradients use the affine-minorant form, which requires $\varphi(z)$ finite. It agrees with the paper's (2.4) on $\Gamma_0(H)$ and is meaningful for the merely convex $\varphi$ of the goal.
• IsProx f z x says that $x$ minimizes $\tfrac12\|u - z\|^2 + f(u)$. The function prox f picks such a minimizer by choice (junk value $0$ if none exists). Every theorem using prox assumes $f \in \Gamma_0(H)$. A prox map is ∃ g, GammaZero g ∧ ∀ z, IsProx g z (p z).
• The primitive is real-valued and built from the pair $(f, g)$ as in Définition 7.a. Theorems about it assume $f \in \Gamma_0(H)$ and $g$ equal to the dual of $f$ (the paper's "duales l'une de l'autre", which this implies).
• In the goal, $\varphi$ is taken real-valued and convex (ConvexOn ℝ Set.univ). This is equivalent to the paper's $]-\infty, +\infty]$-valued $\varphi$, because a subgradient at every point forces $\varphi$ finite everywhere. The contraction condition is §10.a applied to $z \mapsto \{p(z)\}$.
• In 9.b and 10.b the auxiliary convex $\gamma$ may take $+\infty$. Property (III) does not assume $\varphi \in \Gamma_0(H)$.

Trivializing formalizations are ruled out. The goal's $\varphi$ is required to be convex and to have $p(z)$ as a genuine subgradient at every point, with $\varphi(z)$ finite. $\Gamma_0(H)$ excludes the constant $+\infty$, under which every point would minimize the proximal objective. No theorem applies prox outside $\Gamma_0(H)$, where its junk value would make statements vacuous.

Needed infrastructure: Fenchel–Moreau biconjugation for EReal-valued functions on a Hilbert space, existence of minimizers of coercive lsc convex functions (weak compactness of balls), and a Fréchet-derivative argument for the envelope. Contributions are welcome at every milestone. Also welcome are helper lemmas on EReal arithmetic for convex functions, and alternative proofs of 10.c via Minty's theorem on firmly nonexpansive maps.

Selected references

• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
• J.-J. Moreau, Fonctions convexes duales et points proximaux dans un espace hilbertien, C. R. Acad. Sci. Paris 255 (1962), 2897–2899.
• G. J. Minty, Monotone (nonlinear) operators in Hilbert space, Duke Math. J. 29 (1962), 341–346. https://doi.org/10.1215/S0012-7094-62-02933-2
• 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
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

Motivation

Proximal maps are the basic building block of first-order methods for nonsmooth convex optimization: the proximal point algorithm, forward–backward splitting (ISTA/FISTA), Douglas–Rachford splitting and ADMM all proceed by evaluating maps of the form $z \mapsto \operatorname{argmin}_u \big[\tfrac12\|u - z\|^2 + f(u)\big]$. The notion and its name come from J.-J. Moreau, who introduced proximal points in two 1962 notes in the Comptes rendus and gave the systematic theory in Proximité et dualité dans un espace hilbertien (Bull. Soc. Math. France 93 (1965), 273–299).

The central result of that paper, which Moreau calls the key proposition, links proximal maps to conjugate duality: every point of a Hilbert space splits uniquely into the proximal point of $z$ relative to a convex function plus the proximal point relative to its dual function. The identity $z = \mathrm{prox}_f z + \mathrm{prox}_{f^*} z$ is used throughout modern optimization, for example to compute the proximal map of a norm from the projection onto the dual-norm ball, and in the analysis of primal–dual splitting methods.

Timeline. Moreau (1962) announces proximal points and the decomposition along mutually polar cones. Moreau (1965) proves the general decomposition theorem for $\Gamma_0(H)$ and derives from it the characterization of proximal maps and the maximal monotonicity of subdifferentials in Hilbert space. Rockafellar (Pacific J. Math. 33 (1970)) extends maximal monotonicity of subdifferentials to Banach spaces.

Setting

Let $H$ be a real Hilbert space with inner product $(x \mid y)$ and norm $\|x\|$. Functions take values in the extended real line $[-\infty, +\infty]$.

The class $\Gamma_0(H)$ consists of the functions $f : H \to\ ]-\infty, +\infty]$ that are convex (their epigraph $\{(x, r) : f(x) \le r\}$ is convex in $H \times \mathbb R$), lower semicontinuous, and not identically $+\infty$.

The dual function of $f$ is

$$f^{*}(y) = \sup_{x \in H}\,\big[(x \mid y) - f(x)\big].$$

Two points $x$ and $y$ are conjugate with respect to $f$ and $g = f^*$ when $f(x) + g(y) = (x \mid y)$; the set of such $y$ is the subdifferential $\partial f(x)$.

For $f \in \Gamma_0(H)$ and $z \in H$, the proximal point $\mathrm{prox}_f z$ is the unique minimizer of

$$\Phi(u) = \tfrac12\|u - z\|^2 + f(u).$$

When $f$ is the indicator function of a nonempty closed convex set $C$ (zero on $C$, $+\infty$ outside), $\mathrm{prox}_f z$ is the nearest-point projection $\mathrm{proj}_C z$.

Formalization targets

Goal: Proposition 4.a (Moreau's decomposition)

Let $f \in \Gamma_0(H)$ and $g = f^*$. For all $x, y, z \in H$,

$$\Big(z = x + y \ \text{ and } \ f(x) + g(y) = (x \mid y)\Big) \iff \Big(x = \mathrm{prox}_f z \ \text{ and } \ y = \mathrm{prox}_g z\Big).$$

Milestones

1. (2.3), the Fenchel–Young inequality: $f(x) + f^*(y) \ge (x \mid y)$ for all $x, y$.
2. §2.b, biconjugation: $f^* \in \Gamma_0(H)$ and $f^{**} = f$ for $f \in \Gamma_0(H)$.
3. Proposition 3.a: $\Phi(u) = \tfrac12\|u - z\|^2 + f(u)$ has a strict minimum, so $\mathrm{prox}_f z$ is well defined.

Companions

• Corollaire 4.b: for a closed convex cone $P$ and its polar cone $Q = \{y : (x \mid y) \le 0\ \forall x \in P\}$, $z = x + y$ with $x \in P$, $y \in Q$, $(x \mid y) = 0$ iff $x = \mathrm{proj}_P z$ and $y = \mathrm{proj}_Q z$.
• (5.1): the conjugacy relation is monotone, $(x - x' \mid y - y') \ge 0$.
• Proposition 12.b: the relation $y \in \partial f(x)$ is maximal monotone.

Significance

The decomposition theorem gives, for every $z$, a unique splitting into a pair of conjugate points, and conversely identifies every conjugate pair summing to $z$ with the two proximal points. Special cases are the orthogonal decomposition along a closed subspace and its complement, and the decomposition along a pair of mutually polar cones (Corollaire 4.b). In the rest of Moreau's paper it yields that proximal maps are nonexpansive, that the Moreau envelopes of $f$ and $f^*$ add up to $\tfrac12\|z\|^2$, and that the subdifferential of a function in $\Gamma_0(H)$ is maximal monotone (Proposition 12.b). In algorithms it lets one evaluate $\mathrm{prox}_{f^*}$ from $\mathrm{prox}_f$ at no extra cost, which is the basis of dual and primal–dual proximal methods.

All results in this mission are classical and proved (Moreau 1965; see also Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., 2017, Thm. 14.3). What the mission adds is a machine-checked development. Mathlib contains convex functions, lower semicontinuity and Hilbert-space projections onto closed convex sets, but as of this mission's environment it has no Legendre–Fenchel conjugate for extended-valued functions on a Hilbert space, no proximal map and no maximal monotone operators. The Hilbert projection theorem is on the platform as FamousTheorems.hilbert_projection_theorem; it is the special case of Proposition 3.a for indicator functions.

Difficulty

The two directions of the goal are unequal. That conjugate points summing to $z$ are the two proximal points needs only the definition of the dual function. The converse must produce the conjugacy identity $f(x) + f^*(z - x) = (x \mid z - x)$ from the bare fact that $x$ minimizes $\tfrac12\|u - z\|^2 + f(u)$, and a pointwise first-order argument is unavailable because $f$ need be neither finite nor differentiable anywhere.

The milestones carry the analytic weight. Proposition 3.a needs existence of a minimizer of a function that is neither continuous nor coercive by itself on an infinite-dimensional space, so compactness arguments in the norm topology fail. Biconjugation (§2.b) is the Fenchel–Moreau theorem, which requires a separation theorem in $H \times \mathbb R$ applied to a closed convex epigraph whose values may be $+\infty$.

Formalization scope

Everything lives in the namespace MoreauProx.Decomposition, over {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]; the paper's $(x \mid y)$ is ⟪x, y⟫_ℝ. The following conventions are committed to:

• Functions are H → EReal. $\Gamma_0(H)$ (GammaZero) is the structure: never ⊥, not everywhere ⊤, convex epigraph in H × ℝ, and LowerSemicontinuous in the norm topology. The paper defines $\Gamma_0(H)$ as suprema of nonempty families of continuous affine functions, other than $+\infty$, and states the equivalence with this description (§2.a); the second description is the one formalized. Weak and strong lower semicontinuity agree for convex functions, as the paper remarks, so no weak topology appears.
• The dual function is conj f y = ⨆ x, ⟪x, y⟫_ℝ - f x in EReal; since a - ⊤ = ⊥, this matches both lines of (2.2).
• "$x = \mathrm{prox}_f z$" is the predicate IsProx f z x: $x$ minimizes proxObjective f z u = ‖u - z‖ ^ 2 / 2 + f u. With Proposition 3.a it is equivalent to the paper's notation; no choice function is used.
• The goal assumes GammaZero f and g = conj f; the paper's "$f, g \in \Gamma_0(H)$ dual to each other" follows from this by §2.b, so the goal is not weaker than the paper's.
• The polar cone uses $\le 0$ (the negative of Mathlib's innerDual), and $\mathrm{proj}_C z$ is the predicate IsProj C z x (nearest point).
• Maximal monotonicity is the paper's definition: monotone, and contained in no strictly larger monotone relation.

A formalization that drops the requirement that $f$ be not identically $+\infty$, drops the factor $\tfrac12$, replaces the duality hypothesis by unrelated $f, g$, or reads values through EReal.toReal would make the statement false or vacuous; the definitions above rule these out.

Contributions welcome: proofs of the three milestones and of the goal; reusable infrastructure for extended-valued convex analysis on Hilbert spaces (conjugates, subdifferentials, proximal maps), which the companion mission Proximité et dualité dans un espace hilbertien II builds on.

Selected references

• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
• J.-J. Moreau, Fonctions convexes duales et points proximaux dans un espace hilbertien, C. R. Acad. Sci. Paris 255 (1962), 2897–2899.
• 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
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

Motivation

The generalized assignment problem (GAP) asks for the cheapest way to give each of $n$ tasks to exactly one of $m$ agents when every agent has a limited amount of a resource and different agents consume different amounts of it for the same task. It models assigning jobs to machines or computers, software tasks to programmers, commercials to time slots, and customers to single-source plants in capacitated facility location. The problem is NP-hard, so exact methods rely on lower bounds that are cheap to compute and strong enough to prune a branch and bound tree.

G. Terry Ross and Richard M. Soland (Mathematical Programming 8, 1975) gave such a bound. The relaxation that ignores the resource limits is solved by giving every task to its cheapest agent; the overloaded agents are then repaired by one small binary knapsack problem each, whose optimal values are added as penalties. Their paper then shows that this repaired bound is not an ad hoc heuristic: it is exactly the value of a Lagrangean relaxation of the GAP at an explicit choice of multipliers. This identity made the Ross–Soland bound the reference point for the later Lagrangean and column-generation methods for the GAP (for example Fisher, Jaikumar and Van Wassenhove, Management Science 1986 and Savelsbergh, Operations Research 1997).

Setting

Agents are $I=\{1,\dots,m\}$ and tasks $J=\{1,\dots,n\}$. Giving task $j$ to agent $i$ costs $c_{ij}$ and uses $r_{ij}\ge 0$ units of agent $i$'s resource; agent $i$ has $b_i>0$ units. The problem is

$$\text{(P)}\qquad \min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad\sum_{i\in I}x_{ij}=1\ (j\in J),\quad x_{ij}\in\{0,1\}.$$

Dropping the resource constraints gives the relaxation (PR). It is solved by choosing, for each task $j$, a cheapest agent $i_j$ with $c_{i_jj}=\min_{i}c_{ij}$ and setting $x_{i_jj}=1$; its value is $Z=\sum_jc_{i_jj}$. Let $J_i=\{j: i_j=i\}$ be the tasks this solution gives to agent $i$, $I'=\{i:\sum_{j\in J_i}r_{ij}>b_i\}$ the overloaded agents, and $d_i=\sum_{j\in J_i}r_{ij}-b_i$ the excess of agent $i$. The penalty of moving task $j$ away from $i_j$ is $p_j=\min_{k\ne i_j}(c_{kj}-c_{i_jj})$. For $i\in I'$ the binary knapsack problem

$$\text{(PK}_i)\qquad\min\ z_i=\sum_{j\in J_i}p_jy_{ij}\quad\text{s.t.}\quad\sum_{j\in J_i}r_{ij}y_{ij}\ge d_i,\quad y_{ij}\in\{0,1\}$$

chooses the cheapest set of tasks to move off agent $i$; call its optimal value $z^*_i$. The knapsack bound is

$$\mathrm{LB}=Z+\sum_{i\in I'}z^*_i .$$

Dualizing the assignment constraints with multipliers $\lambda_j$ gives the Lagrangean relaxation

$$\text{(PR}_\lambda)\qquad\min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}+\sum_{j\in J}\lambda_j\Bigl(1-\sum_{i\in I}x_{ij}\Bigr)\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad x_{ij}\in\{0,1\}.$$

Finally $c_{1j}$ and $c_{2j}$ are the smallest and second smallest of $c_{1j},\dots,c_{mj}$, counted with multiplicity.

Formalization targets

Goal: the knapsack bound is the Lagrangean bound at $\lambda=c_2$

For every cheapest-agent choice $j\mapsto i_j$ and every choice of optimal knapsack solutions,

$$\mathrm{LB}=\min\Bigl\{\sum_{i}\sum_{j}c_{ij}x_{ij}+\sum_{j}c_{2j}\Bigl(1-\sum_{i}x_{ij}\Bigr)\ :\ x\ \text{feasible for (PR}_\lambda)\Bigr\},$$

the minimum being attained, and consequently $\mathrm{LB}\le\sum_i\sum_jc_{ij}x_{ij}$ for every $x$ feasible for (P). This is the paper's "principal result of this Lagrangean analysis" (§2, p. 96). It has no constants to improve; it is an identity between two optimization problems.

Milestones

In the paper's order of use: (PR) is solved by the cheapest agents (pp. 93–94); every lower bound on (PR$_\lambda$) is a lower bound on (P) (p. 95); (PR$_\lambda$) separates into one binary knapsack per agent (p. 95); at $\lambda=c_2$ the variables that are zero in the (PR) solution can be fixed at zero, the substitution $y_{ij}=1-x_{ij}$ turns agent $i$'s part into (PK$_i$), $p_j=c_{2j}-c_{1j}$, and agent $i$'s part has value $-\sum_{j\in J_i}p_j+z^*_i$ (p. 96). Two side results close the section: the solution obtained by moving the tasks the knapsacks select has cost exactly LB, so it is optimal whenever it is feasible (pp. 94–95); and the optimal dual multipliers of the bounded-variable linear program (PR$_L$) are exactly the vectors with $c_{1j}\le\lambda_j\le c_{2j}$ (pp. 95–96).

Significance

The identity says that a bound computed from one sorting pass and a handful of small knapsacks equals a Lagrangean dual bound at a closed-form multiplier. Validity of LB for (P) then follows from weak Lagrangean duality alone, and the multiplier $c_2$ is the upper end of the range of optimal dual multipliers of the linear program (PR$_L$), which the paper singles out as a suitable choice of multipliers. The rebuilt solution gives the algorithm a feasible incumbent at no extra cost whenever the knapsack repairs happen to respect all budgets.

The result is proved in the paper, in one sentence. The mission turns that sentence into checked statements: the separation of (PR$_\lambda$), the reduction of each agent's subproblem to (PK$_i$), the handling of ties among cheapest agents, and the role of nonnegative resources. As far as a search of the platform shows, nothing about the generalized assignment problem or its Lagrangean bounds has been formalized; the definitions here (assignment relaxations, per-agent knapsacks, bounded-variable duals) are reusable for other GAP and facility-location missions.

Difficulty

The Lagrangean relaxation at $\lambda=c_2$ is a larger problem than the knapsack bound suggests: a feasible $x$ may give a task to several agents or to none, and may use any agent, not only the cheapest one. The knapsack bound, by contrast, only looks at the tasks each agent receives in the (PR) solution. The paper bridges the two in one sentence of three observations, and each observation depends on a condition the sentence does not state: the sign of the resource coefficients, the treatment of agents that are not overloaded (for which no knapsack is solved), and ties among cheapest agents, which make some penalties zero and require the statement to hold for every tie-break. An inequality in one direction only (LB is a valid bound) is not the claim; the equality needs a feasible point of (PR$_\lambda$) whose value is exactly LB.

Formalization scope

Agents are Fin m and tasks Fin n, indexed from 0. Costs, resources, budgets, multipliers and variables are real numbers; a 0-1 variable is a real equal to 0 or 1, so the paper's sums are literal. The cheapest-agent selection is an arbitrary function a : Fin n → Fin m with IsCheapest c a, so every statement holds for every tie-break. $p_j$ and $c_{2j}$ are minima over the other agents, which requires $m\ge2$ (hm : 1 < m); $c_{2j}$ is proved to be the second smallest cost with multiplicity. Optimal values are never encoded as sInf: $z^*_i$ is the objective of a given optimal knapsack solution, and "the bound provided by (PR$_\lambda$)" is stated as a lower bound over all feasible points that is attained.

Standing hypotheses: $b_i>0$ (printed on p. 92), $r_{ij}\ge0$ (implicit in "the resource required", and necessary: with a negative $r_{ij}$ both (PR$_\lambda$) and (P) can fall below LB), and $m\ge2$. All costs are finite; the "not permissible" pairs of the paper's numerical example are outside the model.

A formalization that states only $\mathrm{LB}\le$ every (PR$_\lambda$) value, or that restricts the (PR$_\lambda$) competitors to the (PR) support or to at most one agent per task, would be a weaker theorem and does not meet the goal. The (PR$_L$) dual is written out explicitly with multipliers $u_{ij}\ge0$ for the bounds $x_{ij}\le1$; "each optimal dual multiplier lies anywhere in the range $c_{1j}\le\lambda_j\le c_{2j}$" is read as "the optimal multipliers are exactly this box".

Needed infrastructure is only finite sums over Fin and Finset.inf'. Proofs of the milestones, and lemmas on separable binary programs that could serve other Lagrangean-relaxation missions, are welcome.

Selected references

• G. T. Ross and R. M. Soland, A branch and bound algorithm for the generalized assignment problem, Mathematical Programming 8 (1975) 91–103. https://doi.org/10.1007/BF01580430
• A. M. Geoffrion, Lagrangean relaxation for integer programming, Mathematical Programming Study 2 (1974) 82–114. https://doi.org/10.1007/BFb0120690
• M. L. Fisher, R. Jaikumar and L. N. Van Wassenhove, A multiplier adjustment method for the generalized assignment problem, Management Science 32 (1986) 1095–1103. https://doi.org/10.1287/mnsc.32.9.1095
• M. Savelsbergh, A branch-and-price algorithm for the generalized assignment problem, Operations Research 45 (1997) 831–841. https://doi.org/10.1287/opre.45.6.831

Motivation

Retailers of seasonal goods sell at a full price first and mark down later. Customers who know this can wait for the markdown, and a firm that always has stock left for the markdown teaches them to wait. One remedy is to stock less than the low-price market would absorb, so that a customer who waits risks not getting the good at all. Liu and van Ryzin (Management Science 54(6), 2008) model this capacity rationing as a two-period game between a monopolist who chooses a stocking quantity and risk-averse customers who choose when to buy, and they characterize exactly when rationing is worth its cost in lost sales. The paper belongs to the revenue-management literature on strategic customers, where the firm's decision must anticipate the customers' best response to it.

Setting

A firm announces a price $p_1$ for period 1 and a lower price $p_2<p_1$ for period 2 and buys $C$ units at unit cost $\alpha<p_2$ before sales start; there is no replenishment. A market of $N>0$ customers, each wanting one unit, has valuations $v$ drawn independently from a distribution $F$; from §3 on, $F$ is uniform on $[0,\bar U]$.

Period-2 requests are filled at random with probability $q$, the fill rate, which customers anticipate correctly. Every customer has the same utility $u$: strictly increasing, concave, twice differentiable, with $u(0)=0$; from §3 on, $u(x)=x^\gamma$ with $0<\gamma<1$ (smaller $\gamma$ means more risk aversion). A customer with valuation $v$ buys in period 1 exactly when

$$v\ge p_1\quad\text{and}\quad u(v-p_1)\ge q\,u(v-p_2).$$

The threshold $v(q)$ separates early buyers from waiters.

Under the §3 assumptions, a cutoff $v\in[p_1,\bar U]$ is induced by the fill rate $q(v)=((v-p_1)/(v-p_2))^\gamma$ and the stocking quantity $C(v)=\frac{N}{\bar U}(\bar U-v+(v-p_2)q(v))$. The firm's profit from a segmented market is

$$\Pi(v)=\frac{N}{\bar U}\left((p_1-\alpha)(\bar U-v)+(p_2-\alpha)(v-p_2)\left(\frac{v-p_1}{v-p_2}\right)^\gamma\right),\tag{6}$$

and the profit from serving everybody at the low price is $\Pi^{NS}=(p_2-\alpha)\frac{N}{\bar U}(\bar U-p_2)$. The firm's optimal profit is the larger of $\Pi^0=\max_{p_1\le v\le\bar U}\Pi(v)$ and $\Pi^{NS}$. The first-order condition of (6) is

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

with root $v^0>p_1$, and the critical valuation bound is

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

In Lean these objects are IsCustomerUtility, buysEarly, cutoff (module LiuVanRyzin.Model) and fillRate, capacity, segProfit, lowPriceProfit, focLHS, criticalU (module LiuVanRyzin.PowerModel).

Formalization targets

Goal: Proposition 3 (p. 1122)

If $\bar U\ge U_c$, rationing is optimal: $v^0\in[p_1,\bar U]$, $v^0$ maximizes $\Pi$ on $[p_1,\bar U]$, and $\Pi(v^0)\ge\Pi^{NS}$. If $\bar U<U_c$, serving the whole market at the low price is optimal:

$$\Pi(v)\le\Pi^{NS}\qquad\text{for all }v\in[p_1,\bar U].$$

The goal fixes no constants; it is the paper's dichotomy, stated with its own (7) and (8).

Milestones, in attack order

1. Proposition 1 (p. 1120): for every $q\in[0,1)$ the threshold $v(q)\ge p_1$ exists and is unique, for a general utility.
2. Proposition 2 (p. 1120): $v(q)$ is strictly increasing in $q$, and convex if $u'''\ge 0$.
3. Proposition 5 (p. 1123): $C(v)$ and $q(v)$ are strictly increasing on $[p_1,\bar U]$, so choosing $C$ is the same as choosing $v$ or $q$.
4. §3.1, root of (7) (p. 1122): the left side of (7) strictly decreases on $v>p_1$ and changes sign, so $v^0$ exists and is unique.
5. Lemma 1 (p. 1122): $\Pi$ is strictly concave on $v\ge p_1$; its maximizer on $[p_1,\bar U]$ is $v^0$ if $v^0\le\bar U$, and $\bar U$ otherwise.
6. §3.1, bounds (p. 1122): $U_c$ decreases in $v^0$, $p_1<v^0<p_1+\gamma(p_2-\alpha)$, and $p_1+\gamma(p_2-\alpha)<U_c<p_1+p_2-\alpha$.

Significance

Proposition 3 answers the paper's central question: whether a firm facing strategic, risk-averse customers should deliberately under-stock. The answer depends on a single number, $U_c$, which depends on prices, cost and risk aversion but not on the market size, and it is compared with the top of the valuation range. Corollary 1, the $\gamma\to1$ limits of Proposition 4, and the comparative statics of Propositions 6–8 on how the optimal fill rate moves with $p_1$, $p_2$ and $\gamma$ are all read off from it. The bounds of milestone 6 turn it into sufficient conditions stated in the primitives alone.

The results are proved in the paper's e-companion (Online Appendix C). No machine-checked proof of any of them is known. Formalizing them gives a verified instance of a pattern that recurs throughout revenue management: a customer best response (a threshold), a reduction of the firm's problem to one scalar decision, a concavity argument, and a comparison of two regimes.

Difficulty

Most of the work is analysis of real powers with a moving base. $\Pi$ contains $(v-p_2)\bigl((v-p_1)/(v-p_2)\bigr)^\gamma$, whose derivative blows up at $v=p_1$, so its concavity on the closed half-line $[p_1,\infty)$ is not a routine second-derivative computation at the endpoint. The regime comparison in Proposition 3 is not implied by Lemma 1: Lemma 1 locates the segmented optimum, but whether it beats $\Pi^{NS}$ depends on $\bar U$, which enters $\Pi$ both through the prefactor $N/\bar U$ and through $\bar U-v$. The equivalence of that comparison with $\bar U\ge U_c$ requires eliminating $(v^0-p_1)/(v^0-p_2)$ with (7).

For Propositions 1–2 the utility is general: the threshold is defined by an inequality between $u(v-p_1)$ and $q\,u(v-p_2)$, and neither its monotonicity in $q$ nor its convexity under $u'''\ge0$ follows from a closed form. Only for $x^\gamma$ is there one.

Formalization scope

All quantities are real numbers. The utility of Propositions 1–2 is a function $u:\mathbb R\to\mathbb R$ that is strictly increasing, concave and continuous on $[0,\infty)$, twice differentiable on $(0,\infty)$, with $u(0)=0$. The threshold $v(q)$ is defined as the infimum of the set of early buyers, not assumed. Powers are Real.rpow; every power-model statement stays on $v\ge p_1$, or on $v>p_1$ where $(v-p_1)^{-1}$ appears. $\Pi$ is written in the closed form (6). The root $v^0$ is a binder constrained by $v^0>p_1$ and (7), and milestone 4 shows such a root exists. "Increases" in Propositions 2 and 5 is read as strictly increasing.

Hypotheses the paper uses without stating them, added here:

• $0\le p_2<\bar U$ in the goal. The uniform law gives $N\bar F(p_2)=\frac N{\bar U}(\bar U-p_2)$ only for $p_2\in[0,\bar U]$, and it makes $\bar U>0$.
• $p_1\le\bar U$ in the second part of Lemma 1, because (6) maximizes over the interval $[p_1,\bar U]$.
• Continuity of $u$ at $0$ in Propositions 1–2. The paper's "twice differentiable" implies it for any utility differentiable at $0$, and $x^\gamma$ satisfies it.
• In Proposition 2, "nonnegative third derivative" is read as $u\in C^3(0,\infty)$ with $u'''\ge0$ there.

The goal cannot be trivialized: $v^0$ is pinned to the root of (7), part 2 quantifies over every $v\in[p_1,\bar U]$, and the optimum is compared with $\Pi^{NS}$ exactly as the paper defines optimality.

Contributions are welcome at every level. Useful ones include the real-power calculus lemmas behind milestones 3–6, a proof of Propositions 1–2 for general concave utilities, and reusable facts about thresholds defined by single-crossing inequalities.

Selected references

• Q. Liu, G. van Ryzin, Strategic Capacity Rationing to Induce Early Purchases, Management Science 54(6):1115–1131, 2008. https://doi.org/10.1287/mnsc.1070.0832
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer, 2004. https://doi.org/10.1007/b139000

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality $F(x) = F_0 + \sum_i x_i F_i \succeq 0$. When the data $F_i$ are uncertain, El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) proposed to optimize against the worst case over a norm-bounded family of perturbations: the robust SDP. Their Theorem 3.1 shows that, for unstructured ("full") perturbations, the robust SDP is itself an SDP in the enlarged variable $(x,\tau)$. Section 4 of the paper then asks what robustification does to the solution. Nominal SDPs are often ill-posed: the optimal set can be a whole face, and optimal points can jump under small data changes. Section 4 shows that, under explicit hypotheses, the robust problem has a unique solution with quadratic growth, which is the sense in which the paper describes robustness as a regularization of SDPs. This mission formalizes that result, Theorem 4.2.

Setting

Fix natural numbers $m, n, p, q$, matrices $F_0, \dots, F_m \in \mathbb{R}^{n\times n}$ (symmetric), $R_0, \dots, R_m \in \mathbb{R}^{q\times n}$, $L \in \mathbb{R}^{n\times p}$, and an objective vector $c \in \mathbb{R}^m$, $c \neq 0$. Write $F(x) = F_0 + \sum_{i=1}^m x_iF_i$ and $R(x) = R_0 + \sum_{i=1}^m x_iR_i$.

With full perturbations, uncertainty level $\rho = 1$ and $D = 0$ (the standing choices of §4), the robust SDP is the SDP

$$\text{minimize } c^Tx \quad\text{subject to}\quad \mathcal{F}(x,\tau) = \begin{bmatrix} F(x) - \tau LL^T & R(x)^T \\ R(x) & \tau I\end{bmatrix} \succeq 0 \tag{15}$$

in the variables $y = (x,\tau) \in \mathbb{R}^m \times \mathbb{R}$. A point is feasible if $\mathcal{F}(x,\tau) \succeq 0$ (symmetric positive semidefinite) and optimal if it is feasible and minimizes $c^Tx$ over all feasible $(x',\tau')$. The solution is the pair $(x,\tau)$.

The paper's hypotheses (§4.1):

• H1 (Slater): $\mathcal{F}(x,\tau) \succ 0$ for some $(x,\tau)$.
• H2 (inf-compactness): every sublevel set $\{(x,\tau)\ \text{feasible} : c^Tx \le M\}$ is bounded.
• H3(a): the nullspace of the pencil $\lambda R_0 + \sum_i x_iR_i$ is one and the same proper subspace $N \subsetneq \mathbb{R}^n$ for every $(\lambda,x) \neq (0,0)$.
• H3(b): for every $x$ the stacked matrix $\begin{bmatrix} L^T \\ R(x)\end{bmatrix}$ has full column rank.

For $\tau > 0$ put $G(x,\tau) = F(x) - \tau LL^T - \frac{1}{\tau}R(x)^TR(x)$, the Schur complement of the block $\tau I$ in $\mathcal{F}(x,\tau)$.

The quadratic growth condition (QGC) holds at an optimal point $y^\star = (x^\star,\tau^\star)$ if there are $\alpha, \varepsilon > 0$ with

$$c^Tx \ \ge\ c^Tx^\star + \alpha\,\|y - y^\star\|^2 \qquad \text{for every feasible } y = (x,\tau),\ \|y - y^\star\| < \varepsilon .$$

Formalization targets

Goal: Theorem 4.2 (p. 39)

Under $c \neq 0$, symmetry of the $F_i$, H1, H2, H3(a) and H3(b):

$$\bigl(\forall\, y^\star \text{ optimal for (15)}:\ \text{QGC holds at } y^\star\bigr)\quad\text{and}\quad \exists!\, y = (x,\tau) \text{ optimal for (15)} .$$

Both halves are stated; uniqueness is of the pair $(x,\tau)$, and existence is part of the claim.

Milestones, in the order the paper's proof uses them

1. §4.1 (p. 38): H3(a) implies $R(x) \neq 0$ for every $x$.
2. §4.2 (p. 39): under H3(a), every feasible $\tau$ is positive; in particular $\tau_{\mathrm{opt}} > 0$.
3. §4.2, Eq. (16): for $\tau > 0$, $\mathcal{F}(x,\tau) \succeq 0 \iff G(x,\tau) \succeq 0$.
4. Appendix A (p. 49): at every optimal $(x,\tau)$ there is a dual matrix $Z \succeq 0$, $Z \neq 0$, with $\operatorname{Tr} ZG(x,\tau) = 0$, $\operatorname{Tr} Z\,\partial G/\partial x_i = c_i$ and $\tau^2\operatorname{Tr}LL^TZ = \operatorname{Tr}R(x)^TR(x)Z$.
5. Appendix A (p. 49): H3(b) rules out $\operatorname{Tr}LL^TZ = \operatorname{Tr}R(x)^TR(x)Z = 0$ for $Z \succeq 0$, $Z \neq 0$, hence $\operatorname{Tr}R(x)^TR(x)Z > 0$.
6. Appendix A (pp. 49–50): under H3(a), with $\tau > 0$, $Z \succeq 0$ and $\operatorname{Tr}R(x)^TR(x)Z > 0$, the Hessian of the Lagrangian $c^Tx - \operatorname{Tr} Z\,G(x,\tau)$ is positive definite.

Significance

The result. Theorem 4.2 turns the robust SDP into a well-posed problem: a unique solution with quadratic growth. Quadratic growth is the property from which the paper's Hölder-stability results (Theorem 4.3, Corollaries 4.1–4.2) follow through the perturbation theory of Bonnans, Cominetti and Shapiro, and it is what justifies using the robust SDP as a regularization of ill-conditioned SDPs (§5.4). The remark after the theorem notes a geometric reading: the growth holds for every objective, so the boundary of the robust feasible set contains no facets.

Formalizing it. The theorem has a published proof (Appendix A), which relies on a second-order sufficient condition for nonlinear SDPs cited from Bonnans, Cominetti and Shapiro. There is no machine-checked proof of it or of any second-order optimality result for SDPs that we know of. A formalization provides a complete account of the dual attainment, complementarity and second-order steps for this concrete problem class, and it checks the paper's computations; one of them, the intermediate display for the second derivative in Appendix A, has a factor error in its cross term that does not affect the conclusion.

Difficulty

The feasible set of (15) is a spectrahedron, and linear objectives over spectrahedra do not in general have unique minimizers, since optimal faces can be flat. Uniqueness therefore cannot come from convexity alone. It has to come from curvature of the boundary at the optimum, and that curvature is carried only by the nonlinear term $\frac{1}{\tau}R(x)^TR(x)$ of the Schur complement, which is degenerate along some directions. Positive definiteness of the Hessian must be recovered from the structural hypotheses H3(a) and H3(b), which interact with a dual matrix $Z$ that is known only to exist. The natural first attempt is to use $\tau > 0$ and the positive semidefiniteness of $Z$ directly. That attempt fails: the second derivative is $\operatorname{Tr} Z\,\mathcal{R}^T\mathcal{R}$ for a direction-dependent matrix $\mathcal{R}$, which vanishes on the kernel of $Z$, so it is not positive without H3(a) relating the kernels of all members of the pencil. Dual attainment and complementarity for (15) also have to be established, and the local second-order bound then has to be converted into a statement about every nearby feasible point.

Formalization scope

• Representation. Data are bundled in RobustSDP.Uniqueness.SDPData m n p q; decision points are pairs y : (Fin m → ℝ) × ℝ; the coefficient Fs i, i : Fin m, is the paper's $F_{i+1}$. $\succeq 0$ and $\succ 0$ are Mathlib's Matrix.PosSemidef and Matrix.PosDef, which include symmetry, as the paper's notation does.
• Conventions fixed. §4's standing choices $D = 0$ and $\rho = 1$ are built into (15). The standing assumptions $c \neq 0$ and symmetric $F_i$ (p. 33) are explicit hypotheses. H2 is read as bounded sublevel sets of the feasible set in $(x,\tau)$; the paper's wording ("any unbounded sequence of feasible points produces an unbounded sequence of objectives") is meant in this sense, as its claim that H1 and H2 give existence of optimal points shows. H3(b)'s full column rank is injectivity of $\xi \mapsto (L^T\xi, R(x)\xi)$. The QGC uses the Euclidean norm on $\mathbb{R}^{m+1}$ in its local form, which is equivalent to the paper's $o(\|y - y_{\mathrm{opt}}\|^2)$ form. It is stated for (15) rather than for the paper's reformulation (16), with which (15) coincides near the optimum because $\tau_{\mathrm{opt}} > 0$. The auxiliary constraint $\tau \ge 0.99\,\tau_{\mathrm{opt}}$ of (16) is not formalized. $G$ uses Lean's τ⁻¹, which is $0$ at $\tau = 0$, so every statement about $G$ assumes $\tau > 0$ or $\tau \ne 0$.
• No trivializing reading. The goal cannot be satisfied by stating only uniqueness of $x$, by reading H2 as "the objective is bounded below", or by reading H3(a) as "$R(x) \neq 0$". The statement quantifies over the pair $(x,\tau)$, and both the quadratic growth and the existence and uniqueness halves are required. The hypotheses are jointly satisfiable: for example $m = 1$, $n = p = 2$, $q = 4$, $F(x) = \mathrm{diag}(3+x, 3-x)$, $L = I_2$, $R(x) = [1; x]\otimes I_2$ and $c = 1$.
• Infrastructure. A complete development needs Schur complements for positive semidefinite block matrices (available in Mathlib), strong duality with dual attainment for inequality-form SDPs under Slater's condition (ConvexOptimization.sdp_strong_duality on the platform, in another Mathlib environment), existence of minimizers on closed bounded sets, second derivatives of matrix-valued maps, and a local second-order argument for convex problems. The duality and second-order parts can be reused beyond this mission. Contributions to any milestone, or alternative proofs that avoid the general Bonnans–Cominetti–Shapiro theory, are welcome.

Selected references

• L. El Ghaoui, F. Oustry and H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1), 33–52, 1998. https://doi.org/10.1137/S1052623496305717
• J. F. Bonnans, R. Cominetti and A. Shapiro, Sensitivity analysis of optimization problems under second order regular constraints, Math. Oper. Res. 23(4), 806–831, 1998 (the paper's reference [10]). https://doi.org/10.1287/moor.23.4.806
• A. Shapiro, First and second order analysis of nonlinear semidefinite programs, Math. Programming Ser. B 77, 301–320, 1997. https://doi.org/10.1007/BF02614439
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173