Optimization

Motivation

Most stochastic programs cannot be solved as stated, because the objective is an expectation over a distribution that is high-dimensional, continuous or known only through a simulator. The standard remedy is the sample average approximation (SAA), also called the Monte Carlo or sample-path method: draw an i.i.d. sample, replace the expectation by the sample mean, and solve the resulting deterministic problem. The method is the workhorse of two-stage stochastic programming, and its statistical behaviour decides how large a sample a practitioner must draw.

For smooth problems with a unique optimum, the classical theory says the SAA solution converges at rate $N^{-1/2}$ and is asymptotically normal. Shapiro and Homem-de-Mello (SIAM J. Optim. 11 (2000)) observed that two-stage linear programs with finitely many scenarios behave quite differently: their optimal solutions are typically sharp, the objective grows linearly away from the minimizer, and then the SAA problem does not just approach the true solution but returns it exactly once the sample is large enough. This mission formalizes that first observation, Theorem 2.1 of the paper. Its sequels in the same series show that the probability of failure decays exponentially in $N$ (mission 2) and extend the picture to multiple optimal solutions in the finite polyhedral case (mission 3).

Setting

Let $P$ be a probability measure on a sample space $(\Omega,\mathcal F)$, let $\Theta\subseteq\mathbb R^m$ be a set of feasible decisions, and let $h:\mathbb R^m\times\Omega\to\mathbb R$ be a cost function. The true problem (1.1) is

$$\min_{x\in\Theta}\ \bigl\{ f(x) := \mathbb E_P\, h(x,\omega) \bigr\}.$$

Let $\omega^1,\omega^2,\dots$ be an i.i.d. sequence of random elements of $\Omega$ with law $P$, defined on some probability space $(S,Q)$. The approximating problem (1.2) uses the first $N$ of them:

$$\min_{x\in\Theta}\ \Bigl\{ \hat f_N(x) := N^{-1}\sum_{j=1}^N h(x,\omega^j) \Bigr\}.$$

For a function $g$ on $\mathbb R^m$ write $\operatorname{argmin}_\Theta g = \{x\in\Theta : g(x)\le g(y)\ \forall y\in\Theta\}$; the optimal set of the true problem is $A=\operatorname{argmin}_\Theta f$. The directional derivative of $g$ at $x$ in direction $d$ is $g'(x,d)=\lim_{t\downarrow0}(g(x+td)-g(x))/t$; for the cost of a single scenario it is written $h'_\omega(x,d)$. The tangent cone $T_\Theta(\bar x)$ to a convex set $\Theta$ at $\bar x\in\Theta$ is the closure of $\{t(x-\bar x): t\ge0,\ x\in\Theta\}$.

Assumption (A). The true problem has a unique optimal solution $\bar x$, i.e. $A=\{\bar x\}$, and there is $c>0$ with

$$f(x)\ \ge\ f(\bar x) + c\,\|x-\bar x\| \qquad \forall\,x\in\Theta. \tag{2.2}$$

An optimal solution with this linear growth is a sharp minimum.

A statement holds w.p.1 for $N$ large enough if for $Q$-almost every sample path there is $N^*$, depending on the path, such that it holds for every $N\ge N^*$.

Formalization targets

Goal: Theorem 2.1 (p. 5)

Suppose (i) $h(\cdot,\omega)$ is convex for every $\omega$; (ii) $f$ is well defined and finite valued; (iii) $\Theta$ is closed and convex; (iv) Assumption (A) holds. Then w.p.1 for $N$ large enough

$$\operatorname*{argmin}_{x\in\Theta}\ \hat f_N(x) = \{\bar x\},$$

that is, the approximating problem has a unique optimal solution $\hat x_N$ and $\hat x_N=\bar x$.

Milestones

1. (A) ⇔ (2.3) (p. 4): for a convex problem, $\bar x$ is a sharp unique minimum iff $f'(\bar x,d)>0$ for all $d\in T_\Theta(\bar x)\setminus\{0\}$.
2. Uniform positivity (p. 4): (2.3) implies $f'(\bar x,d)\ge\varepsilon\|d\|$ for some $\varepsilon>0$ and all $d\in T_\Theta(\bar x)$.
3. Proposition 2.2 (2.5) (p. 5): $f'(x,d)=\mathbb E_P\{h'_\omega(x,d)\}$.
4. (2.10) (p. 5): $\hat f'_N(x,d)=N^{-1}\sum_{j=1}^N h'_{\omega^j}(x,d)$.
5. Proposition 2.2 (2.6) (p. 5): $\lim_N \sup_{\|d\|\le1}|f'(x,d)-\hat f'_N(x,d)|=0$ w.p.1.
6. Proposition 2.2 (2.7) (p. 5): $\lim_N\mathcal H(\partial\hat f_N(x),\partial f(x))=0$ w.p.1, with $\mathcal H$ the Hausdorff distance.
7. (2.11) (p. 6): w.p.1 for $N$ large enough, $\hat f'_N(\bar x,d)>0$ for all $d\in T_\Theta(\bar x)\cap S^{m-1}$.

Significance

The result. Theorem 2.1 says that for convex stochastic programs with a sharp optimum, SAA is not an estimator with sampling error in the usual sense: almost every sample path eventually produces the true solution itself. This is the qualitative statement behind the paper's main quantitative result (Theorem 3.1, mission 2 of this series), that the probability of not obtaining the exact solution decays like $e^{-\beta N}$. Together they explain why, in two-stage linear programs with finitely many scenarios, modest sample sizes often recover the optimal first-stage decision exactly, a phenomenon the paper documents numerically. The proposition on directional derivatives (Proposition 2.2) is of independent use: it is the almost-sure uniform convergence of first-order information of a sample average, which recurs in the asymptotic analysis of SAA estimators.

Formalizing it. The theorem is proved in the paper; nothing here is open. Machine-checked SAA theory is thin: the existing platform material treats uniform convergence of the objective on compact sets, not directional derivatives or exactness at sharp minima. A complete development supplies, on top of Mathlib, the strong law of large numbers applied to directional derivatives of convex integrands, the passage from pointwise to uniform convergence for convex functions, and the characterization of sharp minima by directional derivatives on the tangent cone. Each of these is reusable well beyond this paper.

Difficulty

The obvious argument fails at the step from convergence to exactness. Strong consistency of SAA ($\hat x_N\to\bar x$ w.p.1) says nothing about $\hat x_N$ equalling $\bar x$; for a smooth objective it never does. Exactness has to come from a first-order condition at $\bar x$ that holds with a margin, and that margin must be transferred to $\hat f_N$ uniformly over all tangent directions at once, not one direction at a time, since there are uncountably many directions and each carries its own null set. The second difficulty is that $\hat f_N$ and $f$ are typically nonsmooth (piecewise linear in the motivating examples), so the first-order objects are one-sided directional derivatives, and differentiation under the integral sign, in its usual smooth form, does not apply to them.

Formalization scope

• $\mathbb R^m$ is EuclideanSpace ℝ (Fin m). The sample is one infinite i.i.d. sequence on a separate probability space $(S,Q)$: each $\omega^j$ is measurable with law $P$, and the family is mutually independent. $\hat f_N$ uses the first $N$ terms (0-based in Lean). "W.p.1 for $N$ large enough" is ∀ᵐ s ∂Q, ∀ᶠ N in atTop, …; a fresh sample for each $N$ is not used.
• Hypothesis (ii), "$f$ well defined and finite valued", is encoded as integrability of $h(x,\cdot)$ for every $x$ (a disclosed pin, which includes measurability).
• $f$ is the Bochner integral; directional derivatives are one-sided limits (limUnder along $t\downarrow0$), used only for convex finite functions, where the limits exist. Optimal sets are defined directly as argmin sets, without infima.
• The tangent cone is Mathlib's posTangentConeAt, the cone of limits of $c_n d_n$ with $c_n\ge0$; for convex $\Theta$ it is the closure of $\mathbb R_+(\Theta-\bar x)$. Mathlib's tangentConeAt ℝ, which allows negative scalings and is symmetric, is not the paper's cone and is not used.
• Supremum limits over the unit ball are stated as uniform convergence on the closed unit ball; the Hausdorff distance is the extended-valued Metric.hausdorffEDist. Subdifferentials use the published definition ShorNonsmooth.Subdiff.subdifferential.
• Uniqueness in the goal is the set equality $\operatorname{argmin}_\Theta\hat f_N=\{\bar x\}$; the weaker "$\bar x$ is optimal for (1.2)" is not the theorem. The goal's quantifier order is "almost surely, eventually in $N$"; "for each $N$, almost surely" is a different and false statement.
• Milestones 1 and 2 are stated for an arbitrary finite convex function, which covers both $f$ and $\hat f_N$.

Contributions welcome: proofs of any milestone; in particular the convex-analysis lemmas (milestones 1, 2 and 4) need no probability, and (2.5)–(2.6) need only Mathlib's strong law.

Selected references

• A. Shapiro and T. Homem-de-Mello, On the rate of convergence of optimal solutions of Monte Carlo approximations of stochastic programs, SIAM J. Optim. 11(1):70–86, 2000. https://doi.org/10.1137/S1052623498349541 (the mission cites the authors' preprint, Stochastic Programming E-Print Series).
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorem 10.8, uniform convergence of convex functions). https://doi.org/10.1515/9781400873173
• J.-B. Hiriart-Urruty and C. Lemaréchal, Convex Analysis and Minimization Algorithms I, Springer, 1993 (Theorem V.3.3.8, support functions and Hausdorff distance). https://doi.org/10.1007/978-3-662-02796-7
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009 (Chapter 5, statistical inference for SAA). https://doi.org/10.1137/1.9780898718751

Motivation

Many decision problems in operations research ask for the best element of a finite set of alternatives when each alternative's cost is random: which projects to fund when resource use is uncertain, which crew pairings to fly when delays are random, which items to pack into a knapsack whose overflow is penalized. The expected cost is rarely available in closed form, because it is a high-dimensional integral over the distribution of the random data. The sample average approximation (SAA) method replaces the expectation by an average over a random sample and solves the resulting deterministic problem with a standard discrete optimization routine. The method is widely used in stochastic programming (see Shapiro, Dentcheva and Ruszczyński, Lectures on Stochastic Programming, SIAM 2009, Ch. 5, https://doi.org/10.1137/1.9780898718751).

Kleywegt and Shapiro (preprint; published with Homem-de-Mello as SIAM J. Optim. 12(2):479–502, 2002, https://doi.org/10.1137/S1052623499363220) ask why the method works so well for discrete problems. Their answer is a large-deviations statement: when the feasible set is finite, the probability that the SAA problem returns a wrong answer decays exponentially in the sample size. This mission formalizes that result, Proposition 2.2 of the two-author preprint, together with its consistency companion, Proposition 2.1.

Setting

Let $\mathcal S$ be a nonempty finite set, $W$ a random element of a measurable space $\mathcal W$, and $G : \mathcal S \times \mathcal W \to \mathbb R$ such that $G(x,\cdot)$ is measurable and $\mathbb E|G(x,W)| < \infty$ for every $x \in \mathcal S$. The true problem (1.1) is

$$v^* = \min_{x \in \mathcal S} g(x), \qquad g(x) = \mathbb E\, G(x, W).$$

Let $W^1, W^2, \dots$ be an independent, identically distributed sample with the law of $W$. The sample average function and the SAA problem (2.1) are

$$\hat g_N(x) = \frac1N \sum_{n=1}^N G(x, W^n), \qquad \hat v_N = \min_{x \in \mathcal S} \hat g_N(x).$$

For $\varepsilon \ge 0$, the $\varepsilon$-optimal sets are $\mathcal S^\varepsilon = \{x \in \mathcal S : g(x) \le v^* + \varepsilon\}$ and $\hat{\mathcal S}^\varepsilon_N = \{x \in \mathcal S : \hat g_N(x) \le \hat v_N + \varepsilon\}$; at $\varepsilon = 0$ they are the optimal sets $\mathcal S^*$ and $\hat{\mathcal S}_N$. Two numbers drive the analysis: the maximal deviation $\delta_N = \max_{x \in \mathcal S}|\hat g_N(x) - g(x)|$ of (2.2), and the well-conditioning number

$$\alpha(\varepsilon) = \min_{x \in \mathcal S \setminus \mathcal S^\varepsilon} g(x) - v^* - \varepsilon$$

of (2.3), the gap between the $\varepsilon$-optimal solutions and the rest.

For a real random variable $X$ with moment generating function $M(t) = \mathbb E\, e^{tX}$ and logarithmic moment generating function $\Lambda(t) = \log M(t) \in (-\infty, +\infty]$, the rate function is $I(z) = \sup_{t \ge 0}\{tz - \Lambda(t)\}$. Assumption A requires that for every $x \in \mathcal S$ the moment generating function of $G(x, W)$ be finite in a neighbourhood of $t = 0$.

Formalization targets

Goal: Proposition 2.2

Under Assumption A, for every $\varepsilon \ge 0$ there is $\gamma > 0$ with

$$\limsup_{N \to \infty} \frac1N \log\Big[1 - P\big(\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon\big)\Big] \le -\gamma. \tag{2.5}$$

The constant $\gamma$ is not specified: it depends on $\alpha(\varepsilon)$ through rate functions and cannot be computed before the problem is solved. The goal asserts only its existence, which is the paper's claim.

Milestones

1. $\alpha(\varepsilon) > 0$ whenever $\mathcal S \setminus \mathcal S^\varepsilon \ne \emptyset$ (2.3).
2. $\delta_N < \alpha(\varepsilon)/2$ implies $\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$.
3. The union bound $1 - P(\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon) \le \sum_{x \in \mathcal S} P\{|\hat g_N(x) - g(x)| \ge \alpha(\varepsilon)/2\}$.
4. The large-deviations upper bound (2.4): $\frac1N \log P(Z_N \ge a) \le -I(a)$ for i.i.d. averages $Z_N$.
5. $I(a) > 0$ for $a$ above the mean, when $M$ is finite near $0$.
6. Under Assumption A, $P\{|\hat g_N(x) - g(x)| \ge r\} \le e^{-N\gamma_x} + e^{-N\gamma'_x}$ with $\gamma_x, \gamma'_x > 0$.

Companions

Proposition 2.1 ($\hat v_N \to v^*$ w.p.1, and $\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$ w.p.1 for $N$ large enough), the almost-sure convergence $\delta_N \to 0$ of (2.2), the singleton consequence ($\mathcal S^\varepsilon = \{x^*\}$ implies $\hat{\mathcal S}^\varepsilon_N = \{x^*\}$ eventually), the facts $I(\mu) = 0 = \min I$, the Example of §3.2 showing that a sample size $N > k/2$ can be required, and the computation $\alpha(0) = \min_i c_i$ on the hypercube with best value $1/k^{1/p}$ (§4).

Significance

Proposition 2.2 explains the practical behaviour of the SAA method on discrete problems: an exact optimal solution of the true problem is obtained with probability approaching one exponentially fast, so a moderate sample often suffices even when the number of feasible solutions is astronomically large. It is the basis of the paper's replication argument (§3.2: the probability of success $p(N)$ of one SAA replication tends to one exponentially fast) and identifies $\alpha(\varepsilon)$ as the quantity that governs the difficulty of a stochastic discrete problem, which the numerical study of §4 then examines. Later sample-size estimates for SAA (Shapiro, Dentcheva and Ruszczyński 2009, §5.3) refine the same argument into explicit, non-asymptotic bounds.

The result is proved in the paper. The mission produces a machine-checked proof of it and of its ingredients, including a Lean statement of the Cramér–Chernoff upper bound with the rate function $I$ in the extended reals and the positivity of $I$ above the mean under a local moment condition. To our knowledge none of these is formalized on the platform or in Mathlib in this form.

Difficulty

The argument is short on paper; the formal difficulty is in the large-deviations step. Mathlib has the Chernoff inequality $P(X \ge a) \le e^{-ta}\,\mathbb E e^{tX}$ and the factorization of moment generating functions of independent sums, but the step from there to $\frac1N \log P(Z_N \ge a) \le -I(a)$ requires passing to a supremum over $t$ in the extended reals, handling $t$ where $M(t) = \infty$, and the case $P(Z_N \ge a) = 0$. The positivity $I(a) > 0$ requires $\Lambda'(0) = \mu$, i.e. differentiating the moment generating function at an interior point of its domain. A naive attempt that works with real logarithms fails at probability zero, where $\log 0$ is not $-\infty$, and an attempt that bounds $\delta_N$ by Chebyshev's inequality gives only a polynomial rate.

Formalization scope

The feasible set is a Finset of an arbitrary type X, assumed nonempty; minima and maxima over it are Finset.inf' and Finset.sup', so they are attained. The sample is a sequence W : ℕ → Ω → 𝒲 of measurable maps on a probability space, mutually independent (iIndepFun) and identically distributed with W 0; the paper's $W^n$ is W (n - 1), and $g(x)$ is the expectation of $G(x, W^1)$. Measurability of $G(x,\cdot)$ is Borel measurability. Logarithms of probabilities are ENNReal.log, with $\log 0 = -\infty$, and the limit superior in (2.5) is taken in the extended reals; this is the paper's convention and it makes the goal correct when $\mathcal S^\varepsilon = \mathcal S$, where the event is sure. Assumption A is stated as integrability of $e^{tG(x,W)}$ for $t$ near $0$, not through the value of Mathlib's mgf, which is $0$ where the expectation is infinite. The logarithmic moment generating function is the published definition BellWilliams2001.ThresholdPolicy.logMGF (extended-real valued, $+\infty$ off the domain of $M$), and $I$ is the supremum over $t \ge 0$ only, as on p. 3. Wherever $\alpha(\varepsilon)$ appears, the nonemptiness of $\mathcal S \setminus \mathcal S^\varepsilon$ is a hypothesis; the goal does not mention $\alpha$ and needs none.

A trivializing formalization is ruled out: with Real.log the event "$\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$ is sure" would give $\log 0 = 0$ and make the goal false, and a rate function built from mgf would count infinite moment generating functions as $\Lambda = \log 0 = 0$; neither encoding is used.

A complete development needs the Cramér–Chernoff bound for i.i.d. sums with an extended-real rate function, differentiability of the moment generating function at interior points, and the strong law of large numbers applied to finitely many functions. The large-deviations items (milestones 4 and 5, and $I(\mu) = 0$) are stated for an arbitrary i.i.d. real sequence and are reusable beyond this mission. Proofs of any item, including the optional examples, are welcome.

Selected references

• A. J. Kleywegt and A. Shapiro, The sample average approximation method for stochastic discrete optimization, preprint (two-author version), https://edoc.hu-berlin.de/server/api/core/bitstreams/2dcf2d5b-5fb9-44d1-b36a-5e378c803717/content. Published with T. Homem-de-Mello in SIAM J. Optim. 12(2):479–502, 2002. https://doi.org/10.1137/S1052623499363220
• A. Dembo and O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751

Motivation

Block coordinate descent (BCD), also called the nonlinear Gauss–Seidel method or alternating minimization, minimizes a function of several blocks of variables by exactly minimizing over one block at a time while the others are held fixed. It is used wherever the subproblem in a single block is cheap even though the joint problem is not: alternating least squares, EM-type updates, matrix and tensor factorization, Lasso-type regression with separable penalties, and decomposition methods for large structured programs.

Classical convergence theory for BCD asks for differentiability and strict convexity or uniqueness of block minimizers (Bertsekas and Tsitsiklis, 1989; Grippo and Sciandrone, 2000). Many applications have a nondifferentiable, extended-valued objective: a smooth or merely continuous coupling term $f_0$ plus separate penalties or constraint indicators $f_k$ on each block. Tseng (2001) gave convergence results for this setting. Its §5, formalized here, shows that the separable structure lets one drop continuity of $f$ on a level set and replace strict convexity by quasiconvexity and hemivariance in each block.

Timeline. Auslender (1976) proved convergence of cyclic BCD for strongly convex continuous $f_0$ on a product of closed convex sets with convex $f_k$. Bertsekas and Tsitsiklis (1989, Prop. 3.9 in §3.3.5) treated continuously differentiable convex $f_0$ with block-wise unique minimizers. Grippo and Sciandrone (2000, Prop. 5.1) extended this to continuously differentiable, blockwise strictly pseudoconvex $f_0$ with each $f_k$ the indicator of a closed convex set. Tseng (2001, Prop. 5.1 and Thm. 5.1) covers lower semicontinuous, extended-valued $f_0, f_k$ under Assumptions B1–B3 and C1 or C2 below.

Setting

Fix $N\ge1$ and block dimensions $n_1,\dots,n_N$. A point is $x=(x_1,\dots,x_N)$ with $x_k\in\mathbb R^{n_k}$. The objective has form (1):

$$f(x)=f_0(x)+\sum_{k=1}^N f_k(x_k),$$

with $f_0$ and each $f_k$ taking values in $\mathbb R\cup\{\infty\}$. The effective domain of $h$ is $\operatorname{dom}h=\{x:h(x)<\infty\}$.

A function $h$ is quasiconvex if $h(x+\lambda d)\le\max\{h(x),h(x+d)\}$ for all $x,d$ and $\lambda\in[0,1]$, and hemivariate if it is not constant on any nondegenerate line segment contained in $\operatorname{dom}h$.

The BCD method starts at $x^0\in\operatorname{dom}f$. At iteration $r+1$ it chooses a block $s$ and sets $x^{r+1}_s\in\arg\min_{x_s}f(x^r_1,\dots,x^r_{s-1},x_s,x^r_{s+1},\dots,x^r_N)$ and $x^{r+1}_j=x^r_j$ for $j\ne s$. Under the essentially cyclic rule there is a constant $T\ge N$ such that every block is chosen at least once in any $T$ consecutive iterations.

A point $z\in\operatorname{dom}f$ is a coordinatewise minimum point of $f$ if $f(z+(0,\dots,d_k,\dots,0))\ge f(z)$ for every block $k$ and every $d_k\in\mathbb R^{n_k}$.

The assumptions of §5 are:

• (B1) $f_0$ is continuous on $\operatorname{dom}f_0$;
• (B2) for each block $k$ and each value of the other blocks, $x_k\mapsto f(x_1,\dots,x_N)$ is quasiconvex and hemivariate;
• (B3) $f_0,f_1,\dots,f_N$ are lower semicontinuous;
• (C1) $\operatorname{dom}f_0$ is open and $f_0$ tends to $\infty$ at every boundary point of $\operatorname{dom}f_0$, or
• (C2) $\operatorname{dom}f_0=Y_1\times\cdots\times Y_N$ for some sets $Y_k\subseteq\mathbb R^{n_k}$.

Formalization targets

Goal: Theorem 5.1

Under B1–B3, C1 or C2, and boundedness of $\{x:f(x)\le f(x^0)\}$ for some $x^0\in\operatorname{dom}f$,

$$\text{every essentially cyclic BCD sequence from }x^0\text{ is defined, bounded, and each of its cluster points is a coordinatewise minimum point of }f.$$

Proposition 5.1

Without the level-set bound, for every essentially cyclic BCD sequence that is defined,

$$\{f(x^r)\}\downarrow-\infty\quad\text{or}\quad\text{every cluster point of }\{x^r\}\text{ is a coordinatewise minimum point of }f.$$

Milestones

The milestone list follows the paper's proof: attainment of the block minimization on a bounded level set (p. 478); monotonicity of $f(x^r)$ and membership of cluster points in $\operatorname{dom}f$ (p. 485); claim (11), that consecutive iterates share limits along subsequences; its iterate (20) over a window of $T$ steps; inequality (21) at cluster points; Proposition 5.1 itself; and the remark (p. 483) that a quasiconvex hemivariate function has at most one minimum point.

Significance

The result. Theorem 5.1 guarantees that exact block minimization, applied in any order that visits every block within a bounded window, cannot accumulate at points where a single-block move still decreases $f$. It applies to objectives that are neither differentiable nor continuous on their domain and that need not be convex, which covers problems with constraint indicators on each block and couplings with finite values on the boundary of their domain (Assumption C2). Convexity in each block alone is not enough for results of this kind: the paper notes (pp. 483–484) that Theorem 4.1(b) becomes false under that weaker hypothesis, because Powell's three-variable example is convex in each variable.

The formalization. The result is proved in the paper; no machine-checked proof of it, or of a BCD convergence theorem of this kind, has been published. A formal proof would supply a reusable account of extended-valued lower semicontinuous functions on product spaces, of subsequence arguments for descent methods, and of quasiconvexity and hemivariance, none of which is packaged for this purpose in Mathlib.

Difficulty

The obvious argument fixes a cluster point $z$ and a block $k$ and passes to the limit in the block-optimality of the iterates. That needs the iterates in which block $k$ was last updated to converge to the same $z$, and nothing forces consecutive iterates to be close: BCD can oscillate between distinct limit points of different subsequences. Claim (11) supplies this, and it is where quasiconvexity and hemivariance are spent. The second obstacle is passing to the limit in $f_0$, which is only continuous on its domain and only lower semicontinuous globally; Assumption C1 or C2 is what keeps the comparison points inside $\operatorname{dom}f_0$.

Formalization scope

• Points are elements of $\prod_{k}\mathbb R^{n_k}$ ((k : Fin N) → EuclideanSpace ℝ (Fin (n k))), with 0-based blocks: paper block $k$ is Lean index $k-1$. The product carries the sup norm of the blocks; boundedness, convergence, cluster points and semicontinuity are the same as for the Euclidean norm.
• Values are extended reals (EReal). Standing hypotheses: $f_0$ and every $f_k$ never take the value $-\infty$, so $f$ is never $-\infty$ and is $\infty$ exactly when one summand is. The objective is always the sum $f_0+\sum_kf_k$, defined once, never a free function with an equation hypothesis.
• "$\{f(x^r)\}\downarrow-\infty$" is convergence to $-\infty$ in the extended reals.
• A BCD run is a pair $(s,x)$ with $s(r)$ the block chosen at iteration $r+1$. "Defined" in Theorem 5.1 is stated as existence of a run from $x^0$ for every sequence of block choices.
• Hemivariance quantifies over segments with distinct endpoints; otherwise B2 would be unsatisfiable.
• In C1, "boundary point" is the topological frontier. The paper's own $\mathrm{bdry}(S)=S\setminus\mathrm{int}(S)$ is empty for open $S$; under B3 both readings give the same theorem.
• In C2 the sets $Y_k$ are arbitrary: neither closedness nor convexity is assumed.
• B2 is assumed of the whole $f$ in each block, for every value of the other blocks; neither convexity of $f$ nor any property of $f_0$ alone replaces it.

A statement that assumes claim (11), (20) or (21), or that the values $f(x^r)$ converge, would trivialize the goal; the goal and Proposition 5.1 assume none of these.

A complete development needs: compactness of closed bounded sets in the product space and minimization of lower semicontinuous EReal functions on compact sets; subsequence extraction for cluster points; and the segment argument behind (11). Contributions of general lemmas on quasiconvex and hemivariate functions, and on lower semicontinuity of finite sums of EReal functions that avoid $-\infty$, are reusable beyond this mission and welcome.

Selected references

• P. Tseng, Convergence of a block coordinate descent method for nondifferentiable minimization, J. Optim. Theory Appl. 109(3):475–494, 2001. https://doi.org/10.1023/A:1017501703105
• L. Grippo and M. Sciandrone, On the convergence of the block nonlinear Gauss–Seidel method under convex constraints, Oper. Res. Lett. 26:127–136, 2000.
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice-Hall, Englewood Cliffs, NJ, 1989.
• A. Auslender, Optimisation: Méthodes Numériques, Masson, Paris, 1976.
• M. J. D. Powell, On search directions for minimization algorithms, Math. Programming 4:193–201, 1973.

Motivation

Stable distributions were proposed as models of asset returns by Mandelbrot and Fama in the 1960s, because empirical returns show heavier tails than the normal law allows; Rachev and Mittnik's monograph Stable Paretian Models in Finance (2000) collects the later development. When the vector $\varrho$ of per-share returns of $s$ assets follows a multivariate $\alpha$-stable law with $\alpha\in(1,2)$, its distribution is determined by the stability index $\alpha$, a shift $m_0\in\mathbb R^s$, and a finite Borel measure $\Gamma$ on the unit sphere, the spectral measure. The risk of a portfolio is then measured by the scale parameter of the return, and choosing an efficient portfolio becomes a deterministic optimization problem in $(\alpha,\Gamma)$.

In practice neither $\alpha$ nor $\Gamma$ is known: both are estimated from data. Whether the optimal portfolio is robust to estimation error is therefore a practical question. Section 5 of Rachev and Römisch, Quantitative stability in stochastic programming: The method of probability metrics (Math. Oper. Res. 27(4), 2002; this mission follows the authors' preprint), answers it with an explicit modulus, as an application of the paper's general stability theory for stochastic programs under perturbations of the underlying probability measure.

Setting

Fix $s\in\mathbb N$ and equip $\mathbb R^s$ with the Euclidean scalar product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$.

• $\Sigma^s=\{\xi\in\mathbb R^s:\langle\xi,\xi\rangle=1\}$ is the unit sphere, and $\mathcal P(\Sigma^s)$ is the set of Borel probability measures on it (normalized spectral measures).
• $X=\{x\in\mathbb R^s_+:\sum_{i=1}^s x_i=1\}$ is the set of portfolios: $x_i$ is the proportion of shares held in asset $i$.
• For $\alpha\in(1,2)$ and $\Gamma\in\mathcal P(\Sigma^s)$, the risk of $x$ is

$$r_{\alpha,\Gamma}(x)=\int_{\Sigma^s}|\langle x,\xi\rangle|^\alpha\,\Gamma(d\xi).$$

• Problem (22) is $\min\{r_{\alpha,\Gamma}(x):x\in X\}$, with optimal value $v(\alpha,\Gamma)$ and solution set $S(\alpha,\Gamma)$.
• The dual Lipschitz metric $\zeta_1$ (the Fortet–Mourier metric of order $1$) on $\mathcal P(\Sigma^s)$ is

$$\zeta_1(\Gamma,\tilde\Gamma)=\sup\Big\{\Big|\int_{\Sigma^s}f\,d\Gamma-\int_{\Sigma^s}f\,d\tilde\Gamma\Big|: f:\Sigma^s\to\mathbb R,\ |f(\xi)-f(\tilde\xi)|\le\|\xi-\tilde\xi\|\Big\}.$$

• The growth function of (22) is $\psi(\tau)=\min\{r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma): d(x,S(\alpha,\Gamma))\ge\tau,\ x\in X\}$ for $\tau\ge0$, its generalized inverse is $\psi^{-1}(t)=\sup\{\tau\ge0:\psi(\tau)\le t\}$, and the stability modulus is $\Psi(\eta)=\eta+\psi^{-1}(2\eta)$.
• $\Gamma$ is nonsingular if $\int_{\Sigma^s}|\langle x,\xi\rangle|^2\Gamma(d\xi)=0$ implies $x=0$.

Formalization targets

Goal: Theorem 5.2, first assertion (p. 25)

For each $(\alpha,\Gamma)\in(1,2)\times\mathcal P(\Sigma^s)$ there is $\delta>0$ such that

$$\sup_{x\in S(\tilde\alpha,\tilde\Gamma)}d\big(x,S(\alpha,\Gamma)\big)\le\Psi\big(\alpha\,\zeta_1(\Gamma,\tilde\Gamma)+e^{-1}|\alpha-\tilde\alpha|\big)$$

whenever $(\tilde\alpha,\tilde\Gamma)\in(1,2)\times\mathcal P(\Sigma^s)$ and $\zeta_1(\Gamma,\tilde\Gamma)+|\alpha-\tilde\alpha|<\delta$. The modulus $\Psi$ is not fixed: it is whatever the growth of the unperturbed problem gives.

Companion: Theorem 5.2, "Moreover" (p. 25)

If $\Gamma$ is nonsingular, then (22) has a unique solution and $\Psi(\eta)\le C\eta^{1/2}$ for some $C>0$ and all sufficiently small $\eta\ge0$.

Milestones

1. Lemma 5.1, first assertion (p. 24): $f_0(\xi,x)=|\langle x,\xi\rangle|^\alpha$ is convex in $x$, and $|f_0(\xi,x)-f_0(\tilde\xi,\tilde x)|\le\alpha(\|\xi-\tilde\xi\|+\|x-\tilde x\|)$ on $\Sigma^s\times X$.
2. Lemma 5.1, second assertion (p. 24): $S(\alpha,\Gamma)\ne\emptyset$, and $\frac14\alpha(\alpha-1)\int_{\Sigma^s}|\langle x-x_*,z\rangle|^2\Gamma(dz)\le r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma)$ for all $x\in X$ and some $x_*\in S(\alpha,\Gamma)$.
3. Proof of Theorem 5.2 (p. 25): $\sup_{t\in[-1,1]}\big||t|^\alpha-|t|^{\tilde\alpha}\big|\le e^{-1}|\alpha-\tilde\alpha|$.
4. Proof of Theorem 5.2 (p. 25): $|r_{\alpha,\Gamma}(x)-r_{\tilde\alpha,\tilde\Gamma}(x)|\le\alpha\zeta_1(\Gamma,\tilde\Gamma)+e^{-1}|\alpha-\tilde\alpha|$ for $x\in X$.
5. Proof of Theorem 5.2 (p. 25): for nonsingular $\Gamma$, $c\|x\|^2\le\int_{\Sigma^s}|\langle x,\xi\rangle|^2\Gamma(d\xi)$ for some $c=c(s,\Gamma)>0$.
6. Proof of Theorem 5.2 (p. 25): for nonsingular $\Gamma$, (22) has a unique solution $x_*$ and $\frac14c\alpha(\alpha-1)\|x-x_*\|^2\le r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma)$ on $X$.

Significance

The theorem bounds how far the optimal portfolios can move when the stability index and the spectral measure are both perturbed, with a modulus computed from the unperturbed problem alone. Combined with the companion, the efficient portfolio of a nonsingular spectral measure is unique and moves by at most $O\big((\zeta_1(\Gamma,\tilde\Gamma)+|\alpha-\tilde\alpha|)^{1/2}\big)$. Since $\zeta_1$ metrizes weak convergence on the compact sphere, any consistent estimator of $\Gamma$ in the weak topology, together with a consistent estimator of $\alpha$, yields consistent estimates of the optimal portfolio, and convergence rates for $\zeta_1$ translate into rates for the portfolio. The paper notes (Example 5.3) that spectral measures of linear transformations of independent stable variables with a full-rank matrix are nonsingular, so the Hölder case covers the discrete spectral measures used in practice.

The result is proved in the paper; nothing here is open. To our knowledge none of it is machine-checked: Mathlib has strong convexity and the real power function but no stability theory of stochastic programs and no Fortet–Mourier metrics. The mission produces a checked proof of the result and a reusable formal treatment of the growth-function modulus $\Psi$ in a concrete, fully explicit instance.

Difficulty

The obvious argument compares the optimal values of the two problems and concludes that a perturbed minimizer is nearly optimal for the unperturbed problem. Turning near-optimality into a distance bound requires the growth function $\psi$ and its generalized inverse; $\psi$ is defined by an infimum over a set that may be empty, and $\psi^{-1}$ by a supremum that may be infinite, so this step has to be handled in extended arithmetic with care. A second difficulty is the $\zeta_1$ term: the map $\xi\mapsto|\langle x,\xi\rangle|^\alpha$ must be shown to be $\alpha$-Lipschitz on the sphere uniformly over $x\in X$, which uses $\|x\|\le1$ on the simplex. The change of exponent from $\alpha$ to $\tilde\alpha$ is controlled by a sharp calculus inequality whose constant $e^{-1}$ needs $\alpha,\tilde\alpha\ge1$. In the nonsingular case, the quadratic form $\int|\langle x,\xi\rangle|^2\Gamma(d\xi)$ must be shown to dominate $c\|x\|^2$, a compactness argument on the unit sphere of $\mathbb R^s$.

Formalization scope

• $\mathbb R^s$ is EuclideanSpace ℝ (Fin s) with coordinates indexed $0,\dots,s-1$. The paper says "the (Euclidean) scalar product", so Euclidean norms are the paper's own.
• $\Sigma^s$ is Metric.sphere 0 1. A spectral measure is a probability measure on $\mathbb R^s$ with $\Gamma((\Sigma^s)^c)=0$, and every integral is a set integral over $\Sigma^s$. For $s=0$ the sphere is empty, no spectral measure exists, and every statement is vacuous, as in the paper.
• The standing assumption $\alpha\in(1,2)$ of Section 5 is a hypothesis of every statement. The $\alpha$-stable law itself is not formalized: the characteristic function on p. 23 only motivates (22), and the mission captures problem (22) exactly.
• $\zeta_1$ is a supremum in $[0,\infty]$ over functions on $\mathbb R^s$ that are $1$-Lipschitz on $\Sigma^s$, integrated over $\Sigma^s$ only. Such functions are continuous on the compact sphere, so no integral can collapse to a default value. For probability measures, $\zeta_1\le2$.
• $v$ is the real infimum of $r_{\alpha,\Gamma}$ over $X$. $S$ is the set of minimizers. The paper's "min" in $\psi$ is read as an infimum in the extended reals, equal to $+\infty$ when no feasible point is at distance at least $\tau$. Distances to sets are extended distances (Metric.infEDist, $+\infty$ to the empty set), and $\psi^{-1}$ and $\Psi$ take values in $[0,\infty]$.
• Ruled out: a real-valued supremum for $\psi^{-1}$ (which would be $0$ on unbounded sets), a real distance (which is $0$ to the empty set), and test functions integrated over all of $\mathbb R^s$ (whose off-sphere values could make an integral undefined). Any of these would make the goal trivially true.
• "Sufficiently small $\eta$" is read as "all $\eta\in[0,\eta_0]$ for some $\eta_0>0$". Milestone 6 holds for every constant $c>0$ of the norm bound of milestone 5, fixed before $\alpha$, as $c=c(s,\Gamma)$ on the page.

Welcome contributions: the inequality $\big||t|^\alpha-|t|^{\tilde\alpha}\big|\le e^{-1}|\alpha-\tilde\alpha|$ on $[-1,1]$, strong convexity of $|t|^\alpha$ on $[-1,1]$, and a general lemma converting a growth function and a uniform objective perturbation into a distance bound; the last is reusable for every stability result of the paper.

Selected references

• S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: The method of probability metrics, Mathematics of Operations Research 27(4) (2002) 792–818. https://doi.org/10.1287/moor.27.4.792.304 (preprint at edoc.hu-berlin.de, followed here).
• S. T. Rachev, S. Mittnik, Stable Paretian Models in Finance, Wiley, Chichester, 2000 (reference [33] of the paper).
• G. Samorodnitsky, M. S. Taqqu, Stable Non-Gaussian Random Processes, Chapman & Hall, 1994. https://doi.org/10.1201/9780203738818
• B. Mandelbrot, The variation of certain speculative prices, Journal of Business 36(4) (1963) 394–419. https://doi.org/10.1086/294632
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

A stochastic program minimizes an expected cost under expected-value constraints, and the expectation is taken with respect to a probability distribution $\mu$ of the random data. In applications $\mu$ is rarely known: it is estimated from samples, replaced by a finite scenario tree, or chosen from a parametric family. Whether the optimal value and the optimal decisions of the approximate problem are close to those of the true problem therefore decides whether the approximation can be trusted. Quantitative stability asks for explicit bounds on the change of optimal values and solution sets in terms of a distance between $\mu$ and its perturbation $\nu$.

S. T. Rachev and W. Römisch (Quantitative stability in stochastic programming: The method of probability metrics, Math. Oper. Res. 27(4), 2002; this mission follows the authors' preprint) organize this question around a single probability distance, built directly from the integrands of the problem. Their general results (Section 2) are then specialized to two-stage linear and mixed-integer programs, to chance constraints, to empirical approximations, and to a portfolio problem. This mission covers the general part: Proposition 2.1 and Theorems 2.2 and 2.3.

Setting

Let $X\subseteq\mathbb R^m$ be a nonempty closed set, $\Xi\subseteq\mathbb R^s$ a closed set, and $f_j:\Xi\times\mathbb R^m\to\overline{\mathbb R}$, $j=0,\dots,d$, normal integrands: each epigraph $\{(x,r):f_j(\xi,x)\le r\}$ is closed and the epigraphical mapping $\xi\mapsto\operatorname{epi} f_j(\xi,\cdot)$ is measurable. For a Borel probability measure $\nu$ on $\Xi$ the problem is

$$\min\Big\{\int_\Xi f_0(\xi,x)\,\nu(d\xi):\ x\in X,\ \int_\Xi f_j(\xi,x)\,\nu(d\xi)\le0,\ j=1,\dots,d\Big\},$$

with feasible set $M(\nu)$, optimal value $v(\nu)$ and solution set $S(\nu)$; $\mu$ is the original measure.

For a nonempty set $\mathcal U\subseteq\mathbb R^m$, the localized problem restricts $x$ to $X\cap\operatorname{cl}\mathcal U$, with feasible set $M_{\mathcal U}(\nu)$, value $v_{\mathcal U}(\nu)$ and solutions $S_{\mathcal U}(\nu)$. The admissible measures $\mathcal P_{\mathcal F_{\mathcal U}}$ are those under which $\int\inf_{x\in X,\|x\|\le r}f_j(\xi,x)\nu(d\xi)>-\infty$ for every $r>0$ and $\sup_{x\in X\cap\operatorname{cl}\mathcal U}\int f_j(\xi,x)\nu(d\xi)<\infty$. The minimal information distance is

$$d_{\mathcal F_{\mathcal U}}(\mu,\nu)=\sup_{x\in X\cap\operatorname{cl}\mathcal U}\ \max_{j=0,\dots,d}\Big|\int_\Xi f_j(\xi,x)\,\mu(d\xi)-\int_\Xi f_j(\xi,x)\,\nu(d\xi)\Big|.$$

The constraints are metrically regular at $(\bar x,0)$ if there are $a\ge0$, $\varepsilon>0$ with $d(x,M_y(\mu))\le a\max_j\max\{0,\int f_j(\xi,x)\mu(d\xi)-y_j\}$ for $x\in X$ near $\bar x$ and small $y\in\mathbb R^d$, where $M_y(\mu)$ is the feasible set with right-hand sides $y$. A nonempty set is a CLM set (complete local minimizing set) with respect to an open $\mathcal U$ if it equals $S_{\mathcal U}(\nu)$ and lies in $\mathcal U$. The growth function is $\psi(\tau)=\inf\{\int f_0(\xi,x)\mu(d\xi)-v(\mu):d(x,S(\mu))\ge\tau,\ x\in M_{\mathcal U}(\mu)\}$, with $\psi^{-1}(t)=\sup\{\tau\ge0:\psi(\tau)\le t\}$ and $\Psi(\eta)=\eta+\psi^{-1}(\eta)$.

Formalization targets

Goal: Theorem 2.3, δ-local form

Under the assumptions of Theorem 2.2 — $\mu\in\mathcal P_{\mathcal F_{\mathcal U}}$; $S(\mu)\ne\emptyset$ and $\mathcal U$ an open bounded neighbourhood of $S(\mu)$; if $d\ge1$, $x\mapsto\int f_0(\xi,x)\mu(d\xi)$ Lipschitz on $X\cap\operatorname{cl}\mathcal U$; metric regularity at every $(\bar x,0)$, $\bar x\in S(\mu)$ — there are $\hat L\ge1$ and $\delta>0$ with

$$\emptyset\ne S_{\mathcal U}(\nu)\subseteq S(\mu)+\Psi\big(\hat L\,d_{\mathcal F_{\mathcal U}}(\mu,\nu)\big)\mathbb B\qquad\text{for all }\nu\in\mathcal P_{\mathcal F_{\mathcal U}},\ d_{\mathcal F_{\mathcal U}}(\mu,\nu)<\delta.$$

The constants are existential: the goal fixes the shape of the estimate, not its constants.

Milestones

1. Proposition 2.1: $(x,\nu)\mapsto\int f_j(\xi,x)\nu(d\xi)$ is lower semicontinuous on $(X\cap\operatorname{cl}\mathcal U)\times(\mathcal P_{\mathcal F_{\mathcal U}},d_{\mathcal F_{\mathcal U}})$, and $\nu\mapsto M_{\mathcal U}(\nu)$ has a closed graph.
2. Display (5) and its converse: near $\bar x\in S(\mu)$, $M_{\mathcal U}(\mu)$ and $M_{\mathcal U}(\nu)$ lie within $a\,d_{\mathcal F_{\mathcal U}}(\mu,\nu)$ of each other.
3. Theorem 2.2: Berge upper semicontinuity of $S_{\mathcal U}$ at $\mu$, the Lipschitz estimate $|v(\mu)-v_{\mathcal U}(\nu)|\le L\,d_{\mathcal F_{\mathcal U}}(\mu,\nu)$, and the CLM property, for $\nu$ near $\mu$; for $d=0$, the estimate with $L=1$ for all $\nu$.
4. Theorem 2.3 for $d=0$, for every $\nu\in\mathcal P_{\mathcal F_{\mathcal U}}$, as printed.

Significance

Theorem 2.2 shows that the distance $d_{\mathcal F_{\mathcal U}}$ carries exactly the information about $\mu$ that the problem uses: any probability metric that dominates it inherits the Lipschitz estimate of optimal values. This is the mechanism by which the paper derives stability with respect to Fortet–Mourier metrics for two-stage programs, with respect to discrepancies for mixed-integer and chance-constrained programs, and convergence rates for empirical approximations via empirical-process bounds. Theorem 2.3 adds the solution sets: their deviation is controlled by $\Psi$, which is determined by the growth of the objective near $S(\mu)$; quadratic growth yields Hölder continuity with rate $\tfrac12$ (Remark 2.4).

The results are proved on paper. No machine-checked version of these stability theorems, of metric regularity for expected-value constraints, or of the minimal information distance exists on the platform. The formalization also settles the exact quantifier structure of Theorem 2.3: its printed form ("for each $\nu$") is true only for $d=0$, and the mission states the δ-local form that the proof establishes.

Difficulty

The obvious argument compares the two problems pointwise in $x$: the integrals differ by at most $d_{\mathcal F_{\mathcal U}}(\mu,\nu)$, so the optimal values should too. This works without constraints, but with $d\ge1$ the feasible sets themselves move, and a point feasible for $\mu$ need not be feasible for $\nu$. Controlling this displacement needs metric regularity of the constraint system, which is only local, around each point of $S(\mu)$; passing from local to uniform constants requires compactness of $S(\mu)$ and a covering argument. A second difficulty is extended-real analysis: the integrands take the value $+\infty$, lower semicontinuity must come from Fatou's lemma under the integrability conditions defining $\mathcal P_{\mathcal F_{\mathcal U}}$, and the existence of localized solutions depends on this lower semicontinuity on the compact set $X\cap\operatorname{cl}\mathcal U$.

Formalization scope

$\mathbb R^m$ and $\mathbb R^s$ are EuclideanSpace ℝ (Fin m), EuclideanSpace ℝ (Fin s); the paper never fixes its norm, and every statement has existential constants, so the Euclidean norm is a faithful instance. Measures are Borel probability measures on the subtype $\Xi$. Integrals of extended-real integrands use the published DupacovaWets.Consistency.expect ($+\infty$ when $\int f^+=\infty$). The integrands are indexed by Fin (d+1), with index $0$ the objective. Values $v$, $v_{\mathcal U}$ and $\psi$ are infima in $\overline{\mathbb R}$ ($+\infty$ on empty sets; the paper's "min" in $\psi$ is read as an infimum); $d_{\mathcal F_{\mathcal U}}$, $\psi^{-1}$ and $\Psi$ take values in $[0,\infty]$; distances to sets are extended distances (infinite to the empty set). Lower semicontinuity and closed graphs in Proposition 2.1 are stated sequentially, which is equivalent in the extended pseudometric space $(\mathcal P_{\mathcal F_{\mathcal U}},d_{\mathcal F_{\mathcal U}})$. The balls $B(\bar x,\bar\varepsilon)$ in (5) are closed balls.

Standing assumptions carried by every statement: $X$ nonempty and closed, $\Xi$ closed, all $f_j$ normal integrands, and measures in $\mathcal P_{\mathcal F_{\mathcal U}}$. Every value estimate asserts that both optimal values are finite, so no bound holds through an $\infty-\infty$ convention, and the distance to an empty feasible set is $+\infty$, so metric regularity cannot hold vacuously. The one deliberate deviation from the page is the δ in the goal, explained above.

A complete development needs Fatou's lemma for extended-real integrands bounded below by an integrable function, measurability of infima of normal integrands, and Berge's stability theorem for parametric programs. The first two are reusable for every stochastic-programming mission on the platform. Contributions of these lemmas as separate theorems are welcome.

Selected references

• S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: The method of probability metrics, Math. Oper. Res. 27(4) (2002), 792–818. https://doi.org/10.1287/moor.27.4.792.304
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (normal integrands, Ch. 14; metric regularity, Ch. 9). https://doi.org/10.1007/978-3-642-02431-3
• B. Bank, J. Guddat, D. Klatte, B. Kummer, K. Tammer, Non-Linear Parametric Optimization, Akademie-Verlag, Berlin, 1982 (Berge stability, Thm. 4.2.1).
• D. Klatte, A note on quantitative stability results in nonlinear optimization, in: Proceedings 19. Jahrestagung Mathematische Optimierung, Seminarbericht Nr. 90, Humboldt-Universität Berlin, 1987, 77–86 (the proof pattern of Theorem 2.2).

Motivation

AdaBoost (Freund and Schapire, 1996) combines many weak classifiers, such as small decision trees, into a single strong classifier by repeatedly reweighting the training data. In the late 1990s it was among the most accurate off-the-shelf classifiers, but why it worked was unclear. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) gave a statistical explanation: AdaBoost fits an additive model by stagewise minimization of the exponential criterion $E(e^{-yF(x)})$, and the population minimizer of that criterion is half the log-odds of the class probability. Boosting is therefore a form of additive logistic regression. This reading underlies gradient boosting, LogitBoost, and the later theory of classification-calibrated surrogate losses.

The exponential criterion was introduced by Schapire and Singer (1998) as an upper bound on misclassification error, and Breiman (1997) used it in his analysis of AdaBoost. Lemma 1 of the 2000 paper is the statement that identifies its population minimizer.

Setting

A feature $x$ ranges over a measurable space $X$ and a label $y$ takes the values $-1$ and $1$. The pair $(x, y)$ has a joint law $\nu$, a probability measure on $X \times \{-1, 1\}$, with marginal $\nu_X$ on $X$. Disintegrating $\nu$ gives the conditional class probabilities $P(y = 1 \mid x)$ and $P(y = -1 \mid x)$.

For a function $F : X \to \mathbb R$ the exponential criterion (11) is the joint expectation

$$J(F) = E\big(e^{-yF(x)}\big) = \int e^{-yF(x)}\, d\nu(x, y),$$

a number in $[0, \infty]$. Its conditional version at $x$ is $E(e^{-yF(x)} \mid x)$. Given a current estimate $F$, the weighted conditional expectation with weight $w(x, y) = e^{-yF(x)}$ is

$$E_w[g(x, y) \mid x] = \frac{E[w(x, y)\, g(x, y) \mid x]}{E[w(x, y) \mid x]},$$

and $P_w(y = \pm 1 \mid x) = E_w[1_{[y = \pm 1]} \mid x]$. The half log-odds is

$$F^\star(x) = \tfrac12 \log \frac{P(y = 1 \mid x)}{P(y = -1 \mid x)}.$$

Formalization targets

Goal: Lemma 1

Assume $0 < P(y = 1 \mid x) < 1$ for $\nu_X$-almost every $x$. Then $F^\star$ is measurable, and for every measurable $F : X \to \mathbb R$,

$$E\big(e^{-yF^\star(x)}\big) \le E\big(e^{-yF(x)}\big),$$

and, for $\nu_X$-almost every $x$, (13) and (14) hold:

$$P(y = 1 \mid x) = \frac{e^{F^\star(x)}}{e^{-F^\star(x)} + e^{F^\star(x)}}, \qquad P(y = -1 \mid x) = \frac{e^{-F^\star(x)}}{e^{-F^\star(x)} + e^{F^\star(x)}}.$$

Milestones

1. The conditional criterion (proof of Lemma 1): $E(e^{-yF(x)} \mid x) = P(y = 1 \mid x) e^{-F(x)} + P(y = -1 \mid x) e^{F(x)}$, and $J(F)$ is the $\nu_X$-average of the conditional criterion for measurable $F$.
2. Its derivative in $F(x)$: $-P(y = 1 \mid x) e^{-F(x)} + P(y = -1 \mid x) e^{F(x)}$.
3. Corollary 3: at an optimal $F$, the weighted conditional mean of $y$ vanishes, $E_w(y \mid x) = 0$ almost everywhere.
4. Result 2 with (23)–(24): for a measurable current estimate $F$, the Real AdaBoost step $f(x) = \tfrac12 \log\big(P_w(y = 1 \mid x)/P_w(y = -1 \mid x)\big)$ minimizes $J(F + f)$ over measurable $f$, and $F + f = F^\star$ almost everywhere.
5. Corollary 1: on a region where $F$ is a constant $c$, the average of $e^{-y_i c}$ is minimized at $c = \tfrac12 \log(n_+/n_-)$, and the sample proportions are the symmetric logistic transform of that $c$.
6. Display (15): $e^{F}/(e^{-F} + e^{F}) = e^{2F}/(1 + e^{2F})$, so the symmetric logistic transform of (13) is the usual logistic model with a factor $2$.

Significance

Lemma 1 is what makes the rest of the paper a statement about logistic regression. Because the minimizer of $J$ is the half log-odds, an additive model $F = \sum_m f_m$ built by minimizing $J$ estimates $\tfrac12 \operatorname{logit} P(y = 1 \mid x)$, and the transform (13) converts it into a class probability. Result 2 shows that one population step of Real AdaBoost from any starting point already reaches $F^\star$, so the many iterations used in practice come from the crude approximation of conditional expectations by trees, not from the criterion. Corollary 3 gives the first-order condition used to interpret the AdaBoost weights. The other missions of this series (Discrete AdaBoost, LogitBoost, Gentle AdaBoost, multiclass LogitBoost) all rest on these population facts.

All of these results are proved in the paper; none is open. What this mission adds is a machine-checked version in the population setting, with conditional probabilities obtained from an honest disintegration of the joint law instead of being postulated. No formalization of the exponential criterion's population minimizer is known to exist on the platform or in Mathlib. The pointwise calculus is elementary; the work is in the measure-theoretic layer.

Difficulty

The paper's proof minimizes the conditional criterion pointwise and sets the derivative to zero. Turning this into a statement about $J$ requires three things the one-line proof does not mention. First, the joint expectation must be rewritten as an iterated integral, which needs the disintegration of $\nu$ and measurability of everything integrated. Second, the pointwise minimizer $F^\star$ must itself be a measurable function of $x$, which the calculus says nothing about. Third, the comparison is against every measurable competitor, including those with $J(F) = \infty$, so integrability cannot be assumed. Corollary 3 has a further difficulty: it assumes nothing about the class probabilities, so a proof must show that optimality of $F$ forces them strictly between $0$ and $1$ almost everywhere, a fact the paper's one-line proof does not address.

Formalization scope

Labels live on Bool, with sgn true = 1 and sgn false = -1. The joint law is ν : Measure (X × Bool) with [IsProbabilityMeasure ν] on an arbitrary measurable space X. $P(y = b \mid x)$ is (ν.condKernel x {b}).toReal, read off Mathlib's conditional kernel. It is determined only $\nu_X$-almost everywhere, so (13), (14), Corollary 3 and the identity of Result 2 are almost-everywhere statements; the conditional formula and its derivative hold at every $x$. $J$ is a lower Lebesgue integral in $[0, \infty]$. Competitors range over all measurable functions $X \to \mathbb R$. Derivatives are stated with HasDerivAt.

The hypothesis $0 < P(y = 1 \mid x) < 1$ almost everywhere is added to Lemma 1 and Result 2. Without it the ratio in (12) is $0$ or undefined, Real.log 0 = 0 would give a junk value, and no minimizer of $J$ exists. Corollary 1 assumes both labels occur in the region, which is the sample counterpart.

Several formalizations would make the targets trivial, and none is used here. Defining $J$ through its conditional formula would make milestone 1 a definition and the goal pointwise, so $J$ is the joint expectation under $\nu$. A Bochner integral would return $0$ for a non-integrable $e^{-yF}$ and make every such $F$ a minimizer, so $J$ takes values in $[0, \infty]$. A bare deriv is $0$ at points of non-differentiability. Writing the logistic transform as $1/(1 + e^{-F})$ in place of $e^{F}/(e^{-F} + e^{F})$ would lose the factor $2$ that (15) records.

A complete development needs the disintegration of a measure on $X \times \mathrm{Bool}$, iterated lower integrals, measurability of the conditional kernel, and elementary calculus of $t \mapsto a e^{-t} + b e^{t}$. Lemmas about conditional expectations against condKernel on a finite label set, and the measurability of $x \mapsto P(y = 1 \mid x)$, are reusable in the other missions of this series. Contributions of either kind are welcome.

Selected references

• J. Friedman, T. Hastie and R. Tibshirani, Additive logistic regression: a statistical view of boosting (with discussion), Annals of Statistics 28(2), 337–407, 2000. https://doi.org/10.1214/aos/1016218223
• Y. Freund and R. E. Schapire, Experiments with a new boosting algorithm, Proceedings of ICML, 148–156, 1996. https://dl.acm.org/doi/10.5555/3091696.3091715
• R. E. Schapire and Y. Singer, Improved boosting algorithms using confidence-rated predictions, Proceedings of COLT, 80–91, 1998; Machine Learning 37, 297–336, 1999. https://doi.org/10.1023/A:1007614523901
• L. Breiman, Prediction games and arcing algorithms, Technical Report 504, Statistics Department, UC Berkeley, 1997; Neural Computation 11(7), 1493–1517, 1999. https://doi.org/10.1162/089976699300016106