Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.99791Formalized record≤ 2.996001Open frontier

3 provers on it3 of 4 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record

6 provers on it7 of 7 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.37134Formalized record≤ 2.371177Open frontier

16 provers on it7 of 8 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.99791Formalized record≤ 2.996001Open frontier

3 provers on it3 of 4 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record

6 provers on it7 of 7 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.37134Formalized record≤ 2.371177Open frontier

16 provers on it7 of 8 missions formalized

All missions

Convex Optimization Operations Research Optimization+1·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 thms2 active usersReviewed

Combinatorics Convex Optimization Optimization+1·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 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Revenue Management with Forward-Looking Buyers: Under Weakly Decreasing Demand the Deterministic Optimal Cutoffs Fall over Time and Satisfy One-Period Look-AheadResearch Paper

Motivation

Retailers of seasonal goods (fashion, electronics, airline seats) sell a fixed stock over a finite season to customers who arrive over time, and those customers know that prices may fall. A customer who expects a markdown waits, and a seller who ignores this loses revenue. The classical revenue-management literature (Gallego and van Ryzin 1994; Talluri and van Ryzin 2004) models myopic customers who buy on arrival or leave; the literature on forward-looking (strategic) buyers, for instance Aviv and Pazgal (2008), studies particular price paths.

Board and Skrzypacz ask the mechanism-design question: among all selling schemes, which maximizes the seller's expected discounted revenue when buyers arrive over time, have private values and time their purchases strategically? Their answer, published in the Journal of Political Economy in 2016, is that the optimal mechanism has a simple structure: in every period the seller sells to the highest remaining buyer if and only if his value exceeds a cutoff that depends only on the period and the number of units left. When demand is weakly decreasing over time, the cutoffs are characterized by one-period indifference conditions, which in the continuous-time limit can be implemented by posted prices. The source used here is the authors' accepted manuscript of February 6, 2015; all page numbers refer to that manuscript.

Setting

A seller has units of a good and sells them over periods $t\in\{1,\dots,T\}$ ; unsold units are worth zero after period $T$ . Payoffs are discounted by $\delta\in(0,1)$ . At the start of period $t$ a random number $N_t$ of buyers arrives, independently across periods, with a law that may depend on $t$ . Each buyer wants one unit; his value is drawn independently from a distribution with continuous density $f$ , distribution function $F$ and support $[\underline v,\bar v]$ . The marginal revenue of a buyer with value $v$ is

m(v)=v-\frac{1-F(v)}{f(v)},

assumed strictly increasing and continuously differentiable, with $m(\underline v)<0$ .

By the standard mechanism-design reduction (§2.1, eq. (2.5)), the seller's problem is to choose when to serve each buyer so as to maximize the expected discounted sum of the served buyers' marginal revenues. The state in period $t$ , after the period- $t$ entrants have arrived, is the number $k$ of units left and the values $y^1\ge y^2\ge\cdots$ of the buyers present. The value $\Pi^k_t$ and the pre-entry value $\tilde\Pi^k_{t}$ satisfy the Bellman equation (4.3):

\Pi^k_t(\mathbf y)=\max_{0\le j\le k}\Big[\sum_{i=1}^j m(y^i)+\delta\,\tilde\Pi^{k-j}_{t+1}(\mathbf y^{-j})\Big],\qquad \tilde\Pi^k_{t+1}(\mathbf y)=E_{t+1}\big[\Pi^k_{t+1}(\mathbf y\cup\mathbf v_{t+1})\big],

where $\mathbf y^{-j}$ is the set of buyers left after the $j$ highest are served and $\mathbf v_{t+1}$ the next period's entrants. Selling one unit to $y^1$ today rather than none gives the difference function

\Delta\Pi^k_t(y^1,\mathbf y^{-1})=m(y^1)+\delta\tilde\Pi^{k-1}_{t+1}(\mathbf y^{-1})-\delta\tilde\Pi^k_{t+1}(y^1,\mathbf y^{-1}),

and the cutoff $x^k_t$ is the smallest $y\in[\underline v,\bar v]$ with $\Delta\Pi^k_t(y,\varnothing)\ge 0$ . Comparing selling to $y^1$ today with waiting and selling at least one unit tomorrow (to the best of $y^1$ and the entrants) gives $D\Pi^k_t(y^1)$ (p. 17). Demand is weakly decreasing in the usual stochastic order if $P(N_{t+1}>x)\le P(N_t>x)$ for all $x$ and $t$ .

Formalization targets

Goal: Theorem 2 (p. 17)

If $N_t$ is weakly decreasing in the usual stochastic order then, for every $k\ge 1$ ,

x^k_{t+1}\le x^k_t\quad(1\le t\le T-1),\qquad D\Pi^k_t(x^k_t)=0,

and $x^k_t$ is the unique root of $D\Pi^k_t$ in $[\underline v,\bar v]$ for $t\le T-1$ : the seller is indifferent between selling to the cutoff type today and waiting one period to sell that unit tomorrow (the one-period-look-ahead property).

Central milestone: Theorem 1 (p. 15)

For every $t$ and $k\ge 1$ , the optimal rule sells to the highest buyer iff $y^1\ge x^k_t$ , whatever the values of the lower buyers; $x^{k+1}_t\le x^k_t$ ; and $x^k_t$ is the unique root of $\Delta\Pi^k_t$ .

Milestones

In attack order:

Lemma 1: allocations are monotone in values.
Lemma 2: with cutoffs decreasing in the unit index, units can be treated one at a time.
Equation (A.1): increasing differences of $\Pi$ .
Lemma 3: $\Delta\Pi$ is independent of lower buyers, continuous and strictly increasing in $y^1$ , and increasing in $k$ .
Footnote 12: the boundary values of $\Delta\Pi$ .
Theorem 1.
Strict monotonicity of $D\Pi$ in $y^1$ (p. 18).
Lemma 4: $D\Pi^k_{t+1}\ge D\Pi^k_t$ .

After the goal, (4.7) gives the period- $(T-1)$ cutoff equation $m(x^k_{T-1})=\delta E_T[\max\{m(x^k_{T-1}),m(v^k_T)\}]$ .

Significance

Theorem 1 says that the optimal allocation does not depend on how many buyers are present or what their values are, only on time and inventory. This is what makes the optimal mechanism implementable without eliciting values from buyers as they arrive. Theorem 2 turns the global dynamic program into local indifference conditions. In the continuous-time limit (§5 of the paper) these become differential equations, and the optimum is implemented by posted prices with an auction at the end of the season. Under weakly decreasing demand, therefore, the classical revenue-management practice of posting prices loses nothing against the best possible mechanism.

The paper's results are proved, in prose, with envelope-theorem and coupling arguments. They have not been machine-checked. A formal development would produce a verified backward-induction model of multi-unit dynamic allocation with random arrivals, with the structural results (monotonicity, deterministic cutoffs, monotone comparative statics in inventory and time) that recur across dynamic pricing and optimal stopping. Two printed gaps are recorded below: the positivity of $m(\bar v)$ , and the restriction of footnote 12 to $t\le T-1$ .

Difficulty

The obvious argument fails at "deterministic". A priori the cutoff for the highest buyer depends on the values of the lower buyers, because selling a unit today changes which of them will be served later and when. Lemma 3(a) holds only under the induction hypothesis that all future cutoffs are already deterministic and decreasing in inventory, so Lemma 3, Theorem 1 and (A.1) form a single backward induction over periods and units, and none of them can be proved in isolation. The value function is an expectation, over a random number of i.i.d. entrants, of a maximum over sorted values, so continuity and strict monotonicity in $y^1$ (Lemma 3(b), and the same for $D\Pi$ ) are not available from general facts. The tempting argument for Theorem 2, that cutoffs fall over time simply because fewer buyers arrive later, is incomplete: Lemma 4 has to compare two periods with different arrival laws and different future cutoffs at once.

Formalization scope

Periods are natural numbers $1,\dots,T$ with $T\ge1$ , and units are natural numbers. Values, marginal revenues and profits are real numbers. The buyers present form a finite multiset of reals, and an absent buyer is absent, never a value $0$ . The value law is the measure with density $f$ ; the density is positive and continuous on $[\underline v,\bar v]$ and zero outside, and $m$ is defined from $f$ and $F$ . Expectations over a cohort are lower Lebesgue integrals against $\sum_n P(N_t=n)\,\mu^{\otimes n}$ of nonnegative bounded quantities, so no non-measurable or non-integrable integrand can silently become $0$ . The value function is defined by the Bellman equation (4.3), with $\Pi_{T+1}\equiv0$ . The sequence problem (4.1) over purchase times is not formalized; the paper says either may be used (footnote 16).

Standing assumptions and handled gaps:

$\delta\in(0,1)$ ;
$N_t$ independent across periods (only the marginal laws enter);
$m$ strictly increasing and $C^1$ on $[\underline v,\bar v]$ with $m(\underline v)<0$ ;
added: $m(\bar v)>0$ , which footnote 12 uses without stating; without it no unit is ever sold and no cutoff exists;
added: $f>0$ on the closed support, needed for $m$ to be defined there;
footnote 12's equality $\Delta\Pi^k_t(\bar v)=(1-\delta)m(\bar v)$ is stated for $t\le T-1$ only, since $\Delta\Pi^k_T=m$ ;
$D\Pi^k_t$ is used only for $t\le T-1$ , and Lemma 4 needs $t+1\le T-1$ ;
"decreasing" and "increasing" are weak except in Lemma 3(b) and for $D\Pi$ ;
at $y^1=x^k_t$ both selling and waiting are optimal.

The cutoff is defined from $\Delta\Pi$ , never as the threshold of an optimal policy, and "optimal" always means maximal in (4.3) over every number of units sold. A formalization that postulates a threshold policy, replaces the random cohort by its mean, or sets absent buyers to value $0$ would trivialize or change the statements and is ruled out. The mechanism-design reduction (IC/IR to (2.5)) and the continuous-time results of §5 are out of scope.

The usual stochastic order is the published platform definition StochasticOrders.Usual.UsualOrder. A complete development needs finite-horizon dynamic programming over multisets, expectations of functions of sorted i.i.d. samples, envelope arguments, and monotone coupling for the usual stochastic order on $\mathbb N$ ; these parts are reusable beyond this mission. Proofs of any milestone are welcome, as is a proof that (4.3) agrees with the sequence problem (4.1).

Selected references

S. Board and A. Skrzypacz, Revenue Management with Forward-Looking Buyers, Journal of Political Economy 124(4), 2016. https://doi.org/10.1086/686713
R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 1994. https://doi.org/10.1287/mnsc.40.8.999
Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3), 2008. https://doi.org/10.1287/msom.1070.0183
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000
M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

14 thms2 active usersReviewed

Convex Optimization Machine Learning Optimization+1·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XV: SVRG with η = 1/(10β) and k = 20κ Contracts the Expected Optimality Gap by 0.9 per EpochTextbook

Motivation

Many optimization problems in machine learning minimize an average of losses, one loss for each observation. A full gradient step examines every observation, while a stochastic gradient step examines one. The latter is cheaper per step, but its sampled gradient can remain noisy even near the optimum. Section 6.3 of Bubeck's monograph studies stochastic variance reduced gradient descent (SVRG), which periodically computes a full gradient at an anchor point and uses it to correct subsequent sampled gradients. The question for this mission is whether that correction gives a geometric reduction of the expected objective gap at the constants printed in Theorem 6.5.

Bubeck places this method alongside full gradient descent and stochastic gradient descent for finite sums. The section records that earlier stochastic average gradient and dual coordinate ascent methods attain a gradient-computation cost of order $(m+\kappa)\log(1/\varepsilon)$ for the same regime, where $m$ is the number of components and $\kappa$ is a condition number. The target here is the precise SVRG convergence statement in the book, rather than a comparison of implementation costs. The source's discussion on pp. 334–336 gives the context and the algorithm.

Setting

Let $f_1,\ldots,f_m:\mathbb R^n\to\mathbb R$ be differentiable convex functions, with $m\ge1$ , and define the finite-sum objective and its gradient by

f(x)=\frac1m\sum_{i=1}^m f_i(x),\qquad G(x)=\frac1m\sum_{i=1}^m \nabla f_i(x).

Each component is $\beta$ -smooth when its gradient is $\beta$ -Lipschitz in the Euclidean norm: $\|\nabla f_i(x)-\nabla f_i(z)\|_2\le\beta\|x-z\|_2$ for all $x,z$ . The average $f$ is $\alpha$ -strongly convex, meaning that for all $x,z$ it lies at least $\frac\alpha2\|z-x\|_2^2$ above its first-order affine approximation at $x$ . The constants $\alpha$ and $\beta$ are positive, $x^*$ minimizes $f$ over $\mathbb R^n$ , and $\kappa=\beta/\alpha$ .

An epoch begins at an anchor $y$ . Its first inner iterate is $x_1=y$ . For $t=1,\ldots,k$ , draw $i_t$ uniformly from $\{1,\ldots,m\}$ , independently across steps and epochs, and update

x_{t+1}=x_t-\eta\bigl(\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)+G(y)\bigr).

The next anchor is the average $y^+=k^{-1}\sum_{t=1}^k x_t$ . In particular, this average uses $x_1$ through $x_k$ , while the last updated point $x_{k+1}$ is excluded. Starting from an arbitrary $y^{(1)}$ and repeating the epoch produces $y^{(s+1)}$ . The expectation of $f(y^{(s+1)})$ is over all $sk$ sampled indices in the first $s$ epochs.

Formalization targets

Goal: geometric contraction across epochs

Theorem 6.5 sets $\eta=1/(10\beta)$ and $k=20\kappa$ and asserts, for every $s\ge1$ ,

\mathbb E f(y^{(s+1)})-f(x^*) \le 0.9^s\bigl(f(y^{(1)})-f(x^*)\bigr).

The epoch length is a count, so the statement takes $k\in\mathbb N$ and explicitly requires $k=20\beta/\alpha$ . The goal uses exactly the book's step size, epoch length, and contraction factor.

Milestones: second moments and a single epoch

Lemma 6.4 bounds $\mathbb E_i\|\nabla f_i(x)-\nabla f_i(x^*)\|_2^2$ by $2\beta(f(x)-f(x^*))$ . Equation (6.3) bounds the second moment of the corrected sampled direction by the objective gaps at the current point and the anchor. Equation (6.2), the unbiased-direction display, and the one-step display express how that direction changes squared distance to $x^*$ . The later display on p. 338 bounds one epoch for any positive step size with $2\beta\eta<1$ . Finally, equation (6.1) substitutes the stated constants to obtain the factor $0.9$ for one epoch. These seven source claims form the milestone list in reading order.

Significance

The theorem gives an explicit accuracy guarantee after a specified number of epochs: an initial gap $D$ falls below $0.9^sD$ in expectation. Because each epoch uses a full gradient at its anchor as well as sampled component gradients, the result makes clear which quantity contracts and which operations are counted. It is a concrete linear-rate statement for a method whose individual stochastic gradients need not approach zero at the optimum. Bubeck, §6.3 discusses this issue when introducing the correction term.

The mathematical result is already proved in the monograph. The remaining task is to produce machine-checked proofs of its precise finite-sum model, the single-index estimates, the epoch inequality, and the full repeated-epoch guarantee. The mission drafts those statements and definitions; no proof is claimed for the open theorem items. The finite uniform-average representation and the separation between a conditional one-step average and the full multi-epoch average can be reused in other finite-sum stochastic algorithms.

Difficulty

The sampled component gradient $\nabla f_{i_t}(x_t)$ need not be small when $x_t$ is near $x^*$ , so a bound using only its norm does not yield the desired fixed-step contraction. The correction $-\nabla f_{i_t}(y)+G(y)$ has mean zero relative to the full gradient at the current iterate, but its second moment still depends on both $x_t$ and $y$ . The proof must control those two gaps while respecting the fact that $x_t$ depends on earlier samples. A single-index estimate with $x_t$ held fixed and an expectation over complete sample histories are different statements; confusing them would make the goal weaker or false.

Formalization scope

The carrier is EuclideanSpace ℝ (Fin n) with its usual inner product and norm. The Fin m components and every sample array are finite. A real-valued uniform average is an ordinary finite sum divided by the number of arrays, and $m\ge1$ and $k\ge1$ prevent an empty average. Independent uniform sampling is represented by averaging over every function from step positions to component indices. The multi-epoch sample space has one such block for every epoch. There are no integrals or measurability side conditions.

The component assumptions include differentiability with an explicit gradient map, convexity on all of $\mathbb R^n$ , and the book's gradient-Lipschitz version of smoothness. Strong convexity is imposed on the average objective alone, using the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn definition on the whole space. The book's standing notation assumes a minimizing $x^*$ exists; this is explicit. Positivity of $\alpha$ and $\beta$ , and integrality of $20\beta/\alpha$ , make the displayed divisions and epoch length meaningful. The general epoch bound also requires $0<\eta$ and $2\beta\eta<1$ . Dimension zero is allowed: the theorem remains a statement about the unique point of $\mathbb R^0$ and its zero objective gap.

The direction always contains the sampled difference $\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)$ and the full anchor gradient $G(y)$ . Replacing that direction with $G(x_t)$ would define gradient descent and would not satisfy this mission's algorithm. Contributions are welcome for the finite averaging identities, the component-gradient estimate, the conditional one-step calculation, the epoch inequality, and the induction across epochs.

Selected references

Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 2015, pp. 231–358. arXiv:1405.4980v2
Rie Johnson and Tong Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, Advances in Neural Information Processing Systems 26 (NIPS), 2013 (the origin of SVRG, cited by Bubeck on p. 335). https://proceedings.neurips.cc/paper/2013/hash/ac1dd209cbcc5e5d1c6e28598e8cbbe8-Abstract.html

10 thms2 active usersReviewed

Convex Optimization Machine Learning Optimization+1·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 thms2 active usersReviewed

Convex Optimization Numerical Analysis Optimization·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 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·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 thms2 active usersReviewed

Completed

Machine Learning Optimal Transport Optimization+1·Captain: mikedeng1

Robust Wasserstein Profile Inference and Applications to Machine Learning 2: ℓp-Regularized Logistic Regression and the Hinge-Loss SVM Are Wasserstein DRO under a Label-Preserving Transport CostResearch Paper

Motivation

Regularized logistic regression and the support vector machine (SVM) are two of the most widely used linear classifiers. Both are usually introduced as empirical risk minimization plus a norm penalty $\|\beta\|_p$ whose size is tuned by cross-validation, with the penalty justified heuristically as a guard against overfitting. Distributionally robust optimization (DRO) offers a different reading: instead of minimizing the average loss on the training sample, minimize the worst average loss over all distributions close to the empirical one. Blanchet, Kang and Murthy (arXiv:1610.05627v4; J. Appl. Probab. 56(3), 2019) show that, for a suitable notion of closeness based on optimal transport, the robust problem and the penalized problem coincide exactly. The penalty is then the price of robustness against perturbations of the predictors, and the regularization parameter becomes the radius of an uncertainty set, which the same paper later chooses by a statistical criterion (the robust Wasserstein profile).

Related earlier work: Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) studied Wasserstein-robust logistic regression with a metric that charges a finite price $\kappa$ for flipping a label, and obtained regularized logistic regression only in the limit $\kappa \to \infty$ . The result formalized here is the exact statement at $\kappa = \infty$ , together with the analogous statement for the hinge loss.

Setting

Training data are pairs $(X_1,Y_1),\dots,(X_n,Y_n)$ with predictors $X_i \in \mathbb R^d$ and labels $Y_i \in \{-1,+1\}$ , $n \ge 1$ . Their empirical distribution is $P_n = \frac1n\sum_{i=1}^n \delta_{(X_i,Y_i)}$ , a probability measure on $Z = \mathbb R^d \times \mathbb R$ .

For a cost $c : Z \times Z \to [0,\infty]$ , the optimal transport cost between probability measures $P$ and $Q$ on $Z$ is

D_c(P,Q) = \inf\big\{\mathbb E_\pi[c(U,W)] : \pi \text{ a probability measure on } Z\times Z,\ \pi_U = P,\ \pi_W = Q\big\}.

The cost used here is the label-preserving cost: for $q \in [1,\infty]$ ,

N_q\big((x,y),(u,v)\big) = \|x - u\|_q \text{ if } y = v, \qquad +\infty \text{ otherwise}.

Every distribution $P$ with $D_{N_q}(P,P_n) < \infty$ has the same label distribution as $P_n$ ; only the predictors are perturbed. The exponent $p$ is the conjugate of $q$ , $1/p + 1/q = 1$ .

The losses are the log-exponential loss $\log(1 + e^{-y\beta^T x})$ and the hinge loss $(1 - y\beta^T x)^+$ , for a coefficient vector $\beta \in \mathbb R^d$ . The worst-case expected loss at radius $\delta \ge 0$ is $\sup\{\mathbb E_P[l] : D_{N_q}(P,P_n) \le \delta\}$ , the supremum over probability measures $P$ on $Z$ .

Formalization targets

Goal: Theorem 2 (p. 11)

For every $\delta \ge 0$ and every $\beta \in \mathbb R^d$ ,

\sup_{P:\ D_{N_q}(P,P_n)\le\delta} \mathbb E_P\big[\log(1 + e^{-Y\beta^T X})\big] = \frac1n\sum_{i=1}^n \log(1 + e^{-Y_i\beta^T X_i}) + \delta\|\beta\|_p,

\sup_{P:\ D_{N_q}(P,P_n)\le\delta} \mathbb E_P\big[(1 - Y\beta^T X)^+\big] = \frac1n\sum_{i=1}^n (1 - Y_i\beta^T X_i)^+ + \delta\|\beta\|_p,

and consequently the two identities obtained by taking $\inf_{\beta}$ on both sides, which is how the paper prints the theorem.

Milestones

Proposition 1 (p. 10): strong duality, $\sup_{P: D_c(P,P_n)\le\delta}\mathbb E_P[l] = \min_{\gamma\ge0}\{\gamma\delta + \frac1n\sum_i\varphi_\gamma(X_i,Y_i)\}$ with $\varphi_\gamma(z_0) = \sup_z\{l(z) - \gamma c(z,z_0)\}$ , for a lower semicontinuous cost vanishing on the diagonal, an upper semicontinuous loss and $\delta > 0$ .
Logistic inner supremum (proof of Theorem 2, p. 30): $\sup_x\{\log(1+e^{-y_0\beta^T x}) - \lambda\|x - x_0\|_q\}$ equals the loss at $x_0$ if $\|\beta\|_p \le \lambda$ and $+\infty$ otherwise.
Logistic outer minimisation (p. 30): the infimum over $\lambda \ge 0$ of $\delta\lambda$ plus the average of these suprema equals the regularized empirical loss.
Hinge inner supremum (pp. 30–31) and 5. hinge outer minimisation (p. 31): the same two steps for the hinge loss.

Significance

The theorem identifies two standard estimators as exact solutions of a robust decision problem. Consequences: the penalty $\delta\|\beta\|_p$ has a quantitative meaning (the adversary's transport budget), the regularization parameter can be chosen by the paper's robust Wasserstein profile instead of cross-validation, and the norm of the penalty is tied to the geometry of the perturbations (perturbations measured in $\ell_\infty$ give an $\ell_1$ penalty). The same identity is the input of the paper's coverage bound (Proposition 6) for $\rho = 1$ .

The result is proved on paper; no machine-checked version is known. The formalization adds a precise statement of the objects involved (couplings with both marginals fixed, an infinite cost across labels, expectations of nonnegative losses with values in $[0,\infty]$ ), a checked version of the duality step specialised to this cost, and the treatment of boundary cases ( $\delta = 0$ , $\beta = 0$ , $q \in \{1,\infty\}$ ) that the paper does not discuss.

Difficulty

The identities are short once Proposition 1 is available, so the weight of the mission lies in two places. First, Proposition 1 itself is a strong duality theorem for optimal transport over all probability measures on $\mathbb R^{d+1}$ , with a cost that takes the value $+\infty$ and an unbounded loss, and with attainment of the dual minimum; it is quoted from Blanchet and Murthy (Math. Oper. Res. 2019) and not proved in this paper. The weak-duality inequality is routine; the reverse inequality requires constructing near-optimal distributions from the dual, which needs measurable selection of near-maximizers and does not follow from finite-dimensional convex duality. Second, the inner suprema require an exact Hölder-attainment argument for the pair of conjugate norms $\ell_p$ and $\ell_q$ , including $q = 1$ and $q = \infty$ , and for the hinge loss a minimax exchange over $\alpha \in [0,1]$ . Bypassing duality by a direct construction of the worst distribution is possible for the upper value but not obviously for the lower bound at the boundary $\lambda = \|\beta\|_p$ .

Formalization scope

Predictors are Fin d → ℝ, a data point is (Fin d → ℝ) × ℝ with the product Borel σ-algebra, and samples are indexed by Fin n with 0 < n. Labels are real numbers with the hypothesis $Y_i \in \{-1,+1\}$ , which Theorem 2 inherits from Example 2; the cost $N_q$ is defined on all of $\mathbb R^d\times\mathbb R$ .
The $\ell_q$ norm is the norm of PiLp q, with q p : ℝ≥0∞ and p.HolderConjugate q; $q = 1$ and $q = \infty$ are included, and no further restriction on $q$ is imposed.
The transport cost is an infimum in $[0,\infty]$ over probability measures on $Z\times Z$ with both marginals fixed. Expectations are lower Lebesgue integrals of the nonnegative losses, and the worst case is a supremum in $[0,\infty]$ over probability measures. The empirical distribution is the published platform definition WassersteinDRO.Regularization.empiricalDistribution.
Readings. The paper prints the SVM identity without $\inf_\beta$ on the right; the goal states the per- $\beta$ identities (what the proof establishes) and the identities of infima with $\inf_\beta$ on both sides. The proof's displays write the transport norm as $\|\cdot\|_p$ and the penalty as $\|\beta\|_q$ , the reverse of the theorem; milestones use the theorem's convention. The logistic chain's printed indicators $\mathbf 1_{\{\lambda>\|\beta\|\}}$ , $\infty\mathbf 1_{\{\lambda\le\|\beta\|\}}$ should read $\ge$ and $<$ ; the stated end-to-end identity is unaffected. Proposition 1 is stated with a fixed nonnegative loss and $\delta > 0$ .
A trivializing formalization is ruled out: a cost infimum over sub-probability couplings or with one marginal free, or a Bochner expectation that vanishes on non-integrable laws, would make the worst case $+\infty$ or $0$ ; the definitions here fix both marginals, use probability measures only and integrate in $[0,\infty]$ . At $\delta = 0$ the ball is $\{P_n\}$ and both sides reduce to the empirical loss.
Infrastructure needed: optimal-transport duality with extended-valued lower semicontinuous costs (reusable well beyond this mission), Hölder equality cases for PiLp, and calculus for the logistic function. Contributions to any of these are welcome, as are proofs of the inner suprema, which are independent of Proposition 1.

Selected references

J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019; arXiv:1610.05627v4. https://arxiv.org/abs/1610.05627
J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, NIPS 2015. https://arxiv.org/abs/1509.09259

12 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·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 thms2 active usersReviewed

Completed

Operations Research Optimization 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 thms2 active usersReviewed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

A Robust Optimization Approach to Inventory Theory: The Optimal Robust Policy Is the Optimal Nominal Policy for an Explicit Modified Demand, at Extra Cost (2ph/(p+h))·ΣA_kResearch Paper

Motivation

Classical inventory theory chooses order quantities against a probability distribution of demand. The resulting dynamic programs are optimal in expectation but need the distribution, and they become intractable once several installations, capacities or fixed costs interact. Robust optimization replaces the distribution by an uncertainty set and asks for the order sequence whose worst-case cost over that set is smallest. Bertsimas and Thiele (Operations Research 54(1), 2006) applied the budget-of-uncertainty approach of Bertsimas and Sim (The Price of Robustness, Operations Research 52(1), 2004) to finite-horizon inventory control. Their main structural result says that robustness does not destroy the structure of the classical problem. The robust problem is a deterministic (nominal) inventory problem with an explicitly modified demand, and the price of robustness is an explicit constant.

Setting

A single item is ordered at a single installation over periods $k = 0, \dots, T-1$ . The stock at the beginning of the horizon is $x_0$ . Orders $u_k \ge 0$ arrive immediately, demand $w_k$ is subtracted, and excess demand is backlogged, so the stock at the end of period $k$ is

x_{k+1} = x_0 + \sum_{i=0}^{k} (u_i - w_i).

The demand of period $k$ is uncertain: $w_k = \bar w_k + \hat w_k z_k$ with a nominal demand $\bar w_k$ , a maximal deviation $\hat w_k \ge 0$ and a scaled deviation $z_k \in [-1, 1]$ . A budget of uncertainty $\Gamma_k$ limits the total scaled deviation up to period $k$ . The budgets satisfy $0 \le \Gamma_0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$ .

Each period costs $C(u_k) + R(x_{k+1})$ . The purchasing cost is $C(u) = K + cu$ for $u > 0$ and $C(0) = 0$ , with $c > 0$ and $K \ge 0$ . The holding/shortage cost is $R(x) = \max(hx, -px)$ , with $h \ge 0$ and $p > c$ . The nominal problem with demand $w$ minimizes $\sum_{k<T} (C(u_k) + R(x_{k+1}))$ over $u \ge 0$ for a fixed demand sequence $w$ .

For each $k$ , $A_k$ is the optimal value of the linear program

A_k = \max\Big\{\sum_{i=0}^{k} \hat w_i z_i \;:\; \sum_{i=0}^{k} z_i \le \Gamma_k,\ 0 \le z_i \le 1\Big\} \qquad (13)

It is the worst-case deviation of the cumulative demand up to $k$ from its nominal value, with $A_{-1} = 0$ . Write $\bar x_{k+1} = x_0 + \sum_{i\le k}(u_i - \bar w_i)$ for the nominal stock. The robust formulation (14) minimizes $\sum_{k<T} (C(u_k) + y_k)$ over $(u, y, q, r)$ subject to the following constraints for every $k < T$ :

$u_k \ge 0$ , $q_k \ge 0$ , and $r_{ik} \ge 0$ , $q_k + r_{ik} \ge \hat w_i$ for $i \le k$ ;
$y_k \ge h(\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$ ;
$y_k \ge p(-\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$ .

The variables $q, r$ are the dual of (13). Formulation (14) is equivalent to requiring the holding and shortage constraints of period $k$ for every demand whose scaled deviations satisfy $|z_i| \le 1$ and $\sum_{i \le k}|z_i| \le \Gamma_k$ .

Formalization targets

Goal: Theorem 3.2 (a), (b), (d)

Let the modified demand be

w'_k = \bar w_k + \frac{p-h}{p+h}\,(A_k - A_{k-1}). \qquad (20)

Write $N_{w'}(u)$ for the nominal cost of $u$ under demand $w'$ . Then:

For every $u \ge 0$ , the minimum of the objective of (14) over the feasible $(y, q, r)$ is attained and equals

N_{w'}(u) + \frac{2ph}{p+h}\sum_{k=0}^{T-1} A_k.

$u$ is the order part of an optimal solution of (14) if and only if $u$ is optimal for the nominal problem with demand $w'$ .
The optimal cost of (14) is the optimal nominal cost under $w'$ plus $\frac{2ph}{p+h}\sum_k A_k$ .
If $K = 0$ and $w'_k \ge 0$ , the order-up-to policy with levels $S_k = w'_k$ is robust-optimal.

Milestones

The milestones are the steps of the paper's proof, in order:

LP (13) and its dual are attained with the common value $A_k$ .
The constraints of (14) are the robust counterpart of the $k$ -th holding/shortage pair (10)–(11).
For fixed orders, the value of (14) is the sum (21).
The modified stock (22) satisfies $x'_{k+1} = \bar x_{k+1} - \frac{p-h}{p+h}A_k$ .
The max identity (23): $\max(h(\bar x+A), p(-\bar x+A)) = \max(hx', -px') + \frac{2ph}{p+h}A$ .
Lemma 3.1(b): for nonnegative demand, the nominal problem without fixed cost is solved by ordering up to $S_k = w_k$ .
Remark 1: $A_{k-1} \le A_k$ , so $w'_k \ge \bar w_k$ when $p \ge h$ .
Remark 3: under i.i.d. demand, $A_k = \hat w\Gamma_k$ , which gives the closed-form thresholds.

Significance

The theorem reduces robust inventory control to nominal inventory control. Every structural fact known for the deterministic problem then transfers to the robust one. These include the optimality of base-stock policies without fixed cost and the threshold structure with a fixed cost. The robust base-stock levels are explicit: they shift the nominal levels by $\frac{p-h}{p+h}(A_k - A_{k-1})$ , upward when shortage is more expensive than holding. The extra cost $\frac{2ph}{p+h}\sum_k A_k$ quantifies the price of protection as a function of the budgets. The paper uses the same reduction for capacitated orders (Theorem 3.3) and for supply networks (§4).

The result has been proved since 2006, and no machine-checked proof of it, or of any budgeted robust counterpart, is known to exist. This mission provides several formalizations for reuse:

the budgeted robust counterpart of a pair of piecewise-linear constraints;
the duality of the fractional knapsack LP (13);
the optimality of base-stock orders for a deterministic backlogged inventory problem.

Difficulty

The algebraic core, identity (23), is elementary. The work is in the reductions around it. The first is that (14) really is the worst case of (10)–(11): this needs strong duality for (13), together with attainment on both sides, and the observation that the minimizing and maximizing deviations of a constraint pair differ. The second is that the minimum of (14) over the auxiliary variables, for fixed orders, is (21). This requires the dual optimum to be attained with the value of (13), and $h, p \ge 0$ so that the cost is monotone in $A_k$ . The third is the base-stock part, which needs Lemma 3.1(b), a global optimality statement for a $T$ -period problem with backlogging. The paper proves that lemma by an explicit dual certificate. An argument through first-order conditions in each period is not enough, because orders in one period affect every later stock level.

Formalization scope

All data are real numbers and sequences are ℕ → ℝ; only indices $k < T$ matter. stock w u k denotes $x_{k+1}$ , the stock at the end of period $k$ . The standing assumptions of §3.1 are fields of the model:

$c > 0$ , $K \ge 0$ , $h \ge 0$ , $p > c$ ;
$\hat w_k \ge 0$ ;
$\Gamma_0 \ge 0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$ .

The conventions and corrections are:

Fixed cost. The paper writes it with binary variables and a big- $M$ constraint. Here it is the indicator $C(u_k)$ in the objective, as in the paper's own (21).
"Optimal". It always means minimality over all feasible points.
The policy. It is the order sequence chosen at time 0.
$A_k$ . It is the value of (13), as in Remark 1 after the theorem, not "the optimal $q^*, r^*$ of (14)", which need not be unique.
The robust formulation. (14) is formalized as printed: the $k$ -th constraint pair is protected by the budget $\Gamma_k$ alone, not by the intersection of all budgets up to $k$ .
Sign slip. The page's $x_{k+1} = \bar x_{k+1} + \sum \hat w_i z_i$ is a sign slip for $\bar x_{k+1} - \sum \hat w_i z_i$ . The formal statements use the correct sign; the result is unaffected because the deviation set is symmetric.
Part (b). It is stated under $w'_k \ge 0$ . As printed it fails when $p < h$ makes $w'$ negative, for example $T = 2$ , $\bar w = \hat w = (10, 0)$ , $\Gamma = (0, 1)$ , $c = 1$ , $h = 4$ , $p = 2$ , $x_0 = 0$ . Lemma 3.1(b) carries the matching hypothesis of nonnegative demand.
Remark 3. It adds $\Gamma_0 \le 1$ .
Remark 1. Its inequalities are weak.
Not stated. The (s, S) clause of (a) and part (c) are excluded. They rest on a stochastic theorem cited from Bertsekas (1995) and on thresholds stated through the optimal ordering times.

A trivializing formalization is ruled out: the robust cost is formulation (14) with its variables $y, q, r$ , and $A_k$ is the value of LP (13). Neither is the closed-form objective (21) nor an arbitrary sequence. Contributions are welcome on the LP duality of (13) (a fractional knapsack), on the robust counterpart milestone, and on Lemma 3.1(b), each of which is independent of the others.

Selected references

D. Bertsimas, A. Thiele, A Robust Optimization Approach to Inventory Theory, Operations Research 54(1):150–168, 2006. https://doi.org/10.1287/opre.1050.0238
D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1):35–53, 2004. https://doi.org/10.1287/opre.1030.0065
A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. 1, Athena Scientific, 1995.

12 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity VII: Conditional Gradient Descent (Frank–Wolfe) with γ_s = 2/(s + 1) Has Rate 2βR²/(t + 1) in Any NormTextbook

Motivation

Many constrained optimization problems in machine learning and statistics have a feasible set $\mathcal X$ over which a linear function is cheap to minimize but a Euclidean projection is expensive: the $\ell_1$ -ball, the simplex, the nuclear-norm ball, the convex hull of a combinatorial family. Projected gradient descent needs a projection at every step. Conditional gradient descent, introduced by Frank and Wolfe in 1956 for quadratic programming, replaces the projection by a call to a linear minimization oracle over $\mathcal X$ , and its iterates are convex combinations of oracle outputs, which makes them sparse when $\mathcal X$ is a polytope.

This mission is the seventh 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 Section 3.3, whose main result, Theorem 3.8, is the $O(1/t)$ rate of the method in the form given by Jaggi (2013), going back to Dunn and Harshbarger (1978).

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ . For a linear form $g$ on $E$ , written $v\mapsto g^\top v$ , the dual norm is $\|g\|_*=\sup_{\|v\|\le1}g^\top v$ . Let $\mathcal X\subseteq E$ be nonempty, compact and convex, with diameter $R=\sup_{x,y\in\mathcal X}\|x-y\|$ .

Let $f:E\to\mathbb R$ be differentiable with gradient $\nabla f(x)$ , a linear form on $E$ . For $\beta\ge0$ , $f$ is β-smooth with respect to $\|\cdot\|$ on $\mathcal X$ if

\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|\qquad(x,y\in\mathcal X).

A point $x^*\in\mathcal X$ with $f(x^*)=\min_{x\in\mathcal X}f(x)$ is fixed throughout, and $\delta_t=f(x_t)-f(x^*)$ .

Given step sizes $(\gamma_s)_{s\ge1}$ , a run of conditional gradient descent is a pair of sequences with $x_1\in\mathcal X$ and, for every $t\ge1$ ,

y_t\in\operatorname*{argmin}_{y\in\mathcal X}\nabla f(x_t)^\top y\quad(3.8),\qquad x_{t+1}=(1-\gamma_t)x_t+\gamma_ty_t\quad(3.9).

The minimizer $y_t$ need not be unique; any choice is allowed.

Formalization targets

Goal: Theorem 3.8 (p. 272)

If $f$ is convex and $\beta$ -smooth with respect to $\|\cdot\|$ and $\gamma_s=\frac{2}{s+1}$ for $s\ge1$ , then every run satisfies, for every $t\ge2$ ,

f(x_t)-f(x^*)\le\frac{2\beta R^2}{t+1}.

Milestones

Inequality (3.4) in an arbitrary norm (p. 267, used on p. 272): for $x,y\in\mathcal X$ , $0\le f(x)-f(y)-\nabla f(y)^\top(x-y)\le\frac{\beta}{2}\|x-y\|^2$ .
The one-step recursion (pp. 272–273): for any run with $\gamma_s\in[0,1]$ ,

\delta_{s+1}\le(1-\gamma_s)\delta_s+\frac{\beta}{2}\gamma_s^2R^2 .

Initialization (p. 273): if $\gamma_1=1$ , then $\delta_2\le\frac{\beta}{2}R^2$ .
The induction (p. 273): a real sequence with $\delta_2\le\frac{\beta}{2}R^2$ and the recursion of milestone 2 with $\gamma_s=\frac{2}{s+1}$ for $s\ge2$ satisfies $\delta_t\le\frac{2\beta R^2}{t+1}$ for $t\ge2$ .

Significance

Theorem 3.8 is the basic guarantee for projection-free first-order optimization. Its rate does not depend on the dimension, and it depends on the geometry only through the product $\beta R^2$ , both measured in the same norm, which may be chosen to fit $\mathcal X$ : for the $\ell_1$ -ball, smoothness in $\|\cdot\|_1$ with dual norm $\|\cdot\|_\infty$ gives much better constants than the Euclidean analysis. The book applies it this way to a LASSO-type problem (Section 3.3, pp. 274–276), and the same bound underlies the sparse-approximation corollary on the simplex (p. 273) and the many later variants of the method (away steps, stochastic and online conditional gradient).

The result is classical and proved in the book. What this mission adds is a machine-checked statement and proof in an arbitrary finite-dimensional normed space, with the dual norm as the operator norm on linear forms, and a reusable encoding of norm-smoothness and of conditional gradient runs. On Prove2Me a related result is already proved: Lan's Theorem 7.1 (First-order and Stochastic Optimization Methods), which bounds $f(y_k)-f^*$ by $\frac{2L}{k(k+1)}\sum_{i\le k}\|x_i-y_{i-1}\|^2$ with a different indexing; after the diameter bound it yields $2\beta R^2/t$ at Bubeck's iterate $x_t$ , which is weaker than Theorem 3.8 by one step.

Difficulty

The difficulty is in the bookkeeping of norms and indices, not in a deep idea. Inequality (3.4) is proved in the book only for the Euclidean norm, where $\nabla f(x)\in\mathbb R^n$ and the Cauchy–Schwarz inequality is used; in a general norm it needs the pairing between a linear form and a vector and the bound $|g^\top v|\le\|g\|_*\|v\|$ . The rate $2\beta R^2/(t+1)$ is attained only by starting the induction at $t=2$ , where the step $\gamma_1=1$ erases the dependence on the starting point; at $t=1$ the bound can fail, since $\delta_1$ is arbitrary. A first attempt that runs the induction from $t=1$ with an arbitrary $\delta_1$ does not give the stated constant.

Formalization scope

$E$ is a type with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]; nothing is specialised to the Euclidean norm. The gradient is an explicit derivative map f' : E → (E →L[ℝ] ℝ) with HasFDerivAt f (f' x) x for every x; $\nabla f(x)^\top v$ is f' x v, and $\|\cdot\|_*$ is the operator norm, which equals $\sup_{\|v\|\le1}g^\top v$ . $R$ is Metric.diam X, which equals the supremum of $\|x-y\|$ over $\mathcal X$ because $\mathcal X$ is compact. Sequences are indexed by ℕ with the first iterate at index 1.

Committed conventions: $\mathcal X$ compact, convex and containing $x^*$ (hence nonempty); convexity of $f$ and the Lipschitz bound on the gradient are assumed on $\mathcal X$ only, which is weaker than the book's global assumptions; $\beta\ge0$ ; the existence of the minimizer $x^*$ is the book's standing assumption (p. 242); the conclusion is stated for $t\ge2$ , as in the book. Runs are predicates: $y_t$ is any minimizer of the linear form over $\mathcal X$ and $y_t\in\mathcal X$ is required, so the goal quantifies over every run with $\gamma_s=2/(s+1)$ . A formalization in which $y_t$ need not lie in $\mathcal X$ , or in which smoothness is assumed only along the iterates, states a different theorem and is excluded.

A complete development needs the descent inequality (3.4) for Fréchet derivatives in a normed space (reusable for every smooth method in the series and beyond), the fact that the iterates stay in $\mathcal X$ , and a scalar induction. Proofs of the milestones are welcome independently; milestone 4 is a statement about real sequences only.

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
M. Frank and P. Wolfe, An algorithm for quadratic programming, Naval Research Logistics Quarterly 3(1–2):95–110, 1956. https://doi.org/10.1002/nav.3800030109
J. C. Dunn and S. Harshbarger, Conditional gradient algorithms with open loop step size rules, Journal of Mathematical Analysis and Applications 62(2):432–444, 1978. https://doi.org/10.1016/0022-247X(78)90137-3
M. Jaggi, Revisiting Frank–Wolfe: projection-free sparse convex optimization, Proceedings of ICML 2013, PMLR 28(1):427–435. https://proceedings.mlr.press/v28/jaggi13.html
G. Lan, First-order and Stochastic Optimization Methods for Machine Learning, Springer, 2020, Theorem 7.1. https://doi.org/10.1007/978-3-030-39568-1

6 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·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 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research+1·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 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity IV: Gradient Descent on a Convex β-Smooth Function Has Rate 2β‖x₁ − x*‖²/(t − 1)Textbook

Motivation

Gradient descent goes back to Cauchy (1847). It is the simplest method for minimizing a differentiable function, and most of the first-order methods in large-scale optimization and machine learning are variants of it. Its appeal in high dimension is that its oracle complexity, the number of gradient evaluations needed to reach a given accuracy, can be bounded independently of the dimension. For a merely Lipschitz convex function the projected subgradient method needs on the order of $1/\varepsilon^2$ steps to reach accuracy $\varepsilon$ (Theorem 3.2 of the book). Under a smoothness assumption gradient descent does much better, because the gradients shrink near the optimum and the steps adapt automatically.

This mission formalizes the basic result of that kind: Theorem 3.3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). It states that gradient descent with step size $1/\beta$ on a convex $\beta$ -smooth function on $\mathbb R^n$ has optimality gap $O(1/t)$ after $t$ steps. The result and its proof are standard; versions appear in Nesterov's Introductory Lectures on Convex Optimization (2004, §2.1.5). It is the fourth mission in a series that formalizes the capstone results of Bubeck's monograph.

Setting

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

$f$ is convex if $f((1-\lambda)x+\lambda y)\le(1-\lambda)f(x)+\lambda f(y)$ for all $x,y$ and $\lambda\in[0,1]$ .
For $\beta\ge0$ , $f$ is $\beta$ -smooth if its gradient is $\beta$ -Lipschitz:

\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|\qquad\text{for all }x,y\in\mathbb R^n.

A minimizer is a point $x^*$ with $f(x^*)\le f(y)$ for every $y$ . Throughout the book a minimizer is assumed to exist.
Gradient descent with step size $\eta>0$ , started at $x_1\in\mathbb R^n$ , is the sequence

x_{t+1}=x_t-\eta\nabla f(x_t),\qquad t\ge1. \tag{3.1}

The optimality gaps are $\delta_s=f(x_s)-f(x^*)\ge0$ .

Formalization targets

Goal: Theorem 3.3 (p. 267)

If $f$ is convex and $\beta$ -smooth with $\beta>0$ , $x^*$ is a minimizer, and $(x_t)$ is gradient descent with $\eta=1/\beta$ , then for every $t\ge2$

f(x_t)-f(x^*)\le\frac{2\beta\|x_1-x^*\|^2}{t-1}.

Milestones

These are the statements the book's proof uses, in the book's order:

Lemma 3.4 (p. 267). For any $\beta$ -smooth $f$ , with no convexity: $|f(x)-f(y)-\nabla f(y)^\top(x-y)|\le\frac\beta2\|x-y\|^2$ .
(3.4) (p. 267). For convex $\beta$ -smooth $f$ : $0\le f(x)-f(y)-\nabla f(y)^\top(x-y)\le\frac\beta2\|x-y\|^2$ .
(3.5) (p. 267). For convex $f$ , one step of length $1/\beta$ decreases $f$ by at least $\frac1{2\beta}\|\nabla f(x)\|^2$ .
Lemma 3.5 (p. 268). If (3.4) holds, then $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac1{2\beta}\|\nabla f(x)-\nabla f(y)\|^2$ .
(3.6) (p. 269). Co-coercivity: $(\nabla f(x)-\nabla f(y))^\top(x-y)\ge\frac1\beta\|\nabla f(x)-\nabla f(y)\|^2$ .
Distances decrease (proof of Theorem 3.3, p. 269). $\|x_{s+1}-x^*\|\le\|x_s-x^*\|$ for every $s\ge1$ .
The recursion (p. 268). $\delta_{s+1}\le\delta_s-\frac{1}{2\beta\|x_1-x^*\|^2}\delta_s^2$ .
From the recursion to the rate (p. 269). For $\omega>0$ and non-negative reals, $\omega\delta_s^2+\delta_{s+1}\le\delta_s$ for all $s\ge 1$ implies $1/\delta_t\ge\omega(t-1)$ .

Stronger companion: footnote 4 (p. 269)

Under the same hypotheses, $f(x_t)-f(x^*)\le 2\beta\|x_1-x^*\|^2/(t+3)$ for every $t\ge1$ .

Significance

Theorem 3.3 is the reference rate for first-order methods on smooth convex problems. Several later results in the book are measured against it. Nesterov's accelerated gradient descent (§3.7) improves $1/t$ to $1/t^2$ , the lower bounds of §3.5 show that $1/t^2$ cannot be beaten by any black-box first-order method, and adding strong convexity (§3.4) upgrades $1/t$ to a linear rate. Its ingredients are reused throughout the book and the optimization literature: the descent lemma (Lemma 3.4), the one-step improvement (3.5) and co-coercivity (3.6). Co-coercivity is the finite-dimensional case of the Baillon–Haddad theorem.

The result is classical and fully proved on paper. To our knowledge Mathlib does not contain this rate for gradient descent on convex smooth functions, and no published Prove2Me theorem states it. The mission provides it, together with Lemma 3.4 and co-coercivity as reusable statements on EuclideanSpace ℝ (Fin n). These are the facts that later missions of the series on projected gradient descent, strong convexity and acceleration need. Formalizing the improved constant of footnote 4 is a welcome addition.

Difficulty

Two steps are not routine. The first is Lemma 3.4, where the book integrates the gradient along a segment. In Lean this needs a mean-value or fundamental-theorem-of-calculus argument for a function on a Euclidean space, together with a Cauchy–Schwarz estimate, and Mathlib's HasGradientAt interface has to be connected to one-variable derivatives along lines.

The second is the monotonicity of $\|x_s-x^*\|$ . The natural first attempt is to telescope the one-step improvement (3.5) together with the convexity bound $\delta_s\le\|x_s-x^*\|\|\nabla f(x_s)\|$ . That gives a recursion involving $\|x_s-x^*\|$ , which is not controlled by $\|x_1-x^*\|$ without further work. Making the recursion uniform requires co-coercivity (3.6), which comes from Lemma 3.5. That lemma's hypothesis is the two-sided inequality (3.4), not smoothness directly. The final numerical step divides by the gaps $\delta_s$ , so zero gaps need separate handling.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), and $x^\top y$ is ⟪x, y⟫_ℝ.
The gradient is an explicit map $g:\mathbb R^n\to\mathbb R^n$ with the hypothesis ∀ x, HasGradientAt f (g x) x.
$\beta$ -smoothness (IsBetaSmooth f g β) is the book's definition: $\beta\ge0$ , the gradient-existence hypothesis, and the Lipschitz bound $\|g(x)-g(y)\|\le\beta\|x-y\|$ . The book's "continuously differentiable" follows from it.
Convexity is Mathlib's ConvexOn ℝ Set.univ f. A minimizer is a point xstar with ∀ y, f xstar ≤ f y; its existence is the book's standing assumption, and $\nabla f(x^*)=0$ is derived, not assumed.
A gradient-descent run (IsGDRun g η x) is a sequence x : ℕ → ℝⁿ with $\eta>0$ and $x_{t+1}=x_t-\eta g(x_t)$ for every $t\ge1$ . The book's $x_1$ is x 1, and index $0$ is unused. Every theorem quantifies over all runs with $\eta=1/\beta$ .

Disclosed side conditions:

$\beta>0$ wherever the page divides by $\beta$ . Convexity is retained for (3.5), as in its source context.
$t\ge2$ in the goal, where the page's bound has denominator $t-1$ .
Statements in which the page divides by $\delta_s$ or by $\|x_1-x^*\|^2$ are multiplied through, so that they stay true and meaningful when those quantities vanish.

A trivializing formalization is ruled out. Smoothness is the Lipschitz condition on the gradient, so Lemma 3.4 and (3.4) are not restatements of the definition, as they would be if the quadratic upper bound (3.4) were taken as the definition of smoothness. The run predicate also fixes the step size $1/\beta$ .

A complete development needs:

the segment integral or mean-value estimate for HasGradientAt functions;
first-order characterizations of convexity for differentiable functions;
elementary inner-product algebra.

Lemma 3.4, Lemma 3.5 and (3.6) are reusable well beyond this mission. Proofs of any milestone are welcome independently.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–357, 2015. arXiv:1405.4980v2; §3.2, pp. 266–269.
A. Cauchy, Méthode générale pour la résolution des systèmes d'équations simultanées, C. R. Acad. Sci. Paris 25:536–538, 1847.
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9
J.-B. Baillon and G. Haddad, Quelques propriétés des opérateurs angle-bornés et n-cycliquement monotones, Israel J. Math. 26:137–150, 1977. doi:10.1007/BF03007664

10 thms2 active usersReviewed

Completed

Mathematical Physics Quantum Information·Captain: Lucas

Peres-Terno: the no-communication theorem for commuting Kraus operatorsResearch Paper

Motivation

Two observers, Alice and Bob, share a quantum system. Alice performs some intervention (a measurement, possibly followed by discarding part of her apparatus) and Bob, somewhere else, performs his own. If the statistics of Bob's outcomes could depend on what Alice chose to do, Alice could send Bob a message through the shared system alone, and if the two interventions are spacelike separated this would be a signal faster than light. Quantum mechanics and special relativity coexist peacefully only because this does not happen: the no-communication theorem guarantees that Bob's marginal statistics are independent of Alice's intervention whenever the two interventions are "local" to different parts of the system.

The review article of Peres and Terno, Quantum information and relativity theory (Rev. Mod. Phys. 76, 2004), develops the operational toolkit of quantum information (Kraus matrices, positive-operator-valued measures, completely positive maps) in Sec. II.D and then derives, in Sec. II.E, a sufficient algebraic condition for the absence of instantaneous information transfer: all of Alice's Kraus matrices commute with all of Bob's (their Eq. (9)). This mission formalizes that derivation together with the facts about Kraus matrices and complete positivity that the same pages state.

Setting

A quantum state on a finite-dimensional Hilbert space $\mathbb C^d$ is a density matrix $\rho$ : a positive semidefinite $d\times d$ complex matrix with $\operatorname{tr}\rho = 1$ .

An intervention with outcomes $\mu$ is described by Kraus matrices $A_{\mu m}$ , where the label $m$ ranges over a finite set indexing the subsystems discarded at the end of the interaction. When outcome $\mu$ occurs, the state is updated (Eq. (6)) to the unnormalized matrix

\rho'_\mu = \sum_m A_{\mu m}\,\rho\,A_{\mu m}^\dagger ,

and the probability of outcome $\mu$ is $p_\mu = \operatorname{tr}\rho'_\mu$ . The matrices

E_\mu = \sum_m A_{\mu m}^\dagger A_{\mu m}

(Eq. (8)) are the POVM elements; the intervention is complete when $\sum_\mu E_\mu = \mathbb 1$ .

A map $T$ on matrices is positive if it sends positive semidefinite matrices to positive semidefinite matrices, and completely positive if $T\otimes\mathbb 1$ , acting blockwise on matrices over $\mathbb C^d\otimes\mathbb C^n$ , is positive for every ancilla dimension $n$ .

For the no-communication theorem, Alice's Kraus matrices $A_{\mu m}$ and Bob's Kraus matrices $B_{\nu n}$ act on the same finite-dimensional space. The probability that Bob obtains $\nu$ , irrespective of Alice's outcome, is (Eq. (10))

p_\nu = \sum_\mu \operatorname{tr}\Big(\sum_{m,n} B_{\nu n} A_{\mu m}\,\rho\,A_{\mu m}^\dagger B_{\nu n}^\dagger\Big).

Formalization targets

Goal: no-communication (Sec. II.E, Eqs. (9)-(11))

If $[A_{\mu m}, B_{\nu n}] = 0$ for all $\mu, m, \nu, n$ , Alice's POVM is complete, and $\rho$ is a density matrix, then for every outcome $\nu$ of Bob

\sum_\mu \operatorname{tr}\Big(\sum_{m,n} B_{\nu n} A_{\mu m}\,\rho\,A_{\mu m}^\dagger B_{\nu n}^\dagger\Big) = \operatorname{tr}\Big(\sum_n B_{\nu n}\,\rho\,B_{\nu n}^\dagger\Big),

so all of Alice's operators disappear from Bob's statistics.

Milestones (Sec. II.D-II.E)

Eq. (7): $\sum_m \operatorname{tr}(A_{\mu m}\rho A_{\mu m}^\dagger) = \operatorname{tr}(\rho E_\mu)$ .
Eq. (8): every $E_\mu$ is positive semidefinite.
Eqs. (7)-(8): for a density matrix and a complete POVM, the $p_\mu$ are nonnegative reals summing to $1$ .
Eq. (6) defines a completely positive map.
Eq. (6) is the most general completely positive linear map: every completely positive linear map between matrix algebras has a finite Kraus representation.
Time reversal (transposition, i.e. complex conjugation of a Hermitian $\rho$ ) is a positive map,
but it is not completely positive.
The exchange step of Sec. II.E: under the commutation hypothesis, $\operatorname{tr}\sum_{m,n} B_{\nu n}A_{\mu m}\rho A_{\mu m}^\dagger B_{\nu n}^\dagger = \operatorname{tr}\big(E_\mu \sum_n B_{\nu n}\rho B_{\nu n}^\dagger\big)$ .

Significance

The no-communication theorem is the consistency check between quantum measurement theory and relativistic causality, and it is the starting point of the relativistic measurement theory developed in Sec. III of the review. The commutation condition (9) is exactly what local quantum field theory provides for spacelike separated regions, so this algebraic form is the one later used for microcausality arguments. The Kraus representation (milestones 4-5) is a basic structural theorem of quantum information theory, and the failure of complete positivity for transposition (milestones 6-7) underlies the partial-transpose entanglement criterion.

The results are classical and their proofs are known; the mission produces machine-checked versions on top of Mathlib's matrix library. The finite Kraus representation theorem (milestone 5) requires Choi-matrix machinery that is not, to the knowledge of this proposal, available in Mathlib in this form; it is reusable well beyond this mission.

Difficulty

The goal and milestones 1-3 and 8 are finite-dimensional trace manipulations; the care needed is in keeping the order of products right, using the adjoint of the commutation relation, and summing over indices in the correct order. Milestone 7 needs an explicit entangled witness on $\mathbb C^2\otimes\mathbb C^n$ . Milestone 5 is the substantial one: the obvious approach of writing $T(\rho)$ in a basis does not produce Kraus operators directly; a positivity argument (via the Choi matrix of $T$ and its spectral decomposition) is needed.

Formalization scope

All Hilbert spaces are finite dimensional: matrices are indexed by arbitrary finite types with complex entries. Outcome sets and discarded-subsystem label sets are finite types; Alice's and Bob's label sets may depend on the outcome. Kraus matrices for the single-intervention milestones may be rectangular ( $e\times d$ ), reflecting that the system after the intervention may differ from the original one; in the no-communication theorem both observers' matrices are square on a common space. The order on $\mathbb C$ used for "nonnegative probability" is the standard partial order ( $z\ge 0$ iff $z$ is real and nonnegative). Complete positivity quantifies over ancillas $\mathbb C^n$ for every $n\in\mathbb N$ , with $T\otimes\mathbb 1$ acting blockwise. Time reversal is encoded by the linear map $\rho\mapsto\rho^{T}$ ; on Hermitian matrices this coincides with complex conjugation, and only the linear extension gives a meaningful complete-positivity statement.

The goal keeps the hypotheses of the source setting (both POVMs complete, $\rho$ a density matrix); none of them can be dropped silently by a degenerate encoding, and the conclusion is an identity of complex numbers, so no hypothesis is vacuous: for instance, single-outcome trivial interventions with $A = B = \mathbb 1$ satisfy all of them.

Note: the sentence on p. 100 of the source claiming that commuting POVM elements are necessarily orthogonal projections is not included; as stated it fails (e.g. $E_1 = E_2 = \tfrac12\mathbb 1$ ).

Selected references

A. Peres and D. R. Terno, Quantum information and relativity theory, Rev. Mod. Phys. 76, 93-123 (2004). https://doi.org/10.1103/RevModPhys.76.93
K. Kraus, States, Effects, and Operations, Lecture Notes in Physics 190, Springer (1983). https://doi.org/10.1007/3-540-12732-1
M.-D. Choi, Completely positive linear maps on complex matrices, Linear Algebra Appl. 10, 285-290 (1975). https://doi.org/10.1016/0024-3795(75)90075-0

10 thms2 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

Rademacher and Gaussian Complexities: Risk Bounds and Structural Results 6: The Expected Maximum Discrepancy Lies Between R_n(F)/2 − 2√(2/n) and R_n(F) + 4√(2/n)Research Paper

Motivation

Data-dependent risk bounds in statistical learning theory control the gap between the expected loss of a learned function and its empirical loss by a complexity penalty that is computed from the training data. The first such penalties were the maximum discrepancy of a function class (Bartlett, Boucheron and Lugosi, Model selection and error estimation, Machine Learning 48, 2002) and its Rademacher complexity (Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Trans. Inf. Theory 47, 2001; Koltchinskii and Panchenko 2000). The maximum discrepancy compares the behaviour of the class on two fixed halves of the sample; the Rademacher complexity compares it on two random halves. Bartlett and Mendelson (JMLR 3, 2002), Lemma 3, show that these two quantities are equivalent up to a factor 2 and an additive $O(1/\sqrt n)$ . This mission formalizes that lemma from the published JMLR article (pp. 463–482); the proof is its Appendix A.

Setting

Let $\mu$ be a probability measure on a measurable space $\mathcal X$ and let $X_1,\dots,X_n$ be independent samples from $\mu$ . Let $F$ be a class of measurable functions $f:\mathcal X\to[-1,1]$ . Let $\sigma_1,\dots,\sigma_n$ be independent uniform $\{\pm1\}$ -valued random variables, independent of the sample.

The Rademacher complexity of $F$ is

R_n(F) = \mathbf E\sup_{f\in F}\left|\frac2n\sum_{i=1}^n\sigma_i f(X_i)\right|.

For even $n$ , the maximum discrepancy of $F$ is the random variable

\hat D_n(F) = \sup_{f\in F}\left(\frac2n\sum_{i=1}^{n/2}f(X_i) - \frac2n\sum_{i=n/2+1}^n f(X_i)\right),

with no absolute value, and the expected maximum discrepancy is $D_n(F)=\mathbf E\hat D_n(F)$ . The class is closed under negation if $f\in F$ implies $-f\in F$ , and $-F=\{-f:f\in F\}$ .

The proof works with the conditional supremum function

s(N) = \frac2n\,\mathbf E\left[\sup_{f\in F}\sum_{i=1}^n\sigma_i f(X_i)\;\middle|\;\sum_{i=1}^n\sigma_i=N\right],

defined for the values $N$ that $\sum_i\sigma_i$ can take.

Formalization targets

Goal: Lemma 3, first and second displays

For every even $n\ge2$ ,

\frac{R_n(F)}{2} - 2\sqrt{\frac2n} \le D_n(F) \le R_n(F) + 4\sqrt{\frac2n},

and if $F$ is closed under negation,

R_n(F) - 4\sqrt{\frac2n} \le D_n(F).

Milestones (Appendix A, pp. 479–480)

$R_n(F)\ge\mathbf E\,s(\sum_i\sigma_i)$ , with equality when $F$ is closed under negation.
$D_n(F) = s(0)$ .
$|s(N_1)-s(N_2)|\le 4|N_2-N_1|/n$ .
$|\mathbf E s(N)-s(\mathbf EN)|\le\mathbf E|s(N)-s(\mathbf EN)|\le4\sqrt{2/n}$ for $N=\sum_i\sigma_i$ .
$R_n(F)=R_n(F\cup-F)\le D_n(F\cup-F)+4\sqrt{2/n}$ .
$D_n(F\cup-F)\le 2D_n(F)+D_n(\{f_0,-f_0\})$ for any $f_0\in F$ (a corrected form of the printed step, see below).

Significance

Lemma 3 makes the maximum discrepancy and the Rademacher complexity interchangeable in risk bounds: a bound in terms of one gives a bound in terms of the other with an explicit additive loss. The maximum discrepancy can be computed by a single empirical risk minimization on a relabelled sample, while the Rademacher complexity has the structural properties (monotonicity, convex-hull invariance, contraction) that make it easy to bound for concrete classes; the lemma transfers the second kind of estimate to the first quantity.

The lemma is proved in the paper; no machine-checked proof of it, or of the comparison between fixed and random half-sample splits, is known to exist. Formalizing it requires the exchangeability argument for i.i.d. samples, the conditioning of a uniform sign vector on its sum, and a moment bound for the Rademacher sum $\sum_i\sigma_i$ , all with explicit constants.

Difficulty

The heart of the proof is that, conditioned on the number of positive signs, a uniform sign vector splits the i.i.d. sample into two random subsets of fixed sizes, and every split of the same sizes has the same law as the fixed split. Making this precise requires a permutation-invariance argument for product measures applied to a supremum over an arbitrary class, where measurability is not automatic. The step from classes closed under negation to general classes is where the printed argument is loose: since $\hat D_n$ has no absolute value, $\hat D_n(F\cup-F)$ is a maximum of two suprema that may be negative, and the naive bound $D_n(F\cup-F)\le2D_n(F)$ fails.

Formalization scope

The Lean development lives in the namespace RadGauss.Discrepancy. Sign vectors are Fin n → Bool (true ↦ 1, false ↦ -1) and expectations over signs are finite averages over all $2^n$ sign vectors; $s(N)$ is the average over the sign vectors with sum $N$ . $R_n$ takes values in $[0,\infty]$ (a lower Lebesgue integral of an $[0,\infty]$ -valued supremum), while $\hat D_n$ , $D_n$ and $s$ are real, because the maximum discrepancy is signed. Inequalities of the form $a-c\le D$ are written $a\le D+c$ with real terms embedded by ENNReal.ofReal; this is equivalent to the printed form since $D_n(F)\ge0$ for nonempty $F$ .

Hypotheses added to the page, all disclosed in each item:

the sample size is even, $n=2m$ with $m\ge1$ , since $\hat D_n$ needs half sums;
$F$ is nonempty (the supremum over the empty class is $-\infty$ in the paper and $0$ in Lean);
every $f\in F$ is measurable, and for every sign vector $\sigma$ the map $x\mapsto\sup_{f\in F}\sum_i\sigma_if(x_i)$ is measurable. This is the measurability guard: without it the Bochner integrals defining $D_n$ and $s$ would silently be $0$ .

Corrections of printed statements:

The Lipschitz bound on $s$ is printed for $0\le n_2<n_1\le n$ but used for negative values of $\sum_i\sigma_i$ ; it is stated for every pair of attainable values.
The printed step $D_n(F\cup-F)\le2D_n(F)$ is false for the signed $\hat D_n$ of p. 464 ( $F=\{f\}$ , $f(X)$ uniform on $\{\pm1\}$ , $n=2$ gives $1\le0$ ); the milestone states it with the additional term $D_n(\{f_0,-f_0\})\le2/\sqrt n$ . The goal itself remains true.
The third display of Lemma 3, $P\{|\hat D_n(F)-D_n(F)|\ge\epsilon\}\le2\exp(-\epsilon^2n/2)$ , is false as printed ( $F=\{f\}$ as above, $n=2$ , $\epsilon=2$ : the probability is $1/2>2e^{-4}$ ) and is not part of the mission.

A formalization in which $D_n$ or $s$ is a junk value (non-integrable or non-measurable suprema, an empty class, an odd sample size with truncated $n/2$ ) would make the goal trivial or meaningless; the hypotheses above rule that out, and the class $F=\{0\}$ satisfies all of them.

Welcome contributions include general lemmas on the invariance of $\mathbf E\sup_{f\in F}\Phi_f(X_{\pi(1)},\dots,X_{\pi(n)})$ under permutations $\pi$ of an i.i.d. sample, conditioning of uniform sign vectors on their sum, and the bound $\mathbf E|\sum_i\sigma_i|\le\sqrt n$ . These are reusable well beyond this mission.

Selected references

P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002) 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
P. L. Bartlett, S. Boucheron, G. Lugosi, Model selection and error estimation, Machine Learning 48 (2002) 85–113. https://doi.org/10.1023/A:1013999503812
V. Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Transactions on Information Theory 47 (2001) 1902–1914. https://doi.org/10.1109/18.930926
L. Devroye, L. Györfi, G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. https://doi.org/10.1007/978-1-4612-0711-5

10 thms2 active usersReviewed

Completed

Dynamic Programming Graph Theory Operations Research+1·Captain: mikedeng1

On a Routing Problem: Successive Approximations from the Direct-Route Policy Decrease to the Unique Solution of the Routing Equation Within N − 1 IterationsResearch Paper

Motivation

Finding the quickest route between two points of a road network is among the oldest problems of operations research. It is the subproblem inside vehicle routing, network flow and many dynamic programs. Richard Bellman's four-page note On a routing problem (Quarterly of Applied Mathematics, 1958) treats it as a dynamic program. The minimal travel times satisfy a nonlinear system of equations, and that system can be solved by successive approximations that terminate after a number of steps bounded in advance. The iteration is now known as the Bellman–Ford method. A footnote added in proof records that Max Woodbury and George Dantzig had obtained the same scheme independently, and Ford's RAND report of 1956 describes a closely related labelling procedure.

Timeline.

1956. L. R. Ford Jr., Network flow theory (RAND P-923): a label-improving procedure for shortest paths.
1957. Bellman's Dynamic Programming (Princeton) states the principle of optimality used here.
1958. Bellman's note: the routing equation, its uniqueness, approximation in policy space with an (N − 1)-step bound, and a second, monotone increasing scheme.
1959. Dijkstra gives a label-setting method for nonnegative lengths.
1962. Floyd's Algorithm 97 computes all pairs of shortest distances.

Setting

There are $N$ cities, numbered $1, \dots, N$ . Every two of them are linked by a direct road, and city $N$ is the destination. The travel time from $i$ to $j$ is a real number $t_{ij}$ ; the matrix $T = (t_{ij})$ need not be symmetric. Throughout, $t_{ij} > 0$ for $i \ne j$ .

A route from $i$ to $N$ is a sequence of cities $i = c_0, c_1, \dots, c_m = N$ in which consecutive cities differ. Its stops are $c_1, \dots, c_{m-1}$ , and its time is $\sum_{r<m} t_{c_r c_{r+1}}$ . The minimal time $f_i$ (3.1) is the least time of a route from $i$ to $N$ , and $f_N = 0$ .

The routing equation (3.2) is the system

F_i = \min_{j \ne i}\,[t_{ij} + F_j]\quad (i = 1, \dots, N-1), \qquad F_N = 0 .

Approximation in policy space (§5) starts from the direct-route policy (5.2), $f_i^{(0)} = t_{iN}$ , and iterates (5.1):

f_i^{(k+1)} = \min_{j \ne i}\,[t_{ij} + f_j^{(k)}]\quad (i \ne N), \qquad f_N^{(k+1)} = 0 .

The second scheme (§7, (7.1)) starts instead from $\underline f_i^{(0)} = \min_{j\ne i} t_{ij}$ and uses the same step.

Formalization targets

Goal: convergence within $N - 1$ iterations

For every $k \ge N - 1$ the following hold. Each $f_i^{(k)}$ is the minimal time from $i$ to $N$ , attained by a route. The vector $f^{(k)}$ solves (3.2). Every real solution of (3.2) equals $f^{(k)}$ :

k \ge N-1 \;\Longrightarrow\; f^{(k)} = f = \text{the unique solution of (3.2)}.

This is the claim of the Summary ("converges after at most $(N-1)$ iterations") and of the last sentence of §5. The paper's bound $N - 1$ is kept, although $N - 2$ also suffices.

Milestones

(3.2): the minimal times exist and satisfy the routing equation.
§4: (3.2) has at most one solution.
(5.4): $f^{(1)} \le f^{(0)}$ .
§5, the sentence after (5.4): $f_i^{(k)}$ is the minimal time over routes with at most $k$ stops.
(5.5): $f^{(k+1)} \le f^{(k)}$ for all $k$ .
§7: the scheme (7.1) increases, stays below the solution of (3.2) (7.2), and equals it from some index on.

Significance

The result. The note turns an enumeration over exponentially many paths into $N - 1$ rounds of $N$ minimisations each, with a bound fixed before the computation starts. The uniqueness theorem makes the routing equation a characterisation of the minimal times, not merely a property of them. This is the template for later correctness proofs of shortest-path and value-iteration algorithms. The monotone decrease (5.5) is the first instance of policy improvement: every iterate is the value of an actual routing policy.

Formalizing it. The results are classical and proved. What this mission adds is a machine-checked development against the paper's own objects. Routes, their times and minimal times are defined from scratch. The iteration is stated exactly as printed, apart from the corrected initial value at the destination. The (N − 1)-step termination is asserted as an equality, not a limit. Related platform items treat other methods and do not cover these statements. One is the label-correcting method (BertsekasDP.label_correcting_correctness_of_nonneg_arcs, BertsekasDP.label_correcting_terminates). Another is the stochastic shortest path problem under a termination assumption that fails for deterministic routing (BertsekasDP.ssp_main_theorem). There are also the generic candidate-list algorithm (BertsekasNetwork.generic_shortest_path_algorithm), Floyd's Algorithm 97 and Dijkstra's method.

Difficulty

The minimum in (3.2) may be attained at a $j$ whose own optimal route passes back through $i$ . The routing equation is a fixed-point equation for an operator that is monotone but not a contraction in any fixed norm. The standard contraction argument for discounted dynamic programs therefore does not apply. Uniqueness has to use $t_{ij} > 0$ to exclude zero-time cycles: with $t_{12} = t_{21} = 0$ , the system (3.2) has infinitely many solutions. The $N - 1$ bound depends on the at-most- $k$ -stops reading of $f^{(k)}$ and on the fact that an optimal route never needs to revisit a city. Neither is visible from the recursion alone. For the scheme of §7, the page gives no bound on the number of iterations, and none holds uniformly in $t$ .

Formalization scope

Cities are Fin (n + 1), so $N = n + 1$ , with standing hypothesis $n \ge 1$ . City $N$ is Fin.last n, and travel times are t : Fin (n + 1) → Fin (n + 1) → ℝ with $t_{ij} > 0$ for $i \ne j$ . Diagonal entries are unconstrained and never used. No symmetry, triangle inequality or integrality is assumed. A route is a list of cities with distinct consecutive entries ending at $N$ . Repeated cities are allowed; with positive times this changes no minimum. Minimal times are attained minima over routes (IsMinTime, IsMinTimeWithin), not real infima. The minimum in (3.2) is a Finset.inf' over all $j \ne i$ , the destination included.

The paper's loose phrases are made explicit as follows.

"Using an optimal policy" (3.1) becomes a minimum attained by a route and below every route.
"Represents the minimum time for a path with at most one stop" becomes, for every $k$ , a minimum over routes with at most $k + 1$ roads.
"Converges after at most $(N - 1)$ iterations" becomes $f^{(k)} = f$ for every $k \ge N - 1$ .
"Only a finite number of iterations will be required" (§7) becomes $\exists K, \forall k \ge K$ , $\underline f^{(k)} = f$ .
"The solution of (3.2)" in §7 becomes an arbitrary solution of (3.2), which milestones 1–2 show is the vector of minimal times.

Two printed slips are corrected. (5.2) is printed for $i = 1, \dots, N$ , which would set $f_N^{(0)} = t_{NN}$ , and with $t_{NN} > 0$ statements (5.4), (5.5) and the goal would be false. The formalization uses $f_N^{(0)} = 0$ , the value the paper's own justification needs. (7.1) prints " $N = 1$ " for $N - 1$ . Section 6 (computational aspects) and the closing expectation of §7 that the first method converges faster are not formalized.

The goal cannot be satisfied trivially. The minimal times are defined from routes, not as a solution of (3.2) or as a limit of the iteration, so the goal connects the recursion to the routing problem itself.

The development needs only finite minima, lists and induction; nothing beyond core Mathlib. The route and minimal-time layer is reusable for other deterministic shortest-path results. Proofs of any milestone are welcome, as are proofs of the sharper bound $N - 2$ .

Selected references

R. Bellman, On a routing problem, Quarterly of Applied Mathematics 16(1) (1958), 87–90. https://doi.org/10.1090/qam/102435
R. Bellman, Dynamic Programming, Princeton University Press, 1957.
R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
L. R. Ford Jr., Network flow theory, RAND Corporation P-923, 1956. https://www.rand.org/pubs/papers/P923.html
E. W. Dijkstra, A note on two problems in connexion with graphs, Numerische Mathematik 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
R. W. Floyd, Algorithm 97: Shortest path, Communications of the ACM 5(6) (1962), 345. https://doi.org/10.1145/367766.368168

8 thms2 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

Rademacher and Gaussian Complexities: Risk Bounds and Structural Results 5: Kernel Expansions with α′Kα ≤ B² Have Rademacher and Gaussian Complexity at Most 2B√(E k(X,X)/n)Research Paper

Motivation

Kernel methods, such as support vector machines, predict with functions of the form $x \mapsto \sum_i \alpha_i k(x, x_i)$ : finite expansions of a fixed similarity function $k$ centred at data points. Their statistical behaviour is governed by the size of the class of such expansions that the method searches. Bartlett and Mendelson, in Rademacher and Gaussian Complexities: Risk Bounds and Structural Results (JMLR 3, 2002), develop risk bounds in terms of the Rademacher and Gaussian complexities of a class, and in §4.3 (pp. 476–478) compute these complexities for the class of kernel expansions whose coefficient vector has quadratic form $\alpha' K \alpha \le B^2$ . The resulting bound depends on the kernel only through its diagonal $k(x,x)$ , which is what makes margin bounds for support vector machines dimension-free. This mission formalizes that computation. The source is the published JMLR article (pages cited by the journal's printed numbers).

Setting

Let $\mathcal X$ be a compact topological space. A kernel is a continuous function $k : \mathcal X \times \mathcal X \to \mathbb R$ such that for every $m$ and all $x_1, \dots, x_m \in \mathcal X$ the Gram matrix $K_{ij} = k(x_i, x_j)$ is symmetric and positive semidefinite. For $B \ge 0$ the class of kernel expansions is

F = \Big\{x \mapsto \sum_{i=1}^m \alpha_i k(x, x_i) : m \in \mathbb N,\ x_i \in \mathcal X,\ \alpha_i \in \mathbb R,\ \sum_{i,j}\alpha_i\alpha_j k(x_i, x_j) \le B^2\Big\},

with centres anywhere in $\mathcal X$ (Lean: kernelClass k B).

For a class $F$ of real functions on $\mathcal X$ and a sample $x_1, \dots, x_n$ , let $\sigma_1, \dots, \sigma_n$ be independent uniform signs and $g_1, \dots, g_n$ independent standard Gaussians. The empirical Rademacher complexity and empirical Gaussian complexity (Definition 2, p. 464) are

\hat R_n(F) = \mathbb E_\sigma \sup_{f\in F}\Big|\frac2n\sum_{i=1}^n \sigma_i f(x_i)\Big|, \qquad \hat G_n(F) = \mathbb E_g \sup_{f\in F}\Big|\frac2n\sum_{i=1}^n g_i f(x_i)\Big|.

For a probability measure $\mu$ on $\mathcal X$ and an i.i.d. sample $X_1, \dots, X_n \sim \mu$ , the Rademacher complexity is $R_n(F) = \mathbb E \hat R_n(F)$ and the Gaussian complexity is $G_n(F) = \mathbb E \hat G_n(F)$ (Lean: empiricalRademacher, empiricalGaussian, rademacherComplexity, gaussianComplexity).

A feature map of $k$ is a map $\Phi : \mathcal X \to \mathcal H$ into a real Hilbert space with $k(x_1, x_2) = \langle \Phi(x_1), \Phi(x_2) \rangle$ .

Formalization targets

Goal: the expected complexity bound (§4.3, p. 478, display after the proof of Lemma 22)

With $X \sim \mu$ ,

R_n(F) \le 2B\sqrt{\frac{\mathbb E\, k(X,X)}{n}}, \qquad G_n(F) \le 2B\sqrt{\frac{\mathbb E\, k(X,X)}{n}}.

Milestone 1: feature-map inclusion (p. 477)

For any feature map $\Phi$ of $k$ , $\|\sum_i \alpha_i \Phi(x_i)\|^2 = \sum_{i,j}\alpha_i\alpha_j k(x_i,x_j)$ , and hence $F \subseteq \{x \mapsto \langle w, \Phi(x)\rangle : \|w\| \le B\}$ .

Milestone 2: Lemma 22 (p. 477)

For every sample $X_1, \dots, X_n$ ,

\hat G_n(F) \le \frac{2B}{n}\sqrt{\sum_{i=1}^n k(X_i, X_i)}, \qquad \hat R_n(F) \le \frac{2B}{n}\sqrt{\sum_{i=1}^n k(X_i, X_i)}.

Significance

The goal shows that the kernel class has complexity of order $n^{-1/2}$ , with a constant given by $B$ and the quantity $\mathbb E\, k(X,X)$ , which is the trace of the integral operator $T_k f = \int k(\cdot, y) f(y)\, d\mu(y)$ on $L_2(\mu)$ . No dimension of the feature space enters. Fed into the paper's margin-cost risk bound (Theorem 21, p. 476), the sample-wise Lemma 22 gives a data-dependent misclassification bound for support vector machines in terms of the trace of the Gram matrix of the training sample. Bounds of this form are the standard complexity estimate for kernel classes in learning theory textbooks.

The result is proved in the paper; nothing in this mission is open mathematics. What the mission adds is a machine-checked version with the paper's normalization (factor $2/n$ , absolute value inside the supremum), covering both the Rademacher and the Gaussian complexity, for expansions with centres anywhere in $\mathcal X$ . Related statements on the platform (Mohri et al.'s Theorem 5.10 and Proposition 9.3) use the $1/n$ normalization without absolute value, assume a uniform bound $\sup_x k(x,x) \le r^2$ , and treat only the Rademacher case, so they do not imply the targets here.

Difficulty

The class $F$ is defined through the kernel, not through a feature map, and its expansions have arbitrarily many centres anywhere in $\mathcal X$ . The supremum over $F$ is therefore a supremum over an infinite-dimensional family, and must be controlled without assuming a separate numerical upper bound on $k(x,x)$ or that the feature space is finite dimensional. For the Gaussian complexity the supremum sits inside an expectation over a continuous random vector, and the passage from the sample-wise bound to the expected bound must move an expectation inside a square root in the right direction. A bound with $\sup_x k(x,x)$ in place of $\mathbb E\, k(X,X)$ is weaker and is not the target.

Formalization scope

Conventions committed to in Lean:

Complexities take values in $[0, \infty]$ (ℝ≥0∞); expectations over the Gaussian vector and over the sample are lower Lebesgue integrals against product measures, and the Rademacher expectation is the exact average over the $2^n$ sign vectors $\sigma : \mathrm{Fin}\,n \to \mathbb Z^\times$ . An unbounded class has complexity $+\infty$ , so a junk value of $0$ for a real supremum or a non-integrable expectation cannot make the bounds trivial.
A kernel (IsKernel k) carries compactness of $\mathcal X$ , joint continuity, and positive semidefiniteness (with symmetry) of every Gram matrix, as in the paper's definition. The goal puts the Borel $\sigma$ -algebra on $\mathcal X$ and assumes $\mu$ is a probability measure; $\mathbb E\, k(X,X)$ is the Bochner integral of the continuous function $x \mapsto k(x,x)$ .
$B \ge 0$ is assumed in every statement (the paper fixes $B > 0$ ). For $B < 0$ the right-hand sides are negative while the left-hand sides are not, and the inclusion of milestone 1 fails.
No $n \ge 1$ hypothesis: at $n = 0$ both sides of every bound are $0$ in Lean.
The feature map in milestone 1 is a hypothesis (any real Hilbert space and any $\Phi$ with $k = \langle \Phi(\cdot), \Phi(\cdot)\rangle$ ); its existence is the RKHS theorem, referenced as the supporting platform item FoundationsML.Kernels.RKHS_exists.
No measurability or integrability hypotheses on $\hat R_n(F)$ or $\hat G_n(F)$ are assumed, and none is needed.

A trivializing formalization is ruled out: the goal is stated for the kernel class $F$ itself, not for the larger ball of linear functionals of a feature map, and not for the subclass with centres at the sample points.

Infrastructure a complete development needs: Gaussian integration over $\mathbb R^n$ (second moments of a standard Gaussian vector), Jensen's inequality for the square root under a lower Lebesgue integral, and Cauchy–Schwarz for positive semidefinite bilinear forms (or the RKHS feature map). The Definition 2 complexities are shared with the paper's other missions and reusable. Contributions of any of these milestones, and of proofs of the goal that avoid the feature map, are welcome.

Selected references

P. L. Bartlett and S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
N. Cristianini and J. Shawe-Taylor, An Introduction to Support Vector Machines, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511801389
N. Aronszajn, Theory of Reproducing Kernels, Transactions of the American Mathematical Society 68 (1950), 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
M. Mohri, A. Rostamizadeh and A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018. https://mitpress.mit.edu/9780262039406/

8 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity I: The Center of Gravity Method Satisfies f(x_t) − min f ≤ 2B(1 − 1/e)^{t/n}Textbook

Motivation

Black-box convex optimization asks how many queries to an oracle are needed to minimize a convex function to accuracy $\varepsilon$ . In fixed dimension $n$ the answer is of order $n\log(1/\varepsilon)$ , and the first algorithm to attain it is the center of gravity method, discovered independently by Levin (1965) and Newman (1965). It is the opening example of cutting plane methods: algorithms that keep a set known to contain a minimizer and shrink it with one half-space per oracle call. The ellipsoid method and Vaidya's method, which underlie the polynomial-time solvability of linear programming and convex feasibility problems, follow the same template with cheaper sets. This mission is the first of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (2015), and covers its §2.1.

Timeline:

1960: B. Grünbaum proves that every half-space whose boundary passes through the centroid of a convex body in $\mathbb R^n$ contains at least a fraction $(n/(n+1))^n \ge 1/e$ of its volume.
1965: A. Levin and D. J. Newman independently introduce the center of gravity method and prove its linear rate.
1983: A. Nemirovski and D. Yudin show that $\Omega(n\log(1/\varepsilon))$ oracle calls are necessary for small $\varepsilon$ , so the method's oracle complexity is optimal.

Setting

Let $\mathcal X\subset\mathbb R^n$ be a convex body: a compact convex set with non-empty interior. Let $f:\mathcal X\to[-B,B]$ be continuous and convex, and let $x^*\in\mathcal X$ be a minimizer of $f$ on $\mathcal X$ . A vector $w$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le w^\top(x-y)$ for every $y\in\mathcal X$ . The first order oracle returns, at a query point, some subgradient there; the zeroth order oracle returns the value of $f$ .

For a set $\mathcal S$ of finite positive volume, its center of gravity is

c(\mathcal S)=\frac{1}{\mathrm{vol}(\mathcal S)}\int_{x\in\mathcal S}x\,dx .

The center of gravity method sets $\mathcal S_1=\mathcal X$ and, for $t\ge1$ , computes $c_t=c(\mathcal S_t)$ , queries the first order oracle at $c_t$ to obtain a subgradient $w_t$ , and sets

\mathcal S_{t+1}=\mathcal S_t\cap\{x\in\mathbb R^n:(x-c_t)^\top w_t\le0\}.

After $t$ steps it outputs $x_t\in\operatorname{argmin}_{1\le r\le t}f(c_r)$ , found with $t$ calls to the zeroth order oracle.

The Lean development names these objects IsConvexBody, IsSubgradientOn, centroid and IsCenterOfGravityRun in the namespace ConvexOptAlg.CenterGravity.

Formalization targets

Goal: Theorem 2.1 (p. 245)

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

f(x_t)-\min_{x\in\mathcal X}f(x)\le 2B\Big(1-\frac1e\Big)^{t/n}.

Milestones (proof of Theorem 2.1, pp. 246–247)

Lemma 2.2 (Grünbaum). If $\mathcal K$ is centered, $\int_{\mathcal K}x\,dx=0$ , then for every $w\ne0$ ,

\mathrm{Vol}\big(\mathcal K\cap\{x:x^\top w\ge0\}\big)\ge\tfrac1e\,\mathrm{Vol}(\mathcal K).

(2.2). $\mathcal S_t\setminus\mathcal S_{t+1}\subset\{x\in\mathcal X:(x-c_t)^\top w_t>0\}\subset\{x\in\mathcal X:f(x)>f(c_t)\}$ , hence $x^*\in\mathcal S_t$ for every $t$ .
Volume decay. If $w_s\ne0$ for $s\le t$ , then $\mathrm{vol}(\mathcal S_{t+1})\le(1-1/e)^t\,\mathrm{vol}(\mathcal X)$ .
Shrunk copies. For $\varepsilon\in[0,1]$ and $\mathcal X_\varepsilon=\{(1-\varepsilon)x^*+\varepsilon x: x\in\mathcal X\}$ , $\mathrm{vol}(\mathcal X_\varepsilon)=\varepsilon^n\,\mathrm{vol}(\mathcal X)$ .
Values on shrunk copies. Every $x_\varepsilon\in\mathcal X_\varepsilon$ satisfies $f(x_\varepsilon)\le f(x^*)+2\varepsilon B$ .

Significance

Theorem 2.1 is a linear rate whose number of queries to reach accuracy $\varepsilon$ , $O(n\log(2B/\varepsilon))$ , depends on the dimension only linearly and on the accuracy only logarithmically, and matches the Nemirovski–Yudin lower bound. It is the reference point against which the ellipsoid method ( $O(n^2\log(1/\varepsilon))$ queries) and Vaidya's method are measured, and the randomized center of gravity method of §6.7 of the book rests on the same analysis. Grünbaum's inequality is a basic fact of convex geometry with uses well beyond optimization, for instance in the analysis of query complexity and of approximate centroid computations by random walks.

On the formal side, the theorem has been proved since 1965 and the lemma since 1960; neither is known to have a machine-checked proof. A complete development adds to Mathlib-based libraries the center of gravity of a set, the volume of homothetic images in the form used here, Grünbaum's inequality, and a reusable predicate for cutting plane runs. The later missions of this series (the ellipsoid method in particular) reuse the shrunk-copy argument of milestones 4 and 5.

Difficulty

The steps (2.2), the shrunk-copy volume and the value bound are short. The volume decay and the final comparison are bookkeeping once one knows that each cut keeps the method's sets convex bodies with positive volume. The difficulty is Lemma 2.2. A half-space through the centroid need not split the volume evenly: for a cone the smaller side tends to $1/e$ of the volume as $n\to\infty$ , so no symmetry argument works, and the bound must hold uniformly in the dimension. The classical proofs rely on tools of convex geometry, such as volume comparisons between a body and a symmetrized body, that are not available in Lean in the needed form. A second source of work is that the method's sets are defined through centroids: it has to be shown that they remain convex bodies of positive volume, so that each centroid is the genuine center of gravity, and this fact is not available before the volume estimates are.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; volumes are kept in $[0,\infty]$ in every statement. The function is a total map f : EuclideanSpace ℝ (Fin n) → ℝ with $|f|\le B$ , continuity and convexity required on $\mathcal X$ only; its values off $\mathcal X$ are irrelevant. Subgradients are relative to $\mathcal X$ (Definition 1.2). A run is a predicate on sequences indexed from $1$ ; the oracle's choice of subgradient is free, and every theorem holds for all runs. The minimizer $x^*$ is a hypothesis, as in the book's standing notation; it exists here by compactness. The output $x_t$ is any argmin, so the goal bounds the minimum $\min_{1\le r\le t}f(c_r)$ .

Added hypotheses, all disclosed in the statements: $n\ge1$ in the goal, because the exponent $t/n$ is undefined for $n=0$ ; and in Lemma 2.2, that the centered set is a convex body, because in Lean the integral of a non-integrable function is $0$ , which would make every unbounded convex set "centered". The milestone on volume decay assumes $w_s\ne0$ , which is the book's own reduction.

The center of gravity is defined with the real volume $\mathrm{vol}(\mathcal S)$ and is meaningless when that volume is $0$ or infinite. The run predicate does not assume the volumes are positive; that every set of a run is a convex body of positive volume is part of what has to be proved, and a formalization in which runs could degenerate to sets of zero volume, or in which the centroid is an arbitrary point, is not the book's method.

Contributions welcome: proofs of any item; a general Grünbaum inequality for convex sets of finite positive volume; lemmas on centroids (membership in the closed convex hull, translation behaviour) that later missions can reuse.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §2.1. https://arxiv.org/abs/1405.4980
B. Grünbaum, Partitions of mass-distributions and of convex bodies by hyperplanes, Pacific Journal of Mathematics 10(4):1257–1261, 1960. https://doi.org/10.2140/pjm.1960.10.1257
A. Yu. Levin, On an algorithm for the minimization of convex functions, Soviet Mathematics Doklady 6:286–290, 1965.
D. J. Newman, Location of the maximum on unimodal surfaces, Journal of the ACM 12(3):395–398, 1965. https://doi.org/10.1145/321281.321291
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

7 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

On the Graph Structure of Convex Polyhedra in n-Space II: Whitney's Theorem, a Graph Is n-Tuply Connected iff Any Two Points Are Joined by n Disjoint PathsResearch Paper

Motivation

Vertex connectivity measures how robust a network is against the failure of nodes. It can be measured in two ways that look different. One way counts the fewest nodes whose removal disconnects the network. The other counts the routes between two nodes that share no intermediate node. Whitney's theorem (1932) says that the two measures agree for every pair of nodes. It is the vertex form of Menger's theorem, and it underlies reliability analysis of communication and transportation networks, the design of fault-tolerant routing, and much of structural graph theory.

M. L. Balinski's 1961 paper On the graph structure of convex polyhedra in n-space proves that the graph of a bounded full-dimensional polyhedron in $n$ -space is $n$ -tuply connected (the subject of Mission I of this series). It then invokes Whitney's theorem to conclude that any two vertices of such a polyhedron are joined by $n$ disjoint paths. Balinski gives a short new proof of Whitney's theorem through the max-flow min-cut theorem of Ford and Fulkerson and of Dantzig and Fulkerson. That makes the theorem a consequence of linear programming duality. This mission formalizes that part of the paper: the network vocabulary, the max-flow min-cut theorem with capacities on both points and lines, the integrality of maximum flows, and Whitney's theorem itself.

Timeline.

1927: Menger states the disjoint-paths theorem for separating sets.
1932: Whitney proves the characterization of $n$ -connected graphs by $n$ disjoint paths between every pair of points.
1956: Ford and Fulkerson and Dantzig and Fulkerson prove the max-flow min-cut theorem.
1961: Balinski derives Whitney's theorem from it with a unit-capacity network.

Setting

A graph $G$ consists of a finite set $V$ of points and a set of lines, each line being a pair of distinct points. A path from $p_s$ to $p_k$ is a sequence of lines $(p_1,p_2),(p_2,p_3),\dots,(p_m,p_{m+1})$ with $p_1 = p_s$ , $p_{m+1} = p_k$ and $m \ge 1$ . Paths are disjoint if they have no point in common except possibly their first and last points.

$G$ is $n$ -tuply connected if it has at least $n+1$ points and, for every set $X$ of fewer than $n$ points, the graph $G - X$ remaining after deleting $X$ is connected. $G$ has $n$ disjoint paths from $p_s$ to $p_k$ if there are $n$ pairwise distinct paths from $p_s$ to $p_k$ , none of which repeats a point, and no two of which share a point other than $p_s$ and $p_k$ .

A network is a connected graph with a capacity $c(x) \ge 0$ on every point and $c(e) \ge 0$ on every line, and with a distinguished source $p_s$ and sink $p_k$ . A flow assigns a number $f(C) \ge 0$ to every path $C$ from $p_s$ to $p_k$ , such that for every point $x$ and every line $e$

\sum_{C \ni x} f(C) \le c(x), \qquad \sum_{C \ni e} f(C) \le c(e).

Its value is $\operatorname{val}(f) = \sum_C f(C)$ . A disconnecting set is a pair $(X,F)$ of points and lines that meets every walk from $p_s$ to $p_k$ . Its value is $\sum_{x\in X} c(x) + \sum_{e \in F} c(e)$ .

The unit network of the proof has capacity $1$ on every point except $p_s$ and $p_k$ , and capacity $n+1$ on every line except the line $p_sp_k$ (if present), which has capacity $1$ . In Lean these are IsNTuplyConnected, HasNDisjointPaths, IsFlow, flowValue, IsDisconnecting, cutValue, unitCapV and unitCapE, all in the namespace Balinski61.Whitney.

Formalization targets

Goal: Whitney's theorem (p. 434)

For a finite graph $G$ with at least two points and any $n \ge 0$ :

G \text{ is } n\text{-tuply connected} \iff \text{for all } p_s \ne p_k,\ G \text{ has } n \text{ disjoint paths from } p_s \text{ to } p_k.

Both directions are part of the goal.

Milestones, in the order of the proof

Max-flow min-cut (p. 433). In every network there is a number $M$ that is the value of some flow and of some disconnecting set, with every flow of value at most $M$ and every disconnecting set of value at least $M$ .
Integrality (p. 434). If all capacities are integers, some maximum flow has only integer path flows.
Min-cut in the unit network (p. 434). If $G$ is $n$ -tuply connected and $p_s \ne p_k$ , every disconnecting set of the unit network has value at least $n$ .
Paths from unit flows (p. 434). An integral flow of value at least $n$ in the unit network yields $n$ disjoint paths from $p_s$ to $p_k$ .
Sufficiency (p. 434). If every pair of distinct points is joined by $n$ disjoint paths, $G$ is $n$ -tuply connected.

Significance

Whitney's theorem turns a statement about all small deletion sets into the existence of explicit, verifiable path systems, and back again. In applications it certifies connectivity by exhibiting paths, and it certifies that connectivity is no larger by exhibiting a separating set. It is the base of the theory of $k$ -connected graphs: ear decompositions, the fan lemma, and the structure of minimally $k$ -connected graphs all use it. Inside this paper it supplies the COROLLARY that any two vertices of a bounded full-dimensional polyhedron in $n$ -space are joined by $n$ disjoint edge paths.

None of these results is formalized for vertex connectivity at this Mathlib revision. Mathlib has edge connectivity and connected components but no vertex Menger theorem. The Prove2Me library has max-flow min-cut statements for arc capacities only and integrality results for basic solutions of network LPs, but no flow model with capacities on points. A completed development gives a reusable vertex-capacitated max-flow min-cut theorem for undirected graphs and the first machine-checked Whitney theorem in this library. The results are classical and proved; the remaining work is the formalization.

Difficulty

The sufficiency direction is elementary. The necessity direction needs a global object (a flow, or a family of paths) to exist from purely local hypotheses about deletions. The obvious induction on $n$ , which deletes a point and applies the hypothesis to a smaller graph, does not keep the path systems disjoint. In Balinski's route the weight falls on max-flow min-cut and integrality for path flows with capacities on points, neither of which exists in the library. A second difficulty sits in a case the paper's proof skips: a disconnecting set of the unit network may use the line $p_sp_k$ (capacity $1$ ) together with up to $n-2$ points, and the deletion hypothesis of $n$ -tuple connectedness speaks only about points.

Formalization scope

Graphs are Mathlib SimpleGraphs on a Fintype with decidable equality and adjacency. Paths are walks with IsPath. A flow is a real function on the finite type G.Path ps pk of simple paths; "through a point" and "through a line" mean membership in the walk's support and edge list. Capacities are functions V → ℝ and Sym2 V → ℝ. Nonnegativity, connectivity of $G$ and $p_s \ne p_k$ are hypotheses of the network theorems.

The following readings of loose phrases are explicit in the statements:

"dropping out $n-1$ or fewer points" is $|X| < n$ ;
" $n$ disjoint paths" means $n$ pairwise distinct simple paths. The printed path syntax permits repeated vertices; in a graph with lines $p_s a$ , $p_s b$ , and $p_s p_k$ , the distinct walks $p_s,a,p_s,p_k$ and $p_s,b,p_s,p_k$ share only their endpoints even though the graph is not $2$ -tuply connected. The theorem therefore uses its conventional simple-path reading;
path flows live on simple paths (merging and shortcutting changes no maximum value);
the paper leaves the capacities of $p_s$ and $p_k$ in the unit network unassigned, and here they are $n+1$ ;
"the condition is sufficient is obvious" is the full statement that $n$ -tuple connectedness follows;
the hypothesis $|V| \ge 2$ is added to the goal and to sufficiency, because the paper's "any pair of points" presupposes it and the equivalence fails for a one-point graph.

The max-flow min-cut milestone states that the maximum and the minimum are attained. A statement that only bounds some flow by every cut is satisfied by the zero flow. A connectivity notion without the $n+1$ point count would make every complete graph $n$ -connected for all $n$ . Both trivializations are excluded.

Contributions welcome: a vertex-capacitated augmenting-path or LP-duality proof of max-flow min-cut for path flows, integrality by an augmenting-path argument, the unit-network lemmas, and direct combinatorial proofs of Whitney's theorem that bypass flows.

Selected references

M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific J. Math. 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168. https://doi.org/10.2307/2371086
L. R. Ford, Jr. and D. R. Fulkerson, Maximal flow through a network, Canadian J. Math. 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
G. B. Dantzig and D. R. Fulkerson, On the max-flow min-cut theorem of networks, in Linear Inequalities and Related Systems, Ann. of Math. Stud. 38, Princeton Univ. Press, 1956, 215–221. https://doi.org/10.1515/9781400881987
K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115

9 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Airline Seat Allocation with Multiple Nested Fare Classes 1: Protection Levels Solving f₁Pr[X₁ > p₁ ∩ … ∩ X₁ + … + X_k > p_k] = f_{k+1} Maximize Expected RevenueResearch Paper

Motivation

An airline sells the seats of one flight leg at several fares. Cheaper fares are booked earlier, so the airline must decide, while low-fare requests arrive, how many seats to hold back for later and more valuable passengers. In nested booking control a seat that could be sold at a low fare is always available to a higher fare. The airline therefore chooses protection levels: $p_k$ seats are reserved for the $k$ most expensive classes together, and a request of class $k+1$ is accepted only while more than $p_k$ seats remain.

For two classes the optimal protection level was found by Littlewood (1972): protect $p_1$ seats, where $f_1 \Pr[X_1 > p_1] = f_2$ . For more classes the industry used the EMSRa heuristic of Belobaba (1987, 1989), which applies Littlewood's rule to each pair of classes separately and adds the results. Brumelle and McGill (1993) gave the exact optimality conditions for any number of nested classes and showed that EMSRa is in general not optimal. Their conditions are part of the standard theory of single-leg revenue management, as presented in Talluri and van Ryzin (2004).

Setting

There are fare classes $k = 1, 2, \dots$ , numbered from the highest fare. Class $k$ has fare $f_k$ and random demand $X_k \ge 0$ . The standing assumptions (pp. 128–129) are: the demands are mutually independent random variables on a probability space $(\Omega, \mathcal F, P)$ , and the fares are strictly decreasing, $f_1 > f_2 > \cdots$ . Demands arrive in order of increasing fare: all of class $k+1$ before any of class $k$ . There are no cancellations or no-shows, and the decision to close a class depends only on the number of current bookings.

A protection-level policy is a vector $p = (p_1, p_2, \dots)$ with $p_k \ge 0$ ; the dummy $p_0 = 0$ . The revenue $R_k[s; p; x]$ of the $k$ highest classes with $s$ seats available and demand vector $x$ is defined recursively by (8)–(9), p. 130:

R_1[s; p; x] = f_1 \min(s, x_1),

R_{k+1}[s; p; x] = \begin{cases} R_k[s; p; x] & 0 \le s < p_k, \\ (s - p_k) f_{k+1} + R_k[p_k; p; x] & p_k \le s < p_k + x_{k+1}, \\ x_{k+1} f_{k+1} + R_k[s - x_{k+1}; p; x] & p_k + x_{k+1} \le s. \end{cases}

The expected revenue is $ER_k[s; p; X] = E\,R_k[s; p; X]$ . A policy $p$ is optimal if $ER_k[s; q; X] \le ER_k[s; p; X]$ for every policy $q$ , every $k \ge 1$ and every $s \ge 0$ .

For $g : \mathbb R \to \mathbb R$ , $\delta_+ g[s]$ and $\delta_- g[s]$ denote the right and left derivatives, and the subdifferential $\delta g[s]$ is the interval $[\delta_+ g[s], \delta_- g[s]]$ , with $\delta_- g[0] = +\infty$ (p. 131).

Formalization targets

Goal: Theorem 3 (p. 134)

If the protection levels satisfy

f_1 \Pr[X_1 > p_1 \cap X_1 + X_2 > p_2 \cap \dots \cap X_1 + \dots + X_k > p_k] = f_{k+1} \quad \text{for all } k \ge 1, \tag{31}

then $p$ is optimal.

Milestones

(27), p. 132: $ER_1$ is concave, and $\delta ER_1[s; p; X] = [f_1 \Pr[X_1 > s], f_1 \Pr[X_1 \ge s]]$ .
Lemma 1, p. 131: if $ER_k[\,\cdot\,; p; X]$ is concave on $s \ge 0$ and $f_{k+1} \in \delta ER_k[p_k; p; X]$ , then $E\{R_{k+1}[s; p; X] \mid X_{k+1}\}$ is concave in $s$ .
Corollary 1, p. 131: under the same conditions $ER_{k+1}[\,\cdot\,; p; X]$ is concave on $s \ge 0$ .
Theorem 1, p. 131: if $f_{k+1} \in \delta ER_k[p_k; p; X]$ for every $k$ (condition (20)), then $p$ is optimal.
Lemma 2, p. 134: under (31), for $s \ge p_k$ ,

\delta_+ E\{R_{k+1}[s; p; X] \mid X_{k+1}\} = f_1 \Pr[X_1 > p_1 \cap \dots \cap X_1 + \dots + X_k > p_k \cap X_1 + \dots + X_{k+1} > s \mid X_{k+1}].

Corollary 2, p. 134: the unconditional version (37) of Lemma 2 for $\delta_+ ER_{k+1}[s; p; X]$ .

Significance

Theorem 3 turns the optimal nested protection levels into a sequence of equations in the joint distribution of the cumulative demands $X_1 + \dots + X_j$ . For $k = 1$ it is Littlewood's rule. For $k \ge 2$ it identifies exactly what EMSRa approximates: EMSRa replaces the joint event in (31) by separate pairwise comparisons, and the paper shows (§4) that EMSRa can both over- and underestimate the optimal protection levels. The conditions are also the input of numerical methods: given demand forecasts, the levels $p_1, p_2, \dots$ are found one after another by solving (31), and §3.3 notes that a continuous joint demand distribution guarantees a solution exists.

The results are proved in the paper. As far as is known they have no machine-checked proof. Related platform items cover the two-class, integer-seat case from Belobaba (1987) (SeatInventory.Nested.emsr_protection_level_optimal) and the integer marginal-seat-revenue analogue of (27). They use a different model: two classes, natural-number seats and first differences. This mission formalizes the multi-class statement with real-valued seats and one-sided derivatives. A sister mission of the series proves the existence of optimal integer policies for integer-valued demand (Theorem 2).

Difficulty

The expected revenue is not differentiable: for discrete demand it is piecewise linear, so first-order conditions must be stated with one-sided derivatives and subdifferentials. The natural approach, to optimize each protection level separately with the others fixed, fails without concavity, and concavity of $ER_{k+1}$ in $s$ is not automatic. It holds only when the lower protection levels already satisfy the first-order conditions. Concavity and optimality must therefore be carried through one joint induction over the classes. Passing from (31) to (20) requires computing the right derivative of the expected revenue in closed form for every $s \ge p_k$ . This involves exchanging differentiation with expectation and conditioning on one class's demand at a time.

Formalization scope

Classes are indexed by $\mathbb N$ from $1$ ; fares, demands and protection levels are sequences $\mathbb N \to \mathbb R$ , with no bound on the number of classes. Seats and protection levels are real numbers.
Expectation is the Bochner integral on a probability space. The standing assumptions are a single predicate: probability measure, measurable nonnegative demands, mutual independence (iIndepFun), strictly decreasing fares.
$E\{\cdot \mid X_k\}$ evaluated at $X_k = y$ is the integral with the $k$ -th demand frozen at $y$ . Because the demands are independent this is a version of the conditional expectation, and "with probability 1" becomes "for every $y \ge 0$ ", which is stronger.
One-sided derivatives are HasDerivWithinAt on half-lines and must exist; derivWithin, which returns $0$ where no derivative exists, is not used. $\delta_- g[0] = +\infty$ is encoded as a disjunct.
Optimality is global: $p$ beats every policy $q$ at every level $k$ and every $s \ge 0$ . The page's proof of Theorem 1 shows coordinatewise optimality of $p_k$ , and the global form follows by induction on $k$ .
Fares are not assumed positive in the model: under (20) or (31) with strictly decreasing fares, $f_1 > 0$ follows. The milestone (27), stated with only the hypotheses on $X_1$ that it needs, assumes $X_1 \ge 0$ and $f_1 \ge 0$ , without which $ER_1$ is not concave.
No continuity of the demand distribution is assumed. Theorem 3 is conditional on a solution of (31).
The page's hypothesis of Lemma 1 has the misprint " $(p_0, \dots, p_{k+1})$ " for $(p_0, \dots, p_{k-1})$ . The formal statement uses the latter.

The goal assumes only the standing assumptions, $p \ge 0$ , and (31). It does not assume concavity, condition (20) or any derivative formula: those are milestones. A formalization that quantified optimality over one level, one value of $s$ , or policies differing from $p$ in one coordinate would be weaker than the paper and is excluded.

A complete development needs one-sided derivatives of integrals of piecewise-linear functions (dominated convergence for difference quotients), concavity of piecewise functions glued at points where the slopes decrease, and the independence calculus that turns $E[E\{\cdot \mid X_{k+1}\}]$ into an iterated integral. These pieces are reusable for other newsvendor-type and revenue-management models. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.

Selected references

S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes, Operations Research 41(1), 127–137, 1993. https://doi.org/10.1287/opre.41.1.127
K. Littlewood, Forecasting and Control of Passenger Bookings, AGIFORS Symposium Proceedings 12, 95–117, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 2005. https://doi.org/10.1057/palgrave.rpm.5170134
P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, 1987. http://hdl.handle.net/1721.1/68077
P. P. Belobaba, Application of a Probabilistic Decision Model to Airline Seat Inventory Control, Operations Research 37(2), 183–197, 1989. https://doi.org/10.1287/opre.37.2.183
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

8 thms2 active usersReviewed

Discrete Geometry Graph Theory Linear Optimization·Captain: mikedeng1

On the Graph Structure of Convex Polyhedra in n-Space I: The Vertices and Edges of a Bounded Full-Dimensional Polyhedron in n-Space Form an n-Tuply Connected GraphResearch Paper

Motivation

The vertices and edges of a convex polytope form a graph, and much of polyhedral combinatorics and of the theory of the simplex method is about that graph: how far apart two vertices can be (the Hirsch question), which graphs arise (Steinitz's theorem in dimension 3), and how robust the graph is. In 1961 M. L. Balinski proved that the graph of a full-dimensional polytope in $n$ -space cannot be disconnected by deleting fewer than $n$ vertices (Pacific J. Math. 11 (1961) 431–434). The result, now called Balinski's theorem, is a standard entry in textbooks on polytopes (Grünbaum, Convex Polytopes, §11.3; Ziegler, Lectures on Polytopes, Thm 3.14) and is the starting point of the study of connectivity of polytope graphs. Its proof uses only linear programming: the improving-edge step of the simplex method and the connectivity of the graph of a face.

Timeline. Steinitz (1922) characterised the graphs of 3-polytopes as the 3-connected planar graphs, so the case $n=3$ is contained in his theorem. Balinski (1961) proved $n$ -connectivity in every dimension. Whitney (1932) had shown that $n$ -connectivity is equivalent to the existence of $n$ disjoint paths between any two points; Balinski gives a new proof of that equivalence through max-flow min-cut and draws the corollary that any two vertices of a full-dimensional polytope in $\mathbb R^n$ are joined by $n$ disjoint edge paths.

Setting

Fix integers $n$ (the dimension of the space) and $m$ (the number of inequalities), vectors $a_1,\dots,a_m\in\mathbb R^n$ (the rows of a matrix $A$ ) and $b\in\mathbb R^m$ . Balinski's system (1) describes

S=\{X\in\mathbb R^n : AX\le b\}=\{x : \langle a_i,x\rangle\le b_i,\ i=1,\dots,m\},

written Hirsch.Hpoly a b in Lean. The paper assumes throughout two standing assumptions (StandingAssumptions a b):

the only solution to $AX\le0$ is $X=0$ ;
some $X^0$ satisfies $AX^0<b$ .

A vertex of $S$ is an extreme point. An edge is a segment $[u,v]$ , $u\neq v$ , that is an extreme subset of $S$ (Hirsch.Adj S u v). The graph $G(S)$ (polyGraph S) has the vertices as points and the edges as lines.

A graph is $n$ -tuply connected (IsNTuplyConnected G n) if it has at least $n+1$ points and remains connected after dropping out any $n-1$ or fewer points. Two points are joined by $n$ disjoint paths (HasDisjointPaths G u v n) if there are $n$ distinct paths from $u$ to $v$ which share no point other than $u$ and $v$ .

Formalization targets

Goal: the THEOREM (p. 432)

\text{(i), (ii)}\ \Longrightarrow\ G(S)\ \text{is } n\text{-tuply connected}.

That is, $|\operatorname{ext} S|\ge n+1$ and $G(S)-X$ is connected for every set $X$ of at most $n-1$ vertices.

Milestones, in the order the proof uses them

$S$ has finitely many vertices, $S=\operatorname{conv}(\operatorname{ext}S)$ , and $S$ lies in no hyperplane $\{\langle c,x\rangle=d\}$ , $c\neq0$ (p. 432).
$|\operatorname{ext}S|\ge n+1$ (p. 432).
Preliminary remark: every vertex has degree at least $n$ in $G(S)$ (p. 432).
Improving neighbour: if $\langle c,\cdot\rangle$ is not maximal on $S$ at a vertex $v$ , some neighbour $w$ of $v$ has $\langle c,w\rangle>\langle c,v\rangle$ (p. 432, case (a)).
The graph of a face is connected (p. 433, case (a)); this is the published, proved Hirsch.face_connected.
Two vertices with $\langle c,\cdot\rangle>d$ are joined by a path in $G(S)$ all of whose points satisfy $\langle c,\cdot\rangle>d$ (pp. 432–433, case (a)).
COROLLARY (p. 434): any two distinct vertices are joined by $n$ disjoint paths:

u\neq v\ \Longrightarrow\ \exists\,P_1,\dots,P_n:\ P_i\cap P_j\subseteq\{u,v\}\ (i\neq j).

Significance

The result. Balinski's theorem says that polytope graphs are highly connected, which constrains which graphs can be graphs of $n$ -polytopes and is the base case of later results on the connectivity of polytope graphs. Together with Whitney's theorem it gives $n$ vertex-disjoint edge paths between any two vertices. The improving-neighbour step is the local optimality criterion of the simplex method.

Formalizing it. The theorem is classical and proved; it has not been formalized. On this platform the case $n=1$ (the graph of a polytope is connected) is proved as Hirsch.graph_connected_general, and connectivity of the graph of each face as Hirsch.face_connected, both by Shuze Chen; LinearOptimization.polyhedron_bounded_convex_hull_extreme proves the convex-hull clause of milestone 1 for a matrix-form polyhedron under the hypotheses "nonempty and bounded", and ConnPreservingHamPath.IsKConnected.le_ncard_neighborSet proves "connectivity at most minimum degree" for its own notion of $k$ -connectivity. This mission adds vertex $n$ -connectivity in every dimension, the simplex improving-neighbour lemma for H-polytopes, and the corollary on disjoint paths. The corollary needs Whitney's theorem, which is the goal of the companion mission On the Graph Structure of Convex Polyhedra in n-Space II.

Difficulty

An induction on dimension through facets does not directly control where the deleted vertices lie. Balinski's argument leans on several facts the paper calls obvious or clear: that a vertex with no improving neighbour is optimal, that the graph of a face is connected, that $n$ points of $\mathbb R^n$ lie on a common hyperplane while $S$ does not, and that $S$ has at least $n+1$ vertices. Each needs its own development from the two algebraic assumptions, in particular the passage from (i)–(ii) to a bounded full-dimensional polytope with finitely many vertices, and the identification of extreme segments with edges. Deleting fewer than $n-1$ vertices, which the definition requires and the proof's text does not treat, needs a separate argument. The proof also tacitly needs the affine function to take a nonzero value at some vertex.

Formalization scope

Space: EuclideanSpace ℝ (Fin n); rows a : Fin m → EuclideanSpace ℝ (Fin n), b : Fin m → ℝ. The published Hirsch_model names the dimension d and the number of rows n; here $n$ is the dimension, as in the paper.
The two standing assumptions are hypotheses of every theorem, stated literally, not replaced by "bounded and full-dimensional".
Vertices are Set.extremePoints ℝ S; edges are Hirsch.Adj (extreme segments). $G(S)$ is a SimpleGraph on the vertex subtype.
Counts use Set.encard; " $n-1$ or fewer points" is X.encard < n. A path of the paper is a Mathlib Walk (consecutive points distinct).
Explicit readings of loose phrases: "form a graph" includes finiteness of the vertex set (milestone 1); "lies within no hyperplane" is "for every $c\neq0$ and $d$ some point of $S$ has $\langle c,x\rangle\neq d$ "; "whose graph is clearly connected" is the referenced Hirsch.face_connected; the affine function $y_0$ of the proof is an arbitrary $x\mapsto\langle c,x\rangle-d$ , and only the "maximum"/" $>$ " forms are stated (the others follow for $-c,-d$ ); "at least $n$ disjoint paths between any pair of vertices" is a family of $n$ pairwise distinct paths without repeated points, sharing only their endpoints, between two distinct vertices.
Trivializing formalizations are ruled out: edges are not arbitrary pairs of vertices (that makes the goal nearly free), $n$ -tuply connected requires both the point count and connectivity after deletion, and the disjoint paths must be pairwise distinct (otherwise $n$ copies of one edge would do).
Welcome contributions: the passage from (i)–(ii) to a polytope (finiteness of vertices, Krein–Milman in this setting), the simplex optimality criterion for H-polytopes, and conversion between Hirsch walk vocabulary and Mathlib Walks; all are reusable beyond this mission.

Selected references

M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific J. Math. 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168. https://doi.org/10.2307/2371086
A. W. Tucker, Linear inequalities and convex polyhedral sets, Proc. Second Symposium in Linear Programming, Washington D.C., 1955, 569–602.
B. Grünbaum, Convex Polytopes, 2nd ed., Springer GTM 221, 2003, §11.3. https://doi.org/10.1007/978-1-4613-0019-9
G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995, Theorem 3.14. https://doi.org/10.1007/978-1-4613-8431-1

11 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey 4: Under Sennott's Conditions an Average-Cost Optimal Stationary Policy ExistsResearch Paper

Motivation

Many controlled queueing, inventory and maintenance systems are modelled as controlled Markov processes (CMPs) on a countable state space whose one-stage cost grows without bound: the holding cost of a queue grows with its length. For such systems the natural performance measure is the long-run average cost, and the basic question is whether some simple policy, one that looks only at the current state and never randomizes, is optimal among all policies, including those that use the whole history.

When the cost is bounded, the classical answer goes through a bounded solution of the average cost optimality equation (ACOE). For unbounded costs, bounded solutions are rare: in many queueing models the relative value function grows with the state, and growth conditions such as (5.2) of the survey may fail (Arapostathis et al. 1993, p. 307). Sennott (1986; 1989) replaced boundedness by one-sided conditions on the discounted value functions, which are often easy to verify for queueing models because the relative values are bounded below. This mission formalizes Sennott's existence theorem in the form given in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus, Theorem 5.9.

Timeline. For bounded costs, Ross (1983, the survey's Theorem 5.2) obtained a bounded ACOE solution, and with it an optimal stationary policy, when the differential discounted values are uniformly bounded. Federgruen, Hordijk and Tijms (1979) treated unbounded costs under Lyapunov-type recurrence conditions, which restrict how fast the cost may grow (survey, Remark 5.7). Sennott (1986, 1989) replaced these by a uniform lower bound and a pointwise, one-step integrable upper bound on the differential discounted values. The survey (1993, Theorem 5.9) states the result with compact action sets and continuous data, and Sennott's 1999 book (§7.2) gives the finite-action version in textbook form.

Setting

The state space is $S=\{0,1,2,\dots\}$ . For each state $i$ the set $U(i)$ of admissible actions is a nonempty compact subset of a metric space $A$ . Choosing $a\in U(i)$ in state $i$ costs $c(i,a)\ge0$ , and the next state is $j$ with probability $P(j\mid i,a)$ . For fixed $i,j$ , the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$ .

An admissible policy $\pi\in\Pi$ chooses the action at time $t$ according to a probability distribution $\pi_t(\cdot\mid h_t)$ concentrated on $U(x_t)$ , where $h_t=(x_0,a_0,\dots,x_t)$ is the history; it may use the whole history and may randomize. A stationary deterministic policy $f\in\Pi_{SD}$ is a map $f:S\to A$ with $f(i)\in U(i)$ , applied at every step. Given an initial state $i$ and a policy $\pi$ , the states and actions $(X_t,A_t)$ form a stochastic process with law $P^\pi_i$ and expectation $E^\pi_i$ .

For $\beta\in(0,1)$ , the discounted cost and the average cost of $\pi$ from $i$ are

J_\beta(i,\pi)=E^\pi_i\sum_{t=0}^\infty\beta^tc(X_t,A_t),\qquad J(i,\pi)=\limsup_{N\to\infty}\frac1N\,E^\pi_i\sum_{t=0}^{N-1}c(X_t,A_t),

both in $[0,\infty]$ . The optimal values are $J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi)$ and $J^*(i)=\inf_{\pi\in\Pi}J(i,\pi)$ , and the differential discounted value is $h_\beta(i)=J^*_\beta(i)-J^*_\beta(0)$ . A policy $f\in\Pi_{SD}$ is AC-optimal if $J(i,f)=J^*(i)$ for every $i$ .

Sennott's conditions (Assumptions 5.14–5.16) are:

$J^*_\beta(i)<\infty$ for all $i\in S$ and $\beta\in(0,1)$ ;
there is a nonnegative integer $L$ with $h_\beta(i)\ge-L$ for all $i$ and $\beta$ ;
there is $M:S\to\mathbb R_+$ with $h_\beta(i)\le M(i)$ for all $i$ and $\beta$ , and for each $i$ some $a(i)\in U(i)$ with $\sum_jP(j\mid i,a(i))M(j)<\infty$ .

Formalization targets

Goal: Theorem 5.9

\text{Under Assumptions 5.14–5.16, there is } f\in\Pi_{SD}\text{ with } J(i,f)=\inf_{\pi\in\Pi}J(i,\pi)\ \text{ for every } i\in S.

The goal asserts only existence. It does not fix the optimal cost, and it does not claim that the optimal cost is constant or that an optimality equation holds.

Milestones

Theorem 2.1 (i), (iii), countable form: the discounted cost optimality equation $J^*_\beta(i)=\inf_{a\in U(i)}\{c(i,a)+\beta\sum_jP(j\mid i,a)J^*_\beta(j)\}$ and a $\beta$ -discount optimal $f_\beta\in\Pi_{SD}$ .
Display (5.15): $(1-\beta)J^*_\beta(0)+h_\beta(i)=c(i,f_\beta(i))+\beta\sum_jP(j\mid i,f_\beta(i))h_\beta(j)$ .
The limit objects: along a subsequence $\beta_n\to1$ , $f_{\beta_n}\to f$ , $h_{\beta_n}\to h\ge-L$ pointwise, and $(1-\beta_n)J^*_{\beta_n}(i)\to\rho^*$ , a constant.
The average cost optimality inequality (ACOI) $\rho^*+h(i)\ge c(i,f(i))+\sum_jP(j\mid i,f(i))h(j)$ .
An ACOI along $f$ with $h$ bounded below gives $J(i,f)\le\rho$ .
Theorem A.2: the Abelian inequalities between Cesàro and Abel means (already on the platform).
$J(i,\pi)\ge\rho^*$ for every $\pi\in\Pi$ .

Significance

The result. Theorem 5.9 is the standard existence theorem for average-optimal stationary policies with unbounded costs on countable state spaces. Its conditions are verified routinely for controlled queues, where relative values are monotone in the queue length and hence bounded below. It shows that randomization and memory do not reduce the long-run average cost, and the ACOI it produces is the starting point for value and policy iteration and for structural results such as threshold policies.

Formalizing it. The theorem is proved in the literature (Sennott 1989; Sennott 1999, Theorem 7.2.3; survey, p. 308). It has no machine-checked proof. The finite-action version, SennottDP.SEN.thm_7_2_3_sen_acoi, is posed on Prove2Me and still open; this mission poses the compact-action version, which needs continuity and compactness arguments that the finite case avoids. A formal proof also requires a general theory of history-dependent policies on path space (Ionescu-Tulcea), the discounted optimality equation with unbounded costs, and the passage from Abel to Cesàro means. All three are reusable well beyond this paper.

Difficulty

The obvious argument lets $\beta\to1$ in the discounted optimality equation (5.6). Two steps fail without more structure. First, $h_\beta$ need not converge, and with unbounded costs it is not uniformly bounded, so the limit has to be taken pointwise along a subsequence, with only a lower bound uniform in the state. Second, the limit cannot be passed through the infinite sum $\sum_jP(j\mid i,a)h_\beta(j)$ by dominated convergence, because no integrable dominating function exists for every action. Only an inequality survives (Fatou), so the limit is an ACOI, not an equation. The inequality then has to be turned into optimality against all of $\Pi$ , which includes history-dependent randomized policies whose costs are not described by any optimality equation. The lower bound for these comes from comparing Cesàro and Abel means, not from dynamic programming.

Formalization scope

The Lean development uses the following representation and conventions.

States, actions, model. The state space is ℕ. The action space is a metric space with its Borel σ-algebra. U i is nonempty and compact, c is measurable and nonnegative on admissible pairs, P is a Markov kernel, and $c(i,\cdot)$ , $P(j\mid i,\cdot)$ are continuous on $U(i)$ .
Policies. $\Pi$ consists of all history-dependent randomized policies, with admissibility required almost surely. $J^*$ and $J^*_\beta$ are infima over all of $\Pi$ , never over stationary policies only. Restricting the infimum to $\Pi_{SD}$ would drop the Tauberian half of the theorem and is not the paper's statement.
Costs. Costs are lower Lebesgue integrals in $[0,\infty]$ against the Ionescu-Tulcea path measure, and the average cost is a limsup in $[0,\infty]$ .
Explicit hypotheses. $h_\beta$ is a difference of real parts and is used only under Assumption 5.14, so it is never read off an infinite $J^*_\beta$ . The quantifiers over $i$ and $\beta$ in Assumption 5.15, implicit on the page, are universal, and $L$ is a natural number as printed. Every series $\sum_jP(j\mid i,a)h(j)$ carries a summability hypothesis or conclusion.
Corrected claim. Remark 5.8(a) as printed claims that any scalar $\rho$ satisfying the ACOI with $h$ bounded below is the optimal average cost. That is false ( $h\equiv0$ , $\rho=\sup c$ ), so only the inequality $J(i,f)\le\rho$ , which the proof uses, is stated.
Sequences. The milestones about limits are stated for any sequence $\beta_n\in(0,1)$ with $\beta_n\to1$ , not only increasing ones.

A trivializing formalization is excluded. Sennott's conditions are satisfiable (a one-action, zero-cost model satisfies all three), and AC-optimality is measured against all admissible policies, so the goal cannot hold vacuously or by a junk value.

Welcome contributions: the Markov property of the path measure for history-dependent policies; the discounted optimality equation for nonnegative unbounded costs; a measurable-selection or compactness argument for minimizing actions on compact $U(i)$ ; Fatou's lemma for series with converging weights; and the Abelian inequalities in a form applied to expected costs.

Selected references

A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Oper. Res. 37(4) (1989) 626–633. https://doi.org/10.1287/opre.37.4.626
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
L. I. Sennott, A new condition for the existence of optimal stationary policies in average cost Markov decision processes, Oper. Res. Lett. 5 (1986) 17–23 (reference [155] of the survey; no stable link checked).
S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, New York, 1983 (reference [150] of the survey).
A. Federgruen, A. Hordijk, H. C. Tijms, Denumerable state semi-Markov decision processes with unbounded costs, average cost criterion, Stochastic Process. Appl. 9 (1979) 223–235 (reference [53] of the survey).
R. Sznajder, J. A. Filar, Some comments on a theorem of Hardy and Littlewood, J. Optim. Theory Appl. 75 (1992) (reference [176] of the survey, cited for Theorem A.2).

11 thms2 active usersReviewed

Combinatorics Machine Learning Theoretical Computer Science·Captain: mikedeng1

A Characterization of Multiclass Learnability 1: Classes of Finite DS Dimension Have n → r Sample Compression Schemes with r Polylogarithmic in nResearch Paper

Motivation

In multiclass classification a learner sees examples $(x, y)$ with $x$ in a domain $\mathcal X$ and a label $y$ in a set $\mathcal Y$ , and must predict labels of new points. When $\mathcal Y$ is finite, the Natarajan dimension characterizes PAC learnability, extending the role of the VC dimension in binary classification (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler, Long 1995). Label sets in practice are often unbounded: structured prediction, ranking, and language modelling all predict from very large or infinite label spaces. For infinite $\mathcal Y$ the Natarajan dimension fails to characterize learnability, and the question of which combinatorial parameter does was left open by Daniely and Shalev-Shwartz.

Timeline:

1989–1995. Natarajan, then Ben-David et al. and Haussler–Long: for finite $\mathcal Y$ , learnability is equivalent to finite Natarajan dimension, with sample complexity depending on $\log|\mathcal Y|$ .
2011–2015. Daniely, Sabato, Ben-David and Shalev-Shwartz show that ERM can fail for multiclass problems with many labels. Daniely and Shalev-Shwartz (COLT 2014) introduce the DS dimension, prove that finite DS dimension is necessary for learnability, and ask whether it is sufficient.
2022. Brukhim, Carmon, Dinur, Moran, Yehudayoff prove sufficiency, so the DS dimension characterizes multiclass PAC learnability, and show that the Natarajan dimension does not.

Setting

A concept class is a set $\mathcal H\subseteq\mathcal Y^{\mathcal X}$ of functions. For a sequence $S=(x_1,\dots,x_n)$ the projection $\mathcal H|_S\subseteq\mathcal Y^n$ is the set of label words $(h(x_1),\dots,h(x_n))$ , $h\in\mathcal H$ . A finite non-empty set $B\subseteq\mathcal Y^d$ is a pseudo-cube if every $h\in B$ has, in every coordinate $i$ , a neighbour $g\in B$ that differs from $h$ exactly in coordinate $i$ . The sequence $S$ is DS-shattered if $\mathcal H|_S$ contains an $n$ -dimensional pseudo-cube, and the DS dimension $d_{DS}(\mathcal H)$ is the maximum length of a DS-shattered sequence. The Natarajan dimension $d_N(\mathcal H)\le d_{DS}(\mathcal H)$ is the same with Boolean cubes $\prod_i\{f(i),g(i)\}$ , $f(i)\ne g(i)$ , in place of pseudo-cubes.

A sample $S\in(\mathcal X\times\mathcal Y)^n$ is $\mathcal H$ -realizable if some $h\in\mathcal H$ is consistent with it. An $n\to r$ sample compression scheme for $\mathcal H$ (Littlestone and Warmuth 1986) is a single reconstruction function $\rho:(\mathcal X\times\mathcal Y)^r\to\mathcal Y^{\mathcal X}$ such that every realizable sample of size $n$ contains $r$ of its examples $S'$ with $\rho(S')$ consistent with the whole sample. Logarithms are base $2$ throughout.

Formalization targets

Goal: Theorem 36 (p. 22)

For $\mathcal H$ with $d_{DS}(\mathcal H)=d_{DS}<\infty$ and $d_N(\mathcal H)=d_N$ , and all integers $n,t>0$ , there is an $n\to r$ sample compression scheme, $r\le n$ , with

r\le\left(\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)+10^3d_N\log\left(\binom{d_{DS}+t+1}{t+1}\log(2n)\right)\right)\log(2n).

Milestones

The scheme combines two components, each with its own chain of results:

List learning from the DS dimension. Lemma 13 (orientations of out-degree $\le d$ on $\mathcal Y^{d+1}$ ), Claim 16 (the one-inclusion algorithm is right on some leave-one-out example), Fact 14 (leave-one-out symmetrization), Proposition 32 (a list PAC learner with list size $\binom{d+t}{t}$ and success probability $\frac{t+1}{d+t+1}$ ), Lemma 39 (an $n\to r_1$ list compression scheme with $r_1\le\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)\log(2n)$ and menu size $\le\binom{d_{DS}+t+1}{t+1}\log(2n)$ ).
Learning from a menu via shifting. Claim 22, Corollary 23, Claim 26, Proposition 27 ( $\operatorname{avd}\le4d_E$ ), Corollary 28, Lemma 29 ( $d_E\le5d_N\log p$ ), Lemma 17 (orientations of out-degree $\le20d_N\log p$ on $[p]^n$ ), Proposition 34 (error $\le20d_N\log(p)/n$ given a $p$ -menu), Lemma 40 (an $n\to r_2$ compression scheme given a $p$ -menu with $r_2\le10^3d_N\log(p)\log(2n)$ ).

Significance

Theorem 36 is the algorithmic heart of the characterization: by the standard "compression implies generalization" argument it gives PAC learnability of every class of finite DS dimension, with sample complexity $\tilde O(d_{DS}^{3/2}/\epsilon)$ in the realizable case ( $t=\lceil d_{DS}^{1/2}\rceil$ ), and with the agnostic case following by known reductions. It also exhibits sample compression schemes of size polylogarithmic in $n$ for multiclass classes with infinitely many labels, in contrast to the constant-size schemes known for finite VC classes.

The result is proved in the paper; none of it is formalized. The formalization would produce a machine-checked theory of one-inclusion graphs and their orientations, multiclass shifting, the exponential dimension, list learning, and sample compression schemes for arbitrary label sets. These objects recur throughout learning theory (one-inclusion graphs in optimal PAC learning, shifting in VC theory), so the infrastructure is reusable beyond this mission.

Difficulty

The natural first idea, running empirical risk minimization or bounding the Natarajan dimension, fails: classes with Natarajan dimension $1$ and infinitely many labels can be unlearnable, and ERM can fail even for learnable classes. The DS dimension gives only a weak guarantee: by Claim 16, among $d+1$ leave-one-out runs, one is correct. Turning this into a learner requires a list learner whose menus are still of unbounded total size, and then learning with a menu of size $p$ , where the obstacle is controlling one-inclusion graph orientations over $[p]^n$ by the Natarajan dimension. Multiclass shifting does not preserve the average degree (Example 20), so the binary argument breaks down, and a new potential ( $\operatorname{avd}'$ ) and a new dimension ( $d_E$ ) are needed. Lemma 13 for infinite classes needs a compactness argument.

Formalization scope

Lean conventions:

A class is H : Set (X → Y) with arbitrary types X, Y; sequences and samples are functions on Fin n ( $[n]$ is 0-based).
The DS, Natarajan and exponential dimensions are suprema in ℕ∞, so unbounded families give ⊤; hypotheses are written dsDim H = dDS with dDS : ℕ. A pseudo-cube is required to be finite.
Logarithms are Real.logb 2. Menu sizes use Set.encard.
A compression scheme is a reconstruction function fixed before the sample (∃ ρ, ∀ S, ∃ S'); a subsample may repeat and reorder examples. Theorem 36 states $r\le n$ explicitly.
Orientations of the one-inclusion graph of $V\subseteq\mathcal Y^m$ are maps sending a direction $i$ and a vertex $v$ to the head of the edge of direction $i$ through $v$ ; the out-degree of $v$ counts directions whose head is not $v$ .
Classes over $[p]$ use labels Fin p; the shifting condition $1\le g(i)\le|e_f|$ becomes $g(i)<|e_f|$ .
The one-inclusion algorithm (Algorithms 1 and 3) is parametrized by a permutation-equivariant choice of minimal orientations, the reading under which the paper's leave-one-out proofs are valid; statements about the algorithm hold for every such choice. Its default output on non-realizable input requires a non-empty label set, assumed in Claim 16 and Propositions 32 and 34. Lemma 40 assumes a non-empty label set because it is false for $\mathcal X\ne\emptyset=\mathcal Y$ .
Distributions are discrete (PMF), and i.i.d. probabilities are sums over $\mathcal Z^m$ . The measure-theoretic generality of the paper is not attempted.

A trivial formalization is ruled out by these choices. Placing the reconstruction function after the sample would let it output the consistent hypothesis. A dimension in ℕ defined by sSup would be $0$ for infinite dimension. Pseudo-cubes without finiteness would change the dimension (Example 8).

Contributions welcome: proofs of any milestone, in particular the shifting results of §3 (self-contained combinatorics on finite classes), Fact 14 (pure discrete probability), and Lemma 13; general-purpose lemmas about one-inclusion graphs, orientations and sample compression schemes are reusable by other learning-theory missions.

Selected references

N. Brukhim, D. Carmon, I. Dinur, S. Moran, A. Yehudayoff, A Characterization of Multiclass Learnability, FOCS 2022; arXiv:2203.01550v1 (2022). https://arxiv.org/abs/2203.01550
A. Daniely, S. Shalev-Shwartz, Optimal Learners for Multiclass Problems, COLT 2014. https://arxiv.org/abs/1405.2690
N. Littlestone, M. Warmuth, Relating Data Compression and Learnability, unpublished technical report, University of California, Santa Cruz, 1986 (no stable link).
D. Haussler, N. Littlestone, M. Warmuth, Predicting {0,1}-Functions on Randomly Drawn Points, Information and Computation 115(2), 1994. https://doi.org/10.1006/inco.1994.1097
D. Haussler, P. M. Long, A Generalization of Sauer's Lemma, Journal of Combinatorial Theory, Series A 71(2), 1995. https://doi.org/10.1016/0097-3165(95)90006-3
S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of Learnability for Classes of {0,…,n}-Valued Functions, JCSS 50(1), 1995. https://doi.org/10.1006/jcss.1995.1008
B. K. Natarajan, On Learning Sets and Functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804

20 thms2 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All 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

Revenue Management with Forward-Looking Buyers: Under Weakly Decreasing Demand the Deterministic Optimal Cutoffs Fall over Time and Satisfy One-Period Look-AheadResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 17)

Central milestone: Theorem 1 (p. 15)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Convex Optimization: Algorithms and Complexity XV: SVRG with η = 1/(10β) and k = 20κ Contracts the Expected Optimality Gap by 0.9 per EpochTextbook

Motivation

Setting

Formalization targets

Goal: geometric contraction across epochs

Milestones: second moments and a single epoch

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

Robust Wasserstein Profile Inference and Applications to Machine Learning 2: ℓp-Regularized Logistic Regression and the Hinge-Loss SVM Are Wasserstein DRO under a Label-Preserving Transport CostResearch Paper

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