All missions

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

Networks of agents that interact both cooperatively and competitively are modelled by signed graphs: a positive edge weight means that one agent moves towards another, a negative weight means that it moves towards the other's opposite. Since Altafini's work on consensus over antagonistic networks (IEEE TAC 2013), the standard target on such networks has been bipartite consensus or bipartite tracking: the agents split into two camps that converge to values of equal size and opposite sign. With a leader, the camp containing the leader tracks the leader's state and the other camp tracks its negative.

Most analyses assume that all agents update at the same instants. In practice agents sample and communicate on their own clocks. Shi, Zheng, Shao and Cheng (arXiv:2004.01867v2, SIAM J. Control Optim. 2021) handle this asynchronous setting with a matrix tool: products of sub-stochastic matrices (nonnegative, row sums at most one) whose row-sum deficits propagate along the communication graph. This mission formalizes their first application, bipartite tracking of first-order agents with a static leader (§3).

Setting

There is one leader $v_0$ and $n$ followers $v_1,\dots,v_n$. Follower weights form a matrix $\mathcal A=[a_{ij}]\in\mathbb R^{n\times n}$: the edge $(v_j,v_i)$ exists iff $a_{ij}\neq 0$, cooperative if $a_{ij}>0$, competitive if $a_{ij}<0$. The number $a_{i0}$ is the weight of the leader edge $(v_0,v_i)$, which exists iff $a_{i0}\ne 0$. The digraph $\tilde{\mathcal G}$ consists of the followers' digraph, the leader and the leader edges.

• C1 (structural balance). The agents split as $\mathcal V_1\cup\mathcal V_2$ with $v_0\in\mathcal V_1$, every weight inside a set is $\ge 0$ and every weight between the sets is $\le 0$.
• C2 (leader reachability). Every follower is reached from $v_0$ by a directed path in $\tilde{\mathcal G}$.

Time is discrete with step size $\tau>0$. Follower $v_i$ communicates only at its own instants $s^i_0\tau<s^i_1\tau<\cdots$ with $s^i_0=0$ and

$$s^i_{k+1}-s^i_k\le h\qquad(2.10)$$

for a constant $h\in\mathbb Z_+$. Positions $x_i(k)\in\mathbb R^p$ evolve by $x_0(k+1)=x_0(k)$ and $x_i(k+1)=x_i(k)+\tau u_i(k)$, with the asynchronous protocol

$$u_i(k)=\psi\sum_{v_j\in\mathcal N_i}|a_{ij}|\big[\operatorname{sgn}(a_{ij})x_j(k)-x_i(k)\big]+\psi|a_{i0}|\big[\operatorname{sgn}(a_{i0})x_0(k)-x_i(k)\big]$$

at the instants of $v_i$, and $u_i(k)=0$ otherwise. Here $\psi>0$ is a gain. Bipartite tracking (Definition 3.1) means $\|x_i(k)-x_0(k)\|\to 0$ for $v_i\in\mathcal V_1$ and $\|x_i(k)+x_0(k)\|\to 0$ for $v_i\in\mathcal V_2$. With $d_M=\max_i\big(\sum_{v_j\in\mathcal N_i}|a_{ij}|+|a_{i0}|\big)$, the gain condition is

$$\psi<\frac{1}{\tau d_M}.\qquad(3.7)$$

In the error coordinates $e_i=x_i-x_0$ on $\mathcal V_1$ and $e_i=-x_i-x_0$ on $\mathcal V_2$, the closed loop is $e(k+1)=(M(k)\otimes I_p)e(k)$ with $M(k)=I_n-\tau\psi\mathcal D(k)-\tau\psi\mathcal B(k)+\tau\psi|\mathcal A(k)|$, where only the rows of followers active at time $k\tau$ differ from the identity.

Formalization targets

Goal: Theorem 3.3, sufficiency

$$\psi<\frac1{\tau d_M},\ \ \mathrm{C1},\ \ \mathrm{C2}\ \Longrightarrow\ \lim_{k\to\infty}\|x_i(k)-x_0(k)\|=0\ (v_i\in\mathcal V_1),\quad \lim_{k\to\infty}\|x_i(k)+x_0(k)\|=0\ (v_i\in\mathcal V_2),$$

for every choice of instants satisfying (2.10) and every initial state.

Milestones

1. Theorem 2.4 1): a product $F_q\cdots F_1$ of sub-stochastic matrices is sub-stochastic.
2. Theorem 2.4 2): with positive diagonals, if every row $i_2$ is fed through $[F_{s_2}]_{i_2i_1}>0$ by a row $i_1$ with $\Lambda_{i_1}[F_{s_1}]<1$, $s_1<s_2$, then $\|\prod_{s=1}^qF_s\|_\infty<1$ and $\rho(\prod_{s=1}^qF_s)<1$.
3. The matrices $M(k)$ (p. 15): under (3.7) they are sub-stochastic with positive diagonals, and $\Lambda_i[M(k)]<1$ exactly when $v_i$ hears the leader at $k\tau$.
4. Error system (3.6): under C1, $e_i(k+1)=\sum_j[M(k)]_{ij}e_j(k)$.
5. Lemma 3.2: under (3.7), C1 and C2, $\big\|\prod_{s=k}^{k+Ph-1}M(s)\big\|_\infty<1$ for every $k$, where $P=\max_i d(v_0,v_i)$ is the largest directed distance from the leader.

Significance

The theorem says that asynchrony costs nothing qualitatively: as long as every follower communicates at least once every $h$ steps and the gain respects (3.7), the network reaches bipartite tracking under the same topological conditions C1 and C2 as in the synchronous case. No common clock, dwell-time condition or joint connectivity of the switching graphs is required. The same product argument is reused in the rest of the paper for second-order and general linear agents, delays and switching topologies, so the milestones here are the base case of that series.

The result is proved in the paper; it has not been formalized. Formalizing it produces a checked theory of products of sub-stochastic matrices with row-sum deficits (Theorem 2.4), which applies to positive switched systems in general, and a reusable encoding of signed digraphs with a leader, structural balance and asynchronous protocols.

Difficulty

Each single matrix $M(k)$ is only marginally stable: its rows of followers that do not hear the leader at time $k\tau$ sum to exactly one, so no single step contracts, and the spectral radius of an individual $M(k)$ may equal one. Contraction appears only in products, and only once a deficit created at a leader edge has had time to travel along the paths of C2, one edge per window of $h$ steps; this requires that deficits never disappear again, which is where positive diagonals (from (3.7)) enter. The passage from "every window product has $\|\cdot\|_\infty<1$" to convergence also needs a uniform bound below one over all windows; the paper's (3.14) uses it without comment. The bound holds because $M(k)$ depends on $k$ only through the set of active followers, so the window products range over a finite set.

Formalization scope

Followers are Fin n (0-based) and the leader is not an index; $a_{ij}$ is a i j and $a_{i0}$ is b i. Positions lie in EuclideanSpace ℝ (Fin p); the paper's norm is unspecified and all norms on $\mathbb R^p$ give the same limits. Eigenvalues are complex: $\rho(F)<1$ means every element of spectrum ℂ of the complexified matrix has modulus $<1$. $\|F\|_\infty$ is the largest absolute row sum. Products multiply later factors on the left. $\operatorname{sgn}$ is Real.sign. The maxima $d_M$ and $P$ are given as values with IsGreatest hypotheses over exactly the printed sets, and (3.7) is kept as printed. C1 is stated for the partition $\mathcal V_1=\{v_0\}\cup V_1$, $\mathcal V_2=$ the remaining followers; fixing the leader in $\mathcal V_1$ is the paper's "with no loss of generality" convention. Definition 3.1 is stated for that same partition.

Only the "if" half of Theorem 3.3 is a target. Definition 3.1 presupposes the partition of C1, so necessity of C1 has no formal meaning, and the printed necessity argument is an informal case discussion. Theorem 2.4 2) is stated with one $(i_1,s_1,s_2)$ per row $i_2$, as its proof and the example on p. 8 use it; this is implied by the literal reading.

Three formalizations would trivialize the goal and are ruled out: a protocol in which every follower updates at every step (the synchronous special case, which drops the asynchronous instants); dropping the sign conditions of C1, or leaving the leader's side free, under which the followers of $\mathcal V_2$ need not approach $-x_0$; and a goal stated about the error system (3.6) instead of the agents' positions $x_i$.

The development needs finite matrix products, the ∞-norm bound on eigenvalues (Gershgorin), and elementary walk reachability in digraphs. All of these exist in Mathlib in some form. Contributions are welcome on every milestone. The product theorem 2.4 does not depend on the network model and is reusable for positive switched systems.

Selected references

• L. Shi, W. X. Zheng, J. Shao, Y. Cheng, Sub/super-stochastic matrix with applications to bipartite tracking control over signed networks, arXiv:2004.01867v2, 2020; SIAM J. Control Optim. 59 (2021). https://arxiv.org/abs/2004.01867, https://doi.org/10.1137/19M1239982
• C. Altafini, Consensus problems on networks with antagonistic interactions, IEEE Trans. Automat. Control 58(4), 2013. https://doi.org/10.1109/TAC.2012.2224251

Motivation

The Kolmogorov–Čentsov continuity criterion is the standard way to prove that a random field has a continuous version: a moment bound on increments, $\mathbf E|X_u - X_v|^\alpha \le c_0|u - v|^{d+\beta}$, yields a modification whose paths are Hölder continuous of every order $\gamma < \beta/\alpha$ (Karatzas–Shreve 1991, §2.2; Revuz–Yor 1999, Ch. I). It is used for Brownian motion, Brownian sheets, solutions of stochastic PDEs, Gaussian free field approximations and many other random fields.

The classical statement says only that the Hölder constant $M$ is finite almost surely. Many applications need more: a bound on the tail $\mathbf P[M \ge t]$ whose constant depends only on the parameters $\alpha, \beta, c_0$ and not on the particular field, so that the bound holds uniformly over a family of fields.

This mission formalizes such a quantitative version, Proposition 2.3 in §2.3 of J. Miller and S. Sheffield, Liouville quantum gravity and the Brownian map II: geodesics and continuity of the embedding (Ann. Probab. 2021). The authors state it, note that it follows "by carefully following the proof" of the classical criterion, and write the proof out (pp. 30–31). They apply it to the circle-average process of the Gaussian free field (Proposition 2.4, p. 33) and again in Lemma 5.12 (p. 63).

The paper's main theorems (the $\sqrt{8/3}$-Liouville quantum gravity sphere equipped with the QLE(8/3, 0) metric has the law of the Brownian map; continuity of the embedding) are not part of this mission. Their objects, among them the Gaussian free field, SLE$_6$, quantum surfaces, the QLE metric of Miller–Sheffield 2020 and the Brownian map, have no formal substrate in Mathlib or on the platform. Proposition 2.3 is a self-contained probabilistic tool that the paper proves in full, and it is statable today.

Setting

Fix a dimension $d \in \mathbb N$. The index set is the cube $[0,1]^d$ with the Euclidean distance $|u - v|$. A random field is a family $(X_u)_{u \in [0,1]^d}$ of real random variables on a probability space $(\Omega, \mathcal F, \mathbf P)$. The field satisfies the Kolmogorov condition with constants $\alpha, \beta, c_0 > 0$ if

$$\mathbf E\big[|X_u - X_v|^\alpha\big] \le c_0 |u - v|^{d+\beta} \qquad \text{for all } u, v \in [0,1]^d. \tag{2.6}$$

A modification of $X$ is a field $Y$ on the same space with $\mathbf P[Y_u = X_u] = 1$ for every $u$. For $\gamma > 0$, the $\gamma$-Hölder norm of a function $f$ on the cube is

$$M_\gamma(f) = \sup_{u \ne v} \frac{|f(u) - f(v)|}{|u - v|^\gamma} \in [0, \infty].$$

The proof works on the dyadic grid $\mathcal D_k$, the points of the cube whose coordinates are integer multiples of $2^{-k}$, and on the set $\widetilde{\mathcal D}_k$ of adjacent pairs $\{u, v\} \subseteq \mathcal D_k$, which differ in exactly one coordinate, by $2^{-k}$. In Lean the cube is Cube d, and the grid and the pairs are dyadicGrid d k and IsAdjacentPair d k u v.

Formalization targets

Goal: Proposition 2.3 (p. 30)

For every $\gamma \in (0, \beta/\alpha)$ there is a constant $c_1(\gamma) > 0$, depending only on $d, \alpha, \beta, \gamma, c_0$, such that every field satisfying (2.6) has one modification $Y$ with, for every $\gamma \in (0, \beta/\alpha)$,

$$\forall \omega\ \exists M > 0:\ |Y_u(\omega) - Y_v(\omega)| \le M|u - v|^\gamma \ \ \forall u, v, \tag{2.7}$$ $$\mathbf P\big[M_\gamma(Y(\omega)) \ge t\big] \le c_1(\gamma)\, t^{-\alpha} \qquad \text{for all } t \ge 1. \tag{2.8}$$

Milestones (attack order)

1. (2.9), p. 30: $\mathbf P[|X_u - X_v| \ge \delta] \le c_0 \delta^{-\alpha}|u - v|^{d+\beta}$.
2. (2.10), p. 31: for $\{u, v\} \in \widetilde{\mathcal D}_k$, $\mathbf P[|X_u - X_v| \ge t2^{-\gamma k}] \le c_0 t^{-\alpha} 2^{-k(d+\beta-\alpha\gamma)}$.
3. (2.11), p. 31: $\mathbf P[\max_{\widetilde{\mathcal D}_k} |X_u - X_v| \ge t2^{-\gamma k}] \le c_1 t^{-\alpha}2^{-k(\beta-\alpha\gamma)}$, with $c_1$ uniform in $k$, $t$ and the field (this $c_1$ is not the one of (2.8)).
4. (2.12), p. 31: $\mathbf P[\sup_k \max_{\widetilde{\mathcal D}_k} 2^{\gamma k}|X_u - X_v| \ge t] \le c_2 t^{-\alpha}$.
5. Closing claim of the proof, p. 31: a deterministic statement. If $2^{\gamma k}|f(u) - f(v)| \le t$ for all adjacent pairs at all levels, then $|f(u) - f(v)| \le c_3 t|u - v|^\gamma$ for all dyadic $u, v$, with $c_3$ depending on $d, \gamma$ only.
6. (2.7), p. 30: the classical criterion alone, a modification that is $\gamma$-Hölder for every $\gamma \in (0, \beta/\alpha)$.

Significance

The tail bound (2.8) is what makes the criterion usable for families of fields. In the paper, it bounds the modulus of continuity of the Gaussian free field circle averages at every scale with a single constant, which feeds the estimates on the Liouville quantum gravity metric. More generally, polynomial tails for Hölder norms with field-independent constants are the input to tightness arguments for sequences of random fields, to union bounds over many scales or many fields, and to moment bounds for Hölder norms.

The result itself is known: the authors derive it from the textbook proof, which they write out. What is missing is a machine-checked version. At the pinned Mathlib revision, ProbabilityTheory.IsKolmogorovProcess defines the hypothesis (2.6), but no continuity theorem is proved from it, qualitative or quantitative. The platform has an Open goal for the qualitative one-parameter theorem on $[0, \infty)$, KolmogorovChentsov.exists_modification_holderOnWith_Icc, a different statement that the mission does not duplicate. A proof of this mission's goal would give the classical $d$-parameter criterion on the cube (milestone 6) and its quantitative form together.

Difficulty

The probabilistic steps (2.9)–(2.12) are Markov's inequality and two union bounds. They become concrete once the adjacent pairs are counted: $|\widetilde{\mathcal D}_k|$ is of order $d\,2^{dk}$, and summing over scales needs $\gamma < \beta/\alpha$. Formalizing them requires care with suprema in $[0,\infty]$ and with outer measures of events that are not obviously measurable.

The central difficulty is the deterministic chaining claim and the passage from dyadic points to the whole cube. The paper calls the claim "not difficult to see", but its constant must be uniform over pairs of dyadic points of arbitrarily fine and unequal levels, and the obvious attempt, comparing values along the straight segment between two points, fails because the points of the segment are not dyadic, so the hypothesis says nothing about them. The second difficulty is the modification itself: one field $Y$ must serve every $\gamma < \beta/\alpha$ at once, must agree with $X$ almost surely at every point, and the tail bound for the dyadic supremum must transfer to the Hölder norm over the whole cube, an uncountable supremum whose event is not obviously measurable.

Formalization scope

• Index set: Cube d, the subtype of EuclideanSpace ℝ (Fin d) with coordinates in $[0,1]$, so $|u - v|$ is Euclidean. Because all constants are existential, the statements do not depend on the norm, but Euclidean is the default reading.
• Hypothesis (2.6): Mathlib's IsKolmogorovProcess X P α (d + β) c₀ with c₀ : ℝ≥0, plus 0 < α, 0 < β, 0 < c₀. It reads (2.6) with the lower Lebesgue integral in $[0,\infty]$, so it cannot hold through a junk value of a non-integrable expectation. It also requires each pair $(X_u, X_v)$ to be Borel measurable, which is the measurability included in "random field". The probability space is [IsProbabilityMeasure P].
• Hölder norm: $M_\gamma$ is eHolderNorm γ, valued in $[0,\infty]$. A real supremum, which is 0 on unbounded families and would make (2.8) trivially true, is ruled out. The supremum of (2.12) is likewise an ℝ≥0∞-valued ⨆, and its event is $\{t \le \sup\}$, not the weaker "some term is $\ge t$".
• Uniformity: the constants $c_1$ of (2.8) (a function of $\gamma$), $c_1$ of (2.11), $c_2$ and $c_3$ are quantified before the probability space and the field. A version in which the constant may depend on the field, or one with a different modification for each $\gamma$, is a weaker theorem and is ruled out. The probability space ranges over Type (universe 0).
• Conventions: (2.7) holds for every $\omega$ (the paper states it for the modification itself). Probabilities of events not shown measurable are outer measures. The dyadic level $k$ ranges over $\mathbb N$ including $0$. Adjacent pairs are ordered, which doubles a count that the constants absorb. The milestones add $t > 0$ and $\delta > 0$, which the paper leaves implicit, and carry $\gamma \in (0, \beta/\alpha)$ from (2.10) on. The constants may depend on $d$, which the paper's list "$\alpha, \beta, \gamma, c_0$" leaves implicit.

A complete development needs counting lemmas for the dyadic grid, a chaining lemma on dyadic points, and the extension of a uniformly Hölder function from a dense subset (Mathlib's HolderOnWith and uniform-continuity extension tools apply). The chaining lemma and the quantitative criterion are reusable for any Hölder-regularity argument on cubes. Contributions are welcome for each milestone independently and for an alternative proof of the goal through Mathlib's PairReduction chaining machinery.

Selected references

• J. Miller, S. Sheffield, Liouville quantum gravity and the Brownian map II: geodesics and continuity of the embedding, Ann. Probab., 2021 (accepted manuscript, Apollo repository, University of Cambridge). https://doi.org/10.1214/21-AOP1506
• J. Miller, S. Sheffield, Liouville quantum gravity and the Brownian map I: the QLE(8/3, 0) metric, Invent. Math. 219(1), 75–152, 2020. https://arxiv.org/abs/1507.00719
• I. Karatzas, S. E. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Graduate Texts in Mathematics 113, Springer, 1991. https://doi.org/10.1007/978-1-4612-0949-2
• D. Revuz, M. Yor, Continuous Martingales and Brownian Motion, 3rd ed., Grundlehren der Mathematischen Wissenschaften 293, Springer, 1999. https://doi.org/10.1007/978-3-662-06400-9
• Mathlib, Mathlib/Probability/Process/Kolmogorov.lean (the predicate IsKolmogorovProcess). https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Probability/Process/Kolmogorov.lean

Motivation

The expected error of the randomized SVD with a $k\times(k+p)$ Gaussian test matrix is $\bigl(1+\tfrac{k}{p-1}\bigr)^{1/2}$ times the optimal error (Halko–Martinsson–Tropp 2011, Theorem 10.5). The factor $\tfrac{k}{p-1}$ is $\mathbb E\|G^{\dagger}\|_F^2$ for a $k\times(k+p)$ standard Gaussian matrix $G$: the quality of every Gaussian sketching method is governed by inverse moments of a Gaussian matrix — moments of its pseudoinverse, equivalently of the inverse of the Wishart matrix $GG^{\mathsf T}$. The expected spectral error uses $\mathbb E\|G^{\dagger}\|$ instead (Tropp–Webber 2023, Lemmas B.2–B.3), and deviation bounds use tail estimates for both norms (HMT Proposition 10.4). None of these inverse moments is available in Mathlib. This mission proves them.

Setting

A standard Gaussian matrix $G\in\mathbb R^{r\times k}$ has independent $\mathcal N(0,1)$ entries; its law is $\gamma_{r,k}$. Throughout, $G$ is wide or square, $r\le k$, so that $GG^{\mathsf T}\in\mathbb R^{r\times r}$ is almost surely invertible; $GG^{\mathsf T}$ is a Wishart matrix with $k$ degrees of freedom and $(GG^{\mathsf T})^{-1}$ is inverse-Wishart.

The pseudoinverse of a full-row-rank matrix is $G^{\dagger}=G^{\mathsf T}(GG^{\mathsf T})^{-1}$. Its norms are determined by the inverse Wishart matrix:

$$\|G^{\dagger}\|_F^2=\operatorname{tr}(GG^{\mathsf T})^{-1},\qquad \|G^{\dagger}\|^2=\|(GG^{\mathsf T})^{-1}\|=\sigma_{\min}(G)^{-2},$$

where $\|\cdot\|_F$ is the Frobenius norm, $\|\cdot\|$ the spectral norm (largest singular value) and $\sigma_{\min}(G)$ the smallest of the $r$ singular values of $G$. The letter $e$ denotes Euler's number.

Formalization targets

Goal — Tropp–Webber inverse spectral moment (Lemma B.3)

For integer $1\le p\le18$ and $k\ge r+2p$,

$$\Bigl(\mathbb E\,\bigl\|(GG^{\mathsf T})^{-1}\bigr\|^p\Bigr)^{1/p}\le\frac{e^2(k+r)}{2(k-r)^2}.$$

The case $p=1$ is $\mathbb E\|G^{\dagger}\|^2\le e^2(k+r)/(2(k-r)^2)$, the spectral inverse moment at the heart of expected spectral-norm error bounds. It is the goal because it is the one inverse moment that is not an exact formula: its proof passes through Edelman's bound on the density of $\lambda_{\min}(GG^{\mathsf T})$ and an explicit integration, and it implies the expectation bound of HMT Proposition 10.2 by Jensen's inequality.

Milestones

• Inverse-Wishart mean. $\mathbb E(GG^{\mathsf T})^{-1}=\frac{1}{k-r-1}I_r$ for $r\le k-2$ (Tropp–Webber Lemma B.2).
• Frobenius inverse moment. $\mathbb E\|G^{\dagger}\|_F^2=\frac{r}{k-r-1}$ for $k-r\ge2$ (HMT Proposition 10.2 (10.3) and A.5).
• Second-order inverse-Wishart moments. $\mathbb E\|G^{\dagger}\|_F^4=\frac{r^2(k-r)-2r(r-1)}{(k-r)(k-r-1)(k-r-3)}$ and $\mathbb E\|(GG^{\mathsf T})^{-1}\|_F^2=\frac{r(k-1)}{(k-r)(k-r-1)(k-r-3)}$ for $r\le k-4$ (Tropp–Webber Lemma B.2).
• Chen–Dongarra tail. $\mathbb P\{\|G^{\dagger}\|>t\}\le\frac{1}{\sqrt{2\pi(k-r+1)}}\bigl(\frac{e\sqrt k}{k-r+1}\bigr)^{k-r+1}t^{-(k-r+1)}$ for $k\ge r\ge2$, $t>0$ (HMT Proposition A.3).
• Expected spectral norm of the pseudoinverse. $\mathbb E\|G^{\dagger}\|\le\frac{e\sqrt k}{k-r}$ for $r\ge2$, $k\ge r+1$ (HMT Proposition 10.2 (10.4) and A.4).
• Frobenius tail. $\mathbb P\{\|G^{\dagger}\|_F^2>\frac{12r}{k-r}t\}\le4t^{-(k-r)/2}$ for $k-r\ge4$, $t\ge1$ (HMT Theorem A.6).

Significance

The results. Combined with the second-moment identity and block independence of Mission I, the Frobenius inverse moment gives the expected Frobenius error of the randomized SVD and of generalized Nyström; the spectral inverse moment gives the expected spectral error and the core-noise bounds of truncated sketching methods; the two tail bounds give the large-deviation statements of HMT §10.3. The second-order inverse-Wishart moments quantify the variance of $\|G^{\dagger}\|_F^2$, which Tropp–Webber use for concentration of the randomized SVD error.

Formalizing them. The inverse-Wishart mean and the second-order moments are classical multivariate-statistics formulas (Muirhead; von Rosen) with no Mathlib counterpart. The Chen–Dongarra tail requires the exact distribution of $\sigma_{\min}$, or at least Edelman's density bound; the Frobenius tail is HMT's own argument through the bidiagonal (Householder) model of a Gaussian matrix and chi-square moment estimates. Every statement here is a proved theorem in the literature; none has a machine-checked proof.

Difficulty

There is no Wishart distribution in Mathlib. The direct approach — compute the density of $GG^{\mathsf T}$ and integrate — needs the Wishart density, a change of variables on the cone of positive-definite matrices, and the matrix-variate gamma function. The classical route to the mean avoids this: by rotational invariance $(GG^{\mathsf T})^{-1}$ has the same law as $Q(GG^{\mathsf T})^{-1}Q^{\mathsf T}$ for every orthogonal $Q$, so its mean is a multiple of the identity, and the trace is $\sum_i 1/\chi^2_{k-r+1}$-type quantities whose means are elementary; making "the diagonal entries of $(GG^{\mathsf T})^{-1}$ are reciprocals of $\chi^2_{k-r+1}$ variables" rigorous requires the Gram–Schmidt (QR) decomposition of a Gaussian matrix and the independence of its factors. The spectral inverse moment needs a lower-tail bound for $\lambda_{\min}(GG^{\mathsf T})$ of the exact order $t^{(k-r+1)/2}$; a union bound over rows loses a factor $r$ and does not give the stated constant. The naive attempt to bound $\mathbb E\|G^{\dagger}\|^2$ by $\mathbb E\|G^{\dagger}\|_F^2$ loses a factor $r$ as well.

Formalization scope

$G$ is sampled from the product measure $\gamma_{r,k}$ on arrays; $(\cdot)^{-1}$ is Mathlib's total matrix inverse, equal to $0$ on the null set where $GG^{\mathsf T}$ is singular, and $G^{\dagger}$ is defined as $G^{\mathsf T}(GG^{\mathsf T})^{-1}$ (pinvR). Every inequality is stated together with integrability of its integrand, so the Lean convention that a non-integrable function integrates to $0$ cannot make a bound vacuous; identities with nonzero right-hand sides force integrability on their own but are also stated with it. The inverse-Wishart mean is stated entrywise. Tail bounds are inequalities between a measure in $[0,\infty]$ and $\operatorname{ofReal}$ of the real bound. Real powers with non-integer exponents are Mathlib's rpow; all bases are positive under the hypotheses. The spectral norm is Mathlib's $\ell_2$ operator norm. The sizes follow Tropp–Webber ($G\in\mathbb R^{r\times k}$); HMT's $k\times(k+p)$ and $m\times n$ conventions are translated in each item's source field.

Welcome contributions: a Wishart/inverse-Wishart library (QR decomposition of a Gaussian matrix, Bartlett decomposition, chi-square moments $\mathbb E\,\Xi^{-q}=\Gamma(k/2-q)/(2^q\Gamma(k/2))$), and the distribution of $\sigma_{\min}$ of a Gaussian matrix (Edelman).

Selected references

• N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions, SIAM Review 53(2), 217–288, 2011. https://arxiv.org/abs/0909.4061
• J. A. Tropp, R. J. Webber, Randomized algorithms for low-rank matrix approximation: design, analysis, and applications, 2023. https://arxiv.org/abs/2306.12418
• R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027
• L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12, 134–139, 1918. https://doi.org/10.1093/biomet/12.1-2.134
• S. Dasgupta, A. Gupta, An elementary proof of a theorem of Johnson and Lindenstrauss, Random Structures & Algorithms 22, 60–65, 2003. https://doi.org/10.1002/rsa.10073
• M. Rudelson, R. Vershynin, The Littlewood–Offord problem and invertibility of random matrices, Advances in Mathematics 218, 600–633, 2008. https://arxiv.org/abs/math/0703503
• Y. Chen, J. Dongarra, Condition numbers of Gaussian random matrices, SIAM J. Matrix Anal. Appl. 27(3), 603–620, 2005. https://doi.org/10.1137/040616413
• A. Edelman, Eigenvalues and condition numbers of random matrices, SIAM J. Matrix Anal. Appl. 9(4), 543–560, 1988. https://doi.org/10.1137/0609045
• Y. Gordon, Some inequalities for Gaussian processes and applications, Israel J. Math. 50, 265–289, 1985. https://doi.org/10.1007/BF02759761
• K. R. Davidson, S. J. Szarek, Local operator theory, random matrices and Banach spaces, Handbook of the Geometry of Banach Spaces, Vol. 1, 317–366, 2001. https://doi.org/10.1016/S1874-5849(01)80010-3
• M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89, 2001. https://doi.org/10.1090/surv/089

Shared definitions: the items of this mission import Definitions.Def_GaussianMatrix_basic, a draft of Mission I; submit that proposal first so the import resolves at compile time.

Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.

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

Motivation

A chance-constrained program minimizes a cost $f(x)$ over decisions $x\in\mathbb R^n$ subject to the requirement that a random constraint holds with probability at least $1-\alpha$: $\mathbb P\big(C(x,\xi)\le0\big)\ge1-\alpha$, where $C(x,\xi)=\max_{j=1,\dots,m}c_j(x,\xi)$ collects $m$ constraint functions and $\alpha\in(0,1)$ is a risk level. Such constraints model reliability requirements in power systems, finance and engineering design. They are hard to handle numerically: the probability is rarely available in closed form, its sample estimate is a step function of $x$, and the feasible region is in general nonconvex.

Peña-Ordieres, Luedtke and Wächter (arXiv:1905.07377v2; SIAM J. Optim. 30(3), 2020, DOI 10.1137/19M1261985) replace the probability by a smoothed sample quantile, which turns the chance constraint into a single smooth nonlinear constraint, and solve the resulting problem with a trust-region method built on an $\ell_1$ exact penalty, in the spirit of the S$\ell_1$QP method for regular nonlinear programs (Nocedal and Wright). This mission formalizes the analytic core of that method: the smoothed quantile is well defined and has a bounded, Lipschitz gradient, and the piecewise quadratic model used to compute trust-region steps agrees with the penalty function up to second order.

Setting

Fix $\varepsilon>0$. The smoothed indicator $\Gamma_\varepsilon:\mathbb R\to[0,1]$ equals $1$ on $(-\infty,-\varepsilon]$, $0$ on $[\varepsilon,\infty)$, and a strictly decreasing function $\gamma_\varepsilon$ in between, chosen so that $\Gamma_\varepsilon$ is differentiable (equation (2.2)). The concrete choice is the quartic kernel (2.6),

$$\gamma_\varepsilon(y)=\tfrac{15}{16}\Big(-\tfrac15(y/\varepsilon)^5+\tfrac23(y/\varepsilon)^3-y/\varepsilon+\tfrac8{15}\Big),$$

which makes $\Gamma_\varepsilon$ twice continuously differentiable.

Fix a sample $\xi_1,\dots,\xi_N$ of the random vector. For $z\in\mathbb R^N$, the smoothed $(1-\alpha)$-quantile $Q_\varepsilon(z)$ is the number $q$ solving

$$\sum_{i=1}^N\Gamma_\varepsilon(z_i-q)=(1-\alpha)N. \tag{2.3}$$

It is applied to the vector $C^N(x)$ with entries $[C^N(x)]_i=\max_jc_j(x,\xi_i)$, and the smoothed sample problem requires $Q_\varepsilon(C^N(x))\le0$.

With deterministic constraints $g:\mathbb R^n\to\mathbb R^p$ and a penalty parameter $\pi>0$, the exact penalty function is

$$\varphi_\pi(x)=f(x)+\pi\Big(\|[g(x)]^+\|_1+[Q_\varepsilon(C^N(x))]^+\Big). \tag{5.3}$$

The trust-region step at $x$ minimizes the model

$$m(x,H;d)=f(x)+\nabla f(x)^{\mathsf T}d+\tfrac12d^{\mathsf T}Hd+\pi\Big(\|[g(x)+\nabla g(x)^{\mathsf T}d]^+\|_1+[\widetilde Q_\varepsilon(C^N(x);\widetilde C^N(x;d)-C^N(x))]^+\Big), \tag{5.6}$$

where $H$ is a symmetric matrix, $\widetilde Q_\varepsilon(z;p)=Q_\varepsilon(z)+\nabla Q_\varepsilon(z)^{\mathsf T}p$ and $[\widetilde C^N(x;d)]_i=\max_j\{c_j(x,\xi_i)+\nabla c_j(x,\xi_i)^{\mathsf T}d\}$.

Formalization targets

Goal: Proposition 5.3

If $f$ and $g$ have Lipschitz gradients, each $c_j(\cdot,\xi_i)$ is $L$-Lipschitz with $L'$-Lipschitz gradient, $\gamma_\varepsilon$ is the quartic kernel and $(1-\alpha)N\notin\mathbb Z$, then for fixed $L_H$ there is a constant $K$ with

$$|\varphi_\pi(x+d)-m(x,H;d)|\le K\|d\|^2\qquad\text{for all }x,d\in\mathbb R^n,\ H=H^{\mathsf T},\ \|H\|\le L_H .$$

The constant is not specified, so the goal survives any sharpening of the estimate.

Milestones

1. Lemma 2.1: equation (2.3) has a unique solution when $\gamma_\varepsilon$ is strictly decreasing, $\Gamma_\varepsilon$ is differentiable and $(1-\alpha)N\notin\mathbb Z$.
2. Gradient formula (proof of Proposition 4.1): $[\nabla Q_\varepsilon(z)]_i=\Gamma'_\varepsilon(z_i-Q_\varepsilon(z))/\sum_j\Gamma'_\varepsilon(z_j-Q_\varepsilon(z))$.
3. Gradient bounds: the denominator is at most $-\kappa<0$ uniformly in $z$, and $0\le[\nabla Q_\varepsilon(z)]_i\le1$.
4. Proposition 4.1: $Q_\varepsilon$ has bounded Lipschitz continuous gradients.
5. Linearization bound (5.7)–(5.8): $\|C^N(x+d)-\widetilde C^N(x;d)\|_2\le\sqrt N\,L'\|d\|^2$.
6. Proposition 5.1 (companion): a local minimum $x^*$ of the quantile-constrained problem (5.1) gives the local minimum $(x^*,C^N(x^*))$ of the lifted problem (5.2).

Significance

Proposition 5.3 is the hypothesis under which the trust-region convergence theory of Conn, Gould and Toint (cited as Theorem 5.4, from their Theorem 11.2.5) applies: it guarantees that the method of §5 converges to stationary points of $\varphi_\pi$. Combined with the exact-penalty result of Curtis and Overton (cited as Theorem 5.2), which says that for $\pi$ large enough local minimizers of the smoothed problem are local minimizers of $\varphi_\pi$, this justifies solving the smoothed chance-constrained problem by minimizing $\varphi_\pi$. Proposition 4.1 is independently useful: it says that the smoothed quantile can be handed to any smooth nonlinear solver as a constraint with a bounded, Lipschitz gradient.

The results are proved in the paper. None of them has a machine-checked proof that this mission is aware of. A formalization would also settle two points the printed proofs leave thin: the uniform lower bound on the denominator in Proposition 4.1, which the paper asserts without argument, and the existence part of Lemma 2.1, whose printed proof argues only uniqueness.

Difficulty

The model error splits into three parts. The $f$ and $g$ parts are standard Taylor estimates. The quantile part is the substance. First, $Q_\varepsilon$ is defined only implicitly, so its differentiability needs the implicit function theorem, and its gradient bound needs a lower bound on $\big|\sum_j\Gamma'_\varepsilon(z_j-Q_\varepsilon(z))\big|$ that is uniform over all $z\in\mathbb R^N$, not just pointwise. The pointwise statement is easy: some sample lies strictly inside the smoothing window. The uniform statement needs a quantitative version of that fact, which uses the fractional part of $(1-\alpha)N$. Second, $C^N$ is a maximum of smooth functions and is not differentiable, so the model linearizes each $c_j$ before taking the maximum; one has to show this costs only $O(\|d\|^2)$, uniformly in $x$.

Formalization scope

All objects are defined in one module, SmoothCCP.PenaltyModel.Setting. Decisions and directions live in EuclideanSpace ℝ (Fin n), so gradients and $d^{\mathsf T}Hd$ are inner products. $H$ is a self-adjoint continuous linear operator and $\|H\|$ is its operator norm. Sample values are a fixed list ξs : Fin N → Ξ; this mission involves no probability. $Q_\varepsilon$ is a function on Fin N → ℝ (sup norm), defined as the least root of (2.3) via sInf. Its gradient is the Fréchet derivative. $\Gamma'_\varepsilon$ is deriv of the smoothed indicator, which is differentiable for the quartic kernel, including at $\pm\varepsilon$. The maximum over $j$ uses Finset.sup' and needs $m\ge1$ (the paper's §5 has $m>1$). The Euclidean norm on $\mathbb R^N$ appears explicitly only in milestone 5, where it is written $\sqrt{\sum_i(\cdot)^2}$ to match the printed factor $\sqrt N$.

Standing hypotheses: $\varepsilon>0$, $0<\alpha<1$, $N\ge1$, and $(1-\alpha)N\notin\mathbb Z$. From Proposition 4.1 on, $\gamma_\varepsilon$ is the quartic kernel. Three readings are disclosed in the goal's statement. The Lipschitz hypotheses (5.4)–(5.5) are assumed on all of $\mathbb R^n$ and per component $c_j$, because the conclusion ranges over all $x,d\in\mathbb R^n$. The quartic kernel and $(1-\alpha)N\notin\mathbb Z$ are assumed because the proof uses Proposition 4.1. The $O(\|d\|^2)$ constant is quantified after all data and $L_H$ and before $x$, $d$, $H$.

$Q_\varepsilon$ is the paper's quantile, defined from (2.3), not a function assumed to satisfy it. A statement in which the uniform constant may depend on $x$, $d$ or $H$, or in which (2.3) has no root, would be trivial and is excluded.

A complete development needs the implicit function theorem for $Q_\varepsilon$ (Mathlib's HasStrictFDerivAt.implicitFunction or a one-dimensional argument), first-order Taylor bounds for functions with Lipschitz gradients, and elementary facts about the quartic kernel. The Taylor bounds and the facts about maxima of linearizations are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• A. Peña-Ordieres, J. R. Luedtke, A. Wächter, Solving chance-constrained problems via a smooth sample-based nonlinear approximation, SIAM J. Optim. 30(3), 2020. Preprint arXiv:1905.07377v2. https://arxiv.org/abs/1905.07377v2, https://doi.org/10.1137/19M1261985
• J. Nocedal, S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006 (the S$\ell_1$QP method). https://doi.org/10.1007/978-0-387-40065-5
• F. E. Curtis, M. L. Overton, A sequential quadratic programming algorithm for nonconvex, nonsmooth constrained optimization, SIAM J. Optim. 22(2), 2012, pp. 474–500. https://doi.org/10.1137/090780201
• A. R. Conn, N. I. M. Gould, Ph. L. Toint, Trust-Region Methods, SIAM, 2000. https://doi.org/10.1137/1.9780898719857