Completed

An Introduction to Stochastic PDEs I: The Cameron–Martin TheoremTextbook

Motivation

A stochastic partial differential equation is driven by noise that lives on an infinite-dimensional function space, and the first object one has to control is the law of that noise: a Gaussian measure on a separable Banach space. Martin Hairer's lecture notes An Introduction to Stochastic PDEs (arXiv:0907.4178) devote their first technical chapter (Section 4) to exactly this, because every later construction — stochastic convolutions, invariant measures for semilinear equations, the ergodic theory of the stochastic Navier–Stokes equations — is phrased against it.

The single structural fact that chapter produces is the Cameron–Martin theorem (Theorem 4.44, p. 31). It answers the question: in which directions may one translate an infinite-dimensional Gaussian measure without destroying its null sets? In finite dimensions the answer is "all of them", because Lebesgue measure is translation invariant. In infinite dimensions the admissible directions form a proper, and typically much smaller, Hilbert subspace $H_\mu \subset B$ — the Cameron–Martin space — and the translated measure is either equivalent to $\mu$ or mutually singular with it, with nothing in between. This dichotomy is the reason Girsanov-type changes of measure, Schilder-type large deviation rate functions, support theorems and Malliavin calculus all take the form they do.

Setting

Throughout, $B$ is a separable Banach space, $B^{*}$ its topological dual, and $\mu$ a Borel probability measure on $B$ .

$\mu$ is Gaussian (Definition 4.4, p. 19) if for every continuous linear functional $\ell \in B^{*}$ the push-forward $\ell_{*}\mu$ is a Gaussian measure on $\mathbb R$ in the sense of Definition 4.1, i.e. has characteristic function $\exp(-\tfrac{\sigma}{2}\ell^{2} + i\ell m)$ ; the degenerate case $\sigma = 0$ , a Dirac mass, is included. It is centred if all these one-dimensional laws have mean zero, which is expressed here as $\int_B x \, \mu(dx) = 0$ .

For a centred Gaussian $\mu$ the covariance form (4.2, p. 20) is

C_\mu(\ell, \ell') \;=\; \int_B \ell(x)\,\ell'(x)\, \mu(dx), \qquad \ell, \ell' \in B^{*} .

It is well defined because $\|x\|^{2}$ is $\mu$ -integrable, and it is a bounded bilinear form (Corollary 4.14, p. 22).

The Cameron–Martin space (Definition 4.26, p. 27) is classically built as the completion of

\mathring H_\mu \;=\; \{\, h \in B : \exists\, h^{*} \in B^{*} \text{ with } C_\mu(h^{*}, \ell) = \ell(h) \ \ \forall \ell \in B^{*} \,\}

under $\|h\|_\mu^{2} = C_\mu(h^{*}, h^{*})$ . This mission uses the equivalent intrinsic description of Exercise 4.38 (p. 29), which avoids the completion:

\|h\|_\mu \;=\; \sup\{\, \ell(h) \;:\; \ell \in B^{*},\ C_\mu(\ell, \ell) \le 1 \,\}, \qquad H_\mu = \{\, h \in B : \|h\|_\mu < \infty \,\} .

The supremum is taken in $[0, \infty]$ ; since $-\ell$ is admissible whenever $\ell$ is, it equals $\sup |\ell(h)|$ over the same set. For $h \in B$ write $T_h : B \to B$ , $T_h(x) = x + h$ .

Formalization targets

Goal — Theorem 4.44 (Cameron–Martin)

For a centred Gaussian measure $\mu$ on a separable Banach space $B$ and $h \in B$ ,

(T_h)_{*}\mu \ \ll \ \mu \qquad \Longleftrightarrow \qquad h \in H_\mu .

Both implications are asserted: translation along a Cameron–Martin direction produces an absolutely continuous measure, and translation along any other direction does not (in fact it produces a mutually singular measure).

Milestones

The milestone list follows the route of Section 4.2:

Exercise 4.38 — the supremum description agrees with Definition 4.26 on $\mathring H_\mu$ .
Proposition 4.32 — $H_\mu \subset B$ with $\|h\|^{2} \le \|C_\mu\| \, \|h\|_\mu^{2}$ .
Proposition 4.40 — every $L^{2}(\mu)$ -limit of elements of $B^{*}$ has a centred Gaussian law whose variance is its own $L^2$ norm squared.
Equation (4.14) — the explicit density $D_h(x) = \exp(h^{*}(x) - \tfrac12\|h\|_\mu^{2})$ of the shifted measure, for $h \in \mathring H_\mu$ .
The total-variation separation bound $\|\mathcal N(0,1) - \mathcal N(m,1)\|_{\mathrm{TV}} \ge 2 - 2e^{-m^{2}/8}$ used in the converse half of Theorem 4.44.
Proposition 4.45 — $H_\mu$ is exactly the intersection of all measurable linear subspaces of full measure.

Significance

The Cameron–Martin theorem is what makes the Cameron–Martin space a canonical object rather than a formal construction: $H_\mu$ is simultaneously the set of admissible shifts, the intersection of all full-measure linear subspaces (Proposition 4.45), and the space whose unit ball governs Gaussian isoperimetry (Theorem 4.53, Borell–Sudakov–Cirel'son). Downstream in the notes it is used to identify invariant measures of linear SPDEs and to compare them; outside the notes it is the starting point of Malliavin calculus and of large deviation theory for Gaussian measures.

Status, precisely. The Mathlib library pinned by this mission already contains a substantial part of Section 4: the predicate IsGaussian (Definition 4.4), uniqueness of measures with equal characteristic functionals on a separable Banach space (Propositions 4.8 and 4.11), invariance of $\mu \otimes \mu$ under rotations (Proposition 4.12), Fernique's theorem (Theorem 4.13), and the covariance form of (4.2) together with its boundedness (Corollary 4.14) as a continuous bilinear form on the dual. Those results are therefore not milestones here; they are the assumed foundation. What is absent, and what this mission asks for, is everything from the Cameron–Martin space onwards: its definition, its elementary properties, and Theorem 4.44 itself. No machine-checked proof of the infinite-dimensional Cameron–Martin theorem is known to the captain in any Lean library.

Difficulty

The naive route — write down the two densities and take their ratio — is unavailable: there is no translation-invariant reference measure on an infinite-dimensional Banach space, so "the density of $\mu$ " does not exist and the Radon–Nikodym derivative of $(T_h)_{*}\mu$ with respect to $\mu$ must be produced directly, as the exponential of a random variable.

That random variable is the obstruction. For $h \in \mathring H_\mu$ the functional $h^{*}$ is continuous and the computation is a characteristic-function identity. But $\mathring H_\mu$ is in general strictly smaller than $H_\mu$ : a general $h \in H_\mu$ has an associated $h^{*}$ that exists only as an $L^{2}(\mu)$ -limit of continuous functionals, defined $\mu$ -almost everywhere and linear only on a measurable subspace of full measure (Propositions 4.34 and 4.39). Establishing that these limits are Gaussian with the expected variance (Proposition 4.40) is the technical bridge, and it is why milestone 3 is stated as a statement about $L^{2}$ -limits rather than about elements of $B^{*}$ .

The converse half has a different shape. One must produce, for $h \notin H_\mu$ , a single one-dimensional projection that separates $\mu$ from $(T_h)_{*}\mu$ arbitrarily well; unboundedness of $\ell(h)$ over the covariance unit ball supplies $\ell$ with $C_\mu(\ell,\ell) = 1$ and $\ell(h)$ as large as desired, and the quantitative Gaussian total-variation bound of milestone 5 converts this into total variation distance $2$ , i.e. mutual singularity.

Formalization scope

The development is in Lean 4 with Mathlib, in the namespace HairerSPDE, shared by the whole series drawn from these notes. The conventions it commits to:

$B$ carries NormedAddCommGroup, NormedSpace ℝ, its Borel σ-algebra, CompleteSpace and SecondCountableTopology — the last two encode "separable Banach space".
Gaussianity is Mathlib's IsGaussian, which is Definition 4.4 verbatim; centredness is the extra hypothesis $\int x \, d\mu = 0$ , needed because IsGaussian permits a non-zero mean.
The covariance form is Mathlib's covarianceBilinDual, which equals (4.2) for centred measures with finite second moment and is set to zero otherwise; Fernique's theorem rules the degenerate branch out for Gaussian measures.
The Cameron–Martin norm is the $[0,\infty]$ -valued supremum above, so membership in $H_\mu$ is finiteness of that supremum; this is the only new definition the mission publishes.
Translation is fun x ↦ x + h, absolute continuity is Mathlib's ≪, and "measurable linear subspace" is a Submodule ℝ B whose carrier is a measurable set.

The goal is an equivalence, so neither half can be discharged vacuously: the direction $h \in H_\mu \Rightarrow (T_h)_*\mu \ll \mu$ is non-trivial already for $h \ne 0$ in finite dimensions, and the converse has content precisely when $H_\mu \ne B$ . Note that $\|0\|_\mu = 0$ always, and that for $\mu$ a Dirac mass the covariance form vanishes and $H_\mu = \{0\}$ ; both degenerate cases are inside the statement rather than excluded by hypothesis.

Contributions welcome beyond the milestones: the reproducing kernel space $R_\mu$ and the isomorphism of Proposition 4.34, measurable linear extensions (Proposition 4.39), the dilation singularity of Proposition 4.43, and $\mu(H_\mu) = 0$ in the infinite-dimensional case (second half of Proposition 4.45). All of these are reusable outside this mission.

Selected references

M. Hairer, An Introduction to Stochastic PDEs, lecture notes, 2009/2023. arXiv:0907.4178
V. I. Bogachev, Gaussian Measures, Mathematical Surveys and Monographs 62, American Mathematical Society, 1998. DOI:10.1090/surv/062
X. Fernique, Intégrabilité des vecteurs gaussiens, C. R. Acad. Sci. Paris Sér. A-B 270 (1970), A1698–A1699.
G. Da Prato, J. Zabczyk, Stochastic Equations in Infinite Dimensions, Cambridge University Press, 1992. DOI:10.1017/CBO9780511666223

21 thms4 active usersReviewed

Completed

Control Theory Dynamic Programming Operations Research·Captain: Shuze Chen

Dynamic Programming and Optimal Control V: LQG and Certainty EquivalenceTextbook

Motivation

The separation theorem — certainty equivalence for linear-quadratic control with imperfect state information — is one of the celebrated structural results of stochastic control: the optimal controller splits into a least-squares estimator and the deterministic LQR actuator, designed independently. It underlies every LQG autopilot and Kalman-filter-based regulator. Section 5.2 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) proves it from the DP algorithm over information vectors, with Lemma 5.2.1 supplying the key fact that the estimation error is beyond the controller's influence. No formal analogue exists in Mathlib.

Setting

Linear dynamics and measurements

x_{k+1} = A_k x_k + B_k u_k + w_k, \qquad z_k = C_k x_k + v_k,

with quadratic cost $\mathbb{E}\big[x_N^\top Q_N x_N + \sum_{k<N}(x_k^\top Q_k x_k + u_k^\top R_k u_k)\big]$ , $Q_k \succeq 0$ , $R_k \succ 0$ . The initial state and the zero-mean disturbances/noises are independent with finite ranges; independence is structural — the sample space is the product of an initial-state coordinate and per-stage noise coordinates (BertsekasLQGModel, BertsekasLQGSample, BertsekasLQGProb). A policy maps the realized measurement history $(z_0,\dots,z_k)$ to $u_k$ ; the closed-loop process is BertsekasLQGTraj, the expected cost BertsekasLQGCost. The estimator $\mathbb{E}[x_k \mid I_k]$ is an explicit conditional average (BertsekasCondExpVec, BertsekasLQGEstimate); the gains $L_k$ come from the time-varying Riccati recursion (BertsekasLQGRiccati, BertsekasLQGGain).

Target

\pi^*(I_k) = L_k\, \mathbb{E}[x_k \mid I_k] \ \text{ along its own trajectories} \quad\Longrightarrow\quad J(\pi^*) \le J(\pi)\ \ \forall \pi,

— BertsekasDP.lqg_certainty_equivalence (goal). Milestone: Lemma 5.2.1 in pointwise form — the error $x_k - \mathbb{E}[x_k \mid I_k]$ is the same under any two policies, outcome by outcome (lqg_estimation_error_policy_independent).

Significance

This is the theorem that justifies designing estimator and controller separately — remove it and the entire LQG methodology loses its warrant. The formalization also yields the first machine-checked instance of the informational decomposition (control-dependent part + policy-independent error) that recurs throughout imperfect-information control. Notably the result needs no Gaussian assumption — only zero mean and independence — and the finite-support model makes that generality exact. The result is classical (Joseph–Tou 1961, Gunckel–Franklin 1963; the book's §5.2); the formal proof is new.

Difficulty

The heart is Lemma 5.2.1: showing the estimation error coincides, sample by sample, with the error of the control-free system — which requires proving that the observation-history σ-events under any policy coincide with those of the control-free system (controls are determined by the history, so they shift observations by a known amount). Then the DP argument over information histories must carry the quadratic decomposition through the backward recursion. Bookkeeping over histories-as-lists is the main formal burden; probability theory stays finite.

Formalization scope

Finite-support randomness (all expectations are finite sums); conditional expectation with the explicit junk value 0 on zero-probability events — the goal's hypothesis is accordingly restricted to outcomes of positive probability. Policies are functions of the measurement list only (equivalent to the book's information vector for deterministic policies, since past controls are recoverable from past measurements). Matrices are time-varying; positive definiteness of $R_k$ makes every matrix inverse in the gains genuine. Measurement noise covariance is not assumed positive definite — the estimator is the abstract conditional expectation, not the Kalman filter (whose recursive form, §5.2.1, would be a natural follow-up mission).

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§5.2, Lemma 5.2.1.) http://www.athenasc.com/dpbook.html
P. D. Joseph, J. T. Tou, On linear control theory, Trans. AIEE 80 (1961), 193–196. https://doi.org/10.1109/TAI.1961.6371743
T. L. Gunckel, G. F. Franklin, A general solution for linear sampled-data control, J. Basic Eng. 85 (1963), 197–201. https://doi.org/10.1115/1.3656559

5 thms4 active usersReviewed

Completed

Markov Chain Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times VIII: Path Coupling and Approximate CountingTextbook

Motivation

The coupling method of Mission III asks for a coupling of two copies of a chain from every pair of starting states — often painful to construct globally. Chapter 14 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) replaces that global demand by a local one. The path coupling technique of Bubley and Dyer says: put a connected graph structure on the state space, and couple one step of the chain only across edges; if each edge contracts in expectation, contraction propagates automatically along paths to arbitrary pairs of distributions. The bookkeeping runs through the transportation metric (Kantorovich distance) between distributions, whose theory — attainment by an optimal coupling, the triangle inequality — is developed on the way. The chapter's payoff is the sharpest elementary bound for sampling proper colorings (Theorem 14.8: the Glauber dynamics mixes in $O(n\log n)$ steps once $q>2\Delta$ ), and, through the sampling-to-counting reduction of Jerrum–Valiant–Vazirani, a polynomial-time approximation algorithm for counting colorings — the paradigm of the Markov chain Monte Carlo method as an algorithmic tool.

Setting

All chains live on a finite state space $V$ with a transition matrix $P$ ; $P^t(x,\cdot)$ is the time- $t$ distribution from $x$ , $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ the total variation distance, $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$ the worst-case distance to the stationary distribution $\pi$ , and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ the mixing time. A coupling of distributions $\mu,\nu$ is a distribution $q$ on $V\times V$ with marginals $\mu$ and $\nu$ .

Given a metric-like cost $\rho$ on pairs of states, the transportation metric between two distributions is the cheapest expected cost of moving one onto the other:

\rho_K(\mu,\nu)=\min\Bigl\{\sum_{x,y}\rho(x,y)\,q(x,y)\;:\;q\ \text{a coupling of}\ \mu,\nu\Bigr\}.

Given a connected graph structure $G$ on the state space with edge lengths $\ell\ge1$ , the path metric $\rho(x,y)$ is the least total length of a $G$ -path from $x$ to $y$ .

For the colorings application: a $q$ -coloring of the vertices of a graph is proper when adjacent vertices receive distinct colors, and the Glauber dynamics on proper colorings picks a uniform vertex and re-samples its color uniformly among the colors legal there; its stationary distribution is uniform on the proper colorings. Throughout, $n$ is the number of vertices and $\Delta$ the maximum degree of the graph being colored.

Formalization targets

Goal

Theorem 14.8, the capstone of Chapter 14: for the Glauber dynamics on proper $q$ -colorings, if $q>2\Delta$ then

t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{q-\Delta}{q-2\Delta}\;n\,\bigl(\log n-\log\varepsilon\bigr)\Bigr\rceil.

Milestones

Lemma 14.3 and Remark 14.2 — the transportation distance is attained by an optimal coupling, and satisfies the triangle inequality (so it is a genuine metric on distributions).
Theorem 14.6, path coupling (Bubley–Dyer) — if for every edge $\{x,y\}$ of a connected graph structure there is a coupling of the one-step distributions $P(x,\cdot),P(y,\cdot)$ contracting the path metric by $e^{-\alpha}$ in expectation, then one step of the chain contracts the transportation metric of arbitrary distribution pairs by $e^{-\alpha}$ .
Corollary 14.7 — under the same hypotheses, $d(t)\le e^{-\alpha t}\,\mathrm{diam}(V)$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil(\log\mathrm{diam}(V)-\log\varepsilon)/\alpha\rceil$ , where $\mathrm{diam}(V)$ is the largest path-metric distance between two states.
Theorem 14.12, approximate counting — for $q>2\Delta$ there is a randomized estimator, computed from an explicit polynomial number of independent uniform random seeds, which with probability at least $1-\eta$ estimates the number of proper $q$ -colorings within a $(1\pm\varepsilon)$ factor: rapid sampling yields rapid approximate counting.

Significance

The results. Path coupling converted the coupling method from an art into a calculus: one bounds a single-edge contraction constant, and the machinery does the rest. It is the standard tool for Glauber dynamics on colorings, independent sets, and other constraint-satisfaction models, and the $q>2\Delta$ colorings bound is its flagship application. Theorem 14.12 is the discrete embodiment of the Jerrum–Valiant–Vazirani equivalence between approximate counting and sampling — the conceptual foundation of the entire MCMC approach to $\#\mathrm P$ -hard counting problems.

Formalizing them. Mathlib has no transportation/Kantorovich metric in the finite setting, no path coupling, and nothing on approximate counting. The transportation-metric layer (optimal couplings, triangle inequality) is reusable far beyond this mission — it is the finite Wasserstein distance. The path-coupling theorem feeds directly into Mission IX (Ising) and is quoted throughout modern mixing literature.

Difficulty

The transportation metric asks for minimization over the (compact) polytope of couplings: attainment is a finite-dimensional compactness argument, and the triangle inequality requires gluing two optimal couplings along their common marginal — the classic construction that must be carried out with explicit finite sums here. Path coupling itself is an induction along geodesics of the path metric, with the subtlety that the composite coupling produced along a path need not be optimal, only admissible; the bookkeeping of the contraction constant through the induction is exactly the kind of argument Lean keeps honest. Theorem 14.8 instantiates the machinery: the single-edge coupling for colorings needs a careful case analysis of the proposed recolorings at the two endpoints (matching legal colors bijectively), and the contraction constant $(q-2\Delta)/(q-\Delta)$ emerges from counting disagreeing proposals. Theorem 14.12 layers a probabilistic-amplification argument (medians of means over independent runs) on top of the mixing bound; its combinatorial core — expressing $|\Omega|^{-1}$ as a telescoping product of marginal probabilities — is elementary but notation-heavy, and the formal statement quantifies over explicit seed spaces, so the whole estimator is a finite object.

Formalization scope

The transportation metric is an sInf over coupling costs (the coupling polytope is nonempty for genuine distributions, and attainment is part of the milestone, so the junk value never propagates); the path metric is an sInf over walk lengths in a connected graph. The Glauber dynamics on colorings is the restriction to proper colorings of the single-site heat-bath chain of Mission II, matching §3.3 of the book; its state space is the subtype of proper colorings, nonempty whenever $q>2\Delta$ (a fact the hypotheses of the goal supply). Mixing-time upper bounds are stated with the book's explicit ceilings, so no rounding slack is hidden. In Theorem 14.12 the estimator is presented concretely as a function of finitely many uniform seeds, and "with probability $\ge1-\eta$ " is a counting inequality over the seed space — no measure theory enters. Contributions of intermediate lemmas (optimal-coupling gluing, geodesic decompositions, colorings edge-coupling) are welcome and will be reused by Mission IX.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
R. Bubley, M. Dyer, Path coupling: a technique for proving rapid mixing in Markov chains, FOCS 1997. https://doi.org/10.1109/SFCS.1997.646111
M. Jerrum, A very simple algorithm for estimating the number of k-colorings of a low-degree graph, Random Structures Algorithms 7 (1995). https://doi.org/10.1002/rsa.3240070205
M. Jerrum, L. Valiant, V. Vazirani, Random generation of combinatorial structures from a uniform distribution, Theoret. Comput. Sci. 43 (1986). https://doi.org/10.1016/0304-3975(86)90174-X

9 thms4 active usersReviewed

Completed

Markov Chain Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times VI: Networks, Hitting Times, and Cover TimesTextbook

Motivation

A reversible Markov chain is an electrical network: states are nodes, and the conductance $c(x,y)=\pi(x)P(x,y)$ turns hitting probabilities into voltages and hitting times into resistances. This dictionary, going back to Kakutani and popularized by Doyle and Snell, converts probabilistic estimates into the physical laws of circuits — series/parallel reduction, energy minimization, monotonicity under edge removal. Chapters 9–11 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the dictionary and its two crown results: the commute time identity of Chandra–Raghavan–Ruzzo–Smolensky–Tiwari, $\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)=c_G\,R(a\leftrightarrow b)$ , and the Matthews method bounding cover times by hitting times with harmonic-number precision.

Setting

A network is a symmetric nonnegative conductance function $c$ on pairs of vertices; the associated walk moves with probabilities

P(x,y)=c(x,y)/c(x)

where $c(x)=\sum_y c(x,y)$ , and $c_G=\sum_x c(x)$ . A function $h$ is harmonic at $x$ if $h(x)=\sum_y P(x,y)h(y)$ . The voltage with boundary values $1$ at $a$ and $0$ at $z$ is $W(x)=\mathbb P_x\{\tau_a<\tau_z\}$ , the harmonic extension of its boundary data; the current flowing out of $a$ has strength $\|I\|=\sum_y c(a,y)\,[W(a)-W(y)]$ , and the effective resistance is $R(a\leftrightarrow z)=\|I\|^{-1}$ . A flow from $a$ to $z$ is an antisymmetric edge function obeying the node law off $\{a,z\}$ ; its energy is $\mathcal E(\theta)=\sum_e\theta(e)^2/c(e)$ . Hitting times $\tau_S=\min\{t\ge0:X_t\in S\}$ , their expectations, the Green's function $G_{\tau_z}(a,x)$ , the maximal hitting time $t_{\mathrm{hit}}$ , and the cover time $t_{\mathrm{cov}}$ (expected time to visit every state, maximized over starts) all use the trajectory calculus of Mission I.

Formalization targets

Goal

\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)\;=\;c_G\,R(a\leftrightarrow b).

This is Proposition 10.6, the commute time identity — the exact bridge between the probabilistic and electrical sides, and the engine of the transience/recurrence theory of Mission XII.

Milestones

Reversibility and stationarity of the network walk with $\pi(x)=c(x)/c_G$ (§9.1); Proposition 9.1 (existence and uniqueness of harmonic extensions with given boundary values, $h(x)=\mathbb E_x f(X_{\tau_B})$ ); Lemma 9.6 (the Green's function identity $G_{\tau_z}(a,a)=c(a)R(a\leftrightarrow z)$ ); Theorem 9.10 (Thomson's principle: $R(a\leftrightarrow z)$ is the minimal energy of a unit flow, attained); Theorem 9.12 (Rayleigh monotonicity: lowering conductances raises effective resistance); Lemma 10.1 (the random target lemma: $\sum_y\mathbb E_a(\tau_y)\pi(y)$ does not depend on $a$ ); Corollary 10.8 (the resistance triangle inequality); Theorem 11.2 (Matthews: $t_{\mathrm{cov}}\le t_{\mathrm{hit}}\,(1+\tfrac12+\dots+\tfrac1n)$ ); Proposition 11.4 (the matching Matthews lower bound over subsets).

Significance

The results. The commute time identity computes hitting times from circuit reductions — this is how hitting times on trees, tori and glued graphs are actually evaluated — and, through Thomson and Rayleigh, makes them monotone under graph operations, something invisible probabilistically. The Matthews bounds pin cover times up to a $\log n$ factor in complete generality; they are the tool behind cover-time results for lamplighter groups in Mission XI's sequel. Green's function identities feed Mission XII's recurrence theory, where $R(a\leftrightarrow\infty)$ decides transience.

Formalizing them. Mathlib has graph Laplacians but no electrical network theory: no effective resistance, no flows, no energy, no Thomson/Rayleigh, no hitting or cover times. This mission publishes that layer over the trajectory calculus of Mission I. It is the most reusable single block of the series outside Missions I–II: effective resistance on finite networks is of independent interest to combinatorics (spanning trees, spectral sparsification) well beyond mixing times.

Difficulty

The identity chain behind the goal runs: Green's function of the stopped walk $\to$ escape probability $\mathbb P_a\{\tau_z<\tau_a^+\}=\bigl(c(a)R(a\leftrightarrow z)\bigr)^{-1}$ (via harmonic uniqueness) $\to$ the Aldous–Fill occupation identity $G_\tau(a,x)=\mathbb E_a(\tau)\pi(x)$ for stopping times with $X_\tau=a$ — each step is a manipulation of infinite series of trajectory sums whose exchange steps (splitting a path at its first visit, last-exit decompositions) need summability from Mission I's Lemma 1.13. Thomson's principle is a finite-dimensional convex minimization: existence of the minimizer needs a compactness or completing-the-square argument, and the identification of the minimizer with the current flow needs the cycle law; the naive "differentiate the energy" route must be made exact. Matthews' method is a clean but genuinely clever argument — a uniformly random ordering of targets and the harmonic-number telescoping; the formal cost is the exchangeability of the randomized order against the chain, handled combinatorially.

Formalization scope

Networks are functions $c:V\times V\to\mathbb R$ with a symmetry-and-nonnegativity predicate; loops are permitted; connectivity enters as irreducibility of the induced walk. The voltage is defined probabilistically as $\mathbb P_x\{\tau_a<\tau_z\}$ (the book's harmonic characterization is Proposition 9.1); $R(a\leftrightarrow z)$ is the reciprocal of the explicit current strength, with total division junk when $a,z$ are disconnected — statements carry irreducibility so this does not arise. Energy counts each undirected edge once, formalized as half the ordered double sum, and $0^2/0=0$ handles absent edges. Cover times are tail sums of the explicit event "some state unvisited". The Matthews lower bound is stated with an arbitrary lower bound $m$ for the pairwise hitting times of the subset $A$ — equivalent to the book's min over pairs and easier to instantiate.

Welcome contributions: series/parallel reduction laws, the cycle and node law API for flows, escape-probability lemmas — all reused in Mission XII's infinite-network arguments.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
P. G. Doyle, J. L. Snell, Random Walks and Electric Networks, MAA, 1984. https://arxiv.org/abs/math/0001057
A. K. Chandra, P. Raghavan, W. L. Ruzzo, R. Smolensky, P. Tiwari, The electrical resistance of a graph captures its commute and cover times, STOC 1989. https://doi.org/10.1145/73007.73062
P. Matthews, Covering problems for Markov chains, Ann. Probab. 16 (1988). https://doi.org/10.1214/aop/1176991894

15 thms4 active usersReviewed

Completed

Experimental Design Operations Research Reinforcement Learning+1·Captain: Shuze Chen

Treatment Locality in A/B TestingResearch Paper

Modern A/B tests must infer lifetime treatment effects — e.g. customer lifetime value under a new feature — from short-horizon experiment data. Chen, Simchi-Levi and Wang (arXiv:2407.19618) model the experiment as a Markov decision process and exploit a structural fact of many practical interventions: the treatment is local, modifying the system at a single crucial state only. This mission formalizes the core asymptotic theory of the paper: for any differentiable estimator built from the experiment's transition and reward statistics, information sharing — pooling across test arms the samples collected away from the treated state — keeps the estimator asymptotically normal with the same asymptotic bias and never increases its asymptotic variance (Theorem 9), and is asymptotically efficient among unbiased estimators (Theorem 5). The route runs through a Markov chain central limit theorem with the asymptotic variance identified as the autocovariance series, and the linearization/delta method for functionals of chain statistics.

42 thms4 active users

Completed

Markov Chain Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary DistributionTextbook

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary Distribution

Motivation

Finite Markov chains are the basic model for memoryless random dynamics: card shuffles, random walks on graphs and groups, Monte Carlo samplers, and queueing systems are all chains on a finite state space. The single most used fact about them is that an irreducible chain has exactly one stationary distribution — a probability vector $\pi$ with $\pi = \pi P$ — and that this $\pi$ is strictly positive and encodes the long-run behaviour of the chain through the return-time identity $\pi(x) = 1/\mathbb{E}_x(\tau_x^+)$ . Every later result in the theory of mixing times (convergence theorems, coupling bounds, spectral methods, cutoff) is a statement about the distance of the chain from this $\pi$ , so nothing in the subject can be formalized before this mission is.

This mission is the first in a series formalizing D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times (AMS, 2009), covering Chapters 1–2: the basic vocabulary of finite chains (stochastic matrices, irreducibility, period, reversibility, time reversal, random walks on graphs and groups) and the classical examples of Chapter 2 (gambler's ruin, coupon collecting, the reflection principle for simple random walk on $\mathbb{Z}$ ). Later missions in the series build on the definitions published here.

Setting

A chain on a finite state space $\Omega$ is presented by its transition matrix, a matrix $P \in \mathbb{R}^{\Omega\times\Omega}$ with nonnegative entries whose rows sum to $1$ . A distribution is a row vector $\mu$ with nonnegative entries summing to $1$ ; one step of the chain carries $\mu$ to $\mu P$ , and the $t$ -step transition probabilities are the entries of the matrix power $P^t$ .

The chain is irreducible if for all states $x, y$ there is a $t$ with $P^t(x,y) > 0$ . The period of a state $x$ is $\gcd\,\mathcal{T}(x)$ where $\mathcal{T}(x) = \{t \ge 1 : P^t(x,x) > 0\}$ , and the chain is aperiodic if every state has period $1$ . A distribution $\pi$ is stationary if $\pi P = \pi$ , and $\pi$ and $P$ are in detailed balance (the chain is reversible) if $\pi(x)P(x,y) = \pi(y)P(y,x)$ for all $x,y$ .

Trajectory events over a finite horizon are finite sums of path weights: a length- $t$ trajectory is a function $\omega : \{0,\dots,t\} \to \Omega$ , with weight $\prod_{i<t} P(\omega_i, \omega_{i+1})$ conditional on its starting state. The tail probability $\mathbb{P}_x\{\tau_z^+ > t\}$ of the first hitting time $\tau_z^+ = \min\{t \ge 1 : X_t = z\}$ is the sum of the weights of the trajectories from $x$ that avoid $z$ at times $1,\dots,t$ , and expectations of hitting times are recovered by the tail-sum formula $\mathbb{E}(Y) = \sum_{t\ge0} \mathbb{P}\{Y > t\}$ , formalized as a tsum over $t$ .

Formalization targets

Goal

$\text{$P$ stochastic and irreducible on a finite nonempty $\Omega$} \;\Longrightarrow\; \exists!\, \pi,\ \pi = \pi P .$

This is Corollary 1.17 of the book. It asserts only existence and uniqueness, leaving the finer structure of $\pi$ to the milestones; it is the weakest statement on which the rest of the series can stand, which is why it is the goal.

Milestones toward and around the goal

The milestone list follows the book's own route: well-definedness of the period (Lemma 1.6), positivity of some matrix power for irreducible aperiodic chains (Proposition 1.7), finiteness of expected hitting times (Lemma 1.13), existence of a positive stationary distribution together with

\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1

(Proposition 1.14), constancy of harmonic functions (Lemma 1.16), stationarity from detailed balance (Proposition 1.19), the stationary and reversible measure $\pi(x) = \deg(x)/2|E|$ of simple random walk on a graph (Examples 1.12 and 1.20), the time reversal $\hat P$ and its path-reversal identity (Proposition 1.22), and the random walks on finite groups of Section 2.6 (Propositions 2.12–2.14). From Chapter 2 the list adds the gambler's ruin formulas $\mathbb{P}_k\{X_\tau = n\} = k/n$ and $\mathbb{E}_k(\tau) = k(n-k)$ (Proposition 2.1), the coupon collector expectation $n\sum_{k\le n} 1/k$ and tail bound $e^{-c}$ (Propositions 2.3 and 2.4), and the reflection principle and the bound $\mathbb{P}_k\{\tau_0 > r\} \le 12k/\sqrt{r}$ for simple random walk on $\mathbb{Z}$ (Lemma 2.18 and Theorem 2.17).

Significance

The result itself. Existence and uniqueness of $\pi$ is the pivot on which the entire quantitative theory turns: it defines the target of convergence, and the identity $\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1$ ties the stationary measure to return times, which later missions use for hitting-time and cover-time results. Detailed balance is the practical tool by which stationary measures of graph and group walks are computed, and the Chapter 2 examples (gambler's ruin, coupon collecting, reflection) are the standard building blocks reused throughout the book — the coupon collector bound, for instance, is exactly the estimate behind the $n \log n + cn$ analysis of the top-to-random shuffle in a later mission of this series.

Formalizing it. Mathlib currently has no theory of finite Markov chains: no stochastic-matrix predicate, no stationary distribution, no periodicity, no hitting times. Everything proved in this mission is new formal mathematics, and the definition layer published here (mm_basic, mm_path, mm_classical) is the shared foundation that all twelve subsequent missions of the series import. All results are classical and have textbook proofs; none has a machine-checked proof.

Difficulty

The delicate point is the existence proof. The natural first idea — extract $\pi$ from an eigenvector of $P^{\mathsf T}$ for eigenvalue $1$ , or invoke a fixed-point theorem — either does not give positivity and nonnegativity without further work, or uses compactness machinery (Brouwer) that is unavailable. The book's proof instead builds $\tilde\pi(y) = \mathbb{E}_z(\text{visits to } y \text{ before } \tau_z^+)$ and verifies $\tilde\pi P = \tilde\pi$ by reindexing trajectory sums; formalizing it requires managing infinite series of path sums (summability from the geometric tail bound of Lemma 1.13, exchanging tsum with finite sums, splitting a trajectory at its last step). The uniqueness half is linear algebra via constancy of harmonic functions (Lemma 1.16), which is elementary but requires a maximum-principle argument over a finite state space. The reflection principle and Theorem 2.17 are finite combinatorics on $\pm 1$ paths — the bijection is easy to describe and fiddly to implement.

Formalization scope

States form a Fintype with decidable equality; chains are Matrix V V ℝ with the row-stochasticity predicate IsStochastic; distributions are functions V → ℝ with the predicate IsDist. Everything is distribution-side: no probability space or measure theory is used. The period is formalized as $\sup\{d : d \mid t \text{ for all } t \in \mathcal{T}(x)\}$ , which equals $\gcd \mathcal{T}(x)$ when $\mathcal{T}(x) \neq \varnothing$ and takes the junk value $0$ otherwise. Expectations of hitting times are tsums of tail probabilities, with the usual junk value $0$ for non-summable families — the statements are arranged (e.g. multiplicatively, $\pi(x)\cdot\mathbb{E}_x(\tau_x^+) = 1$ ) so that junk values cannot make them vacuously true. Existence statements carry a Nonempty V hypothesis; irreducibility on the empty space is vacuous, and without nonemptiness the goal would be false, not trivial. The coupon collector and the walk on $\mathbb{Z}$ are presented directly by their driving randomness (uniform draws Fin t → Fin n, uniform sign strings Fin r → Bool), so those probabilities are elementary counting; in particular the reflection principle is stated as an equality of cardinalities of sets of sign strings — this is equivalent to the probabilistic statement because all $2^r$ strings are equally likely.

Contributions welcome beyond the milestone list: simp lemmas for the definition layer, the taboo-matrix representation of avoidance probabilities (useful for Lemma 1.13), and any interface lemmas connecting pathWeight sums to matrix powers — these will be reused by every later mission in the series.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
J. R. Norris, Markov Chains, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9780511810633
D. Aldous, J. A. Fill, Reversible Markov Chains and Random Walks on Graphs, 2002 (unfinished monograph). https://www.stat.berkeley.edu/~aldous/RWG/book.html

20 thms4 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Achieving High Individual Service Levels Without Safety Stock? Optimal Rationing Policy of Pooled Resources II: The Max-Weighted-Service Policy Is Almost Surely Asymptotically OptimalResearch Paper

Motivation

Firms that serve several customers from shared capacity, such as a warehouse supplying several retailers, a flexible production line building several products, or an assemble-to-order system, often sign contracts that guarantee each customer an individual service level. Typical targets are the probability of filling a customer's whole demand (Type-I), the expected fraction of demand filled (Type-II or Type-III), each required to be at least a target $\beta_j$ . Once demand is realized, the firm must decide how to ration the pooled resources among customers. Jiang, Wang and Zhang (SSRN 3385089, published in Operations Research, doi:10.1287/opre.2022.2386) ask how much capacity suffices and which rationing policy meets all targets at least cost. The exact optimal policy is an infinite-dimensional program over randomized policies, (11). This mission formalizes the paper's answer to the second question: a simple, learnable policy is asymptotically optimal.

Setting

There are $n$ customers $N=\{1,\dots,n\}$ and $m$ resources. The capacity vector $c\in\mathbb R^m_{\ge0}$ is fixed. The demand $\tilde D\in\mathbb R^n_{\ge0}$ is random with law $F$ . After observing a demand vector $D$ , the firm chooses a solution $(s,y)$ from a compact set $P(c,D)$ . Here $s_j\le D_j$ is the demand of customer $j$ that is fulfilled and $y_{ij}$ is the amount of resource $i$ given to customer $j$ . The solution costs $f(y)$ , with $f$ linear, and customer $j$ receives service $R_j(s_j,D_j)\ge0$ .

A deterministic policy $\varphi$ maps each demand vector to a feasible solution $(s(\varphi,c,D),y(\varphi,c,D))$ . A randomized policy $\lambda$ picks a deterministic policy at random.
The service level of customer $j$ under $\lambda$ is $\int E_{\tilde D}[R_j(s_j(\varphi,c,\tilde D),\tilde D_j)]\,d\lambda(\varphi)$ , and the expected cost is $\int E_{\tilde D}[f(y(\varphi,c,\tilde D))]\,d\lambda(\varphi)$ .
The capacity $c$ is feasible if some $\lambda$ meets every target $\beta_j\in(0,1)$ . $\mathrm{Obj}(11)$ is the least expected cost among such $\lambda$ .
For weights $w\in\mathbb R^n_{\ge0}$ , the Max-Weighted-Service problem (16) is $\min_{(y,s)\in P(c,D)} f(y)-\sum_j w_jR_j(s_j,D_j)$ . The policy $\varphi_w$ picks one of its optimal solutions for every $D$ .
Algorithm 1 draws independent samples $D^{(1)},\dots,D^{(T)}$ from $F$ . It starts from $w^{(1)}=0$ and updates the weights by

w^{(t+1)}_j=\Big[w^{(t)}_j+\gamma_T\big(\beta_j-R_j(s_j(\varphi_{w^{(t)}},c,D^{(t)}),D^{(t)}_j)\big)\Big]^+,\qquad \gamma_T=T^{-(1/2+\epsilon)}.

It then adopts $\varphi_w$ at a uniformly drawn iterate $w$ .

The Lean development uses the same letters: detService, detCost, IsFeasible, obj11, mwsObjective, mwsIter, stepSize, G, Gstar, Lterm.

Formalization targets

Goal: Theorem 3 (p. 17)

Under Assumptions 1 and 3, if $c$ is feasible and $\epsilon\in(0,1/2)$ , then almost surely

\limsup_{T\to\infty}\frac1T\sum_{t=1}^TE_{\tilde D^t}\big[f(y(\varphi_{w^{(t)}},c,\tilde D^t))\big]\le\mathrm{Obj}(11),\qquad \liminf_{T\to\infty}\frac1T\sum_{t=1}^TE_{\tilde D^t}\big[R_j(s_j(\varphi_{w^{(t)}},c,\tilde D^t),\tilde D^t_j)\big]\ge\beta_j\ \ \forall j.

Here $\tilde D^t$ is a fresh copy of the demand, so each expectation is taken with the iterate fixed. The statement holds for every tie-breaking rule in (16).

Milestones (pp. 52–54)

Weak duality: $\sum_jw_j\beta_j+E[f(y(\varphi_w))]-\sum_jw_jE[R_j(s_j(\varphi_w),\tilde D_j)]\le\mathrm{Obj}(11)$ for every $w\ge0$ .
Lemma 4 (Azuma's inequality) and Lemma 5 (Borel–Cantelli), both already proved on the platform and referenced.
(57): a pathwise regret bound for the iterates against $G(w^*)=\sup_{w\ge0}G(w)$ .
The noise vanishes: $\gamma_T\sum_{t\le T}L_t\to0$ almost surely, for the martingale terms $L_t$ of (55).
Lemma 6: $w^{(T+1)}_j/(T\gamma_T)\to0$ almost surely.

Significance

Theorem 3 replaces an optimization over probability measures on a space of functions by a sequence of finite-dimensional problems (16) and a one-line dual update. Problem (16) is often solved greedily: under a polymatroid structure the paper's Theorem 4 turns it into an index rule. The result therefore justifies a practical rationing heuristic with a guarantee: a firm that runs Algorithm 1 on historical demand gets a policy whose average cost is asymptotically no worse than the optimum of (11), and whose service levels asymptotically meet every individual target.

On the formal side, the statement and its milestones combine a projected stochastic subgradient method, a triangular array of bounded martingale differences, and the weak duality of a semi-infinite program. The paper proves the result; none of it has been machine-checked. A formal proof must also repair the paper's argument for (28): the stochastic-dominance induction on p. 54 does not establish an almost-sure limit.

Difficulty

The obvious argument treats the iterates as a standard online gradient method with a fixed step. That handles the expected regret but not the almost-sure claim. The noise terms $L_t$ depend on the horizon $T$ , both through $\gamma_T$ and through every earlier iterate, so they form a triangular array, not a single martingale. Classical stochastic-approximation theorems with decreasing steps do not apply. Feasibility of $c$ enters only through the dual bound $G(w^*)\le\mathrm{Obj}(11)$ . The expectations $E_{\tilde D^t}$ are over a fresh copy with the random iterate held fixed, and that must be kept separate from the sample $D^{(t)}$ the iterate itself uses. The service half (28) needs a bound on the growth of the dual weights (Lemma 6), and that bound itself needs the cost to be bounded on feasible allocations.

Formalization scope

Indices are 0-based: customers and resources are Fin n and Fin m. The Lean iterate at index $t$ is the page's $w^{(t+1)}$ , and $\sum_{t=1}^T$ becomes a sum over $0,\dots,T-1$ .
Randomized policies are finite mixtures of measurable deterministic policies. Every quantity here depends on a mixture only through finitely many expectations, so this is no restriction.
Selections: the theorems quantify over every selection $w\mapsto\varphi_w$ of optimal solutions of (16). It is assumed jointly measurable in $(w,D)$ , so that the iterates are random variables.
Sampling: all horizons $T$ read the first $T$ entries of one i.i.d. sequence. That single probability space is what "almost surely as $T\to\infty$ " requires.
Limits: $\limsup\le$ and $\liminf\ge$ are written as "for every $\varepsilon>0$ , eventually in $T$ ".
Norms: the Euclidean norm in (57) is a written-out sum of squares, because Lean's default norm on Fin n → ℝ is the sup norm.
Added hypotheses, beyond Assumptions 1 and 3 and the standing assumptions of §1.1:
- $R_j\ge0$ and jointly measurable;
- $s\le D$ on $P(c,D)$ for $D\ge0$ ; instances whose page-level $P(c,D)$ is empty for negative $D$ extend it by $P(c,D^+)$ ;
- $|f|\le K$ on feasible allocations, which the paper's proof of Lemma 6 uses implicitly.

Two formalizations would make (27) trivial, and both are ruled out. $\mathrm{Obj}(11)$ is the infimum of the cost over feasible mixtures; it is neither defined from the algorithm nor identified with $G(w^*)$ . Feasibility and $|f|\le K$ keep that infimum from being Lean's junk value $0$ . The selection depends on $w$ alone, not on $\beta$ or on the sample path.

The development needs Bochner integrals, independence (iIndepFun), conditional expectation and the referenced Azuma and Borel–Cantelli results. The triangular-array strong law for bounded martingale differences with summable exponential tails is reusable beyond this mission. Contributions toward any milestone, or a repaired proof of (28), are welcome.

Selected references

J. Jiang, S. Wang, J. Zhang, Achieving High Individual Service-Levels without Safety Stock? Optimal Rationing Policy of Pooled Resources, SSRN 3385089 (version of 31 July 2021); Operations Research (2023). https://ssrn.com/abstract=3385089, https://doi.org/10.1287/opre.2022.2386
K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967) 357–367. https://doi.org/10.2748/tmj/1178243286
A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, Kluwer (2001) 135–165. https://doi.org/10.1007/978-1-4757-3403-4_7
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19 (2009) 1574–1609. https://doi.org/10.1137/070704277

9 thms3 active usersReviewed

Markov Chain Operations Research·Captain: mikedeng1

Lightning Network Economics: Channels IV: The Long-Run Number of Channel Transactions per On-Chain Transaction in Closed FormResearch Paper

Payment channels and blockchain congestion

A blockchain such as Bitcoin settles a limited number of transactions per unit of time, and every on-chain transaction pays a fee that rises with congestion. The Lightning Network moves payments off the chain. Two parties lock funds in a payment channel with one on-chain transaction, and they can then pay each other any number of times by updating the channel balance privately. A new on-chain transaction is needed only when one side of the channel runs out of funds and the channel must be reset.

Guasoni, Huberman and Shikhelman (Management Science, 2023) model a channel between two nodes that pay each other at Poisson rates. They compute its cost and its optimal size, and in §3.3 they quantify how much a channel relieves the chain. The relief is the long-run number of channel transactions carried per on-chain transaction (Proposition 2). A related quantity is the probability that the payee side of the channel, not the payer side, is exhausted first (Proposition 1). This mission formalizes both results, which are statements about two finite random walks.

Setting

Node 1 commits $l_1\ge1$ units to the channel and node 2 commits $l_2\ge1$ units. Node 1 pays node 2 one unit at the jumps of a Poisson process with rate $\lambda_1$ , and node 2 pays node 1 at rate $\lambda_2$ , independently. Write $q=\lambda_2/\lambda_1$ . The balance $X$ starts at $0$ . It moves up by one when node 2 pays and down by one when node 1 pays. Node 2 has exhausted its side when $X=l_2$ , and node 1 when $X=-l_1$ .

Only the sequence of payments matters here, not their timing or discounting. Observed at its jumps, the balance is a random walk that steps up with probability $p=\lambda_2/(\lambda_1+\lambda_2)$ and down with probability $1-p=\lambda_1/(\lambda_1+\lambda_2)$ . Two versions of this walk appear.

The absorbed walk on $\{-l_1,\dots,l_2\}$ stops at $-l_1$ and at $l_2$ . Write $\mathbb P_0\{\tau_{l_2}<\tau_{-l_1}\}$ for the probability that, from the balance $0$ , it reaches $l_2$ before $-l_1$ .
The reset walk returns the balance to $0$ as soon as it reaches $l_2$ or $-l_1$ , which models an on-chain reset of the channel. It lives on the interior balances $\{-l_1+1,\dots,l_2-1\}$ . For a stationary distribution $m$ of this walk, $m(n)$ is the long-run fraction of transactions the balance spends at $n$ , with $m(l_2)=m(-l_1)=0$ .

The transactions that trigger an on-chain reset are the up-moves from $l_2-1$ and the down-moves from $-l_1+1$ . Their stationary fraction is

f(m)=m(l_2-1)\,\frac{\lambda_2}{\lambda_1+\lambda_2}+m(-l_1+1)\,\frac{\lambda_1}{\lambda_1+\lambda_2},

and the long-term ratio of channel to on-chain transactions is $1/f(m)$ .

Formalization targets

Goal: Proposition 2 (Congestion Reduction)

For $\lambda_1,\lambda_2>0$ with $\lambda_1\neq\lambda_2$ and $l_1,l_2\ge1$ , the reset walk has a stationary distribution, and every stationary distribution $m$ satisfies

\frac1{f(m)}=\frac{(q+1)\Bigl(\bigl(l_2(q^{l_1}-1)-l_1\bigr)q^{l_2}+l_1\Bigr)}{(q-1)(q^{l_1+l_2}-1)}.

Milestones

(28) and (29): $m(n)=m(0)\,\dfrac{q^{l_2}-q^n}{q^{l_2}-1}$ for $0\le n\le l_2$ , and $m(n)=m(0)\,\dfrac{q^{l_1+n}-1}{q^{l_1}-1}$ for $-l_1\le n\le0$ .
(30): $m(0)=\dfrac{(q^{l_1}-1)(q^{l_2}-1)}{\bigl(l_2(q^{l_1}-1)-l_1\bigr)q^{l_2}+l_1}$ .
The on-chain fraction $f(m)$ is the reciprocal of the goal's closed form.
Proposition 2 (i)–(ii): the closed form tends to $l_1$ as $q\downarrow0$ and to $l_1l_2$ as $q\to1$ .
Proposition 1 (i)(a),(c): $\mathbb P_0\{\tau_{l_2}<\tau_{-l_1}\}=\dfrac{1-q^{-l_1}}{1-q^{-l_1-l_2}}$ if $\lambda_2>\lambda_1>0$ , and $=1$ if $\lambda_2>\lambda_1=0$ .
Proposition 1 (i)(b), corrected: for $\lambda_1=\lambda_2>0$ the probability is $l_1/(l_1+l_2)$ , which is the published gambler's ruin theorem.

Significance

Proposition 2 measures how much a channel relieves the chain. A unidirectional channel of size $l_1$ carries $l_1$ payments per on-chain transaction. A symmetric bidirectional channel carries $l_1l_2$ , which grows with the product of the two sizes rather than their sum. For a fixed total commitment, the relief is therefore largest when the flows are balanced. This is the paper's quantitative case that bidirectional channels reduce congestion far more than one-way ones. The probabilities of Proposition 1 tell each node how likely it is to be the one whose funds run out.

Both results are proved in the paper by elementary difference-equation arguments. Neither has a machine-checked proof. Formalizing them gives a verified closed form for the stationary law of a biased walk with resets at both ends. It also gives a biased gambler's-ruin probability on top of the platform's Markov chain library, which so far has only the fair case. The formalization also corrects case (b) of Proposition 1, which as printed claims $1/2$ for every $l_1,l_2$ ; the paper's own proof gives $l_1/(l_1+l_2)$ .

Difficulty

The reset walk is not a birth–death chain: the balance $0$ receives the reset flow from both ends, so the walk is in general not reversible, and the detailed-balance shortcut that gives the stationary law of a reflected walk in one line fails. The balance equation (27) holds only away from $0$ and from the two reset points. In Lean, the abstract equation $mP=m$ on Fin (l₁ + l₂ - 1) must be related to recurrences indexed by integer balances, and the edge cases $l_1=1$ and $l_2=1$ , where the bottom or top balance is $0$ itself, have to be handled. For Proposition 1, the hitting probability is defined as an infinite series of first-passage probabilities over trajectories, and the closed form is a statement about the value of that series.

Formalization scope

The walks are transition matrices in the platform's MarkovMixing vocabulary (mm_basic, mm_path). Stationarity is MarkovMixing.IsStationary (nonnegative, sums to one, $mP=m$ ), and hitting probabilities are MarkovMixing.hitBeforeProb, a series that sums to $0$ when it is not summable. The absorbed walk is absorbed almost surely, so this convention is never triggered.
The absorbed walk has states Fin (l₁ + l₂ + 1), with index $i$ for the balance $i-l_1$ . The reset walk has states Fin (l₁ + l₂ - 1), with index $j$ for the balance $j+1-l_1$ . massAt reads $m(n)$ at an integer balance and returns $0$ outside the interior, which is the paper's convention $m(l_2)=m(-l_1)=0$ .
Rates are real with $\lambda_1,\lambda_2>0$ , and sizes are natural numbers $l_1,l_2\ge1$ .
The hypothesis $\lambda_1\neq\lambda_2$ ( $q\neq1$ ) is added to Proposition 2 and to (28)–(30). The formulas divide by $q-1$ , and the paper treats $q=1$ only as a limit.
The "long-term ratio" is read as $1/f(m)$ for a stationary $m$ , as in the paper's proof. Its identification with a pathwise long-run average is an ergodic theorem that the paper does not state and the mission does not ask for.
Proposition 2 (i)–(ii) are limits of the closed form along $q\downarrow0$ and $q\to1$ , $q\neq1$ .
The following would trivialize the problem and are excluded: fixing the sizes or the rates, setting $\lambda_1=\lambda_2$ , defining the long-term ratio or the stationary distribution by the closed form, or quantifying over stationary distributions without proving that one exists.
The platform has the Proved results MarkovMixing.exists_stationary_pos and MarkovMixing.stationary_unique for irreducible chains, and the fair gambler's ruin. Lemmas on stationary laws of chains with resets, and biased gambler's-ruin results on the MarkovMixing chains, would be reusable beyond this mission and are welcome.

Selected references

P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, Management Science, Articles in Advance, published online November 6, 2023, pp. 1–14. https://doi.org/10.1287/mnsc.2022.01664
J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, white paper, 2016. https://lightning.network/lightning-network-paper.pdf
D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (§1.5, §2.1). https://doi.org/10.1090/mbk/058

13 thms3 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: mikedeng1

Quantum Amplitude Amplification and Estimation: Est_Amp(A, χ, M) Outputs ã with |ã − a| ≤ 2πk√(a(1−a))/M + k²π²/M² with Probability ≥ 8/π² for k = 1 and > 1 − 1/(2(k−1)) for k ≥ 2Research Paper

Motivation

Many quantum algorithms end in a measurement that succeeds only with some probability $a$ . Two questions follow: how to raise that probability, and how to learn its value. G. Brassard, P. Høyer, M. Mosca and A. Tapp answered both in Quantum Amplitude Amplification and Estimation (arXiv:quant-ph/0005055, 2000; Contemporary Mathematics 305, 2002). Amplitude amplification generalizes Grover's search (Grover 1996) to an arbitrary algorithm $\mathcal A$ and an arbitrary notion of success. Amplitude estimation combines amplification with the quantum Fourier transform to estimate $a$ with error of order $1/M$ after $M$ applications of $\mathcal A$ , where classical sampling needs order $1/M^2$ samples. Quantum counting, quantum Monte Carlo integration (Montanaro 2015) and many quantum speedups for statistics and finance rest on this estimation step.

Timeline:

1996: Grover's search algorithm.
1997: Brassard and Høyer (arXiv:quant-ph/9704027) introduce the amplification operator $\mathbf Q$ for a general algorithm.
1998: Brassard, Høyer and Tapp (arXiv:quant-ph/9805082) give quantum counting.
2000: the paper formalized here presents amplification, estimation and counting in a unified form with explicit constants.

Setting

Let $\mathcal H = \mathbb C^\iota$ be a finite-dimensional Hilbert space with computational basis $\{|x\rangle : x\in\iota\}$ and a distinguished zero state $|0\rangle$ . A quantum algorithm without measurements is a unitary matrix $\mathcal A$ on $\mathcal H$ , and a Boolean function $\chi:\iota\to\{0,1\}$ calls a basis state good when $\chi(x)=1$ . Write $|\Psi\rangle=\mathcal A|0\rangle=|\Psi_1\rangle+|\Psi_0\rangle$ for the splitting into the projections onto the good and the bad subspaces. The initial success probability is $a=\langle\Psi_1|\Psi_1\rangle$ , the probability that measuring $|\Psi\rangle$ gives a good state, and $\theta_a\in[0,\pi/2]$ is the angle with $\sin^2\theta_a=a$ .

The operator $\mathbf S_\chi$ flips the sign of the amplitudes of good states, $\mathbf S_0$ flips the sign of the amplitude of $|0\rangle$ , and the amplification operator is

\mathbf Q=-\mathcal A\,\mathbf S_0\,\mathcal A^{-1}\,\mathbf S_\chi .

For an integer $M\ge1$ , the quantum Fourier transform is $F_M:|x\rangle\mapsto\frac1{\sqrt M}\sum_{y=0}^{M-1}e^{2\pi\imath xy/M}|y\rangle$ , and the controlled power is $\Lambda_M(U):|j\rangle|y\rangle\mapsto|j\rangle U^j|y\rangle$ . The phase state is $|S_M(\omega)\rangle=\frac1{\sqrt M}\sum_y e^{2\pi\imath\omega y}|y\rangle$ , and $d(\omega_0,\omega_1)=\min_{z\in\mathbb Z}|z+\omega_1-\omega_0|$ is the circular distance. The algorithm $\mathbf{Est\_Amp}(\mathcal A,\chi,M)$ applies $(F_M^{-1}\otimes I)\,\Lambda_M(\mathbf Q)\,(F_M\otimes I)$ to $|0\rangle\mathcal A|0\rangle$ , measures the first register to obtain $y\in\{0,\dots,M-1\}$ , and outputs $\tilde a=\sin^2(\pi y/M)$ .

Formalization targets

Goal: Theorem 12 (Amplitude Estimation)

For every positive integer $k$ , the event

|\tilde a-a|\le 2\pi k\frac{\sqrt{a(1-a)}}{M}+k^2\frac{\pi^2}{M^2}

has probability at least $8/\pi^2$ when $k=1$ , and greater than $1-\frac1{2(k-1)}$ when $k\ge2$ . If $a=0$ then $\tilde a=0$ with certainty. If $a=1$ and $M$ is even, then $\tilde a=1$ with certainty.

Milestones, in attack order

Lemma 1: $\mathbf Q$ acts on $|\Psi_1\rangle$ and $|\Psi_0\rangle$ by an explicit $2\times2$ matrix.
Equations (3)–(5): for $0<a<1$ , $|\Psi_\pm\rangle$ are orthonormal eigenvectors of $\mathbf Q$ with eigenvalues $e^{\pm\imath2\theta_a}$ .
Equation (6): $|\Psi\rangle$ in that eigenbasis.
Lemma 7: the error in the angle controls the error in $\sin^2$ .
Lemma 10: the overlap $|\langle S_M(\omega_0)|S_M(\omega_1)\rangle|^2$ .
Theorem 11: the exact law of phase estimation and its two tail bounds.
Two steps of the proof of Theorem 12 (p. 20): the state after $\Lambda_M(\mathbf Q)$ , and the outcome law as an even mixture of two phase-estimation laws.

Further statements from the same development are included as companion targets: the success probability $\sin^2((2m+1)\theta_a)$ after $m$ rounds, Theorem 2 (quadratic speedup), Lemma 5 (the phase-generalized $\mathbf Q$ ), Theorem 13 (counting) and Corollary 14.

Significance

Theorem 12 is the quantitative core of quantum estimation algorithms. Its error bound scales as $1/M$ in the number of applications of $\mathbf Q$ , and that scaling is the quadratic speedup behind quantum counting (Theorem 13), quantum mean estimation, and quantum Monte Carlo methods for option pricing and risk analysis. The exact clauses for $a\in\{0,1\}$ make the estimator usable as a zero-error test for the existence of a good state.

All results here are proved in the paper and widely reproduced in textbooks; none is open. What the mission adds is a machine-checked account with the paper's constants: $8/\pi^2$ , the strict tail bound $1-1/(2(k-1))$ , and the additive term $k^2\pi^2/M^2$ . It also covers every modulus $M\ge1$ , not only powers of two, and arbitrary $\mathcal A$ and $\chi$ , not only uniform search. Related statements are posed on the platform but unproved:

QAlgorithms.Nannicini.amplitudeEstimation_error is the special case $k=1$ , $M=2^m$ , with a bit-string presentation of the algorithm.
QAlgorithms.Nannicini.groverOperator_eigenstates states (3)–(4) for an abstract reflection.
QAlgorithms.DeWolf.amplitudeAmplification covers (8) and the $1-a$ half of Theorem 2.

The Grover theorems already proved on the platform treat a single marked item with a uniform start.

Difficulty

The obvious argument has two parts: $\mathbf Q$ rotates a plane by $2\theta_a$ , and phase estimation reads off $\theta_a$ . Neither part settles the measurement law. The outcome probability is a sum over the second register of the squared amplitudes of an entangled state. Reducing it to two independent phase-estimation laws requires orthonormality of $|\Psi_\pm\rangle$ , and that holds only for $0<a<1$ . The goal does not assume this: the degenerate cases $a\in\{0,1\}$ , where $|\Psi_\pm\rangle$ do not exist, must be handled separately.

On the phase-estimation side, the tail bound for $k\ge2$ must be strict and must hold for every $M\ge1$ . The bound $8/\pi^2$ for $k=1$ relies on a minimization over $\Delta\in[0,1/M]$ that needs $M>2$ , while the goal has no such hypothesis, so the small cases $M\le2$ need their own argument. Finally, the second eigenphase appears as $1-\theta_a/\pi$ , and the matching outcome $M-y$ wraps to $0$ at $y=0$ .

Formalization scope

States are vectors $\iota\to\mathbb C$ over a finite type $\iota$ (the paper writes $\chi:\mathbb Z\to\{0,1\}$ ), operators are matrices, and $\{0,1\}$ is Bool. $\mathcal A$ is assumed unitary and $\mathcal A^{-1}$ is written $\mathcal A^\dagger$ . The second register is Fin M with $M\ge1$ ; $F_M$ is the platform's published Fourier matrix ShorAlgorithms.Shared.fourierMatrix (same sign and normalization as (13)), $F_M^{-1}$ is its conjugate transpose, and $\Lambda_M$ is an explicit matrix on Fin M × ι. The outcome law is the sum over the second register of squared moduli of the final state, and an event's probability is the sum of the outcome probabilities over it. $a$ is computed from $\mathcal A$ , $\chi$ and $|0\rangle$ , and $\theta_a=\arcsin\sqrt a$ . The goal assumes neither $0<a<1$ nor $M>2$ , and it keeps the strict inequality for $k\ge2$ . The step "after step 2, ignoring global phase" is stated with its phase $-\imath$ written out.

A formalization that takes $a$ or $\theta_a$ as a free parameter, assumes the mixture form of the outcome law, or reasons about $|\Psi_\pm\rangle$ without deriving them from $\mathcal A$ and $\chi$ would make the goal trivial. The statements here do none of these: every quantity is computed from $\mathcal A$ , $\chi$ , $|0\rangle$ and $M$ . The clauses "uses exactly $M$ evaluations of $f$ " (Theorem 12) and "requires exactly $\lceil\sqrt N\rceil$ evaluations" (Corollary 14) are not formalized, because the matrix model has no oracle whose calls could be counted. Theorem 13 is stated for any unitary sending $|0\rangle$ to the uniform superposition, which includes $F_N$ , as the paper allows on p. 20.

A complete development needs:

geometric sums of roots of unity;
the Fejér-kernel identity of Lemma 10;
the inequality $\sin x\ge 2x/\pi$ on $[0,\pi/2]$ ;
a bound on $\sum_{j\ge k}1/j^2$ ;
Kronecker-product bookkeeping for two-register states.

The phase-estimation part (Lemma 10, Theorem 11) does not depend on amplification and can be reused by any later formalization of Fourier-based phase estimation. Proofs of individual milestones, and lemmas on Fin M Fourier sums, are welcome.

Selected references

G. Brassard, P. Høyer, M. Mosca, A. Tapp, Quantum Amplitude Amplification and Estimation, in Quantum Computation and Information, Contemporary Mathematics 305, AMS, 2002, pp. 53–74. arXiv:quant-ph/0005055
G. Brassard, P. Høyer, An exact quantum polynomial-time algorithm for Simon's problem, ISTCS 1997. arXiv:quant-ph/9704027
G. Brassard, P. Høyer, A. Tapp, Quantum counting, ICALP 1998. arXiv:quant-ph/9805082
L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
A. Montanaro, Quantum speedup of Monte Carlo methods, Proc. R. Soc. A 471, 2015. arXiv:1504.06987

14 thms3 active usersReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics XC: Structural Corporate Default and Rating-Migration Credit ValuationTextbook

Motivation

Credit risk matters to insurer bond holdings, pension scheme fixed-income investment and counterparty guarantees. Merton's corporate debt model derives terminal shareholder and bondholder payoffs from limited liability and asset value. Jarrow–Lando–Turnbull introduces observable ratings with Markov state migrations and default, motivating a second, independently defined view of risky fixed-income valuation.

Setting

A firm has nonnegative terminal assets and a single promise of face-value debt. Creditors are paid no more than the promise and no more than available assets; equity gets the residual. Finite genuine probability masses attach to terminal asset scenarios and yield discounted debt and equity claim valuations. Separately, a three-state rating matrix contains two non-default ratings and a terminal default state, with nonnegative row probabilities and full row-sum constraints.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Merton limited liability and terminal default payoffs

Strict asset deficit is equivalent to zero equity except for solvent zero-cashflow special cases.

E_T=(V_T-D)^+,\quad B_T=\min(V_T,D)

Finite default risk premiums and risk-neutral debt pricing

A bond priced equally to risk-free debt has zero model spread.

B_0=e^{-rT}\mathbb E^{\mathbb Q}[\min(V_T,D)]

Three-state rating migration and recoverable default claims

Structural terminal solvency and an independent absorbing-rating transition system reconcile riskier defaultable debt prices, nonnegative credit value deductions and genuinely two-period probability conservation.

\sum_j P_{ij}=1,\quad P_{\text{default,default}}=1

Capstone theorem

Structural terminal solvency and an independent absorbing-rating transition system reconcile riskier defaultable debt prices, nonnegative credit value deductions and genuinely two-period probability conservation.

\sum_j P_{ij}=1,\quad P_{\text{default,default}}=1

Significance

As discussed in Merton's corporate-credit model, The mission connects terminal firm claims to an actual finite risk-neutral weighted value: equity plus debt exhaust firm assets, expected discounted defaultable debt is bounded above by its risk-free counterpart, and credit value deductions are nonnegative. The genuine two-step rating migration law preserves total probability mass. These independently defined results jointly give an actuarial foundation for pricing defaultable corporate securities and recognising credit exposures in asset-liability valuation.

Difficulty

It must be proved that the limited-liability payoffs partition total assets, with exact boundary conditions where assets equal or fall below face value. The pricing theorem must distinguish actual discounted expected creditor payments from assuming a closed-form Black–Scholes price; no lognormal risk-neutral firm distribution is postulated. Credit spreads require positive debt prices and maturities. A rating transition matrix must be proved stochastic under composition, and an absorbing default state is a model condition rather than automatically true for arbitrary matrices.

Formalization scope

Limited liability and rating-migration probabilities are distinct mathematical constructs in this model. The complete diffusion-based Merton option value and continuous-time rating default models remain future mathematical research. The current target is nontrivial because it derives the bond valuation from limited-liability terminal payouts and an actual probability space, and the migration law from an independent finite transition kernel. Existing bond-present-value and state-reward missions are useful, but they do not identify shareholder and debt recovery claims. Its expected payoff and finite rating matrix infrastructure is reusable in asset-liability modelling and insurer counterparty credit valuation.

A firm's terminal assets must be partitioned consistently between equity and creditor payoffs. Above the promised debt face amount bondholders receive the promise and owners receive remaining assets. At the strict default threshold the owners' limited liability makes equity worthless and bondholders recover the remaining assets. The source values these payoffs using a proper finite risk-neutral scenario law, proving that discounted risky debt is no more valuable than the risk-free debt promise. The other branch builds a genuinely stochastic three-state rating transition matrix and derives two-step migration probabilities from matrix multiplication. Those observed or risk-neutral migration probabilities are not interchangeable without an additional measure-change argument. This is precise finite corporate credit mathematics; it is not a fabricated full closed-form structural diffusion model or a continuous-time default-intensity theory.

The new credit mission establishes exact one-period finite-state structural debt/equity payoff pricing and two-step rating probability conservation. It does not claim Merton's Black–Scholes closed-form equity value, stochastic diffusion replication, or the full continuous-time JLT risk-neutral generator model. The default-state absorbing property needs additional row restrictions and is not asserted for unrestricted transition matrices. Those are substantial extensions, and the current theorem bodies remain unproved.

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

Robert C. Merton (1974), On the Pricing of Corporate Debt: The Risk Structure of Interest Rates, Journal of Finance 29(2), 449–470. https://doi.org/10.1111/j.1540-6261.1974.tb03058.x
Robert A. Jarrow, David Lando and Stuart M. Turnbull (1997), A Markov Model for the Term Structure of Credit Risk Spreads, Review of Financial Studies 10(2), 481–523. https://doi.org/10.1093/rfs/10.2.481

48 thms3 active usersReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics LXXXIX: Expected Utility, Certainty Equivalents and Stochastic Risk OrdersTextbook

Motivation

Insurance economics prices risk using the utility of wealth rather than merely its variance. Pratt's seminal work derives risk aversion and the certainty-equivalent insurance premium, while Rothschild and Stiglitz connect comparative risk to probability order. Earlier actuarial entropic premium missions contain special finite retention objectives but do not derive an independently constructed expected wealth utility with premium indifference and finite stochastic dominance.

Setting

Losses are monetary outcomes on a genuinely finite scenario probability model, whose masses are nonnegative and sum to one. The exponential CARA wealth utility is strictly increasing and concave for positive aversion. The certainty-equivalent premium is constructed from the actual exponential moment of loss. Full insurance replaces the uncertain loss with a fixed premium and its utility is compared with the truly weighted uninsured outcome.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Expected exponential utility and absolute risk aversion

Utility of deterministic wealth equals its scenario expectation.

u_a(w)=-e^{-aw},\quad A(w)=-u''_a(w)/u'_a(w)=a

Actuarial insurance certainty equivalents and premium indifference

Risk-averse exponential expected utility demands at least the expected claim cost.

\pi_a(X)=\frac{1}{a}\log\mathbb E[e^{aX}]

Genuine pathwise coupling and finite first-order stochastic dominance

The actuarial insurer and policyholder indifference premium follows from genuinely averaged utility, with positive risk loading and a finite-scenario stochastic risk ordering.

X\le Y\ \text{a.s.}\Longrightarrow \mathbb E[\phi(X)]\le\mathbb E[\phi(Y)]

Capstone theorem

The actuarial insurer and policyholder indifference premium follows from genuinely averaged utility, with positive risk loading and a finite-scenario stochastic risk ordering.

X\le Y\ \text{a.s.}\Longrightarrow \mathbb E[\phi(X)]\le\mathbb E[\phi(Y)]

Significance

As discussed in Pratt's utility-risk treatment, The capstone proves a complete indifference premium identity, not merely its algebraic definition, and derives risk loading above expected loss from convexity of the exponential. A coupled stochastic order implies both the ordering of actual finite distribution functions and higher expected utility for increasing utility functions. The same ordering is related to excess-of-loss premiums through statewise monotonicity. These results supply core insurer and policyholder pricing foundations.

Difficulty

The logarithmic certainty equivalent requires strictly positive exponential moments and a nonzero risk-aversion parameter. The actual expected utility factorization must account for the sign of negative exponential utility. Risk loading requires Jensen's inequality or an equivalent discrete exponential-convexity argument, not the assertion that every risk is profitable to insure. The comparison of finite CDFs must reverse the inequality for higher wealth, while a higher loss severity raises stop-loss costs. Pathwise coupling is stronger than the entire stochastic-dominance order and is identified as such.

Formalization scope

Certainty-equivalent premium and stochastic risk ordering are distinct mathematical constructs in this model. A future generalisation will derive second-order stochastic dominance via integrals of real CDFs and concave expected utility, not merely a pathwise coupling. The current project is nontrivial because the CARA indifference identity follows by differentiating and averaging the actual utility, and the insurer's risk loading is derived from Jensen's inequality. Existing specialised exponential risk-price examples provide a useful benchmark but do not replace these general sources. The premium and coupling functions are reusable for nonproportional reinsurance, risk classification and comparative risk analysis.

Under constant absolute risk aversion the negative exponential utility function is increasing and concave in wealth when risk aversion is positive, even though its numerical utility level is negative. A fair premium is not obtained by simply assuming a desired level of profit. The expected uninsured utility is calculated from true scenario probabilities, the utility with full insurance is calculated using a fixed premium and the resulting indifference equation is solved from the loss exponential moment. The log moment premium must then be compared against expected claim cost using convexity, and the sign of this loading depends on risk aversion. Finite distribution functions and expected excess claims are independently defined for comparison. The pathwise coupling order in the source is stronger than first-order stochastic dominance, so no false claim of characterising all stochastic orders is made. Second-order dominance requires a separate distribution-integral analysis.

This is a genuine finite-probability CARA model with exactly derived insured/uninsured premium indifference. The stochastic order is proven for explicit statewise couplings and thus yields a strong sufficient condition for first-order stochastic dominance, not a complete characterisation of arbitrary second-order stochastic dominance. General concave utility risk orders, mean-preserving spreads, Arrow–Pratt comparative aversion for all utility families, and infinite random variables are future developments. All proof obligations are open.

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

John W. Pratt (1964), Risk Aversion in the Small and in the Large, Econometrica 32, 122–136. https://doi.org/10.2307/1913738
Michael Rothschild and Joseph E. Stiglitz (1970), Increasing Risk: I. A Definition, Journal of Economic Theory 2, 225–243. https://doi.org/10.1016/0022-0531(70)90038-4

46 thms3 active usersReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics XCI: Joint-Life Mortality Profit and Contingent Survivor BenefitsTextbook

Motivation

Mortality experience in joint-life assurance and pensions depends not only on whether someone died, but on which insured life survives and which survivor or joint reserve must then be held. Standard multiple-life actuarial valuations motivate last-survivor, reversionary and guaranteed pension benefits. Earlier actuarial missions XLV and XLVI treat basic reversionary annuities and single-life mortality profit separately; this connects them through a genuine four-outcome death-strain model.

Setting

Two members start alive and experience independent yearly survival outcomes. Exactly four mutually exclusive joint states follow: both survive, only the first survives, only the second survives, or neither survives. Their probabilities use product and complement survival factors. The year-end reserve and any benefits can differ for every one of these states. Opening reserves plus premiums earn the annual return before payment and the next state contingent reserve is recognized.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Independent joint-life outcomes and probabilities

Each valid joint-life outcome has nonnegative mass.

p_{xy}=p_xp_y,\quad p_{x\dagger y}=(1-p_x)p_y

Outcome-dependent reserves, benefits and death strain

Additional state-specific benefit claims add to expected death strain.

D_{s}=B_s+V_s-(V_0+P)(1+i)

Joint mortality profit and limited-contingent survivor benefits

An exhaustive, correctly normalized two-life outcome model makes the mortality experience profit mean zero, retaining separate survivor reserves, death benefits and guaranteed payment conventions.

\Pi_{\text{mort}}=\sum_s p_s D_s-D_{\text{observed}}

Capstone theorem

An exhaustive, correctly normalized two-life outcome model makes the mortality experience profit mean zero, retaining separate survivor reserves, death benefits and guaranteed payment conventions.

\Pi_{\text{mort}}=\sum_s p_s D_s-D_{\text{observed}}

Significance

As discussed in Dickson, Hardy and Waters' multiple-life analysis, The capstone derives actual four-state normalization and reconciles joint mortality profit as expected death strain less observed state-specific death strain, whose expected result is zero under its own properly normalized law. The state-specific reserve functions distinguish the two possible remaining single-life liabilities rather than collapsing them into a single average. Limited-reversionary and certain guarantee payments are represented as separate conditional benefits.

Difficulty

Four disjoint probabilities must be normalized with exact endpoint treatment. Reserve releases after each death outcome may have opposite signs to death-benefit payments, so the state strain must include both payout and next-state reserve less the accumulated starting fund. Expected mortality profit cannot be asserted by defining it to have zero mean: it must follow from the actual weighted expectation of the observed strain. Independence is an explicit current assumption; arbitrary dependent lives need a separate four-state probability law.

Formalization scope

Joint-life mortality profit and state-dependent death strain are distinct mathematical constructs in this model. A future mission could introduce dependent lifetimes and within-year order of deaths, then compute first-to-die and last-survivor benefit present values directly from the joint survival law. The present work is nontrivial because both survivor reserves and actual death claims differ across the four states, while the mean mortality profit emerges from their normalised probability distribution. Existing joint-life annuity and single-life profit missions do not establish this combination. The outcome-specific reserve and mortality gain functions are reusable for spouse's pensions, death-in-service benefits and multi-life experience analysis.

Four disjoint annual outcomes must be considered for a policy whose two insured lives begin the year alive. They are both alive, only the first alive, only the second alive and both dead. Each outcome has a separate year-end reserve and may have a different death or survivor benefit. Accordingly, its actual death strain includes the benefit paid plus the new reserve less accumulated beginning-year funds. Expected strain is a genuine probability-weighted average of those four observed strains. The mortality experience profit for any one realised outcome equals the expected strain less that outcome's actual strain. Its expectation must be shown to vanish under the normalised four-outcome probability distribution, rather than by assuming zero mean. This framework supplies an actuarial bridge from joint-life/reversionary benefits to experience profit analysis and guarantee-period pensions. Within-year timing and dependent life outcomes require additional formal work.

This is a complete one-year joint mortality-experience model with explicit separate survivor reserves, not a full continuous-time ordering of first and second deaths inside the same policy year. Guarantee-period timing is represented by a separate deterministic indicator input. Exact age differences, policy options, death-payment timing and dependence-copula extensions can build on these definitions later. All theorem statements remain unproved.

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, Cambridge University Press. https://www.cambridge.org/core/books/actuarial-mathematics-for-life-contingent-risks/
S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Wiley. https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521

54 thms3 active usersReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics LXXVII: Compound Aggregate Masses and the Full Finite Panjer RecursionTextbook

Motivation

Panjer's original 1981 result derives the aggregate claims recursion from a special frequency probability law and arbitrary nonnegative-integer severity mass distribution, including claims worth zero. The original article and the Sundt–Jewell extension underpin the mission. Earlier actuarial mission LIV handles direct recurrence algebra, while LXXIII derives the Bernoulli first positive aggregate mass identity. This mission formalises a full positive-aggregate-severity recursion for a genuinely constructed compound law.

Setting

A claim count N has probability weights p_n supported on {0,...,m}, with no artificial truncation of an otherwise infinite count distribution. Independent severity masses f_j on nonnegative integer amounts admit a genuine n-fold convolution, with count-zero convolution equal to a unit atom at zero. Thus g_k=Σ_{n=0}^m p_n(f^{*n})k is defined independently of Panjer's formula. The count recursion p_n=(a+b/n)p{n−1} is assumed only for 1≤n≤m+1, including its boundary p_{m+1}=0, and p_n=0 above m. No conclusion about the aggregate g is assumed.

Formalization targets

Aggregate claims from an actual frequency distribution

Write $p_n$ for the probability of exactly $n$ claims and $f_j$ for the probability that one claim has size $j$ . The frequency law is genuinely supported on $0,\ldots,m$ ; an infinite Poisson distribution is not silently truncated. The empty portfolio has aggregate size zero, while $f^{*n}$ denotes the distribution obtained by summing $n$ independent severities.

The first group constructs the aggregate probability $g_k$ directly from the frequency and severity laws:

g_k=\sum_{n=0}^{m}p_n(f^{*n})_k,\qquad (f^{*0})_0=1.

It also proves the zero-severity convolution identities, nonnegative mass preservation, and finite frequency and severity generating-function relationships.

The Panjer law and its upper support boundary

The count probabilities obey a Panjer recurrence with coefficients $a$ and $b$ . Crucially, the finite-support model includes the transition from $m$ to the compulsory zero probability at $m+1$ :

p_n=\left(a+\frac{b}{n}\right)p_{n-1}, \qquad 1\le n\le m+1,\qquad p_{m+1}=0.

This makes the assumed count law compatible with the finite aggregate distribution. For a claim size that may equal zero, the aggregate zero atom involves every possible claim count:

g_0=G_N(f_0)=\sum_{n=0}^{m}p_n f_0^{\,n}.

Corrected aggregate recursion and valuation

The central target is the entire positive-aggregate-size Panjer recurrence, not merely its first positive atom. For every integer $k\ge1$ , the result is

(1-af_0)g_k= \sum_{j=1}^{k}\left(a+\frac{bj}{k}\right) f_jg_{k-j}.

The factor $1-af_0$ is essential because a positive number of claims may still produce aggregate size zero. Further targets establish properties of cumulative aggregate probabilities, capital exceedance tails and finite stop-loss expectations. Every aggregate probability is defined independently of the recurrence it is subsequently required to satisfy.

Significance

The original Panjer paper gives the classical aggregate-loss setting. The capstone derives (1-a f_0)g_k=Σ_{j=1}^k(a+bj/k) f_j g_{k-j} for every positive aggregate amount from the actual random sum, together with g_0=G_N(f_0). The generator gives a count-supported finite Panjer family; it does not claim an infinite Poisson/negative-binomial count law. The exact zero claim-size correction is essential even when count N is positive, because multiple claims may all have zero monetary size. The authoring graph also includes frequency PGFs, severity convolution, CDF/tail and stop-loss identities.

Difficulty

Existing actuarial probability and Panjer steps are established subject areas. Every formal result introduced in this mission is an open Lean theorem target; none has an accepted proof. A vacuous or trivial definition of the aggregate as the recurrence solution is explicitly ruled out. The proof must rearrange nested severity convolutions, differentiate coefficient identities or establish the equivalent frequency recursion, and manage the zero-severity term that multiplies g_k itself. The count-support cutoff must satisfy the Panjer multiplier at m+1 to avoid invalid boundary terms. The recurrence at k=0 is not defined due to division by k; zero aggregate mass follows separately from the frequency PGF. Because f_0 may be positive, truncating the count sum at arbitrary m with an infinite count law would be mathematically invalid; we avoid that by using a genuine finite count distribution.

Formalization scope

This mission supplies a full k≥1 Panjer relation under an exact finite-support frequency model, not general infinite Poisson or geometric counts and not continuous claim severities. Positivity and mass normalisation require additional explicit probability conditions beyond the purely algebraic count recurrence, so the capstone is a valid algebraic identity even before imposing proper probability weights. All formal results remain Lean theorem targets without accepted proofs. The finite model is a reusable foundation for formal-power-series and analytic infinite-frequency cases.

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

Harry H. Panjer (1981), Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12(1), 22–26. https://doi.org/10.1017/S0515036100006796
Bjørn Sundt and William S. Jewell (1981), Further Results on Recursive Evaluation of Compound Distributions, ASTIN Bulletin 12(1), 27–39. https://doi.org/10.1017/S0515036100006802
S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 21, section 21.11. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml

58 thms3 active usersReviewed

Bandit Algorithms Operations Research Stochastic Systems·Captain: mikedeng1

Learning Unknown Service Rates in Queues 3: In Heavy Traffic Every α-Consistent Scheduling Policy Has Average Queue-Regret at Least D(μ)(K−1) log t / (4 log log t) Up to Time (K−1)D(μ)/(4ε)Research Paper

Motivation

A switch network is a set of $U$ queues served by $K\ge U$ servers. In every time slot each server can serve at most one queue, so a scheduler must pick a matching of queues to servers. Such systems model input-queued packet switches, crowdsourcing platforms that route job types to worker types, and wireless links with unknown channel quality. When the success probability of each queue–server link is unknown, the scheduler has to learn it from the services it observes while the queues are building up. This makes switch scheduling a multi-armed bandit problem in which the cost is not cumulative reward but queue length.

Krishnasamy, Sen, Johari and Shakkottai (arXiv:1604.06377, Operations Research 2021) measure a scheduler by its queue-regret: the expected difference between its queue lengths and those of a genie that knows the best matching. They show that the queue-regret has two regimes. In the late stage, once the queues regularly empty, it decays like $1/t$ (their Theorem 3, the subject of a sibling mission). In the early stage it grows like $\log t/\log\log t$ , as the regret of a classical bandit does, and the system is then effectively unstable. This mission is about the early stage, made precise in the paper's Theorem 8: in heavy traffic, where the arrival rates are close to the best service rates, every reasonable policy pays logarithmic queue-regret for a long time.

The lower-bound technique descends from Lai and Robbins (1985): a policy that does well on every instance must explore each sub-optimal link about $\log t/\mathrm{KL}$ times, a count obtained by a change of measure and the Bretagnolle–Huber inequality.

Setting

Queues are indexed by $u\in[U]$ and servers by $k\in[K]$ . In every slot $t\ge1$ , queue $u$ receives an arrival $A_u(t)\sim\mathrm{Bernoulli}(\lambda_u)$ , and link $(u,k)$ offers a service $R_{uk}(t)\sim\mathrm{Bernoulli}(\mu_{uk})$ . All of these are independent and i.i.d. over slots. Notation:

$\mu^*_u=\max_k\mu_{uk}$ , attained at $k^*_u$ ;
$\epsilon_u=\mu^*_u-\lambda_u$ and $\Delta_{uk}=\mu^*_u-\mu_{uk}$ ;
$\Delta=\min_{u,k\ne k^*_u}\Delta_{uk}$ , $\mu_{\min}=\min\mu_{uk}$ and $\mu^*=\max\mu_{uk}$ ;
$\bar\epsilon=\frac1U\sum_u\epsilon_u$ .

Assumption 1 asks that every queue have a unique best server and that the best servers of distinct queues be distinct. Assumption 2 is $\epsilon_u>0$ for every $u$ . Assumption 3 draws the initial queue vector from the stationary law of the genie queues.

A scheduler picks a matching $\kappa(t)$ , so queue $u$ is served by server $\kappa_u(t)$ . Its decision may use the past schedules, the services observed on the scheduled links, and private randomness. The queues evolve as $Q_u(t)=(Q_u(t-1)+A_u(t)-R_{u\kappa_u(t)}(t))^+$ . The genie always schedules $k^*$ and has queues $Q^*_u(t)$ . The queue-regret is $\Psi_u(t)=\mathbb E[Q_u(t)-Q^*_u(t)]$ . The schedule counts are $T_{uk}(t+1)=\sum_{s=1}^t\mathbb 1\{\kappa_u(s)=k\}$ .

A policy is $\alpha$ -consistent ( $\alpha\in(0,1)$ ) if on every instance $\mathbb E[T_{uk}(t+1)]\le C\,t^{\alpha}$ for all $u$ and all $k\ne k^*_u$ , with a constant $C$ that may depend on the instance. The key constant is

D(\mu)=\frac{\Delta}{\mathrm{KL}\big(\mu_{\min},\frac{\mu^*+1}{2}\big)},

where $\mathrm{KL}$ is the Bernoulli Kullback–Leibler divergence.

Formalization targets

Goal: Theorem 8 (p. 18)

Fix $\mu$ , an $\alpha$ -consistent policy and $\gamma>1/(1-\alpha)$ . There exist constants $\tau$ and $C_1$ , the same for every arrival vector $\lambda$ , such that, with $T_0=\max\{C_1K^\gamma,\tau\}$ and $\eta=(K-1)D(\mu)/(2T_0)$ :

\bar\epsilon<\tfrac\eta2\ \Longrightarrow\ \frac1U\sum_u\Psi_u(t)\ge\frac{D(\mu)}4(K-1)\frac{\log t}{\log\log t}\quad\text{for } t\in\Big[T_0,\ \tfrac{(K-1)D(\mu)}{4\bar\epsilon}\Big],

\epsilon_u<\eta\ \Longrightarrow\ \Psi_u(t)\ge\frac{D(\mu)}4\max\{U-1,2(K-U)\}\frac{\log t}{\log\log t}\quad\text{for } t\in\Big[T_0,\ \tfrac{(K-1)D(\mu)}{2\epsilon_u}\Big].

Milestones

Lemma 18 (Bretagnolle–Huber, p. 37), referenced from the platform.
Lemma 19 (p. 37): for $t>\tau$ , $\mathbb E[T_{uk}(t+1)]+\sum_{u'\ne u}\mathbb 1\{k^*_{u'}=k\}\mathbb E[T_{u'k^*_u}(t+1)]\ge\frac{(1-\alpha)\log t-\log(4KC)}{\mathrm{KL}(\mu_{\min},(\mu^*+1)/2)}$ .
Corollary 20 (p. 39): the summed forms of Lemma 19, with factors $U(K-1)D(\mu)$ , $(U-1)D(\mu)$ and $(K-U)D(\mu)$ .
Lemma 22 (p. 42): $\Psi_u(t)\ge\sum_{k\ne k^*_u}\Delta_{uk}\mathbb E[T_{uk}(t+1)]-\epsilon_u t$ for any policy.

Significance

Theorem 8 complements the late-stage $1/t$ lower bound. Together they show that queue-regret goes through a phase transition. Up to time of order $K/\epsilon$ , the queue-regret of any consistent policy grows like $\log t/\log\log t$ . Since the left end of the window does not move as $\epsilon\to0$ while the right end grows like $1/\epsilon$ , the heavily loaded regime is exactly where learning costs are visible in queue lengths. The theorem also explains why algorithms designed for the late stage (Q-UCB, Q-ThS in the same paper) cannot avoid this early cost.

The formalization adds a machine-checked statement of a lower bound whose constants are pinned down precisely. In particular it states which quantities $\tau$ and $C_1$ may depend on (see below). Along the way it builds a reusable model of a learning switch scheduler: randomized, history-dependent policies, the coupled genie system and the stationary initial law. It also provides a Lai–Robbins-type count bound (Lemma 19) for matching bandits. The results are proved on paper in the held preprint (§9.2). To the best of the platform's records none of them has been formalized.

Difficulty

The obvious route to Theorem 8 is to bound the queue-regret below by the regret of the corresponding bandit. That fails, because queue-regret is not cumulative: an empty queue forgives past mistakes. The proof therefore needs the stationary start (Assumption 3), so that $\mathbb E[Q^*_u(t)]=\mathbb E[Q_u(0)]$ and the sub-optimal schedules show up as a drift (Lemma 22). This holds only up to a load term $\epsilon_u t$ , which limits the window.

The count bound (Lemma 19) requires a change of measure between two instances that swap the best servers of two queues. It needs a chain rule for the KL divergence of adaptively collected observations, where the policy's own randomness must cancel. Neither the swapped instances nor the trajectory law are standard Mathlib objects.

Formalization scope

Queues are Fin U and servers are Fin K, with $1\le U\le K$ and $K\ge2$ . $K=1$ is trivial, and for it $\Delta$ is an empty minimum.
Slots are 1-based. Matchings are embeddings Fin U ↪ Fin K.
Probability space. The randomness is a product of independent uniforms on $[0,1]$ per slot (arrivals, link services, one private scheduler seed), i.i.d. over slots. Bernoulli variables arise by thresholding. The initial state is drawn independently.
Policies see only past schedules and the services on scheduled links (p. 6), plus a private uniform. This covers every randomized, history-dependent policy, and each choice is required to be measurable in the seed.
The genie shares the initial state, arrivals and services of the policy's system. Queue-regret is a Lebesgue integral of $Q_u(t)-Q^*_u(t)$ , a difference bounded by $t$ .
Assumption 3 is the product of the geometric laws $(1-\rho_u)\rho_u^n$ , $\rho_u=\lambda_u(1-\mu^*_u)/((1-\lambda_u)\mu^*_u)$ . This is the stationary law of the printed recursion.
α-consistency quantifies over every instance with entries in $[0,1]$ satisfying Assumption 1. The constant is chosen after the instance, and the definition does not mention $\lambda$ , because the schedule does not depend on it.
$D(\mu)$ and $1/\mathrm{KL}$ are set to $0$ when $\mu^*=1$ , where the divergence is infinite.
Lemma 19 and Corollary 20 carry $C>0$ , which is without loss of generality. Corollary 20(c)'s sum $\sum_{k>U}$ is the sum over servers that are optimal for no queue.
Constants of Theorem 8. The paper says $\tau,C_1$ are "independent of $(\lambda,\mu)$ ". Its proof supports independence of $\lambda$ only, so the formal statement chooses $\tau,C_1$ after $\mu$ and the policy but before $\lambda$ . Choosing them after $\lambda$ would trivialize the theorem, since a huge $C_1$ makes the hypothesis $\bar\epsilon<\eta/2$ unsatisfiable. The formal $\tau$ also exceeds $e$ , so that $\log\log t>0$ on the window, and $t$ ranges over integers.
Assumptions. Assumptions 1–3 appear exactly where the paper uses them: Lemma 22 and Theorem 8 assume all three, Lemma 19 and Corollary 20 only Assumption 1.

The source is the arXiv v4 preprint; the paper's proofs are in its §§8–9. Welcome contributions include the KL chain rule for adaptively scheduled Bernoulli observations, stationarity of the geometric law for the genie chain, and measurability of the trajectory.

Selected references

S. Krishnasamy, R. Sen, R. Johari, S. Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach, Operations Research 69(1), 2021; preprint arXiv:1604.06377v4. https://arxiv.org/abs/1604.06377
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794
S. Bubeck, V. Perchet, P. Rigollet, Bounded regret in stochastic multi-armed bandits, COLT 2013. https://arxiv.org/abs/1302.1611

9 thms3 active usersReviewed

Bandit Algorithms Operations Research Stochastic Systems·Captain: mikedeng1

Learning Unknown Service Rates in Queues 1: Every α-Consistent Scheduling Policy Has Average Queue-Regret at Least λ_min D(μ)(1−α)(K−1)/(8t) for Infinitely Many tResearch Paper

Motivation

Many service systems must route work to servers whose quality is not known in advance: crowdsourcing platforms matching job types to worker types, wireless schedulers assigning users to channels, call centers routing request classes to agent pools. Learning the unknown service rates is a multi-armed bandit problem, but the cost of a bad decision is not a lost reward. It is a longer queue, and a queue can recover from past mistakes when it empties. Krishnasamy, Sen, Johari and Shakkottai (arXiv:1604.06377v4, Operations Research 2021, doi:10.1287/opre.2020.1995) measure the cost of learning by the queue-regret, the expected excess queue length relative to a genie that knows the rates. Their analysis shows two regimes. Early on the regret grows like a bandit regret. After the system has learned enough to stabilize, queues regenerate and the regret decays. This mission formalizes their lower bound for the second regime: no reasonable learning policy can make the late-stage queue-regret decay faster than $1/t$ .

The lower bound adapts the classical consistency-based bandit lower bounds of Lai and Robbins (1985) and their non-asymptotic, hypothesis-testing form (Bubeck, Perchet and Rigollet 2013) to queue dynamics. The step from counts of suboptimal schedules to queue lengths is specific to queues.

Setting

A switch has $U$ queues and $K\ge U$ servers. Time is slotted, $t=1,2,\dots$ . In slot $t$ queue $u$ receives an arrival $A_u(t)\sim\mathrm{Bernoulli}(\lambda_u)$ , and the link between queue $u$ and server $k$ offers a service $R_{uk}(t)\sim\mathrm{Bernoulli}(\mu_{uk})$ . All of these are independent, and i.i.d. over slots. A problem instance is the pair $(\lambda,\mu)$ , with every entry in $[0,1]$ .

In every slot the scheduler picks a matching $\kappa(t)$ : queue $u$ is assigned server $\kappa_u(t)$ , and distinct queues get distinct servers. The scheduler knows neither $\lambda$ nor $\mu$ . Its decision in slot $t$ may use the past schedules, the services observed on the scheduled links in slots $1,\dots,t-1$ , and its own randomness. Queue $u$ receives $S_u(t)=R_{u\kappa_u(t)}(t)$ and evolves as

Q_u(t)=\big(Q_u(t-1)+A_u(t)-S_u(t)\big)^+ .

Assumption 1 (unique optimal matching) says that each queue $u$ has a unique best server $k^*_u$ , and that $u\ne u'$ implies $k^*_u\ne k^*_{u'}$ . The genie always schedules $k^*$ . Its queues $Q^*$ start from the same $Q(0)$ and see the same arrivals and offered services, with $S^*_u(t)=R_{uk^*_u}(t)$ . The queue-regret of queue $u$ is $\Psi_u(t)=\mathbb E[Q_u(t)-Q^*_u(t)]$ .

Write $\mu^*_u=\mu_{uk^*_u}$ , $\Delta_{uk}=\mu^*_u-\mu_{uk}$ , $\Delta=\min_{u,k\ne k^*_u}\Delta_{uk}$ , $\mu_{\min}=\min_{u,k}\mu_{uk}$ , $\mu^*=\max_{u,k}\mu_{uk}$ , $\lambda_{\min}=\min_u\lambda_u$ . With the Bernoulli divergence $\mathrm{KL}(p,q)=p\log\frac pq+(1-p)\log\frac{1-p}{1-q}$ , display (2) of the paper defines

D(\mu)=\frac{\Delta}{\mathrm{KL}\big(\mu_{\min},\tfrac{\mu^*+1}{2}\big)} .

Let $T_{uk}(t+1)=\sum_{s=1}^t\mathbf 1\{\kappa_u(s)=k\}$ . For $\alpha\in(0,1)$ , a policy is $\alpha$ -consistent (Definition 2) if for every instance with a unique optimal matching there is a constant $C(\lambda,\mu)$ with $\mathbb E[T_{uk}(t+1)]\le C(\lambda,\mu)\,t^\alpha$ for all $u$ and all $k\ne k^*_u$ . Consistency rules out policies tuned to one instance, such as "always schedule a fixed matching", which would have zero regret on that instance and linear regret elsewhere.

Formalization targets

Goal: Theorem 3 (p. 12)

For every instance with a unique optimal matching, every law of the initial queue lengths, every $\alpha\in(0,1)$ and every $\alpha$ -consistent policy:

\frac1U\sum_{u\in[U]}\Psi_u(t)\;\ge\;\frac{\lambda_{\min}}{8}D(\mu)(1-\alpha)(K-1)\cdot\frac1t\quad\text{for infinitely many } t,

\Psi_u(t)\;\ge\;\frac{\lambda_{\min}}{8}D(\mu)(1-\alpha)\max\{U-1,\,2(K-U)\}\cdot\frac1t\quad\text{for infinitely many } t,\ \text{for each } u.

Milestones

Lemma 18 (p. 37), the Bretagnolle–Huber inequality $P(\mathcal A)+Q(\mathcal A^c)\ge\frac12e^{-\mathrm{KL}(P\|Q)}$ . It is already proved on the platform and enters as a reference.
Lemma 19 (p. 37). For $t>\tau$ : $\mathbb E[T_{uk}(t+1)]+\sum_{u'\ne u}\mathbf 1\{k^*_{u'}=k\}\mathbb E[T_{u'k^*_u}(t+1)]\ge\frac{(1-\alpha)\log t-\log(4KC)}{\mathrm{KL}(\mu_{\min},(\mu^*+1)/2)}$ .
Corollary 20 (p. 39). The same bound summed over all queues, over one queue, and over the servers that are optimal for no queue.
Lemma 21 (p. 41). For any policy, $\Psi_u(t)\ge\lambda_u\sum_{k\ne k^*_u}\Delta_{uk}\,\mathbb P[\kappa_u(t)=k]$ .
Fact 1 (p. 42). If $\sum_{m\le n}a_m\ge C\log n$ eventually, then $a_n\ge C/(2n)$ infinitely often.

A companion item, Lemma 1 (p. 10), states $\Psi_u(t)\le\sum_{l=1}^t\mathbb E[S^*_u(l)-S_u(l)]$ : queue-regret never exceeds the bandit regret.

Significance

Theorem 3 shows that the paper's Q-UCB algorithm, whose late-stage queue-regret is $O(\log^3 t/t)$ (Theorem 5), is optimal in its dependence on $t$ up to polylogarithmic factors. It also separates queue-regret from bandit regret. The bandit regret of a consistent policy grows like $\log t$ , while the queue-regret decays to zero. The cost of learning in a queue is transient, but it cannot vanish faster than $1/t$ . The theorem holds for every initial law of the queues, so it does not depend on the system starting in steady state.

The proof is complete in the source (§9.1, pp. 37–42). As far as we know none of it is machine-checked. A formal development would also give the first formal bandit lower bound in which the consistency class must contain the alternative instances of a change-of-measure argument, here instances with two optimal servers swapped, together with a reusable model of a learning scheduler on a switch.

Difficulty

The obvious route is to bound the regret of each slot by the probability of a suboptimal schedule (Lemma 21), and to bound the number of suboptimal schedules from below by a Lai–Robbins argument. Both steps resist direct proof.

For the first step, $Q$ and $Q^*$ share arrivals and services but are not ordered pathwise, because the policy's services are independent across links. A comparison exists only in distribution.

For the second step, the alternative instance must again satisfy Assumption 1, so a single service rate cannot simply be raised. When server $k$ is the best server of another queue $u'$ , the best servers of $u$ and $u'$ must be swapped, and the divergence decomposition then involves two links.

The final step goes from a cumulative bound to an "infinitely often" bound, and only from a logarithmic lower bound on partial sums. A lower bound on cumulative regret does not give a bound for every large $t$ .

Formalization scope

Queues and servers are Fin U and Fin K (0-based), with $1\le U\le K$ . The hypothesis $K\ge2$ is added: for $K=1$ the policy and the genie coincide and both sides are zero, and the minimum defining $\Delta$ would range over an empty set. Slots are 1-based.

The probability space is canonical: $\Omega=\mathbb N^U\times\text{Seed}^{\mathbb N}$ with law $\nu\otimes\mathrm{Unif}^{\otimes\mathbb N}$ . A seed holds one uniform per arrival, one per link and one for the scheduler, and $A_u(t)=\mathbf 1\{W_u(t)\le\lambda_u\}$ , $R_{uk}(t)=\mathbf 1\{V_{uk}(t)\le\mu_{uk}\}$ . A policy maps the history of past schedules and observed services, together with a private uniform seed, to a matching. The only constraint is measurability in the seed, so every randomized history-dependent policy is covered. The law $\nu$ of $Q(0)$ is arbitrary, as the paper notes after Theorem 3, so Assumption 3 is not used. Assumption 2 (stability under the optimal matching, $\lambda_u<\mu^*_u$ for every $u$ ), which the paper assumes whenever queue-regret is evaluated (p. 8), is a hypothesis of Theorem 3 and of Lemmas 1 and 21. Lemma 19 and Corollary 20 concern schedule counts, which do not depend on the arrival rates.

$\Psi_u(t)$ is a Bochner integral of $Q_u(t)-Q^*_u(t)$ , which is bounded by $t$ . Expected counts are integrals under the seed law, since the schedule never observes arrivals or $Q(0)$ . $D(\mu)$ and $1/\mathrm{KL}$ are set to $0$ when $\mu^*=1$ , where the divergence is $+\infty$ . Corollary 20(c)'s $\sum_{k>U}$ becomes the sum over servers outside the range of $k^*$ . Fact 1 is stated for every real sequence: the printed "bounded" is not needed and does not hold in the application. "For infinitely many $t$ " is ∃ᶠ t in atTop.

$\alpha$ -consistency quantifies over every service matrix in $[0,1]^{U\times K}$ satisfying Assumption 1, and its constant is chosen after the instance. Requiring consistency on the given instance only would make Theorem 3 false, because the genie's own policy has $\Psi\equiv0$ . A constant chosen before the instance would make the hypothesis unsatisfiable.

A complete development needs the canonical seed space and its measurability, a chain rule for the KL divergence of the history laws, the Bretagnolle–Huber inequality (available), and an elementary harmonic-sum estimate. The switch model and the consistency class are reusable for the paper's early-stage lower bound and its upper bound. Proofs of any milestone, and alternative proofs of Lemma 21 that avoid the coupling, are welcome.

The source is the arXiv v4 preprint; the paper's proofs are in its §§8–9.

Selected references

S. Krishnasamy, R. Sen, R. Johari, S. Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach, Operations Research 69(1), 2021. Preprint arXiv:1604.06377v4. https://arxiv.org/abs/1604.06377v4
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6(1), 1985. https://doi.org/10.1016/0196-8858(85)90002-8
A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009 (Lemma 2.6). https://doi.org/10.1007/b13794
S. Bubeck, V. Perchet, P. Rigollet, Bounded regret in stochastic multi-armed bandits, COLT 2013. https://arxiv.org/abs/1302.1611

8 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Distributionally Robust Joint Chance Constraints with Second-Order Moment Information II: Over Scaling Parameters, Worst-Case CVaR Is Essentially Exact for Joint Chance ConstraintsResearch Paper

Motivation

A chance constraint asks that a decision $x\in\mathbb R^n$ satisfy uncertain inequalities with high probability. In the setting of Zymler, Kuhn and Rustem (Math. Program. 137, 2013), $m$ affine inequalities $y_i^0(x)+y_i(x)^\top\tilde\xi\le0$ , whose coefficients depend affinely on $x$ , must hold jointly with probability at least $1-\epsilon$ . Joint chance constraints appear wherever several safety conditions must hold at once: portfolio and network design, water reservoir operation, production planning under uncertain demand. They are hard for two reasons. Checking feasibility of a fixed $x$ requires a multi-dimensional integral, and the feasible set is typically nonconvex (Prékopa 1995). Moreover the distribution of $\tilde\xi$ is rarely known; often only its mean and covariance can be estimated.

The distributionally robust version requires the constraint for every distribution consistent with the known first and second moments. A standard tractable inner approximation replaces the probability by a worst-case Conditional Value-at-Risk (CVaR) of a single loss. For a joint constraint this needs the $m$ inequalities aggregated into one loss, and the choice of aggregation decides how much is lost.

Timeline. Charnes and Cooper (1959) and Miller and Wagner (1965) introduced chance constraints; Prékopa proved convexity of joint constraints with log-concave right-hand sides. Nemirovski and Shapiro (2006) studied convex (CVaR-type) approximations. El Ghaoui, Oks and Oustry (2003) and Calafiore and El Ghaoui (2006) gave exact SDP and SOCP reformulations of individual robust chance constraints under moment information. Chen, Sim, Sun and Teo (2010) introduced scaling parameters and an SOCP approximation of joint constraints. Zymler, Kuhn and Rustem (2013) showed that the worst-case CVaR of the scaled max-loss admits an exact LMI representation and that, with the scaling parameters free, it is essentially exact.

Setting

Let $\tilde\xi$ be a random vector in $\mathbb R^k$ . Fix $\mu\in\mathbb R^k$ and a positive definite $\Sigma\in\mathbb S^k$ , and let $\mathcal P$ be the set of all probability measures on $\mathbb R^k$ with finite second moments, mean $\mu$ and covariance $\Sigma$ . The second-order moment matrix is

\Omega=\begin{bmatrix}\Sigma+\mu\mu^\top&\mu\\ \mu^\top&1\end{bmatrix}.

For a measurable loss $L$ , a probability measure $\mathbb P$ and $\epsilon\in(0,1)$ , the CVaR is

\mathbb P\text{-}\mathrm{CVaR}_\epsilon(L(\tilde\xi))=\inf_{\beta\in\mathbb R}\Big\{\beta+\tfrac1\epsilon\,\mathbb E_{\mathbb P}\big((L(\tilde\xi)-\beta)^+\big)\Big\},

and the worst-case CVaR is its supremum over $\mathbb P\in\mathcal P$ .

The data are vectors $a_i^0,a_i^j\in\mathbb R^n$ and scalars $b_i^0,b_i^j$ for $i=1,\dots,m$ , $j=1,\dots,k$ , with $y_i^j(x)=(a_i^j)^\top x-b_i^j$ and $y_i(x)=[y_i^1(x),\dots,y_i^k(x)]^\top$ . The sets of interest are:

the robust joint chance constraint set $\mathcal X^{\mathrm{JCC}}=\{x:\inf_{\mathbb P\in\mathcal P}\mathbb P(y_i^0(x)+y_i(x)^\top\tilde\xi\le0\ \forall i)\ge1-\epsilon\}$ ;
its strict version $\mathcal X^{\mathrm{JCC}}_\circ$ , with every $\le0$ replaced by $<0$ ;
for scaling parameters $\alpha\in\mathcal A=\{\alpha\in\mathbb R^m:\alpha_i>0\ \forall i\}$ , the worst-case CVaR approximation $\mathcal Z^{\mathrm{JCC}}(\alpha)=\{x:\mathcal J(x,\alpha)\le0\}$ with

\mathcal J(x,\alpha)=\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-}\mathrm{CVaR}_\epsilon\Big(\max_{i=1,\dots,m}\alpha_i\big(y_i^0(x)+y_i(x)^\top\tilde\xi\big)\Big);

the union $\mathcal Z^{\mathrm{JCC}}=\bigcup_{\alpha\in\mathcal A}\mathcal Z^{\mathrm{JCC}}(\alpha)$ .

Formalization targets

Goal: Theorem 3.6 (p. 20)

\mathcal X^{\mathrm{JCC}}_\circ\subseteq\mathcal Z^{\mathrm{JCC}}\subseteq\mathcal X^{\mathrm{JCC}}.

The goal makes no regularity assumption on the constraint functions; it holds for all data, all $m\ge1$ , all $\mu$ , all $\Sigma\succ0$ and all $\epsilon\in(0,1)$ .

Milestones

(7), p. 6: for every measurable loss $L$ , $\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-}\mathrm{CVaR}_\epsilon(L)\le0$ implies $\inf_{\mathbb P\in\mathcal P}\mathbb P(L\le0)\ge1-\epsilon$ .
p. 17: $\mathcal Z^{\mathrm{JCC}}(\alpha)\subseteq\mathcal X^{\mathrm{JCC}}$ for every $\alpha\in\mathcal A$ .
Lemma A.1, p. 30: $\sup_{\mathbb P\in\mathcal P}\mathbb E_{\mathbb P}(f^+)=\inf\{\langle\Omega,M\rangle:M\succeq0,\ [\xi^\top\,1]M[\xi^\top\,1]^\top\ge f(\xi)\ \forall\xi\}$ for every measurable $f$ .
(31), p. 16: $\mathcal J(x,\alpha)=\inf_\beta\{\beta+\frac1\epsilon\sup_{\mathbb P\in\mathcal P}\mathbb E_{\mathbb P}([\max_i\alpha_i(y_i^0(x)+y_i(x)^\top\tilde\xi)-\beta]^+)\}$ .
Theorem 3.3, p. 16: $\mathcal Z^{\mathrm{JCC}}(\alpha)$ is the set of $x$ for which some $(\beta,M)$ satisfies $\beta+\frac1\epsilon\langle\Omega,M\rangle\le0$ , $M\succeq0$ and the $m$ LMIs

M-\begin{bmatrix}0&\tfrac12\alpha_iy_i(x)\\ \tfrac12\alpha_iy_i(x)^\top&\alpha_iy_i^0(x)-\beta\end{bmatrix}\succeq0 .

Lemma A.2, p. 31: for every Borel $\mathcal S$ , $\sup_{\mathbb P\in\mathcal P}\mathbb P(\tilde\xi\in\mathcal S)=\inf\{\langle\Omega,M\rangle:M\succeq0,\ [\xi^\top\,1]M[\xi^\top\,1]^\top\ge1\ \forall\xi\in\mathcal S\}$ .
Lemma 2.2 (S-lemma), p. 8: the lossless S-procedure for one strictly feasible quadratic constraint, already proved on the platform.
(40), p. 21: $\mathcal X^{\mathrm{JCC}}_\circ$ is the set of $x$ for which some $M\succeq0$ and $\alpha>0$ satisfy $\langle\Omega,M\rangle\le\epsilon$ and the LMIs of Theorem 3.3 with $\beta=-1$ .

Significance

The result. The worst-case CVaR approximation $\mathcal Z^{\mathrm{JCC}}(\alpha)$ is an LMI-representable inner approximation of the robust joint chance constraint for each fixed $\alpha$ (Theorem 3.3). Theorem 3.6 says that optimizing over $\alpha$ loses at most the boundary between the strict and the non-strict constraint: no tractable family based on the scaled max-loss can be uniformly better. Remark 3.2 of the paper observes that, for well-specified constraints, $\mathcal X^{\mathrm{JCC}}$ and $\mathcal X^{\mathrm{JCC}}_\circ$ differ by a Lebesgue-null set. Together with the inclusions of §3.3, it places the approximation at least as tight as the Bonferroni and Chen–Sim–Sun–Teo approximations and as close to $\mathcal X^{\mathrm{JCC}}$ as the strict constraint allows; it is the reason to treat $\alpha$ as a decision variable.

Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. None of it is machine-checked. A formal proof requires moment-problem duality for the full moment set (Lemmas A.1 and A.2, which the paper sketches by citing Isii and Calafiore–El Ghaoui), a minimax interchange over a non-compact set of distributions, and the S-lemma, which is available on the platform. Each milestone is reusable: Lemmas A.1 and A.2 are the generalized Chebyshev bounds behind most of moment-based distributionally robust optimization.

Difficulty

The second inclusion is the conservativeness of CVaR, a Markov-type argument. The first inclusion is where the content lies. It requires the worst-case probability of a union of half-spaces to be an attained semidefinite program value, and an S-lemma certificate for each row. The obvious proof applies the S-lemma to every row, but the S-lemma's converse needs a strictly feasible point, which a row with $y_i(x)=0$ lacks; such rows must be treated separately. Similarly, the SDP representations are stated as existence of a feasible point, so the infima must be shown to be attained. The interchange of the supremum over $\mathcal P$ and the infimum over $\beta$ in (31) cannot cite weak compactness: $\mathcal P$ is not weakly compact, since mass can escape to infinity while the second moments stay fixed.

Formalization scope

$\mathbb R^k$ is Fin k → ℝ; matrices in $\mathbb S^{k+1}$ are indexed by Fin k ⊕ Unit with the extra coordinate last; $M\succeq0$ is Matrix.PosSemidef (which includes symmetry); $\langle X,Y\rangle=\operatorname{Tr}(XY)$ .
$\mathcal P$ consists of probability measures with every coordinate in $L^2$ , mean $\mu$ and covariance $\Sigma$ (the published MomentDRO.Conf definitions), so moments are genuine integrals.
CVaR, the worst-case CVaR, worst-case expectations and SDP values take values in the extended reals. The expectation of a positive part is a lower Lebesgue integral. A supremum over $\mathcal P$ or an infimum over an infeasible set may be infinite.
Standing assumptions, carried by every theorem: $\Sigma\succ0$ and $\epsilon\in(0,1)$ (p. 5). The theorems about the max-loss also assume $m\ge1$ , implicit in the maximum over $i=1,\dots,m$ . Milestone (7) assumes the loss measurable, as on p. 5.
$\alpha\in\mathcal A$ is componentwise strict positivity, $\alpha_i>0$ for all $i$ , not the product-order $\alpha>0$ .
A real-valued supremum would be $0$ on an unbounded set and make " $\mathcal J(x,\alpha)\le0$ " true by a junk value. The extended-real encoding rules this out, and the moment set is nonempty under $\Sigma\succ0$ , so no statement holds vacuously.
Printed slips: the lower-left block " $\tfrac12\alpha_iy_i^\top$ " of (30) is read as $\tfrac12\alpha_iy_i(x)^\top$ ; " $\bigcup_{\alpha\in\mathcal S}$ " on p. 20 is read as $\bigcup_{\alpha\in\mathcal A}$ ; the index range " $i=1,\dots,n$ " on p. 2 is read as $i=1,\dots,m$ . The printed homogeneous S-lemma is replaced by the inhomogeneous one the proofs use.
Contributions welcome: the moment-duality lemmas, the minimax interchange (31), attainment of the SDP infima, and the degenerate-row case of (40).

Selected references

S. Zymler, D. Kuhn, B. Rustem, Distributionally robust joint chance constraints with second-order moment information, Math. Program. 137 (2013) 167–198. https://doi.org/10.1007/s10107-011-0494-7
W. Chen, M. Sim, J. Sun, C.-P. Teo, From CVaR to uncertainty set: implications in joint chance-constrained optimization, Oper. Res. 58 (2010) 470–485. https://doi.org/10.1287/opre.1090.0712
G. Calafiore, L. El Ghaoui, On distributionally robust chance-constrained linear programs, J. Optim. Theory Appl. 130 (2006) 1–22. https://doi.org/10.1007/s10957-006-9084-x
L. El Ghaoui, M. Oks, F. Oustry, Worst-case value-at-risk and robust portfolio optimization: a conic programming approach, Oper. Res. 51 (2003) 543–556. https://doi.org/10.1287/opre.51.4.543.16101
A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17 (2006) 969–996. https://doi.org/10.1137/050622328
R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, J. Risk 2 (2000) 21–41. https://doi.org/10.21314/JOR.2000.038
A. Prékopa, Stochastic Programming, Kluwer, 1995. https://doi.org/10.1007/978-94-017-3087-7

13 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Distributionally Robust Joint Chance Constraints with Second-Order Moment Information I: Worst-Case CVaR Is Exact for Individual Chance Constraints with Concave or Quadratic LossesResearch Paper

Motivation

A chance constraint asks that an uncertain constraint hold with high probability: a decision is acceptable if the loss $L(\tilde\xi)$ it incurs is nonpositive with probability at least $1-\epsilon$ . Chance constraints appear in portfolio selection, power-system dispatch, inventory control and engineering design, wherever an occasional violation is tolerable but a frequent one is not. Two obstacles stand in the way of using them. The distribution of $\tilde\xi$ is rarely known exactly, and even when it is, the feasible set of a chance constraint is in general nonconvex and hard to compute.

Distributionally robust chance constraints address the first obstacle by requiring the constraint to hold for every distribution consistent with the available information. Zymler, Kuhn and Rustem (Math. Program. 137, 2013) take that information to be the mean and the covariance of $\tilde\xi$ . The standard way around the second obstacle is to replace the probability by the Conditional Value-at-Risk (CVaR) of Rockafellar and Uryasev (J. Risk 2, 2000): a nonpositive CVaR implies the chance constraint, and the worst-case CVaR over a moment set can be computed by semidefinite programming. The approximation is conservative, and the question this mission formalizes is when it loses nothing.

Timeline. Isii (Ann. Inst. Statist. Math. 12, 1960) established strong duality for moment problems, the basis of generalized Chebyshev bounds; Calafiore, Topcu and El Ghaoui (Systems & Control Letters 58, 2009) gave the semidefinite form of the worst-case probability of a set under mean and covariance information that the paper uses as Lemma A.2. El Ghaoui, Oks and Oustry (Oper. Res. 51, 2003) computed the worst-case Value-at-Risk of a portfolio under mean and covariance information. Calafiore and El Ghaoui (J. Optim. Theory Appl. 130, 2006) showed that a distributionally robust individual chance constraint with a loss affine in $\tilde\xi$ is a second-order cone constraint. Zymler, Kuhn and Rustem (2013) showed that the worst-case CVaR approximation is exact for every continuous loss that is concave or quadratic in $\tilde\xi$ (Theorem 2.2), which is the goal of this mission, and extended the approach to joint chance constraints (the companion mission II).

Setting

Let $\tilde\xi$ be a random vector in $\mathbb R^k$ . Fix a mean vector $\mu\in\mathbb R^k$ and a covariance matrix $\Sigma\in\mathbb S^k$ with $\Sigma\succ0$ (positive definite). The moment set $\mathcal P$ is the set of all probability distributions $\mathbb P$ on $\mathbb R^k$ with finite second moments, $\mathbb E_{\mathbb P}[\tilde\xi]=\mu$ and $\mathbb E_{\mathbb P}[(\tilde\xi-\mu)(\tilde\xi-\mu)^\top]=\Sigma$ . The second-order moment matrix is

\Omega=\begin{bmatrix}\Sigma+\mu\mu^\top & \mu\\ \mu^\top & 1\end{bmatrix},

and $\langle X,Y\rangle=\operatorname{Tr}(XY)$ is the trace scalar product.

Fix a tolerance $\epsilon\in(0,1)$ and a loss $L:\mathbb R^k\to\mathbb R$ . Write $x^+=\max\{x,0\}$ . The CVaR of $L(\tilde\xi)$ under $\mathbb P$ is

\mathbb P\text{-}\mathrm{CVaR}_\epsilon(L(\tilde\xi))=\inf_{\beta\in\mathbb R}\Big\{\beta+\frac1\epsilon\,\mathbb E_{\mathbb P}\big((L(\tilde\xi)-\beta)^+\big)\Big\},

and the worst-case CVaR is its supremum over $\mathbb P\in\mathcal P$ . The distributionally robust individual chance constraint is $\inf_{\mathbb P\in\mathcal P}\mathbb P(L(\tilde\xi)\le0)\ge1-\epsilon$ . The worst-case Value-at-Risk is

\mathrm{WC\text{-}VaR}_\epsilon(L(\tilde\xi))=\inf\Big\{\gamma\in\mathbb R:\ \inf_{\mathbb P\in\mathcal P}\mathbb P\big(L(\tilde\xi)\le\gamma\big)\ge1-\epsilon\Big\}.

A loss is quadratic if $L(\xi)=\xi^\top Q\xi+q^\top\xi+q^0$ , with no sign condition on $Q$ .

Formalization targets

Goal: Theorem 2.2

For a continuous loss $L$ that is either concave or (possibly nonconcave) quadratic in $\xi$ ,

\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-}\mathrm{CVaR}_\epsilon\big(L(\tilde\xi)\big)\le0\iff\inf_{\mathbb P\in\mathcal P}\mathbb P\big(L(\tilde\xi)\le0\big)\ge1-\epsilon .

The implication from left to right holds for every loss; the content of the theorem is the converse.

Milestones

(15): for every measurable $L$ , the chance constraint holds iff $\mathrm{WC\text{-}VaR}_\epsilon(L(\tilde\xi))\le0$ .
Lemma A.2: for a Borel set $\mathcal S$ , $\sup_{\mathbb P\in\mathcal P}\mathbb P(\tilde\xi\in\mathcal S)=\inf\{\langle\Omega,M\rangle: M\succeq0,\ [\xi^\top 1]M[\xi^\top 1]^\top\ge1\ \forall\xi\in\mathcal S\}$ .
Lemma 2.1 (nonlinear Farkas lemma) for convex functions under a Slater point.
Lemma 2.2 (the $\mathcal S$ -lemma), through the platform's proved lossless S-procedure.
(20): for the losses of Theorem 2.2,

\mathrm{WC\text{-}VaR}_\epsilon(L(\tilde\xi))=\inf\Big\{\beta+\tfrac1\epsilon\langle\Omega,M\rangle:\ M\succeq0,\ [\xi^\top\ 1]M[\xi^\top\ 1]^\top+\beta-L(\xi)\ge0\ \forall\xi\Big\}.

Lemma A.1: $\sup_{\mathbb P\in\mathcal P}\mathbb E_{\mathbb P}((f(\tilde\xi))^+)=\inf\{\langle\Omega,M\rangle: M\succeq0,\ [\xi^\top 1]M[\xi^\top 1]^\top\ge f(\xi)\ \forall\xi\}$ for measurable $f$ .
The display after (20): for the losses of Theorem 2.2, the worst-case CVaR equals $\inf_\beta\{\beta+\frac1\epsilon\sup_{\mathbb P}\mathbb E_{\mathbb P}((L(\tilde\xi)-\beta)^+)\}$ and the value of the program in (20).
The identity of p. 9: for the losses of Theorem 2.2, the worst-case CVaR equals the worst-case VaR.

Significance

The theorem says that for concave and for quadratic losses the worst-case CVaR constraint, which is a linear matrix inequality in the decision through (20), describes exactly the feasible set of the distributionally robust chance constraint. Its affine special case (Corollary 2.1 of the paper) gives an exact semidefinite representation of robust individual chance constraints with affine dependence on the uncertainty, the case most used in robust portfolio and engineering models. The same equality between worst-case CVaR and worst-case VaR is the starting point of the paper's treatment of joint chance constraints, where an exact representation is obtained by optimizing over scaling parameters (mission II). The quadratic case covers losses such as portfolio variance terms or quadratic constraint functions, which are neither convex nor concave in general.

The results are proved in the paper, but parts of the argument are sketches. Lemmas A.1 and A.2 are strong duality theorems for moment problems that the paper cites from Isii and from Calafiore et al. rather than proves, and the interchange of supremum and infimum in the worst-case CVaR is justified by a citation to a stochastic saddle-point theorem. To our knowledge none of these results has a machine-checked proof. A formalization produces a checked moment-duality theorem with given mean and covariance, a nonlinear Farkas lemma, and a complete proof of the exactness theorem.

Difficulty

The direction from the worst-case CVaR constraint to the chance constraint is elementary. The converse cannot be obtained distribution by distribution: for a single distribution the CVaR is strictly larger than the VaR in general, and for a convex piecewise-linear loss the worst-case equivalence fails (Example 2.1 of the paper). The identity therefore depends on the specific moment set and the specific loss classes, and passes through two infinite-dimensional dualities. The moment set $\mathcal P$ is not compact in the weak topology, since mass can escape to infinity while the first two moments stay fixed, so the minimax interchange in the worst-case CVaR does not follow from a standard compact minimax theorem. Lemmas A.1 and A.2 are stated for an arbitrary measurable function and an arbitrary Borel set; their strong duality uses $\Sigma\succ0$ in an essential way. Finally, the semi-infinite constraint "for all $\xi$ with $L(\xi)>\gamma$ " involves a strict inequality on a nonconvex set, and turning it into a matrix inequality is where concavity or quadraticity of $L$ enters.

Formalization scope

$\mathbb R^k$ is Fin k → ℝ; matrices in $\mathbb S^{k+1}$ are indexed by Fin k ⊕ Unit with the extra coordinate last, so that $[\xi^\top 1]M[\xi^\top 1]^\top$ is liftQuad M ξ. $\Omega$ is built from the published ConvexOptimization.symQuadBlock.
$\mathcal P$ is every probability measure with every coordinate in $L^2$ , mean $\mu$ and covariance $\Sigma$ (the published MomentDRO.Conf.HasSecondMoments, meanVec, covMat). It is not restricted to discrete laws, densities or a support set.
The standing assumptions $\Sigma\succ0$ and $\epsilon\in(0,1)$ are hypotheses of every theorem. Lemma 2.1 involves no distribution and does not carry them. Lemma A.1 needs measurability of $f$ and Lemma A.2 a Borel set, as printed; (15) is stated for every measurable loss.
CVaR, the worst-case CVaR, the worst-case expectation, the worst-case VaR and the values of the semidefinite programs are extended reals. Expectations of positive parts are lower Lebesgue integrals and may be $+\infty$ ; an infimum over an empty feasible set is $+\infty$ . A formalization with real-valued suprema would assign $0$ to an unbounded worst-case CVaR and make the constraint "worst-case CVaR $\le 0$ " hold by a default value; this encoding rules that out.
A quadratic loss is $\xi^\top Q\xi+q^\top\xi+q^0$ with $Q$ neither symmetric nor definite; concavity is on all of $\mathbb R^k$ .
The printed $\mathcal S$ -lemma (homogeneous forms, general $p$ ) is replaced by the platform's proved lossless S-procedure for two inhomogeneous quadratics under a Slater point, which is the form the proof uses.

A complete development needs moment-problem duality on $\mathbb R^k$ , a convex Farkas lemma, and the S-procedure (already proved on the platform). The first two are reusable beyond this mission, in particular by mission II, which uses Lemmas A.1 and A.2 verbatim. Proofs of any milestone are welcome independently.

Selected references

S. Zymler, D. Kuhn, B. Rustem, Distributionally robust joint chance constraints with second-order moment information, Mathematical Programming 137 (2013) 167–198. https://doi.org/10.1007/s10107-011-0494-7
R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2 (2000) 21–41. https://doi.org/10.21314/JOR.2000.038
K. Isii, The extrema of probability determined by generalized moments (I) bounded random variables, Annals of the Institute of Statistical Mathematics 12 (1960) 119–134 (reference [14] of the paper).
G. Calafiore, U. Topcu, L. El Ghaoui, Parameter estimation with expected and residual-at-risk criteria, Systems & Control Letters 58 (2009) 39–46 (reference [7] of the paper).
L. El Ghaoui, M. Oks, F. Oustry, Worst-case value-at-risk and robust portfolio optimization: a conic programming approach, Operations Research 51 (2003) 543–556. https://doi.org/10.1287/opre.51.4.543.16101
G. C. Calafiore, L. El Ghaoui, On distributionally robust chance-constrained linear programs, Journal of Optimization Theory and Applications 130 (2006) 1–22. https://doi.org/10.1007/s10957-006-9084-x
I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007) 371–418. https://doi.org/10.1137/S003614450444614X

13 thms3 active usersReviewed

Linear algebra Machine Learning Numerical Analysis+2·Captain: mikedeng1

An Introduction to Matrix Concentration Inequalities III: A Matrix Sampling Estimator Satisfies E‖R̄ₙ − B‖ ≤ √(2m₂(R)log(d₁ + d₂)/n) + 2L log(d₁ + d₂)/(3n)Textbook

Motivation

Matrix approximation replaces a large or complicated matrix with a random matrix that is easier to store or compute. Averaging independent realizations improves accuracy while retaining the structure of each realization. Examples in Tropp's monograph include sparse approximations and randomized matrix products. The practical question is how the number of samples, the size of one sample, and its second moment control the spectral norm error. Tropp, §6.2

The book proves a matrix Bernstein inequality in Theorem 6.1.1, then applies it to an empirical matrix average in Corollary 6.2.1. Theorem 6.1.1 is already posed as TroppMatrixConcentration.matrix_bernstein on Prove2Me and is currently Open. This mission records the application with its own hypotheses and constants. The capstone concerns the estimator that a reader would construct, rather than a sum of abstract centered summands. Tropp, §§6.1–6.2

Setting

Let $B$ be a fixed complex $d_1\times d_2$ matrix. A sample matrix $R$ has the same size, has expectation $B$ , and has spectral norm at most $L$ almost surely. The equality $\mathbb ER=B$ makes one sample an unbiased estimate of $B$ . The almost-sure bound limits the size of every sample except on a probability-zero set. The dimensions $d_1,d_2$ are positive integers, and $n$ is a positive sample count.

Take independent copies $R_1,\ldots,R_n$ with the distribution of $R$ . Their matrix sampling estimator is

\overline R_n=\frac1n\sum_{k=1}^nR_k.

For any rectangular matrix $A$ , $A^*$ denotes its conjugate transpose and $\|A\|$ its spectral norm. The per-sample second moment is

m_2(R)=\max\{\|\mathbb E(RR^*)\|,\|\mathbb E(R^*R)\|\}.

Both terms matter for a rectangular matrix: $RR^*$ and $R^*R$ act on different coordinate spaces. All expectations of matrices are entrywise expectations, represented by Bochner integrals in Lean. The almost-sure norm bound guarantees the moments used here are finite. Tropp, equations (6.2.4)–(6.2.6)

Formalization targets

Empirical matrix approximation

Corollary 6.2.1 gives an expectation estimate and a tail estimate for the same estimator. For every real $t\ge0$ ,

\mathbb E\|\overline R_n-B\|\le \sqrt{\frac{2m_2(R)\log(d_1+d_2)}{n}}+ \frac{2L\log(d_1+d_2)}{3n},

\mathbb P\{\|\overline R_n-B\|\ge t\}\le (d_1+d_2)\exp\left(\frac{-nt^2/2}{m_2(R)+2Lt/3}\right).

The goal includes both bounds. The expectation estimate controls average error; the tail estimate controls the chance of an error above a chosen threshold. The dimension enters only through $\log(d_1+d_2)$ in the expectation bound and the factor $d_1+d_2$ in the tail bound. These are the book's constants, including the factors $2$ and $3$ in the linear terms. Tropp, Corollary 6.2.1, p. 81

Supporting statements

The milestone list follows Corollary 6.1.2 for uncentered summands, the bound $\|n^{-1}(R_k-B)\|\le2L/n$ , and the variance estimate $v(\overline R_n-B)\le m_2(R)/n$ . Equation (6.2.7) is a companion: a stated lower bound on $n$ implies $\mathbb E\|\overline R_n-B\|\le2\varepsilon$ for $\varepsilon>0$ . Tropp, pp. 77, 82

Significance

The result turns a bound on one random matrix into a quantitative guarantee for an empirical approximation. It lets a user choose a sample count for a target error and evaluate both average error and failure probability. The same framework is instantiated later in the monograph for matrix sparsification and multiplication; those applications depend on controlling $L$ and $m_2(R)$ for their particular sampling laws. Tropp, §§6.2–6.4

This is a known mathematical result proved in the book. Its Lean statement is an open formalization target. The mission adds a reusable empirical-mean definition and application statements built on the already published matrix spectral norm and rectangular second-moment definitions. A proof of the general matrix Bernstein theorem remains separate; the mission can draw on it when that platform theorem is proved.

Difficulty

The estimator error is a centered sum, but the sampling assumptions are given for an uncentered random matrix $R$ . Bounding the centered summands changes the uniform bound from $L$ to $2L/n$ . The variance parameter must be related to the second moment of one uncentered sample, with the correct $1/n$ scaling. Dropping the common-distribution condition would leave no relation between the samples' second moments and $m_2(R)$ . Applying scalar concentration to entries would not directly give the stated spectral norm bound or its dimension dependence. Tropp, proof of Corollary 6.2.1, p. 82

Formalization scope

Matrices are Matrix (Fin d₁) (Fin d₂) ℂ. The spectral norm and rectSecondMoment are imported from tc's published TroppMatrixConcentration definitions. An arbitrary probability space carries a measurable reference matrix $R_0$ and a finite family $R_k$ ; iIndepFun expresses independence and IdentDistrib expresses equality in law with $R_0$ . The estimator is the finite sum scaled by $n^{-1}$ . No particular sampling scheme or deterministic choice of $R$ is fixed: the formal goal requires only the source's unbiasedness and boundedness conditions.

The Lean statements explicitly require $d_1,d_2\ge1$ , $n>0$ , measurability, and the almost-sure form of $\|R\|\le L$ . These make the logarithm and inverse sample count meaningful and make the random matrix laws well behaved. For the uncentered Bernstein corollary, integrability of each $S_k$ is explicit because a bounded deviation from an unspecified mean alone does not establish that the mean exists. The goal also asserts integrability of its error norm, preventing a Bochner integral from silently taking Lean's default value for a nonintegrable function. The bound on $R$ supplies that integrability. When the denominator in a tail formula is zero, the displayed total real division gives a loose bound at the degenerate case; the source's probabilistic claim remains valid.

Contributions that formalize the centered-summand calculation, the variance estimate, or the transfer from the general matrix Bernstein theorem are within scope. The imported matrix and probability definitions are reusable in other matrix concentration missions. The local empirical-mean definition is reusable whenever a matrix estimator averages finitely many random samples.

Selected references

Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, arXiv:1501.01571v1, especially §§6.1–6.4.

7 thms3 active usersReviewed

Completed

Linear algebra Numerical Analysis Random Matrix Theory·Captain: mikedeng1

An Introduction to Matrix Concentration Inequalities II: A Random Row-and-Column Submatrix Z = PBR Satisfies E‖Z‖² ≤ 3(p/d)(r/n)‖B‖² Plus Logarithmic Row, Column and Entry TermsTextbook

Motivation and context

Large matrices are often reduced by retaining only some rows or columns. The reduced matrix is cheaper to store and apply, but its spectral norm can be distorted by a single unusually large row, column, or entry. A useful estimate must show both the average effect of sampling and the cost of these local concentrations. In §5.2 of Tropp's monograph, matrix Chernoff inequalities give numerical estimates for independently sampled columns and for independently sampled rows and columns. The latter is the capstone of this mission.

The general matrix Chernoff inequality, Theorem 5.1.1, is already an Open goal in tc's Chapter 5 mission on Prove2Me. The intrinsic-dimension Chernoff inequality, Theorem 7.2.1, is likewise Open in tc's Chapter 7 mission. This mission concerns the application statements that those chapter missions have not posed: the numerical bound (5.2.2), its three displayed intermediate estimates, and companion consequences in §§5.1.1, 5.2.1 and 7.2.2. The motivation for choosing this target is that it connects a general concentration result to a concrete random matrix model; its terms can be read directly from a deterministic input matrix.

Setting

Fix a complex matrix $B\in\mathbb C^{d\times n}$ with $d,n\ge1$ . For each row $j$ , let $\delta_j$ equal one when that row is retained and zero otherwise. For each column $k$ , let $\xi_k$ have the analogous meaning. The whole family is independent, with $\delta_j\sim\operatorname{Bernoulli}(p/d)$ and $\xi_k\sim\operatorname{Bernoulli}(r/n)$ , where $0\le p\le d$ and $0\le r\le n$ . Thus $p$ and $r$ are the expected numbers of retained rows and columns. Put

P=\operatorname{diag}(\delta_1,\ldots,\delta_d),\qquad R=\operatorname{diag}(\xi_1,\ldots,\xi_n),\qquad Z=PBR.

The zeros remain in the matrix: $Z$ has the same dimensions as $B$ , but entries in discarded rows or columns vanish. Write $b_{j:}$ for row $j$ , $b_{:k}$ for column $k$ , and $b_{jk}$ for an entry. Their vector norms are Euclidean, while $\|B\|$ and $\|Z\|$ denote the spectral operator norm. The source uses $\mathbb E$ for expectation over the selections. Its maxima range over all rows, columns or entries of $B$ , so a highly uneven matrix is distinguished from one whose mass is spread evenly.

The first milestone is the streamlined upper matrix Chernoff expectation bound. For a finite independent family of positive semidefinite Hermitian matrices $X_k$ with eigenvalues at most $L$ , let $Y=\sum_kX_k$ and $\mu_{\max}=\lambda_{\max}(\mathbb EY)$ . The bound uses the book's numerical constant $1.72$ . The subsequent milestones specialize this setting to the row and column selectors above. A separate companion states the lower bound with $0.63$ and the two weakened tail inequalities of §5.1.1.

Formalization targets

The goal is the exact displayed estimate (5.2.2), with the book's rounded constants:

\begin{aligned} \mathbb E\|PBR\|^2\le{}&3\frac pd\frac rn\|B\|^2 +2\frac{p\log d}{d}\max_k\|b_{:k}\|^2\\ &+2\frac{r\log n}{n}\max_j\|b_{j:}\|^2 +(\log d)(\log n)\max_{j,k}|b_{jk}|^2. \end{aligned}

Its milestone chain is (5.1.8), followed by (5.2.3), (5.2.4), and (5.2.5). These are the claims the text places immediately before the final estimate. They bound, respectively, the first column-selection stage, the norm of the row-selected matrix, and the largest column norm after row selection. The companion (5.2.1) gives both the top and least squared singular-value bounds for column selection alone. The companion from §7.2.2 replaces $\log d$ by $\log(2\operatorname{srank}(B))$ , where $\operatorname{srank}(B)=\|B\|_F^2/\|B\|^2$ is stable rank.

Significance

The goal separates four sources of size in a sampled matrix. The first term scales the squared spectral norm by the expected row and column retention fractions. The remaining terms record concentrations in a column, a row, and an individual entry. Consequently, the estimate can be evaluated from $B$ and the two sampling rates without specifying a distribution for $B$ itself. It is an expectation bound, not a claim that every realized submatrix is close to $B$ .

The formal development would make the application layer of Tropp's Chapter 5 available alongside tc's general, currently Open matrix Chernoff theorem. A proof of that general theorem does not itself identify the random projectors, their joint independence, or the deterministic quantities on the right side of (5.2.2). The stable-rank companion also links the Chapter 7 notion of intrinsic dimension to a concrete rectangular matrix statistic. Both the chapter's general theorems and this mission's statements remain Open on the platform; none is being presented as already machine proved. Tropp, §§5.2 and 7.2.2 gives the mathematical results.

Difficulty

Sampling both rows and columns introduces two interacting random projectors. Merely applying a one-stage column estimate to $B$ leaves the row selection uncontrolled; merely applying a one-stage row estimate leaves the sampled column norms random. The two families must be independent of each other as well as independent internally. That distinction is substantial: separate independence claims for the row family and the column family do not imply independence between $P$ and $R$ . The final estimate must also retain the book's exact $3$ and $2$ coefficients rather than replacing the right side by an unspecified constant times a simpler expression.

Formalization scope

Matrices are Matrix (Fin d) (Fin n) ℂ, matching the book's general complex-matrix convention. The spectral norm, extreme eigenvalues, Borel measurable matrix space, and intrinsic dimension come from tc's published definitions, which this mission references. Random selectors are measurable real-valued functions on a probability space; their Bernoulli law specifies almost-sure values zero or one and the probability of one. The row and column selectors form one jointly independent family. Products with diagonal selector matrices define $PB$ , $BR$ and $PBR$ ; a deterministic diagonal or an unconstrained zero-one function would not be the sampled model.

Every sampling rate is within its Bernoulli domain. Nonzero dimensions keep the maxima over finite, inhabited sets and give the logarithms their intended arguments. Lean's Bochner integral otherwise returns zero on a nonintegrable function; each expectation inequality records integrability in its conclusion, which follows from measurable, bounded Bernoulli selectors and Tropp's standing regularity convention in §2.2.1. The maxima of column, row, and entry magnitudes are real finite suprema, equal to maxima for these finite nonempty index sets. The intrinsic-dimension identity assumes $p>0$ and $B\ne0$ for scale invariance; the final stable-rank bound itself includes zero sampling and the zero matrix.

The definitions of Bernoulli selection, random diagonal projections, sampled matrices, finite norm maxima and stable rank are reusable outside this mission. Contributions can address their structural identities, integrability, the four milestones, the goal, or the independent column-selection companions. The book's constants $1.72$ and $0.63$ are retained as decimals; $3$ and $2$ are the rounded coefficients printed in (5.2.2), as the text explains on p. 66.

Selected references

Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, arXiv:1501.01571v1, §§2.1, 2.2, 5.1, 5.2, 7.2.
Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, DOI:10.1561/2200000048. The formalization cites the pinned arXiv version above for page and equation indices.

11 thms3 active usersReviewed

Completed

Combinatorics Linear algebra Random Matrix Theory·Captain: mikedeng1

An Introduction to Matrix Concentration Inequalities I: A Matrix Gaussian Series Satisfies v(Z) ≤ E‖Z‖² ≤ 2v(Z)(1 + log(d₁ + d₂))Textbook

Motivation

Random matrices arise when observations, signs, or model coefficients fluctuate. Their spectral norm measures the largest amplification they can cause to a vector. A bound on that norm can turn entrywise randomness into a statement about the behavior of an entire linear operator. Tropp's chapter develops a common framework for Gaussian and Rademacher sums of fixed matrices, then applies it to Wigner matrices, rectangular Gaussian matrices, random signs, Toeplitz matrices, and a rounding scheme for a quadratic optimization relaxation (Tropp, Chapter 4). The applications show what the general estimate says when the matrices have concrete structure.

The chapter's general matrix-series theorem, Theorem 4.1.1, is already an open statement in tc's Prove2Me Chapter 4 mission. This mission targets the squared-norm comparison in §4.1.2 and the worked consequences that are not part of that existing goal. They are useful benchmarks because their dimensions, coefficients, and variance statistics are explicit. The existing platform status is a formalization status: Tropp proves these mathematical bounds in the cited book; the Chapter 4 theorem and the results proposed here do not yet have machine-checked proofs.

Setting

Fix positive integers $d_1,d_2$ and a finite family of complex $d_1\times d_2$ matrices $B_k$ . Let $\gamma_k$ be independent standard Gaussian real variables, each with mean zero and variance one. Their matrix Gaussian series is $Z=\sum_k\gamma_k B_k$ . For a complex matrix $M$ , write $M^*$ for its conjugate transpose and $\|M\|$ for its Euclidean operator norm. The matrix variance statistic is

v(Z)=\max\{\|\mathbb E(ZZ^*)\|,\ \|\mathbb E(Z^*Z)\|\}.

For this Gaussian series, the two expected products equal the corresponding sums of coefficient products, so $v(Z)$ can be computed from the fixed $B_k$ . This is the same statistic and norm as Theorem 4.1.1, equations (4.1.2)–(4.1.4) (Tropp, p. 42). Expectations are entrywise Bochner integrals for matrix-valued functions and ordinary integrals for real quantities.

A Rademacher variable takes values $-1$ and $1$ with equal probability. Some companion examples replace the Gaussian coefficients by independent Rademacher variables. For a Hermitian square matrix $Y$ , $\lambda_{\min}(Y)$ denotes its smallest real eigenvalue. In the signed-entry example, the relevant matrix statistic is the larger of the greatest squared row norm and the greatest squared column norm of a fixed matrix.

Formalization targets

Squared norm of a Gaussian series

The goal is the pair of inequalities in (4.1.7), together with explicit integrability of the random squared norm:

v(Z)\le\mathbb E\|Z\|^2\le2v(Z)\bigl(1+\log(d_1+d_2)\bigr).

The constants and the logarithm are exactly those printed on pp. 43–44. The left side identifies a necessary scale; the right side gives a dimension-dependent upper estimate. The two milestones are the Jensen lower-bound display and the tail-integration display in §4.1.2. The latter is stated for any measurable matrix with the chapter's tail bound and positive variance, because the displayed integration step itself uses only those properties. It retains the exact split-point expression and the factor $2$ .

Worked series

Companion statements record the minimum-eigenvalue consequences (4.6.4)–(4.6.5), the Wigner estimate (4.2.3), the rectangular Gaussian estimate (4.2.6), the randomly signed-entry estimate (4.3.3), the Toeplitz estimate (4.4.3), and the MaxQP rounding scale in §4.5. Their deterministic variance identities are part of the statements, rather than assumptions. In particular the Wigner bound keeps $\log(2d)$ and the Toeplitz bound keeps the exact coefficient sum $dI_d$ (Tropp, pp. 46–52).

Significance

The squared-norm comparison says that $v(Z)$ is the correct baseline for the size of a Gaussian series in mean square, while allowing a logarithmic penalty for matrix dimension. It also shows why an expectation estimate and a tail estimate answer different questions: the chapter discusses examples where a tail bound can be loose even when the expected norm is controlled (Tropp, pp. 44–45). The example statements make the abstract variance statistic usable for standard matrix ensembles and for signed matrices with prescribed entries.

A machine-checked development would connect the existing spectral and probability definitions to explicit examples, finite-sum variance identities, and integrability of Gaussian matrix norms. Those components can be reused in later sampling and numerical linear algebra missions. The general Chapter 4 matrix-series theorem remains an open platform target; these application statements are not claimed to be already formalized or proved there.

Difficulty

The central obstacle is moving from a tail estimate for $\|Z\|$ to a finite, sharp expectation for $\|Z\|^2$ . The tail estimate has a dimension factor, while the desired bound has its logarithm; an unspecialized bound at a single threshold does not provide the stated constant. At the modeling level, matrix variance uses expectations of matrix products, so it must coincide with the finite sums of coefficient squares for each example. A definition that silently returns zero for a nonintegrable Bochner integral would make the upper inequality misleading. The Gaussian law, measurability, and moment behavior therefore matter to the statement as well as to eventual proofs.

Formalization scope

Matrices use Matrix (Fin d₁) (Fin d₂) ℂ with $d_1,d_2\ge1$ and tc's spectralNorm and rectSecondMoment definitions. The probability space is arbitrary; coefficient functions are measurable and independent, and their pushforward laws are exactly standard Gaussian or Rademacher as the page requires. Families may be empty. Real random coefficients scale complex matrices. Integrability of $\|Z\|^2$ is a conclusion of the goal and tail-integration milestone, while the minimum-eigenvalue expectation companion likewise asserts integrability. The tail-integration milestone assumes $v(Z)>0$ because its displayed denominator divides by $v(Z)$ ; the Gaussian goal itself includes $v(Z)=0$ .

The Wigner coefficients are indexed by pairs $i<j$ ; rectangular and signed-entry coefficients by row-column pairs; Toeplitz coefficients by diagonals $-(d-1),\ldots,d-1$ . The Toeplitz index in Lean is shifted to Fin (2*d-1). Row and column maxima range over the nonempty finite row and column sets. The signed-entry theorem permits complex fixed entries and uses $|b_{ij}|^2$ ; the printed example starts with real entries. MaxQP uses the positive scale $\alpha=1/\sqrt{2\log(d_1+d_2)}$ and tc's positive-semidefinite order for the two relaxation constraints. None of the coefficient-square identities is supplied as a hypothesis; each is a conclusion to establish.

Context. The existing TroppMatrixConcentration.ch4_matrix_series formalizes Theorem 4.1.1 and is Open. Its Gaussian/Rademacher variance identity and norm/tail bounds provide the chapter context. The present goal specializes the same Gaussian model and asks for the separate second-moment result (4.1.7). Reusable contributions include finite-matrix identities, Gaussian moment integrability, and tail-integration lemmas. A valid proof must preserve the actual standard laws and independence, and cannot redefine $v(Z)$ as the expected squared norm.

Selected references

Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, arXiv:1501.01571v1, Chapter 4, pp. 42–52.

8 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition VI: Randomized Proximal Coordinate Descent Has Expected Rate (1 − μ/(dL))^kResearch Paper

Motivation

Many problems in machine learning and statistics have the composite form $\min_x F(x)=f(x)+g(x)$ , where $f$ is a smooth loss and $g$ is a non-smooth regularizer such as $\lambda\|x\|_1$ . When $g$ is separable, $g(x)=\sum_i g_i(x_i)$ , the method of choice at scale is often randomized proximal coordinate descent: at each step one coordinate is drawn at random and a one-dimensional proximal problem is solved in that coordinate only. Each step is cheap, and the method underlies standard solvers for $\ell_1$ -regularized regression and for the dual of support vector machines.

Classical linear-convergence guarantees for this method assume strong convexity of $f$ or of $F$ (Richtárik and Takáč, 2014), or rely on the Kurdyka–Łojasiewicz property with constants that are hard to make explicit. Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) introduced the proximal-PL inequality, a generalization of the Polyak–Łojasiewicz condition to composite problems, and showed that it alone yields linear rates for proximal-gradient methods. Theorem 6 of that paper, the subject of this mission, extends the analysis to randomized proximal coordinate descent.

Timeline. Polyak (1963) and Łojasiewicz (1963) introduced the gradient-domination inequality for smooth problems. Nesterov (2012) analysed randomized coordinate descent for smooth convex problems; Richtárik and Takáč (2014) extended it to composite separable problems under strong convexity. Karimi, Nutini and Schmidt (2016) obtained the rate $(1-\mu/(dL))^k$ for the proximal coordinate method under proximal-PL alone (Theorem 6, p. 10, proof in Appendix H, p. 23).

Setting

Write $\mathbb R^d$ for the Euclidean space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ ; $x_i$ is the $i$ -th coordinate of $x$ , $e_i$ the $i$ -th basis vector, and $\nabla_i f(x)$ the $i$ -th coordinate of the gradient. The data are:

a differentiable $f:\mathbb R^d\to\mathbb R$ whose gradient is $L$ -Lipschitz, $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ , with $L>0$ ;
convex univariate functions $g_1,\dots,g_d:\mathbb R\to\mathbb R$ and the separable $g(x)=\sum_i g_i(x_i)$ ;
$F=f+g$ , which has a minimizer $x^*$ ; write $F^*=F(x^*)$ .

For $\alpha>0$ the quantity

\mathcal D_g(x,\alpha)=-2\alpha\min_y\Big[\langle\nabla f(x),y-x\rangle+\frac\alpha2\|y-x\|^2+g(y)-g(x)\Big]

measures the best decrease of a quadratic upper model of $F$ at $x$ . $F$ satisfies the proximal-PL inequality with constant $\mu>0$ if

\tfrac12\,\mathcal D_g(x,L)\ \ge\ \mu\,\big(F(x)-F^*\big)\qquad\text{for all }x.

The coordinate-wise proximal-gradient method starts at $x_0$ . At step $k$ it draws $i_k$ uniformly from $\{1,\dots,d\}$ , independently of the past, and sets $x_{k+1}=x_k+\alpha^\star e_{i_k}$ , where $\alpha^\star$ minimizes

\alpha\,\nabla_{i_k}f(x_k)+\frac L2\alpha^2+g_{i_k}(x_{k,i_k}+\alpha)-g_{i_k}(x_{k,i_k}).\tag{16}

Formalization targets

Goal: Theorem 6 (p. 10)

For every $k\ge0$ ,

\mathbb E\big[F(x_k)-F^*\big]\ \le\ \Big(1-\frac{\mu}{dL}\Big)^k\big[F(x_0)-F^*\big].\tag{17}

The constant $\mu/(dL)$ is the paper's; no further constant is fixed.

Milestones (Appendix H, p. 23)

(62), the coordinate upper model: $F(x+te_i)-F(x)\le t\nabla_i f(x)+\frac L2t^2+g_i(x_i+t)-g_i(x_i)$ .
The expected-improvement identity: $\frac1d\sum_i\min_{t}\big[t\nabla_i f(x)+\frac L2t^2+g_i(x_i+t)-g_i(x_i)\big]=-\frac1{2Ld}\mathcal D_g(x,L)$ .
(63), the expected descent: $\mathbb E[F(x_{k+1})\mid x_k=x]\le F(x)-\frac1{2Ld}\mathcal D_g(x,L)$ .

A companion statement (not a milestone, not in the paper) asserts that the one-dimensional step (16) exists for convex $g_i$ and $L>0$ .

Significance

The result. Theorem 6 gives a linear rate for proximal coordinate descent on every composite problem satisfying proximal-PL, a class that contains $\ell_1$ -regularized least squares and other problems that are not strongly convex. The rate matches that of plain randomized coordinate descent under PL (Theorem 3 of the paper) with the composite term added, and the factor $d$ is the usual price of updating one coordinate per step.

Formalizing it. The result is proved on paper; no machine-checked proof is known. A formal proof requires the coordinate descent lemma, the exchange of a separable minimum with a sum, and an exact accounting of the expectation over random index sequences. The definitions of $\mathcal D_g$ , proximal-PL and the random-coordinate run built here are reusable for other proximal and coordinate methods.

Difficulty

The one-step argument is short once the expected-improvement identity is available; the difficulty is in that identity. Its left side averages over coordinates the minima of one-dimensional models, while $\mathcal D_g$ is a minimum over the whole space. Equating them requires that the full-space minimum split across coordinates, which is where separability of $g$ is used, and that each minimum be attained, which requires convexity of the $g_i$ and $L>0$ . A second point is the expectation: the iterate after $k$ steps is a function of the whole index word $(i_0,\dots,i_{k-1})$ , and the one-step expected descent must be propagated through the tower of conditional expectations to the $k$ -step bound.

Formalization scope

The space is EuclideanSpace ℝ (Fin d) with $d\ge1$ (0 < d); the gradient is Mathlib's gradient f, and $\nabla_i f(x)$ is gradient f x i.
The Lipschitz gradient is the literal hypothesis $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ with $L>0$ and Differentiable ℝ f, as in the setup of Theorem 5. Appendix H uses only coordinate-wise Lipschitz continuity, which follows.
$X^*\neq\emptyset$ is a point $x^*$ minimizing $F$ ; $F^*$ is $F(x^*)$ , never a free real.
The $g_i$ are real-valued convex functions. Extended-valued $g_i$ (box indicators, used for the SVM dual in §4.4) are outside this formalization.
The minimum in $\mathcal D_g$ is a real infimum; it is attained, hence equal to the paper's minimum, for convex $g_i$ and $L>0$ , and every statement using it carries these hypotheses.
The update is any step selection $\mathrm{sel}(x,i)=x+t^\star e_i$ with $t^\star$ a minimizer of (16); the selection is a hypothesis-constrained parameter, never an arbitrary map. Equation (16) as printed assigns the minimizing step to $x_{k+1}$ ; the iterate $x_k+\alpha^\star e_{i_k}$ of Appendix H is what is encoded.
$\mathbb E[F(x_k)-F^*]$ is the exact average over all $d^k$ index words, each of probability $d^{-k}$ , which is the law of i.i.d. uniform coordinates.
A formalization that leaves the update unconstrained, takes $F^*$ as a free constant, or computes $\mathcal D_g$ as a junk infimum would make the goal false or vacuous; these are ruled out by the conventions above.

Contributions welcome: proofs of the three milestones and the goal, the existence of the coordinate step, and a version with extended-valued $g_i$ .

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
P. Richtárik, M. Takáč, Iteration complexity of randomized block-coordinate descent methods for minimizing a composite function, Mathematical Programming 144, 2014. https://doi.org/10.1007/s10107-012-0614-z
Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM J. Optim. 22(2), 2012. https://doi.org/10.1137/100802001
B. T. Polyak, Gradient methods for minimizing functionals, USSR Comput. Math. Math. Phys. 3(4), 1963. https://doi.org/10.1016/0041-5553(63)90382-3

7 thms3 active usersReviewed

Bandit Algorithms Machine Learning·Captain: mikedeng1

A Modern Introduction to Online Learning VIII: Tsallis-INF Has Adversarial Regret 32L∞√((d − 1)T) and Stochastic Pseudo-Regret 256L∞² Σ_i (1 + ln T)/Δ_iTextbook

Why bandit feedback matters

In online learning with bandit feedback, the learner chooses one action and sees only that action's loss. This is the information pattern of sequential trials in which testing one option does not reveal the outcomes of the others. The learner must keep its cumulative loss close to that of a good fixed action while learning which actions are good. A full-information method can update from every arm's loss each round; here the unseen losses have to be handled through the observations the learner actually receives. Chapter 9 of Orabona's text develops this distinction for multi-armed bandits.

Two environments are treated in the chapter. With an oblivious adversary, all losses are fixed before play, although the learner does not know them. With a stochastic environment, each arm has a fixed loss distribution and new losses are drawn across rounds. An algorithm with a guarantee in both environments does not need to be told which generated its data. Theorem 9.17 gives such a pair of guarantees for the FTRL version of Tsallis-INF, using the precise constants stated in the pinned version of the book.

Arms, losses, and the algorithm

There are $d$ arms and $T$ rounds, numbered $1,\ldots,T$ . In round $t$ , the learner forms a probability vector $x_t=(x_{t,1},\ldots,x_{t,d})$ on the simplex $\Delta^{d-1}$ , draws an arm $A_t$ with probability $x_{t,i}$ of choosing $i$ , and observes only $g_{t,A_t}$ . The loss $g_{t,i}$ of an unchosen arm is not revealed. For an oblivious adversary, the entire table $(g_{t,i})$ is deterministic and the expectation is over the learner's draws.

Algorithm 9.6 uses the importance-weighted estimate $\widetilde g_{t,i}=g_{t,i}/x_{t,i}$ if $A_t=i$ , and $0$ otherwise. Its Tsallis-INF FTRL prediction minimizes, over $x\in\Delta^{d-1}$ ,

\left\langle\sum_{s=1}^{t-1}\widetilde g_s,x\right\rangle -4L_\infty\sqrt t\sum_{i=1}^{d}\sqrt{x_i}.

The minimizer has positive coordinates. Thus each denominator $x_{t,i}$ used by the estimator is positive. In the stochastic environment, arm $i$ has mean $\mu_i$ ; if $j$ is a best arm, its gap is $\Delta_i=\mu_i-\mu_j$ . The pull count $S_{T,i}$ is the number of rounds through $T$ in which arm $i$ is selected. Stochastic pseudo-regret compares the learner's expected loss with $T\mu_j$ , the expected loss of always playing the best arm.

Formalization targets

The mission's main theorem is the adversarial claim of Theorem 9.17, p. 165. For every fixed comparator arm $k$ and losses in $[0,L_\infty]$ ,

\mathbb E\!\left[\sum_{t=1}^{T}(g_{t,A_t}-g_{t,k})\right] \le 32L_\infty\sqrt{(d-1)T}.

Taking $k$ to be the best arm in the fixed loss table yields the stated adversarial regret bound. The companion item formalizes the second claim of the same theorem: if the losses are stochastic with a unique best arm and $T\ge1$ , then

\mathrm{P\!\operatorname{-}Regret}_T \le256L_\infty^2\sum_{i:\Delta_i\ne0}\frac{1+\ln T}{\Delta_i}.

The milestone list contains the chapter's pseudo-regret decomposition (Lemma 9.10), its sub-Gaussian sample-mean bound (Corollary 9.9, reused from an existing formal statement), and the probability-sensitive Tsallis-INF inequality (9.8). These are distinct mathematical claims rather than alternate names for the final bound.

What the result provides

The adversarial bound grows like $\sqrt{T}$ and remains valid for any fixed bounded loss table. The stochastic bound instead measures the difficulty of distinguishing arms through the positive gaps $\Delta_i$ and grows logarithmically with the horizon for fixed gaps. Both refer to the same FTRL update and the same importance-weighted estimator. The finite-horizon constants $32$ and $256$ are part of the target, not unspecified factors hidden in asymptotic notation.

Both claims are proved in the book. The work here is to give their hypotheses, random experiment, and algorithm a machine-checkable Lean interface, then formalize the known arguments. At this drafting stage the theorem bodies are open Lean problems; a successful build checks that their statements are well formed, not that the regret bounds have been proved. The resulting finite-history bandit protocol and stochastic pseudo-regret definitions can also support other loss-based bandit algorithms. The existing formalized sub-Gaussian tail bound can be reused for concentration results elsewhere in the chapter.

Where the proof is difficult

The learner observes only one coordinate, while regret is measured against losses across all arms. The importance-weighted estimate corrects the missing observations in expectation, but its size can grow when a selected arm has small probability. Consequently, a bound based only on a uniform estimate of its magnitude loses the probability dependence needed for the theorem's constants. The stochastic claim adds another difficulty: the learner's choices depend on past observed losses, so a current loss must be related to a random pull count without letting the choice depend on that current loss.

There are two tempting but invalid shortcuts. Permitting $x_t$ to inspect $g_t$ would change the bandit protocol, and taking an expectation under an arbitrary path measure would no longer describe the arm draws of Algorithm 9.6. The formal statements tie each prediction to its FTRL objective and each path probability to the predictions made along that history.

Formalization scope

Arms are Fin d; the main theorem permits $d=1$ , where both its regret and bound are zero. Rounds retain the book's $1,\ldots,T$ indexing. A finite path has a dummy coordinate zero, fixed to an arbitrary anchor arm; this coordinate is never played or scored. The adversarial losses are a fixed table, selected before any draw. A path has probability equal to the product of the algorithm's conditional arm probabilities, and regret against a fixed arm is a finite weighted sum over paths. The FTRL run predicate requires simplex membership, strict positivity, minimization against every simplex point, and dependence only on past arm choices. The last two properties specify the intended update on every possible history.

The stochastic model first samples a loss table from a probability measure and then draws an arm path conditionally using the same Algorithm 9.6. Current-round loss vectors are independent across rounds, while coordinates within one round need not be independent. Each arm has the same mean in every round. The policy is a measurable function of the observed history (past arms and their losses); its expected loss is explicitly integrable. Loss bounds are imposed on every outcome in the chosen sample space, which can be taken as the support of bounded distributions. The stochastic statement adds $T\ge1$ to make the logarithmic formula's domain explicit, and the unique-best-arm assumption ensures every denominator $\Delta_i$ in the displayed sum is positive. Lemma 9.10 also spells out the integrability of its means and pull counts.

The development needs finite probability laws, real integrals, simplex geometry, and properties of the square-root regularizer. The independent tail bound for sample means is already available as a referenced theorem. Contributions that establish existence and interiority of the FTRL minimizer, the normalization of the path law, or the stated regret inequalities fit this scope. A choice rule that sees the current loss, a path law unrelated to $x_t$ , or a zero integrability default does not satisfy the intended bandit model.

Selected references

Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 9, pp. 151–169. arXiv

6 thms3 active usersReviewed

Bandit Algorithms Machine Learning Reinforcement Learning·Captain: mikedeng1

Provably Efficient Reinforcement Learning with Linear Function Approximation 2: LSVI-UCB Has Regret O(√(d³H³Tι²) + ζdHT√ι) on ζ-Approximately Linear MDPsResearch Paper

Motivation

Reinforcement learning with large or continuous state spaces relies on function approximation: value functions are represented as functions of a $d$ -dimensional feature map instead of tables indexed by states. Before 2019, regret guarantees for exploration with function approximation either needed strong assumptions (deterministic dynamics, a generative model) or applied only to tabular problems. Jin, Yang, Wang and Jordan (arXiv:1907.05388, COLT 2020) showed that in a linear MDP, where transitions and rewards are linear in known features, an optimistic version of least-squares value iteration, LSVI-UCB, has regret $\tilde O(\sqrt{d^3H^3T})$ , with no dependence on the number of states or actions (Theorem 3.1).

Exact linearity is rarely satisfied by features chosen in practice. A guarantee that collapses under a small modelling error would say little about real use, and a naive adaptation of linear-bandit methods can break down entirely when the model is wrong. Theorem 3.2 of the same paper addresses this: if the MDP is only $\zeta$ -approximately linear, LSVI-UCB with an episode-dependent bonus still has sublinear regret plus an additive term linear in $\zeta T$ . This mission formalizes that result. A companion mission formalizes Theorem 3.1.

Setting

An episodic MDP has a measurable state space $\mathcal S$ , a finite action set $\mathcal A$ , a horizon $H$ , and for each step $h\in[H]$ a transition kernel $\mathbb P_h(\cdot\mid x,a)$ and a reward $r_h:\mathcal S\times\mathcal A\to[0,1]$ . A policy $\pi$ chooses an action $\pi(x,h)$ at state $x$ and step $h$ . Its value functions satisfy the Bellman equation

Q^\pi_h(x,a)=r_h(x,a)+\int V^\pi_{h+1}\,\mathrm d\mathbb P_h(\cdot\mid x,a),\qquad V^\pi_h(x)=Q^\pi_h(x,\pi(x,h)),\qquad V^\pi_{H+1}=0,

and $V^\star_h(x)=\max_aQ^\star_h(x,a)$ is the optimal value, with $Q^\star$ defined by the same recursion.

A feature map $\phi:\mathcal S\times\mathcal A\to\mathbb R^d$ with $\|\phi\|\le1$ makes the MDP $\zeta$ -approximately linear (Assumption B) if for every step $h$ there are signed measures $\mu_h=(\mu_h^{(1)},\dots,\mu_h^{(d)})$ on $\mathcal S$ and a vector $\theta_h$ with

\big\|\mathbb P_h(\cdot\mid x,a)-\langle\phi(x,a),\mu_h(\cdot)\rangle\big\|_{\mathrm{TV}}\le\zeta,\qquad|r_h(x,a)-\langle\phi(x,a),\theta_h\rangle|\le\zeta

for all $(x,a)$ , together with the normalization $\|\theta_h\|\le\sqrt d$ and a $\sqrt d$ bound on the masses of $\mu_h$ . At $\zeta=0$ this is a linear MDP.

LSVI-UCB (Algorithm 1) plays $K$ episodes. In episode $k$ , with data $\phi^\tau_h=\phi(x^\tau_h,a^\tau_h)$ from earlier episodes, it computes backwards from $Q^k_{H+1}\equiv0$

\Lambda^k_h=\sum_{\tau<k}\phi^\tau_h(\phi^\tau_h)^\top+\lambda I,\qquad w^k_h=(\Lambda^k_h)^{-1}\sum_{\tau<k}\phi^\tau_h\big[r_h(x^\tau_h,a^\tau_h)+\max_aQ^k_{h+1}(x^\tau_{h+1},a)\big],

Q^k_h(x,a)=\min\big\{\langle w^k_h,\phi(x,a)\rangle+\beta_k\|\phi(x,a)\|_{(\Lambda^k_h)^{-1}},\,H\big\},

and then acts greedily, $a^k_h=\arg\max_aQ^k_h(x^k_h,a)$ . An adversary may choose each initial state $x^k_1$ . The regret after $K$ episodes is

\mathrm{Regret}(K)=\sum_{k=1}^K\big[V^\star_1(x^k_1)-V^{\pi_k}_1(x^k_1)\big],

where $\pi_k$ is the greedy policy of episode $k$ . Throughout, $T=KH$ and $\iota=\log(2dT/p)$ .

Formalization targets

Goal: Theorem 3.2

There are absolute constants $c,C>0$ such that for every $\zeta$ -approximately linear MDP, every $p\in(0,1)$ and every run of LSVI-UCB with $\lambda=1$ and $\beta_k=c\,(d\sqrt\iota+\zeta\sqrt{kd})H$ , with probability at least $1-p$ ,

\mathrm{Regret}(K)\le C\Big(\sqrt{d^3H^3T\iota^2}+\zeta dHT\sqrt\iota\Big).

The constants are not fixed numerically, so improvements of the constants in the proof do not invalidate the target.

Milestones

The milestones follow Appendix C: the approximate linearity of $Q^\pi$ (Lemma C.1) and the bound on its weights (Lemma C.2); the trace inequality D.1 and the adversarial-noise bound C.4; the self-normalized concentration bound D.3 (published) and the concentration event of Lemma C.3; the key estimate C.5; approximate optimism C.6; the recursive formula C.7; and the elliptical potential lemma D.2 (published) with the bonus-sum bound (21)–(24).

Significance

Theorem 3.2 shows that the regret of LSVI-UCB degrades gracefully under misspecification: the extra cost is of order $\zeta dHT\sqrt\iota$ , linear in $T$ because of the bias of linear approximation and negligible when $\zeta\lesssim1/\sqrt T$ . The paper also converts it into a PAC guarantee with an additive $\tilde O(\zeta dH^2)$ error. It is a reference point for later work on misspecified linear bandits and RL, which asks how far the linear term can be improved.

The result is proved on paper; no machine-checked proof is known. The formalization supplies an episodic MDP on a general measurable state space, LSVI-UCB as a function of the observed data, and its interaction with an adaptive adversary on a filtered probability space. These are shared with the companion mission on Theorem 3.1 and are reusable for other optimistic algorithms with linear function approximation. At $\zeta=0$ the goal specializes to Theorem 3.1 under the same normalization; this is a consistency check, not a dependency.

Difficulty

The central difficulty is that the regression targets $r_h+V^k_{h+1}(x^\tau_{h+1})$ depend on the data through $V^k_{h+1}$ , which is computed from all earlier episodes. A martingale concentration bound for a fixed function does not apply. Lemma C.3 needs a bound that holds uniformly over the class of functions LSVI-UCB can produce, which requires a covering-number argument whose size depends on $\beta_k$ ; that is why the constant $C$ must be independent of $c_\beta$ and $c_\beta$ is chosen afterwards. Under misspecification a second error appears: the deviations $r_h-\langle\phi,\theta_h\rangle$ and $(\mathbb P_h-\langle\phi,\mu_h\rangle)V$ are not mean-zero and can be adversarial, so they cannot be concentrated away. Lemma C.4 absorbs them into the bonus at the price of the $\zeta\sqrt{kd}$ term in $\beta_k$ . Optimism then holds only up to an error that accumulates over the horizon (Lemma C.6).

Formalization scope

Indices are 1-based, as on the page; values and estimates are $0$ outside $1\le h\le H$ .
Values: $V^\pi$ and $V^\star$ are defined by the Bellman recursions (1) and (2), not by $\sup_\pi$ .
Measurability: the state space is a bare measurable space. Features $\phi(\cdot,a)$ are assumed measurable, and lemmas about a policy $\pi$ assume it measurable, so that every integral is meaningful.
Actions: $\mathcal A$ is finite and nonempty. Argmax ties are broken towards the least action of a fixed linear order on $\mathcal A$ .
Interaction: the run is a process adapted to an arbitrary filtration, with actions given by Algorithm 1 and the next-state law holding conditionally on the past. The initial states are only required to be adapted.
Probability statements: "with probability $1-p$ " is "the bad set has (outer) measure at most $p$ ".
Constants: $c$ and $C$ are quantified before all types, dimensions, horizons, $\zeta$ , $p$ and runs. The hypotheses $d,H,K\ge1$ and $0\le\zeta\le1$ are stated.
Assumption B measures the TV distance by the total variation norm $|\nu|(\mathcal S)$ . The page's normalization $\|\mu_h(\mathcal S)\|\le\sqrt d$ is replaced by the same bound on the vector of total variations $(|\mu_h^{(i)}|(\mathcal S))_i$ , because Lemma C.2 is false under the printed form; the replacement implies the printed condition and holds for tabular MDPs.
Lemma C.7 carries the $+4H\zeta$ term that its own proof derives; the printed statement omits it. Theorem 3.2 is unaffected.

Lemmas C.3 and C.5 are formalized as printed. Their proofs use $\sup_x|V^k_{h+1}(x)|\le H$ , which Algorithm 1 does not enforce from below; a solver may find that one of them needs an additional argument.

A formalization in which the goal assumes the event $\mathfrak E$ , the optimism of Lemma C.6 or the recursion of Lemma C.7, or in which the run does not fix the actions to Algorithm 1's, would be trivial or false; the goal assumes none of these. Contributions are welcome on the linear-algebra lemmas (D.1, C.4, (21)–(24)), on measurability of the LSVI-UCB estimates, and on the covering argument behind Lemma C.3.

Selected references

C. Jin, Z. Yang, Z. Wang, M. I. Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020; arXiv:1907.05388v2, 2019. https://arxiv.org/abs/1907.05388
Y. Abbasi-Yadkori, D. Pál, C. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
L. F. Yang, M. Wang, Sample-Optimal Parametric Q-Learning Using Linearly Additive Features, ICML 2019; arXiv:1902.04779. https://arxiv.org/abs/1902.04779

16 thms3 active usersReviewed

Completed

Machine Learning Optimization·Captain: mikedeng1

Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition III: Randomized Coordinate Descent Has Expected Rate (1 − μ/(dL))^kResearch Paper

Motivation

Coordinate descent changes one component of a parameter vector at a time. This matters when evaluating or updating a single component is cheaper than handling the full vector, for example in problems with sparse features. The coordinate chosen at each step can be random or selected from the current gradient. Karimi, Nutini, and Schmidt study these choices for objectives that satisfy a Polyak–Łojasiewicz (PL) inequality, a condition that controls objective error by the size of the gradient without assuming convexity. Their Theorem 3 gives an explicit expected rate for uniform random coordinates, while §3.2 gives a rate for the greedy Gauss–Southwell choice. Karimi, Nutini, and Schmidt (2016), §3

The question is how much of the familiar full-gradient linear rate survives when an update sees only one coordinate. The theorem answers this with a dimension factor: each uniform draw accesses one of $d$ coordinates, and the rate depends on $\mu/(dL)$ . The same paper relates the greedy rule to earlier work on coordinate descent and boosting; this mission treats its stated greedy rate as a companion result, using the same coordinate update. Karimi, Nutini, and Schmidt (2016), §§3.1–3.2

Setting

Let $d\ge1$ , and let $f:\mathbb R^d\to\mathbb R$ be differentiable. Write $\nabla_i f(x)$ for coordinate $i$ of its gradient and $e_i$ for the corresponding standard basis vector. The paper's coordinate-wise upper bound (5), with $L>0$ , is

f(x+\alpha e_i)\le f(x)+\alpha\nabla_i f(x)+\frac L2\alpha^2 \quad\text{for every }x\in\mathbb R^d,\ i\in\{1,\ldots,d\},\ \alpha\in\mathbb R.

Here $i$ ranges over the $d$ coordinates. The bound concerns motion along one coordinate. It is the exact smoothness condition used in Theorem 3. Let $x^*$ be a global minimizer and put $f^*=f(x^*)$ ; thus the solution set is nonempty and $f^*$ is an attained optimal value. The PL inequality (3) with $\mu>0$ says

\frac12\|\nabla f(x)\|^2\ge\mu\bigl(f(x)-f^*\bigr) \quad\text{for every }x\in\mathbb R^d.

The randomized coordinate-descent step (6) draws $i_k$ uniformly from the $d$ coordinates, independently at each time, and sets $x_{k+1}=x_k-L^{-1}\nabla_{i_k}f(x_k)e_{i_k}$ . The initial point $x_0$ is arbitrary. For $k$ draws, expectation means the average over all $d^k$ words $(i_0,\ldots,i_{k-1})$ , each assigned weight $d^{-k}$ . In particular, at $k=0$ the empty word has weight one and the iterate is $x_0$ .

The Gauss–Southwell rule instead chooses a coordinate with the largest $|\nabla_i f(x_k)|$ ; ties may be resolved in any way. Its rate uses a PL inequality in the maximum-coordinate norm, $\|\nabla f(x)\|_\infty=\max_i|\nabla_i f(x)|$ , with constant $\mu_1>0$ . Karimi, Nutini, and Schmidt (2016), pp. 5–6

Formalization targets

Theorem 3: uniform random coordinates

For every $k\ge0$ , the goal is the paper's expected suboptimality bound

\mathbb E[f(x_k)-f^*] \le\left(1-\frac{\mu}{dL}\right)^k\bigl(f(x_0)-f^*\bigr).

The target includes the specific update (6), the coordinate condition (5), and the PL inequality (3). The three milestones are the paper's displayed one-coordinate decrease, its uniform expected decrease involving $\|\nabla f(x)\|^2$ , and the resulting conditional expected gap contraction. They are indexed to the proof of Theorem 3 on page 5. Karimi, Nutini, and Schmidt (2016), Theorem 3 and proof

Greedy coordinate choice

The companion target is the rate stated in §3.2 when the maximum-norm PL inequality holds:

f(x_k)-f^* \le\left(1-\frac{\mu_1}{L}\right)^k\bigl(f(x_0)-f^*\bigr).

This bound applies to any run that chooses a maximizing coordinate at every step. The different PL modulus is part of the statement; it need not equal the modulus $\mu$ in Theorem 3. Karimi, Nutini, and Schmidt (2016), §3.2

Significance

Theorem 3 gives a quantitative guarantee for a method that reads one gradient component per update. The guarantee depends on the attained optimum, the coordinate smoothness constant, the PL modulus, and the number of coordinates. It applies to objectives satisfying PL even when convexity is unavailable. The companion result records how the stated rate changes when the coordinate is selected by the largest gradient component and the PL condition is measured in the corresponding dual norm. Karimi, Nutini, and Schmidt (2016), §3

The paper proves these claims, but this mission asks for machine-checked proofs of their exact hypotheses and constants. A complete development will make the finite random experiment explicit and give reusable definitions for coordinate updates and expectations of finite coordinate-choice histories. The PL predicate is already published in the theorem library; the coordinate model and the results here remain to be formalized.

Difficulty

A bound for a single coordinate update depends on one component of the gradient. An arbitrary coordinate can have a zero component even when the full gradient is large, so a pointwise decrease with the full gradient norm cannot be asserted for every choice. The theorem instead concerns the expectation over a uniform choice and then over the complete history of choices. The main formal difficulty is keeping those two levels of expectation aligned with a state $x_k$ that itself depends on earlier draws. For the greedy companion, the selected coordinate may not be unique; the statement must cover every maximizing choice without assuming a fixed tie-breaking rule.

Formalization scope

The vector space is EuclideanSpace ℝ (Fin d). The shared definitions give (5), the step (6), the iterate produced by a word Fin k → Fin d, and the expected gap as a real finite sum. The published ShiOptRates.PolyakLojasiewicz predicate represents (3) after multiplying both sides by two. Every theorem using uniform draws assumes $d>0$ ; every step with $1/L$ assumes $L>0$ . The goal also states differentiability, an explicit global minimizer, and $\mu>0$ . No convexity is assumed. A free real number called $f^*$ would change the PL condition and could invalidate the rate, so the formal statement uses $f(x^*)$ throughout.

The index-word average is an exact finite representation of independent uniform sampling, including $k=0$ . It does not sample coordinates without replacement. The companion theorem represents the maximum-norm PL condition by requiring its inequality at every maximizing coordinate, which is equivalent for $d>0$ , and quantifies over every run satisfying the Gauss–Southwell update relation. Useful contributions include proofs of the three displayed milestones, the passage from one draw to the word average, and the greedy companion. The paper's optional remark on sampling proportional to coordinate-specific constants $L_i$ and its exact-coordinate-minimization remark are outside this proposal.

Selected references

H. Karimi, J. Nutini, and M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD, 2016; arXiv:1608.04636v4.

7 thms3 active usersReviewed

Completed

Machine Learning Operations Research Optimization·Captain: mikedeng1

Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming 1: The Randomized Stochastic Gradient Method Has (1/L)E‖∇f(x_R)‖² ≤ (D_f² + σ²Σγ_k²)/Σ(2γ_k − Lγ_k²)Research Paper

Motivation

Stochastic gradient methods are the standard tool for minimizing an objective that can only be accessed through noisy gradient samples. Training a machine-learning model on sampled data, simulation-based optimization, and stochastic programs with endogenous uncertainty are all of this kind. In many of these applications the objective is nonconvex: the loss or the regularizer of a learning problem may be nonconvex, as may the expected cost of a simulation model.

Before 2013 the complexity theory of stochastic approximation (SA) was essentially a convex theory. Robbins and Monro (1951) introduced the method. Polyak and Juditsky (1992) and Nemirovski, Juditsky, Lan and Shapiro (2009) established optimal rates for convex problems, and Lan (2012) unified the smooth, nonsmooth and stochastic convex cases. None of these results covered nonconvex objectives. Ghadimi and Lan (2013) gave the first non-asymptotic complexity bound for a stochastic gradient method on a smooth nonconvex problem. The bound is stated for the expected squared gradient norm at a randomly chosen iterate, and it is the result this mission formalizes.

Setting

The problem is

f^*=\inf_{x\in\mathbb R^n} f(x),

where $f:\mathbb R^n\to\mathbb R$ is differentiable and bounded below, and its gradient is $L$ -Lipschitz: $\|\nabla f(y)-\nabla f(x)\|\le L\|y-x\|$ for all $x,y$ . This class is written $\mathcal C^{1,1}_L(\mathbb R^n)$ . The function need not be convex.

The gradient is accessible only through a stochastic first-order oracle: at the $k$ -th query point $x_k$ it returns $G(x_k,\xi_k)$ , where $\xi_1,\xi_2,\dots$ are random variables and $G$ is a Borel function. Assumption A1 asks that for every $k\ge1$ , conditionally on the past, $G(x_k,\xi_k)$ is an unbiased estimate of $\nabla f(x_k)$ , and that its error $\delta_k=G(x_k,\xi_k)-\nabla f(x_k)$ has second moment $\mathbb E\|\delta_k\|^2\le\sigma^2$ . The noise variables need not be independent of each other or of the iterates.

The randomized stochastic gradient (RSG) method takes an initial point $x_1$ , an iteration limit $N$ , stepsizes $\gamma_k$ and a probability mass function $P_R$ on $\{1,\dots,N\}$ . It draws a random index $R\sim P_R$ , runs

x_{k+1}=x_k-\gamma_k\,G(x_k,\xi_k),\qquad k=1,\dots,R,

and outputs $x_R$ . The mass function used in the main theorem is

P_R(k)=\frac{2\gamma_k-L\gamma_k^2}{\sum_{j=1}^N(2\gamma_j-L\gamma_j^2)},\qquad k=1,\dots,N.

The constants are $D_f=[2(f(x_1)-f^*)/L]^{1/2}$ and, in the convex case with minimizer $x^*$ , $D_X=\|x_1-x^*\|$ .

Formalization targets

Goal: Theorem 2.1 a)

If $0<\gamma_k<2/L$ for $k=1,\dots,N$ , $N\ge1$ , and $R$ has the mass function above, then under Assumption A1

\frac1L\,\mathbb E\big[\|\nabla f(x_R)\|^2\big]\le\frac{D_f^2+\sigma^2\sum_{k=1}^N\gamma_k^2}{\sum_{k=1}^N(2\gamma_k-L\gamma_k^2)},

where the expectation is over $R$ and the noise. Any stepsize sequence below $2/L$ is allowed, so the goal does not fix a step rule, and the step rules of the paper's corollaries follow from it.

Milestones

The quadratic bound (1.6): $|f(y)-f(x)-\langle\nabla f(x),y-x\rangle|\le\frac L2\|y-x\|^2$ (already proved on the platform).
The one-step inequality (2.8) and its pathwise sum (2.9).
The conditional mean-zero property (2.10), $\mathbb E[\langle\nabla f(x_k),\delta_k\rangle\mid\xi_{[k-1]}]=0$ .
The averaged bound (2.11), $\sum_k(\gamma_k-\frac L2\gamma_k^2)\,\mathbb E\|\nabla f(x_k)\|^2\le f(x_1)-f^*+\frac{L\sigma^2}{2}\sum_k\gamma_k^2$ .
The weighting identity: $\mathbb E\|\nabla f(x_R)\|^2$ equals the $P_R$ -weighted average of $\mathbb E\|\nabla f(x_k)\|^2$ .
For the convex companion: co-coercivity (1.8) (already proved on the platform) and its consequence (2.12), $\frac1L\|\nabla f(y)\|^2\le\langle\nabla f(y),y-x^*\rangle$ when $\nabla f(x^*)=0$ .

Companion statements

Theorem 2.1 b) bounds $\mathbb E[f(x_R)-f^*]$ by $(D_X^2+\sigma^2\sum\gamma_k^2)/\sum(2\gamma_k-L\gamma_k^2)$ when $f$ is convex with a minimizer. Corollary 2.2 specializes both bounds to the stepsizes $\gamma_k=\min\{1/L,\tilde D/(\sigma\sqrt N)\}$ :

\frac1L\,\mathbb E\|\nabla f(x_R)\|^2\le\frac{LD_f^2}{N}+\Big(\tilde D+\frac{D_f^2}{\tilde D}\Big)\frac{\sigma}{\sqrt N},

and the analogous bound with $D_X$ for $\mathbb E[f(x_R)-f^*]$ in the convex case.

Significance

Theorem 2.1 a) is the basic guarantee for stochastic gradient descent on smooth nonconvex objectives. With the stepsizes of Corollary 2.2 it shows that $O(\sigma^2/\epsilon^2)$ oracle calls suffice to reach $\mathbb E\|\nabla f(x_R)\|^2\le\epsilon$ . The paper builds two further methods on it: a two-phase variant with large-deviation guarantees, and a zeroth-order variant (RSGF) that uses Gaussian smoothing when only function values are available. Later analyses of variance-reduced and adaptive stochastic methods for nonconvex problems measure their improvements against this bound.

The result is proved on paper; no machine-checked proof of it is known. A formalized fixed-step bound of the form "some iterate among the first $K$ has small expected squared gradient" exists, but it is a different statement: it has no randomized output and no general stepsizes. A complete formalization would check the measure-theoretic content that the paper treats informally: integrability of the iterates' gradients, the conditional-expectation step under dependent noise, and the role of the independence of $R$ .

Difficulty

The algebra of (2.8)–(2.9) is routine. The difficulty is in the probability. The noise may depend on the past, so the cross term $\langle\nabla f(x_k),\delta_k\rangle$ vanishes only in conditional expectation, and only once $x_k$ is known to be measurable with respect to the past. Its integrability is not assumed anywhere: $\nabla f(x_k)$ must be shown to have a finite second moment from the recursion, the Lipschitz gradient and Assumption A1. The randomized output adds a second step, where $\mathbb E\|\nabla f(x_R)\|^2$ is rewritten as a weighted average. This needs $R$ independent of the noise, and $\|\nabla f(x_k)\|^2$ has to be exhibited as a measurable function of the noise sequence. A proof that replaces $x_R$ by the deterministic weighted average skips exactly this step.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $f\in\mathcal C^{1,1}_L$ is the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth f g L, with the gradient given as a map $g$ . $f^*$ is the greatest lower bound of the range of $f$ , not an arbitrary lower bound.
Indices are 1-based. The iterates satisfy $x_1$ given and $x_{k+1}=x_k-\gamma_kG(x_k,\xi_k)$ for $k\ge1$ , pointwise on the sample space. The noise takes values in a general measurable space.
Assumption A1 is stated along the trajectory and in conditional form, with respect to any filtration to which the noise is adapted. The paper's history filtration $\sigma(\xi_1,\dots,\xi_k)$ is one admissible choice. Every conditional expectation and every integral in a hypothesis comes with an integrability clause. Every bounded expectation in a conclusion comes with an integrability conjunct.
The output index $R$ is a measurable random variable with values in $\{1,\dots,N\}$ and law $P_R$ . It is assumed independent of the whole noise sequence; the paper leaves this implicit (Step 0 draws $R$ before any oracle call).
Added hypotheses, all implicit on the page: $L>0$ ; $\gamma_k>0$ ; independence of $R$ . In Corollary 2.2 the stepsize (2.13) is read as $\gamma_k=1/L$ when $\sigma=0$ , the paper's convention $\tilde D/0=+\infty$ , because Lean's $\tilde D/0=0$ would otherwise give $\gamma_k=0$ .
The goal concerns the integral of $\|\nabla f(x_{R(\omega)}(\omega))\|^2$ over the sample space. A statement about the weighted sum of $\mathbb E\|\nabla f(x_k)\|^2$ with $R$ removed, or one that drops the integrability conjunct, would trivialize the randomized output and does not formalize the goal.
Infrastructure: measurability of the iterates as functions of the noise, the pull-out property of conditional expectation for inner products, and a second-moment induction along the recursion. These are reusable for the paper's two-phase and zeroth-order methods and for other stochastic-approximation analyses. Proofs of any milestone, or of the integrability lemmas on their own, are welcome.

Selected references

S. Ghadimi and G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4), 2341–2368, 2013. Preprint arXiv:1309.5549v1 (cited version). https://arxiv.org/abs/1309.5549
H. Robbins and S. Monro, A stochastic approximation method, Ann. Math. Statist. 22(3), 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
B. T. Polyak and A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
A. Nemirovski, A. Juditsky, G. Lan and A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19(4), 1574–1609, 2009. https://doi.org/10.1137/070704277
G. Lan, An optimal method for stochastic composite optimization, Math. Program. 133, 365–397, 2012. https://doi.org/10.1007/s10107-010-0434-y
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

13 thms3 active usersReviewed