Convex Optimization

Motivation

Matroids and their integral generalizations, integral base polytopes, are the combinatorial structures on which the greedy algorithm is exact. Edmonds' theory relates them to submodular and supermodular set functions: a polytope is a base polytope exactly when its support function, restricted to $0/1$ vectors, is supermodular and the greedy formula evaluates it everywhere. Dress and Wenzel's valuated matroids (1990) and Murota's M-concave functions carry the exchange axiom from sets to functions on sets. This paper (Adv. Math. 124, 1996) sets up the resulting theory of discrete concave functions on base sets, later developed into discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003).

The question behind this mission is how the set-level correspondence between exchange and supermodularity extends to functions. Section 5 of the paper answers it with the Local Supermodularity Theorem: the exchange property of a function is a supermodularity property of its concave conjugate, holding locally at every point.

Setting

Let $V$ be a finite nonempty set, $n=|V|$. For $u\in V$ let $\chi_u\in\mathbb Z^V$ be the unit vector, for $X\subseteq V$ let $\chi_X$ be its characteristic vector, $x(X)=\sum_{v\in X}x(v)$, and $\langle p,x\rangle=\sum_v p(v)x(v)$. For a finite $B\subseteq\mathbb Z^V$, $\overline B$ is its convex hull.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that

$$\text{(B1)}\quad x,y\in B,\ u\in\operatorname{supp}^+(x-y)\ \Rightarrow\ \exists v\in\operatorname{supp}^-(x-y):\ x-\chi_u+\chi_v\in B.$$

A function $\omega:B\to\mathbb R$ satisfies the exchange property (EXC) (is M-concave) if for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v,\ y+\chi_u-\chi_v\in B$ and $\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v)$. Write $\omega[p](x)=\omega(x)+\langle p,x\rangle$ and $\operatorname{argmax}(g)$ for the maximizers of $g$ on $B$.

The support function of $B$ is $\psi^\circ(p)=\min\{\langle p,x\rangle\mid x\in B\}$. A positively homogeneous $h:\mathbb R^V\to\mathbb R$ is "matroidal" if

• (C1) $X\mapsto h(\chi_X)$ is supermodular, and
• (C2) $h(p)=\sum_{j=1}^n(p_j-p_{j+1})\,h(\chi_{V_j})$ whenever $V=\{v_1,\dots,v_n\}$ with $p(v_1)\ge\dots\ge p(v_n)$, $p_j=p(v_j)$, $V_j=\{v_1,\dots,v_j\}$, $p_{n+1}=0$.

The concave conjugate is $\omega^\circ(p)=\min\{\langle p,x\rangle-\omega(x)\mid x\in B\}$, the concave closure is $\hat\omega(b)=\inf_p\{\langle p,b\rangle-\omega^\circ(p)\}$, the subdifferential is $\partial\omega^\circ(p_0)=\{b\mid\omega^\circ(p)-\omega^\circ(p_0)\le\langle p-p_0,b\rangle\ \forall p\}$, and the localization of $\omega^\circ$ at $p_0$ is $\hat L(\omega^\circ,p_0)(p)=\inf\{\langle p,b\rangle\mid b\in\partial\omega^\circ(p_0)\}$.

Formalization targets

Goal: the Local Supermodularity Theorem (Theorem 5.3, corrected)

For $\omega$ on a finite integral base set $B$,

$$\omega\ \text{satisfies (EXC)}\iff\Big(\omega=\hat\omega\ \text{on}\ B\Big)\ \text{and}\ \Big(\hat L(\omega^\circ,p_0)\ \text{is "matroidal" for every}\ p_0\in\mathbb R^V\Big).$$

The printed Theorem 5.3 has only the second condition on the right. Its "only if" direction holds as printed; its "if" direction is false without the first condition, and a separate item of the mission states the counterexample: $B=\{(2,0),(1,1),(0,2)\}$, $\omega=(0,-10,0)$.

Milestones

1. Theorem 2.1: (B1) is equivalent to $B$ being the integer points of an integral submodular (equivalently, supermodular) system, whose defining function is determined by $B$.
2. Theorem 5.1: if $B=\mathbb Z^V\cap\overline B$, then $B$ satisfies (B1) iff $\psi^\circ$ is "matroidal".
3. Lemma 5.2: sums of "matroidal" functions are "matroidal".
4. Theorem 4.4: (EXC) holds iff every $\operatorname{argmax}(\omega[p])$ satisfies (B1).
5. Eq. (5.12): $\hat L(\omega^\circ,p_0)(p)=\min\{\langle p,x\rangle\mid x\in\operatorname{argmax}(\omega[-p_0])\}$.

Significance

The result. Theorem 5.3 is the function-level version of Theorem 5.1. Condition (C1) is a supermodularity condition, so the theorem expresses (EXC) as "a collection of local supermodularity" properties of $\omega^\circ$, in the same way that (B1) corresponds to supermodularity of a support function. In the paper this characterization of the conjugate side underlies the Fenchel-type duality of Section 6, and more generally the conjugacy between M-concave and L-convex functions in discrete convex analysis.

The formalization. No part of this theory is formalized in Lean or on this platform: base sets, (EXC), "matroidal" functions and concave conjugates of functions on base sets are all new. The mission also corrects the published statement: the reduction from localizations to base sets needs every integer point of $\operatorname{conv}(\operatorname{argmax}\,\omega[-p_0])$ to be a maximizer, and the concave-closure condition supplies this. A machine-checked proof would settle both the corrected theorem and the counterexample. Theorem 2.1 and Lemma 5.2 are classical but have no formal proof either.

Difficulty

$\omega^\circ$ depends only on the concave closure $\hat\omega$, so any characterization of (EXC) through $\omega^\circ$ alone cannot see values of $\omega$ below $\hat\omega$. That is why the goal needs the extra clause. The "only if" direction needs the full theory of Section 4: M-concave functions coincide with their concave closure, and all their maximizer sets are base sets. Theorem 5.1 needs the greedy algorithm on integral base polytopes, together with the fact that the base polytope of an integral supermodular function has integral vertices. Theorem 2.1 is the folklore statement that polyhedral and exchange descriptions agree, and the paper does not prove it. Eq. (5.12) needs the subdifferential of a finite minimum of affine functions to be the convex hull of the active gradients, stated globally rather than only near $p_0$.

Formalization scope

Integer vectors are V → ℤ, real vectors V → ℝ, with [Fintype V] [DecidableEq V] [Nonempty V]. A finite subset of $\mathbb Z^V$ is a Finset (V → ℤ). A function on $B$ is a total function (V → ℤ) → ℝ whose values off $B$ are never used. The mission commits to the following readings:

• Minima. $\psi^\circ$, $\omega^\circ$ are real infima over the finite set $B$, hence minima for nonempty $B$ (every statement has $B$ nonempty). $\hat\omega$ is a real infimum used only at points of $B$, where it is bounded below.
• Localization. $\hat L$ is a real sInf over the subdifferential, defined by (5.8)–(5.9) exactly, not by the formula (5.12). Eq. (5.12) is stated with IsLeast, so it asserts attainment, not just the value.
• (C2). It is required for every bijection Fin n ≃ V along which $p$ is non-increasing. This is equivalent to "for some" such indexing. "Matroidal" includes positive homogeneity but not concavity.
• Theorem 2.1. The page's "$\forall X\subset V$" is read as all $X\subseteq V$. The set functions are integer-valued, and "Moreover" is read strongly: every $f$ (resp. $g$) as in (b) (resp. (c)) equals the displayed max (resp. min).
• Theorem 4.4. "$\overline{\operatorname{argmax}(\omega[p])}$ is an integral base polytope" is read as "$\operatorname{argmax}(\omega[p])$ satisfies (B1)", following Lemma 4.3 and the proof of Theorem 5.3. The literal convex-hull reading makes the "if" direction false (same counterexample).
• Theorem 5.1 keeps the page's hypothesis $B=\mathbb Z^V\cap\overline B$.

Trivializing formalizations are ruled out. Defining $\hat L$ by (5.12) would reduce the goal to Theorems 4.4 and 5.1. A "matroidal" without (C2) would be satisfied by support functions of non-base sets. An $\omega^\circ$ taken as a supremum would reverse the sign conventions.

The development needs: the greedy algorithm and integrality for integral base polytopes, supergradients of polyhedral concave functions, and the Section 4 results of the paper (concave closure of M-concave functions, Lemma 4.3). The base-set and "matroidal" layers can be reused beyond this mission. Proofs of any milestone, of the counterexample, and a proof of the "only if" direction on its own are all welcome.

Selected references

• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996), 272–311. https://doi.org/10.1006/aima.1996.0084
• A. W. M. Dress, W. Wenzel, Valuated matroids: a new look at the greedy algorithm, Applied Mathematics Letters 3 (1990), 33–35.
• S. Fujishige, Submodular Functions and Optimization, 2nd ed., Annals of Discrete Mathematics 58, Elsevier, 2005.
• L. Lovász, Submodular functions and convexity, in Mathematical Programming: The State of the Art, Springer, 1983, 235–257. https://doi.org/10.1007/978-3-642-68874-4_10
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

Motivation

Many engineering and economic planning problems must meet random requirements with a prescribed reliability: a reservoir must satisfy demand with probability at least $0.95$, a power system must cover load except on rare days, an inventory must avoid shortage with high probability. Probabilistic constrained programming (also called chance-constrained programming) models this by requiring that a system of random inequalities hold jointly with probability at least $p$.

The first obstacle to solving such problems is structural. The probability that random constraints are satisfied is, in general, neither concave nor convex in the decision, so the feasible set need not be convex and local search can stall. Prékopa's theory of logarithmically concave measures (1971–1973) removed that obstacle for a large class of distributions, and it is the basis of the numerical methods of Chapter 5 of Ermoliev and Wets, Numerical Techniques for Stochastic Optimization (Springer 1988). This mission formalizes the structural theorems of that chapter.

Timeline:

• 1959: Charnes and Cooper, individual chance constraints.
• 1971: Prékopa, logarithmic concave measures with application to stochastic programming (Acta Sci. Math. Szeged 32).
• 1973: Prékopa, logarithmic concave measures and functions (Acta Sci. Math. Szeged 34), containing the marginal theorem: marginals of log-concave functions are log-concave.
• 1970s–1980s: nonlinear programming methods for (5.1) (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) combined with Monte Carlo evaluation of $h_0$; the chapter surveys them.

Setting

Let $\xi$ be a random vector in $\mathbb R^q$ on a probability space $(\Omega, \mathcal F, P)$ and let $g_1, \dots, g_r : \mathbb R^n \times \mathbb R^q \to \mathbb R$. The chapter studies problem (5.1):

$$\min h(x) \quad \text{s.t.} \quad h_0(x) = P\bigl(g_1(x,\xi) \ge 0, \dots, g_r(x,\xi) \ge 0\bigr) \ge p, \quad h_1(x) \ge p_1, \dots, h_m(x) \ge p_m .$$

The function $h_0$ is the probability function (chanceProb in Lean). In the special case $g_i(x,y) = T_i x - y_i$ it equals $F(Tx)$, where $F$ is the joint distribution function of $\xi$.

A function $f \ge 0$ is logarithmically concave on a convex set $S$ if

$$f(\lambda u + (1-\lambda) v) \ge f(u)^{\lambda} f(v)^{1-\lambda}, \qquad u, v \in S,\ 0 < \lambda < 1 .$$

Where $f > 0$ this is concavity of $\log f$; the power form also makes sense where $f = 0$. Nondegenerate normal densities, uniform densities on convex bodies and exponential densities are log-concave.

Section 5.7 introduces the polynomial distribution (5.19) on the cube $0 < z_j \le 1$:

$$F(z_1, \dots, z_n) = \frac{1}{\sum_{i=1}^{N} c_i z_1^{\alpha_{i1}} \cdots z_n^{\alpha_{in}}}, \qquad c_i > 0,\ \alpha_{ij} \le 0,\ \textstyle\sum_j \alpha_{ij} < 0$$

(polyDistF in Lean).

Formalization targets

Goal: Theorem 5.1

If $g_1, \dots, g_r$ are jointly concave on $\mathbb R^{n+q}$ and $\xi$ has a log-concave density $f$ on $\mathbb R^q$, then

$$h_0 \text{ is logarithmically concave on } \mathbb R^n .$$

Its immediate consequence is that the feasible set $\{x : h_0(x) \ge p\}$ is convex for every $p$.

Milestones

1. Theorem 5.2.1: if $h$ is log-concave on the convex set $H = \{h \ge p\}$, $0 < p < 1$, then $h - p$ is log-concave on $H$. This makes the logarithmic penalty function (5.5) of the SUMT method convex.
2. Theorem 5.2.2: under the standing assumptions of §5.2, every interior point $z$ of the feasible set of (5.1) satisfies $h_i(z) > p_i$, $i = 0, \dots, m$.
3. Theorem 5.7.1 (proved content, (5.21)): for $n = 2$ and oppositely ordered exponents, $\partial^2 F / \partial z_1 \partial z_2 \ge 0$ on $(0,1)^2$.
4. Theorem 5.7.2: the polynomial distribution function is log-concave on $(0,1]^n$.

The platform theorem ConvexOptimization.prekopa_marginal_log_concave (Prékopa's marginal theorem, proved) is included as a reference item.

Significance

Theorem 5.1 turns a probabilistic constraint into a convex constraint after taking logarithms. This is what makes convergence proofs for nonlinear programming methods (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) applicable to (5.1) and to the reliability maximization problem (5.4); without it, those methods have no guarantee of finding a global optimum. Theorems 5.2.1 and 5.2.2 are the two facts that make the SUMT method of §5.2 well defined and convex on the interior of the feasible set. Theorem 5.7.2 shows that probabilistic constraints under the polynomial distribution define convex sets, so they can be added to geometric programmes.

On status: Theorem 5.1 is a classical result, proved in Prékopa's papers (the chapter itself refers to Prékopa's survey for the proof). Prékopa's marginal theorem and the Prékopa–Leindler inequality are already machine-checked on this platform; Theorem 5.1 and the §5.2 and §5.7 theorems are, as far as a search of the platform shows, not formalized. The work is formalizing known proofs, in the log-concavity predicate the platform already uses.

Difficulty

The obvious argument for Theorem 5.1, "the constraint set is convex and the density is log-concave, so the probability is log-concave", hides the real content: log-concavity of a probability as a function of a parameter is a statement about integrals, and it does not follow from pointwise properties of the integrand without a Prékopa–Leindler-type inequality. Concavity of each $g_i$ separately in $x$ and in $y$ is not enough; joint concavity in $(x, y)$ is used essentially. The probability function vanishes on large regions in typical examples, so any argument that takes logarithms pointwise fails at the boundary of its support.

For Theorem 5.2.2 the naive argument fails at the index $i = 0$: nothing about $h_0$ is assumed directly, and log-concavity of $h_0$ is exactly Theorem 5.1. For Theorem 5.7.1 the difficulty is a sign condition on a covariance; without the ordering hypothesis the mixed derivative can be negative.

Formalization scope

$\mathbb R^n$ and $\mathbb R^q$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin q); the constraint functions take pairs $(x, y)$ in the product, and concavity is ConcaveOn ℝ Set.univ on that product (joint concavity). A "continuous probability distribution with density $f$" is stated as P.map ξ = volume.withDensity (ENNReal.ofReal ∘ f) with $\xi$ and $f$ measurable and $P$ a probability measure. Log-concavity is the platform definition ConvexOptimization.LogConcaveOn (nonnegativity plus the power inequality), imported as a reference item; concavity of Real.log ∘ h₀ would be a different, wrong property because Lean's Real.log 0 = 0. Indices are 0-based (Fin r, Fin m, Fin N, Fin n); the probabilistic constraint $i = 0$ of Theorem 5.2.2 is stated separately from $h_1, \dots, h_m$. The polynomial distribution is a formula on Fin n → ℝ with real powers, used only on the cube.

No constant of the book is replaced by an explicit value: every result of this chapter is qualitative.

Corrections of the printed text, recorded in each item's Formalization Note:

• Theorem 5.1 states the density condition "for every $x_1, x_2 \in \mathbb R^n$"; the density lives on $\mathbb R^q$ and the condition is imposed there.
• (5.19) prints the first factor as $z_i^{\alpha_{i1}}$ and the domain index as $i = 1, \dots, N$; they are read as $z_1^{\alpha_{i1}}$ and $j = 1, \dots, n$.
• Theorem 5.7.1 prints its ordering hypothesis with transposed indices ($\alpha_{11} \le \alpha_{12} \le \dots \le \alpha_{1n}$); following the proof, it is read as: across the $N$ terms the $z_1$-exponents increase and the $z_2$-exponents decrease.
• Theorem 5.7.1 claims "is a probability distribution function"; the book proves only (5.21), and normalization would need $\sum_i c_i = 1$, which is not assumed. The formal statement is (5.21), the mixed derivative as an iterated deriv.

Theorem 5.2.2 carries all six assumptions of §5.2, including compactness of the feasible set and the Slater point; it does not assume log-concavity of $h_0$, which must be derived from the density and concavity hypotheses. A trivializing formalization, such as one with a density hypothesis that no probability law satisfies or a log-concavity predicate that holds for every function vanishing somewhere, is ruled out: the density hypotheses are satisfiable (checked locally) and LogConcaveOn is the multiplicative inequality at every pair of points.

Needed infrastructure: Prékopa's marginal theorem (available), log-concavity of indicators of convex sets and of products, measurability of the constraint set, and Artin's theorem that a sum of log-convex functions is log-convex (for Theorem 5.7.2). Artin's theorem and closure properties of LogConcaveOn are reusable beyond this mission, and contributions of them are welcome.

Selected references

• A. Prékopa, "Numerical Solution of Probabilistic Constrained Programming Problems", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 5, pp. 123–139. https://doi.org/10.1007/978-3-642-61370-8
• A. Prékopa, "Logarithmic concave measures with application to stochastic programming", Acta Sci. Math. (Szeged) 32 (1971), 301–316.
• A. Prékopa, "On logarithmic concave measures and functions", Acta Sci. Math. (Szeged) 34 (1973), 335–343.
• A. Charnes and W. W. Cooper, "Chance-constrained programming", Management Science 6 (1959), 73–79. https://doi.org/10.1287/mnsc.6.1.73
• B. L. Miller and H. M. Wagner, "Chance constrained programming with joint constraints", Operations Research 13 (1965), 930–945. https://doi.org/10.1287/opre.13.6.930
• A. Prékopa, Stochastic Programming, Kluwer 1995. https://doi.org/10.1007/978-94-017-3087-7

Motivation

Many design problems in control, finance and operations research are convex programs with uncertain constraints: a decision $\theta$ must satisfy $\theta\in\Theta_\delta$ for a parameter $\delta$ that is not known in advance. Enforcing the constraint for every possible $\delta$ (robust optimization) is often intractable or too conservative, and a chance-constrained formulation needs the distribution of $\delta$, which in practice is rarely known. The scenario approach replaces the uncertain constraint by the constraints of $N$ observed samples $\delta_1,\dots,\delta_N$ and solves the resulting ordinary convex program. The question it answers is how much of the unseen uncertainty the resulting decision still violates.

The answer, the generalization theorem of the scenario approach, is distribution-free: the probability that the scenario solution violates more than a fraction $\varepsilon$ of the uncertainty is bounded by a binomial tail that depends only on $N$ and on the number $d$ of decision variables. This mission formalizes that theorem as it is presented in Chapters 3 and 5 of Campi and Garatti's textbook Introduction to the Scenario Approach (SIAM/MOS 2018), the first mission of a series on the book.

Timeline. Calafiore and Campi introduced scenario programs and bounded the violation of their solutions through the count of support constraints (Math. Program. 2005; IEEE TAC 2006). Campi and Garatti proved in 2008 that the binomial-tail bound of Theorem 3.7 holds for every convex scenario program under existence and uniqueness of the solution, and that it is attained with equality by fully supported problems (SIAM J. Optim. 2008), which settled the tightness question. The textbook (DOI 10.1137/1.9781611975444) presents the theorem with a complete proof for fully supported problems in the plane.

Setting

Fix a cost vector $c\in\mathbb R^d$, a domain $\Theta\subseteq\mathbb R^d$, a measurable space $\Delta$ of uncertainty instances with a probability $\mathbb P$, and a constraint set $\Theta_\delta\subseteq\mathbb R^d$ for each $\delta\in\Delta$.

• The violation of a decision $\theta$ (Definition 3.1) is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$, the probability that $\theta$ fails the constraint of a fresh instance.
• For a sample $(\delta_1,\dots,\delta_m)$, the scenario program is

$$\min_{\theta\in\Theta}c^T\theta\quad\text{subject to}\quad\theta\in\bigcap_{i=1}^{m}\Theta_{\delta_i}.$$

A solution is a feasible point of least cost. With $m=N$ i.i.d. samples its solution is denoted $\theta^*$; it is a random vector, a function of the sample, and $V(\theta^*)$ is a random variable in $[0,1]$.

• Assumption 3.4 (convexity): $\Theta$ and every $\Theta_\delta$ are convex and closed. Assumption 3.6 (existence and uniqueness): for every $m$ and every sample, the program with $m$ constraints has exactly one solution.
• A constraint is a support constraint (Definition 5.1) if its removal improves the solution. A problem is fully supported (Definition 5.4) if for every $m\ge d$ the program with $m$ constraints has, with probability 1, exactly $d$ support constraints.

Formalization targets

Goal: Theorem 3.7

For $1\le d\le N$ and every $\varepsilon\in[0,1]$, under Assumptions 3.4 and 3.6,

$$\mathbb P^N\{V(\theta^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.$$

The right-hand side is the upper tail of a Beta$(d,N-d+1)$ distribution. The statement leaves $\mathbb P$, $\Theta$ and the constraint family completely unspecified beyond the two assumptions.

Milestones

1. Helly's lemma (Lemma 5.3), referenced from the platform in its $d$-dimensional form.
2. Theorem 5.2: for every $m$ and every sample, a convex scenario program has at most $d$ support constraints.
3. Eq. (5.3): for a fully supported problem with $d=N=2$, $\mathbb P^2\{V(\theta^*)>\varepsilon\}=1-\varepsilon^2$.
4. Eq. (5.2): for fully supported problems, Theorem 3.7 holds with equality.
5. Eqs. (3.5)–(3.6): the bound is the Beta$(d,N-d+1)$ distribution function (a published incomplete-beta identity).
6. Eq. (3.9): $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}\le 2^{d-1}(1-\varepsilon/2)^N\le2^{d-1}e^{-\varepsilon N/2}$.
7. Theorem 3.8: $\mathbb E[V(\theta^*)]\le d/(N+1)$.
8. Theorem 1.3: if $N\ge\frac2\varepsilon(\ln\frac1\beta+d-1)$, then $V(\theta^*)\le\varepsilon$ with probability at least $1-\beta$.

Significance

Theorem 3.7 is what makes the scenario approach usable as a design method: it certifies the reliability of a decision computed from data without any knowledge of the data-generating distribution, requiring only independence of the samples. Theorems 3.8 and 1.3 are its two most used consequences, an expected-violation bound and an explicit sample size, and later chapters of the book (constraint removal, the FAST algorithm, empirical-cost results) build on the same statement. Equality for fully supported problems shows that the bound cannot be improved for any $d$ and $N$.

The theorem is proved in the literature; it has no machine-checked proof. A formalization produces, beyond the result itself, a reusable library of scenario programs, violation probabilities and support constraints on which the rest of the series (constraint removal, nonconvex support sets) can be stated, and it checks the measure-theoretic content that the book deliberately leaves aside ("measurability issues are glossed over throughout", p. 33).

Difficulty

The deterministic part, at most $d$ support constraints, is a short consequence of Helly's theorem. The probabilistic part is where the obvious approach fails. A uniform-convergence argument over all $\theta$ (Vapnik–Chervonenkis theory, footnote 11 of the book) gives bounds of the wrong order and can be vacuous, because it ignores that only the solution matters. The sharp bound is an exact statement about the law of $V(\theta^*)$, not a union bound, and problems with fewer than $d$ support constraints, or with degenerate configurations of constraints, must be shown to be no worse than fully supported ones; the book treats the general case only in the plane and refers to Campi & Garatti 2008 for general $d$. Handling the null sets and the exchangeability of the samples under the product measure is a substantial part of the work.

Formalization scope

• Decisions live in EuclideanSpace ℝ (Fin d); the cost is inner ℝ c θ. A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ : Fin m => P), and P is a probability measure.
• The violation is the real number (P {δ | θ ∉ Θδ δ}).toReal; probabilities of events over the sample are compared in $[0,\infty]$ through ENNReal.ofReal.
• The solution $\theta^*$ is a function θstar : (Fin N → Δ) → EuclideanSpace ℝ (Fin d) together with the hypothesis that θstar ω solves the program for every sample; it is never an arbitrary map.
• Assumption 3.6 is stated for every $m$ including $m=0$ (a unique minimizer on $\Theta$ itself) and for every sample, as on the page.
• Hypotheses the page leaves implicit are explicit: the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is jointly measurable and θstar is measurable (the book's p. 33 convention); $\varepsilon\in[0,1]$; $d\ge1$.
• A support constraint is one whose removal leaves a feasible point of strictly smaller cost than the solution; the count is a Finset.card over Fin m.
• Theorem 3.8 asserts integrability of $V(\theta^*)$ together with the bound, so it cannot hold through the convention that a non-integrable function integrates to $0$. Theorem 1.3's own sentence omits the assumptions; they are added as in §3.2.1, where it is derived from Theorem 3.7.

A statement in which $\theta^*$ is any feasible point of the program, or merely a measurable function of the sample, is false and does not count as a formalization of Theorem 3.7; nor does one in which Assumption 3.6 is weakened to almost every sample. Contributions of general infrastructure are welcome: exchangeability arguments for product measures, the binomial–beta identity, and Helly-type counting lemmas are reusable well beyond this mission.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 2008. https://doi.org/10.1137/07069821X
• G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102, 2005. https://doi.org/10.1007/s10107-003-0499-y
• G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 2006. https://doi.org/10.1109/TAC.2006.875041
• E. Helly, Über Mengen konvexer Körper mit gemeinschaftlichen Punkten, Jahresbericht der DMV 32, 1923.

Motivation

A discrete function defined only on the integer lattice cannot, by itself, be minimized by the tools of continuous optimization — gradients and convexity in the classical sense simply do not apply. Murota's theory of M-convex functions closes this gap by showing that the exchange axiom alone, a purely combinatorial condition, is enough to guarantee that a discrete function behaves exactly like a convex one: its minimizers form a well-structured (M-convex) set, it can be extended to a genuine convex function on real space without gaining any new local minima, and its behavior under a change of price vector (in the economic interpretation where the function is a cost and its argument a bundle of goods) satisfies the same gross substitutes law economists have studied since Kelso and Crawford's matching-market models. This mission develops the second half of that connection: from local optimality (established in the companion mission) to the full structural picture — minimizer sets, price-substitution laws, and the extension of M-convex functions to genuine convex functions in real variables.

Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) and sibling mission 22-ch06b-mconvexfunctions (Discrete Convex Analysis XXI) cover this chapter's optimality theory (the M-optimality criterion, the exchange axiom as sequential improvement) and its algebraic toolkit (domain operations, worked examples). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results on minimizer structure, gross substitutability, and convex extension that this chapter's remaining sections develop: the M-convexity of minimizer sets, the gross substitutes and stepwise gross substitutes properties and their characterizing role, a minimizer-cut theorem with scaling, integral convexity of M♮-convex functions, and — this mission's goal — the theorem characterizing M-convexity entirely through the polyhedral structure of a function's convex extension.

Setting

Fix a finite ground set $V$. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain, write $f[p](x) = f(x) - \langle p,x \rangle$ for the linear reweighting by $p \in \mathbb R^V$, and $\arg\min g = \{x : g(x) \le g(y)\ \forall y\}$ for the minimizer set of any function $g$. The convex closure $\bar f(x)$ of $f$ at a real point $x$ is the infimum, over finite convex combinations of points of $\operatorname{dom} f$ representing $x$, of the corresponding combination of function values; $f$ is convex extensible if $\bar f$ agrees with $f$ on $\mathbb Z^V$, and integrally convex if $\bar f(x)$ can always be computed using only points from $x$'s own integral neighborhood $N(x)$ (the integer vectors within one unit of $x$ in every coordinate). A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for $x,y \in \operatorname{dom}_{\mathbb R} g$ and $u \in \operatorname{supp}^+(x-y)$, some $v \in \operatorname{supp}^-(x-y)$ and $\alpha_0 > 0$ make the exchange inequality hold for every $\alpha \in [0,\alpha_0]$.

Formalization targets

Goal: convex extensibility characterizes M-convexity

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain,

$$f \text{ is M-convex} \iff \bigl(f \text{ is convex extensible}\bigr) \wedge \bigl(\forall p \in \mathbb R^V,\ \arg\min \bar f[-p] \text{ is an M-convex polyhedron, if nonempty}\bigr),$$

with the M♮-analogue using M♮-convex polyhedra (Theorem 6.43). This is the weakest stable form: it characterizes M-convexity purely by properties of the (unique) convex closure, without reference to any specific algorithm for computing it or any bound on the polyhedron's complexity.

Supporting structural targets

Ten further results build the toolkit this goal draws on and the picture it completes: the M-convexity of minimizer sets (Proposition 6.29), the gross substitutes and stepwise gross substitutes properties and the theorems showing they characterize M-convexity and M♮-convexity among convex-extensible functions (Propositions 6.32-6.33, 6.35, Theorems 6.34, 6.36), a minimizer-cut theorem with scaling used algorithmically in Chapter 10 (Theorem 6.39), integral convexity of M♮-convex functions (Theorem 6.42), a shared-coefficient convex-combination theorem for pairs of M♮-convex functions used in Chapter 8's separation theorem (Theorem 6.44), and the polyhedral-M-convexity of an M-convex function's convex extension together with the correspondence between polyhedral M♮-convexity and the real exchange axiom (Theorems 6.45, 6.47).

Significance

Theorem 6.43 is what makes the whole edifice of M-convex function theory a genuine extension of M-convex set theory (chapters 4-5) rather than a separate parallel development: it says that knowing a function's convex extension is polyhedral, with every price-weighted minimizer set an M-convex polyhedron, is not merely a consequence of M-convexity but an exact characterization of it. This is the theorem that lets later results (the discrete conjugacy theorem of Chapter 8, the separation theorems for M♮-convex functions) move freely between the discrete and continuous pictures. The gross substitutes property (Propositions 6.32-6.36) is independently significant outside this book: it is the exact condition, discovered independently in mathematical economics (Kelso-Crawford, Gul-Stacchetti), under which competitive equilibria with indivisible goods are guaranteed to exist — Murota's theorem that gross substitutability characterizes M-convexity (among convex-extensible functions) is what unifies the economic and combinatorial literatures on this question, taken up again in Chapter 11.

None of these results are open — they are Murota's systematic account of a theory with roots in matroid theory, submodular optimization, and mathematical economics. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiom, ConvexClosureVal, ArgMinOn) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The forward direction of Theorem 6.43 (M-convex $\implies$ convex extensible with polyhedral minimizers) is comparatively direct given Theorem 6.42 and Proposition 6.29. The converse is substantial: it must show that a function whose weighted minimizer sets are all M-convex polyhedra — a purely global, polyhedral condition — satisfies the local exchange axiom (M-EXCloc[Z]), and the book's proof does this by an edge-direction argument on the polyhedron $B = \arg\min f$: every edge of an M-convex polyhedron must be parallel to some $\chi_u - \chi_v$, a fact borrowed from the combinatorial structure of chapter 4's base polyhedra applied to a carefully perturbed weight vector. No shortcut through convex analysis alone succeeds, because ordinary polyhedral theory says nothing about which combinatorial directions a polyhedron's edges must follow — that content comes entirely from the M-convexity of the minimizer sets, not from convexity of the closure by itself.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; functions are (V→ℤ)→WithTop ℝ (integer domain) or (V→ℝ)→WithTop ℝ (real domain, for the polyhedral theorems). The convex closure is built directly from finite convex-combination representations rather than an abstract closure operator, and integral convexity compares it against the same construction restricted to each point's integral neighborhood (Fintype.piFinset of per-coordinate Finset.Icc). Real M-convex/M♮-convex polyhedra are defined as convex hulls of M-convex/M♮-convex integer sets, reusing chapters 4-5's own characterization. The real-variable exchange axioms (Theorems 6.45, 6.47) are formalized from the book's primal (interval-of-$\alpha$) definition, not the directional-derivative reformulation (M-EXC'[R]); Theorem 6.47's own three-way equivalence is correspondingly stated with only its first two legs (see Difficulty and MODERATION_NOTES.md/HARD.md — this is a documented scope choice, not a trivializing omission, since the six results using the primal axiom already exercise the chapter's real- variable machinery in full). No numeric constants are hard-coded anywhere in this mission beyond the book's own literal coefficients in Theorem 6.39's cut bound ((n-1)(α-1)). This mission's definitions are redeclared from chunks 06-mconvex-functions-i and 22-ch06b-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal's converse direction and Theorem 6.44's shared-coefficient construction carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• A. S. Kelso Jr. and V. P. Crawford, "Job matching, coalition formation, and gross substitutes," Econometrica, 50 (1982), pp. 1483-1504.
• F. Gul and E. Stacchetti, "Walrasian equilibrium with gross substitutes," Journal of Economic Theory, 87 (1999), pp. 95-124.

Motivation

The subgradient method for a nonsmooth convex function converges, but slowly: when the level sets of the objective are elongated, the subgradient is nearly orthogonal to the direction towards the minimum, and the method zigzags. For smooth functions the remedy is a change of metric (Newton and quasi-Newton methods); for nonsmooth functions no Hessian exists to supply one. N. Z. Shor's answer was to learn a metric from the subgradients themselves: after each step, stretch the space along the latest (transformed) subgradient, so that components of future subgradients parallel to it are damped. These subgradient methods with space dilation along the gradient (SDG methods) are the ancestors of Shor's r-algorithm and of the ellipsoid method, which the book (p. 49) describes as a special case of the same family and which Khachiyan later used to show that linear programming is solvable in polynomial time.

Section 3.4 of Shor's monograph (Springer 1985, translated by K. C. Kiwiel and A. Ruszczyński, doi:10.1007/978-3-642-82118-9) proves that, under a two-sided condition on the objective, a suitable SDG method decreases function values at the speed of a geometric progression whose ratio is invariant under nonsingular linear changes of variables. This mission formalizes that chain of results.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x,y)$. For a unit vector $\xi$ and a coefficient $\alpha \ge 0$, the operator of space dilation along $\xi$ is

$$R_\alpha(\xi)\,x = x + (\alpha - 1)(x,\xi)\,\xi ,$$

which multiplies the component of $x$ along $\xi$ by $\alpha$ and leaves the orthogonal complement fixed.

Let $f : E_n \to \mathbb{R}$ and let $g : E_n \to E_n$ be a generalized gradient: a subgradient of $f$ when $f$ is convex, an almost-gradient when $f$ is almost differentiable. The SDG method starts from $x_0$ and a nonsingular operator $B_0 = A_0^{-1}$. At step $k = 0, 1, \dots$: if $g(x_k) = 0$ it stops; otherwise it forms the transformed gradient $\tilde g_k = B_k^* g(x_k)$, the direction $\xi_{k+1} = \tilde g_k/\|\tilde g_k\|$, and

$$x_{k+1} = x_k - h_{k+1} B_k \xi_{k+1}, \qquad B_{k+1} = B_k R_{1/\alpha_{k+1}}(\xi_{k+1}), \qquad A_{k+1} = R_{\alpha_{k+1}}(\xi_{k+1}) A_k ,$$

with a stepsize $h_{k+1}$ and a dilation coefficient $\alpha_{k+1}$. So $A_k$ is the accumulated space transformation, $B_k = A_k^{-1}$, and each step is a subgradient step for $\varphi_k(y) = f(B_k y)$ in the variables $y = A_k x$.

The quantitative results assume, for a point $x^*$ and the ball $S_d = \{x : \|x - x^*\| \le d\}$, the two-sided condition

$$N\,[f(x) - f(x^*)] \le (g(x),\, x - x^*) \le M\,[f(x) - f(x^*)], \qquad x \in S_d, \quad M > N > 0. \qquad (3.18)$$

For a convex function the lower inequality holds with $N = 1$; the upper one bounds how far $f$ is from a positively homogeneous function around $x^*$.

Formalization targets

Goal: Theorem 3.4

Under (3.18), with $B_0 = I$, $x_0 \in S_d$, stepsizes $h_{k+1} = \frac{2MN}{M+N}\frac{f(x_k)-f(x^*)}{\|\tilde g_k\|}$, a constant coefficient $1 < \alpha \le \frac{M+N}{M-N}$, and $G$ a bound for $\|g\|$ on $S_d$: there are $c > 0$ and indices $k_1 < k_2 < \cdots$ with

$$f(x_{k_p}) - f(x^*) \le c\,\alpha^{-k_p/n},$$

and for every $k \ge 1$

$$\min_{0 \le i \le k-1}\,[f(x_i) - f(x^*)] \le \frac{G\sqrt{k(\alpha^2-1)}\,d}{N\sqrt{\alpha^{2k/n}-1}} .$$

Milestones

1. Eq. (3.4): $\|R_\alpha(\xi)x\| = \sqrt{\|x\|^2 + (\alpha^2-1)(x,\xi)^2}$.
2. Theorem 3.1: if $\|g(x_k)\| \le d$ and $1+\delta \le \alpha_k \le \alpha^*$, then $\|\tilde g_{k_p}\| < c\,(\prod_{j\le k_p}\alpha_j)^{-1/n}$ along a subsequence.
3. Theorem 3.2: for constant $\alpha > 1$ and $B_0 = I$, $\min_{0\le r\le k-1}\|\tilde g_r\| \le d\sqrt{k(\alpha^2-1)}/\sqrt{\alpha^{2k/n}-1}$.
4. Theorem 3.3: under (3.18) and the rules above, $\|A_k(x_k - x^*)\| \le d$ for all $k$.

Significance

The result shows that one fixed rule, depending only on $M$, $N$ and $n$, yields linear convergence of function values for every objective satisfying (3.18), at a ratio $\alpha^{-1/n}$ that does not deteriorate when the problem is badly scaled: the method, and hence its rate, is invariant under nonsingular linear changes of variables. This is the property the ellipsoid method inherits (Section 3.8 of the book), and the same space-dilation machinery drives the r-algorithm (Section 3.7), still used for large nonsmooth problems such as Lagrangian duals of integer programs.

The theorems are proved in the book; none of them, and no space-dilation method, has a machine-checked proof to our knowledge, and the platform has no statement about variable-metric subgradient methods. The mission provides a reusable formal model of the SDG iteration, the eigenvalue-growth arguments behind Theorems 3.1–3.2, and the one-step invariant of Theorem 3.3. The formalization also corrects two points of the printed text (see Formalization scope).

Difficulty

Theorem 3.3 is a one-step computation, but Theorems 3.1 and 3.2 are not: they relate the size of the transformed gradients to the growth of the singular values of $A_k$, whose determinant is $\prod_j \alpha_j$. A bound on $\|\tilde g_k\|$ at a single step says nothing, since the dilations can concentrate in few directions; the argument has to control the largest singular value of $A_k$ over many steps against the geometric-mean lower bound $(\det A_k)^{1/n}$. The dimension $n$ enters the rate exactly through this comparison. Theorem 3.4 then needs the invariant of Theorem 3.3 to keep every iterate inside $S_d$, where (3.18) and the bound $G$ are available.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$ in the rate statements. Operators are continuous linear maps; $B_0$ is a continuous linear equivalence and $A_0$ its inverse. The state $(x_k, B_k, A_k)$ is produced by a defined recursion sdg, not assumed; $\tilde g_k$ is gTilde.
• The stepsize rule receives the index, the current point and $\tilde g_k$; the dilation coefficient at step $k$ is α (k+1). When $g(x_k) = 0$ the state is repeated, which encodes the book's stop; no division by zero is used.
• The book states Theorems 3.1–3.4 for almost differentiable $f$ with $g$ an almost-gradient; the proofs use only the bounds on $\|g\|$ and (3.18), so the Lean statements quantify over every map $g$ with those properties. $G$ is any bound for $\|g\|$ on $S_d$ in place of the maximum.
• Theorems 3.2–3.4 take $B_0 = I$, as their proofs do; Theorem 3.1 allows any nonsingular $B_0$.
• Two corrections to the printed statements, both following the proofs: Theorem 3.4's record bound carries the factor $1/N$ that the proof derives, and the record minima in Theorems 3.2 and 3.4 range over the indices $0, \dots, k-1$ that the proof controls, rather than $1, \dots, k$.
• Constants $c$ and subsequences are existential and chosen after the data of the run, before the index $p$. A statement placing $c$ after $p$, or dropping (3.18) on $S_d$, would be trivially true or false and is ruled out.

Useful infrastructure, reusable for the r-algorithm and ellipsoid chapters: identities for $R_\alpha(\xi)$, determinants and singular values of products of rank-one dilations, and the invariance of the SDG iteration under a linear change of variables. Proofs of any milestone, and alternative arguments for Theorem 3.1, are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §§3.2–3.4, pp. 49–62 (translated by K. C. Kiwiel and A. Ruszczyński). https://doi.org/10.1007/978-3-642-82118-9

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access only to function values: the objective is the output of a simulator or a black-box program, and its gradient is unavailable or too expensive. Derivative-free (or zeroth-order) methods address this setting. Nesterov and Spokoiny (Found. Comput. Math. 17 (2017)) showed that a very simple oracle, the finite difference of $f$ along a random Gaussian direction, can replace the gradient in standard first-order schemes at the price of a factor depending only on the dimension. Their analysis became the reference point for later work on zeroth-order stochastic optimization and on gradient-free methods in reinforcement learning and adversarial attacks.

This mission covers Section 6 of the paper: the accelerated random method $\mathcal{FG}_\mu$ and its rate, Theorem 9. It is the third mission of a series; the first covers random search for nonsmooth problems (Theorem 6), the second the random gradient method for smooth problems (Theorem 8).

Setting

Let $E$ be a real inner product space of dimension $n \ge 2$ with norm $\|\cdot\|$ (the paper's space with operator $B$ is $E$ with the inner product $\langle Bx, y\rangle$). Let $u$ be a standard Gaussian vector in $E$, and write $\mathbb E_u$ for expectation over $u$.

The objective $f : E \to \mathbb R$ is differentiable with Lipschitz gradient, $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x - y\|$ with $L_1 > 0$, and strongly convex with parameter $\tau \ge 0$:

$$f(y) \ge f(x) + \langle\nabla f(x), y - x\rangle + \tfrac{\tau}{2}\|y - x\|^2 .$$

The value $\tau = 0$ is allowed (plain convexity). The condition number is $\kappa = \tau/L_1$. The problem $f^* = \min_{x \in E} f(x)$ is assumed solvable, with minimizer $x^*$.

For $\mu \ge 0$ the Gaussian approximation is $f_\mu(x) = \mathbb E_u f(x + \mu u)$, and the random gradient-free oracle is

$$B^{-1}g_\mu(x) = \frac{f(x + \mu u) - f(x)}{\mu}\,u \quad (\mu > 0), \qquad B^{-1}g_0(x) = \langle\nabla f(x), u\rangle\,u .$$

The paper (p. 548) sets $\theta_n = 1/(16(n+1)^2L_1(f))$ and $h_n = 1/(4(n+4)L_1(f))$. This mission uses $\theta_n = 1/(16(n+4)^2L_1)$; the reason is given under Formalization scope. Method $\mathcal{FG}_\mu$ (Eq. (60)) chooses $x_0 \in E$, $v_0 = x_0$ and $\gamma_0 > 0$ with $\gamma_0 \ge \tau$, and at every iteration $k \ge 0$:

1. computes $\alpha_k > 0$ with $\theta_n^{-1}\alpha_k^2 = (1 - \alpha_k)\gamma_k + \alpha_k\tau \equiv \gamma_{k+1}$;
2. sets $\lambda_k = \alpha_k\tau/\gamma_{k+1}$, $\beta_k = \alpha_k\gamma_k/(\gamma_k + \alpha_k\tau)$ and $y_k = (1-\beta_k)x_k + \beta_k v_k$;
3. draws a fresh Gaussian direction $u_k$, independent of the past, and computes $g_\mu(y_k)$;
4. sets $x_{k+1} = y_k - h_n B^{-1}g_\mu(y_k)$ and $v_{k+1} = (1-\lambda_k)v_k + \lambda_k y_k - (\theta_n/\alpha_k)B^{-1}g_\mu(y_k)$.

Write $\phi_k = \mathbb E f(x_k)$ (expectation over $u_0, \dots, u_{k-1}$), $\psi_k = \prod_{i=0}^{k-1}(1-\alpha_i)$ and $C_k = 1 + \sum_{i=1}^{k-1}\prod_{j=k-i}^{k-1}(1-\alpha_j)$ for $k \ge 1$, with $\psi_0 = 1$ and $C_0 = 0$ (p. 550).

Formalization targets

Goal: Theorem 9 (p. 549)

For all $k \ge 0$,

$$\phi_k - f^* \le \psi_k\Big[f(x_0) - f(x^*) + \frac{\gamma_0}{2}\|x_0 - x^*\|^2\Big] + \mu^2 L_1\Big(n + \frac{3(n+8)}{16}C_k\Big), \tag{62}$$

where

$$\psi_k \le \min\Big\{\Big(1 - \frac{\kappa^{1/2}}{4(n+4)}\Big)^k,\ \Big(1 + \frac{k}{8(n+4)}\sqrt{\frac{\gamma_0}{L_1}}\Big)^{-2}\Big\}, \qquad C_k \le \min\Big\{k,\ \frac{4(n+4)}{\kappa^{1/2}}\Big\}.$$

The two regimes are a rate $O(n^2/k^2)$ for convex $f$ and a linear rate with ratio $1 - \kappa^{1/2}/(4(n+4))$ for strongly convex $f$, both up to a bias proportional to $\mu^2$.

Milestones

In attack order: Lemma 1 (Gaussian moments, (16)–(17)); Theorem 3.1 (the bound (32) on the second moment of $g_0$); Theorem 1's (19), $|f_\mu - f| \le \frac{\mu^2}{2}L_1 n$; Eq. (12), $L_1(f_\mu) \le L_1(f)$; Lemma 5, the bound (37) on $\mathbb E_u\|g_\mu(x)\|_*^2$ in terms of $\nabla f_\mu(x)$; Eq. (21), $\nabla f_\mu = \mathbb E_u g_\mu$; and Eq. (11), $f_\mu \ge f$ for convex $f$.

Significance

Theorem 9 shows that the $n$-fold slowdown of gradient-free methods relative to their gradient counterparts survives acceleration: $\mathcal{FG}_\mu$ reaches accuracy $\epsilon$ in $O(n L_1^{1/2}R/\epsilon^{1/2})$ iterations for convex $f$, against $O(nL_1R^2/\epsilon)$ for the non-accelerated random gradient method. The analysis also quantifies how small the finite-difference step $\mu$ must be for this to hold. The result is used as the baseline accelerated zeroth-order rate in later work.

The theorem is proved in the paper. As far as is known it has not been machine-checked, and Mathlib has no Gaussian smoothing, no random gradient-free oracle and no analysis of an accelerated method driven by random directions. A formal proof also settles the constant question raised by the printed $\theta_n$ (see below).

Difficulty

The deterministic fast gradient method is analysed by an estimate-sequence argument in which the gradient step is exact. Here the step uses $g_\mu(y_k)$, which is an unbiased estimate of $\nabla f_\mu(y_k)$ and not of $\nabla f(y_k)$, and whose second moment is of order $n\|\nabla f_\mu\|^2$ plus a bias term. The step size and the coupling parameter $\theta_n$ must absorb this second moment, and the argument must be run for $f_\mu$ rather than $f$. The estimate sequence then has to be passed through expectations over the history $u_0, \dots, u_{k-1}$, which requires the independence of $u_k$ from $x_k, v_k, y_k$ and integrability of every quantity involved. Transporting the result from $f_\mu$ back to $f$ uses (11) and (19), and requires that $f_\mu$ inherits strong convexity with the same parameter $\tau$, a fact the paper uses without stating it.

Formalization scope

$E$ is an arbitrary finite-dimensional real inner product space (InnerProductSpace ℝ E, FiniteDimensional ℝ E, Borel measurable), $n$ is Module.finrank ℝ E, and the Gaussian is Mathlib's stdGaussian E. The operator $B$ is absorbed into the inner product, so $\nabla f$ is gradient f and $B^{-1}g_\mu$ is $\frac{f(x+\mu u)-f(x)}{\mu}u$. This is not a restriction to $B = I$ on $\mathbb R^n$. All expectations are Bochner integrals; under the hypotheses every integrand is integrable, so no integrability hypothesis is added.

The run is a structure over a probability space $(\Omega, \mathbb P)$: directions $u_k$ that are measurable, mutually independent (iIndepFun) and standard Gaussian; deterministic sequences $\gamma, \alpha$ satisfying step a) as equations; and random points $x_k, v_k$ satisfying steps b)–d) for every outcome. The smoothing parameter satisfies $\mu \ge 0$, and at $\mu = 0$ the oracle is $g_0$. The goal pins $\theta = 1/(16(n+4)^2L_1)$ and $h = 1/(4(n+4)L_1)$. $\psi_k$ and $C_k$ are definitions computed from $\alpha$.

The constant $\theta_n$. The paper prints $\theta_n = \frac{1}{16(n+1)^2L_1(f)}$. The proof (pp. 549–550) needs $\frac{h_n}{4(n+4)} - \frac{h_n^2L_1}{2} = \frac{1}{32(n+4)^2L_1} = \frac{\theta_n}{2}$, $\alpha_k \ge [\tau\theta_n]^{1/2} = \frac{\kappa^{1/2}}{4(n+4)}$ and $\theta_n^{1/2} = \frac{1}{4(n+4)L_1^{1/2}}$, which hold only with $(n+4)$. With the printed value $\theta_n$ is larger than the first inequality allows, and the argument does not go through. The mission therefore states Theorem 9 with $\theta_n = \frac{1}{16(n+4)^2L_1}$; all other constants are as printed.

Two trivializing formalizations are ruled out. First, the bound $C_k \le 4(n+4)/\kappa^{1/2}$ carries the hypothesis $\tau > 0$: at $\tau = 0$ the paper's value is $+\infty$, while Lean's division by zero would turn it into $C_k \le 0$, which is false. $\psi_k$ and $C_k$ are definitions from the run, not free variables that only satisfy the bounds. Second, the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the exact gradient (which would give Nesterov's deterministic method) and not an arbitrary direction sequence.

A complete development needs Gaussian integration by parts in an inner product space, moment bounds for $\|u\|$, differentiation under the integral sign for $f_\mu$, and conditional expectation along an i.i.d. sequence. The smoothing layer (Lemma 1, (11), (12), (19), (21), (32), (37)) is reusable for any zeroth-order method, and contributions of these components as separate lemmas are welcome.

Selected references

• Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (Lemma 2.2.4 and Section 2.2.1, the estimate-sequence analysis the proof of Theorem 9 follows). https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Missions 29-ch08b-conjugacyduality and 30-ch08c-conjugacyduality built the M2-/L2-convex function classes and proved their conjugacy correspondence is nearly complete. This mission finishes that correspondence (Theorems 8.48-8.49) and then turns to chapter 8's capstone application: a Lagrangian duality theory for integer programs, built entirely from the M-/L-convexity machinery developed across the whole book. It develops the general perturbation-based duality framework (mirroring Rockafellar's conjugate duality for nonlinear programming), specializes it to M-convex programs via the perturbation $F_r$, and proves the strong duality theorem this specialization exists to deliver — together with its mirror construction recovering the primal problem from the dual.

Setting

An M-convex program consists of a set $B\subseteq\mathbb Z^V$ satisfying (REG) — $B$ is an M-convex set — and an objective $c:\mathbb Z^V\to\mathbb Z\cup\{+\infty\}$ satisfying (OBJ) — $c$ is an M-convex function. The general duality framework embeds any $f(x)=c(x)+\delta_B(x)$ in a family of perturbed problems via $F:\mathbb Z^V\times\mathbb Z^V\to\mathbb Z\cup\{+\infty\}$ with $F(x,0)=f(x)$, yielding an optimal-value function $\varphi$, a Lagrangian $K$, and a dual objective $g$. For M-convex programs the perturbation $F_r(x,u)=c(x)+\delta_B(x+u)+r(u)$, for an M-convex regularizer $r$ with $r(0)=0$, makes this framework concrete; the case $r\equiv 0$ is written with subscript $0$.

Formalization targets

Goal: Strong duality for M-convex programs (Theorem 8.59)

For a feasible, bounded-below M-convex program, $\min(P)=\varphi_r(0)=\varphi_r^{\bullet\bullet}(0) =\max(D_r)$, and $\operatorname{opt}(D_r)=-\partial_{\mathbb Z}\varphi_r(0)$. This is the theorem mission 11-conjugacy-ii-lagrange's own STATUS.md explicitly deferred, noting it needs the specific M-convex perturbation $F_r$ (Eq. (8.61)) and Propositions 8.55-8.56/Theorems 8.57-8.58 as prerequisites — all built as milestones of this mission.

Supporting structural targets

Theorem 8.48 completes the M2-/L2-convex conjugacy correspondence; Theorem 8.49 characterizes separable convex functions as exactly the M$^\natural_2$-and-L$^\natural_2$-convex functions. Theorem 8.53 (reduced to parts (1),(2),(4)) gives the general perturbation-independent duality identities: the dual objective is $g=-\varphi^{\bullet}(-\cdot)$, weak duality's biconjugate form $\sup(D)=\varphi^{\bullet\bullet}(0)$, and the equivalence of strong duality with biconjugate exactness. Proposition 8.55 shows the M-convex perturbation $F_r$ legitimately instantiates the general framework; Proposition 8.56 (reduced to part (1)) gives the closed form for the unregularized Lagrangian kernel $K_0$ via the conjugate of $B$'s indicator function; Theorems 8.57 and 8.58 establish the resulting convexity/concavity of the kernel, the dual objective, and the optimal-value function in each of their arguments. Propositions 8.62-8.63 and Theorems 8.64-8.65 build and analyze the mirror construction — the dual perturbation $G_r$, its optimal-value function $\gamma_r$, and the dual-of-dual reconstruction — showing that for bounded $B$ the process exactly recovers the primal problem and its own strong duality theorem.

Significance

This is chapter 8's payoff: a full nonlinear-integer-programming duality theory, built without any convexity assumption beyond M-/L-convexity, mirroring Rockafellar's classical conjugate duality approach line for line while replacing every continuous convexity argument with a discrete M-/L-convexity one. Theorem 8.59's proof is a two-line consequence of the machinery this mission assembles (Theorems 8.35, 8.53, 8.58), which is itself the point: the discrete theory's hard combinatorial work (Theorems 8.35, 8.36, 8.42 from prior missions) is what makes the strong duality theorem here nearly free, exactly as convex analysis makes classical Lagrangian duality nearly free once Fenchel duality is established. The bidirectional construction of Theorems 8.62-8.65 is the discrete analogue of the classical fact that Lagrangian duality is symmetric between primal and dual convex programs.

None of these results are open — they are Murota's own account of M2-/L2-conjugacy and Lagrangian duality (section 8.3.3 and section 8.4), continuing chapter 8's duality program to its conclusion. What this mission contributes is a faithful, machine-checked formal statement of each, completing the platform's coverage of chapter 8's duality theorems begun in missions 10-conjugacy-i and 11-conjugacy-ii-lagrange; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The EReal-valued ($\mathbb Z\cup\{\pm\infty\}$) typing is essential and new to this mission: unlike every prior mission in this series, the general framework's derived quantities ($\varphi$, $K$, $g$, and their mirror-construction analogues $G_r$, $\gamma_r$, $\tilde K_r$, $\tilde f$) are defined as infima/suprema over families that are not a priori bounded, so they can genuinely equal $-\infty$ or $+\infty$ — a value WithTop ℝ cannot represent and whose sInf instance would silently substitute a junk value (0) rather than correctly returning $-\infty$. The book's own repeated "$X$ is convex (resp. concave), or $X\equiv+\infty$, or $X\equiv-\infty$" disjunctive escape clauses (Theorems 8.57, 8.58, Propositions 8.63) are captured with two small generic combinators, IsEmbedOf/IsNegOf, rather than restating the embedding by hand at each of the roughly dozen occurrences.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; the base M-/L-/M2-/L2-convexity vocabulary is redeclared verbatim from missions 29-ch08b-conjugacyduality and 30-ch08c-conjugacyduality, since sibling drafts in this series cannot yet reference one another. Two results carry a documented partial-coverage scope reduction (see HARD.md): Theorem 8.53 is placed with only parts (1),(2),(4), the purely algebraic identities holding unconditionally for any perturbation $F$, omitting parts (3),(5),(6), which characterize $\operatorname{opt}(D)$ under the book's own biconjugacy hypothesis (8.55) — a hypothesis this mission's M-convex-specific Theorem 8.59 later establishes directly rather than invoking Theorem 8.53's general form; and Proposition 8.56 is placed with only part (1), the $K_0$ closed form, omitting part (2), the $K_r$ closed form via the infimal convolution $\delta_{-B}\square r[y]$, not independently needed elsewhere in this chunk. One numbered result nominally in this chunk's page range, Theorem 8.46, is not re-placed here: it was already found and placed as a milestone in mission 30-ch08c-conjugacyduality, whose own page range overlaps this chunk's by one page (PDF251/printed 233) — see HARD.md. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 8.57 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• R. T. Rockafellar, "Conjugate duality and optimization," CBMS-NSF Regional Conference Series in Applied Mathematics, SIAM, 1974 [177] (the classical conjugate-duality framework this mission's section 8.4 adapts to the discrete M-/L-convex setting).
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (the original source of M2-/L2-convexity, Theorems 8.35, 8.36, 8.45, 8.46, 8.48, and the Lagrange duality theory of section 8.4).

Motivation

Portfolio selection and other decisions under risk are routinely solved as mean–risk models: maximize the expected outcome minus a multiple of a risk measure over the feasible set. Such a model is computationally convenient, but it is only defensible if its answers agree with the preferences of risk-averse decision makers. The standard formal expression of those preferences is second-degree stochastic dominance (SSD): a random outcome $X$ dominates $Y$ when every nondecreasing concave utility prefers $X$. A mean–risk model whose optimal solution may be SSD-dominated by another feasible decision recommends something every risk-averse investor would reject; the classical mean–variance model has exactly this defect.

Ogryczak and Ruszczyński (SIAM J. Optim. 13 (2002) 60–78) characterize SSD through the absolute Lorenz curve (the second quantile function) and use this dual view to study risk measures defined from quantiles: the vertical diameter of the dual dispersion space, the tail Gini measure and the Gini mean difference. Their §5 shows that the mean–Gini model, with trade-off coefficient at most one, has optimal solutions and that all of them are SSD-efficient. This mission formalizes that result together with the lemmas it rests on. A companion mission of this series formalizes the dual characterization of SSD itself (the paper's Theorems 3.1–3.2).

Timeline. Yitzhaki (1982) showed the mean–Gini necessary condition for SSD for bounded distributions; Ogryczak and Ruszczyński proved SSD consistency of mean-semideviation models (Eur. J. Oper. Res. 116 (1999)) and, in the present paper, extended the analysis to quantile-based and Gini-type risk measures for general integrable outcomes, with existence and efficiency of optimal solutions over sets in $L_q$.

Setting

Let $(\Omega,\mathcal B,P)$ be a probability space and $X:\Omega\to\mathbb R$ an integrable random variable with mean $\mu_X=E X$ and distribution function $F_X(\eta)=P\{X\le\eta\}$. The second performance function is

$$F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}F_X(\xi)\,d\xi ,$$

and $X\succeq_{SSD}Y$ means $F_X^{(2)}(\eta)\le F_Y^{(2)}(\eta)$ for all $\eta\in\mathbb R$. Strict dominance is $X\succ_{SSD}Y$ iff $X\succeq_{SSD}Y$ and not $Y\succeq_{SSD}X$. For a set $Q$ of random variables, $X\in Q$ is SSD-efficient in $Q$ if no $Y\in Q$ satisfies $Y\succ_{SSD}X$.

The left quantile function is $F_X^{(-1)}(p)=\inf\{\eta:F_X(\eta)\ge p\}$ for $0<p\le1$; a number $q$ is a $p$-quantile if $P\{X<q\}\le p\le P\{X\le q\}$. The absolute Lorenz curve is $F_X^{(-2)}(p)=\int_0^pF_X^{(-1)}(\alpha)\,d\alpha$ on $[0,1]$. From it the paper defines

• the vertical diameter $h_X(p)=\mu_Xp-F_X^{(-2)}(p)$, $p\in[0,1]$ (eq. (3.6));
• the Gini mean difference $\Gamma_X=2\int_0^1(\mu_Xp-F_X^{(-2)}(p))\,dp$ (eq. (3.8));
• the tail Gini measure $G_X(p)=\frac{2}{p^2}\int_0^p(\mu_X\alpha-F_X^{(-2)}(\alpha))\,d\alpha$, $p\in(0,1]$ (eq. (4.8)), so that $\Gamma_X=G_X(1)$.

The optimization problem is

$$\max_{X\in Q}\ (\mu_X-\lambda r_X),\tag{5.1}$$

with $\lambda>0$, $r_X$ one of these dual risk measures, and $Q$ a convex, closed, bounded subset of $L_q(\Omega,P)$ for some $q>1$.

Formalization targets

Goal: Theorem 5.3

For $1<q<\infty$, a nonempty convex bounded closed $Q\subseteq L_q$, $r_X=\Gamma_X$ and every $\lambda\in(0,1]$:

$$\operatorname*{arg\,max}_{X\in Q}(\mu_X-\lambda\Gamma_X)\neq\emptyset\quad\text{and every } X\in\operatorname*{arg\,max}_{X\in Q}(\mu_X-\lambda\Gamma_X)\text{ is SSD-efficient in }Q.$$

Milestones

1. Lemma 3.4: for $p\in(0,1)$, $h_X(p)=\min_{\xi\in\mathbb R}E\{\max(p(X-\xi),(1-p)(\xi-X))\}$, attained at any $p$-quantile.
2. Lemma 5.1: $X\mapsto h_X(p)$ is convex and positively homogeneous on $L_1$ for $p\in[0,1]$.
3. Lemma 5.2: $X\mapsto G_X(p)$ is convex and positively homogeneous on $L_1$ for $p\in(0,1]$.
4. (4.1): $X\succeq_{SSD}Y\Rightarrow\mu_X\ge\mu_Y$.
5. Proposition 4.5: $X\succeq_{SSD}Y\Rightarrow\mu_X-\Gamma_X\ge\mu_Y-\Gamma_Y$ and $X\succ_{SSD}Y\Rightarrow\mu_X-\Gamma_X>\mu_Y-\Gamma_Y$.

Companion: Theorem 5.4

For $r_X=h_X(p)/p$ with $p\in(0,1)$ and $\lambda\in(0,1]$, the optimal set $Q^*$ is nonempty and each $X\in Q^*$ has an SSD-efficient $X^*\in Q^*$ with $\mu_{X^*}=\mu_X$ and $h_{X^*}(p)=h_X(p)$.

Significance

Theorem 5.3 certifies the mean–Gini model as a safe decision rule: whatever trade-off $\lambda\in(0,1]$ is chosen, the model returns a decision that no feasible alternative dominates for all risk-averse utilities, and such a decision exists under assumptions natural for portfolio sets in $L_q$. Theorem 5.4 gives the weaker but still usable guarantee for the tail-value-at-risk type measure $h_X(p)/p$, for which non-efficient optima can occur. Lemma 3.4 is the bridge to computation: it turns $h_X(p)$ into an expected piecewise-linear loss minimized over a scalar, which is how these models become linear programs over scenarios (§6 of the paper).

On the formalization side, the results are proved in the paper but, as far as a search of the platform shows, not machine-checked anywhere. A complete development produces reusable infrastructure: quantile functions and their integrals for integrable random variables, convexity of law-invariant functionals on $L_1$, the Gini mean difference, and an existence argument for concave maximization over weakly compact subsets of $L_q$.

Difficulty

The existence half needs weak compactness of $Q$ in the reflexive space $L_q$ and weak upper semicontinuity of $\mu_X-\lambda\Gamma_X$. The functional is defined through quantiles, which are not linear in $X$, so neither its concavity nor its continuity is visible from the definition. Closedness of $Q$ in the norm topology must be upgraded to weak closedness, which uses convexity. The efficiency half needs the strict inequality (4.7): a strict SSD relation must produce a strict gap in the integrated absolute Lorenz curves, and the pointwise inequality of $F^{(2)}$ alone does not give strictness in $\Gamma$. The obvious attempt to argue efficiency from (4.6) alone fails: it yields only a weak inequality, which is compatible with an optimum being strictly dominated.

Formalization scope

• One probability space $(\Omega,P)$ with IsProbabilityMeasure P; random variables are functions Ω → ℝ, and all random variables compared by $\succeq_{SSD}$ live on it.
• $F_X^{(2)}$ is the Bochner integral of P.real {X ≤ ξ} over $(-\infty,\eta]$; $\mu_X$ is ∫ X ∂P. Every statement about general random variables assumes Integrable X P (the paper's standing $E|X|<\infty$).
• $F_X^{(-1)}$ uses the real sInf; its junk value at $p=1$ does not enter any integral and is never used pointwise. $F_X^{(-2)}$ is used only on $[0,1]$, so it is real-valued here; the extended-real version with $+\infty$ off $[0,1]$ belongs to the companion mission.
• $\Gamma_X$ is defined by the area formula (3.8), not by the double-integral formula that the paper cites; $h_X$ is defined by (3.6), not by the minimum (3.7), so Lemma 3.4 is a genuine statement.
• $L_q$ is Mathlib's Lp ℝ q P with 1 < q and q ≠ ∞ (the paper's $q$ is a real number $>1$); the functionals are applied to the function of an $L_q$ element, and SSD-efficiency in $Q$ refers to the image of $Q$ in functions. Positive homogeneity is stated for the $L_1$ element $c\cdot X$.
• Added hypothesis: $Q$ is nonempty. The paper does not write it, and without it the optimal set is empty.
• Optimal solutions are maximizers in $Q$, not a supremum value. The trade-off coefficient is lam because λ is a Lean keyword; the range $\lambda\in(0,1]$ is kept exactly.
• A trivializing formalization is ruled out: the weak relation $\succeq_{SSD}$ must not replace the strict relation in SSD-efficiency (every $X$ weakly dominates itself), and $\Gamma$ must not be a hand-chosen closed form.

Needed infrastructure: quantile functions and the identity $\int_0^1F_X^{(-1)}=\mu_X$; the minimum representation of Lemma 3.4; convexity of law-invariant functionals on Lp; weak compactness of bounded closed convex sets in reflexive Lp. Contributions of general lemmas about quantiles and Lorenz curves are welcome and reusable beyond this mission.

Selected references

• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13(1) (2002) 60–78. https://doi.org/10.1137/S1052623400375075
• W. Ogryczak, A. Ruszczyński, From stochastic dominance to mean-risk models: semideviations as risk measures, Eur. J. Oper. Res. 116 (1999) 33–50. https://doi.org/10.1016/S0377-2217(98)00167-2
• S. Yitzhaki, Stochastic dominance, mean variance, and Gini's mean difference, Amer. Econ. Rev. 72 (1982) 178–185. https://www.jstor.org/stable/1808584