Optimization

Convex Optimization Operations Research Probability·Captain: mikedeng1

The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs: Fully-Supported Problems Attain the Binomial Violation Tail ExactlyResearch Paper

Motivation

Many design problems in control, finance and engineering are convex programs whose constraints depend on an uncertain parameter $\delta$ : a solution must satisfy $x\in\mathcal X_\delta$ for every $\delta$ in a possibly infinite set $\Delta$ . Enforcing all constraints (robust optimization) is often intractable or overly conservative. The scenario approach draws $N$ independent samples of $\delta$ , solves the convex program with those $N$ constraints only, and asks how likely it is that the resulting solution violates a fresh constraint. The question matters wherever a randomized design is certified by a confidence statement, from robust control to chance-constrained portfolio selection.

Timeline.

Calafiore and Campi (Math. Program. 2005; IEEE TAC 2006) introduced the method and bounded the probability that the violation exceeds $\varepsilon$ by a quantity of order $\binom Nd(1-\varepsilon)^{N-d}$ . The bound is valid but loose.
Campi and Garatti (SIAM J. Optim. 2008, this mission's source) proved the bound $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ for every convex problem satisfying existence and uniqueness of solutions. They showed it is attained with equality by every fully-supported problem, so it cannot be improved without further assumptions.
Later work extended the result to non-unique solutions, constraint removal, and non-convex decisions (Campi and Garatti, Introduction to the Scenario Approach, SIAM 2018).

Setting

Let $(\Delta,\mathcal D,\mathbb P)$ be a probability space, $c\in\mathbb R^d$ with $d\ge1$ , and let $\mathcal X\subseteq\mathbb R^d$ and $\mathcal X_\delta\subseteq\mathbb R^d$ ( $\delta\in\Delta$ ) be convex closed sets. The violation probability of a point $x$ is

V(x)=\mathbb P\{\delta\in\Delta:\ x\notin\mathcal X_\delta\}.

For a multi-extraction $(\delta^{(1)},\dots,\delta^{(m)})\in\Delta^m$ , the program $P_m$ minimises $c^\top x$ over $x\in\mathcal X\cap\bigcap_{i=1}^m\mathcal X_{\delta^{(i)}}$ . It is assumed that every $P_m$ has a unique solution $x^*_m$ . A constraint $\delta^{(r)}$ is a support constraint of $P_m$ if its removal changes the solution. A convex $P_m$ has at most $d$ support constraints (Proposition 2.2). The problem is fully-supported if, for every $m\ge d$ , the program $P_m$ built from $m$ independent samples has exactly $d$ support constraints with $\mathbb P^m$ -probability one.

Two further objects carry the argument. For $\mathcal I\subseteq\{1,\dots,m\}$ of cardinality $d$ , $S_{\mathcal I}$ is the set of multi-extractions whose support constraints have exactly the indexes in $\mathcal I$ . The violation law is

F(\alpha)=\mathbb P^d\{V(x^*_d)\le\alpha\},

the distribution of the violation of the solution built from $d$ samples.

Formalization targets

Goal: Theorem 2.4, equation (2.3)

For a fully-supported problem, every $N\ge d$ and every $\varepsilon\in[0,1]$ ,

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

Milestones (PART 1 of §3)

Proposition 2.2: at most $d$ support constraints.
$S_{\bar{\mathcal I}}\subseteq\widetilde S_{\bar{\mathcal I}}$ for $\bar{\mathcal I}=\{1,\dots,d\}$ , where $\widetilde S_{\bar{\mathcal I}}$ is the set where $\delta^{(d+1)},\dots,\delta^{(m)}$ are not violated by the solution generated by $\delta^{(1)},\dots,\delta^{(d)}$ ; and $\widetilde S_{\bar{\mathcal I}}\subseteq S_{\bar{\mathcal I}}$ up to a probability-zero set.
(3.3): $\mathbb P^m\{S_{\mathcal I}\}=\int_0^1(1-\alpha)^{m-d}F(\mathrm d\alpha)$ for every $\mathcal I$ of cardinality $d$ .
(3.4): $\binom md\int_0^1(1-\alpha)^{m-d}F(\mathrm d\alpha)=1$ for all $m\ge d$ .
Moment uniqueness: $F(\alpha)=\alpha^d$ is the only distribution on $[0,1]$ satisfying (3.4).
(3.2): $F(\alpha)=\alpha^d$ .
Partition chain: $\mathbb P^N\{V(x^*_N)>\varepsilon\}=\binom Nd\int_{(\varepsilon,1]}(1-\alpha)^{N-d}F(\mathrm d\alpha)$ .
Integration by parts: $\binom Nd\int_\varepsilon^1(1-\alpha)^{N-d}\,d\,\alpha^{d-1}\,\mathrm d\alpha=\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ .

Significance

The result. Equation (2.3) shows that the scenario bound (2.2) is tight: no bound that depends only on $N$ , $d$ and $\varepsilon$ can be smaller, because a fully-supported problem attains it. The distribution of $V(x^*_N)$ is then a Beta law, $\mathbb P^N\{V(x^*_N)\le\varepsilon\}$ being the probability that a $\mathrm{Binomial}(N,\varepsilon)$ variable is at least $d$ , the same for every fully-supported problem. This is what fixes the sample sizes used in practice: $N$ is chosen so that the binomial tail is below a confidence level $\beta$ . Fact (3.2), that $V(x^*_d)$ has distribution function $\alpha^d$ whatever the problem, is a distribution-free statement of independent interest.

Formalizing it. The result is proved in the source. As far as is known it has no machine-checked proof. The goal statement is already posed on the platform, and this mission supplies the paper's proof structure as milestones. Two milestones are reusable outside the scenario approach: the uniqueness of a distribution on $[0,1]$ given the moments $\int(1-\alpha)^k\,\mathrm dF=1/\binom{d+k}d$ , and the incomplete-beta identity for binomial tails.

Difficulty

The obvious route would compute the law of $V(x^*_N)$ directly, but it depends on the geometry of the constraints. The paper never computes it. It obtains the law of $V(x^*_d)$ only implicitly, through the infinite family of identities (3.4), and recovers it by a uniqueness theorem for moment problems. Two points need care. First, full support holds only almost surely: duplicated samples, for instance, produce programs with fewer than $d$ support constraints, so every set identity holds only up to null sets. Second, the claim that removing a non-support constraint keeps the first $d$ constraints as the only support constraints uses Proposition 2.2. Two identical non-support constraints show that a constraint can become a support constraint after another is removed, unless the count is bounded by $d$ .

Formalization scope

Goal. The goal is the already-posed platform statement ScenarioApproach.Generalization.violation_tail_eq_binomial_sum_of_fullySupported (theorem id cffaa932-832c-42ca-9e81-1848ffab7e34), referenced as it stands and not restated. Proposition 2.2 is the platform statement card_support_constraints_le_dim (f70e8aa3-…). This mission adds the PART 1 steps as milestones under ScenarioExact.PartOne.

Representation. Decisions are vectors in EuclideanSpace ℝ (Fin d). A multi-extraction is ω : Fin m → Δ, with 0-based indexes, so $\bar{\mathcal I}$ is $\{i : i<d\}$ and " $\delta^{(d+1)},\dots,\delta^{(m)}$ " are the indexes $j\ge d$ . $\mathbb P^m$ is Measure.pi (fun _ : Fin m => P). $V$ , the feasible set, solutions, support constraints and full support are the published definitions violation, feasibleSet, IsSolution, IsSupportConstraint and FullySupported. A support constraint is one whose removal admits a feasible point of strictly smaller cost, which under uniqueness is the paper's "its removal changes the solution". Full support is almost sure, not pointwise.

Hypotheses made explicit. Assumption 1 is entered as existence and uniqueness of the solution for every number of constraints and every sample, together with a family of solution maps θs k, each assumed to solve $P_k$ and to be measurable. Under uniqueness, θs N is the goal's solution map. The paper's "measurability ... is assumed for granted" (p. 4) is replaced by joint measurability of $\{(x,\delta):x\in\mathcal X_\delta\}$ and measurability of the solution maps, the same two hypotheses as the goal. No set $S_{\mathcal I}$ is assumed measurable. The nonempty-interior clause of Assumption 1 is unused in PART 1 and is not assumed, so the milestones compose with the goal.

Conventions. $F$ is the push-forward measure violationLaw on $\mathbb R$ , with $F(\alpha)$ = violationLaw … (Set.Iic α). Integrals against $F$ are lower Lebesgue integrals of nonnegative integrands, as extended nonnegative reals: over $[0,1]$ for $\int_0^1$ , and over $(\varepsilon,1]$ for $\int_\varepsilon^1$ in the partition chain, since that integral comes from the event $V>\varepsilon$ . The integration-by-parts identity is a real interval integral. Ranges are $1\le d$ , $d\le m$ , $d\le N$ and $0\le\varepsilon\le1$ .

Ruled out. A pointwise "exactly $d$ support constraints for every sample" would be unsatisfiable for many problems (repeated samples) and would trivialise the probabilistic content, so it is not used. Assuming measurability of the event $\{V(x^*_N)>\varepsilon\}$ or of $S_{\mathcal I}$ , or the identity $\mathbb P^m\{S_{\mathcal I}\}=\mathbb P^m\{\widetilde S_{\mathcal I}\}$ , as a hypothesis would assume part of the conclusion, so none of these is a hypothesis.

Infrastructure. A complete development needs: the support-constraint count (Proposition 2.2, a Helly-type argument), invariance of product measures under coordinate permutations, the change-of-variables formula for push-forward measures, the Hausdorff moment uniqueness theorem on $[0,1]$ , and the binomial–incomplete-beta identity. The last two are general results, and contributions of them are welcome independently.

Selected references

M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM J. Optim. 19(3) (2008) 1211–1230. https://doi.org/10.1137/07069821X
G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Math. Program. 102 (2005) 25–46. https://doi.org/10.1007/s10107-003-0499-y
G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Trans. Automat. Control 51(5) (2006) 742–753. https://doi.org/10.1109/TAC.2006.875041
M. C. Campi, S. Garatti, Introduction to the Scenario Approach, SIAM, 2018. https://doi.org/10.1137/1.9781611975444
A. N. Shiryaev, Probability, 2nd ed., Springer, 1996, Chapter II, §12. https://doi.org/10.1007/978-1-4757-2539-1

14 thms1 active userReviewed

Combinatorics Convex Optimization Probability·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XVII: Goemans–Williamson Rounding of the MAXCUT SDP Relaxation Has Expected Value at Least 0.878 Times the Maximum CutTextbook

Motivation

MAXCUT asks for a partition of the vertices of a weighted graph into two sets that maximizes the total weight of the edges between them. It is one of Karp's original NP-hard problems, so no polynomial-time exact algorithm is expected, and the natural question is how close a polynomial-time algorithm can come to the optimum. Sampling a uniformly random partition already achieves, in expectation, half of the optimal value. For two decades this factor $1/2$ was essentially the best known.

Goemans and Williamson (J. ACM 42(6), 1995) replaced the combinatorial problem by a semidefinite relaxation, solvable in polynomial time by interior point methods, and rounded its solution with a random Gaussian hyperplane. They proved that the resulting cut has expected weight at least $0.878$ times the maximum. The technique founded the use of semidefinite programming in approximation algorithms. Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) showed that, assuming the Unique Games Conjecture, no polynomial-time algorithm achieves a better constant. Nesterov (Optim. Methods Softw. 9, 1998) extended the rounding analysis to maximizing any positive semidefinite quadratic form over the hypercube, with the constant $2/\pi$ .

This mission formalizes the presentation of these results in §6.6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 343–347.

Setting

Let $n\ge 0$ and let $A\in\mathbb R^{n\times n}$ be a symmetric matrix with non-negative entries; $A_{i,j}$ is the weight between points $i$ and $j$ . The graph Laplacian is $L=D-A$ , where $D$ is the diagonal matrix with entries $\sum_{j=1}^n A_{i,j}$ . For $x\in\{-1,1\}^n$ the vector $x$ encodes a partition, and MAXCUT is (6.7)

\max_{x\in\{-1,1\}^n} x^\top L x .

Write $\langle M,X\rangle=\operatorname{Tr}(M^\top X)$ for the Frobenius inner product and $\mathbb S^n_+$ for the symmetric positive semidefinite matrices. Since $x^\top Lx=\langle L,xx^\top\rangle$ and $xx^\top\in\mathbb S^n_+$ has unit diagonal, MAXCUT is bounded above by the SDP relaxation

\max\bigl\{\langle L,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1,\ i\in[n]\bigr\}.

A solution $\Sigma$ of the relaxation is any feasible matrix attaining this maximum. The rounding draws $\xi\sim\mathcal N(0,\Sigma)$ , a centered Gaussian vector with covariance $\Sigma$ , and outputs $\zeta=\operatorname{sign}(\xi)\in\{-1,1\}^n$ coordinatewise.

Formalization targets

Goal: Theorem 6.11 (Goemans–Williamson)

For $A$ symmetric with non-negative entries, $L=D-A$ , $\Sigma$ any solution of the relaxation, $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$ :

\mathbb E\,\zeta^\top L\zeta\ \ge\ 0.878\max_{x\in\{-1,1\}^n}x^\top Lx.

Milestones

Bounded entries. If $\Sigma\in\mathbb S^n_+$ and $\Sigma_{i,i}=1$ , then $|\Sigma_{i,j}|\le 1$ (remark in the proof of Lemma 6.12).
Lemma 6.12 (Sheppard's formula). If $\xi\sim\mathcal N(0,\Sigma)$ with $\Sigma_{i,i}=1$ and $\zeta=\operatorname{sign}(\xi)$ , then $\mathbb E\,\zeta_i\zeta_j=\frac{2}{\pi}\arcsin(\Sigma_{i,j})$ .
Inequality (6.8). $1-\frac{2}{\pi}\arcsin(t)\ge 0.878(1-t)$ for all $t\in[-1,1]$ .
Relaxation inequality. $\max_{x}x^\top Lx=\max_x\langle L,xx^\top\rangle\le\langle L,\Sigma\rangle$ for every solution $\Sigma$ .

The separately stated Laplacian identity on p. 346 is also included as a theorem item: if $X_{i,i}=1$ for all $i$ , then $\langle L,X\rangle=\sum_{i,j}A_{i,j}(1-X_{i,j})$ ; for $x\in\{-1,1\}^n$ , $x^\top Lx=\sum_{i,j}A_{i,j}(1-x_ix_j)$ .

Companion: Theorem 6.13 (Nesterov)

For $B\in\mathbb S^n_+$ , $\Sigma$ a solution of $\max\{\langle B,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1\}$ , $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$ :

\mathbb E\,\zeta^\top B\zeta\ \ge\ \frac{2}{\pi}\max_{x\in\{-1,1\}^n}x^\top Bx.

Significance

The result. Theorem 6.11 is a polynomial-time randomized $0.878$ -approximation for MAXCUT: the relaxation is a semidefinite program, and sampling a Gaussian vector and taking signs is cheap. Repeated sampling turns the bound in expectation into a cut of value close to $0.878$ times the optimum with high probability. The same scheme of relaxation followed by randomized rounding underlies approximation algorithms for MAX-2SAT, correlation clustering and quadratic programs over the hypercube, and Nesterov's Theorem 6.13 is the version for an arbitrary positive semidefinite objective.

Formalizing it. Both theorems were proved long ago. To our knowledge neither has a machine-checked proof in Mathlib. The platform has related statements from other books, in different forms: Grothendieck's identity for a standard Gaussian and two unit vectors, and the relaxation guarantee with a Grothendieck constant. This mission states the textbook's results for a Gaussian with a possibly singular covariance matrix, which is the form the rounding uses. A complete development needs Sheppard's formula for a degenerate bivariate Gaussian, an elementary but careful real-variable inequality, and a link between Mathlib's multivariate Gaussian and Gram factorizations of $\Sigma$ . All three are reusable.

Difficulty

The algebra (the Laplacian identity and milestone 4) is routine. The probabilistic core is Lemma 6.12. The textbook argument reduces it to the probability that a uniformly random direction separates two unit vectors, which is "a quick picture" on paper. In Lean this requires showing that the pair $(\xi_i,\xi_j)$ has the law of $(\langle V_i,\varepsilon\rangle,\langle V_j,\varepsilon\rangle)$ for a standard Gaussian $\varepsilon$ , and then computing an angular measure in the plane, including the degenerate cases $\Sigma_{i,j}=\pm1$ , where the pair is supported on a line. A density-based argument fails there, because $\mathcal N(0,\Sigma)$ has no density when $\Sigma$ is singular, and singular solutions of the relaxation occur (for instance $\Sigma=xx^\top$ ). Inequality (6.8) is a statement about a transcendental function on a closed interval with a tight constant ( $0.878$ against the true minimum $\approx0.87856$ ), so crude estimates do not suffice near the minimizer $t\approx-0.689$ .

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin n → ℝ. $\mathbb S^n_+$ is Matrix.PosSemidef, which includes symmetry, and $\langle M,X\rangle$ is trace (Mᵀ * X).
$\mathcal N(0,\Sigma)$ is Mathlib's ProbabilityTheory.multivariateGaussian 0 Σ on EuclideanSpace ℝ (Fin n), defined for every positive semidefinite $\Sigma$ , singular ones included. Expectations are Bochner integrals against it, and each theorem also asserts integrability of its (bounded) integrand.
The sign is $\{-1,1\}$ -valued: $\operatorname{sign}(r)=1$ for $r\ge0$ and $-1$ for $r<0$ . Mathlib's Real.sign would give $\operatorname{sign}(0)=0$ , which takes $\zeta$ out of $\{-1,1\}^n$ ; the two agree almost surely because $\Sigma_{i,i}=1$ .
The maximum over the hypercube is a finite maximum (Finset.sup') over the $2^n$ Boolean vectors read as $\pm1$ vectors, so it is never a junk value. "The solution" of the relaxation means any maximizer, and maximizers exist since the feasible set is compact and contains the identity.
Standing hypotheses: in Theorem 6.11, $A$ symmetric with non-negative entries (the book's MAXCUT setting); in Lemma 6.12, $\Sigma$ positive semidefinite (implicit in " $\xi\sim\mathcal N(0,\Sigma)$ "); in Theorem 6.13, $B$ positive semidefinite. The identities of milestones 4 and 5 hold for every real matrix $A$ and are stated without hypotheses on $A$ .
Ruled out: tying $\xi$ 's law to anything other than $\Sigma$ , or dropping optimality of $\Sigma$ , would make the goal false or vacuous; here the law is exactly $\mathcal N(0,\Sigma)$ and $\Sigma$ is a maximizer.
Welcome contributions: Sheppard's formula in Mathlib's multivariate Gaussian language, a proof of (6.8), and the Schur product theorem ( $A,B\succeq0\Rightarrow A\circ B\succeq0$ ) used in Theorem 6.13.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2
M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6):1115–1145, 1995. doi:10.1145/227683.227684
Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optim. Methods Softw. 9(1–3):141–160, 1998. doi:10.1080/10556789808805690
S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37(1):319–357, 2007. doi:10.1137/S0097539705447372
W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation, Phil. Trans. R. Soc. A 192:101–167, 1899. doi:10.1098/rsta.1899.0003

6 thms1 active userReviewed

Completed

Convex Optimization Machine Learning Probability·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XVI: Random Coordinate Descent RCD(γ) on a Strongly Convex Coordinate-Smooth Function Has Rate (1 − 1/κ_γ)^tTextbook

Motivation

When a problem has millions of variables, even one full gradient can be too expensive to compute, while a single partial derivative $\partial f/\partial x_i$ is often cheap: in regularized regression, support vector machines and many structured problems, updating one coordinate costs a small fraction of a full gradient step. Coordinate descent methods exploit this by moving along one coordinate at a time. They are among the oldest optimization schemes and were for a long time analysed only for cyclic orders and only asymptotically.

Nesterov (2012) showed that choosing the coordinate at random, with probabilities depending on the coordinate-wise smoothness constants, gives global, non-asymptotic rates that can beat full gradient descent in total work. This mission formalizes that analysis as presented in §6.4 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 338–342, and in particular its linear rate for strongly convex functions (Theorem 6.8).

Setting

Let $f:\mathbb R^n\to\mathbb R$ be differentiable, write $\nabla_i f(x)=\frac{\partial f}{\partial x_i}(x)$ and let $e_i$ be the $i$ -th standard basis vector. The function is directionally smooth with constants $\beta_1,\dots,\beta_n>0$ if

|\nabla_i f(x+ue_i)-\nabla_i f(x)|\le\beta_i|u|\qquad\text{for all } i\in[n],\ x\in\mathbb R^n,\ u\in\mathbb R,

equivalently, each one-variable restriction $u\mapsto f(x+ue_i)$ is $\beta_i$ -smooth.

For a real exponent $c$ , the weighted norms are

\|x\|_{[c]}=\sqrt{\textstyle\sum_{i}\beta_i^{c}x_i^2},\qquad \|x\|^*_{[c]}=\sqrt{\textstyle\sum_{i}\beta_i^{-c}x_i^2}.

For $\alpha>0$ , $f$ is $\alpha$ -strongly convex w.r.t. a norm $\|\cdot\|$ if $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac{\alpha}{2}\|x-y\|^2$ for all $x,y$ . The point $x^*$ is a minimizer of $f$ .

For $\gamma\ge0$ , RCD( $\gamma$ ) starts at $x_1\in\mathbb R^n$ and iterates

x_{s+1}=x_s-\frac{1}{\beta_{i_s}}\nabla_{i_s}f(x_s)\,e_{i_s},

where $i_1,i_2,\dots$ are drawn independently from $p_\gamma(i)=\beta_i^\gamma/\sum_{j}\beta_j^\gamma$ . The case $\gamma=0$ is uniform sampling; $\gamma=1$ samples proportionally to $\beta_i$ .

Formalization targets

Goal: Theorem 6.8 (p. 341)

Let $\gamma\ge0$ , let $f$ be $\alpha$ -strongly convex w.r.t. $\|\cdot\|_{[1-\gamma]}$ and directionally smooth with constants $\beta_i$ , and let $\kappa_\gamma=\sum_i\beta_i^\gamma/\alpha$ . Then for every $t\ge0$

\mathbb E f(x_{t+1})-f(x^*)\le\Big(1-\frac{1}{\kappa_\gamma}\Big)^t\big(f(x_1)-f(x^*)\big).

Milestones

Lemma 6.9 (p. 341): for $f$ $\alpha$ -strongly convex w.r.t. any norm, $f(x)-f(x^*)\le\frac{1}{2\alpha}\|\nabla f(x)\|_*^2$ .
One coordinate step (p. 340): $f\big(x-\frac{1}{\beta_i}\nabla_i f(x)e_i\big)-f(x)\le-\frac{1}{2\beta_i}(\nabla_i f(x))^2$ .
Expected decrease (p. 340): $\mathbb E_{i_s}f(x_{s+1})-f(x_s)\le-\frac{1}{2\sum_i\beta_i^\gamma}\big(\|\nabla f(x_s)\|^*_{[1-\gamma]}\big)^2$ .
Lemma 6.9 in the weighted norm (p. 342): $\big(\|\nabla f(x)\|^*_{[1-\gamma]}\big)^2\ge2\alpha(f(x)-f(x^*))$ .
Contraction (pp. 341–342): one step multiplies the expected gap by at most $1-1/\kappa_\gamma$ .

Companion: Theorem 6.7 (pp. 339–340)

For $f$ convex and directionally smooth, and $t\ge2$ ,

\mathbb E f(x_t)-f(x^*)\le\frac{2R_{1-\gamma}^2(x_1)\sum_i\beta_i^\gamma}{t-1},\qquad R_{1-\gamma}(x_1)=\sup_{f(x)\le f(x_1)}\|x-x^*\|_{[1-\gamma]}.

Significance

Theorem 6.8 says random coordinate descent converges linearly, with a rate governed by $\sum_i\beta_i^\gamma/\alpha$ instead of the global smoothness constant. For $\gamma=1$ , directional smoothness implies $f$ is $\beta$ -smooth with $\beta\le\sum_i\beta_i$ , so for functions whose global smoothness constant is of the order of $\sum_i\beta_i$ , RCD(1) attains the accuracy of gradient descent after the same number of iterations (book, p. 340, comparing Theorem 6.7 with Theorem 3.3), while each iteration touches a single coordinate. The same per-step inequalities underlie later accelerated and parallel coordinate methods.

These results are proved in the literature (Nesterov 2012; Bubeck 2015). Their contribution here is a machine-checked version. As far as a search of the Prove2Me catalogue shows, no coordinate descent rate of this kind has been formalized there; a Euclidean-norm special case of Lemma 6.9 exists on the platform as a separate result, but not the arbitrary-norm lemma or the weighted-norm instance used here.

Difficulty

The main obstacle is bookkeeping of the randomness: the per-step inequality holds for each fixed iterate, while the theorem is about the expectation over the whole sequence of draws $i_1,\dots,i_t$ , so the pointwise contraction has to be passed through the tower of conditional expectations. In the strongly convex case this is linear and exact; for Theorem 6.7 the recursion on $\delta_s=\mathbb Ef(x_s)-f(x^*)$ is quadratic, and since $\delta_s$ is an expectation while the gradient norm at $x_s$ is random, the pointwise inequality does not transfer to $\delta_s$ verbatim. A second point is geometric: strong convexity, the dual norm and the sampling distribution must use matching weights ( $\beta_i^{1-\gamma}$ against $\beta_i^{\gamma}$ ), and a mismatch silently changes the constant.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The gradient is an explicit map $g$ with HasGradientAt f (g x) x, so $\nabla_i f(x)=g(x)_i$ . Lemma 6.9 is stated for a finite-dimensional real normed space with the Fréchet derivative and the operator norm as the dual norm.
Powers $\beta_i^c$ are real powers. The theorems assume $n\ge1$ , $\alpha>0$ and $\beta_i>0$ , which the book uses implicitly; $\gamma\ge0$ is the book's.
RCD(γ) is a deterministic function of the drawn coordinates, and the expectation over $t$ independent draws from $p_\gamma$ is the finite sum $\sum_{(i_1,\dots,i_t)\in[n]^t}\prod_s p_\gamma(i_s)\,F(i_1,\dots,i_t)$ . No measure theory or integrability conventions are involved.
The minimizer $x^*$ is assumed to exist, as the book does throughout; its uniqueness, which the book assumes "only for sake of notation", is not used.
In Theorem 6.7 the supremum $R_{1-\gamma}(x_1)$ is passed as any real upper bound $R$ on the sublevel set, which is equivalent when the supremum is finite and avoids Lean's value $0$ for an unbounded supremum.
Directional smoothness is required at every $x$ and $u$ , and $p_\gamma$ is fixed by the $\beta_i$ ; neither is weakened to hold only along the iterates, which would change the theorem.

A complete development needs the one-dimensional descent lemma (3.5), weighted Cauchy–Schwarz for the dual pair $\|\cdot\|_{[c]},\|\cdot\|^*_{[c]}$ , and a decomposition of the finite expectation over $[n]^{t+1}$ into the last draw and the first $t$ . The weighted-norm and finite-expectation lemmas are reusable for other randomized coordinate and sampling methods. Proofs of the milestones and of either theorem are welcome.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §6.4, pp. 338–342.
Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2):341–362, 2012. doi:10.1137/100802001
P. Richtárik and M. Takáč, Parallel coordinate descent methods for big data optimization, Mathematical Programming 156:433–484, 2016. arXiv:1212.0873

7 thms1 active userReviewed

Convex Optimization Machine Learning Probability·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XIV: Stochastic Mirror Descent on a β-Smooth Function with Noise σ Has Rate Rσ√(2/t) + βR²/tTextbook

Motivation

Many optimization problems in statistics and machine learning ask to minimize an expected loss $f(x)=\mathbb E_\xi\,\ell(x,\xi)$ , or an average $f(x)=\frac1m\sum_{i=1}^m f_i(x)$ over a large data set. Exact gradients of such an $f$ are unavailable or too expensive, but unbiased random estimates are cheap: the gradient of the loss at one sample, or of one randomly chosen summand. The observation that first-order methods still make progress when the gradients are only correct on average goes back to Robbins and Monro (1951) and underlies stochastic gradient descent.

Chapter 6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (2015), studies this setting through stochastic mirror descent (S-MD). Its Section 6.1 shows that in the non-smooth case a noisy oracle costs nothing in rate. Section 6.2 asks what smoothness buys: for a general stochastic oracle it cannot buy acceleration, but Theorem 6.3, whose proof the book takes from Dekel, Gilad-Bachrach, Shamir and Xiao (2012), shows that the rate splits into a noise term of order $1/\sqrt t$ and a smoothness term of order $1/t$ . The book uses it to justify mini-batch SGD. This mission is the fourteenth of a series that formalizes the section capstones of the book.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ . Gradients are linear forms $g$ on $E$ , the value of $g$ at $v$ is written $g^\top v$ , and the dual norm is $\|g\|_*=\sup_{\|v\|\le1}g^\top v$ . Let $\mathcal X\subseteq E$ be compact and convex.

A mirror map is a function $\Phi$ on an open convex set $\mathcal D$ with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\ne\emptyset$ . It is strictly convex and differentiable on $\mathcal D$ , its gradient $\nabla\Phi$ takes every value, and $\|\nabla\Phi(x)\|_*\to\infty$ as $x$ approaches the boundary of $\mathcal D$ . Its Bregman divergence is $D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y)$ . The map is 1-strongly convex on $\mathcal X\cap\mathcal D$ if $D_\Phi(y,x)\ge\frac12\|x-y\|^2$ there. A function $f$ is $\beta$ -smooth on $\mathcal X$ if $\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|$ for $x,y\in\mathcal X$ .

A stochastic oracle returns, at a query point $x$ , a random linear form $\tilde g(x)$ . When the query point is itself random, the book requires the conditional expectation given the query point, $\mathbb E(\tilde g(x)\mid x)$ , to be a subgradient of $f$ at $x$ . In the smooth case it requires $\mathbb E(\tilde g(x)\mid x)=\nabla f(x)$ together with the variance bound $\mathbb E(\|\tilde g(x)-\nabla f(x)\|_*^2\mid x)\le\sigma^2$ .

S-MD with step $\gamma$ starts at $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ and, writing $\tilde g_s=\tilde g(x_s)$ , iterates

x_{s+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}\ \gamma\,\tilde g_s^\top x+D_\Phi(x,x_s).

Let $R^2\ge\sup_{x\in\mathcal X\cap\mathcal D}\Phi(x)-\Phi(x_1)$ , and let $x^*$ minimize $f$ on $\mathcal X$ .

Formalization targets

Goal: Theorem 6.3

Let $f$ be convex and $\beta$ -smooth, and let the oracle have variance at most $\sigma^2$ . Then for every $t\ge1$ , S-MD with step $1/(\beta+1/\eta)$ and $\eta=\frac R\sigma\sqrt{2/t}$ satisfies

\mathbb E\,f\Big(\frac1t\sum_{s=1}^t x_{s+1}\Big)-f(x^*)\le R\sigma\sqrt{\frac2t}+\frac{\beta R^2}{t}.

Milestones (the proof's four displays)

For points $x_s,x_{s+1}\in\mathcal X\cap\mathcal D$ and $\eta>0$ , the smoothness step is

f(x_{s+1})-f(x_s)\le\tilde g_s^\top(x_{s+1}-x_s)+\tfrac\eta2\|\nabla f(x_s)-\tilde g_s\|_*^2+(\beta+1/\eta)D_\Phi(x_{s+1},x_s).

If $x_{s+1}$ is the S-MD step, the mirror step is

\tfrac{1}{\beta+1/\eta}\tilde g_s^\top(x_{s+1}-x^*)\le D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})-D_\Phi(x_{s+1},x_s).

Combining the two gives a pathwise bound on $f(x_{s+1})$ with the cross term $(\tilde g_s-\nabla f(x_s))^\top(x^*-x_s)$ . Taking expectations gives the expected one-step bound

\mathbb Ef(x_{s+1})-f(x^*)\le(\beta+1/\eta)\,\mathbb E\big(D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})\big)+\frac{\eta\sigma^2}{2}.

Companion: Theorem 6.1 and (4.10)

For a convex $f$ with $\mathbb E(\|\tilde g(x)\|_*^2\mid x)\le B^2$ , S-MD with $\eta=\frac RB\sqrt{2/t}$ satisfies

\mathbb E\,f\Big(\frac1t\sum_{s=1}^tx_s\Big)-\min_{\mathcal X}f\le RB\sqrt{2/t}.

This rests on the deterministic regret bound (4.10) of mirror descent along arbitrary vectors $g_s$ :

\sum_{s\le t}g_s^\top(x_s-x)\le\frac{R^2}{\eta}+\frac{\eta}{2\rho}\sum_{s\le t}\|g_s\|_*^2.

Significance

Theorem 6.3 says exactly how much smoothness helps under noise. As $\sigma\to0$ it recovers the $\beta R^2/t$ rate of deterministic smooth optimization. For large $t$ the noise term $R\sigma\sqrt{2/t}$ dominates; the book notes, citing Tsybakov (2003), that smoothness brings no acceleration for a general stochastic oracle. Averaging $m$ independent oracle answers divides the variance by $m$ , so the theorem quantifies the benefit of mini-batches: the noise term shrinks by $\sqrt m$ while the smoothness term is unchanged. Theorem 6.1 is the matching non-smooth statement and the template for stochastic subgradient methods in any norm.

These are classical, proved results. None of them is known to be formalized in Lean, and the platform has no stochastic mirror descent statement. Its stochastic gradient items cover the Euclidean strongly convex case and the non-convex gradient-norm case. This mission adds a reusable stochastic-oracle layer in an arbitrary norm, with conditional expectations given random query points, on top of the mirror-map layer of Chapter 4.

Difficulty

The deterministic steps are short manipulations of Bregman divergences. The difficulty is in the passage to expectations. The query point $x_s$ is random, so unbiasedness enters only through the conditional expectation given $x_s$ . Making the cross term vanish requires pulling the $\sigma(x_s)$ -measurable vector $x^*-x_s$ out of a conditional expectation of a dual-valued random variable. Every expectation also has to exist. When $\nabla\Phi$ blows up at the boundary of $\mathcal D$ , the Bregman terms $D_\Phi(x^*,x_s)$ are not bounded a priori, and their integrability has to be derived from the recursion. A further obstacle is that the minimizer $x^*$ may lie on the boundary of $\mathcal D$ , where $\Phi$ is not part of the book's data. Treating $\mathbb E$ informally, or assuming $x^*\in\mathcal D$ , skips exactly these points.

Formalization scope

Spaces and gradients. $E$ is a finite-dimensional real normed space. Gradients are explicit maps Φ' f' : E → (E →L[ℝ] ℝ), $g^\top v$ is g v, and $\|\cdot\|_*$ is the operator norm. $\beta$ -smoothness is stated with derivatives relative to $\mathcal X$ . $\Phi$ is a total function, constrained only by the mirror-map axioms on $\mathcal D$ .
Runs and oracle. S-MD is a run predicate. For every outcome, $x_1$ minimizes $\Phi$ on $\mathcal X\cap\mathcal D$ , and $x_{s+1}$ is some minimizer of the step objective. The oracle is a predicate on the random sequences $(x_s,\tilde g_s)$ : each $x_s$ is measurable, and the conditional expectations are taken given $\sigma(x_s)$ . Every conditioned quantity is integrable.
Conclusions. Every bound on an expectation also asserts integrability. Without it, the Lean integral of a non-integrable function is $0$ and the bound could hold trivially.
Standing assumptions. The book's $R^2=\sup(\Phi-\Phi(x_1))$ is replaced by any upper bound $R^2$ . The minimizer $x^*\in\mathcal X$ exists (p. 242). $\mathcal X$ is compact and convex (Chapter 4), and convex functions are closed (p. 236).
Positivity side conditions. $R,\sigma,B>0$ and $t\ge1$ make the step sizes and bounds defined, and $\beta\ge0$ .

A variance hypothesis stated only at deterministic points would not control the random iterates, and is not used. Run predicates that let $x_{s+1}$ be an arbitrary point of $\mathcal X\cap\mathcal D$ would make the theorems false, and are not used either.

A complete development needs: first-order optimality over a convex set, the three-point identity of Bregman divergences, the descent lemma in an arbitrary norm, and continuity of the gradient of a differentiable convex function. On the probability side it needs pull-out and conditional Jensen properties for dual-valued conditional expectations. The probability layer is reusable for every stochastic first-order method in the book, including SVRG and random coordinate descent. Proofs of the milestones are welcome, and so are general lemmas about conditional expectations of continuous-linear-map-valued random variables.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, https://arxiv.org/abs/1405.4980 (Chapter 6, pp. 329–333; Chapter 4, pp. 297–307).
O. Dekel, R. Gilad-Bachrach, O. Shamir, L. Xiao, Optimal distributed online prediction using mini-batches, Journal of Machine Learning Research 13:165–202, 2012. https://jmlr.org/papers/v13/dekel12a.html
H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277

6 thms1 active userReviewed

Convex Optimization Numerical Analysis·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XIII: Newton's Method Converges Quadratically, ‖x_{k+1} − x‖ ≤ (M/μ)‖x_k − x‖², from ‖x₀ − x*‖ ≤ μ/(2M)Textbook

Motivation

Newton's method is the basic second-order method of continuous optimization: at the current point it replaces the objective by its second-order Taylor model and jumps to the stationary point of that model. Its defining property is speed near a nondegenerate minimum, where the error is squared at every step, so that the number of correct digits roughly doubles per iteration. This local behaviour is what makes Newton's method the inner engine of interior point methods, the polynomial-time algorithms for linear, conic and general convex programming (Nesterov and Nemirovski, 1994). In S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2), §5.3.2 recalls the traditional local analysis of Newton's method, Theorem 5.3, before turning to the affine-invariant self-concordance analysis used for interior point methods. This mission formalizes that theorem and the four steps of its proof.

Setting

Let $\mathbb R^n$ carry the Euclidean norm $\|\cdot\|$ , and write $\|A\|$ for the operator norm of a linear map $A:\mathbb R^n\to\mathbb R^n$ , so that $\|Ax\|\le\|A\|\,\|x\|$ . Let $f:\mathbb R^n\to\mathbb R$ be a $C^2$ function, with gradient $\nabla f(x)\in\mathbb R^n$ and Hessian $\nabla^2 f(x)$ , a linear map $\mathbb R^n\to\mathbb R^n$ (the derivative of the gradient map). For a real number $c$ , $A\succeq cI_n$ means $\langle Av,v\rangle\ge c\|v\|^2$ for all $v\in\mathbb R^n$ .

The Hessian is $M$ -Lipschitz if $\|\nabla^2 f(x)-\nabla^2 f(y)\|\le M\|x-y\|$ for all $x,y\in\mathbb R^n$ .

Newton's method starts at $x_0\in\mathbb R^n$ and iterates, for $k\ge0$ ,

x_{k+1}=x_k-[\nabla^2 f(x_k)]^{-1}\nabla f(x_k).

A point $x^*$ is a local minimum of $f$ if $f(x^*)\le f(x)$ for all $x$ in a neighbourhood of $x^*$ ; it has strictly positive Hessian if $\nabla^2 f(x^*)\succeq\mu I_n$ for some $\mu>0$ .

Formalization targets

Goal: Theorem 5.3 (p. 320)

Assume the Hessian of $f$ is $M$ -Lipschitz, $M>0$ , and $x^*$ is a local minimum with $\nabla^2 f(x^*)\succeq\mu I_n$ , $\mu>0$ . If $\|x_0-x^*\|\le\mu/(2M)$ , then Newton's method from $x_0$ is well defined (every Hessian along the iterates is invertible, so the sequence exists and is unique) and

\|x_{k+1}-x^*\|\le\frac M\mu\,\|x_k-x^*\|^2\quad(k\ge0),\qquad x_k\to x^*.

Milestones (p. 321, the steps of the proof)

The integral formula $\int_0^1\nabla^2 f(x+sh)\,h\,ds=\nabla f(x+h)-\nabla f(x)$ .
The error representation of one Newton step, $x_{k+1}-x^*=[\nabla^2 f(x_k)]^{-1}\int_0^1[\nabla^2 f(x_k)-\nabla^2 f(x^*+s(x_k-x^*))](x_k-x^*)\,ds$ .
The Lipschitz bound $\int_0^1\|\nabla^2 f(x_k)-\nabla^2 f(x^*+s(x_k-x^*))\|\,ds\le\frac M2\|x_k-x^*\|$ .
The Hessian lower bound $\nabla^2 f(x_k)\succeq(\mu-M\|x_k-x^*\|)I_n\succeq\frac\mu2I_n$ when $\|x_k-x^*\|\le\mu/(2M)$ .

Significance

The theorem gives a quantitative basin of quadratic convergence: an explicit radius $\mu/(2M)$ , depending only on the curvature at the minimum and the Lipschitz constant of the Hessian, inside which Newton's method needs only $O(\log\log(1/\varepsilon))$ iterations to reach accuracy $\varepsilon$ . It is the classical statement whose shortcomings (dependence on a choice of norm, constants that change under linear changes of variables) motivate the self-concordance theory of the following subsections, and it is the local convergence result invoked whenever a damped or globalized Newton scheme is shown to enter its quadratic phase.

On the formal side, Mathlib has the calculus this needs (Fréchet derivatives, interval integrals of vector-valued maps, operator norms) but no convergence theorem for multivariate Newton's method for minimization. A formal proof produces reusable pieces: the integral form of the mean value theorem for gradients, the stability of a positive-definite lower bound under Lipschitz perturbations, and an inverse-operator norm bound from a quadratic-form lower bound. The result itself is classical and fully proved in the literature; what is open here is its machine-checked proof in this form.

Difficulty

The individual inequalities are short, but the argument is an induction in which well-definedness and the rate are proved together: the Hessian at $x_k$ is invertible only because $x_k$ is still in the ball of radius $\mu/(2M)$ , and $x_{k+1}$ stays in that ball only because of the rate. A proof that first assumes the sequence exists and then bounds it is circular. The proof also passes between two kinds of control on the Hessian, a lower bound on its quadratic form and an operator-norm bound on its inverse, and the second is only meaningful once invertibility is established. Finally, the integral manipulations need integrability of the maps $s\mapsto\nabla^2 f(x^*+s(x_k-x^*))(x_k-x^*)$ , which comes from the continuity of the Hessian.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The gradient and Hessian are explicit maps $g:\mathbb R^n\to\mathbb R^n$ and $H:\mathbb R^n\to(\mathbb R^n\to_L\mathbb R^n)$ with ContDiff ℝ 2 f, HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every point; the norm on $H(x)$ is Mathlib's operator norm, as on the page. $A\succeq cI_n$ is the quadratic-form inequality. A Newton run is a sequence $x:\mathbb N\to\mathbb R^n$ indexed from $0$ satisfying the linear system $\nabla^2 f(x_k)(x_k-x_{k+1})=\nabla f(x_k)$ ; no inverse of a possibly singular operator appears in any hypothesis, and "well defined" is a conclusion: a unique run exists from $x_0$ and every Hessian along it is bijective. The rate and $x_k\to x^*$ are asserted for every run. The error representation is stated with both sides multiplied by $\nabla^2 f(x_k)$ , which is equivalent to the printed form once the Hessian is invertible. Milestones 3 and 4 use only the Lipschitz property and are stated for any Lipschitz map $H$ .

Added hypothesis: $M>0$ (the radius $\mu/(2M)$ divides by $M$ ; with $M=0$ , Lean's convention $\mu/0=0$ would collapse the hypothesis to $x_0=x^*$ ). Convexity of $f$ is not assumed, as on the page; $x^*$ is a local minimum and $\nabla f(x^*)=0$ is derived, not assumed. Encoding the Newton step with Lean's inverse (which returns $0$ on singular maps), or replacing $\nabla^2 f(x^*)\succeq\mu I_n$ by mere invertibility, would change the theorem and is ruled out.

A complete development needs the fundamental theorem of calculus for $C^1$ vector-valued maps along segments, Hessian-based quadratic-form estimates, and operator-norm bounds for inverses; all are reusable for the analysis of damped Newton, cubic regularization and interior point methods. Proofs of the milestones independently of the goal are welcome.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §5.3.2, Theorem 5.3, pp. 320–321.
Yu. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. doi:10.1137/1.9781611970791
Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004, Theorem 1.2.5. doi:10.1007/978-1-4419-8853-9

6 thms1 active userReviewed

Completed

Convex Optimization Machine Learning·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity X: Nesterov's Accelerated Gradient Descent on a β-Smooth α-Strongly Convex Function Has Rate ((α + β)/2)‖x₁ − x*‖² exp(−(t − 1)/√κ)Textbook

Why accelerated rates matter

First-order methods, which query only function values and gradients, are the workhorse of large-scale optimization in machine learning, signal processing and operations research, because each step costs little more than one gradient evaluation. For a function that is both strongly convex and smooth, plain gradient descent converges geometrically, but the number of steps needed to reach accuracy $\varepsilon$ scales with the condition number $\kappa$ of the problem. In 1983 Nesterov showed that a gradient method with a carefully chosen momentum term needs a number of steps proportional to $\sqrt\kappa$ instead, and that this is optimal for black-box first-order methods. On ill-conditioned problems, where $\kappa$ is in the thousands or millions, the difference between $\kappa$ and $\sqrt\kappa$ is the difference between practical and impractical.

This mission is the tenth of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2). It covers §3.7.1, the smooth and strongly convex case of Nesterov's accelerated gradient descent, and its main result, Theorem 3.18.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$ . Let $f:\mathbb R^n\to\mathbb R$ be differentiable with gradient $\nabla f$ .

$f$ is $\beta$ -smooth if its gradient is $\beta$ -Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|$ for all $x,y$ .
$f$ is $\alpha$ -strongly convex ( $\alpha>0$ ) if for all $x,y$

f(y)\ge f(x)+\nabla f(x)^\top(y-x)+\frac\alpha2\|y-x\|^2 .

The condition number is $\kappa=\beta/\alpha$ ; for $n\ge1$ one always has $\kappa\ge1$ .
$x^*$ denotes a minimizer of $f$ on $\mathbb R^n$ .

Nesterov's accelerated gradient descent starts at an arbitrary point $x_1=y_1$ and iterates, for $t\ge1$ ,

y_{t+1}=x_t-\frac1\beta\nabla f(x_t),\qquad x_{t+1}=\Big(1+\frac{\sqrt\kappa-1}{\sqrt\kappa+1}\Big)y_{t+1}-\frac{\sqrt\kappa-1}{\sqrt\kappa+1}\,y_t .

The point $y_{t+1}$ is a gradient step from $x_t$ , and $x_{t+1}$ moves beyond $y_{t+1}$ in the direction $y_{t+1}-y_t$ by the fixed momentum factor $(\sqrt\kappa-1)/(\sqrt\kappa+1)$ .

The analysis in the book uses auxiliary quadratic functions $\Phi_s$ (an estimate sequence), defined from the points $x_s$ by

\Phi_1(x)=f(x_1)+\frac\alpha2\|x-x_1\|^2,\qquad \Phi_{s+1}(x)=\Big(1-\frac1{\sqrt\kappa}\Big)\Phi_s(x)+\frac1{\sqrt\kappa}\Big(f(x_s)+\nabla f(x_s)^\top(x-x_s)+\frac\alpha2\|x-x_s\|^2\Big),

together with their centres $v_s$ (with $v_1=x_1$ and the recursion (3.21) of the book) and their minimum values $\Phi^*_s$ .

Formalization targets

Goal: Theorem 3.18

For every run of the method and every $t\ge1$ ,

f(y_t)-f(x^*)\le\frac{\alpha+\beta}2\,\|x_1-x^*\|^2\exp\Big(-\frac{t-1}{\sqrt\kappa}\Big).

Milestones, from the book's proof

(3.18): $\Phi_{s+1}(x)\le f(x)+(1-1/\sqrt\kappa)^s(\Phi_1(x)-f(x))$ for all $x$ .
(3.19): $f(y_s)\le\min_{x\in\mathbb R^n}\Phi_s(x)$ .
The geometric rate: $f(y_t)-f(x^*)\le\frac{\alpha+\beta}2\|x_1-x^*\|^2(1-1/\sqrt\kappa)^{t-1}$ .
The form $\Phi_s(x)=\Phi^*_s+\frac\alpha2\|x-v_s\|^2$ with $v_s$ given by (3.21).
The identity (3.22) for $\Phi^*_{s+1}$ .
The inequality (3.20), the inductive step of (3.19).
The coupling $v_s-x_s=\sqrt\kappa\,(x_s-y_s)$ .

The geometric form in milestone 3 is slightly stronger than the goal, which follows from $1-u\le e^{-u}$ .

Significance

Theorem 3.18 gives $\varepsilon$ -accuracy after $O(\sqrt\kappa\log(1/\varepsilon))$ gradient evaluations. Projected gradient descent with step $1/\beta$ on the same class contracts only at the rate $\exp(-t/\kappa)$ (Theorem 3.10 of the book). The lower bound of Theorem 3.15 shows that no black-box first-order method can do better than $((\sqrt\kappa-1)/(\sqrt\kappa+1))^{2(t-1)}$ , so the accelerated rate is optimal up to constants. The estimate-sequence argument is the template for many later accelerated methods: proximal, stochastic and variance-reduced variants such as Katyusha, and accelerated coordinate descent.

The result is classical and fully proved on paper. No machine-checked proof of the accelerated rate for strongly convex smooth functions is known to exist in Lean's Mathlib. This mission produces one, with the estimate sequence $\Phi_s$ , its centres and its minimum values as reusable objects, and with every algebraic identity of the book's proof stated separately.

Difficulty

The algorithm is two lines, but its analysis is not a one-step contraction: neither $\|x_t-x^*\|$ nor $f(y_t)-f(x^*)$ decreases by the factor $1-1/\sqrt\kappa$ at every step. A Lyapunov argument for gradient descent, applied directly to $y_t$ , gives only the rate $1-1/\kappa$ . The book obtains the rate through the auxiliary functions $\Phi_s$ . The inequality (3.18) is easy, but (3.19), that the minimum of $\Phi_s$ never drops below $f(y_s)$ , depends on the exact choice of the momentum factor. It holds only through the identity $v_s-x_s=\sqrt\kappa(x_s-y_s)$ , which ties the centre of $\Phi_s$ to the iterates. Formally, the obstacles are the bookkeeping of the recursive quadratics on $\mathbb R^n$ and the algebra in $\sqrt\kappa$ , $1/\sqrt\kappa$ and $1/(\alpha\sqrt\kappa)=\sqrt\kappa/\beta$ .

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The gradient is an explicit map g with HasGradientAt f (g x) x at every point, which is part of the smoothness predicate IsBetaSmooth f g β. Strong convexity is the published definition OnlineConvexOpt.ConvexBasics.StronglyConvexOn Set.univ f g α, which is the book's (3.13).
A run of the method is a predicate IsNesterovSCRun g α β x y on two sequences indexed from $1$ , with $x_1=y_1$ arbitrary. Every theorem holds for every run, that is, every starting point.
$\kappa$ is kappa α β = β / α. All theorems assume $\alpha>0$ and $\beta>0$ . The second is implied by the other hypotheses for $n\ge1$ ; no hypothesis $\alpha\le\beta$ is added.
The existence of a minimizer $x^*$ is the book's standing assumption, written as a hypothesis.
$\Phi_s$ , $v_s$ and $\Phi^*_s=\Phi_s(v_s)$ are explicit recursive definitions. The book's $\Phi^*_s=\min\Phi_s$ is recovered by milestone 4, and no real infimum is used. The minimum in (3.19) is stated as $f(y_s)\le\Phi_s(x)$ for every $x$ .
The identities of milestones 4, 5 and 7 are algebraic and are stated without convexity or smoothness, for arbitrary sequences or runs.
Ruled out as trivializing: a run predicate that drops $x_1=y_1$ breaks (3.19) at $s=1$ and is not used. A minimum value $\Phi^*_s$ defined through (3.22) would make that identity a tautology, so $\Phi^*_s$ is defined as a value of $\Phi_s$ .
The definitions are local to the namespace ConvexOptAlg.NesterovStrong. β-smoothness duplicates the predicate of other missions of the series and will be merged afterwards. Contributions welcome: proofs of the milestones, and general lemmas on quadratics $z\mapsto c+\frac\alpha2\|z-v\|^2$ that the algebraic milestones need.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §3.7.1, Theorem 3.18, pp. 290–293.
Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27:372–376, 1983.
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9

10 thms1 active userReviewed

Completed

Convex Optimization Machine Learning·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity VIII: No Black-Box Method Beats 3β‖x₁ − x*‖²/(32(t + 1)²) on β-Smooth Convex FunctionsTextbook

Why lower bounds for first-order methods

Upper bounds for an optimization method say how fast it converges; oracle complexity lower bounds say how fast any method of a given kind can possibly converge. Chapter 3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015, arXiv:1405.4980) proves upper bounds for subgradient descent on Lipschitz functions and for gradient methods on smooth functions. Section 3.5 (Lower bounds, pp. 279–283) shows that these rates cannot be improved by more than a numerical constant, as long as the number of queries is smaller than the dimension. For smooth convex functions the matching lower bound is what identifies Nesterov's accelerated gradient descent, with its $1/t^2$ rate, as an optimal method.

Timeline. The lower bounds first appeared in A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization (Wiley, 1983). The presentation followed by the book, with an explicit tridiagonal quadratic as the hard instance and the "span of past gradients" restriction on the method, is that of Y. Nesterov, Introductory Lectures on Convex Optimization (Kluwer, 2004), §2.1.2. Nesterov's accelerated method (1983) attains the matching upper bound.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $x^\top y$ , coordinates $x(1),\dots,x(n)$ , canonical basis $e_1,\dots,e_n$ and balls $\mathrm B_2(R)=\{x:\|x\|\le R\}$ . A first-order oracle for $f$ answers a query $x$ with a subgradient $g\in\partial f(x)$ (the gradient when $f$ is differentiable). A black-box procedure maps the history $(x_1,g_1,\dots,x_t,g_t)$ to the next query $x_{t+1}$ . Section 3.5 restricts attention to procedures with

x_1=0,\qquad x_{t+1}\in\mathrm{Span}(g_1,\dots,g_t)\quad(t\ge0), \tag{3.15}

which covers gradient descent, its accelerated variants and conjugate gradient. A function is $\beta$ -smooth if its gradient is $\beta$ -Lipschitz; $L$ -Lipschitz on $\mathcal X$ if every subgradient at every point of $\mathcal X$ has norm at most $L$ ; $\alpha$ -strongly convex if $x\mapsto f(x)-\frac\alpha2\|x\|^2$ is convex.

The hard smooth instance uses, for $k\le n$ , the symmetric tridiagonal matrix $A_k$ with entries $2$ on the first $k$ diagonal positions and $-1$ on the neighbouring off-diagonal positions of the leading $k\times k$ block, zero elsewhere, and the quadratics

f_k(x)=\frac\beta8x^\top A_kx-\frac\beta4x^\top e_1 ,\qquad f_k^*=\inf_{x\in\mathbb R^n}f_k(x).

Formalization targets

Goal: Theorem 3.14 (p. 282)

For $1\le t\le\frac{n-1}2$ and $\beta>0$ there are a $\beta$ -smooth convex $f$ and a minimizer $x^*$ such that every procedure satisfying (3.15) has

\min_{1\le s\le t}f(x_s)-f(x^*)\ \ge\ \frac{3\beta}{32}\,\frac{\|x_1-x^*\|^2}{(t+1)^2}.

The constant $3/32$ is the book's.

Milestones (proof of Theorem 3.14, pp. 282–283)

$0\preceq A_k\preceq4I_n$ , through $x^\top A_kx=x(1)^2+x(k)^2+\sum_{i=1}^{k-1}(x(i)-x(i+1))^2$ .
For $f=f_{2t+1}$ and any procedure satisfying (3.15), $x_s\in\mathrm{Span}(e_1,\dots,e_{s-1})$ ; hence $f(x_s)=f_s(x_s)$ for $s\le t$ .
$x_k^*(i)=1-\frac i{k+1}$ solves $A_kx=e_1$ , minimizes $f_k$ , and $f_k^*=-\frac\beta8\bigl(1-\frac1{k+1}\bigr)$ .
$\|x_k^*\|^2\le\frac{k+1}3$ .
$f_t^*-f_{2t+1}^*=\frac\beta8\bigl(\frac1{t+1}-\frac1{2t+2}\bigr)\ge\frac{3\beta}{32}\frac{\|x^*_{2t+1}\|^2}{(t+1)^2}$ .

Companion: Theorem 3.13 (p. 280)

For $1\le t\le n$ and $L,R>0$ there are a convex $f$ , $L$ -Lipschitz on $\mathrm B_2(R)$ , and a first-order oracle for it such that every procedure satisfying (3.15) has $\min_{s\le t}f(x_s)-\min_{\mathrm B_2(R)}f\ge\frac{RL}{2(1+\sqrt t)}$ ; and for $\alpha>0$ there are an $\alpha$ -strongly convex $f$ , $L$ -Lipschitz on $\mathrm B_2(\frac L{2\alpha})$ , and an oracle with gap at least $\frac{L^2}{8\alpha t}$ over that ball.

Significance

The upper bounds of Chapter 3 (projected subgradient descent at rate $RL/\sqrt t$ , accelerated gradient descent at rate $\beta\|x_1-x^*\|^2/t^2$ ) become optimal statements only through these lower bounds: no method in the class (3.15) can be faster by more than a constant factor while $t$ is below the dimension. The restriction to $t\lesssim n$ is necessary, since Chapter 2's cutting-plane methods converge exponentially once the number of queries exceeds the dimension.

The results are classical and proved. Formalizing them yields machine-checked versions of the quadratic-form computation for the tridiagonal matrix, of the Krylov-type support argument under (3.15), and of the explicit minimizer of $f_k$ , each reusable in other lower-bound arguments (Theorem 3.15 in $\ell_2$ , lower bounds for strongly convex smooth functions, conjugate gradient analyses). The platform held no formal statement of these oracle lower bounds when this mission was drafted.

Difficulty

Each analytic step is elementary; the difficulty is in the bookkeeping. The span argument is an induction that must track, at each step, that the gradient of a tridiagonal quadratic at a vector supported on the first $s-1$ coordinates is supported on the first $s$ , and that the span hypothesis transfers this to the next query. The minimizer computation requires solving $A_kx=e_1$ on the leading block and showing that the coordinates beyond $k$ do not affect $f_k$ . A natural first attempt, choosing the hard function after seeing the procedure, proves a much weaker statement and is excluded by the quantifier order: the function is fixed first and must defeat every procedure.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Coordinates in Lean are 0-based; the definitions provide the book's 1-based coordinate coord x i and basis vector basisVec n i, and the matrix tridiag n k translates book index $i$ to Fin n index $i-1$ . The query sequence starts at index $1$ . The oracle is a fixed map $g$ , so (3.15) reads $x_{t+1}\in\mathrm{Span}(g(x_1),\dots,g(x_t))$ with $x_1=0$ . In Theorem 3.14 the oracle is the gradient, given as a map with HasGradientAt everywhere; $\beta$ -smoothness is the Lipschitz bound on that map. In Theorem 3.13 the oracle is part of what is constructed, because the book's proof uses a specific "resisting" subgradient selection and the claim fails for an arbitrary one.

Committed conventions, each stated in the item's Formalization Note: the minimum over $1\le s\le t$ is the bound for every such $s$ , and $t\ge1$ is required; $t\le(n-1)/2$ is $2t+1\le n$ ; the minimizer $x^*$ is existentially chosen together with $f$ (the hard function has many minimizers when $2t+1<n$ , and the bound is false for some of them); the minimum over a ball is the bound against every point of the ball; $f_k^*$ is the real infimum, asserted to be attained.

A formalization that let the function depend on the procedure, dropped $x_1=0$ , or took the span over gradients at points other than the queries would state a different and weaker theorem; the statements here keep $f$ (and the oracle) before the universally quantified procedure.

Infrastructure needed: quadratic forms of explicit matrices on EuclideanSpace, gradients of quadratics, and span/support lemmas for EuclideanSpace.single-type vectors. Contributions of proofs for any milestone, and of the strongly convex $\ell_2$ lower bound (Theorem 3.15, not included here), are welcome.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

8 thms1 active userReviewed

Operations Research Optimal Transport Probability·Captain: mikedeng1

Quantifying Distributional Model Risk via Optimal Transport 1: Strong Duality — the Worst-Case Expectation over an Optimal-Transport Ball on a Polish Space Equals Its Dual over (λ, φ)Research Paper

Motivation

A probability model $\mu$ for a random element $X$ is rarely known exactly. Distributionally robust performance analysis replaces the single expectation $E_\mu[f(X)]$ by its worst case over all models within a prescribed distance of $\mu$ . When the distance is an optimal-transport cost, the neighbourhood contains models whose support differs from that of $\mu$ . That matters in stochastic-process applications such as ruin probabilities for insurance reserves, where the natural alternatives (a compensated Poisson process against a Brownian motion) are mutually singular and likelihood-based divergences such as Kullback–Leibler are infinite.

Blanchet and Murthy (arXiv:1604.01446, Math. Oper. Res. 2019) prove that the worst-case expectation over an optimal-transport ball equals a one-dimensional dual problem. They assume only that the underlying space is Polish, the cost lower semicontinuous and the performance function upper semicontinuous and integrable.

Timeline. Esfahani and Kuhn (arXiv:1505.05116, 2015/2018) obtained a dual reformulation for Wasserstein balls around empirical measures on $\mathbb R^d$ . Gao and Kleywegt (arXiv:1604.02199, 2016) proved a general duality whose proof, as Blanchet and Murthy note, uses the local compactness of the space. Blanchet and Murthy (2016, v2 2017) removed local compactness and continuity of the cost. This covers path spaces such as $C[0,T]$ and $D[0,T]$ .

Setting

Let $S$ be a Polish space with Borel σ-algebra $\mathcal B(S)$ , and let $\mu$ be a probability measure on $S$ (the baseline model).

Cost (A1). $c : S\times S\to[0,\infty)$ is lower semicontinuous, and $c(x,y)=0$ if and only if $x=y$ .
Performance function (A2). $f : S\to\mathbb R$ is upper semicontinuous and $\mu$ -integrable.
Budget. $\delta>0$ .

The primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S\times S$ whose first marginal is $\mu$ and whose transport cost satisfies $\int c\,d\pi\le\delta$ . The second marginal of $\pi$ is the alternative model. The primal objective is $I(\pi)=\int f(y)\,d\pi(x,y)$ , and the primal value is

I=\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}.

The universal σ-algebra $\mathcal U(S)$ is the intersection of the completions of $\mathcal B(S)$ under all probability measures. Write $m\mathcal U(S;\bar{\mathbb R})$ for the $\mathcal U(S)$ -measurable functions $S\to[-\infty,\infty]$ . The dual feasible set $\Lambda_{c,f}$ consists of the pairs $(\lambda,\varphi)$ with $\lambda\ge0$ , $\varphi\in m\mathcal U(S;\bar{\mathbb R})$ and $\varphi(x)+\lambda c(x,y)\ge f(y)$ for all $x,y$ . The dual objective is $J(\lambda,\varphi)=\lambda\delta+\int\varphi\,d\mu$ , and the dual value is $J=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\}$ . Finally,

\varphi_\lambda(x)=\sup_{y\in S}\{f(y)-\lambda c(x,y)\}\in\mathbb R\cup\{\infty\}.

Formalization targets

Goal: Theorem 1

Under (A1) and (A2):

strong duality,

\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\};

there is $\lambda^*\ge0$ such that $(\lambda^*,\varphi_{\lambda^*})$ is a dual optimizer;
a feasible $\pi^*$ and a feasible $(\lambda^*,\varphi_{\lambda^*})$ with finite $J(\lambda^*,\varphi_{\lambda^*})$ are optimal with $I(\pi^*)=J(\lambda^*,\varphi_{\lambda^*})$ if and only if the complementary slackness conditions hold:

f(y)-\lambda^*c(x,y)=\varphi_{\lambda^*}(x)\ \ \pi^*\text{-a.s.},\qquad \lambda^*\Big(\int c\,d\pi^*-\delta\Big)=0.

The "if" direction is stated without the finiteness assumption.

Milestones

Weak duality $I\le J$ (5). Lemma 15. Strong duality with a primal optimizer on compact $S$ , first for continuous costs (Proposition 5), then for lower semicontinuous ones (Proposition 6). Universal measurability of $\varphi_\lambda$ (§4.2). Lemma 16. The restricted dual bound of Proposition 7. Lemma 8. The univariate formula (9):

I=\inf_{\lambda\ge0}\Big\{\lambda\delta+E_\mu\Big[\sup_{y\in S}\{f(y)-\lambda c(X,y)\}\Big]\Big\}.

Significance

The result. Formula (9) turns an infinite-dimensional optimization over probability measures into a one-dimensional convex minimization that involves only the baseline $\mu$ . A modeller can therefore evaluate it by sampling from $\mu$ . Theorem 1 is the input for the worst-case probability formula for closed sets (Theorem 3 of the paper) and for the existence of worst-case transport plans (Corollary 1). Its complementary slackness conditions describe the structure of every worst-case plan: mass is moved from $x$ to maximizers of $f(z)-\lambda^*c(x,z)$ , and the budget is exhausted whenever $\lambda^*>0$ .

Formalizing it. The result is proved on paper. To our knowledge it has no machine-checked proof. The only related statement on Prove2Me is a special case (empirical baseline, bounded continuous loss, power-of-norm cost on $\mathbb R^m$ ). A complete development would contain duality on compact spaces via Fenchel duality, the extension to σ-compact supports, and measurable-selection arguments for universally measurable functions. The measurable-selection part reuses Bertsekas–Shreve's analytic-set theory, which is already posed on the platform.

Difficulty

The obvious route copies Kantorovich duality. That route fails here because the feasible set $\Phi_{\mu,\delta}$ fixes only one marginal, so it is not tight on a non-compact space. Prokhorov compactness is available only on compact pieces $S_n\times S_n$ . The duality must then be transported to the whole space by a limiting argument that keeps control of the dual multipliers.

A second obstacle is measurability. For a merely lower semicontinuous cost on a non-locally-compact space, $\varphi_\lambda$ need not be Borel measurable, so the dual must range over universally measurable functions. Removing the restriction $y\in S_\pi$ from the envelope (Lemma 8) needs a measurable selection theorem. Arguments that assume closed balls are compact do not apply in the target spaces $C[0,T]$ and $D[0,T]$ .

Formalization scope

Space and costs. S carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]. The cost is a real-valued curried function c : S → S → ℝ; (A1) is the structure AssumptionA1; (A2) is UpperSemicontinuous f together with Integrable f μ; and 0 < δ is assumed throughout.
Extended reals. $I$ , $J$ , $I(\pi)$ , $J(\lambda,\varphi)$ and $\varphi_\lambda$ live in EReal. The integral of an extended-real function is $\int\varphi^+-\int\varphi^-$ with lower Lebesgue integrals, and $\infty-\infty$ evaluates to $-\infty$ . A coupling with $\int f^-\,d\pi=\infty$ therefore never raises $I$ , which is the paper's reading in footnote 2.
Measurability and integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. For such $\varphi$ the lower integral equals the integral against the completion of $\mu$ .
Variants. The dual feasible set takes a set $K$ : with $K=S$ it is (6b), and with $K=S_\pi$ it is (29).
Hidden hypothesis. The "only if" part of Theorem 1(b) carries the hypothesis $J(\lambda^*,\varphi_{\lambda^*})<\infty$ . Without it the equivalence fails when $I=J=\infty$ .
Ruled-out trivializations. A primal that fixes both marginals (or neither), a dual over Borel-measurable $\varphi$ , and a Bochner integral for $\int f\,d\pi$ (which is $0$ off $L^1(\pi)$ ) all describe different problems and are ruled out by the definitions.
Infrastructure and contributions. Needed: Fenchel duality on $C_b(S\times S)$ and its dual $M(S\times S)$ (Riesz–Markov–Kakutani), Prokhorov's theorem, Sion's minimax theorem, and Jankov–von Neumann selection. Several are on the platform or in Mathlib, and all are reusable beyond this mission. Proofs of the milestones in any order, and of the posed Bertsekas–Shreve tools, are welcome.

Selected references

J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2):565–600, 2019. arXiv:1604.01446v2, doi:10.1287/moor.2018.0936
R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, 2016. arXiv:1604.02199
P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171:115–166, 2018. arXiv:1505.05116
D. Bertsekas and S. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 7. MIT open copy
C. Villani, Optimal Transport: Old and New, Springer, 2008. doi:10.1007/978-3-540-71050-9

19 thms1 active userReviewed

Operations Research Probability·Captain: mikedeng1

On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems 1: For Symmetric Right-Hand-Side Uncertainty, the Robust Optimum Is at Most Twice the Stochastic OptimumResearch Paper

Motivation

Many planning problems are made in two stages: a first decision $x$ (capacity, inventory, a network design) is fixed before an uncertain demand is revealed, and a second decision $y$ (recourse, routing, overtime) is taken afterwards. Two-stage stochastic optimization models the demand as random and minimizes expected cost; its second stage is a whole policy $\omega\mapsto y(\omega)$ , and the problem is intractable in general, especially with integer variables (Dyer and Stougie, 2006). Robust optimization instead picks one static pair $(x,y)$ that is feasible for every possible demand and minimizes its worst-case cost; it is a single deterministic mixed-integer program and needs no knowledge of the distribution (Ben-Tal and Nemirovski, 2002; Bertsimas and Sim, 2004).

The question this mission addresses is how much is lost by solving the robust problem in place of the stochastic one. Bertsimas and Goyal (Math. Oper. Res. 2010) show that when only the right-hand side is uncertain, the uncertainty set is symmetric and the distribution is centred at its point of symmetry, the loss is at most a factor of two, and that this factor is tight.

Setting

Fix $A\in\mathbb R^{m\times n_1}$ , $B\in\mathbb R^{m\times n_2}$ and nonnegative costs $c\in\mathbb R^{n_1}_+$ , $d\in\mathbb R^{n_2}_+$ . A set $\Omega$ of scenarios carries a probability measure $\mu$ , and each scenario $\omega$ has a right-hand side $b(\omega)\in\mathbb R^m_+$ . The uncertainty set is $\mathcal I_b(\Omega)=\{b(\omega):\omega\in\Omega\}$ . First-stage variables are nonnegative, with integer values on a designated set of coordinates; second-stage variables are nonnegative reals ( $p_2=0$ ).

The stochastic problem $\Pi_{\mathrm{Stoch}}(b)$ , (1.1), chooses $x$ and a policy $y(\cdot)$ :

z_{\mathrm{Stoch}}(b)=\inf\ c^Tx+\mathbb E_\mu[d^Ty(\omega)]\quad\text{s.t.}\quad Ax+By(\omega)\ge b(\omega)\ \ \forall\omega\in\Omega .

The robust problem $\Pi_{\mathrm{Rob}}(b)$ , (1.2), chooses one $y$ for all scenarios:

z_{\mathrm{Rob}}(b)=\inf\ c^Tx+d^Ty\quad\text{s.t.}\quad Ax+By\ge b(\omega)\ \ \forall\omega\in\Omega .

A set $P$ is symmetric (Definition 1.2) if there is $u^0\in P$ with $u^0+z\in P\iff u^0-z\in P$ for all $z$ ; $u^0$ is its point of symmetry. Hypercubes, ellipsoids and norm balls are symmetric. A probability measure on a symmetric set is symmetric (Definition 1.4) if it gives a set and its reflection $\{2u^0-x\}$ the same mass.

Formalization targets

Goal: Theorem 2.1 (p. 10)

If $\mathcal I_b(\Omega)$ is symmetric with point of symmetry $b(\omega^0)$ , $p_2=0$ , and $\mu$ satisfies

\mathbb E_\mu[b(\omega)]\ \ge\ b(\omega^0)\qquad(2.1)

then

z_{\mathrm{Rob}}(b)\ \le\ 2\cdot z_{\mathrm{Stoch}}(b).

Milestones on the way

Lemma 2.2 (p. 12): the coordinatewise bounding box $H$ of a symmetric set $S$ is the smallest hypercube containing $S$ .
Lemma 2.3 (p. 12): the centre $x^0$ of $H$ is the point of symmetry of $S$ , and $x\le 2x^0$ on $S$ when $S\subseteq\mathbb R^n_+$ .
Eqs. (2.9)–(2.10) (p. 13): if $(x,y)$ covers $b(\omega^0)$ then $(2x,2y)$ covers every $b(\omega)$ , so it is robust feasible.
p. 14 display: under (2.1), the mean second-stage decision $\mathbb E_\mu[y(\omega)]$ covers $b(\omega^0)$ .
Lemma 2.1 (p. 11): a symmetric probability measure has mean $u^0$ , so it satisfies (2.1).
Theorem 2.7 (p. 21): the same bound $z_{\mathrm{Rob}}(b)\le 2\,z_{\mathrm{Stoch}}(b)$ when $\mathcal I_b(\Omega)$ is convex and positive (contained in a symmetric subset of $\mathbb R^m_+$ whose centre lies in $\mathcal I_b(\Omega)$ ).

Significance

The result. The robust problem is one mixed-integer program, independent of $\mu$ ; the stochastic problem optimizes over policies and requires the distribution. Theorem 2.1 says that under symmetry the static robust solution $(x,y)$ used in every scenario is a 2-approximation of the optimal expected cost, for every centred distribution at once. The companion results of the paper show the hypotheses matter: the bound is tight for symmetric sets, the gap is unbounded (at least $n+1$ ) on the non-symmetric simplex (Theorem 2.6), and unbounded when costs are uncertain as well (Theorem 3.1). The theorem also underlies later work on the power of static and affine policies in adaptive optimization (Bertsimas and Goyal, 2012).

Formalizing it. The theorem and its proof are published; nothing in this mission is open mathematics. To our knowledge none of these statements has a machine-checked proof. The mission produces a reusable Lean model of two-stage stochastic and robust mixed-integer covering problems with arbitrary scenario spaces, extended-real optimal values and genuine expectations, together with the elementary geometry of point-symmetric sets. The same objects are used by the other missions of this series (the simplex and cost-uncertainty gaps, and the adaptability gap).

Difficulty

Each step of the published argument is short; the difficulty is in stating it at the right generality. The paper begins "consider an optimal solution" of $\Pi_{\mathrm{Stoch}}(b)$ ; optimal policies need not exist for an arbitrary scenario space, so the statement is about infima and every step must work for an arbitrary feasible pair. Passing from " $Ax+By(\omega)\ge b(\omega)$ for all $\omega$ " to " $Ax+B\,\mathbb E_\mu[y]\ge\mathbb E_\mu[b]$ " needs integrability of the policy and of $b$ and linearity of the Bochner integral through a matrix. The bound $b(\omega)\le 2b(\omega^0)$ uses symmetry together with nonnegativity of the uncertainty set; symmetry alone does not give it. Integrality of the second stage breaks the argument, since $\mathbb E_\mu[y(\omega)]$ need not be integral.

Formalization scope

Vectors are Fin k → ℝ with the componentwise order, products A *ᵥ x and inner products c ⬝ᵥ x. The mixed-integer domain is "nonnegative with integer values on a set $I$ of coordinates", which is the paper's $\mathbb R^{n-p}_+\times\mathbb Z^p_+$ up to relabelling.
$\Omega$ is an arbitrary measurable space with a probability measure; $\mathcal I_b(\Omega)$ is Set.range b. Constraints hold for every scenario, not almost surely.
Second-stage policies are $\mu$ -integrable, and $b$ is $\mu$ -integrable in every statement that uses (2.1). Without these, Lean's integral of a non-integrable function is $0$ and (2.1) would degenerate.
$z_{\mathrm{Stoch}}$ and $z_{\mathrm{Rob}}$ are infima in EReal, equal to $+\infty$ when infeasible; no attainment is assumed. A real-valued infimum would return $0$ on an infeasible robust problem and make the goal trivial; that formalization is ruled out.
The bounding box of (2.5)–(2.7) uses suprema and infima, with boundedness assumed where needed.
Corrections to the page: Lemma 2.3's inequality $x\le 2x^0$ is stated under $S\subseteq\mathbb R^n_+$ , which its proof uses and which holds in every application; Lemma 2.1 assumes the measure has a mean; Theorem 2.7 carries the standing assumption $p_2=0$ of §2.

Contributions welcome: proofs of the milestones and the goal, and general lemmas on point-symmetric sets and on interchanging Bochner integrals with matrix–vector products, both reusable outside this mission.

Selected references

D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited from the authors' manuscript, MIT DSpace)
A. Ben-Tal, A. Nemirovski, Robust optimization — methodology and applications, Mathematical Programming 92, 2002. https://doi.org/10.1007/s101070100286
D. Bertsimas, M. Sim, The price of robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065
M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Mathematical Programming 106, 2006. https://doi.org/10.1007/s10107-005-0578-0
D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134, 2012. https://doi.org/10.1007/s10107-011-0444-4

10 thms1 active userReviewed

Completed

Convex Optimization Machine Learning·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity VI: Gradient Descent with η = 2/(α + β) on a β-Smooth α-Strongly Convex Function Has Rate (β/2)exp(−4t/(κ + 1))‖x₁ − x*‖²Textbook

Motivation

Gradient descent is a basic method for minimizing a differentiable function when evaluating its gradient is practical but solving the optimization problem directly is not. The rate at which its iterates approach an optimizer depends on the assumptions about the function. For a convex function with a Lipschitz gradient, the value error decreases at a sublinear rate. Adding strong convexity changes the behavior: the distance from the optimizer contracts at each step, giving an exponential bound on the value error. This section of Bubeck's monograph identifies a fixed step size that uses both the smoothness and curvature constants and gives the corresponding rate.

The result matters when a high-accuracy answer is needed. A sublinear bound makes each extra digit progressively more expensive; an exponential bound says that a fixed number of additional gradient evaluations reduces the error by a fixed factor. The theorem is a textbook result, already proved mathematically. This mission asks for its precise machine-checked statement and the source's supporting inequalities, rather than for a new optimization method.

Setting

Work in Euclidean space $\mathbb R^n$ with $n\ge1$ , equipped with its usual inner product and norm. A differentiable function $f:\mathbb R^n\to\mathbb R$ has gradient $g(x)=\nabla f(x)$ . It is $\beta$ -smooth when its gradient is $\beta$ -Lipschitz: $\|g(x)-g(y)\|\le\beta\|x-y\|$ for every $x,y$ . It is $\alpha$ -strongly convex when, for every $x,y$ ,

f(y)\ge f(x)+\langle g(x),y-x\rangle+\frac\alpha2\|y-x\|^2.

The first condition limits how rapidly the gradient changes. The second gives a quadratic lower bound on the function around any point. Here $\alpha>0$ and $\beta\ge0$ . In positive dimension, the two conditions together entail $\beta\ge\alpha$ , so the condition number $\kappa=\beta/\alpha$ is at least one. The case $\alpha=\beta$ remains part of the target.

A point $x^*$ is a global minimizer when $f(x^*)\le f(y)$ for every $y$ . The book assumes such a point exists as a standing convention. A gradient descent run is a sequence $(x_t)_{t\ge1}$ satisfying $x_{t+1}=x_t-\eta g(x_t)$ at each positive index. Its first iterate $x_1$ is arbitrary. The step size in this mission is fixed at $\eta=2/(\alpha+\beta)$ , rather than chosen by line search or adapted along the run.

Formalization targets

The central target is Theorem 3.12 of Bubeck, p. 279. For every integer $t\ge0$ , the gradient descent run satisfies

f(x_{t+1})-f(x^*)\le \frac\beta2\exp\!\left(-\frac{4t}{\kappa+1}\right)\|x_1-x^*\|^2.

At $t=0$ this is a smoothness bound on the initial value gap. For subsequent iterations it gives a linear convergence rate with the explicit exponential factor stated in the book. No initial-radius bound or bounded domain is imposed: the actual squared distance $\|x_1-x^*\|^2$ appears in the conclusion.

The milestones trace the mathematical claims stated in the source. Equation (3.6) is the co-coercivity inequality for gradients of convex smooth functions. The proof of Lemma 3.11 introduces $\phi(z)=f(z)-(\alpha/2)\|z\|^2$ , and identifies it as convex and $(\beta-\alpha)$ -smooth. Lemma 3.11 combines curvature and smoothness into a sharper inequality for two gradients. The proof of Theorem 3.12 then gives a value-gap bound, a one-step distance contraction, and its iterated exponential form. These statements are separately useful: the co-coercivity and contraction bounds can be reused in analyses of related first-order methods.

Significance

The theorem states a complete guarantee for the algorithm: an explicit rule, the hypotheses on the objective, and a bound valid for every iteration count. It makes the role of $\kappa$ visible. When $\kappa$ is close to one, the contraction is strong; when the smoothness constant is much larger than the curvature constant, more iterations are needed for the same error reduction. The stated dependence supports comparisons with projected and accelerated gradient methods elsewhere in the same monograph.

Formalizing the result requires a common interface for actual gradients, smoothness, strong convexity, and algorithm runs. The strong-convexity predicate is an existing published definition, while the local smoothness and run definitions use Bubeck's conventions. Once these interfaces and the inequalities are proved, later missions can use the resulting declarations to compare rates without translating between informal meanings of “smooth” or changing the iterate index. The source provides a mathematical proof; these draft Lean theorems carry sorry and do not yet constitute machine-checked proofs.

Difficulty

The main issue is getting the sharp contraction factor from two assumptions that control different parts of the gradient step. A direct Lipschitz estimate on the update map does not by itself express the mixed inner-product term with the constants needed for the stated factor. Lemma 3.11 is the source's precise bridge between the gradient difference, the point displacement, and their inner product. The case $\alpha=\beta$ also needs to remain valid: a proof route that divides by $\beta-\alpha$ cannot cover that boundary by the same calculation.

The last display in the proof of Theorem 3.12 joins a one-step inequality involving $x_t$ to an exponential inequality involving $x_1$ . The latter is the cumulative statement after $t$ steps. Keeping these as separate milestones makes each quantified claim explicit while preserving the theorem's bound.

Formalization scope

Lean represents $\mathbb R^n$ as EuclideanSpace ℝ (Fin n), with $n>0$ . The gradient is an explicit map $g$ required to be the actual gradient of $f$ at every point. Smoothness is the gradient Lipschitz condition, not a quadratic upper bound used as a definition. Strong convexity uses the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn predicate on the whole space; its formula is the book's (3.13). Iterates are indexed from one, and index zero imposes no condition. The norm, inner product, constants, and real exponential follow the printed formulas.

The added explicit conditions are $n>0$ , $\alpha>0$ , and $\beta>0$ where Equation (3.6) divides by $\beta$ . Positive dimension excludes a degenerate space where curvature imposes no restriction on smoothness. The positivity of $\alpha$ makes $\kappa$ meaningful; the source treats it as a positive strong-convexity parameter. The minimizer hypothesis is the book's standing convention. There is no assumption that $g(x^*)=0$ : that property follows from global minimality and differentiability. A gradient map unrelated to $f$ would trivialize the model, so the smoothness definition includes the gradient identity.

The local development needs Euclidean inner-product identities, convexity, differentiability, Lipschitz gradient bounds, and real exponential estimates. The auxiliary function and the two co-coercivity inequalities are reusable outside this chapter. Contributions should prove the exact milestone statements and the final theorem, including $t=0$ and $\alpha=\beta$ , without weakening constants or substituting another gradient descent step.

Selected references

Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2; DOI:10.1561/2200000050.

9 thms1 active userReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

An Analysis of Stochastic Shortest Path Problems: If Every Improper Policy Has Infinite Cost, the Optimal Cost Is the Unique Fixed Point of Bellman's Operator and Value Iteration Converges to ItResearch Paper

Motivation

A shortest path problem asks how to reach a destination at minimum cost. In a stochastic shortest path problem, a decision at a state selects a probability distribution over successor states, so both the route and its total cost are random. Costs may have either sign. This makes the problem relevant to finite-state control models where rewards and expenses occur before eventual termination. Bertsekas and Tsitsiklis analyze this setting without requiring all one-stage costs to be nonnegative or all to be nonpositive. Their condition instead rules out an improper stationary policy whose costs stay finite from every initial state. Bertsekas and Tsitsiklis (1991), pp. 580–583.

Earlier treatments established Bellman-equation and algorithmic conclusions under positive or nonnegative costs. The 1991 paper traces the finite-control development from Eaton and Zadeh and the compact-control extension from Kushner, then removes the sign restriction while retaining finite state space. It also explains why the Bellman mapping need not contract when an improper policy is available. Bertsekas and Tsitsiklis (1991), pp. 581, 585. A separate, proved Prove2Me theorem from Bertsekas's textbook treats the special case in which every policy is proper and controls are finite; the result here permits improper policies and compact control spaces.

Setting

There are $n\ge1$ states. State $1$ is the destination. At state $i$ , a control $u\in U(i)$ incurs a real cost $c_i(u)$ and moves the process to state $j$ with probability $p_{ij}(u)$ . A selector $\mu$ chooses one control $\mu(i)$ at every state. A policy $\pi=(\mu_0,\mu_1,\ldots)$ may change selectors over time; a stationary policy repeats one selector. The matrix $P(\mu)$ has entries $p_{ij}(\mu(i))$ , and $c(\mu)$ is the vector of one-stage costs. Bertsekas and Tsitsiklis (1991), p. 582.

The cost vector $x(\pi)$ is the coordinatewise limit inferior of expected partial costs, including the possibility of infinite values. The optimal cost $x_i^*$ is the infimum of $x_i(\pi)$ over all policies, including nonstationary ones. Optimality of a policy means it attains that infimum from every initial state. The fixed-selector operator is $T_\mu(x)=c(\mu)+P(\mu)x$ ; the Bellman operator $T$ takes the coordinatewise infimum of these vectors over selectors. Bertsekas and Tsitsiklis (1991), pp. 582–583, equations (2)–(6).

A stationary policy is proper when its probability of reaching state $1$ tends to one from every starting state. Assumption 1 says state $1$ is absorbing and cost-free, at least one proper stationary policy exists, and every improper stationary policy has a partial-cost coordinate tending to $+\infty$ . Assumption 2 makes each control space compact, each cost function lower semicontinuous, and each transition-probability coordinate continuous. Work takes place in $X=\{x\in\mathbb R^n:x_1=0\}$ . Bertsekas and Tsitsiklis (1991), pp. 583–584.

Formalization targets

Proposition 2: Bellman's equation and value iteration

Under Assumptions 1 and 2, the optimal cost is finite and is the unique fixed point of $T$ in $X$ . Every initial $x\in X$ has

\lim_{t\to\infty}T^t(x)=x^*.

A stationary selector $\mu$ is optimal exactly when $T_\mu(x^*)=T(x^*)$ ; an optimal proper stationary selector exists. These are all clauses of Proposition 2, rather than separate targets selected from it. Bertsekas and Tsitsiklis (1991), p. 586, Proposition 2.

Supporting results

The milestone list follows the source's Proposition 1, Lemmas 1–3, and the numbered equations used by their proof. Proposition 1 supplies a weighted maximum-norm contraction when every stationary policy is proper. Lemma 1 describes fixed costs of a proper policy and characterizes properness through a Bellman inequality. Lemma 2 gives continuity of $T$ . Lemma 3 controls limits of proper policies; its second part detects a limit that becomes improper through diverging costs. Appendix equations (22) and (24), and the policy-improvement equation (15), provide the paper's intermediate targets. Bertsekas and Tsitsiklis (1991), pp. 585–587, 591–592.

Significance

Proposition 2 identifies the cost of the best policy by a finite-dimensional Bellman equation even though the definition of optimal cost ranges over all, possibly nonstationary, policies. Its convergence clause justifies value iteration from any vector whose destination coordinate is zero. Its policy criterion and existence clause connect a fixed point to an implementable stationary decision rule. The paper applies these conclusions to successive approximation and policy iteration in §4. Bertsekas and Tsitsiklis (1991), pp. 586, 590–591.

The paper proves these statements. This mission seeks machine-checked proofs of their exact finite-state formulation and of the listed intermediate results. The resulting finite stochastic-matrix, hitting, and policy-cost infrastructure can also support other undiscounted control problems. The related proved Prove2Me result for the all-proper finite-control case does not settle this mission's compact-control or improper-policy cases.

Difficulty

When every stationary policy is proper, a common weighted maximum norm makes the Bellman mapping contract. An improper policy can destroy this route: Figure 2 has an absorbing destination and satisfies both assumptions, yet $T(0,x_2)=(0,\min\{1+x_2,2\})$ is not a contraction in any norm on $X$ . The main result therefore needs a way to retain fixed-point uniqueness and convergence without a uniform contraction rate. Compactness matters because a sequence of proper selectors may converge to an improper selector; Lemma 3 explains the associated cost behavior. Bertsekas and Tsitsiklis (1991), pp. 585–586, 591–595.

Formalization scope

States are Fin n, with the paper's state $1$ represented by 0; the model requires $n\ge1$ . A control set $U(i)$ is a type with a metric, with compactness asserted for its whole carrier. Transition rows explicitly have nonnegative entries summing to one. These are the probability-vector conditions implicit in the word “probability.” Assumption 1 supplies a selector and therefore nonempty control sets. The paper writes $T:\mathbb R^n\to\mathbb R^n$ ; where a theorem uses only Assumption 1, finite real Bellman infima are made explicit through TRealValued. Under Assumption 2, compactness and lower semicontinuity give real attained minima. Bertsekas and Tsitsiklis (1991), pp. 582–584.

Policy costs and their infimum use extended reals so that an improper policy's $+\infty$ cost is represented without a default finite value. Proposition 2 concludes, rather than assumes, that $x^*$ has real coordinates. Its policy infimum ranges over every sequence of selectors. Matrix products use the identity at time zero; $T^0$ is the identity. The destination-zero restriction is retained in every fixed-point and iteration claim. Defining optimal cost as a Bellman fixed point, or restricting the infimum to stationary policies, would remove the result the paper proves. Solvers can contribute the finite-chain, matrix-inverse, semicontinuity, and convergence arguments needed by these targets.

Selected references

Dimitri P. Bertsekas and John N. Tsitsiklis, An Analysis of Stochastic Shortest Path Problems, Mathematics of Operations Research 16(3), 580–595, 1991. DOI.

11 thms1 active userReviewed

Control Theory Dynamic Programming Operations Research+2·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case IX: Imperfect State Information — Reduction to a Perfect-Information Model through a Statistic Sufficient for ControlTextbook

Motivation

In most control problems the controller does not see the state of the system. It sees noisy observations, remembers its past controls, and must act on that record. Inventory systems with delayed or inaccurate counts, maintenance of machines whose wear is only inspected, target tracking, and medical treatment planned from test results all have this form. The standard device for such problems is to replace the hidden state by a summary of the record, most often the conditional distribution of the state given the observations, and to solve a dynamic program whose state is that summary.

For finite or countable spaces this reduction goes back to Åström (1965) and Striebel (1965), who introduced the conditional distribution of the state as a "sufficient statistic" for control. Chapter 10 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996) carries it out for Borel state, control and observation spaces, with universally measurable policies and costs that are only lower semianalytic. In that generality the measurability of the reduced model is the whole difficulty, and the chapter isolates exactly what a summary must satisfy for the reduction to be exact.

Setting

The imperfect state information model (ISI) of Definition 10.3 has a nonempty Borel state space $S$ , control space $C$ and observation space $Z$ ; a discount factor $\alpha>0$ ; a lower semianalytic cost $g:SC\to R^*=[-\infty,\infty]$ ; a Borel state transition kernel $t(dx'\mid x,u)$ ; Borel observation kernels $s_0(dz\mid x)$ and $s(dz\mid u,x)$ ; and a horizon $N$ . The initial state $x_0$ has distribution $p\in P(S)$ , $z_0\sim s_0(\cdot\mid x_0)$ , and then $x_{k+1}\sim t(\cdot\mid x_k,u_k)$ , $z_{k+1}\sim s(\cdot\mid u_k,x_{k+1})$ . The controller knows the information vector $i_k=(z_0,u_0,\dots,u_{k-1},z_k)\in I_k$ and must choose $u_k\in U_k(i_k)$ , where the constraint set $\Gamma_k=\{(i_k,u)\mid u\in U_k(i_k)\}$ is analytic.

A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ consists of universally measurable stochastic kernels $\mu_k(du_k\mid p;i_k)$ that respect the constraints (Definition 10.4). Together with $p$ it determines probability measures $P_k(\pi,p)$ on the histories $(x_0,z_0,u_0,\dots,x_k,z_k,u_k)$ , the cost

J_{N,\pi}(p)=\int\Big[\sum_{k=0}^{N-1}\alpha^k g(x_k,u_k)\Big]dP_{N-1}(\pi,p),

and the optimal cost $J^*_N(p)=\inf_\pi J_{N,\pi}(p)$ (Definition 10.5). Assumption $(F^+)$ asks that the expected discounted negative part of the cost be finite for every policy and initial distribution; $(F^-)$ asks the same of the positive part.

A statistic is a sequence of Borel maps $\eta_k:P(S)I_k\to Y_k$ into nonempty Borel spaces. It is sufficient for control (Definition 10.6) if (a) the constraints can be read off from it, $\Gamma_k=\{(i_k,u)\mid(\eta_k(p;i_k),u)\in\hat\Gamma_k\}$ with $\hat\Gamma_k$ analytic; (b) the conditional law of $\eta_{k+1}$ given $(\eta_k,u_k)$ is a Borel kernel $\hat t_k(dy_{k+1}\mid y_k,u_k)$ , for every $p$ and every policy; and (c) the conditional expectation of $g(x_k,u_k)$ given $(\eta_k,u_k)$ is a lower semianalytic function $\hat g_k(y_k,u_k)$ . The perfect state information model (PSI) of Definition 10.7 has states $y_k\in Y_k$ , constraints $\hat U_k(y_k)=(\hat\Gamma_k)_{y_k}$ , costs $\hat g_k$ and transitions $\hat t_k$ ; its cost and optimal cost at $y\in Y_0$ are $\hat J_{N,\hat\pi}(y)$ and $\hat J^*_N(y)$ . The initial distribution of $y_0$ is

\varphi(p)(\underline Y_0)=\int_S s_0(\{z_0\mid\eta_0(p;z_0)\in\underline Y_0\}\mid x_0)\,p(dx_0).

A Markov (PSI) policy $\hat\mu_k(du\mid y_k)$ acts in (ISI) through $\mu_k(du\mid p;i_k)=\hat\mu_k(du\mid\eta_k(p;i_k))$ .

Formalization targets

Goal: Proposition 10.3

Under $(F^+,\hat F^+)$ or $(F^-,\hat F^-)$ ,

J^*_N(p)=\int_{Y_0}\hat J^*_N(y_0)\,\varphi(p)(dy_0)\qquad\forall p\in P(S),

and a Markov (PSI) policy that is optimal, $\varphi(p)$ -optimal or weakly $\varphi(p)$ - $\varepsilon$ -optimal for (PSI) is respectively optimal, optimal at $p$ , or $\varepsilon$ -optimal at $p$ for (ISI); under $(F^+,\hat F^+)$ an $\varepsilon$ -optimal (PSI) policy is $\varepsilon$ -optimal for (ISI). Here $\hat\pi$ is weakly $q$ - $\varepsilon$ -optimal if $\int\hat J_{N,\hat\pi}\,dq\le\int\hat J^*_N\,dq+\varepsilon$ when $\int\hat J^*_N\,dq>-\infty$ and $\int\hat J_{N,\hat\pi}\,dq\le-1/\varepsilon$ otherwise, and $q$ -optimal if $q(\{y_0\mid\hat J_{N,\hat\pi}(y_0)=\hat J^*_N(y_0)\})=1$ (Definition 10.8).

Milestones

Lemma 10.1: the process $(\eta_0,u_0,\dots,\eta_k,u_k)$ generated in (ISI) by a Markov (PSI) policy has the law $\hat P_k[\hat\pi,\varphi(p)]$ .
Proposition 10.2: $J_{N,\hat\pi}(p)=\int\hat J_{N,\hat\pi}\,d\varphi(p)$ for Markov $\hat\pi$ .
Corollary 10.2.1: $J^*_N(p)\le\int\hat J^*_N\,d\varphi(p)$ .
Lemma 10.2: every (ISI) policy is matched in cost by some Markov (PSI) policy.
Proposition 10.4: $\varepsilon$ -optimal nonrandomized (ISI) policies that depend on $i_k$ only through $\eta_k(p;i_k)$ .
Proposition 10.6: the identity maps on $P(S)I_k$ form a statistic sufficient for control.

Significance

Proposition 10.3 says that an imperfect-information problem loses nothing by being solved in the reduced model: the optimal cost is the $\varphi(p)$ -average of the reduced optimal cost, and good reduced policies are good original policies. Combined with Proposition 10.6, every (ISI) model has such a reduction, so the finite-horizon dynamic programming theory of Chapter 8 (existence of $\varepsilon$ -optimal policies, the dynamic programming algorithm) transfers to partially observed problems on Borel spaces. Proposition 10.4 turns this into a structural statement about the original problem: nearly optimal controllers need to retain only the statistic.

These results are proved in the book. None of them is formalized: the platform's related results (Bäuerle–Rieder's partially observable models with observation densities, and the linear-quadratic-Gaussian separation theorem) work in different models and do not cover universally measurable policies, analytic constraints, or lower semianalytic costs. A machine-checked version makes the conditional-expectation bookkeeping of the reduction explicit, and the definitions of this mission (universal measurability, lower semianalytic functions, the book's extended integral, history measures built from universally measurable kernels) are reusable by every other chapter of the book.

Difficulty

The obvious argument says: replace the state by the statistic, observe that costs and transitions depend only on the statistic, and conclude. In the Borel setting each step is a measurability claim that the naive argument does not supply. The conditions of Definition 10.6 are almost-everywhere statements about conditional distributions under every pair $(p,\pi)$ , while the reduced model needs genuine kernels; the policies are only universally measurable, so integrals and compositions must be taken with respect to completions; the costs take the values $\pm\infty$ , so interchanging sums and integrals requires the finiteness assumptions $(F^\pm)$ and $(\hat F^\pm)$ ; and the inequality $J^*_N\ge\int\hat J^*_N\,d\varphi(p)$ requires producing, from an arbitrary history-dependent (ISI) policy, a Markov (PSI) policy with the same cost, which the naive argument does not do.

Formalization scope

Horizon. Only finite horizons $N\ge1$ are covered, hence only the cases $(F^+,\hat F^+)$ and $(F^-,\hat F^-)$ of the book's statements; the infinite-horizon cases $(P,\hat P)$ , $(N,\hat N)$ , $(D,\hat D)$ are out of scope.
Extended reals. Costs live in EReal with the book's convention $\infty-\infty=+\infty$ written out explicitly (badd, bsum, extIntegral); Mathlib's EReal subtraction ( $\top-\top=\bot$ ) is never used where both terms can be infinite.
Spaces and measures. $S$ , $C$ , $Z$ , $Y_k$ are Borel spaces in the sense of Definition 7.7 with their Borel $\sigma$ -algebras; $P(S)$ carries the weak topology and the Giry $\sigma$ -algebra. Policies are families of maps into ProbabilityMeasure C that are measurable for the completion of every probability measure. History measures are characterized by their values on rectangles. Families indexed by the stage are indexed by all of $\mathbb N$ ; only stages $k<N$ are constrained.
Conditional statements. Conditions (22) and (23) are stated through the defining relations of conditional probability and expectation, for every $p$ and every policy, with (23) required when $g(x_k,u_k)$ is quasi-integrable.
Policies in Proposition 10.3. The (PSI) policies in the optimality transfers are Markov, as in Proposition 10.2.
No trivialization. Definition 10.6 is the full definition: analytic $\hat\Gamma_k$ with full projection, Borel kernels $\hat t_k$ satisfying (22) for every $p$ and policy, and lower semianalytic $\hat g_k$ satisfying (23); a weaker notion would make Proposition 10.6 empty.

Contributions are welcome on any milestone. Basic facts that a full development needs, such as composition of universally measurable maps (Proposition 7.44), measurability of integrals against universally measurable kernels (Proposition 7.46), and existence of the history measures (Proposition 7.45), can be posed and proved as supporting lemmas; they are reusable across the book.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10 (1965) 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
C. Striebel, Sufficient statistics in the optimum control of stochastic systems, Journal of Mathematical Analysis and Applications 12 (1965) 576–592. https://doi.org/10.1016/0022-247X(65)90027-2
N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9

12 thms1 active userReviewed

Dynamic Programming Operations Research·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case IV: The Generalized Abstract Model — Restricted Policy Classes under ContractionTextbook

Why restricted policy classes

Abstract dynamic programming, in the form developed by Denardo (1967) and Bertsekas (1977), studies sequential decision problems through a single monotone mapping $H(x,u,J)$ : the cost of using control $u$ at state $x$ when the future is valued by the function $J$ . Chapters 2–5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), analyze this model when policies are arbitrary selectors $\mu:S\to C$ and $H$ is defined on all extended-real functions on $S$ .

That generality breaks down as soon as the state and control spaces are uncountable. A stochastic control problem on Borel spaces needs measurable policies, so that the expected cost is an integral rather than an outer integral, and the functions on which $H$ acts must be measurable for the same reason. Chapter 6 of the book introduces a generalized abstract model in which the policies are drawn from a prescribed class $\tilde M$ and $H$ is only defined on a prescribed class $\tilde F$ of functions. The examples on p. 94 are the models of Part II: universally measurable policies with lower semianalytic costs (Chapters 8–9), analytically measurable policies (Section 11.2), and the semicontinuous models of Definitions 8.7–8.8. Chapter 6 is the bridge that lets the abstract results of Part I be invoked for these models.

Setting

The data are a state space $S$ , a control space $C$ , nonempty constraint sets $U(x)\subseteq C$ , and three restricted classes: sets of functions $F^*\subset\tilde F\subset F$ , where $F$ is the set of all functions $S\to[-\infty,\infty]$ , and a set $\tilde M$ of selectors $\mu:S\to C$ with $\mu(x)\in U(x)$ . The mapping $H:S\times C\times\tilde F\to[-\infty,\infty]$ is monotone: $J\le J'$ in $\tilde F$ implies $H(x,u,J)\le H(x,u,J')$ . For $\mu\in\tilde M$ and $J\in\tilde F$ ,

T_\mu(J)(x)=H[x,\mu(x),J],\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J).

A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ with every $\mu_k\in\tilde M$ ; their set is $\tilde\Pi$ . Given $J_0\in F^*$ with $J_0>-\infty$ , the $N$ -stage and infinite-horizon costs are

J_{N,\pi}=(T_{\mu_0}\cdots T_{\mu_{N-1}})(J_0),\qquad J_\pi(x)=\lim_{N\to\infty}J_{N,\pi}(x),

and the optimal costs are $J^*_N=\inf_{\pi\in\tilde\Pi}J_{N,\pi}$ and $J^*=\inf_{\pi\in\tilde\Pi}J_\pi$ . For a stationary policy $(\mu,\mu,\dots)$ write $J_\mu$ .

Five standing conditions tie the classes together: A.1 (every control $u\in U(x)$ is the value $\mu(x)$ of some $\mu\in\tilde M$ ), A.2 ( $F^*$ is closed under $T$ and under adding constants), A.3 ( $\tilde F$ is closed under every $T_\mu$ , $\mu\in\tilde M$ , and under adding constants), A.4 ( $\varepsilon$ -minimizing selectors for $T(J)$ , $J\in F^*$ , exist in $\tilde M$ ), and A.5 ( $\tilde F$ and $F^*$ are closed under pointwise limits). Assumption $\tilde C$ asks for a closed subset $\bar B$ of the space $B$ of bounded real functions with the sup norm $\|\cdot\|$ , containing $J_0$ and invariant under $T$ on $\bar B\cap F^*$ and under $T_\mu$ on $\bar B\cap\tilde F$ , such that every $J_\pi$ exists and is real, each $T_\mu$ is $\alpha$ -Lipschitz on $B\cap\tilde F$ , and every $m$ -fold composition $T_{\mu_0}\cdots T_{\mu_{m-1}}$ is a $\rho$ -contraction on $\bar B\cap\tilde F$ for some $\rho<1$ .

Formalization targets

Goal: Proposition 6.4 (p. 97)

Under A.1–A.5 and $\tilde C$ : $J^*\in\bar B\cap F^*$ is the unique fixed point of $T$ in $\bar B\cap F^*$ , with $T(J')\le J'\Rightarrow J^*\le J'$ and $J'\le T(J')\Rightarrow J'\le J^*$ ; each $J_\mu$ , $\mu\in\tilde M$ , is the unique fixed point of $T_\mu$ in $\bar B\cap\tilde F$ ;

\lim_{N\to\infty}\|T^N(J)-J^*\|=0\ \ (J\in\bar B\cap F^*),\qquad\lim_{N\to\infty}\|T_\mu^N(J)-J_\mu\|=0\ \ (J\in\bar B\cap\tilde F);

a stationary $(\mu^*,\mu^*,\dots)\in\tilde\Pi$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$ ; and for every $\varepsilon>0$ some stationary policy in $\tilde\Pi$ satisfies $\|J^*-J_{\mu_\varepsilon}\|\le\varepsilon$ .

Milestones

In attack order:

Proposition 6.3(a) (p. 96) — under A.1–A.4 and the exact selection assumption, a uniformly $N$ -stage optimal policy exists iff the infimum in $T^{k+1}(J_0)(x)=\inf_{u\in U(x)}H[x,u,T^k(J_0)]$ is attained for each $x\in S$ and $k<N$ .
Proposition 6.5(a) (p. 97) — under A.1–A.5, $\tilde C$ and exact selection: if for each $x$ some policy in $\tilde\Pi$ is optimal at $x$ , then an optimal stationary policy exists in $\tilde\Pi$ .

Further results of the chapter

The other results of Sections 6.2–6.3 are posed in the mission as separate theorems:

Proposition 6.2 — $\pi^*$ is uniformly $N$ -stage optimal iff $(T_{\mu_k^*}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$ ; such a policy forces $J^*_N=T^N(J_0)$ .
Proposition 6.1(a) — under Assumption $\tilde F.2$ and $J^*_k>-\infty$ : $J^*_N=T^N(J_0)$ and $N$ -stage $\varepsilon$ -optimal policies exist in $\tilde\Pi$ .
Proposition 6.1(b) — under Assumption $\tilde F.3$ and $J_{k,\pi}<\infty$ : $J^*_N=T^N(J_0)$ and $\{\varepsilon_n\}$ -dominated convergence to optimality.
Proposition 6.3(b) — compact level sets $U_k(x,\lambda)$ give both $J^*_N=T^N(J_0)$ and a uniformly $N$ -stage optimal policy.
Proposition 6.5(b) — compact level sets of the iterates $T^k(J)$ , $k\ge\bar k$ , give an optimal stationary policy.

Significance

Proposition 6.4 is the statement that makes value iteration, Bellman's equation and stationary $\varepsilon$ -optimal policies available for discounted problems whose admissible policies are restricted, for instance to measurable ones. Without it, each measurable model would need its own fixed-point argument. The finite-horizon Propositions 6.1–6.3 play the same role for the dynamic programming algorithm $J^*_N=T^N(J_0)$ , and their hypotheses ( $\tilde F.3$ , exact selection) are exactly what Chapters 7–8 verify for universally measurable policies.

The book states Propositions 6.4 and 6.5 without proof (p. 97), referring to the proofs of Chapter 4; Propositions 6.1–6.3 are justified by "nearly verbatim repetition" of Chapter 3. A formalization therefore supplies proofs that are only indicated in print, and checks that A.1–A.5 really suffice for each step of the Chapter 3–4 arguments. None of these results has a machine-checked proof that we know of; the companion missions of this series formalize the unrestricted special case ( $F^*=\tilde F=F$ , $\tilde M=M$ ) of Chapters 3 and 4.

Difficulty

The Chapter 4 proof of Proposition 4.2 applies the contraction mapping theorem to $T$ on $\bar B$ . Here the obvious transcription fails at two points. First, $T$ maps $\bar B\cap F^*$ into itself but $T_\mu$ only maps $\bar B\cap\tilde F$ into itself, so the fixed-point theorem must be applied on two different sets, and these are closed only because of A.5. Second, every argument that picks a near-minimizing selector at each state must produce a selector in $\tilde M$ : pointwise choices are no longer allowed, and A.1, A.4 and the exact selection assumption are the only sources of admissible selectors. Proofs of Chapter 3–4 that build a policy state by state cannot be copied.

Formalization scope

Functions on $S$ are S → EReal. $H$ is a total Lean function, but monotonicity is assumed only on $\tilde F$ and every statement evaluates $H$ only at functions of $\tilde F$ . $J_\pi$ is limUnder; Assumption $\tilde C$ makes the limit exist. $B$ is Mathlib's $\ell^\infty(S,\mathbb R)$ ; a bound $\|G-G'\|\le c$ between extended-real functions means both are real everywhere and $|G(x)-G'(x)|\le c$ , which is how the book's convention $\infty-\infty=\infty$ reads a norm of a difference. No statement adds values of opposite infinite sign, so Mathlib's EReal addition agrees with the book's wherever it is used. $J^*_N$ and $J^*$ are infima over $\tilde\Pi$ only, the $\varepsilon$ -optimality notions keep the book's two-case form at $-\infty$ , and $N$ is a positive integer.

The chapter collapses to Chapters 3–4 if $F^*=\tilde F=F$ or $\tilde M=M$ is built in; here $F^*$ , $\tilde F$ and $\tilde M$ are arbitrary and constrained only by A.1–A.5, and $J^*$ is never defined as a fixed point.

A complete development needs the $m$ -step contraction mapping theorem on a closed subset of $\ell^\infty$ , monotonicity lemmas for $T$ and $T_\mu$ , and the restricted-class versions of Propositions 3.1–3.4 and 4.1–4.4. These are reusable for the Borel models of Chapters 8–9. Proofs of any milestone, and sorry-free lemmas about the Assumption $\tilde C$ contraction, are welcome.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 6. https://web.mit.edu/dimitrib/www/soc.html
D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control and Optimization 15(3), 1977, 438–464. https://doi.org/10.1137/0315031
E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2), 1967, 165–177. https://doi.org/10.1137/1009030

7 thms1 active userReviewed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Maximal Flow Through a Network II: In an ab-Planar Network Some Chain from Source to Sink Meets Every Cut Exactly OnceResearch Paper

Motivation

The maximum flow problem asks how much of a commodity can be shipped from a source to a sink through a network whose arcs have limited capacities. L. R. Ford, Jr. and D. R. Fulkerson's 1956 paper Maximal Flow Through a Network proved the minimal cut theorem: the largest flow value equals the smallest total capacity of a set of arcs that separates source from sink. That theorem is formalized in the companion mission Maximal Flow Through a Network I.

The second section of the same paper treats a special class of networks, those that remain planar after an arc from source to sink is added. For these networks the paper shows that one particular source–sink chain crosses every minimal separating set exactly once. This structural fact turns the minimal cut theorem into a simple computing procedure: repeatedly push as much flow as possible along such a chain and delete the arcs it saturates. The paper notes that G. Dantzig had conjectured, before the minimal cut theorem was proved, that this procedure yields a maximal flow on planar networks. The same "uppermost path" idea underlies later algorithms for maximum flow in planar graphs with source and sink on a common face (Itai and Shiloach, 1979).

The statement is short and purely combinatorial in its conclusion, but its hypothesis is topological. This mission isolates that theorem.

Setting

A network $N$ has a finite set $V$ of vertices and a finite set $E$ of arcs. Each arc $e$ joins two distinct end vertices, written $\mathrm{tail}(e)$ and $\mathrm{head}(e)$ ; arcs carry no direction, and two arcs may join the same pair of vertices. Two distinct vertices are distinguished, the source $a$ and the sink $b$ , and each arc carries a positive capacity (capacities play no role in the target below).

A chain joining $u$ and $w$ is a set $C$ of distinct arcs that can be arranged as $\alpha_1(v_0v_1), \alpha_2(v_1v_2), \dots, \alpha_k(v_{k-1}v_k)$ with $v_0 = u$ , $v_k = w$ , and the vertices $v_0, \dots, v_k$ pairwise distinct; each arc may be traversed in either direction. The empty set is the null chain from $u$ to $u$ .

A set $D$ of arcs is a disconnecting set if every chain joining $a$ and $b$ contains an arc of $D$ . A disconnecting set none of whose proper subsets is disconnecting is a cut.

The network is ab-planar if the graph of $N$ , together with one additional arc joining $a$ and $b$ , can be drawn in the plane without crossings: vertices go to distinct points of $\mathbb R^2$ ; each arc, including the added arc $ab$ , goes to an injective continuous path between the points of its end vertices; no arc passes through a vertex other than its ends; and two distinct arcs meet only at endpoints of both. In Lean the drawing is the structure ABPlaneDrawing N, and $N$ is ab-planar when Nonempty (ABPlaneDrawing N). The section's standing assumption is that no arc of $N$ already joins $a$ and $b$ .

Formalization targets

Goal: Theorem 2 (p. 403)

If $N$ is ab-planar, no arc of $N$ joins $a$ and $b$ , and some chain joins $a$ and $b$ , then

\exists\, T \text{ a chain joining } a \text{ and } b \ \text{ such that }\ |T \cap D| = 1 \ \text{ for every cut } D \text{ of } N.

This is FordFulkerson56.Planar.ab_planar_exists_chain_meeting_each_cut_once. "Precisely once" is exact cardinality one, neither "at least once" (true of every chain) nor "at most once".

Milestone: a chain meeting a cut in one prescribed arc (proof of Theorem 2, p. 403)

For every network $N$ , every cut $D$ and every arc $\alpha \in D$ , there is a chain $C$ joining $a$ and $b$ with $C \cap D = \{\alpha\}$ . No planarity is involved; the statement is what the minimality of a cut provides to the proof.

Further item: the Fig. 2 example (p. 403)

In the "gas, water, electricity" graph $K_{3,3}$ with the arc $ab$ removed, every chain joining $a$ and $b$ meets some cut in three arcs. This network is not ab-planar, so the example shows that the planarity hypothesis of Theorem 2 cannot be dropped.

Significance

Theorem 2 and the minimal cut theorem together give the paper's procedure for planar networks: if $T$ meets every cut once, then imposing a flow $k$ on $T$ lowers the value of every cut by exactly $k$ , so the minimal cut value, and hence the maximal flow value, drops by $k$ . Saturated arcs can then be deleted and the step repeated. Without the "exactly once" property the reduction could overshoot the cut structure, and the greedy step would not be justified. The theorem is also one of the earliest instances of the link between planarity and cut structure that later underlies planar duality arguments for minimum cuts.

The result has been known since 1956 and is not open. No machine-checked version is recorded on the platform, and Mathlib, at the pinned revision, has neither planar graphs nor the Jordan curve theorem. A formal proof would be the first formalized statement about source–sink planar networks in this library, and the counterexample item records, as a checkable fact, that the hypothesis is necessary.

Difficulty

The conclusion is combinatorial while the hypothesis is a drawing in $\mathbb R^2$ . The paper's proof normalises the drawing (the added arc $ab$ on the outer boundary, the graph in a vertical strip with $a$ on the left line and $b$ on the right), selects the "top-most" chain from $a$ to $b$ , and argues that a chain meeting a cut below the top-most chain must cross another such chain. Each of these steps rests on plane topology: the existence of the outer region, the meaning of "top-most", and the fact that two chains with interleaved endpoints on a boundary must intersect, which is a form of the Jordan curve theorem.

The naive purely combinatorial route fails: the analogous statement for arbitrary networks is false (Fig. 2), so any argument has to use the drawing somewhere. Replacing the drawing by a combinatorial embedding (rotation systems, faces) is possible but then requires proving that the two notions agree, which is again Jordan-curve territory.

Formalization scope

Conventions committed to in the Lean statements:

Vertices and arcs are finite types V, E with decidable equality. Arcs are undirected, may be parallel, and have two distinct end vertices. Source and sink are distinct, capacities are positive (structure Network).
A chain is a Finset E that is the arc set of some arrangement as a simple path (IsChainWalk, IsChain); the null chain is allowed.
IsDisconnecting and IsCut quantify over all chains joining source and sink; a cut is a disconnecting set no proper subset of which is disconnecting.
ab-planarity is a plane drawing of the graph with the extra arc indexed by none : Option E, with injective Paths in ℝ × ℝ as arcs.

Hypotheses of the goal: hno_ab, the standing assumption of §2 (no arc joins $a$ and $b$ , p. 403); hconn, that some chain joins $a$ and $b$ . The second is not stated in the paper; its proof starts from "the chain joining a and b which is top-most", which presupposes one, and without it the statement is false (if $a$ and $b$ are disconnected, the empty set is a cut and no chain exists).

The drawing structure is satisfiable (a three-vertex path network has an explicit drawing), so the planarity hypothesis is not vacuous; and it covers the added arc $ab$ and all crossings, so $K_{3,3}$ minus $ab$ is not ab-planar and the goal is not refuted by the paper's own example. A formalization that dropped the arc $ab$ from the drawing, or quantified over disconnecting sets instead of cuts, would state a false theorem and is ruled out.

A complete development needs basic plane topology for paths in $\mathbb R^2$ (a Jordan-curve-type separation lemma for simple closed curves, or an equivalent statement about crossing paths in a strip), together with combinatorial lemmas about chains (concatenation and shortcutting of chains at a common vertex). The topological lemmas are reusable well beyond this mission. Proofs through a combinatorial embedding are welcome, provided the equivalence with ABPlaneDrawing is proved.

Selected references

L. R. Ford, Jr. and D. R. Fulkerson, Maximal Flow Through a Network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
H. Whitney, Non-separable and planar graphs, Transactions of the American Mathematical Society 34 (1932), 339–362. https://doi.org/10.1090/S0002-9947-1932-1501641-2
A. Itai and Y. Shiloach, Maximum flow in planar networks, SIAM Journal on Computing 8 (1979), 135–150. https://doi.org/10.1137/0208012
H. Whitney, Planar graphs, Fundamenta Mathematicae 21 (1933), 73–84. https://doi.org/10.4064/fm-21-1-73-84

7 thms1 active userReviewed

Machine Learning Operations Research Reinforcement Learning·Captain: mikedeng1

Twice Regularized MDPs and the Equivalence Between Robustness and Regularization 2: The Greedy Policy of the R2 Optimal Value Is the Unique Optimal R2 PolicyResearch Paper

Motivation

A robust Markov decision process (robust MDP) evaluates a policy against the worst transition kernel and reward in an uncertainty set around a nominal model $(P_0, r_0)$ . It is the standard model for planning when the dynamics are estimated from data (Iyengar 2005; Nilim and El Ghaoui 2005; Wiesemann, Kuhn and Rustem 2013). Its Bellman update contains an inner optimization over the uncertainty set at every state, which makes robust planning costly when the sets are not $(s,a)$ -rectangular.

Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) show that, for $s$ -rectangular ball uncertainty sets, this inner optimization can be replaced by an explicit penalty that depends both on the policy and on the value function. The resulting twice regularized (R²) MDPs have Bellman operators with no inner optimization over models. The first mission of this series formalizes the robust–regularized equivalence (Theorem 4.1 of the paper). This mission formalizes Section 5: the R² Bellman operators are monotone and contracting under a bound on the transition radius, and the greedy policy of the R² optimal value is optimal.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite nonempty sets of states and actions, $\gamma\in(0,1)$ a discount factor, $P_0(s'\mid s,a)$ a transition kernel and $r_0(s,a)$ a reward. A policy $\pi\in\Delta_{\mathcal A}^{\mathcal S}$ assigns to each state a probability distribution $\pi_s$ on $\mathcal A$ . For $v\in\mathbb R^{\mathcal S}$ write $q_s(a)=r_0(s,a)+\gamma\sum_{s'}P_0(s'\mid s,a)v(s')$ and

[T^\pi_{(P_0,r_0)}v](s)=\sum_a\pi_s(a)\,q_s(a).

All norms $\|\cdot\|$ below are $\ell_2$ -norms, $\|a\|=\big(\sum_z a(z)^2\big)^{1/2}$ ; $\|\cdot\|_\infty$ is the sup norm.

Fix nonnegative radii $\alpha^r_s,\alpha^P_s$ for each state. The R² regularizer is $\Omega_{v,\mathrm R^2}(\pi_s)=\|\pi_s\|\,(\alpha^r_s+\alpha^P_s\gamma\|v\|)$ , and the R² Bellman operators are

[T^{\pi,\mathrm R^2}v](s)=[T^\pi_{(P_0,r_0)}v](s)-\Omega_{v,\mathrm R^2}(\pi_s),\qquad [T^{*,\mathrm R^2}v](s)=\max_{\pi\in\Delta^{\mathcal S}_{\mathcal A}}[T^{\pi,\mathrm R^2}v](s).

A policy $\pi$ is greedy for $v$ when $T^{\pi,\mathrm R^2}v=T^{*,\mathrm R^2}v$ .

Assumption 5.1 (bounded radius). For each $s$ there is $\epsilon_s>0$ with

\alpha^P_s\le\min\Big(\frac{1-\gamma-\epsilon_s}{\gamma\sqrt{|\mathcal S|}}\ ;\ \min_{u\in\mathbb R^{\mathcal A}_+,\|u\|=1,\ w\in\mathbb R^{\mathcal S}_+,\|w\|=1}\ \sum_{a,s'}u(a)P_0(s'\mid s,a)w(s')\Big),

and $\epsilon_*=\min_s\epsilon_s$ . The R² value function $v^{\pi,\mathrm R^2}$ of a policy and the R² optimal value $v^{*,\mathrm R^2}$ are the fixed points of $T^{\pi,\mathrm R^2}$ and $T^{*,\mathrm R^2}$ .

Formalization targets

Goal: Theorem 5.1 (p. 8)

Under Assumption 5.1, $T^{*,\mathrm R^2}$ and every $T^{\pi,\mathrm R^2}$ have unique fixed points; a greedy policy $\pi^{*,\mathrm R^2}$ for $v^{*,\mathrm R^2}$ exists, and every such policy satisfies

v^{\pi^{*,\mathrm R^2},\mathrm R^2}=v^{*,\mathrm R^2}\ \ge\ v^{\pi,\mathrm R^2}\qquad\text{for all }\pi\in\Delta^{\mathcal S}_{\mathcal A};

every optimal policy is greedy; and when $\alpha^r_s>0$ for all $s$ the greedy policy is unique, hence the unique optimal R² policy.

Milestones

Proposition 2.1 (p. 3): for $\Omega$ strongly convex on the simplex, $\Omega^*(y)=\max_{a\in\Delta}\langle a,y\rangle-\Omega(a)$ is differentiable with Lipschitz gradient equal to the unique maximizer, satisfies $\Omega^*(y+c\mathbb 1)=\Omega^*(y)+c$ , and is non-decreasing.
Proposition 5.1 (i) (p. 8): $v_1\le v_2$ implies $T^{\pi,\mathrm R^2}v_1\le T^{\pi,\mathrm R^2}v_2$ and $T^{*,\mathrm R^2}v_1\le T^{*,\mathrm R^2}v_2$ .
Proposition 5.1 (iii) (p. 8):

\|T^{\pi,\mathrm R^2}v_1-T^{\pi,\mathrm R^2}v_2\|_\infty\le(1-\epsilon_*)\|v_1-v_2\|_\infty,\qquad \|T^{*,\mathrm R^2}v_1-T^{*,\mathrm R^2}v_2\|_\infty\le(1-\epsilon_*)\|v_1-v_2\|_\infty.

Significance

Theorem 5.1 is the R² counterpart of the fundamental theorem of discounted dynamic programming: optimal R² values are achieved by stationary policies obtained by a single greedy step. Together with the contraction of Proposition 5.1 (iii) it justifies the R² modified policy iteration algorithm of the paper, whose greedy step is a projection onto the simplex rather than a robust max–min problem. Combined with the first mission of the series, which identifies the robust value of an $s$ -rectangular ball-constrained MDP with the optimum of an R²-regularized program, it gives a route to robust planning at the cost of regularized planning.

The results are proved in the paper (App. C), partly by reference to Geist, Scherrer and Pietquin (2019) for the optimality operator. No machine-checked proof of any of them exists; this mission produces the first. Prop. 2.1 is a general fact of convex analysis (Danskin-type smoothness of a conjugate on the simplex) that is reusable for any regularized MDP or entropy-regularized game.

Difficulty

The R² evaluation operator is not affine: the value regularizer $-\alpha^P_s\gamma\|\pi_s\|\,\|v\|$ is concave in $v$ and decreases as $\|v\|$ grows. Monotonicity therefore does not follow from the positivity of $P_0$ as in the standard case; it requires the second bound of Assumption 5.1, which compares the $\ell_2$ variation of $\|v\|$ with the minimal nonnegative bilinear form of $P_0(\cdot\mid s,\cdot)$ . Likewise the contraction modulus is not $\gamma$ but $1-\epsilon_*$ , because the regularizer is $\sqrt{|\mathcal S|}$ -Lipschitz between the $\ell_2$ and sup norms. The optimality step of the classical proof uses linearity of $T^\pi$ when comparing values of policies; here only monotonicity and contraction are available. Uniqueness of the greedy policy rests on strict concavity on the simplex, which holds only when the regularization weight is positive.

Formalization scope

States and actions are finite nonempty types; transitions are arrays P₀ : S → A → S → ℝ with the published predicate IsTransitionKernel; value functions are S → ℝ with the pointwise order. The $\ell_2$ -norm is an explicit l2norm (Mathlib's norm on S → ℝ is the sup norm, used only for $\|\cdot\|_\infty$ ). $T^{*,\mathrm R^2}v(s)$ is the real supremum over the simplex $\Delta_{\mathcal A}$ (attained), and the inner minimum of Assumption 5.1 is the real infimum over nonnegative $\ell_2$ -unit vectors; the witnesses $\epsilon_s$ are explicit. Greedy policies are a predicate, never a function, and the R² value functions are not defined by choice: the goal asserts their existence and uniqueness and speaks about the fixed points.

Disclosed deviations from the page. Assumption 5.1 is a hypothesis of Theorem 5.1 (its proof assumes it). The uniqueness clause of Theorem 5.1 additionally assumes $\alpha^r_s>0$ for all $s$ : with one state, two actions, zero reward and zero radii every policy is greedy and optimal. Proposition 2.1 assumes $\Omega$ continuous on the simplex, without which the maximum need not be attained, and strong convexity is Mathlib's StrongConvexOn for some modulus (norm-independent in finite dimension). Proposition 5.1 (ii) is false as printed and is not drafted: with one state, one action, $P_0=1$ , $r_0=0$ , $\gamma=1/2$ , $\alpha^r=0$ , $\alpha^P=1/2$ , $\epsilon=1/4$ , one has $Tv=v/2-|v|/4$ , and $v_1=-1$ , $c=1$ give $T(v_1+c)=0>-1/4=Tv_1+\gamma c$ . Remark 5.1, Algorithm 1 and the $\ell_p$ variant of App. C.1 are out of scope. The inner minimum of Assumption 5.1 is $0$ whenever some $P_0(s'\mid s,a)=0$ , forcing $\alpha^P_s=0$ ; this is the assumption as printed.

A formalization in which $\|\cdot\|$ is the sup norm, the inner minimum ranges over all unit vectors (making the assumption unsatisfiable), or the value functions are postulated rather than shown to exist would be trivial or wrong; the drafted statements avoid all three. Contributions welcome: Prop. 2.1 as a general convex-analysis lemma, Banach fixed-point plumbing for S → ℝ with the sup norm, and the strict concavity of $p\mapsto\langle p,q\rangle-c\|p\|$ on the simplex.

Selected references

E. Derman, M. Geist, S. Mannor, Twice regularized MDPs and the equivalence between robustness and regularization, NeurIPS 2021. arXiv:2110.06267v1
M. Geist, B. Scherrer, O. Pietquin, A theory of regularized Markov decision processes, ICML 2019. arXiv:1901.11275
A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. doi:10.1287/opre.1050.0216
G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. doi:10.1287/moor.1040.0129
W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov decision processes, Mathematics of Operations Research 38(1), 2013. doi:10.1287/moor.1120.0566
A. Mensch, M. Blondel, Differentiable dynamic programming for structured prediction and attention, ICML 2018. arXiv:1802.03676

9 thms1 active userReviewed

Analysis Differential Geometry·Captain: mikedeng1

Projection-like Retractions on Matrix Manifolds I: Coming Back to a Submanifold Along a Smooth Field of Transverse Subspaces Defines a RetractionResearch Paper

Motivation

Iterative methods for optimization and equation solving on a smooth constraint set $\mathcal M$ (orthogonal matrices, fixed-rank matrices, spheres, Stiefel and Grassmann manifolds) compute an update vector $u$ in the tangent space at the current iterate $x$ and then have to return to $\mathcal M$ . The Riemannian exponential map does this along geodesics, but computing it means solving an ordinary differential equation. The notion of retraction, introduced by Adler, Dedieu, Margulies, Martens and Shub (IMA J. Numer. Anal., 2002) and developed in the book of Absil, Mahony and Sepulchre (Princeton, 2008), captures what such a return map needs for Newton's method to keep its local quadratic convergence and for gradient methods to converge: smoothness, $R(x,0)=x$ , and first-order agreement with the exponential.

Absil and Malick (SIAM J. Optim., 2012; HAL hal-00651608v2) give a general recipe for building retractions on submanifolds of a Euclidean space: move tangentially from $x$ to $x+u$ , then come back to $\mathcal M$ along a prescribed family of admissible directions. This mission formalizes that recipe, Theorem 4.2 of the paper ("retractors give retractions"), together with the two lemmas its proof rests on.

Setting

Let $\mathcal E$ be a Euclidean space of dimension $n$ (in the paper's examples, $\mathbb R^{n\times m}$ with the Frobenius inner product). A set $\mathcal M\subseteq\mathcal E$ is a $C^k$ submanifold of dimension $d$ if around every $\bar x\in\mathcal M$ it is a coordinate slice: there are an open neighbourhood $\mathcal U$ of $\bar x$ and a $C^k$ diffeomorphism $\phi$ of $\mathcal U$ onto an open subset of $\mathbb R^n$ with $\mathcal M\cap\mathcal U=\{x\in\mathcal U:\phi_{d+1}(x)=\dots=\phi_n(x)=0\}$ . Throughout, $k\ge2$ .

The tangent space $\mathrm T_{\mathcal M}(x)$ is the linear subspace of $\mathcal E$ of tangent directions of $\mathcal M$ at $x$ , the normal space $\mathrm N_{\mathcal M}(x)$ is its orthogonal complement, and the tangent bundle is $\mathrm T\mathcal M=\{(x,u):x\in\mathcal M,\ u\in\mathrm T_{\mathcal M}(x)\}$ .

A map $R$ from $\mathrm T\mathcal M$ to $\mathcal M$ is a retraction around $\bar x$ (Definition 2.1) if, on a neighbourhood $\mathcal U$ of $(\bar x,0)$ in $\mathrm T\mathcal M$ , it is of class $C^{k-1}$ , satisfies $R(x,0)=x$ , and $u\mapsto R(x,u)$ has derivative $\mathrm{id}_{\mathrm T_{\mathcal M}(x)}$ at $u=0$ . It is a retraction on $\mathcal M$ if this holds around every point.

A retractor (Definition 4.1) is a $C^{k-1}$ map $D$ , defined on a neighbourhood of the zero section of $\mathrm T\mathcal M$ , with values in the Grassmann manifold $\mathrm{Gr}(n-d,\mathcal E)$ of $(n-d)$ -dimensional linear subspaces, such that $D(x,0)\cap\mathrm T_{\mathcal M}(x)=\{0\}$ for every $x\in\mathcal M$ . Given $D$ , set $\mathcal D(x,u)=x+u+D(x,u)$ and let

R(x,u)=\{\text{points of }\mathcal M\cap\mathcal D(x,u)\text{ nearest to }x+u\}.

Formalization targets

Goal: Theorem 4.2 (retractors give retractions)

\forall\bar x\in\mathcal M\ \ \exists r:\quad R(x,u)=\{r(x,u)\}\ \text{ for }(x,u)\in\mathrm T\mathcal M\text{ near }(\bar x,0),\quad\text{and } r \text{ is a retraction around } \bar x.

The theorem asserts both that the point-to-set map $R$ is single-valued near the zero section and that it is a retraction there.

Milestone: Lemma 4.7 (the normal case $D(x,u)=\mathrm N_{\mathcal M}(x)$ )

Near $(\bar x,0)$ there is one and only one smallest $v(x,u)\in\mathrm N_{\mathcal M}(x)$ with $x+u+v(x,u)\in\mathcal M$ ; $\mathrm D_u v(x,0)=0$ ; and $R(x,u)=x+u+v(x,u)$ is a retraction around $\bar x$ , hence on $\mathcal M$ .

Milestone: Lemma 4.8 (straightening up)

On a neighbourhood of the zero section, $D(x,u)=\{v+A(x,u)v:\ v\in\mathrm N_{\mathcal M}(x)\}$ for a unique linear $A(x,u):\mathrm N_{\mathcal M}(x)\to\mathrm T_{\mathcal M}(x)$ depending $C^{k-1}$ on $(x,u)$ .

Further: Theorem 4.9 (second order)

If $k\ge3$ and $D(x,0)=\mathrm N_{\mathcal M}(x)$ for all $x\in\mathcal M$ , then $\frac{\mathrm d^2}{\mathrm dt^2}R(x,tu)|_{t=0}\in\mathrm N_{\mathcal M}(x)$ for all $(x,u)\in\mathrm T\mathcal M$ .

Significance

Theorem 4.2 reduces the construction of a retraction to the choice of a smooth field of subspaces transverse to the tangent space at $u=0$ . The orthographic retraction ( $D=\mathrm N_{\mathcal M}(x)$ ) and the projective retraction $R(x,u)=P_{\mathcal M}(x+u)$ ( $D=\mathrm N_{\mathcal M}(P_{\mathcal M}(x+u))$ ) are both instances, as are the gnomonic, orthographic and stereographic projections on the sphere. Theorem 4.9 then certifies, by a check at $u=0$ only, that a retraction agrees with the exponential to second order, which matters for the superlinear convergence of Riemannian trust-region and Newton methods. Lemma 4.7 goes beyond an earlier result on tangential parameterizations (reference [28, Th. 3.4] of the paper) by giving $C^{k-1}$ regularity jointly in $(x,u)$ , not only in $u$ (Remark 4.4 of the paper).

The results are proved in the paper. None of them is machine-checked: Mathlib has the implicit function theorem and smooth manifolds, but no embedded submanifolds of a Euclidean space with their tangent and normal bundles, no retractions, and no smooth Grassmannian-valued maps. The work here is to formalize the known proof and to build this layer, which every later mission of this series (projective, spectral, fixed-rank and Stiefel retractions) also needs.

Difficulty

The statement is an implicit-function argument, but the obvious one does not apply directly. The unknown $v$ lives in the normal space $\mathrm N_{\mathcal M}(x)$ , which moves with $x$ , and $(x,u)$ ranges over the tangent bundle, a $C^{k-1}$ submanifold of $\mathcal E\times\mathcal E$ rather than an open set of a vector space. The equation has to be read in charts of the bundle, which costs one derivative; the uniqueness given by the implicit function theorem holds only locally in $(x,u,v)$ , and turning it into "the smallest $v$ ", or "the nearest point of $\mathcal M\cap\mathcal D(x,u)$ ", requires excluding far-away intersection points. For a general retractor, the subspace $D(x,u)$ also moves, and has to be written as a graph over the normal space with a $C^{k-1}$ dependence before a second implicit-function argument applies.

Formalization scope

$\mathcal E$ is a finite-dimensional real inner product space E, $n$ is Module.finrank ℝ E, and $k,d$ are natural numbers with $2\le k$ and $d\le n$ (the latter inside the submanifold definition). The coordinate slice uses an open partial homeomorphism E → EuclideanSpace ℝ (Fin n), $C^k$ in both directions, with 0-based coordinates. $\mathrm T_{\mathcal M}(x)$ is the span of Mathlib's tangent cone (chart-free), $\mathrm N_{\mathcal M}(x)$ its orthogonal complement. Retractions and retractors are total maps on $\mathcal E\times\mathcal E$ constrained only on $O\cap\mathrm T\mathcal M$ with $O$ open; "of class $C^{k-1}$ on a subset of $\mathrm T\mathcal M$ " is ContDiffOn on that set. A Grassmannian-valued map is $C^{k-1}$ when its orthogonal projector $P_{D(x,u)}$ is, and the dimension $n-d$ of $D(x,u)$ is part of the definition. The set-valued $R$ uses the published nearest-point predicate RandomGradFree.Nonsmooth.IsMetricProjection. In Lemma 4.8, $A(x,u)$ is extended by $0$ on $\mathrm T_{\mathcal M}(x)$ so that it is an operator on $\mathcal E$ . Theorem 4.9 assumes $k\ge3$ , the standing assumption of the definition of second-order retractions (display (2.3)), and reads the page's " $D(\bar x,0)=\mathrm N_{\mathcal M}(x)$ " as $D(x,0)=\mathrm N_{\mathcal M}(x)$ for all $x\in\mathcal M$ .

The goal is not satisfied by exhibiting some retraction: it requires the nearest-point set $R(x,u)$ to equal a singleton $\{r(x,u)\}$ (so it is nonempty) and that very $r$ to be a retraction. Theorem 4.9 requires the curve $t\mapsto R(x,tu)$ to be twice differentiable, so a junk second derivative of $0$ does not satisfy it.

A complete development needs: finite-rank facts for tangent spaces of slices ( $\dim\mathrm T_{\mathcal M}(x)=d$ ), smoothness of $x\mapsto P_{\mathrm N_{\mathcal M}(x)}$ , charts of $\mathrm T\mathcal M$ and of the Whitney sum $\mathrm T\mathcal M\oplus\mathrm N\mathcal M$ , ContDiffOn on submanifolds, and local orthonormal frames of a smooth field of subspaces. All of these are reusable beyond this mission. Contributions to any of them, and proofs of the two lemmas, are welcome.

Selected references

P.-A. Absil, J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 (authors' version: https://hal.science/hal-00651608)
P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://press.princeton.edu/absil
R. L. Adler, J.-P. Dedieu, J. Y. Margulies, M. Martens, M. Shub, Newton's method on Riemannian manifolds and a geometric model for the human spine, IMA J. Numer. Anal. 22(3):359–390, 2002. https://doi.org/10.1093/imanum/22.3.359

10 thms1 active userReviewed

Analysis Dynamical Systems Operations Research·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems III: Bounded Subgradient Trajectories Converge with Łojasiewicz RatesResearch Paper

Motivation

Many optimization algorithms are discretizations of a continuous-time descent: the gradient flow $\dot x=-\nabla f(x)$ for smooth objectives, and its nonsmooth analogue, the subgradient dynamical system, for objectives with kinks or constraints. A basic question about such a flow is whether a bounded trajectory actually converges, rather than merely accumulating on a continuum of critical points, and how fast. For real-analytic $f$ this was settled by Łojasiewicz through his gradient inequality, which forces bounded gradient trajectories to have finite length. Without some such structure the answer is negative: there are smooth functions whose bounded gradient trajectories spiral forever around a circle of critical points.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the Łojasiewicz inequality to nonsmooth subanalytic functions, possibly taking the value $+\infty$ , by replacing $\|\nabla f\|$ with the least norm of a limiting subgradient. Section 4 of the paper turns this inequality into convergence results for subgradient trajectories of convex and lower- $C^2$ functions. This mission formalizes that section. The same "Łojasiewicz argument" later became the Kurdyka–Łojasiewicz framework behind convergence proofs for proximal, alternating and splitting algorithms (Attouch–Bolte 2009; Bolte–Sabach–Teboulle 2014).

Timeline. Łojasiewicz (1963, 1984) proved the gradient inequality for real-analytic functions and finite length of bounded analytic gradient trajectories. Kurdyka (Ann. Inst. Fourier 1998) extended it to $C^1$ functions definable in an o-minimal structure. Kurdyka, Mostowski and Parusiński (2000) proved Thom's gradient conjecture for analytic functions. Bolte, Daniilidis and Lewis (2007) gave the nonsmooth subanalytic version and the trajectory results formalized here.

Setting

Let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$ . The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y\to x,\,y\neq x}\big(f(y)-f(x)-\langle x^*,y-x\rangle\big)/\|y-x\|\ge0$ . The limiting subdifferential $\partial f(x)$ is the set of limits of $x_k^*\in\hat\partial f(x_k)$ with $x_k\to x$ and $f(x_k)\to f(x)$ . The nonsmooth slope is $m_f(x)=\inf\{\|x^*\|: x^*\in\partial f(x)\}$ , equal to $+\infty$ when $\partial f(x)=\emptyset$ , and $\operatorname{crit} f=\{x: 0\in\partial f(x)\}$ is the set of critical points.

The standing assumptions of Section 4 are:

$(\mathcal H1)$ $f$ is either lower semicontinuous and convex, or lower- $C^2$ with $\operatorname{dom} f=\mathbb R^n$ . Lower- $C^2$ means that near each point $f=\max_{s\in S}F(\cdot,s)$ for a compact space $S$ and a jointly continuous $F$ with jointly continuous first and second $x$ -derivatives.
$(\mathcal H2)$ $f$ is somewhere finite and bounded from below.
$(\mathcal H3)$ $f$ is subanalytic: its graph is locally the projection of a bounded set defined by finitely many real-analytic equalities and strict inequalities.

A trajectory of the subgradient system $(\mathcal G)$ is an absolutely continuous curve $x:[0,T)\to\mathbb R^n$ , $T\in(0,+\infty]$ , with $\dot x(t)+\partial f(x(t))\ni0$ for almost every $t$ and $\partial f(x(t))\neq\emptyset$ for every $t$ . It is maximal if it admits no extension to a longer interval. The Łojasiewicz inequality holds around $a$ with exponent $\theta$ if $|f-f(a)|^\theta/m_f$ is bounded near $a$ , with $0^0=1$ and $\infty/\infty=0/0=0$ . A Łojasiewicz exponent at $a\in\operatorname{dom} f$ is any such $\theta\in[0,1)$ .

Formalization targets

Goal: Theorem 4.7

Under $(\mathcal H1)$ – $(\mathcal H3)$ , every bounded maximal trajectory $x$ is defined on $[0,+\infty)$ and converges to a critical point $a$ . For every Łojasiewicz exponent $\theta$ at $a$ there are $k,k'>0$ and $t_0\ge0$ such that for $t\ge t_0$

\|x(t)-a\|\le \begin{cases} k\,(t+1)^{-\frac{1-\theta}{2\theta-1}}, & \theta\in(\tfrac12,1),\\[2pt] k\,e^{-k't}, & \theta=\tfrac12,\end{cases}

and for $\theta\in[0,\tfrac12)$ , $x(t)=a$ for all large $t$ . The constants are existential, so the goal survives any later sharpening of them.

Milestones

Corollary 4.1(i): for almost every $t$ , $\frac{d}{dt}f(x(t))=\langle\dot x(t),x^*\rangle$ for every $x^*\in\partial f(x(t))$ .
Corollary 4.1(iii): every trajectory extends to a maximal one on $[0,+\infty)$ with $\dot x\in L^2$ .
Corollary 4.2: $\|\dot x(t)\|=m_f(x(t))$ and $\frac{d}{dt}f(x(t))=-m_f(x(t))^2$ almost everywhere.
Inequality (20): the Łojasiewicz inequality holds around every point of $\operatorname{dom}\partial f$ .
Theorem 4.5: bounded maximal trajectories have finite length $\int_0^\infty\|\dot x\|<\infty$ and converge to a critical point.
The tail bound $\int_t^\infty\|\dot x\|\le\frac{c}{1-\theta}(f(x(t))-f(a))^{1-\theta}$ .
Inequality (27): $\int_t^\infty\|\dot x\|\le\frac{c^{1/\theta}}{1-\theta}\|\dot x(t)\|^{(1-\theta)/\theta}$ for almost every large $t$ .

Significance

Theorem 4.5 says that for convex or lower- $C^2$ subanalytic objectives, including constrained problems through indicator functions of subanalytic sets, the subgradient flow never oscillates indefinitely: bounded trajectories converge to one critical point. Theorem 4.7 adds rates that depend only on the Łojasiewicz exponent at the limit: exponential at $\theta=\tfrac12$ , polynomial above it, finite time below it. These are continuous-time templates for the convergence analyses of proximal and splitting methods under the Kurdyka–Łojasiewicz property.

On the formalization side, the results are proved on paper but, to our knowledge, not formalized in any proof assistant. A development would provide reusable infrastructure: a Lean notion of a trajectory of a differential inclusion on $[0,T)$ , a chain rule for $f\circ x$ along absolutely continuous curves, and a comparison lemma for the differential inequality $\dot\sigma\le-L\sigma^\alpha$ . The analysis of Section 4 uses subanalyticity only through inequality (20), so Theorems 4.5 and 4.7 can be attacked with (20) as an imported milestone, independently of the subanalytic geometry.

Difficulty

Compactness gives cluster points of a bounded trajectory, and the decrease of $f$ gives convergence of $f(x(t))$ . Neither gives convergence of $x(t)$ . The usual first idea, that $\int_0^\infty\|\dot x\|^2<\infty$ forces convergence, fails, since square-integrable speed allows infinite length. The difficulty is to control $\int\|\dot x\|$ rather than $\int\|\dot x\|^2$ . That needs a lower bound on the slope in terms of the function gap near the cluster point, which is exactly what (20) supplies, plus a trapping argument showing the tail of the trajectory stays in the ball where (20) holds. In the nonsmooth setting the chain rule itself is nontrivial: $f\circ x$ is differentiable almost everywhere with derivative $\langle\dot x,x^*\rangle$ for every $x^*\in\partial f(x(t))$ , which relies on $\partial f=\hat\partial f$ for convex and lower- $C^2$ functions. Global existence on $[0,+\infty)$ (Corollary 4.1(iii)) must also be established before any asymptotic statement makes sense.

Formalization scope

Space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "bounded from below" by a real number excludes $-\infty$ . The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff, and convexity is the published MoreauProx.Characterization.EConvex (convex epigraph). The slope $m_f$ is valued in $[0,+\infty]$ . The Łojasiewicz inequality is encoded as $|f(y)-f(a)|^\theta\le C\|v\|$ for $y$ near $a$ and every $v\in\partial f(y)$ , which is the bounded ratio under the paper's conventions. Times are real numbers and $T\in[0,+\infty]$ . Curves are functions $\mathbb R\to\mathbb R^n$ whose values outside $[0,T)$ are irrelevant. "Absolutely continuous on $[0,T)$ " means absolutely continuous on every compact $[0,b]\subseteq[0,T)$ . Velocities appear only "for almost every $t$ ". Lengths are lower Lebesgue integrals $\int^-\|\dot x\|$ in $[0,+\infty]$ , never Bochner integrals (which would vanish for a non-integrable speed).

Two trivializations are ruled out. Maximality is a hypothesis and $T=+\infty$ is a conclusion: assuming $T=+\infty$ would narrow the theorem, and dropping maximality would make it false. Rates are claimed for every Łojasiewicz exponent at the limit, not for one chosen exponent. Corollary 4.1(iii) is stated as "defined on $\mathbb R_+$ with $\dot{\hat x}\in L^2$ ", because the printed $\hat x\in W^{1,2}(\mathbb R_+)$ would fail for any trajectory with nonzero limit.

Needed infrastructure: absolutely continuous curves and their a.e. derivatives (Mathlib's AbsolutelyContinuousOnInterval), chain rules for convex and lower- $C^2$ functions, existence and uniqueness for monotone differential inclusions (Brézis), and an ODE comparison principle. Contributions to any of these are reusable well beyond this mission.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4) (2007) 1205–1223. https://doi.org/10.1137/050644641
H. Brézis, Opérateurs maximaux monotones et semi-groupes de contractions dans les espaces de Hilbert, North-Holland, 1973.
J.-P. Aubin, A. Cellina, Differential Inclusions, Springer, 1984. https://doi.org/10.1007/978-3-642-69512-4
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116 (2009) 5–16. https://doi.org/10.1007/s10107-007-0133-5

17 thms1 active userReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Asymptotic Behavior of Statistical Estimators and of Optimal Solutions of Stochastic Optimization Problems: Optimal Solutions Under Estimated Distributions Are Strongly ConsistentResearch Paper

Motivation

Many estimation procedures in statistics, and most stochastic optimization models in operations research, have the same shape: a decision or parameter $x\in\mathbb R^n$ is chosen to minimize an expected loss $Ef(x)=\int f(x,\xi)\,P(d\xi)$ under a distribution $P$ that is not known. In practice $P$ is replaced by an estimate $P^\nu$ built from the information available at stage $\nu$ (an empirical measure, a smoothed or parametric fit, a Bayesian posterior), and the minimizer of the estimated problem is used in place of the true one. The basic question is whether this is justified: do the estimated solutions converge to a true solution, and the estimated optimal values to the true optimal value, as information accumulates?

For maximum likelihood this is Wald's consistency theorem (Wald 1949); Huber extended it to M-estimators under non-standard conditions (Huber 1967). Both settings are unconstrained, or constrained to an open set, and assume finite-valued criteria. Constrained least squares, $L^1$ and Huber regression with inequality constraints, variance-component models with Heywood cases, and two-stage stochastic programs with recourse all lead instead to criteria that take the value $+\infty$ off a closed feasible set and are only lower semicontinuous in $x$ .

J. Dupačová and R. Wets (IIASA WP-86-41, 1986; journal version Ann. Statist. 16 (1988)) proved consistency in this generality by combining epi-convergence of functions with the theory of measurable multifunctions and normal integrands. This mission formalizes their §3.

Setting

$\Xi$ is a Polish space with its Borel $\sigma$ -field and $P$ is a probability measure on it. The integrand is $f:\mathbb R^n\times\Xi\to(-\infty,\infty]$ , and the true problem is to minimize

Ef(x)=\int_\Xi f(x,\xi)\,P(d\xi),

with the convention that $Ef(x)=+\infty$ whenever $\xi\mapsto f(x,\xi)$ is not bounded above by a summable function. The effective domain of a function $h:\mathbb R^n\to[-\infty,\infty]$ is $\operatorname{dom}h=\{x: h(x)<\infty\}$ , and $\operatorname{argmin}h=\{x: h(x)=\inf h\}$ .

Information arrives on a probability space $(Z,\mathcal F,\mu)$ with an increasing sequence of $\sigma$ -fields $\mathcal F^1\subseteq\mathcal F^2\subseteq\dots\subseteq\mathcal F$ . Each sample $\zeta\in Z$ yields probability measures $P^\nu(\cdot,\zeta)$ on $\Xi$ , and $\zeta\mapsto P^\nu(A,\zeta)$ is $\mathcal F^\nu$ -measurable for every Borel $A$ : the estimate at stage $\nu$ uses only stage- $\nu$ information. The estimated problem minimizes

E^\nu f(x,\zeta)=\int_\Xi f(x,\xi)\,P^\nu(d\xi,\zeta).

A sequence $g^\nu$ epi-converges to $g$ if, at every $x$ , $\liminf g^\nu(x^\nu)\ge g(x)$ along every sequence $x^\nu\to x$ , and $\limsup g^\nu(x^\nu)\le g(x)$ along some sequence $x^\nu\to x$ .

The standing hypotheses are Assumption 3.4: $\operatorname{dom}f=S\times\Xi$ with $S$ closed and nonempty; $f(x,\cdot)$ is continuous for $x\in S$ ; $f(\cdot,\xi)$ is lower semicontinuous; and $f$ is locally lower Lipschitz on $S$ with a bounded continuous modulus $\beta(\xi)$ . Assumption 3.5 asks that, for $\mu$ -almost every $\zeta$ , $P^\nu(\cdot,\zeta)$ converge in distribution to $P$ , that $|f(x,\cdot)|$ be uniformly tight along $P=P^0,P^1,\dots$ for each $x\in S$ , and that $\int\inf_x f(x,\xi)\,P^\nu(d\xi,\zeta)>-\infty$ for all $\nu$ .

Formalization targets

Goal: Theorem 3.9, "In particular" (pp. 21–22)

Let $D\subseteq\mathbb R^n$ be compact, suppose $(\operatorname{argmin}E^\nu f)\cap D\neq\emptyset$ $\mu$ -a.s. for every $\nu$ , and suppose $\{x^*\}=\operatorname{argmin}Ef\cap D$ . Then there are $\mathcal F^\nu$ -measurable selections $x^\nu$ of $\operatorname{argmin}E^\nu f$ with

x^\nu(\zeta)\to x^*\quad\text{and}\quad \inf E^\nu f(\cdot,\zeta)\to\inf Ef\qquad\text{for }\mu\text{-almost every }\zeta .

The goal does not assume that $Ef$ has a unique global minimizer, and it does not assume convexity.

Milestones

In attack order:

Proposition 3.3: epi-convergence gives $\limsup(\inf g^\nu)\le\inf g$ , limits of minimizers are minimizers, and the minimum is attained in the closure of a bounded $D$ .
Lemma 3.6: almost surely, $Ef$ and every $E^\nu f$ are proper and l.s.c., with domain $S$ .
Theorem 3.7: almost surely, $E^\nu f$ epi-converges and converges pointwise to $Ef$ .
Theorem 3.8: almost surely, the epigraphs of $E^\nu f$ are closed, and they depend $\mathcal F^\nu$ -measurably on $\zeta$ .
Theorem 3.9:
- (3.14) $\limsup(\inf E^\nu f)\le\inf Ef$ a.s.;
- (i) cluster points of estimated minimizers minimize $Ef$ ;
- (ii) $\zeta\mapsto\operatorname{argmin}E^\nu f(\cdot,\zeta)$ is closed-valued and $\mathcal F^\nu$ -measurable.
Proposition 3.1: the measurable selection theorem.

Significance

The result separates two things: the statistical input, which is only convergence in distribution of $P^\nu$ plus a tightness condition, and the variational output, which is convergence of optimal values and solutions. It therefore applies to any estimator $P^\nu$ that converges weakly almost surely: empirical measures, kernel estimates, parametric fits. It also covers constrained and nonsmooth problems: the feasible set enters through $f=+\infty$ off $S$ , and only lower semicontinuity in $x$ is required. Asymptotic distribution results for constrained estimators, such as the second part of the same paper and the subsequent literature on sample average approximation, start from this consistency.

The theorem is proved on paper. To the best of current knowledge none of it is machine-checked. Mathlib has weak convergence of probability measures, lower semicontinuity and extended-real integrals. It does not have epi-convergence, Effros-measurable multifunctions, normal integrands or the Kuratowski–Ryll-Nardzewski selection theorem. A formal proof produces these as reusable components. It also has to supply the details that the paper's proof of Theorem 3.8 leaves as a sketch.

Difficulty

Pointwise convergence $E^\nu f(x)\to Ef(x)$ is not enough to move minimizers to the limit, and uniform convergence fails because $f$ is $+\infty$ off $S$ and need not be bounded. Epi-convergence is the right notion. Proving it needs a liminf inequality along moving points $x^\nu\to x$ under moving measures $P^\nu$ . That combines Fatou's lemma, the lower Lipschitz bound and the tightness condition, and the integrands are extended-real-valued, so care is needed.

The second difficulty is measurability. The exceptional null set lies in $\mathcal F$ but not in $\mathcal F^\nu$ , so " $\mathcal F^\nu$ -measurable" has to be understood on a full-measure set in the trace $\sigma$ -field. The paper's argument for Theorem 3.8 appeals to continuity of $P\mapsto\operatorname{epi}E_Pf$ in the epi-topology, and it remarks itself that Theorem 3.7 gives this only along sequences satisfying Assumption 3.5. A solver will have to rebuild this step, for example through the normal-integrand structure of $E^\nu f$ .

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with its Euclidean norm.
$\Xi$ is a Polish space with its Borel $\sigma$ -algebra. This is exactly a closed subset of a Polish space with the relative Borel field.
$f$ is EReal-valued. Every expectation is the mission's expect: $+\infty$ when $\int f^+=\infty$ , and $\int f^+-\int f^-$ otherwise, both computed as Lebesgue integrals of $[0,\infty]$ -valued functions. A Bochner integral, which would assign $0$ to non-integrable functions, is never used for $Ef$ or $E^\nu f$ .
The sample index is shifted: Lean's Pν k and 𝔽 k are the paper's $P^{k+1}$ and $\mathcal F^{k+1}$ , and $P=P^0$ is a separate argument.
Infima, $\liminf$ and $\limsup$ are taken in $[-\infty,\infty]$ .
Measurability on the full-measure set $Z_0$ uses the trace $\sigma$ -field.
The selections in the goal are total, $\mathcal F^\nu$ -measurable maps $Z\to\mathbb R^n$ that select almost surely. This is equivalent to the paper's maps $Z_0\to\mathbb R^n$ .
"Random l.s.c. function" in Theorem 3.8 is encoded by the equivalent conditions (3.4i)–(3.4ii): nonempty, closed and measurable epigraphs.
Lower Lipschitz (3.10) is written additively.
The hypothesis that $\Xi$ is the support of $P$ is omitted. It is unused in §3, and omitting it strengthens every statement.
Nothing beyond the page is assumed: no convexity, no compact $S$ , no bounded $f$ , no unique minimizer, no i.i.d. sampling, no empirical $P^\nu$ , no completeness of $\mu$ or $\mathcal F^\nu$ .

The hypotheses are not vacuous. A sorry-free check verifies all of them, including those of the goal, for $f(x,\xi)=\|x\|^2$ with Dirac measures. Defining the expectation through a Bochner integral, or dropping $S\neq\emptyset$ (which makes every $\operatorname{argmin}$ all of $\mathbb R^n$ ), would trivialize or change the statements; the definitions above rule both out.

Contributions are welcome on any milestone. Proposition 3.1 (Kuratowski–Ryll-Nardzewski for $\mathbb R^m$ -valued multifunctions) and Proposition 3.3 (deterministic epi-convergence facts) are independent of the probabilistic setting and reusable beyond this mission.

Selected references

J. Dupačová, R. Wets, Asymptotic Behavior of Statistical Estimators and Optimal Solutions for Stochastic Optimization Problems, IIASA Working Paper WP-86-41, 1986. https://pure.iiasa.ac.at/id/eprint/2818/ — journal version: Ann. Statist. 16(4), 1517–1549, 1988. https://doi.org/10.1214/aos/1176351052
A. Wald, Note on the consistency of the maximum likelihood estimate, Ann. Math. Statist. 20, 595–601, 1949. https://doi.org/10.1214/aoms/1177729938
P. J. Huber, The behavior of maximum likelihood estimates under nonstandard conditions, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1, 221–233, 1967. https://projecteuclid.org/euclid.bsmsp/1200512988
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (Ch. 7 epi-convergence; Ch. 14 measurable multifunctions and normal integrands). https://doi.org/10.1007/978-3-642-02431-3

13 thms1 active userReviewed

Calculus of Variations Control Theory·Captain: mikedeng1

On the Variational Principle III: Every Terminal-Cost Control Problem Has ε-Optimal Measurable Controls Satisfying the Pontryagin Maximum Principle up to εResearch Paper

Motivation

The Pontryagin maximum principle is the basic first-order necessary condition of optimal control: along an optimal control, the control value at almost every time extremizes a Hamiltonian built from the dynamics and an adjoint vector. The classical statement presupposes that an optimal control exists. For many problems none does: the set of trajectories is not closed, or the cost does not attain its infimum, and the classical principle then says nothing.

Ekeland's 1974 paper On the Variational Principle (DOI 10.1016/0022-247X(74)90025-0) proves a general result about lower semicontinuous functions on complete metric spaces (its Theorem 1.1, now called Ekeland's variational principle) and closes with an application to control theory in §7 (pp. 348–351): for every terminal-cost problem satisfying mild regularity and growth conditions, there are ε-optimal controls that satisfy the maximum principle up to ε, whether or not an optimal control exists. The argument equips the measurable controls with the metric "measure of the set where two controls differ", which has since become a standard device in nonsmooth and approximate optimal control. For the classical theory, Ekeland refers to the treatise of Pallu de la Barrière (Optimal Control Theory, Saunders, 1967).

Setting

Fix $n \ge 0$ , a horizon $T > 0$ , an initial state $x_0 \in \mathbb R^n$ , and a nonempty compact metrizable space $K$ of control values, with its Borel σ-algebra. A control is a measurable map $u : [0, T] \to K$ . The dynamics are a map $f : \mathbb R^n \times K \times [0, T] \to \mathbb R^n$ , and the state obeys

\frac{dx}{dt}(t) = f(x(t), u(t), t) \ \text{ a.e.}, \qquad x(0) = x_0. \qquad (7.1)

A trajectory of $u$ (Lean: IsTrajectory f x₀ T u x) is a function $x$ continuous on $[0, T]$ with $x(t) = x_0 + \int_0^t f(x(s), u(s), s)\,ds$ for all $t \in [0, T]$ . The standing hypotheses are:

(a) $f$ and its state Jacobian $f_x' = (\partial f/\partial x_1, \dots, \partial f/\partial x_n)$ (Lean: fx) are continuous on $\mathbb R^n \times K \times [0, T]$ ;
(b) $\langle x, f(x, u, t)\rangle \le c\,(1 + \|x\|^2)$ for some constant $c$ .

The terminal cost is given by a $C^1$ function $g : \mathbb R^n \to \mathbb R$ , and the problem is to minimize $g(x(T))$ over all controls. The adjoint vector $p$ along a pair $(u, x)$ (Lean: IsAdjoint fx g T u x p) solves the linear equation

\frac{dp}{dt}(t) = -{}^t f_x'(x(t), u(t), t)\, p(t), \qquad p(T) = g'(x(T)),

where ${}^t A$ is the transpose. The control distance (Lean: ctrlDist T u₁ u₂) is

\delta(u_1, u_2) = \operatorname{meas}\{t \in [0, T] \mid u_1(t) \neq u_2(t)\},

and the needle variation $v_\tau$ of a control $u_\varepsilon$ at $t_0$ with value $u_0 \in K$ (Lean: needle T uε u₀ t₀ τ) equals $u_0$ on $[0, T] \cap\, ]t_0 - \tau, t_0[$ and $u_\varepsilon$ elsewhere.

Formalization targets

Goal: Theorem 7.1

For every $\varepsilon > 0$ there is a control $u_\varepsilon$ with trajectory $x_\varepsilon$ and adjoint vector $p_\varepsilon$ such that

g(x_\varepsilon(T)) \le \inf_u g(x(T)) + \varepsilon, \qquad \langle f(x_\varepsilon(t), u_\varepsilon(t), t), p_\varepsilon(t)\rangle \le \min_{w \in K} \langle f(x_\varepsilon(t), w, t), p_\varepsilon(t)\rangle + \varepsilon \ \text{ a.e. on } [0, T].

Milestones

(7.2), a priori bound: every trajectory satisfies $\|x(t)\|^2 \le (\|x_0\|^2 + 2cT)e^{2cT}$ .
Well-posedness (p. 348): every control has exactly one trajectory on $[0, T]$ .
Lemma 7.2: $(\mathcal U, \delta)$ is a complete metric space (on almost-everywhere classes).
Lemma 7.3: $u \mapsto g(x(T))$ is continuous on $(\mathcal U, \delta)$ .
(7.15)–(7.16): a control $u_\varepsilon$ with $F(u_\varepsilon) \le \inf F + \varepsilon^2$ and $F(u) \ge F(u_\varepsilon) - \varepsilon\,\delta(u, u_\varepsilon)$ for all $u$ , where $F(u) = g(x(T))$ .
Lemma 7.4: the right derivative of $\tau \mapsto g(x_\tau(T))$ at $\tau = 0$ , for the needle variations $v_\tau$ , equals $\langle f(x_\varepsilon(t_0), u_0, t_0) - f(x_\varepsilon(t_0), u_\varepsilon(t_0), t_0), p_\varepsilon(t_0)\rangle$ .

Significance

The result. Theorem 7.1 decouples the maximum principle from existence of optimal controls. Any minimizing sequence can be replaced by one consisting of controls that satisfy the necessary condition up to a vanishing error, so approximate extremals are available for numerical schemes and for limiting arguments (relaxation, convergence of extremals) in problems without compactness or convexity of the velocity sets. The same scheme, a complete metric on controls plus Ekeland's principle plus needle variations, underlies later proofs of the maximum principle with state constraints and in nonsmooth settings.

Formalizing it. The theorem has a published proof, which the paper sketches in four pages and partly defers to classical results (local existence for measurable controls, differentiability of trajectories with respect to needle variations). Neither Mathlib nor the platform contains this theorem or a maximum principle for measurable controls with time-dependent dynamics; the nearest platform items assume an exact optimum, a running cost and globally Lipschitz autonomous dynamics. A formalization requires a Carathéodory theory of ODEs in Lean, the complete metric space of controls, and a rigorous version of the classical first-variation computation. Each of these is useful well beyond this paper.

Difficulty

The obvious argument fails at its first step: a minimizing sequence of controls has no convergent subsequence in any useful sense, because measurable controls with values in $K$ are not compact in the metric $\delta$ and their weak limits are relaxed controls, which are not controls. Ekeland's principle avoids compactness, but it needs a complete metric space on which the cost is lower semicontinuous. Completeness of $(\mathcal U, \delta)$ (Lemma 7.2) and continuity of the cost (Lemma 7.3) both require care. Continuity must hold for trajectories driven by merely measurable controls, which converge only in measure. The needle derivative (Lemma 7.4) holds only at times where the trajectory satisfies the state equation in the classical sense, which is almost every time but not every time.

Formalization scope

Controls are functions ℝ → K with Measurable u; only values on $[0, T]$ matter. Trajectories and adjoint vectors are functions ℝ → EuclideanSpace ℝ (Fin n), continuous on $[0, T]$ and solving the integral form of their equation. The paper uses the same form in (7.13). A definition that asks for a derivative at every time would be unsatisfiable for discontinuous controls and would make the goal vacuous; the integral form avoids this.
Hypothesis (a) is stated as joint continuity of f and fx on univ ×ˢ univ ×ˢ Icc 0 T together with HasFDerivAt (fun y => f y u t) (fx x u t) x. Hypothesis (b) is ∃ c, … with the order of arguments $f(x, u, t)$ ; the page prints $f(t, x, u)$ in (b), a slip.
The transpose ${}^t f_x'$ is ContinuousLinearMap.adjoint, and $g'(x)$ is gradient g x.
Infima over controls are never taken as real ⨅; (7.4) and (7.15) are stated as "for every control $u$ with trajectory $x$ ".
(7.5) is printed with " $\times\,\varepsilon$ ". The proof's last line (7.21) gives " $+\,\varepsilon$ ", which is what is stated. The minimum over the compact $K$ is replaced by the equivalent "for every $w \in K$ ", with one null set for all $w$ .
Added hypothesis: [Nonempty K] in the goal and milestone 5. With $K$ empty no control exists and the existential statements would be false.
Lemma 7.2 is stated as the triangle inequality, " $\delta = 0$ iff almost-everywhere equality on $[0, T]$ ", and sequential completeness for measurable controls. Lemma 7.3 is sequential continuity. Lemma 7.4 is a one-sided derivative within $[0, t_0]$ at $0$ , stated for an arbitrary measurable $u_\varepsilon$ .
Theorem 1.1 (Ekeland's principle) is a separate mission of this series and still a draft, so milestone 5 states the instance used here directly.
Out of scope: the uniform bound (7.3) and the remark after Theorem 7.1 that one may take $\varepsilon = 0$ in (7.5) when (7.4) holds with $\varepsilon = 0$ .

Welcome contributions include Carathéodory existence and uniqueness for ODEs with measurable time dependence, Gronwall-type estimates for absolutely continuous functions, the complete metric space of measurable maps under the disagreement measure, and differentiability of flows with respect to initial data.

Selected references

I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974), 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979), 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
R. Pallu de la Barrière, Optimal Control Theory, Saunders, Philadelphia, 1967.
L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, New York, 1962.

11 thms1 active userReviewed

Functional Analysis Operations Research·Captain: mikedeng1

On the Variational Principle II: Under Linearly Independent Active Constraint Gradients, a Bounded-Below Problem Has ε²-Optimal Feasible Points Satisfying the Lagrange Multiplier Rule up to εResearch Paper

Motivation

The classical Lagrange multiplier rule and its inequality-constrained form, the Karush–Kuhn–Tucker (KKT) conditions, are necessary conditions satisfied at a minimizer of a constrained problem. In finite dimensions, a continuous function bounded below on a closed bounded feasible set attains its minimum, so the rule describes an actual point. In an infinite-dimensional Banach space this fails: closed bounded sets are not compact, minimizing sequences need not converge, and a smooth function bounded below on a smooth constraint set can have no minimizer at all. The multiplier rule then has nothing to describe.

Ekeland's 1974 paper On the Variational Principle (DOI) introduced a principle (its Theorem 1.1) that replaces "a minimizer exists" with "near every almost-minimizer there is a point that strictly minimizes a slightly perturbed function". Section 3 of the paper uses this to prove that, for a problem with finitely many smooth equality and inequality constraints satisfying a linear-independence regularity condition, nearly optimal feasible points satisfy the KKT conditions up to a small error, with no compactness and no existence of a minimizer. This is the first appearance of what is now called an approximate or asymptotic KKT condition, a notion central to the convergence theory of nonlinear programming algorithms.

Setting

Let $V$ be a real Banach space with dual $V^*$ (continuous linear functionals) and dual norm $\|x^*\|_*=\sup_{\|h\|\le1}\langle x^*,h\rangle$ . Let $F:V\to\mathbb R$ be Fréchet-differentiable, with derivative $F'(v)\in V^*$ , and let $G_1,\dots,G_m:V\to\mathbb R$ be $C^1$ (continuously Fréchet-differentiable). Fix $0\le p\le m$ and consider

\inf F(v)\quad\text{subject to}\quad G_i(v)=0\ (1\le i\le p),\qquad G_i(v)\ge0\ (p+1\le i\le m). \tag{3.1}

The feasible set is $\mathcal C=\{v\in V : G_i(v)=0 \text{ for } i\le p,\ G_i(v)\ge0 \text{ for } i>p\}$ (3.2). At $v\in\mathcal C$ the saturated constraints are $I(v)=\{i : G_i(v)=0\}$ (3.3). The regularity assumption (3.4) is: for every $v\in\mathcal C$ , the derivatives $G_i'(v)$ , $i\in I(v)$ , are linearly independent in $V^*$ .

In the Lean development these are EkelandVP.Constraints.feasibleSet p G and EkelandVP.Constraints.IsRegular p G, with constraints indexed by Fin m.

Formalization targets

Goal: Theorem 3.1 (p. 330)

Assume (3.4), $\mathcal C\ne\emptyset$ , and that $F$ is bounded below on $\mathcal C$ (3.5). Then for every $\varepsilon>0$ there are $v_\varepsilon\in\mathcal C$ and $\lambda_1,\dots,\lambda_m\in\mathbb R$ with

F(v_\varepsilon)\le\inf_{\mathcal C}F+\varepsilon^2,\qquad \lambda_i\ge0\ (i>p),\qquad \lambda_i=0 \text{ if } G_i(v_\varepsilon)\ne0,

\Big\|F'(v_\varepsilon)-\sum_{i=1}^m\lambda_iG_i'(v_\varepsilon)\Big\|_*\le\varepsilon.

Milestones, in the order of the paper's proof

(3.8)–(3.12): a feasible $v$ with $F(v)\le\inf_{\mathcal C}F+\varepsilon^2$ and $F(w)\ge F(v)-\varepsilon\|w-v\|$ for all $w\in\mathcal C$ (the variational principle applied to $F$ restricted to $\mathcal C$ ; no regularity needed).
(3.16): at a regular feasible point $v$ , every $h$ with $\langle G_i'(v),h\rangle=0$ ( $i\le p$ ) and $\langle G_i'(v),h\rangle\ge0$ ( $i>p$ , $i\in I(v)$ ) is the initial velocity of a $C^1$ curve $u:[0,\tau]\to\mathcal C$ with $u(0)=v$ .
Lemma 3.2: at a point with the property of milestone 1, $\langle F'(v),h\rangle\ge-\varepsilon\|h\|$ for every such $h$ .
Lemma 3.3: an $\varepsilon$ -Farkas–Minkowski lemma in $V^*$ : if $\langle w^*,h\rangle\ge-\varepsilon\|h\|$ whenever $\langle u_i^*,h\rangle=0$ and $\langle v_j^*,h\rangle\ge0$ , then $\|w^*-\sum\lambda_iu_i^*-\sum\mu_jv_j^*\|_*\le\varepsilon$ for some $\lambda_i\in\mathbb R$ and $\mu_j\ge0$ .

An additional item states Corollary 3.4 (p. 333), the one-constraint case: if $G(v)=0\Rightarrow G'(v)\ne0$ , $\{G=0\}\neq\emptyset$ and $F$ is bounded below on $\{G=0\}$ , then for every $\varepsilon>0$ there are $v_\varepsilon$ with $G(v_\varepsilon)=0$ and $\lambda_\varepsilon\in\mathbb R$ with $\|F'(v_\varepsilon)-\lambda_\varepsilon G'(v_\varepsilon)\|_*\le\varepsilon$ .

Significance

The result. Theorem 3.1 is an existence theorem for approximate KKT points that needs neither compactness nor attainment of the infimum. It shows that every bounded-below problem with regular constraints has a sequence of feasible points whose objective values converge to the infimum and along which the KKT residual tends to zero. This is the property that later work calls approximate KKT or asymptotic KKT (AKKT) and uses as a stopping criterion and as a sequential optimality condition for nonlinear programming. Corollary 3.4 is the corresponding nonlinear eigenvalue statement: on a regular level set, $F'$ is approximately proportional to $G'$ at almost-minimizing points.

Formalizing it. The result is classical and proved in the paper; to our knowledge no machine-checked version exists. Mathlib has the Fréchet derivative, the implicit function theorem for strictly differentiable maps, Banach–Alaoglu and the Hahn–Banach separation theorems, but no Ekeland principle in this form, no Lyusternik-type tangent-curve theorem for mixed equality–inequality constraints, and no Farkas lemma in a dual Banach space. Each milestone is a reusable piece of nonlinear optimization theory in Banach spaces.

Difficulty

The obvious argument, "take a minimizer and apply the Lagrange multiplier rule", fails at the first step because no minimizer need exist. The variational principle supplies a point $v_\varepsilon$ that minimizes $F+\varepsilon\|\cdot-v_\varepsilon\|$ on $\mathcal C$ , but that function is not differentiable at $v_\varepsilon$ , so the multiplier rule cannot be applied to it directly either. Two further gaps remain. Linearized feasible directions (those satisfying the derivative conditions on the active constraints) need not be directions along which one can actually move inside $\mathcal C$ ; closing this gap requires the regularity assumption and completeness of $V$ , and must keep the active inequality constraints nonnegative, not just the equalities. And the resulting first-order inequality, which holds only up to $\varepsilon\|h\|$ , must be turned into an approximate multiplier representation in $V^*$ , an infinite-dimensional dual space in which the usual finite-dimensional Farkas lemma does not apply as stated.

Formalization scope

$V$ is a real Banach space: [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V]. $V^*$ is V →L[ℝ] ℝ with the operator norm; $F'(v)$ is fderiv ℝ F v.
Constraints are one family G : Fin m → V → ℝ, 0-based: the paper's constraint $i$ is Lean index $i-1$ , an equality constraint iff its index is $<p$ . p ≤ m is assumed in the goal.
$C^1$ is ContDiff ℝ 1; $F$ is Differentiable ℝ F (Fréchet-differentiable everywhere).
No infimum over $\mathcal C$ is formed: "bounded below" is BddBelow (F '' 𝒞) and " $F(v)\le\inf_{\mathcal C}F+\varepsilon^2$ " is " $F(v)\le F(w)+\varepsilon^2$ for all $w\in\mathcal C$ ". A real infimum over an empty or unbounded set would be a junk value.
Added hypotheses, disclosed in each item: $\mathcal C\ne\emptyset$ (goal and milestone 1) and $\{G=0\}\ne\emptyset$ (Corollary 3.4). Without them the paper's hypotheses hold vacuously ( $\inf\emptyset=+\infty$ ) while the conclusion asks for a feasible point.
Lemma 3.3 is stated with $\le\varepsilon$ . The paper prints $<\varepsilon$ in (3.20), which fails for $V=\mathbb R$ , no constraints and $w^*=\varepsilon\,\mathrm{id}$ ; its proof gives $\le$ , and Theorem 3.1 uses $\le$ .
Lemma 3.2 and milestone 2 assume the linear independence (3.4) only at the point $v$ under consideration, and Lemma 3.2 is stated for any feasible $v$ with property (3.12); this is exactly what the paper's proof uses.
Regularity is a linear independence of the indexed family $(G_i'(v))_{i\in I(v)}$ , so a repeated saturated constraint violates it; the constraint qualification cannot be trivialized by collapsing duplicates.

Contributions welcome: a general Ekeland principle with the strict-minimizer conclusion, a Lyusternik–Graves tangent-curve theorem for $C^1$ maps with surjective derivative onto $\mathbb R^k$ , and a closedness result for finitely generated cones in $V^*$ .

Selected references

I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974) 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979) 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60 (2011) 627–641. https://doi.org/10.1080/02331930903578700

7 thms1 active userReviewed

Bandit Algorithms Convex Optimization Machine Learning+1·Captain: mikedeng1

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems IV: Online Stochastic Mirror Descent for Combinatorial Semi-BanditsTextbook

Motivation

Many sequential decision problems ask a learner to choose, round after round, a combination of items: a set of $m$ ads out of $d$ , a path in a network, a matching. After each choice the learner sees the loss of the items it used, not of those it did not. This is online combinatorial optimization with semi-bandit feedback. It contains the classical adversarial multi-armed bandit (choose one of $d$ arms) and is a standard model in online advertising, routing and ranking.

Chapter 5 of Bubeck and Cesa-Bianchi's monograph arXiv:1204.5721v2 treats this problem with one algorithm, Online Stochastic Mirror Descent (OSMD). Every regret bound in the chapter comes from a single mirror-descent inequality, specialized through the choice of a convex "regularizer". The chapter's capstone, Theorem 5.7, shows that a polynomial regularizer gives pseudo-regret $O(\sqrt{mdn})$ with no logarithmic factor. For $m=1$ this is the minimax-optimal rate of the adversarial bandit, first attained by the INF strategy of Audibert and Bubeck (2009). The semi-bandit version is due to Audibert, Bubeck and Lugosi (2014).

Setting

Vectors live in $\mathbb R^d$ . The arm set is a nonempty $\mathcal C\subseteq\{0,1\}^d$ with $\|v\|_1=m$ for every $v\in\mathcal C$ , and $\mathcal K=\mathrm{Conv}(\mathcal C)$ . An oblivious adversary fixes loss vectors $\ell_1,\dots,\ell_n\in[0,1]^d$ . In round $t$ the learner plays a random arm $v_t\in\mathcal C$ , pays $\ell_t^\top v_t$ , and observes $(\ell_t(1)v_t(1),\dots,\ell_t(d)v_t(d))$ . The pseudo-regret is

\bar R_n=\mathbb E\sum_{t=1}^n\ell_t^\top v_t-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t^\top x .

A Legendre function on $\bar D$ , for a nonempty open convex $D$ , is a continuous $F:\bar D\to\mathbb R$ that is strictly convex and $C^1$ on $D$ and whose gradient norm tends to $+\infty$ at $\bar D\setminus D$ . Its Bregman divergence is $D_F(x,y)=F(x)-F(y)-(x-y)^\top\nabla F(y)$ , and its Legendre–Fenchel transform is $F^*(u)=\sup_{x\in\bar D}(x^\top u-F(x))$ .

Online Mirror Descent with learning rate $\eta>0$ and vectors $g_t$ starts at $x_1\in\arg\min_{\mathcal K}F$ . It then sets $\nabla F(w_{t+1})=\nabla F(x_t)-\eta g_t$ and $x_{t+1}=\arg\min_{y\in\mathcal K}D_F(y,w_{t+1})$ . OSMD uses a random estimate $g_t=\tilde\ell_t$ of the loss. In the semi-bandit case it plays $v_t$ with $\mathbb E[v_t\mid x_t]=x_t$ and uses

\tilde\ell_t(i)=\frac{\ell_t(i)\,v_t(i)}{x_t(i)}. \tag{5.5}

A $0$ -potential is a convex, $C^1$ , increasing $\psi:(-\infty,a)\to(0,\infty)$ with $\psi(-\infty)=0$ , $\psi(a^-)=+\infty$ and $\int_0^1|\psi^{-1}|<\infty$ . It defines the Legendre function $F_\psi(x)=\sum_i\int_0^{x_i}\psi^{-1}(s)\,ds$ on $[0,\infty)^d$ . With $\psi=\exp$ this is the negative entropy.

Formalization targets

Goal: Theorem 5.7 (p. 80)

For every $0$ -potential $\psi$ and non-negative unbiased estimates,

\bar R_n\le\frac{\sup_{\mathcal K}F_\psi-F_\psi(x_1)}{\eta}+\frac\eta2\sum_{t=1}^n\sum_{i=1}^d\mathbb E\left[\frac{\tilde\ell_t(i)^2}{(\psi^{-1})'(x_t(i))}\right].

For $\psi(x)=(-x)^{-q}$ with $q>1$ , the estimate (5.5) and $\eta=\sqrt{\tfrac{2}{q-1}\,m^{1-2/q}/(n\,d^{1-2/q})}$ ,

\bar R_n\le q\sqrt{\tfrac{2}{q-1}\,mdn},\qquad\text{and }\ \bar R_n\le2\sqrt{2mdn}\ \text{ at }q=2.

Milestones

Lemma 5.1: $F^{**}=F$ , $\nabla F^*=(\nabla F)^{-1}$ on $D^*$ , and $D_F(x,y)=D_{F^*}(\nabla F(y),\nabla F(x))$ .
Lemma 5.2: existence, uniqueness and the Pythagorean inequality of Bregman projections.
Theorem 5.3: $\sum_t\ell_t(x_t)-\sum_t\ell_t(x)\le\frac{F(x)-F(x_1)}\eta+\frac1\eta\sum_tD_{F^*}(\nabla F(x_t)-\eta\nabla\ell_t(x_t),\nabla F(x_t))$ .
Theorem 5.5, linear losses, and its corrected general form.
Lemma 5.3: $F_\psi$ is Legendre and $D_{F_\psi^*}(u,v)\le\frac12\sum_i\psi'(v_i)(u_i-v_i)^2$ for $u\le v$ .
Theorem 5.6: with the negative entropy, $\bar R_n\le\sqrt{2mdn\ln(d/m)}$ .

Significance

Theorem 5.7 is the sharpest semi-bandit bound in the monograph. It shows that removing the $\sqrt{\ln(d/m)}$ factor of the exponential-weights analysis (Theorem 5.6) is a matter of the regularizer, not of a new algorithm. The same OSMD template gives the Euclidean-ball bound of Theorem 5.8 and is reused for bandit convex optimization in Chapter 6. Lemma 5.1, Lemma 5.2 and Theorem 5.3 are the standard mirror-descent toolkit, used throughout online learning and optimization.

All results of the chapter are proved in the book. Lemmas 5.1 and 5.2 are cited from Cesa-Bianchi and Lugosi (2006). None of them is formalized on Prove2Me. The published mirror-descent bound of Bandit Algorithms XII treats linear losses with a comparator inside $D$ and Euclidean-space vectors; it is not Theorem 5.3. The mission adds a machine-checked version of the whole chain, from Legendre duality to the explicit constant $q\sqrt{2mdn/(q-1)}$ , with two of the printed statements corrected (below).

Difficulty

The pathwise mirror-descent inequality is a telescoping argument, but several of its steps rest on convex analysis that Mathlib does not package. One is the existence and interior location of Bregman projections onto a set that touches the boundary of $D$ . Another is the differentiability of $F^*$ on the open dual space and the identity $\nabla F^*=(\nabla F)^{-1}$ . A third is the closed form of $F_\psi^*$ for a potential defined through an improper integral of $\psi^{-1}$ .

The probabilistic step is not a martingale argument. Only conditioning on the current iterate $x_t$ is available. The estimate (5.5) divides by $x_t(i)$ , so its integrability and unbiasedness have to be derived from the fact that the iterates stay in the open orthant. Finally, the explicit constant requires a Hölder step, $\sum_ix_1(i)^{1-1/q}\le m^{(q-1)/q}d^{1/q}$ , and the matching bound $\sum_ix_t(i)^{1/q}\le m^{1/q}d^{1-1/q}$ .

Formalization scope

Vectors are Fin d → ℝ. The arm set is a Set of $0/1$ vectors with coordinate sum $m$ , and $\mathcal K$ is convexHull ℝ C. Rounds are $t=1,\dots,n$ , sums run over Finset.Icc 1 n, and index $0$ is unused. A randomized run is a family of measurable processes $x_t, v_t, \tilde\ell_t, w_t$ on a probability space, with the deterministic OMD recursion holding on every sample path. $\mathbb E[\cdot\mid x_t]$ is the coordinatewise conditional expectation given $\sigma(x_t)$ , which is exactly what the book's proofs use. Losses are oblivious, so $\bar R_n\le B$ is stated as "for every $x\in\mathcal K$ , $\mathbb E\sum_t\ell_t^\top v_t-\sum_t\ell_t^\top x\le B$ ". $F^*$ is valued in EReal, and $D_{F^*}$ is evaluated only on the open dual space, where $F^*$ is finite. Wherever an expectation of a possibly non-integrable quantity appears on a right-hand side, its integrability is assumed: the book's bound is then $+\infty$ and trivial, while Lean's integral would be $0$ .

Corrections and instantiations, each labelled in the item's Formalization Note:

Theorem 5.7, corrected misprint. The book prints $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{d^{1-2/q}}}$ . The proof (p. 81) gives the stated bound only for $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{n\,d^{1-2/q}}}$ , which is stated. At $q=2$ this is $\eta=\sqrt{2/n}$ .
Theorem 5.5, corrected misprint. In the first bound the book prints $\mathbb E[\|x_t-\tilde x_t\|\,\|\tilde g_t\|_*]$ . That statement fails for $\ell_t(x)=x^2$ on $[-1,1]$ with $F=x^2/2$ and $\tilde x_t=\pm1$ . The version stated uses $\|\nabla\ell_t(\tilde x_t)\|_*$ , as the proof's first inequality does. The linear-loss bound is stated as printed.
Lemma 5.2. "For all $z\in K\cap D$ " is read as "for the projection $z$ ", which lies in $K\cap D$ .
Hypotheses made explicit: $q>1$ ; non-negativity of the estimates in Theorem 5.6 (used in its proof); unbiasedness $\mathbb E[\tilde\ell_t\mid x_t]=\ell_t$ in the general parts of Theorems 5.6 and 5.7; $\mathcal K\cap(0,\infty)^d\ne\emptyset$ (OMD's requirement $K\cap D\ne\emptyset$ ); a subgradient selection as an explicit input.
Theorem 5.6's particular bound uses the book's $\eta=\sqrt{\frac{2m}{nd}\ln\frac dm}$ as printed. There are no O(·) constants in the chapter's statements.

A trivializing formalization would let $\eta$ , $x_t$ or the estimate be junk values: an OSMD step at $\eta=0$ , a Lean division $x/0=0$ , or a regret written as a real infimum over an unbounded set. Here every run is the book's algorithm on the open orthant, and each bound is stated against every comparator in $\mathcal K$ .

Reusable beyond this mission: the Legendre/Bregman layer, the OMD run predicate and the $\omega$ -potential layer. Proofs of Lemmas 5.1 and 5.2 in this generality would be welcome additions to the library.

Selected references

S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012; arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721
N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921
J.-Y. Audibert, S. Bubeck, Regret bounds and minimax policies under partial monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
J.-Y. Audibert, S. Bubeck, G. Lugosi, Regret in online combinatorial optimization, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0598

12 thms1 active userReviewed

Discrete Geometry Linear Optimization Operations Research·Captain: mikedeng1

Sensitivity Theorems in Integer Linear Programming: Every Integral m×n Matrix Has Chvátal Rank at Most 2^(n³+1)·n^(5n)·Δ(A)^(n+1)Research Paper

Motivation

An integer linear program $\max\{wx : Ax \le b,\ x \text{ integral}\}$ is usually attacked through its linear programming relaxation $\max\{wx : Ax \le b\}$ , which drops the integrality constraint. Two questions follow at once. How far can an optimal solution of the relaxation be from an optimal integer solution? And how many rounds of rounding-based cutting planes are needed before the relaxation describes the integer points exactly? Branch-and-bound, cutting-plane methods and the parametric analysis of integer programs all depend on the answers.

W. Cook, A.M.H. Gerards, A. Schrijver and É. Tardos, Sensitivity theorems in integer linear programming (Math. Programming 34 (1986) 251–264), answer both in terms of the number of variables $n$ and the largest subdeterminant $\Delta(A)$ of the constraint matrix, independently of the right-hand side.

Timeline.

1958–1963: Gomory introduces integer rounding cuts. In 1973 Chvátal (Discrete Math. 4) shows that finitely many rounds reach the integer hull of a bounded polyhedron.
1977–1979: Blair and Jeroslow prove that for a fixed matrix $A$ the distance between LP and IP optima, and the gap between their values, are bounded by constants depending on $A$ .
1980: Schrijver (Ann. Discrete Math. 9) proves that the Chvátal closure of a rational polyhedron is a polyhedron, and that every rational polyhedron, bounded or not, reaches its integer hull after finitely many rounds.
1986: Cook, Gerards, Schrijver and Tardos prove the explicit bounds of this mission, $n\Delta(A)$ for proximity, and show that every integral matrix has finite Chvátal rank.
Later work, for example Eisenbrand and Weismantel (2018), replaces the $\ell_\infty$ proximity bound by $\ell_1$ bounds for programs in standard form.

Setting

All matrices, vectors and polyhedra are rational. Let $A$ be an integral $m\times n$ matrix. A square submatrix of order $k$ , where $1\le k\le\min(m,n)$ , keeps $k$ rows and $k$ columns of $A$ . The quantity $\Delta(A)$ is the largest $|\det B|$ over all such submatrices $B$ . So $\Delta(0)=0$ , and $\Delta(A)\ge 1$ whenever $A\ne 0$ . Norms are $\|x\|_\infty=\max_i|x_i|$ and $\|x\|_1=\sum_i|x_i|$ .

For $b\in\mathbb{Q}^m$ write $P=\{x\in\mathbb{Q}^n : Ax\le b\}$ . An optimal solution of $\max\{wx : Ax\le b\}$ is a point of $P$ maximizing $wx$ . For $\max\{wx : Ax\le b,\ x\text{ integral}\}$ it is an integral point of $P$ maximizing $wx$ among the integral points of $P$ . A rational polyhedron is a set $\{x : Dx\le d\}$ with $D$ , $d$ rational. The integer hull $P_I$ is the convex hull of the integral points of $P$ .

If $ay\le\beta$ for all $y\in P$ , with $a$ integral and $\beta$ rational, then every integral point of $P$ satisfies the Chvátal cut $ax\le\lfloor\beta\rfloor$ . The Chvátal closure $P'$ is the set of points satisfying all Chvátal cuts. Set $P^{(0)}=P$ and $P^{(i)}=(P^{(i-1)})'$ . Then $P_I\subseteq P^{(i)}$ for all $i$ . The Chvátal rank of $P$ is the least $t$ with $P^{(t)}=P_I$ . The Chvátal rank of the matrix $A$ is the supremum of the Chvátal ranks of $\{x : Ax\le b\}$ over all integral vectors $b$ .

Formalization targets

Goal: Theorem 10 (p. 260)

\sup_{b\in\mathbb{Z}^m}\ \operatorname{rank}\{x : Ax\le b\}\ \le\ 2^{n^3+1}\,n^{5n}\,\Delta(A)^{n+1}.

In particular, every integral matrix has finite Chvátal rank, and the bound does not depend on $m$ or on $b$ .

Milestones, in attack order

Theorem 1 (p. 252). Suppose $Ax\le b$ has an integral solution and the LP maximum exists. Then every LP optimum has an IP optimum within $\ell_\infty$ -distance $n\Delta(A)$ , and every IP optimum has an LP optimum within the same distance.
Corollary 2 (p. 253). Under the same hypotheses, $\max\{wx: Ax\le b\}-\max\{wx : Ax\le b,\ x\text{ integral}\}\le n\Delta(A)\|w\|_1$ .
Theorem 5 (p. 255). Changing $b$ to $b'$ moves LP optima by at most $n\Delta(A)\|b-b'\|_\infty$ and IP optima by at most $n\Delta(A)(\|b-b'\|_\infty+2)$ . This result is off the goal's path.
Theorem 6 (p. 256). A non-optimal integral solution can be improved by an integral solution within $\ell_\infty$ -distance $n\Delta(A)$ .
Theorem 7 (p. 257). A single integral matrix $M$ , with entries at most $n^{2n}\Delta(A)^n$ in absolute value, gives $\{x: Ax\le b\}_I=\{x : Mx\le d_b\}$ for every $b$ for which $Ax\le b$ has an integral solution.
Theorem 8, printed "Theorem 9" (p. 259). If a rational polyhedron $P\subseteq\mathbb{Q}^n$ has no integral point, then $P^{(n^{2n}2^{n^3})}=\emptyset$ .
Corollary 9 (p. 260). Let $q=\max\{wx : x\in P_I\}$ with $w$ integral. Then $P^{(r)}\subseteq\{x : wx\le q\}$ for $r=(n^{2n}2^{n^3}+1)(\lfloor\max\{wx : x\in P\}\rfloor-q)+1$ .

Significance

The result. Theorem 10 shows that the number of Gomory–Chvátal rounding rounds needed for $\{x : Ax\le b\}$ is controlled by $A$ alone. It is the first general finite bound on the Chvátal rank of a matrix. Earlier, the matrices of Chvátal rank 0 had been characterized by Hoffman and Kruskal: they are the matrices whose transpose is unimodular. Some classes of rank 1 had also been characterized (Edmonds–Johnson, Gerards–Schrijver). The proximity results of §2 are used on their own. They bound the work needed to solve an integer program from an LP optimum, and they show that the optimal value of an integer program changes at most affinely with $b$ . They are also the standard starting point for the later proximity literature.

Formalizing it. All results are proved in the paper. As far as is known, none of them has a machine-checked proof: the Prove2Me corpus holds no Chvátal rank bound, and its existing proximity theorems concern a different bound, the $\ell_1$ bound with $\Delta$ the largest entry. This mission asks for Lean proofs of the paper's statements with the constants exactly as printed. It also builds a reusable layer over $\mathbb{Q}$ : polyhedra, LP and IP optimality, integer hulls, the Chvátal closure and the Chvátal rank.

Difficulty

The proximity theorems need a conic decomposition $\bar x-\bar z=\sum\lambda_i g^i$ into integral generators with entries bounded by $\Delta(A)$ . That requires Cramer's rule bounds on cone generators and Carathéodory's theorem, and neither is in Mathlib in this form for rational polyhedral cones.

Theorem 7 needs finite generation of integral cones with explicit coefficient bounds, together with LP duality.

The Chvátal-rank part is harder. The obvious induction on the value of a valid inequality fails, because the value gap $\lfloor\max_P wx\rfloor-q$ is not bounded independently of $b$ until Theorem 7 and Corollary 2 bound it by $n^{2n+2}\Delta(A)^{n+1}$ . Theorem 8 itself rests on a flatness theorem for lattice-free polyhedra (Lenstra; Grötschel–Lovász–Schrijver), which the paper cites without proof. It also needs Schrijver's lemma that $P^{(k)}\cap F\subseteq F^{(k)}$ for faces $F$ , and invariance under unimodular affine maps. None of these is in Mathlib.

Formalization scope

Rationality. Everything is over $\mathbb{Q}$ , following the paper's standing assumption on p. 252. Points are Fin n → ℚ, $A$ is Matrix (Fin m) (Fin n) ℤ cast to $\mathbb{Q}$ , and a polyhedron is a finite system of rational inequalities.
$\Delta(A)$ . Only nonempty submatrices count, so $\Delta(0)=0$ .
Optimality. "The maximum exists" means an optimal solution exists. Existence claims that the paper proves are part of the conclusions: the IP optimum in Theorem 1 and Corollary 2, and $\max\{wx : x\in P\}$ in Corollary 9.
Chvátal closure. It is defined for every subset of $\mathbb{Q}^n$ , using all integral $a$ and rational $\beta$ . The rank is valued in $\mathbb{N}\cup\{\infty\}$ , with $\infty$ if no iterate equals $P_I$ . A version with junk value $0$ would make the goal trivial and is not used. The matrix rank is a supremum over integral $b$ , as printed.
Added hypotheses. Theorems 1 and 6 carry the hypothesis $A\ne0$ . For $A=0$ the bound $n\Delta(A)=0$ makes both statements false, and the proof on p. 257 assumes $A\ne0$ as well. In Corollary 9 the value $q$ is taken to be an integer. This loses nothing, because a maximum of an integral $w$ over $P_I$ is attained at an integral point.
Constants. All constants are exactly as printed, written in $\mathbb{N}$ with $0^0=1$ .

A complete development needs the following:

cone generation with Cramer bounds and Carathéodory's theorem;
LP duality and Farkas' lemma over $\mathbb{Q}$ ;
the polyhedrality of $P'$ for rational polyhedra (Schrijver 1980);
Schrijver's face lemma and unimodular invariance;
a flatness theorem.

The LP, cone and Chvátal-closure layers are reusable beyond this mission. Proofs of any milestone are welcome, and so is groundwork such as polyhedrality of the Chvátal closure or the flatness theorem, submitted as separate theorems.

Selected references

W. Cook, A.M.H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34 (1986) 251–264. https://doi.org/10.1007/BF01582230
V. Chvátal, Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Mathematics 4 (1973) 305–337. https://doi.org/10.1016/0012-365X(73)90167-2
A. Schrijver, On cutting planes, Annals of Discrete Mathematics 9 (1980) 291–296. https://doi.org/10.1016/S0167-5060(08)70085-2
W. Cook, C.R. Coullard, Gy. Turán, On the complexity of cutting-plane proofs, Discrete Applied Mathematics 18 (1987) 25–38. https://doi.org/10.1016/0166-218X(87)90039-4
F. Eisenbrand, R. Weismantel, Proximity results and faster algorithms for integer programming using the Steinitz lemma, ACM Transactions on Algorithms 16 (2020), Art. 5. https://doi.org/10.1145/3340322

11 thms1 active userReviewed

Control Theory Mathematical Physics Partial Differential Equations+2·Captain: mikedeng1

Optimization of Mean-field Spin Glasses III: The Lagrangian Value of the Stochastic Control Problem Equals the Parisi FunctionalResearch Paper

Motivation

The ground-state energy of a mixed $p$ -spin spin glass, $\mathsf{OPT}_N=\max_{\sigma\in\{\pm1\}^N}H_N(\sigma)/N$ , converges almost surely to the infimum of the Parisi functional over non-decreasing order parameters (Auffinger–Chen 2017). El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) study algorithms that find near-optimal configurations. They introduce incremental approximate message passing (IAMP) and show that, among a broad class of such algorithms, the best achievable energy is the infimum of the Parisi functional over a larger space of order parameters (their Theorem 4).

The upper bound in Theorem 4 is reduced, in Section 4 of the paper, to a stochastic optimal control problem. The energy reached by a message-passing algorithm becomes the objective of a control problem driven by a Brownian motion, with a terminal constraint and a variance constraint. The variance constraint is removed by a Lagrange multiplier $\tfrac12\xi''\gamma$ . Proposition 4.1 states that the resulting Lagrangian value is exactly the Parisi functional $\mathsf P(\gamma)$ . This mission formalizes that duality and the verification argument behind it (Section 7).

Setting

Mixture. Real coefficients $(c_k)_{k\ge2}$ define the mixture $\xi(t)=\sum_{k\ge2}c_k^2t^k$ , with the standing assumption $\xi(1+\varepsilon)<\infty$ for some $\varepsilon>0$ . Its derivatives $\xi'$ , $\xi''$ are nonnegative and nondecreasing on $[0,1]$ .

Order parameters. $\mathsf{SF}_+$ is the set of nonnegative step functions

\gamma=\sum_{i=1}^m\gamma_i\,\mathbb I_{[t_{i-1},t_i)},\qquad 0=t_0<t_1<\dots<t_m=1,\ \gamma_i\ge0 .

Put $\nu(t)=\int_t^1\xi''(s)\gamma(s)\,ds$ .

Parisi PDE and functional. $\Phi_\gamma:[0,1]\times\mathbb R\to\mathbb R$ solves

\partial_t\Phi_\gamma+\tfrac12\xi''(t)\big(\partial_x^2\Phi_\gamma+\gamma(t)(\partial_x\Phi_\gamma)^2\big)=0,\qquad\Phi_\gamma(1,x)=|x| .

For $\gamma\in\mathsf{SF}_+$ it is given explicitly by the Cole–Hopf recursion: with $r(t)=\xi'(1)-\xi'(t)$ and $G\sim\mathsf N(0,1)$ , for $t\in[t_{i-1},t_i)$ ,

\Phi_\gamma(t,x)=\frac1{\gamma_i}\log\mathbb E\exp\big\{\gamma_i\Phi_\gamma(t_i,x+\sqrt{r(t)-r(t_i)}\,G)\big\}.

The Parisi functional is $\mathsf P(\gamma)=\Phi_\gamma(0,0)-\tfrac12\int_0^1t\,\xi''(t)\gamma(t)\,dt$ .

Control problem. Let $B$ be a standard Brownian motion. A control $u\in D[t,1]$ is a process on $[t,1]$ , progressively measurable for the filtration of $(B_r)_{r\in[t,1]}$ , with $\mathbb E\int_t^1\xi''(s)u_s^2\,ds<\infty$ . The value is

\mathcal J_\gamma(t,z)=\sup_{u\in D[t,1]}\mathbb E\Big[\int_t^1\xi''(s)u_s\,ds+\frac12\int_t^1\nu(s)\big(\xi''(s)u_s^2-1\big)ds\Big]\quad\text{s.t.}\quad z+\int_t^1\sqrt{\xi''(s)}\,u_s\,dB_s\in(-1,1)\ \text{a.s.}

Candidate value function. With $\Phi^*_\gamma(t,z)=\inf_x\{\Phi_\gamma(t,x)-xz\}$ ,

V(t,z)=\Phi^*_\gamma(t,z)-\tfrac12\nu(t)z^2-\tfrac12\int_t^1\nu(s)\,ds .

Formalization targets

Goal: Proposition 4.1

\mathcal J_\gamma(0,0)=\mathsf P(\gamma)\qquad\text{for every }\gamma\in\mathsf{SF}_+ .

Milestones

Lemma 7.2 (a)–(e): $\Phi_\gamma(t,\cdot)$ is smooth for $t<1$ , with derivatives jointly continuous on $[0,1)\times\mathbb R$ and $C^1$ in time where $\gamma$ is constant. The range of $\partial_x\Phi_\gamma(t,\cdot)$ is $(-1,1)$ , it is strictly increasing, and $0<\partial_x^2\Phi_\gamma(t',x)\le C(t,\gamma)$ for $t'\le t$ .
Envelope identities (proof of Lemma 7.3): $\partial_z\Phi^*_\gamma(t,z)=-x^*_t(z)$ and $\partial_z^2\Phi^*_\gamma(t,z)=-1/\partial_x^2\Phi_\gamma(t,x^*_t(z))$ , where $x^*_t(z)$ is the unique root of $\partial_x\Phi_\gamma(t,x)=z$ .
Lemma 7.3: $V$ solves the HJB equation

\partial_tV+\xi''(t)\sup_{\lambda\in\mathbb R}\Big\{\lambda+\frac{\lambda^2}{2}\big(\nu(t)+\partial_z^2V\big)\Big\}-\frac12\nu(t)=0,\qquad V(1,z)=0 .

Evaluation at the origin: $V(0,0)=\mathsf P(\gamma)$ .
Proposition 7.1: $\mathcal J_\gamma(t,z)=V(t,z)$ for all $(t,z)\in[0,1]\times(-1,1)$ .

Proposition 7.1 at $(0,0)$ together with milestone 4 gives the goal.

Significance

The result. By integration by parts (Eq. (4.4) of the paper), $\mathcal J_\gamma(0,0)$ bounds the value of the constrained control problem (4.2). That problem in turn bounds the asymptotic energy of every message-passing algorithm in the class of Theorem 4. Proposition 4.1 turns the bound into $\inf_{\gamma\in\mathsf{SF}_+}\mathsf P(\gamma)$ , which is the analytic core of the optimality statement for IAMP. It is also an instance of a broader principle: the Parisi functional has a stochastic-control representation (Jagannath–Tobasco 2016).

Formalizing it. The result is proved in the paper; no machine-checked version exists. A complete formalization needs a verification theorem for a control problem with a state constraint ( $M_1\in(-1,1)$ ), Itô's formula for a $C^{1,2}$ function that is only piecewise $C^1$ in time, and quantitative regularity of the Cole–Hopf solution. Each of these is reusable well beyond spin glasses.

Difficulty

The value function $\mathcal J_\gamma$ is not known to be smooth, and the dynamic-programming equation (4.6) is only heuristic. The proof therefore guesses a solution and verifies it. Two steps carry the difficulty.

First, the guess $V$ is a Legendre transform. Its regularity, and the sign $\nu+\partial_z^2V<0$ that makes the HJB supremum finite, rest on strict convexity and bounded curvature of $\Phi_\gamma(t,\cdot)$ (Lemma 7.2). These must be proved by induction through the Cole–Hopf recursion, including the steps with $\gamma_i=0$ .

Second, the verification argument applies Itô's formula to $V(s,M^u_s)$ , where $M^u$ is a martingale confined to $(-1,1)$ and $V$ is only $C^1$ in time between the jumps of $\gamma$ . The boundary $\theta\to1$ needs a dominated-convergence argument, and attaining the supremum needs an explicit optimal feedback control built from an SDE.

Formalization scope

Mixture. $\xi$ is a coefficient sequence $c:\mathbb N\to\mathbb R$ with $c_0=c_1=0$ imposed. $\xi'$ and $\xi''$ are explicit termwise series.
Step functions. $\mathsf{SF}_+$ is represented by its data (breakpoints and values). $\gamma$ is extended by $0$ outside $[0,1)$ ; its value at $t=1$ never matters.
Cole–Hopf. $\Phi_\gamma$ is defined by the recursion. When $\gamma_i=0$ , the recursion uses its limit, the heat semigroup, instead of dividing by zero. Expectations over $G$ are integrals against gaussianReal 0 1.
Derivatives. Space derivatives are deriv/iteratedDeriv. Time derivatives are right derivatives, because $\gamma$ jumps.
Legendre transform. $\Phi^*_\gamma$ is a real infimum, used only for $|z|<1$ , where it is bounded below.
Brownian motion and filtration. $B$ is a Mathlib IsBrownianReal process on $\mathbb R_{\ge0}$ , with each $B_r$ measurable. The filtration is $\mathcal F^t_s=\sigma(B_r:t\le r\le s)$ .
Stochastic integral. It is the $L^2$ Itô integral of the published definition Peng1990.SMP.IsItoIntegral (horizon $1$ ), whose integrability class is exactly $\mathbb E\int\xi''u^2<\infty$ .
Supremum. $\mathcal J_\gamma(t,z)=v$ is stated as " $v$ is the least upper bound of the objective values of admissible controls" (IsLUB), never as a real sSup. A default value of an empty or unbounded supremum therefore cannot make a statement trivially true.
Disclosed hypothesis. Lemma 7.2, the envelope identities and Lemma 7.3 assume that $\xi$ is not identically zero (some $c_k\neq0$ ). For $\xi\equiv0$ one has $\Phi_\gamma(t,x)=|x|$ for all $t$ , and these statements fail. Proposition 7.1, the evaluation at the origin and the goal need no such hypothesis.
Lemma 7.3. The statement includes the inequality $\nu+\partial_z^2V<0$ , which the page proves. This rules out reading the HJB supremum as a default value.

The paper's algorithmic results (Theorems 2–4, Corollary 2.2) are out of scope. They need the AMP and state-evolution machinery of Section 5 and Appendix A, and an informal model of computation. The optional bound (4.4) is not stated.

Welcome contributions include the regularity of Cole–Hopf solutions (Gaussian convolution, log-moment-generating functions), a general verification theorem for one-dimensional controlled martingales with a terminal state constraint, and Itô's formula for $C^{1,2}$ functions.

Selected references

A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144, 2016. https://arxiv.org/abs/1502.04398
N. Touzi, Optimal Stochastic Control, Stochastic Target Problems, and Backward SDE, Fields Institute Monographs 29, Springer, 2012 (cited as [Tou12] in the paper; the verification argument of Section 7 follows its Theorem 4.1).

14 thms1 active userReviewed

Mathematical Physics Partial Differential Equations Probability·Captain: mikedeng1

Optimization of Mean-field Spin Glasses I: Every Minimizer of the Extended Parisi Functional Has Full SupportResearch Paper

Motivation

The Ising mixed $p$ -spin model assigns to each configuration $\sigma \in \{-1,+1\}^N$ the energy of a random polynomial whose covariance is $\mathbb E\{H_N(\sigma)H_N(\sigma')\} = N\xi(\langle\sigma,\sigma'\rangle/N)$ . Its ground-state energy $\max_\sigma H_N(\sigma)/N$ converges to the value of a variational problem, the zero-temperature Parisi formula (Auffinger–Chen 2017), in which a functional $\mathsf P$ is minimized over non-decreasing order parameters $\gamma$ . El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) ask how close a polynomial-time algorithm can get to this maximum. Their answer is an extended variational principle: the best value reachable by incremental approximate message passing is $\inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$ , where the space $\mathscr L$ drops the monotonicity constraint.

The algorithm that reaches this value is built from a minimizer $\gamma_*$ of $\mathsf P$ over $\mathscr L$ , and it runs along the set of times where $\gamma_*$ is positive. Theorem 5 of the paper (p. 30) shows that this set is dense: a minimizer has full support. This mission formalizes that theorem and the first- and second-order optimality conditions it rests on (Section 6.1, pp. 22–31).

Timeline. Parisi proposed the variational formula in 1979. Talagrand (2006) and Panchenko (2013) proved it at positive temperature. Auffinger and Chen (2017) established the zero-temperature version with $\Phi(1,x)=|x|$ and proved that a minimizer over the monotone space exists. Jagannath and Tobasco (2016) developed the PDE and SDE tools for the Parisi functional that Section 6.1 of the present paper adapts to non-monotone order parameters. Montanari (2019) gave the first message passing algorithm for the Sherrington–Kirkpatrick case; the present paper (2020) extended it to general mixtures and introduced $\mathscr L$ .

Setting

A mixture is $\xi(t) = \sum_{k\ge2} c_k^2 t^k$ with $\xi(1+\varepsilon) < \infty$ for some $\varepsilon > 0$ ; its derivatives $\xi'$ , $\xi''$ are the termwise differentiated power series, non-negative and non-decreasing on $[0,1]$ .

An order parameter is a function $\gamma : [0,1) \to \mathbb R_{\ge0}$ . The extended space is

\mathscr L = \Bigl\{\gamma : [0,1)\to\mathbb R_{\ge0} : \|\xi''\gamma\|_{\mathrm{TV}[0,t]}<\infty\ \forall t\in[0,1),\ \int_0^1\xi''(t)\gamma(t)\,dt<\infty\Bigr\},

with the weighted distance $\|\gamma_1-\gamma_2\|_{1,\xi''} = \int_0^1\xi''(t)|\gamma_1(t)-\gamma_2(t)|\,dt$ . The non-negative step functions $\mathsf{SF}_+$ are the finite sums $\sum_i a_i\mathbb I_{[t_{i-1},t_i)}$ with $0=t_0<\dots<t_m=1$ and $a_i\ge0$ .

For a terminal condition $f_0$ (convex, continuous, even, non-negative, differentiable off $0$ with $0\le f_0'\le1$ on $(0,\infty)$ ) and $\gamma\in\mathsf{SF}_+$ , the Parisi PDE

\partial_t\Phi + \tfrac12\xi''(t)\bigl(\partial_x^2\Phi + \gamma(t)(\partial_x\Phi)^2\bigr) = 0,\qquad \Phi(1,x) = f_0(x),

has the explicit Cole–Hopf solution $\Phi^\gamma$ : on $[t_{i-1},t_i)$ , $\Phi(t,x) = \gamma_i^{-1}\log\mathbb E\exp\{\gamma_i\Phi(t_i, x+\sqrt{\xi'(t_i)-\xi'(t)}\,G)\}$ with $G\sim\mathsf N(0,1)$ . For $\gamma\in\mathscr L$ , $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n\to\gamma$ in the weighted distance. The Parisi functional is

\mathsf P(\gamma) = \Phi^\gamma(0,0) - \frac12\int_0^1 t\,\xi''(t)\gamma(t)\,dt .

Given a Brownian motion $B$ , the process $X$ solves $dX_t = \xi''(t)\gamma(t)\,\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$ , $X_0 = 0$ . The support of $\gamma$ is $S(\gamma) = \{t\in[0,1):\gamma(t)>0\}$ , and $\overline S(\gamma)$ is its closure in $[0,1)$ .

Formalization targets

Goal: Theorem 5

With $f_0(x) = |x|$ , if $\gamma_*\in\mathscr L$ satisfies $\mathsf P(\gamma_*) = \inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$ , then

\overline S(\gamma_*) = [0,1).

Milestones

The path to the goal, in attack order:

Proposition 6.1(b),(c): on step functions, $\partial_x\Phi$ is non-decreasing with $|\partial_x\Phi|\le1$ , and $\|\Phi^{\gamma_1}-\Phi^{\gamma_2}\|_\infty\le\|\xi''(\gamma_1-\gamma_2)\|_1$ .
Lemma 6.2: these properties pass to $\gamma\in\mathscr L$ .
Lemma 6.5: the SDE has a unique strong solution on $[0,1]$ .
Corollary 6.6: $\mathbb E\{\partial_x\Phi(t_2,X_{t_2})^2\}-\mathbb E\{\partial_x\Phi(t_1,X_{t_1})^2\}=\int_{t_1}^{t_2}\xi''(s)\,\mathbb E\{(\partial_x^2\Phi(s,X_s))^2\}\,ds$ .
Lemma 6.7: the map $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$ .
Proposition 6.8: the first variation $\frac{d}{ds}\mathsf P(\gamma+s\delta)|_{s=0+}=\frac12\int_0^1\xi''\delta\,(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t)\,dt$ .
Lemma 6.9: $S(\gamma)$ is a countable disjoint union of intervals.
Corollary 6.10: $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\}=t$ on $\overline S(\gamma_*)$ and $\ge t$ off it.
Corollary 6.11: $\xi''(t)\,\mathbb E\{\partial_x^2\Phi^{\gamma_*}(t,X_t)^2\}=1$ on $\overline S(\gamma_*)$ .
Lemma 6.12: the law of $X_t$ has a density, bounded below on compact sets, once $\gamma$ vanishes.

Significance

The result. Full support identifies the extended variational principle as one whose minimizers are "nowhere flat". The algorithm of Theorem 3 in the paper follows $\gamma_*$ through incremental steps whose size is set by $\gamma_*$ , and it needs no special treatment of gaps where $\gamma_* = 0$ . The stationarity conditions (Corollaries 6.10–6.11) also characterize minimizers over $\mathscr L$ the way the Auffinger–Chen conditions characterize minimizers over the monotone space. They are the starting point for comparing $\inf_{\mathscr L}\mathsf P$ with the Parisi value.

Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The paper's proofs rely on cited PDE regularity (Jagannath–Tobasco 2016) and on standard SDE theory, often in one line. The mission produces a machine-checked chain from the explicit Cole–Hopf formula to the support theorem. Along the way it builds the Parisi PDE solution on a non-monotone class, a first-variation formula, and stationarity conditions, none of which have a formal counterpart. No formal statement of the Parisi functional or the Parisi PDE exists on Prove2Me (index search, 2026-10-03).

Difficulty

Two steps resist a direct argument. The first is the first variation (Proposition 6.8): differentiating $\Phi^\gamma(0,0)$ in $\gamma$ requires comparing the SDE for $\gamma$ with the SDE for the perturbed parameter and controlling their difference uniformly, which needs bounds on $\partial_x^2\Phi$ that degenerate as $t\to1$ . The second is the exclusion of gaps: on an interval where $\gamma_*=0$ the PDE is a time-changed heat equation, and the contradiction comes from a strict inequality, which requires the law of $X_t$ to charge every interval (Lemma 6.12). The obvious idea of perturbing $\gamma_*$ upward on a gap only yields the inequality (6.14), which is consistent with a gap; the second-order identity at the gap's endpoints is what closes the argument.

Formalization scope

Conventions committed to in Lean:

The mixture is a coefficient sequence $c$ with $c_0=c_1=0$ ; $\xi,\xi',\xi''$ are explicit series.
Order parameters are functions $\mathbb R\to\mathbb R$ read only on $[0,1)$ . Membership in $\mathscr L$ uses eVariationOn for the total variation and IntegrableOn for the integral; the latter includes the a.e.-measurability that the paper takes for granted.
$\Phi^\gamma$ for step functions is the Cole–Hopf recursion (7.3). For a piece with $\gamma_i = 0$ the formula's limit, the heat semigroup, is used instead of a division by zero. $\mathbb E$ over $G$ is integration against gaussianReal 0 1. For $\gamma\in\mathscr L$ , $\Phi^\gamma$ is a limit along the filter of step functions converging in the weighted $L^1$ distance; it is never "some solution of the PDE".
$\partial_x\Phi$ and $\partial_x^2\Phi$ are iterated derivs in $x$ . Lemma 6.2's weak-derivative claim is stated as "convex and 1-Lipschitz", its equivalent.
The SDE uses the published strong-solution concept EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by zero after time $1$ . The driver is assumed to be a standard Brownian motion (IsBrownianReal). Statements about $X$ hold for every strong solution, which by Lemma 6.5 is unique.
Section 6.1's results are stated for every admissible $f_0$ ; $\mathsf P$ is parametrized by $f_0$ , and Theorem 5 fixes $f_0=|\cdot|$ .
Minimality is " $\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma\in\mathscr L$ ", never a real infimum. $\overline S(\gamma)$ is closure (S γ) ∩ Ico 0 1. Right-continuity of $\gamma_*$ , the paper's convention from p. 28, is a hypothesis.
Disclosed hypothesis $\xi\not\equiv0$ (some $c_k\neq0$ ) on Theorem 5, Corollaries 6.10–6.11 and Lemma 6.12. For $\xi\equiv0$ every $\gamma$ minimizes $\mathsf P$ and $X\equiv0$ , so $\gamma_*\equiv0$ has empty support and each of those statements fails. When $c_2=0$ no minimizer exists (Corollary 6.11 at $t=0$ ), and Theorem 5 is vacuous, as in the paper.
Lemma 6.12's density bound is stated without choosing density versions: $\varepsilon\,\mathrm{Leb}(A)\le\mathbb P(X_t\in A)$ for measurable $A\subseteq[-M,M]$ .

A trivializing formalization is excluded: $\Phi^\gamma$ and $X$ are the paper's objects, built from the data, so the goal cannot be met by choosing a convenient solution, and minimality over $\mathscr L$ cannot be satisfied by a junk infimum.

Not formalized: the weak formulation (6.4) of Lemma 6.2, printed with a wrong boundary term; the stochastic-integral identity (6.7) of Lemma 6.5; the regularity Lemmas 6.3–6.4; Proposition 6.1(a). The paper's algorithmic Theorems 2–4 are out of scope, because they concern algorithms in an informal model of computation and an AMP state-evolution theory that is not part of this mission.

Useful infrastructure beyond this mission: the Cole–Hopf solution and its Lipschitz dependence on $\gamma$ , the Parisi functional on $\mathscr L$ , and the SDE (6.3). Contributions that formalize Itô's formula for these processes or the regularity of $\Phi^\gamma$ are welcome as supporting lemmas.

Selected references

A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Annals of Probability, 2017. https://arxiv.org/abs/1606.05335
A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proceedings of the AMS, 2016. https://arxiv.org/abs/1502.04398
A. Montanari, Optimization of the Sherrington–Kirkpatrick Hamiltonian, FOCS 2019. https://arxiv.org/abs/1812.10897
M. Talagrand, The Parisi formula, Annals of Mathematics 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
D. Panchenko, The Parisi ultrametricity conjecture, Annals of Mathematics 177(1), 2013. https://doi.org/10.4007/annals.2013.177.1.8

22 thms1 active userReviewed

Mathematical Physics Partial Differential Equations Probability·Captain: mikedeng1

Optimization of Mean-field Spin Glasses II: Under No Overlap Gap, the Monotone Parisi Minimizer Also Minimizes the Extended FunctionalResearch Paper

Motivation

The mixed $p$ -spin model is a random polynomial on the hypercube $\{-1,+1\}^N$ : a centered Gaussian process $H_N(\boldsymbol\sigma)$ with covariance $\mathbb E\{H_N(\boldsymbol\sigma)H_N(\boldsymbol\sigma')\} = N\xi(\langle\boldsymbol\sigma,\boldsymbol\sigma'\rangle/N)$ . Its maximum $\mathrm{OPT}_N = \max_{\boldsymbol\sigma} H_N(\boldsymbol\sigma)/N$ is a canonical random optimization problem; for $\xi(t) = c_2^2t^2$ it is the ground state of the Sherrington–Kirkpatrick model. Auffinger and Chen (AC17) proved that $\mathrm{OPT}_N$ converges almost surely to the infimum of the zero-temperature Parisi functional $\mathsf P$ over a space $\mathscr U$ of non-decreasing order parameters.

El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) characterize what a class of message-passing algorithms achieves on this problem. The answer is the infimum of the same functional over a larger space $\mathscr L$ of order parameters that need not be monotone. Whether these algorithms reach the true optimum is therefore the question whether $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$ . The paper proves this equality under the no-overlap gap assumption, that the Parisi minimizer over $\mathscr U$ can be taken strictly increasing (Assumption 2, p. 8). This is believed to hold for the Sherrington–Kirkpatrick model and to fail for pure $p$ -spin models with $p \ge 3$ . This mission formalizes that equality, stated as a property of the minimizer.

Timeline. Parisi's formula (1979) was proved by Talagrand (2006) and Panchenko (2013). Auffinger and Chen (2017) gave its zero-temperature form (1.7). Jagannath and Tobasco (JT16) gave a PDE and variational treatment of the Parisi functional at positive temperature, including its convexity. Montanari (Mon19) gave a message-passing algorithm for the Sherrington–Kirkpatrick model under no overlap gap. El Alaoui, Montanari and Sellke (2020) extended it to mixed $p$ -spin models and introduced the extended principle over $\mathscr L$ .

Setting

A mixture is $\xi(t) = \sum_{k\ge2} c_k^2 t^k$ with $\xi(1+\varepsilon) < \infty$ for some $\varepsilon > 0$ , with derivatives $\xi'$ and $\xi''$ given by the termwise series. Order parameters are functions $\gamma : [0,1) \to \mathbb R_{\ge0}$ , in one of two spaces:

\mathscr U = \Big\{\gamma \text{ non-decreasing},\ \int_0^1\gamma(t)\,dt < \infty\Big\},\qquad \mathscr L = \Big\{\|\xi''\gamma\|_{TV[0,t]} < \infty\ \forall t<1,\ \int_0^1\xi''(t)\gamma(t)\,dt < \infty\Big\}.

Here $\|\cdot\|_{TV[0,t]}$ is total variation on $[0,t]$ , and $\mathscr U \subseteq \mathscr L$ .

For a step function $\gamma = \sum_i \gamma_i \mathbb I_{[t_{i-1},t_i)}$ with $\gamma_i \ge 0$ (the space $\mathrm{SF}_+$ ), the Parisi PDE

\partial_t\Phi + \tfrac12\xi''(t)\big(\partial_x^2\Phi + \gamma(t)(\partial_x\Phi)^2\big) = 0,\qquad \Phi(1,x) = |x|,

is solved explicitly by the Cole–Hopf recursion (7.3). It is a Gaussian log-moment-generating step on each piece, and a heat-semigroup step where $\gamma_i = 0$ . For general $\gamma \in \mathscr L$ , $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n \to \gamma$ in the weighted norm $\int_0^1\xi''|\gamma_n - \gamma|$ . The Parisi functional is

\mathsf P(\gamma) = \Phi^\gamma(0,0) - \frac12\int_0^1 t\,\xi''(t)\gamma(t)\,dt .

The process $X$ is the strong solution of $dX_t = \xi''(t)\gamma(t)\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$ , $X_0 = 0$ (Eq. (6.3)), driven by a standard Brownian motion $B$ .

Formalization targets

Goal: the monotone minimizer is a minimizer over $\mathscr L$ (Section 6.3, p. 34)

If $\gamma_* \in \mathscr U$ is strictly increasing on $[0,1)$ and $\mathsf P(\gamma_*) \le \mathsf P(\gamma)$ for every $\gamma \in \mathscr U$ , then

\mathsf P(\gamma_*) \le \mathsf P(\gamma)\qquad\text{for every }\gamma \in \mathscr L .

Since $\mathscr U \subseteq \mathscr L$ , this is the paper's main result 2 (p. 4), $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$ under no overlap gap.

Milestones

Lemma 6.7 (p. 27): for $\gamma\in\mathscr L$ , $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$ .
Proposition 6.8 (p. 27): the right derivative of $s\mapsto\mathsf P(\gamma+s\delta)$ at $0$ is $\frac12\int_0^1\xi''(t)\delta(t)\big(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t\big)\,dt$ , for admissible directions $\delta$ that vanish near $t = 1$ .
Lemma 6.15 (p. 33): under no overlap gap, $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\} = t$ for every $t\in[0,1)$ .
Convexity (Section 6.3, p. 34): $\mathsf P$ is convex on $\mathscr L$ .

Significance

The result. The goal identifies the value reached by the paper's message-passing algorithm with the ground-state energy whenever the Parisi minimizer is strictly increasing. Combined with the paper's algorithmic theorem, it yields a $(1-\varepsilon)$ -approximation of $\mathrm{OPT}_N$ in time linear in the input size, for the Sherrington–Kirkpatrick model and any other mixture with no overlap gap (Corollary 2.2). It also gives a structural fact about the variational problem: when the minimizer is strictly increasing, the monotonicity constraint in $\mathscr U$ is not binding.

Formalizing it. The result is proved in the paper, but the proof leans on an external citation ([JT16, Theorem 20]) for convexity of $\mathsf P$ on $\mathscr L$ . It also applies the first-variation formula in a direction that does not meet that formula's stated hypotheses. A machine-checked development closes both gaps. No part of this theory (the Parisi PDE, its Cole–Hopf solution, or the extended functional) has been formalized before, to our knowledge.

Difficulty

The obvious argument is: convexity plus stationarity gives a global minimum. Both inputs are hard. Stationarity (Lemma 6.15) needs the first variation of $\mathsf P$ in directions that keep $\gamma_*+s\delta$ monotone. That variation is a derivative of the solution of a nonlinear PDE with respect to its coefficient, expressed through an SDE driven by that solution's own gradient. Convexity of $\mathsf P$ on $\mathscr L$ is not visible from the formula: $\Phi^\gamma(0,0)$ is defined through a limit of nested Cole–Hopf recursions, and the paper does not prove it, citing a positive-temperature argument instead. Finally, the goal needs the first variation in the direction $\gamma - \gamma_*$ , which is generally non-zero near $t = 1$ , where $\xi''\gamma$ may blow up. Proposition 6.8 as stated excludes such directions.

Formalization scope

Mixture. A coefficient sequence c : ℕ → ℝ with $c_0 = c_1 = 0$ and $\sum_k c_k^2(1+\varepsilon)^k < \infty$ for some $\varepsilon>0$ . $\xi'$ and $\xi''$ are explicit power series.
Order parameters. Functions $\mathbb R\to\mathbb R$ ; membership in $\mathscr U$ and $\mathscr L$ reads only $[0,1)$ . Total variation is eVariationOn; finiteness of integrals is IntegrableOn (which includes measurability).
Cole–Hopf. Step-function data $(m,t,a)$ with $m\ge1$ . The $\gamma_i = 0$ pieces use the heat semigroup, the limit of (7.3). The terminal condition is $|x|$ . Gaussian expectations are integrals against gaussianReal 0 1.
$\Phi^\gamma$ on $\mathscr L$ . limUnder of the Cole–Hopf values along step-function data converging to $\gamma$ in the weighted $L^1$ distance. $\partial_x$ is deriv in $x$ .
SDE. The published definition EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by $0$ after time $1$ . Brownian motion is Mathlib's IsBrownianReal, and expectations are Bochner integrals.
Minimality. Always attainment, $\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma$ in the space, never a real infimum (which Lean sets to $0$ on unbounded sets).
Disclosed hypothesis. Lemma 6.15 assumes that some $c_k \ne 0$ . For $\xi\equiv0$ it is false: $\mathsf P\equiv0$ , $X\equiv0$ , and the left side is constant in $t$ . The goal does not need it.
Ruled out. A formalization that defines $\Phi^\gamma$ as an arbitrary weak solution of the PDE, or via a choice from an unproved existence statement, would make $\mathsf P$ unconstrained. It is not acceptable. Encoding the hypothesis on $\gamma_*$ as minimality over $\mathscr L$ would make the goal trivial.
Proof gaps in the source. Convexity of $\mathsf P$ on $\mathscr L$ is cited, not proved. The step from stationarity to the goal applies Proposition 6.8 outside its stated hypotheses. The statements are the paper's and are believed true.
Out of scope. The paper's algorithmic results (Theorems 2–4, Corollary 2.2) assert algorithms with complexity bounds in an informal computation model, and rest on a long state-evolution analysis. They are not part of this mission.

Contributions welcome: Cole–Hopf regularity (smoothness and the bound $|\partial_x\Phi|\le1$ ), the Lipschitz estimate in $\gamma$ that makes $\Phi^\gamma$ well defined, well-posedness of the SDE, and Itô calculus for the first variation. The Cole–Hopf layer and the SDE well-posedness are reusable for the companion missions on the full-support theorem and the stochastic-control duality of the same paper.

Selected references

A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904v1
A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144(7), 2016. https://arxiv.org/abs/1502.04398
A. Montanari, Optimization of the Sherrington–Kirkpatrick Hamiltonian, FOCS 2019. https://arxiv.org/abs/1812.10897
M. Talagrand, The Parisi formula, Ann. Math. 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
D. Panchenko, The Parisi ultrametricity conjecture, Ann. Math. 177(1), 2013. https://arxiv.org/abs/1112.1003

11 thms1 active userReviewed

Missions

The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs: Fully-Supported Problems Attain the Binomial Violation Tail ExactlyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.4, equation (2.3)

Milestones (PART 1 of §3)

Significance

Difficulty

Formalization scope

Selected references

Convex Optimization: Algorithms and Complexity XVII: Goemans–Williamson Rounding of the MAXCUT SDP Relaxation Has Expected Value at Least 0.878 Times the Maximum CutTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 6.11 (Goemans–Williamson)

Milestones

Companion: Theorem 6.13 (Nesterov)

Significance

Difficulty

Formalization scope

Selected references

Convex Optimization: Algorithms and Complexity XVI: Random Coordinate Descent RCD(γ) on a Strongly Convex Coordinate-Smooth Function Has Rate (1 − 1/κ_γ)^tTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 6.8 (p. 341)

Milestones

Companion: Theorem 6.7 (pp. 339–340)

Significance

Difficulty

Formalization scope

Selected references

Convex Optimization: Algorithms and Complexity XIV: Stochastic Mirror Descent on a β-Smooth Function with Noise σ Has Rate Rσ√(2/t) + βR²/tTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 6.3

Milestones (the proof's four displays)

Companion: Theorem 6.1 and (4.10)

Significance

Difficulty

Formalization scope

Selected references

Convex Optimization: Algorithms and Complexity XIII: Newton's Method Converges Quadratically, ‖x_{k+1} − x*‖ ≤ (M/μ)‖x_k − x*‖², from ‖x₀ − x*‖ ≤ μ/(2M)Textbook

Motivation

Setting

Formalization targets

Goal: Theorem 5.3 (p. 320)

Milestones (p. 321, the steps of the proof)

Significance

Difficulty

Formalization scope

Selected references

Convex Optimization: Algorithms and Complexity X: Nesterov's Accelerated Gradient Descent on a β-Smooth α-Strongly Convex Function Has Rate ((α + β)/2)‖x₁ − x*‖² exp(−(t − 1)/√κ)Textbook

Why accelerated rates matter

Setting

Formalization targets

Goal: Theorem 3.18

Milestones, from the book's proof

Significance

Difficulty

Formalization scope

Selected references

Convex Optimization: Algorithms and Complexity VIII: No Black-Box Method Beats 3β‖x₁ − x*‖²/(32(t + 1)²) on β-Smooth Convex FunctionsTextbook

Why lower bounds for first-order methods

Setting

Formalization targets

Goal: Theorem 3.14 (p. 282)

Milestones (proof of Theorem 3.14, pp. 282–283)

Companion: Theorem 3.13 (p. 280)

Significance

Difficulty

Formalization scope

Selected references

Quantifying Distributional Model Risk via Optimal Transport 1: Strong Duality — the Worst-Case Expectation over an Optimal-Transport Ball on a Polish Space Equals Its Dual over (λ, φ)Research Paper

Motivation

Setting

Formalization targets

Convex Optimization: Algorithms and Complexity XIII: Newton's Method Converges Quadratically, ‖x_{k+1} − x‖ ≤ (M/μ)‖x_k − x‖², from ‖x₀ − x*‖ ≤ μ/(2M)Textbook