Optimization

Motivation

Many nonconvex optimization problems in binary variables have a polynomial objective or polynomial constraints. The standard way to bring them into the reach of linear and mixed-integer programming solvers is to introduce one new variable per monomial and to study the convex hull of the resulting set of feasible 0/1 vectors, the multilinear polytope. Strong linear descriptions of this polytope translate directly into tighter relaxations in global solvers such as BARON, which is where the inequalities of this mission were tested (Del Pia and Khajavirad 2021, §2.5).

The multilinear polytope of a general hypergraph has no compact description, so the question is for which hypergraphs a given family of inequalities is enough. The quadratic case is classical: the Boolean quadric polytope of a graph (Padberg 1989) is described by its standard linearization exactly when the graph is a forest, and the odd-cycle inequalities are the first facets that appear on a cycle. For higher-degree monomials, Del Pia and Khajavirad showed in 2018 that their flower relaxation is exact if and only if the hypergraph is γ-acyclic. The 2021 paper introduces the stronger running intersection relaxation and asks the same question for it. This mission formalizes the necessary condition the paper proves: the relaxation cannot be exact unless the hypergraph is β-acyclic.

Setting

A hypergraph $G=(V,E)$ is a finite node set $V$ with a set $E$ of subsets of $V$ of size at least two (no loops, no parallel edges). Its multilinear set is

$$\mathcal S_G=\Big\{z\in\{0,1\}^{V+E}: z_e=\prod_{v\in e}z_v\ \ \forall e\in E\Big\},$$

and the multilinear polytope is $\mathrm{MP}_G=\operatorname{conv}\mathcal S_G$. The standard linearization is

$$\mathrm{MP}^{\mathrm{LP}}_G=\Big\{z: z_v\le 1\ \forall v;\ z_e\ge 0,\ z_e\ge\sum_{v\in e}z_v-|e|+1\ \forall e;\ z_e\le z_v\ \forall e,\ v\in e\Big\}.$$

An ordering $p_1,\dots,p_m$ of a multiset of sets is a running intersection ordering if each $p_k$, $k\ge2$, meets the union of its predecessors inside a single predecessor $p_j$; it induces $N(p_1)=\emptyset$ and $N(p_k)=p_k\cap\bigcup_{i<k}p_i$. A running intersection inequality has a center $e_0\in E$, neighbors $e_k$ ($k\in K$) meeting $e_0$ such that $\tilde E=\{e_0\cap e_k\}$ admits a running intersection ordering, and nodes $u_k\in N(e_0\cap e_k)$ when these sets are nonempty:

$$-\sum_{k:\,N(e_0\cap e_k)\ne\emptyset}z_{u_k}+\sum_{v\in e_0\setminus\bigcup_k e_k}z_v+\sum_{k\in K}z_{e_k}-z_{e_0}\le\omega-1,$$

with $\omega$ the number of connected components of $(e_0,\tilde E)$. The running intersection relaxation $\mathrm{MP}^{\mathrm{RI}}_G$ is $\mathrm{MP}^{\mathrm{LP}}_G$ together with all these inequalities.

A β-cycle of length $t\ge3$ is a sequence $v_1,e_1,\dots,v_t,e_t,v_1$ of distinct nodes and distinct edges in which each $v_i$ lies in $e_{i-1}$ and $e_i$ and in no other $e_j$; $G$ is β-acyclic if it has none. For $W\subseteq V$ the subhypergraph $G_W$ has node set $W$ and edges $\{e\cap W: |e\cap W|\ge2\}$.

Formalization targets

Goal: Proposition 5

$$G\ \text{not β-acyclic}\ \Longrightarrow\ \mathrm{MP}_G\subsetneq\mathrm{MP}^{\mathrm{RI}}_G .$$

The milestones follow the paper's proof, in order:

1. $\mathrm{MP}_G\subseteq\mathrm{MP}^{\mathrm{LP}}_G$ (p. 1014) and validity of every running intersection inequality (Proposition 1), giving $\mathrm{MP}_G\subseteq\mathrm{MP}^{\mathrm{RI}}_G$.
2. Lemma 3: β-cycles of $G_{V'}$ lift to β-cycles of $G$ of the same length.
3. Lemma 5: $\mathrm{MP}_{G_{\bar V}}=\mathrm{proj}_{G_{\bar V}}(\mathrm{MP}_G\cap L_{\bar V})$, with $L_{\bar V}=\{z: z_v=1\ \forall v\notin\bar V\}$.
4. Lemma 6: $\mathrm{MP}^{\mathrm{RI}}_{G_{\bar V}}\subseteq\mathrm{proj}_{G_{\bar V}}(\mathrm{MP}^{\mathrm{RI}}_G\cap L_{\bar V})$.
5. The reduction: strictness for $G_W$ implies strictness for $G$.
6. For a shortest β-cycle $C$, $G_{V(C)}$ is a chordless cycle, possibly enclosed by the edge $V(C)$.
7. Strictness for a chordless cycle.
8. Strictness for a chordless cycle enclosed by the edge $V(C)$.

Significance

The result is one half of the paper's picture of when the running intersection relaxation is exact. Proposition 5 shows β-acyclicity is necessary; Theorem 3 of the paper shows that kite-free β-acyclicity is sufficient; Example 2 shows β-acyclicity alone is not. Combined with the 2018 characterization of the flower relaxation by γ-acyclicity, it places the running intersection relaxation strictly between two acyclicity notions and tells a solver designer that on hypergraphs with β-cycles some other family of cuts (for instance odd-cycle-type inequalities lifted from Padberg's) is unavoidable.

The intermediate results are reusable on their own. Lemma 5 is a general statement that multilinear polytopes of induced subhypergraphs are projections of faces, and Lemma 3 with the shortest-cycle structure step is pure hypergraph combinatorics.

The result is proved in the paper. No part of it, nor the multilinear polytope, nor the Boolean quadric polytope, is formalized in Lean or Mathlib as far as a search of the platform showed. Lemma 6 is stated in the paper without proof, and the two strictness cases are justified there by "it can be checked" and by a citation of Padberg; a formal proof closes these gaps.

Difficulty

The obvious argument exhibits a point of $\mathrm{MP}^{\mathrm{RI}}_G\setminus\mathrm{MP}_G$ directly from a β-cycle of $G$. This fails because a β-cycle of $G$ is surrounded by arbitrary other edges, which contribute running intersection inequalities that can cut off any candidate point. The paper's route is to pass to the subhypergraph induced by the cycle's nodes, and that step requires two facts with real content: the projection lemmas (Lemma 6 is an inclusion between relaxations defined by different families of inequalities), and the structure of $G_{V(C)}$, which holds only for a shortest β-cycle. A long β-cycle can have chords in $G_{V(C)}$.

Strictness on the two small families requires a point, or an inequality, separating $\mathrm{MP}$ from $\mathrm{MP}^{\mathrm{RI}}$. That means controlling every running intersection inequality of the cycle, over all centers, neighbor sets, orderings and choices of $u_k$, and also checking that the separating inequality is valid for $\mathrm{MP}$.

Formalization scope

Lean conventions:

• Nodes are elements of a finite type α with decidable equality. Hypergraphs carry their node set and their edge set as Finsets, with every edge of size at least two.
• Points of $\mathbb R^{V+E}$ are functions α ⊕ Finset α → ℝ, and every polytope of $G$ is pinned to zero off $G$'s own coordinates, so polytopes of different hypergraphs, and the projection $\mathrm{proj}_{G_{\bar V}}$, live in one space.
• $\mathrm{MP}^{\mathrm{LP}}_G$ is exactly (8), with no row $z_v\ge0$.
• $\mathrm{MP}^{\mathrm{RI}}_G$ quantifies over all centers, all sets of distinct neighbors other than $e_0$, all running intersection orderings and all choices of $u_k$.
• $\omega$ is the number of connected components of the 2-section graph on $e_0$.
• Orderings and cycles are 0-indexed.
• The projection takes the choice $e'(f)$ of an edge of $G$ with trace $f$ as an argument, and Lemmas 5 and 6 hold for every choice.
• The strict inclusion $\subset$ of the paper is Lean's ⊂ ($\subseteq$ and $\ne$).

There is one disclosed addition. Lemma 6 and the reduction step assume that $G_{\bar V}$ has no isolated node. Without it both statements are false: since (8) has no lower bound on $z_v$, a node isolated in $G_{\bar V}$ is unbounded below in $\mathrm{MP}^{\mathrm{RI}}_{G_{\bar V}}$. The paper uses them only for $\bar V=V(C)$, where the hypothesis holds. The goal itself carries no added hypothesis.

A trivializing formalization is ruled out. A relaxation missing some running intersection inequalities (a fixed ordering, a fixed $u_k$, a fixed neighbor set) would make strictness easier, and an empty or mis-pinned relaxation would make the inclusion false. The definitions here take the full family.

A complete development needs:

• convex hulls of finite point sets and separation of a point from them;
• connected components of the 2-section graph;
• running intersection orderings;
• the combinatorics of β-cycles.

The β-cycle and subhypergraph material and Lemma 5 are reusable beyond this mission. Contributions are welcome on any milestone, on alternative proofs of the two strictness cases (for instance by an explicit fractional point), and on a proof of Lemma 6.

Selected references

• A. Del Pia and A. Khajavirad, The running intersection relaxation of the multilinear polytope, Mathematics of Operations Research 46(3):1008–1037, 2021. https://doi.org/10.1287/moor.2021.1121
• A. Del Pia and A. Khajavirad, A polyhedral study of binary polynomial programs, Mathematics of Operations Research 42(2):389–410, 2017. https://doi.org/10.1287/moor.2016.0804
• A. Del Pia and A. Khajavirad, The multilinear polytope for acyclic hypergraphs, SIAM Journal on Optimization 28(2):1049–1076, 2018. https://doi.org/10.1137/16M1095998
• M. Padberg, The Boolean quadric polytope: some characteristics, facets and relatives, Mathematical Programming 45:139–172, 1989. https://doi.org/10.1007/BF01589101
• C. Beeri, R. Fagin, D. Maier and M. Yannakakis, On the desirability of acyclic database schemes, Journal of the ACM 30(3):479–513, 1983. https://doi.org/10.1145/2402.322389

Motivation

Binary polynomial optimization asks to minimize a polynomial over $\{0,1\}^n$. The standard way to attack it with linear programming is to introduce one variable $z_e$ for every monomial $\prod_{v\in e} z_v$ and to work with the convex hull of the resulting set of binary points. This convex hull, the multilinear polytope, is the object behind the cutting planes that global solvers such as BARON add at every node of a branch-and-bound tree, and in general its facets are as hard to describe as the original problem is to solve. The useful theory is therefore structural: which hypergraphs of monomials give multilinear polytopes with an explicit, combinatorial description.

A line of work by Del Pia and Khajavirad answers this for increasingly general classes of acyclic hypergraphs: Berge-acyclic and γ-acyclic hypergraphs via flower inequalities (SIAM J. Optim. 2018), sufficient conditions for decomposing multilinear sets (Math. Program. 2018), and, in the paper this mission formalizes (Math. Oper. Res. 2021), the running intersection inequalities, a generalization of flower inequalities that does not need γ-acyclicity. The paper reports that adding these cuts reduces BARON's root-node relaxation gap by more than 95% on most of 35 computer-vision instances.

Setting

A hypergraph $G=(V,E)$ has a finite node set $V$ and a set $E$ of subsets of $V$, each with at least two nodes. Points live in $\mathbb R^{V+E}$, one coordinate per node and per edge. The multilinear set and multilinear polytope are

$$\mathcal S_G=\Big\{z\in\{0,1\}^{V+E}: z_e=\prod_{v\in e}z_v\ \forall e\in E\Big\},\qquad \mathrm{MP}_G=\operatorname{conv}\mathcal S_G .$$

The standard linearization $\mathrm{MP}^{\mathrm{LP}}_G$ replaces each equation $z_e=\prod_{v\in e}z_v$ by its convex hull over the unit cube: $z_v\le 1$, $z_e\ge 0$, $z_e\ge\sum_{v\in e}z_v-|e|+1$ and $z_e\le z_v$ for $v\in e$.

An ordering $p_1,\dots,p_m$ of a family of sets is a running intersection ordering if each $p_k$ meets the union of its predecessors inside a single predecessor $p_j$; write $N(p_k)=p_k\cap\bigcup_{i<k}p_i$ and $N(p_1)=\emptyset$. Given a center edge $e_0$ and neighbor edges $e_k$, $k\in K$, meeting $e_0$ such that the sets $e_0\cap e_k$ admit a running intersection ordering, and nodes $u_k\in N(e_0\cap e_k)$ wherever this set is nonempty, the running intersection inequality is

$$-\sum_{k:\,N(e_0\cap e_k)\neq\emptyset}z_{u_k}+\sum_{v\in e_0\setminus\bigcup_k e_k}z_v+\sum_{k\in K}z_{e_k}-z_{e_0}\le\omega-1,$$

with $\omega$ the number of connected components of the hypergraph on $e_0$ with edges $e_0\cap e_k$. The running intersection relaxation $\mathrm{MP}^{\mathrm{RI}}_G$ is $\mathrm{MP}^{\mathrm{LP}}_G$ together with all these inequalities.

A β-cycle is a cyclic sequence of $t\ge 3$ distinct nodes and distinct edges $v_1,e_1,\dots,v_t,e_t$ in which $v_i$ lies in $e_{i-1}$ and $e_i$ and in no other edge of the cycle; $G$ is β-acyclic if it has none. A kite is three edges $e_0,e_1,e_2$ with $|e_0\cap e_1\cap e_2|\ge 2$, $(e_0\cap e_1)\setminus e_2\ne\emptyset$ and $(e_0\cap e_2)\setminus e_1\ne\emptyset$; $G$ is kite-free if it has none. $G$ is two-laminar if any two distinct edges sharing at least two nodes are strictly nested.

Formalization targets

Goal: Theorem 3 (p. 1023)

For every kite-free β-acyclic hypergraph $G$ without isolated nodes,

$$\mathrm{MP}_G=\mathrm{MP}^{\mathrm{RI}}_G .$$

Milestones

In attack order: validity of the inequalities (Proposition 1); heredity of β-acyclicity (Lemma 3); kite-free implies edge-induced subhypergraphs are two-laminar (Lemma 7); β-acyclicity as the running intersection property of every edge subset (Lemma 4); the explicit facet description of $\mathrm{MP}_G$ for two-laminar β-acyclic $G$ by system (20) (Proposition 6) and its consequence $\mathrm{MP}_G=\mathrm{MP}^{\mathrm{RI}}_G$ there (Corollary 3); the decomposition theorem for multilinear sets (Theorem 1); and five steps of the inductive proof of Theorem 3 in §5.3: $G_\omega$ is kite-free β-acyclic with one maximal edge fewer, the inductive step $\mathrm{MP}_{G^+}=\mathrm{MP}^{\mathrm{RI}}_{G^+}$, Claim 14 on partial hypergraphs, the projection $\mathrm{MP}_G=\mathrm{proj}\,\mathrm{MP}_{G^+}$, and the Fourier–Motzkin step $\mathrm{MP}^{\mathrm{RI}}_G\subseteq\mathrm{proj}\,\mathrm{MP}^{\mathrm{RI}}_{G^+}$.

Companions

Theorem 2 (p. 1022), the polynomial-size extended formulation $\mathrm{MP}_{G^+}=\bigcap_{i}\mathrm{MP}_{G^+_i}$ over the maximal edges, and the form (19) taken by running intersection inequalities in kite-free β-acyclic hypergraphs.

Significance

Theorem 3 gives a description of the multilinear polytope in the original space, by inequalities defined combinatorially from the hypergraph, for a class that strictly contains the γ-acyclic hypergraphs covered by flower inequalities. With Theorem 2 it implies that linear optimization and separation over $\mathrm{MP}_G$ are polynomial for kite-free β-acyclic hypergraphs, and that separation can be done without the ellipsoid method. The paper also shows (Proposition 5, a separate mission of this series) that β-acyclicity is necessary for $\mathrm{MP}_G=\mathrm{MP}^{\mathrm{RI}}_G$, so the characterization sits close to the boundary of what such relaxations can achieve.

All results of this mission are proved in the paper; none is machine-checked. A complete development would be the first formal treatment of hypergraph acyclicity degrees and of multilinear polytopes, and would include a formal Fourier–Motzkin elimination argument on a structured polytope.

Difficulty

The inclusion $\mathrm{MP}_G\subseteq\mathrm{MP}^{\mathrm{RI}}_G$ is a validity check. The reverse inclusion is the content. A direct argument through integrality fails: for two-laminar β-acyclic hypergraphs, facets have general integer coefficients, so total unimodularity and balancedness arguments used for laminar hypergraphs do not apply. The decomposition step is also harder than in earlier work: the shared part of the two pieces may be an edge whose nodes are only partly covered by edges of one side, so a point cannot be written by pairing one vertex of each side. Finally, the induction lifts to $G^+$, which has an extra variable, and the projection back must be shown to produce only running intersection inequalities, which requires recognizing every Fourier–Motzkin combination as one.

Formalization scope

Nodes form a type α with Fintype and DecidableEq; a point is a function z : α ⊕ Finset α → ℝ, and every polytope of a hypergraph vanishes off that hypergraph's coordinates, so that polytopes of different hypergraphs, lifts and projections are literal sets in one space. Hypergraphs have no loops or parallel edges, as the paper assumes. Orderings are lists, 0-based. The relaxation quantifies over every center, every neighbor set, every running intersection ordering and every choice of the nodes $u_k$; the number of components counts isolated nodes and ignores loops. The standard linearization has no row $z_v\ge 0$, exactly as printed.

One hypothesis is added to the paper: no isolated nodes, on Theorem 3, Corollary 3, Theorem 2 and the inductive step. It is necessary: for $V=\{a,b,c\}$, $E=\{\{a,b\}\}$ the point with $z_c=-1$ and all other coordinates $0$ lies in $\mathrm{MP}^{\mathrm{RI}}_G$ but not in $\mathrm{MP}_G$. No other result carries it.

A trivializing formalization is ruled out by construction: restricting the relaxation to one fixed ordering or choice of $u_k$ would make the goal false rather than easy, and the goal is an equality of sets, not an inclusion.

A complete development needs: convex hulls of finite sets of 0/1 points, hypergraph connectivity, β-acyclicity and the running intersection property (Lemma 4 is a classical database-theory theorem of Beeri, Fagin, Maier and Yannakakis), and Fourier–Motzkin elimination. The hypergraph acyclicity layer is reusable beyond this mission, including by the two other missions of this series. Proofs of any milestone, and of reusable lemmas on hypergraph acyclicity, are welcome.

Selected references

• A. Del Pia, A. Khajavirad, The running intersection relaxation of the multilinear polytope, Math. Oper. Res. 46(3):1008–1037, 2021. https://doi.org/10.1287/moor.2021.1121
• A. Del Pia, A. Khajavirad, The multilinear polytope for acyclic hypergraphs, SIAM J. Optim. 28(2):1049–1076, 2018. https://doi.org/10.1137/16M1095998
• A. Del Pia, A. Khajavirad, On decomposability of multilinear sets, Math. Program. 170(2):387–415, 2018. https://doi.org/10.1007/s10107-017-1158-y
• C. Beeri, R. Fagin, D. Maier, M. Yannakakis, On the desirability of acyclic database schemes, J. ACM 30(3):479–513, 1983. https://doi.org/10.1145/2402.322389
• R. Fagin, Degrees of acyclicity for hypergraphs and relational database schemes, J. ACM 30(3):514–550, 1983. https://doi.org/10.1145/2402.322390

Motivation

Binary polynomial optimization asks for the maximum of a polynomial over $\{0,1\}^n$. Linearizing each monomial $\prod_{v\in e}z_v$ by a new variable $z_e$ turns the problem into a linear program over the convex hull of a set of 0/1 points, the multilinear polytope of the hypergraph whose edges are the monomials. Global solvers such as BARON build polyhedral relaxations of this polytope at every node of their branch-and-bound trees, so valid inequalities that are as strong as possible, that is, facet-defining, translate directly into smaller root gaps.

Del Pia and Khajavirad introduced running intersection inequalities in The running intersection relaxation of the multilinear polytope (Math. Oper. Res. 46 (2021) 1008–1037, doi:10.1287/moor.2021.1121). They generalize the flower inequalities of the same authors (SIAM J. Optim. 2018), which are facet-defining when the support hypergraph is $\gamma$-acyclic, to support hypergraphs that are not. This mission formalizes the paper's sufficient condition for a running intersection inequality to define a facet (§2.4, Proposition 4) together with the structural results it rests on.

Timeline. Crama (1993) studied the standard linearization; Del Pia and Khajavirad (2017, Math. Oper. Res.) proved that the multilinear polytope is full dimensional and gave lifting theorems for facets; flower inequalities followed in 2018; running intersection inequalities and the facet conditions formalized here appeared in 2021.

Setting

A hypergraph $G=(V,E)$ has a finite node set $V$ and a set $E$ of subsets of $V$ of cardinality at least two. Its multilinear set is

$$\mathcal S_G=\Big\{z\in\{0,1\}^{V+E}:\ z_e=\prod_{v\in e}z_v\ \ \forall e\in E\Big\},$$

and its multilinear polytope is $\mathrm{MP}_G=\operatorname{conv}\mathcal S_G$.

A multiset $F$ of sets has the running intersection property if its elements can be ordered $p_1,\dots,p_m$ so that each $p_k\cap(p_1\cup\dots\cup p_{k-1})$, $k\ge 2$, is contained in a single earlier $p_j$. Such an ordering defines $N(p_1)=\emptyset$ and $N(p_k)=p_k\cap\bigcup_{i<k}p_i$. A leaf of $F$ is an element that comes last in some such ordering.

Fix an edge $e_0$ (the center) and edges $e_k$, $k\in K$, adjacent to $e_0$ (the neighbors), such that the multiset $\tilde E=\{e_0\cap e_k:k\in K\}$ has the running intersection property. Choose an ordering of $\tilde E$, and for each $k$ with $N(e_0\cap e_k)\neq\emptyset$ a node $u_k\in N(e_0\cap e_k)$. The running intersection inequality is

$$-\sum_{k\in K:\,N(e_0\cap e_k)\neq\emptyset} z_{u_k}+\sum_{v\in e_0\setminus\bigcup_{k}e_k} z_v+\sum_{k\in K}z_{e_k}-z_{e_0}\ \le\ \omega-1,$$

where $\omega$ is the number of connected components of the hypergraph $\tilde G=(e_0,\tilde E)$. Its support hypergraph $G$ has node set $e_0\cup\bigcup_k e_k$ and edge set $\{e_0\}\cup\{e_k:k\in K\}$. An inequality defines a facet of $\mathrm{MP}_G$ if it is valid and the face it cuts out is nonempty of dimension $\dim\mathrm{MP}_G-1$.

Formalization targets

Goal: Proposition 4 (p. 1016)

Assume

1. $|e_0\cap e_k|\ge 2$ for every $k\in K$;
2. for every $K'\subseteq K$ with $e_0\cap\bigcap_{k\in K'}e_k\neq\emptyset$: $\ e_0\cap\big(e_i\setminus\bigcup_{k\in K'\setminus\{i\}}e_k\big)\neq\emptyset$ for all $i\in K'$;
3. each nonempty $N(e_0\cap e_k)$ meets $U=\{u_k: N(e_0\cap e_k)\neq\emptyset\}$ in exactly one node.

Then the running intersection inequality defines a facet of $\mathrm{MP}_G$ for its support hypergraph $G$.

Milestones

Lemma 1 (p. 1011, leaves and reorderings), Lemma 2 (p. 1011, components $=n_0+|\{e:N(e)=\emptyset\}|$), Proposition 1 (p. 1012, validity), and the full dimensionality of $\mathrm{MP}_G$ (cited on p. 1016 from [12]):

$$\dim\mathrm{MP}_G=|V|+|E|.$$

Companions

Corollary 2 (p. 1017): $|e_0\cap e_k|\ge 2$ and $|e_0\cap e_k\cap e_{k'}|\le 1$ for $k\neq k'$ suffice. Proposition 2 and Corollary 1 (pp. 1013–1014): the multiset $\{N(e)\}$, hence the system of inequalities, does not depend on the ordering. Proposition 3 (p. 1014): necessary conditions for a facet of the running intersection relaxation $\mathrm{MP}^{\mathrm{RI}}_G$.

Significance

Proposition 4 certifies a large family of facets of multilinear polytopes whose support hypergraphs contain cycles that flower inequalities cannot handle. Together with the lifting theorems of Del Pia and Khajavirad (2017), it yields sufficient conditions under which these inequalities define facets of the multilinear polytope of general hypergraphs (p. 1015); §2.5 of the paper reports that running intersection cuts reduce BARON's root-node relaxation gap on image-restoration instances. Proposition 3 and Example 1 show that condition 1 is necessary while conditions 2–3 are not, so the result is a sufficient condition and not a characterization.

The results are proved in the paper; none is formalized. A Lean development would provide the first machine-checked library for the running intersection property (orderings, leaves, the multiset of $N$-sets), the connected-component count of Lemma 2, and the multilinear polytope as a convex hull with an exact dimension count, all reusable for the companion missions on the tightness of $\mathrm{MP}^{\mathrm{RI}}_G$ for kite-free $\beta$-acyclic hypergraphs and its strictness otherwise.

Difficulty

Validity (Proposition 1) decomposes over the connected components of $\tilde G$; the facet claim does not, because a face of codimension one is a global object and the neighbors of different components, and the nodes $u_k$ shared between neighbors, interact in it. Conditions 2 and 3 are exactly where this interaction is controlled, and Example 1 of the paper shows that dropping condition 3 does not destroy facetness, so no simple equivalence is available to fall back on. Formally, three nontrivial ingredients have no Mathlib counterpart: the combinatorics of running intersection orderings (Lemma 1, Proposition 2), the count of connected components of a hypergraph with loops and parallel edges (Lemma 2), and the affine dimension of a convex hull of 0/1 points in a space indexed by nodes and edges.

Formalization scope

Nodes form a finite type α; every hypergraph's space $\mathbb R^{V+E}$ lives inside α ⊕ Finset α → ℝ, with the coordinates outside $V+E$ pinned to $0$ in the definition of $\mathcal S_G$, so $\dim\mathrm{MP}_G=|V|+|E|$ is meaningful. Orderings are lists indexed from $0$. The number of components is that of the 2-section graph on the node set. An inequality is given by its data: center, a set $K$ of distinct neighbors other than $e_0$, an ordering of $K$ whose traces form a running intersection ordering of $\tilde E$, and the choice $k\mapsto u_k$; the first sum runs over neighbors, so a node chosen for two neighbors has coefficient $-2$. "Defines a facet" requires a nonempty face and compares dimensions as $\dim F+1=\dim P$, so the empty face can never qualify and no truncated subtraction occurs. The facet statement is about $\mathrm{MP}_G$ for the support hypergraph only, not for a larger host hypergraph, which would require the lifting theorems. The reading $k\neq k'$ is used where the page's "for all $k,k'$" would otherwise be contradictory (Corollary 2, Proposition 3(i)); Lemma 2 is stated for lists of nonempty sets, which covers its use on $\tilde G$.

Contributions welcome: proofs of the milestones, a reusable library for the running intersection property and $\alpha$-acyclic hypergraphs, and the full-dimensionality proof.

Selected references

• A. Del Pia, A. Khajavirad, The running intersection relaxation of the multilinear polytope, Math. Oper. Res. 46(3):1008–1037, 2021. https://doi.org/10.1287/moor.2021.1121
• A. Del Pia, A. Khajavirad, A polyhedral study of binary polynomial programs, Math. Oper. Res. 42(2):389–410, 2017. https://doi.org/10.1287/moor.2016.0804
• A. Del Pia, A. Khajavirad, The multilinear polytope for acyclic hypergraphs, SIAM J. Optim. 28(2):1049–1076, 2018. https://doi.org/10.1137/16M1095998
• C. Beeri, R. Fagin, D. Maier, M. Yannakakis, On the desirability of acyclic database schemes, J. ACM 30(3):479–513, 1983. https://doi.org/10.1145/2402.322389
• Y. Crama, Concave extensions for nonlinear 0–1 maximization problems, Math. Programming 61:53–60, 1993. https://doi.org/10.1007/BF01582138

Motivation

Sinkhorn distributionally robust optimization (Wang, Gao and Xie, arXiv:2109.11926) hedges a learning or decision problem against distribution shift. It minimizes the worst-case expected loss over all distributions within an entropically regularized optimal-transport distance (the Sinkhorn distance) of a nominal distribution $\widehat{\mathbb P}$. Strong duality, the subject of the first mission of this series, reduces the problem at a fixed Lagrange multiplier $\lambda>0$ to minimizing an objective of nested-expectation form,

$$F(\theta)=\mathbb E_{x\sim\widehat{\mathbb P}}\Big[\lambda\epsilon\log\mathbb E_{z\sim\mathbb Q_{x}}\big[e^{f_\theta(z)/(\lambda\epsilon)}\big]\Big].$$

A logarithm sits between the two expectations, so a mini-batch of samples gives a biased estimate of $F$ and of its subgradients, and stochastic gradient methods do not apply directly. Problems of this shape are known as conditional stochastic optimization (Hu, Chen and He 2020, 2021; references [54], [55] of arXiv:2109.11926v5). The paper's algorithmic contribution is a biased stochastic mirror descent (BSMD) for this objective, with two subgradient estimators and explicit complexity guarantees. This mission formalizes that guarantee, Theorem 2 of the paper.

Setting

The decision $\theta$ lives in a closed convex set $\Theta\subseteq\mathbb R^{d_\theta}$. A norm $\|\cdot\|$ on $\mathbb R^{d_\theta}$ satisfies $\mathfrak c\|\cdot\|_2\le\|\cdot\|\le\mathfrak d\|\cdot\|_2$ with $\mathfrak c>0$ (Assumption EC.1), and has dual norm $\|\cdot\|_*$. A distance generating function $\omega$ is continuously differentiable on $\Theta$ and $\kappa$-strongly convex with respect to $\|\cdot\|$. It induces the Bregman divergence $D_\omega(\theta,\theta')=\omega(\theta')-\omega(\theta)-\langle\nabla\omega(\theta),\theta'-\theta\rangle$ and the prox-mapping $\mathrm{Prox}_\theta(y)=\arg\min_{\theta'\in\Theta}\{\langle y,\theta'-\theta\rangle+D_\omega(\theta,\theta')\}$.

The data are a probability measure $\widehat{\mathbb P}$ and a Markov kernel $x\mapsto\mathbb Q_x$ on a measurable space $\mathcal Z$, fixed $\lambda,\epsilon>0$, and a loss $f_\theta(z)$. Assumption 2 requires three things: (I) $f_\theta(z)$ is convex in $\theta$; (II) it is $L_f$-Lipschitz in $\theta$ for the Euclidean norm; (III) $0\le f_\theta(z)\le B$ for $\theta\in\Theta$. Write $K=B/(\lambda\epsilon)$.

The level-$\ell$ approximation replaces the inner expectation by an average of $2^\ell$ i.i.d. draws:

$$F^\ell(\theta)=\mathbb E\Big[\lambda\epsilon\log\Big(2^{-\ell}\textstyle\sum_{j=1}^{2^\ell}e^{f_\theta(z_j)/(\lambda\epsilon)}\Big)\Big],\qquad x\sim\widehat{\mathbb P},\ z_j\mid x\sim\mathbb Q_x .$$

Its sample subgradient is $g^\ell$. The SG estimator is $v^{SG}=g^L$. The RT-MLMC estimator draws a level $\hat\ell\in\{0,\dots,L\}$ with probability $p_\ell=2^{-\ell}/(2-2^{-L})$ and returns $p_{\hat\ell}^{-1}G^{\hat\ell}$, where $G^\ell$ is the antithetic difference between the level-$\ell$ subgradient and the average of its two half-sample versions. BSMD iterates $\theta_{t+1}=\mathrm{Prox}_{\theta_t}(h\,v(\theta_t))$, $t=0,\dots,T-1$, with a fresh sample at every step.

Formalization targets

Goal: Theorem 2 with the explicit parameters of its proof

For $\delta>0$ let $L=\max\big(1,\lceil\log_2(2\lambda\epsilon e^{2K}/\delta)\rceil\big)$, $\theta^*\in\arg\min_\Theta F$, $\bar\theta^*\in\arg\min_\Theta F^L$ and $D=D_\omega(\theta_0,\bar\theta^*)$. With the SG estimator and

$$T=\Big\lceil\frac{8L_f^2D}{\kappa\mathfrak c^2\delta^2}\Big\rceil,\qquad h=\sqrt{\frac{2\kappa\mathfrak c^2D}{TL_f^2}},$$

or with the RT-MLMC estimator, $M^2=2(L+1)L_f^2e^{4K}/\mathfrak c^2$ and

$$T=\Big\lceil\frac{16(L+1)L_f^2De^{4K}}{\kappa\mathfrak c^2\delta^2}\Big\rceil,\qquad h=\sqrt{\frac{2\kappa D}{TM^2}},$$

the average $\hat\theta$ of the iterates is δ-optimal:

$$\mathbb E[F(\hat\theta)]-F(\theta^*)\le\delta .$$

Milestones

1. §4.1.1 (p. 15): $\mathbb E g^\ell$ is a subgradient of $F^\ell$, $\mathbb E G^\ell=\mathbb E g^\ell-\mathbb E g^{\ell-1}$, and hence $\mathbb E v^{RT\text{-}MLMC}=\mathbb E v^{SG}$.
2. Lemma EC.6 (I): $|F^\ell-F|\le\lambda\epsilon e^{2K}2^{-(\ell+1)}$ on $\Theta$.
3. Lemma EC.6 (III): $\mathbb E\|g^\ell\|_2^2\le L_f^2$ and $\mathbb E\|G^\ell\|_2^2\le L_f^2e^{4K}2^{-\ell}$.
4. Lemma EC.7: BSMD with subgradient bias $\Delta_F$ and second moment $M_*^2$ satisfies $\mathbb E[F(\hat\theta)-F(\theta^*)]\le2\Delta_F+M_*\sqrt{2D/(\kappa T)}$.
5. The RT-MLMC second-moment bound $\mathbb E\|v^{RT\text{-}MLMC}\|_*^2\le2(L+1)L_f^2e^{4K}/\mathfrak c^2$ (p. ec20).

Significance

Theorem 2 converts into sample complexities: $O(\delta^{-2})$ draws from $\widehat{\mathbb P}$ with either estimator. From $\mathbb Q_x$, SG needs $O(\lambda\epsilon e^{2K}\delta^{-3})$ draws and RT-MLMC $\tilde O(K^2e^{4K}\delta^{-2})$. The $\widehat{\mathbb P}$-rate matches the lower bound for general convex stochastic programming. This is what makes Sinkhorn DRO computationally competitive with empirical risk minimization, and it is the inner oracle of the paper's bisection search over $\lambda$ (Theorem 3, not part of this mission). Lemma EC.7 is a reusable statement in its own right: mirror descent with uniformly biased stochastic subgradients loses only an additive $2\Delta_F$.

The result is proved in the paper, partly by citation: the bias and variance bounds are attributed to Hu et al. and the BSMD bound to Nemirovski et al. To our knowledge none of it is machine-checked. The mission produces a self-contained Lean proof and, along the way, a formal mirror-descent analysis with biased oracles and an MLMC variance bound for log-sum-exp functionals.

Difficulty

The obvious route is to treat $v$ as an unbiased stochastic subgradient of $F$ and cite standard stochastic mirror descent. That fails because $\mathbb E v$ is a subgradient of $F^L$, not of $F$. Closing the gap requires the uniform bias bound of Lemma EC.6 (I), a second-order Taylor bound for $\log$ on $[1,e^K]$ against the variance of a sample mean. The RT-MLMC bound requires the antithetic cancellation in $G^\ell$ to be exhibited explicitly. The naive bound $\|G^\ell\|\le2L_f$ gives no decay in $\ell$, and the estimator's second moment then grows like $2^L$ instead of $L$. Finally, the expectation over a run of $T$ dependent iterates needs a careful product-measure argument: the iterate $\theta_t$ is a function of $\xi_0,\dots,\xi_{t-1}$, and $\xi_t$ is independent of it.

Formalization scope

• Representation. $\mathbb R^{d_\theta}$ is EuclideanSpace ℝ (Fin d). The mirror norm is a function with the norm axioms and Assumption EC.1, and its dual norm is a real supremum over its unit ball. $\nabla\omega$ is a gradient within $\Theta$.

• Prox-mapping. It is a map characterized by its argmin property on $\Theta$.

• The kernel. $\mathbb Q$ is an arbitrary Markov kernel. This contains the paper's Gibbs kernel $\mathbb Q_{x,\epsilon}$, which the BSMD analysis never uses.

• Subgradients. "$\nabla_\theta$" always means a selected subgradient; no differentiability of the loss is assumed. $g^\ell$ and $G^\ell$ are given in explicit chain-rule form, the same selected subgradients in every block.

• Randomness. A run of length $T$ is driven by $T$ i.i.d. samples under Measure.pi. The RT-MLMC sample is $(\hat\ell,x,z_1,\dots,z_{2^L})$, with level $\hat\ell$ reading the first $2^{\hat\ell}$ draws.

• Measurability and integrability. The prox-mapping and the subgradient selector are measurable. Every expectation in a conclusion comes with its integrability, which rules out a vacuous reading in which a non-integrable quantity has expectation $0$.

• Explicit forms of the paper's $O(\cdot)$. The paper writes $O(\cdot)$ and $\tilde O(\cdot)$; its proof (p. ec20) yields the hyper-parameters stated above. They are fixed in the goal, not quantified existentially:

  • $L=\max(1,\lceil\log(2\lambda\epsilon e^{2K}/\delta)/\log2\rceil)$ for both estimators;
  • SG: $T=\max(1,\lceil8L_f^2D/(\kappa\mathfrak c^2\delta^2)\rceil)$ and $h=\sqrt{2\kappa\mathfrak c^2D/(TL_f^2)}$;
  • RT-MLMC: $M^2=2(L+1)L_f^2e^{4K}/\mathfrak c^2$, $T=\max(1,\lceil16(L+1)L_f^2De^{4K}/(\kappa\mathfrak c^2\delta^2)\rceil)$ and $h=\sqrt{2\kappa D/(TM^2)}$.

  The max 1 guards enforce the paper's $L\in\mathbb N_+$ and $T\ge1$. The sample counts are not stated as Lean claims, since they follow by construction: per iteration, one draw from $\widehat{\mathbb P}$, plus $2^L$ draws from $\mathbb Q_x$ for SG or $(L+1)/(2-2^{-L})$ in expectation for RT-MLMC. Remark EC.1 prints the latter as $L/(2-2^{-L})$.

• Two corrections to the printed text.

  • The output averages $\theta_0,\dots,\theta_{T-1}$. The paper prints $\theta_1,\dots,\theta_T$, for which Lemma EC.7 has a two-dimensional counterexample with $T=1$ (in the Lemma EC.7 item).
  • The RT-MLMC constant $M^2$ keeps the factor $\mathfrak c^{-2}$ that the paper's display drops; the paper's $T$ already carries it. Both versions agree in the Euclidean case $\mathfrak c=1$.

• Contributions welcome. Proofs of the milestones. A reusable Lean development of stochastic mirror descent with biased oracles. The MLMC bias and variance lemmas for $\log$ of a sample mean. A follow-up mission on the bisection search (Theorem 3).

Selected references

• J. Wang, R. Gao, Y. Xie, Sinkhorn Distributionally Robust Optimization, arXiv:2109.11926v5, 2025. https://arxiv.org/abs/2109.11926v5
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust Stochastic Approximation Approach to Stochastic Programming, SIAM J. Optim. 19(4):1574–1609, 2009 (reference [77] of arXiv:2109.11926v5).
• Y. Hu, X. Chen, N. He, Sample Complexity of Sample Average Approximation for Conditional Stochastic Optimization, SIAM J. Optim. 30(3):2103–2133, 2020 (reference [54] of arXiv:2109.11926v5).
• Y. Hu, X. Chen, N. He, On the Bias-Variance-Cost Tradeoff of Stochastic Optimization, NeurIPS 2021 (reference [55] of arXiv:2109.11926v5).
• J. H. Blanchet, P. W. Glynn, Unbiased Monte Carlo for Optimization and Functions of Expectations via Multi-Level Randomization, Winter Simulation Conference, 3656–3667, 2015 (reference [22] of arXiv:2109.11926v5).

Motivation

Distributionally robust optimization (DRO) hedges a decision against uncertainty in the data distribution. It minimizes the worst-case expected loss over an ambiguity set of distributions around a nominal one, typically the empirical distribution of the data. Ambiguity sets built from the Wasserstein (optimal-transport) distance are standard in operations research and machine learning, because they contain distributions with supports different from the nominal one. A known drawback is that the worst case is attained at discrete distributions, which is unrealistic when the true distribution is continuous.

Wang, Gao and Xie (arXiv:2109.11926v5) replace the Wasserstein distance by the Sinkhorn distance, the entropically regularized optimal-transport cost of Cuturi (NeurIPS 2013). Their main theorem is a strong duality result: the infinite-dimensional worst-case problem over a Sinkhorn ball equals a one-dimensional convex minimization. This mission formalizes that theorem.

Timeline:

• 2013: Cuturi introduces the Sinkhorn distance as a fast surrogate for optimal transport.
• 2016–2023: strong duality for Wasserstein DRO, by Gao and Kleywegt (arXiv:1604.02199), Blanchet and Murthy (arXiv:1604.01446), and Zhang, Yang and Gao (arXiv:2205.00362).
• 2021–2025: Wang, Gao and Xie prove strong duality for Sinkhorn DRO for a general measurable sample space, a measurable loss and an arbitrary nominal distribution.

Setting

Let $\mathcal Z$ be a measurable space. The data are:

• a nominal probability distribution $\widehat{\mathbb P}$;
• a σ-finite reference measure $\nu\neq0$;
• a transport cost $c:\mathcal Z\times\mathcal Z\to[0,\infty]$;
• a regularization parameter $\epsilon>0$ and a radius $\rho\in\mathbb R$;
• a loss $f:\mathcal Z\to\mathbb R\cup\{\infty\}$.

For a probability distribution $\mathbb P$, the Sinkhorn distance (Definition 1, with reference measures $\widehat{\mathbb P}$ and $\nu$) is

$$\mathcal W_\epsilon(\widehat{\mathbb P},\mathbb P)=\inf_{\gamma\in\Gamma(\widehat{\mathbb P},\mathbb P)}\mathbb E_{(x,y)\sim\gamma}\Big[c(x,y)+\epsilon\log\frac{d\gamma(x,y)}{d\widehat{\mathbb P}(x)\,d\nu(y)}\Big],$$

where $\Gamma(\widehat{\mathbb P},\mathbb P)$ is the set of couplings with these marginals. The primal value is the worst-case expected loss over the Sinkhorn ball,

$$V=\sup\big\{\mathbb E_{\mathbb P}[f]:\ \mathcal W_\epsilon(\widehat{\mathbb P},\mathbb P)\le\rho\big\}.$$

The dual problem uses three more objects. The kernel distribution is $d\mathbb Q_{x,\epsilon}(z)\propto e^{-c(x,z)/\epsilon}\,d\nu(z)$. The adjusted radius is $\bar\rho=\rho+\epsilon\,\mathbb E_{x\sim\widehat{\mathbb P}}[\log\mathbb E_{z\sim\nu}e^{-c(x,z)/\epsilon}]$. The dual value is

$$V_D=\inf_{\lambda\ge0}\Big\{\lambda\bar\rho+\lambda\epsilon\,\mathbb E_{x\sim\widehat{\mathbb P}}\Big[\log\mathbb E_{z\sim\mathbb Q_{x,\epsilon}}\big[e^{f(z)/(\lambda\epsilon)}\big]\Big]\Big\},$$

where the objective at $\lambda=0$ is $\operatorname{ess\,sup}_\nu f$.

Assumption 1 requires:

• $c$ is measurable and, for $\widehat{\mathbb P}$-a.e. $x$, finite $\nu$-a.e.;
• $\mathbb E_\nu e^{-c(x,\cdot)/\epsilon}<\infty$ for $\widehat{\mathbb P}$-a.e. $x$;
• $f$ is measurable;
• every coupling with first marginal $\widehat{\mathbb P}$ disintegrates along $\widehat{\mathbb P}$.

Condition 1 asks for some $\lambda>0$ with $\mathbb E_{\mathbb Q_{x,\epsilon}}[e^{f/(\lambda\epsilon)}]<\infty$ for $\widehat{\mathbb P}$-a.e. $x$.

Formalization targets

Goal: Theorem 1 (strong duality)

Under Assumption 1:

$$\text{(I) }\ \exists\,\mathbb P:\ \mathcal W_\epsilon(\widehat{\mathbb P},\mathbb P)\le\rho\iff\bar\rho\ge0;\qquad \text{(II) }\ \bar\rho\ge0\implies V=V_D.$$

(III) If $\bar\rho>0$, then $V=V_D<\infty$ when the dual objective is finite at some $\lambda>0$, and $V=V_D=\infty$ otherwise.

(IV) If $\bar\rho>0$ and Condition 1 holds, then $0$ is the unique dual minimizer if and only if

$$\operatorname{ess\,sup}_\nu f<\infty\quad\text{and}\quad\bar\rho\ge\epsilon\,\mathbb E_{x\sim\widehat{\mathbb P}}\big[\log\big(1/\mathbb Q_{x,\epsilon}(A)\big)\big],\qquad A=\{f=\operatorname{ess\,sup}_\nu f\}.$$

Milestones

The milestones are the numbered lemmas of the paper's proof, in the order the proof uses them:

• Lemma EC.2: the Gibbs variational principle, $\sup_{\mathbb P\ll\nu}\mathbb E_{\mathbb P}[f-\tau\log\frac{d\mathbb P}{d\nu}]=\tau\log\mathbb E_\nu e^{f/\tau}$.
• Lemma EC.3: measurability of the inner value $x\mapsto v_x(\lambda)$.
• Lemma 1: weak duality $V\le V_D$.
• Lemma 2: a KL-constrained reformulation of the primal problem.
• Lemma EC.4: existence of a dual minimizer.
• Lemma 3: the first-order condition (9) and uniqueness when $\lambda^*>0$.
• Lemma EC.5: the criterion for $\lambda^*=0$.

Significance

The result. Theorem 1 turns a supremum over an infinite-dimensional set of distributions into a scalar convex program. That program can be solved by first-order methods using only samples from $\widehat{\mathbb P}$ and from the kernels $\mathbb Q_{x,\epsilon}$, which is the basis of the paper's algorithm (Section 4). The proof also constructs the worst-case distribution: it is absolutely continuous with respect to $\nu$, not discrete. Theorem 1(IV) says exactly when the ambiguity constraint is binding. The finite-support conic reformulation (Corollary 1) and the closed form for linear losses (Example 1) both follow from the theorem.

Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. Formalization adds two things. First, it pins down the extended-valued conventions: $V$, $V_D$ and $f$ all take values in $[-\infty,\infty]$, and the paper does not specify how undefined expectations and the $\lambda=0$ objective are treated. Second, it checks every case of the proof, including the degenerate ones. Doing so has already corrected two statements; see Formalization scope.

Difficulty

Weak duality (Lemma 1) is Lagrangian relaxation plus the Gibbs principle. The difficulty is the reverse inequality $V\ge V_D$. Interchanging the supremum over distributions with the infimum over $\lambda$ requires a minimax theorem. The usual minimax theorems need compactness or semicontinuity in the distribution variable. The paper's setting has neither: $\mathcal Z$ is an arbitrary measurable space, $f$ is only measurable and may be $+\infty$, and $\widehat{\mathbb P}$ is arbitrary. So a minimax theorem cannot be applied directly.

The proof instead constructs near-optimal primal distributions from the dual minimizer. This needs three separate cases:

• $\lambda^*>0$, with a first-order condition;
• $\lambda^*=0$, with a distribution concentrated on the essential maximizers of $f$;
• Condition 1 fails, with a truncation argument.

Each case needs integrability facts about $\mathbb E_{\mathbb Q_{x,\epsilon}}[e^{f/(\lambda\epsilon)}]$ in which $x$ and $\lambda$ interact. Disintegrating couplings (Assumption 1(IV)) and making the extended-valued expectations meaningful are a further source of work in Lean.

Formalization scope

All values (primal value, Sinkhorn distance, dual objective) are EReal. Expectations are the published DupacovaWets.Consistency.expect: $\int g^+-\int g^-$, with lower Lebesgue integrals in $[0,\infty]$ and the convention $\infty-\infty=+\infty$. The Bochner integral appears only in $\bar\rho$, which every theorem assumes finite.

Further conventions:

• Sinkhorn distance. The cost and the entropy form a single integrand. A coupling not absolutely continuous with respect to $\widehat{\mathbb P}\otimes\nu$ contributes $+\infty$. An infeasible primal has $V=-\infty$.
• Dual objective. The value at $\lambda=0$ is defined as Mathlib's essSup f ν, not as a limit. Logarithms are ENNReal.log, so $\log\infty=\infty$ and $\log 0=-\infty$; $e^{+\infty}=+\infty$.
• Kernels. $\mathbb Q_{x,\epsilon}$ is a normalized withDensity measure. Families $\{\gamma_x\}_{x\in\operatorname{supp}\widehat{\mathbb P}}$ are Markov kernels on all of $\mathcal Z$.

Hypotheses added to the page:

• $\nu$ is σ-finite and nonzero;
• $\epsilon>0$;
• $x\mapsto\log\mathbb E_\nu e^{-c(x,\cdot)/\epsilon}$ is $\widehat{\mathbb P}$-integrable, so that $\bar\rho\in\mathbb R$.

"$\nu\{0\le c<\infty\}=1$" is read as "$\nu$-a.e.". "$\lambda^*=0$" is read as "$0$ is the unique dual minimizer".

Corrections to the paper:

• Theorem 1(III). The paper's version with Condition 1 is false: a.e.-finite inner expectations do not make the dual objective finite. A counterexample on $\mathbb N$ is in the goal's note. The goal is stated with the integrated condition "the dual objective is finite at some $\lambda>0$".
• Lemma 3. The lemma is stated under the added hypothesis that the dual objective is finite at some $\lambda_1<\lambda^*$ (and is not $-\infty$ at $\lambda^*$). Without it, $\lambda^*$ can sit at the edge of the domain where the objective is finite, and (9) fails.

No statement involves an $O(\cdot)$ constant.

A formalization that lets an undefined Sinkhorn integrand evaluate to $-\infty$ (Mathlib's $\top+\bot=\bot$) is ruled out: it would put every distribution into the ball and make the theorem trivial. The combined integrand and the $+\infty$ convention exclude this.

A complete development needs:

• a Gibbs/Donsker–Varadhan variational principle for σ-finite reference measures and extended-valued functions;
• disintegration of couplings;
• convexity and differentiation of $\lambda\mapsto\lambda\log\mathbb E e^{f/\lambda}$.

The first two are reusable well beyond this mission. Contributions toward any milestone, and toward these general lemmas, are welcome.

Selected references

• J. Wang, R. Gao, Y. Xie, Sinkhorn Distributionally Robust Optimization, arXiv:2109.11926v5, 2025. https://arxiv.org/abs/2109.11926
• M. Cuturi, Sinkhorn Distances: Lightspeed Computation of Optimal Transport, NeurIPS, 2013. https://arxiv.org/abs/1306.0895
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1604.02199
• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research, 2019. https://arxiv.org/abs/1604.01446
• L. Zhang, J. Yang, R. Gao, A Short and General Duality Proof for Wasserstein Distributionally Robust Optimization, Operations Research, 2024. https://arxiv.org/abs/2205.00362

Motivation

Policy gradient methods are the main family of reinforcement learning algorithms that search directly over a parameterized class of stochastic policies $\pi_\theta$, $\theta\in\mathbb R^d$, by stochastic gradient ascent on the expected discounted return. They underlie REINFORCE, actor-critic methods and their deep-learning descendants. The return is a nonconvex function of $\theta$, and the gradient is available only through Monte Carlo samples of trajectories, so the basic question is what the iterates of such a method converge to.

Classical analyses of actor-critic algorithms (Konda and Tsitsiklis, 2003) use the ODE method of stochastic approximation and assume that the gradient estimate is unbiased. In the infinite-horizon discounted setting, a trajectory of finite length cannot by itself produce an unbiased sample of the gradient. Zhang, Koppel, Zhu and Başar (arXiv:1906.08383, SIAM J. Control Optim. 58(6), 2020) resolve this with random horizons: drawing the trajectory lengths from geometric distributions makes the resulting estimate exactly unbiased and almost surely bounded. They then prove convergence of the resulting random-horizon policy gradient (RPG) algorithm with the supermartingale convergence theorem, an optimization argument that also yields rates. This mission formalizes that first part of the paper (§2–§4 and App. A.1–A.4). The paper's later results on escaping saddle points are not part of it.

Setting

A finite Markov decision process is a tuple $(\mathcal S,\mathcal A,P,R,\gamma)$: finite state and action sets, transition probabilities $P(s'\mid s,a)$, rewards $R(s,a)$ and a discount factor $\gamma\in(0,1)$. A stochastic policy $\pi$ gives a probability vector $\pi(\cdot\mid s)$ on $\mathcal A$ at each state. Its value $V_\pi(s)=\mathbb E\big(\sum_{t\ge0}\gamma^tR(s_t,a_t)\mid s_0=s\big)$ and Q-function $Q_\pi(s,a)$ are the expected discounted returns from a state, respectively a state-action pair.

A parameterized policy assigns to each $\theta\in\mathbb R^d$ a policy $\pi_\theta$. Fix an initial state $s_0$. The objective is

$$J(\theta)=V_{\pi_\theta}(s_0),\qquad \max_{\theta\in\mathbb R^d}J(\theta).$$

The score function is $\nabla_\theta\log\pi_\theta(a\mid s)$. The discounted state-occupancy measure is $\rho_{\pi_\theta}(s)=(1-\gamma)\sum_{t\ge0}\gamma^tp(s_t=s\mid s_0,\pi_\theta)$, and $\rho_\theta(s,a)=\rho_{\pi_\theta}(s)\pi_\theta(a\mid s)$.

Assumption 3.1 asks for $|R(s,a)|\le U_R$ and for a differentiable policy whose score exists, is $L_\Theta$-Lipschitz in $\theta$ and is bounded in norm by $B_\Theta>0$. Two constants recur below:

$$L=\frac{U_RL_\Theta}{(1-\gamma)^2}+\frac{(1+\gamma)U_RB_\Theta^2}{(1-\gamma)^3},\qquad \hat\ell=\frac{B_\Theta U_R}{(1-\gamma)(1-\gamma^{1/2})}.$$

The RPG algorithm (Algorithm 3) works as follows at the current iterate $\theta_k$:

1. Draw a horizon $T\sim\mathrm{Geom}(1-\gamma)$ and simulate $s_0,a_0,\dots,s_T,a_T$ under $\pi_{\theta_k}$.
2. From the last pair $(s_T,a_T)$, the subroutine EstQ draws an independent $T'\sim\mathrm{Geom}(1-\gamma^{1/2})$, rolls out $T'$ further steps and returns $\hat Q=\sum_{t=0}^{T'}\gamma^{t/2}R(s_t,a_t)$.
3. Update

$$\theta_{k+1}=\theta_k+\alpha_k\hat\nabla J(\theta_k),\qquad \hat\nabla J(\theta)=\frac{1}{1-\gamma}\hat Q\,\nabla\log\pi_\theta(a_T\mid s_T).$$

Assumption 4.1 is the Robbins–Monro condition $\sum_k\alpha_k=\infty$, $\sum_k\alpha_k^2<\infty$.

Formalization targets

Goal: Theorem 4.2, in the form its proof establishes

Under Assumptions 3.1 and 4.1, almost surely

$$\lim_{k\to\infty}\|\nabla J(\theta_k)\|=0,$$

and almost surely every cluster point $\bar\theta$ of $(\theta_k)$ satisfies $\nabla J(\bar\theta)=0$. The page states the conclusion as "$\lim_k\theta_k\in\Theta^*$", where $\Theta^*$ is the set of stationary points. Read literally, that asserts convergence of $\theta_k$, which fails when $J$ has no stationary point at all (one state, two actions, a softmax policy). The goal states what the proof on p. 30 concludes.

Milestones

1. $|Q_\pi(s,a)|,|V_\pi(s)|\le U_R/(1-\gamma)$ (p. 6).
2. The policy gradient theorem (3.4): $\nabla J(\theta)=\frac1{1-\gamma}\mathbb E_{(s,a)\sim\rho_\theta}[\nabla\log\pi_\theta(a\mid s)Q_{\pi_\theta}(s,a)]$.
3. Lemma 3.2: $\nabla J$ is $L$-Lipschitz.
4. Theorem 3.4, $\hat\nabla J$ clauses: $\mathbb E\hat\nabla J(\theta)=\nabla J(\theta)$, $\|\nabla J(\theta)\|\le B_\Theta U_R/(1-\gamma)^2$, $\|\hat\nabla J(\theta)\|\le\hat\ell$ a.s.
5. Lemma A.1: the ascent inequality (A.23), and $W_k=J(\theta_k)-L\hat\ell^2\sum_{j\ge k}\alpha_j^2$ is a bounded submartingale with $\mathbb E[W_{k+1}\mid\mathcal F_k]\ge W_k+\alpha_k\|\nabla J(\theta_k)\|^2$.
6. (A.26): $\sum_k\alpha_k\|\nabla J(\theta_k)\|^2<\infty$ a.s.
7. (A.27): $\liminf_k\|\nabla J(\theta_k)\|=0$ a.s.

Companion: Corollary 4.4 in its explicit form (A.37)

With constant stepsize $\alpha>0$ and Assumption 3.1 only, for every $k\ge1$,

$$\frac1k\sum_{m=1}^k\mathbb E\|\nabla J(\theta_m)\|^2\le\frac{1}{k\alpha}\cdot\frac{2U_R}{1-\gamma}+L\alpha\hat\ell^2.$$

Significance

The theorem shows that Monte Carlo policy gradient, with a sampling scheme that can be implemented from simulated trajectories alone, behaves like an exact stochastic gradient method on a smooth nonconvex objective. It needs no ODE approximation, no two-timescale critic and no assumption that the estimate is unbiased: unbiasedness is proved (Theorem 3.4). The same estimates give the finite-time bound of Corollary 4.4 and are the starting point of the paper's second part, which adds perturbations to escape saddle points.

To our knowledge none of these results has been machine-checked. The mission's work is to formalize the known proof: the infinite-horizon policy gradient theorem with a vector parameter, the smoothness bound with its explicit constant, the exact law of the random-horizon estimator and its moments, and the supermartingale argument. The formal statements also repair three misprints of the source: the conclusion of Theorem 4.2, the tail $\sum_{j=k}^\infty\alpha_k^2$ of (A.22), which is read as $\sum_{j\ge k}\alpha_j^2$, and the $O(\cdot)$ of Corollary 4.4, which is replaced by its explicit form (A.37).

Difficulty

Each step of the argument is standard on paper. The work is in the parts that the paper treats in one line:

• Unbiasedness. It rests on two separate identities. The law of the last state of a $\mathrm{Geom}(1-\gamma)$-length trajectory is $\rho_{\pi_\theta}$. A $\gamma^{1/2}$-discounted sum over a $\mathrm{Geom}(1-\gamma^{1/2})$ horizon has the mean of a $\gamma$-discounted infinite sum. Both are exchanges of infinite sums over trajectories of unbounded length.
• Smoothness. Lemma 3.2 requires differentiating $J$ twice through an infinite series of policy-dependent transition matrices, with bounds uniform in $\theta$.
• The final step. (A.26) and the non-summability of the stepsizes give only $\liminf\|\nabla J(\theta_k)\|=0$. Upgrading this to a limit needs a separate pathwise argument, which uses the Lipschitz continuity of $\nabla J$ and the almost sure convergence of the martingale part of the iterates. The tempting first idea, that a summable series with non-summable weights forces its terms to zero, is false.

Formalization scope

• Finite case. The state and action spaces are finite types. The paper also allows compact real vector spaces; this mission does not cover them. Values, Q-functions and occupation probabilities are the published FoundationsML layer (PolicyValue, QFunction, OccupationDist, IsPolicy, IsTransitionKernel). $\mathbb R^d$ is EuclideanSpace ℝ (Fin d), and $\nabla$ is Mathlib's gradient.
• Assumption 3.1 includes $\pi_\theta(a\mid s)>0$: this is the reading of "the score function exists", since $\log 0$ is a junk value in Lean. It also states $L_\Theta\ge0$, which is implicit in "$L_\Theta$-Lipschitz".
• The algorithm is encoded by its exact sampling law. rpgLaw θ is the law of $\hat\nabla J(\theta)$, built from the geometric horizons, the trajectory probabilities and EstQ. A run is a filtered probability space carrying $\theta_k$ and $g_k$ with $\theta_{k+1}=\theta_k+\alpha_kg_k$ on every path, $\theta_k$ adapted, and the conditional law of $g_k$ given $\mathcal F_k$ equal to rpgLaw θ_k.
• Ruled out. Postulating an abstract "unbiased bounded oracle" in place of rpgLaw would assume Theorem 3.4 and turn the goal into generic SGD; that encoding is ruled out. A sorry-free example shows that the run hypothesis is satisfiable and that rpgLaw is a probability measure.
• Stepsizes and limits. The stepsizes are positive; the page says only "stepsize", and its proofs divide by $\alpha_k$. Divergence of $\sum\alpha_k$ is Tendsto of the partial sums to $+\infty$. "Cluster point" is MapClusterPt.
• Contributions welcome: proofs of any milestone, in particular the infinite-horizon policy gradient theorem with vector parameters and the unbiasedness of rpgLaw. These are reusable for every Monte Carlo policy gradient analysis.

Selected references

• K. Zhang, A. Koppel, H. Zhu, T. Başar, Global Convergence of Policy Gradient Methods to (Almost) Locally Optimal Policies, SIAM J. Control Optim. 58(6), 2020. https://arxiv.org/abs/1906.08383 (v3 is the source of this mission)
• R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 1999. https://papers.nips.cc/paper/1713-policy-gradient-methods-for-reinforcement-learning-with-function-approximation
• V. R. Konda, J. N. Tsitsiklis, On Actor-Critic Algorithms, SIAM J. Control Optim. 42(4), 2003. https://doi.org/10.1137/S0363012901385691
• D. P. Bertsekas, J. N. Tsitsiklis, Gradient Convergence in Gradient Methods with Errors, SIAM J. Optim. 10(3), 2000. https://doi.org/10.1137/S1052623497331063
• H. Robbins, D. Siegmund, A Convergence Theorem for Non Negative Almost Supermartingales and Some Applications, in Optimizing Methods in Statistics, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8