Probability

Control Theory Stochastic Systems·Captain: mikedeng1

Linear-Quadratic Optimal Control Problems for Mean-Field Stochastic Differential Equations: Two Riccati Equations Give the Optimal State-Feedback Control and the Value ⟨Π(0)x, x⟩Research Paper

Motivation

Linear-quadratic (LQ) control is the setting in which stochastic optimal control has a closed-form answer: the optimal control is a linear feedback of the state, and the feedback gain comes from a Riccati differential equation. In the mean-field version, the expectation $\mathbb E[X]$ of the state and $\mathbb E[u]$ of the control appear in the dynamics and in the cost. Mean-field SDEs go back to Kac (1956) and McKean (1966) as models of interacting particle systems. A cost containing $\mathbb E[X]$ can penalize the variance $\operatorname{var}(X)=\mathbb E|X|^2-|\mathbb E[X]|^2$ of the state, which is what is wanted when the optimal state should not be too sensitive to the noise (mean–variance portfolio selection is the standard example). With such a cost the problem is no longer a classical LQ problem: the weights on $\mathbb E[X]$ may be negative definite, and the cost is not an expectation of a function of the state path, so the classical Riccati theory does not apply as it stands.

J. Yong (SIAM J. Control Optim. 51(4), 2013, pp. 2809–2838) solved the problem with deterministic coefficients. He derives the optimality system, a linear mean-field forward–backward SDE, and decouples it with two Riccati equations. One governs the deviation $X-\mathbb E[X]$ , the other the mean $\mathbb E[X]$ . The optimal control is then an explicit state feedback.

Timeline:

1956, 1966: Kac and McKean introduce the McKean–Vlasov (mean-field) SDE.
1968–1998: the classical stochastic LQ problem and its Riccati equation (Wonham 1968; Chen, Li and Zhou 1998; Yong–Zhou 1999, the paper's reference [38]).
2009–2011: maximum principles for mean-field SDE control (Buckdahn–Djehiche–Li; Andersson–Djehiche; Meyer-Brandis–Øksendal–Zhou).
2013: Yong, the mean-field LQ problem solved by two Riccati equations (this mission).

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a complete probability space carrying a one-dimensional standard Brownian motion $W$ , and let $\mathbb F$ be the natural filtration of $W$ augmented by the $\mathbb P$ -null sets. Fix a horizon $T>0$ . An admissible control is an $\mathbb F$ -progressively measurable $u:[0,T]\times\Omega\to\mathbb R^m$ with $\mathbb E\int_0^T|u|^2ds<\infty$ ; the set of them is $\mathcal U[0,T]$ . For $x\in\mathbb R^n$ the state solves

dX=\big(AX+\bar A\,\mathbb E[X]+Bu+\bar B\,\mathbb E[u]\big)ds+\big(CX+\bar C\,\mathbb E[X]+Du+\bar D\,\mathbb E[u]\big)dW,\qquad X(0)=x,

with deterministic matrix-valued coefficients. The cost is

J(x;u)=\mathbb E\Big\{\int_0^T\big[\langle QX,X\rangle+\langle\bar Q\,\mathbb E[X],\mathbb E[X]\rangle+\langle Ru,u\rangle+\langle\bar R\,\mathbb E[u],\mathbb E[u]\rangle\big]ds+\langle GX(T),X(T)\rangle+\langle\bar G\,\mathbb E[X(T)],\mathbb E[X(T)]\rangle\Big\}.

Problem (MF-LQ): minimize $J(x;\cdot)$ over $\mathcal U[0,T]$ . The assumptions are:

(H1): the eight coefficients are in $L^\infty(0,T)$ .
(H2): the weights are bounded and symmetric, and for some $\delta>0$ , $Q,\ Q+\bar Q\ge0$ , $R,\ R+\bar R\ge\delta I$ and $G,\ G+\bar G\ge0$ .

The weights $\bar Q,\bar R,\bar G$ themselves need not be semidefinite.

With $\Sigma_0=R+D^TPD$ and $\Sigma_1=R+\bar R+(D+\bar D)^TP(D+\bar D)$ , the two Riccati equations are

\dot P+PA+A^TP+C^TPC+Q-(PB+C^TPD)\Sigma_0^{-1}(B^TP+D^TPC)=0,\qquad P(T)=G,\tag{4.8}

\dot\Pi+\Pi(A+\bar A)+(A+\bar A)^T\Pi+(C+\bar C)^TP(C+\bar C)+Q+\bar Q-\big[\Pi(B+\bar B)+(C+\bar C)^TP(D+\bar D)\big]\Sigma_1^{-1}\big[(B+\bar B)^T\Pi+(D+\bar D)^TP(C+\bar C)\big]=0,\tag{4.9}

with $\Pi(T)=G+\bar G$ . Write $K_0=\Sigma_0^{-1}(B^TP+D^TPC)$ and $K_1=\Sigma_1^{-1}[(B+\bar B)^T\Pi+(D+\bar D)^TP(C+\bar C)]$ .

Formalization targets

Goal: Theorem 4.1 (p. 2827)

Under (H1)–(H2), (4.8) and (4.9) have unique solutions $P$ and $\Pi$ on $[0,T]$ . The closed-loop system obtained by substituting

u^*=-K_0\big(X^*-\mathbb E[X^*]\big)-K_1\,\mathbb E[X^*]

into the state equation has a unique solution $X^*$ . With $Y=P(X^*-\mathbb E[X^*])+\Pi\,\mathbb E[X^*]$ and the explicit $Z$ , the 4-tuple $(X^*,u^*,Y,Z)$ solves the optimality system, and $(X^*,u^*)$ is optimal. Moreover

\inf_{u\in\mathcal U[0,T]}J(x;u)=\langle\Pi(0)x,x\rangle\qquad\forall x\in\mathbb R^n.\tag{4.10}

Milestones

Proposition 2.6: the state equation is well posed in $\widehat{\mathcal X}[0,T]$ .
Proposition 2.8: $J(0;u)\ge\delta\,\mathbb E\int_0^T|u|^2ds$ , and (MF-LQ) has a unique optimal control.
Theorem 3.1: the necessary condition, i.e. the MF-BSDE (3.1) and the stationarity condition (3.2).
Theorem 3.2: the sufficient condition.
Corollary 3.3: unique solvability of the MF-FBSDE (3.3).
§4, p. 2825: (4.8) has a unique solution $P\ge0$ .
§4, p. 2825: the matrix identity $P-P\widetilde D\Sigma_1^{-1}\widetilde D^TP=P^{1/2}(I+P^{1/2}\widetilde D\widetilde R^{-1}\widetilde D^TP^{1/2})^{-1}P^{1/2}\ge0$ .
§4, p. 2826: (4.9) has a unique solution $\Pi\ge0$ .
Proof of Theorem 4.1, p. 2828: the completion-of-squares identity $J(x;u)-\langle\Pi(0)x,x\rangle=\mathbb E\int_0^T(\langle\Sigma_0w_0,w_0\rangle+\langle\Sigma_1w_1,w_1\rangle)ds$ .

The Woodbury identity used on p. 2826 is already proved on the platform (FamousTheorems.woodbury_identity) and is referenced.

Significance

The result. Theorem 4.1 reduces a mean-field stochastic control problem, whose state law enters the dynamics, to two matrix ODEs. The optimal control is computable offline: integrate $P$ and $\Pi$ backward, then feed back the state and its mean. The value $\langle\Pi(0)x,x\rangle$ is explicit, so cost comparisons between the mean-field problem and its classical counterpart become comparisons between Riccati solutions; §5 of the paper does exactly this for variance-penalized costs. When all barred coefficients vanish, $\Pi=P$ and the classical stochastic LQ feedback is recovered.

Formalizing it. The result is proved, not open; this mission formalizes the known proof. No continuous-time stochastic LQ theorem exists on the platform. The mission builds on the published stochastic calculus of Peng1990.SMP.Stochastic (Itô integrals, SDE and BSDE solutions, $L^2_{\mathbb F}$ ) and adds a reusable mean-field LQ setting, matrix Riccati equations in integral form, and a verification theorem. None of the statements has a machine-checked proof yet.

Difficulty

The Riccati equations are nonlinear matrix ODEs with only $L^\infty$ coefficients. Local existence is routine, but global existence on $[0,T]$ needs an a priori bound, which a local fixed-point argument does not give. The bound comes from the control interpretation of the equation, and it requires semidefiniteness of $P$ . The second equation contains $P$ , and its quadratic term is only controlled when $\Sigma_1\ge\delta I$ , which in turn needs $P\ge0$ . Its "state weight" is semidefinite only through the identity of milestone 7, even though $\bar Q$ itself may be negative definite. On the stochastic side, the verification step (milestone 9) and the duality arguments of Theorems 3.1–3.2 apply Itô's product rule to $\langle P(X-\mathbb E X),X-\mathbb E X\rangle$ and to $\langle X,Y\rangle$ for processes driven by the same Brownian motion, with an absolutely continuous (not differentiable) $P$ . Itô's formula is not yet available on the platform: it is the open goal EthierKurtz.ito_formula. Existence in Proposition 2.8 needs a minimizer of a coercive continuous quadratic functional on the Hilbert space $L^2_{\mathbb F}(0,T;\mathbb R^m)$ .

Formalization scope

States are Fin n → ℝ, controls Fin m → ℝ, time is ℝ≥0, and the horizon satisfies $T>0$ . The probability space is complete. $W$ is Peng1990.SMP.IsStdBrownian with one coordinate, and $\mathbb F$ is ReflectedBSDE.Existence.augmentedFiltration. $\mathbb E[X(s)]$ is the Bochner integral of the solution itself. Every mean-field term is a closure over the process being solved for, never a free deterministic input. Solutions of the forward and backward equations are the published SolvesSDE/SolvesBSDE notions: progressive, square-integrable, with the integral identity at each $t\in[0,T]$ almost surely. Controls and $Z$ -components are identified up to $ds\otimes d\mathbb P$ -null sets.

Other conventions:

$L^\infty$ coefficients are measurable functions with an entrywise bound on $[0,T]$ .
(H2) is transcribed literally, with nothing assumed on $\bar Q,\bar R,\bar G$ alone.
Riccati equations are stated in integral form $P(t)=G+\int_t^TF(s,P(s))ds$ with an integrable right-hand side, since solutions are only absolutely continuous.
The class of (4.8) is the regular class $\Sigma_0\ge\varepsilon I$ , so that Matrix.inv is a true inverse. For (4.9), $\Sigma_1\ge\delta I$ follows from (H2) once $P\ge0$ .
The value (4.10) is stated as a lower bound for every admissible control together with equality at $u^*$ , not as an infimum of a set of reals.
The page's "positive definite" for $P$ and $\Pi$ is false in general ( $G=Q=0$ gives $P\equiv0$ ); the milestones assert positive semidefiniteness.

A formalization in which the mean $\mathbb E[X]$ is an independent input, or in which a Riccati "solution" may use the junk value $0$ of a singular inverse, would trivialize the problem. Both are ruled out by the definitions above. A sorry-free sanity file shows that (H1)–(H2) hold for data with $\bar Q=-\tfrac12I$ negative definite, and that the Riccati class is non-empty.

Contributions are welcome on all of the following:

the Itô product rule for the published Itô processes;
the existence of continuous versions;
Gronwall-type uniqueness for linear mean-field SDEs and BSDEs;
Carathéodory theory for matrix Riccati equations with measurable coefficients;
the PSD matrix identity, which uses only Mathlib linear algebra.

Selected references

J. Yong, Linear-quadratic optimal control problems for mean-field stochastic differential equations, SIAM J. Control Optim. 51(4) (2013) 2809–2838. https://doi.org/10.1137/120892477
J. Yong and X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3
S. Chen, X. Li and X. Y. Zhou, Stochastic linear quadratic regulators with indefinite control weight costs, SIAM J. Control Optim. 36(5) (1998) 1685–1702. https://doi.org/10.1137/S0363012996310478
R. Buckdahn, B. Djehiche and J. Li, A general stochastic maximum principle for SDEs of mean-field type, Appl. Math. Optim. 64 (2011) 197–216. https://doi.org/10.1007/s00245-011-9136-y
H. P. McKean, A class of Markov processes associated with nonlinear parabolic equations, Proc. Natl. Acad. Sci. USA 56 (1966) 1907–1911. https://doi.org/10.1073/pnas.56.6.1907

15 thms2 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Algorithms for #BIS-Hard Problems on Expander Graphs 4: On Almost Every Δ-Regular Bipartite Graph with Δ ≥ Cq² log² q, Proper q-Colorings Reduce to Kotecký–Preiss Polymer ModelsResearch Paper

Motivation

Counting the proper $q$ -colorings of a graph, and sampling one uniformly at random, are basic problems of approximate counting with a long history in statistical physics, where proper colorings are the zero-temperature antiferromagnetic Potts model. On bipartite graphs these problems are tied to #BIS, the problem of approximately counting independent sets in a bipartite graph, whose complexity is unresolved. Galanis, Štefankovič, Vigoda and Yang showed that approximately counting proper $q$ -colorings is #BIS-hard on bipartite graphs of maximum degree $\Delta$ whenever $q \le \Delta/(2\log\Delta)$ (SIAM J. Comput. 45(6), 2016). A positive result in that regime therefore has to use structure beyond bipartiteness and bounded degree.

Jenssen, Keevash and Perkins (SIAM J. Comput. 49(4) 2020) use expansion. Their Theorem 5 says that for $\Delta \ge Cq^2\log^2 q$ there is an FPTAS and a polynomial-time sampler for proper $q$ -colorings on almost every $\Delta$ -regular bipartite graph. This answered Conjecture 1 of the authors' SODA 2019 extended abstract. Liao, Lin, Lu and Mao (APPROX/RANDOM 2019) independently proved a similar result under a slightly stronger condition on $\Delta$ . The organizing idea, that most colorings of a strongly expanding bipartite graph follow one of a few patterns, comes from the work of Peled and Spinka on rigidity of colorings of $\mathbb Z^d$ (arXiv:1808.03597).

This mission is the fourth of a series formalizing the four main results of that paper; it covers Theorem 5.

Setting

Fix integers $q \ge 3$ , $\Delta \ge 3$ and $m \ge 1$ . The vertex set is $V = \mathcal O \sqcup \mathcal E$ , two sides of $m$ vertices each (so $n = 2m$ ). $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ is the finite set of labelled simple graphs on $V$ whose edges all join $\mathcal O$ to $\mathcal E$ and in which every vertex has degree $\Delta$ . A property holds for almost every $\Delta$ -regular bipartite graph if the fraction of graphs in $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ having it tends to $1$ as $m \to \infty$ .

A proper $q$ -coloring is a map $f : V \to [q]$ with $f(u) \ne f(v)$ on every edge; $\mathcal X_q(G)$ is their set and $Z_G(q) = |\mathcal X_q(G)|$ . A pattern is a pair $(A,B)$ of disjoint sets with $A \cup B = [q]$ ; there are $2^q$ of them. A coloring agrees with $(A,B)$ at $v$ if $v \in \mathcal O$ and $f(v) \in A$ , or $v \in \mathcal E$ and $f(v) \in B$ . For $S \subseteq V$ , $\chi_{A,B}(S)$ is the set of proper colorings that disagree with $(A,B)$ at every vertex of $S$ and agree everywhere else.

$G^3$ joins two vertices at $G$ -distance at most $3$ . A set is little if $|S| \le 4q\frac{\log\Delta}{\Delta}m$ . A polymer is a little set that is connected in $G^3$ ; $\mathcal C(G)$ is the set of polymers, and two polymers are compatible if their $G$ -distance exceeds $3$ . For a pattern $(A,B)$ , the weight and the polymer partition function are

w_{A,B}(\gamma) = \frac{|\chi_{A,B}(\gamma)|}{|A|^m|B|^m}, \qquad \Xi_{A,B}(G) = \sum_{\Gamma} \prod_{\gamma\in\Gamma} w_{A,B}(\gamma),

the sum over all families $\Gamma \subseteq \mathcal C(G)$ of pairwise compatible polymers, the empty family included. Finally $\hat Z$ is an $\varepsilon$ -relative approximation to $Z$ if $e^{-\varepsilon}\hat Z \le Z \le e^{\varepsilon}\hat Z$ .

Formalization targets

Goal: the deterministic core of Theorem 5

There is an absolute constant $C > 0$ such that for all $q \ge 3$ and $\Delta \ge Cq^2\log^2 q$ , almost every $\Delta$ -regular bipartite graph $G$ satisfies

e^{-\varepsilon}\tilde Z_G(q) \le Z_G(q) \le e^{\varepsilon}\tilde Z_G(q), \qquad \tilde Z_G(q) = \sum_{(A,B)} |A|^m|B|^m\,\Xi_{A,B}(G), \quad \varepsilon = e^{-m/(4q)},

and, for every pattern $(A,B)$ and every polymer $\gamma \in \mathcal C(G)$ , the Kotecký–Preiss condition

\sum_{\gamma' \in \mathcal C(G):\ d(\gamma',\gamma)\le 3} w_{A,B}(\gamma')\,e^{|\gamma'| + g(\gamma')} \le |\gamma|, \qquad g(\gamma) = \frac{\Delta}{10q^2\log\Delta}|\gamma|.

The constant $C$ is left existential, as in the paper.

Milestones

In the order of the proof:

Lemma 23, the expansion of almost every regular bipartite graph;
Lemma 27, the bound on $|\chi_{A,B}(S)|$ ;
Lemma 28, the covering of $\mathcal X_q(G)$ by $\chi_{A,B}(S)$ with $S$ little;
the product formula after (13);
Claim 30, the size bound for sparse sets;
the binomial estimate, an existing platform theorem;
Lemma 29, the reduction;
the weight bound of §5.1;
the per-vertex estimate (15).

Significance

The goal is the whole mathematical content of Theorem 5. The paper's algorithm (its Theorem 8, adapted from Helmuth, Perkins and Regts, Algorithmic Pirogov–Sinai theory) takes exactly these two facts as input. Given the Kotecký–Preiss condition, the cluster expansion of each $\log\Xi_{A,B}(G)$ converges and truncating it gives the estimator; the reduction transfers the estimate to $Z_G(q)$ . With the goal proved, the remaining distance to the FPTAS is algorithmic bookkeeping, not combinatorics.

The result has been proved since 2019 and is not formalized anywhere. A formal proof would add a machine-checked polymer-model reduction for a spin system with exponentially many ground states, a reusable model of uniformly random regular bipartite graphs, and a checked instance of the "expansion implies few ground states" argument used throughout this literature.

Difficulty

The obvious first idea is a one-ground-state expansion, as for the hard-core model, where configurations are close to "all even" or "all odd". For colorings there are $2^q$ patterns. A coloring can lie close to several of them, so the reduction must show that the sets $\chi_{A,B}(S)$ with $S$ little overlap only negligibly. That needs an inclusion–exclusion step whose error is exponentially small in $m/q$ . A second difficulty is the size of polymers: little sets are $q$ times larger than the sets of the hard-core analysis. Claim 30 is what keeps the union of compatible polymers from becoming a large set that the expansion no longer controls. Finally, the constants must be uniform in $q$ . The single condition $\Delta \ge Cq^2\log^2 q$ has to cover the expansion lemma, the reduction and the Kotecký–Preiss estimate at once.

Formalization scope

The FPTAS and the sampling algorithm are not formalized. Mathlib has no machine model in which "polynomial time" could be stated, and the running times carry unquantified constants. The goal is the mathematics the algorithm rests on: the reduction and the Kotecký–Preiss condition, with the paper's constants $e^{-m/(4q)}$ , $4q\log\Delta/\Delta$ and $\Delta/(10q^2\log\Delta)$ . Neither half may be dropped. Replacing $e^{-m/(4q)}$ by an existential error, or summing the Kotecký–Preiss condition over compatible rather than incompatible polymers, would make the goal trivial or wrong.

Conventions committed to in Lean:

Vertices are Fin m ⊕ Fin m, and $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ is the set of labelled $\Delta$ -regular graphs with edges only between the two fixed sides. The paper does not fix a bipartition; this fixed-sides model is a disclosed choice, matching §5's $|\mathcal O| = |\mathcal E| = m$ .
Distances are Mathlib's extended distance edist, so vertices in different components are at distance $\infty$ and never incompatible.
A pattern is encoded by $A \subseteq [q]$ with $B = [q]\setminus A$ . Patterns with an empty side are kept: their weights are $0$ under Lean's $x/0 = 0$ , so they contribute $0$ to $\tilde Z_G(q)$ , as on the page for large $m$ .
log is the natural logarithm; the binomial estimate is used in nats.

Added hypotheses:

$A, B \ne \emptyset$ in Lemma 27 and in the product formula, which divide by $|A|$ and $|B|$ ;
$\Delta \ge 3$ in Lemma 28 and Claim 30, the paper's standing convention (§1.3);
$m \ge 1$ in Lemma 29, which fails on the empty vertex set.

The goal needs none of these, since its limit is in $m$ and its constant absorbs $\Delta$ .

A complete development needs a counting theory of random regular bipartite graphs (for Lemma 23, through Bassalygo's expansion theorem), counts of connected sets in bounded-degree graphs, and inclusion–exclusion over patterns. The random-graph model and the polymer-model definitions are reusable across this series and beyond. Proofs of any milestone, and alternative routes to Lemma 23, are welcome.

Selected references

M. Jenssen, P. Keevash and W. Perkins, Algorithms for #BIS-hard problems on expander graphs, SIAM J. Comput. 49(4) (2020) 681–710. https://doi.org/10.1137/19M1286669
A. Galanis, D. Štefankovič, E. Vigoda and L. Yang, Ferromagnetic Potts model: refined #BIS-hardness and related results, SIAM J. Comput. 45(6) (2016) 2004–2065.
R. Peled and Y. Spinka, Rigidity of proper colorings of $\mathbb Z^d$ , arXiv:1808.03597 (2018). https://arxiv.org/abs/1808.03597
C. Liao, J. Lin, P. Lu and Z. Mao, Counting independent sets and colorings on random regular bipartite graphs, APPROX/RANDOM 2019, Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2019).
T. Helmuth, W. Perkins and G. Regts, Algorithmic Pirogov–Sinai theory, Probab. Theory Related Fields (2020); extended abstract at STOC 2019.
R. Kotecký and D. Preiss, Cluster expansion for abstract polymer models, Comm. Math. Phys. 103(3) (1986) 491–498.
L. A. Bassalygo, Asymptotically optimal switching circuits, Problems Inform. Transmission 17(3) (1981) 206–211.

13 thms2 active usersReviewed

Completed

Functional Analysis Statistics·Captain: mikedeng1

Distance Covariance in Metric Spaces 1: On Spaces of Strong Negative Type, Zero Distance Covariance Forces a Product MeasureResearch Paper

Motivation

Testing whether two random quantities are independent is one of the basic tasks of statistics. Classical correlation only detects linear dependence. Distance covariance, introduced by Székely, Rizzo and Bakirov (Ann. Statist. 2007) for random vectors in Euclidean spaces, is a dependence measure that vanishes exactly under independence. It only needs the distances between sample points, and its empirical version is a simple V-statistic. These properties made it a standard tool for nonparametric independence testing.

Lyons (Ann. Probab. 41 (2013), arXiv:1106.5758) asked in which metric spaces this characterization of independence survives. The answer is the class of metric spaces of strong negative type, which includes all separable Hilbert spaces. On such spaces, distance covariance gives a test of independence that is consistent against every alternative. This mission formalizes that result, Theorem 3.11 of the paper, together with the chain of results its proof rests on.

Timeline. Schoenberg (1937, 1938) characterized metric spaces of negative type by isometric embeddings of $(\mathcal X,d^{1/2})$ into Hilbert space. Székely, Rizzo and Bakirov (2007) defined distance covariance on $\mathbb R^p\times\mathbb R^q$ and proved that it vanishes only under independence. Lyons (2013) extended the theory to general metric spaces and identified strong negative type as the exact condition. The Errata (Ann. Probab. 46 (2018), 2400–2405; included in arXiv:1106.5758, pp. 24–29) added a standing separability assumption and repaired a gap in Lemma 3.8. The Second Errata appeared in Ann. Probab. 49 (2021).

Setting

Let $(\mathcal X,d)$ and $(\mathcal Y,d)$ be separable metric spaces with their Borel $\sigma$ -fields. A finite measure $\mu$ on $\mathcal X$ has a finite first moment if $\int d(o,x)\,d\mu(x)<\infty$ for some (equivalently every) $o\in\mathcal X$ . For such $\mu$ define

a_\mu(x)=\int d(x,x')\,d\mu(x'),\qquad D(\mu)=\int d(x,x')\,d\mu^2(x,x'),

d_\mu(x,x')=d(x,x')-a_\mu(x)-a_\mu(x')+D(\mu).

For a probability measure $\theta$ on $\mathcal X\times\mathcal Y$ whose marginals $\mu$ and $\nu$ have finite first moments, the distance covariance is

\operatorname{dcov}(\theta)=\int d_\mu(x,x')\,d_\nu(y,y')\,d\theta^2\big((x,y),(x',y')\big).

$\theta$ is a product measure if $\theta=\mu\times\nu$ .

$(\mathcal X,d)$ has negative type if $\sum_{i,j\le n}\alpha_i\alpha_j d(x_i,x_j)\le0$ for all $n$ , all points $x_1,\dots,x_n$ and all real weights with $\sum_i\alpha_i=0$ . For finite measures $\mu_1,\mu_2$ with finite first moments, $D(\mu_1-\mu_2)$ is the integral of $d$ against $(\mu_1-\mu_2)^2$ . On spaces of negative type $D(\mu_1-\mu_2)\le0$ for probability measures $\mu_1,\mu_2$ . The space has strong negative type if, in addition, $D(\mu_1-\mu_2)=0$ only when $\mu_1=\mu_2$ .

An embedding is a map $\phi:\mathcal X\to H$ into a real Hilbert space with $d(x,x')=\|\phi(x)-\phi(x')\|^2$ . Its barycenter map is $\beta_\phi(\mu)=\int\phi\,d\mu$ . The tensor embedding $(x,y)\mapsto\phi(x)\otimes\psi(y)$ takes values in the Hilbert tensor product $H\otimes K$ . $M^1(\mathcal X)$ denotes the finite signed measures whose variation has finite first moment. $M^{1,1}(\mathcal X\times\mathcal Y)$ denotes those on the product whose variation has marginals of finite first moment.

Formalization targets

Goal: Theorem 3.11

If $\mathcal X$ and $\mathcal Y$ have strong negative type and the marginals $\mu,\nu$ of the probability measure $\theta$ have finite first moments, then

\operatorname{dcov}(\theta)=0\ \Longrightarrow\ \theta=\mu\times\nu .

Milestones

Lemma 2.1: $d_\mu\in L^2(\mu\times\mu)$ . The integrability of $d_\mu(x,x')d_\nu(y,y')$ against $\theta^2$ (p. 4) follows, so $\operatorname{dcov}(\theta)$ is a genuine integral.
Schoenberg's theorem (p. 9): a separable space has negative type if and only if it has an embedding into $\ell^2(\mathbb N)$ .
Identity (3.4): $D(\mu)=-2\|\beta_\phi(\mu)\|^2$ when $\mu(\mathcal X)=0$ . Proposition 3.1: strong negative type holds iff $\beta_\phi$ is injective on probability measures with finite first moment.
Proposition 3.5: $d_\mu(x,x')=-2\langle\phi(x)-\beta_\phi(\mu),\phi(x')-\beta_\phi(\mu)\rangle$ , together with $a_\mu(x)=\|\phi(x)-\beta_\phi(\mu)\|^2+D(\mu)/2$ and $D(\mu)=2\operatorname{Var}(\phi(X))$ .
Proposition 3.7: $\operatorname{dcov}(\theta)=4\|\beta_{\phi\otimes\psi}(\theta-\mu\times\nu)\|^2$ .
Lemma 3.9 (injectivity of $\beta_\phi$ on $M^1(\mathcal X)$ ) and Lemma 3.8 in its errata form (injectivity of $\beta_{\phi\otimes\psi}$ on $M^{1,1}(\mathcal X\times\mathcal Y)$ ).

The converse, that a product measure has $\operatorname{dcov}(\theta)=0$ (p. 5), is included as a companion statement.

Significance

The result. Theorem 3.11 makes the empirical distance covariance a consistent test of independence against all alternatives on any pair of separable metric spaces of strong negative type. Examples are separable Hilbert spaces and their subsets, and every space of negative type after replacing $d$ by $d^r$ , $0<r<1$ . Its companion, Proposition 3.15 (a separate mission of this series), shows that strong negative type is exactly the right hypothesis. Proposition 3.7 also identifies distance covariance with Brownian covariance and with the original Euclidean definition, through specific choices of embedding.

Formalizing it. The result is proved, with the gap in Lemma 3.8 closed by the Errata (2018). No part of it has a machine-checked proof that we know of. A formalization needs barycenters of Hilbert-space-valued maps against measures, the Hilbert tensor product of two real Hilbert spaces, and Schoenberg's embedding theorem. None of these is in Mathlib in this form, and all are reusable well beyond distance covariance.

Difficulty

The obvious route reads $\operatorname{dcov}(\theta)=0$ as "the barycenters of $\theta$ and of $\mu\times\nu$ coincide in $H\otimes K$ " and concludes by injectivity. Strong negative type only gives injectivity of $\beta_\phi$ on probability measures, while $\theta-\mu\times\nu$ is a signed measure on a product space. Getting from injectivity on single factors to injectivity on $M^{1,1}$ of the product is where the original proof had a gap: an auxiliary signed measure built from $\theta$ was not shown to have a finite first moment. The errata version changes the embeddings so that this can be done. Two smaller obstacles are integrability (the definition of $\operatorname{dcov}$ is meaningful only by Lemma 2.1) and the construction of the Hilbert space in Schoenberg's theorem.

Formalization scope

All spaces are Lean metric spaces with their Borel $\sigma$ -fields and SecondCountableTopology. This is the separability the author adds in Errata (i), which makes $d$ measurable on the product. Measures are Mathlib Measures. A probability $\theta$ on $\mathcal X\times\mathcal Y$ has marginals θ.map Prod.fst and θ.map Prod.snd. "Product measure" means $\theta$ equals the product of these marginals. Hilbert spaces are real (Errata (viii)). Existential embeddings land in $\ell^2(\mathbb N)$ , which suffices for separable spaces. The Hilbert tensor product is the completion of the algebraic tensor product with its inner product. $D(\mu_1-\mu_2)$ is defined by its bilinear expansion. Injectivity on $M^1$ and $M^{1,1}$ is stated for pairs of finite measures, which is equivalent to injectivity on signed measures via the Jordan decomposition.

Every integral here is a Bochner integral, which is $0$ for a non-integrable integrand. Each statement therefore carries the finite-first-moment hypotheses of the paper, and integrability itself is a milestone. Negative type and strong negative type are defined by (3.1) and by the condition on $D(\mu_1-\mu_2)$ , not through an embedding or a barycenter map, so Schoenberg's theorem and Proposition 3.1 are not definitional. A statement with a "product measure" whose factors are free, or with dcov defined without the moment hypotheses, would be a different and trivializable theorem.

Welcome contributions: barycenter calculus for Hilbert-valued integrals, tensor-product integrals, Schoenberg's theorem, and proofs of any milestone.

Selected references

R. Lyons, Distance covariance in metric spaces, Ann. Probab. 41 (2013), 3284–3305. https://doi.org/10.1214/12-AOP803 ; author's version with both errata: https://arxiv.org/abs/1106.5758
R. Lyons, Errata to "Distance covariance in metric spaces", Ann. Probab. 46 (2018), 2400–2405; reproduced in https://arxiv.org/abs/1106.5758 (version of 19 Dec. 2020), pp. 24–29
G. J. Székely, M. L. Rizzo, N. K. Bakirov, Measuring and testing dependence by correlation of distances, Ann. Statist. 35 (2007), 2769–2794. https://doi.org/10.1214/009053607000000505
I. J. Schoenberg, Metric spaces and positive definite functions, Trans. Amer. Math. Soc. 44 (1938), 522–536. https://doi.org/10.1090/S0002-9947-1938-1501980-0

11 thms2 active usersReviewed

Completed

Statistics·Captain: mikedeng1

Dynamic Assortment Personalization in High Dimensions 2: The Empirical Type Frequencies Satisfy ‖μ̂ − μ⋆‖_q ≤ min{8√((τ+m)/N), m^{1/q}√((τ+log 2m)/(2N))} with Probability at Least 1 − e^{−τ}Research Paper

Motivation

A retailer that personalizes the set of products it shows to each customer needs to know who its customers are. In the low-rank multinomial-logit model of Kallus and Udell, Dynamic Assortment Personalization in High Dimensions (arXiv:1610.05604), every arriving customer belongs to one of $m$ customer types, and the type of each arrival is drawn independently from an unknown type distribution $\mu^\star$ . Planning a non-personalized assortment, or weighting the per-type preference estimates, requires an estimate of $\mu^\star$ from the observed types. When $m$ is large (types may be fine-grained customer profiles), the question is how many observations are needed before that estimate is reliable, and in which norm.

Theorem 4 of the paper answers this for the simplest estimator, the empirical frequencies, with an explicit, non-asymptotic bound in every $\ell_q$ norm, $1\le q\le\infty$ . The bound has two regimes: one that is good when the sample size $N$ is only slightly larger than $m$ , and one that is good when $N$ is large compared with $m^{2/q}$ .

Setting

Customer types are labelled $1,\dots,m$ . The type distribution is a vector $\mu^\star$ in the probability simplex

\Delta^m=\Big\{\mu\in\mathbb R^m:\ \mu_i\ge0,\ \sum_{i=1}^m\mu_i=1\Big\}.

The observation model (Sec. 3.2, p. 13) consists of $N$ records $(i_t,j_t,S_t)$ , $t=1,\dots,N$ : the type $i_t$ of the $t$ -th customer, the item $j_t$ the customer chose, and the assortment $S_t$ offered. The types $i_1,\dots,i_N$ are independent and identically distributed with $\mathbb P(i_t=i)=\mu^\star_i$ . The items and assortments play no role for the type distribution.

The empirical type frequencies (Sec. 3.2.1, p. 14) are

\hat\mu_i=\frac1N\sum_{t=1}^N\mathbb I[i_t=i],\qquad i=1,\dots,m.

For $v\in\mathbb R^m$ and $q\in[1,\infty]$ the $\ell_q$ norm is $\|v\|_q=(\sum_i|v_i|^q)^{1/q}$ , and $\|v\|_\infty=\max_i|v_i|$ ; the convention $m^{1/q}=1$ at $q=\infty$ is used throughout.

The proof works with the empirical Rademacher complexity of the sample: with $I_t=e_{i_t}$ the indicator vector of the $t$ -th type,

\widehat{\mathfrak R}_N=\frac1{2^N}\sum_{\epsilon\in\{-1,+1\}^N}\ \sup_{\|v\|_\infty\le1}\ \frac1N\sum_{t=1}^N\epsilon_t\,v^TI_t .

Formalization targets

Goal: Theorem 4 (p. 18)

For every $\tau\ge0$ and $q\in[1,\infty]$ , with probability at least $1-e^{-\tau}$ ,

\|\hat\mu-\mu^\star\|_q\ \le\ \min\left\{8\sqrt{\frac{\tau+m}{N}},\ \frac{m^{1/q}}{\sqrt2}\sqrt{\frac{\tau+\log(2m)}{N}}\right\}.

The goal keeps the paper's constants and its single statement over all $q\in[1,\infty]$ , including $q=\infty$ .

Milestones (proof of Theorem 4, p. 44)

The coordinatewise tail bound, for $\eta\ge0$ :

\mathbb P(\|\hat\mu-\mu^\star\|_q>\eta)\le\sum_{i=1}^m\mathbb P\big(|\hat\mu_i-\mu^\star_i|>\eta/m^{1/q}\big)\le2m\exp(-2N\eta^2/m^{2/q}).

The deterministic complexity bound, for every sample:

\widehat{\mathfrak R}_N=\frac1N\sum_{i=1}^m\frac1{2^N}\sum_{\epsilon}\Big|\sum_{t=1}^N\mathbb I[i_t=i]\epsilon_t\Big|\le\frac1{\sqrt N}\sum_{i=1}^m\sqrt{\hat\mu_i}\le\sqrt{\frac mN}.

The $\ell_1$ tail bound, for $\eta\ge0$ :

\mathbb P(\|\mu^\star-\hat\mu\|_1>\eta)\le e^{\,m-N\eta^2/64}.

Significance

The first term of the minimum shows that $\hat\mu$ is consistent in every $\ell_q$ norm as soon as $N$ grows faster than $m$ , and gives $\sqrt{m/N}$ -consistency in $\ell_1$ , i.e. in total variation. A coordinatewise argument alone cannot give this: for $q=1$ it yields a bound that does not vanish unless $N$ grows faster than $m^2$ . The second term is the sharper one in the regime $N\gg m^{2/q}$ , for instance in $\ell_\infty$ , where it gives the familiar $\sqrt{\log(m)/N}$ rate. In the paper the estimate of $\mu^\star$ enters non-personalized assortment planning, where the expected revenue of an assortment is averaged over types.

On the formalization side, the result is proved in the paper; nothing about it is open. As far as a search of the Prove2Me catalog shows, no machine-checked version of this statement, or of an $\ell_q$ concentration bound for empirical frequencies with these constants, exists. A complete development would also supply, in finite and elementary form, a coordinatewise Hoeffding bound for binomial proportions and an $\ell_1$ deviation bound for categorical samples, both reusable well beyond this mission.

Difficulty

The second term is a union bound and a binomial tail bound. The first term is where the work is. The obvious route, bounding each coordinate separately and summing, costs a factor $m$ in the $\ell_1$ norm and gives a useless rate when $N$ is comparable to $m$ . The proof instead treats $\|\hat\mu-\mu^\star\|_1$ as the supremum of an empirical process over the $\ell_\infty$ unit ball, controls its mean through the Rademacher complexity (where the absolute value of a sum of $N\hat\mu_i$ random signs must be bounded by $\sqrt{N\hat\mu_i}$ ), and then needs concentration of the supremum around its mean with constants good enough to produce the stated $8$ and $1/64$ . The paper's p. 44 citation of a symmetrization result states it with the empirical rather than the expected complexity, so that step has to be redone with care rather than transcribed.

Formalization scope

Source. The arXiv preprint arXiv:1610.05604. The PDF has no arXiv stamp, version or date and is pinned by its sha256 2b0104810fa9d656f2b79f8a44f791b2a3da388f3f6707564f4619da2050216a. Its printed page numbers equal the PDF page numbers.
Types and samples. Types are Fin m and draws Fin N, both 0-based. A sample is a map x : Fin N → Fin m.
Probability. The i.i.d. law is explicit: the probability of an event is the finite sum, over the samples in the event, of $\prod_t\mu^\star_{x_t}$ . No measure theory is used. Restricting the observations $(i_t,j_t,S_t)$ to the types is exact, because the types are i.i.d. $\mu^\star$ regardless of the items and assortments.
Standing assumptions. $\mu^\star\in\Delta^m$ (Mathlib's stdSimplex), which forces $m\ge1$ , and $N\ge1$ , added because $\hat\mu$ is undefined for an empty sample. The milestones' tail bounds assume $\eta\ge0$ , which the paper leaves implicit. For $\eta<0$ the events are certain and the printed bounds can be smaller than $1$ .
Norms and exponents. $\|\cdot\|_q$ is Mathlib's PiLp norm on $\mathbb R^m$ for $q\in[1,\infty]$ , with $q$ an extended nonnegative real; $m^{1/q}$ and $m^{2/q}$ use an exponent defined as $0$ at $q=\infty$ and $1/q$ otherwise. $\log$ is the natural logarithm.
The Rademacher complexity is defined by the paper's supremum over the $\ell_\infty$ unit ball, a nonempty index set on which the objective is bounded, so the supremum is genuine.
Corrected misprint. On p. 44 the Hoeffding display prints $2m\exp(-2n\eta^2/m^{2/q})$ with $n$ , the number of items. The formal statement uses the sample size $N$ , which is what the argument produces and what Theorem 4 needs. In the complexity chain, the binomial coefficient printed as $\binom{m}{\lceil N\hat\mu_i/2\rceil}$ should be $\binom{N\hat\mu_i}{\lceil N\hat\mu_i/2\rceil}$ ; that line is not part of the formal statement.
Not a trivialization. The probability is taken under the i.i.d. product law of $\mu^\star$ , not for a fixed sample and not under the uniform law on samples. The events use the paper's strict and non-strict inequalities as printed.
Welcome contributions. An elementary Hoeffding bound for the binomial proportion; a bounded-differences (McDiarmid) inequality for functions of finitely many independent finite-valued draws; a symmetrization inequality relating $\mathbb E\|\hat\mu-\mu^\star\|_1$ to the Rademacher complexity; and alternative proofs of the $\ell_1$ term.

Selected references

N. Kallus, M. Udell, Dynamic Assortment Personalization in High Dimensions, arXiv preprint, 2016; Operations Research 68(4), 2020. https://arxiv.org/abs/1610.05604
P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3, 463–482, 2002 (the paper cites it as 2003). https://www.jmlr.org/papers/v3/bartlett02a.html
W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301), 13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830
C. McDiarmid, On the Method of Bounded Differences, Surveys in Combinatorics, London Mathematical Society Lecture Note Series 141, 148–188, 1989. https://doi.org/10.1017/CBO9781107359949.008

6 thms2 active usersReviewed

Graph Theory Mathematical Physics·Captain: mikedeng1

Algorithms for #BIS-Hard Problems on Expander Graphs 3: On Almost Every Δ-Regular Bipartite Graph, the Hard-Core Model at λ > 50 log²Δ/Δ Reduces to Two Kotecký–Preiss Polymer ModelsResearch Paper

Motivation

The hard-core model assigns weight to independent vertex sets of a graph. Its partition function counts those sets when the activity is one and weights larger sets more heavily when the activity increases. Counting independent sets on bipartite graphs is a standard benchmark for approximate counting: the general problem is difficult, while random regular graphs have additional expansion that can make approximation possible. Jenssen, Keevash and Perkins prove an approximation and sampling theorem for almost every sufficiently high degree regular bipartite graph when the activity is above an explicit threshold Jenssen–Keevash–Perkins, Theorem 2.

The question is specific to a random graph model. It does not assert the same conclusion for every regular bipartite graph. The authors use a criterion attributed to Bassalygo to show that almost every graph in the model has the expansion needed by their argument Jenssen–Keevash–Perkins, Theorem 22 and Lemma 23. Liao, Lin, Lu and Mao independently obtained related counting results under somewhat stronger parameter conditions Liao–Lin–Lu–Mao, 2019.

Setting

Let $G$ be a simple graph with two labelled sides $\mathcal O$ and $\mathcal E$ , each containing $m$ vertices, and let every vertex have degree $\Delta$ . An independent set $I$ contains no adjacent pair. For activity $\lambda>0$ , the hard-core partition function is

Z_G(\lambda)=\sum_{I\text{ independent}}\lambda^{|I|}.

For a vertex set $S$ , its vertex boundary $\partial S$ consists of vertices outside $S$ with a neighbor in $S$ . The graph is a bipartite $(\sigma,\rho)$ -expander when every subset of either side with size at most $\sigma m$ has boundary of size at least $\rho$ times its size. The expansion parameters used here are $\sigma=4\log\Delta/\Delta$ and $\rho=\Delta/(4\log\Delta)-1/2$ . A set is tiny when its size is at most $\sigma m$ Jenssen–Keevash–Perkins, Definition 21 and §4.4.

The graph $G^2$ joins distinct vertices whose distance in $G$ is at most two. On either side, a polymer is a nonempty, tiny, $G^2$ -connected vertex set. Two polymers on the same side are compatible if every pair of their vertices is more than distance two apart in $G$ . A polymer $\gamma$ has weight $w_\gamma=\lambda^{|\gamma|}/(1+\lambda)^{|\partial\gamma|}$ . Summing products of weights over mutually compatible polymer families gives the partition functions $\Xi^{\mathcal E}(G)$ and $\Xi^{\mathcal O}(G)$ Jenssen–Keevash–Perkins, §§4.1, 4.4.

“Almost every” means that, for fixed $\Delta$ , the fraction of labelled $\Delta$ -regular bipartite graphs satisfying a property tends to one as $m$ tends to infinity. The random graph is chosen uniformly from graphs on the two fixed sides Jenssen–Keevash–Perkins, p. 3.

Formalization targets

The first target is the authors' expansion premise: for all sufficiently large $\Delta$ , almost every graph is a bipartite $(4\log\Delta/\Delta,\Delta/(4\log\Delta)-1/2)$ -expander. The main target combines two deterministic claims on almost every such graph. For every $\lambda>50\log^2\Delta/\Delta$ , write $n=2m$ and

\widehat Z_G(\lambda)=(1+\lambda)^m\bigl(\Xi^{\mathcal E}(G)+\Xi^{\mathcal O}(G)\bigr),\qquad \varepsilon_0=(1+\lambda)^{-n/4}.

First, $\widehat Z_G$ is an $\varepsilon_0$ -relative approximation in the paper's exponential convention:

e^{-\varepsilon_0}\widehat Z_G(\lambda)\le Z_G(\lambda)\le e^{\varepsilon_0}\widehat Z_G(\lambda).

Second, each of the two polymer models obeys the Kotecký–Preiss condition with decay $g(\gamma)=|\gamma|\Delta\log(1+\lambda)/(10\log\Delta)$ :

\sum_{\gamma'\text{ incompatible with }\gamma}w_{\gamma'}e^{|\gamma'|+g(\gamma')}\le |\gamma|.

The same graph event must support every activity above the threshold; the activity quantifier is inside the limiting probability. The intermediate targets are Bassalygo's entropy criterion, the high probability expansion lemma, the tiny-side lemma for independent sets, the approximation lemma at its weaker activity threshold, a published binomial-entropy estimate, and the per-vertex polymer sum bound Jenssen–Keevash–Perkins, Theorem 22, Lemmas 23–25 and §4.5.

Significance

The reduction expresses a weighted independent-set count through two finite polymer partition functions whose weights decay under the same expansion condition. The KP bound supplies the convergence condition used by the paper's general polymer approximation theorem. Together these are the mathematical inputs to its algorithmic Theorem 2 Jenssen–Keevash–Perkins, Theorems 2, 8.

A formal proof would make the expansion assumptions, distance convention, graph probability limit, and error normalization explicit. The target is a formalization of a published result, not an open conjecture. The proposal contains statements and definitions; their proofs remain to be supplied. The binomial estimate is already machine checked on Prove2Me and is included by reference.

Difficulty

An independent set can occupy vertices on both sides of a bipartite graph. Merely taking one side as the dominant phase double counts sets that are sparse on both sides. The tiny-side lemma and the polymer decomposition identify and control that overlap. The random graph step also requires an expansion estimate strong enough to apply to every small subset of either side, rather than only to a typical subset Jenssen–Keevash–Perkins, §§4.4–4.5.

Formalization scope

Lean uses finite simple graphs on $\mathrm{Fin}(m)\oplus\mathrm{Fin}(m)$ , with the left and right summands serving as the odd and even sides. This fixes a labelled bipartition for the uniform random graph model. Distances use extended natural graph distance, so vertices in different components have infinite distance. Polymer families include the empty family, and graph connectivity excludes the empty polymer. Sizes are natural numbers; thresholds involving logarithms are real inequalities. Binary entropy in the cited expansion theorem is measured in bits, while Mathlib's binary entropy is converted from natural units. The approximation uses exponential relative error exactly as in Definition 10 of the paper.

The FPTAS, sampling algorithm, and running-time assertion are outside this mission because Mathlib has no matching machine and cost model. The goal formalizes both the partition-function reduction and its KP condition, the mathematical inputs consumed by the paper's algorithm theorem. It quantifies over all activities above the threshold within the almost-every event, preventing a separate favorable graph set for each activity. The fixed-sides model and the explicit domain of Bassalygo's entropy formula are disclosed representation choices. The tiny-side milestone (Lemma 24) carries a graph-size threshold depending on the degree: as printed, for every graph size, it fails on small dense graphs (the complete bipartite graph minus disjoint complete blocks), and the main result uses it only as the graph size grows. Reusable contributions include finite graph expansion lemmas, polymer partition-function identities, and bounds on connected vertex sets.

Selected references

M. Jenssen, P. Keevash and W. Perkins, Algorithms for #BIS-hard problems on expander graphs, SIAM Journal on Computing 49(4), 2020, 681–710. DOI.
L. Bassalygo, Asymptotically optimal switching circuits, Problems of Information Transmission 17(3), 1981, 206–211. Publisher record.
C. Liao, J. Lin, P. Lu and Z. Mao, Counting independent sets and colorings on random regular bipartite graphs, APPROX/RANDOM, 2019. DOI.

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Distributionally Robust Convex Optimization IV: An Absolute Mean Spread Bound Describes Exactly the z̃-Marginals of a Lifted Ambiguity SetResearch Paper

Motivation

Distributionally robust optimization handles an uncertain parameter $\tilde z\in\mathbb R^P$ whose distribution is only partly known. A decision must satisfy an expectation constraint for every distribution in an ambiguity set, the set of distributions consistent with the available information. Wiesemann, Kuhn and Sim (Optimization Online preprint 3757, 2013; Operations Research 62(6), 2014, doi:10.1287/opre.2014.1314) introduce a standardized ambiguity set. Its members are joint distributions of $\tilde z$ and auxiliary random vectors $\tilde u$ , constrained by expectation conditions and by probability bounds on conic confidence sets. Worst-case expectation constraints over such a set have tractable conic reformulations. The practical question is which kinds of distributional information this format can express. A set over $(\tilde z,\tilde u)$ describes information about $\tilde z$ through its $\tilde z$ -marginals, so the precise claim is that some set of distributions of $\tilde z$ equals the projection of a standardized set.

Section 3 of the paper settles this question for several common descriptors of dispersion. One of them is the absolute mean spread, the gap between the mean of a random variable above a threshold and its mean below it. Levi, Perakis and Uichanco used it to describe demand uncertainty in data-driven newsvendor models (Oper. Res. 63(6), 2015). The paper notes that, unlike variance or coefficient-of-variation bounds, spread information "can no longer be constructed via straightforward application of Theorem 5", its general lifting result for conic-representable moment bounds. Proposition 2 provides a dedicated lifting instead.

Setting

Fix $f\in\mathbb R^P$ , a threshold $\theta\in\mathbb R$ , a spread budget $\sigma\ge0$ and a probability level $\rho\in(0,1)$ . For a probability distribution $\mathbb Q$ on $\mathbb R^P$ under which $f^\top\tilde z$ has a finite mean, write

\mathbb E_{\mathbb Q}[f^\top\tilde z\mid A]=\frac{\mathbb E_{\mathbb Q}[f^\top\tilde z\,\mathbf 1_A]}{\mathbb Q[A]},\qquad A\in\{f^\top\tilde z\ge\theta\},\ \{f^\top\tilde z<\theta\}.

The absolute mean spread of $f^\top\tilde z$ at $\theta$ is $\mathbb E_{\mathbb Q}[f^\top\tilde z\mid f^\top\tilde z\ge\theta]-\mathbb E_{\mathbb Q}[f^\top\tilde z\mid f^\top\tilde z<\theta]$ . The target set (spreadSet) consists of the $\mathbb Q$ with $\mathbb Q[f^\top\tilde z\ge\theta]=\rho$ whose spread is at most $\sigma$ .

The lifted ambiguity set $\mathcal P$ (liftedSpreadSet) consists of the probability distributions $\mathbb P$ of $(\tilde z,\tilde u,\tilde v,\tilde w)$ on $\mathbb R^P\times\mathbb R^3$ with $\mathbb E_{\mathbb P}[\tilde w]=\sigma$ and $\mathbb P[f^\top\tilde z\ge\theta]=\rho$ , satisfying almost surely

f^\top\tilde z=\theta+\tilde u-\tilde v,\qquad \tilde w\ge\rho^{-1}\tilde u+(1-\rho)^{-1}\tilde v,\qquad \tilde u,\tilde v\ge0 .

The marginal $\Pi_{\tilde z}\mathbb P$ is the law of $\tilde z$ under $\mathbb P$ , and $\Pi_{\tilde z}\mathcal P=\{\Pi_{\tilde z}\mathbb P:\mathbb P\in\mathcal P\}$ .

For the companion result, the Huber loss (8) is $H_\delta(z)=\tfrac12z^2$ if $|z|\le\delta$ and $\delta(|z|-\tfrac12\delta)$ otherwise, for $\delta>0$ .

Formalization targets

Goal: Proposition 2 (Absolute Mean Spread), pp. 17–18

\Pi_{\tilde z}\mathcal P=\Big\{\mathbb Q\in\mathcal P_0(\mathbb R^P):\ \mathbb E_{\mathbb Q}[f^\top\tilde z\mid f^\top\tilde z\ge\theta]-\mathbb E_{\mathbb Q}[f^\top\tilde z\mid f^\top\tilde z<\theta]\le\sigma,\ \mathbb Q[f^\top\tilde z\ge\theta]=\rho\Big\}.

The page states the conclusion as $\mathbb Q^0\in\Pi_{\tilde z}\mathcal P=\{\dots\}$ for a given $\mathbb Q^0$ in the right-hand set. The set identity is the content, and it is the goal.

Milestones

The milestones follow the two inclusions of the proof (pp. 40–41).

For every $\mathbb P\in\mathcal P$ :

\mathbb E_{\mathbb P}[f^\top\tilde z\mid f^\top\tilde z\ge\theta]\le\rho^{-1}\mathbb E_{\mathbb P}[\tilde u]+\theta,\qquad \mathbb E_{\mathbb P}[f^\top\tilde z\mid f^\top\tilde z<\theta]\ge(1-\rho)^{-1}\mathbb E_{\mathbb P}[-\tilde v]+\theta.

Combining them gives

\text{spread}\le\rho^{-1}\mathbb E_{\mathbb P}[\tilde u]+(1-\rho)^{-1}\mathbb E_{\mathbb P}[\tilde v]\le\mathbb E_{\mathbb P}[\tilde w]=\sigma,

and hence $\Pi_{\tilde z}\mathcal P$ is contained in the target set. 2. For $\mathbb Q$ in the target set, $\tilde u=[f^\top\tilde z-\theta]^+$ and $\tilde v=[\theta-f^\top\tilde z]^+$ satisfy

\mathbb E[\tilde u]=\rho\,\mathbb E_{\mathbb Q}[f^\top\tilde z\mid f^\top\tilde z\ge\theta]-\rho\theta,\qquad \mathbb E[\tilde v]=(1-\rho)\,\mathbb E_{\mathbb Q}[-f^\top\tilde z\mid f^\top\tilde z<\theta]+(1-\rho)\theta .

Consequently $\mathbb E[\rho^{-1}\tilde u+(1-\rho)^{-1}\tilde v]$ equals the spread, and the target set is contained in $\Pi_{\tilde z}\mathcal P$ . 3. A companion, Proposition 3, assertion 3 (p. 21): for $\delta>0$ and $g\ge0$ , the distributions with $\mathbb E_{\mathbb Q}[H_\delta(f^\top\tilde z)]\le g$ are exactly the $\tilde z$ -marginals of a lifted set on $\mathbb R^P\times\mathbb R^5_+$ with auxiliary variables $\tilde u,\tilde v,\tilde w,\tilde s,\tilde t$ .

Significance

The proposition places absolute mean spread information inside the paper's standardized framework. Every result proved there for standardized sets therefore applies to spread-constrained ambiguity sets. The lifted set of Proposition 2 violates the paper's nesting condition (N), so Theorem 1's exact reformulation does not apply. Instead, Theorem 3 and Observation 1 give conservative approximations, which here are linear programs (p. 18). The Huber companion does the same for an expected Huber loss bound, a robust alternative to a variance bound.

Both results are proved in the paper. Neither has a machine-checked proof that this mission is aware of. A formalization adds three things: a checked equality of the two sets, with every integrability and positivity side condition made explicit; reusable lemmas on elementary conditional means of a scalar projection; and a check of the companion. The companion's printed proof contains an incorrect intermediate identity (see Difficulty), although the proposition itself holds.

Difficulty

The obvious reading of the inclusion $\Pi_{\tilde z}\mathcal P\subseteq$ target is "the constraint on $\tilde w$ bounds the spread pointwise". That reading fails, because the spread is a ratio of expectations over two complementary events, and $\tilde u$ and $\tilde v$ are not determined by $\tilde z$ . Only their difference is fixed, almost surely. The bound must hold for every coupling of $(\tilde u,\tilde v)$ with $\tilde z$ that respects the constraints. The reverse inclusion needs an explicit lift of an arbitrary $\mathbb Q$ . The lift has to meet the moment condition $\mathbb E[\tilde w]=\sigma$ exactly, not just as an inequality. The paper leaves that step implicit.

In Lean the main friction is measure-theoretic bookkeeping: integrability of the auxiliary coordinates (which is derived, not assumed), set integrals over the two half-spaces, and push-forwards along the first projection. In the Huber companion, the identity the proof states for the minimized integrand is false in general: with $\delta=1$ and $\tilde u=\tilde v=\tfrac12$ the left side is $\tfrac14$ and the right side is $\tfrac12$ . The inclusion $\Pi_{\tilde z}\mathcal P\subseteq\{\dots\}$ needs a different pointwise inequality.

Formalization scope

$\mathbb R^P$ is Fin nP → ℝ, with $f^\top z$ written f ⬝ᵥ z. The lifted outcome space is (Fin nP → ℝ) × (ℝ × ℝ × ℝ), and $\tilde u,\tilde v,\tilde w$ are the projections uOf, vOf, wOf. The Huber lift uses Fin 5 → ℝ with components $0,\dots,4=\tilde u,\tilde v,\tilde w,\tilde s,\tilde t$ .
The marginal $\Pi_{\tilde z}\mathbb P$ is μ.map Prod.fst. Both theorems are stated as set identities between Set (Measure _).
Conditional means are elementary: $\mathbb E[f^\top\tilde z\,\mathbf 1_A]/\mathbb Q[A]$ (condMeanGe, condMeanLt). σ-algebra conditioning is not used. Both events have probability $\rho$ or $1-\rho$ , both positive because $\rho\in(0,1)$ , so no division by zero occurs.
Integrability convention.
- Members of the target set have $f^\top\tilde z$ integrable, and members of $\mathcal P$ have $\tilde w$ integrable. These are the expectations the page writes, and Lean's integral of a non-integrable function is $0$ , so without these clauses the sets would contain junk members.
- Integrability of $\tilde u$ , $\tilde v$ and $f^\top\tilde z$ under $\mathbb P\in\mathcal P$ is not assumed. It follows from $0\le\tilde u\le\rho\tilde w$ and $0\le\tilde v\le(1-\rho)\tilde w$ almost surely.
- In the companion, $H_\delta(f^\top\tilde z)$ is required to be integrable under $\mathbb Q$ .
Hypotheses are the page's: $\sigma\ge0$ and $0<\rho<1$ ; for the companion, $\delta>0$ and $g\ge0$ . Nothing is added.
Printed typo. Proposition 3.3 prints $H_\delta(t^\top\tilde z)$ in its conclusion. No $t$ occurs there, and the hypothesis and the proof use $f^\top\tilde z$ , so the Lean states $f^\top\tilde z$ .
No trivializing reading. Neither side is empty by construction: the law $\tfrac12(\delta_{-1}+\delta_1)$ on $\mathbb R^1$ with $f=1$ , $\theta=0$ , $\rho=\tfrac12$ , $\sigma=2$ lies in the target set and is the marginal of a member of $\mathcal P$ , as checked in a sorry-free sanity file. For $P=0$ both sides are empty, consistently.
Infrastructure. Elementary conditional means of a scalar projection over complementary half-spaces, set integrals of positive and negative parts, and push-forwards along Prod.fst are reusable beyond this mission. Proofs of the individual milestones are welcome, as are reusable lemmas on lifts of the form $z\mapsto(z,\phi(z))$ .

Selected references

W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Optimization Online preprint 3757 (version of September 22, 2013); Operations Research 62(6):1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6):1294–1306, 2015. https://doi.org/10.1287/opre.2015.1422
P. J. Huber, Robust Estimation of a Location Parameter, Annals of Mathematical Statistics 35(1):73–101, 1964. https://doi.org/10.1214/aoms/1177703732

12 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Distributionally Robust Convex Optimization II: The Naïve Approximation Implies the Infimal Convolution Bound, Which Implies the Distributionally Robust ConstraintResearch Paper

Motivation

A constraint $\mathbb E[v(x,\tilde z)] \le w$ on a decision $x$ needs the distribution of the random vector $\tilde z$ , which in practice is known only through partial information: a support, some moments, the probability mass of a few regions. Distributionally robust optimization requires the constraint for every distribution consistent with that information. Wiesemann, Kuhn and Sim (Optimization Online 3757, 2013; Oper. Res. 62(6), 2014) introduced a standardized ambiguity set built from expectation conditions and probability bounds on confidence sets. Their Theorem 1 shows that the worst-case constraint over such a set is equivalent to a finite conic system, provided the confidence sets satisfy a nesting condition: any two are strictly nested or disjoint.

Many natural ambiguity sets violate nesting, for instance two overlapping confidence ellipsoids. For these the paper (§2.2) proposes two conservative approximations, the naïve approximation and the infimal convolution bound, and Theorem 3 orders them: the naïve approximation implies the infimal convolution bound, which implies the robust constraint. Infimal convolution bounds of this type had been used in classical and distributionally robust optimization before, e.g. in Goh and Sim (2010), Theorem 4. This mission formalizes Theorem 3, the steps of its proof, and Proposition 1, which compares partitions.

Setting

The random vector is $\tilde z \in \mathbb R^P$ , with an auxiliary $\tilde u \in \mathbb R^Q$ . A proper cone $\mathcal K$ is a closed convex cone with $\mathcal K\cap(-\mathcal K)=\{0\}$ and nonempty interior, and $x \preccurlyeq_{\mathcal K} y$ means $y - x\in\mathcal K$ . For $i \in \mathcal I = \{1,\dots,I\}$ the confidence sets are $\mathcal C_i = \{(z,u) : C_iz + D_iu \preccurlyeq_{\mathcal K_i} c_i\}$ , and the ambiguity set is

\mathcal P = \Big\{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \ \mathbb P[(\tilde z,\tilde u)\in\mathcal C_i]\in[\underline p_i,\overline p_i]\ \ \forall i\in\mathcal I\Big\}.

The standing conditions are: (C1) $\mathcal C_I$ is bounded with $\underline p_I = \overline p_I = 1$ (it is the support); (C2) some $\mathbb P\in\mathcal P$ meets every non-degenerate probability bound strictly; (C3) $v(x,z) = \max_{l}\,[(S_lz+s_l)^\top x + \mathbf t_l^\top z + t_l]$ , a maximum of finitely many bi-affine pieces, so $v$ is convex in $x$ . The distributionally robust constraint (3) is $\mathbb E_{\mathbb P}[v(x,\tilde z)]\le w$ for all $\mathbb P\in\mathcal P$ .

Write $A \Subset B$ when $A$ lies in the interior of $B$ . A partition $\{\mathcal I_j\}_{j\in\mathcal J}$ of $\mathcal I$ , with $J = |\mathcal J|$ blocks, satisfies the weak nesting condition (N′) if within each block any two distinct confidence sets are strictly nested or disjoint. The outer approximation $\mathcal P^j$ keeps the expectation condition and only the probability bounds of block $j$ :

\mathcal P^j = \Big\{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \ \mathbb P[(\tilde z,\tilde u)\in\mathcal C_i]\in[\underline p_i,\overline p_i]\ \ \forall i\in\mathcal I_j\Big\}.

With $\Gamma(x) = \{(y,\delta) : \sum_j y_j = x,\ \sum_j\delta_j = 1,\ \delta > 0\}$ , the naïve approximation (6) and the infimal convolution bound (7) are

\min_{j\in\mathcal J}\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}[v(x,\tilde z)]\le w,\qquad \inf_{(y,\delta)\in\Gamma(x)}\sum_{j\in\mathcal J}\delta_j\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}[v(y_j/\delta_j,\tilde z)]\le w.

Formalization targets

Goal: Theorem 3 (p. 13)

\text{(6)}\ \Longrightarrow\ \text{(7)}\ \Longrightarrow\ \text{(3)},\qquad\text{and (3)} \Longrightarrow \text{(7)},\ \text{(3)}\Longrightarrow\text{(6)}\ \text{ if } J = 1,

under (C1)–(C3), (N′) and one disclosed added hypothesis, the uniform first-moment bound (see Formalization scope).

Milestones (proof of Theorem 3, p. 37; Proposition 1, p. 14)

$\mathcal P\subseteq\mathcal P^j$ for every $j$ (p. 12).
The chain: for $(y,\delta)\in\Gamma(x)$ , $\sum_j\delta_j\sup_{\mathcal P^j}\mathbb E[v(y_j/\delta_j,\tilde z)] \ge \sum_j\delta_j\sup_{\mathcal P}\mathbb E[v(y_j/\delta_j,\tilde z)] \ge \sup_{\mathcal P}\mathbb E[v(x,\tilde z)]$ .
(7) $\Rightarrow$ (3).
The limiting display: with $\delta_{j^\star}(k) = 1-1/k$ , $y_{j^\star} = x$ and $\delta_j(k) = 1/(k(J-1))$ , $y_j = 0$ otherwise,

\sum_j\delta_j(k)\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}[v(y_j/\delta_j(k),\tilde z)]\ \xrightarrow[k\to\infty]{}\ \sup_{\mathbb P\in\mathcal P^{j^\star}}\mathbb E_{\mathbb P}[v(x,\tilde z)].

(6) $\Rightarrow$ (7).
If $J = 1$ then $\mathcal P = \mathcal P^1$ .
Proposition 1: if one partition refines another, both satisfying (N′), then (7) for the finer partition implies (7) for the coarser one.

Significance

The result. Theorem 1 of the paper needs nesting; Theorem 3 is what remains when nesting fails. It certifies that both surrogates are safe (a decision satisfying either satisfies the robust constraint) and that the infimal convolution bound is never looser than the naïve one. The paper also shows that (7), with $\Gamma(x)$ replaced by a closed approximation, has a conic reformulation (Observation 1), while optimizing over (6) with several constraints is strongly NP-hard (Theorem 4). Proposition 1 then says coarser partitions give tighter bounds, which guides the choice of partition.

Formalizing it. The result is proved in the paper; no machine-checked version is known. Formalizing it produces a reusable layer of extended-real worst-case expectations over sets of probability measures, with the infimal convolution and the perspective $\delta\,v(y/\delta,\cdot)$ , and it corrects a gap in the printed proof of (6) $\Rightarrow$ (7) (see below).

Difficulty

The implications (7) $\Rightarrow$ (3) and Proposition 1 are short on paper; in Lean the work lies in extended-real arithmetic, where $-\infty+\infty=-\infty$ , and in the integrability of $v(x,\tilde z)$ . The step (6) $\Rightarrow$ (7) is the delicate one. The constraint $\delta>0$ forbids putting all weight on the minimizing block, so the bound is reached only in a limit, and the limit requires every block's worst-case expectation of $v(0,\tilde z)$ , and of $\delta\,v(x/\delta,\tilde z)$ uniformly in $\delta$ , to be controlled. The outer approximations drop the support condition (C1) for blocks that do not contain $I$ , so these worst-case values can be $+\infty$ , and the printed justification fails.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ; the outcome space is $(\texttt{Fin nP → ℝ})\times(\texttt{Fin nQ → ℝ})$ with its Borel σ-algebra. Indices are 0-based: $\mathcal I$ is Fin (nI + 1) (so $I\ge1$ ), $\mathcal C_I$ is index Fin.last nI, and $\mathcal J$ is Fin nJ. A partition is a surjective block map blk : Fin (nI + 1) → Fin nJ, so every block is nonempty; " $J=1$ " is nJ = 1. Distributions in $\mathcal P$ and in every $\mathcal P^j$ are probability measures with a finite first moment, since a Lean integral of a non-integrable function is $0$ . Worst-case expectations, (6) and (7) take values in EReal, with $\sup\emptyset=-\infty$ ; the minimum in (6) is a finite infimum, and $y_j/\delta_j$ is used only on $\Gamma(x)$ , where $\delta>0$ . Constraint (3) is in its $\forall$ -form.

Added hypothesis. The goal, milestone 4 and milestone 5 assume a uniform first-moment bound: for every $j$ , $\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}\|\tilde z\| < \infty$ . Without it (6) $\Rightarrow$ (7) is false: with $P=1$ , $\mathcal C_1=[0,\tfrac12]$ of probability at least $\tfrac12$ , $\mathcal C_2=[0,1]$ of probability $1$ , the singleton partition, $v(x,z)=z$ and $w=1$ , (6) holds through $\mathcal P^2$ , while $\mathcal P^1$ contains $\tfrac12\delta_0+\tfrac12\delta_M$ for every $M$ , so (7) fails. The bound holds whenever every block contains a bounded confidence set with $\underline p_i=1$ . No other hypothesis is added; (N′), (C1) and the cone conditions are kept as on the page although the proofs do not use them.

The definitions rule out the trivializing formalizations: no expectation is a junk integral, empty blocks are excluded by surjectivity, the ambiguity set is nonempty under (C2), and no real-valued supremum or division by a zero weight appears. Contributions welcome: proofs of the milestones, and reusable lemmas on EReal suprema of integrals and on perspectives of piecewise-affine functions.

Selected references

W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Optimization Online preprint 3757, version of September 22, 2013. https://optimization-online.org/wp-content/uploads/2013/02/3757.pdf
W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Operations Research 62(6):1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
J. Goh, M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4):902–917, 2010. https://doi.org/10.1287/opre.1090.0712

9 thms2 active usersReviewed

Completed

Machine Learning Statistics·Captain: mikedeng1

Robustness May Be at Odds with Accuracy 1: Every Classifier with Standard Accuracy ≥ 1 − δ Has ℓ∞ Robust Accuracy ≤ pδ/(1 − p) Against ε ≥ 2ηResearch Paper

Motivation

Classifiers trained to be robust against small, adversarially chosen input perturbations routinely lose standard accuracy. Adversarial training (Madry et al., 2018) improves worst-case accuracy under an $\ell_p$ -bounded attack, but on MNIST, CIFAR-10 and ImageNet the resulting models are measurably less accurate on unperturbed inputs, and the loss grows with the attack radius. A natural reading is that this is an artefact of training procedures or of finite data.

Tsipras, Santurkar, Engstrom, Turner and Mądry (ICLR 2019) argue otherwise: they exhibit a simple distribution on which every classifier faces the trade-off, so that the tension is a property of the data distribution itself and survives infinite data, including for the Bayes-optimal classifier. The argument isolates a distinction that has since been influential: robust features, moderately correlated with the label and stable under small perturbations, versus non-robust features, individually weak but jointly highly predictive and easily flipped. This mission formalizes the paper's first theorem, Theorem 2.1, and its proof in Appendix C.

Setting

Fix $d \in \mathbb N$ , a probability $p$ with $\tfrac12 \le p < 1$ , and $\eta \ge 0$ . The distribution $\mathcal D$ of an input-label pair $(x, y)$ , $x = (x_1, x_2, \dots, x_{d+1}) \in \mathbb R^{d+1}$ , is the data model (3):

y \sim \mathrm{Unif}\{-1,+1\}, \qquad x_1 = \begin{cases} +y & \text{w.p. } p\\ -y & \text{w.p. } 1-p\end{cases}, \qquad x_2, \dots, x_{d+1} \overset{\text{i.i.d.}}{\sim} \mathcal N(\eta y, 1),

with $x_1$ and $(x_2, \dots, x_{d+1})$ independent given $y$ . Write $G_+$ and $G_-$ for the law $\mathcal N(\pm\eta, 1)^{\otimes d}$ of the weak features given $y = +1$ and $y = -1$ .

A classifier is a measurable map $f : \mathbb R^{d+1} \to \{-1, +1\}$ . Its standard accuracy is $\Pr_{(x,y)\sim\mathcal D}[f(x) = y]$ , the objective (1) of the paper with the 0–1 loss. Its $\ell_\infty$ robust accuracy at radius $\varepsilon$ is

\mathrm{acc}_\varepsilon(f) = \Pr_{(x,y)\sim\mathcal D}\big[f(x + \delta) = y \text{ for every } \delta \in \mathbb R^{d+1} \text{ with } \|\delta\|_\infty \le \varepsilon\big],

the objective (2) with the 0–1 loss and perturbation set $\Delta = \{\|\delta\|_\infty \le \varepsilon\}$ . In Lean these are stdAcc d p η f and robustAcc d p η f ε, each an average with weight $\tfrac12$ of the two class-conditional probabilities. The proof also uses $p_{ij}$ , the probability that $f$ predicts $+1$ when $x_1 = i$ and the weak features follow $G_j$ (pij), and the shift adversary $x_i \mapsto x_i - 2\eta y$ for $i \ge 2$ (shiftAdv, accuracy shiftAcc).

Formalization targets

Goal: Theorem 2.1 (p. 5)

For every measurable classifier $f$ and every $\delta \in \mathbb R$ ,

\Pr[f(x) = y] \ge 1 - \delta \ \Longrightarrow\ \mathrm{acc}_\varepsilon(f) \le \frac{p}{1-p}\,\delta \qquad \text{for every } \varepsilon \ge 2\eta.

The statement quantifies over all classifiers, not a parametric family, and over every radius $\varepsilon \ge 2\eta$ .

Milestones (App. C, pp. 14–16)

The shift $z_i \mapsto z_i - 2\eta y$ pushes $\mathcal N(\eta y, 1)^{\otimes d}$ forward to $\mathcal N(-\eta y, 1)^{\otimes d}$ : it changes $G_+$ to $G_-$ and vice versa.
For $\varepsilon \ge 2\eta \ge 0$ , robust accuracy is at most the accuracy against the shift adversary.
$\Pr[f(x) = y] = \tfrac12\big(p(1 + p_{++} - p_{--}) + (1-p)(1 + p_{-+} - p_{+-})\big)$ .
$\Pr[f(x_{\mathrm{adv}}) = y] = \tfrac12\big(p(1 + p_{+-} - p_{-+}) + (1-p)(1 + p_{--} - p_{++})\big)$ .
With $a = 1 - p_{++} + p_{--} \ge 0$ and $b = 1 - p_{-+} + p_{+-}$ : $1 - \tfrac12(pa + (1-p)b) \ge 1 - \delta$ implies $\tfrac12((1-p)a + pb) \le \tfrac{p}{1-p}\delta$ .

Companion statements (§2.1, pp. 4–5)

Tightness. $\mathrm{sign}(x_1)$ has standard accuracy $p$ and robust accuracy $p$ for $0 \le \varepsilon < 1$ ; at $\delta = 1-p$ the bound of Theorem 2.1 is attained.
Standard classification is easy. For $f_{\mathrm{avg}}(x) = \mathrm{sign}(\tfrac1d\sum_{i\ge2} x_i)$ , $\Pr[f_{\mathrm{avg}}(x) = y] = \Pr[\mathcal N(\eta, 1/d) > 0]$ , which exceeds $99\%$ when $\eta \ge 3/\sqrt d$ .

Significance

Theorem 2.1 converts the empirical observation into a statement about a distribution: on $\mathcal D$ , standard accuracy $1 - \delta$ caps robust accuracy at $\frac{p}{1-p}\delta$ , so as $\delta \to 0$ robust accuracy falls to $0$ , while the adversary's budget $\varepsilon = 2\eta = \Theta(1/\sqrt d)$ is small compared with the feature scale $\pm 1$ . Together with the companion statements it shows that the model admits a classifier with accuracy above $99\%$ and a classifier with robust accuracy $p$ , but no classifier with both. It underlies the paper's conclusion that robust training must give up non-robust features, and the later line of work on robust versus non-robust features.

The result is proved in the paper, with an elementary argument. As far as the platform record and a search of the literature show, it has not been machine-checked. The formalization adds an exact, convention-explicit version of the model and of robust accuracy (worst case over a closed $\ell_\infty$ ball, outer measure of a possibly non-measurable event), a Lean statement of the shift-invariance property of Gaussian products that the argument rests on, and a reusable template for 0–1-loss adversarial objectives that later missions on robustness in Gaussian models can follow.

Difficulty

The obvious attempt is to bound robust accuracy for a specific classifier, or for linear classifiers, where the adversary's best response is explicit. That does not reach the theorem: the claim is about every measurable $f$ , for which no best response is computable and the robust event need not even be measurable. On the formal side, the statements involve the pushforward of a product of Gaussians under a coordinatewise shift, the decomposition of the class-conditional law into the two-point law of $x_1$ and the product $G_\pm$ , and a measure applied to a possibly non-measurable robust event; none of these is available as a ready-made lemma for this model.

Formalization scope

Inputs live in Fin (d + 1) → ℝ; coordinate 0 is $x_1$ and coordinate i.succ is $x_{i+2}$ . The Mathlib norm on this type is the sup norm, so ‖δ‖ ≤ ε is exactly the $\ell_\infty$ ball. Labels and predictions are the reals $\pm1$ . The class-conditional law is ((x1Law p y).prod (weakLaw d η y)).map (Matrix.vecCons ·.1 ·.2) with weakLaw d η y = Measure.pi (fun _ => gaussianReal (y * η) 1). Accuracies are real numbers in $[0,1]$ computed with toReal. The robust event is measured by its outer measure, i.e. under the completion of $\mathcal D$ ; no measurability of that event is assumed.

The standing assumption $p \ge \tfrac12$ of model (3) is a hypothesis of every statement. Four hypotheses implicit on the page are explicit: $p < 1$ in the goal (the bound divides by $1-p$ , and Lean's $p/0 = 0$ would make the statement false at $p = 1$ ); $\eta \ge 0$ (the page takes $\eta$ large, $\Theta(1/\sqrt d)$ ; with $\eta < 0$ the case $\varepsilon = 0$ has no adversary and the statement fails); measurability of $f$ ; and $f(x) \in \{\pm1\}$ for every $x$ .

A trivializing formalization is ruled out: the goal is stated for every measurable $\{\pm1\}$ -valued classifier and for the worst case over the full $\ell_\infty$ ball of every radius $\varepsilon \ge 2\eta$ , not for linear classifiers, not for the fixed shift adversary, and not with the $p_{ij}$ among its hypotheses; those appear only in milestones.

The development needs Mathlib's gaussianReal, Measure.pi, product measures and pushforwards. Welcome contributions: the Gaussian shift identity (reusable for any Gaussian location model), the disintegration of condLaw along $x_1$ , and the two accuracy formulas.

Selected references

D. Tsipras, S. Santurkar, L. Engstrom, A. Turner, A. Mądry, Robustness May Be at Odds with Accuracy, ICLR 2019; arXiv:1805.12152v5 (2019). https://arxiv.org/abs/1805.12152
A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018. https://arxiv.org/abs/1804.11285

7 thms2 active usersReviewed

Bandit Algorithms Operations Research·Captain: mikedeng1

A Primal-Dual Learning Algorithm for Personalized Dynamic Pricing with an Inventory Constraint: The Primal-Dual Learning Algorithm Has Regret at Most C(log n)^(2+δ) n^(−1/2)Research Paper

Motivation

A firm selling a fixed stock of a perishable product over a finite season must set prices without knowing how demand responds to them. Online retail and travel platforms often see a customer's segment before quoting a price, so they can price-discriminate across consumer types. Learning a separate demand curve for each type, however, seems to cost more exploration as the number of types grows. Chen and Gallego (arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022) give a learning algorithm whose regret does not depend on the number of types. Their key step is to learn a single scalar first: the shadow price of inventory.

Earlier work on the single-type problem frames the question. Besbes and Zeevi (Operations Research, 2009) defined the regret against the fluid benchmark and showed that no policy can achieve regret decaying faster than $n^{-1/2}$ . Wang, Deng and Ye (Operations Research, 2014) gave a single-product algorithm whose regret matches this rate up to logarithmic factors. Chen and Gallego extend the rate to $M$ types with one inventory constraint.

Setting

There are $M\ge1$ consumer types, a season $[0,T]$ and an inventory $c$ . When the firm charges price $p$ to type $m$ , type- $m$ consumers arrive at rate $d_m(p)$ . Prices range over $[0,p_\infty]$ , where $p_\infty$ is a choke price with $d_m(p_\infty)=0$ . Assumption 1 asks that each $d_m$ be strictly decreasing, bounded and Lipschitz, and that the revenue rate $r_m(\lambda)=\lambda d_m^{-1}(\lambda)$ be Lipschitz and twice differentiable, with $0<M_3\le-r_m''\le M_4$ .

The fluid problem (2) maximizes $\sum_m\int_0^Tp_m(t)d_m(p_m(t))\,dt$ subject to $\sum_m\int_0^Td_m(p_m(t))\,dt\le c$ . Its optimal value is $J^D(T,c)$ . Its dual is one-dimensional. With

\mathcal R_m(z)=\max_{p}d_m(p)(p-z),\qquad \mathcal P_m(z)=\operatorname*{argmax}_pd_m(p)(p-z),\qquad g(z)=cz+T\sum_m\mathcal R_m(z),

the dual optimum is $z^*=\operatorname{argmin}_{z\ge0}g(z)$ , and the optimal fluid prices are the constants $p^*_m=\mathcal P_m(z^*)$ .

In the $n$ -th system demand and inventory scale together: type $m$ arrives as a Poisson process with rate $n\,d_m(p)$ , and the inventory is $nc$ . The firm does not know $d_m$ . It knows $T$ , $c$ , $n$ , the constants of Assumption 1 and, by Assumption 2, intervals $[\underline p,\overline p]$ and $[0,\overline z]$ that contain every $p^*_m$ and $z^*$ . A policy $\pi$ has expected revenue $J^\pi_n(T,c)$ , and its regret is

R^\pi_n(T,c)=1-\frac{J^\pi_n(T,c)}{J^D_n(T,c)}.

Algorithm 1, the primal-dual learning algorithm, runs phases $k=1,\dots,K$ of shrinking lengths $\tau^{(k)}$ . In each learning phase it tests a price grid inside the current interval estimators of every $p^*_m$ . It then minimizes an empirical dual function on a grid of $z$ and re-centres the interval estimators of $z^*$ and $p^*_m$ . In the last phase it either charges a marked-up price (sufficient capacity), or tests two prices and interpolates between them so that total sales end close to $nc$ (insufficient capacity). Its tuning depends on a constant $\epsilon>0$ .

Formalization targets

Goal: Theorem 1 (p. 17)

For every $\delta>0$ one can choose $\epsilon>0$ and a constant $C$ , independent of $n$ , such that

R^\pi_n(T,c)\le C(\log n)^{2+\delta}n^{-1/2}\qquad\text{for all }n\ge3.

The two capacity regimes (Propositions 2–3)

z^*=0:\ R^\pi_n=O\big((\log n)^{2+16\epsilon}n^{-1/2}\big),\qquad z^*>0:\ R^\pi_n=O\big((\log n)^{2+18\epsilon}n^{-1/2}\big).

Milestones

Proposition 1: the fluid problem is solved by the constant prices $p^*$ , with complementary slackness; and the monotonicity, convexity and derivative of $\mathcal P_m$ and $\mathcal R_m$ .
Lemmas 9 and 10: a Poisson tail bound decaying faster than any power, and $\mathbb E|X-\lambda|\le\sqrt\lambda$ .
Lemmas 1 and 2: $K\le3\log n+3$ , and the learning phases take at most half the season.
Lemmas 3–5: the interval estimators contain $z^*$ , $p^*_m$ and $\mathcal P_m$ on the dual interval, except with probability $O((\log n)^2/n)$ .
Lemmas 6–7: the sales at the start of the last phase are close to the fluid level.
Lemma 8: when $z^*>0$ , $\mathbb E|S(T)-nc|=O((\log n)^\epsilon n^{1/2})$ .

Significance

Theorem 1 states that personalized pricing for $M$ types under a shared inventory constraint is learnable at the single-type rate $n^{-1/2}$ , up to logarithms, with a constant independent of $n$ . Combined with the Besbes–Zeevi lower bound, the algorithm is rate-optimal. Learning the scalar shadow price $z^*$ , instead of the joint optimum of an $M$ -dimensional problem, is what avoids the curse of dimensionality.

The result is proved in the paper; no machine-checked version exists. A formalization would add to the platform a multi-type Poisson pricing model with stock-outs, the one-dimensional Lagrangian dual of the fluid revenue-management problem, an exactly specified multi-phase learning algorithm, and reusable Poisson deviation lemmas. Lemmas 1, 2, 9 and 10 and Proposition 1 can be proved independently of the probabilistic analysis.

Difficulty

The obvious argument estimates every $p^*_m$ directly and charges the estimate. With interval estimators of width $n^{-1/4}$ this loses revenue of order $n^{-1/4}$ per unit time when the inventory constraint binds ( $z^*>0$ ), because $p^*_m$ is then not the unconstrained maximizer of $p\,d_m(p)$ . The paper's (11) and (19) show the loss. The bound $n^{-1/2}$ requires steering the total sales to within $O(n^{1/2})$ of the inventory, which is Lemma 8, and a second-order expansion of the revenue around $p^*$ that uses the first-order condition $r_m'(d_m(p^*_m))=z^*$ .

Formally, a further difficulty is the closed loop: the prices of a phase depend on the counts of earlier phases, and the counts are Poisson only conditionally, through the random time change $N_m(n\int_0^td_m(P_m(s))\,ds)$ .

Formalization scope

All declarations live in the namespace PrimalDualPricing.Regret. Printed page numbers equal PDF page numbers in the cited preprint.

Model. Types are Fin M. Each $d_m:\mathbb R\to\mathbb R$ satisfies Assumption 1 on $[0,p_\infty]$ and is otherwise any extension with $0\le d_m\le M_1$ ; the last-phase prices $\underline p^{(K)}_m-\alpha$ and $\overline p^{(K)}_m+\alpha$ can leave $[0,p_\infty]$ . $d_m(p_\infty)=0$ encodes the choke price. $\mathcal P_m$ and $z^*$ are fields carrying their optimality properties.
Assumption 2 is read with $z^*\in[0,\overline z)$ ; the page prints $(0,\overline z)$ , which would drop the case $z^*=0$ that Proposition 2 and Theorem 1 cover. The price interval is placed in the domain, $0\le\underline p<\overline p\le p_\infty$ .
Remark 2 assumes $M_3\le g''\le M_4$ ; this is read on $[0,\overline z]$ , because globally it is unsatisfiable. Each $\mathcal P_m$ is $M_2$ -Lipschitz.
The fluid value $J^D$ is the supremum of (2) over measurable price paths. The identity $J^D=T\sum_mp^*_md_m(p^*_m)$ is Proposition 1.4, a milestone, and is not built into the definition.
The algorithm. The grid sizes $N^{(k)}$ , $N_z^{(k)}$ are rounded up. Grid spacing is $\Delta_m/N$ for prices and $\Delta_z/(N_z+1)$ for duals: the text and Table 1, respectively the text and line 15, agree on these, and Algorithm 1 line 7 and Table 1 print the other forms. Ties in (8)–(9) go to the smallest index. $\theta$ in (14) is projected onto $[0,1]$ , with $\theta=0$ when (14) is degenerate. An empty $p^l$ period in step 4 follows the pseudo-code. The decision rules never take $d_m$ , $\mathcal P_m$ or $z^*$ as arguments.
The system. $M$ independent unit-rate Poisson processes (the published IsPoissonProcess) with right-continuous, jointly measurable paths. The inventory of the $n$ -th system is $\lfloor nc\rfloor$ units, and nothing is sold after the stock-out. Lemmas 6–8 use the uncapped sales of the paper's modified system (§4).
Asymptotics. " $O(f(n))$ " is read as $\exists C$ , independent of $n$ and the phase index, for all $n\ge3$ . "Sufficiently small $\epsilon$ " is read as every $\epsilon\in(0,\epsilon_0)$ . The algorithm needs $n\ge3$ for $K$ to exist.
Corrected misprints. Proposition 1.2 prints $\mathcal R_m'=-\sum_md_m(\mathcal P_m)$ with the index reused; the statement is $-d_m(\mathcal P_m(z))$ . Proposition 1.3 and the global form of the bound in 1.1 fail at the kinks of $\mathcal P_m$ . Part 1's derivative bound is stated as a Lipschitz bound, and part 3 is omitted. Lemmas 3–4 are stated in product form. Propositions 2–3 are stated through their regret conclusions. The printed comparison $\tilde J^\pi_n\le J^\pi_n$ (pp. 13–14) can fail when a last-phase price exceeds $\overline p$ , so it is not used.

A formalization that lets the policy read the true demand, measures regret against anything other than $J^D_n$ , ignores the stock-out in $J^\pi_n$ , or assumes the high-probability events of Lemma 5 would trivialize the goal; none of these is done here.

Contributions to the reusable parts are welcome: Poisson tails, the envelope theorem for $\mathcal R_m$ , and the time-change construction of policy-driven Poisson sales.

Selected references

N. Chen, G. Gallego, A Primal-dual Learning Algorithm for Personalized Dynamic Pricing with an Inventory Constraint, arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1812.09234
O. Besbes, A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6), 2009. https://doi.org/10.1287/opre.1080.0640
Z. Wang, S. Deng, Y. Ye, Close the Gaps: A Learning-While-Doing Algorithm for Single-Product Revenue Management Problems, Operations Research 62(2), 2014. https://doi.org/10.1287/opre.2013.1249
G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24

21 thms2 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming 4: The Mini-Batch RSAG Method Bounds the Expected Gradient Mapping on Nonconvex Stochastic Composite ProblemsResearch Paper

Motivation

Training a model by stochastic gradients on a constrained or regularized loss is a stochastic composite problem: a smooth expected loss, observed only through noisy gradients, plus a simple non-smooth term such as a constraint set or an $\ell_1$ penalty. For convex losses, accelerated stochastic approximation methods attain the optimal rates (Lan 2012; Ghadimi & Lan 2012). For nonconvex losses, the available guarantees came from randomized stochastic gradient methods (Ghadimi & Lan 2013) and their mini-batch proximal versions (Ghadimi, Lan & Zhang 2016), which are not optimal when the problem happens to be convex.

Ghadimi and Lan (arXiv:1310.3787v1, 2013; Math. Program. 156, 2016) gave one accelerated scheme covering both cases. This mission formalizes its most general result, Theorem 4 (§3.2): the randomized stochastic accelerated gradient (RSAG) method with mini-batches, on a composite objective whose smooth part may be nonconvex and whose gradients are noisy.

Setting

Work in $\mathbb R^n$ with the Euclidean norm. The problem (1.3) is

\min_{x\in\mathbb R^n}\ \Phi(x):=\Psi(x)+\mathcal X(x),\qquad\Psi=f+h,

where $f$ is differentiable with $L_f$ -Lipschitz gradient and may be nonconvex, $h$ is convex and differentiable with $L_h$ -Lipschitz gradient, $L_\Psi=L_f+L_h$ , and $\mathcal X$ is a convex, possibly non-smooth function with bounded domain $K$ (for instance the indicator of a convex compact set, or that indicator plus $\|\cdot\|_1$ ).

The prox map (2.37) is $\mathcal P(x,y,c)=\operatorname{argmin}_u\{\langle y,u\rangle+\frac1{2c}\|u-x\|^2+\mathcal X(u)\}$ for $c>0$ , and the gradient mapping (2.38) is $\mathcal G(x,y,c)=\frac1c[x-\mathcal P(x,y,c)]$ . With $y=\nabla\Psi(x)$ , a small $\|\mathcal G\|$ certifies approximate stationarity. Assumption 2 asks for $M$ with $\|\mathcal P(x,y,c)\|\le M$ for all $x,y$ and $c>0$ .

Gradients come from a stochastic oracle: queried at $x$ , it returns $G(x,\xi)$ for a random sample $\xi$ . Assumption 1 asks that the output be unbiased, $\mathbb E[G(x,\xi)]=\nabla\Psi(x)$ , with variance at most $\sigma^2$ .

Algorithm 4 takes $\alpha_1=1$ , $\alpha_k\in(0,1)$ for $k\ge2$ , $\beta_k,\lambda_k>0$ , batch sizes $m_k\ge1$ , starts from $x_0=x^{ag}_0$ , and for $k\ge1$ sets

x^{md}_k=(1-\alpha_k)x^{ag}_{k-1}+\alpha_kx_{k-1},\qquad\bar G_k=\frac1{m_k}\sum_{i=1}^{m_k}G(x^{md}_k,\xi_{k,i}),

x_k=\mathcal P(x_{k-1},\bar G_k,\lambda_k),\qquad x^{ag}_k=\mathcal P(x^{md}_k,\bar G_k,\beta_k).

With $\Gamma_1=1$ and $\Gamma_k=(1-\alpha_k)\Gamma_{k-1}$ (2.6), the output is $(x^{md}_R,x^{ag}_R)$ , where $R\in\{1,\dots,N\}$ is drawn independently of the oracle with

\mathrm{Prob}\{R=k\}=\frac{\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)}{\sum_{j=1}^N\Gamma_j^{-1}\beta_j(1-L_\Psi\beta_j)}.\tag{3.7}

Formalization targets

Goal: Theorem 4 (pp. 21–22)

Fix $N\ge1$ , assume for $k=1,\dots,N$

\alpha_k\lambda_k\le\beta_k<\frac1{L_\Psi}\ \ (2.9),\qquad\frac{\alpha_1}{\lambda_1\Gamma_1}\ge\frac{\alpha_2}{\lambda_2\Gamma_2}\ge\cdots\ \ (2.10),

let $x^*$ be an optimal solution and $S=\sum_{k=1}^N\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)$ . Then

\mathbb E\big[\|\mathcal G(x^{md}_R,\nabla\Psi(x^{md}_R),\beta_R)\|^2\big]\le\frac8S\Big[\frac{\|x_0-x^*\|^2}{2\lambda_1}+\frac{L_f}{\Gamma_N}(\|x^*\|^2+2M^2)+\sigma^2\sum_{k=1}^N\frac{\beta_k(4+(1-L_\Psi\beta_k)^2)}{4\Gamma_k(1-L_\Psi\beta_k)m_k}\Big],\tag{3.30}

and, if $L_f=0$ ,

\mathbb E\big[\Phi(x^{ag}_R)-\Phi(x^*)\big]\le\frac1S\sum_{k=1}^N\beta_k(1-L_\Psi\beta_k)\Big(\frac{\|x_0-x^*\|^2}{2\lambda_1}+\sigma^2\sum_{j=1}^k\frac{\beta_j(4+(1-L_\Psi\beta_j)^2)}{4\Gamma_j(1-L_\Psi\beta_j)m_j}\Big).\tag{3.31}

The expectations are over $R$ and all samples. The goal keeps general step sizes and batch sizes; Corollaries 4 and 5 (explicit policies) are left for follow-up work.

Milestones

In the order of the proof: Lemma 4 ( $\mathcal G(x,\cdot,c)$ is 1-Lipschitz); the mini-batch variance bound (3.28) and its consequence (3.29) for the gradient mapping; Lemma 1, (2.16) and Lemma 5, the two-sided bound $-\frac{L_f}2\|y-x\|^2\le\Psi(y)-\Psi(x)-\langle\nabla\Psi(x),y-x\rangle\le\frac{L_\Psi}2\|y-x\|^2$ ; the three-point inequalities (3.32)–(3.33) and their combination (3.34); the descent bound (2.46) (already proved on the platform) and (2.47); the one-step and summed inequalities of p. 22; the iterate bound (2.52); the summed inequality at $x=x^*$ ; and the expected bound (3.35).

Significance

The result. Theorem 4 covers stochastic composite problems whether or not $\Psi$ is convex, with one step-size policy. Under Corollary 4's policy and batch sizes it gives a sample complexity for $\mathbb E\|\mathcal G\|^2\le\epsilon$ that improves the dependence on $L_h$ over mini-batch proximal stochastic gradient [Ghadimi, Lan & Zhang 2016], and when $L_f=0$ it recovers the optimal rate for convex stochastic composite optimization. Its proof is a template for later variance-controlled accelerated methods: a weighted Lyapunov argument in which nonconvexity enters only through $L_f$ and noise only through the martingale and variance terms.

Formalizing it. The result has been proved and refereed since 2016. As far as is known, no proof assistant has a formalization of it, and the platform has no accelerated stochastic method with a nonconvex guarantee. A complete development gives machine-checked versions of the mini-batch variance bound for martingale-difference noise, the Lipschitz property of the gradient mapping, the proximal three-point inequality on a convex domain, and the composite accelerated analysis with noise. Each of these can be reused in other stochastic proximal methods.

Difficulty

Copying the deterministic composite proof (Theorem 2) fails in two places. First, the deterministic step bounds $\min_k\|\mathcal G_k\|$ through the decrease $\|x^{ag}_k-x^{md}_k\|^2$ , but here $x^{ag}_k$ is computed from $\bar G_k$ , so this decrease measures the stochastic gradient mapping. Passing back to the exact one costs an extra variance term, which is why the constant is 8 rather than 2. Second, the noise $\bar\delta_k$ appears in two ways. The linear term $\langle\bar\delta_k,x^*-x_{k-1}\rangle$ vanishes only in expectation, and only because $x_{k-1}$ is fixed before the batch is drawn. The quadratic terms need the variance of an average of dependent samples, which is $\sigma^2/m_k$ only when the samples within a batch are conditionally unbiased given the earlier ones. A pathwise argument cannot remove either term, and an unconditional reading of Assumption 1 does not give the second.

Formalization scope

Space and smoothness. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) (the published GhadimiLan.RSG.E). Smoothness of $f$ and $h$ is the platform's ConvexOptAlg.SmoothGD.IsBetaSmooth. $\Psi$ , $\nabla\Psi$ and $L_\Psi$ are given with the identities $\Psi=f+h$ , $\nabla\Psi=\nabla f+\nabla h$ , $L_\Psi=L_f+L_h$ .
The convex term is its domain K with finite values X and ConvexOn ℝ K X; the prox map is a function P with the minimizer hypothesis IsProxMap K X P. A real-valued $\mathcal X$ on all of $\mathbb R^n$ is excluded: it makes Assumption 2 unsatisfiable and the goal vacuous. So is a free P with no minimizer property.
The noise. Oracle calls are numbered consecutively; iteration $k$ makes calls $S_{k-1}+1,\dots,S_{k-1}+m_k$ with $S_k=m_1+\dots+m_k$ , all at $x^{md}_k$ . Assumption 1 is the published GhadimiLan.RSG.AssumptionA1 along these query points: conditional unbiasedness given a filtration of the earlier calls, and conditional variance bound $\sigma^2$ . This conditional form is what the paper's proof uses, and the i.i.d. setting satisfies it. The oracle is jointly measurable. The variance bound (3.28) is a milestone and is never assumed.
The output index $R$ is measurable, takes values in $\{1,\dots,N\}$ with mass function (3.7), and is independent of the whole sample sequence. Algorithm 4 runs pathwise, for every $k$ , and is evaluated at $R$ , which is the paper's "run $N$ steps, output the $R$ -th iterate". Integrability of every expected quantity is part of each conclusion.
Excluded trivializations: batch size fixed to 1 (general $m_k$ is kept), $\sigma=0$ , a fixed $R$ , and (3.28) taken as a hypothesis.
Conventions. Indexing is 1-based, and $\Gamma_k=\prod_{i=2}^k(1-\alpha_i)$ , so $\Gamma_1=1$ . (2.9) and (2.10) are imposed for $k=1,\dots,N$ , and $\beta_k<1/L_\Psi$ is written $L_\Psi\beta_k<1$ . Two hypotheses are added: an optimal $x^*$ exists (the statement uses it), and $\|x_0\|\le M$ (used silently in (2.52) at $k=1$ ). The page prints $\Phi(x)$ on the left of (3.35) where $\Phi(x^*)$ is meant; the Lean states $\Phi(x^*)$ .

Contributions welcome: proofs of any milestone. Lemma 4, (3.28) and the three-point inequality are self-contained and reusable. Also welcome: the measurability of the iterates, and Corollaries 4–5 as follow-up statements.

Selected references

S. Ghadimi, G. Lan, Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming, arXiv:1310.3787v1, 2013; Math. Program. 156 (2016) 59–99. https://arxiv.org/abs/1310.3787v1 · https://doi.org/10.1007/s10107-015-0871-8
S. Ghadimi, G. Lan, H. Zhang, Mini-batch stochastic approximation methods for nonconvex stochastic composite optimization, Math. Program. 155 (2016) 267–305 (reference [13] of the paper: the mini-batch variance bound and Proposition 1, the Lipschitz property of $\mathcal G$ ). https://doi.org/10.1007/s10107-014-0846-1
S. Ghadimi, G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23 (2013) 2341–2368 (the randomized stochastic gradient method). https://doi.org/10.1137/120880811
S. Ghadimi, G. Lan, Optimal stochastic approximation algorithms for strongly convex stochastic composite optimization, I: a generic algorithmic framework, SIAM J. Optim. 22 (2012) 1469–1492 (reference [11] of the paper; its Lemma 2 is the three-point inequality). https://doi.org/10.1137/110848864
G. Lan, An optimal method for stochastic composite optimization, Math. Program. 133 (2012) 365–397. https://doi.org/10.1007/s10107-010-0434-y

22 thms2 active usersReviewed

Completed

Machine Learning Statistics·Captain: mikedeng1

A Modern Introduction to Online Learning XV: Online Learning Bounds Rademacher Complexity, Giving Massart's Lemma G∞√(2 ln d)/√TTextbook

Why random signs matter in learning

Learning theory asks whether a rule that fits an observed sample will also perform well on future observations. A class with many functions can fit accidental patterns in the sample, so its size and geometry affect the reliability of empirical risk estimates. Empirical Rademacher complexity measures this ability to fit noise: attach an independent random sign to each observed point, let the class choose its best function after seeing all signs, and average the resulting signed score. A smaller value supports tighter uniform generalization bounds. Orabona, §16.1, pp. 270–271

Online learning studies a different protocol. A learner chooses a prediction before each round's loss is revealed, and its regret compares its cumulative loss with that of a fixed competitor chosen in hindsight. Chapter 16 of Orabona's book connects these two quantities. The connection matters because an online algorithm's regret estimate can be used to control the statistical complexity of a class of predictors, even though the online game and the random-sign experiment are defined differently. Orabona, Theorem 16.4, p. 272

Setting and notation

Fix a horizon $T\ge1$ and vectors $z_1,\ldots,z_T\in\mathbb R^d$ . For each $t$ , let $\varepsilon_t$ be an independent Rademacher sign, equal to $1$ or $-1$ with probability one half each. Given a nonempty bounded set $V\subseteq\mathbb R^d$ , define its linear class by

H_{\mathrm{lin}}=\{z\mapsto\langle x,z\rangle:x\in V\}.

The empirical complexity on the fixed sample $S=(z_1,\ldots,z_T)$ is

\widehat{\mathfrak R}_S(H_{\mathrm{lin}}) =\frac1T\mathbb E_\varepsilon\left[ \sup_{x\in V}\sum_{t=1}^T\varepsilon_t\langle x,z_t\rangle \right].

This is a finite expectation over the $2^T$ possible sign assignments. The supremum is over the same comparison set $V$ for every assignment; the chosen $x$ may depend on the signs. The book's general Definition 16.1 allows an arbitrary class of real-valued functions, while this mission uses its linear specialization from the discussion immediately preceding Theorem 16.4. Orabona, Definition 16.1 and §16.1, pp. 270–272

For the final bound, $V$ is the probability simplex $\Delta^{d-1}=\{x\in\mathbb R^d:x_i\ge0,\ \sum_i x_i=1\}$ . The supremum of a linear score over this simplex is the maximum of its $d$ coordinate scores. Write $G_\infty$ for a common bound on the infinity norm of the sample vectors, so $|z_{t,i}|\le G_\infty$ for every round and coordinate. Orabona, Corollary 16.7, p. 273

Formalization targets

The central target is Corollary 16.7, called Massart's Lemma in the book:

\frac1T\mathbb E_\varepsilon\left[ \max_{1\le i\le d}\sum_{t=1}^T\varepsilon_tz_{t,i} \right] \le \frac{G_\infty\sqrt{2\ln d}}{\sqrt T}.

Its constant and dependence on $d$ and $T$ are part of the target. The result includes $d=1$ : in that case the expectation and the bound are both zero. Orabona, Corollary 16.7, p. 273

Two statements supply the chapter's route to this target. Theorem 16.4 says that if a nonanticipating online linear algorithm has worst-case regret at most $R(T)$ for all loss vectors in a symmetric set $Z$ , then $\widehat{\mathfrak R}_S(H_{\mathrm{lin}})\le R(T)/T$ for any sample in $Z$ . The Exponentiated Gradient regret bound of §6.6 gives, on the simplex, $\sum_t(\ell_t(x_t)-\ell_t(u))\le(\ln d)/\eta+(\eta/2)\sum_t\|g_t\|_\infty^2$ for every simplex competitor $u$ . The milestone list quotes both source statements. Orabona, Theorem 16.4, p. 272; §6.6, p. 81

What the result provides

The goal supplies a sample-dependent complexity bound using only a coordinate bound, the number of coordinates, and the sample size. Its square-root dependence on $\ln d$ explains why a simplex-indexed class can have much smaller complexity than a crude bound that scales directly with $d$ . In applications where a generalization estimate contains empirical Rademacher complexity, this result gives a concrete quantity to insert for a finite coordinate class. Orabona, §16.1, pp. 271–273

The mathematical statements are proved in the book. This mission asks for machine-checked proofs of the exact finite-sign formulation of the goal, the regret-to-complexity reduction, and the source's Exponentiated Gradient regret estimate. The local proposal currently contains statements with proof placeholders; it does not claim that these three items have already been proved in Lean. The resulting finite-sign and bounded-supremum definitions can also support other empirical-process arguments.

Where the work is difficult

The reduction has to respect the order of the online game. A bound for a learner allowed to inspect the current random sign would not imply the same complexity estimate: it could choose its round- $t$ point using information that a genuine online learner lacks. The algorithm therefore needs a precise causality condition, as well as a regret guarantee that holds for every admissible gradient sequence. Orabona, proof of Theorem 16.4, p. 272

The simplex result also depends on the exact regret coefficient. A generic $O(\sqrt T)$ estimate does not recover the displayed $\sqrt{2\ln d}$ constant. At the boundaries, real division and logarithms in Lean are total, so the statements must say when $T$ and $d$ are positive. The one-dimensional case is meaningful and must stay in the theorem.

Formalization scope

Vectors are functions Fin d → ℝ, representing $\mathbb R^d$ with its coordinate pairing. Samples, predictions and gradients use rounds $1,\ldots,T$ ; index zero is unused. The random-sign expectation is an exact average over Boolean assignments, with no measure-theoretic integrability convention. Both Rademacher averages require $T\ge1$ . The signed linear supremum is real-valued and receives evidence that $V$ is nonempty and bounded. Theorem 16.4 also records the book's closedness hypothesis.

Theorem 16.4 formalizes deterministic online algorithms. The source permits internal randomization as well; that extension requires an independent probability model for the algorithm's random choices. The Exponentiated Gradient item represents losses by real-valued functions and requires the subgradient inequality on the simplex, where the book evaluates them. Its run predicate requires $\eta>0$ and includes the uniform initial point and coordinate update of Algorithm 6.2. The goal itself has no algorithm hypothesis. Its infinity-norm assumption is expressed as coordinate absolute-value bounds.

The definitions exclude an empty comparison class or an unbounded real supremum being silently assigned a default Lean value. A complete development needs finite-sign averaging identities, properties of real suprema over bounded sets, simplex geometry, and the regret analysis of Exponentiated Gradient. Contributions to these reusable components, to the two milestones, and to the goal are in scope. The PAC-Bayes and time-uniform concentration parts of Chapter 16 are reserved for separate work because they need different probability and measure-theory objects.

Selected references

Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 16 and §6.6. arXiv

5 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning·Captain: mikedeng1

A Modern Introduction to Online Learning IV: Every Deterministic Online Linear Optimization Algorithm Has Regret at Least √2·LD√T/4Textbook

Why lower bounds matter

Online learning studies decisions made before their costs are known. An algorithm selects a point, observes a loss, and repeats. Regret compares its accumulated loss with the loss of one fixed point chosen after the sequence is known. Upper bounds show what a particular algorithm can guarantee; a lower bound shows what every algorithm must sometimes suffer. The distinction matters when deciding whether a rate such as $\sqrt T$ can be improved by changing the update rule. Chapter 5 of Orabona's Online Learning: A Modern Introduction Using Convex Optimization addresses this question for online linear optimization.

The chapter begins with bounded decision sets and then examines unbounded decision spaces. On bounded sets, the main result gives a quantitative obstruction with an explicit constant for every deterministic algorithm. The book compares that order with the regret upper bound for online subgradient descent: the square-root dependence on the number of rounds is optimal up to a constant factor under the same loss-scale and diameter parameters (Orabona, Theorem 5.1 and discussion, pp. 50–51). The same chapter shows a different phenomenon for unprojected subgradient descent with steps that decay too slowly: its regret can have order $T^{2-\alpha}$ for $0<\alpha<1$ (Orabona, Theorem 5.4, p. 52).

The online linear optimization setting

Let $V$ be a nonempty subset of Euclidean space $\mathbb R^d$ . On round $t$ , a deterministic online algorithm selects $x_t\in V$ using only the loss vectors from rounds $1,\ldots,t-1$ . It then observes $g_t\in\mathbb R^d$ and pays the linear loss $\langle g_t,x_t\rangle$ . The adversary may select any loss vectors satisfying $\|g_t\|_2\le L$ . This is the online linear optimization protocol used in the chapter; it also supplies lower bounds for online convex optimization because linear functions are convex (Orabona, §5.1, p. 50).

For a fixed competitor $u\in V$ , define

\operatorname{Regret}_T(u) =\sum_{t=1}^{T}\langle g_t,x_t\rangle -\sum_{t=1}^{T}\langle g_t,u\rangle.

The competitor is fixed across all $T$ rounds, although it may be selected after the loss sequence. The algorithm must make its own choices causally. These two quantifier positions are part of the mathematical claim. In particular, the hard sequence and competitor can depend on the algorithm, while the algorithm cannot use a future loss vector to choose its current prediction.

The bounded setting also uses the diameter $D=\max_{v,w\in V}\|v-w\|_2$ . The theorem assumes $V$ is closed, bounded, and convex, and that $D>0$ . In finite-dimensional Euclidean space, closedness and boundedness make $V$ compact, so this maximum exists. The positive diameter excludes a singleton feasible set, where the algorithm and the only comparator coincide. These hypotheses and the diameter convention are stated in Theorem 5.1, pp. 50–51.

Formalization targets

Worst-case regret on every bounded convex set

The goal is the chapter's Theorem 5.1. For every deterministic algorithm on such a set $V$ , every positive integer $T$ , and every nonnegative loss scale $L$ , there are bounded loss vectors and a competitor $u\in V$ for which

\operatorname{Regret}_T(u)\ge \frac{\sqrt2}{4}LD\sqrt T.

The book prints the exact factor $\sqrt2/4$ . The scale $L$ appears in its conclusion and in the restriction $\|g_t\|_2\le L$ but is not introduced before that sentence, so the formal statement quantifies it explicitly. At $L=0$ , the bound reads zero; for $L>0$ it gives a positive lower bound when $D>0$ and $T\ge1$ (Orabona, Theorem 5.1, pp. 50–51).

Supporting targets

Three milestones support and contextualize the goal. The first is the real-coefficient, $p=1$ lower-bound case of Khintchine's inequality, which controls the mean absolute value of a weighted sum of independent random signs (Orabona, Theorem A.14, p. 296). The second is the finite first-moment principle: a random sequence whose expected loss is at least $K$ has an outcome with loss at least $K$ (Orabona, §5.1, p. 50). The third records the lower-bound example for unprojected online subgradient descent with step size $t^{-\alpha}$ :

\operatorname{Regret}_T(0)\ge\frac12\phi(\alpha)T^{2-\alpha}, \qquad \phi(\alpha)=\frac1{2-\alpha}+\frac{(1/2)^{1-\alpha}-1}{1-\alpha}.

This last target uses the book's threshold $T\ge2/((1-\alpha)\phi(\alpha))$ and $0<\alpha<1$ (Orabona, Theorem 5.4, p. 52).

What the results establish

The goal rules out an $o(\sqrt T)$ worst-case regret guarantee for deterministic online linear optimization under a fixed positive loss scale and positive diameter. Because the result applies to every nonempty bounded closed convex $V$ with $D>0$ , it does not rely on a symmetric feasible set or a chosen cube. The explicit constant permits direct comparison with concrete algorithmic guarantees. Theorem 5.4 separately identifies a failure mode for unprojected online subgradient descent on an unbounded domain. Both conclusions are proved in the book; the remaining task here is to give their statements and supporting objects machine-checkable Lean meanings, then prove them in Lean. Hazan's related lower bound uses a hypercube instance and an unspecified absolute constant, so it is related context rather than the same formal target.

The mathematical difficulty

A hard sequence must be chosen after the algorithm is fixed and must respect the algorithm's information at every round. A sequence selected independently of that quantifier order need not be hard: an algorithm tailored to a known sequence can choose its best fixed point on every round. The bound must also hold on any convex body with positive diameter, including sets whose geometry is asymmetric. The proof therefore needs a way to extract a uniform numerical lower bound from only the diameter and the loss norm bound, while retaining the algorithm's causal dependence on earlier losses (Orabona, §5.1, pp. 50–51).

Formalization scope

Lean represents $\mathbb R^d$ by EuclideanSpace ℝ (Fin d), with vectors $g_t$ and decisions $x_t$ indexed from round one; index zero is unused. A deterministic algorithm is a function of a full loss sequence together with an explicit non-anticipation condition. Its outputs are required to lie in $V$ . Regret is a finite sum against one fixed competitor. The positive horizon, positive diameter, closedness, boundedness, convexity, and nonemptiness are explicit. This rules out trivializing the goal by using a singleton domain, an anticipatory algorithm, or a fixed hard sequence that precedes the algorithm's quantifier.

The Khintchine milestone uses the uniform distribution on a finite Boolean cube; each Boolean coordinate represents an independent Rademacher sign. Its expectation is an ordinary finite average and is always defined. The finite first-moment milestone uses arbitrary nonnegative weights summing to one. Theorem 5.4 uses linear losses of norm at most one in arbitrary positive Euclidean dimension, which are convex and $1$ -Lipschitz. Its auxiliary function $\phi$ is used only for $0<\alpha<1$ , where the printed formula's denominators are nonzero. The separate limiting claim about $\phi$ and the later coin-betting lower bounds are outside this mission's current milestones. Contributions establishing the Rademacher inequality, the geometric lower bound, the causal regret argument, and the unprojected descent example all fit this scope.

Selected references

Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. arXiv.
Elad Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016; arXiv:1909.05207. arXiv.

6 thms2 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming 3: The Randomized Stochastic AG Method Bounds E‖∇Ψ(x_R^md)‖² on Nonconvex Problems and Is Optimal on Convex OnesResearch Paper

Motivation

In stochastic programming the objective $\Psi(x)=\mathbb E_\xi[F(x,\xi)]$ is an expectation that cannot be evaluated, and an algorithm sees only noisy gradients $G(x,\xi)$ drawn from a stochastic first-order oracle. Stochastic gradient descent and its relatives are the standard methods. For convex $\Psi$ the optimal rate is known: Lan's accelerated stochastic approximation method (Lan, Math. Program. 2012) reaches an expected optimality gap of order $L\|x_0-x^*\|^2/N^2+\sigma\|x_0-x^*\|/\sqrt N$ after $N$ oracle calls. For smooth nonconvex $\Psi$ , Ghadimi and Lan's randomized stochastic gradient (RSG) method (arXiv:1309.5549, SIAM J. Optim. 2013) bounds the expected squared gradient norm at a randomly chosen iterate, but it is only nearly optimal when $\Psi$ happens to be convex.

Saeed Ghadimi and Guanghui Lan (arXiv:1310.3787v1, 2013; Mathematical Programming 156, 2016) combined the two lines: the randomized stochastic accelerated gradient (RSAG) method has a guarantee for nonconvex problems, and with suitable step sizes it attains the optimal rate on convex ones. This mission formalizes that result, Theorem 3 of the paper, together with the steps of its proof in §3.1.

Setting

Let $\Psi:\mathbb R^n\to\mathbb R$ be differentiable with Lipschitz gradient: $\|\nabla\Psi(y)-\nabla\Psi(x)\|\le L_\Psi\|y-x\|$ for all $x,y$ , with $L_\Psi>0$ . Gradients are available only through a stochastic oracle: at its $k$ -th call, with input $x$ , it returns $G(x,\xi_k)$ , where $\xi_1,\xi_2,\dots$ are random variables on a probability space and $G$ is jointly measurable.

Algorithm 3 (RSAG). The inputs are $x_0\in\mathbb R^n$ , step sizes $\alpha_1=1$ , $\alpha_k\in(0,1)$ for $k\ge2$ , $\beta_k>0$ , $\lambda_k>0$ , an iteration limit $N\ge1$ , and a probability mass function $p_1,\dots,p_N$ . A termination index $R$ with $\Pr\{R=k\}=p_k$ is drawn first, independently of the noise. With $x^{ag}_0=x_0$ , for $k=1,2,\dots$ ,

x^{md}_k=(1-\alpha_k)x^{ag}_{k-1}+\alpha_kx_{k-1},\qquad x_k=x_{k-1}-\lambda_kG(x^{md}_k,\xi_k),\qquad x^{ag}_k=x^{md}_k-\beta_kG(x^{md}_k,\xi_k),

and the method stops at $k=R$ and outputs $(x^{md}_R,x^{ag}_R)$ . The oracle error is $\delta_k=G(x^{md}_k,\xi_k)-\nabla\Psi(x^{md}_k)$ .

Assumption 1 asks that the oracle be unbiased, $\mathbb E[\delta_k]=0$ , with variance $\mathbb E\|\delta_k\|^2\le\sigma^2$ . The paper does not require the $\xi_k$ to be independent.

The weights are $\Gamma_1=1$ , $\Gamma_k=(1-\alpha_k)\Gamma_{k-1}$ , and for a horizon $N$

C_k=1-L_\Psi\lambda_k-\frac{L_\Psi(\lambda_k-\beta_k)^2}{2\alpha_k\Gamma_k\lambda_k}\Big(\sum_{\tau=k}^N\Gamma_\tau\Big).

Formalization targets

Goal: Theorem 3 (pp. 15–16)

Fix $N\ge1$ . The expectations are taken over $R$ and $\xi_{[N]}=(\xi_1,\dots,\xi_N)$ .

a) If $\Psi$ is bounded below with $\Psi^*=\inf\Psi$ , $C_k>0$ for $k\le N$ , and $p_k=\lambda_kC_k/\sum_{j}\lambda_jC_j$ (3.4), then

\mathbb E\|\nabla\Psi(x^{md}_R)\|^2\le\frac{1}{\sum_{k=1}^N\lambda_kC_k}\Big[\Psi(x_0)-\Psi^*+\frac{L_\Psi\sigma^2}{2}\sum_{k=1}^N\lambda_k^2\Big(1+\frac{(\lambda_k-\beta_k)^2}{\alpha_k\Gamma_k\lambda_k^2}\sum_{\tau=k}^N\Gamma_\tau\Big)\Big].\tag{3.5}

b) If $\Psi$ is convex with a minimizer $x^*$ , $\alpha_k/(\lambda_k\Gamma_k)$ is nonincreasing (2.10), $\alpha_k\lambda_k\le L_\Psi\beta_k^2$ and $\beta_k<1/L_\Psi$ (3.6), and $p_k\propto\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)$ (3.7), then

\mathbb E\|\nabla\Psi(x^{md}_R)\|^2\le\frac{(2\lambda_1)^{-1}\|x_0-x^*\|^2+L_\Psi\sigma^2\sum_{k}\Gamma_k^{-1}\beta_k^2}{\sum_{k}\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)},\tag{3.8}

\mathbb E[\Psi(x^{ag}_R)-\Psi(x^*)]\le\frac{\sum_{k}\beta_k(1-L_\Psi\beta_k)\big[(2\lambda_1)^{-1}\|x_0-x^*\|^2+L_\Psi\sigma^2\sum_{j\le k}\Gamma_j^{-1}\beta_j^2\big]}{\sum_{k}\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)}.\tag{3.9}

The goal keeps every printed constant and leaves the step sizes free. Corollary 3 specializes them; it is not part of this mission.

Milestones

Part a): the quadratic bound (2.1) (already proved on the platform); a pathwise one-step inequality for $\Psi(x_k)$ (p. 16); a stochastic version of (2.17) bounding $\|x^{ag}_{k-1}-x_{k-1}\|^2$ ; the summed inequality with martingale terms $b_k$ (pp. 16–17); its expectation (p. 17); the identity expressing $\mathbb E\|\nabla\Psi(x^{md}_R)\|^2$ as a $p$ -weighted average (p. 17); Theorem 3 a). Part b): Lemma 1 (p. 4); the convexity bound (2.21); (3.10) with a sign corrected; the stochastic version of (2.22); (3.11); its two consequences at $x=x^*$ (p. 18); the weighting identity for $\Psi(x^{ag}_R)$ (p. 18); Theorem 3 b).

Significance

The result. Theorem 3 gives one stochastic first-order method with two guarantees. On a nonconvex problem it finds an approximate stationary point with an explicit bound on $\mathbb E\|\nabla\Psi\|^2$ . On a convex problem its optimality gap matches the lower bound for stochastic convex optimization, which the RSG method does not. The method does not need to know which case it is in; only the step-size policy changes. Later work on accelerated and variance-reduced methods for nonconvex stochastic problems builds on the same analysis, and Theorem 4 of the paper extends it to composite problems with mini-batches.

Formalizing it. The result is proved in the paper and, as far as we know, has not been machine-checked. A formal proof would check the bookkeeping that a reader usually takes on trust: the nested sums in $C_k$ and $b_k$ , the conditional-expectation arguments that make $\{b_k\}$ a martingale difference sequence, and the passage from fixed horizons to the random output $R$ . The printed proof has small errors (see Formalization scope), so the formal statements record the corrected forms.

Difficulty

The deterministic analysis of the AG method (Theorem 1) bounds $\Psi(x_N)$ along a single trajectory. In the stochastic case the same chain produces cross terms $\langle\nabla\Psi(x_{k-1}),\delta_k\rangle$ and $\langle\nabla\Psi(x^{md}_k),\delta_k\rangle$ . These cross terms do not vanish pathwise, and the variance terms come with coefficients involving $\sum_{\tau\ge k}\Gamma_\tau$ that grow backwards in time. The obvious argument would take expectations termwise. It fails unless one shows that each cross-term coefficient is measurable with respect to the past, so that its product with $\delta_k$ has zero mean under conditional unbiasedness. This also requires square-integrability of every iterate, which the hypotheses do not state and which has to be established by induction. A second difficulty is the random output: the bound is on $\mathbb E\|\nabla\Psi(x^{md}_R)\|^2$ , an integral over $R$ and the noise jointly, so the independence of $R$ from the noise has to be used explicitly.

Formalization scope

Space and smoothness. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) (the published GhadimiLan.RSG.E n). $\Psi\in\mathcal C^{1,1}_{L_\Psi}$ is the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth Ψ g LΨ, with $g=\nabla\Psi$ , and $L_\Psi>0$ .
The run. It is defined along each noise realization by recursion and evaluated pointwise on $\Omega$ . Indices are 1-based. $\Gamma_k=\prod_{i=2}^k(1-\alpha_i)$ , so $\Gamma_1=1$ . The run is recorded for every $k$ ; the paper itself notes that stopping at $R$ is the same as running $N$ steps and outputting the $R$ -th pair.
Assumption 1 is the published GhadimiLan.RSG.AssumptionA1 applied to the middle points: for a filtration to which the noise is adapted, $\mathbb E[G(x^{md}_k,\xi_k)\mid\mathcal F_{k-1}]=\nabla\Psi(x^{md}_k)$ a.s. and $\mathbb E\|\delta_k\|^2\le\sigma^2$ . This conditional form is what the paper's martingale-difference step uses. It holds when the $\xi_k$ are independent, and it allows dependent noise, as the paper does.
The termination index. $R$ is measurable, takes values in $\{1,\dots,N\}$ , has the mass function (3.4) or (3.7), and is independent of the whole noise sequence. Each part of the goal quantifies over its own $R$ .
Conditions on step sizes. (2.7), (2.10) and (3.6) are required for $k=1,\dots,N$ .
Expectations. Every expectation is a Lebesgue integral, and its integrability is part of the conclusion, since Lean assigns $0$ to the integral of a non-integrable function.
Corrected typos. On p. 16, $\delta_k$ is read as $\delta_\tau$ in the stochastic (2.17), and the middle line of the summed chain has a wrong sign. In (3.10) the term $\beta_k\langle\nabla\Psi(x^{md}_k),\delta_k\rangle$ should carry a minus sign, which this mission states as "(3.10), sign corrected". On p. 18, $\|x_0-x\|$ means $\|x_0-x^*\|$ . None of these affects the theorem.

The following versions would make the goal trivial and are excluded: a deterministic oracle ( $\sigma=0$ hard-wired), $R$ fixed to $N$ , an oracle $G$ not tied to $\nabla\Psi$ , and an unconditional unbiasedness hypothesis too weak to support the martingale step.

A complete development needs conditional expectations of vector-valued random variables, square-integrability of the iterates, and the independence calculus for the random index. These parts are reusable for the companion RSG and mini-batch RSAG missions. Contributions are welcome on any milestone. The pathwise milestones (one-step bound, (2.17), (2.21), (2.22), (3.10)) need no probability theory.

Selected references

S. Ghadimi, G. Lan, Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming, arXiv:1310.3787v1, 2013; Math. Program. 156 (2016) 59–99. https://arxiv.org/abs/1310.3787
S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM J. Optim. 23 (2013) 2341–2368. https://arxiv.org/abs/1309.5549
G. Lan, An optimal method for stochastic composite optimization, Math. Program. 133 (2012) 365–397. https://doi.org/10.1007/s10107-010-0434-y
Y. Nesterov, A method for unconstrained convex minimization problem with the rate of convergence O(1/k²), Doklady AN SSSR 269 (1983) 543–547.

21 thms2 active usersReviewed

Completed

Combinatorics Stochastic Systems·Captain: mikedeng1

Separation of Time-Scales and Model Reduction for Stochastic Reaction Networks 2: Positive Combinations Preserve the Balance Condition When Production and Consumption Sets Are DisjointResearch Paper

Multiscale reaction networks and the balance condition

Stochastic models of chemical reaction networks in cell biology routinely combine species present in a handful of copies with species present in thousands, and rate constants that differ by orders of magnitude. Simulating such a system exactly is expensive, and model reduction replaces it with a lower-dimensional limit. A systematic approach, developed by Ball, Kurtz, Popovic and Rempala (2006) and by Kang and Kurtz (arXiv:1011.1672), normalizes species numbers and rate constants by powers of a large parameter $N$ and derives limits as $N\to\infty$ on several time-scales.

For such limits to exist, the normalized species numbers must stay of order one. For a single species this is the species balance condition: either the fastest reaction producing it is as fast as the fastest reaction consuming it, or the time-scale considered is short enough that the imbalance does not show. Kang and Kurtz observed (arXiv:1011.1672v1, §3.2, p. 9) that this is not enough: a collection of species can be produced collectively at a different order of magnitude from the rate at which it is consumed, even when every member is balanced. They therefore impose a balance condition on every nonnegative linear combination of species, which is infinitely many conditions. Section 3.4 of their paper proves combinatorial lemmas that reduce the work of checking them. This mission formalizes the lemmas on positive combinations of two weight vectors.

Setting

A reaction network has $s_0$ species $S_1,\dots,S_{s_0}$ and $r_0$ reactions. Reaction $k$ consumes $\nu_{ik}\in\mathbb N$ molecules of $S_i$ and produces $\nu'_{ik}\in\mathbb N$ ; its net change is the vector $\zeta_k=\nu'_k-\nu_k$ . Each species carries a scaling exponent $\alpha_i\ge0$ and each reaction an exponent $\beta_k\in\mathbb R$ ; put

\rho_k=\beta_k+\nu_k\cdot\alpha=\beta_k+\sum_i\nu_{ik}\alpha_i,

the order of magnitude (as a power of $N$ ) of the rate of reaction $k$ .

A weight vector $\theta\in[0,\infty)^{s_0}$ describes the linear combination $\theta\cdot X=\sum_i\theta_iX_i$ . Its sign sets (Definition 3.1) are

\Gamma^+_\theta=\{k:\theta\cdot\zeta_k>0\},\qquad\Gamma^-_\theta=\{k:\theta\cdot\zeta_k<0\},

the reactions that increase and decrease $\theta\cdot X$ . Maxima $\max_{k\in S}\rho_k$ are taken in $\mathbb R\cup\{-\infty\}$ , with $\max_{k\in\emptyset}\rho_k=-\infty$ , and $a\vee b$ is the maximum.

Fix a time-scale exponent $\gamma\in\mathbb R$ . Condition 3.2 holds for $\theta$ if either the balance equation

\max_{k\in\Gamma^-_\theta}\rho_k=\max_{k\in\Gamma^+_\theta}\rho_k\tag{3.7}

or the time-scale constraint

\gamma\le\gamma_\theta\equiv\max_{i:\theta_i>0}\alpha_i-\max_{k\in\Gamma^+_\theta\cup\Gamma^-_\theta}\rho_k\tag{3.8}

holds, with $\gamma_\theta=+\infty$ when $\Gamma^+_\theta\cup\Gamma^-_\theta=\emptyset$ .

Formalization targets

Goal: Lemma 3.8 (p. 18)

Let $\theta^1,\theta^2\in[0,\infty)^{s_0}$ , $c_1,c_2>0$ , and suppose

\Gamma^+_{\theta^1}\cap\Gamma^-_{\theta^2}=\emptyset\quad\text{or}\quad\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2}=\emptyset.

Then (i) if Condition 3.2 holds for $\theta^1$ and $\theta^2$ , it holds for $c_1\theta^1+c_2\theta^2$ ; and (ii) if (3.7) holds for $\theta^1$ and $\theta^2$ , it holds for $c_1\theta^1+c_2\theta^2$ .

Milestones, in the order the paper uses them

(3.16)–(3.17) (p. 15): $\Gamma^\pm_{c_1\theta^1+c_2\theta^2}\subseteq\Gamma^\pm_{\theta^1}\cup\Gamma^\pm_{\theta^2}$ , hence

\max_{k\in\Gamma^\pm_{c_1\theta^1+c_2\theta^2}}\rho_k\le\max_{k\in\Gamma^\pm_{\theta^1}}\rho_k\vee\max_{k\in\Gamma^\pm_{\theta^2}}\rho_k.

Lemma 3.5 (p. 17): (3.8) for $\theta^1,\dots,\theta^m$ implies (3.8) for $\sum_jc_j\theta^j$ , $c_j>0$ .
Lemma 3.6 (p. 17): if $\max_{\Gamma^-_{\theta^1}}\rho=\max_{\Gamma^+_{\theta^1}}\rho>\max_{\Gamma^+_{\theta^2}\cup\Gamma^-_{\theta^2}}\rho$ , then (3.7) holds for $c_1\theta^1+c_2\theta^2$ .
Lemma 3.7 (p. 18): (3.7) for $\theta^1$ and (3.8) for $\theta^2$ give Condition 3.2 for $c_1\theta^1+c_2\theta^2$ .
(3.35)–(3.36) (p. 19): if $\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2}=\emptyset$ , then

\max_{\Gamma^-_{\theta^1}}\rho\le\max_{\Gamma^-_{c_1\theta^1+c_2\theta^2}}\rho\le\max_{\Gamma^-_{\theta^1}}\rho\vee\max_{\Gamma^-_{\theta^2}}\rho,\quad\max_{\Gamma^+_{\theta^2}}\rho\le\max_{\Gamma^+_{c_1\theta^1+c_2\theta^2}}\rho\le\max_{\Gamma^+_{\theta^1}}\rho\vee\max_{\Gamma^+_{\theta^2}}\rho.

Companion results

Remark 3.9 (p. 18): if no reaction that consumes a species in the support of $\theta^1$ produces a species in the support of $\theta^2$ , then $\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2}=\emptyset$ .
Lemma 3.10 (p. 19): if (3.7) holds for $\theta^1$ , $\theta^2$ and for $\theta^1-\frac{\theta^1\cdot\zeta_k}{\theta^2\cdot\zeta_k}\theta^2$ for every $k\in(\Gamma^+_{\theta^1}\cap\Gamma^-_{\theta^2})\cup(\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2})$ , then (3.7) holds for $c_1\theta^1+c_2\theta^2$ for all $c_1,c_2>0$ .

Significance

Condition 3.2 must hold for every $\theta\in[0,\infty)^{s_0}$ before the limit theorems of the paper's Sections 4–5 apply. Lemma 3.8, together with the decomposition over strongly connected components (Lemma 3.4, the subject of the first mission of this series), turns that infinite family into finitely many checks for many networks: once the condition is known for some generating vectors, it propagates to their positive combinations whenever the sign sets do not conflict. Remark 3.9 gives a condition on the stoichiometry alone under which they do not conflict, and Lemma 3.10 reduces checking balance along a ray of combinations to finitely many breakpoints.

The results are proved in the paper (arXiv:1011.1672v1, pp. 15–19; published in Ann. Appl. Probab. 23(2), 2013), but none is formalized anywhere to our knowledge. The printed proof of Lemma 3.10 is a sketch that treats only the first breakpoint of the ray $\theta^1+c\theta^2$ ; a machine-checked proof would settle it in full. The definitions of the sign sets, the balance equation and the time-scale constraint are reusable for the other missions of this series.

Difficulty

The proofs are elementary, and the work lies in the bookkeeping. Every statement mixes three conventions: maxima over sets that can be empty (value $-\infty$ ), a time-scale constant that can be $+\infty$ , and strict versus weak sign conditions on $\theta\cdot\zeta_k$ . Lemma 3.8 is a case analysis on which disjunct of Condition 3.2 holds for each of $\theta^1$ and $\theta^2$ ; the obvious idea of applying (3.16)–(3.17) alone fails in the case where both vectors are balanced at the same level ((3.34) in the paper), where only upper bounds are available. That case needs the disjointness hypothesis to get the matching lower bounds (3.35)–(3.36). Lemma 3.10 needs an argument along the whole ray $\theta^1+c\theta^2$ , $c>0$ : the sign pattern of $(\theta^1+c\theta^2)\cdot\zeta_k$ changes at finitely many values of $c$ , and balance has to be tracked through each change, not only the first.

Formalization scope

Species are Fin s and reactions Fin r (0-based indices; $s_0,r_0$ are arbitrary naturals). ν k i is $\nu_{ik}$ ; $\zeta_{ik}$ , $\rho_k$ and $\theta\cdot\zeta_k$ are real numbers, and $\rho$ is defined from $\nu,\alpha,\beta$ rather than taken as a free parameter. A combination $c_1\theta^1+c_2\theta^2$ is c₁ • θ₁ + c₂ • θ₂ on Fin s → ℝ. Maxima are Finset.sup into WithBot ℝ, so the maximum over the empty set is $\bot=-\infty$ and $\vee$ is ⊔. $\gamma_\theta$ is an EReal defined by cases: $+\infty$ if $\Gamma^+_\theta\cup\Gamma^-_\theta=\emptyset$ , otherwise the difference of the two maxima computed in $\mathbb R$ (or $-\infty$ if no $\theta_i$ is positive). Every statement carries the paper's standing assumptions $\alpha\ge0$ , $\theta^1,\theta^2\ge0$ and $c_1,c_2>0$ .

These choices rule out the trivializing encodings: a real-valued maximum with a default value of $0$ on the empty set would make the balance equation hold spuriously; a subtraction in EReal would turn $-\infty-(-\infty)$ into $-\infty$ ; and dropping $\theta\ge0$ or $c_1,c_2>0$ would change which reactions lie in the sign sets of the combination. In Lemma 3.8 the disjointness of the sign sets is a disjunction, as printed, and the second paragraph's "Condition 3.7" is read as the balance equation (3.7).

The development needs only finite sets, finite sums and order on $\mathbb R\cup\{\pm\infty\}$ ; no probability theory is involved. Lemmas about Finset.sup into WithBot ℝ over unions and subsets are reusable. Proofs of the milestones, of the goal, and of Lemma 3.10 are all welcome.

Selected references

H.-W. Kang and T. G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, arXiv:1011.1672v1, 2010; Ann. Appl. Probab. 23(2), 2013. https://arxiv.org/abs/1011.1672, https://doi.org/10.1214/12-AAP841
K. Ball, T. G. Kurtz, L. Popovic and G. Rempala, Asymptotic analysis of multiscale approximations to reaction networks, Ann. Appl. Probab. 16(4):1925–1961, 2006. https://doi.org/10.1214/105051606000000420
Y. Cao, D. T. Gillespie and L. R. Petzold, The slow-scale stochastic simulation algorithm, J. Chem. Phys. 122(1):014116, 2005. https://doi.org/10.1063/1.1824902

8 thms2 active usersReviewed

Completed

Combinatorics Stochastic Systems·Captain: mikedeng1

Separation of Time-Scales and Model Reduction for Stochastic Reaction Networks 3: The Second Time-Scale r₂ Is Strictly Slower than the First Time-Scale r₁Research Paper

Motivation

Chemical reaction networks can contain reactions whose rates differ by powers of a large scaling parameter. A species may then change on one time scale while other combinations of species remain nearly fixed until a later one. This matters when replacing a detailed network by a smaller model: the quantities retained at the first scale need not be the quantities that evolve at the next. Kang and Kurtz formulate this separation using the reaction exponents and the changes made by each reaction, before analyzing the stochastic process limits in their paper. This mission concerns the algebraic separation of the first two natural time scales in Lemma 4.4, rather than a convergence theorem for the stochastic processes.

Setting

A reaction network has a finite set of species and a finite set of indexed reactions. For reaction $k$ , the nonnegative integer $\nu_{ik}$ is the number of molecules of species $i$ consumed, and $\nu'_{ik}$ is the number produced. Its net change is $\zeta_{ik}=\nu'_{ik}-\nu_{ik}$ . The two reaction vectors may coincide; allowing such a reaction does not make it change any species. The paper introduces a nonnegative abundance exponent $\alpha_i$ for each species and a real rate exponent $\beta_k$ for each reaction. The exponent relevant to a reaction under that abundance scaling is $\rho_k=\beta_k+\sum_i\nu_{ik}\alpha_i$ §2 and §3.2.

A nonnegative vector $\theta$ assigns weights to the species. The weighted quantity changes by $\theta\cdot\zeta_k$ when reaction $k$ occurs. Define $\Gamma^+_\theta$ and $\Gamma^-_\theta$ as the reactions for which this dot product is respectively positive and negative. Let $\alpha_\theta$ be the greatest $\alpha_i$ among indices with $\theta_i>0$ . The natural time scale of this combination is

\gamma_\theta=\alpha_\theta-\max_{k\in\Gamma^+_\theta\cup\Gamma^-_\theta}\rho_k.

An empty maximum is $-\infty$ , so a combination unaffected by every reaction has $\gamma_\theta=+\infty$ . In particular $\gamma_0=+\infty$ ; the unused value of $\alpha_0$ has no effect. A coordinate vector gives a single species' scale $\gamma_i$ . The first time scale is $r_1=\min_i\gamma_i$ (3.5), Definition 3.1, and (4.1).

At scale $r_1$ , define $\Gamma_i^{r_1}=\{k:r_1+\rho_k=\alpha_i\}$ . It contains every reaction meeting that exponent equation, including one that leaves species $i$ unchanged. Let $\mathbb S_1$ consist of the coordinate vectors $e_i$ for which $\Gamma_i^{r_1}$ is nonempty, and let $\Pi_1$ be the coordinate projection onto their span. The nonnegative combinations whose projection is unchanged by each such reaction form

\mathbb K_2=\left\{\theta\geq0:\theta\cdot\Pi_1\zeta_k=0\quad \text{for every }k\in\bigcup_i\Gamma_i^{r_1}\right\}.

The second time scale is $r_2=\inf_{\theta\in\mathbb K_2}\gamma_\theta$ . This is the paper's minimum over $\mathbb K_2$ : despite the infinite set of eligible vectors, every finite value of $\gamma_\theta$ is a difference of one of finitely many $\alpha_i$ and one of finitely many $\rho_k$ §4, p. 21.

Formalization targets

The first milestone compares each weighted combination with the species in its positive support and identifies $r_1$ among all nonnegative combinations:

\gamma_\theta\geq\min_{i:\theta_i>0}\gamma_i, \qquad r_1=\inf_{\eta\geq0}\gamma_\eta.

The second milestone is the first sentence of Lemma 4.4. For $\theta\in\mathbb K_2$ and $l\in\Gamma_i^{r_1}$ , a nonzero $\theta\cdot\zeta_l$ implies $\alpha_\theta>\alpha_i$ . The goal is the lemma's strict separation:

r_2>r_1.

These statements and their source order are on p. 21 of the preprint. The goal allows $r_2=+\infty$ , which represents the absence of a later changing combination in $\mathbb K_2$ .

Significance

The strict inequality says that the quantities eligible for the second scale cannot move at the first scale. It makes the two-scale terminology precise for this exponent model and separates an algebraic fact about reaction vectors from the later analysis of stochastic limits. A reduced process on the second scale requires additional stability and convergence conditions; Lemma 4.4 alone supplies neither. The paper explicitly discusses that limitation immediately after its proof on p. 22.

This mission packages the reaction-exponent definitions and the scale-separation statements as Lean declarations. Their proof obligations remain open in the proposal. Reusable parts include the finite reaction indexing, real-valued net-change vectors, the explicit convention for empty maxima, and the extended-real scale definitions. A complete development may also establish supporting facts about the finite range of $\gamma_\theta$ and the coordinate projection; such facts are useful beyond this lemma. The paper's stochastic limit theorems are outside this mission's scope.

Difficulty

Checking separately that every $\theta\in\mathbb K_2$ has $\gamma_\theta>r_1$ does not establish $r_2>r_1$ : an infimum of strictly larger values can still equal $r_1$ . The statement needs the finite-range property of the scale function, together with the interaction between the fast-reaction equation defining $\Gamma_i^{r_1}$ and the projected orthogonality condition defining $\mathbb K_2$ . Empty reaction sets and zero weighted combinations also require explicit extended-real values. Replacing their scales with a default real number would change the claim Lemma 4.4, pp. 21–22.

Formalization scope

Species and reactions are Fin s and Fin r; their indices begin at zero, while the paper numbers them from one. The stoichiometric arrays have natural-number entries, $\zeta$ and $\rho$ are real-valued, and theorems carry $\alpha_i\geq0$ . The sets of changing reactions and the positive support of $\theta$ are finite sets. Empty maxima use a bottom-extended real, while $\gamma_i$ , $\gamma_\theta$ , $r_1$ , and $r_2$ live in extended reals. Finite scale differences are calculated in the reals before conversion. The formulas define $\rho$ from $\nu,\alpha,\beta$ and construct $\mathbb K_2$ from $r_1$ ; neither is a free input. No extra positivity condition is imposed on $\beta$ .

The coordinate projection $\Pi_1$ retains the indices belonging to $\mathbb S_1$ . The infimum for $r_2$ ranges over all of $\mathbb K_2$ , including the zero vector and combinations unchanged by every reaction. The goal assumes that some reaction changes a species. Without this necessary nondegeneracy condition, $r_1=r_2=+\infty$ and the strict conclusion is false. It adds no condition on the initial stochastic state: the assumption at the start of §4 belongs to its process-limit statements. The paper develops at-most-binary mass-action rates in §2, but Lemma 4.4 uses only the indexed reaction vectors and their exponents; the Lean declarations expose exactly those algebraic data.

Selected references

H.-W. Kang and T. G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, arXiv:1011.1672v1, 2010; published in Annals of Applied Probability 23(2), 2013. Preprint, DOI.

5 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Stochastic Systems·Captain: mikedeng1

Separation of Time-Scales and Model Reduction for Stochastic Reaction Networks 1: The Balance Condition for Linear Combinations of Species Decomposes over Strongly Connected ComponentsResearch Paper

Why reaction-network balance matters

A stochastic reaction network tracks the counts of chemical species as reactions occur. Different species and reaction rates may grow at different powers of a large system-size parameter. Kang and Kurtz's model-reduction paper uses these powers to identify candidate time scales and combinations of species that can remain bounded. Before a reduced model can be justified, the dominant reactions that increase a combination must be compared with those that decrease it. Condition 3.2 makes that comparison.

Checking the condition for every nonnegative linear combination is a large task even for a finite network: the weights range over a continuum, and changing a weight can change which reactions increase or decrease the combination. The paper's Lemma 3.4 relates this task to the directed graph of species. It says that combinations supported on different strongly connected components can be checked component by component. This mission formalizes that result and the claims in its proof that carry the reduction.

The network and its graph

There are finitely many species $S_i$ and finitely many indexed reactions $k$ . Reaction $k$ consumes $\nu_{ik}$ molecules of species $i$ and produces $\nu'_{ik}$ molecules of that species. The stoichiometric change is $\zeta_{ik}=\nu'_{ik}-\nu_{ik}$ . Species $i$ has a nonnegative scaling exponent $\alpha_i$ , and reaction $k$ has a real exponent $\beta_k$ . The effective reaction exponent is $\rho_k=\beta_k+\sum_i\nu_{ik}\alpha_i$ .

For a vector of nonnegative weights $\theta$ , the scalar $\theta\cdot\zeta_k$ is the change in its linear combination when reaction $k$ occurs. Write $\Gamma^+_\theta$ for reactions with positive change and $\Gamma^-_\theta$ for reactions with negative change. The balance equation equates the largest $\rho_k$ on these two sets. If that equation fails, the time-scale inequality permits a chosen exponent $\gamma$ only when it is no larger than $\gamma_\theta$ , the largest $\alpha_i$ on the support of $\theta$ minus the largest $\rho_k$ on $\Gamma^+_\theta\cup\Gamma^-_\theta$ . Condition 3.2 is the disjunction of these two alternatives.

The species graph has an edge $S_i\to S_j$ when one reaction consumes $S_i$ and produces $S_j$ . Its strongly connected components are the maximal sets of species that can reach one another by directed paths. A single species is a component when it shares no larger mutual-reachability class. A nonnegative vector supported in one such component is a component-level test vector.

Formalization targets

The goal is Lemma 3.4, p. 15. Suppose $\theta=\sum_{j=1}^m\theta^j$ , each $\theta^j$ is nonnegative and supported within one maximal strongly connected component, and distinct pieces belong to distinct components. For fixed $\gamma$ , the lemma asserts all three implications:

\begin{aligned} \bigl(\forall j,\;\mathrm{Cond}_{3.2}(\gamma,\theta^j)\bigr)&\Longrightarrow\mathrm{Cond}_{3.2}(\gamma,\theta),\\ \bigl(\forall j,\;\mathrm{Balance}(\theta^j)\bigr)&\Longrightarrow\mathrm{Balance}(\theta),\\ \bigl(\forall j,\;\gamma\le\gamma_{\theta^j}\bigr)&\Longrightarrow\gamma\le\gamma_\theta. \end{aligned}

The companion consequence on the same page quantifies over all nonnegative vectors: if any one of these properties holds for every vector supported in a strongly connected subgraph, then it holds for every vector. The milestones mirror the paper's proof: a chain of component pieces cannot revisit a piece; under Condition 3.2 the maximal positive exponent either satisfies the time-scale bound or is bounded by the maximal negative exponent; and the two uniform cases yield their respective alternatives.

What the result establishes

Lemma 3.4 replaces a global family of tests with tests inside individual strongly connected components. In the paper this narrows the balance checks needed before the authors study separated time scales and reduced stochastic models. The uniform balance and uniform time-scale clauses matter separately: the first preserves equality of dominant positive and negative exponents, while the second preserves the same admissible $\gamma$ across a sum of pieces. The general Condition 3.2 clause allows different pieces to satisfy different alternatives.

The mathematical result was proved in the 2010 arXiv preprint and published in 2013; it is not an open conjecture. This proposal supplies Lean statements and a reusable finite reaction-network vocabulary, with proofs left for solvers. The local sanity file checks the empty-maximum and zero-vector behavior without using sorry. The draft theorem files compile as statements, but their six proofs are not yet machine checked.

Where the reasoning is difficult

The obvious inequality for a sum says that a reaction increasing $\theta$ increases at least one piece. It does not say that the piece's dominant increasing reaction also increases the sum: contributions from other pieces can cancel it. Consequently, taking a maximum separately on each piece does not directly give the balance equation for the sum. The graph restriction is decisive because a sequence of compensating reactions would otherwise be able to cycle among pieces. The milestones isolate that no-repetition property and the two inequalities the paper obtains from it.

Formalization scope

Species, reactions, and pieces are represented by Fin s, Fin r, and Fin m; these are zero-based versions of the paper's one-based indices. The stoichiometric coefficients are natural numbers, the changes $\zeta_k$ and all scaling exponents are real, and $\alpha_i\ge0$ . Following the standing restriction on p. 5, each reaction consumes at most two molecules. The paper's $\rho_k$ is computed from $\beta_k$ , $\nu_k$ , and $\alpha$ , not supplied independently.

For a reaction set $A$ , $\max_{k\in A}\rho_k$ uses WithBot ℝ, so the maximum of an empty set is $-\infty$ , as the paper explicitly uses on p. 17. The support maximum in $\gamma_\theta$ is an ordinary real maximum when relevant. The value $\gamma_\theta$ is represented in EReal: when $\Gamma^+_\theta\cup\Gamma^-_\theta$ is empty, it is $+\infty$ and the time-scale inequality holds for every real $\gamma$ . Subtraction is performed in the reals before conversion to EReal. Thus zero vectors do not acquire a spurious bound from a default-valued maximum or extended-real subtraction.

An edge uses positive consumption and positive production in the same indexed reaction, matching the wording on pp. 4 and 15. Mutual reachability defines a component. Each piece is required to lie in one component, and different pieces in different components. These conditions prevent splitting a single component into separately balanced pieces, which would make the goal false. An empty family of pieces is permitted; its sum is zero. The definition file is useful for the other balance results in the paper, while the graph and component lemmas can support later work on reaction-network decomposition.

Selected references

Hye-Won Kang and Thomas G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, arXiv:1011.1672v1, 2010, especially §2 and §§3.2–3.4, pp. 4–17. Preprint.
Hye-Won Kang and Thomas G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, Annals of Applied Probability 23(2), 2013. DOI. The numbered statements in this mission follow the pinned 2010 preprint.

6 thms2 active usersReviewed

Machine Learning Optimization·Captain: mikedeng1

Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition IV: Stochastic Gradient Rates LC²/(2kμ²) and (1 − 2μα)^k [f(x_0) − f*] + LC²α/(4μ)Research Paper

Motivation

Stochastic gradient (SG) methods are the default algorithms for training machine-learning models: when an objective is an average over a very large number of training examples, computing its full gradient even a few times is infeasible, while the gradient of a single randomly chosen example is cheap. The classical convergence theory of SG rates its expected suboptimality under strong convexity — the $O(1/k)$ rate of Nemirovski, Juditsky, Lan and Shapiro (2009) — yet common models such as least squares with a rank-deficient design and logistic regression are convex but not strongly convex.

Karimi, Nutini and Schmidt (2016) observed that the much older Polyak–Łojasiewicz (PL) inequality of Polyak (1963) is enough to recover linear rates for gradient descent and its variants without any convexity. Their Theorem 4 transfers this observation to SG: under PL alone, SG with a decreasing step attains the $O(1/k)$ rate known from the strongly convex case, and SG with a constant step converges linearly to a neighbourhood of the optimum whose size is proportional to the step. This mission formalizes that theorem.

Setting

Let $d\ge0$ and let $\mathbb R^d$ carry the Euclidean norm $\|\cdot\|$ . An index $i$ ranges over a measurable space $I$ with a probability measure $\nu$ , and each index has a differentiable component function $f_i:\mathbb R^d\to\mathbb R$ . The stochastic optimization problem (7) is to minimize

f(x) = \mathbb E_{i\sim\nu}[f_i(x)],

of which the finite sum $f = \frac1n\sum_{i=1}^n f_i$ (8) is the case of the uniform distribution on $n$ indices. The component gradients are unbiased: $\mathbb E_{i\sim\nu}[\nabla f_i(x)] = \nabla f(x)$ for every $x$ .

The SG method (9) starts from a point $x_0$ and, given step sizes $\alpha_k>0$ and indices $i_0,i_1,\dots$ drawn independently from $\nu$ , iterates

x_{k+1} = x_k - \alpha_k\nabla f_{i_k}(x_k).

The iterate $x_k$ is a random vector, a function of $i_0,\dots,i_{k-1}$ .

The standing assumptions on $f$ (§2 of the paper) are:

$\nabla f$ is $L$ -Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$ , with $L>0$ ;
the solution set is non-empty: some $x^*$ minimizes $f$ , and $f^* = f(x^*)$ ;
the PL inequality (3) with constant $\mu>0$ : $\tfrac12\|\nabla f(x)\|^2\ge\mu\,(f(x)-f^*)$ for all $x$ .

Theorem 4 adds a second-moment bound along the iterates: $\mathbb E_{i\sim\nu}\big[\|\nabla f_i(x_k)\|^2\big]\le C^2$ for every iterate $x_k$ .

Formalization targets

Goal: Theorem 4 (p. 6)

Under the assumptions above,

with the decreasing step $\alpha_k = \dfrac{2k+1}{2\mu(k+1)^2}$ ,

\mathbb E[f(x_k)-f^*]\le\frac{LC^2}{2k\mu^2}\qquad(k\ge1);

with a constant step $\alpha_k=\alpha$ , $0<\alpha<\dfrac1{2\mu}$ ,

\mathbb E[f(x_k)-f^*]\le(1-2\mu\alpha)^k\,[f(x_0)-f^*]+\frac{LC^2\alpha}{4\mu}\qquad(k\ge0).

The second-moment bound is assumed separately for the run of each scheme, with the same constant $C$ .

Milestones (proof of Theorem 4, p. 7)

One-step bound. For any point $x$ with $\mathbb E_i\|\nabla f_i(x)\|^2\le C^2$ and any step $a$ ,

\mathbb E_i[f(x-a\nabla f_i(x))]\le f(x)-a\|\nabla f(x)\|^2+\frac{LC^2a^2}{2}.

Recursion (10). Along the run, whenever $\alpha_k\ge0$ ,

\mathbb E[f(x_{k+1})-f^*]\le(1-2\alpha_k\mu)\,\mathbb E[f(x_k)-f^*]+\frac{LC^2\alpha_k^2}{2}.

Decreasing step rate, the first half of the goal.
Constant step rate, the second half of the goal.

Significance

The result. Theorem 4 places SG under PL on the same footing as SG under strong convexity: the same $O(1/k)$ rate, with constants depending on $L$ , $\mu$ and $C$ only, and no convexity. Since PL holds for least squares with any design matrix and, over any compact set, for logistic regression (§2.3 of the paper), the theorem gives explicit SG rates for these models. The constant-step bound quantifies the practitioners' rule of halving the step when progress stalls: halving $\alpha$ at least halves the noise floor $LC^2\alpha/(4\mu)$ .

Formalizing it. The result is proved, in a short argument, in the paper. To our knowledge no machine-checked proof exists: the existing Lean formalizations of SG rates on Prove2Me concern stationarity of non-convex objectives under a variance bound, a different noise model with a different conclusion. The remaining work is to formalize the paper's proof, which requires a usable treatment of expectations over an i.i.d. index sequence (conditioning the step from $x_k$ on the past) — infrastructure that every later analysis of a stochastic first-order method can reuse.

Difficulty

The deterministic content is elementary: the descent lemma, unbiasedness, the PL inequality, a telescoping sum and a geometric series. The difficulty is probabilistic bookkeeping. Recursion (10) takes the expectation of a one-step inequality with respect to $i_k$ alone, holding $x_k$ fixed; this is legitimate because $i_k$ is independent of $i_0,\dots,i_{k-1}$ , of which $x_k$ is a function. Making this precise requires measurability of the iterates in the sample path and a Fubini-type decomposition of the product law into the first $k$ coordinates, the $k$ -th coordinate and the rest. A second subtlety is that the second-moment bound holds only at the iterates, not at every point, so the one-step bound must be applied pointwise in the path, on a set of full measure, rather than once and for all.

Formalization scope

The space is EuclideanSpace ℝ (Fin d) and $\nabla$ is Mathlib's gradient. The index law is an arbitrary probability measure $\nu$ on a measurable space, and the path law is the infinite product Measure.infinitePi (fun _ => ν); the run is a deterministic function sgRun of the path. The Lipschitz-gradient assumption is stated literally on $\nabla f$ ; the PL inequality is the published predicate ShiOptRates.PolyakLojasiewicz f (gradient f) μ (f xstar) (inequality (3) multiplied by 2); the solution set is a point xstar with ∀ y, f xstar ≤ f y, and $f^*$ is f xstar, never a free real.

Every expectation of a gap is a lower Lebesgue integral of $\max(f(x_k)-f^*,0)$ with values in $[0,\infty]$ , which equals $\mathbb E[f(x_k)-f^*]$ because $f^*$ is the minimum; no integrability side condition can make a bound hold by default. The second-moment bound is the lower Lebesgue integral of $\|\nabla f_i(x_k)\|^2$ , required for almost every path and every $k$ . Unbiasedness and problem (7) carry explicit integrability, so a non-integrable gradient cannot turn them into trivialities.

The second-moment bound is deliberately not imposed at every point $x$ . With the bound at every point, $\|\nabla f\|\le C$ everywhere, so $f-f^*\le C^2/(2\mu)$ by PL, while along the gradient-ascent flow $f-f^*$ grows exponentially unless it vanishes; hence $f$ would be constant and the theorem vacuous. Along the iterates the hypothesis is met by non-constant objectives such as $f(x)=\tfrac12\|x\|^2$ .

Additions relative to the page, all disclosed in the statements: each $f_i$ is differentiable; $(i,x)\mapsto\nabla f_i(x)$ is jointly measurable, so that the iterates are random variables; the constant step is positive; the decreasing-step rate is stated for $k\ge1$ ; and "each $f$ has an $L$ -Lipschitz continuous gradient" is read as a condition on $f$ , the only one the proof uses. The page's proof of the constant-step bound writes the exponent $k$ where $k+1$ is meant; the statements follow the theorem's (correct) form.

Contributions welcome: the measurability of the run, the conditioning step for infinitePi, the deterministic one-step bound, and the two scalar recursions, each of which is reusable for other SG analyses.

Selected references

H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4, 2020. https://arxiv.org/abs/1608.04636
B. T. Polyak, Gradient methods for minimizing functionals, USSR Computational Mathematics and Mathematical Physics 3(4), 1963. https://doi.org/10.1016/0041-5553(63)90382-3
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4), 2009. https://doi.org/10.1137/070704277
F. Bach, E. Moulines, Non-strongly-convex smooth stochastic approximation with convergence rate O(1/n), NeurIPS 2013. https://arxiv.org/abs/1306.2119

7 thms2 active usersReviewed

Functional Analysis Markov Chain Statistics·Captain: mikedeng1

Spectral Gaps for a Metropolis–Hastings Algorithm in Infinite Dimensions I: The pCN Algorithm Has a Wasserstein Spectral Gap Uniform in the Dimension When the Potential Is Globally LipschitzResearch Paper

Motivation

Sampling from a distribution described relative to a Gaussian reference law is common in Bayesian inverse problems, where an unknown function or initial condition is inferred from noisy observations. Such a distribution is naturally infinite dimensional before it is approximated on a computer. A numerical method must therefore behave reliably as the approximation dimension grows. Hairer, Stuart and Vollmer study this question for Metropolis–Hastings chains and prove that the preconditioned Crank–Nicolson (pCN) chain admits a Wasserstein mixing bound with an iteration count independent of the projection dimension Hairer, Stuart and Vollmer (2014). This mission formalizes their globally Lipschitz case, Theorem 2.12.

The central practical concern is concrete: refining a discretization should improve the target approximation without forcing the number of Markov steps needed for a fixed contraction to grow with the number of coordinates. A bound on each finite dimensional chain separately would not settle that concern, because its constants could deteriorate with dimension. The theorem requires one set of constants for the infinite dimensional chain and every finite dimensional projection.

Setting

Let $H$ be a separable real Hilbert space. Its Gaussian reference measure $\gamma$ has mean zero and a covariance eigenbasis $e_1,e_2,\ldots$ . The subspace $K_m$ is the span of the first $m$ eigenvectors, and $\gamma_m$ is the law of the orthogonal projection of a $\gamma$ -distributed vector onto $K_m$ . The potential $\Phi:H\to\mathbb R$ determines the target measures

\mu(dx)=M e^{-\Phi(x)}\gamma(dx),\qquad \mu_m(dx)=M_m e^{-\Phi(x)}\gamma_m(dx),

where $M$ and $M_m$ normalize each measure. The paper's finite dimensional chain has state space $K_m$ , rather than the whole space $H$ with unused coordinates Hairer, Stuart and Vollmer (2014), (1.1)–(1.2).

At step size $0<\delta\le1/2$ , the pCN proposal from $x$ is $y=\sqrt{1-2\delta}\,x+\sqrt{2\delta}\,\xi$ , with $\xi$ drawn from $\gamma$ or $\gamma_m$ as appropriate. The move is accepted with probability $1\wedge e^{\Phi(x)-\Phi(y)}$ ; rejection leaves the state at $x$ . Write $P$ and $P_m$ for these transition kernels Hairer, Stuart and Vollmer (2014), (1.3), (1.5)–(1.6).

The potential is globally Lipschitz, $e^{-\Phi}$ is $\gamma$ -integrable, and the acceptance probability has a positive lower bound in specified balls centered at $\sqrt{1-2\delta}\,x$ outside a bounded region. These are Assumptions 2.10 and 2.11 Hairer, Stuart and Vollmer (2014), p. 12. The allowed ball radius is either a positive constant or $r_0\|x\|^a$ with $r_0>0$ and $1/2<a<1$ .

Formalization targets

Uniform Wasserstein contraction

For $\varepsilon>0$ , set $d_\varepsilon(x,y)=1\wedge\|x-y\|/\varepsilon$ . Choose the Lyapunov function $V(x)=\|x\|^i$ , where $i\ge1$ , or, in the growing-radius case, $V(x)=e^{v\|x\|}$ with $v>0$ . The weighted cost is $\widetilde d(x,y)=\sqrt{d_\varepsilon(x,y)(1+V(x)+V(y))}$ , and $W_{\widetilde d}$ is its infimum over couplings.

Theorem 2.12 asserts that $\mu$ and each $\mu_m$ are the unique invariant probability measures of $P$ and $P_m$ . It also asserts that, for every sufficiently small $\varepsilon$ , there is one integer $\widetilde n$ satisfying both bounds for all probability measures on the respective spaces and for every $m$ Hairer, Stuart and Vollmer (2014), p. 12:

W_{\widetilde d}(\nu_1P^{\widetilde n},\nu_2P^{\widetilde n})\le\tfrac12 W_{\widetilde d}(\nu_1,\nu_2),

W_{\widetilde d_m}(\nu_1P_m^{\widetilde n},\nu_2P_m^{\widetilde n})\le\tfrac12 W_{\widetilde d_m}(\nu_1,\nu_2).

Here $\widetilde d_m$ is the same formula restricted to $K_m$ . The milestone list includes the uniform Lyapunov, contraction and smallness claims and the cited weak Harris theorem; the Gaussian projection comparison of Lemma 3.1 is a further stated lemma of the mission. Fernique's Gaussian exponential-moment result is linked to its existing published formalization.

Significance

The result bounds the number of pCN iterations needed for a fixed Wasserstein contraction uniformly over the finite dimensional approximations. It also identifies the intended target as the only invariant probability measure, so the contraction describes convergence toward the measure used by the inverse problem. The weighted Wasserstein cost permits this statement on an unbounded Hilbert space, where an ordinary total variation small-set argument would impose a different kind of regularity Hairer, Stuart and Vollmer (2014), §§2.2–2.3.

The paper proved Theorem 2.12 in 2014. The remaining work here is a machine-checked development of the pCN kernels, Gaussian projections, Wasserstein estimates, and weak Harris application. A formalized Fernique theorem already exists in the platform library; the pCN estimates and Theorem 2.12 are open draft statements in this proposal. They will be reusable in the locally Lipschitz pCN regime and in analyses of other Metropolis kernels that satisfy the same abstract contraction conditions.

Difficulty

The pCN proposal contracts the starting points, but the accept–reject step can break that direct coupling: one chain may accept a proposal while the other rejects it. A bound on the proposal distance alone therefore does not imply a bound on the transition laws. The probability of that mismatched decision must be controlled near each pair of starting points, while the acceptance lower bound must remain uniform on the projected spaces. Large starting points also require a Lyapunov estimate to enter the bounded region used by the weak Harris theorem Hairer, Stuart and Vollmer (2014), §§3.1.1–3.1.3.

Formalization scope

The Lean development represents $H$ as a complete separable real inner product space with Borel measurable structure, $\gamma$ as a centered Gaussian probability measure, and the chosen Hilbert basis as diagonalizing its covariance. Second countability is stated explicitly for the measurable pCN construction; for a separable metric space it follows from the standing setting. The projected law is the pushforward by the orthogonal projection onto $K_m$ , a reading of the Karhunen–Loève formula in the paper. A measurable map is essential here: Mathlib's pushforward returns zero for a nonmeasurable map.

The target is Mathlib's normalized tilted measure. The theorem explicitly concludes that both the infinite dimensional and projected targets are probability measures, so the possible junk zero from a nonintegrable tilt cannot satisfy the result. Wasserstein costs and Lyapunov expectations use extended nonnegative integrals. This avoids the junk zero of a nonintegrable Bochner integral and the junk values of a real infimum. Couplings are measures with the prescribed marginals. The acceptance kernel uses the paper's $1\wedge e^{\Phi(x)-\Phi(y)}$ , including the first proposal and its rejection probability.

“Sufficiently small $\varepsilon$ ” means $\exists\varepsilon_0>0\,\forall\varepsilon\in(0,\varepsilon_0]$ . The iteration count is chosen before $m$ and before the input probability measures. Positive radius, positive power exponent and positive exponential coefficient exclude empty acceptance balls and the constant Lyapunov function. The $m=0$ projection is retained as the zero dimensional subspace. Contributions that establish the Gaussian comparison, the three pCN estimates, or the abstract weak Harris statement are within scope.

Selected references

M. Hairer, A. M. Stuart and S. J. Vollmer, Spectral gaps for a Metropolis–Hastings algorithm in infinite dimensions, Annals of Applied Probability 24(6), 2014, 2455–2490. arXiv:1112.1392v4, DOI:10.1214/13-AAP982.

10 thms2 active usersReviewed

Dynamical Systems Markov Chain Stochastic Systems·Captain: mikedeng1

Coexistence and Extinction for Stochastic Kolmogorov Systems 1: If Every Boundary Ergodic Measure Repels, X Converges Exponentially Fast in Total Variation to a Unique Interior Stationary LawResearch Paper

Motivation

Whether interacting species can coexist in a fluctuating environment is one of the basic questions of mathematical ecology. Deterministic models (Lotka–Volterra competition, predator–prey systems, food chains) answer it through invasion criteria: a population persists if, whenever it is rare, it grows. In a random environment the analogous criterion is phrased through Lyapunov exponents (long-run per-capita growth rates) computed against stationary distributions of the subcommunities in which some species are absent. Schreiber, Benaïm and Atchadé ([SBA11], J. Math. Biol. 62 (2011), MR 2786721) proved such a criterion for stochastic differential equations on a compact state space; A. Hening and D. H. Nguyen (arXiv:1704.06984, Ann. Appl. Probab. 2018) extended it to the non-compact orthant $\mathbb R^n_+$ , which is where population sizes actually live, and added an exponential rate of convergence.

Timeline. [SBA11] (2011) gave the compact-state SDE criterion via a minimax principle; Hening and Nguyen (2017/2018) removed compactness, proved convergence in total variation at a geometric rate, and in the same paper gave matching extinction results (the second and third missions of this series).

Setting

Let $n\ge1$ be the number of populations and $X(t)=(X_1(t),\dots,X_n(t))\in\mathbb R^n_+=[0,\infty)^n$ their sizes. The stochastic Kolmogorov system is

dX_i(t)=X_i(t)f_i(X(t))\,dt+X_i(t)g_i(X(t))\,dE_i(t),\qquad i=1,\dots,n,

where $f_i$ are per-capita growth rates, $g_i$ noise intensities, and $E(t)=\Gamma^\top B(t)$ with $B$ an $n$ -dimensional standard Brownian motion and $\Sigma=\Gamma^\top\Gamma=(\sigma_{ij})$ . Write $\mathbb R^{n,\circ}_+=(0,\infty)^n$ for the states with all species present, $\partial\mathbb R^n_+$ for its complement (some species absent) and $\|x\|=\sum_i|x_i|$ .

Assumption 1.1 (standing) requires: the matrix $(g_i(x)g_j(x)\sigma_{ij})$ is positive definite on $\mathbb R^n_+$ ; $f_i,g_i$ are locally Lipschitz; and for some $c\in\mathbb R^{n,\circ}_+$ , $\gamma_b>0$ ,

\limsup_{\|x\|\to\infty}\Big[\frac{\sum_ic_ix_if_i(x)}{1+c^\top x}-\frac12\frac{\sum_{i,j}\sigma_{ij}c_ic_jx_ix_jg_i(x)g_j(x)}{(1+c^\top x)^2}+\gamma_b\Big(1+\sum_i(|f_i(x)|+g_i^2(x))\Big)\Big]<0,

a dissipativity condition satisfied by logistic and competitive Lotka–Volterra models.

$P_X(t,x,\cdot)$ is the law of $X(t)$ started at $x$ . A probability measure $\mu$ is invariant if $\int P_X(t,x,\cdot)\,\mu(dx)=\mu$ for all $t$ ; ergodic invariant measures are the extreme points of that convex set. $\mathcal M$ is the set of ergodic invariant probability measures supported on $\partial\mathbb R^n_+$ (it contains the Dirac mass $\delta^*$ at $0$ ), and $\mathrm{Conv}(\mathcal M)$ its finite convex combinations. The Lyapunov exponent of species $i$ at $\mu$ is

\lambda_i(\mu)=\int\Big(f_i(x)-\frac{\sigma_{ii}g_i^2(x)}{2}\Big)\mu(dx).

Assumption 1.2: $\max_i\lambda_i(\mu)>0$ for every $\mu\in\mathrm{Conv}(\mathcal M)$ — every boundary state is invadable by some missing species.

Formalization targets

Goal: Theorem 1.1 (p. 6)

Under Assumptions 1.1 and 1.2 there is an invariant probability measure $\pi^*$ with $\pi^*(\mathbb R^{n,\circ}_+)=1$ , it is the only invariant probability measure concentrated on $\mathbb R^{n,\circ}_+$ , and for some $r\in(0,1)$ and every $x\in\mathbb R^{n,\circ}_+$ there is $C_x$ with

\|P_X(t,x,\cdot)-\pi^*\|_{TV}\le C_x\,r^t,\qquad t\ge0.

This is strong stochastic persistence (Definition 1.1) with an exponential rate; it leaves the rate $r$ and the constants unspecified, as the paper does.

Milestones

The milestones follow the proof: well-posedness, invariant faces and the moment bound (3.6) (Lemma 3.1); uniform moment bounds and the Feller property (Lemma 3.2); integrability under invariant measures (Lemma 3.3); $\delta^*\in\mathcal M$ ; convergence of occupation-measure integrals (Lemma 3.4); the log-Laplace bound (Lemma 3.5); irreducibility, aperiodicity and petite compacts for the skeleton chain (Lemma 3.6); the weighted invasion rate (4.1); boundary repulsion on average (Lemma 4.1); the Lyapunov contraction near the boundary (Proposition 4.1); the geometric drift (4.18); geometric ergodicity of the skeleton chain (4.26).

Significance

The result. Theorem 1.1 turns coexistence into a checkable condition on boundary subcommunities: one computes invasion rates of missing species against the stationary laws of the smaller systems. It is the persistence half of a dichotomy whose extinction half (Theorems 1.2–1.3) uses the same exponents, and it underlies the classification of stochastic food chains in the paper's own §2 (Theorem 2.1). The exponential rate gives quantitative mixing and supports further limit theorems for time averages.

Formalizing it. The theorem is proved in the paper but no machine-checked proof is recorded in this mission. A formalization exercises a chain of tools largely absent from current libraries: strong solutions of SDEs with locally Lipschitz coefficients on a closed orthant, the Feller property, tightness and weak limits of occupation measures, invariant and ergodic measures of diffusions, Meyn–Tweedie theory for skeleton chains, and log-Laplace (cumulant) estimates. Each milestone is a self-contained target; several (Lemma 3.5, the Meyn–Tweedie step) are independent of the population model.

Difficulty

The naive argument — positive invasion rates at each boundary ergodic measure imply that the process is pushed away from the boundary — fails twice. First, the state space is non-compact, so occupation measures need not be tight and the growth-rate functionals are unbounded; Assumption 1.1(3) and the moment bounds of Lemmas 3.2–3.4 are what replace compactness. Second, invasion rates are averages along the boundary dynamics, not pointwise drifts: the Lyapunov function $V(x)=(1+c^\top x)/\prod_ix_i^{p_i}$ decreases only on average over a time window of length $T^*$ , and turning this into a uniform contraction of $V^\theta$ requires controlling the full log-Laplace transform of the increment $\ln V(X(T))-\ln V(x)$ (Proposition 4.1), not just its mean. Uniformity of all constants in the starting point is the delicate part.

Formalization scope

The process is a family X x of strong solutions, one from each $x\in\mathbb R^n_+$ , on one probability space driven by one Brownian motion, using the published Ethier–Kurtz definitions SolvesBrownianSDE and IsStandardBrownian on $\mathbb R^n=$ SDEState n. Coordinates are Fin n; $n\ge1$ . The coefficients are functions on $\mathbb R^n$ read at the positive part $x^+$ , which agrees with the model on $\mathbb R^n_+$ . The norm is $\ell^1$ . Invariance is stated through the transition probabilities $P_X(t,x,\cdot)=$ law of $X^x(t)$ ; ergodic means extremal invariant. The $\limsup<0$ of (1.2) is written as " $\le-\varepsilon$ for $\|x\|\ge R$ ". Total variation is the published MarkovChainCLT.tvDist, $\sup_A|\mu(A)-\nu(A)|$ ; the paper does not fix the factor $2$ , and geometric convergence is insensitive to it. The constants $M>0,\delta_0$ of §3 are data satisfying (3.1), (3.2); $H$ is the supremum (3.5).

Deviations, all disclosed in the items: aperiodicity is the Meyn–Tweedie notion (no cycle of $d\ge2$ nonempty disjoint sets), because the literal definition on p. 15 makes every chain aperiodic; (4.1), cited from [SBA11, Lemma 4], retains the attained minimum $2\rho^*$ and is stated only in the direction used. Lemma 3.5 allows $K_2$ to depend on the fixed $\theta_0$ as its proof requires, despite the page saying “only on $K_1$ ”. Expectations of nonnegative quantities are lower Lebesgue integrals; wherever a Bochner integral appears, its integrability is part of the conclusion.

Trivializing readings are excluded: uniqueness is among invariant measures on $\mathbb R^{n,\circ}_+$ only (boundary invariant measures always exist), $\mathcal M$ is nonempty ( $\delta^*\in\mathcal M$ is a milestone, so Assumption 1.2 is never vacuous), and every existential constant is quantified before the points it must be uniform in. The logistic model on p. 4 gives a nonvacuous instance of Assumption 1.1.

Contributions welcome: general SDE well-posedness on invariant closed sets, Feller and tightness results for diffusions, Meyn–Tweedie geometric ergodicity for kernels, and cumulant-generating-function bounds, all reusable beyond this mission.

Selected references

A. Hening, D. H. Nguyen, Coexistence and extinction for stochastic Kolmogorov systems, Ann. Appl. Probab. 28(3), 2018. arXiv:1704.06984v1. https://arxiv.org/abs/1704.06984
S. J. Schreiber, M. Benaïm, K. A. S. Atchadé, Persistence in fluctuating environments, J. Math. Biol. 62(5), 655–683, 2011. MR 2786721, https://mathscinet.ams.org/mathscinet-getitem?mr=2786721
S. P. Meyn, R. L. Tweedie, Stability of Markovian processes I: criteria for discrete-time chains, Adv. Appl. Probab. 24(3), 542–574, 1992. MR 1174380, https://mathscinet.ams.org/mathscinet-getitem?mr=1174380
R. Khasminskii, Stochastic Stability of Differential Equations, 2nd ed., Springer, 2012. MR 2894052, https://mathscinet.ams.org/mathscinet-getitem?mr=2894052

20 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Approximate Revenue Maximization with Multiple Items 2: Selling Two I.I.D. Goods Separately Guarantees at Least e/(e + 1) ≈ 73% of the Optimal RevenueResearch Paper

Motivation

A seller with several goods can sell them one at a time or offer a mechanism that links allocation and payment across goods. Separate selling asks the seller to solve a one-good pricing problem for each item. A general mechanism can offer lotteries and menus whose outcomes depend on the buyer's whole valuation vector. The difference matters because the buyer's private information covers several values at once, and an optimal multidimensional mechanism need not resemble an ordinary posted price. Hart and Nisan ask how much revenue is guaranteed by simple selling rules when the joint valuation distribution is unrestricted apart from the stated independence assumptions (Hart and Nisan, arXiv:1204.1846v3).

This mission isolates their two-good, identically distributed result, Theorem B. The paper first gives a one-half guarantee for two independent goods with potentially different distributions, then improves the guarantee to $e/(e+1)$ when their distributions agree. The improvement is a claim about every probability law on nonnegative values. It assumes neither a density nor a regularity condition on the tail of that law. The paper proves the result in Appendix A.1 after stating it in the introduction (Hart and Nisan, pp. 6 and 31–35).

Setting

There is one risk-neutral buyer and one seller. For two goods, the buyer's private valuation is a vector $(Y,Z)$ with $Y,Z\ge0$ . Values are additive: receiving both goods is worth $Y+Z$ . The seller knows the distribution of the vector but not the realized values. In this mission, $Y$ and $Z$ are independent and have the same arbitrary probability law $\nu$ on $\mathbb R_{\ge0}$ . A law, rather than a named pair of random variables on a probability space, carries all the data needed by the revenue quantities.

A direct mechanism $\mu=(q,s)$ takes a reported pair $x=(y,z)$ and returns an allocation probability $q_i(x)\in[0,1]$ for each good and a real payment $s(x)$ to the seller. The buyer's payoff from reporting truthfully is $b(x)=q(x)\cdot x-s(x)$ . The mechanism is incentive compatible (IC) if truthful reporting is at least as good as any other report for every possible valuation, and individually rational (IR) if truthful payoff is nonnegative everywhere. These requirements hold on the whole nonnegative orthant, as in Section 2.1 of the paper (Hart and Nisan, pp. 11–14).

Write $R(\mu;X)$ for the expected payment under a valuation law $X$ and $\operatorname{Rev}(X)$ for the supremum of $R(\mu;X)$ over feasible, IC, IR mechanisms. For one good, write $\operatorname{Rev}_1(\nu)$ . The separate-selling revenue for two identically distributed goods is $\operatorname{SRev}(Y,Z)=2\operatorname{Rev}_1(\nu)$ . Equation (1) of the paper identifies the one-good value with the supremum of posted-price revenue $p\Pr[Y\ge p]$ ; the supremum formulation covers laws for which no maximizing price exists (Hart and Nisan, p. 12; Myerson, 1981).

Formalization targets

Theorem B: the guarantee for two i.i.d. goods

The goal is the exact upper bound written at the start of the paper's proof:

\operatorname{Rev}(Y,Z)\le\frac{e+1}{e}\bigl(\operatorname{Rev}(Y)+\operatorname{Rev}(Z)\bigr)=\frac{e+1}{e}\operatorname{SRev}(Y,Z).

Equivalently, separate selling guarantees at least $e/(e+1)$ of optimal revenue whenever the ratio has an ordinary meaning. The inequality itself is the stable formulation at zero and infinite revenues. The formal goal uses the exact constant $(e+1)/e$ , not the rounded percentage in the theorem's prose (Hart and Nisan, Theorem B, p. 6; proof, p. 31).

Supporting targets

The milestones include the one-good posted-price identity, the fact that nonnegative payments suffice when optimizing, symmetrization for identical independent goods, Lemma 19's lower-valuation revenue bound, equation (12), and the two expectation estimates and final numerical bound used after it. Proposition 5's IC characterization is also a draft theorem, though it is not a milestone. Each statement retains its source's domain and the constant $1/e$ . The final inequality for the right side of (12) is stated for every nondecreasing allocation function into $[0,1]$ , as required by the paper's argument on pp. 33–35.

Significance

Theorem B gives a distribution-free quantitative guarantee for an easy-to-describe selling rule in a setting where the optimal rule may depend on the buyer's entire two-dimensional private type. Its $e/(e+1)$ guarantee is stronger than the one-half guarantee for merely independent goods stated as Theorem A. The conclusion concerns the best revenue available from all feasible IC and IR mechanisms, so the benchmark includes randomized allocations and payments depending on both reported values (Hart and Nisan, pp. 6 and 11–13).

The formalization target is a machine-checked version of a proved result, not a new conjecture. The proposal currently contains compiled Lean statements with unproved theorem bodies. A completed development would prove the stated inequality and its selected supporting results. It would also supply reusable definitions for direct mechanisms with additive nonnegative values, extended-real revenue, optimal revenue as a supremum, and symmetry of two-good mechanisms. No machine-checked proof of these proposed Hart–Nisan statements is claimed here.

Difficulty

The one-good posted-price formula does not directly control an arbitrary two-good mechanism: allocation of either good and the payment can depend on both reported values. Applying a one-good bound separately to the two coordinates therefore leaves terms that depend on the other coordinate. In particular, a direct comparison between each marginal posted-price optimum and the total payment loses the improved constant. The proof has to control the dependence created by a joint mechanism while retaining the exact $1/e$ numerical estimate. A second formal difficulty is that an admissible mechanism can have a negative expected payment even though optimal revenue is nonnegative, while an unrestricted law can give infinite optimal revenue. Replacing every expectation by an ordinary real integral or clipping each mechanism's revenue would change Lemma 19 and the intermediate inequalities (Hart and Nisan, pp. 31–35).

Formalization scope

Valuations are finite vectors $\iota\to\mathbb R_{\ge0}$ ; the main theorem fixes $\iota=\operatorname{Fin}(2)$ . The two-good law is the product of the same one-good probability measure in both coordinates, so independence and identical distribution are built into the data. The model represents allocation probabilities as real numbers with explicit bounds $0\le q_i\le1$ . It requires IC and IR pointwise on all reports. No positive transfer (NPT) means $s(x)\ge0$ and is imposed only on supporting statements where the paper uses it. Following the paper's footnote 12, admissibility also requires the payment function to be measurable.

An individual expected payment is an extended real difference of positive and negative Lebesgue integrals. For IC mechanisms, the negative part is finite because the payment is bounded below by its value at zero. Optimal revenue is the supremum of the nonnegative clips of admissible mechanisms' expected payments; the zero mechanism makes this the same supremum as in the paper. Lemma 19 and equation (12) keep individual revenue in the extended reals. Supporting inequalities that write $r=\operatorname{Rev}_1(\nu)$ as a real number explicitly assume $r<\infty$ ; Theorem B does not. Integrals of bounded threshold functions use ordinary real expectation, while the nonnegative term $W$ uses a nonnegative Lebesgue integral. The goal cannot be satisfied by a correlated joint law, a bounded-support special case, a vacuous assumption on $\nu$ , or a rounded constant.

The reusable work includes one-good posted-price revenue for arbitrary laws, a nonnegative-transfer reduction, a faithful single-mechanism revenue type, and probability identities for two independent coordinates. Theorem A, Theorem 7, Theorem 16, and a full formalization of the paper's other selling rules are outside this mission.

Selected references

Sergiu Hart and Noam Nisan, Approximate Revenue Maximization with Multiple Items, Journal of Economic Theory, 2017. Source used here: arXiv:1204.1846v3.
Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. DOI:10.1287/moor.6.1.58.

11 thms2 active usersReviewed

Dynamical Systems Harmonic Analysis Machine Learning·Captain: mikedeng1

Approximation Bounds for Random Neural Networks and Reservoir Systems II: Echo State Networks with Random Weights Approximate Regular Functionals with an Explicit L² Error Bound (Theorem 2)Research Paper

Motivation

Reservoir computing learns an input/output system from data in two stages. A dynamical system, the reservoir, is driven by the input sequence and its state is recorded; then only a linear readout of that state is trained, by least squares. The echo state network (ESN) is the most widely used reservoir: its state evolves by $x_t = \sigma(Ax_{t-1} + Cz_t + \zeta)$ , with the matrices $A, C$ and the vector $\zeta$ drawn at random and never trained. ESNs predict chaotic systems well in practice (Jaeger & Haas, Science 2004), and they are known to be universal: for every fading-memory input/output map some ESN approximates it (Grigoryeva & Ortega, Neural Netw. 2018). Universality does not explain the practice, where the reservoir weights are random and fixed in advance. Gonon, Grigoryeva & Ortega (Ann. Appl. Probab. 2023) prove that an ESN whose weights are drawn from an explicit distribution that does not depend on the target approximates every sufficiently regular target, with an explicit $L^2$ error bound. This mission formalizes that result, Theorem 2, and the chain of results its proof rests on.

Setting

Time runs over $\mathbb Z_- = \{0, -1, -2, \dots\}$ . Inputs take values in a set $D_d$ with $0 \in D_d \subset B_M \subset \mathbb R^d$ , where $B_M$ is the closed Euclidean ball of radius $M > 0$ . The input $Z = (Z_t)_{t \in \mathbb Z_-}$ is a $D_d$ -valued process with law $\mu_Z$ . The target is a functional $H^* : (D_d)^{\mathbb Z_-} \to \mathbb R$ , the present output as a function of the whole input history. All norms are Euclidean.

Regularity. Fix weights $w_{-i} > 0$ with $\sum_i i\, w_{-i} < \infty$ . $H^*$ is $w$ -Lipschitz with constant $L > 0$ if $|H^*(u) - H^*(v)| \le L\sum_{i \ge 0} w_{-i}\|u_{-i} - v_{-i}\|$ . Assumption 1 asks, in addition, for every $T \ge 1$ : with $q = d(T+1)$ , the truncation $H^*_T(z_0, \dots, z_{-T}) = H^*(\dots, 0, z_{-T}, \dots, z_0)$ has a Fourier representation $H^*_T(u) = \int_{\mathbb R^q} e^{i\langle w, u\rangle} g_T(w)\,dw$ on $(D_d)^{T+1}$ , with $g_T \in L^1$ and $\int \max(1, \|w\|^3)|g_T(w)|^2\,dw < \infty$ .

The random ESN. Fix $T, N \ge 1$ , $R > 0$ , and a bound $M_T$ with $\|(Z_0, \dots, Z_{-T})\| \le M_T$ almost surely. Draw $A_1, \dots, A_N$ i.i.d. uniform on $B_R \subset \mathbb R^q$ and, independently, $\zeta_1, \dots, \zeta_N$ i.i.d. uniform on $[-\max(M_TR,1), \max(M_TR,1)]$ . With $S$ the block shift on $\mathbb R^q$ and $c$ the embedding of $\mathbb R^d$ into the first block, and $a$ the matrix with rows $A_i^\top$ , put

\bar A = \begin{pmatrix} S & 0\\ aS & 0\end{pmatrix},\quad \bar C = \begin{pmatrix} c\\ ac\end{pmatrix},\quad \bar\zeta = \begin{pmatrix} 0\\ \zeta\end{pmatrix},\quad A = \begin{pmatrix}\bar A & -\bar A\\ -\bar A & \bar A\end{pmatrix},\quad C = \begin{pmatrix}\bar C\\ -\bar C\end{pmatrix},\quad \zeta = \begin{pmatrix}\bar\zeta\\ -\bar\zeta\end{pmatrix}.

The ESN is $X_t = \sigma(AX_{t-1} + CZ_t + \zeta)$ , $Y_t = WX_t$ , with $\sigma(x) = \max(x, 0)$ and state space $\mathbb R^{2(N+d(T+1))}$ .

Formalization targets

Goal: Theorem 2 (p. 54)

For every $H^*$ satisfying Assumption 1 there is a readout $W$ , a function of the random weights alone, such that the ESN has the echo state property (a unique state sequence for every input) and

\mathbb E\big[|Y_0 - H^*(Z)|^2\big]^{1/2} \le \frac{\sqrt{C_{T,R}}}{\sqrt N} + \int_{\mathbb R^q \setminus B_R}|g_T(u)|\,du + LM\sum_{i > T} w_{-i},

with $C_{T,R} = 16\max(M_TR,1)\mathrm{Vol}_q(B_R)(M_T+1)^2(M_T^3+M_T+16)\int_{B_R}\max(1,\|u\|^3)|g_T(u)|^2\,du$ .

Milestones

(8), p. 33: a scalar identity expressing $e^{iz} - iz - 1$ as an integral of ReLU ramps.
Proposition 2, pp. 31–32: under a Fourier condition, $f$ is an integral of ReLU ridge functions with a compactly supported, square-integrable weight $\pi$ .
Proposition 3, pp. 41–42: a static ReLU network with uniformly sampled inner weights achieves mean-square error $C^*/N$ .
Corollary 1, p. 43: the same with a dimension-free integrability condition and a truncation term.
Remark 10, p. 53: the shift reservoir is nilpotent, has $K = I$ and stores the last $T+1$ inputs.
Proposition 6, p. 51: a linear reservoir with a random ReLU readout satisfies the bound (54).
(64)–(66), pp. 55–56: every solution of the ESN reduces to the linear shift reservoir, which gives uniqueness.

Significance

Theorem 2 is the first approximation bound for echo state networks whose recurrent and input weights are sampled from a generic distribution rather than constructed from the target. The bound separates three error sources: a Monte Carlo term decaying like $N^{-1/2}$ , a truncation term in the sampling radius $R$ , and a memory term in the window length $T$ . Because the readout can be taken to be the least-squares readout, the bound also controls the trained networks used in practice, and it is the input to the paper's rate and universality corollaries (Corollaries 4 and 5).

Status: the result is proved on paper. No part of it is formalized; the only reservoir-computing material on the platform is the published definition ReservoirESN (the state equation), which this mission reuses. A formal proof would supply the first machine-checked random-feature approximation bound with explicit constants.

Difficulty

The obvious argument fails in two places. First, the classical integral representations of Barron type place the inner weights on unbounded sets, which cannot be sampled uniformly; Proposition 2 needs a change of variables that makes the weight compactly supported while keeping it square integrable, and this costs the factor $R^{-(2q+2)}$ and the condition (5). Second, a ReLU network is not contractive, so the echo state property of the ESN cannot be taken from the standard contraction criterion; it has to be derived from the block structure of $A$ , which makes the difference of the two state halves follow a nilpotent linear recursion.

Formalization scope

$\mathbb R^q$ is EuclideanSpace ℝ (Fin (T+1) × Fin d), block $k$ holding $z_{-k}$ ; input sequences are ℕ → EuclideanSpace ℝ (Fin d) with index $k = -t$ , and $x_t = F(x_{t-1}, z_t)$ is the published ReservoirESN.IsSolution. Points of $\mathbb R^{q+1}$ are pairs with norm $(\|w\|^2 + u^2)^{1/2}$ . The uniform laws are Lebesgue measure conditioned on the ball or interval; $N$ i.i.d. rows have the product law. The input is independent of the weights (§4.1) and $D_d$ -valued with $0 \in D_d \subset B_M$ (§5.1): expectations are iterated lower Lebesgue integrals over $\mu_Z$ and the product law, and probability- $(1-\delta)$ statements bound the product measure of the bad set. The scalar output case $m = 1$ is used, as in the paper. Assumption 1 is required for every $T \ge 1$ , as printed.

A readout allowed to depend on the input would make every bound trivial; in every statement the readout is a measurable function of the inner weights alone.

Departures from the print, each disclosed in the item: the last term of Proposition 6 is the $L^2(\mu_Z)$ norm of $\|K^{-1}S^{T+1}X_{-T-1}\|$ , which the page prints outside the expectation; the state space of the linear reservoir (52) is a parameter $D_N$ , as in §2.1, and its solution is assumed to be a random process; Proposition 3 omits " $C^* > 0$ " (the explicit value (33) is used); measurability of the Fourier density $g$ is stated where the page leaves it implicit.

A complete development needs Fourier integrals on Euclidean spaces, change of variables under linear maps, product measures and Fubini–Tonelli, and an importance-sampling variance bound. The static results (Propositions 2, 3, Corollary 1) are reusable for random-feature models beyond reservoir computing. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

L. Gonon, L. Grigoryeva, J.-P. Ortega, Approximation bounds for random neural networks and reservoir systems, Ann. Appl. Probab. 33(1), 28–69, 2023. https://doi.org/10.1214/22-AAP1806
L. Grigoryeva, J.-P. Ortega, Echo state networks are universal, Neural Netw. 108, 495–508, 2018. https://doi.org/10.1016/j.neunet.2018.08.025
H. Jaeger, H. Haas, Harnessing nonlinearity: predicting chaotic systems and saving energy in wireless communication, Science 304, 78–80, 2004. https://doi.org/10.1126/science.1091277
A. R. Barron, Universal approximation bounds for superpositions of a sigmoidal function, IEEE Trans. Inf. Theory 39, 930–945, 1993. https://doi.org/10.1109/18.256500
J. M. Klusowski, A. R. Barron, Approximation by combinations of ReLU and squared ReLU ridge functions with ℓ1 and ℓ0 controls, IEEE Trans. Inf. Theory 64, 7649–7656, 2018. https://doi.org/10.1109/tit.2018.2874447
C. Cuchiero, L. Gonon, L. Grigoryeva, J.-P. Ortega, J. Teichmann, Discrete-time signatures and randomness in reservoir computing, IEEE Trans. Neural Netw. Learn. Syst., 2021. https://doi.org/10.1109/TNNLS.2021.3076777

11 thms2 active usersReviewed

Dynamical Systems Machine Learning·Captain: mikedeng1

Approximation Bounds for Random Neural Networks and Reservoir Systems III: Echo State Networks with Output Feedback and Random Weights Approximate Contracting Reservoirs (Theorem 4)Research Paper

Motivation

An echo state network with output feedback is a recurrent model whose previous output is fed back into its next hidden-state update. In reservoir computing only the linear output weights are trained, while the internal weights are fixed, typically after being drawn at random. This raises a quantitative question: if the internal rows are sampled from a fixed law, can a network with $N$ blocks of random rows and a suitable linear readout approximate a given input–output rule, and at what rate in $N$ ? Gonon, Grigoryeva and Ortega answer this for targets generated by contracting reservoir systems. Their Theorem 4 (p. 63) gives, with explicit constants, a probability bound and an excess-risk bound of order $1/\sqrt N$ , plus a term decaying geometrically in the length $T$ of the observation window. The input set is not required to be bounded: the bound depends on the input process only through $\mathbb E[\max_{t}\|Z_t\|]$ over the window.

Setting

Inputs are vectors in a set $D_d\subseteq\mathbb R^d$ and an input history is $z=(z_t)_{t\in\mathbb Z_-}$ , with $\mathbb Z_-=\{0,-1,-2,\dots\}$ . A target reservoir is a map $F^*:\mathbb R^{N^*}\times D_d\to B_M$ , with $B_M$ the closed Euclidean ball of radius $M$ , such that $F^*(\cdot,v)$ is an $r$ -contraction for every $v\in D_d$ , with $r\in(0,1)$ . Its reservoir functional is $H^*(z)=x^*_0$ , where $x^*_t=F^*(x^*_{t-1},z_t)$ for all $t\in\mathbb Z_-$ . The output dimension is $m=N^*$ .

The approximating network has $N$ blocks of $N^*$ rows. Each row is a vector $\omega=(a,c,\zeta)\in\mathbb R^{N^*+d+1}$ , and the $\bar N=NN^*$ rows $U_j^{(i)}$ of $[A,C,\zeta]$ are i.i.d. with law $\pi$ . With an activation $\sigma$ and a readout matrix $W\in\mathbb M_{m,\bar N}$ , the system is

x_t=\sigma(Ay_{t-1}+Cz_t+\zeta),\qquad y_t=Wx_t,\qquad t=-T,\dots,0,\qquad y_{-T-1}=\Xi,

with $T\ge1$ and $\|\Xi\|\le M$ ; its functional is $H^{A,C,\zeta}_W(z)=y_0$ . For each $k\ge1$ and $j=1,\dots,N^*$ a signed measure $\pi_j^k\ll\pi$ defines the integral map

F_j^{*,N}(x,v)=\int\sigma((x,v,1)\cdot\omega)\,\pi_j^N(d\omega).

The constant $C_*=4\sqrt3L_\sigma\sup_{k}\sum_j(\int\|\omega\|^2(d\pi_j^k/d\pi)^2d\pi)^{1/2}$ measures the size of these densities, and $s_N=\mathbb E[\max_{t\in\{0,\dots,-T\}}\sup_{x\in B_{M+1}}\|F^{*,N}(x,Z_t)-F^*(x,Z_t)\|]$ is the approximation error of $F^{*,N}$ . The input process $Z$ is independent of $(A,C,\zeta)$ , $Y_0$ is an integrable target, and the loss $L\ge0$ is Lipschitz with constant $L_L$ . The echo state event $\Omega_{\mathrm{ESP}}$ of (87) is the event that $\|WF^{A,C,\zeta}(x,Z_t)\|\le M+1$ for all $x\in B_{M+1}$ and $t\in\{0,\dots,-T\}$ , where $F^{A,C,\zeta}(x,v)=\sigma(Ax+Cv+\zeta)$ .

Formalization targets

Steps of the proof

The milestones are the displayed estimates of the proof, in attack order:

(89): one step of the error recursion on $\Omega_{\mathrm{ESP}}$ , $\mathbb E[\|Y_t-X^*_t\|\mathbb 1_{\Omega_{\mathrm{ESP}}}]\le\mathbb E[\sup_{y}\|\cdots\|]+s_N+r\,\mathbb E[\|Y_{t-1}-X^*_{t-1}\|\mathbb 1_{\Omega_{\mathrm{ESP}}}]$ ;
(90): splitting into coordinates and symmetrization of the uniform error of the random map;
(91): a deterministic bound on Rademacher averages,

\mathbb E_\varepsilon\sup_{y\in B_{M+1}}\Big|\sum_{i=1}^N v_i\varepsilon_i\sigma((y,z,1)\cdot u_i)\Big|\le2L_\sigma\Big((M+1)\big(\textstyle\sum_iv_i^2\|a_i\|^2\big)^{1/2}+\|z\|\big(\sum_iv_i^2\|c_i\|^2\big)^{1/2}+\big(\sum_iv_i^2\zeta_i^2\big)^{1/2}\Big);

(92)–(93): for each fixed input $z\in D_d$ ,

\mathbb E\sup_{y\in B_{M+1}}\Big\|\frac1N\sum_{i=1}^NW_i\sigma(A^{(i)}y+C^{(i)}z+\zeta^{(i)})-F^{*,N}(y,z)\Big\|\le\frac{(M+2+\|z\|)C_*}{\sqrt N};

(96): $\mathbb P(\Omega\setminus\Omega_{\mathrm{ESP}})\le2(M+2+\mathbb E[\max_t\|Z_t\|])C_*/\sqrt N+2s_N$ .

Goal: Theorem 4

There is a readout $W$ , a function of $(A,C,\zeta)$ alone, such that for every $\delta\in(0,1)$ and every $\|\Xi\|\le M$ , with probability at least $\max(1-\delta-2C_*(M+2+\mathbb E[\max_t\|Z_t\|])/\sqrt N-2s_N,0)$ , the event $\Omega_{\mathrm{ESP}}$ holds and

|\mathcal R(H^{A,C,\zeta}_W)-\mathcal R(H^*)|\le \frac{L_L}{\delta}\Big[\frac{(M+2+\max_t\mathbb E\|Z_t\|)C_*}{(1-r)\sqrt N}+\frac{s_N}{1-r}+2(M+1)r^{T+1}\Big],

where $\mathcal R(H)=\mathbb E[L(H(Z),Y_0)]$ is evaluated at fixed network weights.

Significance

The bound separates three sources of error: sampling $N$ blocks of random rows (rate $1/\sqrt N$ ), the approximation of $F^*$ by the integral map $F^{*,N}$ ( $s_N$ ), and the finite initialization of the feedback recursion ( $r^{T+1}$ ). Only the readout depends on the target; the internal weights are generated without it. The theorem also bounds the probability that the random feedback map leaves the state ball on which the recursion is controlled, which is the form in which the echo state property enters. Via Theorem 3 (p. 62), which specializes the densities through the paper's Proposition 2, it gives approximation rates for ReLU output-feedback networks.

The paper proves the result on pp. 63–68. No part of it is formalized. A complete development would give machine-checked Rademacher symmetrization and contraction estimates for random features, uniform-over-a-ball bounds for sampled integral maps, and a treatment of finite feedback recursions on product probability spaces, all reusable outside reservoir computing.

Difficulty

A pointwise approximation of $F^*$ by the sampled map does not control the feedback system, because the next feedback value is itself the random output of the previous update. The comparison must hold uniformly over the state ball $B_{M+1}$ and over the whole input window, and the event that the recursion leaves the ball must be charged to an explicit probability. The uniform bound requires symmetrization and the Ledoux–Talagrand contraction principle for a supremum over a continuum of states, with per-index contractions; Lipschitz continuity of $\sigma$ alone does not supply the vanishing at zero that principle needs. The input is unbounded, so the input dependence must be tracked through $\|z\|$ and integrated at the end.

Formalization scope

States, inputs, outputs and rows are Euclidean spaces (EuclideanSpace); a row is indexed by $(\{1..N^*\}\sqcup\{1..d\})\sqcup\{\ast\}$ and the rows by $\{1..N\}\times\{1..N^*\}$ . Time $t\in\mathbb Z_-$ is the index $-t\in\mathbb N$ ; the equation (78) is the published ReservoirESN.IsSolution. The rows have law $\pi^{\otimes NN^*}$ on their own space and $(Z,Y_0)$ lives on a separate probability space; the probability is under the product law, which encodes the independence of §6.1. Signed measures $\pi_j^k$ are their Radon–Nikodym densities with respect to $\pi$ , with integrability and first-moment hypotheses. $C_*$ , $s_N$ and $\mathbb E[\max_t\|Z_t\|]$ are extended nonnegative integrals and suprema, converted to reals only under their finiteness hypotheses; the risk integrals are finite under the loss Lipschitz bound, integrable target and input-moment assumption; the supremum in (87) is unfolded. $F^*$ is assumed jointly measurable, the standing convention that makes $s_N$ and $H^*(Z)$ random variables; the standing assumptions $d,N^*\ge1$ and $M>0$ (p. 30) and $T\ge1$ (§6.1) are hypotheses.

Trivialization ruled out. The readout is a measurable function of the rows only and is chosen before $\delta$ and $\Xi$ . A readout allowed to look at the input $Z$ would make the claim a different and much weaker statement.

Correction of the print. The goal and milestones (91), (93), (96) assume $\sigma(0)=0$ : the contraction principle cited at (91) needs contractions vanishing at zero, while the printed theorem states only that $\sigma$ is Lipschitz. ReLU, the paper's application, satisfies it. The goal retains the printed full risk difference. Its proof passes through (88), where an indicator depending on $Z$ is moved inside a risk integral; this step needs further justification. The milestone quotations keep the printed text.

Contributions are welcome on each milestone, on general Rademacher symmetrization and contraction lemmas for suprema over compact parameter sets, on measurability of suprema of continuous random fields, and on the printed form of the risk bound.

Selected references

L. Gonon, L. Grigoryeva and J.-P. Ortega, Approximation bounds for random neural networks and reservoir systems, The Annals of Applied Probability 33(1), 2023, 28–69. https://doi.org/10.1214/22-AAP1806
M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991 (Theorem 4.12, the contraction principle). https://doi.org/10.1007/978-3-642-20212-4

8 thms2 active usersReviewed

Information Theory Quantum Information·Captain: mikedeng1

Semidefinite Programming Hierarchies for Constrained Bilinear Optimization II: De Finetti Without Symmetry — Random Subsystems Are 3k^{3/2}d_B³ log d_B/√(n−k+1)-Close to Product in ExpectationResearch Paper

Motivation

Quantum information often describes a system through a state shared among many small registers. One would like to replace the state on a few registers by a product of their individual states, because product states are easier to estimate and optimize over. The usual finite quantum de Finetti theorems obtain such approximations from permutation symmetry. A physical preparation, however, need not be symmetric. Berta, Borderi, Fawzi and Scholz give a quantitative statement that instead selects the retained registers at random and conditions on measurements of other registers. Their Theorem 2.5 is the target here.

The authors place this result alongside their hierarchy for constrained bilinear optimization, but the theorem without symmetry is independent of the hierarchy. In §2.6 they compare its polynomial dependence on the local dimension and the number of retained registers with the earlier no-symmetry approximation discussed in their reference [12]. The result identifies exactly what random selection and measurement can supply when a global permutation-invariance hypothesis is unavailable.

Setting

Let $B$ be a quantum system of dimension $d_B$ , and let $\rho$ be an arbitrary density operator on $n$ copies of $B$ . Choose a uniformly random permutation of these copies. Its first $k$ positions form an ordered tuple $\vec i=(i_1,\ldots,i_k)$ of systems to retain; the remaining $r=n-k$ positions form an ordered tuple $\vec j=(j_1,\ldots,j_r)$ available for measurement. There is no symmetry condition on $\rho$ .

A measurement on $B$ has finitely many outcomes $z$ and positive operators $M_z$ whose sum is the identity. Measure the first $m$ systems $j_1,\ldots,j_m$ , where $0\le m\le r$ , and condition the retained state on the observed outcomes. Write $\rho_{\vec i\mid z}$ for that conditional state and $\rho_{i_s\mid z}$ for its marginal on the $s$ th retained system. The trace norm $\|X\|_1=\operatorname{Tr}\sqrt{X^\dagger X}$ measures the error between $\rho_{\vec i\mid z}$ and $\rho_{i_1\mid z}\otimes\cdots\otimes\rho_{i_k\mid z}$ . The expectation is over the uniform permutation and the measurement outcomes, with their Born-rule probabilities.

The distortion with side information of a fixed measurement is the largest ratio between an input trace norm and the norm left after measuring only its $B$ factor. The input ranges over Hermitian operators on $A\otimes B$ , over every finite-dimensional side system $A$ , with zero partial trace on both $A$ and $B$ . The paper's $f(B\mid\cdot)$ is the infimum of this distortion over all measurements on $B$ equation (10). A state two-design is a finite family of rank-one projectors whose average second tensor power is the projector onto the symmetric subspace with the normalization in Lemma D.1. The projectors give an explicit measurement with distortion at most $d_B^2(d_B+1)$ .

Formalization targets

The principal target is the explicit form of Theorem 2.5. For $1\le k\le n$ , put $r=n-k$ . With the two-design measurement, some $m\in\{0,\ldots,r\}$ satisfies

\mathbb E_{\vec i,\vec j,z}\left\|\rho_{\vec i\mid z}-\bigotimes_{s=1}^k\rho_{i_s\mid z}\right\|_1 \le k d_B^2(d_B+1)\sqrt{\frac{(2\ln 2)(k-1)\log_2 d_B}{r+1}} \le \frac{3k^{3/2}d_B^3\log_2 d_B}{\sqrt{r+1}}.

Here the $z$ in the expectation is the outcome string for the first $m$ members of $\vec j$ . The same $m$ is chosen before taking that expectation. This rate is stated with its constants and its two consecutive inequalities; an existence assertion without the error bound would lose the theorem's content.

The milestone path also states the telescoping trace-norm inequality of equation (12), the measurement estimate of Lemma D.1, and the final averaged inequality on p. 11. A companion milestone treats any fixed POVM with its own distortion. That formulation captures the proof's arbitrary-measurement step without treating the infimum $f(B\mid\cdot)$ as if every measurement attained it.

Significance

For an arbitrary multipartite state, random ordering and conditioning give one measured prefix length at which the selected registers have small expected distance from a product. The explicit rate is polynomial in $d_B$ and $k$ and decays as $1/\sqrt{n-k+1}$ . It therefore gives a quantitative approximation guarantee under a selection rule that can be applied without first establishing exchangeability Berta et al., §2.6.

The theorem is proved in the paper; the work here is to express its state, measurement, conditional distribution, and norm bound in Lean and to connect the estimate to reusable finite-dimensional quantum-information definitions. The local statements are currently proof obligations, not machine-checked proofs. The published density-operator, trace-norm, and partial-trace definitions are reused. Once proved, the statements can serve as a precise interface for subsequent formal work on randomized subsystem selection and information-theoretic decoupling.

Difficulty

Randomly choosing systems does not turn the original state into a product state. A direct bound on the distance to a product can be large even when each one-system marginal is simple, because correlations among the retained systems remain. Equation (12) breaks the total error into successive correlation terms; the paper controls their average by measuring other systems and using information-theoretic estimates. A second difficulty is that a measurement can erase distinctions between different input operators. The two-design estimate supplies a dimension-dependent bound on that loss, uniformly over the size of a side system.

The printed theorem leaves the measurement $M_B$ unspecified while using the minimum distortion over all measurements. A trivial measurement cannot satisfy that reading. The proof explicitly permits the measurement built from a state two-design, with $d_B^2(d_B+1)$ replacing $f(B\mid\cdot)$ ; that is the measurement used in the goal proof of Theorem 2.5, p. 10.

Formalization scope

The $B$ system has basis Fin dB; $n$ copies have basis Fin n → Fin dB. The formalization writes $n=k+r$ , assumes $k\ge1$ , and ranges over $m\le r$ . A state is a positive semidefinite complex matrix with trace one. Permutations act on the copy coordinates, and their finite uniform average models the paper's random ordered tuples. Measurement outcomes are finite words; the conditional state divides the unnormalized post-measurement state by its probability. A zero-probability outcome uses Lean's zero inverse and contributes zero to the weighted expectation. The existence of a state and of a nonempty two-design rules out zero-dimensional and empty-outcome instances in the goal.

The fixed-measurement distortion and $f(B\mid\cdot)$ take values in extended nonnegative reals, so a measurement that destroys a nonzero operator has infinite distortion. The logarithm is base two except for $\ln 2$ . The definitions use the paper's unnormalized trace norm, with no factor $1/2$ . No mutual-information estimate or Pinsker inequality is assumed in the goal: both belong to possible proofs. Contributions proving the stated milestones, the positivity and normalization of the conditional states, or reusable trace-norm facts for finite tensor products all advance the target.

Selected references

M. Berta, F. Borderi, O. Fawzi and V. B. Scholz, Semidefinite programming hierarchies for constrained bilinear optimization, Mathematical Programming, 2021; arXiv:1810.12197v3.

12 thms2 active usersReviewed

Optimization·Captain: visuddhi

VC Theory for Inventory Policies: Xie–Ma–Xin BoundsResearch Paper

Learning inventory policies from historical demand

An inventory policy chooses how much stock to order before demand is observed. Its quality is assessed by the holding and backlogging costs it incurs on future demand. A policy chosen to perform well on historical demand can overfit those observations. A useful statistical guarantee therefore controls the difference between historical and future costs simultaneously over the policies that the procedure may select. Xie, Ma and Xin establish such guarantees for stationary base-stock, $(s,S)$ , and nonstationary base-stock policy classes.

This formalization covers the principal bound families in that paper. Its first goal is the expected generalization and estimation bound for nonstationary base-stock policies with no fixed ordering cost, Corollary 4.10. Its supporting targets include Theorem 4.9 and the constructive product-sample partition in Lemma 4.12. The other principal bounds remain in the explicit scope below and await their own full Lean declarations. The companion inventory-information project needs these results as proved dependencies; merely citing the paper does not close that project's formal proof obligations.

Demand, policy classes and statistical errors

There are $T+L$ periods, a deterministic lead time $L\ge0$ , and demand bounded by $U>0$ . The first order arrives in period $L+1$ . Average loss means the sum of holding and backlogging costs in periods $L+1,\ldots,T+L$ , divided by the positive horizon $T$ . The initial pipeline is empty, and initial inventory is nonpositive for the base-stock models. Holding and backlogging cost coefficients are $h,b\in[0,1]$ . Nonstationary base-stock policies in the first goal have no fixed ordering cost and use levels $S^t\in[0,(L+1)U]$ .

The Lean model indexes the first period by zero. It uses the source's explicit finite-maximum formula for post-replenishment inventory, with the demand interval summed up to, but excluding, the observation period. In mathematical notation the inventory in period $L+k+1$ is $\max_{0\le j\le k}(S_j-\sum_{j\le r<k+L}d_r)$ . Cost is evaluated after subtracting the current demand $d_{L+k}$ . This is a backlog model; applications to lost sales require a separate equivalence argument.

Data comprise $N>0$ IID demand trajectories from a probability measure $\mu$ on the bounded trajectory space. Different periods of the same trajectory can be dependent. Generalization error is the one-sided supremum $\mathrm{GE}=\sup_S(R(S)-\widehat R(S))$ , where $R$ is expected average loss and $\widehat R$ is empirical average loss. Estimation error is $R(\widehat S)-R(S_*)$ , for an empirical minimizer and a best-in-class population policy. It is not the error relative to every history-dependent inventory policy. These conventions follow Sections 3 and 4.

Formalization targets

The first goal, Corollary 4.10, asserts the existence of one absolute constant $C>0$ such that

\mathbb E\mathrm{EE}\le\mathbb E\mathrm{GE}\le C(L+1)U/\sqrt N.

The constant is quantified before the horizon, lead time, support, costs, demand distribution, sample size, and policy selections. The first inequality explicitly refers to actual minimizers, with an integrable selected risk. The GE conclusion holds independently of whether a particular selector has been supplied.

Its principal complexity target is Theorem 4.9: for each relevant period and $0<\gamma\le1$ , the normalized inventory class has fat-shattering dimension at most $2/\gamma+1$ . The Lean statement says directly that every $\gamma$ -shattered indexed sample has cardinality at most that number. It uses the source convention of a strict upper label and non-strict lower label.

Lemma 4.12 partitions all $N^D$ product indices into $N^{D-1}$ groups of $N$ indices. Every coordinate of every group traverses the original row indices exactly once. The formal statement uses a bijection between anchor-offset pairs and complete index tuples, together with a coordinate-permutation assertion. The dimension $D=d+1$ is positive, and $N=1$ and $D=1$ are included.

The full scope also retains Theorem 4.1 and Corollary 4.2 (stationary policies), Theorem 4.4 and Corollary 4.5 ( $(s,S)$ upper bounds), Theorem 4.7 and Corollary 4.8 ( $(s,S)$ fat-shattering and GE lower bounds), and the expected Product ERM comparison in equation (4.7). They are catalogued with their assumptions but are not yet all encoded. The GE lower bound is not asserted to be a minimax policy-regret lower bound.

What the formalization supplies

The nonstationary policy vector grows with the horizon, while the expected average-loss bound has no horizon factor. A verified version supplies a reusable statistical ingredient for finite-horizon inventory learning. Total-cost bounds require multiplication by the horizon. Absolute uniform deviation, period-dependent costs, high-probability statements, initial-state reductions, and censoring require further bridge theorems. They are not attributed to Corollary 4.10 without those proofs.

The cyclic partition has a complete locally checked Lean proof with axiom dependencies only propext and Quot.sound. The two statistical targets remain open. Neither a drafted declaration nor a local proof is described as a server-verified contribution.

Mathematical difficulty

Ordinary pseudodimension can grow with the horizon for the nonstationary class, so it does not by itself give the desired horizon-free rate. A full proof needs scale-sensitive complexity, probability, and integration infrastructure. For Product ERM, coordinate independence must be explicit: the groups in the partition need not be independent of each other. The expected comparison transfers upper bounds; it cannot reverse direction to transfer a GE lower bound.

Formalization scope and conventions

The shared environment is Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Demand and policy coordinates are bounded real subtypes with their usual measurable structures. Probability is over IID whole trajectories. Finite maximum indices are nonempty. Positive $T,N,U$ prevent zero denominators in the targets. General definitions remain total, and their behavior outside these hypotheses is exposed in the independent read-backs.

Complete proofs must establish the boundedness and measurability needed for the real suprema and integrals to have their usual meaning. They may not assume the convergence bound, replace arbitrary probability measures by finite-support distributions, or silently restrict the policy class. The $(s,S)$ branch additionally needs explicit unbounded-domain conventions when holding or backlogging costs vanish. Reusable contributions include shattering, symmetrization, entropy bounds, selection and integrability facts, and finite-product sampling.

Selected references

Yaqi Xie, Will Ma and Linwei Xin, VC Theory for Inventory Policies, arXiv:2404.11509v3, 2026. https://arxiv.org/abs/2404.11509v3
Hanzhang Qin, David Simchi-Levi and Ruihao Zhu, Information Limits of Multistage Inventory Control: Learning, Valuation, and Censoring, arXiv:2609.37380v1, 2026. https://arxiv.org/abs/2609.37380v1

6 thms2 active usersReviewed

Completed

Machine Learning Operations Research Optimization·Captain: mikedeng1

Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming 3: The Two-Phase RSG Method Finds an (ε, Λ)-Solution within S(Λ)[N(ε) + T(ε, Λ)] Oracle CallsResearch Paper

Motivation

Stochastic optimization methods often see only noisy gradients. For a nonconvex objective, a useful guarantee is that an output point has a small gradient: this is a first-order stationarity certificate, even when there is no claim that the point is globally optimal. A guarantee on the expected squared gradient leaves open how often one particular run succeeds. The two-phase randomized stochastic gradient method of Ghadimi and Lan (2013) addresses that question by generating several candidates and using further oracle calls to select one. The paper gives an explicit bound on the probability of failure and on the number of oracle calls needed for a prescribed accuracy and confidence.

The work sits within stochastic approximation, where the objective may be a population expectation or another function accessible through noisy observations. The 2013 paper develops first- and zeroth-order methods for smooth nonconvex problems. This mission concerns its two-phase first-order result, Theorem 2.4, rather than the Gaussian smoothing results in its later section. The source for every index here is the arXiv v1 preprint; the printed page and PDF page coincide.

Setting

The objective is a differentiable function $f:\mathbb R^n\to\mathbb R$ bounded below, with true optimal value $f^*=\inf_x f(x)$ . Its gradient map $g=\nabla f$ is $L$ -Lipschitz: $\|g(y)-g(x)\|\le L\|y-x\|$ for all $x,y$ . The mission uses $L>0$ . No convexity is assumed.

A stochastic first-order oracle returns a vector $G(x_k,\xi_k)$ when called at the current iterate $x_k$ . Assumption A1 says that the oracle is unbiased at that iterate and has squared error of expectation at most $\sigma^2$ . The noise may depend on earlier calls. In the formal model, the mean is conditional on the past, and the oracle and squared-error random variables are integrable. This makes explicit the probabilistic assumptions used when the paper takes expectations. The model takes $\sigma>0$ because the paper's displayed stepsize and post-optimization sample size otherwise degenerate under Lean's total division convention.

A randomized stochastic gradient run starts at $x_1$ and uses $x_{k+1}=x_k-\gamma_k G(x_k,\xi_k)$ . It chooses an output index $R\in\{1,\ldots,N\}$ with the probability mass function in equation (2.3), independently of that run's oracle noise, and outputs $x_R$ . For a parameter $\widetilde D>0$ , the constant stepsize in equation (2.13) is $\gamma_k=\min\{1/L,\widetilde D/(\sigma\sqrt N)\}$ . The paper writes $D_f=\sqrt{2(f(x_1)-f^*)/L}$ and

\mathcal B_N=\frac{LD_f^2}{N}+\left(\widetilde D+\frac{D_f^2}{\widetilde D}\right)\frac{\sigma}{\sqrt N}.

The two-phase method makes $S$ independent RSG runs, yielding $\bar x_1,\ldots,\bar x_S$ . For each candidate it averages $T$ fresh oracle outputs into an estimated gradient $\widehat g_s$ . It selects a candidate $\bar x^*$ whose estimated-gradient norm is minimal. The post-optimization samples for different candidates may be recycled; the paper explicitly permits this. The candidate itself is known when its post-optimization samples are taken, so the conditional oracle assumption is stated relative to a filtration that contains it at time zero.

Formalization targets

The first target is the one-run mean bound of Corollary 2.2, $L^{-1}\mathbb E\|g(x_R)\|^2\le\mathcal B_N$ , followed by the one-run tail bound (2.19). Lemma 2.3(a) controls the squared norm of a sum of vector martingale differences. Equation (2.28) relates a selected candidate's true gradient to the best candidate and the estimation errors. Equation (2.29) factors the probability of simultaneous failure across independent runs and bounds it, while (2.30) bounds the other source of failure: every optimization run performing poorly, and at least one estimated gradient being inaccurate.

For arbitrary positive $S,N,T$ , Theorem 2.4(a) states the stronger quantitative tail bound

\Pr\left\{\|g(\bar x^*)\|^2\ge2\left(4L\mathcal B_N+\frac{3\lambda\sigma^2}{T}\right)\right\}\le\frac{S+1}{\lambda}+2^{-S}\qquad(\lambda>0).

The goal, Theorem 2.4(b), specializes those parameters to an accuracy $\varepsilon>0$ and failure probability $0<\Lambda<1$ . It sets

S=\left\lceil\log_2\frac2\Lambda\right\rceil,\qquad N=\left\lceil\max\left\{\frac{32L^2D_f^2}{\varepsilon},\left(\frac{32L(\widetilde D+D_f^2/\widetilde D)\sigma}{\varepsilon}\right)^2\right\}\right\rceil,\qquad T=\left\lceil\frac{24(S+1)\sigma^2}{\Lambda\varepsilon}\right\rceil.

An $(\varepsilon,\Lambda)$ -solution is a point satisfying $\Pr\{\|g(\bar x^*)\|^2\le\varepsilon\}\ge1-\Lambda$ . With those parameter values, the method computes such a point using at most $S(N+T)$ stochastic first-order oracle calls. The formulas and constants above are those of equations (2.24)–(2.27) of the preprint.

Significance

The result turns a mean stationarity bound into a confidence guarantee for one returned point, with an explicit accounting of both candidate generation and candidate assessment. It identifies how the number of independent runs, iterations per run, and gradient estimates scale with the requested accuracy and failure probability. Without the post-optimization phase, the paper's direct Markov estimate (2.19) gives a less favorable dependence on the failure probability for a single run.

The mathematical theorem is proved in the 2013 paper; the Lean declarations in this proposal are statements awaiting machine-checked proofs. A completed formalization would give reusable definitions for a dependent-noise gradient oracle, a random-output stochastic-gradient run, and a post-optimization selection procedure. The vector martingale estimate and finite-candidate inequality could also serve later stochastic-optimization developments. Contributions to the probability and measurability infrastructure, as well as the final rate proof, are within scope.

Difficulty

Selecting the candidate with the smallest estimated gradient need not select the one with the smallest true gradient. The estimates are random and are evaluated at candidates that are themselves random outputs of earlier oracle runs. A bound for a fixed point does not address this dependence. The argument needs a conditional oracle contract at each candidate and a separate guarantee that the optimization runs supply a sufficiently good candidate. The paper's intermediate display (2.31) applies a fixed-candidate tail estimate to the selected candidate even though the selection examines the same estimates; that step is not justified by the stated assumptions. The final bound can be phrased without treating (2.31) as a separate target.

Formalization scope

The space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Iterations and oracle samples retain the paper's one-based indexing; candidate runs use Fin S, which reindexes the paper's $1,\ldots,S$ . The objective's true infimum is carried by IsGLB (Set.range f) fstar, so $D_f$ cannot be weakened by substituting an arbitrary lower bound. Each candidate is generated by the RSG recursion and the mass function (2.3); the one-run performance bound is a theorem, not a hypothesis of the two-phase model. Independent candidate outputs are required for (2.29). The selected candidate may be any minimizer of the estimated-gradient norm, with any tie rule; no measurability of the selection is assumed.

All expectations are Bochner integrals, with integrability included in the oracle assumptions and in the one-run conclusion. Probabilities are ℝ≥0∞ values. The noise carrier is generalized from the paper's Borel subsets of Euclidean space to a measurable type. The general vector martingale lemma omits the paper's Polish-space and trivial-time-zero conditions; neither is needed for its squared-norm bound, and the latter would conflict with a candidate known at time zero. Its non-strict tail statement is restricted to a positive sum of variance bounds, because the printed version is false when every bound is zero. The goal reads the logarithm in (2.24) as base two, matching the paper's final $2^{-S}\le\Lambda/2$ comparison. Positive $\sigma$ and $\widetilde D$ avoid zero steps and an empty post-optimization average.

The formal goal states the probability guarantee. The $S(N+T)$ oracle-call bound follows directly from the algorithm's two loops and is recorded in the theorem's prose rather than in a separate operational semantics for calls. A complete proof may use Mathlib's conditional expectations, independent random variables, finite sums, and real logarithm and ceiling libraries. No assumption may simply postulate the one-run gradient bound or the final success probability.

Selected references

Saeed Ghadimi and Guanghui Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. arXiv:1309.5549v1.

11 thms2 active usersReviewed

Missions

Linear-Quadratic Optimal Control Problems for Mean-Field Stochastic Differential Equations: Two Riccati Equations Give the Optimal State-Feedback Control and the Value ⟨Π(0)x, x⟩Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 (p. 2827)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Algorithms for #BIS-Hard Problems on Expander Graphs 4: On Almost Every Δ-Regular Bipartite Graph with Δ ≥ Cq² log² q, Proper q-Colorings Reduce to Kotecký–Preiss Polymer ModelsResearch Paper

Motivation

Setting

Formalization targets

Goal: the deterministic core of Theorem 5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Distance Covariance in Metric Spaces 1: On Spaces of Strong Negative Type, Zero Distance Covariance Forces a Product MeasureResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.11

Milestones

Significance

Difficulty

Formalization scope

Selected references

Dynamic Assortment Personalization in High Dimensions 2: The Empirical Type Frequencies Satisfy ‖μ̂ − μ⋆‖_q ≤ min{8√((τ+m)/N), m^{1/q}√((τ+log 2m)/(2N))} with Probability at Least 1 − e^{−τ}Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 18)

Milestones (proof of Theorem 4, p. 44)

Significance

Difficulty

Formalization scope

Selected references

Algorithms for #BIS-Hard Problems on Expander Graphs 3: On Almost Every Δ-Regular Bipartite Graph, the Hard-Core Model at λ > 50 log²Δ/Δ Reduces to Two Kotecký–Preiss Polymer ModelsResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Distributionally Robust Convex Optimization IV: An Absolute Mean Spread Bound Describes Exactly the z̃-Marginals of a Lifted Ambiguity SetResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (Absolute Mean Spread), pp. 17–18

Milestones

Significance

Difficulty

Formalization scope

Selected references

Distributionally Robust Convex Optimization II: The Naïve Approximation Implies the Infimal Convolution Bound, Which Implies the Distributionally Robust ConstraintResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 13)

Milestones (proof of Theorem 3, p. 37; Proposition 1, p. 14)

Significance

Difficulty

Formalization scope

Selected references

Robustness May Be at Odds with Accuracy 1: Every Classifier with Standard Accuracy ≥ 1 − δ Has ℓ∞ Robust Accuracy ≤ pδ/(1 − p) Against ε ≥ 2ηResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.1 (p. 5)

Milestones (App. C, pp. 14–16)

Companion statements (§2.1, pp. 4–5)

Significance

Difficulty

Formalization scope