Optimization

Motivation

Value-at-Risk (VaR) is the loss level that a portfolio exceeds with probability at most $\varepsilon$. It is the standard risk measure of banking regulation, and its classical computation assumes Gaussian returns: for a Gaussian return vector with mean $\hat x$ and covariance $\Gamma$ it equals $-\Phi^{-1}(\varepsilon)\sqrt{w^\top\Gamma w} - \hat x^\top w$, where $\Phi$ is the standard normal distribution function. Real returns are not exactly Gaussian, and a VaR computed from a misspecified distribution can badly understate risk.

El Ghaoui, Oks and Oustry (Oper. Res. 51(4), 2003) replace the single distribution by a class $\mathcal P$ of distributions and define the worst-case VaR as the smallest loss level whose probability is at most $\varepsilon$ under every distribution of the class. Their first class, distributions with a given mean and covariance, leads to the Chebyshev-type bound of their Theorem 1, whose worst case is attained by discrete distributions. §4.2 of the paper asks instead for distributions that stay close to a Gaussian, measured by relative entropy (Kullback–Leibler divergence). Such balls are the basic uncertainty sets of distributionally robust optimization and of robust control in economics (Hansen and Sargent's multiplier and constraint preferences), and they give a smooth worst case. Theorem 9 computes the resulting worst-case VaR in closed form.

Setting

Returns are random vectors $x \in \mathbb R^n$ and a portfolio is a vector $w \in \mathbb R^n$ with $w \neq 0$; its return is $r(w,x) = w^\top x$. For a level $\gamma \in \mathbb R$ the loss set is $\mathcal S_\gamma = \{x : \gamma \le -x^\top w\}$ (Eq. 13 of the paper).

Given a class $\mathcal P$ of probability distributions on $\mathbb R^n$ and $\varepsilon \in (0,1)$, the worst-case Value-at-Risk (Eq. 4) is

$$V_{\mathcal P}(w) = \min\Big\{\gamma \in \mathbb R : \sup_{P \in \mathcal P} P(\mathcal S_\gamma) \le \varepsilon\Big\}.$$

Fix a mean $\hat x \in \mathbb R^n$ and a positive definite covariance $\Gamma \succ 0$, and let $P_0 = \mathcal N(\hat x, \Gamma)$ be the reference Gaussian. For $d \ge 0$ the relative-entropy class (Eq. 43) is

$$\mathcal P_d = \Big\{P \text{ probability on } \mathbb R^n : \mathrm{KL}(P, P_0) = \int \log\frac{dP}{dP_0}\,dP \le d\Big\},$$

with $\mathrm{KL}(P,P_0) = +\infty$ unless $P$ is absolutely continuous with respect to $P_0$.

The risk factor (Eq. 45) is

$$f(\varepsilon,d) = \sup_{\lambda>0}\frac{e^{\varepsilon/\lambda - d} - 1}{e^{1/\lambda} - 1}, \qquad \kappa(\varepsilon,d) = -\Phi^{-1}\big(f(\varepsilon,d)\big),$$

and the Gaussian tail of the loss set is $\phi(\gamma) = P_0(\mathcal S_\gamma) = 1 - \Phi\big((\gamma + w^\top\hat x)/\sqrt{w^\top\Gamma w}\big)$.

Formalization targets

Goal: Theorem 9 (p. 553)

For $\Gamma \succ 0$, $w \neq 0$, $d \ge 0$ and $0 < \varepsilon < 1$, the minimum in (4) over $\mathcal P_d$ exists and

$$V_{\mathcal P_d}(w) = \kappa(\varepsilon,d)\sqrt{w^\top\Gamma w} - \hat x^\top w. \tag{44}$$

Milestones

The milestones follow the proof of Theorem 9 on pp. 553–554, in attack order.

1. Eq. (45). The two expressions of $f$ agree: $\sup_{\lambda>0}\frac{e^{\varepsilon/\lambda-d}-1}{e^{1/\lambda}-1} = \sup_{v>0}\frac{e^{-d}(v+1)^\varepsilon - 1}{v}$.
2. Gaussian tail. $P_0(\mathcal S_\gamma) = 1 - \Phi\big((\gamma + w^\top\hat x)/\sqrt{w^\top\Gamma w}\big)$.
3. Eq. (47). For $\lambda > 0$, the Lagrangian $L(Q) = Q(\mathcal S_\gamma) + \lambda_0(1 - Q(\mathbb R^n)) + \lambda(d - \mathrm{KL}\text{-integral})$ is maximised over finite measures $Q \ll P_0$ by the exponentially tilted density $dQ^\star/dP_0 = \exp((\chi_{\mathcal S} - \lambda_0)/\lambda - 1)$, with value

$$\theta(\lambda_0,\lambda) = \lambda_0 + \lambda d + \lambda e^{-\lambda_0/\lambda - 1}\big((e^{1/\lambda}-1)\phi(\gamma) + 1\big).$$

4. Eq. (48). $\min_{\lambda_0\in\mathbb R}\theta(\lambda_0,\lambda) = \lambda d + \lambda\log\big((e^{1/\lambda}-1)\phi(\gamma)+1\big)$.
5. Duality. $\sup_{P\in\mathcal P_d} P(\mathcal S_\gamma) = \inf_{\lambda>0}\big(\lambda d + \lambda\log((e^{1/\lambda}-1)\phi(\gamma)+1)\big)$.
6. Inversion. For $d > 0$: some $\lambda > 0$ makes the dual value at most $\varepsilon$ if and only if $\gamma \ge \kappa(\varepsilon,d)\sqrt{w^\top\Gamma w} - w^\top\hat x$.
7. Remark after Theorem 9. $f(\varepsilon, 0) = \varepsilon$, so $\kappa(\varepsilon,0) = -\Phi^{-1}(\varepsilon)$. The risk factor $\kappa(\varepsilon, d)$ is strictly increasing in $d \ge 0$.

Significance

Theorem 9 says that an entropy ball around a Gaussian leaves the form of the Gaussian VaR unchanged: only the risk factor moves, from $-\Phi^{-1}(\varepsilon)$ to $\kappa(\varepsilon,d)$, a scalar computed by a one-dimensional maximisation. The worst-case VaR therefore stays a convex function of $w$ whenever $\kappa \ge 0$, and minimising it over a polytope of portfolios is a second-order cone program (problem (3) of the paper). The number $f(\varepsilon,d)$ is the largest $p$ with $\mathrm{KL}(\mathrm{Bernoulli}(\varepsilon)\,\|\,\mathrm{Bernoulli}(p)) \le d$, which ties the result to the binary-divergence bounds used throughout information theory.

The theorem was proved in 2003. The worst-case-probability step (milestone 5) is an instance of the Donsker–Varadhan / Gibbs variational duality for relative-entropy balls, which the paper imports from the literature (Smith 1995). No machine-checked proof of Theorem 9 or of this duality on $\mathbb R^n$ is known. A formalization would give a verified closed form for a relative-entropy distributionally robust chance constraint, and the duality and tilting lemmas would serve any mission on KL-ball robust optimization.

Difficulty

The obvious argument is Lagrangian duality for the infinite-dimensional problem $\sup\{P(\mathcal S_\gamma) : \mathrm{KL}(P,P_0) \le d\}$. Weak duality and the pointwise maximisation that produces the tilted density are elementary. The difficulty is the step the paper cites rather than proves: that the duality gap is zero, and that the supremum over distributions equals the infimum of the dual over $\lambda > 0$. The feasible set is a set of measures, the objective is an indicator, and the constraint is a divergence that is $+\infty$ off a set of absolutely continuous measures, so a finite-dimensional Slater argument does not apply as stated.

The second difficulty is at the boundary of the parameters. At $d = 0$ the supremum defining $f(\varepsilon,0)$ is approached only as $\lambda \to \infty$, so the final inversion step behaves differently from $d > 0$. At $\varepsilon = 1$ the theorem is false, since every level $\gamma$ is feasible and (4) has no minimum.

Formalization scope

Returns live in EuclideanSpace ℝ (Fin n). $P_0$ is Mathlib's multivariateGaussian xhat Γ with Γ.PosDef, and $\mathrm{KL}$ is InformationTheory.klDiv, which is $\infty$ unless $P \ll P_0$ with integrable log-likelihood ratio and equals $\int\log\frac{dP}{dP_0}\,dP$ otherwise for probability measures. The class $\mathcal P_d$ requires IsProbabilityMeasure P. $\Phi$ is cdf (gaussianReal 0 1), and $\Phi^{-1}(p)$ is defined as $\inf\{t : p \le \Phi(t)\}$, which inverts $\Phi$ on $(0,1)$. The quadratic form $w^\top\Gamma w$ is a double sum, and $\|\Gamma^{1/2}w\|_2$ is written $\sqrt{w^\top\Gamma w}$.

Conventions the Lean statements commit to:

• "min" in (4) is IsLeast of the feasible set $\{\gamma : P(\mathcal S_\gamma) \le \varepsilon \ \forall P \in \mathcal P_d\}$. "$\sup_{P}P(\mathcal S_\gamma) \le \varepsilon$" is written "for every $P$", with probabilities compared in $[0,\infty]$.
• The paper prints $\varepsilon \in (0,1]$. The mission assumes $0 < \varepsilon < 1$, because the goal is false at $\varepsilon = 1$.
• $w \neq 0$ is the paper's assumption that the admissible set of portfolios excludes $0$.
• $f(\varepsilon,d)$ is a Lean sSup of a set that is nonempty and bounded above by $1$ for $\varepsilon \le 1$, $d \ge 0$.
• The duality of milestone 5 is stated as the existence of one real number that is both the least upper bound of the worst-case probabilities and the greatest lower bound of the dual values, not as an equality of Lean's sSup and sInf.
• Eq. (48) is stated as an attained minimum (IsLeast), which the calculus gives.
• Milestone 3 works with finite measures $Q \ll P_0$ with integrable log-likelihood ratio in place of the paper's densities $p$. It uses the complement of $\mathcal S_\gamma$ where the paper writes $\{\gamma \ge -x^\top w\}$, which differs by a $P_0$-null hyperplane.
• Milestone 6 assumes $d > 0$; the goal keeps $d \ge 0$.

Restricting $\mathcal P_d$ to $\{P_0\}$, dropping IsProbabilityMeasure, or taking an arbitrary reference measure would trivialize or change the theorem. The class is the full KL ball around the nondegenerate Gaussian.

Infrastructure a complete development needs: the pushforward of a multivariate Gaussian under a linear functional (a one-dimensional Gaussian), the Gibbs variational principle for relative entropy, the strong duality for KL balls, and properties of $\Phi$ and its quantile (continuity, strict monotonicity, symmetry $\Phi(-t) = 1 - \Phi(t)$). The Gaussian-quantile and KL-ball duality lemmas are reusable beyond this mission. Contributions of any of these as separate lemmas are welcome.

Selected references

• L. El Ghaoui, M. Oks, F. Oustry, Worst-Case Value-at-Risk and Robust Portfolio Optimization: A Conic Programming Approach, Operations Research 51(4):543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
• J. E. Smith, Generalized Chebychev Inequalities: Theory and Applications in Decision Analysis, Operations Research 43(5):807–825, 1995. https://doi.org/10.1287/opre.43.5.807
• M. D. Donsker, S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, I, Communications on Pure and Applied Mathematics 28(1):1–47, 1975. https://doi.org/10.1002/cpa.3160280102
• L. P. Hansen, T. J. Sargent, Robust Control and Model Uncertainty, American Economic Review 91(2):60–66, 2001. https://doi.org/10.1257/aer.91.2.60

Motivation

Many problems in optimization and variational analysis reduce to finding a zero of a maximal monotone operator $T$: minimizers of a proper convex lower semicontinuous function are the zeros of its subdifferential, and saddle points and solutions of variational inequalities are zeros of associated monotone operators. The classical tool is Rockafellar's proximal point algorithm (Rockafellar 1976), which in a Hilbert space converges weakly but, as Güler showed (Güler 1991), not strongly in general.

Solodov and Svaiter (Math. Program. 87, 2000) modified the method in a Hilbert space $H$: after each proximal step they project the starting point $x_0$ onto the intersection of two half-spaces, and they proved that the resulting sequence converges strongly to the metric projection of $x_0$ onto $T^{-1}0$. Kamimura and Takahashi (SIAM J. Optim. 13, 2003) extended this result to Banach spaces such as $L^p$, $1<p<\infty$, replacing the identity by the duality mapping and the metric projection by a generalized projection defined through the duality mapping. This mission formalizes that extension.

Setting

Let $E$ be a real Banach space with dual $E^*$, and write $\langle x,f\rangle$ for the value of $f\in E^*$ at $x\in E$.

• The duality mapping is $Jx=\{v\in E^*:\langle x,v\rangle=\|x\|^2=\|v\|^2\}$. When $E$ is smooth (the limit $\lim_{t\to0}(\|x+ty\|-\|x\|)/t$ exists for all unit $x,y$), $J$ is single valued. $E$ is uniformly smooth if this limit is attained uniformly over unit $x,y$, and uniformly convex if $\|x_n-y_n\|\to0$ whenever $\|x_n\|=\|y_n\|=1$ and $\|(x_n+y_n)/2\|\to1$.
• An operator $T:E\to2^{E^*}$ is monotone if $\langle x_1-x_2,y_1-y_2\rangle\ge0$ for $y_i\in Tx_i$, and maximal monotone if no other monotone operator has a strictly larger graph. $T^{-1}0=\{x:0\in Tx\}$.
• For smooth $E$, $\varphi(x,y)=\|x\|^2-2\langle x,Jy\rangle+\|y\|^2$. The generalized projection $Q_Cx$ of $x$ onto a nonempty closed convex set $C$ is the unique minimizer of $\varphi(\cdot,x)$ over $C$ (it exists and is unique in reflexive, strictly convex, smooth spaces).
• The algorithm (3.1): from $x_0\in E$ and positive reals $r_n$,

$$0=v_n+\tfrac1{r_n}(Jy_n-Jx_n),\ v_n\in Ty_n,\quad H_n=\{z:\langle z-y_n,v_n\rangle\le0\},\quad W_n=\{z:\langle z-x_n,Jx_0-Jx_n\rangle\le0\},\quad x_{n+1}=Q_{H_n\cap W_n}x_0 .$$

In Lean, $J$ is J : E → StrongDual ℝ E with ∀ x, J x ∈ dualityMap x, $\varphi$ is phi J, "$z=Q_Cx$" is IsGenProj J C x z, and a run of (3.1) is IsHybridRun T J r x y v with starting point x 0.

Formalization targets

Goal: Theorem 8

If $E$ is uniformly convex and uniformly smooth, $T$ is maximal monotone, $T^{-1}0\neq\emptyset$, $r_n>0$ and $\liminf_n r_n>0$, then every sequence generated by (3.1) satisfies

$$x_n\ \longrightarrow\ Q_{T^{-1}0}\,x_0\quad\text{in norm}.$$

Milestones

In the order of the paper: the single-valuedness of $J$ on smooth spaces and its uniform continuity on bounded sets for uniformly smooth spaces (§2, properties 2 and 4); Xu's characterization of uniform convexity (Proposition 1); $\varphi(y_n,z_n)\to0$ with one bounded sequence implies $y_n-z_n\to0$ (Proposition 2); existence and uniqueness of $Q_Cx$ (Proposition 3); its variational characterization $\langle z-x_0,Jx_0-Jx\rangle\ge0$ (Proposition 4); the inequality $\varphi(y,Q_Cx)+\varphi(Q_Cx,x)\le\varphi(y,x)$ (Proposition 5); Rockafellar's surjectivity theorem $R(J+rT)=E^*$ (Theorem 6); well-definedness of (3.1) (Proposition 7); $T^{-1}0\subseteq H_n\cap W_n$ (Remark 1); and the monotonicity step

$$\varphi(x_{n+1},x_n)+\varphi(x_n,x_0)\le\varphi(x_{n+1},x_0).\tag{3.2}$$

Significance

The theorem gives a strongly convergent method for finding zeros of maximal monotone operators in a class of Banach spaces that includes $L^p$ and $\ell^p$ for $1<p<\infty$, and it identifies the limit: it is not an arbitrary zero but the generalized projection of the starting point. Applied to $T=\partial f$ it yields a strongly convergent minimization method for proper convex lower semicontinuous functions (§4 of the paper). The generalized projection $Q_C$, the function $\varphi$ and the hybrid (CQ-type) projection scheme became standard tools in the later Banach-space fixed-point and splitting literature.

The result is proved in the paper; the mission's contribution is a machine-checked proof. As far as the platform catalog and Mathlib show, none of its ingredients is formalized: Mathlib has uniformly convex and strictly convex spaces and the double dual, but no duality mapping, no notion of smoothness, no monotone operators and no generalized projection.

Difficulty

The obvious route, copying the Hilbert-space proof of Solodov and Svaiter, fails at every place where that proof uses the inner product: the projection onto $H_n\cap W_n$ is no longer characterized by orthogonality, $\|x-y\|^2$ is not a Bregman-type distance, and weak convergence of $x_{n_i}$ together with $\|x_{n_i}\|\to\|w\|$ no longer yields strong convergence for free. The paper replaces these steps with properties of $\varphi$ and of $J$, which in turn rest on the geometry of $E$: uniform convexity (through Proposition 1) and uniform smoothness (through the uniform continuity of $J$). In Lean, these geometric facts, reflexivity of uniformly convex spaces (Milman–Pettis) and Rockafellar's surjectivity theorem are all absent and have to be built.

Formalization scope

• $E$ is a real Banach space (NormedAddCommGroup, NormedSpace ℝ, CompleteSpace). The dual is StrongDual ℝ E with the operator norm; $\langle x,f\rangle$ is f x. Sequences are indexed by $\mathbb N$ from $0$.
• Uniform convexity is Mathlib's UniformConvexSpace (ε–δ form, equivalent to the sequential definition); strict convexity is StrictConvexSpace ℝ E; reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual. Smoothness and uniform smoothness are defined from the limit (2.1) over real $t\neq0$; uniform smoothness uses one $\delta$ for all unit $x,y$.
• Maximality quantifies over all monotone operators whose graph contains that of $T$.
• The single-valued $J$ is a function constrained by ∀ x, J x ∈ dualityMap x in every statement that uses it; on a smooth space this determines $J$ (a milestone).
• $Q_C$ and the algorithm are relations, not functions; the goal is stated for every run of (3.1) and asserts the existence of a generalized projection $z$ of $x_0$ onto $T^{-1}0$ with $x_n\to z$. $\liminf r_n>0$ is "some $c>0$ bounds $r_n$ below eventually", and $r_n>0$ is a separate hypothesis.
• The goal assumes neither reflexivity, strict convexity nor smoothness (they follow from the uniform hypotheses), nor that $T^{-1}0$ is closed or convex (that follows from maximality).
• Trivializing formalizations are ruled out: $J$ must be the duality mapping, runs of (3.1) exist (Proposition 7), and the limit must be identified as $Q_{T^{-1}0}x_0$, not merely shown to exist.

Reusable infrastructure: the duality mapping and its properties, smooth and uniformly smooth spaces, Milman–Pettis, monotone operators and Rockafellar's surjectivity theorem, and the generalized projection. Contributions to any of these are welcome independently of the goal.

Selected references

• S. Kamimura and W. Takahashi, Strong convergence of a proximal-type algorithm in a Banach space, SIAM J. Optim. 13(3):938–945, 2003. https://doi.org/10.1137/S105262340139611X
• M. V. Solodov and B. F. Svaiter, Forcing strong convergence of proximal point iterations in a Hilbert space, Math. Program. 87:189–202, 2000. https://doi.org/10.1007/s101070050002
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM J. Control Optim. 14(5):877–898, 1976. https://doi.org/10.1137/0314056
• R. T. Rockafellar, On the maximality of sums of nonlinear monotone operators, Trans. Amer. Math. Soc. 149:75–88, 1970. https://doi.org/10.1090/S0002-9947-1970-0282272-5
• O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM J. Control Optim. 29(2):403–419, 1991. https://doi.org/10.1137/0329022
• H.-K. Xu, Inequalities in Banach spaces with applications, Nonlinear Anal. 16(12):1127–1138, 1991. https://doi.org/10.1016/0362-546X(91)90200-K

Motivation

Many firms learn part of future demand before it has to be served: customers place orders days or weeks ahead of the date they need the goods, or commit to delivery dates in contracts. Advance demand information of this kind reduces the uncertainty the inventory manager has to protect against, and the question is how replenishment decisions should use it. Gallego and Özer (Management Science 47(10), 2001) model orders placed up to $N$ periods ahead and a supply lead time $L$. They show that, with a fixed ordering cost, the classical $(s,S)$ structure survives with parameters that depend on the observed future demand, and they identify when that dependence disappears.

The classical theory this builds on is the finite-horizon inventory model with a set-up cost. Scarf (1960) introduced $K$-convexity to prove that $(s,S)$ policies are optimal there. Veinott (1966) and Iglehart (1963) bounded the optimal policy parameters by myopic quantities. Gallego and Özer extend both results to a state that carries a vector of observed demands.

Setting

Periods are $t = 1, \dots, T$. In period $t$ customers place orders $D_t = (D_{t,t}, \dots, D_{t,t+N})$ for periods $t, \dots, t+N$; $D_t$ is a random vector with law $\mu_t$ and nonnegative components. The lead time $L$ and the information horizon $N$ satisfy $N > L+1$; write $M = N - L - 1 \ge 1$. The state at the start of period $t$ is a pair $(x_t, o_t)$: the modified inventory position $x_t \in \mathbb{R}$, and the vector

$$o_t = (o_{t,t+L+1}, \dots, o_{t,t+N-1}) \in \mathbb{R}^M$$

of demands already observed for the periods beyond the protection period $t, \dots, t+L$.

The manager raises $x_t$ to an order-up-to level $y \ge x_t$, paying a set-up cost $K_t > 0$ if $y > x_t$. After $D_t$ is observed, the state moves to

$$x_{t+1} = y - \sum_{s=t}^{t+L+1} D_{t,s} - o_{t,t+L+1},\qquad o_{t+1,s} = o_{t,s} + D_{t,s}\ \ (s = t+L+2,\dots,t+N),$$

with $o_{t,t+N} = 0$. With a convex single-period cost $G_t$, discount factors $\alpha_t > 0$ and $\delta(z) = \mathbf 1\{z > 0\}$, the optimal cost satisfies $J_{T+1} \equiv 0$ and

$$J_t(x, o) = \min_{y \ge x}\{K_t\delta(y - x) + V_t(y, o)\},\qquad V_t(y, o) = G_t(y) + \alpha_{t+1}\,\mathbb E\,J_{t+1}(x_{t+1}, o_{t+1}).$$

Let $H_t(x, o) = K_t + \min_{y\ge x}V_t(y,o) - V_t(x,o)$. The order-up-to level $S_t(o)$ is the least minimizer of $V_t(\cdot, o)$, and the reorder point is $s_t(o) = \max\{x : H_t(x,o) \le 0\}$.

A function $g$ is $(a,b)$-convex, $g \in C(a,b)$, if $g(\theta x_1 + (1-\theta)x_2) \le \theta(a + g(x_1)) + (1-\theta)(b + g(x_2))$ for all $x_1 \le x_2$ and $\theta \in [0,1]$; $C(0,K)$ is Scarf's $K$-convexity. In the stationary problem $G_t = G$, $K_t = K$, $\alpha_t = \alpha$ and $\mu_t = \nu$, and the myopic levels are

$$S^m = \min\{y : G(y) \le G(x)\ \forall x\},\quad s^m = \max\{y \le S^m : G(y) \ge K + G(S^m)\},\quad \overline S = \inf\{y > S^m : G(y) > G(S^m) + \alpha K\}.$$

Formalization targets

Goal: Theorem 2 (p. 1350)

For the stationary problem, every $1 \le t \le T$ and every observed-demand vector $o_t \ge 0$,

$$o_{t,t+L+1} \ge \overline S - s^m \implies S_t(o_t) = S^m.$$

Only the observed demand for the first period beyond the protection period is compared with the threshold; the other components of $o_t$ are free.

Milestones

• Lemma 1, Parts 1, 2, 4, 5 (p. 1349): inclusion, positive combinations, expectations, and $g(\max(x,s))$ for $(a,b)$-convex functions.
• Lemma 2 and Corollary 1 (p. 1350): for $V \in C(0,K)$ with a minimizer $S$, $H$ changes sign once from $-$ to $+$, and (for continuous $V$) $J(x) = V(\max(s,x))$.
• Theorem 1, Parts 1–3 (p. 1350): $V_t(\cdot, o_t) \in C(0, K_t)$ is coercive, a state-dependent $(s_t(o_t), S_t(o_t))$ policy is optimal, and $J_t(\cdot, o_t) \in C(0, K_t)$ with its limits at $\pm\infty$.
• Lemma 3 (p. 1351): $S^m \le S_t(o_t) \le \overline S$ and $s^m \le s_t(o_t)$.

Significance

Theorem 1 says that advance demand information does not destroy the $(s,S)$ structure: the optimal policy is still a reorder point and an order-up-to level, now functions of $o_t$. Theorem 2 is a horizon result. Once enough demand is already booked for period $t+L+1$, the order-up-to level is the myopic one, computed from $G$ alone, and the rest of the information vector can be ignored. The threshold $\overline S - s^m$ grows with the set-up cost. In practice the manager then orders only to cover demand up to period $t+L$, knowing another order will be placed in period $t+1$, and the search for state-dependent policies is confined to states with little booked demand.

The results are proved in the paper, with some steps argued informally (the unit forward difference in Lemma 3, a minimum over an open set in the definition of $\overline S$). As far as the platform's catalog shows, no $(s,S)$ optimality theorem of this form has a machine-checked proof: the platform has $K$-convexity lemmas for a single constant, not for $(a,b)$-convexity or a dynamic program with a vector state. A formal proof would check the infinite-state induction and the conditions under which the expectation in (9) is finite. The $(a,b)$-convexity layer and the one-period results (Lemma 2, Corollary 1) are reusable for any set-up cost model.

Difficulty

The obvious induction proves $K$-convexity of $V_t$ and then applies Scarf's argument. The vector state makes each step conditional on facts the scalar case gets for free. The expectation in (9) mixes a random shift of $x$ with a random update of $o$, so preserving $K$-convexity needs Lemma 1, Part 4 rather than the scalar version. Coercivity and continuity of $V_t(\cdot, o)$, and measurability and integrability of $D \mapsto J_{t+1}(x_{t+1}, o_{t+1})$, must be carried through the induction jointly in $(x, o)$. They cannot be assumed.

For Theorem 2, $V_t$ is not a function of $G$ alone, and a comparison of $S_t(o_t)$ with $S^m$ has to control $\mathbb E J_{t+1}$. That requires the lower bound $s^m \le s_{t+1}(o_{t+1})$ at the next period, which holds only on the nonnegative state space.

Formalization scope

Everything is stated about the functional equation (8)–(9). The paper derives it in Appendix A from a control problem over history-dependent policies, citing Özer (2000); that reduction is out of scope. The demand vector is Fin (L + M + 2) → ℝ and $o$ is Fin M → ℝ, with component $j$ equal to $o_{t,t+L+1+j}$. $J$ is defined by backward recursion, minima over $y \ge x$ are infima over $\{y : x \le y\}$, and expectations are Bochner integrals. $G_t$ is an abstract primitive, not built from holding and penalty costs.

The paper's hypotheses are $G_t$ convex with $G_t(y) \to \infty$ as $|y| \to \infty$ (stated for $\widetilde G_t$, used for $G_t$), $K_t > 0$ (Section 4), and $\alpha_{t+1}K_{t+1} \le K_t$. The formalization adds hypotheses the paper uses without stating:

• positive discount factors;
• demands nonnegative almost surely;
• every demand component has a finite mean, and $|G_t(y)| \le a_t + b_t|y|$ (so the expectation in (9) is finite);
• continuity of $V$ in the abstract Corollary 1;
• nonnegative observed demands $o_t$ in Lemma 3 and Theorem 2, where the lower bound fails for negative $o_{t,t+L+1}$.

All hypotheses are placed on the primitives; nothing is assumed about the derived $V_t$ or $J_t$. A Solutions/verification instance ($G(y) = |y|$, $K = 1$, $\alpha = 1/2$, zero demand) shows these hypotheses can be met together.

The definition of $\overline S$ is read as an infimum: the paper prints a minimum over an open set. $S_t(o_t)$ and $s_t(o_t)$ appear through IsLeast and IsGreatest, never as sInf/sSup values. A default value therefore cannot satisfy a conclusion, and vacuous readings (an empty minimizer set, an unbounded reorder set) are excluded. The infinite-horizon results (Lemma 4, Theorem 3, Corollary 2) and the zero set-up cost case are not part of this mission. Contributions are welcome at every level, and most of all a reusable library for $(a,b)$-convex functions.

Selected references

• G. Gallego, Ö. Özer, Integrating Replenishment Decisions with Advance Demand Information, Management Science 47(10):1344–1360, 2001. https://doi.org/10.1287/mnsc.47.10.1344.10261
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• A. F. Veinott, On the Optimality of (s,S) Inventory Policies: New Conditions and a New Proof, SIAM Journal on Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259

Motivation

Many convex sets that appear in optimization have complicated descriptions in their own space but simple descriptions as projections of higher-dimensional sets. A polytope with exponentially many facets can be the shadow of a polyhedron with polynomially many; the unit disk is the projection of a slice of the cone of $2\times 2$ positive semidefinite matrices. Such a representation, a lift, turns linear optimization over the original set into a linear or semidefinite program over the lifted one, so the size of the smallest lift measures how hard the set is for conic optimization.

For polytopes and polyhedral lifts, Yannakakis (Yannakakis 1991) showed that the minimal size of a lift equals the nonnegative rank of the polytope's slack matrix. This turned questions about extended formulations into questions about matrix factorizations, and it is the basis of the lower bounds of Fiorini, Massar, Pokutta, Tiwary and de Wolf (2012) for the cut, stable set and traveling salesman polytopes. Lift-and-project hierarchies (Sherali–Adams, Lovász–Schrijver, Lasserre) all produce lifts to nonnegative orthants or positive semidefinite cones, so a criterion for the existence of a lift is also a criterion for when such a hierarchy can succeed.

Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 38(2), 2013) extended Yannakakis' theorem from polytopes and polyhedral cones to arbitrary convex bodies and arbitrary closed convex cones. Their Theorem 2.4 is the target of this mission.

Timeline:

• 1991, Yannakakis: polytopes, polyhedral lifts, nonnegative factorizations of the slack matrix.
• 2012, Fiorini, Massar, Pokutta, Tiwary, de Wolf: superpolynomial lower bounds on polyhedral lifts via nonnegative rank; a positive semidefinite analogue for polytopes.
• 2011/2013, Gouveia, Parrilo, Thomas: convex bodies and general closed convex cones (Theorem 2.4), with psd rank as the semidefinite analogue of nonnegative rank.

Setting

Throughout, $\mathbb R^k$ carries the Euclidean inner product $\langle\cdot,\cdot\rangle$.

A convex body is a set $C \subseteq \mathbb R^n$ that is convex, compact, and contains the origin in its interior. Its polar is

$$C^\circ = \{\, y \in \mathbb R^n : \langle x, y\rangle \le 1 \text{ for all } x \in C \,\}.$$

A point $p \in C$ is an extreme point if $p = (p_1+p_2)/2$ with $p_1,p_2\in C$ forces $p_1 = p_2 = p$; $\operatorname{ext}(C)$ is the set of extreme points. The slack operator of $C$ is

$$S_C : \operatorname{ext}(C)\times\operatorname{ext}(C^\circ) \to \mathbb R, \qquad S_C(x,y) = 1 - \langle x,y\rangle .$$

It is nonnegative, and for a polytope it is the slack matrix: rows indexed by vertices, columns by facet normals.

Let $K \subseteq \mathbb R^m$ be a full-dimensional closed convex cone: closed, convex, closed under nonnegative scaling, with nonempty interior. Its dual is $K^* = \{y : \langle x,y\rangle \ge 0 \ \forall x\in K\}$.

• A $K$-lift of $C$ is $Q = K\cap L$, where $L\subseteq\mathbb R^m$ is an affine subspace and $\pi:\mathbb R^m\to\mathbb R^n$ is a linear map with $C = \pi(K\cap L)$. The lift is proper if $L$ meets the interior of $K$ (Definition 2.1).
• $S_C$ is $K$-factorizable if there are maps, not necessarily linear, $A:\operatorname{ext}(C)\to K$ and $B:\operatorname{ext}(C^\circ)\to K^*$ with $S_C(x,y) = \langle A(x), B(y)\rangle$ for all $(x,y)$ (Definition 2.2).

In Lean these are IsConvexBody, IsClosedConvexCone, HasLift, HasProperLift and SlackFactorizable in the namespace ConeLifts.Factorization, together with the series' shared ConeLifts.Shared.polar and ConeLifts.Shared.dualCone.

Formalization targets

Goal: Theorem 2.4

For $n \ge 1$, a convex body $C\subseteq\mathbb R^n$ and a full-dimensional closed convex cone $K\subseteq\mathbb R^m$:

$$\bigl(C \text{ has a proper } K\text{-lift} \Rightarrow S_C \text{ is } K\text{-factorizable}\bigr) \;\wedge\; \bigl(S_C \text{ is } K\text{-factorizable} \Rightarrow C \text{ has a } K\text{-lift}\bigr).$$

The two implications are not an equivalence: the forward one assumes properness, and the lift produced by the converse may be improper.

Milestones

In the order the paper's proof uses them:

1. (§2, p. 3) $C = \operatorname{conv}(\operatorname{ext} C)$ and $C^\circ = \operatorname{conv}(\operatorname{ext} C^\circ)$.
2. (proof, p. 4) For every $c\in\operatorname{ext}(C^\circ)$, $\max\{\langle c,x\rangle : x\in C\} = 1$, attained.
3. (proof, p. 4) If $C = \pi(K\cap L)$, $L = w_0 + L_0$ and $w_0\in\operatorname{int}K$, then for $c \in \operatorname{ext}(C^\circ)$

$$1 = \min\{\langle w_0, z\rangle : z - \pi^*(c)\in K^*,\ z\in L_0^\perp\},$$

with the minimum attained. 4. (proof, p. 5) For $L = \{(x,z) : 1-\langle x,y\rangle = \langle z, B(y)\rangle\ \forall y\in\operatorname{ext}(C^\circ)\}$ and its projection $L_K$ to $\mathbb R^m$: $0\notin L_K$. 5. (proof, p. 5) If $B$ maps into $K^*$, $z\in K$ and $(x,z)\in L$, then $x\in C$. 6. (proof, p. 5) For each $z\in K\cap L_K$ there is a unique $x_z$ with $(x_z,z)\in L$.

Significance

The result. Theorem 2.4 makes the existence of a lift of a convex body to a given cone a purely algebraic question about its slack operator. Every lower bound on lift size in the paper and its successors goes through it: the nonnegative-rank bounds for polytopes (Section 4 of the paper), the proof that the stable set polytope of an $n$-vertex graph has no lift to $\mathcal S^n_+$ (Section 5), and the later psd-rank literature. It also puts Yannakakis' theorem and its semidefinite analogue under a single statement.

Formalizing it. The theorem is proved on paper; no machine-checked version is known to exist. Formalizing it requires conic strong duality with dual attainment under a Slater condition, which Mathlib does not have, and finite-dimensional Krein–Milman for the polar body. The companion missions of this series (nonnegative-rank lower bounds; stable set polytopes and psd lifts) use the correspondence as their entry point.

Difficulty

The converse half is elementary once the extreme points of $C^\circ$ are known to generate it. The forward half is not: $B(c)$ must be an element of $K^*$ that certifies $\langle c, x\rangle \le 1$ on $C$ through the lift. A separating functional gives this certificate on $\pi(K\cap L)$, but writing it as $z - \pi^*(c)$ with $z \perp L_0$, $z - \pi^*(c)\in K^*$ and $\langle w_0,z\rangle = 1$ exactly is conic duality with a zero gap and an attained dual optimum. For closed convex cones the gap can be positive or the dual unattained unless a constraint qualification holds; this is why properness is assumed. Weak duality alone gives only $\ge 1$, and a dual sequence approaching $1$ does not yield a factor. The paper notes (p. 5) that, since the proof uses strong duality, it is not obvious how to remove properness for a general closed convex cone.

Formalization scope

Conventions fixed by the Lean statements:

• $\mathbb R^k$ is EuclideanSpace ℝ (Fin k); every pairing, in $S$, in $K^*$ and in the factorization, is its inner product.
• The polar is one-sided, $\langle x,y\rangle\le 1$; Mathlib's absolute polar is not used.
• A convex body is compact, convex, with $0$ in its interior. The paper's "full-dimensional convex body in $\mathbb R^n$" is read as including $n\ge 1$: for $n = 0$, $C = \{0\}$ has the proper $\mathbb R^m$-lift $\{0\}$ while $S_C(0,0) = 1$ cannot factor through $K^* = \{0\}$, so the forward half is false there. The goal and milestones 2–3 assume $1\le n$.
• $K$ is closed, convex, contains $0$ and is closed under nonnegative scaling; full-dimensionality is (interior K).Nonempty. Pointedness is not assumed.
• $L$ is a Mathlib AffineSubspace and $\pi$ a linear map; the lift condition is the set equality $C = \pi(K\cap L)$.
• $A, B$ are total functions $\mathbb R^n\to\mathbb R^m$ constrained only on $\operatorname{ext}(C)$, resp. $\operatorname{ext}(C^\circ)$, which is equivalent to maps out of the extreme points. They are not required to be linear or continuous.
• Milestone 3 is the second, substituted form of the paper's dual ($z = M^{\mathsf T}y$), stated with L.directionᗮ and LinearMap.adjoint π; minima and maxima are stated with IsLeast/IsGreatest, so attainment is part of every claim.

Trivializing readings are excluded: $\pi$ is linear, not an arbitrary function (with an arbitrary function every set is a "lift"); $L$ is an affine subspace, not an arbitrary set; and $B$ takes values in $K^*$, not $K$, which for a cone that is not self-dual would be a different and generally false statement.

Needed infrastructure: finite-dimensional Krein–Milman in the form $C = \operatorname{conv}(\operatorname{ext} C)$ for compact convex sets (Mathlib has the closure form); the bipolar theorem $(C^\circ)^\circ = C$ for closed convex $C\ni 0$ with the one-sided polar; compactness of $C^\circ$ when $0\in\operatorname{int} C$; and conic linear programming duality with a Slater point, including dual attainment. The last two are reusable well beyond this mission. Proofs of individual milestones, and of these general facts as separate lemmas, are welcome.

Selected references

• J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Mathematics of Operations Research 38(2):248–264, 2013. arXiv:1111.3164v2, doi:10.1287/moor.1120.0575
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43(3):441–466, 1991. doi:10.1016/0022-0000(91)90024-Y
• S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary, R. de Wolf, Linear vs. semidefinite extended formulations: exponential separation and strong lower bounds, STOC 2012. arXiv:1111.0837

Motivation

Max $k$-cover is the basic coverage problem of combinatorial optimization. The input is a collection of subsets of a finite ground set and a number $k$; the task is to choose $k$ subsets that together cover as many points as possible. It models facility and sensor placement, the selection of a small committee or feature set representing a population, and budgeted versions of set cover. It is also the prototype of maximizing a monotone submodular function under a cardinality constraint.

The greedy algorithm covers at least a $1-1/e\approx 0.632$ fraction of the optimum. This bound goes back to Hochbaum and Pathria and, for general submodular functions, to Nemhauser, Wolsey and Fisher (1978). For two decades it was not known whether a polynomial-time algorithm could do better. Uriel Feige answered the question in A Threshold of ln n for Approximating Set Cover (J. ACM 45(4), 1998, pp. 634–652, doi:10.1145/285055.285059), Section 5. His Theorem 5.3 (p. 648) states: "For any $\epsilon > 0$, max $k$-cover cannot be approximated in polynomial time within a ratio of $(1 - 1/e + \epsilon)$, unless $P = NP$." Together with the greedy bound, it makes $1-1/e$ the exact approximation threshold of max $k$-cover.

Timeline:

• 1978: Nemhauser, Wolsey and Fisher prove the greedy $1-1/e$ bound for monotone submodular maximization.
• 1992: Arora, Lund, Motwani, Sudan and Szegedy prove the PCP theorem. With Papadimitriou–Yannakakis (1991) it gives Theorem 2.1.1 of the paper: MAX 3SAT-B has a constant gap unless P = NP.
• 1994: Lund and Yannakakis introduce partition-system reductions from multi-prover proof systems to set cover.
• 1995: Raz proves the parallel repetition theorem (Theorem 2.2.2 of the paper).
• 1998: Feige proves the ln n threshold for set cover (the subject of mission I of this series) and the $1-1/e$ threshold for max $k$-cover.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$, a list of subsets $S_1,\dots,S_s$ of the points, and a number $k$. Its value $\mathrm{opt}$ is the largest number of points covered by at most $k$ of the sets. Instances are written over a three-letter alphabet:

• $n$ in unary;
• each set as its characteristic bit-vector;
• $k$ in unary.

Following p. 648, a polynomial-time algorithm approximates max $k$-cover within a ratio $\delta$ if on every input it outputs a number $v$ with

$$\delta\cdot\mathrm{opt}\le v\le\mathrm{opt}.$$

The algorithm need not name the sets. This is the non-constructive notion of approximation.

The proof is a reduction from the MAX 3SAT-5 problem. A 3CNF-5 formula has exactly three literals per clause, over three distinct variables, and every variable occurs in exactly five clauses. The reduction goes through a $k$-prover proof system for such a formula $\varphi$ with $M$ clauses:

• The verifier picks $\ell$ clauses at random, and a distinguished variable in each; there are $R=(3M)^\ell$ random strings $r$.
• Each prover $P_i$ is attached to a code word of length $\ell$ and weight $\ell/2$; distinct words are at Hamming distance at least $\ell/3$.
• On coordinate $j$, prover $P_i$ receives the clause if its bit is 1, and the distinguished variable if its bit is 0.
• Answers are satisfying assignments of the received clauses and bits for the received variables.
• Two provers are consistent if they assign the same values to the distinguished variables. The verifier weakly accepts if some pair of distinct provers is consistent, and strongly accepts if every pair is.

The max $k'$-cover instance of §5 attaches to every random string $r$ a copy $B_r$ of the explicit partition system. Its points are the vectors in $\{0,\dots,k-1\}^L$ with $L=2^\ell$, so $m=k^L$. Its $L$ partitions are labelled by the $\ell$-bit strings, and each splits the points by the value of one coordinate. There are $N=mR$ points in all. For each prover $i$, question $q$ and answer $a$, the set $S_{(q,a,i)}$ collects, for every $r$ on which $P_i$ receives $q$, the $i$th part of the partition of $B_r$ labelled by the values that $a$ gives to the distinguished variables of $r$. The budget is $k'=kQ$, where $Q$ is the number of questions a single prover can receive.

Formalization targets

Goal: Theorem 5.3

$$\forall\varepsilon>0:\quad \text{max } k\text{-cover is approximable within } 1-\tfrac1e+\varepsilon \ \Longrightarrow\ \mathrm{P}=\mathrm{NP},$$

conditional on the two cited results below. The ratio is left free (any $\varepsilon>0$), so the goal records the shape of the threshold and not a particular constant.

Milestones

• Proposition 2.1.2 (p. 640): for some $\varepsilon>0$ it is NP-hard to distinguish satisfiable 3CNF-5 formulas from those in which at most a $(1-\varepsilon)$-fraction of the clauses can be satisfied simultaneously.
• Lemma 2.3.1 (p. 643): a satisfiable $\varphi$ admits a strategy that always strongly accepts; on a far-from-satisfiable $\varphi$ the weak acceptance probability is at most $k^2\,2^{-c\ell}$.
• Coverage of the explicit partition system (p. 649): $j$ subsets from pairwise different partitions cover exactly $(1-(1-1/k)^j)m$ points.
• Proposition 5.4 (p. 649): if at most $kQ$ sets cover a $(1-1/e+\varepsilon)$-fraction of the points, then at least an $\varepsilon/3$-fraction of the random strings are good. Here $r$ is good if $w_r\le3k/\varepsilon$ sets meet $B_r$ and two of them from different provers lie in the same partition.
• Decoding (p. 649): such a covering yields a strategy that weakly accepts with probability at least $(\varepsilon/3)(\varepsilon/3k)^2$.
• Gap (p. 649): a satisfiable formula gives a cover of all $N$ points by $kQ$ sets. If at most a $(1-\varepsilon')$-fraction of the clauses are satisfiable, $kQ$ sets cover at most $(1-1/e+g(k))N$ points, where $g(k)\to0$, for all large $\ell$.
• Proposition 5.1 (p. 647): every greedy run covers at least $(1-1/e)\,\mathrm{opt}$ points.

Significance

The result closes the approximability of max $k$-cover: the greedy algorithm cannot be beaten by any constant unless P = NP. Consequences:

• Submodular maximization. Coverage functions are monotone submodular, so the bound transfers to monotone submodular maximization under a cardinality constraint, whenever the function is given in a form that encodes a coverage instance.
• Other problems. Hardness results for facility location, budgeted allocation, and welfare maximization with coverage valuations reduce from it.
• The reduction itself. The $\ell$-fold $k$-prover system combined with a partition system that is exactly countable is the template for later $1-1/e$ hardness proofs.

Status: the theorem has been proved since 1998. It has not been formalized; neither the reduction nor the underlying proof systems exist in Mathlib or on this platform. This mission produces:

• a machine-checked reduction from MAX 3SAT-5 to max $k$-cover;
• an exact counting lemma for product partition systems;
• the averaging and concavity argument of Proposition 5.4;
• a formal statement of the greedy bound for coverage.

The cited PCP-based gap (Theorem 2.1.1) and parallel repetition (Theorem 2.2.2) remain hypotheses. They are separate, much larger formalization projects.

Difficulty

The obvious argument uses the soundness of the proof system directly: a large cover should force consistent answers. It fails because a cover may spend many sets on a few random strings and cover them completely, while covering the rest partially without any two sets from the same partition. What saves the argument is exact counting. For sets from pairwise different partitions, coverage is exactly $h(j)=(1-(1-1/k)^j)m$, a concave function of the number $j$ of sets used. Since the sets meet a random string $k$ times on average, Jensen's inequality caps the total coverage of such "unstructured" strings at about $(1-(1-1/k)^k)$, which tends to $1-1/e$. A further obstacle is that the reduction must run in polynomial time. The paper therefore takes $\ell$ and $k$ constant (unlike the set-cover reduction, where $\ell=\Theta(\log\log n)$), and the soundness bound $k^2 2^{-c\ell}$ must beat $(\varepsilon/3)(\varepsilon/3k)^2$ at a constant $\ell$. The quantifier order ($k$ large first, then $\ell$ large) is part of the difficulty.

A second obstacle is the machine model. The goal is a statement about polynomial-time Turing machines, so the reduction and the decision procedure built from a hypothetical approximation algorithm must be compiled into Cook's one-tape machines.

Formalization scope

• Machine model. CookPvsNP_defs (a published platform definition): one-tape Turing machines, $\mathrm{P}$, $\mathrm{NP}$, polynomial-time computable functions, CNF formulas and their encoding. "P = NP" is P Bool = NP Bool, the form in which CookPvsNP.P_ne_NP states the open problem.
• Cited results as hypotheses. Theorem 2.1.1 enters as Thm211. Raz's theorem enters as RazRepetition, its consequence stated on p. 642: the $\ell$-fold clause–variable game on a far-from-satisfiable 3CNF-5 formula has acceptance probability at most $2^{-c\ell}$. This is weaker than Raz's general theorem, so the conditional statement is stronger. No hypothesis about max $k$-cover is assumed.
• Approximation. The value form above, with no size threshold. For $\varepsilon>1/e$ the ratio exceeds one and the hypothesis is unsatisfiable on any instance with $\mathrm{opt}>0$; those values are vacuous, as in the paper.
• $\mathrm{opt}$. Taken over at most $k$ sets. This agrees with the paper's "exactly $k$" whenever $k\le s$.
• Probability and counting. Probabilities are uniform counts over the $(3M)^\ell$ random strings. Fractions in lower-bound statements are written as counts compared with multiples of $R$.
• Canonical answers. The type of answers is restricted to satisfying assignments of the received clauses, following the paper's "without loss of generality" (p. 643). All indices are 0-based.
• Partition system. The §4 construction is defined for any partition system with $\ell$-bit partition labels and instantiated with the explicit product system. Its $L=2^\ell$ coordinates are the $\ell$-bit strings themselves.
• Not formalized. The running time of the greedy algorithm, and the constructive variant (Proposition 5.2), which belongs to the set-cover mission.

A trivializing formalization is ruled out: every cited input is a named, satisfiable proposition about 3CNF formulas or the two-prover game, never about max $k$-cover, and the approximation hypothesis is satisfiable for ratios up to $1$.

Needed infrastructure, reusable beyond this mission:

• composition and simulation lemmas for Cook's machines;
• the uniformity of the verifier's questions on 3CNF-5 formulas;
• concavity of $j\mapsto 1-(1-1/k)^j$;
• $(1-1/k)^k\to 1/e$ bounds.

Contributions to any of these, or to either cited theorem, are welcome.

Selected references

• U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4) (1998) 634–652. https://doi.org/10.1145/285055.285059
• R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3) (1998) 763–803 (STOC 1995). https://doi.org/10.1137/S0097539795280895
• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3) (1998) 501–555. https://doi.org/10.1145/278298.278306
• C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3) (1991) 425–440. https://doi.org/10.1016/0022-0000(91)90023-X
• C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5) (1994) 960–981. https://doi.org/10.1145/185675.306789
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions—I, Math. Programming 14 (1978) 265–294. https://doi.org/10.1007/BF01588971
• S. Cook, The P versus NP problem, Clay Mathematics Institute. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Variational inequalities and complementarity problems are the standard formulation of equilibrium in operations research and mathematical economics: traffic equilibria, spatial price equilibria, Nash equilibria of convex games, and the optimality conditions of constrained optimization all take this form. Many applications have two features that the classical theory does not cover. The feasible set of a player or a flow can depend on the current state (a quasi-variational inequality, as in generalized Nash games with shared constraints), and the response map can be set-valued (a subdifferential, or a best-response correspondence). D. Chan and J. S. Pang (Math. Oper. Res. 7 (1982) 211–222) introduced the generalized quasi-variational inequality covering both, proved existence theorems for it, and derived existence for a new generalized implicit complementarity problem.

Timeline of the results this mission builds on:

• 1966: Hartman and Stampacchia prove existence for the variational inequality on a compact convex set.
• 1973: Bensoussan, Goursat and Lions introduce quasi-variational inequalities for impulse control.
• 1976: Saigal extends the complementarity problem to set-valued maps.
• 1974: Moré gives coercivity conditions for nonlinear complementarity problems; a special version of the lemma of §3 appears there.
• 1979: Fang and Peterson prove a general existence theorem for generalized variational inequalities (report, University of Maryland Baltimore County); the lemma of §3 and the constant-$K$ case of Theorem 3.2 are taken from there.
• 1982: Chan and Pang prove existence for the generalized quasi-variational inequality using the Eilenberg–Montgomery fixed point theorem, and derive existence for the generalized implicit complementarity problem under strong copositivity (Theorem 4.2), the goal of this mission.

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $x^T y$ and norm $\|x\|$. A point-to-set mapping $K$ assigns to each $x\in\mathbb R^n$ a set $K(x)\subseteq\mathbb R^n$. Given point-to-set mappings $K$ and $f$, the problem $\mathrm{GQVI}(K,f)$ asks for vectors $x,y$ with

$$x\in K(x),\qquad y\in f(x),\qquad (x'-x)^T y\ge 0\ \text{ for all } x'\in K(x).$$

A cone is a convex set containing $0$ and closed under nonnegative scaling. The dual cone of a set $S$ is $S^*=\{y : y^T x\ge 0 \text{ for all } x\in S\}$. For a point-to-point map $m$, a cone-valued map $L$ and a point-to-set map $f$, the problem $\mathrm{GICP}(L,m,f)$ asks for $x,y$ with

$$x\in m(x)+L(x),\qquad y\in f(x)\cap L(x)^*,\qquad y^T\big(x-m(x)\big)=0 .$$

A mapping $f$ is upper semicontinuous on a set $C$ at $x\in C$ if for each open $G\supseteq f(x)$ there is a neighbourhood $N$ of $x$ with $f(y)\subseteq G$ for $y\in N\cap C$; lower semicontinuous if for each open $G$ meeting $f(x)$, $f(y)$ meets $G$ for all $y$ near $x$ in $C$; continuous if both. A set $S$ is contractible if some point $x\in S$ and a continuous $g:S\times[0,1]\to S$ satisfy $g(x',0)=x'$, $g(x',1)=x$. $B_r$ is the closed ball of radius $r$ about the origin, $C_r$ its boundary sphere. For point-to-set maps $\mu$ and $K$, the coercivity function is

$$C_{\mu,K}(r,x^0)=\inf_{x\in K(x)\cap C_r}\Big[\inf_{y\in\mu(x)}(x-x^0)^T y\Big]\Big/(r+\|x^0\|),$$

with $\inf\emptyset=+\infty$. The map $\mu$ is strongly copositive with respect to $K$ at $x^0$ if $x^0\in K(x^0)$ and for some $\alpha>0$ and $y^0\in\mu(x^0)$, $(y-y^0)^T(x-x^0)\ge\alpha\|x-x^0\|^2$ for all $x\in K(x)$ and $y\in\mu(x)$. For $\mu$ and $q\in\mathbb R^n$, $(\mu+q)(x)=\{y+q : y\in\mu(x)\}$.

Formalization targets

Goal: Theorem 4.2 (p. 218)

Let $\tilde L$ be a closed cone with nonempty interior, $m$ continuous, $K(x)=m(x)+\tilde L$, and $\mu$ a mapping with nonempty contractible compact values, upper semicontinuous on $\mathbb R^n$. If some $\tilde u$ satisfies $\tilde u-m(x)\in\tilde L$ for all $x$, and $\mu$ is strongly copositive with respect to $K$ at $\tilde u$, then for every $q$

$$\exists\, x,y:\quad x-m(x)\in\tilde L,\quad y\in\mu(x)+q,\quad y\in\tilde L^*,\quad y^T(x-m(x))=0 .$$

Milestones, in the order the proof uses them

• Theorem 3.1 (p. 214): for continuous $\varphi$ quasi-concave in its first argument on a nonempty compact convex $C$, some $u^*\in V(u^*)=K(u^*)\cap C$ and $w^*\in f(u^*)$ satisfy $\varphi(v,u^*,w^*)\le\varphi(u^*,u^*,w^*)$ for all $v\in V(u^*)$.
• Lemma of §3 (p. 215): a variational inequality on $W\cap E$ at a point of $W\cap E^0$ extends to $W$.
• Theorem 3.2 (p. 215): existence for $\mathrm{GQVI}(K,f)$ from a compact truncation $C=U\cap E$ and a boundary condition on $\partial E$.
• Theorem 4.1 (p. 217): if $C_{\mu,K}(r,x^0)\ge 0$, then $\mathrm{GQVI}(K,\mu+q)$ has a solution in $B_r$ whenever $\|q\|\le C_{\mu,K}(r,x^0)$.
• Corollary 4.1 (pp. 217–218): under the coercivity condition (4), $\mathrm{GQVI}(K,\mu+q)$ is solvable for every $q$, with bounded solution set.
• Lemma 4.1 (p. 218): strong copositivity at $x^0$ implies coercivity (4) at $x^0$.
• Proposition 2.1 (p. 213): $\mathrm{GICP}(L,m,f)$ and $\mathrm{GQVI}(m+L,f)$ have the same solutions.

Significance

Theorem 4.2 gives existence for complementarity problems whose cone is translated by a state-dependent map $m$ and whose response map is set-valued. It contains existence for the implicit complementarity problem of Capuzzo-Dolcetta, Mosco and Pang ($\tilde L=\mathbb R^n_+$) with strongly monotone data (Corollary 4.2 of the paper), and Saigal's generalized complementarity problem ($m\equiv0$). Theorems 3.2 and 4.1 are general-purpose existence tools for quasi-variational inequalities with set-valued maps; Theorem 3.2 reduces to the Fang–Peterson theorem when $K$ is constant, and Corollary 3.1 to the Hartman–Stampacchia theorem when in addition $f$ is single-valued.

All results of the paper are proved; none is open. To our knowledge none of them has been formalized: no proof assistant library contains quasi-variational inequalities with set-valued maps, and Mathlib has neither Kakutani's nor the Eilenberg–Montgomery fixed point theorem (nor Brouwer's). A formal proof of the goal therefore also produces a reusable library of set-valued existence theory.

Difficulty

The whole chain rests on Theorem 3.1, whose proof applies the Eilenberg–Montgomery fixed point theorem for upper semicontinuous maps with acyclic (here contractible) compact values; this in turn needs either singular homology or an approximation argument, neither of which is available in Mathlib. Replacing "contractible" by "convex" to use Kakutani's theorem would prove a strictly weaker theorem: the paper states contractible values deliberately. The second difficulty is that the fixed point only solves the problem on the truncation $V(x)=K(x)\cap C$; turning it into a solution over all of $K(x)$ needs the boundary argument of Theorem 3.2, and for Theorem 4.2 the continuity of $x\mapsto (m(x)+\tilde L)\cap B_\rho$, which is where the solidity of $\tilde L$ is used. The obvious approach of applying Theorem 3.2 directly with $C=\mathbb R^n$ fails because $C$ must be compact.

Formalization scope

The space is EuclideanSpace ℝ (Fin n), so all norms and balls are Euclidean (not the sup norm of Fin n → ℝ). Point-to-set mappings are functions into Set; semicontinuity "on $C$" is Mathlib's UpperHemicontinuousOn/LowerHemicontinuousOn with neighbourhoods relative to $C$, and "on $\mathbb R^n$" is UpperHemicontinuous. Cones are PointedCone ℝ _ (convex, containing $0$, as footnote 1 of the paper says). Balls are centred at the origin.

Conventions that the Lean statements make explicit:

• The paper takes its semicontinuity from Berge, whose upper semicontinuous maps have compact values. Theorems 3.1, 3.2, 4.1 and Corollary 4.1 are false without this ($K(x)\equiv(0,1)$, $C=[0,1]$, $f\equiv\{1\}$), so each one carries an explicit closedness hypothesis on $K(x)\cap C$ or $K(x)\cap B_\rho$. Theorem 4.2 needs none, since $m(x)+\tilde L$ is closed.
• Every infimum uses $\inf\emptyset=+\infty$. Bounds of the form $C_{\mu,K}(r,x^0)\ge c$, condition (v) of Theorem 3.2, and the limit (4) are stated in universally quantified form. A real-valued $C_{\mu,K}$ would be wrong: it returns $0$ on an empty set.
• Lemma 4.1 is stated at the same point $x^0$, which is what its proof gives. In Corollary 4.1 the bound $r$ on the solutions is chosen after $q$.
• Three glyphs are illegible in the scan and are read from the proofs: $\le$ in Theorem 3.1, $\ge 0$ in Theorem 3.2(v), and $\ge$ in the Lemma of §3.

A trivializing formalization is ruled out: the GQVI solution tests over all of $K(x)$, not over $V(x)=K(x)\cap C$, and the GICP solution keeps both the dual-cone condition and the complementarity equation. Dropping any of these would turn the goal into a restatement of Theorem 3.1.

A complete development needs: an Eilenberg–Montgomery (or at least Kakutani plus an acyclicity argument) fixed point theorem for set-valued maps, Berge's maximum theorem, and basic facts on hemicontinuity of intersections and translates of set-valued maps. The fixed point theorems, the maximum theorem and the hemicontinuity lemmas are reusable far beyond this mission. Contributions of any of these as separate theorems are welcome.

Selected references

• D. Chan, J. S. Pang, The generalized quasi-variational inequality problem, Mathematics of Operations Research 7(2) (1982) 211–222. https://doi.org/10.1287/moor.7.2.211
• S. Eilenberg, D. Montgomery, Fixed point theorems for multi-valued transformations, American Journal of Mathematics 68 (1946) 214–222. https://doi.org/10.2307/2371832
• C. Berge, Topological Spaces, Macmillan, New York, 1963.
• S. C. Fang, E. L. Peterson, Generalized variational inequalities, Mathematics Research Report 79-10, Department of Mathematics, University of Maryland Baltimore County, 1979 (no public link).
• J. J. Moré, Coercivity conditions in nonlinear complementarity problems, SIAM Review 16(1) (1974) 1–16. https://doi.org/10.1137/1016001
• P. Hartman, G. Stampacchia, On some non-linear elliptic differential-functional equations, Acta Mathematica 115 (1966) 271–310. https://doi.org/10.1007/BF02392210
• R. Saigal, Extension of the generalized complementarity problem, Mathematics of Operations Research 1(3) (1976) 260–266. https://doi.org/10.1287/moor.1.3.260