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.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

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.960614Formalized record

4 provers on it7 of 7 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.995561Formalized record

3 provers on it5 of 5 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.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 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.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 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

38 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.25Formalized record

16 provers on it9 of 9 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)

See all campaigns →

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.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

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.960614Formalized record

4 provers on it7 of 7 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.995561Formalized record

3 provers on it5 of 5 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.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 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.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 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

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Algebra Algebraic Geometry·Captain: Lucas

Hilbert's Nullstellensatz (Wikipedia) I: Formulations over Algebraically Closed FieldsTextbook

Motivation

Hilbert's Nullstellensatz ("theorem of zeros") is the basic link between algebra and geometry. It was proved by David Hilbert in his second major paper on invariant theory in 1893, after his 1890 paper that proved the basis theorem, and it is a foundational result of algebraic geometry. It gives an algebraic criterion for when a system of polynomial equations over an algebraically closed field has a solution, and an algebraic criterion for when one polynomial vanishes wherever a given family does. Every dictionary between affine varieties and ideals — points and maximal ideals, algebraic sets and radical ideals, irreducible sets and prime ideals — is a consequence.

This mission follows the Wikipedia article Hilbert's Nullstellensatz (snapshot of 27 September 2026): its introduction, its section Formulations, the statement of Zariski's lemma from Proofs, and the first theorem of Generalizations (finitely generated algebras over Jacobson rings).

Setting

Let $k$ be a field and $K$ an algebraically closed field extension of $k$ (every non-constant polynomial over $K$ has a root in $K$ ). Write $k[X_1,\dots,X_n]$ for the polynomial ring in $n$ variables. A point is an $n$ -tuple $a = (a_1,\dots,a_n) \in K^n$ , and $f(a)$ is the value of a polynomial $f$ at $a$ .

For an ideal $J$ , the algebraic set (zero locus) is $\mathrm V(J) = \{a \in K^n : f(a) = 0 \text{ for all } f \in J\}$ .
For $U \subseteq K^n$ , the vanishing ideal is $\mathrm I(U) = \{p : p(a) = 0 \text{ for all } a \in U\}$ .
The radical of $J$ is $\sqrt J = \{p : p^r \in J \text{ for some } r \in \mathbb N\}$ .
For $a \in K^n$ , $\mathfrak m_a = (X_1 - a_1, \dots, X_n - a_n)$ is the ideal of the point.
A subset $W \subseteq K^n$ is irreducible (Zariski topology) if it is nonempty and is not covered by two algebraic sets without lying in one of them.
A commutative ring is Jacobson if every radical ideal is an intersection of maximal ideals.

Formalization targets

Goal: the Nullstellensatz

If $p \in k[X_1,\dots,X_n]$ vanishes on $\mathrm V(J) \subseteq K^n$ , then

\exists\, r \in \mathbb N,\qquad p^r \in J.

This is the statement of the article's section Formulations, with the coefficient field $k$ and the algebraically closed field $K$ allowed to differ.

Milestones

Systems of equations. Over algebraically closed $K$ : a system $f_1 = \dots = f_m = 0$ has no solution in $K^n$ iff $g_1 f_1 + \dots + g_m f_m = 1$ for some $g_i$ ; and $f$ vanishes on all solutions iff $f^r = g_1 f_1 + \dots + g_m f_m$ for some $r$ and $g_i$ .
Geometric form. $\mathrm I(\mathrm V(J)) = \sqrt J$ .
Weak Nullstellensatz. A proper ideal of $k[X_1,\dots,X_n]$ has a common zero in $K^n$ ; algebraic closedness is needed, as $(X^2+1) \subseteq \mathbb R[X]$ shows; for $K = \mathbb C$ , $n = 1$ this is the fundamental theorem of algebra: $P$ has a complex root iff $\deg P \ne 0$ .
Correspondences. $\mathrm V$ is an order-reversing bijection from radical ideals onto algebraic sets, with inverse $\mathrm I$ ; $\mathrm I(\{a\}) = \mathfrak m_a$ is maximal; every maximal ideal of $K[X_1,\dots,X_n]$ is some $\mathfrak m_a$ ; an algebraic set $W$ is irreducible iff $\mathrm I(W)$ is prime.
Intersections. $\sqrt J = \bigcap_{\mathfrak m \supseteq J} \mathfrak m = \bigcap_{a \in \mathrm V(J)} \mathfrak m_a$ .
Zariski's lemma. A field finitely generated as an algebra over a field $K$ is a finite extension of $K$ .
Jacobson rings. A finitely generated algebra $S$ over a Jacobson ring $R$ is Jacobson, and for a maximal ideal $\mathfrak n \subseteq S$ , $\mathfrak n \cap R$ is maximal and $S/\mathfrak n$ is finite over $R/(\mathfrak n \cap R)$ .

Significance

The Nullstellensatz makes the zero sets of polynomial systems accessible through ideals: solvability of a system becomes the ideal-membership question $1 \in J$ , and the geometry of algebraic sets becomes the algebra of radical ideals. Consequences include the identification of the points of $K^n$ with the maximal ideals of $K[X_1,\dots,X_n]$ , the description of irreducible algebraic sets by prime ideals, and the reduction of the fundamental theorem of algebra to the case $n=1$ . The Jacobson-ring version extends the first equality of the intersection formula to every finitely generated algebra over a field.

All statements here are classical and proved. Mathlib already contains versions of several of them in its own vocabulary (Jacobson rings, Zariski's lemma, and a Nullstellensatz over an algebraically closed coefficient field). What this mission adds is a single set of statements matching the article's formulations: the version with separate fields $k \subseteq K$ , the explicit systems-of-equations form, the point-ideal and irreducibility correspondences over $K^n$ , and the intersection formula — and, for solvers, the bridges from these concrete statements to Mathlib's abstract ones.

Difficulty

The inclusion $\sqrt J \subseteq \mathrm I(\mathrm V(J))$ is immediate; the content is the reverse inclusion, which requires producing a point of $K^n$ from purely algebraic data. When $k \ne K$ the ideal $J$ lives over $k$ while the points live over $K$ , so a result stated only for $K[X_1,\dots,X_n]$ does not apply directly: an ideal of $k[X]$ must be related to the ideal it generates in $K[X]$ without losing membership information. For the correspondences, the explicit ideals $\mathfrak m_a$ and the closed-set definition of irreducibility must be matched with the abstract notions (maximal spectrum, irreducible closed subsets) used in the library.

Formalization scope

Points of $K^n$ are functions $\mathrm{Fin}\,n \to K$ ; polynomials are MvPolynomial (Fin n) k. When $k \ne K$ , $K$ is a $k$ -algebra and evaluation of a polynomial over $k$ at a point of $K^n$ goes through $k \to K$ .
$n = 0$ is allowed throughout; so is the unit ideal $J = k[X]$ , where $\mathrm V(J) = \emptyset$ and empty intersections of ideals are the whole ring.
Irreducibility is stated through closed sets (algebraic sets) without putting a topology on $K^n$ . The degree in the $n=1$ statement is Mathlib's Polynomial.degree, with $\deg 0 = -\infty$ .
In the goal, the exponent $r$ may be $0$ ; that witness only works when $J$ is the unit ideal, so it does not trivialize the statement.
Out of scope: the proofs via resultants and Gröbner bases, the effective Nullstellensatz, Lang's infinite-variable version, the scheme-theoretic generalizations, and the projective and analytic Nullstellensätze.
Reusable output: the definitions $\mathrm V$ , $\mathrm I$ , algebraic set, irreducible set and $\mathfrak m_a$ , and bridges to Mathlib's MvPolynomial.zeroLocus, MvPolynomial.vanishingIdeal, and IsJacobsonRing.

Selected references

D. Hilbert, Ueber die vollen Invariantensysteme, Mathematische Annalen 42 (1893).
Wikipedia contributors, Hilbert's Nullstellensatz. https://en.wikipedia.org/wiki/Hilbert%27s_Nullstellensatz
M. F. Atiyah, I. G. Macdonald, Introduction to Commutative Algebra, Addison-Wesley, 1969, Chapters 5 and 7.
D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Springer GTM 150, 1995, Chapter 4.

15 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Selected Topics in Column Generation III: Ryan–Foster Branching — a Fractional Basic Set-Partitioning Solution Covers Some Row Pair FractionallyResearch Paper

Motivation

Column generation solves linear programs with far too many variables to list: one works with a small subset $J' \subseteq J$ of the columns, the restricted master problem (RMP), and adds columns of negative reduced cost as a pricing problem finds them (Lübbecke and Desrosiers 2005, §2.1). Many integer programs from vehicle routing, crew scheduling and crew pairing are reformulated so that the master problem is a set-partitioning problem: every row (a customer, a flight leg, a task) must be covered by exactly one selected column (a route, a pairing, a schedule). The linear relaxation of such a master is solved by column generation, and an integer solution is then sought by branch-and-price, branch-and-bound with column generation at every node.

Branching in branch-and-price is not free. Fixing a master variable $\lambda_j$ to $0$ does not stop the pricing problem from regenerating the same column, and handling that complicates the pricing problem. The rule that avoids this for set partitioning goes back to Ryan and Foster (1981): branch on a pair of rows, requiring them to be covered either by the same column or by two different columns. Both requirements are constraints the pricing problem can respect directly. Lübbecke and Desrosiers call it "the most common scheme in conjunction with column generation" (§7.3, p. 1020) and state the proposition that makes it well defined as their Proposition 3.

Timeline:

1981: Ryan and Foster introduce the pair-of-rows branching rule for set partitioning in crew scheduling.
1998: the branch-and-price survey of Barnhart et al. (1998) presents the rule as the branching scheme for set-partitioning masters.
2005: Lübbecke and Desrosiers state it as Proposition 3 of their survey, attributing it to Ryan and Foster without proof.

Setting

Rows are indexed by $\{1, \dots, m\}$ and columns by a finite set $J'$ . A matrix $A = (a_{rj}) \in \{0,1\}^{m \times |J'|}$ has every entry equal to $0$ or $1$ ; column $j$ covers row $r$ when $a_{rj} = 1$ . The set-partitioning system of the RMP's linear relaxation is

A\lambda = \mathbf 1, \qquad \lambda \ge \mathbf 0, \qquad \lambda \in \mathbb R^{J'} .

A vector $\lambda$ is a basic feasible solution of this system when it satisfies all its constraints and, among the constraints active at $\lambda$ (the $m$ equality rows, and the constraints $\lambda_j \ge 0$ with $\lambda_j = 0$ ), there are $|J'|$ linearly independent ones. Equivalently, $\lambda$ is feasible and the columns of $A$ in the support of $\lambda$ are linearly independent. A solution is fractional when it is not a $0/1$ vector, $\lambda \notin \{0,1\}^{|J'|}$ .

For two rows $r, s$ the Ryan–Foster quantity is $\sum_{j \in J'} a_{rj} a_{sj} \lambda_j$ , written pairCover A lam r s in Lean: the total weight on the columns that cover both rows. For $r = s$ it is the row sum, equal to $1$ on every feasible $\lambda$ .

Formalization targets

Goal: Proposition 3 (p. 1020)

For every $0/1$ matrix $A$ and every fractional basic feasible solution $\lambda$ of $A\lambda = \mathbf 1$ , $\lambda \ge \mathbf 0$ ,

\exists\, r, s \in \{1, \dots, m\}: \qquad 0 < \sum_{j \in J'} a_{rj}\, a_{sj}\, \lambda_j < 1 .

The two rows are automatically distinct. The statement concerns every fractional basic solution, not only an optimal one, and no cost vector enters it.

Milestone: the branches keep every integer solution (§7.3, p. 1020)

For every $0/1$ solution $\lambda \in \{0,1\}^{|J'|}$ of $A\lambda = \mathbf 1$ and every pair of rows $r, s$ ,

\sum_{j \in J'} a_{rj}\, a_{sj}\, \lambda_j \in \{0, 1\} .

This is the paper's requirement that "integer solutions remain intact" (p. 1019), specialised to the two branches " $= 1$ " and " $= 0$ " of the paragraph after Proposition 3.

Significance

Proposition 3 is what makes Ryan–Foster branching a valid branching scheme in the sense of §7.3: the current fractional solution violates both branches for the chosen pair, so it is excluded from both children, while by the milestone every integer solution survives in one of them. The same pair-of-rows idea underlies branching in bin packing, graph colouring, vehicle routing and crew scheduling codes, where it is used because both branches translate into constraints on the pricing problem rather than on individual master variables.

The paper states the result and refers its proof to Ryan and Foster (1981); no machine-checked version of the proposition is known. This mission produces a formal statement tied to a standard, representation-aware definition of basic solutions (Bertsimas–Tsitsiklis Definition 2.9, already on the platform) and, once proved, a verified lemma that any formal development of branch-and-price for set partitioning can cite.

Difficulty

An argument that uses only feasibility and a fractional coordinate cannot work. Without basicness the claim is false: with one row and two identical columns, $A = [1\ 1]$ , the vector $\lambda = (\tfrac12, \tfrac12)$ is feasible and fractional, yet the only pair of rows is $r = s$ , whose quantity is $1$ . The difficulty is to turn basicness, a linear-algebra condition, into a combinatorial statement about which rows the fractional columns cover. A set-partitioning matrix need not have full row rank, so the familiar description of basic solutions through an invertible basis matrix is not available in general.

Formalization scope

Rows are Fin m and columns Fin n, so $J'$ is identified with $\{0, \dots, n-1\}$ . $A$ is a real matrix Matrix (Fin m) (Fin n) ℝ with the hypothesis IsZeroOneMatrix A (every entry $0$ or $1$ ); $\lambda$ is lam : Fin n → ℝ, since λ is a Lean keyword. Columns are $0/1$ vectors; the equivalent reading as subsets of the rows is only prose.
"Basic solution" is not defined in the paper. It is read as Bertsimas–Tsitsiklis Definition 2.9 for the standard-form constraint family: LinearOptimization.IsBasicFeasibleSolution (LinearOptimization.stdFormSystem A (fun _ => 1)) lam, from the platform definitions BasicSolution and ActiveConstraints. This definition needs no full-row-rank assumption, which a set-partitioning matrix need not satisfy, and it is not replaced by an ad hoc support condition.
Typo correction. The paper writes "i.e., $\lambda \notin \{0,1\}^m$ ". Since $\lambda$ has one coordinate per column, the statement reads it as $\lambda \notin \{0,1\}^{|J'|}$ : ¬ IsZeroOneVector lam.
The rows $r, s$ range over all of $\{1, \dots, m\}$ , including $r = s$ , as on the page; no distinctness is assumed or required.
"Fractional basic solution" is any such solution, not the RMP optimum; no costs or optimality hypothesis enter.
The milestone reads the paragraph after Proposition 3, together with the validity requirement "integer solutions remain intact" (p. 1019), as the dichotomy for all $0/1$ solutions of $A\lambda = \mathbf 1$ . The sentence about transferring the branching information to the pricing problem is not formalized.
Edge cases: for $m = 0$ basicness forces $\lambda = 0$ , and for $n = 0$ the vector is empty; in both cases no fractional basic solution exists and the goal is vacuous, as on the page.
A trivializing formalization is ruled out: dropping basicness makes the goal false (the $[1\ 1]$ example above), dropping the $0/1$ hypothesis on $A$ changes the meaning of the quantity, and replacing "fractional basic" by an unsatisfiable hypothesis would make it empty; the hypotheses are satisfied, for instance, by three rows, the columns $\{1,2\}, \{2,3\}, \{1,3\}$ and $\lambda = (\tfrac12, \tfrac12, \tfrac12)$ .

A complete development needs linear-algebra facts about basic solutions of standard-form systems without a rank assumption (support columns linearly independent), which are reusable beyond this mission. Contributions welcome: that characterization as a lemma, and proofs of the milestone and of the goal.

Selected references

M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
D. M. Ryan and B. A. Foster, An integer programming approach to scheduling, in A. Wren (ed.), Computer Scheduling of Public Transport, North-Holland, 1981, pp. 269–280.
C. Barnhart, E. L. Johnson, G. L. Nemhauser, M. W. P. Savelsbergh and P. H. Vance, Branch-and-Price: Column Generation for Solving Huge Integer Programs, Operations Research 46(3):316–329, 1998. https://doi.org/10.1287/opre.46.3.316
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Definition 2.9.

5 thms4 active usersReviewed

Completed

Analysis Dynamical Systems Functional Analysis+1·Captain: mikedeng1

Ordinary Differential Equations and Dynamical Systems IV: Regular Sturm–Liouville ProblemsTextbook

Why regular Sturm–Liouville problems

Separation of variables reduces the heat equation, the wave equation and the Schrödinger equation on an interval to an eigenvalue problem for a second-order ordinary differential operator with boundary conditions at both ends. Whether the method works depends on one fact: the eigenfunctions of that operator must be complete, so that every reasonable initial profile can be expanded in them. Chapter 5 of Gerald Teschl's Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012) proves this for regular Sturm–Liouville problems. It does so without Lebesgue integration or Hilbert-space completeness: it works in the space of continuous functions with a weighted scalar product, and it develops the necessary spectral theory of compact symmetric operators from scratch.

A short history. Sturm and Liouville (1836–1837) studied the zeros and the eigenvalues of such equations and the expansion of functions in eigenfunctions. Hilbert and Schmidt (1904–1907) put the expansion on a rigorous footing through their theory of integral equations with symmetric kernels, from which the abstract spectral theorem for compact symmetric operators emerged.

Setting

Let $a < b$ and let $p, q, r$ be real functions on $[a,b]$ with

r, q \in C([a,b], \mathbb{R}), \qquad p \in C^1([a,b], \mathbb{R}), \qquad p(x) > 0,\ r(x) > 0 \ \ (x \in [a,b]). \qquad (5.45)

These regularity assumptions hold throughout. The Sturm–Liouville operator is

L f = \frac{1}{r}\Bigl( -(p f')' + q f \Bigr),

acting on the domain

D(L) = \{ f \in C^2([a,b], \mathbb{C}) : \cos(\alpha) f(a) - \sin(\alpha) p(a) f'(a) = 0,\ \ \cos(\beta) f(b) - \sin(\beta) p(b) f'(b) = 0 \}

for fixed real $\alpha, \beta$ (the separated boundary conditions; $\alpha = 0$ is Dirichlet, $\alpha = \pi/2$ Neumann). The underlying space is $H_0 = C([a,b], \mathbb{C})$ with the weighted scalar product

\langle f, g \rangle = \int_a^b f(x)^* g(x)\, r(x)\, dx

and norm $\|f\| = \sqrt{\langle f, f\rangle}$ . $H_0$ is an inner product space but it is not complete. A number $z \in \mathbb{C}$ is an eigenvalue of $L$ if $L f = z f$ for some $f \in D(L)$ that does not vanish identically; $f$ is an eigenfunction. An orthonormal basis of $H_0$ is an orthonormal sequence $(u_n)$ such that $\|f - \sum_{n<N} \langle u_n, f\rangle u_n\| \to 0$ for every $f \in H_0$ .

For the abstract part, $H_0$ is any complex inner product space (again not assumed complete). A linear operator $A$ on a dense subspace is symmetric if $\langle g, Af\rangle = \langle Ag, f\rangle$ ; an everywhere defined $A$ is compact if $(A f_n)$ has a convergent subsequence in $H_0$ whenever $(f_n)$ is bounded.

For $z \in \mathbb{C}$ let $u_a(z,\cdot)$ , $u_b(z,\cdot)$ solve $L u = z u$ with $u_a(z,a) = \sin\alpha$ , $p(a)u_a'(z,a) = \cos\alpha$ , $u_b(z,b) = \sin\beta$ , $p(b)u_b'(z,b) = \cos\beta$ . Their Wronskian is $W(z) = u_b p u_a' - p u_b' u_a$ , which does not depend on the point where it is evaluated. When $W(z) \neq 0$ , the resolvent $R_L(z)$ is the integral operator with the Green function $G(z,x,t) = W(z)^{-1} u_b(z,\max(x,t))\, u_a(z,\min(x,t))$ and weight $r$ .

Formalization targets

Goal: eigenfunction expansion (Theorem 5.11)

There are real numbers $E_n$ and real-valued eigenfunctions $u_n \in D(L)$ , $L u_n = E_n u_n$ , such that:

the $E_n$ are pairwise distinct and are all the eigenvalues of $L$ , and every eigenfunction for $E_n$ is a multiple of $u_n$ (the eigenvalues are simple);
$|E_n| \to \infty$ (the eigenvalues accumulate only at $\infty$ );
$\langle u_m, u_n \rangle = \delta_{mn}$ , and for every $f \in H_0$

f = \sum_{n=0}^{\infty} \langle u_n, f \rangle\, u_n \quad \text{in } H_0, \qquad (5.70)

for $f \in D(L)$ the series (5.70) converges uniformly on $[a,b]$ .

Milestones

Theorem 5.4. Eigenvalues of a symmetric operator are real, and eigenvectors for different eigenvalues are orthogonal.
Theorem 5.5. A compact symmetric operator on a nonzero inner product space has an eigenvalue $\alpha_0$ with $|\alpha_0| = \|A\| = \sup_{\|f\|=1}\|Af\|$ .
Theorem 5.6 (spectral theorem). A compact symmetric operator has real eigenvalues $\alpha_j$ with orthonormal eigenvectors $u_j$ , infinitely many when $H_0$ is infinite dimensional and then $\alpha_j \to 0$ , and $f = \sum_j \langle u_j, f\rangle u_j$ for every $f \in \operatorname{Ran}(A)$ ; if $\operatorname{Ran}(A)$ is dense the $u_j$ are an orthonormal basis.
Lemma 5.9. $W(z)$ is an entire function of $z$ whose zeros are exactly the eigenvalues of $L$ .
Lemma 5.10. For $W(z) \ne 0$ , $R_L(z)$ is compact on $H_0$ , and symmetric for real $z$ .
Lemma 5.12 (Rayleigh–Ritz). The eigenvalues can be ordered $E_0 < E_1 < \cdots$ ; $E_0 = \min \langle f, Lf\rangle = \min Q(f)$ over normalized $f \in D(L)$ , attained exactly at the eigenfunctions for $E_0$ ; and $\min_{[a,b]} q \le E_0$ when $0 \le \alpha \le \pi/2 \le \beta \le \pi$ . Here $Q$ is the quadratic form $\int_a^b (p |f'|^2 + q |f|^2)\,dx$ plus the boundary terms $\cot(\alpha)|f(a)|^2 - \cot(\beta)|f(b)|^2$ (dropped when the angle is $0$ ).

Significance

Theorem 5.11 is the statement that makes eigenfunction expansions legitimate: Fourier sine and cosine series are its special case $p = r = 1$ , $q = 0$ , and it covers any positive weight and any smooth positive stiffness with separated boundary conditions. Solutions of the heat and wave equations on an interval with variable coefficients are built from it. The uniform convergence for $f \in D(L)$ is the version needed to differentiate or evaluate such series pointwise. Lemma 5.12 provides the variational characterisation of the lowest eigenvalue, the starting point for comparison theorems and eigenvalue estimates.

On the formal side, Mathlib has the spectral theorem for self-adjoint operators on finite-dimensional spaces, compact operators on normed spaces, and $L^2$ spaces. It has no Sturm–Liouville theory, no Green functions for boundary value problems, and no spectral theorem for compact symmetric operators on incomplete inner product spaces. The platform has finite-dimensional Rayleigh-quotient results and compactness of $L^2$ convolution operators, but nothing on this setting. The results here are classical and proved; what is missing is a machine-checked proof in the book's elementary setting of continuous functions.

Difficulty

The operator $L$ is unbounded on $H_0$ (Problem 5.16), so the obvious first idea, applying a spectral theorem for compact or bounded symmetric operators to $L$ itself, does not work. Completeness of the eigenfunctions is also subtle because $H_0$ is not complete. Hilbert-space arguments that produce limits in a completion, or that go through $L^2$ , do not by themselves give an expansion of a continuous function in continuous eigenfunctions with convergence in $H_0$ , still less uniform convergence. Simplicity of the eigenvalues depends on the separated boundary conditions and fails for periodic ones. On the formal side, one needs analytic dependence of solutions of a linear ODE on a complex parameter, one-sided derivatives at the endpoints, and interval integrals of piecewise-defined kernels.

Formalization scope

Spaces. The abstract results use a type with [NormedAddCommGroup E] [InnerProductSpace ℂ E] and no CompleteSpace. Symmetry on a dense domain is IsSymmetricOp; for everywhere defined operators it is Mathlib's LinearMap.IsSymmetric. Compactness is IsCompactOp: subsequences converge in $H_0$ itself. $H_0 = C([a,b],\mathbb{C})$ is represented by functions $\mathbb{R} \to \mathbb{C}$ continuous on Set.Icc a b, with SLInner the weighted scalar product (5.52) as an interval integral. It is not $L^2$ and not a HilbertBasis.
Operator and domain. SLOp, SLDomain, IsSLEigenfunction implement (5.53)–(5.55) with derivWithin on Set.Icc a b (one-sided at the endpoints) and ContDiffOn ℝ 2. RegularSL is (5.45), including $a < b$ . $\alpha, \beta$ are arbitrary reals.
Quantifier readings. "Countable, discrete, accumulating only at $\infty$ " is an injective sequence $E_n$ exhausting the eigenvalues with $|E_n| \to \infty$ . "Simple" is: every eigenfunction for $E_n$ equals $c\,u_n$ on $[a,b]$ . "Can be chosen real-valued" is an existential choice of $u_n : \mathbb{R} \to \mathbb{R}$ . $\|A\|$ in Theorem 5.5 is expressed by IsLUB of $\{\|Af\| : \|f\|=1\}$ , and Theorem 5.5 assumes $H_0 \neq \{0\}$ . In Theorem 5.6, $N \in \mathbb{N}_0 \cup \{\infty\}$ is ℕ∞: $N = \infty$ in infinite dimension and $N = \dim H_0$ otherwise. The minima of Lemma 5.12 are IsLeast (attained), and "equality iff $f = u_0$ " reads as "iff $f$ is an eigenfunction for $E_0$ ", i.e. $f = c\,u_0$ with $|c| = 1$ . $\min q \le E_0$ is $\exists x \in [a,b],\ q(x) \le E_0$ . Norm convergence is $\operatorname{Re}\langle f - S_N, f - S_N\rangle \to 0$ .
Ruling out trivial readings. The resolvent is only considered with $W(z) \ne 0$ (Lean's $0^{-1} = 0$ would make it the zero operator). Scalar products are only applied to functions continuous on $[a,b]$ , so no integral takes a junk value. Eigenfunctions must be nonzero on $[a,b]$ . The expansion must hold in the weighted norm for every continuous $f$ , which an orthonormal family that is merely orthonormal would not satisfy.

A complete development needs linear ODEs with a complex parameter and their analytic dependence on it, Green functions, an Arzelà–Ascoli argument in $C([a,b])$ , and the spectral theorem for compact symmetric operators on an inner product space. The definitions RegularSL, SLOp, SLDomain, SLInner and SLWronskian are reusable for the oscillation and comparison theory (Theorems 5.17–5.25) in the rest of the chapter. Contributions connecting IsCompactOp to Mathlib's IsCompactOperator on the completion are welcome.

Selected references

G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, American Mathematical Society, 2012. Author's preliminary version: https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf ; published version: https://doi.org/10.1090/gsm/140
J. C. F. Sturm, Mémoire sur les équations différentielles linéaires du second ordre, Journal de Mathématiques Pures et Appliquées 1 (1836), 106–186. http://www.numdam.org/item/JMPA_1836_1_1__106_0/
J. Liouville, Mémoire sur le développement des fonctions ou parties de fonctions en séries dont les divers termes sont assujettis à satisfaire à une même équation différentielle du second ordre, Journal de Mathématiques Pures et Appliquées 1 (1836), 253–265. http://www.numdam.org/item/JMPA_1836_1_1__253_0/
E. Schmidt, Zur Theorie der linearen und nichtlinearen Integralgleichungen. I, Mathematische Annalen 63 (1907), 433–476. https://doi.org/10.1007/BF01449770

17 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Probability+1·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems IV: The Optimal Randomized Two-Server Ratio 1652/1069 on the 3-4-5 TriangleResearch Paper

Motivation

The $k$ -server problem is a basic model of on-line decision making. $k$ mobile servers move in a metric space, requests for points arrive one at a time, and each request has to be covered by a server before the next one arrives. The cost is the total distance the servers move. The problem includes paging, caching and disk-head scheduling as special cases (Manasse, McGeoch, Sleator 1990). An on-line algorithm is judged by its competitive factor: how much its cost can exceed that of an off-line algorithm that knows the whole request sequence in advance.

For randomized algorithms against an oblivious adversary (one that fixes the whole request sequence before the algorithm flips any coins), the best-understood case is paging, which is the $k$ -server problem on a uniform metric space. There the optimal factor is the harmonic number $H_k=\sum_{i=1}^k 1/i$ . Fiat et al. proved the lower bound (1991) and McGeoch and Sleator the matching upper bound (1991). Karlin, Manasse, McGeoch and Owicki (Algorithmica 11, 1994, §5) asked whether $H_k$ -competitive algorithms also exist when the metric space is not uniform. They answered no, already for two servers on three points: on certain triangles the optimal randomized factor is strictly larger than $H_2 = 3/2$ . This mission formalizes their Theorem 13, which gives the exact optimal factor on the triangle with edge lengths 3, 4 and 5.

Timeline:

1990: Manasse, McGeoch and Sleator introduce the $k$ -server problem; $k$ is the deterministic optimum for $k=2$ .
1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the $H_k$ lower bound for randomized paging. McGeoch and Sleator give an $H_k$ -competitive paging algorithm.
1994: Karlin, Manasse, McGeoch and Owicki determine the optimal randomized two-server factors on the isosceles triangles $1$ - $d$ - $d$ (Theorem 12) and on the 3-4-5 triangle (Theorem 13, the ratio $1652/1069$ ). Both exceed $3/2$ .

Setting

Let $M$ be a metric space with exactly three points $a, b, c$ , where $d(a,b)=3$ , $d(a,c)=5$ and $d(b,c)=4$ . A configuration $C$ gives the positions of two labelled servers in $M$ . A request sequence $\sigma$ is a finite list of points of $M$ .

A deterministic on-line algorithm assigns to each prefix of a request sequence a configuration, in which the last request is covered. Its configuration after a prefix therefore cannot depend on later requests. Its initial configuration is the one it assigns to the empty prefix, and its cost $C_A(\sigma)$ on $\sigma$ is the total distance its servers move while serving $\sigma$ request by request.

The optimal off-line cost $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the infimum, over all schedules that start at $C_0$ and cover each request of $\sigma$ in turn, of the total distance moved.

A randomized on-line algorithm $A$ is a probability distribution over deterministic on-line algorithms, all starting at $C_0$ . The cost on each fixed $\sigma$ is required to be measurable in the random choice, and $\mathbf{E}C_A(\sigma)$ is the expected cost. $A$ is $\rho$ -competitive against an oblivious adversary if there is a constant $a$ such that for every request sequence $\sigma$ ,

\mathbf{E}C_A(\sigma) \le \rho\cdot C_{opt}(\sigma) + a .

These are the definitions of p. 543 of the paper. They are the platform's published KServer_model and KServer_randomized, which this mission reuses unchanged: KServer.RandomizedAlgorithm 2 M and A.IsCompetitiveFrom C₀ ρ.

Formalization targets

Goal: Theorem 13

For every initial configuration $C_0$ of the two servers,

\Big(\forall A,\ \forall \rho,\ A \text{ is } \rho\text{-competitive from } C_0 \Rightarrow \rho \ge \tfrac{1652}{1069}\Big)\ \wedge\ \Big(\exists A,\ A \text{ is } \tfrac{1652}{1069}\text{-competitive from } C_0\Big).

The first claim is quantified over all randomized algorithms, so it also covers deterministic ones (point masses). The second claim asks for one algorithm. Together they say that $1652/1069 \approx 1.545$ is the exact optimal randomized factor on this triangle.

Milestones

The phase LP lower bound (p. 568). Twelve linear constraints in nine probabilities $\pi_1,\dots,\pi_9$ , three potentials $\Phi_{ab},\Phi_{ac},\Phi_{bc}$ and a ratio $\alpha$ , one constraint for each possible phase of the request sequence, of the form

\text{A's cost} \le \alpha\cdot(\text{opt's cost}) + \Phi_{\text{initial}} - \Phi_{\text{final}}.

Every real solution has $\alpha \ge 1652/1069$ . 2. The LP attainment (p. 568). The paper's printed probabilities lie in $[0,1]$ , and with suitable potentials they satisfy all twelve constraints at $\alpha = 1652/1069$ . 3. Theorem 13, first claim: the lower bound for every randomized algorithm. 4. Theorem 13, second claim: a $1652/1069$ -competitive randomized algorithm exists.

Significance

The result. Theorem 13 shows that the $H_k$ behaviour of randomized paging does not carry over to general metric spaces. Two servers on a three-point space already force a factor above $3/2$ . The value is exact, which makes this triangle a test case for any general theory of randomized $k$ -server algorithms on small metric spaces. With Theorem 12 (the isosceles triangles, a companion mission of this series), it is one of the few non-uniform metric spaces with a known optimal randomized factor.

Formalizing it. The result has been proved since 1994. To our knowledge there is no machine-checked proof. The paper derives both bounds from two framework theorems for phase-based algorithms: Theorem 3 (an LP lower bound for phase-based algorithms bounds every algorithm) and Theorem 2 (a lazy phase-based algorithm with LP bound $\alpha$ is $\alpha$ -competitive). The phase tables themselves (which phases can occur and what they cost) are stated without detailed proof. A formal proof has to supply both framework arguments for this space and verify the phase tables, as well as the finite linear algebra of milestones 1 and 2. The milestones isolate the exact-arithmetic core so that it can be closed independently of the probabilistic part.

Difficulty

The two LP milestones are finite exact-arithmetic facts. The hard part is linking them to Theorem 13.

For the lower bound, an algorithm need not be phase-based at all. Its probabilities may depend on the whole history, not only on the current phase, and it may leave the configuration of the off-line optimum at the end of a phase. The obvious attempt is to fix one hard request sequence and compare costs, but that cannot work: randomization defeats any single sequence. The reduction from arbitrary algorithms to phase-based ones (the paper's Theorem 3) is the substantive step.

For the upper bound, the printed probabilities describe the algorithm's marginal position after each prefix of a phase. They have to be realized as a single probability distribution over deterministic on-line algorithms that is lazy (it moves only to serve a request) and whose expected cost per phase equals the table's entry. On top of this, the LP accounting has to be turned into a bound on arbitrary request sequences, including partial phases and a start away from the optimum's configuration.

Formalization scope

Model. The platform definitions KServer_model and KServer_randomized are used unchanged. Servers are labelled (Config 2 M = Fin 2 → M). A deterministic algorithm is a function of the request prefix, which makes it on-line by construction. A randomized algorithm is a mixed strategy with a probability measure and a measurability field, and its expected cost is the lower Lebesgue integral of the nonnegative cost. The off-line optimum is a real infimum over schedules from $C_0$ ; the set is nonempty and bounded below by $0$ . Competitiveness allows any real additive constant.
The triangle is given by hypotheses on an arbitrary metric space: every point equals $a$ , $b$ or $c$ , and $d(a,b)=3$ , $d(a,c)=5$ , $d(b,c)=4$ . These hypotheses are satisfiable ( $3+4\ge5$ ) and force three distinct points.
Initial configuration. Both claims are stated for every initial configuration $C_0$ , including both servers on one point. The paper does not fix the start; the additive constant absorbs it.
LP milestones. The thirteen LP variables are free reals, with no box $0\le\pi_i\le 1$ , exactly as the paper permits. This makes milestone 1 stronger than the boxed version; the minimum is the same either way. The twelve constraints are written out one per hypothesis, in the table's order, with the potential difference $\Phi_{\text{initial}} - \Phi_{\text{final}}$ on the right. In milestone 2 the potentials are existentially quantified, since the paper names none.
Not stated. The paper's Theorems 2 and 3 (the phase framework) and the phase tables are not separate milestones. Milestone 1 feeds the first claim through Theorem 3, and milestone 2 feeds the second claim through Theorem 2. Contributions formalizing phase-based algorithms, laziness and the LP-bound reduction for finite metric spaces would be reusable for Theorem 12 and Theorem 14 of the same paper.
Ruled out. The lower bound is not restricted to deterministic or to phase-based algorithms, and it is not stated as "one sequence defeats every algorithm". The constant is exactly $1652/1069$ , not an approximation, and the attainment claim is not weakened to "for some initial configuration".

Selected references

A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, Journal of Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, Journal of Algorithms 12 (1991) 685–699. https://doi.org/10.1016/0196-6774(91)90041-V
L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6 (1991) 816–825. https://doi.org/10.1007/BF01759073

7 thms4 active usersReviewed

Completed

Analysis Dynamical Systems Linear algebra·Captain: mikedeng1

Ordinary Differential Equations and Dynamical Systems II: Linear Systems and Floquet TheoryTextbook

Motivation

Linear systems of ordinary differential equations $\dot x = A(t)x$ are the first case of the general theory in which solutions can be described structurally rather than merely shown to exist. They arise directly (circuits, mechanical vibrations, Hill's equation for the stability of periodic motions, the Mathieu equation for parametric resonance) and indirectly, as the linearization of a nonlinear system along an equilibrium or a periodic orbit. In the second role they decide stability: the linearized stability theorems of later chapters, the Poincaré map of a periodic orbit and the stable-manifold theory all reduce questions about nonlinear flows to questions about linear systems with constant or periodic coefficients.

For periodic coefficients the central structural result is due to Gaston Floquet (Sur les équations différentielles linéaires à coefficients périodiques, Annales scientifiques de l'École Normale Supérieure 12 (1883), 47–88, doi:10.24033/asens.220), preceded by G. W. Hill's 1877 work on the lunar perigee, which studied the same equation in the scalar second-order case. Liouville's formula for the Wronski determinant goes back to Abel (1829) and Liouville (1838). This mission follows Chapter 3 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012), in the author's preliminary version.

Setting

Fix $n \in \mathbb{N}$ , an interval $I \subseteq \mathbb{R}$ and a continuous matrix function $A : I \to \mathbb{R}^{n\times n}$ . A solution of the linear first-order system

\dot x(t) = A(t)\,x(t) \qquad (3.79)

on $I$ is a function $x$ with values in $\mathbb{R}^n$ that at every $t \in I$ has derivative $A(t)x(t)$ (one-sided at an endpoint of $I$ ). In Lean this is TeschlODE.Linear.IsSolution A I x.

The principal matrix solution $\Pi(t,t_0)$ is, for each $t_0 \in I$ , the matrix function that solves the matrix initial value problem

\frac{d}{dt}\Pi(t,t_0) = A(t)\,\Pi(t,t_0), \qquad \Pi(t_0,t_0) = \mathbb{I}. \qquad (3.83)

Its columns are the solutions of (3.79) starting at the canonical basis vectors, and every solution is $x(t) = \Pi(t,t_0)x(t_0)$ . In Lean the property is TeschlODE.Linear.IsPrincipalMatrixSolution A I Φ (the Lean name of $\Pi$ is Φ). The Wronski determinant of $n$ solutions $\varphi_1,\dots,\varphi_n$ is $W(t) = \det(\varphi_1(t),\dots,\varphi_n(t))$ .

A system is periodic if $I = \mathbb{R}$ and $A(t+T) = A(t)$ for all $t$ , for some $T > 0$ (3.117). Its monodromy matrix is $M(t_0) = \Pi(t_0+T, t_0)$ (3.119). A logarithm of a square matrix $M$ is any matrix $B$ with $\exp(B) = M$ (3.200), where $\exp$ is the matrix exponential.

Formalization targets

Goal: Floquet's theorem (Theorem 3.15)

Let $A \in C(\mathbb{R}, \mathbb{R}^{n\times n})$ be $T$ -periodic with $T > 0$ and $\Pi$ its principal matrix solution. For every $t_0 \in \mathbb{R}$ there exist $Q(t_0) \in \mathbb{C}^{n\times n}$ and $P(\cdot,t_0) : \mathbb{R} \to \mathbb{C}^{n\times n}$ with

\Pi(t,t_0) = P(t,t_0)\,\exp\big((t-t_0)\,Q(t_0)\big), \qquad P(t+T,t_0) = P(t,t_0), \qquad P(t_0,t_0) = \mathbb{I}.

Milestones

In attack order:

Theorem 3.9 — for continuous $A$ on an interval $I$ the initial value problem $\dot x = A(t)x$ , $x(t_0) = x_0$ has a unique solution, defined on all of $I$ .
Theorem 3.10 — the solutions form an $n$ -dimensional vector space, and a principal matrix solution exists with $x(t) = \Pi(t,t_0)x_0$ .
Lemma 3.14 — for $T$ -periodic $A$ , $\Pi(t+T, t_0+T) = \Pi(t,t_0)$ .
Lemma 3.11 (Liouville's formula) — $W(t) = W(t_0)\exp\big(\int_{t_0}^t \operatorname{tr} A(s)\,ds\big)$ .
Lemma 3.34 — a complex matrix has a logarithm iff its determinant is nonzero; a real matrix whose real eigenvalues are all positive has a real logarithm; the square of an invertible real matrix has a real logarithm.
Theorem 3.12 (variation of constants) — the solution of $\dot x = A(t)x + g(t)$ , $x(t_0) = x_0$ , is $x(t) = \Pi(t,t_0)x_0 + \int_{t_0}^t \Pi(t,s)g(s)\,ds$ .

Milestone 6 is not needed for the goal; it completes the linear theory of Section 3.4 on the same definitions and is the input to the perturbation results of Section 3.7.

Significance

Floquet's theorem reduces a periodic linear system to one with constant coefficients by a periodic change of variables. Its consequences in the book are the real version with doubled period (Corollary 3.16), the stability criterion in terms of Floquet multipliers (the eigenvalues of $M(t_0)$ , Corollary 3.17), the reduction $y = P^{-1}x$ to $\dot y = Q y$ (Corollary 3.18), and the stability analysis of Hill's equation. Later in the book, the stability of a periodic orbit of a nonlinear system is read off from the Floquet multipliers of its linearization, via the Poincaré map.

All results of this mission have been proved for more than a century. What the mission adds is a machine-checked development: Mathlib has the matrix exponential (NormedSpace.exp, with Matrix.exp_add_of_commute), Picard–Lindelöf and Gronwall-type uniqueness for ODEs, but no principal matrix solution, no Liouville formula, no matrix logarithm and no Floquet theory. The two platform nodes named after Floquet's and Liouville's theorems are retired placeholders whose statement is True; no faithful formalization exists on the platform.

Difficulty

The obvious guess for the solution, $\exp\big(\int_{t_0}^t A(s)\,ds\big)x_0$ , is wrong as soon as the values $A(t)$ do not commute, so neither Floquet's theorem nor the variation-of-constants formula can be obtained from the constant-coefficient theory by substitution. Floquet's theorem as stated is equivalent to the existence of a logarithm of the monodromy matrix: once $M(t_0) = \exp(TQ)$ is available, the periodicity of $P$ follows from Lemma 3.14. The existence of a matrix logarithm for every invertible complex matrix is the main missing piece of infrastructure; the logarithm is not unique and not continuous in the matrix, and a real invertible matrix need not have a real logarithm (a negative eigenvalue with a single Jordan block prevents it), which is why $Q(t_0)$ is complex. Liouville's formula, which gives $\det M(t_0) = \exp\big(\int_0^T \operatorname{tr} A\big) \neq 0$ , needs the derivative of a determinant along a matrix solution.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ; $A(t)x$ is Matrix.mulVec. The goal and Lemma 3.34 use Matrix (Fin n) (Fin n) ℂ for $P$ , $Q$ and the complex logarithm; $\Pi(t,t_0)$ is compared with $P\exp(\cdot)$ after coercing its entries to $\mathbb{C}$ .
An interval is a set $I$ with Set.OrdConnected I; continuity is ContinuousOn A I. Derivatives are HasDerivWithinAt … I t at every $t \in I$ (one-sided at endpoints in $I$ ); the matrix derivative in (3.83) is taken entrywise. In Section 3.6 (Lemma 3.14 and the goal) $I = \mathbb{R}$ and $A$ is Continuous.
The principal matrix solution enters as a hypothesis IsPrincipalMatrixSolution A Set.univ Φ. Theorem 3.10 shows such a $\Phi$ exists and Theorem 3.9 shows it is unique on $I\times I$ , so this hypothesis names the principal matrix solution, not an arbitrary function.
Periodicity is 0 < T and ∀ t, A (t + T) = A t. The periodicity of $P$ is required with the same $T$ and for all $t$ , together with $P(t_0,t_0) = \mathbb{I}$ . Without the periodicity of $P$ the goal would be trivial ( $Q = 0$ , $P = \Pi$ ); with it, the goal carries the full content of the theorem.
The matrix exponential is Mathlib's NormedSpace.exp. "Logarithm" means any $B$ with NormedSpace.exp B = M; no branch is fixed. In the third claim of Lemma 3.34 the hypothesis $\det A \ne 0$ is explicit: the book states it in the paragraph containing the lemma, and without it the claim fails at $A = 0$ .
"The solutions form an $n$ -dimensional vector space" is expressed through restrictions to $I$ : closure under linear combinations, $n$ solutions linearly independent on $I$ , and every solution a combination of them on $I$ .
Needed infrastructure, reusable beyond this mission: existence and uniqueness for linear systems on arbitrary intervals, the principal matrix solution and its cocycle property $\Pi(t,t_1)\Pi(t_1,t_0) = \Pi(t,t_0)$ , the derivative of $\det$ along a matrix solution, and the matrix logarithm (via the Jordan form or via the holomorphic functional calculus). Contributions of any of these as standalone lemmas are welcome.

Selected references

G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, American Mathematical Society, 2012; author's preliminary version, Chapter 3. https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf (published version: doi:10.1090/gsm/140).
G. Floquet, Sur les équations différentielles linéaires à coefficients périodiques, Annales scientifiques de l'École Normale Supérieure 12 (1883), 47–88. doi:10.24033/asens.220
W. J. Culver, On the existence and uniqueness of the real logarithm of a matrix, Proceedings of the AMS 17 (1966), 1146–1151. doi:10.1090/S0002-9939-1966-0202740-6

9 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Probability+1·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems I: Optimal Competitiveness of Randomized Block Snoopy CachingResearch Paper

Motivation

In a shared-memory multiprocessor, each processor keeps copies of memory blocks in its own cache, and all caches listen ("snoop") on a common bus. Every bus cycle spent keeping these copies consistent is a cycle not available for useful work, so the protocol that decides when a block is shared by several caches and when it is private to one cache directly controls bus traffic. The decision has to be made on-line, without knowing which processor will touch the block next.

Karlin, Manasse, Rudolph and Sleator (Algorithmica 1988) introduced competitive analysis for this problem and gave a deterministic algorithm with competitive ratio $2$ , which is optimal among deterministic algorithms. Karlin, Manasse, McGeoch and Owicki (Algorithmica 1994) showed that randomization helps: against an oblivious adversary the optimal ratio for block snoopy caching is $e_p/(e_p-1)$ , where $p$ is the cost of transferring a block. The same paper develops a general method for "nonuniform" problems, in which some state transitions are much more expensive than others, and the snoopy-caching result is its first application.

Setting

Fix $n$ processors and one memory block $B$ holding $p-1$ variables; transferring $B$ over the bus costs $p$ bus cycles. The block is in one of $n+1$ states: shared between all caches, or private to the cache of processor $i$ .

A request is a read $\mathrm{R}_i$ or a write $\mathrm{W}_i$ by processor $i$ . Moving from a private state to any other state costs $p$ ; moving from the shared state is free. A read $\mathrm{R}_i$ costs $0$ if $B$ is shared or private to $i$ and $+\infty$ otherwise. A write $\mathrm{W}_i$ costs $0$ if $B$ is private to $i$ , $1$ if $B$ is shared (one bus cycle broadcasts the new value), and $+\infty$ otherwise.

Before request $j$ the system is in state $s_{j-1}$ . A read is a look-ahead-one request: the algorithm may change state at the moment of the request, after seeing it. A write is a look-ahead-zero request: it is served in whatever state the system is in. After either kind, the algorithm may move again. The cost of a request is the cost of the move to the serving state, plus the task cost there, plus the cost of the move afterwards. Every write is preceded by a read to the same block, so in an admissible sequence each write $\mathrm{W}_i$ directly follows $\mathrm{R}_i$ or $\mathrm{W}_i$ .

The off-line optimum $C_{opt}(s_0,\sigma)$ is the least total cost of serving $\sigma$ from the initial state $s_0$ with full knowledge of $\sigma$ . A randomized on-line algorithm $A$ is a probability distribution over deterministic on-line algorithms; its expected cost on $\sigma$ is $\mathbf{E}C_A(\sigma)$ . $A$ is $c$ -competitive against an oblivious adversary from $s_0$ if there is a constant $a$ with

\mathbf{E}C_A(\sigma)\le c\cdot C_{opt}(s_0,\sigma)+a

for every admissible $\sigma$ . Put

e_p=\left(1+\frac1p\right)^p .

Formalization targets

Goal: Theorem 4

For $n\ge 2$ , $p\ge 1$ and every initial state $s_0$ :

\Big(\forall A\ \forall c:\ A \text{ is } c\text{-competitive from } s_0 \Rightarrow c\ge \tfrac{e_p}{e_p-1}\Big)\ \wedge\ \exists A:\ A \text{ is } \tfrac{e_p}{e_p-1}\text{-competitive from } s_0 .

The two conjuncts are milestones of their own: the lower bound (Theorem 4, first claim) and attainment (Theorem 4, second claim).

The phase linear program (§3.2, pp. 552–554)

For $p\ge1$ , real $\pi_1,\dots,\pi_{p+1}$ with $\pi_{p+1}=1$ , and real $\alpha$ with

\pi_{k+1}p+\sum_{i=1}^{k}(1-\pi_i)\le\alpha k\qquad(k=0,\dots,p),

one has $\alpha\ge e_p/(e_p-1)$ . Conversely, at $\alpha=e_p/(e_p-1)$ the choice $\pi_k=(\alpha-1)\big(((p+1)/p)^{k-1}-1\big)$ satisfies $\pi_{p+1}=1$ , $0\le\pi_1\le\dots\le\pi_{p+1}$ , and makes every constraint an equality.

Significance

The theorem settles the randomized competitive ratio of block snoopy caching exactly: $2$ at $p=1$ , $9/5$ at $p=2$ , decreasing to $e/(e-1)\approx1.582$ as $p\to\infty$ , against the deterministic optimum $2$ . The same ratio $e/(e-1)$ is the randomized optimum for the continuous ski-rental and spin-block problems treated later in the paper, and the snoopy-caching case is its discrete counterpart with ratio $e_p/(e_p-1)$ . The phase-LP method used here recurs in the paper's two-server results.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of the snoopy-caching task system with look-ahead-zero requests, of randomized algorithms against an oblivious adversary with infinite task costs allowed, and of the off-line optimum, together with the exact optimal ratio. The platform's fractional ski-rental result (PrimalDualOnline.SkiRental.fractional_competitive) proves an $e_B/(e_B-1)$ bound for a different model: one deterministic fractional algorithm, with no lower bound over randomized algorithms. It is related work, not a special case.

Difficulty

The linear program is elementary. The gap is between the LP and the algorithms. The paper's lower bound reduces arbitrary randomized algorithms to phase-based ones, whose state distribution at the end of each phase agrees with the optimal algorithm's known state, and whose behaviour inside a phase depends only on the number of writes so far. This reduction (Theorems 1 and 3 of the paper, pp. 545–549) is where the argument is not routine. An algorithm may keep the block private to a processor that is not the active one, may randomize over histories rather than over phase lengths, and the off-line optimum is not a sum of per-phase costs at the ends of the sequence. The obvious approach, bounding a single adversarial phase, does not suffice, because an algorithm may pay more in one phase and recover it in the next; the additive constant $a$ and the infinite horizon have to be handled. For attainment, the mixture of threshold algorithms must be written as a genuine distribution over on-line algorithms, with the initial phase from a private state absorbed into the additive constant.

Formalization scope

Everything lives in the namespace NonuniformCompetitive.Snoopy. States are Option (Fin n) (none = shared). Costs are in ℝ≥0∞; $+\infty$ is a genuine outcome, so an algorithm that ever pays $+\infty$ with positive probability on an admissible sequence is not competitive. A deterministic on-line algorithm is a pair of functions of the request prefix (the state at the moment of the last request, and the state after it), with the look-ahead-zero rule as a field. Moves "immediately before" a request are made without knowledge of it and are recorded as moves after the previous request. A randomized algorithm is a probability space with a measurable cost on every sequence, and its expected cost is a lower Lebesgue integral. The off-line optimum is an infimum in ℝ≥0∞ over schedules starting in $s_0$ ; it is finite on admissible sequences.

Conventions added to the printed statement, all from the paper's setting: (i) $n\ge2$ , since with one processor the block can stay private for free; (ii) one block, since the proof of Theorem 4 splits a multi-block system into independent blocks (p. 551); (iii) admissibility in the form "each write of $i$ directly follows a read or write of $i$ ", the reading of "every write is preceded by a read to the same block" that the proof uses; without it every algorithm is defeated by a write from a processor whose block copy was invalidated; (iv) $p\in\mathbb{N}$ , $p\ge1$ ; (v) both claims from every initial state, with an additive constant depending on $n$ , $p$ , $s_0$ .

The lower bound is over all randomized algorithms, not over phase-based or deterministic ones; a statement restricted to phase-based algorithms, or the LP alone in place of the goal, would not be Theorem 4. The LP variables are free, as in the paper.

Welcome contributions: a formal version of the phase reduction (Theorems 1 and 3 of the paper) for this task system, which is reusable for the paper's other nonuniform problems; the threshold algorithms and their mixture; and a proof that the off-line optimum decomposes by write runs up to a bounded error.

Selected references

A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), 542–571. https://doi.org/10.1007/BF01189993
A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3 (1988), 79–119. https://doi.org/10.1007/BF01762111
A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.

8 thms4 active usersReviewed

Completed

Analysis Functional Analysis Harmonic Analysis+1·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics III: The Herglotz Representation and Stieltjes InversionTextbook

Motivation

In spectral theory the resolvent of a self-adjoint operator $A$ is studied through scalar functions $F_\psi(z) = \langle \psi, (A - z)^{-1}\psi\rangle$ , defined for non-real $z$ . Each $F_\psi$ is holomorphic on the upper half plane and maps it into itself. The spectral theorem, in the form presented in G. Teschl's Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), comes down to the converse: a function of this kind with the right growth is the Cauchy–Stieltjes transform of a finite measure on $\mathbb{R}$ , and that measure is the spectral measure of $\psi$ . In the other direction, the absolutely continuous, singularly continuous and pure point spectra of Schrödinger operators are identified by looking at the boundary values of $F_\psi$ on the real axis. This mission formalizes the appendix to Chapter 3 of Teschl's book (Section 3.4, The Herglotz theorem, pp. 106–110) and Theorem 3.10, the measure-theoretic layer that the rest of the book's spectral analysis stands on.

The representation goes back to G. Herglotz (1911) for the disc and R. Nevanlinna (1922) for the half plane. The inversion formula is due to T. J. Stieltjes (1894). The link between boundary values and the Lebesgue decomposition of the measure is classical harmonic analysis on the half plane (Fatou, de la Vallée Poussin) and is the tool behind the spectral-type results of Gilbert–Pearson subordinacy theory and Aronszajn–Donoghue rank-one perturbation theory.

Setting

Write $\mathbb{C}_+ = \{z \in \mathbb{C} \mid \operatorname{Im}(z) > 0\}$ . A Herglotz function is a holomorphic map $F$ on $\mathbb{C}_+$ with $\operatorname{Im} F(z) > 0$ for every $z \in \mathbb{C}_+$ (IsHerglotz).

For a Borel measure $\mu$ on $\mathbb{R}$ , its Borel transform is

F(z) = \int_{\mathbb{R}} \frac{d\mu(\lambda)}{\lambda - z}

(borelTransform μ). The spectrum of $\mu$ is its set of growth points, $\sigma(\mu) = \{\lambda \mid \mu((\lambda-\varepsilon,\lambda+\varepsilon)) > 0 \text{ for all } \varepsilon > 0\}$ (measureSpectrum).

With $B_\varepsilon(x) = (x - \varepsilon, x + \varepsilon)$ and $|\cdot|$ Lebesgue measure, the upper and lower derivatives of $\mu$ are $(\overline{D}\mu)(x) = \limsup_{\varepsilon\downarrow0} \mu(B_\varepsilon(x))/|B_\varepsilon(x)|$ and $(\underline{D}\mu)(x) = \liminf_{\varepsilon\downarrow0} \mu(B_\varepsilon(x))/|B_\varepsilon(x)|$ , values in $[0,\infty]$ (upperDeriv, lowerDeriv). The derivative $(D\mu)(x)$ is the limit when it exists, possibly $\infty$ (HasMeasureDeriv μ x d).

A set $A$ is a support of $\mu$ if $\mu(\mathbb{R}\setminus A) = 0$ (IsSupport). A support $M$ is a minimal support if every Borel $M_0 \subseteq M$ with $\mu(M_0) = 0$ is Lebesgue-null (IsMinimalSupport). The Lebesgue decomposition $d\mu = d\mu_{ac} + d\mu_s$ with respect to Lebesgue measure refines to $d\mu_s = d\mu_{sc} + d\mu_{pp}$ , where $\mu_{pp}$ lives on the atoms of $\mu$ . The absolutely continuous part $\mu_{ac}$ and the singularly continuous part $\mu_{sc}$ are acPart μ and scPart μ.

Formalization targets

Goal: Herglotz representation (Theorem 3.20)

If $F$ is a Herglotz function and $|F(z)| \le M/\operatorname{Im}(z)$ for all $z \in \mathbb{C}_+$ , then there is a Borel measure $\mu$ on $\mathbb{R}$ with $\mu(\mathbb{R}) \le M$ and

F(z) = \int_{\mathbb{R}} \frac{d\mu(\lambda)}{\lambda - z}, \qquad z \in \mathbb{C}_+ .

Milestones

Theorem 3.10. For a finite Borel measure $\mu$ , the transform is holomorphic on $\mathbb{C}\setminus\sigma(\mu)$ , is a Herglotz function when $\mu \ne 0$ , and satisfies $F(z^*) = F(z)^*$ and $|F(z)| \le \mu(\mathbb{R})/\operatorname{Im}(z)$ on $\mathbb{C}_+$ .
Theorem 3.21. $\mu$ is determined by its transform on $\mathbb{C}_+$ , and for $\lambda_1 < \lambda_2$

\tfrac12\bigl(\mu((\lambda_1,\lambda_2)) + \mu([\lambda_1,\lambda_2])\bigr) = \lim_{\varepsilon\downarrow0}\frac1\pi\int_{\lambda_1}^{\lambda_2}\operatorname{Im}F(\lambda+i\varepsilon)\,d\lambda .

Theorem 3.22. For every $\lambda$ , $(\underline D\mu)(\lambda) \le \liminf_{\varepsilon\downarrow0}\frac1\pi\operatorname{Im}F(\lambda+i\varepsilon) \le \limsup_{\varepsilon\downarrow0}\frac1\pi\operatorname{Im}F(\lambda+i\varepsilon) \le (\overline D\mu)(\lambda)$ .
Theorem 3.23. $\lim_{\varepsilon\downarrow0}\frac1\pi\operatorname{Im}F(\lambda+i\varepsilon)$ exists in $[0,\infty]$ for $\mu$ -a.e. and Lebesgue-a.e. $\lambda$ , equals $(D\mu)(\lambda)$ wherever the latter exists; the set where it is $\infty$ supports $\mu_{sc}$ , and the set where it lies in $(0,\infty)$ is a minimal support of $\mu_{ac}$ .
Corollary 3.24. If $\limsup_{\varepsilon\downarrow0}\operatorname{Im}F(\lambda+i\varepsilon) < \infty$ for all $\lambda$ in a Borel set $I$ , then $\mu|_I$ is absolutely continuous.
Corollary 3.25. $\lim_{\varepsilon\downarrow0}F(\lambda+i\varepsilon)$ exists (finite or $\infty$ ) $\mu$ -a.e. and Lebesgue-a.e., and is finite Lebesgue-a.e.

Significance

Theorem 3.20 together with Theorem 3.10 is a bijection between finite Borel measures on $\mathbb{R}$ and Herglotz functions of bounded growth $\operatorname{Im}(z)|F(z)|$ . In Teschl's development it produces the spectral measures $\mu_\psi$ from the resolvent, and hence the projection-valued measure of an unbounded self-adjoint operator. Theorems 3.21–3.25 turn spectral questions into boundary-value questions. The later chapters on Sturm–Liouville operators and one-dimensional Schrödinger operators decide which spectral type an operator has by reading $\operatorname{Im} F(\lambda + i0)$ for the Weyl–Titchmarsh function.

These are textbook results with complete published proofs. Mathlib has the upper half plane as a type, Lebesgue decomposition, Radon–Nikodym derivatives and Vitali-family differentiation of measures, but it has no Borel (Cauchy–Stieltjes) transform of a measure on $\mathbb{R}$ , no Herglotz representation on the half plane, and no Stieltjes inversion. The remaining work is to formalize the known proofs against Mathlib's measure theory and complex analysis. No machine-checked version of these statements is known to exist on Prove2Me.

Difficulty

For the goal, the measure has to be built: nothing in the hypothesis names it. A Herglotz function gives no measure directly, only a family of absolutely continuous approximations coming from the boundary values of $\operatorname{Im} F$ slightly above the real axis. The difficulty is to pass to a limit that is only a measure (it may have atoms and singular parts), and to identify the limit's transform with $F$ itself, not just its imaginary part. The uniform bound is what makes the limit exist and keeps its mass at most $M$ . Without it the general Nevanlinna representation carries an extra linear term and a non-finite measure, and the statement here fails.

For the boundary-value theorems, the pointwise behaviour of the Poisson integral has to be compared with the symmetric derivatives of $\mu$ at each point, including points where $\mu$ is singular. The almost-everywhere statements for both $\mu$ and Lebesgue measure need the differentiation theory of measures in its singular form: the derivative is infinite $\mu_s$ -almost everywhere, not only finite Lebesgue-almost everywhere.

Formalization scope

Measures are MeasureTheory.Measure ℝ on the Borel σ-algebra. Every theorem assumes IsFiniteMeasure μ, except the goal, whose conclusion μ Set.univ ≤ ENNReal.ofReal M makes μ finite. Functions on the half plane are ℂ → ℂ, constrained only on {z | 0 < z.im}. The Borel transform is a Bochner integral. Every claim evaluates it where the integrand is bounded, so Mathlib's convention that a non-integrable integral is $0$ never enters.

Limits as $\varepsilon \downarrow 0$ are taken along 𝓝[>] 0. The quantities that may be infinite (derivatives of measures, boundary values of $\operatorname{Im}F$ ) live in ℝ≥0∞, with $\operatorname{Im}F(\lambda+i\varepsilon)$ , which is nonnegative for $\varepsilon > 0$ , embedded by ENNReal.ofReal. An infinite limit of $F$ itself is Tendsto … (Bornology.cobounded ℂ). The lower and upper derivatives, the supports and the parts $\mu_{ac}$ , $\mu_{sc}$ are defined in the mission's namespace exactly as in the book (Sec. A.8, Sec. 3.2).

Three readings of the printed text are fixed. Theorem 3.22 is stated for $\operatorname{Im}F(\lambda+i\varepsilon)$ , which is what its proof estimates. Theorem 3.23's identity takes the factor $1/\pi$ once, consistent with Theorem 3.22. Theorem 3.10's Herglotz conclusion is stated for $\mu \ne 0$ : the book's Herglotz functions map into the open half plane, and the zero measure's transform is identically zero.

A Herglotz function is defined analytically (holomorphic, positive imaginary part), never as "a Borel transform"; the latter would make the goal a tautology. No object is taken as data. The chunk uses no Hilbert space, no operator, and no projection-valued measure.

Useful infrastructure: UpperHalfPlane, Cauchy's integral formula on rectangles and semicircles, weak compactness of finite measures on $\mathbb{R}$ (Helly/Prokhorov), Mathlib's VitaliFamily.ae_tendsto_rnDeriv and Measure.singularPart. A reusable Poisson-kernel library for the half plane would be a welcome by-product, as would the vague-convergence lemmas of the book's Appendix A.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009, Sec. 3.2, Sec. 3.4 and Sec. A.8. https://doi.org/10.1090/gsm/099
G. Herglotz, Über Potenzreihen mit positivem, reellen Teil im Einheitskreis, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, Math.-Phys. Klasse 63 (1911), 501–511.
R. Nevanlinna, Asymptotische Entwicklungen beschränkter Funktionen und das Stieltjessche Momentenproblem, Annales Academiae Scientiarum Fennicae A 18 (1922).
T. J. Stieltjes, Recherches sur les fractions continues, Annales de la Faculté des Sciences de Toulouse 8 (1894), J1–J122. https://doi.org/10.5802/afst.108
F. Gesztesy, E. Tsekanovskii, On matrix-valued Herglotz functions, Mathematische Nachrichten 218 (2000), 61–138. https://doi.org/10.1002/1522-2616(200010)218:1<61::AID-MANA61>3.0.CO;2-D

28 thms4 active usersReviewed

Completed

Analysis Functional Analysis Mathematical Physics·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics I: Self-Adjoint Extensions and Defect IndicesTextbook

Why self-adjoint extensions matter

In quantum mechanics an observable is a self-adjoint operator on a complex Hilbert space $\mathfrak{H}$ . Physics, however, usually hands over a symmetric operator: a differential expression such as $-\mathrm{i}\,\tfrac{d}{dx}$ or $-\Delta + V$ on a convenient domain of smooth functions, on which integration by parts shows $\langle \varphi, A\psi\rangle = \langle A\varphi, \psi\rangle$ . Symmetry is easy to check and self-adjointness is not. Two questions then decide whether the formal expression defines a physical theory: does $A$ have a self-adjoint extension at all, and if so, how many? Different extensions correspond to different boundary conditions and to different dynamics (via Stone's theorem), so the answer is physically meaningful.

John von Neumann answered both questions in 1929–1930 with the Cayley transform and the defect indices (von Neumann 1930). His criterion is the goal of this mission, in the form given in Chapter 2 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), from which every statement of the mission is taken.

Setting

Let $\mathfrak{H}$ be a complex Hilbert space with inner product $\langle\cdot,\cdot\rangle$ , conjugate-linear in the first argument. A linear operator $A$ is a linear map $A : \mathfrak{D}(A) \to \mathfrak{H}$ defined on a linear subspace $\mathfrak{D}(A)$ , its domain. An operator $B$ extends $A$ , written $A \subseteq B$ , if $\mathfrak{D}(A) \subseteq \mathfrak{D}(B)$ and $B\psi = A\psi$ for $\psi \in \mathfrak{D}(A)$ .

$A$ is symmetric if $\mathfrak{D}(A)$ is dense and $\langle \varphi, A\psi\rangle = \langle A\varphi, \psi\rangle$ for all $\varphi, \psi \in \mathfrak{D}(A)$ . For densely defined $A$ the adjoint $A^*$ has domain $\{\psi \mid \exists \tilde\psi : \langle\psi, A\varphi\rangle = \langle\tilde\psi, \varphi\rangle \ \forall \varphi \in \mathfrak{D}(A)\}$ and acts by $A^*\psi = \tilde\psi$ . $A$ is self-adjoint if $A = A^*$ , domains included, and essentially self-adjoint if its closure $\overline{A}$ (the operator whose graph is the closure of the graph of $A$ ) is self-adjoint.

For $z \in \mathbb{C}$ , $A + z$ is the operator $\psi \mapsto A\psi + z\psi$ on $\mathfrak{D}(A)$ . The resolvent set $\rho(A)$ is the set of $z$ for which $A - z : \mathfrak{D}(A) \to \mathfrak{H}$ is a bijection with bounded inverse $R_A(z) = (A-z)^{-1}$ , and the spectrum is $\sigma(A) = \mathbb{C}\setminus\rho(A)$ .

For symmetric $A$ the defect spaces and defect indices are

K_\pm = \operatorname{Ran}(A \pm \mathrm{i})^\perp = \operatorname{Ker}(A^* \mp \mathrm{i}), \qquad d_\pm(A) = \dim K_\pm,

where $\dim$ is the Hilbert dimension (the cardinality of an orthonormal basis, possibly infinite). The Cayley transform of $A$ is

V = (A - \mathrm{i})(A + \mathrm{i})^{-1} : \operatorname{Ran}(A + \mathrm{i}) \to \operatorname{Ran}(A - \mathrm{i}).

Formalization targets

Goal: von Neumann's criterion (Theorem 2.26)

For every symmetric operator $A$ ,

\exists\, B \supseteq A \text{ self-adjoint} \iff d_+(A) = d_-(A).

Milestones

In the order of the book:

Corollary 2.2. A self-adjoint operator has no proper symmetric extension.
Lemma 2.3. If $A$ is symmetric and $\operatorname{Ran}(A + z) = \operatorname{Ran}(A + z^*) = \mathfrak{H}$ for one $z \in \mathbb{C}$ , then $A$ is self-adjoint.
Lemma 2.7. A symmetric $A$ is essentially self-adjoint iff $\overline{\operatorname{Ran}(A+z)} = \overline{\operatorname{Ran}(A+z^*)} = \mathfrak{H}$ for one $z \in \mathbb{C}\setminus\mathbb{R}$ , iff $\operatorname{Ker}(A^*+z) = \operatorname{Ker}(A^*+z^*) = \{0\}$ for one such $z$ ; for nonnegative $A$ , a real $z > 0$ (spectral point $-z < 0$ ) may be used too.
Theorem 2.18. A symmetric $A$ is self-adjoint iff $\sigma(A) \subseteq \mathbb{R}$ ; it is self-adjoint with $A \ge E$ iff $\sigma(A) \subseteq [E,\infty)$ ; and then $\|R_A(z)\| \le |\operatorname{Im} z|^{-1}$ and $\|R_A(\lambda)\| \le |\lambda - E|^{-1}$ for $\lambda < E$ .
Theorem 2.25. The Cayley transform is a bijection from the symmetric operators onto the isometric operators $V$ with $\operatorname{Ran}(1 - V)$ dense.
Theorem 2.26, (2.103)–(2.104). For a closed symmetric $A$ with a self-adjoint extension $A_1$ whose Cayley transform is $V_1$ : $\mathfrak{D}(A_1) = \mathfrak{D}(A) + (1 - V_1)K_+$ and $A_1(\psi + \varphi_+ - V_1\varphi_+) = A\psi + \mathrm{i}\varphi_+ + \mathrm{i}V_1\varphi_+$ .
Lemma 2.27. $A$ is closed iff $\mathfrak{D}(V)$ is closed iff $\operatorname{Ran}(V)$ is closed iff $V$ is closed.
Theorem 2.28. If a symmetric $A$ commutes with a conjugation $C$ ( $C$ -real), then $d_+(A) = d_-(A)$ .

Significance

The criterion is the standard tool for deciding whether a formal Hamiltonian is a legitimate observable, and for classifying its realizations: by the parametrization (2.103)–(2.104), the self-adjoint extensions correspond to the unitary maps $K_+ \to K_-$ . Theorem 2.28 turns the criterion into a practical test, since every real differential operator, for example a Schrödinger operator with real potential, is $C$ -real for complex conjugation and therefore has self-adjoint extensions. Lemma 2.7 and Theorem 2.18 are the everyday criteria for self-adjointness and the basic spectral facts on which Chapters 3–6 of the book rest. The Friedrichs extension, Weyl's limit point/limit circle theory and the Kato–Rellich theorem all refine these statements.

All of these results are classical and proved in every text on unbounded operators (for example Schmüdgen 2012, Chapters 3 and 13). None is formalized in Mathlib, which provides the adjoint, closure and self-adjointness of a LinearPMap but no resolvent set, spectrum, Cayley transform or defect theory for unbounded operators. The platform's existing material on essential self-adjointness is stated for specific Hamiltonians on bespoke structures, not for general operators. A formal proof here supplies the unbounded-operator layer that every later mission in this series (spectral theorem, Kato–Rellich, Weyl's theorem, Sturm–Liouville theory) restates.

Difficulty

The obvious reduction, "a self-adjoint extension is a unitary extension of the Cayley transform, and a unitary $K_+ \to K_-$ exists iff the dimensions agree", hides most of the work. The correspondence between extensions of $A$ and extensions of $V$ runs through the inverse Cayley transform $A = \mathrm{i}(1+V)(1-V)^{-1}$ , which requires injectivity of $1 - V$ and careful bookkeeping of partial domains. Extending an isometry to a unitary requires passing to closures of $\operatorname{Ran}(A \pm \mathrm{i})$ when $A$ is not closed. Equal Hilbert dimension must be converted into an actual unitary between the defect spaces. Theorem 2.18 needs the self-adjointness criterion of Lemma 2.7 in the direction "spectrum real implies self-adjoint", where the range conditions come from the resolvent set rather than from symmetry. Each of these steps is routine on paper and requires explicit domain management in Lean.

Formalization scope

Operators are Mathlib LinearPMaps H →ₗ.[ℂ] H on a complex Hilbert space (InnerProductSpace ℂ H, CompleteSpace H). Separability, part of the book's standing assumption, is not needed by any statement and is not assumed. Extension is the order A ≤ B. Self-adjointness is Mathlib's IsSelfAdjoint (equality with LinearPMap.adjoint), and symmetry includes density of the domain, so every adjoint in the mission is taken of a densely defined operator and is the book's $A^*$ . The closure is LinearPMap.closure; closedness is LinearPMap.IsClosed.

The mission uses the series' shared definitions TeschlQM.Shared.IsSymmetric, TeschlQM.Shared.IsEssentiallySelfAdjoint and TeschlQM.Shared.IsResolventAt, resolventSet, spectrum, and defines, in the namespace TeschlQM.SelfAdjoint: addScalar, rangeAdd, kerAdd for $A + z$ , $\operatorname{Ran}(A+z)$ , $\operatorname{Ker}(A+z)$ ; IsCayleyTransform, IsIsometric, rangeOneSub; defectPlus, defectMinus, HasEqualDefectIndices; IsConjugation, IsCReal. Nothing that the book derives is taken as data: the Cayley transform is a relation that determines $V$ from $A$ , and its existence and uniqueness are part of Theorem 2.25.

Conventions that matter:

$\sigma(A)$ is defined exactly as on p. 73 of the book (bijective onto $\mathfrak{H}$ with bounded inverse), not with Mathlib's Banach-algebra spectrum. For a non-closed operator this makes $\sigma(A) = \mathbb{C}$ .
$K_\pm$ are $\operatorname{Ran}(A\pm\mathrm{i})^\perp$ , and $d_+ = d_-$ is expressed as the existence of a unitary K₊ ≃ₗᵢ[ℂ] K₋, which is equivalent to equality of Hilbert dimensions. Reading "self-adjoint extension" with the order reversed, or taking $K_\pm$ as kernels of $A \mp \mathrm{i}$ (which are trivial for symmetric $A$ ), would make the goal trivial; neither is used.
A conjugation satisfies $\langle C\psi, C\varphi\rangle = \langle\varphi,\psi\rangle$ (antiunitary). The book prints $\langle\psi,\varphi\rangle$ on the right, which no nonzero conjugate-linear map satisfies.
In Lemma 2.7 the book admits " $z \in (-\infty, 0)$ " for nonnegative $A$ while writing the conditions on $A + z$ ; the correct range in that convention, and the one its proof uses, is $z \in (0, \infty)$ , which is what is stated.
The (2.103)–(2.104) milestone assumes $A$ closed; without it (2.103) is false (a non-closed essentially self-adjoint $A$ is a counterexample).

Reusable parts: the resolvent/spectrum layer and the Cayley transform are needed throughout the rest of the book. Proofs of any milestone, and API lemmas about rangeAdd, kerAdd and adjoints (such as $\operatorname{Ker}(A^*) = \operatorname{Ran}(A)^\perp$ and the reversal $A \subseteq B \Rightarrow B^* \subseteq A^*$ ), are welcome.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, AMS Graduate Studies in Mathematics 99, 2009, Chapter 2. https://doi.org/10.1090/gsm/099
J. von Neumann, Allgemeine Eigenwerttheorie Hermitescher Funktionaloperatoren, Mathematische Annalen 102 (1930), 49–131. https://doi.org/10.1007/BF01782338
K. Schmüdgen, Unbounded Self-adjoint Operators on Hilbert Space, Graduate Texts in Mathematics 265, Springer, 2012. https://doi.org/10.1007/978-94-007-4753-1

16 thms4 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Random Gradient-Free Minimization of Convex Functions III: Accelerated Random SearchResearch Paper

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 9 (p. 549)

For all $k \ge 0$ ,

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

where

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

Selected references

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

14 thms4 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Random Gradient-Free Minimization of Convex Functions II: Random Gradient Descent for Smooth and Strongly Convex ProblemsResearch Paper

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access to the objective only through its values: the function is computed by a black-box code, and derivatives are unavailable or too expensive to program. Zeroth-order (derivative-free) methods address this setting. Classical derivative-free methods (pattern search, Nelder–Mead, model-based trust regions) come with weak or no global complexity guarantees for convex problems.

Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that replacing the gradient by a finite difference along a random Gaussian direction yields methods whose expected complexity is that of the corresponding gradient method multiplied by a factor proportional to the dimension. Their paper is a standard reference for zeroth-order convex optimization and for Gaussian smoothing, and its oracle and analysis are reused in bandit convex optimization, zeroth-order stochastic optimization (e.g. Ghadimi–Lan 2013) and derivative-free reinforcement learning.

This mission concerns Section 5 of the paper: the random gradient method $\mathcal{RG}_\mu$ for smooth convex functions and its linear rate for strongly convex ones.

Setting

Let $E$ be a real inner product space of finite dimension $n$ , with norm $\|\cdot\|$ . (The paper works with a space carrying an operator $B = B^* \succ 0$ and norm $\|x\| = \langle Bx, x\rangle^{1/2}$ ; choosing $\langle B\cdot,\cdot\rangle$ as the inner product gives exactly this setting, and the dual norm $\|\cdot\|_*$ becomes the norm of the Riesz representative.)

A function $f : E \to \mathbb R$ belongs to $C^{1,1}(E)$ with constant $L_1$ if it is differentiable and $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x - y\|$ for all $x, y$ . It is strongly convex with parameter $\tau > 0$ if $f(y) \ge f(x) + \langle \nabla f(x), y - x\rangle + \frac{\tau}{2}\|y-x\|^2$ for all $x, y$ .

Let $u$ be a standard Gaussian vector of $E$ (coordinates in any orthonormal basis are independent $N(0,1)$ ). The Gaussian approximation of $f$ with parameter $\mu \ge 0$ is $f_\mu(x) = \mathbb E_u f(x + \mu u)$ , and the moments are $M_p = \mathbb E_u\|u\|^p$ . The random gradient-free oracle returns, for a sampled direction $u$ ,

B^{-1}g_\mu(x) = \frac{f(x+\mu u) - f(x)}{\mu}\, u \quad (\mu > 0), \qquad B^{-1}g_0(x) = f'(x,u)\, u,

and the symmetric oracle is $B^{-1}\hat g_\mu(x) = \frac{f(x+\mu u) - f(x - \mu u)}{2\mu}u$ .

Consider $f^* = \min_{x\in E} f(x)$ for a convex $f \in C^{1,1}(E)$ , assumed solvable with a minimizer $x^*$ , and $n \ge 2$ . The random gradient method $\mathcal{RG}_\mu$ (Eq. (54), p. 546) is:

Method $\mathcal{RG}_\mu$ : Choose $x_0 \in E$ . Iteration $k \ge 0$ . a). Generate $u_k$ and corresponding $g_\mu(x_k)$ . b). Compute $x_{k+1} = x_k - hB^{-1}g_\mu(x_k)$ .

The directions $u_0, u_1, \dots$ are independent standard Gaussian vectors, and $\phi_k = \mathbb E f(x_k)$ (with $\phi_0 = f(x_0)$ ).

Formalization targets

Goal: Theorem 8 (p. 546)

With step size $h = \frac{1}{4(n+4)L_1}$ and any $\mu \ge 0$ , for every $N \ge 0$ ,

\frac{1}{N+1}\sum_{k=0}^{N}(\phi_k - f^*) \le \frac{4(n+4)L_1\|x_0-x^*\|^2}{N+1} + \frac{9\mu^2(n+4)^2L_1}{25},

and, if $f$ is strongly convex with parameter $\tau > 0$ , then with $\delta_\mu = \frac{18\mu^2(n+4)^2}{25\tau}L_1$ ,

\phi_N - f^* \le \frac12 L_1\left[\delta_\mu + \left(1 - \frac{\tau}{8(n+4)L_1}\right)^{N}\big(\|x_0-x^*\|^2 - \delta_\mu\big)\right].

Both bounds are one theorem with one proof in the paper, so the goal states their conjunction, with every constant as printed.

Milestones

The milestones are the results the paper's proof of Theorem 8 rests on, in attack order:

Lemma 1 (p. 534): $M_p \le n^{p/2}$ for $p \in [0,2]$ and $n^{p/2} \le M_p \le (p+n)^{p/2}$ for $p \ge 2$ .
Theorem 3.1, (32) (p. 537): $\mathbb E_u\|g_0(x)\|_*^2 \le (n+4)\|\nabla f(x)\|_*^2$ at a point of differentiability.
Theorem 4.2, (35) (p. 538): $\mathbb E_u\|g_\mu(x)\|_*^2 \le \frac{\mu^2}{2}L_1^2(n+6)^3 + 2(n+4)\|\nabla f(x)\|_*^2$ , and the same with $\frac{\mu^2}{8}$ for $\hat g_\mu$ .
Eq. (21) (pp. 534–535): for $\mu > 0$ , $f_\mu$ is differentiable with $\nabla f_\mu(x) = \mathbb E_u B^{-1}g_\mu(x)$ .
Eq. (25) (p. 535): $\mathbb E_u \langle\nabla f(x), u\rangle u = \nabla f(x)$ , the $\mu = 0$ counterpart.
Convexity of $f_\mu$ (p. 533) and Eq. (11): $f \le f_\mu$ for convex $f$ .
Theorem 1, (19) (p. 534): $|f_\mu(x) - f(x)| \le \frac{\mu^2}{2}L_1 n$ .

Significance

The result. Theorem 8 shows that a method using two function values per iteration reaches accuracy $\epsilon$ on a smooth convex problem in $O(\frac{n}{\epsilon}L_1\|x_0 - x^*\|^2)$ iterations, and in $O(\frac{nL_1}{\tau}\ln\frac{L_1\|x_0-x^*\|^2}{\epsilon})$ iterations under strong convexity, provided $\mu$ is small enough. This is $n$ times the complexity of the deterministic gradient method, which is the natural price for replacing an $n$ -dimensional gradient by one directional estimate. The strongly convex bound makes explicit the bias floor $\frac12 L_1\delta_\mu$ caused by the finite-difference step, and shows that it vanishes for the limiting method $\mathcal{RG}_0$ .

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. A formalization produces a reusable Gaussian-smoothing layer on Mathlib's stdGaussian (moments of the Gaussian norm, differentiation of $f_\mu$ under the integral, variance bounds of random oracles) and a complete expected-complexity proof of a randomized first-order method, in which the probabilistic structure (independent directions, iterates depending only on past directions, tower property) has to be handled explicitly.

Difficulty

The deterministic part of the argument is the textbook analysis of gradient descent. The difficulty is in the Gaussian facts it uses. The obvious bound on the oracle's second moment, $\mathbb E\langle\nabla f(x),u\rangle^2\|u\|^2 \le \|\nabla f(x)\|^2 M_4 \le (n+4)^2\|\nabla f(x)\|^2$ , loses a factor of $n$ and would give a quadratic dependence on dimension; the $(n+4)$ of (32) needs a sharper computation. The moment bounds of Lemma 1 for non-integer $p$ and the differentiation under the integral in (21) are measure-theoretic steps that Mathlib does not package. Finally, the step from per-iteration inequalities to bounds on $\phi_k$ requires conditioning on the past directions, which must be set up on a probability space carrying the whole sequence $u_0, u_1, \dots$ .

Formalization scope

$E$ is an arbitrary finite-dimensional real inner product space with MeasurableSpace and BorelSpace, $n$ is Module.finrank ℝ E, and $\nabla f$ is Mathlib's gradient. Expectations over $u$ are Bochner integrals against ProbabilityTheory.stdGaussian E. A run of $\mathcal{RG}_\mu$ lives on a probability space $(\Omega, P)$ : measurable directions $u_k$ , jointly independent (iIndepFun) with law stdGaussian E, iterates with $x_0$ deterministic and the update holding for every $k$ and outcome. $\phi_k$ is ∫ ω, f (x k ω) ∂P. The oracle is defined by cases, with $f'(x,u)u$ at $\mu = 0$ ( $f'(x,u)$ the one-sided directional derivative of Eq. (23), a Filter.limUnder, which equals fderiv ℝ f x u for differentiable $f$ ), so the goal covers every $\mu \ge 0$ as the paper claims. $L_1$ and $\tau$ are any constants satisfying the defining inequalities. The standing assumptions of Section 5 (convexity, a global minimizer $x^*$ , $n \ge 2$ ) and $L_1 > 0$ are explicit hypotheses; $n \ge 2$ is needed for the constant $9/25$ .

A trivializing formalization is ruled out: the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the true gradient (which would be deterministic gradient descent), and every expectation in the statements is of a quantity that is integrable under the stated hypotheses, so no bound holds through a junk value of a non-integrable integral.

A complete development needs Gaussian moment computations in finite dimension, differentiation under the integral sign for $f_\mu$ , the variance bounds of the oracles, and a conditional-expectation argument for the iteration. The smoothing layer is reusable for the companion missions on random search for nonsmooth problems and on the accelerated random method, and for other zeroth-order methods. Contributions of any of the milestones, of general Gaussian-integrability lemmas, or of alternative proofs are welcome.

Selected references

Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4):2341–2368, 2013. https://doi.org/10.1137/120880811
Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

14 thms4 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Random Gradient-Free Minimization of Convex Functions I: Random Search for Nonsmooth Convex ProblemsResearch Paper

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access to the values of an objective function but not to its gradient: the function is computed by a black-box program, by a simulator, or by a model whose derivatives are unavailable or too expensive. Zeroth-order (or derivative-free) methods use only function values. Classical direct-search methods of this kind usually come without complexity bounds.

Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that a very simple randomized scheme has explicit, dimension-dependent worst-case complexity bounds. The idea is to replace the gradient by a finite difference of $f$ along a random Gaussian direction. The resulting oracle is an unbiased estimate of the gradient of a smoothed version of $f$ . Their analysis is the reference point for the later literature on zeroth-order stochastic optimization, bandit convex optimization and gradient-free training.

This mission covers the paper's result for nonsmooth convex problems over a closed convex set: the projected random search method $\mathcal{RS}_\mu$ and its convergence bound, Theorem 6.

Setting

Let $E$ be a real inner product space of finite dimension $n$ , with norm $\|\cdot\|$ . (The paper works with a space carrying a positive definite operator $B$ and the norm $\langle Bx, x\rangle^{1/2}$ . This is the same thing as an arbitrary finite-dimensional inner product space, with $B$ encoding the inner product, and the development is written in that generality.)

A function $f : E \to \mathbb R$ is Lipschitz continuous with constant $L_0 \ge 0$ if $|f(x) - f(y)| \le L_0 \|x - y\|$ for all $x, y$ . The paper calls this class $C^{0,0}(E)$ and writes $L_0(f)$ for the constant.

Let $u$ be a standard Gaussian vector in $E$ : its coordinates in any orthonormal basis are independent $N(0,1)$ variables. For $\mu \ge 0$ the Gaussian smoothing of $f$ is

f_\mu(x) = \mathbb E_u\, f(x + \mu u),

and the Gaussian moments are $M_p = \mathbb E_u \|u\|^p$ .

For $\mu > 0$ the random gradient-free oracle at $x$ draws $u$ and returns the vector

g_\mu(x) = \frac{f(x+\mu u) - f(x)}{\mu}\, u .

It costs two function values.

The problem is

f^* = \min_{x \in Q} f(x),

where $Q \subseteq E$ is closed and convex, $f$ is convex and Lipschitz, and $x^* \in Q$ is a minimizer. With $\pi_Q$ the Euclidean projection onto $Q$ , positive steps $h_0, h_1, \ldots$ and a starting point $x_0 \in Q$ , the random search method $\mathcal{RS}_\mu$ iterates

x_{k+1} = \pi_Q\big(x_k - h_k\, g_\mu(x_k)\big),

drawing a fresh independent Gaussian direction $u_k$ at every iteration. The iterates are random. Write $\phi_k = \mathbb E f(x_k)$ and $S_N = \sum_{k=0}^N h_k$ .

Formalization targets

Goal: Theorem 6

For every $N \ge 0$ ,

\frac{1}{S_N}\sum_{k=0}^{N} h_k(\phi_k - f^*) \le \mu L_0\, n^{1/2} + \frac{1}{S_N}\left[\frac12\|x_0 - x^*\|^2 + \frac{(n+4)^2}{2} L_0^2 \sum_{k=0}^{N} h_k^2\right].

The step sizes, the smoothing parameter and the horizon are left free, so every step-size rule in the paper follows from this one inequality. The constants are the paper's.

Milestones

The facts about smoothing and the oracle on which the goal rests, in the paper's order:

Lemma 1: $M_p \le n^{p/2}$ for $p \in [0,2]$ and $n^{p/2} \le M_p \le (p+n)^{p/2}$ for $p \ge 2$ .
Theorem 1 (18): $|f_\mu(x) - f(x)| \le \mu L_0 n^{1/2}$ .
Convexity of $f_\mu$ for convex $f$ .
Eq. (11): $f_\mu \ge f$ for convex $f$ .
Eq. (21): $\nabla f_\mu(x) = \mathbb E_u\, g_\mu(x)$ for $\mu > 0$ .
Theorem 4.1 (34): $\mathbb E_u \|g_\mu(x)\|^2 \le L_0^2 (n+4)^2$ .
Theorem 2 ( $\mu \ge 0$ ): $f(y) \ge f(x) - \mu L_0 n^{1/2} + \langle \nabla f_\mu(x), y - x\rangle$ for all $y$ , where at $\mu = 0$ the vector is the limiting $\nabla f_0(x) = \mathbb E_u[f'(x,u)\,u]$ of Eq. (24).

Significance

Theorem 6 shows that a method using only function values, with no subgradient, solves nonsmooth convex problems with the classical projected-subgradient guarantee. Two things change: $L_0^2$ is multiplied by $(n+4)^2$ , and a bias $\mu L_0 n^{1/2}$ appears, which can be made as small as desired. With suitable $\mu$ , $h_k$ and $N$ an $\epsilon$ -accurate expected value is reached in $O(n^2 L_0^2 R^2/\epsilon^2)$ oracle calls. The factor $n^2$ quantifies the cost of not having gradients. The same analysis carries over to stochastic objectives (the paper's Theorem 7).

The results are proved in the paper. As far as is known, none of them has a machine-checked proof. The mission produces a Lean development of Gaussian smoothing on an arbitrary finite-dimensional inner product space: the moment bounds, the approximation, convexity and gradient identities, and the oracle variance bound. On top of it sits the full convergence theorem for a randomized projected method, stated for the actual random process rather than for an idealized expectation recursion. The smoothing layer is reusable: the same facts underlie the smooth and accelerated random methods of the same paper and most Gaussian-smoothing analyses in zeroth-order optimization.

Difficulty

A plain subgradient analysis does not apply. The vector $g_\mu(x_k)$ is not a subgradient of $f$ , nor an unbiased estimate of one. It is an unbiased estimate of the gradient of a different function, $f_\mu$ , and its second moment grows with the dimension. The argument therefore has to move between $f$ and $f_\mu$ at exactly the right places, using properties of $f_\mu$ that hold for every nonsmooth Lipschitz $f$ .

Those properties are genuinely analytic. Differentiating $f_\mu$ requires differentiating a Gaussian integral of a function that need not be differentiable. The moment bounds need estimates of $\mathbb E\|u\|^p$ for real $p$ . In the probabilistic part, $x_k$ depends on $u_0, \ldots, u_{k-1}$ , and each one-step estimate has to be integrated using the independence of $u_k$ from the past. Mathlib provides the standard Gaussian measure and independence, but no Gaussian smoothing, no projection onto convex sets and no conditional-expectation argument for this kind of recursion.

Formalization scope

The space is E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E], and $n$ is Module.finrank ℝ E. No lower bound on $n$ is assumed. The Gaussian is ProbabilityTheory.stdGaussian E, and expectations are Bochner integrals against it. $f_\mu$ is the definition smoothing, $M_p$ is moment (with real exponent Real.rpow), and $g_\mu$ is oracle.

The projection is the relation IsMetricProjection Q y z ( $z \in Q$ and $z$ is a nearest point of $Q$ to $y$ ). The run is the predicate IsRandomSearchRun: directions $u_k : \Omega \to E$ on a probability space $(\Omega, P)$ , measurable, mutually independent (iIndepFun) and each with law stdGaussian E; a deterministic $x_0 \in Q$ ; and the update above for every $k$ and every outcome.

$\phi_k$ is $\int f(x_k)\,dP$ . The Lipschitz constant $L_0 \ge 0$ is any constant satisfying the Lipschitz inequality. It is an explicit hypothesis, because the paper's bound uses $L_0(f)$ , which presupposes $f \in C^{0,0}(E)$ . The smoothing parameter satisfies $\mu > 0$ and every step satisfies $h_k > 0$ .

Two trivializing formalizations are ruled out. First, an expectation of a non-integrable function would be $0$ as a Bochner integral; Lipschitz continuity of $f$ makes every expectation in the mission integrable, and no statement relies on the junk value. Second, a run whose directions are not independent standard Gaussians, or whose update uses a subgradient instead of the finite difference, is a different theorem (the projected subgradient method). The run predicate fixes the paper's process exactly. A run exists for every closed $Q$ containing $x_0$ (on the countable product of Gaussians), so the goal is not vacuous.

A complete development needs:

Gaussian integration by parts, or differentiation under the integral, for Lipschitz integrands;
moment estimates for the standard Gaussian norm;
existence and nonexpansiveness of projections onto closed convex sets;
an expectation argument for the random recursion.

The smoothing lemmas, the moment bounds and the projection facts are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, general lemmas about stdGaussian and projections, and alternative proofs of Lemma 1 (for example through the chi distribution).

Selected references

Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
A. D. Flaxman, A. T. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
J. C. Duchi, M. I. Jordan, M. J. Wainwright, A. Wibisono, Optimal rates for zero-order convex optimization: the power of two function evaluations, IEEE Trans. Inf. Theory 61(5):2788–2806, 2015. https://arxiv.org/abs/1312.2139

14 thms4 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

The Distributionally Robust Chance-Constrained Vehicle Routing Problem I: With a Subadditive Demand Estimator the Two-Index Vehicle Flow Formulation Is ExactResearch Paper

Motivation

The capacitated vehicle routing problem (CVRP) asks for delivery routes of minimum cost. Each route starts and ends at a depot, every customer is visited exactly once, and the demand served on a route does not exceed the vehicle capacity. The problem is central in logistics and one of the most studied problems in combinatorial optimization. Its standard exact methods are branch-and-cut algorithms built on the two-index vehicle flow formulation, a 0/1 program over arcs whose capacity constraints are the rounded capacity inequalities (RCIs); see Laporte, Nobert and Desrochers (1985) and Semet, Toth and Vigo (2014).

In practice customer demands are uncertain. A chance-constrained CVRP requires each route to respect its capacity with probability at least $1-\epsilon$ under a known distribution. That distribution is rarely known. Most solution methods also need independent demands. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP. There the chance constraint must hold for every distribution in an ambiguity set $\mathcal P$ of plausible distributions. The ambiguity set may contain dependent distributions and uncountably many of them, so it is not clear a priori that the problem can be solved by the usual branch-and-cut machinery. This mission formalizes the paper's answer to that question: its Theorem 1 and the counterexample that precedes it.

Setting

The graph is complete and directed. Its nodes are $V=\{0,\dots,n\}$ and its arcs are $A=\{(i,j)\in V\times V:i\neq j\}$ . Node $0$ is the depot and $V_C=\{1,\dots,n\}$ are the customers. There are $m$ vehicles, indexed by $K=\{1,\dots,m\}$ , each of capacity $Q>0$ . Traversing the arc $(i,j)$ costs $c(i,j)\ge 0$ ; costs may be asymmetric.

A route $\mathbf R_k=(R_{k,1},\dots,R_{k,n_k})$ is an ordered list of customers, with $R_{k,0}=R_{k,n_k+1}=0$ . A route set $\mathbf R=(\mathbf R_1,\dots,\mathbf R_m)\in\mathfrak P(V_C,m)$ partitions $V_C$ into $m$ nonempty ordered routes. Its cost is $c(\mathbf R)=\sum_{k}\sum_{l=0}^{n_k}c(R_{k,l},R_{k,l+1})$ .

The demand vector $\tilde{\boldsymbol q}\in\mathbb R^n$ is random. The ambiguity set $\mathcal P$ is a set of probability distributions of $\tilde{\boldsymbol q}$ and $\epsilon\in(0,1)$ is the risk level. The problem RVRP( $\mathcal P$ ) minimizes $c(\mathbf R)$ over route sets such that

\mathbb P\Big[\textstyle\sum_{i\in\mathbf R_k}\tilde q_i\le Q\Big]\ge 1-\epsilon\qquad\forall\,\mathbb P\in\mathcal P,\ \forall\,k\in K .

With $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x:\mathbb Q[\tilde X\le x]\ge1-\epsilon\}$ , the demand estimator of the paper's Eq. (2) is

d_{\mathcal P}(S)=\max\left\{\left\lceil\frac1Q\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\right\rceil,1\right\}\quad(S\neq\emptyset),\qquad d_{\mathcal P}(\emptyset)=0 .

The problem 2VF( $\mathcal P$ ) minimizes $\sum_{(i,j)\in A}c(i,j)x_{ij}$ over $x\in\{0,1\}^A$ with in- and out-degree $1$ at every customer and $m$ at the depot, and with the RCIs

\sum_{i\in V\setminus S}\sum_{j\in S}x_{ij}\ge d_{\mathcal P}(S)\qquad\forall\,S\subseteq V_C,\ S\neq\emptyset .

A route set induces the arc vector with $x_{ij}=1$ exactly when $(i,j)=(R_{k,l},R_{k,l+1})$ for some $k,l$ (the paper's Eq. (3)). The estimator satisfies the subadditivity condition (S) if $d_{\mathcal P}(S\cup T)\le d_{\mathcal P}(S)+d_{\mathcal P}(T)$ for all $S,T\subseteq V_C$ .

Formalization targets

Goal: Theorem 1

Assume $\tilde{\boldsymbol q}\ge\mathbf 0$ $\mathbb P$ -a.s. for all $\mathbb P\in\mathcal P$ , and assume $d_{\mathcal P}$ is real valued and satisfies (S). Then:

\begin{aligned} &\text{(i)}\ \ \mathbf R \text{ feasible in RVRP}(\mathcal P)\ \Longrightarrow\ x(\mathbf R)\text{ feasible in 2VF}(\mathcal P),\ \ c(x(\mathbf R))=c(\mathbf R);\\ &\text{(ii)}\ \ x\text{ feasible in 2VF}(\mathcal P)\ \Longrightarrow\ x=x(\mathbf R)\text{ for an RVRP}(\mathcal P)\text{-feasible }\mathbf R,\text{ unique up to reordering routes},\ c(x)=c(\mathbf R). \end{aligned}

Milestones

The chance constraint $\mathbb Q[\tilde X\le\tau]\ge1-\epsilon$ is equivalent to $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]\le\tau$ (p. 720).
Eq. (1): a route satisfies its robust chance constraint if and only if the worst-case VaR of its cumulative demand is at most $Q$ .
Example 1: an instance with two customers where a route set is RVRP( $\mathcal P$ )-feasible, yet its induced flow violates the RCI for $S=\{1,2\}$ , since $d_{\mathcal P}(\{1,2\})\ge3$ .
Example 1 (continued): on that instance $d_{\mathcal P}$ violates (S).
Theorem 1 (i) and 6. Theorem 1 (ii), stated separately.

Significance

Theorem 1 separates the modeling question from the algorithmic one. Whenever the ambiguity set yields a subadditive estimator, the distributionally robust CVRP is solved exactly by a two-index flow branch-and-cut. The only change from the deterministic case is the right-hand side $d_{\mathcal P}(S)$ of the RCIs, however many distributions $\mathcal P$ contains. The companion missions of this series show that (S) holds for every moment ambiguity set (Theorem 2 of the paper) and compute $d_{\mathcal P}$ for several classes of such sets. Example 1 shows that the hypothesis cannot be dropped: ambiguity sets that pin down each customer's marginal distribution break the equivalence.

The paper's proofs are in its online supplement; no machine-checked version of these statements exists. Formalizing them produces a checked reduction between a stochastic routing model and an integer program. It also produces reusable definitions of route sets, induced arc flows and RCIs over directed graphs with a depot.

Difficulty

Direction (ii) is a graph decomposition. A 0/1 vector with the prescribed degrees splits into $m$ depot cycles plus possibly depot-free subtours. The RCIs, through the $\max\{\cdot,1\}$ in $d_{\mathcal P}$ , must exclude the subtours, and the RCI on the customers of a single route must enforce that route's chance constraint. Uniqueness up to reordering requires that directed routes are recovered from arcs.

Direction (i) is where (S) enters. The naive argument bounds the number of vehicles entering $S$ by $d_{\mathcal P}(S)$ directly from the chance constraints. It fails because the chance constraints control each route separately, while $d_{\mathcal P}(S)$ looks at the joint worst case of the demands in $S$ ; Example 1 is exactly this failure. A set $S$ is typically visited by several routes, each covering only part of it. Relating the per-route guarantees to the joint quantity $d_{\mathcal P}(S)$ needs both hypotheses of the theorem: nonnegative demands and (S).

Formalization scope

Customers are Fin n (0-based; the paper's customer $i$ is i - 1). Nodes are Fin (n+1) with the depot 0 and customer i at i.succ, and vehicles are Fin m. A route set is R : Fin m → List (Fin n): every route is nonempty and the concatenated routes are a permutation of all customers. Arc vectors are ℕ-valued functions on ordered node pairs, with values in $\{0,1\}$ and the non-arcs $(i,i)$ fixed to $0$ .

Distributions are measures on Fin n → ℝ, and the ambiguity set is a set of probability measures. Chance constraints are written ENNReal.ofReal (1 - ε) ≤ P {q | …}. Value-at-risk is the published MultistageStochastic.valueAtRisk at level 1 - ε. The worst-case VaR is a real sSup and $d_{\mathcal P}$ is integer valued.

Two conventions implicit on the page are explicit hypotheses:

$Q>0$ , because (2) divides by $Q$ ;
boundedness of the VaR values for every customer set, which encodes the paper's declaration $d_{\mathcal P}:2^{V_C}\to\mathbb R_+$ .

A real sSup of an unbounded set is $0$ in Lean. Without the boundedness hypothesis every such estimator would silently equal $1$ and (ii) would fail. For an empty ambiguity set the Lean estimator equals $1$ on nonempty sets, as the paper's does.

The RCIs range over all nonempty customer sets with the depot on the outside. The estimator keeps the ceiling and the $\max\{\cdot,1\}$ . 2VF feasibility mentions neither routes nor chance constraints. RVRP feasibility does not mention $d_{\mathcal P}$ . A formalization in which either side refers to the other, or in which $d_{\mathcal P}$ drops the $\max\{\cdot,1\}$ , is not this theorem.

Useful contributions include lemmas on the decomposition of degree-constrained 0/1 arc vectors into depot cycles, monotonicity of VaR under almost-sure ordering, and the CDF right-continuity behind milestone 1.

Related platform work: SupplyChainTheory_vrp formalizes a different, symmetric, unit-demand VRP and is not reused.

Selected references

S. Ghosal, W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
G. Laporte, Y. Nobert, M. Desrochers, Optimal routing under capacity and distance restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050
F. Semet, P. Toth, D. Vigo, Classical exact algorithms for the capacitated vehicle routing problem, in P. Toth, D. Vigo (eds.), Vehicle Routing: Problems, Methods, and Applications, 2nd ed., SIAM, 2014, 37–57. https://doi.org/10.1137/1.9781611973594.ch2
J. Lysgaard, A. N. Letchford, R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming 100(2):423–445, 2004. https://doi.org/10.1007/s10107-003-0481-8

12 thms4 active usersReviewed

Completed

Bandit Algorithms Machine Learning Operations Research+2·Captain: mikedeng1

Optimal Best Arm Identification with Fixed Confidence III: δ-PAC Guarantee of Chernoff's Stopping Rule for Bernoulli BanditsResearch Paper

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions ("arms") one at a time, and must eventually stop and name the arm with the largest mean, with an error probability at most a prescribed risk $\delta$ , while using as few samples as possible. The problem goes back to the sequential design of experiments (Chernoff, 1959; Even-Dar, Mannor and Mansour, 2006) and underlies adaptive A/B testing, clinical trial design and hyperparameter selection.

Any fixed-confidence strategy consists of three parts: a sampling rule, a stopping rule and a decision rule. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) proposed the Track-and-Stop strategy, the first shown to match the asymptotic lower bound on the expected sample complexity. Its stopping rule is a generalized likelihood ratio (GLR) test, Chernoff's stopping rule. Its correctness, the guarantee that the recommended arm is wrong with probability at most $\delta$ , must hold whatever the sampling rule, which is what allows the sampling rule to be tuned freely for efficiency. This mission formalizes that guarantee for Bernoulli arms, Theorem 10 of the paper, with its explicit threshold $\beta(t,\delta) = \log(2t(K-1)/\delta)$ .

Setting

The arms are $\mathcal A = \{1,\dots,K\}$ . A Bernoulli bandit model is a mean vector $\boldsymbol\mu = (\mu_1,\dots,\mu_K) \in [0,1]^K$ : pulling arm $a$ returns reward $1$ with probability $\mu_a$ and $0$ otherwise, independently of the past. The class $\mathcal S$ contains the models with a unique optimal arm $a^*(\boldsymbol\mu)$ , i.e. $\mu_{a^*} > \mu_i$ for all $i \ne a^*$ .

At round $t$ the learner chooses an arm $A_t$ as a (possibly randomized) function of the past observations and observes a reward $X_t$ . Write $N_a(t)$ for the number of pulls of arm $a$ among the first $t$ rounds, $s_a(t)$ for the number of those pulls that returned $1$ , and $\hat\mu_a(t) = N_a(t)^{-1}\sum_{s \le t} X_s \mathbb 1\{A_s = a\}$ for the empirical mean. The likelihood of arm $a$ 's observations under mean $u$ is $p_u(\underline X^a_{N_a(t)}) = u^{s_a(t)}(1-u)^{N_a(t)-s_a(t)}$ .

The GLR statistic for "arm $a$ is at least as good as arm $b$ " is

Z_{a,b}(t) = \log \frac{\max_{\mu'_a \ge \mu'_b} p_{\mu'_a}(\underline X^a_{N_a(t)})\, p_{\mu'_b}(\underline X^b_{N_b(t)})}{\max_{\mu'_a \le \mu'_b} p_{\mu'_a}(\underline X^a_{N_a(t)})\, p_{\mu'_b}(\underline X^b_{N_b(t)})}.

Chernoff's stopping rule with exploration rate $\beta(t,\delta)$ is

\tau_\delta = \inf\{t \ge 1 : \exists a \in \mathcal A,\ \forall b \ne a,\ Z_{a,b}(t) > \beta(t,\delta)\},

and the decision rule recommends $\hat a_{\tau_\delta} \in \operatorname{argmax}_a \hat\mu_a(\tau_\delta)$ .

The Krichevsky–Trofimov (KT) distribution on binary sequences $x \in \{0,1\}^n$ is $\mathrm{kt}(x) = \int_0^1 \big(\pi\sqrt{u(1-u)}\big)^{-1} p_u(x)\,\mathrm du$ , the Bernoulli likelihood mixed over the Beta $(1/2,1/2)$ prior.

Formalization targets

Goal: Theorem 10

For every $\delta \in (0,1)$ , every sampling strategy, and the threshold $\beta(t,\delta) = \log\big(2t(K-1)/\delta\big)$ ,

\forall \boldsymbol\mu \in \mathcal S,\qquad \mathbb P_{\boldsymbol\mu}\big(\tau_\delta < \infty,\ \hat a_{\tau_\delta} \ne a^*\big) \le \delta .

Milestone: Lemma 11 (Willems, Shtarkov and Tjalkens, 1995)

$\mathrm{kt}$ is a probability law on $\{0,1\}^n$ , and for $n \ge 1$ ,

\sup_{x\in\{0,1\}^n}\ \sup_{u\in[0,1]} \frac{p_u(x)}{\mathrm{kt}(x)} \le 2\sqrt n .

Milestone: the pairwise crossing bound of Appendix C.1

With $T_{a,b} = \inf\{t : Z_{a,b}(t) > \beta(t,\delta)\}$ , for all arms with $\mu_a < \mu_b$ ,

\mathbb P_{\boldsymbol\mu}(T_{a,b} < \infty) \le \frac{\delta}{K-1}.

Significance

Theorem 10 decouples correctness from efficiency. Because the guarantee holds for every sampling strategy, any sampling rule, including the C-Tracking and D-Tracking rules of Track-and-Stop, the uniform rule, or a heuristic, inherits $\delta$ -correctness as soon as it is paired with Chernoff's stopping rule at this threshold. The asymptotic optimality result of the paper (Theorem 14) then only has to control the sample complexity. The threshold is explicit, with no unspecified constant, in contrast to the deviational threshold of Proposition 12.

The result is proved in the paper, in Appendix C.1, and rests on Lemma 11, which the paper quotes from the universal coding literature without proof. As far as the platform's catalog shows, none of these results is formalized. The platform holds a machine-checkable statement of the analogous result for Gaussian arms with the Lattimore–Szepesvári threshold (BanditAlgorithm.chernoff_stopping_rule_sound, Lemma 33.7 of Bandit Algorithms), which is a different model and a different threshold. Formalizing Theorem 10 adds a proof of Lemma 11 (the KT regret bound, reusable in information theory and universal prediction), the Bernoulli GLR statistic, and a change of measure from the true bandit law to a Bayesian mixture law on the trajectory space.

Difficulty

The obvious approach bounds, for each fixed $t$ , the probability that $Z_{a,b}(t)$ exceeds $\beta(t,\delta)$ by a concentration inequality and sums over $t$ . This fails: the sampling strategy is arbitrary and adaptive, so $N_a(t)$ and $N_b(t)$ are random and depend on the past rewards, and a fixed-sample-size deviation bound does not apply; a union bound over the possible values of the counts loses more than the threshold allows. The maximum likelihood in the numerator of $Z_{a,b}$ is also not a probability density, so the likelihood ratio cannot directly be read as a change of measure. The argument must control the whole trajectory law under an arbitrary randomized policy, and must handle empty samples (an arm never pulled contributes likelihood $1$ ) and the boundary means $0$ and $1$ .

Formalization scope

The formalization is in Lean 4 with Mathlib and reuses the platform's canonical bandit model: StochasticBandit, BanditPolicy (a Markov kernel per round from the observed history to the next arm, so randomized strategies are included), banditTrajMeasure (the law of the infinite trajectory, where coordinate $s$ is round $s+1$ ) and IsSoundBAI from BanditTrajectory; bernoulliBandit from bernoulliRelativeEntropy; and only the pull counts trajPullCount and empirical means trajEmpiricalMean from TrackAndStop. The Gaussian GLR and threshold of TrackAndStop are not used.

Conventions committed to:

Arms are Fin K. Bernoulli means range over $[0,1]$ , degenerate laws included; the paper's exponential-family mean space is $(0,1)$ , so the $[0,1]$ statement implies the paper's.
$Z_{a,b}(t)$ is defined as the ratio of the two maxima over $[0,1]^2$ , not by the closed form (7), which holds only when $\hat\mu_a(t) \ge \hat\mu_b(t)$ . Both maxima are attained and positive.
The stopping rule ranges over $t \ge 1$ ; at $t = 0$ there is no observation and the paper's $\beta(0,\delta) = \log 0$ is undefined. $\tau_\delta = \infty$ when the rule never fires.
The decision rule is quantified: the goal holds for every recommendation that maximizes the empirical mean at $\tau_\delta$ , whatever the tie-breaking.
Probabilities of events are outer measures under the trajectory law; no measurability is assumed.
$K \ge 1$ only. For $K = 1$ the statement is trivially true (no suboptimal arm).

Disclosed deviations from the page: Lemma 11's ratio bound is stated for $n \ge 1$ , since at $n = 0$ the printed bound reads $1 \le 0$ ; the use of the lemma in Appendix C.1 is unaffected. Appendix C.1 calls the result "Proposition 10" (a slip for Theorem 10) and prints the KT density as $1/\sqrt{\pi u(1-u)}$ (a slip for $1/(\pi\sqrt{u(1-u)})$ of Lemma 11, which is the normalized one); the formalization follows Lemma 11.

A trivializing formalization is ruled out: stating the result for Gaussian arms or with the Lattimore–Szepesvári threshold is the platform's existing Lemma 33.7 and is not Theorem 10, and a free decision rule without the argmax hypothesis would make the claim false rather than faithful.

Contributions welcome: a proof of Lemma 11; a change-of-measure lemma for banditTrajMeasure under a mixture of environments; and the union-bound reduction from the goal to the pairwise claim.

Selected references

A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2, 2016. https://arxiv.org/abs/1602.04589
F. M. J. Willems, Y. M. Shtarkov, T. J. Tjalkens, The context-tree weighting method: basic properties, IEEE Transactions on Information Theory 41(3), 1995. https://doi.org/10.1109/18.382012
R. Krichevsky, V. Trofimov, The performance of universal encoding, IEEE Transactions on Information Theory 27(2), 1981. https://doi.org/10.1109/TIT.1981.1056331
H. Chernoff, Sequential design of experiments, Annals of Mathematical Statistics 30(3), 1959. https://doi.org/10.1214/aoms/1177706205
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 33. https://doi.org/10.1017/9781108571401

10 thms4 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities III: Uniform Convergence and the Entropy per ObservationResearch Paper

Motivation

Estimating a probability by the relative frequency of the event in an independent sample is justified for one event by the law of large numbers. Statistics and learning theory need more: the frequencies of a whole class of events $S$ must approach their probabilities simultaneously, so that a quantity chosen after looking at the data (the empirical risk minimizer, the empirical distribution function) is still close to its expectation. Glivenko's theorem on the empirical distribution function is the classical instance; empirical risk minimization rests on the same property for the class of loss sets of a model.

Vapnik and Chervonenkis, On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities, Theory Probab. Appl. 16 (1971), treat this question in two parts. The first gives a distribution-free sufficient condition through the growth function (Theorems 1–3). The second, which this mission formalizes, gives a condition that is necessary and sufficient for a fixed distribution: Theorem 4, the entropy criterion.

Timeline. 1933: Glivenko and Cantelli prove uniform convergence for the class of rays $\{x \le a\}$ on the line. 1968: Vapnik and Chervonenkis announce the results in Dokl. Akad. Nauk SSSR 181. 1971: the full paper appears, with the growth-function bound and the entropy criterion. Later work (Talagrand 1987; Dudley, Giné and Zinn 1991) recasts such criteria as the theory of Glivenko–Cantelli classes.

Setting

Let $X$ be a set carrying a probability measure $P$ , and $S$ a collection of measurable subsets of $X$ (events). A sample of size $l$ is a sequence $x_1, \dots, x_l$ of independent draws from $P$ ; repetitions are allowed. For $A \in S$ the relative frequency $\nu_A^{(l)}$ is the fraction of sample terms lying in $A$ , and $P_A = P(A)$ . The maximal deviation is

\pi^{(l)}(x_1, \dots, x_l) = \sup_{A \in S} \bigl|\nu_A^{(l)} - P_A\bigr| .

The relative frequencies converge in probability to the probabilities uniformly over $S$ when $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \to 0$ as $l \to \infty$ for every $\varepsilon > 0$ .

Each $A \in S$ induces in a sample the subsample of terms lying in $A$ . The index $\Delta^S(x_1, \dots, x_l)$ is the number of different subsamples induced by the sets of $S$ ; it lies between $0$ and $2^l$ . The entropy of $S$ in samples of size $l$ is

H^S(l) = \mathbf{E} \log_2 \Delta^S(x_1, \dots, x_l) .

For a sample of size $2l$ , split into halves $x_1, \dots, x_l$ and $x_{l+1}, \dots, x_{2l}$ with relative frequencies $\nu'_A$ and $\nu''_A$ , the semi-sample deviation is $\rho^{(l)} = \sup_{A \in S} |\nu'_A - \nu''_A|$ . Finally $\Phi(n, r)$ is defined by the recurrence $\Phi(n, r) = \Phi(n, r-1) + \Phi(n-1, r-1)$ , $\Phi(0, r) = \Phi(n, 0) = 1$ .

Formalization targets

Goal: Theorem 4 (p. 275)

\Bigl(\forall \varepsilon > 0:\ \lim_{l\to\infty} \mathbf{P}\{\pi^{(l)} > \varepsilon\} = 0\Bigr) \iff \lim_{l \to \infty} \frac{H^S(l)}{l} = 0 .

Milestones

Entropy rate. (12) $\Delta^S(x_1, \dots, x_l) \le \Delta^S(x_1, \dots, x_k)\Delta^S(x_{k+1}, \dots, x_l)$ ; the subadditivity $H^S(l_1 + l_2) \le H^S(l_1) + H^S(l_2)$ ; Lemma 3, $H^S(l)/l \to c \in [0, 1]$ ; Lemma 4, $\mathbf{P}(|l^{-1}\log_2 \Delta^S - c| > \varepsilon) \to 0$ .
Sufficiency. Lemma 2, $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \le 2\,\mathbf{P}\{\rho^{(l)} \ge \varepsilon/2\}$ for $l \ge 2/\varepsilon^2$ ; the per-sample permutation bound $2\Delta^S(x_1, \dots, x_{2l}) e^{-\varepsilon^2 l/8}$ ; and

\mathbf{P}\{\rho^{(l)} \ge \tfrac{\varepsilon}{2}\} \le 2\Bigl(\frac{2}{e}\Bigr)^{\varepsilon^2 l/8} + \mathbf{P}\Bigl\{\tfrac{1}{2l}\log_2 \Delta^S(x_1, \dots, x_{2l}) > \tfrac{\varepsilon^2}{16}\Bigr\} .

Necessity. Lemma 1 (Sauer–Shelah in sequence form); step 1°, $1 - \mathbf{P}(C') \ge (1 - \mathbf{P}(Q))^2$ with $C' = \{\rho^{(l)} > 2\varepsilon\}$ ; (26), $\mathbf{P}\{\Delta^S > \Phi([ql], l)\} \to 1$ when $0 < q < \frac14$ and $q\log_2(2e/q) < c$ ; and (29), $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \to 1$ when moreover $0 < \varepsilon < q/7$ .

Significance

Theorem 4 characterizes uniform convergence for a given distribution exactly, with no gap between the necessary and the sufficient condition. It separates the cases the growth-function bound cannot: a class may have $m^S(l) = 2^l$ for every $l$ (all open subsets of $[0,1]$ ) and still satisfy $H^S(l)/l \to 0$ under a particular $P$ , or fail it. The entropy $H^S(l)$ is the distribution-dependent quantity from which later work on Glivenko–Cantelli classes and on consistency of empirical risk minimization proceeds; the 1981 paper of the same authors extends the criterion to classes of functions. The quantitative form (29) states more than the negation of convergence: when the entropy rate is positive, the maximal deviation stays above a fixed $\varepsilon$ with probability tending to one.

The result has been proved since 1971; it has not been formalized. The platform holds Sauer–Shelah variants over sets of distinct points and PAC bounds with other constants, but no statement of the VC entropy or of Theorem 4. The mission produces machine-checked statements of the entropy criterion and of its supporting lemmas with the paper's own constants ( $l \ge 2/\varepsilon^2$ , $2e^{-\varepsilon^2 l/8}$ , $\delta = \varepsilon^2/16$ , $\varepsilon < q/7$ ).

Difficulty

The sufficiency half is a variant of the proof of the growth-function bound; its new ingredient is the concentration of $l^{-1} \log_2 \Delta^S$ (Lemma 4), which needs subadditivity and a law of large numbers over independent blocks of the sample rather than a single mean estimate. The hypergeometric tail estimate behind the permutation bound is omitted in the paper ("a simple but long computation").

Necessity is harder. The obvious attempt, bounding $\mathbf{P}\{\pi^{(l)} > \varepsilon\}$ from below by exhibiting a single bad event, fails: $S$ may be uncountable and no single $A$ deviates with non-vanishing probability. A positive entropy rate has to be converted into a combinatorial statement about typical samples ((26) combines Lemma 4 with an estimate of $\Phi([ql], l)$ ), and that statement back into a lower bound on a probability over the product measure; the constants $q < \frac14$ and $\varepsilon < q/7$ must be tracked through both conversions, and the conclusion $\lim \mathbf{P}\{\pi^{(l)} > \varepsilon\} = 1$ needs the unweakened inequality of step 1°.

Formalization scope

A sample of size $l$ is a function Fin l → X (positions $0, \dots, l-1$ ) and its law is the product measure Measure.pi (fun _ => P), with P a probability measure. A subsample is a set of positions, so the index counts distinct Finset (Fin l) of the form $\{i : x_i \in A\}$ . The halves of x : Fin (l + l) → X are x ∘ Fin.castAdd l and x ∘ Fin.natAdd l. $P_A$ is P.real A; the suprema $\pi^{(l)}$ and $\rho^{(l)}$ are real suprema over the subtype of $S$ (values in $[0,1]$ ; $0$ for $S = \emptyset$ ). $H^S(l)$ is a Bochner integral of Real.logb 2 of the index, and $[ql]$ is ⌊q * l⌋₊. Probabilities are values in $[0, \infty]$ , except in the inequalities between probabilities (step 1°, the sufficiency estimate), which use Measure.real.

Measurability. The paper assumes, and the statements carry as hypotheses, that the events of $S$ are measurable (p. 264), that $\pi^{(l)}$ is a random variable (p. 265), that $\rho^{(l)}$ is measurable (p. 268), and that the index is measurable in the sample (p. 273). Each statement carries the ones its proof uses. Without them the Bochner integral defining $H^S(l)$ can be the junk value $0$ and the equivalence can fail; replacing them by " $S$ countable" would weaken the theorem. The goal is not trivialized by degenerate cases: the equivalence is not vacuous for any class, and $S = \emptyset$ gives the true instance $H^S = 0$ , $\pi^{(l)} = 0$ .

Corrections of the printed text. Lemma 2 is printed for $l > 2/\varepsilon^2$ ; its proof gives $l \ge 2/\varepsilon^2$ , which is stated. On p. 275 Lemma 2 is recalled as " $2\mathbf{P}(C) \ge \frac12 P(Q)$ ", meaning $\mathbf{P}(C) \ge \frac12\mathbf{P}(Q)$ . On p. 276 the first display carries a stray upper limit "4" on the integral, and the region of integration is printed $\{\log_2 \Delta^S \le 2\delta\}$ where $\{\log_2\Delta^S \le 2\delta l\}$ is meant. The event $C'$ is defined with " $> 2\varepsilon$ " (p. 276) but integrated in step 3° as $\theta(\cdot - 2\varepsilon)$ , which counts " $\ge 2\varepsilon$ "; the strict form is stated, and the estimate of step 3° is itself strict. Step 1° is stated unweakened. Milestone texts are verbatim.

Contributions welcome: a reusable development of the index and its submultiplicativity, the hypergeometric tail bound for sampling without replacement, a block law of large numbers for subadditive functionals of i.i.d. samples, and the permutation-invariance argument for product measures on Fin (l + l) → X.

Selected references

V. N. Vapnik and A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and Its Applications 16(2) (1971), 264–280. https://doi.org/10.1137/1116025
V. N. Vapnik and A. Ya. Chervonenkis, Necessary and sufficient conditions for the uniform convergence of means to their expectations, Theory of Probability and Its Applications 26(3) (1981), 532–553. https://doi.org/10.1137/1126059
M. Talagrand, The Glivenko–Cantelli problem, Annals of Probability 15(3) (1987), 837–870. https://doi.org/10.1214/aop/1176992069
R. M. Dudley, E. Giné and J. Zinn, Uniform and universal Glivenko–Cantelli classes, Journal of Theoretical Probability 4(3) (1991), 485–510. https://doi.org/10.1007/BF01210321

16 thms4 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXVII: Directional Derivatives and Quasi L-Convex FunctionsTextbook

Motivation

This mission completes chapter 7's L-convex function theory and closes the book on it. It first finishes the theory of positively homogeneous L-convex functions — showing they coincide exactly with the classical Lovász extensions of submodular set functions, a one-to-one correspondence that recognizes forty years of submodular-optimization machinery as a special case of L-convex function theory. It then proves the L-side capstone this series has been building toward since mission 26-ch07b-lconvexfunctions: polyhedral L-convexity is characterized simultaneously by directional derivatives, subdifferentials, and weighted-minimizer polyhedra — the exact mirror of what mission 24-ch06d-mconvexfunctions proved for M-convex functions. Finally it develops quasi L-convex functions, the L-side analogue of mission 25-ch06e-mconvexfunctions's quasi M-convex functions, ending exactly where chapter 7 itself ends.

Setting

Fix a finite ground set $V$ . The class $0L[\mathbb R \to \mathbb R]$ consists of polyhedral L-convex functions that are positively homogeneous; $0L[\mathbb Z \to \mathbb Z]$ , its integer-valued integer-domain analogue. A positively homogeneous L-convex function $g$ induces a submodular set function $\rho_g(X) = g(\chi_X)$ ; conversely the Lovász extension $\hat\rho$ of a submodular set function is positively homogeneous L-convex. The base polyhedron $B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ \forall X,\ x(V) = \rho(V)\}$ of a submodular $\rho$ is always an M-convex polyhedron. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is quasi submodular (QSB) if $g(p\wedge q) \le g(p)$ or $g(p\vee q) \le g(q)$ for all $p,q$ ; the weaker (QSBw) requires only $\max\{g(p),g(q)\} \ge \min\{g(p\wedge q), g(p\vee q)\}$ .

Formalization targets

Goal: the four characterizations of polyhedral L-convexity (Theorem 7.45)

For a polyhedral convex function $g$ with $\operatorname{dom}_{\mathbb R} g \ne \emptyset$ : $g$ is L-convex if and only if every directional derivative $g'(p;\cdot)$ is $0L[\mathbb R \to \mathbb R]$ , if and only if every subdifferential $\partial_{\mathbb R} g(p)$ is an M-convex polyhedron, if and only if every weighted minimizer set is an L-convex polyhedron. Not present in this chunk's own extraction table (its label opens mid-paragraph, missed by the same extractor failure already documented for mission 25-ch06e-mconvexfunctions's Theorem 6.68), found by direct reading and chosen as goal because it is the exact L-side mirror of mission 24-ch06d-mconvexfunctions's own milestone Theorem 6.63, and its proof is assembled entirely from results already in this series (Theorem 7.43, Proposition 7.34, Theorem 7.40).

Supporting structural targets

Fifteen further results build the two remaining pieces of chapter 7's theory. Propositions 7.37-7.39 and Theorem 7.40 establish the one-to-one correspondence between positively homogeneous L-convex functions and submodular set functions via the Lovász extension; Proposition 7.41 gives a minimizer-polyhedron characterization of this class, and Proposition 7.42 shows directional derivatives of L-convex functions automatically land in it. Theorem 7.43 — the L-side mirror of mission 24-ch06d-mconvexfunctions's own goal, Theorem 6.61 — proves the directional- derivative/subdifferential correspondence via the induced submodular set function's base polyhedron; Proposition 7.44 checks consistency at integer points, and Theorem 7.46 refines Theorem 7.45 to the integral case. Theorem 7.49 (also missed by the extractor) gives the quasi-submodularity implication hierarchy and its perturbation-equivalence capstone, mirroring mission 25-ch06e-mconvexfunctions's Theorem 6.68 exactly. Proposition 7.50 and Theorems 7.51-7.52 build the level-set/perturbation machinery quasi submodularity needs; Theorems 7.53-7.54 (both missed by the extractor, the latter's full statement requiring one page beyond this chunk's nominal range, at the very end of chapter 7) give the quasi L-optimality and quasi L-proximity theorems.

Significance

The 0L/submodular correspondence (Theorem 7.40) is the precise sense in which L-convex function theory generalizes submodular set function theory rather than merely resembling it: every submodular set function is literally the restriction to $\{0,1\}^V$ of a positively homogeneous L-convex function, and every algorithm for one transfers to the other through this exact dictionary. The goal, Theorem 7.45, completes the parallel structure this series has built since chapter 6: M-convexity and L-convexity are now each characterized in the same four convex-analytic vocabularies, setting up chapter 8's conjugacy theorem, which will show these two characterizations are not merely analogous but literally dual to each other under the Legendre-Fenchel transform. The quasi-submodularity results matter for the same reason as their M-side counterparts: chapter 10's algorithms for L-convex-function minimization remain correct under nonlinear rescalings that destroy L-convexity itself but preserve quasi submodularity.

None of these results are open — they are Murota's account of how far L-convex function theory extends beyond the polyhedral case (to positive homogeneity and its submodular-function incarnation) and how far its exchange-style inequality can be relaxed while preserving optimization theory (to quasi submodularity), mirroring chapter 6's identical two-part program for M-convex functions. What this mission contributes is a faithful, machine-checked formal statement of each, including four theorems (7.45, 7.49, 7.53, 7.54) the platform's own automated extractor missed entirely — one of them requiring a page beyond this chunk's own nominal range to complete, since chapter 7 ends there and this is the last mission covering it — extending the shared Lean vocabulary (ZeroLR, BasePolyhedron, QSBw) this series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to prove all six pairwise implications among its four conditions independently; the book's own proof instead chains through results already established: (a)⇒(b) is Proposition 7.42, (a)⇒(c) is Theorem 7.43, (a)⇒(d) is Proposition 7.34, (b)⇔(c) uses the 0L/M0[R] correspondence, and (d)⇒(b) is the genuinely hard direction, requiring Proposition 7.41 applied to the directional derivative itself (showing $\arg\min(g'(p;\cdot)[-x])$ is an L-convex cone by an explicit description via the admissible-potential set of the distance function underlying $\arg\min g[-x]$ ). The remaining combinatorial difficulty in this block is in Theorem 7.43's proof: identifying $\partial_{\mathbb R} g(p)$ with the base polyhedron $B(\rho_{g,p})$ requires the L-optimality criterion (Theorem 7.33, mission 27-ch07c-lconvexfunctions) applied pointwise, a chain of logical equivalences with no single-step shortcut, exactly mirroring how mission 24-ch06d-mconvexfunctions's Theorem 6.61 needed the M-optimality criterion.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-convex functions are (V→ℝ)→WithTop ℝ (polyhedral) or (V→ℤ)→WithTop ℝ (integer-domain). All sixteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus four the extractor missed (Theorems 7.45, 7.49, 7.53, 7.54) — are placed, with two documented, content-preserving scope decisions: Theorem 7.43 omits the dual-integral refinement clauses for L[R→R|Z]/L[Z→Z] (the same decision mission 24-ch06d-mconvexfunctions's Theorem 6.61 made), and Proposition 7.50 states the general inequalities without restating their "In particular" specializations, which add no independent content — see HARD.md. " $\inf g[-x]>-\infty$ " is replaced by the equivalent (ArgMinR ...).Nonempty hypothesis throughout, matching mission 25-ch06e-mconvexfunctions's identical substitution. This mission's base vocabulary is redeclared from missions 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the sixteen sorrys are welcome; the goal and Theorem 7.43 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 [152] (the polyhedral theory Theorems 7.26-7.46 are drawn from).
P. Milgrom and C. Shannon, "Monotone comparative statics," Econometrica, 62 (1994), pp. 157-180 [129] (the origin of the quasi-submodularity condition (SSQSB)).

68 thms4 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research+1·Captain: mikedeng1

Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders IV: A Truthful Value-Query Mechanism for Subadditive BiddersResearch Paper

Motivation

In a combinatorial auction a seller offers several indivisible items at once, and bidders value bundles of items rather than items one at a time. Allocating the items to maximize total value is the central optimization problem of the area, and it arises in spectrum licensing, procurement and transport contracting (Cramton, Shoham and Steinberg, Combinatorial Auctions, MIT Press, 2006). Two obstacles meet. Computationally, a valuation has $2^m$ numbers, so an algorithm can only query it, and even then optimization is hard. Strategically, the valuations are private: a bidder reports whatever maximizes its own utility, so an algorithm that is a good approximation on true inputs may be useless on reported ones.

The classical answer to the strategic obstacle is the VCG payment scheme, which makes truthful reporting a dominant strategy but requires the exact optimum. Nisan and Ronen (2007) showed that an approximation algorithm becomes truthful under VCG payments essentially only when it is maximal in range: it fixes a restricted set of allocations in advance and optimizes exactly over that set. Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010, §5) give such an algorithm for complement-free (subadditive) bidders that uses only value queries and loses a factor of order $\sqrt m$ . For general valuations in the value-query model the paper cites a lower bound of order $m/\log m$ (Dobzinski and Schapira, working paper 2005; Blumrosen and Nisan, Hebrew University Discussion Paper 381, 2005; see the paper's references [7] and [2]), and the same paper (Theorem 6.1) shows that even XOS bidders cannot be approximated within $m^{1/2-\epsilon}$ with polynomially many value queries.

Setting

A set $M=\{1,\dots,m\}$ of items is sold to $n$ bidders. Bidder $i$ has a valuation $v_i$ that assigns a real number $v_i(S)$ to every bundle $S\subseteq M$ . Throughout, valuations are normalized, $v_i(\emptyset)=0$ , and monotone, $S\subseteq T\Rightarrow v_i(S)\le v_i(T)$ . A valuation is complement free (CF) if $v(S\cup T)\le v(S)+v(T)$ for all bundles $S,T$ . An allocation $A=(A_1,\dots,A_n)$ gives the bidders pairwise disjoint bundles (items may stay unallocated), and its social welfare is $\sum_i v_i(A_i)$ .

The mechanism receives reports $b=(b_1,\dots,b_n)$ and runs the following algorithm $\mathrm{ALG}$ :

query $b_i(M)$ and $b_i(\{j\})$ for every bidder $i$ and item $j$ ;
compute a maximum-weight matching $P$ in the complete bipartite graph between items and bidders, where the edge between item $j$ and bidder $i$ costs $b_i(\{j\})$ ;
if the bidder $t$ maximizing $b_i(M)$ has $b_t(M)$ strictly larger than the weight $|P|$ , give all items to $t$ ; otherwise give every item matched by $P$ to its matched bidder.

Its range $R$ is the set of allocations that give all of $M$ to one bidder, together with the allocations in which every bidder receives at most one item. Under VCG payments bidder $i$ receives $\sum_{k\ne i}b_k(\mathrm{ALG}(b)_k)$ , so its utility is $v_i(\mathrm{ALG}(b)_i)+\sum_{k\ne i}b_k(\mathrm{ALG}(b)_k)$ . The mechanism is incentive compatible on a class of valuations if no bidder can raise its utility by misreporting within that class, whatever the others report.

Formalization targets

Goal: Theorem 5.1 (p. 11)

For every choice of the maximum-weight matching and of the top bidder as functions of the reports, for every profile $v$ of normalized, monotone, CF valuations and every allocation $O$ ,

\sum_{i=1}^n v_i(O_i)\;\le\;2\sqrt m\,\sum_{i=1}^n v_i\big(\mathrm{ALG}(v)_i\big),

and the mechanism $(\mathrm{ALG},\text{VCG payments})$ is incentive compatible on the CF valuations.

Milestones, in attack order

§5.1, VCG. Welfare maximization with Groves payments is incentive compatible (a published platform theorem, AGT.vcg_incentive_compatible).
§5.1, maximal in range. Any allocation rule that optimizes reported welfare exactly over a fixed range is incentive compatible under VCG payments on the same domain.
ALG is maximal in range with range $R$ on normalized reports.
The CF single-item bound. For a CF valuation and $c\in T$ maximizing $v(\{j\})$ over $T$ : $v(T)\le\sum_{j\in T}v(\{j\})\le|T|\,v(\{c\})$ .
First case. If bidders with $|O_i|\ge\sqrt m$ carry at least half the welfare of $O$ , then $\sum_i v_i(O_i)\le 2\sqrt m\,v_t(M)$ for the top bidder $t$ .
Second case. Otherwise some allocation in which every bidder gets at most one item has welfare at least $\sum_i v_i(O_i)/(2\sqrt m)$ .

Significance

The theorem shows that, for subadditive bidders, the $\sqrt m$ barrier known for general valuations can be matched by a truthful mechanism that asks each bidder only $m+1$ value queries. It is one of the early examples of maximal-in-range mechanism design, a template later used for many truthful approximation mechanisms in combinatorial auctions, and it sits against Theorem 6.1 of the same paper, which shows that for XOS bidders no value-query algorithm with polynomially many queries does better than $m^{1/2-\epsilon}$ .

The result is proved in the paper. What this mission adds is a machine-checked proof: a formal model of VCG-based mechanisms over a restricted range, a proof that the §5.2 algorithm is maximal in range for every tie-breaking of its two optimization steps, and the explicit constant $2$ in the $O(\sqrt m)$ bound. To our knowledge neither half of Theorem 5.1 is formalized elsewhere; the general VCG theorem exists on the platform in the setting of arbitrary outcome sets.

Difficulty

The approximation argument partitions the bidders of a reference allocation by whether their bundles have at least $\sqrt m$ items, and the two cases need different facts: disjointness bounds the number of large bundles by $\sqrt m$ , and subadditivity bounds each small bundle by its size times its best item. A naive transcription breaks at degenerate inputs: the page divides by $|T_i|$ and writes strict inequalities, both of which fail when a bundle is empty or all values are zero, so the formal statement must be organized around non-strict bounds.

Incentive compatibility has a different obstacle. It holds only if the allocation rule depends on the reports alone and optimizes exactly over its range, including at ties between the grand bundle and the matching. The matching and the top bidder are not unique, so the proof must work for an arbitrary but fixed tie-breaking, and the welfare of the matching allocation must be identified with the matching weight, which uses normalization of every bidder who receives nothing.

Formalization scope

Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity (the paper's standing assumptions, p. 1) and complement freedom are hypotheses; IsCFValuation bundles all three. An allocation is a family of pairwise disjoint bundles; unallocated items are allowed. A matching is a partial map Fin m → Option (Fin n) with no bidder matched twice.

Conventions the formalization commits to:

Explicit constant. The paper writes $O(\sqrt m)$ ; its proof yields $2\sqrt m$ (both cases end with $|OPT|/(2\sqrt m)$ ), and the goal states $2\sqrt m$ with Real.sqrt m.
Oracles and ties. The maximum-weight matching and the top bidder enter as functions mat, top of the report profile, each with a specification hypothesis; the goal is stated for every such pair. The algorithm reads only the reports; the tie between $b_t(M)$ and $|P|$ goes to the matching, as on the page.
Payments. The mechanism pays each bidder $\sum_{k\ne i}b_k(\cdot)$ , the paper's convention (footnote 2, p. 11); incentive compatibility is stated on the CF domain, the paper's. The local definition mirrors AGT.MechIncentiveCompatible on outcomes $a\mapsto v_i(a_i)$ .
Reference allocation. The approximation is stated against every allocation $O$ , not only an optimal one; this is equivalent and avoids a junk maximum.
Printed slips. The strict inequalities and the division by $|T_i|$ in the second case are replaced by non-strict, multiplied forms; the first case concludes for a bidder maximizing $v_i(M)$ rather than $v_i(O_i)$ .
Degenerate sizes. At $m=0$ everything is zero and the bound holds trivially; with $n=0$ no top-bidder rule exists.
Out of scope. "In polynomial time" is a running-time claim and is not modelled.

A trivializing formalization is ruled out: the ratio is the explicit $2\sqrt m$ rather than an existential constant, incentive compatibility is over the full CF domain (not additive reports only) for a rule that cannot see true valuations, and the rules mat, top are satisfiable (a maximum over the finitely many matchings exists; a top bidder exists when $n\ge1$ ).

Useful infrastructure: finite maximum-weight matchings on complete bipartite graphs, subadditivity bounds over Finset sums, and a reusable lemma that maximal-in-range rules with VCG payments are truthful. Contributions of any milestone are welcome; milestones 2 and 4 are self-contained.

Selected references

S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
N. Nisan, A. Ronen, Computationally Feasible VCG Mechanisms, Journal of Artificial Intelligence Research 29:19–47, 2007. https://doi.org/10.1613/jair.2046
S. Dobzinski, M. Schapira, Optimal Upper and Lower Approximation Bounds for k-Duplicates Combinatorial Auctions, working paper, The Hebrew University of Jerusalem, 2005 (reference [7] of the paper).
L. Blumrosen, N. Nisan, On the Computational Power of Iterative Auctions I: Demand Queries, Discussion Paper 381, Center for the Study of Rationality, The Hebrew University of Jerusalem, 2005 (reference [2] of the paper).
N. Nisan, Introduction to Mechanism Design (for Computer Scientists), in N. Nisan, T. Roughgarden, E. Tardos, V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, pp. 209–242.
P. Cramton, Y. Shoham, R. Steinberg (eds.), Combinatorial Auctions, MIT Press, 2006.

8 thms4 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXIV: Quasi M-Convex FunctionsTextbook

Motivation

Every characterization of M-convexity so far in this series — the exchange axiom, the optimality criterion, convex extensibility, the directional-derivative/subdifferential correspondence — has been an equivalence with M-convexity itself: a function either is M-convex or it is not. Section 6.14 asks a different question: what happens when the exchange axiom's defining inequality is relaxed to only the sign patterns it actually forces? The answer is a hierarchy of "quasi M-convex" conditions — weaker than M-convexity, strong enough to keep the optimality criterion and the proximity/minimizer-cut theorems intact — and, at the top of that hierarchy, a genuinely new characterization of M-convexity itself: a function is M-convex if and only if every one of its linear perturbations is quasi M-convex in the weakest sense. This mission formalizes that entire hierarchy and its capstone, plus two further characterizations of polyhedral M-convexity (via directional derivatives, subdifferentials, and weighted-minimizer polyhedra) that complete the real-variable theory chunk 24-ch06d-mconvexfunctions began.

Setting

Fix a finite ground set $V$ and $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ . Write $\Delta f(z;v,u) = f(z + \chi_v - \chi_u) - f(z)$ . Relaxing the exchange axiom's inequality $\Delta f(x;v,u) + \Delta f(y;u,v) \le 0$ to the sign patterns it forces gives quasi M-convexity (QM) and semistrict quasi M-convexity (SSQM), and requiring only some pair $(u,v)$ rather than every $u$ gives their weaker variants (QMw), (SSQMw); the minimization-only variants (SSQM $\ne$ ), (SSQM $\ne_w$ ) replace " $x,y \in \operatorname{dom} f$ " with " $f(x) \ne f(y)$ ". The set-level analogue (Q-EXC)/(Q-EXCw) relaxes the M-convex-set exchange axiom the same way. For $\alpha \in \mathbb R$ , the level set $L(f,\alpha) = \{x \in \mathbb Z^V : f(x) \le \alpha\}$ . A polyhedral convex function $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (real-variable) M-convex, $f \in M[\mathbb R \to \mathbb R]$ , if it satisfies the real exchange axiom (M-EXC[R]) from chunk 24-ch06d-mconvexfunctions; $L_0[\mathbb R]$ denotes polyhedra realized as $D(\gamma)$ for a triangle-inequality distance function $\gamma$ , and $M_0[\mathbb R]$ denotes real M-convex polyhedral cones.

Formalization targets

Goal: the quasi M-convexity hierarchy (Theorem 6.68)

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ : (1) the implication diagram (M-EXC[Z]) $\Rightarrow$ (SSQM) $\Rightarrow$ (QM), (M-EXCw[Z]) $\Rightarrow$ (SSQMw) $\Rightarrow$ (QMw), (M-EXC[Z]) $\Leftrightarrow$ (M-EXCw[Z]), (SSQM) $\Rightarrow$ (SSQMw), (QM) $\Rightarrow$ (QMw); (2) $f$ satisfies (M-EXC[Z]) if and only if $f[p]$ satisfies (QMw) for every $p \in \mathbb R^V$ . This theorem is not named in the chunk's own extraction table — the automated extractor, which requires a result's label to start a text line, misses it because it opens mid-paragraph directly after an ASCII-rendered implication diagram — but it is the capstone of the section: its own proof is "combining Theorems 6.72 and 6.74," both formalized here as milestones, and part (2) answers exactly the question a reader of this stretch would ask: what does the entire apparatus of quasi M-convexity ultimately say about M-convexity itself?

Supporting structural targets

Fourteen further results build the hierarchy and complete the real-variable theory. Proposition 6.62 checks the two halves of chunk 24-ch06d-mconvexfunctions's Theorem 6.61 agree at integer points. Theorems 6.63–6.64 add two more characterizations of polyhedral M-convexity — via positively homogeneous directional derivatives and $L_0[\mathbb R]$ -valued subdifferentials, and via $M_0[\mathbb R]$ / $M_0[\mathbb Z|\mathbb R]$ -valued weighted-minimizer polyhedra — to the convex-extensibility characterization chunk 23-ch06c-mconvexfunctions proved. Theorem 6.67 gives two equivalent reformulations of (QMw) as pointwise inequalities; Propositions 6.69–6.70 and Theorems 6.72–6.74 build the level-set/perturbation machinery the goal needs. Theorem 6.75 is the (SSQM $\ne_w$ ) analogue of Theorem 6.67. Theorem 6.76 is the quasi M-optimality criterion (optimality still characterized by local non-improvement, under only the weak quasi-convexity hypotheses). Theorems 6.77–6.79 show the M-minimizer-cut and M-proximity theorems (from missions 06-mconvex-functions-i and 23-ch06c-mconvexfunctions) hold verbatim under the strictly weaker (SSQM $\ne$ ) hypothesis.

Significance

The hierarchy's practical payoff is immediate: Theorems 6.77–6.79 mean the algorithms of chapter 10 that rely on minimizer cuts and proximity bounds do not actually need the full exchange axiom to run correctly on nonlinearly rescaled M-convex functions (Example 6.66 shows any nondecreasing scaling $\phi \circ f$ of an M-convex $f$ is quasi M-convex, yet nonlinear scalings are common in practice and destroy M-convexity itself). The goal, Theorem 6.68, is significant independently: it says the exchange axiom — a condition that looks irreducibly combinatorial, quantifying over pairs of points and directions — is equivalent to a purely ordinal, perturbation-based condition (every linear tilt of $f$ has no strict local improvement that a level set can't witness), giving a genuinely different lens on why M-convexity is the right discrete analogue of convexity. Theorems 6.63–6.64 close out chunk 24-ch06d-mconvexfunctions's program of characterizing polyhedral M-convexity in every classical convex-analytic vocabulary at once (directional derivatives, subdifferentials, weighted minimizers), completing the bridge to Chapter 8's duality theory that chunk builds toward.

None of these results are open — they are Murota's account of how far the exchange axiom's defining inequality can be relaxed while keeping optimization theory intact. What this mission contributes is a faithful, machine-checked formal statement of each, including four theorems (6.68, 6.76, 6.77, 6.78) the platform's own automated extractor missed entirely, extending the shared Lean vocabulary (DeltaF, QMw, LevelSet) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to prove the implication diagram's six arrows and the perturbation equivalence as six independent facts; the book's own proof of part (2) instead derives it in one step from Theorems 6.72 and 6.74 — themselves nontrivial (Theorem 6.74's proof strengthens the local exchange axiom equivalence (Theorem 6.4) to hold whenever the domain merely satisfies (Q-EXCw), then runs a bipartite-matching argument on a 4-point neighborhood to verify the resulting local condition). The difficulty is genuinely upstream of the goal's own statement: everything the goal needs is already proved by the time Theorem 6.68 is reached, so the formalization work is in stating the sixteen distinct axioms and their level-set reformulations precisely enough that "combining 6.72 and 6.74" is literally how a Lean proof would proceed.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; integer-domain functions are (V→ℤ)→WithTop ℝ, real-domain ones (V→ℝ)→WithTop ℝ. All fifteen numbered results — including the four (6.68, 6.76, 6.77, 6.78) the automated extractor missed because their labels open mid-paragraph — are placed as milestone or goal, and every clause of every one is stated in full; no partial-coverage scope reduction was needed in this chunk (contrast chunks 22-ch06b-mconvexfunctions/24-ch06d-mconvexfunctions, which restated 4-of-8-part operations theorems). Two formalization choices are recorded in HARD.md/MODERATION_NOTES.md: " $\inf f[-p] > -\infty$ " is replaced by the equivalent (ArgMinOn ...).Nonempty hypothesis (WithTop ℝ has no $-\infty$ element), matching mission 23-ch06c-mconvexfunctions's identical substitution; and $M_0[\mathbb R]$ / $M_0[\mathbb Z|\mathbb R]$ are realized via the book's own indicator-function device rather than a freestanding cone axiom. This mission's definitions are redeclared from chunks 06-mconvex-functions-i, 22–24-ch06*-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the fifteen sorrys are welcome; the goal and Theorem 6.74 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
M. Avriel, W. E. Diewert, S. Schaible, and I. Zang, Generalized Concavity, Plenum Press, 1988 (the continuous quasi-convexity theory this chapter's discrete analogue generalizes).

56 thms4 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research+2·Captain: mikedeng1

Dual Stochastic Dominance and Related Mean-Risk Models 2: Mean–Gini Optimal Portfolios Exist and Are SSD-EfficientResearch Paper

Motivation

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

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

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

Setting

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

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

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

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

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

The optimization problem is

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

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

Formalization targets

Goal: Theorem 5.3

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

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

Milestones

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

Companion: Theorem 5.4

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

10 thms4 active usersReviewed

Completed

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

Robust Control of Markov Decision Processes with Uncertain Transition Matrices 2: The Robust Bellman Recursion for Discounted Infinite-Horizon MDPsResearch Paper

Motivation

A Markov decision process (MDP) is solved by dynamic programming only when its transition probabilities are known. In practice they are estimated from data, and the optimal policy of the estimated model can perform badly on the true one. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) showed that, when the uncertainty on the transition matrices has a product ("rectangular") structure, the robust problem, in which the controller minimises the worst expected cost over all admissible transition matrices, keeps the structure of dynamic programming. The robust Bellman operator replaces the expectation of the next-stage value by a support function of the uncertainty set. That operator is the basis of later work on robust MDPs and robust reinforcement learning.

Timeline:

Bagnell, Ng and Schneider (2001) considered the max–min value $\psi_\infty(\Pi, \mathcal T)$ and stated without proof that it is computed by the recursion below.
Iyengar (Math. Oper. Res. 30(2), 2005; technical report 2003) independently proved the robust Bellman recursion for the discounted infinite-horizon case.
Nilim and El Ghaoui (2005), Theorem 3, prove the recursion and perfect duality of the stationary discounted game. This mission formalizes that theorem.

Setting

The state space is $\mathcal X = \{1,\dots,n\}$ and the action set $\mathcal A$ is finite and nonempty. Each state–action pair has a cost $c(i,a) \ge 0$ , and costs are discounted by a factor $\nu \in [0,1)$ : the cost at stage $t$ is $\nu^t c(i,a)$ .

Write $\Delta_n = \{p \in \mathbb R^n_+ : p^T\mathbf 1 = 1\}$ for the probability simplex. For each action $a$ and state $i$ a nonempty set $\mathcal P_i^a \subseteq \Delta_n$ is given. It is the set of distributions of the next state that nature may use from state $i$ under action $a$ . No convexity or closedness is assumed. Uncertainty is rectangular: the admissible transition matrices for action $a$ form the product $\mathcal P^a = \mathcal P_1^a \times \cdots \times \mathcal P_n^a$ , so every row is chosen independently.

A stationary control policy $\pi = (\mathbf a, \mathbf a, \dots)$ applies one decision rule $\mathbf a : \mathcal X \to \mathcal A$ at every stage; $\Pi_s$ is the set of them. A stationary policy of nature $\tau \in \mathcal T_s$ fixes one matrix $P^a \in \mathcal P^a$ for each action and uses it forever. Nature chooses after the controller.

From an initial state $i_0$ , the state distribution evolves as $\mu_0 = e_{i_0}$ , $\mu_{t+1}(j) = \sum_i \mu_t(i) P^{\mathbf a(i)}(i,j)$ . The discounted cost is

C_\infty(\pi,\tau) = \sum_{t\ge 0} \nu^t \sum_i \mu_t(i)\, c(i,\mathbf a(i)).

The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v) = \sup\{p^T v : p \in \mathcal P\}$ . The robust Bellman operator $g$ and, for a stationary policy $\pi$ , the robust evaluation operator $g_\pi$ act on $v \in \mathbb R^n$ by

g(v)_i = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \qquad g_\pi(v)_i = c(i,\mathbf a(i)) + \nu\,\sigma_{\mathcal P_i^{\mathbf a(i)}}(v).

The two values of the game are

\phi_\infty(\Pi_s,\mathcal T_s) = \min_{\pi\in\Pi_s}\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau), \qquad \psi_\infty(\Pi_s,\mathcal T_s) = \sup_{\tau\in\mathcal T_s}\min_{\pi\in\Pi_s} C_\infty(\pi,\tau).

Formalization targets

Goal: Theorem 3 (Robust Bellman Recursion)

There is a unique $v \in \mathbb R^n$ with $v = g(v)$ , i.e.

v(i) = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \quad i \in \mathcal X, \tag{19}

value iteration $v_{k+1} = g(v_k)$ converges to $v$ from every starting vector (20), and

\phi_\infty(\Pi_s,\mathcal T_s) = v(i_0) = \psi_\infty(\Pi_s,\mathcal T_s).

In addition, every policy that picks a minimising action in (19) is optimal (21), every nature policy whose rows attain $\sigma_{\mathcal P_i^a}(v)$ is optimal for nature (22), and for each stationary $\pi$ the worst-case cost $\sup_\tau C_\infty(\pi,\tau)$ is $v^\pi(i_0)$ , where $v^\pi$ is the unique fixed point of $g_\pi$ (23).

Milestones

Lemma 2 (corrected): for a nondecreasing sup-norm contraction $g$ and $q \ge 0$ , the program $\max q^T v$ s.t. $v \le g(v)$ has value $q^T v_\infty$ at the fixed point $v_\infty$ , every feasible $v$ satisfies $v \le v_\infty$ , and $v_\infty$ is the unique optimizer when $q > 0$ .
The operators $g$ of (29) and $g_\pi$ of (30) are nondecreasing and $\nu$ -Lipschitz in $\|\cdot\|_\infty$ .
(26): $C_\infty(\pi,\tau) = \max\{v(i_0) : v(i) \le c(i,\mathbf a(i)) + \nu \sum_j P^{\mathbf a(i)}(i,j) v(j)\}$ .
(28) ⇒ (23): $\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau) = v^\pi(i_0)$ .
(27) ⇒ (19): $\psi_\infty(\Pi_s,\mathcal T_s) = v(i_0)$ .

Significance

The theorem makes the robust discounted problem as tractable as the nominal one. The optimal robust policy is stationary, deterministic and computed by value iteration. Each iteration evaluates one support function per state–action pair, and the paper computes these efficiently for likelihood and entropy uncertainty sets (§§5–6). Perfect duality means that the order of play does not change the value: announcing the policy to an adversarial nature costs nothing. The sequel in this series (Theorem 4) uses Theorem 3 to show that restricting to stationary policies loses nothing.

The result is proved in the paper and, independently, by Iyengar (2005). No machine-checked proof of it is known to exist. Mathlib provides the Banach fixed-point theorem, but it has no MDP library, no discounted cost along a Markov chain and no robust Bellman operator. The mission produces that layer.

Difficulty

The fixed-point half is a direct application of the Banach fixed-point theorem once the $\nu$ -contraction is established. The substance is the link between the fixed point and the probabilistic cost, and the duality.

$C_\infty(\pi,\tau)$ is an infinite series along a Markov chain. Identifying it with the solution of a linear system requires summing a matrix geometric series.
Nature's sets are neither closed nor convex, so its maxima are suprema that need not be attained. The worst case over $\mathcal T_s$ must be approached by rows that nearly attain the support function, with an error controlled through the contraction.
The min–max and max–min values are taken over different information structures. Equality has to come from the fixed point, not from a minimax theorem: the policy set is finite and discrete and nature's set is not convex, so no convexity argument applies.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ, with the componentwise order and Mathlib's sup metric, which is $\|\cdot\|_\infty$ .
The model (RobustMDP.Discounted.Model) carries the costs, the discount $\nu \in [0,1)$ (the range printed in Theorem 3; §4 prints $(0,1)$ ) and the row sets. The row sets are assumed nonempty and contained in $\Delta_n$ and nothing else. Nonemptiness is implicit in the paper.
$\Pi_s$ is Fin n → A. $\mathcal T_s$ is the subtype of A → Fin n → Fin n → ℝ whose rows lie in the row sets, which encodes rectangularity.
$C_\infty$ is a tsum of the discounted stage costs along the forward state distribution. The terms are nonnegative and at most $\nu^t\max c$ , so the series is summable and the tsum is the limit of the $N$ -stage costs, the paper's definition.
$\sigma_{\mathcal P}$ is a real sSup. It is the genuine supremum because every set it is applied to is nonempty and inside $\Delta_n$ .
Every "max" over nature is a supremum: IsLUB, or ⨆ inside $\min_\pi\sup_\tau$ , whose inner sets are shown bounded by conclusion (23). Minima over the finite $\Pi_s$ and over $\mathcal A$ are ⨅ and Finset.inf'. The argmax rows of (22) appear only as a hypothesis on a given nature policy that attains them.
Corrected statements:
- Lemma 2 is false as printed for $q$ with zero entries, so uniqueness of the optimizer is stated only for $q > 0$ .
- In (30), $\sigma(v^\pi)$ is read as $\sigma(v)$ .
- The proof's references to "Lemma 1", "(15) and (16)" and "(14)" are read as Lemma 2, (27)–(28) and (26).
Defining $C_\infty(\pi,\tau)$ as the fixed point of $w = c_\pi + \nu P_\pi w$ would make milestone (26) a tautology and conclusion (23) nearly so. The cost here is the probabilistic series, and the fixed-point characterizations must be proved.
Welcome contributions include a reusable library of discounted Markov chain costs on finite state spaces (the geometric-series identity behind (26)) and support-function lemmas on the simplex (monotonicity, the bound $\sigma_{\mathcal P}(u) - \sigma_{\mathcal P}(v) \le \|u-v\|_\infty$ ). Both are needed by the other missions of this series.

Selected references

A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
J. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-processes/
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

10 thms4 active usersReviewed

Completed

Combinatorics Convex Optimization Discrete Geometry+2·Captain: Shuze Chen

Discrete Convex Analysis XXII: Convex Extensibility of M-Convex FunctionsTextbook

Motivation

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

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

Setting

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

Formalization targets

Goal: convex extensibility characterizes M-convexity

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

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

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

Supporting structural targets

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

47 thms4 active usersReviewed

Completed

Analysis Control Theory Dynamical Systems+2·Captain: mikedeng1

Generalized Gradients and Applications II: Flow-Invariant Sets of Lipschitz Differential InclusionsResearch Paper

Motivation

A closed set $F\subseteq\mathbb R^n$ is flow-invariant for a dynamical system when every trajectory that starts in $F$ stays in $F$ . Invariance of sets underlies state constraints in optimal control, safety certificates for controlled systems, comparison and maximum principles for differential equations, and the positivity of solutions of kinetic and population models. The question is always the same: which infinitesimal condition at the points of $F$ is equivalent to the global statement that trajectories cannot leave $F$ ?

For a smooth vector field and a smooth boundary the answer is that the field must not point strictly outward. For a nonsmooth set, such as a polyhedron, the positive orthant or a set with inward cusps, "pointing inward" must be made precise through a notion of tangent vector that works at corners. Frank H. Clarke's 1975 paper introduces the generalized gradient of a Lipschitz function and derives from it a normal cone and a tangent cone for arbitrary closed sets. Its Theorem (4.4) shows that this tangent cone is exactly the right notion: for a Lipschitz differential inclusion $\dot x\in X(x)$ , a closed set is flow-invariant if and only if $X(x)$ is contained in the tangent cone at each point of the set.

Timeline:

1942. Nagumo characterizes invariance for continuous ODEs with unique solutions by a condition on the distance function (Proc. Phys.-Math. Soc. Japan 24).
1969. Bony proves an invariance theorem for Lipschitz vector fields, stated through exterior normals, in the course of a maximum principle for degenerate elliptic operators (Bony 1969).
1970. Brezis characterizes flow-invariant closed sets of a locally Lipschitz vector field by $\lim_{\delta\downarrow0} d_F(y+\delta X(y))/\delta=0$ (Brezis 1970).
1972. Redheffer gives simplified proofs of the Bony and Brezis theorems under weaker "uniqueness function" hypotheses (Amer. Math. Monthly 79, 740–747).
1975. Clarke extends the characterization to Lipschitz multifunctions with nonempty compact values, with tangency in the sense of his new tangent cone, and recovers Bony and Brezis as corollaries (Clarke 1975, Theorem (4.4), Corollaries (4.10), (4.12)).

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $\zeta\cdot v$ and norm $|\cdot|$ .

Generalized gradient. For $f:\mathbb R^n\to\mathbb R$ Lipschitz on bounded sets, $\partial f(x)$ is the convex hull of all limits $\lim_i\nabla f(x+h_i)$ with $h_i\to0$ and $f$ differentiable at each $x+h_i$ (Definition (1.1)). The generalized directional derivative is $f^\circ(x;v)=\limsup_{h\to0,\ \delta\downarrow0}[f(x+h+\delta v)-f(x+h)]/\delta$ (Definition (1.3)).

Distance function. For a nonempty closed $E\subseteq\mathbb R^n$ , $d_E(x)=\min\{|x-e|:e\in E\}$ . It is Lipschitz with constant $1$ . A point $e\in E$ with $|x-e|=d_E(x)$ is a closest point to $x$ ; it exists but need not be unique.

Normal and tangent cones. For $e\in E$ , the cone of normals is

N_E(e)=\operatorname{cl}\{p:\ s\,p\in\partial d_E(e)\text{ for some }s>0\}\qquad\text{(Definition (3.1))},

and the tangent cone is its dual,

T_E(e)=\{\zeta:\ \zeta\cdot v\le0\text{ for all }v\in N_E(e)\}\qquad\text{(Definition (3.6))}.

Differential inclusions. A multifunction $X$ assigns to each $x\in\mathbb R^n$ a set $X(x)\subseteq\mathbb R^n$ ; standing assumption of §4: every $X(x)$ is nonempty and compact. A trajectory is an absolutely continuous $x:[0,1]\to\mathbb R^n$ with $\dot x(t)\in X(x(t))$ for almost every $t$ ((4.1)). $X$ is Lipschitz if there is $K$ such that for all $x_1,x_2$ and $v_1\in X(x_1)$ some $v_2\in X(x_2)$ has $|v_1-v_2|\le K|x_1-x_2|$ ((4.2)). A closed set $F$ is flow-invariant for $X$ if every trajectory with $x(0)\in F$ has $x(t)\in F$ for all $t\in[0,1]$ ((4.3)).

Formalization targets

Goal: Theorem (4.4)

Let $X$ be a Lipschitz multifunction with nonempty compact values and $F$ a nonempty closed subset of $\mathbb R^n$ . Then

F\text{ is flow-invariant for }X\iff X(x)\subseteq T_F(x)\ \text{ for every }x\in F.

Milestones, in the order the proof uses them

Proposition (1.4). $f^\circ(x;v)=\max\{\zeta\cdot v:\zeta\in\partial f(x)\}$ for locally Lipschitz $f$ .
Proposition (2.4). If $\nabla d_E(x)$ exists and is nonzero, then $x\notin E$ , $x$ has a unique closest point $e$ , and $\nabla d_E(x)=(x-e)/|x-e|$ .
Corollary (2.5). For $e\in E$ , $\partial d_E(e)=\operatorname{co}\{0,\lim (x_i-e_i)/|x_i-e_i|\}$ over $x_i\notin E$ , $x_i\to e$ , $e_i$ closest to $x_i$ .
Proposition (3.2). $N_E(e)=\operatorname{cl}\operatorname{co}\{\lim s_i(x_i-e_i)\}$ over $s_i\ge0$ , $x_i\to e$ , $e_i$ closest to $x_i$ .
Inequality (4.8). If $X(y)\subseteq T_F(y)$ on $F$ and $x$ is a trajectory, then $f(t)=d_F(x(t))$ satisfies $f'(t)\le Kf(t)$ almost everywhere.
Limit (4.9). If $F$ is flow-invariant, then $d_F(y+\delta v)/\delta\to0$ as $\delta\downarrow0$ for every $y\in F$ and $v\in X(y)$ .
Proposition (3.7). $v\in T_E(e_0)$ iff $\lim_{e\to e_0,\,e\in E}\liminf_{\delta\downarrow0} d_E(e+\delta v)/\delta=0$ .

Significance

The result. Theorem (4.4) turns a statement about all trajectories of a set-valued dynamical system into a pointwise geometric condition on $F$ that can be checked without solving anything. It is the prototype of the strong invariance theorems of nonsmooth control theory, later developed in viability theory and in the monograph of Clarke, Ledyaev, Stern and Wolenski, and it is the tool behind state-constrained optimal control and Lyapunov-type arguments for nonsmooth systems. Its corollaries recover the Bony and Brezis theorems for Lipschitz vector fields. The companion milestones (2.5), (3.2) and (3.7) are standalone facts of nonsmooth geometry: the Clarke normal cone is generated by limits of proximal normals, and Clarke tangency can be tested along rays from nearby points of the set.

Formalizing it. The result is proved in the paper and has been reproved in textbooks; to the best of our knowledge it has no machine-checked proof. Mathlib contains Rademacher's theorem, absolutely continuous functions on intervals and the Bouligand tangent cone, but no Clarke generalized gradient, no Clarke normal or tangent cone, and no theory of differential inclusions. A complete development supplies a first nonsmooth-analysis layer on top of Mathlib and a first existence theorem for Lipschitz differential inclusions.

Difficulty

The direction (2) $\Rightarrow$ (1) looks like a Gronwall argument for $f(t)=d_F(x(t))$ , but $d_F$ is not differentiable, $x$ is only absolutely continuous, and the closest point to $x(t)$ can jump. The step that must be controlled is the comparison between $\dot x(t)$ , a nearby admissible velocity at the closest point, and the normal $x(t)-y$ ; this is where Proposition (3.2) enters, and it is why the Clarke cone, rather than a weaker cone, is needed.

The direction (1) $\Rightarrow$ (2) needs a trajectory through an arbitrary $y\in F$ whose initial velocity is a prescribed $v\in X(y)$ . For a nonconvex multifunction this is Filippov's theorem [7, Theorem 5], which the paper cites and does not prove. A solver must prove it, or an equivalent existence result for Lipschitz inclusions with compact values, from scratch in Lean. The Clarke tangent cone and the more familiar Bouligand (contingent) cone differ pointwise at nonconvex corners, so a statement written with Mathlib's tangentConeAt is a different theorem from (4.4). That the two universal conditions " $X(x)\subseteq T_F(x)$ for all $x\in F$ " are equivalent for Lipschitz $X$ is a later, separate result and cannot be assumed.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $d_E$ is Metric.infDist · E; " $e$ is a closest point to $x$ " is e ∈ E ∧ dist x e = infDist x E.
$\partial f$ and $f^\circ$ follow Definitions (1.1) and (1.3). The gradient limits carry DifferentiableAt, because Mathlib's gradient is $0$ off the differentiability set. $f^\circ$ is a real limsup, and every theorem using it carries the §1 Lipschitz hypothesis.
$N_E$ and $T_E$ are defined from $\partial d_E$ as in (3.1) and (3.6). The tangent cone is not Mathlib's tangentConeAt.
A trajectory is x : ℝ → ℝⁿ with AbsolutelyContinuousOnInterval x 0 1 and, for almost every $t\in[0,1]$ , ∃ w ∈ X (x t), HasDerivAt x w t. Values outside $[0,1]$ are irrelevant.
Standing assumptions made explicit: $X(x)$ nonempty and compact for every $x$ (§4, p. 259); $E$ , $F$ nonempty and closed and $e\in E$ (§3, p. 254); $f$ Lipschitz on bounded sets (§1, p. 247). The Lipschitz constant of (4.2) is global.
Ruled out: dropping absolute continuity (Cantor-type curves would leave $F$ ), using deriv in (4.1), using a punctured filter in (3.7), which would make (3.7)(2) hold at isolated points, and assuming Filippov's theorem as a hypothesis of (4.9) or of the goal.
Needed infrastructure: the Clarke calculus for $d_E$ , a chain-rule-type estimate for $d_F\circ x$ along absolutely continuous curves, a Gronwall lemma for absolutely continuous functions (Mathlib has norm_le_gronwallBound_of_norm_deriv_right_le for the differentiable case), and Filippov's existence theorem. The generalized gradient, cones and trajectory notions are reusable by any nonsmooth-optimization or control mission. Contributions of any of these as separate lemmas are welcome.
The §1 definitions duplicate those of the companion mission Generalized Gradients and Applications I; the two missions were drafted at the same time.

Selected references

F. H. Clarke, Generalized gradients and applications, Trans. Amer. Math. Soc. 205 (1975), 247–262. https://doi.org/10.1090/s0002-9947-1975-0367131-6
A. F. Filippov, Classical solutions of differential equations with multivalued right-hand side, SIAM J. Control 5 (1967), 609–621. https://doi.org/10.1137/0305040
H. Brezis, On a characterization of flow-invariant sets, Comm. Pure Appl. Math. 23 (1970), 261–263. https://doi.org/10.1002/cpa.3160230211
J. M. Bony, Principe du maximum, inégalité de Harnack et unicité du problème de Cauchy pour les opérateurs elliptiques dégénérés, Ann. Inst. Fourier 19 (1969), 277–304. https://doi.org/10.5802/aif.319
R. M. Redheffer, The theorems of Bony and Brezis on flow-invariant sets, Amer. Math. Monthly 79 (1972), 740–747. MR 46 #2166.
F. H. Clarke, Yu. S. Ledyaev, R. J. Stern, P. R. Wolenski, Nonsmooth Analysis and Control Theory, Graduate Texts in Mathematics 178, Springer, 1998. https://doi.org/10.1007/b97650

16 thms4 active usersReviewed

Completed

Discrete Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Elementare Theorie der konvexen Polyeder II: Finitely Many Linear Inequalities Define a Convex Polytope Iff Their Normals Positively Span and the Region Has an Interior PointResearch Paper

Motivation

A convex polytope has two standard descriptions: as the convex hull of finitely many points, and as the intersection of finitely many half-spaces. Linear programming uses both at once. The feasible region of a linear program is given by inequalities, while the simplex method and the theory of basic solutions work with its vertices. That the two descriptions define the same class of sets is the Minkowski–Weyl theorem.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv., 1935, pp. 290–306) gave an elementary, self-contained proof of this equivalence. An English translation appeared in Contributions to the Theory of Games I (Annals of Mathematics Studies 24, 1950), where it served as the polyhedral foundation for the minimax theorem and linear inequality theory in early game theory and linear programming.

Timeline:

Minkowski (1896, 1910): convex bodies, supporting planes and polyhedra in Geometrie der Zahlen, the setting Weyl's paper takes up.
Farkas (1902): the lemma on homogeneous linear inequalities that is Weyl's Satz 3.
Weyl (1935): the finite-basis theorem for cones (Hauptsatz, Satz 1), the duality between a cone and its extreme supports (§3), and the two descriptions of a convex polyhedron (§4). The paper states explicit conditions under which a finite system of inequalities defines a polytope.
Motzkin (1936), Gale, Kuhn, Tucker (1951): systematic treatments of linear inequalities built on this foundation.

Setting

Write $(a x) = a_1 x_1 + \dots + a_n x_n$ for vectors of $\mathbb{R}^n$ . A point system is a finite set $S \subseteq \mathbb{R}^n$ . It is non-degenerate if no $\alpha \neq 0$ has $(\alpha s) = 0$ for all $s \in S$ . A vector $\alpha \neq 0$ is a support of $S$ if $(\alpha s) \ge 0$ for all $s \in S$ . A support is an extreme support if equality holds at $n-1$ linearly independent points of $S$ . A point $x$ is representable by $S$ if $x = \sum_{s \in S} c_s s$ with all $c_s \ge 0$ .

Read as inequalities $(a \xi) \ge 0$ , $a \in S$ , the same $S$ defines the cone $(S)$ of solutions. An extreme solution is a nonzero $\xi \in (S)$ at which $n-1$ linearly independent inequalities of $S$ are tight. The dual system $\Sigma$ consists of the inequalities $(\alpha x) \ge 0$ , one for each extreme solution $\alpha$ , and $(\Sigma)$ is the cone it defines.

For polytopes, Weyl passes to the hyperplane $x_n = -1$ , identified with $\mathbb{R}^m$ , $m = n-1$ . A convex polyhedron is $\operatorname{conv} S$ for a finite $S \subseteq \mathbb{R}^m$ whose affine span is all of $\mathbb{R}^m$ . Given a finite index set $J$ , normals $A_j \in \mathbb{R}^m$ and constants $b_j \in \mathbb{R}$ , the inequalities $A_j \cdot x - b_j \ge 0$ cut out a region

H = \{x \in \mathbb{R}^m : A_j \cdot x - b_j \ge 0 \ \text{for all } j \in J\}.

In Weyl's notation, row $j$ is $(\alpha x) \equiv \alpha_1 x_1 + \dots + \alpha_{n-1}x_{n-1} - \alpha_n \ge 0$ , with $A_j = (\alpha_1,\dots,\alpha_{n-1})$ and $b_j = \alpha_n$ .

Formalization targets

Goal: §4 II (pp. 302–303)

Assume no row is identically zero ( $A_j \ne 0$ or $b_j \ne 0$ ). Then

H \text{ is a convex polyhedron} \iff \Big(\forall \pi' \in \mathbb{R}^m\ \exists \nu \ge 0:\ \pi' = \sum_j \nu_j A_j\Big) \ \wedge\ \Big(\exists c:\ A_j \cdot c - b_j > 0 \ \forall j\Big).

In words, the normals must positively span $\mathbb{R}^m$ and $H$ must contain an inner point. The goal is the equivalence, not either half alone.

Milestones, in the order the proof of §4 II uses them

Satz 1 (Hauptsatz), p. 291: for a non-degenerate $S$ , every $x$ with $(\alpha x) \ge 0$ for all extreme supports $\alpha$ is representable by $S$ .
Zusatz, pp. 294–295: a non-degenerate $S$ has no extreme support iff $0 = \sum_s c_s s$ with all $c_s > 0$ .
Satz 3, p. 296 (Farkas): if $(p\xi) \ge 0$ on all of $(S)$ , then $p$ is a nonnegative combination of $S$ . This milestone is the published platform theorem LinearOptimization.farkas_cone_corollary.
Satz 6, p. 297: for non-degenerate $S$ , $p \in (\Sigma)$ iff $(p\xi) \ge 0$ for all $\xi \in (S)$ .
§3 II, p. 298: for non-degenerate $S$ , every $\pi \in (S)$ is a nonnegative combination of finitely many extreme solutions.
Satz 9, p. 299: if $S$ is non-degenerate and $(S)$ has an inner point, then $\Sigma$ is non-degenerate.
§4 I, p. 301: a convex polyhedron $\operatorname{conv} S$ has an extreme support and equals the set cut out by its extreme supports.

Significance

The result. §4 II gives both directions of the Minkowski–Weyl theorem for full-dimensional polytopes, together with a test on the data $(A, b)$ : positive spanning of the normals is equivalent to boundedness, and a strictly feasible point is equivalent to full dimension. Several parts of LP theory start from this equivalence: finiteness of the vertex set of a bounded feasible region, the existence of an optimal vertex, and the passage between the primal (inequality) and dual (generator) descriptions used in polyhedral combinatorics.

Formalizing it. The theorem has been proved since 1935; the work here is formalization. Mathlib has convex hulls, extreme points, and pointed cones with their duals, but no Minkowski–Weyl theorem for polytopes or for cones. On this platform, Farkas-type lemmas (LinearOptimization.farkas_cone_corollary) and the statement that a nonempty bounded polyhedron is the hull of its extreme points (Bertsimas–Tsitsiklis Thm 2.9) are published. Neither gives the "only if" direction, the positive-spanning criterion, or full-dimensionality.

Difficulty

The "only if" direction and the reduction from a strictly feasible bounded region to cones are routine. The hard step is the finiteness statement: why a finite set of inequalities has only finitely many generators, and why these generate the whole region. Mathlib's compactness results give "a compact convex set is the closed hull of its extreme points" (Krein–Milman). That result does not show that the extreme points are finite in number, nor that there are finitely many of them in a form that can be computed from the inequalities. Weyl's route avoids topology. It goes through the Hauptsatz, proved by induction on dimension, and the duality between $S$ and $\Sigma$ . Each step of that duality needs non-degeneracy, and keeping that hypothesis alive through the dualization (Satz 9) is where care is needed.

Formalization scope

The homogeneous space is Fin n → ℝ, with dot product ⬝ᵥ. Point systems are Finsets; the zero vector is allowed in them. "Representable" is an explicit nonnegative sum over the Finset.
Non-degeneracy is the literal condition " $(\alpha s)=0$ for all $s \in S$ implies $\alpha = 0$ ", not span = ⊤.
Extreme supports and extreme solutions quantify over all vectors with the property. Positive multiples are not identified, and no representatives are chosen.
Extreme solutions are required to be nonzero and to lie in $(S)$ . This is implicit in the paper.
§4 is stated in affine form on Fin m → ℝ, a point $x$ standing for Weyl's $(x,-1)$ . Linear independence of $n-1$ homogenized points becomes affine independence of $m$ points, and non-degeneracy becomes affineSpan ℝ S = ⊤.
A "convex polyhedron" is the hull of a finite set with full affine span. Dropping full-dimensionality would make the "only if" false, since a segment in $\mathbb{R}^2$ has no inner point.
Added hypotheses: no zero row in the goal (Weyl's half-spaces have nonzero normal $(\alpha_1,\dots,\alpha_n)$ , p. 291). Non-degeneracy of $S$ in Satz 6 and in the p. 298 representation, where it is inherited from Satz 4.
Condition (i) of the goal is positive spanning, i.e. nonnegative coefficients. Linear spanning of $\mathbb{R}^m$ would be strictly weaker and would make the statement false.
A trivializing formalization is ruled out: the goal is an equivalence, "convex polyhedron" is an existential over finite point sets with full affine span, and no hypothesis restricts $J$ , $m$ or the data beyond the nonzero rows. For $m = 0$ the statement is true and non-vacuous.
Useful infrastructure, reusable beyond this mission: a Minkowski–Weyl theorem for polyhedral cones in Fin n → ℝ, extreme rays of pointed polyhedral cones, and the homogenization dictionary between cones in $\mathbb{R}^{m+1}$ and polytopes in $\mathbb{R}^m$ . Proofs of any milestone, and alternative routes to the goal (e.g. via Fourier–Motzkin elimination), are welcome.

Selected references

H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici (1935), 290–306. https://doi.org/10.1007/bf01292722
H. Weyl, The elementary theory of convex polyhedra, in: H. W. Kuhn, A. W. Tucker (eds.), Contributions to the Theory of Games I, Annals of Mathematics Studies 24, Princeton University Press, 1950.
J. Farkas, Theorie der einfachen Ungleichungen, Journal für die reine und angewandte Mathematik 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
H. Minkowski, Geometrie der Zahlen, Teubner, Leipzig, 1896/1910.
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (Minkowski–Weyl).

13 thms4 active usersReviewed

Completed

Analysis Operations Research Optimization·Captain: mikedeng1

A Nonsmooth Version of Newton's Method III: Semismoothness of the Augmented Lagrangian GradientResearch Paper

Motivation

The augmented Lagrangian method (method of multipliers) of Hestenes, Powell and Rockafellar solves a constrained nonlinear program by repeatedly minimizing an unconstrained merit function in the primal variables and then updating the multipliers. For inequality constraints, the augmented Lagrangian in the form the paper takes from Rockafellar (Rockafellar 1981) is continuously differentiable but not twice differentiable, even when all problem data are smooth: its Hessian jumps across the surfaces where a constraint switches between the "active" and "inactive" formula. Newton's method for the inner minimization therefore has no classical Hessian to work with on those surfaces.

Qi and Sun (Math. Programming 58, 1993) extended Newton's method to equations $F(x) = 0$ with $F$ locally Lipschitz, replacing the Jacobian by an element of Clarke's generalized Jacobian, and proved local superlinear convergence when $F$ is semismooth. Section 4 of the paper, an example suggested by Rockafellar, shows that the gradient of the augmented Lagrangian of a $C^2$ program is semismooth, so the nonsmooth Newton method applies to the stationarity equation $\nabla L_r = 0$ . This mission formalizes that result, Theorem 4.1.

Setting

Let $f_0, f_1, \dots, f_m : \mathbb{R}^n \to \mathbb{R}$ be of class $C^2$ and consider

\text{(NLP)}\quad \min f_0(x)\ \text{ s.t. }\ f_i(x) = 0,\ i = 1,\dots,p,\qquad f_i(x) \le 0,\ i = p+1,\dots,m. \tag{4.1}

Fix $r > 0$ . For a constraint value $a$ and a multiplier $y$ put

\phi(r, a, y) = \begin{cases} y a + \tfrac12 r a^2, & y + r a \ge 0,\\ -\tfrac{1}{2r} y^2, & y + r a \le 0,\end{cases}

(the two cases agree when $y + ra = 0$ ). The augmented Lagrangian is the function of $(x, y) \in \mathbb{R}^n \times \mathbb{R}^m$

L_r(x, y) = f_0(x) + \sum_{i=1}^{p}\Big(y_i f_i(x) + \tfrac12 r f_i(x)^2\Big) + \sum_{i=p+1}^{m} \phi\big(r, f_i(x), y_i\big).

For a locally Lipschitz map $F$ between finite-dimensional spaces, let $D_F$ be the set where $F$ is differentiable. Clarke's generalized Jacobian is $\partial F(x) = \mathrm{co}\{\lim JF(x_i) : x_i \to x,\ x_i \in D_F\}$ . $F$ is semismooth at $x$ if it is locally Lipschitz near $x$ and, for every direction $h$ , the limit of $V h'$ over $V \in \partial F(x + t h')$ , $h' \to h$ , $t \downarrow 0$ , exists.

For a single constraint function $g$ the proof works with $\eta(x, s) = \phi(r, g(x), s)$ on $\mathbb{R}^n \times \mathbb{R}$ , and with the surface $s + r g(x) = 0$ on which the two formulas for $\phi$ meet.

Formalization targets

Goal: Theorem 4.1

For $r > 0$ and $f_0, \dots, f_m \in C^2$ :

L_r \in C^1, \qquad \nabla L_r \text{ semismooth at } (x,y) \text{ whenever } \exists\, i > p:\ y_i + r f_i(x) = 0,

\nabla L_r \in C^1 \text{ near } (x, y) \text{ whenever } y_i + r f_i(x) \neq 0 \text{ for all } i > p.

All three clauses are the theorem; the last two together cover every point.

Milestones

$\eta \in C^1$ , with $\nabla\eta(x,s) = \big((s + r g(x))\nabla g(x),\ g(x)\big)$ if $s + r g(x) \ge 0$ and $(0, -s/r)$ if $s + r g(x) \le 0$ , and $\nabla \eta$ is locally Lipschitz.
Eq. (4.2): the Hessian of $\eta$ on each side of the surface, and $\nabla\eta \in C^1$ near every point off it.
Eq. (4.7): if $\bar s + r g(\bar x) = 0$ and $\bar s + t_j\alpha_j + r g(\bar x + t_j h_j) = 0$ with $h_j \to h$ , $\alpha_j \to \alpha$ , $t_j \downarrow 0$ , then $\alpha + r\nabla g(\bar x)^{\mathsf T} h = 0$ .
$\nabla\eta$ is semismooth, jointly in $(x, s)$ , at every point of the surface.

Significance

The result places the inner problem of the augmented Lagrangian method inside the scope of the paper's convergence theory: with $F = \nabla L_r$ , the generalized-Jacobian Newton iteration converges locally superlinearly at a root where every element of $\partial F$ is nonsingular. Its practical content is that second-order methods can be run on $L_r$ even though $L_r$ is only $C^{1}$ , with the elements of $\partial \nabla L_r$ playing the role of Hessians. The same pattern (a $C^1$ merit function with semismooth gradient) recurs in extended linear-quadratic programming and in semismooth Newton methods for complementarity problems.

The theorem is proved in the paper by direct computation. As far as a search of the platform showed, none of the objects involved (Clarke's generalized Jacobian, semismoothness, Rockafellar's augmented Lagrangian) has a published formalization there, and Mathlib has none of them. The mission produces a machine-checked version of the computation and, as a by-product, reusable statements about $C^1$ functions obtained by gluing two $C^2$ pieces along a hypersurface.

Difficulty

Clauses 1 and 3 are calculus with a case split: one has to check that the two formulas for $\phi$ and for its gradient match on the surface. Clause 2 is where the argument is not routine. On the surface, $\nabla\eta$ is not differentiable, and the generalized Jacobian $\partial\nabla\eta$ there contains convex combinations of the two one-sided Hessians of (4.2). Semismoothness asks that $V(h', \alpha')$ have a single limit over all such $V$ , for all approaches $(h', \alpha') \to (h, \alpha)$ , $t \downarrow 0$ , including approaches that cross the surface infinitely often. The two one-sided Hessians are different matrices, so no single derivative describes $\nabla\eta$ near the surface, and the existence of the limit must be shown for approaches that alternate between the two sides and for the convex combinations that $\partial\nabla\eta$ contains on the surface itself. General theorems that piecewise-smooth maps are semismooth appear in later literature but are not available in Mathlib, so they cannot be invoked as a shortcut. A second obstacle is infrastructure: Mathlib has no generalized Jacobian, so every fact about $\partial\nabla\eta$ (which limits of derivatives occur near the surface) must be derived from the definition.

Formalization scope

$\mathbb{R}^n$ and $\mathbb{R}^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $L_r$ is a function on their product, and $\eta$ on EuclideanSpace ℝ (Fin n) × ℝ.
The constraint index $i \in \{1,\dots,m\}$ is i : Fin m with paper index i.val + 1; equality constraints are i.val < p, inequality constraints p ≤ i.val. The paper's implicit $p \le m$ is not assumed (for $p > m$ there are no inequality constraints).
The paper's first sum prints $h(r_i, f_i(x), y_i)$ ; the single $r$ is used, as in the paper's definition of $h$ .
$\phi$ uses the first branch when $y + ra \ge 0$ ; the branches agree on the boundary. Every statement assumes $r > 0$ .
$C^2$ is ContDiff ℝ 2 on all of $\mathbb{R}^n$ ; "smooth" is the paper's continuously differentiable, ContDiffAt ℝ 1 of the gradient at the point.
$\nabla L_r$ and $\nabla\eta$ are Fréchet derivatives, valued in continuous linear functionals; semismoothness is invariant under the Riesz isometry to gradient vectors and under equivalent norms on the domain (Mathlib's product has the sup norm).
The Jacobian in Clarke's definition is fderiv, limits are along sequences, and no closure is taken in the convex hull. Semismoothness is the explicit $\varepsilon$ – $\delta$ form of the paper's limit, uniform over $V \in \partial F(x + th')$ .
Hessians in (4.2) are stated as the Fréchet derivative of the gradient map applied to a direction.

A formalization that states only $L_r \in C^1$ , or only the semismoothness of one term $\eta$ , is not Theorem 4.1; the goal contains all three clauses for the full $L_r$ . The combination step from the terms $\eta$ to $L_r$ uses that sums of semismooth maps and $C^1$ maps with locally Lipschitz derivative are semismooth; the paper cites this without proof, and a solver will need to prove it.

Contributions welcome: the lemmas above; general facts about clarkeJac (it contains fderiv at points of strict differentiability; it is a singleton for $C^1$ maps; behaviour under sums and linear maps); and the semismoothness of sums.

Selected references

L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
R. T. Rockafellar, Proximal subgradients, marginal values, and augmented Lagrangians in nonconvex optimization, Mathematics of Operations Research 6 (1981) 427–437. https://doi.org/10.1287/moor.6.3.427
F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (reprinted SIAM Classics in Applied Mathematics 5, 1990). https://doi.org/10.1137/1.9781611971309
R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15 (1977) 959–972. https://doi.org/10.1137/0315061

8 thms4 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Robust Mean-Covariance Solutions for Stochastic Optimization III: Concave Utilities with a Monotone Second Derivative Have a Closed-Form Robust ObjectiveResearch Paper

Motivation

A decision maker who chooses a portfolio $x\in\mathbb R^n$ of risky assets with random return vector $R$ receives the scalar return $x'R$ and evaluates it by an expected utility $E[u(x'R)]$ . In practice the law of $R$ is not known; what can be estimated with some confidence are its mean $\mu$ and covariance $\Sigma$ . The robust mean-covariance objective replaces the unknown law by the worst law consistent with these two moments:

U(x)=\inf\{E[u(x'R)] : R \text{ has mean } \mu \text{ and covariance } \Sigma\}.

Ioana Popescu (Operations Research 55(1), 2007) showed that $U(x)$ depends on $x$ only through $\mu_x=x'\mu$ and $\sigma_x^2=x'\Sigma x$ , and that for large classes of utilities it has a closed form or reduces to a one-dimensional search. This turns a robust stochastic program into a parametric mean-variance program, which is the practical point of the paper. This mission formalizes the closed form for concave utilities with a monotone second derivative (Proposition 7), a class that contains the exponential utility $1-e^{-ay}$ and all concave quadratics. The reduction to $(\mu_x,\sigma_x)$ is the subject of the companion mission Robust Mean-Covariance Solutions for Stochastic Optimization I; the two-point case is mission II.

The underlying univariate question is a moment problem in the tradition of Chebyshev-type bounds: the extremal value of $E[u(r)]$ over all laws with prescribed mean and variance. Scarf (1958) solved an instance for a piecewise-linear inventory cost, and Birge and Dulá (1991) treated two-point extremal laws on bounded domains.

Setting

Fix $m\in\mathbb R$ and $s\ge 0$ . The mean-variance class $\mathbb M_{(m,s^2)}$ is the set of Borel probability measures $\nu$ on $\mathbb R$ with $\int r^2\,d\nu<\infty$ , $\int r\,d\nu=m$ and $\int (r-m)^2\,d\nu=s^2$ (Lean: MeanVarClass m (s ^ 2)). For a utility $u:\mathbb R\to\mathbb R$ the robust objective is

U(m,s)=\inf\Big\{\int u\,d\nu : \nu\in\mathbb M_{(m,s^2)}\Big\},

with $\min$ read, as in the paper, "in the wide sense of $\inf$ ", so the value $-\infty$ is allowed. The paper's $U(x)$ is $U(\mu_x,\sigma_x)$ .

For $p\in(0,1)$ the two-point law $r_p$ puts mass $p$ on $b=m+\sqrt{(1-p)/p}\,s$ and mass $1-p$ on $a=m-\sqrt{p/(1-p)}\,s$ ; these are exactly the two-point laws of $\mathbb M_{(m,s^2)}$ . Its expected utility is the two-point objective (8),

U(p)=p\,u(b)+(1-p)\,u(a)\qquad(\texttt{twoPointValue u m s p}).

A supporting quadratic of $u$ is $q(y)=Ay^2+By+C$ with $q\le u$ on $\mathbb R$ ; the set of their coefficients is $\mathcal Q$ . Since every $r\sim(m,s^2)$ has $E[q(r)]=A(m^2+s^2)+Bm+C$ , each element of $\mathcal Q$ gives a lower bound on $U(m,s)$ (Proposition 3). The function $u$ has the one-point support property with respect to $(m,s^2)$ (Definition 3, OnePointSupportWrt u m s) if some supporting quadratic touches $u$ at $m$ and $E[u(r_p)]\to E[q(r_p)]$ as $p\to0^+$ or as $p\to1^-$ ; it has one-point support (OnePointSupport u) if this holds for every $m$ and every $s\ge0$ .

Formalization targets

Goal: Proposition 7

Let $u$ be concave and twice differentiable with monotone $u''$ .

(a) If $u'$ is convex, then

U(m,s)=u(m)+\lim_{y\to-\infty}u''(y)\,\frac{s^2}{2}\qquad\text{for all } m,\ s.

(b) If $u'$ is concave, the same holds with $\lim_{y\to+\infty}u''(y)$ .

In each part the limit $L$ of $u''$ exists in $[-\infty,0]$ . When $L$ is finite the goal asserts that $u$ is integrable under every law of every class, that $u(m)+Ls^2/2$ is the greatest lower bound of the expected utilities, and that $u$ has one-point support. When $L=-\infty$ and $s>0$ it asserts $U(m,s)=-\infty$ .

Milestones

Display (9): $\partial U/\partial p=u(b)-u(a)-(b-a)\,\frac{u'(b)+u'(a)}{2}$ .
For convex $u'$ and $s>0$ , $U(p)$ is nonincreasing on $(0,1)$ .
Appendix (4): $\lim_{p\to1^-}U(p)=u(m)+\frac{s^2}{2}\lim_{y\to-\infty}u''(y)$ , including the value $-\infty$ .
Proposition 3: every $E[u(r)]$ dominates every $A(m^2+s^2)+Bm+C$ with $(A,B,C)\in\mathcal Q$ .
The function $d(y)=\frac{u(y)-u(m)}{(y-m)^2}-\frac{u'(m)}{y-m}$ is nondecreasing on $\{y \neq m\}$ when $u'$ is convex.
Appendix (5): $q(y)=\tfrac12u''(-\infty)(y-m)^2+u'(m)(y-m)+u(m)$ supports $u$ , and $\inf_{y\ne m}d(y)=\lim_{y\to-\infty}d(y)=\tfrac12u''(-\infty)$ .

An additional item states Proposition 8: a monotone convex $u$ has one-point support and $U(m,s)=u(m)$ .

Significance

Proposition 7 turns the worst-case expected utility into a mean-variance criterion with an explicit risk weight: a prudent investor ( $u'$ convex) is penalized by $\tfrac12\lim_{y\to-\infty}u''(y)$ per unit of variance, an imprudent one by the limit at $+\infty$ . With Proposition 1, the robust portfolio problem becomes $\max_x\ u(\mu_x)+\tfrac12 L\,\sigma_x^2$ , a concave mean-variance program. For exponential utility the weight is $-\infty$ (Example 3 of the paper), so the robust investor must eliminate variance entirely; this is a qualitative statement about robustness that follows only from the $-\infty$ case of the theorem.

The result is published with a proof in the appendix of the paper. It has, to the best of our search, no machine-checked version, and the platform currently holds no statement of Propositions 3, 7 or 8 or Definition 3. A formal proof would also check two points where the printed argument is incomplete: the proof's step " $\lim_{y\to-\infty}u'(y)=\infty$ " fails for affine $u$ , where the theorem nevertheless holds, and the claim that $u$ "has one-point support" fails when $\lim u''=-\infty$ (see the scope section). Related platform work on worst-case expectations over ambiguity sets is the mission Wasserstein Distributionally Robust Optimization II, which uses a different ambiguity set.

Difficulty

The infimum ranges over all laws with two prescribed moments, an infinite-dimensional set with no compactness, and in the relevant cases it is not attained. The natural first idea, restricting to two-point laws and minimizing over $p$ , gives only an upper bound (display (7)), and here the minimizing $p$ runs off to the boundary: the extremal law puts vanishing mass on a point escaping to $-\infty$ . Identifying the limiting value requires controlling $u(m-sq)/(1+q^2)$ as $q\to\infty$ , a second-order asymptotic statement about $u$ at $-\infty$ . The matching lower bound requires a supporting quadratic whose curvature is exactly $\tfrac12\lim u''$ ; showing that it lies below $u$ everywhere, not only near $m$ , is a global statement that uses the convexity of $u'$ on the whole line. The finite-limit and infinite-limit cases also behave differently: in the second, no supporting quadratic exists at all.

Formalization scope

Laws are Measure ℝ with IsProbabilityMeasure, finite second moment is MemLp id 2, and the class is parameterized by mean $m$ and variance $s^2$ with $s\ge0$ . The statements are univariate: $U(x)$ of the paper is the univariate objective at $(\mu_x,\sigma_x)$ by Proposition 1 of the paper (mission I). Derivatives are deriv u and deriv (deriv u); "twice differentiable" is differentiability of $u$ and of $u'$ . Limits of $u''$ are explicit hypotheses (Tendsto … atBot (𝓝 L) or Tendsto … atBot atBot), never limUnder. Limits in $p$ are one-sided inside $(0,1)$ . Expectations under two-point laws are written by the explicit formula (8).

"Min" is never a real ⨅, which Lean evaluates to $0$ on sets unbounded below. The finite case uses IsGLB together with integrability of $u$ under every law of the class; the infinite case asserts that integrable laws with arbitrarily small expected utility exist; Proposition 3 is stated as "every value $\ge$ every value". Proposition 3 assumes $u$ integrable under the law; Proposition 8 takes the infimum over laws under which $u$ is integrable, which for convex $u$ loses nothing.

One correction to the printed statement: Proposition 7 opens with "then $u$ has one-point support", which is false when $\lim u''=-\infty$ , since no quadratic lies below $1-e^{-ay}$ on $\mathbb R$ . The formalization asserts one-point support only in the finite-limit case and the value $-\infty$ in the other. A formalization that took $\min$ as a real infimum, dropped the integrability conjunct, or asserted one-point support unconditionally would be either trivially satisfiable or false; none of these is used.

A complete development needs: moments of two-point laws, a second-order l'Hôpital or Taylor argument at $-\infty$ , the trapezoid inequality for convex functions, and Jensen-type integration of quadratic lower bounds. The mean-variance class, the two-point objective and the supporting-quadratic lemmas are reusable for mission II and for other moment-problem bounds. Proofs of any milestone, and of part (b), are welcome.

Selected references

I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30, 1991.
S. Karlin, W. J. Studden, Tchebycheff Systems: With Applications in Analysis and Statistics, Interscience, 1966.

11 thms4 active usersReviewed

Completed

Combinatorics Probability·Captain: mikedeng1

Limits of Permutation Sequences II: Convergence Is Equivalent to Being Cauchy in the Rectangular DistanceResearch Paper

Motivation

For dense graphs, convergence of subgraph densities was shown by Lovász and Szegedy (2006) to have graphons as limit objects, and Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) proved that the same convergence is metric: a graph sequence converges exactly when it is Cauchy in the cut distance. The metric view is what makes the space of graphons compact and connects limit theory with regularity lemmas and property testing.

Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) developed the corresponding theory for permutations. Besides the existence of limits (the subject of mission I of this series), they introduced a rectangular distance $d_\square$ between permutations, a normalized version of Cooper's discrepancy (Cooper, J. Combin. Theory Ser. A, 2004; reference [7] of the paper), and proved in Theorem 1.8 that convergence of a permutation sequence is the same as being Cauchy for $d_\square$ . This mission formalizes that theorem.

Timeline:

2004. Cooper introduces the discrepancy of a permutation as a measure of quasirandomness.
2006–2008. Lovász–Szegedy and Borgs et al. establish graph limits and the cut-distance characterization of convergence.
2011–2013. Hoppen et al. prove the permutation analogues, including Theorem 1.8 (this paper).

Setting

For $n \ge 1$ , $S_n$ is the set of permutations of $[n]=\{1,\dots,n\}$ , $|\pi| = n$ for $\pi\in S_n$ , and $\mathcal S=\bigcup_n S_n$ . For $\tau\in S_k$ and $\pi\in S_n$ , $\Lambda(\tau,\pi)$ counts the increasing $k$ -tuples $x_1<\dots<x_k$ in $[n]$ with $\pi(x_i)<\pi(x_j)\iff\tau(i)<\tau(j)$ , and the subpermutation density is $t(\tau,\pi)=\Lambda(\tau,\pi)/\binom nk$ for $k\le n$ and $0$ for $k>n$ . A permutation sequence $(\sigma_n)$ is convergent if $t(\tau,\sigma_n)$ converges for every fixed $\tau\in\mathcal S$ .

A limit permutation is a Lebesgue measurable $Z:[0,1]^2\to[0,1]$ such that $Z(x,\cdot)$ is a cdf (non-decreasing, right-continuous, $Z(x,1)=1$ ) for every $x$ and $\int_0^1 Z(x,y)\,dx=y$ for every $y$ ; the set of them is $\mathcal Z$ . Each $Z$ has an associated random point $(X,Y)$ with $X\sim U[0,1]$ and conditional cdf $Z(X,\cdot)$ , joint distribution function $F(x,y)=\int_0^x Z(t,y)\,dt$ , and pattern densities $t(\tau,Z)$ (the probability that $k$ independent copies of $(X,Y)$ form the pattern $\tau$ ).

For $\sigma\in S_n$ , the step limit permutation $Z_\sigma$ spreads the permutation matrix of $\sigma$ uniformly over the corresponding $n\times n$ grid cells. The rectangular distance of $Z_1,Z_2\in\mathcal Z$ is

d_\square(Z_1,Z_2)=\sup_{x_1<x_2,\ y_1<y_2}\left|\int_{x_1}^{x_2}\big(Z_1(x,y_2)-Z_1(x,y_1)\big)dx-\int_{x_1}^{x_2}\big(Z_2(x,y_2)-Z_2(x,y_1)\big)dx\right|,

the largest difference between the probabilities the two random points give to an axis-parallel rectangle, and $d_\infty(Z_1,Z_2)=\sup_{x,y}|F_1(x,y)-F_2(x,y)|$ . On permutations of possibly different lengths, $d_\square(\sigma,\pi):=d_\square(Z_\sigma,Z_\pi)$ . A sequence is Cauchy with respect to $d_\square$ if for every $\varepsilon>0$ there is $n_0$ with $d_\square(\sigma_n,\sigma_m)<\varepsilon$ for all $n,m\ge n_0$ .

Formalization targets

Goal: Theorem 1.8, under $|\sigma_n|\to\infty$

|\sigma_n|\to\infty\ \Longrightarrow\ \Big((\sigma_n)\ \text{convergent}\iff(\sigma_n)\ \text{is } d_\square\text{-Cauchy}\Big).

Milestones

In the order the proof uses them:

Lemma 3.5: $|t(\tau,\sigma)-t(\tau,Z_\sigma)|\le\frac1n\binom k2$ for $\tau\in S_k$ , $\sigma\in S_n$ , $k\le n$ .
Eq. (49): for $|\sigma_n|\to\infty$ , $\sigma_n\to Z\iff Z_{\sigma_n}\xrightarrow{t}Z$ .
Eq. (34): $d_\infty\le d_\square\le 4\,d_\infty$ on $\mathcal Z$ .
Lemma 2.1: for uniform marginals, weak convergence is equivalent to uniform convergence of joint distribution functions.
Lemma 2.2 (a): every law on $[0,1]^2$ with uniform marginals has a limit permutation as its conditional cdf.
Lemma 5.3: weak, $d_\square$ - and density convergence on $\mathcal Z$ coincide.
Theorem 1.6 (i): a convergent sequence with $|\sigma_n|\to\infty$ converges to some $Z\in\mathcal Z$ .
Claim 2.4: a convergent sequence with $|\sigma_n|\not\to\infty$ is eventually constant.
Theorem 1.8 ( $\Rightarrow$ ): every convergent sequence is $d_\square$ -Cauchy, with no condition on lengths.

Significance

Theorem 1.8 identifies density convergence, defined through infinitely many pattern counts, with a single metric condition. With Theorem 1.6 it shows that the completion of $(\mathcal S,d_\square)$ is $\mathcal Z$ modulo almost-everywhere equality, which is compact; permutations are isolated points of it (Claim 2.4). This is the permutation counterpart of the cut-distance theory of graph limits, and it is the metric in which the paper's testability and sampling results (Lemma 4.2) are quantitative.

The theorem is proved in the paper. To the best of current knowledge neither it nor the underlying permuton theory is formalized in any proof assistant. The mission produces machine-checked statements of the rectangular distance, its comparison with the sup-norm distance of distribution functions, and the Cauchy characterization, all reusable for quasirandom permutations and permutation property testing.

Difficulty

The direction "convergent $\Rightarrow$ Cauchy" needs a limit permutation for the sequence and the equivalence of density and $d_\square$ convergence on $\mathcal Z$ (Lemma 5.3), which is not formal: density convergence involves every pattern, $d_\square$ a supremum over rectangles. For "Cauchy $\Rightarrow$ convergent", completeness of bounded functions under the sup norm gives a uniform limit $F$ of the distribution functions, but a uniform limit of distribution functions of limit permutations is not visibly the distribution function of a limit permutation. Identifying it needs weak compactness, Lemma 2.1 and the regular conditional cdf of Lemma 2.2.

The literal statement also fails for sequences whose lengths do not tend to infinity, as explained under Formalization scope; the reduction "we may assume $|\sigma_n|\to\infty$ " covers only one direction.

Formalization scope

$[0,1]$ is Mathlib's unitInterval with Lebesgue measure; a limit permutation is a curried real function Z : I → I → ℝ, almost-everywhere measurable on the square, with the cdf and integral conditions for every $x$ and every $y$ . $S_n$ is Equiv.Perm (Fin n) (0-based) and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n).
$d_\square$ on $\mathcal Z$ is the integral form of the paper's Eq. (32); $d_\infty$ is Eq. (33) with $F_i(x,y)=\int_0^x Z_i(t,y)\,dt$ . Both are real suprema of bounded families. $Z_\sigma$ is in closed form, with the first row used at $x=0$ (a null-set choice).
$d_\square$ on permutations is defined for every pair of lengths as $d_\square(Z_\sigma,Z_\pi)$ , the paper's extension (Sect. 4.1); the same-length formula (31) is not needed. A definition that returned $0$ or junk for different lengths would make every sequence with growing lengths Cauchy and is ruled out.
Correction. The paper states Theorem 1.8 for all sequences. Without $|\sigma_n|\to\infty$ , "Cauchy $\Rightarrow$ convergent" is false: interleaving $\sigma=(1,2)$ with permutations $\tau_k$ , $|\tau_k|\to\infty$ , $d_\square(Z_{\tau_k},Z_\sigma)\to0$ , gives a Cauchy sequence along which $t(\sigma,\cdot)$ alternates between $1$ and values tending to $3/4$ . The goal carries $|\sigma_n|\to\infty$ ; the true direction without it is milestone 9.
"Convergent" is the paper's Definition 1.2 (all densities converge), not the existence of a limit $Z$ . The Cauchy condition uses the explicit $\varepsilon$ – $n_0$ form with strict inequality, not a metric-space instance.
Theorem 1.6 (i) is also the goal of mission I; it is restated here in this mission's namespace.

Needed infrastructure: Prokhorov compactness of probability measures on the square, the Portmanteau theorem, completeness of bounded functions under the sup norm, and conditional cdfs (ProbabilityTheory.condCDF). Contributions on any milestone, and alternative proofs of the Cauchy characterization, are welcome.

Selected references

C. Hoppen, Y. Kohayakawa, C. G. Moreira, B. Ráth, R. M. Sampaio, Limits of permutation sequences, arXiv:1103.5844v2, 2012; J. Combin. Theory Ser. B 103 (2013). https://arxiv.org/abs/1103.5844v2
J. N. Cooper, Quasirandom permutations, J. Combin. Theory Ser. A 106 (2004) no. 1, 123–143 (cited as [7] in arXiv:1103.5844v2).
L. Lovász, B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96 (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002
C. Borgs, J. T. Chayes, L. Lovász, V. T. Sós, K. Vesztergombi, Convergent sequences of dense graphs I: Subgraph frequencies, metric properties and testing, Adv. Math. 219 (2008) 1801–1851. https://doi.org/10.1016/j.aim.2007.08.004
P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962

21 thms4 active usersReviewed